From b39ef9bfdec53eb78fa078e2f5e049c95ebb11c2 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 11 Sep 2024 14:55:04 -0400
Subject: [PATCH] x86-symbolic: Use SysV-compatible stack setup in test suite

---
 symbolic/src/Data/Macaw/Symbolic/Testing.hs | 10 ++++--
 x86_symbolic/macaw-x86-symbolic.cabal       |  1 +
 x86_symbolic/tests/Main.hs                  | 35 +++++++++++++++++++--
 3 files changed, 42 insertions(+), 4 deletions(-)

diff --git a/symbolic/src/Data/Macaw/Symbolic/Testing.hs b/symbolic/src/Data/Macaw/Symbolic/Testing.hs
index d3e5359c..1d404cfe 100644
--- a/symbolic/src/Data/Macaw/Symbolic/Testing.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/Testing.hs
@@ -29,6 +29,12 @@ module Data.Macaw.Symbolic.Testing (
   MemModelPreset(..),
   describeMemModelPreset,
   toAddrSymMap,
+  freshRegs,
+  InitialMem(..),
+  initialMem,
+  lazyInitialMem,
+  simDiscoveredFunction,
+  summarizeExecution,
   -- * Execution features
   SomeBackend(..),
   defaultExecFeatures,
@@ -583,8 +589,8 @@ lazyInitialMem binfo bak archInfo archVals = do
 
 data InitialMem p sym arch
   = InitialMem
-    { _initMemMem :: CLM.MemImpl sym
-    , _initMemMmConf :: MS.MemModelConfig p sym arch CLM.Mem
+    { initMemMem :: CLM.MemImpl sym
+    , initMemMmConf :: MS.MemModelConfig p sym arch CLM.Mem
     }
 
 -- | Set up the symbolic execution engine with initial states and execute
diff --git a/x86_symbolic/macaw-x86-symbolic.cabal b/x86_symbolic/macaw-x86-symbolic.cabal
index 1f1930cc..89397ce6 100644
--- a/x86_symbolic/macaw-x86-symbolic.cabal
+++ b/x86_symbolic/macaw-x86-symbolic.cabal
@@ -46,6 +46,7 @@ test-suite macaw-x86-symbolic-tests
   hs-source-dirs: tests
   build-depends:
     base >= 4,
+    bv-sized,
     bytestring,
     containers,
     crucible,
diff --git a/x86_symbolic/tests/Main.hs b/x86_symbolic/tests/Main.hs
index 8f40ef5f..56b003a7 100644
--- a/x86_symbolic/tests/Main.hs
+++ b/x86_symbolic/tests/Main.hs
@@ -8,6 +8,7 @@
 module Main (main) where
 
 import           Control.Lens ( (^.) )
+import qualified Data.BitVector.Sized as BVS
 import qualified Data.ByteString as BS
 import qualified Data.ByteString.Char8 as BS8
 import qualified Data.ElfEdit as Elf
@@ -18,6 +19,7 @@ import qualified Data.Parameterized.Classes as PC
 import qualified Data.Parameterized.Nonce as PN
 import           Data.Parameterized.Some ( Some(..) )
 import           Data.Proxy ( Proxy(..) )
+import qualified Data.Sequence as Seq
 import qualified Prettyprinter as PP
 import           System.FilePath ( (</>), (<.>) )
 import qualified System.FilePath.Glob as SFG
@@ -34,6 +36,7 @@ import qualified Data.Macaw.Symbolic.Testing as MST
 import qualified Data.Macaw.X86 as MX
 import           Data.Macaw.X86.Symbolic ()
 import qualified Data.Macaw.X86.Symbolic as MXS
+import qualified Data.Macaw.X86.Symbolic.ABI.SysV as SysV
 import qualified What4.Config as WC
 import qualified What4.Interface as WI
 import qualified What4.ProblemFeatures as WPF
@@ -41,7 +44,9 @@ import qualified What4.Solver as WS
 
 import qualified Lang.Crucible.Backend as CB
 import qualified Lang.Crucible.Backend.Online as CBO
+import qualified Lang.Crucible.FunctionHandle as CFH
 import qualified Lang.Crucible.Simulator as CS
+import qualified Lang.Crucible.Types as CT
 import qualified Lang.Crucible.LLVM.MemModel as LLVM
 
 import qualified What4.FloatMode as W4
@@ -171,8 +176,34 @@ mkSymExTest expected mmPreset exePath = TT.askOption $ \saveSMT@(SaveSMT _) -> T
               let extract = x86ResultExtractor archVals
               logger <- makeGoalLogger saveSMT solver name exePath
               let ?memOpts = LLVM.defaultMemOptions
-              simRes <- MST.simulateAndVerify solver logger bak execFeatures MX.x86_64_linux_info archVals binariesInfo mmPreset extract dfi
-              TTH.assertEqual "AssertionResult" expected simRes
+
+              MS.withArchConstraints archVals $ do
+                halloc <- CFH.newHandleAllocator
+                let ?recordLLVMAnnotation = \_ _ _ -> return ()
+
+                MST.InitialMem initMem mmConf <-
+                  case mmPreset of
+                    MST.DefaultMemModel -> MST.initialMem binariesInfo bak MX.x86_64_linux_info archVals
+                    MST.LazyMemModel -> MST.lazyInitialMem binariesInfo bak MX.x86_64_linux_info archVals
+
+                let symArchFns = MS.archFunctions archVals
+                initRegs <- MST.freshRegs symArchFns sym
+                let kib = 1024
+                let mib = 1024 * kib
+                stackSize <- WI.bvLit sym CT.knownNat (BVS.mkBV CT.knownNat mib)
+                (regs, mem) <- SysV.allocStack bak initMem initRegs stackSize
+                retAddr <- SysV.freshRetAddr sym
+                let spilled = SysV.SpilledArgs Seq.Empty
+                (regs', mem') <- SysV.pushStackFrame bak mem regs spilled retAddr
+                let crucRegTypes = MS.crucArchRegTypes symArchFns
+                let regsEntry = CS.RegEntry (CT.StructRepr crucRegTypes) regs'
+
+                let iMem = MST.InitialMem mem' mmConf
+                (memVar, execResult) <-
+                  MST.simDiscoveredFunction bak execFeatures archVals halloc iMem regsEntry binariesInfo dfi
+
+                simRes <- MST.summarizeExecution solver logger bak memVar extract execResult
+                TTH.assertEqual "AssertionResult" expected simRes
 
 writeMacawIR :: (MC.ArchConstraints arch) => SaveMacaw -> String -> M.DiscoveryFunInfo arch ids -> IO ()
 writeMacawIR (SaveMacaw sm) name dfi