From 5927744da636063556118f469cc8f9354b1cabe6 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Fri, 25 Sep 2015 12:05:19 -0700 Subject: added introduced and ghost local variables --- Test/civl/wsq.bpl | 106 +++++++++++++++++++++++------------------------------- 1 file changed, 45 insertions(+), 61 deletions(-) (limited to 'Test/civl/wsq.bpl') diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl index 17f53401..39dad919 100644 --- a/Test/civl/wsq.bpl +++ b/Test/civl/wsq.bpl @@ -89,13 +89,11 @@ 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} oldH:int; - var {:ghost} oldT:int; - var {:ghost} oldStatusT:bool; + var {:ghost} {:layer 3} oldH:int; + var {:ghost} {:layer 3} oldT:int; + var {:ghost} {:layer 3} oldStatusT:bool; - - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; assert {:layer 3} {:expand} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -104,8 +102,7 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I call t := readT_put(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && put_in_cs; assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -115,9 +112,8 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I call writeItems_put(tid,t, task); - oldH := H; - oldT := T; - oldStatusT := status[T]; + call oldH, oldT := GhostRead(); + call oldStatusT := GhostReadStatus(); yield; assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && t == T && tid == ptTid && !take_in_cs && put_in_cs; assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -128,8 +124,7 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I call writeT_put(tid, t+1); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -147,11 +142,10 @@ 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} oldH:int; - var {:ghost} oldT:int; + var {:ghost} {:layer 3} oldH:int; + var {:ghost} {:layer 3} oldT:int; - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -164,8 +158,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); { - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -173,8 +166,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call t := readT_take_init(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -185,8 +177,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu t := t-1; call writeT_take(tid, t); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !take_in_cs && !put_in_cs && t_ss[tid] == t; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -196,8 +187,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call h := readH_take(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && !put_in_cs && h_ss[tid] == h && t_ss[tid] == t; assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -214,8 +204,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call writeT_take_abort(tid, h); task := EMPTY; - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} h <= H; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; @@ -227,8 +216,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call task, taskstatus := readItems(tid, t); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} H >= h; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && h_ss[tid] == h && t_ss[tid] == t; @@ -240,8 +228,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu if(t>h) { call takeExitCS(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && h_ss[tid] == h && t_ss[tid] == t; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -250,8 +237,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu return; } call writeT_take_eq(tid, h+1); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; @@ -265,8 +251,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call chk := CAS_H_take(tid, h,h+1); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == oldH -1 && task != EMPTY); assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; @@ -279,8 +264,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu if(!chk) { - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -290,8 +274,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu goto LOOP_ENTRY_1; } - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -301,8 +284,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu return; } - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !put_in_cs; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -322,11 +304,10 @@ 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} oldH:int; - var {:ghost} oldT:int; + var {:ghost} {:layer 3} oldH:int; + var {:ghost} {:layer 3} oldT:int; - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} stealerTid(tid); assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); @@ -341,8 +322,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); invariant {:layer 3} !steal_in_cs[tid]; { - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} stealerTid(tid); assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); @@ -352,8 +332,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call h := readH_steal(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} H >= h; assert {:layer 3} !steal_in_cs[tid]; @@ -365,8 +344,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call t := readT_steal(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} steal_in_cs[tid]; assert {:layer 3} stealerTid(tid) && H >= h && steal_in_cs[tid] && h_ss[tid] == h; @@ -381,8 +359,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu task := EMPTY; call stealExitCS(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} !steal_in_cs[tid]; assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid] && h_ss[tid] == h; @@ -395,8 +372,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call task, taskstatus := readItems(tid, h); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} stealerTid(tid) && steal_in_cs[tid] && h_ss[tid] == h; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); @@ -408,8 +384,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call chk := CAS_H_steal(tid, h,h+1); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} h_ss[tid] == h; assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == h && task != EMPTY && taskstatus == IN_Q); @@ -423,8 +398,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu goto LOOP_ENTRY_2; } - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); @@ -433,14 +407,24 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu return; } - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} chk && task != EMPTY; assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; assert {:layer 3} oldH <= H; } +procedure {:layer 3} {:inline 1} GhostRead() returns (oldH: int, oldT: int) +{ + oldH := H; + oldT := T; +} + +procedure {:layer 3} {:inline 1} GhostReadStatus() returns (oldStatus: bool) +{ + oldStatus := status[T]; +} + procedure {:yields}{:layer 0,3} readH_take({:linear "tid"} tid:Tid) returns (y: int); ensures {:atomic} |{A: assert tid == ptTid; y := H; -- cgit v1.2.3 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 (limited to 'Test/civl/wsq.bpl') 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