Re: [klee-dev] Path constraints as equations of integers

[Dan Liew]

Hi,

On 1 November 2016 at 12:17, Papapanagiotakis-Bousy, Iason
 wrote:
> Hello,
>
>
>
> I am a new user of KLEE, I was looking into symbolic execution in order to
> extract the constraints of the input variables of a program for each path in
> the code.
>
> Following the initial tutorials and searching on the web I’ve managed to get
> both the KQuery and SMT2 formatted constraints generated by KLEE.
>
>
>
> I was wondering if there is a (new) capability of KLEE or an available
> script/tool to generate the constraints as a systems of equations of
> integers and not Bit Vectors as the default output in KQuery and SMT2 is.

There is no option for this. KLEE analyses programs precisely so it
has no use for printing
expressions in an approximate form (i.e. using integers).

You of course could do this yourself by either modifying KLEE's
ExprSMTLIBPrinter class
to print KLEE's expressions differently or write your own tool to
parse QF_ABV queries
and rewrite them as AUFNIRA queries.

I don't know if there any existing tools to rewrite QF_ABV constraints
to AUFNIRA.

> While the output generated works fine with SMT solvers for the main purpose
> of KLEE, it would help a lot if constraints could also be presented in a
> human-friendly way.

KLEE does have a few options to make the printed SMT-LIBv2 queries
slightly easier
to read (`-smtlib-human-readable`, `-smtlib-abbreviation-mode`,
`-smtlib-display-constants`).
These might help you.

Thanks,
Dan.

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

Re: [klee-dev] Print out intermediate symbolic representation for each path instead on generating test-case for each path

[Dan Liew]

Hi,

On 2 November 2016 at 15:52,   wrote:
> Dear Klee developers,
>
>
> I am trying to use Klee for specification generation. To do that I need
> Klee's intermediate symbolic results. Specifically, I need the guards of
> each path in the program to be printed in their symbolic forms.  For
> example, in the following program:
>
>
> get_sign(int a,char * sign)
>
> {
>
>  if (a==0)  *sign = 0;
>
> else if (a<0)  *sign = -1;
>
> else *sign = 1;
>
> }
>
>
> I want,
>
>
> Path1 : (a==0)
>
> Path2 : (a<0)
>
> Path3: (a>0)
>
>
> as output and if it is possible to have the value of sign or the range of
> sign value for each path.
>
>
> Path1: (a==0)==> *sign = 0;
>
> Path2: (a<0)==> *sign = -1;
>
> Path3: (a>0)==> *sign = 1;

Whilst KLEE is running you can use the `klee_print_expr()` (see
`include/klee/klee.h`) to print the representation of an expression
for debugging purposes. E.g. in example you would do

```
klee_print_expr("ANYTHING", a)
```

However for more complicated programs you should just look at the
generated constraints for each path. You can use
the `-write-smt2s` to write the constraints for each path in SMT-LIBv2
format. You can also use `-write-pcs` to write the constraints
in KLEE's native constraint language.

HTH,
Dan

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