[klee-dev] Possibly incorrect models generated

[Alberto Barbaro]

Hi all,
I'm generating the .smt2 file for the following simple c program:

#include 

int main() {
int a;
int another;

klee_make_symbolic(, sizeof(a), "a");
klee_make_symbolic(, sizeof(another), "another");

if ( a == 77 ) {
a += 6;
another = 5;
} else {
a = 9;
if ( another == 12 ) {
a += 7;
} else {
a += 10;
}
}

return 0;
}

I can compile it using clang -I ../../include -emit-llvm -c -g simple.c and
obtain the .smt2 running klee -write-smt2s simple.bc. At this point I would
like to see the model for the 3 test case and I have the following results:

klee@a8a6399e6799:~/klee_src/examples/simple$ ktest-tool --write-ints
klee-last/test01.ktest
ktest file : 'klee-last/test01.ktest'
args   : ['simple.bc']
num objects: 2
object0: name: b'a'
object0: size: 4
object0: data: 77
object1: name: b'another'
object1: size: 4
object1: data: 0


klee@a8a6399e6799:~/klee_src/examples/simple$ ktest-tool --write-ints
klee-last/test02.ktest
ktest file : 'klee-last/test02.ktest'
args   : ['simple.bc']
num objects: 2
object0: name: b'a'
object0: size: 4
object0: data: 0
object1: name: b'another'
object1: size: 4
object1: data: 0

klee@a8a6399e6799:~/klee_src/examples/simple$ ktest-tool --write-ints
klee-last/test03.ktest
ktest file : 'klee-last/test03.ktest'
args   : ['simple.bc']
num objects: 2
object0: name: b'a'
object0: size: 4
object0: data: 0
object1: name: b'another'
object1: size: 4
object1: data: 12

I feel I'm missing something because, for instance, I cannot see the case
where a = 0 and another = 12.

Can you help me to understand if the models are correct and why?

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

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

[Frank Busse]

Hi,


On Fri, 9 Nov 2018 08:38:23 +
Alberto Barbaro  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 +
>> Alberto Barbaro  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.

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