From 9b2a33a9a14ba9a34e0bc0014914beb1ba5de870 Mon Sep 17 00:00:00 2001 From: Andrei Date: Sun, 14 Jan 2024 07:38:32 +0000 Subject: [PATCH 1/3] Add support for x86 64 bit integer stack arguments. --- intTests/test_llvm_x86_08/test | Bin 0 -> 1120 bytes intTests/test_llvm_x86_08/test.bc | Bin 0 -> 3116 bytes intTests/test_llvm_x86_08/test.c | 8 +++ intTests/test_llvm_x86_08/test.o | Bin 0 -> 1088 bytes intTests/test_llvm_x86_08/test.saw | 21 ++++++ intTests/test_llvm_x86_08/test.sh | 9 +++ src/SAWScript/Crucible/LLVM/X86.hs | 105 +++++++++++++++++++---------- 7 files changed, 109 insertions(+), 34 deletions(-) create mode 100755 intTests/test_llvm_x86_08/test create mode 100644 intTests/test_llvm_x86_08/test.bc create mode 100644 intTests/test_llvm_x86_08/test.c create mode 100644 intTests/test_llvm_x86_08/test.o create mode 100644 intTests/test_llvm_x86_08/test.saw create mode 100755 intTests/test_llvm_x86_08/test.sh diff --git a/intTests/test_llvm_x86_08/test b/intTests/test_llvm_x86_08/test new file mode 100755 index 0000000000000000000000000000000000000000..ece6555093b7efbdaa18e2339f26ba3e6cba9716 GIT binary patch literal 1120 zcmbtS&npCR6n`_;kMe8DVZ-5@D@_!U#EQ|R*+OkO5Ni#)F{5^8g~*=N#KE87Pw*d5 zdvJAhbWx7n92D=(yvN#HLAcq9{Dk6C8D+!6H)PDO1XD89uf zf0JhYYjm+eJ6ZzmAg=YaG&Wu0-o40ECUGu>hp&x~9v z^Vj?z!n2auaB^!~g^cTf;X4OD7}-77bv!JJhpwO5K+F~WLR3WvzEkv#YzW|H@*chC zpF!uLlB*sbvUr)K8LNsGRt#Wtd{AKok-7_}e@BR@TxT4m78V7?Erj_Ybz=9dmvlUU3CLJwf^oBx9Sozloy>;D89 Cs9>Q0 literal 0 HcmV?d00001 diff --git a/intTests/test_llvm_x86_08/test.bc b/intTests/test_llvm_x86_08/test.bc new file mode 100644 index 0000000000000000000000000000000000000000..062d659c5aeabc616acb0db91589d81adb4a5413 GIT binary patch literal 3116 zcma)8e@q+K9e>8gXAZWrU@M^Y1miZM%_HJcnYov22I&p*I!z#L~A z8`@4bra7v5lhZ~jn=;9?(UflcgGOjVQ&icQcph^j%Cd?vgkT{lWt5>cn<6z@_kH$A z6{(Z`WU1DO_QKfJyRuXS8_uc_ zY6pFIx%&QBP(&Om(}`)h%%2cAkHCAx;jj?kh+!QugqGLT%M<$+C#ab;h2B*!q}59i z_1qdY6ICyzG;=Jqv8G<1*te}!=c1Znb8JDL(0m4Rb;e zLYpQaI*fUhc-0g0bHeZfhfRxZ5n3GqpA=G*h z8wsfO8el^CnMAzoiD$DC%WrwzXtgd@p~5`<0OETGbb~BH&8|`1m7vdXK9IxTk_#J(Bll zSm0=(Dql`+CCD{K;bRoHcgP(Z*`S zsT{NuuXu>3G4Y6}BLWA^u@i$jV(@+`z=k41mrNK?3H-P)G#)*+y+dxVlK)JRTa4I| z!)z&XhFWH+IW09CRnM`~PZE}HG2IfICNuKic?GUR z;JH}9Lxk-@KqUl{Lem>o)Q}Q}fp?7AN@P+GAT^+y>U?;@w_DsGmRY=UAuP;Aca6 zzmxZJ0fW~UI0r-h20Wpww|B6wD{MT`#TZ|31bu-Z?d)ZJJ@lZP_j~(&bX`L&Q(LF6 zs|yx->l)ibEZ?CeQvtA ziZwEU8R6tLGNNvTtArLP%JQP<`F*f4QGAOPjuplxl9Zr4$}`5Nei1J;msWC{ zi*ud%#hIITPo4ht-akzJ_;1(G6}lF3bITj2%03(|w6ZHpOEb&4#f9a$Q)Q`wFYm*- zq=mP=dw3n>J2BkBjRVIrkXcRhnUT9xc48mg9dH~06*mfbbg=QZo&3}W>8V)9NvinN zM&6r@M2R6?;q(X#zUe@uiE$ha)Oj0)jKjSCH<3)C@oC% zz(lbaWsjCn)8^y1(js)bLPV}44{ah*q^zXmd&-1oBx2n!as7;@Z%IV&KOq}CZf>oG zJFGm#CT7k^IMo$qzlf4PnQupedC&haXQYyn^3+&b6roj>k8Q)TKgfs24Dl9P_XoN6r>PcnwD2hpnR)pLz_$V|g#FuoKNO%nVP8ag*3}|fY zfQk#&7zr3}2xmMH{4bp$}_pmmPx_C@+C; u6`;YlA>76}i_h3vm!qfF<%ZLjcNcGw-Q*4W&ind9zOR$Gc^JkxH?wqAHGJMk z=F5(MoIG=D^-{%8rsr9TEr?yl#0p?s?10gX8QuC7`1nRP|{z?4nvfI}P{{QvjM0sgM4%nxppr2I@jvegFUf literal 0 HcmV?d00001 diff --git a/intTests/test_llvm_x86_08/test.saw b/intTests/test_llvm_x86_08/test.saw new file mode 100644 index 0000000000..23d20e826a --- /dev/null +++ b/intTests/test_llvm_x86_08/test.saw @@ -0,0 +1,21 @@ +enable_experimental; + +m <- llvm_load_module "test.bc"; + +let test_spec = do { + x <- llvm_fresh_var "x" (llvm_int 64); + llvm_execute_func + [ llvm_term {{ 0 : [64] }} + , llvm_term {{ 1 : [64] }} + , llvm_term {{ 2 : [64] }} + , llvm_term {{ 3 : [64] }} + , llvm_term {{ 4 : [64] }} + , llvm_term {{ 5 : [64] }} + , llvm_term x + , llvm_term {{ 1 : [64] }} + ]; + llvm_return (llvm_term {{ x - 1 }}); +}; + +llvm_verify_x86 m "./test" "test" [] true test_spec w4; + diff --git a/intTests/test_llvm_x86_08/test.sh b/intTests/test_llvm_x86_08/test.sh new file mode 100755 index 0000000000..22954402c3 --- /dev/null +++ b/intTests/test_llvm_x86_08/test.sh @@ -0,0 +1,9 @@ +#!/bin/sh +set -e + +clang -c -emit-llvm -g -frecord-command-line test.c +# clang -c -target x86_64 test.c +# ld.lld -o test test.o +clang -o test test.c +$SAW test.saw + diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 0e8f7715b2..029f5ebe06 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -975,6 +975,8 @@ setupMemory globsyms balign = do setArgs env tyenv nameEnv . fmap snd . Map.elems $ ms ^. MS.csArgBindings + pushFreshReturnAddress + pure env -- | Given an alist of symbol names and sizes (in bytes), allocate space and copy @@ -1008,8 +1010,7 @@ setupGlobals globsyms = do mem' <- liftIO $ foldlM writeGlobal mem globs x86Mem .= mem' --- | Allocate memory for the stack, and pushes a fresh pointer as the return --- address. +-- | Allocate memory for the stack. allocateStack :: X86Constraints => Integer {- ^ Stack size in bytes -} -> @@ -1021,16 +1022,31 @@ allocateStack szInt balign = do mem <- use x86Mem regs <- use x86Regs sz <- liftIO $ W4.bvLit sym knownNat $ BV.mkBV knownNat $ szInt + 8 - (base, mem') <- liftIO $ C.LLVM.doMalloc bak C.LLVM.HeapAlloc C.LLVM.Mutable "stack_alloc" mem sz balign + (base, finalMem) <- liftIO $ C.LLVM.doMalloc bak C.LLVM.HeapAlloc C.LLVM.Mutable "stack_alloc" mem sz balign + ptr <- liftIO $ C.LLVM.doPtrAddOffset bak finalMem base sz + x86Mem .= finalMem + finalRegs <- setReg Macaw.RSP ptr regs + x86Regs .= finalRegs + +-- | Push a fresh pointer as the return address. +pushFreshReturnAddress :: + X86Constraints => + X86Sim () +pushFreshReturnAddress = do + SomeOnlineBackend bak <- use x86Backend + sym <- use x86Sym + mem <- use x86Mem + regs <- use x86Regs sn <- case W4.userSymbol "stack" of Left err -> throwX86 $ "Invalid symbol for stack: " <> show err Right sn -> pure sn fresh <- liftIO $ C.LLVM.LLVMPointer <$> W4.natLit sym 0 <*> W4.freshConstant sym sn (W4.BaseBVRepr $ knownNat @64) - ptr <- liftIO $ C.LLVM.doPtrAddOffset bak mem' base =<< W4.bvLit sym knownNat (BV.mkBV knownNat szInt) - writeAlign <- integerToAlignment defaultStackBaseAlign - finalMem <- liftIO $ C.LLVM.doStore bak mem' ptr + rsp <- getReg Macaw.RSP regs + ptr <- liftIO $ C.LLVM.doPtrAddOffset bak mem rsp =<< W4.bvLit sym knownNat (BV.mkBV knownNat (-8)) + let writeAlign = C.LLVM.noAlignment + finalMem <- liftIO $ C.LLVM.doStore bak mem ptr (C.LLVM.LLVMPointerRepr $ knownNat @64) (C.LLVM.bitvectorType 8) writeAlign fresh x86Mem .= finalMem @@ -1152,36 +1168,57 @@ setArgs :: Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} -> [MS.SetupValue LLVM] {- ^ Arguments passed to llvm_execute_func -} -> X86Sim () -setArgs env tyenv nameEnv args - | length args > length argRegs = throwX86 "More arguments than would fit into general-purpose registers" - | otherwise = do - sym <- use x86Sym - cc <- use x86CrucibleContext - mem <- use x86Mem - let - setRegSetupValue rs (reg, sval) = - exceptToFail (typeOfSetupValue cc tyenv nameEnv sval) >>= \case - 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 - C.LLVM.IntType 64 -> do +setArgs env tyenv nameEnv args = do + SomeOnlineBackend bak <- use x86Backend + sym <- use x86Sym + cc <- use x86CrucibleContext + mem <- use x86Mem + let + setRegSetupValue rs (reg, sval) = + exceptToFail (typeOfSetupValue cc tyenv nameEnv sval) >>= \case + 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 + C.LLVM.IntType 64 -> do + val <- C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64) + =<< resolveSetupVal cc mem env tyenv nameEnv sval + setReg reg val rs + C.LLVM.IntType _ -> do + C.LLVM.LLVMValInt base off <- resolveSetupVal cc mem env tyenv nameEnv sval + case testLeq (incNat $ W4.bvWidth off) (knownNat @64) of + Nothing -> fail "Argument bitvector does not fit in a single general-purpose register" + Just LeqProof -> do + off' <- W4.bvZext sym (knownNat @64) off val <- C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64) - =<< resolveSetupVal cc mem env tyenv nameEnv sval + $ C.LLVM.LLVMValInt base off' setReg reg val rs - C.LLVM.IntType _ -> do - C.LLVM.LLVMValInt base off <- resolveSetupVal cc mem env tyenv nameEnv sval - case testLeq (incNat $ W4.bvWidth off) (knownNat @64) of - Nothing -> fail "Argument bitvector does not fit in a single general-purpose register" - Just LeqProof -> do - off' <- W4.bvZext sym (knownNat @64) off - val <- C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64) - $ C.LLVM.LLVMValInt base off' - setReg reg val rs - _ -> fail "Argument does not fit into a single general-purpose register" - regs <- use x86Regs - newRegs <- liftIO . foldlM setRegSetupValue regs $ zip argRegs args - x86Regs .= newRegs + _ -> fail "Argument does not fit into a single general-purpose register" + regs <- use x86Regs + newRegs <- liftIO . foldlM setRegSetupValue regs $ zip argRegs args + x86Regs .= newRegs + + let stackArgs = reverse $ Prelude.drop (length argRegs) args + forM_ stackArgs $ \sval -> do + liftIO $ exceptToFail (typeOfSetupValue cc tyenv nameEnv sval) >>= \case + C.LLVM.PtrType _ -> pure () + C.LLVM.IntType 64 -> pure () + _ -> fail "Stack argument is not a 64 bit integer." + + regs' <- use x86Regs + rsp <- getReg Macaw.RSP regs' + rsp' <- liftIO $ C.LLVM.doPtrAddOffset bak mem rsp =<< W4.bvLit sym knownNat (BV.mkBV knownNat (-8)) + newRegs' <- setReg Macaw.RSP rsp' regs' + x86Regs .= newRegs' + + val <- liftIO $ C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64) + =<< resolveSetupVal cc mem env tyenv nameEnv sval + + mem' <- use x86Mem + mem'' <- liftIO $ + C.LLVM.doStore bak mem' rsp' (C.LLVM.LLVMPointerRepr $ knownNat @64) (C.LLVM.bitvectorType 8) C.LLVM.noAlignment val + x86Mem .= mem'' + where argRegs = [Macaw.RDI, Macaw.RSI, Macaw.RDX, Macaw.RCX, Macaw.R8, Macaw.R9] -------------------------------------------------------------------------------- From 0d096334669651e940155d4d3a4c0cc3d6aaf18f Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 16 Jan 2024 01:26:51 +0000 Subject: [PATCH 2/3] Address comments. --- intTests/test_llvm_x86_08/Makefile | 15 +++++++++++++++ intTests/test_llvm_x86_08/test.o | Bin 1088 -> 0 bytes src/SAWScript/Crucible/LLVM/X86.hs | 30 ++++++++++++++++++++++++----- 3 files changed, 40 insertions(+), 5 deletions(-) create mode 100644 intTests/test_llvm_x86_08/Makefile delete mode 100644 intTests/test_llvm_x86_08/test.o diff --git a/intTests/test_llvm_x86_08/Makefile b/intTests/test_llvm_x86_08/Makefile new file mode 100644 index 0000000000..581cb12764 --- /dev/null +++ b/intTests/test_llvm_x86_08/Makefile @@ -0,0 +1,15 @@ +CC = clang +CFLAGS = -g -frecord-command-line -O0 + +all: test.bc test + +test.bc: test.c + $(CC) $(CFLAGS) -c -emit-llvm $< -o $@ + +test: test.c + $(CC) $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc test + diff --git a/intTests/test_llvm_x86_08/test.o b/intTests/test_llvm_x86_08/test.o deleted file mode 100644 index 2300d13e2ff8d1d8c14c38251393d98721924dad..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1088 zcmbtSJ4*vW5S~kXLewA%!3U&PT#`bx@Npuiha?t4#75;zE*i{TLb8!4NUVgzCO^O; zKSi*xwY0PmEVZ)`bY|VvV@c=0>^JkxH?wqAHGJMk z=F5(MoIG=D^-{%8rsr9TEr?yl#0p?s?10gX8QuC7`1nRP|{z?4nvfI}P{{QvjM0sgM4%nxppr2I@jvegFUf diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 029f5ebe06..d0ced45957 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -78,6 +78,7 @@ import Verifier.SAW.SCTypeCheck (scTypeCheck) import Verifier.SAW.Simulator.What4.ReturnTrip +import SAWScript.Panic (panic) import SAWScript.Proof import SAWScript.Prover.SolverStats import SAWScript.TopLevel @@ -960,11 +961,14 @@ setupMemory :: setupMemory globsyms balign = do setupGlobals globsyms - -- Allocate a reasonable amount of stack (4 KiB + 0b10000 for least valid alignment + 1 qword for IP) - allocateStack (4096 + 16) balign - ms <- use x86MethodSpec + -- Allocate a reasonable amount of stack (4 KiB + 1 qword for the previous + -- %rbp value + 1 qword for the return address + 1 qword for each stack + -- argument) + let argsStackSize = fromIntegral $ 8 * (length $ Prelude.drop (length argRegs) $ Map.elems $ ms ^. MS.csArgBindings) + allocateStack (4096 + 16 + argsStackSize) balign + let tyenv = ms ^. MS.csPreState . MS.csAllocs nameEnv = MS.csTypeNames ms @@ -1021,7 +1025,7 @@ allocateStack szInt balign = do sym <- use x86Sym mem <- use x86Mem regs <- use x86Regs - sz <- liftIO $ W4.bvLit sym knownNat $ BV.mkBV knownNat $ szInt + 8 + sz <- liftIO $ W4.bvLit sym knownNat $ BV.mkBV knownNat $ szInt (base, finalMem) <- liftIO $ C.LLVM.doMalloc bak C.LLVM.HeapAlloc C.LLVM.Mutable "stack_alloc" mem sz balign ptr <- liftIO $ C.LLVM.doPtrAddOffset bak finalMem base sz x86Mem .= finalMem @@ -1044,6 +1048,18 @@ pushFreshReturnAddress = do <$> W4.natLit sym 0 <*> W4.freshConstant sym sn (W4.BaseBVRepr $ knownNat @64) rsp <- getReg Macaw.RSP regs + + -- x86-64 System V ABI specifies that: "In other words, the stack needs to be + -- 16 (32 or 64) byte aligned immediately before the call instruction is + -- executed. Once control has been transferred to the function entry point, + -- i.e. immediately after the return address has been pushed, %rsp points to + -- the return address, and the value of (%rsp + 8) is a multiple of 16 (32 or + -- 64)." + stackAlign <- integerToAlignment defaultStackBaseAlign + is_aligned <- liftIO $ C.LLVM.isAligned sym (knownNat @64) rsp stackAlign + when (W4.asConstantPred is_aligned /= Just True) $ + panic "SAWScript.Crucible.LLVM.X86.pushFreshReturnAddress" ["%rsp is not 16 byte aligned before the call instruction is executed."] + ptr <- liftIO $ C.LLVM.doPtrAddOffset bak mem rsp =<< W4.bvLit sym knownNat (BV.mkBV knownNat (-8)) let writeAlign = C.LLVM.noAlignment finalMem <- liftIO $ C.LLVM.doStore bak mem ptr @@ -1198,6 +1214,9 @@ setArgs env tyenv nameEnv args = do newRegs <- liftIO . foldlM setRegSetupValue regs $ zip argRegs args x86Regs .= newRegs + -- x86-64 System V ABI specifies that: "Once registers are assigned, the + -- arguments passed in memory are pushed on the stack in reversed + -- (right-to-left21) order." let stackArgs = reverse $ Prelude.drop (length argRegs) args forM_ stackArgs $ \sval -> do liftIO $ exceptToFail (typeOfSetupValue cc tyenv nameEnv sval) >>= \case @@ -1219,7 +1238,8 @@ setArgs env tyenv nameEnv args = do C.LLVM.doStore bak mem' rsp' (C.LLVM.LLVMPointerRepr $ knownNat @64) (C.LLVM.bitvectorType 8) C.LLVM.noAlignment val x86Mem .= mem'' - where argRegs = [Macaw.RDI, Macaw.RSI, Macaw.RDX, Macaw.RCX, Macaw.R8, Macaw.R9] +argRegs :: [Macaw.X86Reg (Macaw.BVType 64)] +argRegs = [Macaw.RDI, Macaw.RSI, Macaw.RDX, Macaw.RCX, Macaw.R8, Macaw.R9] -------------------------------------------------------------------------------- -- ** Postcondition From ab915d47804faf02c7975407309e11315d777046 Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 16 Jan 2024 01:29:25 +0000 Subject: [PATCH 3/3] Address comments. --- intTests/test_llvm_x86_08/test.bc | Bin 3116 -> 3252 bytes intTests/test_llvm_x86_08/test.saw | 2 ++ 2 files changed, 2 insertions(+) diff --git a/intTests/test_llvm_x86_08/test.bc b/intTests/test_llvm_x86_08/test.bc index 062d659c5aeabc616acb0db91589d81adb4a5413..e4cf358ab70354542708fbbd18618d9487a8ac01 100644 GIT binary patch delta 1921 zcmZXUeN0nV6u{4Wee@M*X$x#VwbX~8D{kP!N`Y+4T8fH>&FWm@GM2TJ@-eZNQok^+ zuYCB(g6?Vk0~43EjwR@rVbkp2wS^IeppFyNMjm;rujHY+$O8j&?a8OP&USEHKAY{MLt z1ue4FVq(Q^wnZg1?UpPed-xFBVv?F7(m`3W=%f~bZ8j0y;R^Psi3KgR8WT3-)u>@E zsu`k;cc~J|@00wp6yR7fBKc$q?OW;<&FEi5LcYJ7b!w)9QNwgRYr?6SjvD7eS?I(_ zRFeo9r=wZpF2n7R=4QAR+~>V;n;5w$hn_ zl79Q^vb}WFIvBwiWX;%&({V#>u3Jc(jit>CT7=xfe>ltod=xHB%FzuAUV6wV#&1?^ zJ7pNlhj2}j?N!ePmrzvf@e~%-x?Lqjr5kEX-5aXi7NNM%;x4Lny;Hs48`#gg8(rQy z{(#5d+_2Bf7Zw!=1;ybjNqOmxt#-cBbHLN+*t%(P5#FWDNiAAm-QZon@K#t>t_bFD z7x;WPpYPe*5Xf(AJg}D!c$xzRxU+9@RqY1IQ4I;LPF;>_b78BK!zWa{{awng$9p^t zFy2ORP)wOHDs1d94?N(mtL=dbvs&{IH-0b=TsK`)+b@-ynL#yWR`5BY(QJ*kgKEoYFqxwX+WGBQXt6AUx0J20z0^24i~- z>lKPoR&N=WcdVRT|L@-+1vIPtaG-3 z6?A7HrT~~|h8j>tzz{oDuDN0T?`P4|{mNL$riwNpLKmq3b}!?CKV@cX2E~*cRsiSO z)je^}5n6%1biLiakyos9C}LQj7iR!ft1Wb#9QFT$lj1Q> zTC;MKz%~F3DBEXs&rsc@+iCCO^hR)r)w9UT)GV<&(BO&u9Ltfqz+&P{EN+1{M_5a! zTZ<@l>JsX2Lh(I^a%u@GsBDicvAXZ0mG<^?td~wMT#-p$V*N%ij^|in2C{OQGleE* zjRwSa-mL7H>7n4PZm`RiE#TqGQ7$uqZs~NGAvEUAdkkn$1yKN8Jisc{m~XG>P?O@R z$pQFP0PMU^lQLzH9>n!tSA(~~8(2)d3w#@G1t(3coYyFs;zY^;E9t_Ca#d_0hrz5r z*3^~gr}QdCf1=CgQoE2}_{<3!)L}mL#XX-hCTkVa0X&#mFQZOZoOTjF&|e@VB}yd< z+1rgm2GQg^f)YAGcVPgakprYYsCz$5f24zwD6#?|Q}am* zE~%E2svNIMuT%4*s$4>yc2N0s)q{B1BaLctRDBoYrMyoVa)+fOh{Y43PGYDo>A0PbWKl{)*nsD+P?NTjB6Vrl}d3Jt|QFFFICcB35li- z(*W;8@0aKlS>sJfNFAxbo;mB`^j`1a+2|j5ZJ1*MoWZFh1>=}c zt|JN4n6Da*P)D`BiM?Kisvj*u3V;SMc4IOLWFTW~xn*8}-9O4Bu2!>r*>uO)xoBCS z>wc0)E_a#bOWHfemMKe{F{7{?s+@`SX0yNNdKYgk^`;6PrJqd|hq=|oLbf&Co5{{E zJ?uDkb>|Or@Ba4fiK1_LF};%SDE)4{I7+SNa`P*T+2xgVM`=RL1+JhS(M0bP6Brit zlKaEAk*!K*Yem-uP9f1AU7YSYEPoCC!Z<~riM87lGW3b%HU4QkI2DjKXTl!uc8U9}=H|%2q26tcIW|a3FItW2l z+$qLIBb1}x>0(X~xWBmkX{9t)`^XLoXm5aPVDHAJ(0PmOh@m>N0dV>77*L5z__d6+ zJO?vUv79&V!Je91N&K#OGQrzfh?N(@NH#uul?Dc3>bR`M8hLv*0`PN5>SjA1vCK{! zR)D=%n;5M<(Wa7v(NM8wFZ(=RPJ;3x=}X}EyNQxwpc@5BrI4zVP&aK&_mUX=T8Wjf z#%c?I@ud>UtBPs&7~feXbA3$H_hi_WdNMrOWV0Fo%oPd8^n91hr@U;e!YKSerX2*^ zju)60aG9hcF`2}8T3P+lBXoavtt0gcFJ5J%vsM%l0gDVxIt6Kmnc~thelmOomg&8kNBIj{0S}ui@0;^TL0pgSQmTXPDyv25&1`yBA zp>lLPnqsg6nO(J0uiP&n9)F3e1F6$?N|Gd@*X5 diff --git a/intTests/test_llvm_x86_08/test.saw b/intTests/test_llvm_x86_08/test.saw index 23d20e826a..3365a2b57b 100644 --- a/intTests/test_llvm_x86_08/test.saw +++ b/intTests/test_llvm_x86_08/test.saw @@ -2,6 +2,8 @@ enable_experimental; m <- llvm_load_module "test.bc"; +// Test a function with more than 6 arguments to ensure that the remaining +// arguments are spilled to the stack on x86-64. let test_spec = do { x <- llvm_fresh_var "x" (llvm_int 64); llvm_execute_func