Merge

4 files changed, 56 insertions, 31 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 43523b55..5e69b179 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1186,6 +1186,15 @@ namespace Microsoft.Boogie {
       }

     }

 

+    public int TimeLimit

+    {

+      get

+      {

+        int tl = CommandLineOptions.Clo.ProverKillTime;

+        CheckIntAttribute("timeLimit", ref tl);

+        return tl;

+      }

+    }

 

     public NamedDeclaration(IToken/*!*/ tok, string/*!*/ name)

       : base(tok) {

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index fcb3157b..51034bf3 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1496,6 +1496,9 @@ namespace Microsoft.Boogie {
        Assign a unique ID to an implementation to be used for verification

        result caching (default: ""<impl. name>:0"").

 

+     {:timeLimit N}

+       Set the time limit for a given implementation.

+

   ---- On functions ----------------------------------------------------------

 

      {:builtin ""spec""}

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index 84ce264d..27312f38 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -156,24 +156,33 @@ namespace Microsoft.Boogie
                 else if (cmd is CallCmd)

                 {

                     CallCmd callCmd = (CallCmd)cmd;

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

+                    while (callCmd != null)

                     {

-                        if (FindDomainName(callCmd.Proc.InParams[i]) == null) continue;

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

-                        if (start.Contains(ie.Decl))

-                        {

-                            start.Remove(ie.Decl);

-                        }

-                        else

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

                         {

-                            Error(ie, "unavailable source for a linear read");

+                            if (FindDomainName(callCmd.Proc.InParams[i]) == null) continue;

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

+                            if (start.Contains(ie.Decl))

+                            {

+                                start.Remove(ie.Decl);

+                            }

+                            else

+                            {

+                                Error(ie, "unavailable source for a linear read");

+                            }

                         }

+                        callCmd = callCmd.InParallelWith;

                     }

+                    callCmd = (CallCmd)cmd;

                     availableLocalLinearVars[callCmd] = new HashSet<Variable>(start);

-                    foreach (IdentifierExpr ie in callCmd.Outs)

+                    while (callCmd != null)

                     {

-                        if (FindDomainName(ie.Decl) == null) continue;

-                        start.Add(ie.Decl);

+                        foreach (IdentifierExpr ie in callCmd.Outs)

+                        {

+                            if (FindDomainName(ie.Decl) == null) continue;

+                            start.Add(ie.Decl);

+                        }

+                        callCmd = callCmd.InParallelWith;

                     }

                 }

                 else if (cmd is HavocCmd)

@@ -356,19 +365,6 @@ namespace Microsoft.Boogie
             return base.VisitCallCmd(node);

         }

 

-        private void TransformCallCmd(CallCmd callCmd, Dictionary<string, Expr> domainNameToExpr)

-        {

-            foreach (var domainName in linearDomains.Keys)

-            {

-                callCmd.Ins.Add(domainNameToExpr[domainName]);

-            }

-            CallCmd parallelCallCmd = callCmd.InParallelWith;

-            if (parallelCallCmd != null)

-            {

-                TransformCallCmd(parallelCallCmd, domainNameToExpr);

-            }

-        }

-

         private void AddDisjointnessExpr(CmdSeq newCmds, Absy absy, Dictionary<string, Variable> domainNameToInputVar)

         {

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

@@ -427,6 +423,18 @@ namespace Microsoft.Boogie
                                     callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False)));

                                 }

                             }

+                            else if (callCmd.InParallelWith != null)

+                            {

+                                while (callCmd != null)

+                                {

+                                    foreach (var domainName in linearDomains.Keys)

+                                    {

+                                        var domain = linearDomains[domainName];

+                                        callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False)));

+                                    }

+                                    callCmd = callCmd.InParallelWith;

+                                }

+                            }

                             else

                             {

                                 Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();

@@ -441,7 +449,10 @@ namespace Microsoft.Boogie
                                     IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

                                     domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName]));

                                 }

-                                TransformCallCmd(callCmd, domainNameToExpr);

+                                foreach (var domainName in linearDomains.Keys)

+                                {

+                                    callCmd.Ins.Add(domainNameToExpr[domainName]);

+                                }

                             }

                         }

                         else if (cmd is YieldCmd)

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index 14f5f328..e353700f 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -131,7 +131,7 @@ namespace Microsoft.Boogie
         public override Cmd VisitCallCmd(CallCmd node)

         {

             ProcedureInfo info = procNameToInfo[node.callee];

-            if (!node.IsAsync && !info.isAtomic)

+            if (node.InParallelWith != null || node.IsAsync || !info.isAtomic)

             {

                 procNameToInfo[currentImpl.Name].isAtomic = false;

                 moreProcessingRequired = true;

@@ -487,6 +487,10 @@ namespace Microsoft.Boogie
                     CallCmd callCmd = cmd as CallCmd;

                     if (callCmd != null)

                     {

+                        if (callCmd.InParallelWith != null || callCmd.IsAsync || !procNameToInfo[callCmd.callee].isAtomic)

+                        {

+                            AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

+                        }

                         if (callCmd.InParallelWith != null)

                         {

                             List<Expr> ins;

@@ -507,14 +511,12 @@ namespace Microsoft.Boogie
                             dummyCallCmd.Proc = dummyAsyncTargetProc;

                             newCmds.Add(dummyCallCmd);

                         }

-                        else if (procNameToInfo[callCmd.callee].isAtomic)

+                        else

                         {

                             newCmds.Add(callCmd);

                         }

-                        else

+                        if (callCmd.InParallelWith != null || callCmd.IsAsync || !procNameToInfo[callCmd.callee].isAtomic)

                         {

-                            AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

-                            newCmds.Add(callCmd);

                             HashSet<Variable> availableLocalLinearVars = new HashSet<Variable>(linearTypechecker.availableLocalLinearVars[callCmd]);

                             foreach (IdentifierExpr ie in callCmd.Outs)

                             {