Iavor Diatchki
1ea6792f28
Add special treatment for "aligning" pointers.
...
We don't really do anything with alignment, but sometime asm code
ands pointers to align them. For example `andq $(-64), %rsp`
aligns the pointer to a multiple of 64.
To support code like this we treat "and"-ing a pointer with a special
constant of the form 0xFFFF...FF000 (i.e., and alignment) as a subtracting
`0x0000...00XXX` where the `XXX` is symbolic.
This looses some information (i.e., we don't know that the result is aligned).
However, it is good enough for checking memory safety, as it covers
all possible results of the alignment.
2018-03-16 13:35:58 -07:00
Rob Dockins
4a4b9d7a8a
Minor update to track crucible API
2018-03-15 17:21:42 -07:00
Iavor Diatchki
f8dfc368c6
Allow reading from raw global addresses.
2018-03-14 17:20:22 -07:00
Iavor Diatchki
9c7070f8e6
Haddock comments fixes, thanks to Brian
2018-03-09 09:51:55 -08:00
Iavor Diatchki
89529ed7e3
Be more lenient when interpreting bogus expressions.
...
Previously we were asserting that some bogus-y things don't happen.
Unfortunately, these expressions can occur in code that was not
directly written by the user (e.g., comparisons for setting various
machine flags). To allow for that, we allow the expressions, but
give them undefined values. So the proof will succeed only if it
does not depend on the values of these bogus comparisons.
2018-03-07 10:22:46 -08:00
Iavor Diatchki
417c34429d
Add some support for function calls.
...
We basically punt, by passing-in a function to use as the implementation of
all functions. This function is supposed to look at the IP, and
decide what to do.
2018-03-05 16:29:15 -08:00
Iavor Diatchki
32710829f6
Use pointer addition, only when the value is not a bit-vector.
...
The other version was getting confusing by the NULL pointer.
2018-03-05 13:47:55 -08:00
Iavor Diatchki
4fa262a14c
Implement MacawFresh for booleans.
2018-03-05 13:47:21 -08:00
Iavor Diatchki
9094d1bd91
Improve failure message.
2018-03-01 14:36:24 -08:00
Iavor Diatchki
c69349e957
Add support for global memory regions.
2018-03-01 10:00:32 -08:00
Joe Hendrix
54038b5f20
Merge branch 'mem-model' of github.com:GaloisInc/macaw into mem-model
2018-02-26 12:44:07 -08:00
Joe Hendrix
fa6f74b583
Remove unused freshVarsForRegs
2018-02-26 12:42:08 -08:00
Iavor Diatchki
aac5a3e00f
Commit the bug fix.
2018-02-21 15:24:25 -08:00
Iavor Diatchki
e3f4e0875b
Bugfix and show more info when failing.
2018-02-21 15:06:18 -08:00
Iavor Diatchki
8bf523f8b1
Fill in imitted lemma
2018-02-21 09:47:53 -08:00
Joe Hendrix
0f6d030c86
Initialize variable for storing registers before use.
2018-02-19 12:48:59 -08:00
Iavor Diatchki
b8aa67918b
Assocaite global memory varaible name with its value.
2018-02-13 16:44:35 -08:00
Iavor Diatchki
470182dccb
Only pass around the memory var during execution, not CFG generation.
2018-02-13 10:14:22 -08:00
Iavor Diatchki
ad5f7ceddb
Add write operation
2018-02-12 10:28:39 -08:00
Iavor Diatchki
b57483b1f8
Start on writeMem
2018-02-09 16:59:42 -08:00
Iavor Diatchki
1c07b88ae7
Implement conditional read.
2018-02-09 15:30:06 -08:00
Iavor Diatchki
3c2fdeafe4
Implement reading from memory.
2018-02-09 14:13:39 -08:00
Iavor Diatchki
86c730043e
Cleanup pointer manipulation operations.
2018-02-09 11:41:39 -08:00
Iavor Diatchki
c7bb8d87c4
More memory model.
2018-02-08 16:49:42 -08:00
Iavor Diatchki
561d211972
Get started on integrating the LLVM memory model.
2018-02-06 16:47:13 -08:00
Joe Hendrix
e1e558239e
Minor cleanups.
2018-01-29 01:06:59 -08:00
Joe Hendrix
cfeabfde05
Minor cleanups.
2018-01-24 10:49:12 -08:00
Joe Hendrix
679108d73e
Merge branch 'master' of github.com:GaloisInc/macaw
2018-01-23 15:17:12 -08:00
Joe Hendrix
e94689bd7a
Continued macaw-symbolic progress.
2018-01-23 15:16:26 -08:00
Iavor Diatchki
8d4e940bb7
More simplifications; revert back to original.
...
It would appear that once the lifted wrapper functions were
in places, the types happen to match.
2018-01-23 15:09:38 -08:00
Iavor Diatchki
66ad7e521b
Define the traversableFC instance.
2018-01-23 14:30:29 -08:00
Joe Hendrix
d1bdff9866
Additional code for macaw-symbolic.
2018-01-22 16:58:33 -08:00
Joe Hendrix
365aa7fb39
Additional macaw-symbolic progress.
2018-01-22 16:38:17 -08:00
Joe Hendrix
8b97faa731
More progress on Macaw symbolic; compile fixes for Macaw changes.
2018-01-22 15:28:20 -08:00
Joe Hendrix
b7e06e64ee
Progress on macaw-symbolic and macaw-x86-symbolic.
2018-01-16 15:06:31 -08:00
Joe Hendrix
f6699b1b57
Port to use crucible syntax extensions.
2018-01-09 10:40:14 -08:00
Joe Hendrix
9530bf97bb
Update for crucible syntax-extensions.
2018-01-08 13:45:32 -08:00
Joe Hendrix
7ee4f6ef28
Start support for ParsedBlock.
2018-01-05 11:02:11 -08:00
Joe Hendrix
250c41d40b
Progrsss on symbolic and fixes to x86-support.
2018-01-03 13:18:13 -08:00
Joe Hendrix
cbcd835f48
Fix macaw-symbolic compilation bugs.
2018-01-02 22:26:17 -08:00
Joe Hendrix
deab99869d
Update for parameterized-utils compat.
2018-01-02 17:31:42 -08:00
Joe Hendrix
a15fc42ed4
Minor updates.
2017-12-21 15:42:33 -08:00
Joe Hendrix
478e7db31a
Refactor X86 semantics types; add tuples to Macaw.
2017-12-01 13:58:20 -08:00
Joe Hendrix
2bd710b49d
Move global function argument analysis to Macaw; Syscall changes
...
We also moved the syscall interface to be X86 specific to be compat
with earlier changes.
2017-11-22 14:07:55 -08:00
Joe Hendrix
9b2b95512d
Add support for memory "regions" to better support relocatable files.
2017-11-07 13:15:03 -08:00
Joe Hendrix
f34642e398
Fix macaw-symbolic to work with macaw-base changes.
2017-10-27 16:40:21 -07:00
Joe Hendrix
3f9e470b84
Fix macaw-symbolic compile error.
2017-10-17 14:09:48 -07:00
Joe Hendrix
135add62ae
Minor refactorings so ARM disassembler doesn't need MemSegmentOff.
2017-10-12 23:34:39 -07:00
Joe Hendrix
b17122e4c5
Fix macaw-symbolic compile error; add additional operands.
2017-10-06 14:35:22 -07:00
Joe Hendrix
dd7c817702
Modify BVTestBit to require arguments have same width.
2017-10-06 11:22:55 -07:00
Joe Hendrix
c77d1ac421
Remove generic quot/rem ops, and BoolMux; Refactor macaw-symbolic.
2017-10-02 14:40:14 -07:00
Joe Hendrix
7c33bf82e4
Update license information.
2017-09-27 15:59:06 -07:00
Joe Hendrix
0242a88fa6
Rename macaw to macaw-base and move directory.
2017-09-27 15:41:37 -07:00
