mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-26 09:22:20 +03:00
cc85cfe657
This cleanup consolidates the interface to macaw symbolic into two (and a half) modules: - Data.Macaw.Symbolic for clients who just need to symbolically simulate machine code - Data.Macaw.Symbolic.Backend for clients that need to implement new architectures - Data.Macaw.Symbolic.Memory provides a reusable example implementation of machine pointer to LLVM memory model pointer mapping Most functions are now documented and are grouped by use case. There are two worked (compiling) examples in the haddocks that show how to translate Macaw into Crucible and then symbolically simulate the results (including setting up all aspects of Crucible). The examples are included in the symbolic/examples directory and can be loaded with GHCi to type check them. The Data.Macaw.Symbolic.Memory module still needs a worked example. There were very few changes to actual code as part of this overhaul, but there are a few places where complicated functions were hidden behind newtypes, as users never need to construct the values themselves (e.g., MacawArchEvalFn and MacawSymbolicArchFunctions). There was also a slight consolidation of constraint synonyms to reduce duplication. All callers will have to be updated. There is also now a README for macaw-symbolic that explains its purpose and includes pointers to the new haddocks. This commit also fixes up the (minor) breakage in the macaw-x86-symbolic implementation from the API changes.
34 lines
1.4 KiB
Haskell
34 lines
1.4 KiB
Haskell
{-# LANGUAGE FlexibleContexts #-}
|
|
{-# LANGUAGE ScopedTypeVariables #-}
|
|
{-# LANGUAGE TypeApplications #-}
|
|
import Control.Monad.ST ( stToIO )
|
|
import qualified Data.Macaw.CFG as MC
|
|
import qualified Data.Macaw.Discovery as MD
|
|
import qualified Data.Macaw.Symbolic as MS
|
|
import qualified Data.Map as Map
|
|
import Data.Proxy ( Proxy(..) )
|
|
import qualified Data.Text.Encoding as TE
|
|
import qualified Data.Text.Encoding.Error as TEE
|
|
import qualified Lang.Crucible.CFG.Core as CC
|
|
import qualified Lang.Crucible.FunctionHandle as CFH
|
|
import qualified What4.FunctionName as WFN
|
|
import qualified What4.ProgramLoc as WPL
|
|
|
|
translate :: forall arch ids
|
|
. (MS.ArchInfo arch, MC.MemWidth (MC.ArchAddrWidth arch))
|
|
=> MD.DiscoveryFunInfo arch ids
|
|
-> IO ()
|
|
translate dfi =
|
|
case MS.archVals (Proxy @arch) of
|
|
Nothing -> putStrLn "Architecture does not support symbolic reasoning"
|
|
Just MS.ArchVals { MS.archFunctions = archFns } -> do
|
|
hdlAlloc <- CFH.newHandleAllocator
|
|
let nameText = TE.decodeUtf8With TEE.lenientDecode (MD.discoveredFunName dfi)
|
|
let name = WFN.functionNameFromText nameText
|
|
let posFn addr = WPL.BinaryPos nameText (maybe 0 fromIntegral (MC.segoffAsAbsoluteAddr addr))
|
|
cfg <- stToIO $ MS.mkFunCFG archFns hdlAlloc Map.empty name posFn dfi
|
|
useCFG cfg
|
|
|
|
useCFG :: CC.SomeCFG (MS.MacawExt arch) (MS.MacawFunctionArgs arch) (MS.MacawFunctionResult arch) -> IO ()
|
|
useCFG _ = return ()
|