GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-21 13:01:44 +03:00
Code Issues Projects Releases Wiki Activity
435 Commits 53 Branches 0 Tags 14 MiB
c8f4146e1f
Commit Graph

244 Commits

Author SHA1 Message Date
Ben Selfridge
ccd344f027 Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-10-17 12:32:40 -07:00
Ben Selfridge
0649ea4f0c Nearly done with semmc->macaw, need to complete addEltTH function 2017-10-17 12:27:57 -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
cf0a6df0da Simplify the sequencing of our generated monadic PPCGenerator actions 
We were building up a list and calling sequence; instead, just generate a single
do block directly
 2017-10-16 19:51:32 -07:00
Ben Selfridge
1a5946bd0d Nearly done with semmc -> macaw, need to complete a few more cases 2017-10-16 16:40:51 -07:00
Ben Selfridge
e2121de437 Finished bound variable case in addEltTH 2017-10-16 15:53:28 -07:00
Ben Selfridge
17e44dae2a Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-10-16 15:37:49 -07:00
Ben Selfridge
fdf03c5c80 Rearranged a few things 2017-10-16 15:37:19 -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
690687b0b6 started fixing up the BoundVar case 2017-10-16 14:15:12 -07:00
Ben Selfridge
ebe47b74fc work in progress TH translation 2017-10-16 11:35:12 -07:00
Ben Selfridge
d48f30f173 Filled out some TH stuff 2017-10-13 14:26:39 -07:00
Ben Selfridge
50884f8af8 merging 2017-10-13 13:14:58 -07:00
Ben Selfridge
6058c2ebec started template haskell stuff 2017-10-12 10:21:48 -07:00
Tristan Ravitch
b5ac6be425 Add some documentation and build some helpful maps for the TH translation 2017-10-12 10:11:16 -07:00
Tristan Ravitch
90e66cd252 Update to the latest macaw changes 2017-10-11 21:04:04 -07:00
Tristan Ravitch
e5895833ba Plumb through most of the TH bits to generate 'execInstruction' 
The remaining part is 'genCaseBody', which is where we'll write the translator
from ParameterizedFormula to TH Exps.  The semantics are loaded from semmc and
the outer case expression breaking down instructions is all in place.  This has
several accompanying changes in semmc and dismantle.
 2017-10-11 18:07:56 -07:00
Ben Selfridge
54f5715c8b filled out locToReg 2017-10-10 15:37:22 -07:00
Ben Selfridge
b270a2b9a2 Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-10-10 14:51:54 -07:00
Ben Selfridge
064d0c4e8d Added TestBit, done (for now) with crucible expressions 2017-10-10 14:51:25 -07:00
Ben Selfridge
d0fac23418 Fixed BVSelect a bit; need to re-examine type proofs 2017-10-10 14:35:00 -07:00
Ben Selfridge
578c1c0258 Completed BVConcat and BVSelect 2017-10-10 12:32:20 -07:00
Tristan Ravitch
c0889aa8bb Enable formula loading in the TH entry point 
Also update the semmc submodule to the required version.
 2017-10-09 23:18:33 -07:00
Ben Selfridge
6db1a2d43c rewrote crucAppToExpr in applicative style 2017-10-09 16:07:52 -07:00
Ben Selfridge
b1cbc0548e Completed refactoring of Expr type. 2017-10-09 14:02:52 -07:00
Ben Selfridge
058963f8fe Changed Expr type to be non-recursive 2017-10-09 11:27:59 -07:00
Tristan Ravitch
c1566e7946 Fix an issue with formula loading 
Also disable formula loading for now because it raises an exception due to some
unhandled constructs in the parser.
 2017-10-06 22:14:34 -07:00
Tristan Ravitch
95361474ae Feed semantics to the genExecInstruction calls 
These lists come from semmc and contain the bytestrings of the semantics files
for each opcode.

NOTE: The lists are currently empty (presumably due to bugs), but the logic for
moving data around and setting up a SimpleBuilder instance is at least right.
 2017-10-06 16:58:53 -07:00
Tristan Ravitch
072571d219 Expand the initial abstract state for a block 
We needed to note that the LNK register contains the return address
 2017-10-04 17:01:56 -07:00
Tristan Ravitch
38cb6cdfd8 Add a note about TranslateError 2017-10-04 17:01:56 -07:00
Ben Selfridge
c76cd00e72 trying to fix git 2017-10-04 16:40:14 -07:00
Tristan Ravitch
0a974b1a15 Add the TH invocation to PPC32 2017-10-04 16:00:18 -07:00
Tristan Ravitch
1e55026ae5 Add a definition of absEvalArchFn 
We'll have to expand this as we add functions
 2017-10-04 15:55:28 -07:00
Tristan Ravitch
711eabc058 Implement postCallAbsState and absEvalArchStmt 
absEvalArchStmt is trivial (for now)
 2017-10-04 15:53:03 -07:00
Tristan Ravitch
ac776b7340 Remove a redundant export 2017-10-04 15:51:03 -07:00
Tristan Ravitch
f12166c2c3 Add a trivial definition of the architecture-specific abstract evaluation function 2017-10-04 15:46:33 -07:00
Tristan Ravitch
ab29030e14 Implement the initial abstract state 2017-10-04 15:44:59 -07:00
Tristan Ravitch
6a14cfffb8 Implement archDemandContext 
This required a few more instances and a wrapper around `ArchStmt`
 2017-10-04 14:40:36 -07:00
Ben Selfridge
7e563acef8 Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-10-04 14:09:02 -07:00
Ben Selfridge
bb0d7e7341 converting from crucible Elt type to Macaw Apps 2017-10-04 14:08:09 -07:00
Tristan Ravitch
57db5aa6f6 Add a definition of the jump table entry size 2017-10-04 13:26:08 -07:00
Tristan Ravitch
c02b0c605c Add a trap arch-specific statement 2017-10-04 13:25:56 -07:00
Tristan Ravitch
7f8410ce7f Fill in some previously undefined IP value calculations 2017-10-04 11:24:16 -07:00
Tristan Ravitch
af6ead250a Add some documentation 2017-10-04 11:08:42 -07:00
Tristan Ravitch
20f078e9eb Hook up the execInstruction functions 
These are now referenced in the necessary spots in the ArchitectureInfo definitions
 2017-10-04 10:16:54 -07:00
Tristan Ravitch
498ff33a6d Finish the disassembler skeleton 
There are still some IP values to compute, but the shape of the algorithm is there
 2017-10-04 10:10:06 -07:00
Tristan Ravitch
047e84c586 Remove an unused import 2017-10-04 10:10:06 -07:00
Tristan Ravitch
48f556ffcb Add some more helpers for the Generator monad 2017-10-04 10:10:06 -07:00
Tristan Ravitch
00f2b1d423 Add a context that we'll need 2017-10-04 10:10:06 -07:00
Tristan Ravitch
eec7075b46 Implement catchError in a MonadError instance 2017-10-04 10:10:06 -07:00
Ben Selfridge
3a49345b15 Added Semantics directory, had forgotten to add it previously 2017-10-04 10:03:29 -07:00
Ben Selfridge
5de25b8906 Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-10-04 10:00:04 -07:00
Tristan Ravitch
9b8a7bac21 Remove an unused module 
The rewriters are now in the Arch module
 2017-10-04 08:48:52 -07:00
Tristan Ravitch
a851cddebd Add arch-specific decls + type instances + rewriters 
This also lets us add 'withArchConstraints' easily.
 2017-10-03 18:59:35 -07:00
Tristan Ravitch
8a1195b1c6 Fill in the AddrWidthReprs for PPC 2017-10-03 18:07:21 -07:00
Tristan Ravitch
d1c86fd6d4 Remove unused imports 2017-10-03 18:07:15 -07:00
Tristan Ravitch
c751e02e6c Use a ConstraintKind to simplify a number of constraint contexts 2017-10-03 18:05:46 -07:00
Tristan Ravitch
adf8a46f91 Implement more of the PPCGenerator state 2017-10-03 18:00:54 -07:00
Tristan Ravitch
2ec88811c5 Add special purpose registers to the definition of 'RegisterInfo' 2017-10-03 16:37:01 -07:00
Tristan Ravitch
171cc0d5ca Remove an unused module 2017-10-03 16:31:41 -07:00
Tristan Ravitch
4a8828429c Implement 'RegisterInfo' for PPCReg 2017-10-03 16:31:16 -07:00
Ben Selfridge
ad8d5fc3b4 Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-10-03 14:43:33 -07:00
Tristan Ravitch
dc261436c7 Generalize the type of PPCReg 
The width of a GPR was formerly fixed to 64 bits.  It now reflects the actual arch.
 2017-10-03 13:40:11 -07:00
Tristan Ravitch
5e136dceec Let PPCGenerator report errors 
It doesn't right now, but the translation from semantics to macaw will have some
opportunities around invalid encodings.
 2017-10-03 13:39:59 -07:00
Tristan Ravitch
19b65973fc Apply the state transformer 
Committing now to experiment with adding failure modes to PPCGenerator
 2017-10-03 13:23:20 -07:00
Tristan Ravitch
620b6f5980 Plumb through a parameter for the semantics lookup function 
This is the function that will be generated via TH for PPC32 and PPC64.
 2017-10-03 11:55:40 -07:00
Tristan Ravitch
6ed9d0d45d Simplify more type variables and implement the error throwing function for the disassembler 
We had two different state thread parameters: s and ids.  We only need one (for
now), so unify them.
 2017-10-03 11:09:23 -07:00
Tristan Ravitch
7aadfdf373 Remove a literal width of 64 
That should have been a function of the architecture
 2017-10-03 10:31:06 -07:00
Tristan Ravitch
083f9b4fa1 Remove a type parameter 
We don't need the separate w - it is just a function (ArchAddrWidth) of the architecture.
 2017-10-03 09:36:41 -07:00
Tristan Ravitch
d5c5d40ddb Add more disassembly infrastructure 2017-10-02 17:32:59 -07:00
Ben Selfridge
2b810be25a Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-10-02 14:38:20 -07:00
Tristan Ravitch
7869f0e6c7 More work on disassemble 2017-10-02 14:29:15 -07:00
Tristan Ravitch
385bff0c4d Move the generator monad into its own module 2017-10-02 14:17:36 -07:00
Tristan Ravitch
4b6b82cd13 Flesh out disassembleFn a bit more 2017-10-02 13:35:51 -07:00
Tristan Ravitch
20e5b5f00d Add some type instance declarations for ppc32 and ppc64 2017-10-02 13:35:04 -07:00
Ben Selfridge
0526c6ae21 merging 2017-10-02 12:55:52 -07:00
Ben Selfridge
6f0d49f76e Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc 2017-10-02 12:54:43 -07:00
Tristan Ravitch
90a9c5ff65 Generalize the architecture info def 
Now we can use the same infrastructure for PPC32 and PPC64.  There might be some
rough edges, but we can work around those with type functions.

This change also adds an implementation for the preserved registers across
system calls for macaw.
 2017-10-02 11:44:46 -07:00
Ben Selfridge
136d772abf merging some things 2017-10-02 11:23:08 -07:00
Tristan Ravitch
4d9c7cd028 Split up the functions that will comprise ppc_linux_info 2017-10-02 11:19:34 -07:00
Ben Selfridge
677ba803b3 Added a couple things 2017-10-02 11:10:00 -07:00
Tristan Ravitch
1f1a6d8561 Abstract the stubs to work for ppc32 and ppc64 2017-10-02 10:59:40 -07:00
Tristan Ravitch
61218ca31d Add stubs for most of the architecture info functions 2017-10-02 10:54:10 -07:00
Tristan Ravitch
45f08a2036 Fill in the endianness of the arch info 2017-10-02 10:37:44 -07:00
Tristan Ravitch
c997e2dada Use explicit exports for PPCReg 2017-10-02 10:32:58 -07:00
Tristan Ravitch
6b967e1e8a Fill out the fields of ppc_linux_info 2017-10-02 10:32:05 -07:00
Tristan Ravitch
cdd9647db9 Simplify some helpers in macaw-ppc 
Use the MonadState combinators and a lift instead of explicitly wrapping
monadic actions.
 2017-10-02 10:27:12 -07:00
Tristan Ravitch
202a95b959 Re-use the PPC arch tag (specifically, PPC64) from semmc-ppc 2017-10-02 10:26:51 -07:00
Tristan Ravitch
8820b01805 Depend on semmc/semmc-ppc and enable warnings 2017-10-02 10:26:39 -07:00
Tristan Ravitch
07ff647dcf Add some missing instances for PPCReg 2017-10-02 09:40:17 -07:00
Ben Selfridge
7a443bfe99 added a few more functions for PPCGenerator 2017-09-29 17:35:29 -07:00
Ben Selfridge
b234b673f9 Added addStmt to PPCGenerator monad 2017-09-29 15:37:41 -07:00
Ben Selfridge
65a7e8c17c second commit 2017-09-29 09:37:45 -07:00
Ben Selfridge
bf9b320e38 first commit 2017-08-28 15:48:55 -07:00