573 lines
20 KiB
C#
573 lines
20 KiB
C#
//
|
|
// StackToSymbolicAdapter.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.Collections.Generic;
|
|
using Mono.CodeContracts.Static.AST;
|
|
using Mono.CodeContracts.Static.AST.Visitors;
|
|
using Mono.CodeContracts.Static.ControlFlow;
|
|
using Mono.CodeContracts.Static.DataStructures;
|
|
|
|
namespace Mono.CodeContracts.Static.Analysis.HeapAnalysis {
|
|
struct StackToSymbolicAdapter<Data, Result, Visitor> : IILVisitor<APC, int, int, Data, Result>
|
|
where Visitor : IILVisitor<APC, SymbolicValue, SymbolicValue, Data, Result> {
|
|
private readonly Visitor delegatee;
|
|
private readonly HeapAnalysis parent;
|
|
|
|
public StackToSymbolicAdapter (HeapAnalysis parent, Visitor delegatee)
|
|
{
|
|
this.parent = parent;
|
|
this.delegatee = delegatee;
|
|
}
|
|
|
|
private bool PreStateLookup (APC pc, out Domain domain)
|
|
{
|
|
return this.parent.PreStateLookup (pc, out domain);
|
|
}
|
|
|
|
private bool PostStateLookup (APC pc, out Domain domain)
|
|
{
|
|
return this.parent.PostStateLookup (pc, out domain);
|
|
}
|
|
|
|
private SymbolicValue ConvertSource (APC pc, int source)
|
|
{
|
|
Domain domain;
|
|
if (!PreStateLookup (pc, out domain) || domain.IsBottom)
|
|
return new SymbolicValue ();
|
|
if (source < 0)
|
|
return new SymbolicValue (domain.VoidAddr);
|
|
|
|
SymbolicValue sv;
|
|
domain.TryGetCorrespondingValueAbstraction (source, out sv);
|
|
return sv;
|
|
}
|
|
|
|
private SymbolicValue ConvertOldSource (APC pc, int source)
|
|
{
|
|
Domain domain;
|
|
if (!PreStateLookup (pc, out domain) || domain.IsBottom)
|
|
return new SymbolicValue ();
|
|
|
|
if (source < 0)
|
|
return new SymbolicValue (domain.VoidAddr);
|
|
|
|
Domain oldDomain = AnalysisDecoder.FindOldState (pc, domain);
|
|
if (oldDomain == null)
|
|
return new SymbolicValue (domain.VoidAddr);
|
|
|
|
SymbolicValue sv;
|
|
oldDomain.TryGetCorrespondingValueAbstraction (source, out sv);
|
|
return sv;
|
|
}
|
|
|
|
private SymbolicValue ConvertDest (APC pc, int dest)
|
|
{
|
|
Domain domain;
|
|
if (!PostStateLookup (pc, out domain))
|
|
return new SymbolicValue ();
|
|
|
|
SymbolicValue sv;
|
|
domain.TryGetCorrespondingValueAbstraction (dest, out sv);
|
|
return sv;
|
|
}
|
|
|
|
private SymbolicValue ConvertOldDest (APC pc, int dest)
|
|
{
|
|
SymbolicValue sv = default(SymbolicValue);
|
|
Domain domain;
|
|
if (!PostStateLookup (pc, out domain))
|
|
return sv;
|
|
|
|
domain.OldDomain.TryGetCorrespondingValueAbstraction (dest, out sv);
|
|
return sv;
|
|
}
|
|
|
|
private SymbolicValue ConvertSourceDeref (APC pc, int source)
|
|
{
|
|
Domain domain;
|
|
if (!PreStateLookup (pc, out domain))
|
|
return new SymbolicValue ();
|
|
if (source < 0)
|
|
return new SymbolicValue (domain.VoidAddr);
|
|
|
|
SymValue addr = domain.LoadValue (source);
|
|
if (!PostStateLookup (pc, out domain))
|
|
return new SymbolicValue ();
|
|
|
|
return domain.TryLoadValue (addr);
|
|
}
|
|
|
|
private SymbolicValue TryConvertUnbox (APC pc, int source)
|
|
{
|
|
Domain domain;
|
|
if (!PreStateLookup (pc, out domain))
|
|
return new SymbolicValue ();
|
|
|
|
if (source < 0)
|
|
return new SymbolicValue (domain.VoidAddr);
|
|
|
|
SymbolicValue sv;
|
|
if (!domain.TryGetUnboxedValue (source, out sv))
|
|
domain.TryGetCorrespondingValueAbstraction (source, out sv);
|
|
return sv;
|
|
}
|
|
|
|
private ArgumentSourceWrapper<ArgList> ConvertSources<ArgList> (APC pc, ArgList args)
|
|
where ArgList : IIndexable<int>
|
|
{
|
|
return new ArgumentSourceWrapper<ArgList> (args, this.parent.GetPreState (pc));
|
|
}
|
|
|
|
private bool InsideOld (APC pc)
|
|
{
|
|
Domain domain;
|
|
return PreStateLookup (pc, out domain) && domain.OldDomain != null;
|
|
}
|
|
|
|
#region Implementation of IExpressionILVisitor<APC,int,int,Data,Result>
|
|
public Result Binary (APC pc, BinaryOperator op, int dest, int operand1, int operand2, Data data)
|
|
{
|
|
if (op != BinaryOperator.Cobjeq) {
|
|
return this.delegatee.Binary (pc, op, ConvertDest (pc, dest),
|
|
ConvertSource (pc, operand1), ConvertSource (pc, operand2),
|
|
data);
|
|
}
|
|
|
|
SymbolicValue op1 = TryConvertUnbox (pc, operand1);
|
|
SymbolicValue op2 = TryConvertUnbox (pc, operand2);
|
|
|
|
return this.delegatee.Binary (pc, op, ConvertDest (pc, dest), op1, op2, data);
|
|
}
|
|
|
|
public Result Isinst (APC pc, TypeNode type, int dest, int obj, Data data)
|
|
{
|
|
return this.delegatee.Isinst (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
|
|
}
|
|
|
|
public Result LoadNull (APC pc, int dest, Data polarity)
|
|
{
|
|
return this.delegatee.LoadNull (pc, ConvertDest (pc, dest), polarity);
|
|
}
|
|
|
|
public Result LoadConst (APC pc, TypeNode type, object constant, int dest, Data data)
|
|
{
|
|
return this.delegatee.LoadConst (pc, type, constant, ConvertDest (pc, dest), data);
|
|
}
|
|
|
|
public Result Sizeof (APC pc, TypeNode type, int dest, Data data)
|
|
{
|
|
return this.delegatee.Sizeof (pc, type, ConvertDest (pc, dest), data);
|
|
}
|
|
|
|
public Result Unary (APC pc, UnaryOperator op, bool unsigned, int dest, int source, Data data)
|
|
{
|
|
return this.delegatee.Unary (pc, op, unsigned, ConvertDest (pc, dest), ConvertSource (pc, source), data);
|
|
}
|
|
#endregion
|
|
|
|
#region Implementation of ISyntheticILVisitor<APC,int,int,Data,Result>
|
|
public Result Entry (APC pc, Method method, Data data)
|
|
{
|
|
return this.delegatee.Entry (pc, method, data);
|
|
}
|
|
|
|
public Result Assume (APC pc, EdgeTag tag, int source, Data data)
|
|
{
|
|
return this.delegatee.Assume (pc, tag, ConvertSource (pc, source), data);
|
|
}
|
|
|
|
public Result Assert (APC pc, EdgeTag tag, int source, Data data)
|
|
{
|
|
return this.delegatee.Assert (pc, tag, ConvertSource (pc, source), data);
|
|
}
|
|
|
|
public Result BeginOld (APC pc, APC matchingEnd, Data data)
|
|
{
|
|
return this.delegatee.BeginOld (pc, matchingEnd, data);
|
|
}
|
|
|
|
public Result EndOld (APC pc, APC matchingBegin, TypeNode type, int dest, int source, Data data)
|
|
{
|
|
return this.delegatee.Nop (pc, data);
|
|
}
|
|
|
|
public Result LoadStack (APC pc, int offset, int dest, int source, bool isOld, Data data)
|
|
{
|
|
SymbolicValue src = isOld ? ConvertOldSource (pc, source) : ConvertSource (pc, source);
|
|
return this.delegatee.LoadStack (pc, offset, ConvertDest (pc, dest), src, isOld, data);
|
|
}
|
|
|
|
public Result LoadStackAddress (APC pc, int offset, int dest, int source, TypeNode type, bool isOld, Data data)
|
|
{
|
|
return this.delegatee.LoadStackAddress (pc, offset, ConvertDest (pc, dest), ConvertSource (pc, source), type, isOld, data);
|
|
}
|
|
|
|
public Result LoadResult (APC pc, TypeNode type, int dest, int source, Data data)
|
|
{
|
|
return this.delegatee.LoadResult (pc, type, ConvertDest (pc, dest), ConvertSource (pc, source), data);
|
|
}
|
|
#endregion
|
|
|
|
#region Implementation of IILVisitor<APC,int,int,Data,Result>
|
|
public Result Arglist (APC pc, int dest, Data data)
|
|
{
|
|
return this.delegatee.Arglist (pc, ConvertDest (pc, dest), data);
|
|
}
|
|
|
|
public Result Branch (APC pc, APC target, bool leavesExceptionBlock, Data data)
|
|
{
|
|
return this.delegatee.Branch (pc, target, leavesExceptionBlock, data);
|
|
}
|
|
|
|
public Result BranchCond (APC pc, APC target, BranchOperator bop, int value1, int value2, Data data)
|
|
{
|
|
return this.delegatee.BranchCond (pc, target, bop, ConvertSource (pc, value1), ConvertSource (pc, value2), data);
|
|
}
|
|
|
|
public Result BranchTrue (APC pc, APC target, int cond, Data data)
|
|
{
|
|
return this.delegatee.BranchTrue (pc, target, ConvertSource (pc, cond), data);
|
|
}
|
|
|
|
public Result BranchFalse (APC pc, APC target, int cond, Data data)
|
|
{
|
|
return this.delegatee.BranchFalse (pc, target, ConvertSource (pc, cond), data);
|
|
}
|
|
|
|
public Result Break (APC pc, Data data)
|
|
{
|
|
return this.delegatee.Break (pc, data);
|
|
}
|
|
|
|
public Result Call<TypeList, ArgList> (APC pc, Method method, bool virt, TypeList extraVarargs, int dest, ArgList args, Data data)
|
|
where TypeList : IIndexable<TypeNode>
|
|
where ArgList : IIndexable<int>
|
|
{
|
|
if (!this.parent.MetaDataProvider.IsVoidMethod (method) && InsideOld (pc))
|
|
return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data);
|
|
|
|
return DelegateCall (pc, method, virt, extraVarargs, dest, args, data);
|
|
}
|
|
|
|
public Result Calli<TypeList, ArgList> (APC pc, TypeNode returnType, TypeList argTypes, bool instance, int dest, int functionPointer, ArgList args, Data data)
|
|
where TypeList : IIndexable<TypeNode>
|
|
where ArgList : IIndexable<int>
|
|
{
|
|
if (!this.parent.MetaDataProvider.IsVoid (returnType) && InsideOld (pc))
|
|
return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data);
|
|
|
|
return this.delegatee.Calli (pc, returnType, argTypes, instance,
|
|
ConvertDest (pc, dest), ConvertSource (pc, functionPointer),
|
|
ConvertSources (pc, args), data);
|
|
}
|
|
|
|
public Result CheckFinite (APC pc, int dest, int source, Data data)
|
|
{
|
|
return this.delegatee.CheckFinite (pc, ConvertDest (pc, dest), ConvertSource (pc, source), data);
|
|
}
|
|
|
|
public Result CopyBlock (APC pc, int destAddress, int srcAddress, int len, Data data)
|
|
{
|
|
return this.delegatee.CopyBlock (pc, ConvertSource (pc, destAddress), ConvertSource (pc, srcAddress), ConvertSource (pc, len), data);
|
|
}
|
|
|
|
public Result EndFilter (APC pc, int decision, Data data)
|
|
{
|
|
return this.delegatee.EndFilter (pc, ConvertSource (pc, decision), data);
|
|
}
|
|
|
|
public Result EndFinally (APC pc, Data data)
|
|
{
|
|
return this.delegatee.EndFinally (pc, data);
|
|
}
|
|
|
|
public Result Jmp (APC pc, Method method, Data data)
|
|
{
|
|
return this.delegatee.Jmp (pc, method, data);
|
|
}
|
|
|
|
public Result LoadArg (APC pc, Parameter argument, bool isOld, int dest, Data data)
|
|
{
|
|
return this.delegatee.LoadArg (pc, argument, isOld, ConvertDest (pc, dest), data);
|
|
}
|
|
|
|
public Result LoadArgAddress (APC pc, Parameter argument, bool isOld, int dest, Data data)
|
|
{
|
|
return this.delegatee.LoadArgAddress (pc, argument, isOld, ConvertDest (pc, dest), data);
|
|
}
|
|
|
|
public Result LoadLocal (APC pc, Local local, int dest, Data data)
|
|
{
|
|
return this.delegatee.LoadLocal (pc, local, ConvertDest (pc, dest), data);
|
|
}
|
|
|
|
public Result LoadLocalAddress (APC pc, Local local, int dest, Data data)
|
|
{
|
|
return this.delegatee.LoadLocalAddress (pc, local, ConvertDest (pc, dest), data);
|
|
}
|
|
|
|
public Result Nop (APC pc, Data data)
|
|
{
|
|
return this.delegatee.Nop (pc, data);
|
|
}
|
|
|
|
public Result Pop (APC pc, int source, Data data)
|
|
{
|
|
return this.delegatee.Pop (pc, ConvertSource (pc, source), data);
|
|
}
|
|
|
|
public Result Return (APC pc, int source, Data data)
|
|
{
|
|
return this.delegatee.Return (pc, ConvertSource (pc, source), data);
|
|
}
|
|
|
|
public Result StoreArg (APC pc, Parameter argument, int source, Data data)
|
|
{
|
|
return this.delegatee.StoreArg (pc, argument, ConvertSource (pc, source), data);
|
|
}
|
|
|
|
public Result StoreLocal (APC pc, Local local, int source, Data data)
|
|
{
|
|
return this.delegatee.StoreLocal (pc, local, ConvertSource (pc, source), data);
|
|
}
|
|
|
|
public Result Switch (APC pc, TypeNode type, IEnumerable<Pair<object, APC>> cases, int value, Data data)
|
|
{
|
|
return this.delegatee.Switch (pc, type, cases, ConvertSource (pc, value), data);
|
|
}
|
|
|
|
public Result Box (APC pc, TypeNode type, int dest, int source, Data data)
|
|
{
|
|
return this.delegatee.Box (pc, type, ConvertDest (pc, dest), ConvertSource (pc, source), data);
|
|
}
|
|
|
|
public Result ConstrainedCallvirt<TypeList, ArgList> (APC pc, Method method, TypeNode constraint,
|
|
TypeList extraVarargs, int dest, ArgList args, Data data)
|
|
where TypeList : IIndexable<TypeNode>
|
|
where ArgList : IIndexable<int>
|
|
{
|
|
return this.delegatee.ConstrainedCallvirt (pc, method, constraint, extraVarargs,
|
|
ConvertDest (pc, dest), ConvertSources (pc, args), data);
|
|
}
|
|
|
|
public Result CastClass (APC pc, TypeNode type, int dest, int obj, Data data)
|
|
{
|
|
return this.delegatee.CastClass (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
|
|
}
|
|
|
|
public Result CopyObj (APC pc, TypeNode type, int destPtr, int sourcePtr, Data data)
|
|
{
|
|
return this.delegatee.CopyObj (pc, type, ConvertSource (pc, destPtr), ConvertSource (pc, sourcePtr), data);
|
|
}
|
|
|
|
public Result Initobj (APC pc, TypeNode type, int ptr, Data data)
|
|
{
|
|
return this.delegatee.Initobj (pc, type, ConvertSource (pc, ptr), data);
|
|
}
|
|
|
|
public Result LoadElement (APC pc, TypeNode type, int dest, int array, int index, Data data)
|
|
{
|
|
if (InsideOld (pc))
|
|
return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data);
|
|
return this.delegatee.LoadElement (pc, type, ConvertDest (pc, dest), ConvertSource (pc, array), ConvertSource (pc, index), data);
|
|
}
|
|
|
|
public Result LoadField (APC pc, Field field, int dest, int obj, Data data)
|
|
{
|
|
if (InsideOld (pc))
|
|
return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data);
|
|
|
|
return this.delegatee.LoadField (pc, field, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
|
|
}
|
|
|
|
public Result LoadFieldAddress (APC pc, Field field, int dest, int obj, Data data)
|
|
{
|
|
return this.delegatee.LoadFieldAddress (pc, field, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
|
|
}
|
|
|
|
public Result LoadLength (APC pc, int dest, int array, Data data)
|
|
{
|
|
return this.delegatee.LoadLength (pc, ConvertDest (pc, dest), ConvertSource (pc, array), data);
|
|
}
|
|
|
|
public Result LoadStaticField (APC pc, Field field, int dest, Data data)
|
|
{
|
|
if (InsideOld (pc))
|
|
return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data);
|
|
|
|
return this.delegatee.LoadStaticField (pc, field, ConvertDest (pc, dest), data);
|
|
}
|
|
|
|
public Result LoadStaticFieldAddress (APC pc, Field field, int dest, Data data)
|
|
{
|
|
return this.delegatee.LoadStaticFieldAddress (pc, field, ConvertDest (pc, dest), data);
|
|
}
|
|
|
|
public Result LoadTypeToken (APC pc, TypeNode type, int dest, Data data)
|
|
{
|
|
return this.delegatee.LoadTypeToken (pc, type, ConvertDest (pc, dest), data);
|
|
}
|
|
|
|
public Result LoadFieldToken (APC pc, Field type, int dest, Data data)
|
|
{
|
|
return this.delegatee.LoadFieldToken (pc, type, ConvertDest (pc, dest), data);
|
|
}
|
|
|
|
public Result LoadMethodToken (APC pc, Method type, int dest, Data data)
|
|
{
|
|
return this.delegatee.LoadMethodToken (pc, type, ConvertDest (pc, dest), data);
|
|
}
|
|
|
|
public Result NewArray<ArgList> (APC pc, TypeNode type, int dest, ArgList lengths, Data data) where ArgList : IIndexable<int>
|
|
{
|
|
return this.delegatee.NewArray (pc, type, ConvertDest (pc, dest), ConvertSources (pc, lengths), data);
|
|
}
|
|
|
|
public Result NewObj<ArgList> (APC pc, Method ctor, int dest, ArgList args, Data data) where ArgList : IIndexable<int>
|
|
{
|
|
return this.delegatee.NewObj (pc, ctor, ConvertDest (pc, dest), ConvertSources (pc, args), data);
|
|
}
|
|
|
|
public Result MkRefAny (APC pc, TypeNode type, int dest, int obj, Data data)
|
|
{
|
|
return this.delegatee.MkRefAny (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
|
|
}
|
|
|
|
public Result RefAnyType (APC pc, int dest, int source, Data data)
|
|
{
|
|
return this.delegatee.RefAnyType (pc, ConvertDest (pc, dest), ConvertSource (pc, source), data);
|
|
}
|
|
|
|
public Result RefAnyVal (APC pc, TypeNode type, int dest, int source, Data data)
|
|
{
|
|
return this.delegatee.RefAnyVal (pc, type, ConvertDest (pc, dest), ConvertSource (pc, source), data);
|
|
}
|
|
|
|
public Result Rethrow (APC pc, Data data)
|
|
{
|
|
return this.delegatee.Rethrow (pc, data);
|
|
}
|
|
|
|
public Result StoreElement (APC pc, TypeNode type, int array, int index, int value, Data data)
|
|
{
|
|
return this.delegatee.StoreElement (pc, type, ConvertSource (pc, array), ConvertSource (pc, index), ConvertSource (pc, value), data);
|
|
}
|
|
|
|
public Result StoreField (APC pc, Field field, int obj, int value, Data data)
|
|
{
|
|
return this.delegatee.StoreField (pc, field, ConvertSource (pc, obj), ConvertSource (pc, value), data);
|
|
}
|
|
|
|
public Result StoreStaticField (APC pc, Field field, int value, Data data)
|
|
{
|
|
return this.delegatee.StoreStaticField (pc, field, ConvertSource (pc, value), data);
|
|
}
|
|
|
|
public Result Throw (APC pc, int exception, Data data)
|
|
{
|
|
return this.delegatee.Throw (pc, ConvertSource (pc, exception), data);
|
|
}
|
|
|
|
public Result Unbox (APC pc, TypeNode type, int dest, int obj, Data data)
|
|
{
|
|
return this.delegatee.Unbox (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
|
|
}
|
|
|
|
public Result UnboxAny (APC pc, TypeNode type, int dest, int obj, Data data)
|
|
{
|
|
return this.delegatee.UnboxAny (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
|
|
}
|
|
|
|
private Result DelegateCall<TypeList, ArgList> (APC pc, Method method, bool virt, TypeList extraVarargs, int dest, ArgList args, Data data)
|
|
where TypeList : IIndexable<TypeNode>
|
|
where ArgList : IIndexable<int>
|
|
{
|
|
TypeNode declaringType = this.parent.MetaDataProvider.DeclaringType (method);
|
|
if (args.Count == 2) {
|
|
string name = this.parent.MetaDataProvider.Name (method);
|
|
if (name == "Equals") {
|
|
return this.delegatee.Binary (pc, BinaryOperator.Cobjeq,
|
|
ConvertDest (pc, dest),
|
|
TryConvertUnbox (pc, args [0]), TryConvertUnbox (pc, args [1]), data);
|
|
}
|
|
|
|
if (this.parent.MetaDataProvider.IsReferenceType (declaringType)) {
|
|
if (name == "op_Inequality") {
|
|
return this.delegatee.Binary (pc, BinaryOperator.Cne_Un,
|
|
ConvertDest (pc, dest),
|
|
ConvertSource (pc, args [0]), ConvertSource (pc, args [1]), data);
|
|
}
|
|
if (name == "op_Equality") {
|
|
return this.delegatee.Binary (pc, BinaryOperator.Cobjeq,
|
|
ConvertDest (pc, dest),
|
|
ConvertSource (pc, args [0]), ConvertSource (pc, args [1]), data);
|
|
}
|
|
}
|
|
}
|
|
|
|
return this.delegatee.Call (pc, method, virt, extraVarargs, ConvertDest (pc, dest), ConvertSources (pc, args), data);
|
|
}
|
|
#endregion
|
|
|
|
#region Nested type: ArgumentSourceWrapper
|
|
private struct ArgumentSourceWrapper<ArgList> : IIndexable<SymbolicValue>
|
|
where ArgList : IIndexable<int> {
|
|
private readonly Domain state;
|
|
private readonly ArgList underlying;
|
|
|
|
public ArgumentSourceWrapper (ArgList underlying, Domain state)
|
|
{
|
|
this.underlying = underlying;
|
|
this.state = state;
|
|
}
|
|
|
|
#region Implementation of IIndexable<SymbolicValue>
|
|
public int Count
|
|
{
|
|
get { return this.underlying.Count; }
|
|
}
|
|
|
|
public SymbolicValue this [int index]
|
|
{
|
|
get { return Map (this.underlying [index]); }
|
|
}
|
|
|
|
private SymbolicValue Map (int i)
|
|
{
|
|
SymbolicValue sv = default(SymbolicValue);
|
|
if (this.state == null)
|
|
return sv;
|
|
|
|
this.state.TryGetCorrespondingValueAbstraction (i, out sv);
|
|
return sv;
|
|
}
|
|
#endregion
|
|
}
|
|
#endregion
|
|
}
|
|
}
|