GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-18 19:41:44 +03:00
Code Issues Projects Releases Wiki Activity
407 Commits 51 Branches 0 Tags 14 MiB
556cfa5a47
Commit Graph

407 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Tristan Ravitch
2d54ca1362 ppc: Fix some expected test output 
Recent changes in macaw(-base) mean that we split blocks more aggressively.  The
old expected outputs were conservative - these new values are much more in line
with intuitive expectation (with more aggressive splitting of blocks and less
code duplication between blocks).
 2018-03-23 15:14:54 -07:00
Kevin Quick
0e36353f63 Update dismantle submodule reference. 2018-03-15 17:41:28 -07:00
Kevin Quick
0069d3c907
[arm] Add ExtractValue for Maybe of Thumb LowGPR operand. 2018-03-11 10:54:33 -07:00
Kevin Quick
7d12033f0c Merge branch 'master' of https://gitlab-ext.galois.com/macaw/macaw-semmc 2018-03-11 10:54:24 -07:00
Kevin Quick
0942725e07 Update semmc submodule reference. 2018-03-11 10:54:10 -07:00
Kevin Quick
24991edd70 Merge branch 'master' of https://gitlab-ext.galois.com/macaw/macaw-semmc 2018-03-11 10:35:03 -07:00
Kevin Quick
b0205af9ff
[arm] Added ExtractValue for Thumb AddrModeIs4 operand. 2018-03-11 10:34:44 -07:00
Kevin Quick
99a8959b04 Update dismantle and semmc submodule references. 2018-03-11 10:31:36 -07:00
Kevin Quick
c50f01efef
[arm] Added test exe and results for test-just-exit-t32. 2018-03-10 21:55:29 -08:00
Kevin Quick
5e72398ef2
[arm] Add support for the Thumb Reglist operand. 2018-03-10 10:05:52 -08:00
Kevin Quick
0c67eddda8
Unsupported functions (nonceAppEval) should error immediately. 
Original version was pushing error into generated TH, which was
generating the error statement into the SSA formula; this breaks
formula interpretation at compile time but hides the error.  Instead,
this changes it so that the error is thrown during TH evaluation.
 2018-03-10 10:04:03 -08:00
Kevin Quick
1bceb8dc32
[arm] Update for change in export of numGPR from semmc-ppc. 2018-03-10 10:03:01 -08:00
Kevin Quick
86defa921b Merge branch 'THGenWrapper' 2018-03-07 14:50:42 -08:00
Kevin Quick
491c302bfb
[arm] Add support for ARM Thumb TImm01020S4 operand. 2018-03-07 14:48:34 -08:00
Kevin Quick
fc02db5664
Update semmc submodule reference. 2018-03-07 14:46:45 -08:00
Kevin Quick
ca2c54a98f [arm] Simplification of instruction decode selection wrapping. 2018-03-07 10:19:55 -08:00
Kevin Quick
af590fc7db
[arm] Add support for imm5 operand type. 2018-03-07 10:07:51 -08:00
Kevin Quick
cf9b6c5a30
[arm] Updated disassemble operation to support A32 or T32 block disassembly. 2018-03-07 10:06:29 -08:00
Kevin Quick
acb8812d68
[arm] Fix non-semantics instruction matcher to return Nothing when unrecognized. 2018-03-07 00:42:01 -08:00
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