Merge pull request #2193 from GaloisInc/2159-prepare-llvm-struct

Prepare to deprecate llvm_struct

doc/manual/manual.md

@@ -2330,7 +2330,7 @@ LLVM types are built with this set of functions:
 * `llvm_float : LLVMType`
 * `llvm_double : LLVMType`
 * `llvm_packed_struct : [LLVMType] -> LLVMType`
-* `llvm_struct : [LLVMType] -> LLVMType`
+* `llvm_struct_type : [LLVMType] -> LLVMType`
 
 Java types are built up using the following functions:
 
@@ -2440,7 +2440,7 @@ The following LLVM types correspond to Cryptol types:
 * `llvm_array <n> <ty>`: Corresponds to the Cryptol sequence `[<n>][<cty>]`,
   where `<cty>` is the Cryptol type corresponding to `<ty>`.
 * `llvm_int <n>`: Corresponds to the Cryptol word `[<n>]`.
-* `llvm_struct [<ty_1>, ..., <ty_n>]` and `llvm_packed_struct [<ty_1>, ..., <ty_n>]`:
+* `llvm_struct_type [<ty_1>, ..., <ty_n>]` and `llvm_packed_struct [<ty_1>, ..., <ty_n>]`:
   Corresponds to the Cryptol tuple `(<cty_1>, ..., <cty_n>)`, where `<cty_i>`
   is the Cryptol type corresponding to `<ty_i>` for each `i` ranging from `1`
   to `n`.

exercises/functional-correctness/point/exercise.saw

@@ -19,8 +19,8 @@ m <- llvm_load_module "point.bc";
 //     llvm_struct_value [ <field_0>, <field_1>, ... <field_n> ];
 
 let point_eq_spec = do {
-    (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_struct "struct.point");
-    (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_struct "struct.point");
+    (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_alias "struct.point");
+    (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_alias "struct.point");
 
     llvm_execute_func [p1_ptr, p2_ptr];
 
@@ -42,18 +42,18 @@ let point_new_spec = do {
 
     llvm_execute_func [ llvm_term p_x, llvm_term p_y ];
 
-    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point");
+    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_alias "struct.point");
     llvm_return ret_ptr;
 };
 
 point_new_ov <- llvm_verify m "point_new" [] true point_new_spec z3;
 
 let point_copy_spec = do {
-    (p, p_ptr) <- ptr_to_fresh_readonly "p" (llvm_struct "struct.point");
+    (p, p_ptr) <- ptr_to_fresh_readonly "p" (llvm_alias "struct.point");
 
     llvm_execute_func [p_ptr];
 
-    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point");
+    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_alias "struct.point");
     llvm_return ret_ptr;
 };
 
@@ -68,15 +68,15 @@ point_copy_ov <- llvm_verify m "point_copy" [point_new_ov] true point_copy_spec
 
 let point_add_spec = do {
     llvm_alloc_global "ZERO";
-    zero_global <- llvm_fresh_var "zero_global" (llvm_struct "struct.point");
+    zero_global <- llvm_fresh_var "zero_global" (llvm_alias "struct.point");
     llvm_points_to (llvm_global "ZERO") (llvm_term zero_global);
 
-    (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_struct "struct.point");
-    (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_struct "struct.point");
+    (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_alias "struct.point");
+    (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_alias "struct.point");
 
     llvm_execute_func [p1_ptr, p2_ptr];
 
-    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point");
+    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_alias "struct.point");
     llvm_return ret_ptr;
 };
 

exercises/functional-correctness/point/solution.saw

@@ -4,7 +4,7 @@ import "Point.cry";
 m <- llvm_load_module "point.bc";
 
 let fresh_point_readonly name = do {
-    p_ptr <- llvm_alloc_readonly (llvm_struct "struct.point");
+    p_ptr <- llvm_alloc_readonly (llvm_alias "struct.point");
     p_x <- llvm_fresh_var (str_concat name ".x") (llvm_int 32);
     p_y <- llvm_fresh_var (str_concat name ".y") (llvm_int 32);
     llvm_points_to p_ptr (llvm_struct_value [ llvm_term p_x, llvm_term p_y]);
@@ -28,7 +28,7 @@ point_eq_ov <- llvm_verify m "point_eq" [] true
     (w4_unint_z3 []);
 
 let alloc_assign_point p = do {
-    p_ptr <- llvm_alloc (llvm_struct "struct.point");
+    p_ptr <- llvm_alloc (llvm_alias "struct.point");
     llvm_points_to p_ptr (llvm_struct_value [ llvm_term {{ p.x }}, llvm_term {{ p.y }}]);
     return p_ptr;
 };

exercises/memory-safety/point/exercise.saw

@@ -11,8 +11,8 @@ include "../../common/helpers.saw";
 // Write memory safety specs and proofs for point_eq, point_new, and point_copy.
 // Use the override your point_new proof returns in your point_copy proof.
 
-// Remember: You can declare struct types with:
-//    llvm_struct "struct.<name>"
+// Remember: You can refer to struct types with:
+//    llvm_alias "struct.<name>"
 
 ////////////////////////////////////////////////////////////////////////////////
 // Part 2: Global Variables

exercises/memory-safety/point/solution.saw

@@ -3,8 +3,8 @@ include "../../common/helpers.saw";
 m <- llvm_load_module "point.bc";
 
 let point_eq_spec = do {
-    (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_struct "struct.point");
-    (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_struct "struct.point");
+    (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_alias "struct.point");
+    (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_alias "struct.point");
 
     llvm_execute_func [p1_ptr, p2_ptr];
 
@@ -22,7 +22,7 @@ let point_new_spec = do {
 
     llvm_execute_func [ llvm_term p_x, llvm_term p_y ];
 
-    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point");
+    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_alias "struct.point");
     llvm_return ret_ptr;
 };
 
@@ -31,11 +31,11 @@ point_new_ov <- llvm_verify m "point_new" [] true
     (w4_unint_z3 []);
 
 let point_copy_spec = do {
-    (p, p_ptr) <- ptr_to_fresh_readonly "p" (llvm_struct "struct.point");
+    (p, p_ptr) <- ptr_to_fresh_readonly "p" (llvm_alias "struct.point");
 
     llvm_execute_func [p_ptr];
 
-    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point");
+    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_alias "struct.point");
     llvm_return ret_ptr;
 };
 
@@ -45,15 +45,15 @@ point_copy_ov <- llvm_verify m "point_copy" [point_new_ov] true
 
 let point_add_spec = do {
     llvm_alloc_global "ZERO";
-    zero_global <- llvm_fresh_var "zero_global" (llvm_struct "struct.point");
+    zero_global <- llvm_fresh_var "zero_global" (llvm_alias "struct.point");
     llvm_points_to (llvm_global "ZERO") (llvm_term zero_global);
 
-    (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_struct "struct.point");
-    (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_struct "struct.point");
+    (p1, p1_ptr) <- ptr_to_fresh_readonly "p1" (llvm_alias "struct.point");
+    (p2, p2_ptr) <- ptr_to_fresh_readonly "p2" (llvm_alias "struct.point");
 
     llvm_execute_func [p1_ptr, p2_ptr];
 
-    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_struct "struct.point");
+    (ret, ret_ptr) <- ptr_to_fresh "ret" (llvm_alias "struct.point");
     llvm_return ret_ptr;
 };
 

exercises/sha512/exercise.saw

@@ -29,7 +29,7 @@ let SHA512_CBLOCK = 128;
 let SHA512_DIGEST_LENGTH = 64;
 
 // Size of the SHA512 context struct
-let SHA512_CTX_SIZE = llvm_sizeof m (llvm_struct "struct.sha512_state_st");
+let SHA512_CTX_SIZE = llvm_sizeof m (llvm_alias "struct.sha512_state_st");
 
 ////////////////////////////////////////////////////////////////////////////////
 // BEGIN Part 1
@@ -98,7 +98,7 @@ let pointer_to_fresh_sha512_state_st name n = do {
   let state = {{ { h = h, block = (block # zero) : [SHA512_CBLOCK][8], n = `n : [32], sz = sz } }};
 
   // `ptr` is a pointer to a `sha512_state_st` struct
-  ptr <- llvm_alloc (llvm_struct "struct.sha512_state_st");
+  ptr <- llvm_alloc (llvm_alias "struct.sha512_state_st");
   points_to_sha512_state_st_common ptr (h, sz, block, {{ `n : [32]}}) n;
 
   return (state, ptr);

exercises/sha512/solution.saw

@@ -23,7 +23,7 @@ let SHA512_CBLOCK = 128;
 let SHA512_DIGEST_LENGTH = 64;
 
 // Size of the SHA512 context struct
-let SHA512_CTX_SIZE = llvm_sizeof m (llvm_struct "struct.sha512_state_st");
+let SHA512_CTX_SIZE = llvm_sizeof m (llvm_alias "struct.sha512_state_st");
 
 
 ////////////////////////////////////////////////////////////////////////////////
@@ -54,7 +54,7 @@ let SHA512_CTX_SIZE = llvm_sizeof m (llvm_struct "struct.sha512_state_st");
  * through the function, subject to precondition constraints.  For example,
  * if a precondition states that a variable `sha_ptr` is a pointer to an
  * `sha512_state_st` struct:
- *     ctx_ptr <- llvm_alloc (llvm_struct "struct.sha512_state_st");
+ *     ctx_ptr <- llvm_alloc (llvm_alias "struct.sha512_state_st");
  * And the function call description takes `sha_ptr` as an input:
  *     llvm_execute_func [sha_ptr];
  * Then SAW will reason about the function over all possible `sha512_state_st`
@@ -180,7 +180,7 @@ let pointer_to_fresh_sha512_state_st name n = do {
   let state = {{ { h = h, block = (block # zero) : [SHA512_CBLOCK][8], n = `n : [32], sz = sz } }};
 
   // `ptr` is a pointer to a `sha512_state_st` struct
-  ptr <- llvm_alloc (llvm_struct "struct.sha512_state_st");
+  ptr <- llvm_alloc (llvm_alias "struct.sha512_state_st");
   points_to_sha512_state_st_common ptr (h, sz, block, {{ `n : [32]}}) n;
 
   return (state, ptr);
@@ -200,7 +200,7 @@ let points_to_sha512_state_st ptr state num = do {
  */
 let SHA512_Init_spec = do {
   // Precondition: `sha_ptr` is a pointer to a `sha512_state_st` struct
-  sha_ptr <- llvm_alloc (llvm_struct "struct.sha512_state_st");
+  sha_ptr <- llvm_alloc (llvm_alias "struct.sha512_state_st");
 
   // Call function with `sha_ptr`
   llvm_execute_func [sha_ptr];

saw-remote-api/python/tests/saw-in-progress/HMAC/spec/HMAC.py

@@ -54,7 +54,7 @@ def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None, *, re
 #     is_ready_for_input0 <- crucible_fresh_var "is_ready_for_input" (llvm_int 8);
 #     currently_in_hash0 <- crucible_fresh_var "currently_in_hash" (llvm_int 64);
 #     md_len0 <- crucible_fresh_var "md_len" (llvm_int 32);
-#     (_, pimpl) <- ptr_to_fresh_readonly "impl" (llvm_struct "struct.s2n_hash");
+#     (_, pimpl) <- ptr_to_fresh_readonly "impl" (llvm_alias "struct.s2n_hash");
 #     crucible_points_to pstate
 #       (crucible_struct
 #         [ pimpl
@@ -122,7 +122,7 @@ def setup_hash_state(c : Contract, pstate : SetupVal) -> Tuple[Any, FreshVar]:
 #     alg <- crucible_fresh_var "alg" (llvm_int 32);
 #     is_ready_for_input <- crucible_fresh_var "is_ready_for_input" (llvm_int 8);
 #     currently_in_hash <- crucible_fresh_var "currently_in_hash" (llvm_int 64);
-#     (_, pimpl) <- ptr_to_fresh_readonly "impl" (llvm_struct "struct.s2n_hash");
+#     (_, pimpl) <- ptr_to_fresh_readonly "impl" (llvm_alias "struct.s2n_hash");
 
 #     crucible_points_to pstate
 #       (crucible_struct
@@ -146,7 +146,7 @@ def setup_hash_state(c : Contract, pstate : SetupVal) -> Tuple[Any, FreshVar]:
 # };
 
 # let hash_init_spec = do {
-#     pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+#     pstate <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
 #     (st0, _) <- setup_hash_state pstate;
 #     alg <- crucible_fresh_var "alg" (llvm_int 32);
 #     crucible_execute_func [pstate, crucible_term alg];
@@ -158,7 +158,7 @@ def setup_hash_state(c : Contract, pstate : SetupVal) -> Tuple[Any, FreshVar]:
 # };
 
 # let hash_reset_spec = do {
-#     pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+#     pstate <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
 #     (st0, _) <- setup_hash_state pstate;
 #     crucible_execute_func [pstate];
 #     let st1 = {{ hash_init_c_state st0 }};
@@ -167,8 +167,8 @@ def setup_hash_state(c : Contract, pstate : SetupVal) -> Tuple[Any, FreshVar]:
 # };
 
 # let hash_copy_spec = do {
-#     pstate1 <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
-#     pstate2 <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+#     pstate1 <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
+#     pstate2 <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
 #     (st1, _) <- setup_hash_state pstate1;
 #     (st2, _) <- setup_hash_state pstate2;
 #     crucible_execute_func [pstate1, pstate2];
@@ -178,7 +178,7 @@ def setup_hash_state(c : Contract, pstate : SetupVal) -> Tuple[Any, FreshVar]:
 # };
 
 # let hash_update_spec msg_size = do {
-#     pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+#     pstate <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
 #     (msg, pmsg) <- ptr_to_fresh_readonly "msg" (llvm_array msg_size (llvm_int 8));
 #     (st0, _) <- setup_hash_state pstate;
 #     let size = crucible_term {{ `msg_size : [32] }};
@@ -189,7 +189,7 @@ def setup_hash_state(c : Contract, pstate : SetupVal) -> Tuple[Any, FreshVar]:
 # };
 
 # let hash_update_unbounded_spec = do {
-#     pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+#     pstate <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
 #     (st0, _) <- setup_hash_state pstate;
 
 #     size <- crucible_fresh_var "size" (llvm_int 32);
@@ -206,7 +206,7 @@ def setup_hash_state(c : Contract, pstate : SetupVal) -> Tuple[Any, FreshVar]:
 # };
 
 # let hash_digest_spec digest_size = do {
-#     pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+#     pstate <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
 #     (dgst, pdgst) <- ptr_to_fresh "out" (llvm_array digest_size (llvm_int 8));
 #     (st0, _) <- setup_hash_state pstate;
 #     size <- crucible_fresh_var "size" (llvm_int 32);
@@ -218,7 +218,7 @@ def setup_hash_state(c : Contract, pstate : SetupVal) -> Tuple[Any, FreshVar]:
 # };
 
 # let hash_get_currently_in_hash_total_spec = do {
-#     pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+#     pstate <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
 #     pout <- crucible_alloc (llvm_int 64);
 #     (st0, currently_in_hash) <- setup_hash_state pstate;
 #     crucible_execute_func [pstate, pout];
@@ -231,7 +231,7 @@ def setup_hash_state(c : Contract, pstate : SetupVal) -> Tuple[Any, FreshVar]:
 # // HMAC.
 
 # let setup_hmac_state alg0 hash_block_size0 block_size0 digest_size0 = do {
-#     pstate <- crucible_alloc (llvm_struct "struct.s2n_hmac_state");
+#     pstate <- crucible_alloc (llvm_alias "struct.s2n_hmac_state");
 #     currently_in_hash_block0 <- crucible_fresh_var "currently_in_hash_block" (llvm_int 32);
 #     xor_pad0 <- crucible_fresh_var "xor_pad" (llvm_array 128 (llvm_int 8));
 #     let digest_size = eval_size {| SHA512_DIGEST_LENGTH |};

saw-remote-api/python/tests/saw-in-progress/HMAC/spec/HMAC.saw

@@ -71,7 +71,7 @@ let setup_hash_state pstate = do {
     is_ready_for_input0 <- crucible_fresh_var "is_ready_for_input" (llvm_int 8);
     currently_in_hash0 <- crucible_fresh_var "currently_in_hash" (llvm_int 64);
     md_len0 <- crucible_fresh_var "md_len" (llvm_int 32);
-    (_, pimpl) <- ptr_to_fresh_readonly "impl" (llvm_struct "struct.s2n_hash");
+    (_, pimpl) <- ptr_to_fresh_readonly "impl" (llvm_alias "struct.s2n_hash");
     crucible_points_to pstate
       (crucible_struct
         [ pimpl
@@ -107,7 +107,7 @@ let update_hash_state pstate st = do {
     alg <- crucible_fresh_var "alg" (llvm_int 32);
     is_ready_for_input <- crucible_fresh_var "is_ready_for_input" (llvm_int 8);
     currently_in_hash <- crucible_fresh_var "currently_in_hash" (llvm_int 64);
-    (_, pimpl) <- ptr_to_fresh_readonly "impl" (llvm_struct "struct.s2n_hash");
+    (_, pimpl) <- ptr_to_fresh_readonly "impl" (llvm_alias "struct.s2n_hash");
 
     crucible_points_to pstate
       (crucible_struct
@@ -131,7 +131,7 @@ let update_hash_state pstate st = do {
 };
 
 let hash_init_spec = do {
-    pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+    pstate <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
     (st0, _) <- setup_hash_state pstate;
     alg <- crucible_fresh_var "alg" (llvm_int 32);
     crucible_execute_func [pstate, crucible_term alg];
@@ -143,7 +143,7 @@ let hash_init_spec = do {
 };
 
 let hash_reset_spec = do {
-    pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+    pstate <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
     (st0, _) <- setup_hash_state pstate;
     crucible_execute_func [pstate];
     let st1 = {{ hash_init_c_state st0 }};
@@ -152,8 +152,8 @@ let hash_reset_spec = do {
 };
 
 let hash_copy_spec = do {
-    pstate1 <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
-    pstate2 <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+    pstate1 <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
+    pstate2 <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
     (st1, _) <- setup_hash_state pstate1;
     (st2, _) <- setup_hash_state pstate2;
     crucible_execute_func [pstate1, pstate2];
@@ -163,7 +163,7 @@ let hash_copy_spec = do {
 };
 
 let hash_update_spec msg_size = do {
-    pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+    pstate <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
     (msg, pmsg) <- ptr_to_fresh_readonly "msg" (llvm_array msg_size (llvm_int 8));
     (st0, _) <- setup_hash_state pstate;
     let size = crucible_term {{ `msg_size : [32] }};
@@ -174,7 +174,7 @@ let hash_update_spec msg_size = do {
 };
 
 let hash_update_unbounded_spec = do {
-    pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+    pstate <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
     (st0, _) <- setup_hash_state pstate;
 
     size <- crucible_fresh_var "size" (llvm_int 32);
@@ -191,7 +191,7 @@ let hash_update_unbounded_spec = do {
 };
 
 let hash_digest_spec digest_size = do {
-    pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+    pstate <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
     (dgst, pdgst) <- ptr_to_fresh "out" (llvm_array digest_size (llvm_int 8));
     (st0, _) <- setup_hash_state pstate;
     size <- crucible_fresh_var "size" (llvm_int 32);
@@ -203,7 +203,7 @@ let hash_digest_spec digest_size = do {
 };
 
 let hash_get_currently_in_hash_total_spec = do {
-    pstate <- crucible_alloc (llvm_struct "struct.s2n_hash_state");
+    pstate <- crucible_alloc (llvm_alias "struct.s2n_hash_state");
     pout <- crucible_alloc (llvm_int 64);
     (st0, currently_in_hash) <- setup_hash_state pstate;
     crucible_execute_func [pstate, pout];
@@ -216,7 +216,7 @@ let hash_get_currently_in_hash_total_spec = do {
 // HMAC.
 
 let setup_hmac_state alg0 hash_block_size0 block_size0 digest_size0 = do {
-    pstate <- crucible_alloc (llvm_struct "struct.s2n_hmac_state");
+    pstate <- crucible_alloc (llvm_alias "struct.s2n_hmac_state");
     currently_in_hash_block0 <- crucible_fresh_var "currently_in_hash_block" (llvm_int 32);
     xor_pad0 <- crucible_fresh_var "xor_pad" (llvm_array 128 (llvm_int 8));
     let digest_size = eval_size {| SHA512_DIGEST_LENGTH |};