llvm: don't initialize globals by default

Instead, add crucible_global_initializer.

The current behavior of globals is unsound (ref: GaloisInc#203). Instead,
we provide an option for the user to initialize globals as necessary.

It would be best to have more informative error messages when the
symbolic simulator accesses invalid memory because a global hasn't
been initialized.

intTests/runtests.sh

@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ################################################################
 # Setup environment.

saw-script.cabal

@@ -33,7 +33,7 @@ library
     , cryptol-verifier
     , crucible >= 0.4 && < 0.5
     , crucible-jvm
-    , crucible-llvm
+    , crucible-llvm >= 0.2
     , crucible-saw
     , deepseq
     , either

src/SAWScript/CrucibleBuiltins.hs

@@ -99,7 +99,7 @@ import           What4.Utils.MonadST
 import qualified Lang.Crucible.Backend as Crucible
 import qualified Lang.Crucible.Backend.SAWCore as Crucible
 import qualified Lang.Crucible.CFG.Core as Crucible
-  (AnyCFG(..), SomeCFG(..), CFG, TypeRepr(..), cfgHandle,
+  (AnyCFG(..), CFG, TypeRepr(..), cfgHandle,
    asBaseType, AsBaseType(..), freshGlobalVar)
 import qualified Lang.Crucible.CFG.Extension as Crucible
   (IsSyntaxExtension)
@@ -690,11 +690,6 @@ setupCrucibleContext bic opts (LLVMModule _ llvm_mod (Some mtrans)) action = do
              -- register the callable override functions
              _llvmctx' <- execStateT Crucible.register_llvm_overrides ctx
 
-             -- initialize LLVM global variables
-             _ <- case Crucible.initMemoryCFG mtrans of
-                     Crucible.SomeCFG initCFG ->
-                       Crucible.callCFG initCFG Crucible.emptyRegMap
-
              -- register all the functions defined in the LLVM module
              mapM_ Crucible.registerModuleFn $ Map.toList $ Crucible.cfgMap mtrans
 

src/SAWScript/CrucibleLLVM.hs

@@ -69,7 +69,6 @@ module SAWScript.CrucibleLLVM
   , transContext
   , llvmPtrWidth
   , initializeMemory
-  , initMemoryCFG
   , LLVMContext
   , translateModule
     -- * Re-exports from "Lang.Crucible.LLVM.MemModel"
@@ -151,7 +150,7 @@ import qualified Lang.Crucible.LLVM.LLVMContext as TyCtx
 
 import Lang.Crucible.LLVM.Translation
   (llvmMemVar, toStorableType, symbolMap, LLVMHandleInfo(LLVMHandleInfo),
-   cfgMap, transContext, llvmPtrWidth, initializeMemory, initMemoryCFG,
+   cfgMap, transContext, llvmPtrWidth, initializeMemory,
    ModuleTranslation, LLVMContext, translateModule)
 
 import Lang.Crucible.LLVM.MemModel

src/SAWScript/CrucibleMethodSpecIR.hs

@@ -70,15 +70,21 @@ newtype AllocIndex = AllocIndex Int
 nextAllocIndex :: AllocIndex -> AllocIndex
 nextAllocIndex (AllocIndex n) = AllocIndex (n + 1)
 
+-- | From the manual: "The SetupValue type corresponds to values that can occur
+-- during symbolic execution, which includes both Term values, pointers, and
+-- composite types consisting of either of these (both structures and arrays)."
 data SetupValue where
-  SetupVar    :: AllocIndex -> SetupValue
-  SetupTerm   :: TypedTerm -> SetupValue
-  SetupStruct :: [SetupValue] -> SetupValue
-  SetupArray  :: [SetupValue] -> SetupValue
-  SetupElem   :: SetupValue -> Int -> SetupValue
-  SetupField  :: SetupValue -> String -> SetupValue
-  SetupNull   :: SetupValue
-  SetupGlobal :: String -> SetupValue
+  SetupVar               :: AllocIndex -> SetupValue
+  SetupTerm              :: TypedTerm -> SetupValue
+  SetupStruct            :: [SetupValue] -> SetupValue
+  SetupArray             :: [SetupValue] -> SetupValue
+  SetupElem              :: SetupValue -> Int -> SetupValue
+  SetupField             :: SetupValue -> String -> SetupValue
+  SetupNull              :: SetupValue
+  SetupGlobal            :: String -> SetupValue
+  -- ^ A pointer to a global variable
+  SetupGlobalInitializer :: String -> SetupValue
+  -- ^ This represents the value of a global's initializer.
   deriving (Show)
 
 setupToTypedTerm :: Options -> SharedContext -> SetupValue -> MaybeT IO TypedTerm

src/SAWScript/CrucibleOverride.hs

@@ -562,14 +562,15 @@ matchPointsTos opts sc cc spec prepost = go False []
     setupVars :: SetupValue -> Set AllocIndex
     setupVars v =
       case v of
-        SetupVar    i  -> Set.singleton i
-        SetupStruct xs -> foldMap setupVars xs
-        SetupArray  xs -> foldMap setupVars xs
-        SetupElem x _  -> setupVars x
-        SetupField x _ -> setupVars x
-        SetupTerm   _  -> Set.empty
-        SetupNull      -> Set.empty
-        SetupGlobal _  -> Set.empty
+        SetupVar    i            -> Set.singleton i
+        SetupStruct xs           -> foldMap setupVars xs
+        SetupArray  xs           -> foldMap setupVars xs
+        SetupElem x _            -> setupVars x
+        SetupField x _           -> setupVars x
+        SetupTerm   _            -> Set.empty
+        SetupNull                -> Set.empty
+        SetupGlobal _            -> Set.empty
+        SetupGlobalInitializer _ -> Set.empty
 
 
 ------------------------------------------------------------------------
@@ -1059,14 +1060,15 @@ instantiateSetupValue ::
   IO SetupValue
 instantiateSetupValue sc s v =
   case v of
-    SetupVar _     -> return v
-    SetupTerm tt   -> SetupTerm <$> doTerm tt
-    SetupStruct vs -> SetupStruct <$> mapM (instantiateSetupValue sc s) vs
-    SetupArray  vs -> SetupArray <$> mapM (instantiateSetupValue sc s) vs
-    SetupElem _ _  -> return v
-    SetupField _ _ -> return v
-    SetupNull      -> return v
-    SetupGlobal _  -> return v
+    SetupVar _               -> return v
+    SetupTerm tt             -> SetupTerm   <$> doTerm tt
+    SetupStruct vs           -> SetupStruct <$> mapM (instantiateSetupValue sc s) vs
+    SetupArray  vs           -> SetupArray  <$> mapM (instantiateSetupValue sc s) vs
+    SetupElem _ _            -> return v
+    SetupField _ _           -> return v
+    SetupNull                -> return v
+    SetupGlobal _            -> return v
+    SetupGlobalInitializer _ -> return v
   where
     doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t
 

src/SAWScript/CrucibleResolveSetupValue.hs

@@ -1,5 +1,7 @@
-{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 
 module SAWScript.CrucibleResolveSetupValue
   ( LLVMVal, LLVMPtr
@@ -37,8 +39,9 @@ import qualified What4.Interface as W4
 import qualified What4.Expr.Builder as W4
 import qualified What4.ProgramLoc as W4
 
-import qualified Lang.Crucible.Backend.SAWCore as Crucible
-import qualified SAWScript.CrucibleLLVM as Crucible
+import qualified Lang.Crucible.LLVM.Translation      as CrucibleT
+import qualified Lang.Crucible.Backend.SAWCore       as Crucible
+import qualified SAWScript.CrucibleLLVM              as Crucible
 
 import Verifier.SAW.Rewriter
 import Verifier.SAW.SharedTerm
@@ -113,7 +116,7 @@ typeOfSetupValue cc env nameEnv val =
   do let ?lc = cc^.ccTypeCtx
      typeOfSetupValue' cc env nameEnv val
 
-typeOfSetupValue' ::
+typeOfSetupValue' :: forall m wptr.
   Monad m =>
   CrucibleContext wptr ->
   Map AllocIndex (W4.ProgramLoc, Crucible.MemType) ->
@@ -174,7 +177,14 @@ typeOfSetupValue' cc env nameEnv val =
       -- and b) it prevents us from doing a type-safe dereference
       -- operation.
       return (Crucible.PtrType Crucible.VoidType)
-    SetupGlobal name ->
+    -- A global and its initializer have the same type.
+    SetupGlobal            name -> findGlobalType name
+    SetupGlobalInitializer name -> findGlobalType name
+  where
+    lc = cc^.ccTypeCtx
+    dl = Crucible.llvmDataLayout lc
+    findGlobalType :: String -> m Crucible.MemType
+    findGlobalType name =
       do let m = cc^.ccLLVMModule
              tys = [ (L.globalSym g, L.globalType g) | g <- L.modGlobals m ] ++
                    [ (L.decName d, L.decFunType d) | d <- L.modDeclares m ] ++
@@ -185,13 +195,10 @@ typeOfSetupValue' cc env nameEnv val =
              case let ?lc = lc in Crucible.liftType ty of
                Nothing -> fail $ "typeOfSetupValue: invalid type " ++ show ty
                Just symTy -> return (Crucible.PtrType symTy)
-  where
-    lc = cc^.ccTypeCtx
-    dl = Crucible.llvmDataLayout lc
 
 -- | Translate a SetupValue into a Crucible LLVM value, resolving
 -- references
-resolveSetupVal ::
+resolveSetupVal :: forall arch.
   Crucible.HasPtrWidth (Crucible.ArchWidth arch) =>
   CrucibleContext arch ->
   Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) ->
@@ -250,6 +257,13 @@ resolveSetupVal cc env tyenv nameEnv val =
     SetupGlobal name ->
       do let mem = cc^.ccLLVMEmptyMem
          Crucible.ptrToPtrVal <$> Crucible.doResolveGlobal sym mem (L.Symbol name)
+    SetupGlobalInitializer name ->
+      case Map.lookup (L.Symbol name) (CrucibleT.globalMap $ cc^.ccLLVMModuleTrans) of
+        -- There was an error in global -> constant translation
+        Just (Left  e) -> fail e
+        Just (Right v) ->
+          let ?lc = lc in CrucibleT.constToLLVMVal @arch sym (cc^.ccLLVMEmptyMem) v
+        Nothing          -> fail $ "resolveSetupVal: global not found: " ++ name
   where
     sym = cc^.ccBackend
     lc = cc^.ccTypeCtx

src/SAWScript/Interpreter.hs

@@ -1756,6 +1756,15 @@ primitives = Map.fromList
     [ "Return a SetupValue representing a pointer to the named global."
     , "The String may be either the name of a global value or a function name." ]
 
+  , prim "crucible_global_initializer"
+    "String -> SetupValue"
+    (pureVal CIR.SetupGlobalInitializer)
+    [ "Return a SetupValue representing the value of the initializer of a named"
+    , "global. The String should be the name of a global value."
+    , "Note that initializing global variables may be unsound in the presence"
+    , "of compositional verification (see GaloisInc/saw-script#203)."
+    ] -- TODO: There should be a section in the manual about global-unsoundness.
+
   , prim "crucible_term"
     "Term -> SetupValue"
     (pureVal CIR.SetupTerm)