diff --git a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs index c75af40e..bd941b6b 100644 --- a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs +++ b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs @@ -40,9 +40,10 @@ import qualified Data.Parameterized.TraversableFC as FC import qualified Dismantle.PPC as D import qualified Lang.Crucible.CFG.Extension as C import qualified Lang.Crucible.CFG.Reg as C -import qualified Lang.Crucible.Types as C -import qualified Lang.Crucible.Solver.Symbol as C +import qualified Lang.Crucible.Solver.BoolInterface as C import qualified Lang.Crucible.Solver.Interface as C +import qualified Lang.Crucible.Solver.Symbol as C +import qualified Lang.Crucible.Types as C import qualified Data.Macaw.CFG as MC import qualified Data.Macaw.Types as MT @@ -159,10 +160,13 @@ ppcGenStmt s = do s' <- TF.traverseF f s void (MS.evalArchStmt (PPCPrimStmt s')) -ppcGenTermStmt :: MP.PPCTermStmt ids +ppcGenTermStmt :: forall ppc ids s + . (MS.MacawArchStmtExtension ppc ~ PPCStmtExtension ppc) + => MP.PPCTermStmt ids -> MC.RegState (MP.PPCReg ppc) (MC.Value ppc ids) -> MS.CrucGen ppc ids s () -ppcGenTermStmt _ts _rs = error "ppcGenTermStmt is not yet implemented" +ppcGenTermStmt ts _rs = + void (MS.evalArchStmt (PPCPrimTerm ts)) data PPCStmtExtension ppc (f :: C.CrucibleType -> *) (ctp :: C.CrucibleType) where -- | Wrappers around the arch-specific functions in PowerPC; these are diff --git a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs index 5baa35f7..184febbe 100644 --- a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs +++ b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs @@ -26,12 +26,14 @@ import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.NatRepr as NR import Text.Printf ( printf ) +import qualified Lang.Crucible.LLVM.MemModel.Pointer as LL import qualified Lang.Crucible.Simulator.ExecutionTree as C import qualified Lang.Crucible.Simulator.RegMap as C -import qualified Lang.Crucible.Solver.Symbol as C +import qualified Lang.Crucible.Simulator.SimError as C +import qualified Lang.Crucible.Solver.BoolInterface as C import qualified Lang.Crucible.Solver.Interface as C +import qualified Lang.Crucible.Solver.Symbol as C import qualified Lang.Crucible.Types as C -import qualified Lang.Crucible.LLVM.MemModel.Pointer as LL import qualified Data.Macaw.CFG as MC import qualified Data.Macaw.Types as MT @@ -63,14 +65,49 @@ termSemantics :: (C.IsSymInterface sym, 1 <= MC.ArchAddrWidth ppc) -> MP.PPCTermStmt ids -> S ppc sym rtp bs r ctx -> IO (C.RegValue sym C.UnitType, S ppc sym rtp bs r ctx) -termSemantics = error "Terminator statement semantics not yet implemented" +termSemantics = error "PowerPC-specific terminator statement semantics not yet implemented" stmtSemantics :: (C.IsSymInterface sym, 1 <= MC.ArchAddrWidth ppc) => SymFuns ppc sym -> MP.PPCStmt ppc (A.AtomWrapper (C.RegEntry sym)) -> S ppc sym rtp bs r ctx -> IO (C.RegValue sym C.UnitType, S ppc sym rtp bs r ctx) -stmtSemantics = error "Statement semantics not yet implemented" +stmtSemantics _sf stmt s = + case stmt of + MP.Attn -> do + let reason = C.GenericSimError "ppc_attn" + C.addFailedAssertion (C.stateSymInterface s) reason + -- These are cache hints that can't be observed in our current memory model + -- (i.e., they require concurrency to be observed). + -- + -- Some take memory addresses as arguments. We don't actually touch those + -- addresses here, as they might not be valid (the instructions don't fault + -- on invalid addresses). + MP.Sync -> return ((), s) + MP.Isync -> return ((), s) + MP.Dcba {} -> return ((), s) + MP.Dcbf {} -> return ((), s) + MP.Dcbi {} -> return ((), s) + MP.Dcbst {} -> return ((), s) + MP.Dcbz {} -> return ((), s) + MP.Dcbzl {} -> return ((), s) + MP.Dcbt {} -> return ((), s) + MP.Dcbtst {} -> return ((), s) + MP.Icbi {} -> return ((), s) + MP.Icbt {} -> return ((), s) + -- These are transactional memory instructions. These also can't really + -- fail without concurrency, so we don't have them do anything. FIXME: That + -- might not be entirely correct - there could be some interesting side + -- effects that need to be captured somehow. We could, for example, model + -- Tcheck as both failing and succeeding to explore both paths. + MP.Tabort {} -> return ((), s) + MP.Tabortdc {} -> return ((), s) + MP.Tabortdci {} -> return ((), s) + MP.Tabortwc {} -> return ((), s) + MP.Tabortwci {} -> return ((), s) + MP.Tbegin {} -> return ((), s) + MP.Tcheck {} -> return ((), s) + MP.Tend {} -> return ((), s) funcSemantics :: (C.IsSymInterface sym, MS.ToCrucibleType mt ~ t, 1 <= MC.ArchAddrWidth ppc) => SymFuns ppc sym @@ -83,12 +120,14 @@ funcSemantics sf pf s = let sym = C.stateSymInterface s lhs' <- toValBV sym lhs rhs' <- toValBV sym rhs + -- FIXME: Make sure that the semantics when rhs == 0 exactly match PowerPC. v <- LL.llvmPointer_bv sym =<< C.bvUdiv sym lhs' rhs' return (v, s) MP.SDiv _rep lhs rhs -> do let sym = C.stateSymInterface s lhs' <- toValBV sym lhs rhs' <- toValBV sym rhs + -- FIXME: Make sure that the semantics when rhs == 0 exactly match PowerPC. v <- LL.llvmPointer_bv sym =<< C.bvSdiv sym lhs' rhs' return (v, s) MP.FP1 name v fpscr -> do @@ -191,5 +230,4 @@ toValBV :: (C.IsSymInterface sym) -> IO (C.RegValue sym (C.BVType w)) toValBV sym (A.AtomWrapper x) = LL.projectLLVM_bv sym (C.regValue x) -type S ppc sym rtp bs r ctx = C.CrucibleState MS.MacawSimulatorState sym (MS.MacawExt ppc) rtp bs r ctx - +type S ppc sym rtp bs r ctx = C.CrucibleState (MS.MacawSimulatorState sym) sym (MS.MacawExt ppc) rtp bs r ctx