From 1f8368fd50c720fe8080d6724e8bbfaecb6f486d Mon Sep 17 00:00:00 2001 From: Dan Liew 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 rather than List so that when the NAryExpr is immutable I can return ``_Args.AsReadOnly()`` (instead of ``_Args``) which returns a read only wrapper around the List so that clients cannot change the list. I came across two problems * Making this change required changing types all over the place (from List to IList). 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/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc); ``` It potentially allows the instance of the args to be changed which seems very suspect. --- Source/Core/Absy.cs | 3 +- Source/Core/AbsyExpr.cs | 91 +++++++++++++++++--------- Source/Core/Duplicator.cs | 2 +- Source/Core/StandardVisitor.cs | 6 +- Source/Core/Util.cs | 2 +- Source/UnitTests/CoreTests/ExprImmutability.cs | 14 ++++ 6 files changed, 80 insertions(+), 38 deletions(-) diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 9f7e57cf..a1a54024 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -4129,6 +4129,7 @@ namespace Microsoft.Boogie { } public static class Emitter { + public static void Emit(this List/*!*/ decls, TokenTextWriter stream) { Contract.Requires(stream != null); Contract.Requires(cce.NonNullElements(decls)); @@ -4156,7 +4157,7 @@ namespace Microsoft.Boogie { } } - public static void Emit(this List ts, TokenTextWriter stream) { + public static void Emit(this IList ts, TokenTextWriter stream) { Contract.Requires(stream != null); string sep = ""; stream.push(); diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 4efabe97..3938e396 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1105,7 +1105,7 @@ namespace Microsoft.Boogie { /// /// /// - void Emit(List/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext); + void Emit(IList/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext); void Resolve(ResolutionContext/*!*/ rc, Expr/*!*/ subjectForErrorReporting); @@ -1135,7 +1135,7 @@ namespace Microsoft.Boogie { /// /// Returns the result type of the IAppliable, supposing the argument are of the correct types. /// - Type/*!*/ ShallowType(List/*!*/ args); + Type/*!*/ ShallowType(IList/*!*/ args); T Dispatch(IAppliableVisitor/*!*/ visitor); } @@ -1151,7 +1151,7 @@ namespace Microsoft.Boogie { } } - public void Emit(List args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + public void Emit(IList args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { Contract.Requires(args != null); Contract.Requires(stream != null); throw new NotImplementedException(); @@ -1178,7 +1178,7 @@ namespace Microsoft.Boogie { throw new NotImplementedException(); } - public Type ShallowType(List args) { + public Type ShallowType(IList args) { Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); @@ -1278,7 +1278,7 @@ namespace Microsoft.Boogie { } } - public void Emit(List args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + public void Emit(IList args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); stream.SetToken(ref this.tok); @@ -1346,7 +1346,7 @@ namespace Microsoft.Boogie { this.FunctionName, arg0type); return null; } - public Type ShallowType(List args) { + public Type ShallowType(IList args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); switch (this.op) { @@ -1494,7 +1494,7 @@ namespace Microsoft.Boogie { } } - public void Emit(List args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + public void Emit(IList args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); stream.SetToken(ref this.tok); @@ -1716,7 +1716,7 @@ namespace Microsoft.Boogie { return null; } - public Type ShallowType(List args) { + public Type ShallowType(IList args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); switch (this.op) { @@ -1954,7 +1954,7 @@ namespace Microsoft.Boogie { return Func.GetHashCode(); } - virtual public void Emit(List args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + virtual public void Emit(IList args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); this.name.Emit(stream, 0xF0, false); @@ -2027,7 +2027,7 @@ namespace Microsoft.Boogie { return actualResultType[0]; } } - public Type ShallowType(List args) { + public Type ShallowType(IList args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); Contract.Assume(name.Type != null); @@ -2075,7 +2075,7 @@ namespace Microsoft.Boogie { } } - public void Emit(List/*!*/ args, TokenTextWriter/*!*/ stream, + public void Emit(IList/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(args != null); //Contract.Requires(stream != null); @@ -2127,7 +2127,7 @@ namespace Microsoft.Boogie { return this.Type; } - public Type ShallowType(List args) { + public Type ShallowType(IList args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); return this.Type; @@ -2206,7 +2206,7 @@ namespace Microsoft.Boogie { } } - virtual public void Emit(List args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + virtual public void Emit(IList args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); stream.Write(this.name); @@ -2237,7 +2237,7 @@ namespace Microsoft.Boogie { return this.type; } - public Type ShallowType(List args) { + public Type ShallowType(IList args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); return this.type; @@ -2264,8 +2264,21 @@ namespace Microsoft.Boogie { _Fun = value; } } - // FIXME: Protect this field when immutable - public List Args; + private List _Args; + public IList Args { + get { + if (Immutable) + return _Args.AsReadOnly(); + else + return _Args; + } + set { + if (Immutable) + throw new InvalidOperationException("Cannot change Args of Immutable NAryExpr"); + + _Args = value as List; + } + } [ContractInvariantMethod] void ObjectInvariant() { @@ -2279,16 +2292,30 @@ namespace Microsoft.Boogie { public TypeParamInstantiation TypeParameters = null; [Captured] - public NAryExpr(IToken/*!*/ tok, IAppliable/*!*/ fun, List/*!*/ args, bool immutable=false) + public NAryExpr(IToken/*!*/ tok, IAppliable/*!*/ fun, IList/*!*/ args, bool immutable=false) : base(tok, immutable) { Contract.Requires(tok != null); Contract.Requires(fun != null); Contract.Requires(args != null); _Fun = fun; - Args = args; Contract.Assert(Contract.ForAll(0, args.Count, index => args[index] != null)); - if (immutable) - CachedHashCode = ComputeHashCode(); + if (immutable) { + // We need to make a new list because the client might be holding + // references to the list that they gave us which could be used to + // circumvent the immutability enforcement + _Args = new List(args); + CachedHashCode = ComputeHashCode(); + } else { + if (args is List) { + // Preserve NAryExpr's old behaviour, we take ownership of the List. + // We can only do this if the type matches + _Args = args as List; + } + else { + // Otherwise we must make a copy + _Args = new List (args); + } + } } [Pure] [Reads(ReadsAttribute.Reads.Nothing)] @@ -2365,7 +2392,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); + Type = Fun.Typecheck(ref _Args, out tpInsts, tc); // FIXME: Might break immutability TypeParameters = tpInsts; } IOverloadedAppliable oa = Fun as IOverloadedAppliable; @@ -2431,7 +2458,7 @@ namespace Microsoft.Boogie { return Arity.GetHashCode() * 2823; } - public void Emit(List/*!*/ args, TokenTextWriter/*!*/ stream, + public void Emit(IList/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(args != null); //Contract.Requires(stream != null); @@ -2439,7 +2466,7 @@ namespace Microsoft.Boogie { Emit(args, stream, contextBindingStrength, fragileContext, false); } - public static void Emit(List/*!*/ args, TokenTextWriter/*!*/ stream, + public static void Emit(IList/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext, bool withRhs) { Contract.Requires(args != null); @@ -2464,7 +2491,7 @@ namespace Microsoft.Boogie { if (withRhs) { stream.Write(" := "); - cce.NonNull(args.FindLast(Item => true)).Emit(stream); + cce.NonNull(args.Last()).Emit(stream); } stream.Write("]"); @@ -2550,7 +2577,7 @@ namespace Microsoft.Boogie { /// /// Returns the result type of the IAppliable, supposing the argument are of the correct types. /// - public Type ShallowType(List args) { + public Type ShallowType(IList args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); Expr a0 = cce.NonNull(args[0]); @@ -2612,7 +2639,7 @@ namespace Microsoft.Boogie { return Arity.GetHashCode() * 28231; } - public void Emit(List/*!*/ args, TokenTextWriter/*!*/ stream, + public void Emit(IList/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(args != null); //Contract.Requires(stream != null); @@ -2633,7 +2660,7 @@ namespace Microsoft.Boogie { } // it is assumed that each of the arguments has already been typechecked - public static Type Typecheck(List/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, + public static Type Typecheck(IList/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc, IToken/*!*/ typeCheckingSubject, string/*!*/ opName) { @@ -2656,9 +2683,9 @@ namespace Microsoft.Boogie { // error messages have already been created by MapSelect.Typecheck return null; } - Type rhsType = cce.NonNull(cce.NonNull(args.FindLast(Item => true)).Type); + Type rhsType = cce.NonNull(cce.NonNull(args.Last()).Type); if (!resultType.Unify(rhsType)) { - tc.Error(cce.NonNull(args.FindLast(Item => true)).tok, + tc.Error(cce.NonNull(args.Last()).tok, "right-hand side in {0} with wrong type: {1} (expected: {2})", opName, rhsType, resultType); return null; @@ -2681,7 +2708,7 @@ namespace Microsoft.Boogie { /// /// Returns the result type of the IAppliable, supposing the argument are of the correct types. /// - public Type ShallowType(List args) { + public Type ShallowType(IList args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); return cce.NonNull(args[0]).ShallowType; @@ -2743,7 +2770,7 @@ namespace Microsoft.Boogie { return 1; } - public void Emit(List args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + public void Emit(IList args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); stream.SetToken(this); @@ -2800,7 +2827,7 @@ namespace Microsoft.Boogie { /// /// Returns the result type of the IAppliable, supposing the argument are of the correct types. /// - public Type ShallowType(List args) { + public Type ShallowType(IList args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); return cce.NonNull(args[1]).ShallowType; diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 4350571a..becd1791 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -214,7 +214,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return base.VisitExpr((Expr)node.Clone()); } - public override List VisitExprSeq(List list) { + public override IList VisitExprSeq(IList list) { //Contract.Requires(list != null); Contract.Ensures(Contract.Result>() != null); return base.VisitExprSeq(new List(list)); 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 VisitExprSeq(List list) { + public virtual IList VisitExprSeq(IList list) { Contract.Requires(list != null); Contract.Ensures(Contract.Result>() != null); lock (list) @@ -257,7 +257,7 @@ namespace Microsoft.Boogie { Expr e = (Expr)this.Visit(node); return e; } - public override List VisitExprSeq(List exprSeq) { + public override IList VisitExprSeq(IList exprSeq) { //Contract.Requires(exprSeq != null); Contract.Ensures(Contract.Result>() != null); for (int i = 0, n = exprSeq.Count; i < n; i++) @@ -821,7 +821,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() == node); return (Expr)this.Visit(node); } - public override List VisitExprSeq(List exprSeq) + public override IList VisitExprSeq(IList exprSeq) { Contract.Ensures(Contract.Result>() == exprSeq); for (int i = 0, n = exprSeq.Count; i < n; i++) diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index 4afd6f69..3b8412b9 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -487,7 +487,7 @@ namespace Microsoft.Boogie { } else if (e is NAryExpr) { NAryExpr ne = (NAryExpr)e; IAppliable fun = ne.Fun; - List eSeq = ne.Args; + var eSeq = ne.Args; if (fun != null) { if ((fun.FunctionName == "$Length" || fun.FunctionName == "$StringLength") && eSeq.Count == 1) { Expr e0 = eSeq[0]; diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs index 3dd2e427..a26f8b8b 100644 --- a/Source/UnitTests/CoreTests/ExprImmutability.cs +++ b/Source/UnitTests/CoreTests/ExprImmutability.cs @@ -199,6 +199,20 @@ namespace CoreTests e.Fun = new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Sub); } + [Test(), ExpectedException(typeof(NotSupportedException))] + public void ProtectedNAryArgsList() + { + var e = GetUnTypedImmutableNAry(); + e.Args.Add(null); + } + + [Test(), ExpectedException(typeof(InvalidOperationException))] + public void ProtectedNAryArgs() + { + var e = GetUnTypedImmutableNAry(); + e.Args = new List(); + } + [Test(), ExpectedException(typeof(InvalidOperationException))] public void ProtectedForAllExprBody() { -- cgit v1.2.3