Add debug-intrinsics option to control translating llvm.dbg statements

Unfortunately, Clang can sometimes generate ill-scoped `llvm.dbg` statements
(see #778), so this patch adds a `debug-intrinsics` option that controls
whether `llvm.dbg` statements should be translated at all. The default value
for `crux-llvm` is `no`, as `crux-llvm` does not yet make use of `llvm.dbg`
information. We may wish to revisit this choice in the future should the
upstream LLVM bug (https://bugs.llvm.org/show_bug.cgi?id=51155) be fixed.

Fixes #778.

crucible-llvm/src/Lang/Crucible/LLVM/Translation.hs

@@ -187,7 +187,7 @@ buildRegTypeMap m0 bb = foldM stmt m0 (L.bbStmts bb)
 
 
 -- | Generate crucible code for each LLVM statement in turn.
-generateStmts :: (?laxArith :: Bool)
+generateStmts :: (?laxArith :: Bool, ?debugIntrinsics :: Bool)
         => TypeRepr ret
         -> L.BlockLabel
         -> [L.Stmt]
@@ -308,7 +308,7 @@ findFile _ = Nothing
 -- | Lookup the block info for the given LLVM block and then define a new crucible block
 --   by translating the given LLVM statements.
 defineLLVMBlock
-        :: (?laxArith :: Bool)
+        :: (?laxArith :: Bool, ?debugIntrinsics :: Bool)
         => TypeRepr ret
         -> Map L.BlockLabel (LLVMBlockInfo s)
         -> L.BasicBlock
@@ -326,7 +326,7 @@ defineLLVMBlock _ _ _ = fail "LLVM basic block has no label!"
 --
 --   This step introduces a new dummy entry point that simply jumps to the LLVM entry
 --   point.  It is inconvenient to avoid doing this when using the Generator interface.
-genDefn :: (?laxArith :: Bool)
+genDefn :: (?laxArith :: Bool, ?debugIntrinsics :: Bool)
         => L.Define
         -> TypeRepr ret
         -> LLVMGenerator s arch ret (Expr ext s ret)
@@ -357,7 +357,8 @@ genDefn defn retType =
 --
 -- | Translate a single LLVM function definition into a crucible CFG.
 transDefine :: forall arch wptr.
-               (HasPtrWidth wptr, wptr ~ ArchWidth arch, ?laxArith :: Bool, ?optLoopMerge :: Bool)
+               ( HasPtrWidth wptr, wptr ~ ArchWidth arch
+               , ?laxArith :: Bool, ?optLoopMerge :: Bool, ?debugIntrinsics :: Bool )
             => HandleAllocator
             -> LLVMContext arch
             -> L.Define
@@ -386,7 +387,7 @@ transDefine halloc ctx d = do
 -- | Translate a module into Crucible control-flow graphs.
 -- Note: We may want to add a map from symbols to existing function handles
 -- if we want to support dynamic loading.
-translateModule :: (?laxArith :: Bool, ?optLoopMerge :: Bool)
+translateModule :: (?laxArith :: Bool, ?optLoopMerge :: Bool, ?debugIntrinsics :: Bool)
                 => HandleAllocator -- ^ Generator for nonces.
                 -> GlobalVar Mem   -- ^ Memory model to associate with this context
                 -> L.Module        -- ^ Module to translate

crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs

@@ -1362,7 +1362,7 @@ translateSelect instr _ _ _ _ _ _ =
 
 -- | Do the heavy lifting of translating LLVM instructions to crucible code.
 generateInstr :: forall s arch ret a.
-   (?laxArith :: Bool) =>
+   (?laxArith :: Bool, ?debugIntrinsics :: Bool) =>
    TypeRepr ret   {- ^ Type of the function return value -} ->
    L.BlockLabel   {- ^ The label of the current LLVM basic block -} ->
    L.Instr        {- ^ The instruction to translate -} ->
@@ -1811,7 +1811,8 @@ callFunction instr _tailCall fnTy _fn _args _assign_f =
 -- | Generate a call to an LLVM function, with a continuation to fetch more
 -- instructions.
 callFunctionWithCont :: forall s arch ret a.
-   L.Instr {- ^ Source instruction o the call -} -> 
+   (?debugIntrinsics :: Bool) =>
+   L.Instr {- ^ Source instruction o the call -} ->
    Bool    {- ^ Is the function a tail call? -} ->
    L.Type  {- ^ type of the function to call -} ->
    L.Value {- ^ function value to call -} ->
@@ -1845,7 +1846,7 @@ callFunctionWithCont instr tailCall_ fnTy fn args assign_f k
               extensionStmt (LLVM_Debug (LLVM_Dbg_Value repr val lv di)) >> k
             _ -> k
 
-     -- Skip calls to debugging intrinsics.  We might want to support these in some way
+     -- Skip calls to other debugging intrinsics.  We might want to support these in some way
      -- in the future.  However, they take metadata values as arguments, which
      -- would require some work to support.
      | L.ValSymbol nm <- fn
@@ -1871,24 +1872,33 @@ callFunctionWithCont instr tailCall_ fnTy fn args assign_f k
      | otherwise = callFunction (Just instr) tailCall_ fnTy fn args assign_f >> k
 
 -- | Match the arguments used by @dbg.addr@, @dbg.declare@, and @dbg.value@.
-dbgArgs :: 
+dbgArgs ::
+  (?debugIntrinsics :: Bool) =>
   [L.Typed L.Value] {- ^ debug call arguments -} ->
   LLVMGenerator s arch ret (Either String (LLVMExpr s arch, L.DILocalVariable, L.DIExpression))
-dbgArgs args =
-  case args of
-    [valArg, lvArg, diArg] ->
-      case valArg of
-        L.Typed _ (L.ValMd (L.ValMdValue val)) ->
-          case lvArg of
-            L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoLocalVariable lv))) ->
-              case diArg of
-                L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoExpression di))) -> 
-                  do v <- transTypedValue val
-                     pure (Right (v, lv, di))
-                _ -> pure (Left ("dbg: argument 3 expected DIExpression, got: " ++ show diArg))
-            _ -> pure (Left ("dbg: argument 2 expected local variable metadata, got: " ++ show lvArg))
-        _ -> pure (Left ("dbg: argument 1 expected value metadata, got: " ++ show valArg))
-    _ -> pure (Left ("dbg: expected 3 arguments, got: " ++ show (length args)))     
+dbgArgs args
+  | -- Why guard translating llvm.dbg statements behind its own option? It's
+    -- because Clang can sometimes generate llvm.dbg statements with improperly
+    -- scoped arguments—see https://bugs.llvm.org/show_bug.cgi?id=51155. This
+    -- wreaks all sorts of havoc on Crucible's later analyses, so one can work
+    -- around the issue by not translating the llvm.dbg statements at all.
+    ?debugIntrinsics
+  = case args of
+      [valArg, lvArg, diArg] ->
+        case valArg of
+          L.Typed _ (L.ValMd (L.ValMdValue val)) ->
+            case lvArg of
+              L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoLocalVariable lv))) ->
+                case diArg of
+                  L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoExpression di))) ->
+                    do v <- transTypedValue val
+                       pure (Right (v, lv, di))
+                  _ -> pure (Left ("dbg: argument 3 expected DIExpression, got: " ++ show diArg))
+              _ -> pure (Left ("dbg: argument 2 expected local variable metadata, got: " ++ show lvArg))
+          _ -> pure (Left ("dbg: argument 1 expected value metadata, got: " ++ show valArg))
+      _ -> pure (Left ("dbg: expected 3 arguments, got: " ++ show (length args)))
+  | otherwise
+  = pure (Left ("Not translating llvm.dbg statement due to debugIntrinsics not being enabled"))
 
 typedValueAsCrucibleValue ::
   L.Typed L.Value ->

crucible-llvm/test/MemSetup.hs

@@ -62,6 +62,7 @@ withLLVMCtx mod' action =
         sym <- CBS.newSimpleBackend CBS.FloatRealRepr nonceGen
         let ?laxArith = False
         let ?optLoopMerge = False
+        let ?debugIntrinsics = False
         memVar <- LLVMM.mkMemVar "test_llvm_memory" halloc
         Some (LLVMTr.ModuleTranslation _ ctx _ _) <- LLVMTr.translateModule halloc memVar mod'
         case LLVMTr.llvmArch ctx            of { LLVME.X86Repr width ->

crucible-llvm/test/Tests.hs

@@ -222,6 +222,7 @@ testBuildTranslation srcPath llvmTransTests =
       trans = do halloc <- newHandleAllocator
                  let ?laxArith = False
                  let ?optLoopMerge = False
+                 let ?debugIntrinsics = False
                  memVar <- mkMemVar "buildTranslation_test_llvm_memory" halloc
                  translateModule halloc memVar =<<
                    (fromRight (error "parsing was already verified") <$> parseLLVM bcPath)

crux-llvm/src/Crux/LLVM/Config.hs

@@ -71,6 +71,7 @@ data LLVMOptions = LLVMOptions
   , noCompile :: Bool
   , optLevel :: Int
   , loopMerge :: Bool
+  , debugIntrinsics :: Bool
   }
 
 -- | The @c-src@ directory, which contains @crux-llvm@–specific files such as
@@ -161,6 +162,9 @@ llvmCruxConfig = do
          loopMerge <- Crux.section "opt-loop-merge" Crux.yesOrNoSpec False
                         "Insert merge blocks in loops with early exits (i.e. breaks or returns). This may improve simulation performance."
 
+         debugIntrinsics <- Crux.section "debug-intrinsics" Crux.yesOrNoSpec False
+                              "Translate statements using certain llvm.dbg intrinsic functions."
+
          return LLVMOptions { .. }
 
    , Crux.cfgEnv  =

crux-llvm/src/Crux/LLVM/Simulate.hs

@@ -192,6 +192,7 @@ prepLLVMModule llvmOpts halloc sym bcFile memVar = do
     llvmMod <- parseLLVM bcFile
     Some trans <- let ?laxArith = laxArithmetic llvmOpts
                       ?optLoopMerge = loopMerge llvmOpts
+                      ?debugIntrinsics = debugIntrinsics llvmOpts
                   in translateModule halloc memVar llvmMod
     mem <- let llvmCtxt = trans ^. transContext in
              let ?lc = llvmCtxt ^. llvmTypeCtx

crux-llvm/test-data/golden/T778.c

@@ -0,0 +1,22 @@
+unsigned int addflt(unsigned int a , unsigned int b )
+{
+  unsigned int ma = a;
+  unsigned int mb = b;
+  int ea = (int)(a >> 24U) - 128;
+  int eb = (int)(b >> 24U) - 128;
+  unsigned int delta = ea - eb;
+
+  mb = mb >> delta;
+  ma = ma + mb;
+
+  // This if statement seems critical
+  if (ma) {
+    ea = ea + 1;
+  }
+
+  return ((unsigned int) ea);
+}
+
+int main() {
+  return 0;
+}

crux-llvm/test-data/golden/T778.config

@@ -0,0 +1,3 @@
+-- We may wish to reconsider this choice if
+-- https://bugs.llvm.org/show_bug.cgi?id=51155 is fixed in the future.
+debug-intrinsics: no

crux-llvm/test-data/golden/T778.good

@@ -0,0 +1 @@
+[Crux] Overall status: Valid.

uc-crux-llvm/src/UCCrux/LLVM/Main.hs

@@ -177,6 +177,7 @@ translateLLVMModule ucOpts halloc memVar moduleFilePath llvmMod =
     Some trans <-
       let ?laxArith = laxArithmetic llvmOpts
           ?optLoopMerge = loopMerge llvmOpts
+          ?debugIntrinsics = debugIntrinsics llvmOpts
        in translateModule halloc memVar llvmMod
     llvmPtrWidth
       (trans ^. transContext)