diff options
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 Binary files differdeleted file mode 100644 index 2e400e8e..00000000 --- a/Build/CodePlex.Tools.MsBuild.dll +++ /dev/null diff --git a/Build/CodePlex.Tools.Wiki.dll b/Build/CodePlex.Tools.Wiki.dll Binary files differdeleted file mode 100644 index 9ea2bea8..00000000 --- a/Build/CodePlex.Tools.Wiki.dll +++ /dev/null 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> - @@ -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 |