Update Crux-llvm testing

crux-llvm/.gitignore

@@ -0,0 +1,2 @@
+**/test-data/golden/*.print_out
+results

crux-llvm/crux-llvm.cabal

@@ -179,7 +179,7 @@ test-suite crux-llvm-test
                 QuickCheck,
                 tasty            >= 0.10,
                 tasty-hunit      >= 0.10,
-                tasty-golden     >= 2.3,
+                tasty-sugar      > 1.0.1.0,
                 text,
                 what4
 

crux-llvm/test-data/golden/funnel.stp.good

@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)

crux-llvm/test-data/golden/funnel.stp.print

@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

crux-llvm/test-data/golden/funptr-array.c

@@ -0,0 +1,23 @@
+/* See https://github.com/GaloisInc/crucible/issues/10 */
+
+#include <crucible.h>
+
+typedef int int_function(int);
+
+int succ(int x) { return x+1; }
+int pred(int x) { return x-1; }
+
+int mytestfunction(int i, int j) {
+    int_function *funs[] = { succ, pred };
+    return funs[i](j);
+}
+
+int main() {
+    int arg = __VERIFIER_nondet_int();
+    int v   = __VERIFIER_nondet_int();
+    int r;
+    assuming(arg >= 0 && arg <= 1);
+    r = mytestfunction(arg, v);
+    check (r == v + 1);
+    return 0;
+}

crux-llvm/test-data/golden/funptr-array.good

@@ -0,0 +1,36 @@
+[Crux] Counter example for /home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-array.c:12:12: error: in mytestfunction
+Failed to load function handle
+Details:
+  Cannot resolve a symbolic pointer to a function handle: (ite (eq 0x0:[64] (bvSum (bvMul 0x8:[64] (bvSext 64 cX@9:bv)))) 6 7, 0x0:[64])
+[Crux] Found counterexample for verification goal
+/home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-array.c:12:12: error: in mytestfunction
+Failed to load function handle
+Details:
+  Cannot resolve a symbolic pointer to a function handle: (ite (eq 0x0:[64] (bvSum (bvMul 0x8:[64] (bvSext 64 cX@9:bv)))) 6 7, 0x0:[64])
+  The given pointer could not be resolved to a callable function
+  Cannot resolve a symbolic pointer to a function handle: (ite (eq 0x0:[64] (bvSum (bvMul 0x8:[64] (bvSext 64 cX@9:bv)))) 6 7, 0x0:[64])
+  Attempting to load callable function with type: i32(i32)
+    Via pointer: (6, 0x0:[64])
+  In memory state:
+    Stack frame mytestfunction
+      No writes or allocations
+    Stack frame main
+      No writes or allocations
+    Base memory
+      Allocations:
+        GlobalAlloc 11 0x20:[64] Immutable 1-byte-aligned [global variable  ] .str
+        GlobalAlloc 10 0x10:[64] Immutable 16-byte-aligned [global variable  ] __const.mytestfunction.funs
+        GlobalAlloc 9 0x0:[64] Immutable 1-byte-aligned [defined function ] main
+        GlobalAlloc 8 0x0:[64] Immutable 1-byte-aligned [defined function ] mytestfunction
+        GlobalAlloc 7 0x0:[64] Immutable 1-byte-aligned [defined function ] pred
+        GlobalAlloc 6 0x0:[64] Immutable 1-byte-aligned [defined function ] succ
+        GlobalAlloc 5 0x0:[64] Immutable 1-byte-aligned [external function] crucible_assert
+        GlobalAlloc 4 0x0:[64] Immutable 1-byte-aligned [external function] crucible_assume
+        GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned [external function] __VERIFIER_nondet_int
+        GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [external function] llvm.dbg.declare
+        GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] llvm.dbg.value
+      Writes:
+        Indexed chunk:
+          10 |->   *(10, 0x0:[64]) := [(6, 0x0:[64]),(7, 0x0:[64])]
+          11 |->   *(11, 0x0:[64]) := "test-data/golden/funptr-array.c\NUL"
+[Crux] Overall status: Invalid.

crux-llvm/test-data/golden/funptr-array.print

@@ -0,0 +1 @@
+*** Crux failed with non-zero result: "1"

crux-llvm/test-data/golden/funptr-array.stp.good

@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)

crux-llvm/test-data/golden/funptr-array.stp.print

@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

crux-llvm/test-data/golden/funptr-fiddle.c

@@ -0,0 +1,22 @@
+#include <crucible.h>
+
+int f(void) {
+    return 42;
+}
+
+unsigned long int g(void) {
+    return 99;
+}
+
+unsigned long int sel(int a) {
+    if (a < 10)
+        return (unsigned long int)(&f) + 1;
+    return (unsigned long int)(&g) + 0;
+}
+
+int main() {
+    int arg = 3;
+    int (*fptr)(void) = sel(arg);
+    check (fptr() == 42);
+    return 0;
+}

crux-llvm/test-data/golden/funptr-fiddle.good

@@ -0,0 +1,16 @@
+[Crux] Counter example for /home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-fiddle.c:0:0: error: in sel
+Undefined behavior encountered
+Details:
+  Addition of an offset to a pointer resulted in a pointer to an address outside of the allocation
+[Crux] Found counterexample for verification goal
+/home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-fiddle.c:0:0: error: in sel
+Undefined behavior encountered
+Details:
+  Addition of an offset to a pointer resulted in a pointer to an address outside of the allocation
+  Pointer: (3, 0x0:[64])
+  Offset: 0x1:[64]
+  Reference: 
+    The C language standard, version C11
+    §6.5.6 Additive operators, ¶8
+    Document URL: http://www.iso-9899.info/n1570.html
+[Crux] Overall status: Invalid.

crux-llvm/test-data/golden/funptr-fiddle.print

@@ -0,0 +1 @@
+*** Crux failed with non-zero result: "1"

crux-llvm/test-data/golden/funptr-fiddle.stp.good

@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)

crux-llvm/test-data/golden/funptr-fiddle.stp.print

@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

crux-llvm/test-data/golden/funptr-fiddle2.c

@@ -0,0 +1,22 @@
+#include <crucible.h>
+
+int f(void) {
+    return 42;
+}
+
+unsigned long int g(void) {
+    return 99;
+}
+
+unsigned long int sel(int a) {
+    if (a < 10)
+        return (unsigned long int)(&f) + 1 - 1;
+    return (unsigned long int)(&g) + 0;
+}
+
+int main() {
+    int arg = 3;
+    int (*fptr)(void) = sel(arg);
+    check ((fptr)() == 42);
+    return 0;
+}

crux-llvm/test-data/golden/funptr-fiddle2.good

@@ -0,0 +1,11 @@
+[Crux] Counter example for /home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-fiddle2.c:0:0: error: in sel
+Error translating constant
+Illegal operation applied to pointer argument
+
+[Crux] Found counterexample for verification goal
+/home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-fiddle2.c:0:0: error: in sel
+Error translating constant
+Illegal operation applied to pointer argument
+
+
+[Crux] Overall status: Invalid.

crux-llvm/test-data/golden/funptr-fiddle2.print

@@ -0,0 +1 @@
+*** Crux failed with non-zero result: "1"

crux-llvm/test-data/golden/funptr-fiddle2.stp.good

@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)

crux-llvm/test-data/golden/funptr-fiddle2.stp.print

@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

crux-llvm/test-data/golden/funptr-fiddle3.c

@@ -0,0 +1,22 @@
+#include <crucible.h>
+
+int f(void) {
+    return 42;
+}
+
+unsigned long int g(void) {
+    return 99;
+}
+
+unsigned long int sel(int a) {
+    if (a < 10)
+        return (unsigned long int)(&f) + 0;
+    return (unsigned long int)(&g) + 0;
+}
+
+int main() {
+    int arg = 3;
+    int (*fptr)(void) = sel(arg);
+    check ((fptr)() == 42);
+    return 0;
+}

crux-llvm/test-data/golden/funptr-fiddle3.good

@@ -0,0 +1 @@
+[Crux] Overall status: Valid.

crux-llvm/test-data/golden/funptr-fiddle3.stp.good

@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)

crux-llvm/test-data/golden/funptr-fiddle3.stp.print

@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

crux-llvm/test-data/golden/funptr.c

@@ -0,0 +1,22 @@
+#include <crucible.h>
+
+int f(void) {
+    return 42;
+}
+
+int g(void) {
+    return 99;
+}
+
+unsigned long int sel(int a) {
+    if (a < 10)
+        return (unsigned long int)(&f);
+    return (unsigned long int)(&g);
+}
+
+int main() {
+    int arg = 3;
+    int (*fptr)(void) = sel(arg);
+    check (fptr() == 42);
+    return 0;
+}

crux-llvm/test-data/golden/funptr.good

@@ -0,0 +1 @@
+[Crux] Overall status: Valid.

crux-llvm/test-data/golden/funptr.stp.good

@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)

crux-llvm/test-data/golden/funptr.stp.print

@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

crux-llvm/test-data/golden/gcd-test.boolector.good

@@ -0,0 +1,3 @@
+[Crux] user error (Invalid solver configuration:
+boolector is not a valid online solver (expected yices, cvc4, z3, or stp)
+)

crux-llvm/test-data/golden/gcd-test.boolector.print

@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

crux-llvm/test-data/golden/gcd-test.stp.good

@@ -0,0 +1,16 @@
+[Crux] Goal timeout requested but not supported by STP
+depth = 0
+depth = 1
+depth = 2
+depth = 3
+depth = 4
+depth = 5
+depth = 6
+depth = 7
+depth = 8
+depth = 9
+depth = 10
+depth = 11
+depth = 12
+????
+[Crux] user error (STP is not configured to produce UNSAT cores)

crux-llvm/test-data/golden/gcd-test.stp.print

@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

crux-llvm/test-data/golden/hello.stp.good

@@ -0,0 +1,3 @@
+[Crux] Goal timeout requested but not supported by STP
+Hello, world
+[Crux] Overall status: Valid.

crux-llvm/test-data/golden/hello2.stp.good

@@ -0,0 +1,3 @@
+[Crux] Goal timeout requested but not supported by STP
+Hello again, world
+[Crux] Overall status: Valid.

crux-llvm/test-data/golden/printing.stp.good

@@ -0,0 +1,7 @@
+[Crux] Goal timeout requested but not supported by STP
+44
+4294967252
+2c
+2C
+--------------------------
+[Crux] Overall status: Valid.

crux-llvm/test-data/golden/string.stp.good

@@ -0,0 +1,4 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] SMTLIB backend does not support function types as first class.
+CallStack (from HasCallStack):
+  error, called at src/What4/Protocol/SMTLib2.hs:369:3 in what4-1.0.0.0.99-inplace:What4.Protocol.SMTLib2

crux-llvm/test-data/golden/string.stp.print

@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

crux-llvm/test-data/golden/string2.stp.good

@@ -0,0 +1,4 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] SMTLIB backend does not support function types as first class.
+CallStack (from HasCallStack):
+  error, called at src/What4/Protocol/SMTLib2.hs:369:3 in what4-1.0.0.0.99-inplace:What4.Protocol.SMTLib2

crux-llvm/test-data/golden/string2.stp.print

@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

crux-llvm/test-data/golden/strlen_test.stp.good

@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] user error (STP is not configured to produce UNSAT cores)

crux-llvm/test-data/golden/strlen_test.stp.print

@@ -0,0 +1 @@
+*** Crux failed with exception: "ExitFailure 1"

crux-llvm/test-data/golden/strlen_test2.cvc4.good

@@ -0,0 +1,29 @@
+i = 0
+string[(length - i) - 1] = ????
+i = 1
+string[(length - i) - 1] = ????
+i = 2
+string[(length - i) - 1] = ????
+i = 3
+string[(length - i) - 1] = ????
+i = 4
+string[(length - i) - 1] = ????
+i = 5
+string[(length - i) - 1] = ????
+i = 6
+string[(length - i) - 1] = ????
+i = 7
+string[(length - i) - 1] = ????
+i = 8
+string[(length - i) - 1] = ????
+i = 9
+string[(length - i) - 1] = ????
+i = 10
+string[(length - i) - 1] = ????
+i = 11
+string[(length - i) - 1] = ????
+i = 12
+string[(length - i) - 1] = ????
+i = 13
+string[(length - i) - 1] = ????
+[Crux] Overall status: Valid.

crux-llvm/test-data/golden/strlen_test2.z3.good

@@ -0,0 +1,29 @@
+i = 0
+string[(length - i) - 1] = ????
+i = 1
+string[(length - i) - 1] = ????
+i = 2
+string[(length - i) - 1] = ????
+i = 3
+string[(length - i) - 1] = ????
+i = 4
+string[(length - i) - 1] = ????
+i = 5
+string[(length - i) - 1] = ????
+i = 6
+string[(length - i) - 1] = ????
+i = 7
+string[(length - i) - 1] = ????
+i = 8
+string[(length - i) - 1] = ????
+i = 9
+string[(length - i) - 1] = ????
+i = 10
+string[(length - i) - 1] = ????
+i = 11
+string[(length - i) - 1] = ????
+i = 12
+string[(length - i) - 1] = ????
+i = 13
+string[(length - i) - 1] = ????
+[Crux] Overall status: Valid.

crux-llvm/test-data/golden/uint-cast.stp.good

@@ -0,0 +1,6 @@
+[Crux] Goal timeout requested but not supported by STP
+bvZext 32 (bvSelect 0 8 cX@3:bv)
+bvZext 32 (bvSelect 8 8 cX@3:bv)
+bvZext 32 (bvSelect 16 8 cX@3:bv)
+bvZext 32 (bvSelect 24 8 cX@3:bv)
+[Crux] Overall status: Valid.

crux-llvm/test-data/golden/vector-gep.stp.good

@@ -0,0 +1,2 @@
+[Crux] Goal timeout requested but not supported by STP
+[Crux] Overall status: Valid.

crux-llvm/test-data/golden/vector-select.stp.good

@@ -0,0 +1,3 @@
+[Crux] Goal timeout requested but not supported by STP
+0x1:[32]
+[Crux] Overall status: Valid.