Evaluator refactor #684
Evaluator refactor #684
Conversation
…ites. Uses of the `BitWord` operations now generally require an extra `sym` argument that makes the types unambiguous, and this propigates through quite a few functions. This other `sym` argument will be necessary when we make a `what4` backend, so it's a necessary refactor anyway.
use the `LargeBitsVal` representation. This simplifies a lot of code, and is probably more efficent in the most cases anyway.
This fits better into the current module structure, and is a lot less confusing.
into a `Generic` module. Refactor the `EvalPrims` class away, pusing the `iteValue` operation into `BitWord` and demoting the `evalPrim` operation into an ordinary (non-typeclass) operation.
a single new module `Crypol.Eval.SBV`.
modules. The module structure needs to be a bit more cut up than I would like to avoid module import cycles.
type to indicate concrete evaluation.
module. Push primitive type if/then/else operations into the `Backend` class, and promote `iteValue` and `mergeValue` to operations on generic values.
alongside the value being computed. For now, this is just the infrastructure; soon, we'll push the computation of side effects into the `Backend` class, where they can interact with this new monad.
that interact with the `SEval` monad. Also, finish pushing the methods of the `Arith` class into the evaluation backend where they can be generically referenced by both the concrete and symbolic evaluators.
and use generic implementations.
backends to make them line up, and make it more obvious that most of the primitives are uniformly defined for both backends. The remaining primitives that have significant structural differences are the sequence indexing and updating primitives, the shifts/rotates, and `error`, `random` and `trace`. While doing this, push the various to/from integer coercions into the `Backend` class and make the operations uniform.
a non-monadic version of bit literals, and it's somewhat more convenient.
Any non-concrete values in error messages are rendered as '?'
check for index in bounds conditions, and the interface between the backend-specific operations is cleaned up.
directly in the `Backend` class definition. Each backend was essentially doing this anyway. Also add an `integerAsLit` operation.
since we're going to restrict signed division to bitvectors.
…ntation. The concrete evaluator still uses a direct implementation, but this one, based on a barrel-shifter, can also be used byt the what4 backend.
module, moving SBV specific code into `Cryptol.Symbolic.SBV`
There was a problem hiding this comment.
This seems like a great improvement, overall. I only skimmed the files that were all additions or all deletions, assuming that most of those were from code being moved from one place to another. If you made notable changes along with moving them, I'd be happy to review those, too. Just let me know what those are.
|
Oh, another thing worth noting: this breaks |
|
There is a bit of a performance regression for random testing, though that's perhaps unavoidable with a new layer of indirection. Running |
|
OK, that's a good one to look at. I wonder if some |
`Z` should make these cases impossible.
concrete evaluator.
After quite a few INLINE and SPECIALIZE pragmas, I was able to get down to about 30% slowdown for the new simulator. That isn't great, but it isn't catastrophic either. Time profiles were extremely unhelpful, charging most of the runtime to |
|
That seems like a sufficient improvement to me. This is also only one benchmark. I'm quite happy to merge this as-is and focus on performance improvements as a separate effort later. |
This is basically a reorg/cleanup of evaluator-related code in Cryptol. The impetus for this is to make the upcoming new evaluation mode based on What4 to be easier to implement.
I don't think I'm quite done with what I want to do here, but I'd like to start CI looking at this branch.