Commit Graph

404 Commits

Author SHA1 Message Date
Kevin Quick
83dc9ad394
[arm] Cleanup imports and avoid name conflicts in Macaw.ARM.Arch. 2018-02-22 17:16:55 -08:00
Kevin Quick
a15840ead7
[arm] whitespace/formatting cleanup. 2018-02-22 17:05:38 -08:00
Kevin Quick
b444c76969
[arm] Implement rewriteArchTermStmt (ARMSyscall only so far). 2018-02-22 17:03:26 -08:00
Kevin Quick
10d9144f1e
[arm] Added support for SVC syscall with argument. 2018-02-22 17:01:20 -08:00
Kevin Quick
747ce16f5f
[arm] Add arm_LR link register and initialize it in the abstract state. 2018-02-22 16:58:34 -08:00
Kevin Quick
3120eda53f
[arm] Add value extraction for LdstSoReg operand. 2018-02-22 16:24:02 -08:00
Kevin Quick
1027ad0c06
[arm] Simple armNonceAppEval: no arch-specific overrides needed. 2018-02-22 16:22:54 -08:00
Kevin Quick
a9b55b655b
[arm] Added identifyCall and identifyReturn trivial implementations. 2018-02-22 16:15:34 -08:00
Kevin Quick
cc623ae16f
[arm] Added trivial rewriteArchFn ... currently no ARM primitives. 2018-02-22 16:09:32 -08:00
Kevin Quick
99bbff0f5f
[arm] Add rewriteStmt (trivial implementation). 2018-02-22 16:08:01 -08:00
Kevin Quick
d53ad182e8
Add genExecInstructionLogging and genExecInstructionLogStdErr.
Allows generatino of exec instructions with logging output to stderr
or another designated location, which can be useful for diagnostic
purposes.
2018-02-22 15:54:35 -08:00
Kevin Quick
d2fb7b751a
[arm] Output logging information while generating instructions. 2018-02-22 15:43:54 -08:00
Kevin Quick
24f1f65cc6
[arm] Add value extraction for SoRegReg operand. 2018-02-20 08:52:02 -08:00
Kevin Quick
2e6245b378
[arm] Add value extraction for SoRegImm operand 2018-02-20 08:50:56 -08:00
Kevin Quick
ef503793b7
Show unsupported Crucible elt in error message. 2018-02-20 08:46:57 -08:00
Kevin Quick
c94f02d071
Add semantics support for BVUrem operation. 2018-02-20 08:43:55 -08:00
Kevin Quick
0e540d2025
[arm] Added CPSR as a known register. 2018-02-20 08:38:17 -08:00
Kevin Quick
add6dd96f9 Update submodule reference: dismantle 2018-02-17 12:09:33 -08:00
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