diff options
34 files changed, 375 insertions, 157 deletions
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index b10cd6cd..971e7271 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -30,52 +30,57 @@ namespace Microsoft.Boogie if (moverTypeChecker.procToActionInfo.Count == 0)
return;
+ List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo));
+ sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; });
+ List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo));
+ sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; });
+
Dictionary<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>();
- foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values)
+ int indexIntoSortedByCreatedLayerNum = 0;
+ int indexIntoSortedByAvailableUptoLayerNum = 0;
+ HashSet<AtomicActionInfo> currPool = new HashSet<AtomicActionInfo>();
+ while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count)
{
- AtomicActionInfo atomicAction = action as AtomicActionInfo;
- if (atomicAction == null) continue;
- foreach (int layerNum in moverTypeChecker.AllLayerNums)
+ var currLayerNum = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum].createdAtLayerNum;
+ pools[currLayerNum] = new HashSet<AtomicActionInfo>(currPool);
+ while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count)
{
- if (action.createdAtLayerNum < layerNum && layerNum <= action.availableUptoLayerNum)
- {
- if (!pools.ContainsKey(layerNum))
- {
- pools[layerNum] = new HashSet<AtomicActionInfo>();
- }
- pools[layerNum].Add(atomicAction);
- }
+ var actionInfo = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum] as AtomicActionInfo;
+ if (actionInfo.createdAtLayerNum > currLayerNum) break;
+ pools[currLayerNum].Add(actionInfo);
+ indexIntoSortedByCreatedLayerNum++;
}
+ while (indexIntoSortedByAvailableUptoLayerNum < sortedByAvailableUptoLayerNum.Count)
+ {
+ var actionInfo = sortedByAvailableUptoLayerNum[indexIntoSortedByAvailableUptoLayerNum] as AtomicActionInfo;
+ if (actionInfo.availableUptoLayerNum > currLayerNum) break;
+ pools[currLayerNum].Remove(actionInfo);
+ indexIntoSortedByAvailableUptoLayerNum++;
+ }
+ currPool = pools[currLayerNum];
}
Program program = moverTypeChecker.program;
MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls);
- foreach (int layerNum1 in pools.Keys)
+ foreach (int layerNum in pools.Keys)
{
- foreach (AtomicActionInfo first in pools[layerNum1])
+ foreach (AtomicActionInfo first in pools[layerNum])
{
Debug.Assert(first.moverType != MoverType.Top);
if (first.moverType == MoverType.Atomic)
continue;
- foreach (int layerNum2 in pools.Keys)
+ foreach (AtomicActionInfo second in pools[layerNum])
{
- if (layerNum2 < layerNum1) continue;
- foreach (AtomicActionInfo second in pools[layerNum2])
+ if (first.IsRightMover)
+ {
+ moverChecking.CreateCommutativityChecker(program, first, second);
+ moverChecking.CreateGatePreservationChecker(program, second, first);
+ }
+ if (first.IsLeftMover)
{
- if (second.createdAtLayerNum < layerNum1)
- {
- if (first.IsRightMover)
- {
- moverChecking.CreateCommutativityChecker(program, first, second);
- moverChecking.CreateGatePreservationChecker(program, second, first);
- }
- if (first.IsLeftMover)
- {
- moverChecking.CreateCommutativityChecker(program, second, first);
- moverChecking.CreateGatePreservationChecker(program, first, second);
- moverChecking.CreateFailurePreservationChecker(program, second, first);
- }
- }
+ moverChecking.CreateCommutativityChecker(program, second, first);
+ moverChecking.CreateGatePreservationChecker(program, first, second);
+ moverChecking.CreateFailurePreservationChecker(program, second, first);
}
}
}
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 8865b69e..dbd1dcbd 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -1160,7 +1160,7 @@ namespace Microsoft.Boogie public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
{
Program program = linearTypeChecker.program;
- foreach (int layerNum in moverTypeChecker.AllLayerNums.Except(new int[] { 0 }))
+ foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))
{
if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 8eb93e09..13356aff 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -22,12 +22,14 @@ namespace Microsoft.Boogie public Procedure proc;
public int createdAtLayerNum;
public int availableUptoLayerNum;
+ public bool hasImplementation;
public ActionInfo(Procedure proc, int createdAtLayerNum, int availableUptoLayerNum)
{
this.proc = proc;
this.createdAtLayerNum = createdAtLayerNum;
this.availableUptoLayerNum = availableUptoLayerNum;
+ this.hasImplementation = false;
}
public virtual bool IsRightMover
@@ -226,6 +228,7 @@ namespace Microsoft.Boogie int maxLayerNum;
public Dictionary<Absy, HashSet<int>> absyToLayerNums;
HashSet<Variable> auxVars;
+ public int leastUnimplementedLayerNum;
private static List<int> FindLayers(QKeyValue kv)
{
@@ -260,20 +263,58 @@ namespace Microsoft.Boogie return MoverType.Top;
}
- private HashSet<int> allLayerNums;
- public IEnumerable<int> AllLayerNums
+ public MoverTypeChecker(Program program)
+ {
+ this.auxVars = new HashSet<Variable>();
+ this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();
+ this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();
+ this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
+ this.errorCount = 0;
+ this.checkingContext = new CheckingContext(null);
+ this.program = program;
+ this.enclosingProc = null;
+ this.enclosingImpl = null;
+ this.canAccessSharedVars = false;
+ this.canAccessAuxVars = false;
+ this.minLayerNum = int.MaxValue;
+ this.maxLayerNum = -1;
+ this.leastUnimplementedLayerNum = int.MaxValue;
+ foreach (var g in program.GlobalVariables)
+ {
+ List<int> layerNums = FindLayers(g.Attributes);
+ if (layerNums.Count == 0)
+ {
+ // Cannot access atomic actions
+ }
+ else if (layerNums.Count == 1)
+ {
+ this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue);
+ }
+ else if (layerNums.Count == 2)
+ {
+ this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]);
+ }
+ else
+ {
+ Error(g, "Too many layer numbers");
+ }
+ }
+ }
+
+ private HashSet<int> allCreatedLayerNums;
+ public IEnumerable<int> AllCreatedLayerNums
{
get
{
- if (allLayerNums == null)
+ if (allCreatedLayerNums == null)
{
- allLayerNums = new HashSet<int>();
+ allCreatedLayerNums = new HashSet<int>();
foreach (ActionInfo actionInfo in procToActionInfo.Values)
{
- allLayerNums.Add(actionInfo.createdAtLayerNum);
+ allCreatedLayerNums.Add(actionInfo.createdAtLayerNum);
}
}
- return allLayerNums;
+ return allCreatedLayerNums;
}
}
@@ -300,6 +341,11 @@ namespace Microsoft.Boogie Error(proc, "Incorrect number of layers");
continue;
}
+ if (availableUptoLayerNum <= createdAtLayerNum)
+ {
+ Error(proc, "Creation layer number must be less than the available upto layer number");
+ continue;
+ }
foreach (Ensures e in proc.Ensures)
{
MoverType moverType = GetMoverType(e);
@@ -323,68 +369,69 @@ namespace Microsoft.Boogie enclosingImpl = null;
base.VisitEnsures(e);
canAccessSharedVars = false;
- if (maxLayerNum <= createdAtLayerNum && availableUptoLayerNum <= minLayerNum)
+ if (maxLayerNum > createdAtLayerNum)
{
- // ok
+ Error(e, "A variable being accessed is introduced after this action is created");
}
- else
+ else if (availableUptoLayerNum > minLayerNum)
{
Error(e, "A variable being accessed is hidden before this action becomes unavailable");
}
-
- procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum);
+ else
+ {
+ procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum);
+ }
}
+ if (errorCount > 0) continue;
if (!procToActionInfo.ContainsKey(proc))
{
procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum);
}
}
if (errorCount > 0) return;
- this.VisitProgram(program);
- if (errorCount > 0) return;
- YieldTypeChecker.PerformYieldSafeCheck(this);
- }
-
- public IEnumerable<Variable> SharedVariables
- {
- get { return this.globalVarToSharedVarInfo.Keys; }
- }
-
- public MoverTypeChecker(Program program)
- {
- this.auxVars = new HashSet<Variable>();
- this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();
- this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();
- this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
- this.errorCount = 0;
- this.checkingContext = new CheckingContext(null);
- this.program = program;
- this.enclosingProc = null;
- this.enclosingImpl = null;
- this.canAccessSharedVars = false;
- this.canAccessAuxVars = false;
- this.minLayerNum = int.MaxValue;
- this.maxLayerNum = -1;
- foreach (var g in program.GlobalVariables)
+ foreach (var impl in program.Implementations)
{
- List<int> layerNums = FindLayers(g.Attributes);
- if (layerNums.Count == 0)
+ if (!procToActionInfo.ContainsKey(impl.Proc)) continue;
+ procToActionInfo[impl.Proc].hasImplementation = true;
+ }
+ foreach (var proc in procToActionInfo.Keys)
+ {
+ ActionInfo actionInfo = procToActionInfo[proc];
+ if (actionInfo.hasImplementation) continue;
+ if (leastUnimplementedLayerNum == int.MaxValue)
{
- // Cannot access atomic actions
+ leastUnimplementedLayerNum = actionInfo.createdAtLayerNum;
}
- else if (layerNums.Count == 1)
+ else if (leastUnimplementedLayerNum == actionInfo.createdAtLayerNum)
{
- this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue);
+ // do nothing
}
- else if (layerNums.Count == 2)
+ else
{
- this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]);
+ Error(proc, "All unimplemented atomic actions must be created at the same layer");
}
- else
+ }
+ foreach (var g in this.globalVarToSharedVarInfo.Keys)
+ {
+ var info = globalVarToSharedVarInfo[g];
+ if (!this.AllCreatedLayerNums.Contains(info.introLayerNum))
{
- Error(g, "Too many layer numbers");
+ Error(g, "Variable must be introduced with creation of some atomic action");
+ }
+ if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum))
+ {
+ Error(g, "Variable must be hidden with creation of some atomic action");
}
}
+ if (errorCount > 0) return;
+ this.VisitProgram(program);
+ if (errorCount > 0) return;
+ YieldTypeChecker.PerformYieldSafeCheck(this);
+ }
+
+ public IEnumerable<Variable> SharedVariables
+ {
+ get { return this.globalVarToSharedVarInfo.Keys; }
}
public override Implementation VisitImplementation(Implementation node)
@@ -602,7 +649,11 @@ namespace Microsoft.Boogie absyToLayerNums[node] = new HashSet<int>();
foreach (int layerNum in attrs)
{
- if (layerNum > enclosingProcLayerNum)
+ if (layerNum == leastUnimplementedLayerNum || !AllCreatedLayerNums.Contains(layerNum))
+ {
+ Error(node, "Illegal layer number");
+ }
+ else if (layerNum > enclosingProcLayerNum)
{
Error(node, "The layer cannot be greater than the layer of enclosing procedure");
}
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 8e844ede..95884626 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -136,12 +136,12 @@ namespace Microsoft.Boogie {
foreach (var impl in moverTypeChecker.program.Implementations)
{
- if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum == 0) continue;
+ if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue;
impl.PruneUnreachableBlocks();
Graph<Block> implGraph = Program.GraphFromImpl(impl);
implGraph.ComputeLoops();
int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;
- foreach (int layerNum in moverTypeChecker.AllLayerNums)
+ foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))
{
if (layerNum > specLayerNum) continue;
YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers);
diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl index b204d9de..f439b607 100644 --- a/Test/og/DeviceCache.bpl +++ b/Test/og/DeviceCache.bpl @@ -48,8 +48,13 @@ ensures {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old( assert {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;
}
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X);
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X)
ensures {:layer 1} xl != nil;
+{
+ yield;
+ call xl := AllocateLow();
+ yield;
+}
procedure {:yields} {:layer 1} main({:linear_in "tid"} xls: [X]bool)
requires {:layer 1} xls == mapconstbool(true);
@@ -200,3 +205,6 @@ ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; retur procedure {:yields} {:layer 0,1} release({:linear "tid"} tid: X);
ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|;
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assume tid != nil; return true; }|;
diff --git a/Test/og/DeviceCache.bpl.expect b/Test/og/DeviceCache.bpl.expect index 8c696418..9ec7a92d 100644 --- a/Test/og/DeviceCache.bpl.expect +++ b/Test/og/DeviceCache.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 29 verified, 0 errors
+Boogie program verifier finished with 30 verified, 0 errors
diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl index a912a89a..7345b5b2 100644 --- a/Test/og/FlanaganQadeer.bpl +++ b/Test/og/FlanaganQadeer.bpl @@ -11,8 +11,13 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool MapConstBool(false)[x := true]
}
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X);
-ensures {:layer 1} xls != nil;
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X)
+ensures {:layer 1} xl != nil;
+{
+ yield;
+ call xl := AllocateLow();
+ yield;
+}
procedure {:yields} {:layer 1} main()
{
@@ -38,6 +43,9 @@ ensures {:atomic} |{A: l := nil; return true; }|; procedure {:yields} {:layer 0,1} Set(val: int);
ensures {:atomic} |{A: x := val; return true; }|;
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xl: X);
+ensures {:atomic} |{ A: assume xl != nil; return true; }|;
+
procedure {:yields} {:layer 1} foo({:linear_in "tid"} tid': X, val: int)
requires {:layer 1} tid' != nil;
{
diff --git a/Test/og/FlanaganQadeer.bpl.expect b/Test/og/FlanaganQadeer.bpl.expect index 5b2909f1..fef5ddc0 100644 --- a/Test/og/FlanaganQadeer.bpl.expect +++ b/Test/og/FlanaganQadeer.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl index b8406f2e..7767e179 100644 --- a/Test/og/Program4.bpl +++ b/Test/og/Program4.bpl @@ -15,7 +15,12 @@ function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool var {:layer 0,1} a:[Tid]int;
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid:Tid);
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid)
+{
+ yield;
+ call tid := AllocateLow();
+ yield;
+}
procedure {:yields} {:layer 1} main() {
var {:linear "tid"} tid:Tid;
@@ -55,3 +60,6 @@ ensures {:atomic} |{A:
a[tid] := val; return true;
}|;
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid);
+ensures {:atomic} |{ A: return true; }|;
diff --git a/Test/og/Program4.bpl.expect b/Test/og/Program4.bpl.expect index 3de74d3e..5b2909f1 100644 --- a/Test/og/Program4.bpl.expect +++ b/Test/og/Program4.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/og/Program5.bpl b/Test/og/Program5.bpl index af87eac5..55e4219f 100644 --- a/Test/og/Program5.bpl +++ b/Test/og/Program5.bpl @@ -5,8 +5,8 @@ const unique nil: Tid; function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;
function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;
-var {:layer 0,3} Color:int;
-var {:layer 0,3} lock:Tid;
+var {:layer 0} Color:int;
+var {:layer 0} lock:Tid;
function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
{
@@ -72,6 +72,6 @@ procedure {:yields} {:layer 0,1} SetColorLocked({:linear "tid"} tid:Tid, newCol: procedure {:yields} {:layer 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns (col:int);
ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|;
-procedure {:yields} {:layer 1,2} GetColorNoLock() returns (col:int);
+procedure {:yields} {:layer 0,2} GetColorNoLock() returns (col:int);
ensures {:atomic} |{A: col := Color; return true;}|;
diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl index cfbeaf3a..c826b810 100644 --- a/Test/og/akash.bpl +++ b/Test/og/akash.bpl @@ -18,15 +18,6 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool x
}
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int);
-ensures {:layer 1} xls != 0;
-
-procedure {:yields} {:layer 1} Allocate_1() returns ({:linear "1"} xls: [int]bool);
-ensures {:layer 1} xls == mapconstbool(true);
-
-procedure {:yields} {:layer 1} Allocate_2() returns ({:linear "2"} xls: [int]bool);
-ensures {:layer 1} xls == mapconstbool(true);
-
var {:layer 0,1} g: int;
var {:layer 0,1} h: int;
@@ -36,14 +27,23 @@ ensures {:atomic} |{A: g := val; return true; }|; procedure {:yields} {:layer 0,1} SetH(val:int);
ensures {:atomic} |{A: h := val; return true; }|;
-procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int)
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int)
+ensures {:layer 1} xl != 0;
+{
+ yield;
+ call xl := AllocateLow();
+ yield;
+}
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int);
+ensures {:atomic} |{ A: assume xls != 0; return true; }|;
+
+procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int)
+requires {:layer 1} x == mapconstbool(true);
+requires {:layer 1} y == mapconstbool(true);
{
- var {:linear "1"} x: [int]bool;
- var {:linear "2"} y: [int]bool;
var {:linear "tid"} tid_child: int;
tid_out := tid_in;
- call x := Allocate_1();
- call y := Allocate_2();
yield;
call SetG(0);
diff --git a/Test/og/akash.bpl.expect b/Test/og/akash.bpl.expect index 5b2909f1..fef5ddc0 100644 --- a/Test/og/akash.bpl.expect +++ b/Test/og/akash.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/chris.bpl b/Test/og/chris.bpl new file mode 100644 index 00000000..b54292ef --- /dev/null +++ b/Test/og/chris.bpl @@ -0,0 +1,28 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var{:layer 1} x:int;
+
+procedure{:yields}{:layer 2} Havoc()
+ ensures{:atomic} |{ A: return true; }|;
+{
+ yield;
+}
+
+procedure{:yields}{:layer 1} Recover()
+ ensures{:atomic} |{ A: assert x == 5; return true; }|;
+{
+ yield;
+}
+
+procedure{:yields}{:layer 3} P()
+ ensures{:atomic} |{ A: return true; }|;
+ requires{:layer 2,3} x == 5;
+ ensures {:layer 2,3} x == 5;
+{
+
+ yield; assert{:layer 2,3} x == 5;
+ call Havoc();
+ yield; assert{:layer 3} x == 5;
+ call Recover();
+ yield; assert{:layer 2,3} x == 5;
+}
diff --git a/Test/og/chris.bpl.expect b/Test/og/chris.bpl.expect new file mode 100644 index 00000000..be6b95ba --- /dev/null +++ b/Test/og/chris.bpl.expect @@ -0,0 +1,2 @@ +
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/og/chris2.bpl b/Test/og/chris2.bpl new file mode 100644 index 00000000..73f112ed --- /dev/null +++ b/Test/og/chris2.bpl @@ -0,0 +1,34 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var{:layer 20} x:int;
+
+procedure{:yields}{:layer 20,25} p_gt1_lower();
+ ensures{:both}
+ |{
+ A:
+ x := x + 1;
+ return true;
+ }|;
+
+procedure{:yields}{:layer 25,40} p_gt1()
+ ensures{:both}
+ |{
+ A:
+ x := x + 1;
+ return true;
+ }|;
+{
+ yield;
+ call p_gt1_lower();
+ yield;
+}
+
+procedure{:yields}{:layer 20,40} p_gt2();
+ ensures{:both}
+ |{
+ A:
+ assert x == 0;
+ return true;
+ }|;
+
+
diff --git a/Test/og/chris2.bpl.expect b/Test/og/chris2.bpl.expect new file mode 100644 index 00000000..2bf339f7 --- /dev/null +++ b/Test/og/chris2.bpl.expect @@ -0,0 +1,18 @@ +(0,0): Error BP5003: A postcondition might not hold on this return path.
+chris2.bpl(30,5): Related location: Gate not preserved by p_gt1_lower
+Execution trace:
+ (0,0): this_A
+(0,0): Error BP5003: A postcondition might not hold on this return path.
+(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1_lower
+Execution trace:
+ (0,0): this_A
+(0,0): Error BP5003: A postcondition might not hold on this return path.
+chris2.bpl(30,5): Related location: Gate not preserved by p_gt1
+Execution trace:
+ (0,0): this_A
+(0,0): Error BP5003: A postcondition might not hold on this return path.
+(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1
+Execution trace:
+ (0,0): this_A
+
+Boogie program verifier finished with 1 verified, 4 errors
diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl index 8752d402..e481291a 100644 --- a/Test/og/linear-set.bpl +++ b/Test/og/linear-set.bpl @@ -23,10 +23,21 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool var {:layer 0,1} x: int;
var {:layer 0,1} l: [X]bool;
-procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
+
+procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool)
ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
+{
+ yield;
+ call xls1, xls2 := SplitLow(xls);
+ yield;
+}
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: [X]bool);
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: [X]bool)
+{
+ yield;
+ call xls := AllocateLow();
+ yield;
+}
procedure {:yields} {:layer 0,1} Set(v: int);
ensures {:atomic} |{A: x := v; return true; }|;
@@ -37,6 +48,11 @@ ensures {:atomic} |{A: assume l == None(); l := tidls; return true; }|; procedure {:yields} {:layer 0,1} Unlock();
ensures {:atomic} |{A: l := None(); return true; }|;
+procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
+ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|;
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: [X]bool);
+ensures {:atomic} |{ A: return true; }|;
procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool)
requires {:layer 1} tidls' != None() && xls' == All();
diff --git a/Test/og/linear-set.bpl.expect b/Test/og/linear-set.bpl.expect index 3de74d3e..fef5ddc0 100644 --- a/Test/og/linear-set.bpl.expect +++ b/Test/og/linear-set.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl index a3b84702..24d8a13a 100644 --- a/Test/og/linear-set2.bpl +++ b/Test/og/linear-set2.bpl @@ -24,11 +24,21 @@ var {:layer 0,1} x: int; var {:layer 0,1} l: X;
const nil: X;
-procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
+procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool)
ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
+{
+ yield;
+ call xls1, xls2 := SplitLow(xls);
+ yield;
+}
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X);
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X)
ensures {:layer 1} xls != nil;
+{
+ yield;
+ call xls := AllocateLow();
+ yield;
+}
procedure {:yields} {:layer 0,1} Set(v: int);
ensures {:atomic} |{A: x := v; return true; }|;
@@ -39,6 +49,12 @@ ensures {:atomic} |{A: assume l == nil; l := tidls; return true; }|; procedure {:yields} {:layer 0,1} Unlock();
ensures {:atomic} |{A: l := nil; return true; }|;
+procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
+ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|;
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: X);
+ensures {:atomic} |{ A: assume xls != nil; return true; }|;
+
procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool)
requires {:layer 1} tidls' != nil && xls' == All();
{
diff --git a/Test/og/linear-set2.bpl.expect b/Test/og/linear-set2.bpl.expect index 3de74d3e..fef5ddc0 100644 --- a/Test/og/linear-set2.bpl.expect +++ b/Test/og/linear-set2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors
+Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl index 308e4b8b..7fb0a081 100644 --- a/Test/og/multiset.bpl +++ b/Test/og/multiset.bpl @@ -63,7 +63,7 @@ ensures {:both} |{ A: }|;
-procedure {:yields} {:layer 0} setEltToNull(j : int, {:linear "tid"} tid: X);
+procedure {:yields} {:layer 0,2} setEltToNull(j : int, {:linear "tid"} tid: X);
ensures {:left} |{ A:
assert owner[j] == tid;
assert 0 <= j && j < max;
@@ -75,7 +75,7 @@ ensures {:left} |{ A: return true;
}|;
-procedure {:yields} {:layer 0} setValid(j : int, {:linear "tid"} tid: X);
+procedure {:yields} {:layer 0,2} setValid(j : int, {:linear "tid"} tid: X);
ensures {:both} |{ A:
assert 0 <= j && j < max;
assert lock[j] == tid;
@@ -86,7 +86,7 @@ ensures {:both} |{ A: return true;
}|;
-procedure {:yields} {:layer 0} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool);
+procedure {:yields} {:layer 0,2} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool);
ensures {:both} |{ A:
assert 0 <= j && j < max;
assert lock[j] == tid;
@@ -95,7 +95,7 @@ ensures {:both} |{ A: return true;
}|;
-procedure {:yields} {:layer 1} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int)
+procedure {:yields} {:layer 1,2} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int)
requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done;
ensures {:layer 1} Inv(valid, elt, owner);
ensures {:right} |{ A: assert tid != nil && tid != done;
diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl index 74b738d6..b80b6315 100644 --- a/Test/og/new1.bpl +++ b/Test/og/new1.bpl @@ -9,10 +9,6 @@ function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool x
}
-procedure {:yields} {:layer 1} Allocate_Perm({:linear_in "Perm"} Permissions: [int]bool) returns ({:linear "Perm"} xls: [int]bool);
-requires {:layer 1} Permissions == mapconstbool(true);
-ensures {:layer 1} xls == mapconstbool(true);
-
procedure {:yields} {:layer 1} PB({:linear_in "Perm"} permVar_in:[int]bool)
requires {:layer 1} permVar_in[0] && g == 0;
{
@@ -31,14 +27,11 @@ requires {:layer 1} permVar_in[0] && g == 0; }
procedure {:yields} {:layer 1} Main({:linear_in "Perm"} Permissions: [int]bool)
-requires {:layer 0,1} Permissions == mapconstbool(true);
+requires {:layer 1} Permissions == mapconstbool(true);
{
- var {:linear "Perm"} permVar_out: [int]bool;
-
- call permVar_out := Allocate_Perm(Permissions);
yield;
call SetG(0);
- async call PB(permVar_out);
+ async call PB(Permissions);
yield;
}
diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl index ad40ffa0..c28edf2b 100644 --- a/Test/og/parallel2.bpl +++ b/Test/og/parallel2.bpl @@ -8,7 +8,12 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool MapConstBool(false)[x := true]
}
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int);
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int)
+{
+ yield;
+ call tid := AllocateLow();
+ yield;
+}
procedure {:yields} {:layer 0,1} Write(idx: int, val: int);
ensures {:atomic} |{A: a[idx] := val; return true; }|;
@@ -48,4 +53,7 @@ ensures {:layer 1} old(a)[i] == a[i]; {
yield;
assert {:layer 1} old(a)[i] == a[i];
-}
\ No newline at end of file +}
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int);
+ensures {:atomic} |{ A: return true; }|;
diff --git a/Test/og/parallel2.bpl.expect b/Test/og/parallel2.bpl.expect index fef5ddc0..05d394c7 100644 --- a/Test/og/parallel2.bpl.expect +++ b/Test/og/parallel2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl index 5340c4c8..f06ff4b8 100644 --- a/Test/og/parallel4.bpl +++ b/Test/og/parallel4.bpl @@ -2,7 +2,12 @@ // RUN: %diff "%s.expect" "%t"
var {:layer 0,1} a:int;
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int);
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int)
+{
+ yield;
+ call tid := AllocateLow();
+ yield;
+}
function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
@@ -35,3 +40,6 @@ procedure {:yields} {:layer 1} Yield() {
yield;
}
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int);
+ensures {:atomic} |{ A: return true; }|;
diff --git a/Test/og/parallel4.bpl.expect b/Test/og/parallel4.bpl.expect index 0bef8d9e..eaead450 100644 --- a/Test/og/parallel4.bpl.expect +++ b/Test/og/parallel4.bpl.expect @@ -1,6 +1,6 @@ -parallel4.bpl(26,3): Error BP5001: This assertion might not hold.
+parallel4.bpl(31,3): Error BP5001: This assertion might not hold.
Execution trace:
(0,0): og_init
(0,0): anon01
-Boogie program verifier finished with 2 verified, 1 error
+Boogie program verifier finished with 3 verified, 1 error
diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl index ea35a3b2..87afc888 100644 --- a/Test/og/parallel5.bpl +++ b/Test/og/parallel5.bpl @@ -2,7 +2,12 @@ // RUN: %diff "%s.expect" "%t"
var {:layer 0,1} a:[int]int;
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int);
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int)
+{
+ yield;
+ call tid := AllocateLow();
+ yield;
+}
function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
@@ -48,4 +53,7 @@ ensures {:layer 1} old(a)[i] == a[i]; {
yield;
assert {:layer 1} old(a)[i] == a[i];
-}
\ No newline at end of file +}
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int);
+ensures {:atomic} |{ A: return true; }|;
diff --git a/Test/og/parallel5.bpl.expect b/Test/og/parallel5.bpl.expect index fef5ddc0..05d394c7 100644 --- a/Test/og/parallel5.bpl.expect +++ b/Test/og/parallel5.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl index cb3dd138..675b3842 100644 --- a/Test/og/t1.bpl +++ b/Test/og/t1.bpl @@ -18,15 +18,6 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool x
}
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int);
-ensures {:layer 1} xls != 0;
-
-procedure {:yields} {:layer 1} Allocate_1() returns ({:linear "1"} xls: [int]bool);
-ensures {:layer 1} xls == mapconstbool(true);
-
-procedure {:yields} {:layer 1} Allocate_2() returns ({:linear "2"} xls: [int]bool);
-ensures {:layer 1} xls == mapconstbool(true);
-
var {:layer 0,1} g: int;
var {:layer 0,1} h: int;
@@ -44,14 +35,23 @@ ensures {:layer 1} x == mapconstbool(true) && g == 0; assert {:layer 1} x == mapconstbool(true) && g == 0;
}
-procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int)
+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int)
+ensures {:layer 1} xl != 0;
+{
+ yield;
+ call xl := AllocateLow();
+ yield;
+}
+
+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int);
+ensures {:atomic} |{ A: assume xls != 0; return true; }|;
+
+procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int)
+requires {:layer 1} x == mapconstbool(true);
+requires {:layer 1} y == mapconstbool(true);
{
- var {:linear "1"} x: [int]bool;
- var {:linear "2"} y: [int]bool;
var {:linear "tid"} tid_child: int;
tid_out := tid_in;
- call x := Allocate_1();
- call y := Allocate_2();
yield;
call SetG(0);
diff --git a/Test/og/t1.bpl.expect b/Test/og/t1.bpl.expect index 41fb28d9..f0195727 100644 --- a/Test/og/t1.bpl.expect +++ b/Test/og/t1.bpl.expect @@ -4,7 +4,7 @@ Execution trace: t1.bpl(84,13): anon0
(0,0): anon05
(0,0): inline$SetG_1$0$Entry
- t1.bpl(34,21): inline$SetG_1$0$this_A
+ t1.bpl(25,21): inline$SetG_1$0$this_A
(0,0): inline$Impl_YieldChecker_A_1$0$L1
-Boogie program verifier finished with 3 verified, 1 error
+Boogie program verifier finished with 4 verified, 1 error
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl index 68e308d0..91863e1a 100644 --- a/Test/og/ticket.bpl +++ b/Test/og/ticket.bpl @@ -33,8 +33,13 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool) if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket)
}
-procedure {:yields} {:layer 2} Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
+procedure {:yields} {:layer 2} Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X)
ensures {:layer 1} {:layer 2} xl != nil;
+{
+ yield;
+ call xls, xl := AllocateLow(xls');
+ yield;
+}
procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)
requires {:layer 2} xls' == mapconstbool(true);
@@ -138,3 +143,5 @@ ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|; procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X);
ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|;
+procedure {:yields} {:layer 0,2} AllocateLow({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
+ensures {:atomic} |{ A: assume xl != nil; return true; }|;
diff --git a/Test/og/ticket.bpl.expect b/Test/og/ticket.bpl.expect index f7c1129d..28c26eab 100644 --- a/Test/og/ticket.bpl.expect +++ b/Test/og/ticket.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 14 verified, 0 errors
+Boogie program verifier finished with 16 verified, 0 errors
diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl index 9a612eb2..8622dd9e 100644 --- a/Test/og/treiber-stack.bpl +++ b/Test/og/treiber-stack.bpl @@ -16,24 +16,24 @@ axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true] 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));
-procedure {:yields} {:layer 0} ReadTopOfStack() returns (v:Node);
+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} Load(i:Node) returns (v:Node);
+procedure {:yields} {:layer 0,1} Load(i:Node) returns (v:Node);
ensures {:right} |{ A: assert dom(Stack)[i] || dom(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} 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:Node, v:Node) 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} 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: Node, newVal: Node, {: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} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);
+procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: Node, newVal: Node) 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;
C: assume oldVal != TopOfStack; r := false; return true; }|;
|