From 1f8368fd50c720fe8080d6724e8bbfaecb6f486d Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 12 Feb 2015 10:52:46 +0000
Subject: Protect the Args field of NAryExpr when it is immutable.

* Made changing the reference throw an exception if the NAryExpr was
constructed as immutable
* Changed the type of NAryExpr.Args to be IList<Expr> rather than
List<Expr> so that when the NAryExpr is immutable I can return
``_Args.AsReadOnly()`` (instead of ``_Args``) which returns a read
only wrapper around the List<Expr> so that clients cannot change the
list.

I came across two problems

* Making this change required changing types all over the place (from
List<Expr> to IList<Expr>). I feel that changes are extensive enough
that there's a good chance that out of tree clients using Boogie's
libraries might break. I've waited for a code review but this didn't
happen so I'm committing anyway.

* I came across something that looks like bad design of the IAppliable
interface which potentially breaks immutability enforcement. I've left
this as a "FIXME" in this. Here's the problematic method.

```
Type Typecheck(ref List<Expr>/*!*/ args, out
TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/
tc);
```

It potentially allows the instance of the args to be changed which
seems very suspect.
---
 Source/Core/StandardVisitor.cs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Source/Core/StandardVisitor.cs')

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 82cd5025..8c3d6326 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -30,7 +30,7 @@ namespace Microsoft.Boogie {
     public virtual void TransferStateTo(Visitor targetVisitor) {
     }
 
-    public virtual List<Expr> VisitExprSeq(List<Expr> list) {
+    public virtual IList<Expr> VisitExprSeq(IList<Expr> list) {
       Contract.Requires(list != null);
       Contract.Ensures(Contract.Result<List<Expr>>() != null);
       lock (list)
@@ -257,7 +257,7 @@ namespace Microsoft.Boogie {
       Expr e = (Expr)this.Visit(node);
       return e;
     }
-    public override List<Expr> VisitExprSeq(List<Expr> exprSeq) {
+    public override IList<Expr> VisitExprSeq(IList<Expr> exprSeq) {
       //Contract.Requires(exprSeq != null);
       Contract.Ensures(Contract.Result<List<Expr>>() != null);
       for (int i = 0, n = exprSeq.Count; i < n; i++)
@@ -821,7 +821,7 @@ namespace Microsoft.Boogie {
           Contract.Ensures(Contract.Result<Expr>() == node);
           return (Expr)this.Visit(node);
       }
-      public override List<Expr> VisitExprSeq(List<Expr> exprSeq)
+      public override IList<Expr> VisitExprSeq(IList<Expr> exprSeq)
       {
           Contract.Ensures(Contract.Result<List<Expr>>() == exprSeq);
           for (int i = 0, n = exprSeq.Count; i < n; i++)
-- 
cgit v1.2.3