From 5f99422e40da153fc82e6b9a89b0f3ac92e9f2b7 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 30 May 2023 15:28:10 -0400 Subject: [PATCH] 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