mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.HeapAnalysis/StackToSymbolicAdapter.cs

   1 //
   2 // StackToSymbolicAdapter.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 using System.Collections.Generic;
  29 using Mono.CodeContracts.Static.AST;
  30 using Mono.CodeContracts.Static.AST.Visitors;
  31 using Mono.CodeContracts.Static.ControlFlow;
  32 using Mono.CodeContracts.Static.DataStructures;
  33
  34 namespace Mono.CodeContracts.Static.Analysis.HeapAnalysis {
  35         struct StackToSymbolicAdapter<Data, Result, Visitor> : IILVisitor<APC, int, int, Data, Result>
  36                 where Visitor : IILVisitor<APC, SymbolicValue, SymbolicValue, Data, Result> {
  37                 private readonly Visitor delegatee;
  38                 private readonly HeapAnalysis parent;
  39
  40                 public StackToSymbolicAdapter (HeapAnalysis parent, Visitor delegatee)
  41                 {
  42                         this.parent = parent;
  43                         this.delegatee = delegatee;
  44                 }
  45
  46                 private bool PreStateLookup (APC pc, out Domain domain)
  47                 {
  48                         return this.parent.PreStateLookup (pc, out domain);
  49                 }
  50
  51                 private bool PostStateLookup (APC pc, out Domain domain)
  52                 {
  53                         return this.parent.PostStateLookup (pc, out domain);
  54                 }
  55
  56                 private SymbolicValue ConvertSource (APC pc, int source)
  57                 {
  58                         Domain domain;
  59                         if (!PreStateLookup (pc, out domain) || domain.IsBottom)
  60                                 return new SymbolicValue ();
  61                         if (source < 0)
  62                                 return new SymbolicValue (domain.VoidAddr);
  63
  64                         SymbolicValue sv;
  65                         domain.TryGetCorrespondingValueAbstraction (source, out sv);
  66                         return sv;
  67                 }
  68
  69                 private SymbolicValue ConvertOldSource (APC pc, int source)
  70                 {
  71                         Domain domain;
  72                         if (!PreStateLookup (pc, out domain) || domain.IsBottom)
  73                                 return new SymbolicValue ();
  74
  75                         if (source < 0)
  76                                 return new SymbolicValue (domain.VoidAddr);
  77
  78                         Domain oldDomain = AnalysisDecoder.FindOldState (pc, domain);
  79                         if (oldDomain == null)
  80                                 return new SymbolicValue (domain.VoidAddr);
  81
  82                         SymbolicValue sv;
  83                         oldDomain.TryGetCorrespondingValueAbstraction (source, out sv);
  84                         return sv;
  85                 }
  86
  87                 private SymbolicValue ConvertDest (APC pc, int dest)
  88                 {
  89                         Domain domain;
  90                         if (!PostStateLookup (pc, out domain))
  91                                 return new SymbolicValue ();
  92
  93                         SymbolicValue sv;
  94                         domain.TryGetCorrespondingValueAbstraction (dest, out sv);
  95                         return sv;
  96                 }
  97
  98                 private SymbolicValue ConvertOldDest (APC pc, int dest)
  99                 {
 100                         SymbolicValue sv = default(SymbolicValue);
 101                         Domain domain;
 102                         if (!PostStateLookup (pc, out domain))
 103                                 return sv;
 104
 105                         domain.OldDomain.TryGetCorrespondingValueAbstraction (dest, out sv);
 106                         return sv;
 107                 }
 108
 109                 private SymbolicValue ConvertSourceDeref (APC pc, int source)
 110                 {
 111                         Domain domain;
 112                         if (!PreStateLookup (pc, out domain))
 113                                 return new SymbolicValue ();
 114                         if (source < 0)
 115                                 return new SymbolicValue (domain.VoidAddr);
 116
 117                         SymValue addr = domain.LoadValue (source);
 118                         if (!PostStateLookup (pc, out domain))
 119                                 return new SymbolicValue ();
 120
 121                         return domain.TryLoadValue (addr);
 122                 }
 123
 124                 private SymbolicValue TryConvertUnbox (APC pc, int source)
 125                 {
 126                         Domain domain;
 127                         if (!PreStateLookup (pc, out domain))
 128                                 return new SymbolicValue ();
 129
 130                         if (source < 0)
 131                                 return new SymbolicValue (domain.VoidAddr);
 132
 133                         SymbolicValue sv;
 134                         if (!domain.TryGetUnboxedValue (source, out sv))
 135                                 domain.TryGetCorrespondingValueAbstraction (source, out sv);
 136                         return sv;
 137                 }
 138
 139                 private ArgumentSourceWrapper<ArgList> ConvertSources<ArgList> (APC pc, ArgList args)
 140                         where ArgList : IIndexable<int>
 141                 {
 142                         return new ArgumentSourceWrapper<ArgList> (args, this.parent.GetPreState (pc));
 143                 }
 144
 145                 private bool InsideOld (APC pc)
 146                 {
 147                         Domain domain;
 148                         return PreStateLookup (pc, out domain) && domain.OldDomain != null;
 149                 }
 150
 151                 #region Implementation of IExpressionILVisitor<APC,int,int,Data,Result>
 152                 public Result Binary (APC pc, BinaryOperator op, int dest, int operand1, int operand2, Data data)
 153                 {
 154                         if (op != BinaryOperator.Cobjeq) {
 155                                 return this.delegatee.Binary (pc, op, ConvertDest (pc, dest),
 156                                                               ConvertSource (pc, operand1), ConvertSource (pc, operand2),
 157                                                               data);
 158                         }
 159
 160                         SymbolicValue op1 = TryConvertUnbox (pc, operand1);
 161                         SymbolicValue op2 = TryConvertUnbox (pc, operand2);
 162
 163                         return this.delegatee.Binary (pc, op, ConvertDest (pc, dest), op1, op2, data);
 164                 }
 165
 166                 public Result Isinst (APC pc, TypeNode type, int dest, int obj, Data data)
 167                 {
 168                         return this.delegatee.Isinst (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
 169                 }
 170
 171                 public Result LoadNull (APC pc, int dest, Data polarity)
 172                 {
 173                         return this.delegatee.LoadNull (pc, ConvertDest (pc, dest), polarity);
 174                 }
 175
 176                 public Result LoadConst (APC pc, TypeNode type, object constant, int dest, Data data)
 177                 {
 178                         return this.delegatee.LoadConst (pc, type, constant, ConvertDest (pc, dest), data);
 179                 }
 180
 181                 public Result Sizeof (APC pc, TypeNode type, int dest, Data data)
 182                 {
 183                         return this.delegatee.Sizeof (pc, type, ConvertDest (pc, dest), data);
 184                 }
 185
 186                 public Result Unary (APC pc, UnaryOperator op, bool unsigned, int dest, int source, Data data)
 187                 {
 188                         return this.delegatee.Unary (pc, op, unsigned, ConvertDest (pc, dest), ConvertSource (pc, source), data);
 189                 }
 190                 #endregion
 191
 192                 #region Implementation of ISyntheticILVisitor<APC,int,int,Data,Result>
 193                 public Result Entry (APC pc, Method method, Data data)
 194                 {
 195                         return this.delegatee.Entry (pc, method, data);
 196                 }
 197
 198                 public Result Assume (APC pc, EdgeTag tag, int source, Data data)
 199                 {
 200                         return this.delegatee.Assume (pc, tag, ConvertSource (pc, source), data);
 201                 }
 202
 203                 public Result Assert (APC pc, EdgeTag tag, int source, Data data)
 204                 {
 205                         return this.delegatee.Assert (pc, tag, ConvertSource (pc, source), data);
 206                 }
 207
 208                 public Result BeginOld (APC pc, APC matchingEnd, Data data)
 209                 {
 210                         return this.delegatee.BeginOld (pc, matchingEnd, data);
 211                 }
 212
 213                 public Result EndOld (APC pc, APC matchingBegin, TypeNode type, int dest, int source, Data data)
 214                 {
 215                         return this.delegatee.Nop (pc, data);
 216                 }
 217
 218                 public Result LoadStack (APC pc, int offset, int dest, int source, bool isOld, Data data)
 219                 {
 220                         SymbolicValue src = isOld ? ConvertOldSource (pc, source) : ConvertSource (pc, source);
 221                         return this.delegatee.LoadStack (pc, offset, ConvertDest (pc, dest), src, isOld, data);
 222                 }
 223
 224                 public Result LoadStackAddress (APC pc, int offset, int dest, int source, TypeNode type, bool isOld, Data data)
 225                 {
 226                         return this.delegatee.LoadStackAddress (pc, offset, ConvertDest (pc, dest), ConvertSource (pc, source), type, isOld, data);
 227                 }
 228
 229                 public Result LoadResult (APC pc, TypeNode type, int dest, int source, Data data)
 230                 {
 231                         return this.delegatee.LoadResult (pc, type, ConvertDest (pc, dest), ConvertSource (pc, source), data);
 232                 }
 233                 #endregion
 234
 235                 #region Implementation of IILVisitor<APC,int,int,Data,Result>
 236                 public Result Arglist (APC pc, int dest, Data data)
 237                 {
 238                         return this.delegatee.Arglist (pc, ConvertDest (pc, dest), data);
 239                 }
 240
 241                 public Result Branch (APC pc, APC target, bool leavesExceptionBlock, Data data)
 242                 {
 243                         return this.delegatee.Branch (pc, target, leavesExceptionBlock, data);
 244                 }
 245
 246                 public Result BranchCond (APC pc, APC target, BranchOperator bop, int value1, int value2, Data data)
 247                 {
 248                         return this.delegatee.BranchCond (pc, target, bop, ConvertSource (pc, value1), ConvertSource (pc, value2), data);
 249                 }
 250
 251                 public Result BranchTrue (APC pc, APC target, int cond, Data data)
 252                 {
 253                         return this.delegatee.BranchTrue (pc, target, ConvertSource (pc, cond), data);
 254                 }
 255
 256                 public Result BranchFalse (APC pc, APC target, int cond, Data data)
 257                 {
 258                         return this.delegatee.BranchFalse (pc, target, ConvertSource (pc, cond), data);
 259                 }
 260
 261                 public Result Break (APC pc, Data data)
 262                 {
 263                         return this.delegatee.Break (pc, data);
 264                 }
 265
 266                 public Result Call<TypeList, ArgList> (APC pc, Method method, bool virt, TypeList extraVarargs, int dest, ArgList args, Data data)
 267                         where TypeList : IIndexable<TypeNode>
 268                         where ArgList : IIndexable<int>
 269                 {
 270                         if (!this.parent.MetaDataProvider.IsVoidMethod (method) && InsideOld (pc))
 271                                 return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data);
 272
 273                         return DelegateCall (pc, method, virt, extraVarargs, dest, args, data);
 274                 }
 275
 276                 public Result Calli<TypeList, ArgList> (APC pc, TypeNode returnType, TypeList argTypes, bool instance, int dest, int functionPointer, ArgList args, Data data)
 277                         where TypeList : IIndexable<TypeNode>
 278                         where ArgList : IIndexable<int>
 279                 {
 280                         if (!this.parent.MetaDataProvider.IsVoid (returnType) && InsideOld (pc))
 281                                 return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data);
 282
 283                         return this.delegatee.Calli (pc, returnType, argTypes, instance,
 284                                                      ConvertDest (pc, dest), ConvertSource (pc, functionPointer),
 285                                                      ConvertSources (pc, args), data);
 286                 }
 287
 288                 public Result CheckFinite (APC pc, int dest, int source, Data data)
 289                 {
 290                         return this.delegatee.CheckFinite (pc, ConvertDest (pc, dest), ConvertSource (pc, source), data);
 291                 }
 292
 293                 public Result CopyBlock (APC pc, int destAddress, int srcAddress, int len, Data data)
 294                 {
 295                         return this.delegatee.CopyBlock (pc, ConvertSource (pc, destAddress), ConvertSource (pc, srcAddress), ConvertSource (pc, len), data);
 296                 }
 297
 298                 public Result EndFilter (APC pc, int decision, Data data)
 299                 {
 300                         return this.delegatee.EndFilter (pc, ConvertSource (pc, decision), data);
 301                 }
 302
 303                 public Result EndFinally (APC pc, Data data)
 304                 {
 305                         return this.delegatee.EndFinally (pc, data);
 306                 }
 307
 308                 public Result Jmp (APC pc, Method method, Data data)
 309                 {
 310                         return this.delegatee.Jmp (pc, method, data);
 311                 }
 312
 313                 public Result LoadArg (APC pc, Parameter argument, bool isOld, int dest, Data data)
 314                 {
 315                         return this.delegatee.LoadArg (pc, argument, isOld, ConvertDest (pc, dest), data);
 316                 }
 317
 318                 public Result LoadArgAddress (APC pc, Parameter argument, bool isOld, int dest, Data data)
 319                 {
 320                         return this.delegatee.LoadArgAddress (pc, argument, isOld, ConvertDest (pc, dest), data);
 321                 }
 322
 323                 public Result LoadLocal (APC pc, Local local, int dest, Data data)
 324                 {
 325                         return this.delegatee.LoadLocal (pc, local, ConvertDest (pc, dest), data);
 326                 }
 327
 328                 public Result LoadLocalAddress (APC pc, Local local, int dest, Data data)
 329                 {
 330                         return this.delegatee.LoadLocalAddress (pc, local, ConvertDest (pc, dest), data);
 331                 }
 332
 333                 public Result Nop (APC pc, Data data)
 334                 {
 335                         return this.delegatee.Nop (pc, data);
 336                 }
 337
 338                 public Result Pop (APC pc, int source, Data data)
 339                 {
 340                         return this.delegatee.Pop (pc, ConvertSource (pc, source), data);
 341                 }
 342
 343                 public Result Return (APC pc, int source, Data data)
 344                 {
 345                         return this.delegatee.Return (pc, ConvertSource (pc, source), data);
 346                 }
 347
 348                 public Result StoreArg (APC pc, Parameter argument, int source, Data data)
 349                 {
 350                         return this.delegatee.StoreArg (pc, argument, ConvertSource (pc, source), data);
 351                 }
 352
 353                 public Result StoreLocal (APC pc, Local local, int source, Data data)
 354                 {
 355                         return this.delegatee.StoreLocal (pc, local, ConvertSource (pc, source), data);
 356                 }
 357
 358                 public Result Switch (APC pc, TypeNode type, IEnumerable<Pair<object, APC>> cases, int value, Data data)
 359                 {
 360                         return this.delegatee.Switch (pc, type, cases, ConvertSource (pc, value), data);
 361                 }
 362
 363                 public Result Box (APC pc, TypeNode type, int dest, int source, Data data)
 364                 {
 365                         return this.delegatee.Box (pc, type, ConvertDest (pc, dest), ConvertSource (pc, source), data);
 366                 }
 367
 368                 public Result ConstrainedCallvirt<TypeList, ArgList> (APC pc, Method method, TypeNode constraint,
 369                                                                       TypeList extraVarargs, int dest, ArgList args, Data data)
 370                         where TypeList : IIndexable<TypeNode>
 371                         where ArgList : IIndexable<int>
 372                 {
 373                         return this.delegatee.ConstrainedCallvirt (pc, method, constraint, extraVarargs,
 374                                                                    ConvertDest (pc, dest), ConvertSources (pc, args), data);
 375                 }
 376
 377                 public Result CastClass (APC pc, TypeNode type, int dest, int obj, Data data)
 378                 {
 379                         return this.delegatee.CastClass (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
 380                 }
 381
 382                 public Result CopyObj (APC pc, TypeNode type, int destPtr, int sourcePtr, Data data)
 383                 {
 384                         return this.delegatee.CopyObj (pc, type, ConvertSource (pc, destPtr), ConvertSource (pc, sourcePtr), data);
 385                 }
 386
 387                 public Result Initobj (APC pc, TypeNode type, int ptr, Data data)
 388                 {
 389                         return this.delegatee.Initobj (pc, type, ConvertSource (pc, ptr), data);
 390                 }
 391
 392                 public Result LoadElement (APC pc, TypeNode type, int dest, int array, int index, Data data)
 393                 {
 394                         if (InsideOld (pc))
 395                                 return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data);
 396                         return this.delegatee.LoadElement (pc, type, ConvertDest (pc, dest), ConvertSource (pc, array), ConvertSource (pc, index), data);
 397                 }
 398
 399                 public Result LoadField (APC pc, Field field, int dest, int obj, Data data)
 400                 {
 401                         if (InsideOld (pc))
 402                                 return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data);
 403
 404                         return this.delegatee.LoadField (pc, field, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
 405                 }
 406
 407                 public Result LoadFieldAddress (APC pc, Field field, int dest, int obj, Data data)
 408                 {
 409                         return this.delegatee.LoadFieldAddress (pc, field, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
 410                 }
 411
 412                 public Result LoadLength (APC pc, int dest, int array, Data data)
 413                 {
 414                         return this.delegatee.LoadLength (pc, ConvertDest (pc, dest), ConvertSource (pc, array), data);
 415                 }
 416
 417                 public Result LoadStaticField (APC pc, Field field, int dest, Data data)
 418                 {
 419                         if (InsideOld (pc))
 420                                 return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data);
 421
 422                         return this.delegatee.LoadStaticField (pc, field, ConvertDest (pc, dest), data);
 423                 }
 424
 425                 public Result LoadStaticFieldAddress (APC pc, Field field, int dest, Data data)
 426                 {
 427                         return this.delegatee.LoadStaticFieldAddress (pc, field, ConvertDest (pc, dest), data);
 428                 }
 429
 430                 public Result LoadTypeToken (APC pc, TypeNode type, int dest, Data data)
 431                 {
 432                         return this.delegatee.LoadTypeToken (pc, type, ConvertDest (pc, dest), data);
 433                 }
 434
 435                 public Result LoadFieldToken (APC pc, Field type, int dest, Data data)
 436                 {
 437                         return this.delegatee.LoadFieldToken (pc, type, ConvertDest (pc, dest), data);
 438                 }
 439
 440                 public Result LoadMethodToken (APC pc, Method type, int dest, Data data)
 441                 {
 442                         return this.delegatee.LoadMethodToken (pc, type, ConvertDest (pc, dest), data);
 443                 }
 444
 445                 public Result NewArray<ArgList> (APC pc, TypeNode type, int dest, ArgList lengths, Data data) where ArgList : IIndexable<int>
 446                 {
 447                         return this.delegatee.NewArray (pc, type, ConvertDest (pc, dest), ConvertSources (pc, lengths), data);
 448                 }
 449
 450                 public Result NewObj<ArgList> (APC pc, Method ctor, int dest, ArgList args, Data data) where ArgList : IIndexable<int>
 451                 {
 452                         return this.delegatee.NewObj (pc, ctor, ConvertDest (pc, dest), ConvertSources (pc, args), data);
 453                 }
 454
 455                 public Result MkRefAny (APC pc, TypeNode type, int dest, int obj, Data data)
 456                 {
 457                         return this.delegatee.MkRefAny (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
 458                 }
 459
 460                 public Result RefAnyType (APC pc, int dest, int source, Data data)
 461                 {
 462                         return this.delegatee.RefAnyType (pc, ConvertDest (pc, dest), ConvertSource (pc, source), data);
 463                 }
 464
 465                 public Result RefAnyVal (APC pc, TypeNode type, int dest, int source, Data data)
 466                 {
 467                         return this.delegatee.RefAnyVal (pc, type, ConvertDest (pc, dest), ConvertSource (pc, source), data);
 468                 }
 469
 470                 public Result Rethrow (APC pc, Data data)
 471                 {
 472                         return this.delegatee.Rethrow (pc, data);
 473                 }
 474
 475                 public Result StoreElement (APC pc, TypeNode type, int array, int index, int value, Data data)
 476                 {
 477                         return this.delegatee.StoreElement (pc, type, ConvertSource (pc, array), ConvertSource (pc, index), ConvertSource (pc, value), data);
 478                 }
 479
 480                 public Result StoreField (APC pc, Field field, int obj, int value, Data data)
 481                 {
 482                         return this.delegatee.StoreField (pc, field, ConvertSource (pc, obj), ConvertSource (pc, value), data);
 483                 }
 484
 485                 public Result StoreStaticField (APC pc, Field field, int value, Data data)
 486                 {
 487                         return this.delegatee.StoreStaticField (pc, field, ConvertSource (pc, value), data);
 488                 }
 489
 490                 public Result Throw (APC pc, int exception, Data data)
 491                 {
 492                         return this.delegatee.Throw (pc, ConvertSource (pc, exception), data);
 493                 }
 494
 495                 public Result Unbox (APC pc, TypeNode type, int dest, int obj, Data data)
 496                 {
 497                         return this.delegatee.Unbox (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
 498                 }
 499
 500                 public Result UnboxAny (APC pc, TypeNode type, int dest, int obj, Data data)
 501                 {
 502                         return this.delegatee.UnboxAny (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data);
 503                 }
 504
 505                 private Result DelegateCall<TypeList, ArgList> (APC pc, Method method, bool virt, TypeList extraVarargs, int dest, ArgList args, Data data)
 506                         where TypeList : IIndexable<TypeNode>
 507                         where ArgList : IIndexable<int>
 508                 {
 509                         TypeNode declaringType = this.parent.MetaDataProvider.DeclaringType (method);
 510                         if (args.Count == 2) {
 511                                 string name = this.parent.MetaDataProvider.Name (method);
 512                                 if (name == "Equals") {
 513                                         return this.delegatee.Binary (pc, BinaryOperator.Cobjeq,
 514                                                                       ConvertDest (pc, dest),
 515                                                                       TryConvertUnbox (pc, args [0]), TryConvertUnbox (pc, args [1]), data);
 516                                 }
 517
 518                                 if (this.parent.MetaDataProvider.IsReferenceType (declaringType)) {
 519                                         if (name == "op_Inequality") {
 520                                                 return this.delegatee.Binary (pc, BinaryOperator.Cne_Un,
 521                                                                               ConvertDest (pc, dest),
 522                                                                               ConvertSource (pc, args [0]), ConvertSource (pc, args [1]), data);
 523                                         }
 524                                         if (name == "op_Equality") {
 525                                                 return this.delegatee.Binary (pc, BinaryOperator.Cobjeq,
 526                                                                               ConvertDest (pc, dest),
 527                                                                               ConvertSource (pc, args [0]), ConvertSource (pc, args [1]), data);
 528                                         }
 529                                 }
 530                         }
 531
 532                         return this.delegatee.Call (pc, method, virt, extraVarargs, ConvertDest (pc, dest), ConvertSources (pc, args), data);
 533                 }
 534                 #endregion
 535
 536                 #region Nested type: ArgumentSourceWrapper
 537                 private struct ArgumentSourceWrapper<ArgList> : IIndexable<SymbolicValue>
 538                         where ArgList : IIndexable<int> {
 539                         private readonly Domain state;
 540                         private readonly ArgList underlying;
 541
 542                         public ArgumentSourceWrapper (ArgList underlying, Domain state)
 543                         {
 544                                 this.underlying = underlying;
 545                                 this.state = state;
 546                         }
 547
 548                         #region Implementation of IIndexable<SymbolicValue>
 549                         public int Count
 550                         {
 551                                 get { return this.underlying.Count; }
 552                         }
 553
 554                         public SymbolicValue this [int index]
 555                         {
 556                                 get { return Map (this.underlying [index]); }
 557                         }
 558
 559                         private SymbolicValue Map (int i)
 560                         {
 561                                 SymbolicValue sv = default(SymbolicValue);
 562                                 if (this.state == null)
 563                                         return sv;
 564
 565                                 this.state.TryGetCorrespondingValueAbstraction (i, out sv);
 566                                 return sv;
 567                         }
 568                         #endregion
 569                         }
 570                 #endregion
 571         }
 572 }