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 <[email protected]> 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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[test.pc]
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
