GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 14:06:13 +03:00
Code Issues Projects Releases Wiki Activity
3,086 Commits 68 Branches 27 Tags 82 MiB
gitpod
Commit Graph

3086 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Matthew Yacavone
ff26feb83c add test_DES, fix string literals in test_SHA256 2021-04-15 13:38:13 -04:00
Matthew Yacavone
1a34e05361 Merge branch 'master' into rpc/more-examples 2021-04-15 12:57:43 -04:00
Andrew Kent
34749601e6
Merge pull request #1159 from GaloisInc/rpc/feat/check 
feat(rpc): check, AES example/test
 2021-04-14 14:53:12 -07:00
Matthew Yacavone
ec2a23abf1 add SHA256 test, add from_cryptol_arg to CryptolEvalExpr 2021-04-14 17:33:06 -04:00
robdockins
76d1dc9df7
Merge pull request #1136 from GaloisInc/word-eval-refactor 
Word eval refactor
 2021-04-14 08:39:23 -07:00
Rob Dockins
3f66dbf713 Rework memoMap to squash space leaks. 
The main benefit of this reorganization is that it
notices when a memoized `SeqMap` has been forced
at all of its locations.  This allows us to
discard the underlying computation, which will
never need to be consulted again.  This, in turn,
allows the garbage collector to reclaim the associated
memory and help prevent certain classes of space leaks.
 2021-04-13 16:14:57 -07:00
Rob Dockins
29c5bc9224 Fixes that help a small amount with space leaks 2021-04-13 15:35:57 -07:00
Felix Yan
6d17c2e97b
Allow sbv 8.14 
Tested to build fine here.
 2021-04-14 03:33:21 +08:00
Rob Dockins
aac42f4991 Fix test suite 2021-04-13 10:27:17 -07:00
Rob Dockins
69ad34b231 Add test case for issue640 
I think we've finally cracked the nut on this strictness bug.
Fixes #640
 2021-04-13 10:27:17 -07:00
Rob Dockins
31ab387c19 Update the test for issue 211 to restore the old test behavior. 
Also, test for looping computations in addition to `error` computations.
This doesn't let us cheat by eta-expanding the error, as we were
doing before.
 2021-04-13 10:27:17 -07:00
Rob Dockins
838a252770 Make the "large bit size" a bit more reasonable. 2021-04-13 10:27:17 -07:00
Rob Dockins
d4c3402496 Make joinWords lazier in its arguments 2021-04-13 10:27:17 -07:00
Rob Dockins
5d96829dcd Increase the strictness in the SuiteB SHA padding function. 
With the lazier join operator, this squashes a space leak in examples that
do a lot of hashing.
 2021-04-13 10:27:17 -07:00
Rob Dockins
77f6718766 Make joinWordVal lazier in its arguments. 2021-04-13 10:27:17 -07:00
Rob Dockins
f7d66df8e2 Keep a thunk for packed words alongside bitmap representations. 
This lets us share work, and lets us optimistically treat the word
as packed if we know it has already been forced.  It also lets
us delay unpacking decisions.
 2021-04-13 10:27:17 -07:00
Rob Dockins
6853ba0330 Don't reexport the SeqMap API 2021-04-13 10:27:17 -07:00
Rob Dockins
5f4b979d0b Tweak the way delayWordValue works. 
This should eliminte the possiblity of building up chains
of thunked word values.
 2021-04-13 10:27:17 -07:00
Rob Dockins
149428c0d8 Remove the splitWordVal operation. 
Replace it with `takeWordVal` and `dropWordVal` instead.
 2021-04-13 10:27:17 -07:00
Rob Dockins
cc8822f736 Update reference implementation and documentation 2021-04-13 10:27:17 -07:00
Rob Dockins
b812cd5036 Temporary fix to the test for issue211. 
We should either decide that the semantics of `#` requires it to be
strict in its arguments, or we should fix the definition.
 2021-04-13 10:27:17 -07:00
Rob Dockins
e65bf8cd0c Change largeBitsVal into bitmapWordVal. 
Update it's type to prepare for upcoming changes
 2021-04-13 10:27:17 -07:00
Rob Dockins
55a48ba34e Stop eta-expanding the error combinator. 
This breaks the test for issue211, but we were cheating
on it anyway.
 2021-04-13 10:27:17 -07:00
Rob Dockins
6d53e912e0 Fix another width accounting bug 2021-04-13 10:27:17 -07:00
Rob Dockins
62bcabac12 Fix a bug with width accounting 2021-04-13 10:27:17 -07:00
Rob Dockins
9823884083 typo 2021-04-13 10:27:17 -07:00
Rob Dockins
afd4cd6234 Try harder to see if thunks have already been forced. 2021-04-13 10:27:17 -07:00
Rob Dockins
f88b67d838 Make word updates more uniform between SBV and What4. 
Push word updating logic into the WordValue module, which
finally allows us to delete the abstraction leaking `viewWordOrBits`
family of helpers.
 2021-04-13 10:27:17 -07:00
Rob Dockins
7c3f1ac67b Implement signed right shift uniformly 2021-04-13 10:27:17 -07:00
Rob Dockins
9d4183975e Push word shifts into the Backend class and define shifts uniformly. 2021-04-13 10:27:17 -07:00
Rob Dockins
e7df405732 Fix import in cryptol-remote-api 2021-04-13 10:27:17 -07:00
Rob Dockins
07f4ba9d67 Make indexPrim lazier in its sequence argument. 2021-04-13 10:27:17 -07:00
Rob Dockins
d291318bdf Rework shifting in the concrete simulator to use the same code paths 
as the symbolic simulators.
 2021-04-13 10:27:17 -07:00
Rob Dockins
8ca536d387 Reduce the amount of sequence memoization that occurs in shifts. 
Memoization now only occurs in the barrel shifter when a symbolic
bit is encountered, instead of at every shift.
 2021-04-13 10:27:17 -07:00
Rob Dockins
ebc83275ad Consolidate some code related to indexing and shifting. 
Introduce the concept of "index segments", which allows us to
delay deciding if index values should be treated as packed
or unpacked until they are consumed in an indexing operation.
 2021-04-13 10:27:17 -07:00
Rob Dockins
a2aa432420 Continue consolidating WordValue code into the related module 2021-04-13 10:27:17 -07:00
Rob Dockins
6bf4d2e44e Remove uses of panic in SeqMap 2021-04-13 10:27:17 -07:00
Rob Dockins
69a589d151 Update the reference interpreter 2021-04-13 10:27:17 -07:00
Rob Dockins
50117717a5 Tweak split, join, reverse and transpose. 
Make sure they are sufficently lazy in their arguments.
Join is still to eager in some cases, but that will require
a larger refactoring.
 2021-04-13 10:27:17 -07:00
Rob Dockins
b5454bce29 Fix test suite 2021-04-13 10:27:17 -07:00
Rob Dockins
d3accfb042 Make take and drop primitive instead of splitAt. 
This allows us to generalize the type of `take` and simplifies
the implementations.
 2021-04-13 10:27:17 -07:00
Rob Dockins
a112ed8cf7 Update cryptol-remote-api 2021-04-13 10:27:17 -07:00
Rob Dockins
87d8912fa3 Complete the job of making SeqMap abstract. 2021-04-13 10:27:17 -07:00
Rob Dockins
3f185449ee Move WordValue into a separate module. 2021-04-13 10:27:17 -07:00
Rob Dockins
7fc748d9f9 Complete the process of making WordVal abstract. 2021-04-13 10:27:17 -07:00
Rob Dockins
b9635b26dc Relocate most of the logic that works directly on WordValue values 
into the `Value` module.  Remove most uses of the `WordValue` constructors
in other modules, but don't quite make the type abstract yet.
 2021-04-13 10:27:17 -07:00
Rob Dockins
3f710468e8 Break SeqMap out into a separate module 2021-04-13 10:27:17 -07:00
Rob Dockins
5a84ea5b58 Squash warnings 2021-04-13 10:27:17 -07:00
Rob Dockins
b24e2f5130 Remove the eta delay mechanisim from the evaluator. 
This brings the evaluator more in line with the reference semantics,
although there may still be some differences.
 2021-04-13 10:27:17 -07:00
Rob Dockins
3942a3decf Rework the # operator. 
It is now lazier in its arguments when required.
 2021-04-13 10:27:17 -07:00