z3Exe flag seems to have stopped working

[bobismijnnaam]

In VerCors we call carbon by supplying an explicit path to z3:

class CarbonVerifier[O](o:OriginFactory[O]) extends SilverImplementation[O](o) {
  override def createVerifier(tool_home:Path,settings:Properties):viper.silver.verifier.Verifier = {
    val carbon = viper.carbon.CarbonVerifier(Seq("startedBy" -> "example", "fullCmd" -> "dummy"))
    carbon.parseCommandLine(Seq(
        "--z3Exe", Configuration.getZ3Path.getAbsolutePath,
        "--boogieExe",Configuration.getBoogiePath.getAbsolutePath,
        "-"))
    carbon.start()
    carbon
  }

}

This seems effective enough: in the screenshot below this path appears in the call to boogie.

However, upon termination, Boogie reports it cannot find "z3" in the same folder Boogie is located in:

So it seems to have swapped out the path I passed for some reason. The issue is resolved when I copy the executable at the z3 path to the Boogie folder and name it "z3.exe", but we'd like to avoid that and keep the tools separate.

For what it's worth, I've looked a bit through carbon's code, and it seems to handle the presence of the flag just fine. But when I pull the carbon repository and run carbon from the command line, the same problem happens: besides adding the --z3Exe flag, z3.exe needs to be present in the boogie folder, to make verification work.

This used to work on 20.07, but after upgrading to 21.01 this broke. The boogie version we use is: "2.4.1.10503", which is the one available from the viper/ETH Zurich site. Did I miss an interface change, is this a bug, or is the boogie version we use no longer supported?

[gauravpartha]

Thanks for the detailed report.

I think you are using the Boogie version that we used for the 20.07 release. In the 21.01 Carbon release, we use a new Boogie version (which is distributed with the 21.01 release zip, boogie/Binaries/Boogie in http://viper.ethz.ch/downloads/ViperToolsLastReleaseLinux.zip, if you are on Linux). I get the same error as you report, if I use the old Boogie version, but with the new Boogie version there are no issues. The Boogie command line options changed since the old version (in particular, the Z3 executable option).

Does it fix your issue if you use the Boogie version distributed via the 21.01 release?

Further information

The commit for the Boogie version that we use in 21.01 is given by boogie-org/boogie@bae82d3. We compile it using .NET Core 3.1, so Mono is not required anymore on Linux. In the zip referenced above, we include all .NET Core dependencies, so you do not need to download anything externally.

[bobismijnnaam]

Thanks for the quick response! I'll look at it first thing tomorrow!

[bobismijnnaam]

It seems to work perfectly, only need to test windows and mac but those weren't a problem last time so I suspect it will be fine. One (very, very) minor comment, though: when I run the linux version of the boogie supplied with carbon the version it prints is 1.0.0.0. Maybe in the next major version that can be fixed, but might be more trouble than it's worth. (Or is it really version 1.0.0.0? I thought Boogie was beyond 2 already)

[gauravpartha]

One (very, very) minor comment, though: when I run the linux version of the boogie supplied with carbon the version it prints is 1.0.0.0. Maybe in the next major version that can be fixed, but might be more trouble than it's worth. (Or is it really version 1.0.0.0? I thought Boogie was beyond 2 already)

We had issues compiling Boogie with "GitVersionTask" (which gives a version number to Boogie) and had to disable it, which leads to the number 1.0.0.0 (the actual version is definitely above 2). For the next release, we plan to update Boogie again. I hope the GitVersionTask problem is resolved by then such that the version number for Boogie is visible.

[gauravpartha]

We have upgraded Carbon to use Boogie 2.15.9 in the merged PR #441. We were able to enable GitVersionTask, and thus the corresponding binary (that we will distribute with the next release) should display the correct version (instead of 1.0.0.0).