mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-28 01:35:33 +03:00
Refactor to support Boolean type; start mapping to Crucible.
This commit is contained in:
Joe Hendrix
parent
0c3c935b7b
commit
3fe64acd07
24
macaw-symbolic/macaw-symbolic.cabal
Normal file
24
macaw-symbolic/macaw-symbolic.cabal
Normal file
@ -0,0 +1,24 @@
|
||||
name: macaw-symbolic
|
||||
version: 0.0.1
|
||||
author: Galois, Inc.
|
||||
maintainer: jhendrix@galois.com
|
||||
build-type: Simple
|
||||
cabal-version: >= 1.9.2
|
||||
|
||||
library
|
||||
build-depends:
|
||||
base >= 4,
|
||||
containers,
|
||||
crucible,
|
||||
macaw,
|
||||
mtl,
|
||||
parameterized-utils
|
||||
|
||||
hs-source-dirs: src
|
||||
|
||||
exposed-modules:
|
||||
Data.Macaw.Symbolic.App
|
||||
Data.Macaw.Symbolic
|
||||
|
||||
ghc-options: -Wall -Werror
|
||||
ghc-prof-options: -O2 -fprof-auto-top
|
||||
92
macaw-symbolic/src/Data/Macaw/Symbolic.hs
Normal file
92
macaw-symbolic/src/Data/Macaw/Symbolic.hs
Normal file
@ -0,0 +1,92 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE KindSignatures #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
module Data.Macaw.Symbolic
|
||||
( stepBlocks
|
||||
) where
|
||||
|
||||
import Control.Monad.ST
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import qualified Data.Parameterized.Context as Ctx
|
||||
import Data.Parameterized.Ctx
|
||||
import qualified Data.Parameterized.Map as MapF
|
||||
import Data.String
|
||||
import Data.Word
|
||||
import qualified Lang.Crucible.CFG.Core as C
|
||||
import qualified Lang.Crucible.CFG.Reg as CR
|
||||
import qualified Lang.Crucible.CFG.SSAConversion as C
|
||||
import qualified Lang.Crucible.Config as C
|
||||
import qualified Lang.Crucible.FunctionHandle as C
|
||||
import qualified Lang.Crucible.Simulator.ExecutionTree as C
|
||||
import qualified Lang.Crucible.Simulator.GlobalState as C
|
||||
import qualified Lang.Crucible.Simulator.OverrideSim as C
|
||||
import qualified Lang.Crucible.Simulator.RegMap as C
|
||||
import Lang.Crucible.Solver.Interface
|
||||
import Numeric (showHex)
|
||||
import System.IO (stdout)
|
||||
|
||||
import qualified Data.Macaw.CFG.Block as M
|
||||
|
||||
data ReoptSimulatorState sym = ReoptSimulatorState
|
||||
|
||||
type family ArchRegContext (arch :: *) :: Ctx C.CrucibleType
|
||||
|
||||
type ArchRegStruct (arch :: *) = C.StructType (ArchRegContext arch)
|
||||
|
||||
type MacawFunctionArgs arch = EmptyCtx ::> ArchRegStruct arch
|
||||
type MacawFunctionResult arch = ArchRegStruct arch
|
||||
|
||||
translateBlock :: Map Word64 (CR.Label s)
|
||||
-> M.Block arch ids
|
||||
-> CR.Block s (MacawFunctionResult arch)
|
||||
translateBlock = undefined
|
||||
|
||||
--data MacawRegClass (tp :: M.TypeRepr) =
|
||||
|
||||
stepBlocks :: forall sym arch ids
|
||||
. IsSymInterface sym
|
||||
=> sym
|
||||
-> Ctx.Assignment C.TypeRepr (ArchRegContext arch)
|
||||
-> Word64
|
||||
-> Map Word64 (M.Block arch ids)
|
||||
-- ^ Map from block indices to block
|
||||
-> IO (C.ExecResult ReoptSimulatorState sym (C.RegEntry sym (C.StructType (ArchRegContext arch))))
|
||||
stepBlocks sym regTypes addr macawBlockMap = do
|
||||
let macawStructRepr = C.StructRepr regTypes
|
||||
halloc <- C.newHandleAllocator
|
||||
let argTypes = Ctx.empty Ctx.%> macawStructRepr
|
||||
let nm = fromString $ "macaw_0x" ++ showHex addr ""
|
||||
h <- stToIO $ C.mkHandle' halloc nm argTypes macawStructRepr
|
||||
-- Map block map to Crucible CFG
|
||||
let blockLabelMap :: Map Word64 (CR.Label ())
|
||||
blockLabelMap = Map.fromList [ (w, CR.Label (fromIntegral w)) | w <- Map.keys macawBlockMap ]
|
||||
-- Create control flow graph
|
||||
let rg :: CR.CFG () (MacawFunctionArgs arch) (MacawFunctionResult arch)
|
||||
rg = CR.CFG { CR.cfgHandle = h
|
||||
, CR.cfgBlocks = translateBlock blockLabelMap <$> Map.elems macawBlockMap
|
||||
}
|
||||
cfg <- C.initialConfig 0 []
|
||||
let ctx :: C.SimContext ReoptSimulatorState sym
|
||||
ctx = C.SimContext { C._ctxSymInterface = sym
|
||||
, C.ctxSolverProof = \a -> a
|
||||
, C.ctxIntrinsicTypes = MapF.empty
|
||||
, C.simConfig = cfg
|
||||
, C.simHandleAllocator = halloc
|
||||
, C.printHandle = stdout
|
||||
, C._functionBindings = C.emptyHandleMap
|
||||
, C._cruciblePersonality = ReoptSimulatorState
|
||||
}
|
||||
-- Create the symbolic simulator state
|
||||
let s = C.initSimState ctx C.emptyGlobals C.defaultErrorHandler
|
||||
-- Define the arguments to call the Reopt CFG with.
|
||||
-- This should be a symbolic variable for each register in the architecture.
|
||||
let args :: C.RegMap sym (MacawFunctionArgs arch)
|
||||
args = undefined
|
||||
-- Run the symbolic simulator.
|
||||
case C.toSSA rg of
|
||||
C.SomeCFG g ->
|
||||
C.runOverrideSim s macawStructRepr $ do
|
||||
C.regValue <$> C.callCFG g args
|
||||
37
macaw-symbolic/src/Data/Macaw/Symbolic/App.hs
Normal file
37
macaw-symbolic/src/Data/Macaw/Symbolic/App.hs
Normal file
@ -0,0 +1,37 @@
|
||||
{-
|
||||
-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# OPTIONS_GHC -Wwarn #-}
|
||||
module Data.Macaw.Symbolic.App where
|
||||
|
||||
import Control.Monad.Identity
|
||||
import qualified Data.Macaw.CFG as M
|
||||
import qualified Data.Macaw.Types as M
|
||||
import qualified Lang.Crucible.CFG.Expr as C
|
||||
import qualified Lang.Crucible.CFG.Reg as C
|
||||
import qualified Lang.Crucible.Types as C
|
||||
|
||||
type family ToCrucibleType (mtp :: M.Type) :: C.CrucibleType where
|
||||
ToCrucibleType (M.BVType w) = C.BVType w
|
||||
|
||||
type CrucGen = Identity
|
||||
|
||||
valueToCrucible :: M.Value arch ids tp -> CrucGen (C.Value s (ToCrucibleType tp))
|
||||
valueToCrucible = undefined
|
||||
|
||||
valueToBool :: M.Value arch ids M.BoolType -> CrucGen (C.Value s C.BoolType)
|
||||
valueToBool = undefined
|
||||
|
||||
crucibleValue :: C.App (C.Value s) ctp -> CrucGen (C.Value s ctp)
|
||||
crucibleValue = undefined
|
||||
|
||||
appToCrucible :: M.App (M.Value arch ids) tp -> CrucGen (C.Value s (ToCrucibleType tp))
|
||||
appToCrucible app =
|
||||
case app of
|
||||
M.Mux w c t f -> do
|
||||
crucibleValue =<<
|
||||
C.BVIte <$> valueToBool c
|
||||
<*> pure w
|
||||
<*> valueToCrucible t
|
||||
<*> valueToCrucible f
|
||||
@ -133,7 +133,9 @@ class Eq d => AbsDomain d where
|
||||
-- The first parameter is the width of pointers on the value. It is expected
|
||||
-- to be at most 64 bits.
|
||||
data AbsValue w (tp :: Type)
|
||||
= forall n . (tp ~ BVType n) => FinSet !(Set Integer)
|
||||
= (tp ~ BoolType) => BoolConst !Bool
|
||||
-- ^ A Boolean constant
|
||||
| forall n . (tp ~ BVType n) => FinSet !(Set Integer)
|
||||
-- ^ Denotes that this value can take any one of the fixed set.
|
||||
| (tp ~ BVType w) => CodePointers !(Set (SegmentedAddr w)) !Bool
|
||||
-- ^ A possibly empty set of values that either point to a code segment.
|
||||
@ -242,6 +244,7 @@ instance Show (AbsValue w tp) where
|
||||
show = show . pretty
|
||||
|
||||
instance Pretty (AbsValue w tp) where
|
||||
pretty (BoolConst b) = text (show b)
|
||||
pretty (FinSet s) = text "finset" <+> ppIntegerSet s
|
||||
pretty (CodePointers s b) = text "code" <+> ppSet (s0 ++ sd)
|
||||
where s0 = if b then [text "0"] else []
|
||||
@ -459,6 +462,7 @@ mayBeMember _n _v = True
|
||||
|
||||
-- | Returns true if this value represents the empty set.
|
||||
isBottom :: AbsValue w tp -> Bool
|
||||
isBottom BoolConst{} = False
|
||||
isBottom (FinSet v) = Set.null v
|
||||
isBottom (CodePointers v b) = Set.null v && not b
|
||||
isBottom (StackOffset _ v) = Set.null v
|
||||
@ -745,10 +749,10 @@ instance ShowF r => PrettyRegValue r (AbsValue w) where
|
||||
|
||||
|
||||
absTrue :: AbsValue w BoolType
|
||||
absTrue = FinSet (Set.singleton 1)
|
||||
absTrue = BoolConst True
|
||||
|
||||
absFalse :: AbsValue w BoolType
|
||||
absFalse = FinSet (Set.singleton 0)
|
||||
absFalse = BoolConst False
|
||||
|
||||
-- | This returns the smallest abstract value that contains the
|
||||
-- given unsigned integer.
|
||||
@ -775,19 +779,19 @@ concreteStackOffset a o = StackOffset a (Set.singleton (fromInteger o))
|
||||
------------------------------------------------------------------------
|
||||
-- Restrictions
|
||||
|
||||
hasMaximum :: TypeRepr tp -> AbsValue w tp -> Maybe Integer
|
||||
hasMaximum :: TypeRepr (BVType w) -> AbsValue p (BVType w) -> Maybe Integer
|
||||
hasMaximum tp v =
|
||||
case v of
|
||||
FinSet s | Set.null s -> Nothing
|
||||
| otherwise -> Just $! Set.findMax s
|
||||
CodePointers s b | Set.null s -> if b then Just 0 else Nothing
|
||||
| otherwise -> Just $ case tp of BVTypeRepr n -> maxUnsigned n
|
||||
StridedInterval si -> Just (SI.intervalEnd si)
|
||||
TopV -> Just $ case tp of BVTypeRepr n -> maxUnsigned n
|
||||
_ -> Nothing
|
||||
FinSet s | Set.null s -> Nothing
|
||||
| otherwise -> Just $! Set.findMax s
|
||||
CodePointers s b | Set.null s -> if b then Just 0 else Nothing
|
||||
| otherwise -> Just $ case tp of BVTypeRepr n -> maxUnsigned n
|
||||
StridedInterval si -> Just (SI.intervalEnd si)
|
||||
TopV -> Just $ case tp of BVTypeRepr n -> maxUnsigned n
|
||||
_ -> Nothing
|
||||
|
||||
|
||||
hasMinimum :: TypeRepr tp -> AbsValue w tp -> Maybe Integer
|
||||
hasMinimum :: TypeRepr (BVType w) -> AbsValue p (BVType w) -> Maybe Integer
|
||||
hasMinimum _tp v =
|
||||
case v of
|
||||
FinSet s | Set.null s -> Nothing
|
||||
@ -807,10 +811,9 @@ abstractULt :: MemWidth w
|
||||
-> AbsValue w tp
|
||||
-> (AbsValue w tp, AbsValue w tp)
|
||||
abstractULt _tp TopV TopV = (TopV, TopV)
|
||||
abstractULt tp x y
|
||||
abstractULt tp@(BVTypeRepr n) x y
|
||||
| Just u_y <- hasMaximum tp y
|
||||
, Just l_x <- hasMinimum tp x
|
||||
, BVTypeRepr n <- tp =
|
||||
, Just l_x <- hasMinimum tp x =
|
||||
-- debug DAbsInt' ("abstractLt " ++ show (pretty x) ++ " " ++ show (pretty y) ++ " -> ")
|
||||
( meet x (stridedInterval $ SI.mkStridedInterval n False 0 (u_y - 1) 1)
|
||||
, meet y (stridedInterval $ SI.mkStridedInterval n False (l_x + 1)
|
||||
@ -821,14 +824,13 @@ abstractULt _tp x y = (x, y)
|
||||
-- | @abstractULeq x y@ refines x and y with the knowledge that @x <= y@
|
||||
abstractULeq :: MemWidth w
|
||||
=> TypeRepr tp
|
||||
-> AbsValue w tp
|
||||
-> AbsValue w tp
|
||||
-> (AbsValue w tp, AbsValue w tp)
|
||||
-> AbsValue w tp
|
||||
-> AbsValue w tp
|
||||
-> (AbsValue w tp, AbsValue w tp)
|
||||
abstractULeq _tp TopV TopV = (TopV, TopV)
|
||||
abstractULeq tp x y
|
||||
abstractULeq tp@(BVTypeRepr n) x y
|
||||
| Just u_y <- hasMaximum tp y
|
||||
, Just l_x <- hasMinimum tp x
|
||||
, BVTypeRepr n <- tp =
|
||||
, Just l_x <- hasMinimum tp x =
|
||||
( meet x (stridedInterval $ SI.mkStridedInterval n False 0 u_y 1)
|
||||
, meet y (stridedInterval $ SI.mkStridedInterval n False l_x
|
||||
(maxUnsigned n) 1))
|
||||
@ -1099,21 +1101,6 @@ deleteRange l h m
|
||||
deleteRange (k+1) h (Map.delete k m)
|
||||
_ -> m
|
||||
|
||||
-- Return the width of a value.
|
||||
someValueWidth :: ( HasRepr (ArchReg arch) TypeRepr
|
||||
)
|
||||
=> Value arch ids tp
|
||||
-> Integer
|
||||
someValueWidth v =
|
||||
case typeRepr v of
|
||||
BVTypeRepr w -> natValue w
|
||||
|
||||
valueByteSize :: ( HasRepr (ArchReg arch) TypeRepr
|
||||
)
|
||||
=> Value arch ids tp
|
||||
-> Int64
|
||||
valueByteSize v = fromInteger $ (someValueWidth v + 7) `div` 8
|
||||
|
||||
-- | Prune stack based on write that may modify stack.
|
||||
pruneStack :: AbsBlockStack w -> AbsBlockStack w
|
||||
pruneStack = Map.filter f
|
||||
@ -1143,6 +1130,7 @@ transferValue c v = do
|
||||
amap = c^.absAssignments
|
||||
aregs = c^.absInitialRegs
|
||||
case v of
|
||||
BoolValue b -> BoolConst b
|
||||
BVValue w i
|
||||
| 0 <= i && i <= maxUnsigned w -> abstractSingleton code_width is_code w i
|
||||
| otherwise -> error $ "transferValue given illegal value " ++ show (pretty v)
|
||||
@ -1183,7 +1171,7 @@ addMemWrite a memRepr v r =
|
||||
++" in SomeStackOffset case") $
|
||||
r & curAbsStack %~ pruneStack
|
||||
(StackOffset _ s, v_abs) ->
|
||||
let w = valueByteSize v
|
||||
let w = fromInteger (memReprBytes memRepr)
|
||||
e = StackEntry memRepr v_abs
|
||||
stk0 = r^.curAbsStack
|
||||
-- Delete information about old assignment
|
||||
|
||||
@ -169,13 +169,14 @@ assertPred _ _ bnds = Right bnds
|
||||
|
||||
-- | Lookup an upper bound or return analysis for why it is not defined.
|
||||
unsignedUpperBound :: ( MapF.OrdF (ArchReg arch)
|
||||
, MapF.ShowF (ArchReg arch)
|
||||
)
|
||||
, MapF.ShowF (ArchReg arch)
|
||||
)
|
||||
=> IndexBounds (ArchReg arch) ids
|
||||
-> Value arch ids tp
|
||||
-> Either String (UpperBound tp)
|
||||
unsignedUpperBound bnds v =
|
||||
case v of
|
||||
BoolValue _ -> Left "Boolean values do not have bounds."
|
||||
BVValue _ i -> Right (IntegerUpperBound i)
|
||||
RelocatableValue{} ->
|
||||
Left "Relocatable values do not have bounds."
|
||||
|
||||
@ -43,6 +43,7 @@ refineProcState :: RefineConstraints arch
|
||||
-> AbsValue (ArchAddrWidth arch) tp -- ^ Abstract value to assign value.
|
||||
-> AbsProcessorState (ArchReg arch) ids
|
||||
-> AbsProcessorState (ArchReg arch) ids
|
||||
refineProcState (BoolValue _) _av regs = regs -- Skip refinment for literal values
|
||||
refineProcState (BVValue _n _val) _av regs = regs -- Skip refinment for literal values
|
||||
refineProcState (RelocatableValue _ _) _av regs = regs -- Skip refinment for relocatable values
|
||||
refineProcState (Initial r) av regs =
|
||||
@ -84,8 +85,8 @@ refineApp app av regs =
|
||||
|
||||
-- FIXME: HACK
|
||||
-- This detects r - x < 0 || r - x == 0, i.e. r <= x
|
||||
BVOr _ (getAssignApp -> Just (UsbbOverflows _ r xv@(BVValue sz x) (BVValue _ 0)))
|
||||
(getAssignApp -> Just (BVEq (getAssignApp -> Just (BVAdd _ r' y)) (BVValue _ 0)))
|
||||
OrApp (getAssignApp -> Just (UsbbOverflows _ r xv@(BVValue sz x) (BoolValue False)))
|
||||
(getAssignApp -> Just (Eq (getAssignApp -> Just (BVAdd _ r' y)) (BVValue _ 0)))
|
||||
| Just Refl <- testEquality r r'
|
||||
, Just Refl <- testEquality y (mkLit sz (negate x))
|
||||
, Just b <- asConcreteSingleton av ->
|
||||
@ -93,10 +94,10 @@ refineApp app av regs =
|
||||
|
||||
-- FIXME: HACK
|
||||
-- This detects not (r - x < 0) && not (r - x == 0), i.e. x < r
|
||||
BVAnd _ (getAssignApp -> Just (BVComplement _
|
||||
(getAssignApp -> Just (UsbbOverflows _ r xv@(BVValue sz x) (BVValue _ 0)))))
|
||||
(getAssignApp -> Just (BVComplement _
|
||||
(getAssignApp -> Just (BVEq (getAssignApp -> Just (BVAdd _ r' y)) (BVValue _ 0)))))
|
||||
AndApp (getAssignApp -> Just
|
||||
(NotApp (getAssignApp -> Just (UsbbOverflows _ r xv@(BVValue sz x) (BoolValue False)))))
|
||||
(getAssignApp -> Just
|
||||
(NotApp (getAssignApp -> Just (Eq (getAssignApp -> Just (BVAdd _ r' y)) (BVValue _ 0)))))
|
||||
| Just Refl <- testEquality r r'
|
||||
, Just Refl <- testEquality y (mkLit sz (negate x))
|
||||
, Just b <- asConcreteSingleton av ->
|
||||
|
||||
@ -66,42 +66,44 @@ data App (f :: Type -> *) (tp :: Type) where
|
||||
-- Truncate a bitvector value.
|
||||
Trunc :: (1 <= n, n+1 <= m) => !(f (BVType m)) -> !(NatRepr n) -> App f (BVType n)
|
||||
-- Signed extension.
|
||||
SExt :: (1 <= m, m+1 <= n) => f (BVType m) -> NatRepr n -> App f (BVType n)
|
||||
SExt :: (1 <= m, m+1 <= n, 1 <= n) => f (BVType m) -> NatRepr n -> App f (BVType n)
|
||||
-- Unsigned extension.
|
||||
UExt :: (1 <= m, m+1 <= n) => f (BVType m) -> NatRepr n -> App f (BVType n)
|
||||
UExt :: (1 <= m, m+1 <= n, 1 <= n) => f (BVType m) -> NatRepr n -> App f (BVType n)
|
||||
|
||||
----------------------------------------------------------------------
|
||||
-- Boolean operations
|
||||
|
||||
BoolMux :: !(f BoolType) -> !(f BoolType) -> !(f BoolType) -> App f BoolType
|
||||
AndApp :: !(f BoolType) -> !(f BoolType) -> App f BoolType
|
||||
OrApp :: !(f BoolType) -> !(f BoolType) -> App f BoolType
|
||||
NotApp :: !(f BoolType) -> App f BoolType
|
||||
XorApp :: !(f BoolType) -> !(f BoolType) -> App f BoolType
|
||||
|
||||
----------------------------------------------------------------------
|
||||
-- Bitvector operations
|
||||
|
||||
BVAdd :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVSub :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVAdd :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVSub :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
-- Multiply two numbers
|
||||
BVMul :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVMul :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
-- Unsigned division (rounds fractions to zero).
|
||||
--
|
||||
-- This operation is not defined when the denominator is zero. The
|
||||
-- caller should raise a #de exception in this case (see
|
||||
-- 'Reopt.Semantics.Implementation.exec_div').
|
||||
BVQuot :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVQuot :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
-- Unsigned modulo (rounds fractional results to zero)
|
||||
--
|
||||
-- See 'BVQuot' for usage.
|
||||
BVRem :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVRem :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
-- Signed division (rounds fractional results to zero).
|
||||
--
|
||||
-- See 'BVQuot' for usage.
|
||||
BVSignedQuot :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVSignedQuot :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
-- Signed modulo (rounds fractional results to zero).
|
||||
--
|
||||
@ -110,13 +112,13 @@ data App (f :: Type -> *) (tp :: Type) where
|
||||
-- x = (y * BVSignedQuot x y) + BVSignedRem x y
|
||||
--
|
||||
-- See 'BVQuot' for usage.
|
||||
BVSignedRem :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVSignedRem :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
-- Unsigned less than.
|
||||
BVUnsignedLt :: !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
|
||||
BVUnsignedLt :: (1 <= n) => !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
|
||||
|
||||
-- Unsigned less than or equal.
|
||||
BVUnsignedLe :: !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
|
||||
BVUnsignedLe :: (1 <= n) => !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
|
||||
|
||||
-- Signed less than
|
||||
BVSignedLt :: (1 <= n) => !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
|
||||
@ -129,29 +131,29 @@ data App (f :: Type -> *) (tp :: Type) where
|
||||
BVTestBit :: !(f (BVType n)) -> !(f (BVType log_n)) -> App f BoolType
|
||||
|
||||
-- Bitwise complement
|
||||
BVComplement :: !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVComplement :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
|
||||
-- Bitwise and
|
||||
BVAnd :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVAnd :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
-- Bitwise or
|
||||
BVOr :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVOr :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
-- Exclusive or
|
||||
BVXor :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVXor :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
-- Logical left shift (x * 2 ^ n)
|
||||
BVShl :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVShl :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
-- Logical right shift (x / 2 ^ n)
|
||||
BVShr :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
BVShr :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
-- Arithmetic right shift (x / 2 ^ n)
|
||||
BVSar :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
-- Compare for equality.
|
||||
BVEq :: !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
|
||||
Eq :: !(f tp) -> !(f tp) -> App f BoolType
|
||||
|
||||
-- Return true if value contains even number of true bits.
|
||||
EvenParity :: !(f (BVType 8)) -> App f BoolType
|
||||
|
||||
-- Reverse the bytes in a bitvector expression.
|
||||
ReverseBytes :: !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
|
||||
ReverseBytes :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
-- Add two values and a carry bit to determine if they have an unsigned
|
||||
-- overflow.
|
||||
@ -186,12 +188,12 @@ data App (f :: Type -> *) (tp :: Type) where
|
||||
-- bsf "bit scan forward" returns the index of the least-significant
|
||||
-- bit that is 1. Undefined if value is zero.
|
||||
-- All bits at indices less than return value must be unset.
|
||||
Bsf :: !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
|
||||
Bsf :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
-- bsr "bit scan reverse" returns the index of the most-significant
|
||||
-- bit that is 1. Undefined if value is zero.
|
||||
-- All bits at indices greater than return value must be unset.
|
||||
Bsr :: !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
|
||||
Bsr :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
----------------------------------------------------------------------
|
||||
-- Floating point operations
|
||||
@ -273,7 +275,8 @@ data App (f :: Type -> *) (tp :: Type) where
|
||||
-- If the conversion is out of the range of the bitvector, then a floating
|
||||
-- point exception should be raised.
|
||||
-- If that exception is masked, then this returns -1 (as a signed bitvector).
|
||||
TruncFPToSignedBV :: FloatInfoRepr flt
|
||||
TruncFPToSignedBV :: (1 <= n)
|
||||
=> FloatInfoRepr flt
|
||||
-> f (FloatType flt)
|
||||
-> NatRepr n
|
||||
-> App f (BVType n)
|
||||
@ -381,9 +384,11 @@ ppAppA pp a0 =
|
||||
Trunc x w -> sexprA "trunc" [ pp x, ppNat w ]
|
||||
SExt x w -> sexprA "sext" [ pp x, ppNat w ]
|
||||
UExt x w -> sexprA "uext" [ pp x, ppNat w ]
|
||||
BoolMux c t f -> sexprA "bool_mux" [ pp c, pp t, pp f ]
|
||||
AndApp x y -> sexprA "and" [ pp x, pp y ]
|
||||
OrApp x y -> sexprA "or" [ pp x, pp y ]
|
||||
NotApp x -> sexprA "not" [ pp x ]
|
||||
XorApp x y -> sexprA "xor" [ pp x, pp y ]
|
||||
BVAdd _ x y -> sexprA "bv_add" [ pp x, pp y ]
|
||||
BVSub _ x y -> sexprA "bv_sub" [ pp x, pp y ]
|
||||
BVMul _ x y -> sexprA "bv_mul" [ pp x, pp y ]
|
||||
@ -403,7 +408,7 @@ ppAppA pp a0 =
|
||||
BVShl _ x y -> sexprA "bv_shl" [ pp x, pp y ]
|
||||
BVShr _ x y -> sexprA "bv_shr" [ pp x, pp y ]
|
||||
BVSar _ x y -> sexprA "bv_sar" [ pp x, pp y ]
|
||||
BVEq x y -> sexprA "bv_eq" [ pp x, pp y ]
|
||||
Eq x y -> sexprA "eq" [ pp x, pp y ]
|
||||
EvenParity x -> sexprA "even_parity" [ pp x ]
|
||||
ReverseBytes _ x -> sexprA "reverse_bytes" [ pp x ]
|
||||
UadcOverflows _ x y c -> sexprA "uadc_overflows" [ pp x, pp y, pp c ]
|
||||
@ -442,9 +447,11 @@ instance HasRepr (App f) TypeRepr where
|
||||
SExt _ w -> BVTypeRepr w
|
||||
UExt _ w -> BVTypeRepr w
|
||||
|
||||
BoolMux{} -> knownType
|
||||
AndApp{} -> knownType
|
||||
OrApp{} -> knownType
|
||||
NotApp{} -> knownType
|
||||
XorApp{} -> knownType
|
||||
|
||||
BVAdd w _ _ -> BVTypeRepr w
|
||||
BVSub w _ _ -> BVTypeRepr w
|
||||
@ -467,7 +474,7 @@ instance HasRepr (App f) TypeRepr where
|
||||
BVShl w _ _ -> BVTypeRepr w
|
||||
BVShr w _ _ -> BVTypeRepr w
|
||||
BVSar w _ _ -> BVTypeRepr w
|
||||
BVEq _ _ -> knownType
|
||||
Eq _ _ -> knownType
|
||||
EvenParity _ -> knownType
|
||||
ReverseBytes w _ -> BVTypeRepr w
|
||||
|
||||
|
||||
@ -93,6 +93,7 @@ import Data.Parameterized.NatRepr
|
||||
import Data.Parameterized.Nonce
|
||||
import Data.Parameterized.Some
|
||||
import Data.Parameterized.TraversableF
|
||||
import Data.Proxy
|
||||
import Data.Set (Set)
|
||||
import qualified Data.Set as Set
|
||||
import Data.Text (Text)
|
||||
@ -212,10 +213,15 @@ type ArchSegmentedAddr arch = SegmentedAddr (ArchAddrWidth arch)
|
||||
-- | A value at runtime.
|
||||
data Value arch ids tp
|
||||
= forall n
|
||||
. (tp ~ BVType n)
|
||||
. (tp ~ BVType n, 1 <= n)
|
||||
=> BVValue !(NatRepr n) !Integer
|
||||
-- ^ A constant bitvector
|
||||
| ( tp ~ BVType (ArchAddrWidth arch))
|
||||
| (tp ~ BoolType)
|
||||
=> BoolValue !Bool
|
||||
-- ^ A constant Boolean
|
||||
| ( tp ~ BVType (ArchAddrWidth arch)
|
||||
, 1 <= ArchAddrWidth arch
|
||||
)
|
||||
=> RelocatableValue !(NatRepr (ArchAddrWidth arch)) !(ArchSegmentedAddr arch)
|
||||
-- ^ A given memory address.
|
||||
| AssignedValue !(Assignment arch ids tp)
|
||||
@ -241,7 +247,7 @@ data Assignment arch ids tp =
|
||||
-- or least significant byte. The following indices either store
|
||||
-- the next lower or higher bytes.
|
||||
data MemRepr (tp :: Type) where
|
||||
BVMemRepr :: !(NatRepr w) -> !Endianness -> MemRepr (BVType (8*w))
|
||||
BVMemRepr :: (1 <= w) => !(NatRepr w) -> !Endianness -> MemRepr (BVType (8*w))
|
||||
|
||||
instance Pretty (MemRepr tp) where
|
||||
pretty (BVMemRepr w BigEndian) = text "bvbe" <+> text (show w)
|
||||
@ -260,7 +266,10 @@ instance TestEquality MemRepr where
|
||||
Nothing
|
||||
|
||||
instance HasRepr MemRepr TypeRepr where
|
||||
typeRepr (BVMemRepr w _) = BVTypeRepr (natMultiply n8 w)
|
||||
typeRepr (BVMemRepr w _) =
|
||||
let r = (natMultiply n8 w)
|
||||
in case leqMulPos (Proxy :: Proxy 8) w of
|
||||
LeqProof -> BVTypeRepr r
|
||||
|
||||
-- | The right hand side of an assignment is an expression that
|
||||
-- returns a value.
|
||||
@ -270,8 +279,7 @@ data AssignRhs (arch :: *) ids tp where
|
||||
-> AssignRhs arch ids tp
|
||||
|
||||
-- An expression with an undefined value.
|
||||
SetUndefined :: (tp ~ BVType n)
|
||||
=> !(NatRepr n) -- Width of undefined value.
|
||||
SetUndefined :: !(TypeRepr tp)
|
||||
-> AssignRhs arch ids tp
|
||||
|
||||
-- Read memory at given location.
|
||||
@ -291,7 +299,7 @@ instance HasRepr (AssignRhs arch ids) TypeRepr where
|
||||
typeRepr rhs =
|
||||
case rhs of
|
||||
EvalApp a -> typeRepr a
|
||||
SetUndefined w -> BVTypeRepr w
|
||||
SetUndefined tp -> tp
|
||||
ReadMem _ tp -> typeRepr tp
|
||||
EvalArchFn _ rtp -> rtp
|
||||
|
||||
@ -299,6 +307,7 @@ instance ( HasRepr (ArchReg arch) TypeRepr
|
||||
)
|
||||
=> HasRepr (Value arch ids) TypeRepr where
|
||||
|
||||
typeRepr (BoolValue _) = BoolTypeRepr
|
||||
typeRepr (BVValue w _) = BVTypeRepr w
|
||||
typeRepr (RelocatableValue w _) = BVTypeRepr w
|
||||
typeRepr (AssignedValue a) = typeRepr (assignRhs a)
|
||||
@ -316,6 +325,11 @@ valueWidth v =
|
||||
|
||||
instance OrdF (ArchReg arch)
|
||||
=> OrdF (Value arch ids) where
|
||||
|
||||
compareF (BoolValue x) (BoolValue y) = fromOrdering (compare x y)
|
||||
compareF BoolValue{} _ = LTF
|
||||
compareF _ BoolValue{} = GTF
|
||||
|
||||
compareF (BVValue wx vx) (BVValue wy vy) =
|
||||
case compareF wx wy of
|
||||
LTF -> LTF
|
||||
@ -324,6 +338,7 @@ instance OrdF (ArchReg arch)
|
||||
compareF BVValue{} _ = LTF
|
||||
compareF _ BVValue{} = GTF
|
||||
|
||||
|
||||
compareF (RelocatableValue _ x) (RelocatableValue _ y) =
|
||||
fromOrdering (compare x y)
|
||||
compareF RelocatableValue{} _ = LTF
|
||||
@ -359,11 +374,11 @@ instance OrdF (ArchReg arch)
|
||||
------------------------------------------------------------------------
|
||||
-- Value operations
|
||||
|
||||
mkLit :: NatRepr n -> Integer -> Value arch ids (BVType n)
|
||||
mkLit :: (1 <= n) => NatRepr n -> Integer -> Value arch ids (BVType n)
|
||||
mkLit n v = BVValue n (v .&. mask)
|
||||
where mask = maxUnsigned n
|
||||
|
||||
bvValue :: KnownNat n => Integer -> Value arch ids (BVType n)
|
||||
bvValue :: (KnownNat n, 1 <= n) => Integer -> Value arch ids (BVType n)
|
||||
bvValue i = mkLit knownNat i
|
||||
|
||||
valueAsApp :: Value arch ids tp -> Maybe (App (Value arch ids) tp)
|
||||
@ -509,6 +524,7 @@ ppLit w i
|
||||
|
||||
-- | Pretty print a value.
|
||||
ppValue :: ShowF (ArchReg arch) => Prec -> Value arch ids tp -> Doc
|
||||
ppValue _ (BoolValue b) = text $ if b then "true" else "false"
|
||||
ppValue p (BVValue w i) = assert (i >= 0) $ parenIf (p > colonPrec) $ ppLit w i
|
||||
ppValue p (RelocatableValue _ a) = parenIf (p > plusPrec) $ text (show a)
|
||||
ppValue _ (AssignedValue a) = ppAssignId (assignId a)
|
||||
@ -542,7 +558,7 @@ ppAssignRhs :: (Applicative m, ArchConstraints arch)
|
||||
-> AssignRhs arch ids tp
|
||||
-> m Doc
|
||||
ppAssignRhs pp (EvalApp a) = ppAppA pp a
|
||||
ppAssignRhs _ (SetUndefined w) = pure $ text "undef ::" <+> brackets (text (show w))
|
||||
ppAssignRhs _ (SetUndefined tp) = pure $ text "undef ::" <+> brackets (text (show tp))
|
||||
ppAssignRhs pp (ReadMem a repr) =
|
||||
(\d -> text "read_mem" <+> d <+> PP.parens (pretty repr)) <$> pp a
|
||||
ppAssignRhs pp (EvalArchFn f _) = ppArchFn pp f
|
||||
|
||||
@ -90,6 +90,7 @@ addAssignmentDemands a = do
|
||||
addValueDemands :: Value arch ids tp -> DemandComp arch ids ()
|
||||
addValueDemands v = do
|
||||
case v of
|
||||
BoolValue{} -> pure ()
|
||||
BVValue{} -> pure ()
|
||||
RelocatableValue{} -> pure ()
|
||||
AssignedValue a -> addAssignmentDemands a
|
||||
|
||||
@ -118,13 +118,6 @@ addBinding srcId val = Rewriter $ do
|
||||
fail $ "Assignment " ++ show srcId ++ " is already bound."
|
||||
srcAssignedValues .= MapF.insert srcId val m
|
||||
|
||||
asApp :: Value arch tgt tp -> Maybe (App (Value arch tgt) tp)
|
||||
asApp (AssignedValue a) =
|
||||
case assignRhs a of
|
||||
EvalApp app -> Just app
|
||||
_ -> Nothing
|
||||
asApp _ = Nothing
|
||||
|
||||
-- | Return true if values are identical
|
||||
identValue :: TestEquality (ArchReg arch) => Value arch tgt tp -> Value arch tgt tp -> Bool
|
||||
identValue (BVValue _ x) (BVValue _ y) = x == y
|
||||
@ -134,16 +127,15 @@ identValue (Initial x) (Initial y) | Just Refl <- testEquality x y = True
|
||||
identValue _ _ = False
|
||||
|
||||
boolLitValue :: Bool -> Value arch ids BoolType
|
||||
boolLitValue True = BVValue n1 1
|
||||
boolLitValue False = BVValue n1 0
|
||||
boolLitValue = BoolValue
|
||||
|
||||
rewriteApp :: App (Value arch tgt) tp -> Rewriter arch src tgt (Value arch tgt tp)
|
||||
rewriteApp app = do
|
||||
ctx <- Rewriter $ gets rwContext
|
||||
rwctxConstraints ctx $ do
|
||||
case app of
|
||||
Mux _ (BVValue _ c) t f -> do
|
||||
if c `testBit` 0 then
|
||||
Mux _ (BoolValue c) t f -> do
|
||||
if c then
|
||||
pure t
|
||||
else
|
||||
pure f
|
||||
@ -155,21 +147,21 @@ rewriteApp app = do
|
||||
UExt (BVValue _ x) w -> do
|
||||
pure $ BVValue w x
|
||||
|
||||
AndApp (BVValue _ xc) y -> do
|
||||
if xc `testBit` 0 then
|
||||
AndApp (BoolValue xc) y -> do
|
||||
if xc then
|
||||
pure y
|
||||
else
|
||||
pure (BVValue n1 0)
|
||||
AndApp x y@BVValue{} -> rewriteApp (AndApp y x)
|
||||
pure (BoolValue False)
|
||||
AndApp x y@BoolValue{} -> rewriteApp (AndApp y x)
|
||||
|
||||
OrApp (BVValue _ xc) y -> do
|
||||
if xc `testBit` 0 then
|
||||
pure (BVValue n1 1)
|
||||
OrApp (BoolValue xc) y -> do
|
||||
if xc then
|
||||
pure (BoolValue True)
|
||||
else
|
||||
pure y
|
||||
OrApp x y@BVValue{} -> rewriteApp (OrApp y x)
|
||||
NotApp (BVValue _ xc) ->
|
||||
pure $ boolLitValue (not (xc `testBit` 0))
|
||||
OrApp x y@BoolValue{} -> rewriteApp (OrApp y x)
|
||||
NotApp (BoolValue b) ->
|
||||
pure $ boolLitValue (not b)
|
||||
|
||||
BVAdd _ x (BVValue _ 0) -> do
|
||||
pure x
|
||||
@ -179,13 +171,13 @@ rewriteApp app = do
|
||||
BVAdd w (BVValue _ x) y -> do
|
||||
rewriteApp (BVAdd w y (BVValue w x))
|
||||
-- (x + yc) + zc -> x + (yc + zc)
|
||||
BVAdd w (asApp -> Just (BVAdd _ x (BVValue _ yc))) (BVValue _ zc) -> do
|
||||
BVAdd w (valueAsApp -> Just (BVAdd _ x (BVValue _ yc))) (BVValue _ zc) -> do
|
||||
rewriteApp (BVAdd w x (BVValue w (toUnsigned w (yc + zc))))
|
||||
-- (x - yc) + zc -> x + (zc - yc)
|
||||
BVAdd w (asApp -> Just (BVSub _ x (BVValue _ yc))) (BVValue _ zc) -> do
|
||||
BVAdd w (valueAsApp -> Just (BVSub _ x (BVValue _ yc))) (BVValue _ zc) -> do
|
||||
rewriteApp (BVAdd w x (BVValue w (toUnsigned w (zc - yc))))
|
||||
-- (xc - y) + zc => (xc + zc) - y
|
||||
BVAdd w (asApp -> Just (BVSub _ (BVValue _ xc) y)) (BVValue _ zc) -> do
|
||||
BVAdd w (valueAsApp -> Just (BVSub _ (BVValue _ xc) y)) (BVValue _ zc) -> do
|
||||
rewriteApp (BVSub w (BVValue w (toUnsigned w (xc + zc))) y)
|
||||
|
||||
-- x - yc = x + (negate yc)
|
||||
@ -209,18 +201,16 @@ rewriteApp app = do
|
||||
BVTestBit (BVValue xw xc) (BVValue _ ic) | ic < min (natValue xw) (toInteger (maxBound :: Int)) -> do
|
||||
let v = xc `testBit` fromInteger ic
|
||||
pure $! boolLitValue v
|
||||
BVTestBit x (BVValue _ 0) | Just Refl <- testEquality (typeWidth x) n1 -> do
|
||||
pure x
|
||||
BVTestBit (asApp -> Just (UExt x _)) i@(BVValue _ ic) -> do
|
||||
BVTestBit (valueAsApp -> Just (UExt x _)) i@(BVValue _ ic) -> do
|
||||
let xw = typeWidth x
|
||||
if ic < natValue xw then
|
||||
rewriteApp (BVTestBit x i)
|
||||
else
|
||||
pure (BVValue n1 0)
|
||||
BVTestBit (asApp -> Just (BVXor _ x y@BVValue{})) i -> do
|
||||
pure (BoolValue False)
|
||||
BVTestBit (valueAsApp -> Just (BVXor _ x y@BVValue{})) i -> do
|
||||
xb <- rewriteApp (BVTestBit x i)
|
||||
yb <- rewriteApp (BVTestBit y i)
|
||||
rewriteApp (BVXor n1 xb yb)
|
||||
rewriteApp (XorApp xb yb)
|
||||
|
||||
BVComplement w (BVValue _ x) -> do
|
||||
pure (BVValue w (toUnsigned w (complement x)))
|
||||
@ -262,23 +252,35 @@ rewriteApp app = do
|
||||
let s = min y (natValue w)
|
||||
pure (BVValue w (toUnsigned w (toSigned w x `shiftR` fromInteger s)))
|
||||
|
||||
Eq (BoolValue x) (BoolValue y) -> do
|
||||
pure $! boolLitValue (x == y)
|
||||
|
||||
BVEq (BVValue _ x) (BVValue _ y) -> do
|
||||
Eq (BoolValue True) y -> do
|
||||
pure $! y
|
||||
Eq (BoolValue False) y -> do
|
||||
rewriteApp $ NotApp y
|
||||
|
||||
Eq x (BoolValue True) -> do
|
||||
pure $! x
|
||||
Eq x (BoolValue False) -> do
|
||||
rewriteApp $ NotApp x
|
||||
|
||||
Eq (BVValue _ x) (BVValue _ y) -> do
|
||||
pure $! boolLitValue (x == y)
|
||||
|
||||
-- Move constant to right hand side.
|
||||
BVEq x@BVValue{} y -> do
|
||||
rewriteApp (BVEq y x)
|
||||
Eq x@BVValue{} y -> do
|
||||
rewriteApp (Eq y x)
|
||||
|
||||
BVEq (asApp -> Just (BVAdd w x (BVValue _ o))) (BVValue _ yc) -> do
|
||||
rewriteApp (BVEq x (BVValue w (toUnsigned w (yc - o))))
|
||||
Eq (valueAsApp -> Just (BVAdd w x (BVValue _ o))) (BVValue _ yc) -> do
|
||||
rewriteApp (Eq x (BVValue w (toUnsigned w (yc - o))))
|
||||
|
||||
BVEq (asApp -> Just (UExt x _)) (BVValue _ yc) -> do
|
||||
Eq (valueAsApp -> Just (UExt x _)) (BVValue _ yc) -> do
|
||||
let u = typeWidth x
|
||||
if yc > maxUnsigned u then
|
||||
pure (BVValue n1 0)
|
||||
pure (BoolValue False)
|
||||
else
|
||||
rewriteApp (BVEq x (BVValue u (toUnsigned u yc)))
|
||||
rewriteApp (Eq x (BVValue u (toUnsigned u yc)))
|
||||
|
||||
_ -> evalRewrittenRhs (EvalApp app)
|
||||
|
||||
@ -299,6 +301,7 @@ rewriteAssignRhs rhs =
|
||||
rewriteValue :: Value arch src tp -> Rewriter arch src tgt (Value arch tgt tp)
|
||||
rewriteValue v =
|
||||
case v of
|
||||
BoolValue b -> pure (BoolValue b)
|
||||
BVValue w i -> pure (BVValue w i)
|
||||
RelocatableValue w a -> pure (RelocatableValue w a)
|
||||
AssignedValue (Assignment aid _) -> do
|
||||
|
||||
@ -5,6 +5,7 @@ Maintainer : Joe Hendrix <jhendrix@galois.com>
|
||||
This module provides a function for folding over the subexpressions in
|
||||
a value without revisiting shared subterms.
|
||||
-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
@ -73,6 +74,7 @@ foldValueCached litf rwf initf assignf = getStateMonadMonoid . go
|
||||
-> StateMonadMonoid (Map (Some (AssignId ids)) m) m
|
||||
go v =
|
||||
case v of
|
||||
BoolValue b -> return (litf (knownNat :: NatRepr 1) (if b then 1 else 0))
|
||||
BVValue sz i -> return $ litf sz i
|
||||
RelocatableValue w a -> pure $ rwf w a
|
||||
Initial r -> return $ initf r
|
||||
|
||||
@ -14,6 +14,7 @@ n-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Data.Macaw.Memory
|
||||
( Memory
|
||||
@ -190,7 +191,7 @@ instance Ord (MemWord w) where
|
||||
compare (MemWord x) (MemWord y) = compare x y
|
||||
|
||||
-- | Typeclass for legal memory widths
|
||||
class MemWidth w where
|
||||
class (1 <= w) => MemWidth w where
|
||||
-- | @addrWidthMod w@ returns @2^(8 * addrSize w - 1)@.
|
||||
addrWidthMod :: p w -> Word64
|
||||
|
||||
|
||||
@ -73,8 +73,10 @@ data Type
|
||||
| X86_80Float
|
||||
-- | 128 bit binary IEE754
|
||||
| QuadFloat
|
||||
-- | 16 bit binary IEE754
|
||||
-- | 16 bit binary IEE754
|
||||
| HalfFloat
|
||||
-- | A Boolean value
|
||||
| BoolType
|
||||
|
||||
-- Return number of bytes in the type.
|
||||
type family TypeBytes (tp :: Type) :: Nat where
|
||||
@ -101,31 +103,45 @@ type FloatType tp = BVType (8 * TypeBytes tp)
|
||||
|
||||
type BVType = 'BVType
|
||||
|
||||
type BoolType = BVType 1
|
||||
type BoolType = 'BoolType
|
||||
|
||||
-- | A runtime representation of @Type@ for case matching purposes.
|
||||
data TypeRepr (tp :: Type) where
|
||||
BVTypeRepr :: !(NatRepr n) -> TypeRepr (BVType n)
|
||||
BoolTypeRepr :: TypeRepr BoolType
|
||||
BVTypeRepr :: (1 <= n) => !(NatRepr n) -> TypeRepr (BVType n)
|
||||
|
||||
type_width :: TypeRepr (BVType n) -> NatRepr n
|
||||
type_width (BVTypeRepr n) = n
|
||||
|
||||
instance TestEquality TypeRepr where
|
||||
testEquality BoolTypeRepr BoolTypeRepr = do
|
||||
return Refl
|
||||
testEquality (BVTypeRepr m) (BVTypeRepr n) = do
|
||||
Refl <- testEquality m n
|
||||
return Refl
|
||||
testEquality _ _ = Nothing
|
||||
|
||||
instance OrdF TypeRepr where
|
||||
compareF BoolTypeRepr BoolTypeRepr = EQF
|
||||
compareF BoolTypeRepr _ = LTF
|
||||
compareF _ BoolTypeRepr = GTF
|
||||
compareF (BVTypeRepr m) (BVTypeRepr n) = do
|
||||
case compareF m n of
|
||||
LTF -> LTF
|
||||
EQF -> EQF
|
||||
GTF -> GTF
|
||||
|
||||
instance Show (TypeRepr tp) where
|
||||
show BoolTypeRepr = "bool"
|
||||
show (BVTypeRepr w) = "[" ++ show w ++ "]"
|
||||
|
||||
class KnownType tp where
|
||||
knownType :: TypeRepr tp
|
||||
|
||||
instance KnownNat n => KnownType (BVType n) where
|
||||
instance KnownType BoolType where
|
||||
knownType = BoolTypeRepr
|
||||
|
||||
instance (KnownNat n, 1 <= n) => KnownType (BVType n) where
|
||||
knownType = BVTypeRepr knownNat
|
||||
|
||||
------------------------------------------------------------------------
|
||||
@ -185,11 +201,36 @@ floatInfoBytes fir =
|
||||
QuadFloatRepr -> knownNat
|
||||
X86_80FloatRepr -> knownNat
|
||||
|
||||
floatInfoBytesIsPos :: FloatInfoRepr flt -> LeqProof 1 (TypeBytes flt)
|
||||
floatInfoBytesIsPos fir =
|
||||
case fir of
|
||||
HalfFloatRepr -> LeqProof
|
||||
SingleFloatRepr -> LeqProof
|
||||
DoubleFloatRepr -> LeqProof
|
||||
QuadFloatRepr -> LeqProof
|
||||
X86_80FloatRepr -> LeqProof
|
||||
|
||||
|
||||
floatInfoBits :: FloatInfoRepr flt -> NatRepr (8 * TypeBytes flt)
|
||||
floatInfoBits fir = natMultiply (knownNat :: NatRepr 8) (floatInfoBytes fir)
|
||||
|
||||
floatTypeRepr :: FloatInfoRepr flt -> TypeRepr (BVType (8 * TypeBytes flt))
|
||||
floatTypeRepr fir = BVTypeRepr (floatInfoBits fir)
|
||||
floatTypeRepr fir =
|
||||
case fir of
|
||||
HalfFloatRepr -> knownType
|
||||
SingleFloatRepr -> knownType
|
||||
DoubleFloatRepr -> knownType
|
||||
QuadFloatRepr -> knownType
|
||||
X86_80FloatRepr -> knownType
|
||||
|
||||
floatInfoBitsIsPos :: FloatInfoRepr flt -> LeqProof 1 (8 * TypeBytes flt)
|
||||
floatInfoBitsIsPos fir =
|
||||
case fir of
|
||||
HalfFloatRepr -> LeqProof
|
||||
SingleFloatRepr -> LeqProof
|
||||
DoubleFloatRepr -> LeqProof
|
||||
QuadFloatRepr -> LeqProof
|
||||
X86_80FloatRepr -> LeqProof
|
||||
|
||||
------------------------------------------------------------------------
|
||||
--
|
||||
|
||||
Loading…
Reference in New Issue
Block a user