diff --git a/CHANGES.md b/CHANGES.md index 89430e19f5..c30667bcc3 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -17,6 +17,14 @@ * New command `w4_unint_z3_using` like `w4_unint_z3`, but use the given Z3 tactic. +* A new `llvm_points_to_bitfield` command has been introduced, providing a + version of `llvm_points_to` that is specifically tailored for structs + containing bitfields. In order to use `llvm_points_to_bitfield`, one must + also use the new `enable_lax_loads_and_stores` command, which relaxes some + of Crucible's assumptions about reading from uninitialized memory. (This + command also comes with a corresponding `disable_lax_loads_and_stores` + command.) For more details on how each of these commands should be used, + consult the "Bitfields" section of the SAW manual. # Version 0.9 diff --git a/deps/crucible b/deps/crucible index c811db88db..acd37d5fc6 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit c811db88db74110c99903f98f70c0f48bee46485 +Subproject commit acd37d5fc69ea41cd8ade700994f69d26c0ed530 diff --git a/deps/llvm-pretty b/deps/llvm-pretty index 15bc003b80..ed904c679d 160000 --- a/deps/llvm-pretty +++ b/deps/llvm-pretty @@ -1 +1 @@ -Subproject commit 15bc003b807c20e273245ea51d72c22c237dba45 +Subproject commit ed904c679d1a10ff98d1968da3407ff56cfa06a2 diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 9752198b7c..f06f234ad6 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -1212,6 +1212,31 @@ Ultimately, we plan to implement a more generic tactic that leaves certain constants uninterpreted in whatever prover is ultimately used (provided that uninterpreted functions are expressible in the prover). +Note that each of the `unint_*` tactics have variants that are prefixed +with `sbv_` and `w4_`. The `sbv_`-prefixed tactics make use of the SBV +library to represent and solve SMT queries: + +* `sbv_unint_cvc4 : [String] -> ProofScript ()` + +* `sbv_unint_yices : [String] -> ProofScript ()` + +* `sbv_unint_z3 : [String] -> ProofScript ()` + +The `w4_`-prefixed tactics make use of the What4 library instead of SBV: + +* `w4_unint_cvc4 : [String] -> ProofScript ()` + +* `w4_unint_yices : [String] -> ProofScript ()` + +* `w4_unint_z3 : [String] -> ProofScript ()` + +In most specifications, the choice of SBV versus What4 is not important, as +both libraries are broadly compatible in terms of functionality. There are some +situations where one library may outpeform the other, however, due to +differences in how each library represents certain SMT queries. There are also +some experimental features that are only supported with What4 at the moment, +such as `enable_lax_loads_and_stores`. + ## Other External Provers In addition to the built-in automated provers already discussed, SAW @@ -2218,6 +2243,78 @@ the value of an array element. * `jvm_field_is : JVMValue -> String -> JVMValue -> JVMSetup ()` specifies the name of an object field. +### Bitfields + +SAW has experimental support for specifying `struct`s with bitfields, such as +in the following example: + +~~~~ .c +struct s { + uint8_t x:1; + uint8_t y:1; +}; +~~~~ + +Normally, a `struct` with two `uint8_t` fields would have an overall size of +two bytes. However, because the `x` and `y` fields are declared with bitfield +syntax, they are instead packed together into a single byte. + +Because bitfields have somewhat unusual memory representations in LLVM, some +special care is required to write SAW specifications involving bitfields. For +this reason, there is a dedicated `llvm_points_to_bitfield` function for this +purpose: + +* `llvm_points_to_bitfield : SetupValue -> String -> SetupValue -> CrucibleSetup ()` + +The type of `llvm_points_to_bitfield` is similar that of `llvm_points_to`, +except that it takes the name of a field within a bitfield as an additional +argument. For example, here is how to assert that the `y` field in the `struct` +example above should be `0`: + +~~~~ +ss <- llvm_alloc (llvm_alias "struct.s"); +llvm_points_to_bitfield ss "y" (llvm_term {{ 0 : [1] }}); +~~~~ + +Note that the type of the right-hand side value (`0`, in this example) must +be a bitvector whose length is equal to the size of the field within the +bitfield. In this example, the `y` field was declared as `y:1`, so `y`'s value +must be of type `[1]`. + +Note that the following specification is _not_ equivalent to the one above: + +~~~~ +ss <- llvm_alloc (llvm_alias "struct.s"); +llvm_points_to (llvm_field ss "y") (llvm_term {{ 0 : [1] }}); +~~~~ + +`llvm_points_to` works quite differently from `llvm_points_to_bitfield` under +the hood, so using `llvm_points_to` on bitfields will almost certainly not work +as expected. + +In order to use `llvm_points_to_bitfield`, one must also use the +`enable_lax_loads_and_stores` command: + +* `enable_lax_loads_and_stores: TopLevel ()` + +Both `llvm_points_to_bitfield` and `enable_lax_loads_and_stores` are +experimental commands, so these also require using `enable_experimental` before +they can be used. + +The `enable_lax_loads_and_stores` command relaxes some +of SAW's assumptions about uninitialized memory, which is necessary to make +`llvm_points_to_bitfield` work under the hood. For example, reading from +uninitialized memory normally results in an error in SAW, but with +`enable_lax_loads_and_stores`, such a read will instead return a symbolic +value. At present, `enable_lax_loads_and_stores` only works with What4-based +tactics (e.g., `w4_unint_z3`); using it with SBV-based tactics +(e.g., `sbv_unint_z3`) will result in an error. + +Note that SAW relies on LLVM debug metadata in order to determine which struct +fields reside within a bitfield. As a result, you must pass `-g` to `clang` when +compiling code involving bitfields in order for SAW to be able to reason about +them. + ## Global variables Mutable global variables that are accessed in a function must first be allocated diff --git a/intTests/test_bitfield_basic/Makefile b/intTests/test_bitfield_basic/Makefile new file mode 100644 index 0000000000..f7abdbe50b --- /dev/null +++ b/intTests/test_bitfield_basic/Makefile @@ -0,0 +1,11 @@ +CC = clang +CFLAGS = -g -emit-llvm -frecord-command-line -O0 + +all: test.bc + +test.bc: test.c + $(CC) $(CFLAGS) -c $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc diff --git a/intTests/test_bitfield_basic/test.bc b/intTests/test_bitfield_basic/test.bc new file mode 100644 index 0000000000..67499f17bb Binary files /dev/null and b/intTests/test_bitfield_basic/test.bc differ diff --git a/intTests/test_bitfield_basic/test.c b/intTests/test_bitfield_basic/test.c new file mode 100644 index 0000000000..fd395526f4 --- /dev/null +++ b/intTests/test_bitfield_basic/test.c @@ -0,0 +1,34 @@ +#include +#include + +struct s { + int32_t w; + uint8_t x1:1; + uint8_t x2:2; + uint8_t y:1; + int32_t z; +}; + +uint8_t get_x2(struct s *ss) { + return ss->x2; +} + +bool get_y(struct s *ss) { + return ss->y; +} + +void set_x2(struct s *ss, uint8_t x2) { + ss->x2 = x2; +} + +void set_y(struct s *ss, bool y) { + ss->y = y; +} + +void set_x2_alt(struct s *ss, uint8_t x2) { + set_x2(ss, x2); +} + +void set_y_alt(struct s *ss, bool y) { + set_y(ss, y); +} diff --git a/intTests/test_bitfield_basic/test.saw b/intTests/test_bitfield_basic/test.saw new file mode 100644 index 0000000000..ee1b4b46f7 --- /dev/null +++ b/intTests/test_bitfield_basic/test.saw @@ -0,0 +1,55 @@ +enable_experimental; +enable_lax_loads_and_stores; + +let get_x2_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 2); + llvm_points_to_bitfield ss "x2" (llvm_term z); + llvm_execute_func [ss]; + llvm_return (llvm_term {{ zext z : [8] }}); +}; + +let get_y_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 1); + llvm_points_to_bitfield ss "y" (llvm_term z); + llvm_execute_func [ss]; + llvm_return (llvm_term z); +}; + +let set_x2_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 8); + llvm_execute_func [ss, llvm_term z]; + llvm_points_to_bitfield ss "x2" (llvm_term {{ drop z : [2] }}); +}; + +let set_x2_alt_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 2); + llvm_execute_func [ss, llvm_term {{ zext z : [8] }}]; + llvm_points_to_bitfield ss "x2" (llvm_term z); +}; + +let set_y_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 1); + llvm_execute_func [ss, llvm_term z]; + llvm_points_to_bitfield ss "y" (llvm_term z); +}; + +let set_y_alt_spec = set_y_spec; + +m <- llvm_load_module "test.bc"; + +llvm_verify m "get_x2" [] false get_x2_spec (w4_unint_z3 []); +llvm_verify m "get_y" [] false get_y_spec (w4_unint_z3 []); +llvm_verify m "set_x2" [] false set_x2_spec (w4_unint_z3 []); +llvm_verify m "set_x2_alt" [] false set_x2_alt_spec (w4_unint_z3 []); +llvm_verify m "set_y" [] false set_y_spec (w4_unint_z3 []); +llvm_verify m "set_y_alt" [] false set_y_alt_spec (w4_unint_z3 []); + +set_x2_ov <- llvm_unsafe_assume_spec m "set_x2" set_x2_spec; +llvm_verify m "set_x2_alt" [set_x2_ov] false set_x2_alt_spec (w4_unint_z3 []); +set_y_ov <- llvm_unsafe_assume_spec m "set_y" set_y_spec; +llvm_verify m "set_y_alt" [set_y_ov] false set_y_alt_spec (w4_unint_z3 []); diff --git a/intTests/test_bitfield_basic/test.sh b/intTests/test_bitfield_basic/test.sh new file mode 100755 index 0000000000..6c3e577771 --- /dev/null +++ b/intTests/test_bitfield_basic/test.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash + +set -e + +$SAW test.saw diff --git a/intTests/test_bitfield_duplicate_points_to/Makefile b/intTests/test_bitfield_duplicate_points_to/Makefile new file mode 100644 index 0000000000..f7abdbe50b --- /dev/null +++ b/intTests/test_bitfield_duplicate_points_to/Makefile @@ -0,0 +1,11 @@ +CC = clang +CFLAGS = -g -emit-llvm -frecord-command-line -O0 + +all: test.bc + +test.bc: test.c + $(CC) $(CFLAGS) -c $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc diff --git a/intTests/test_bitfield_duplicate_points_to/test.bc b/intTests/test_bitfield_duplicate_points_to/test.bc new file mode 100644 index 0000000000..2abbc5ae3d Binary files /dev/null and b/intTests/test_bitfield_duplicate_points_to/test.bc differ diff --git a/intTests/test_bitfield_duplicate_points_to/test.c b/intTests/test_bitfield_duplicate_points_to/test.c new file mode 100644 index 0000000000..39487ddaaa --- /dev/null +++ b/intTests/test_bitfield_duplicate_points_to/test.c @@ -0,0 +1,14 @@ +#include +#include + +struct s { + int32_t w; + uint8_t x1:1; + uint8_t x2:2; + uint8_t y:1; + int32_t z; +}; + +bool get_y(struct s *ss) { + return ss->y; +} diff --git a/intTests/test_bitfield_duplicate_points_to/test.saw b/intTests/test_bitfield_duplicate_points_to/test.saw new file mode 100644 index 0000000000..a94d009bea --- /dev/null +++ b/intTests/test_bitfield_duplicate_points_to/test.saw @@ -0,0 +1,15 @@ +enable_experimental; +enable_lax_loads_and_stores; + +let get_y_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 1); + // Duplicate llvm_points_to_bitfield statements involving `y` + llvm_points_to_bitfield ss "y" (llvm_term z); + llvm_points_to_bitfield ss "y" (llvm_term z); + llvm_execute_func [ss]; + llvm_return (llvm_term z); +}; + +m <- llvm_load_module "test.bc"; +fails (llvm_verify m "get_y" [] false get_y_spec (w4_unint_z3 [])); diff --git a/intTests/test_bitfield_duplicate_points_to/test.sh b/intTests/test_bitfield_duplicate_points_to/test.sh new file mode 100755 index 0000000000..6c3e577771 --- /dev/null +++ b/intTests/test_bitfield_duplicate_points_to/test.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash + +set -e + +$SAW test.saw diff --git a/intTests/test_bitfield_smt_array/Makefile b/intTests/test_bitfield_smt_array/Makefile new file mode 100644 index 0000000000..f7abdbe50b --- /dev/null +++ b/intTests/test_bitfield_smt_array/Makefile @@ -0,0 +1,11 @@ +CC = clang +CFLAGS = -g -emit-llvm -frecord-command-line -O0 + +all: test.bc + +test.bc: test.c + $(CC) $(CFLAGS) -c $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc diff --git a/intTests/test_bitfield_smt_array/test.bc b/intTests/test_bitfield_smt_array/test.bc new file mode 100644 index 0000000000..33519966be Binary files /dev/null and b/intTests/test_bitfield_smt_array/test.bc differ diff --git a/intTests/test_bitfield_smt_array/test.c b/intTests/test_bitfield_smt_array/test.c new file mode 100644 index 0000000000..fd395526f4 --- /dev/null +++ b/intTests/test_bitfield_smt_array/test.c @@ -0,0 +1,34 @@ +#include +#include + +struct s { + int32_t w; + uint8_t x1:1; + uint8_t x2:2; + uint8_t y:1; + int32_t z; +}; + +uint8_t get_x2(struct s *ss) { + return ss->x2; +} + +bool get_y(struct s *ss) { + return ss->y; +} + +void set_x2(struct s *ss, uint8_t x2) { + ss->x2 = x2; +} + +void set_y(struct s *ss, bool y) { + ss->y = y; +} + +void set_x2_alt(struct s *ss, uint8_t x2) { + set_x2(ss, x2); +} + +void set_y_alt(struct s *ss, bool y) { + set_y(ss, y); +} diff --git a/intTests/test_bitfield_smt_array/test.saw b/intTests/test_bitfield_smt_array/test.saw new file mode 100644 index 0000000000..d1db89d74e --- /dev/null +++ b/intTests/test_bitfield_smt_array/test.saw @@ -0,0 +1,55 @@ +enable_experimental; +enable_lax_loads_and_stores; +enable_smt_array_memory_model; + +let get_x2_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 2); + llvm_points_to_bitfield ss "x2" (llvm_term z); + llvm_execute_func [ss]; + llvm_return (llvm_term {{ zext z : [8] }}); +}; + +let get_y_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 1); + llvm_points_to_bitfield ss "y" (llvm_term z); + llvm_execute_func [ss]; + llvm_return (llvm_term z); +}; + +let set_x2_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 8); + llvm_execute_func [ss, llvm_term z]; + llvm_points_to_bitfield ss "x2" (llvm_term {{ drop z : [2] }}); +}; + +let set_x2_alt_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 2); + llvm_execute_func [ss, llvm_term {{ zext z : [8] }}]; + llvm_points_to_bitfield ss "x2" (llvm_term z); +}; + +let set_y_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 1); + llvm_execute_func [ss, llvm_term z]; + llvm_points_to_bitfield ss "y" (llvm_term z); +}; + +let set_y_alt_spec = set_y_spec; + +m <- llvm_load_module "test.bc"; + +llvm_verify m "get_x2" [] false get_x2_spec (w4_unint_z3 []); +llvm_verify m "get_y" [] false get_y_spec (w4_unint_z3 []); +llvm_verify m "set_x2" [] false set_x2_spec (w4_unint_z3 []); +llvm_verify m "set_x2_alt" [] false set_x2_alt_spec (w4_unint_z3 []); +llvm_verify m "set_y" [] false set_y_spec (w4_unint_z3 []); + +set_x2_ov <- llvm_unsafe_assume_spec m "set_x2" set_x2_spec; +llvm_verify m "set_x2_alt" [set_x2_ov] false set_x2_alt_spec (w4_unint_z3 []); +set_y_ov <- llvm_unsafe_assume_spec m "set_y" set_y_spec; +llvm_verify m "set_y_alt" [set_y_ov] false set_y_alt_spec (w4_unint_z3 []); diff --git a/intTests/test_bitfield_smt_array/test.sh b/intTests/test_bitfield_smt_array/test.sh new file mode 100755 index 0000000000..1ea587c8fc --- /dev/null +++ b/intTests/test_bitfield_smt_array/test.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash + +set -e + +# llvm_points_to_bitfield and enable_smt_array_memory_model currently do not +# mix. See #1540. +! $SAW test.saw diff --git a/intTests/test_bitfield_wrong_type/Makefile b/intTests/test_bitfield_wrong_type/Makefile new file mode 100644 index 0000000000..f7abdbe50b --- /dev/null +++ b/intTests/test_bitfield_wrong_type/Makefile @@ -0,0 +1,11 @@ +CC = clang +CFLAGS = -g -emit-llvm -frecord-command-line -O0 + +all: test.bc + +test.bc: test.c + $(CC) $(CFLAGS) -c $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc diff --git a/intTests/test_bitfield_wrong_type/test.bc b/intTests/test_bitfield_wrong_type/test.bc new file mode 100644 index 0000000000..02d9b20b95 Binary files /dev/null and b/intTests/test_bitfield_wrong_type/test.bc differ diff --git a/intTests/test_bitfield_wrong_type/test.c b/intTests/test_bitfield_wrong_type/test.c new file mode 100644 index 0000000000..9bf199316e --- /dev/null +++ b/intTests/test_bitfield_wrong_type/test.c @@ -0,0 +1,14 @@ +#include +#include + +struct s { + int32_t w; + uint8_t x1:1; + uint8_t x2:2; + uint8_t y:1; + int32_t z; +}; + +void set_y(struct s *ss, bool y) { + ss->y = y; +} diff --git a/intTests/test_bitfield_wrong_type/test.saw b/intTests/test_bitfield_wrong_type/test.saw new file mode 100644 index 0000000000..8c89b60435 --- /dev/null +++ b/intTests/test_bitfield_wrong_type/test.saw @@ -0,0 +1,14 @@ +enable_experimental; +enable_lax_loads_and_stores; + +let set_y_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + // Note that the type is 8 bits, which is a different number of bits than + // what is specified in the bitfield. + z <- llvm_fresh_var "z" (llvm_int 8); + llvm_execute_func [ss, llvm_term z]; + llvm_points_to_bitfield ss "y" (llvm_term z); +}; + +m <- llvm_load_module "test.bc"; +fails (llvm_verify m "set_y" [] false set_y_spec (w4_unint_z3 [])); diff --git a/intTests/test_bitfield_wrong_type/test.sh b/intTests/test_bitfield_wrong_type/test.sh new file mode 100755 index 0000000000..6c3e577771 --- /dev/null +++ b/intTests/test_bitfield_wrong_type/test.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash + +set -e + +$SAW test.saw diff --git a/intTests/test_bitfield_x86/Makefile b/intTests/test_bitfield_x86/Makefile new file mode 100644 index 0000000000..1a3bb3f6a4 --- /dev/null +++ b/intTests/test_bitfield_x86/Makefile @@ -0,0 +1,17 @@ +CC = clang +CFLAGS = -g -frecord-command-line -O0 + +all: test.bc test.exe + +test.bc: test.c + $(CC) $(CFLAGS) -c -emit-llvm $< -o $@ + +test.o: test.c + $(CC) $(CFLAGS) -c $< -o $@ + +test.exe: test.o + $(CC) $(CFLAGS) $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc test.exe diff --git a/intTests/test_bitfield_x86/test.bc b/intTests/test_bitfield_x86/test.bc new file mode 100644 index 0000000000..ef6aec72e8 Binary files /dev/null and b/intTests/test_bitfield_x86/test.bc differ diff --git a/intTests/test_bitfield_x86/test.c b/intTests/test_bitfield_x86/test.c new file mode 100644 index 0000000000..3ff259cc8b --- /dev/null +++ b/intTests/test_bitfield_x86/test.c @@ -0,0 +1,38 @@ +#include +#include + +struct s { + int32_t w; + uint8_t x1:1; + uint8_t x2:2; + uint8_t y:1; + int32_t z; +}; + +uint8_t get_x2(struct s *ss) { + return ss->x2; +} + +bool get_y(struct s *ss) { + return ss->y; +} + +void set_x2(struct s *ss, uint8_t x2) { + ss->x2 = x2; +} + +void set_y(struct s *ss, bool y) { + ss->y = y; +} + +void set_x2_alt(struct s *ss, uint8_t x2) { + set_x2(ss, x2); +} + +void set_y_alt(struct s *ss, bool y) { + set_y(ss, y); +} + +int main() { + return 0; +} diff --git a/intTests/test_bitfield_x86/test.exe b/intTests/test_bitfield_x86/test.exe new file mode 100755 index 0000000000..f7f5ee7ea0 Binary files /dev/null and b/intTests/test_bitfield_x86/test.exe differ diff --git a/intTests/test_bitfield_x86/test.o b/intTests/test_bitfield_x86/test.o new file mode 100644 index 0000000000..1207e45fb7 Binary files /dev/null and b/intTests/test_bitfield_x86/test.o differ diff --git a/intTests/test_bitfield_x86/test.saw b/intTests/test_bitfield_x86/test.saw new file mode 100644 index 0000000000..6fdf67482f --- /dev/null +++ b/intTests/test_bitfield_x86/test.saw @@ -0,0 +1,50 @@ +enable_experimental; +enable_lax_loads_and_stores; + +let get_x2_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 2); + llvm_points_to_bitfield ss "x2" (llvm_term z); + llvm_execute_func [ss]; + llvm_return (llvm_term {{ zext z : [8] }}); +}; + +let get_y_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 1); + llvm_points_to_bitfield ss "y" (llvm_term z); + llvm_execute_func [ss]; + llvm_return (llvm_term z); +}; + +let set_x2_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 8); + llvm_execute_func [ss, llvm_term z]; + llvm_points_to_bitfield ss "x2" (llvm_term {{ drop z : [2] }}); +}; + +let set_x2_alt_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 2); + llvm_execute_func [ss, llvm_term {{ zext z : [8] }}]; + llvm_points_to_bitfield ss "x2" (llvm_term z); +}; + +let set_y_spec = do { + ss <- llvm_alloc (llvm_alias "struct.s"); + z <- llvm_fresh_var "z" (llvm_int 1); + llvm_execute_func [ss, llvm_term z]; + llvm_points_to_bitfield ss "y" (llvm_term z); +}; + +let set_y_alt_spec = set_y_spec; + +m <- llvm_load_module "test.bc"; + +llvm_verify_x86 m "test.exe" "get_x2" [] false get_x2_spec (w4_unint_z3 []); +llvm_verify_x86 m "test.exe" "get_y" [] false get_y_spec (w4_unint_z3 []); +llvm_verify_x86 m "test.exe" "set_x2" [] false set_x2_spec (w4_unint_z3 []); +llvm_verify_x86 m "test.exe" "set_x2_alt" [] false set_x2_alt_spec (w4_unint_z3 []); +llvm_verify_x86 m "test.exe" "set_y" [] false set_y_spec (w4_unint_z3 []); +llvm_verify_x86 m "test.exe" "set_y_alt" [] false set_y_alt_spec (w4_unint_z3 []); diff --git a/intTests/test_bitfield_x86/test.sh b/intTests/test_bitfield_x86/test.sh new file mode 100755 index 0000000000..6c3e577771 --- /dev/null +++ b/intTests/test_bitfield_x86/test.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash + +set -e + +$SAW test.saw diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md index 75331c25a9..519e62d56e 100644 --- a/saw-remote-api/CHANGELOG.md +++ b/saw-remote-api/CHANGELOG.md @@ -6,6 +6,16 @@ * `SAW/set option`'s `"option"` parameter is now allowed to be `"What4 eval"`, which controls whether to enable or disable What4 translation for SAWCore expressions during Crucible symbolic execution. +* `SAW/set option`'s `"option"` parameter is now allowed to be + `"lax loads and stores"`, which controls whether to enable or disable relaxed + validity checking for memory loads and stores in Crucible. +* Specifications now have additional `pre points to bitfield` and + `post points to bitfield` fields, each of which is a list of "points-to" + relationships pertaining to structs that contain bitfields. If not specified, + these will default to empty lists. Bitfields are only meaningful for LLVM + verification, so JVM specifications must leave these lists empty. Attempting + to provide a non-empty list for either of these fields in a JVM specification + will result in an error. ## 0.9.0 -- 2021-11-19 diff --git a/saw-remote-api/docs/SAW.rst b/saw-remote-api/docs/SAW.rst index c3bbec7b18..34acd08a71 100644 --- a/saw-remote-api/docs/SAW.rst +++ b/saw-remote-api/docs/SAW.rst @@ -515,7 +515,7 @@ Parameter fields ``option`` - The option to set and its accompanying value (i.e., true or false); one of the following:``lax arithmetic``, ``lax pointer ordering``, ``debug intrinsics``, ``SMT array memory model``, ``What4 hash consing``, or ``What4 eval`` + The option to set and its accompanying value (i.e., true or false); one of the following:``lax arithmetic``, ``lax pointer ordering``, ``lax loads and stores``, ``debug intrinsics``, ``SMT array memory model``, ``What4 hash consing``, or ``What4 eval`` diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md index e3bacdff89..7c4cb19f3f 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -7,6 +7,12 @@ equivalent to `set_option(LaxPointerOrdering(), True)` in `saw-client. `LaxPointerOrdering`, as well as all other possible options, can be imported from the `saw_client.option` module. +* Add a `points_to_bitfield` command that allows specifying fields of structs + that contain bitfields. The caveats described in the Bitfields section of the + SAW manual also apply to Python. Notably, one must use + `set_option(LaxLoadsAndStores(), True)` in order for `points_to_bitfield` to + work as expected. `points_to_bitfield` is only supported for LLVM (and not + JVM) verification. ## 0.9.0 -- 2021-11-19 diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py index f17ae1057d..1c327f792b 100644 --- a/saw-remote-api/python/saw_client/crucible.py +++ b/saw-remote-api/python/saw_client/crucible.py @@ -271,6 +271,22 @@ def to_json(self) -> Any: "check points to type": check_target_type_json, "condition": self.condition.to_json() if self.condition is not None else self.condition} + +class PointsToBitfield: + """The workhorse for ``points_to_bitfield``. + """ + def __init__(self, pointer : SetupVal, field_name : str, + target : SetupVal) -> None: + self.pointer = pointer + self.field_name = field_name + self.target = target + + def to_json(self) -> Any: + return {"pointer": self.pointer.to_json(), + "field name": self.field_name, + "points to": self.target.to_json()} + + @dataclass class GhostVariable: name: str @@ -295,6 +311,7 @@ class State: conditions : List[Condition] = dataclasses.field(default_factory=list) allocated : List[Allocated] = dataclasses.field(default_factory=list) points_to : List[PointsTo] = dataclasses.field(default_factory=list) + points_to_bitfield : List[PointsToBitfield] = dataclasses.field(default_factory=list) ghost_values : List[GhostValue] = dataclasses.field(default_factory=list) def to_json(self) -> Any: @@ -302,6 +319,7 @@ def to_json(self) -> Any: 'conditions': [c.to_json() for c in self.conditions], 'allocated': [a.to_init_json() for a in self.allocated], 'points to': [p.to_json() for p in self.points_to], + 'points to bitfield': [p.to_json() for p in self.points_to_bitfield], 'ghost values': [g.to_json() for g in self.ghost_values] } @@ -447,6 +465,23 @@ def points_to(self, pointer : SetupVal, target : SetupVal, *, else: raise Exception("wrong state") + def points_to_bitfield(self, pointer : SetupVal, field_name : str, + target : SetupVal) -> None: + """Declare that the memory location indicated by the ``pointer`` + is a bitfield whose field, indicated by the ``field_name``, + contains the ``target``. + + Currently, this function only supports LLVM verification. Attempting to + use this function for JVM verification will result in an error. + """ + pt = PointsToBitfield(pointer, field_name, target) + if self.__state == 'pre': + self.__pre_state.points_to_bitfield.append(pt) + elif self.__state == 'post': + self.__post_state.points_to_bitfield.append(pt) + else: + raise Exception("wrong state") + def ghost_value(self, var: GhostVariable, value: CryptolTerm) -> None: """Declare that the given ghost variable should have a value specified by the given Cryptol expression. @@ -551,12 +586,14 @@ def to_json(self) -> Any: 'pre allocated': [a.to_init_json() for a in self.__pre_state.allocated], 'pre ghost values': [g.to_json() for g in self.__pre_state.ghost_values], 'pre points tos': [pt.to_json() for pt in self.__pre_state.points_to], + 'pre points to bitfields': [pt.to_json() for pt in self.__pre_state.points_to_bitfield], 'argument vals': [a.to_json() for a in self.__arguments] if self.__arguments is not None else [], 'post vars': [v.to_init_json() for v in self.__post_state.fresh], 'post conds': [c.to_json() for c in self.__post_state.conditions], 'post allocated': [a.to_init_json() for a in self.__post_state.allocated], 'post ghost values': [g.to_json() for g in self.__post_state.ghost_values], 'post points tos': [pt.to_json() for pt in self.__post_state.points_to], + 'post points to bitfields': [pt.to_json() for pt in self.__post_state.points_to_bitfield], 'return val': self.__returns.to_json()} return self.__cached_json diff --git a/saw-remote-api/python/saw_client/option.py b/saw-remote-api/python/saw_client/option.py index 5051455d8b..974b9e8a5a 100644 --- a/saw-remote-api/python/saw_client/option.py +++ b/saw-remote-api/python/saw_client/option.py @@ -19,6 +19,12 @@ def __str__(self) -> str: return "lax pointer ordering" +@dataclass +class LaxLoadsAndStores(SAWOption): + def __str__(self) -> str: + return "lax loads and stores" + + @dataclass class DebugIntrinsics(SAWOption): def __str__(self) -> str: diff --git a/saw-remote-api/python/tests/saw/test-files/llvm_points_to_bitfield.bc b/saw-remote-api/python/tests/saw/test-files/llvm_points_to_bitfield.bc new file mode 100644 index 0000000000..641d5cb3d1 Binary files /dev/null and b/saw-remote-api/python/tests/saw/test-files/llvm_points_to_bitfield.bc differ diff --git a/saw-remote-api/python/tests/saw/test-files/llvm_points_to_bitfield.c b/saw-remote-api/python/tests/saw/test-files/llvm_points_to_bitfield.c new file mode 100644 index 0000000000..fd395526f4 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/llvm_points_to_bitfield.c @@ -0,0 +1,34 @@ +#include +#include + +struct s { + int32_t w; + uint8_t x1:1; + uint8_t x2:2; + uint8_t y:1; + int32_t z; +}; + +uint8_t get_x2(struct s *ss) { + return ss->x2; +} + +bool get_y(struct s *ss) { + return ss->y; +} + +void set_x2(struct s *ss, uint8_t x2) { + ss->x2 = x2; +} + +void set_y(struct s *ss, bool y) { + ss->y = y; +} + +void set_x2_alt(struct s *ss, uint8_t x2) { + set_x2(ss, x2); +} + +void set_y_alt(struct s *ss, bool y) { + set_y(ss, y); +} diff --git a/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py b/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py new file mode 100644 index 0000000000..10f3f5e6d7 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py @@ -0,0 +1,114 @@ +from pathlib import Path +import unittest +from saw_client import * +from saw_client.llvm import Contract, LLVMIntType, alias_ty, cryptol, i8, void +from saw_client.option import LaxLoadsAndStores + + +i1 = LLVMIntType(1) +i2 = LLVMIntType(2) + + +class GetX2Contract(Contract): + def specification(self): + ss = self.alloc(alias_ty('struct.s')) + z = self.fresh_var(i2, 'z') + self.points_to_bitfield(ss, 'x2', z) + + self.execute_func(ss) + + self.returns(cryptol(f'zext {z.name()} : [8]')) + + +class GetYContract(Contract): + def specification(self): + ss = self.alloc(alias_ty('struct.s')) + z = self.fresh_var(i1, 'z') + self.points_to_bitfield(ss, 'y', z) + + self.execute_func(ss) + + self.returns(z) + + +class SetX2Contract(Contract): + def specification(self): + ss = self.alloc(alias_ty('struct.s')) + z = self.fresh_var(i8, 'z') + + self.execute_func(ss, z) + + self.points_to_bitfield(ss, 'x2', cryptol(f'drop {z.name()} : [2]')) + self.returns(void) + + +class SetX2AltContract(Contract): + def specification(self): + ss = self.alloc(alias_ty('struct.s')) + z = self.fresh_var(i2, 'z') + + self.execute_func(ss, cryptol(f'zext {z.name()} : [8]')) + + self.points_to_bitfield(ss, 'x2', z) + self.returns(void) + + +def y_spec(c : Contract) -> None: + ss = c.alloc(alias_ty('struct.s')) + z = c.fresh_var(i1, 'z') + + c.execute_func(ss, z) + + c.points_to_bitfield(ss, 'y', z) + c.returns(void) + + +class SetYContract(Contract): + def specification(self): + y_spec(self) + + +class SetYAltContract(Contract): + def specification(self): + y_spec(self) + + +class LLVMNestedStructTest(unittest.TestCase): + def test_llvm_struct(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults()) + + bcname = str(Path('tests','saw','test-files', 'llvm_points_to_bitfield.bc')) + mod = llvm_load_module(bcname) + + set_option(LaxLoadsAndStores(), True) + + result = llvm_verify(mod, 'get_x2', GetX2Contract()) + self.assertIs(result.is_success(), True) + + result = llvm_verify(mod, 'get_y', GetYContract()) + self.assertIs(result.is_success(), True) + + result = llvm_verify(mod, 'set_x2', SetX2Contract()) + self.assertIs(result.is_success(), True) + + result = llvm_verify(mod, 'set_x2_alt', SetX2AltContract()) + self.assertIs(result.is_success(), True) + + result = llvm_verify(mod, 'set_y', SetYContract()) + self.assertIs(result.is_success(), True) + + result = llvm_verify(mod, 'set_y_alt', SetYAltContract()) + self.assertIs(result.is_success(), True) + + set_x2_ov = llvm_assume(mod, 'set_x2', SetX2Contract()) + result = llvm_verify(mod, 'set_x2_alt', SetX2AltContract(), lemmas=[set_x2_ov]) + self.assertIs(result.is_success(), True) + + set_y_ov = llvm_assume(mod, 'set_y', SetYContract()) + result = llvm_verify(mod, 'set_y_alt', SetYAltContract(), lemmas=[set_x2_ov]) + self.assertIs(result.is_success(), True) + + +if __name__ == "__main__": + unittest.main() diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 758c7337d9..655f3f461d 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -110,6 +110,12 @@ data SetupStep ty (Maybe CryptolAST) -- ^ The source, the target, the type to check the target, -- and the condition that must hold in order for the source to point to the target + | SetupPointsToBitfield (CrucibleSetupVal CryptolAST) + Text + (CrucibleSetupVal CryptolAST) + -- ^ The source bitfield, + -- the name of the field within the bitfield, + -- and the target. | SetupExecuteFunction [CrucibleSetupVal CryptolAST] -- ^ Function's arguments | SetupPrecond CryptolAST -- ^ Function's precondition | SetupPostcond CryptolAST -- ^ Function's postcondition @@ -218,6 +224,7 @@ initialState readFileFn = , rwCrucibleAssertThenAssume = False , rwLaxArith = False , rwLaxPointerOrdering = False + , rwLaxLoadsAndStores = False , rwDebugIntrinsics = True , rwWhat4HashConsing = False , rwWhat4HashConsingX86 = False diff --git a/saw-remote-api/src/SAWServer/Data/Contract.hs b/saw-remote-api/src/SAWServer/Data/Contract.hs index d3647de328..6fc7aa3902 100644 --- a/saw-remote-api/src/SAWServer/Data/Contract.hs +++ b/saw-remote-api/src/SAWServer/Data/Contract.hs @@ -11,6 +11,7 @@ module SAWServer.Data.Contract , Allocated(..) , GhostValue(..) , PointsTo(..) + , PointsToBitfield(..) ) where import Control.Applicative @@ -34,12 +35,14 @@ data Contract ty cryptolExpr = , preAllocated :: [Allocated ty] , preGhostValues :: [GhostValue cryptolExpr] , prePointsTos :: [PointsTo ty cryptolExpr] + , prePointsToBitfields :: [PointsToBitfield cryptolExpr] , argumentVals :: [CrucibleSetupVal cryptolExpr] , postVars :: [ContractVar ty] , postConds :: [cryptolExpr] , postAllocated :: [Allocated ty] , postGhostValues :: [GhostValue cryptolExpr] , postPointsTos :: [PointsTo ty cryptolExpr] + , postPointsToBitfields :: [PointsToBitfield cryptolExpr] , returnVal :: Maybe (CrucibleSetupVal cryptolExpr) } deriving stock (Functor, Foldable, Traversable) @@ -67,6 +70,13 @@ data PointsTo ty cryptolExpr = , condition :: Maybe cryptolExpr } deriving stock (Functor, Foldable, Traversable) +data PointsToBitfield cryptolExpr = + PointsToBitfield + { bfPointer :: CrucibleSetupVal cryptolExpr + , bfFieldName :: Text + , bfPointsTo :: CrucibleSetupVal cryptolExpr + } deriving stock (Functor, Foldable, Traversable) + data CheckAgainstTag = TagCheckAgainstPointerType | TagCheckAgainstCastedType @@ -86,6 +96,13 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (PointsTo ty cryptolExp <*> o .:? "check points to type" <*> o .:? "condition" +instance FromJSON cryptolExpr => FromJSON (PointsToBitfield cryptolExpr) where + parseJSON = + withObject "Points-to-bitfield relationship" $ \o -> + PointsToBitfield <$> o .: "pointer" + <*> o .: "field name" + <*> o .: "points to" + instance FromJSON cryptolExpr => FromJSON (GhostValue cryptolExpr) where parseJSON = withObject "ghost variable value" $ \o -> @@ -115,12 +132,14 @@ instance (FromJSON ty, FromJSON e) => FromJSON (Contract ty e) where <*> o .: "pre allocated" <*> o .:? "pre ghost values" .!= [] <*> o .: "pre points tos" + <*> o .:? "pre points to bitfields" .!= [] <*> o .: "argument vals" <*> o .: "post vars" <*> o .: "post conds" <*> o .: "post allocated" <*> o .:? "post ghost values" .!= [] <*> o .: "post points tos" + <*> o .:? "post points to bitfields" .!= [] <*> o .:? "return val" instance FromJSON CheckAgainstTag where diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index 3aaf83b616..dec9344cdf 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -55,10 +55,11 @@ import SAWServer setServerVal ) import SAWServer.Data.Contract ( PointsTo(PointsTo), + PointsToBitfield, Allocated(Allocated), ContractVar(ContractVar), - Contract(preVars, preConds, preAllocated, prePointsTos, - argumentVals, postVars, postConds, postAllocated, postPointsTos, + Contract(preVars, preConds, preAllocated, prePointsTos, prePointsToBitfields, + argumentVals, postVars, postConds, postAllocated, postPointsTos, postPointsToBitfields, returnVal) ) import SAWServer.Data.SetupValue () import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp) @@ -94,12 +95,14 @@ compileJVMContract fileReader bic cenv0 c = (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) mapM_ (\p -> getTypedTerm cenvPre p >>= jvm_precond) (preConds c) mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c) + mapM_ setupPointsToBitfields (prePointsToBitfields c) --mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= jvm_execute_func allocsPost <- mapM setupAlloc (postAllocated c) (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c) mapM_ (\p -> getTypedTerm cenvPost p >>= jvm_postcond) (postConds c) mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c) + mapM_ setupPointsToBitfields (postPointsToBitfields c) --mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) case returnVal c of Just v -> getSetupVal (envPost, cenvPost) v >>= jvm_return @@ -142,6 +145,10 @@ compileJVMContract fileReader bic cenv0 c = GlobalLValue name -> jvm_static_field_is name sv _ -> JVMSetupM $ fail "Invalid points-to statement." + setupPointsToBitfields :: PointsToBitfield (P.Expr P.PName) -> JVMSetupM () + setupPointsToBitfields _ = + JVMSetupM $ fail "Points-to-bitfield not supported in JVM API." + --setupGhostValue _ _ _ = fail "Ghost values not supported yet in JVM API." resolve :: Map ServerName a -> ServerName -> JVMSetupM a diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs index 893663d790..b0b27a30db 100644 --- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs @@ -26,6 +26,7 @@ import Data.Aeson (FromJSON(..), withObject, (.:)) import Data.ByteString (ByteString) import Data.Map (Map) import qualified Data.Map as Map +import qualified Data.Text as Text import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) @@ -39,6 +40,7 @@ import SAWScript.Crucible.LLVM.Builtins , llvm_execute_func , llvm_fresh_var , llvm_points_to_internal + , llvm_points_to_bitfield , llvm_ghost_value , llvm_return , llvm_precond @@ -63,7 +65,7 @@ import SAWServer as Server getHandleAlloc, setServerVal ) import SAWServer.Data.Contract - ( PointsTo(..), GhostValue(..), Allocated(..), ContractVar(..), Contract(..) ) + ( PointsTo(..), PointsToBitfield(..), GhostValue(..), Allocated(..), ContractVar(..), Contract(..) ) import SAWServer.Data.LLVMType (JSONLLVMType, llvmType) import SAWServer.Data.SetupValue () import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp) @@ -93,12 +95,14 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c = (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) mapM_ (\p -> getTypedTerm cenvPre p >>= llvm_precond) (preConds c) mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c) + mapM_ (setupPointsToBitfield (envPre, cenvPre)) (prePointsToBitfields c) mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= llvm_execute_func allocsPost <- mapM setupAlloc (postAllocated c) (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c) mapM_ (\p -> getTypedTerm cenvPost p >>= llvm_postcond) (postConds c) mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c) + mapM_ (setupPointsToBitfield (envPost, cenvPost)) (postPointsToBitfields c) mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) case returnVal c of Just v -> getSetupVal (envPost, cenvPost) v >>= llvm_return @@ -132,6 +136,16 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c = let chkTgt' = fmap (fmap llvmType) chkTgt llvm_points_to_internal chkTgt' cond' ptr val + setupPointsToBitfield :: + (Map ServerName ServerSetupVal, CryptolEnv) -> + PointsToBitfield (P.Expr P.PName) -> + LLVMCrucibleSetupM () + setupPointsToBitfield env (PointsToBitfield p fieldName v) = + do ptr <- getSetupVal env p + let fieldName' = Text.unpack fieldName + val <- getSetupVal env v + llvm_points_to_bitfield ptr fieldName' val + setupGhostValue genv cenv (GhostValue serverName e) = do g <- resolve genv serverName t <- getTypedTerm cenv e diff --git a/saw-remote-api/src/SAWServer/SetOption.hs b/saw-remote-api/src/SAWServer/SetOption.hs index 59b070bee2..2244dfcf37 100644 --- a/saw-remote-api/src/SAWServer/SetOption.hs +++ b/saw-remote-api/src/SAWServer/SetOption.hs @@ -33,6 +33,8 @@ setOption opt = updateRW rw { rwLaxArith = enabled } EnableLaxPointerOrdering enabled -> updateRW rw { rwLaxPointerOrdering = enabled } + EnableLaxLoadsAndStores enabled -> + updateRW rw { rwLaxLoadsAndStores = enabled } EnableDebugIntrinsics enabled -> updateRW rw { rwDebugIntrinsics = enabled } EnableSMTArrayMemoryModel enabled -> @@ -46,6 +48,7 @@ setOption opt = data SetOptionParams = EnableLaxArithmetic Bool | EnableLaxPointerOrdering Bool + | EnableLaxLoadsAndStores Bool | EnableDebugIntrinsics Bool | EnableSMTArrayMemoryModel Bool | EnableWhat4HashConsing Bool @@ -56,6 +59,7 @@ parseOption o name = case name of "lax arithmetic" -> EnableLaxArithmetic <$> o .: "value" "lax pointer ordering" -> EnableLaxPointerOrdering <$> o .: "value" + "lax loads and stores" -> EnableLaxLoadsAndStores <$> o .: "value" "debug intrinsics" -> EnableDebugIntrinsics <$> o .: "value" "SMT array memory model" -> EnableSMTArrayMemoryModel <$> o .: "value" "What4 hash consing" -> EnableWhat4HashConsing <$> o .: "value" @@ -73,6 +77,7 @@ instance Doc.DescribedMethod SetOptionParams OK where Doc.Paragraph [Doc.Text "The option to set and its accompanying value (i.e., true or false); one of the following:" , Doc.Literal "lax arithmetic", Doc.Text ", " , Doc.Literal "lax pointer ordering", Doc.Text ", " + , Doc.Literal "lax loads and stores", Doc.Text ", " , Doc.Literal "debug intrinsics", Doc.Text ", " , Doc.Literal "SMT array memory model", Doc.Text ", " , Doc.Literal "What4 hash consing", Doc.Text ", or " diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index a781fc2a88..b5ce18adb5 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -48,6 +48,7 @@ module SAWScript.Crucible.LLVM.Builtins , llvm_conditional_points_to_at_type , llvm_points_to_internal , llvm_points_to_array_prefix + , llvm_points_to_bitfield , llvm_fresh_pointer , llvm_unsafe_assume_spec , llvm_fresh_var @@ -192,7 +193,7 @@ import SAWScript.Crucible.Common (Sym, SAWCruciblePersonality) import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), nextAllocIndex, PrePost(..)) import qualified SAWScript.Crucible.Common.MethodSpec as MS import SAWScript.Crucible.Common.MethodSpec (SetupValue(..)) -import SAWScript.Crucible.Common.Override hiding (getSymInterface) +import SAWScript.Crucible.Common.Override import qualified SAWScript.Crucible.Common.Setup.Builtins as Setup import qualified SAWScript.Crucible.Common.Setup.Type as Setup @@ -348,7 +349,9 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic = (\(_, setup_value) -> setupValueAsExtCns setup_value) (Map.elems $ method_spec ^. MS.csArgBindings) let reference_input_parameters = mapMaybe - (\(LLVMPointsTo _ _ _ setup_value) -> llvmPointsToValueAsExtCns setup_value) + (\case + LLVMPointsTo _ _ _ setup_value -> llvmPointsToValueAsExtCns setup_value + LLVMPointsToBitfield _ _ _ val -> setupValueAsExtCns val) (method_spec ^. MS.csPreState ^. MS.csPointsTos) let input_parameters = nub $ value_input_parameters ++ reference_input_parameters let pre_free_variables = Map.fromList $ @@ -369,7 +372,9 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic = Nothing -> Nothing let reference_output_parameters = mapMaybe - (\(LLVMPointsTo _ _ _ setup_value) -> llvmPointsToValueAsExtCns setup_value) + (\case + LLVMPointsTo _ _ _ setup_value -> llvmPointsToValueAsExtCns setup_value + LLVMPointsToBitfield _ _ _ val -> setupValueAsExtCns val) (method_spec ^. MS.csPostState ^. MS.csPointsTos) let output_parameters = nub $ filter (isNothing . (Map.!?) pre_free_variables) $ @@ -428,8 +433,11 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic = setup_value_substitute_output_parameter (method_spec ^. MS.csRetValue) extracted_post_state_points_tos <- liftIO $ mapM - (\(LLVMPointsTo x y z value) -> - LLVMPointsTo x y z <$> llvm_points_to_value_substitute_output_parameter value) + (\case + LLVMPointsTo x y z value -> + LLVMPointsTo x y z <$> llvm_points_to_value_substitute_output_parameter value + LLVMPointsToBitfield x y z value -> + LLVMPointsToBitfield x y z <$> setup_value_substitute_output_parameter value) (method_spec ^. MS.csPostState ^. MS.csPointsTos) let extracted_method_spec = method_spec & MS.csRetValue .~ extracted_ret_value & @@ -957,15 +965,22 @@ setupPrePointsTos mspec opts cc env pts mem0 = foldM go mem0 pts go :: MemImpl -> MS.PointsTo (LLVM arch) -> IO MemImpl go mem (LLVMPointsTo _loc cond ptr val) = do ptr' <- resolveSetupVal cc mem env tyenv nameEnv ptr - ptr'' <- case ptr' of - Crucible.LLVMValInt blk off - | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth - -> return (Crucible.LLVMPointer blk off) - _ -> throwMethodSpec mspec "Non-pointer value found in points-to assertion" + ptr'' <- unpackPtrVal ptr' cond' <- mapM (resolveSAWPred cc . ttTerm) cond storePointsToValue opts cc env tyenv nameEnv mem cond' ptr'' val Nothing + go mem (LLVMPointsToBitfield _loc ptr fieldName val) = + do (bfIndex, ptr') <- resolveSetupValBitfield cc mem env tyenv nameEnv ptr fieldName + ptr'' <- unpackPtrVal ptr' + + storePointsToBitfieldValue opts cc env tyenv nameEnv mem ptr'' bfIndex val + + unpackPtrVal :: LLVMVal -> IO (LLVMPtr (Crucible.ArchWidth arch)) + unpackPtrVal (Crucible.LLVMValInt blk off) + | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth + = return (Crucible.LLVMPointer blk off) + unpackPtrVal _ = throwMethodSpec mspec "Non-pointer value found in points-to assertion" -- | Sets up globals (ghost variable), and collects boolean terms -- that should be assumed to be true. @@ -1397,6 +1412,7 @@ setupLLVMCrucibleContext pathSat lm action = crucible_assert_then_assume_enabled <- gets rwCrucibleAssertThenAssume what4HashConsing <- gets rwWhat4HashConsing laxPointerOrdering <- gets rwLaxPointerOrdering + laxLoadsAndStores <- gets rwLaxLoadsAndStores what4Eval <- gets rwWhat4Eval allocSymInitCheck <- gets rwAllocSymInitCheck crucibleTimeout <- gets rwCrucibleTimeout @@ -1405,6 +1421,7 @@ setupLLVMCrucibleContext pathSat lm action = do let ?lc = ctx^.Crucible.llvmTypeCtx let ?memOpts = Crucible.defaultMemOptions { Crucible.laxPointerOrdering = laxPointerOrdering + , Crucible.laxLoadsAndStores = laxLoadsAndStores } let ?intrinsicsOpts = Crucible.defaultIntrinsicsOptions let ?recordLLVMAnnotation = \_ _ _ -> return () @@ -2171,26 +2188,12 @@ llvm_points_to_internal mbCheckType cond (getAllLLVM -> ptr) (getAllLLVM -> val) do cc <- getLLVMCrucibleContext loc <- getW4Position "llvm_points_to" Crucible.llvmPtrWidth (ccLLVMContext cc) $ \wptr -> Crucible.withPtrWidth wptr $ - do let ?lc = ccTypeCtx cc - st <- get - let rs = st ^. Setup.csResolvedState - if st ^. Setup.csPrePost == PreState && MS.testResolved ptr [] rs - then throwCrucibleSetup loc "Multiple points-to preconditions on same pointer" - else Setup.csResolvedState %= MS.markResolved ptr [] + do st <- get let env = MS.csAllocations (st ^. Setup.csMethodSpec) nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec) - ptrTy <- typeOfSetupValue cc env nameEnv ptr - lhsTy <- case ptrTy of - Crucible.PtrType symTy -> - case Crucible.asMemType symTy of - Right lhsTy -> return lhsTy - Left err -> throwCrucibleSetup loc $ unlines - [ "lhs not a valid pointer type: " ++ show ptrTy - , "Details:" - , err - ] - _ -> throwCrucibleSetup loc $ "lhs not a pointer type: " ++ show ptrTy + let path = [] + lhsTy <- llvm_points_to_check_lhs_validity ptr loc path valTy <- typeOfSetupValue cc env nameEnv val case mbCheckType of @@ -2202,6 +2205,82 @@ llvm_points_to_internal mbCheckType cond (getAllLLVM -> ptr) (getAllLLVM -> val) Setup.addPointsTo (LLVMPointsTo loc cond ptr $ ConcreteSizeValue val) +-- | Like 'llvm_points_to_internal', but specifically geared towards the needs +-- of fields within bitfields. In particular, rather than checking +-- 'Crucible.MemType' compatibility against the type that that LHS points to, +-- which corresponds to the overall bitfield type, this checks compatibility +-- against the type of the field /within/ the bitfield, which is often a +-- smaller type. +llvm_points_to_bitfield :: + AllLLVM SetupValue {- ^ lhs pointer -} -> + String {- ^ name of field in bitfield -} -> + AllLLVM SetupValue {- ^ rhs value -} -> + LLVMCrucibleSetupM () +llvm_points_to_bitfield (getAllLLVM -> ptr) fieldName (getAllLLVM -> val) = + LLVMCrucibleSetupM $ + do cc <- getLLVMCrucibleContext + loc <- getW4Position "llvm_points_to_bitfield" + Crucible.llvmPtrWidth (ccLLVMContext cc) $ \wptr -> Crucible.withPtrWidth wptr $ + do st <- get + let env = MS.csAllocations (st ^. Setup.csMethodSpec) + nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec) + + -- NB: Don't use [] for the path here. It's perfectly acceptable to + -- have multiple llvm_points_to_bitfield statements on the same + -- pointer provided that the field names are different, so we use + -- the field name as the path. + let path = [Left fieldName] + _ <- llvm_points_to_check_lhs_validity ptr loc path + + bfIndex <- resolveSetupBitfieldIndexOrFail cc env nameEnv ptr fieldName + let lhsFieldTy = Crucible.IntType $ fromIntegral $ biFieldSize bfIndex + valTy <- typeOfSetupValue cc env nameEnv val + -- Currently, we require the type of the RHS value to precisely match + -- the type of the field within the bitfield. One could imagine + -- having finer-grained control over this (e.g., + -- llvm_points_to_bitfield_at_type or llvm_points_to_bitfield_untyped), + -- but no one has asked for this yet. + checkMemTypeCompatibility loc lhsFieldTy valTy + + Setup.addPointsTo (LLVMPointsToBitfield loc ptr fieldName val) + +-- | Perform a set of validity checks that are shared in common between +-- 'llvm_points_to_internal' and 'llvm_points_to_bitfield': +-- +-- * Check that there are no dupplicate points-to preconditions on the LHS +-- pointer with the supplied path. +-- +-- * Check that the LHS is in fact a valid pointer type. +-- +-- Returns the 'Crucible.MemType' that the LHS points to. +llvm_points_to_check_lhs_validity :: + SetupValue (LLVM arch) {- ^ lhs pointer -} -> + W4.ProgramLoc {- ^ the location in the program -} -> + [Either String Int] {- ^ the path from the pointer to the pointee -} -> + StateT (Setup.CrucibleSetupState (LLVM arch)) TopLevel Crucible.MemType +llvm_points_to_check_lhs_validity ptr loc path = + do cc <- getLLVMCrucibleContext + let ?lc = ccTypeCtx cc + st <- get + let rs = st ^. Setup.csResolvedState + if st ^. Setup.csPrePost == PreState && MS.testResolved ptr path rs + then throwCrucibleSetup loc "Multiple points-to preconditions on same pointer" + else Setup.csResolvedState %= MS.markResolved ptr path + let env = MS.csAllocations (st ^. Setup.csMethodSpec) + nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec) + ptrTy <- typeOfSetupValue cc env nameEnv ptr + case ptrTy of + Crucible.PtrType symTy -> + case Crucible.asMemType symTy of + Right lhsTy -> return lhsTy + Left err -> throwCrucibleSetup loc $ unlines + [ "lhs not a valid pointer type: " ++ show ptrTy + , "Details:" + , err + ] + + _ -> throwCrucibleSetup loc $ "lhs not a pointer type: " ++ show ptrTy + llvm_points_to_array_prefix :: AllLLVM SetupValue -> TypedTerm -> diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index fedada1446..0c38edb90b 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -70,6 +70,7 @@ module SAWScript.Crucible.LLVM.MethodSpecIR -- * PointsTo , LLVMPointsTo(..) , LLVMPointsToValue(..) + , llvmPointsToProgramLoc , ppPointsTo -- * AllocGlobal , LLVMAllocGlobal(..) @@ -359,19 +360,32 @@ ccTypeCtx = view CL.llvmTypeCtx . ccLLVMContext type instance MS.PointsTo (LLVM arch) = LLVMPointsTo arch -data LLVMPointsTo arch = - LLVMPointsTo ProgramLoc (Maybe TypedTerm) (MS.SetupValue (LLVM arch)) (LLVMPointsToValue arch) +data LLVMPointsTo arch + = LLVMPointsTo ProgramLoc (Maybe TypedTerm) (MS.SetupValue (LLVM arch)) (LLVMPointsToValue arch) + -- | A variant of 'LLVMPointsTo' tailored to the @llvm_points_to_bitfield@ + -- command, which doesn't quite fit into the 'LLVMPointsToValue' paradigm. + -- The 'String' represents the name of the field within the bitfield. + | LLVMPointsToBitfield ProgramLoc (MS.SetupValue (LLVM arch)) String (MS.SetupValue (LLVM arch)) data LLVMPointsToValue arch = ConcreteSizeValue (MS.SetupValue (LLVM arch)) | SymbolicSizeValue TypedTerm TypedTerm +-- | Return the 'ProgramLoc' corresponding to an 'LLVMPointsTo' statement. +llvmPointsToProgramLoc :: LLVMPointsTo arch -> ProgramLoc +llvmPointsToProgramLoc (LLVMPointsTo pl _ _ _) = pl +llvmPointsToProgramLoc (LLVMPointsToBitfield pl _ _ _) = pl + ppPointsTo :: LLVMPointsTo arch -> PPL.Doc ann ppPointsTo (LLVMPointsTo _loc cond ptr val) = MS.ppSetupValue ptr PPL.<+> PPL.pretty "points to" PPL.<+> PPL.pretty val PPL.<+> maybe PPL.emptyDoc (\tt -> PPL.pretty "if" PPL.<+> MS.ppTypedTerm tt) cond +ppPointsTo (LLVMPointsToBitfield _loc ptr fieldName val) = + MS.ppSetupValue ptr <> PPL.pretty ("." ++ fieldName) + PPL.<+> PPL.pretty "points to (bitfield)" + PPL.<+> MS.ppSetupValue val instance PPL.Pretty (LLVMPointsTo arch) where pretty = ppPointsTo diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 0a0e2f439e..75cd7a1d6d 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -42,10 +42,12 @@ module SAWScript.Crucible.LLVM.Override , executeSetupCondition , matchArg , matchPointsToValue + , matchPointsToBitfieldValue , assertTermEqualities , methodSpecHandler , valueToSC , storePointsToValue + , storePointsToBitfieldValue , doAllocSymInit , diffMemTypes @@ -90,7 +92,9 @@ import qualified Lang.Crucible.Backend.Online as Crucible import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr(UnitRepr)) import qualified Lang.Crucible.FunctionHandle as Crucible import qualified Lang.Crucible.LLVM.Bytes as Crucible +import qualified Lang.Crucible.LLVM.DataLayout as Crucible import qualified Lang.Crucible.LLVM.MemModel as Crucible +import qualified Lang.Crucible.LLVM.MemType as Crucible import qualified Lang.Crucible.LLVM.Translation as Crucible import qualified Lang.Crucible.Simulator.GlobalState as Crucible import qualified Lang.Crucible.Simulator.OverrideSim as Crucible @@ -213,6 +217,14 @@ ppPointsToAsLLVMVal opts cc sc spec (LLVMPointsTo loc cond ptr val) = do , "Assertion made at:" PP.<+> PP.pretty (W4.plSourceLoc loc) ] +ppPointsToAsLLVMVal opts cc sc spec (LLVMPointsToBitfield loc ptr fieldName val) = do + pretty1 <- ppSetupValueAsLLVMVal opts cc sc spec ptr + let pretty2 = MS.ppSetupValue val + pure $ PP.vcat [ "Pointer (bitfield):" PP.<+> pretty1 <> PP.pretty ("." ++ fieldName) + , "Pointee:" PP.<+> pretty2 + , "Assertion made at:" PP.<+> + PP.pretty (W4.plSourceLoc loc) + ] -- | Create an error stating that the 'LLVMVal' was not equal to the 'SetupValue' notEqual :: @@ -972,14 +984,14 @@ matchPointsTos opts sc cc spec prepost = go False [] go True delayed [] = go False [] delayed -- progress the next points-to in the work queue - go progress delayed (c@(LLVMPointsTo loc _ _ _):cs) = + go progress delayed (c:cs) = do ready <- checkPointsTo c if ready then do err <- learnPointsTo opts sc cc spec prepost c case err of Just msg -> do doc <- ppPointsToAsLLVMVal opts cc sc spec c - failure loc (BadPointerLoad (Right doc) msg) + failure (llvmPointsToProgramLoc c) (BadPointerLoad (Right doc) msg) Nothing -> go True delayed cs else do go progress (c:delayed) cs @@ -987,6 +999,7 @@ matchPointsTos opts sc cc spec prepost = go False [] -- determine if a precondition is ready to be checked checkPointsTo :: PointsTo (LLVM arch) -> OverrideMatcher (LLVM arch) md Bool checkPointsTo (LLVMPointsTo _loc _ p _) = checkSetupValue p + checkPointsTo (LLVMPointsToBitfield _loc p _ _) = checkSetupValue p checkSetupValue :: SetupValue (LLVM arch) -> OverrideMatcher (LLVM arch) md Bool checkSetupValue v = @@ -1424,6 +1437,9 @@ learnPointsTo :: learnPointsTo opts sc cc spec prepost (LLVMPointsTo loc maybe_cond ptr val) = do (_memTy, ptr1) <- resolveSetupValue opts cc sc spec Crucible.PtrRepr ptr matchPointsToValue opts sc cc spec prepost loc maybe_cond ptr1 val +learnPointsTo opts sc cc spec prepost (LLVMPointsToBitfield loc ptr fieldName val) = + do (bfIndex, ptr1) <- resolveSetupValueBitfield opts cc sc spec ptr fieldName + matchPointsToBitfieldValue opts sc cc spec prepost loc ptr1 bfIndex val matchPointsToValue :: forall arch md ann. @@ -1460,17 +1476,7 @@ matchPointsToValue opts sc cc spec prepost loc maybe_cond ptr val = -- then the load type should be determined by the rhs. storTy <- Crucible.toStorableType memTy res <- liftIO $ Crucible.loadRaw sym mem ptr storTy alignment - let summarizeBadLoad = - let dataLayout = Crucible.llvmDataLayout (ccTypeCtx cc) - sz = Crucible.memTypeSize dataLayout memTy - in map (PP.pretty . unwords) - [ [ "When reading through pointer:", show (Crucible.ppPtr ptr) ] - , [ "in the ", stateCond prepost, "of an override" ] - , [ "Tried to read something of size:" - , show (Crucible.bytesToInteger sz) - ] - , [ "And type:", show (Crucible.ppMemType memTy) ] - ] + let badLoadSummary = summarizeBadLoad cc memTy prepost ptr case res of Crucible.NoErr pred_ res_val -> do pred_' <- case maybe_cond of @@ -1479,32 +1485,10 @@ matchPointsToValue opts sc cc spec prepost loc maybe_cond ptr val = liftIO $ W4.impliesPred sym cond' pred_ Nothing -> return pred_ addAssert pred_' $ Crucible.SimError loc $ - Crucible.AssertFailureSimError (show $ PP.vcat $ summarizeBadLoad) "" + Crucible.AssertFailureSimError (show $ PP.vcat badLoadSummary) "" pure Nothing <* matchArg opts sc cc spec prepost res_val memTy val' _ -> do - -- When we have a concrete failure, we do a little more computation to - -- try and find out why. - let (blk, _offset) = Crucible.llvmPointerView ptr - pure $ Just $ PP.vcat . (summarizeBadLoad ++) $ - case W4.asNat blk of - Nothing -> [""] - Just blk' -> - let possibleAllocs = - Crucible.possibleAllocs blk' (Crucible.memImplHeap mem) - in [ PP.pretty $ unwords - [ "Found" - , show (length possibleAllocs) - , "possibly matching allocation(s):" - ] - , bullets '-' (map (PP.viaShow . Crucible.ppSomeAlloc) possibleAllocs) - -- TODO: remove 'viaShow' when crucible switches to prettyprinter - ] - -- This information tends to be overwhelming, but might be useful? - -- We should brainstorm about better ways of presenting it. - -- PP.<$$> PP.text (unwords [ "Here are the details on why reading" - -- , "from each matching write failed" - -- ]) - -- PP.<$$> PP.text (show err) + pure $ Just $ describeConcreteMemoryLoadFailure mem badLoadSummary ptr SymbolicSizeValue expected_arr_tm expected_sz_tm -> do maybe_allocation_array <- liftIO $ @@ -1555,6 +1539,164 @@ matchPointsToValue opts sc cc spec prepost loc maybe_cond ptr val = _ -> return $ Just errMsg +-- | Like 'matchPointsToValue', but specifically geared towards the needs +-- of fields within bitfields. In particular, this performs all of the +-- necessary bit-twiddling on the LHS (a bitfield) to extract the necessary +-- field and match it against the RHS. +matchPointsToBitfieldValue :: + forall arch md ann. + ( ?memOpts :: Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , Crucible.HasPtrWidth (Crucible.ArchWidth arch) + , Crucible.HasLLVMAnn Sym + ) => + Options -> + SharedContext -> + LLVMCrucibleContext arch -> + MS.CrucibleMethodSpecIR (LLVM arch) -> + PrePost -> + W4.ProgramLoc -> + LLVMPtr (Crucible.ArchWidth arch) -> + BitfieldIndex -> + SetupValue (LLVM arch) -> + OverrideMatcher (LLVM arch) md (Maybe (PP.Doc ann)) +matchPointsToBitfieldValue opts sc cc spec prepost loc ptr bfIndex val = + do sym <- Ov.getSymInterface + + mem <- readGlobal $ Crucible.llvmMemVar + $ ccLLVMContext cc + + let alignment = Crucible.noAlignment -- default to byte alignment (FIXME) + + -- Unlike in matchPointsToValue, we compute the MemTy/StorageType not from + -- the RHS value, but from the BitfieldIndex. This is because we need to + -- load the entire bitfield, which can be larger than the size of the RHS + -- value. + let memTy = biBitfieldType bfIndex + storTy <- Crucible.toStorableType memTy + res <- liftIO $ Crucible.loadRaw sym mem ptr storTy alignment + let badLoadSummary = summarizeBadLoad cc memTy prepost ptr + case res of + Crucible.NoErr pred_ res_val -> do + addAssert pred_ $ Crucible.SimError loc $ + Crucible.AssertFailureSimError (show $ PP.vcat badLoadSummary) "" + case res_val of + -- This will only work if: + -- + -- * The bitfield is in fact a bitvector, and + -- * The width of the RHS type is less than the width of the + -- bitfield type. + -- + -- We check these criteria in this case. + Crucible.LLVMValInt bfBlk bfBV + | let bfWidth = W4.bvWidth bfBV + , Some rhsWidth <- mkNatRepr $ fromIntegral $ biFieldSize bfIndex + -> case (testLeq (knownNat @1) rhsWidth, testLeq (incNat rhsWidth) bfWidth) of + (Just LeqProof, Just LeqProof) -> + do -- Here is where we perform the bit-twiddling needed + -- to match the RHS value against the field within the + -- bitfield. We will use this as a running example: + -- + -- struct s { + -- int32_t w; + -- uint8_t x1:1; + -- uint8_t x2:2; + -- uint8_t y:1; + -- int32_t z; + -- }; + -- + -- Let us imagine that we are matching against the + -- `y` field. The bitfield (bfBV) will look something + -- like 0b????Y???, where `Y` denotes the value of the + -- `y` bit. + let -- The offset (in bits) of the field within the + -- bitfield. For `y`, this is 3 (x1's offset is 0 + -- and `x2`'s offset is 1). + bfOffset = biFieldOffset bfIndex + bfOffsetBV = BV.mkBV bfWidth $ fromIntegral bfOffset + + -- Use a logical right shift to make the bits of the + -- field within the bitfield become the least + -- significant bits. In the `y` example, this is + -- tantamount to shifting 0b????Y??? right by `bfOffset` + -- (i.e., 3 bits) to become 0b000????Y. + bfBV' <- liftIO $ W4.bvLshr sym bfBV =<< W4.bvLit sym bfWidth bfOffsetBV + + -- Finally, truncate the bitfield such that only the + -- bits for the field remain. In the `y` example, this + -- means truncating 0b000????Y to `0bY`. + bfBV'' <- liftIO $ W4.bvTrunc sym rhsWidth bfBV' + + -- Match the truncated bitfield against the RHS value. + let res_val' = Crucible.LLVMValInt bfBlk bfBV'' + pure Nothing <* matchArg opts sc cc spec prepost res_val' memTy val + _ -> + fail $ unlines + [ "llvm_points_to_bitfield: RHS value's size must be less then or equal to bitfield's size" + , "Bitvector width: " ++ show bfWidth + , "RHS value width: " ++ show rhsWidth + ] + _ -> fail $ unlines + [ "llvm_points_to_bitfield: The bitfield must be a bitvector" + , "Bitfield value: " ++ show (Crucible.ppTermExpr res_val) + ] + _ -> + -- When we have a concrete failure, we do a little more computation to + -- try and find out why. + pure $ Just $ describeConcreteMemoryLoadFailure mem badLoadSummary ptr + +-- | Give a general summary of why a call to 'Crucible.loadRaw' in +-- @matchPointsTo{Bitfield}Value@ failed. This is used for error-message +-- purposes. +summarizeBadLoad :: + LLVMCrucibleContext arch -> + Crucible.MemType -> + PrePost -> + LLVMPtr wptr -> + [PP.Doc ann] +summarizeBadLoad cc memTy prepost ptr = + let dataLayout = Crucible.llvmDataLayout (ccTypeCtx cc) + sz = Crucible.memTypeSize dataLayout memTy + in map (PP.pretty . unwords) + [ [ "When reading through pointer:", show (Crucible.ppPtr ptr) ] + , [ "in the ", stateCond prepost, "of an override" ] + , [ "Tried to read something of size:" + , show (Crucible.bytesToInteger sz) + ] + , [ "And type:", show (Crucible.ppMemType memTy) ] + ] + +-- | Give a summary of why a call to 'Crucible.loadRaw' in +-- @matchPointsTo{Bitfield}Value@ concretely failed. This is used for +-- error-message purposes. +describeConcreteMemoryLoadFailure :: + Crucible.MemImpl Sym -> + [PP.Doc ann] {- A summary of why the load failed -} -> + LLVMPtr w -> + PP.Doc ann +describeConcreteMemoryLoadFailure mem badLoadSummary ptr = do + let (blk, _offset) = Crucible.llvmPointerView ptr + PP.vcat . (badLoadSummary ++) $ + case W4.asNat blk of + Nothing -> [""] + Just blk' -> + let possibleAllocs = + Crucible.possibleAllocs blk' (Crucible.memImplHeap mem) + in [ PP.pretty $ unwords + [ "Found" + , show (length possibleAllocs) + , "possibly matching allocation(s):" + ] + , bullets '-' (map (PP.viaShow . Crucible.ppSomeAlloc) possibleAllocs) + -- TODO: remove 'viaShow' when crucible switches to prettyprinter + ] + -- This information tends to be overwhelming, but might be useful? + -- We should brainstorm about better ways of presenting it. + -- PP.<$$> PP.text (unwords [ "Here are the details on why reading" + -- , "from each matching write failed" + -- ]) + -- PP.<$$> PP.text (show err) + ------------------------------------------------------------------------ stateCond :: PrePost -> String @@ -1682,14 +1824,22 @@ invalidateMutableAllocs opts sc cc cs = do -- set of (concrete base pointer, size) for each postcondition memory write postPtrs <- Set.fromList <$> catMaybes <$> mapM - (\(LLVMPointsTo _loc _cond ptr val) -> case val of - ConcreteSizeValue val' -> do - (_, Crucible.LLVMPointer blk _) <- resolveSetupValue opts cc sc cs Crucible.PtrRepr ptr - sz <- (return . Crucible.storageTypeSize) - =<< Crucible.toStorableType - =<< typeOfSetupValue cc (MS.csAllocations cs) (MS.csTypeNames cs) val' - return $ Just (W4.asNat blk, sz) - SymbolicSizeValue{} -> return Nothing) + (\case + LLVMPointsTo _loc _cond ptr val -> case val of + ConcreteSizeValue val' -> do + (_, Crucible.LLVMPointer blk _) <- resolveSetupValue opts cc sc cs Crucible.PtrRepr ptr + sz <- (return . Crucible.storageTypeSize) + =<< Crucible.toStorableType + =<< typeOfSetupValue cc (MS.csAllocations cs) (MS.csTypeNames cs) val' + return $ Just (W4.asNat blk, sz) + SymbolicSizeValue{} -> return Nothing + LLVMPointsToBitfield _loc ptr fieldName _val -> do + (bfIndex, Crucible.LLVMPointer blk _) <- + resolveSetupValueBitfield opts cc sc cs ptr fieldName + let memTy = biBitfieldType bfIndex + storTy <- Crucible.toStorableType memTy + let sz = Crucible.storageTypeSize storTy + pure $ Just (W4.asNat blk, sz)) (cs ^. MS.csPostState ^. MS.csPointsTos) -- partition allocations into those overwritten by a postcondition write @@ -1853,6 +2003,19 @@ executePointsTo opts sc cc spec overwritten_allocs (LLVMPointsTo _loc cond ptr v mem' <- liftIO $ storePointsToValue opts cc m tyenv nameEnv mem cond' ptr' val' invalidate_msg writeGlobal memVar mem' +executePointsTo opts sc cc spec _overwritten_allocs (LLVMPointsToBitfield _loc ptr fieldName val) = + do (bfIndex, ptr') <- resolveSetupValueBitfield opts cc sc spec ptr fieldName + let memVar = Crucible.llvmMemVar (ccLLVMContext cc) + mem <- readGlobal memVar + + m <- OM (use setupValueSub) + s <- OM (use termSub) + let tyenv = MS.csAllocations spec + let nameEnv = MS.csTypeNames spec + val' <- liftIO $ instantiateSetupValue sc s val + + mem' <- liftIO $ storePointsToBitfieldValue opts cc m tyenv nameEnv mem ptr' bfIndex val' + writeGlobal memVar mem' storePointsToValue :: ( ?memOpts :: Crucible.MemOptions @@ -1938,6 +2101,170 @@ storePointsToValue opts cc env tyenv nameEnv base_mem maybe_cond ptr val maybe_i Crucible.doConditionalWriteOperation sym base_mem cond store_op Nothing -> store_op base_mem +-- | Like 'storePointsToValue', but specifically geared towards the needs +-- of fields within bitfields. In particular, this performs all of the +-- necessary bit-twiddling on the LHS (a bitfield) to store the RHS value in +-- the right place in the bitfield. +storePointsToBitfieldValue :: + ( ?memOpts :: Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , Crucible.HasPtrWidth (Crucible.ArchWidth arch) + , Crucible.HasLLVMAnn Sym + ) => + Options -> + LLVMCrucibleContext arch -> + Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> + Map AllocIndex (MS.AllocSpec (LLVM arch)) -> + Map AllocIndex (MS.TypeName (LLVM arch)) -> + Crucible.MemImpl Sym -> + LLVMPtr (Crucible.ArchWidth arch) -> + BitfieldIndex -> + SetupValue (LLVM arch) -> + IO (Crucible.MemImpl Sym) +storePointsToBitfieldValue opts cc env tyenv nameEnv base_mem ptr bfIndex val = do + let sym = cc ^. ccBackend + + let alignment = Crucible.noAlignment -- default to byte alignment (FIXME) + + smt_array_memory_model_enabled <- W4.getOpt + =<< W4.getOptionSetting enableSMTArrayMemoryModel (W4.getConfiguration sym) + + -- Unlike in storePointsToValue, we compute the MemTy/StorageType not from + -- the RHS value, but from the BitfieldIndex. This is because we need to + -- load the entire bitfield, which can be larger than the size of the RHS + -- value. + let memTy = biBitfieldType bfIndex + storTy <- Crucible.toStorableType memTy + + case val of + SetupTerm _tm + | smt_array_memory_model_enabled -> + -- See #1540. + fail $ unlines + [ "llvm_points_to_bitfield currently does not work in" + , "combination with the enable_smt_array_memory_model option." + ] + _ -> do + -- Resolve the RHS value as an LLVMVal. + rhsVal <- X.handle (handleException opts) $ + resolveSetupVal cc base_mem env tyenv nameEnv val + + -- Load the bitfield that `ptr` points to. + bfLoadedVal <- Crucible.loadRaw sym base_mem ptr storTy alignment + + -- Assert that the bitfield was loaded successfully. If not, abort. + let badLoadSummary = summarizeBadLoad cc memTy PreState ptr + bfVal <- case bfLoadedVal of + Crucible.NoErr p res_val -> do + let rsn = Crucible.AssertFailureSimError "Error loading bitvector" $ + show badLoadSummary + Crucible.assert sym p rsn + pure res_val + Crucible.Err _p -> + fail $ show $ describeConcreteMemoryLoadFailure base_mem badLoadSummary ptr + + case (bfVal, rhsVal) of + -- This will only work if: + -- + -- * Both the bitfield and the RHS value are bitvectors, and + -- * The width of the RHS type is less than or equal to the width + -- of the bitfield type. + -- + -- We check these criteria in this case. + (Crucible.LLVMValInt bfBlk bfBV, Crucible.LLVMValInt _rhsBlk rhsBV) + -> let bfWidth = W4.bvWidth bfBV + rhsWidth = W4.bvWidth rhsBV in + case testLeq (incNat rhsWidth) bfWidth of + Nothing -> + fail $ unlines + [ "llvm_points_to_bitfield: RHS value's size must be less then or equal to bitfield's size" + , "Bitvector width: " ++ show bfWidth + , "RHS value width: " ++ show rhsWidth + ] + Just LeqProof -> + do -- Here is where we perform the bit-twiddling needed + -- to store the RHS value in the bitfield. We will use + -- this as a running example: + -- + -- struct s { + -- int32_t w; + -- uint8_t x1:1; + -- uint8_t x2:2; + -- uint8_t y:1; + -- int32_t z; + -- }; + -- + -- Let us imagine that we are setting the `y` field to + -- be 1. + let -- The offset (in bits) of the field within the + -- bitfield. For `y`, this is 3 (x1's offset is 0 + -- and `x2`'s offset is 1). + bfOffset = biFieldOffset bfIndex + bfOffsetBV = BV.mkBV bfWidth $ fromIntegral bfOffset + + -- A bitmask with the nth bit (zero-indexed) is + -- set, where n equals the size of the field + -- (in bits) within the bitfield. Since `y` is + -- 1-bit, this would make `fieldBitsBV` be + -- 0b00000010, or 2. + fieldBitsBV = BV.bit' bfWidth $ + fromIntegral $ biFieldSize bfIndex + + -- A bitmask with the (n-1) least significant bits + -- set to 1, where n equals the value of + -- `fieldBitsBV`. For `y`, `leastBitsBV` would be + -- equal to 0b00000001, or 1. + leastBitsBV = BV.sub bfWidth fieldBitsBV (BV.one bfWidth) + + -- A bitmask with the bits corresponding to the + -- field within the bitfield set to 1, and all + -- other bits are set to 0. For `y`, `bitmaskBV` + -- would be equal to 0b00001000, or 8. + bitmaskBV = BV.shl bfWidth leastBitsBV $ fromIntegral bfOffset + + -- A bitmask with the bits corresponding to the + -- field within the bitfield set to 0, and all + -- other bits are set to 1. For `y`, `compBitmaskBV` + -- would be equal to 0b11110111, or 247. + compBitmaskBV = BV.complement bfWidth bitmaskBV + compBitmaskSymBV <- W4.bvLit sym bfWidth compBitmaskBV + + -- Clear all of the bits in the bitfield + -- corresponding to the field, leaving all other bits + -- unchanged. If the original bitvector was 0b????????, + -- then `bfBV'` is 0b????0???. + bfBV' <- W4.bvAndBits sym bfBV compBitmaskSymBV + + -- Zero-extend the RHS value to be the same width as + -- the bitfield. In our running example, we + -- sign-extend 0b1 (1) to 0b00000001. + rhsBV' <- W4.bvZext sym bfWidth rhsBV + + -- Left-shift the zero-extended RHS value such that + -- its contents are in the same position as the field + -- in the bitfield. In our running example, `rhsBV''` + -- is 0b00001000, or 8. + rhsBV'' <- W4.bvShl sym rhsBV' =<< W4.bvLit sym bfWidth bfOffsetBV + + -- Finally, set the bits in the bitfield to the RHS + -- value with a bitwise-or operation. In our running + -- example, `bfBV''` is 0b????1???. + bfBV'' <- W4.bvOrBits sym bfBV' rhsBV'' + + -- Store the bitfield's value back to memory. + -- + -- Bear in mind that this whole process is repeated once per + -- field, even if the fields all reside within the same + -- bitfield. See #1541 for an alternative approach that + -- would optimize this further. + let bfVal' = Crucible.LLVMValInt bfBlk bfBV'' + Crucible.storeConstRaw sym base_mem ptr storTy alignment bfVal' + _ -> fail $ unlines + [ "llvm_points_to_bitfield: Both the bitfield and RHS value must be bitvectors" + , "Bitfield value: " ++ show (Crucible.ppTermExpr bfVal) + , "RHS value: " ++ show (MS.ppSetupValue val) + ] + ------------------------------------------------------------------------ @@ -2045,5 +2372,46 @@ resolveSetupValue opts cc sc spec tp sval = val <- liftIO $ Crucible.unpackMemValue sym tp lval return (memTy, val) +-- | Like 'resolveSetupValueLLVM', but specifically geared towards the needs +-- of fields within bitfields. See the Haddocks for 'resolveSetupValBitfield' +-- for the salient details. +resolveSetupValueBitfieldLLVM :: + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + Options -> + LLVMCrucibleContext arch -> + SharedContext -> + MS.CrucibleMethodSpecIR (LLVM arch) -> + SetupValue (LLVM arch) -> + String -> + OverrideMatcher (LLVM arch) md (BitfieldIndex, LLVMVal) +resolveSetupValueBitfieldLLVM opts cc sc spec sval fieldName = + do m <- OM (use setupValueSub) + s <- OM (use termSub) + mem <- readGlobal (Crucible.llvmMemVar (ccLLVMContext cc)) + let tyenv = MS.csAllocations spec + nameEnv = MS.csTypeNames spec + sval' <- liftIO $ instantiateSetupValue sc s sval + liftIO $ resolveSetupValBitfield cc mem m tyenv nameEnv sval' fieldName `X.catch` handleException opts + +-- | Like 'resolveSetupValue', but specifically geared towards the needs +-- of fields within bitfields. Note that the LHS value must be a pointer, so +-- there is no need to pass a 'Crucible.TypeRepr' here. Moreover, the second +-- return value is always specialized to 'LLVMPtr'. See also the Haddocks for +-- 'resolveSetupValueBitfieldLLVM' for other differences. +resolveSetupValueBitfield :: + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + Options -> + LLVMCrucibleContext arch -> + SharedContext -> + MS.CrucibleMethodSpecIR (LLVM arch) -> + SetupValue (LLVM arch) -> + String -> + OverrideMatcher (LLVM arch) md (BitfieldIndex, LLVMPtr (Crucible.ArchWidth arch)) +resolveSetupValueBitfield opts cc sc spec sval fieldName = + do (bfIndex, lval) <- resolveSetupValueBitfieldLLVM opts cc sc spec sval fieldName + sym <- Ov.getSymInterface + val <- liftIO $ Crucible.unpackMemValue sym Crucible.PtrRepr lval + pure (bfIndex, val) + enableSMTArrayMemoryModel :: W4.ConfigOption W4.BaseBoolType enableSMTArrayMemoryModel = (W4.configOption W4.knownRepr "smt-array-memory-model") diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index 7aa00ad0e8..ebcbede425 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -18,12 +18,16 @@ Stability : provisional module SAWScript.Crucible.LLVM.ResolveSetupValue ( LLVMVal, LLVMPtr , resolveSetupVal + , resolveSetupValBitfield , typeOfSetupValue , resolveTypedTerm , resolveSAWPred , resolveSAWSymBV , resolveSetupFieldIndex , resolveSetupFieldIndexOrFail + , BitfieldIndex(..) + , resolveSetupBitfieldIndex + , resolveSetupBitfieldIndexOrFail , resolveSetupElemIndexOrFail , equalValsPred , memArrayToSawCoreTerm @@ -42,6 +46,7 @@ import Data.Map (Map) import qualified Data.Map as Map import qualified Data.Set as Set import qualified Data.Vector as V +import Data.Word (Word64) import Numeric.Natural import qualified Text.LLVM.AST as L @@ -58,6 +63,7 @@ import qualified What4.Interface as W4 import qualified Lang.Crucible.LLVM.Bytes as Crucible import qualified Lang.Crucible.LLVM.MemModel as Crucible +import qualified Lang.Crucible.LLVM.MemType as Crucible import qualified Lang.Crucible.LLVM.Translation as Crucible import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible @@ -71,7 +77,7 @@ import Verifier.SAW.Name import Verifier.SAW.TypedTerm import Verifier.SAW.Simulator.What4 import Verifier.SAW.Simulator.What4.ReturnTrip -import Text.LLVM.DebugUtils as L +import qualified Text.LLVM.DebugUtils as L import SAWScript.Crucible.Common (Sym, sawCoreState) import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), SetupValue(..), ppTypedTermType) @@ -96,17 +102,17 @@ resolveSetupValueInfo cc env nameEnv v = case v of SetupGlobal _ name -> case lookup (L.Symbol name) globalTys of - Just (L.Alias alias) -> L.Pointer (guessAliasInfo mdMap alias) + Just (L.Alias alias) -> L.Pointer (L.guessAliasInfo mdMap alias) _ -> L.Unknown SetupVar i | Just alias <- Map.lookup i nameEnv - -> L.Pointer (guessAliasInfo mdMap alias) + -> L.Pointer (L.guessAliasInfo mdMap alias) SetupField () a n -> fromMaybe L.Unknown $ do L.Pointer (L.Structure xs) <- return (resolveSetupValueInfo cc env nameEnv a) - listToMaybe [L.Pointer i | (n',_,i) <- xs, n == n' ] + listToMaybe [L.Pointer i | L.StructFieldInfo{L.sfiName = n', L.sfiInfo = i} <- xs, n == n' ] _ -> L.Unknown where @@ -125,7 +131,7 @@ resolveSetupFieldIndex :: resolveSetupFieldIndex cc env nameEnv v n = case resolveSetupValueInfo cc env nameEnv v of L.Pointer (L.Structure xs) -> - case [o | (n',o,_) <- xs, n == n' ] of + case [o | L.StructFieldInfo{L.sfiName = n', L.sfiOffset = o} <- xs, n == n' ] of [] -> Nothing o:_ -> do Crucible.PtrType symTy <- typeOfSetupValue cc env nameEnv v @@ -158,7 +164,133 @@ resolveSetupFieldIndexOrFail cc env nameEnv v n = L.Pointer (L.Structure xs) -> unlines $ [ msg , "The following field names were found for this struct:" - ] ++ map ("- "++) [n' | (n', _, _) <- xs] + ] ++ map ("- "++) [n' | L.StructFieldInfo{L.sfiName = n'} <- xs] + _ -> unlines [msg, "No field names were found for this struct"] + +-- | Information about a field within a bitfield in a struct. For example, +-- given the following C struct: +-- +-- @ +-- struct s { +-- int32_t w; +-- uint8_t x1:1; +-- uint8_t x2:2; +-- uint8_t y:1; +-- int32_t z; +-- }; +-- @ +-- +-- The 'BitfieldIndex'es for @x1@, @x2@, and @y@ are as follows: +-- +-- @ +-- -- x1 +-- 'BitfieldIndex' +-- { 'biFieldSize' = 1 +-- , 'biFieldOffset' = 0 +-- , 'biBitfieldIndex' = 4 +-- , 'biBitfieldType' = i8 +-- } +-- +-- -- x2 +-- 'BitfieldIndex' +-- { 'biFieldSize' = 2 +-- , 'biFieldOffset' = 1 +-- , 'biBitfieldIndex' = 4 +-- , 'biBitfieldType' = i8 +-- } +-- +-- -- y +-- 'BitfieldIndex' +-- { 'biFieldSize' = 1 +-- , 'biFieldOffset' = 3 +-- , 'biBitfieldIndex' = 4 +-- , 'biBitfieldType' = i8 +-- } +-- @ +-- +-- Note that the 'biFieldSize's and 'biFieldOffset's are specific to each +-- individual field, while the 'biBitfieldIndex'es and 'biBitfieldType's are +-- all the same, as the latter two all describe the same bitfield. +data BitfieldIndex = BitfieldIndex + { biFieldSize :: Word64 + -- ^ The size (in bits) of the field within the bitfield. + , biFieldOffset :: Word64 + -- ^ The offset (in bits) of the field from the start of the bitfield. + , biBitfieldIndex :: Int + -- ^ The struct field index corresponding to the overall bitfield, where + -- the index represents the number of bytes the bitfield is from the + -- start of the struct. + , biBitfieldType :: Crucible.MemType + -- ^ The 'Crucible.MemType' of the overall bitfield. + } deriving Show + +-- | Returns @'Just' bi@ if SAW is able to find a field within a bitfield with +-- the supplied name in the LLVM debug metadata. Returns 'Nothing' otherwise. +resolveSetupBitfieldIndex :: + LLVMCrucibleContext arch {- ^ crucible context -} -> + Map AllocIndex LLVMAllocSpec {- ^ allocation types -} -> + Map AllocIndex Crucible.Ident {- ^ allocation type names -} -> + SetupValue (LLVM arch) {- ^ pointer to struct -} -> + String {- ^ field name -} -> + Maybe BitfieldIndex {- ^ information about bitfield -} +resolveSetupBitfieldIndex cc env nameEnv v n = + case resolveSetupValueInfo cc env nameEnv v of + L.Pointer (L.Structure xs) + | (fieldOffsetStartingFromStruct, bfInfo):_ <- + [ (fieldOffsetStartingFromStruct, bfInfo) + | L.StructFieldInfo + { L.sfiName = n' + , L.sfiOffset = fieldOffsetStartingFromStruct + , L.sfiBitfield = Just bfInfo + } <- xs + , n == n' + ] + -> do Crucible.PtrType symTy <- typeOfSetupValue cc env nameEnv v + Crucible.StructType si <- + let ?lc = lc + in either (\_ -> Nothing) Just $ Crucible.asMemType symTy + bfIndex <- + V.findIndex (\fi -> Crucible.bytesToBits (Crucible.fiOffset fi) + == fromIntegral (L.biBitfieldOffset bfInfo)) + (Crucible.siFields si) + let bfType = Crucible.fiType $ Crucible.siFields si V.! bfIndex + fieldOffsetStartingFromBitfield = + fieldOffsetStartingFromStruct - L.biBitfieldOffset bfInfo + pure $ BitfieldIndex { biFieldSize = L.biFieldSize bfInfo + , biFieldOffset = fieldOffsetStartingFromBitfield + , biBitfieldIndex = bfIndex + , biBitfieldType = bfType + } + + _ -> Nothing + where + lc = ccTypeCtx cc + +-- | Like 'resolveSetupBitfieldIndex', but if SAW cannot find the supplied +-- name, fail instead of returning 'Nothing'. +resolveSetupBitfieldIndexOrFail :: + Fail.MonadFail m => + LLVMCrucibleContext arch {- ^ crucible context -} -> + Map AllocIndex LLVMAllocSpec {- ^ allocation types -} -> + Map AllocIndex Crucible.Ident {- ^ allocation type names -} -> + SetupValue (LLVM arch) {- ^ pointer to struct -} -> + String {- ^ field name -} -> + m BitfieldIndex {- ^ field index -} +resolveSetupBitfieldIndexOrFail cc env nameEnv v n = + case resolveSetupBitfieldIndex cc env nameEnv v n of + Just i -> pure i + Nothing -> + let msg = "Unable to resolve field name: " ++ show n + in + fail $ + -- Show the user what fields were available (if any) + case resolveSetupValueInfo cc env nameEnv v of + L.Pointer (L.Structure xs) -> unlines $ + [ msg + , "The following bitfield names were found for this struct:" + ] ++ map ("- "++) [n' | L.StructFieldInfo{ L.sfiName = n' + , L.sfiBitfield = Just{} + } <- xs] _ -> unlines [msg, "No field names were found for this struct"] typeOfSetupValue :: @@ -366,6 +498,42 @@ resolveSetupVal cc mem env tyenv nameEnv val = do lc = ccTypeCtx cc dl = Crucible.llvmDataLayout lc +-- | Like 'resolveSetupVal', but specifically geared towards the needs of +-- fields within bitfields. This is very similar to calling 'resolveSetupVal' +-- on a 'SetupField', instead of computing an offset into the struct based off +-- of the /field's/ offset from the beginning of the struct, this computes an +-- offset based off of the overall /bitfield's/ offset from the beginning of +-- the struct. This is important because in order to impose conditions on +-- fields within bitfields, we must load/store the entire bitfield. The field's +-- offset may be larger than the bitfield's offset, so the former offset is not +-- suited for this purpose. +-- +-- In addition to returning the resolved 'LLVMVal', this also returns the +-- 'BitfieldIndex' for the field within the bitfield. This ends up being useful +-- for call sites to this function so that they do not have to recompute it. +resolveSetupValBitfield :: + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + LLVMCrucibleContext arch -> + Crucible.MemImpl Sym -> + Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> + Map AllocIndex LLVMAllocSpec -> + Map AllocIndex Crucible.Ident -> + SetupValue (LLVM arch) -> + String -> + IO (BitfieldIndex, LLVMVal) +resolveSetupValBitfield cc mem env tyenv nameEnv val fieldName = do + do let sym = cc^.ccBackend + lval <- resolveSetupVal cc mem env tyenv nameEnv val + bfIndex <- resolveSetupBitfieldIndexOrFail cc tyenv nameEnv val fieldName + delta <- resolveSetupElemIndexOrFail cc tyenv nameEnv val (biBitfieldIndex bfIndex) + offsetLval <- case lval of + Crucible.LLVMValInt blk off -> + do deltaBV <- W4.bvLit sym (W4.bvWidth off) (Crucible.bytesToBV (W4.bvWidth off) delta) + off' <- W4.bvAdd sym off deltaBV + return (Crucible.LLVMValInt blk off') + _ -> fail "resolveSetupValBitfield: expected a pointer value" + pure (bfIndex, offsetLval) + resolveTypedTerm :: (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => LLVMCrucibleContext arch -> diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 123f1d576f..40dc93da45 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -297,8 +297,11 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se | Just Refl <- testEquality (C.LLVM.X86Repr $ knownNat @64) . C.LLVM.llvmArch $ modTrans llvmModule ^. C.LLVM.transContext = do start <- io getCurrentTime + laxLoadsAndStores <- gets rwLaxLoadsAndStores let ?ptrWidth = knownNat @64 let ?memOpts = C.LLVM.defaultMemOptions + { C.LLVM.laxLoadsAndStores = laxLoadsAndStores + } let ?recordLLVMAnnotation = \_ _ _ -> return () sc <- getSharedContext opts <- getOptions @@ -766,6 +769,13 @@ assumePointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tptval) = do cond' <- liftIO $ mapM (resolveSAWPred cc . ttTerm) cond mem' <- liftIO $ LO.storePointsToValue opts cc env tyenv nameEnv mem cond' ptr tptval Nothing x86Mem .= mem' +assumePointsTo env tyenv nameEnv (LLVMPointsToBitfield _ tptr fieldName tptval) = do + opts <- use x86Options + cc <- use x86CrucibleContext + mem <- use x86Mem + (bfIndex, ptr) <- resolvePtrSetupValueBitfield env tyenv nameEnv tptr fieldName + mem' <- liftIO $ LO.storePointsToBitfieldValue opts cc env tyenv nameEnv mem ptr bfIndex tptval + x86Mem .= mem' resolvePtrSetupValue :: X86Constraints => @@ -792,6 +802,42 @@ resolvePtrSetupValue env tyenv nameEnv tptr = do _ -> liftIO $ C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64) =<< resolveSetupVal cc mem env tyenv nameEnv tptr +-- | Like 'resolvePtrSetupValue', but specifically geared towards the needs of +-- fields within bitfields. In addition to returning the resolved 'Ptr', this +-- also returns the 'BitfieldIndex' for the field within the bitfield. This +-- ends up being useful for call sites to this function so that they do not +-- have to recompute it. +resolvePtrSetupValueBitfield :: + X86Constraints => + Map MS.AllocIndex Ptr -> + Map MS.AllocIndex LLVMAllocSpec -> + Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} -> + MS.SetupValue LLVM -> + String -> + X86Sim (BitfieldIndex, Ptr) +resolvePtrSetupValueBitfield env tyenv nameEnv tptr fieldName = do + sym <- use x86Sym + cc <- use x86CrucibleContext + mem <- use x86Mem + -- symTab <- use x86ElfSymtab + -- base <- use x86GlobalBase + case tptr of + -- TODO RGS: What should we do about the SetupGlobal case? + {- + MS.SetupGlobal () nm -> case + (Vector.!? 0) + . Vector.filter (\e -> Elf.steName e == encodeUtf8 (Text.pack nm)) + $ Elf.symtabEntries symTab of + Nothing -> throwX86 $ mconcat ["Global symbol \"", nm, "\" not found"] + Just entry -> do + let addr = fromIntegral $ Elf.steValue entry + liftIO $ C.LLVM.doPtrAddOffset sym mem base =<< W4.bvLit sym knownNat (BV.mkBV knownNat addr) + -} + _ -> do + (bfIndex, lval) <- liftIO $ resolveSetupValBitfield cc mem env tyenv nameEnv tptr fieldName + val <- liftIO $ C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64) lval + pure (bfIndex, val) + -- | Write each SetupValue passed to llvm_execute_func to the appropriate -- x86_64 register from the calling convention. setArgs :: @@ -950,6 +996,20 @@ assertPointsTo env tyenv nameEnv pointsTo@(LLVMPointsTo loc cond tptr tptval) = doc <- LO.ppPointsToAsLLVMVal opts cc sc ms pointsTo O.failure loc (O.BadPointerLoad (Right doc) msg) Nothing -> pure () +assertPointsTo env tyenv nameEnv pointsTo@(LLVMPointsToBitfield loc tptr fieldName tptval) = do + opts <- use x86Options + sc <- use x86SharedContext + cc <- use x86CrucibleContext + ms <- use x86MethodSpec + + (bfIndex, ptr) <- resolvePtrSetupValueBitfield env tyenv nameEnv tptr fieldName + pure $ do + err <- LO.matchPointsToBitfieldValue opts sc cc ms MS.PostState loc ptr bfIndex tptval + case err of + Just msg -> do + doc <- LO.ppPointsToAsLLVMVal opts cc sc ms pointsTo + O.failure loc (O.BadPointerLoad (Right doc) msg) + Nothing -> pure () -- | Gather and run the solver on goals from the simulator. checkGoals :: diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index a13a0851b5..5621dd90f2 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -481,6 +481,7 @@ buildTopLevelEnv proxy opts = , rwProfilingFile = Nothing , rwLaxArith = False , rwLaxPointerOrdering = False + , rwLaxLoadsAndStores = False , rwDebugIntrinsics = True , rwWhat4HashConsing = False , rwWhat4HashConsingX86 = False @@ -569,6 +570,16 @@ disable_lax_pointer_ordering = do rw <- getTopLevelRW putTopLevelRW rw { rwLaxPointerOrdering = False } +enable_lax_loads_and_stores :: TopLevel () +enable_lax_loads_and_stores = do + rw <- getTopLevelRW + putTopLevelRW rw { rwLaxLoadsAndStores = True } + +disable_lax_loads_and_stores :: TopLevel () +disable_lax_loads_and_stores = do + rw <- getTopLevelRW + putTopLevelRW rw { rwLaxLoadsAndStores = False } + enable_debug_intrinsics :: TopLevel () enable_debug_intrinsics = do rw <- getTopLevelRW @@ -845,6 +856,16 @@ primitives = Map.fromList Current [ "Disable lax rules for pointer ordering comparisons in Crucible." ] + , prim "enable_lax_loads_and_stores" "TopLevel ()" + (pureVal enable_lax_loads_and_stores) + Current + [ "Enable relaxed validity checking for memory loads and stores in Crucible." ] + + , prim "disable_lax_loads_and_stores" "TopLevel ()" + (pureVal disable_lax_loads_and_stores) + Current + [ "Disable relaxed validity checking for memory loads and stores in Crucible." ] + , prim "enable_debug_intrinsics" "TopLevel ()" (pureVal enable_debug_intrinsics) Current @@ -2506,6 +2527,20 @@ primitives = Map.fromList Experimental [ "Legacy alternative name for `llvm_points_to_array_prefix`." ] + , prim "llvm_points_to_bitfield" "SetupValue -> String -> SetupValue -> LLVMSetup ()" + (pureVal (llvm_points_to_bitfield)) + Experimental + [ "A variant of `llvm_points_to` that is meant to be used on struct fields" + , "that reside within bitfields. `llvm_points_to_bitfield ptr fieldName rhs`" + , "should be used instead of `llvm_points_to (llvm_field ptr fieldName) rhs`," + , "as the latter will not behave as one would expect for technical reasons." + , "" + , "This command should only be used in combination with" + , "`enable_lax_loads_and_stores`, as this option relaxes some assumptions" + , "about the memory model that are crucial to how `llvm_points_to_bitfield`" + , "operates." + ] + , prim "llvm_equal" "SetupValue -> SetupValue -> LLVMSetup ()" (pureVal llvm_equal) Current diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index c3007ad64f..8bc714696f 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -439,6 +439,7 @@ data TopLevelRW = , rwCrucibleAssertThenAssume :: Bool , rwProfilingFile :: Maybe FilePath , rwLaxArith :: Bool + , rwLaxLoadsAndStores :: Bool , rwLaxPointerOrdering :: Bool , rwDebugIntrinsics :: Bool