GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-23 11:58:47 +03:00
Code Issues Projects Releases Wiki Activity
2,142 Commits 65 Branches 28 Tags 83 MiB
d08046d063
Commit Graph

2142 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
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
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
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
Rob Dockins
f016a9a9fc Define carry and scarry instead of making them primitive. 2020-03-17 13:25:39 -07:00
Rob Dockins
e079ab4cf6 Push the Logic, Cmp and SignedCmp class methods into the Backend 
and use generic implementations.
 2020-03-17 11:50:44 -07:00
Rob Dockins
31109c2143 Push error handling into the backend class using methods 
that interact with the `SEval` monad.  Also, finish pushing
the methods of the `Arith` class into the evaluation backend
where they can be generically referenced by both the concrete
and symbolic evaluators.
 2020-03-16 17:52:59 -07:00
Rob Dockins
9d74dd1383 In symbolic evaluation mode, use a monad that tracks safety conditions 
alongside the value being computed.  For now, this is just the infrastructure;
soon, we'll push the computation of side effects into the `Backend`
class, where they can interact with this new monad.
 2020-03-13 14:15:52 -07:00
Rob Dockins
b108bf0e79 Allow the evaluation monad to depend on the backend 2020-03-13 12:25:41 -07:00
Rob Dockins
71b2f8ce70 Rename the BitWord class into Backend, and split into a separate 
module.  Push primitive type if/then/else operations into the `Backend`
class, and promote `iteValue` and `mergeValue` to operations
on generic values.
 2020-03-13 12:04:27 -07:00
Rob Dockins
8718489531 Create a new sentinal datatype Concrete instead of using the unit 
type to indicate concrete evaluation.
 2020-03-11 14:08:30 -07:00
Rob Dockins
be45b4ea29 Move definitions specific to the concrete evaluator in to separate 
modules.  The module structure needs to be a bit more cut up than
I would like to avoid module import cycles.
 2020-03-11 10:26:22 -07:00
Rob Dockins
bdb8f49143 Refactor Cryptol.Symbolic.Prims and Cryptol.Symbolic.Value into 
a single new module `Crypol.Eval.SBV`.
 2020-03-09 14:32:07 -07:00
Rob Dockins
0341fd0480 Split out the primitive definitions used by multiple evalautors 
into a `Generic` module.  Refactor the `EvalPrims` class away,
pusing the `iteValue` operation into `BitWord` and demoting
the `evalPrim` operation into an ordinary (non-typeclass)
operation.
 2020-03-09 14:09:19 -07:00
Rob Dockins
fbbaed8c83 Rename module Cryptol.Prims.Eval into Cryptol.Eval.Concrete. 
This fits better into the current module structure, and is a lot
less confusing.
 2020-03-09 11:29:08 -07:00
Rob Dockins
d5a44a2d8d Drop the Show requirement for SBit, SWord and SInteger 2020-03-06 17:00:25 -08:00
Rob Dockins
0bee8c4167 Remove the BitsVal constructor for WordVal and instead exclusively 
use the `LargeBitsVal` representation.  This simplifies a lot of code,
and is probably more efficent in the most cases anyway.
 2020-03-06 13:40:49 -08:00
Rob Dockins
df4332ea48 Remove unnecessary NFData constraints/instances 2020-03-05 16:53:41 -08:00
Rob Dockins
ce06a16d13 Push BitWord operations into IO and fixup 2020-03-05 16:28:56 -08:00
Rob Dockins
cb82015cd5 Refactor the BitWord class to use associated types, and fixup use sites. 
Uses of the `BitWord` operations now generally require an extra `sym`
argument that makes the types unambiguous, and this propigates through
quite a few functions.  This other `sym` argument will be necessary
when we make a `what4` backend, so it's a necessary refactor anyway.
 2020-03-05 10:29:06 -08:00
Iavor Diatchki
3038eacf54 Add a test for record updating. 
This completes the implementation of record updates.
Fixes #399
 2020-01-21 11:35:19 -08:00
Iavor Diatchki
38471c0cbc Update utility script to use cabal exec 2020-01-21 10:56:09 -08:00
Iavor S. Diatchki
1e883e9f1d
Merge pull request #681 from GaloisInc/cabal-tweak 
Add cabal bounds to the `haskeline` package.
 2020-01-14 14:21:52 -08:00
Rob Dockins
918040f682 Add cabal bounds to the haskeline package. Apparently 
version 0.8 contains some breaking changes.
 2020-01-06 11:34:47 -08:00
Iavor S. Diatchki
be642ce32b
Merge pull request #678 from GaloisInc/ml_update 
Update cryptol-test-runner maintainer and license
 2019-12-24 09:50:22 -08:00
Kevin Quick
578d268b8e
Update cryptol-test-runner maintainer and license 2019-12-23 18:18:54 -08:00
brianhuffman
8132030263
Merge pull request #672 from GaloisInc/bh-fixity 
Refactor Fixity-related code
 2019-12-17 07:38:19 -08:00
Brian Huffman
330d4dd2d9 Refactor Fixity module so Cryptol.Utils.PP can import it. 
Also make some other parts of the code less dependent on the
internal representation of the Fixity datatype.
 2019-12-16 18:05:30 -08:00
Brian Huffman
aec6cb0a7e Add regression test for #670. 2019-12-16 18:02:56 -08:00
Brian Huffman
7211c9f251 Pretty-print infix type operators with unspecified fixity as infix. 
Fixes #670.
 2019-12-16 18:02:56 -08:00
brianhuffman
1ce2ef2c73
Merge pull request #675 from GaloisInc/remove-test444 
Revert "Add regression test for #444."
 2019-12-16 17:59:44 -08:00
Brian Huffman
3281e7c121 Revert "Add regression test for #444." 
This reverts commit 85bff672ef.

The error message in the expected output file `issue444.icry.stdout`
contained a system-specific absolute file path.

Fixes #673.
 2019-12-16 14:12:44 -08:00
brianhuffman
ce6f1edd24
Merge pull request #669 from GaloisInc/issue614 
Do renaming on types the same way we do renaming on expressions.
 2019-12-13 15:47:19 -08:00