[klee-dev] How to remove the current state from states?

[Frank Busse]

Hi,


On Fri, 9 Nov 2018 08:38:23 +0000
Alberto Barbaro <barbaro.alberto at gmail.com> wrote:

> Thanks for your answer. I still have problem with this searcher anyway. For
> me it is not obvious how to select between 10 states. This happens after
> the first branch encountered in the code. So at the moment I'm iterating on
> all of them and discard it one by one if I encountere an instruction that
> is not in instruction.txt. do you think this approach is fine or for
> example I should save all the states encountered during the execution with
> real input and using them just reexecute the same path but with symbolic
> input?

sorry, I haven't read the thread about the guided search. I guess what
you have now is a trace in instructions.txt of a single state (the run
with concrete). And you want to replicate that trace in a second run on
symbolic data with a new searcher. Correct?

First of all, I'm not sure if this works as the trace in the second run
might differ from the first:
- imho the setup code for symbolic file handling from POSIX layer
  should be in the new trace
- setup routines for uclibc might behave differently and introduce
  divergences

You have to analyse where the branch happens and if there exist an
identical trace among your states. If this is not the case, you could
for instance start filtering states beginning with your program's main()
etc..

To your question: assuming that this approach works, you need to check
if the current instruction of a state is at the correct position in your
instructions.txt. The "position" in file is the line number and in your
state it should be state.steppedInstructions. If it doesn't match, you
can terminate or postpone the state, depending on your use case.

If you need to introduce a mitigation as above you obviously have to
keep an additional offset per state to fix divergences.


Kind regards,

Frank

>> On Sat, 3 Nov 2018 17:21:02 +0000
>> Alberto Barbaro <barbaro.alberto at gmail.com> wrote:
>>  
>>> Just a quick one. Can I use the same approach for the current state and
>>> just remove it?  
>>
>> from a searcher? The current state is only passed in
>> Executor::updateStates - so this should be fine. But we still have issue
>> #952 (easy to fix) in case sth. goes wrong.