fixed bug (reported by Akash) in treatment of linear parameters to calls

5 files changed, 143 insertions, 16 deletions

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index 3d244316..3f31a8aa 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -563,41 +563,90 @@ namespace Microsoft.Boogie
 

         void TransformCallCmd(CmdSeq newCmds, CallCmd callCmd, Dictionary<Variable, LocalVariable> copies, Dictionary<string, HashSet<Variable>> domainNameToScope)

         {

-            HashSet<Variable> rhsVars = new HashSet<Variable>();

+            Dictionary<string, HashSet<Variable>> domainNameToRhsVars = new Dictionary<string, HashSet<Variable>>();

+            List<AssignLhs> lhss = new List<AssignLhs>();

+            List<Expr> rhss = new List<Expr>(); 

             for (int i = 0; i < callCmd.Proc.InParams.Length; i++)

             {

                 if (QKeyValue.FindStringAttribute(callCmd.Proc.InParams[i].Attributes, "linear") == null) continue;

                 IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr;

                 Variable source = ie.Decl;

-                rhsVars.Add(source);

+                var domainName = varToDomainName[source];

+                var allocator = linearDomains[domainName].allocator;

+                if (!copies.ContainsKey(allocator))

+                {

+                    copies[allocator] = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("copy_{0}", allocator.Name), allocator.TypedIdent.Type));

+                }

+                if (!copies.ContainsKey(source))

+                {

+                    copies[source] = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("copy_{0}", source.Name), source.TypedIdent.Type));

+                }

+                if (!domainNameToRhsVars.ContainsKey(domainName))

+                {

+                    domainNameToRhsVars[domainName] = new HashSet<Variable>();

+                    lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, copies[allocator])));

+                    rhss.Add(new IdentifierExpr(Token.NoToken, allocator));

+                }

+                domainNameToRhsVars[domainName].Add(source);

+                lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, copies[source])));

+                rhss.Add(new IdentifierExpr(Token.NoToken, source));

+                callCmd.Ins[i] = new IdentifierExpr(Token.NoToken, copies[source]);

             }

+            newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));

+

             HashSet<Variable> lhsVars = new HashSet<Variable>();

-            HashSet<string> domainNames = new HashSet<string>();

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

             foreach (IdentifierExpr ie in callCmd.Outs)

             {

                 Variable v = ie.Decl;

                 if (!varToDomainName.ContainsKey(v)) continue;

                 lhsVars.Add(v);

-                domainNames.Add(varToDomainName[v]);

+                lhsDomainNames.Add(varToDomainName[v]);

+            }

+

+            foreach (var domainName in domainNameToRhsVars.Keys)

+            {

+                var domain = linearDomains[domainName];

+                HashSet<Variable> scope = new HashSet<Variable>();

+                IdentifierExprSeq havocExprs = new IdentifierExprSeq();

+                foreach (Variable v in domainNameToRhsVars[domainName])

+                {

+                    if (lhsVars.Contains(v)) continue;

+                    havocExprs.Add(new IdentifierExpr(Token.NoToken, v));

+                    scope.Add(v);

+                }

+                if (havocExprs.Length > 0)

+                {

+                    scope.Add(domain.allocator);

+                    havocExprs.Add(new IdentifierExpr(Token.NoToken, domain.allocator));

+                    newCmds.Add(new HavocCmd(Token.NoToken, havocExprs));

+                    newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, scope)));

+                    Expr expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False));

+                    foreach (IdentifierExpr ie in havocExprs)

+                    {

+                        expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(ie.Decl.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), expr));

+                    }

+                    expr = Expr.Binary(BinaryOperator.Opcode.Eq, expr, new IdentifierExpr(Token.NoToken, copies[domain.allocator]));

+                    newCmds.Add(new AssumeCmd(Token.NoToken, expr));

+                    foreach (Variable v in scope)

+                    {

+                        if (v == domain.allocator) continue;

+                        Drain(newCmds, copies[v], varToDomainName[v]);

+                    }

+                }

             }

-            foreach (Variable v in lhsVars.Union(rhsVars))

+

+            foreach (Variable v in lhsVars)

             {

                 Drain(newCmds, v, varToDomainName[v]);

             }

+            

             newCmds.Add(callCmd);

-            foreach (string domainName in domainNames)

+            

+            foreach (string domainName in lhsDomainNames)

             {

                 newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName])));

             } 

-            IdentifierExprSeq havocExprs = new IdentifierExprSeq();

-            foreach (Variable v in rhsVars.Except(lhsVars))

-            {

-                havocExprs.Add(new IdentifierExpr(Token.NoToken, v));

-            }

-            if (havocExprs.Length > 0)

-            {

-                TransformHavocCmd(newCmds, new HavocCmd(Token.NoToken, havocExprs), copies, domainNameToScope);

-            }

         }

 

         void TransformAssignCmd(CmdSeq newCmds, AssignCmd assignCmd, Dictionary<Variable, LocalVariable> copies, Dictionary<string, HashSet<Variable>> domainNameToScope)

diff --git a/Test/linear/Answer b/Test/linear/Answer
index 680f9895..662e6670 100644
--- a/Test/linear/Answer
+++ b/Test/linear/Answer
@@ -27,3 +27,14 @@ Execution trace:
     allocator.bpl(6,3): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

+

+-------------------- f1.bpl --------------------

+

+Boogie program verifier finished with 2 verified, 0 errors

+

+-------------------- f2.bpl --------------------

+f2.bpl(18,4): Error BP5001: This assertion might not hold.

+Execution trace:

+    f2.bpl(14,4): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/linear/f1.bpl b/Test/linear/f1.bpl
new file mode 100644
index 00000000..0d9189ab
--- /dev/null
+++ b/Test/linear/f1.bpl
@@ -0,0 +1,48 @@
+function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

+const {:existential true} b0: bool;

+const {:existential true} b1: bool;

+const {:existential true} b2: bool;

+const {:existential true} b3: bool;

+const {:existential true} b4: bool;

+const {:existential true} b5: bool;

+const {:existential true} b6: bool;

+const {:existential true} b7: bool;

+const {:existential true} b8: bool;

+

+axiom(b0);

+axiom(b1);

+axiom(b2);

+axiom(b3);

+axiom(b4);

+axiom(b5);

+axiom(!b6);

+axiom(!b7);

+axiom(b8);

+

+procedure {:entrypoint} main({:linear "1"} x_in: [int]bool) 

+  requires b0 ==> x_in == mapconstbool(true);

+  requires b1 ==> x_in != mapconstbool(false);

+{

+   var {:linear "1"} x: [int] bool;

+   assume x == x_in;

+

+   assume x == mapconstbool(true);

+

+   call foo(x);

+   

+   assert b6 ==> x == mapconstbool(true);

+   assert b7 ==> x != mapconstbool(false);

+   assert b8 ==> x == mapconstbool(false);

+}

+

+procedure foo({:linear "1"} x_in: [int]bool)

+  requires b2 ==> x_in == mapconstbool(true);

+  requires b3 ==> x_in != mapconstbool(false);

+{

+   var {:linear "1"} x: [int] bool;

+   assume x == x_in;

+

+   assert b4 ==> x == mapconstbool(true);

+   assert b5 ==> x != mapconstbool(false);

+

+}

diff --git a/Test/linear/f2.bpl b/Test/linear/f2.bpl
new file mode 100644
index 00000000..4e4bfbcf
--- /dev/null
+++ b/Test/linear/f2.bpl
@@ -0,0 +1,19 @@
+function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

+function {:builtin "MapOr"} mapunion([int]bool, [int]bool) : [int]bool;

+

+procedure Split({:linear "1"} xls: [int]bool) returns ({:linear "1"} xls1: [int]bool, {:linear "1"} xls2: [int]bool);

+ensures xls == mapunion(xls1, xls2) && xls1 != mapconstbool(false) && xls2 != mapconstbool(false);

+

+

+procedure {:entrypoint} main() 

+{

+   var {:linear "1"} x: [int] bool;

+   var {:linear "1"} x1: [int] bool;

+   var {:linear "1"} x2: [int] bool;

+

+   havoc x;

+   assume x == mapconstbool(true);

+

+   call x1, x2 := Split(x);

+   assert false;

+}

diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat
index 5681784a..3ccd660c 100644
--- a/Test/linear/runtest.bat
+++ b/Test/linear/runtest.bat
@@ -9,7 +9,7 @@ for %%f in (typecheck.bpl) do (
   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f

 )

 

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

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

   echo.

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

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