fixed bugs in both parallel calls and linear stuff (reported by Chris)

also added improved error reporting suggested by Chris

12 files changed, 122 insertions, 33 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index c4db46f4..9d1038f5 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -192,7 +192,7 @@ namespace Microsoft.Boogie {
             ogTransform.Transform();

             int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;

             CommandLineOptions.Clo.PrintUnstructured = 1;

-            PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false);

+            PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false);

             CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;

         }

         LinearSetTransform linearTransform = new LinearSetTransform(program);

@@ -213,7 +213,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring) {

+    static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring, bool setTokens = true) {

       Contract.Requires(program != null);

       Contract.Requires(filename != null);

       bool oldPrintDesugaring = CommandLineOptions.Clo.PrintDesugarings;

@@ -221,8 +221,8 @@ namespace Microsoft.Boogie {
         CommandLineOptions.Clo.PrintDesugarings = false;

       }

       using (TokenTextWriter writer = filename == "-" ?

-                                      new TokenTextWriter("<console>", Console.Out) :

-                                      new TokenTextWriter(filename)) {

+                                      new TokenTextWriter("<console>", Console.Out, setTokens) :

+                                      new TokenTextWriter(filename, setTokens)) {

         if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never) {

           writer.WriteLine("// " + CommandLineOptions.Clo.Version);

           writer.WriteLine("// " + CommandLineOptions.Clo.Environment);

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index f409d67a..c092139d 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -393,7 +393,24 @@ namespace Microsoft.Boogie
                     proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToInParams[domainName])));

                 }

             }

-

+            foreach (var decl in program.TopLevelDeclarations)

+            {

+                Procedure proc = decl as Procedure;

+                if (proc == null) continue;

+                HashSet<string> domainNamesForOutParams = new HashSet<string>();

+                foreach (Variable v in proc.OutParams)

+                {

+                    var domainName = QKeyValue.FindStringAttribute(v.Attributes, "linear");

+                    if (domainName == null) continue;

+                    if (!linearDomains.ContainsKey(domainName))

+                    {

+                        linearDomains[domainName] = new LinearDomain(program, v, domainName);

+                    }

+                    if (domainNamesForOutParams.Contains(domainName)) continue;

+                    domainNamesForOutParams.Add(domainName);

+                    proc.Modifies.Add(new IdentifierExpr(Token.NoToken, linearDomains[domainName].allocator));

+                }

+            }

             foreach (LinearDomain domain in linearDomains.Values)

             {

                 program.TopLevelDeclarations.Add(domain.allocator);

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index fd14823b..fd97c20e 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -105,6 +105,10 @@ namespace Microsoft.Boogie
                 CallCmd iter = node;

                 while (iter != null)

                 {

+                    if (!procNameToInfo.ContainsKey(iter.Proc.Name))

+                    {

+                        procNameToInfo[iter.Proc.Name] = new ProcedureInfo();

+                    }

                     procNameToInfo[iter.Proc.Name].isThreadStart = true;

                     CreateYieldCheckerProcedure(iter.Proc);

                     procNameToInfo[iter.Proc.Name].inParallelCall = true;

@@ -353,7 +357,7 @@ namespace Microsoft.Boogie
                     foreach (Requires r in impl.Proc.Requires)

                     {

                         if (r.Free) continue;

-                        cmds.Add(new AssertCmd(Token.NoToken, r.Condition));

+                        cmds.Add(new AssertCmd(r.tok, r.Condition));

                     }

                     yields.Add(cmds);

                     cmds = new CmdSeq();

@@ -363,7 +367,7 @@ namespace Microsoft.Boogie
                     foreach (Ensures e in impl.Proc.Ensures)

                     {

                         if (e.Free) continue;

-                        cmds.Add(new AssertCmd(Token.NoToken, e.Condition));

+                        cmds.Add(new AssertCmd(e.tok, e.Condition));

                     }

                     yields.Add(cmds);

                     cmds = new CmdSeq();

@@ -385,15 +389,15 @@ namespace Microsoft.Boogie
                             PredicateCmd pcmd = cmd as PredicateCmd;

                             if (pcmd == null)

                             {

+                                DesugarYield(cmds, newCmds);

                                 if (cmds.Length > 0)

                                 {

-                                    DesugarYield(cmds, newCmds);

                                     yields.Add(cmds);

                                     cmds = new CmdSeq();

                                 }

                                 insideYield = false;

                             }

-                            else 

+                            else

                             {

                                 cmds.Add(pcmd);

                             }

@@ -433,11 +437,14 @@ namespace Microsoft.Boogie
                             newCmds.Add(cmd);

                         }

                     }

-                    if (cmds.Length > 0)

+                    if (insideYield)

                     {

                         DesugarYield(cmds, newCmds);

-                        yields.Add(cmds);

-                        cmds = new CmdSeq();

+                        if (cmds.Length > 0)

+                        {

+                            yields.Add(cmds);

+                            cmds = new CmdSeq();

+                        }

                     } 

                     if (b.TransferCmd is ReturnCmd && (!info.isAtomic || info.isEntrypoint || info.isThreadStart))

                     {

@@ -500,7 +507,7 @@ namespace Microsoft.Boogie
                         PredicateCmd predCmd = (PredicateCmd)cmd;

                         var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);

                         if (predCmd is AssertCmd)

-                            newCmds.Add(new AssertCmd(Token.NoToken, newExpr));

+                            newCmds.Add(new AssertCmd(predCmd.tok, newExpr));

                         else

                             newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));

                     }

diff --git a/Test/linear/Answer b/Test/linear/Answer
index 86e42862..69caec25 100644
--- a/Test/linear/Answer
+++ b/Test/linear/Answer
@@ -12,9 +12,17 @@ typecheck.bpl(51,4): Error: Only variable can be assigned to a linear variable
 typecheck.bpl(53,4): Error: The domains of formal and actual parameters must be the same

 typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same

 typecheck.bpl(57,4): Error: Only a linear argument can be passed to a linear parameter

-typecheck.bpl(64,6): Error: Only linear variable can be assigned to another linear variable

+typecheck.bpl(61,4): Error: A linear set can occur only once as an in parameter

+typecheck.bpl(66,6): Error: Only linear variable can be assigned to another linear variable

 0 type checking errors detected in typecheck.bpl

 

 -------------------- list.bpl --------------------

 

 Boogie program verifier finished with 2 verified, 0 errors

+

+-------------------- allocator.bpl --------------------

+allocator.bpl(8,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    allocator.bpl(6,3): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/linear/allocator.bpl b/Test/linear/allocator.bpl
new file mode 100644
index 00000000..4b162a83
--- /dev/null
+++ b/Test/linear/allocator.bpl
@@ -0,0 +1,10 @@
+procedure A({:linear "tid"} i': int) returns ({:linear "tid"} i: int);

+  ensures i == i';

+

+procedure{:entrypoint} B({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

+{

+  assume i == i';

+  call i := A(i);

+  assert false;

+}

+

diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat
index df176994..d054b097 100644
--- a/Test/linear/runtest.bat
+++ b/Test/linear/runtest.bat
@@ -3,7 +3,7 @@ setlocal
 

 set BGEXE=..\..\Binaries\Boogie.exe

 

-for %%f in (typecheck.bpl list.bpl) do (

+for %%f in (typecheck.bpl list.bpl allocator.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f

diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index f79f8fb5..c188d5b5 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -57,9 +57,13 @@ procedure D()
     call a, x := E(c, x);

 

     call c, x := E(a, x);

+

+    call a := F(a) | x := F(a);

 }

 

 procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)

 {

     c := a;

-}
\ No newline at end of file
+}

+

+procedure F({:linear "D"} a: X) returns ({:linear "D"} c: X);
\ No newline at end of file
diff --git a/Test/og/Answer b/Test/og/Answer
index a8d4ba44..1b341ee4 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -1,21 +1,21 @@
 

 -------------------- foo.bpl --------------------

-OwickiGriesDesugared.bpl(171,4): Error BP5001: This assertion might not hold.

+foo.bpl(13,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    OwickiGriesDesugared.bpl(17,0): anon0

-    OwickiGriesDesugared.bpl(169,0): inline$YieldChecker_PC$0$L1

+    foo.bpl(5,5): anon0

+    (0,0): inline$YieldChecker_PC$0$L1

 

 Boogie program verifier finished with 3 verified, 1 error

 

 -------------------- bar.bpl --------------------

-OwickiGriesDesugared.bpl(171,4): Error BP5001: This assertion might not hold.

+bar.bpl(12,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    OwickiGriesDesugared.bpl(17,0): anon0

-    OwickiGriesDesugared.bpl(169,0): inline$YieldChecker_PC$0$L1

-OwickiGriesDesugared.bpl(171,4): Error BP5001: This assertion might not hold.

+    bar.bpl(5,5): anon0

+    (0,0): inline$YieldChecker_PC$0$L1

+bar.bpl(12,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    OwickiGriesDesugared.bpl(68,0): anon0

-    OwickiGriesDesugared.bpl(169,0): inline$YieldChecker_PC$0$L1

+    bar.bpl(17,5): anon0

+    (0,0): inline$YieldChecker_PC$0$L1

 

 Boogie program verifier finished with 2 verified, 2 errors

 

@@ -24,17 +24,21 @@ Boogie program verifier finished with 2 verified, 2 errors
 Boogie program verifier finished with 2 verified, 0 errors

 

 -------------------- parallel1.bpl --------------------

-OwickiGriesDesugared.bpl(171,4): Error BP5001: This assertion might not hold.

+parallel1.bpl(9,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    OwickiGriesDesugared.bpl(17,0): anon0

-    OwickiGriesDesugared.bpl(169,0): inline$YieldChecker_PC$0$L1

-OwickiGriesDesugared.bpl(177,4): Error BP5001: This assertion might not hold.

+    parallel1.bpl(5,5): anon0

+    (0,0): inline$YieldChecker_PC$0$L1

+parallel1.bpl(13,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    OwickiGriesDesugared.bpl(17,0): anon0

-    OwickiGriesDesugared.bpl(175,0): inline$YieldChecker_PC$0$L2

+    parallel1.bpl(5,5): anon0

+    (0,0): inline$YieldChecker_PC$0$L2

 

 Boogie program verifier finished with 3 verified, 2 errors

 

+-------------------- parallel3.bpl --------------------

+

+Boogie program verifier finished with 3 verified, 0 errors

+

 -------------------- linear-set.bpl --------------------

 

 Boogie program verifier finished with 2 verified, 0 errors

@@ -54,3 +58,13 @@ Boogie program verifier finished with 5 verified, 0 errors
 -------------------- parallel2.bpl --------------------

 

 Boogie program verifier finished with 4 verified, 0 errors

+

+-------------------- parallel4.bpl --------------------

+parallel4.bpl(14,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    parallel4.bpl(12,3): anon0

+    (0,0): inline$YieldChecker_t$0$enter

+    (0,0): inline$YieldChecker_t$0$exit

+    parallel4.bpl(12,3): anon0$2

+

+Boogie program verifier finished with 2 verified, 1 error

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 444b9805..f2d45204 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -32,4 +32,5 @@ ensures old(a)[i] == a[i];
 {

     assume i == i';

     yield;

+    assert old(a)[i] == a[i];

 }
\ No newline at end of file
diff --git a/Test/og/parallel3.bpl b/Test/og/parallel3.bpl
new file mode 100644
index 00000000..a99a5eb8
--- /dev/null
+++ b/Test/og/parallel3.bpl
@@ -0,0 +1,7 @@
+procedure {:entrypoint} main() 

+{

+    call A() | B();

+}

+

+procedure A() {}

+procedure B() {}

diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
new file mode 100644
index 00000000..a5b2768f
--- /dev/null
+++ b/Test/og/parallel4.bpl
@@ -0,0 +1,21 @@
+var a:int;

+

+procedure {:entrypoint} main() 

+{

+  var {:linear "tid"} i: int;

+  var {:linear "tid"} j: int;

+  call i := t(i) | j := t(j);

+}

+

+procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+{

+  assume i == i';

+  call Yield();

+  assert a == old(a);

+  a := a + 1;

+}

+

+procedure Yield()

+{

+  yield;

+}

diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index 0cca4898..a1cbfba0 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -3,13 +3,13 @@ setlocal
 

 set BGEXE=..\..\Binaries\Boogie.exe

 

-for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl) do (

+for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl parallel3.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f

 )

 

-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl) do (

+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis  /OwickiGries:OwickiGriesDesugared.bpl %%f