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

[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.

Post by 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
pre-computing the set of inputs, if you will.
This seems to work, mostly, but we get some warnings from klee when we
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Jason Biatek]

Post by 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?

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.

Post by Daniel Liew
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

Post by Daniel Liew

Post by 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
pre-computing the set of inputs, if you will.
This seems to work, mostly, but we get some warnings from klee when we
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[test.pc]