[klee-dev] Getting symbolic expressions from the symbolic store with `klee_print_expr`

[Ferhat Erata]

Hi,

I wanted to ask about converting symbolic expressions in KQuery format
to SMTLIB format.

Currently, I am able to obtain the symbolic expressions using
`klee_print_expr` in KQuery format, but I need to manipulate them in
bit-vector logic, which requires converting them to SMTLIB format to
process them with preferably with Z3 or STP. I tried to modify the
code in `SpecialFunctionHandler.cpp` to generate SMTLIB expressions.
However, the resulting expressions are invalid assertions.

I have included an example in the email to illustrate my situation. I
would appreciate it if you could provide me with feedback.

Thank you for your time and assistance.

Best,
~ Ferhat

------------------------------------------

Please find an example in the following:
```
#include "klee/klee.h"

int main(int argc, char *argv[]) {
  int x;
  klee_make_symbolic(&x, sizeof(x), "x");
  int b, c;
  b = x + 10;
  klee_print_expr("b", b);
  c = x * x;
  klee_print_expr("c", c);
}
```

KLEE returns the following output in KQuery representations for those
variables as expected:
```
b:(Add w32 10
          (ReadLSB w32 0 x))
c:(Mul w32 N0:(ReadLSB w32 0 x)
          N0)
```

The first thing that came to my mind was to convert those expressions
to SMTLIB expressions. Therefore, I changed the code in
`SpecialFunctionHandler.cpp` as follows:
```
void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state,
                                  KInstruction *target,
                                  std::vector<ref<Expr> > &arguments) {
  assert(arguments.size()==2 &&
         "invalid number of arguments to klee_print_expr");

  std::string msg_str = readStringAtAddress(state, arguments[0]);
  llvm::errs() << msg_str << ":" << arguments[1] << "\n";

  llvm::errs() << "----\n";
  ExprSMTLIBPrinter printer;
  printer.setOutput(llvm::errs());
  Query query(state.constraints, arguments[1]);
  printer.setQuery(query);
  printer.generateOutput();
}
```

Now, I get the following:
```
b:(Add w32 10
          (ReadLSB w32 0 x))
(set-logic QF_AUFBV )
(declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (=  (_ bv4294967286 32) (concat  (select  x (_ bv3 32) )
(concat  (select  x (_ bv2 32) ) (concat  (select  x (_ bv1 32) )
(select  x (_ bv0 32) ) ) ) ) ) )
(check-sat)
(exit)

c:(Mul w32 N0:(ReadLSB w32 0 x)
          N0)
(set-logic QF_AUFBV )
(declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (=  (_ bv0 32) (bvmul  (! (concat  (select  x (_ bv3 32) )
(concat  (select  x (_ bv2 32) ) (concat  (select  x (_ bv1 32) )
(select  x (_ bv0 32) ) ) ) ) :named ?B1) ?B1 ) ) )
(check-sat)
(exit)
```

However, you can see that the code that I added turns them into
invalid assertions, however, I would expect getting symbolic
expressions that is semantically equivalent to those of KQuery:
```
[4294967286 ==
 Concat(x[3], Concat(x[2], Concat(x[1], x[0])))]
------------------------
[0 ==
 Concat(x[3], Concat(x[2], Concat(x[1], x[0])))*
 Concat(x[3], Concat(x[2], Concat(x[1], x[0])))]
```

I would expect something similar to this with an additional symbolic input:
```
[Concat(b[3], Concat(b[2], Concat(b[1], b[0]))) == 10 +
 Concat(x[3], Concat(x[2], Concat(x[1], x[0])))]
------------------------
[Concat(c[3], Concat(c[2], Concat(c[1], c[0]))) ==
 Concat(x[3], Concat(x[2], Concat(x[1], x[0])))*
 Concat(x[3], Concat(x[2], Concat(x[1], x[0])))]
```

Best,
~ Ferhat