Merge branch 'master' of https://github.com/GaloisInc/crucible

GaloisInc · Jul 25, 2017 · e87e00a · e87e00a
2 parents 909ad57 + 866a5c7
commit e87e00a
Show file tree

Hide file tree

Showing 4 changed files with 54 additions and 1 deletion.
diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs
@@ -100,8 +100,9 @@ register_llvm_overrides = do
  register_llvm_override llvmObjectsizeOverride_32
  register_llvm_override llvmObjectsizeOverride_64
 
- -- C standard libraray functions
+ -- C standard library functions
  register_llvm_override llvmMemcpyOverride
+ register_llvm_override llvmMemcpyChkOverride
  register_llvm_override llvmMemmoveOverride
  register_llvm_override llvmMemsetOverride
  register_llvm_override llvmMallocOverride
@@ -406,6 +407,37 @@ llvmMemcpyOverride =
  return $ regValue $ args^._1 -- return first argument
  )
 
+llvmMemcpyChkOverride
+ :: IsSymInterface sym
+ => LLVMOverride p sym (EmptyCtx ::> LLVMPointerType
+ ::> LLVMPointerType
+ ::> BVType PtrWidth
+ ::> BVType PtrWidth)
+ LLVMPointerType
+llvmMemcpyChkOverride =
+ let nm = "__memcpy_chk" in
+ ( L.Declare
+ { L.decRetType = L.PtrTo $ L.PrimType L.Void
+ , L.decName = L.Symbol nm
+ , L.decArgs = [ L.PtrTo $ L.PrimType L.Void
+ , L.PtrTo $ L.PrimType L.Void
+ , L.PrimType $ L.Integer (fromIntegral $ natValue ptrWidth)
+ , L.PrimType $ L.Integer (fromIntegral $ natValue ptrWidth)
+ ]
+ , L.decVarArgs = False
+ , L.decAttrs = []
+ }
+ , \memOps -> mkOverride (functionNameFromText (Text.pack nm)) $ do
+ sym <- getSymInterface
+ (RegMap args) <- getOverrideArgs
+ let args' = Ctx.empty Ctx.%> (args^._1) Ctx.%> (args^._2) Ctx.%> (args^._3)
+ align <- liftIO $ RegEntry knownRepr <$> bvLit sym knownNat 0
+ volatile <- liftIO $ RegEntry knownRepr <$> bvLit sym knownNat 0
+ Ctx.uncurryAssignment (callMemcpy sym memOps)
+ (args' Ctx.%> align Ctx.%> volatile)
+ return $ regValue $ args^._1 -- return first argument
+ )
+
 llvmMemmoveOverride
  :: IsSymInterface sym
  => LLVMOverride p sym (EmptyCtx ::> LLVMPointerType

diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Translation.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Translation.hs
@@ -2067,6 +2067,13 @@ findFile (L.ValMdRef x) =
  case TyCtx.lookupMetadata y of
  Just (L.ValMdNode [Just (L.ValMdString fname), Just (L.ValMdString _fpath)]) -> fname
  _ -> ""
+ Just (L.ValMdDebugInfo di) ->
+ case di of
+ L.DebugInfoLexicalBlock (L.dilbFile -> Just (L.ValMdDebugInfo (L.DebugInfoFile dif))) ->
+ L.difFilename dif
+ L.DebugInfoSubprogram (L.dispFile -> Just (L.ValMdDebugInfo (L.DebugInfoFile dif))) ->
+ L.difFilename dif
+ _ -> ""
  _ -> ""
 findFile _ = ""
 

diff --git a/crucible/src/Lang/Crucible/Solver/Interface.hs b/crucible/src/Lang/Crucible/Solver/Interface.hs
@@ -73,6 +73,7 @@ module Lang.Crucible.Solver.Interface
  , IsExprBuilder(..)
  -- ** IsSymInterface
  , BoundVar
+ , IsSymFn(..)
  , IsSymInterface(..)
  -- * Bound variables
  , SymEncoder(..)
@@ -1694,10 +1695,18 @@ cplxLogBase base sym x = do
 -- 'IsSymInterface'.
 type family SymFn sym :: Ctx BaseType -> BaseType -> *
 
+class IsSymFn fn where
+ -- | Get the argument types of a function.
+ fnArgTypes :: fn args ret -> Ctx.Assignment BaseTypeRepr args
+
+ -- | Get the return type of a function.
+ fnReturnType :: fn args ret -> BaseTypeRepr ret
+
 -- | This extends the interface for building expressions with operations
 -- for creating new constants and functions.
 class ( IsBoolSolver sym
  , IsExprBuilder sym
+ , IsSymFn (SymFn sym)
  , OrdF (SymExpr sym)
  ) => IsSymInterface sym where
 

diff --git a/crucible/src/Lang/Crucible/Solver/SimpleBuilder.hs b/crucible/src/Lang/Crucible/Solver/SimpleBuilder.hs
@@ -846,6 +846,11 @@ testSimpleSymFnEq :: SimpleSymFn t a1 r1
  -> Maybe ((a1::>r1) :~: (a2::>r2))
 testSimpleSymFnEq f g = testEquality (symFnId f) (symFnId g)
 
+
+instance IsSymFn (SimpleSymFn t) where
+ fnArgTypes = symFnArgTypes
+ fnReturnType = symFnReturnType
+
 ------------------------------------------------------------------------
 -- asConjunction