GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-22 23:32:15 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of github.com:GaloisInc/macaw-semmc

Browse Source
This commit is contained in:
Kevin Quick 2019-02-08 14:37:54 -08:00
commit 9f46c9e60b
3 changed files with 13 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs
View File

@ -74,6 +74,7 @@ ppc64MacawSymbolicFns =
{ MSB.crucGenArchConstraints = \x -> x
, MSB.crucGenArchRegName = ppcRegName
, MSB.crucGenRegAssignment = ppcRegAssignment
, MSB.crucGenRegStructType = ppcRegStructType
, MSB.crucGenArchFn = ppcGenFn
, MSB.crucGenArchStmt = ppcGenStmt
, MSB.crucGenArchTermStmt = ppcGenTermStmt
@ -85,6 +86,7 @@ ppc32MacawSymbolicFns =
{ MSB.crucGenArchConstraints = \x -> x
, MSB.crucGenArchRegName = ppcRegName
, MSB.crucGenRegAssignment = ppcRegAssignment
, MSB.crucGenRegStructType = ppcRegStructType
, MSB.crucGenArchFn = ppcGenFn
, MSB.crucGenArchStmt = ppcGenStmt
, MSB.crucGenArchTermStmt = ppcGenTermStmt
@ -170,6 +172,12 @@ ppcRegAssignment =
Ctx.<++> (R.repeatAssign (MP.PPC_GP . D.GPR . fromIntegral) :: Ctx.Assignment (MP.PPCReg (MP.AnyPPC v)) (R.CtxRepeat 32 (MT.BVType (RegSize v))))
Ctx.<++> (R.repeatAssign (MP.PPC_FR . D.VSReg . fromIntegral) :: Ctx.Assignment (MP.PPCReg (MP.AnyPPC v)) (R.CtxRepeat 64 (MT.BVType 128)))
ppcRegStructType :: forall v
. ( MP.KnownVariant v )
=> C.TypeRepr (MS.ArchRegStruct (MP.AnyPPC v))
ppcRegStructType =
C.StructRepr (MS.typeCtxToCrucible $ FC.fmapFC MT.typeRepr ppcRegAssignment)
data PPCSymbolicException v = MissingRegisterInState (Some (MP.PPCReg (MP.AnyPPC v)))
deriving instance Show (PPCSymbolicException v)

6
macaw-ppc/src/Data/Macaw/PPC/Arch.hs
View File

@ -29,6 +29,7 @@ import GHC.TypeLits
import Control.Lens ( (^.) )
import Data.Bits
import Data.Coerce ( coerce )
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import Data.Parameterized.Classes ( OrdF, knownRepr )
import qualified Data.Parameterized.NatRepr as NR
@ -72,10 +73,7 @@ instance MC.PrettyF PPCTermStmt where
PPCTrap -> PP.text "ppc_trap"
rewriteTermStmt :: PPCTermStmt src -> Rewriter ppc s src tgt (PPCTermStmt tgt)
rewriteTermStmt s =
case s of
PPCSyscall -> pure PPCSyscall
PPCTrap -> pure PPCTrap
rewriteTermStmt s = pure (coerce s)
data PPCStmt ppc (v :: MT.Type -> *) where
Attn :: PPCStmt ppc v

7
macaw-semmc/src/Data/Macaw/SemMC/TH.hs
View File

@ -135,14 +135,13 @@ instructionMatcher ltr ena ae lib archSpecificMatcher formulas operandResultType
]
return (lam, fullDefs)
-- | Unimplemented instructions return Nothing here, which will be translated
-- into a TranslationError inside the generator.
unimplementedInstruction :: Q (Name, Dec)
unimplementedInstruction = do
fname <- newName "noMatch"
arg1Nm <- newName "unknownOpcode"
fdecl <- funD fname
[clause [varP arg1Nm]
(normalB [| error ("Unimplemented instruction: " ++ show $(varE arg1Nm)) |])
[]]
fdecl <- funD fname [clause [varP arg1Nm] (normalB [| Nothing |]) []]
return (fname, fdecl)