summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.travis.yml16
-rw-r--r--Build/CodePlex.Tools.MsBuild.dllbin131072 -> 0 bytes
-rw-r--r--Build/CodePlex.Tools.Wiki.dllbin45056 -> 0 bytes
-rw-r--r--Build/updateVersionFile.xml19
-rw-r--r--README.md4
-rw-r--r--Source/AbsInt/IntervalDomain.cs8
-rw-r--r--Source/Concurrency/CivlRefinement.cs14
-rw-r--r--Source/Concurrency/CivlTypeChecker.cs219
-rw-r--r--Source/Core/Absy.cs28
-rw-r--r--Source/Core/AbsyCmd.cs18
-rw-r--r--Source/Core/AbsyQuant.cs27
-rw-r--r--Source/Core/CommandLineOptions.cs16
-rw-r--r--Source/Core/ResolutionContext.cs12
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs5
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs59
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs17
-rw-r--r--Source/Provers/SMTLib/SMTLibNamer.cs2
-rw-r--r--Source/Provers/SMTLib/TypeDeclCollector.cs5
-rw-r--r--Source/VCExpr/VCExprAST.cs3
-rw-r--r--Source/VCGeneration/Check.cs8
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs23
-rw-r--r--Source/VCGeneration/VC.cs228
-rw-r--r--Source/VCGeneration/Wlp.cs36
-rw-r--r--Source/version.ssc12
-rw-r--r--Test/aitest0/Intervals.bpl15
-rw-r--r--Test/aitest0/Intervals.bpl.expect2
-rw-r--r--Test/aitest0/Issue25.bpl14
-rw-r--r--Test/aitest0/Issue25.bpl.expect8
-rw-r--r--Test/civl/Program4.bpl119
-rw-r--r--Test/civl/Program4.bpl.expect2
-rw-r--r--Test/civl/alloc.bpl69
-rw-r--r--Test/civl/chris8.bpl15
-rw-r--r--Test/civl/chris8.bpl.expect2
-rw-r--r--Test/civl/funky.bpl133
-rw-r--r--Test/civl/funky.bpl.expect2
-rw-r--r--Test/civl/ticket.bpl5
-rw-r--r--Test/civl/treiber-stack.bpl61
-rw-r--r--Test/civl/wsq.bpl14
-rw-r--r--Test/commandline/multiple_procs_unusual_identifiers.bpl75
-rw-r--r--Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl28
-rw-r--r--Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl17
-rw-r--r--Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl17
-rw-r--r--Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl23
-rw-r--r--Test/extractloops/detLoopExtract2.bpl27
-rw-r--r--Test/extractloops/detLoopExtract2.bpl.expect2
-rw-r--r--Test/extractloops/detLoopExtractNested.bpl23
-rw-r--r--Test/extractloops/detLoopExtractNested.bpl.expect19
-rw-r--r--Test/linear/typecheck.bpl3
-rw-r--r--Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect3
-rw-r--r--Test/optimization/Optimization0.bpl84
-rw-r--r--Test/optimization/Optimization0.bpl.expect135
-rw-r--r--Test/optimization/Optimization1.bpl32
-rw-r--r--Test/optimization/Optimization1.bpl.expect5
-rw-r--r--Test/optimization/Optimization2.bpl12
-rw-r--r--Test/optimization/Optimization2.bpl.expect3
-rw-r--r--Test/optimization/Optimization3.bpl20
-rw-r--r--Test/optimization/Optimization3.bpl.expect31
-rw-r--r--Test/optimization/lit.local.cfg3
-rw-r--r--Test/test0/AssertVerifiedUnder0.bpl8
-rw-r--r--Test/test0/AssertVerifiedUnder0.bpl.expect3
-rw-r--r--Test/test1/AssertVerifiedUnder0.bpl8
-rw-r--r--Test/test1/AssertVerifiedUnder0.bpl.expect3
-rw-r--r--Test/test1/StatementIds0.bpl24
-rw-r--r--Test/test1/StatementIds0.bpl.expect5
-rw-r--r--Test/test15/CaptureState.bpl.expect18
-rw-r--r--Test/test2/BadLineNumber.bpl15
-rw-r--r--Test/test2/BadLineNumber.bpl.expect7
-rw-r--r--Test/unnecessaryassumes/unnecessaryassumes0.bpl13
-rw-r--r--Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect3
-rw-r--r--Test/unnecessaryassumes/unnecessaryassumes1.bpl23
-rw-r--r--Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect3
71 files changed, 1636 insertions, 299 deletions
diff --git a/.travis.yml b/.travis.yml
index c5d0c21d..41ee569f 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -6,16 +6,18 @@ env:
- BOOGIE_CONFIG=Debug
- BOOGIE_CONFIG=Release
install:
- - sudo apt-key adv --recv-keys --keyserver keyserver.ubuntu.com C504E590
- # FIXME: We should not be using GPUVerify's repo for Z3
- - sudo sh -c 'echo "deb http://ppa.launchpad.net/delcypher/gpuverify-smt/ubuntu precise main" > /etc/apt/sources.list.d/smt.list'
+ - wget http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_12.04/Release.key
+ - sudo apt-key add - < Release.key
+ # Use Z3 package built by the OpenSUSE build service https://build.opensuse.org/package/show/home:delcypher:z3/z3
+ - sudo sh -c "echo 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_12.04/ /' >> /etc/apt/sources.list.d/z3.list"
- sudo apt-get update
- - nuget restore ${TRAVIS_SOLUTION}
- # Install Z3
- - sudo apt-get -y install z3=4.3.2-0~precise2
+ # 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}
+ # Install Z3 executable
+ - sudo apt-get -y install 'z3=4.4.1-*'
# Install needed python tools
- sudo pip install lit OutputCheck pyyaml
- - mkdir -p Source/packages && cd Source/packages && nuget install NUnit.Runners -Version 2.6.3
+ - mkdir -p Source/packages && cd Source/packages && travis_retry nuget install NUnit.Runners -Version 2.6.3
- cd ../../
script:
- xbuild /p:Configuration=${BOOGIE_CONFIG} ${TRAVIS_SOLUTION}
diff --git a/Build/CodePlex.Tools.MsBuild.dll b/Build/CodePlex.Tools.MsBuild.dll
deleted file mode 100644
index 2e400e8e..00000000
--- a/Build/CodePlex.Tools.MsBuild.dll
+++ /dev/null
Binary files differ
diff --git a/Build/CodePlex.Tools.Wiki.dll b/Build/CodePlex.Tools.Wiki.dll
deleted file mode 100644
index 9ea2bea8..00000000
--- a/Build/CodePlex.Tools.Wiki.dll
+++ /dev/null
Binary files differ
diff --git a/Build/updateVersionFile.xml b/Build/updateVersionFile.xml
deleted file mode 100644
index cb083c7a..00000000
--- a/Build/updateVersionFile.xml
+++ /dev/null
@@ -1,19 +0,0 @@
-<Project xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
- <UsingTask AssemblyFile="CodePlex.Tools.MsBuild.dll" TaskName="CreateAssemblyInfo" />
-
- <Target Name="CreateAssemblyInfo">
- <CreateAssemblyInfo
- Version="$(CCNetLabel)"
- CreateVersionFile="true"
- ForceReadOnly="true"
- VersionFileName="..\Source\version.ssc"
- />
- <CreateAssemblyInfo
- Version="$(CCNetLabel)"
- CreateVersionFile="true"
- ForceReadOnly="true"
- VersionFileName="..\Source\version.cs"
- />
- </Target>
-</Project>
-
diff --git a/README.md b/README.md
index a976b249..1dd0ba5a 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@
|-------------------------------|---------------------------------|
| [![linux build status][1]][2] | [![windows_build_status][3]][4] |
-[1]: https://travis-ci.org/boogie-org/boogie.svg
+[1]: https://travis-ci.org/boogie-org/boogie.svg?branch=master
[2]: https://travis-ci.org/boogie-org/boogie
[3]: https://pmbuilds.inf.ethz.ch/buildStatus/icon?job=boogie
[4]: #FIXME
@@ -48,7 +48,7 @@ You can also report issues on our [issue tracker](https://github.com/boogie-org/
### Requirements
- [NuGet](https://www.nuget.org/)
-- [Z3](https://github.com/Z3Prover/z3) 4.3.2 or [CVC4](http://cvc4.cs.nyu.edu/web/) **FIXME_VERSION** (note
+- [Z3](https://github.com/Z3Prover/z3) 4.4.1 or [CVC4](http://cvc4.cs.nyu.edu/web/) **FIXME_VERSION** (note
CVC4 support is experimental)
#### Windows specific
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 0d2676f2..2fd37463 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -698,9 +698,13 @@ namespace Microsoft.Boogie.AbstractInterpretation
lo = Lo; hi = Hi;
if (hi != null) {
Lo = node.Type.IsReal ? -hi : 1 - hi;
+ } else {
+ Lo = null;
}
if (lo != null) {
Hi = node.Type.IsReal ? -lo : 1 - lo;
+ } else {
+ Hi = null;
}
}
else if (op.Op == UnaryOperator.Opcode.Not) {
@@ -880,6 +884,10 @@ namespace Microsoft.Boogie.AbstractInterpretation
if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
Lo = BigInteger.Zero;
Hi = hi1;
+ if (lo0 < lo1 && hi0 != null && hi0 < lo1) {
+ Lo = lo0;
+ Hi = hi0;
+ }
}
break;
case BinaryOperator.Opcode.RealDiv:
diff --git a/Source/Concurrency/CivlRefinement.cs b/Source/Concurrency/CivlRefinement.cs
index dfe50ef9..75ff2358 100644
--- a/Source/Concurrency/CivlRefinement.cs
+++ b/Source/Concurrency/CivlRefinement.cs
@@ -315,19 +315,9 @@ namespace Microsoft.Boogie
foreach (var v in civlTypeChecker.localVarToLocalVariableInfo.Keys)
{
LocalVariableInfo info = civlTypeChecker.localVarToLocalVariableInfo[v];
- if (info.isGhost)
+ if (layerNum < info.layer)
{
- if (info.layer != layerNum)
- {
- availableVars.Remove(v);
- }
- }
- else
- {
- if (layerNum < info.layer)
- {
- availableVars.Remove(v);
- }
+ availableVars.Remove(v);
}
}
return availableVars;
diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
index 71feb927..b426d9ed 100644
--- a/Source/Concurrency/CivlTypeChecker.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -333,26 +333,24 @@ namespace Microsoft.Boogie
public class AtomicProcedureInfo
{
public bool isPure;
- public HashSet<int> layers;
+ public LayerRange layerRange;
public AtomicProcedureInfo()
{
this.isPure = true;
- this.layers = null;
+ this.layerRange = null;
}
- public AtomicProcedureInfo(HashSet<int> layers)
+ public AtomicProcedureInfo(LayerRange layerRange)
{
this.isPure = false;
- this.layers = layers;
+ this.layerRange = layerRange;
}
}
public class LocalVariableInfo
{
- public bool isGhost;
public int layer;
- public LocalVariableInfo(bool isGhost, int layer)
+ public LocalVariableInfo(int layer)
{
- this.isGhost = isGhost;
this.layer = layer;
}
}
@@ -364,7 +362,6 @@ namespace Microsoft.Boogie
Implementation enclosingImpl;
HashSet<Variable> sharedVarsAccessed;
int introducedLocalVarsUpperBound;
- int ghostVarIntroLayerAllowed;
public Program program;
public int errorCount;
@@ -373,28 +370,15 @@ namespace Microsoft.Boogie
public Dictionary<Procedure, AtomicProcedureInfo> procToAtomicProcedureInfo;
public Dictionary<Absy, HashSet<int>> absyToLayerNums;
public Dictionary<Variable, LocalVariableInfo> localVarToLocalVariableInfo;
+ Dictionary<CallCmd, int> pureCallLayer;
public bool CallExists(CallCmd callCmd, int enclosingProcLayerNum, int layerNum)
{
Debug.Assert(procToAtomicProcedureInfo.ContainsKey(callCmd.Proc));
var atomicProcedureInfo = procToAtomicProcedureInfo[callCmd.Proc];
- if (callCmd.Proc.Modifies.Count > 0)
- {
- return enclosingProcLayerNum == layerNum;
- }
- if (callCmd.Outs.Count == 0)
- {
- return true;
- }
- var outputVar = callCmd.Outs[0].Decl;
- var localVariableInfo = localVarToLocalVariableInfo[outputVar];
- if (localVariableInfo.isGhost)
- {
- return localVariableInfo.layer == layerNum;
- }
if (atomicProcedureInfo.isPure)
{
- return localVariableInfo.layer <= layerNum;
+ return pureCallLayer[callCmd] <= layerNum;
}
else
{
@@ -456,13 +440,13 @@ namespace Microsoft.Boogie
this.enclosingImpl = null;
this.sharedVarsAccessed = null;
this.introducedLocalVarsUpperBound = int.MinValue;
- this.ghostVarIntroLayerAllowed = int.MinValue;
this.localVarToLocalVariableInfo = new Dictionary<Variable, LocalVariableInfo>();
this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();
this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();
this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
- this.procToAtomicProcedureInfo = new Dictionary<Procedure, AtomicProcedureInfo>();
+ this.procToAtomicProcedureInfo = new Dictionary<Procedure, AtomicProcedureInfo>();
+ this.pureCallLayer = new Dictionary<CallCmd, int>();
foreach (var g in program.GlobalVariables)
{
@@ -553,27 +537,39 @@ namespace Microsoft.Boogie
foreach (var proc in program.Procedures)
{
if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
- var procLayerNums = RemoveDuplicatesAndSort(FindLayers(proc.Attributes));
+ var procLayerNums = FindLayers(proc.Attributes);
if (procLayerNums.Count == 0) continue;
foreach (IdentifierExpr ie in proc.Modifies)
{
if (!globalVarToSharedVarInfo.ContainsKey(ie.Decl))
{
Error(proc, "Atomic procedure cannot modify a global variable without layer numbers");
+ continue;
}
- else if (globalVarToSharedVarInfo[ie.Decl].introLayerNum != procLayerNums[0])
- {
- Error(proc, "The introduction layer of a modified global variable must be identical to the layer of the atomic procedure");
- }
}
- if (proc.Modifies.Count == 0 || procLayerNums.Count == 1)
+ int lower, upper;
+ if (procLayerNums.Count == 1)
+ {
+ lower = procLayerNums[0];
+ upper = procLayerNums[0];
+ }
+ else if (procLayerNums.Count == 2)
{
- procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(new HashSet<int>(procLayerNums));
+ lower = procLayerNums[0];
+ upper = procLayerNums[1];
+ if (lower >= upper)
+ {
+ Error(proc, "Lower layer must be less than upper layer");
+ continue;
+ }
}
else
{
- Error(proc, "An atomic procedure with more than one layer must not modify a global variable");
+ Error(proc, "Atomic procedure must specify a layer range");
+ continue;
}
+ LayerRange layerRange = new LayerRange(lower, upper);
+ procToAtomicProcedureInfo[proc] = new AtomicProcedureInfo(layerRange);
}
if (errorCount > 0) return;
@@ -592,7 +588,7 @@ namespace Microsoft.Boogie
this.sharedVarsAccessed = new HashSet<Variable>();
(new PurityChecker(this)).VisitImplementation(impl);
LayerRange upperBound = FindLayerRange();
- LayerRange lowerBound = new LayerRange(atomicProcedureInfo.layers);
+ LayerRange lowerBound = atomicProcedureInfo.layerRange;
if (!lowerBound.Subset(upperBound))
{
Error(impl, "Atomic procedure cannot access global variable");
@@ -695,14 +691,14 @@ namespace Microsoft.Boogie
Variable v = proc.InParams[i];
var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum);
if (layer == int.MinValue) continue;
- localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer);
+ localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
}
for (int i = 0; i < proc.OutParams.Count; i++)
{
Variable v = proc.OutParams[i];
var layer = FindLocalVariableLayer(proc, v, procToActionInfo[proc].createdAtLayerNum);
if (layer == int.MinValue) continue;
- localVarToLocalVariableInfo[v] = new LocalVariableInfo(false, layer);
+ localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
}
}
foreach (Implementation node in program.Implementations)
@@ -712,21 +708,21 @@ namespace Microsoft.Boogie
{
var layer = FindLocalVariableLayer(node, v, procToActionInfo[node.Proc].createdAtLayerNum);
if (layer == int.MinValue) continue;
- localVarToLocalVariableInfo[v] = new LocalVariableInfo(QKeyValue.FindBoolAttribute(node.Attributes, "ghost"), layer);
+ localVarToLocalVariableInfo[v] = new LocalVariableInfo(layer);
}
for (int i = 0; i < node.Proc.InParams.Count; i++)
{
Variable v = node.Proc.InParams[i];
if (!localVarToLocalVariableInfo.ContainsKey(v)) continue;
var layer = localVarToLocalVariableInfo[v].layer;
- localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(false, layer);
+ localVarToLocalVariableInfo[node.InParams[i]] = new LocalVariableInfo(layer);
}
for (int i = 0; i < node.Proc.OutParams.Count; i++)
{
Variable v = node.Proc.OutParams[i];
if (!localVarToLocalVariableInfo.ContainsKey(v)) continue;
var layer = localVarToLocalVariableInfo[v].layer;
- localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(false, layer);
+ localVarToLocalVariableInfo[node.OutParams[i]] = new LocalVariableInfo(layer);
}
}
if (errorCount > 0) return;
@@ -818,13 +814,17 @@ namespace Microsoft.Boogie
}
for (int i = 0; i < node.Ins.Count; i++)
{
- var formal = node.Proc.InParams[i];
- if (localVarToLocalVariableInfo.ContainsKey(formal))
+ Visit(node.Ins[i]);
+ if (introducedLocalVarsUpperBound != int.MinValue)
{
- introducedLocalVarsUpperBound = localVarToLocalVariableInfo[formal].layer;
+ var formal = node.Proc.InParams[i];
+ if (!localVarToLocalVariableInfo.ContainsKey(formal) ||
+ introducedLocalVarsUpperBound > localVarToLocalVariableInfo[formal].layer)
+ {
+ Error(node, "An introduced local variable is accessed but not available");
+ }
+ introducedLocalVarsUpperBound = int.MinValue;
}
- Visit(node.Ins[i]);
- introducedLocalVarsUpperBound = int.MinValue;
}
for (int i = 0; i < node.Outs.Count; i++)
{
@@ -840,69 +840,83 @@ namespace Microsoft.Boogie
}
else if (procToAtomicProcedureInfo.ContainsKey(node.Proc))
{
- // 1. Outputs are either all ghost or all introduced.
- // 2. All outputs have the same layer; call it output layer.
- // 3. If callee is impure and has outputs, output layer is a member of layer set of callee.
- // 4. If callee is impure and has introduced outputs, then creation number of caller belongs to layer set of callee.
- // 5. If callee is impure and modifies globals, then creation number of caller belongs to layer set of callee.
-
- Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
- bool isGhost = false; // This assignment stops the compiler from complaining.
- // In the absence of errors, isGhost is initialized by loop below.
- foreach (var ie in node.Outs)
+ var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc];
+ if (atomicProcedureInfo.isPure)
{
- if (localVarToLocalVariableInfo.ContainsKey(ie.Decl))
+ if (node.Outs.Count > 0)
{
- var localVariableInfo = localVarToLocalVariableInfo[ie.Decl];
- if (introducedLocalVarsUpperBound == int.MinValue)
+ int inferredLayer = int.MinValue;
+ foreach (var ie in node.Outs)
{
- introducedLocalVarsUpperBound = localVariableInfo.layer;
- isGhost = localVariableInfo.isGhost;
- var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc];
- if (!atomicProcedureInfo.isPure)
+ if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl)) continue;
+ if (inferredLayer < localVarToLocalVariableInfo[ie.Decl].layer)
{
- if (!atomicProcedureInfo.layers.Contains(introducedLocalVarsUpperBound))
+ inferredLayer = localVarToLocalVariableInfo[ie.Decl].layer;
+ }
+ }
+ pureCallLayer[node] = inferredLayer;
+ if (inferredLayer != int.MinValue)
+ {
+ foreach (var ie in node.Outs)
+ {
+ if (!localVarToLocalVariableInfo.ContainsKey(ie.Decl))
{
- Error(node, "Layer of output variable must be a layer of the callee");
+ Error(node, "Output variable must be introduced");
}
- if (!isGhost && !atomicProcedureInfo.layers.Contains(enclosingProcLayerNum))
+ else if (inferredLayer != localVarToLocalVariableInfo[ie.Decl].layer)
{
- Error(node, "The creation layer of caller must be a layer of the callee");
+ Error(node, "All output variables must be introduced at the same layer");
}
}
}
- else
+ Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+ foreach (var e in node.Ins)
{
- if (localVariableInfo.layer != introducedLocalVarsUpperBound)
+ Visit(e);
+ if (inferredLayer < introducedLocalVarsUpperBound)
{
- Error(node, "All outputs must have the same layer");
- }
- if (localVariableInfo.isGhost != isGhost)
- {
- Error(node, "Outputs are either all ghost or all introduced");
+ Error(node, "An introduced local variable is not accessible");
}
+ introducedLocalVarsUpperBound = int.MinValue;
}
}
else
{
- Error(node, "Output variable must be a ghost or introduced local variable");
+ Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
+ int inferredLayer = int.MinValue;
+ foreach (var e in node.Ins)
+ {
+ Visit(e);
+ if (inferredLayer < introducedLocalVarsUpperBound)
+ {
+ inferredLayer = introducedLocalVarsUpperBound;
+ }
+ introducedLocalVarsUpperBound = int.MinValue;
+ }
+ pureCallLayer[node] = inferredLayer;
}
}
-
- if (node.Proc.Modifies.Count > 0)
+ else
{
- var atomicProcedureInfo = procToAtomicProcedureInfo[node.Proc];
- if (!atomicProcedureInfo.layers.Contains(enclosingProcLayerNum))
+ if (enclosingProcLayerNum != atomicProcedureInfo.layerRange.upperLayerNum)
{
- Error(node, "The layer of called atomic procedure must be identical to the creation layer of callee");
+ Error(node, "Creation layer of caller must be the upper bound of the layer range of callee");
+ }
+ foreach (var ie in node.Proc.Modifies)
+ {
+ if (enclosingProcLayerNum != globalVarToSharedVarInfo[ie.Decl].introLayerNum)
+ {
+ Error(node, "Creation layer of caller must be identical to the introduction layer of modified variable");
+ }
+ }
+ foreach (var ie in node.Outs)
+ {
+ if (localVarToLocalVariableInfo.ContainsKey(ie.Decl) &&
+ enclosingProcLayerNum == localVarToLocalVariableInfo[ie.Decl].layer)
+ continue;
+ Error(node, "Output variable must be introduced at the creation layer of caller");
}
- introducedLocalVarsUpperBound = enclosingProcLayerNum;
- }
- foreach (var e in node.Ins)
- {
- Visit(e);
}
- introducedLocalVarsUpperBound = int.MinValue;
return node;
}
else
@@ -973,19 +987,9 @@ namespace Microsoft.Boogie
else if ((node.Decl is Formal || node.Decl is Variable) && localVarToLocalVariableInfo.ContainsKey(node.Decl))
{
var localVariableInfo = localVarToLocalVariableInfo[node.Decl];
- if (localVariableInfo.isGhost)
+ if (introducedLocalVarsUpperBound < localVariableInfo.layer)
{
- if (ghostVarIntroLayerAllowed != localVariableInfo.layer)
- {
- Error(node, "Ghost variable inaccessible");
- }
- }
- else
- {
- if (introducedLocalVarsUpperBound < localVariableInfo.layer)
- {
- Error(node, "Introduced variable inaccessible");
- }
+ introducedLocalVarsUpperBound = localVariableInfo.layer;
}
}
return base.VisitIdentifierExpr(node);
@@ -1003,9 +1007,12 @@ namespace Microsoft.Boogie
{
sharedVarsAccessed = new HashSet<Variable>();
Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
- introducedLocalVarsUpperBound = Least(FindLayers(ensures.Attributes));
base.VisitEnsures(ensures);
CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.createdAtLayerNum);
+ if (introducedLocalVarsUpperBound > Least(FindLayers(ensures.Attributes)))
+ {
+ Error(ensures, "An introduced local variable is accessed but not available");
+ }
introducedLocalVarsUpperBound = int.MinValue;
sharedVarsAccessed = null;
}
@@ -1016,9 +1023,12 @@ namespace Microsoft.Boogie
{
sharedVarsAccessed = new HashSet<Variable>();
Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
- introducedLocalVarsUpperBound = Least(FindLayers(requires.Attributes));
base.VisitRequires(requires);
CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum);
+ if (introducedLocalVarsUpperBound > Least(FindLayers(requires.Attributes)))
+ {
+ Error(requires, "An introduced local variable is accessed but not available");
+ }
introducedLocalVarsUpperBound = int.MinValue;
sharedVarsAccessed = null;
return requires;
@@ -1033,16 +1043,13 @@ namespace Microsoft.Boogie
}
sharedVarsAccessed = new HashSet<Variable>();
Debug.Assert(introducedLocalVarsUpperBound == int.MinValue);
- var layerNums = FindLayers(node.Attributes);
- introducedLocalVarsUpperBound = Least(layerNums);
- if (layerNums.Count == 1)
- {
- ghostVarIntroLayerAllowed = layerNums[0];
- }
base.VisitAssertCmd(node);
CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum);
+ if (introducedLocalVarsUpperBound > Least(FindLayers(node.Attributes)))
+ {
+ Error(node, "An introduced local variable is accessed but not available");
+ }
introducedLocalVarsUpperBound = int.MinValue;
- ghostVarIntroLayerAllowed = int.MinValue;
sharedVarsAccessed = null;
return node;
}
@@ -1115,7 +1122,7 @@ namespace Microsoft.Boogie
{
civlTypeChecker.Error(node, "Pure procedure can only call pure procedures");
}
- else if (!callerInfo.layers.IsSubsetOf(calleeInfo.layers))
+ else if (!callerInfo.layerRange.Subset(calleeInfo.layerRange))
{
civlTypeChecker.Error(node, "Caller layers must be subset of callee layers");
}
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index c2e68002..8a8558bf 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -696,6 +696,8 @@ namespace Microsoft.Boogie {
}
}
+ public readonly ISet<string> NecessaryAssumes = new HashSet<string>();
+
public IEnumerable<Block> Blocks()
{
return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item);
@@ -750,15 +752,28 @@ namespace Microsoft.Boogie {
Contract.Assert(block != null);
var auxCmd = block.TransferCmd as GotoCmd;
if (auxCmd == null) continue;
- foreach(var bl in auxCmd.labelTargets)
+ foreach (var bl in auxCmd.labelTargets)
{
if (loopBlocks.Contains(bl)) continue;
- immSuccBlks.Add(bl);
+ immSuccBlks.Add(bl);
}
}
return immSuccBlks;
}
+ private HashSet<Block> GetBlocksInAllNaturalLoops(Block header, Graph<Block/*!*/>/*!*/ g)
+ {
+ Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option");
+ var allBlocksInNaturalLoops = new HashSet<Block>();
+ foreach (Block/*!*/ source in g.BackEdgeNodes(header))
+ {
+ Contract.Assert(source != null);
+ g.NaturalLoops(header, source).Iter(b => allBlocksInNaturalLoops.Add(b));
+ }
+ return allBlocksInNaturalLoops;
+ }
+
+
void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g,
List<Implementation/*!*/>/*!*/ loopImpls,
Dictionary<string, Dictionary<string, Block>> fullMap) {
@@ -975,10 +990,11 @@ namespace Microsoft.Boogie {
GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd;
Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null &&
auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1);
- var blksThatBreakOut = GetBreakBlocksOfLoop(header, source, g);
- var loopNodes = g.NaturalLoops(header, source);
+ //BUGFIX on 10/26/15: this contains nodes present in NaturalLoops for a different backedgenode
+ var loopNodes = GetBlocksInAllNaturalLoops(header, g); //var loopNodes = g.NaturalLoops(header, source);
foreach(var bl in auxGotoCmd.labelTargets) {
- if (!loopNodes.Contains(bl)) {
+ if (g.Nodes.Contains(bl) && //newly created blocks are not present in NaturalLoop(header, xx, g)
+ !loopNodes.Contains(bl)) {
Block auxNewBlock = new Block();
auxNewBlock.Label = ((Block)bl).Label;
//these blocks may have read/write locals that are not present in naturalLoops
@@ -2225,6 +2241,7 @@ namespace Microsoft.Boogie {
}
public class Incarnation : LocalVariable {
public int incarnationNumber;
+ public readonly Variable OriginalVariable;
public Incarnation(Variable/*!*/ var, int i) :
base(
var.tok,
@@ -2232,6 +2249,7 @@ namespace Microsoft.Boogie {
) {
Contract.Requires(var != null);
incarnationNumber = i;
+ OriginalVariable = var;
}
}
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 404945a9..2e33e1dd 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2463,6 +2463,12 @@ namespace Microsoft.Boogie {
} finally {
rc.TypeBinderState = previousTypeBinderState;
}
+
+ var id = QKeyValue.FindStringAttribute(Attributes, "id");
+ if (id != null)
+ {
+ rc.AddStatementId(tok, id);
+ }
}
public override void AddAssignedVariables(List<Variable> vars) {
@@ -2890,6 +2896,12 @@ namespace Microsoft.Boogie {
public override void Resolve(ResolutionContext rc) {
//Contract.Requires(rc != null);
Expr.Resolve(rc);
+
+ var id = QKeyValue.FindStringAttribute(Attributes, "id");
+ if (id != null)
+ {
+ rc.AddStatementId(tok, id);
+ }
}
public override void AddAssignedVariables(List<Variable> vars) {
//Contract.Requires(vars != null);
@@ -3206,8 +3218,14 @@ namespace Microsoft.Boogie {
this.Expr.Emit(stream);
stream.WriteLine(";");
}
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ ResolveAttributes(Attributes, rc);
+ base.Resolve(rc);
+ }
public override void Typecheck(TypecheckingContext tc) {
//Contract.Requires(tc != null);
+ TypecheckAttributes(Attributes, tc);
Expr.Typecheck(tc);
Contract.Assert(Expr.Type != null); // follows from Expr.Typecheck postcondition
if (!Expr.Type.Unify(Type.Bool)) {
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 9f94490b..3a27eddf 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -338,6 +338,17 @@ namespace Microsoft.Boogie {
public override void Resolve(ResolutionContext rc) {
//Contract.Requires(rc != null);
+
+ if ((Key == "minimize" || Key == "maximize") && Params.Count != 1)
+ {
+ rc.Error(this, "attributes :minimize and :maximize accept only one argument");
+ }
+
+ if (Key == "verified_under" && Params.Count != 1)
+ {
+ rc.Error(this, "attribute :verified_under accepts only one argument");
+ }
+
foreach (object p in Params) {
if (p is Expr) {
((Expr)p).Resolve(rc);
@@ -348,8 +359,20 @@ namespace Microsoft.Boogie {
public override void Typecheck(TypecheckingContext tc) {
//Contract.Requires(tc != null);
foreach (object p in Params) {
- if (p is Expr) {
- ((Expr)p).Typecheck(tc);
+ var expr = p as Expr;
+ if (expr != null) {
+ expr.Typecheck(tc);
+ }
+ if ((Key == "minimize" || Key == "maximize")
+ && (expr == null || !(expr.Type.IsInt || expr.Type.IsReal || expr.Type.IsBv)))
+ {
+ tc.Error(this, "attributes :minimize and :maximize accept only one argument of type int, real or bv");
+ break;
+ }
+ if (Key == "verified_under" && (expr == null || !expr.Type.IsBool))
+ {
+ tc.Error(this, "attribute :verified_under accepts only one argument of type bool");
+ break;
}
}
}
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index f4cba1dc..e9aa3ceb 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -11,6 +11,7 @@ using System.IO;
using System.Linq;
using System.Diagnostics;
using System.Diagnostics.Contracts;
+using System.Text.RegularExpressions;
namespace Microsoft.Boogie {
public class CommandLineOptionEngine
@@ -478,6 +479,8 @@ namespace Microsoft.Boogie {
public string AbstractHoudini = null;
public bool UseUnsatCoreForContractInfer = false;
public bool PrintAssignment = false;
+ // TODO(wuestholz): Add documentation for this flag.
+ public bool PrintNecessaryAssumes = false;
public int InlineDepth = -1;
public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values
public bool UseUncheckedContracts = false;
@@ -1618,6 +1621,7 @@ namespace Microsoft.Boogie {
ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) ||
ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||
ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
+ ps.CheckBooleanFlag("printNecessaryAssumes", ref PrintNecessaryAssumes) ||
ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) ||
ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
@@ -1700,7 +1704,7 @@ namespace Microsoft.Boogie {
// no preference
return true;
}
- return ProcsToCheck.Contains(methodFullname);
+ return ProcsToCheck.Any(s => Regex.IsMatch(methodFullname, "^" + Regex.Escape(s).Replace(@"\*", ".*") + "$"));
}
public virtual StringCollection ParseNamedArgumentList(string argList) {
@@ -1857,7 +1861,15 @@ namespace Microsoft.Boogie {
Multiple .bpl files supplied on the command line are concatenated into one
Boogie program.
- /proc:<p> : limits which procedures to check
+ /proc:<p> : Only check procedures matched by pattern <p>. This option
+ may be specified multiple times to match multiple patterns.
+ The pattern <p> matches the whole procedure name (i.e.
+ pattern ""foo"" will only match a procedure called foo and
+ not fooBar). The pattern <p> may contain * wildcards which
+ match any character zero or more times. For example the
+ pattern ""ab*d"" would match abd, abcd and abccd but not
+ Aabd nor abdD. The pattern ""*ab*d*"" would match abd,
+ abcd, abccd, Abd and abdD.
/noResolve : parse only
/noTypecheck : parse and resolve only
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 474a91dd..279e00bf 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -339,6 +339,18 @@ namespace Microsoft.Boogie {
varContext = varContext.ParentContext;
}
+ public readonly ISet<string> StatementIds = new HashSet<string>();
+
+ public void AddStatementId(IToken tok, string name)
+ {
+ if (StatementIds.Contains(name))
+ {
+ Error(tok, "more than one statement with same id: " + name);
+ return;
+ }
+ StatementIds.Add(name);
+ }
+
public void AddVariable(Variable var, bool global) {
Contract.Requires(var != null);
var previous = FindVariable(cce.NonNull(var.Name), !global);
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 9623139a..9bc855be 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1008,6 +1008,11 @@ namespace Microsoft.Boogie
CleanupCheckers(requestId);
}
+ if (CommandLineOptions.Clo.PrintNecessaryAssumes && program.NecessaryAssumes.Any())
+ {
+ Console.WriteLine("Necessary assume command(s): {0}", string.Join(", ", program.NecessaryAssumes));
+ }
+
cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
outputCollector.WriteMoreOutput();
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index e93ecee9..7e98e8f8 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -246,9 +246,9 @@ namespace Microsoft.Boogie.SMTLib
// Set produce-unsat-cores last. It seems there's a bug in Z3 where if we set it earlier its value
// gets reset by other set-option commands ( https://z3.codeplex.com/workitem/188 )
- if (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini))
+ if (CommandLineOptions.Clo.PrintNecessaryAssumes || (CommandLineOptions.Clo.ContractInfer && (CommandLineOptions.Clo.UseUnsatCoreForContractInfer || CommandLineOptions.Clo.ExplainHoudini)))
{
- SendThisVC("(set-option :produce-unsat-cores true)");
+ SendCommon("(set-option :produce-unsat-cores true)");
this.usingUnsatCore = true;
}
@@ -401,6 +401,8 @@ namespace Microsoft.Boogie.SMTLib
PrepareCommon();
+ OptimizationRequests.Clear();
+
string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
FlushAxioms();
@@ -408,7 +410,20 @@ namespace Microsoft.Boogie.SMTLib
SendThisVC("(push 1)");
SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
+
+ if (CommandLineOptions.Clo.PrintNecessaryAssumes && NamedAssumeVars != null)
+ {
+ foreach (var v in NamedAssumeVars)
+ {
+ SendThisVC(string.Format("(declare-fun {0} () Bool)", v));
+ SendThisVC(string.Format("(assert (! {0} :named {1}))", v, "aux$$" + v.Name));
+ }
+ }
+
SendThisVC(vcString);
+
+ SendOptimizationRequests();
+
FlushLogFile();
if (Process != null) {
@@ -422,6 +437,17 @@ namespace Microsoft.Boogie.SMTLib
FlushLogFile();
}
+ private void SendOptimizationRequests()
+ {
+ if (options.Solver == SolverKind.Z3 && 0 < OptimizationRequests.Count)
+ {
+ foreach (var r in OptimizationRequests)
+ {
+ SendThisVC(r);
+ }
+ }
+ }
+
public override void Reset(VCExpressionGenerator gen)
{
if (options.Solver == SolverKind.Z3)
@@ -446,6 +472,7 @@ namespace Microsoft.Boogie.SMTLib
if (options.Solver == SolverKind.Z3)
{
this.gen = gen;
+ SendThisVC("(reset)");
Namer.Reset();
common.Clear();
SetupAxiomBuilder(gen);
@@ -1264,6 +1291,22 @@ namespace Microsoft.Boogie.SMTLib
result = GetResponse();
+ var reporter = handler as VC.VCGen.ErrorReporter;
+ // TODO(wuestholz): Is the reporter ever null?
+ if (CommandLineOptions.Clo.PrintNecessaryAssumes && NamedAssumeVars != null && NamedAssumeVars.Any() && result == Outcome.Valid && reporter != null)
+ {
+ SendThisVC("(get-unsat-core)");
+ var resp = Process.GetProverResponse();
+ if (resp.Name != "")
+ {
+ reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length));
+ }
+ foreach (var arg in resp.Arguments)
+ {
+ reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length));
+ }
+ }
+
if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && result == Outcome.TimeOut)
{
#region Run timeout diagnostics
@@ -1812,6 +1855,7 @@ namespace Microsoft.Boogie.SMTLib
private Model GetErrorModel() {
if (!options.ExpectingModel())
return null;
+
SendThisVC("(get-model)");
Process.Ping();
Model theModel = null;
@@ -1906,6 +1950,9 @@ namespace Microsoft.Boogie.SMTLib
result = Outcome.Invalid;
wasUnknown = true;
break;
+ case "objectives":
+ // We ignore this.
+ break;
default:
HandleProverError("Unexpected prover response: " + resp.ToString());
break;
@@ -1944,6 +1991,8 @@ namespace Microsoft.Boogie.SMTLib
return result;
}
+ readonly IList<string> OptimizationRequests = new List<string>();
+
protected string VCExpr2String(VCExpr expr, int polarity)
{
Contract.Requires(expr != null);
@@ -1983,10 +2032,8 @@ namespace Microsoft.Boogie.SMTLib
DeclCollector.Collect(sortedExpr);
FeedTypeDeclsToProver();
-
-
AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options));
- string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options);
+ string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, OptimizationRequests);
Contract.Assert(res != null);
if (CommandLineOptions.Clo.Trace)
@@ -2096,6 +2143,7 @@ namespace Microsoft.Boogie.SMTLib
public override void Assert(VCExpr vc, bool polarity)
{
+ OptimizationRequests.Clear();
string a = "";
if (polarity)
{
@@ -2107,6 +2155,7 @@ namespace Microsoft.Boogie.SMTLib
}
AssertAxioms();
SendThisVC(a);
+ SendOptimizationRequests();
}
public override void DefineMacro(Macro f, VCExpr vc) {
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index dcf95bd2..de8798b8 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -34,14 +34,14 @@ namespace Microsoft.Boogie.SMTLib
public class SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/>
{
- public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts)
+ public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, IList<string> optReqs = null)
{
Contract.Requires(e != null);
Contract.Requires(namer != null);
Contract.Ensures(Contract.Result<string>() != null);
StringWriter sw = new StringWriter();
- SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts);
+ SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, optReqs);
Contract.Assert(lin != null);
lin.Linearise(e, LineariserOptions.Default);
return cce.NonNull(sw.ToString());
@@ -74,12 +74,15 @@ namespace Microsoft.Boogie.SMTLib
internal int UnderQuantifier = 0;
internal readonly SMTLibProverOptions ProverOptions;
- public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts)
+ readonly IList<string> OptimizationRequests;
+
+ public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList<string> optReqs = null)
{
Contract.Requires(wr != null); Contract.Requires(namer != null);
this.wr = wr;
this.Namer = namer;
this.ProverOptions = opts;
+ this.OptimizationRequests = optReqs;
}
public void Linearise(VCExpr expr, LineariserOptions options)
@@ -263,6 +266,14 @@ namespace Microsoft.Boogie.SMTLib
}
return true;
}
+ if (OptimizationRequests != null
+ && (node.Op.Equals(VCExpressionGenerator.MinimizeOp) || node.Op.Equals(VCExpressionGenerator.MaximizeOp)))
+ {
+ string optOp = node.Op.Equals(VCExpressionGenerator.MinimizeOp) ? "minimize" : "maximize";
+ OptimizationRequests.Add(string.Format("({0} {1})", optOp, ToString(node[0], Namer, ProverOptions)));
+ Linearise(node[1], options);
+ return true;
+ }
return node.Accept<bool, LineariserOptions/*!*/>(OpLineariser, options);
}
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 900bdbcc..f1179159 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Boogie.SMTLib
"flet", "implies", "!=", "if_then_else",
// Z3 extensions
"lblneg", "lblpos", "lbl-lit",
- "if", "&&", "||", "equals", "equiv", "bool",
+ "if", "&&", "||", "equals", "equiv", "bool", "minimize", "maximize",
// Boogie-defined
"real_pow", "UOrdering2", "UOrdering3",
// Floating point (final draft SMTLIB-v2.5)
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 32e28560..1c23c22f 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -255,7 +255,10 @@ void ObjectInvariant()
RegisterType(node.Type);
string decl =
"(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
- AddDeclaration(decl);
+ if (!printedName.StartsWith("assume$$"))
+ {
+ AddDeclaration(decl);
+ }
KnownVariables.Add(node);
if(declHandler != null)
declHandler.VarDecl(node);
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 0a9ba6b3..2fbb102c 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -341,6 +341,9 @@ namespace Microsoft.Boogie {
public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool);
+ public static readonly VCExprOp MinimizeOp = new VCExprCustomOp("minimize##dummy", 2, Type.Bool);
+ public static readonly VCExprOp MaximizeOp = new VCExprCustomOp("maximize##dummy", 2, Type.Bool);
+
public VCExprOp BoogieFunctionOp(Function func) {
Contract.Requires(func != null);
Contract.Ensures(Contract.Result<VCExprOp>() != null);
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 3c3b5cae..8c1ae407 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -346,7 +346,7 @@ namespace Microsoft.Boogie {
}
}
- public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {
+ public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, IList<VCExprVar> namedAssumeVars = null) {
Contract.Requires(descriptiveName != null);
Contract.Requires(vc != null);
Contract.Requires(handler != null);
@@ -356,10 +356,11 @@ namespace Microsoft.Boogie {
hasOutput = false;
outputExn = null;
this.handler = handler;
-
+
thmProver.Reset(gen);
SetTimeout();
proverStart = DateTime.UtcNow;
+ thmProver.NamedAssumeVars = namedAssumeVars;
thmProver.BeginCheck(descriptiveName, vc, handler);
// gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy
@@ -386,6 +387,9 @@ namespace Microsoft.Boogie {
// -----------------------------------------------------------------------------------------------
public abstract class ProverInterface {
+
+ public IList<VCExprVar> NamedAssumeVars;
+
public static ProverInterface CreateProver(Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, int taskID = -1) {
Contract.Requires(prog != null);
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index ae0a1147..19438924 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1133,7 +1133,8 @@ namespace VC {
}
if (returnBlocks > 1) {
string unifiedExitLabel = "GeneratedUnifiedExit";
- Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(Token.NoToken));
+ Block unifiedExit;
+ unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken));
Contract.Assert(unifiedExit != null);
foreach (Block b in impl.Blocks) {
if (b.TransferCmd is ReturnCmd) {
@@ -1539,6 +1540,26 @@ namespace VC {
PredicateCmd pc = (PredicateCmd)c.Clone();
Contract.Assert(pc != null);
+ QKeyValue current = pc.Attributes;
+ while (current != null)
+ {
+ if (current.Key == "minimize" || current.Key == "maximize") {
+ Contract.Assume(current.Params.Count == 1);
+ var param = current.Params[0] as Expr;
+ Contract.Assume(param != null && (param.Type.IsInt || param.Type.IsReal || param.Type.IsBv));
+ current.ClearParams();
+ current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
+ }
+ if (current.Key == "verified_under") {
+ Contract.Assume(current.Params.Count == 1);
+ var param = current.Params[0] as Expr;
+ Contract.Assume(param != null && param.Type.IsBool);
+ current.ClearParams();
+ current.AddParam(Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, param));
+ }
+ current = current.Next;
+ }
+
Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) {
string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 33e2f928..ad067c04 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1386,7 +1386,8 @@ namespace VC {
var exprGen = ctx.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context);
+ var namedAssumeVars = new List<VCExprVar>();
+ VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context, namedAssumeVars: namedAssumeVars);
Contract.Assert(vc != null);
if (!CommandLineOptions.Clo.UseLabels)
@@ -1414,7 +1415,7 @@ namespace VC {
string desc = cce.NonNull(impl.Name);
if (no >= 0)
desc += "_split" + no;
- checker.BeginCheck(desc, vc, reporter);
+ checker.BeginCheck(desc, vc, reporter, namedAssumeVars);
}
private void SoundnessCheck(HashSet<List<Block>/*!*/>/*!*/ cache, Block/*!*/ orig, List<Block/*!*/>/*!*/ copies) {
@@ -1519,7 +1520,7 @@ namespace VC {
}
}
- public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext)
+ public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null)
{
Contract.Requires(impl != null);
Contract.Requires(proverContext != null);
@@ -1527,10 +1528,10 @@ namespace VC {
Contract.Ensures(Contract.Result<VCExpr>() != null);
label2absy = new Dictionary<int, Absy>();
- return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);
+ return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext, namedAssumeVars: namedAssumeVars);
}
- public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) {
+ public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext, IList<VCExprVar> namedAssumeVars = null) {
Contract.Requires(impl != null);
Contract.Requires(proverContext != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -1567,7 +1568,8 @@ namespace VC {
}
break;
case CommandLineOptions.VCVariety.DagIterative:
- vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount);
+ // TODO(wuestholz): Support named assume statements not just for this encoding.
+ vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount, namedAssumeVars: namedAssumeVars);
break;
case CommandLineOptions.VCVariety.Doomed:
vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount);
@@ -2021,6 +2023,16 @@ namespace VC {
protected ProverContext/*!*/ context;
Program/*!*/ program;
+ public IEnumerable<string> NecessaryAssumes
+ {
+ get { return program.NecessaryAssumes; }
+ }
+
+ public void AddNecessaryAssume(string id)
+ {
+ program.NecessaryAssumes.Add(id);
+ }
+
public ErrorReporter(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,
Dictionary<int, Absy>/*!*/ label2absy,
List<Block/*!*/>/*!*/ blocks,
@@ -2229,10 +2241,11 @@ namespace VC {
impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List<Cmd>(), new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] })));
ResetPredecessors(impl.Blocks);
- if(CommandLineOptions.Clo.KInductionDepth < 0) {
+ var k = Math.Max(CommandLineOptions.Clo.KInductionDepth, QKeyValue.FindIntAttribute(impl.Attributes, "kInductionDepth", -1));
+ if(k < 0) {
ConvertCFG2DAGStandard(impl, edgesCut, taskID);
} else {
- ConvertCFG2DAGKInduction(impl, edgesCut, taskID);
+ ConvertCFG2DAGKInduction(impl, edgesCut, taskID, k);
}
#region Debug Tracing
@@ -2497,14 +2510,12 @@ namespace VC {
return referencedVars;
}
- private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID) {
+ private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID, int inductionK) {
// K-induction has not been adapted to be aware of these parameters which standard CFG to DAG transformation uses
Contract.Requires(edgesCut == null);
Contract.Requires(taskID == -1);
-
- int inductionK = CommandLineOptions.Clo.KInductionDepth;
- Contract.Assume(inductionK >= 0);
+ Contract.Requires(0 <= inductionK);
bool contRuleApplication = true;
while (contRuleApplication) {
@@ -2819,6 +2830,11 @@ namespace VC {
mvInfo = new ModelViewInfo(program, impl);
Convert2PassiveCmd(impl, mvInfo);
+ if (QKeyValue.FindBoolAttribute(impl.Attributes, "may_unverified_instrumentation"))
+ {
+ InstrumentWithMayUnverifiedConditions(impl, exitBlock);
+ }
+
#region Peep-hole optimizations
if (CommandLineOptions.Clo.RemoveEmptyBlocks){
#region Get rid of empty blocks
@@ -2854,6 +2870,190 @@ namespace VC {
return gotoCmdOrigins;
}
+ #region Simplified May-Unverified Analysis and Instrumentation
+
+ static void InstrumentWithMayUnverifiedConditions(Implementation impl, Block unifiedExitBlock)
+ {
+ var q = new Queue<Block>();
+ q.Enqueue(unifiedExitBlock);
+ var conditionOnBlockEntry = new Dictionary<Block, HashSet<Variable>>();
+ while (q.Any())
+ {
+ var block = q.Dequeue();
+
+ if (conditionOnBlockEntry.ContainsKey(block))
+ {
+ continue;
+ }
+
+ var gotoCmd = block.TransferCmd as GotoCmd;
+ if (gotoCmd != null && gotoCmd.labelTargets.Any(b => !conditionOnBlockEntry.ContainsKey(b)))
+ {
+ q.Enqueue(block);
+ continue;
+ }
+
+ HashSet<Variable> cond = new HashSet<Variable>();
+ if (gotoCmd != null)
+ {
+ var mayInstrs = new List<Block>();
+ bool noInstr = true;
+ foreach (var succ in gotoCmd.labelTargets)
+ {
+ var c = conditionOnBlockEntry[succ];
+ if (c != null)
+ {
+ mayInstrs.Add(succ);
+ }
+ else
+ {
+ noInstr = false;
+ }
+ cond = JoinVariableSets(cond, c);
+ }
+ if (!noInstr)
+ {
+ foreach (var instr in mayInstrs)
+ {
+ InstrumentWithCondition(instr, 0, conditionOnBlockEntry[instr]);
+ }
+ }
+ }
+
+ for (int i = block.Cmds.Count - 1; 0 <= i; i--)
+ {
+ var cmd = block.Cmds[i];
+ if (cond == null) { break; }
+
+ var assertCmd = cmd as AssertCmd;
+ if (assertCmd != null)
+ {
+ var litExpr = assertCmd.Expr as LiteralExpr;
+ if (litExpr != null && litExpr.IsTrue)
+ {
+ continue;
+ }
+
+ HashSet<Variable> vu = null;
+ if (assertCmd.VerifiedUnder == null)
+ {
+ vu = null;
+ }
+ else
+ {
+ HashSet<Variable> vars;
+ if (IsConjunctionOfAssumptionVariables(assertCmd.VerifiedUnder, out vars))
+ {
+ vu = vars;
+ // TODO(wuestholz): Maybe drop the :verified_under attribute.
+ }
+ else
+ {
+ vu = null;
+ }
+ }
+
+ if (vu == null)
+ {
+ InstrumentWithCondition(block, i + 1, cond);
+ }
+
+ cond = JoinVariableSets(cond, vu);
+ }
+ }
+
+ if (cond != null && block.Predecessors.Count == 0)
+ {
+ // TODO(wuestholz): Should we rather instrument each block?
+ InstrumentWithCondition(block, 0, cond);
+ }
+
+ foreach (var pred in block.Predecessors)
+ {
+ q.Enqueue(pred);
+ }
+
+ conditionOnBlockEntry[block] = cond;
+ }
+ }
+
+ private static void InstrumentWithCondition(Block block, int idx, HashSet<Variable> condition)
+ {
+ var conj = Expr.BinaryTreeAnd(condition.Select(v => (Expr)new IdentifierExpr(Token.NoToken, v)).ToList());
+ block.Cmds.Insert(idx, new AssumeCmd(Token.NoToken, Expr.Not(conj)));
+ }
+
+ static HashSet<Variable> JoinVariableSets(HashSet<Variable> c0, HashSet<Variable> c1)
+ {
+ // We use the following lattice:
+ // - Top: null (i.e., true)
+ // - Bottom: new HashSet<Variable>() (i.e., false)
+ // - Other Elements: new HashSet<Variable>(...) (i.e., conjunctions of assumption variables)
+
+ if (c0 == null || c1 == null)
+ {
+ return null;
+ }
+ var result = new HashSet<Variable>(c0);
+ result.UnionWith(c1);
+ return result;
+ }
+
+ static bool IsAssumptionVariableOrIncarnation(Variable v)
+ {
+ if (QKeyValue.FindBoolAttribute(v.Attributes, "assumption")) { return true; }
+ var incar = v as Incarnation;
+ return incar == null || QKeyValue.FindBoolAttribute(incar.OriginalVariable.Attributes, "assumption");
+ }
+
+ static bool IsConjunctionOfAssumptionVariables(Expr expr, out HashSet<Variable> variables)
+ {
+ Contract.Requires(expr != null);
+
+ variables = null;
+ var litExpr = expr as LiteralExpr;
+ if (litExpr != null && (litExpr.IsFalse || litExpr.IsTrue))
+ {
+ if (litExpr.IsTrue)
+ {
+ variables = new HashSet<Variable>();
+ }
+ return true;
+ }
+
+ var idExpr = expr as IdentifierExpr;
+ if (idExpr != null && IsAssumptionVariableOrIncarnation(idExpr.Decl))
+ {
+ variables = new HashSet<Variable>();
+ variables.Add(idExpr.Decl);
+ return true;
+ }
+
+ var andExpr = expr as NAryExpr;
+ if (andExpr != null)
+ {
+ var fun = andExpr.Fun as BinaryOperator;
+ if (fun != null && fun.Op == BinaryOperator.Opcode.And && andExpr.Args != null)
+ {
+ bool res = true;
+ variables = new HashSet<Variable>();
+ foreach (var op in andExpr.Args)
+ {
+ HashSet<Variable> vars;
+ var r = IsConjunctionOfAssumptionVariables(op, out vars);
+ res &= r;
+ variables = JoinVariableSets(variables, vars);
+ if (!res) { break; }
+ }
+ return res;
+ }
+ }
+
+ return false;
+ }
+
+ #endregion
+
private static void HandleSelectiveChecking(Implementation impl)
{
if (QKeyValue.FindBoolAttribute(impl.Attributes, "selective_checking") ||
@@ -3193,7 +3393,7 @@ namespace VC {
Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
out int assertionCount,
- bool isPositiveContext = true)
+ bool isPositiveContext = true, IList<VCExprVar> namedAssumeVars = null)
{
Contract.Requires(blocks != null);
Contract.Requires(proverCtxt != null);
@@ -3253,7 +3453,7 @@ namespace VC {
}
VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext);
- VCExpr vc = Wlp.Block(block, SuccCorrect, context);
+ VCExpr vc = Wlp.Block(block, SuccCorrect, context, namedAssumeVars);
assertionCount += context.AssertionCount;
VCExprVar v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool);
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index b4ee4c09..508a1400 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -48,7 +48,7 @@ namespace VC {
public class Wlp
{
- public static VCExpr Block(Block b, VCExpr N, VCContext ctxt)
+ public static VCExpr Block(Block b, VCExpr N, VCContext ctxt, IList<VCExprVar> namedAssumeVars = null)
//modifies ctxt.*;
{
Contract.Requires(b != null);
@@ -63,7 +63,7 @@ namespace VC {
for (int i = b.Cmds.Count; --i >= 0; )
{
- res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt);
+ res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt, namedAssumeVars);
}
int id = b.UniqueId;
@@ -87,7 +87,7 @@ namespace VC {
/// <summary>
/// Computes the wlp for an assert or assume command "cmd".
/// </summary>
- public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt) {
+ internal static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt, IList<VCExprVar> namedAssumeVars = null) {
Contract.Requires(cmd != null);
Contract.Requires(N != null);
Contract.Requires(ctxt != null);
@@ -186,17 +186,41 @@ namespace VC {
if (naryExpr.Fun is FunctionCall) {
int id = ac.UniqueId;
ctxt.Label2absy[id] = ac;
- return gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N);
+ return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(gen.LabelPos(cce.NonNull("si_fcall_" + id.ToString()), ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr)), N));
}
}
}
- return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
+ var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
+
+ var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id");
+ if (CommandLineOptions.Clo.PrintNecessaryAssumes && aid != null && namedAssumeVars != null)
+ {
+ var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool);
+ namedAssumeVars.Add(v);
+ expr = gen.ImpliesSimp(v, expr);
+ }
+ return MaybeWrapWithOptimization(ctxt, gen, ac.Attributes, gen.ImpliesSimp(expr, N));
} else {
Console.WriteLine(cmd.ToString());
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected command
}
}
-
+
+ private static VCExpr MaybeWrapWithOptimization(VCContext ctxt, VCExpressionGenerator gen, QKeyValue attrs, VCExpr expr)
+ {
+ var min = QKeyValue.FindExprAttribute(attrs, "minimize");
+ if (min != null)
+ {
+ expr = gen.Function(VCExpressionGenerator.MinimizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(min), expr);
+ }
+ var max = QKeyValue.FindExprAttribute(attrs, "maximize");
+ if (max != null)
+ {
+ expr = gen.Function(VCExpressionGenerator.MaximizeOp, ctxt.Ctxt.BoogieExprTranslator.Translate(max), expr);
+ }
+ return expr;
+ }
+
public static CommandLineOptions.SubsumptionOption Subsumption(AssertCmd ac) {
Contract.Requires(ac != null);
int n = QKeyValue.FindIntAttribute(ac.Attributes, "subsumption", -1);
diff --git a/Source/version.ssc b/Source/version.ssc
deleted file mode 100644
index 5bdcf170..00000000
--- a/Source/version.ssc
+++ /dev/null
@@ -1,12 +0,0 @@
-// ==++==
-//
-//
-//
-// ==--==
-// Warning: Automatically generated file. DO NOT EDIT
-// Generated at Dienstag, 5. Juli 2011 11:26:45
-
-using System.Reflection;
-[assembly: AssemblyVersion("2.2.30705.1126")]
-[assembly: AssemblyFileVersion("2.2.30705.1126")]
-
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
index fddce05a..8d40b81d 100644
--- a/Test/aitest0/Intervals.bpl
+++ b/Test/aitest0/Intervals.bpl
@@ -332,3 +332,18 @@ procedure W0(N: real)
assert N - i <= bf0 - 1.0;
}
}
+
+// mod
+
+procedure Mod0(n: int)
+ requires 10 < n;
+{
+ var i: int;
+
+ i := 0;
+ while (i < 10)
+ {
+ i := (i mod n) + 1;
+ }
+ assert i == 10;
+}
diff --git a/Test/aitest0/Intervals.bpl.expect b/Test/aitest0/Intervals.bpl.expect
index a0769ec5..980593a9 100644
--- a/Test/aitest0/Intervals.bpl.expect
+++ b/Test/aitest0/Intervals.bpl.expect
@@ -54,4 +54,4 @@ Execution trace:
Intervals.bpl(303,3): anon3_LoopHead
Intervals.bpl(303,3): anon3_LoopDone
-Boogie program verifier finished with 16 verified, 11 errors
+Boogie program verifier finished with 17 verified, 11 errors
diff --git a/Test/aitest0/Issue25.bpl b/Test/aitest0/Issue25.bpl
new file mode 100644
index 00000000..6ffcd113
--- /dev/null
+++ b/Test/aitest0/Issue25.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie -infer:j "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+const N: int;
+axiom 0 <= N;
+
+procedure vacuous_post()
+ensures (forall k, l: int :: 0 <= k && k <= l && l < N ==> N < N); // Used to verify at some point (see https://github.com/boogie-org/boogie/issues/25).
+{
+var x: int;
+x := -N;
+while (x != x) {
+}
+}
diff --git a/Test/aitest0/Issue25.bpl.expect b/Test/aitest0/Issue25.bpl.expect
new file mode 100644
index 00000000..f56502e2
--- /dev/null
+++ b/Test/aitest0/Issue25.bpl.expect
@@ -0,0 +1,8 @@
+Issue25.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
+Issue25.bpl(8,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Issue25.bpl(11,3): anon0
+ Issue25.bpl(12,1): anon2_LoopHead
+ Issue25.bpl(12,1): anon2_LoopDone
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl
index 68c2a5f3..11ba8afa 100644
--- a/Test/civl/Program4.bpl
+++ b/Test/civl/Program4.bpl
@@ -1,67 +1,138 @@
// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-type Tid;
-var {:layer 0,1} a:[Tid]int;
+var {:layer 0,2} a:[int]int;
+var {:layer 0,1} count: int;
+var {:layer 1,1} {:linear "tid"} allocated:[int]bool;
-procedure {:yields} {:layer 1} main() {
- var {:linear "tid"} tid:Tid;
+procedure {:yields} {:layer 2} main()
+requires {:layer 1} allocated == MapConstBool(false);
+{
+ var {:layer 1} {:linear "tid"} tid:int;
+ var i: int;
yield;
- while (true) {
- call tid := Allocate();
- async call P(tid);
+ assert {:layer 1} AllocInv(count, allocated);
+ while (true)
+ invariant {:layer 1} AllocInv(count, allocated);
+ {
+ call tid, i := Allocate();
+ async call P(tid, i);
yield;
+ assert {:layer 1} AllocInv(count, allocated);
}
yield;
}
-procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid)
-ensures {:layer 1} a[tid] == old(a)[tid] + 1;
+procedure {:yields} {:layer 2} P({:layer 1} {:linear "tid"} tid: int, i: int)
+requires {:layer 1} tid == i;
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
+ensures {:layer 2} a[tid] == old(a)[tid] + 1;
{
var t:int;
yield;
- assert {:layer 1} a[tid] == old(a)[tid];
- call t := Read(tid);
+ assert {:layer 1} AllocInv(count, allocated);
+ assert {:layer 2} a[tid] == old(a)[tid];
+ call t := Read(tid, i);
yield;
- assert {:layer 1} a[tid] == t;
- call Write(tid, t + 1);
+ assert {:layer 1} AllocInv(count, allocated);
+ assert {:layer 2} a[tid] == t;
+ call Write(tid, i, t + 1);
yield;
- assert {:layer 1} a[tid] == t + 1;
+ assert {:layer 1} AllocInv(count, allocated);
+ assert {:layer 2} a[tid] == t + 1;
}
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid)
+procedure {:yields} {:layer 1,2} Allocate() returns ({:layer 1} {:linear "tid"} tid: int, i: int)
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} tid == i;
+ensures {:atomic}
+|{A:
+ return true;
+}|;
{
yield;
- call tid := AllocateLow();
+ assert {:layer 1} AllocInv(count, allocated);
+ call i := AllocateLow();
+ call tid := MakeLinear(i);
yield;
+ assert {:layer 1} AllocInv(count, allocated);
}
-procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);
+procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "tid"} tid: int, i: int) returns (val: int)
+requires {:layer 1} tid == i;
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
ensures {:atomic}
|{A:
val := a[tid]; return true;
}|;
+{
+ yield;
+ assert {:layer 1} AllocInv(count, allocated);
+ call val := ReadLow(i);
+ yield;
+ assert {:layer 1} AllocInv(count, allocated);
+}
-procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int);
+procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear "tid"} tid: int, i: int, val: int)
+requires {:layer 1} tid == i;
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
ensures {:atomic}
|{A:
a[tid] := val; return true;
}|;
+{
+ yield;
+ assert {:layer 1} AllocInv(count, allocated);
+ call WriteLow(i, val);
+ yield;
+ assert {:layer 1} AllocInv(count, allocated);
+}
-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid);
-ensures {:atomic} |{ A: return true; }|;
+function {:inline} AllocInv(count: int, allocated:[int]bool): (bool)
+{
+ (forall x: int :: allocated[x] ==> x < count)
+}
+
+procedure {:yields} {:layer 0,1} ReadLow(i: int) returns (val: int);
+ensures {:atomic}
+|{A:
+ val := a[i]; return true;
+}|;
+
+procedure {:yields} {:layer 0,1} WriteLow(i: int, val: int);
+ensures {:atomic}
+|{A:
+ a[i] := val; return true;
+}|;
+procedure {:yields} {:layer 0,1} AllocateLow() returns (i: int);
+ensures {:atomic}
+|{A:
+ i := count;
+ count := i + 1;
+ return true;
+}|;
+// We can prove that this primitive procedure preserves the permission invariant locally.
+// We only need to using its specification and the definitions of TidCollector and TidSetCollector.
+procedure {:layer 1} MakeLinear(i: int) returns ({:linear "tid"} tid: int);
+requires !allocated[i];
+modifies allocated;
+ensures tid == i && allocated == old(allocated)[i := true];
-function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;
-function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;
+function {:builtin "MapConst"} MapConstBool(bool): [int]bool;
+function {:builtin "MapOr"} MapOr([int]bool, [int]bool) : [int]bool;
-function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
{
MapConstBool(false)[x := true]
}
-function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
+function {:inline} {:linear "tid"} TidSetCollector(x: [int]bool) : [int]bool
{
x
}
diff --git a/Test/civl/Program4.bpl.expect b/Test/civl/Program4.bpl.expect
index 9823d44a..f08c6e00 100644
--- a/Test/civl/Program4.bpl.expect
+++ b/Test/civl/Program4.bpl.expect
@@ -1,2 +1,2 @@
-Boogie program verifier finished with 6 verified, 0 errors
+Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Test/civl/alloc.bpl b/Test/civl/alloc.bpl
index 33535b00..68b7e6c6 100644
--- a/Test/civl/alloc.bpl
+++ b/Test/civl/alloc.bpl
@@ -11,21 +11,26 @@ axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && m
function EmptyLmap(): (lmap);
axiom (dom(EmptyLmap()) == MapConstBool(false));
-function Add(x: lmap, i: int, v: int): (lmap);
-axiom (forall x: lmap, i: int, v: int :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);
+function Add(x: lmap, i: int): (lmap);
+axiom (forall x: lmap, i: int :: dom(Add(x, i)) == dom(x)[i:=true] && map(Add(x, i)) == map(x));
function Remove(x: lmap, i: int): (lmap);
axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));
+function {:inline} PoolInv(unallocated:[int]bool, pool: lmap) : (bool)
+{
+ (forall x: int :: unallocated[x] ==> dom(pool)[x])
+}
+
procedure {:yields} {:layer 2} Main()
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
{
var {:layer 1} {:linear "mem"} l: lmap;
var i: int;
par Yield() | Dummy();
while (*)
- invariant {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ invariant {:layer 1} PoolInv(unallocated, pool);
{
call l, i := Alloc();
async call Thread(l, i);
@@ -35,8 +40,8 @@ ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
}
procedure {:yields} {:layer 2} Thread({:layer 1} {:linear_in "mem"} local_in: lmap, i: int)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
requires {:layer 1} dom(local_in)[i] && map(local_in)[i] == mem[i];
requires {:layer 2} dom(local_in)[i];
{
@@ -50,13 +55,13 @@ requires {:layer 2} dom(local_in)[i];
call o := Read(local, i);
assert {:layer 2} o == 42;
while (*)
- invariant {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ invariant {:layer 1} PoolInv(unallocated, pool);
{
call l, y := Alloc();
call l := Write(l, y, 42);
call o := Read(l, y);
assert {:layer 2} o == 42;
- call Free(l);
+ call Free(l, y);
par Yield() | Dummy();
}
par Yield() | Dummy();
@@ -68,8 +73,8 @@ procedure {:pure} {:inline 1} Copy({:linear_in "mem"} l: lmap) returns ({:linear
}
procedure {:yields} {:layer 1,2} Alloc() returns ({:layer 1} {:linear "mem"} l: lmap, i: int)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
ensures {:right} |{ A: assume dom(l)[i]; return true; }|;
{
@@ -79,17 +84,21 @@ ensures {:right} |{ A: assume dom(l)[i]; return true; }|;
call YieldMem(l, i);
}
-procedure {:yields} {:layer 1,2} Free({:layer 1} {:linear_in "mem"} l: lmap)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+procedure {:yields} {:layer 1,2} Free({:layer 1} {:linear_in "mem"} l: lmap, i: int)
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
+requires {:layer 1} dom(l)[i];
ensures {:both} |{ A: return true; }|;
{
call Yield();
+ call FreeLinear(l, i);
+ call ReturnAddr(i);
+ call Yield();
}
procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "mem"} l: lmap, i: int) returns (o: int)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
ensures {:both} |{ A: assert dom(l)[i]; o := map(l)[i]; return true; }|;
{
@@ -99,8 +108,8 @@ ensures {:both} |{ A: assert dom(l)[i]; o := map(l)[i]; return true; }|;
}
procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
ensures {:layer 1} dom(l')[i] && map(l')[i] == mem[i];
ensures {:both} |{ A: assert dom(l)[i]; l' := cons(dom(l), map(l)[i := o]); return true; }|;
@@ -116,26 +125,31 @@ modifies pool;
requires dom(pool)[i];
ensures pool == Remove(old(pool), i) && dom(l)[i] && map(l)[i] == mem[i];
+procedure {:layer 1} FreeLinear({:linear_in "mem"} l: lmap, i: int);
+modifies pool;
+requires dom(l)[i];
+ensures pool == Add(old(pool), i);
+
procedure {:layer 1} WriteLinear({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap);
requires dom(l)[i];
ensures l' == cons(dom(l), map(l)[i := o]);
procedure {:yields} {:layer 1} Yield()
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
{
yield;
- assert {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ assert {:layer 1} PoolInv(unallocated, pool);
}
procedure {:yields} {:layer 1} YieldMem({:layer 1} {:linear "mem"} l: lmap, i: int)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
{
yield;
- assert {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ assert {:layer 1} PoolInv(unallocated, pool);
assert {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
}
@@ -144,7 +158,7 @@ procedure {:yields} {:layer 2} Dummy()
yield;
}
-var {:layer 1, 1} pool: lmap;
+var {:layer 1, 1} {:linear "mem"} pool: lmap;
var {:layer 0, 1} mem:[int]int;
var {:layer 0, 1} unallocated:[int]bool;
@@ -155,4 +169,7 @@ procedure {:yields} {:layer 0, 1} WriteLow(i: int, o: int);
ensures {:atomic} |{ A: mem[i] := o; return true; }|;
procedure {:yields} {:layer 0, 1} PickAddr() returns (i: int);
-ensures {:atomic} |{ A: assume unallocated[i]; unallocated[i] := false; return true; }|; \ No newline at end of file
+ensures {:atomic} |{ A: assume unallocated[i]; unallocated[i] := false; return true; }|;
+
+procedure {:yields} {:layer 0, 1} ReturnAddr(i: int);
+ensures {:atomic} |{ A: unallocated[i] := true; return true; }|; \ No newline at end of file
diff --git a/Test/civl/chris8.bpl b/Test/civl/chris8.bpl
new file mode 100644
index 00000000..070cfec4
--- /dev/null
+++ b/Test/civl/chris8.bpl
@@ -0,0 +1,15 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var{:layer 1,1} x:int;
+
+procedure{:layer 1}{:extern} P1(i:int);
+procedure{:pure}{:extern} P2(j:int);
+
+procedure{:yields}{:layer 1,2} A1({:layer 1}i:int)
+ ensures {:atomic} |{ A: return true; }|;
+{
+ yield;
+ call P1(i);
+ call P2(i);
+ yield;
+}
diff --git a/Test/civl/chris8.bpl.expect b/Test/civl/chris8.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/civl/chris8.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/civl/funky.bpl b/Test/civl/funky.bpl
new file mode 100644
index 00000000..ad5bf271
--- /dev/null
+++ b/Test/civl/funky.bpl
@@ -0,0 +1,133 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+const nil: X;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+ MapConstBool(false)[x := true]
+}
+
+var {:layer 0, 3} A: X;
+var {:layer 0, 3} B: X;
+var {:layer 0, 3} counter: int;
+
+procedure {:yields} {:layer 0, 3} LockA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil; assume A == nil; A := tid; return true; }|;
+
+procedure {:yields} {:layer 0, 1} IncrA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter + 1; return true; }|;
+
+procedure {:yields} {:layer 0, 1} DecrA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter - 1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} UnlockA({:linear "tid"} tid: X);
+ensures {:left} |{ A: assert tid != nil && A == tid; A := nil; return true; }|;
+
+procedure {:yields} {:layer 0, 3} LockB({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil; assume B == nil; B := tid; return true; }|;
+
+procedure {:yields} {:layer 0, 2} IncrB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter + 1; return true; }|;
+
+procedure {:yields} {:layer 0, 1} DecrB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter - 1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} UnlockB({:linear "tid"} tid: X);
+ensures {:left} |{ A: assert tid != nil && B == tid; B := nil; return true; }|;
+
+procedure {:yields} {:layer 0, 3} AssertA({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} AssertB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|;
+
+procedure {:pure} AllocTid() returns ({:linear "tid"} tid: X);
+ensures tid != nil;
+
+procedure {:yields} {:layer 1, 2} AbsDecrB({:linear "tid"} tid: X)
+ensures {:right} |{ A: assert tid != nil && B == tid && counter == 0; counter := counter - 1; return true; }|;
+{
+ yield;
+ call DecrB(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 2, 3} AbsAssertA({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|;
+{
+ yield;
+ call AssertA(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 2, 3} AbsAssertB({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|;
+{
+ yield;
+ call AssertB(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 1} TA({:linear "tid"} tid: X)
+requires {:layer 1} tid != nil;
+{
+ yield;
+ call LockA(tid);
+ call IncrA(tid);
+ call DecrA(tid);
+ call UnlockA(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 2, 3} TB({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && counter == 0; return true; }|;
+{
+ yield;
+ call LockB(tid);
+ call AbsDecrB(tid);
+ call IncrB(tid);
+ call UnlockB(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 3} AbsTB({:linear "tid"} tid: X)
+requires {:layer 3} tid != nil && counter == 0;
+{
+ yield;
+ assert {:layer 3} counter == 0;
+ call TB(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 3} main({:linear "tid"} tid: X)
+requires {:layer 3} tid != nil && counter == 0;
+{
+ var {:linear "tid"} cid: X;
+
+ yield;
+ assert {:layer 3} counter == 0;
+ while (*)
+ invariant {:layer 3} counter == 0;
+ {
+ if (*) {
+ call cid := AllocTid();
+ async call TA(cid);
+ }
+ if (*) {
+ call cid := AllocTid();
+ async call AbsTB(cid);
+ }
+ yield;
+ assert {:layer 3} counter == 0;
+ call LockA(tid);
+ call AbsAssertA(tid);
+ call LockB(tid);
+ call AbsAssertB(tid);
+ call UnlockB(tid);
+ call UnlockA(tid);
+ yield;
+ assert {:layer 3} counter == 0;
+ }
+ yield;
+} \ No newline at end of file
diff --git a/Test/civl/funky.bpl.expect b/Test/civl/funky.bpl.expect
new file mode 100644
index 00000000..0a114594
--- /dev/null
+++ b/Test/civl/funky.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 75 verified, 0 errors
diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl
index 9fc55646..df19aae4 100644
--- a/Test/civl/ticket.bpl
+++ b/Test/civl/ticket.bpl
@@ -6,7 +6,6 @@ axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);
axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
type X;
-function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
var {:layer 0,2} t: int;
var {:layer 0,2} s: int;
@@ -42,7 +41,7 @@ ensures {:layer 1} {:layer 2} xl != nil;
}
procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)
-requires {:layer 2} xls' == mapconstbool(true);
+requires {:layer 2} xls' == MapConstBool(true);
{
var {:linear "tid"} tid: X;
var {:linear "tid"} xls: [X]bool;
@@ -132,7 +131,7 @@ ensures {:layer 1} Inv1(T,t);
}
procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool);
-ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
+ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);
ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|;
diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl
index 751ce861..a184886d 100644
--- a/Test/civl/treiber-stack.bpl
+++ b/Test/civl/treiber-stack.bpl
@@ -1,62 +1,71 @@
// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-type Node = int;
-const unique null: Node;
+
+const null: int;
type lmap;
-function {:linear "Node"} dom(lmap): [Node]bool;
-function map(lmap): [Node]Node;
-function {:builtin "MapConst"} MapConstBool(bool) : [Node]bool;
+function {:linear "Node"} dom(lmap): [int]bool;
+function map(lmap): [int]int;
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
function EmptyLmap(): (lmap);
axiom (dom(EmptyLmap()) == MapConstBool(false));
-function Add(x: lmap, i: Node, v: Node): (lmap);
-axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);
+function Add(x: lmap, i: int, v: int): (lmap);
+axiom (forall x: lmap, i: int, v: int :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);
-function Remove(x: lmap, i: Node): (lmap);
-axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));
+function Remove(x: lmap, i: int): (lmap);
+axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));
-procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:Node);
-ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|;
+procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:int);
+ensures {:right} |{ A: assume v == null || dom(Stack)[v] || Used[v]; return true; }|;
-procedure {:yields} {:layer 0,1} Load(i:Node) returns (v:Node);
-ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C;
+procedure {:yields} {:layer 0,1} Load(i:int) returns (v:int);
+ensures {:right} |{ A: assert dom(Stack)[i] || Used[i]; goto B,C;
B: assume dom(Stack)[i]; v := map(Stack)[i]; return true;
C: assume !dom(Stack)[i]; return true; }|;
-procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);
+procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:int, v:int) returns ({:linear "Node"} l_out:lmap);
ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|;
-procedure {:yields} {:layer 0,1} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);
+procedure {:yields} {:layer 0,1} TransferToStack(oldVal: int, newVal: int, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);
ensures {:atomic} |{ A: assert dom(l_in)[newVal];
goto B,C;
B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true;
C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|;
-procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);
+procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: int, newVal: int) returns (r: bool);
ensures {:atomic} |{ A: goto B,C;
- B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true;
+ B: assume oldVal == TopOfStack; TopOfStack := newVal; Used[oldVal] := true; Stack := Remove(Stack, oldVal); r := true; return true;
C: assume oldVal != TopOfStack; r := false; return true; }|;
-var {:layer 0} TopOfStack: Node;
+var {:layer 0} TopOfStack: int;
var {:linear "Node"} {:layer 0} Stack: lmap;
-function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool)
+function {:inline} Inv(TopOfStack: int, Stack: lmap) : (bool)
{
BetweenSet(map(Stack), TopOfStack, null)[TopOfStack] &&
Subset(BetweenSet(map(Stack), TopOfStack, null), Union(Singleton(null), dom(Stack)))
}
-var {:linear "Node"} {:layer 0} Used: lmap;
+var {:linear "Node"} {:layer 0} Used: [int]bool;
+
+function {:inline} {:linear "Node"} NodeCollector(x: int) : [int]bool
+{
+ MapConstBool(false)[x := true]
+}
+function {:inline} {:linear "Node"} NodeSetCollector(x: [int]bool) : [int]bool
+{
+ x
+}
-procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)
+procedure {:yields} {:layer 1} push(x: int, {:linear_in "Node"} x_lmap: lmap)
requires {:layer 1} dom(x_lmap)[x];
requires {:layer 1} Inv(TopOfStack, Stack);
ensures {:layer 1} Inv(TopOfStack, Stack);
ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; return true; }|;
{
- var t: Node;
+ var t: int;
var g: bool;
var {:linear "Node"} t_lmap: lmap;
@@ -71,7 +80,6 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret
call t_lmap := Store(t_lmap, x, t);
call g, t_lmap := TransferToStack(t, x, t_lmap);
if (g) {
- assert {:layer 1} map(Stack)[x] == t;
break;
}
yield;
@@ -82,13 +90,13 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret
assert {:expand} {:layer 1} Inv(TopOfStack, Stack);
}
-procedure {:yields} {:layer 1} pop() returns (t: Node)
+procedure {:yields} {:layer 1} pop() returns (t: int)
requires {:layer 1} Inv(TopOfStack, Stack);
ensures {:layer 1} Inv(TopOfStack, Stack);
-ensures {:atomic} |{ A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;
+ensures {:atomic} |{ A: assume TopOfStack != null; t := TopOfStack; Used[t] := true; TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;
{
var g: bool;
- var x: Node;
+ var x: int;
yield;
assert {:layer 1} Inv(TopOfStack, Stack);
@@ -115,7 +123,6 @@ function Subset([int]bool, [int]bool) returns (bool);
function Empty() returns ([int]bool);
function Singleton(int) returns ([int]bool);
-function Reachable([int,int]bool, int) returns ([int]bool);
function Union([int]bool, [int]bool) returns ([int]bool);
axiom(forall x:int :: !Empty()[x]);
diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl
index 39dad919..0a2227b6 100644
--- a/Test/civl/wsq.bpl
+++ b/Test/civl/wsq.bpl
@@ -89,9 +89,9 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|;
{
var t: int;
- var {:ghost} {:layer 3} oldH:int;
- var {:ghost} {:layer 3} oldT:int;
- var {:ghost} {:layer 3} oldStatusT:bool;
+ var {:layer 3} oldH:int;
+ var {:layer 3} oldT:int;
+ var {:layer 3} oldStatusT:bool;
call oldH, oldT := GhostRead();
yield;
@@ -142,8 +142,8 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
{
var h, t: int;
var chk: bool;
- var {:ghost} {:layer 3} oldH:int;
- var {:ghost} {:layer 3} oldT:int;
+ var {:layer 3} oldH:int;
+ var {:layer 3} oldT:int;
call oldH, oldT := GhostRead();
yield;
@@ -304,8 +304,8 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
{
var h, t: int;
var chk: bool;
- var {:ghost} {:layer 3} oldH:int;
- var {:ghost} {:layer 3} oldT:int;
+ var {:layer 3} oldH:int;
+ var {:layer 3} oldT:int;
call oldH, oldT := GhostRead();
yield;
diff --git a/Test/commandline/multiple_procs_unusual_identifiers.bpl b/Test/commandline/multiple_procs_unusual_identifiers.bpl
new file mode 100644
index 00000000..a3a4a4c1
--- /dev/null
+++ b/Test/commandline/multiple_procs_unusual_identifiers.bpl
@@ -0,0 +1,75 @@
+// RUN: %boogie "-proc:*Bar*" "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 10 verified, 0 errors
+
+procedure foo()
+{
+ assert false;
+}
+
+procedure bar()
+{
+ assert false;
+}
+
+/* Start should be matched */
+
+procedure _Bar()
+{
+ assert true;
+}
+
+procedure .Bar()
+{
+ assert true;
+}
+
+procedure ..Bar..()
+{
+ assert true;
+}
+
+procedure $Bar()
+{
+ assert true;
+}
+
+procedure #Bar()
+{
+ assert true;
+}
+
+procedure 'Bar''()
+{
+ assert true;
+}
+
+procedure ``Bar``()
+{
+ assert true;
+}
+
+procedure ~Bar()
+{
+ assert true;
+}
+
+procedure Bar^^()
+{
+ assert true;
+}
+
+/* This is Boogie2 claims backslash is a valid identifier
+ but the parser rejects this.
+procedure Bar\\()
+{
+ assert true;
+}
+*/
+
+procedure ??Bar()
+{
+ assert true;
+}
+
+/* End should be matched */
diff --git a/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl b/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl
new file mode 100644
index 00000000..e0f8eef3
--- /dev/null
+++ b/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl
@@ -0,0 +1,28 @@
+// RUN: %boogie "-proc:*Bar" "-proc:*Foo" "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 4 verified, 0 errors
+
+procedure foo()
+{
+ assert false;
+}
+
+procedure helpfulFoo()
+{
+ assert true;
+}
+
+procedure Foo()
+{
+ assert true;
+}
+
+procedure translucentBar()
+{
+ assert true;
+}
+
+procedure opaqueBar()
+{
+ assert true;
+}
diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl
new file mode 100644
index 00000000..0f6571ba
--- /dev/null
+++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl
@@ -0,0 +1,17 @@
+// RUN: %boogie "-proc:*Bar" "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors
+procedure foo()
+{
+ assert false;
+}
+
+procedure translucentBar()
+{
+ assert true;
+}
+
+procedure opaqueBar()
+{
+ assert true;
+}
diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl
new file mode 100644
index 00000000..5cb102e2
--- /dev/null
+++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl
@@ -0,0 +1,17 @@
+// RUN: %boogie "-proc:bar*" "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors
+procedure foo()
+{
+ assert false;
+}
+
+procedure bar()
+{
+ assert true;
+}
+
+procedure barzzz()
+{
+ assert true;
+}
diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl
new file mode 100644
index 00000000..7e19fe79
--- /dev/null
+++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl
@@ -0,0 +1,23 @@
+// RUN: %boogie "-proc:trivial*ZZZ" "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors
+procedure foo()
+{
+ assert false;
+}
+
+// should not be matched
+procedure trivialFooZZX()
+{
+ assert false;
+}
+
+procedure trivialFooZZZ()
+{
+ assert true;
+}
+
+procedure trivialBarZZZ()
+{
+ assert true;
+}
diff --git a/Test/extractloops/detLoopExtract2.bpl b/Test/extractloops/detLoopExtract2.bpl
new file mode 100644
index 00000000..f2befc53
--- /dev/null
+++ b/Test/extractloops/detLoopExtract2.bpl
@@ -0,0 +1,27 @@
+// RUN: %boogie -nologo -nologo -stratifiedInline:1 -extractLoops -deterministicExtractLoops -recursionBound:6 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+//This example checks the bug fix in the loop extract for http://symdiff.codeplex.com/workitem/4
+procedure {:entrypoint} Main() returns(r:int)
+{
+ var i, j : int;
+ var Flag : bool;
+ var b : bool;
+ i := 0;
+ j := 0;
+ Flag := false;
+ while(i<3)
+ {
+ havoc b;
+ if (b || Flag) {
+ i := i + 1;
+ j := j + 1;
+ }
+ else {
+ Flag := true;
+ j := j + 1;
+ }
+ }
+ assume !(i == j || i == j - 1);
+ return;
+}
diff --git a/Test/extractloops/detLoopExtract2.bpl.expect b/Test/extractloops/detLoopExtract2.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/extractloops/detLoopExtract2.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/extractloops/detLoopExtractNested.bpl b/Test/extractloops/detLoopExtractNested.bpl
new file mode 100644
index 00000000..65de20c1
--- /dev/null
+++ b/Test/extractloops/detLoopExtractNested.bpl
@@ -0,0 +1,23 @@
+// RUN: %boogie -nologo -stratifiedInline:1 -extractLoops -deterministicExtractLoops -recursionBound:100 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+//This example checks the bug fix in the loop extract for http://symdiff.codeplex.com/workitem/1
+
+var t: int;
+procedure {:entrypoint} NestedLoops()
+modifies t;
+//ensures t == 6;
+{
+ var i:int, j:int;
+ i, j, t := 0, 0, 0;
+ while(i < 2) {
+ j := 0;
+ while (j < 3) {
+ t := t + 1;
+ j := j + 1;
+ }
+ i := i + 1;
+ }
+ assume true; //would be provable (!true) wihtout the fix
+}
+
diff --git a/Test/extractloops/detLoopExtractNested.bpl.expect b/Test/extractloops/detLoopExtractNested.bpl.expect
new file mode 100644
index 00000000..f4932ede
--- /dev/null
+++ b/Test/extractloops/detLoopExtractNested.bpl.expect
@@ -0,0 +1,19 @@
+(0,0): Error BP5001: This assertion might not hold.
+Execution trace:
+ detLoopExtractNested.bpl(12,12): anon0
+ detLoopExtractNested.bpl(14,8): anon5_LoopBody
+ detLoopExtractNested.bpl(16,10): anon6_LoopBody
+ detLoopExtractNested.bpl(16,10): anon6_LoopBody
+ detLoopExtractNested.bpl(16,10): anon6_LoopBody
+ detLoopExtractNested.bpl(15,6): anon6_LoopDone
+ detLoopExtractNested.bpl(15,6): anon6_LoopDone
+ detLoopExtractNested.bpl(14,8): anon5_LoopBody
+ detLoopExtractNested.bpl(16,10): anon6_LoopBody
+ detLoopExtractNested.bpl(16,10): anon6_LoopBody
+ detLoopExtractNested.bpl(16,10): anon6_LoopBody
+ detLoopExtractNested.bpl(15,6): anon6_LoopDone
+ detLoopExtractNested.bpl(15,6): anon6_LoopDone
+ detLoopExtractNested.bpl(13,4): anon5_LoopDone
+ detLoopExtractNested.bpl(13,4): anon5_LoopDone
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index b4f784d3..c3c294c9 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -89,11 +89,14 @@ modifies g;
procedure {:yields} {:layer 0} I({:linear_in ""} x:int) returns({:linear ""} x':int)
{
+ yield;
x' := x;
+ yield;
}
procedure {:yields} {:layer 0} J()
{
+ yield;
}
procedure {:yields} {:layer 1} P1({:linear_in ""} x:int) returns({:linear ""} x':int)
diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect
index 9f960f26..3c0d0b20 100644
--- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect
+++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect
@@ -127,7 +127,8 @@ Execution trace:
daytona_bug2_ioctl_example_2.bpl(3832,3): inline$storm_IoCancelIrp$0$anon10#2
daytona_bug2_ioctl_example_2.bpl(3892,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#2
daytona_bug2_ioctl_example_2.bpl(3902,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Else#2
- daytona_bug2_ioctl_example_2.bpl(3928,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Then#2
+ daytona_bug2_ioctl_example_2.bpl(3915,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Else#2
+ daytona_bug2_ioctl_example_2.bpl(3923,3): inline$storm_IoAcquireCancelSpinLock$0$anon10_Then#2
daytona_bug2_ioctl_example_2.bpl(3933,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2
daytona_bug2_ioctl_example_2.bpl(3944,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2
daytona_bug2_ioctl_example_2.bpl(3949,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2
diff --git a/Test/optimization/Optimization0.bpl b/Test/optimization/Optimization0.bpl
new file mode 100644
index 00000000..24424e53
--- /dev/null
+++ b/Test/optimization/Optimization0.bpl
@@ -0,0 +1,84 @@
+// RUN: %boogie /printModel:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function may_fail(f: int) : bool;
+
+procedure test0()
+{
+ var x: int;
+
+ havoc x;
+ assume 42 < x;
+ assume {:minimize x} true;
+ assert may_fail(x);
+}
+
+procedure test1()
+{
+ var x: int;
+
+ x := 24;
+ if (*) {
+ x := 42;
+ }
+ assume {:minimize x} true;
+ assert may_fail(x);
+}
+
+procedure test2()
+{
+ var x: int;
+
+ x := 1;
+ while (*) {
+ x := x + 1;
+ }
+ assume {:minimize x} true;
+ assert x < 10;
+}
+
+procedure test3()
+{
+ var x: int;
+
+ havoc x;
+ assume x < 42;
+ assume {:maximize x} true;
+ assert may_fail(x);
+}
+
+procedure test4()
+{
+ var x: int;
+
+ x := 24;
+ if (*) {
+ x := 42;
+ }
+ assume {:maximize x} true;
+ assert may_fail(x);
+}
+
+procedure test5()
+{
+ var x: int;
+
+ x := 1;
+ while (*) {
+ x := x - 1;
+ }
+ assume {:maximize x} true;
+ assert x < 1;
+}
+
+procedure test6()
+{
+ var x: int;
+
+ x := 1;
+ if (*) {
+ x := 2;
+ }
+ assume {:maximize x} true;
+ assert may_fail(x);
+}
diff --git a/Test/optimization/Optimization0.bpl.expect b/Test/optimization/Optimization0.bpl.expect
new file mode 100644
index 00000000..f5a51848
--- /dev/null
+++ b/Test/optimization/Optimization0.bpl.expect
@@ -0,0 +1,135 @@
+*** MODEL
+%lbl%@280 -> false
+%lbl%+260 -> true
+%lbl%+39 -> true
+x@0 -> 43
+tickleBool -> {
+ true -> true
+ false -> true
+ else -> true
+}
+may_fail -> {
+ 43 -> false
+ else -> false
+}
+*** END_MODEL
+Optimization0.bpl(13,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Optimization0.bpl(10,5): anon0
+*** MODEL
+%lbl%@321 -> false
+%lbl%+299 -> true
+%lbl%+66 -> true
+%lbl%+68 -> true
+x@0@@0 -> 24
+tickleBool -> {
+ true -> true
+ false -> true
+ else -> true
+}
+may_fail -> {
+ 24 -> false
+ else -> false
+}
+*** END_MODEL
+Optimization0.bpl(25,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Optimization0.bpl(20,7): anon0
+ Optimization0.bpl(21,5): anon3_Else
+ Optimization0.bpl(24,5): anon2
+*** MODEL
+%lbl%@353 -> false
+%lbl%+335 -> true
+%lbl%+95 -> true
+%lbl%+99 -> true
+x@0@@1 -> 10
+tickleBool -> {
+ true -> true
+ false -> true
+ else -> true
+}
+*** END_MODEL
+Optimization0.bpl(37,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Optimization0.bpl(32,7): anon0
+ Optimization0.bpl(33,5): anon3_LoopHead
+ Optimization0.bpl(33,5): anon3_LoopDone
+*** MODEL
+%lbl%@386 -> false
+%lbl%+122 -> true
+%lbl%+375 -> true
+x@0@@2 -> 41
+tickleBool -> {
+ true -> true
+ false -> true
+ else -> true
+}
+may_fail -> {
+ 41 -> false
+ else -> false
+}
+*** END_MODEL
+Optimization0.bpl(47,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Optimization0.bpl(44,5): anon0
+*** MODEL
+%lbl%@414 -> false
+%lbl%+147 -> true
+%lbl%+151 -> true
+%lbl%+392 -> true
+x@0@@3 -> 42
+tickleBool -> {
+ true -> true
+ false -> true
+ else -> true
+}
+may_fail -> {
+ 42 -> false
+ else -> false
+}
+*** END_MODEL
+Optimization0.bpl(59,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Optimization0.bpl(54,7): anon0
+ Optimization0.bpl(56,11): anon3_Then
+ Optimization0.bpl(58,5): anon2
+*** MODEL
+%lbl%@446 -> false
+%lbl%+178 -> true
+%lbl%+182 -> true
+%lbl%+428 -> true
+x@0@@4 -> 1
+tickleBool -> {
+ true -> true
+ false -> true
+ else -> true
+}
+*** END_MODEL
+Optimization0.bpl(71,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Optimization0.bpl(66,7): anon0
+ Optimization0.bpl(67,5): anon3_LoopHead
+ Optimization0.bpl(67,5): anon3_LoopDone
+*** MODEL
+%lbl%@490 -> false
+%lbl%+209 -> true
+%lbl%+213 -> true
+%lbl%+468 -> true
+x@0@@5 -> 2
+tickleBool -> {
+ true -> true
+ false -> true
+ else -> true
+}
+may_fail -> {
+ 2 -> false
+ else -> false
+}
+*** END_MODEL
+Optimization0.bpl(83,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Optimization0.bpl(78,7): anon0
+ Optimization0.bpl(80,11): anon3_Then
+ Optimization0.bpl(82,5): anon2
+
+Boogie program verifier finished with 0 verified, 7 errors
diff --git a/Test/optimization/Optimization1.bpl b/Test/optimization/Optimization1.bpl
new file mode 100644
index 00000000..60df1edd
--- /dev/null
+++ b/Test/optimization/Optimization1.bpl
@@ -0,0 +1,32 @@
+// RUN: %boogie /noVerify /printModel:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0(n: int)
+{
+ assume {:minimize} true;
+}
+
+procedure test1(n: int)
+{
+ assume {:maximize} true;
+}
+
+procedure test2(n: int)
+{
+ assume {:minimize n, n} true;
+}
+
+procedure test3(n: int)
+{
+ assume {:maximize n, n} true;
+}
+
+procedure test4(n: int)
+{
+ assume {:minimize true} true;
+}
+
+procedure test5(n: int)
+{
+ assume {:maximize true} true;
+}
diff --git a/Test/optimization/Optimization1.bpl.expect b/Test/optimization/Optimization1.bpl.expect
new file mode 100644
index 00000000..d8508807
--- /dev/null
+++ b/Test/optimization/Optimization1.bpl.expect
@@ -0,0 +1,5 @@
+Optimization1.bpl(6,11): Error: attributes :minimize and :maximize accept only one argument
+Optimization1.bpl(11,11): Error: attributes :minimize and :maximize accept only one argument
+Optimization1.bpl(16,11): Error: attributes :minimize and :maximize accept only one argument
+Optimization1.bpl(21,11): Error: attributes :minimize and :maximize accept only one argument
+4 name resolution errors detected in Optimization1.bpl
diff --git a/Test/optimization/Optimization2.bpl b/Test/optimization/Optimization2.bpl
new file mode 100644
index 00000000..7d80d735
--- /dev/null
+++ b/Test/optimization/Optimization2.bpl
@@ -0,0 +1,12 @@
+// RUN: %boogie /noVerify /printModel:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0(n: int)
+{
+ assume {:minimize true} true;
+}
+
+procedure test1(n: int)
+{
+ assume {:maximize true} true;
+}
diff --git a/Test/optimization/Optimization2.bpl.expect b/Test/optimization/Optimization2.bpl.expect
new file mode 100644
index 00000000..cab2fd3d
--- /dev/null
+++ b/Test/optimization/Optimization2.bpl.expect
@@ -0,0 +1,3 @@
+Optimization2.bpl(6,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv
+Optimization2.bpl(11,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv
+2 type checking errors detected in Optimization2.bpl
diff --git a/Test/optimization/Optimization3.bpl b/Test/optimization/Optimization3.bpl
new file mode 100644
index 00000000..02499c31
--- /dev/null
+++ b/Test/optimization/Optimization3.bpl
@@ -0,0 +1,20 @@
+// RUN: %boogie /printModel:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0()
+{
+ var x: int;
+
+ assume x < 42;
+ assume {:maximize x} true;
+ assert (exists y: int :: y < x);
+}
+
+procedure test1()
+{
+ var x: int;
+
+ assume x < 42;
+ assume {:maximize x} true;
+ assert (forall y: int :: y < x);
+}
diff --git a/Test/optimization/Optimization3.bpl.expect b/Test/optimization/Optimization3.bpl.expect
new file mode 100644
index 00000000..6a0066fc
--- /dev/null
+++ b/Test/optimization/Optimization3.bpl.expect
@@ -0,0 +1,31 @@
+*** MODEL
+%lbl%@80 -> false
+%lbl%+33 -> true
+%lbl%+61 -> true
+x -> 41
+tickleBool -> {
+ true -> true
+ false -> true
+ else -> true
+}
+*** END_MODEL
+Optimization3.bpl(10,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Optimization3.bpl(8,5): anon0
+*** MODEL
+%lbl%@115 -> false
+%lbl%+105 -> true
+%lbl%+56 -> true
+x@@0 -> 41
+y@@0!1!1 -> 719
+tickleBool -> {
+ true -> true
+ false -> true
+ else -> true
+}
+*** END_MODEL
+Optimization3.bpl(19,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Optimization3.bpl(17,5): anon0
+
+Boogie program verifier finished with 0 verified, 2 errors
diff --git a/Test/optimization/lit.local.cfg b/Test/optimization/lit.local.cfg
new file mode 100644
index 00000000..35c7e558
--- /dev/null
+++ b/Test/optimization/lit.local.cfg
@@ -0,0 +1,3 @@
+# Do not run tests in this directory and below
+config.unsupported = True
+# TODO(wuestholz): Enable these tests once we can rely on a version of Z3 that includes changeset 5948013b1b04d8529bce366c0c7b87e1d88a1827.
diff --git a/Test/test0/AssertVerifiedUnder0.bpl b/Test/test0/AssertVerifiedUnder0.bpl
new file mode 100644
index 00000000..1b054f68
--- /dev/null
+++ b/Test/test0/AssertVerifiedUnder0.bpl
@@ -0,0 +1,8 @@
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0()
+{
+ assert {:verified_under} true;
+ assert {:verified_under true, false} true;
+}
diff --git a/Test/test0/AssertVerifiedUnder0.bpl.expect b/Test/test0/AssertVerifiedUnder0.bpl.expect
new file mode 100644
index 00000000..b3d8177d
--- /dev/null
+++ b/Test/test0/AssertVerifiedUnder0.bpl.expect
@@ -0,0 +1,3 @@
+AssertVerifiedUnder0.bpl(6,11): Error: attribute :verified_under accepts only one argument
+AssertVerifiedUnder0.bpl(7,11): Error: attribute :verified_under accepts only one argument
+2 name resolution errors detected in AssertVerifiedUnder0.bpl
diff --git a/Test/test1/AssertVerifiedUnder0.bpl b/Test/test1/AssertVerifiedUnder0.bpl
new file mode 100644
index 00000000..e419a5ef
--- /dev/null
+++ b/Test/test1/AssertVerifiedUnder0.bpl
@@ -0,0 +1,8 @@
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0()
+{
+ assert {:verified_under 4} true;
+ assert {:verified_under 3.0} true;
+}
diff --git a/Test/test1/AssertVerifiedUnder0.bpl.expect b/Test/test1/AssertVerifiedUnder0.bpl.expect
new file mode 100644
index 00000000..6d3c04cd
--- /dev/null
+++ b/Test/test1/AssertVerifiedUnder0.bpl.expect
@@ -0,0 +1,3 @@
+AssertVerifiedUnder0.bpl(6,11): Error: attribute :verified_under accepts only one argument of type bool
+AssertVerifiedUnder0.bpl(7,11): Error: attribute :verified_under accepts only one argument of type bool
+2 type checking errors detected in AssertVerifiedUnder0.bpl
diff --git a/Test/test1/StatementIds0.bpl b/Test/test1/StatementIds0.bpl
new file mode 100644
index 00000000..abf26159
--- /dev/null
+++ b/Test/test1/StatementIds0.bpl
@@ -0,0 +1,24 @@
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0(n: int)
+{
+ assume {:id "s0"} true;
+ assert {:id "s0"} true;
+}
+
+procedure test1()
+{
+ call {:id "s0"} P();
+}
+
+procedure test2(n: int)
+{
+ while (*)
+ invariant {:id "s0"} true;
+ invariant {:id "s0"} true;
+ {
+ }
+}
+
+procedure P();
diff --git a/Test/test1/StatementIds0.bpl.expect b/Test/test1/StatementIds0.bpl.expect
new file mode 100644
index 00000000..4783d912
--- /dev/null
+++ b/Test/test1/StatementIds0.bpl.expect
@@ -0,0 +1,5 @@
+StatementIds0.bpl(7,4): Error: more than one statement with same id: s0
+StatementIds0.bpl(12,4): Error: more than one statement with same id: s0
+StatementIds0.bpl(18,6): Error: more than one statement with same id: s0
+StatementIds0.bpl(19,6): Error: more than one statement with same id: s0
+4 name resolution errors detected in StatementIds0.bpl
diff --git a/Test/test15/CaptureState.bpl.expect b/Test/test15/CaptureState.bpl.expect
index 5d9d41c5..6939fee4 100644
--- a/Test/test15/CaptureState.bpl.expect
+++ b/Test/test15/CaptureState.bpl.expect
@@ -14,17 +14,17 @@ $mv_state_const -> 3
F -> T@FieldName!val!0
Heap -> |T@[Ref,FieldName]Int!val!0|
m -> **m
-m@0 -> (- 276)
-m@1 -> (- 275)
-m@3 -> (- 275)
+m@0 -> (- 2)
+m@1 -> (- 1)
+m@3 -> (- 1)
r -> **r
-r@0 -> (- 550)
+r@0 -> (- 2)
this -> T@Ref!val!0
x -> 719
y -> **y
Select_[Ref,FieldName]$int -> {
- |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 276)
- else -> (- 276)
+ |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 2)
+ else -> (- 2)
}
$mv_state -> {
3 0 -> true
@@ -49,13 +49,13 @@ tickleBool -> {
*** STATE top
*** END_STATE
*** STATE then
- m -> (- 276)
+ m -> (- 2)
*** END_STATE
*** STATE postUpdate0
- m -> (- 275)
+ m -> (- 1)
*** END_STATE
*** STATE end
- r -> (- 550)
+ r -> (- 2)
m -> 7
*** END_STATE
*** END_MODEL
diff --git a/Test/test2/BadLineNumber.bpl b/Test/test2/BadLineNumber.bpl
new file mode 100644
index 00000000..b8776a4e
--- /dev/null
+++ b/Test/test2/BadLineNumber.bpl
@@ -0,0 +1,15 @@
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure p();
+ ensures false;
+
+implementation p()
+{
+ if (*)
+ {
+ }
+ else
+ {
+ }
+} \ No newline at end of file
diff --git a/Test/test2/BadLineNumber.bpl.expect b/Test/test2/BadLineNumber.bpl.expect
new file mode 100644
index 00000000..bc5d1984
--- /dev/null
+++ b/Test/test2/BadLineNumber.bpl.expect
@@ -0,0 +1,7 @@
+BadLineNumber.bpl(15,1): Error BP5003: A postcondition might not hold on this return path.
+BadLineNumber.bpl(5,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ BadLineNumber.bpl(9,5): anon0
+ BadLineNumber.bpl(14,5): anon3_Else
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/unnecessaryassumes/unnecessaryassumes0.bpl b/Test/unnecessaryassumes/unnecessaryassumes0.bpl
new file mode 100644
index 00000000..a955495a
--- /dev/null
+++ b/Test/unnecessaryassumes/unnecessaryassumes0.bpl
@@ -0,0 +1,13 @@
+// RUN: %boogie /printNecessaryAssumes "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0(n: int)
+{
+ assume {:id "s0"} 0 < n;
+ assume {:id "s0"} 0 < n;
+}
+
+procedure test1(n: int)
+{
+ assume {:id "s0"} 0 < n;
+}
diff --git a/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect
new file mode 100644
index 00000000..9e420fa7
--- /dev/null
+++ b/Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect
@@ -0,0 +1,3 @@
+unnecessaryassumes0.bpl(7,4): Error: more than one statement with same id: s0
+unnecessaryassumes0.bpl(12,4): Error: more than one statement with same id: s0
+2 name resolution errors detected in unnecessaryassumes0.bpl
diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl b/Test/unnecessaryassumes/unnecessaryassumes1.bpl
new file mode 100644
index 00000000..04226dfd
--- /dev/null
+++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl
@@ -0,0 +1,23 @@
+// RUN: %boogie /printNecessaryAssumes "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0(n: int)
+{
+ assume {:id "s0"} 0 < n;
+ assert 0 <= n; // verified under s0
+}
+
+procedure test1(n: int)
+{
+ assume 0 < n;
+ assume {:id "s1"} n == 3;
+ assert 0 <= n; // verified under true
+}
+
+procedure test2(n: int)
+{
+ assume 0 < n;
+ assume {:id "s2"} n <= 42;
+ assume {:id "s3"} 42 <= n;
+ assert n == 42; // verified under s2 and s3
+}
diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect
new file mode 100644
index 00000000..dd04bb46
--- /dev/null
+++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect
@@ -0,0 +1,3 @@
+Necessary assume command(s): s0, s3, s2
+
+Boogie program verifier finished with 3 verified, 0 errors