Deprecate llvm_struct.

Change references to either llvm_alias (which has the same type and does
the same thing) or llvm_struct_type (which is sometimes what people
referring to llvm_struct are actually trying to do).

Alas, the manual was wrong and cited llvm_struct when it wanted
llvm_struct_type...

CHANGES.md

@@ -9,6 +9,13 @@
 * Add `mir_equal` and `jvm_equal` commands, which mirror the `llvm_equal`
   command for the MIR and JVM backends, respectively.
 
+## Deprecations
+
+* `llvm_struct` has been marked deprecated.
+It is the same as `llvm_alias` and you should use this instead.
+(If you were looking for a function to create a struct type from its
+contents, that's `llvm_struct_type`.)
+
 ## Bug fixes
 
 * Function types in records no longer require gratuitous parentheses.

doc/manual/manual.md

@@ -2272,7 +2272,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:
 
@@ -2382,7 +2382,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 |};