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 Domain(SymGraph<SymFunction, AbstractType> newEgraph, IImmutableMap<SymValue, SymFunction> constantMap, IImmutableSet<SymValue> unmodifiedSinceEntry, IImmutableSet<SymValue> unmodifiedFieldsSinceEntry, IImmutableSet<SymValue> modifiedAtCall, Domain from, Domain oldDomain)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 Domain(HeapAnalysis parent)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 Dump(TextWriter tw)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 Clone()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 IsRootedInParameter(Sequence<PathElement> path)157 public static bool IsRootedInParameter (Sequence<PathElement> path) 158 { 159 return path.Head is PathElement<Parameter>; 160 } 161 Address(Local local)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 Address(Parameter v)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 Address(SymFunction v)184 public SymValue Address (SymFunction v) 185 { 186 return this.egraph [v]; 187 } 188 Address(int v)189 public SymValue Address (int v) 190 { 191 return Address (this.Functions.For (v)); 192 } 193 AssignConst(int dest, TypeNode type, object constant)194 public void AssignConst (int dest, TypeNode type, object constant) 195 { 196 AssignConst (Address (this.Functions.For (dest)), type, constant); 197 } 198 AssignConst(SymValue address, TypeNode type, object constant)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 AssignValue(int dest, FlatDomain<TypeNode> type)210 public void AssignValue (int dest, FlatDomain<TypeNode> type) 211 { 212 AssignValue (Address (this.Functions.For (dest)), type); 213 } 214 AssignValue(SymValue address, FlatDomain<TypeNode> type)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 AssignNull(int addr)233 public void AssignNull (int addr) 234 { 235 AssignNull (Address (this.Functions.For (addr))); 236 } 237 AssignNull(SymValue addr)238 public void AssignNull (SymValue addr) 239 { 240 Havoc (addr); 241 this.egraph [this.Functions.ValueOf, addr] = Null; 242 } 243 AssignZero(SymValue addr)244 private void AssignZero (SymValue addr) 245 { 246 this.egraph [this.Functions.ValueOf, addr] = Zero; 247 } 248 AssignZeroEquivalent(SymValue addr, TypeNode t)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 AssignSpecialUnary(int dest, SymFunction op, int source, FlatDomain<TypeNode> typeOfValue)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 AssignSpecialUnary(int dest, SymValue result, FlatDomain<TypeNode> typeOfValue)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 AssignPureBinary(int dest, BinaryOperator op, FlatDomain<TypeNode> typeOpt, int op1, int op2)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 AssignPureUnary(int dest, UnaryOperator op, FlatDomain<TypeNode> typeOpt, int operand)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 ConstantValue(object constant, TypeNode type)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 Havoc(int i)309 public void Havoc (int i) 310 { 311 Havoc (Address (i)); 312 } 313 Havoc(SymValue addr)314 public void Havoc (SymValue addr) 315 { 316 this.egraph.EliminateAll (addr); 317 } 318 HavocIfStruct(SymValue address)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 HavocMutableFields(SymFunction except, SymValue address, ref IImmutableSet<SymValue> havoced)326 private void HavocMutableFields (SymFunction except, SymValue address, ref IImmutableSet<SymValue> havoced) 327 { 328 HavocFields (except, address, ref havoced, false); 329 } 330 HavocFields(SymFunction except, SymValue address, ref IImmutableSet<SymValue> havoced, bool havocImmutable)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 HavocConstructor(SymFunction except, SymValue address, SymFunction c, ref IImmutableSet<SymValue> havoced, bool havocImmutable)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 HavocPseudoFields(SymValue address)364 public void HavocPseudoFields (SymValue address) 365 { 366 IImmutableSet<SymValue> havoced = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey); 367 HavocPseudoFields (null, address, ref havoced); 368 } 369 HavocPseudoFields(SymFunction except, SymValue address, ref IImmutableSet<SymValue> havoced)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 HavocPseudoFields(SymFunction except, IEnumerable<Method> getters, SymValue address, ref IImmutableSet<SymValue> havoced)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 HavocPseudoFields(IEnumerable<Method> getters, SymValue address)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 MakeUnmodifiedField(SymValue address)408 private void MakeUnmodifiedField (SymValue address) 409 { 410 this.unmodifiedFieldsSinceEntry = this.unmodifiedFieldsSinceEntry.Add (address); 411 } 412 MakeModified(SymValue address)413 private void MakeModified (SymValue address) 414 { 415 this.unmodifiedSinceEntry = this.unmodifiedSinceEntry.Remove (address); 416 } 417 CopyValue(SymValue destAddr, SymValue sourceAddr)418 public void CopyValue (SymValue destAddr, SymValue sourceAddr) 419 { 420 AbstractType type = this.egraph [sourceAddr]; 421 CopyValue (destAddr, sourceAddr, type.Type); 422 } 423 CopyValue(SymValue destAddr, SymValue sourceAddr, FlatDomain<TypeNode> addrType)424 public void CopyValue (SymValue destAddr, SymValue sourceAddr, FlatDomain<TypeNode> addrType) 425 { 426 CopyValue (destAddr, sourceAddr, addrType, true, false); 427 } 428 CopyValue(SymValue destAddr, SymValue sourceAddr, FlatDomain<TypeNode> addrType, bool setTargetAddrType, bool cast)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 CopyOldValue(APC pc, int dest, int source, Domain target, bool atEndOld)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 CopyOldValue(APC pc, SymValue destAddr, SymValue srcAddr, Domain target, bool atEndOld)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 CopyOldValue(APC pc, SymValue destAddr, SymValue srcAddr, FlatDomain<TypeNode> addrType, Domain target, bool atEndOld)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 CopyOldValue(APC pc, SymValue destAddr, SymValue srcAddr, FlatDomain<TypeNode> addrType, bool setTargetAddrType, bool atEndOld, Domain target)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 CopyOldValueToDest(APC pc, SymValue destAddr, SymValue source, FlatDomain<TypeNode> addrType, Domain target)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 GetAccessPathsRaw(SymValue sv, AccessPathFilter<Method> filter, bool compress)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 GetAccessPathsRaw(SymValue sv, Sequence<PathElementBase> path, HashSet<SymValue> visited, AccessPathFilter<Method> filter, bool compress)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 GetBestAccessPath(SymValue sv, AccessPathFilter<Method> filter, bool compress, bool allowLocal, bool preferLocal)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 GetAccessPathsFiltered(SymValue sv, AccessPathFilter<Method> filter, bool compress)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 PathIsVisibleAccordingToFilter(Sequence<PathElementBase> path, AccessPathFilter<Method> filter)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 TryPropagateTypeInfo(Sequence<PathElementBase> path, out Sequence<PathElementBase> result)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 TryPropagateTypeInfoRecurse(Sequence<PathElementBase> path, TypeNode prevType, out Sequence<PathElementBase> result)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 GetAccessPathsTyped(SymValue sv, AccessPathFilter<Method> filter, bool compress)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 CopyNonStructWithFieldValue(SymValue destAddr, SymValue sv, FlatDomain<TypeNode> addrType)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 IsConstant(SymValue source, out TypeNode type, out object constant)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 CopyOldStructValue(APC pc, SymValue destAddr, SymValue srcAddr, TypeNode type, Domain target, bool atEndOld)691 private void CopyOldStructValue (APC pc, SymValue destAddr, SymValue srcAddr, TypeNode type, Domain target, bool atEndOld) 692 { 693 throw new NotImplementedException (); 694 } 695 SetValue(SymValue destAddr, SymValue sourceAddr, FlatDomain<TypeNode> addrType, bool cast)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 CopyPrimValue(SymValue destAddr, SymValue sourceAddr, bool cast, FlatDomain<TypeNode> elementType)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 CopyValueToOldState(APC pc, TypeNode type, int dest, int source, Domain target)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 CopyValueToOldState(APC pc, TypeNode addrType, SymValue destAddress, SymValue srcAddress, Domain target)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 CopyPrimitiveValueToOldState(APC pc, TypeNode addrType, SymValue destAddress, SymValue sv, Domain target)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 IsValidSymbol(SymValue sv)759 private bool IsValidSymbol (SymValue sv) 760 { 761 return this.egraph.IsValidSymbol (sv); 762 } 763 Assign(SymValue destAddress, TypeNode addrType)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 CopyStructValueToOldState(APC pc, SymValue destAddress, SymValue srcAddress, FlatDomain<TypeNode> targetType, Domain target)782 private void CopyStructValueToOldState (APC pc, SymValue destAddress, SymValue srcAddress, FlatDomain<TypeNode> targetType, Domain target) 783 { 784 throw new NotImplementedException (); 785 } 786 ManifestArrayLength(SymValue arrayValue)787 public void ManifestArrayLength (SymValue arrayValue) 788 { 789 SetType (this.egraph [this.Functions.Length, arrayValue], MetaDataProvider.System_Int32); 790 } 791 NeedsArrayLengthManifested(TypeNode type)792 public bool NeedsArrayLengthManifested (TypeNode type) 793 { 794 return MetaDataProvider.IsArray (type) || MetaDataProvider.System_String.Equals (type); 795 } 796 CopyStructValue(SymValue destAddr, SymValue sourceAddr, TypeNode type)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 OldValueAddress(Parameter p)810 public SymValue OldValueAddress (Parameter p) 811 { 812 return Address (OldValueParameterConstructor (p)); 813 } 814 OldValueParameterConstructor(Parameter argument)815 private SymFunction OldValueParameterConstructor (Parameter argument) 816 { 817 return this.Functions.For ("$OldParameter_" + MetaDataProvider.Name (argument)); 818 } 819 CopyParameterIntoShadow(Parameter p)820 public void CopyParameterIntoShadow (Parameter p) 821 { 822 CopyValue (Address (OldValueParameterConstructor (p)), Address (this.Functions.For (p))); 823 } 824 Copy(int dest, int source)825 public void Copy (int dest, int source) 826 { 827 CopyValue (Address (this.Functions.For (dest)), Address (this.Functions.For (source))); 828 } 829 IsIEnumerable(TypeNode type)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 GetSpecialUnary(SymFunction op, int source, FlatDomain<TypeNode> type)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 LookupAddressAndManifestType(SymValue[] args, SymFunction op, TypeNode type, out bool fresh)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 IsZero(SymValue symValue)858 public bool IsZero (SymValue symValue) 859 { 860 return this.egraph [symValue].IsZero; 861 } 862 Value(int v)863 public SymValue Value (int v) 864 { 865 return Value (Address (this.Functions.For (v))); 866 } 867 Value(SymValue address)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 Value(Parameter p)879 public SymValue Value (Parameter p) 880 { 881 return Value (Address (this.Functions.For (p))); 882 } 883 MakeUnmodified(SymValue value)884 public void MakeUnmodified (SymValue value) 885 { 886 this.unmodifiedSinceEntry = this.unmodifiedSinceEntry.Add (value); 887 } 888 IsUnmodified(SymValue value)889 private bool IsUnmodified (SymValue value) 890 { 891 return this.unmodifiedSinceEntry.Contains (value); 892 } 893 CurrentType(int stackPos)894 public AbstractType CurrentType (int stackPos) 895 { 896 return CurrentType (Value (Address (this.Functions.For (stackPos)))); 897 } 898 CurrentType(SymValue address)899 private AbstractType CurrentType (SymValue address) 900 { 901 return this.egraph [address]; 902 } 903 Assume(int t, bool truth)904 public Domain Assume (int t, bool truth) 905 { 906 return Assume (Value (t), truth); 907 } 908 Assume(SymValue sv, bool truth)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 IsNonZero(SymValue sv)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 BinaryResultType(BinaryOperator op, AbstractType t1, AbstractType t2)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 IsStructWithFields(FlatDomain<TypeNode> type)971 private bool IsStructWithFields (FlatDomain<TypeNode> type) 972 { 973 if (!type.IsNormal()) 974 return false; 975 976 return !MetaDataProvider.HasValueRepresentation (type.Value); 977 } 978 TargetType(FlatDomain<TypeNode> type)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 SetType(SymValue sv, FlatDomain<TypeNode> type)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 SetTypeIfUnknown(SymValue sv, FlatDomain<TypeNode> type)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 MakeTotallyModified(SymValue dest)1008 private void MakeTotallyModified (SymValue dest) 1009 { 1010 this.unmodifiedSinceEntry = this.unmodifiedSinceEntry.Remove (dest); 1011 this.unmodifiedFieldsSinceEntry = this.unmodifiedFieldsSinceEntry.Remove (dest); 1012 } 1013 AreUnmodified(IEnumerable<SymValue> values)1014 private bool AreUnmodified (IEnumerable<SymValue> values) 1015 { 1016 return values.All (IsUnmodified); 1017 } 1018 AnyAreModifiedAtCall(IEnumerable<SymValue> values)1019 private bool AnyAreModifiedAtCall (IEnumerable<SymValue> values) 1020 { 1021 return values.Any (IsModifiedAtCall); 1022 } 1023 IsModifiedAtCall(SymValue sv)1024 private bool IsModifiedAtCall (SymValue sv) 1025 { 1026 return (this.ModifiedAtCall != null && this.ModifiedAtCall.Contains (sv)); 1027 } 1028 GetStateAt(APC pc)1029 public Domain GetStateAt (APC pc) 1030 { 1031 Domain ifFound; 1032 this.parent.PreStateLookup (pc, out ifFound); 1033 1034 return ifFound; 1035 } 1036 TryGetCorrespondingValueAbstraction(int v, out SymbolicValue sv)1037 public bool TryGetCorrespondingValueAbstraction (int v, out SymbolicValue sv) 1038 { 1039 return TryGetCorrespondingValueAbstraction (this.Functions.For (v), out sv); 1040 } 1041 TryGetCorrespondingValueAbstraction(SymFunction v, out SymbolicValue sv)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 TryCorrespondingValue(SymValue address)1059 private SymValue TryCorrespondingValue (SymValue address) 1060 { 1061 if (IsStructAddress (this.egraph [address])) 1062 return address; 1063 1064 return TryValue (address); 1065 } 1066 IsStructAddress(AbstractType abstractType)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 TryAddress(SymFunction c)1079 private SymValue TryAddress (SymFunction c) 1080 { 1081 return this.egraph.TryLookup (c); 1082 } 1083 TryGetCorrespondingValueAbstraction(Local v, out SymbolicValue sv)1084 public bool TryGetCorrespondingValueAbstraction (Local v, out SymbolicValue sv) 1085 { 1086 return TryGetCorrespondingValueAbstraction (this.Functions.For (v), out sv); 1087 } 1088 TryGetUnboxedValue(int source, out SymbolicValue sv)1089 public bool TryGetUnboxedValue (int source, out SymbolicValue sv) 1090 { 1091 return TryGetUnboxedValue (TryValue (Address (source)), out sv); 1092 } 1093 TryGetUnboxedValue(SymValue box, out SymbolicValue sv)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 TryValue(SymValue address)1107 public SymValue TryValue (SymValue address) 1108 { 1109 return this.egraph.TryLookup (this.Functions.ValueOf, address); 1110 } 1111 GetType(SymValue symbol)1112 public AbstractType GetType (SymValue symbol) 1113 { 1114 return this.egraph [symbol]; 1115 } 1116 CreateObject(TypeNode type)1117 public SymValue CreateObject (TypeNode type) 1118 { 1119 SymValue sv = this.egraph.FreshSymbol (); 1120 SetType (sv, type); 1121 return sv; 1122 } 1123 CreateValue(TypeNode type)1124 public SymValue CreateValue (TypeNode type) 1125 { 1126 SymValue sv = this.egraph.FreshSymbol (); 1127 SetType (sv, MetaDataProvider.ManagedPointer (type)); 1128 return sv; 1129 } 1130 HavocArrayAtIndex(SymValue arrayValue, SymValue indexValue)1131 public void HavocArrayAtIndex (SymValue arrayValue, SymValue indexValue) 1132 { 1133 this.egraph.Eliminate (this.Functions.ElementAddress, arrayValue); 1134 } 1135 CreateArray(TypeNode type, SymValue len)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 ElementAddress(SymValue array, SymValue index, TypeNode elementAddressType)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 CopyValueAndCast(SymValue destAddr, SymValue srcAddr, TypeNode addrType)1156 public void CopyValueAndCast (SymValue destAddr, SymValue srcAddr, TypeNode addrType) 1157 { 1158 CopyValue (destAddr, srcAddr, addrType, true, true); 1159 } 1160 HavocObjectAtCall(SymValue obj, ref IImmutableSet<SymValue> havoced, bool havocFields, bool havocReadonlyFields)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 IsThis(Method currentMethod, int i)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 AssignValueAndNullnessAtConv_IU(int dest, int source, bool unsigned)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 AssignValueAndNullnessAtConv_IU(SymValue address, bool unsigned, AbstractType aType)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 UnaryResultType(UnaryOperator op, AbstractType type)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 CopyStackAddress(SymValue destAddr, int temporaryForWhichAddressIsTaken)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 PseudoFieldAddress(SymValue ptr, Method getter)1230 public SymValue PseudoFieldAddress (SymValue ptr, Method getter) 1231 { 1232 TypeNode pseudoFieldAddressType; 1233 return PseudoFieldAddress (ptr, getter, out pseudoFieldAddressType, false); 1234 } 1235 PseudoFieldAddress(SymValue sv, Method m, out TypeNode pseudoFieldAddressType, bool materialize)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 FieldAddress(SymValue ptr, Field field)1253 public SymValue FieldAddress (SymValue ptr, Field field) 1254 { 1255 TypeNode fieldAddressType; 1256 return FieldAddress (ptr, field, out fieldAddressType); 1257 } 1258 FieldAddress(SymValue ptr, Field field, out TypeNode fieldAddressType)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 Assign(Parameter parameter, TypeNode type)1273 public void Assign (Parameter parameter, TypeNode type) 1274 { 1275 AssignValue (Address (this.Functions.For (parameter)), type); 1276 } 1277 PseudoFieldAddressOfOutParameter(int index, SymValue fieldAddr, TypeNode pType)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 ObjectVersion(SymValue sv)1285 public SymValue ObjectVersion (SymValue sv) 1286 { 1287 return this.egraph [this.Functions.ObjectVersion, sv]; 1288 } 1289 PseudoFieldAddress(SymValue[] args, Method method, out TypeNode pseudoFieldAddressType, bool materialize)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 AssignReturnValue(int dest, TypeNode type)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 MaterializeAccordingToType(SymValue sv, TypeNode type, int depth)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 ManifestStructId(SymValue sv)1347 public void ManifestStructId (SymValue sv) 1348 { 1349 StructId (sv); 1350 } 1351 StructId(SymValue sv)1352 public SymValue StructId (SymValue sv) 1353 { 1354 return this.egraph [this.Functions.StructId, sv]; 1355 } 1356 LookupAddressAndManifestType(SymValue sv, SymFunction c, TypeNode type, out bool fresh)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 HavocFields(SymValue sv, IEnumerable<Field> fields, ref IImmutableSet<SymValue> havoced)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 IsUnmodifiedForFields(SymValue sv)1378 private bool IsUnmodifiedForFields (SymValue sv) 1379 { 1380 return this.unmodifiedFieldsSinceEntry.Contains (sv); 1381 } 1382 HavocUp(SymValue srcAddr, ref IImmutableSet<SymValue> havocedAtCall, bool havocFields)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 HavocUpField(SymValue sv, ref IImmutableSet<SymValue> havocedAtCall, bool havocFields)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 HavocUpObjectVersion(SymFunction accessedVia, SymValue sv, ref IImmutableSet<SymValue> havocedAtCall, bool havocFields)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 CopyAddress(SymValue destAddr, SymValue srcAddr, TypeNode type)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 AssignArrayLength(SymValue destAddr, SymValue array)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 ResetModifiedAtCall()1433 public void ResetModifiedAtCall () 1434 { 1435 this.ModifiedAtCall = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey); 1436 } 1437 LoadValue(int source)1438 public SymValue LoadValue (int source) 1439 { 1440 return Value (source); 1441 } 1442 TryLoadValue(SymValue addr)1443 public SymbolicValue TryLoadValue (SymValue addr) 1444 { 1445 return new SymbolicValue (Value (addr)); 1446 } 1447 TryGetArrayLength(SymValue arrayValue, out SymValue length)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 TryGetCorrespondingValueAbstraction(Parameter p, out SymbolicValue sv)1454 public bool TryGetCorrespondingValueAbstraction (Parameter p, out SymbolicValue sv) 1455 { 1456 return TryGetCorrespondingValueAbstraction (this.Functions.For (p), out sv); 1457 } 1458 GetAccessPath(SymValue sv)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 GetAccessPathList(SymValue symbol, AccessPathFilter<Method> filter, bool allowLocal, bool preferLocal)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 LessEqual(Domain that, out IImmutableMap<SymValue, Sequence<SymValue>> forward, out IImmutableMap<SymValue, SymValue> backward)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 IsResultEGraph(IMergeInfo mi)1478 public bool IsResultEGraph (IMergeInfo mi) 1479 { 1480 return mi.IsResultGraph (this.egraph); 1481 } 1482 IsGraph1(IMergeInfo mi)1483 public bool IsGraph1 (IMergeInfo mi) 1484 { 1485 return mi.IsGraph1 (this.egraph); 1486 } 1487 IsGraph2(IMergeInfo mi)1488 public bool IsGraph2 (IMergeInfo mi) 1489 { 1490 return mi.IsGraph2 (this.egraph); 1491 } 1492 GetForwardIdentityMap()1493 public IImmutableMap<SymValue, Sequence<SymValue>> GetForwardIdentityMap () 1494 { 1495 return this.egraph.GetForwardIdentityMap (); 1496 } 1497 Join(Domain that, bool widening, out bool weaker, out IMergeInfo mergeInfo)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 RecomputeConstantMap(SymGraph<SymFunction, AbstractType> graph)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 ComputeJoinOfSets(IMergeInfo mergeInfo, Domain domain, Domain that, out IImmutableSet<SymValue> resultUnmodifiedSinceEntry, out IImmutableSet<SymValue> resultUnmodifiedFieldsSinceEntry, out IImmutableSet<SymValue> resultModifiedAtCall, ref bool weaker)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 Join(Domain that)1611 public Domain Join(Domain that) 1612 { 1613 throw new NotImplementedException(); 1614 } 1615 Join(Domain that, bool widening, out bool weaker)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 Widen(Domain that)1622 public Domain Widen(Domain that) 1623 { 1624 throw new NotImplementedException(); 1625 } 1626 Meet(Domain that)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 LessEqual(Domain that)1633 public bool LessEqual (Domain that) 1634 { 1635 return this.egraph.LessEqual (that.egraph); 1636 } 1637 ImmutableVersion()1638 public Domain ImmutableVersion () 1639 { 1640 this.egraph.ImmutableVersion (); 1641 return this; 1642 } 1643 #endregion 1644 } 1645 } 1646