Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Tweak the term model to avoid a panic situation #1368

Merged
merged 2 commits into from
Jul 6, 2021
Merged

Tweak the term model to avoid a panic situation #1368

merged 2 commits into from
Jul 6, 2021

Commits on Jul 2, 2021

  1. Tweak the term model to avoid a panic situation. 

    This would occur when concrete nat values were round-tripped
via a bitvector type in the term model, and into a sequence
indexing primitive.

This tweak fixes a particular instance of this problem, but
highlights the fact that we need much more robust handing of the
sequencing primitives and natural numbers.
    @robdockins
    robdockins committed Jul 2, 2021
    Configuration menu
    Copy the full SHA
    cb59fc6 View commit details
    Browse the repository at this point in the history

  2. Remove a variety of panic cases in the saw-core simulator primitives. 

    Also, add a switch that controls if the evalutor will be have in
a "symbolic" way.

Adding a new `PrimExcept` constructor that allows primitives to
cause fallback behavior after examining all their arguments.
As with the existing `PrimFilterFun`, this causes term reconstruction
in the term model evaluator, and raises an error in the other evaluators.
We use this new type of primitive to remove cases that would otherwise
panic.

In addition, we add a flag to the `BasePrims` record that controls
if we do symbolic muxing for sequence operations and `ite`. For the
term model, we disable this behavior and fall back earlier on term
reconstruction. This avoids constructing large mux trees in some cases.
    @robdockins
    robdockins committed Jul 2, 2021
    Configuration menu
    Copy the full SHA
    1bbcad4 View commit details
    Browse the repository at this point in the history