Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc

macaw-ppc/macaw-ppc.cabal

@@ -16,9 +16,13 @@ extra-source-files:  ChangeLog.md
 cabal-version:       >=1.10
 
 library
-  exposed-modules:     Data.Macaw.PPC,
+  exposed-modules:     Data.Macaw.PPC
-                       Data.Macaw.PPC.ArchTypes,
+                       Data.Macaw.PPC.ArchTypes
+                       Data.Macaw.PPC.Disassemble
+                       Data.Macaw.PPC.Eval
+                       Data.Macaw.PPC.Identify
                        Data.Macaw.PPC.PPCReg
+                       Data.Macaw.PPC.Rewrite
   -- other-modules:       
   -- other-extensions:    
   build-depends:       base >=4.9 && <5,

macaw-ppc/src/Data/Macaw/PPC.hs

@@ -1,8 +1,10 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
+
 module Data.Macaw.PPC (
   ppc_linux_info,
   ppc32_linux_info,
@@ -25,6 +27,7 @@ import Data.Macaw.CFG.Core
 import qualified Data.Macaw.CFG.DemandSet as MDS
 import Data.Macaw.CFG.Rewriter
 import qualified Data.Macaw.Memory as MM
+import Data.Macaw.Types
 import qualified Data.Parameterized.Map as MapF
 import qualified Data.Parameterized.Nonce as NC
 import qualified Dismantle.PPC as D
@@ -33,8 +36,21 @@ import qualified SemMC.Architecture.PPC32 as PPC32
 import qualified SemMC.Architecture.PPC64 as PPC64
 
 import Data.Macaw.PPC.ArchTypes
+import Data.Macaw.PPC.Disassemble ( disassembleFn )
+import Data.Macaw.PPC.Eval ( mkInitialAbsState,
+                             absEvalArchFn,
+                             absEvalArchStmt,
+                             postCallAbsState,
+                             preserveRegAcrossSyscall
+                           )
+import Data.Macaw.PPC.Identify ( identifyCall,
+                                 identifyReturn
+                               )
 import Data.Macaw.PPC.PPCReg
--- import Data.Macaw.PPC.Rewrite
+import Data.Macaw.PPC.Rewrite ( rewriteArchFn,
+                                rewriteArchStmt,
+                                rewriteArchTermStmt
+                              )
 
 data Hole = Hole
 
@@ -47,6 +63,13 @@ data Expr ids tp where
   ValueExpr :: !(Value PPC ids tp) -> Expr ids tp
   AppExpr   :: !(App (Expr ids) tp) -> Expr ids tp
 
+------------------------------------------------------------------------
+-- Location
+
+data Location addr (tp :: Type) where
+  MemoryAddr :: !addr -> !(MemRepr tp) -> Location addr tp
+  FullRegister :: !(PPCReg tp) -> Location addr tp
+
 ------------------------------------------------------------------------
 -- BlockSeq
 data BlockSeq ids = BlockSeq
@@ -137,65 +160,6 @@ getReg r = PPCGenerator $ St.StateT $ \genState -> do
   let expr = ValueExpr (genState ^. blockState ^. pBlockState ^. boundValue r)
   return (expr, genState)
 
-setReg :: PPCReg tp -> Value PPC ids tp -> PPCGenerator w s ids ()
-setReg = undefined
-
-disassembleFn :: proxy ppc -> MM.Memory (ArchAddrWidth ppc)
-              -> NC.NonceGenerator (ST ids) ids
-              -> ArchSegmentOff ppc
-              -> ArchAddrWord ppc
-              -> MA.AbsBlockState (ArchReg ppc)
-              -- ^ NOTE: We are leaving the type function ArchReg here because
-              -- we need to generalize over PPC64 vs PPC32
-              -> ST ids ([Block ppc ids], MM.MemWord (ArchAddrWidth ppc), Maybe String)
-disassembleFn = undefined
-
-preserveRegAcrossSyscall :: proxy ppc -> ArchReg ppc tp -> Bool
-preserveRegAcrossSyscall = undefined
-
-mkInitialAbsState :: proxy ppc -> MM.Memory (RegAddrWidth (ArchReg ppc))
-                  -> ArchSegmentOff ppc
-                  -> MA.AbsBlockState (ArchReg ppc)
-mkInitialAbsState = undefined
-
-absEvalArchFn :: proxy ppc -> AbsProcessorState (ArchReg ppc) ids
-              -> ArchFn ppc (Value ppc ids) tp
-              -> AbsValue (RegAddrWidth (ArchReg ppc)) tp
-absEvalArchFn = undefined
-
-absEvalArchStmt :: proxy ppc -> AbsProcessorState (ArchReg ppc) ids
-                -> ArchStmt ppc ids
-                -> AbsProcessorState (ArchReg ppc) ids
-absEvalArchStmt = undefined
-
-postCallAbsState :: proxy ppc -> AbsBlockState (ArchReg ppc)
-                 -> ArchSegmentOff ppc
-                 -> AbsBlockState (ArchReg ppc)
-postCallAbsState = undefined
-
-identifyCall :: proxy ppc -> MM.Memory (ArchAddrWidth ppc)
-             -> [Stmt ppc ids]
-             -> RegState (ArchReg ppc) (Value ppc ids)
-             -> Maybe (Seq.Seq (Stmt ppc ids), ArchSegmentOff ppc)
-identifyCall = undefined
-
-identifyReturn :: proxy ppc -> [Stmt ppc ids]
-               -> RegState (ArchReg ppc) (Value ppc ids)
-               -> Maybe [Stmt ppc ids]
-identifyReturn = undefined
-
-rewriteArchFn :: proxy ppc -> ArchFn ppc (Value ppc src) tp
-              -> Rewriter ppc src tgt (Value ppc tgt tp)
-rewriteArchFn = undefined
-
-rewriteArchStmt :: proxy ppc -> ArchStmt ppc src
-                -> Rewriter ppc src tgt ()
-rewriteArchStmt = undefined
-
-rewriteArchTermStmt :: proxy ppc -> ArchTermStmt ppc src
-                    -> Rewriter ppc src tgt (ArchTermStmt ppc tgt)
-rewriteArchTermStmt = undefined
-
 archDemandContext :: proxy ppc -> MDS.DemandContext ppc ids
 archDemandContext = undefined
 

macaw-ppc/src/Data/Macaw/PPC/Disassemble.hs

@@ -0,0 +1,18 @@
+module Data.Macaw.PPC.Disassemble ( disassembleFn ) where
+
+import           Control.Monad.ST ( ST )
+
+import           Data.Macaw.AbsDomain.AbsState as MA
+import           Data.Macaw.CFG
+import           Data.Macaw.CFG.Block
+import qualified Data.Macaw.Memory as MM
+import qualified Data.Parameterized.Nonce as NC
+
+disassembleFn :: proxy ppc
+              -> MM.Memory (ArchAddrWidth ppc)
+              -> NC.NonceGenerator (ST ids) ids
+              -> ArchSegmentOff ppc
+              -> ArchAddrWord ppc
+              -> MA.AbsBlockState (ArchReg ppc)
+              -> ST ids ([Block ppc ids], MM.MemWord (ArchAddrWidth ppc), Maybe String)
+disassembleFn = undefined

macaw-ppc/src/Data/Macaw/PPC/Eval.hs

@@ -0,0 +1,38 @@
+module Data.Macaw.PPC.Eval (
+  mkInitialAbsState,
+  absEvalArchFn,
+  absEvalArchStmt,
+  postCallAbsState,
+  preserveRegAcrossSyscall
+  ) where
+
+import           Data.Macaw.AbsDomain.AbsState as MA
+import           Data.Macaw.CFG
+import qualified Data.Macaw.Memory as MM
+
+preserveRegAcrossSyscall :: proxy ppc -> ArchReg ppc tp -> Bool
+preserveRegAcrossSyscall = undefined
+
+mkInitialAbsState :: proxy ppc
+                  -> MM.Memory (RegAddrWidth (ArchReg ppc))
+                  -> ArchSegmentOff ppc
+                  -> MA.AbsBlockState (ArchReg ppc)
+mkInitialAbsState = undefined
+
+absEvalArchFn :: proxy ppc
+              -> AbsProcessorState (ArchReg ppc) ids
+              -> ArchFn ppc (Value ppc ids) tp
+              -> AbsValue (RegAddrWidth (ArchReg ppc)) tp
+absEvalArchFn = undefined
+
+absEvalArchStmt :: proxy ppc
+                -> AbsProcessorState (ArchReg ppc) ids
+                -> ArchStmt ppc ids
+                -> AbsProcessorState (ArchReg ppc) ids
+absEvalArchStmt = undefined
+
+postCallAbsState :: proxy ppc
+                 -> AbsBlockState (ArchReg ppc)
+                 -> ArchSegmentOff ppc
+                 -> AbsBlockState (ArchReg ppc)
+postCallAbsState = undefined

macaw-ppc/src/Data/Macaw/PPC/Identify.hs

@@ -0,0 +1,22 @@
+module Data.Macaw.PPC.Identify (
+  identifyCall,
+  identifyReturn
+  ) where
+
+import qualified Data.Sequence as Seq
+
+import           Data.Macaw.CFG
+import qualified Data.Macaw.Memory as MM
+
+identifyCall :: proxy ppc
+             -> MM.Memory (ArchAddrWidth ppc)
+             -> [Stmt ppc ids]
+             -> RegState (ArchReg ppc) (Value ppc ids)
+             -> Maybe (Seq.Seq (Stmt ppc ids), ArchSegmentOff ppc)
+identifyCall = undefined
+
+identifyReturn :: proxy ppc
+               -> [Stmt ppc ids]
+               -> RegState (ArchReg ppc) (Value ppc ids)
+               -> Maybe [Stmt ppc ids]
+identifyReturn = undefined

macaw-ppc/src/Data/Macaw/PPC/Rewrite.hs

@@ -0,0 +1,23 @@
+module Data.Macaw.PPC.Rewrite (
+  rewriteArchFn,
+  rewriteArchStmt,
+  rewriteArchTermStmt
+  ) where
+
+import Data.Macaw.CFG
+import Data.Macaw.CFG.Rewriter
+
+rewriteArchFn :: proxy ppc
+              -> ArchFn ppc (Value ppc src) tp
+              -> Rewriter ppc src tgt (Value ppc tgt tp)
+rewriteArchFn = undefined
+
+rewriteArchStmt :: proxy ppc
+                -> ArchStmt ppc src
+                -> Rewriter ppc src tgt ()
+rewriteArchStmt = undefined
+
+rewriteArchTermStmt :: proxy ppc
+                    -> ArchTermStmt ppc src
+                    -> Rewriter ppc src tgt (ArchTermStmt ppc tgt)
+rewriteArchTermStmt = undefined