From c0ed1a049930917e6a58ecf98e1fcddfc74b6ea9 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 6 Dec 2021 13:59:52 -0500 Subject: [PATCH] x86: Pass the right nameEnv in resolvePtrSetupValue Previously, `resolvePtrSetupValue` would pass an empty `Map` of `Ident` to `resolveSetupVal`, which prevented SAW from lookup up struct field names properly. The fix is quite straightforward, luckily enough. Fixes #1533. --- .gitignore | 1 + intTests/test1533/Makefile | 17 +++++++++++++++++ intTests/test1533/test.bc | Bin 0 -> 3068 bytes intTests/test1533/test.c | 14 ++++++++++++++ intTests/test1533/test.exe | Bin 0 -> 17448 bytes intTests/test1533/test.saw | 14 ++++++++++++++ intTests/test1533/test.sh | 5 +++++ src/SAWScript/Crucible/LLVM/X86.hs | 15 +++++++++------ 8 files changed, 60 insertions(+), 6 deletions(-) create mode 100644 intTests/test1533/Makefile create mode 100644 intTests/test1533/test.bc create mode 100644 intTests/test1533/test.c create mode 100755 intTests/test1533/test.exe create mode 100644 intTests/test1533/test.saw create mode 100755 intTests/test1533/test.sh diff --git a/.gitignore b/.gitignore index cd17cabf33..b963d42e4f 100644 --- a/.gitignore +++ b/.gitignore @@ -24,6 +24,7 @@ intTests/test_intro_examples/*.cnf intTests/test_llvm_x86_0[1234]/test intTests/test_llvm_x86_0[1234]/test.o intTests/test_llvm_x86_0[1234]/test.bc +intTests/test1533/test.o intTests/test*/*.out intTests/test_crucible_jvm/Stat.class intTests/test_profiling/prof diff --git a/intTests/test1533/Makefile b/intTests/test1533/Makefile new file mode 100644 index 0000000000..1a3bb3f6a4 --- /dev/null +++ b/intTests/test1533/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/test1533/test.bc b/intTests/test1533/test.bc new file mode 100644 index 0000000000000000000000000000000000000000..db4443b74592866e2762a38eb08291419ed3637f GIT binary patch literal 3068 zcma(TZA@F&_1Mq&I$)lifEp;a`y86cO5@lVN+E{M;4FofuBNT3RPBU6FxUwg+s|O* zWYcr(_BpFJIc=m`Q#YA5KUz)N$Qo7MR&55ej3TchQ4}$TB3KB`)-+;kw`FRj?p!PoO{oC=kwm%YcE`TupXca0NhIR{f|ET>ygJlyYNKKpfDgonqCQTK?+bK z)dK>!2RlhLpXphY^~=?k&X*-A<=!eqqfYjcTTp*f+WT@%Z%S>c?@%;6R&D7`_XQX9 z&4+i18FkOg(&0tL`FhTNB+b1qvGk@I_8azRTTaeCe}-FFM7gIqfSm{}dlWmk;TL3e zd(NeBxSpEH*6$ifXKGTZ0d*HIThw2!ADrKOtPk=Asp9vFg3YF1D&5>t6!NnEM|*8M zP{v>bzz-2NE$qAV1vW_#b{H5=nGVIsbXE*EkhoJk>0_p2VmwH~1`_r$;XZPr59eZg zPK;$q+{f^O*zOa9c@lw=UbEuTElIdVy>?5lSx9J?W@>NhHJ20GRi|b?p~Y3;6=W(W zhC#t+#h_0_nX#A{36i*hOat8`;Z|leTQ1!y=r(6G7g5xVX0@PMpV7`IG+(i&r}{|L z$4nVSD$vKAFo>bN7|n|9?}`zQ#BBsvnAcvLsl7a>Eul0jp>|cTxhc_pB}5U8iR}(C z?jtcD6IYOsQw--wfvSo>t+21@HEaKiJtsywNVM#n@1O}War*0hvbLdJ6?B_=&ALQ~ zDt+)@%A}|BVz5D+M2BR>Xuj-!41|vfy-9ep7)I0ZU(4vaZQ#(Wn;V*?gbp3MKBI$^ z1;*-Qta(O2Az6_(ltW{{xQKBKWsW#&FG}v)7HY2+G}|uSW}^0LUb`x}Z^c=Qu3kda zsY8=DaRc19z0ShxI<$IzPJA`>W9 zZcec8f5`!W=9C);N}D@r8+={@!T~h^a)U*eQ#bA$$Yyrzd*q_bz7#g3_85}8;5;(D zg6pjcL9?)-8L5|ar|li7Vy0KX+#!4}q}&44$7=Rdfo)axVgxW#G$ZD!^0s7CiRoUn zcW0RHQY?c-b3#F;`@|qtPmr04i9t?mEbU}(W!Vk0DqvP!-)6TRY^!=fdksrdubp@4 zM$D(J?JQ>qk=f35JL@^ zN8)rYap3kgdwZSzdx5=WX55RIH8Yx0d0ca8mMV4cl3&f*I~VPpx$^jKvE!`0Bh6UP z7ESom&reyeFxJ_k@^^kQcvK7rlMyUIrx62cTGCo_+<(^)%*Pms4L(p_2Vj+I|SFUba6B(;R>wb1JOs}{c~$lh7VmdtGnH={9 zBD|^3p%fymP+f;Uk?Ef2P~dd6IVQEti` z=KT`^uEl&1KV#dZdomE2Y~c<^UEvY#nab*6uX}Qo>ko`fd`XFVe6H{i?~i*;lYH1T z=69RM#-_%NEoPJ3A23y98%H_gNZ9L{2oD=Q6XWBklyS@-@N&i{%$(7~8NK8Fh>`Mf z73(F|XP`|HCK6#*3 znK@HZD_dn^Mz+teyS@Ea?Yk}KTVFl@%R%YBW{ST0&O<*x^p0hB>pQb=|6=e(^1UZr zp0|(l{ml>XZ#3=A?s8MC@x<}tHGH$@G5&$3y*YRb>!04=HPv{BM)4>*8qC?du{>t& zoy)~jTbhe_WA@Op-_mO<`Fc;=btn6w1Is|QNsB@Cp@aRDs(k70Swl))=aSafu(+7+ ze6kA*EnB4T5*G(>3}KzDhaO8nX=j@O{%Qtz9Oru;S7Oa7gPem*+mD_)=@szQho)4UBN;jk@*gL2Jpdm`J*Nr=Xx-Tx&d$$Db}D6N zcMv#*T>R5#c*!yJ1*Q584&Nv>)TiZguqCpM$vuMwfVgtbfyC1c5+$h}j5CP~jkq9n zmt*prY`v_Ziv!TW*T<_C>E(D;FGv?~KJM}d(BJTrbH%qnywm^^K@K`t;bGXBkT{@8 zI)>&oqQ3p%4Aob`%+63-U2%a_N>P&WE5{^dG_=)^DJ z{t6Eb3#Cy=>52oD_q7ah`p%~C%l$ZoZ==q;5Tef06tCnmJroWOyGIWWd+{s@d#U#- TN7UWK4toBR+m*wEGGqHU@jce( literal 0 HcmV?d00001 diff --git a/intTests/test1533/test.c b/intTests/test1533/test.c new file mode 100644 index 0000000000..a5c8c447f0 --- /dev/null +++ b/intTests/test1533/test.c @@ -0,0 +1,14 @@ +#include + +struct s { + uint8_t x1; + uint8_t x2; +}; + +uint8_t get_x2(struct s *ss) { + return ss->x2; +} + +int main() { + return 0; +} diff --git a/intTests/test1533/test.exe b/intTests/test1533/test.exe new file mode 100755 index 0000000000000000000000000000000000000000..a7b66fc687993a11a5eccc55d0f4536a0eb0191b GIT binary patch literal 17448 zcmeHOYit}>6+W}$wVgOwuj4-4Bs5de7DwvNu9MVtnlzd9E4!8RAaz0!q|<$j?Irtg zcV>fKUaiuXTS^@X5N|3FQiO^W@goXSTM`l)RYEBJ0|<(!5D|gWl0u6Dv|Y}*bI(4; zYqdWRf0!f9oO{ka-??|ry)*aD%)Or*n-~u$3NQs=2au$N4WV++0R7vAD0M^71qNua z0oqa1hKC_?h`TA~GXXb)d8f2fkrVE?%s(D5P$JnN2J6MS&bfxf30EgWCMD-g=3zIR za6w8+8RYdb|EVm1Ios9B(+G^D8GG?IuLO`MyZIpaQzII8FS zB@X+3S>AGSIU%o)Ifo~j&!q>qMDy85K3A;FMdpSEBZFIXyQFUt*L@XMg! zv5V=o-_=%ZeM5cm6VJX>9@#i}1J#@AK>o;vi0oy!gr4%aJj#DR)P+WCS{QCboz_AR zcpVw4_8^!hrA^yOl^wH?$`xVPL~?k<+@x>PZ^hi{La8WoP4wi}RKXfj9XXzrwYe3P z_W@bf<(-B|QQI_L%asN_U$cbx%#VN{0Y3tM1pEm25%446N5GGOAA$dq2>iYK`hO*k z{-rbVMDR~hfW*V6oj~L3%^es{ln#blgaa^PxKg&IDf_v z?0gJa_3G~+{LMwOKRcy&Z+J++7f=l|@l^f;ckITxK&AIUV&USY`>WOJ3&Cxu zQ4XD5QXbjA`gpw#1W7D>=1Ss;u`Ast4TRM5sD6|`aQgh%+jJ@DkMQx2Ogwpq8UctO zOfLK)ejvH(?kZ^Ivq^xu_8xqm+>b75uOs*XeuhlBOjKgS0m~=5b zUPhhx7msPO8O7rE;ubJ~hlC-lF{RQ241p zGSv44bu6Sk*)|sH|9o&X6nmsS5gIz$u`6U0LqqXUEFS6~4r#-ozTr@KIMgZX`!j?; zjefXp223Bj88CkANQmKLUOP{0R6FSSAAaFPP|pTwl#=P?@h1xpA*%*4cg;8QSt;|H<$fuz6jlKA z{!2vbd5QX523JeYtV1R)NIaKI@3lm@7*`PE@sF>l&k1RdKcj`LNIQJp6!LMIFV+7u z#_P)8tH50&Be!e)2hx?IQ_;5SoAp>^;I@ho2R^$grpLBybk&f_r;5|s5vy$HN=0n| zv(R>nG}RzlvCFiWJDSfQDMSWh(R8jDbup1?EizTMGNp1hk|`AmsiIizZE2CcF)fnO z9Lsj}j20=msS^AUYuzSl-YMd_3O6LUbThKB>{3xo2UwtQ49dYWojVWXSq&VU`U+&+)2Q)&M)vS3@s7fJd$lr~sFV37`DJ(V8irciHC4TY~=7wS>gV3!Q&s9e)-^r@lSyS8ajY#iW=(bBCpsvS7UavmxLh{ z;SoIA;2x@^qWn9wnivI=Dk<72SIp!qSu2XG?aje0a_Rkav4V}}*Z^*WAOM{CSnZ({>N6FK`t(!N) zwB?v{o1jv(bJImDt7T?VWn6Sm)gCe(5bNYPMei{5)&cv>&B)p{mJdb(>clLPu&v|L@t>>?WerbPx zP54>buT;E%H5i8zG7kLBc^m4r7X7Uk^r6IgoRttGvvQ}b!7^yBT%B@%A;Ea?_-T`hD#V!vOc8p010Q1`>&H^2mRLM;QA_%;V=lvJZ5@KH1+m z4m+hEP3mb7C;BSt$&WV<-;?%@<2TuVAN5p!ul=XUKCtxpc2fEY%lg-1m?=B9Q^D1W z8OT~?YdU8;R@rn4W+q=MS~d}^`Y2cthJFj zl`H1VRJoj*H*q{G&%;zXRj|x#rBIkhNP}derPE|8M@G{e-yh#SW{&L{HBH1c*=4~T z{pgMv!%mv~5fGV$e3t$=xF|5ORB~WW-5LgUFjn*)yPL=ZomiuHb zYt8|kS{(CAB7nLzBinc;iwKrngxlCIg45_ORmf$qtP=XdlRlfrgzF5W0Xof|u`7X& z({>?Xh;`gJX`z*su1sV9m@08Pl}?wfBP=yqVT|Y=`fm`8Sa@sUv)?72FY*3g@5n{A zjr2hj=-rF)Jg?&Yt~WLsW162wtRBQfBcA79m!w0D4JG&DM^XO|d{^W0d7joun@Ewk z{`~yvbk()<9!$}coAErK>zDY1w8WPI5hup;d*ngXlPTkQ-Zv}pLlV!-8$X)l)4M0* zd470Y;;CFBu0Pu`Ka6?wF3U2{BTq=YMqngw{ar1<{g|MbGM?v~7bKqFpSgVR^*@AI zx+bnC$Z-J&13}&yk+=OG_uzS4(Ioy$o`6ZU>m1LE9z4%;PxZJaI1)CIw|sg-q#|nL ziDtO=n#;WQEHnQWnh~DkSKp`Y;c4#7qW#&IeEww%4d0xi*xhzav0GkeA{zv#j9{Hssmmn+}(4)7`_$QRe2 z=QI5h&*iYa3uSW9P zUb_t5mha|te>ajBf73Gfcity{K;pgedvudq>eG#dW17ovANDgy+jDsztxqV Map MS.AllocIndex Ptr -> Map MS.AllocIndex LLVMAllocSpec -> + Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} -> MS.SetupValue LLVM -> X86Sim Ptr -resolvePtrSetupValue env tyenv tptr = do +resolvePtrSetupValue env tyenv nameEnv tptr = do sym <- use x86Sym cc <- use x86CrucibleContext mem <- use x86Mem @@ -789,7 +790,7 @@ resolvePtrSetupValue env tyenv tptr = do let addr = fromIntegral $ Elf.steValue entry liftIO $ C.LLVM.doPtrAddOffset sym mem base =<< W4.bvLit sym knownNat (BV.mkBV knownNat addr) _ -> liftIO $ C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64) - =<< resolveSetupVal cc mem env tyenv Map.empty tptr + =<< resolveSetupVal cc mem env tyenv nameEnv tptr -- | Write each SetupValue passed to llvm_execute_func to the appropriate -- x86_64 register from the calling convention. @@ -852,6 +853,7 @@ assertPost globals env premem preregs = do postregs <- use x86Regs let tyenv = ms ^. MS.csPreState . MS.csAllocs + nameEnv = MS.csTypeNames ms prersp <- getReg Macaw.RSP preregs expectedIP <- liftIO $ C.LLVM.doLoad sym premem prersp (C.LLVM.bitvectorType 8) @@ -890,7 +892,7 @@ assertPost globals env premem preregs = do pointsToMatches <- forM (ms ^. MS.csPostState . MS.csPointsTos) - $ assertPointsTo env tyenv + $ assertPointsTo env tyenv nameEnv let setupConditionMatchesPre = fmap -- assume preconditions (LO.executeSetupCondition opts sc cc ms) @@ -931,15 +933,16 @@ assertPointsTo :: X86Constraints => Map MS.AllocIndex Ptr {- ^ Associates each AllocIndex with the corresponding allocation -} -> Map MS.AllocIndex LLVMAllocSpec {- ^ Associates each AllocIndex with its specification -} -> + Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} -> LLVMPointsTo LLVMArch {- ^ llvm_points_to statement from the precondition -} -> X86Sim (LLVMOverrideMatcher md ()) -assertPointsTo env tyenv pointsTo@(LLVMPointsTo loc cond tptr tptval) = do +assertPointsTo env tyenv nameEnv pointsTo@(LLVMPointsTo loc cond tptr tptval) = do opts <- use x86Options sc <- use x86SharedContext cc <- use x86CrucibleContext ms <- use x86MethodSpec - ptr <- resolvePtrSetupValue env tyenv tptr + ptr <- resolvePtrSetupValue env tyenv nameEnv tptr pure $ do err <- LO.matchPointsToValue opts sc cc ms MS.PostState loc cond ptr tptval case err of