Tristan Ravitch
06f64078df
Wip/ppc no block labels ( #66 )
...
Update to API changes in macaw-base in macaw-ppc and macaw-arm
The "block label" abstraction (used during arch-specific disassembly) was removed some time ago in the base macaw library. This change updates macaw-ppc and macaw-arm to remove uses of block labels. The major change is that the disassembly function only returns a single block at a time instead of a sequence of blocks.
To facilitate this, the handling of the PowerPC conditional trap instruction (trap doubleword) is now an architecture-specific terminator instruction instead of encoding the logic of conditional trapping. We will now have to encode the conditional trapping logic in macaw-ppc-symbolic. Note that we have not done so yet.
This commit also updates the expected results of the PowerPC tests; the number of discovered blocks is different, but not significantly so. It is hard to tell if this is a regression or an improvement.
2019-08-09 16:11:59 -07:00
Kevin Quick
eb93bb4e3a
[ppc-symbolic] updates for crucible nonce change from (ST h) to IO
...
Changes for compatibility with Crucible pull request
285 (https://github.com/GaloisInc/crucible/pull/285 ) and the
corresponding changes in macaw symbolic.
2019-07-19 13:19:14 -07:00
Kevin Quick
9c5ebee0bc
Added ArchInfo lookupReg and updateReg for PPC.
2019-02-08 17:28:43 -08:00
Luke Maurer
7d720b74f6
Add new crucGenRegStructType to MacawSymbolicArchFunctions for PPC
2019-01-28 14:48:25 -08:00
Tristan Ravitch
cfcc1fc0d4
Update to the latest macaw-symbolic
...
There was some API churn, mostly a few renames and new modules.
2019-01-10 18:23:19 -08:00
Luke Maurer
aaa7a6cf85
Add new parameter to CrucGen monad
2019-01-03 12:13:55 -08:00
Luke Maurer
dbce1b1265
Refactor to use AnyPPC
2018-12-21 11:47:40 -08:00
Luke Maurer
b5a75832a3
Adapt to and re-export new AnyPPC arch constructor
2018-12-20 16:43:46 -08:00
Andrei Stefanescu
76ff48eec0
Propagate changes for X86_64 RepMovs and RepStos.
2018-11-27 10:31:03 -08:00
Andrei Stefanescu
1c002f160b
Minor fixes.
2018-09-18 21:56:17 -07:00
Andrei Stefanescu
32961d20cb
Use name instead of nonce id for uninterpreted functions.
2018-09-14 19:01:27 -07:00
Andrei Stefanescu
85ef5b4f0b
Add float le and float round.
2018-09-14 19:01:19 -07:00
Andrei Stefanescu
4b498807fd
Handle floating-point rounding.
2018-09-12 11:10:23 -07:00
Andrei Stefanescu
b0c98ccc5c
Use op name as argument instead of uninterpreted function name.
2018-09-06 14:47:37 -07:00
Andrei Stefanescu
f448a4ae9f
Add symbolic semantics to PPC floats.
2018-09-06 14:47:37 -07:00
Kevin Quick
932b3df9ff
[ppc-symbolic] Update LLVM memory model pointer import for newer crucible.
2018-08-27 15:25:37 -07:00
Tristan Ravitch
981b775c7c
Update submodules
2018-07-24 16:57:36 -07:00
Tristan Ravitch
84473060e3
Generalize the lookup/update register assignment utilities
...
Instead of having them return 'Maybe', use 'MonadThrow'
2018-05-18 17:50:22 -07:00
Kevin Quick
f81f2437ee
Update for crucible reorganization and new what4 module.
2018-05-18 08:33:58 -07:00
Tristan Ravitch
c943d45d21
ppc-symbolic: Export some more helpers
2018-05-15 18:41:04 -07:00
Tristan Ravitch
fd3ab9145a
ppc-symbolic: Generate term statements in the translation
2018-05-10 07:58:00 -04:00
Kevin Quick
dc79e6b636
[ppc-symbolic] Update Crucible IsSymInterface and simulator state.
2018-05-07 15:59:05 -07:00
Tristan Ravitch
7bab701643
ppc-symbolic: Implement semantics for the ppc-specific statements
...
Except for Attn, these are all no-ops since we don't have a concurrency model.
That could change later - we might want to model them as both failing and
succeeding in some cases (esp the transactional memory instructions).
2018-05-07 08:15:05 -07:00
Kevin Quick
1b401bbe94
[ppc-symbolic] Remove extraneous file.
2018-05-04 17:43:10 -07:00
Tristan Ravitch
78af7939b6
ppc-symbolic: Sketch out terminator handling and interpretation
2018-05-04 17:16:06 -07:00
Tristan Ravitch
df607d4044
ppc-symbolic: Translate macaw statements
...
Still need to translate terminal statements (esp. system call and trap)
2018-05-04 16:48:31 -07:00
Tristan Ravitch
6d7bb6f6e4
ppc-symbolic: Fill out the semantics for the arch-specific functions
2018-05-04 15:46:54 -07:00
Tristan Ravitch
6b3bf072cf
ppc-symbolic: Add more descriptive failures
2018-05-04 10:16:46 -07:00
Tristan Ravitch
1c97ca1314
ppc-symbolic: Implement the function evaluators
2018-05-04 10:15:25 -07:00
Tristan Ravitch
05c01beec0
Re-export newSymFuns from the top-level module
2018-05-04 09:32:13 -07:00
Tristan Ravitch
c3ba017fcc
Start macaw-ppc-symbolic
2018-05-03 16:41:33 -07:00
