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

Update Crux-llvm testing #618

Draft
wants to merge 17 commits into
base: master
Choose a base branch
from
Draft

Update Crux-llvm testing #618

wants to merge 17 commits into from

Conversation

kquick
Copy link
Member

@kquick kquick commented Jan 17, 2021

  • Switch to using tasty-sugar for better parameterizing tests.

  • Add yices tests.

  • Add timeouts to crucible invocations.

  • Verify stdout/stderr of each crucible invocation independently of the explicit output.

@kquick kquick marked this pull request as draft January 18, 2021 06:28
@kquick kquick marked this pull request as ready for review January 18, 2021 18:16
@robdockins
Copy link
Contributor

Overall, I like the idea here. However, the test suite just fails hard if any one of the solvers isn't installed, and doesn't run any of the other tests.

Test suite crux-llvm-test: RUNNING...
crux-llvm-test: stp: readCreateProcess: runInteractiveProcess: exec: does not exist (No such file or directory)
Test suite crux-llvm-test: FAIL

For local development purposes, it would be much nicer if we could just skip or at least gracefully fail tests for solvers that aren't installed.

@kquick
Copy link
Member Author

kquick commented Jan 19, 2021

Good catch! I was so focused on making it work with all the solvers I forgot about working without all the solvers.

I've updated it now so that a missing solver doesn't cause the testing to completely abort, however, individual tests for that solver will still fail. For development purposes one could bypass these with a cabal run crux-llvm-tests -- -p z3 would run only the z3 tests.

An alternative would be to simply not run tests for which a solver wasn't present. I'm a little undecided on this point, but my general thought is that by defaulting to run tests for all the solvers this will help ensure we don't forget about testing against some of them. As a developer, you can always just create a PR and let the CI system test the other solvers, but this defaults to being thorough unless you use a specific narrowing as described above.

Let me know what you think about this, @robdockins and @travitch .

@travitch
Copy link
Contributor

I'm also not sure what the best policy is. My first thought was that as a user I'd probably just want it to run the tests that I have solvers for, otherwise I'll be drowned in failures that I have to manually triage (and then CI will yell at me if I actually messed something up).

In that case, we'd want to be careful and maybe have a flag that really forces all solvers to be tested (and turn a failure to find a solver into an overall CI failure) that we could enable for CI. It would be unfortunate if a CI misconfiguration in the future accidentally got through just because no solvers ran.

@robdockins
Copy link
Contributor

I think the most convenient would be more or less what @travitch suggests: for local development run tests for all the solvers that are installed, but have some way to force all the solvers to be exercised for CI.

@kquick kquick marked this pull request as draft January 27, 2021 23:26
@@ -0,0 +1,36 @@
[Crux] Counter example for /home/kquick/work/crux-sugar/crux-llvm/test-data/golden/funptr-array.c:12:12: error: in mytestfunction
Copy link
Contributor

Choose a reason for hiding this comment

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

Is this supposed to be part of the file, given it has paths from your env in it?

Copy link
Member Author

Choose a reason for hiding this comment

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

Yup, I'm working on that right now. The input is a relative path, but somewhere it's getting the fully-rooted path, which isn't good for several reasons. Thanks for catching this!

@kquick
Copy link
Member Author

kquick commented Feb 1, 2021

With the merge of the loopmerge functionality and corresponding test changes, this PR has gotten too messy. I will create a sequence of PR's to make incremental steps towards the final goal, starting with #631

@robdockins robdockins removed their request for review April 19, 2021 21:53
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.

4 participants