From a6b78b0ea28c22744fa846d7729b5c50247f9987 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Fri, 16 Oct 2015 14:08:21 -0700 Subject: bug fix in the type checking of calls to atomic procedures --- Source/Concurrency/CivlRefinement.cs | 14 +-- Source/Concurrency/CivlTypeChecker.cs | 219 ++++++++++++++++++---------------- Test/civl/chris8.bpl | 15 +++ Test/civl/chris8.bpl.expect | 2 + Test/civl/wsq.bpl | 14 +-- 5 files changed, 139 insertions(+), 125 deletions(-) create mode 100644 Test/civl/chris8.bpl create mode 100644 Test/civl/chris8.bpl.expect 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 layers; + public LayerRange layerRange; public AtomicProcedureInfo() { this.isPure = true; - this.layers = null; + this.layerRange = null; } - public AtomicProcedureInfo(HashSet 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 sharedVarsAccessed; int introducedLocalVarsUpperBound; - int ghostVarIntroLayerAllowed; public Program program; public int errorCount; @@ -373,28 +370,15 @@ namespace Microsoft.Boogie public Dictionary procToAtomicProcedureInfo; public Dictionary> absyToLayerNums; public Dictionary localVarToLocalVariableInfo; + Dictionary 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(); this.absyToLayerNums = new Dictionary>(); this.globalVarToSharedVarInfo = new Dictionary(); this.procToActionInfo = new Dictionary(); - this.procToAtomicProcedureInfo = new Dictionary(); + this.procToAtomicProcedureInfo = new Dictionary(); + this.pureCallLayer = new Dictionary(); 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(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(); (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(); 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(); 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(); 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/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/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; -- cgit v1.2.3 From deef37064f673be0391a7224ed8551b1e68be829 Mon Sep 17 00:00:00 2001 From: Shuvendu Lahiri Date: Mon, 26 Oct 2015 17:27:52 -0700 Subject: Bug fix for deterministExtractLoops for Shaobo's example --- Source/Core/Absy.cs | 21 ++++++-- Test/extractloops/detLoopExtract2.bpl | 27 ++++++++++ Test/extractloops/detLoopExtract2.bpl.expect | 2 + Test/snapshots/Snapshots41.v0.bpl | 70 ++++++++++++------------- Test/snapshots/Snapshots41.v1.bpl | 78 ++++++++++++++-------------- 5 files changed, 120 insertions(+), 78 deletions(-) create mode 100644 Test/extractloops/detLoopExtract2.bpl create mode 100644 Test/extractloops/detLoopExtract2.bpl.expect diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index c2e68002..8c04007b 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -750,15 +750,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 GetBlocksInAllNaturalLoops(Block header, Graph/*!*/ g) + { + Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option"); + var allBlocksInNaturalLoops = new HashSet(); + 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/*!*/ g, List/*!*/ loopImpls, Dictionary> fullMap) { @@ -975,8 +988,8 @@ 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)) { Block auxNewBlock = new Block(); 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/snapshots/Snapshots41.v0.bpl b/Test/snapshots/Snapshots41.v0.bpl index 631fe544..dbfe3e2d 100644 --- a/Test/snapshots/Snapshots41.v0.bpl +++ b/Test/snapshots/Snapshots41.v0.bpl @@ -1,35 +1,35 @@ -procedure {:checksum "0"} M(x: int); -implementation {:id "M"} {:checksum "1"} M(x: int) -{ assert x < 20 || 10 <= x; // always true - assert x < 10; // error - call Other(x); // error: precondition violation -} - -procedure {:checksum "10"} Other(y: int); - requires 0 <= y; -implementation {:id "Other"} {:checksum "11"} Other(y: int) -{ -} - -procedure {:checksum "20"} Posty() returns (z: int); - ensures 2 <= z; // error: postcondition violation -implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int) -{ - var t: int; - t := 20; - if (t < z) { - } else { // the postcondition violation occurs on this 'else' branch - } -} - -procedure {:checksum "30"} NoChangeWhazzoeva(u: int); -implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int) -{ - assert u != 53; // error -} - -procedure {:checksum "40"} NoChangeAndCorrect(); -implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() -{ - assert true; -} +procedure {:checksum "0"} M(x: int); +implementation {:id "M"} {:checksum "1"} M(x: int) +{ assert x < 20 || 10 <= x; // always true + assert x < 10; // error + call Other(x); // error: precondition violation +} + +procedure {:checksum "10"} Other(y: int); + requires 0 <= y; +implementation {:id "Other"} {:checksum "11"} Other(y: int) +{ +} + +procedure {:checksum "20"} Posty() returns (z: int); + ensures 2 <= z; // error: postcondition violation +implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int) +{ + var t: int; + t := 20; + if (t < z) { + } else { // the postcondition violation occurs on this 'else' branch + } +} + +procedure {:checksum "30"} NoChangeWhazzoeva(u: int); +implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int) +{ + assert u != 53; // error +} + +procedure {:checksum "40"} NoChangeAndCorrect(); +implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() +{ + assert true; +} diff --git a/Test/snapshots/Snapshots41.v1.bpl b/Test/snapshots/Snapshots41.v1.bpl index 0cd9fbf9..9864e0e4 100644 --- a/Test/snapshots/Snapshots41.v1.bpl +++ b/Test/snapshots/Snapshots41.v1.bpl @@ -1,39 +1,39 @@ -procedure {:checksum "0"} M(x: int); -implementation {:id "M"} {:checksum "1"} M(x: int) -{ -assert x < 20 || 10 <= x; // always true - - assert x < 10; // error - call Other(x); // error: precondition violation - assert x == 7; // error: this is a new error in v1 -} - - - procedure {:checksum "10"} Other(y: int); - requires 0 <= y; - implementation {:id "Other"} {:checksum "11"} Other(y: int) - { - } - - - -procedure {:checksum "20"} Posty() returns (z: int); - ensures 2 <= z; // error: postcondition violation -implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int) -{ - var t: int; - t := 20; - if (t < z) { - assert true; // this is a new assert - } else { // the postcondition violation occurs on this 'else' branch - } -} - - procedure {:checksum "30"} NoChangeWhazzoeva(u: int); - implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int) - { - assert u != 53; // error - } - -procedure {:checksum "40"} NoChangeAndCorrect(); -implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() { assert true; } +procedure {:checksum "0"} M(x: int); +implementation {:id "M"} {:checksum "1"} M(x: int) +{ +assert x < 20 || 10 <= x; // always true + + assert x < 10; // error + call Other(x); // error: precondition violation + assert x == 7; // error: this is a new error in v1 +} + + + procedure {:checksum "10"} Other(y: int); + requires 0 <= y; + implementation {:id "Other"} {:checksum "11"} Other(y: int) + { + } + + + +procedure {:checksum "20"} Posty() returns (z: int); + ensures 2 <= z; // error: postcondition violation +implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int) +{ + var t: int; + t := 20; + if (t < z) { + assert true; // this is a new assert + } else { // the postcondition violation occurs on this 'else' branch + } +} + + procedure {:checksum "30"} NoChangeWhazzoeva(u: int); + implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int) + { + assert u != 53; // error + } + +procedure {:checksum "40"} NoChangeAndCorrect(); +implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() { assert true; } -- cgit v1.2.3 From e037ca99cdc163ca43690aaef3c380ebc1ce1962 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 26 Oct 2015 21:12:35 -0700 Subject: fixed --- Test/linear/typecheck.bpl | 3 +++ 1 file changed, 3 insertions(+) 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) -- cgit v1.2.3 From 02f5c060ca5ce6bff003034ed634c114d5592398 Mon Sep 17 00:00:00 2001 From: Shuvendu Lahiri Date: Tue, 27 Oct 2015 17:40:33 -0700 Subject: fix for deterministicExtractLoops for nested loops --- Source/Core/Absy.cs | 3 ++- Test/extractloops/detLoopExtractNested.bpl | 23 +++++++++++++++++++++++ Test/extractloops/detLoopExtractNested.bpl.expect | 19 +++++++++++++++++++ 3 files changed, 44 insertions(+), 1 deletion(-) create mode 100644 Test/extractloops/detLoopExtractNested.bpl create mode 100644 Test/extractloops/detLoopExtractNested.bpl.expect diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 8c04007b..d2243085 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -991,7 +991,8 @@ namespace Microsoft.Boogie { //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 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 -- cgit v1.2.3 From 0732077773c80e86f8fbbc0be94ae9c034ad1924 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 29 Oct 2015 18:40:23 -0500 Subject: Add support for annotating implementations with k-ind. depth. --- Source/VCGeneration/VC.cs | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 33e2f928..79f56934 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2229,10 +2229,11 @@ namespace VC { impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List(), new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { 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 +2498,12 @@ namespace VC { return referencedVars; } - private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary> edgesCut, int taskID) { + private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary> 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) { -- cgit v1.2.3 From 90f2ae09d29b841ff42cdd8f441bda684c3421e2 Mon Sep 17 00:00:00 2001 From: Shaobo Date: Fri, 30 Oct 2015 14:53:07 -0600 Subject: Added wild card matching for /proc flag --- Source/Core/CommandLineOptions.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index f4cba1dc..d7644915 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 @@ -1700,7 +1701,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) { -- cgit v1.2.3 From 12c5ff0211e844156706f8e617c94ab221c1b456 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 31 Oct 2015 08:19:49 +0000 Subject: Added test cases for the new asterisk wildcard behaviour of the ``-proc`` command line argument. --- .../multiple_procs_unusual_identifiers.bpl | 75 ++++++++++++++++++++++ ...ultiple_procs_verify_four_asterisk_wildcard.bpl | 28 ++++++++ ...le_procs_verify_two_asterisk_wildcard_begin.bpl | 17 +++++ ...iple_procs_verify_two_asterisk_wildcard_end.bpl | 17 +++++ ...rocs_verify_two_asterisk_wildcard_inbetween.bpl | 23 +++++++ 5 files changed, 160 insertions(+) create mode 100644 Test/commandline/multiple_procs_unusual_identifiers.bpl create mode 100644 Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl create mode 100644 Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl create mode 100644 Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl create mode 100644 Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl 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; +} -- cgit v1.2.3 From 8d1864f189552068d22f174b6eeaee202568de36 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 31 Oct 2015 08:52:02 +0000 Subject: Document the new behaviour of the ``-proc:`` command line option in the output of Boogie's help. --- Source/Core/CommandLineOptions.cs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index d7644915..3892bbc0 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1858,7 +1858,15 @@ namespace Microsoft.Boogie { Multiple .bpl files supplied on the command line are concatenated into one Boogie program. - /proc:

: limits which procedures to check + /proc:

: Only check procedures matched by pattern

. This option + may be specified multiple times to match multiple patterns. + The pattern

matches the whole procedure name (i.e. + pattern ""foo"" will only match a procedure called foo and + not fooBar). The pattern

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 -- cgit v1.2.3 From f049d2ec646244bc40964b36d961966fe2a3e4dc Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 16 Nov 2015 12:04:37 -0600 Subject: Add support for identifying unnecessary assumes. --- Source/Core/Absy.cs | 2 ++ Source/Core/AbsyCmd.cs | 12 +++++++++ Source/Core/CommandLineOptions.cs | 3 +++ Source/Core/ResolutionContext.cs | 12 +++++++++ Source/ExecutionEngine/ExecutionEngine.cs | 5 ++++ Source/Provers/SMTLib/ProverInterface.cs | 30 ++++++++++++++++++++-- Source/VCGeneration/Check.cs | 16 ++++++++++-- Source/VCGeneration/VC.cs | 28 ++++++++++++++------ Source/VCGeneration/Wlp.cs | 17 +++++++++--- Test/unnecessaryassumes/unnecessaryassumes0.bpl | 13 ++++++++++ .../unnecessaryassumes0.bpl.expect | 3 +++ Test/unnecessaryassumes/unnecessaryassumes1.bpl | 23 +++++++++++++++++ .../unnecessaryassumes1.bpl.expect | 3 +++ 13 files changed, 151 insertions(+), 16 deletions(-) create mode 100644 Test/unnecessaryassumes/unnecessaryassumes0.bpl create mode 100644 Test/unnecessaryassumes/unnecessaryassumes0.bpl.expect create mode 100644 Test/unnecessaryassumes/unnecessaryassumes1.bpl create mode 100644 Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index d2243085..8be4f24e 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -696,6 +696,8 @@ namespace Microsoft.Boogie { } } + public readonly ISet NecessaryAssumes = new HashSet(); + public IEnumerable Blocks() { return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item); diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 404945a9..c33f0743 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 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 vars) { //Contract.Requires(vars != null); diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 3892bbc0..e9aa3ceb 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -479,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; @@ -1619,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) || 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 StatementIds = new HashSet(); + + 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..cb8442e5 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; } @@ -408,6 +408,15 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(push 1)"); SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")"); + + if (NamedAssumeVars != null) + { + foreach (var v in NamedAssumeVars) + { + SendThisVC(string.Format("(assert (! {0} :named {1}))", v, "aux$$" + v.Name)); + } + } + SendThisVC(vcString); FlushLogFile(); @@ -446,6 +455,7 @@ namespace Microsoft.Boogie.SMTLib if (options.Solver == SolverKind.Z3) { this.gen = gen; + SendThisVC("(reset)"); Namer.Reset(); common.Clear(); SetupAxiomBuilder(gen); @@ -1264,6 +1274,22 @@ namespace Microsoft.Boogie.SMTLib result = GetResponse(); + var reporter = handler as VC.VCGen.ErrorReporter; + // TODO(wuestholz): Is the reporter ever null? + if (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 diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 3c3b5cae..da445a00 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 namedAssumeVars = null) { Contract.Requires(descriptiveName != null); Contract.Requires(vc != null); Contract.Requires(handler != null); @@ -357,9 +357,18 @@ namespace Microsoft.Boogie { outputExn = null; this.handler = handler; - thmProver.Reset(gen); + if (namedAssumeVars != null && namedAssumeVars.Any()) + { + // TODO(wuestholz): Avoid doing a full reset. This is currently necessary for old versions of Z3 due to a bug. + thmProver.FullReset(gen); + } + else + { + 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 +395,9 @@ namespace Microsoft.Boogie { // ----------------------------------------------------------------------------------------------- public abstract class ProverInterface { + + public IList 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/VC.cs b/Source/VCGeneration/VC.cs index 79f56934..2762fc72 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(); + 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/*!*/>/*!*/ cache, Block/*!*/ orig, List/*!*/ copies) { @@ -1519,7 +1520,7 @@ namespace VC { } } - public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary/*!*/ label2absy, ProverContext proverContext) + public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary/*!*/ label2absy, ProverContext proverContext, IList namedAssumeVars = null) { Contract.Requires(impl != null); Contract.Requires(proverContext != null); @@ -1527,10 +1528,10 @@ namespace VC { Contract.Ensures(Contract.Result() != null); label2absy = new Dictionary(); - return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext); + return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext, namedAssumeVars: namedAssumeVars); } - public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary/*!*/ label2absy, ProverContext proverContext) { + public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary/*!*/ label2absy, ProverContext proverContext, IList namedAssumeVars = null) { Contract.Requires(impl != null); Contract.Requires(proverContext != null); Contract.Ensures(Contract.Result() != 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 NecessaryAssumes + { + get { return program.NecessaryAssumes; } + } + + public void AddNecessaryAssume(string id) + { + program.NecessaryAssumes.Add(id); + } + public ErrorReporter(Dictionary/*!*/ gotoCmdOrigins, Dictionary/*!*/ label2absy, List/*!*/ blocks, @@ -3192,7 +3204,7 @@ namespace VC { Dictionary label2absy, ProverContext proverCtxt, out int assertionCount, - bool isPositiveContext = true) + bool isPositiveContext = true, IList namedAssumeVars = null) { Contract.Requires(blocks != null); Contract.Requires(proverCtxt != null); @@ -3252,7 +3264,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..74b77188 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 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 { ///

/// Computes the wlp for an assert or assume command "cmd". /// - 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 namedAssumeVars = null) { Contract.Requires(cmd != null); Contract.Requires(N != null); Contract.Requires(ctxt != null); @@ -190,7 +190,16 @@ namespace VC { } } } - 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 (aid != null && namedAssumeVars != null) + { + var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool); + namedAssumeVars.Add(v); + expr = gen.ImpliesSimp(v, expr); + } + return gen.ImpliesSimp(expr, N); } else { Console.WriteLine(cmd.ToString()); Contract.Assert(false); throw new cce.UnreachableException(); // unexpected command 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 -- cgit v1.2.3 From 75a179354ea7b78682904575d5692efa0068fcf0 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 16 Nov 2015 12:13:45 -0600 Subject: Add a test. --- Test/test1/StatementIds0.bpl | 15 +++++++++++++++ Test/test1/StatementIds0.bpl.expect | 3 +++ 2 files changed, 18 insertions(+) create mode 100644 Test/test1/StatementIds0.bpl create mode 100644 Test/test1/StatementIds0.bpl.expect diff --git a/Test/test1/StatementIds0.bpl b/Test/test1/StatementIds0.bpl new file mode 100644 index 00000000..85b9cd36 --- /dev/null +++ b/Test/test1/StatementIds0.bpl @@ -0,0 +1,15 @@ +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0(n: int) +{ + assume {:id "s0"} 0 < n; + assert {:id "s0"} 0 < n; +} + +procedure test1(n: int) +{ + call {:id "s0"} P(); +} + +procedure P(); diff --git a/Test/test1/StatementIds0.bpl.expect b/Test/test1/StatementIds0.bpl.expect new file mode 100644 index 00000000..944c3257 --- /dev/null +++ b/Test/test1/StatementIds0.bpl.expect @@ -0,0 +1,3 @@ +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 +2 name resolution errors detected in StatementIds0.bpl -- cgit v1.2.3 From 67a0a458aad9ece669a49cca085b695a56003d0e Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 16 Nov 2015 12:50:24 -0600 Subject: Add a test. --- Test/test1/StatementIds0.bpl | 15 ++++++++++++--- Test/test1/StatementIds0.bpl.expect | 4 +++- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/Test/test1/StatementIds0.bpl b/Test/test1/StatementIds0.bpl index 85b9cd36..abf26159 100644 --- a/Test/test1/StatementIds0.bpl +++ b/Test/test1/StatementIds0.bpl @@ -3,13 +3,22 @@ procedure test0(n: int) { - assume {:id "s0"} 0 < n; - assert {:id "s0"} 0 < n; + assume {:id "s0"} true; + assert {:id "s0"} true; } -procedure test1(n: int) +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 index 944c3257..4783d912 100644 --- a/Test/test1/StatementIds0.bpl.expect +++ b/Test/test1/StatementIds0.bpl.expect @@ -1,3 +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 -2 name resolution errors detected in StatementIds0.bpl +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 -- cgit v1.2.3 From 3f417a0223b4e5d0139c5b035e573895ac2ad84c Mon Sep 17 00:00:00 2001 From: qunyanm Date: Mon, 16 Nov 2015 11:03:28 -0800 Subject: Use EndCurly token for the ReturnCmd when creating unifiedExit Instead of using NoToken for the ReturnCmd, use the EndCurly when creating unifiedExit. --- Source/VCGeneration/ConditionGeneration.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index ae0a1147..b26750ab 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1133,7 +1133,7 @@ namespace VC { } if (returnBlocks > 1) { string unifiedExitLabel = "GeneratedUnifiedExit"; - Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), new ReturnCmd(Token.NoToken)); + Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), new ReturnCmd(impl.StructuredStmts.EndCurly)); Contract.Assert(unifiedExit != null); foreach (Block b in impl.Blocks) { if (b.TransferCmd is ReturnCmd) { -- cgit v1.2.3 From a799e128af68911228d081202ba0bd294ced4a4f Mon Sep 17 00:00:00 2001 From: qunyanm Date: Mon, 16 Nov 2015 12:27:44 -0800 Subject: Use EndCurly token for the ReturnCmd when creating unifiedExit Instead of using NoToken for the ReturnCmd, use the EndCurly, if it exists, when creating unifiedExit --- Source/VCGeneration/ConditionGeneration.cs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index b26750ab..0e5fce82 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1133,7 +1133,12 @@ namespace VC { } if (returnBlocks > 1) { string unifiedExitLabel = "GeneratedUnifiedExit"; - Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), new ReturnCmd(impl.StructuredStmts.EndCurly)); + Block unifiedExit; + if (impl.StructuredStmts != null) { + unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), new ReturnCmd(impl.StructuredStmts.EndCurly)); + } else { + unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), new ReturnCmd(Token.NoToken)); + } Contract.Assert(unifiedExit != null); foreach (Block b in impl.Blocks) { if (b.TransferCmd is ReturnCmd) { -- cgit v1.2.3 From e25dac8edab3e3f23db7c83b393ed388840d239f Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Tue, 17 Nov 2015 14:03:06 -0600 Subject: Fix issue #25. --- Source/AbsInt/IntervalDomain.cs | 4 ++++ Test/aitest0/Issue25.bpl | 14 ++++++++++++++ Test/aitest0/Issue25.bpl.expect | 8 ++++++++ 3 files changed, 26 insertions(+) create mode 100644 Test/aitest0/Issue25.bpl create mode 100644 Test/aitest0/Issue25.bpl.expect diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 0d2676f2..ee9d632b 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) { 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..80eeb1a7 --- /dev/null +++ b/Test/aitest0/Issue25.bpl.expect @@ -0,0 +1,8 @@ +Bug25.bpl(12,1): Error BP5003: A postcondition might not hold on this return path. +Bug25.bpl(8,1): Related location: This is the postcondition that might not hold. +Execution trace: + Bug25.bpl(11,3): anon0 + Bug25.bpl(12,1): anon2_LoopHead + Bug25.bpl(12,1): anon2_LoopDone + +Boogie program verifier finished with 0 verified, 1 error -- cgit v1.2.3 From 9a4448732895ffe451642b2bebd95dcf1ed371d4 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Tue, 17 Nov 2015 14:13:58 -0600 Subject: Fix test output. --- Test/aitest0/Issue25.bpl.expect | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Test/aitest0/Issue25.bpl.expect b/Test/aitest0/Issue25.bpl.expect index 80eeb1a7..f56502e2 100644 --- a/Test/aitest0/Issue25.bpl.expect +++ b/Test/aitest0/Issue25.bpl.expect @@ -1,8 +1,8 @@ -Bug25.bpl(12,1): Error BP5003: A postcondition might not hold on this return path. -Bug25.bpl(8,1): Related location: This is the postcondition that might not hold. +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: - Bug25.bpl(11,3): anon0 - Bug25.bpl(12,1): anon2_LoopHead - Bug25.bpl(12,1): anon2_LoopDone + 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 -- cgit v1.2.3 From a51f4e6cba57b6711e36ef482f4e320c9cf0542f Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Wed, 18 Nov 2015 15:46:24 -0600 Subject: Add experimental support for optimization (requires Z3 build after changeset 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). --- Source/Core/AbsyCmd.cs | 6 + Source/Core/AbsyQuant.cs | 17 ++- Source/Provers/SMTLib/ProverInterface.cs | 21 +++- Source/Provers/SMTLib/SMTLibLineariser.cs | 17 ++- Source/Provers/SMTLib/SMTLibNamer.cs | 2 +- Source/VCExpr/VCExprAST.cs | 3 + Source/VCGeneration/ConditionGeneration.cs | 12 ++ Source/VCGeneration/Wlp.cs | 21 +++- Test/optimization/Optimization0.bpl | 86 ++++++++++++++ Test/optimization/Optimization0.bpl.expect | 182 +++++++++++++++++++++++++++++ Test/optimization/Optimization1.bpl | 32 +++++ Test/optimization/Optimization1.bpl.expect | 5 + Test/optimization/Optimization2.bpl | 12 ++ Test/optimization/Optimization2.bpl.expect | 3 + Test/optimization/lit.local.cfg | 3 + 15 files changed, 410 insertions(+), 12 deletions(-) create mode 100644 Test/optimization/Optimization0.bpl create mode 100644 Test/optimization/Optimization0.bpl.expect create mode 100644 Test/optimization/Optimization1.bpl create mode 100644 Test/optimization/Optimization1.bpl.expect create mode 100644 Test/optimization/Optimization2.bpl create mode 100644 Test/optimization/Optimization2.bpl.expect create mode 100644 Test/optimization/lit.local.cfg diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index c33f0743..2e33e1dd 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -3218,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..39f18657 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -338,6 +338,12 @@ 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"); + } + foreach (object p in Params) { if (p is Expr) { ((Expr)p).Resolve(rc); @@ -348,8 +354,15 @@ 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; } } } diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index cb8442e5..ca530da2 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -401,6 +401,8 @@ namespace Microsoft.Boogie.SMTLib PrepareCommon(); + OptimizationRequests.Clear(); + string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))"; FlushAxioms(); @@ -418,6 +420,15 @@ namespace Microsoft.Boogie.SMTLib } SendThisVC(vcString); + + if (options.Solver == SolverKind.Z3 && 0 < OptimizationRequests.Count) + { + foreach (var r in OptimizationRequests) + { + SendThisVC(r); + } + } + FlushLogFile(); if (Process != null) { @@ -1838,6 +1849,7 @@ namespace Microsoft.Boogie.SMTLib private Model GetErrorModel() { if (!options.ExpectingModel()) return null; + SendThisVC("(get-model)"); Process.Ping(); Model theModel = null; @@ -1932,6 +1944,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; @@ -1970,6 +1985,8 @@ namespace Microsoft.Boogie.SMTLib return result; } + readonly IList OptimizationRequests = new List(); + protected string VCExpr2String(VCExpr expr, int polarity) { Contract.Requires(expr != null); @@ -2009,10 +2026,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) 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 { - public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts) + public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, IList optReqs = null) { Contract.Requires(e != null); Contract.Requires(namer != null); Contract.Ensures(Contract.Result() != 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 OptimizationRequests; + + public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList 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(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/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 0a9ba6b3..2a06447e 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 VCExprNAryOp(2, Type.Bool); + public static readonly VCExprOp MaximizeOp = new VCExprNAryOp(2, Type.Bool); + public VCExprOp BoogieFunctionOp(Function func) { Contract.Requires(func != null); Contract.Ensures(Contract.Result() != null); diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index ae0a1147..5971d6f8 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1539,6 +1539,18 @@ 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)); + } + 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/Wlp.cs b/Source/VCGeneration/Wlp.cs index 74b77188..741ed723 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -186,7 +186,7 @@ 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)); } } } @@ -199,13 +199,28 @@ namespace VC { namedAssumeVars.Add(v); expr = gen.ImpliesSimp(v, expr); } - return gen.ImpliesSimp(expr, N); + 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/Test/optimization/Optimization0.bpl b/Test/optimization/Optimization0.bpl new file mode 100644 index 00000000..c704c855 --- /dev/null +++ b/Test/optimization/Optimization0.bpl @@ -0,0 +1,86 @@ +// RUN: %boogie /doNotUseLabels /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); +} + +// TODO(wuestholz): Make this work without the /doNotUseLabels flag. diff --git a/Test/optimization/Optimization0.bpl.expect b/Test/optimization/Optimization0.bpl.expect new file mode 100644 index 00000000..d2f9b606 --- /dev/null +++ b/Test/optimization/Optimization0.bpl.expect @@ -0,0 +1,182 @@ +*** MODEL +%lbl%@280 -> false +%lbl%+260 -> true +%lbl%+39 -> true +x@0 -> 43 +ControlFlow -> { + 0 0 -> 260 + 0 260 -> 39 + 0 39 -> (- 280) + else -> 260 +} +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%@328 -> false +%lbl%+306 -> true +%lbl%+66 -> true +%lbl%+68 -> true +x@0@@0 -> 24 +ControlFlow -> { + 0 0 -> 306 + 0 306 -> 66 + 0 68 -> (- 328) + 0 66 -> 68 + else -> 306 +} +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%@360 -> false +%lbl%+342 -> true +%lbl%+95 -> true +%lbl%+99 -> true +x@0@@1 -> 10 +ControlFlow -> { + 0 0 -> 342 + 0 342 -> 95 + 0 95 -> 99 + 0 99 -> (- 360) + else -> 342 +} +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%@393 -> false +%lbl%+122 -> true +%lbl%+382 -> true +x@0@@2 -> 41 +ControlFlow -> { + 0 0 -> 382 + 0 382 -> 122 + 0 122 -> (- 393) + else -> 382 +} +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%@421 -> false +%lbl%+147 -> true +%lbl%+151 -> true +%lbl%+399 -> true +x@0@@3 -> 42 +ControlFlow -> { + 0 0 -> 399 + 0 399 -> 147 + 0 147 -> 151 + 0 151 -> (- 421) + else -> 399 +} +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%@453 -> false +%lbl%+178 -> true +%lbl%+182 -> true +%lbl%+435 -> true +x@0@@4 -> 1 +ControlFlow -> { + 0 0 -> 435 + 0 435 -> 178 + 0 178 -> 182 + 0 182 -> (- 453) + else -> 435 +} +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%@497 -> false +%lbl%+209 -> true +%lbl%+213 -> true +%lbl%+475 -> true +x@0@@5 -> 2 +ControlFlow -> { + 0 0 -> 475 + 0 475 -> 209 + 0 209 -> 213 + 0 213 -> (- 497) + else -> 475 +} +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/lit.local.cfg b/Test/optimization/lit.local.cfg new file mode 100644 index 00000000..158a1e4d --- /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 Z3 4.4.2 or higher. -- cgit v1.2.3 From c8d15354d033713295a6c55802c6dfe55a95f2b5 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Wed, 18 Nov 2015 22:21:47 -0600 Subject: Improve experimental support for optimization (requires Z3 changeset 5948013b1b04d8529bce366c0c7b87e1d88a1827 or later). --- Test/optimization/Optimization0.bpl | 2 +- Test/optimization/Optimization0.bpl.expect | 71 +++++------------------------- 2 files changed, 13 insertions(+), 60 deletions(-) diff --git a/Test/optimization/Optimization0.bpl b/Test/optimization/Optimization0.bpl index c704c855..d000fd79 100644 --- a/Test/optimization/Optimization0.bpl +++ b/Test/optimization/Optimization0.bpl @@ -1,4 +1,4 @@ -// RUN: %boogie /doNotUseLabels /printModel:4 "%s" > "%t" +// RUN: %boogie /printModel:4 "%s" > "%t" // RUN: %diff "%s.expect" "%t" function may_fail(f: int) : bool; diff --git a/Test/optimization/Optimization0.bpl.expect b/Test/optimization/Optimization0.bpl.expect index d2f9b606..f5a51848 100644 --- a/Test/optimization/Optimization0.bpl.expect +++ b/Test/optimization/Optimization0.bpl.expect @@ -3,12 +3,6 @@ %lbl%+260 -> true %lbl%+39 -> true x@0 -> 43 -ControlFlow -> { - 0 0 -> 260 - 0 260 -> 39 - 0 39 -> (- 280) - else -> 260 -} tickleBool -> { true -> true false -> true @@ -23,18 +17,11 @@ Optimization0.bpl(13,5): Error BP5001: This assertion might not hold. Execution trace: Optimization0.bpl(10,5): anon0 *** MODEL -%lbl%@328 -> false -%lbl%+306 -> true +%lbl%@321 -> false +%lbl%+299 -> true %lbl%+66 -> true %lbl%+68 -> true x@0@@0 -> 24 -ControlFlow -> { - 0 0 -> 306 - 0 306 -> 66 - 0 68 -> (- 328) - 0 66 -> 68 - else -> 306 -} tickleBool -> { true -> true false -> true @@ -51,18 +38,11 @@ Execution trace: Optimization0.bpl(21,5): anon3_Else Optimization0.bpl(24,5): anon2 *** MODEL -%lbl%@360 -> false -%lbl%+342 -> true +%lbl%@353 -> false +%lbl%+335 -> true %lbl%+95 -> true %lbl%+99 -> true x@0@@1 -> 10 -ControlFlow -> { - 0 0 -> 342 - 0 342 -> 95 - 0 95 -> 99 - 0 99 -> (- 360) - else -> 342 -} tickleBool -> { true -> true false -> true @@ -75,16 +55,10 @@ Execution trace: Optimization0.bpl(33,5): anon3_LoopHead Optimization0.bpl(33,5): anon3_LoopDone *** MODEL -%lbl%@393 -> false +%lbl%@386 -> false %lbl%+122 -> true -%lbl%+382 -> true +%lbl%+375 -> true x@0@@2 -> 41 -ControlFlow -> { - 0 0 -> 382 - 0 382 -> 122 - 0 122 -> (- 393) - else -> 382 -} tickleBool -> { true -> true false -> true @@ -99,18 +73,11 @@ Optimization0.bpl(47,5): Error BP5001: This assertion might not hold. Execution trace: Optimization0.bpl(44,5): anon0 *** MODEL -%lbl%@421 -> false +%lbl%@414 -> false %lbl%+147 -> true %lbl%+151 -> true -%lbl%+399 -> true +%lbl%+392 -> true x@0@@3 -> 42 -ControlFlow -> { - 0 0 -> 399 - 0 399 -> 147 - 0 147 -> 151 - 0 151 -> (- 421) - else -> 399 -} tickleBool -> { true -> true false -> true @@ -127,18 +94,11 @@ Execution trace: Optimization0.bpl(56,11): anon3_Then Optimization0.bpl(58,5): anon2 *** MODEL -%lbl%@453 -> false +%lbl%@446 -> false %lbl%+178 -> true %lbl%+182 -> true -%lbl%+435 -> true +%lbl%+428 -> true x@0@@4 -> 1 -ControlFlow -> { - 0 0 -> 435 - 0 435 -> 178 - 0 178 -> 182 - 0 182 -> (- 453) - else -> 435 -} tickleBool -> { true -> true false -> true @@ -151,18 +111,11 @@ Execution trace: Optimization0.bpl(67,5): anon3_LoopHead Optimization0.bpl(67,5): anon3_LoopDone *** MODEL -%lbl%@497 -> false +%lbl%@490 -> false %lbl%+209 -> true %lbl%+213 -> true -%lbl%+475 -> true +%lbl%+468 -> true x@0@@5 -> 2 -ControlFlow -> { - 0 0 -> 475 - 0 475 -> 209 - 0 209 -> 213 - 0 213 -> (- 497) - else -> 475 -} tickleBool -> { true -> true false -> true -- cgit v1.2.3 From 51d0b71fa4fd0795c56f1cddbd85b49625c6c91e Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 19 Nov 2015 11:09:58 -0600 Subject: Minor changes --- Source/VCExpr/VCExprAST.cs | 4 ++-- Test/optimization/Optimization0.bpl | 2 -- Test/optimization/lit.local.cfg | 2 +- 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 2a06447e..2fbb102c 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -341,8 +341,8 @@ namespace Microsoft.Boogie { public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool); - public static readonly VCExprOp MinimizeOp = new VCExprNAryOp(2, Type.Bool); - public static readonly VCExprOp MaximizeOp = new VCExprNAryOp(2, 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); diff --git a/Test/optimization/Optimization0.bpl b/Test/optimization/Optimization0.bpl index d000fd79..24424e53 100644 --- a/Test/optimization/Optimization0.bpl +++ b/Test/optimization/Optimization0.bpl @@ -82,5 +82,3 @@ procedure test6() assume {:maximize x} true; assert may_fail(x); } - -// TODO(wuestholz): Make this work without the /doNotUseLabels flag. diff --git a/Test/optimization/lit.local.cfg b/Test/optimization/lit.local.cfg index 158a1e4d..35c7e558 100644 --- a/Test/optimization/lit.local.cfg +++ b/Test/optimization/lit.local.cfg @@ -1,3 +1,3 @@ # Do not run tests in this directory and below config.unsupported = True -# TODO(wuestholz): Enable these tests once we can rely on Z3 4.4.2 or higher. +# TODO(wuestholz): Enable these tests once we can rely on a version of Z3 that includes changeset 5948013b1b04d8529bce366c0c7b87e1d88a1827. -- cgit v1.2.3 From 261c125776d911fda9b545094cb182f3ceb0cdd2 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 19 Nov 2015 11:18:42 -0600 Subject: Add a test. --- Test/optimization/Optimization3.bpl | 20 +++++++++++++++++++ Test/optimization/Optimization3.bpl.expect | 31 ++++++++++++++++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100644 Test/optimization/Optimization3.bpl create mode 100644 Test/optimization/Optimization3.bpl.expect diff --git a/Test/optimization/Optimization3.bpl b/Test/optimization/Optimization3.bpl new file mode 100644 index 00000000..c1dba49c --- /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; // TODO(wuestholz): Currently, Z3 does not produce a model with "x == 41" here. It seems like this is due to the fact that it returns "unknown". + 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..6f308d7d --- /dev/null +++ b/Test/optimization/Optimization3.bpl.expect @@ -0,0 +1,31 @@ +*** MODEL +%lbl%@80 -> false +%lbl%+33 -> true +%lbl%+61 -> true +x -> (- 962) +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 -- cgit v1.2.3 From 3e37476e15593fe7889b2644bcf389f90f985e35 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 19 Nov 2015 14:19:25 -0600 Subject: Update test output after Nikolaj's enhancement in Z3. --- Test/optimization/Optimization3.bpl | 2 +- Test/optimization/Optimization3.bpl.expect | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Test/optimization/Optimization3.bpl b/Test/optimization/Optimization3.bpl index c1dba49c..02499c31 100644 --- a/Test/optimization/Optimization3.bpl +++ b/Test/optimization/Optimization3.bpl @@ -6,7 +6,7 @@ procedure test0() var x: int; assume x < 42; - assume {:maximize x} true; // TODO(wuestholz): Currently, Z3 does not produce a model with "x == 41" here. It seems like this is due to the fact that it returns "unknown". + assume {:maximize x} true; assert (exists y: int :: y < x); } diff --git a/Test/optimization/Optimization3.bpl.expect b/Test/optimization/Optimization3.bpl.expect index 6f308d7d..6a0066fc 100644 --- a/Test/optimization/Optimization3.bpl.expect +++ b/Test/optimization/Optimization3.bpl.expect @@ -2,7 +2,7 @@ %lbl%@80 -> false %lbl%+33 -> true %lbl%+61 -> true -x -> (- 962) +x -> 41 tickleBool -> { true -> true false -> true -- cgit v1.2.3 From 5bb7ad4c69ed1c782e50272d37bf116007a52f4c Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 19 Nov 2015 14:39:36 -0600 Subject: Fix issue with partially-verified assertions. --- Source/Core/AbsyQuant.cs | 10 ++++++++++ Source/VCGeneration/ConditionGeneration.cs | 8 ++++++++ Test/test0/AssertVerifiedUnder0.bpl | 8 ++++++++ Test/test0/AssertVerifiedUnder0.bpl.expect | 3 +++ Test/test1/AssertVerifiedUnder0.bpl | 8 ++++++++ Test/test1/AssertVerifiedUnder0.bpl.expect | 3 +++ 6 files changed, 40 insertions(+) create mode 100644 Test/test0/AssertVerifiedUnder0.bpl create mode 100644 Test/test0/AssertVerifiedUnder0.bpl.expect create mode 100644 Test/test1/AssertVerifiedUnder0.bpl create mode 100644 Test/test1/AssertVerifiedUnder0.bpl.expect diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 39f18657..3a27eddf 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -344,6 +344,11 @@ namespace Microsoft.Boogie { 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); @@ -364,6 +369,11 @@ namespace Microsoft.Boogie { 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; + } } } public void AddLast(QKeyValue other) { diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 5971d6f8..6a2eec29 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1549,8 +1549,16 @@ namespace VC { 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/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 -- cgit v1.2.3 From f19110ec25d4ee962558627150d22e4c8a26a2a0 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Fri, 20 Nov 2015 11:24:17 -0600 Subject: Add simplified may-unverified analysis and instrumentation. --- Source/Core/Absy.cs | 2 + Source/VCGeneration/VC.cs | 189 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 191 insertions(+) diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 8be4f24e..8a8558bf 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2241,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, @@ -2248,6 +2249,7 @@ namespace Microsoft.Boogie { ) { Contract.Requires(var != null); incarnationNumber = i; + OriginalVariable = var; } } diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 2762fc72..ad067c04 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2830,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 @@ -2865,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(); + q.Enqueue(unifiedExitBlock); + var conditionOnBlockEntry = new Dictionary>(); + 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 cond = new HashSet(); + if (gotoCmd != null) + { + var mayInstrs = new List(); + 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 vu = null; + if (assertCmd.VerifiedUnder == null) + { + vu = null; + } + else + { + HashSet 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 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 JoinVariableSets(HashSet c0, HashSet c1) + { + // We use the following lattice: + // - Top: null (i.e., true) + // - Bottom: new HashSet() (i.e., false) + // - Other Elements: new HashSet(...) (i.e., conjunctions of assumption variables) + + if (c0 == null || c1 == null) + { + return null; + } + var result = new HashSet(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 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(); + } + return true; + } + + var idExpr = expr as IdentifierExpr; + if (idExpr != null && IsAssumptionVariableOrIncarnation(idExpr.Decl)) + { + variables = new HashSet(); + 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(); + foreach (var op in andExpr.Args) + { + HashSet 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") || -- cgit v1.2.3 From fe8de9444fb6ce90216a9b8268d8a13daa9a9f2a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 21 Nov 2015 18:27:06 +0000 Subject: Teach the TravisCI build to use the ``travis_retry`` command when using NuGet. The motivation here is that the ``nuget`` command is a little flakey (sometimes it times out) in the legacy TravisCI infrastructure. This command will retry the command passed to it a few times. Hopefully this will stop the random build failures we've been having. --- .travis.yml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index c5d0c21d..11ed4d64 100644 --- a/.travis.yml +++ b/.travis.yml @@ -10,12 +10,13 @@ install: # 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' - sudo apt-get update - - nuget restore ${TRAVIS_SOLUTION} + # 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 - sudo apt-get -y install z3=4.3.2-0~precise2 # 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} -- cgit v1.2.3 From 280cb724b7499ed4f09f9a54e5ae457b1eb254ae Mon Sep 17 00:00:00 2001 From: qunyanm Date: Wed, 25 Nov 2015 11:50:43 -0800 Subject: Use the EndCurly token when creating the ReturnCmd for unifiedExit When there are more than one exit blocks, an unified exit block is created which includes a ReturnCmd. However, the ReturnCmd is created with NoToken. This causes the line/column number reported for a failed postcondition to be (0,0). The right token should be the EndCurly since the ReturnCmd is in the exit block. --- Source/VCGeneration/ConditionGeneration.cs | 6 +----- Test/test2/BadLineNumber.bpl | 15 +++++++++++++++ Test/test2/BadLineNumber.bpl.expect | 7 +++++++ 3 files changed, 23 insertions(+), 5 deletions(-) create mode 100644 Test/test2/BadLineNumber.bpl create mode 100644 Test/test2/BadLineNumber.bpl.expect diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 0e5fce82..043d0985 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1134,11 +1134,7 @@ namespace VC { if (returnBlocks > 1) { string unifiedExitLabel = "GeneratedUnifiedExit"; Block unifiedExit; - if (impl.StructuredStmts != null) { - unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), new ReturnCmd(impl.StructuredStmts.EndCurly)); - } else { - unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), new ReturnCmd(Token.NoToken)); - } + unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), 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) { 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 -- cgit v1.2.3 From c03c5ba246565fcb3b16630051c6235f06c4bef8 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 1 Dec 2015 17:01:22 +0000 Subject: Teach TravisCI to use Z3 4.4.1 from repositories that I'm currently maintaining on the OpenSUSE build service. See https://build.opensuse.org/package/show/home:delcypher:z3/z3 --- .travis.yml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/.travis.yml b/.travis.yml index 11ed4d64..41ee569f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -6,14 +6,15 @@ 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 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 - - sudo apt-get -y install z3=4.3.2-0~precise2 + # 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 && travis_retry nuget install NUnit.Runners -Version 2.6.3 -- cgit v1.2.3 From 75b5befa9f82f6fd54817d9cec20522af1a797a6 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 19 Nov 2015 18:23:03 -0600 Subject: Update test output for Z3 4.4.1. --- README.md | 2 +- Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect | 3 ++- Test/test15/CaptureState.bpl.expect | 18 +++++++++--------- 3 files changed, 12 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index a976b249..224d7196 100644 --- a/README.md +++ b/README.md @@ -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/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/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 -- cgit v1.2.3 From f97656456a74564cdf96633c3f46223d39e2c6f2 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Mon, 16 Nov 2015 11:03:28 -0800 Subject: Use the EndCurly token when creating the ReturnCmd for unifiedExit When there are more than one exit blocks, an unified exit block is created which includes a ReturnCmd. However, the ReturnCmd is created with NoToken. This causes the line/column number reported for a failed postcondition to be (0,0). The right token should be the EndCurly since the ReturnCmd is in the exit block. --- Source/VCGeneration/ConditionGeneration.cs | 3 ++- Test/test2/BadLineNumber.bpl | 15 +++++++++++++++ Test/test2/BadLineNumber.bpl.expect | 7 +++++++ 3 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 Test/test2/BadLineNumber.bpl create mode 100644 Test/test2/BadLineNumber.bpl.expect diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 6a2eec29..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(), new ReturnCmd(Token.NoToken)); + Block unifiedExit; + unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), 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) { 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 -- cgit v1.2.3 From 3e4a58021e7f9b2bd31dd195f9a7b2f02d5b4c02 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 2 Dec 2015 09:27:06 +0000 Subject: TravisCI build icon should only show build status for master branch, not all branches. --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 224d7196..1dd0ba5a 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ |-------------------------------|---------------------------------| | [![linux build status][1]][2] | [![windows_build_status][3]][4] | -[1]: https://travis-ci.org/boogie-org/boogie.svg +[1]: https://travis-ci.org/boogie-org/boogie.svg?branch=master [2]: https://travis-ci.org/boogie-org/boogie [3]: https://pmbuilds.inf.ethz.ch/buildStatus/icon?job=boogie [4]: #FIXME -- cgit v1.2.3 From 9b355c4e494bc6427e3d165288c09e113a86000a Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Wed, 2 Dec 2015 12:02:43 -0600 Subject: Remove workaround for older versions of Z3. --- Source/VCGeneration/Check.cs | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index da445a00..8c1ae407 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -356,16 +356,8 @@ namespace Microsoft.Boogie { hasOutput = false; outputExn = null; this.handler = handler; - - if (namedAssumeVars != null && namedAssumeVars.Any()) - { - // TODO(wuestholz): Avoid doing a full reset. This is currently necessary for old versions of Z3 due to a bug. - thmProver.FullReset(gen); - } - else - { - thmProver.Reset(gen); - } + + thmProver.Reset(gen); SetTimeout(); proverStart = DateTime.UtcNow; thmProver.NamedAssumeVars = namedAssumeVars; -- cgit v1.2.3 From 9f50f449bef2aeed660a8e3c0b5eb73ad7fe1e78 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 3 Dec 2015 09:37:45 -0600 Subject: Remove unused directory. --- Build/CodePlex.Tools.MsBuild.dll | Bin 131072 -> 0 bytes Build/CodePlex.Tools.Wiki.dll | Bin 45056 -> 0 bytes Build/updateVersionFile.xml | 19 ------------------- 3 files changed, 19 deletions(-) delete mode 100644 Build/CodePlex.Tools.MsBuild.dll delete mode 100644 Build/CodePlex.Tools.Wiki.dll delete mode 100644 Build/updateVersionFile.xml diff --git a/Build/CodePlex.Tools.MsBuild.dll b/Build/CodePlex.Tools.MsBuild.dll deleted file mode 100644 index 2e400e8e..00000000 Binary files a/Build/CodePlex.Tools.MsBuild.dll and /dev/null differ diff --git a/Build/CodePlex.Tools.Wiki.dll b/Build/CodePlex.Tools.Wiki.dll deleted file mode 100644 index 9ea2bea8..00000000 Binary files a/Build/CodePlex.Tools.Wiki.dll and /dev/null differ diff --git a/Build/updateVersionFile.xml b/Build/updateVersionFile.xml deleted file mode 100644 index cb083c7a..00000000 --- a/Build/updateVersionFile.xml +++ /dev/null @@ -1,19 +0,0 @@ - - - - - - - - - -- cgit v1.2.3 From 8938d00be93e780d54917c1448bc534702766fdf Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Thu, 3 Dec 2015 09:39:44 -0600 Subject: Remove unused file. --- Source/version.ssc | 12 ------------ 1 file changed, 12 deletions(-) delete mode 100644 Source/version.ssc 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")] - -- cgit v1.2.3 From 1c16dc829c81426e17427c0d103ed831a48f1f81 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Sun, 27 Dec 2015 15:08:38 -0600 Subject: Enable optimization for more prover queries. --- Source/Provers/SMTLib/ProverInterface.cs | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index ca530da2..b8fd2f50 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -421,13 +421,7 @@ namespace Microsoft.Boogie.SMTLib SendThisVC(vcString); - if (options.Solver == SolverKind.Z3 && 0 < OptimizationRequests.Count) - { - foreach (var r in OptimizationRequests) - { - SendThisVC(r); - } - } + SendOptimizationRequests(); FlushLogFile(); @@ -442,6 +436,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) @@ -2137,6 +2142,7 @@ namespace Microsoft.Boogie.SMTLib public override void Assert(VCExpr vc, bool polarity) { + OptimizationRequests.Clear(); string a = ""; if (polarity) { @@ -2148,6 +2154,7 @@ namespace Microsoft.Boogie.SMTLib } AssertAxioms(); SendThisVC(a); + SendOptimizationRequests(); } public override void DefineMacro(Macro f, VCExpr vc) { -- cgit v1.2.3 From dd8e69b7b71a9375b7206a70633deae234175ef8 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 28 Dec 2015 20:22:03 -0600 Subject: Improve precision of abstract interpreter for modulo operations. --- Source/AbsInt/IntervalDomain.cs | 4 ++++ Test/aitest0/Intervals.bpl | 15 +++++++++++++++ Test/aitest0/Intervals.bpl.expect | 2 +- 3 files changed, 20 insertions(+), 1 deletion(-) diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index ee9d632b..2fd37463 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -884,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/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 -- cgit v1.2.3 From 5d23ab3bf5bc80ee1bf5bbc6194a6de67264c61f Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 28 Dec 2015 20:28:04 -0600 Subject: Fix issue with ids for assume-statements. --- Source/Provers/SMTLib/ProverInterface.cs | 5 +++-- Source/Provers/SMTLib/TypeDeclCollector.cs | 5 ++++- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index b8fd2f50..7e98e8f8 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -411,10 +411,11 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(push 1)"); SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")"); - if (NamedAssumeVars != null) + 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)); } } @@ -1292,7 +1293,7 @@ namespace Microsoft.Boogie.SMTLib var reporter = handler as VC.VCGen.ErrorReporter; // TODO(wuestholz): Is the reporter ever null? - if (NamedAssumeVars != null && NamedAssumeVars.Any() && result == Outcome.Valid && reporter != null) + if (CommandLineOptions.Clo.PrintNecessaryAssumes && NamedAssumeVars != null && NamedAssumeVars.Any() && result == Outcome.Valid && reporter != null) { SendThisVC("(get-unsat-core)"); var resp = Process.GetProverResponse(); 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); -- cgit v1.2.3 From 2dafee57c84cd8d3bdccdba1bc348936a9548b94 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Tue, 29 Dec 2015 12:15:46 -0600 Subject: Minor change --- Source/VCGeneration/Wlp.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 741ed723..508a1400 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -193,7 +193,7 @@ namespace VC { var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr); var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id"); - if (aid != null && namedAssumeVars != null) + if (CommandLineOptions.Clo.PrintNecessaryAssumes && aid != null && namedAssumeVars != null) { var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool); namedAssumeVars.Add(v); -- cgit v1.2.3 From 24a49931e1c7d456008296e1255d8506d28cb18b Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Fri, 8 Jan 2016 11:36:11 -0800 Subject: added Free code --- Test/civl/alloc.bpl | 69 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 43 insertions(+), 26 deletions(-) diff --git a/Test/civl/alloc.bpl b/Test/civl/alloc.bpl index 33535b00..56515ba8 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(pool)[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 -- cgit v1.2.3 From 107dae2093c2049c674cb4a32cd01143765893b9 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sun, 10 Jan 2016 09:19:12 -0800 Subject: fixed a small problem in the precondition for FreeLinear --- Test/civl/alloc.bpl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/civl/alloc.bpl b/Test/civl/alloc.bpl index 56515ba8..68b7e6c6 100644 --- a/Test/civl/alloc.bpl +++ b/Test/civl/alloc.bpl @@ -127,7 +127,7 @@ 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(pool)[i]; +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); -- cgit v1.2.3 From f75e5ba707885666ead81d7c5ec1653e7a09f3ff Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sun, 17 Jan 2016 19:11:04 -0800 Subject: updated the example to implement the allocation of thread identifiers; this example provides another illustration of abstracting ordinary variables by linear variables --- Test/civl/Program4.bpl | 119 +++++++++++++++++++++++++++++++++--------- Test/civl/Program4.bpl.expect | 2 +- 2 files changed, 96 insertions(+), 25 deletions(-) diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl index 68c2a5f3..a6dfcb2a 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"} unallocated:[int]bool; -procedure {:yields} {:layer 1} main() { - var {:linear "tid"} tid:Tid; +procedure {:yields} {:layer 2} main() +requires {:layer 1} AllocInv(count, unallocated); +{ + 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, unallocated); + while (true) + invariant {:layer 1} AllocInv(count, unallocated); + { + call tid, i := Allocate(); + async call P(tid, i); yield; + assert {:layer 1} AllocInv(count, unallocated); } 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, unallocated); +ensures {:layer 1} AllocInv(count, unallocated); +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, unallocated); + 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, unallocated); + 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, unallocated); + 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, unallocated); +ensures {:layer 1} AllocInv(count, unallocated); +ensures {:layer 1} tid == i; +ensures {:atomic} +|{A: + return true; +}|; { yield; - call tid := AllocateLow(); + assert {:layer 1} AllocInv(count, unallocated); + call i := AllocateLow(); + call tid := MakeLinear(i); yield; + assert {:layer 1} AllocInv(count, unallocated); } -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, unallocated); +ensures {:layer 1} AllocInv(count, unallocated); ensures {:atomic} |{A: val := a[tid]; return true; }|; +{ + yield; + assert {:layer 1} AllocInv(count, unallocated); + call val := ReadLow(i); + yield; + assert {:layer 1} AllocInv(count, unallocated); +} -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, unallocated); +ensures {:layer 1} AllocInv(count, unallocated); ensures {:atomic} |{A: a[tid] := val; return true; }|; +{ + yield; + assert {:layer 1} AllocInv(count, unallocated); + call WriteLow(i, val); + yield; + assert {:layer 1} AllocInv(count, unallocated); +} -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid); -ensures {:atomic} |{ A: return true; }|; +function {:inline} AllocInv(count: int, unallocated:[int]bool): (bool) +{ + (forall x: int :: count <= x ==> unallocated[x]) +} + +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 unallocated[i]; +modifies unallocated; +ensures tid == i && unallocated == old(unallocated)[i := false]; -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 -- cgit v1.2.3 From c36b3d93a9c55dcb1d37d8b6ca09ae0b5114ec0b Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 19 Jan 2016 15:07:06 -0800 Subject: some fixes --- Test/civl/treiber-stack.bpl | 59 ++++++++++++++++++++++++++------------------- 1 file changed, 34 insertions(+), 25 deletions(-) diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl index 751ce861..bb0201a9 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 unique 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 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; @@ -82,13 +91,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); -- cgit v1.2.3 From 4d9ec68b4b038ff2e4fe91eec2e82b1d613ee3b0 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 21 Jan 2016 21:28:00 -0800 Subject: improved some of the annotations --- Test/civl/Program4.bpl | 54 ++++++++++++++++++++++----------------------- Test/civl/treiber-stack.bpl | 4 ++-- 2 files changed, 29 insertions(+), 29 deletions(-) diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl index a6dfcb2a..11ba8afa 100644 --- a/Test/civl/Program4.bpl +++ b/Test/civl/Program4.bpl @@ -2,51 +2,51 @@ // RUN: %diff "%s.expect" "%t" var {:layer 0,2} a:[int]int; var {:layer 0,1} count: int; -var {:layer 1,1} {:linear "tid"} unallocated:[int]bool; +var {:layer 1,1} {:linear "tid"} allocated:[int]bool; procedure {:yields} {:layer 2} main() -requires {:layer 1} AllocInv(count, unallocated); +requires {:layer 1} allocated == MapConstBool(false); { var {:layer 1} {:linear "tid"} tid:int; var i: int; yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); while (true) - invariant {:layer 1} AllocInv(count, unallocated); + invariant {:layer 1} AllocInv(count, allocated); { call tid, i := Allocate(); async call P(tid, i); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); } yield; } procedure {:yields} {:layer 2} P({:layer 1} {:linear "tid"} tid: int, i: int) requires {:layer 1} tid == i; -requires {:layer 1} AllocInv(count, unallocated); -ensures {:layer 1} AllocInv(count, unallocated); +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} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); assert {:layer 2} a[tid] == old(a)[tid]; call t := Read(tid, i); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); assert {:layer 2} a[tid] == t; call Write(tid, i, t + 1); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); assert {:layer 2} a[tid] == t + 1; } procedure {:yields} {:layer 1,2} Allocate() returns ({:layer 1} {:linear "tid"} tid: int, i: int) -requires {:layer 1} AllocInv(count, unallocated); -ensures {:layer 1} AllocInv(count, unallocated); +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); ensures {:layer 1} tid == i; ensures {:atomic} |{A: @@ -54,48 +54,48 @@ ensures {:atomic} }|; { yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); call i := AllocateLow(); call tid := MakeLinear(i); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); } 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, unallocated); -ensures {:layer 1} AllocInv(count, unallocated); +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, unallocated); + assert {:layer 1} AllocInv(count, allocated); call val := ReadLow(i); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); } 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, unallocated); -ensures {:layer 1} AllocInv(count, unallocated); +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, unallocated); + assert {:layer 1} AllocInv(count, allocated); call WriteLow(i, val); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); } -function {:inline} AllocInv(count: int, unallocated:[int]bool): (bool) +function {:inline} AllocInv(count: int, allocated:[int]bool): (bool) { - (forall x: int :: count <= x ==> unallocated[x]) + (forall x: int :: allocated[x] ==> x < count) } procedure {:yields} {:layer 0,1} ReadLow(i: int) returns (val: int); @@ -121,9 +121,9 @@ ensures {:atomic} // 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 unallocated[i]; -modifies unallocated; -ensures tid == i && unallocated == old(unallocated)[i := false]; +requires !allocated[i]; +modifies allocated; +ensures tid == i && allocated == old(allocated)[i := true]; function {:builtin "MapConst"} MapConstBool(bool): [int]bool; function {:builtin "MapOr"} MapOr([int]bool, [int]bool) : [int]bool; diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl index bb0201a9..64e01c99 100644 --- a/Test/civl/treiber-stack.bpl +++ b/Test/civl/treiber-stack.bpl @@ -1,7 +1,7 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" // RUN: %diff "%s.expect" "%t" -const unique null: int; +const null: int; type lmap; function {:linear "Node"} dom(lmap): [int]bool; function map(lmap): [int]int; @@ -17,7 +17,7 @@ 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:int); -ensures {:right} |{ A: assume dom(Stack)[v] || Used[v]; return true; }|; +ensures {:right} |{ A: assume v == null || dom(Stack)[v] || Used[v]; return true; }|; procedure {:yields} {:layer 0,1} Load(i:int) returns (v:int); ensures {:right} |{ A: assert dom(Stack)[i] || Used[i]; goto B,C; -- cgit v1.2.3 From 1e0f2b1ea7e9cbfd1c7923674c0ed4601263d09a Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 26 Jan 2016 10:11:24 -0800 Subject: another fix --- Test/civl/treiber-stack.bpl | 2 -- 1 file changed, 2 deletions(-) diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl index 64e01c99..a184886d 100644 --- a/Test/civl/treiber-stack.bpl +++ b/Test/civl/treiber-stack.bpl @@ -80,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; @@ -124,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]); -- cgit v1.2.3 From 5fb565e439255ede7dc3653708af41678b6c1062 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 9 Feb 2016 21:35:24 -0800 Subject: added an example --- Test/civl/funky.bpl | 133 +++++++++++++++++++++++++++++++++++++++++++++ Test/civl/funky.bpl.expect | 2 + Test/civl/ticket.bpl | 5 +- 3 files changed, 137 insertions(+), 3 deletions(-) create mode 100644 Test/civl/funky.bpl create mode 100644 Test/civl/funky.bpl.expect 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; }|; -- cgit v1.2.3