[refinement] Add initial refinement framework.

refinement/macaw-refinement.cabal

@@ -61,8 +61,10 @@ library
 
   hs-source-dirs: src
 
-  exposed-modules:
-    Data.Macaw.Refinement
+  exposed-modules: Data.Macaw.Refinement
+
+  other-modules: Data.Macaw.Refinement.Target
+                 Data.Macaw.Refinement.UnknownTransfer
 
   default-language: Haskell2010
   ghc-options: -Wall -Wcompat

refinement/src/Data/Macaw/Refinement.hs

@@ -14,11 +14,20 @@ import           Data.Macaw.CFG.AssignRhs
 import qualified Data.Macaw.Discovery as MD
 import           Data.Macaw.Discovery.State
 import qualified Data.Macaw.Memory as MM
+import           Data.Macaw.Refinement.Target
+import           Data.Macaw.Refinement.UnknownTransfer
 import           Data.Parameterized.Classes
 
+----------------------------------------------------------------------
+-- * Discovery Entrypoints
+--
+-- These entrypoints match those of Data.Macaw.Discovery and can be
+-- used in place of the calls to Discovery because internally they
+-- will call discovery and then perform the additional refinements.
 
--- | Expand an initial discovery state by exploring from a given set of function
--- entry points.  This entry point can be used as an alternative to the same named function in Data.Macaw.Discovery.
+-- | Expand an initial discovery state by exploring from a given set
+-- of function entry points.  This entry point can be used as an
+-- alternative to the same named function in Data.Macaw.Discovery.
 cfgFromAddrsAndState :: forall arch . ShowF (ArchReg arch) =>
                         MD.DiscoveryState arch
                      -> [ArchSegmentOff arch]
@@ -58,7 +67,17 @@ cfgFromAddrs ainfo mem addrSymMap =
   cfgFromAddrsAndState (emptyDiscoveryState mem addrSymMap ainfo)
 
 
+----------------------------------------------------------------------
+-- * Refinement process
+--
+-- This is the main entrypoint to refining the discovered information.
+-- This is invoked automatically by the Discovery entrypoints, or if
+-- discovery has already yielded a 'DiscoveryState' result, that
+-- result can be refined by passing it to the 'refineDiscovery'
+-- entrypoint.
+
 -- | Refine an existing discovery state by using a symbolic backend to
 -- perform additional discovery for incomplete blocks.
 refineDiscovery :: DiscoveryState arch -> DiscoveryState arch
-refineDiscovery discState = discState
+refineDiscovery = symbolicUnkTransferRefinement
+                  . symbolicTargetRefinement

refinement/src/Data/Macaw/Refinement/Target.hs

@@ -0,0 +1,12 @@
+-- | This module uses symbolic evaluation to refine the discovered CFG
+-- and determine possible targets for transfers.
+
+module Data.Macaw.Refinement.Target
+  ( symbolicTargetRefinement
+  )
+where
+
+import           Data.Macaw.Discovery.State
+
+symbolicTargetRefinement :: DiscoveryState arch -> DiscoveryState arch
+symbolicTargetRefinement = id

refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs

@@ -0,0 +1,12 @@
+-- | This module uses symbolic evaluation to refine the discovered CFG
+-- and resolve unknown transfer classify failures.
+
+module Data.Macaw.Refinement.UnknownTransfer
+  ( symbolicUnkTransferRefinement
+  )
+where
+
+import           Data.Macaw.Discovery.State
+
+symbolicUnkTransferRefinement :: DiscoveryState arch -> DiscoveryState arch
+symbolicUnkTransferRefinement = id

refinement/tests/RefinementTests.hs

@@ -267,6 +267,14 @@ compareToExpected formName actual fn =
                         putStrLn $ "Generated actual output to: " <> outFileName
                         TTH.assertBool badMsg False
 
+----------------------------------------------------------------------
+
+-- | The ExpectedInfo is the format of information stored in the
+-- .expected files.  Ideally this would be a 'Show' output so that a
+-- 'Read' could import native data structures for a more refined
+-- comparison, but unfortunately the 'read . show == id' intent is not
+-- held for Macaw/Flexdis86, so the actual stored and compared format
+-- is generally the 'pretty' output of the structures.
 data ExpectedInfo arch = Expected
   { expBinaryName  :: String
   , expEntryPoints :: [EntryPoint arch]