diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 2 | ||||
| -rw-r--r-- | Source/Core/LinearSets.cs | 15 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 10 | ||||
| -rw-r--r-- | Test/og/FlanaganQadeer.bpl | 42 | ||||
| -rw-r--r-- | Test/og/runtest.bat | 2 |
5 files changed, 59 insertions, 12 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 69fb547c..c4db46f4 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -197,7 +197,7 @@ namespace Microsoft.Boogie { }
LinearSetTransform linearTransform = new LinearSetTransform(program);
linearTransform.Transform();
-
+
EliminateDeadVariablesAndInline(program);
int errorCount, verified, inconclusives, timeOuts, outOfMemories;
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 4edbfeed..d2904d59 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -285,11 +285,6 @@ namespace Microsoft.Boogie b.Cmds = newCmds;
}
- foreach (var v in copies.Values)
- {
- impl.LocVars.Add(v);
- }
-
{
// Loops
impl.PruneUnreachableBlocks();
@@ -332,6 +327,11 @@ namespace Microsoft.Boogie newCmds.AddRange(impl.Blocks[0].Cmds);
impl.Blocks[0].Cmds = newCmds;
}
+
+ foreach (var v in copies.Values)
+ {
+ impl.LocVars.Add(v);
+ }
}
foreach (var decl in program.TopLevelDeclarations)
@@ -437,7 +437,10 @@ namespace Microsoft.Boogie lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, copies[allocator])));
rhss.Add(new IdentifierExpr(Token.NoToken, allocator));
}
- newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
+ if (lhss.Count > 0)
+ {
+ newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
+ }
foreach (string domainName in domainNameToHavocVars.Keys)
{
var allocator = linearDomains[domainName].allocator;
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index 6eaf9650..55565375 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -232,17 +232,19 @@ namespace Microsoft.Boogie // Create substitution maps
Hashtable map = new Hashtable();
VariableSeq locals = new VariableSeq();
- foreach (Variable inParam in impl.Proc.InParams)
+ for (int i = 0; i < impl.Proc.InParams.Length; i++)
{
+ Variable inParam = impl.Proc.InParams[i];
var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
locals.Add(copy);
- map[inParam] = new IdentifierExpr(Token.NoToken, copy);
+ map[impl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy);
}
- foreach (Variable outParam in impl.Proc.OutParams)
+ for (int i = 0; i < impl.Proc.OutParams.Length; i++)
{
+ Variable outParam = impl.Proc.OutParams[i];
var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type), outParam.Attributes);
locals.Add(copy);
- map[outParam] = new IdentifierExpr(Token.NoToken, copy);
+ map[impl.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy);
}
foreach (Variable local in impl.LocVars)
{
diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl new file mode 100644 index 00000000..63a7fc0d --- /dev/null +++ b/Test/og/FlanaganQadeer.bpl @@ -0,0 +1,42 @@ +const nil: X;
+var l: X;
+var x: int;
+
+procedure {:entrypoint} main()
+{
+ var {:linear "tid"} tid: X;
+ var val: int;
+
+ while (*)
+ {
+ havoc tid, val;
+ assume tid != nil;
+ call {:async} foo(tid, val);
+ }
+}
+
+procedure foo({:linear "tid"} tid': X, val: int)
+requires tid' != nil;
+{
+ var {:linear "tid"} tid: X;
+ assume tid == tid';
+
+ assume l == nil;
+ l := tid;
+ call tid := Yield(tid);
+ x := val;
+ call tid := Yield(tid);
+ assert x == val;
+ call tid := Yield(tid);
+ l := nil;
+}
+
+procedure Yield({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)
+requires tid' != nil;
+ensures tid == tid';
+ensures old(l) == tid ==> old(l) == l && old(x) == x;
+{
+ assume tid == tid';
+ assert {:yield} tid != nil;
+ assert (old(l) == tid ==> old(l) == l && old(x) == x);
+}
\ No newline at end of file diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat index 353097c1..3ec39f7e 100644 --- a/Test/og/runtest.bat +++ b/Test/og/runtest.bat @@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl) do ( %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
)
-for %%f in (linear-set.bpl linear-set2.bpl) do (
+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f Maps.bpl
|