Merge pull request #1088 from GaloisInc/T1085

Add llvm_struct_type, llvm_packed_struct_type, and llvm_alias

CHANGES.md

@@ -15,6 +15,15 @@ When the path to Java is known, SAW can automatically add system-related
 JAR files to the JAR path, which eliminates the need to manually specify
 these files with `-j`.
 
+SAWScript includes two new functions, `llvm_struct_type` and
+`llvm_packed_struct_type`, for constructing an LLVM struct type from a list
+of other LLVM types. This is not to be confused with the existing `llvm_struct`
+function, which takes a string as an argument and returns the corresponding
+alias type (which is often, but not necessarily, defined as a struct type).
+To avoid confusion, a new `llvm_alias` function has been introduced, and
+`llvm_struct` is now a synonym for `llvm_alias`. The `llvm_struct` function
+continues to be available for now.
+
 # Version 0.7
 
 ## New Features

doc/manual/manual.md

@@ -1924,10 +1924,12 @@ commands.
 LLVM types are built with this set of functions:
 
 * `llvm_int : Int -> LLVMType`
+* `llvm_alias : String -> LLVMType`
 * `llvm_array : Int -> LLVMType -> LLVMType`
-* `llvm_struct : String -> LLVMType`
 * `llvm_float : LLVMType`
 * `llvm_double : LLVMType`
+* `llvm_packed_struct : [LLVMType] -> LLVMType`
+* `llvm_struct : [LLVMType] -> LLVMType`
 
 Java types are built up using the following functions:
 
@@ -2441,10 +2443,10 @@ let dotprod_spec n = do {
     let nt = llvm_term {{ `n : [32] }};
     (xs, xsp) <- ptr_to_fresh "xs" (llvm_array n (llvm_int 32));
     (ys, ysp) <- ptr_to_fresh "ys" (llvm_array n (llvm_int 32));
-    let xval = llvm_struct [ xsp, nt ];
-    let yval = llvm_struct [ ysp, nt ];
-    xp <- alloc_init (llvm_struct "struct.vec_t") xval;
-    yp <- alloc_init (llvm_struct "struct.vec_t") yval;
+    let xval = llvm_alias [ xsp, nt ];
+    let yval = llvm_alias [ ysp, nt ];
+    xp <- alloc_init (llvm_alias "struct.vec_t") xval;
+    yp <- alloc_init (llvm_alias "struct.vec_t") yval;
     llvm_execute_func [xp, yp];
     llvm_return (llvm_term {{ dotprod xs ys }});
 };

examples/llvm/dotprod_struct.saw

@@ -18,8 +18,8 @@ let dotprod_spec n = do {
     (ys, ysp) <- ptr_to_fresh "ys" (llvm_array n (llvm_int 32));
     let xval = llvm_struct_value [ xsp, nt ];
     let yval = llvm_struct_value [ ysp, nt ];
-    xp <- alloc_init (llvm_struct "struct.vec_t") xval;
-    yp <- alloc_init (llvm_struct "struct.vec_t") yval;
+    xp <- alloc_init (llvm_alias "struct.vec_t") xval;
+    yp <- alloc_init (llvm_alias "struct.vec_t") yval;
     llvm_execute_func [xp, yp];
     llvm_return (llvm_term {{ dotprod xs ys }});
 };

examples/llvm/iterative_average/test.saw

@@ -16,7 +16,7 @@ let ptr_to_fresh n ty = do {
 // Verify 'init'.
 
 let init_spec = do {
-  (s, sp) <- ptr_to_fresh "st" (llvm_struct "struct.state");
+  (s, sp) <- ptr_to_fresh "st" (llvm_alias "struct.state");
 
   llvm_execute_func [sp];
 
@@ -32,7 +32,7 @@ print "";
 // Verify 'update'.
 
 let update_spec xs_len = do {
-  (st0, stp) <- ptr_to_fresh "st" (llvm_struct "struct.state");
+  (st0, stp) <- ptr_to_fresh "st" (llvm_alias "struct.state");
   (xs0, xsp) <- ptr_to_fresh "xs" (llvm_array xs_len (llvm_int 32));
 
   llvm_execute_func [stp, xsp, llvm_term {{ `xs_len : [32] }}];
@@ -54,7 +54,7 @@ print "";
 // Verify 'digest'.
 
 let digest_spec = do {
-  (st0, stp) <- ptr_to_fresh "st" (llvm_struct "struct.state");
+  (st0, stp) <- ptr_to_fresh "st" (llvm_alias "struct.state");
   avgp <- llvm_alloc (llvm_int 32);
 
   // Avoid division by zero

examples/llvm/nested-full.saw

@@ -10,7 +10,7 @@ let f_spec = do {
     x <- llvm_fresh_var "x" (llvm_int 32);
     z <- llvm_fresh_var "z" (llvm_int 32);
     let s = (llvm_term {{ (x, (a, b), z) }});
-    p <- alloc_init (llvm_struct "struct.t") s;
+    p <- alloc_init (llvm_alias "struct.t") s;
     llvm_execute_func [p];
     llvm_return (llvm_term {{ b }});
 };

examples/llvm/nested.saw

@@ -1,5 +1,5 @@
 let f_spec = do {
-    tp <- llvm_alloc (llvm_struct "struct.t");
+    tp <- llvm_alloc (llvm_alias "struct.t");
     b <- llvm_fresh_var "b" (llvm_int 32);
 
     // The following will work if nested.bc is compiled with debug info

examples/llvm/ptrcheck.saw

@@ -13,7 +13,7 @@ let ptr_to_fresh n ty = do {
 };
 
 llvm_verify m "f" [] false do {
-    (s, sp) <- ptr_to_fresh "s" (llvm_struct "struct.s");
+    (s, sp) <- ptr_to_fresh "s" (llvm_alias "struct.s");
     llvm_execute_func [sp];
     llvm_return (llvm_term {{ 0 : [32] }});
 } abc;

examples/llvm/struct.saw

@@ -12,22 +12,22 @@ let ptr_to_fresh n ty = do {
 
 let set_spec = do {
     (x, px) <- ptr_to_fresh "x" (llvm_array 2 (llvm_int 32));
-    po <- alloc_init (llvm_struct "struct.s") (llvm_struct_value [px]);
+    po <- alloc_init (llvm_alias "struct.s") (llvm_struct_value [px]);
     llvm_execute_func [po];
     llvm_points_to po (llvm_struct_value [px]);
     llvm_points_to px (llvm_term {{ [0, 0] : [2][32] }});
 };
 
 let add_spec = do {
     (x, px) <- ptr_to_fresh "x" (llvm_array 2 (llvm_int 32));
-    po <- alloc_init (llvm_struct "struct.s") (llvm_struct_value [px]);
+    po <- alloc_init (llvm_alias "struct.s") (llvm_struct_value [px]);
     llvm_execute_func [po];
     llvm_return (llvm_term {{ x@0 + x@1 }});
 };
 
 let id_spec = do {
     (x, px) <- ptr_to_fresh "x" (llvm_array 2 (llvm_int 32));
-    po <- alloc_init (llvm_struct "struct.s") (llvm_struct_value [px]);
+    po <- alloc_init (llvm_alias "struct.s") (llvm_struct_value [px]);
     llvm_execute_func [po];
     llvm_return po;
 };

examples/llvm/union/test.saw

@@ -18,7 +18,7 @@ let ptr_to_fresh n ty = do {
 // The argument 'INC' specifies which 'alg' enum to test.
 let inc_spec INC = do {
 
-  stp <- llvm_alloc (llvm_struct "struct.st");
+  stp <- llvm_alloc (llvm_alias "struct.st");
 
   // The union is represented by the largest element type,
   // i.e. 'inc_2_st'. The inner '.0' dereferences the union itself.

examples/partial-spec/partial-spec.saw

@@ -1,5 +1,5 @@
 let inc_spec : CrucibleSetup () = do {
-  m <- llvm_alloc (llvm_struct "struct.my_struct");
+  m <- llvm_alloc (llvm_alias "struct.my_struct");
   counter <- llvm_fresh_var "counter" (llvm_int 32);
   llvm_points_to (llvm_field m "counter") (llvm_term counter);
   llvm_execute_func [m];

examples/salsa20/djb/salsa20.saw

@@ -179,7 +179,7 @@ let {{
  */
 let ECRYPT_keysetup_setup (kBytes: Int) : CrucibleSetup () = do {
     x_input <- llvm_fresh_var "x->input" (llvm_array 16 u32); let x = {{ {input = x_input} }};
-    p_x <- alloc_init (llvm_struct "struct.ECRYPT_ctx") (llvm_struct_value [ llvm_term x_input ]);
+    p_x <- alloc_init (llvm_alias "struct.ECRYPT_ctx") (llvm_struct_value [ llvm_term x_input ]);
     (k, p_k) <- ptr_to_fresh "k" (llvm_array kBytes u8);
     let kbits = {{ (`kBytes * 8):u32 }}; let ct_kbits = llvm_term kbits;
     let ivbits = {{ 0:u32 }}; let ct_ivbits = llvm_term ivbits; // ignored (ECRYPT test suite compatibility)
@@ -213,7 +213,7 @@ let {{
 /** method specification for ECRYPT_ivsetup, which initializes the IV and counter component of a "context" for encryption in a manner compatible with the ECRYPT validation framework */
 let ECRYPT_ivsetup_setup : CrucibleSetup () = do {
     x_input <- llvm_fresh_var "x->input" (llvm_array 16 u32); let x = {{ {input = x_input} }};
-    p_x <- alloc_init (llvm_struct "struct.ECRYPT_ctx") (llvm_struct [ llvm_term x_input ]);
+    p_x <- alloc_init (llvm_alias "struct.ECRYPT_ctx") (llvm_alias [ llvm_term x_input ]);
     (iv, p_iv) <- ptr_to_fresh "iv" (llvm_array 8 u8);
 
     llvm_execute_func [p_x, p_iv];
@@ -254,7 +254,7 @@ let {{
 /** method specification of ECRYPT_encrypt_bytes */
 let ECRYPT_encrypt_bytes_setup (bytes: Int) : CrucibleSetup () = do {
     x_input <- llvm_fresh_var "x->input" (llvm_array 16 u32); let x = {{ {input = x_input} }};
-    p_x <- alloc_init (llvm_struct "struct.ECRYPT_ctx") (llvm_struct_value [ llvm_term x_input ]);
+    p_x <- alloc_init (llvm_alias "struct.ECRYPT_ctx") (llvm_struct_value [ llvm_term x_input ]);
     (m, p_m) <- ptr_to_fresh "m" (llvm_array bytes u8);
     p_c <- llvm_alloc (llvm_array bytes u8);
     let {{ bytes = `bytes:u32 }};
@@ -324,7 +324,7 @@ let ECRYPT_encrypt_bytes_setup' (bytes: Int) (a: Int) : CrucibleSetup () = do {
                 n = (U8TO32_LITTLE v) # (zero:[2][32])
                 [k0, k1] = (split ((U8TO32_LITTLE k) # zero)):[2][4][32] }};
     // x_input <- llvm_fresh_var "x->input" (llvm_array 16 u32);
-    p_x <- alloc_init (llvm_struct "struct.ECRYPT_ctx") (llvm_struct_value [ llvm_term x_input ]);
+    p_x <- alloc_init (llvm_alias "struct.ECRYPT_ctx") (llvm_struct_value [ llvm_term x_input ]);
 
     (m, p_m) <- ptr_to_fresh "m" (llvm_array bytes u8);
     p_c <- llvm_alloc (llvm_array bytes u8);

intTests/test0028/test.saw

@@ -1,7 +1,17 @@
 /** f clears the 2x4 array of 32-bit unsigned ints in the referenced struct */
     let f_spec : CrucibleSetup() = do {
         i <- llvm_fresh_var "w.i" (llvm_array 2 (llvm_array 4 (llvm_int 32)));
-        pw <- llvm_alloc (llvm_struct "struct.BI");
+        pw <- llvm_alloc (llvm_alias "struct.BI");
+        llvm_points_to pw (llvm_struct_value [llvm_term i]);
+
+        llvm_execute_func [pw];
+        llvm_points_to pw (llvm_struct_value [llvm_term {{ zero:[2][4][32] }} ]);
+    };
+
+    // A variant of f_spec that uses llvm_struct_type instead of llvm_alias.
+    let f_spec2 : CrucibleSetup() = do {
+        i <- llvm_fresh_var "w.i" (llvm_array 2 (llvm_array 4 (llvm_int 32)));
+        pw <- llvm_alloc (llvm_struct_type [llvm_array 2 (llvm_array 4 (llvm_int 32))]);
         llvm_points_to pw (llvm_struct_value [llvm_term i]);
 
         llvm_execute_func [pw];
@@ -12,6 +22,7 @@
         structTest <- llvm_load_module "test.bc";
 
         f_result <- llvm_verify structTest "f" [] false f_spec z3;
+        f_result2 <- llvm_verify structTest "f" [] false f_spec2 z3;
 
         print "Done!";
-    };
+    };

intTests/test0031_unit_test/test.saw

@@ -2,7 +2,7 @@
 let setup = do {
   x <- llvm_fresh_var "x" (llvm_int 32);
 
-  p_a <- llvm_alloc (llvm_struct "struct.a_t");
+  p_a <- llvm_alloc (llvm_alias "struct.a_t");
   llvm_points_to p_a ( llvm_term {{ x }} );
 
   llvm_execute_func [ p_a ];

intTests/test0038_rust/test.saw

@@ -8,7 +8,7 @@ let f_spec : CrucibleSetup() = do {
     //     %BI = type { [0 x i32], [2 x [4 x i32]], [0 x i32] }
     //
     i <- llvm_fresh_var "w.i" (llvm_array 2 (llvm_array 4 (llvm_int 32)));
-    pw <- llvm_alloc (llvm_struct "BI");
+    pw <- llvm_alloc (llvm_alias "BI");
     llvm_points_to pw
       (llvm_struct_value [ llvm_term {{ zero:[0][32] }}
                          , llvm_term i
@@ -32,4 +32,4 @@ let main : TopLevel () = do {
     f_result <- llvm_verify structTest "f" [] false f_spec z3;
 
     print "Done!";
-};
+};

intTests/test0051_compositional_extract_2/test.saw

@@ -10,19 +10,19 @@ let ptr_to_fresh nm ty = do {
 };
 
 let add_spec = do {
-  r_p <- llvm_alloc (llvm_struct "struct.uint128_t");
-  (_, a_p) <- ptr_to_fresh "a" (llvm_struct "struct.uint128_t");
-  (_, b_p) <- ptr_to_fresh "b" (llvm_struct "struct.uint128_t");
+  r_p <- llvm_alloc (llvm_alias "struct.uint128_t");
+  (_, a_p) <- ptr_to_fresh "a" (llvm_alias "struct.uint128_t");
+  (_, b_p) <- ptr_to_fresh "b" (llvm_alias "struct.uint128_t");
   llvm_execute_func [r_p, a_p, b_p];
-  r <- llvm_fresh_var "r" (llvm_struct "struct.uint128_t");
+  r <- llvm_fresh_var "r" (llvm_alias "struct.uint128_t");
   llvm_points_to r_p (llvm_term r);
 };
 
 let sum_spec n = do {
-  s_p <- llvm_alloc (llvm_struct "struct.uint128_t");
-  (_, a_p) <- ptr_to_fresh "a" (llvm_array n (llvm_struct "struct.uint128_t"));
+  s_p <- llvm_alloc (llvm_alias "struct.uint128_t");
+  (_, a_p) <- ptr_to_fresh "a" (llvm_array n (llvm_alias "struct.uint128_t"));
   llvm_execute_func [s_p, a_p, (llvm_term {{ `n:[64] }})];
-  s <- llvm_fresh_var "s" (llvm_struct "struct.uint128_t");
+  s <- llvm_fresh_var "s" (llvm_alias "struct.uint128_t");
   llvm_points_to s_p (llvm_term s);
 };
 

intTests/test0060/test.saw

@@ -45,7 +45,7 @@ llvm_verify m "array_swap" [] false array_swap_spec z3;
 let struct_swap_spec = do {
     x <- llvm_fresh_var "x" (llvm_int 32);
     y <- llvm_fresh_var "y" (llvm_int 32);
-    s <- llvm_alloc (llvm_struct "struct.foo");
+    s <- llvm_alloc (llvm_alias "struct.foo");
     llvm_points_to s (llvm_packed_struct_value [llvm_term x, llvm_term y]);
 
     llvm_execute_func [s];
@@ -54,4 +54,18 @@ let struct_swap_spec = do {
     llvm_points_to (llvm_field s "y") (llvm_term x);
 };
 
+// A variant of struct_swap_spec that uses llvm_struct_type instead of llvm_alias.
+let struct_swap_spec2 = do {
+    x <- llvm_fresh_var "x" (llvm_int 32);
+    y <- llvm_fresh_var "y" (llvm_int 32);
+    s <- llvm_alloc (llvm_packed_struct_type [llvm_int 32, llvm_int 32]);
+    llvm_points_to s (llvm_packed_struct_value [llvm_term x, llvm_term y]);
+
+    llvm_execute_func [s];
+
+    llvm_points_to (llvm_elem s 0) (llvm_term y);
+    llvm_points_to (llvm_elem s 1) (llvm_term x);
+};
+
 llvm_verify m "struct_swap" [] false struct_swap_spec z3;
+llvm_verify m "struct_swap" [] false struct_swap_spec2 z3;

intTests/test0065_match_llvm_elem/test.saw

@@ -21,7 +21,7 @@ let g_false_spec = do {
 };
 
 let h_spec = do {
-  s_p <- llvm_alloc (llvm_struct "struct.s");
+  s_p <- llvm_alloc (llvm_alias "struct.s");
   llvm_execute_func [(llvm_field s_p "y"), s_p];
 };
 

intTests/test_llvm_sizeof/test.saw

@@ -9,20 +9,20 @@ let s1 = llvm_sizeof bc1 (llvm_int 8);
 let s2 = llvm_sizeof bc1 (llvm_int 16);
 let s3 = llvm_sizeof bc1 (llvm_int 32);
 let s4 = llvm_sizeof bc1 (llvm_int 64);
-let s5 = llvm_sizeof bc1 (llvm_struct "struct.foo");
-let s6 = llvm_sizeof bc1 (llvm_struct "struct.bar");
-let s7 = llvm_sizeof bc1 (llvm_array 2 (llvm_struct "struct.foo"));
-let s8 = llvm_sizeof bc2 (llvm_struct "struct.baz");
-let s9 = llvm_sizeof bc2 (llvm_array 8 (llvm_struct "struct.baz"));
+let s5 = llvm_sizeof bc1 (llvm_alias "struct.foo");
+let s6 = llvm_sizeof bc1 (llvm_alias "struct.bar");
+let s7 = llvm_sizeof bc1 (llvm_array 2 (llvm_alias "struct.foo"));
+let s8 = llvm_sizeof bc2 (llvm_alias "struct.baz");
+let s9 = llvm_sizeof bc2 (llvm_array 8 (llvm_alias "struct.baz"));
 let s0 = llvm_sizeof bc2 (llvm_type "void*");
 
 // This is a workaround to delay evaluation of a pure function
 // so that `fails` can catch any errors raised.
 let apply f x = do { () <- return (); return (f x); };
 
 fails (apply (llvm_sizeof bc1) (llvm_type "void"));
-fails (apply (llvm_sizeof bc1) (llvm_struct "baz"));
-fails (apply (llvm_sizeof bc2) (llvm_struct "foo"));
+fails (apply (llvm_sizeof bc1) (llvm_alias "baz"));
+fails (apply (llvm_sizeof bc2) (llvm_alias "foo"));
 
 prove_print z3 {{
   `s1 == (1 : Integer) /\

intTests/test_llvm_tuple/test.saw

@@ -15,7 +15,7 @@ let {{
 swap_ov <-
   llvm_verify bc "swap" [] false
     do {
-      let t = llvm_struct "struct.triple";
+      let t = llvm_alias "struct.triple";
       p <- llvm_alloc t;
       x <- llvm_fresh_var "x" t;
       llvm_points_to p (llvm_term x);

intTests/test_profiling/dotprod_struct.saw

@@ -18,8 +18,8 @@ let dotprod_spec n = do {
     (ys, ysp) <- ptr_to_fresh "ys" (llvm_array n (llvm_int 32));
     let xval = llvm_struct_value [ xsp, nt ];
     let yval = llvm_struct_value [ ysp, nt ];
-    xp <- alloc_init (llvm_struct "struct.vec_t") xval;
-    yp <- alloc_init (llvm_struct "struct.vec_t") yval;
+    xp <- alloc_init (llvm_alias "struct.vec_t") xval;
+    yp <- alloc_init (llvm_alias "struct.vec_t") yval;
     llvm_execute_func [xp, yp];
     llvm_return (llvm_term {{ dotprod xs ys }});
 };