Crash on klee-examples/basic/polynomial.c bug

[rasoolmaghareh]

This is the output that I am seeing:

clang -emit-llvm -g -I/home/issta21-322/TracerX/tracerx/Release+Asserts/include -I/home/issta21-322/TracerX/tracerx/Release+Asserts/../include -Wno-int-conversion -c polynomial.c
SOLVER_FLAGS="-solver-backend=z3" OUTPUT_DIR=polynomial.tx make polynomial.klee-out
make[1]: Entering directory '/home/issta21-322/TracerX-examples/basic'
KLEE: output directory is "/home/issta21-322/TracerX-examples/basic/polynomial.tx"
Using Z3 solver backend
KLEE: Logging all queries in .pc format to /home/issta21-322/TracerX-examples/basic/polynomial.tx/all-queries.pc

KLEE: Logging all queries in .smt2 format to /home/issta21-322/TracerX-examples/basic/polynomial.tx/all-queries.smt2

KLEE: Deterministic memory allocation starting from 0x7ff30000000
klee: /home/issta21-322/TracerX/z3/build/include/z3++.h:1215: z3::expr z3::operator!(const z3::expr&): Assertion `a.is_bool()' failed.
0  klee            0x0000000000e983e2 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  klee            0x0000000000e97c34
2  libpthread.so.0 0x00007fe588132390
3  libc.so.6       0x00007fe5858ef438 gsignal + 56
4  libc.so.6       0x00007fe5858f103a abort + 362
5  libc.so.6       0x00007fe5858e7be7
6  libc.so.6       0x00007fe5858e7c92
7  klee            0x00000000005ea2b4
8  klee            0x00000000005e697d klee::Z3Simplification::txExpr2z3Expr(z3::expr&, z3::context&, klee::ref<klee::Expr>, std::map<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, klee::ref<klee::Expr>, std::less<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >, std::allocator<std::pair<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const, klee::ref<klee::Expr> > > >&) + 6141
9  klee            0x00000000005e61d2 klee::Z3Simplification::txExpr2z3Expr(z3::expr&, z3::context&, klee::ref<klee::Expr>, std::map<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, klee::ref<klee::Expr>, std::less<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >, std::allocator<std::pair<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const, klee::ref<klee::Expr> > > >&) + 4178
10 klee            0x00000000005e589f klee::Z3Simplification::txExpr2z3Expr(z3::expr&, z3::context&, klee::ref<klee::Expr>, std::map<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, klee::ref<klee::Expr>, std::less<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >, std::allocator<std::pair<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const, klee::ref<klee::Expr> > > >&) + 1823
11 klee            0x00000000005e589f klee::Z3Simplification::txExpr2z3Expr(z3::expr&, z3::context&, klee::ref<klee::Expr>, std::map<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, klee::ref<klee::Expr>, std::less<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >, std::allocator<std::pair<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const, klee::ref<klee::Expr> > > >&) + 1823
12 klee            0x00000000005e6558 klee::Z3Simplification::txExpr2z3Expr(z3::expr&, z3::context&, klee::ref<klee::Expr>, std::map<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, klee::ref<klee::Expr>, std::less<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >, std::allocator<std::pair<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const, klee::ref<klee::Expr> > > >&) + 5080
13 klee            0x00000000005e5eaf klee::Z3Simplification::txExpr2z3Expr(z3::expr&, z3::context&, klee::ref<klee::Expr>, std::map<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, klee::ref<klee::Expr>, std::less<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >, std::allocator<std::pair<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const, klee::ref<klee::Expr> > > >&) + 3375
14 klee            0x00000000005e9ba1 klee::Z3Simplification::simplify(klee::ref<klee::Expr>) + 241
15 klee            0x00000000005dda58 klee::TxWeakestPreCondition::PushUp(std::vector<std::pair<klee::KInstruction*, int>, std::allocator<std::pair<klee::KInstruction*, int> > >) + 600
16 klee            0x00000000005b7cd8 klee::TxTreeNode::generateWPInterpolant() + 1032
17 klee            0x00000000005be5eb klee::TxSubsumptionTableEntry::TxSubsumptionTableEntry(klee::TxTreeNode*, std::vector<llvm::Instruction*, std::allocator<llvm::Instruction*> > const&) + 1163
18 klee            0x00000000005be96b klee::TxTree::remove(klee::ExecutionState*, klee::TimingSolver*, bool) + 779
19 klee            0x000000000054a3b1 klee::Executor::updateStates(klee::ExecutionState*) + 513
20 klee            0x000000000056142e klee::Executor::run(klee::ExecutionState&) + 5982
21 klee            0x0000000000561f59 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1705
22 klee            0x000000000052825d main + 10365
23 libc.so.6       0x00007fe5858da840 __libc_start_main + 240
24 klee            0x000000000053bb69 _start + 41
Command terminated by signal 6
0.08user 0.01system 0:00.34elapsed 27%CPU (0avgtext+0avgdata 26348maxresident)k
0inputs+176outputs (0major+1715minor)pagefaults 0swaps
make[2]: Entering directory '/home/issta21-322/TracerX-examples/basic'
warning: ignoring debug info with an invalid version (1) in polynomial.bc
Writing 'cfg.polynomial.dot'...
Printing analysis 'Print CFG of function to 'dot' file' for function 'polynomial':
Writing 'cfg.main.dot'...
Printing analysis 'Print CFG of function to 'dot' file' for function 'main':
----------------------------------------------------------------------------
|    Path     |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
----------------------------------------------------------------------------
|polynomial.tx|       0|     0.00|     0.00|     0.00|     305|        0.00|
----------------------------------------------------------------------------
make[2]: Leaving directory '/home/issta21-322/TracerX-examples/basic'
make[1]: Leaving directory '/home/issta21-322/TracerX-examples/basic'

[ArpitaDutta]

This program fails while converting the Expr::Xor expr at txExpr2z3Expr().

In this program, every variable is of integer type and we are applying boolean operations on them.

int polynomial(int p1, int p2) {
  int x = 0;
  if (((2 * (p1 ^ 3)) - (p1 ^ 2) - (7 * p1) + 2) == 0) // p1=2
    x = x + 2;
  if (p2 > 5)
    x = x * 2;
  return x;
}

Here ^ is Xor operator.

During the Tx to Z3 expr conversion for Xor expressions, z3 checks whether the variables are of boolean type or not. It is failing to satisfy this condition.

As the program name suggests (polynomial.c), ^ used here is actually meant for the power operation.

[rasoolmaghareh]

Can we add support for xor to Z3 solver class?

[ArpitaDutta]

At present we are dealing with the xor operations in the following manner:

 case Expr::Xor: {
    z3::expr t1 = c.bool_val(false);
    bool r1 = txExpr2z3Expr(t1, c, txe->getKid(0), emap);
    if (r1) {
      z3::expr t2 = c.bool_val(false);
      bool r2 = txExpr2z3Expr(t2, c, txe->getKid(1), emap);
      if (r2) {
        z3e = not(not(t2) && not(t1));
        return true;
      }
    }
    return false;
  }

We are utilizing the not operator from Z3++.h to formulate the Xor operator. The code for not in Z3++.h is as follows:

 inline expr operator!(expr const & a) { //std::cout<<"not !!";
    assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }

This function checks whether the operand is Boolean or not. Since our operands are not Boolean type, we are facing the crash.

[rasoolmaghareh]

Let's try to add a warning message for this case to avoid a crash and not do the simplification.

[ArpitaDutta]

Avoided Z3simplification whenever a non-boolean operand is passed to XOR or NOT operators. (Commit 4b0c2b8dfc11794dceef381b8498af892af91015)

[ArpitaDutta]

WP output:

************Basic Block Coverage Report Starts****************
KLEE: done: Total number of single time Visited Basic Blocks: 5
KLEE: done: Total number of Basic Blocks: 6
************Basic Block Coverage Report Ends****************
************ICMP/Atomic Condition Coverage Report Starts****************
KLEE: done: Total number of Covered ICMP/Atomic Condition: 2
KLEE: done: Total number of All ICMP/Atomic Condition: 2
************ICMP/Atomic Condition Coverage Report Ends****************
KLEE: Memory cap NOT exceeded!

KLEE: done: Total reduced symbolic execution tree nodes = 3
KLEE: done: Total number of visited basic blocks = 5

KLEE: done: Subsumption statistics
KLEE: done:     Time for actual solver calls in subsumption check (ms) = 0
KLEE: done:     Number of solver calls for subsumption check (failed) = 0 (0)
KLEE: done:     Concrete store expression build time (ms) = 0
KLEE: done:     Symbolic store expression build time (ms) = 0
KLEE: done:     Solver access time (ms) = 0
KLEE: done:     Average table entries per subsumption checkpoint = 1.00
KLEE: done:     Number of subsumption checks = 3
KLEE: done:     Average solver calls per subsumption check = 0.00

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 0.199
KLEE: done:     remove = 1.731
KLEE: done:     subsumptionCheck = 0.138
KLEE: done:     markPathCondition = 0.041
KLEE: done:     split = 0.02
KLEE: done:     executeOnNode = 0.107
KLEE: done:     executeMemoryOperation = 0.546

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.002
KLEE: done:     get WP Interpolant = 0.956
KLEE: done:     addConstraintTime = 0.098
KLEE: done:     splitTime = 0.016
KLEE: done:     execute = 0.097
KLEE: done:     bindCallArguments = 0.008
KLEE: done:     bindReturnValue = 0.005
KLEE: done:     getStoredExpressions = 0
KLEE: done:     getStoredCoreExpressions = 0.01

KLEE: done: total instructions = 42
KLEE: done: completed paths = 2, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 1
KLEE: done:     average branching depth of subsumed paths = 0
KLEE: done:     average instructions of completed paths = 35.5
KLEE: done:     average instructions of subsumed paths = 0
KLEE: done:     subsumed paths = 0
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 2
KLEE: done: generated tests = 0, among which
KLEE: done:     early-terminating tests (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     error tests = 0
KLEE: done:     program exit tests = 0

KLEE: done: NOTE:
KLEE: done:     Subsumed paths / tests counts are nondeterministic for
KLEE: done:     programs with dynamically-allocated memory such as those
KLEE: done:     using malloc, since KLEE may reuse the address of the
KLEE: done:     same malloc calls in different paths. This nondeterminism
KLEE: done:     does not cause loss of error reports.
--------------------------------------------------------------------------------------
|         Path          |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
--------------------------------------------------------------------------------------
|polynomial-3/klee-out-0|      42|     0.14|    12.79|     4.29|     305|       93.77|
--------------------------------------------------------------------------------------

[rasoolmaghareh]

Issue Fixed.