GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-05 23:17:42 +03:00
Code Issues Projects Releases Wiki Activity
1,948 Commits 67 Branches 28 Tags 96 MiB
209686bb60
Commit Graph

285 Commits

Author SHA1 Message Date
Brian Huffman
e512dc2c17 Update test case output. 2018-06-15 14:15:39 -07:00
Brian Huffman
b3df205e04 Adapt test output to new primitives. 2018-06-15 10:18:02 -07:00
Brian Huffman
570f0be2ea Remove redundant fin constraint from the type of demote. 
`fin bits` and `bits >= width val` together imply `fin val`.
 2018-06-14 12:33:20 -07:00
Brian Huffman
dda5d34131 Fix constraints on type of primitive intmod. 
The old type did not forbid literals of the invalid type `Z inf`.
 2018-06-14 12:24:32 -07:00
Brian Huffman
50f54c9610 Fix test output due to addition of new primitive. 2018-06-14 06:22:59 -07:00
Brian Huffman
ab000984d2 Remove redundant prelude functions not, extend, and extendSigned. 
These were recently moved here from Cryptol::Extras. They are duplicates
of existing functions `complement`, `zext`, and `sext`.

See #427.
 2018-05-24 14:41:09 -07:00
Aaron Tomb
c42a135fce Update tests to account for Cryptol::Extras merge 2018-05-24 09:23:17 -07:00
Brian Huffman
62dfa1d58f Use sbv version 7.7. Fixes #486. 
Also add regression test for #486.
 2018-04-30 09:54:26 -07:00
Brian Huffman
3be72ae2cb Replace indexing primitives (!!) and (@@) with cryptol implementations. 2018-04-18 16:50:39 -07:00
Brian Huffman
2cdf9bd159 Replace primitives pmult, pmod, pdiv with cryptol implementations. 2018-04-15 06:56:20 -07:00
Diatchki
fcf5230bbd Fix build 
Make it work with GHC 8.2
 2018-04-03 09:55:31 -07:00
Aaron Tomb
02e9ea5ea5 Fix test output due to re-sorting environment 2018-04-02 15:35:10 -07:00
Aaron Tomb
0bbb7fa6ec Fix tests with GHC 8.4.1 2018-04-02 15:35:03 -07:00
Brian Huffman
fccf55f30f Remove obsolete cvs-era $Header$ keywords. 2018-03-22 13:33:12 -07:00
Brian Huffman
5cd9141fe7 Add functions head and last to Cryptol prelude. Fixes #465. 
Also fix regression test output.
 2018-03-16 15:10:36 -07:00
Iavor Diatchki
01b72ce0f9 When a test fails, print a suggestion how to make the output gold. 2017-12-21 10:14:44 -08:00
Iavor Diatchki
2272a59314 Rename type synonyms properly. 2017-12-01 10:29:42 -08:00
Iavor Diatchki
3443331f06 Add a test 2017-12-01 09:51:43 -08:00
Iavor Diatchki
f658f0244d Add another test. 2017-11-28 14:26:12 -08:00
Iavor Diatchki
c5e0540a0f Fix test. 2017-10-30 14:24:47 -07:00
Iavor Diatchki
3f4cc570cf Use a record for all module parameters at the value level. Also improve PP 2017-10-25 16:39:29 -07:00
Iavor Diatchki
9ecc8f720d Add some tests. 2017-10-24 14:04:41 -07:00
Iavor Diatchki
ca6b34f621 Refactor module system things; better loading of `A modules. 2017-10-23 15:12:12 -07:00
Iavor Diatchki
d52c5f5938 Merge remote-tracking branch 'origin/master' into abstract-types 
# Conflicts:
#	src/Cryptol/Parser/ParserUtils.hs
 2017-10-20 14:07:47 -07:00
Brian Huffman
8db89ab3ee Add test case for issue #474. 2017-10-20 11:09:51 -07:00
Iavor Diatchki
b8780ab68f Add some tests. 2017-10-18 14:33:41 -07:00
Iavor Diatchki
043334f8f9 Name is cryptol nowadays 2017-10-16 14:05:17 -07:00
Iavor Diatchki
1f2cacbae5 Merge branch 'master' of github.com:GaloisInc/cryptol 2017-10-04 15:50:41 -07:00
Iavor Diatchki
5208739653 Don't print directly to stdout. Fixes #166 2017-10-04 15:50:31 -07:00
Brian Huffman
2b568897da Remove implicit Bit type signature on rhs of property declarations. 
Fixes #224.

It might be desirable to add some other check for `property` declarations
to make sure that their types are predicates of some arity.
 2017-10-04 15:26:17 -07:00
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
2885d469da Disabe the utf-8-ident test in a different way 
If you use a `.fails` file, then the test suite fails if that test
succeeds, which it does on most platforms.
 2017-07-21 12:25:44 -07:00
Aaron Tomb
bfe457f9ab Note that the test parser.utf-8-ident fails 
This fails on Windows and we don't really know how to fix it. The fact
that it always fails masks more interesting failures, so I think it's
better to just skip it for now.
 2017-07-21 11:04:06 -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
Iavor S. Diatchki
3c2c9a857a Fix test to account for printing of operators' precedences. 2017-02-08 16:07:54 -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
e9c8b6ccd1 Add regression test for bitshift operations 2016-08-22 15:36:16 -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
Brian Huffman
0024dd0300 Update test output 2016-08-10 13:49:09 -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
Trevor Elliott
3c59bf3231 Update the test output for mono-bind test 4 
The type variable name was the only change.
 2016-05-31 11:51:01 -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
Trevor Elliott
7976026789 Update test output renamer errors 2016-05-27 18:50:27 -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
10acbdbfb8 Add comment in README explaining how to run tests. 2016-03-04 09:05:47 -08:00
Thomas M. DuBuisson
b40c1ce25d Add known failure for issue 314. 2016-03-04 09:05:23 -08:00