Speculation -spec-type=coverage not working on one example.

[rasoolmaghareh]

@sanghu1790, I moved your message to a new issue. I think the two issues in speculation are different.

Hi Rasool and Linh,

I experimented the program for the speculation slowness issue. I ran "Mpals6-B2-cil.c" program which is big in size, but to see the difference I found it suitable. Later we can reduce the size or take some other small program.

After my current investigation and recalling previous conversations, the issue of slowness is due to running a program with and without providing "Spec_Avoid" files (these are dependent files after prepossessing). I ran the programs with and without Spec_Avoid file on following commits:

1. master-0df7858a09741d0e19809dcc1a19fffd1179e445
2. spec_custom_dyn-cfeb033c8912a8ce6ba84ed2b3f1117915fe40d3(most-recent)
3. spec_custom_dyn-ab4f9fb8cc0869e99a507b2512c97a505266b255(two-commits-back)

A. For the experiment with Spec_Avoid files on 1, 2, and 3, all finished in 35 sec approx. And also I see their stats are also same. But, some numbers in spec.txt files of all these three results are little changed, that I think we can check, why it had happened.

B. For the experiment without Spec_Avoid files on 1 and 3 above are very slow (THE PROBLEM WE ARE DEALING), whereas for 2, it is very fast and finished in 34 sec approx, just like happened in A above. Also, here the info stats and spec.txt files are very different.

From the above investigation, I have observed that "Removing Independence checks" and without Spec_Avoid files works very faster as compared to others. My question is why providing dependency files or not so much matter in performance? If we provide dependency files then the checking time should be more so it should be more expensive, but if we dont provide any such files so still it should be faster. At least the master branch should be align with spec_custom_dyn (most recent) branch. But, I remember this during the preparation of master branch we took the decision to not to "Removing Independence checks" from speculation sub-tree. Now, we can discuss after looking into consequences.

Still, @Linh, please check why our metrics stats of info and spec.txt files of these are different. Is there any mistake or every thing is fine.

@Rasool, Just to tell you, if you remember I encountored this issues because we were trying to run spec, with different number of Spec_Avoid files (like all files, no files, only one file, deleting one file) etc. And our observation was different performance on different runs. Then we discussed and agreed that, if we dont provide any files still it should work fine, but this is not the case now in master branch.

All, files and results are in zip folder, have a look. Speculation-fix.zip

I ran with these commands:

Run master branch /home/sanghu/TracerX/tracerx/Release+Asserts/bin/klee --max-memory=32000 --max-time=600 -solver-backend=z3 --search=dfs -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -spec-dependency=/home/sanghu/Desktop/Speculation-fix -spec-strategy=custom -spec-type=coverage ${BENCHMARK}.bc

Run spec_custom_dyn branch /home/sanghu/TracerX/tracerx/Release+Asserts/bin/klee --max-memory=32000 --max-time=600 -solver-backend=z3 --search=dfs -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -speculation ${BENCHMARK}.bc

Thanks, sanghu

[xuanlinhha]

I ran master-0df7858a09741d0e19809dcc1a19fffd1179e445 without spec avoid file but it not finished on my machine

[xuanlinhha]

@sanghu: on spec_custom_dyn how do you specify the folder containing spec avoid files ?

[sanghu1790]

@xuanlinhha To run master branch in speculation mode I have used this command:

/home/sanghu/TracerX/tracerx/Release+Asserts/bin/klee --max-memory=32000 --max-time=600 -solver-backend=z3 --search=dfs -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -spec-dependency=/home/sanghu/Desktop/Speculation-fix -spec-strategy=custom -spec-type=coverage ${BENCHMARK}.bc

Here, -spec-dependency=/home/sanghu/Desktop/Speculation-fix is the path to put Spec_Avoid files. SpecAvoid files should be inside Speculation-fix.

Please note that for 'spec_custom_dyn' we dont provide '-spec-dependency' command, in that case the current directory will be the place where Spec_Avoid files should be kept.

[xuanlinhha]

Hi @sanghu1790 I tried to reproduce your result but for this branch spec_custom_dyn-ab4f9fb8 with speculation files, the result I received is like this:

KLEE: KLEE: WATCHDOG: watching 10164

KLEE: output directory is "/home/xuanlinhha/TracerX/run-test/output/Mpals6-B2-cil"
Using Z3 solver backend
tcmalloc: large alloc 1452982272 bytes == 0x1040d8000 @ 
tcmalloc: large alloc 1452982272 bytes == 0x109afe000 @ 
tcmalloc: large alloc 1452982272 bytes == 0x108fcc000 @ 
KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via INT

KLEE: ctrl-c detected, requesting interpreter to halt.
tcmalloc: large alloc 2147491840 bytes == 0x262388000 @ 
KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via gdb

Could not attach to process.  If your uid matches the uid of the target
process, check the setting of /proc/sys/kernel/yama/ptrace_scope, or try
again as the root user.  For more details, see /etc/sysctl.d/10-ptrace.conf
ptrace: Operation not permitted.
No symbol table is loaded.  Use the "file" command.
The program is not being run.
KLEE: WARNING: KLEE: WATCHDOG: kill(9)ing child (I tried to be nice)

[sanghu1790]

@xuanlinhha Can you please cross verify the command options: Run spec_custom_dyn branch "/home/sanghu/TracerX/tracerx/Release+Asserts/bin/klee --max-memory=32000 --max-time=600 -solver-backend=z3 --search=dfs -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -speculation ${BENCHMARK}.bc" Keep your and mine parameter same.

Secondly also cross verify the Spec_Avoid files placed at the current directory where your "c" program and make script are running. I believe the problem is just run issue.

[xuanlinhha]

/home/xuanlinhha/TracerX/tracerx/Release+Asserts/bin/klee --max-memory=32000 --max-time=600 -solver-backend=z3 --search=dfs -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -speculation -output-dir=/home/xuanlinhha/TracerX/run-test/output/Mpals6-B2-cil /home/xuanlinhha/TracerX/run-test/output/Mpals6-B2-cil.bc

[sanghu1790]

Yes. This is correct command option. Can you run and check? The program should finished in approx 35 sec.

[xuanlinhha]

no, it is timeouts on my machine, attached is the result: Mpals6-B2-cil_spec_custom_dyn-ab4f9fb8-with-spec.zip

[sanghu1790]

Can you check if Spec_Avoid files are stored here "/home/xuanlinhha/TracerX/run-test/output/" on your machine. This is my results, please cross verify: Mpals6-B2-cil-5--spec_custom_dyn-ab4f9fb8cc0869e99a507b2512c97a505266b255(two-commits-back).zip Still I suspect you are not providing the specavoid files properly.

[sanghu1790]

This is yours @xuanlinhha Total Independence Yes: 16815 Total Independence No: 0 Total Dynamic Yes: 0 Total Dynamic No: 0 Total Independence No, Dynamic Yes & Success: 0 Total Independence No, Dynamic Yes & Fail: 0 Total speculation failures because of New BB: 0 Total speculation failures because of New BB with no interpolation: 0 Total speculation failures because of Revisted: 0 Total speculation failures because of Revisted with no interpolation: 0 Total speculation failures because of Bug Hit: 0 Total speculation fail time: 0 Frequency of failures because New BB with no interpolation: Frequency of failures because Revisted with no interpolation:

This is mine results: Total Independence Yes: 0 Total Independence No: 2736 Total Dynamic Yes: 1417 Total Dynamic No: 1319 Total Independence No, Dynamic Yes & Success: 1171 Total Independence No, Dynamic Yes & Fail: 246 Total speculation failures because of New BB: 239 Total speculation failures because of New BB with no interpolation: 239 Total speculation failures because of Revisted: 7 Total speculation failures because of Revisted with no interpolation: 5 Total speculation failures because of Bug Hit: 0 Total speculation fail time: 0.682169 Frequency of failures because New BB with no interpolation: 54249128: 3 54251592: 10 54251816: 63 54253496: 10 54255960: 9 54256184: 7 54257864: 9 54260328: 8 54260552: 6 54262232: 9 54457760: 12 55198616: 7 55198840: 5 55200520: 11 55202984: 6 55203208: 7 55204888: 6 55207352: 5 55207576: 8 55209256: 5 55211720: 4 55211944: 9 55213624: 4 55232504: 3 55232728: 10 55368840: 1 55381856: 2 Frequency of failures because Revisited with no interpolation: 54405400: 3 55383584: 2

It shows that your run doesn't read spec avoid files.

[xuanlinhha]

// load avoid BB
  bbOrderToSpecAvoid = readBBOrderToSpecAvoid("/home/xuanlinhha/TracerX/run-test/Speculation-fix/Mpals6-B2-SpecAvoid");
  llvm::errs() << "bbOrderToSpecAvoid size = " << bbOrderToSpecAvoid.size() << "\n";

I fixed the path into source code, and it prints: bbOrderToSpecAvoid size = 1 is that correct?

[xuanlinhha]

And I am working on this commit: ab4f9fb8cc0869e9 Do you see it is strange here @sanghu1790 ?

name=SpecAvoid_149.txt
name=SpecAvoid_155.txt
...
name=SpecAvoid_20.txt
name=SpecAvoid_167.txt

bbOrderToSpecAvoid size = 1

it can see all the files in the folder but just only have 1 BB

[sanghu1790]

@xuanlinhha First of all tell me this new run was faster? Did it finished in 35 sec.

[xuanlinhha]

no @sanghu1790, it does not run faster at all, it was a timeout

[sanghu1790]

I just ran the same program ans it finished in 36 sec. I ran on this commit:

commit ab4f9fb8cc0869e99a507b2512c97a505266b255 Author: xuanlinhha xuanlinhha@gmail.com Date: Wed Sep 25 13:41:00 2019 +0800

Temporary fix for getting depending variables' name

---

Using this command: /home/sanghu/TracerX/tracerx/Release+Asserts/bin/klee --max-memory=32000 --max-time=600 -solver-backend=z3 --search=dfs -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -speculation ${BENCHMARK}.bc

Result is here: Linh-email.zip

Make sure that all spec avoid files are in same directory where .bc file exist.

[xuanlinhha]

Hi @sanghu1790, With speculation avoid files, we have 3 versions:

1. master-0df7858
2. spec_custom_dyn-cfeb033c
3. spec_custom_dyn-ab4f9fb8

1 vs 2: Cannot compare because in 2 we don't check dependency 1 vs 3: The numbers in spec.txt are different because in 3 we count independenceYes/independenceNo and dynamicYes/dynamicNo in speculationFork. If we delete the increasing in speculationFork, the numbers will be the same. You can check again this

[sanghu1790]

Hi @xuanlinhha Point A: 1 vs 2: Cannot compare because in 2 we don't check dependency Answer: I agree.

Point B: 1 vs 3: The numbers in spec.txt are different because in 3 we count independenceYes/independenceNo and dynamicYes/dynamicNo in speculationFork. If we delete the increasing in speculationFork, the numbers will be the same. You can check again this Answer: I am fine with this mismatch in the counting, and we can rely on the new counting on master branch, since now we are using MAP (I remember). Thanks for above justifications.

Now @xuanlinhha , can you also try above without Spec_Avoid files? We need to check, why 1 and 3 took more than 600 sec and 2 finished in 36 sec (on machine). Is it the only difference of disabling "Independence Checks" in "speculationFork" or something else? If it is the case then why in master branch we dont follow disabling "Independence Checks" in "speculationFork"?

[xuanlinhha]

@sanghu1790 When running without spec avoid files, 1-3 is corresponded to -spec-strategy=custom -spec-type=coverage and 2- is -spec-strategy=custom -spec-type=safety in current master branch. But when I run with -spec-strategy=custom -spec-type=coverage, I see there are bug, so I need to check the cause why

[xuanlinhha]

slow-running.zip @sanghu1790 the problem of slow running now become this: -spec-strategy=custom -spec-type=coverage is slower than -spec-strategy=custom -spec-type=safety The difference between 2 versions is that described in this matrix:

When running without speculation avoid file, the independency check always returns True

[sanghu1790]

@xuanlinhha Thanks linh. You mean all time Independence check will be YES. So, then body of this condition will satisfy.

if (TxSpeculationHelper::isIndependent(vars, bbOrderToSpecAvoid)) {
            // open speculation & assume success
            independenceYes++;
            //          StatsTracker::increaseEle(curBB, 0, true);
            //          StatsTracker::increaseEle(curBB, 2, false);
            return StatePair(&current, 0);
          }

But, I dont see any other stuff above which will take heavy time. What went wrong after this?

[xuanlinhha]

Yes, this is -spec-strategy=custom -spec-type=coverage

Total Independence Yes: 47673
Total Independence No: 0
Total Dynamic Yes: 0
Total Dynamic No: 0

Yes, this is -spec-strategy=custom -spec-type=safety

Total Independence Yes: 0
Total Independence No: 0
Total Dynamic Yes: 193
Total Dynamic No: 1
Total Independence No, Dynamic Yes & Success: 131
Total Independence No, Dynamic Yes & Fail: 62

Why it runs slow, this is I also don't know

[sanghu1790]

@xuanlinhha As I can see if we have independece check YES then we just assume the spec success happened, and not marking.

Can we try running with marking for this special case and let see what happens? Add this txTree->markPathCondition(current, unsatCore); and check?

Copy this below code and let us see what happens here.

if (TxSpeculationHelper::isIndependent(vars, bbOrderToSpecAvoid)) {
            // open speculation & assume success
            independenceYes++;
            //          StatsTracker::increaseEle(curBB, 0, true);
            //          StatsTracker::increaseEle(curBB, 2, false);
          txTree->markPathCondition(current, unsatCore);
            return StatePair(&current, 0);
          }

[xuanlinhha]

it also gives a timeout @sanghu1790 If we do in that way, equivalent to all speculations are fail.

[sanghu1790]

Hi @xuanlinhha As we discussed I ran TIMID and CUSTOM on master branch.

1. TIMID (WITH SPEC AVOID FILES)= Approx. 200 sec and timeout
2. TIMID (WITHOUT SPEC AVOID FILES)= Approx. 200 sec and timeout
3. CUSTOM (WITH SPEC AVOID FILES)= 27 sec and finished
4. CUSTOM (WITHOUT SPEC AVOID FILES)= Approx. 200 sec and timeout TIMID-CUSTOM-MASTER-RESULT.zip You can check their spec.txt files in this zip file.

[sanghu1790]

@xuanlinhha I ran on fix_skip_void_type after fixed issue, still the same results.

1. TIMID (WITH SPEC AVOID FILES)= Approx. 200 sec and timeout
2. TIMID (WITHOUT SPEC AVOID FILES)= Approx. 200 sec and timeout

I think if we are able to get to know that why without specavoid files TIMID isn't working, then automatically the CUSTOM issue will also get fixed.

But interesting fact is below:

1. Below is spec stats for TIMID (WITH SPEC AVOID FILES)

   Total Independence Yes: 0
   Total Independence No: 405
   StatsTracker Total: 0
   StatsTracker Fail: 405
   StatsTracker Success: 0
   Total speculation failures because of New BB: 0
   Total speculation failures because of New BB with no interpolation: 0
   Total speculation failures because of Revisted: 0
   Total speculation failures because of Revisted with no interpolation: 0
   Total speculation failures because of Bug Hit: 0
   Total speculation fail time: 0
   Frequency of failures because New BB with no interpolation:
   Frequency of failures because Revisted with no interpolation:

2. Below is spec stats for TIMID (WITHOUT SPEC AVOID FILES)

   Total Independence Yes: 39098
   Total Independence No: 0
   StatsTracker Total: 39098
   StatsTracker Fail: 0
   StatsTracker Success: 39098
   Total speculation failures because of New BB: 0
   Total speculation failures because of New BB with no interpolation: 0
   Total speculation failures because of Revisted: 0
   Total speculation failures because of Revisted with no interpolation: 0
   Total speculation failures because of Bug Hit: 0
   Total speculation fail time: 0
   Frequency of failures because New BB with no interpolation:
   Frequency of failures because Revisted with no interpolation:

   Both 1 and 2 above tool huge time of 200 sec. It should be rapidly work. Now, I think the problem is coming from somewhere else. I suspect the check with "NEW BB". Cam we turnoff this check during the coverage mode? I want to see the difference. Make a new commit with commented code for the check of NEW BB. Later we will delete that commit if it doesn't work.

[xuanlinhha]

We don't need to commit with just a comment @sanghu1790 , I commented and tested on my local machine, but it is still slow

[sanghu1790]

@xuanlinhha Thanks for checking that too linh. Then we need to see other possibilities.

I am quite surprise with this Total Independence Yes: 39098 above. If we do nothing when the Independence check is Yes (just assuming spec yes) then why it is taking huge time. What I feel is that it tries to visit every node (in normal tree and spec tree both) and the general subsumption also ineffective here. Now, I think we need to focus on exploration of paths. Why they are so indifferent?

1. Below is spec stats for TIMID (WITH SPEC AVOID FILES)

   KLEE: done: total instructions = 6064
   KLEE: done: completed paths = 55, among which
   KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
   KLEE: done:     average branching depth of completed paths = 20.2143
   KLEE: done:     average branching depth of subsumed paths = 21.2927
   KLEE: done:     average instructions of completed paths = 568.929
   KLEE: done:     average instructions of subsumed paths = 509.878
   KLEE: done:     subsumed paths = 41
   KLEE: done:     error paths = 0
   KLEE: done:     program exit paths = 14

2. Below is info stats for TIMID (WITHOUT SPEC AVOID FILES)

   KLEE: done: total instructions = 564053
   KLEE: done: completed paths = 13098, among which
   KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
   KLEE: done:     average branching depth of completed paths = 19.4054
   KLEE: done:     average branching depth of subsumed paths = 18.8045
   KLEE: done:     average instructions of completed paths = 552.054
   KLEE: done:     average instructions of subsumed paths = 403.397
   KLEE: done:     subsumed paths = 13061
   KLEE: done:     error paths = 0
   KLEE: done:     program exit paths = 37

Can we look at here linh? Why the number of paths so different. In 1 we do explore the spec tree, and in 2 we restrict the spec tree to be explore, then why this huge path numbers are different.

Thanks, Sanghu

[xuanlinhha]

In TIMID, if we have more Total Independence Yes, we have better interpolants and we subsume more often. so I think having more instructions and paths is reasonable.

[sanghu1790]

That's what my point is. If we have better interpolants generated so we may have more subsumption and ultimately the execution time will be automatically reduced. But, you see above this is not the case. 2 is more time consuming that 1, which I think should be reversed.

[xuanlinhha]

But with TIMID, the running times, we have not seen the difference mah, both are timeouts

[sanghu1790]

Oh Yes sorry I am wrong. Both have timeout. We need to check some more aspects.

[sanghu1790]

Hi @xuanlinhha , I think we did several checks and couldn't found the correct reason why the slowness happening.

Just a last try, check without independence check in coverage mode but use dynamic check in custom and new basic block check in aggressive and custom both. I am saying to utilise the code recently we decided to do for safety mode, in addition to that just add "new basic block" check. Then we will run without specavoid files on coverage mode to check the results.

Then at last we will take final decision on spec coverage.

[xuanlinhha]

You see in the matrix, the custom row, the coverage has 3 more things compared with safety: 1 - Independence checking in branchFork 2 - Independence checking in speculationFork 3 - New BB checking I have tested with the followings:

• Remove 1 of the 3 differences (1 or 2 or 3) in coverage => still slow running
• Remove 2 of the 3 differences (1&2 or 1&3 or 2&3) in coverage => still slow running
• Remove 3 differences (1&2&3) in coverage => as fast as safety

[sanghu1790]

This is something new you mentioned here, about "Remove 3 checkings in coverage => as fast as safety" So you mean to say, If we enable COVERAGE mode on CUSTOM without specavoid files, do independece check and custom check on branchFork and SpeculationFork functions along with DISABLED "New BB check" then it is faster, right?

Because when we checked TIMID we had slowness result as you mentioned in below comment. https://github.com/tracer-x/klee/issues/364#issuecomment-619660712

If above is correct then I think we no need of "New BB check" permanent but yeah we need to look at total number of blocks shouldn't be less as compared to KLEE and DEL-TX.

We can experiment on few programs to just check.

[xuanlinhha]

Our original problem is that when running without spec avoid files, the running time of this setting: -spec-strategy=custom -spec-type=coverage is slower than this: -spec-strategy=custom -spec-type=safety

If we look at the matrix, the differences between 2 settings are 3 points, as I said above. And I step by step trace what is the reason causing the difference by changing the source code for this -spec-strategy=custom -spec-type=coverage to make it as similar as -spec-strategy=custom -spec-type=safety

[sanghu1790]

HI @xuanlinhha As per our phone call discussion, let us try to get the reason Why "independence yes" checks take huge time without spec avoid files? I think this is very important to know.

Based on above we will finally take the decision.

[xuanlinhha]

@sanghu1790 the problem now is becoming like this: Untitled spreadsheet - Sheet1 (3).pdf

I remove New BB checking, run with -spec-strategy=custom -spec-type=coverage, and change value returned from Independence checking. Because we run without spec avoid files, so if Independence checking always returns FALSE, it is equivalent with -spec-strategy=custom -spec-type=safety

The strange statistics is like this:

|=> First Case | completed paths = 374 | subsumed paths = 365 | BCov(%) = 77.85
|=> Second Case | completed paths = 4037 | subsumed paths = 4006 | BCov(%) = 30.87

info-First Case.txt info-Second Case.txt

[sanghu1790]

Hi @xuanlinhha , Yeah I see your point. This is strange stats. As per your defined cases, First-case has all time "dynamic checks" and it will explore speculation sub-stree, so it's paths and coverage must be more that normal. In second case, we assume all time "Independence checks" are YES, so we assume all time spec successes. Here, in second case we dont create the speculation sub-stree and we see the paths are more and coverage is less than the first case.

What I am thinking now is to put "dynamic check" inside "Independence check YES" to check the situation what will happen. What I can estimate here is that, if this is true then we need to make below:

For coverage mode

1. With spec avoid files: Keep "Independence check", "dynamic check" , and "New BB check".
2. Without spec avoid files: Keep "dynamic check", and "New BB check" ( remove "Independence check" just like safety)

Whats your opinion?

[rasoolmaghareh]

May I also confirm here that the current implementation with spec-avoid files is working fine with the following setting?

1- With spec avoid files: Keep "Independence check", "dynamic check", and "New BB check".

If so, I think I agree with @sanghu1790 for setting 2 when we don't have spec-avoid files.

[sanghu1790]

@rasoolmaghareh

1. Up to now setting 1 was working well as per my experience. But, when we will do actual experiments on all programs then, we can observe the real scenario.

2. One more point is that, if we will supply spec avoid files then they should be complete set (after pre-processing) OR dont supply any files, for the correct results. But, supply of partial spec avoid files (either supply one file or (n-1) where n is the total spec avoid files) is not recommended. The performance may hamper.

[rasoolmaghareh]

ok, for conclusion let's consider these two cases and confirm they are correct for coverage mode:

1- With complete set of spec avoid files: Keep "Independence check", "dynamic check" , and "New BB check".

2- Without any spec avoid files: Keep "dynamic check", and "New BB check" ( remove "Independence check" just like safety)

[sanghu1790]

Yes I agree with this.

@xuanlinhha Whats your opinion? Do you want to do more finding on "independence check YES" case?

@rasoolmaghareh honestly I and linh didn't got the real answer why "independence check YES" is taking huge time. My proposal was based on the several attempts we made to see the best results, and we found this case. Do you have any idea about the above case where "independence check YES" is so expensive?

[xuanlinhha]

@rasoolmaghareh:

2- Without any spec avoid files: Keep "dynamic check", and "New BB check" ( remove "Independence check" just like safety)

=> In safety we don't have "New BB check"

@sanghu1790: I think if users run with coverage but not provide spec avoid files, we can print an error message and ask them to run with safety

[sanghu1790]

Hi @xuanlinhha Rasool and I both are aware about point number 2 for coverage is with "New BB check" and safety is without "New BB check". Don't worry we all are on same page. Am I right @rasoolmaghareh .

Regarding the printing message, I agree @xuanlinhha but we need to facilitate the users to use without specavoid files too. Hence we require point 2 for that. But we can give warning message.

[rasoolmaghareh]

yes.

[xuanlinhha]

But if like this:

2- Without any spec avoid files: Keep "dynamic check", and "New BB check" ( remove "Independence check" just like safety)

Cannot resolve the program of @sanghu1790

[sanghu1790]

@xuanlinhha

I am referring your comment https://github.com/tracer-x/klee/issues/364#issuecomment-620526258 and my comment https://github.com/tracer-x/klee/issues/364#issuecomment-620937143, I estimate that

2- Without any spec avoid files: Keep "dynamic check", and "New BB check" ( remove "Independence check" just like safety)

will run faster based on your sample run.

But yeah before merging to master branch we should run couple of programs.

But, overall my view would be to run coverage with mandatory spec avoid files. We will take final decision based on experiments.

[xuanlinhha]

I have checked on my side, and no non-speculation states are deleted when backjump But one thing I noticed is that all the interpolants inside the speculation subtree only contain the counter variable i2=1 but the from non-speculation nodes contain many information being marked. Maybe the interpolant inside spec-tree make more subsumption checks success and we run faster

[rasoolmaghareh]

Can you please share the generated interpolants in both speculation tree and outside speculation tree here?

[xuanlinhha]

The second file is big, so I zipped it: intepolant-in-spec-output.txt

interpolant-out-spec-output.txt.zip

You see the marked variables are global ones. All interpolations outside spec-tree have symbolically-addressed store = []