Loop breaking

[domainexpert]

@Himeshi Towards resolving #12. This is not ready to be merged.

[domainexpert]

As at @0aaadab need to add stacking of StoreFrame, with each element StoreFrame of the stack corresponds to a cyclic path with identifiable constant trip count.

[domainexpert]

ATM call to getLoopFor in TripCounter::getTripCount does not work.

[domainexpert]

Replaced getLoopFor with a map.

[domainexpert]

Next is to implement proper expression loading such that after the loop is exited, when a datum is loaded from memory and and the load address exists in the SymbolicError::loopResultErrorState, two things happen:

1. The loaded value is a fresh symbolic array.
2. The loaded error comes from SymbolicError::loopResultErrorState.

[domainexpert]

Next is to implement the replacement by unconstrained symbolic values all stored values that were modified within the loop, when the loop is terminated prematurely.

[domainexpert]

At the moment, in the process of creating fresh symbolic values upon exiting of loops, of all values stored within the loop. The last commit domainexpert/klee@df2e740 is not yet working.

[domainexpert]

The program used to test this is currently basic/loop.c in loop-breaking branch of domainexpert/fp-examples repo.

[domainexpert]

ATM the error result for loop.c in fp-examples loop-breaking branch seems incorrect.

[domainexpert]

The previously-mentioned problem has been fixed, also the error expression has been corrected.

[domainexpert]

Next is to make basic/adpcm_encoder_constant_iter.c working in domainexpert/fp-examples loop-breaking branch. Also may need to clear value errors that when loop is exited to improve performance.

[domainexpert]

Made basic/adpcm_encoder_constant_iter.c working. Clearing value errors is not yet implemented, as it is uncertain if it would improve performance.

[domainexpert]

@Himeshi I think this is ready for review.

[domainexpert]

@Himeshi This PR addresses both #12 as well as #9 (via commit 8aa5834).

[domainexpert]

@Himeshi Still need to ensure that the following cases are correctly handled:

1. Branching loop: In two iterations, the store instruction is only executed once.
2. Different instructions can store to the same memory locations within the same iteration. In such case, the error amount of the value stored in the address should pertain to the second store.

[domainexpert]

@Himeshi Changed back to WIP.

[domainexpert]

Case 1 has to be refined into sub-cases:

1.a. There is only one store to the error location. In this case, the error amount upon exiting should be the same as the first store.

1.b. There is no store to the error location. In this case, the error amount upon exiting should be the same as before entering the loop.

In the following example, due to the loop breaking algorithm terminates after 2 iterations, we c can be stored into 2, 1 (in two paths), and 0 times.

int main(int argc, char **argv) {
  int c = 0, e = 0;
  char a[INPUT_SIZE];

  klee_make_symbolic(&c, sizeof(c), "c");
  klee_track_error(&c, "c_error");

  for (int i = 0; i < INPUT_SIZE; ++i) {
    char d;

    klee_make_symbolic(&d, sizeof(char), "d");

    if (d) {
      c++;
    } else {
      e++;
    }
  }

  // Bound the error
  klee_bound_error(c, 1.3);

  return 0;
}

In case 2, it should be the case that the error amount should be that of the last store in the second iteration. Say, there are two stores to %c in each iteration: First iteration executes store1 and store2, and the second iterator executes only store1. Then the error is computed using store1.

EDIT: Added more details

[domainexpert]

@Himeshi Confirmed that the case 1 example worked perfectly

$ make loop_branching2.loop
clang -c -emit-llvm -g -o loop_branching2_123.bc loop_branching2.c
opt -mem2reg < loop_branching2_123.bc > loop_branching2.bc
rm -f loop_branching2_123.bc
EXTRA_OPTIONS="-loop-breaking" OUTPUT_DIR="loop_branching2.loop" make loop_branching2.klee
make[1]: Entering directory '/home/dcsandr/software/fp-examples/basic'
if [ -z "$OUTPUT_DIR" ] ; then \
    OUTPUT_DIR="loop_branching2.klee" ; \
fi ; \
/home/dcsandr/software/klee/Release+Asserts/bin/klee -search=dfs -output-dir="$OUTPUT_DIR" $EXTRA_OPTIONS -precision loop_branching2.bc
KLEE: output directory is "/home/dcsandr/software/fp-examples/basic/loop_branching2.loop"
KLEE: Using STP solver backend

KLEE: done: total instructions = 96
KLEE: done: completed paths = 4
KLEE: done: generated tests = 4
make[1]: Leaving directory '/home/dcsandr/software/fp-examples/basic'
rm loop_branching2.bc
$ ls -l loop_branching2.loop/*.fp_error
-rw-rw-r-- 1 dcsandr dcsandr 200 Jun 26 19:07 loop_branching2.loop/test000001.fp_error
-rw-rw-r-- 1 dcsandr dcsandr 416 Jun 26 19:07 loop_branching2.loop/test000002.fp_error
-rw-rw-r-- 1 dcsandr dcsandr 416 Jun 26 19:07 loop_branching2.loop/test000003.fp_error
-rw-rw-r-- 1 dcsandr dcsandr 744 Jun 26 19:07 loop_branching2.loop/test000004.fp_error

There are four error expressions corresponding to the four paths: The first one where there is no store to c executed, the error amount is just the same as before entering the loop, that is c_error.

$ cat loop_branching2.loop/test000001.fp_error
Line 39 of /home/dcsandr/software/fp-examples/basic/loop_branching2.c (main): __error__40610544 == ((Read w8 0 c_error)) && (__error__40610544 <= 1.300000e+00) && (__error__40610544 >= -1.300000e+00)

The second and third error expressions are for when there is only a single store to c in the two iterations:

$ cat loop_branching2.loop/test000002.fp_error
Line 39 of /home/dcsandr/software/fp-examples/basic/loop_branching2.c (main): __error__40637456 == ((Extract w8 0 (ZExt w64 (Extract w8 0 (UDiv w32 (Mul w32 (ZExt w32 (Read w8 0 c_error))
                                                          N0:(ReadLSB w32 0 c))
                                                 (Add w32 1 N0)))))) && (__error__40637456 <= 1.300000e+00) && (__error__40637456 >= -1.300000e+00)

The fourth error expression is when two stores into c were encountered, note the multiplication by loop trip count (10) -1 in the following:

$ cat loop_branching2.loop/test000004.fp_error
Line 39 of /home/dcsandr/software/fp-examples/basic/loop_branching2.c (main): __error__40639392 == ((Extract w8 0 (Add w64 N0:(ZExt w64 N1:(Extract w8 0 (UDiv w32 (Mul w32 (ZExt w32 (Read w8 0 c_error))
                                                                         N2:(ReadLSB w32 0 c))
                                                                N3:(Add w32 1 N2))))
                        (Mul w64 9
                                 (Sub w64 (ZExt w64 (Extract w8 0 (UDiv w32 (Mul w32 (ZExt w32 N1) N3)
                                                                            (Add w32 2 N2))))
                                          N0))))) && (__error__40639392 <= 1.300000e+00) && (__error__40639392 >= -1.300000e+00)

[domainexpert]

Case 2 has to be simplified. The store that we are talking about is always the last store of the iteration of the same address, hence there is no ambiguity on in between which stores the errors should be measured.

[domainexpert]

The last commit fp-analysis/klee@f55b14aeb486dae96e2c3a6f9b7d4953236bc794 refines the loop breaking error expression:

1. In case both the first and the second stored errors were non-constant symbolic expressions, then the error amount is: the first stored error + (trip count - 1) * (second stored error - first stored error).

2. In case the first stored error was a constant and the second stored error was a non-constant symbolic expression, then the resulting error was the symbolic expression.

3. In case the second stored error was a constant, then the resulting error is the constant.

[domainexpert]

@Himeshi All error semantics issues I could think of have been resolved. Again removed WIP, and please review.