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

   1 //
   2 // AnalysisDecoder.cs
   3 //
   4 // Authors:
   5 //      Alexander Chebaturkin (chebaturkin@gmail.com)
   6 //
   7 // Copyright (C) 2011 Alexander Chebaturkin
   8 //
   9 // Permission is hereby granted, free of charge, to any person obtaining
  10 // a copy of this software and associated documentation files (the
  11 // "Software"), to deal in the Software without restriction, including
  12 // without limitation the rights to use, copy, modify, merge, publish,
  13 // distribute, sublicense, and/or sell copies of the Software, and to
  14 // permit persons to whom the Software is furnished to do so, subject to
  15 // the following conditions:
  16 //
  17 // The above copyright notice and this permission notice shall be
  18 // included in all copies or substantial portions of the Software.
  19 //
  20 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
  21 // EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
  22 // MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  23 // NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
  24 // LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
  25 // OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
  26 // WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  27 //
  28
  29 using System;
  30 using System.Collections.Generic;
  31 using Mono.CodeContracts.Static.AST;
  32 using Mono.CodeContracts.Static.AST.Visitors;
  33 using Mono.CodeContracts.Static.ControlFlow;
  34 using Mono.CodeContracts.Static.DataStructures;
  35 using Mono.CodeContracts.Static.Lattices;
  36 using Mono.CodeContracts.Static.Providers;
  37
  38 namespace Mono.CodeContracts.Static.Analysis.HeapAnalysis {
  39         struct AnalysisDecoder : IILVisitor<APC, int, int, Domain, Domain> {
  40                 private readonly HeapAnalysis parent;
  41
  42                 public AnalysisDecoder (HeapAnalysis parent)
  43                 {
  44                         this.parent = parent;
  45                 }
  46
  47                 public IContractProvider ContractProvider
  48                 {
  49                         get { return this.parent.ContractProvider; }
  50                 }
  51
  52                 public IMetaDataProvider MetaDataProvider
  53                 {
  54                         get { return this.parent.MetaDataProvider; }
  55                 }
  56                 #region Helper Methods
  57                 private void UnaryEffect (UnaryOperator op, int dest, int source, Domain data)
  58                 {
  59                         switch (op)
  60                         {
  61                         case UnaryOperator.Conv_i:
  62                                 data.AssignValueAndNullnessAtConv_IU (dest, source, false);
  63                                 break;
  64                         case UnaryOperator.Conv_u:
  65                                 data.AssignValueAndNullnessAtConv_IU (dest, source, true);
  66                                 break;
  67                         case UnaryOperator.Not:
  68                                 data.AssignSpecialUnary (dest, data.Functions.UnaryNot, source, MetaDataProvider.System_Int32);
  69                                 break;
  70                         default:
  71                                 data.AssignPureUnary (dest, op, data.UnaryResultType (op, data.CurrentType (source)), source);
  72                                 break;
  73                         }
  74                 }
  75
  76                 private Domain BinaryEffect (APC pc, BinaryOperator op, int dest, int op1, int op2, Domain data)
  77                 {
  78                         FlatDomain<TypeNode> resultType = data.BinaryResultType (op, data.CurrentType (op1), data.CurrentType (op2));
  79                         switch (op) {
  80                         case BinaryOperator.Ceq:
  81                         case BinaryOperator.Cobjeq:
  82                                 {
  83                                         SymValue srcValue = data.Value (op1);
  84                                         if (data.IsZero (srcValue)) {
  85                                                 data.AssignSpecialUnary (dest, data.Functions.UnaryNot, op2, resultType);
  86                                                 break;
  87                                         }
  88                                         SymValue val2 = data.Value (op2);
  89                                         if (data.IsZero (val2)) {
  90                                                 data.AssignSpecialUnary (dest, data.Functions.UnaryNot, op1, resultType);
  91                                                 break;
  92                                         }
  93                                         goto default;
  94                                 }
  95                         case BinaryOperator.Cne_Un:
  96                                 {
  97                                         SymValue val1 = data.Value (op1);
  98                                         if (data.IsZero (val1)) {
  99                                                 data.AssignSpecialUnary (dest, data.Functions.NeZero, op2, resultType);
 100                                                 break;
 101                                         }
 102                                         SymValue val2 = data.Value (op2);
 103                                         if (data.IsZero (val2)) {
 104                                                 data.AssignSpecialUnary (dest, data.Functions.NeZero, op1, resultType);
 105                                                 break;
 106                                         }
 107                                         goto default;
 108                                 }
 109                         default:
 110                                 data.AssignPureBinary (dest, op, resultType, op1, op2);
 111                                 break;
 112                         }
 113
 114                         data.Havoc (2);
 115                         return data;
 116                 }
 117
 118                 private void LoadArgEffect (Parameter argument, bool isOld, int dest, Domain data)
 119                 {
 120                         SymValue address = isOld ? data.OldValueAddress (argument) : data.Address (argument);
 121                         IMetaDataProvider metadataDecoder = MetaDataProvider;
 122                         data.CopyValue (data.Address (dest), address, metadataDecoder.ManagedPointer (metadataDecoder.ParameterType (argument)));
 123                 }
 124
 125                 private void StoreLocalEffect (Local local, int source, Domain data)
 126                 {
 127                         data.CopyValue (data.Address (local), data.Address (source), MetaDataProvider.ManagedPointer (MetaDataProvider.LocalType (local)));
 128                         data.Havoc (source);
 129                 }
 130
 131                 private void IsinstEffect (TypeNode type, int dest, Domain data)
 132                 {
 133                         data.AssignValue (dest, type);
 134                 }
 135
 136                 private void LoadLocalEffect (Local local, int dest, Domain data)
 137                 {
 138                         data.CopyValue (data.Address (dest), data.Address (local), MetaDataProvider.ManagedPointer (MetaDataProvider.LocalType (local)));
 139                 }
 140
 141                 private Domain AssumeEffect (APC pc, EdgeTag tag, int condition, Domain data)
 142                 {
 143                         data = data.Assume (condition, tag != EdgeTag.False);
 144                         if (!data.IsBottom)
 145                                 data.Havoc (condition);
 146
 147                         return data;
 148                 }
 149
 150                 private Domain AssertEffect (APC pc, EdgeTag tag, int condition, Domain data)
 151                 {
 152                         data = data.Assume (condition, true);
 153                         if (!data.IsBottom)
 154                                 data.Havoc (condition);
 155
 156                         return data;
 157                 }
 158
 159                 private static void LoadStackAddressEffect (APC pc, int offset, int dest, int source, Domain data)
 160                 {
 161                         data.CopyStackAddress (data.Address (dest), source);
 162                 }
 163
 164                 private Domain CallEffect<TypeList, ArgList> (APC pc, Method method, bool virt, TypeList extraVarargs, int dest, ArgList args, Domain data, TypeNode constraint, bool constrainedCall)
 165                         where TypeList : IIndexable<TypeNode>
 166                         where ArgList : IIndexable<int>
 167                 {
 168                         TypeNode t = constraint;
 169                         if (!pc.InsideContract)
 170                                 data.ResetModifiedAtCall ();
 171
 172                         IImmutableMap<TypeNode, TypeNode> instantiationMap = ComputeTypeInstantiationMap (pc, method);
 173                         bool derefThis = false;
 174                         if (virt)
 175                         {
 176                                 if (MetaDataProvider.IsStruct (constraint))
 177                                         DevirtualizeImplementingMethod (constraint, ref method);
 178                                 else
 179                                 {
 180                                         if (constrainedCall && MetaDataProvider.IsReferenceType (Specialize (instantiationMap, constraint)))
 181                                                 derefThis = true;
 182                                         SymValue loc = data.Value (args[0]);
 183                                         if (derefThis)
 184                                                 loc = data.Value (loc);
 185                                         AbstractType aType = data.GetType (loc);
 186                                         if (aType.IsNormal)
 187                                                 DevirtualizeImplementingMethod (aType.ConcreteType, ref method);
 188                                 }
 189                         }
 190                         string name = MetaDataProvider.Name (method);
 191                         if (args.Count > 0)
 192                         {
 193                                 if ((MetaDataProvider.Equal (t, MetaDataProvider.System_String) || MetaDataProvider.Equal (t, MetaDataProvider.System_Array))
 194                                     && (name == "get_Length" || name == "get_LongLength"))
 195                                 {
 196                                         data.AssignArrayLength (data.Address (dest), data.Value (args[0]));
 197                                         return data;
 198                                 }
 199                                 if (MetaDataProvider.Equal (t, MetaDataProvider.System_Object) && name == "MemberwiseClone")
 200                                 {
 201                                         TypeNode t2 = data.GetType (data.Value (args[0])).ConcreteType;
 202                                         SymValue obj = data.CreateObject (t2);
 203                                         data.CopyStructValue (obj, data.Value (args[0]), t2);
 204                                         data.CopyAddress (data.Address (dest), obj, t2);
 205                                         return data;
 206                                 }
 207                                 if (args.Count > 1 && MetaDataProvider.IsReferenceType (t))
 208                                 {
 209                                         if (name.EndsWith ("op_Inequality"))
 210                                                 return Binary (pc, BinaryOperator.Cne_Un, dest, args[0], args[1], data);
 211                                         if (name.EndsWith ("op_Equality"))
 212                                                 return Binary (pc, BinaryOperator.Cobjeq, dest, args[0], args[1], data);
 213                                 }
 214                                 if (MetaDataProvider.Equal (t, MetaDataProvider.System_IntPtr) && name.StartsWith ("op_Explicit"))
 215                                 {
 216                                         data.Copy (dest, args[0]);
 217                                         return data;
 218                                 }
 219                         }
 220                         //todo:
 221                         //                              if (extraVarargs.Count == 0 && !this.MetaDataProvider.IsVoidMethod(method) && this.ContractProvider.)
 222
 223                         {
 224                                 Property property;
 225                                 if (MetaDataProvider.IsPropertySetter (method, out property))
 226                                 {
 227                                         if (args.Count <= 2)
 228                                         {
 229                                                 Method getter;
 230                                                 if (MetaDataProvider.HasGetter (property, out getter))
 231                                                 {
 232                                                         SymValue obj;
 233                                                         SymValue srcAddr;
 234                                                         if (args.Count == 1)
 235                                                         {
 236                                                                 obj = data.Globals;
 237                                                                 srcAddr = data.Address (args[0]);
 238                                                         }
 239                                                         else
 240                                                         {
 241                                                                 obj = data.Value (args[0]);
 242                                                                 if (derefThis)
 243                                                                         obj = data.Value (obj);
 244                                                                 srcAddr = data.Address (args[1]);
 245                                                         }
 246                                                         if (MetaDataProvider.Equal (MetaDataProvider.DeclaringType (this.parent.CurrentMethod), MetaDataProvider.Unspecialized (MetaDataProvider.DeclaringType (method))))
 247                                                         {
 248                                                                 data.HavocUp (obj, ref data.ModifiedAtCall, false);
 249
 250                                                                 if (MetaDataProvider.IsAutoPropertyMember (method))
 251                                                                 {
 252                                                                         foreach (Field f in this.parent.StackContextProvider.MethodContext.Modifies (method))
 253                                                                         {
 254                                                                                 TypeNode fieldAddressType;
 255                                                                                 SymValue destAddr = data.FieldAddress (obj, f, out fieldAddressType);
 256                                                                                 data.CopyValue (destAddr, srcAddr, fieldAddressType);
 257                                                                         }
 258                                                                 }
 259                                                                 else
 260                                                                         data.HavocFields (obj, this.parent.StackContextProvider.MethodContext.Modifies (method), ref data.ModifiedAtCall);
 261                                                         }
 262                                                         TypeNode pseudoFieldAddressType;
 263                                                         SymValue destAddr1 = data.PseudoFieldAddress (obj, getter, out pseudoFieldAddressType, true);
 264                                                         data.CopyValue (destAddr1, srcAddr, pseudoFieldAddressType);
 265                                                         data.AssignValue (dest, MetaDataProvider.System_Void);
 266                                                         return data;
 267                                                 }
 268                                         }
 269                                         else
 270                                         {
 271                                                 Method getter;
 272                                                 if (MetaDataProvider.HasGetter (property, out getter))
 273                                                 {
 274                                                         var args1 = new SymValue[GetNonOutArgs (method) - 1];
 275                                                         int num = 0;
 276                                                         for (int i = 0; i < args.Count - 1; i++)
 277                                                         {
 278                                                                 bool isOut;
 279                                                                 SymValue sv = KeyForPureFunctionArgument (method, i, args[i], data, instantiationMap, out isOut);
 280                                                                 if (!isOut)
 281                                                                         args1[num++] = sv;
 282                                                         }
 283                                                         SymValue thisSV = data.Value (args[0]);
 284                                                         if (derefThis)
 285                                                                 thisSV = data.Value (thisSV);
 286                                                         TypeNode pseudoFieldAddressType;
 287                                                         SymValue pseudoField = data.PseudoFieldAddress (args1, getter, out pseudoFieldAddressType, false);
 288                                                         AssignAllOutParameters (data, pseudoField, method, args);
 289                                                         SymValue srcAddr = data.Address (args[args.Count - 1]);
 290                                                         data.CopyValue (pseudoField, srcAddr, pseudoFieldAddressType);
 291                                                         if (MetaDataProvider.Equal (MetaDataProvider.DeclaringType (this.parent.CurrentMethod), MetaDataProvider.Unspecialized (MetaDataProvider.DeclaringType (method))))
 292                                                         {
 293                                                                 data.HavocUp (thisSV, ref data.ModifiedAtCall, false);
 294                                                                 data.HavocFields (thisSV, this.parent.StackContextProvider.MethodContext.Modifies (method), ref data.ModifiedAtCall);
 295                                                         }
 296                                                 }
 297                                                 data.AssignValue (dest, MetaDataProvider.System_Void);
 298                                                 return data;
 299                                         }
 300                                 }
 301                                 bool insideConstructor = MetaDataProvider.IsConstructor (method);
 302                                 HavocParameters (pc, method, extraVarargs, args, data, constraint, insideConstructor, false, derefThis);
 303                                 data.AssignReturnValue (dest, MetaDataProvider.ReturnType (method));
 304                                 return data;
 305                         }
 306                 }
 307
 308                 private static Domain DoWithBothDomains (Domain data, Func<Domain, Domain> action)
 309                 {
 310                         data = action (data);
 311                         if (data.OldDomain != null)
 312                                 data.OldDomain = action (data.OldDomain);
 313                         return data;
 314                 }
 315
 316                 private static Domain DoWithBothDomains (Domain data, Action<Domain> action)
 317                 {
 318                         action (data);
 319                         if (data.OldDomain != null)
 320                                 action (data.OldDomain);
 321                         return data;
 322                 }
 323                 #endregion
 324
 325                 #region IILVisitor<APC,int,int,Domain,Domain> Members
 326                 public Domain Binary (APC pc, BinaryOperator op, int dest, int operand1, int operand2, Domain data)
 327                 {
 328                         AnalysisDecoder it = this;
 329                         return DoWithBothDomains (data, d => it.BinaryEffect (pc, op, dest, operand1, operand2, d));
 330                 }
 331
 332                 public Domain Isinst (APC pc, TypeNode type, int dest, int obj, Domain data)
 333                 {
 334                         AnalysisDecoder it = this;
 335                         return DoWithBothDomains (data, d => it.IsinstEffect (type, dest, d));
 336                 }
 337
 338                 public Domain LoadNull (APC pc, int dest, Domain polarity)
 339                 {
 340                         return DoWithBothDomains (polarity, d => d.AssignNull (dest));
 341                 }
 342
 343                 public Domain LoadConst (APC pc, TypeNode type, object constant, int dest, Domain data)
 344                 {
 345                         return DoWithBothDomains (data, d => d.AssignConst (dest, type, constant));
 346                 }
 347
 348                 public Domain Sizeof (APC pc, TypeNode type, int dest, Domain data)
 349                 {
 350                         AnalysisDecoder it = this;
 351                         return DoWithBothDomains (data, d => d.AssignValue (dest, it.MetaDataProvider.System_Int32));
 352                 }
 353
 354                 public Domain Unary (APC pc, UnaryOperator op, bool unsigned, int dest, int source, Domain data)
 355                 {
 356                         AnalysisDecoder it = this;
 357                         return DoWithBothDomains (data, d => it.UnaryEffect (op, dest, source, d));
 358                 }
 359
 360                 public Domain Entry (APC pc, Method method, Domain data)
 361                 {
 362                         IIndexable<Local> locals = MetaDataProvider.Locals (method);
 363                         for (int i = 0; i < locals.Count; i++)
 364                                 MaterializeLocal (locals [i], method, data);
 365
 366                         TypeNode declaringType = MetaDataProvider.DeclaringType (method);
 367                         IIndexable<Parameter> parameters = MetaDataProvider.Parameters (method);
 368                         for (int i = 0; i < parameters.Count; i++)
 369                                 MaterializeParameter (parameters [i], declaringType, data, false);
 370
 371                         if (!MetaDataProvider.IsStatic (method))
 372                                 MaterializeParameter (MetaDataProvider.This (method), declaringType, data, true);
 373
 374                         if (MetaDataProvider.IsConstructor (method)) {
 375                                 Parameter p = MetaDataProvider.This (method);
 376                                 SymValue ptr = data.Value (p);
 377
 378                                 foreach (Field field in MetaDataProvider.Fields (declaringType)) {
 379                                         if (MetaDataProvider.IsStatic (field))
 380                                                 continue;
 381
 382                                         TypeNode fieldType = MetaDataProvider.FieldType (field);
 383                                         if (MetaDataProvider.IsStruct (fieldType))
 384                                                 data.AssignConst (data.FieldAddress (ptr, field), fieldType, 0);
 385                                         else
 386                                                 data.AssignNull (data.FieldAddress (ptr, field));
 387                                 }
 388
 389                                 foreach (Property property in MetaDataProvider.Properties (declaringType)) {
 390                                         Method getter;
 391                                         if (!MetaDataProvider.IsStatic (property) && MetaDataProvider.HasGetter (property, out getter)
 392                                             && MetaDataProvider.IsCompilerGenerated (getter) && MetaDataProvider.Parameters (getter).Count == 0) {
 393                                                 TypeNode propertyType = MetaDataProvider.ReturnType (getter);
 394                                                 if (MetaDataProvider.IsStruct (propertyType))
 395                                                         data.AssignConst (data.PseudoFieldAddress (ptr, getter), propertyType, 0);
 396                                                 else
 397                                                         data.AssignNull (data.PseudoFieldAddress (ptr, getter));
 398                                         }
 399                                 }
 400                         }
 401
 402                         return data;
 403                 }
 404
 405                 public Domain Assume (APC pc, EdgeTag tag, int condition, Domain data)
 406                 {
 407                         AnalysisDecoder it = this;
 408                         return DoWithBothDomains (data, d => it.AssumeEffect (pc, tag, condition, data));
 409                 }
 410
 411                 public Domain Assert (APC pc, EdgeTag tag, int condition, Domain data)
 412                 {
 413                         AnalysisDecoder it = this;
 414                         return DoWithBothDomains (data, d => it.AssertEffect (pc, tag, condition, data));
 415                 }
 416
 417                 public Domain BeginOld (APC pc, APC matchingEnd, Domain data)
 418                 {
 419                         if (data.InsideOld++ == 0) {
 420                                 Domain oldState = FindOldState (pc, data);
 421                                 if (oldState == null)
 422                                         throw new InvalidOperationException ("begin_old in weird calling context");
 423                                 Domain domain = oldState.Clone ();
 424                                 domain.BeginOldPC = pc;
 425                                 data.OldDomain = domain;
 426                         }
 427
 428                         return data;
 429                 }
 430
 431                 public Domain EndOld (APC pc, APC matchingBegin, TypeNode type, int dest, int source, Domain data)
 432                 {
 433                         if (--data.InsideOld == 0)
 434                                 data.OldDomain = null;
 435
 436                         data.Copy (dest, source);
 437                         return data;
 438                 }
 439
 440                 public Domain LoadStack (APC pc, int offset, int dest, int source, bool isOld, Domain data)
 441                 {
 442                         if (isOld) {
 443                                 Domain oldState = FindOldState (pc, data);
 444                                 oldState.CopyOldValue (pc, dest, source, data, false);
 445                                 if (data.OldDomain != null)
 446                                         oldState.CopyOldValue (pc, dest, source, data.OldDomain, false);
 447                         } else {
 448                                 data.Copy (dest, source);
 449                                 if (data.OldDomain != null)
 450                                         data.OldDomain.Copy (dest, source);
 451                         }
 452
 453                         return data;
 454                 }
 455
 456                 public Domain LoadStackAddress (APC pc, int offset, int dest, int source, TypeNode type, bool isOld, Domain data)
 457                 {
 458                         if (isOld) {
 459                                 TypeNode ptrType = MetaDataProvider.ManagedPointer (type);
 460                                 Domain oldState = FindOldState (pc, data);
 461                                 SymValue srcOldAddr = oldState.Address (source);
 462                                 SymValue sv = data.CreateValue (type);
 463
 464                                 oldState.CopyOldValue (pc, sv, srcOldAddr, data, true);
 465                                 data.CopyAddress (data.Address (dest), sv, ptrType);
 466                                 if (data.OldDomain != null) {
 467                                         TypeNode ptrPtrType = MetaDataProvider.ManagedPointer (ptrType);
 468                                         oldState.CopyOldValueToDest (pc, data.OldDomain.Address (dest), srcOldAddr, ptrPtrType, data.OldDomain);
 469                                 }
 470                         } else {
 471                                 LoadStackAddressEffect (pc, offset, dest, source, data);
 472                                 if (data.OldDomain != null)
 473                                         LoadStackAddressEffect (pc, offset, dest, source, data.OldDomain);
 474                         }
 475                         return data;
 476                 }
 477
 478                 public Domain LoadResult (APC pc, TypeNode type, int dest, int source, Domain data)
 479                 {
 480                         return DoWithBothDomains (data, d => d.Copy (dest, source));
 481                 }
 482
 483                 public Domain Arglist (APC pc, int dest, Domain data)
 484                 {
 485                         throw new NotImplementedException ();
 486                 }
 487
 488                 public Domain Branch (APC pc, APC target, bool leavesExceptionBlock, Domain data)
 489                 {
 490                         throw new InvalidOperationException ("Should not see branches, should see assumes. See APCDecoder");
 491                 }
 492
 493                 public Domain BranchCond (APC pc, APC target, BranchOperator bop, int value1, int value2, Domain data)
 494                 {
 495                         throw new InvalidOperationException ("Should not see branches, should see assumes. See APCDecoder");
 496                 }
 497
 498                 public Domain BranchTrue (APC pc, APC target, int cond, Domain data)
 499                 {
 500                         throw new InvalidOperationException ("Should not see branches, should see assumes. See APCDecoder");
 501                 }
 502
 503                 public Domain BranchFalse (APC pc, APC target, int cond, Domain data)
 504                 {
 505                         throw new InvalidOperationException ("Should not see branches, should see assumes. See APCDecoder");
 506                 }
 507
 508                 public Domain Break (APC pc, Domain data)
 509                 {
 510                         return data;
 511                 }
 512
 513                 public Domain Call<TypeList, ArgList> (APC pc, Method method, bool virt, TypeList extraVarargs, int dest, ArgList args, Domain data)
 514                         where TypeList : IIndexable<TypeNode>
 515                         where ArgList : IIndexable<int>
 516                 {
 517                         TypeNode declaringType = MetaDataProvider.DeclaringType (method);
 518                         if (data.OldDomain == null)
 519                                 return CallEffect (pc, method, virt, extraVarargs, dest, args, data, declaringType, false);
 520                         data.OldDomain = CallEffect (pc, method, virt, extraVarargs, dest, args, data.OldDomain, declaringType, false);
 521                         if (!MetaDataProvider.IsVoidMethod (method))
 522                                 data.OldDomain.CopyOldValue (data.OldDomain.BeginOldPC, dest, dest, data, true);
 523                         return data;
 524                 }
 525
 526                 public Domain Calli<TypeList, ArgList> (APC pc, TypeNode returnType, TypeList argTypes, bool instance, int dest, int functionPointer, ArgList args, Domain data)
 527                         where TypeList : IIndexable<TypeNode>
 528                         where ArgList : IIndexable<int>
 529                 {
 530                         if (data.OldDomain == null)
 531                                 return CalliEffect (pc, returnType, argTypes, instance, dest, functionPointer, args, data);
 532                         data.OldDomain = CalliEffect (pc, returnType, argTypes, instance, dest, functionPointer, args, data.OldDomain);
 533                         if (!MetaDataProvider.IsVoid (returnType))
 534                                 data.OldDomain.CopyOldValue (data.OldDomain.BeginOldPC, dest, dest, data, true);
 535                         return data;
 536                 }
 537
 538                 public Domain CheckFinite (APC pc, int dest, int source, Domain data)
 539                 {
 540                         data.Copy (dest, source);
 541                         if (data.OldDomain != null)
 542                                 data.OldDomain.Copy (dest, source);
 543
 544                         return data;
 545                 }
 546
 547                 public Domain CopyBlock (APC pc, int destAddress, int srcAddress, int len, Domain data)
 548                 {
 549                         data.Havoc (destAddress);
 550                         data.Havoc (srcAddress);
 551                         data.Havoc (len);
 552
 553                         return data;
 554                 }
 555
 556                 public Domain EndFilter (APC pc, int decision, Domain data)
 557                 {
 558                         data.Havoc (decision);
 559
 560                         return data;
 561                 }
 562
 563                 public Domain EndFinally (APC pc, Domain data)
 564                 {
 565                         return data;
 566                 }
 567
 568                 public Domain Jmp (APC pc, Method method, Domain data)
 569                 {
 570                         return data;
 571                 }
 572
 573                 public Domain LoadArg (APC pc, Parameter argument, bool isOld, int dest, Domain data)
 574                 {
 575                         LoadArgEffect (argument, isOld, dest, data);
 576                         if (data.OldDomain != null)
 577                                 LoadArgEffect (argument, isOld, dest, data.OldDomain);
 578
 579                         return data;
 580                 }
 581
 582                 public Domain LoadArgAddress (APC pc, Parameter argument, bool isOld, int dest, Domain data)
 583                 {
 584                         LoadArgAddressEffect (argument, isOld, dest, data);
 585                         if (data.OldDomain != null)
 586                                 LoadArgAddressEffect (argument, isOld, dest, data.OldDomain);
 587                         return data;
 588                 }
 589
 590                 public Domain LoadLocal (APC pc, Local local, int dest, Domain data)
 591                 {
 592                         LoadLocalEffect (local, dest, data);
 593                         if (data.OldDomain != null)
 594                                 data.CopyValueToOldState (data.OldDomain.BeginOldPC, MetaDataProvider.LocalType (local), dest, dest, data.OldDomain);
 595
 596                         return data;
 597                 }
 598
 599                 public Domain LoadLocalAddress (APC pc, Local local, int dest, Domain data)
 600                 {
 601                         LoadLocalAddressEffect (local, dest, data);
 602                         if (data.OldDomain != null)
 603                                 LoadLocalAddressEffect (local, dest, data.OldDomain);
 604
 605                         return data;
 606                 }
 607
 608                 public Domain Nop (APC pc, Domain data)
 609                 {
 610                         return data;
 611                 }
 612
 613                 public Domain Pop (APC pc, int source, Domain data)
 614                 {
 615                         data.Havoc (source);
 616                         if (data.OldDomain != null)
 617                                 data.OldDomain.Havoc (source);
 618
 619                         return data;
 620                 }
 621
 622                 public Domain Return (APC pc, int source, Domain data)
 623                 {
 624                         data.Havoc (source);
 625
 626                         return data;
 627                 }
 628
 629                 public Domain StoreArg (APC pc, Parameter argument, int source, Domain data)
 630                 {
 631                         data.CopyValue (data.Address (argument), data.Address (source), MetaDataProvider.ManagedPointer (MetaDataProvider.ParameterType (argument)));
 632                         data.Havoc (source);
 633
 634                         return data;
 635                 }
 636
 637                 public Domain StoreLocal (APC pc, Local local, int source, Domain data)
 638                 {
 639                         AnalysisDecoder it = this;
 640                         return DoWithBothDomains (data, d => it.StoreLocalEffect (local, source, d));
 641                 }
 642
 643                 public Domain Switch (APC pc, TypeNode type, IEnumerable<Pair<object, APC>> cases, int value, Domain data)
 644                 {
 645                         throw new InvalidOperationException ("Should only see assumes");
 646                 }
 647
 648                 public Domain Box (APC pc, TypeNode type, int dest, int source, Domain data)
 649                 {
 650                         AnalysisDecoder it = this;
 651                         return DoWithBothDomains (data, (d) => it.BoxEffect (type, dest, source, d));
 652                 }
 653
 654                 public Domain ConstrainedCallvirt<TypeList, ArgList> (APC pc, Method method, TypeNode constraint, TypeList extraVarargs, int dest, ArgList args, Domain data)
 655                         where TypeList : IIndexable<TypeNode>
 656                         where ArgList : IIndexable<int>
 657                 {
 658                         if (data.OldDomain == null)
 659                                 return CallEffect (pc, method, true, extraVarargs, dest, args, data, constraint, true);
 660
 661                         data.OldDomain = CallEffect (pc, method, true, extraVarargs, dest, args, data.OldDomain, constraint, true);
 662                         if (!MetaDataProvider.IsVoidMethod (method))
 663                                 data.OldDomain.CopyOldValue (data.OldDomain.BeginOldPC, dest, dest, data, true);
 664                         return data;
 665                 }
 666
 667                 public Domain CastClass (APC pc, TypeNode type, int dest, int obj, Domain data)
 668                 {
 669                         AnalysisDecoder it = this;
 670                         return DoWithBothDomains (data, d => it.CastClassEffect (type, dest, obj, d));
 671                 }
 672
 673                 public Domain CopyObj (APC pc, TypeNode type, int destPtr, int sourcePtr, Domain data)
 674                 {
 675                         data.CopyValue (data.Value (destPtr), data.Value (sourcePtr), MetaDataProvider.ManagedPointer (type));
 676                         data.Havoc (destPtr);
 677                         data.Havoc (sourcePtr);
 678                         return data;
 679                 }
 680
 681                 public Domain Initobj (APC pc, TypeNode type, int ptr, Domain data)
 682                 {
 683                         SymValue obj = data.Value (ptr);
 684                         data.Havoc (obj);
 685                         foreach (Field field in MetaDataProvider.Fields (type)) {
 686                                 SymValue dest = data.FieldAddress (obj, field);
 687                                 data.AssignZeroEquivalent (dest, MetaDataProvider.FieldType (field));
 688                         }
 689                         data.Havoc (ptr);
 690                         return data;
 691                 }
 692
 693                 public Domain LoadElement (APC pc, TypeNode type, int dest, int array, int index, Domain data)
 694                 {
 695                         if (data.OldDomain != null) {
 696                                 LoadElementEffect (type, dest, array, index, data.OldDomain);
 697                                 data.OldDomain.CopyOldValue (data.OldDomain.BeginOldPC, dest, dest, data, true);
 698                         } else
 699                                 LoadElementEffect (type, dest, array, index, data);
 700
 701                         return data;
 702                 }
 703
 704                 public Domain LoadField (APC pc, Field field, int dest, int obj, Domain data)
 705                 {
 706                         if (data.OldDomain != null) {
 707                                 LoadFieldEffect (field, dest, obj, data.OldDomain);
 708                                 data.OldDomain.CopyOldValue (data.OldDomain.BeginOldPC, dest, dest, data, true);
 709                         } else
 710                                 LoadFieldEffect (field, dest, obj, data);
 711
 712                         return data;
 713                 }
 714
 715                 public Domain LoadFieldAddress (APC pc, Field field, int dest, int obj, Domain data)
 716                 {
 717                         AnalysisDecoder it = this;
 718                         return DoWithBothDomains (data, domain => it.LoadFieldAddressEffect (pc, field, dest, obj, domain));
 719                 }
 720
 721                 public Domain LoadLength (APC pc, int dest, int array, Domain data)
 722                 {
 723                         AnalysisDecoder it = this;
 724                         return DoWithBothDomains (data, domain => it.LoadLengthEffect (dest, array, domain));
 725                 }
 726
 727                 public Domain LoadStaticField (APC pc, Field field, int dest, Domain data)
 728                 {
 729                         if (data.OldDomain != null) {
 730                                 LoadStaticFieldEffect (field, dest, data.OldDomain);
 731                                 data.OldDomain.CopyOldValue (data.OldDomain.BeginOldPC, dest, dest, data, true);
 732                         } else
 733                                 LoadStaticFieldEffect (field, dest, data);
 734                         return data;
 735                 }
 736
 737                 public Domain LoadStaticFieldAddress (APC pc, Field field, int dest, Domain data)
 738                 {
 739                         AnalysisDecoder it = this;
 740                         return DoWithBothDomains (data, domain => it.LoadStaticFieldAddressEffect (field, dest, domain));
 741                 }
 742
 743                 public Domain LoadTypeToken (APC pc, TypeNode type, int dest, Domain data)
 744                 {
 745                         throw new NotImplementedException ();
 746                 }
 747
 748                 public Domain LoadFieldToken (APC pc, Field type, int dest, Domain data)
 749                 {
 750                         throw new NotImplementedException ();
 751                 }
 752
 753                 public Domain LoadMethodToken (APC pc, Method type, int dest, Domain data)
 754                 {
 755                         throw new NotImplementedException ();
 756                 }
 757
 758                 public Domain NewArray<ArgList> (APC pc, TypeNode type, int dest, ArgList lengths, Domain data) where ArgList : IIndexable<int>
 759                 {
 760                         AnalysisDecoder it = this;
 761                         return DoWithBothDomains (data, d => it.NewArrayEffect<ArgList> (type, dest, lengths, d));
 762                 }
 763
 764                 public Domain NewObj<ArgList> (APC pc, Method ctor, int dest, ArgList args, Domain data) where ArgList : IIndexable<int>
 765                 {
 766                         AnalysisDecoder it = this;
 767                         return DoWithBothDomains (data, d => it.NewObjEffect (pc, ctor, dest, args, d));
 768                 }
 769
 770                 public Domain MkRefAny (APC pc, TypeNode type, int dest, int obj, Domain data)
 771                 {
 772                         throw new NotImplementedException ();
 773                 }
 774
 775                 public Domain RefAnyType (APC pc, int dest, int source, Domain data)
 776                 {
 777                         throw new NotImplementedException ();
 778                 }
 779
 780                 public Domain RefAnyVal (APC pc, TypeNode type, int dest, int source, Domain data)
 781                 {
 782                         throw new NotImplementedException ();
 783                 }
 784
 785                 public Domain Rethrow (APC pc, Domain data)
 786                 {
 787                         return data.Bottom;
 788                 }
 789
 790                 public Domain StoreElement (APC pc, TypeNode type, int array, int index, int value, Domain data)
 791                 {
 792                         AnalysisDecoder it = this;
 793                         return DoWithBothDomains (data, d => it.StoreElementEffect (type, array, index, value, d));
 794                 }
 795
 796                 public Domain StoreField (APC pc, Field field, int obj, int value, Domain data)
 797                 {
 798                         data.CopyValue (data.FieldAddress (data.Value (obj), field), data.Address (value));
 799                         if (!MetaDataProvider.IsCompilerGenerated (field))
 800                                 data.HavocPseudoFields (data.Value (obj));
 801                         data.Havoc (obj);
 802                         data.Havoc (value);
 803                         return data;
 804                 }
 805
 806                 public Domain StoreStaticField (APC pc, Field field, int value, Domain data)
 807                 {
 808                         data.CopyValue (data.FieldAddress (data.Globals, field), data.Address (value));
 809                         data.Havoc (value);
 810                         return data;
 811                 }
 812
 813                 public Domain Throw (APC pc, int exception, Domain data)
 814                 {
 815                         data.Havoc (exception);
 816                         return data;
 817                 }
 818
 819                 public Domain Unbox (APC pc, TypeNode type, int dest, int obj, Domain data)
 820                 {
 821                         AnalysisDecoder it = this;
 822                         return DoWithBothDomains (data, d => d.AssignValue (dest, it.MetaDataProvider.ManagedPointer (type)));
 823                 }
 824
 825                 public Domain UnboxAny (APC pc, TypeNode type, int dest, int obj, Domain data)
 826                 {
 827                         return DoWithBothDomains (data, d => d.AssignValue (dest, type));
 828                 }
 829                 #endregion
 830
 831                 private void MaterializeParameter (Parameter parameter, TypeNode declaringType, Domain data, bool aggressiveMaterialization)
 832                 {
 833                         TypeNode type = MetaDataProvider.ParameterType (parameter);
 834                         data.Assign (parameter, type);
 835                         MaterializeParameterInfo (data.Address (parameter), MetaDataProvider.ManagedPointer (type), 0, data, declaringType, aggressiveMaterialization);
 836                         data.CopyParameterIntoShadow (parameter);
 837                 }
 838
 839                 private void MaterializeParameterInfo (SymValue sv, TypeNode t, int depth, Domain data, TypeNode fromType, bool aggressiveMaterialization)
 840                 {
 841                         data.MakeUnmodified (sv);
 842                         data.SetType (sv, t);
 843                         if (depth > 2 && !aggressiveMaterialization || depth > 5)
 844                                 return;
 845                         if (MetaDataProvider.IsManagedPointer (t)) {
 846                                 TypeNode elemType = MetaDataProvider.ElementType (t);
 847                                 if (!MetaDataProvider.HasValueRepresentation (elemType)) {
 848                                         data.ManifestStructId (sv);
 849                                         foreach (Field field in MetaDataProvider.Fields (elemType)) {
 850                                                 if (!MetaDataProvider.IsStatic (field) && MetaDataProvider.IsVisibleFrom (field, fromType)) {
 851                                                         TypeNode fieldAddressType;
 852                                                         MaterializeParameterInfo (data.FieldAddress (sv, field, out fieldAddressType), fieldAddressType, depth + 1, data, fromType, aggressiveMaterialization);
 853                                                 }
 854                                         }
 855                                         ManifestProperties (sv, depth + 1, data, fromType, aggressiveMaterialization, elemType);
 856                                 } else
 857                                         MaterializeParameterInfo (data.Value (sv), elemType, depth + 1, data, fromType, aggressiveMaterialization);
 858                         } else {
 859                                 if (MetaDataProvider.IsClass (t)) {
 860                                         foreach (Field field in MetaDataProvider.Fields (t)) {
 861                                                 if (!MetaDataProvider.IsStatic (field) && MetaDataProvider.IsVisibleFrom (field, fromType)) {
 862                                                         TypeNode fieldAddressType;
 863                                                         MaterializeParameterInfo (data.FieldAddress (sv, field, out fieldAddressType), fieldAddressType, depth + 1, data, fromType, aggressiveMaterialization);
 864                                                 }
 865                                         }
 866                                 } else if (data.NeedsArrayLengthManifested (t))
 867                                         data.ManifestArrayLength (sv);
 868                         }
 869                 }
 870
 871                 private void ManifestProperties (SymValue sv, int depth, Domain data, TypeNode fromType, bool aggressiveMaterialization, TypeNode type)
 872                 {
 873                         foreach (Property property in MetaDataProvider.Properties (type)) {
 874                                 Method getter;
 875                                 if (MetaDataProvider.IsStatic (property) || !MetaDataProvider.HasGetter (property, out getter) || !MetaDataProvider.IsVisibleFrom (getter, fromType))
 876                                         continue;
 877
 878                                 TypeNode pseudoFieldAddressType;
 879                                 MaterializeParameterInfo (data.PseudoFieldAddress (sv, getter, out pseudoFieldAddressType, false), pseudoFieldAddressType, depth + 1, data, fromType, aggressiveMaterialization);
 880                         }
 881
 882                         if (!MetaDataProvider.IsInterface (type))
 883                                 return;
 884
 885                         foreach (TypeNode iface in MetaDataProvider.Interfaces (type)) {
 886                                 if (MetaDataProvider.IsVisibleFrom (iface, fromType))
 887                                         ManifestProperties (sv, depth, data, fromType, aggressiveMaterialization, iface);
 888                         }
 889                 }
 890
 891                 private void MaterializeLocal (Local local, Method method, Domain data)
 892                 {
 893                         TypeNode t = MetaDataProvider.LocalType (local);
 894                         data.AssignZeroEquivalent (data.Address (local), t);
 895                 }
 896
 897                 private void HavocParameters (APC pc, Method method, IIndexable<TypeNode> extraVarargs, IIndexable<int> args, Domain data, TypeNode declaringType, bool insideConstructor, bool thisArgMissing,
 898                                               bool derefThis)
 899                 {
 900                         IIndexable<Parameter> parameters = MetaDataProvider.Parameters (method);
 901                         IIndexable<Parameter> unspecializedParameters = null;
 902                         if (MetaDataProvider.IsSpecialized (method))
 903                                 unspecializedParameters = MetaDataProvider.Parameters (MetaDataProvider.Unspecialized (method));
 904                         int index2 = 0;
 905                         int num1 = 0;
 906                         for (int index1 = 0; index1 < args.Count; ++index1) {
 907                                 bool materialize = false;
 908                                 bool nonFirstThis = false;
 909                                 int num2 = args [index1];
 910                                 bool parameterHasGenericType = false;
 911                                 bool havocReadonlyFields = false;
 912                                 TypeNode ype;
 913
 914                                 if (index1 == 0 && !thisArgMissing && !MetaDataProvider.IsStatic (method)) {
 915                                         num1 = 1;
 916                                         ype = MetaDataProvider.ParameterType (MetaDataProvider.This (method));
 917                                         if (MetaDataProvider.IsPrimitive (declaringType) || MetaDataProvider.Equal (declaringType, MetaDataProvider.System_Object)) {
 918                                                 if (MetaDataProvider.IsStruct (declaringType))
 919                                                         data.Value (data.Value (args [0]));
 920                                                 continue;
 921                                         }
 922                                         if (MetaDataProvider.IsConstructor (method)) {
 923                                                 if (insideConstructor && data.IsThis (this.parent.CurrentMethod, num2)) {
 924                                                         if (TypesEqualModuloInstantiation (declaringType, MetaDataProvider.DeclaringType (this.parent.CurrentMethod)))
 925                                                                 havocReadonlyFields = true;
 926                                                         else
 927                                                                 continue;
 928                                                 }
 929                                                 if (MetaDataProvider.IsStruct (declaringType))
 930                                                         materialize = true;
 931                                         }
 932                                 } else if (index2 < parameters.Count) {
 933                                         if (data.IsThis (this.parent.CurrentMethod, num2))
 934                                                 nonFirstThis = true;
 935                                         Parameter p = parameters [index2];
 936                                         materialize = MetaDataProvider.IsOut (p);
 937                                         ype = MetaDataProvider.ParameterType (p);
 938                                         if (unspecializedParameters != null) {
 939                                                 TypeNode unspecType = MetaDataProvider.ParameterType (unspecializedParameters [index2]);
 940                                                 parameterHasGenericType = MetaDataProvider.IsFormalTypeParameter (unspecType) || MetaDataProvider.IsMethodFormalTypeParameter (unspecType);
 941                                         }
 942                                         ++index2;
 943                                 } else if (!data.IsThis (this.parent.CurrentMethod, num2))
 944                                         ype = extraVarargs [index1 - index2 - num1];
 945                                 else
 946                                         continue;
 947                                 if (!pc.InsideContract) {
 948                                         bool havocFields = AggressiveUpHavocMethod (method);
 949                                         if (havocFields || materialize || MustHavocParameter (method, declaringType, ype, parameterHasGenericType, nonFirstThis)) {
 950                                                 SymValue loc = data.Value (num2);
 951                                                 if (derefThis && index1 == 0 && num1 == 1)
 952                                                         loc = data.Value (loc);
 953                                                 data.HavocObjectAtCall (loc, ref data.ModifiedAtCall, havocFields, havocReadonlyFields);
 954                                                 if (materialize)
 955                                                         data.MaterializeAccordingToType (loc, ype, 0);
 956                                         }
 957                                 }
 958                                 data.Havoc (num2);
 959                         }
 960                 }
 961
 962                 private bool MustHavocParameter (Method method, TypeNode declaringType, TypeNode pt, bool parameterHasGenericType, bool nonFirstThis)
 963                 {
 964                         if (parameterHasGenericType || MetaDataProvider.IsStruct (pt) || MetaDataProvider.Equal (declaringType, MetaDataProvider.System_Object) ||
 965                             IsImmutable (pt) || nonFirstThis || MetaDataProvider.Equal (pt, MetaDataProvider.System_Object))
 966                                 return false;
 967
 968                         return true;
 969                 }
 970
 971                 private bool IsImmutable (TypeNode pt)
 972                 {
 973                         return MetaDataProvider.Equal (pt, MetaDataProvider.System_String);
 974                 }
 975
 976                 private bool AggressiveUpHavocMethod (Method method)
 977                 {
 978                         if (MetaDataProvider.Name (MetaDataProvider.DeclaringType (method)) != "Monitor")
 979                                 return false;
 980                         string name = MetaDataProvider.Name (method);
 981
 982                         return (name == "Exit" || name == "Wait");
 983                 }
 984
 985                 private bool TypesEqualModuloInstantiation (TypeNode a, TypeNode b)
 986                 {
 987                         a = MetaDataProvider.Unspecialized (a);
 988                         b = MetaDataProvider.Unspecialized (b);
 989                         return MetaDataProvider.Equal (a, b);
 990                 }
 991
 992                 private SymValue KeyForPureFunctionArgument (Method method, int index, int arg, Domain data, IImmutableMap<TypeNode, TypeNode> specialization, out bool isOut)
 993                 {
 994                         bool isByRef;
 995                         TypeNode type;
 996                         bool isPrimitive;
 997                         if (!ParameterHasValueRepresentation (method, index, specialization, out isPrimitive, out isOut, out isByRef, out type))
 998                                 return data.StructId (isByRef ? data.Value (arg) : data.Address (arg));
 999                         SymValue sv = data.Value (arg);
1000                         if (isByRef)
1001                                 sv = data.Value (sv);
1002                         return isPrimitive || IsImmutableType (type) ? sv : data.ObjectVersion (sv);
1003                 }
1004
1005                 private bool ParameterHasValueRepresentation (Method method, int index, IImmutableMap<TypeNode, TypeNode> specialization, out bool isPrimitive, out bool isOut, out bool isByRef, out TypeNode type)
1006                 {
1007                         if (index == 0 && !MetaDataProvider.IsStatic (method)) {
1008                                 isOut = false;
1009                                 type = MetaDataProvider.DeclaringType (method);
1010                                 isPrimitive = MetaDataProvider.IsPrimitive (type);
1011                                 bool hasValueRepresentation = MetaDataProvider.HasValueRepresentation (type);
1012                                 isByRef = (isPrimitive || !hasValueRepresentation);
1013                                 return hasValueRepresentation;
1014                         }
1015
1016                         int paramIndex = MetaDataProvider.IsStatic (method) ? index : (index - 1);
1017                         Parameter p = MetaDataProvider.Parameters (method) [paramIndex];
1018                         type = MetaDataProvider.ParameterType (p);
1019                         type = Specialize (specialization, type);
1020                         isOut = MetaDataProvider.IsOut (p);
1021                         if (isByRef = MetaDataProvider.IsManagedPointer (type))
1022                                 type = MetaDataProvider.ElementType (type);
1023
1024                         isPrimitive = MetaDataProvider.IsPrimitive (type);
1025                         return MetaDataProvider.HasValueRepresentation (type);
1026                 }
1027
1028                 private bool IsImmutableType (TypeNode type)
1029                 {
1030                         //todo: implement
1031                         return false;
1032                 }
1033
1034                 private int GetNonOutArgs (Method method)
1035                 {
1036                         int res = MetaDataProvider.IsStatic (method) ? 1 : 0;
1037                         IIndexable<Parameter> parameters = MetaDataProvider.Parameters (method);
1038                         for (int i = 0; i < parameters.Count; ++i) {
1039                                 if (!MetaDataProvider.IsOut (parameters [i]))
1040                                         ++res;
1041                         }
1042
1043                         return res;
1044                 }
1045
1046                 private void AssignAllOutParameters<ArgList> (Domain data, SymValue fieldAddr, Method method, ArgList args)
1047                         where ArgList : IIndexable<int>
1048                 {
1049                         int index = 0;
1050
1051                         if (!MetaDataProvider.IsStatic (method))
1052                                 ++index;
1053                         IIndexable<Parameter> parameters = MetaDataProvider.Parameters (method);
1054                         for (; index < parameters.Count; index++) {
1055                                 Parameter p = parameters [index];
1056                                 if (MetaDataProvider.IsOut (p)) {
1057                                         TypeNode pType = MetaDataProvider.ParameterType (p);
1058                                         SymValue srcAddr = data.PseudoFieldAddressOfOutParameter (index, fieldAddr, pType);
1059                                         SymValue destAddr = data.Value (args [index]);
1060                                         data.CopyValue (destAddr, srcAddr, pType);
1061                                 }
1062                         }
1063                 }
1064
1065                 private TypeNode Specialize (IImmutableMap<TypeNode, TypeNode> instantiationMap, TypeNode declaringType)
1066                 {
1067                         throw new NotImplementedException ();
1068                 }
1069
1070                 private void DevirtualizeImplementingMethod (TypeNode declaringType, ref Method method)
1071                 {
1072                         throw new NotImplementedException ();
1073                 }
1074
1075                 private IImmutableMap<TypeNode, TypeNode> ComputeTypeInstantiationMap (APC pc, Method method)
1076                 {
1077                         IImmutableMap<TypeNode, TypeNode> specialization = ImmutableMap<TypeNode, TypeNode>.Empty;
1078                         foreach (var edge in pc.SubroutineContext.AsEnumerable ()) {
1079                                 Method calledMethod;
1080                                 bool isVirtual;
1081                                 bool isNewObj;
1082                                 if (edge.From.IsMethodCallBlock (out calledMethod, out isNewObj, out isVirtual))
1083                                         MetaDataProvider.IsSpecialized (calledMethod, ref specialization);
1084                                 else if (edge.To.IsMethodCallBlock (out calledMethod, out isNewObj, out isVirtual))
1085                                         MetaDataProvider.IsSpecialized (calledMethod, ref specialization);
1086                         }
1087                         return specialization;
1088                 }
1089
1090                 private Domain CalliEffect<TypeList, ArgList> (APC pc, TypeNode returnType, TypeList argTypes, bool isInstance, int dest, int functionPointer, ArgList args, Domain data)
1091                         where TypeList : IIndexable<TypeNode>
1092                         where ArgList : IIndexable<int>
1093                 {
1094                         for (int i = 0; i < args.Count; i++) {
1095                                 int num = args [i];
1096                                 TypeNode type;
1097                                 if (isInstance) {
1098                                         if (i > 0)
1099                                                 type = argTypes [i - 1];
1100                                         else {
1101                                                 SymValue sv = data.Value (num);
1102                                                 AbstractType aType = data.GetType (sv);
1103                                                 type = aType.IsNormal ? aType.ConcreteType : MetaDataProvider.System_Object;
1104                                         }
1105                                 } else
1106                                         type = argTypes [i];
1107                                 if (!MetaDataProvider.IsStruct (type)) {
1108                                         data.ResetModifiedAtCall ();
1109                                         data.HavocObjectAtCall (data.Value (num), ref data.ModifiedAtCall, false, false);
1110                                 }
1111                                 data.Havoc (num);
1112                         }
1113                         data.AssignValue (dest, returnType);
1114                         return data;
1115                 }
1116
1117                 private void LoadArgAddressEffect (Parameter p, bool isOld, int dest, Domain data)
1118                 {
1119                         SymValue srcAddr = isOld ? data.OldValueAddress (p) : data.Address (p);
1120                         data.CopyAddress (data.Address (dest), srcAddr, MetaDataProvider.ManagedPointer (MetaDataProvider.ParameterType (p)));
1121                 }
1122
1123                 private void LoadLocalAddressEffect (Local local, int dest, Domain data)
1124                 {
1125                         data.CopyAddress (data.Address (dest), data.Address (local), MetaDataProvider.ManagedPointer (MetaDataProvider.LocalType (local)));
1126                 }
1127
1128                 private void BoxEffect (TypeNode type, int dest, int source, Domain data)
1129                 {
1130                         if (MetaDataProvider.IsReferenceType (type))
1131                                 data.Copy (dest, source);
1132                         else {
1133                                 SymValue srcAddr = data.Address (source);
1134                                 TypeNode systemObject = MetaDataProvider.System_Object;
1135                                 SymValue specialUnary = data.GetSpecialUnary (data.Functions.BoxOperator, source, systemObject);
1136                                 data.SetValue (specialUnary, srcAddr, MetaDataProvider.ManagedPointer (type), false);
1137                                 data.AssignSpecialUnary (dest, specialUnary, systemObject);
1138                         }
1139                 }
1140
1141                 private void CastClassEffect (TypeNode type, int dest, int obj, Domain data)
1142                 {
1143                         SymValue destAddr = data.Address (dest);
1144                         TypeNode mp = MetaDataProvider.ManagedPointer (type);
1145                         data.CopyValueAndCast (destAddr, data.Address (obj), mp);
1146                 }
1147
1148                 private void LoadElementEffect (TypeNode type, int dest, int array, int index, Domain data)
1149                 {
1150                         TypeNode t = type;
1151                         if (!MetaDataProvider.IsStruct (type)) {
1152                                 SymValue sv = data.Value (array);
1153                                 AbstractType aType = data.GetType (sv);
1154                                 if (aType.IsNormal && MetaDataProvider.IsArray (aType.ConcreteType)) {
1155                                         t = MetaDataProvider.ElementType (aType.ConcreteType);
1156                                         if (t == null)
1157                                                 t = type;
1158                                 }
1159                         }
1160                         TypeNode elementAddressType = MetaDataProvider.ManagedPointer (t);
1161                         data.CopyValue (data.Address (dest), data.ElementAddress (data.Value (array), data.Value (index), elementAddressType), elementAddressType);
1162                         data.Havoc (index);
1163                 }
1164
1165                 private void LoadFieldEffect (Field field, int dest, int obj, Domain data)
1166                 {
1167                         SymValue ptr;
1168                         if (MetaDataProvider.IsStruct (MetaDataProvider.DeclaringType (field))) {
1169                                 AbstractType abstractType = data.GetType (data.Address (obj));
1170                                 ptr = abstractType.IsNormal
1171                                       && MetaDataProvider.IsManagedPointer (abstractType.ConcreteType)
1172                                       && MetaDataProvider.IsStruct (MetaDataProvider.ElementType (abstractType.ConcreteType))
1173                                         ? data.Address (obj)
1174                                         : data.Value (obj);
1175                         } else
1176                                 ptr = data.Value (obj);
1177                         TypeNode fieldAddressType;
1178                         SymValue srcAddr = data.FieldAddress (ptr, field, out fieldAddressType);
1179                         data.CopyValue (data.Address (dest), srcAddr, fieldAddressType);
1180                 }
1181
1182                 private void LoadFieldAddressEffect (APC pc, Field field, int dest, int obj, Domain data)
1183                 {
1184                         SymValue sv = data.Value (obj);
1185                         TypeNode fieldAddressType;
1186                         SymValue srcAddr = data.FieldAddress (sv, field, out fieldAddressType);
1187                         data.CopyAddress (data.Address (dest), srcAddr, fieldAddressType);
1188                         if (!pc.InsideContract && MetaDataProvider.Equal (MetaDataProvider.DeclaringType (this.parent.CurrentMethod), MetaDataProvider.Unspecialized (MetaDataProvider.DeclaringType (field))))
1189                                 data.HavocPseudoFields (this.parent.StackContextProvider.MethodContext.AffectedGetters (field), sv);
1190                 }
1191
1192                 private void LoadLengthEffect (int dest, int array, Domain data)
1193                 {
1194                         data.AssignArrayLength (data.Address (dest), data.Value (array));
1195                 }
1196
1197                 private void LoadStaticFieldEffect (Field field, int dest, Domain data)
1198                 {
1199                         TypeNode fieldAddressType;
1200                         SymValue srcAddr = data.FieldAddress (data.Globals, field, out fieldAddressType);
1201                         data.CopyValue (data.Address (dest), srcAddr, fieldAddressType);
1202                 }
1203
1204                 private void LoadStaticFieldAddressEffect (Field field, int dest, Domain data)
1205                 {
1206                         TypeNode fieldAddressType;
1207                         SymValue srcAddr = data.FieldAddress (data.Globals, field, out fieldAddressType);
1208                         data.CopyAddress (data.Address (dest), srcAddr, fieldAddressType);
1209                 }
1210
1211                 private void NewArrayEffect<T> (TypeNode type, int dest, IIndexable<int> list, Domain data)
1212                 {
1213                         if (list.Count == 1) {
1214                                 SymValue array = data.CreateArray (type, data.Value (list [0]));
1215                                 data.CopyAddress (data.Address (dest), array, MetaDataProvider.ArrayType (type, 1));
1216                         } else
1217                                 data.AssignValue (dest, type);
1218                 }
1219
1220                 private void NewObjEffect<ArgList> (APC pc, Method ctor, int dest, ArgList args, Domain data)
1221                         where ArgList : IIndexable<int>
1222                 {
1223                         for (int i = 0; i < args.Count; ++i)
1224                                 data.Havoc (args [i]);
1225
1226                         TypeNode declaringType = MetaDataProvider.DeclaringType (ctor);
1227                         if (MetaDataProvider.IsStruct (declaringType)) {
1228                                 SymValue srcAddr = data.CreateValue (declaringType);
1229                                 data.MaterializeAccordingToType (srcAddr, MetaDataProvider.ManagedPointer (declaringType), 0);
1230                                 HavocParameters (pc, ctor, Indexable<TypeNode>.Empty, args, data, declaringType, false, true, false);
1231                                 data.CopyValue (data.Address (dest), srcAddr, MetaDataProvider.ManagedPointer (declaringType));
1232                                 return;
1233                         }
1234
1235                         SymValue sv = data.CreateObject (declaringType);
1236                         HavocParameters (pc, ctor, Indexable<TypeNode>.Empty, args, data, declaringType, false, true, false);
1237                         data.CopyAddress (data.Address (dest), sv, declaringType);
1238                 }
1239
1240                 private void StoreElementEffect (TypeNode type, int array, int index, int value, Domain data)
1241                 {
1242                         TypeNode elementAddressType = MetaDataProvider.ManagedPointer (type);
1243                         SymValue arrayValue = data.Value (array);
1244                         SymValue indexValue = data.Value (index);
1245                         data.HavocArrayAtIndex (arrayValue, indexValue);
1246                         data.CopyValue (data.ElementAddress (arrayValue, indexValue, elementAddressType), data.Address (value), elementAddressType);
1247                         data.Havoc (array);
1248                         data.Havoc (index);
1249                         data.Havoc (value);
1250                 }
1251
1252                 public static Domain FindOldState (APC pc, Domain data)
1253                 {
1254                         for (LispList<Edge<CFGBlock, EdgeTag>> list = pc.SubroutineContext; list != null; list = list.Tail) {
1255                                 Edge<CFGBlock, EdgeTag> pair = list.Head;
1256                                 if (pair.Tag == EdgeTag.Exit || pair.Tag.Is (EdgeTag.AfterMask))
1257                                         return data.GetStateAt (new APC (pair.From.Subroutine.EntryAfterRequires, 0, list.Tail));
1258                         }
1259                         return null;
1260                 }
1261         }
1262 }