Dbg def use

crucible-llvm/crucible-llvm.cabal

@@ -101,6 +101,7 @@ library
  Lang.Crucible.LLVM.MemModel.Options
  Lang.Crucible.LLVM.MemModel.Type
  Lang.Crucible.LLVM.MemModel.Value
+ Lang.Crucible.LLVM.Translation.BlockInfo
  Lang.Crucible.LLVM.Translation.Constant
  Lang.Crucible.LLVM.Translation.Expr
  Lang.Crucible.LLVM.Translation.Instruction

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
 
@@ -39,7 +41,7 @@ import Data.Maybe (fromMaybe)
 
 import qualified Text.LLVM.AST as L
 
-import Lang.Crucible.LLVM.Translation.Instruction (callFunction)
+import Lang.Crucible.LLVM.Translation.Instruction (callOrdinaryFunction)
 import Lang.Crucible.LLVM.Translation.Monad (LLVMGenerator, LLVMState(..))
 
 -- Generating CFGs
@@ -140,7 +142,7 @@ callCtors select mod_ = do
 
  ctors <- either err (pure . filter select) (globalCtors mod_)
  forM_ ctors $ \ctor ->
- callFunction Nothing False ty (L.ValSymbol (ctorFunction ctor)) [] (const (pure ()))
+ callOrdinaryFunction Nothing False ty (L.ValSymbol (ctorFunction ctor)) [] (const (pure ()))
  return (App EmptyApp)
 
 -- | Call each function in @llvm.global_ctors@ in order of decreasing priority
@@ -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

@@ -1,7 +1,7 @@
 -- |
 -- Module : Lang.Crucible.LLVM.Translation
 -- Description : Translation of LLVM AST into Crucible control-flow graph
--- Copyright : (c) Galois, Inc 2014-2018
+-- Copyright : (c) Galois, Inc 2014-2021
 -- License : BSD3
 -- Maintainer : Rob Dockins <[email protected]>
 -- Stability : provisional
@@ -52,8 +52,7 @@
 --
 -- A (probably) partial list of things we intend to support, but do not yet:
 --
--- * Checking of alignment constraints on load, store, alloca, etc.
--- * Various vector instructions. This includes a variety of instructions
+-- * Various vector instructions. This includes a variety of instructions
 -- that LLVM allows to take vector arguments, but are currently only
 -- defined on scalar (nonvector) arguments. (Progress has been made on
 -- this, but may not yet be complete).
@@ -81,6 +80,7 @@ module Lang.Crucible.LLVM.Translation
  , LLVMContext(..)
  , llvmTypeCtx
  , translateModule
+ , LLVMTranslationWarning(..)
 
  , module Lang.Crucible.LLVM.Translation.Constant
  , module Lang.Crucible.LLVM.Translation.Options
@@ -89,13 +89,18 @@ 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 Prettyprinter (pretty)
 
 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 +197,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
@@ -312,12 +322,12 @@ findFile _ = Nothing
 defineLLVMBlock
  :: (?transOpts :: TranslationOptions)
  => TypeRepr ret
- -> Map L.BlockLabel (LLVMBlockInfo s)
+ -> LLVMBlockInfoMap s
  -> L.BasicBlock
  -> 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 +361,31 @@ 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 =
+ malformedLLVMModule ("Invalid SSA form for function: " <> pretty nm)
+ ([ "The following LLVM virtual registers have at least one use site that"
+ , "is not dominated by the corresponding definition:" ] ++
+ [ " " <> pretty (show (L.ppIdent i)) | 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 +394,10 @@ transDefine :: forall arch wptr.
  (HasPtrWidth wptr, wptr ~ ArchWidth arch, ?transOpts :: TranslationOptions)
  => HandleAllocator
  -> LLVMContext arch
+ -> IORef [LLVMTranslationWarning]
  -> 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 +407,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 +419,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, [LLVMTranslationWarning])
 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 +444,5 @@ translateModule halloc mvar m = do
  , _transContext = ctx'
  , modTransNonce = nonce
  }))
+ warns <- reverse <$> readIORef warnRef
+ return (mtrans, warns)