From 1b359da7399b04bc0b34656df2757af81a1b6b5f Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 23 Jan 2018 15:28:20 -0800 Subject: [PATCH 1/3] Define a pretty printer, and appT --- x86_symbolic/src/Data/Macaw/X86/Symbolic.hs | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) diff --git a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs index c186511b..20113d90 100644 --- a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs +++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs @@ -18,9 +18,11 @@ module Data.Macaw.X86.Symbolic import Data.Parameterized.Context as Ctx import Data.Parameterized.TraversableFC import GHC.TypeLits +import Data.Functor.Identity(Identity(..)) import qualified Data.Macaw.CFG as M import Data.Macaw.Symbolic +import Data.Macaw.Symbolic.PersistentState(typeToCrucible) import qualified Data.Macaw.Types as M import qualified Data.Macaw.X86 as M import qualified Data.Macaw.X86.X86Reg as M @@ -103,15 +105,13 @@ newtype AtomWrapper (f :: C.CrucibleType -> *) (tp :: M.Type) liftAtomMap :: (forall s. f s -> g s) -> AtomWrapper f t -> AtomWrapper g t liftAtomMap f (AtomWrapper x) = AtomWrapper (f x) -liftAtomFold :: (forall s. f s -> m) -> AtomWrapper f t -> m -liftAtomFold f (AtomWrapper x) = f x - liftAtomTrav :: Applicative m => (forall s. f s -> m (g s)) -> (AtomWrapper f t -> m (AtomWrapper g t)) liftAtomTrav f (AtomWrapper x) = AtomWrapper <$> f x - +liftAtomIn :: (forall s. f s -> a) -> AtomWrapper f t -> a +liftAtomIn f (AtomWrapper x) = f x -- | We currently make a type like this, we could instead a generic @@ -123,23 +123,19 @@ data X86StmtExtension (f :: C.CrucibleType -> *) (ctp :: C.CrucibleType) where X86StmtExtension f (ToCrucibleType t) -appT :: X86StmtExtension f t -> C.TypeRepr t -appT (X86PrimFn x) = - case M.typeRepr x of - M.BoolTypeRepr -> C.BoolRepr - instance C.PrettyApp X86StmtExtension where + ppApp ppSub (X86PrimFn x) = d + where Identity d = M.ppArchFn (Identity . liftAtomIn ppSub) x instance C.TypeApp X86StmtExtension where - appType = appT - + appType (X86PrimFn x) = typeToCrucible (M.typeRepr x) instance FunctorFC X86StmtExtension where fmapFC f (X86PrimFn x) = X86PrimFn (fmapFC (liftAtomMap f) x) instance FoldableFC X86StmtExtension where - foldMapFC f (X86PrimFn x) = foldMapFC (liftAtomFold f) x + foldMapFC f (X86PrimFn x) = foldMapFC (liftAtomIn f) x instance TraversableFC X86StmtExtension where traverseFC f (X86PrimFn x) = X86PrimFn <$> traverseFC (liftAtomTrav f) x From 04408c595a4983972c01f261c42950d61a1b0a9b Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 23 Jan 2018 16:01:50 -0800 Subject: [PATCH 2/3] Move semantics function to a separate module. This is yet to be defined. --- x86_symbolic/macaw-x86-symbolic.cabal | 1 + x86_symbolic/src/Data/Macaw/X86/Semantics.hs | 46 ++++++++++++++++++++ x86_symbolic/src/Data/Macaw/X86/Symbolic.hs | 21 +++------ 3 files changed, 53 insertions(+), 15 deletions(-) create mode 100644 x86_symbolic/src/Data/Macaw/X86/Semantics.hs diff --git a/x86_symbolic/macaw-x86-symbolic.cabal b/x86_symbolic/macaw-x86-symbolic.cabal index 027fcd2f..94c424b7 100644 --- a/x86_symbolic/macaw-x86-symbolic.cabal +++ b/x86_symbolic/macaw-x86-symbolic.cabal @@ -20,6 +20,7 @@ library exposed-modules: Data.Macaw.X86.Symbolic + Data.Macaw.X86.Semantics ghc-options: -Wall ghc-prof-options: -O2 -fprof-auto-top diff --git a/x86_symbolic/src/Data/Macaw/X86/Semantics.hs b/x86_symbolic/src/Data/Macaw/X86/Semantics.hs new file mode 100644 index 00000000..0becbcd9 --- /dev/null +++ b/x86_symbolic/src/Data/Macaw/X86/Semantics.hs @@ -0,0 +1,46 @@ +{-# Language GADTs #-} +{-# Language RankNTypes #-} +{-# Language KindSignatures #-} +{-# Language DataKinds #-} +module Data.Macaw.X86.Semantics where + +import qualified Lang.Crucible.Simulator.ExecutionTree as C +import qualified Lang.Crucible.Simulator.RegMap as C +import qualified Lang.Crucible.Solver.Interface as C +import qualified Lang.Crucible.Types as C + +import qualified Data.Macaw.Types as M +import Data.Macaw.Symbolic.CrucGen(MacawExt) +import Data.Macaw.Symbolic +import qualified Data.Macaw.X86 as M + + +type S sym rtp bs r ctx = + C.CrucibleState MacawSimulatorState sym (MacawExt M.X86_64) rtp bs r ctx + +semantics :: + (C.IsSymInterface sym, ToCrucibleType mt ~ t) => + M.X86PrimFn (AtomWrapper (C.RegEntry sym)) mt -> + S sym rtp bs r ctx -> IO (C.RegValue sym t, S sym rtp bs r ctx) +semantics _x _s = undefined + + + +-------------------------------------------------------------------------------- + +newtype AtomWrapper (f :: C.CrucibleType -> *) (tp :: M.Type) + = AtomWrapper (f (ToCrucibleType tp)) + +liftAtomMap :: (forall s. f s -> g s) -> AtomWrapper f t -> AtomWrapper g t +liftAtomMap f (AtomWrapper x) = AtomWrapper (f x) + +liftAtomTrav :: + Applicative m => + (forall s. f s -> m (g s)) -> (AtomWrapper f t -> m (AtomWrapper g t)) +liftAtomTrav f (AtomWrapper x) = AtomWrapper <$> f x + +liftAtomIn :: (forall s. f s -> a) -> AtomWrapper f t -> a +liftAtomIn f (AtomWrapper x) = f x + + + diff --git a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs index 20113d90..5755ddb3 100644 --- a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs +++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs @@ -26,6 +26,7 @@ import Data.Macaw.Symbolic.PersistentState(typeToCrucible) import qualified Data.Macaw.Types as M import qualified Data.Macaw.X86 as M import qualified Data.Macaw.X86.X86Reg as M +import Data.Macaw.X86.Semantics import qualified Flexdis86.Register as F import qualified Lang.Crucible.CFG.Extension as C @@ -34,6 +35,9 @@ import qualified Lang.Crucible.Types as C import qualified Lang.Crucible.Solver.Symbol as C import qualified Lang.Crucible.Solver.Interface as C + + + ------------------------------------------------------------------------ -- Utilities for generating a type-level context with repeated elements. @@ -99,20 +103,6 @@ x86RegAssignment = ------------------------------------------------------------------------ -- Other X86 specific -newtype AtomWrapper (f :: C.CrucibleType -> *) (tp :: M.Type) - = AtomWrapper (f (ToCrucibleType tp)) - -liftAtomMap :: (forall s. f s -> g s) -> AtomWrapper f t -> AtomWrapper g t -liftAtomMap f (AtomWrapper x) = AtomWrapper (f x) - -liftAtomTrav :: - Applicative m => - (forall s. f s -> m (g s)) -> (AtomWrapper f t -> m (AtomWrapper g t)) -liftAtomTrav f (AtomWrapper x) = AtomWrapper <$> f x - -liftAtomIn :: (forall s. f s -> a) -> AtomWrapper f t -> a -liftAtomIn f (AtomWrapper x) = f x - -- | We currently make a type like this, we could instead a generic -- X86PrimFn function @@ -180,4 +170,5 @@ x86_64MacawSymbolicFns = -- | X86_64 specific function for evaluating a Macaw X86_64 program in Crucible. x86_64MacawEvalFn :: C.IsSymInterface sym => MacawArchEvalFn sym M.X86_64 -x86_64MacawEvalFn = undefined +x86_64MacawEvalFn (X86PrimFn x) s = semantics x s + From da4f1b873eb3a935e07c60e18b454003effc5f8e Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 23 Jan 2018 16:02:38 -0800 Subject: [PATCH 3/3] Needs only Functor --- x86_symbolic/src/Data/Macaw/X86/Semantics.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/x86_symbolic/src/Data/Macaw/X86/Semantics.hs b/x86_symbolic/src/Data/Macaw/X86/Semantics.hs index 0becbcd9..65523c53 100644 --- a/x86_symbolic/src/Data/Macaw/X86/Semantics.hs +++ b/x86_symbolic/src/Data/Macaw/X86/Semantics.hs @@ -35,7 +35,7 @@ liftAtomMap :: (forall s. f s -> g s) -> AtomWrapper f t -> AtomWrapper g t liftAtomMap f (AtomWrapper x) = AtomWrapper (f x) liftAtomTrav :: - Applicative m => + Functor m => (forall s. f s -> m (g s)) -> (AtomWrapper f t -> m (AtomWrapper g t)) liftAtomTrav f (AtomWrapper x) = AtomWrapper <$> f x