Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Prepare to deprecate llvm_struct #2193

Merged
merged 1 commit into from
Jan 22, 2025
Merged

Prepare to deprecate llvm_struct #2193

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions doc/manual/manual.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:

Expand Down Expand Up @@ -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`.
Expand Down
18 changes: 9 additions & 9 deletions exercises/functional-correctness/point/exercise.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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];

Expand All @@ -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;
};

Expand All @@ -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;
};

Expand Down
4 changes: 2 additions & 2 deletions exercises/functional-correctness/point/solution.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]);
Expand All @@ -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;
};
Expand Down
4 changes: 2 additions & 2 deletions exercises/memory-safety/point/exercise.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
18 changes: 9 additions & 9 deletions exercises/memory-safety/point/solution.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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];

Expand All @@ -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;
};

Expand All @@ -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;
};

Expand All @@ -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;
};

Expand Down
4 changes: 2 additions & 2 deletions exercises/sha512/exercise.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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);
Expand Down
8 changes: 4 additions & 4 deletions exercises/sha512/solution.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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");


////////////////////////////////////////////////////////////////////////////////
Expand Down Expand Up @@ -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`
Expand Down Expand Up @@ -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);
Expand All @@ -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];
Expand Down
22 changes: 11 additions & 11 deletions saw-remote-api/python/tests/saw-in-progress/HMAC/spec/HMAC.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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];
Expand All @@ -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 }};
Expand All @@ -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];
Expand All @@ -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] }};
Expand All @@ -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);
Expand All @@ -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);
Expand All @@ -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];
Expand All @@ -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 |};
Expand Down
22 changes: 11 additions & 11 deletions saw-remote-api/python/tests/saw-in-progress/HMAC/spec/HMAC.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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];
Expand All @@ -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 }};
Expand All @@ -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];
Expand All @@ -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] }};
Expand All @@ -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);
Expand All @@ -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);
Expand All @@ -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];
Expand All @@ -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 |};
Expand Down
Loading