Tristan Ravitch
|
f180b23d65
|
ppc: Add more semantics for floating point instructions
|
2018-03-01 14:43:25 -08:00 |
|
Kevin Quick
|
3af6050855
|
[arm] Explicit ARM Dismantle module reference to avoid confusion.
|
2018-03-01 12:53:49 -08:00 |
|
Kevin Quick
|
a7d3270520
|
[arm] Add ExtractValue instance for Word16 (Shift_so_reg_imm operand).
|
2018-03-01 12:51:12 -08:00 |
|
Kevin Quick
|
6820e66e86
|
Merge branch 'master' of https://gitlab-ext.galois.com/macaw/macaw-semmc
|
2018-03-01 12:03:25 -08:00 |
|
Kevin Quick
|
a5c20d8824
|
Update macaw submodule
|
2018-03-01 11:50:42 -08:00 |
|
Tristan Ravitch
|
fac5a84d5b
|
Update the semmc submodule
|
2018-03-01 09:22:32 -08:00 |
|
Daniel Wagner
|
851168f9ad
|
let tests compile again
|
2018-03-01 11:45:59 -05:00 |
|
Kevin Quick
|
6d373bfcc5
|
[arm] Add value extraction for BranchExecuteTarget operand encoding.
|
2018-03-01 00:31:08 -08:00 |
|
Tristan Ravitch
|
3542977fc7
|
Update the semmc submodule
This has some more instructions for PowerPC
|
2018-02-28 23:22:56 -08:00 |
|
Tristan Ravitch
|
82bbd93d2a
|
ppc: Add arch statements for hardware transactional memory
These instructions are mostly outside of our model. That said, they do have
effects on the CPU state that we really should model, but are not yet.
|
2018-02-28 22:33:10 -08:00 |
|
Tristan Ravitch
|
1b16f163ac
|
Submodule updates
|
2018-02-28 22:33:03 -08:00 |
|
Kevin Quick
|
610fdc93b5
|
[arm] Use renamed version of expected binary analysis results.
|
2018-02-27 10:48:11 -08:00 |
|
Kevin Quick
|
70d4cbee2d
|
[arm] Update ARMTests to validate binary analysis against expected results.
|
2018-02-27 10:46:01 -08:00 |
|
Kevin Quick
|
16dbc72948
|
[arm] Update naming scheme for generated A32 and T32 test executables.
|
2018-02-27 10:02:33 -08:00 |
|
Kevin Quick
|
6cb56fcef3
|
Merge branch 'master' of https://gitlab-ext.galois.com/macaw/macaw-semmc
|
2018-02-23 15:41:19 -08:00 |
|
Kevin Quick
|
1606ad994d
|
[arm] Add arch-specific handling for arm.isR15 uninterpreted function.
|
2018-02-23 15:40:19 -08:00 |
|
Kevin Quick
|
a592e40b12
|
Update macaw submodule to 6a0a59e
|
2018-02-23 15:04:15 -08:00 |
|
Kevin Quick
|
70a71cc64c
|
[arm] Minimal ELF binary format loading functionality for initial testing.
|
2018-02-22 18:00:18 -08:00 |
|
Kevin Quick
|
e8b9d8a6a4
|
[ppc] Update for changed Macaw.Memory LoadOptions.
|
2018-02-22 17:37:40 -08:00 |
|
Kevin Quick
|
2983562204
|
[arm] Update for argument change to Macaw.Memory.LoadOptions.
|
2018-02-22 17:36:07 -08:00 |
|
Kevin Quick
|
50b4d3e784
|
[arm] remove unused semantics TH definitions.
|
2018-02-22 17:24:44 -08:00 |
|
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 |
|