GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-24 00:42:28 +03:00
Code Issues Projects Releases Wiki Activity

Nearly done with semmc -> macaw, need to complete a few more cases

Browse Source
This commit is contained in:
Ben Selfridge 2017-10-16 16:40:51 -07:00
parent e2121de437
commit 1a5946bd0d
2 changed files with 43 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
macaw-ppc/src/Data/Macaw/PPC/Operand.hs
View File

@ -1,5 +1,6 @@
{-# LANGUAGE DataKinds #-} {-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-} {-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ScopedTypeVariables #-}
@ -9,7 +10,9 @@
-- | Tools for extracting Macaw values from instruction operands -- | Tools for extracting Macaw values from instruction operands
module Data.Macaw.PPC.Operand ( module Data.Macaw.PPC.Operand (
ExtractValue, ExtractValue,
extractValue extractValue,
ToPPCReg,
toPPCReg
) where ) where
import GHC.TypeLits import GHC.TypeLits
@ -68,3 +71,15 @@ instance ExtractValue arch D.CRBitRC (BVType 5) where
instance ExtractValue arch D.CRRC (BVType 3) where instance ExtractValue arch D.CRRC (BVType 3) where
extractValue (D.CRRC b) = return $ MC.BVValue NR.knownNat (fromIntegral b) extractValue (D.CRRC b) = return $ MC.BVValue NR.knownNat (fromIntegral b)
class ToPPCReg a arch tp | a arch -> tp where
toPPCReg :: a -> R.PPCReg arch tp
instance ToPPCReg D.GPR PPC32.PPC (BVType 32) where
toPPCReg = R.PPC_GP
instance ToPPCReg D.GPR PPC64.PPC (BVType 64) where
toPPCReg = R.PPC_GP
instance ToPPCReg D.FR arch (BVType 128) where
toPPCReg = R.PPC_FR

42
macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs
View File

@ -165,7 +165,7 @@ genCaseBody :: forall a sh t arch
-> SL.ShapedList (FreeParamF Name) sh -> SL.ShapedList (FreeParamF Name) sh
-> Q Exp -> Q Exp
genCaseBody ipVarName opc semantics varNames = genCaseBody ipVarName opc semantics varNames =
translateFormula semantics (BoundVarInterpretations locVars opVars) translateFormula semantics (BoundVarInterpretations locVars opVars) varNames
where where
binders = ipVarName : FC.toListFC unFreeParamF varNames binders = ipVarName : FC.toListFC unFreeParamF varNames
@ -271,26 +271,26 @@ translateFormula :: forall arch t sh .
M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch) M.RegAddrWidth (PPCReg arch) ~ APPC.ArchRegWidth arch)
=> ParameterizedFormula (Sym t) arch sh => ParameterizedFormula (Sym t) arch sh
-> BoundVarInterpretations arch t -> BoundVarInterpretations arch t
-> SL.ShapedList (FreeParamF Name) sh
-> Q Exp -> Q Exp
translateFormula semantics bvInterps = do translateFormula semantics bvInterps varNames = do
let exps = map translateDefinition (Map.toList (pfDefs semantics)) let exps = map translateDefinition (Map.toList (pfDefs semantics))
[| Just (sequence_ $(listE exps)) |] [| Just (sequence_ $(listE exps)) |]
where translateDefinition :: Map.Pair (Parameter arch sh) (S.SymExpr (Sym t)) where translateDefinition :: Map.Pair (Parameter arch sh) (S.SymExpr (Sym t))
-> Q Exp -> Q Exp
translateDefinition (Map.Pair param expr) = do translateDefinition (Map.Pair param expr) = do
case param of case param of
OperandParameter w idx -> [| undefined |] OperandParameter w idx -> do
e <- addEltTH bvInterps expr
let FreeParamF name = varNames `SL.indexShapedList` idx
[| do val <- $(return e)
let reg = toPPCReg $(varE name)
curPPCState . M.boundValue reg .= val |]
LiteralParameter loc -> do LiteralParameter loc -> do
e <- addEltTH bvInterps expr e <- addEltTH bvInterps expr
reg <- locToRegTH (Proxy @arch) loc reg <- locToRegTH (Proxy @arch) loc
[| do val <- $(return e) [| do val <- $(return e)
curPPCState . M.boundValue $(return reg) .= val curPPCState . M.boundValue $(return reg) .= val |]
-- case c of
-- ValueExpr val -> curPPCState . M.boundValue $(return reg) .= val
-- AppExpr app -> do
-- assignment <- addAssignment (M.EvalApp app)
-- curPPCState . M.boundValue $(return reg) .= M.AssignedValue assignment
|]
FunctionParameter str operand w -> [| undefined |] FunctionParameter str operand w -> [| undefined |]
addEltTH :: forall arch t ctp . addEltTH :: forall arch t ctp .
@ -340,27 +340,27 @@ crucAppToExprTH elt bvInterps = case elt of
S.TrueBool -> [| return $ ValueExpr (M.BoolValue True) |] S.TrueBool -> [| return $ ValueExpr (M.BoolValue True) |]
S.FalseBool -> [| return $ ValueExpr (M.BoolValue False) |] S.FalseBool -> [| return $ ValueExpr (M.BoolValue False) |]
S.NotBool bool -> S.NotBool bool ->
[| AppExpr (M.NotApp <$> $(addEltTH bvInterps bool)) |] [| AppExpr <$> (M.NotApp <$> $(addEltTH bvInterps bool)) |]
S.AndBool bool1 bool2 -> S.AndBool bool1 bool2 ->
[| AppExpr (M.AndApp <$> $(addEltTH bvInterps bool1) <*> $(addEltTH bvInterps bool2)) |] [| AppExpr <$> (M.AndApp <$> $(addEltTH bvInterps bool1) <*> $(addEltTH bvInterps bool2)) |]
S.XorBool bool1 bool2 -> S.XorBool bool1 bool2 ->
[| AppExpr (M.XorApp <$> $(addEltTH bvInterps bool1) <*> $(addEltTH bvInterps bool2)) |] [| AppExpr <$> (M.XorApp <$> $(addEltTH bvInterps bool1) <*> $(addEltTH bvInterps bool2)) |]
S.IteBool test t f -> S.IteBool test t f ->
[| AppExpr (M.Mux M.BoolTypeRepr [| AppExpr <$> (M.Mux M.BoolTypeRepr
<$> $(addEltTH bvInterps test) <$> $(addEltTH bvInterps test)
<*> $(addEltTH bvInterps t) <*> $(addEltTH bvInterps t)
<*> $(addEltTH bvInterps f)) |] <*> $(addEltTH bvInterps f)) |]
S.BVIte w numBranches test t f -> S.BVIte w numBranches test t f ->
[| AppExpr (M.Mux (M.BVTypeRepr $(natReprTH w)) [| AppExpr <$> (M.Mux (M.BVTypeRepr $(natReprTH w))
<$> $(addEltTH bvInterps test) <$> $(addEltTH bvInterps test)
<*> $(addEltTH bvInterps t) <*> $(addEltTH bvInterps t)
<*> $(addEltTH bvInterps f)) |] <*> $(addEltTH bvInterps f)) |]
S.BVEq bv1 bv2 -> S.BVEq bv1 bv2 ->
[| AppExpr (M.Eq <$> $(addEltTH bvInterps bv1) <*> $(addEltTH bvInterps bv2)) |] [| AppExpr <$> (M.Eq <$> $(addEltTH bvInterps bv1) <*> $(addEltTH bvInterps bv2)) |]
S.BVSlt bv1 bv2 -> S.BVSlt bv1 bv2 ->
[| AppExpr (M.BVSignedLt <$> $(addEltTH bvInterps bv1) <*> $(addEltTH bvInterps bv2)) |] [| AppExpr <$> (M.BVSignedLt <$> $(addEltTH bvInterps bv1) <*> $(addEltTH bvInterps bv2)) |]
S.BVUlt bv1 bv2 -> S.BVUlt bv1 bv2 ->
[| AppExpr (M.BVUnsignedLt <$> $(addEltTH bvInterps bv1) <*> $(addEltTH bvInterps bv2)) |] [| AppExpr <$> (M.BVUnsignedLt <$> $(addEltTH bvInterps bv1) <*> $(addEltTH bvInterps bv2)) |]
S.BVConcat w bv1 bv2 -> do S.BVConcat w bv1 bv2 -> do
[| error "BVConcat" |] [| error "BVConcat" |]
-- [| AppExpr (M.BVUnsignedLt <$> $(addEltTH bvInterps bv1) <*> $(addEltTH bvInterps bv2)) |] -- [| AppExpr (M.BVUnsignedLt <$> $(addEltTH bvInterps bv1) <*> $(addEltTH bvInterps bv2)) |]
@ -396,10 +396,10 @@ crucAppToExprTH elt bvInterps = case elt of
-- Just Refl <- return $ testEquality n w -- Just Refl <- return $ testEquality n w
-- return $ ValueExpr bvVal -- return $ ValueExpr bvVal
S.BVNeg w bv -> do S.BVNeg w bv -> do
-- [| error "BVNeg" |] -- Note: This is still untested
[| do bvVal <- $(addEltTH bvInterps bv) [| do bvVal <- $(addEltTH bvInterps bv)
bvComp <- addExpr (AppExpr (M.BVComplement $(natReprTH w) bvVal)) bvComp <- addExpr (AppExpr (M.BVComplement $(natReprTH w) bvVal))
AppExpr <$> (M.BVAdd $(natReprTH w) bvComp (M.mkLit $(natReprTH w) 1)) |] return $ AppExpr (M.BVAdd $(natReprTH w) bvComp (M.mkLit $(natReprTH w) 1)) |]
-- bvVal <- addElt bv -- bvVal <- addElt bv
-- bvComp <- addExpr (AppExpr (M.BVComplement w bvVal)) -- bvComp <- addExpr (AppExpr (M.BVComplement w bvVal))
-- return $ AppExpr (M.BVAdd w bvComp (M.mkLit w 1)) -- return $ AppExpr (M.BVAdd w bvComp (M.mkLit w 1))
@ -439,7 +439,7 @@ crucAppToExprTH elt bvInterps = case elt of
S.BVTrunc w bv -> S.BVTrunc w bv ->
[| AppExpr <$> (M.Trunc <$> $(addEltTH bvInterps bv) <*> (pure $(natReprTH w))) |] [| AppExpr <$> (M.Trunc <$> $(addEltTH bvInterps bv) <*> (pure $(natReprTH w))) |]
S.BVBitNot w bv -> S.BVBitNot w bv ->
[| AppExpr <$> (M.BVComplement <$> $(addEltTH bvInterps bv) <*> (pure $(natReprTH w))) |] [| AppExpr <$> (M.BVComplement $(natReprTH w) <$> $(addEltTH bvInterps bv)) |]
S.BVBitAnd w bv1 bv2 -> S.BVBitAnd w bv1 bv2 ->
[| AppExpr <$> (M.BVAnd $(natReprTH w) [| AppExpr <$> (M.BVAnd $(natReprTH w)
<$> $(addEltTH bvInterps bv1) <$> $(addEltTH bvInterps bv1)