Skip to content

Allocate global variables before populating constants #2623

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
+53 −10
Open

Allocate global variables before populating constants #2623

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
bfca3b6
Add ability to allocate all globals
glguy Sep 19, 2025
083a004
Add three global allocation options for LLVM
glguy Sep 26, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 17 additions & 9 deletions saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 \""
Expand Down Expand Up @@ -1701,6 +1699,7 @@ setupLLVMCrucibleContext pathSat lm action =
what4PushMuxOps <- gets rwWhat4PushMuxOps
laxPointerOrdering <- gets rwLaxPointerOrdering
laxLoadsAndStores <- gets rwLaxLoadsAndStores
globalAllocMode <- gets rwLLVMGlobalAllocMode
noSatisfyingWriteFreshConstant <- gets rwNoSatisfyingWriteFreshConstant
pathSatSolver <- gets rwPathSatSolver
what4Eval <- gets rwWhat4Eval
Expand Down Expand Up @@ -1759,8 +1758,17 @@ setupLLVMCrucibleContext pathSat lm action =
intrinsics halloc stdout
bindings (Crucible.llvmExtensionImpl ?memOpts)
Common.SAWCruciblePersonality
mem <- Crucible.populateConstGlobals bak (view Crucible.globalInitMap mtrans)
=<< Crucible.initializeMemoryConstGlobals 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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's a populateAllGlobals on the Crucible side and I would hazard a guess you probably want it here...

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was assuming that would set the mutable globals to their initial values, which is a stronger precondition than I want.

LLVMAllocNoGlobals ->
Crucible.initializeMemory (const False) bak ctx llvm_mod

let globals = Crucible.llvmGlobals (Crucible.llvmMemVar ctx) mem

Expand Down
6 changes: 5 additions & 1 deletion saw-central/src/SAWCentral/Crucible/LLVM/CrucibleLLVM.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,8 @@ module SAWCentral.Crucible.LLVM.CrucibleLLVM
-- * Re-exports from "Lang.Crucible.LLVM.Globals"
, GlobalInitializerMap
, initializeMemoryConstGlobals
, initializeAllMemory
, initializeMemory
, makeGlobalMap
, populateConstGlobals
-- * Re-exports from "Lang.Crucible.LLVM.Translation"
Expand Down Expand Up @@ -164,7 +166,9 @@ 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,
initializeMemory)

import Lang.Crucible.LLVM.Translation
(llvmMemVar, transContext, llvmPtrWidth, llvmTypeCtx,
Expand Down
9 changes: 9 additions & 0 deletions saw-central/src/SAWCentral/Value.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -847,6 +855,7 @@ data TopLevelRW =
, rwLaxLoadsAndStores :: Bool
, rwLaxPointerOrdering :: Bool
, rwDebugIntrinsics :: Bool
, rwLLVMGlobalAllocMode :: LLVMGlobalAllocMode

-- FIXME: These might be better split into "simulator hash-consing" and "tactic hash-consing"
, rwWhat4HashConsing :: Bool
Expand Down
22 changes: 22 additions & 0 deletions saw-script/src/SAWScript/Interpreter.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1079,6 +1079,7 @@ buildTopLevelEnv proxy opts scriptArgv =
, rwLaxArith = False
, rwLaxPointerOrdering = False
, rwLaxLoadsAndStores = False
, rwLLVMGlobalAllocMode = LLVMAllocConstantGlobals
, rwDebugIntrinsics = True
, rwWhat4HashConsing = False
, rwWhat4HashConsingX86 = False
Expand Down Expand Up @@ -1885,6 +1886,11 @@ disable_lax_loads_and_stores = do
rw <- getTopLevelRW
putTopLevelRW rw { rwLaxLoadsAndStores = False }

llvm_set_global_alloc_mode :: LLVMGlobalAllocMode -> TopLevel ()
llvm_set_global_alloc_mode mode = do
rw <- getTopLevelRW
putTopLevelRW rw { rwLLVMGlobalAllocMode = mode }

set_solver_cache_path :: Text -> TopLevel ()
set_solver_cache_path pathtxt = do
let path :: FilePath = Text.unpack pathtxt
Expand Down Expand Up @@ -5341,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)
Expand Down
Loading