Range analysis using Klee

[Radu Stoenescu]

Hello,

I am trying to use Klee for performing a very trivial range analysis: I
would like to see what is the set of possible values of a given symbol just
before existing a function call.

After some more convoluted attempts I settled for the following approach:
In the *framePopped *method of StatsTracker I am trying to find the symbol
in the AddressSpace pertaining to the current ExecutionState and if the
symbol is found I invoke the *read* method of the corresponding ObjectSpace
instance. Finally this expression is passed to the *getRange *of the
currently employed solver, along with the ExecutionState (which carries the
constraints currently in place).

The trouble is that my above approach doesn't seem to work, even in the
simplest example: an unsigned integer multiplied by 2. No matter what I do
- the range is 0 - 2^32-1 (no constraints or mutations seem to affect this
output).

Is this the bad way of doing things or am I just a poor coder and I messed
things up along the way ?

Many thanks,
Radu.

[Oscar Soria Dustmann]

Hi Radu,

we're currently working on something very related to this. However, you
can already have klee tell you the closure of the admissible range for a
given expression. Could you send us the code that doesn't work for you?
For one thing, are you talking about running code that calls special
functions or did you modify klee itself? In order to help you out it
would be helpful to see the code.

Cheers, Oscar

Post by Radu Stoenescu
Hello,
I am trying to use Klee for performing a very trivial range analysis: I
would like to see what is the set of possible values of a given symbol just
before existing a function call.
In the *framePopped *method of StatsTracker I am trying to find the symbol
in the AddressSpace pertaining to the current ExecutionState and if the
symbol is found I invoke the *read* method of the corresponding ObjectSpace
instance. Finally this expression is passed to the *getRange *of the
currently employed solver, along with the ExecutionState (which carries the
constraints currently in place).
The trouble is that my above approach doesn't seem to work, even in the
simplest example: an unsigned integer multiplied by 2. No matter what I do
- the range is 0 - 2^32-1 (no constraints or mutations seem to affect this
output).
Is this the bad way of doing things or am I just a poor coder and I messed
things up along the way ?
Many thanks,
Radu.
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev