1716 lines
42 KiB
C#
1716 lines
42 KiB
C#
//
|
|
// BoxedExpression.cs
|
|
//
|
|
// Authors:
|
|
// Alexander Chebaturkin (chebaturkin@gmail.com)
|
|
//
|
|
// Copyright (C) 2011 Alexander Chebaturkin
|
|
//
|
|
// Permission is hereby granted, free of charge, to any person obtaining
|
|
// a copy of this software and associated documentation files (the
|
|
// "Software"), to deal in the Software without restriction, including
|
|
// without limitation the rights to use, copy, modify, merge, publish,
|
|
// distribute, sublicense, and/or sell copies of the Software, and to
|
|
// permit persons to whom the Software is furnished to do so, subject to
|
|
// the following conditions:
|
|
//
|
|
// The above copyright notice and this permission notice shall be
|
|
// included in all copies or substantial portions of the Software.
|
|
//
|
|
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
|
// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
|
|
// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
|
// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
|
|
// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
|
|
// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
|
|
// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
|
//
|
|
|
|
using System;
|
|
using System.Collections;
|
|
using System.Collections.Generic;
|
|
using System.IO;
|
|
using System.Linq;
|
|
using Mono.CodeContracts.Static.AST;
|
|
using Mono.CodeContracts.Static.AST.Visitors;
|
|
using Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding;
|
|
using Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths;
|
|
using Mono.CodeContracts.Static.ControlFlow;
|
|
using Mono.CodeContracts.Static.DataStructures;
|
|
using Mono.CodeContracts.Static.Providers;
|
|
|
|
namespace Mono.CodeContracts.Static.Proving {
|
|
internal abstract class BoxedExpression {
|
|
public virtual bool IsVariable
|
|
{
|
|
get { return false; }
|
|
}
|
|
|
|
public virtual bool IsBooleanTyped
|
|
{
|
|
get { return false; }
|
|
}
|
|
|
|
public virtual object UnderlyingVariable
|
|
{
|
|
get { return false; }
|
|
}
|
|
|
|
public virtual PathElement[] AccessPath
|
|
{
|
|
get { return null; }
|
|
}
|
|
|
|
public virtual bool IsConstant
|
|
{
|
|
get { return false; }
|
|
}
|
|
|
|
public virtual object Constant
|
|
{
|
|
get { throw new InvalidOperationException (); }
|
|
}
|
|
|
|
public virtual object ConstantType
|
|
{
|
|
get { throw new InvalidOperationException (); }
|
|
}
|
|
|
|
public virtual bool IsSizeof
|
|
{
|
|
get { return false; }
|
|
}
|
|
|
|
public virtual bool IsUnary
|
|
{
|
|
get { return false; }
|
|
}
|
|
|
|
public virtual UnaryOperator UnaryOperator
|
|
{
|
|
get { throw new InvalidOperationException (); }
|
|
}
|
|
|
|
public virtual BoxedExpression UnaryArgument
|
|
{
|
|
get { throw new InvalidOperationException (); }
|
|
}
|
|
|
|
public virtual bool IsBinary
|
|
{
|
|
get { return false; }
|
|
}
|
|
|
|
public virtual BinaryOperator BinaryOperator
|
|
{
|
|
get { throw new InvalidOperationException (); }
|
|
}
|
|
|
|
public virtual BoxedExpression BinaryLeftArgument
|
|
{
|
|
get { throw new InvalidOperationException (); }
|
|
}
|
|
|
|
public virtual BoxedExpression BinaryRightArgument
|
|
{
|
|
get { throw new InvalidOperationException (); }
|
|
}
|
|
|
|
public virtual bool IsIsinst
|
|
{
|
|
get { return false; }
|
|
}
|
|
|
|
public virtual bool IsNull
|
|
{
|
|
get { return false; }
|
|
}
|
|
|
|
public virtual bool IsCast
|
|
{
|
|
get { return false; }
|
|
}
|
|
|
|
public virtual bool IsResult
|
|
{
|
|
get { return false; }
|
|
}
|
|
|
|
public virtual bool TryGetType (out object type)
|
|
{
|
|
type = null;
|
|
return false;
|
|
}
|
|
|
|
public virtual bool IsBinaryExpression (out BinaryOperator op, out BoxedExpression left, out BoxedExpression right)
|
|
{
|
|
op = BinaryOperator.Add;
|
|
left = null;
|
|
right = null;
|
|
return false;
|
|
}
|
|
|
|
public virtual bool IsUnaryExpression (out UnaryOperator op, out BoxedExpression argument)
|
|
{
|
|
op = UnaryOperator.Conv_i;
|
|
argument = null;
|
|
return false;
|
|
}
|
|
|
|
public virtual bool Sizeof (out int size)
|
|
{
|
|
return false.Without (out size);
|
|
}
|
|
|
|
public virtual bool IsIsinstExpression (out BoxedExpression expr, out TypeNode type)
|
|
{
|
|
expr = null;
|
|
type = null;
|
|
return false;
|
|
}
|
|
|
|
public abstract void AddFreeVariables (HashSet<BoxedExpression> set);
|
|
|
|
public virtual BoxedExpression Substitute (BoxedExpression what, BoxedExpression replace)
|
|
{
|
|
if (this == what || Equals (what))
|
|
return replace;
|
|
|
|
return RecursiveSubstitute (what, replace);
|
|
}
|
|
|
|
public abstract BoxedExpression Substitute<Variable> (Func<Variable, BoxedExpression, BoxedExpression> map);
|
|
|
|
protected internal virtual BoxedExpression RecursiveSubstitute (BoxedExpression what, BoxedExpression replace)
|
|
{
|
|
return this;
|
|
}
|
|
|
|
public abstract Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
where Visitor : IILVisitor<PC, Dummy, Dummy, Data, Result>;
|
|
|
|
public static BoxedExpression Var (object var)
|
|
{
|
|
return new VariableExpression (var);
|
|
}
|
|
|
|
public static BoxedExpression Const (object value, TypeNode type)
|
|
{
|
|
return new ConstantExpression (value, type);
|
|
}
|
|
|
|
public static BoxedExpression For<Variable, Expression> (Expression external, IFullExpressionDecoder<Variable, Expression> decoder)
|
|
where Expression : IEquatable<Expression>
|
|
{
|
|
return new ExternalBox<Variable, Expression> (external, decoder);
|
|
}
|
|
|
|
public static BoxedExpression MakeIsinst (TypeNode type, BoxedExpression arg)
|
|
{
|
|
return new IsinstExpression (arg, type);
|
|
}
|
|
|
|
public static BoxedExpression Convert<Variable, ExternalExpression> (ExternalExpression expr, IFullExpressionDecoder<Variable, ExternalExpression> decoder)
|
|
{
|
|
TypeNode type;
|
|
object value;
|
|
if (decoder.IsConstant (expr, out value, out type))
|
|
return new ConstantExpression (value, type);
|
|
if (decoder.IsNull (expr))
|
|
return new ConstantExpression (null, null);
|
|
|
|
object variable;
|
|
if (decoder.IsVariable (expr, out variable)) {
|
|
Sequence<PathElement> variableAccessPath = decoder.GetVariableAccessPath (expr);
|
|
return new VariableExpression (variable, variableAccessPath);
|
|
}
|
|
|
|
if (decoder.IsSizeof (expr, out type)) {
|
|
int sizeAsConstant;
|
|
return decoder.TrySizeOfAsConstant (expr, out sizeAsConstant) ? new SizeOfExpression (type, sizeAsConstant) : new SizeOfExpression (type);
|
|
}
|
|
|
|
ExternalExpression arg;
|
|
if (decoder.IsIsinst (expr, out arg, out type))
|
|
return new IsinstExpression (Convert (arg, decoder), type);
|
|
|
|
UnaryOperator op;
|
|
if (decoder.IsUnaryExpression (expr, out op, out arg))
|
|
return new UnaryExpression (op, Convert (arg, decoder));
|
|
|
|
BinaryOperator bop;
|
|
ExternalExpression left;
|
|
ExternalExpression right;
|
|
if (!decoder.IsBinaryExpression (expr, out bop, out left, out right))
|
|
throw new InvalidOperationException ();
|
|
|
|
return new BinaryExpression (bop, Convert (left, decoder), Convert (right, decoder));
|
|
}
|
|
|
|
public static BoxedExpression Binary (BinaryOperator bop, BoxedExpression left, BoxedExpression right)
|
|
{
|
|
return new BinaryExpression (bop, left, right);
|
|
}
|
|
|
|
public static BoxedExpression Unary (UnaryOperator op, BoxedExpression arg)
|
|
{
|
|
return new UnaryExpression (op, arg);
|
|
}
|
|
|
|
#region Nested type: AssertExpression
|
|
public class AssertExpression : ContractExpression {
|
|
public AssertExpression (BoxedExpression condition, EdgeTag tag, APC pc) : base (condition, tag, pc)
|
|
{
|
|
}
|
|
|
|
#region Overrides of ContractExpression
|
|
public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
{
|
|
return visitor.Assert (pc, this.Tag, Dummy.Value, data);
|
|
}
|
|
|
|
public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
|
|
{
|
|
BoxedExpression cond = this.Condition.Substitute (map);
|
|
if (cond == this.Condition)
|
|
return this;
|
|
if (cond == null)
|
|
return null;
|
|
|
|
return new AssertExpression (cond, this.Tag, this.Apc);
|
|
}
|
|
#endregion
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: AssumeExpression
|
|
public class AssumeExpression : ContractExpression {
|
|
public AssumeExpression (BoxedExpression condition, EdgeTag tag, APC pc)
|
|
: base (condition, tag, pc)
|
|
{
|
|
}
|
|
|
|
#region Overrides of ContractExpression
|
|
public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
{
|
|
return visitor.Assume (pc, this.Tag, Dummy.Value, data);
|
|
}
|
|
|
|
public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
|
|
{
|
|
BoxedExpression cond = this.Condition.Substitute (map);
|
|
if (cond == this.Condition)
|
|
return this;
|
|
if (cond == null)
|
|
return null;
|
|
|
|
return new AssumeExpression (cond, this.Tag, this.Apc);
|
|
}
|
|
#endregion
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: BinaryExpression
|
|
public class BinaryExpression : BoxedExpression {
|
|
public readonly BoxedExpression Left;
|
|
public readonly BinaryOperator Op;
|
|
public readonly BoxedExpression Right;
|
|
|
|
public BinaryExpression (BinaryOperator op, BoxedExpression left, BoxedExpression right)
|
|
{
|
|
this.Op = op;
|
|
this.Left = left;
|
|
this.Right = right;
|
|
}
|
|
|
|
public override bool IsBinary
|
|
{
|
|
get { return true; }
|
|
}
|
|
|
|
public override BoxedExpression BinaryLeftArgument
|
|
{
|
|
get { return this.Left; }
|
|
}
|
|
|
|
public override BoxedExpression BinaryRightArgument
|
|
{
|
|
get { return this.Right; }
|
|
}
|
|
|
|
public override BinaryOperator BinaryOperator
|
|
{
|
|
get { return this.Op; }
|
|
}
|
|
|
|
public override bool IsBinaryExpression (out BinaryOperator op, out BoxedExpression left, out BoxedExpression right)
|
|
{
|
|
op = this.Op;
|
|
left = this.Left;
|
|
right = this.Right;
|
|
return true;
|
|
}
|
|
|
|
#region Overrides of BoxedExpression
|
|
public override void AddFreeVariables (HashSet<BoxedExpression> set)
|
|
{
|
|
this.Left.AddFreeVariables (set);
|
|
this.Right.AddFreeVariables (set);
|
|
}
|
|
|
|
protected internal override BoxedExpression RecursiveSubstitute (BoxedExpression what, BoxedExpression replace)
|
|
{
|
|
BoxedExpression left = this.Left.Substitute (what, replace);
|
|
BoxedExpression right = this.Right.Substitute (what, replace);
|
|
if (left == this.Left && right == this.Right)
|
|
return this;
|
|
|
|
return new BinaryExpression (this.Op, left, right);
|
|
}
|
|
|
|
public override BoxedExpression Substitute<Variable> (Func<Variable, BoxedExpression, BoxedExpression> map)
|
|
{
|
|
BoxedExpression left = this.Left.Substitute (map);
|
|
if (left == null)
|
|
return null;
|
|
|
|
BoxedExpression right = this.Right.Substitute (map);
|
|
if (right == null)
|
|
return null;
|
|
|
|
if (this.Left == left && this.Right == right)
|
|
return this;
|
|
return new BinaryExpression (this.Op, left, right);
|
|
}
|
|
|
|
public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
{
|
|
return visitor.Binary (pc, this.Op, Dummy.Value, Dummy.Value, Dummy.Value, data);
|
|
}
|
|
#endregion
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: CastExpression
|
|
public class CastExpression : BoxedExpression {
|
|
public readonly TypeNode CastToType;
|
|
public readonly BoxedExpression Expr;
|
|
|
|
public CastExpression (TypeNode castToType, BoxedExpression expr)
|
|
{
|
|
this.CastToType = castToType;
|
|
this.Expr = expr;
|
|
}
|
|
|
|
public override bool IsCast
|
|
{
|
|
get { return true; }
|
|
}
|
|
|
|
public override PathElement[] AccessPath
|
|
{
|
|
get { return this.Expr.AccessPath; }
|
|
}
|
|
|
|
public override BoxedExpression BinaryLeftArgument
|
|
{
|
|
get { return this.Expr.BinaryLeftArgument; }
|
|
}
|
|
|
|
public override BoxedExpression BinaryRightArgument
|
|
{
|
|
get { return this.Expr.BinaryRightArgument; }
|
|
}
|
|
|
|
public override BinaryOperator BinaryOperator
|
|
{
|
|
get { return this.Expr.BinaryOperator; }
|
|
}
|
|
|
|
public override object Constant
|
|
{
|
|
get { return this.Expr.Constant; }
|
|
}
|
|
|
|
public override object ConstantType
|
|
{
|
|
get { return this.Expr.ConstantType; }
|
|
}
|
|
|
|
public override bool IsBinary
|
|
{
|
|
get { return this.Expr.IsBinary; }
|
|
}
|
|
|
|
public override bool IsBooleanTyped
|
|
{
|
|
get { return this.Expr.IsBooleanTyped; }
|
|
}
|
|
|
|
public override bool IsConstant
|
|
{
|
|
get { return this.Expr.IsConstant; }
|
|
}
|
|
|
|
|
|
public override bool IsSizeof
|
|
{
|
|
get { return this.Expr.IsSizeof; }
|
|
}
|
|
|
|
public override bool IsNull
|
|
{
|
|
get { return this.Expr.IsNull; }
|
|
}
|
|
|
|
public override bool IsIsinst
|
|
{
|
|
get { return this.Expr.IsIsinst; }
|
|
}
|
|
|
|
public override bool IsResult
|
|
{
|
|
get { return this.Expr.IsResult; }
|
|
}
|
|
|
|
public override bool IsUnary
|
|
{
|
|
get { return this.Expr.IsUnary; }
|
|
}
|
|
|
|
public override bool IsVariable
|
|
{
|
|
get { return this.Expr.IsVariable; }
|
|
}
|
|
|
|
public override BoxedExpression UnaryArgument
|
|
{
|
|
get { return this.Expr.UnaryArgument; }
|
|
}
|
|
|
|
public override UnaryOperator UnaryOperator
|
|
{
|
|
get { return this.Expr.UnaryOperator; }
|
|
}
|
|
|
|
public override object UnderlyingVariable
|
|
{
|
|
get { return this.Expr.UnderlyingVariable; }
|
|
}
|
|
|
|
|
|
public override void AddFreeVariables (HashSet<BoxedExpression> set)
|
|
{
|
|
this.Expr.AddFreeVariables (set);
|
|
}
|
|
|
|
public override BoxedExpression Substitute<Variable> (Func<Variable, BoxedExpression, BoxedExpression> map)
|
|
{
|
|
return this.Expr.Substitute (map);
|
|
}
|
|
|
|
public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
{
|
|
return this.Expr.ForwardDecode<Data, Result, Visitor> (pc, visitor, data);
|
|
}
|
|
|
|
public override bool IsBinaryExpression (out BinaryOperator op, out BoxedExpression left, out BoxedExpression right)
|
|
{
|
|
return this.Expr.IsBinaryExpression (out op, out left, out right);
|
|
}
|
|
|
|
protected internal override BoxedExpression RecursiveSubstitute (BoxedExpression what, BoxedExpression replace)
|
|
{
|
|
return this.Expr.RecursiveSubstitute (what, replace);
|
|
}
|
|
|
|
public override BoxedExpression Substitute (BoxedExpression what, BoxedExpression replace)
|
|
{
|
|
return this.Expr.Substitute (what, replace);
|
|
}
|
|
|
|
public override bool IsUnaryExpression (out UnaryOperator op, out BoxedExpression argument)
|
|
{
|
|
return this.Expr.IsUnaryExpression (out op, out argument);
|
|
}
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: ConstantExpression
|
|
public class ConstantExpression : BoxedExpression {
|
|
public readonly TypeNode Type;
|
|
public readonly object Value;
|
|
private readonly bool is_boolean;
|
|
|
|
public ConstantExpression (object value, TypeNode type)
|
|
: this (value, type, false)
|
|
{
|
|
}
|
|
|
|
public ConstantExpression (object value, TypeNode type, bool isBoolean)
|
|
{
|
|
this.Value = value;
|
|
this.Type = type;
|
|
this.is_boolean = isBoolean;
|
|
}
|
|
|
|
public override bool IsBooleanTyped
|
|
{
|
|
get { return this.is_boolean; }
|
|
}
|
|
|
|
public override bool IsConstant
|
|
{
|
|
get { return true; }
|
|
}
|
|
|
|
public override object Constant
|
|
{
|
|
get { return this.Value; }
|
|
}
|
|
|
|
public override object ConstantType
|
|
{
|
|
get { return this.Type; }
|
|
}
|
|
|
|
public override bool IsNull
|
|
{
|
|
get
|
|
{
|
|
if (this.Value == null)
|
|
return true;
|
|
|
|
var conv = this.Value as IConvertible;
|
|
if (conv != null) {
|
|
try {
|
|
if (conv.ToInt32 (null) == 0)
|
|
return true;
|
|
} catch {
|
|
return false;
|
|
}
|
|
}
|
|
|
|
return false;
|
|
}
|
|
}
|
|
|
|
public override void AddFreeVariables (HashSet<BoxedExpression> set)
|
|
{
|
|
}
|
|
|
|
public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
|
|
{
|
|
return this;
|
|
}
|
|
|
|
public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
{
|
|
if (this.Value == null)
|
|
return visitor.LoadNull (pc, Dummy.Value, data);
|
|
|
|
return visitor.LoadConst (pc, this.Type, this.Value, Dummy.Value, data);
|
|
}
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: ContractExpression
|
|
public abstract class ContractExpression : BoxedExpression {
|
|
public readonly APC Apc;
|
|
public readonly BoxedExpression Condition;
|
|
public readonly EdgeTag Tag;
|
|
|
|
public ContractExpression (BoxedExpression condition, EdgeTag tag, APC pc)
|
|
{
|
|
this.Tag = tag;
|
|
this.Condition = condition;
|
|
this.Apc = pc;
|
|
}
|
|
|
|
public override void AddFreeVariables (HashSet<BoxedExpression> set)
|
|
{
|
|
this.Condition.AddFreeVariables (set);
|
|
}
|
|
|
|
public abstract override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data);
|
|
public abstract override BoxedExpression Substitute<Variable> (Func<Variable, BoxedExpression, BoxedExpression> map);
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: ExternalBox
|
|
public class ExternalBox<Variable, LabeledSymbol> : BoxedExpression
|
|
where LabeledSymbol : IEquatable<LabeledSymbol> {
|
|
private readonly IFullExpressionDecoder<Variable, LabeledSymbol> decoder;
|
|
private readonly LabeledSymbol expr;
|
|
private Optional<Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression>> binary;
|
|
|
|
private Optional<Tuple<bool, object, TypeNode>> constant;
|
|
private Optional<Tuple<bool, BoxedExpression, TypeNode>> isInst;
|
|
private Optional<Pair<bool, object>> isVar;
|
|
private Optional<Pair<bool, TypeNode>> type;
|
|
private Optional<Tuple<bool, UnaryOperator, BoxedExpression>> unary;
|
|
private Optional<object> var;
|
|
|
|
public ExternalBox (LabeledSymbol external, IFullExpressionDecoder<Variable, LabeledSymbol> decoder)
|
|
{
|
|
this.expr = external;
|
|
this.decoder = decoder;
|
|
}
|
|
|
|
public override bool IsBinary
|
|
{
|
|
get
|
|
{
|
|
Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> binary;
|
|
TryGetBinaryFromCache (out binary);
|
|
return binary.Item1;
|
|
}
|
|
}
|
|
|
|
public override BinaryOperator BinaryOperator
|
|
{
|
|
get
|
|
{
|
|
Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> binary;
|
|
bool res = TryGetBinaryFromCache (out binary);
|
|
if (!res)
|
|
throw new InvalidOperationException ();
|
|
|
|
return binary.Item2;
|
|
}
|
|
}
|
|
|
|
public override BoxedExpression BinaryLeftArgument
|
|
{
|
|
get
|
|
{
|
|
Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> binary;
|
|
bool res = TryGetBinaryFromCache (out binary);
|
|
if (!res)
|
|
throw new InvalidOperationException ();
|
|
|
|
return binary.Item3;
|
|
}
|
|
}
|
|
|
|
public override BoxedExpression BinaryRightArgument
|
|
{
|
|
get
|
|
{
|
|
Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> binary;
|
|
bool res = TryGetBinaryFromCache (out binary);
|
|
if (!res)
|
|
throw new InvalidOperationException ();
|
|
|
|
return binary.Item4;
|
|
}
|
|
}
|
|
|
|
public override bool IsConstant
|
|
{
|
|
get
|
|
{
|
|
Tuple<bool, object, TypeNode> consta;
|
|
TryGetConstantFromCache (out consta);
|
|
|
|
return consta.Item1;
|
|
}
|
|
}
|
|
|
|
public override object Constant
|
|
{
|
|
get
|
|
{
|
|
Tuple<bool, object, TypeNode> consta;
|
|
if (!TryGetConstantFromCache (out consta))
|
|
throw new InvalidOperationException ();
|
|
|
|
return consta.Item2;
|
|
}
|
|
}
|
|
|
|
public override object ConstantType
|
|
{
|
|
get
|
|
{
|
|
Tuple<bool, object, TypeNode> consta;
|
|
if (!TryGetConstantFromCache (out consta))
|
|
throw new InvalidOperationException();
|
|
|
|
return consta.Item3;
|
|
}
|
|
}
|
|
|
|
public override bool IsIsinst
|
|
{
|
|
get
|
|
{
|
|
Tuple<bool, BoxedExpression, TypeNode> isinst;
|
|
TryGetIsInstFromCache (out isinst);
|
|
return isinst.Item1;
|
|
}
|
|
}
|
|
|
|
public override bool IsNull
|
|
{
|
|
get { return this.decoder.IsNull (this.expr); }
|
|
}
|
|
|
|
public override bool IsUnary
|
|
{
|
|
get
|
|
{
|
|
Tuple<bool, UnaryOperator, BoxedExpression> unary;
|
|
TryGetUnaryFromCache (out unary);
|
|
return unary.Item1;
|
|
}
|
|
}
|
|
|
|
public override UnaryOperator UnaryOperator
|
|
{
|
|
get
|
|
{
|
|
Tuple<bool, UnaryOperator, BoxedExpression> unary;
|
|
if (!TryGetUnaryFromCache (out unary))
|
|
throw new InvalidOperationException();
|
|
return unary.Item2;
|
|
}
|
|
}
|
|
|
|
public override BoxedExpression UnaryArgument
|
|
{
|
|
get
|
|
{
|
|
Tuple<bool, UnaryOperator, BoxedExpression> unary;
|
|
if (!TryGetUnaryFromCache (out unary))
|
|
throw new InvalidOperationException ();
|
|
return unary.Item3;
|
|
}
|
|
}
|
|
|
|
public override bool IsSizeof
|
|
{
|
|
get
|
|
{
|
|
TypeNode type;
|
|
return this.decoder.IsSizeof (this.expr, out type);
|
|
}
|
|
}
|
|
|
|
public override bool IsVariable
|
|
{
|
|
get
|
|
{
|
|
Pair<bool, object> var1;
|
|
TryGetIsVariableFromCache (out var1);
|
|
return var1.Key;
|
|
}
|
|
}
|
|
|
|
public override object UnderlyingVariable
|
|
{
|
|
get
|
|
{
|
|
if (!this.var.IsValid)
|
|
this.var = this.decoder.UnderlyingVariable (this.expr);
|
|
|
|
return this.var.Value;
|
|
}
|
|
}
|
|
|
|
private bool TryGetBinaryFromCache (out Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> binary)
|
|
{
|
|
if (this.binary.IsValid) {
|
|
binary = this.binary.Value;
|
|
return true;
|
|
}
|
|
BinaryOperator op;
|
|
LabeledSymbol left;
|
|
LabeledSymbol right;
|
|
bool res = this.decoder.IsBinaryExpression (this.expr, out op, out left, out right);
|
|
this.binary = binary = new Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> (res, op, For (left, this.decoder), For (right, this.decoder));
|
|
|
|
return res;
|
|
}
|
|
|
|
private bool TryGetUnaryFromCache (out Tuple<bool, UnaryOperator, BoxedExpression> unary)
|
|
{
|
|
if (this.unary.IsValid) {
|
|
unary = this.unary.Value;
|
|
return true;
|
|
}
|
|
UnaryOperator op;
|
|
LabeledSymbol arg;
|
|
bool res = this.decoder.IsUnaryExpression (this.expr, out op, out arg);
|
|
this.unary = unary = new Tuple<bool, UnaryOperator, BoxedExpression> (res, op, For (arg, this.decoder));
|
|
|
|
return res;
|
|
}
|
|
|
|
private bool TryGetIsInstFromCache (out Tuple<bool, BoxedExpression, TypeNode> isinst)
|
|
{
|
|
if (this.isInst.IsValid) {
|
|
isinst = this.isInst.Value;
|
|
return true;
|
|
}
|
|
|
|
LabeledSymbol arg;
|
|
TypeNode type;
|
|
bool res = this.decoder.IsIsinst (this.expr, out arg, out type);
|
|
this.isInst = isinst = new Tuple<bool, BoxedExpression, TypeNode> (res, For (arg, this.decoder), type);
|
|
|
|
return res;
|
|
}
|
|
|
|
private bool TryGetConstantFromCache (out Tuple<bool, object, TypeNode> result)
|
|
{
|
|
if (this.constant.IsValid) {
|
|
result = this.constant.Value;
|
|
return true;
|
|
}
|
|
object value;
|
|
TypeNode type;
|
|
bool res = this.decoder.IsConstant (this.expr, out value, out type);
|
|
this.constant = result = new Tuple<bool, object, TypeNode> (res, value, type);
|
|
|
|
return res;
|
|
}
|
|
|
|
private bool TryGetTypeFromCache (out Pair<bool, TypeNode> result)
|
|
{
|
|
if (this.type.IsValid) {
|
|
result = this.type.Value;
|
|
return true;
|
|
}
|
|
|
|
TypeNode type;
|
|
bool res = this.decoder.TryGetType (this.expr, out type);
|
|
this.type = result = new Pair<bool, TypeNode> (res, type);
|
|
|
|
return res;
|
|
}
|
|
|
|
private bool TryGetIsVariableFromCache (out Pair<bool, object> result)
|
|
{
|
|
if (this.isVar.IsValid) {
|
|
result = this.isVar.Value;
|
|
return true;
|
|
}
|
|
|
|
object value;
|
|
bool res = this.decoder.IsVariable (this.expr, out value);
|
|
this.isVar = result = new Pair<bool, object> (res, value);
|
|
|
|
return res;
|
|
}
|
|
|
|
public override bool IsBinaryExpression (out BinaryOperator op, out BoxedExpression left, out BoxedExpression right)
|
|
{
|
|
Tuple<bool, BinaryOperator, BoxedExpression, BoxedExpression> bin;
|
|
if (!TryGetBinaryFromCache (out bin) || !bin.Item1) {
|
|
op = BinaryOperator.Add;
|
|
left = null;
|
|
right = null;
|
|
return false;
|
|
}
|
|
|
|
op = bin.Item2;
|
|
left = bin.Item3;
|
|
right = bin.Item4;
|
|
return true;
|
|
}
|
|
|
|
public override bool IsIsinstExpression (out BoxedExpression expr, out TypeNode type)
|
|
{
|
|
Tuple<bool, BoxedExpression, TypeNode> isinst;
|
|
if (!TryGetIsInstFromCache (out isinst) || !isinst.Item1) {
|
|
expr = null;
|
|
type = null;
|
|
return false;
|
|
}
|
|
|
|
expr = isinst.Item2;
|
|
type = isinst.Item3;
|
|
return true;
|
|
}
|
|
|
|
public override bool IsUnaryExpression (out UnaryOperator op, out BoxedExpression argument)
|
|
{
|
|
Tuple<bool, UnaryOperator, BoxedExpression> unary;
|
|
if (!TryGetUnaryFromCache (out unary) || !unary.Item1) {
|
|
op = UnaryOperator.Conv_i;
|
|
argument = null;
|
|
return false;
|
|
}
|
|
|
|
op = unary.Item2;
|
|
argument = unary.Item3;
|
|
return true;
|
|
}
|
|
|
|
protected internal override BoxedExpression RecursiveSubstitute (BoxedExpression what, BoxedExpression replace)
|
|
{
|
|
return Convert (this.expr, this.decoder).Substitute (what, replace);
|
|
}
|
|
|
|
public override void AddFreeVariables (HashSet<BoxedExpression> set)
|
|
{
|
|
this.decoder.AddFreeVariables (this.expr, new SetWrapper (set, this.decoder));
|
|
}
|
|
|
|
public override BoxedExpression Substitute<V> (Func<V, BoxedExpression, BoxedExpression> map)
|
|
{
|
|
return Convert (this.expr, this.decoder).Substitute (map);
|
|
}
|
|
|
|
public override bool TryGetType (out object type)
|
|
{
|
|
Pair<bool, TypeNode> result;
|
|
if (!TryGetTypeFromCache (out result) || !result.Key) {
|
|
type = null;
|
|
return false;
|
|
}
|
|
|
|
type = result.Value;
|
|
return true;
|
|
}
|
|
|
|
public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
{
|
|
Tuple<bool, object, TypeNode> constant;
|
|
if (TryGetConstantFromCache (out constant)) {
|
|
if (constant.Item2 != null)
|
|
return visitor.LoadConst (pc, constant.Item3, constant, Dummy.Value, data);
|
|
|
|
return visitor.LoadNull (pc, Dummy.Value, data);
|
|
}
|
|
|
|
UnaryOperator op;
|
|
LabeledSymbol arg;
|
|
if (this.decoder.IsUnaryExpression (this.expr, out op, out arg))
|
|
return visitor.Unary (pc, op, false, Dummy.Value, Dummy.Value, data);
|
|
|
|
BinaryOperator bop;
|
|
LabeledSymbol left;
|
|
LabeledSymbol right;
|
|
if (this.decoder.IsBinaryExpression (this.expr, out bop, out left, out right))
|
|
return visitor.Binary (pc, bop, Dummy.Value, Dummy.Value, Dummy.Value, data);
|
|
TypeNode type;
|
|
if (this.decoder.IsIsinst (this.expr, out arg, out type))
|
|
return visitor.Isinst (pc, type, Dummy.Value, Dummy.Value, data);
|
|
if (this.decoder.IsNull (this.expr))
|
|
return visitor.LoadNull (pc, Dummy.Value, data);
|
|
if (this.decoder.IsSizeof (this.expr, out type))
|
|
return visitor.Sizeof (pc, type, Dummy.Value, data);
|
|
|
|
return visitor.Nop (pc, data);
|
|
}
|
|
|
|
#region Nested type: SetWrapper
|
|
private struct SetWrapper : ISet<LabeledSymbol>, IEnumerable<LabeledSymbol> {
|
|
private readonly IFullExpressionDecoder<Variable, LabeledSymbol> decoder;
|
|
private readonly HashSet<BoxedExpression> set;
|
|
|
|
#region Implementation of IEnumerable
|
|
public IEnumerator<LabeledSymbol> GetEnumerator ()
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
IEnumerator IEnumerable.GetEnumerator ()
|
|
{
|
|
return GetEnumerator ();
|
|
}
|
|
#endregion
|
|
|
|
public SetWrapper (HashSet<BoxedExpression> set, IFullExpressionDecoder<Variable, LabeledSymbol> decoder)
|
|
{
|
|
this.set = set;
|
|
this.decoder = decoder;
|
|
}
|
|
|
|
#region Implementation of ICollection<ExternalExpression>
|
|
public void Add (LabeledSymbol item)
|
|
{
|
|
this.set.Add (For (item, this.decoder));
|
|
}
|
|
|
|
bool ISet<LabeledSymbol>.Add (LabeledSymbol item)
|
|
{
|
|
Add (item);
|
|
return true;
|
|
}
|
|
|
|
public void UnionWith (IEnumerable<LabeledSymbol> other)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
public void IntersectWith (IEnumerable<LabeledSymbol> other)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
public void ExceptWith (IEnumerable<LabeledSymbol> other)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
public void SymmetricExceptWith (IEnumerable<LabeledSymbol> other)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
public bool IsSubsetOf (IEnumerable<LabeledSymbol> other)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
public bool IsSupersetOf (IEnumerable<LabeledSymbol> other)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
public bool IsProperSupersetOf (IEnumerable<LabeledSymbol> other)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
public bool IsProperSubsetOf (IEnumerable<LabeledSymbol> other)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
public bool Overlaps (IEnumerable<LabeledSymbol> other)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
public bool SetEquals (IEnumerable<LabeledSymbol> other)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
|
|
public void Clear ()
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
public bool Contains (LabeledSymbol item)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
public void CopyTo (LabeledSymbol[] array, int arrayIndex)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
public bool Remove (LabeledSymbol item)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
|
|
public int Count
|
|
{
|
|
get { throw new NotImplementedException (); }
|
|
}
|
|
|
|
public bool IsReadOnly
|
|
{
|
|
get { throw new NotImplementedException (); }
|
|
}
|
|
#endregion
|
|
}
|
|
#endregion
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: IsinstExpression
|
|
public class IsinstExpression : BoxedExpression {
|
|
private readonly BoxedExpression arg;
|
|
private readonly TypeNode type;
|
|
|
|
public IsinstExpression (BoxedExpression boxedExpression, TypeNode type)
|
|
{
|
|
this.arg = boxedExpression;
|
|
this.type = type;
|
|
}
|
|
|
|
public override bool IsIsinst
|
|
{
|
|
get { return true; }
|
|
}
|
|
|
|
public override BoxedExpression UnaryArgument
|
|
{
|
|
get { return this.arg; }
|
|
}
|
|
|
|
public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
{
|
|
return visitor.Isinst (pc, this.type, Dummy.Value, Dummy.Value, data);
|
|
}
|
|
|
|
public override void AddFreeVariables (HashSet<BoxedExpression> set)
|
|
{
|
|
this.arg.AddFreeVariables (set);
|
|
}
|
|
|
|
public override BoxedExpression Substitute<Variable> (Func<Variable, BoxedExpression, BoxedExpression> map)
|
|
{
|
|
BoxedExpression arg = this.arg.Substitute (map);
|
|
if (arg == this.arg)
|
|
return this;
|
|
if (arg == null)
|
|
return null;
|
|
|
|
return new IsinstExpression (arg, this.type);
|
|
}
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: OldExpression
|
|
public class OldExpression : BoxedExpression {
|
|
private const string ContractOldValueTemplate = "Contract.OldValue({0})";
|
|
|
|
public readonly BoxedExpression Old;
|
|
public readonly TypeNode Type;
|
|
|
|
public OldExpression (BoxedExpression old, TypeNode type)
|
|
{
|
|
this.Old = old;
|
|
this.Type = type;
|
|
}
|
|
|
|
#region Overrides of BoxedExpression
|
|
public override void AddFreeVariables (HashSet<BoxedExpression> set)
|
|
{
|
|
this.Old.AddFreeVariables (set);
|
|
}
|
|
|
|
public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
|
|
{
|
|
BoxedExpression old = this.Old.Substitute (map);
|
|
if (old == this.Old)
|
|
return this;
|
|
if (old == null)
|
|
return null;
|
|
|
|
return new OldExpression (old, this.Type);
|
|
}
|
|
|
|
public override bool IsBinaryExpression (out BinaryOperator op, out BoxedExpression left, out BoxedExpression right)
|
|
{
|
|
return this.Old.IsBinaryExpression (out op, out left, out right);
|
|
}
|
|
|
|
public override bool IsUnaryExpression (out UnaryOperator op, out BoxedExpression argument)
|
|
{
|
|
return this.Old.IsUnaryExpression (out op, out argument);
|
|
}
|
|
|
|
public override bool IsIsinstExpression (out BoxedExpression expr, out TypeNode type)
|
|
{
|
|
return this.Old.IsIsinstExpression (out expr, out type);
|
|
}
|
|
|
|
public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
{
|
|
return visitor.EndOld (pc, new PC (pc.Node, 0), this.Type, Dummy.Value, Dummy.Value, data);
|
|
}
|
|
#endregion
|
|
|
|
public override PathElement[] AccessPath
|
|
{
|
|
get { return this.Old.AccessPath; }
|
|
}
|
|
|
|
public override BoxedExpression BinaryLeftArgument
|
|
{
|
|
get { return this.Old.BinaryLeftArgument; }
|
|
}
|
|
|
|
public override BoxedExpression BinaryRightArgument
|
|
{
|
|
get { return this.Old.BinaryRightArgument; }
|
|
}
|
|
|
|
public override BinaryOperator BinaryOperator
|
|
{
|
|
get { return this.Old.BinaryOperator; }
|
|
}
|
|
|
|
public override object Constant
|
|
{
|
|
get { return this.Old.Constant; }
|
|
}
|
|
|
|
public override object ConstantType
|
|
{
|
|
get { return this.Old.ConstantType; }
|
|
}
|
|
|
|
public override bool IsBinary
|
|
{
|
|
get { return this.Old.IsBinary; }
|
|
}
|
|
|
|
public override bool IsConstant
|
|
{
|
|
get { return this.Old.IsConstant; }
|
|
}
|
|
|
|
public override bool IsSizeof
|
|
{
|
|
get { return this.Old.IsSizeof; }
|
|
}
|
|
|
|
public override bool IsNull
|
|
{
|
|
get { return this.Old.IsNull; }
|
|
}
|
|
|
|
public override bool IsIsinst
|
|
{
|
|
get { return this.Old.IsIsinst; }
|
|
}
|
|
|
|
public override bool IsUnary
|
|
{
|
|
get { return this.Old.IsUnary; }
|
|
}
|
|
|
|
public override bool IsVariable
|
|
{
|
|
get { return this.Old.IsVariable; }
|
|
}
|
|
|
|
public override BoxedExpression UnaryArgument
|
|
{
|
|
get { return this.Old.UnaryArgument; }
|
|
}
|
|
|
|
public override UnaryOperator UnaryOperator
|
|
{
|
|
get { return this.Old.UnaryOperator; }
|
|
}
|
|
|
|
public override object UnderlyingVariable
|
|
{
|
|
get { return this.Old.UnderlyingVariable; }
|
|
}
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: PC
|
|
public struct PC {
|
|
public readonly int Index;
|
|
public readonly BoxedExpression Node;
|
|
|
|
public PC (BoxedExpression expr, int index)
|
|
{
|
|
this.Node = expr;
|
|
this.Index = index;
|
|
}
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: ResultExpression
|
|
public class ResultExpression : BoxedExpression {
|
|
private const string ContractResultTemplate = "Contract.Result<{0}>()";
|
|
|
|
public readonly TypeNode Type;
|
|
|
|
public ResultExpression (TypeNode type)
|
|
{
|
|
this.Type = type;
|
|
}
|
|
|
|
public override bool IsResult
|
|
{
|
|
get { return true; }
|
|
}
|
|
|
|
public override void AddFreeVariables (HashSet<BoxedExpression> set)
|
|
{
|
|
}
|
|
|
|
public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
|
|
{
|
|
return this;
|
|
}
|
|
|
|
public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
{
|
|
return visitor.LoadResult (pc, this.Type, Dummy.Value, Dummy.Value, data);
|
|
}
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: SizeOfExpression
|
|
public class SizeOfExpression : BoxedExpression {
|
|
public readonly int SizeAsConstant;
|
|
public readonly TypeNode Type;
|
|
|
|
public SizeOfExpression (TypeNode type, int sizeAsConstant)
|
|
{
|
|
this.Type = type;
|
|
this.SizeAsConstant = sizeAsConstant;
|
|
}
|
|
|
|
public SizeOfExpression (TypeNode type)
|
|
: this (type, -1)
|
|
{
|
|
}
|
|
|
|
public override bool IsSizeof
|
|
{
|
|
get { return true; }
|
|
}
|
|
|
|
public override bool Sizeof (out int size)
|
|
{
|
|
size = SizeAsConstant;
|
|
return size >= 0;
|
|
}
|
|
|
|
public override void AddFreeVariables (HashSet<BoxedExpression> set)
|
|
{
|
|
}
|
|
|
|
public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
|
|
{
|
|
return this;
|
|
}
|
|
|
|
public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
{
|
|
return visitor.Sizeof (pc, this.Type, Dummy.Value, data);
|
|
}
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: UnaryExpression
|
|
public class UnaryExpression : BoxedExpression {
|
|
public readonly BoxedExpression Argument;
|
|
public readonly UnaryOperator Op;
|
|
|
|
public UnaryExpression (UnaryOperator op, BoxedExpression argument)
|
|
{
|
|
this.Op = op;
|
|
this.Argument = argument;
|
|
}
|
|
|
|
public override bool IsUnary
|
|
{
|
|
get { return true; }
|
|
}
|
|
|
|
public override BoxedExpression UnaryArgument
|
|
{
|
|
get { return this.Argument; }
|
|
}
|
|
|
|
public override UnaryOperator UnaryOperator
|
|
{
|
|
get { return this.Op; }
|
|
}
|
|
|
|
public override bool IsUnaryExpression (out UnaryOperator op, out BoxedExpression argument)
|
|
{
|
|
op = this.Op;
|
|
argument = this.Argument;
|
|
return true;
|
|
}
|
|
|
|
public override void AddFreeVariables (HashSet<BoxedExpression> set)
|
|
{
|
|
this.Argument.AddFreeVariables (set);
|
|
}
|
|
|
|
public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
|
|
{
|
|
BoxedExpression argument = this.Argument.Substitute (map);
|
|
if (argument == this.Argument)
|
|
return this;
|
|
if (argument == null)
|
|
return null;
|
|
|
|
return new UnaryExpression (this.Op, argument);
|
|
}
|
|
|
|
protected internal override BoxedExpression RecursiveSubstitute (BoxedExpression what, BoxedExpression replace)
|
|
{
|
|
BoxedExpression argument = this.Argument.Substitute (what, replace);
|
|
|
|
if (argument == this.Argument)
|
|
return this;
|
|
|
|
return new UnaryExpression (this.Op, argument);
|
|
}
|
|
|
|
public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
{
|
|
return visitor.Unary (pc, this.Op, false, Dummy.Value, Dummy.Value, data);
|
|
}
|
|
|
|
public override bool Equals (object obj)
|
|
{
|
|
if (this == obj)
|
|
return true;
|
|
|
|
var unary = obj as UnaryExpression;
|
|
return unary != null && this.Op == unary.Op && this.Argument.Equals (unary.Argument);
|
|
}
|
|
|
|
public override int GetHashCode ()
|
|
{
|
|
return this.Op.GetHashCode () * 13 + (this.Argument == null ? 0 : this.Argument.GetHashCode ());
|
|
}
|
|
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: ValueAtReturnExpression
|
|
public class ValueAtReturnExpression : BoxedExpression {
|
|
private const string ContractValueAtReturnTemplate = "Contract.ValueAtReturn({0})";
|
|
|
|
public readonly TypeNode Type;
|
|
public readonly BoxedExpression Value;
|
|
|
|
public ValueAtReturnExpression (BoxedExpression old, TypeNode type)
|
|
{
|
|
this.Value = old;
|
|
this.Type = type;
|
|
}
|
|
|
|
#region Overrides of BoxedExpression
|
|
public override void AddFreeVariables (HashSet<BoxedExpression> set)
|
|
{
|
|
this.Value.AddFreeVariables (set);
|
|
}
|
|
|
|
public override BoxedExpression Substitute<Variable1> (Func<Variable1, BoxedExpression, BoxedExpression> map)
|
|
{
|
|
BoxedExpression value = this.Value.Substitute (map);
|
|
if (value == this.Value)
|
|
return this;
|
|
if (value == null)
|
|
return null;
|
|
|
|
return new ValueAtReturnExpression (value, this.Type);
|
|
}
|
|
|
|
public override bool IsBinaryExpression (out BinaryOperator op, out BoxedExpression left, out BoxedExpression right)
|
|
{
|
|
return this.Value.IsBinaryExpression (out op, out left, out right);
|
|
}
|
|
|
|
public override bool IsUnaryExpression (out UnaryOperator op, out BoxedExpression argument)
|
|
{
|
|
return this.Value.IsUnaryExpression (out op, out argument);
|
|
}
|
|
|
|
public override bool IsIsinstExpression (out BoxedExpression expr, out TypeNode type)
|
|
{
|
|
return this.Value.IsIsinstExpression (out expr, out type);
|
|
}
|
|
|
|
public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
{
|
|
throw new NotImplementedException ();
|
|
}
|
|
#endregion
|
|
|
|
public override PathElement[] AccessPath
|
|
{
|
|
get { return this.Value.AccessPath; }
|
|
}
|
|
|
|
public override BoxedExpression BinaryLeftArgument
|
|
{
|
|
get { return this.Value.BinaryLeftArgument; }
|
|
}
|
|
|
|
public override BoxedExpression BinaryRightArgument
|
|
{
|
|
get { return this.Value.BinaryRightArgument; }
|
|
}
|
|
|
|
public override BinaryOperator BinaryOperator
|
|
{
|
|
get { return this.Value.BinaryOperator; }
|
|
}
|
|
|
|
public override object Constant
|
|
{
|
|
get { return this.Value.Constant; }
|
|
}
|
|
|
|
public override object ConstantType
|
|
{
|
|
get { return this.Value.ConstantType; }
|
|
}
|
|
|
|
public override bool IsBinary
|
|
{
|
|
get { return this.Value.IsBinary; }
|
|
}
|
|
|
|
public override bool IsConstant
|
|
{
|
|
get { return this.Value.IsConstant; }
|
|
}
|
|
|
|
public override bool IsSizeof
|
|
{
|
|
get { return this.Value.IsSizeof; }
|
|
}
|
|
|
|
public override bool IsNull
|
|
{
|
|
get { return this.Value.IsNull; }
|
|
}
|
|
|
|
public override bool IsIsinst
|
|
{
|
|
get { return this.Value.IsIsinst; }
|
|
}
|
|
|
|
public override bool IsUnary
|
|
{
|
|
get { return this.Value.IsUnary; }
|
|
}
|
|
|
|
public override bool IsVariable
|
|
{
|
|
get { return this.Value.IsVariable; }
|
|
}
|
|
|
|
public override BoxedExpression UnaryArgument
|
|
{
|
|
get { return this.Value.UnaryArgument; }
|
|
}
|
|
|
|
public override UnaryOperator UnaryOperator
|
|
{
|
|
get { return this.Value.UnaryOperator; }
|
|
}
|
|
|
|
public override object UnderlyingVariable
|
|
{
|
|
get { return this.Value.UnderlyingVariable; }
|
|
}
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: VariableExpression
|
|
public class VariableExpression : BoxedExpression {
|
|
private readonly PathElement[] Path;
|
|
private readonly object UnderlyingVar;
|
|
public readonly object VarType;
|
|
|
|
public VariableExpression (object var)
|
|
: this (var, (Sequence<PathElement>) null)
|
|
{
|
|
}
|
|
|
|
public VariableExpression (object var, Sequence<PathElement> path)
|
|
{
|
|
this.UnderlyingVar = var;
|
|
this.Path = path != null ? path.AsEnumerable ().ToArray () : null;
|
|
}
|
|
|
|
public VariableExpression (object var, Sequence<PathElement> path, object type)
|
|
: this (var, path)
|
|
{
|
|
this.VarType = type;
|
|
}
|
|
|
|
public VariableExpression (object var, PathElement[] path)
|
|
{
|
|
this.UnderlyingVar = var;
|
|
this.Path = path;
|
|
}
|
|
|
|
public VariableExpression (object var, PathElement[] path, object type)
|
|
: this (var, path)
|
|
{
|
|
this.VarType = type;
|
|
}
|
|
|
|
public override bool IsVariable
|
|
{
|
|
get { return true; }
|
|
}
|
|
|
|
public override object UnderlyingVariable
|
|
{
|
|
get { return this.UnderlyingVar; }
|
|
}
|
|
|
|
public override PathElement[] AccessPath
|
|
{
|
|
get { return this.Path; }
|
|
}
|
|
|
|
public override bool IsBooleanTyped
|
|
{
|
|
get { return this.Path != null && this.Path [this.Path.Length - 1].IsBooleanTyped; }
|
|
}
|
|
|
|
public override bool TryGetType (out object type)
|
|
{
|
|
type = this.VarType;
|
|
return type != null;
|
|
}
|
|
|
|
public override void AddFreeVariables (HashSet<BoxedExpression> set)
|
|
{
|
|
set.Add (this);
|
|
}
|
|
|
|
protected internal override BoxedExpression RecursiveSubstitute (BoxedExpression what, BoxedExpression replace)
|
|
{
|
|
var varExpr = what as VariableExpression;
|
|
if (varExpr != null && varExpr.UnderlyingVar.Equals (this.UnderlyingVar))
|
|
return replace;
|
|
|
|
return this;
|
|
}
|
|
|
|
public override Result ForwardDecode<Data, Result, Visitor> (PC pc, Visitor visitor, Data data)
|
|
{
|
|
return visitor.Nop (pc, data);
|
|
}
|
|
|
|
public override bool Equals (object obj)
|
|
{
|
|
if (this == obj)
|
|
return true;
|
|
var boxedExpression = obj as BoxedExpression;
|
|
if (boxedExpression != null && boxedExpression.IsVariable)
|
|
return this.UnderlyingVar.Equals (boxedExpression.UnderlyingVariable);
|
|
|
|
return false;
|
|
}
|
|
|
|
public override int GetHashCode ()
|
|
{
|
|
return this.UnderlyingVariable != null ? 0 : this.UnderlyingVariable.GetHashCode ();
|
|
}
|
|
|
|
public override BoxedExpression Substitute<Variable> (Func<Variable, BoxedExpression, BoxedExpression> map)
|
|
{
|
|
if (!(this.UnderlyingVar is Variable))
|
|
return this;
|
|
var variable = ((Variable) this.UnderlyingVar);
|
|
return map (variable, this);
|
|
}
|
|
}
|
|
#endregion
|
|
}
|
|
}
|