Fix what looked like a serious design issue when Type checking

anything that implements the IAppliable interface. Type checking
should never need to change the reference of a list of arguments
(hence the removal of the ``ref`` keyword) and we need to use IList<Expr>
instead of List<Expr> to allow NAryExpr to do its type checking.

2 files changed, 14 insertions, 13 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 7557a796..75f2c519 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1131,7 +1131,7 @@ namespace Microsoft.Boogie {
     /// </summary>

     /// <param name="args"></param>

     /// <param name="tc"></param>

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

+    Type Typecheck(IList<Expr>/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc);

 

     // Contract.Requires( Microsoft.SpecSharp.Collections.Reductions.Forall{Expr! arg in args; arg.Type != null});

 

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

     }

 

-    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

       Contract.Requires(args != null);

       Contract.Requires(tc != null);

       Contract.Ensures(Contract.ValueAtReturn(out args) != null);

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

     }

 

-    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

       //Contract.Requires(tc != null);

       //Contract.Requires(args != null);

       Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);

@@ -1625,7 +1625,7 @@ namespace Microsoft.Boogie {
         return 2;

       }

     }

-    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

       //Contract.Requires(tc != null);

       //Contract.Requires(args != null);

       Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);

@@ -1997,7 +1997,7 @@ namespace Microsoft.Boogie {
         return Func.InParams.Count;

       }

     }

-    public virtual Type Typecheck(ref List<Expr> actuals, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public virtual Type Typecheck(IList<Expr> actuals, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

       //Contract.Requires(tc != null);

       //Contract.Requires(actuals != null);

       Contract.Ensures(Contract.ValueAtReturn(out actuals) != null);

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

     }

 

-    public Type Typecheck(ref List<Expr>/*!*/ args,

+    public Type Typecheck(IList<Expr>/*!*/ args,

                           out TypeParamInstantiation/*!*/ tpInstantiation,

                           TypecheckingContext/*!*/ tc) {

       //Contract.Requires(args != null);

@@ -2223,7 +2223,7 @@ namespace Microsoft.Boogie {
       //Contract.Requires(rc != null);

     }

 

-    public virtual Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public virtual Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

       //Contract.Requires(tc != null);

       //Contract.Requires(args != null);

       Contract.Ensures(args != null);

@@ -2395,7 +2395,7 @@ namespace Microsoft.Boogie {
         // typechecked and does not need to be checked again

                TypeParameters == null) {

         TypeParamInstantiation tpInsts;

-        Type = Fun.Typecheck(ref _Args, out tpInsts, tc); // FIXME: Might break immutability

+        Type = Fun.Typecheck(Args, out tpInsts, tc); // Make sure we pass Args so if this Expr is immutable it is protected

         TypeParameters = tpInsts;

       }

       IOverloadedAppliable oa = Fun as IOverloadedAppliable;

@@ -2563,12 +2563,13 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

       //Contract.Requires(tc != null);

       //Contract.Requires(args != null);

       Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);

       Contract.Assume(args.Count == Arity + 1);

 

+      // FIXME: Wny are we passing a copy?

       List<Expr> actualArgs = new List<Expr>();

       for (int i = 1; i < args.Count; ++i)

         actualArgs.Add(args[i]);

@@ -2697,7 +2698,7 @@ namespace Microsoft.Boogie {
       return cce.NonNull(args[0]).Type;

     }

 

-    public Type Typecheck(ref List<Expr>/*!*/ args,

+    public Type Typecheck(IList<Expr>/*!*/ args,

                           out TypeParamInstantiation/*!*/ tpInstantiation,

                           TypecheckingContext/*!*/ tc) {

       //Contract.Requires(args != null);

@@ -2803,7 +2804,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public Type Typecheck(ref List<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

+    public Type Typecheck(IList<Expr> args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {

       //Contract.Requires(tc != null);

       //Contract.Requires(args != null);

       Contract.Ensures(args != null);

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 446621af..97309155 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -437,7 +437,7 @@ namespace Microsoft.Boogie {
     public static IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/

                   MatchArgumentTypes(List<TypeVariable>/*!*/ typeParams,

                                      List<Type>/*!*/ formalArgs,

-                                     List<Expr>/*!*/ actualArgs,

+                                     IList<Expr>/*!*/ actualArgs,

                                      List<Type> formalOuts,

                                      List<IdentifierExpr> actualOuts,

                                      string/*!*/ opName,

@@ -507,7 +507,7 @@ namespace Microsoft.Boogie {
     public static List<Type> CheckArgumentTypes(List<TypeVariable>/*!*/ typeParams,

                                              out List<Type/*!*/>/*!*/ actualTypeParams,

                                              List<Type>/*!*/ formalIns,

-                                             List<Expr>/*!*/ actualIns,

+                                             IList<Expr>/*!*/ actualIns,

                                              List<Type>/*!*/ formalOuts,

                                              List<IdentifierExpr> actualOuts,

                                              IToken/*!*/ typeCheckingSubject,