Update crucible and macaw submodules, changes to x86 initial stack

src/SAWScript/Crucible/LLVM/X86.hs

@@ -24,6 +24,7 @@ Stability   : provisional
 
 module SAWScript.Crucible.LLVM.X86
   ( llvm_verify_x86
+  , defaultStackBaseAlign
   ) where
 
 import Control.Lens.TH (makeLenses)
@@ -78,11 +79,13 @@ import SAWScript.Crucible.LLVM.MethodSpecIR
 import SAWScript.Crucible.LLVM.ResolveSetupValue
 import qualified SAWScript.Crucible.LLVM.Override as LO
 
+import qualified What4.Config as W4
 import qualified What4.Expr as W4
 import qualified What4.FunctionName as W4
 import qualified What4.Interface as W4
 import qualified What4.LabeledPred as W4
 import qualified What4.ProgramLoc as W4
+import qualified What4.Expr.Builder as W4.B
 
 import qualified Lang.Crucible.Analysis.Postdom as C
 import qualified Lang.Crucible.Backend as C
@@ -98,6 +101,7 @@ import qualified Lang.Crucible.Simulator.RegMap as C
 import qualified Lang.Crucible.Simulator.SimError as C
 import qualified Lang.Crucible.Simulator.PathSatisfiability as C
 
+import qualified Lang.Crucible.LLVM.Bytes as C.LLVM
 import qualified Lang.Crucible.LLVM.DataLayout as C.LLVM
 import qualified Lang.Crucible.LLVM.Extension as C.LLVM
 import qualified Lang.Crucible.LLVM.Intrinsics as C.LLVM
@@ -156,6 +160,17 @@ runX86Sim st m = runStateT (unX86Sim m) st
 throwX86 :: MonadThrow m => String -> m a
 throwX86 = throw . X86Error
 
+defaultStackBaseAlign :: Integer
+defaultStackBaseAlign = 16
+
+integerToAlignment ::
+  (MonadIO m, MonadThrow m) =>
+  Integer ->
+  m C.LLVM.Alignment
+integerToAlignment i
+  | Just ba <- C.LLVM.toAlignment (C.LLVM.toBytes i) = pure ba
+  | otherwise = throwX86 $ mconcat ["Invalid alignment specified: ", show i]
+
 setReg ::
   (MonadIO m, MonadThrow m) =>
   Register ->
@@ -235,11 +250,13 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se
       opts <- getOptions
       basic_ss <- getBasicSS
       sym <- liftIO $ newSAWCoreBackend sc
+      rw <- getTopLevelRW
+      cacheTermsSetting <- liftIO $ W4.getOptionSetting W4.B.cacheTerms $ W4.getConfiguration sym
+      _ <- liftIO $ W4.setOpt cacheTermsSetting $ rwWhat4HashConsingX86 rw
       sawst <- liftIO $ sawCoreState sym
       halloc <- getHandleAlloc
       let mvar = C.LLVM.llvmMemVar . view C.LLVM.transContext $ modTrans llvmModule
       sfs <- liftIO $ Macaw.newSymFuns sym
-      rw <- getTopLevelRW
       let cenv = rwCryptol rw
       liftIO $ sawRegisterSymFunInterp sawst (Macaw.fnAesEnc sfs) $ cryptolUninterpreted cenv "aesenc"
       liftIO $ sawRegisterSymFunInterp sawst (Macaw.fnAesEncLast sfs) $ cryptolUninterpreted cenv "aesenclast"
@@ -282,7 +299,8 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se
       let ?lc = modTrans llvmModule ^. C.LLVM.transContext . C.LLVM.llvmTypeCtx
 
       emptyState <- liftIO $ initialState sym opts sc cc elf relf methodSpec globsyms maxAddr
-      (env, preState) <- liftIO . runX86Sim emptyState $ setupMemory globsyms
+      balign <- integerToAlignment $ rwStackBaseAlign rw
+      (env, preState) <- liftIO . runX86Sim emptyState $ setupMemory globsyms balign
 
       let
         funcLookup = Macaw.LookupFunctionHandle $ \st _mem regs -> do
@@ -304,7 +322,7 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se
                       pure
                         ( C.cfgHandle funcCFG
                         , st & C.stateContext . C.functionBindings
-                          %~ C.insertHandleMap (C.cfgHandle funcCFG) (C.UseCFG funcCFG $ C.postdomInfo funcCFG)
+                          %~ C.FnBindings . C.insertHandleMap (C.cfgHandle funcCFG) (C.UseCFG funcCFG $ C.postdomInfo funcCFG) . C.fnBindings
                         )
                     Nothing -> fail $ mconcat
                       [ "Unable to find CFG for function at address "
@@ -322,7 +340,7 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se
                 Macaw.macawExtensions (Macaw.x86_64MacawEvalFn sfs) mvar
                 (mkGlobalMap . Map.singleton 0 $ preState ^. x86GlobalBase)
                 funcLookup noExtraValidityPred
-              , C._functionBindings = C.insertHandleMap (C.cfgHandle cfg) (C.UseCFG cfg $ C.postdomInfo cfg) C.emptyHandleMap
+              , C._functionBindings = C.FnBindings $ C.insertHandleMap (C.cfgHandle cfg) (C.UseCFG cfg $ C.postdomInfo cfg) C.emptyHandleMap
               , C._cruciblePersonality = Macaw.MacawSimulatorState
               , C._profilingMetrics = Map.empty
               }
@@ -541,12 +559,13 @@ initialState sym opts sc cc elf relf ms globs maxAddr = do
 setupMemory ::
   X86Constraints =>
   [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} ->
+  C.LLVM.Alignment {- ^ Stack base alignment -} ->
   X86Sim (Map MS.AllocIndex Ptr)
-setupMemory globsyms = do
+setupMemory globsyms balign = do
   setupGlobals globsyms
 
-  -- Allocate a reasonable amount of stack (4 KiB + 1 qword for IP)
-  allocateStack 4096
+  -- Allocate a reasonable amount of stack (4 KiB + 0b10000 for least valid alignment + 1 qword for IP)
+  allocateStack (4096 + 16) balign
 
   ms <- use x86MethodSpec
 
@@ -597,25 +616,25 @@ setupGlobals globsyms = do
 allocateStack ::
   X86Constraints =>
   Integer {- ^ Stack size in bytes -} ->
+  C.LLVM.Alignment {- ^ Stack base alignment -} ->
   X86Sim ()
-allocateStack szInt = do
+allocateStack szInt balign = do
   sym <- use x86Sym
   mem <- use x86Mem
   regs <- use x86Regs
-  let align = C.LLVM.exponentToAlignment 4
   sz <- liftIO $ W4.bvLit sym knownNat $ BV.mkBV knownNat $ szInt + 8
-  (base, mem') <- liftIO $ C.LLVM.doMalloc sym C.LLVM.HeapAlloc C.LLVM.Mutable
-    "stack_alloc" mem sz align
+  (base, mem') <- liftIO $ C.LLVM.doMalloc sym C.LLVM.HeapAlloc C.LLVM.Mutable "stack_alloc" mem sz balign
   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 sym mem' base =<< W4.bvLit sym knownNat (BV.mkBV knownNat szInt)
+  writeAlign <- integerToAlignment defaultStackBaseAlign
   finalMem <- liftIO $ C.LLVM.doStore sym mem' ptr
     (C.LLVM.LLVMPointerRepr $ knownNat @64)
-    (C.LLVM.bitvectorType 8) align fresh
+    (C.LLVM.bitvectorType 8) writeAlign fresh
   x86Mem .= finalMem
   finalRegs <- setReg Macaw.RSP ptr regs
   x86Regs .= finalRegs

src/SAWScript/Interpreter.hs

@@ -471,7 +471,9 @@ buildTopLevelEnv proxy opts =
                    , rwProfilingFile = Nothing
                    , rwLaxArith = False
                    , rwWhat4HashConsing = False
+                   , rwWhat4HashConsingX86 = False
                    , rwPreservedRegs = []
+                   , rwStackBaseAlign = defaultStackBaseAlign
                    }
        return (bic, ro0, rw0)
 
@@ -546,6 +548,16 @@ disable_what4_hash_consing = do
   rw <- getTopLevelRW
   putTopLevelRW rw { rwWhat4HashConsing = False }
 
+enable_x86_what4_hash_consing :: TopLevel ()
+enable_x86_what4_hash_consing = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwWhat4HashConsingX86 = True }
+
+disable_x86_what4_hash_consing :: TopLevel ()
+disable_x86_what4_hash_consing = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwWhat4HashConsingX86 = False }
+
 add_x86_preserved_reg :: String -> TopLevel ()
 add_x86_preserved_reg r = do
   rw <- getTopLevelRW
@@ -556,6 +568,16 @@ default_x86_preserved_reg = do
   rw <- getTopLevelRW
   putTopLevelRW rw { rwPreservedRegs = [] }
 
+set_x86_stack_base_align :: Integer -> TopLevel ()
+set_x86_stack_base_align a = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwStackBaseAlign = a }
+
+default_x86_stack_base_align :: TopLevel ()
+default_x86_stack_base_align = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwStackBaseAlign = defaultStackBaseAlign }
+
 include_value :: FilePath -> TopLevel ()
 include_value file = do
   oldpath <- io $ getCurrentDirectory
@@ -2387,6 +2409,16 @@ primitives = Map.fromList
     Experimental
     [ "Legacy alternative name for `llvm_verify_x86`." ]
 
+  , prim "enable_x86_what4_hash_consing" "TopLevel ()"
+    (pureVal enable_x86_what4_hash_consing)
+    Experimental
+    [ "Enable hash consing for What4 expressions during x86 verification." ]
+
+  , prim "disable_x86_what4_hash_consing" "TopLevel ()"
+    (pureVal disable_x86_what4_hash_consing)
+    Current
+    [ "Disable hash consing for What4 expressions during x86 verification." ]
+
   , prim "add_x86_preserved_reg" "String -> TopLevel ()"
     (pureVal add_x86_preserved_reg)
     Current
@@ -2395,7 +2427,17 @@ primitives = Map.fromList
   , prim "default_x86_preserved_reg" "TopLevel ()"
     (pureVal default_x86_preserved_reg)
     Current
-    [ "Use the default set of callee-saved registers during x86 verification.." ]
+    [ "Use the default set of callee-saved registers during x86 verification." ]
+
+  , prim "set_x86_stack_base_align" "Int -> TopLevel ()"
+    (pureVal set_x86_stack_base_align)
+    Experimental
+    [ "Set the alignment of the stack allocation base to 2^n during x86 verification." ]
+
+  , prim "default_x86_stack_base_align" "TopLevel ()"
+    (pureVal default_x86_stack_base_align)
+    Experimental
+    [ "Use the default stack allocation base alignment during x86 verification." ]
 
   , prim "llvm_array_value"
     "[SetupValue] -> SetupValue"

src/SAWScript/Value.hs

@@ -401,8 +401,13 @@ data TopLevelRW =
   , rwCrucibleAssertThenAssume :: Bool
   , rwProfilingFile :: Maybe FilePath
   , rwLaxArith :: Bool
+
+  -- FIXME: These might be better split into "simulator hash-consing" and "tactic hash-consing"
   , rwWhat4HashConsing :: Bool
+  , rwWhat4HashConsingX86 :: Bool
+
   , rwPreservedRegs :: [String]
+  , rwStackBaseAlign :: Integer
   }
 
 newtype TopLevel a =

src/SAWScript/X86.hs

@@ -69,6 +69,7 @@ import Lang.Crucible.Simulator.EvalStmt(executeCrucible)
 import Lang.Crucible.Simulator.ExecutionTree
           (ExecResult(..), SimContext(..), FnState(..)
           , ExecState(InitialState)
+          , FunctionBindings(..)
           )
 import Lang.Crucible.Simulator.SimError(SimError(..), SimErrorReason)
 import Lang.Crucible.Backend
@@ -475,9 +476,8 @@ doSim opts elf sfs name (globs,overs) st checkPost =
                               , simHandleAllocator = allocator opts
                               , printHandle = stdout
                               , extensionImpl = macawExtensions (x86_64MacawEvalFn sfs) mvar globs (callHandler overs sym) noExtraValidityPred
-                              , _functionBindings =
-                                   insertHandleMap (cfgHandle cfg) (UseCFG cfg (postdomInfo cfg)) $
-                                   emptyHandleMap
+                              , _functionBindings = FnBindings $
+                                insertHandleMap (cfgHandle cfg) (UseCFG cfg (postdomInfo cfg)) emptyHandleMap
                               , _cruciblePersonality = MacawSimulatorState
                               , _profilingMetrics = Map.empty
                               }

src/SAWScript/X86Spec.hs

@@ -1082,7 +1082,7 @@ setupGlobals opts gs fs s
                             let halloc = simHandleAllocator (st ^. stateContext)
                             h <- mkHandle halloc fname
                             let addBinding = over (stateContext . functionBindings)
-                                               (insertHandleMap h (UseOverride o))
+                                               (FnBindings . insertHandleMap h (UseOverride o) . fnBindings)
                             return (h, addBinding st)
                       )