about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2016-03-22 09:55:53 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2016-03-22 10:32:49 +0000
commita6e21a84f3ffa0bfb2031db2abf7e584bc07649f (patch)
treeb4d59874b000a60cb0550e67c5a29f5ba568bbd4 /test
parent253796d20214c0886cbc84fbabf0ba4bfd28a8db (diff)
downloadklee-a6e21a84f3ffa0bfb2031db2abf7e584bc07649f.tar.gz
Try to fix #348
The problem was that ``assertCreatedPointEvaluatesToTrue()`` used in the
IndependentSolver assumed that it would be given an assignment for every
array. If this wasn't the case the ``Assignment`` object by default
would just replace every read of an unknown array with a byte filled
with zeros.

This problem would appear if
``IndependentSolver::getInitialValues(...)`` was called without asking
for assignment for used arrays.

I saw two ways of fixing this

* Get an assignment for all arrays even if the client didn't ask
  for them. This guarantees that is the query is satisfiable then
  we can compute a concrete assignment.

* Just do a "best effort" check and only check expressions that can
  be fully assigned to.

I chose the latter because the first option seems pretty wasteful,
especially for an assert.

The second option isn't ideal though as it would be possible to
compute an assignment that for the whole query leads to "unsat"
but we wouldn't notice.
Diffstat (limited to 'test')
-rw-r--r--test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery15
-rw-r--r--test/regression/lit.local.cfg2
2 files changed, 17 insertions, 0 deletions
diff --git a/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery b/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery
new file mode 100644
index 00000000..9116ea47
--- /dev/null
+++ b/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery
@@ -0,0 +1,15 @@
+# RUN: %kleaver %s 2>&1 | FileCheck %s
+array n_args[4] : w32 -> w8 = symbolic
+array n_args_1[4] : w32 -> w8 = symbolic
+array A-data-stat[144] : w32 -> w8 = symbolic
+array stdin-stat[144] : w32 -> w8 = symbolic
+(query [(Ult N0:(ReadLSB w32 0 n_args) 2)
+(Slt 0 N0)
+(Ult N1:(ReadLSB w32 0 n_args_1) 3)
+(Slt 0 N1)
+(Slt 1 N1)
+(Eq false (Eq 0 (And w64 (ReadLSB w64 8 A-data-stat) 2147483647)))
+(Ult (ReadLSB w64 56 A-data-stat) 65536)
+(Eq false (Eq 0 (And w64 (ReadLSB w64 8 stdin-stat) 2147483647)))]
+(Eq false (Ult (ReadLSB w64 56 stdin-stat) 65536)) [] [n_args])
+# CHECK: INVALID
diff --git a/test/regression/lit.local.cfg b/test/regression/lit.local.cfg
new file mode 100644
index 00000000..d64daf29
--- /dev/null
+++ b/test/regression/lit.local.cfg
@@ -0,0 +1,2 @@
+# Look for .kquery files too
+config.suffixes.add('.kquery')