Adding no-compression command line argument

[rasoolmaghareh]

@domainexpert This commit contains the changes from #276 too.

EDIT: countNode -> #276

[domainexpert]

@rasoolmaghareh I have not finished reviewing, but I have rebased this PR to the merged #276. For the time being, would you please do the following on your clone:

git fetch origin
git checkout no-merge
git reset --hard origin/no-merge.

The first command fetch the latest copy from the origin repository, which is tracer-x/klee, but without merging them with the latest branch. The second command ensures that we're at the no-merge branch. The third command ensures that your local no-merge branch is synchronized with the no-merge branch that I rebased.

EDIT: Explanation on the git commands

[rasoolmaghareh]

@domainexpert thanks a lot. I applied the changes.

[domainexpert]

@rasoolmaghareh I have added a commit that corrects the indentation.

[domainexpert]

@rasoolmaghareh Please don't forget to first pull from this branch (since I have added a commit).

[domainexpert]

@rasoolmaghareh Before you work further, and although we both have spent time on it, I have a second thought about merging this PR based on your email since for the following example that you mentioned, the number of nodes increase without gain in subsumption. (I hope you don't mind I paste it here, but please feel free to object.)

#include <klee/klee.h>

int main()
{
  int N;

  klee_make_symbolic(&N, sizeof(N), "N");

  klee_assume(0 <= N);
  klee_assume(N <= 10);

  int x = 0, i = 0;
  while (i < N) {
    if (i % 2 == 0) {
      x += 2;
    }
    if (i % 3 == 0) {
      x += 3;
    }
    i++;
  }
  return 0;
}

According to you we have the following trees with compression (21 nodes, 0 subsumptions) and without compression (105 nodes, 0 subsumptions). Unvisited nodes in the symbolic tree are infeasible nodes. Based on your observation, the difference in the number of nodes comes from mainly "deterministic branches" and "loop outgoing edges where loop count is a fixed number".

Since the disabling of compression does not work well for the above example, is there an example where it does work well (you mentioned nsichneu.c before)? A lot of changing of the original KLEE code makes me a bit reluctant to merge. I think it is a good idea to stick close to the original KLEE code, so that we can benefit from updates to KLEE.

Please let me know your thoughts.

[rasoolmaghareh]

@domainexpert, Joxan and I had two discussions on the point that how much forcing no-compression is effective. My checks show that in cases such as adpcm the number of subsumes still remains 0 when forcing no-compression. Also, we are not able to analyze nsichneu without compression. Considering the point that interpolants at deterministic choice points might only subsume narrow cases and considering the overhead, we also agreed that no-compression might not be useful. I suggest we keep the code in a separate branch in case in future we want to revisit it. May I know your thoughts?

[rasoolmaghareh]

Just for a reference in future, at the current status, the remaining tasks are as follow:

1- Fixing the representation of infeasible-nodes in TxTreeGraph. Currently, they are marked as unvisited nodes. 2- There is a lot of code that is being repeated between the bodies of the then, else if, and else clauses in Executor::fork function.

[domainexpert]

@rasoolmaghareh Do you have numbers for nsichneu.c comparing compression and no compression cases? (If not, I can try to get them.)

[rasoolmaghareh]

The analysis for nsichneu without compression hits the 1 hour time limit. However, for adpcm which was similar to nsichneu (having 0 subsumption), the number of subsumptions still remains 0. These are the details:

• Visited Basic Blocks: 67396 (the same with & without compression)
• Total Instructions: 981603 (the same with & without compression)
• Subsumed paths: 0
• Program exit paths: 156

Compression:

• Number of subsumption checks: 331
• Avg. table entry per subsumption checkpoint: 34.55
• Solver access time: 53.42
• Concrete store build time(ms): 20.97

No-compression:

• Number of subsumption checks: 44997
• Avg. table entry per subsumption checkpoint: 1745.57
• Solver access time: 29.52
• Concrete store build time(ms): 1959.57
• Infeasible paths: 44686

[domainexpert]

@rasoolmaghareh Ok, thank you for the numbers, the notes, and the hard work for the PR, but I think let's not merge this PR based on the numbers. Closed PR's commits are archived anyway, such as #147, #127 etc. If you agree, I'll close it.

[rasoolmaghareh]

Sure.

[domainexpert]

@rasoolmaghareh Thank you for your understanding. We should probably do the same to #197, which does not show performance improvement, but I would like to try to run another test, if I can find time.