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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
