Tristan Ravitch
981b775c7c
Update submodules
2018-07-24 16:57:36 -07:00
Tristan Ravitch
7a512574dd
x86: Fix a bug in the BinaryLoader implementation
...
The binary loader for x86_64/ELF was adding all symbol values as code discovery
roots. We only want to add the addresses of code objects.
2018-07-09 17:26:42 -07:00
Tristan Ravitch
7e6dc9ee8c
arm: Relax the base version bounds for macaw-arm
2018-07-08 22:28:58 -07:00
Tristan Ravitch
3f7699d4b3
Merge branch 'master' of github.com:GaloisInc/macaw-semmc into HEAD
2018-07-08 21:53:14 -07:00
Tristan Ravitch
ebfae218a9
Include symbol values in the entry points list for x86 (when available)
2018-07-08 21:52:28 -07:00
Tristan Ravitch
eee1f4d7a0
Update the semmc submodule
...
This has some new semantics, including for the TD/TDI instructions, which fix
the tests.
2018-07-03 20:13:35 -07:00
Tristan Ravitch
aee4309c85
Merge branch 'master' of github.com:GaloisInc/macaw-semmc into HEAD
2018-07-03 17:53:41 -07:00
Tristan Ravitch
332e85b8b1
ppc: Implement semantics for TD and TDI
...
The semantics for these instructions cannot be represented in our semantics
language, as they have side effects (i.e., they trap). This currently means
that we have to implement their semantics by hand in macaw-ppc.
2018-07-03 17:44:40 -07:00
Tristan Ravitch
b417cec636
ppc: Update to the test_bit_dynamic changes in semmc-ppc
...
This splits test_bit_dynamic into a 32 bit case and a 64 bit case
2018-07-03 17:44:06 -07:00
Luke Maurer
b70231334a
Merge branch 'df'
2018-07-03 14:27:01 -07:00
Luke Maurer
3548613d3a
Merge branch 'df' of github.com:GaloisInc/macaw-semmc into df
2018-07-03 13:13:32 -07:00
Luke Maurer
6477e710d4
Use "df_" rather than "_df_" as prefix for defined functions
...
The underscore squelches potentially useful warnings, since if a defined
function isn't being used, something is indeed wrong.
2018-07-03 13:10:06 -07:00
Luke Maurer
2a6686375f
Update semmc
2018-07-03 12:24:34 -07:00
Luke Maurer
7232622bd8
Support defined functions in PPC32; use all defined functions in PPC
2018-07-03 12:24:34 -07:00
Luke Maurer
2b5adeb1c4
Support for defined functions in PPC64
2018-07-03 12:24:34 -07:00
Luke Maurer
47d9d61998
Remove now-unnecessary optimization flags
...
The spliced TH code has gotten small enough that running multiple
iterations of the simplifier isn't horrible.
2018-07-03 12:24:34 -07:00
Luke Maurer
40bc26f21f
Update semmc
2018-07-03 12:24:34 -07:00
Luke Maurer
3a44feda6a
Whitespace error
2018-07-03 12:23:36 -07:00
Luke Maurer
eaca69e13b
Use defined functions to generate TH for ARM
2018-07-03 12:23:36 -07:00
Luke Maurer
f6e58bbd47
Support defined functions in TH
2018-07-03 12:23:36 -07:00
Tristan Ravitch
a8caa0985d
Submodule updates
2018-07-02 20:54:53 -07:00
Luke Maurer
26519002ab
Update semmc
2018-06-29 11:00:42 -07:00
Luke Maurer
fedf457e02
Support defined functions in PPC32; use all defined functions in PPC
2018-06-29 10:53:48 -07:00
Luke Maurer
33a4805b01
Support for defined functions in PPC64
2018-06-28 15:44:06 -07:00
Luke Maurer
c8f4146e1f
Remove now-unnecessary optimization flags
...
The spliced TH code has gotten small enough that running multiple
iterations of the simplifier isn't horrible.
2018-06-28 13:38:04 -07:00
Luke Maurer
633df42860
Enable caching in What4 expression builder
...
With caching disabled, we weren't doing any sharing recovery when
emitting Template Haskell. The cache in the `MacawQ` monad wasn't
helping because the expression builder generates a fresh nonce for each
expression it doesn't find in the cache; with no cache, every
subexpression was distinct from every other one.
2018-06-28 11:11:02 -07:00
Luke Maurer
bc9fb08f6f
Update semmc
2018-06-28 10:12:23 -07:00
Luke Maurer
457c8cec2e
Enable caching in What4 expression builder
2018-06-28 10:12:04 -07:00
Luke Maurer
0b37eff77e
Whitespace error
2018-06-26 11:35:50 -07:00
Luke Maurer
d3c40eb308
Use defined functions to generate TH for ARM
2018-06-26 11:04:29 -07:00
Luke Maurer
fbdae275cb
Support defined functions in TH
2018-06-26 11:04:07 -07:00
Tristan Ravitch
cad178cd62
ppc: Fix identifyReturn
...
Some recent semantics fixes broke a fragile pattern in identifyReturn; there is
now an extra shiftR.
2018-06-14 14:57:32 -07:00
Daniel Wagner
04e867bf4b
future-proof alignment detection
2018-06-12 14:18:19 -04:00
Daniel Wagner
082e024b55
bump deps
2018-06-11 13:13:11 -04:00
Daniel Wagner
9874e6db20
IP alignment rulesfor PPC
2018-06-11 10:36:18 -04:00
Daniel Wagner
9e8279e70c
fix alignment detection to match updated extract definition
2018-06-08 11:50:36 -04:00
Daniel Wagner
b7ec429874
add alignment information for PPC64
2018-06-01 15:35:41 -04:00
Daniel Wagner
989eb30a85
bump macaw dep
2018-06-01 15:35:41 -04:00
Ben Selfridge
6a5524e464
Fixed macaw-arm bound variable for UF bug
2018-06-01 10:23:34 -07:00
Ben Selfridge
2427ddf048
fixed stack and used Data.Functor.Product instead of hand-rolled type
2018-05-24 14:09:49 -07:00
Kevin Quick
138db42d15
[arm] Remove unneeded import.
2018-05-22 13:18:31 -07:00
Kevin Quick
30296f081c
[arm] Update for semmc renaming from ARM to AArch32.
2018-05-22 13:18:05 -07:00
Tristan Ravitch
4ca53dfb5c
Submodule updates
...
The code was already updated, but there were some missing submodule updates
2018-05-21 17:53:10 -07:00
Tristan Ravitch
b15f360d25
Documentation updates
2018-05-21 17:53:01 -07:00
Tristan Ravitch
9664914923
Update the PowerPC tests to deal with the latest macaw-semmc changes
...
The new binary loading interface does manage to simplify things
2018-05-21 14:32:29 -07:00
Tristan Ravitch
7cbd23dbf8
Add a generic interface for finding the entry points of a binary
...
Includes implementations for x86 and PowerPC 64/32
2018-05-20 21:41:21 -07:00
Tristan Ravitch
796e8bc29e
ppc: Generalize some error handling around the TOC
2018-05-18 19:31:18 -07:00
Tristan Ravitch
d6c2446a00
Whitespace
2018-05-18 17:52:18 -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
Tristan Ravitch
c4118b9fff
Clean up the TOC function implementation
2018-05-18 17:50:02 -07:00
