Improve handling of constant array in Z3

2 files changed, 39 insertions, 0 deletions

diff --git a/test/Solver/Z3ConstantArray.c b/test/Solver/Z3ConstantArray.c
new file mode 100644
index 00000000..482679e9
--- /dev/null
+++ b/test/Solver/Z3ConstantArray.c
@@ -0,0 +1,28 @@
+// REQUIRES: z3
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out -solver-backend=z3 -write-cvcs -write-smt2s -debug-z3-dump-queries=%t.smt2   %t1.bc
+// RUN: cat %t.klee-out/test000001.smt2 | FileCheck --check-prefix=TEST-CASE %s
+// RUN: cat %t.klee-out/test000002.smt2 | FileCheck --check-prefix=TEST-CASE %s
+// RUN: cat %t.smt2 | FileCheck %s
+
+#include "klee/klee.h"
+
+int main(int argc, char **argv) {
+  // CHECK-DAG: (assert (= (select const_arr11 #x00000000) #x67))
+  // CHECK-DAG: (assert (= (select const_arr11 #x00000001) #x79))
+  // CHECK-DAG: (assert (= (select const_arr11 #x00000002) #x7a))
+  // CHECK-DAG: (assert (= (select const_arr11 #x00000003) #x00))
+  // TEST-CASE-DAG: (assert (=  (select const_arr1 (_ bv0 32) ) (_ bv103 8) ) )
+  // TEST-CASE-DAG: (assert (=  (select const_arr1 (_ bv1 32) ) (_ bv121 8) ) )
+  // TEST-CASE-DAG: (assert (=  (select const_arr1 (_ bv2 32) ) (_ bv122 8) ) )
+  // TEST-CASE-DAG: (assert (=  (select const_arr1 (_ bv3 32) ) (_ bv0 8) ) )
+  char c[4] = {'g', 'y', 'z', '\0'};
+  unsigned i;
+  klee_make_symbolic(&i, sizeof i, "i");
+  klee_assume(i < 4);
+  if (c[i] < 'y')
+    return 0;
+  else
+    return 1;
+}
diff --git a/test/Solver/Z3LargeConstantArray.kquery b/test/Solver/Z3LargeConstantArray.kquery
new file mode 100644
index 00000000..c6f9aa76
--- /dev/null
+++ b/test/Solver/Z3LargeConstantArray.kquery
@@ -0,0 +1,11 @@
+# REQUIRES: z3
+# RUN: %kleaver -solver-backend=z3 -max-solver-time=20 -debug-z3-dump-queries=%t.smt2  %s &> /dev/null
+# RUN: grep '(assert (= (select const_arr10' %t.smt2 -c | grep 3770
+array const_arr10[3770] : w32 -> w8 = [32 0 0 0 192 193 124 5 0 0 0 0 64 242 107 41 0 0 0 0 48 235 107 41 0 0 0 0 0 0 0 0 0 0 0 0 144 0 0 0 14 0 0 0 0 0 0 0 10 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 144 33 0 0 65 42 0 0 5 0 0 0 0 0 0 0 7 136 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 16 146 162 90 0 0 0 0 55 110 115 21 0 0 0 0 83 146 162 90 0 0 0 0 55 110 115 21 0 0 0 0 75 204 147 90 0 0 0 0 55 110 115 21 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 121 0 0 0 100 101 102 105 110 101 40 96 98 39 44 32 96 117 39 41 10 100 101 102 105 110 101 40 96 104 39 44 32 96 108 39 41 10 100 101 102 105 110 101 40 96 105 39 44 32 96 107 39 41 10 100 101 102 105 110 101 40 96 121 39 44 32 96 107 39 41 10 100 101 102 105 110 101 40 96 65 39 44 32 96 108 39 41 10 100 101 102 105 110 101 40 96 110 39 44 32 50 41 10 100 101 102 105 110 101 40 96 80 39 44 32 50 41 10 0 10 0 10 0 10 128 2 0 0 3 0 0 0 0 0 0 0 200 67 198 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 248 255 255 255 255 255 255 255 252 255 255 255 255 255 255 255 0 0 0 0 0 0 0 0 249 77 23 3 0 0 0 0 160 42 129 41 0 0 0 0 252 255 255 255 255 255 255 255 0 0 0 0 255 255 255 255 252 255 255 255 255 255 255 255 0 0 0 0 0 0 0 0 252 255 255 255 255 255 255 255 0 0 0 0 0 0 0 0 252 255 255 255 255 255 255 255 0 0 0 0 0 0 0 0 252 255 255 255 255 255 255 255 64 13 129 41 0 0 0 0 56 217 22 3 0 0 0 0 96 168 132 41 0 0 0 0 255 255 255 255 255 255 255 255 33 4 0 0 0 0 0 0 48 24 129 41 0 0 0 0 80 43 125 41 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 248 255 255 255 255 255 255 255 176 23 129 41 0 0 0 0 252 255 255 255 255 255 255 255 16 14 129 41 0 0 0 0 252 255 255 255 255 255 255 255 32 227 132 41 0 0 0 0 252 255 255 255 255 255 255 255 208 251 132 41 0 0 0 0 252 255 255 255 255 255 255 255 144 16 129 41 0 0 0 0 252 255 255 255 255 255 255 255 192 3 133 41 0 0 0 0 252 255 255 255 255 255 255 255 96 3 133 41 0 0 0 0 252 255 255 255 255 255 255 255 176 26 124 41 0 0 0 0 252 255 255 255 255 255 255 255 16 27 124 41 0 0 0 0 252 255 255 255 255 255 255 255 16 51 124 41 0 0 0 0 252 255 255 255 255 255 255 255 48 59 129 41 0 0 0 0 252 255 255 255 255 255 255 255 0 68 0 0 0 105 110 116 101 114 110 97 108 32 101 114 114 111 114 32 100 101 116 101 99 116 101 100 59 32 112 108 101 97 115 101 32 114 101 112 111 114 116 32 116 104 105 115 32 98 117 103 32 116 111 32 60 98 117 103 45 109 52 64 103 110 117 46 111 114 103 62 0 19 0 0 0 83 101 103 109 101 110 116 97 116 105 111 110 32 102 97 117 108 116 0 8 0 0 0 65 98 111 114 116 101 100 0 20 0 0 0 73 108 108 101 103 97 108 32 105 110 115 116 114 117 99 116 105 111 110 0 25 0 0 0 70 108 111 97 116 105 110 103 32 112 111 105 110 116 32 101 120 99 101 112 116 105 111 110 0 10 0 0 0 66 117 115 32 101 114 114 111 114 0 2 0 0 0 96 0 2 0 0 0 39 0 2 0 0 0 35 0 2 0 0 0 10 0 40 0 0 0 32 136 117 41 0 0 0 0 24 107 198 4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 40 1 0 0 20 25 100 59 116 43 0 0 2 27 100 59 116 43 0 0 223 24 100 59 116 43 0 0 0 0 0 0 0 0 0 0 189 22 100 59 116 43 0 0 181 25 100 59 116 43 0 0 140 30 100 59 116 43 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 58 24 100 59 116 43 0 0 228 29 100 59 116 43 0 0 242 22 100 59 116 43 0 0 5 24 100 59 116 43 0 0 0 0 0 0 0 0 0 0 1 29 100 59 116 43 0 0 167 24 100 59 116 43 0 0 148 23 100 59 116 43 0 0 134 22 100 59 116 43 0 0 114 27 100 59 116 43 0 0 219 21 100 59 116 43 0 0 96 23 100 59 116 43 0 0 0 0 0 0 0 0 0 0 236 25 100 59 116 43 0 0 0 0 0 0 0 0 0 0 60 29 100 59 116 43 0 0 126 25 100 59 116 43 0 0 37 26 100 59 116 43 0 0 0 0 0 0 0 0 0 0 28 30 100 59 116 43 0 0 41 23 100 59 116 43 0 0 116 29 100 59 116 43 0 0 81 22 100 59 116 43 0 0 148 26 100 59 116 43 0 0 0 0 0 0 0 0 0 0 224 27 100 59 116 43 0 0 74 25 100 59 116 43 0 0 84 30 100 59 116 43 0 0 40 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 7 22 100 59 116 43 0 0 2 0 0 0 0 48 0 0 248 158 196 4 0 0 0 0 10 0 0 0 99 104 97 110 103 101 99 111 109 0 40 0 0 0 204 23 100 59 116 43 0 0 0 0 128 48 0 0 0 0 65 22 100 59 116 43 0 0 2 0 0 0 170 133 41 0 248 160 196 4 0 0 0 0 12 0 0 0 99 104 97 110 103 101 113 117 111 116 101 0 40 0 0 0 172 29 100 59 116 43 0 0 8 0 0 0 0 0 0 0 125 22 100 59 116 43 0 0 2 0 0 0 0 0 0 38 200 163 196 4 0 0 0 0 5 0 0 0 100 101 99 114 0 40 0 0 0 0 0 0 0 0 0 0 0 12 0 80 120 0 0 0 0 178 22 100 59 116 43 0 0 2 0 0 0 0 0 0 0 152 166 196 4 0 0 0 0 7 0 0 0 100 101 102 105 110 101 0 40 0 0 0 25 28 100 59 116 43 0 0 8 0 0 0 0 0 0 0 233 22 100 59 116 43 0 0 2 0 0 0 17 148 64 0 88 170 196 4 0 0 0 0 5 0 0 0 100 101 102 110 0 40 0 0 0 112 24 100 59 116 43 0 0 0 0 0 0 0 0 0 0 30 23 100 59 116 43 0 0 2 0 0 0 160 0 32 7 56 172 196 4 0 0 0 0 7 0 0 0 100 105 118 101 114 116 0 40 0 0 0 81 28 100 59 116 43 0 0 0 0 0 0 0 0 0 0 85 23 100 59 116 43 0 0 2 0 0 0 0 0 0 48 40 173 196 4 0 0 0 0 7 0 0 0 100 105 118 110 117 109 0 40 0 0 0 93 26 100 59 116 43 0 0 0 154 4 0 0 0 0 0 140 23 100 59 116 43 0 0 2 0 0 0 0 0 0 0 24 174 196 4 0 0 0 0 4 0 0 0 100 110 108 0 40 0 0 0 59 27 100 59 116 43 0 0 0 121 34 0 0 0 0 0 192 23 100 59 116 43 0 0 2 0 0 0 160 176 133 41 8 175 196 4 0 0 0 0 8 0 0 0 100 117 109 112 100 101 102 0 40 0 0 0 138 28 100 59 116 43 0 0 8 0 0 0 0 0 0 0 248 23 100 59 116 43 0 0 2 0 0 0 0 0 0 0 24 236 197 4 0 0 0 0 9 0 0 0 101 114 114 112 114 105 110 116 0 40 0 0 0 0 0 0 0 0 0 0 0 8 0 0 64 0 0 0 0 49 24 100 59 116 43 0 0 2 0 0 0 1 0 0 0 24 242 197 4 0 0 0 0 5 0 0 0 101 118 97 108 0 40 0 0 0 0 0 0 0 0 0 0 0 8 41 0 0 0 0 0 0 102 24 100 59 116 43 0 0 2 0 0 0 0 0 73 1 152 243 197 4 0 0 0 0 6 0 0 0 105 102 100 101 102 0 40 0 0 0 0 0 0 0 0 0 0 0 8 0 0 0 0 0 0 0 156 24 100 59 116 43 0 0 2 0 0 0 0 0 0 0 88 244 197 4 0 0 0 0 7 0 0 0 105 102 101 108 115 101 0 40 0 0 0 0 0 0 0 0 0 0 0 8 203 0 0 0 0 0 0 211 24 100 59 116 43 0 0 2 0 0 0 0 0 0 0 24 245 197 4 0 0 0 0 8 0 0 0 105 110 99 108 117 100 101 0 40 0 0 0 0 0 0 0 0 0 0 0 8 0 0 0 0 0 0 0 11 25 100 59 116 43 0 0 2 0 0 0 0 0 0 0 152 246 197 4 0 0 0 0 5 0 0 0 105 110 99 114 0 40 0 0 0 195 28 100 59 116 43 0 0 8 0 0 0 0 0 0 0 64 25 100 59 116 43 0 0 2 0 0 0 96 176 133 41 88 247 197 4 0 0 0 0 6 0 0 0 105 110 100 101 120 0 40 0 0 0 204 26 100 59 116 43 0 0 8 0 0 0 0 0 0 0 118 25 100 59 116 43 0 0 2 0 0 0 0 0 0 0 152 249 197 4 0 0 0 0 4 0 0 0 108 101 110 0 40 0 0 0 0 0 0 0 0 0 0 0 0 52 33 0 0 0 0 0 170 25 100 59 116 43 0 0 2 0 0 0 9 63 116 43 88 250 197 4 0 0 0 0 7 0 0 0 109 52 101 120 105 116 0 40 0 0 0 0 0 0 0 0 0 0 0 8 0 0 176 0 0 0 0 225 25 100 59 116 43 0 0 2 0 0 0 0 0 0 0 72 251 197 4 0 0 0 0 7 0 0 0 109 52 119 114 97 112 0 40 0 0 0 169 27 100 59 116 43 0 0 8 0 0 0 0 0 0 0 24 26 100 59 116 43 0 0 2 0 0 0 20 0 0 30 88 118 196 4 0 0 0 0 9 0 0 0 109 97 107 101 116 101 109 112 0 40 0 0 0 0 0 0 0 0 0 0 0 8 0 0 176 0 0 0 0 81 26 100 59 116 43 0 0 2 0 0 0 8 0 0 0 40 121 196 4 0 0 0 0 8 0 0 0 109 107 115 116 101 109 112 0 40 0 0 0 0 0 0 0 0 0 0 0 8 0 0 0 0 0 0 0 137 26 100 59 116 43 0 0 2 0 0 0 0 0 0 0 168 7 198 4 0 0 0 0 7 0 0 0 112 111 112 100 101 102 0 40 0 0 0 0 0 0 0 0 0 0 0 12 0 0 64 0 0 0 0 192 26 100 59 116 43 0 0 2 0 0 0 192 122 127 41 152 8 198 4 0 0 0 0 8 0 0 0 112 117 115 104 100 101 102 0 40 0 0 0 0 0 0 0 0 0 0 0 8 0 0 0 0 0 0 0 248 26 100 59 116 43 0 0 2 0 0 0 0 0 0 0 120 10 198 4 0 0 0 0 6 0 0 0 115 104 105 102 116 0 40 0 0 0 0 0 0 0 0 0 0 0 8 0 0 0 0 0 0 0 46 27 100 59 116 43 0 0 2 0 0 0 0 0 52 0 104 11 198 4 0 0 0 0 9 0 0 0 115 105 110 99 108 117 100 101 0 40 0 0 0 0 0 0 0 0 0 0 0 8 0 0 0 0 0 0 0 103 27 100 59 116 43 0 0 2 0 0 0 0 0 0 0 88 12 198 4 0 0 0 0 7 0 0 0 115 117 98 115 116 114 0 40 0 0 0 0 0 0 0 0 0 0 0 8 0 0 0 0 0 0 0 158 27 100 59 116 43 0 0 2 0 0 0 0 0 64 11 72 13 198 4 0 0 0 0 7 0 0 0 115 121 115 99 109 100 0 40 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 213 27 100 59 116 43 0 0 2 0 0 0 0 0 0 48 56 14 198 4 0 0 0 0 7 0 0 0 115 121 115 118 97 108 0 40 0 0 0 0 0 0 0 0 0 0 0 0 0 0 64 0 0 0 0 12 28 100 59 116 43 0 0 2 0 0 0 0 0 0 0 40 15 198 4 0 0 0 0 9 0 0 0 116 114 97 99 101 111 102 102 0 40 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 69 28 100 59 116 43 0 0 2 0 0 0 0 0 0 0 8 234 197 4 0 0 0 0 8 0 0 0 116 114 97 99 101 111 110 0 40 0 0 0 0 0 0 0 0 0 0 0 8 0 0 0 0 0 0 0 125 28 100 59 116 43 0 0 2 0 0 0 0 0 0 192 248 234 197 4 0 0 0 0 9 0 0 0 116 114 97 110 115 108 105 116 0 40 0 0 0 0 0 0 0 0 0 0 0 8 41 0 0 0 0 0 0 182 28 100 59 116 43 0 0 2 0 0 0 0 0 0 0 200 22 198 4 0 0 0 0 9 0 0 0 117 110 100 101 102 105 110 101 0 40 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 239 28 100 59 116 43 0 0 2 0 0 0 0 112 8 0 184 23 198 4 0 0 0 0 9 0 0 0 117 110 100 105 118 101 114 116 0 1 0 0 0 0 40 0 0 0 0 0 0 0 0 0 0 0 0 99 8 0 0 0 0 0 45 29 100 59 116 43 0 0 1 0 0 0 0 0 0 224 252 28 100 59 116 43 0 0 5 0 0 0 117 110 105 120 0 2 0 0 0 117 0 40 0 0 0 0 0 0 0 0 0 0 0 0 255 95 52 0 0 0 0 104 29 100 59 116 43 0 0 1 0 0 0 240 43 134 41 54 29 100 59 116 43 0 0 2 0 0 0 98 0 2 0 0 0 108 0 40 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 160 29 100 59 116 43 0 0 1 0 0 0 87 0 0 0 110 29 100 59 116 43 0 0 2 0 0 0 104 0 2 0 0 0 107 0 40 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 216 29 100 59 116 43 0 0 1 0 0 0 3 24 0 128 166 29 100 59 116 43 0 0 2 0 0 0 105 0 2 0 0 0 107 0 40 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 16 30 100 59 116 43 0 0 1 0 0 0 64 236 0 0 222 29 100 59 116 43 0 0 2 0 0 0 121 0 2 0 0 0 108 0 40 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 72 30 100 59 116 43 0 0 1 0 0 0 48 0 0 0 22 30 100 59 116 43 0 0 2 0 0 0 65 0 2 0 0 0 50 0 40 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 128 30 100 59 116 43 0 0 1 0 0 0 48 120 134 41 78 30 100 59 116 43 0 0 2 0 0 0 110 0 2 0 0 0 50 0 40 0 0 0 21 22 100 59 116 43 0 0 0 0 0 0 0 0 0 0 184 30 100 59 116 43 0 0 1 0 0 0 0 0 0 0 134 30 100 59 116 43 0 0 2 0 0 0 80 0]
+array stdin[121] : w32 -> w8 = symbolic
+(query
+[] 
+(Eq (Add w8 192 0) (Read w8 (ZExt w32 (Read w8 0 stdin)) const_arr10))
+[]
+[stdin])
+