From 16dfcaab0d0eace9025223d51bd5a0fe19bf77ae Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Thu, 24 Jan 2019 14:48:55 -0800 Subject: [PATCH] [refinement] Add initial refinement framework. --- refinement/macaw-refinement.cabal | 6 +++-- refinement/src/Data/Macaw/Refinement.hs | 25 ++++++++++++++++--- .../src/Data/Macaw/Refinement/Target.hs | 12 +++++++++ .../Data/Macaw/Refinement/UnknownTransfer.hs | 12 +++++++++ refinement/tests/RefinementTests.hs | 8 ++++++ 5 files changed, 58 insertions(+), 5 deletions(-) create mode 100644 refinement/src/Data/Macaw/Refinement/Target.hs create mode 100644 refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs diff --git a/refinement/macaw-refinement.cabal b/refinement/macaw-refinement.cabal index c522a1d9..0e578255 100644 --- a/refinement/macaw-refinement.cabal +++ b/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 diff --git a/refinement/src/Data/Macaw/Refinement.hs b/refinement/src/Data/Macaw/Refinement.hs index e646fe82..026f21b5 100644 --- a/refinement/src/Data/Macaw/Refinement.hs +++ b/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 diff --git a/refinement/src/Data/Macaw/Refinement/Target.hs b/refinement/src/Data/Macaw/Refinement/Target.hs new file mode 100644 index 00000000..816e382c --- /dev/null +++ b/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 diff --git a/refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs b/refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs new file mode 100644 index 00000000..d7640252 --- /dev/null +++ b/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 diff --git a/refinement/tests/RefinementTests.hs b/refinement/tests/RefinementTests.hs index 10d4bd28..a6a00ddf 100644 --- a/refinement/tests/RefinementTests.hs +++ b/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]