crucible-llvm: Add llvm debug statements

Author: glguy

Diff for: crucible-llvm/src/Lang/Crucible/LLVM/Extension/Syntax.hs

@@ -227,6 +227,43 @@ data LLVMStmt (f :: CrucibleType -> Type) :: CrucibleType -> Type where
      !(f (LLVMPointerType wptr)) {- Second pointer -} ->
      LLVMStmt f (BVType wptr)
 
+  -- | Debug information
+  LLVM_Debug ::
+    !(LLVM_Dbg f c)              {- Debug variant -} ->
+    LLVMStmt f UnitType
+
+-- | Debug statement variants - these have no semantic meaning
+data LLVM_Dbg f c where
+  -- | Annotates a value pointed to by a pointer with local-variable debug information
+  -- 
+  -- <https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-addr>
+  LLVM_Dbg_Addr ::
+    HasPtrWidth wptr =>
+    !(f (LLVMPointerType wptr))  {- Pointer to local variable -} ->
+    L.DILocalVariable            {- Local variable information -} ->
+    L.DIExpression               {- Complex expression -} ->
+    LLVM_Dbg f (LLVMPointerType wptr)
+
+  -- | Annotates a value pointed to by a pointer with local-variable debug information
+  -- 
+  -- <https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-declare>
+  LLVM_Dbg_Declare ::
+    HasPtrWidth wptr =>
+    !(f (LLVMPointerType wptr))  {- Pointer to local variable -} ->
+    L.DILocalVariable            {- Local variable information -} ->
+    L.DIExpression               {- Complex expression -} ->
+    LLVM_Dbg f (LLVMPointerType wptr)
+
+  -- | Annotates a value with local-variable debug information
+  --
+  -- <https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-value>
+  LLVM_Dbg_Value ::
+    !(TypeRepr c)                {- Type of local variable -} ->
+    !(f c)                       {- Value of local variable -} ->
+    L.DILocalVariable            {- Local variable information -} ->
+    L.DIExpression               {- Complex expression -} ->
+    LLVM_Dbg f c
+
 $(return [])
 
 instance TypeApp LLVMExtensionExpr where
@@ -315,6 +352,7 @@ instance TypeApp LLVMStmt where
     LLVM_PtrLe{} -> knownRepr
     LLVM_PtrAddOffset w _ _ _ -> LLVMPointerRepr w
     LLVM_PtrSubtract w _ _ _ -> BVRepr w
+    LLVM_Debug{} -> knownRepr
 
 instance PrettyApp LLVMStmt where
   ppApp pp = \case
@@ -342,6 +380,13 @@ instance PrettyApp LLVMStmt where
        pretty "ptrAddOffset" <+> ppGlobalVar mvar <+> pp x <+> pp y
     LLVM_PtrSubtract _ mvar x y ->
        pretty "ptrSubtract" <+> ppGlobalVar mvar <+> pp x <+> pp y
+    LLVM_Debug dbg -> ppApp pp dbg
+
+instance PrettyApp LLVM_Dbg where
+  ppApp pp = \case
+    LLVM_Dbg_Addr    x _ _ -> pretty "dbg.addr"    <+> pp x
+    LLVM_Dbg_Declare x _ _ -> pretty "dbg.declare" <+> pp x
+    LLVM_Dbg_Value _ x _ _ -> pretty "dbg.value"   <+> pp x
 
 -- TODO: move to a Pretty instance
 ppGlobalVar :: GlobalVar Mem -> Doc ann
@@ -351,6 +396,26 @@ ppGlobalVar = viaShow
 ppAlignment :: Alignment -> Doc ann
 ppAlignment = viaShow
 
+instance TestEqualityFC LLVM_Dbg where
+  testEqualityFC testSubterm = $(U.structuralTypeEquality [t|LLVM_Dbg|]
+    [(U.DataArg 0 `U.TypeApp` U.AnyType, [|testSubterm|])
+    ,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
+    ])
+
+instance OrdFC LLVM_Dbg where
+  compareFC compareSubterm = $(U.structuralTypeOrd [t|LLVM_Dbg|]
+    [(U.DataArg 0 `U.TypeApp` U.AnyType, [|compareSubterm|])
+    ,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])
+    ])
+
+instance FoldableFC LLVM_Dbg where
+  foldMapFC = foldMapFCDefault
+instance FunctorFC LLVM_Dbg where
+  fmapFC = fmapFCDefault
+
+instance TraversableFC LLVM_Dbg where
+  traverseFC = $(U.structuralTraversal [t|LLVM_Dbg|] [])
+
 instance TestEqualityFC LLVMStmt where
   testEqualityFC testSubterm =
     $(U.structuralTypeEquality [t|LLVMStmt|]
@@ -359,6 +424,7 @@ instance TestEqualityFC LLVMStmt where
        ,(U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|testEquality|])
        ,(U.ConType [t|CtxRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
        ,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
+       ,(U.ConType [t|LLVM_Dbg|] `U.TypeApp` U.DataArg 0 `U.TypeApp` U.AnyType, [|testEqualityFC testSubterm|])
        ])
 
 instance OrdFC LLVMStmt where
@@ -369,6 +435,7 @@ instance OrdFC LLVMStmt where
        ,(U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|compareF|])
        ,(U.ConType [t|CtxRepr|] `U.TypeApp` U.AnyType, [|compareF|])
        ,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])
+       ,(U.ConType [t|LLVM_Dbg|] `U.TypeApp` U.DataArg 0 `U.TypeApp` U.AnyType, [|compareFC compareSubterm|])
        ])
 
 instance FunctorFC LLVMStmt where
@@ -379,4 +446,6 @@ instance FoldableFC LLVMStmt where
 
 instance TraversableFC LLVMStmt where
   traverseFC =
-    $(U.structuralTraversal [t|LLVMStmt|] [])
+    $(U.structuralTraversal [t|LLVMStmt|]
+      [(U.ConType [t|LLVM_Dbg|] `U.TypeApp` U.DataArg 0 `U.TypeApp` U.AnyType, [|traverseFC|])
+      ])

Diff for: crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs

@@ -518,6 +518,8 @@ evalStmt sym = eval
   eval (LLVM_PtrSubtract _w mvar (regValue -> x) (regValue -> y)) =
     do mem <- getMem mvar
        liftIO $ doPtrSubtract sym mem x y
+  
+  eval LLVM_Debug{} = pure ()
 
 
 mkMemVar :: Text

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

@@ -1820,13 +1820,32 @@ callFunctionWithCont :: forall s arch ret a.
    LLVMGenerator s arch ret a {- ^ continuation for next instructions -} ->
    LLVMGenerator s arch ret a
 callFunctionWithCont instr tailCall_ fnTy fn args assign_f k
+
+     | L.ValSymbol "llvm.dbg.declare" <- fn =
+       do (val, lv, di) <- dbgArgs args
+          ptr <- case asScalar val of
+                   Scalar _ PtrRepr ptr -> pure ptr
+                   _ -> fail "dbg.declare: expected pointer"
+          extensionStmt (LLVM_Debug (LLVM_Dbg_Declare ptr lv di)) >> k
+
+     | L.ValSymbol "llvm.dbg.addr" <- fn =
+       do (val, lv, di) <- dbgArgs args
+          ptr <- case asScalar val of
+                   Scalar _ PtrRepr ptr -> pure ptr
+                   _ -> fail "dbg.addr: expected pointer"
+          extensionStmt (LLVM_Debug (LLVM_Dbg_Addr ptr lv di)) >> k
+
+     | L.ValSymbol "llvm.dbg.value" <- fn =
+       do (val, lv, di) <- dbgArgs args
+          case asScalar val of
+            Scalar _ repr v1 -> extensionStmt (LLVM_Debug (LLVM_Dbg_Value repr v1 lv di)) >> k
+            NotScalar -> fail "dbg.value: expected scalar"
+
      -- Skip calls to 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
-     , nm `elem` [ "llvm.dbg.declare"
-                 , "llvm.dbg.value"
-                 , "llvm.dbg.label"
+     , nm `elem` [ "llvm.dbg.label"
                  , "llvm.lifetime.start"
                  , "llvm.lifetime.start.p0i8"
                  , "llvm.lifetime.end"
@@ -1847,6 +1866,30 @@ 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 :: 
+  [L.Typed L.Value] {- ^ debug call arguments -} ->
+  LLVMGenerator s arch ret (LLVMExpr s arch, L.DILocalVariable, L.DIExpression)
+dbgArgs args =
+  do (valArg, lvArg, diArg) <-
+       case args of
+         [valArg, lvArg, diArg] -> pure (valArg, lvArg, diArg)
+         _ -> fail "dbg expected 3 arguments"
+     val <-
+       case valArg of
+         L.Typed _ (L.ValMd (L.ValMdValue val)) -> pure val
+         _ -> fail "dbg: argument 1 expected value metadata"
+     lv <-
+       case lvArg of
+         L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoLocalVariable lv))) -> pure lv
+         _ -> fail "dbg: argument 2 expected local variable metadata"
+     di <-
+       case diArg of
+         L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoExpression di))) -> pure di
+         _ -> fail "dbg: argument 3 expected DIExpression"
+     v <- transTypedValue val
+     pure (v, lv, di)
+
 typedValueAsCrucibleValue ::
   L.Typed L.Value ->
   LLVMGenerator s arch ret (Some (Value s))