Kevin Quick
8d020b18b8
Update (temporarily) to kquick branch of s-cargot with fast pretty-printing.
2018-02-16 13:48:16 -08:00
Kevin Quick
4a8a84ba9b
Add s-cargot-letbind submodule.
2018-02-16 13:40:41 -08:00
Kevin Quick
075a0f54e4
[arm] ExtractValue instances for Pred, SBit, and BranchExecuteTarget operands.
2018-02-07 11:38:04 -08:00
Kevin Quick
22bbdf7ee7
Common ExtractValue instances for sharing amongst architectures.
2018-02-07 11:34:38 -08:00
Kevin Quick
0ccba8974d
[arm] Initial nonce app eval, covering arm_is_r15
2018-02-02 16:49:56 -08:00
Kevin Quick
d5292afc76
[arm] add missing import for Operand support with genInstruction.
2018-02-02 16:46:47 -08:00
Kevin Quick
66ade6a20e
Merge branch 'master' of https://gitlab-ext.galois.com/macaw/macaw-semmc
2018-02-02 16:07:26 -08:00
Kevin Quick
4595a15cc3
[arm] Initial operand support with GP registers handled.
2018-02-02 16:06:52 -08:00
Kevin Quick
f6a0f7bc49
[arm] ARM uses the term PC (Program Counter) instead of IP (Instruction Ptr).
2018-02-02 15:57:02 -08:00
Kevin Quick
f4280134cc
[arm] Correct word size import for disassembly errors.
2018-02-02 15:48:01 -08:00
Ben Selfridge
7ec04d8d22
bump semmc
2018-02-01 12:07:09 -08:00
Ben Selfridge
372301aecc
s-cargot now under submodules
2018-01-31 16:44:16 -08:00
Ben Selfridge
674f08e668
bumped up-to-date dismantle and semmc
2018-01-31 15:19:57 -08:00
Ben Selfridge
146473e5bc
reconfigure stack.yaml for macaw-arm
2018-01-29 12:49:50 -08:00
Kevin Quick
5f77195513
Update dismantle version for semmc-arm needs.
2018-01-24 12:42:47 -08:00
Kevin Quick
55320831b4
[arm] Use error for TBD functions for runtime visible identification
2018-01-24 11:08:03 -08:00
Ben Selfridge
fda3d5af22
updated stack.yaml
2018-01-22 16:27:54 -08:00
Ben Selfridge
a66f3922c1
bumped semmc
2018-01-22 16:27:29 -08:00
Ben Selfridge
b3b5aca1e9
bumped semmc version
2018-01-22 13:51:32 -08:00
Tristan Ravitch
aaf2f67ea4
ppc: Add arch-specific statements for some icache instructions
2018-01-22 11:22:24 -08:00
Tristan Ravitch
71e3d868b8
Fix a bug in handling arch-specific statements
...
The system call instructions TRAP and SC were updating the IP twice, which led
to skipping instructions. The IP increment for these instructions was already
handled in the abstract interpretation of arch-specific terminators.
2018-01-22 10:34:52 -08:00
Tristan Ravitch
46333f1a09
Submodule updates
2018-01-22 10:26:20 -08:00
Tristan Ravitch
260ac399c6
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
2018-01-19 18:12:47 -08:00
Tristan Ravitch
37d6ca6732
Fix a bug where arch-specific statements weren't incrementing the IP
2018-01-19 18:12:15 -08:00
Ben Selfridge
7e47db94a3
Updated macaw-ppc to handle floating-point UFs
2018-01-17 12:54:30 -08:00
Kevin Quick
8229de9ff7
Merge branch 'master' into kwq/macaw-arm
2018-01-10 11:30:05 -08:00
Tristan Ravitch
2c1a2e9b97
Submodule updates
2018-01-09 16:54:56 -08:00
Ben Selfridge
69087e8835
update semmc
2018-01-09 14:02:51 -08:00
Ben Selfridge
6780e14c81
merging to newest semmc
2018-01-09 11:45:08 -08:00
Ben Selfridge
dc5659dc14
updated semmc
2018-01-09 11:37:17 -08:00
Ben Selfridge
f6face9136
Added VSCR for vector semantics
2018-01-08 17:56:00 -08:00
Tristan Ravitch
f256869311
Update crucible and parameterized-utils
2018-01-08 15:32:38 -08:00
Tristan Ravitch
77129fbe3e
Update the semmc submodule
2018-01-08 15:32:38 -08:00
Kevin Quick
7bc9b2c65b
[arm] Misc cleanup in ARM disassembly.
2018-01-08 13:40:57 -08:00
Kevin Quick
e48fcbd073
[arm] Initial support for abstract statement evaluation via semmc info.
2018-01-08 13:38:28 -08:00
Ben Selfridge
63c2fec79b
Simplified code using addArchExpr.
2018-01-05 14:58:15 -08:00
Ben Selfridge
5cf4c68498
Fixed a bug I introduced because of a delete in the wrong buffer
2018-01-05 14:23:11 -08:00
Ben Selfridge
3c3ffbc375
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
2018-01-05 13:38:36 -08:00
Ben Selfridge
d3f72ee39e
Set semmc version to new.
2018-01-05 13:30:12 -08:00
Ben Selfridge
d95b1f6b3f
Updated macaw-ppc code to handle VecN PPCPrimFns.
2018-01-05 13:27:53 -08:00
Kevin Quick
704c778acd
Added initial ARM architecture-specific evaluation function.
2018-01-05 06:44:29 -08:00
Kevin Quick
b533f4a92a
Added ARM Macaw disassembly functionality.
2018-01-04 17:18:22 -08:00
Kevin Quick
716ae2a28f
Minimal initial ARM abstract block state creation and dependencies.
2018-01-04 16:14:20 -08:00
Tristan Ravitch
2247747bef
Update submodules to the latest macaw (and others)
...
Macaw has removed all floating point expression types, so we duplicate those as
arch-specific functions for PowerPC until the more general floating point
support is ready.
2018-01-02 18:17:32 -08:00
Kevin Quick
cd1c676554
[arm] Initial ARM ELF file macaw import and parse.
2017-12-28 16:30:25 -08:00
Kevin Quick
77d4341ac1
Initial tests for analyzing test-just-exit ARM binary.
2017-12-20 15:26:01 -08:00
Kevin Quick
307450ce14
Add generated output files and editor backup files to gitignore.
2017-12-20 10:13:31 -08:00
Kevin Quick
046ce166d3
Initial empty framwork for macaw-arm ARM support.
2017-12-18 17:46:17 -08:00
Tristan Ravitch
5a2999089a
Remove some tracing
2017-12-18 17:15:05 -08:00
Tristan Ravitch
b7359957bf
Remove the Witness type and related constraint magic
...
This change uses ShapeReprs, and requires changes from dismantle and semmc
2017-12-17 21:29:17 -08:00
