+//
+// Domain.cs
+//
+// Authors:
+// Alexander Chebaturkin (chebaturkin@gmail.com)
+//
+// Copyright (C) 2011 Alexander Chebaturkin
+//
+// Permission is hereby granted, free of charge, to any person obtaining
+// a copy of this software and associated documentation files (the
+// "Software"), to deal in the Software without restriction, including
+// without limitation the rights to use, copy, modify, merge, publish,
+// distribute, sublicense, and/or sell copies of the Software, and to
+// permit persons to whom the Software is furnished to do so, subject to
+// the following conditions:
+//
+// The above copyright notice and this permission notice shall be
+// included in all copies or substantial portions of the Software.
+//
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Linq;
+using Mono.CodeContracts.Static.AST;
+using Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths;
+using Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph;
+using Mono.CodeContracts.Static.ControlFlow;
+using Mono.CodeContracts.Static.DataStructures;
+using Mono.CodeContracts.Static.Lattices;
+using Mono.CodeContracts.Static.Providers;
+
+namespace Mono.CodeContracts.Static.Analysis.HeapAnalysis {
+ class Domain : IAbstractDomain<Domain> {
+ private static Domain BottomValue;
+ public readonly FunctionsTable Functions;
+ private readonly Dictionary<APC, Domain> begin_old_saved_states;
+ private readonly SymGraph<SymFunction, AbstractType> egraph;
+ private readonly HeapAnalysis parent;
+ private TypeCache IEnumerable1Type = new TypeCache (@"System.Collections.IEnumerable`1");
+ private TypeCache IEnumerableType = new TypeCache (@"System.Collections.IEnumerable");
+ public int InsideOld;
+ public IImmutableSet<SymValue> ModifiedAtCall;
+ private IImmutableMap<SymValue, SymFunction> constantLookup;
+ private IImmutableSet<SymValue> unmodifiedFieldsSinceEntry;
+ private IImmutableSet<SymValue> unmodifiedSinceEntry;
+
+ private Domain (SymGraph<SymFunction, AbstractType> newEgraph,
+ IImmutableMap<SymValue, SymFunction> constantMap,
+ IImmutableSet<SymValue> unmodifiedSinceEntry, IImmutableSet<SymValue> unmodifiedFieldsSinceEntry, IImmutableSet<SymValue> modifiedAtCall,
+ Domain from, Domain oldDomain)
+ {
+ this.egraph = newEgraph;
+ this.Functions = from.Functions;
+ this.parent = from.parent;
+ this.begin_old_saved_states = from.begin_old_saved_states;
+ this.constantLookup = constantMap;
+ this.unmodifiedSinceEntry = unmodifiedSinceEntry;
+ this.unmodifiedFieldsSinceEntry = unmodifiedFieldsSinceEntry;
+ this.ModifiedAtCall = modifiedAtCall;
+ this.InsideOld = from.InsideOld;
+ OldDomain = oldDomain;
+ BeginOldPC = from.BeginOldPC;
+ }
+
+ public Domain (HeapAnalysis parent)
+ {
+ this.parent = parent;
+ this.egraph = new SymGraph<SymFunction, AbstractType> (AbstractType.TopValue, AbstractType.BottomValue);
+ this.constantLookup = ImmutableIntKeyMap<SymValue, SymFunction>.Empty (SymValue.GetUniqueKey);
+ this.unmodifiedSinceEntry = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
+ this.unmodifiedFieldsSinceEntry = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
+ this.ModifiedAtCall = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
+ this.Functions = new FunctionsTable (parent.MetaDataProvider);
+ this.begin_old_saved_states = new Dictionary<APC, Domain> ();
+
+ SymValue nullValue = this.egraph.FreshSymbol ();
+ this.egraph [this.Functions.NullValue] = nullValue;
+ this.egraph [nullValue] = AbstractType.BottomValue;
+ this.egraph [ConstantValue (0, MetaDataProvider.System_Int32)] = new AbstractType (MetaDataProvider.System_Int32, true);
+ }
+
+ public Domain OldDomain { get; set; }
+ public APC BeginOldPC { get; set; }
+
+ public SymValue Globals
+ {
+ get { return this.egraph.ConstRoot; }
+ }
+
+ private SymValue Null
+ {
+ get { return this.egraph [this.Functions.NullValue]; }
+ }
+
+ private SymValue Zero
+ {
+ get { return this.egraph [this.Functions.ZeroValue]; }
+ }
+
+ public SymValue VoidAddr
+ {
+ get { return this.egraph [this.Functions.VoidAddr]; }
+ }
+
+ private IMetaDataProvider MetaDataProvider
+ {
+ get { return this.parent.MetaDataProvider; }
+ }
+
+ public IEnumerable<SymValue> Variables
+ {
+ get { return this.egraph.Variables; }
+ }
+
+ #region IAbstractDomain<Domain> Members
+ public void Dump (TextWriter tw)
+ {
+ this.egraph.Dump (tw);
+ tw.WriteLine ("Unmodified locations:");
+ foreach (SymValue sv in this.unmodifiedSinceEntry.Elements)
+ tw.Write ("{0} ", sv);
+ tw.WriteLine ();
+
+ tw.WriteLine ("Unmodified locations for fields:");
+ foreach (SymValue sv in this.unmodifiedFieldsSinceEntry.Elements)
+ tw.Write ("{0} ", sv);
+ tw.WriteLine ();
+
+ if (this.ModifiedAtCall != null) {
+ tw.WriteLine ("Modified locations at last call");
+ foreach (SymValue sv in this.ModifiedAtCall.Elements)
+ tw.Write ("{0} ", sv);
+ tw.WriteLine ();
+ }
+ if (OldDomain == null)
+ return;
+
+ tw.WriteLine ("## has old domain ##");
+ OldDomain.egraph.Dump (tw);
+ tw.WriteLine ("## end old domain ##");
+ }
+
+ public Domain Clone ()
+ {
+ return new Domain (this.egraph.Clone (), this.constantLookup, this.unmodifiedSinceEntry, this.unmodifiedFieldsSinceEntry, this.ModifiedAtCall, this, OldDomain == null ? null : OldDomain.Clone ());
+ }
+ #endregion
+
+ public static bool IsRootedInParameter (LispList<PathElement> path)
+ {
+ return path.Head is PathElement<Parameter>;
+ }
+
+ public SymValue Address (Local local)
+ {
+ SymFunction function = this.Functions.For (local);
+ SymValue sv = this.egraph.TryLookup (function);
+ if (sv == null) {
+ sv = this.egraph [function];
+ SetType (sv, MetaDataProvider.ManagedPointer (MetaDataProvider.LocalType (local)));
+ }
+ return sv;
+ }
+
+ public SymValue Address (Parameter v)
+ {
+ SymFunction function = this.Functions.For (v);
+ SymValue sv = this.egraph.TryLookup (function);
+ if (sv == null) {
+ sv = this.egraph [function];
+ SetType (sv, MetaDataProvider.ManagedPointer (MetaDataProvider.ParameterType (v)));
+ }
+ return sv;
+ }
+
+ public SymValue Address (SymFunction v)
+ {
+ return this.egraph [v];
+ }
+
+ public SymValue Address (int v)
+ {
+ return Address (this.Functions.For (v));
+ }
+
+ public void AssignConst (int dest, TypeNode type, object constant)
+ {
+ AssignConst (Address (this.Functions.For (dest)), type, constant);
+ }
+
+ public void AssignConst (SymValue address, TypeNode type, object constant)
+ {
+ SymValue value = ConstantValue (constant, type);
+ SetType (address, MetaDataProvider.ManagedPointer (type));
+ this.egraph [this.Functions.ValueOf, address] = value;
+
+ var str = constant as string;
+ if (str != null)
+ this.egraph [this.Functions.Length, value] = ConstantValue (str.Length, MetaDataProvider.System_Int32);
+ }
+
+ public void AssignValue (int dest, FlatDomain<TypeNode> type)
+ {
+ AssignValue (Address (this.Functions.For (dest)), type);
+ }
+
+ private void AssignValue (SymValue address, FlatDomain<TypeNode> type)
+ {
+ Havoc (address);
+ SetType (address, type.IsNormal ? MetaDataProvider.ManagedPointer (type.Concrete) : type);
+ if (IsStructWithFields (type))
+ return;
+
+ SymValue fresh = this.egraph.FreshSymbol ();
+ SetType (fresh, type);
+ this.egraph [this.Functions.ValueOf, address] = fresh;
+
+ if (!type.IsNormal)
+ return;
+
+ if (NeedsArrayLengthManifested (type.Concrete))
+ ManifestArrayLength (fresh);
+ }
+
+ public void AssignNull (int addr)
+ {
+ AssignNull (Address (this.Functions.For (addr)));
+ }
+
+ public void AssignNull (SymValue addr)
+ {
+ Havoc (addr);
+ this.egraph [this.Functions.ValueOf, addr] = Null;
+ }
+
+ private void AssignZero (SymValue addr)
+ {
+ this.egraph [this.Functions.ValueOf, addr] = Zero;
+ }
+
+ public void AssignZeroEquivalent (SymValue addr, TypeNode t)
+ {
+ if (MetaDataProvider.IsReferenceType (t))
+ AssignNull (addr);
+ else if (MetaDataProvider.HasValueRepresentation (t))
+ AssignZero (addr);
+ }
+
+ public void AssignSpecialUnary (int dest, SymFunction op, int source, FlatDomain<TypeNode> typeOfValue)
+ {
+ SymValue specialUnary = GetSpecialUnary (op, source, typeOfValue);
+ AssignSpecialUnary (dest, specialUnary, typeOfValue);
+ }
+
+ public void AssignSpecialUnary (int dest, SymValue result, FlatDomain<TypeNode> typeOfValue)
+ {
+ SymValue address = Address (dest);
+ AssignValue (address, typeOfValue);
+ this.egraph [this.Functions.ValueOf, address] = result;
+ }
+
+ public void AssignPureBinary (int dest, BinaryOperator op, FlatDomain<TypeNode> typeOpt, int op1, int op2)
+ {
+ var args = new[] {Value (op1), Value (op2)};
+ SymFunction c = this.Functions.For (op);
+ TypeNode type = !typeOpt.IsNormal ? MetaDataProvider.System_Int32 : typeOpt.Concrete;
+
+ bool fresh;
+
+ SymValue pointerValue = LookupAddressAndManifestType (args, c, type, out fresh);
+ SymValue destAddr = Address (dest);
+
+ SetType (destAddr, MetaDataProvider.ManagedPointer (type));
+ this.egraph [this.Functions.ValueOf, destAddr] = pointerValue;
+ }
+
+ public void AssignPureUnary (int dest, UnaryOperator op, FlatDomain<TypeNode> typeOpt, int operand)
+ {
+ SymFunction c = this.Functions.For (op);
+ TypeNode type = !typeOpt.IsNormal ? MetaDataProvider.System_Int32 : typeOpt.Concrete;
+
+ SymValue unaryOperand = this.egraph [c, Value (operand)];
+ SymValue sv = Address (dest);
+
+ SetType (sv, MetaDataProvider.ManagedPointer (type));
+ this.egraph [this.Functions.ValueOf, sv] = unaryOperand;
+ }
+
+ private SymValue ConstantValue (object constant, TypeNode type)
+ {
+ SymFunction symFunction = this.Functions.ForConstant (constant, type);
+ SymValue sv = this.egraph.TryLookup (symFunction);
+ if (sv == null) {
+ sv = this.egraph [symFunction];
+ SetType (sv, type);
+ this.constantLookup = this.constantLookup.Add (sv, symFunction);
+ }
+ return sv;
+ }
+
+ public void Havoc (int i)
+ {
+ Havoc (Address (i));
+ }
+
+ public void Havoc (SymValue addr)
+ {
+ this.egraph.EliminateAll (addr);
+ }
+
+ private void HavocIfStruct (SymValue address)
+ {
+ AbstractType aType = this.egraph [address];
+ if (aType.IsBottom || (aType.IsNormal && MetaDataProvider.IsStruct (aType.ConcreteType)))
+ Havoc (address);
+ }
+
+ private void HavocMutableFields (SymFunction except, SymValue address, ref IImmutableSet<SymValue> havoced)
+ {
+ HavocFields (except, address, ref havoced, false);
+ }
+
+ private void HavocFields (SymFunction except, SymValue address, ref IImmutableSet<SymValue> havoced, bool havocImmutable)
+ {
+ if (havoced.Contains (address))
+ return;
+
+ havoced = havoced.Add (address);
+ MakeTotallyModified (address);
+ foreach (SymFunction c in this.egraph.Functions (address))
+ HavocConstructor (except, address, c, ref havoced, havocImmutable);
+ }
+
+ private void HavocConstructor (SymFunction except, SymValue address, SymFunction c, ref IImmutableSet<SymValue> havoced, bool havocImmutable)
+ {
+ if (c == this.Functions.ValueOf)
+ this.egraph [this.Functions.OldValueOf, address] = this.egraph [c, address];
+ if (c == this.Functions.ValueOf || c == this.Functions.ObjectVersion || c == this.Functions.StructId) {
+ this.egraph.Eliminate (c, address);
+ havoced = havoced.Add (address);
+ } else {
+ var fieldWrapper = c as Wrapper<Field>;
+ if (fieldWrapper != null && fieldWrapper != except) {
+ if (havocImmutable || !MetaDataProvider.IsReadonly (fieldWrapper.Item))
+ HavocFields (except, this.egraph [c, address], ref havoced, havocImmutable);
+
+ return;
+ }
+
+ var methodWrapper = c as Wrapper<Method>;
+ if (methodWrapper != null && methodWrapper != except)
+ HavocFields (except, this.egraph [c, address], ref havoced, havocImmutable);
+ }
+ }
+
+ public void HavocPseudoFields (SymValue address)
+ {
+ IImmutableSet<SymValue> havoced = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
+ HavocPseudoFields (null, address, ref havoced);
+ }
+
+ private void HavocPseudoFields (SymFunction except, SymValue address, ref IImmutableSet<SymValue> havoced)
+ {
+ if (havoced.Contains (address))
+ return;
+ havoced = havoced.Add (address);
+ if (IsUnmodified (address)) {
+ MakeModified (address);
+ MakeUnmodifiedField (address);
+ }
+ this.egraph.Eliminate (this.Functions.ObjectVersion, address);
+ this.egraph.Eliminate (this.Functions.StructId, address);
+ foreach (SymFunction c in this.egraph.Functions (address)) {
+ if (c != except && c is Wrapper<Method>)
+ HavocMutableFields (except, this.egraph [c, address], ref havoced);
+ }
+ }
+
+ private void HavocPseudoFields (SymFunction except, IEnumerable<Method> getters, SymValue address, ref IImmutableSet<SymValue> havoced)
+ {
+ if (havoced.Contains (address))
+ return;
+ havoced = havoced.Add (address);
+ if (IsUnmodified (address)) {
+ MakeModified (address);
+ MakeUnmodifiedField (address);
+ }
+ this.egraph.Eliminate (this.Functions.ObjectVersion, address);
+ this.egraph.Eliminate (this.Functions.StructId, address);
+ foreach (Method m in getters)
+ HavocMutableFields (except, this.egraph [this.Functions.For (m), address], ref havoced);
+ }
+
+ public void HavocPseudoFields (IEnumerable<Method> getters, SymValue address)
+ {
+ IImmutableSet<SymValue> havoced = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
+ HavocPseudoFields (null, getters, address, ref havoced);
+ }
+
+ private void MakeUnmodifiedField (SymValue address)
+ {
+ this.unmodifiedFieldsSinceEntry = this.unmodifiedFieldsSinceEntry.Add (address);
+ }
+
+ private void MakeModified (SymValue address)
+ {
+ this.unmodifiedSinceEntry = this.unmodifiedSinceEntry.Remove (address);
+ }
+
+ public void CopyValue (SymValue destAddr, SymValue sourceAddr)
+ {
+ AbstractType type = this.egraph [sourceAddr];
+ CopyValue (destAddr, sourceAddr, type.Type);
+ }
+
+ public void CopyValue (SymValue destAddr, SymValue sourceAddr, FlatDomain<TypeNode> addrType)
+ {
+ CopyValue (destAddr, sourceAddr, addrType, true, false);
+ }
+
+ private void CopyValue (SymValue destAddr, SymValue sourceAddr, FlatDomain<TypeNode> addrType, bool setTargetAddrType, bool cast)
+ {
+ MakeTotallyModified (destAddr);
+ if (destAddr != sourceAddr)
+ HavocIfStruct (destAddr);
+ if (setTargetAddrType)
+ SetType (destAddr, addrType);
+
+ SetValue (destAddr, sourceAddr, addrType, cast);
+ }
+
+ public void CopyOldValue (APC pc, int dest, int source, Domain target, bool atEndOld)
+ {
+ CopyOldValue (pc, target.Address (dest), Address (source), target, atEndOld);
+ }
+
+ public void CopyOldValue (APC pc, SymValue destAddr, SymValue srcAddr, Domain target, bool atEndOld)
+ {
+ AbstractType abstractType = this.egraph [srcAddr];
+ CopyOldValue (pc, destAddr, srcAddr, abstractType.Type, target, atEndOld);
+ }
+
+ private void CopyOldValue (APC pc, SymValue destAddr, SymValue srcAddr, FlatDomain<TypeNode> addrType, Domain target, bool atEndOld)
+ {
+ CopyOldValue (pc, destAddr, srcAddr, addrType, true, atEndOld, target);
+ }
+
+ private void CopyOldValue (APC pc, SymValue destAddr, SymValue srcAddr, FlatDomain<TypeNode> addrType, bool setTargetAddrType, bool atEndOld, Domain target)
+ {
+ target.MakeTotallyModified (destAddr);
+ if (destAddr != srcAddr)
+ target.HavocIfStruct (destAddr);
+ if (setTargetAddrType)
+ target.SetType (destAddr, addrType);
+
+ FlatDomain<TypeNode> targetType = TargetType (addrType);
+
+ if (IsStructWithFields (targetType))
+ CopyOldStructValue (pc, destAddr, srcAddr, targetType.Concrete, target, atEndOld);
+ else if (atEndOld && targetType.IsNormal && MetaDataProvider.IsManagedPointer (targetType.Concrete)) {
+ srcAddr = TryValue (srcAddr);
+ if (srcAddr == null)
+ return;
+ destAddr = target.Value (destAddr);
+ CopyOldValue (pc, destAddr, srcAddr, targetType, setTargetAddrType, atEndOld, target);
+ } else {
+ SymValue source = this.egraph.TryLookup (this.Functions.ValueOf, srcAddr);
+ if (source == null) {
+ if (this.egraph.IsImmutable)
+ return;
+ source = this.egraph [this.Functions.ValueOf, srcAddr];
+ }
+ CopyOldValueToDest (pc, destAddr, source, addrType, target);
+ }
+ }
+
+ public void CopyOldValueToDest (APC pc, SymValue destAddr, SymValue source, FlatDomain<TypeNode> addrType, Domain target)
+ {
+ if (pc.InsideEnsuresAtCall) {
+ TypeNode type;
+ object constant;
+
+ if (IsConstant (source, out type, out constant)) {
+ SymValue sv = target.ConstantValue (constant, type);
+ target.CopyNonStructWithFieldValue (destAddr, sv, addrType);
+ return;
+ }
+
+ foreach (var sv in GetAccessPathsRaw (source, AccessPathFilter<Method>.NoFilter, false))
+ throw new NotImplementedException ();
+ }
+ }
+
+ private IEnumerable<LispList<PathElementBase>> GetAccessPathsRaw (SymValue sv, AccessPathFilter<Method> filter, bool compress)
+ {
+ var visited = new HashSet<SymValue> ();
+ return GetAccessPathsRaw (sv, null, visited, filter, compress);
+ }
+
+ private IEnumerable<LispList<PathElementBase>> GetAccessPathsRaw (SymValue sv, LispList<PathElementBase> path, HashSet<SymValue> visited, AccessPathFilter<Method> filter, bool compress)
+ {
+ if (sv == this.egraph.ConstRoot)
+ yield return path;
+ else if (!visited.Contains (sv)) {
+ visited.Add (sv);
+ foreach (var term in this.egraph.EqTerms (sv)) {
+ if (!(term.Function is Wrapper<object>) && !(term.Function is Wrapper<int>)) {
+ PathElementBase next = term.Function.ToPathElement (compress);
+ if (next != null && !filter.FilterOutPathElement (term.Function)) {
+ LispList<PathElementBase> newPath;
+
+ if (path == null || !compress || (!(next is PathElement<Method>)))
+ newPath = path.Cons (next);
+ else
+ newPath = path.Tail.Cons (next);
+
+ foreach (var item in GetAccessPathsRaw (term.Args [0], newPath, visited, filter, compress))
+ yield return item;
+ }
+ }
+ }
+ }
+ }
+
+ private LispList<PathElementBase> GetBestAccessPath (SymValue sv, AccessPathFilter<Method> filter, bool compress, bool allowLocal, bool preferLocal)
+ {
+ LispList<PathElementBase> bestParameterPath = null;
+ LispList<PathElementBase> bestLocalPath = null;
+ LispList<PathElementBase> bestFieldMethodPath = null;
+
+ foreach (var path in GetAccessPathsFiltered (sv, filter, compress)) {
+ if (path != null) {
+ if (path.Head is PathElement<Parameter>) {
+ if (bestParameterPath == null || bestParameterPath.Length () > path.Length ())
+ bestParameterPath = path;
+ } else if (filter.AllowLocal && allowLocal && path.Head is PathElement<Local>) {
+ if (!path.Head.ToString ().Contains ("$") && (bestLocalPath == null || bestLocalPath.Length () > path.Length ()))
+ bestLocalPath = path;
+ } else if (path.Head is PathElement<Field> && path.Head.Func.IsStatic) {
+ if (bestFieldMethodPath == null || bestFieldMethodPath.Length () > path.Length ())
+ bestFieldMethodPath = path;
+ } else if (path.Head is PathElement<Method> && path.Head.Func.IsStatic) {
+ if (bestFieldMethodPath == null || bestFieldMethodPath.Length () > path.Length ())
+ bestFieldMethodPath = path;
+ }
+ }
+ }
+ if (preferLocal && bestLocalPath != null)
+ return bestLocalPath;
+ if (bestParameterPath != null)
+ return bestParameterPath;
+ if (allowLocal && bestLocalPath != null)
+ return bestLocalPath;
+
+ return bestFieldMethodPath;
+ }
+
+ public IEnumerable<LispList<PathElementBase>> GetAccessPathsFiltered (SymValue sv, AccessPathFilter<Method> filter, bool compress)
+ {
+ return GetAccessPathsTyped (sv, filter, compress).Where (path => PathIsVisibleAccordingToFilter (path, filter));
+ }
+
+ private bool PathIsVisibleAccordingToFilter (LispList<PathElementBase> path, AccessPathFilter<Method> filter)
+ {
+ if (path.Length () == 0 || !filter.HasVisibilityMember)
+ return true;
+
+ Method visibilityMember = filter.VisibilityMember;
+ TypeNode t = MetaDataProvider.DeclaringType (visibilityMember);
+ TypeNode type = default(TypeNode);
+
+ while (path != null) {
+ PathElement pathElement = path.Head;
+ if (!pathElement.TryGetResultType (out type))
+ return true;
+ while (MetaDataProvider.IsManagedPointer (type))
+ type = MetaDataProvider.ElementType (type);
+ if ("this" != pathElement.ToString ()) {
+ var peMethod = pathElement as PathElement<Method>;
+ if (peMethod != null) {
+ Method method = peMethod.Element;
+ if (!MetaDataProvider.IsVisibleFrom (method, t))
+ return false;
+ }
+
+ var peProperty = pathElement as PathElement<Property>;
+ if (peProperty != null) {
+ Property property = peProperty.Element;
+ Method method;
+ if (!MetaDataProvider.HasGetter (property, out method))
+ MetaDataProvider.HasSetter (property, out method);
+
+ if (!MetaDataProvider.IsVisibleFrom (method, t))
+ return false;
+ }
+
+ var peField = pathElement as PathElement<Field>;
+ if (peField != null) {
+ Field field = peField.Element;
+ if (!MetaDataProvider.IsVisibleFrom (field, t))
+ return false;
+ }
+ }
+ path = path.Tail;
+ }
+ return true;
+ }
+
+ private bool TryPropagateTypeInfo (LispList<PathElementBase> path, out LispList<PathElementBase> result)
+ {
+ if (path == null) {
+ result = null;
+ return true;
+ }
+ PathElementBase head = path.Head;
+ TypeNode prevType;
+ if (!head.TrySetType (MetaDataProvider.System_IntPtr, MetaDataProvider, out prevType)) {
+ result = null;
+ return false;
+ }
+
+ LispList<PathElementBase> result1;
+ if (!TryPropagateTypeInfoRecurse (path.Tail, prevType, out result1)) {
+ result = null;
+ return false;
+ }
+ if (head.IsAddressOf && head is PathElement<Parameter> && result1 != null && result1.Head.IsDeref) {
+ var pathElement = (PathElement<Parameter>) head;
+ result = result1.Tail.Cons (new ParameterPathElement (pathElement.Element, pathElement.Description, pathElement.Func, MetaDataProvider));
+ return true;
+ }
+
+ result = result1.Cons (head);
+ return true;
+ }
+
+ private bool TryPropagateTypeInfoRecurse (LispList<PathElementBase> path, TypeNode prevType, out LispList<PathElementBase> result)
+ {
+ if (path == null) {
+ result = null;
+ return true;
+ }
+ PathElementBase head = path.Head;
+ if (head.TrySetType (prevType, MetaDataProvider, out prevType)) {
+ LispList<PathElementBase> updatedPath;
+ if (TryPropagateTypeInfoRecurse (path.Tail, prevType, out updatedPath)) {
+ result = updatedPath.Cons (head);
+ return true;
+ }
+ }
+
+ result = null;
+ return false;
+ }
+
+ private IEnumerable<LispList<PathElementBase>> GetAccessPathsTyped (SymValue sv, AccessPathFilter<Method> filter, bool compress)
+ {
+ var visited = new HashSet<SymValue> ();
+ foreach (var path in GetAccessPathsRaw (sv, null, visited, filter, compress)) {
+ LispList<PathElementBase> result;
+ if (TryPropagateTypeInfo (path, out result))
+ yield return result;
+ }
+ }
+
+ private void CopyNonStructWithFieldValue (SymValue destAddr, SymValue sv, FlatDomain<TypeNode> addrType)
+ {
+ this.egraph [this.Functions.ValueOf, destAddr] = sv;
+ SetType (destAddr, addrType);
+ }
+
+ public bool IsConstant (SymValue source, out TypeNode type, out object constant)
+ {
+ SymFunction c = this.constantLookup [source];
+ if (c != null)
+ return this.Functions.IsConstant (c, out type, out constant);
+
+ type = default(TypeNode);
+ constant = null;
+ return false;
+ }
+
+ private void CopyOldStructValue (APC pc, SymValue destAddr, SymValue srcAddr, TypeNode type, Domain target, bool atEndOld)
+ {
+ throw new NotImplementedException ();
+ }
+
+ public void SetValue (SymValue destAddr, SymValue sourceAddr, FlatDomain<TypeNode> addrType, bool cast)
+ {
+ FlatDomain<TypeNode> type = TargetType (addrType);
+ if (IsStructWithFields (type))
+ CopyStructValue (destAddr, sourceAddr, type.Concrete);
+
+ CopyPrimValue (destAddr, sourceAddr, cast, type);
+ }
+
+ private void CopyPrimValue (SymValue destAddr, SymValue sourceAddr, bool cast, FlatDomain<TypeNode> elementType)
+ {
+ SymValue value = this.egraph [this.Functions.ValueOf, sourceAddr];
+ if (cast)
+ SetType (value, elementType);
+ else
+ SetTypeIfUnknown (value, elementType);
+
+ if (elementType.IsNormal) {
+ if (NeedsArrayLengthManifested (elementType.Concrete))
+ ManifestArrayLength (value);
+ }
+
+ this.egraph [this.Functions.ValueOf, destAddr] = value;
+ }
+
+ public void CopyValueToOldState (APC pc, TypeNode type, int dest, int source, Domain target)
+ {
+ SymValue destAddress = target.Address (dest);
+ SymValue srcAddress = Address (source);
+
+ AbstractType aType = GetType (srcAddress);
+ TypeNode addrType = aType.IsNormal ? aType.ConcreteType : MetaDataProvider.ManagedPointer (type);
+ CopyValueToOldState (pc, addrType, destAddress, srcAddress, target);
+ }
+
+ private void CopyValueToOldState (APC pc, TypeNode addrType, SymValue destAddress, SymValue srcAddress, Domain target)
+ {
+ target.MakeTotallyModified (destAddress);
+ if (destAddress != srcAddress)
+ target.HavocIfStruct (destAddress);
+ target.SetType (destAddress, addrType);
+ FlatDomain<TypeNode> targetType = TargetType (addrType);
+ if (IsStructWithFields (targetType))
+ CopyStructValueToOldState (pc, destAddress, srcAddress, targetType, target);
+ else {
+ SymValue sv = this.egraph.TryLookup (this.Functions.ValueOf, srcAddress);
+ if (sv == null) {
+ if (this.egraph.IsImmutable)
+ return;
+ sv = this.egraph [this.Functions.ValueOf, srcAddress];
+ }
+ CopyPrimitiveValueToOldState (pc, addrType, destAddress, sv, target);
+ }
+ }
+
+ private void CopyPrimitiveValueToOldState (APC pc, TypeNode addrType, SymValue destAddress, SymValue sv, Domain target)
+ {
+ if (target.IsValidSymbol (sv))
+ target.CopyNonStructWithFieldValue (destAddress, sv, addrType);
+ else
+ target.Assign (destAddress, addrType);
+ }
+
+ private bool IsValidSymbol (SymValue sv)
+ {
+ return this.egraph.IsValidSymbol (sv);
+ }
+
+ private void Assign (SymValue destAddress, TypeNode addrType)
+ {
+ Havoc (destAddress);
+ SetType (destAddress, addrType);
+ FlatDomain<TypeNode> targetType = TargetType (addrType);
+ if (IsStructWithFields (targetType))
+ return;
+
+ SymValue fresh = this.egraph.FreshSymbol ();
+ SetType (fresh, targetType);
+ this.egraph [this.Functions.ValueOf, destAddress] = fresh;
+ if (!targetType.IsNormal)
+ return;
+
+ if (NeedsArrayLengthManifested (targetType.Concrete))
+ ManifestArrayLength (fresh);
+ }
+
+ private void CopyStructValueToOldState (APC pc, SymValue destAddress, SymValue srcAddress, FlatDomain<TypeNode> targetType, Domain target)
+ {
+ throw new NotImplementedException ();
+ }
+
+ public void ManifestArrayLength (SymValue arrayValue)
+ {
+ SetType (this.egraph [this.Functions.Length, arrayValue], MetaDataProvider.System_Int32);
+ }
+
+ public bool NeedsArrayLengthManifested (TypeNode type)
+ {
+ return MetaDataProvider.IsArray (type) || MetaDataProvider.System_String.Equals (type);
+ }
+
+ public void CopyStructValue (SymValue destAddr, SymValue sourceAddr, TypeNode type)
+ {
+ if (destAddr == null)
+ return;
+ this.egraph [this.Functions.StructId, destAddr] = this.egraph [this.Functions.StructId, sourceAddr];
+ foreach (SymFunction function in this.egraph.Functions (sourceAddr)) {
+ if (function.ActsAsField) {
+ TypeNode functionType = function.FieldAddressType ();
+ CopyValue (this.egraph [function, destAddr], this.egraph [function, sourceAddr], functionType);
+ }
+ }
+ }
+
+ public SymValue OldValueAddress (Parameter p)
+ {
+ return Address (OldValueParameterConstructor (p));
+ }
+
+ private SymFunction OldValueParameterConstructor (Parameter argument)
+ {
+ return this.Functions.For ("$OldParameter_" + MetaDataProvider.Name (argument));
+ }
+
+ public void CopyParameterIntoShadow (Parameter p)
+ {
+ CopyValue (Address (OldValueParameterConstructor (p)), Address (this.Functions.For (p)));
+ }
+
+ public void Copy (int dest, int source)
+ {
+ CopyValue (Address (this.Functions.For (dest)), Address (this.Functions.For (source)));
+ }
+
+ private bool IsIEnumerable (TypeNode type)
+ {
+ TypeNode ienumerableType;
+ return (this.IEnumerable1Type.TryGet (MetaDataProvider, out ienumerableType) && MetaDataProvider.DerivesFrom (type, ienumerableType)
+ || this.IEnumerableType.TryGet (MetaDataProvider, out ienumerableType) && MetaDataProvider.DerivesFrom (type, ienumerableType));
+ }
+
+ public SymValue GetSpecialUnary (SymFunction op, int source, FlatDomain<TypeNode> type)
+ {
+ SymValue value = Value (source);
+ SymValue sv = this.egraph [op, value];
+ SetType (sv, type);
+ return sv;
+ }
+
+ private SymValue LookupAddressAndManifestType (SymValue[] args, SymFunction op, TypeNode type, out bool fresh)
+ {
+ SymValue sv = this.egraph.TryLookup (op, args);
+ if (sv != null) {
+ fresh = false;
+ return sv;
+ }
+ fresh = true;
+ sv = this.egraph [op, args];
+ SetType (sv, type);
+ return sv;
+ }
+
+ public bool IsZero (SymValue symValue)
+ {
+ return this.egraph [symValue].IsZero;
+ }
+
+ public SymValue Value (int v)
+ {
+ return Value (Address (this.Functions.For (v)));
+ }
+
+ public SymValue Value (SymValue address)
+ {
+ bool fresh;
+ SymValue symbol = this.egraph.LookupOrManifest (this.Functions.ValueOf, address, out fresh);
+
+ if (fresh && IsUnmodified (address))
+ MakeUnmodified (symbol);
+
+ return symbol;
+ }
+
+ public SymValue Value (Parameter p)
+ {
+ return Value (Address (this.Functions.For (p)));
+ }
+
+ public void MakeUnmodified (SymValue value)
+ {
+ this.unmodifiedSinceEntry = this.unmodifiedSinceEntry.Add (value);
+ }
+
+ private bool IsUnmodified (SymValue value)
+ {
+ return this.unmodifiedSinceEntry.Contains (value);
+ }
+
+ public AbstractType CurrentType (int stackPos)
+ {
+ return CurrentType (Value (Address (this.Functions.For (stackPos))));
+ }
+
+ private AbstractType CurrentType (SymValue address)
+ {
+ return this.egraph [address];
+ }
+
+ public Domain Assume (int t, bool truth)
+ {
+ return Assume (Value (t), truth);
+ }
+
+ private Domain Assume (SymValue sv, bool truth)
+ {
+ if (!truth) {
+ if (IsNonZero (sv))
+ return Bottom;
+ this.egraph [sv] = this.egraph [sv].ButZero;
+ foreach (var term in this.egraph.EqTerms (sv)) {
+ if (term.Function == this.Functions.UnaryNot || term.Function == this.Functions.NeZero)
+ return Assume (term.Args [0], true);
+ }
+ } else {
+ if (this.egraph [sv].IsZero)
+ return Bottom;
+ foreach (var term in this.egraph.EqTerms (sv)) {
+ if (term.Function == this.Functions.UnaryNot || term.Function == this.Functions.NeZero)
+ return Assume (term.Args [0], false);
+ }
+ }
+
+ return this;
+ }
+
+ private bool IsNonZero (SymValue sv)
+ {
+ foreach (var term in this.egraph.EqTerms (sv)) {
+ var wrapper = term.Function as Wrapper<object>;
+ if (wrapper != null && wrapper.Item is int && (int) wrapper.Item != 0)
+ return true;
+ }
+ return false;
+ }
+
+ public FlatDomain<TypeNode> BinaryResultType (BinaryOperator op, AbstractType t1, AbstractType t2)
+ {
+ switch (op) {
+ case BinaryOperator.Add:
+ case BinaryOperator.Add_Ovf:
+ case BinaryOperator.Add_Ovf_Un:
+ if (t1.IsZero)
+ return t2.Type;
+ return t1.Type;
+ case BinaryOperator.Sub:
+ case BinaryOperator.Sub_Ovf:
+ case BinaryOperator.Sub_Ovf_Un:
+ return t1.Type;
+ case BinaryOperator.Ceq:
+ case BinaryOperator.Cobjeq:
+ case BinaryOperator.Cne_Un:
+ case BinaryOperator.Cge:
+ case BinaryOperator.Cge_Un:
+ case BinaryOperator.Cgt:
+ case BinaryOperator.Cgt_Un:
+ case BinaryOperator.Cle:
+ case BinaryOperator.Cle_Un:
+ case BinaryOperator.Clt:
+ case BinaryOperator.Clt_Un:
+ return MetaDataProvider.System_Boolean;
+ default:
+ return t1.Type;
+ }
+ }
+
+ private bool IsStructWithFields (FlatDomain<TypeNode> type)
+ {
+ if (!type.IsNormal)
+ return false;
+
+ return !MetaDataProvider.HasValueRepresentation (type.Concrete);
+ }
+
+ private FlatDomain<TypeNode> TargetType (FlatDomain<TypeNode> type)
+ {
+ if (!type.IsNormal)
+ return type;
+
+ TypeNode normalType = type.Concrete;
+ if (MetaDataProvider.IsManagedPointer (normalType))
+ return MetaDataProvider.ElementType (normalType);
+
+ return FlatDomain<TypeNode>.TopValue;
+ }
+
+ public void SetType (SymValue sv, FlatDomain<TypeNode> type)
+ {
+ AbstractType abstractType = this.egraph [sv];
+ if (abstractType.IsZero)
+ return;
+
+ this.egraph [sv] = abstractType.With (type);
+ }
+
+ private void SetTypeIfUnknown (SymValue sv, FlatDomain<TypeNode> type)
+ {
+ AbstractType abstractType = this.egraph [sv];
+
+ if (!abstractType.IsZero && (!abstractType.Type.IsNormal || abstractType.Type.Equals (MetaDataProvider.System_IntPtr)))
+ this.egraph [sv] = abstractType.With (type);
+ }
+
+ private void MakeTotallyModified (SymValue dest)
+ {
+ this.unmodifiedSinceEntry = this.unmodifiedSinceEntry.Remove (dest);
+ this.unmodifiedFieldsSinceEntry = this.unmodifiedFieldsSinceEntry.Remove (dest);
+ }
+
+ private bool AreUnmodified (IEnumerable<SymValue> values)
+ {
+ return values.All (IsUnmodified);
+ }
+
+ private bool AnyAreModifiedAtCall (IEnumerable<SymValue> values)
+ {
+ return values.Any (IsModifiedAtCall);
+ }
+
+ private bool IsModifiedAtCall (SymValue sv)
+ {
+ return (this.ModifiedAtCall != null && this.ModifiedAtCall.Contains (sv));
+ }
+
+ public Domain GetStateAt (APC pc)
+ {
+ Domain ifFound;
+ this.parent.PreStateLookup (pc, out ifFound);
+
+ return ifFound;
+ }
+
+ public bool TryGetCorrespondingValueAbstraction (int v, out SymbolicValue sv)
+ {
+ return TryGetCorrespondingValueAbstraction (this.Functions.For (v), out sv);
+ }
+
+ private bool TryGetCorrespondingValueAbstraction (SymFunction v, out SymbolicValue sv)
+ {
+ if (!IsBottom) {
+ SymValue loc = TryAddress (v);
+ if (loc != null) {
+ SymValue symbol = TryCorrespondingValue (loc);
+ if (symbol != null) {
+ sv = new SymbolicValue (symbol);
+ return true;
+ }
+ }
+ }
+
+ sv = default(SymbolicValue);
+ return false;
+ }
+
+ private SymValue TryCorrespondingValue (SymValue address)
+ {
+ if (IsStructAddress (this.egraph [address]))
+ return address;
+
+ return TryValue (address);
+ }
+
+ private bool IsStructAddress (AbstractType abstractType)
+ {
+ if (!abstractType.IsNormal)
+ return false;
+
+ TypeNode normalType = abstractType.ConcreteType;
+ if (MetaDataProvider.IsManagedPointer (normalType))
+ return !MetaDataProvider.HasValueRepresentation (MetaDataProvider.ElementType (normalType));
+
+ return false;
+ }
+
+ private SymValue TryAddress (SymFunction c)
+ {
+ return this.egraph.TryLookup (c);
+ }
+
+ public bool TryGetCorrespondingValueAbstraction (Local v, out SymbolicValue sv)
+ {
+ return TryGetCorrespondingValueAbstraction (this.Functions.For (v), out sv);
+ }
+
+ public bool TryGetUnboxedValue (int source, out SymbolicValue sv)
+ {
+ return TryGetUnboxedValue (TryValue (Address (source)), out sv);
+ }
+
+ private bool TryGetUnboxedValue (SymValue box, out SymbolicValue sv)
+ {
+ if (box != null) {
+ SymValue symbol = TryValue (box);
+ if (symbol != null && this.egraph.TryLookup (this.Functions.BoxOperator, symbol) == box) {
+ sv = new SymbolicValue (symbol);
+ return true;
+ }
+ }
+ sv = new SymbolicValue ();
+ return false;
+ }
+
+ public SymValue TryValue (SymValue address)
+ {
+ return this.egraph.TryLookup (this.Functions.ValueOf, address);
+ }
+
+ public AbstractType GetType (SymValue symbol)
+ {
+ return this.egraph [symbol];
+ }
+
+ public SymValue CreateObject (TypeNode type)
+ {
+ SymValue sv = this.egraph.FreshSymbol ();
+ SetType (sv, type);
+ return sv;
+ }
+
+ public SymValue CreateValue (TypeNode type)
+ {
+ SymValue sv = this.egraph.FreshSymbol ();
+ SetType (sv, MetaDataProvider.ManagedPointer (type));
+ return sv;
+ }
+
+ public void HavocArrayAtIndex (SymValue arrayValue, SymValue indexValue)
+ {
+ this.egraph.Eliminate (this.Functions.ElementAddress, arrayValue);
+ }
+
+ public SymValue CreateArray (TypeNode type, SymValue len)
+ {
+ SymValue sv = this.egraph.FreshSymbol ();
+ this.egraph [this.Functions.Length, sv] = len;
+ SetType (sv, MetaDataProvider.ArrayType (type, 1));
+ return sv;
+ }
+
+ public SymValue ElementAddress (SymValue array, SymValue index, TypeNode elementAddressType)
+ {
+ SymValue objVersion = this.egraph [this.Functions.ObjectVersion, array];
+ SymValue sv = this.egraph.TryLookup (this.Functions.ElementAddress, objVersion, index);
+ if (sv == null) {
+ sv = this.egraph [this.Functions.ElementAddress, objVersion, index];
+ SetType (sv, elementAddressType);
+ this.egraph [this.Functions.ResultOfLoadElement, sv] = Zero;
+ }
+ return sv;
+ }
+
+ public void CopyValueAndCast (SymValue destAddr, SymValue srcAddr, TypeNode addrType)
+ {
+ CopyValue (destAddr, srcAddr, addrType, true, true);
+ }
+
+ public void HavocObjectAtCall (SymValue obj, ref IImmutableSet<SymValue> havoced, bool havocFields, bool havocReadonlyFields)
+ {
+ HavocFields (null, obj, ref havoced, havocReadonlyFields);
+ HavocUp (obj, ref havoced, havocFields);
+ }
+
+ public bool IsThis (Method currentMethod, int i)
+ {
+ if (MetaDataProvider.IsStatic (currentMethod))
+ return false;
+ return Value (MetaDataProvider.This (currentMethod)) == Value (i);
+ }
+
+ public void AssignValueAndNullnessAtConv_IU (int dest, int source, bool unsigned)
+ {
+ AbstractType aType = CurrentType (source);
+ AssignValueAndNullnessAtConv_IU (Address (this.Functions.For (dest)), unsigned, aType);
+ }
+
+ private void AssignValueAndNullnessAtConv_IU (SymValue address, bool unsigned, AbstractType aType)
+ {
+ Havoc (address);
+ FlatDomain<TypeNode> type = aType.Type;
+ if (!IsStructWithFields (type)) {
+ SymValue ptrValue = this.egraph.FreshSymbol ();
+ if (type.IsNormal)
+ aType = new AbstractType (!unsigned ? MetaDataProvider.System_IntPtr : MetaDataProvider.System_UIntPtr, aType.IsZero);
+ SetType (address, type.IsNormal ? MetaDataProvider.ManagedPointer (type.Concrete) : type);
+ this.egraph [ptrValue] = aType;
+ this.egraph [this.Functions.ValueOf, address] = ptrValue;
+ } else
+ SetType (address, type.IsNormal ? MetaDataProvider.ManagedPointer (type.Concrete) : type);
+ }
+
+ public TypeNode UnaryResultType (UnaryOperator op, AbstractType type)
+ {
+ switch (op) {
+ case UnaryOperator.Conv_i1:
+ return MetaDataProvider.System_Int8;
+ case UnaryOperator.Conv_i2:
+ return MetaDataProvider.System_Int16;
+ case UnaryOperator.Conv_i4:
+ return MetaDataProvider.System_Int32;
+ case UnaryOperator.Conv_i8:
+ return MetaDataProvider.System_Int64;
+ case UnaryOperator.Conv_u1:
+ return MetaDataProvider.System_UInt8;
+ case UnaryOperator.Conv_u2:
+ return MetaDataProvider.System_UInt16;
+ case UnaryOperator.Conv_u4:
+ return MetaDataProvider.System_UInt32;
+ case UnaryOperator.Conv_u8:
+ return MetaDataProvider.System_UInt64;
+ default:
+ if (type.IsNormal)
+ return type.ConcreteType;
+ return MetaDataProvider.System_Int32;
+ }
+ }
+
+ public void CopyStackAddress (SymValue destAddr, int temporaryForWhichAddressIsTaken)
+ {
+ SymValue srcAddr = Address (temporaryForWhichAddressIsTaken);
+ this.egraph [this.Functions.ValueOf, destAddr] = srcAddr;
+ AbstractType aType = CurrentType (srcAddr);
+ FlatDomain<TypeNode> t = !aType.IsNormal ? new FlatDomain<TypeNode> () : MetaDataProvider.ManagedPointer (aType.Type.Concrete);
+ SetType (destAddr, t);
+ }
+
+ public SymValue PseudoFieldAddress (SymValue ptr, Method getter)
+ {
+ TypeNode pseudoFieldAddressType;
+ return PseudoFieldAddress (ptr, getter, out pseudoFieldAddressType, false);
+ }
+
+ public SymValue PseudoFieldAddress (SymValue sv, Method m, out TypeNode pseudoFieldAddressType, bool materialize)
+ {
+ pseudoFieldAddressType = MetaDataProvider.ManagedPointer (MetaDataProvider.ReturnType (m));
+ m = MetaDataProvider.Unspecialized (m);
+ bool fresh;
+ SymValue elem = LookupAddressAndManifestType (sv, this.Functions.For (m), pseudoFieldAddressType, out fresh);
+ if (fresh) {
+ if (IsUnmodified (sv))
+ MakeModified (elem);
+ if (IsModifiedAtCall (sv))
+ this.ModifiedAtCall = this.ModifiedAtCall.Add (elem);
+ if (materialize)
+ MaterializeAccordingToType (elem, pseudoFieldAddressType, 0);
+ }
+ return elem;
+ }
+
+ public SymValue FieldAddress (SymValue ptr, Field field)
+ {
+ TypeNode fieldAddressType;
+ return FieldAddress (ptr, field, out fieldAddressType);
+ }
+
+ public SymValue FieldAddress (SymValue ptr, Field field, out TypeNode fieldAddressType)
+ {
+ fieldAddressType = MetaDataProvider.ManagedPointer (MetaDataProvider.FieldType (field));
+ bool fresh;
+ SymValue sv = LookupAddressAndManifestType (ptr, this.Functions.For (field), fieldAddressType, out fresh);
+ if (fresh) {
+ if (IsUnmodifiedForFields (ptr) || MetaDataProvider.IsReadonly (field))
+ MakeUnmodified (sv);
+ if (IsModifiedAtCall (ptr))
+ this.ModifiedAtCall = this.ModifiedAtCall.Add (sv);
+ }
+ return sv;
+ }
+
+ public void Assign (Parameter parameter, TypeNode type)
+ {
+ AssignValue (Address (this.Functions.For (parameter)), type);
+ }
+
+ public SymValue PseudoFieldAddressOfOutParameter (int index, SymValue fieldAddr, TypeNode pType)
+ {
+ SymValue sv = this.egraph [this.Functions.ForConstant (index, MetaDataProvider.System_Int32), fieldAddr];
+ MaterializeAccordingToType (sv, pType, 2);
+ return sv;
+ }
+
+ public SymValue ObjectVersion (SymValue sv)
+ {
+ return this.egraph [this.Functions.ObjectVersion, sv];
+ }
+
+ public SymValue PseudoFieldAddress (SymValue[] args, Method method, out TypeNode pseudoFieldAddressType, bool materialize)
+ {
+ if (args.Length == 0 || args.Length == 1)
+ return PseudoFieldAddress (Globals, method, out pseudoFieldAddressType, materialize);
+ pseudoFieldAddressType = MetaDataProvider.ManagedPointer (MetaDataProvider.ReturnType (method));
+ method = MetaDataProvider.Unspecialized (method);
+
+ bool fresh;
+ SymValue sv = LookupAddressAndManifestType (args, this.Functions.For (method), pseudoFieldAddressType, out fresh);
+ if (fresh) {
+ if (AreUnmodified (args))
+ MakeUnmodified (sv);
+ if (AnyAreModifiedAtCall (args))
+ this.ModifiedAtCall = this.ModifiedAtCall.Add (sv);
+ if (materialize)
+ MaterializeAccordingToType (sv, pseudoFieldAddressType, 0);
+ }
+ return sv;
+ }
+
+ public void AssignReturnValue (int dest, TypeNode type)
+ {
+ AssignValue (dest, type);
+ if (MetaDataProvider.HasValueRepresentation (type))
+ this.egraph [this.Functions.ResultOfCall, Value (dest)] = Zero;
+ else
+ MaterializeAccordingToType (Address (dest), MetaDataProvider.ManagedPointer (type), 0);
+ }
+
+ public void MaterializeAccordingToType (SymValue sv, TypeNode type, int depth)
+ {
+ SetType (sv, type);
+ if (depth > 2)
+ return;
+
+ if (MetaDataProvider.IsManagedPointer (type)) {
+ TypeNode elementType = MetaDataProvider.ElementType (type);
+ if (!MetaDataProvider.HasValueRepresentation (elementType)) {
+ ManifestStructId (sv);
+ foreach (Field field in MetaDataProvider.Fields (elementType)) {
+ if (!MetaDataProvider.IsStatic (field)) {
+ TypeNode fieldAddressType;
+ MaterializeAccordingToType (FieldAddress (sv, field, out fieldAddressType), fieldAddressType, depth + 1);
+ }
+ }
+ foreach (Property property in MetaDataProvider.Properties (elementType)) {
+ Method getter;
+ if (!MetaDataProvider.IsStatic (property) && MetaDataProvider.HasGetter (property, out getter)) {
+ TypeNode pseudoFieldAddressType;
+ MaterializeAccordingToType (PseudoFieldAddress (sv, getter, out pseudoFieldAddressType, false), pseudoFieldAddressType, depth + 1);
+ }
+ }
+ } else
+ MaterializeAccordingToType (Value (sv), elementType, depth + 1);
+ }
+ }
+
+ public void ManifestStructId (SymValue sv)
+ {
+ StructId (sv);
+ }
+
+ public SymValue StructId (SymValue sv)
+ {
+ return this.egraph [this.Functions.StructId, sv];
+ }
+
+ private SymValue LookupAddressAndManifestType (SymValue sv, SymFunction c, TypeNode type, out bool fresh)
+ {
+ SymValue value = this.egraph.TryLookup (c, sv);
+ if (value != null) {
+ fresh = false;
+ return value;
+ }
+
+ fresh = true;
+ value = this.egraph [c, sv];
+ SetType (value, type);
+
+ return value;
+ }
+
+ public void HavocFields (SymValue sv, IEnumerable<Field> fields, ref IImmutableSet<SymValue> havoced)
+ {
+ foreach (Field f in fields)
+ HavocConstructor (null, sv, this.Functions.For (f), ref havoced, false);
+ }
+
+ private bool IsUnmodifiedForFields (SymValue sv)
+ {
+ return this.unmodifiedFieldsSinceEntry.Contains (sv);
+ }
+
+ public void HavocUp (SymValue srcAddr, ref IImmutableSet<SymValue> havocedAtCall, bool havocFields)
+ {
+ foreach (var term in this.egraph.EqTerms (srcAddr)) {
+ if (term.Function == this.Functions.ValueOf)
+ HavocUpField (term.Args [0], ref havocedAtCall, havocFields);
+ }
+ }
+
+ private void HavocUpField (SymValue sv, ref IImmutableSet<SymValue> havocedAtCall, bool havocFields)
+ {
+ foreach (var term in this.egraph.EqTerms (sv)) {
+ SymFunction accessedVia = term.Function;
+ if (accessedVia is Wrapper<Field>)
+ HavocUpObjectVersion (accessedVia, term.Args [0], ref havocedAtCall, havocFields);
+ else {
+ var methodWrapper = accessedVia as Wrapper<Method>;
+ Property property;
+ if (methodWrapper != null && !MetaDataProvider.IsStatic (methodWrapper.Item) && MetaDataProvider.IsPropertyGetter (methodWrapper.Item, out property))
+ HavocUpObjectVersion (accessedVia, term.Args [0], ref havocedAtCall, havocFields);
+ }
+ }
+ }
+
+ private void HavocUpObjectVersion (SymFunction accessedVia, SymValue sv, ref IImmutableSet<SymValue> havocedAtCall, bool havocFields)
+ {
+ if (havocedAtCall.Contains (sv))
+ return;
+ this.egraph.Eliminate (this.Functions.ObjectVersion, sv);
+ if (havocFields)
+ HavocMutableFields (accessedVia, sv, ref havocedAtCall);
+ else
+ HavocPseudoFields (accessedVia, sv, ref havocedAtCall);
+
+ HavocUp (sv, ref havocedAtCall, false);
+ }
+
+ public void CopyAddress (SymValue destAddr, SymValue srcAddr, TypeNode type)
+ {
+ this.egraph [this.Functions.ValueOf, destAddr] = srcAddr;
+ SetType (destAddr, MetaDataProvider.ManagedPointer (type));
+ }
+
+ public void AssignArrayLength (SymValue destAddr, SymValue array)
+ {
+ SymValue length = this.egraph [this.Functions.Length, array];
+ SetType (length, MetaDataProvider.System_Int32);
+ this.egraph [this.Functions.ValueOf, destAddr] = length;
+ SetType (destAddr, MetaDataProvider.ManagedPointer (MetaDataProvider.System_Int32));
+ }
+
+ public void ResetModifiedAtCall ()
+ {
+ this.ModifiedAtCall = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
+ }
+
+ public SymValue LoadValue (int source)
+ {
+ return Value (source);
+ }
+
+ public SymbolicValue TryLoadValue (SymValue addr)
+ {
+ return new SymbolicValue (Value (addr));
+ }
+
+ public bool TryGetArrayLength (SymValue arrayValue, out SymValue length)
+ {
+ length = this.egraph.TryLookup (this.Functions.Length, arrayValue);
+ return length != null;
+ }
+
+ public bool TryGetCorrespondingValueAbstraction (Parameter p, out SymbolicValue sv)
+ {
+ return TryGetCorrespondingValueAbstraction (this.Functions.For (p), out sv);
+ }
+
+ public string GetAccessPath (SymValue sv)
+ {
+ LispList<PathElementBase> bestAccessPath = GetBestAccessPath (sv, AccessPathFilter<Method>.NoFilter, true, true, false);
+ if (bestAccessPath == null)
+ return null;
+
+ return bestAccessPath.Select (i => (PathElement) i).ToCodeString ();
+ }
+
+ public LispList<PathElement> GetAccessPathList (SymValue symbol, AccessPathFilter<Method> filter, bool allowLocal, bool preferLocal)
+ {
+ return GetBestAccessPath (symbol, filter, true, allowLocal, preferLocal).Coerce<PathElementBase, PathElement> ();
+ }
+
+ public bool LessEqual (Domain that, out IImmutableMap<SymValue, LispList<SymValue>> forward, out IImmutableMap<SymValue, SymValue> backward)
+ {
+ return this.egraph.LessEqual (that.egraph, out forward, out backward);
+ }
+
+ public bool IsResultEGraph (IMergeInfo mi)
+ {
+ return mi.IsResultGraph (this.egraph);
+ }
+
+ public bool IsGraph1 (IMergeInfo mi)
+ {
+ return mi.IsGraph1 (this.egraph);
+ }
+
+ public bool IsGraph2 (IMergeInfo mi)
+ {
+ return mi.IsGraph2 (this.egraph);
+ }
+
+ public IImmutableMap<SymValue, LispList<SymValue>> GetForwardIdentityMap ()
+ {
+ return this.egraph.GetForwardIdentityMap ();
+ }
+
+ public Domain Join (Domain that, bool widening, out bool weaker, out IMergeInfo mergeInfo)
+ {
+ SymGraph<SymFunction, AbstractType> graph = this.egraph.Join (that.egraph, out mergeInfo, widening);
+ weaker = mergeInfo.Changed;
+
+ IImmutableSet<SymValue> resultUnmodifiedSinceEntry;
+ IImmutableSet<SymValue> resultUnmodifiedFieldsSinceEntry;
+ IImmutableSet<SymValue> resultModifiedAtCall;
+
+ ComputeJoinOfSets (mergeInfo, this, that, out resultUnmodifiedSinceEntry, out resultUnmodifiedFieldsSinceEntry, out resultModifiedAtCall, ref weaker);
+ Domain oldDomain = null;
+ if (OldDomain != null) {
+ bool oldWeaker;
+ IMergeInfo oldMergeInfo;
+ oldDomain = OldDomain.Join (that.OldDomain, widening, out oldWeaker, out oldMergeInfo);
+ }
+
+ return new Domain (graph, RecomputeConstantMap (graph), resultUnmodifiedSinceEntry, resultUnmodifiedFieldsSinceEntry, resultModifiedAtCall, this, oldDomain);
+ }
+
+ private IImmutableMap<SymValue, SymFunction> RecomputeConstantMap (SymGraph<SymFunction, AbstractType> graph)
+ {
+ IImmutableMap<SymValue, SymFunction> result = ImmutableIntKeyMap<SymValue, SymFunction>.Empty (SymValue.GetUniqueKey);
+ foreach (SymFunction constant in graph.Constants) {
+ if (this.Functions.IsConstantOrMethod (constant))
+ result.Add (graph [constant], constant);
+ }
+ return result;
+ }
+
+ private void ComputeJoinOfSets (IMergeInfo mergeInfo, Domain domain, Domain that,
+ out IImmutableSet<SymValue> resultUnmodifiedSinceEntry,
+ out IImmutableSet<SymValue> resultUnmodifiedFieldsSinceEntry,
+ out IImmutableSet<SymValue> resultModifiedAtCall, ref bool weaker)
+ {
+ resultUnmodifiedSinceEntry = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
+ resultUnmodifiedFieldsSinceEntry = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
+ resultModifiedAtCall = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
+
+ foreach (var tuple in mergeInfo.MergeTriples) {
+ SymValue symValue1 = tuple.Item1;
+ SymValue symValue2 = tuple.Item2;
+ SymValue elem = tuple.Item3;
+
+ bool unmodifiedSinceEntryContains = domain.unmodifiedSinceEntry.ContainsSafe (symValue1);
+ bool modifiedAtCallContains = domain.ModifiedAtCall.ContainsSafe (symValue1);
+
+ if (unmodifiedSinceEntryContains) {
+ if (that.unmodifiedSinceEntry.ContainsSafe (symValue2))
+ resultUnmodifiedSinceEntry = resultUnmodifiedSinceEntry.Add (elem);
+ else if (that.unmodifiedFieldsSinceEntry.ContainsSafe (symValue2))
+ resultUnmodifiedFieldsSinceEntry = resultUnmodifiedFieldsSinceEntry.Add (elem);
+ }
+
+ if (modifiedAtCallContains)
+ resultModifiedAtCall = resultModifiedAtCall.Add (elem);
+ }
+
+ if (that.unmodifiedSinceEntry.Count () > resultUnmodifiedSinceEntry.Count ()) {
+ weaker = true;
+ if (DebugOptions.Debug)
+ Console.WriteLine ("---Result changed due to fewer unmodified locations since entry");
+ } else {
+ if (that.unmodifiedFieldsSinceEntry.Count () > resultUnmodifiedFieldsSinceEntry.Count ()) {
+ weaker = true;
+ if (DebugOptions.Debug)
+ Console.WriteLine ("---Result changed due to fewer unmodified locations for fields since entry");
+ }
+ }
+ }
+
+ #region Implementation of IAbstractDomain<Domain>
+ public Domain Top
+ {
+ get
+ {
+ return new Domain (this.egraph.Top, ImmutableIntKeyMap<SymValue, SymFunction>.Empty (SymValue.GetUniqueKey), ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey),
+ ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey), ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey), this, null);
+ }
+ }
+
+ public Domain Bottom
+ {
+ get
+ {
+ if (BottomValue == null) {
+ BottomValue = new Domain (this.egraph.Bottom, ImmutableIntKeyMap<SymValue, SymFunction>.Empty (SymValue.GetUniqueKey), ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey),
+ ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey), ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey),
+ this, null);
+ BottomValue.ImmutableVersion ();
+ }
+ return BottomValue;
+ }
+ }
+
+ public bool IsTop
+ {
+ get { return this.egraph.IsTop; }
+ }
+
+ public bool IsBottom
+ {
+ get
+ {
+ if (this == BottomValue || this.egraph.IsBottom)
+ return true;
+ if (OldDomain != null)
+ return OldDomain.IsBottom;
+
+ return false;
+ }
+ }
+
+ public Domain Join (Domain that, bool widening, out bool weaker)
+ {
+ IMergeInfo mergeInfo;
+ return Join (that, widening, out weaker, out mergeInfo);
+ }
+
+ public Domain Meet (Domain that)
+ {
+ SymGraph<SymFunction, AbstractType> graph = this.egraph.Meet (that.egraph);
+ return new Domain (graph, RecomputeConstantMap (graph), this.unmodifiedSinceEntry, this.unmodifiedFieldsSinceEntry, null, this, OldDomain);
+ }
+
+ public bool LessEqual (Domain that)
+ {
+ return this.egraph.LessEqual (that.egraph);
+ }
+
+ public Domain ImmutableVersion ()
+ {
+ this.egraph.ImmutableVersion ();
+ return this;
+ }
+ #endregion
+ }
+}