[klee-dev] Using klee with embedded systems code

[Daniel Liew]

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?

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

Thanks,
Dan.

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.pc
Type: application/octet-stream
Size: 1215 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20140123/d8dc167a/attachment.obj>