GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-11 07:00:49 +03:00
Code Issues Projects Releases Wiki Activity
1,049 Commits 68 Branches 28 Tags 95 MiB
73d6a68c67
Commit Graph

1049 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Robert Dockins
73d6a68c67 Merge branch 'new-eval' of github.com:robdockins/cryptol into new-eval 2016-07-13 09:54:24 -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
Brian Huffman
c2e0cc5839 Remove unused AES functions. Fixes #352. 2016-07-07 14:40:08 -07:00
Adam C. Foltzer
8352132c14 Merge branch 'release/2.4.0' 2016-07-06 16:21:06 -07:00
Adam C. Foltzer
3c25c096a7 clean up build a bit 2016-07-06 16:20:01 -07:00
Thomas M. DuBuisson
8485f28a6b Add necessary type arguments to scytale example. 2016-07-05 15:07:14 -07:00
Adam C. Foltzer
054a3e2248 instantiate Scytale diameter 
Fixes #349
 2016-07-05 14:42:59 -07:00
Ryan Scott
117dc0a931 Put bench/data/*.cry in extra-source-files 2016-07-05 09:58:50 -07:00
Adam C. Foltzer
2c428804bc remove splitBy and update documentation 
Closes #291
 2016-07-05 09:58:49 -07:00
Adam C. Foltzer
78cacc4d3e Merge pull request #333 from RyanGlScott/master 
Put bench/data/*.cry in extra-source-files
 2016-07-05 08:49:53 -07:00
Adam C. Foltzer
6fd99ff3ab clean up build a bit 2016-06-27 14:59:10 -07:00
Robert Dockins
e0dc226787 Make random value generation work on a slightly larger class of types. 
Simplify types when calculating random generators to avoid spurrious
failures.
 2016-06-25 12:45:01 -07:00
Brian Huffman
2cface6f31 Parser disallows declarations like "f x # y = y". 
Fixes #342.
 2016-06-16 17:05:59 -07:00
Rob Dockins
cbdbe35a89 Tweak the thunk strategy for the evaulator, and make sure to 
eta-expand word values when necessary.
 2016-06-13 22:14:28 -07:00
Rob Dockins
88b6ae5bfa Squash some incomplete pattern match warnings 2016-06-13 22:12:16 -07:00
Robert Dockins
8ecb6898a6 Merge remote-tracking branch 'github/new-eval' into new-eval 2016-06-13 16:45:44 -07:00
Robert Dockins
c18df5df40 Fix up some most-merge problems 2016-06-13 16:43:25 -07:00
Robert Dockins
c3c1bb2c74 Merge branch 'master' into new-eval-merge 2016-06-13 16:29:36 -07:00
Robert Dockins
37fea4cd9d Remove the lexCompare case for infinite streams, which should never occur. 2016-06-13 16:23:39 -07:00
Robert Dockins
3f934ae27f Delete the unused cvt function 2016-06-13 16:02:27 -07:00
Rob Dockins
b9464335b9 Plug a space leak in the implementation of random sequences 2016-06-12 22:43:37 -07:00
Robert Dockins
98a9e16944 Move to directly pattern matching on the new type evaluation datatype 
instead of using helper destructor functions.
 2016-06-09 14:19:12 -04:00
Robert Dockins
d2789c0214 Start manually merging Brian's changes regarding type values and evaluation 2016-06-09 13:30:51 -04:00
Robert Dockins
b95b734b74 Refactoring of how bits and words are handled in the interpreters. 
The major change in this patch is to add a new type of 'WordValue'
which is always used to represent finite sequences of bits.  A word
value is either a packed word, or a sequence of lazy bits.  The 'VSeq'
constructor, in constrast, is now never used for a finite sequence of
bits.

This avoids certain thorny problems that arise when trying to faithfully
implement the lazy semantics of Cryptol.  We now do not have to commit
to a value at type '[n]' being represented as a packed word or as an
unpacked word until relatively late.  This allows us to perform type-directed
eta-expansion at every recursive call before we know how words will be represented.

This patch fixes all the outstanding strictness bugs that I know of.

Unfortunately, we seem to lose some ground on performance.  The new evaluator
is now about 5% slower than the old one on the AES benchmark, and quite a bit
slower on the SHA1 benchmark.  Fortunately, the use if LRU caches for memoization
of sequences seems to keep heap usage to manageable levels; so programs generally
complete, even if they take a long time.
 2016-06-09 08:31:23 -04:00
Adam C. Foltzer
20965a0b0b fully qualify cygpath to avoid weird hemlock error 2016-06-08 16:56:22 -07:00
Adam C. Foltzer
921b50a1a9 add GHC 8 stackage nightly 2016-06-07 14:29:20 -07:00
Adam C. Foltzer
76be770d83 clean up 7.8-isms 2016-06-07 13:40:15 -07:00
Brian Huffman
1e3d1f642a New evalType function works on either kind * or # 
Cryptol.Eval.Type now provides three evaluation functions
for types:

  evalType    :: EvalEnv -> Type -> Either Nat' TValue
  evalValType :: EvalEnv -> Type -> TValue
  evalNumType :: EvalEnv -> Type -> Nat'

evalValType requires the type to have kind *.
evalNumType requires the type to have kind #.
evalType works on a Cryptol types of either kind.
 2016-06-06 15:43:22 -07:00
Brian Huffman
9fb3d53d88 TValue represents only value types; Nat' is for size types 
We now have separate evalType and evalNumType functions
for use with kind * and #, respectively.
 2016-06-06 15:10:31 -07:00
Brian Huffman
38f143abcc Pattern match on TValues instead of discriminator functions 2016-06-06 13:31:44 -07:00
Brian Huffman
4de0580d1c Redefine type TValue as an inductive datatype. 
This mostly takes care of issue #343, but some problems
remain:

- There is no TValue representation for newtypes
- Many incomplete pattern warnings in Symbolic/Prims.hs
 2016-06-06 11:36:14 -07:00
Robert Dockins
99526f5700 Merge branch 'master' of github.com:GaloisInc/cryptol into new-eval 2016-06-01 15:22:09 -07:00
Adam C. Foltzer
7c9d2a5158 tweak JSON deriving for cryptol-server 2016-05-31 16:11:50 -07:00
Adam C. Foltzer
875d78800f add note about Z3 on 64-bit Linux 2016-05-31 15:47:50 -07:00
Trevor Elliott
e974a1159b Correct the printing of names with the parsed AST 
Fixes #340
 2016-05-31 14:04:05 -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
Trevor Elliott
e0d52087b5 Fix type renaming in patterns 
Fixes #341
 2016-05-31 10:59:26 -07:00
Thomas M. DuBuisson
d9ba571286 Merge branch 'master' of https://github.com/GaloisInc/cryptol 2016-05-31 10:39:11 -07:00
Thomas M. DuBuisson
363651c907 Fixes #320 Use -N1, not -N, as the default RTS option. 2016-05-31 10:38:13 -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
Brian Huffman
0623fdcc63 Evaluate types of predicates before checking their validity 
Fixes #339.
 2016-05-31 10:15:12 -07:00
Rob Dockins
db28a2f719 Fix a bug that somtimes mixed up the length with the element type of 
a comprehension match statement.
 2016-05-31 08:54:36 -07:00
Rob Dockins
bdcfdd39a1 Update benchmarks for new interpreters 2016-05-30 23:07:05 -07:00
Rob Dockins
e69f790661 Add a utility function for forcing internal thunks in interpreter values. 2016-05-30 22:06:11 -07:00
Rob Dockins
9075c98f36 Make the implementation of "random" in the symbolic simulator more lazy. 
We only want to panic if the thunk is acutally forced.
 2016-05-30 22:04:26 -07:00
Rob Dockins
2d19a3d39c Fix a bug with the implementation of extractWord for symbolic values. 2016-05-30 22:02:29 -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
Rob Dockins
a54c4b0952 Implement the 'trace' primitive in the symbolic simulator. 
When executing symbolically, the trace primitive produces no
output, and merely forces its first two arguments.
 2016-05-30 17:48:24 -07:00