From bfca3b6ec7455a8ba066f0e4a151a02f6b3690eb Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Fri, 19 Sep 2025 15:51:52 -0700 Subject: [PATCH 1/2] Add ability to allocate all globals This is necessary when global constants depend on the addresses of global variables. --- .../src/SAWCentral/Crucible/LLVM/Builtins.hs | 6 ++++- .../SAWCentral/Crucible/LLVM/CrucibleLLVM.hs | 4 +++- saw-central/src/SAWCentral/Value.hs | 1 + saw-script/src/SAWScript/Interpreter.hs | 23 +++++++++++++++++++ 4 files changed, 32 insertions(+), 2 deletions(-) diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs index c9b96aa049..88ad718608 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs @@ -1701,6 +1701,7 @@ setupLLVMCrucibleContext pathSat lm action = what4PushMuxOps <- gets rwWhat4PushMuxOps laxPointerOrdering <- gets rwLaxPointerOrdering laxLoadsAndStores <- gets rwLaxLoadsAndStores + allocAllGlobals <- gets rwAllocAllGlobals noSatisfyingWriteFreshConstant <- gets rwNoSatisfyingWriteFreshConstant pathSatSolver <- gets rwPathSatSolver what4Eval <- gets rwWhat4Eval @@ -1759,8 +1760,11 @@ setupLLVMCrucibleContext pathSat lm action = intrinsics halloc stdout bindings (Crucible.llvmExtensionImpl ?memOpts) Common.SAWCruciblePersonality + let memoryInitializer = if allocAllGlobals + then Crucible.initializeAllMemory + else Crucible.initializeMemoryConstGlobals mem <- Crucible.populateConstGlobals bak (view Crucible.globalInitMap mtrans) - =<< Crucible.initializeMemoryConstGlobals bak ctx llvm_mod + =<< memoryInitializer bak ctx llvm_mod let globals = Crucible.llvmGlobals (Crucible.llvmMemVar ctx) mem diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/CrucibleLLVM.hs b/saw-central/src/SAWCentral/Crucible/LLVM/CrucibleLLVM.hs index 360bbeb96e..7ee650fbac 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/CrucibleLLVM.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/CrucibleLLVM.hs @@ -67,6 +67,7 @@ module SAWCentral.Crucible.LLVM.CrucibleLLVM -- * Re-exports from "Lang.Crucible.LLVM.Globals" , GlobalInitializerMap , initializeMemoryConstGlobals + , initializeAllMemory , makeGlobalMap , populateConstGlobals -- * Re-exports from "Lang.Crucible.LLVM.Translation" @@ -164,7 +165,8 @@ import Lang.Crucible.LLVM.TypeContext import qualified Lang.Crucible.LLVM.TypeContext as TyCtx import Lang.Crucible.LLVM.Globals - (GlobalInitializerMap, initializeMemoryConstGlobals, makeGlobalMap, populateConstGlobals) + (GlobalInitializerMap, makeGlobalMap, populateConstGlobals, + initializeAllMemory, initializeMemoryConstGlobals) import Lang.Crucible.LLVM.Translation (llvmMemVar, transContext, llvmPtrWidth, llvmTypeCtx, diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs index 2beb60f9e6..bffd44177a 100644 --- a/saw-central/src/SAWCentral/Value.hs +++ b/saw-central/src/SAWCentral/Value.hs @@ -847,6 +847,7 @@ data TopLevelRW = , rwLaxLoadsAndStores :: Bool , rwLaxPointerOrdering :: Bool , rwDebugIntrinsics :: Bool + , rwAllocAllGlobals :: Bool -- ^ allocate all globals unconditionally -- FIXME: These might be better split into "simulator hash-consing" and "tactic hash-consing" , rwWhat4HashConsing :: Bool diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs index 1c45518d95..34513004d1 100644 --- a/saw-script/src/SAWScript/Interpreter.hs +++ b/saw-script/src/SAWScript/Interpreter.hs @@ -1079,6 +1079,7 @@ buildTopLevelEnv proxy opts scriptArgv = , rwLaxArith = False , rwLaxPointerOrdering = False , rwLaxLoadsAndStores = False + , rwAllocAllGlobals = False , rwDebugIntrinsics = True , rwWhat4HashConsing = False , rwWhat4HashConsingX86 = False @@ -1885,6 +1886,16 @@ disable_lax_loads_and_stores = do rw <- getTopLevelRW putTopLevelRW rw { rwLaxLoadsAndStores = False } +enable_alloc_all_globals :: TopLevel () +enable_alloc_all_globals = do + rw <- getTopLevelRW + putTopLevelRW rw { rwAllocAllGlobals = True } + +disable_alloc_all_globals :: TopLevel () +disable_alloc_all_globals = do + rw <- getTopLevelRW + putTopLevelRW rw { rwAllocAllGlobals = False } + set_solver_cache_path :: Text -> TopLevel () set_solver_cache_path pathtxt = do let path :: FilePath = Text.unpack pathtxt @@ -2693,6 +2704,18 @@ primitives = Map.fromList Current [ "Disable relaxed validity checking for memory loads and stores in Crucible." ] + , prim "enable_alloc_all_globals" "TopLevel ()" + (pureVal enable_alloc_all_globals) + Experimental + [ "Enable allocation of all globals automatically. This is necessary when" + , " constants depend on the addresses of globals." + ] + + , prim "disable_alloc_all_globals" "TopLevel ()" + (pureVal disable_alloc_all_globals) + Experimental + [ "Disable allocation of all globals automatically." ] + , prim "set_path_sat_solver" "String -> TopLevel ()" (pureVal set_path_sat_solver) Experimental From 083a00484e9c2fb419b906bb2ab4c6d800680435 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Fri, 26 Sep 2025 10:34:20 -0700 Subject: [PATCH 2/2] Add three global allocation options for LLVM When using no automatic allocations, constant globals must be manually allocated just the same as mutable globals. ``` let llvm_use_constant name = do { llvm_alloc_global name; llvm_points_to (llvm_global name) (llvm_global_initializer name); }; ``` --- .../src/SAWCentral/Crucible/LLVM/Builtins.hs | 30 ++++++++------ .../SAWCentral/Crucible/LLVM/CrucibleLLVM.hs | 4 +- saw-central/src/SAWCentral/Value.hs | 10 ++++- saw-script/src/SAWScript/Interpreter.hs | 41 +++++++++---------- 4 files changed, 49 insertions(+), 36 deletions(-) diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs index 88ad718608..7af6b67a3e 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs @@ -1042,12 +1042,7 @@ setupGlobalAllocs cc mspec mem0 = foldM go mem0 $ mspec ^. MS.csGlobalAllocs gimap = view Crucible.globalInitMap mtrans case Map.lookup symbol gimap of Just (g, Right (mt, _)) -> ccWithBackend cc $ \bak -> - do when (L.gaConstant $ L.globalAttrs g) . throwMethodSpec mspec $ mconcat - [ "Global variable \"" - , name - , "\" is not mutable" - ] - let sz = Crucible.memTypeSize (Crucible.llvmDataLayout ?lc) mt + do let sz = Crucible.memTypeSize (Crucible.llvmDataLayout ?lc) mt sz' <- W4.bvLit sym ?ptrWidth $ Crucible.bytesToBV ?ptrWidth sz alignment <- case L.globalAlign g of @@ -1061,7 +1056,10 @@ setupGlobalAllocs cc mspec mem0 = foldM go mem0 $ mspec ^. MS.csGlobalAllocs ] Just al -> return al _ -> pure $ Crucible.memTypeAlign (Crucible.llvmDataLayout ?lc) mt - (ptr, mem') <- Crucible.doMalloc bak Crucible.GlobalAlloc Crucible.Mutable name mem sz' alignment + let mutability + | L.gaConstant (L.globalAttrs g) = Crucible.Immutable + | otherwise = Crucible.Mutable + (ptr, mem') <- Crucible.doMalloc bak Crucible.GlobalAlloc mutability name mem sz' alignment pure $ Crucible.registerGlobal mem' [symbol] ptr _ -> throwMethodSpec mspec $ mconcat [ "Global variable \"" @@ -1701,7 +1699,7 @@ setupLLVMCrucibleContext pathSat lm action = what4PushMuxOps <- gets rwWhat4PushMuxOps laxPointerOrdering <- gets rwLaxPointerOrdering laxLoadsAndStores <- gets rwLaxLoadsAndStores - allocAllGlobals <- gets rwAllocAllGlobals + globalAllocMode <- gets rwLLVMGlobalAllocMode noSatisfyingWriteFreshConstant <- gets rwNoSatisfyingWriteFreshConstant pathSatSolver <- gets rwPathSatSolver what4Eval <- gets rwWhat4Eval @@ -1760,11 +1758,17 @@ setupLLVMCrucibleContext pathSat lm action = intrinsics halloc stdout bindings (Crucible.llvmExtensionImpl ?memOpts) Common.SAWCruciblePersonality - let memoryInitializer = if allocAllGlobals - then Crucible.initializeAllMemory - else Crucible.initializeMemoryConstGlobals - mem <- Crucible.populateConstGlobals bak (view Crucible.globalInitMap mtrans) - =<< memoryInitializer bak ctx llvm_mod + + mem <- + case globalAllocMode of + LLVMAllocConstantGlobals -> + Crucible.populateConstGlobals bak (view Crucible.globalInitMap mtrans) + =<< Crucible.initializeMemoryConstGlobals bak ctx llvm_mod + LLVMAllocAllGlobals -> + Crucible.populateConstGlobals bak (view Crucible.globalInitMap mtrans) + =<< Crucible.initializeAllMemory bak ctx llvm_mod + LLVMAllocNoGlobals -> + Crucible.initializeMemory (const False) bak ctx llvm_mod let globals = Crucible.llvmGlobals (Crucible.llvmMemVar ctx) mem diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/CrucibleLLVM.hs b/saw-central/src/SAWCentral/Crucible/LLVM/CrucibleLLVM.hs index 7ee650fbac..134ee3915a 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/CrucibleLLVM.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/CrucibleLLVM.hs @@ -68,6 +68,7 @@ module SAWCentral.Crucible.LLVM.CrucibleLLVM , GlobalInitializerMap , initializeMemoryConstGlobals , initializeAllMemory + , initializeMemory , makeGlobalMap , populateConstGlobals -- * Re-exports from "Lang.Crucible.LLVM.Translation" @@ -166,7 +167,8 @@ import qualified Lang.Crucible.LLVM.TypeContext as TyCtx import Lang.Crucible.LLVM.Globals (GlobalInitializerMap, makeGlobalMap, populateConstGlobals, - initializeAllMemory, initializeMemoryConstGlobals) + initializeAllMemory, initializeMemoryConstGlobals, + initializeMemory) import Lang.Crucible.LLVM.Translation (llvmMemVar, transContext, llvmPtrWidth, llvmTypeCtx, diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs index bffd44177a..17ba012e4f 100644 --- a/saw-central/src/SAWCentral/Value.hs +++ b/saw-central/src/SAWCentral/Value.hs @@ -70,6 +70,8 @@ module SAWCentral.Value ( TopLevelRW(..), -- used by ... a lot of places, let's not try to make a list just yet TopLevel(..), + -- Used by TopLevelRW + LLVMGlobalAllocMode(..), -- used by SAWCentral.Builtins, SAWScript.REPL.Monad, SAWScript.Interpreter, -- SAWServer.TopLevel runTopLevel, @@ -809,6 +811,12 @@ data JavaCodebase = -- ^ At least one Java-related command has been invoked successfully. -- We cache the resulting 'JSS.Codebase' for subsequent commands. +data LLVMGlobalAllocMode + = LLVMAllocConstantGlobals -- ^ constants are allocated, globals need llvm_alloc_global + | LLVMAllocAllGlobals -- ^ all globals are allocated + | LLVMAllocNoGlobals -- ^ No globals are allocated, use llvm_alloc_global and llvm_alloc_constant + deriving (Show) + data TopLevelRW = TopLevelRW { rwValueInfo :: Map SS.LName (SS.PrimitiveLifecycle, SS.Schema, Value) @@ -847,7 +855,7 @@ data TopLevelRW = , rwLaxLoadsAndStores :: Bool , rwLaxPointerOrdering :: Bool , rwDebugIntrinsics :: Bool - , rwAllocAllGlobals :: Bool -- ^ allocate all globals unconditionally + , rwLLVMGlobalAllocMode :: LLVMGlobalAllocMode -- FIXME: These might be better split into "simulator hash-consing" and "tactic hash-consing" , rwWhat4HashConsing :: Bool diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs index 34513004d1..8fa3186e61 100644 --- a/saw-script/src/SAWScript/Interpreter.hs +++ b/saw-script/src/SAWScript/Interpreter.hs @@ -1079,7 +1079,7 @@ buildTopLevelEnv proxy opts scriptArgv = , rwLaxArith = False , rwLaxPointerOrdering = False , rwLaxLoadsAndStores = False - , rwAllocAllGlobals = False + , rwLLVMGlobalAllocMode = LLVMAllocConstantGlobals , rwDebugIntrinsics = True , rwWhat4HashConsing = False , rwWhat4HashConsingX86 = False @@ -1886,15 +1886,10 @@ disable_lax_loads_and_stores = do rw <- getTopLevelRW putTopLevelRW rw { rwLaxLoadsAndStores = False } -enable_alloc_all_globals :: TopLevel () -enable_alloc_all_globals = do +llvm_set_global_alloc_mode :: LLVMGlobalAllocMode -> TopLevel () +llvm_set_global_alloc_mode mode = do rw <- getTopLevelRW - putTopLevelRW rw { rwAllocAllGlobals = True } - -disable_alloc_all_globals :: TopLevel () -disable_alloc_all_globals = do - rw <- getTopLevelRW - putTopLevelRW rw { rwAllocAllGlobals = False } + putTopLevelRW rw { rwLLVMGlobalAllocMode = mode } set_solver_cache_path :: Text -> TopLevel () set_solver_cache_path pathtxt = do @@ -2704,18 +2699,6 @@ primitives = Map.fromList Current [ "Disable relaxed validity checking for memory loads and stores in Crucible." ] - , prim "enable_alloc_all_globals" "TopLevel ()" - (pureVal enable_alloc_all_globals) - Experimental - [ "Enable allocation of all globals automatically. This is necessary when" - , " constants depend on the addresses of globals." - ] - - , prim "disable_alloc_all_globals" "TopLevel ()" - (pureVal disable_alloc_all_globals) - Experimental - [ "Disable allocation of all globals automatically." ] - , prim "set_path_sat_solver" "String -> TopLevel ()" (pureVal set_path_sat_solver) Experimental @@ -5364,6 +5347,22 @@ primitives = Map.fromList Current [ "Legacy alternative name for `llvm_null`." ] + , prim "llvm_alloc_all_globals" "TopLevel ()" + (pureVal (llvm_set_global_alloc_mode LLVMAllocAllGlobals)) + Experimental + [ "Enable allocation of all constant and mutable globals automatically." + ] + + , prim "llvm_alloc_constant_globals" "TopLevel ()" + (pureVal (llvm_set_global_alloc_mode LLVMAllocConstantGlobals)) + Experimental + [ "Enable allocation of constant globals automatically. (default)" ] + + , prim "llvm_alloc_no_globals" "TopLevel ()" + (pureVal (llvm_set_global_alloc_mode LLVMAllocNoGlobals)) + Experimental + [ "Disable allocation of all globals automatically." ] + , prim "llvm_global" "String -> SetupValue" (pureVal CIR.anySetupGlobal)