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

Whitespace only

Browse Source
This commit is contained in:
Ryan Scott 2023-08-08 16:01:26 -04:00 committed by Ryan Scott
parent 21e3b8f461
commit 2ce038c086
2 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
View File

@ -84,7 +84,7 @@ armNonceAppEval bvi nonceApp =
-- failure, undefined behavior and unpredictable behavior flags -- failure, undefined behavior and unpredictable behavior flags
-- are not used, and have been wrapped in the following 3 functions. -- are not used, and have been wrapped in the following 3 functions.
-- To save time, for now we can simply avoid translating them. -- To save time, for now we can simply avoid translating them.
"uf_update_assert" -> case args of "uf_update_assert" -> case args of
Ctx.Empty Ctx.:> _assertVar -> Just $ do Ctx.Empty Ctx.:> _assertVar -> Just $ do
--assertVarE <- addEltTH M.LittleEndian bvi assertVar --assertVarE <- addEltTH M.LittleEndian bvi assertVar
@ -372,7 +372,7 @@ armNonceAppEval bvi nonceApp =
appendStmt $ [| join (execWriteGPRs <$> $(refBinding gprs')) |] appendStmt $ [| join (execWriteGPRs <$> $(refBinding gprs')) |]
setEffectful setEffectful
liftQ [| return $ unitValue |] liftQ [| return $ unitValue |]
"uf_update_simds" "uf_update_simds"
| Ctx.Empty Ctx.:> simds <- args -> Just $ do | Ctx.Empty Ctx.:> simds <- args -> Just $ do
simds' <- addEltTH M.LittleEndian bvi simds simds' <- addEltTH M.LittleEndian bvi simds
@ -427,7 +427,7 @@ natReprFromIntTH i = [| knownNat :: M.NatRepr $(litT (numTyLit (fromIntegral i))
-- address (either a memory address, or a register number) and 'val' is the value -- address (either a memory address, or a register number) and 'val' is the value
-- to be written. -- to be written.
data WriteAction f w where data WriteAction f w where
-- | A single write action -- | A single write action
WriteAction :: forall f w WriteAction :: forall f w
. (1 <= w) . (1 <= w)
=> M.NatRepr w => M.NatRepr w
@ -840,7 +840,7 @@ armAppEvaluator endianness interps elt =
res <- liftQ $ tupE $ map varE nms res <- liftQ $ tupE $ map varE nms
return $ EagerBoundExp res return $ EagerBoundExp res
False -> return bnd False -> return bnd
fldBnd <- refField (Ctx.size reprs) idx bnd fldBnd <- refField (Ctx.size reprs) idx bnd
extractBound fldBnd extractBound fldBnd
WB.StructCtor _ (Ctx.Empty Ctx.:> e) -> Just $ do WB.StructCtor _ (Ctx.Empty Ctx.:> e) -> Just $ do
@ -851,8 +851,8 @@ armAppEvaluator endianness interps elt =
fldEs <- sequence $ FC.toListFC (addEltTH endianness interps) flds fldEs <- sequence $ FC.toListFC (addEltTH endianness interps) flds
case all isEager fldEs of case all isEager fldEs of
True -> liftQ $ [| return $(tupE (map refEager fldEs)) |] True -> liftQ $ [| return $(tupE (map refEager fldEs)) |]
False -> liftQ $ joinTuple (map refBinding fldEs) False -> liftQ $ joinTuple (map refBinding fldEs)
WB.BVSdiv w bv1 bv2 -> return $ do WB.BVSdiv w bv1 bv2 -> return $ do
e1 <- addEltTH endianness interps bv1 e1 <- addEltTH endianness interps bv1
e2 <- addEltTH endianness interps bv2 e2 <- addEltTH endianness interps bv2
@ -861,7 +861,7 @@ armAppEvaluator endianness interps elt =
e1 <- addEltTH endianness interps bv1 e1 <- addEltTH endianness interps bv1
e2 <- addEltTH endianness interps bv2 e2 <- addEltTH endianness interps bv2
liftQ [| G.addExpr =<< $(joinOp2 [| \e1E e2E -> addArchAssignment (URem $(natReprTH w) e1E e2E) |] e1 e2) |] liftQ [| G.addExpr =<< $(joinOp2 [| \e1E e2E -> addArchAssignment (URem $(natReprTH w) e1E e2E) |] e1 e2) |]
WB.BVSrem w bv1 bv2 -> return $ do WB.BVSrem w bv1 bv2 -> return $ do
e1 <- addEltTH endianness interps bv1 e1 <- addEltTH endianness interps bv1
e2 <- addEltTH endianness interps bv2 e2 <- addEltTH endianness interps bv2

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

@ -62,8 +62,8 @@ import qualified What4.Interface as SI
import qualified SemMC.Architecture.Location as L import qualified SemMC.Architecture.Location as L
data MacawSemMC t = MacawSemMC data MacawSemMC t = MacawSemMC
type Sym t fs = S.ExprBuilder t MacawSemMC fs type Sym t fs = S.ExprBuilder t MacawSemMC fs
data BoundVarInterpretations arch t fs = data BoundVarInterpretations arch t fs =
BoundVarInterpretations { locVars :: Map.MapF (SI.BoundVar (Sym t fs)) (L.Location arch) BoundVarInterpretations { locVars :: Map.MapF (SI.BoundVar (Sym t fs)) (L.Location arch)