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

2023-04-03 Thread 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(, 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 ,
   KInstruction *target,
   std::vector > ) {
   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

Re: [klee-dev] General question

2023-04-03 Thread Cristian Cadar 

Hi both,

Let me answer this as part of the more detailed email Ferhat sent today.

But more generally, you can use Kleaver to load queries in KQuery format 
and print them to SMT-LIB2 format:


kleaver --print-smtlib file.kquery

Best,
Cristian

On 30/03/2023 21:57, Ferhat Erata wrote:

Hi Teja,

I was also looking for this feature. Have you come up with a workaround?

Do you know if there is a way to transform expressions in kquery format 
to smt2 format?


Best,
~ Ferhat


On Mon, Jan 9, 2023 at 7:21 AM Teja Sai Srikar Bodavula 
mailto:btssri...@gmail.com>> wrote:


Hello, I was wondering if there is way in which we can get
symbolic formula for a variable in a code in smt2 format unlike
kquery format which we get using klee_print_expr.
___
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


___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] General question

2023-04-03 Thread Ferhat Erata 
Hi Teja,

I was also looking for this feature. Have you come up with a workaround?

Do you know if there is a way to transform expressions in kquery format to
smt2 format?

Best,
~ Ferhat


On Mon, Jan 9, 2023 at 7:21 AM Teja Sai Srikar Bodavula 
wrote:

> Hello, I was wondering if there is way in which we can get
> symbolic formula for a variable in a code in smt2 format unlike
> kquery format which we get using klee_print_expr.
> ___
> 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

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

2023-04-03 Thread 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(, 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 ,
  KInstruction *target,
  std::vector > ) {
  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