Minimal initial ARM abstract block state creation and dependencies.

macaw-arm/macaw-arm.cabal

@@ -14,7 +14,9 @@ cabal-version:       >=1.10
 
 library
   exposed-modules:     Data.Macaw.ARM
+                     , Data.Macaw.ARM.Arch
                      , Data.Macaw.ARM.ARMReg
+                     , Data.Macaw.ARM.Eval
                      , Data.Macaw.ARM.BinaryFormat.ELF
                      , Data.Macaw.ARM.Semantics.ARMSemantics
   -- other-modules:       
@@ -24,10 +26,12 @@ library
                      , bytestring
                      , cereal
                      , containers
+                     , dismantle-arm
                      , elf-edit
                      , lens
                      , macaw-base
                      , macaw-semmc
+                     , parameterized-utils
                      , semmc-arm
                      , vector
   -- build-tools:         arm-none-eabi-gcc

macaw-arm/src/Data/Macaw/ARM.hs

@@ -1,12 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeApplications #-}
 
--- {-# LANGUAGE FlexibleContexts #-}
--- {-# LANGUAGE ScopedTypeVariables #-}
--- {-# LANGUAGE RankNTypes #-}
--- {-# LANGUAGE GADTs #-}
--- {-# LANGUAGE GeneralizedNewtypeDeriving #-}
-
 module Data.Macaw.ARM
     ( -- * Macaw configurations
       arm_linux_info,
@@ -18,31 +12,25 @@ module Data.Macaw.ARM
     )
     where
 
-
-import qualified Data.Macaw.ARM.Semantics.ARMSemantics as ARMSem
-import qualified Data.Macaw.AbsDomain.AbsState as MA
+import           Data.Macaw.ARM.Eval
 import qualified Data.Macaw.Architecture.Info as MI
-import           Data.Macaw.CFG ( ArchSegmentOff )
 import qualified Data.Macaw.Memory as MM
-import           Data.Macaw.Types ( BVType )
-import qualified SemMC.ARM as ARM
 import           Data.Proxy ( Proxy(..) )
-import           Data.Macaw.ARM.ARMReg
+import qualified SemMC.ARM as ARM
 
 
 -- | The type tag for ARM (32-bit)
 type ARM = ARM.ARM
 
 
--- arm_linux_info :: (ArchSegmentOff ARM.ARM -> Maybe (MA.AbsValue 32 (BVType 32))) -> MI.ArchitectureInfo ARM.ARM
 arm_linux_info :: MI.ArchitectureInfo ARM.ARM
 arm_linux_info =
-    MI.ArchitectureInfo { MI.withArchConstraints = undefined -- id -- \x -> x
+    MI.ArchitectureInfo { MI.withArchConstraints = undefined -- \x -> x
                         , MI.archAddrWidth = MM.Addr32
                         , MI.archEndianness = MM.LittleEndian
-                        , MI.jumpTableEntrySize = undefined -- jumpTableEntrySize proxy
+                        , MI.jumpTableEntrySize = 0 -- undefined -- jumpTableEntrySize proxy
                         , MI.disassembleFn = undefined -- disassembleFn proxy ARMSem.execInstruction
-                        , MI.mkInitialAbsState = undefined -- mkInitialAbsState proxy tocMap
+                        , MI.mkInitialAbsState = mkInitialAbsState proxy
                         , MI.absEvalArchFn = undefined -- absEvalArchFn proxy
                         , MI.absEvalArchStmt = undefined -- absEvalArchStmt proxy
                         , MI.postCallAbsState = undefined -- postCallAbsState proxy

macaw-arm/src/Data/Macaw/ARM/ARMReg.hs

@@ -1,27 +1,31 @@
 -- | Defines the register types for ARM, along with some helpers
 
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Data.Macaw.ARM.ARMReg
     ( ARMReg(..)
+    -- , ArchWidth(..)
     )
     where
 
-import           GHC.TypeLits
 import qualified Data.Macaw.CFG as MC
+import           Data.Macaw.Types ( TypeRepr(..), HasRepr, BVType
+                                  , typeRepr, n32 )
+import           Data.Parameterized.Classes
+import           Data.Parameterized.Some ( Some(..) )
+import           GHC.TypeLits
+import qualified Data.Parameterized.TH.GADT as TH
 import qualified SemMC.ARM as ARM
-import           Data.Macaw.Types ( BVType )
+
 
 data ARMReg tp where
     ARM_IP :: (w ~ MC.RegAddrWidth ARMReg, 1 <= w) => ARMReg (BVType w)
@@ -33,8 +37,38 @@ instance Show (ARMReg tp) where
     show r = case r of
                ARM_IP -> "ip"
 
--- instance ShowF ARMReg where
---     showF = show
+instance ShowF ARMReg where
+    showF = show
+
+$(return [])  -- allow template haskell below to see definitions above
+
+instance TestEquality ARMReg where
+    testEquality = $(TH.structuralTypeEquality [t| ARMReg |] [])
+
+instance OrdF ARMReg where
+    compareF = $(TH.structuralTypeOrd [t| ARMReg |] [])
+
+instance HasRepr ARMReg TypeRepr where
+    typeRepr r =
+        case r of
+          ARM_IP -> BVTypeRepr n32
 
 type instance MC.ArchReg ARM.ARM = ARMReg
 type instance MC.RegAddrWidth ARMReg = 32
+
+
+instance ( 1 <= MC.RegAddrWidth ARMReg
+         , KnownNat (MC.RegAddrWidth ARMReg)
+         -- , MM.MemWidth (MC.RegAddrWidth (MC.ArchReg arm))
+         -- , MC.ArchReg arm ~ ARMReg
+         -- , ArchWidth arm
+         ) =>
+    MC.RegisterInfo ARMReg where
+      archRegs = armRegs
+      sp_reg = undefined
+      ip_reg = ARM_IP
+      syscall_num_reg = undefined
+      syscallArgumentRegs = undefined
+
+armRegs :: forall w. (w ~ MC.RegAddrWidth ARMReg, 1 <= w) => [Some ARMReg]
+armRegs = [ Some ARM_IP ]

macaw-arm/src/Data/Macaw/ARM/Arch.hs

@@ -0,0 +1,114 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# LANGUAGE StandaloneDeriving    #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications      #-}
+
+module Data.Macaw.ARM.Arch
+    -- ( ARMArchConstraints
+    -- , ARMStmt(..)
+    -- )
+    where
+
+
+import           Data.Macaw.ARM.ARMReg
+import qualified Data.Macaw.CFG as MC
+import qualified Data.Macaw.Memory as MM
+import qualified Data.Macaw.SemMC.Operands as O
+import qualified Data.Macaw.Types as MT
+import qualified Data.Parameterized.TraversableFC as FCls
+import qualified Dismantle.ARM as D
+import           GHC.TypeLits
+import qualified SemMC.ARM as ARM
+import qualified Text.PrettyPrint.ANSI.Leijen as PP
+
+-- ----------------------------------------------------------------------
+-- ARM-specific statement definitions
+
+data ARMStmt (v :: MT.Type -> *) where
+    WhatShouldThisBe :: ARMStmt v
+
+type instance MC.ArchStmt ARM.ARM = ARMStmt
+
+instance MC.IsArchStmt ARMStmt where
+    ppArchStmt pp stmt =
+        case stmt of
+          WhatShouldThisBe -> PP.text "arm_what?"
+
+-- ----------------------------------------------------------------------
+-- ARM terminal statements (which have instruction-specific effects on
+-- control-flow and register state).
+
+data ARMTermStmt ids where
+    ARMSyscall :: ARMTermStmt ids
+
+deriving instance Show (ARMTermStmt ids)
+
+type instance MC.ArchTermStmt ARM.ARM = ARMTermStmt
+
+instance MC.PrettyF ARMTermStmt where
+    prettyF ts =
+        case ts of
+          ARMSyscall -> PP.text "arm_syscall"
+
+-- instance PrettyF (ArchTermStmt ARM.ARM))
+
+-- ----------------------------------------------------------------------
+-- ARM functions.  These may return a value, and may depend on the
+-- current state of the heap and the set of registeres defined so far
+-- and the result type, but should not affect the processor state.
+
+-- type family ArchStmt (arch :: *) :: (Type -> *) -> *
+-- data ARMStmt (v :: MT.Type -> *) where
+--     WhatShouldThisBe :: ARMStmt v
+-- type instance MC.ArchStmt ARM.ARM = ARMStmt
+
+-- type family ArchFn :: (arch :: *) :: (Type -> *) -> Type -> *
+-- data ARMPrimFn f (tp :: (MT.Type -> *) -> MT.Type) where
+--     NoPrimKnown :: ARMPrimFn tp
+data ARMPrimFn f tp where
+    NoPrimKnown :: f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ARM.ARM))) -> ARMPrimFn f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ARM.ARM)))
+
+instance MC.IsArchFn ARMPrimFn where
+  ppArchFn pp f =
+      case f of
+        NoPrimKnown rhs -> (\rhs' -> PP.text "arm_noprimknown " PP.<> rhs') <$> pp rhs
+
+instance FCls.FunctorFC ARMPrimFn where
+  fmapFC = FCls.fmapFCDefault
+
+instance FCls.FoldableFC ARMPrimFn where
+  foldMapFC = FCls.foldMapFCDefault
+
+instance FCls.TraversableFC ARMPrimFn where
+  traverseFC go f =
+    case f of
+      NoPrimKnown rhs -> NoPrimKnown <$> go rhs
+
+type instance MC.ArchFn ARM.ARM = ARMPrimFn
+
+-- ----------------------------------------------------------------------
+-- The aggregate set of architectural constraints to express for ARM
+-- computations
+
+type ARMArchConstraints arm = ( MC.ArchReg arm ~ ARMReg
+                              , MC.ArchFn arm ~ ARMPrimFn
+                              , MC.ArchStmt arm ~ ARMStmt
+                              -- , MC.ArchTermStmt arm ~ ARMTermStmt
+                              -- , ArchWidth arm
+                              , MM.MemWidth (MC.RegAddrWidth (MC.ArchReg arm))
+                              , 1 <= MC.RegAddrWidth ARMReg
+                              , KnownNat (MC.RegAddrWidth ARMReg)
+                              , MC.ArchConstraints arm
+                              -- , O.ExtractValue arm D.GPR (MT.BVType (MC.RegAddrWidth (MC.ArchReg arm)))
+                              -- , O.ExtractValue arm (Maybe D.GPR) (MT.BVType (MC.RegAddrWidth (MC.ArchReg arm)))
+                              )

macaw-arm/src/Data/Macaw/ARM/Eval.hs

@@ -0,0 +1,33 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Macaw.ARM.Eval
+    ( mkInitialAbsState
+    )
+    where
+
+import           Control.Lens ( (&) )
+import           Data.Macaw.ARM.Arch
+import           Data.Macaw.AbsDomain.AbsState as MA
+import           Data.Macaw.CFG
+import qualified Data.Macaw.Memory as MM
+
+-- | Set up an initial abstract state that holds at the beginning of a basic
+-- block.
+--
+-- The 'MM.Memory' is the mapped memory region
+--
+-- The 'ArchSegmentOff' is the start address of the basic block.
+--
+mkInitialAbsState :: (ARMArchConstraints arm, ArchStmt arm ~ ARMStmt)
+                  => proxy arm
+                  -> MM.Memory (RegAddrWidth (ArchReg arm))
+                  -> ArchSegmentOff arm
+                  -> MA.AbsBlockState (ArchReg arm)
+mkInitialAbsState _ _mem startAddr =
+    MA.top & MA.setAbsIP startAddr

macaw-arm/tests/ARMTests.hs

@@ -9,29 +9,21 @@ module ARMTests
     where
 
 
-import           Control.Lens ( (^.), to )
 import           Control.Monad.Catch (throwM, Exception)
 import qualified Data.ElfEdit as E
 import qualified Data.Foldable as F
-import           Data.List (intercalate)
 import qualified Data.Macaw.ARM as RO
-import           Data.Macaw.ARM.ARMReg
 import qualified Data.Macaw.ARM.BinaryFormat.ELF as ARMELF
 import qualified Data.Macaw.AbsDomain.AbsState as MA
 import qualified Data.Macaw.Discovery as MD
-import qualified Data.Macaw.Discovery.State as MD
 import qualified Data.Macaw.Memory as MM
 import           Data.Macaw.Types ( BVType )
 import qualified Data.Map as M
-import           Data.Maybe ( fromJust, mapMaybe )
 import           Data.Monoid
-import           Data.Parameterized.NatRepr
-import qualified Data.Parameterized.Some as PU
 import           Data.Proxy ( Proxy(..) )
 import qualified Data.Set as S
 import           Data.Typeable ( Typeable )
 import           Data.Word ( Word64 )
-import           Debug.Trace (trace)
 import qualified SemMC.ARM as ARM
 import           Shared
 import           System.FilePath ( dropExtension, replaceExtension )