Commit Graph

230 Commits

Author SHA1 Message Date
Tristan Ravitch
8d5e39c87f base: Add additional simplification rules to the rewriter 2018-03-27 18:13:46 -07:00
Tristan Ravitch
c2c5835b10 base: Add another case to the abstract interpretation
Now handle shifts of constants
2018-03-27 18:13:23 -07:00
Kevin Quick
594e9e025d
Restrict Semigroup imports to avoid collisions on unused definitions. 2018-03-27 10:43:04 -07:00
Kevin Quick
818f7a7767
Remove unused import in Macaw CFG Core. 2018-03-27 10:42:28 -07:00
Kevin Quick
377c3d1a2b
Use architecture-specific identifyReturn in Discovery process.
Instead of inline analysis of whether the instruction pointer has been
updated to contain the ReturnAddr symbolic value, defer the
determination of the call return to the (previously defined but
unused) architecture-specific handling.  This allows architectures
like ARM that perform modifications on the values loaded to the
instruction pointer (e.g. clearing lower bits) to provide their own
recognition of a return operation.

Also modifies the signature of identifyReturn to return a Sequence of
statements to match the identifyCall type signature.

Replaces the previously unused identifyX86Return with the inline
detection of IP == ReturnAddr.
2018-03-27 10:35:55 -07:00
Joe Hendrix
ceefa7ae75
Update memory to use explicit BSS region and disable includeBSS option. 2018-03-23 16:26:07 -07:00
Joe Hendrix
557408132c
Merge branch 'master' of github.com:GaloisInc/macaw 2018-03-23 14:13:09 -07:00
Aaron Tomb
e33ecf3e84 Fix build with GHC 8.4.1 2018-03-23 14:09:28 -07:00
Jason Dagit
e1ea0c8def Discovery: pretty instance for DiscoveryFunInfo now prints function address 2018-03-14 17:32:29 -07:00
Ben Davis
9b592c3285
Add exploreFnPred to DiscoveryState to optionally filter exploration 2018-03-02 08:39:49 -05:00
Kevin Quick
601b9def8c Merge branch 'master' of https://github.com/GaloisInc/macaw 2018-03-01 11:00:14 -08:00
Kevin Quick
e35acdcb19
Minor comment fixup. 2018-03-01 10:59:11 -08:00
Kevin Quick
84eb0a0a80 Revert "Add BVUrem App support."
This reverts commit 6a0a59e298.

Do not want to add BVUrem because divide by zero can cause an
exception and this will greatly increase the complexity for analysis.
2018-03-01 10:57:28 -08:00
Iavor Diatchki
da2a29b595 :Merge branch 'master' of github.com:GaloisInc/macaw 2018-03-01 10:00:41 -08:00
Iavor Diatchki
c69349e957 Add support for global memory regions. 2018-03-01 10:00:32 -08:00
Joe Hendrix
14ab6352f5
Export elfAddrWidth 2018-02-28 09:26:10 -08:00
Iavor Diatchki
2e21856afe Merge remote-tracking branch 'origin/master' into mem-model
# Conflicts:
#	base/src/Data/Macaw/Memory/ElfLoader.hs
2018-02-27 16:36:08 -08:00
Joe Hendrix
9c8d7921f8
Merge branch 'master' of github.com:GaloisInc/macaw 2018-02-26 13:18:15 -08:00
Joe Hendrix
027c355001
Remove reloc hack 2018-02-26 13:04:01 -08:00
Kevin Quick
6a0a59e298
Add BVUrem App support. 2018-02-21 20:39:57 -08:00
Joe Hendrix
cc2d09a07d
Use type synonym to clarify argument for including BSS. 2018-02-20 16:37:26 -08:00
Joe Hendrix
d8cc235368
Fix bug in loading Elf sections with no data. 2018-02-20 16:28:54 -08:00
Iavor Diatchki
6cafcdf254 More verbose failures. 2018-02-20 11:53:18 -08:00
Joe Hendrix
b20ab6664c
Provide additional control options for discovery. 2018-02-14 23:16:21 -08:00
Iavor Diatchki
c772eb31f4 Derive Show instance for Endianness 2018-02-09 14:12:57 -08:00
Joe Hendrix
526f8c5e6f
Move additional functions to discovery; extend loading options. 2018-02-07 14:50:53 -08:00
Joe Hendrix
dbba6dfad9
Merge branch 'master' into jhx-reloc-experiment
This also patches for elf-edit changes.
2018-01-30 15:15:20 -08:00
Joe Hendrix
197a0b3ed1
Add additional utilities and flexibility for loading elf files. 2018-01-29 18:18:39 -08:00
Joe Hendrix
7e144a51f4
Memory interface renamings. 2018-01-29 11:05:19 -08:00
Joe Hendrix
e1e558239e
Minor cleanups. 2018-01-29 01:06:59 -08:00
Joe Hendrix
ca7ab08124
Merge branch 'master' of github.com:GaloisInc/macaw 2018-01-29 00:22:54 -08:00
Joe Hendrix
cbbec5378c
Haddock improvements; some module reoganization. 2018-01-29 00:20:54 -08:00
Daniel Wagner
fbe716607f fix segment equality check 2018-01-26 14:09:01 -08:00
Daniel Wagner
fc76fd5dc0 split blocks when we discover a jump into their middle 2018-01-26 10:18:31 -08:00
Joe Hendrix
b3cd6fd049
Fix loop in X86 bvUle simplification. 2018-01-23 16:06:54 -08:00
Joe Hendrix
e94689bd7a
Continued macaw-symbolic progress. 2018-01-23 15:16:26 -08:00
Joe Hendrix
eda3c6412a
Fix error in resolving symbols. 2018-01-23 13:38:49 -08:00
Joe Hendrix
bedd8a6ab4
Introduce MemSymbol type so we can have common type for Elf and Mach-O symbols. 2018-01-21 18:21:09 -08:00
Joe Hendrix
278b079a49
Fix warnings; remove -Werror 2018-01-21 07:56:04 -08:00
Joe Hendrix
79b5606e3c
Merge remote-tracking branch 'origin/avx' 2018-01-16 15:38:14 -08:00
Joe Hendrix
b7e06e64ee
Progress on macaw-symbolic and macaw-x86-symbolic. 2018-01-16 15:06:31 -08:00
Tristan Ravitch
46a97a16b4 Fix a haddock parse bug 2018-01-08 22:50:53 -08:00
Joe Hendrix
b89f60bf2b
Replace SymbolAddrMap with AddrSymMap for better code reused in reopt. 2018-01-08 12:28:28 -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
Iavor Diatchki
70aaccb406 Merge remote-tracking branch 'origin/master' into avx
# Conflicts:
#	symbolic/src/Data/Macaw/Symbolic.hs
#	symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
#	symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
#	x86/src/Data/Macaw/X86/Getters.hs
2018-01-03 12:01:10 -08:00
Joe Hendrix
cbcd835f48
Fix macaw-symbolic compilation bugs. 2018-01-02 22:26:17 -08:00
Ben Davis
ebbca0aded
Hack: filter out known bad addresses from concretize abs ptrs 2017-12-23 10:51:11 -05:00
Joe Hendrix
a15fc42ed4
Minor updates. 2017-12-21 15:42:33 -08:00
Iavor Diatchki
1f2e80f1a5 Implement a couple of instructions 2017-12-18 16:53:27 -08:00
Ben Davis
c1b6b472ef
Generalize relocation code in ElfLoader for X86_64 and ARM32 2017-12-15 14:30:36 -05:00
Joe Hendrix
209c3c1aba
Elf-load symbol table information support non-absolute addresses. 2017-12-11 15:14:22 -08:00
Joe Hendrix
0c9efc984c
Revise parameterized-utils list cons. 2017-12-08 11:43:56 -08:00
Joe Hendrix
b9eda0a9b9
Use more parameterized-utils features. 2017-12-07 00:24:04 -08:00
Joe Hendrix
32b53b96b1
Migrate floating point code to architecture specific backends.
This should complete the transition so that all App values are total
functions, and functions with side effects are architecture-specific.
2017-12-06 16:58:33 -08:00
Joe Hendrix
4d5b90e285
Begin cleaning up floating point and x86-specific functions. 2017-12-05 13:31:12 -08:00
Joe Hendrix
be8e0cff26
Fiz tuple field to actually take tuple as argument. 2017-12-01 14:46:46 -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
e62b4e4e56
Add Show instance for MemRepr. 2017-11-20 15:05:13 -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
b99927f3b0
Fix issue in architecture-specific statement addresses. 2017-10-31 12:00:09 -07:00
Joe Hendrix
8e9b453189
Simplify demand computation. 2017-10-27 16:24:16 -07:00
Joe Hendrix
f7503f12a5
Generalize ArchStmt. 2017-10-27 15:57:36 -07:00
Joe Hendrix
4c67e08e21
Generalize semantics of architecture-specific term statement.
This also makes some small changes/improvments to the rewriter and
removes redundent argument from x86-backend.
2017-10-27 09:26:26 -07:00
Joe Hendrix
ac0a59674a
Export simplification functions. 2017-10-25 15:43:54 -07:00
Joe Hendrix
bcea135f2c
Export additional types from discovery. 2017-10-23 14:59:37 -07:00
Joe Hendrix
f29ffca628
Merge branch 'master' of github.com:GaloisInc/macaw 2017-10-23 13:57:14 -07:00
Joe Hendrix
16693d4a63
Generalize disassembler so that it can be used with ST RealWorld. 2017-10-23 13:55:58 -07:00
Tristan Ravitch
537bcceafa Add floating point negation to the App type 2017-10-18 13:41:12 -07:00
Tristan Ravitch
618857f21d Add a constructor to the App type for floating point absolute value 2017-10-18 11:17:00 -07:00
Joe Hendrix
5eaf2605ed
Add support for adc/sbb. 2017-10-17 11:50:23 -07:00
Joe Hendrix
135add62ae
Minor refactorings so ARM disassembler doesn't need MemSegmentOff. 2017-10-12 23:34:39 -07:00
Joe Hendrix
c95d3e7d0f
Cleanups to Macaw. 2017-10-10 11:38:28 -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
1cfe6cf08c
Update READMEs. 2017-09-27 16:12:44 -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