Commit Graph

1766 Commits

Author SHA1 Message Date
Lisanna Dettwyler
906cef407d Merge remote-tracking branch 'origin/master' into lisanna/ci-init-8.10.2 2020-10-21 10:20:04 -07:00
Kevin Quick
e7c9d2ea00
Merge pull request #172 from GaloisInc/redundant_unpack_cases
Extract single Assignment element without redundant pattern case
2020-10-21 10:00:16 -07:00
Kevin Quick
7d497c1f46
Merge branch 'master' into redundant_unpack_cases 2020-10-21 09:59:34 -07:00
LisannaAtGalois
5adf154a62
Merge pull request #168 from GaloisInc/lisanna/ci-more-ghc
Init 8.6.5 testing
2020-10-21 09:40:18 -07:00
Kevin Quick
923089d767
Extract single Assignment element without redundant pattern case 2020-10-20 21:09:15 -07:00
Lisanna Dettwyler
31c2217a9d Annotate known issues 2020-10-20 14:08:36 -07:00
Lisanna Dettwyler
47544e4b2d Fix warnings in GHC 8.10 2020-10-20 13:53:22 -07:00
Lisanna Dettwyler
e12f71e5be Init CI for 8.10.2 2020-10-20 13:53:09 -07:00
Lisanna Dettwyler
a5f11c114d remove 8.10 2020-10-20 13:44:37 -07:00
Lisanna Dettwyler
a38ec82fda Remove 8.10 from this PR 2020-10-20 13:44:37 -07:00
Lisanna Dettwyler
f0790505cc Invalidate cabal cache when dependencies change 2020-10-20 13:44:37 -07:00
Lisanna Dettwyler
66c41039a6 Init [8.6.5 8.10.1] testing 2020-10-20 13:44:37 -07:00
LisannaAtGalois
5a22913f2a
Merge pull request #169 from GaloisInc/lisanna/gha-dep-fns
Replace deprecated GitHub Actions functions
2020-10-19 14:13:12 -07:00
Lisanna Dettwyler
5ca4f4e501 Replace deprecated GitHub Actions functions 2020-10-15 09:56:29 -07:00
Sam Breese
3a071e317b
symbolic: Fix PackBits and UnpackBits (#166) 2020-10-12 14:20:05 -04:00
Sam Breese
34e7394c14
x86: Implement semantics for a few instructions (#167)
* x86: Add aesenc, aesenclast, aesdec, aesdeclast

* x86: Add vpcmpgtd

* WIP

* Implement Pshufb

* Fix AESNI_AESEncLast.

* Fix PtCmpGt.

* Refactor AESNI instructions a bit

* Finish refactoring

* Forgot MultiWayIf

* Reduce duplication a bit

* Address comments

Co-authored-by: Andrei Stefanescu <andrei@stefanescu.io>
2020-10-08 19:37:17 -04:00
Sam Breese
5fdfdb2eaa
x86: Add some entries to the export list of Data.Macaw.X86 (#164) 2020-10-08 18:25:30 -04:00
Sam Breese
00d8530255
symbolic: Add special cases for null pointers in doPtrEq (#165) 2020-10-08 14:38:46 -04:00
Tristan Ravitch
cbc7a3ca31
Feature/aarch32 symbolic backend (#162)
aarch32-symbolic: Implement most of the remaining macaw-aarch32-symbolic bits

It should be usable now, modulo some execution-time semantics for the floating
point operations.  There will be a separate ticket covering the changes required
for them (some refactoring of how they are handled during translation is required).
2020-10-05 12:31:39 -07:00
Joe Hendrix
6a83d23989
Merge pull request #161 from GaloisInc/jhx/github-actions
Switch to GitHub actions
2020-09-29 14:55:54 -07:00
Joe Hendrix
0baa499c2a Migrate from Travis to Github Actions 2020-09-29 13:47:34 -07:00
robdockins
3c2d237a59
Merge pull request #159 from GaloisInc/crucible-mem-fix
Update to use new `HasLLVMAnn` API
2020-09-16 10:31:36 -07:00
Rob Dockins
e9b960c6d5 Bump semmc submodule 2020-09-15 16:24:24 -07:00
Rob Dockins
99f8cb0bdf Update to use new HasLLVMAnn API, which requires an action for
recording (or discarding) annotations rather than a map.
2020-09-11 14:40:02 -07:00
Sam Breese
b248cf7f45
x86: Add semantics for vpunpckhqdq, vxorps, vpaddb, and movbe (#155)
* Add semantics for vpunpckhqdq

* Add semantics for movbe

* Add semantics for vxorps and vpaddb
2020-08-20 14:50:20 -04:00
Kevin Quick
4713bc91c7
Merge pull request #157 from GaloisInc/llvm_annotations_upd
Update for addition of badBehaviorMap implicit for LLVM annotations.
2020-08-11 11:08:57 -07:00
Kevin Quick
de31610929
Update submodules. 2020-08-10 17:47:35 -07:00
Kevin Quick
1db2d1669c
[symbolic] Defer badBehaviorMap creation to caller instead. 2020-08-10 14:50:45 -07:00
Kevin Quick
fc419e4c18
[refinement] update for badBehaviorMap implicit parameter. 2020-08-10 13:47:44 -07:00
Kevin Quick
22f2a3122c
[x86_symbolic] Create badBehaviorMap earlier in test. 2020-08-10 09:48:50 -07:00
Kevin Quick
ad46e191c6
Update for addition of badBehaviorMap implicit for LLVM annotations.
See https://github.com/GaloisInc/crucible/pull/453
2020-08-08 22:16:48 -07:00
Daniel Matichuk
cd4dd31343
Merge pull request #156 from GaloisInc/feature/smartmux
aarch32: support non-concrete conditional writes
2020-08-06 14:19:03 -07:00
Daniel Matichuk
75d998f719 aarch32: avoid symbolic addresses
this changes the write action model to instead index
writes based on the macaw term representing the address
to be written
2020-08-05 16:53:27 -07:00
Daniel Matichuk
b42cce3f1c aarch32: support non-concrete conditional writes 2020-08-04 23:57:50 -07:00
Daniel Matichuk
f74cd557d5
Merge pull request #154 from GaloisInc/feature/normflat2
Update macaw-aarch32 for changes to the ASL translator
2020-08-03 15:04:03 -07:00
Daniel Matichuk
68193b9ef9 bump submodules 2020-07-31 00:33:10 -07:00
Daniel Matichuk
53db924e77 add macaw-asl-tests to travis CI 2020-07-31 00:31:29 -07:00
Daniel Matichuk
f1d3bb61da delete dead code 2020-07-31 00:31:29 -07:00
Daniel Matichuk
f2defdcdc4 aarch32: use empty tuple for unit type 2020-07-31 00:31:29 -07:00
Daniel Matichuk
204efeed42 Merge remote-tracking branch 'origin/master' into feature/normflat2 2020-07-28 12:43:24 -07:00
Daniel Matichuk
626071e459 bump submodules 2020-07-28 12:40:52 -07:00
Daniel Matichuk
44c2536f30 add default arch type override for ppc 2020-07-28 11:57:07 -07:00
Daniel Matichuk
dd8b78bb7b aarch32: fix floating point uf calls 2020-07-28 11:57:07 -07:00
Daniel Matichuk
278d365a31 aarch32: simplify write action representation 2020-07-28 11:57:07 -07:00
Daniel Matichuk
f53ea84cd9 module import cleanup 2020-07-28 11:57:07 -07:00
Daniel Matichuk
6e54d1488b avoid redundant let-bindings 2020-07-28 11:57:07 -07:00
Daniel Matichuk
468c329fa1 use compilation-friendly boolean and bitvector ops 2020-07-28 11:57:07 -07:00
Daniel Matichuk
838ef3924d aarch32: wrap up stateful operations as values 2020-07-28 11:57:07 -07:00
Daniel Matichuk
3e03ec11ab allow for arch-specific type translation 2020-07-28 11:57:07 -07:00
Daniel Matichuk
dcd5339b5a allow for manual bind pattern 2020-07-28 11:57:07 -07:00