mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-28 10:08:13 +03:00
Implement NoStarIsType for GHC 8.6.
This commit is contained in:
parent
1d7cdc87eb
commit
3f77e763e9
@ -3,7 +3,7 @@ version: 0.0.1
|
||||
author: Galois, Inc.
|
||||
maintainer: jhendrix@galois.com
|
||||
build-type: Simple
|
||||
cabal-version: >= 1.9.2
|
||||
cabal-version: >= 1.10
|
||||
license: BSD3
|
||||
license-file: LICENSE
|
||||
|
||||
@ -20,6 +20,7 @@ library
|
||||
parameterized-utils,
|
||||
what4 >= 0.4
|
||||
hs-source-dirs: src
|
||||
default-language: Haskell2010
|
||||
|
||||
exposed-modules:
|
||||
Data.Macaw.X86.Symbolic
|
||||
@ -27,6 +28,8 @@ library
|
||||
|
||||
ghc-options: -Wall
|
||||
ghc-prof-options: -O2 -fprof-auto-top
|
||||
if impl(ghc >= 8.6)
|
||||
default-extensions: NoStarIsType
|
||||
|
||||
test-suite macaw-x86-symbolic-tests
|
||||
type: exitcode-stdio-1.0
|
||||
|
@ -34,9 +34,10 @@ module Data.Macaw.X86.Crucible
|
||||
|
||||
import Control.Lens ((^.))
|
||||
import Data.Bits hiding (xor)
|
||||
import Data.Kind ( Type )
|
||||
import Data.Parameterized.Context.Unsafe (empty,extend)
|
||||
import Data.Parameterized.Utils.Endian (Endian(..))
|
||||
import Data.Parameterized.NatRepr
|
||||
import Data.Parameterized.Utils.Endian (Endian(..))
|
||||
import qualified Data.Parameterized.Vector as PV
|
||||
import Data.Word (Word8)
|
||||
import GHC.TypeLits (KnownNat)
|
||||
@ -156,7 +157,7 @@ pureSem sym fn = do
|
||||
M.RepnzScas{} -> error "RepnzScas"
|
||||
M.X86IDiv {} -> error "X86IDiv"
|
||||
M.X86IRem {} -> error "X86IRem"
|
||||
M.X86Div {} -> error "X86Div"
|
||||
M.X86Div w n d -> error "X86Div"
|
||||
M.X86Rem {} -> error "X86Rem"
|
||||
M.X87_Extend{} -> error "X87_Extend"
|
||||
M.X87_FAdd{} -> error "X87_FAdd"
|
||||
@ -602,7 +603,7 @@ evalApp x = C.evalApp (symIface x) (symTys x) logger evalExt (evalE x)
|
||||
evalExt :: fun -> EmptyExprExtension f a -> IO (RegValue sym a)
|
||||
evalExt _ y = case y of {}
|
||||
|
||||
data E :: * -> CrucibleType -> * where
|
||||
data E :: Type -> CrucibleType -> Type where
|
||||
ValBool :: RegValue sym BoolType -> E sym BoolType
|
||||
ValBV :: (1 <= w) => NatRepr w -> RegValue sym (BVType w) -> E sym (BVType w)
|
||||
Expr :: App () (E sym) t -> E sym t
|
||||
@ -682,7 +683,7 @@ n128 = knownNat
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
newtype AtomWrapper (f :: CrucibleType -> *) (tp :: M.Type)
|
||||
newtype AtomWrapper (f :: CrucibleType -> Type) (tp :: M.Type)
|
||||
= AtomWrapper (f (ToCrucibleType tp))
|
||||
|
||||
liftAtomMap :: (forall s. f s -> g s) -> AtomWrapper f t -> AtomWrapper g t
|
||||
|
@ -29,6 +29,7 @@ module Data.Macaw.X86.Symbolic
|
||||
import Control.Lens ((^.),(%~),(&))
|
||||
import Control.Monad ( void )
|
||||
import Data.Functor.Identity (Identity(..))
|
||||
import Data.Kind
|
||||
import Data.Parameterized.Context as Ctx
|
||||
import Data.Parameterized.Map as MapF
|
||||
import Data.Parameterized.TraversableF
|
||||
@ -185,7 +186,7 @@ freshX86Reg sym r =
|
||||
|
||||
-- | We currently make a type like this, we could instead a generic
|
||||
-- X86PrimFn function
|
||||
data X86StmtExtension (f :: C.CrucibleType -> *) (ctp :: C.CrucibleType) where
|
||||
data X86StmtExtension (f :: C.CrucibleType -> Type) (ctp :: C.CrucibleType) where
|
||||
-- | To reduce clutter, but potentially increase clutter, we just make every
|
||||
-- Macaw X86PrimFn a Macaw-Crucible statement extension.
|
||||
X86PrimFn :: !(M.X86PrimFn (AtomWrapper f) t) ->
|
||||
|
Loading…
Reference in New Issue
Block a user