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

Poor SMT generation for array lookups with concrete indices #371

Closed
travitch opened this issue Dec 11, 2019 · 0 comments · Fixed by #378
Closed

Poor SMT generation for array lookups with concrete indices #371

travitch opened this issue Dec 11, 2019 · 0 comments · Fixed by #378
Labels
what4

Comments

@travitch
Copy link
Contributor

The function sbConcreteLookup has a case where it tries to be smart in the case where an array was constructed with a set of values assigned to concrete indices. This works well when the index being looked up is concrete; however, in the case where the looked up index is symbolic, it creates a mux over all of the possible values in the concrete map. See

crucible/what4/src/What4/Expr/Builder.hs

Line 3514 in b5ba511

Nothing -> Map.foldrWithKey f (sbConcreteLookup sym def mcidx idx) (Hash.hashedMap entry_map)
.

When the array has been initialized at many indexes, this creates a massive mux tree that is probably more harmful than helpful. If the Nothing case at the link above is removed, it just generates a SelectArray, which is compact and probably the right behavior.
@travitch travitch added the what4 label Dec 11, 2019
travitch added a commit that referenced this issue Dec 16, 2019
@travitch
Improve the SMT generated for array lookups with symbolic indices
6a5eae0 
What4 attempts to simplify array lookups of values with concrete indices.  In
cases where the index to look up in symbolic, that fails and it instead
generates a huge mux over all possible indexes, which is very expensive and
counterproductive.

This commit removes the special handling of symbolic indices, allowing the
generated SMT to fall back on just issuing an SMT array lookup.

Fixes #371
@travitch travitch mentioned this issue Dec 16, 2019
Merged
robdockins pushed a commit that referenced this issue Dec 30, 2019
@travitch @robdockins
Improve the SMT generated for array lookups with symbolic indices
ce240b9 
What4 attempts to simplify array lookups of values with concrete indices.  In
cases where the index to look up in symbolic, that fails and it instead
generates a huge mux over all possible indexes, which is very expensive and
counterproductive.

This commit removes the special handling of symbolic indices, allowing the
generated SMT to fall back on just issuing an SMT array lookup.

Fixes #371
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
what4
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Improve the SMT generated for array lookups with symbolic indices GaloisInc/crucible
1 participant
@travitch