Commit Graph

33 Commits

Author SHA1 Message Date
Tristan Ravitch
02c2fcd96a
Clean up the PowerPC architecture specifications (#130)
This commit reduces duplication in the PowerPC backend.  Instances are now in terms of the generic `AnyPPC` type, rather than having separate instances for 32 and 64 bit.  Shuffling some type parameters also allows us to remove a large number of type equalities that e.g., fix the arch register type to `PPCReg`.
2020-04-19 11:56:42 -07:00
Daniel Wagner
97c9e20089 add memory model as type argument in a few places 2020-03-18 00:21:15 -04:00
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