GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-07 08:19:12 +03:00
Code Issues Projects Releases Wiki Activity
1,862 Commits 67 Branches 28 Tags 96 MiB
f96e1e49fb
Commit Graph

204 Commits

Author SHA1 Message Date
Brian Huffman
3a154f948a Add regression test for issue #463. 2017-10-04 13:47:24 -07:00
Rob Dockins
2df09a428a Change how test coverage statistics are computed. 
This formulation accounts for the fact that test vectors
are chosen randomly with replacement.

Fixes #461
 2017-10-03 17:37:48 -07:00
Rob Dockins
9785ed1e32 Add a rule to the numeric solver for "linear unifiers" 
Check for situations where a unification variable is involved in
a sum of terms not containing additional unification variables,
and replace it with a solution and an inequality.
`s1 = ?a + s2 ~~> (?a = s1 - s2, s1 >= s2)`

Fixes #212
 2017-10-03 12:49:17 -07:00
Rob Dockins
e7d3ed02f9 Add testcase for issue #389. 
Recent improvements to the numeric solver have fixed this issue.

Fixes #389.
 2017-10-02 18:15:02 -07:00
Rob Dockins
42064dd9f2 Add testcase for issue #325. 2017-10-02 17:49:12 -07:00
Rob Dockins
37f9dc4c4f Add test for issue #78. 
Fixes #78.
 2017-10-02 15:48:51 -07:00
Rob Dockins
d5bfb1b648 Minor update to test suite 2017-10-02 15:40:46 -07:00
Brian Huffman
940b9c80ec Merge branch 'integer' 2017-09-29 14:23:28 -07:00
Brian Huffman
5e4d094eb3 Fix test output due to counterexample printing change. 2017-09-29 14:23:18 -07:00
Brian Huffman
cce32a4868 Merge branch 'master' into integer 
This brings the Logic and Zero type classes into the integer branch.
 2017-09-28 13:18:27 -07:00
Brian Huffman
1ed5640339 Merge branch 'master' into logic-class 
# Conflicts:
#	tests/mono-binds/test05.icry.stdout
 2017-09-26 16:50:53 -07:00
Iavor Diatchki
60523d5986 Delete old solver stuff. 
The main user visible effect of this might be that sometime things on
the Cryptol command line are instantiated in a slightly different way:
we get `inf` sometimes when we got a finite example before.

We could work around this if it is an issue, but I am not sure which
behavior is more reasonable.
 2017-09-26 14:02:52 -07:00
Brian Huffman
35423d0243 Update test output. 2017-09-15 16:38:03 -07:00
Brian Huffman
860060c085 Fix test output. 2017-09-15 14:05:27 -07:00
Brian Huffman
5332d98261 Fix test output 2017-09-13 17:04:52 -07:00
Robert Dockins
ef047d3a19 Fix test breakage due to new operations in the Cryptol prelude. 2017-08-16 17:37:24 -07:00
Robert Dockins
063e3ba898 Update test suite to track typo fix 2017-07-31 14:39:01 -07:00
Robert Dockins
0b9c186132 Make 'random' compute on concrete inputs in the symbolic evaluator. 
This patch does not add a warning when using 'random' in symbolic expressions.
We currently don't have any organized mechanism for generating warnings during
evaluation, and the value of emitting such a warning is debatable.

Fixes #364
 2017-07-27 15:45:37 -07:00
Robert Dockins
36dcd49803 Update the test suite now that issue #116 is fixed. 2017-07-26 15:31:36 -07:00
Aaron Tomb
a04f236169 Update test output for SBV 7.0 
With SBV 7.0, we get back satisfying assignments in a different order.
We should probably adjust this test to be less fragile eventually.
 2017-07-20 09:33:56 -07:00
Iavor Diatchki
4a43c675d9 When checking a binding, treat schema validation constraints 
just like any other constraint from the definition.

In particular, if the schema validity depends on an outer context,
the constraints should be solve in that outer context, not here.

Fixes #314
 2017-07-10 17:35:49 -07:00
Iavor Diatchki
affcc25156 Don't crash when we detect and error, tell the user instead! 
Also, improve the printing of the errors a bit.
 2017-07-10 11:59:39 -07:00
Iavor Diatchki
771c2deaa1 Slightly different error messages, should be OK. 2017-07-10 11:06:14 -07:00
Iavor Diatchki
1e4fb89f4c Fix test, due to changes in the Prelude. 2017-07-10 11:05:59 -07:00
Aaron Tomb
e282c65a7e Fix test failures from latest type checker changes 
Recent changes resolved issue 002, so we no longer need to indicate that
it's expected to fail. Other small changes to the type checker have
made things like type variable numbers change slightly.
 2017-06-20 10:08:36 -07:00
Brian Huffman
9a267b1f0c Removed definition of binary infix (~) from Cryptol prelude. Fixes #423. 
This change partially reverts changeset c620cbf2, which fixed #296,
which was about supporting `:t (~)` in the REPL.

As of this change, `:t (~)` will no longer work in the REPL.
The regression test for issue #296 is removed.
 2017-05-24 09:39:50 -07:00
Robert Dockins
d891fde0c7 Fix a corner case for join on 0-length inner sequences. 
Both the standard and the reference interpreter were producing
incorrect behaviors.  The correct behavior is to return an
empty sequence.

Fixes #395.
 2017-05-10 17:49:37 -07:00
Robert Dockins
7add78ec3c Implement a missing case in the definition of 'transpose'. 
Fixes issue #407
 2017-05-10 16:54:26 -07:00
Brian Huffman
e23a8175cc Add regression tests for #406, #408, and #410. 2017-05-05 14:17:45 -07:00
Iavor S. Diatchki
27eaec689d Fix test. There is indeed defaulting that should be happening here. 2017-02-15 10:02:15 -08:00
Iavor S. Diatchki
5e1a3b6f5a This one works now. 2017-02-15 09:08:15 -08:00
Iavor S. Diatchki
ec58bec6aa Add .cryptolsrc files 2017-02-15 09:08:02 -08:00
Iavor S. Diatchki
2c3145a417 Fix some of the broken tests. 2017-02-08 17:24:15 -08:00
Brian Huffman
dafd48cad0 Simplify type of primitive function 'pmult'. Fixes #366. 
Old: (fin a, fin b) => [a] -> [b] -> [max 1 (a + b) - 1]
New: (fin a, fin b) => [1 + a] -> [1 + b] -> [1 + a + b]
 2016-09-20 15:13:40 -07:00
Brian Huffman
2300a73a76 Add regression test for issue #382. 2016-09-20 11:25:01 -07:00
Brian Huffman
22bb49b3b5 Add regression test for issue #368. 2016-09-19 11:57:06 -07:00
Robert Dockins
3becedd910 Update tests to remove spurious failures 2016-08-18 16:05:23 -07:00
Robert Dockins
28d4f1d3fe Modify 'updates' and 'updatesEnd' to take the indices and values 
as separate vector arguments, rather than as a single vector
argument of pairs.
 2016-08-16 14:36:46 -07:00
Robert Dockins
64267f51ac Add the short-cutting boolean operators (/\), (\/), and (==>) 
to the Cryptol prelude.  This is in service of eventually addressing
issue #241.
 2016-08-12 17:12:34 -07:00
Robert Dockins
f746ef0d66 Fix test suite after changes to Cryptol prelude altered output 2016-08-12 12:22:58 -07:00
Brian Huffman
46793ade99 Rename test "issue289" to "trac289" 
Renamed because this test does not correspond
to github issue number 289.
 2016-08-10 14:07:11 -04:00
Robert Dockins
5d1e1948d8 Add test case to demonstrate tracing, as discussed in issue 68. 
The new evaluator allows us to have more direct control over
evaluation order, and makes it straightforward to implement tracing
primitives.  There are two new primitives 'trace' and 'traceVal' in the
Cryptol prelude that produce tracing output when evaluated.
Fixes #68
 2016-07-13 15:09:56 -07:00
Robert Dockins
e001310299 Add test cases for issue 138. Fixed by new evaluator. 
Fixes #138
 2016-07-13 15:00:00 -07:00
Robert Dockins
3d68677d42 Add test case for issue #268. Fixed by the evaluator rewrite 
Fixes #268
 2016-07-13 14:40:44 -07:00
Robert Dockins
869670b2af Add test case for issue #334. This issue is fixed by the evaluator rewrite. 
Fixes #334
 2016-07-13 14:36:26 -07:00
Robert Dockins
998bddc7a7 Merge remote-tracking branch 'origin/master' into new-eval 
Fix some minor conflicts in the test suite.
Conflicts:
	tests/issues/issue002.icry.fails
	tests/issues/issue148.icry.stdout
	tests/issues/issue198.icry.stdout
	tests/issues/issue214.icry.stdout
	tests/issues/issue290v2.icry.stdout
	tests/issues/issue312.icry.fails
 2016-07-12 14:58:53 -07:00
Adam C. Foltzer
2c428804bc remove splitBy and update documentation 
Closes #291
 2016-07-05 09:58:49 -07:00
Adam C. Foltzer
6fd99ff3ab clean up build a bit 2016-06-27 14:59:10 -07:00
Robert Dockins
99526f5700 Merge branch 'master' of github.com:GaloisInc/cryptol into new-eval 2016-06-01 15:22:09 -07:00
Trevor Elliott
3d67018c70 Ignore the bytes output of issue220 2016-05-31 11:53:38 -07:00
Brian Huffman
3b524e1ae5 Fix test output for issue093. 
Since #171 was fixed in b77dd2a8, the tests and proofs
are run in the order they appear in the source file.
 2016-05-31 10:34:51 -07:00
Rob Dockins
cd515efdb1 Test suite maintenance 2016-05-30 18:16:45 -07:00
Rob Dockins
33710b6d25 Update unit test golden outputs 2016-05-30 17:51:08 -07:00
Trevor Elliott
a139c4e1d1 Fixes #304 2016-05-27 22:00:43 -07:00
Brian Huffman
c6144bd332 Update output for tests 256 and 335 
The :t command now parenthesizes the term when needed.
 2016-05-27 16:25:14 -07:00
Trevor Elliott
0393c8c54d Fixes #335 
The local type bindings from type annotations in patterns were not being
processed correctly, and built-in type/type-functions were getting shadowed in
binders.
 2016-05-24 11:58:55 -07:00
Robert Dockins
38946745c3 Add the 'lg2' type function as a synonym. 
Fixes #248
 2016-05-04 17:54:08 -07:00
Robert Dockins
b6a83d7cb8 Make a friendlier, non-panic error message for cases where patterns 
introduce nontrivial constraints.

Fixes #290
 2016-05-04 17:38:16 -07:00
Robert Dockins
c620cbf237 Update the parser to allow prefix operators in more places. 
This allows us to define (~) as a prefix operator symbol synonym
for `complement`.

Fixes #296.
 2016-05-04 16:26:36 -07:00
Trevor Elliott
cf979723b7 Fixes #322 
Just needed to recurse through the parens and infix cases in `appTys`.
 2016-04-07 21:26:21 -07:00
Brian Huffman
b77dd2a82a :prove checks properties in the order they appear in the source. 
Also add a regression test. Fixes #171.
 2016-03-10 11:36:41 -05:00
Thomas M. DuBuisson
b40c1ce25d Add known failure for issue 314. 2016-03-04 09:05:23 -08:00
Thomas M. DuBuisson
edb9373c4e Add test case for issue #314 2016-03-04 08:58:50 -08:00
Brian Huffman
1953223e9f Add test case for issue #312. 2016-02-19 11:53:33 -08:00
Brian Huffman
1322156d28 Remove trailing whitespace 2016-02-19 10:08:20 -08:00
Brian Huffman
6def46da69 Add (failing) test for issue #2. 2016-02-12 14:46:06 -08:00
Iavor S. Diatchki
f7823544cf Add a test for ticket #308 2016-02-09 11:56:44 -08:00
Brian Huffman
ab4f113084 Add regression test for issue #256. 2016-02-08 15:09:34 -08:00
Brian Huffman
9538c59d23 Fix shift/rotate by amounts greater than 2^63 in evaluator 
Also added regression tests. This should fix issue #306.
 2016-01-27 10:37:55 -08:00
Adam C. Foltzer
4029b6c15c add a test for #126 2016-01-19 18:18:03 -08:00
Adam C. Foltzer
07da2018b7 switch to more portable seeding for random 
The `random` primitive previously took a `[32]` seed, but this causes
inconsistency between 32-bit and 64-bit platforms when the seed is large
enough to wrap around in GHC's representation of an `Int`. This patch
switches to an API that seeds directly with four 64-bit words, and so
should behave the same way on our supported platforms.
 2016-01-19 18:17:34 -08:00
Adam C. Foltzer
ac85cec175 update test with counterexample that z3 produces 
These sorts of tests are inherently unstable, but since Z3 seems to
agree across our platforms on this one, this should help make tests quieter.
 2016-01-12 16:50:22 -08:00
Thomas M. DuBuisson
752310cd0d Merge branch 'master' into writeFile 2015-12-25 21:39:01 -08:00
Adam C. Foltzer
9c07fe1006 merge in the 2.2.6 changes, including z3 switch 2015-12-23 16:10:56 -08:00
Adam C. Foltzer
3ae0dda7ac switch to Z3 for typechecking and proving 
Note: the hardcoding in this patch is only for the 2.2 hotfix branch; in
the 2.3 branch we will only have to change the default setting for the
typechecker.
 2015-12-23 14:59:10 -08:00
Adam C. Foltzer
aeefab69a1 refactor :check and :exhaust 
This is to set up improvements to the cryptol-server, and therefore
pycryptol interface.

This patch also fixes a regression in pretty-printing output caused by a
previous error in fixity of the `<>` operator
 2015-12-22 18:17:20 -08:00
Thomas M. DuBuisson
3afdae127a Add known failure notice for issue 212 2015-12-10 12:36:06 -08:00
Thomas M. DuBuisson
b355dedcf8 Test files for read/write bytearray command. 2015-11-15 10:42:04 -08:00
Trevor Elliott
d71fd8a3ee Issue #148 is fixed now 2015-08-14 17:38:50 -07:00
Iavor S. Diatchki
c9e4fab6a8 Fix up tests. 2015-08-12 15:52:18 -07:00
Adam C. Foltzer
494bf6d92e tweak patch in 170e5953 to work for 7.8; add test 2015-07-01 12:31:37 -04:00
Trevor Elliott
4d469fa2ce Update test output 2015-06-29 16:34:11 -07:00
Trevor Elliott
9b7e46724c Give 100 fixity levels, and fix prelude fixity again 
Also fix issue198, which had been accidentally updated while failing
 2015-06-10 11:55:54 -07:00
Trevor Elliott
fb98af636a Slight test output change 2015-06-09 17:02:07 -07:00
Trevor Elliott
88e44a5937 Location information changed in test 101 2015-06-09 14:45:51 -07:00
Trevor Elliott
f06b4deaea Update 226 output, as it uses :browse 2015-06-09 14:32:17 -07:00
Trevor Elliott
ae6b5dc3e8 Add support for user-defined infix operators 
Squashed commit of the following:

commit 9f03b7cd1a1f169ea192d735890fd6a3503ecb39
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Jun 3 11:40:27 2015 -0700

    Add a test for user-defined infix operators

commit 31656a4640e8189b880fa1ce39779c07872ebe18
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Jun 3 11:39:43 2015 -0700

    Forgot to initialize some fields in the parser

commit 73bcb2e5961691f2258f5a7a12ee2dc92d1a1ad3
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed Jun 3 11:20:40 2015 -0700

    Fix unnecessary panics in the renamer

commit 03cd8130901fb7aeb12d41cc03ce970ce6571423
Author: Trevor Elliott <trevor@galois.com>
Date:   Mon Jun 1 01:29:36 2015 -0700

    Remove a debug print

commit 2934a56b31d51ac971204d3fea9f62bf8829573d
Author: Trevor Elliott <trevor@galois.com>
Date:   Mon Jun 1 01:26:32 2015 -0700

    User-defined operators

commit 47f4b37fc75accaf0284addc2382c341167b8b6b
Author: Trevor Elliott <trevor@galois.com>
Date:   Sun May 31 23:44:51 2015 -0700

    Parse signatures for infix operators

commit a1a11705c2eec6e669159756de2eb2cb19bcfa83
Author: Trevor Elliott <trevor@galois.com>
Date:   Sun May 31 23:28:56 2015 -0700

    Plumb fixity information through

commit 56134ac0d9fb919f280dabfcdab6506195816340
Author: Trevor Elliott <trevor@galois.com>
Date:   Sun May 31 22:03:55 2015 -0700

    Parse fixity declarations

commit f2db0ad5d47d478799dabf03a6cad9be7aec2191
Author: Trevor Elliott <trevor@galois.com>
Date:   Fri May 29 16:00:57 2015 -0700

    Update test output for location changes

commit 15949018865d3ac8efca1a081334a7213c25775c
Merge: 1bd7f16 52f3a83
Author: Trevor Elliott <trevor@galois.com>
Date:   Fri May 29 15:36:20 2015 -0700

    Merge remote-tracking branch 'origin/master' into wip/infix-operators

commit 1bd7f1602bd6bbf5693871f01ca65a4cf3ed3bf8
Author: Trevor Elliott <trevor@galois.com>
Date:   Fri May 29 15:30:14 2015 -0700

    Forgot to consider EParens in translateExprToNumT

commit d63435270d5ca5bdf37584e4781a655a685c9c3b
Author: Trevor Elliott <trevor@galois.com>
Date:   Fri May 29 15:29:47 2015 -0700

    Add | to the operator character set

commit 7be23372c4625bf20b8f8ccf94a148563417f6cb
Author: Trevor Elliott <trevor@galois.com>
Date:   Fri May 29 14:49:07 2015 -0700

    Fix the printing of #Uniq variables

commit f9110e159aa0c3ae7450fe7a4db2a8d275d9bc1a
Author: Trevor Elliott <trevor@galois.com>
Date:   Thu May 28 17:04:26 2015 -0700

    Fix some failing tests

commit 0582fd08cc402c7bfd2de2c02df14fa77906e37e
Author: Trevor Elliott <trevor@galois.com>
Date:   Thu May 28 16:12:18 2015 -0700

    Remove more primitives from the parser

commit f5dafd1ea7954b64f7949c754e0c94abd2598679
Author: Trevor Elliott <trevor@galois.com>
Date:   Wed May 27 18:02:52 2015 -0700

    Do fixity resolution during renaming
 2015-06-03 11:42:33 -07:00
Iavor S. Diatchki
52f3a836b4 Fix test output issues214. 
We get one warning per enumeration which seems reasonable.
 2015-05-27 15:35:24 -07:00
Trevor Elliott
5e92b00789 Fix #177 
Add a name mapping environment to the pretty printer to control how qualified
names get printed.
 2015-05-21 23:17:15 -07:00
Thomas M. DuBuisson
d553a33179 Fix #214: Add the test that shows the success. 
Notice the actual fix is in commit
342b1cf3ff
 2015-05-11 10:25:22 -07:00
Thomas M. DuBuisson
7457f7d5aa Example crash in HEAD (issue #214) 
This shows a type error in 2.2.3 but crashes HEAD.
 2015-05-08 13:56:53 -07:00
Thomas M. DuBuisson
fd4ed49fe5 @yav Another TC example for #212 
So I'm treating this issue as a running conversation centered around
this one topic, let me know if it gets old.
 2015-05-07 23:24:41 -07:00
Thomas M. DuBuisson
94abebdf01 Example type constraint width issues 2015-05-07 09:31:10 -07:00
Brian Huffman
f95d3fadb6 Add regression test for issue #211. 2015-05-05 11:49:12 -07:00
Trevor Elliott
69c9465cab Experiment with defaulting using the SMT solver 2015-04-03 15:12:36 -07:00
Iavor S. Diatchki
afd53bb6a1 Merge remote-tracking branch 'origin/master' into wip/cs 
Conflicts:
	cryptol.cabal
	src/Cryptol/TypeCheck/Solve.hs
	src/Cryptol/TypeCheck/Solver/CrySAT.hs
	src/Cryptol/TypeCheck/Solver/Selector.hs
 2015-03-30 11:29:20 -07:00
Adam C. Foltzer
0536d0f15a update copyright years 2015-03-24 11:19:52 -07:00
Adam C. Foltzer
fe1a2403c9 handle EvalErrors more gracefully in :check 
Fixes #114 (mostly; Ctrl-C still doesn't clean everything up, but fixing
that would require a whole lot of work).
 2015-03-16 17:17:36 -07:00
Brian Huffman
cadfaced80 Update test for issue #177 
The issue is not the set of names in scope, it is the type names
printed out by the :t command. It should use the same names that
are in scope in the module.

If the type of an expression contains a type synonym that is not
in scope at all, then I'm not sure what exactly it should do.
 2015-03-04 11:22:37 -08:00
Brian Huffman
0eb57b9674 Add test for issue #177. 2015-03-04 09:58:53 -08:00