Commit Graph

67 Commits

Author SHA1 Message Date
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
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
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
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
Tristan Ravitch
f1b0775be8 Update to the new parameterized-utils List
This replaces the old ShapedList from dismantle-tablegen
2017-12-13 21:56:29 -08:00
Tristan Ravitch
7bcc90c83d Start migrating shareable TH code from macaw-ppc to macaw-semmc
This change still needs some work, but no other code depends on it yet
2017-12-06 17:28:23 -08:00
Tristan Ravitch
3838d0964d Submodule updates 2017-11-30 17:13:11 -08:00
Tristan Ravitch
5d2af0328f Update the semmc submodule 2017-11-29 20:27:49 -08:00
Tristan Ravitch
52dc736c08 ppc: Add more support for CR and FPSCR instructions 2017-11-29 16:30:46 -08:00
Tristan Ravitch
0a24dbf78e Update the semmc submodule 2017-11-29 11:40:14 -08:00
Tristan Ravitch
5347f7b079 Update the semmc submodule with more semantics 2017-11-28 23:10:58 -08:00
Tristan Ravitch
c4675b47e4 ppc: Add some more semantics for the cr logical operations 2017-11-28 22:36:08 -08:00
Tristan Ravitch
b033f3788c ppc: Change how we translate instructions represented by arch-specific statements
The old method involved providing the TH code a list of match expressions.  This
made it very difficult to inspect arguments of instructions.  The new approach
has the architecture backend provide a function that gets the first opportunity
to process instructions, which is much more flexible.  This commit also includes
support for a number of cache hint instructions that use the new features.
2017-11-28 21:36:49 -08:00
Tristan Ravitch
cea6bf38c8 Update the dismantle submodule
Cleans up a warning
2017-11-28 19:46:18 -08:00
Tristan Ravitch
b1e0b07cc1 Update semmc and dismantle 2017-11-28 18:42:32 -08:00
Tristan Ravitch
289e1f33be [ppc] Updates to support some vector instructions
The semantics for many of the vector instructions are incomplete and just set
the target register to undefined.  This is enough for code discovery (for now).
2017-11-27 18:16:19 -08:00
Tristan Ravitch
1d49256c23 Bump the semmc submodule 2017-11-22 17:04:47 -08:00
Tristan Ravitch
18d5ac3fe4 Add a translation for the undefined value from semmc 2017-11-21 23:37:17 -08:00
Tristan Ravitch
96a787f895 semmc submodule update
This update includes semantics files for the floating point store instructions
2017-11-16 10:17:54 -05:00
Tristan Ravitch
e4d3942094 Update the semmc submodules for some more instruction semantics 2017-11-13 23:33:07 -08:00
Tristan Ravitch
90f066cd5b Add a few more arithmetic and bitwise instructions 2017-11-13 18:05:51 -08:00
Tristan Ravitch
693727330d Update the semmc submodule with more semantics 2017-11-13 16:54:01 -08:00
Tristan Ravitch
0d6877611b Add some bugfixes for popcount in the semmc submodule 2017-11-10 17:22:52 -08:00
Tristan Ravitch
2002afa246 [ppc] Add preliminary support for popcount
It isn't supported in SimpleBuilder, so we use an uninterpreted function in the
formula language for now.
2017-11-10 16:52:38 -08:00
Tristan Ravitch
bbd00f7ef2 [ppc] Add division and a few arch-specific statements
The arch-specific statements are for memory synchronization
2017-11-10 14:48:35 -08:00
Tristan Ravitch
c990077d7b Update the semmc submodule
This update includes many more semantics files covering most of the dotted
instruction variants
2017-11-09 23:31:13 -08:00
Tristan Ravitch
fc1bd8b077 Add support for more instructions
semmc has semantics for many new instructions.  We also added support for
translating the count leading zero functions.
2017-11-09 17:17:51 -08:00
Tristan Ravitch
9b9e1654ec Update the submodules to add more semantics
This focuses on the rotate instructions
2017-11-08 15:47:01 -08:00
Tristan Ravitch
5e150c15a0 Update to the latest semmc
This includes some new semantics required for the test suite
2017-11-08 10:59:43 -08:00
Tristan Ravitch
008c422917 Update to the latest semmc
This includes semantics for generalized branch conditional
2017-11-06 22:25:12 -08:00
Tristan Ravitch
6a45dc0893 [ppc] Fix an issue with floating point translation
The change is actually in the semantics (semmc), where we were extracting the
wrong part of the 128 bit vector registers to operate on.  Many operations were
being simplified to zero, which manifest as unused fprc registers.
2017-11-06 14:25:54 -08:00
Tristan Ravitch
a9baec5d39 Port to the latest macaw
This makes the architecture-specific terminator statement handling actually work
2017-11-06 10:11:34 -08:00
Tristan Ravitch
e765345a7b Add support for the Syscall arch-specific terminator 2017-11-04 16:23:12 -07:00
Tristan Ravitch
0e9b739503 Implement test_bit_dynamic in the TH translation of semantics
It translates to a BVTestBit (since here we know which bit to extract, whereas
we don't in the semantics).
2017-11-03 15:07:52 -07:00
Tristan Ravitch
c788aebab8 Update the dismantle submodule
This fixes a bug in parsing the stdu instruction that was causing our test to
implode.  It still isn't right, but it gets farther (and parses two instructions
out of the block).
2017-10-31 22:23:57 -07:00
Tristan Ravitch
0fb90e5d6b Update dismantle and semmc
This adds some more general instances needed for higher-level dependencies
2017-10-23 18:06:32 -07:00
Tristan Ravitch
28b7b68881 Fill out more of the PPC semantics translation
This covers all of the floating point used so far, as well as memory operations.
Note that this commit relies on changes that aren't pushed to macaw yet.
2017-10-18 17:48:07 -07:00
Tristan Ravitch
ace4520846 Update to the latest macaw 2017-10-18 10:29:57 -07:00
Tristan Ravitch
13def38f25 Fix some compilation errors with an improved evaluator in semmc 2017-10-17 21:38:53 -07:00
Tristan Ravitch
2a7c5bd541 Extend the uninterpreted function evaluator
It is currently very messy because the ppc.is_r0 function breaks some
abstraction boundaries that make it very irregular.  There is some common code
that can probably be factored out, but it will still be a mess.

The other big change is handling the read_mem calls.
2017-10-17 19:16:31 -07:00
Tristan Ravitch
eb8b78b372 Add support for a number of new uninterpreted functions
This covers evaluating all of the statically-evaluated functions in expression
contexts (e.g., is_r0 and the memory reference extraction functions).

The expansion seems pretty reasonable.

There are still some cases to handle w.r.t. floating point elementary functions
and memory reads and writes, which need to be handled a bit differently.

Note: we also have to call the formula simplifier soon.
2017-10-17 17:07:03 -07:00
Tristan Ravitch
07c48afe46 Add instantiations for some uninterpreted functions
This covers functions that are used to isolate locations to be defined from
composite operands (e.g., the base registers of memrr and memri operands).
2017-10-17 11:51:11 -07:00
Tristan Ravitch
db2da637b0 Update the semmc submodule 2017-10-16 23:27:44 -07:00
Tristan Ravitch
792eb1aaf9 [ppc] Add a helper for turning operands into bitvectors
The main function is 'extractValue', which takes an operand and returns a macaw
bitvector for it (in the PPCGenerator monad).

There are still some missing cases for the memory operands.
2017-10-16 15:11:16 -07:00
Ben Selfridge
62d26946dc merging because semmc is being weird 2017-10-16 11:38:38 -07:00
Tristan Ravitch
cc00389c44 [ppc] Update the PPC semantics 2017-10-13 17:05:45 -07:00
Tristan Ravitch
1017c51ead Update the semmc submodule to include the FP base set 2017-10-13 14:20:22 -07:00
Ben Selfridge
50884f8af8 merging 2017-10-13 13:14:58 -07:00