[klee-dev] Using klee with embedded systems code

[Jason Biatek]

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