Merging changes from wuestholz/BoogieInvariantFixesIIII

7 files changed, 209 insertions, 59 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 07448087..cb03116e 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1429,7 +1429,7 @@ namespace Microsoft.Boogie {
       QKeyValue kv;

       for (kv = this.Attributes; kv != null; kv = kv.Next) {

         if (kv.Key == name) {

-          kv.Params.AddRange(vals);

+          kv.AddParams(vals);

           break;

         }

       }

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 11c3670e..d14250c1 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1,4 +1,4 @@
-//-----------------------------------------------------------------------------

+//-----------------------------------------------------------------------------

 //

 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

@@ -132,25 +132,51 @@ namespace Microsoft.Boogie {
 

   public class StmtList {

     [Rep]

-    public readonly List<BigBlock/*!*/>/*!*/ BigBlocks;

+    private readonly List<BigBlock/*!*/>/*!*/ bigBlocks;

+

+    public IList<BigBlock/*!*/>/*!*/ BigBlocks

+    {

+      get

+      {

+        Contract.Ensures(Contract.Result<IList<BigBlock>>() != null);

+        Contract.Ensures(Contract.Result<IList<BigBlock>>().IsReadOnly);

+        return this.bigBlocks.AsReadOnly();

+      }

+    }

+

     public List<Cmd> PrefixCommands;

     public readonly IToken/*!*/ EndCurly;

     public StmtList ParentContext;

     public BigBlock ParentBigBlock;

-    public HashSet<string/*!*/>/*!*/ Labels = new HashSet<string/*!*/>();

+

+    private readonly HashSet<string/*!*/>/*!*/ labels = new HashSet<string/*!*/>();

+

+    public void AddLabel(string label)

+    {

+      labels.Add(label);

+    }

+

+    public IEnumerable<string/*!*/>/*!*/ Labels

+    {

+      get

+      {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string/*!*/>/*!*/>()));

+        return this.labels.AsEnumerable<string>();

+      }

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(EndCurly != null);

-      Contract.Invariant(cce.NonNullElements(BigBlocks));

-      Contract.Invariant(cce.NonNullElements(Labels));

+      Contract.Invariant(cce.NonNullElements(this.bigBlocks));

+      Contract.Invariant(cce.NonNullElements(this.labels));

     }

 

-

-    public StmtList([Captured] List<BigBlock/*!*/>/*!*/ bigblocks, IToken endCurly) {

+    public StmtList(IList<BigBlock/*!*/>/*!*/ bigblocks, IToken endCurly) {

       Contract.Requires(endCurly != null);

       Contract.Requires(cce.NonNullElements(bigblocks));

       Contract.Requires(bigblocks.Count > 0);

-      this.BigBlocks = bigblocks;

+      this.bigBlocks = new List<BigBlock>(bigblocks);

       this.EndCurly = endCurly;

     }

 

@@ -385,7 +411,7 @@ namespace Microsoft.Boogie {
               prefix += "0";

             }

           }

-          stmtList.Labels.Add(b.LabelName);

+          stmtList.AddLabel(b.LabelName);

         }

       }

 

@@ -971,12 +997,33 @@ namespace Microsoft.Boogie {
     // This field is used during passification to null-out entries in block2Incartion hashtable early

     public int succCount;

 

-    public HashSet<Variable/*!*/> liveVarsBefore;

+    private HashSet<Variable/*!*/> _liveVarsBefore;

+

+    public IEnumerable<Variable/*!*/> liveVarsBefore

+    {

+      get

+      {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Variable/*!*/>>(), true));

+        if (this._liveVarsBefore == null)

+          return null;

+        else

+          return this._liveVarsBefore.AsEnumerable<Variable>();

+      }

+      set

+      {

+        Contract.Requires(cce.NonNullElements(value, true));

+        if (value == null)

+          this._liveVarsBefore = null;

+        else

+          this._liveVarsBefore = new HashSet<Variable>(value);

+      }

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(this.label != null);

       Contract.Invariant(this.cmds != null);

-      Contract.Invariant(cce.NonNullElements(liveVarsBefore, true));

+      Contract.Invariant(cce.NonNullElements(this._liveVarsBefore, true));

     }

 

     public bool IsLive(Variable v) {

@@ -1000,7 +1047,7 @@ namespace Microsoft.Boogie {
       this.cmds = cmds;

       this.TransferCmd = transferCmd;

       this.Predecessors = new List<Block>();

-      this.liveVarsBefore = null;

+      this._liveVarsBefore = null;

       this.TraversingStatus = VisitState.ToVisit;

       this.iterations = 0;

     }

@@ -1434,8 +1481,8 @@ namespace Microsoft.Boogie {
       Contract.Requires(lhs != null);

       Contract.Ensures(this.Lhss[index] == lhs);

       this._lhss[index] = lhs;

-    }
-
+    }

+

     private List<Expr/*!*/>/*!*/ _rhss;

 

     public IList<Expr/*!*/>/*!*/ Rhss {

@@ -2724,7 +2771,7 @@ namespace Microsoft.Boogie {
         if (QKeyValue.FindBoolAttribute(e.Attributes, "candidate"))

         {

             assume.Attributes = new QKeyValue(Token.NoToken, "candidate", new List<object>(), assume.Attributes);

-            assume.Attributes.Params.Add(this.callee);

+            assume.Attributes.AddParam(this.callee);

         }

         #endregion

         newBlockBody.Add(assume);

@@ -2896,7 +2943,6 @@ namespace Microsoft.Boogie {
 

   public class EEDTemplate : MiningStrategy {

     private string/*!*/ _reason;

-

     public string/*!*/ reason

     {

       get

@@ -2910,13 +2956,27 @@ namespace Microsoft.Boogie {
         this._reason = value;

       }

     }

+    

+    private List<Expr/*!*/>/*!*/ exprList;

+    public IEnumerable<Expr> Expressions

+    {

+      get

+      {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expr>>()));

+        return this.exprList.AsReadOnly();

+      }

+      set

+      {

+        Contract.Requires(cce.NonNullElements(value));

+        this.exprList = new List<Expr>(value);

+      }

+    }

 

-    public List<Expr/*!*/>/*!*/ exprList;

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(this._reason != null);

-      Contract.Invariant(cce.NonNullElements(exprList));

+      Contract.Invariant(cce.NonNullElements(this.exprList));

     }

 

     public EEDTemplate(string reason, List<Expr/*!*/>/*!*/ exprList) {

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 00a38d23..c5b7b317 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -1,4 +1,4 @@
-//-----------------------------------------------------------------------------

+//-----------------------------------------------------------------------------

 //

 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

@@ -249,22 +249,49 @@ namespace Microsoft.Boogie {
 

   public class QKeyValue : Absy {

     public readonly string/*!*/ Key;

-    public readonly List<object/*!*/>/*!*/ Params;  // each element is either a string or an Expr

+    private readonly List<object/*!*/>/*!*/ _params;  // each element is either a string or an Expr

+

+    public void AddParam(object p)

+    {

+      Contract.Requires(p != null);

+      this._params.Add(p);

+    }

+

+    public void AddParams(IEnumerable<object> ps)

+    {

+      Contract.Requires(cce.NonNullElements(ps));

+      this._params.AddRange(ps);

+    }

+

+    public void ClearParams()

+    {

+      this._params.Clear();

+    }

+

+    public IList<object> Params

+    {

+      get

+      {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IList<object>>()));

+        Contract.Ensures(Contract.Result<IList<object>>().IsReadOnly);

+        return this._params.AsReadOnly();

+      }

+    }

+

     public QKeyValue Next;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Key != null);

-      Contract.Invariant(cce.NonNullElements(Params));

+      Contract.Invariant(cce.NonNullElements(this._params));

     }

 

-

-    public QKeyValue(IToken tok, string key, [Captured] List<object/*!*/>/*!*/ parameters, QKeyValue next)

+    public QKeyValue(IToken tok, string key, IList<object/*!*/>/*!*/ parameters, QKeyValue next)

       : base(tok) {

       Contract.Requires(key != null);

       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(parameters));

       Key = key;

-      Params = parameters;

+      this._params = new List<object>(parameters);

       Next = next;

     }

 

@@ -418,14 +445,14 @@ namespace Microsoft.Boogie {
 

     public Trigger Next;

 

-    public Trigger(IToken/*!*/ tok, bool pos, IList<Expr>/*!*/ tr, Trigger next = null)

+    public Trigger(IToken/*!*/ tok, bool pos, IEnumerable<Expr>/*!*/ tr, Trigger next = null)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(tr != null);

-      Contract.Requires(tr.Count >= 1);

-      Contract.Requires(pos || tr.Count == 1);

+      Contract.Requires(tr.Count() >= 1);

+      Contract.Requires(pos || tr.Count() == 1);

       this.Pos = pos;

-      this.tr = new List<Expr>(tr);

+      this.Tr = new List<Expr>(tr);

       this.Next = next;

     }

 

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4ca08072..072e0323 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1,4 +1,4 @@
-//-----------------------------------------------------------------------------

+//-----------------------------------------------------------------------------

 //

 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

@@ -511,7 +511,7 @@ namespace Microsoft.Boogie {
       Contract.Invariant(0 <= EnhancedErrorMessages && EnhancedErrorMessages < 2);

       Contract.Invariant(0 <= StepsBeforeWidening && StepsBeforeWidening <= 9);

       Contract.Invariant(-1 <= this.bracketIdsInVC && this.bracketIdsInVC <= 1);

-      Contract.Invariant(cce.NonNullElements(ProverOptions));

+      Contract.Invariant(cce.NonNullElements(this.proverOptions));

     }

 

     public int LoopUnrollCount = -1;  // -1 means don't unroll loops

@@ -589,7 +589,28 @@ namespace Microsoft.Boogie {
     public ProverFactory TheProverFactory;

     public string ProverName;

     [Peer]

-    public List<string/*!*/>/*!*/ ProverOptions = new List<string/*!*/>();

+    private List<string> proverOptions = new List<string>();

+

+    public IEnumerable<string> ProverOptions

+    {

+      get

+      {

+        Contract.Ensures(Contract.Result<IEnumerable<string>>() != null);

+        foreach (string s in this.proverOptions)

+          yield return s;

+      }

+    }

+

+    public void AddProverOption(string option)

+    {

+      Contract.Requires(option != null);

+      this.proverOptions.Add(option);

+    }

+

+    public void RemoveAllProverOptions(Predicate<string> match)

+    {

+      this.proverOptions.RemoveAll(match);

+    }

 

     private int bracketIdsInVC = -1;  // -1 - not specified, 0 - no, 1 - yes

 

@@ -637,12 +658,29 @@ namespace Microsoft.Boogie {
     }

     [ContractInvariantMethod]

     void ObjectInvariant4() {

-      Contract.Invariant(cce.NonNullElements(Z3Options));

+      Contract.Invariant(cce.NonNullElements(this.z3Options));

       Contract.Invariant(0 <= Z3lets && Z3lets < 4);

     }

 

     [Peer]

-    public List<string/*!*/>/*!*/ Z3Options = new List<string/*!*/>();

+    private List<string> z3Options = new List<string>();

+

+    public IEnumerable<string> Z3Options

+    {

+      get

+      {

+        Contract.Ensures(Contract.Result<IEnumerable<string>>() != null);

+        foreach (string s in z3Options)

+          yield return s;

+      }

+    }

+

+    public void AddZ3Option(string option)

+    {

+      Contract.Requires(option != null);

+      this.z3Options.Add(option);

+    }

+

     public bool Z3types = false;

     public int Z3lets = 3;  // 0 - none, 1 - only LET TERM, 2 - only LET FORMULA, 3 - (default) any

 

@@ -727,10 +765,18 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public List<string/*!*/> ProcsToCheck = null;  // null means "no restriction"

+    public IEnumerable<string/*!*/> ProcsToCheck {

+      get {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<string/*!*/>>(), true));

+        return this.procsToCheck != null ? this.procsToCheck.AsEnumerable() : null;

+      }

+    }

+

+    private List<string/*!*/> procsToCheck = null;  // null means "no restriction"

+    

     [ContractInvariantMethod]

     void ObjectInvariant5() {

-      Contract.Invariant(cce.NonNullElements(ProcsToCheck, true));

+      Contract.Invariant(cce.NonNullElements(this.procsToCheck, true));

       Contract.Invariant(Ai != null);

     }

 

@@ -804,11 +850,11 @@ namespace Microsoft.Boogie {
           return true;

 

         case "proc":

-          if (ProcsToCheck == null) {

-            ProcsToCheck = new List<string/*!*/>();

+          if (this.procsToCheck == null) {

+            this.procsToCheck = new List<string/*!*/>();

           }

           if (ps.ConfirmArgumentCount(1)) {

-            ProcsToCheck.Add(cce.NonNull(args[ps.i]));

+            this.procsToCheck.Add(cce.NonNull(args[ps.i]));

           }

           return true;

 

@@ -1127,7 +1173,7 @@ namespace Microsoft.Boogie {
         case "p":

         case "proverOpt":

           if (ps.ConfirmArgumentCount(1)) {

-            ProverOptions.Add(cce.NonNull(args[ps.i]));

+            AddProverOption(cce.NonNull(args[ps.i]));

           }

           return true;

 

@@ -1420,7 +1466,7 @@ namespace Microsoft.Boogie {
 		

         case "z3opt":

           if (ps.ConfirmArgumentCount(1)) {

-            Z3Options.Add(cce.NonNull(args[ps.i]));

+            AddZ3Option(cce.NonNull(args[ps.i]));

           }

           return true;

 

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index ad4dd4df..77086f0f 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -28,13 +28,13 @@ namespace Microsoft.Boogie {
       List<Variable>/*!*/ vars = new List<Variable>();

       foreach (Variable/*!*/ var in impl.LocVars) {

         Contract.Assert(var != null);

-        if (usedVars.Contains(var))

+        if (_usedVars.Contains(var))

           vars.Add(var);

       }

       impl.LocVars = vars;

       //Console.WriteLine("New number of local variables = {0}", impl.LocVars.Length);

       //Console.WriteLine("---------------------------------");

-      usedVars.Clear();

+      _usedVars.Clear();

       return impl;

     }

   }

@@ -274,19 +274,35 @@ namespace Microsoft.Boogie {
   }

 

   public class VariableCollector : ReadOnlyVisitor {

-    public HashSet<Variable/*!*/>/*!*/ usedVars;

-    public HashSet<Variable/*!*/>/*!*/ oldVarsUsed;

+    protected HashSet<Variable/*!*/>/*!*/ _usedVars;

+    public IEnumerable<Variable /*!*/>/*!*/ usedVars

+    {

+      get

+      {

+        return _usedVars.AsEnumerable();

+      }

+    }

+

+    protected HashSet<Variable/*!*/>/*!*/ _oldVarsUsed;

+    public IEnumerable<Variable /*!*/>/*!*/ oldVarsUsed

+    {

+      get

+      {

+        return _oldVarsUsed.AsEnumerable();

+      }

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(cce.NonNullElements(usedVars));

-      Contract.Invariant(cce.NonNullElements(oldVarsUsed));

+      Contract.Invariant(cce.NonNullElements(_usedVars));

+      Contract.Invariant(cce.NonNullElements(_oldVarsUsed));

     }

 

     int insideOldExpr;

 

     public VariableCollector() {

-      usedVars = new System.Collections.Generic.HashSet<Variable/*!*/>();

-      oldVarsUsed = new System.Collections.Generic.HashSet<Variable/*!*/>();

+      _usedVars = new System.Collections.Generic.HashSet<Variable/*!*/>();

+      _oldVarsUsed = new System.Collections.Generic.HashSet<Variable/*!*/>();

       insideOldExpr = 0;

     }

 

@@ -303,9 +319,9 @@ namespace Microsoft.Boogie {
       //Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<Expr>() != null);

       if (node.Decl != null) {

-        usedVars.Add(node.Decl);

+        _usedVars.Add(node.Decl);

         if (insideOldExpr > 0) {

-          oldVarsUsed.Add(node.Decl);

+          _oldVarsUsed.Add(node.Decl);

         }

       }

       return node;

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 58366051..f7538b53 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -1,4 +1,4 @@
-//-----------------------------------------------------------------------------

+//-----------------------------------------------------------------------------

 //

 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

@@ -438,12 +438,13 @@ namespace Microsoft.Boogie {
     public virtual QKeyValue VisitQKeyValue(QKeyValue node) {

       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<QKeyValue>() != null);

+      var newParams = new List<object>();

       for (int i = 0, n = node.Params.Count; i < n; i++) {

         var e = node.Params[i] as Expr;

-        if (e != null) {

-          node.Params[i] = (Expr)this.Visit(e);

-        }

+        newParams.Add(e != null ? this.Visit(e) : node.Params[i]);

       }

+      node.ClearParams();

+      node.AddParams(newParams);

       if (node.Next != null) {

         node.Next = (QKeyValue)this.Visit(node.Next);

       }

@@ -522,11 +523,11 @@ namespace Microsoft.Boogie {
       if (origNext != null) {

         Trigger newNext = this.VisitTrigger(origNext);

         if (newNext != origNext) {

-          node = new Trigger(node.tok, node.Pos, node.Tr);  // note: this creates sharing between the old and new Tr sequence

+          node = new Trigger(node.tok, node.Pos, node.Tr.ToList());

           node.Next = newNext;

         }

       }

-      node.Tr = this.VisitExprSeq(new List<Expr>(node.Tr));

+      node.Tr = this.VisitExprSeq(node.Tr.ToList());

       return node;

     }

     // called by default for all nullary type constructors and type variables

@@ -1072,7 +1073,7 @@ namespace Microsoft.Boogie {
           {

               this.VisitTrigger(origNext);

           }

-          node.Tr = this.VisitExprSeq(new List<Expr>(node.Tr));

+          this.VisitExprSeq(node.Tr.ToList());

           return node;

       }

       // called by default for all nullary type constructors and type variables

diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
index 5a8100a7..87b8f3e6 100644
--- a/Source/Core/VCExp.cs
+++ b/Source/Core/VCExp.cs
@@ -81,7 +81,7 @@ The generic options may or may not be used by the prover plugin.
       }

     }

 

-    public virtual void Parse(List<string/*!*/>/*!*/ opts) {

+    public virtual void Parse(IEnumerable<string/*!*/>/*!*/ opts) {

       Contract.Requires(cce.NonNullElements(opts));

       StringBuilder sb = new StringBuilder(stringRepr);

       Contract.Assert(sb != null);