Fix nightly jobs running CBMC latest on the perf suite

[adpaco-aws]

As explained in #2952 , the nightly perf runs started failing over the weekend with this error:

The input was compiled with an old version of goto-cc; please recompile
error: goto-cc exited with status exit status: 1

Changing the build process for CBMC to use make instead of cmake is enough for the error to go away. This action run shows how a successful perf job with the change in this PR.

Resolves #2952

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[jaisnan]

Tyvm!

[tautschnig]

I’m sorry, but we’ll need to dig deeper to see how the build system should relate to that error.

[adpaco-aws]

I’m sorry, but we’ll need to dig deeper to see how the build system should relate to that error.

Fair enough, I've started bisecting on the Dec 15 commits.

[adpaco-aws]

The problem comes from PR diffblue/cbmc#5815, where GOTO_BINARY_VERSION is redefined.

Now, I'm not sure where to go from here. The first question that comes to mind is: why is this error not reproducible with make?

[adpaco-aws]

When comparing the outputs of both build systems, I've realized that make doesn't actually produce a build folder with these commands.

To confirm this, I made this change to the workflow, and then triggered the CI run. Both the perf and regresssion (ubuntu-22.04) jobs print the same at the end of the Build CBMC step:

/usr/bin/cbmc
5.95.1 (cbmc-5.95.1)

Therefore, it's likely that these jobs aren't testing with the CBMC we're building, but the one that we install through the Setup Kani Dependencies step.

Still, this doesn't explain why the perf job is failing. If it was picking up version 5.91.1 as the output of the which cbmc and cbmc --version suggest, then it shouldn't be failing. But it's possible that building Kani with --release is helping it pick-up the newest version? That's what I'm testing in this other CI run.

[adpaco-aws]

Still, this doesn't explain why the perf job is failing. [...] But it's possible that building Kani with --release is helping it pick-up the newest version? That's what I'm testing in this other CI run.

The perf job is picking up the right version because the path to the CBMC binaries is being added to $GITHUB_PATH. The GA runners will use that variable instead of the usual $PATH, so which is not the most reliable way to determine the cbmc location.

Regardless, I've been able to determine that the CBMC being executed in the regression is not the one we're building, but the one we install with the "setup" action earlier. This becomes clear in this CI run, which is running these changes. In that run, the regression fails because it can't find cbmc, while perf also fails because of the version mismatch problem that we're aware of.

Unfortunately, I haven't been able to make the setup action work with two steps using an exclusive condition (i.e., based on inputs.install_cbmc) to determine if the install_deps.sh should be called with --no-cbmc. This would add some complexity here and there, but I don't think we should be installing cbmc in workflows where we want to test a version built from source. The next step is to get that working.

[tautschnig]

Apologies for having been very quiet on this. Failing with current CBMC HEAD should be expected at this time as the new major release being prepared for CBMC includes several breaking changes. We should either ignore the job’s failure, or disable it, or prepare a Kani branch and use that branch for our testing.

[adpaco-aws]

Failing with current CBMC HEAD should be expected at this time as the new major release being prepared for CBMC includes several breaking changes. We should either ignore the job’s failure, or disable it, or prepare a Kani branch and use that branch for our testing.

Agree, #2952 just seems to be the first breaking change to be noticed.

However, I think we need to at least change the regression jobs to use the CBMC built from source. Closing this PR in favor of #2965 which does exacty that.