Add {enable_disable}_debug_intrinsics

saw-remote-api/src/SAWServer.hs

@@ -219,6 +219,7 @@ initialState readFileFn =
                 , rwCrucibleAssertThenAssume = False
                 , rwLaxArith = False
                 , rwLaxPointerOrdering = False
+                , rwDebugIntrinsics = True
                 , rwWhat4HashConsing = False
                 , rwWhat4HashConsingX86 = False
                 , rwStackBaseAlign = defaultStackBaseAlign

saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs

@@ -43,9 +43,11 @@ import SAWScript.Crucible.LLVM.Builtins
     , llvm_return
     , llvm_precond
     , llvm_postcond )
+import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as CL
 import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS
 import qualified SAWScript.Crucible.Common.MethodSpec as CMS (GhostGlobal)
-import SAWScript.Value (BuiltinContext, LLVMCrucibleSetupM(..), biSharedContext)
+import SAWScript.Value
+    ( BuiltinContext, LLVMCrucibleSetupM(..), TopLevelRW(..), biSharedContext )
 import qualified Verifier.SAW.CryptolEnv as CEnv
 import Verifier.SAW.CryptolEnv (CryptolEnv)
 import Verifier.SAW.TypedTerm (TypedTerm)
@@ -57,6 +59,7 @@ import SAWServer as Server
       SAWState,
       CrucibleSetupVal(..),
       sawTask,
+      sawTopLevelRW,
       getHandleAlloc,
       setServerVal )
 import SAWServer.Data.Contract
@@ -209,7 +212,11 @@ llvmLoadModule (LLVMLoadModuleParams serverName fileName) =
      case tasks of
        (_:_) -> Argo.raise $ notAtTopLevel $ map fst tasks
        [] ->
-         do let ?laxArith = False -- TODO read from config
+         do rw <- view sawTopLevelRW <$> Argo.getState
+            let ?transOpts = CL.defaultTranslationOptions
+                               { CL.laxArith        = rwLaxArith rw
+                               , CL.debugIntrinsics = rwDebugIntrinsics rw
+                               }
             halloc <- getHandleAlloc
             loaded <- liftIO (CMS.loadLLVMModule fileName halloc)
             case loaded of

saw-remote-api/src/SAWServer/SetOption.hs

@@ -33,6 +33,8 @@ setOption opt =
          updateRW rw { rwLaxArith = enabled }
        EnableLaxPointerOrdering enabled ->
          updateRW rw { rwLaxPointerOrdering = enabled }
+       EnableDebugIntrinsics enabled ->
+         updateRW rw { rwDebugIntrinsics = enabled }
        EnableSMTArrayMemoryModel enabled ->
          updateRW rw { rwSMTArrayMemoryModel = enabled }
        EnableWhat4HashConsing enabled ->
@@ -42,6 +44,7 @@ setOption opt =
 data SetOptionParams
   = EnableLaxArithmetic Bool
   | EnableLaxPointerOrdering Bool
+  | EnableDebugIntrinsics Bool
   | EnableSMTArrayMemoryModel Bool
   | EnableWhat4HashConsing Bool
 
@@ -50,6 +53,7 @@ parseOption o name =
   case name of
     "lax arithmetic" -> EnableLaxArithmetic <$> o .: "value"
     "lax pointer ordering" -> EnableLaxPointerOrdering <$> o .: "value"
+    "debug intrinsics" -> EnableDebugIntrinsics <$> o .: "value"
     "SMT array memory model" -> EnableSMTArrayMemoryModel <$> o .: "value"
     "What4 hash consing" -> EnableWhat4HashConsing <$> o .: "value"
     _ -> empty
@@ -65,6 +69,7 @@ instance Doc.DescribedMethod SetOptionParams OK where
        Doc.Paragraph [Doc.Text "The option to set and its accompanying value (i.e., true or false); one of the following:"
                      , Doc.Literal "lax arithmetic", Doc.Text ", "
                      , Doc.Literal "lax pointer ordering", Doc.Text ", "
+                     , Doc.Literal "debug intrinsics", Doc.Text ", "
                      , Doc.Literal "SMT array memory model", Doc.Text ", or "
                      , Doc.Literal "What4 hash consing"
                      ])

src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs

@@ -79,6 +79,8 @@ module SAWScript.Crucible.LLVM.CrucibleLLVM
   , LLVMContext
   , translateModule
   , llvmDeclToFunHandleRepr'
+  , TranslationOptions(..)
+  , defaultTranslationOptions
     -- * Re-exports from "Lang.Crucible.LLVM.MemModel"
   , doResolveGlobal
   , Mem
@@ -166,7 +168,8 @@ import Lang.Crucible.LLVM.Globals
 
 import Lang.Crucible.LLVM.Translation
   (llvmMemVar, cfgMap, transContext, llvmPtrWidth, llvmTypeCtx,
-   ModuleTranslation, LLVMContext, translateModule, llvmDeclToFunHandleRepr')
+   ModuleTranslation, LLVMContext, translateModule, llvmDeclToFunHandleRepr',
+   TranslationOptions(..), defaultTranslationOptions)
 
 import Lang.Crucible.LLVM.MemModel
   (Mem, MemImpl, doResolveGlobal, storeRaw, storeConstRaw, mallocRaw, mallocConstRaw,

src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

@@ -248,7 +248,7 @@ modTrans = _modTrans
 -- | Load an LLVM module from the given bitcode file, then parse and
 -- translate to Crucible.
 loadLLVMModule ::
-  (?laxArith :: Bool) =>
+  (?transOpts :: CL.TranslationOptions) =>
   FilePath ->
   Crucible.HandleAllocator ->
   IO (Either LLVM.Error (Some LLVMModule))
@@ -257,8 +257,7 @@ loadLLVMModule file halloc =
      case parseResult of
        Left err -> return (Left err)
        Right llvm_mod ->
-         do let ?optLoopMerge = False
-            memVar <- CL.mkMemVar (Text.pack "saw:llvm_memory") halloc
+         do memVar <- CL.mkMemVar (Text.pack "saw:llvm_memory") halloc
             Some mtrans <- CL.translateModule halloc memVar llvm_mod
             return (Right (Some (LLVMModule file llvm_mod mtrans)))
 

src/SAWScript/Interpreter.hs

@@ -480,6 +480,7 @@ buildTopLevelEnv proxy opts =
                    , rwProfilingFile = Nothing
                    , rwLaxArith = False
                    , rwLaxPointerOrdering = False
+                   , rwDebugIntrinsics = True
                    , rwWhat4HashConsing = False
                    , rwWhat4HashConsingX86 = False
                    , rwPreservedRegs = []
@@ -564,6 +565,16 @@ disable_lax_pointer_ordering = do
   rw <- getTopLevelRW
   putTopLevelRW rw { rwLaxPointerOrdering = False }
 
+enable_debug_intrinsics :: TopLevel ()
+enable_debug_intrinsics = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwDebugIntrinsics = True }
+
+disable_debug_intrinsics :: TopLevel ()
+disable_debug_intrinsics = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwDebugIntrinsics = False }
+
 enable_what4_hash_consing :: TopLevel ()
 enable_what4_hash_consing = do
   rw <- getTopLevelRW
@@ -805,6 +816,16 @@ primitives = Map.fromList
     Current
     [ "Disable lax rules for pointer ordering comparisons in Crucible." ]
 
+  , prim "enable_debug_intrinsics" "TopLevel ()"
+    (pureVal enable_debug_intrinsics)
+    Current
+    [ "Enable translating statements using certain llvm.dbg intrinsic functions in Crucible." ]
+
+  , prim "disable_debug_intrinsics" "TopLevel ()"
+    (pureVal disable_debug_intrinsics)
+    Current
+    [ "Disable translating statements using certain llvm.dbg intrinsic functions in Crucible." ]
+
   , prim "enable_what4_hash_consing" "TopLevel ()"
     (pureVal enable_what4_hash_consing)
     Current

src/SAWScript/LLVMBuiltins.hs

@@ -32,12 +32,17 @@ import qualified Text.LLVM.Parser as LLVM (parseType)
 
 import SAWScript.Value as SV
 
+import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as CL
 import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (LLVMModule, loadLLVMModule)
 
 llvm_load_module :: FilePath -> TopLevel (Some CMS.LLVMModule)
 llvm_load_module file =
   do laxArith <- gets rwLaxArith
-     let ?laxArith = laxArith
+     debugIntrinsics <- gets rwDebugIntrinsics
+     let ?transOpts = CL.defaultTranslationOptions
+                        { CL.laxArith = laxArith
+                        , CL.debugIntrinsics = debugIntrinsics
+                        }
      halloc <- getHandleAlloc
      io (CMS.loadLLVMModule file halloc) >>= \case
        Left err -> fail (LLVM.formatError err)

src/SAWScript/Value.hs

@@ -435,6 +435,7 @@ data TopLevelRW =
   , rwProfilingFile :: Maybe FilePath
   , rwLaxArith :: Bool
   , rwLaxPointerOrdering :: Bool
+  , rwDebugIntrinsics :: Bool
 
   -- FIXME: These might be better split into "simulator hash-consing" and "tactic hash-consing"
   , rwWhat4HashConsing :: Bool