From cbc97c011a0890d3f62b26f26c5a5744561d5277 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 2 Nov 2021 11:57:08 -0400 Subject: [PATCH 1/3] Add `llvm_points_to_bitfield` and `enable_lax_loads_and_stores` This adds support for writing specifications that talk about bitfields in LLVM code by way of the new `llvm_points_to_bitfield` command. Broadly speaking, `llvm_points_to_bitfield ptr fieldName rhs` is like `llvm_points_to (llvm_field ptr fieldName) rhs`, except that `fieldName` is required to be the name of a field within a bitfield. The salient details are: * LLVM bitcode itself does not a built-in concept of bitfields, but LLVM's debug metadata does. Support for retrieving bitfield-related metadata was added to `llvm-pretty` in elliottt/llvm-pretty#90, so this patch bumps the `llvm-pretty` submodule to incorporate it. This patch also updates the `crucible` submodule to incorporate corresponding changes in GaloisInc/crucible#936. * The `LLVMPointsTo` data type now has a new `LLVMPointsToBitfield` data constructor that stores all of the necessary information related to the `llvm_points_to_bitfield` command. As a result, the changes in this patch are fairly insulated from the rest of SAW, as most of the new code involves adding additional cases to handle `LLVMPointsToBitfield`. * Two of the key new functions are `storePointsToBitfieldValue` and `matchPointsToBitfieldValue`, which implement the behavior of `llvm_points_to_bitfield` in pre- and post-conditions. These functions implement the necessary bit-twiddling to store values in and retrieve values out of bitfield. I have left extensive comments in each function describing how all of this works. * Accompanying `llvm_points_to_bitfield` is a new set of `{enable,disable}_lax_loads_and_stores` command, which toggles the Crucible-side option of the same name. When `enable_lax_loads_and_stores` is on, reading from uninitialized memory will return a symbolic value rather than failing outright. This is essential to be able to deal with LLVM bitcode involving bitfields, as reading a field from a bitfield involves reading the entire bitfield at once, which may include parts of the struct that have not been initialized yet. * There are various `test_bitfield_*` test cases under `intTests` to test examples of bitfield-related specifications that should and should not verify. * I have also updated `saw-remote-api` and `saw-client` to handle bitfields as well, along with a Python-specific test case. Fixes #1461. --- CHANGES.md | 8 + deps/crucible | 2 +- deps/llvm-pretty | 2 +- doc/manual/manual.md | 97 ++++ intTests/test_bitfield_basic/Makefile | 11 + intTests/test_bitfield_basic/test.bc | Bin 0 -> 4836 bytes intTests/test_bitfield_basic/test.c | 34 ++ intTests/test_bitfield_basic/test.saw | 55 +++ intTests/test_bitfield_basic/test.sh | 5 + .../Makefile | 11 + .../test_bitfield_duplicate_points_to/test.bc | Bin 0 -> 3148 bytes .../test_bitfield_duplicate_points_to/test.c | 14 + .../test.saw | 15 + .../test_bitfield_duplicate_points_to/test.sh | 5 + intTests/test_bitfield_smt_array/Makefile | 11 + intTests/test_bitfield_smt_array/test.bc | Bin 0 -> 4840 bytes intTests/test_bitfield_smt_array/test.c | 34 ++ intTests/test_bitfield_smt_array/test.saw | 55 +++ intTests/test_bitfield_smt_array/test.sh | 7 + intTests/test_bitfield_wrong_type/Makefile | 11 + intTests/test_bitfield_wrong_type/test.bc | Bin 0 -> 3236 bytes intTests/test_bitfield_wrong_type/test.c | 14 + intTests/test_bitfield_wrong_type/test.saw | 14 + intTests/test_bitfield_wrong_type/test.sh | 5 + intTests/test_bitfield_x86/Makefile | 17 + intTests/test_bitfield_x86/test.bc | Bin 0 -> 5012 bytes intTests/test_bitfield_x86/test.c | 38 ++ intTests/test_bitfield_x86/test.exe | Bin 0 -> 18136 bytes intTests/test_bitfield_x86/test.o | Bin 0 -> 4784 bytes intTests/test_bitfield_x86/test.saw | 50 ++ intTests/test_bitfield_x86/test.sh | 5 + saw-remote-api/CHANGELOG.md | 10 + saw-remote-api/docs/SAW.rst | 2 +- saw-remote-api/python/CHANGELOG.md | 6 + saw-remote-api/python/saw_client/crucible.py | 37 ++ saw-remote-api/python/saw_client/option.py | 6 + .../saw/test-files/llvm_points_to_bitfield.bc | Bin 0 -> 4792 bytes .../saw/test-files/llvm_points_to_bitfield.c | 34 ++ .../tests/saw/test_llvm_points_to_bitfield.py | 114 +++++ saw-remote-api/src/SAWServer.hs | 7 + saw-remote-api/src/SAWServer/Data/Contract.hs | 19 + .../src/SAWServer/JVMCrucibleSetup.hs | 11 +- .../src/SAWServer/LLVMCrucibleSetup.hs | 16 +- saw-remote-api/src/SAWServer/SetOption.hs | 5 + src/SAWScript/Crucible/LLVM/Builtins.hs | 133 ++++- src/SAWScript/Crucible/LLVM/MethodSpecIR.hs | 18 +- src/SAWScript/Crucible/LLVM/Override.hs | 460 ++++++++++++++++-- .../Crucible/LLVM/ResolveSetupValue.hs | 181 ++++++- src/SAWScript/Crucible/LLVM/X86.hs | 60 +++ src/SAWScript/Interpreter.hs | 35 ++ src/SAWScript/Value.hs | 1 + 51 files changed, 1589 insertions(+), 86 deletions(-) create mode 100644 intTests/test_bitfield_basic/Makefile create mode 100644 intTests/test_bitfield_basic/test.bc create mode 100644 intTests/test_bitfield_basic/test.c create mode 100644 intTests/test_bitfield_basic/test.saw create mode 100755 intTests/test_bitfield_basic/test.sh create mode 100644 intTests/test_bitfield_duplicate_points_to/Makefile create mode 100644 intTests/test_bitfield_duplicate_points_to/test.bc create mode 100644 intTests/test_bitfield_duplicate_points_to/test.c create mode 100644 intTests/test_bitfield_duplicate_points_to/test.saw create mode 100755 intTests/test_bitfield_duplicate_points_to/test.sh create mode 100644 intTests/test_bitfield_smt_array/Makefile create mode 100644 intTests/test_bitfield_smt_array/test.bc create mode 100644 intTests/test_bitfield_smt_array/test.c create mode 100644 intTests/test_bitfield_smt_array/test.saw create mode 100755 intTests/test_bitfield_smt_array/test.sh create mode 100644 intTests/test_bitfield_wrong_type/Makefile create mode 100644 intTests/test_bitfield_wrong_type/test.bc create mode 100644 intTests/test_bitfield_wrong_type/test.c create mode 100644 intTests/test_bitfield_wrong_type/test.saw create mode 100755 intTests/test_bitfield_wrong_type/test.sh create mode 100644 intTests/test_bitfield_x86/Makefile create mode 100644 intTests/test_bitfield_x86/test.bc create mode 100644 intTests/test_bitfield_x86/test.c create mode 100755 intTests/test_bitfield_x86/test.exe create mode 100644 intTests/test_bitfield_x86/test.o create mode 100644 intTests/test_bitfield_x86/test.saw create mode 100755 intTests/test_bitfield_x86/test.sh create mode 100644 saw-remote-api/python/tests/saw/test-files/llvm_points_to_bitfield.bc create mode 100644 saw-remote-api/python/tests/saw/test-files/llvm_points_to_bitfield.c create mode 100644 saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py 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 0000000000000000000000000000000000000000..67499f17bb563df40bc6756e486bab751c60fa28 GIT binary patch literal 4836 zcmbVQe^498z2DOb-GPO4HcBjolYBBZqj8NngoA~FL_)+-8ZwbnPoF!@8%`3!QVc>! z0tC)$PDsh&R_-XNJE0wCMx^|a{+JdwG|z3)j)Yu?dXzludNP#f@q+;qzmDU_YtlS- z;2$ix?f3S(yWiW-_xsuJu4uPsu05z<>}YB>9$aqd@y`I&@vk7-Y;;rZ!jU*>)}2X;?# z2t5GOywg$6b-yV8#?Gk(R4a+elxAD!SCd;3Q=N=6ET3ZuExYrnt-Cvak$4HoPVN+K z-Ex6TGizt;zOQqpv4>_Z3X1d>6^)voH_M!98`wOoMd%F3>hra?{|to)qH+_-DaQw* z)JRGSX{k{`dfrElM5WOn6*5sF9~p8`CmirDHBCs-6gBE2!=lvWlY(g~g7QXo!DYBe zaC1ienvp#p(_fsdykTT7$MlN=I~&tOFACGt(1a91bT}mieG=G=Mx{uQ8Z}WP2#+DS zg-LeJWmrUp)k*dOn3`l4Gwjl&em2H#P9Gm~P{TfQ$RuHdKJtV~8c0jSDXHn46yc~* zD}_{OR)1}>@^V(62W!|u<)V?jLFhM)(8E!w$tjKcsHl$|rKtfy3QbTMyj1vTar#vw zd-d;4pO7LJYPjH>e**|nY2^Msxw@=h6b-9Jc8M^+lHUKD#f*=nrJzjpqQn`I$_ zdBU)m2Im{*30?{c(uj!?-+&sgXP7U1NRWnUYIKtT3sxF&it5wLm{yckW=gBXM;5G% zj8g#Lo&es#_CZw%>ja~$N{AB-15H#_i&5MzYe~nOL}>tm3n6}kdfpcg2c^*kq2l_y z;-fSL^*TolBWjeVLTM_@QGG}q3Q_}wcdRT901^mPBux!jslJp7YTTSxtcetmb%3Ly z^NL#{HOf#!#fgR9HyJ7XmiXx>ME2oY!B2EpOD%x(q%1$(DEGE%Wx~8M5`A zcx!@e$**gM1nPv3I)Jx1bwI?-3<}hci5j|H24;svsf(5dw7^ekWFofr*1GD}lIr&v z)lHss&jA}J*?ghC>S8Yz^NCCGLCW4dXK$V;)aP=R({{@^*>XBp45PJ-1$jLjXhv^&T!Gi-Z1K~W%XYnaK6eL z_3JLhkr(5Ze6D5M-Ubf2GuygqZyASXF8Rv}Kq?KxdSJgm(wK-nyTYh$W>nXms*m}a z>}8u_b$R>3vi=$@z@clIjN-(ax$DrC-{dS1 ztm$0+g8g9LesJ7=5KzzCA3-A=LbrfZA%lank1KWMA+v+4i6vit`BF!kF?F{#nA^Xe zGJa>=HABAix#+2>tL-fNTx!1!QIDJHc7}!nG~x|M_Ic`k{e9m0P}tKSiPU%Wdj|Ww zfk?RC;qn~!2abUZANTh5)`wlgbzx7)AB@!d1Cb*zHC&Gkbh-VJ9>2G@yUXng`#qjs zSKt^or0^>AM-_I7yPgU7fh0zLgD&9KMk3U!73 zqu%<#aHzi5@2>Cd9qOxV;OpJ~Kz-46-7&7t+vkte;V!POC*<|?hq~)L{e69|KzCiQ zKj7u+p60na4_5@p)%6$O+@6A2f56i_*zK*4TAI3=_TveI(Yj-SLHGt>3P-vDU)>;7 zfqgzKEM1X*U|wV-=ne1lb#-k_84QH|#{%AN4r2-r{{t2_zFhn;)Q#q@NLSa!3y5e# z)I2g84tKTp_xCEk4Z(-Pk1=cwO_;}+T{UzJ#NHZuYvUCS@8Y3X?k)^MTvAi{g(`&{ ziIDk*u}*me#ULZ0Mx}1@J-)Z>KyF^QsLb;AAoM`OBp(oEDAP(=6-pVG>8KRy{DMM! z2v5bW-9C{xjvJ`z;SA2EiZpJ(Ts1-;vq}$ly}-uyrM2 zBNPLLqzZlWoi0Hns^v&4a`XsRI9)+d(AG`G5toQZWHuE?T`AGViUg`aDDRxhvhz0m zLN*d>_zxmQz)g$Kp&6n&-$9E80BWsX&2}cxIuZ1uAp7pXnJ3eUYO9-5xP>nTmH>eI zw`o;Cs8~;{J{7l_V%zRyDjqbQi&dYCCFQlI?M+Q@H*GhcZG83Y&koD#YjE?`w+{UH z;9KVHjc-lA`P0LS1}$lJym;!pAHKKy)DQBf0;ki;ZEnw-$HTf4$B%Cb*La=`f3A8r zkNx#sI1{#l+)@GewP85wjs_>}ZICjj?alMKu{HJr+|F$HC|EPJOc&Pp~g9!3m9zCMw@L6>m8M372e3$6F!!rgHdB?BZ~w!RK<@UKm<9GBt+~ zecGx+|H~KGvGeh{)L}(JhV2~lM!KSAguXvjqr8J?vR0!-gmslf4M?n%RnKH=+mV&f zzDmCke3AIIf%K`Tpf3Du^3knaPe0e*2P2L#T_W406*-9@$&Qc$LN6X-v{Fr zj2Fjl8_2(mUHG2ZJ*PHpVjMWRPW_A4*~g&FxsKc99;K;?LBbgKR8`_6{;gER*(qoC zPV&80nkJH37SUrw`=vhtMxg-tf8b5ss3;r!BY~9FOm-`(QBY`15S?#gKU~2hm+;73 z(q=oA#Zl!T=ns4h&dK4RKU{PU-RN;1dAAUB=>F#KC=~2?y-JZO`_)rgbYRy(@D+Cx zeAR2!W)aZhpvQR>tXZw_`wp-5UM@Tdy1((0Rd)s7W&hewMJ`}J{UsNEpyu!Kld$2Z z_#WkS>p$(M9`MsD;a(7#F{EvE`!MVu!Ex@yqh2zfI{@Ha>v zF{tAa#E@ts^J?$+PIB0Dxae zVRpFw4=PC)mnknm1jUzZ5OCfBH1HwUg)|*sgRqiiuwTYwHj&e|UShy8E*|`GBWW`# z?vHZH2=b70WJDzV&hF!^I1Pu!G!2p60L*@zV?sJ{vmW z!Dq@*cyPfI+bk$SJPHry(lhYj@%SkeJZYm8#&5ir`mqGae@45CbMQHZby#9Oy|?(k z9Gu7T|8%e{jmOsuJhmiDdgI2pk}T +#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 0000000000000000000000000000000000000000..2abbc5ae3d81e707378165837f1ea72a5d265ad9 GIT binary patch literal 3148 zcma(Te@t7)`Rr$W4%p9z(8d(oeTF2n+894fN+5;~Fl|Z8RFhUys&%rBZLk|K55EUC zPF6j~ZXeB@$+VejRjFj!NMrv@WR0q9t0urHqsXdg7DbGq2o#cL6OGu~RoPmp`_4|f zKQ>Lhr@QaI@9w_)e&6eI&Ru`38lf_TP`{ep`}7OHANavn7oV-@6MJPqGpi9=kt0+g zHzNS(LFhP9Kh?RUIHJ_qTVI!@)ceX*H73PR`$gRo@~+n_x>7oOb&E>>Ou4;lvWL5D zuJ5jr(z?#q<^Cnrg=)t6%3H7jJ-o9)qjyZ8^}@UXJXnyK)^cEc(~69hIFB@8!Qu>zM4l*HyvQR(RXF}_ z0IYVX5TmR;yGgfk>YGUb-?l8_)LQi*c?(Fa^|g-Ebs zbD^qQ#p$CJ2>BC)fT7z>SzS$KZzjEK|5J+!=jn(gRcA?7<*W=s7eMDXU{8}uG+f>^ z3{=b7C!H;+e7Z}7SiyXDRDBC+Khx1)h;);>3oH(iVHjY`irbR41*(0?*`B7_3$ZjL z$q5yn=#esnk4!z@|n{=0r*C7?n#s#lwfPKyJLDI3} zY`sXeeUNNRQI5h+^|%M02;xH|{qP}?L=5M_;}$%Aw+z@uMaiv_M)eRk(nL0K;LZ+x zXM_I79KFp_{Ywxf(}qHET=yE5OL^{9UduRJmz=HH;&>_Fa@N^0Njc8uZE)$=ryN%) z$828xhmgb_lOkMFfRyt{f?g7GQq9NDY40HI-(B=phQ86E-DK!((1NiT*XKwUTE8LIwk?lr#~zQO{FNv191$=oK3uVLq~7V(KlW6 z=WPA_l}^*v=AP9}<8=_Ar^YdxY`>VSP32qC&elS{?b3YfQXX_{EA(6(g?i+{qhP>e zQq7+i>1~hpvkeGg?M+sDlhJF`{dO> z z7#gzi-l&!LMM9il3x$Q};V5q-4BY)8VIUM3^1JI-@!Zax$b*v9yX zZ79@l8yXrPwl=c1{!rLf;%yydtbyT>U?oe8bs!S(jYRxb-^lQ=H|)0#g~9>G`Yg*> zeN0JR#yV1(_512o3HFpuU9XZgp3+qV)_Ap={TPg>Yl8vWLPwcSg;~@#&*p z-+RaTBlVB+@7C_iRP__A=EU*i6@0z#8UE4QeOdHNs0ZZzt|*5$Gz#VD7?*XnL%Pg5 zTUYX@ZW$Kg#q1KOpStKTh{&Jl5K;ofg|_oa$2mwg zsy&x%gT%|^$$yELLFhcd-HOfwuoY3ztLxF;fJJ)={|2Lpn8!re78GQ>xVt_g*GLu3AcE!NWPZazqiJ{GeMhR4895GB0e zhj6e$4>ts1Y_hwB?{G|*-~xO@(Cxl=1VF6uJDj_B-B{^90$SXH+kI~`7Un~P;eekZ z!4h?!=eK76j6%QkzE0!=BA39a(T?=g$$z)K=2@0t#> zYn7Rqe`u&qA!@|VvWyI|GpHG%FAbeySg!43mKU@6G{ zqJwHJ+TY`nokVE671?!^qC;Rji)U(7>=-5?s=2Lx;!!o2~ zR9%Bao&ohaN^_?JEg(hbZ8aQU$t04wd81-ZFEXmPWx(MrJ6CluL$L_N7BwFlHabnW z=S}HnQU_T|dLfC>wX#J;A_NySRd#za3$wCHy@KuM5TjBap}v9#JGl*m_5uvwFX*e& zKUV^)shZ?FeOD0rmpU;8#4~RIF_GRyZJeUMrxq*dw^{UR?Wub8fco^4M<}%FSBJv1q4tbt&{KMUec8=#Z@ +#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 0000000000000000000000000000000000000000..33519966beb0279cb524f82ef7bceb03c6e072f6 GIT binary patch literal 4840 zcmbVQaZnrAnSZMl+64<~ZIoCFD|uyXM&mPP5e^mx5(yDUX~(;xSZSOIuddn>QQny^<*gZ_+Y@q*Ku6hq^Ub` z+xwn`aO-+HoqNo_Z{PRc`}Y05@AtmuLH-T5sCh)z{_>XgDaNd^ z(Avi<%ukLxg6EAj9owWNV|!WFJx8C_aP~vv+|LN}lL_q})1Fkrv(rz%#Qk&*?4INh zx(}pzr=y(feqR2qol^;@RuYpb&9=@LlUou~os2UqpJNFvyYq>yyE}i9cmc^y?i6j^ za)C=TYiI1fZ*r!w2WBn`iu6|$jhg>zmO0Zluz6UE&>4``=WB2M843|ZNYLZ>duuGHr*%-SyeSFA44g1I;lY|ZW$P*@MAT152q^5IHgri2S z6jGsC{ng3J53~9_Si=@77me(7LceK*9*#;)PHEIfMSbKbO$`WAXoAY%rNT#x)2|rW zD}QhLgcPw*!v*L33qXiUBlq^nm1X^+XjnC}ON0TI^ugaOW_%N0yVW&p=7O&ZX%8M4JkwxmfBjHINnsSp|y#6=o~ zP)<-n)&9hFy0VR%4YPrS*%%js>9-TzwImf&n0}!T_{meMyC0GXUz@EDI6L z6Nbe!INvZ&@KR8aMog6WI@EYQ!+haGf;3E1qniX+u+oTARG(hPw4$ssQ(7fHv|wdq zoC5gv81N3Z52{L7Cm3Z_LY!b2XriiGjN(>VOFG^pN&^sF2=VLGv%YvZD2*-%71!n! zpQI_M*Ewn!QKLK+N>gEu>O<;KkQykwV`XswkU*d!X==zy^`%r$?Z?Mx-hYahKJw^v+q(vLV5yRBzMgwBHTZ^4*GT4c{JvppK3ZQO22 zM1mX9W3GoGNS5r-6n zT^S^YqEe8Pbos5S8!6Q?uMY6)m37s+Q`N|v*I$J#Z`9Aa3_bkGmUrVV^Y-Q$vi03~ zYl3XauWN<`>V%IvfVVkyK*Y=p3e=E^8oE^mW`{+oiUSB{ z4W4w*0UIaTe4)PLVlNi+iA(WO%HBL@Z=NXB=W>?QcFQ=~aynNJAH6-+a+z$I&MDvX zOTnX3C>W2x))u6QR*Ix0-3L#pZzAVssN)};Z@N5bV>2QOR80;>K1QbUMytPb)v9x*P+Y5$XOs* z)4BQu`@y{Z;JE!Dpq{rsghn`oehr)o862E_T&XJ$nH^kBEcwz)mpamnsk^no-2Tm! z@q6R0bL0zqqo<~>w6p9psr@!YJ!+=g85$1Ih&LSB=c)Jg_j&6>VNZV~Qs2?<8SL{0 zBH?<6%X8cxI0iC&+}qn*A9fAbg*_pEFjDUiM2^7Ja6LBA<@QH<{NCQ~u5e$Z%M}W_ zMm)W)z%g#f8w&gT16%{Y5B}=*54r~fk--M8W7rky;l5Jr?eMw>k8zI$diqP6VUN!h z>I(Zuz4e3PP<^l8UEkX~)K}NQ*Sr0J`l9W+V_coL&mXD7U0hvH$m{73b=P_N`}$mg z?z&!oz{}Nrndj;}ToEK!*I#^ddkSX#0Z;E>x3@lOY3gd)k0%U9>y8Bm;TwP}9O(v( zb%Rg^_W7`|bVdGwd6AKzH@wf+)wMBYFc9`13wXOZj43?)4_Mgva`D4ZH=4U5U0oY5 zAfgRX^T=p8+|}OS->dj85C954#;`RsVIE_4)zC2zdu!;ejh8jNi-%shyD$iGNloQb zRSG#0A^Qzuo$?5ZK~_SIO5No9d~ex-+`Mj4ndR+4=z*k3-Y3dXrj@cPlrk>UQ7P2< z1%>zko{C$$eIjujH&E4s8JtlSY21LhYJ@&zkq^2#Cel-Z__L z=WY6hY$Vq3-$aUl+ZLZgGemX1gBA?{)LOlo?M$F`BIrdy_Pv2KkEavWRyU_`3ttN? z0RZ){(yD+^v7T0aE^af$w%yKD+;2J;t3DS?%4<#Ao0@*ywB3BR@s+bbIxMTN!Od6R zIq-vn@0hnYzBB#y4-YFEw4~Yb{Hgc}GKfWbg<9R&% zPu075?5{WAT-XY7O9kB7hT*t78l14VLE41@(=N%&8>(E;DT z2gb`7FOJa}XK2xxK8<2(x1tXBAqhu3;H7aj-Q-}uR@yNvI%f9*a4|MpW4_-U1JFNn+-(l%HSBPXX``y==#`#Dt7|3I~)M_F;>3leceLKolp z^*_Od(#g9}H*(J+&XWRNHRyh%9lQ3O2Gb8#)JT-^J<1pN{((f6u}kITl5DM3DOPJ= z<0{thQmd8IV>YrJXNyY67QmEfktz4W{LnoycaV6W7dTObyqP2T z>m-jD)bS8vNVJjiv@`H4eP!FS`ujYJ7pYNzeb@f^yO^~;SZcEfu}X00kWz)@S#(kW zz|W;HJ6ykqO47w;$_o%d@dX2Y*~o z+Kh^O;~(JQi~yWw6|*yeJ}5KsK9PJ^;Si!?+0Q8-IthKac!3ahklV=99QGl8n&H7` zLnl1=OgRb`?q=$5hFb_(yqz4uHXYh#*B>3bU yZWqr;d +#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 0000000000000000000000000000000000000000..02d9b20b958a4c6f4a4482605369bbde03f11620 GIT binary patch literal 3236 zcma(UZA@F&^*)~QbHILn5ZV~9oo7gp*JAuIlmLdxVA_(FsHTgiOzUJD+h8|fjGw{A z$);!Q_R*GBP8PM^mLF!#rfkwAvPM<6Ruy2%DDonjMHOQx0zpVNk%+b3l&RIab8XW7 z*fjN`d(OM(o^$T`yw`MEXKy}MhEO3ws87xvdHTB_^q=_R>a)eYLJt8nogAT^0)&bS zbO;c77$y~~KG(4%IWA>PE$4}Z{Ai)9Tq}9CPhg%X=saKCnP5z1%`(+9MW)Wl?!bbs zx~o*2Vmi(jxR+#C%2?}@lk7)?sWYK^ME^*#{_M>2=h%fM(EBorP$^(jmFxiPeo=C; z>QVy0R$@9?R@yT;Rh&rlFwND7mpHhm1a;MklA}EzBwk9Ue_SnFMkn1Q@gnNFbg>#0 zR$(=$SB20|09P*5-2Vy&5kLp@BrBgBiBRK7F{q-V4)Ls)9FK_602S0zK`$BXrp|Q3 zx7d^tBS|XiC3!(?@``~p6+&5^dey02CfFsNW=E%9h-sFm6?b&%>oLumLp>kUz%Jrt z)L2RkA{n0)16~nyMj~P;Kt=V`IKn&xyE?7jacb9)c6(aA2&$&lYqRQ&Y0Z30{k8by zST_~+l4E)iEA*0Q^x{Zb3@62=cf}A(MJ*Jf(Y)s7wBq`lCJWlI2F03AeTUF|twa`% zh)p&z>ZKxHGAg4+9AYp<&0n5=JV)&%Xg zPQ5{B!K7>dWz6JwS`4VfQ3yy<45xGPheUYEk;@d%i9v7;&RT)c?I9MTy1l7hj%gvV z8`D~Jc9t}INpqSMKuJ>M^|{pOAunPSQkkM0ibdk^o}l<-R=wxcZpRd#q%~{A;Z=tM zLcI)2hZbDk1_pF^Z-YiZ(}LIYb85(7me8)HA^6%Af)fJ{aa>OcmjPmX!d&hkhZvSo z(XR_&)gmikrIi;paamE80)3hm9!JNa-f)i`OjuG3^v%HnlNhqDmhxO&eH*u7J-!0-gq$ zpkCNi_m>gvlh)=$W~x(wTA}#VhYA_iEoJX=EVCh1L1>F1PNd-R@-ZeSKPH=z}Ent7+TpL^N- ze%!obZMjOey&rE&kml@O*_eYmvTq5hWLllg!F8v4Ip60_=_g5R%aXMvm4okQnlD(JCrR^#j1dm~ za>9IrG|yz@zxRoOQ(`a>4?)X0#E?o1rN#1V-&Wp3%1>?dc9Pz*C^uPp7rbEgn)NyD ze24ZrbYM)oz5x}l`75FASM@f}SX(c~%~{)#eMg}FB2*;R+w*x+i6fwWLA&f!-_dDq z&S`!~;Cm#i)9g8=Ctr*=XEWv*YdZww%lWo#t9cTZnW+zpz*8{{_COs&GpAzDZ!z@l zEPcyHf5uhMUGLCtZys9R)Z7FEy35To@%F3n%0#Al%G#36w7ommvXlWI+p^tPN8mnk zP$Lk)Q)2m_7wKJx^6mzdu<{nCyu~X2VWa&Fy~WY6{A@$|mkoN`M&IYGn`^n7ZjZ=W z?tJpbpEAvmteK2))!Lf1woY1G!Rr<4<7gb}>NM0;P}|K~C*|b_f~Ib^IyQCg+{ayM zM(=K`H+8nO zpML-_f7&xRXylz?1Mdp@0wJT%A36!5yb&v~_xVEoKF^@r9u5xs2kfEofX6lH^bfFO zo*?fV_Ota|9sC&@NBc(oq0xG_E9?yRv){?@c6s_n2iW8O{^19du*>TV+Ie5pV;tp! z#z9}7ad2>K$WYH2`+R<5UbkU@HF$=6Ap_oG4gEonYdGjOxQ2&@oPM`q(C7EChG#j} z;9~P$vWDUOSDy=2%VOLFBd?Yb^%G1Ptm?|KVrs`2v8caHt0^&QiphIeM({%!9|)GN<9 zU2mV}k5@m+zg2lOS=xtJvTc{*=8Mo| zWP3W^1`U_Y;NK)p7NPe5ACz>|0xKe6mQ|x8M{Ux_@c!R8geCx2J++kVeR^dWKG72; zl0e{che!!Yx7>&2o#s>y*Q=$sU3(Wx6q3G@m9-~ThW(b8-u zB33!{!i@B%GQvSRY=j#j`6Ge?3GI|cs!^fBnaf1&J;ik-;2>iSZ|q1b82lQOWlMz!YHIhwq ze7f*2c)l%P0LbhDP&P;lT|Xz#wyqx7I?z5_!H1ZQ!))Z;eYVelEy+3;)8024ksvRs zkqh!8HF9K{%&N-%kd&g80ofY^u>E=?LPc&Mo;WW>0m)kjrL%?E6Do9!YjvXM+1&&I zCaLC7j|#QAY|R}N$YOyPI`>3>Pl6QKemq9le4U$UrYeDcEy)o9c!2pR;8OB}9)}vI z_92+Ke|lhI+9{ZLV2t-C@d8FA%!4rNU}Ap!KL8#N_VG97e=r{GV+?Wl3LVMIK+WZ3 xF~)RRZC>L0U>l}^Z6Qp_^&GzB>fC(;b#8pM20i&3b-(KZuKzS%{;tDv{|5gq8qELz literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..ef6aec72e83df1dfc7b461fd5fc205fc1ff3920b GIT binary patch literal 5012 zcmbVQeNbE1mA_9T%GKq?{PC=Hp4#FIMH?4S>Xr5J>e z1PGknJRzkIXXTEZdME6zGb2*}k*1v;lCW8~n|37RIMk!0#C0>2^>|>w#M^PaY?Ef) ziQDeE?;*Q!y`9cp=G~8TKY!=^&be1~+Ot<4tVXB=A>>ict@w$_?1?8g@Yi@msNUC<1Ff|6{-+P4WhZUVKZR zmti+f+x_3+Oq2J|U2svEr>N%YpHwPej3_hK1P0inMd&o_Q+uxd<{u#uAyjH2In~r~ zj2=&mVJ$u35})&v<1uj}M2Agu*iVKX^f3q2#g=I?mZm5CWJC~K{9-6WM^VA3TXGvN z5Zr=MzhTs!i|a4UlwULIF2?oCF5P@w54|YD(4*607%`Ew81jp-W-KN~L-d4+9!Gc# z!7a_`Hr$3~WLTfkork4nbjw-Y%8Y(KuDd;bYSclG`N>g}h!^ye$4ugIMjT6vEoa3j zM^9L3q(<}lD>LO6bNT|ThF2(GHtMbs`rC^zV==MCDNgw5n4g?r=wX)_o~E<-sIaL# z{jyPa`7ceM7NZt=Oj6F@0)&`2es7&zUezxPhIONEg)qR8KKQf4OpRy6kX9T4g`~x? zjHG`sgr6LKjgIhQ7@)yki=etq#DP}VS9KTS22kwEi~&8DCENUDTZR;1k+c{wNv1J@ zUBn46Neem^?3P58T~S`W64zxs=feCmjNKJ!vM5nb486_H2~`Q zoDM8lAPmbHP`+W2;Kh(j95>OzYmnpfjPcS&E^&;ZCvFp9$;u#(sy(%eX+>KVri@y6 zXvxYdI12doDDVzk2vsGm)2ym0DNM72QXQaP%P3ghTYORL4Sj0Fb~%M>F)Ol^#s1A;--{YD1ub ztiv1~TcmCX^aM+f$`hsDw^%wX(Dxfvf$rqK-_57Xcm_$14(CM-BDGJ{unMJsTT*f% z`<@>h#$9sakjmxw*P3#K$SsLdAXML<&%_V{*iw?l_^7XwD7z&=1YXDDFd&2#gp;(_ zRic7GR;i7k)C%XQ_^T1n-P0ThY52^BX||@KJDn=6f8@NVJnW=)Ti+58dIL86 zE{thr1l_q+U4J#vF=e+T^Qle&cuGg6hgBO$^9if|Oi(wgI>Fk&N?ku+A`MH_7RZhT zdq;}wD8y3WpvM?`+#!a*Q$yrvObl^iO`$@4J*{5lH9=mpwyEB9s+-w!`YR9yjQV-E zp`SnA_D-U0(cU^ow!f2TPm*ng&FWDXeauhq$F5KB7cg5xE_&2NkKQbSWyb`uml21x zz*%v8I{v_oP4$fx^>4H4>pbaM0EW)!3Q~UAt-Bz{7&rA%+TOZgZ=II%vw6!YyJd=O zJC$#QO>a%MT_W3N^Q!j(V(73K4ke=C?k+K^6{8uk=7T3SH<0ExPW5_Py=K*{a_Z}V zf-~ta=M3{U!$t7^xZ&~&c$@y$grQ&CW0|!dIGt!KICpIU0q)1>*mO_#XK4-AfZ81|7kgyc;ZL{_cP{^(M_H}#P6g2axcgp~&I0okdAA&$K z9e-wxRbS7luR7JA@^!h3HpBYr_N7(*6*z#SrfoLSF_)-K<}E3EYa!o$HrKk42aN3n z$J{W)LKi&@3Op><{Kt9qb(iLo6>t~LRbF$I(|qn!2U+zRuZHHQE7X6ksMnq9o4kE> zS&FiogmiNE!Arl&TfkVe`Nk#tfr9
    GppUbH`i#yNy;0H?wR2WOvB)s%+K4z4bq zI(hQLt_*AHYi}}lekX1G-jw@IlKN`w#F@*TI^DDBeKtftVrDv72JW4xFB0ABZS)Tf z`WnL#?@%<_*fr!G8T19Ckw%Bxdo&O{0%hc=Z(yJ?;vQ>=c*B8Ev@sBj9)hWnM!Z0; zClKuq_y+oVW0n^0fIE1E8})@FfuSJR#P5Z_hJ7QRkzjPBiR&73hx@switm-QnIyV8Yip5(zgB1U!uc1EYftO?;y#5Nwp!ZaBg<^oM=kp>SV=cW7|X z9qelu2n2mx!#8-Y!OJ!H1_RLsJdcy%aScOq&Eu7p4FtUdBYnO`IBjpsK0J3M)^H>^ z0($_WNVE^oHH<(O-0R1Mr8oLl%!`hPe38BW-rlV#Bf&`ENYK~EVN8*+zhZ^0o#l-o zZ#MTvdwaJkP{f*I=JAP0q_=ZuXaK^~KY{Tf@sli9$Jor1tf`L4LBZECPc~nw=G{E> zDm~I5#HFgspRA&kNPuWKhGnWlC=L+`HLGf7-scBO_U9LCmQ^|49)cbSqU2Wu1txKK47_;4UiWovOC zZrOqvc--Jr^`LbvX(Om%DbPaSVz=8R5VcAOt{gLt1x|Me1dR2z;E-FuBeJ&zhuvwx zrV|KMhETz|kkc*N^h>#Dyy@pent&G=pGR{;?Lm}OJ!>1q1 zBx|i6j`Fyk4z2(I&95`+psQ>%qyAi|G{q}#Wy|g}osHL?ji;3LrtK{)|K76Q{6_Q3 zZ~VAN(O8F@FTcJ2%>!?nw>Q5%`__+os3t9GcD!)n{eO9X_lX}CP6SV7RFxj@TSp@` z$BrJ|7OC?-7Wr!JZXWCF`*0^zK)J09-f&}Z{T&WX+dCj+&e~fS^OGC8^YCJ`;j3W7 zsF!2def!p2>W`fe8a3-UKx#gAsz1ZJ{E(HeE4t8rCed~p0xsE+Nwh=oP3Q4j+09`~ zgU*$<2Vf{tz*l_`F{i9G=)ZaS96KLbNcT`l1-|x<_@ccrGeSQ&Q>VIx7_z=viwNsF ziJFj5uBe^M)psH*p?#ToKJ)_d3yMJ9tf>^{HCNcP>G@frqFTv&LWpCisp>D_;gPrw zndTkHzE;pyr#`2VHODnm4}b3#fuc>y60_I2?}Hui)^~Ml(RQuHjh=B`OA@oWlksk2Un-z%eXE{ zxL*4bE^QIl!Y+&}FX8&h7OwPfi@46nxDEoYt~AMy71G6FF>E4vhYlPeD0(Z1e|Z>!7Ovt2T##76-h}!?2pw3cvgCS?}h;V<7u8Jy~lm;rH#A^(1ov>*-Iq z@IwuMm!4c(dP?k3&9?u)_0$h~S|>b90y~McO%}u|$#bv&9+b5DIb`%EWIOs*W!JwT z5l19z5<9>32Y5_6c{l1qo_WN1(;%w_*^jl8SO2le^yZod2@1Yn_2L7+BavnD!%}iZ zu~DxQYPGNMXfHcDkF+gZ%7yAx=#?hZ+=>Qq960s8bk-*8tQ}N}s^Ht=5ed;0$vo>1D8@-Z3#1Jt189Oq8y?HFeN54zl1pH+x-Xn0@_KPei z#?6C1uBB{7>i@>ClkrRU0KOX_W=j5nIUw6#slYxn=ne#nanj6`m_Y|O5jdaAzDfNv zLrDLZX|AwkQ#jr;wJMi)B&X3NmbuVp)`f2>lJ{3ctueSMT7qd~f5o@7_Mok-dFBcru55(yb@E evqbPao_(9|*x2%8ed|>m^4@tE%g<=M{{I3{p#1Xy literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..f7f5ee7ea0500b0ab6cb8a6dc914ddf236f4f9f9 GIT binary patch literal 18136 zcmeHPYj7LY6~3#LY{hb9#SUN+w_c_Wb*5O7LkNbDL~`szW}F9k6$;5lme#fgSu)yH zVy6Y%abV&EsObzHesl`cp{-|H+H^`YbXurGQUVM^Lw~fils3?$4JAMYsm3*&{mWG8IItmxE${L@7O?bgFOJ(oj0tmQH2zBW)uc%i5ML4eHt85S#RFf12h4qxuSl zi$SJTkTaM^0>fU$R2BQGZp3qjIuuW3*xKHn&eiIY;F91KpdA>>W`tG+PiCYNM2Im` zKJyDwb5Qp=G1kng2=C#!vCie3MNV@T5QjJ!a5CUzz{!A<0Ve}a2Am8y8E`W2f0BW> z>puT}Z2XKjcEIy$h_Tom(}t^XJT`vRdxU2I_3f|sOgz6MHt|Yq{N&8WEj`DkAFPkC z*s;T5PL3%+3Kx7A;O|VL{gM7)UGrWJpM1160;VhQXf!;EG8|&guTfAq(LZ^lzhqq3 z9AS@h`>(&j$;3?T@EfaQhtJ6|>B-ph9~twC9;$^0J08a$Td@veVfluwv58Zs_Y?|+ zCq2tSB5gl1Ydo}nZGR~Sgv2IpJr_IBeQtluJ^iXQ_Oe`e=aZQE+Qt$e`M_M zlEAb`gp#ID$YZaZ6{u1?<7WaGGup=v+p3#Y6UD48%ZeEfD_9 z>8}=XMgQ&7$GShjQwRCOd_}+9d-sZl%NUDp>zVj{bZgJVyU{Jti4V5M?rw8~cysUK z4{=SMe&9oh;qZsD(cJ!GUGo^a=$&}0cjAq%iGM^3^ZyzfKO)7hdMW=;TyHmSkKPpB z9^DaDt>=`lC%_@)>$JEs(VNqp3^*BZGT>yu$$*mqCj(9foD4V_a5CUz;L~P6g5M6M zh4S*90Knfen`R1yuL11^ItjG)%|hWJpqBwX3iKwRCxPAt)D1r{{t9Rd&@({0fHu8V zC?tVi26QjbZv%Z6DE>Z+P1>`GNh1MiVQsY+f5Q%dtO@?^|5u@a7wxR8I)Jh;{5=9P z{+m7Y(FQKR*-nUS0ZbWN3qXtd9VPu<5D$ZXkyXF5q<;wH zW1#<%Ro`FI9|ig3$M`=9`UgJ-?}qsv1bv;=|Fx$7E|9f=9`PFL*Z2e9aP{~b?~%Lx z%H8g6f9qYIE`RvWs+hlHyn3xalJR#${o$y;wbQS3`Wrj_flj}d=Q9m{o&rCVJ9OtX zCj(9foD4V_a5CUzz{!A<0Ve}a2Am9h<{6k5;VzGh=d0mTgg2tKf~V)M=L&wRKEit! z3!a{nUMP5a&Y55Pf$aK~5w5}OK5V3a_oG6V^Kt|UqidjH!P7I#t%9%NR*ZEBir2u{ z8co735R^!@=o}Y#8W*ouvBAT*yb=DRf*H?2VGqBq^7tfS2bXD_pAvc@{+|(guKbe* zT)TSp)k^EuzI?{WD^~?C4~E;?ugr6{{kA3HV0h_bQ_K?ScxFJ^rRDTgHlwtI3T&4O zQ-y`{dJZ4v4yDt(hT7W0p}tfmWMbL|l(znymdNIkZHesAP&~t*_STfP4Pm7%p%|KO z1QSYI*6d~38OWlWNABhMtc4d6%yub|fLMynpmPy}>qpwA4}JoxMeHoPYxZJWkp z%k40FRX-f|11mRH-2&Zx&~;r}y$6U_s=gmNsrolSJZ|p+(9d}W`n8g~=2@VB1cBsX zz89d6fk{=8RPFX*q@1mmTpqU%!{Dq}lHBf^7YR7W%c@QS>Np783#u@h=b-Ca%%pkJ zB7cKN_6IIn=$|Lm!-v@w1Yvzuq*3-??OX2q;>A4;tKd6C_Ar+a^)!GRyA|4ag3Jmv zfmIi>o(9twW7RE8_OJB$;7h?<2XdHZgCzTXJ{*d%nz^9vX+Wj}SYL_t`R4j+xsbh! zvtalcmn7*w{<%nCM)+{P#6JtEOd_36Y9V-|L0z^~yxuU7$-@W3&>1rqJph<7I;`oz zK}70CGL19#-{}B3m=*k^4d7UFWH-`K3p$ zy2ev;tw*YQ+rysm_-ft;$@QK&Lb3~BC_(mK5A%jSb85URJaf_QH6VMy!+z|MYo2z& zJw@pgz6Zp-LW9{MEtJy}S;Gi*WfS=!Eo11RSUhoaDl-67zgbJCLwbC7o1Vy}hK&$R zaSMDA=ppo=LX!GZS~{sh`q+SGs3S{QKBK1wGFnne490WtA_bKzCE#VGo#Ch8W10-7Xv!6tWg)}8)}s~WGCN&S z?q*)Ok{=JF{mVLt3~vt6K36WUW|j6A8Fo$Dm&)zuFxubB<*-}Qds7yL40n!|it<`U z`?|#(-n)TaUx`>nye~69qxX-jN*TVL1}oYJ7}W{o_VbGMLAku1Rod@l*1+h!nR0u$ zYYoq-*_#YiL1RVvg$$otvp1PtWEXK>E>;=kYMD_LWS3L*W0zBvWS3KQRFdOYkDI+& zC`rs7)@3d@k2`JW(J$naHu)t&PIaE?g|RE4Be7B*a6D{l;7?++&&v?Vaa<;LF0{oq z3V#yZ&9*tuTx5xP>E}y-g zU*~>iuPYfQP!D-{Q0&K4w?;v(R9J5fAP<1tzTW1dAJ^>9-2#;Jn92`Vak-CKs}r|30*L&Hi5fi|`W=;}$>piJYMud3b6z!ID}|8%XJfmQ#%( zHIdF{G#xgoWL6zWXZzx5HECpXx*E@qFes;o)0&|rgB{^z;mSs8e=3twHOER_VhV{{PJ*&$# z{0&GD!F!o%cT9MQb!}qm+TIPF(Oz}Knl+odx2Rj9oxR=YmA^Nc(DOWErfSK!5hro! zb;?M@`aY$((?fQ^)_kjyY5?1tmSCc1)j_!UNNY^(*#O2+Y^ix&gZN8BV+NR-OshF9 zolV3I4V@aPggTtktObRt_UXD95bKjs#tRD`4zDv*b<4WdB4MI{VL^R#$cXm=HF72$ zq#l$ZT5gyHGg(6mLYWxs%ctP2*i=%8qMbc$Mtp#A-C$fFWWnTU2K<@S$e9{(eOAV( zpo7`O5x|0cfc{)~a@sE9tX7aC{H%Qz4R=)d z2*TcEHmc|7eRccJini8<-xGMRfbdlJ(fipgR%7VX_aBLuLC1=x`tY=HsF0zcc6=Ae z{|)yRXne06;g(+61W^3+ed#sD#p8PD!LD44zg6H{1wJM$@qP-xPV7Dip=o5g&J)Q7$zw!DY2%(Xk$(4ALKL-jt z_k^eG4*I_ilOldvAA}R9m;C{-XhL|pKA91P4B3GRZ-giMXOLR)#p{@`X-}V1lbap? zDI1>Zz(#>T-}vP3HRxb06hGBHtpZPRlD+M8vKdgIOqi1yBYaO$Vs;2m^gR$)!rvks z_I?812VnALHGNFrXKYFv%Pu+({^2F2w@0i_p>M}8IuAa6xe3JiS(_c-F7WpJePyYM zddUigKH;sDK6_Tvjw?)VL@eCT1B)LCI-j(z@IE-5dlO+E4=y+9DH=#9Z7f_HRL0-8 M!USAn1K3#hUz$3C82|tP literal 0 HcmV?d00001 diff --git a/intTests/test_bitfield_x86/test.o b/intTests/test_bitfield_x86/test.o new file mode 100644 index 0000000000000000000000000000000000000000..1207e45fb764ea0eb44ab9eb4bbca26912c18bb6 GIT binary patch literal 4784 zcmbuCe{3Xm6~NzjXJ@Z3l#2RC$T_?+1VBdo_b>S?!4ZG15P+Yg0S80PTS3G zXV0D4yX`4qlQZOg_(wrZj3MFt$Cwy}MByI@DS{CQBpL|`#y}xzBqBLQ(_SPw-}}yc zv(v9V{lnKx-}imqkMEE9&dhfo+JF0(Q%Zq|g4>{P2?aP_=(neJa~if`E53d=S(QcQmboL@4a=->W}C2 z2Spk)#m}67aAV||&ibEe05hjwDkiJTcqE?tpd1|A1P=dVA}_8#wfd|5A5*>iU#vB& z{(^JDYX^;%?@Ud)_*c56GuQFM&Xfb87ldvN%8RWfuiOr5tuQR_Yt=eSo*xF~nQHA= z!(Tuh9P^sZa!@^43To}f@vz+R!+S6{C{u;XTqB%sc+GmHyZcsH@WM*>Cg}Jb>vL2=qaoi^WO9NmYF{b(7%|2(RRhp_j|JPiTG8q0j0o2lyuh-8&ksYu!B?0NJLl4nSz zbEMxwplrbV20#N-8Knl&eRDvi?1Y(BDxF9i%tGc5+-3UO42^~)btAz4crc;d3EJgm zW3Jq6o>(ePO_t{xemP1iEjXq5wpVMl>!n(2X{qYhOU;JwIi))%ol?z-9%`r5idrq* z=MMcJCvfU3pt?o1b7&yDg5%kRoGudDQSik=@!{0o;mlDCK$CoXh@;Tmi~SGu{a+)F zLOUq-&-VS_B#uJ+CHBwv{f`qzxl;Y-BKH;Zf6sop^Ktz{QT=}+N&~HdQtDrYVN!G( z@KSn>8-A_Xse5I7byaS?g%+~YEiL#RT<|aec|&4GxP06T+(pU^!aBZqO7tr8H<3QT zeH1@|R$ke;+-bXzIb>TaHe{ZR&D@G@%_GSkwuf@h+E!+dojYW!%tto7YUgtwA-UHc zWO4%2h>-b+4cSS1Fqi$jJxpcyAbY}wpW0ULl~f96i6j1R@-#Zr@VCob#aR89$0oPc ze~=9xKYRus-ei;UTfDX>>gzp+j2=Yd4r&s;7f{dQMZCxp()SqIYs~LLO``W6>d)Xs z@lO#%kvf!4yhjj4??u#Qyoj%%CK3KhWa=5y8{y;2k;uZ*Ym;6B!to=ch29$RD;3-F zA}4O?i0I#TZVMl0`>F&_uBxn)#9z;GpI}Y%i#Hs$WgaG{^&ycuxW%;`U@iPNY~RgV z>NspySxfx)*`_CrM7Y%XMuhd*j>akX?JRSN{~_DoF}T$Efx-X6_D@*LID2eA%UbG7 z+%F9-^=W^SNc@M93Gc9$`m(?N%3R`q#`e0wrM^uCP$XW)zm2)nU(-m|Fpqn{Ck;`qV<>O>4*{kGS{Cq_@m5^8T<_Mw!u#^UpDv!<~@VI&iva3|2y-? z4E_f53kKKcVe~y|a9QW)4KC~Ry1_4U{kILi#{7MQzscNTO>3Nd9;XfNusv&Vc`kYe z7yE+2Wgo5@e2s0;PSnZoi@3i>hc%SRNCD;1ePs+|%=e+D z{w0nvRCu8O5Wrf-FPf$)?PTcPyor9Egj>YkvjwA+0bbOLMsdT0J27^v`M=B)&9al` zPit(>pT3(^)13c0=Q-$0iu5n~F?4Q~e>H!s4=0m3mXPFoi8gVOdh%m05Vhn9`f
    FybtlKZsF{6i9EGwKZ>q7Y?X8$iClNcSq|7P_sL4e(yKx(V~^KVnS B5_SLp literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..641d5cb3d127718d4597e0040171e14ee9b3125f GIT binary patch literal 4792 zcmbVQ4Nx2BnSPfQy8;Vo`Ki4!lDsmGN0YH(`7s6qiG+xwG`N-1Ovg7(2MG`s4HiNY zAc)hhkdnncxs?;Qp)<}@G_;dUGaa0`Irk?SfgG3klpJ$&Ex z_kJs6x31gi+{f(q|Mxua^S$3ETJ5PTyUGCa0iaVOZu|5YqEMvWN0opWDzn#nqHGsQE_= zYaSbS_|KRt+Dha&XL~NMdrp0_Ot9}A7v7<29*gn!TkcO(AD({VnDF)-&U-`v_!Oo! zTO9>L_cN;Jw@$?{x*D5Il$Er9HNGJ>)y_GCsyPG28@BE%zOVhQ*t3v#WUFNBR=I>E zw|c_v{hDAI+kEPri%EW-sV#f6G0&N_;hg(VzM-p;? zXGdM~VJ|%rmPh?;z`_Q+bilzr<-ojLKOu(`?5LLxN^-qd_9xj8WXy&Ix9J=u%$bd= zX2Y3?@!Vw5b+h3@#JK1(%tnmZ3PCkHG$98-9Zbl6uZ(ks!*a;aj#}6eAbludVbZYb zHZ6i_WzujKrEr$el)XIVu zW{p=Si!RImvxG0%c%!Vb(gj;&=uQoG2l9c_tJcxuO82zt;Uoz;Xi-dKLA%JKXvzuJ zRdklxvL+Q>N*UJNrjBQ z63I8sQ=;s5$s-n4dKqJ~pJ7p1$R!V}+0okqSg@)=V9Jj#6Irp=JWEn5J+NTq@&pF; z_6X_@j}Mf_tP`B3G$u`O92TK;J3(XQ#pa@)SD9H|4*+U5}#-upUtV%43bwFUl^UOyQ zJIb*`*?~&y>l_=9*v)3mw{|}I_9tJD);)jov+r#YJ{RHsb!mhB{*(ZqCVRyofX3zU zSk;{31e7X?(!BC&CxuPfAb}{Ef6-G1fG$G`95CWkVe~&JaIM!UeZHZ$6amodRVp&i zk}v{*Oeq1^vUWzT=eOj6w1bev;#Xsu;Pl1qiFm>GhtI0)h1Zxv@(5!;)Lr!~B($;EP(bA|$LywrRbc>c}=$1Kq zOPp@WgyVQPpHj0U4%v^V)K3qEWxpWnGsW5)3GK3|^NG5vYuYuZww60%yn-&kY@BtQ zdc-45KaDoc+Z#{O%|DGc$LOZaTG^0`eag%3CdZ!LEfJ;qUF?vB9lDi|(+*2=hgu%s zQLpmIL}bTDYub;Nw7*MfZ-{i~9IA8DkWu2xZo|2(e{nOH686S9d*g%>pH4R%w>ON_ zO~=z!xacQiO&95=>9po&y|Vv+9Pmd&c+_2Th?hf2S^wVWbRU84w@&R!LVMM!TNbo8 z5QShdUY;?{+DsSl-G<1)h*TcN{owgQ zCo&Ov;wq=Tkh}#=8>E_cjjdN+l z*qm{k8bCkjVh51G1G4^?XSFw6x(}D|sOYYVx@&^&_fD;k(_R&|Sp0a2`PGtk#i_j| z+Lsp<54%PwJ9qEB_et_0jg^y01nVDoBDOLIX+oFOh;>4lQ*Ee*i!{6WQ z3k5qu{T-dXp`Kn(Uw36!mAC(prz#Na>JNpg+WNZ&4|%XpmBZcjWUucaroksYeSK9y z_wdeOSD@D)QnCThq5hC(r`z9K~VoxNfK$q3s;R$XDqlNkd2I9~c)J@q2=m-j0s- zA%nhP??IoZTOf-EhyQ^Y)>qChjB#yEN2sG?J%dTOI$Sd{8Vq){_V@Pz^n8<813(<( z3>9jsW{lfbp^jj(qe5L=d$CM(iP)-gE1f`ymlc)Lj0z-lQG=vT^EgD%yFjgmKlZNZ zeY-xL(!Z~n5uKDlX)FNv*Z}$+Y6(hrN#8vY(Sui+3ro*TP|OrXO6?ax2asY5F`u&L zFX4XvjY`;5jFrNsjUlENPUSjYN;8|6$n^o@e!8xRFZ=g$iL{YY3D19fvkG`gP!Fcs zissv0{=;7qzzt)`Q}BH`Sc1ec|Mf_m5Rpkm3t(?0#*}8#SA1 z-=NBf@@xoEZHnWOLi;NAOoC(uFC zEy-vzI?F_wu;>9Q1@b!ZiTj zpQ1Il@a9_8@jzM6(2@vJ(b(o!XSTP(C&0g;e%ckGUS}w1=cd#+uC~}dotT}bipx}D zrym403}L=WvbJ5nS|#1lL>ZxDvm};hM_g+Kaf_?%*;ITz20hXYP&Bf$QG`<3)m(*scWAKet`*F5BI&v)slwaAcm{$UC3p zAa%O!dbB`e*~NitOxRZ%J3=&(wO_l6+c7EjS=DMP&Kp2IMzy~Gzlc#%Ad?>xx>_cG z@OKnw%DI_hs9;zab4ku05*{v-o+-5s!BUTmA=%4yIl9MJz-<2gtUEAe+{9(oD z*!+zPEcn~LQ_7_B-`U5*?rnRJE8zxm)o0~r0A;bK%Xt82vs&@=kiFimg-5aOuXwWR zFOs+DU-FdI0^#Y;wa}*%@8Zd|&J$gznQr=j^VEYptx%l{5;q2XbpvoJdg`_RL4K$| zU?i_$w53N=c;h!T2vkfT-TH<9#>byibVE0E&VtaDz`Am*`!PRu?OWBB*Iv@0XA^rg zU)}L58XCsV7tl+2tJ^hFIsc*vmE6!Q@byC61=}_7VzuQ|QU`*7hx%TeHDx(#CJw0- zzjYna#A9c5)Zy+6-8nCnx`w+r^54-?Lsm;IrLls0Xi1gRQr!^IY;*zf7DebSP$}W8 zQtpNMfqPY))G?{3Lm$o4oJ9*t&)U%7q61~%1^3ycI{G~{E1i$$ zWjtb&1itw^hs3x=nv10DdHpl>A;%DlvHwKcc0_@YCZ*#wdXdS`SM9^?a_K zq=@@Zuq`_VuQX*WNlCqWNA`a)#E+Bz$&fVHzZ~;qd@jw^o7em0(p>#^tS1`JrMY@^ zr$BU&OLO&D1z$u?Oqe1kzai!99Z6oimED~OE4w}T4h?ve8zy^n6fxa7MYpw;eW9+u RF#TP39+`jh^-Pw7{{!`w!>a%Q literal 0 HcmV?d00001 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..7e2d016324 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,172 @@ 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-XOR operation. (We could just as + -- well use bitwise-OR, but bitwise-XOR plays nicer with + -- how What4 represents bitvectors). In our running + -- example, `bfBV''` is 0b????1???. + bfBV'' <- W4.bvXorBits 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 +2374,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..728f743303 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,134 @@ 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, + -- counting from the least significant bit. + , 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 +499,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 From 98650f93b42fd31692f581c1405d6a6d598f1808 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 21 Dec 2021 17:46:46 -0500 Subject: [PATCH 2/3] Whitespace tweaks only --- src/SAWScript/Crucible/LLVM/Override.hs | 56 ++++++++++++------------- 1 file changed, 28 insertions(+), 28 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 7e2d016324..88a04eee87 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1427,12 +1427,12 @@ learnPointsTo :: , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => - Options -> - SharedContext -> - LLVMCrucibleContext arch -> - MS.CrucibleMethodSpecIR (LLVM arch) -> - PrePost -> - PointsTo (LLVM arch) -> + Options -> + SharedContext -> + LLVMCrucibleContext arch -> + MS.CrucibleMethodSpecIR (LLVM arch) -> + PrePost -> + PointsTo (LLVM arch) -> OverrideMatcher (LLVM arch) md (Maybe (PP.Doc ann)) learnPointsTo opts sc cc spec prepost (LLVMPointsTo loc maybe_cond ptr val) = do (_memTy, ptr1) <- resolveSetupValue opts cc sc spec Crucible.PtrRepr ptr @@ -1449,11 +1449,11 @@ matchPointsToValue :: , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => - Options -> - SharedContext -> - LLVMCrucibleContext arch -> - MS.CrucibleMethodSpecIR (LLVM arch) -> - PrePost -> + Options -> + SharedContext -> + LLVMCrucibleContext arch -> + MS.CrucibleMethodSpecIR (LLVM arch) -> + PrePost -> W4.ProgramLoc -> Maybe TypedTerm -> LLVMPtr (Crucible.ArchWidth arch) -> @@ -1550,11 +1550,11 @@ matchPointsToBitfieldValue :: , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => - Options -> - SharedContext -> - LLVMCrucibleContext arch -> - MS.CrucibleMethodSpecIR (LLVM arch) -> - PrePost -> + Options -> + SharedContext -> + LLVMCrucibleContext arch -> + MS.CrucibleMethodSpecIR (LLVM arch) -> + PrePost -> W4.ProgramLoc -> LLVMPtr (Crucible.ArchWidth arch) -> BitfieldIndex -> @@ -2342,11 +2342,11 @@ instantiateSetupValue sc s v = resolveSetupValueLLVM :: (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => - Options -> + Options -> LLVMCrucibleContext arch -> - SharedContext -> + SharedContext -> MS.CrucibleMethodSpecIR (LLVM arch) -> - SetupValue (LLVM arch) -> + SetupValue (LLVM arch) -> OverrideMatcher (LLVM arch) md (Crucible.MemType, LLVMVal) resolveSetupValueLLVM opts cc sc spec sval = do m <- OM (use setupValueSub) @@ -2361,12 +2361,12 @@ resolveSetupValueLLVM opts cc sc spec sval = resolveSetupValue :: (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => - Options -> + Options -> LLVMCrucibleContext arch -> - SharedContext -> + SharedContext -> MS.CrucibleMethodSpecIR (LLVM arch) -> Crucible.TypeRepr tp -> - SetupValue (LLVM arch) -> + SetupValue (LLVM arch) -> OverrideMatcher (LLVM arch) md (Crucible.MemType, Crucible.RegValue Sym tp) resolveSetupValue opts cc sc spec tp sval = do (memTy, lval) <- resolveSetupValueLLVM opts cc sc spec sval @@ -2379,11 +2379,11 @@ resolveSetupValue opts cc sc spec tp sval = -- for the salient details. resolveSetupValueBitfieldLLVM :: (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => - Options -> + Options -> LLVMCrucibleContext arch -> - SharedContext -> + SharedContext -> MS.CrucibleMethodSpecIR (LLVM arch) -> - SetupValue (LLVM arch) -> + SetupValue (LLVM arch) -> String -> OverrideMatcher (LLVM arch) md (BitfieldIndex, LLVMVal) resolveSetupValueBitfieldLLVM opts cc sc spec sval fieldName = @@ -2402,11 +2402,11 @@ resolveSetupValueBitfieldLLVM opts cc sc spec sval fieldName = -- 'resolveSetupValueBitfieldLLVM' for other differences. resolveSetupValueBitfield :: (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => - Options -> + Options -> LLVMCrucibleContext arch -> - SharedContext -> + SharedContext -> MS.CrucibleMethodSpecIR (LLVM arch) -> - SetupValue (LLVM arch) -> + SetupValue (LLVM arch) -> String -> OverrideMatcher (LLVM arch) md (BitfieldIndex, LLVMPtr (Crucible.ArchWidth arch)) resolveSetupValueBitfield opts cc sc spec sval fieldName = From cea41149ce5929d098ee50ef12936819ffb18f4d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 21 Dec 2021 18:00:46 -0500 Subject: [PATCH 3/3] Reference #338 in the FIXMEs adjacent to uses of noAlignment --- src/SAWScript/Crucible/LLVM/Override.hs | 8 ++++---- src/SAWScript/X86Spec.hs | 12 ++++++------ 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 88a04eee87..337ad7b284 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1467,7 +1467,7 @@ matchPointsToValue opts sc cc spec prepost loc maybe_cond ptr val = mem <- readGlobal $ Crucible.llvmMemVar $ ccLLVMContext cc - let alignment = Crucible.noAlignment -- default to byte alignment (FIXME) + let alignment = Crucible.noAlignment -- default to byte alignment (FIXME, see #338) case val of ConcreteSizeValue val' -> @@ -1566,7 +1566,7 @@ matchPointsToBitfieldValue opts sc cc spec prepost loc ptr bfIndex val = mem <- readGlobal $ Crucible.llvmMemVar $ ccLLVMContext cc - let alignment = Crucible.noAlignment -- default to byte alignment (FIXME) + let alignment = Crucible.noAlignment -- default to byte alignment (FIXME, see #338) -- Unlike in matchPointsToValue, we compute the MemTy/StorageType not from -- the RHS value, but from the BitfieldIndex. This is because we need to @@ -2037,7 +2037,7 @@ storePointsToValue :: storePointsToValue opts cc env tyenv nameEnv base_mem maybe_cond ptr val maybe_invalidate_msg = do let sym = cc ^. ccBackend - let alignment = Crucible.noAlignment -- default to byte alignment (FIXME) + let alignment = Crucible.noAlignment -- default to byte alignment (FIXME, see #338) smt_array_memory_model_enabled <- W4.getOpt =<< W4.getOptionSetting enableSMTArrayMemoryModel (W4.getConfiguration sym) @@ -2124,7 +2124,7 @@ storePointsToBitfieldValue :: 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) + let alignment = Crucible.noAlignment -- default to byte alignment (FIXME, see #338) smt_array_memory_model_enabled <- W4.getOpt =<< W4.getOptionSetting enableSMTArrayMemoryModel (W4.getConfiguration sym) diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs index b6c29adc78..badae2c0d0 100644 --- a/src/SAWScript/X86Spec.hs +++ b/src/SAWScript/X86Spec.hs @@ -510,7 +510,7 @@ setLoc l = let lty = llvmBytes w ty = locRepr l val <- packMemValue sym lty ty v - let alignment = noAlignment -- default to byte-aligned (FIXME) + let alignment = noAlignment -- default to byte-aligned (FIXME, see #338) mem1 <- storeConstRaw sym mem loc lty alignment val return s { stateMem = mem1 } @@ -885,7 +885,7 @@ setCryPost opts s (_nm,p) = do let ?ptrWidth = knownNat loc <- adjustPtr sym mem ptrV (bytesToInteger (i *. u)) val <- packMemValue sym llT cruT v - let alignment = noAlignment -- default to byte-aligned (FIXME) + let alignment = noAlignment -- default to byte-aligned (FIXME, see #338) storeConstRaw sym mem loc llT alignment val let cur = Proxy @p @@ -933,7 +933,7 @@ allocate sym ar s = do let ?ptrWidth = knownNat @64 let szInt = bytesToInteger (uncurry (*.) (areaSize ar)) sz <- bvLit sym knownNat (BV.mkBV knownNat szInt) - let alignment = noAlignment -- default to byte-aligned (FIXME) + let alignment = noAlignment -- default to byte-aligned (FIXME, see #338) (base,mem) <- doMalloc sym HeapAlloc mut (areaName ar) (stateMem s) sz alignment ptr <- adjustPtr sym mem base (bytesToInteger (areaPtr ar)) return (base,ptr,mem) @@ -960,7 +960,7 @@ fillFresh sym ptrOk p u todo mem = val <- packMemValue sym lty ty =<< freshVal sym ty ptrOk nm -- Here we use the write that ignore mutability. -- This is because we are writinging initialization code. - let alignment = noAlignment -- default to byte-aligned (FIXME) + let alignment = noAlignment -- default to byte-aligned (FIXME, see #338) mem1 <- storeConstRaw sym mem p lty alignment val p1 <- adjustPtr sym mem1 p elS fillFresh sym ptrOk p1 u more mem1 @@ -1070,7 +1070,7 @@ setupGlobals opts gs fs s let ?ptrWidth = knownNat @64 sz <- bvLit sym knownNat (BV.mkBV knownNat size) - let alignment = noAlignment -- default to byte-aligned (FIXME) + let alignment = noAlignment -- default to byte-aligned (FIXME, see #338) (p,mem) <- doMalloc sym GlobalAlloc Immutable "Globals" (stateMem s) sz alignment let Just base = asNat (fst (llvmPointerView p)) @@ -1146,7 +1146,7 @@ setupGlobals opts gs fs s z <- natLit sym 0 val <- LLVMValInt z <$> bvLit sym w (BV.mkBV w v) let ?ptrWidth = knownNat - let alignment = noAlignment -- default to byte-aligned (FIXME) + let alignment = noAlignment -- default to byte-aligned (FIXME, see #338) mem1 <- storeConstRaw sym mem p lty alignment val p1 <- adjustPtr sym mem1 p szI return (p1,mem1)