Rob Dockins
364d586c7c
Bump what4 submodule
2020-04-27 14:19:44 -07:00
Rob Dockins
c04bcdf633
Update appveyor config
2020-04-27 14:19:44 -07:00
Rob Dockins
402ecf20dd
update travis and cabal.freeze files
2020-04-27 14:19:44 -07:00
Rob Dockins
ed9742be5c
Use panic instead of fail
2020-04-27 14:19:44 -07:00
Rob Dockins
85d727720d
Add sbv-any and sbv-offline to the no-warnings list
2020-04-27 14:19:44 -07:00
Rob Dockins
525ca4a6ec
Track what4 updates. Transition to use bvAtBE bvSetBE, etc.
2020-04-27 14:19:44 -07:00
Rob Dockins
8c9b9e9c53
Add "prefixed" versions of the SBV backend solvers in addition
...
to the default unprefixed ones (which are currently still
SBV-based).
2020-04-27 14:19:44 -07:00
Rob Dockins
d1bc32ba97
Update CHANGES
2020-04-27 14:19:44 -07:00
Rob Dockins
904220c806
Add What4 provers alongside the SBV provers with names such as w4-z3,
...
`w4-yices`, etc. Implement What4 based "offline" solving using
the pseudo-solver name `w4-offline`.
2020-04-27 14:19:44 -07:00
Rob Dockins
aaa0ea1744
Improve the what4 symbolic frontend. Individual solvers can
...
now be selected, and multisat queries are now supported.
2020-04-27 14:19:44 -07:00
Rob Dockins
5277c80522
Do explicit modular reduction for Z operations when the inputs are concrete.
2020-04-27 14:19:44 -07:00
Rob Dockins
922350ff7a
Put together enough of the framework required to run :sat and :prove
...
queries via What4. We still need to support configuring the solver to use,
multisat queries, and portfolio solving.
2020-04-27 14:19:44 -07:00
Rob Dockins
44a2b8e236
Very basic scaffolding for using what4 as a symbolic backend
2020-04-27 14:19:44 -07:00
Rob Dockins
1e1f7af812
Fix the haskeline package upper bound
2020-04-23 17:37:53 -07:00
robdockins
f29f0158ff
Merge pull request #703 from GaloisInc/issue702
...
issue702
2020-04-23 12:22:25 -07:00
brianhuffman
aa6030ba07
Merge pull request #708 from GaloisInc/fix-iterate
...
Redefine prelude function `iterate` to preserve sharing.
2020-04-22 11:22:17 -07:00
Brian Huffman
4dd77c756b
Update type variable numbering in test suite output.
2020-04-20 11:29:49 -07:00
Brian Huffman
0203244cd6
Redefine prelude function iterate to preserve sharing.
...
Fixes #707 .
2020-04-18 08:12:40 -07:00
brianhuffman
30b41e9c45
Merge pull request #700 from GaloisInc/fix-warnings
...
Fix warnings about redundant imports.
2020-04-18 06:34:52 -07:00
Rob Dockins
ce85155dbe
Add unit test for issue702
2020-04-17 17:48:44 -07:00
Rob Dockins
9434236cbd
Enforce a canonical field ordering in the field type constructor for FinType
...
This solves another manifestation of issue #702 .
2020-04-17 17:48:28 -07:00
Rob Dockins
194d02d06d
Sort the fields of a record type before comparing with the fields in
...
a concrete value in `toExpr`.
Fixes #702
2020-04-17 17:09:58 -07:00
robdockins
d8bf07320f
Merge pull request #638 from rjnw/master
...
Fix for freevars and adding some exports.
2020-04-17 16:25:01 -07:00
Brian Huffman
21a09179ff
Fix warnings about redundant imports.
2020-04-09 13:10:29 -07:00
Rob Dockins
c83f831763
Fix benchmark suite
2020-04-03 14:47:16 -07:00
robdockins
87ad864185
Merge pull request #684 from GaloisInc/eval-refactor
...
Evaluator refactor
2020-04-02 09:42:04 -07:00
Rob Dockins
d08046d063
Test case for issue #662
2020-04-02 09:40:44 -07:00
Rob Dockins
4c6424c8a7
Fix for #662 .
...
This fix interprets integer division as "round down" division
in the symbolic simulator, to match the behavior of the concrete
simulator.
2020-03-30 22:53:10 -07:00
Rob Dockins
943e11478a
Add regression test for word updates
2020-03-30 15:09:53 -07:00
Rob Dockins
cfef882fe5
Minor tweaks in the concrete evaluator
2020-03-30 13:40:59 -07:00
Rob Dockins
bdfd4e6bc0
Add INLINE and SPECIALIZE pragmas to generate better code for the
...
concrete evaluator.
2020-03-30 13:01:06 -07:00
Rob Dockins
34ce8ecc00
Change uses of Z 0 to cause panics. The type constraints for
...
`Z` should make these cases impossible.
2020-03-30 09:54:27 -07:00
Rob Dockins
c94c929354
Comment tweaks
2020-03-30 09:35:00 -07:00
Iavor S. Diatchki
761930257d
Merge pull request #690 from GaloisInc/feature/689
...
Feature/688
2020-03-27 10:25:08 -07:00
Rob Dockins
ffdf11d202
Minor style and bugfixes
2020-03-26 16:03:35 -07:00
Rob Dockins
058847f138
Break the symbolic query description datatypes into a separate
...
module, moving SBV specific code into `Cryptol.Symbolic.SBV`
2020-03-26 09:23:00 -07:00
Iavor Diatchki
fcc7a19998
More information when browsing.
...
This implements the feature request in #689
2020-03-24 16:53:48 -07:00
Iavor Diatchki
ec36d1aa38
Just comments and clean-up. Should contain no semantic changes.
2020-03-23 15:05:31 -07:00
Rob Dockins
0ce797f0c9
Fix a bugged implementation of symbolic bit update for SBV words.
2020-03-23 14:49:17 -07:00
Rob Dockins
d26966101f
Promote the logicShift out of the SBV module into a generic implementation.
...
The concrete evaluator still uses a direct implementation, but this
one, based on a barrel-shifter, can also be used byt the what4 backend.
2020-03-23 14:49:05 -07:00
Rob Dockins
c2459cedb4
Minor consolidation/fixes to primitive definitions
2020-03-19 17:31:43 -07:00
Rob Dockins
20ad7e8e86
Remove the "round-to-zero" versions of integer division and modulus,
...
since we're going to restrict signed division to bitvectors.
2020-03-19 17:30:14 -07:00
Rob Dockins
72cf1ccd18
Implement the non-ring operations on Z_n via translation to integers
...
directly in the `Backend` class definition. Each backend was
essentially doing this anyway.
Also add an `integerAsLit` operation.
2020-03-19 16:44:38 -07:00
Rob Dockins
6029ed2198
More documenation in Backend
2020-03-18 14:31:16 -07:00
Rob Dockins
c3ab80721f
use wordAsChar
2020-03-18 14:30:54 -07:00
Rob Dockins
0cb075ead6
Rename intModXXX operations to znXXX. These names are less confusing.
2020-03-18 13:48:12 -07:00
Rob Dockins
5af4469fe1
Reorganize sequence index and update operations. They now uniformly
...
check for index in bounds conditions, and the interface between
the backend-specific operations is cleaned up.
2020-03-18 13:17:49 -07:00
Rob Dockins
9ed0c1d3a9
Make error handling uniform across the symbolic and concrete backends.
...
Any non-concrete values in error messages are rendered as '?'
2020-03-18 08:28:36 -07:00
Rob Dockins
bc99e7d791
Take bitLit out of the SEval monad. The backends all support
...
a non-monadic version of bit literals, and it's somewhat more convenient.
2020-03-17 15:17:25 -07:00
Rob Dockins
47959c55cc
Rearrange/reorganize the primitive tables for the SBV and Concrete
...
backends to make them line up, and make it more obvious that most
of the primitives are uniformly defined for both backends.
The remaining primitives that have significant structural differences
are the sequence indexing and updating primitives, the shifts/rotates,
and `error`, `random` and `trace`.
While doing this, push the various to/from integer coercions
into the `Backend` class and make the operations uniform.
2020-03-17 15:04:36 -07:00
