diff options
| -rw-r--r-- | Source/Core/LinearSets.cs | 10 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 41 | ||||
| -rw-r--r-- | Test/linear/Maps.bpl | 24 | ||||
| -rw-r--r-- | Test/linear/list.bpl | 39 | ||||
| -rw-r--r-- | Test/linear/runtest.bat | 11 | ||||
| -rw-r--r-- | Test/og/Maps.bpl | 24 | ||||
| -rw-r--r-- | Test/og/bar.bpl | 29 | ||||
| -rw-r--r-- | Test/og/foo.bpl | 30 | ||||
| -rw-r--r-- | Test/og/linear-set.bpl | 68 | ||||
| -rw-r--r-- | Test/og/linear-set2.bpl | 69 | ||||
| -rw-r--r-- | Test/og/runtest.bat | 17 |
11 files changed, 341 insertions, 21 deletions
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index ffbd4e31..4edbfeed 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -480,11 +480,15 @@ namespace Microsoft.Boogie lhsVars.Add(v);
domainNames.Add(varToDomainName[v]);
}
- foreach (Variable v in lhsVars.Except(rhsVars))
+ foreach (Variable v in lhsVars.Union(rhsVars))
{
Drain(newCmds, v, varToDomainName[v]);
}
newCmds.Add(callCmd);
+ foreach (string domainName in domainNames)
+ {
+ newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ }
IdentifierExprSeq havocExprs = new IdentifierExprSeq();
foreach (Variable v in rhsVars.Except(lhsVars))
{
@@ -494,10 +498,6 @@ namespace Microsoft.Boogie {
TransformHavocCmd(newCmds, new HavocCmd(Token.NoToken, havocExprs), copies, domainNameToScope);
}
- foreach (string domainName in domainNames)
- {
- newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName])));
- }
}
void TransformAssignCmd(CmdSeq newCmds, AssignCmd assignCmd, Dictionary<Variable, LocalVariable> copies, Dictionary<string, HashSet<Variable>> domainNameToScope)
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index 5991a400..6eaf9650 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -151,7 +151,7 @@ namespace Microsoft.Boogie {
Dictionary<string, ProcedureInfo> procNameToInfo;
IdentifierExprSeq globalMods;
- Hashtable globalMap;
+ Hashtable ogOldGlobalMap;
Program program;
public OwickiGriesTransform(Program program)
@@ -159,15 +159,15 @@ namespace Microsoft.Boogie this.program = program;
procNameToInfo = AsyncAndYieldTraverser.Traverse(program);
AtomicTraverser.Traverse(program, procNameToInfo);
- globalMap = new Hashtable();
+ ogOldGlobalMap = new Hashtable();
globalMods = new IdentifierExprSeq();
bool workTodo = procNameToInfo.Values.Aggregate<ProcedureInfo, bool>(false, (b, info) => (b || !info.isAtomic || info.isThreadStart));
if (workTodo)
{
foreach (Variable g in program.GlobalVariables())
{
- var oldg = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_old_{0}", g.Name), g.TypedIdent.Type));
- globalMap[g] = new IdentifierExpr(Token.NoToken, oldg);
+ var oldg = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og@global_old_{0}", g.Name), g.TypedIdent.Type));
+ ogOldGlobalMap[g] = new IdentifierExpr(Token.NoToken, oldg);
globalMods.Add(new IdentifierExpr(Token.NoToken, g));
}
}
@@ -190,9 +190,9 @@ namespace Microsoft.Boogie {
List<AssignLhs> lhss = new List<AssignLhs>();
List<Expr> rhss = new List<Expr>();
- foreach (Variable g in globalMap.Keys)
+ foreach (Variable g in ogOldGlobalMap.Keys)
{
- lhss.Add(new SimpleAssignLhs(Token.NoToken, (IdentifierExpr)globalMap[g]));
+ lhss.Add(new SimpleAssignLhs(Token.NoToken, (IdentifierExpr)ogOldGlobalMap[g]));
rhss.Add(new IdentifierExpr(Token.NoToken, g));
}
newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
@@ -223,9 +223,9 @@ namespace Microsoft.Boogie // Add free requires
Expr freeRequiresExpr = Expr.True;
- foreach (Variable g in globalMap.Keys)
+ foreach (Variable g in ogOldGlobalMap.Keys)
{
- freeRequiresExpr = Expr.And(freeRequiresExpr, Expr.Eq(new IdentifierExpr(Token.NoToken, g), (IdentifierExpr)globalMap[g]));
+ freeRequiresExpr = Expr.And(freeRequiresExpr, Expr.Eq(new IdentifierExpr(Token.NoToken, g), (IdentifierExpr)ogOldGlobalMap[g]));
}
impl.Proc.Requires.Add(new Requires(true, freeRequiresExpr));
@@ -250,10 +250,18 @@ namespace Microsoft.Boogie locals.Add(copy);
map[local] = new IdentifierExpr(Token.NoToken, copy);
}
- Hashtable oldMap = new Hashtable(map);
- foreach (var global in globalMap.Keys)
+ Hashtable assumeMap = new Hashtable(map);
+ foreach (var global in ogOldGlobalMap.Keys)
{
- oldMap[global] = globalMap[global];
+ assumeMap[global] = ogOldGlobalMap[global];
+ }
+
+ Hashtable ogOldLocalMap = new Hashtable();
+ foreach (var g in program.GlobalVariables())
+ {
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og@local_old_{0}", g.Name), g.TypedIdent.Type));
+ locals.Add(copy);
+ ogOldLocalMap[g] = new IdentifierExpr(Token.NoToken, copy);
}
// Collect the yield predicates and desugar yields
@@ -333,7 +341,8 @@ namespace Microsoft.Boogie if (!procNameToInfo[impl.Name].containsYield && !procNameToInfo[impl.Name].isThreadStart) continue;
// Create the body of the yield checker procedure
- Substitution oldSubst = Substituter.SubstitutionFromHashtable(oldMap);
+ Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap);
+ Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap);
Substitution subst = Substituter.SubstitutionFromHashtable(map);
List<Block> yieldCheckerBlocks = new List<Block>();
StringSeq labels = new StringSeq();
@@ -349,12 +358,12 @@ namespace Microsoft.Boogie foreach (Cmd cmd in cs)
{
PredicateCmd predCmd = (PredicateCmd)cmd;
- newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.Apply(oldSubst, predCmd.Expr)));
+ newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr)));
}
foreach (Cmd cmd in cs)
{
PredicateCmd predCmd = (PredicateCmd)cmd;
- var newExpr = Substituter.Apply(subst, predCmd.Expr);
+ var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);
if (predCmd is AssertCmd)
newCmds.Add(new AssertCmd(Token.NoToken, newExpr));
else
@@ -375,9 +384,9 @@ namespace Microsoft.Boogie procNameToInfo[impl.Name].yieldCheckerImpl = yieldCheckerImpl;
}
- foreach (Variable v in globalMap.Keys)
+ foreach (Variable v in ogOldGlobalMap.Keys)
{
- IdentifierExpr ie = (IdentifierExpr) globalMap[v];
+ IdentifierExpr ie = (IdentifierExpr) ogOldGlobalMap[v];
program.TopLevelDeclarations.Add(ie.Decl);
}
foreach (ProcedureInfo info in procNameToInfo.Values)
diff --git a/Test/linear/Maps.bpl b/Test/linear/Maps.bpl new file mode 100644 index 00000000..5f302034 --- /dev/null +++ b/Test/linear/Maps.bpl @@ -0,0 +1,24 @@ +type X;
+
+function {:builtin "MapAdd"} MapAdd([X]int, [X]int) : [X]int;
+function {:builtin "MapSub"} MapSub([X]int, [X]int) : [X]int;
+function {:builtin "MapMul"} MapMul([X]int, [X]int) : [X]int;
+function {:builtin "MapDiv"} MapDiv([X]int, [X]int) : [X]int;
+function {:builtin "MapMod"} MapMod([X]int, [X]int) : [X]int;
+function {:builtin "MapConst"} MapConstInt(int) : [X]int;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:builtin "MapAnd"} MapAnd([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapNot"} MapNot([X]bool) : [X]bool;
+function {:builtin "MapIte"} MapIteInt([X]bool, [X]int, [X]int) : [X]int;
+function {:builtin "MapIte"} MapIteBool([X]bool, [X]bool, [X]bool) : [X]bool;
+function {:builtin "MapLe"} MapLe([X]int, [X]int) : [X]bool;
+function {:builtin "MapLt"} MapLt([X]int, [X]int) : [X]bool;
+function {:builtin "MapGe"} MapGe([X]int, [X]int) : [X]bool;
+function {:builtin "MapGt"} MapGt([X]int, [X]int) : [X]bool;
+function {:builtin "MapEq"} MapEq([X]int, [X]int) : [X]bool;
+function {:builtin "MapIff"} MapIff([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapImp"} MapImp([X]bool, [X]bool) : [X]bool;
+
+
+
diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl new file mode 100644 index 00000000..9a333351 --- /dev/null +++ b/Test/linear/list.bpl @@ -0,0 +1,39 @@ +var head: X;
+var tail: X;
+var {:linear "Mem"} D: [X]bool;
+var Next:[X]X;
+const nil: X;
+
+procedure malloc() returns (x: X, {:linear "Mem"} M: [X]bool);
+ensures M == MapConstBool(false)[x := true];
+
+procedure Join({:linear "Mem"} A: [X]bool);
+modifies D;
+ensures MapOr(old(D), A) == D;
+
+procedure one()
+requires D[head] && D[tail];
+requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
+ensures D[head] && D[tail];
+ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
+ensures head != tail;
+{
+ var x: X;
+ var {:linear "Mem"} M: [X]bool;
+
+ call x, M := malloc();
+ call Join(M);
+ Next[tail] := x;
+ tail := x;
+ Next[tail] := nil;
+}
+
+procedure two()
+requires head != tail;
+requires D[head] && D[tail];
+requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
+ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);
+ensures D[head] && D[tail];
+{
+ head := Next[head];
+}
diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat new file mode 100644 index 00000000..28c91996 --- /dev/null +++ b/Test/linear/runtest.bat @@ -0,0 +1,11 @@ +@echo off
+setlocal
+
+set BGEXE=..\..\Binaries\Boogie.exe
+
+for %%f in (list.bpl) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f Maps.bpl
+)
+
diff --git a/Test/og/Maps.bpl b/Test/og/Maps.bpl new file mode 100644 index 00000000..5f302034 --- /dev/null +++ b/Test/og/Maps.bpl @@ -0,0 +1,24 @@ +type X;
+
+function {:builtin "MapAdd"} MapAdd([X]int, [X]int) : [X]int;
+function {:builtin "MapSub"} MapSub([X]int, [X]int) : [X]int;
+function {:builtin "MapMul"} MapMul([X]int, [X]int) : [X]int;
+function {:builtin "MapDiv"} MapDiv([X]int, [X]int) : [X]int;
+function {:builtin "MapMod"} MapMod([X]int, [X]int) : [X]int;
+function {:builtin "MapConst"} MapConstInt(int) : [X]int;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:builtin "MapAnd"} MapAnd([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapNot"} MapNot([X]bool) : [X]bool;
+function {:builtin "MapIte"} MapIteInt([X]bool, [X]int, [X]int) : [X]int;
+function {:builtin "MapIte"} MapIteBool([X]bool, [X]bool, [X]bool) : [X]bool;
+function {:builtin "MapLe"} MapLe([X]int, [X]int) : [X]bool;
+function {:builtin "MapLt"} MapLt([X]int, [X]int) : [X]bool;
+function {:builtin "MapGe"} MapGe([X]int, [X]int) : [X]bool;
+function {:builtin "MapGt"} MapGt([X]int, [X]int) : [X]bool;
+function {:builtin "MapEq"} MapEq([X]int, [X]int) : [X]bool;
+function {:builtin "MapIff"} MapIff([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapImp"} MapImp([X]bool, [X]bool) : [X]bool;
+
+
+
diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl new file mode 100644 index 00000000..cddc5338 --- /dev/null +++ b/Test/og/bar.bpl @@ -0,0 +1,29 @@ +var g:int;
+
+procedure PB()
+{
+ g := g + 1;
+}
+
+procedure PC()
+ ensures g == old(g);
+{
+ assert{:yield} g == old(g);
+}
+
+procedure PD()
+{
+ g := 3;
+ call PC();
+ assert g == 3;
+}
+
+procedure{:entrypoint} Main2()
+{
+ while (true)
+ {
+ call{:async} PB();
+ call{:async} PC();
+ call{:async} PD();
+ }
+}
diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl new file mode 100644 index 00000000..d8d5bafd --- /dev/null +++ b/Test/og/foo.bpl @@ -0,0 +1,30 @@ +var g:int;
+
+procedure PB()
+{
+ g := g + 1;
+}
+
+procedure PC()
+ ensures g == 3;
+{
+ g := 3;
+ assert{:yield} g == 3;
+}
+
+procedure PD()
+{
+ call PC();
+ assert g == 3;
+ assert{:yield} true;
+}
+
+procedure{:entrypoint} Main()
+{
+ while (true)
+ {
+ call{:async} PB();
+ call{:async} PC();
+ call{:async} PD();
+ }
+}
diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl new file mode 100644 index 00000000..1a0cde42 --- /dev/null +++ b/Test/og/linear-set.bpl @@ -0,0 +1,68 @@ +function {:inline} Subset(a: [X]bool, b: [X]bool) : bool
+{
+ MapImp(a, b) == MapConstBool(true)
+}
+
+function {:inline} In(a: X, b: [X]bool) : bool
+{
+ b[a]
+}
+
+function {:inline} None() : [X]bool
+{
+ MapConstBool(false)
+}
+
+function {:inline} All() : [X]bool
+{
+ MapConstBool(true)
+}
+
+var x: int;
+var l: [X]bool;
+
+procedure Split({:linear "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
+ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
+
+procedure {:entrypoint} main({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)
+requires tidls' != None() && xls' == All();
+{
+ var {:linear "tid"} tidls: [X]bool;
+ var {:linear "x"} xls: [X]bool;
+ var {:linear "tid"} lsChild: [X]bool;
+ var {:linear "x"} xls1: [X]bool;
+ var {:linear "x"} xls2: [X]bool;
+
+ havoc tidls, xls;
+ assume tidls' == tidls && xls' == xls;
+
+ x := 42;
+ assert {:yield} xls == All();
+ assert x == 42;
+ call xls1, xls2 := Split(xls);
+ havoc lsChild;
+ assume (lsChild != None());
+ call {:async} thread(lsChild, xls1);
+ havoc lsChild;
+ assume (lsChild != None());
+ call {:async} thread(lsChild, xls2);
+}
+
+procedure thread({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)
+requires tidls' != None() && xls' != None();
+{
+ var {:linear "x"} xls: [X]bool;
+ var {:linear "tid"} tidls: [X]bool;
+
+ havoc tidls, xls;
+ assume tidls' == tidls && xls' == xls;
+
+ assume l == None();
+ l := tidls;
+ assert {:yield} tidls != None() && xls != None();
+ x := 0;
+ assert {:yield} tidls != None() && xls != None();
+ assert x == 0;
+ assert {:yield} tidls != None() && xls != None();
+ l := None();
+}
diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl new file mode 100644 index 00000000..a91100b6 --- /dev/null +++ b/Test/og/linear-set2.bpl @@ -0,0 +1,69 @@ +function {:inline} Subset(a: [X]bool, b: [X]bool) : bool
+{
+ MapImp(a, b) == MapConstBool(true)
+}
+
+function {:inline} In(a: X, b: [X]bool) : bool
+{
+ b[a]
+}
+
+function {:inline} None() : [X]bool
+{
+ MapConstBool(false)
+}
+
+function {:inline} All() : [X]bool
+{
+ MapConstBool(true)
+}
+
+var x: int;
+var l: X;
+const nil: X;
+
+procedure Split({:linear "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
+ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
+
+procedure {:entrypoint} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
+requires tidls' != nil && xls' == All();
+{
+ var {:linear "tid"} tidls: X;
+ var {:linear "x"} xls: [X]bool;
+ var {:linear "tid"} lsChild: X;
+ var {:linear "x"} xls1: [X]bool;
+ var {:linear "x"} xls2: [X]bool;
+
+ havoc tidls, xls;
+ assume tidls' == tidls && xls' == xls;
+
+ x := 42;
+ assert {:yield} xls == All();
+ assert x == 42;
+ call xls1, xls2 := Split(xls);
+ havoc lsChild;
+ assume (lsChild != nil);
+ call {:async} thread(lsChild, xls1);
+ havoc lsChild;
+ assume (lsChild != nil);
+ call {:async} thread(lsChild, xls2);
+}
+
+procedure thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
+requires tidls' != nil && xls' != None();
+{
+ var {:linear "x"} xls: [X]bool;
+ var {:linear "tid"} tidls: X;
+
+ havoc tidls, xls;
+ assume tidls' == tidls && xls' == xls;
+
+ assume l == nil;
+ l := tidls;
+ assert {:yield} tidls != nil && xls != None();
+ x := 0;
+ assert {:yield} tidls != nil && xls != None();
+ assert x == 0;
+ assert {:yield} tidls != nil && xls != None();
+ l := nil;
+}
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat new file mode 100644 index 00000000..353097c1 --- /dev/null +++ b/Test/og/runtest.bat @@ -0,0 +1,17 @@ +@echo off
+setlocal
+
+set BGEXE=..\..\Binaries\Boogie.exe
+
+for %%f in (foo.bpl bar.bpl) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
+)
+
+for %%f in (linear-set.bpl linear-set2.bpl) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f Maps.bpl
+)
+
|