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.

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

Add arrayCopy, arraySet, and arrayRangeEqual primitives. #152

Merged
merged 6 commits into from
Aug 25, 2021

Conversation

andreistefanescu
Copy link
Contributor

The implementation supports single-dimensional arrays with bitvector indices. The encoding in SMTLib uses universal quantification, with Z3 the recommended solver. The operations are undefined if any of the index ranges wraps around.

Copy link
Contributor

@robdockins robdockins left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm still working on understanding some of the tricker aspects of this, but I'd like to see a bit more documentation in a few places, and I wonder if there is anything preventing us from implementing ground evaluation on these new array constructs.

what4/src/What4/Expr/App.hs Show resolved Hide resolved
what4/src/What4/Expr/Builder.hs Show resolved Hide resolved
what4/src/What4/Expr/GroundEval.hs Outdated Show resolved Hide resolved
what4/src/What4/Interface.hs Show resolved Hide resolved
what4/src/What4/Interface.hs Outdated Show resolved Hide resolved
what4/src/What4/Expr/Builder.hs Show resolved Hide resolved
what4/src/What4/Expr/Builder.hs Show resolved Hide resolved
what4/src/What4/Protocol/SMTWriter.hs Show resolved Hide resolved
| Just (CopyArray w _a_repr _dest_arr dest_begin_idx src_arr src_begin_idx _len dest_end_idx _src_end_idx) <- asApp arr0
, Just (Empty :> (BVIndexLit _ lookup_idx_bv)) <- mcidx
, lookup_idx_unsigned <- BV.asUnsigned lookup_idx_bv
, Just dest_begin_idx_unsigned <- BV.asUnsigned <$> asBV dest_begin_idx
Copy link
Contributor

@robdockins robdockins Aug 25, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know if it is worth trying to do this, but you can sometimes get useful answers to range questions using the abstract domain computations even when the inputs you start with aren't fully concrete.

EDIT: the technique you use below where you construct, e.g., a Ule term and test if it is concrete will do basically the same thing.

@robdockins
Copy link
Contributor

I'm now relatively convinced about the correctness of these new operations. The remaining issues I have are:

  1. I'd like to see some evidence that the array slicing code is really necessary. That kind of deep rewriting has caused more problems than it solves, in my past experience.
  2. The build failures need addressing. I think they might actually be related to the haddock comments and not the strictness annotation as the error message suggests. I don't think haddock for GHC 8.6 and 8.8 can handle comments attached to GADT arguments :-( so I think you should just remove the ^ character and make them non-haddock comments.

Otherwise, I feel pretty good about this.

@andreistefanescu andreistefanescu merged commit 95fd577 into master Aug 25, 2021
@andreistefanescu andreistefanescu deleted the array-copy-set branch August 25, 2021 21:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants