1646 lines
53 KiB
C#
1646 lines
53 KiB
C#
//
|
|
// 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 (Sequence<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.Value) : 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.Value))
|
|
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.Value;
|
|
|
|
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.Value;
|
|
|
|
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.Value, target, atEndOld);
|
|
else if (atEndOld && targetType.IsNormal() && MetaDataProvider.IsManagedPointer (targetType.Value)) {
|
|
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<Sequence<PathElementBase>> GetAccessPathsRaw (SymValue sv, AccessPathFilter<Method> filter, bool compress)
|
|
{
|
|
var visited = new HashSet<SymValue> ();
|
|
return GetAccessPathsRaw (sv, null, visited, filter, compress);
|
|
}
|
|
|
|
private IEnumerable<Sequence<PathElementBase>> GetAccessPathsRaw (SymValue sv, Sequence<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)) {
|
|
Sequence<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 Sequence<PathElementBase> GetBestAccessPath (SymValue sv, AccessPathFilter<Method> filter, bool compress, bool allowLocal, bool preferLocal)
|
|
{
|
|
Sequence<PathElementBase> bestParameterPath = null;
|
|
Sequence<PathElementBase> bestLocalPath = null;
|
|
Sequence<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<Sequence<PathElementBase>> GetAccessPathsFiltered (SymValue sv, AccessPathFilter<Method> filter, bool compress)
|
|
{
|
|
return GetAccessPathsTyped (sv, filter, compress).Where (path => PathIsVisibleAccordingToFilter (path, filter));
|
|
}
|
|
|
|
private bool PathIsVisibleAccordingToFilter (Sequence<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 (Sequence<PathElementBase> path, out Sequence<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;
|
|
}
|
|
|
|
Sequence<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 (Sequence<PathElementBase> path, TypeNode prevType, out Sequence<PathElementBase> result)
|
|
{
|
|
if (path == null) {
|
|
result = null;
|
|
return true;
|
|
}
|
|
PathElementBase head = path.Head;
|
|
if (head.TrySetType (prevType, MetaDataProvider, out prevType)) {
|
|
Sequence<PathElementBase> updatedPath;
|
|
if (TryPropagateTypeInfoRecurse (path.Tail, prevType, out updatedPath)) {
|
|
result = updatedPath.Cons (head);
|
|
return true;
|
|
}
|
|
}
|
|
|
|
result = null;
|
|
return false;
|
|
}
|
|
|
|
private IEnumerable<Sequence<PathElementBase>> GetAccessPathsTyped (SymValue sv, AccessPathFilter<Method> filter, bool compress)
|
|
{
|
|
var visited = new HashSet<SymValue> ();
|
|
foreach (var path in GetAccessPathsRaw (sv, null, visited, filter, compress)) {
|
|
Sequence<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.Value);
|
|
|
|
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.Value))
|
|
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.Value))
|
|
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.Value);
|
|
}
|
|
|
|
private FlatDomain<TypeNode> TargetType (FlatDomain<TypeNode> type)
|
|
{
|
|
if (!type.IsNormal())
|
|
return type;
|
|
|
|
TypeNode normalType = type.Value;
|
|
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.Value) : type);
|
|
this.egraph [ptrValue] = aType;
|
|
this.egraph [this.Functions.ValueOf, address] = ptrValue;
|
|
} else
|
|
SetType (address, type.IsNormal() ? MetaDataProvider.ManagedPointer (type.Value) : 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.Value);
|
|
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)
|
|
{
|
|
Sequence<PathElementBase> bestAccessPath = GetBestAccessPath (sv, AccessPathFilter<Method>.NoFilter, true, true, false);
|
|
if (bestAccessPath == null)
|
|
return null;
|
|
|
|
return bestAccessPath.Select (i => (PathElement) i).ToCodeString ();
|
|
}
|
|
|
|
public Sequence<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, Sequence<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, Sequence<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)
|
|
{
|
|
throw new NotImplementedException();
|
|
}
|
|
|
|
public Domain Join (Domain that, bool widening, out bool weaker)
|
|
{
|
|
IMergeInfo mergeInfo;
|
|
return Join (that, widening, out weaker, out mergeInfo);
|
|
}
|
|
|
|
public Domain Widen(Domain that)
|
|
{
|
|
throw new NotImplementedException();
|
|
}
|
|
|
|
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
|
|
}
|
|
}
|