422 lines
14 KiB
C#
422 lines
14 KiB
C#
//
|
|
// Analysis.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.AST.Visitors;
|
|
using Mono.CodeContracts.Static.Analysis.Drivers;
|
|
using Mono.CodeContracts.Static.ControlFlow;
|
|
using Mono.CodeContracts.Static.DataFlowAnalysis;
|
|
using Mono.CodeContracts.Static.DataStructures;
|
|
using Mono.CodeContracts.Static.Lattices;
|
|
using Mono.CodeContracts.Static.Providers;
|
|
using Mono.CodeContracts.Static.Proving;
|
|
|
|
namespace Mono.CodeContracts.Static.Analysis.NonNull {
|
|
class Analysis<E, V> : ILVisitorBase<APC, V, V, NonNullDomain<V>, NonNullDomain<V>>,
|
|
IAnalysis<APC, NonNullDomain<V>, IILVisitor<APC, V, V, NonNullDomain<V>, NonNullDomain<V>>, IImmutableMap<V, Sequence<V>>>,
|
|
IMethodResult<V>, IFactBase<V>
|
|
where E : IEquatable<E>
|
|
where V : IEquatable<V>
|
|
{
|
|
private readonly Dictionary<APC, NonNullDomain<V>> callSiteCache = new Dictionary<APC, NonNullDomain<V>> ();
|
|
private readonly IMethodDriver<E, V> method_driver;
|
|
private IFixPointInfo<APC, NonNullDomain<V>> fix_point_info;
|
|
|
|
public Analysis (IMethodDriver<E, V> mdriver)
|
|
{
|
|
this.method_driver = mdriver;
|
|
}
|
|
|
|
protected internal IExpressionContextProvider<E, V> ContextProvider
|
|
{
|
|
get { return this.method_driver.ContextProvider; }
|
|
}
|
|
|
|
protected IMetaDataProvider MetaDataProvider
|
|
{
|
|
get { return this.method_driver.MetaDataProvider; }
|
|
}
|
|
|
|
#region IAnalysis<APC,Domain<V>,IILVisitor<APC,V,V,Domain<V>,Domain<V>>,IImmutableMap<V,Sequence<V>>> Members
|
|
public IILVisitor<APC, V, V, NonNullDomain<V>, NonNullDomain<V>> GetVisitor ()
|
|
{
|
|
return this;
|
|
}
|
|
|
|
public NonNullDomain<V> Join (Pair<APC, APC> edge, NonNullDomain<V> newstate, NonNullDomain<V> prevstate, out bool weaker, bool widen)
|
|
{
|
|
bool nonNullWeaker;
|
|
SetDomain<V> nonNulls = prevstate.NonNulls.Join (newstate.NonNulls, widen, out nonNullWeaker);
|
|
bool nullWeaker;
|
|
SetDomain<V> nulls = prevstate.Nulls.Join (newstate.Nulls, widen, out nullWeaker);
|
|
|
|
weaker = nonNullWeaker || nullWeaker;
|
|
return new NonNullDomain<V> (nonNulls, nulls);
|
|
}
|
|
|
|
public NonNullDomain<V> ImmutableVersion (NonNullDomain<V> state)
|
|
{
|
|
return state;
|
|
}
|
|
|
|
public NonNullDomain<V> MutableVersion (NonNullDomain<V> state)
|
|
{
|
|
return state;
|
|
}
|
|
|
|
public NonNullDomain<V> EdgeConversion (APC from, APC to, bool isJoinPoint, IImmutableMap<V, Sequence<V>> data, NonNullDomain<V> state)
|
|
{
|
|
if (data == null)
|
|
return state;
|
|
SetDomain<V> oldNonNulls = state.NonNulls;
|
|
SetDomain<V> nonNulls = SetDomain<V>.TopValue;
|
|
|
|
SetDomain<V> oldNulls = state.Nulls;
|
|
SetDomain<V> nulls = SetDomain<V>.TopValue;
|
|
foreach (V variable in data.Keys) {
|
|
bool nonNullContains = oldNonNulls.Contains (variable);
|
|
bool nullContains = oldNulls.Contains (variable);
|
|
|
|
if (nonNullContains || nullContains) {
|
|
foreach (V anotherVariable in data [variable].AsEnumerable ()) {
|
|
if (nonNullContains)
|
|
nonNulls = nonNulls.With (anotherVariable);
|
|
if (nullContains)
|
|
nulls = nulls.With (anotherVariable);
|
|
}
|
|
}
|
|
}
|
|
|
|
return new NonNullDomain<V> (nonNulls, nulls);
|
|
}
|
|
|
|
public bool IsBottom (APC pc, NonNullDomain<V> state)
|
|
{
|
|
return state.NonNulls.IsBottom;
|
|
}
|
|
|
|
public Predicate<APC> SaveFixPointInfo (IFixPointInfo<APC, NonNullDomain<V>> fixPointInfo)
|
|
{
|
|
this.fix_point_info = fixPointInfo;
|
|
|
|
//todo: implement this
|
|
return pc => true;
|
|
}
|
|
|
|
public void Dump (Pair<NonNullDomain<V>, TextWriter> pair)
|
|
{
|
|
TextWriter tw = pair.Value;
|
|
tw.Write ("NonNulls: ");
|
|
pair.Key.NonNulls.Dump (tw);
|
|
tw.Write ("Nulls: ");
|
|
pair.Key.Nulls.Dump (tw);
|
|
}
|
|
#endregion
|
|
|
|
#region IFactBase<V> Members
|
|
public FlatDomain<bool> IsNull(APC pc, V variable)
|
|
{
|
|
if (ContextProvider.ValueContext.IsZero (pc, variable))
|
|
return ProofOutcome.True;
|
|
|
|
NonNullDomain<V> domain;
|
|
if (!PreStateLookup (pc, out domain) || domain.NonNulls.IsBottom)
|
|
return ProofOutcome.Bottom;
|
|
if (domain.IsNonNull (variable))
|
|
return ProofOutcome.False;
|
|
if (domain.IsNull (variable))
|
|
return ProofOutcome.True;
|
|
|
|
return ProofOutcome.Top;
|
|
}
|
|
|
|
public FlatDomain<bool> IsNonNull(APC pc, V variable)
|
|
{
|
|
NonNullDomain<V> domain;
|
|
if (!PreStateLookup (pc, out domain) || domain.NonNulls.IsBottom)
|
|
return ProofOutcome.Bottom;
|
|
if (domain.IsNonNull (variable))
|
|
return ProofOutcome.True;
|
|
if (ContextProvider.ValueContext.IsZero (pc, variable) || domain.IsNull (variable))
|
|
return ProofOutcome.False;
|
|
|
|
FlatDomain<TypeNode> aType = ContextProvider.ValueContext.GetType (pc, variable);
|
|
if (aType.IsNormal() && MetaDataProvider.IsManagedPointer (aType.Value))
|
|
return ProofOutcome.True;
|
|
|
|
return ProofOutcome.Top;
|
|
}
|
|
|
|
public bool IsUnreachable (APC pc)
|
|
{
|
|
NonNullDomain<V> domain;
|
|
if (!PreStateLookup (pc, out domain) || domain.NonNulls.IsBottom)
|
|
return true;
|
|
|
|
return false;
|
|
}
|
|
#endregion
|
|
|
|
public override NonNullDomain<V> DefaultVisit (APC pc, NonNullDomain<V> data)
|
|
{
|
|
return data;
|
|
}
|
|
|
|
public static NonNullDomain<V> AssumeNonNull (V dest, NonNullDomain<V> domain)
|
|
{
|
|
if (!domain.NonNulls.Contains (dest))
|
|
return new NonNullDomain<V> (domain.NonNulls.With (dest), domain.Nulls);
|
|
|
|
return domain;
|
|
}
|
|
|
|
public static NonNullDomain<V> AssumeNull (V dest, NonNullDomain<V> before)
|
|
{
|
|
if (!before.Nulls.Contains (dest))
|
|
return new NonNullDomain<V> (before.NonNulls, before.Nulls.With (dest));
|
|
|
|
return before;
|
|
}
|
|
|
|
public override NonNullDomain<V> Assert(APC pc, EdgeTag tag, V condition, NonNullDomain<V> data)
|
|
{
|
|
return ContextProvider.ExpressionContext.Decode
|
|
<Pair<bool, NonNullDomain<V>>, NonNullDomain<V>, ExpressionAssumeDecoder<E, V>>
|
|
(
|
|
ContextProvider.ExpressionContext.Refine (pc, condition),
|
|
new ExpressionAssumeDecoder<E, V> (ContextProvider),
|
|
new Pair<bool, NonNullDomain<V>> (true, data));
|
|
}
|
|
|
|
public override NonNullDomain<V> Assume (APC pc, EdgeTag tag, V condition, NonNullDomain<V> data)
|
|
{
|
|
IExpressionContext<E, V> exprCtx = ContextProvider.ExpressionContext;
|
|
E expr = exprCtx.Refine (pc, condition);
|
|
|
|
return exprCtx.Decode<Pair<bool, NonNullDomain<V>>, NonNullDomain<V>, ExpressionAssumeDecoder<E, V>>
|
|
(expr, new ExpressionAssumeDecoder<E, V> (ContextProvider),
|
|
new Pair<bool, NonNullDomain<V>> (tag != EdgeTag.False, data));
|
|
}
|
|
|
|
public override NonNullDomain<V> Unary (APC pc, UnaryOperator op, bool unsigned, V dest, V source, NonNullDomain<V> data)
|
|
{
|
|
switch (op) {
|
|
case UnaryOperator.Conv_i:
|
|
case UnaryOperator.Conv_u:
|
|
if (data.IsNonNull (source))
|
|
return AssumeNonNull (dest, data);
|
|
break;
|
|
}
|
|
return data;
|
|
}
|
|
|
|
public override NonNullDomain<V> Call<TypeList, ArgList> (APC pc, Method method, bool virt, TypeList extraVarargs, V dest, ArgList args, NonNullDomain<V> data)
|
|
{
|
|
this.callSiteCache [pc] = data;
|
|
if (!MetaDataProvider.IsStatic (method))
|
|
return AssumeNonNull (args [0], data);
|
|
|
|
return data;
|
|
}
|
|
|
|
public override NonNullDomain<V> CastClass (APC pc, TypeNode type, V dest, V obj, NonNullDomain<V> data)
|
|
{
|
|
if (data.NonNulls.Contains (obj))
|
|
return AssumeNonNull (dest, data);
|
|
|
|
return data;
|
|
}
|
|
|
|
public override NonNullDomain<V> Entry (APC pc, Method method, NonNullDomain<V> data)
|
|
{
|
|
APC at = ContextProvider.MethodContext.CFG.Next (pc);
|
|
NonNullDomain<V> domain = data;
|
|
IIndexable<Parameter> parameters = MetaDataProvider.Parameters (method);
|
|
TypeNode eventArgsType;
|
|
bool systemType = MetaDataProvider.TryGetSystemType ("System.EventArgs", out eventArgsType);
|
|
for (int i = 0; i < parameters.Count; i++) {
|
|
Parameter p = parameters [i];
|
|
TypeNode pType = MetaDataProvider.ParameterType (p);
|
|
if (MetaDataProvider.IsManagedPointer (pType)) {
|
|
V sv;
|
|
if (ContextProvider.ValueContext.TryParameterValue (at, p, out sv))
|
|
domain = AssumeNonNull (sv, domain);
|
|
} else {
|
|
V sv;
|
|
if (i == 0 && parameters.Count == 1 && MetaDataProvider.IsArray (pType)
|
|
&& MetaDataProvider.Name (method) == "Main" && MetaDataProvider.IsStatic (method) &&
|
|
ContextProvider.ValueContext.TryParameterValue (pc, p, out sv))
|
|
domain = AssumeNonNull (sv, domain);
|
|
}
|
|
}
|
|
V sv1;
|
|
if (systemType && parameters.Count == 2 && MetaDataProvider.Equal (MetaDataProvider.System_Object, MetaDataProvider.ParameterType (parameters [0])) &&
|
|
MetaDataProvider.DerivesFrom (MetaDataProvider.ParameterType (parameters [1]), eventArgsType)
|
|
&& ContextProvider.ValueContext.TryParameterValue (pc, parameters [1], out sv1))
|
|
domain = AssumeNonNull (sv1, domain);
|
|
if (!MetaDataProvider.IsStatic (method) && ContextProvider.ValueContext.TryParameterValue (pc, MetaDataProvider.This (method), out sv1))
|
|
domain = AssumeNonNull (sv1, domain);
|
|
|
|
return domain;
|
|
}
|
|
|
|
public override NonNullDomain<V> LoadStack (APC pc, int offset, V dest, V source, bool isOld, NonNullDomain<V> data)
|
|
{
|
|
NonNullDomain<V> old;
|
|
if (isOld && TryFindOldState (pc, out old)) {
|
|
if (old.IsNonNull (source))
|
|
return AssumeNonNull (dest, data);
|
|
if (old.IsNull (source))
|
|
return AssumeNull (dest, data);
|
|
}
|
|
|
|
return data;
|
|
}
|
|
|
|
public override NonNullDomain<V> Isinst (APC pc, TypeNode type, V dest, V obj, NonNullDomain<V> data)
|
|
{
|
|
if (data.IsNonNull (obj)) {
|
|
FlatDomain<TypeNode> aType = ContextProvider.ValueContext.GetType (pc, obj);
|
|
if (aType.IsNormal() && MetaDataProvider.DerivesFrom (aType.Value, type))
|
|
return AssumeNonNull (dest, data);
|
|
}
|
|
return data;
|
|
}
|
|
|
|
public override NonNullDomain<V> LoadArgAddress (APC pc, Parameter argument, bool isOld, V dest, NonNullDomain<V> data)
|
|
{
|
|
return AssumeNonNull (dest, data);
|
|
}
|
|
|
|
public override NonNullDomain<V> LoadConst (APC pc, TypeNode type, object constant, V dest, NonNullDomain<V> data)
|
|
{
|
|
if (constant is string)
|
|
return AssumeNonNull (dest, data);
|
|
|
|
return data;
|
|
}
|
|
|
|
public override NonNullDomain<V> LoadElement (APC pc, TypeNode type, V dest, V array, V index, NonNullDomain<V> data)
|
|
{
|
|
return AssumeNonNull (array, data);
|
|
}
|
|
|
|
public override NonNullDomain<V> LoadField (APC pc, Field field, V dest, V obj, NonNullDomain<V> data)
|
|
{
|
|
NonNullDomain<V> domain = AssumeNonNull (obj, data);
|
|
FlatDomain<TypeNode> aType = ContextProvider.ValueContext.GetType (ContextProvider.MethodContext.CFG.Next (pc), dest);
|
|
if (aType.IsNormal() && MetaDataProvider.IsManagedPointer (aType.Value))
|
|
domain = AssumeNonNull (dest, domain);
|
|
|
|
return domain;
|
|
}
|
|
|
|
public override NonNullDomain<V> LoadFieldAddress (APC pc, Field field, V dest, V obj, NonNullDomain<V> data)
|
|
{
|
|
NonNullDomain<V> domain = AssumeNonNull (obj, data);
|
|
return AssumeNonNull (dest, domain);
|
|
}
|
|
|
|
public override NonNullDomain<V> LoadStaticFieldAddress (APC pc, Field field, V dest, NonNullDomain<V> data)
|
|
{
|
|
return AssumeNonNull (dest, data);
|
|
}
|
|
|
|
public override NonNullDomain<V> LoadLength (APC pc, V dest, V array, NonNullDomain<V> data)
|
|
{
|
|
return AssumeNonNull (array, data);
|
|
}
|
|
|
|
public override NonNullDomain<V> NewArray<ArgList> (APC pc, TypeNode type, V dest, ArgList lengths, NonNullDomain<V> data)
|
|
{
|
|
return AssumeNonNull (dest, data);
|
|
}
|
|
|
|
public override NonNullDomain<V> NewObj<ArgList> (APC pc, Method ctor, V dest, ArgList args, NonNullDomain<V> data)
|
|
{
|
|
return AssumeNonNull (dest, data);
|
|
}
|
|
|
|
public override NonNullDomain<V> StoreElement (APC pc, TypeNode type, V array, V index, V value, NonNullDomain<V> data)
|
|
{
|
|
return AssumeNonNull (array, data);
|
|
}
|
|
|
|
public override NonNullDomain<V> StoreField (APC pc, Field field, V obj, V value, NonNullDomain<V> data)
|
|
{
|
|
return AssumeNonNull (obj, data);
|
|
}
|
|
|
|
private bool TryFindOldState (APC pc, out NonNullDomain<V> old)
|
|
{
|
|
if (pc.SubroutineContext.AsEnumerable().Any (edge => edge.Tag.Is (EdgeTag.AfterMask)))
|
|
return this.callSiteCache.TryGetValue (pc, out old);
|
|
|
|
return false.Without (out old);
|
|
}
|
|
|
|
public NonNullDomain<V> InitialValue (Func<V, int> keyConverter)
|
|
{
|
|
return new NonNullDomain<V> (new SetDomain<V> (keyConverter), new SetDomain<V> (keyConverter));
|
|
}
|
|
|
|
#region Implementation of IMethodResult<Variable>
|
|
public IMethodAnalysis MethodAnalysis { get; set; }
|
|
|
|
public void ValidateImplicitAssertions (IFactQuery<BoxedExpression, V> facts, List<string> proofResults)
|
|
{
|
|
}
|
|
|
|
public IFactQuery<BoxedExpression, V> FactQuery
|
|
{
|
|
get { return new SimpleLogicInference<E, V> (ContextProvider, this, this.method_driver.BasicFacts.IsUnreachable); }
|
|
}
|
|
|
|
public FlatDomain<bool> ValidateExplicitAssertion(APC pc, V value)
|
|
{
|
|
NonNullDomain<V> domain;
|
|
if (PreStateLookup (pc, out domain) && !domain.NonNulls.IsBottom) {
|
|
IExpressionContext<E, V> exprCtx = ContextProvider.ExpressionContext;
|
|
return exprCtx.Decode<bool, FlatDomain<bool>, ExpressionAssertDischarger<E, V>>(exprCtx.Refine(pc, value), new ExpressionAssertDischarger<E, V>(this, pc), true);
|
|
}
|
|
return ProofOutcome.Bottom;
|
|
}
|
|
|
|
private bool PreStateLookup (APC pc, out NonNullDomain<V> domain)
|
|
{
|
|
return this.fix_point_info.PreStateLookup (pc, out domain);
|
|
}
|
|
#endregion
|
|
}
|
|
}
|