Merge branch 'master' into refinement

base/README.rst

@@ -9,43 +9,32 @@ The most important user-facing abstractions are:
 
 * The ``Memory`` type, defined in ``Data.Macaw.Memory``, which provides an abstract interface to an address space containing both code and data.
 * The ``memoryForElfSegments`` function is a useful helper to produce a ``Memory`` from an ELF file.
-* The ``cfgFromAddrs`` function, defined in ``Data.Macaw.Discovery``, which performs code discovery on a ``Memory`` given some initial parameters (semantics to use via ``ArchitectureInfo`` and some entry points.
+* The ``cfgFromAddrs`` function, defined in ``Data.Macaw.Discovery``, which performs code discovery on a ``Memory`` given some initial parameters (semantics to use via ``ArchitectureInfo`` and some entry points).
 * The ``DiscoveryInfo`` type, which is the result of ``cfgFromAddrs``; it contains a collection of ``DiscoveryFunInfo`` records, each of which represents a discovered function.  Every basic block is assigned to at least one function.
 
 Architecture-specific code goes into separate libraries.  X86-specific code is in the macaw-x86 repo.
 
-An abbreviated example of using macaw on an ELF file looks like::
+An abbreviated example of using macaw on an X86_64 ELF file looks like::
 
   import qualified Data.Map as M
-
   import qualified Data.ElfEdit as E
   import qualified Data.Parameterized.Some as PU
-  import qualified Data.Macaw.Architecture.Info as AI
+  import qualified Data.Macaw.X86 as MX86
-  import qualified Data.Macaw.Memory as MM
+  import qualified Data.Macaw.Memory.ElfLoader as ML
-  import qualified Data.Macaw.Memory.ElfLoader as MM
   import qualified Data.Macaw.Discovery as MD
-  import qualified Data.Macaw.Discovery.Info as MD
 
-  discoverCode :: E.Elf Word64 -> AI.ArchitectureInfo X86_64 -> (forall ids . MD.DiscoveryInfo X86_64 ids -> a) -> a
+  discoverCode :: E.Elf Word64 -> (forall ids . MD.DiscoveryInfo X86_64 ids -> a) -> a
-  discoverCode elf archInfo k =
+  discoverCode elf k =
-    withMemory MM.Addr64 elf $ \mem ->
+    case ML.resolveElfContents ML.defaultLoadOptions elf of
-      let Just entryPoint = MM.absoluteAddrSegment mem (fromIntegral (E.elfEntry elf))
+      Left e -> error (show e)
-      in case MD.cfgFromAddrs archInfo mem M.empty [entryPoint] [] of
+      Right (_, _, Nothing, _) -> error "Unable to determine entry point"
+      Right (warn, mem, Just entryPoint, _) -> do
+        mapM_ print warn
+        case MD.cfgFromAddrs MX86.x86_64_linux_info mem M.empty [entryPoint] [] of
         PU.Some di -> k di
 
-  withMemory :: forall w m a
-              . (MM.MemWidth w, Integral (E.ElfWordType w))
-             => MM.AddrWidthRepr w
-             -> E.Elf (E.ElfWordType w)
-             -> (MM.Memory w -> m a)
-             -> m a
-  withMemory relaWidth e k =
-    case MM.memoryForElfSegments relaWidth e of
-      Left err -> error (show err)
-      Right (_sim, mem) -> k mem
 
-
+In the callback ``k``, the ``DiscoveryInfo`` can be analyzed as desired.
-In the callback, the ``DiscoveryInfo`` can be analyzed as desired.
 
 Implementing support for an architecture is more involved and requires implementing an ``ArchitectureInfo``, which is defined in ``Data.Macaw.Architecture.Info``.  This structure contains architecture-specific information like:
 

base/src/Data/Macaw/Memory/ElfLoader.hs

@@ -1093,7 +1093,7 @@ symtabSymbolTable e =
 
 -- | Load allocated Elf sections into memory.
 --
--- Normally, Elf uses segments for loading, but the segment
+-- Normally, Elf uses segments for loading, but the section
 -- information tends to be more precise.
 memoryForElfSections :: forall w
                      .  Elf w

symbolic/src/Data/Macaw/Symbolic.hs

@@ -348,7 +348,7 @@ mkParsedBlockCFG :: forall s arch ids
 mkParsedBlockCFG archFns halloc memBaseVarMap posFn b =
   toCoreCFG archFns <$> mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b
 
--- | This create a registerized Crucible CFG from a Macaw
+-- | This creates a registerized Crucible CFG from a Macaw
 -- `DiscoveryFunInfo` value.
 --
 -- Useful as an alternative to 'mkFunCFG' if post-processing
@@ -423,7 +423,7 @@ mkFunCFG :: forall s arch ids
          -> (M.ArchSegmentOff arch -> C.Position)
             -- ^ Function that maps function address to Crucible position
          -> M.DiscoveryFunInfo arch ids
-         -- ^ List of blocks for this region.
+            -- ^ List of blocks for this region.
          -> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
 mkFunCFG archFns halloc memBaseVarMap nm posFn fn =
   toCoreCFG archFns <$> mkFunRegCFG archFns halloc memBaseVarMap nm posFn fn

symbolic/src/Data/Macaw/Symbolic/CrucGen.hs

@@ -52,6 +52,7 @@ module Data.Macaw.Symbolic.CrucGen
   , valueToCrucible
   , evalArchStmt
   , MemSegmentMap
+  , MacawCrucibleValue(..)
     -- * Additional exports
   , runCrucGen
   , setMachineRegs