Kevin Quick
54f87526e7
[arm] Update test LoadOptions for new loadRegionBaseOffset parameter.
2018-03-07 00:40:40 -08:00
Kevin Quick
1e85a15146
[arm] Add operands and genExecInstruction support for Thumb.
2018-03-07 00:36:22 -08:00
Kevin Quick
c3d89976e6
[arm] Update Operand eval to clarify A32 and for GPR number abstraction.
2018-03-07 00:32:17 -08:00
Kevin Quick
9f66c7a773
[arm] Update A32 instruction generation for new type args.
2018-03-07 00:30:15 -08:00
Kevin Quick
97a5902408
[arm] Add appEval for URem since it is not handled directly by Macaw base.
2018-03-07 00:27:51 -08:00
Kevin Quick
40b13f63b3
[arm] Define ARM_GP as standalone instead of in terms of A32 GPR.
...
Removes a dependency of the general Macaw semantics on the underlying
A32 dismantle/semmc representation.
2018-03-05 16:10:54 -08:00
Kevin Quick
a3fe4a0f6b
Modify genExecInstruction to use functions for opcode semantics bodies.
...
Pass operand and architecture types and instead of
case opcode of
ADD -> case operands of
Just GPR gpr0 :< Nil of ->
SSA-semantics
Generate:
let opc_ADD operands = case operands of
Just GPR gpr0 :< Nil of ->
SSA-semantics
in case opcode of
ADD -> opc_ADD operand
This provides better encapsulation for the individual operands and
more specific control over the types (at the cost of a pair of
additional type specifications in the call). This also seems to
reduce memory consumption by about half.
2018-03-05 16:02:17 -08:00
Kevin Quick
334b799dd8
Update dismantle submodule reference.
2018-03-05 15:13:55 -08:00
Kevin Quick
b6816799ad
Update s-cargot and s-cargot-letbind submodule versions (0.1.4.0, 0.2.2.0).
2018-03-05 14:05:39 -08:00
Kevin Quick
ce8ebff929
Switch back to main s-cargot package: pretty-printing is now fast.
2018-03-05 13:36:53 -08:00
Tristan Ravitch
66caf33944
ppc: Submodule update for two new instructions
2018-03-01 17:59:57 -08:00
Tristan Ravitch
14c2740c9f
Update semmc submodule for ppc instructions
2018-03-01 17:40:38 -08:00
Tristan Ravitch
3a2b5ac3f2
Remove the case for BVURem
...
We don't have a constructor for this in macaw (it has to be an arch-specific function)
2018-03-01 14:48:14 -08:00
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
