From 0603c369253785a897c7f30bafd19b17a53709a4 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 22 Feb 2021 11:00:53 -0500 Subject: [PATCH 1/2] Add llvm_struct_type and llvm_packed_struct_type Fixes #1085. --- CHANGES.md | 4 ++++ doc/manual/manual.md | 2 ++ intTests/test0028/test.saw | 13 ++++++++++++- intTests/test0060/test.saw | 14 ++++++++++++++ src/SAWScript/Interpreter.hs | 12 ++++++++++++ src/SAWScript/LLVMBuiltins.hs | 6 ++++++ 6 files changed, 50 insertions(+), 1 deletion(-) diff --git a/CHANGES.md b/CHANGES.md index b178088eb0..708e6f250d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -15,6 +15,10 @@ 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. + # Version 0.7 ## New Features diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 8aafad491d..e2a964eade 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -1928,6 +1928,8 @@ LLVM types are built with this set of functions: * `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: diff --git a/intTests/test0028/test.saw b/intTests/test0028/test.saw index 461e54aaad..526a82b04a 100644 --- a/intTests/test0028/test.saw +++ b/intTests/test0028/test.saw @@ -8,10 +8,21 @@ 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_struct. + 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]; + llvm_points_to pw (llvm_struct_value [llvm_term {{ zero:[2][4][32] }} ]); + }; + let main : TopLevel () = do { 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!"; - }; \ No newline at end of file + }; diff --git a/intTests/test0060/test.saw b/intTests/test0060/test.saw index 67e4e71902..c198335a14 100644 --- a/intTests/test0060/test.saw +++ b/intTests/test0060/test.saw @@ -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_struct. +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; diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 3c69adb44d..2d20a8ff34 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -2403,6 +2403,12 @@ primitives = Map.fromList Current [ "Legacy alternative name for `llvm_array_value`." ] + , prim "llvm_struct_type" + "[LLVMType] -> LLVMType" + (pureVal llvm_struct_type) + Current + [ "The type of an LLVM struct with elements of the given types." ] + , prim "llvm_struct_value" "[SetupValue] -> SetupValue" (pureVal (CIR.anySetupStruct False)) @@ -2415,6 +2421,12 @@ primitives = Map.fromList Current [ "Legacy alternative name for `llvm_struct_value`." ] + , prim "llvm_packed_struct_type" + "[LLVMType] -> LLVMType" + (pureVal llvm_packed_struct_type) + Current + [ "The type of a packed LLVM struct with elements of the given types." ] + , prim "llvm_packed_struct_value" "[SetupValue] -> SetupValue" (pureVal (CIR.anySetupStruct True)) diff --git a/src/SAWScript/LLVMBuiltins.hs b/src/SAWScript/LLVMBuiltins.hs index 3db73336db..37920e6fdf 100644 --- a/src/SAWScript/LLVMBuiltins.hs +++ b/src/SAWScript/LLVMBuiltins.hs @@ -63,3 +63,9 @@ llvm_array n t = LLVM.Array (fromIntegral n) t llvm_struct :: String -> LLVM.Type llvm_struct n = LLVM.Alias (fromString n) + +llvm_packed_struct_type :: [LLVM.Type] -> LLVM.Type +llvm_packed_struct_type = LLVM.PackedStruct + +llvm_struct_type :: [LLVM.Type] -> LLVM.Type +llvm_struct_type = LLVM.Struct From 785db6ef698e2892283b558329e27982c325d863 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 22 Feb 2021 11:30:14 -0500 Subject: [PATCH 2/2] Introduce llvm_alias, make llvm_struct a synonym for llvm_alias This introduces the `llvm_alias` function and makes `llvm_struct` a synonym for `llvm_alias`. For now, `llvm_struct` continues to be available without a deprecation notice. In the future, we may want to deprecate `llvm_struct` in favor of `llvm_alias`, as having two separate functions named `llvm_struct` and `llvm_struct_type` could invite confusion. See the discussion in #1085. --- CHANGES.md | 7 ++++- doc/manual/manual.md | 10 +++---- examples/llvm/dotprod_struct.saw | 4 +-- examples/llvm/iterative_average/test.saw | 6 ++--- examples/llvm/nested-full.saw | 2 +- examples/llvm/nested.saw | 2 +- examples/llvm/ptrcheck.saw | 2 +- examples/llvm/struct.saw | 6 ++--- examples/llvm/union/test.saw | 2 +- examples/partial-spec/partial-spec.saw | 2 +- examples/salsa20/djb/salsa20.saw | 8 +++--- intTests/test0028/test.saw | 4 +-- intTests/test0031_unit_test/test.saw | 2 +- intTests/test0038_rust/test.saw | 4 +-- .../test0051_compositional_extract_2/test.saw | 14 +++++----- intTests/test0060/test.saw | 4 +-- intTests/test0065_match_llvm_elem/test.saw | 2 +- intTests/test_llvm_sizeof/test.saw | 14 +++++----- intTests/test_llvm_tuple/test.saw | 2 +- intTests/test_profiling/dotprod_struct.saw | 4 +-- .../in-progress/HMAC/spec/HMAC.py | 26 +++++++++---------- .../in-progress/HMAC/spec/HMAC.saw | 22 ++++++++-------- saw-remote-api/test-scripts/llvm_struct.py | 8 +++--- src/SAWScript/Interpreter.hs | 10 +++++-- src/SAWScript/LLVMBuiltins.hs | 4 +-- 25 files changed, 91 insertions(+), 80 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 708e6f250d..c5b6be7017 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -17,7 +17,12 @@ 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. +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 diff --git a/doc/manual/manual.md b/doc/manual/manual.md index e2a964eade..e5c2e64d16 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -1924,8 +1924,8 @@ 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` @@ -2443,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 }}); }; diff --git a/examples/llvm/dotprod_struct.saw b/examples/llvm/dotprod_struct.saw index c84a989e8a..6e49ff0425 100644 --- a/examples/llvm/dotprod_struct.saw +++ b/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 }}); }; diff --git a/examples/llvm/iterative_average/test.saw b/examples/llvm/iterative_average/test.saw index eae3354f0f..1a92fc09c3 100644 --- a/examples/llvm/iterative_average/test.saw +++ b/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 diff --git a/examples/llvm/nested-full.saw b/examples/llvm/nested-full.saw index 0f914ffa77..3a07a2518a 100644 --- a/examples/llvm/nested-full.saw +++ b/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 }}); }; diff --git a/examples/llvm/nested.saw b/examples/llvm/nested.saw index 32bd0961a5..2d74b6a564 100644 --- a/examples/llvm/nested.saw +++ 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 diff --git a/examples/llvm/ptrcheck.saw b/examples/llvm/ptrcheck.saw index 3066915ac9..b82458e306 100644 --- a/examples/llvm/ptrcheck.saw +++ b/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; diff --git a/examples/llvm/struct.saw b/examples/llvm/struct.saw index 67209b3a6d..f2f25e4e45 100644 --- a/examples/llvm/struct.saw +++ b/examples/llvm/struct.saw @@ -12,7 +12,7 @@ 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] }}); @@ -20,14 +20,14 @@ let set_spec = do { 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; }; diff --git a/examples/llvm/union/test.saw b/examples/llvm/union/test.saw index 8b830212f8..df48c7d3b2 100644 --- a/examples/llvm/union/test.saw +++ b/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. diff --git a/examples/partial-spec/partial-spec.saw b/examples/partial-spec/partial-spec.saw index 732557ba4c..1384111fbd 100644 --- a/examples/partial-spec/partial-spec.saw +++ b/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]; diff --git a/examples/salsa20/djb/salsa20.saw b/examples/salsa20/djb/salsa20.saw index c0062f8405..dddcfe4ed8 100644 --- a/examples/salsa20/djb/salsa20.saw +++ b/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); diff --git a/intTests/test0028/test.saw b/intTests/test0028/test.saw index 526a82b04a..955afba93a 100644 --- a/intTests/test0028/test.saw +++ b/intTests/test0028/test.saw @@ -1,14 +1,14 @@ /** 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_struct. + // 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))]); diff --git a/intTests/test0031_unit_test/test.saw b/intTests/test0031_unit_test/test.saw index a5750c49cb..ba68a2e904 100644 --- a/intTests/test0031_unit_test/test.saw +++ b/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 ]; diff --git a/intTests/test0038_rust/test.saw b/intTests/test0038_rust/test.saw index d769daf403..8cf3fe8476 100644 --- a/intTests/test0038_rust/test.saw +++ b/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!"; -}; \ No newline at end of file +}; diff --git a/intTests/test0051_compositional_extract_2/test.saw b/intTests/test0051_compositional_extract_2/test.saw index 8ccf4f3748..6581b85730 100644 --- a/intTests/test0051_compositional_extract_2/test.saw +++ b/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); }; diff --git a/intTests/test0060/test.saw b/intTests/test0060/test.saw index c198335a14..4089b242a9 100644 --- a/intTests/test0060/test.saw +++ b/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,7 +54,7 @@ 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_struct. +// 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); diff --git a/intTests/test0065_match_llvm_elem/test.saw b/intTests/test0065_match_llvm_elem/test.saw index 593db56e27..71c720bf8d 100644 --- a/intTests/test0065_match_llvm_elem/test.saw +++ b/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]; }; diff --git a/intTests/test_llvm_sizeof/test.saw b/intTests/test_llvm_sizeof/test.saw index d55ee7b8ba..6d10ac2cb5 100644 --- a/intTests/test_llvm_sizeof/test.saw +++ b/intTests/test_llvm_sizeof/test.saw @@ -9,11 +9,11 @@ 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 @@ -21,8 +21,8 @@ let s0 = llvm_sizeof bc2 (llvm_type "void*"); 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) /\ diff --git a/intTests/test_llvm_tuple/test.saw b/intTests/test_llvm_tuple/test.saw index 69d616b384..bcfb032678 100644 --- a/intTests/test_llvm_tuple/test.saw +++ b/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); diff --git a/intTests/test_profiling/dotprod_struct.saw b/intTests/test_profiling/dotprod_struct.saw index 4ab41912be..78ad223c1c 100644 --- a/intTests/test_profiling/dotprod_struct.saw +++ b/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 }}); }; diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.py b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.py index d93049516d..f6831605ea 100644 --- a/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.py +++ b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.py @@ -26,7 +26,7 @@ # }; def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None, *, read_only : bool = False) -> Tuple[FreshVar, SetupVal]: """Add to``Contract`` ``c`` an allocation of a pointer of type ``ty`` initialized to an unknown fresh value. - + :returns A fresh variable bound to the pointers initial value and the newly allocated pointer. (The fresh variable will be assigned ``name`` if provided/available.)""" var = c.declare_var(ty, name) @@ -55,7 +55,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 @@ -99,7 +99,7 @@ def setup_hash_state(c : Contract, pstate : SetupVal) -> Tuple[Any, FreshVar]: currently_in_hash0 = c.fresh_var(ty.i64, "currently_in_hash") md_len0 = c.fresh_var(ty.i32, "md_len") (_, pimpl) = ptr_to_fresh(c, ty.alias('struct.s2n_hash'), "impl", read_only=True) - c.points_to(pstate, + c.points_to(pstate, struct( pimpl, alg0, @@ -123,7 +123,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 @@ -147,7 +147,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]; @@ -159,7 +159,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 }}; @@ -168,8 +168,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]; @@ -179,7 +179,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] }}; @@ -190,7 +190,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); @@ -207,7 +207,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); @@ -219,7 +219,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]; @@ -232,7 +232,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 |}; diff --git a/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.saw b/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.saw index 11a22257f9..7cb68c7def 100644 --- a/saw-remote-api/test-scripts/in-progress/HMAC/spec/HMAC.saw +++ b/saw-remote-api/test-scripts/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 |}; diff --git a/saw-remote-api/test-scripts/llvm_struct.py b/saw-remote-api/test-scripts/llvm_struct.py index 2894ebc574..3a4b3a11ef 100644 --- a/saw-remote-api/test-scripts/llvm_struct.py +++ b/saw-remote-api/test-scripts/llvm_struct.py @@ -9,7 +9,7 @@ def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None) -> Tuple[FreshVar, SetupVal]: """Add to``Contract`` ``c`` an allocation of a pointer of type ``ty`` initialized to an unknown fresh value. - + :returns A fresh variable bound to the pointers initial value and the newly allocated pointer. (The fresh variable will be assigned ``name`` if provided/available.)""" var = c.fresh_var(ty, name) @@ -18,7 +18,7 @@ def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None) -> Tu # let set_spec = do { # (x, px) <- ptr_to_fresh "x" (llvm_array 2 (llvm_int 32)); -# po <- alloc_init (llvm_struct "struct.s") (crucible_struct [px]); +# po <- alloc_init (llvm_alias "struct.s") (crucible_struct [px]); # crucible_execute_func [po]; # crucible_points_to po (crucible_struct [px]); # crucible_points_to px (crucible_term {{ [0, 0] : [2][32] }}); @@ -36,7 +36,7 @@ def specification(self): # let add_spec = do { # (x, px) <- ptr_to_fresh "x" (llvm_array 2 (llvm_int 32)); -# po <- alloc_init (llvm_struct "struct.s") (crucible_struct [px]); +# po <- alloc_init (llvm_alias "struct.s") (crucible_struct [px]); # crucible_execute_func [po]; # crucible_return (crucible_term {{ x@0 + x@1 }}); # }; @@ -51,7 +51,7 @@ def specification(self): # let id_spec = do { # (x, px) <- ptr_to_fresh "x" (llvm_array 2 (llvm_int 32)); -# po <- alloc_init (llvm_struct "struct.s") (crucible_struct [px]); +# po <- alloc_init (llvm_alias "struct.s") (crucible_struct [px]); # crucible_execute_func [po]; # crucible_return po; # }; diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 2d20a8ff34..82e3435edf 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1712,10 +1712,16 @@ primitives = Map.fromList , "given type." ] + , prim "llvm_alias" "String -> LLVMType" + (pureVal llvm_alias) + Current + [ "The type of an LLVM alias for the given name. Often times, this is used" + , "to alias a struct type." + ] , prim "llvm_struct" "String -> LLVMType" - (pureVal llvm_struct) + (pureVal llvm_alias) Current - [ "The type of an LLVM struct of the given name." + [ "Legacy alternative name for `llvm_alias`." ] , prim "llvm_load_module" "String -> TopLevel LLVMModule" diff --git a/src/SAWScript/LLVMBuiltins.hs b/src/SAWScript/LLVMBuiltins.hs index 37920e6fdf..abebbf10a6 100644 --- a/src/SAWScript/LLVMBuiltins.hs +++ b/src/SAWScript/LLVMBuiltins.hs @@ -61,8 +61,8 @@ llvm_double = LLVM.PrimType (LLVM.FloatType LLVM.Double) llvm_array :: Int -> LLVM.Type -> LLVM.Type llvm_array n t = LLVM.Array (fromIntegral n) t -llvm_struct :: String -> LLVM.Type -llvm_struct n = LLVM.Alias (fromString n) +llvm_alias :: String -> LLVM.Type +llvm_alias n = LLVM.Alias (fromString n) llvm_packed_struct_type :: [LLVM.Type] -> LLVM.Type llvm_packed_struct_type = LLVM.PackedStruct