[klee-dev] Building constraints with Expr

[Papapanagiotakis-Bousy, Iason]

Hi Dan,



Thank you very much for the detailed response, the information you provided is hopefully all I need to implement what I am looking for.



Regards,

Jason



From: Dan Liew<mailto:dan at su-root.co.uk>
Sent: 16 December 2016 19:56
To: Papapanagiotakis-Bousy, Iason<mailto:iason.papapanagiotakis-bousy.15 at ucl.ac.uk>
Cc: klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
Subject: Re: [klee-dev] Building constraints with Expr



Hi,


> I am interested to build an Expr constraint given (in the simplest case)
> something like “x == 0”, how would I do that?

I presume that `x` refers to a symbolic variable here.

KLEE's Expr language works on Arrays rather than plain variables so in
order construct the expression you want you first need to find the
Array corresponding to it and create the appropriate read from that
Array. This usually a concatenation (ConcatExpr) of byte reads
(ReadExpr). Take a look at `Executor::executeMakeSymbolic()` to see
how the Array gets created and how it is stored.

Once you have the `Array*` you can easily create the read (assuming
you want to read the whole array from offset 0) using
`Expr::createTempRead()`. Once you have that then you could do
something like

```
ref<Expr> tempRead = Expr::createTempRead(array, width);
ref<Expr> xEqualsZero = EqExpr::create(tempRead, ConstantExpr::alloc(0, width));
```

> I have been looking at the code in include/klee/Expr.h but it doesn’t seem
> intuitive to me how to proceed.
>
>
>
> My goal is to express some constraints with Expr and subsequently query the
> solver with the getValue() function to check whether my constraints are
> satisfiable on a particular state under evaluation.
>
> If you can think any other way of achieving that without building an Expr
> please feel free to suggest it.

Creating the appropriate the `Expr` is the only sane way to do this.
Once you have the expression you will need to query the solver. BEWARE
for historical reasons KLEE's solver interface generally works in
terms of validity rather than satisfiability which is incredibly
confusing so you need to carefully construct the query.

For satisfiability you can try using solver->mayBeTrue(). Read
`Solver.h` for more detail.

Dan.
-------------- next part --------------
HTML attachment scrubbed and removed