GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-26 23:52:48 +03:00
Code Issues Projects Releases Wiki Activity
1,410 Commits 53 Branches 0 Tags 14 MiB
06b0390cfd
Commit Graph

1410 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Joe Hendrix
e204724358
Merge pull request #27 from GaloisInc/jhx/vec 
Add vector type and operations.
 2019-02-27 08:57:50 -08:00
Joe Hendrix
89ffdf088a
Fix macaw-x86-symbolic and update crucible. 2019-02-27 01:43:53 -08:00
Joe Hendrix
e8d2efcaae
Implement bitcast changes to macaw-symbolic 2019-02-26 17:53:34 -08:00
Kevin Quick
898e7bdb95
[refinement] Added newline to end of expected output file. 2019-02-26 14:51:49 -08:00
Kevin Quick
70657ee811
[x86_symbolic] Use stable value for generating x86 register name. 
Relying on the underlying Show instance representation for the
register name is more brittle, especially if the Show becomes a
structural representation (e.g. "X86_GP 14") that introduces spaces
and other elements that can cause problems.  Generate the register
name in a more reliable manner for the symbolic variable use case
here.
 2019-02-23 21:52:36 -08:00
Kevin Quick
3fe6fdf949
Sort refinement results for test stability and visual convenience. 2019-02-23 21:33:40 -08:00
Kevin Quick
91f871dced
Added llvm-pretty-bc-parser submodule to stack.ghc-8.6.3.yaml. 2019-02-21 22:23:43 -08:00
Kevin Quick
9662651b09
Added llvm-pretty-bc-parser submodule to cabal.project.dist. 2019-02-21 22:23:05 -08:00
Kevin Quick
11a2481135
Add llvm-pretty-bc-parser dependency. 2019-02-21 22:21:51 -08:00
Joe Hendrix
37c0aca3a5
Cleanup travis.yml further. 2019-02-20 16:24:18 -08:00
Joe Hendrix
5b1548c36c
Try fixing travis build 2019-02-20 16:16:34 -08:00
Joe Hendrix
c950affd65
Fix build errors made in previous commit. 2019-02-20 15:57:56 -08:00
Joe Hendrix
43bcf9cafa
Merge remote-tracking branch 'origin/master' into jhx/vec 2019-02-20 15:42:46 -08:00
Joe Hendrix
00096344a7
Support float/vector in reads/writes; Use floating point types. 2019-02-20 15:40:59 -08:00
Kevin Quick
731d68df40
Updated stack build for GHC 8.6.3 to include macaw-semmc packages. 2019-02-20 11:14:10 -08:00
Kevin Quick
ca6e5a947c
Updated README.md to include macaw-semmc information. 
Removed README.org from macaw-semmc, consolidated all README
information to README.md.
 2019-02-20 11:13:54 -08:00
Joe Hendrix
35af2a5c3a
Rename VectorTypeRepr to VecTypeRepr 2019-02-19 10:18:12 -08:00
Kevin Quick
b80ab8fb67
[symbolic] update to latest crucible. 2019-02-19 08:24:45 -08:00
Kevin Quick
228b0085d6 Update macaw-loader and semmc submodule versions. 2019-02-18 15:02:08 -08:00
Kevin Quick
b50e6025e6
Update cabal.project.dist to reflect submodule de-duplication from merge. 2019-02-18 11:42:57 -08:00
Kevin Quick
101a638add
Eliminate duplication in submodules. 2019-02-18 11:42:24 -08:00
Kevin Quick
8aefd5224f
Merge ../macaw-semmc 
Combined .gitignore rules and merged .gitmodules as the concatenation
of the individual .gitmodules; this will result in duplicate
submodules which will be resolved in a subsequent commit.
 2019-02-18 09:44:31 -08:00
Luke Maurer
b23ba5820d CrucGen: Support for jump tables 
This needed a bit more surgery than one would like, since we need to
translate the indirect jump to an if-else chain, which means creating a
bunch of "extra" blocks from within the `CrucGen` monad.
 2019-02-15 18:35:25 -08:00
Tristan Ravitch
1d3610a783 Revert "Fill in undefineds with nonsense so pretty printing works" 
This reverts commit 86ef62645d.

This commit generates invalid Crucible CFGs, which causes downstream analysis to
fail.  Reverting the commit will allow downstream clients to discard invalid CFGs.
 2019-02-15 08:35:17 -08:00
Tristan Ravitch
c527a91521 Merge branch 'master' of github.com:GaloisInc/macaw 2019-02-15 08:31:41 -08:00
Joe Hendrix
fa8583de44
Merge pull request #25 from GaloisInc/jhx/zmm 
Vector improvements
 2019-02-15 08:21:10 -08:00
Joe Hendrix
a2611303ff
Add GHC 8.6.3 stack and switch travis to use it. 2019-02-15 00:42:53 -08:00
Joe Hendrix
3b7e12de16
Update to fix build process. 2019-02-15 00:28:35 -08:00
Tristan Ravitch
934784aed2 Update submodules 
The code has been updated, but the crucible submodule was out of date (w.r.t. some what4 changes in
the natrepr)
 2019-02-14 21:20:59 -08:00
Joe Hendrix
d3947f32b4
Support ZMM, bitcasting, and fixed length vectors. 2019-02-14 11:06:45 -08:00
Luke Maurer
68ae66bff5 NatRepr changes 2019-02-13 14:21:48 -08:00
Luke Maurer
97a6a43c5b Fix for GHC versions < 8.4 2019-02-13 13:42:43 -08:00
Luke Maurer
cbda1717cc Fix for GHC versions < 8.8 
`MonadFail` being a forward-compatibility measure, overriding
`Control.Monad.Fail.fail` in GHC versions <= 8.6 doesn't do anything
unless `Control.Monad.Fail.fail` is invoked explicitly (or the importing
module happens to have `-XMonadFailDesugaring` on).
 2019-02-12 18:24:41 -08:00
Langston Barrett
ee4a4ff268
Merge pull request #24 from siddharthist/pu 
update parameterized-utils submodule
 2019-02-11 15:09:08 -08:00
Langston Barrett
274808a8ae update parameterized-utils submodule 2019-02-11 11:47:19 -08:00
Kevin Quick
3e7bd01560
[refinement] Disabled PPC switching test. 
Attempting to refine the switching test for PPC executables ends up
with a non-terminating Z3 process, so this test is disabled until this
is diagnosed.
 2019-02-08 17:32:21 -08:00
Kevin Quick
5f12c3da88
[symbolic] Remove unneeded debug import. 2019-02-08 17:31:30 -08:00
Kevin Quick
edb486c6b3
Added toCrucibleEndian in symbolic and use for memory setup in refinement. 
Requires updated macaw-loader BinaryFormat information.
 2019-02-08 17:30:18 -08:00
Kevin Quick
0f97a86c3e
Added missing pretty-printer import. 2019-02-08 17:29:03 -08:00
Kevin Quick
9c5ebee0bc
Added ArchInfo lookupReg and updateReg for PPC. 2019-02-08 17:28:43 -08:00
Kevin Quick
9f46c9e60b Merge branch 'master' of github.com:GaloisInc/macaw-semmc 2019-02-08 14:37:54 -08:00
Kevin Quick
d3228847f7
[refinement] add PPC tests expected results. 2019-02-08 14:26:17 -08:00
Kevin Quick
6cb0868d1b
[refinement] import cleanup 2019-02-08 14:20:29 -08:00
Kevin Quick
290e33279a
[refinement] Enable PPC testing. 2019-02-08 14:10:08 -08:00
Kevin Quick
3eeaed08a2 Merge branch 'master' of github.com:GaloisInc/macaw 2019-02-08 08:30:26 -08:00
Andrei Stefanescu
c67e474a19 [refinement] Move symbolic execution code in its own module. 2019-02-07 19:43:58 -08:00
Andrei Stefanescu
5b93187d5b [refinement] Update .cabal file. 2019-02-07 17:25:52 -08:00
Andrei Stefanescu
45e4251bf3 [refinement] Add an unbounded memory allocation at the bottom of the allocation stack. 2019-02-07 17:23:02 -08:00
Kevin Quick
33540121f5 Merge branch 'master' of github.com:GaloisInc/macaw 2019-02-07 17:15:24 -08:00
Kevin Quick
3baf55376b
[refinement] update run-refinement for summary and verbose modes. 2019-02-07 17:15:00 -08:00