From 59943769825b780dcb495826dc57fe67da2cd4c2 Mon Sep 17 00:00:00 2001 From: Bernhard Kragl Date: Thu, 19 Dec 2019 16:24:33 +0100 Subject: [PATCH 1/8] Port lit test and Travis CI configurations to .NET Core --- .gitignore | 31 +++---- .travis.yml | 36 +++++--- README.md | 86 +++++++++---------- .../BoogieDriver/BoogieDriver-NetCore.csproj | 1 - Test/lit.site.cfg | 60 ++++++------- 5 files changed, 100 insertions(+), 114 deletions(-) diff --git a/.gitignore b/.gitignore index 9bb613df2..d5dcf40bf 100644 --- a/.gitignore +++ b/.gitignore @@ -1,26 +1,21 @@ # Nuget -Source/packages/* -Source/**/nupkg +Source/packages/ + +# Binaries +bin/ +obj/ +Binaries/**/*.dll +Binaries/**/*.mdb +Binaries/**/*.exe +Binaries/**/*.pdb +Binaries/**/*.config +Binaries/**/*.vshost.exe.manifest # Tests Source/UnitTests/TestResult.xml -Source/UnitTests/*/bin -Source/UnitTests/*/obj Test/**/Output TestResult.xml -# Binaries -Source/*/bin -Source/*/obj -Source/Provers/*/bin -Source/Provers/*/obj -Binaries/*.dll -Binaries/*.mdb -Binaries/*.exe -Binaries/*.pdb -Binaries/*.config -Binaries/*.vshost.exe.manifest - # Coco/R Scanner.cs.old Parser.cs.old @@ -30,9 +25,7 @@ Parser.cs.old # Visual Studio files Source/_ReSharper.Boogie -Source/Provers/*/*.user -Source/*/*.user -Source/*.user +Source/**/*.user Source/*.suo Source/*.cache Source/.vs/ diff --git a/.travis.yml b/.travis.yml index 2c2551faf..a0ad09f7e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,27 +1,37 @@ # vim: set sw=2 ts=2 softtabstop=2 expandtab: language: csharp -dist: trusty +dist: bionic sudo: true -solution: "Source/Boogie.sln" +dotnet: 3.1 +mono: none env: global: + - SOLUTION=Source/Boogie-NetCore.sln - Z3URL=https://github.com/Z3Prover/z3/releases/download/z3-4.8.4/z3-4.8.4.d6df51951f4c-x64-ubuntu-14.04.zip matrix: - - BOOGIE_CONFIG=Debug - - BOOGIE_CONFIG=Release + - CONFIGURATION=Debug + - CONFIGURATION=Release install: # Download a Z3 release - wget ${Z3URL} - unzip z3*.zip - # NuGet is a little flakey in legacy TravisCI, use travis_retry command to retry the command if it fails - - travis_retry nuget restore ${TRAVIS_SOLUTION} - - travis_retry nuget install -Version 3.10.0 NUnit.Console -OutputDirectory Source/packages/ + - export PATH="$(find $PWD/z3* -name bin -type d):$PATH" # Install needed python tools - sudo pip install lit OutputCheck pyyaml script: - - msbuild /p:Configuration=${BOOGIE_CONFIG} ${TRAVIS_SOLUTION} - # Run unit tests - - python Source/UnitTests/run-unittests.py ${BOOGIE_CONFIG} - # Run driver tests - - ln -s $(find $PWD/z3* -name z3 -type f) Binaries/z3.exe - - lit -v Test/ + - dotnet build -c ${CONFIGURATION} ${SOLUTION} + - dotnet test --no-build -c ${CONFIGURATION} ${SOLUTION} + - lit -v -D dotnet -D configuration=${CONFIGURATION} Test +deploy: + skip_cleanup: true + on: + branch: master + tags: true + condition: ${CONFIGURATION}=Release + - provider: script + script : + - dotnet nuget push Source/BoogieDriver/bin/${CONFIGURATION}/Boogie*.nupkg -k ${NUGET_API_KEY} -s https://api.nuget.org/v3/index.json + - provider: releases + api_key: TODO + file_glob: true + file: Source/BoogieDriver/bin/${CONFIGURATION}/Boogie*.nupkg diff --git a/README.md b/README.md index 8833ec2f1..df7453454 100644 --- a/README.md +++ b/README.md @@ -55,78 +55,74 @@ You can also report issues on our [issue tracker](https://github.com/boogie-org/ ## Building -### Requirements +The preferred way to build (and run) Boogie today is using .NET Core. +Historically, Boogie can also be built using the classic .NET Framework (on +Windows) and Mono (on Linux/OSX), but this might not be supported in the future. -- [NuGet](https://www.nuget.org/) -- [Z3](https://github.com/Z3Prover/z3) 4.8.4 (earlier versions may also work, but the test suite assumes 4.8.4 to produce the expected output) or [CVC4](http://cvc4.cs.nyu.edu/web/) **FIXME_VERSION** (note - CVC4 support is experimental) +To run Boogie, a supported SMT solver has to be available (see below). -#### Windows specific +### .NET Core -- Visual Studio >= 2012 +``` +$ dotnet build Source/Boogie-NetCore.sln +``` + +**TODO**: Describe how to install and run. -#### Linux/OSX specific +### Windows (requires Visual Studio) -- Mono +1. Open ``Source\Boogie.sln`` in Visual Studio. +2. Right click the ``Boogie`` solution in the Solution Explorer and click ``Restore NuGet Packages``. +3. Click ``Build > Build Solution``. -### Windows +The compiled Boogie binary is `Binaries\Boogie.exe`. -1. Open ``Source\Boogie.sln`` in Visual Studio -2. Right click the ``Boogie`` solution in the Solution Explorer and click ``Enable NuGet Package Restore``. - You will probably get a prompt asking to confirm this. Choose ``Yes``. -3. Click ``BUILD > Build Solution``. +### Linux/OSX (requires Mono) -### Linux/OSX +Either open ``Source\Boogie.sln`` in MonoDevelop and perform the same steps as +described for Visual Studio above, of compile on the command line as follows. -You first need to fetch the NuGet packages that Boogie depends on. If you're doing this on the command line run +Fetch the NuGet packages that Boogie depends on: ``` -$ cd /path/to/repository -$ wget https://nuget.org/nuget.exe -$ mono ./nuget.exe restore Source/Boogie.sln +$ nuget restore Source/Boogie.sln ``` -Note if you're using MonoDevelop it has a NuGet plug-in which you can use to "restore" the packages needed by Boogie. - -Note if you see an error message like the following +Build Boogie: ``` -WARNING: Error: SendFailure (Error writing headers) -Unable to find version '2.6.3' of package 'NUnit.Runners'. +$ msbuild Source/Boogie.sln ``` -then you need to initialise Mono's certificate store by running +The compiled Boogie binary is `Binaries/Boogie.exe`, which can be executed with +`mono` or using the wrapper script `Binaries/boogie`. -``` -$ mozroots --import --sync -``` +## Backend SMT Solver -then you can build by running +The default SMT solver for Boogie is [Z3](https://github.com/Z3Prover/z3). +Support for [CVC4](https://cvc4.github.io/) and +[Yices2](https://yices.csl.sri.com/) is experimental. -``` -$ msbuild Source/Boogie.sln -``` +### Z3 -Finally make sure there is a symlink to Z3 in the Binaries directory -(replace with ``cvc4`` if using CVC4 instead). +The current test suite assumes version 4.8.4, but earlier and never versions may +also work. -``` -$ ln -s /usr/bin/z3 Binaries/z3.exe -``` +Option 1: Make sure a Z3 executable called `z3` or `z3.exe` is in your `PATH` +environment variable. -## Running +Option 2: Call Boogie with `/z3exe:`. -On a Windows system call the Boogie binary: +### CVC4 (experimental) -``` -$ Binaries\Boogie.exe -``` +Call Boogie with `/proverOpt:SOLVER=CVC4 /cvc4exe:`. -On a non-Windows system use the wrapper script: +### Yices2 (experimental) -``` -$ Binaries/boogie -``` +Call Boogie with `/proverOpt:SOLVER=Yices2 /yices2exe: /useArrayTheory`. + +Works for unquantified fragments, e.g. arrays + arithmetic + bitvectors. Does +not work for quantifiers, generalized arrays, datatypes. ## Testing diff --git a/Source/BoogieDriver/BoogieDriver-NetCore.csproj b/Source/BoogieDriver/BoogieDriver-NetCore.csproj index cd51e973b..9414572dd 100644 --- a/Source/BoogieDriver/BoogieDriver-NetCore.csproj +++ b/Source/BoogieDriver/BoogieDriver-NetCore.csproj @@ -13,7 +13,6 @@ BoogieDriver netcoreapp3.1 true - nupkg true boogie diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg index 551fea7be..3fa6a27ff 100644 --- a/Test/lit.site.cfg +++ b/Test/lit.site.cfg @@ -72,25 +72,31 @@ def quotePath(path): ### Add Boogie specific substitutions -# Find Boogie.exe +# Find Boogie executable and runtime up = os.path.dirname -repositoryRoot = up( - up( os.path.abspath(__file__) ) - ) +repositoryRoot = up(up(os.path.abspath(__file__))) lit_config.note('Repository root is {}'.format(repositoryRoot)) -binaryDir = os.path.join( repositoryRoot, 'Binaries') -boogieExecutable = os.path.join( binaryDir, 'Boogie.exe') +configuration = lit_config.params.get('configuration', 'Debug') +framework = lit_config.params.get('framework', 'netcoreapp3.1') -if not os.path.exists(boogieExecutable): - lit_config.fatal('Could not find Boogie.exe at {}'.format(boogieExecutable)) +runtime = '' -boogieExecutable = quotePath(boogieExecutable) +if 'dotnet' in lit_config.params: + boogieBinary = 'Source/BoogieDriver/bin/{}/{}/BoogieDriver'.format(configuration, framework) +else: + boogieBinary = 'Binaries/Boogie.exe' + if os.name == 'posix': + runtime = 'mono' -if os.name == 'posix': - boogieExecutable = 'mono ' + boogieExecutable - if lit.util.which('mono') == None: - lit_config.fatal('Cannot find mono. Make sure it is your PATH') +boogieExecutable = quotePath(os.path.join(repositoryRoot, boogieBinary)) + +if not os.path.exists(boogieExecutable): + lit_config.fatal('Could not find Boogie executable at {}'.format(boogieExecutable)) +if runtime and lit.util.which(runtime) == None: + lit_config.fatal('Cannot find {}. Make sure it is in your PATH'.format(runtime)) + +boogieExecutable = runtime + ' ' + boogieExecutable # Expected output does not contain logo boogieExecutable += ' -nologo' @@ -99,32 +105,14 @@ boogieExecutable += ' -nologo' boogieExecutable += ' -useBaseNameForFileName' # Allow user to provide extra arguments to Boogie -boogieParams = lit_config.params.get('boogie_params','') +boogieParams = lit_config.params.get('boogie_params', '') if len(boogieParams) > 0: boogieExecutable = boogieExecutable + ' ' + boogieParams # Inform user what executable is being used lit_config.note('Using Boogie: {}'.format(boogieExecutable)) -config.substitutions.append( ('%boogie', boogieExecutable) ) - -# Sanity check: Check solver executable is available -# FIXME: Should this check be removed entirely? -if os.name != 'nt': - solvers = ['z3.exe','cvc4.exe'] - solverFound = False - for solver in solvers: - if os.path.exists( os.path.join(binaryDir, solver)): - solverFound = True - - if not solverFound: - lit_config.fatal('Could not find solver in "{binaryDir}". Tried looking for {solvers}'.format( - binaryDir=binaryDir, - solvers=solvers - ) - ) -else: - lit_config.warning('Skipping solver sanity check on Windows') +config.substitutions.append(('%boogie', boogieExecutable)) # Add diff tool substitution if os.name == 'posix': @@ -134,17 +122,17 @@ if os.name == 'posix': diffExecutable = lit.util.which('diff') else: # use driver around Python's difflib - pydiff = quotePath( os.path.join(config.test_source_root, 'pydiff.py') ) + pydiff = quotePath(os.path.join(config.test_source_root, 'pydiff.py')) diffExecutable = sys.executable + ' ' + pydiff diffExecutable += ' --unified=3 --strip-trailing-cr --ignore-all-space' lit_config.note("Using diff tool: {}".format(diffExecutable)) -config.substitutions.append( ('%diff', diffExecutable )) +config.substitutions.append(('%diff', diffExecutable)) # Detect the OutputCheck tool outputCheckPath = lit.util.which('OutputCheck') if outputCheckPath == None: lit_config.fatal('The OutputCheck tool is not in your PATH. Please install it.') -config.substitutions.append( ('%OutputCheck', outputCheckPath + ' --dump-file-to-check') ) +config.substitutions.append(('%OutputCheck', outputCheckPath + ' --dump-file-to-check')) From fcb321dfa956e6ef870d15ea0d5e3739ad6f5131 Mon Sep 17 00:00:00 2001 From: Bernhard Kragl Date: Thu, 19 Dec 2019 16:38:43 +0100 Subject: [PATCH 2/8] Update expected test output (same model is printed differently) --- Test/test15/CaptureState.bpl.expect | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/test15/CaptureState.bpl.expect b/Test/test15/CaptureState.bpl.expect index db109e969..6a52f7705 100644 --- a/Test/test15/CaptureState.bpl.expect +++ b/Test/test15/CaptureState.bpl.expect @@ -5,12 +5,12 @@ Execution trace: CaptureState.bpl(19,5): anon4_Then CaptureState.bpl(27,5): anon3 *** MODEL -$mv_state_const -> 4 %lbl%@1 -> false %lbl%+0 -> true %lbl%+3 -> true %lbl%+4 -> true %lbl%+5 -> true +$mv_state_const -> 4 F -> T@FieldName!val!0 Heap -> |T@[Ref,FieldName]Int!val!0| m -> **m From 714d5a0ad9ca0178a09861be6ead3d21550e56c8 Mon Sep 17 00:00:00 2001 From: Bernhard Kragl Date: Thu, 19 Dec 2019 16:41:02 +0100 Subject: [PATCH 3/8] Remove unused field that caused a crash Under .NET Core, the access of UserProcessorTime to update TotalUserTime caused Boogie to crash with an InvalidOperationException on Test/snapshots/runtest.snapshot. Unhandled exception. System.InvalidOperationException: Cannot process request because the process (26852) has exited. at System.Diagnostics.Process.ThrowIfExited(Boolean refresh) at System.Diagnostics.Process.EnsureState(State state) at System.Diagnostics.Process.GetStat() at System.Diagnostics.Process.get_UserProcessorTime() at Microsoft.Boogie.SMTLib.SMTLibProcess.Close() at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Close() The field TotalUserTime is never accessed, so it seems fine to remove it. --- Source/Provers/SMTLib/SMTLibProcess.cs | 3 --- 1 file changed, 3 deletions(-) diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 9b1a6a49a..36f568e23 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -190,11 +190,8 @@ public SExpr GetProverResponse() } } - public static System.TimeSpan TotalUserTime = System.TimeSpan.Zero; - public void Close() { - TotalUserTime += prover.UserProcessorTime; TerminateProver(); DisposeProver(); } From 567f46bac2630933a522b9afff94815c22c039d6 Mon Sep 17 00:00:00 2001 From: Bernhard Kragl Date: Thu, 19 Dec 2019 19:09:35 +0100 Subject: [PATCH 4/8] Travis: common configuration has to be repeated for every provider --- .travis.yml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/.travis.yml b/.travis.yml index a0ad09f7e..30dc671e9 100644 --- a/.travis.yml +++ b/.travis.yml @@ -23,15 +23,20 @@ script: - dotnet test --no-build -c ${CONFIGURATION} ${SOLUTION} - lit -v -D dotnet -D configuration=${CONFIGURATION} Test deploy: - skip_cleanup: true - on: - branch: master - tags: true - condition: ${CONFIGURATION}=Release - provider: script - script : + script: - dotnet nuget push Source/BoogieDriver/bin/${CONFIGURATION}/Boogie*.nupkg -k ${NUGET_API_KEY} -s https://api.nuget.org/v3/index.json + skip_cleanup: true + on: + branch: master + tags: true + condition: ${CONFIGURATION}=Release - provider: releases api_key: TODO file_glob: true file: Source/BoogieDriver/bin/${CONFIGURATION}/Boogie*.nupkg + skip_cleanup: true + on: + branch: master + tags: true + condition: ${CONFIGURATION}=Release From ab0abd065b0ea911b6ca70fa7b9a2f477ca98b97 Mon Sep 17 00:00:00 2001 From: Michael Emmi Date: Thu, 19 Dec 2019 18:19:09 -0500 Subject: [PATCH 5/8] Update .travis.yml --- .travis.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.travis.yml b/.travis.yml index 30dc671e9..cf6831d9a 100644 --- a/.travis.yml +++ b/.travis.yml @@ -4,6 +4,8 @@ dist: bionic sudo: true dotnet: 3.1 mono: none +git: + depth: false env: global: - SOLUTION=Source/Boogie-NetCore.sln From 1e1ecde4b6944e241c133fee6977117ee240f30b Mon Sep 17 00:00:00 2001 From: Michael Emmi Date: Thu, 19 Dec 2019 22:14:24 -0500 Subject: [PATCH 6/8] Added API key for releases --- .travis.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index cf6831d9a..9b7d56fa0 100644 --- a/.travis.yml +++ b/.travis.yml @@ -34,7 +34,8 @@ deploy: tags: true condition: ${CONFIGURATION}=Release - provider: releases - api_key: TODO + api_key: + secure: ZjKhOiIpC6R+Xfp1iJX/1a2DD1o+tYhUefZDqRjUfM4rDZqzvOBvY7mA/1BcqNs4gXJIk3p11Kud72cPSSS8iW2EVlRm2UlfdVOf2wmGys/TILvHNDWUoVFSxhVgxbzMVULp6fIrqDypaZ0PAYZVg2loLkVI5AZ/P35ZRVaa9oE= file_glob: true file: Source/BoogieDriver/bin/${CONFIGURATION}/Boogie*.nupkg skip_cleanup: true From 8b630922c1985cf3e3b6526a13f7cf1e980ac9a6 Mon Sep 17 00:00:00 2001 From: Bernhard Kragl Date: Sat, 21 Dec 2019 00:43:27 +0100 Subject: [PATCH 7/8] Fix typo --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index df7453454..e12542cbe 100644 --- a/README.md +++ b/README.md @@ -105,7 +105,7 @@ Support for [CVC4](https://cvc4.github.io/) and ### Z3 -The current test suite assumes version 4.8.4, but earlier and never versions may +The current test suite assumes version 4.8.4, but earlier and newer versions may also work. Option 1: Make sure a Z3 executable called `z3` or `z3.exe` is in your `PATH` From 4bec6dd06590e30240039c5b4e3df547a58c3605 Mon Sep 17 00:00:00 2001 From: Bernhard Kragl Date: Sat, 21 Dec 2019 15:46:52 +0100 Subject: [PATCH 8/8] Add instructions to install Boogie from nuget.org --- README.md | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index e12542cbe..a34e7fb44 100644 --- a/README.md +++ b/README.md @@ -53,6 +53,18 @@ many aspects of the Boogie IVL but is slightly out of date. We have a public [mailing list](https://mailman.ic.ac.uk/mailman/listinfo/boogie-dev) for users of Boogie. You can also report issues on our [issue tracker](https://github.com/boogie-org/boogie/issues) +## Installation + +Boogie releases are packaged as a .NET Core global tool available at +[nuget.org](https://www.nuget.org/packages/Boogie). To install Boogie simply +run: + +``` +$ dotnet tool install --global boogie +``` + +To run Boogie, a supported SMT solver has to be available (see below). + ## Building The preferred way to build (and run) Boogie today is using .NET Core. @@ -67,7 +79,10 @@ To run Boogie, a supported SMT solver has to be available (see below). $ dotnet build Source/Boogie-NetCore.sln ``` -**TODO**: Describe how to install and run. +The compiled Boogie binary is +`Source/BoogieDriver/bin/${CONFIGURATION}/${FRAMEWORK}/BoogieDriver`. Also, a +NuGet package is placed in `Source/BoogieDriver/bin/Debug/` which can be used +for a local installation. ### Windows (requires Visual Studio)