ApproxSymate / klee

KLEE Symbolic Virtual Machine for Numerical Precision Analysis
Other
0 stars 0 forks source link

WIP: Implemented error propagation in calls and returns #27

Closed domainexpert closed 7 years ago

domainexpert commented 7 years ago

@Himeshi Resolves issue #26. The problem was that the error expressions were not implemented properly in function calls and returns. It still worked without mem2reg since the errors were store in memory using absolute addresses. With mem2reg, the storing into memory at function calls and returns were skipped such that the error expressions were not propagated.

Now runs with basic/add_test.c and basic/add_test2.c should result in non-zero error expression, even when the bitcode has been processed with mem2reg.

domainexpert commented 7 years ago

@Himeshi I have added WIP to the title. Please don't merge this one yet. I have a different and cleaner idea to resolve #26. I realize that in executing a instruction, the current implementation uses ErrorState::getError() to store the error expressions. This is problematic for two reasons:

  1. The need to maintain a parallel mapping of LLVM values to error expressions in ErrorState::valuesMap.
  2. ErrorState::valuesMap may be out of sync with the actual execution, as it is a simple mapping of LLVM values to error expression. To be correct, the LLVM values should be stacked to take into consideration recursive calls (in a return from a call, we want the parent's local values information to be stored in ErrorState::valuesMap).

I would like to change the implementation so that instead we use the error expression stored by KLEE, e.g., via Executor::bindLocal() so we depend on KLEE to perform the stacking of local values.

Perhaps a first step towards this is to change SymbolicError::propagateError()'s argument type std::vector<ref<Expr> > to std::vector<Cell> so that the member function retrieves the error expressions from the cells instead of retrieving it from valuesMap using ErrorState::getError().

domainexpert commented 7 years ago

This is subsumed, and corrected by #30: Due to propagating errors via Cell type, #30 piggybacks on KLEE's mechanism to stack local values in order to stack error values.