Error expression constraint solving using Z3

[domainexpert]

Replacement of #22 caused by problems due to the unforking of fp-analysis/klee from klee/klee. This PR is not yet ready to be merged.

[domainexpert]

@Himeshi This PR is ready for merging. Works with normal as well as the array examples basic/array_testN.c of fp-examples repository. Although the constraints are submitted to Z3, since nonlinear solving cannot be handled, exception is thrown. For example, assuming current directory is basic of fp-examples clone, executing:

$ EXTRA_OPTIONS="-debug-precision" make array_test1.klee

results in:

...
----------------------------------------------
Executing:   call void @klee_bound_error(i64 %2, double 1.300000e+00), !dbg !140
Solving:
(declare-fun arr__index__2 () Real)
(declare-fun arr__index__1 () Real)
(declare-fun arr_error__index__2 () Real)
(declare-fun arr_error__index__1 () Real)
(declare-fun __error__38813184 () Real)
(assert (= __error__38813184
   (/ (+ (* arr_error__index__1 arr__index__1)
         (* arr_error__index__2 arr__index__2))
      (+ arr__index__1 arr__index__2))))
(assert (<= (to_real (div (- 0 13000) 10000)) __error__38813184))
(assert (<= __error__38813184 (to_real (div 13000 10000))))
(maximize arr_error__index__1)
(maximize arr_error__index__2)
(set-option :opt.timeout 4294967295)
(set-option :opt.priority pareto)
(check-sat)

KLEE: WARNING: Unexpected solver failure. Reason is "(incomplete (theory arithmetic)),"

0  libLLVM-3.4.so.1 0x00002b8abbb90042 llvm::sys::PrintStackTrace(_IO_FILE*) + 34
1  libLLVM-3.4.so.1 0x00002b8abbb8fe34
2  libpthread.so.0  0x00002b8abc657390
3  libc.so.6        0x00002b8abebb3428 gsignal + 56
4  libc.so.6        0x00002b8abebb502a abort + 362
5  klee             0x00000000004efc9f
6  klee             0x00000000004eff17 klee::Z3ErrorSolverImpl::internalRunOptimize(klee::Query const&, std::vector<klee::Array const*, std::allocator<klee::Array const*> > const*, std::vector<bool, std::allocator<bool> >*, std::vector<double, std::allocator<double> >*, std::vector<bool, std::allocator<bool> >*, bool&) + 631
7  klee             0x0000000000492618 klee::SpecialFunctionHandler::handleBoundError(klee::ExecutionState&, klee::KInstruction*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 1016
8  klee             0x000000000048f9b1 klee::SpecialFunctionHandler::handle(klee::ExecutionState&, llvm::Function*, klee::KInstruction*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 193
9  klee             0x0000000000463b07 klee::Executor::callExternalFunction(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&) + 87
10 klee             0x000000000046e30a klee::Executor::executeCall(klee::ExecutionState&, klee::KInstruction*, llvm::Function*, std::vector<klee::Cell, std::allocator<klee::Cell> >&) + 2234
11 klee             0x00000000004729a7 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 16615
12 klee             0x00000000004769fc klee::Executor::run(klee::ExecutionState&) + 1660
13 klee             0x000000000047738f klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1791
14 klee             0x000000000044f871 main + 11793
15 libc.so.6        0x00002b8abeb9e830 __libc_start_main + 240
16 klee             0x0000000000457319 _start + 41
Aborted (core dumped)
Makefile:24: recipe for target 'array_test1.klee' failed
make: *** [array_test1.klee] Error 134
rm array_test1.bc

The nonlinearity issue need to be resolved, but that better be the subject of another PR.

[domainexpert]

The output error expression looks slightly different:

Line 28 of /home/dcsandr/software/fp-examples/basic/array_test1.c (main): 
Output Error: (((arr_error__index__1 * arr[1]) + (arr_error__index__2 * arr[2])) / (arr[1] + arr[2]))
Absolute Bound: 1.300000e+00

[domainexpert]

@Himeshi I have removed the review request. I realized these features still need to be implemented:

1. Outputting of the input bounds result, as computed by Z3 into file.
2. Option to make the computation of error bounds by Z3 optional.

[domainexpert]

@Himeshi I have implemented the features I mentioned, no. 1 is not yet tested as we cannot handle nonlinear constraints, no. 2 has been implemented, and due to this, the feature implemented by this PR has to be activated via -compute-error-bound option. For example, in basic directory of fp-examples local clone:

EXTRA_OPTIONS="-compute-error-bound -debug-precision" make array_test1.klee

would call Z3 to compute the error bound. Again, as mentioned above, exception is triggered as Z3 cannot solve nonlinears. Without -compute-error-bound no solving of error bounds using Z3 will be made, and KLEE behaves normally.

I think this PR is ready to be merged.

[domainexpert]

@Himeshi Please note that this PR includes #35.

[domainexpert]

@Himeshi Sorry I am returning this PR to WIP status as I am realizing more can be done:

1. Implement a linearizing routine to obtain solutions for non-input-error symbolic values (e.g., the symbolic variables themselves). The linearizing routine is important to test the solving in cases that can be solved. In some cases it may be possible to use binary search / pareto optimality to find optimal values for the non-error symbolics first, and use the optimal values to ground the non-error symbolics when computing error bounds via pareto optimal. But such more complex mechanism should be the subject of another Issue/PR.
2. There is a need to test the array handling when dereferencing index 0 of the array, since the address is the same as the address of the whole array, specifically, there is a need to test if the output error expression would be correct for a sequence of a[0] dereferencing, for an array a, since the array's input error gets deregistered and replaced with a_errorindex0. We don't want this to happen twice (or more) resulting in a_errorindex0index0, and so on.

[domainexpert]

Pareto optimality can take huge resources to compute compared to lexicographic optimality of optimization functions, however, lexicographic optimality may require lower bound of the optimization functions, because in our case, these are input errors, and say, we don't want values that are unreasonably low (such as negative) due to maximizing another input error.

[domainexpert]

Latest commit domainexpert/klee@8e727fe has resolved issue no. 2 mentioned above. This is done by having the indexed input error variables for arrays created at the execution of load instruction instead of getelementptr. The problem with getelementptr is that it is also used for store, such that the input array also gets generated at point of storing, which is wrong, since input array should only be read. The test example that this is working comes with fp-analysis/fp-examples#17.

[domainexpert]

@Himeshi I am more inclined to resolve issue no. 1 using binary search algorithm, which I mentioned should be subject of another PR. So, I think this PR is ready to be merged.

[domainexpert]

@Himeshi I think this PR is ready for merging. Now the output error expression is as previously:

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

KLEE: done: total instructions = 18
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
rm array_test5.bc
$ cat array_test5.klee/test000001.precision_error 
Line 29 of /home/dcsandr/software/fp-examples/basic/array_test5.c (main): 
Output Error: (((arr_error[0] * arr[0]) + (arr_error[1] * arr[1])) / (arr[0] + arr[1]))
Absolute Bound: 1.300000e+00

Plus, now we can choose between computing error bounds using real number domain or integer domain (not yet implemented), as now the -compute-error-bound can be given argument real or integer, for example:

$ EXTRA_OPTIONS="-compute-error-bound=real" make array_test1.klee
clang -I/home/dcsandr/software/fp-analysis-klee/Release+Asserts/include -I/home/dcsandr/software/fp-analysis-klee/Release+Asserts/../include -c -emit-llvm -g -o array_test1_123.bc array_test1.c
opt -mem2reg < array_test1_123.bc > array_test1.bc
rm -f array_test1_123.bc
if [ -z "$OUTPUT_DIR" ] ; then \
    OUTPUT_DIR="array_test1.klee" ; \
fi ; \
/home/dcsandr/software/fp-analysis-klee/Release+Asserts/bin/klee -search=dfs -output-dir="$OUTPUT_DIR" $EXTRA_OPTIONS -precision array_test1.bc
KLEE: output directory is "/home/dcsandr/software/fp-examples/basic/array_test1.klee"
KLEE: Using STP solver backend
KLEE: Using Z3 for reasoning about error expressions
KLEE: WARNING: Unexpected solver failure. Reason is "(incomplete (theory arithmetic)),"

[domainexpert]

@Himeshi As mentioned, this PR is ready to be merged. The integer solving mode is now implemented. Although Z3 no longer gives up due to nonlinearity, the solving seems to take a long time. For example:

$ EXTRA_OPTIONS="-compute-error-bound=integer -debug-precision" make array_test5.klee
...
Solving:
(declare-fun arr__index__1 () Int)
(declare-fun arr__index__0 () Int)
(declare-fun arr_error__index__1 () Int)
(declare-fun arr_error__index__0 () Int)
(declare-fun __error__39591056 () Int)
(assert (= __error__39591056
   (div (+ (* arr_error__index__0 arr__index__0)
           (* arr_error__index__1 arr__index__1))
        (+ arr__index__0 arr__index__1))))
(assert (<= (div (- 0 13000) 10000) __error__39591056))
(assert (<= __error__39591056 (div 13000 10000)))
(maximize arr_error__index__0)
(maximize arr_error__index__1)
(set-option :opt.timeout 4294967295)
(set-option :opt.priority pareto)
(check-sat)

I aborted the run after minutes.

We could add bounds, for example, using klee_assume as in the following test.c:

#include <klee/klee.h>
#include <stdio.h>

#define SIZE 5

void test_array(char *x);

char arr[SIZE], answer;

int main() {

  /*
     Here we add __arr8__ prefix to declare that this was an array of
     8 bits. This causes array indirection to be used in the output
     error expression.
  */
  klee_make_symbolic(arr, SIZE * sizeof(char), "__arr8__arr");
  klee_track_error(arr, "__arr8__arr_error");

  klee_assume(arr[1] >= 0);
  klee_assume(arr[1] <= 3);
  klee_assume(arr[2] >= 0);
  klee_assume(arr[2] <= 3);

  test_array(arr);

  klee_bound_error(arr[0], 1.3);
  return 0;
}

void test_array(char *x) {
  // x[0] = (x[1] + x[2]) * (x[3] - x[4]);
  x[0] = x[1] + x[2];
}

The run still does not finish after minutes:

$ EXTRA_OPTIONS="-compute-error-bound=integer -debug-precision" make test.klee
...
Solving:
(declare-fun arr__index__2 () Int)
(declare-fun arr__index__1 () Int)
(declare-fun arr_error__index__2 () Int)
(declare-fun arr_error__index__1 () Int)
(declare-fun __error__29965568 () Int)
(assert (= __error__29965568
   (div (+ (* arr_error__index__1 arr__index__1)
           (* arr_error__index__2 arr__index__2))
        (+ arr__index__1 arr__index__2))))
(assert (<= (div (- 0 13000) 10000) __error__29965568))
(assert (<= __error__29965568 (div 13000 10000)))
(assert (<= 0 arr__index__1))
(assert (<= arr__index__1 3))
(assert (<= 0 arr__index__2))
(assert (<= arr__index__2 3))
(maximize arr_error__index__1)
(maximize arr_error__index__2)
(set-option :opt.timeout 4294967295)
(set-option :opt.priority pareto)
(check-sat)

Removing the pareto optimality option does not seem to change the situation. Setting the inputs to constant, however, makes termination immediate, as in the following example:

#include <stdio.h>

#define SIZE 5

void test_array(char *x);

char arr[SIZE], answer;

int main() {

  /*
     Here we add __arr8__ prefix to declare that this was an array of
     8 bits. This causes array indirection to be used in the output
     error expression.
  */
  klee_make_symbolic(arr, SIZE * sizeof(char), "__arr8__arr");
  klee_track_error(arr, "__arr8__arr_error");

  klee_assume(arr[1] == 0);
  klee_assume(arr[2] == 3);

  test_array(arr);

  klee_bound_error(arr[0], 1.3);
  return 0;
}

void test_array(char *x) {
  // x[0] = (x[1] + x[2]) * (x[3] - x[4]);
  x[0] = x[1] + x[2];
}

The run result with debug information is as follows:

(declare-fun arr_error__index__2 () Int)
(declare-fun __error__17858016 () Int)
(declare-fun arr__index__1 () Int)
(declare-fun arr__index__2 () Int)
(declare-fun arr_error__index__1 () Int)
(assert (= __error__17858016 (div (* 3 arr_error__index__2) 3)))
(assert (<= (div (- 0 13000) 10000) __error__17858016))
(assert (<= __error__17858016 (div 13000 10000)))
(assert (= 0 arr__index__1))
(assert (= 3 arr__index__2))
(maximize arr_error__index__1)
(maximize arr_error__index__2)
(set-option :opt.timeout 4294967295)
(set-option :opt.priority pareto)
(check-sat)

(infinity_coefficient, upper_bound, epsilon_coefficient) = (1,0,0)
(infinity_coefficient, upper_bound, epsilon_coefficient) = (0,1,0)
Error Bound for (Read w8 0 arr_error__index__1) is infinity
Error Bound for (Read w8 0 arr_error__index__2) is 1.000000e+00

[domainexpert]

@Himeshi The last modification adds -pareto option to enable pareto optimality-based computation of input errors. Otherwise, uniform error is assumed for all inputs by default. This PR is ready to be merged as ever.