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

   1 //
   2 // Domain.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;
  29 using System.Collections.Generic;
  30 using System.IO;
  31 using System.Linq;
  32 using Mono.CodeContracts.Static.AST;
  33 using Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths;
  34 using Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph;
  35 using Mono.CodeContracts.Static.ControlFlow;
  36 using Mono.CodeContracts.Static.DataStructures;
  37 using Mono.CodeContracts.Static.Lattices;
  38 using Mono.CodeContracts.Static.Providers;
  39
  40 namespace Mono.CodeContracts.Static.Analysis.HeapAnalysis {
  41         class Domain : IAbstractDomain<Domain> {
  42                 private static Domain BottomValue;
  43                 public readonly FunctionsTable Functions;
  44                 private readonly Dictionary<APC, Domain> begin_old_saved_states;
  45                 private readonly SymGraph<SymFunction, AbstractType> egraph;
  46                 private readonly HeapAnalysis parent;
  47                 private TypeCache IEnumerable1Type = new TypeCache (@"System.Collections.IEnumerable`1");
  48                 private TypeCache IEnumerableType = new TypeCache (@"System.Collections.IEnumerable");
  49                 public int InsideOld;
  50                 public IImmutableSet<SymValue> ModifiedAtCall;
  51                 private IImmutableMap<SymValue, SymFunction> constantLookup;
  52                 private IImmutableSet<SymValue> unmodifiedFieldsSinceEntry;
  53                 private IImmutableSet<SymValue> unmodifiedSinceEntry;
  54
  55                 private Domain (SymGraph<SymFunction, AbstractType> newEgraph,
  56                                 IImmutableMap<SymValue, SymFunction> constantMap,
  57                                 IImmutableSet<SymValue> unmodifiedSinceEntry, IImmutableSet<SymValue> unmodifiedFieldsSinceEntry, IImmutableSet<SymValue> modifiedAtCall,
  58                                 Domain from, Domain oldDomain)
  59                 {
  60                         this.egraph = newEgraph;
  61                         this.Functions = from.Functions;
  62                         this.parent = from.parent;
  63                         this.begin_old_saved_states = from.begin_old_saved_states;
  64                         this.constantLookup = constantMap;
  65                         this.unmodifiedSinceEntry = unmodifiedSinceEntry;
  66                         this.unmodifiedFieldsSinceEntry = unmodifiedFieldsSinceEntry;
  67                         this.ModifiedAtCall = modifiedAtCall;
  68                         this.InsideOld = from.InsideOld;
  69                         OldDomain = oldDomain;
  70                         BeginOldPC = from.BeginOldPC;
  71                 }
  72
  73                 public Domain (HeapAnalysis parent)
  74                 {
  75                         this.parent = parent;
  76                         this.egraph = new SymGraph<SymFunction, AbstractType> (AbstractType.TopValue, AbstractType.BottomValue);
  77                         this.constantLookup = ImmutableIntKeyMap<SymValue, SymFunction>.Empty (SymValue.GetUniqueKey);
  78                         this.unmodifiedSinceEntry = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
  79                         this.unmodifiedFieldsSinceEntry = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
  80                         this.ModifiedAtCall = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
  81                         this.Functions = new FunctionsTable (parent.MetaDataProvider);
  82                         this.begin_old_saved_states = new Dictionary<APC, Domain> ();
  83
  84                         SymValue nullValue = this.egraph.FreshSymbol ();
  85                         this.egraph [this.Functions.NullValue] = nullValue;
  86                         this.egraph [nullValue] = AbstractType.BottomValue;
  87                         this.egraph [ConstantValue (0, MetaDataProvider.System_Int32)] = new AbstractType (MetaDataProvider.System_Int32, true);
  88                 }
  89
  90                 public Domain OldDomain { get; set; }
  91                 public APC BeginOldPC { get; set; }
  92
  93                 public SymValue Globals
  94                 {
  95                         get { return this.egraph.ConstRoot; }
  96                 }
  97
  98                 private SymValue Null
  99                 {
 100                         get { return this.egraph [this.Functions.NullValue]; }
 101                 }
 102
 103                 private SymValue Zero
 104                 {
 105                         get { return this.egraph [this.Functions.ZeroValue]; }
 106                 }
 107
 108                 public SymValue VoidAddr
 109                 {
 110                         get { return this.egraph [this.Functions.VoidAddr]; }
 111                 }
 112
 113                 private IMetaDataProvider MetaDataProvider
 114                 {
 115                         get { return this.parent.MetaDataProvider; }
 116                 }
 117
 118                 public IEnumerable<SymValue> Variables
 119                 {
 120                         get { return this.egraph.Variables; }
 121                 }
 122
 123                 #region IAbstractDomain<Domain> Members
 124                 public void Dump (TextWriter tw)
 125                 {
 126                         this.egraph.Dump (tw);
 127                         tw.WriteLine ("Unmodified locations:");
 128                         foreach (SymValue sv in this.unmodifiedSinceEntry.Elements)
 129                                 tw.Write ("{0} ", sv);
 130                         tw.WriteLine ();
 131
 132                         tw.WriteLine ("Unmodified locations for fields:");
 133                         foreach (SymValue sv in this.unmodifiedFieldsSinceEntry.Elements)
 134                                 tw.Write ("{0} ", sv);
 135                         tw.WriteLine ();
 136
 137                         if (this.ModifiedAtCall != null) {
 138                                 tw.WriteLine ("Modified locations at last call");
 139                                 foreach (SymValue sv in this.ModifiedAtCall.Elements)
 140                                         tw.Write ("{0} ", sv);
 141                                 tw.WriteLine ();
 142                         }
 143                         if (OldDomain == null)
 144                                 return;
 145
 146                         tw.WriteLine ("## has old domain ##");
 147                         OldDomain.egraph.Dump (tw);
 148                         tw.WriteLine ("## end old domain ##");
 149                 }
 150
 151                 public Domain Clone ()
 152                 {
 153                         return new Domain (this.egraph.Clone (), this.constantLookup, this.unmodifiedSinceEntry, this.unmodifiedFieldsSinceEntry, this.ModifiedAtCall, this, OldDomain == null ? null : OldDomain.Clone ());
 154                 }
 155                 #endregion
 156
 157                 public static bool IsRootedInParameter (Sequence<PathElement> path)
 158                 {
 159                         return path.Head is PathElement<Parameter>;
 160                 }
 161
 162                 public SymValue Address (Local local)
 163                 {
 164                         SymFunction function = this.Functions.For (local);
 165                         SymValue sv = this.egraph.TryLookup (function);
 166                         if (sv == null) {
 167                                 sv = this.egraph [function];
 168                                 SetType (sv, MetaDataProvider.ManagedPointer (MetaDataProvider.LocalType (local)));
 169                         }
 170                         return sv;
 171                 }
 172
 173                 public SymValue Address (Parameter v)
 174                 {
 175                         SymFunction function = this.Functions.For (v);
 176                         SymValue sv = this.egraph.TryLookup (function);
 177                         if (sv == null) {
 178                                 sv = this.egraph [function];
 179                                 SetType (sv, MetaDataProvider.ManagedPointer (MetaDataProvider.ParameterType (v)));
 180                         }
 181                         return sv;
 182                 }
 183
 184                 public SymValue Address (SymFunction v)
 185                 {
 186                         return this.egraph [v];
 187                 }
 188
 189                 public SymValue Address (int v)
 190                 {
 191                         return Address (this.Functions.For (v));
 192                 }
 193
 194                 public void AssignConst (int dest, TypeNode type, object constant)
 195                 {
 196                         AssignConst (Address (this.Functions.For (dest)), type, constant);
 197                 }
 198
 199                 public void AssignConst (SymValue address, TypeNode type, object constant)
 200                 {
 201                         SymValue value = ConstantValue (constant, type);
 202                         SetType (address, MetaDataProvider.ManagedPointer (type));
 203                         this.egraph [this.Functions.ValueOf, address] = value;
 204
 205                         var str = constant as string;
 206                         if (str != null)
 207                                 this.egraph [this.Functions.Length, value] = ConstantValue (str.Length, MetaDataProvider.System_Int32);
 208                 }
 209
 210                 public void AssignValue (int dest, FlatDomain<TypeNode> type)
 211                 {
 212                         AssignValue (Address (this.Functions.For (dest)), type);
 213                 }
 214
 215                 private void AssignValue (SymValue address, FlatDomain<TypeNode> type)
 216                 {
 217                         Havoc (address);
 218                         SetType (address, type.IsNormal() ? MetaDataProvider.ManagedPointer (type.Value) : type);
 219                         if (IsStructWithFields (type))
 220                                 return;
 221
 222                         SymValue fresh = this.egraph.FreshSymbol ();
 223                         SetType (fresh, type);
 224                         this.egraph [this.Functions.ValueOf, address] = fresh;
 225
 226                         if (!type.IsNormal())
 227                                 return;
 228
 229                         if (NeedsArrayLengthManifested (type.Value))
 230                                 ManifestArrayLength (fresh);
 231                 }
 232
 233                 public void AssignNull (int addr)
 234                 {
 235                         AssignNull (Address (this.Functions.For (addr)));
 236                 }
 237
 238                 public void AssignNull (SymValue addr)
 239                 {
 240                         Havoc (addr);
 241                         this.egraph [this.Functions.ValueOf, addr] = Null;
 242                 }
 243
 244                 private void AssignZero (SymValue addr)
 245                 {
 246                         this.egraph [this.Functions.ValueOf, addr] = Zero;
 247                 }
 248
 249                 public void AssignZeroEquivalent (SymValue addr, TypeNode t)
 250                 {
 251                         if (MetaDataProvider.IsReferenceType (t))
 252                                 AssignNull (addr);
 253                         else if (MetaDataProvider.HasValueRepresentation (t))
 254                                 AssignZero (addr);
 255                 }
 256
 257                 public void AssignSpecialUnary (int dest, SymFunction op, int source, FlatDomain<TypeNode> typeOfValue)
 258                 {
 259                         SymValue specialUnary = GetSpecialUnary (op, source, typeOfValue);
 260                         AssignSpecialUnary (dest, specialUnary, typeOfValue);
 261                 }
 262
 263                 public void AssignSpecialUnary (int dest, SymValue result, FlatDomain<TypeNode> typeOfValue)
 264                 {
 265                         SymValue address = Address (dest);
 266                         AssignValue (address, typeOfValue);
 267                         this.egraph [this.Functions.ValueOf, address] = result;
 268                 }
 269
 270                 public void AssignPureBinary (int dest, BinaryOperator op, FlatDomain<TypeNode> typeOpt, int op1, int op2)
 271                 {
 272                         var args = new[] {Value (op1), Value (op2)};
 273                         SymFunction c = this.Functions.For (op);
 274                         TypeNode type = !typeOpt.IsNormal() ? MetaDataProvider.System_Int32 : typeOpt.Value;
 275
 276                         bool fresh;
 277
 278                         SymValue pointerValue = LookupAddressAndManifestType (args, c, type, out fresh);
 279                         SymValue destAddr = Address (dest);
 280
 281                         SetType (destAddr, MetaDataProvider.ManagedPointer (type));
 282                         this.egraph [this.Functions.ValueOf, destAddr] = pointerValue;
 283                 }
 284
 285                 public void AssignPureUnary (int dest, UnaryOperator op, FlatDomain<TypeNode> typeOpt, int operand)
 286                 {
 287                         SymFunction c = this.Functions.For (op);
 288                         TypeNode type = !typeOpt.IsNormal() ? MetaDataProvider.System_Int32 : typeOpt.Value;
 289
 290                         SymValue unaryOperand = this.egraph [c, Value (operand)];
 291                         SymValue sv = Address (dest);
 292
 293                         SetType (sv, MetaDataProvider.ManagedPointer (type));
 294                         this.egraph [this.Functions.ValueOf, sv] = unaryOperand;
 295                 }
 296
 297                 private SymValue ConstantValue (object constant, TypeNode type)
 298                 {
 299                         SymFunction symFunction = this.Functions.ForConstant (constant, type);
 300                         SymValue sv = this.egraph.TryLookup (symFunction);
 301                         if (sv == null) {
 302                                 sv = this.egraph [symFunction];
 303                                 SetType (sv, type);
 304                                 this.constantLookup = this.constantLookup.Add (sv, symFunction);
 305                         }
 306                         return sv;
 307                 }
 308
 309                 public void Havoc (int i)
 310                 {
 311                         Havoc (Address (i));
 312                 }
 313
 314                 public void Havoc (SymValue addr)
 315                 {
 316                         this.egraph.EliminateAll (addr);
 317                 }
 318
 319                 private void HavocIfStruct (SymValue address)
 320                 {
 321                         AbstractType aType = this.egraph [address];
 322                         if (aType.IsBottom || (aType.IsNormal() && MetaDataProvider.IsStruct (aType.ConcreteType)))
 323                                 Havoc (address);
 324                 }
 325
 326                 private void HavocMutableFields (SymFunction except, SymValue address, ref IImmutableSet<SymValue> havoced)
 327                 {
 328                         HavocFields (except, address, ref havoced, false);
 329                 }
 330
 331                 private void HavocFields (SymFunction except, SymValue address, ref IImmutableSet<SymValue> havoced, bool havocImmutable)
 332                 {
 333                         if (havoced.Contains (address))
 334                                 return;
 335
 336                         havoced = havoced.Add (address);
 337                         MakeTotallyModified (address);
 338                         foreach (SymFunction c in this.egraph.Functions (address))
 339                                 HavocConstructor (except, address, c, ref havoced, havocImmutable);
 340                 }
 341
 342                 private void HavocConstructor (SymFunction except, SymValue address, SymFunction c, ref IImmutableSet<SymValue> havoced, bool havocImmutable)
 343                 {
 344                         if (c == this.Functions.ValueOf)
 345                                 this.egraph [this.Functions.OldValueOf, address] = this.egraph [c, address];
 346                         if (c == this.Functions.ValueOf || c == this.Functions.ObjectVersion || c == this.Functions.StructId) {
 347                                 this.egraph.Eliminate (c, address);
 348                                 havoced = havoced.Add (address);
 349                         } else {
 350                                 var fieldWrapper = c as Wrapper<Field>;
 351                                 if (fieldWrapper != null && fieldWrapper != except) {
 352                                         if (havocImmutable || !MetaDataProvider.IsReadonly (fieldWrapper.Item))
 353                                                 HavocFields (except, this.egraph [c, address], ref havoced, havocImmutable);
 354
 355                                         return;
 356                                 }
 357
 358                                 var methodWrapper = c as Wrapper<Method>;
 359                                 if (methodWrapper != null && methodWrapper != except)
 360                                         HavocFields (except, this.egraph [c, address], ref havoced, havocImmutable);
 361                         }
 362                 }
 363
 364                 public void HavocPseudoFields (SymValue address)
 365                 {
 366                         IImmutableSet<SymValue> havoced = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
 367                         HavocPseudoFields (null, address, ref havoced);
 368                 }
 369
 370                 private void HavocPseudoFields (SymFunction except, SymValue address, ref IImmutableSet<SymValue> havoced)
 371                 {
 372                         if (havoced.Contains (address))
 373                                 return;
 374                         havoced = havoced.Add (address);
 375                         if (IsUnmodified (address)) {
 376                                 MakeModified (address);
 377                                 MakeUnmodifiedField (address);
 378                         }
 379                         this.egraph.Eliminate (this.Functions.ObjectVersion, address);
 380                         this.egraph.Eliminate (this.Functions.StructId, address);
 381                         foreach (SymFunction c in this.egraph.Functions (address)) {
 382                                 if (c != except && c is Wrapper<Method>)
 383                                         HavocMutableFields (except, this.egraph [c, address], ref havoced);
 384                         }
 385                 }
 386
 387                 private void HavocPseudoFields (SymFunction except, IEnumerable<Method> getters, SymValue address, ref IImmutableSet<SymValue> havoced)
 388                 {
 389                         if (havoced.Contains (address))
 390                                 return;
 391                         havoced = havoced.Add (address);
 392                         if (IsUnmodified (address)) {
 393                                 MakeModified (address);
 394                                 MakeUnmodifiedField (address);
 395                         }
 396                         this.egraph.Eliminate (this.Functions.ObjectVersion, address);
 397                         this.egraph.Eliminate (this.Functions.StructId, address);
 398                         foreach (Method m in getters)
 399                                 HavocMutableFields (except, this.egraph [this.Functions.For (m), address], ref havoced);
 400                 }
 401
 402                 public void HavocPseudoFields (IEnumerable<Method> getters, SymValue address)
 403                 {
 404                         IImmutableSet<SymValue> havoced = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
 405                         HavocPseudoFields (null, getters, address, ref havoced);
 406                 }
 407
 408                 private void MakeUnmodifiedField (SymValue address)
 409                 {
 410                         this.unmodifiedFieldsSinceEntry = this.unmodifiedFieldsSinceEntry.Add (address);
 411                 }
 412
 413                 private void MakeModified (SymValue address)
 414                 {
 415                         this.unmodifiedSinceEntry = this.unmodifiedSinceEntry.Remove (address);
 416                 }
 417
 418                 public void CopyValue (SymValue destAddr, SymValue sourceAddr)
 419                 {
 420                         AbstractType type = this.egraph [sourceAddr];
 421                         CopyValue (destAddr, sourceAddr, type.Type);
 422                 }
 423
 424                 public void CopyValue (SymValue destAddr, SymValue sourceAddr, FlatDomain<TypeNode> addrType)
 425                 {
 426                         CopyValue (destAddr, sourceAddr, addrType, true, false);
 427                 }
 428
 429                 private void CopyValue (SymValue destAddr, SymValue sourceAddr, FlatDomain<TypeNode> addrType, bool setTargetAddrType, bool cast)
 430                 {
 431                         MakeTotallyModified (destAddr);
 432                         if (destAddr != sourceAddr)
 433                                 HavocIfStruct (destAddr);
 434                         if (setTargetAddrType)
 435                                 SetType (destAddr, addrType);
 436
 437                         SetValue (destAddr, sourceAddr, addrType, cast);
 438                 }
 439
 440                 public void CopyOldValue (APC pc, int dest, int source, Domain target, bool atEndOld)
 441                 {
 442                         CopyOldValue (pc, target.Address (dest), Address (source), target, atEndOld);
 443                 }
 444
 445                 public void CopyOldValue (APC pc, SymValue destAddr, SymValue srcAddr, Domain target, bool atEndOld)
 446                 {
 447                         AbstractType abstractType = this.egraph [srcAddr];
 448                         CopyOldValue (pc, destAddr, srcAddr, abstractType.Type, target, atEndOld);
 449                 }
 450
 451                 private void CopyOldValue (APC pc, SymValue destAddr, SymValue srcAddr, FlatDomain<TypeNode> addrType, Domain target, bool atEndOld)
 452                 {
 453                         CopyOldValue (pc, destAddr, srcAddr, addrType, true, atEndOld, target);
 454                 }
 455
 456                 private void CopyOldValue (APC pc, SymValue destAddr, SymValue srcAddr, FlatDomain<TypeNode> addrType, bool setTargetAddrType, bool atEndOld, Domain target)
 457                 {
 458                         target.MakeTotallyModified (destAddr);
 459                         if (destAddr != srcAddr)
 460                                 target.HavocIfStruct (destAddr);
 461                         if (setTargetAddrType)
 462                                 target.SetType (destAddr, addrType);
 463
 464                         FlatDomain<TypeNode> targetType = TargetType (addrType);
 465
 466                         if (IsStructWithFields (targetType))
 467                                 CopyOldStructValue (pc, destAddr, srcAddr, targetType.Value, target, atEndOld);
 468                         else if (atEndOld && targetType.IsNormal() && MetaDataProvider.IsManagedPointer (targetType.Value)) {
 469                                 srcAddr = TryValue (srcAddr);
 470                                 if (srcAddr == null)
 471                                         return;
 472                                 destAddr = target.Value (destAddr);
 473                                 CopyOldValue (pc, destAddr, srcAddr, targetType, setTargetAddrType, atEndOld, target);
 474                         } else {
 475                                 SymValue source = this.egraph.TryLookup (this.Functions.ValueOf, srcAddr);
 476                                 if (source == null) {
 477                                         if (this.egraph.IsImmutable)
 478                                                 return;
 479                                         source = this.egraph [this.Functions.ValueOf, srcAddr];
 480                                 }
 481                                 CopyOldValueToDest (pc, destAddr, source, addrType, target);
 482                         }
 483                 }
 484
 485                 public void CopyOldValueToDest (APC pc, SymValue destAddr, SymValue source, FlatDomain<TypeNode> addrType, Domain target)
 486                 {
 487                         if (pc.InsideEnsuresAtCall) {
 488                                 TypeNode type;
 489                                 object constant;
 490
 491                                 if (IsConstant (source, out type, out constant)) {
 492                                         SymValue sv = target.ConstantValue (constant, type);
 493                                         target.CopyNonStructWithFieldValue (destAddr, sv, addrType);
 494                                         return;
 495                                 }
 496
 497                                 foreach (var sv in GetAccessPathsRaw (source, AccessPathFilter<Method>.NoFilter, false))
 498                                         throw new NotImplementedException ();
 499                         }
 500                 }
 501
 502                 private IEnumerable<Sequence<PathElementBase>> GetAccessPathsRaw (SymValue sv, AccessPathFilter<Method> filter, bool compress)
 503                 {
 504                         var visited = new HashSet<SymValue> ();
 505                         return GetAccessPathsRaw (sv, null, visited, filter, compress);
 506                 }
 507
 508                 private IEnumerable<Sequence<PathElementBase>> GetAccessPathsRaw (SymValue sv, Sequence<PathElementBase> path, HashSet<SymValue> visited, AccessPathFilter<Method> filter, bool compress)
 509                 {
 510                         if (sv == this.egraph.ConstRoot)
 511                                 yield return path;
 512                         else if (!visited.Contains (sv)) {
 513                                 visited.Add (sv);
 514                                 foreach (var term in this.egraph.EqTerms (sv)) {
 515                                         if (!(term.Function is Wrapper<object>) && !(term.Function is Wrapper<int>)) {
 516                                                 PathElementBase next = term.Function.ToPathElement (compress);
 517                                                 if (next != null && !filter.FilterOutPathElement (term.Function)) {
 518                                                         Sequence<PathElementBase> newPath;
 519
 520                                                         if (path == null || !compress || (!(next is PathElement<Method>)))
 521                                                                 newPath = path.Cons (next);
 522                                                         else
 523                                                                 newPath = path.Tail.Cons (next);
 524
 525                                                         foreach (var item in GetAccessPathsRaw (term.Args [0], newPath, visited, filter, compress))
 526                                                                 yield return item;
 527                                                 }
 528                                         }
 529                                 }
 530                         }
 531                 }
 532
 533                 private Sequence<PathElementBase> GetBestAccessPath (SymValue sv, AccessPathFilter<Method> filter, bool compress, bool allowLocal, bool preferLocal)
 534                 {
 535                         Sequence<PathElementBase> bestParameterPath = null;
 536                         Sequence<PathElementBase> bestLocalPath = null;
 537                         Sequence<PathElementBase> bestFieldMethodPath = null;
 538
 539                         foreach (var path in GetAccessPathsFiltered (sv, filter, compress)) {
 540                                 if (path != null) {
 541                                         if (path.Head is PathElement<Parameter>) {
 542                                                 if (bestParameterPath == null || bestParameterPath.Length () > path.Length ())
 543                                                         bestParameterPath = path;
 544                                         } else if (filter.AllowLocal && allowLocal && path.Head is PathElement<Local>) {
 545                                                 if (!path.Head.ToString ().Contains ("$") && (bestLocalPath == null || bestLocalPath.Length () > path.Length ()))
 546                                                         bestLocalPath = path;
 547                                         } else if (path.Head is PathElement<Field> && path.Head.Func.IsStatic) {
 548                                                 if (bestFieldMethodPath == null || bestFieldMethodPath.Length () > path.Length ())
 549                                                         bestFieldMethodPath = path;
 550                                         } else if (path.Head is PathElement<Method> && path.Head.Func.IsStatic) {
 551                                                 if (bestFieldMethodPath == null || bestFieldMethodPath.Length () > path.Length ())
 552                                                         bestFieldMethodPath = path;
 553                                         }
 554                                 }
 555                         }
 556                         if (preferLocal && bestLocalPath != null)
 557                                 return bestLocalPath;
 558                         if (bestParameterPath != null)
 559                                 return bestParameterPath;
 560                         if (allowLocal && bestLocalPath != null)
 561                                 return bestLocalPath;
 562
 563                         return bestFieldMethodPath;
 564                 }
 565
 566                 public IEnumerable<Sequence<PathElementBase>> GetAccessPathsFiltered (SymValue sv, AccessPathFilter<Method> filter, bool compress)
 567                 {
 568                         return GetAccessPathsTyped (sv, filter, compress).Where (path => PathIsVisibleAccordingToFilter (path, filter));
 569                 }
 570
 571                 private bool PathIsVisibleAccordingToFilter (Sequence<PathElementBase> path, AccessPathFilter<Method> filter)
 572                 {
 573                         if (path.Length () == 0 || !filter.HasVisibilityMember)
 574                                 return true;
 575
 576                         Method visibilityMember = filter.VisibilityMember;
 577                         TypeNode t = MetaDataProvider.DeclaringType (visibilityMember);
 578                         TypeNode type = default(TypeNode);
 579
 580                         while (path != null) {
 581                                 PathElement pathElement = path.Head;
 582                                 if (!pathElement.TryGetResultType (out type))
 583                                         return true;
 584                                 while (MetaDataProvider.IsManagedPointer (type))
 585                                         type = MetaDataProvider.ElementType (type);
 586                                 if ("this" != pathElement.ToString ()) {
 587                                         var peMethod = pathElement as PathElement<Method>;
 588                                         if (peMethod != null) {
 589                                                 Method method = peMethod.Element;
 590                                                 if (!MetaDataProvider.IsVisibleFrom (method, t))
 591                                                         return false;
 592                                         }
 593
 594                                         var peProperty = pathElement as PathElement<Property>;
 595                                         if (peProperty != null) {
 596                                                 Property property = peProperty.Element;
 597                                                 Method method;
 598                                                 if (!MetaDataProvider.HasGetter (property, out method))
 599                                                         MetaDataProvider.HasSetter (property, out method);
 600
 601                                                 if (!MetaDataProvider.IsVisibleFrom (method, t))
 602                                                         return false;
 603                                         }
 604
 605                                         var peField = pathElement as PathElement<Field>;
 606                                         if (peField != null) {
 607                                                 Field field = peField.Element;
 608                                                 if (!MetaDataProvider.IsVisibleFrom (field, t))
 609                                                         return false;
 610                                         }
 611                                 }
 612                                 path = path.Tail;
 613                         }
 614                         return true;
 615                 }
 616
 617                 private bool TryPropagateTypeInfo (Sequence<PathElementBase> path, out Sequence<PathElementBase> result)
 618                 {
 619                         if (path == null) {
 620                                 result = null;
 621                                 return true;
 622                         }
 623                         PathElementBase head = path.Head;
 624                         TypeNode prevType;
 625                         if (!head.TrySetType (MetaDataProvider.System_IntPtr, MetaDataProvider, out prevType)) {
 626                                 result = null;
 627                                 return false;
 628                         }
 629
 630                         Sequence<PathElementBase> result1;
 631                         if (!TryPropagateTypeInfoRecurse (path.Tail, prevType, out result1)) {
 632                                 result = null;
 633                                 return false;
 634                         }
 635                         if (head.IsAddressOf && head is PathElement<Parameter> && result1 != null && result1.Head.IsDeref) {
 636                                 var pathElement = (PathElement<Parameter>) head;
 637                                 result = result1.Tail.Cons (new ParameterPathElement (pathElement.Element, pathElement.Description, pathElement.Func, MetaDataProvider));
 638                                 return true;
 639                         }
 640
 641                         result = result1.Cons (head);
 642                         return true;
 643                 }
 644
 645                 private bool TryPropagateTypeInfoRecurse (Sequence<PathElementBase> path, TypeNode prevType, out Sequence<PathElementBase> result)
 646                 {
 647                         if (path == null) {
 648                                 result = null;
 649                                 return true;
 650                         }
 651                         PathElementBase head = path.Head;
 652                         if (head.TrySetType (prevType, MetaDataProvider, out prevType)) {
 653                                 Sequence<PathElementBase> updatedPath;
 654                                 if (TryPropagateTypeInfoRecurse (path.Tail, prevType, out updatedPath)) {
 655                                         result = updatedPath.Cons (head);
 656                                         return true;
 657                                 }
 658                         }
 659
 660                         result = null;
 661                         return false;
 662                 }
 663
 664                 private IEnumerable<Sequence<PathElementBase>> GetAccessPathsTyped (SymValue sv, AccessPathFilter<Method> filter, bool compress)
 665                 {
 666                         var visited = new HashSet<SymValue> ();
 667                         foreach (var path in GetAccessPathsRaw (sv, null, visited, filter, compress)) {
 668                                 Sequence<PathElementBase> result;
 669                                 if (TryPropagateTypeInfo (path, out result))
 670                                         yield return result;
 671                         }
 672                 }
 673
 674                 private void CopyNonStructWithFieldValue (SymValue destAddr, SymValue sv, FlatDomain<TypeNode> addrType)
 675                 {
 676                         this.egraph [this.Functions.ValueOf, destAddr] = sv;
 677                         SetType (destAddr, addrType);
 678                 }
 679
 680                 public bool IsConstant (SymValue source, out TypeNode type, out object constant)
 681                 {
 682                         SymFunction c = this.constantLookup [source];
 683                         if (c != null)
 684                                 return this.Functions.IsConstant (c, out type, out constant);
 685
 686                         type = default(TypeNode);
 687                         constant = null;
 688                         return false;
 689                 }
 690
 691                 private void CopyOldStructValue (APC pc, SymValue destAddr, SymValue srcAddr, TypeNode type, Domain target, bool atEndOld)
 692                 {
 693                         throw new NotImplementedException ();
 694                 }
 695
 696                 public void SetValue (SymValue destAddr, SymValue sourceAddr, FlatDomain<TypeNode> addrType, bool cast)
 697                 {
 698                         FlatDomain<TypeNode> type = TargetType (addrType);
 699                         if (IsStructWithFields (type))
 700                                 CopyStructValue (destAddr, sourceAddr, type.Value);
 701
 702                         CopyPrimValue (destAddr, sourceAddr, cast, type);
 703                 }
 704
 705                 private void CopyPrimValue (SymValue destAddr, SymValue sourceAddr, bool cast, FlatDomain<TypeNode> elementType)
 706                 {
 707                         SymValue value = this.egraph [this.Functions.ValueOf, sourceAddr];
 708                         if (cast)
 709                                 SetType (value, elementType);
 710                         else
 711                                 SetTypeIfUnknown (value, elementType);
 712
 713                         if (elementType.IsNormal()) {
 714                                 if (NeedsArrayLengthManifested (elementType.Value))
 715                                         ManifestArrayLength (value);
 716                         }
 717
 718                         this.egraph [this.Functions.ValueOf, destAddr] = value;
 719                 }
 720
 721                 public void CopyValueToOldState (APC pc, TypeNode type, int dest, int source, Domain target)
 722                 {
 723                         SymValue destAddress = target.Address (dest);
 724                         SymValue srcAddress = Address (source);
 725
 726                         AbstractType aType = GetType (srcAddress);
 727                         TypeNode addrType = aType.IsNormal() ? aType.ConcreteType : MetaDataProvider.ManagedPointer (type);
 728                         CopyValueToOldState (pc, addrType, destAddress, srcAddress, target);
 729                 }
 730
 731                 private void CopyValueToOldState (APC pc, TypeNode addrType, SymValue destAddress, SymValue srcAddress, Domain target)
 732                 {
 733                         target.MakeTotallyModified (destAddress);
 734                         if (destAddress != srcAddress)
 735                                 target.HavocIfStruct (destAddress);
 736                         target.SetType (destAddress, addrType);
 737                         FlatDomain<TypeNode> targetType = TargetType (addrType);
 738                         if (IsStructWithFields (targetType))
 739                                 CopyStructValueToOldState (pc, destAddress, srcAddress, targetType, target);
 740                         else {
 741                                 SymValue sv = this.egraph.TryLookup (this.Functions.ValueOf, srcAddress);
 742                                 if (sv == null) {
 743                                         if (this.egraph.IsImmutable)
 744                                                 return;
 745                                         sv = this.egraph [this.Functions.ValueOf, srcAddress];
 746                                 }
 747                                 CopyPrimitiveValueToOldState (pc, addrType, destAddress, sv, target);
 748                         }
 749                 }
 750
 751                 private void CopyPrimitiveValueToOldState (APC pc, TypeNode addrType, SymValue destAddress, SymValue sv, Domain target)
 752                 {
 753                         if (target.IsValidSymbol (sv))
 754                                 target.CopyNonStructWithFieldValue (destAddress, sv, addrType);
 755                         else
 756                                 target.Assign (destAddress, addrType);
 757                 }
 758
 759                 private bool IsValidSymbol (SymValue sv)
 760                 {
 761                         return this.egraph.IsValidSymbol (sv);
 762                 }
 763
 764                 private void Assign (SymValue destAddress, TypeNode addrType)
 765                 {
 766                         Havoc (destAddress);
 767                         SetType (destAddress, addrType);
 768                         FlatDomain<TypeNode> targetType = TargetType (addrType);
 769                         if (IsStructWithFields (targetType))
 770                                 return;
 771
 772                         SymValue fresh = this.egraph.FreshSymbol ();
 773                         SetType (fresh, targetType);
 774                         this.egraph [this.Functions.ValueOf, destAddress] = fresh;
 775                         if (!targetType.IsNormal())
 776                                 return;
 777
 778                         if (NeedsArrayLengthManifested (targetType.Value))
 779                                 ManifestArrayLength (fresh);
 780                 }
 781
 782                 private void CopyStructValueToOldState (APC pc, SymValue destAddress, SymValue srcAddress, FlatDomain<TypeNode> targetType, Domain target)
 783                 {
 784                         throw new NotImplementedException ();
 785                 }
 786
 787                 public void ManifestArrayLength (SymValue arrayValue)
 788                 {
 789                         SetType (this.egraph [this.Functions.Length, arrayValue], MetaDataProvider.System_Int32);
 790                 }
 791
 792                 public bool NeedsArrayLengthManifested (TypeNode type)
 793                 {
 794                         return MetaDataProvider.IsArray (type) || MetaDataProvider.System_String.Equals (type);
 795                 }
 796
 797                 public void CopyStructValue (SymValue destAddr, SymValue sourceAddr, TypeNode type)
 798                 {
 799                         if (destAddr == null)
 800                                 return;
 801                         this.egraph [this.Functions.StructId, destAddr] = this.egraph [this.Functions.StructId, sourceAddr];
 802                         foreach (SymFunction function in this.egraph.Functions (sourceAddr)) {
 803                                 if (function.ActsAsField) {
 804                                         TypeNode functionType = function.FieldAddressType ();
 805                                         CopyValue (this.egraph [function, destAddr], this.egraph [function, sourceAddr], functionType);
 806                                 }
 807                         }
 808                 }
 809
 810                 public SymValue OldValueAddress (Parameter p)
 811                 {
 812                         return Address (OldValueParameterConstructor (p));
 813                 }
 814
 815                 private SymFunction OldValueParameterConstructor (Parameter argument)
 816                 {
 817                         return this.Functions.For ("$OldParameter_" + MetaDataProvider.Name (argument));
 818                 }
 819
 820                 public void CopyParameterIntoShadow (Parameter p)
 821                 {
 822                         CopyValue (Address (OldValueParameterConstructor (p)), Address (this.Functions.For (p)));
 823                 }
 824
 825                 public void Copy (int dest, int source)
 826                 {
 827                         CopyValue (Address (this.Functions.For (dest)), Address (this.Functions.For (source)));
 828                 }
 829
 830                 private bool IsIEnumerable (TypeNode type)
 831                 {
 832                         TypeNode ienumerableType;
 833                         return (this.IEnumerable1Type.TryGet (MetaDataProvider, out ienumerableType) && MetaDataProvider.DerivesFrom (type, ienumerableType)
 834                                 || this.IEnumerableType.TryGet (MetaDataProvider, out ienumerableType) && MetaDataProvider.DerivesFrom (type, ienumerableType));
 835                 }
 836
 837                 public SymValue GetSpecialUnary (SymFunction op, int source, FlatDomain<TypeNode> type)
 838                 {
 839                         SymValue value = Value (source);
 840                         SymValue sv = this.egraph [op, value];
 841                         SetType (sv, type);
 842                         return sv;
 843                 }
 844
 845                 private SymValue LookupAddressAndManifestType (SymValue[] args, SymFunction op, TypeNode type, out bool fresh)
 846                 {
 847                         SymValue sv = this.egraph.TryLookup (op, args);
 848                         if (sv != null) {
 849                                 fresh = false;
 850                                 return sv;
 851                         }
 852                         fresh = true;
 853                         sv = this.egraph [op, args];
 854                         SetType (sv, type);
 855                         return sv;
 856                 }
 857
 858                 public bool IsZero (SymValue symValue)
 859                 {
 860                         return this.egraph [symValue].IsZero;
 861                 }
 862
 863                 public SymValue Value (int v)
 864                 {
 865                         return Value (Address (this.Functions.For (v)));
 866                 }
 867
 868                 public SymValue Value (SymValue address)
 869                 {
 870                         bool fresh;
 871                         SymValue symbol = this.egraph.LookupOrManifest (this.Functions.ValueOf, address, out fresh);
 872
 873                         if (fresh && IsUnmodified (address))
 874                                 MakeUnmodified (symbol);
 875
 876                         return symbol;
 877                 }
 878
 879                 public SymValue Value (Parameter p)
 880                 {
 881                         return Value (Address (this.Functions.For (p)));
 882                 }
 883
 884                 public void MakeUnmodified (SymValue value)
 885                 {
 886                         this.unmodifiedSinceEntry = this.unmodifiedSinceEntry.Add (value);
 887                 }
 888
 889                 private bool IsUnmodified (SymValue value)
 890                 {
 891                         return this.unmodifiedSinceEntry.Contains (value);
 892                 }
 893
 894                 public AbstractType CurrentType (int stackPos)
 895                 {
 896                         return CurrentType (Value (Address (this.Functions.For (stackPos))));
 897                 }
 898
 899                 private AbstractType CurrentType (SymValue address)
 900                 {
 901                         return this.egraph [address];
 902                 }
 903
 904                 public Domain Assume (int t, bool truth)
 905                 {
 906                         return Assume (Value (t), truth);
 907                 }
 908
 909                 private Domain Assume (SymValue sv, bool truth)
 910                 {
 911                         if (!truth) {
 912                                 if (IsNonZero (sv))
 913                                         return Bottom;
 914                                 this.egraph [sv] = this.egraph [sv].ButZero;
 915                                 foreach (var term in this.egraph.EqTerms (sv)) {
 916                                         if (term.Function == this.Functions.UnaryNot || term.Function == this.Functions.NeZero)
 917                                                 return Assume (term.Args [0], true);
 918                                 }
 919                         } else {
 920                                 if (this.egraph [sv].IsZero)
 921                                         return Bottom;
 922                                 foreach (var term in this.egraph.EqTerms (sv)) {
 923                                         if (term.Function == this.Functions.UnaryNot || term.Function == this.Functions.NeZero)
 924                                                 return Assume (term.Args [0], false);
 925                                 }
 926                         }
 927
 928                         return this;
 929                 }
 930
 931                 private bool IsNonZero (SymValue sv)
 932                 {
 933                         foreach (var term in this.egraph.EqTerms (sv)) {
 934                                 var wrapper = term.Function as Wrapper<object>;
 935                                 if (wrapper != null && wrapper.Item is int && (int) wrapper.Item != 0)
 936                                         return true;
 937                         }
 938                         return false;
 939                 }
 940
 941                 public FlatDomain<TypeNode> BinaryResultType (BinaryOperator op, AbstractType t1, AbstractType t2)
 942                 {
 943                         switch (op) {
 944                         case BinaryOperator.Add:
 945                         case BinaryOperator.Add_Ovf:
 946                         case BinaryOperator.Add_Ovf_Un:
 947                                 if (t1.IsZero)
 948                                         return t2.Type;
 949                                 return t1.Type;
 950                         case BinaryOperator.Sub:
 951                         case BinaryOperator.Sub_Ovf:
 952                         case BinaryOperator.Sub_Ovf_Un:
 953                                 return t1.Type;
 954                         case BinaryOperator.Ceq:
 955                         case BinaryOperator.Cobjeq:
 956                         case BinaryOperator.Cne_Un:
 957                         case BinaryOperator.Cge:
 958                         case BinaryOperator.Cge_Un:
 959                         case BinaryOperator.Cgt:
 960                         case BinaryOperator.Cgt_Un:
 961                         case BinaryOperator.Cle:
 962                         case BinaryOperator.Cle_Un:
 963                         case BinaryOperator.Clt:
 964                         case BinaryOperator.Clt_Un:
 965                                 return MetaDataProvider.System_Boolean;
 966                         default:
 967                                 return t1.Type;
 968                         }
 969                 }
 970
 971                 private bool IsStructWithFields (FlatDomain<TypeNode> type)
 972                 {
 973                         if (!type.IsNormal())
 974                                 return false;
 975
 976                         return !MetaDataProvider.HasValueRepresentation (type.Value);
 977                 }
 978
 979                 private FlatDomain<TypeNode> TargetType (FlatDomain<TypeNode> type)
 980                 {
 981                         if (!type.IsNormal())
 982                                 return type;
 983
 984                         TypeNode normalType = type.Value;
 985                         if (MetaDataProvider.IsManagedPointer (normalType))
 986                                 return MetaDataProvider.ElementType (normalType);
 987
 988                         return FlatDomain<TypeNode>.TopValue;
 989                 }
 990
 991                 public void SetType (SymValue sv, FlatDomain<TypeNode> type)
 992                 {
 993                         AbstractType abstractType = this.egraph [sv];
 994                         if (abstractType.IsZero)
 995                                 return;
 996
 997                         this.egraph [sv] = abstractType.With (type);
 998                 }
 999
1000                 private void SetTypeIfUnknown (SymValue sv, FlatDomain<TypeNode> type)
1001                 {
1002                         AbstractType abstractType = this.egraph [sv];
1003
1004                         if (!abstractType.IsZero && (!abstractType.Type.IsNormal() || abstractType.Type.Equals (MetaDataProvider.System_IntPtr)))
1005                                 this.egraph [sv] = abstractType.With (type);
1006                 }
1007
1008                 private void MakeTotallyModified (SymValue dest)
1009                 {
1010                         this.unmodifiedSinceEntry = this.unmodifiedSinceEntry.Remove (dest);
1011                         this.unmodifiedFieldsSinceEntry = this.unmodifiedFieldsSinceEntry.Remove (dest);
1012                 }
1013
1014                 private bool AreUnmodified (IEnumerable<SymValue> values)
1015                 {
1016                         return values.All (IsUnmodified);
1017                 }
1018
1019                 private bool AnyAreModifiedAtCall (IEnumerable<SymValue> values)
1020                 {
1021                         return values.Any (IsModifiedAtCall);
1022                 }
1023
1024                 private bool IsModifiedAtCall (SymValue sv)
1025                 {
1026                         return (this.ModifiedAtCall != null && this.ModifiedAtCall.Contains (sv));
1027                 }
1028
1029                 public Domain GetStateAt (APC pc)
1030                 {
1031                         Domain ifFound;
1032                         this.parent.PreStateLookup (pc, out ifFound);
1033
1034                         return ifFound;
1035                 }
1036
1037                 public bool TryGetCorrespondingValueAbstraction (int v, out SymbolicValue sv)
1038                 {
1039                         return TryGetCorrespondingValueAbstraction (this.Functions.For (v), out sv);
1040                 }
1041
1042                 private bool TryGetCorrespondingValueAbstraction (SymFunction v, out SymbolicValue sv)
1043                 {
1044                         if (!IsBottom) {
1045                                 SymValue loc = TryAddress (v);
1046                                 if (loc != null) {
1047                                         SymValue symbol = TryCorrespondingValue (loc);
1048                                         if (symbol != null) {
1049                                                 sv = new SymbolicValue (symbol);
1050                                                 return true;
1051                                         }
1052                                 }
1053                         }
1054
1055                         sv = default(SymbolicValue);
1056                         return false;
1057                 }
1058
1059                 private SymValue TryCorrespondingValue (SymValue address)
1060                 {
1061                         if (IsStructAddress (this.egraph [address]))
1062                                 return address;
1063
1064                         return TryValue (address);
1065                 }
1066
1067                 private bool IsStructAddress (AbstractType abstractType)
1068                 {
1069                         if (!abstractType.IsNormal())
1070                                 return false;
1071
1072                         TypeNode normalType = abstractType.ConcreteType;
1073                         if (MetaDataProvider.IsManagedPointer (normalType))
1074                                 return !MetaDataProvider.HasValueRepresentation (MetaDataProvider.ElementType (normalType));
1075
1076                         return false;
1077                 }
1078
1079                 private SymValue TryAddress (SymFunction c)
1080                 {
1081                         return this.egraph.TryLookup (c);
1082                 }
1083
1084                 public bool TryGetCorrespondingValueAbstraction (Local v, out SymbolicValue sv)
1085                 {
1086                         return TryGetCorrespondingValueAbstraction (this.Functions.For (v), out sv);
1087                 }
1088
1089                 public bool TryGetUnboxedValue (int source, out SymbolicValue sv)
1090                 {
1091                         return TryGetUnboxedValue (TryValue (Address (source)), out sv);
1092                 }
1093
1094                 private bool TryGetUnboxedValue (SymValue box, out SymbolicValue sv)
1095                 {
1096                         if (box != null) {
1097                                 SymValue symbol = TryValue (box);
1098                                 if (symbol != null && this.egraph.TryLookup (this.Functions.BoxOperator, symbol) == box) {
1099                                         sv = new SymbolicValue (symbol);
1100                                         return true;
1101                                 }
1102                         }
1103                         sv = new SymbolicValue ();
1104                         return false;
1105                 }
1106
1107                 public SymValue TryValue (SymValue address)
1108                 {
1109                         return this.egraph.TryLookup (this.Functions.ValueOf, address);
1110                 }
1111
1112                 public AbstractType GetType (SymValue symbol)
1113                 {
1114                         return this.egraph [symbol];
1115                 }
1116
1117                 public SymValue CreateObject (TypeNode type)
1118                 {
1119                         SymValue sv = this.egraph.FreshSymbol ();
1120                         SetType (sv, type);
1121                         return sv;
1122                 }
1123
1124                 public SymValue CreateValue (TypeNode type)
1125                 {
1126                         SymValue sv = this.egraph.FreshSymbol ();
1127                         SetType (sv, MetaDataProvider.ManagedPointer (type));
1128                         return sv;
1129                 }
1130
1131                 public void HavocArrayAtIndex (SymValue arrayValue, SymValue indexValue)
1132                 {
1133                         this.egraph.Eliminate (this.Functions.ElementAddress, arrayValue);
1134                 }
1135
1136                 public SymValue CreateArray (TypeNode type, SymValue len)
1137                 {
1138                         SymValue sv = this.egraph.FreshSymbol ();
1139                         this.egraph [this.Functions.Length, sv] = len;
1140                         SetType (sv, MetaDataProvider.ArrayType (type, 1));
1141                         return sv;
1142                 }
1143
1144                 public SymValue ElementAddress (SymValue array, SymValue index, TypeNode elementAddressType)
1145                 {
1146                         SymValue objVersion = this.egraph [this.Functions.ObjectVersion, array];
1147                         SymValue sv = this.egraph.TryLookup (this.Functions.ElementAddress, objVersion, index);
1148                         if (sv == null) {
1149                                 sv = this.egraph [this.Functions.ElementAddress, objVersion, index];
1150                                 SetType (sv, elementAddressType);
1151                                 this.egraph [this.Functions.ResultOfLoadElement, sv] = Zero;
1152                         }
1153                         return sv;
1154                 }
1155
1156                 public void CopyValueAndCast (SymValue destAddr, SymValue srcAddr, TypeNode addrType)
1157                 {
1158                         CopyValue (destAddr, srcAddr, addrType, true, true);
1159                 }
1160
1161                 public void HavocObjectAtCall (SymValue obj, ref IImmutableSet<SymValue> havoced, bool havocFields, bool havocReadonlyFields)
1162                 {
1163                         HavocFields (null, obj, ref havoced, havocReadonlyFields);
1164                         HavocUp (obj, ref havoced, havocFields);
1165                 }
1166
1167                 public bool IsThis (Method currentMethod, int i)
1168                 {
1169                         if (MetaDataProvider.IsStatic (currentMethod))
1170                                 return false;
1171                         return Value (MetaDataProvider.This (currentMethod)) == Value (i);
1172                 }
1173
1174                 public void AssignValueAndNullnessAtConv_IU (int dest, int source, bool unsigned)
1175                 {
1176                         AbstractType aType = CurrentType (source);
1177                         AssignValueAndNullnessAtConv_IU (Address (this.Functions.For (dest)), unsigned, aType);
1178                 }
1179
1180                 private void AssignValueAndNullnessAtConv_IU (SymValue address, bool unsigned, AbstractType aType)
1181                 {
1182                         Havoc (address);
1183                         FlatDomain<TypeNode> type = aType.Type;
1184                         if (!IsStructWithFields (type)) {
1185                                 SymValue ptrValue = this.egraph.FreshSymbol ();
1186                                 if (type.IsNormal())
1187                                         aType = new AbstractType (!unsigned ? MetaDataProvider.System_IntPtr : MetaDataProvider.System_UIntPtr, aType.IsZero);
1188                                 SetType (address, type.IsNormal() ? MetaDataProvider.ManagedPointer (type.Value) : type);
1189                                 this.egraph [ptrValue] = aType;
1190                                 this.egraph [this.Functions.ValueOf, address] = ptrValue;
1191                         } else
1192                                 SetType (address, type.IsNormal() ? MetaDataProvider.ManagedPointer (type.Value) : type);
1193                 }
1194
1195                 public TypeNode UnaryResultType (UnaryOperator op, AbstractType type)
1196                 {
1197                         switch (op) {
1198                         case UnaryOperator.Conv_i1:
1199                                 return MetaDataProvider.System_Int8;
1200                         case UnaryOperator.Conv_i2:
1201                                 return MetaDataProvider.System_Int16;
1202                         case UnaryOperator.Conv_i4:
1203                                 return MetaDataProvider.System_Int32;
1204                         case UnaryOperator.Conv_i8:
1205                                 return MetaDataProvider.System_Int64;
1206                         case UnaryOperator.Conv_u1:
1207                                 return MetaDataProvider.System_UInt8;
1208                         case UnaryOperator.Conv_u2:
1209                                 return MetaDataProvider.System_UInt16;
1210                         case UnaryOperator.Conv_u4:
1211                                 return MetaDataProvider.System_UInt32;
1212                         case UnaryOperator.Conv_u8:
1213                                 return MetaDataProvider.System_UInt64;
1214                         default:
1215                                 if (type.IsNormal())
1216                                         return type.ConcreteType;
1217                                 return MetaDataProvider.System_Int32;
1218                         }
1219                 }
1220
1221                 public void CopyStackAddress (SymValue destAddr, int temporaryForWhichAddressIsTaken)
1222                 {
1223                         SymValue srcAddr = Address (temporaryForWhichAddressIsTaken);
1224                         this.egraph [this.Functions.ValueOf, destAddr] = srcAddr;
1225                         AbstractType aType = CurrentType (srcAddr);
1226                         FlatDomain<TypeNode> t = !aType.IsNormal() ? new FlatDomain<TypeNode> () : MetaDataProvider.ManagedPointer (aType.Type.Value);
1227                         SetType (destAddr, t);
1228                 }
1229
1230                 public SymValue PseudoFieldAddress (SymValue ptr, Method getter)
1231                 {
1232                         TypeNode pseudoFieldAddressType;
1233                         return PseudoFieldAddress (ptr, getter, out pseudoFieldAddressType, false);
1234                 }
1235
1236                 public SymValue PseudoFieldAddress (SymValue sv, Method m, out TypeNode pseudoFieldAddressType, bool materialize)
1237                 {
1238                         pseudoFieldAddressType = MetaDataProvider.ManagedPointer (MetaDataProvider.ReturnType (m));
1239                         m = MetaDataProvider.Unspecialized (m);
1240                         bool fresh;
1241                         SymValue elem = LookupAddressAndManifestType (sv, this.Functions.For (m), pseudoFieldAddressType, out fresh);
1242                         if (fresh) {
1243                                 if (IsUnmodified (sv))
1244                                         MakeModified (elem);
1245                                 if (IsModifiedAtCall (sv))
1246                                         this.ModifiedAtCall = this.ModifiedAtCall.Add (elem);
1247                                 if (materialize)
1248                                         MaterializeAccordingToType (elem, pseudoFieldAddressType, 0);
1249                         }
1250                         return elem;
1251                 }
1252
1253                 public SymValue FieldAddress (SymValue ptr, Field field)
1254                 {
1255                         TypeNode fieldAddressType;
1256                         return FieldAddress (ptr, field, out fieldAddressType);
1257                 }
1258
1259                 public SymValue FieldAddress (SymValue ptr, Field field, out TypeNode fieldAddressType)
1260                 {
1261                         fieldAddressType = MetaDataProvider.ManagedPointer (MetaDataProvider.FieldType (field));
1262                         bool fresh;
1263                         SymValue sv = LookupAddressAndManifestType (ptr, this.Functions.For (field), fieldAddressType, out fresh);
1264                         if (fresh) {
1265                                 if (IsUnmodifiedForFields (ptr) || MetaDataProvider.IsReadonly (field))
1266                                         MakeUnmodified (sv);
1267                                 if (IsModifiedAtCall (ptr))
1268                                         this.ModifiedAtCall = this.ModifiedAtCall.Add (sv);
1269                         }
1270                         return sv;
1271                 }
1272
1273                 public void Assign (Parameter parameter, TypeNode type)
1274                 {
1275                         AssignValue (Address (this.Functions.For (parameter)), type);
1276                 }
1277
1278                 public SymValue PseudoFieldAddressOfOutParameter (int index, SymValue fieldAddr, TypeNode pType)
1279                 {
1280                         SymValue sv = this.egraph [this.Functions.ForConstant (index, MetaDataProvider.System_Int32), fieldAddr];
1281                         MaterializeAccordingToType (sv, pType, 2);
1282                         return sv;
1283                 }
1284
1285                 public SymValue ObjectVersion (SymValue sv)
1286                 {
1287                         return this.egraph [this.Functions.ObjectVersion, sv];
1288                 }
1289
1290                 public SymValue PseudoFieldAddress (SymValue[] args, Method method, out TypeNode pseudoFieldAddressType, bool materialize)
1291                 {
1292                         if (args.Length == 0 || args.Length == 1)
1293                                 return PseudoFieldAddress (Globals, method, out pseudoFieldAddressType, materialize);
1294                         pseudoFieldAddressType = MetaDataProvider.ManagedPointer (MetaDataProvider.ReturnType (method));
1295                         method = MetaDataProvider.Unspecialized (method);
1296
1297                         bool fresh;
1298                         SymValue sv = LookupAddressAndManifestType (args, this.Functions.For (method), pseudoFieldAddressType, out fresh);
1299                         if (fresh) {
1300                                 if (AreUnmodified (args))
1301                                         MakeUnmodified (sv);
1302                                 if (AnyAreModifiedAtCall (args))
1303                                         this.ModifiedAtCall = this.ModifiedAtCall.Add (sv);
1304                                 if (materialize)
1305                                         MaterializeAccordingToType (sv, pseudoFieldAddressType, 0);
1306                         }
1307                         return sv;
1308                 }
1309
1310                 public void AssignReturnValue (int dest, TypeNode type)
1311                 {
1312                         AssignValue (dest, type);
1313                         if (MetaDataProvider.HasValueRepresentation (type))
1314                                 this.egraph [this.Functions.ResultOfCall, Value (dest)] = Zero;
1315                         else
1316                                 MaterializeAccordingToType (Address (dest), MetaDataProvider.ManagedPointer (type), 0);
1317                 }
1318
1319                 public void MaterializeAccordingToType (SymValue sv, TypeNode type, int depth)
1320                 {
1321                         SetType (sv, type);
1322                         if (depth > 2)
1323                                 return;
1324
1325                         if (MetaDataProvider.IsManagedPointer (type)) {
1326                                 TypeNode elementType = MetaDataProvider.ElementType (type);
1327                                 if (!MetaDataProvider.HasValueRepresentation (elementType)) {
1328                                         ManifestStructId (sv);
1329                                         foreach (Field field in MetaDataProvider.Fields (elementType)) {
1330                                                 if (!MetaDataProvider.IsStatic (field)) {
1331                                                         TypeNode fieldAddressType;
1332                                                         MaterializeAccordingToType (FieldAddress (sv, field, out fieldAddressType), fieldAddressType, depth + 1);
1333                                                 }
1334                                         }
1335                                         foreach (Property property in MetaDataProvider.Properties (elementType)) {
1336                                                 Method getter;
1337                                                 if (!MetaDataProvider.IsStatic (property) && MetaDataProvider.HasGetter (property, out getter)) {
1338                                                         TypeNode pseudoFieldAddressType;
1339                                                         MaterializeAccordingToType (PseudoFieldAddress (sv, getter, out pseudoFieldAddressType, false), pseudoFieldAddressType, depth + 1);
1340                                                 }
1341                                         }
1342                                 } else
1343                                         MaterializeAccordingToType (Value (sv), elementType, depth + 1);
1344                         }
1345                 }
1346
1347                 public void ManifestStructId (SymValue sv)
1348                 {
1349                         StructId (sv);
1350                 }
1351
1352                 public SymValue StructId (SymValue sv)
1353                 {
1354                         return this.egraph [this.Functions.StructId, sv];
1355                 }
1356
1357                 private SymValue LookupAddressAndManifestType (SymValue sv, SymFunction c, TypeNode type, out bool fresh)
1358                 {
1359                         SymValue value = this.egraph.TryLookup (c, sv);
1360                         if (value != null) {
1361                                 fresh = false;
1362                                 return value;
1363                         }
1364
1365                         fresh = true;
1366                         value = this.egraph [c, sv];
1367                         SetType (value, type);
1368
1369                         return value;
1370                 }
1371
1372                 public void HavocFields (SymValue sv, IEnumerable<Field> fields, ref IImmutableSet<SymValue> havoced)
1373                 {
1374                         foreach (Field f in fields)
1375                                 HavocConstructor (null, sv, this.Functions.For (f), ref havoced, false);
1376                 }
1377
1378                 private bool IsUnmodifiedForFields (SymValue sv)
1379                 {
1380                         return this.unmodifiedFieldsSinceEntry.Contains (sv);
1381                 }
1382
1383                 public void HavocUp (SymValue srcAddr, ref IImmutableSet<SymValue> havocedAtCall, bool havocFields)
1384                 {
1385                         foreach (var term in this.egraph.EqTerms (srcAddr)) {
1386                                 if (term.Function == this.Functions.ValueOf)
1387                                         HavocUpField (term.Args [0], ref havocedAtCall, havocFields);
1388                         }
1389                 }
1390
1391                 private void HavocUpField (SymValue sv, ref IImmutableSet<SymValue> havocedAtCall, bool havocFields)
1392                 {
1393                         foreach (var term in this.egraph.EqTerms (sv)) {
1394                                 SymFunction accessedVia = term.Function;
1395                                 if (accessedVia is Wrapper<Field>)
1396                                         HavocUpObjectVersion (accessedVia, term.Args [0], ref havocedAtCall, havocFields);
1397                                 else {
1398                                         var methodWrapper = accessedVia as Wrapper<Method>;
1399                                         Property property;
1400                                         if (methodWrapper != null && !MetaDataProvider.IsStatic (methodWrapper.Item) && MetaDataProvider.IsPropertyGetter (methodWrapper.Item, out property))
1401                                                 HavocUpObjectVersion (accessedVia, term.Args [0], ref havocedAtCall, havocFields);
1402                                 }
1403                         }
1404                 }
1405
1406                 private void HavocUpObjectVersion (SymFunction accessedVia, SymValue sv, ref IImmutableSet<SymValue> havocedAtCall, bool havocFields)
1407                 {
1408                         if (havocedAtCall.Contains (sv))
1409                                 return;
1410                         this.egraph.Eliminate (this.Functions.ObjectVersion, sv);
1411                         if (havocFields)
1412                                 HavocMutableFields (accessedVia, sv, ref havocedAtCall);
1413                         else
1414                                 HavocPseudoFields (accessedVia, sv, ref havocedAtCall);
1415
1416                         HavocUp (sv, ref havocedAtCall, false);
1417                 }
1418
1419                 public void CopyAddress (SymValue destAddr, SymValue srcAddr, TypeNode type)
1420                 {
1421                         this.egraph [this.Functions.ValueOf, destAddr] = srcAddr;
1422                         SetType (destAddr, MetaDataProvider.ManagedPointer (type));
1423                 }
1424
1425                 public void AssignArrayLength (SymValue destAddr, SymValue array)
1426                 {
1427                         SymValue length = this.egraph [this.Functions.Length, array];
1428                         SetType (length, MetaDataProvider.System_Int32);
1429                         this.egraph [this.Functions.ValueOf, destAddr] = length;
1430                         SetType (destAddr, MetaDataProvider.ManagedPointer (MetaDataProvider.System_Int32));
1431                 }
1432
1433                 public void ResetModifiedAtCall ()
1434                 {
1435                         this.ModifiedAtCall = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
1436                 }
1437
1438                 public SymValue LoadValue (int source)
1439                 {
1440                         return Value (source);
1441                 }
1442
1443                 public SymbolicValue TryLoadValue (SymValue addr)
1444                 {
1445                         return new SymbolicValue (Value (addr));
1446                 }
1447
1448                 public bool TryGetArrayLength (SymValue arrayValue, out SymValue length)
1449                 {
1450                         length = this.egraph.TryLookup (this.Functions.Length, arrayValue);
1451                         return length != null;
1452                 }
1453
1454                 public bool TryGetCorrespondingValueAbstraction (Parameter p, out SymbolicValue sv)
1455                 {
1456                         return TryGetCorrespondingValueAbstraction (this.Functions.For (p), out sv);
1457                 }
1458
1459                 public string GetAccessPath (SymValue sv)
1460                 {
1461                         Sequence<PathElementBase> bestAccessPath = GetBestAccessPath (sv, AccessPathFilter<Method>.NoFilter, true, true, false);
1462                         if (bestAccessPath == null)
1463                                 return null;
1464
1465                         return bestAccessPath.Select (i => (PathElement) i).ToCodeString ();
1466                 }
1467
1468                 public Sequence<PathElement> GetAccessPathList (SymValue symbol, AccessPathFilter<Method> filter, bool allowLocal, bool preferLocal)
1469                 {
1470                         return GetBestAccessPath (symbol, filter, true, allowLocal, preferLocal).Coerce<PathElementBase, PathElement> ();
1471                 }
1472
1473                 public bool LessEqual (Domain that, out IImmutableMap<SymValue, Sequence<SymValue>> forward, out IImmutableMap<SymValue, SymValue> backward)
1474                 {
1475                         return this.egraph.LessEqual (that.egraph, out forward, out backward);
1476                 }
1477
1478                 public bool IsResultEGraph (IMergeInfo mi)
1479                 {
1480                         return mi.IsResultGraph (this.egraph);
1481                 }
1482
1483                 public bool IsGraph1 (IMergeInfo mi)
1484                 {
1485                         return mi.IsGraph1 (this.egraph);
1486                 }
1487
1488                 public bool IsGraph2 (IMergeInfo mi)
1489                 {
1490                         return mi.IsGraph2 (this.egraph);
1491                 }
1492
1493                 public IImmutableMap<SymValue, Sequence<SymValue>> GetForwardIdentityMap ()
1494                 {
1495                         return this.egraph.GetForwardIdentityMap ();
1496                 }
1497
1498                 public Domain Join (Domain that, bool widening, out bool weaker, out IMergeInfo mergeInfo)
1499                 {
1500                         SymGraph<SymFunction, AbstractType> graph = this.egraph.Join (that.egraph, out mergeInfo, widening);
1501                         weaker = mergeInfo.Changed;
1502
1503                         IImmutableSet<SymValue> resultUnmodifiedSinceEntry;
1504                         IImmutableSet<SymValue> resultUnmodifiedFieldsSinceEntry;
1505                         IImmutableSet<SymValue> resultModifiedAtCall;
1506
1507                         ComputeJoinOfSets (mergeInfo, this, that, out resultUnmodifiedSinceEntry, out resultUnmodifiedFieldsSinceEntry, out resultModifiedAtCall, ref weaker);
1508                         Domain oldDomain = null;
1509                         if (OldDomain != null) {
1510                                 bool oldWeaker;
1511                                 IMergeInfo oldMergeInfo;
1512                                 oldDomain = OldDomain.Join (that.OldDomain, widening, out oldWeaker, out oldMergeInfo);
1513                         }
1514
1515                         return new Domain (graph, RecomputeConstantMap (graph), resultUnmodifiedSinceEntry, resultUnmodifiedFieldsSinceEntry, resultModifiedAtCall, this, oldDomain);
1516                 }
1517
1518                 private IImmutableMap<SymValue, SymFunction> RecomputeConstantMap (SymGraph<SymFunction, AbstractType> graph)
1519                 {
1520                         IImmutableMap<SymValue, SymFunction> result = ImmutableIntKeyMap<SymValue, SymFunction>.Empty (SymValue.GetUniqueKey);
1521                         foreach (SymFunction constant in graph.Constants) {
1522                                 if (this.Functions.IsConstantOrMethod (constant))
1523                                         result.Add (graph [constant], constant);
1524                         }
1525                         return result;
1526                 }
1527
1528                 private void ComputeJoinOfSets (IMergeInfo mergeInfo, Domain domain, Domain that,
1529                                                 out IImmutableSet<SymValue> resultUnmodifiedSinceEntry,
1530                                                 out IImmutableSet<SymValue> resultUnmodifiedFieldsSinceEntry,
1531                                                 out IImmutableSet<SymValue> resultModifiedAtCall, ref bool weaker)
1532                 {
1533                         resultUnmodifiedSinceEntry = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
1534                         resultUnmodifiedFieldsSinceEntry = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
1535                         resultModifiedAtCall = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
1536
1537                         foreach (var tuple in mergeInfo.MergeTriples) {
1538                                 SymValue symValue1 = tuple.Item1;
1539                                 SymValue symValue2 = tuple.Item2;
1540                                 SymValue elem = tuple.Item3;
1541
1542                                 bool unmodifiedSinceEntryContains = domain.unmodifiedSinceEntry.ContainsSafe (symValue1);
1543                                 bool modifiedAtCallContains = domain.ModifiedAtCall.ContainsSafe (symValue1);
1544
1545                                 if (unmodifiedSinceEntryContains) {
1546                                         if (that.unmodifiedSinceEntry.ContainsSafe (symValue2))
1547                                                 resultUnmodifiedSinceEntry = resultUnmodifiedSinceEntry.Add (elem);
1548                                         else if (that.unmodifiedFieldsSinceEntry.ContainsSafe (symValue2))
1549                                                 resultUnmodifiedFieldsSinceEntry = resultUnmodifiedFieldsSinceEntry.Add (elem);
1550                                 }
1551
1552                                 if (modifiedAtCallContains)
1553                                         resultModifiedAtCall = resultModifiedAtCall.Add (elem);
1554                         }
1555
1556                         if (that.unmodifiedSinceEntry.Count () > resultUnmodifiedSinceEntry.Count ()) {
1557                                 weaker = true;
1558                                 if (DebugOptions.Debug)
1559                                         Console.WriteLine ("---Result changed due to fewer unmodified locations since entry");
1560                         } else {
1561                                 if (that.unmodifiedFieldsSinceEntry.Count () > resultUnmodifiedFieldsSinceEntry.Count ()) {
1562                                         weaker = true;
1563                                         if (DebugOptions.Debug)
1564                                                 Console.WriteLine ("---Result changed due to fewer unmodified locations for fields since entry");
1565                                 }
1566                         }
1567                 }
1568
1569                 #region Implementation of IAbstractDomain<Domain>
1570                 public Domain Top
1571                 {
1572                         get
1573                         {
1574                                 return new Domain (this.egraph.Top, ImmutableIntKeyMap<SymValue, SymFunction>.Empty (SymValue.GetUniqueKey), ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey),
1575                                                    ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey), ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey), this, null);
1576                         }
1577                 }
1578
1579                 public Domain Bottom
1580                 {
1581                         get
1582                         {
1583                                 if (BottomValue == null) {
1584                                         BottomValue = new Domain (this.egraph.Bottom, ImmutableIntKeyMap<SymValue, SymFunction>.Empty (SymValue.GetUniqueKey), ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey),
1585                                                                   ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey), ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey),
1586                                                                   this, null);
1587                                         BottomValue.ImmutableVersion ();
1588                                 }
1589                                 return BottomValue;
1590                         }
1591                 }
1592
1593                 public bool IsTop
1594                 {
1595                         get { return this.egraph.IsTop; }
1596                 }
1597
1598                 public bool IsBottom
1599                 {
1600                         get
1601                         {
1602                                 if (this == BottomValue || this.egraph.IsBottom)
1603                                         return true;
1604                                 if (OldDomain != null)
1605                                         return OldDomain.IsBottom;
1606
1607                                 return false;
1608                         }
1609                 }
1610
1611             public Domain Join(Domain that)
1612             {
1613                 throw new NotImplementedException();
1614             }
1615
1616             public Domain Join (Domain that, bool widening, out bool weaker)
1617                 {
1618                         IMergeInfo mergeInfo;
1619                         return Join (that, widening, out weaker, out mergeInfo);
1620                 }
1621
1622             public Domain Widen(Domain that)
1623             {
1624                 throw new NotImplementedException();
1625             }
1626
1627             public Domain Meet (Domain that)
1628                 {
1629                         SymGraph<SymFunction, AbstractType> graph = this.egraph.Meet (that.egraph);
1630                         return new Domain (graph, RecomputeConstantMap (graph), this.unmodifiedSinceEntry, this.unmodifiedFieldsSinceEntry, null, this, OldDomain);
1631                 }
1632
1633                 public bool LessEqual (Domain that)
1634                 {
1635                         return this.egraph.LessEqual (that.egraph);
1636                 }
1637
1638                 public Domain ImmutableVersion ()
1639                 {
1640                         this.egraph.ImmutableVersion ();
1641                         return this;
1642                 }
1643                 #endregion
1644         }
1645 }