Merge pull request #1125 from langston-barrett/lb/llvm-cli-overrides

crucible-llvm-cli: Support for overrides; loading and calling functions

crucible-cli/src/Lang/Crucible/CLI.hs

@@ -64,8 +64,8 @@ import What4.Solver (defaultLogData, runZ3InOverride, z3Options)
 -- | Allows users to hook into the various stages of 'simulateProgram'.
 data SimulateProgramHooks ext = SimulateProgramHooks
   { setupHook ::
-      forall p sym rtp a r t st fs. (IsSymInterface sym, sym ~ ExprBuilder t st fs) =>
-        sym ->
+      forall p sym bak rtp a r t st fs. (IsSymBackend sym bak, sym ~ ExprBuilder t st fs) =>
+        bak ->
         HandleAllocator ->
         OverrideSim p sym ext rtp a r ()
     -- ^ Override action to execute before simulation. Used by the LLVM
@@ -159,7 +159,7 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                        let simSt  = InitialState simCtx gst defaultAbortHandler retType $
                                       runOverrideSim retType $
                                         do mapM_ (registerFnBinding . fst) ovrs
-                                           setupHook hooks sym ha
+                                           setupHook hooks bak ha
                                            regValue <$> callFnVal (HandleFnVal mainHdl) emptyRegMap
 
                        hPutStrLn outh "==== Begin Simulation ===="

crucible-llvm-cli/src/Lang/Crucible/LLVM/CLI.hs

@@ -10,6 +10,8 @@ module Lang.Crucible.LLVM.CLI
   ) where
 
 import Control.Monad.IO.Class (liftIO)
+import qualified Data.IntMap as IntMap
+import qualified Data.Map as Map
 
 import Data.Parameterized.NatRepr (knownNat)
 
@@ -24,9 +26,14 @@ import Lang.Crucible.Syntax.Concrete (ParserHooks)
 import Lang.Crucible.Syntax.Overrides (setupOverrides)
 
 import Lang.Crucible.LLVM (llvmExtensionImpl)
-import Lang.Crucible.LLVM.DataLayout (EndianForm(LittleEndian))
-import Lang.Crucible.LLVM.Extension (LLVM)
-import Lang.Crucible.LLVM.MemModel (HasPtrWidth, defaultMemOptions, emptyMem, mkMemVar)
+import Lang.Crucible.LLVM.DataLayout (EndianForm(LittleEndian), defaultDataLayout)
+import Lang.Crucible.LLVM.Extension (LLVM, ArchRepr(X86Repr))
+import Lang.Crucible.LLVM.MemModel (HasPtrWidth)
+import qualified Lang.Crucible.LLVM.MemModel as Mem
+import Lang.Crucible.LLVM.Intrinsics (alloc_and_register_override)
+import Lang.Crucible.LLVM.Intrinsics.Libc (llvmMallocOverride)
+import Lang.Crucible.LLVM.Translation (LLVMContext(..))
+import Lang.Crucible.LLVM.TypeContext (mkTypeContext)
 
 import Lang.Crucible.LLVM.Syntax (llvmParserHooks)
 import Lang.Crucible.LLVM.Syntax.TypeAlias (typeAliasParserHooks, x86_64LinuxTypes)
@@ -42,16 +49,34 @@ withLlvmHooks ::
   IO a
 withLlvmHooks k = do
   ha <- newHandleAllocator
-  mvar <- mkMemVar "llvm_memory" ha
+  mvar <- Mem.mkMemVar "llvm_memory" ha
   let ?ptrWidth = knownNat @64
   let ?parserHooks = llvmParserHooks (typeAliasParserHooks x86_64LinuxTypes) mvar
   let simulationHooks =
         defaultSimulateProgramHooks
-          { setupHook = \_sym _ha -> do
-              mem <- liftIO (emptyMem LittleEndian)
+          { setupHook = \bak _ha -> do
+              mem <- liftIO (Mem.emptyMem LittleEndian)
               writeGlobal mvar mem
+              let ?recordLLVMAnnotation = \_ _ _ -> pure ()
+              let (_errs, tyCtx) =
+                    mkTypeContext
+                      defaultDataLayout
+                      IntMap.empty
+                      []
+              let llvmCtx =
+                    LLVMContext
+                    { llvmArch = X86Repr ?ptrWidth
+                    , llvmPtrWidth = \kont -> kont ?ptrWidth
+                    , llvmMemVar = mvar
+                    , _llvmTypeCtx = tyCtx
+                    , llvmGlobalAliases = Map.empty
+                    , llvmFunctionAliases = Map.empty
+                    }
+              let ?lc = tyCtx
+              let ?memOpts = Mem.defaultMemOptions
+              alloc_and_register_override bak llvmCtx llvmMallocOverride []
           , setupOverridesHook = setupOverrides
           }
   let ext _ = let ?recordLLVMAnnotation = \_ _ _ -> pure ()
-              in llvmExtensionImpl defaultMemOptions
+              in llvmExtensionImpl Mem.defaultMemOptions
   k ext simulationHooks 

crucible-llvm-cli/test-data/ptr.cbl

@@ -21,4 +21,12 @@
     (assert! (equal? vblk0 vblk) "stored block numbers equal")
     (assert! (equal? voff0 voff) "stored offsets equal")
 
+    (let g (resolve-global "malloc"))
+    (let gblk (ptr-block 64 g))
+    (assert! (not (equal? gblk 0)) "malloc block number nonzero")
+    (let h (load-handle (Ptr 64) ((Ptr 64)) g))
+    (let m (funcall h p0))
+    (let mblk (ptr-block 64 m))
+    (assert! (not (equal? mblk 0)) "malloc'd block number nonzero")
+
     (return ())))

crucible-llvm-syntax/README.md

@@ -32,7 +32,13 @@ If the numeral `w` is the width of a pointer and `n` is an arbitrary numeral,
 - `ptr-ite : Bool -> Ptr n -> Ptr n -> Ptr n`: if-then-else for pointers
 - `alloca : Alignment -> Bitvector w -> Ptr w`: allocate space on the stack
 - `load : Alignment -> LLVMType -> Ptr w -> T`: load a value from memory, where the type `T` is determined by the `LLVMType`
+- `load-handle : Type -> [Type] -> Ptr w -> T`: load a function handle from memory, where the type `T` is determined by the given return and argument types
 - `store : Alignment -> LLVMType -> Ptr w -> T -> Unit`: store a value to memory, where the type `T` is determined by the `LLVMType`
+- `resolve-global : String -> Ptr w`: get the address of a global variable
+
+`Type` signifies a Crucible type, rather than an LLVM type. This means there
+are no C- or LLVM-like `Type`s such as `i8*` or `size_t`, but rather the base
+Crucible types as defined by `crucible-syntax`, and `(Ptr n)`.
 
 ## Further extensions
 

crucible-llvm-syntax/crucible-llvm-syntax.cabal

@@ -97,6 +97,7 @@ library
     crucible >= 0.1,
     crucible-llvm,
     crucible-syntax,
+    llvm-pretty,
     mtl,
     parameterized-utils >= 0.1.7,
     prettyprinter,

crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs

@@ -19,9 +19,13 @@ import Control.Monad.IO.Class (MonadIO(..))
 import Control.Monad.State.Strict (MonadState(..))
 import Control.Monad.Writer.Strict (MonadWriter(..))
 import Data.Functor ((<&>))
+import qualified Data.Text as Text
 
 import Prettyprinter (pretty)
 
+-- Optimally, this library wouldn't depend on llvm-pretty...
+import Text.LLVM.AST as L (Symbol(Symbol))
+
 import Data.Parameterized.Context qualified as Ctx
 import Data.Parameterized.Some (Some(..))
 
@@ -169,6 +173,25 @@ llvmAtomParser mvar =
               let stmt = Ext.LLVM_Load mvar ptr tyRep storTy align
               Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
 
+      Atom.AtomName "load-handle" -> Parse.describe "LLVM load-handle arguments" $ do
+        loc <- Parse.position
+        (Some ret, (Some args, assign)) <-
+          Parse.cons
+            Parse.isType
+            (Parse.cons
+              (Parse.someAssign "list of argument types" Parse.isType)
+              (Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr ?ptrWidth)))
+        let (Ctx.Empty, ptr) = Ctx.decompose assign
+        let stmt = Ext.LLVM_LoadHandle mvar Nothing ptr args ret
+        Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
+
+      Atom.AtomName "resolve-global" -> Parse.describe "LLVM resolve-global arguments" $ do
+        loc <- Parse.position
+        let parseSymb = Mem.GlobalSymbol . L.Symbol . Text.unpack <$> Parse.string
+        (symb, ()) <- Parse.cons parseSymb Parse.emptyList
+        let stmt = Ext.LLVM_ResolveGlobal ?ptrWidth mvar symb
+        Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
+
       Atom.AtomName "store" -> Parse.describe "LLVM store arguments" $ do
         loc <- Parse.position
         Parse.depCons parseAlign $ \align ->

crucible-llvm-syntax/test-data/ptr.cbl

@@ -21,4 +21,7 @@
     (assert! (equal? vblk0 vblk) "stored block numbers equal")
     (assert! (equal? voff0 voff) "stored offsets equal")
 
+    (let g (resolve-global "malloc"))
+    (let h (load-handle (Ptr 64) ((Ptr 64)) g))
+
     (return p)))

crucible-llvm-syntax/test-data/ptr.out.good

@@ -19,6 +19,8 @@
       (let voff (ptr-offset 8 v))
       (assert! (equal? vblk0 vblk) "stored block numbers equal")
       (assert! (equal? voff0 voff) "stored offsets equal")
+      (let g (resolve-global "malloc"))
+      (let h (load-handle (Ptr 64) ((Ptr 64)) g))
       (return p)))
 
 test-ptr
@@ -77,6 +79,10 @@ test-ptr
   $22 = stringLit("stored offsets equal")
   % 22:5
   assert($21, $22)
-  % 24:5
+  % 24:12
+  $23 = resolveGlobal crucible-llvm-syntax-test-memory "malloc"
+  % 25:12
+  $24 = loadFunctionHandle crucible-llvm-syntax-test-memory $23 as Nothing
+  % 27:5
   return $4
   % no postdom

crucible-llvm/crucible-llvm.cabal

@@ -67,6 +67,8 @@ library
     Lang.Crucible.LLVM.Extension
     Lang.Crucible.LLVM.Globals
     Lang.Crucible.LLVM.Intrinsics
+    Lang.Crucible.LLVM.Intrinsics.Libc
+    Lang.Crucible.LLVM.Intrinsics.LLVM
     Lang.Crucible.LLVM.MalformedLLVMModule
     Lang.Crucible.LLVM.MemModel
     Lang.Crucible.LLVM.MemModel.CallStack
@@ -90,9 +92,7 @@ library
     Lang.Crucible.LLVM.Extension.Arch
     Lang.Crucible.LLVM.Extension.Syntax
     Lang.Crucible.LLVM.Intrinsics.Common
-    Lang.Crucible.LLVM.Intrinsics.Libc
     Lang.Crucible.LLVM.Intrinsics.Libcxx
-    Lang.Crucible.LLVM.Intrinsics.LLVM
     Lang.Crucible.LLVM.Intrinsics.Options
     Lang.Crucible.LLVM.MemModel.Common
     Lang.Crucible.LLVM.MemModel.Options

crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs

@@ -58,7 +58,7 @@ data MemoryOp sym w
        (Maybe String, LLVMPtr sym w) -- src
        (SymBV sym wlen) -- length
        (Mem sym)
-  | MemLoadHandleOp L.Type (Maybe String) (LLVMPtr sym w) (Mem sym)
+  | MemLoadHandleOp (Maybe L.Type) (Maybe String) (LLVMPtr sym w) (Mem sym)
   | forall wlen. (1 <= wlen) => MemInvalidateOp
        Text (Maybe String) (LLVMPtr sym w) (SymBV sym wlen) (Mem sym)
 
@@ -157,7 +157,11 @@ ppMemoryOp (MemCopyOp (gsym_dest, dest) (gsym_src, src) len mem) =
        ]
 
 ppMemoryOp (MemLoadHandleOp sig gsym ptr mem) =
-  vsep [ "Attempting to load callable function with type:" <+> viaShow (L.ppType sig)
+  vsep [ case sig of
+           Just s ->
+             hsep ["Attempting to load callable function with type:", viaShow (L.ppType s)]
+           Nothing ->
+             hsep ["Attempting to load callable function:"]
        , indent 2 (hsep ([ "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
        , "In memory state:"
        , indent 2 (ppMem mem)

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

@@ -171,7 +171,7 @@ data LLVMStmt (f :: CrucibleType -> Type) :: CrucibleType -> Type where
   LLVM_LoadHandle ::
      HasPtrWidth wptr =>
      !(GlobalVar Mem)            {- Memory global variable -} ->
-     !L.Type                     {- expected LLVM type of the function -} ->
+     !(Maybe L.Type)             {- expected LLVM type of the function (used only for pretty-printing) -} ->
      !(f (LLVMPointerType wptr)) {- Pointer to load from -} ->
      !(CtxRepr args)             {- Expected argument types of the function -} ->
      !(TypeRepr ret)             {- Expected return type of the function -} ->

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

@@ -36,6 +36,7 @@ module Lang.Crucible.LLVM.Globals
   , populateGlobals
   , populateAllGlobals
   , populateConstGlobals
+  , registerFunPtr
 
   , GlobalInitializerMap
   , makeGlobalMap
@@ -233,8 +234,7 @@ allocLLVMFunPtr ::
   Either L.Declare L.Define ->
   IO (MemImpl sym)
 allocLLVMFunPtr bak llvm_ctx mem decl =
-  do let sym = backendGetSym bak
-     let (symbol, displayString) =
+  do let (symbol, displayString) =
            case decl of
              Left d ->
                let s@(L.Symbol nm) = L.decName d
@@ -244,9 +244,27 @@ allocLLVMFunPtr bak llvm_ctx mem decl =
                 in ( s, "[defined function ] " ++ nm)
      let funAliases = llvmFunctionAliases llvm_ctx
      let aliases = map L.aliasName $ maybe [] Set.toList $ Map.lookup symbol funAliases
-     z <- bvLit sym ?ptrWidth (BV.zero ?ptrWidth)
-     (ptr, mem') <- doMalloc bak G.GlobalAlloc G.Immutable displayString mem z noAlignment
-     return $ registerGlobal mem' (symbol:aliases) ptr
+     (_ptr, mem') <- registerFunPtr bak mem displayString symbol aliases
+     return mem'
+
+-- | Create a global allocation assocated with a function
+registerFunPtr ::
+  ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
+  , ?memOpts :: MemOptions ) =>
+  bak ->
+  MemImpl sym ->
+  -- | Display name
+  String ->
+  -- | Function name
+  L.Symbol ->
+  -- | Aliases
+  [L.Symbol] ->
+  IO (LLVMPtr sym wptr, MemImpl sym)
+registerFunPtr bak mem displayName nm aliases = do
+  let sym = backendGetSym bak
+  z <- bvLit sym ?ptrWidth (BV.zero ?ptrWidth)
+  (ptr, mem') <- doMalloc bak G.GlobalAlloc G.Immutable displayName mem z noAlignment
+  return $ (ptr, registerGlobal mem' (nm:aliases) ptr)
 
 ------------------------------------------------------------------------
 -- ** populateGlobals