Merge pull request #166 from boogie-org/netcore

Improvements of the .NET Core build

.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/

.travis.yml

@@ -1,27 +1,45 @@
 # 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
+git:
+  depth: false
 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:
+  - provider: 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:
+      secure: ZjKhOiIpC6R+Xfp1iJX/1a2DD1o+tYhUefZDqRjUfM4rDZqzvOBvY7mA/1BcqNs4gXJIk3p11Kud72cPSSS8iW2EVlRm2UlfdVOf2wmGys/TILvHNDWUoVFSxhVgxbzMVULp6fIrqDypaZ0PAYZVg2loLkVI5AZ/P35ZRVaa9oE=
+    file_glob: true
+    file: Source/BoogieDriver/bin/${CONFIGURATION}/Boogie*.nupkg
+    skip_cleanup: true
+    on:
+      branch: master
+      tags: true
+      condition: ${CONFIGURATION}=Release

README.md

@@ -53,80 +53,91 @@ 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)
 
-## Building
+## Installation
 
-### Requirements
+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:
 
-- [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)
+```
+$ dotnet tool install --global boogie
+```
 
-#### Windows specific
+To run Boogie, a supported SMT solver has to be available (see below).
 
-- Visual Studio >= 2012
+## Building
 
-#### Linux/OSX specific
+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.
 
-- Mono
+To run Boogie, a supported SMT solver has to be available (see below).
 
-### Windows
+### .NET Core
 
-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``.
+```
+$ dotnet build Source/Boogie-NetCore.sln
+```
 
-### Linux/OSX
+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.
 
-You first need to fetch the NuGet packages that Boogie depends on. If you're doing this on the command line run
+### Windows (requires Visual Studio)
 
-```
-$ cd /path/to/repository
-$ wget https://nuget.org/nuget.exe
-$ mono ./nuget.exe restore Source/Boogie.sln
-```
+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``.
 
-Note if you're using MonoDevelop it has a NuGet plug-in which you can use to "restore" the packages needed by Boogie.
+The compiled Boogie binary is `Binaries\Boogie.exe`.
 
-Note if you see an error message like the following
+### Linux/OSX (requires Mono)
 
-```
-WARNING: Error: SendFailure (Error writing headers)
-Unable to find version '2.6.3' of package 'NUnit.Runners'.
-```
+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.
 
-then you need to initialise Mono's certificate store by running
+Fetch the NuGet packages that Boogie depends on:
 
 ```
-$ mozroots --import --sync
+$ nuget restore Source/Boogie.sln
 ```
 
-then you can build by running
+Build Boogie:
 
 ```
 $ msbuild Source/Boogie.sln
 ```
 
-Finally make sure there is a symlink to Z3 in the Binaries directory
-(replace with ``cvc4`` if using CVC4 instead).
+The compiled Boogie binary is `Binaries/Boogie.exe`, which can be executed with
+`mono` or using the wrapper script `Binaries/boogie`.
 
-```
-$ ln -s /usr/bin/z3 Binaries/z3.exe
-```
+## Backend SMT Solver
 
-## 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.
 
-On a Windows system call the Boogie binary:
+### Z3
 
-```
-$ Binaries\Boogie.exe
-```
+The current test suite assumes version 4.8.4, but earlier and newer versions may
+also work.
 
-On a non-Windows system use the wrapper script:
+Option 1: Make sure a Z3 executable called `z3` or `z3.exe` is in your `PATH`
+environment variable.
 
-```
-$ Binaries/boogie
-```
+Option 2: Call Boogie with `/z3exe:<path>`.
+
+### CVC4 (experimental)
+
+Call Boogie with `/proverOpt:SOLVER=CVC4 /cvc4exe:<path>`.
+
+### Yices2 (experimental)
+
+Call Boogie with `/proverOpt:SOLVER=Yices2 /yices2exe:<path> /useArrayTheory`.
+
+Works for unquantified fragments, e.g. arrays + arithmetic + bitvectors. Does
+not work for quantifiers, generalized arrays, datatypes.
 
 ## Testing
 

Source/BoogieDriver/BoogieDriver-NetCore.csproj

@@ -13,7 +13,6 @@
     <AssemblyName>BoogieDriver</AssemblyName>
     <TargetFramework>netcoreapp3.1</TargetFramework>
     <GeneratePackageOnBuild>true</GeneratePackageOnBuild>
-    <PackageOutputPath>nupkg</PackageOutputPath>
     <PackAsTool>true</PackAsTool>
     <ToolCommandName>boogie</ToolCommandName>
   </PropertyGroup>

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();
     }

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'))

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