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

[Cristian Cadar]

Hi Ferhat,

Essentially, you want something like this:

printer.printExpression(arguments[1], ExprSMTLIBPrinter::SORT_BITVECTOR);

To do this right requires a bit more work, but as a quick proof of 
concept, just change the visibility of this method.

Best,
Cristian

On 03/04/2023 01:39, Ferhat Erata wrote:
> 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
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev