GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-02 10:54:04 +03:00
Code Issues Projects Releases Wiki Activity
1,873 Commits 50 Branches 0 Tags 13 MiB
ceb64be843
Commit Graph

319 Commits

Author SHA1 Message Date
Andrei Stefanescu
313b2a738a Add parameters and return type to subprogram datatype 2018-06-26 10:58:43 -07:00
Joe Hendrix
0fc925f989
Update for elf-edit compat 2018-06-15 08:24:52 -07:00
Joe Hendrix
6391a87db1
Merge branch 'master' of github.com:GaloisInc/macaw 2018-06-12 16:20:55 -07:00
Daniel Wagner
f4d4e381b7 have a way to align potentially misaligned IPs 2018-06-11 10:30:32 -04:00
Daniel Wagner
7251bb6b03 MOAR REWRITES 2018-06-11 10:30:32 -04:00
Daniel Wagner
a9d49a96ed don't turn sext into uext 2018-06-11 10:30:32 -04:00
Daniel Wagner
b5c143418d rewrite trunc.sext and trunc.uext 2018-06-11 10:30:32 -04:00
Joe Hendrix
494f6c176d
Updates to Macaw. 2018-06-06 11:48:45 -07:00
Joe Hendrix
77627c391d
Remove redundant IPAlignment constraint. 2018-06-06 11:28:26 -07:00
Daniel Wagner
e3d7c26b8c minor improvement to jump bounds abstract interpretation 2018-05-30 15:50:16 -04:00
Daniel Wagner
024e393e8e more rewrite rules for <= and < 2018-05-30 15:50:16 -04:00
Daniel Wagner
38aeecba21 add/improve rewrite rules for testing bits of shifted values 2018-05-30 15:50:16 -04:00
Daniel Wagner
917f921301 make JumpBounds abstract interpretation more precise 2018-05-30 15:50:16 -04:00
Daniel Wagner
d0566fe03b lay some groundwork for jump table detection on PPC 2018-05-30 15:50:16 -04:00
Daniel Wagner
3814d9c649 documentation fix 2018-05-30 15:50:16 -04:00
Daniel Wagner
5c9707508c rewrite away saturated shifts 2018-05-30 15:50:16 -04:00
Daniel Wagner
fa96a062e1 adding two finsets, get a finset 2018-05-30 15:50:16 -04:00
Ben Selfridge
0dddfcacea fixed haddock parse errors 2018-05-10 16:48:18 -07:00
Tristan Ravitch
0eb0bd14f7 Merge branch 'master' of github.com:GaloisInc/macaw into HEAD 2018-04-25 08:41:41 -07:00
Daniel Wagner
6453486013 delete some debugging print statements 2018-04-24 17:07:07 -04:00
Daniel Wagner
0565805c4f more principled error reporting in readMemReprDyn 2018-04-24 14:52:38 -04:00
Daniel Wagner
3b3bcecc4a handle jump tables again, including PIC tables 2018-04-24 14:52:38 -04:00
Tristan Ravitch
bd686c3c2e Merge branch 'master' of github.com:GaloisInc/macaw into HEAD 2018-04-24 09:07:39 -07:00
Joe Hendrix
9047cb41fb
Fix warnings in macaw-base; Fix errors in macaw-symbolic. 
This also makes some changes to eliminate a couple redundent
type-class constraints in CrucGen.hs which propagated to other changes.
 2018-04-24 01:17:03 -07:00
Tristan Ravitch
ee96681d8d Merge branch 'master' of github.com:GaloisInc/macaw into HEAD 2018-04-23 18:51:19 -07:00
Tristan Ravitch
8c20e0e156 Export another utility and type from Macaw.Memory 
This type is needed to write some type signatures, and we needed an accessor to
extract segment ranges from a SegmentContents.
 2018-04-23 18:50:39 -07:00
Joe Hendrix
052506f202
Remove PhaseHolderStmt. 2018-04-23 11:35:31 -07:00
Joe Hendrix
097edda1ef
Relocation support; various cleanups. 
This patch adds initial support for relocations in Macaw code
discovery, and adds other refactoring.

* It introduces a SymbolValue constructor to represent references to
  symbols within Macaw.
* The various cases for x86 mov are made explicit after the flexdis refactor
  broke the previous code.  We should now support segment register movs and
  give better error messages when seeing mov with control or debug registers.
* The generic exception operation is replaced with Hlt and UD2 terminal
  x86-specific statements.
* CodeAddrReason is split into FunctionExploreReason and BlockExploreReason to
  clarify whether a function or block was discovered.
* The Macaw pretty printer is changed to use write_mem in place of pointer syntax.
* Various other refactoring is made to clarify code.
 2018-04-23 11:24:21 -07:00
Joe Hendrix
0b8e95b0b0
Merge branch 'master' of github.com:GaloisInc/macaw 2018-04-17 16:02:28 -07:00
Brian Huffman
1e3fad7d77 Fix typo in module header description. 2018-04-16 10:07:23 -07:00
Joe Hendrix
2feebceddc
Refactor relocation support; support .rel and some object symbols. 2018-04-05 09:06:12 -07:00
Tristan Ravitch
2524b77cb5 base: Change the type of the address in the ArchState statement 
ArchMemAddr is easier to use than ArchAddrWord in downstream clients, and is
probably more faithful in the case where we want to support shared libraries
and/or object files.
 2018-03-30 10:33:49 -07:00
Tristan Ravitch
ce96c55896 Merge branch 'master' of github.com:GaloisInc/macaw into HEAD 2018-03-29 17:09:05 -07:00
Tristan Ravitch
51b8dae802 Change the pretty printing of the 'ArchState' macaw statement 2018-03-29 17:08:40 -07:00
Joe Hendrix
265f61e206
Merge branch 'master' of github.com:GaloisInc/macaw 2018-03-29 16:30:29 -07:00
Joe Hendrix
007405db1d
Improve robustness of elf loader, and start trying to parse relocations in objects. 2018-03-29 15:21:31 -07:00
Iavor Diatchki
8ac1a914ae Merge branch 'master' of github.com:GaloisInc/macaw 2018-03-29 12:42:24 -07:00
Iavor Diatchki
81f327e037 Add a function to find all symbols, not just functions. 
Joe is working on making this more generic in some way,
so this is just a quick (probably temporary) fix to expose
the needed functionality.
 2018-03-29 12:42:18 -07:00
Jason Dagit
372d7d7208 Add a new macaw statement to record updates to machine registers 
The new statement is called `ArchState`, and has two fields: an address and a
map.  The address is the address of the instruction it is standing in for.  The
map contains a mapping from the *machine registers* that the instruction updated
to the *macaw values* that were assigned to those locations.

This is useful metadata for debugging, but is also required to do some types of
architecture-independent analysis (where we can still reason about machine
register contents).
 2018-03-29 09:53:08 -07:00
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