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);
};
```

Author: glguy

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
 

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,

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

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)