Use llvm_ffi_verify in test_ffi_verify tests

GaloisInc · Oct 2, 2023 · 24675b8 · 24675b8
1 parent 3a11886
commit 24675b8
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 20 deletions.
diff --git a/intTests/test_ffi_verify/test.saw b/intTests/test_ffi_verify/test.saw
@@ -3,45 +3,46 @@ enable_experimental;
 import "test.cry";
 mod <- llvm_load_module "test.bc";
 
-llvm_verify mod "add8" [] true (llvm_ffi_setup {{ add8 }}) z3;
-llvm_verify mod "sub16" [] true (llvm_ffi_setup {{ sub16 }}) z3;
-llvm_verify mod "mul32" [] true (llvm_ffi_setup {{ mul32 }}) z3;
-llvm_verify mod "div64" [] true (llvm_ffi_setup {{ div64 }}) z3;
+llvm_ffi_verify mod {{ add8 }} [] true z3;
+llvm_ffi_verify mod {{ sub16 }} [] true z3;
+llvm_ffi_verify mod {{ mul32 }} [] true z3;
+llvm_ffi_verify mod {{ div64 }} [] true z3;
 
-llvm_verify mod "extendInput" [] true (llvm_ffi_setup {{ extendInput }}) z3;
-llvm_verify mod "maskOutput" [] true (llvm_ffi_setup {{ maskOutput }}) z3;
-llvm_verify mod "noBits" [] true (llvm_ffi_setup {{ noBits }}) z3;
+llvm_ffi_verify mod {{ extendInput }} [] true z3;
+llvm_ffi_verify mod {{ maskOutput }} [] true z3;
+llvm_ffi_verify mod {{ noBits }} [] true z3;
 
-not_ov <- llvm_verify mod "not" [] true (llvm_ffi_setup {{ not }}) z3;
+not_ov <- llvm_ffi_verify mod {{ not }} [] true z3;
 
-llvm_verify mod "usesTypeSynonym" [] true (llvm_ffi_setup {{ usesTypeSynonym }}) z3;
+llvm_ffi_verify mod {{ usesTypeSynonym }} [] true z3;
 
-llvm_verify mod "sum10" [] true (llvm_ffi_setup {{ sum10 }}) z3;
-llvm_verify mod "reverse5" [] true (llvm_ffi_setup {{ reverse5 }}) z3;
+llvm_ffi_verify mod {{ sum10 }} [] true z3;
+llvm_ffi_verify mod {{ reverse5 }} [] true z3;
 
-compoundTypes_ov <- llvm_verify mod "compoundTypes" [] true (llvm_ffi_setup {{ compoundTypes }}) z3;
+compoundTypes_ov <- llvm_ffi_verify mod {{ compoundTypes }} [] true z3;
 
 for [0, 12345, 4294967297] (\n ->
-  llvm_verify mod "typeToValue" [] true (llvm_ffi_setup {{ typeToValue`{n} }}) z3);
+  llvm_ffi_verify mod {{ typeToValue`{n} }} [] true z3);
 for [0, 1, 5, 42, 100] (\n ->
-  llvm_verify mod "sumPoly" [] true (llvm_ffi_setup {{ sumPoly`{n} }}) z3);
+  llvm_ffi_verify mod {{ sumPoly`{n} }} [] true z3);
 for [1, 3, 72] (\n ->
-  llvm_verify mod "inits" [] true (llvm_ffi_setup {{ inits`{n} }}) z3);
+  llvm_ffi_verify mod {{ inits`{n} }} [] true z3);
 let dims = [1, 2, 3];
 for dims (\n ->
   for dims (\m ->
     for dims (\p ->
-      llvm_verify mod "zipMul3" [] true (llvm_ffi_setup {{ zipMul3`{n, m, p} }}) z3)));
+      llvm_ffi_verify mod {{ zipMul3`{n, m, p} }} [] true z3)));
 
 for dims (\a ->
   for dims (\b ->
     for dims (\c ->
       for dims (\d ->
-        llvm_verify mod "reshape" [] true (llvm_ffi_setup {{ reshape`{a, b, c, d} }}) z3))));
+        llvm_ffi_verify mod {{ reshape`{a, b, c, d} }} [] true z3))));
 
 let same_setup = llvm_ffi_setup {{ same }};
 llvm_verify mod "same" [] true same_setup z3;
 llvm_verify mod "same" [compoundTypes_ov] true same_setup z3;
+
 let notnot_setup = llvm_ffi_setup {{ notnot }};
 llvm_verify mod "notnot" [] true notnot_setup z3;
 llvm_verify mod "notnot" [not_ov] true notnot_setup z3;
diff --git a/intTests/test_ffi_verify_salsa/salsa.saw b/intTests/test_ffi_verify_salsa/salsa.saw
@@ -2,9 +2,7 @@ enable_experimental;
 
 import "salsa.cry";
 
-let cipher_setup (a : Int) (w : Int) = llvm_ffi_setup {{ cipher`{a, w} }};
-
 m <- llvm_load_module "salsa.bc";
 for [1, 2] (\a ->
   for [1, 2, 63, 64, 65] (\w ->
-    llvm_verify m "cipher" [] false (cipher_setup a w) z3));
+    llvm_ffi_verify m {{ cipher`{a, w} }} [] false z3));