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