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

implement comment injections #183

Open
wants to merge 12 commits into
base: master
Choose a base branch
from
Open

implement comment injections #183

wants to merge 12 commits into from

Conversation

Ferinko
Copy link
Contributor

@Ferinko Ferinko commented Mar 1, 2023

This PR implements:

  • machinery for adding comments into raw *.smt2 queries
  • usage of said machinery to annotate the most common things we encounter

@Ferinko Ferinko force-pushed the ferinko/annotate_smts branch 2 times, most recently from 4a1095e to c5f0571 Compare March 1, 2023 00:46
In this commit, we add a function `userAnnotatedSources` which replaces
`isStandardSource`. It generates a list of all the user annotated
ScopedFunctions. This list is used to filter modules for solving. This
requires a slight refactor within `FunctionAnalysis.hs`.

* Add `extern_remove_dirty` test.

The basic idea is this:
1. Find all wrapper functions.
2. Compute their respective set of reachable functions.
3. Mark them all as 'don't check' unless they are referenced from a
   different source as well.
@langfield langfield changed the base branch from ferinko/checkpoint_gone to master March 24, 2023 17:58
@Ferinko Ferinko force-pushed the ferinko/annotate_smts branch 2 times, most recently from 8e8119e to 76ac907 Compare March 27, 2023 18:52
Don't verify `@external`-generated wrapper functions
* Use `ssh-agent` to clone with specific private key
* Set `0o400` permissions on private key file
* Add `mathsat` to list of solvers used in tests
Add mathsat installation to Github actions workflow
…ted-specs

Add FAQ about commenting-out annotations
…eadme-additions

Add `README.md` section on details of `CairoSemanticsL`
Copy link
Contributor

@langfield langfield 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 in the process of reviewing this. It adds a lot of code.

Comment on lines +85 to +87
isOptimising :: Vertex -> Bool
isOptimising = isJust . v_preCheckedF

Copy link
Contributor

Choose a reason for hiding this comment

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

Duplicates isPreCheckingVertex (sorry about the name churn).

@langfield langfield force-pushed the master branch 2 times, most recently from 9f9928b to 3397b7c Compare March 31, 2023 15:01
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