Corral

Corral is a solver for the reachability modulo theories problem. Learn more here: http://research.microsoft.com/en-us/projects/verifierq

Dependency on Boogie

Corral has a dependency on Boogie, which is provided as a git submodule. To download the specific revision of Boogie that Corral depends on:

cd ${CORRAL_DIR}
git submodule init
git submodule update

Building and running Corral on Windows

Here is how you set up Corral.

1. Build cba.sln. This solution includes the necessary Boogie projects; there is no longer a separate step to build Boogie.
2. Running Corral requires z3. We have tested Corral against z3 version 4.1; download and copy z3.exe in bin\debug folder, alongside the corral.exe executable.
3. Corral takes a Boogie program as input. There are regressions provided in test\regressions folder. Go to this folder and run perl check.pl to run all the regressions. You can run an individual test, for instance, as follows: go to test\regressions and do: ..\..\bin\debug\corral.exe 001\001.bpl /flags:001\config. The flag /flags:filename instructs corral to read its flags from the file filename.

Building and Running Corral on Linux using Mono

The following worked for Matt McCutchen on Fedora 23. You may need to change the TargetFrameworkVersion to match what your Mono version provides.

cd ${CORRAL_DIR}
xbuild /p:TargetFrameworkVersion=v4.5 /p:Configuration=Debug cba.sln
ln -s ${Z3_DIR}/install/bin/z3 ${CORRAL_DIR}/bin/Debug/z3.exe
mono bin/Debug/corral.exe ...

Building and Running Corral using .NET Core

Currently there are separate project and solution files (*-NetCore.*) to build Corral with .NET Core, which use GitVersion to attach version numbers to the assemblies and package(s) generated by builds.

# Attach HEADs in submodules to appease GitVersion
$ git submodule foreach 'git branch -D master && git checkout -b master'

# Build the solution
$ dotnet build cba-NetCore.sln

# Run the generated executable
$ bin/Debug/netcoreapp3.1/corral ...

⚠️ There is currently a know build problem with .NET Core and GitVersionTask. The workaround is to set the environment variable MSBUILDSINGLELOADCONTEXT=1 and run dotnet build-server shutdown.

Alternatively, Corral can be installed as a .NET Core Global Tool:

$ dotnet tool install --global Corral

Versioning and Release Automation

The main.yml workflow will create and push a new tag each time commits are pushed to the master branch (including PR merges). By default, the created tag increments the patch version number from the previous tag. For example, if the last tagged commit were v2.4.3, then pushing to master would tag the latest commit with v2.4.4. If incrementing minor or major number is desired instead of patch, simply add #minor or #major to the first line of the commit message. For instance:

Adding the next greatest feature. #minor

If the last tagged commit were v2.4.3, then pushing this commit would generate the tag v2.5.0.

For pull-request merges, if minor or major version increments are desired, the first line of the merge commit message can be changed to include #minor or #major.

Note that on each push to master, the following will happen:

• A travis build for master is triggered.
• The GitHub workflow is also triggered.
• Once the workflow pushes a new tag vX.Y.Z, another travis build for vX.Y.Z is triggered.
• The travis build for vX.Y.Z in Release configuration publishes releases to GitHub and NuGet.org.