diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs index 9f2bd25d..8a00c003 100644 --- a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs +++ b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs @@ -84,7 +84,7 @@ armNonceAppEval bvi nonceApp = -- failure, undefined behavior and unpredictable behavior flags -- are not used, and have been wrapped in the following 3 functions. -- To save time, for now we can simply avoid translating them. - + "uf_update_assert" -> case args of Ctx.Empty Ctx.:> _assertVar -> Just $ do --assertVarE <- addEltTH M.LittleEndian bvi assertVar @@ -372,7 +372,7 @@ armNonceAppEval bvi nonceApp = appendStmt $ [| join (execWriteGPRs <$> $(refBinding gprs')) |] setEffectful liftQ [| return $ unitValue |] - + "uf_update_simds" | Ctx.Empty Ctx.:> simds <- args -> Just $ do 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 -- to be written. data WriteAction f w where - -- | A single write action + -- | A single write action WriteAction :: forall f w . (1 <= w) => M.NatRepr w @@ -840,7 +840,7 @@ armAppEvaluator endianness interps elt = res <- liftQ $ tupE $ map varE nms return $ EagerBoundExp res False -> return bnd - + fldBnd <- refField (Ctx.size reprs) idx bnd extractBound fldBnd WB.StructCtor _ (Ctx.Empty Ctx.:> e) -> Just $ do @@ -851,8 +851,8 @@ armAppEvaluator endianness interps elt = fldEs <- sequence $ FC.toListFC (addEltTH endianness interps) flds case all isEager fldEs of 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 e1 <- addEltTH endianness interps bv1 e2 <- addEltTH endianness interps bv2 @@ -861,7 +861,7 @@ armAppEvaluator endianness interps elt = e1 <- addEltTH endianness interps bv1 e2 <- addEltTH endianness interps bv2 liftQ [| G.addExpr =<< $(joinOp2 [| \e1E e2E -> addArchAssignment (URem $(natReprTH w) e1E e2E) |] e1 e2) |] - + WB.BVSrem w bv1 bv2 -> return $ do e1 <- addEltTH endianness interps bv1 e2 <- addEltTH endianness interps bv2 diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs index d82f6bf7..8b456d3c 100644 --- a/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs +++ b/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs @@ -62,8 +62,8 @@ import qualified What4.Interface as SI import qualified SemMC.Architecture.Location as L -data MacawSemMC t = MacawSemMC -type Sym t fs = S.ExprBuilder t MacawSemMC fs +data MacawSemMC t = MacawSemMC +type Sym t fs = S.ExprBuilder t MacawSemMC fs data BoundVarInterpretations arch t fs = BoundVarInterpretations { locVars :: Map.MapF (SI.BoundVar (Sym t fs)) (L.Location arch)