mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/BoxedExpression.cs

   1 //
   2 // BoxedExpression.cs
   3 //
   4 // Authors:
   5 //      Alexander Chebaturkin (chebaturkin@gmail.com)
   6 //
   7 // Copyright (C) 2011 Alexander Chebaturkin
   8 //
   9 // Permission is hereby granted, free of charge, to any person obtaining
  10 // a copy of this software and associated documentation files (the
  11 // "Software"), to deal in the Software without restriction, including
  12 // without limitation the rights to use, copy, modify, merge, publish,
  13 // distribute, sublicense, and/or sell copies of the Software, and to
  14 // permit persons to whom the Software is furnished to do so, subject to
  15 // the following conditions:
  16 //
  17 // The above copyright notice and this permission notice shall be
  18 // included in all copies or substantial portions of the Software.
  19 //
  20 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
  21 // EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
  22 // MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  23 // NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
  24 // LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
  25 // OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
  26 // WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  27 //
  28
  29 using System;
  30 using System.Collections;
  31 using System.Collections.Generic;
  32 using System.IO;
  33 using System.Linq;
  34 using Mono.CodeContracts.Static.AST;
  35 using Mono.CodeContracts.Static.AST.Visitors;
  36 using Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding;
  37 using Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths;
  38 using Mono.CodeContracts.Static.ControlFlow;
  39 using Mono.CodeContracts.Static.DataStructures;
  40 using Mono.CodeContracts.Static.Providers;
  41
  42 namespace Mono.CodeContracts.Static.Proving {
  43         internal abstract class BoxedExpression {
  44                 public virtual bool IsVariable
  45                 {
  46                         get { return false; }
  47                 }
  48
  49                 public virtual bool IsBooleanTyped
  50                 {
  51                         get { return false; }
  52                 }
  53
  54                 public virtual object UnderlyingVariable
  55                 {
  56                         get { return false; }
  57                 }
  58
  59                 public virtual PathElement[] AccessPath
  60                 {
  61                         get { return null; }
  62                 }
  63
  64                 public virtual bool IsConstant
  65                 {
  66                         get { return false; }
  67                 }
  68
  69                 public virtual object Constant
  70                 {
  71                         get { throw new InvalidOperationException (); }
  72                 }
  73
  74                 public virtual object ConstantType
  75                 {
  76                         get { throw new InvalidOperationException (); }
  77                 }
  78
  79                 public virtual bool IsSizeof
  80                 {
  81                         get { return false; }
  82                 }
  83
  84                 public virtual bool IsUnary
  85                 {
  86                         get { return false; }
  87                 }
  88
  89                 public virtual UnaryOperator UnaryOperator
  90                 {
  91                         get { throw new InvalidOperationException (); }
  92                 }
  93
  94                 public virtual BoxedExpression UnaryArgument
  95                 {
  96                         get { throw new InvalidOperationException (); }
  97                 }
  98
  99                 public virtual bool IsBinary
 100                 {
 101                         get { return false; }
 102                 }
 103
 104                 public virtual BinaryOperator BinaryOperator
 105                 {
 106                         get { throw new InvalidOperationException (); }
 107                 }
 108
 109                 public virtual BoxedExpression BinaryLeftArgument
 110                 {
 111                         get { throw new InvalidOperationException (); }
 112                 }
 113
 114                 public virtual BoxedExpression BinaryRightArgument
 115                 {
 116                         get { throw new InvalidOperationException (); }
 117                 }
 118
 119                 public virtual bool IsIsinst
 120                 {
 121                         get { return false; }
 122                 }
 123
 124                 public virtual bool IsNull
 125                 {
 126                         get { return false; }
 127                 }
 128
 129                 public virtual bool IsCast
 130                 {
 131                         get { return false; }
 132                 }
 133
 134                 public virtual bool IsResult
 135                 {
 136                         get { return false; }
 137                 }
 138
 139                 public virtual bool TryGetType (out object type)
 140                 {
 141                         type = null;
 142                         return false;
 143                 }
 144
 145                 public virtual bool IsBinaryExpression (out BinaryOperator op, out BoxedExpression left, out BoxedExpression right)
 146                 {
 147                         op = BinaryOperator.Add;
 148                         left = null;
 149                         right = null;
 150                         return false;
 151                 }
 152
 153                 public virtual bool IsUnaryExpression (out UnaryOperator op, out BoxedExpression argument)
 154                 {
 155                         op = UnaryOperator.Conv_i;
 156                         argument = null;
 157                         return false;
 158                 }
 159
 160                 public virtual bool Sizeof (out int size)
 161                 {
 162                         return false.Without (out size);
 163                 }
 164
 165                 public virtual bool IsIsinstExpression (out BoxedExpression expr, out TypeNode type)
 166                 {
 167                         expr = null;
 168                         type = null;
 169                         return false;
 170                 }
 171
 172                 public abstract void AddFreeVariables (HashSet<BoxedExpression> set);
 173
 174                 public virtual BoxedExpression Substitute (BoxedExpression what, BoxedExpression replace)
 175                 {
 176                         if (this == what || Equals (what))
 177                                 return replace;
 178
 179                         return RecursiveSubstitute (what, replace);
 180                 }
 181
 182                 public abstract BoxedExpression Substitute<Variable> (Func<Variable, BoxedExpression, BoxedExpression> map);
 183
 184                 protected internal virtual BoxedExpression RecursiveSubstitute (BoxedExpression what, BoxedExpression replace)
 185                 {
 186                         return this;
 187                 }
 188
 189                 public abstract Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
 190                         where Visitor : IILVisitor<PC, Dummy, Dummy, Data, Result>;
 191
 192                 public static BoxedExpression Var (object var)
 193                 {
 194                         return new VariableExpression (var);
 195                 }
 196
 197                 public static BoxedExpression Const (object value, TypeNode type)
 198                 {
 199                         return new ConstantExpression (value, type);
 200                 }
 201
 202                 public static BoxedExpression For<Variable, Expression> (Expression external, IFullExpressionDecoder<Variable, Expression> decoder)
 203                         where Expression : IEquatable<Expression>
 204                 {
 205                         return new ExternalBox<Variable, Expression> (external, decoder);
 206                 }
 207
 208                 public static BoxedExpression MakeIsinst (TypeNode type, BoxedExpression arg)
 209                 {
 210                         return new IsinstExpression (arg, type);
 211                 }
 212
 213                 public static BoxedExpression Convert<Variable, ExternalExpression> (ExternalExpression expr, IFullExpressionDecoder<Variable, ExternalExpression> decoder)
 214                 {
 215                         TypeNode type;
 216                         object value;
 217                         if (decoder.IsConstant (expr, out value, out type))
 218                                 return new ConstantExpression (value, type);
 219                         if (decoder.IsNull (expr))
 220                                 return new ConstantExpression (null, null);
 221
 222                         object variable;
 223                         if (decoder.IsVariable (expr, out variable)) {
 224                                 Sequence<PathElement> variableAccessPath = decoder.GetVariableAccessPath (expr);
 225                                 return new VariableExpression (variable, variableAccessPath);
 226                         }
 227
 228                         if (decoder.IsSizeof (expr, out type)) {
 229                                 int sizeAsConstant;
 230                                 return decoder.TrySizeOfAsConstant (expr, out sizeAsConstant) ? new SizeOfExpression (type, sizeAsConstant) : new SizeOfExpression (type);
 231                         }
 232
 233                         ExternalExpression arg;
 234                         if (decoder.IsIsinst (expr, out arg, out type))
 235                                 return new IsinstExpression (Convert (arg, decoder), type);
 236
 237                         UnaryOperator op;
 238                         if (decoder.IsUnaryExpression (expr, out op, out arg))
 239                                 return new UnaryExpression (op, Convert (arg, decoder));
 240
 241                         BinaryOperator bop;
 242                         ExternalExpression left;
 243                         ExternalExpression right;
 244                         if (!decoder.IsBinaryExpression (expr, out bop, out left, out right))
 245                                 throw new InvalidOperationException ();
 246
 247                         return new BinaryExpression (bop, Convert (left, decoder), Convert (right, decoder));
 248                 }
 249
 250                 public static BoxedExpression Binary (BinaryOperator bop, BoxedExpression left, BoxedExpression right)
 251                 {
 252                         return new BinaryExpression (bop, left, right);
 253                 }
 254
 255                 public static BoxedExpression Unary (UnaryOperator op, BoxedExpression arg)
 256                 {
 257                         return new UnaryExpression (op, arg);
 258                 }
 259
 260                 #region Nested type: AssertExpression
 261                 public class AssertExpression : ContractExpression {
 262                         public AssertExpression (BoxedExpression condition, EdgeTag tag, APC pc) : base (condition, tag, pc)
 263                         {
 264                         }
 265
 266                         #region Overrides of ContractExpression
 267                         public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
 268                         {
 269                                 return visitor.Assert (pc, this.Tag, Dummy.Value, data);
 270                         }
 271
 272                         public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
 273                         {
 274                                 BoxedExpression cond = this.Condition.Substitute (map);
 275                                 if (cond == this.Condition)
 276                                         return this;
 277                                 if (cond == null)
 278                                         return null;
 279
 280                                 return new AssertExpression (cond, this.Tag, this.Apc);
 281                         }
 282                         #endregion
 283                 }
 284                 #endregion
 285
 286                 #region Nested type: AssumeExpression
 287                 public class AssumeExpression : ContractExpression {
 288                         public AssumeExpression (BoxedExpression condition, EdgeTag tag, APC pc)
 289                                 : base (condition, tag, pc)
 290                         {
 291                         }
 292
 293                         #region Overrides of ContractExpression
 294                         public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
 295                         {
 296                                 return visitor.Assume (pc, this.Tag, Dummy.Value, data);
 297                         }
 298
 299                         public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
 300                         {
 301                                 BoxedExpression cond = this.Condition.Substitute (map);
 302                                 if (cond == this.Condition)
 303                                         return this;
 304                                 if (cond == null)
 305                                         return null;
 306
 307                                 return new AssumeExpression (cond, this.Tag, this.Apc);
 308                         }
 309                         #endregion
 310                 }
 311                 #endregion
 312
 313                 #region Nested type: BinaryExpression
 314                 public class BinaryExpression : BoxedExpression {
 315                         public readonly BoxedExpression Left;
 316                         public readonly BinaryOperator Op;
 317                         public readonly BoxedExpression Right;
 318
 319                         public BinaryExpression (BinaryOperator op, BoxedExpression left, BoxedExpression right)
 320                         {
 321                                 this.Op = op;
 322                                 this.Left = left;
 323                                 this.Right = right;
 324                         }
 325
 326                         public override bool IsBinary
 327                         {
 328                                 get { return true; }
 329                         }
 330
 331                         public override BoxedExpression BinaryLeftArgument
 332                         {
 333                                 get { return this.Left; }
 334                         }
 335
 336                         public override BoxedExpression BinaryRightArgument
 337                         {
 338                                 get { return this.Right; }
 339                         }
 340
 341                         public override BinaryOperator BinaryOperator
 342                         {
 343                                 get { return this.Op; }
 344                         }
 345
 346                         public override bool IsBinaryExpression (out BinaryOperator op, out BoxedExpression left, out BoxedExpression right)
 347                         {
 348                                 op = this.Op;
 349                                 left = this.Left;
 350                                 right = this.Right;
 351                                 return true;
 352                         }
 353
 354                         #region Overrides of BoxedExpression
 355                         public override void AddFreeVariables (HashSet<BoxedExpression> set)
 356                         {
 357                                 this.Left.AddFreeVariables (set);
 358                                 this.Right.AddFreeVariables (set);
 359                         }
 360
 361                         protected internal override BoxedExpression RecursiveSubstitute (BoxedExpression what, BoxedExpression replace)
 362                         {
 363                                 BoxedExpression left = this.Left.Substitute (what, replace);
 364                                 BoxedExpression right = this.Right.Substitute (what, replace);
 365                                 if (left == this.Left && right == this.Right)
 366                                         return this;
 367
 368                                 return new BinaryExpression (this.Op, left, right);
 369                         }
 370
 371                         public override BoxedExpression Substitute<Variable> (Func<Variable, BoxedExpression, BoxedExpression> map)
 372                         {
 373                                 BoxedExpression left = this.Left.Substitute (map);
 374                                 if (left == null)
 375                                         return null;
 376
 377                                 BoxedExpression right = this.Right.Substitute (map);
 378                                 if (right == null)
 379                                         return null;
 380
 381                                 if (this.Left == left && this.Right == right)
 382                                         return this;
 383                                 return new BinaryExpression (this.Op, left, right);
 384                         }
 385
 386                         public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
 387                         {
 388                                 return visitor.Binary (pc, this.Op, Dummy.Value, Dummy.Value, Dummy.Value, data);
 389                         }
 390                         #endregion
 391                 }
 392                 #endregion
 393
 394                 #region Nested type: CastExpression
 395                 public class CastExpression : BoxedExpression {
 396                         public readonly TypeNode CastToType;
 397                         public readonly BoxedExpression Expr;
 398
 399                         public CastExpression (TypeNode castToType, BoxedExpression expr)
 400                         {
 401                                 this.CastToType = castToType;
 402                                 this.Expr = expr;
 403                         }
 404
 405                         public override bool IsCast
 406                         {
 407                                 get { return true; }
 408                         }
 409
 410                         public override PathElement[] AccessPath
 411                         {
 412                                 get { return this.Expr.AccessPath; }
 413                         }
 414
 415                         public override BoxedExpression BinaryLeftArgument
 416                         {
 417                                 get { return this.Expr.BinaryLeftArgument; }
 418                         }
 419
 420                         public override BoxedExpression BinaryRightArgument
 421                         {
 422                                 get { return this.Expr.BinaryRightArgument; }
 423                         }
 424
 425                         public override BinaryOperator BinaryOperator
 426                         {
 427                                 get { return this.Expr.BinaryOperator; }
 428                         }
 429
 430                         public override object Constant
 431                         {
 432                                 get { return this.Expr.Constant; }
 433                         }
 434
 435                         public override object ConstantType
 436                         {
 437                                 get { return this.Expr.ConstantType; }
 438                         }
 439
 440                         public override bool IsBinary
 441                         {
 442                                 get { return this.Expr.IsBinary; }
 443                         }
 444
 445                         public override bool IsBooleanTyped
 446                         {
 447                                 get { return this.Expr.IsBooleanTyped; }
 448                         }
 449
 450                         public override bool IsConstant
 451                         {
 452                                 get { return this.Expr.IsConstant; }
 453                         }
 454
 455
 456                         public override bool IsSizeof
 457                         {
 458                                 get { return this.Expr.IsSizeof; }
 459                         }
 460
 461                         public override bool IsNull
 462                         {
 463                                 get { return this.Expr.IsNull; }
 464                         }
 465
 466                         public override bool IsIsinst
 467                         {
 468                                 get { return this.Expr.IsIsinst; }
 469                         }
 470
 471                         public override bool IsResult
 472                         {
 473                                 get { return this.Expr.IsResult; }
 474                         }
 475
 476                         public override bool IsUnary
 477                         {
 478                                 get { return this.Expr.IsUnary; }
 479                         }
 480
 481                         public override bool IsVariable
 482                         {
 483                                 get { return this.Expr.IsVariable; }
 484                         }
 485
 486                         public override BoxedExpression UnaryArgument
 487                         {
 488                                 get { return this.Expr.UnaryArgument; }
 489                         }
 490
 491                         public override UnaryOperator UnaryOperator
 492                         {
 493                                 get { return this.Expr.UnaryOperator; }
 494                         }
 495
 496                         public override object UnderlyingVariable
 497                         {
 498                                 get { return this.Expr.UnderlyingVariable; }
 499                         }
 500
 501
 502                         public override void AddFreeVariables (HashSet<BoxedExpression> set)
 503                         {
 504                                 this.Expr.AddFreeVariables (set);
 505                         }
 506
 507                         public override BoxedExpression Substitute<Variable> (Func<Variable, BoxedExpression, BoxedExpression> map)
 508                         {
 509                                 return this.Expr.Substitute (map);
 510                         }
 511
 512                         public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
 513                         {
 514                                 return this.Expr.ForwardDecode<Data, Result, Visitor> (pc, visitor, data);
 515                         }
 516
 517                         public override bool IsBinaryExpression (out BinaryOperator op, out BoxedExpression left, out BoxedExpression right)
 518                         {
 519                                 return this.Expr.IsBinaryExpression (out op, out left, out right);
 520                         }
 521
 522                         protected internal override BoxedExpression RecursiveSubstitute (BoxedExpression what, BoxedExpression replace)
 523                         {
 524                                 return this.Expr.RecursiveSubstitute (what, replace);
 525                         }
 526
 527                         public override BoxedExpression Substitute (BoxedExpression what, BoxedExpression replace)
 528                         {
 529                                 return this.Expr.Substitute (what, replace);
 530                         }
 531
 532                         public override bool IsUnaryExpression (out UnaryOperator op, out BoxedExpression argument)
 533                         {
 534                                 return this.Expr.IsUnaryExpression (out op, out argument);
 535                         }
 536                 }
 537                 #endregion
 538
 539                 #region Nested type: ConstantExpression
 540                 public class ConstantExpression : BoxedExpression {
 541                         public readonly TypeNode Type;
 542                         public readonly object Value;
 543                         private readonly bool is_boolean;
 544
 545                         public ConstantExpression (object value, TypeNode type)
 546                                 : this (value, type, false)
 547                         {
 548                         }
 549
 550                         public ConstantExpression (object value, TypeNode type, bool isBoolean)
 551                         {
 552                                 this.Value = value;
 553                                 this.Type = type;
 554                                 this.is_boolean = isBoolean;
 555                         }
 556
 557                         public override bool IsBooleanTyped
 558                         {
 559                                 get { return this.is_boolean; }
 560                         }
 561
 562                         public override bool IsConstant
 563                         {
 564                                 get { return true; }
 565                         }
 566
 567                         public override object Constant
 568                         {
 569                                 get { return this.Value; }
 570                         }
 571
 572                         public override object ConstantType
 573                         {
 574                                 get { return this.Type; }
 575                         }
 576
 577                         public override bool IsNull
 578                         {
 579                                 get
 580                                 {
 581                                         if (this.Value == null)
 582                                                 return true;
 583
 584                                         var conv = this.Value as IConvertible;
 585                                         if (conv != null) {
 586                                                 try {
 587                                                         if (conv.ToInt32 (null) == 0)
 588                                                                 return true;
 589                                                 } catch {
 590                                                         return false;
 591                                                 }
 592                                         }
 593
 594                                         return false;
 595                                 }
 596                         }
 597
 598                         public override void AddFreeVariables (HashSet<BoxedExpression> set)
 599                         {
 600                         }
 601
 602                         public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
 603                         {
 604                                 return this;
 605                         }
 606
 607                         public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
 608                         {
 609                                 if (this.Value == null)
 610                                         return visitor.LoadNull (pc, Dummy.Value, data);
 611
 612                                 return visitor.LoadConst (pc, this.Type, this.Value, Dummy.Value, data);
 613                         }
 614                 }
 615                 #endregion
 616
 617                 #region Nested type: ContractExpression
 618                 public abstract class ContractExpression : BoxedExpression {
 619                         public readonly APC Apc;
 620                         public readonly BoxedExpression Condition;
 621                         public readonly EdgeTag Tag;
 622
 623                         public ContractExpression (BoxedExpression condition, EdgeTag tag, APC pc)
 624                         {
 625                                 this.Tag = tag;
 626                                 this.Condition = condition;
 627                                 this.Apc = pc;
 628                         }
 629
 630                         public override void AddFreeVariables (HashSet<BoxedExpression> set)
 631                         {
 632                                 this.Condition.AddFreeVariables (set);
 633                         }
 634
 635                         public abstract override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data);
 636                         public abstract override BoxedExpression Substitute<Variable> (Func<Variable, BoxedExpression, BoxedExpression> map);
 637                 }
 638                 #endregion
 639
 640                 #region Nested type: ExternalBox
 641                 public class ExternalBox<Variable, LabeledSymbol> : BoxedExpression
 642                         where LabeledSymbol : IEquatable<LabeledSymbol> {
 643                         private readonly IFullExpressionDecoder<Variable, LabeledSymbol> decoder;
 644                         private readonly LabeledSymbol expr;
 645                         private Optional<Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression>> binary;
 646
 647                         private Optional<Tuple<bool, object, TypeNode>> constant;
 648                         private Optional<Tuple<bool, BoxedExpression, TypeNode>> isInst;
 649                         private Optional<Pair<bool, object>> isVar;
 650                         private Optional<Pair<bool, TypeNode>> type;
 651                         private Optional<Tuple<bool, UnaryOperator, BoxedExpression>> unary;
 652                         private Optional<object> var;
 653
 654                         public ExternalBox (LabeledSymbol external, IFullExpressionDecoder<Variable, LabeledSymbol> decoder)
 655                         {
 656                                 this.expr = external;
 657                                 this.decoder = decoder;
 658                         }
 659
 660                         public override bool IsBinary
 661                         {
 662                                 get
 663                                 {
 664                                         Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> binary;
 665                                         TryGetBinaryFromCache (out binary);
 666                                         return binary.Item1;
 667                                 }
 668                         }
 669
 670                         public override BinaryOperator BinaryOperator
 671                         {
 672                                 get
 673                                 {
 674                                         Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> binary;
 675                                         bool res = TryGetBinaryFromCache (out binary);
 676                                         if (!res)
 677                                                 throw new InvalidOperationException ();
 678
 679                                         return binary.Item2;
 680                                 }
 681                         }
 682
 683                         public override BoxedExpression BinaryLeftArgument
 684                         {
 685                                 get
 686                                 {
 687                                         Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> binary;
 688                                         bool res = TryGetBinaryFromCache (out binary);
 689                                         if (!res)
 690                                                 throw new InvalidOperationException ();
 691
 692                                         return binary.Item3;
 693                                 }
 694                         }
 695
 696                         public override BoxedExpression BinaryRightArgument
 697                         {
 698                                 get
 699                                 {
 700                                         Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> binary;
 701                                         bool res = TryGetBinaryFromCache (out binary);
 702                                         if (!res)
 703                                                 throw new InvalidOperationException ();
 704
 705                                         return binary.Item4;
 706                                 }
 707                         }
 708
 709                         public override bool IsConstant
 710                         {
 711                                 get
 712                                 {
 713                                         Tuple<bool, object, TypeNode> consta;
 714                                         TryGetConstantFromCache (out consta);
 715
 716                                         return consta.Item1;
 717                                 }
 718                         }
 719
 720                         public override object Constant
 721                         {
 722                                 get
 723                                 {
 724                                         Tuple<bool, object, TypeNode> consta;
 725                                         if (!TryGetConstantFromCache (out consta))
 726                                                 throw new InvalidOperationException ();
 727
 728                                         return consta.Item2;
 729                                 }
 730                         }
 731
 732                         public override object ConstantType
 733                         {
 734                                 get
 735                                 {
 736                                         Tuple<bool, object, TypeNode> consta;
 737                                         if (!TryGetConstantFromCache (out consta))
 738                                                 throw new InvalidOperationException();
 739
 740                                         return consta.Item3;
 741                                 }
 742                         }
 743
 744                         public override bool IsIsinst
 745                         {
 746                                 get
 747                                 {
 748                                         Tuple<bool, BoxedExpression, TypeNode> isinst;
 749                                         TryGetIsInstFromCache (out isinst);
 750                                         return isinst.Item1;
 751                                 }
 752                         }
 753
 754                         public override bool IsNull
 755                         {
 756                                 get { return this.decoder.IsNull (this.expr); }
 757                         }
 758
 759                         public override bool IsUnary
 760                         {
 761                                 get
 762                                 {
 763                                         Tuple<bool, UnaryOperator, BoxedExpression> unary;
 764                                         TryGetUnaryFromCache (out unary);
 765                                         return unary.Item1;
 766                                 }
 767                         }
 768
 769                         public override UnaryOperator UnaryOperator
 770                         {
 771                                 get
 772                                 {
 773                                         Tuple<bool, UnaryOperator, BoxedExpression> unary;
 774                                         if (!TryGetUnaryFromCache (out unary))
 775                                                 throw new InvalidOperationException();
 776                                         return unary.Item2;
 777                                 }
 778                         }
 779
 780                         public override BoxedExpression UnaryArgument
 781                         {
 782                                 get
 783                                 {
 784                                         Tuple<bool, UnaryOperator, BoxedExpression> unary;
 785                                         if (!TryGetUnaryFromCache (out unary))
 786                                                 throw new InvalidOperationException ();
 787                                         return unary.Item3;
 788                                 }
 789                         }
 790
 791                         public override bool IsSizeof
 792                         {
 793                                 get
 794                                 {
 795                                         TypeNode type;
 796                                         return this.decoder.IsSizeof (this.expr, out type);
 797                                 }
 798                         }
 799
 800                         public override bool IsVariable
 801                         {
 802                                 get
 803                                 {
 804                                         Pair<bool, object> var1;
 805                                         TryGetIsVariableFromCache (out var1);
 806                                         return var1.Key;
 807                                 }
 808                         }
 809
 810                         public override object UnderlyingVariable
 811                         {
 812                                 get
 813                                 {
 814                                         if (!this.var.IsValid)
 815                                                 this.var = this.decoder.UnderlyingVariable (this.expr);
 816
 817                                         return this.var.Value;
 818                                 }
 819                         }
 820
 821                         private bool TryGetBinaryFromCache (out Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> binary)
 822                         {
 823                                 if (this.binary.IsValid) {
 824                                         binary = this.binary.Value;
 825                                         return true;
 826                                 }
 827                                 BinaryOperator op;
 828                                 LabeledSymbol left;
 829                                 LabeledSymbol right;
 830                                 bool res = this.decoder.IsBinaryExpression (this.expr, out op, out left, out right);
 831                                 this.binary = binary = new Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> (res, op, For (left, this.decoder), For (right, this.decoder));
 832
 833                                 return res;
 834                         }
 835
 836                         private bool TryGetUnaryFromCache (out Tuple<bool, UnaryOperator, BoxedExpression> unary)
 837                         {
 838                                 if (this.unary.IsValid) {
 839                                         unary = this.unary.Value;
 840                                         return true;
 841                                 }
 842                                 UnaryOperator op;
 843                                 LabeledSymbol arg;
 844                                 bool res = this.decoder.IsUnaryExpression (this.expr, out op, out arg);
 845                                 this.unary = unary = new Tuple<bool, UnaryOperator, BoxedExpression> (res, op, For (arg, this.decoder));
 846
 847                                 return res;
 848                         }
 849
 850                         private bool TryGetIsInstFromCache (out Tuple<bool, BoxedExpression, TypeNode> isinst)
 851                         {
 852                                 if (this.isInst.IsValid) {
 853                                         isinst = this.isInst.Value;
 854                                         return true;
 855                                 }
 856
 857                                 LabeledSymbol arg;
 858                                 TypeNode type;
 859                                 bool res = this.decoder.IsIsinst (this.expr, out arg, out type);
 860                                 this.isInst = isinst = new Tuple<bool, BoxedExpression, TypeNode> (res, For (arg, this.decoder), type);
 861
 862                                 return res;
 863                         }
 864
 865                         private bool TryGetConstantFromCache (out Tuple<bool, object, TypeNode> result)
 866                         {
 867                                 if (this.constant.IsValid) {
 868                                         result = this.constant.Value;
 869                                         return true;
 870                                 }
 871                                 object value;
 872                                 TypeNode type;
 873                                 bool res = this.decoder.IsConstant (this.expr, out value, out type);
 874                                 this.constant = result = new Tuple<bool, object, TypeNode> (res, value, type);
 875
 876                                 return res;
 877                         }
 878
 879                         private bool TryGetTypeFromCache (out Pair<bool, TypeNode> result)
 880                         {
 881                                 if (this.type.IsValid) {
 882                                         result = this.type.Value;
 883                                         return true;
 884                                 }
 885
 886                                 TypeNode type;
 887                                 bool res = this.decoder.TryGetType (this.expr, out type);
 888                                 this.type = result = new Pair<bool, TypeNode> (res, type);
 889
 890                                 return res;
 891                         }
 892
 893                         private bool TryGetIsVariableFromCache (out Pair<bool, object> result)
 894                         {
 895                                 if (this.isVar.IsValid) {
 896                                         result = this.isVar.Value;
 897                                         return true;
 898                                 }
 899
 900                                 object value;
 901                                 bool res = this.decoder.IsVariable (this.expr, out value);
 902                                 this.isVar = result = new Pair<bool, object> (res, value);
 903
 904                                 return res;
 905                         }
 906
 907                         public override bool IsBinaryExpression (out BinaryOperator op, out BoxedExpression left, out BoxedExpression right)
 908                         {
 909                                 Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> bin;
 910                                 if (!TryGetBinaryFromCache (out bin) || !bin.Item1) {
 911                                         op = BinaryOperator.Add;
 912                                         left = null;
 913                                         right = null;
 914                                         return false;
 915                                 }
 916
 917                                 op = bin.Item2;
 918                                 left = bin.Item3;
 919                                 right = bin.Item4;
 920                                 return true;
 921                         }
 922
 923                         public override bool IsIsinstExpression (out BoxedExpression expr, out TypeNode type)
 924                         {
 925                                 Tuple<bool, BoxedExpression, TypeNode> isinst;
 926                                 if (!TryGetIsInstFromCache (out isinst) || !isinst.Item1) {
 927                                         expr = null;
 928                                         type = null;
 929                                         return false;
 930                                 }
 931
 932                                 expr = isinst.Item2;
 933                                 type = isinst.Item3;
 934                                 return true;
 935                         }
 936
 937                         public override bool IsUnaryExpression (out UnaryOperator op, out BoxedExpression argument)
 938                         {
 939                                 Tuple<bool, UnaryOperator, BoxedExpression> unary;
 940                                 if (!TryGetUnaryFromCache (out unary) || !unary.Item1) {
 941                                         op = UnaryOperator.Conv_i;
 942                                         argument = null;
 943                                         return false;
 944                                 }
 945
 946                                 op = unary.Item2;
 947                                 argument = unary.Item3;
 948                                 return true;
 949                         }
 950
 951                         protected internal override BoxedExpression RecursiveSubstitute (BoxedExpression what, BoxedExpression replace)
 952                         {
 953                                 return Convert (this.expr, this.decoder).Substitute (what, replace);
 954                         }
 955
 956                         public override void AddFreeVariables (HashSet<BoxedExpression> set)
 957                         {
 958                                 this.decoder.AddFreeVariables (this.expr, new SetWrapper (set, this.decoder));
 959                         }
 960
 961                         public override BoxedExpression Substitute<V> (Func<V, BoxedExpression, BoxedExpression> map)
 962                         {
 963                                 return Convert (this.expr, this.decoder).Substitute (map);
 964                         }
 965
 966                         public override bool TryGetType (out object type)
 967                         {
 968                                 Pair<bool, TypeNode> result;
 969                                 if (!TryGetTypeFromCache (out result) || !result.Key) {
 970                                         type = null;
 971                                         return false;
 972                                 }
 973
 974                                 type = result.Value;
 975                                 return true;
 976                         }
 977
 978                         public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
 979                         {
 980                                 Tuple<bool, object, TypeNode> constant;
 981                                 if (TryGetConstantFromCache (out constant)) {
 982                                         if (constant.Item2 != null)
 983                                                 return visitor.LoadConst (pc, constant.Item3, constant, Dummy.Value, data);
 984
 985                                         return visitor.LoadNull (pc, Dummy.Value, data);
 986                                 }
 987
 988                                 UnaryOperator op;
 989                                 LabeledSymbol arg;
 990                                 if (this.decoder.IsUnaryExpression (this.expr, out op, out arg))
 991                                         return visitor.Unary (pc, op, false, Dummy.Value, Dummy.Value, data);
 992
 993                                 BinaryOperator bop;
 994                                 LabeledSymbol left;
 995                                 LabeledSymbol right;
 996                                 if (this.decoder.IsBinaryExpression (this.expr, out bop, out left, out right))
 997                                         return visitor.Binary (pc, bop, Dummy.Value, Dummy.Value, Dummy.Value, data);
 998                                 TypeNode type;
 999                                 if (this.decoder.IsIsinst (this.expr, out arg, out type))
1000                                         return visitor.Isinst (pc, type, Dummy.Value, Dummy.Value, data);
1001                                 if (this.decoder.IsNull (this.expr))
1002                                         return visitor.LoadNull (pc, Dummy.Value, data);
1003                                 if (this.decoder.IsSizeof (this.expr, out type))
1004                                         return visitor.Sizeof (pc, type, Dummy.Value, data);
1005
1006                                 return visitor.Nop (pc, data);
1007                         }
1008
1009                         #region Nested type: SetWrapper
1010                         private struct SetWrapper : ISet<LabeledSymbol>, IEnumerable<LabeledSymbol> {
1011                                 private readonly IFullExpressionDecoder<Variable, LabeledSymbol> decoder;
1012                                 private readonly HashSet<BoxedExpression> set;
1013
1014                                 #region Implementation of IEnumerable
1015                                 public IEnumerator<LabeledSymbol> GetEnumerator ()
1016                                 {
1017                                         throw new NotImplementedException ();
1018                                 }
1019
1020                                 IEnumerator IEnumerable.GetEnumerator ()
1021                                 {
1022                                         return GetEnumerator ();
1023                                 }
1024                                 #endregion
1025
1026                                 public SetWrapper (HashSet<BoxedExpression> set, IFullExpressionDecoder<Variable, LabeledSymbol> decoder)
1027                                 {
1028                                         this.set = set;
1029                                         this.decoder = decoder;
1030                                 }
1031
1032                                 #region Implementation of ICollection<ExternalExpression>
1033                                 public void Add (LabeledSymbol item)
1034                                 {
1035                                         this.set.Add (For (item, this.decoder));
1036                                 }
1037
1038                                 bool ISet<LabeledSymbol>.Add (LabeledSymbol item)
1039                                 {
1040                                         Add (item);
1041                                         return true;
1042                                 }
1043
1044                                 public void UnionWith (IEnumerable<LabeledSymbol> other)
1045                                 {
1046                                         throw new NotImplementedException ();
1047                                 }
1048
1049                                 public void IntersectWith (IEnumerable<LabeledSymbol> other)
1050                                 {
1051                                         throw new NotImplementedException ();
1052                                 }
1053
1054                                 public void ExceptWith (IEnumerable<LabeledSymbol> other)
1055                                 {
1056                                         throw new NotImplementedException ();
1057                                 }
1058
1059                                 public void SymmetricExceptWith (IEnumerable<LabeledSymbol> other)
1060                                 {
1061                                         throw new NotImplementedException ();
1062                                 }
1063
1064                                 public bool IsSubsetOf (IEnumerable<LabeledSymbol> other)
1065                                 {
1066                                         throw new NotImplementedException ();
1067                                 }
1068
1069                                 public bool IsSupersetOf (IEnumerable<LabeledSymbol> other)
1070                                 {
1071                                         throw new NotImplementedException ();
1072                                 }
1073
1074                                 public bool IsProperSupersetOf (IEnumerable<LabeledSymbol> other)
1075                                 {
1076                                         throw new NotImplementedException ();
1077                                 }
1078
1079                                 public bool IsProperSubsetOf (IEnumerable<LabeledSymbol> other)
1080                                 {
1081                                         throw new NotImplementedException ();
1082                                 }
1083
1084                                 public bool Overlaps (IEnumerable<LabeledSymbol> other)
1085                                 {
1086                                         throw new NotImplementedException ();
1087                                 }
1088
1089                                 public bool SetEquals (IEnumerable<LabeledSymbol> other)
1090                                 {
1091                                         throw new NotImplementedException ();
1092                                 }
1093
1094
1095                                 public void Clear ()
1096                                 {
1097                                         throw new NotImplementedException ();
1098                                 }
1099
1100                                 public bool Contains (LabeledSymbol item)
1101                                 {
1102                                         throw new NotImplementedException ();
1103                                 }
1104
1105                                 public void CopyTo (LabeledSymbol[] array, int arrayIndex)
1106                                 {
1107                                         throw new NotImplementedException ();
1108                                 }
1109
1110                                 public bool Remove (LabeledSymbol item)
1111                                 {
1112                                         throw new NotImplementedException ();
1113                                 }
1114
1115                                 public int Count
1116                                 {
1117                                         get { throw new NotImplementedException (); }
1118                                 }
1119
1120                                 public bool IsReadOnly
1121                                 {
1122                                         get { throw new NotImplementedException (); }
1123                                 }
1124                                 #endregion
1125                         }
1126                         #endregion
1127                         }
1128                 #endregion
1129
1130                 #region Nested type: IsinstExpression
1131                 public class IsinstExpression : BoxedExpression {
1132                         private readonly BoxedExpression arg;
1133                         private readonly TypeNode type;
1134
1135                         public IsinstExpression (BoxedExpression boxedExpression, TypeNode type)
1136                         {
1137                                 this.arg = boxedExpression;
1138                                 this.type = type;
1139                         }
1140
1141                         public override bool IsIsinst
1142                         {
1143                                 get { return true; }
1144                         }
1145
1146                         public override BoxedExpression UnaryArgument
1147                         {
1148                                 get { return this.arg; }
1149                         }
1150
1151                         public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
1152                         {
1153                                 return visitor.Isinst (pc, this.type, Dummy.Value, Dummy.Value, data);
1154                         }
1155
1156                         public override void AddFreeVariables (HashSet<BoxedExpression> set)
1157                         {
1158                                 this.arg.AddFreeVariables (set);
1159                         }
1160
1161                         public override BoxedExpression Substitute<Variable> (Func<Variable, BoxedExpression, BoxedExpression> map)
1162                         {
1163                                 BoxedExpression arg = this.arg.Substitute (map);
1164                                 if (arg == this.arg)
1165                                         return this;
1166                                 if (arg == null)
1167                                         return null;
1168
1169                                 return new IsinstExpression (arg, this.type);
1170                         }
1171                 }
1172                 #endregion
1173
1174                 #region Nested type: OldExpression
1175                 public class OldExpression : BoxedExpression {
1176                         private const string ContractOldValueTemplate = "Contract.OldValue({0})";
1177
1178                         public readonly BoxedExpression Old;
1179                         public readonly TypeNode Type;
1180
1181                         public OldExpression (BoxedExpression old, TypeNode type)
1182                         {
1183                                 this.Old = old;
1184                                 this.Type = type;
1185                         }
1186
1187                         #region Overrides of BoxedExpression
1188                         public override void AddFreeVariables (HashSet<BoxedExpression> set)
1189                         {
1190                                 this.Old.AddFreeVariables (set);
1191                         }
1192
1193                         public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
1194                         {
1195                                 BoxedExpression old = this.Old.Substitute (map);
1196                                 if (old == this.Old)
1197                                         return this;
1198                                 if (old == null)
1199                                         return null;
1200
1201                                 return new OldExpression (old, this.Type);
1202                         }
1203
1204                         public override bool IsBinaryExpression (out BinaryOperator op, out BoxedExpression left, out BoxedExpression right)
1205                         {
1206                                 return this.Old.IsBinaryExpression (out op, out left, out right);
1207                         }
1208
1209                         public override bool IsUnaryExpression (out UnaryOperator op, out BoxedExpression argument)
1210                         {
1211                                 return this.Old.IsUnaryExpression (out op, out argument);
1212                         }
1213
1214                         public override bool IsIsinstExpression (out BoxedExpression expr, out TypeNode type)
1215                         {
1216                                 return this.Old.IsIsinstExpression (out expr, out type);
1217                         }
1218
1219                         public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
1220                         {
1221                                 return visitor.EndOld (pc, new PC (pc.Node, 0), this.Type, Dummy.Value, Dummy.Value, data);
1222                         }
1223                         #endregion
1224
1225                         public override PathElement[] AccessPath
1226                         {
1227                                 get { return this.Old.AccessPath; }
1228                         }
1229
1230                         public override BoxedExpression BinaryLeftArgument
1231                         {
1232                                 get { return this.Old.BinaryLeftArgument; }
1233                         }
1234
1235                         public override BoxedExpression BinaryRightArgument
1236                         {
1237                                 get { return this.Old.BinaryRightArgument; }
1238                         }
1239
1240                         public override BinaryOperator BinaryOperator
1241                         {
1242                                 get { return this.Old.BinaryOperator; }
1243                         }
1244
1245                         public override object Constant
1246                         {
1247                                 get { return this.Old.Constant; }
1248                         }
1249
1250                         public override object ConstantType
1251                         {
1252                                 get { return this.Old.ConstantType; }
1253                         }
1254
1255                         public override bool IsBinary
1256                         {
1257                                 get { return this.Old.IsBinary; }
1258                         }
1259
1260                         public override bool IsConstant
1261                         {
1262                                 get { return this.Old.IsConstant; }
1263                         }
1264
1265                         public override bool IsSizeof
1266                         {
1267                                 get { return this.Old.IsSizeof; }
1268                         }
1269
1270                         public override bool IsNull
1271                         {
1272                                 get { return this.Old.IsNull; }
1273                         }
1274
1275                         public override bool IsIsinst
1276                         {
1277                                 get { return this.Old.IsIsinst; }
1278                         }
1279
1280                         public override bool IsUnary
1281                         {
1282                                 get { return this.Old.IsUnary; }
1283                         }
1284
1285                         public override bool IsVariable
1286                         {
1287                                 get { return this.Old.IsVariable; }
1288                         }
1289
1290                         public override BoxedExpression UnaryArgument
1291                         {
1292                                 get { return this.Old.UnaryArgument; }
1293                         }
1294
1295                         public override UnaryOperator UnaryOperator
1296                         {
1297                                 get { return this.Old.UnaryOperator; }
1298                         }
1299
1300                         public override object UnderlyingVariable
1301                         {
1302                                 get { return this.Old.UnderlyingVariable; }
1303                         }
1304                 }
1305                 #endregion
1306
1307                 #region Nested type: PC
1308                 public struct PC {
1309                         public readonly int Index;
1310                         public readonly BoxedExpression Node;
1311
1312                         public PC (BoxedExpression expr, int index)
1313                         {
1314                                 this.Node = expr;
1315                                 this.Index = index;
1316                         }
1317                 }
1318                 #endregion
1319
1320                 #region Nested type: ResultExpression
1321                 public class ResultExpression : BoxedExpression {
1322                         private const string ContractResultTemplate = "Contract.Result<{0}>()";
1323
1324                         public readonly TypeNode Type;
1325
1326                         public ResultExpression (TypeNode type)
1327                         {
1328                                 this.Type = type;
1329                         }
1330
1331                         public override bool IsResult
1332                         {
1333                                 get { return true; }
1334                         }
1335
1336                         public override void AddFreeVariables (HashSet<BoxedExpression> set)
1337                         {
1338                         }
1339
1340                         public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
1341                         {
1342                                 return this;
1343                         }
1344
1345                         public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
1346                         {
1347                                 return visitor.LoadResult (pc, this.Type, Dummy.Value, Dummy.Value, data);
1348                         }
1349                 }
1350                 #endregion
1351
1352                 #region Nested type: SizeOfExpression
1353                 public class SizeOfExpression : BoxedExpression {
1354                         public readonly int SizeAsConstant;
1355                         public readonly TypeNode Type;
1356
1357                         public SizeOfExpression (TypeNode type, int sizeAsConstant)
1358                         {
1359                                 this.Type = type;
1360                                 this.SizeAsConstant = sizeAsConstant;
1361                         }
1362
1363                         public SizeOfExpression (TypeNode type)
1364                                 : this (type, -1)
1365                         {
1366                         }
1367
1368                         public override bool IsSizeof
1369                         {
1370                                 get { return true; }
1371                         }
1372
1373                         public override bool Sizeof (out int size)
1374                         {
1375                                 size = SizeAsConstant;
1376                                 return size >= 0;
1377                         }
1378
1379                         public override void AddFreeVariables (HashSet<BoxedExpression> set)
1380                         {
1381                         }
1382
1383                         public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
1384                         {
1385                                 return this;
1386                         }
1387
1388                         public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
1389                         {
1390                                 return visitor.Sizeof (pc, this.Type, Dummy.Value, data);
1391                         }
1392                 }
1393                 #endregion
1394
1395                 #region Nested type: UnaryExpression
1396                 public class UnaryExpression : BoxedExpression {
1397                         public readonly BoxedExpression Argument;
1398                         public readonly UnaryOperator Op;
1399
1400                         public UnaryExpression (UnaryOperator op, BoxedExpression argument)
1401                         {
1402                                 this.Op = op;
1403                                 this.Argument = argument;
1404                         }
1405
1406                         public override bool IsUnary
1407                         {
1408                                 get { return true; }
1409                         }
1410
1411                         public override BoxedExpression UnaryArgument
1412                         {
1413                                 get { return this.Argument; }
1414                         }
1415
1416                         public override UnaryOperator UnaryOperator
1417                         {
1418                                 get { return this.Op; }
1419                         }
1420
1421                         public override bool IsUnaryExpression (out UnaryOperator op, out BoxedExpression argument)
1422                         {
1423                                 op = this.Op;
1424                                 argument = this.Argument;
1425                                 return true;
1426                         }
1427
1428                         public override void AddFreeVariables (HashSet<BoxedExpression> set)
1429                         {
1430                                 this.Argument.AddFreeVariables (set);
1431                         }
1432
1433                         public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
1434                         {
1435                                 BoxedExpression argument = this.Argument.Substitute (map);
1436                                 if (argument == this.Argument)
1437                                         return this;
1438                                 if (argument == null)
1439                                         return null;
1440
1441                                 return new UnaryExpression (this.Op, argument);
1442                         }
1443
1444                         protected internal override BoxedExpression RecursiveSubstitute (BoxedExpression what, BoxedExpression replace)
1445                         {
1446                                 BoxedExpression argument = this.Argument.Substitute (what, replace);
1447
1448                                 if (argument == this.Argument)
1449                                         return this;
1450
1451                                 return new UnaryExpression (this.Op, argument);
1452                         }
1453
1454                         public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
1455                         {
1456                                 return visitor.Unary (pc, this.Op, false, Dummy.Value, Dummy.Value, data);
1457                         }
1458
1459                         public override bool Equals (object obj)
1460                         {
1461                                 if (this == obj)
1462                                         return true;
1463
1464                                 var unary = obj as UnaryExpression;
1465                                 return unary != null && this.Op == unary.Op && this.Argument.Equals (unary.Argument);
1466                         }
1467
1468                         public override int GetHashCode ()
1469                         {
1470                                 return this.Op.GetHashCode () * 13 + (this.Argument == null ? 0 : this.Argument.GetHashCode ());
1471                         }
1472
1473                 }
1474                 #endregion
1475
1476                 #region Nested type: ValueAtReturnExpression
1477                 public class ValueAtReturnExpression : BoxedExpression {
1478                         private const string ContractValueAtReturnTemplate = "Contract.ValueAtReturn({0})";
1479
1480                         public readonly TypeNode Type;
1481                         public readonly BoxedExpression Value;
1482
1483                         public ValueAtReturnExpression (BoxedExpression old, TypeNode type)
1484                         {
1485                                 this.Value = old;
1486                                 this.Type = type;
1487                         }
1488
1489                         #region Overrides of BoxedExpression
1490                         public override void AddFreeVariables (HashSet<BoxedExpression> set)
1491                         {
1492                                 this.Value.AddFreeVariables (set);
1493                         }
1494
1495                         public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
1496                         {
1497                                 BoxedExpression value = this.Value.Substitute (map);
1498                                 if (value == this.Value)
1499                                         return this;
1500                                 if (value == null)
1501                                         return null;
1502
1503                                 return new ValueAtReturnExpression (value, this.Type);
1504                         }
1505
1506                         public override bool IsBinaryExpression (out BinaryOperator op, out BoxedExpression left, out BoxedExpression right)
1507                         {
1508                                 return this.Value.IsBinaryExpression (out op, out left, out right);
1509                         }
1510
1511                         public override bool IsUnaryExpression (out UnaryOperator op, out BoxedExpression argument)
1512                         {
1513                                 return this.Value.IsUnaryExpression (out op, out argument);
1514                         }
1515
1516                         public override bool IsIsinstExpression (out BoxedExpression expr, out TypeNode type)
1517                         {
1518                                 return this.Value.IsIsinstExpression (out expr, out type);
1519                         }
1520
1521                         public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
1522                         {
1523                                 throw new NotImplementedException ();
1524                         }
1525                         #endregion
1526
1527                         public override PathElement[] AccessPath
1528                         {
1529                                 get { return this.Value.AccessPath; }
1530                         }
1531
1532                         public override BoxedExpression BinaryLeftArgument
1533                         {
1534                                 get { return this.Value.BinaryLeftArgument; }
1535                         }
1536
1537                         public override BoxedExpression BinaryRightArgument
1538                         {
1539                                 get { return this.Value.BinaryRightArgument; }
1540                         }
1541
1542                         public override BinaryOperator BinaryOperator
1543                         {
1544                                 get { return this.Value.BinaryOperator; }
1545                         }
1546
1547                         public override object Constant
1548                         {
1549                                 get { return this.Value.Constant; }
1550                         }
1551
1552                         public override object ConstantType
1553                         {
1554                                 get { return this.Value.ConstantType; }
1555                         }
1556
1557                         public override bool IsBinary
1558                         {
1559                                 get { return this.Value.IsBinary; }
1560                         }
1561
1562                         public override bool IsConstant
1563                         {
1564                                 get { return this.Value.IsConstant; }
1565                         }
1566
1567                         public override bool IsSizeof
1568                         {
1569                                 get { return this.Value.IsSizeof; }
1570                         }
1571
1572                         public override bool IsNull
1573                         {
1574                                 get { return this.Value.IsNull; }
1575                         }
1576
1577                         public override bool IsIsinst
1578                         {
1579                                 get { return this.Value.IsIsinst; }
1580                         }
1581
1582                         public override bool IsUnary
1583                         {
1584                                 get { return this.Value.IsUnary; }
1585                         }
1586
1587                         public override bool IsVariable
1588                         {
1589                                 get { return this.Value.IsVariable; }
1590                         }
1591
1592                         public override BoxedExpression UnaryArgument
1593                         {
1594                                 get { return this.Value.UnaryArgument; }
1595                         }
1596
1597                         public override UnaryOperator UnaryOperator
1598                         {
1599                                 get { return this.Value.UnaryOperator; }
1600                         }
1601
1602                         public override object UnderlyingVariable
1603                         {
1604                                 get { return this.Value.UnderlyingVariable; }
1605                         }
1606                 }
1607                 #endregion
1608
1609                 #region Nested type: VariableExpression
1610                 public class VariableExpression : BoxedExpression {
1611                         private readonly PathElement[] Path;
1612                         private readonly object UnderlyingVar;
1613                         public readonly object VarType;
1614
1615                         public VariableExpression (object var)
1616                                 : this (var, (Sequence<PathElement>) null)
1617                         {
1618                         }
1619
1620                         public VariableExpression (object var, Sequence<PathElement> path)
1621                         {
1622                                 this.UnderlyingVar = var;
1623                                 this.Path = path != null ? path.AsEnumerable ().ToArray () : null;
1624                         }
1625
1626                         public VariableExpression (object var, Sequence<PathElement> path, object type)
1627                                 : this (var, path)
1628                         {
1629                                 this.VarType = type;
1630                         }
1631
1632                         public VariableExpression (object var, PathElement[] path)
1633                         {
1634                                 this.UnderlyingVar = var;
1635                                 this.Path = path;
1636                         }
1637
1638                         public VariableExpression (object var, PathElement[] path, object type)
1639                                 : this (var, path)
1640                         {
1641                                 this.VarType = type;
1642                         }
1643
1644                         public override bool IsVariable
1645                         {
1646                                 get { return true; }
1647                         }
1648
1649                         public override object UnderlyingVariable
1650                         {
1651                                 get { return this.UnderlyingVar; }
1652                         }
1653
1654                         public override PathElement[] AccessPath
1655                         {
1656                                 get { return this.Path; }
1657                         }
1658
1659                         public override bool IsBooleanTyped
1660                         {
1661                                 get { return this.Path != null && this.Path [this.Path.Length - 1].IsBooleanTyped; }
1662                         }
1663
1664                         public override bool TryGetType (out object type)
1665                         {
1666                                 type = this.VarType;
1667                                 return type != null;
1668                         }
1669
1670                         public override void AddFreeVariables (HashSet<BoxedExpression> set)
1671                         {
1672                                 set.Add (this);
1673                         }
1674
1675                         protected internal override BoxedExpression RecursiveSubstitute (BoxedExpression what, BoxedExpression replace)
1676                         {
1677                                 var varExpr = what as VariableExpression;
1678                                 if (varExpr != null && varExpr.UnderlyingVar.Equals (this.UnderlyingVar))
1679                                         return replace;
1680
1681                                 return this;
1682                         }
1683
1684                         public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
1685                         {
1686                                 return visitor.Nop (pc, data);
1687                         }
1688
1689                         public override bool Equals (object obj)
1690                         {
1691                                 if (this == obj)
1692                                         return true;
1693                                 var boxedExpression = obj as BoxedExpression;
1694                                 if (boxedExpression != null && boxedExpression.IsVariable)
1695                                         return this.UnderlyingVar.Equals (boxedExpression.UnderlyingVariable);
1696
1697                                 return false;
1698                         }
1699
1700                         public override int GetHashCode ()
1701                         {
1702                                 return this.UnderlyingVariable != null ? 0 : this.UnderlyingVariable.GetHashCode ();
1703                         }
1704
1705                         public override BoxedExpression Substitute<Variable> (Func<Variable, BoxedExpression, BoxedExpression> map)
1706                         {
1707                                 if (!(this.UnderlyingVar is Variable))
1708                                         return this;
1709                                 var variable = ((Variable) this.UnderlyingVar);
1710                                 return map (variable, this);
1711                         }
1712                 }
1713                 #endregion
1714         }
1715 }