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

Merge saw-core repo #1213

Merged
merged 2,231 commits into from
Apr 26, 2021
Merged

Merge saw-core repo #1213

merged 2,231 commits into from
Apr 26, 2021

Conversation

brianhuffman
Copy link
Contributor

This merge pulls the previously-separate saw-core repository into the the saw-script repository, in its entirety and with all history intact.

m-yac and others added 30 commits October 19, 2020 14:46
Refactor saw-core `Value` type to make a separate datatype for type values
This works by declaring monomorphic uninterpreted functions at
each type instance, using a name suffix based on the type value.

Fixes #320.
Support uninterpreted polymorphic functions in sbv/what4 backends.
The new parser also uses `fail` in the `IO` monad to signal a parse
error, and avoids partial functions like `read` and `error`.
Modify saw-core external-format parser to use fresh `ExtCns` indices.
the `pdiv`, `pmod` and `pmult` primitives using
essentially the same trick we use in the Cryptol
symbolic backends.
Also reimplement `IntMod` type in simulator backends
to use it.
Also convert primitive implementations to use it.
Quantified variables of type `IntMod n` should work again in
the what4/sbv backends.
…nds.

When we generate an uninterpreted function in a symbolic backend that
takes an argument of type `IntMod n`, we normalize the symbolic integer
argument by reducing mod n. This ensures that the resulting expression
will respect the underlying equivalence relation for the `IntMod n` type.
Also add `getLabelValues` function from saw-script to saw-core-what4.
Improved support for IntMod type in symbolic backends
Reimplement `getAllExtSet` and `getConstantSet` using `Data.IntSet`.
robdockins and others added 5 commits April 19, 2021 09:56
Do the right thing when encountering 0-width bitvectors in the What4 backend
The _CoqProject file used to contain a lot of extraneous files related to my
work on S2N, my work with Talia Ringer, and an attempt at work on BESSPIN.
These are obsolete and irrelevant to saw-core-coq and should be located
elsewhere.

This commit also re-enables the compilation of some saw-core-coq files, notably
CryptolPrimitivesForSAWCore which is necessary for extraction from SAW, and
CoqVectorsExtra which may not be very useful yet.

This also remove all unnecessary Coq and Cryptol files.
Expose Simulator.What4 helper functions for use in compositional crux-mir
@brianhuffman brianhuffman requested a review from atomb April 26, 2021 14:13
@brianhuffman
Copy link
Contributor Author

brianhuffman commented Apr 26, 2021

To facilitate reviewing, here are the commits made after the huge merge commit:

@brianhuffman
Copy link
Contributor Author

brianhuffman commented Apr 26, 2021

Note: This PR includes the saw-core repo up to the commit that the saw-core submodule reference previously pointed to (12a8f95, the merge commit for GaloisInc/saw-core#203). It does not include the most-recently-merged PR GaloisInc/saw-core#197, which saw-script is not yet compatible with. The commit from this saw-core PR should be made into part of a new saw-script PR to adapt to the persistent solver features of cryptol.

@RyanGlScott
Copy link
Contributor

Awesome! I think the only remaining hurdle is to make the saw-core-coq–related CI actions work properly, as they currently appear to error out.

@brianhuffman
Copy link
Contributor Author

It looks like @Ptival got the saw-core-coq CI tests working in GaloisInc/saw-core#195, and they were working for a while, but by GaloisInc/saw-core#203 they were failing again.

@brianhuffman
Copy link
Contributor Author

By including the commits from GaloisInc/saw-core#201 and GaloisInc/saw-core#202, the saw-core-coq CI tests are now passing.

Brian Huffman and others added 8 commits April 26, 2021 15:02
… the saw-script repository,

in its entirety and with all history intact.

Merge remote-tracking branch 'saw-core/prep-merge' into merge-saw-core-repo
After merging repositories, the saw-core and cryptol-saw-core packages
should no longer direct users to create issues on the old saw-core repo.
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.

Glad to see this going through. I think it will save us a lot of effort in the end.

Copy link
Contributor

@atomb atomb left a comment

Choose a reason for hiding this comment

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

This looks good. I'm assuming all the added files are the same as the ones that were in the previous submodule and not reviewing them. :)

Copy link
Contributor

@lisanna-dettwyler lisanna-dettwyler left a comment

Choose a reason for hiding this comment

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

I can take the AR to converge this workflow with .github/workflows/ci.yml at some point.

@Ptival
Copy link
Contributor

Ptival commented Apr 26, 2021

@ldettwy neat, feel free to reach out to me if something in the workflow is confusing or breaks!

@brianhuffman brianhuffman merged commit fdb8987 into master Apr 26, 2021
@mergify mergify bot deleted the merge-saw-core-repo branch April 26, 2021 23:44
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.