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/UnitTests/CoreTests/ExprImmutability.cs | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'Source/UnitTests') 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