Dbg def use

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

@@ -27,8 +27,10 @@ module Lang.Crucible.LLVM.Ctors
  ) where
 
 import Data.Data (Data)
+import Data.IORef (newIORef)
 import Data.String(fromString)
 import Data.Typeable (Typeable)
+import qualified Data.Text as Text
 import GHC.Generics (Generic)
 import Data.Parameterized.Nonce
 
@@ -160,12 +162,15 @@ generatorToCFG :: forall arch wptr ret. (HasPtrWidth wptr, wptr ~ ArchWidth arch
  -> TypeRepr ret
  -> IO (Core.SomeCFG LLVM Core.EmptyCtx ret)
 generatorToCFG name halloc llvmctx gen ret = do
+ ref <- newIORef []
  let ?lc = _llvmTypeCtx llvmctx
  let def :: forall args. FunctionDef LLVM (LLVMState arch) args ret IO
  def _inputs = (state, gen)
  where state = LLVMState { _identMap = empty
  , _blockInfoMap = empty
  , llvmContext = llvmctx
+ , _translationWarnings = ref
+ , _functionSymbol = L.Symbol (Text.unpack name)
  }
 
  hand <- mkHandle' halloc (functionNameFromText name) Ctx.empty ret

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

@@ -89,13 +89,17 @@ module Lang.Crucible.LLVM.Translation
 
 import Control.Lens hiding (op, (:>) )
 import Control.Monad.Except
+import Data.IORef (IORef, newIORef, readIORef)
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
 import Data.Maybe
 import Data.String
 import qualified Data.Text as Text
 
 import qualified Text.LLVM.AST as L
+import qualified Text.LLVM.PP as L
 
 import Data.Parameterized.NatRepr as NatRepr
 import Data.Parameterized.Some
@@ -192,21 +196,26 @@ buildRegTypeMap m0 bb = foldM stmt m0 (L.bbStmts bb)
 generateStmts :: (?transOpts :: TranslationOptions)
  => TypeRepr ret
  -> L.BlockLabel
+ -> Set L.Ident {- ^ Set of usable identifiers -}
  -> [L.Stmt]
  -> LLVMGenerator s arch ret a
-generateStmts retType lab stmts = go (processDbgDeclare stmts)
- where go [] = fail "LLVM basic block ended without a terminating instruction"
- go (x:xs) =
+generateStmts retType lab defSet0 stmts = go defSet0 (processDbgDeclare stmts)
+ where go _ [] = fail "LLVM basic block ended without a terminating instruction"
+ go defSet (x:xs) =
  case x of
  -- a result statement assigns the result of the instruction into a register
- L.Result ident instr md -> do
- setLocation md
- generateInstr retType lab instr (assignLLVMReg ident) (go xs)
+ L.Result ident instr md ->
+ do setLocation md
+ generateInstr retType lab defSet instr
+ (assignLLVMReg ident)
+ (go (Set.insert ident defSet) xs)
 
  -- an effect statement simply executes the instruction for its effects and discards the result
- L.Effect instr md -> do
- setLocation md
- generateInstr retType lab instr (\_ -> return ()) (go xs)
+ L.Effect instr md ->
+ do setLocation md
+ generateInstr retType lab defSet instr
+ (\_ -> return ())
+ (go defSet xs)
 
 -- | Search for calls to intrinsic 'llvm.dbg.declare' and copy the
 -- metadata onto the corresponding 'alloca' statement. Also copy
@@ -317,7 +326,7 @@ defineLLVMBlock
  -> LLVMGenerator s arch ret ()
 defineLLVMBlock retType lm L.BasicBlock{ L.bbLabel = Just lab, L.bbStmts = stmts } = do
  case Map.lookup lab lm of
- Just bi -> defineBlock (block_label bi) (generateStmts retType lab stmts)
+ Just bi -> defineBlock (block_label bi) (generateStmts retType lab (block_use_set bi) stmts)
  Nothing -> fail $ unwords ["LLVM basic block not found in block info map", show lab]
 
 defineLLVMBlock _ _ _ = fail "LLVM basic block has no label!"
@@ -351,9 +360,30 @@ genDefn defn retType =
  case Map.lookup entry_lab bim of
  Nothing -> fail $ unwords ["entry label not found in label map:", show entry_lab]
  Just entry_bi -> do
+ checkEntryPointUseSet nm entry_bi (L.defArgs defn)
  mapM_ (defineLLVMBlock retType bim) (L.defBody defn)
  jump (block_label entry_bi)
 
+
+-- | Check that the input LLVM CFG satisfies the def/use invariant,
+-- and raise an error if some virtual register has a use site that
+-- is not dominated by its definition site.
+checkEntryPointUseSet ::
+ String ->
+ LLVMBlockInfo s ->
+ [L.Typed L.Ident] ->
+ LLVMGenerator s arg ret ()
+checkEntryPointUseSet nm bi args
+ | Set.null unsatisfiedUses = return ()
+ | otherwise = fail $ unlines $
+ [ "Invalid input LLVM for function: " ++ nm
+ , "The following LLVM virtual registers are used before they are defined:"
+ ] ++ map (\i -> " " ++ show (L.ppIdent i)) (Set.toList unsatisfiedUses)
+ where
+ argSet = Set.fromList (map L.typedValue args)
+ useSet = block_use_set bi
+ unsatisfiedUses = Set.difference useSet argSet
+
 ------------------------------------------------------------------------
 -- transDefine
 --
@@ -362,9 +392,10 @@ transDefine :: forall arch wptr.
  (HasPtrWidth wptr, wptr ~ ArchWidth arch, ?transOpts :: TranslationOptions)
  => HandleAllocator
  -> LLVMContext arch
+ -> IORef [(L.Symbol, Position, Text.Text)]
  -> L.Define
  -> IO (L.Symbol, (L.Declare, C.AnyCFG LLVM))
-transDefine halloc ctx d = do
+transDefine halloc ctx warnRef d = do
  let ?lc = ctx^.llvmTypeCtx
  let decl = declareFromDefine d
  let symb@(L.Symbol symb_str) = L.defName d
@@ -374,7 +405,7 @@ transDefine halloc ctx d = do
  h <- mkHandle' halloc fn_name argTypes retType
  let def :: FunctionDef LLVM (LLVMState arch) args ret IO
  def inputs = (s, f)
- where s = initialState d ctx argTypes inputs
+ where s = initialState d ctx argTypes inputs warnRef
  f = genDefn d retType
  sng <- newIONonceGenerator
  (SomeCFG g, []) <- defineFunctionOpt InternalPos sng h def $ \ng cfg ->
@@ -386,19 +417,21 @@ transDefine halloc ctx d = do
 -- translateModule
 
 -- | Translate a module into Crucible control-flow graphs.
+-- Return the translated module and a list of warning messages
+-- generated during translation.
 -- Note: We may want to add a map from symbols to existing function handles
 -- if we want to support dynamic loading.
 translateModule :: (?transOpts :: TranslationOptions)
  => HandleAllocator -- ^ Generator for nonces.
  -> GlobalVar Mem -- ^ Memory model to associate with this context
  -> L.Module -- ^ Module to translate
- -> IO (Some ModuleTranslation)
+ -> IO (Some ModuleTranslation, [(L.Symbol, Position, Text.Text)])
 translateModule halloc mvar m = do
+ warnRef <- newIORef []
  Some ctx <- mkLLVMContext mvar m
  let nonceGen = haCounter halloc
- llvmPtrWidth ctx $ \wptr -> withPtrWidth wptr $
- do pairs <- mapM (transDefine halloc ctx) (L.modDefines m)
-
+ mtrans <- llvmPtrWidth ctx $ \wptr -> withPtrWidth wptr $
+ do pairs <- mapM (transDefine halloc ctx warnRef) (L.modDefines m)
  let ?lc = ctx^.llvmTypeCtx -- implicitly passed to makeGlobalMap
  let ctx' = ctx{ llvmGlobalAliases = globalAliases m
  , llvmFunctionAliases = functionAliases m
@@ -409,3 +442,5 @@ translateModule halloc mvar m = do
  , _transContext = ctx'
  , modTransNonce = nonce
  }))
+ warns <- readIORef warnRef
+ return (mtrans, warns)

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

@@ -47,6 +47,8 @@ import qualified Data.List as List
 import Data.List.NonEmpty (NonEmpty((:|)))
 import qualified Data.Map.Strict as Map
 import Data.Maybe
+import Data.Set (Set)
+import qualified Data.Set as Set
 import Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
 import Data.String
@@ -57,6 +59,7 @@ import Prettyprinter (pretty)
 import GHC.Exts ( Proxy#, proxy# )
 
 import qualified Text.LLVM.AST as L
+import qualified Text.LLVM.PP as L
 
 import qualified Data.BitVector.Sized as BV
 import qualified Data.Parameterized.Context as Ctx
@@ -1384,6 +1387,7 @@ generateInstr :: forall s arch ret a.
  (?transOpts :: TranslationOptions) =>
  TypeRepr ret {- ^ Type of the function return value -} ->
  L.BlockLabel {- ^ The label of the current LLVM basic block -} ->
+ Set L.Ident {- ^ Set of usable identifiers -} ->
  L.Instr {- ^ The instruction to translate -} ->
  (LLVMExpr s arch -> LLVMGenerator s arch ret ())
  {- ^ A continuation to assign the produced value of this instruction to a register -} ->
@@ -1392,7 +1396,7 @@ generateInstr :: forall s arch ret a.
  Straightline instructions should enter this continuation,
  but block-terminating instructions should not. -} ->
  LLVMGenerator s arch ret a
-generateInstr retType lab instr assign_f k =
+generateInstr retType lab defSet instr assign_f k =
  case instr of
  -- skip phi instructions, they are handled in definePhiBlock
  L.Phi _ _ -> k
@@ -1575,12 +1579,12 @@ generateInstr retType lab instr assign_f k =
  k
 
  L.Call tailcall (L.PtrTo fnTy) fn args ->
- callFunctionWithCont instr tailcall fnTy fn args assign_f k
+ callFunctionWithCont defSet instr tailcall fnTy fn args assign_f k
  L.Call _ ty _ _ ->
  fail $ unwords ["unexpected function type in call:", show ty]
 
  L.Invoke fnTy fn args normLabel _unwindLabel -> do
- callFunctionWithCont instr False fnTy fn args assign_f $ definePhiBlock lab normLabel
+ callFunctionWithCont defSet instr False fnTy fn args assign_f $ definePhiBlock lab normLabel
 
  L.Bit op x y ->
  do tp <- liftMemType' (L.typedType x)
@@ -1879,45 +1883,53 @@ callFunction instr _tailCall fnTy _fn _args _assign_f =
 -- instructions.
 callFunctionWithCont :: forall s arch ret a.
  (?transOpts :: TranslationOptions) =>
- L.Instr {- ^ Source instruction o the call -} ->
+ Set L.Ident {- ^ Set of usable identifiers -} ->
+ L.Instr {- ^ Source instruction of the call -} ->
  Bool {- ^ Is the function a tail call? -} ->
  L.Type {- ^ type of the function to call -} ->
  L.Value {- ^ function value to call -} ->
  [L.Typed L.Value] {- ^ argument list -} ->
  (LLVMExpr s arch -> LLVMGenerator s arch ret ()) {- ^ assignment continuation for return value -} ->
  LLVMGenerator s arch ret a {- ^ continuation for next instructions -} ->
  LLVMGenerator s arch ret a
-callFunctionWithCont instr tailCall_ fnTy fn args assign_f k
+callFunctionWithCont defSet instr tailCall_ fnTy fn args assign_f k
 
  -- Supports LLVM 4-12
- | L.ValSymbol "llvm.dbg.declare" <- fn =
- do mbArgs <- dbgArgs args
+ | L.ValSymbol "llvm.dbg.declare" <- fn
+ , debugIntrinsics ?transOpts =
+ do mbArgs <- dbgArgs defSet args
  case mbArgs of
  Right (asScalar -> Scalar _ PtrRepr ptr, lv, di) ->
  extensionStmt (LLVM_Debug (LLVM_Dbg_Declare ptr lv di)) >> k
+ Left msg -> addWarning (Text.pack msg) >> k
  _ -> k
 
  -- Supports LLVM 6-12
- | L.ValSymbol "llvm.dbg.addr" <- fn =
- do mbArgs <- dbgArgs args
+ | L.ValSymbol "llvm.dbg.addr" <- fn
+ , debugIntrinsics ?transOpts =
+ do mbArgs <- dbgArgs defSet args
  case mbArgs of
  Right (asScalar -> Scalar _ PtrRepr ptr, lv, di) ->
  extensionStmt (LLVM_Debug (LLVM_Dbg_Addr ptr lv di)) >> k
+ Left msg -> addWarning (Text.pack msg) >> k
  _ -> k
 
  -- Supports LLVM 6-12 (earlier versions had an extra argument)
- | L.ValSymbol "llvm.dbg.value" <- fn =
- do mbArgs <- dbgArgs args
+ | L.ValSymbol "llvm.dbg.value" <- fn
+ , debugIntrinsics ?transOpts =
+ do mbArgs <- dbgArgs defSet args
  case mbArgs of
  Right (asScalar -> Scalar _ repr val, lv, di) ->
  extensionStmt (LLVM_Debug (LLVM_Dbg_Value repr val lv di)) >> k
+ Left msg -> addWarning (Text.pack msg) >> k
  _ -> k
 
- -- 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.
+ -- Skip calls to other debugging intrinsics.
  | L.ValSymbol nm <- fn
  , nm `elem` [ "llvm.dbg.label"
+ , "llvm.dbg.declare"
+ , "llvm.dbg.addr"
+ , "llvm.dbg.value"
  , "llvm.lifetime.start"
  , "llvm.lifetime.start.p0i8"
  , "llvm.lifetime.end"
@@ -1940,32 +1952,30 @@ callFunctionWithCont instr tailCall_ fnTy fn args assign_f k
 
 -- | Match the arguments used by @dbg.addr@, @dbg.declare@, and @dbg.value@.
 dbgArgs ::
- (?transOpts :: TranslationOptions) =>
+ Set L.Ident {- ^ Set of usable identifiers -} ->
  [L.Typed L.Value] {- ^ debug call arguments -} ->
  LLVMGenerator s arch ret (Either String (LLVMExpr s arch, L.DILocalVariable, L.DIExpression))
-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 ?transOpts
- = case args of
+dbgArgs defSet 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))
+ let unusableIdents = Set.difference (useTypedVal val) defSet
+ in if Set.null unusableIdents then
+ do v <- transTypedValue val
+ pure (Right (v, lv, di))
+ else
+ do let msg = unwords (["dbg intrinsic def/use violation for:"] ++
+ map (show . L.ppIdent) (Set.toList unusableIdents))
+ pure (Left msg)
  _ -> 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 ->