[klee-dev] Using klee with embedded systems code

[Jason Biatek]

On 23 Jan 2014, at 4:52, Daniel Liew wrote:

> I'm afraid I don't really know what's wrong but I can offer you a few
> observations.
>
> 1. Your arrays are all one byte in size, is that intentional?

Sorry, which arrays are these? A lot of this code is auto generated by 
Simulink, the only code I've really created manually is the symbolic 
driver (in the symbolic/ directory), and I don't think any arrays in 
there are one byte. I'm no C expert, so it's possible I messed something 
up somewhere. I can't think of a place where I intentionally created one 
byte arrays.

>
> 2. The query you show is actually satisfiable (despite what the
> warning says). I took your query and modified it a little bit so I
> could get a satisfying assignment. I've attached this file (test.pc)
> which you can pass to the kleaver tool which will evaluate the
> constraints. It shows the following output.
>
> Query 0:        INVALID
>       Array 0:        KP_CLEAR[0]
>       Array 1:        KP_START[0]
>       Array 2:        KP_CLEAR_2[0]
>       Array 3:        KP_START_1[1]
>       Array 4:        KP_1[1]
>       Array 5:        KP_CLEAR_3[1]
>       Array 6:        DOOR_CLOSED_1[0]
>       Array 7:        KP_CLEAR_1[0]
> --
> total queries = 1
> total queries constructs = 39
> valid queries = 0
> invalid queries = 1
> query cex = 1
>
> KLEE's constraint solving is a little bit confusing because the
> underlying solver (STP) works in terms of validity and not
> satisifiability (so it says INVALID) but as you can see from the above
> we get satisfying assignments for each array (e.g. the first byte of
> KP_START_1 can be 1). If you'd like to know more about the constraint
> language see [1]
>
>
> [1] http://ccadar.github.io/klee/KQuery.html
>

Hmm, I will read up on this, thanks for the link. That file's helpful, 
it's good to know how I can pass that output to the solver to play with 
it a little. If anyone can help us understand this error message better, 
we'd greatly appreciate it.

Thanks,
Jason

> On 22 January 2014 22:44, Jason Biatek <biatek at cs.umn.edu> wrote:
>> First, I'm a klee noob, so I apologize if this has been previously
>> answered; I did check the archives but it didn't seem like there was 
>> an
>> equivalent post.
>>
>> We are trying to use klee for bounded test generation for some 
>> embedded
>> controller for a microwave that we generate from MATLAB embedded 
>> code.
>> The software runs as a cyclic task: there is a "step" function that 
>> runs
>> one execution step; in the embedded system, this will be called 
>> forever.
>>
>> Each "step", new inputs are sampled and outputs are computed.  In our
>> initial driver for klee, we executed a bounded loop of n-steps and
>> repeatedly initialized the inputs as symbolic and passed them to the
>> step function. This didn't seem to work, so we took the symbolic
>> initialization out of the loop, instead initializing an array:
>> pre-computing the set of inputs, if you will.
>>
>> This seems to work, mostly, but we get some warnings from klee when 
>> we
>> run the code. They are variations on this:
>>
>> KLEE: WARNING: unable to compute initial values (invalid 
>> constraints?)!
>> array KP_CLEAR[1] : w32 -> w8 = symbolic
>> array KP_START[1] : w32 -> w8 = symbolic
>> array KP_CLEAR_2[1] : w32 -> w8 = symbolic
>> array KP_START_1[1] : w32 -> w8 = symbolic
>> array KP_1[1] : w32 -> w8 = symbolic
>> array KP_CLEAR_3[1] : w32 -> w8 = symbolic
>> array DOOR_CLOSED_1[1] : w32 -> w8 = symbolic
>> array KP_CLEAR_1[1] : w32 -> w8 = symbolic
>> (query [(Eq false
>>            (Eq 0 (Read w8 0 KP_1)))
>>        (Eq 0 (Read w8 0 KP_CLEAR))
>>        (Eq 0 (Read w8 0 KP_CLEAR_1))
>>        (Eq false
>>            (Eq 0 (Read w8 0 KP_START_1)))
>>        (Eq 0 (Read w8 0 KP_START))
>>        (Eq 0 (Read w8 0 DOOR_CLOSED_1))
>>        (Eq 0 (Read w8 0 KP_CLEAR_2))
>>        (Eq false
>>            (Eq 0 (Read w8 0 KP_CLEAR_3)))]
>>       false)
>> KLEE: WARNING: unable to get symbolic solution, losing test case
>>
>> We don't understand these warnings, and when I google, I don't see 
>> much.
>> Could you help us out?  The code for the example is in github under
>> https://github.com/jbiatek/microwave.
>>
>> Thank you in advance!
>>
>> Jason and Mike
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
> [test.pc]