Fix z3 installation on PR CI jobs #5983

thomasspriggs · 2021-03-29T18:06:38Z

Includes updating z3 to 4.8.10 for Windows CI jobs. So that the version, which is currently most recently released is available for use in Windows regression tests. Z3 installation was previously broken, due to the chocolatey package being out of date / broken and due to the installation being missing from various jobs.

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

I have a couple of remarks:

This PR claims to be upgrading z3 on windows, but it also makes a number of other changes, such as probing for z3 version on mac and ubuntu jobs? Is this on purpose? If that's the case, can the PR be renamed to accurately reflect scope of changes, or submit the changes as another PR?
One of the CI jobs is failing because it's probing for z3 when it's not installed.

NlightNFotis · 2021-03-29T18:55:17Z

.github/workflows/pull-request-checks.yaml

@@ -287,7 +287,7 @@ jobs:
          submodules: recursive
      - name: Fetch dependencies
        run: |
-          choco install winflexbison3 strawberryperl
+          choco install winflexbison3 strawberryperl z3


Should this commit be dropped?

This commit exists, so that I am not doing both adding and updating in subsequent commits.

codecov · 2021-03-29T19:24:16Z

Codecov Report

Merging #5983 (037ec0b) into develop (a387193) will increase coverage by 0.07%.
The diff coverage is 94.79%.

@@             Coverage Diff             @@
##           develop    #5983      +/-   ##
===========================================
+ Coverage    75.04%   75.12%   +0.07%     
===========================================
  Files         1433     1435       +2     
  Lines       155817   156301     +484     
===========================================
+ Hits        116932   117416     +484     
  Misses       38885    38885

Impacted Files	Coverage Δ
...nalyses/variable-sensitivity/abstract_object_set.h	`100.00% <ø> (ø)`
...lyses/variable-sensitivity/abstract_value_object.h	`87.71% <ø> (ø)`
...ses/variable-sensitivity/constant_abstract_value.h	`100.00% <ø> (ø)`
...s/variable-sensitivity/value_set_abstract_object.h	`100.00% <ø> (ø)`
src/ansi-c/c_typecheck_base.h	`100.00% <ø> (ø)`
src/ansi-c/expr2c_class.h	`100.00% <ø> (ø)`
src/goto-programs/goto_convert_class.h	`87.30% <ø> (ø)`
src/goto-symex/goto_state.h	`100.00% <ø> (ø)`
src/solvers/smt2/smt2_conv.h	`100.00% <ø> (ø)`
src/util/expr.h	`97.84% <ø> (ø)`
... and 49 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 44b5936...037ec0b. Read the comment docs.

TGWDB

A couple of bookkeeping changes:

The PR comment claims "latest version", which may be true today but will not be in future. Since the PR explicitly sets the version to 4.8.10 can we make that clear? (Specially since we could probably also use something like https://github.com/Z3Prover/z3/releases/latest for the true latest.)
Several places claim to "Check z3 version", but I think they only display the version, there does not appear to be a "check" that this is correct?

thomasspriggs · 2021-03-30T09:40:00Z

After discussion with Fotis, I am going to change this PR to fix Z3 installation across all jobs and add a test. Please wait for me to push the extra changes, before reviewing.

thomasspriggs · 2021-03-30T09:46:24Z

A couple of bookkeeping changes:

The PR comment claims "latest version", which may be true today but will not be in future. Since the PR explicitly sets the version to 4.8.10 can we make that clear? (Specially since we could probably also use something like https://github.com/Z3Prover/z3/releases/latest for the true latest.)

I think this should now be fixed.

Several places claim to "Check z3 version", but I think they only display the version, there does not appear to be a "check" that this is correct?

It is useful as is for confirming that Z3 is installed, in the path and logging the version. We could in theory check that the information printed is what we expect. But I think the changes are useful as is, without adding more functionality. I'll re-word the message a little, in order to try and make this clear.

This was previously missing, which would cause any tests which needed Z3 to fail this job.

Because the `choco` installation of `z3` seems to be broken/outdated. Using `Invoke-WebRequest` instead of `choco` allows us to pin the version installed and to get a version which includes the `z3.exe`, not just `z3.dll`. Using `nuget` was also considered, so that we were still using a package manager. But the up to date `nuget` package was missing the `.exe` file. `wget` is supposed to be aliased to `Invoke-WebRequest` in powershell. However `Invoke-WebRequest` is used rather than `wget` as `wget` does not seem to work for windows github actions jobs.

This was previously missing, which would cause any tests which needed Z3 to fail this job.

For confirmation of version and that installation is successfull. This supports easier debugging for both the github actions `.yaml` and for future test failures. As a bonus we get fast failing CI jobs if the dependency isn't installed properly, because it fails at this step rather than during testing. This z3 version check is done as a separate step because adding to `$env:GITHUB_PATH` doesn't take effect the path until the next step.

This confirms that Z3 is present and working in CI, as well as that cbmc's support for Z3 is not entirely broken.

thomasspriggs · 2021-03-30T17:08:02Z

@TGWDB Your comments should now be addressed. Please re-review when you have a minute.

SaswatPadhi · 2021-03-30T19:11:52Z

Not a blocker if we don't have broken tests right now, but we might soon run into cases where a regression test might pass on Windows & Mac but failing on Ubuntu 18.04 or 20.04 because they're running older versions of Z3 (4.4.1 and 4.8.7 respectively).

Would it be possible to wget the https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip binary from https://github.com/Z3Prover/z3/releases/tag/z3-4.8.10 and just move it to /usr/local/bin or some directory in $PATH?

@tautschnig is listed as the maintainer of the z3 Ubuntu package (https://packages.ubuntu.com/bionic/z3), may be he could help too.

NlightNFotis

LGTM

thomasspriggs · 2021-03-31T09:27:26Z

@SaswatPadhi Now that this is merged, you should be able to re-base and merge #5904

thomasspriggs requested a review from a team as a code owner March 29, 2021 18:06

NlightNFotis reviewed Mar 29, 2021

View reviewed changes

TGWDB requested changes Mar 30, 2021

View reviewed changes

thomasspriggs added do not merge do not review labels Mar 30, 2021

thomasspriggs changed the title ~~Update z3 to 4.8.10 for Windows CI jobs~~ Fix z3 installation on PR CI jobs Mar 30, 2021

thomasspriggs added 3 commits March 30, 2021 11:00

Add z3 installation for windows + make job

400b490

This was previously missing, which would cause any tests which needed Z3 to fail this job.

Add z3 to Ubuntu 18 package pull request check job

13c5d50

This was previously missing, which would cause any tests which needed Z3 to fail this job.

thomasspriggs force-pushed the tas/update_windows_z3 branch from 5ea7a5a to 4c6f240 Compare March 30, 2021 10:01

thomasspriggs force-pushed the tas/update_windows_z3 branch from 4c6f240 to 7dc7632 Compare March 30, 2021 16:25

thomasspriggs removed do not merge do not review labels Mar 30, 2021

Add test that Z3 solver support is present and working

037ec0b

This confirms that Z3 is present and working in CI, as well as that cbmc's support for Z3 is not entirely broken.

thomasspriggs force-pushed the tas/update_windows_z3 branch from 7dc7632 to 037ec0b Compare March 30, 2021 16:53

TGWDB approved these changes Mar 31, 2021

View reviewed changes

NlightNFotis approved these changes Mar 31, 2021

View reviewed changes

NlightNFotis merged commit 9f0dcfd into diffblue:develop Mar 31, 2021

thomasspriggs deleted the tas/update_windows_z3 branch March 31, 2021 09:23

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix z3 installation on PR CI jobs #5983

Fix z3 installation on PR CI jobs #5983

thomasspriggs commented Mar 29, 2021 •

edited

Loading

NlightNFotis left a comment

NlightNFotis Mar 29, 2021

thomasspriggs Mar 30, 2021

codecov bot commented Mar 29, 2021 •

edited

Loading

TGWDB left a comment

thomasspriggs commented Mar 30, 2021

thomasspriggs commented Mar 30, 2021

thomasspriggs commented Mar 30, 2021

SaswatPadhi commented Mar 30, 2021

NlightNFotis left a comment

thomasspriggs commented Mar 31, 2021

Fix z3 installation on PR CI jobs #5983

Fix z3 installation on PR CI jobs #5983

Conversation

thomasspriggs commented Mar 29, 2021 • edited Loading

NlightNFotis left a comment

Choose a reason for hiding this comment

NlightNFotis Mar 29, 2021

Choose a reason for hiding this comment

thomasspriggs Mar 30, 2021

Choose a reason for hiding this comment

codecov bot commented Mar 29, 2021 • edited Loading

Codecov Report

TGWDB left a comment

Choose a reason for hiding this comment

thomasspriggs commented Mar 30, 2021

thomasspriggs commented Mar 30, 2021

thomasspriggs commented Mar 30, 2021

SaswatPadhi commented Mar 30, 2021

NlightNFotis left a comment

Choose a reason for hiding this comment

thomasspriggs commented Mar 31, 2021

thomasspriggs commented Mar 29, 2021 •

edited

Loading

codecov bot commented Mar 29, 2021 •

edited

Loading