GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-27 16:15:12 +03:00
Code Issues Projects Releases Wiki Activity

[ppc-symbolic] Update Crucible IsSymInterface and simulator state.

Browse Source
This commit is contained in:
Kevin Quick 2018-05-07 15:59:05 -07:00
parent 7bab701643
commit dc79e6b636
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21
2 changed files with 7 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -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

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

@ -26,13 +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.Simulator.SimError 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 Lang.Crucible.LLVM.MemModel.Pointer as LL
import qualified Data.Macaw.CFG as MC
import qualified Data.Macaw.Types as MT
@ -229,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