Add support for x86 64 bit integer stack arguments.

GaloisInc · Jan 14, 2024 · a68689e · a68689e
1 parent a400e9e
commit a68689e
Show file tree

Hide file tree

Showing 7 changed files with 104 additions and 34 deletions.
diff --git a/intTests/test_llvm_x86_08/test b/intTests/test_llvm_x86_08/test
diff --git a/intTests/test_llvm_x86_08/test.bc b/intTests/test_llvm_x86_08/test.bc
diff --git a/intTests/test_llvm_x86_08/test.c b/intTests/test_llvm_x86_08/test.c
@@ -0,0 +1,4 @@
+unsigned long test(unsigned long a, unsigned long b, unsigned long c, unsigned long d,unsigned long e, unsigned long f, unsigned long g, unsigned long h) {
+  return g - h;
+}
+
diff --git a/intTests/test_llvm_x86_08/test.o b/intTests/test_llvm_x86_08/test.o
diff --git a/intTests/test_llvm_x86_08/test.saw 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
@@ -0,0 +1,8 @@
+#!/bin/sh
+set -e
+
+clang -c -emit-llvm -g -frecord-command-line test.c
+clang -c -target x86_64 test.c
+ld.lld test.o -o test
+$SAW test.saw
+
diff --git 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]
 
 --------------------------------------------------------------------------------