Skip to content

Add z3 package installation to CI pull request checks #5944

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
Merged
merged 2 commits into from
Mar 17, 2021
Merged

Add z3 package installation to CI pull request checks #5944

merged 2 commits into from
Mar 17, 2021

Conversation

thomasspriggs
Copy link
Contributor

@thomasspriggs thomasspriggs commented Mar 16, 2021 •
edited
Loading

Add z3 package installation to CI pull request checks. This will enable subsequent PRs to add tests which require the z3 solver.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

NlightNFotis
NlightNFotis reviewed Mar 16, 2021
View reviewed changes
Copy link
Contributor

@NlightNFotis NlightNFotis left a comment

Choose a reason for hiding this comment

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

We probably also need z3 for the coverage job as well.

@SaswatPadhi
Copy link
Contributor

SaswatPadhi commented Mar 16, 2021 •
edited
Loading

The test case that I had added in #5904 seems to succeed now -- see: https://github.com/diffblue/cbmc/pull/5944/checks?check_run_id=2124973614#step:11:2064.

But the loop acceleration tests seem to be failing now. Checking if my PR caused this ...

@SaswatPadhi
Copy link
Contributor

SaswatPadhi commented Mar 16, 2021 •
edited
Loading

Okay I just tried this on the develop branch -- ignoring the changes here (and in #5904). This is what I see:

  • If z3 is installed on the system, these tests fail.
  • If z3 is not installed, they pass -- they're not skipped.

This makes me think there's some code in the acceleration regression tests that "prefers" z3 and uses it when available (and fails because of some bug), but doesn't really "need" it because it runs fine without z3?

This was referenced Mar 17, 2021
Closed
Merged
@thomasspriggs
Fix check on value emptiness in polynomial acceleration
fa657ac 
Without z3 installed the regession tests for this don't correctly
exercise this part of the code. This fix addresses a bug which appears
to have been introduced in a previous refactor to replace `nil_typet`
with `optionalt<typet>`.
@thomasspriggs
Add z3 package installation to PR check jobs
0b7431f 
So that tests which require z3 can be run in CI.
@thomasspriggs thomasspriggs force-pushed the tas/smt_struct_fix_ci branch from 04c0aed to 0b7431f Compare March 17, 2021 16:35
@thomasspriggs
Copy link
Contributor Author

Okay I just tried this on the develop branch -- ignoring the changes here (and in #5904). This is what I see:

  • If z3 is installed on the system, these tests fail.
  • If z3 is not installed, they pass -- they're not skipped.

This makes me think there's some code in the acceleration regression tests that "prefers" z3 and uses it when available (and fails because of some bug), but doesn't really "need" it because it runs fine without z3?

There is at least one bug in the implementation of acceleration which was causing failures when z3 is available. I have pushed an additional commit to this branch to fix that issue.

@thomasspriggs thomasspriggs changed the title Add z3 package installation to CI pull request check [DO NOT REVIEW] Add z3 package installation to CI pull request check Mar 17, 2021
@thomasspriggs thomasspriggs marked this pull request as ready for review March 17, 2021 17:20
@thomasspriggs
Copy link
Contributor Author

We probably also need z3 for the coverage job as well.

Added.

@thomasspriggs
Copy link
Contributor Author

I have raised a separate draft PR to run CI with the combination of installing z3 in CI + the fix from #5904. This CI running PR is here - #5949

@thomasspriggs thomasspriggs changed the title Add z3 package installation to CI pull request check Add z3 package installation to CI pull request checks Mar 17, 2021
@codecov
Copy link

codecov bot commented Mar 17, 2021

Codecov Report

Merging #5944 (0b7431f) into develop (316ae8b) will increase coverage by 0.38%.
The diff coverage is 100.00%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5944      +/-   ##
===========================================
+ Coverage    73.56%   73.95%   +0.38%     
===========================================
  Files         1431     1431              
  Lines       155291   155291              
===========================================
+ Hits        114243   114842     +599     
+ Misses       41048    40449     -599
Impacted Files Coverage Δ
src/goto-instrument/accelerate/polynomial.cpp 21.00% <100.00%> (+21.00%) ⬆️
src/goto-checker/report_util.cpp 48.11% <0.00%> (-3.48%) ⬇️
src/goto-checker/properties.cpp 67.24% <0.00%> (-1.73%) ⬇️
src/solvers/smt2/smt2_conv.cpp 59.22% <0.00%> (+0.19%) ⬆️
.../goto-instrument/goto_instrument_parse_options.cpp 62.27% <0.00%> (+1.07%) ⬆️
src/goto-instrument/accelerate/accelerate.cpp 34.89% <0.00%> (+2.51%) ⬆️
src/goto-instrument/accelerate/scratch_program.cpp 67.41% <0.00%> (+11.23%) ⬆️
...to-instrument/accelerate/overflow_instrumenter.cpp 75.23% <0.00%> (+14.28%) ⬆️
src/goto-instrument/accelerate/util.cpp 25.64% <0.00%> (+17.94%) ⬆️
... and 10 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update cce4503...0b7431f. Read the comment docs.

NlightNFotis
NlightNFotis approved these changes Mar 17, 2021
View reviewed changes
Copy link
Contributor

@NlightNFotis NlightNFotis left a comment

Choose a reason for hiding this comment

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

LGTM

@NlightNFotis NlightNFotis merged commit ac11ec8 into diffblue:develop Mar 17, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@NlightNFotis NlightNFotis NlightNFotis approved these changes

@chrisr-diffblue chrisr-diffblue chrisr-diffblue approved these changes

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Awaiting requested review from hannes-steffenhagen-diffblue

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@smowton smowton Awaiting requested review from smowton

Assignees
No one assigned
Labels
CI
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@thomasspriggs @SaswatPadhi @NlightNFotis @chrisr-diffblue