From f8e3ce8d06b9c8c7bb1ae824ea90d62bc12b986f Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 30 May 2023 17:12:42 -0400 Subject: [PATCH 1/7] `heapster-saw`: Simplify and document `translateLLVMGEP` The previous implementation of `translateLLVMGEP` was needlessly complicated, as it required the pointer argument to have a very particular shape to its type. But there's no good reason for this requirement, as the only thing that `translateLLVMGEP` _really_ needs to check for is that all of the index arguments are `0` (so that no pointer offset needs to be computed). I have simplified the implementation of `translateLLVMGEP` to reflect this and expanded its Haddocks accordingly. A secondary benefit of this change is that we no longer match on `PtrTo` in `translateLLVMGEP`, which will make it easier to support opaque pointers in an upcoming commit. Fixes #1875. --- .../Verifier/SAW/Heapster/LLVMGlobalConst.hs | 35 ++++++++++++------- 1 file changed, 22 insertions(+), 13 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs index 6df257516b..7dea55bbb7 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs @@ -189,23 +189,32 @@ translateLLVMConstExpr _ ce = traceAndZeroM ("translateLLVMConstExpr does not yet handle:\n" ++ ppLLVMConstExpr ce) --- | Helper function for 'translateLLVMValue' applied to a @getelemptr@ --- expression +-- | Helper function for 'translateLLVMValue' applied to a constant +-- @getelementptr@ expression. +-- +-- For now, we only support uses of @getelementptr@ where all indices are zero, +-- as this will return the pointer argument without needing to compute an offset +-- into the pointer. Of course, this does mean that any @getelementptr@ +-- expressions involving non-zero indices aren't supported (see #1875 for a +-- contrived example of this). Thankfully, this function is only used to +-- translate LLVM globals, and using @getelementptr@ to initialize globals is +-- quite rare in practice. As such, we choose to live with this limitation until +-- someone complains about it. translateLLVMGEP :: (1 <= w, KnownNat w) => NatRepr w -> L.Type -> (PermExpr (LLVMShapeType w), OpenTerm) -> [L.Typed L.Value] -> LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm) -translateLLVMGEP _ _ vtrans [] = return vtrans -translateLLVMGEP w (L.Array _ tp) vtrans (L.Typed _ (L.ValInteger 0) : ixs) = - translateLLVMGEP w tp vtrans ixs -translateLLVMGEP w (L.PtrTo tp) vtrans (L.Typed _ (L.ValInteger 0) : ixs) = - translateLLVMGEP w tp vtrans ixs -translateLLVMGEP w (L.PackedStruct [tp]) vtrans (L.Typed - _ (L.ValInteger 0) : ixs) = - translateLLVMGEP w tp vtrans ixs -translateLLVMGEP _ tp _ ixs = - traceAndZeroM ("translateLLVMGEP cannot handle arguments:\n" ++ - " " ++ intercalate "," (show tp : map show ixs)) +translateLLVMGEP _ tp vtrans ixs + | all (isZeroIdx . L.typedValue) ixs + = return vtrans + | otherwise + = traceAndZeroM ("translateLLVMGEP cannot handle arguments:\n" ++ + " " ++ intercalate "," (show tp : map show ixs)) + where + -- Check if an index is equal to 0. + isZeroIdx :: L.Value -> Bool + isZeroIdx (L.ValInteger 0) = True + isZeroIdx _ = False -- | Build an LLVM value for a @zeroinitializer@ field of the supplied type llvmZeroInitValue :: L.Type -> LLVMTransM (L.Value) From 4dfd2a41d664850fb191cc24b3e38c802878be90 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 30 May 2023 10:29:14 -0400 Subject: [PATCH 2/7] Adapt to ConstGEP gaining explicit basis type and expression This commit bumps the `llvm-pretty` submodule to bring in a commit from elliottt/llvm-pretty#110 that adds additional fields to `ConstGEP` to represent the basis type and expression to use for offset calculations. This also bumps the `llvm-pretty-bc-parser` and `crucible` submodule to bring in corresponding changes from GaloisInc/llvm-pretty-bc-parser#221 and GaloisInc/crucible#1085, respectively. This change affects one use site in `heapster-saw`, which is easily adapted. --- deps/crucible | 2 +- deps/llvm-pretty | 2 +- deps/llvm-pretty-bc-parser | 2 +- heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/deps/crucible b/deps/crucible index b4422dd2f7..a18468dfd2 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit b4422dd2f75f5a7310bc038a6ca67a91f3692a42 +Subproject commit a18468dfd2e48b3287d6d276faf6c7ecd33f3a8b diff --git a/deps/llvm-pretty b/deps/llvm-pretty index d099d5d0fe..16bc5bd5a0 160000 --- a/deps/llvm-pretty +++ b/deps/llvm-pretty @@ -1 +1 @@ -Subproject commit d099d5d0feab8066bc682f11c8a46c82fb7166b5 +Subproject commit 16bc5bd5a07d6e5d99c1c0f3a57b8eca2ecc944e diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser index 59e6991e1b..9ba94bb3d7 160000 --- a/deps/llvm-pretty-bc-parser +++ b/deps/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit 59e6991e1b89252d4a4aa28a84ab1ac022c18b8d +Subproject commit 9ba94bb3d7e01d710c1eea364ab0b84045c9df78 diff --git a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs index 7dea55bbb7..be82b7ebc8 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs @@ -178,7 +178,7 @@ translateLLVMType _ tp = -- | Helper function for 'translateLLVMValue' applied to a constant expression translateLLVMConstExpr :: (1 <= w, KnownNat w) => NatRepr w -> L.ConstExpr -> LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm) -translateLLVMConstExpr w (L.ConstGEP _ _ _ (L.Typed tp ptr : ixs)) = +translateLLVMConstExpr w (L.ConstGEP _ _ _ (L.Typed tp ptr) ixs) = translateLLVMValue w tp ptr >>= \ptr_trans -> translateLLVMGEP w tp ptr_trans ixs translateLLVMConstExpr w (L.ConstConv L.BitCast From 5f99422e40da153fc82e6b9a89b0f3ac92e9f2b7 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 30 May 2023 15:28:10 -0400 Subject: [PATCH 3/7] Support LLVM 15 and 16, opaque pointers This patch adds support for LLVM 15 and 16 by adding support for opaque pointers, which are described in https://llvm.org/docs/OpaquePointers.html. I have also added a test case involving LLVM bitcode using opaque pointers to kick the tires and ensure that the basics work as expected. For the most part, this is a straightforward process, as most uses of pointer types in SAW already do not care about pointee types. There are some exceptions, however: * The `typeOfSetupValue` function, as well as several places that use this function, scrutinize pointee types of pointers, which would appear to fly in the face of opaque pointers. I attempt to explain in #1876 which this is actually OK for now (although a bit awkward). * The `llvm_boilerplate`/skeleton machinery does not support opaque pointers at all. See #1877. * The `llvm_fresh_expanded_val` command does not support opaque pointers at all. See #1879. This patch also bumps the following submodules to bring in support for opaque pointers: * `llvm-pretty`: elliottt/llvm-pretty#110 * `llvm-pretty-bc-parser`: GaloisInc/llvm-pretty-bc-parser#221 * `crucible`: GaloisInc/crucible#1085 This also bumps the `what4` submodule to bring in the changes from GaloisInc/what4#234. This isn't necessary to support opaque pointers, but it _is_ necessary to support a build plan involving `tasty-sugar-2.2.*`, which `llvm-pretty-bc-parser`'s test suite now requires. --- CHANGES.md | 2 +- README.md | 2 +- deps/crucible | 2 +- deps/llvm-pretty | 2 +- deps/llvm-pretty-bc-parser | 2 +- deps/what4 | 2 +- doc/manual/manual.md | 2 +- .../Verifier/SAW/Heapster/LLVMGlobalConst.hs | 7 ++++--- intTests/test1132-opaque/Makefile | 13 +++++++++++++ intTests/test1132-opaque/test.bc | Bin 0 -> 3436 bytes intTests/test1132-opaque/test.c | 7 +++++++ intTests/test1132-opaque/test.saw | 11 +++++++++++ intTests/test1132-opaque/test.sh | 5 +++++ src/SAWScript/Crucible/LLVM/Builtins.hs | 13 +++++++++++-- src/SAWScript/Crucible/LLVM/Override.hs | 16 +++++++++++----- .../Crucible/LLVM/ResolveSetupValue.hs | 13 +++++++------ src/SAWScript/Crucible/LLVM/X86.hs | 2 +- 17 files changed, 77 insertions(+), 24 deletions(-) create mode 100644 intTests/test1132-opaque/Makefile create mode 100644 intTests/test1132-opaque/test.bc create mode 100644 intTests/test1132-opaque/test.c create mode 100644 intTests/test1132-opaque/test.saw create mode 100644 intTests/test1132-opaque/test.sh diff --git a/CHANGES.md b/CHANGES.md index e3d7b56f8d..e4518b8e1e 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -99,7 +99,7 @@ see the `mir_*` commands documented in the [SAW manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md). -* Support LLVM versions up to 14. +* Support LLVM versions up to 16. # Version 0.9 diff --git a/README.md b/README.md index 6d78db2fec..5f967bbde8 100644 --- a/README.md +++ b/README.md @@ -72,7 +72,7 @@ SAW can analyze LLVM programs (usually derived from C, but potentially for other languages). The only tool strictly required for this is a compiler that can generate LLVM bitcode, such as `clang`. However, having the full LLVM tool suite available can be useful. We have tested -SAW with LLVM and `clang` versions from 3.5 to 14.0, as well as the +SAW with LLVM and `clang` versions from 3.5 to 16.0, as well as the version of `clang` bundled with Apple Xcode. We welcome bug reports on any failure to parse bitcode from LLVM versions in that range. diff --git a/deps/crucible b/deps/crucible index a18468dfd2..b146bcf77a 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit a18468dfd2e48b3287d6d276faf6c7ecd33f3a8b +Subproject commit b146bcf77a8c69ea389e738f541eef91d4e98293 diff --git a/deps/llvm-pretty b/deps/llvm-pretty index 16bc5bd5a0..a454fcbe41 160000 --- a/deps/llvm-pretty +++ b/deps/llvm-pretty @@ -1 +1 @@ -Subproject commit 16bc5bd5a07d6e5d99c1c0f3a57b8eca2ecc944e +Subproject commit a454fcbe4192c07bcced2cf1384686dc7359a4a3 diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser index 9ba94bb3d7..65be0b0e38 160000 --- a/deps/llvm-pretty-bc-parser +++ b/deps/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit 9ba94bb3d7e01d710c1eea364ab0b84045c9df78 +Subproject commit 65be0b0e3898716b1e39659f3d3d49dcc5208d31 diff --git a/deps/what4 b/deps/what4 index ffbad75b1c..2d22d4afaf 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit ffbad75b1ce65577422a19a30a39a5059be8b95f +Subproject commit 2d22d4afaf141195bd4a43a9e5498c2b2e7eaa3d diff --git a/doc/manual/manual.md b/doc/manual/manual.md index b6c9727fd0..4dab9d048a 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -1580,7 +1580,7 @@ The resulting `LLVMModule` can be passed into the various functions described below to perform analysis of specific LLVM functions. The LLVM bitcode parser should generally work with LLVM versions between -3.5 and 14.0, though it may be incomplete for some versions. Debug +3.5 and 16.0, though it may be incomplete for some versions. Debug metadata has changed somewhat throughout that version range, so is the most likely case of incompleteness. We aim to support every version after 3.5, however, so report any parsing failures as [on diff --git a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs index be82b7ebc8..f470783359 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs @@ -182,9 +182,10 @@ translateLLVMConstExpr w (L.ConstGEP _ _ _ (L.Typed tp ptr) ixs) = translateLLVMValue w tp ptr >>= \ptr_trans -> translateLLVMGEP w tp ptr_trans ixs translateLLVMConstExpr w (L.ConstConv L.BitCast - (L.Typed tp@(L.PtrTo _) v) (L.PtrTo _)) = - -- A bitcast from one LLVM pointer type to another is a no-op for us - translateLLVMValue w tp v + (L.Typed fromTp v) toTp) + | L.isPointer fromTp && L.isPointer toTp + = -- A bitcast from one LLVM pointer type to another is a no-op for us + translateLLVMValue w fromTp v translateLLVMConstExpr _ ce = traceAndZeroM ("translateLLVMConstExpr does not yet handle:\n" ++ ppLLVMConstExpr ce) diff --git a/intTests/test1132-opaque/Makefile b/intTests/test1132-opaque/Makefile new file mode 100644 index 0000000000..a639efae03 --- /dev/null +++ b/intTests/test1132-opaque/Makefile @@ -0,0 +1,13 @@ +# NB: Ensure that clang-15 or later is used so that the resulting LLVM bitcode +# uses opaque pointers. +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/test1132-opaque/test.bc b/intTests/test1132-opaque/test.bc new file mode 100644 index 0000000000000000000000000000000000000000..57dd28b8f4754af288479bfe85fb019fcad194ad GIT binary patch literal 3436 zcma)9eN0=|6~Fd#{7f+KnUQ$QG%NnpRZHhM(eb1r>us7@k!B5sud9}`>e-~GD9Vz<7lbex9nK0N zr7##E;u#^96~an#Bu)+oh=B`agcZUt+k_A;g61}2u4`4B>#D`1X4$P;o7A8ebA&xW z*t0|eCdmj99XS#pB03?I6-F{bc!G3S&5L$#C#pWrskS-IX0qz@ta@3rd&ymOmD4N& z>(*SIRBeI++P%F-p;MZ#X4H$5FiP{4$SQ#|hhCrj>Kb689#Y6>%@PTIEMv`#y1)1sEk&L=Mst>dW{w4S53kmA-h)#spZE2wQm z-&mur6{R;7)ZGMyS{IzH)Y&?bvcWvlGcD&+ zKN%+yBxXt-mBxy~jTFyCbMQ7cF)0QS$KTEZY=UdPT zmb#Z9d#9vV6Z9R1hR)3*buTA9!P0kJ6tH(#`b!2YfLaVG?z-q(E~<~Ewq0}%R=2|j z&gZSDZd8oURteu=YYApYWV_TshXF$pz|g~K$Am)uu=Fj(qw<4V;8}c7_jcH`Da!>i z)=9?V!pV?eaSPFqFp?82Rx)-$sQNuDRis9sMRYhshO%S?P{fkqqI8=fV~SG0BrGe0 zv*eJ29C4G;qVxu|CAQB^#SuB8Aj1i=Z;gs)$pQEMfuP*SRt_*^JX<}RnLp6+TZ81fsfTpf7w>}NUx1or3Dw-X%3mXD9d%mM`LXr{IUFY=69e+Ah%SS` zEN|D$&Zs}0RQcH*CACx?00NLPMzj{0C3P=%3H^s)=|Pfo;Sdv-=DI7M%btF^7ng$P$$GyDjFc;aQ;dmniXn4euln< z=-V!8Ged1S0M^tNSi$JjD>IteHq8~S3i8g%8U(-kE0M;pJZhbCK6x%>FSr`+8{!sX zaWXz}^vK-|jXj`wL9@uIu4~n+GwNT9G<%)j_O| zIc|vZhCz9zl+gcu6*9s?9aLi>P z)2Y|mG^;Zze}k8$aE4-Om;`3f5>ZH_01QAyTo`~945=C8f0#k&4WMC72jd)-*H(m0 z9ZY?4?97=@4`dZOUyISy{(46H_5$lBUV1zsvNfGO+i>V%I?6|)jb1~bzmGSBBi{aK z)Nr8RJJ`nuqY*;~=RMIA>;@V+!T0tWB3w)#@rHXsQA1BKdJKj}40r;g(QMN9hq!@3 zzRA+;_gl^TjXdYuZ?zeDi^b|OHJkiR7E2RrYWDVW!ER=V4@Y|XgN(7ck!@rdU3X8^ z0W~n_Y4rB@J=xnk)MvnrJ{0bMf%irm;Um-J;VhiZYx7&0Jsz*s<6|wn+0tzCdQ7a} z*W~kitxXoAdH-VvVqDnIJXc=h0Ph*>W)27a{SPEDZ-5JTMS4bf*I_4fgdgI2U5B44 zcLrlo&eO~L!(1P)5A}nUeE9#I^Gv@#3e)q3k|9r&Hd(g9;OPmLrFvsCqwi+)d|yvg zk2M&*Kg@gk!#+J&*T)5Y`re)(&*-0K8NHV&9|5E9FZVp&dfEHzsgR;xcF1@tqy!EK z<9uG^tcC-=pYY(gS(ixC&KB6F)8_oPvM6^(JIwN`+aUPBoGS>T{_f^$7hnHV;k_~aR&Q`T^@od5 z7Be_p%CWwyX~RujbK#qD6DN|={Wz6KlEVP!GM3Bn-5ENUw@!=f=TmUWicdhYRKeq9 zg;8yCxV@g#%yO#Yq-voYl-!JnzRS?-E*f9fP(D?_`wl2sfcw~f4iX*FnuS}|Y0c!Z z>o^AACvf*k+V+8J=?!>nucPxA^uJ*ddJgEGLkpRskB;>~7qzJpGm}zxrU?f74TF&| zAm7_N=;IA>tEJ1*gimrXuI~;G!udluM4~)k$(ymTK{~G$(bR z+jA~i>q^(bReP~=tU{c_8s_TUKxTGIRIQM(o)BVWQpwxj;it;i(9r*Y=BEW^O*$$? ztjDE*&+{hWcZ8+LAX*7y|7fOW(jVGY@5Haq?He#Jepc&g7qJi2j4NpFE!Lq9)od-Wtd{QY#%~6 z^zobzXh{zGxcn0KtO5#q-o(5g=bT2Lr@PU|Lz)WneOzyEzxRH!{h?{}KE4NoCxZR4 N;Qw%5PFHxH{{k3ZcrpM0 literal 0 HcmV?d00001 diff --git a/intTests/test1132-opaque/test.c b/intTests/test1132-opaque/test.c new file mode 100644 index 0000000000..a02777bd88 --- /dev/null +++ b/intTests/test1132-opaque/test.c @@ -0,0 +1,7 @@ +#include +#include + +void f(uint8_t **x) { + *x = malloc(sizeof(uint8_t)); + **x = 42; +} diff --git a/intTests/test1132-opaque/test.saw b/intTests/test1132-opaque/test.saw new file mode 100644 index 0000000000..91d5afa1cf --- /dev/null +++ b/intTests/test1132-opaque/test.saw @@ -0,0 +1,11 @@ +bc <- llvm_load_module "test.bc"; + +let f_contract = do { + x <- llvm_alloc (llvm_pointer (llvm_int 8)); + llvm_execute_func [x]; + p <- llvm_alloc (llvm_int 8); + llvm_points_to x p; + llvm_points_to p (llvm_term {{ 42 : [8] }}); +}; + +llvm_verify bc "f" [] false f_contract abc; diff --git a/intTests/test1132-opaque/test.sh b/intTests/test1132-opaque/test.sh new file mode 100644 index 0000000000..06d9f2a4ae --- /dev/null +++ b/intTests/test1132-opaque/test.sh @@ -0,0 +1,5 @@ +# A variant of test1132 that instead uses opaque pointers to ensure that the +# basics of SAW work in an opaque pointer context. +set -e + +$SAW test.saw diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index aa8591b13a..402c5404bd 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -2124,15 +2124,24 @@ cryptolTypeOfActual dl mt = do cty <- cryptolTypeOfActual dl ty return $ Cryptol.tSeq (Cryptol.tNum n) cty Crucible.PtrType _ -> - return $ Cryptol.tWord (Cryptol.tNum (Crucible.ptrBitwidth dl)) + return cryptolPtrType + Crucible.PtrOpaqueType -> + return cryptolPtrType Crucible.StructType si -> do let memtypes = V.toList (Crucible.siFieldTypes si) ctys <- traverse (cryptolTypeOfActual dl) memtypes case ctys of [cty] -> return cty _ -> return $ Cryptol.tTuple ctys - _ -> + Crucible.X86_FP80Type -> Nothing + Crucible.VecType{} -> + Nothing + Crucible.MetadataType -> + Nothing + where + cryptolPtrType :: Cryptol.Type + cryptolPtrType = Cryptol.tWord (Cryptol.tNum (Crucible.ptrBitwidth dl)) -- | Generate a fresh variable term. The name will be used when -- pretty-printing the variable in debug output. diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 6c9359aaa5..d193f73864 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1241,9 +1241,15 @@ diffMemTypes x0 y0 = (Crucible.IntType x, Crucible.IntType y) | x == y -> [] (Crucible.FloatType, Crucible.FloatType) -> [] (Crucible.DoubleType, Crucible.DoubleType) -> [] - (Crucible.PtrType{}, Crucible.PtrType{}) -> [] - (Crucible.IntType w, Crucible.PtrType{}) | w == wptr -> [] - (Crucible.PtrType{}, Crucible.IntType w) | w == wptr -> [] + (_, _) + | Crucible.isPointerMemType x0 && Crucible.isPointerMemType y0 -> + [] + (Crucible.IntType w, _) + | Crucible.isPointerMemType y0 && w == wptr -> + [] + (_, Crucible.IntType w) + | Crucible.isPointerMemType x0 && w == wptr -> + [] (Crucible.ArrayType xn xt, Crucible.ArrayType yn yt) | xn == yn -> [ (Nothing : path, l , r) | (path, l, r) <- diffMemTypes xt yt ] @@ -1314,7 +1320,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = (V.toList (Crucible.fiType <$> Crucible.siFields fields)) zs ] - (Crucible.LLVMValInt blk off, Crucible.PtrType _, SetupElem () v i) -> + (Crucible.LLVMValInt blk off, _, SetupElem () v i) | Crucible.isPointerMemType expectedTy -> do let tyenv = MS.csAllocations cs nameEnv = MS.csTypeNames cs delta <- exceptToFail $ resolveSetupElemOffset cc tyenv nameEnv v i @@ -1322,7 +1328,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = =<< W4.bvLit sym (W4.bvWidth off) (Crucible.bytesToBV (W4.bvWidth off) delta) matchArg opts sc cc cs prepost md (Crucible.LLVMValInt blk off') expectedTy v - (Crucible.LLVMValInt blk off, Crucible.PtrType _, SetupField () v n) -> + (Crucible.LLVMValInt blk off, _, SetupField () v n) | Crucible.isPointerMemType expectedTy -> do let tyenv = MS.csAllocations cs nameEnv = MS.csTypeNames cs fld <- exceptToFail $ diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index c9d7647ddc..9223c5b909 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -473,8 +473,8 @@ typeOfSetupValue cc env nameEnv val = SetupCast () v ltp -> do memTy <- typeOfSetupValue cc env nameEnv v - case memTy of - Crucible.PtrType _symTy -> + if Crucible.isPointerMemType memTy + then case let ?lc = lc in Crucible.liftMemType (L.PtrTo ltp) of Left err -> throwError $ unlines [ "typeOfSetupValue: invalid type " ++ show ltp @@ -483,10 +483,11 @@ typeOfSetupValue cc env nameEnv val = ] Right mt -> pure mt - _ -> throwError $ unwords $ - [ "typeOfSetupValue: tried to cast the type of a non-pointer value" - , "actual type of value: " ++ show memTy - ] + else + throwError $ unwords $ + [ "typeOfSetupValue: tried to cast the type of a non-pointer value" + , "actual type of value: " ++ show memTy + ] SetupElem () v i -> do do memTy <- typeOfSetupValue cc env nameEnv v diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 5c2e738a84..8cadba3856 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -1158,7 +1158,7 @@ setArgs env tyenv nameEnv args let setRegSetupValue rs (reg, sval) = exceptToFail (typeOfSetupValue cc tyenv nameEnv sval) >>= \case - C.LLVM.PtrType _ -> do + ty | C.LLVM.isPointerMemType ty -> do val <- C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64) =<< resolveSetupVal cc mem env tyenv nameEnv sval setReg reg val rs From b927837cacaf7bec60d9bc0d05df0a1633ec18c3 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 31 May 2023 10:24:00 -0400 Subject: [PATCH 4/7] Do not support opaque pointers in type skeletons for now See #1877 for further discussion. --- src/SAWScript/Crucible/LLVM/Skeleton.hs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/SAWScript/Crucible/LLVM/Skeleton.hs b/src/SAWScript/Crucible/LLVM/Skeleton.hs index d55d5cf71b..60ae01aacf 100644 --- a/src/SAWScript/Crucible/LLVM/Skeleton.hs +++ b/src/SAWScript/Crucible/LLVM/Skeleton.hs @@ -98,6 +98,13 @@ makeLenses ''ModuleSkeleton parseType :: LLVM.Type -> IO TypeSkeleton parseType (LLVM.PtrTo t) = pure $ TypeSkeleton t True [SizeGuess 1 True "default guess of size 1"] +-- It is unclear how to combine opaque pointers with type skeletons due to the +-- lack of a pointee type. For now, we simply fail if we encounter one +-- (see #1877). +parseType LLVM.PtrOpaque = fail $ unlines + [ "Skeleton generation does not support opaque pointers." + , "You should report this issue at: https://github.com/GaloisInc/saw-script/issues/1877" + ] parseType (LLVM.Array i t) = pure $ TypeSkeleton t True [ SizeGuess (fromIntegral i) True $ "default guess of size " <> Text.pack (show i) ] From 18e39464651342fd539f435cac5d49f151a784e1 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 1 Jun 2023 08:12:27 -0400 Subject: [PATCH 5/7] Do not support opaque pointers in `llvm_fresh_expanded_val` for now See #1879 for further discussion. --- src/SAWScript/Crucible/LLVM/Builtins.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 402c5404bd..3c7c34661d 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -2236,6 +2236,9 @@ constructExpandedSetupValue cc sc loc t = Crucible.MetadataType -> failUnsupportedType "Metadata" Crucible.VecType{} -> failUnsupportedType "Vec" Crucible.X86_FP80Type{} -> failUnsupportedType "X86_FP80" + -- See https://github.com/GaloisInc/saw-script/issues/1879 for why it is + -- tricky to support opaque pointers here. + Crucible.PtrOpaqueType -> failUnsupportedType "PtrOpaque" where failUnsupportedType tyName = throwCrucibleSetup loc $ unwords ["llvm_fresh_expanded_var: " ++ tyName ++ " not supported"] From b7ae243dd440583e3bd259a6cb3441c8325b10aa Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 31 May 2023 11:02:06 -0400 Subject: [PATCH 6/7] CI: Regenerate cabal.GHC-*.config files --- cabal.GHC-8.10.7.config | 39 ++++++++++++++++----------------------- cabal.GHC-9.2.7.config | 39 ++++++++++++++++----------------------- cabal.GHC-9.4.4.config | 39 ++++++++++++++++----------------------- 3 files changed, 48 insertions(+), 69 deletions(-) diff --git a/cabal.GHC-8.10.7.config b/cabal.GHC-8.10.7.config index 3818a165ee..7f3965322a 100644 --- a/cabal.GHC-8.10.7.config +++ b/cabal.GHC-8.10.7.config @@ -18,8 +18,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.adjunctions ==4.4.2, any.aeson ==2.1.2.1, aeson -cffi +ordered-keymap, - any.aeson-typescript ==0.5.0.0, - any.alex ==3.2.7.3, + any.alex ==3.2.7.4, any.ansi-terminal ==0.11.5, ansi-terminal -example, any.ansi-terminal-types ==0.11.5, @@ -119,7 +118,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.doctest ==0.20.1, any.dotgen ==0.4.3, dotgen -devel, - any.easy-file ==0.2.3, + any.easy-file ==0.2.5, any.either ==5.0.2, any.entropy ==0.4.1.10, entropy -donotgetentropy, @@ -140,7 +139,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.foldable1-classes-compat ==0.1, foldable1-classes-compat +tagged, any.free ==5.2, - any.generic-deriving ==1.14.3, + any.generic-deriving ==1.14.4, generic-deriving +base-4-9, any.generic-lens ==2.2.2.0, any.generic-lens-core ==2.2.1.0, @@ -154,7 +153,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.ghc-paths ==0.1.0.12, any.ghc-prim ==0.6.1, any.ghci ==8.10.7, - any.githash ==0.1.6.3, any.gitrev ==1.3.1, any.graphviz ==2999.20.1.0, graphviz -test-parsing, @@ -178,9 +176,10 @@ constraints: any.BoundedChan ==1.0.3.0, any.hpc ==0.6.1.0, any.hsc2hs ==0.68.9, hsc2hs -in-ghc-tree, - any.hspec ==2.10.10, - any.hspec-core ==2.10.10, - any.hspec-discover ==2.10.10, + any.hspec ==2.11.0.1, + any.hspec-api ==2.11.0.1, + any.hspec-core ==2.11.0.1, + any.hspec-discover ==2.11.0.1, any.hspec-expectations ==0.8.2, any.http-date ==0.0.11, any.http-types ==0.12.3, @@ -220,7 +219,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.lifted-async ==0.10.2.4, any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, - any.logict ==0.8.0.0, + any.logict ==0.8.1.0, any.lucid ==2.11.20230408, any.lumberjack ==1.0.2.0, any.math-functions ==0.3.4.2, @@ -230,7 +229,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.memory ==0.18.0, memory +support_bytestring +support_deepseq, any.microlens ==0.4.13.1, - any.microlens-th ==0.4.3.12, + any.microlens-th ==0.4.3.13, any.microstache ==1.0.2.3, any.mmorph ==1.2.0, any.mod ==0.1.2.2, @@ -242,7 +241,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.mono-traversable ==1.0.15.3, any.mtl ==2.2.2, any.mwc-random ==0.15.0.2, - any.network ==3.1.2.8, + any.network ==3.1.2.9, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.1, @@ -252,8 +251,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.old-time ==1.1.0.3, any.optparse-applicative ==0.16.1.0, optparse-applicative +process, - any.optparse-simple ==0.1.1.4, - optparse-simple -build-example, any.ordered-containers ==0.2.3, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, @@ -297,17 +294,16 @@ constraints: any.BoundedChan ==1.0.3.0, any.scotty ==0.12.1, any.semialign ==1.3, semialign +semigroupoids, - any.semigroupoids ==5.3.7, + any.semigroupoids ==6.0.0.1, semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, any.semigroups ==0.20, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, any.semirings ==0.6, semirings +containers +unordered-containers, - any.setenv ==0.1.1.3, any.silently ==1.2.5.3, any.simple-get-opt ==0.4, - any.simple-sendfile ==0.2.30, - simple-sendfile +allow-bsd, + any.simple-sendfile ==0.2.31, + simple-sendfile +allow-bsd -fallback, any.simple-smt ==0.9.7, any.smallcheck ==1.2.1, any.split ==0.2.3.5, @@ -318,8 +314,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.streaming-commons ==0.2.2.6, streaming-commons -use-bytestring-builder, any.strict ==0.5, - any.string-interpolate ==0.3.2.0, - string-interpolate -bytestring-builder -extended-benchmarks -text-builder, any.syb ==0.7.2.3, any.tagged ==0.8.7, tagged +deepseq +transformers, @@ -331,11 +325,11 @@ constraints: any.BoundedChan ==1.0.3.0, any.tasty-golden ==2.3.5, tasty-golden -build-example, any.tasty-hedgehog ==1.4.0.1, - any.tasty-hspec ==1.2.0.3, + any.tasty-hspec ==1.2.0.4, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.2, any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==2.1.0.0, + any.tasty-sugar ==2.2.0.0, any.template-haskell ==2.16.0.0, any.temporary ==1.3, any.terminal-size ==0.3.3, @@ -344,7 +338,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.test-framework-hunit ==0.3.0.2, test-framework-hunit -base3 +base4, any.text ==1.2.4.1, - any.text-conversions ==0.3.1.1, any.text-short ==0.1.5, text-short -asserts, any.tf-random ==0.5, @@ -418,4 +411,4 @@ constraints: any.BoundedChan ==1.0.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2023-04-18T11:48:49Z +index-state: hackage.haskell.org 2023-05-08T16:29:53Z diff --git a/cabal.GHC-9.2.7.config b/cabal.GHC-9.2.7.config index 81c75892c2..d2e57716d1 100644 --- a/cabal.GHC-9.2.7.config +++ b/cabal.GHC-9.2.7.config @@ -18,8 +18,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.adjunctions ==4.4.2, any.aeson ==2.1.2.1, aeson -cffi +ordered-keymap, - any.aeson-typescript ==0.5.0.0, - any.alex ==3.2.7.3, + any.alex ==3.2.7.4, any.ansi-terminal ==0.11.5, ansi-terminal -example, any.ansi-terminal-types ==0.11.5, @@ -119,7 +118,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.doctest ==0.20.1, any.dotgen ==0.4.3, dotgen -devel, - any.easy-file ==0.2.3, + any.easy-file ==0.2.5, any.either ==5.0.2, any.entropy ==0.4.1.10, entropy -donotgetentropy, @@ -140,7 +139,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.foldable1-classes-compat ==0.1, foldable1-classes-compat +tagged, any.free ==5.2, - any.generic-deriving ==1.14.3, + any.generic-deriving ==1.14.4, generic-deriving +base-4-9, any.generic-lens ==2.2.2.0, any.generic-lens-core ==2.2.1.0, @@ -155,7 +154,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.ghc-paths ==0.1.0.12, any.ghc-prim ==0.8.0, any.ghci ==9.2.7, - any.githash ==0.1.6.3, any.gitrev ==1.3.1, any.graphviz ==2999.20.1.0, graphviz -test-parsing, @@ -179,9 +177,10 @@ constraints: any.BoundedChan ==1.0.3.0, any.hpc ==0.6.1.0, any.hsc2hs ==0.68.9, hsc2hs -in-ghc-tree, - any.hspec ==2.10.10, - any.hspec-core ==2.10.10, - any.hspec-discover ==2.10.10, + any.hspec ==2.11.0.1, + any.hspec-api ==2.11.0.1, + any.hspec-core ==2.11.0.1, + any.hspec-discover ==2.11.0.1, any.hspec-expectations ==0.8.2, any.http-date ==0.0.11, any.http-types ==0.12.3, @@ -221,7 +220,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.lifted-async ==0.10.2.4, any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, - any.logict ==0.8.0.0, + any.logict ==0.8.1.0, any.lucid ==2.11.20230408, any.lumberjack ==1.0.2.0, any.math-functions ==0.3.4.2, @@ -231,7 +230,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.memory ==0.18.0, memory +support_bytestring +support_deepseq, any.microlens ==0.4.13.1, - any.microlens-th ==0.4.3.12, + any.microlens-th ==0.4.3.13, any.microstache ==1.0.2.3, any.mmorph ==1.2.0, any.mod ==0.2.0.1, @@ -243,7 +242,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.mono-traversable ==1.0.15.3, any.mtl ==2.2.2, any.mwc-random ==0.15.0.2, - any.network ==3.1.2.8, + any.network ==3.1.2.9, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.1, @@ -253,8 +252,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.old-time ==1.1.0.3, any.optparse-applicative ==0.16.1.0, optparse-applicative +process, - any.optparse-simple ==0.1.1.4, - optparse-simple -build-example, any.ordered-containers ==0.2.3, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, @@ -298,17 +295,16 @@ constraints: any.BoundedChan ==1.0.3.0, any.scotty ==0.12.1, any.semialign ==1.3, semialign +semigroupoids, - any.semigroupoids ==5.3.7, + any.semigroupoids ==6.0.0.1, semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, any.semigroups ==0.20, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, any.semirings ==0.6, semirings +containers +unordered-containers, - any.setenv ==0.1.1.3, any.silently ==1.2.5.3, any.simple-get-opt ==0.4, - any.simple-sendfile ==0.2.30, - simple-sendfile +allow-bsd, + any.simple-sendfile ==0.2.31, + simple-sendfile +allow-bsd -fallback, any.simple-smt ==0.9.7, any.smallcheck ==1.2.1, any.split ==0.2.3.5, @@ -319,8 +315,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.streaming-commons ==0.2.2.6, streaming-commons -use-bytestring-builder, any.strict ==0.5, - any.string-interpolate ==0.3.2.0, - string-interpolate -bytestring-builder -extended-benchmarks -text-builder, any.syb ==0.7.2.3, any.tagged ==0.8.7, tagged +deepseq +transformers, @@ -332,11 +326,11 @@ constraints: any.BoundedChan ==1.0.3.0, any.tasty-golden ==2.3.5, tasty-golden -build-example, any.tasty-hedgehog ==1.4.0.1, - any.tasty-hspec ==1.2.0.3, + any.tasty-hspec ==1.2.0.4, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.2, any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==2.1.0.0, + any.tasty-sugar ==2.2.0.0, any.template-haskell ==2.18.0.0, any.temporary ==1.3, any.terminal-size ==0.3.3, @@ -345,7 +339,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.test-framework-hunit ==0.3.0.2, test-framework-hunit -base3 +base4, any.text ==1.2.5.0, - any.text-conversions ==0.3.1.1, any.text-short ==0.1.5, text-short -asserts, any.tf-random ==0.5, @@ -419,4 +412,4 @@ constraints: any.BoundedChan ==1.0.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2023-04-18T11:48:49Z +index-state: hackage.haskell.org 2023-05-08T16:29:53Z diff --git a/cabal.GHC-9.4.4.config b/cabal.GHC-9.4.4.config index 241bb28fce..5063584852 100644 --- a/cabal.GHC-9.4.4.config +++ b/cabal.GHC-9.4.4.config @@ -19,8 +19,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.adjunctions ==4.4.2, any.aeson ==2.1.2.1, aeson -cffi +ordered-keymap, - any.aeson-typescript ==0.5.0.0, - any.alex ==3.2.7.3, + any.alex ==3.2.7.4, any.ansi-terminal ==0.11.5, ansi-terminal -example, any.ansi-terminal-types ==0.11.5, @@ -119,7 +118,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.doctest ==0.20.1, any.dotgen ==0.4.3, dotgen -devel, - any.easy-file ==0.2.3, + any.easy-file ==0.2.5, any.either ==5.0.2, any.entropy ==0.4.1.10, entropy -donotgetentropy, @@ -140,7 +139,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.foldable1-classes-compat ==0.1, foldable1-classes-compat +tagged, any.free ==5.2, - any.generic-deriving ==1.14.3, + any.generic-deriving ==1.14.4, generic-deriving +base-4-9, any.generic-lens ==2.2.2.0, any.generic-lens-core ==2.2.1.0, @@ -155,7 +154,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.ghc-paths ==0.1.0.12, any.ghc-prim ==0.9.0, any.ghci ==9.4.4, - any.githash ==0.1.6.3, any.gitrev ==1.3.1, any.graphviz ==2999.20.1.0, graphviz -test-parsing, @@ -179,9 +177,10 @@ constraints: any.BoundedChan ==1.0.3.0, any.hpc ==0.6.1.0, any.hsc2hs ==0.68.9, hsc2hs -in-ghc-tree, - any.hspec ==2.10.10, - any.hspec-core ==2.10.10, - any.hspec-discover ==2.10.10, + any.hspec ==2.11.0.1, + any.hspec-api ==2.11.0.1, + any.hspec-core ==2.11.0.1, + any.hspec-discover ==2.11.0.1, any.hspec-expectations ==0.8.2, any.http-date ==0.0.11, any.http-types ==0.12.3, @@ -221,7 +220,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.lifted-async ==0.10.2.4, any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, - any.logict ==0.8.0.0, + any.logict ==0.8.1.0, any.lucid ==2.11.20230408, any.lumberjack ==1.0.2.0, any.math-functions ==0.3.4.2, @@ -231,7 +230,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.memory ==0.18.0, memory +support_bytestring +support_deepseq, any.microlens ==0.4.13.1, - any.microlens-th ==0.4.3.12, + any.microlens-th ==0.4.3.13, any.microstache ==1.0.2.3, any.mmorph ==1.2.0, any.mod ==0.2.0.1, @@ -243,7 +242,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.mono-traversable ==1.0.15.3, any.mtl ==2.2.2, any.mwc-random ==0.15.0.2, - any.network ==3.1.2.8, + any.network ==3.1.2.9, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.1, @@ -253,8 +252,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.old-time ==1.1.0.3, any.optparse-applicative ==0.16.1.0, optparse-applicative +process, - any.optparse-simple ==0.1.1.4, - optparse-simple -build-example, any.ordered-containers ==0.2.3, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, @@ -298,17 +295,16 @@ constraints: any.BoundedChan ==1.0.3.0, any.scotty ==0.12.1, any.semialign ==1.3, semialign +semigroupoids, - any.semigroupoids ==5.3.7, + any.semigroupoids ==6.0.0.1, semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, any.semigroups ==0.20, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, any.semirings ==0.6, semirings +containers +unordered-containers, - any.setenv ==0.1.1.3, any.silently ==1.2.5.3, any.simple-get-opt ==0.4, - any.simple-sendfile ==0.2.30, - simple-sendfile +allow-bsd, + any.simple-sendfile ==0.2.31, + simple-sendfile +allow-bsd -fallback, any.simple-smt ==0.9.7, any.smallcheck ==1.2.1, any.split ==0.2.3.5, @@ -319,8 +315,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.streaming-commons ==0.2.2.6, streaming-commons -use-bytestring-builder, any.strict ==0.5, - any.string-interpolate ==0.3.2.0, - string-interpolate -bytestring-builder -extended-benchmarks -text-builder, any.syb ==0.7.2.3, any.tagged ==0.8.7, tagged +deepseq +transformers, @@ -332,11 +326,11 @@ constraints: any.BoundedChan ==1.0.3.0, any.tasty-golden ==2.3.5, tasty-golden -build-example, any.tasty-hedgehog ==1.4.0.1, - any.tasty-hspec ==1.2.0.3, + any.tasty-hspec ==1.2.0.4, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.2, any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==2.1.0.0, + any.tasty-sugar ==2.2.0.0, any.template-haskell ==2.19.0.0, any.temporary ==1.3, any.terminal-size ==0.3.3, @@ -345,7 +339,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.test-framework-hunit ==0.3.0.2, test-framework-hunit -base3 +base4, any.text ==2.0.1, - any.text-conversions ==0.3.1.1, any.text-short ==0.1.5, text-short -asserts, any.tf-random ==0.5, @@ -419,4 +412,4 @@ constraints: any.BoundedChan ==1.0.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2023-04-18T11:48:49Z +index-state: hackage.haskell.org 2023-05-08T16:29:53Z From 6ccc9342bac7ad9452205add3e3d7d2365f18757 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 1 Jun 2023 16:23:32 -0400 Subject: [PATCH 7/7] Upgrade opaque pointer-related failures to panics This way, users who encounter them in the wild will be more strongly encouraged to report it on the issue tracker. --- src/SAWScript/Crucible/LLVM/Builtins.hs | 6 +++++- src/SAWScript/Crucible/LLVM/Skeleton.hs | 11 +++++++---- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 3c7c34661d..3ddc66f29b 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -2238,7 +2238,11 @@ constructExpandedSetupValue cc sc loc t = Crucible.X86_FP80Type{} -> failUnsupportedType "X86_FP80" -- See https://github.com/GaloisInc/saw-script/issues/1879 for why it is -- tricky to support opaque pointers here. - Crucible.PtrOpaqueType -> failUnsupportedType "PtrOpaque" + Crucible.PtrOpaqueType -> + panic "SAWScript.Crucible.LLVM.Builtins.constructExpandedSetupValue" + [ "llvm_fresh_expanded_val does not support opaque pointers" + , "Please report this at: https://github.com/GaloisInc/saw-script/issues/1879" + ] where failUnsupportedType tyName = throwCrucibleSetup loc $ unwords ["llvm_fresh_expanded_var: " ++ tyName ++ " not supported"] diff --git a/src/SAWScript/Crucible/LLVM/Skeleton.hs b/src/SAWScript/Crucible/LLVM/Skeleton.hs index 60ae01aacf..d9c2b22df5 100644 --- a/src/SAWScript/Crucible/LLVM/Skeleton.hs +++ b/src/SAWScript/Crucible/LLVM/Skeleton.hs @@ -39,6 +39,8 @@ import qualified Data.Set as Set import qualified Text.LLVM as LLVM import qualified Text.LLVM.DebugUtils as LLVM +import SAWScript.Panic (panic) + -------------------------------------------------------------------------------- -- ** Skeletons @@ -101,10 +103,11 @@ parseType (LLVM.PtrTo t) = pure $ TypeSkeleton t True [SizeGuess 1 True "default -- It is unclear how to combine opaque pointers with type skeletons due to the -- lack of a pointee type. For now, we simply fail if we encounter one -- (see #1877). -parseType LLVM.PtrOpaque = fail $ unlines - [ "Skeleton generation does not support opaque pointers." - , "You should report this issue at: https://github.com/GaloisInc/saw-script/issues/1877" - ] +parseType LLVM.PtrOpaque = + panic "SAWScript.Crucible.LLVM.Skeleton.parseType" + [ "Skeleton generation does not support opaque pointers" + , "Please report this at: https://github.com/GaloisInc/saw-script/issues/1877" + ] parseType (LLVM.Array i t) = pure $ TypeSkeleton t True [ SizeGuess (fromIntegral i) True $ "default guess of size " <> Text.pack (show i) ]