Add ability to allocate all globals

This is necessary when global constants depend on the addresses of global variables.

Author: glguy

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
 

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,

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

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