mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.NonNull/Analysis.cs

   1 //
   2 // Analysis.cs
   3 //
   4 // Authors:
   5 //      Alexander Chebaturkin (chebaturkin@gmail.com)
   6 //
   7 // Copyright (C) 2011 Alexander Chebaturkin
   8 //
   9 // Permission is hereby granted, free of charge, to any person obtaining
  10 // a copy of this software and associated documentation files (the
  11 // "Software"), to deal in the Software without restriction, including
  12 // without limitation the rights to use, copy, modify, merge, publish,
  13 // distribute, sublicense, and/or sell copies of the Software, and to
  14 // permit persons to whom the Software is furnished to do so, subject to
  15 // the following conditions:
  16 //
  17 // The above copyright notice and this permission notice shall be
  18 // included in all copies or substantial portions of the Software.
  19 //
  20 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
  21 // EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
  22 // MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  23 // NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
  24 // LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
  25 // OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
  26 // WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  27 //
  28
  29 using System;
  30 using System.Collections.Generic;
  31 using System.IO;
  32 using System.Linq;
  33
  34 using Mono.CodeContracts.Static.AST;
  35 using Mono.CodeContracts.Static.AST.Visitors;
  36 using Mono.CodeContracts.Static.Analysis.Drivers;
  37 using Mono.CodeContracts.Static.ControlFlow;
  38 using Mono.CodeContracts.Static.DataFlowAnalysis;
  39 using Mono.CodeContracts.Static.DataStructures;
  40 using Mono.CodeContracts.Static.Lattices;
  41 using Mono.CodeContracts.Static.Providers;
  42 using Mono.CodeContracts.Static.Proving;
  43
  44 namespace Mono.CodeContracts.Static.Analysis.NonNull {
  45         class Analysis<E, V> : ILVisitorBase<APC, V, V, NonNullDomain<V>, NonNullDomain<V>>,
  46                                    IAnalysis<APC, NonNullDomain<V>, IILVisitor<APC, V, V, NonNullDomain<V>, NonNullDomain<V>>, IImmutableMap<V, Sequence<V>>>,
  47                                    IMethodResult<V>, IFactBase<V>
  48             where E : IEquatable<E>
  49             where V : IEquatable<V>
  50     {
  51                 private readonly Dictionary<APC, NonNullDomain<V>> callSiteCache = new Dictionary<APC, NonNullDomain<V>> ();
  52                 private readonly IMethodDriver<E, V> method_driver;
  53                 private IFixPointInfo<APC, NonNullDomain<V>> fix_point_info;
  54
  55                 public Analysis (IMethodDriver<E, V> mdriver)
  56                 {
  57                         this.method_driver = mdriver;
  58                 }
  59
  60                 protected internal IExpressionContextProvider<E, V> ContextProvider
  61                 {
  62                         get { return this.method_driver.ContextProvider; }
  63                 }
  64
  65                 protected IMetaDataProvider MetaDataProvider
  66                 {
  67                         get { return this.method_driver.MetaDataProvider; }
  68                 }
  69
  70                 #region IAnalysis<APC,Domain<V>,IILVisitor<APC,V,V,Domain<V>,Domain<V>>,IImmutableMap<V,Sequence<V>>> Members
  71                 public IILVisitor<APC, V, V, NonNullDomain<V>, NonNullDomain<V>> GetVisitor ()
  72                 {
  73                         return this;
  74                 }
  75
  76                 public NonNullDomain<V> Join (Pair<APC, APC> edge, NonNullDomain<V> newstate, NonNullDomain<V> prevstate, out bool weaker, bool widen)
  77                 {
  78                         bool nonNullWeaker;
  79                         SetDomain<V> nonNulls = prevstate.NonNulls.Join (newstate.NonNulls, widen, out nonNullWeaker);
  80                         bool nullWeaker;
  81                         SetDomain<V> nulls = prevstate.Nulls.Join (newstate.Nulls, widen, out nullWeaker);
  82
  83                         weaker = nonNullWeaker || nullWeaker;
  84                         return new NonNullDomain<V> (nonNulls, nulls);
  85                 }
  86
  87                 public NonNullDomain<V> ImmutableVersion (NonNullDomain<V> state)
  88                 {
  89                         return state;
  90                 }
  91
  92                 public NonNullDomain<V> MutableVersion (NonNullDomain<V> state)
  93                 {
  94                         return state;
  95                 }
  96
  97                 public NonNullDomain<V> EdgeConversion (APC from, APC to, bool isJoinPoint, IImmutableMap<V, Sequence<V>> data, NonNullDomain<V> state)
  98                 {
  99                         if (data == null)
 100                                 return state;
 101                         SetDomain<V> oldNonNulls = state.NonNulls;
 102                         SetDomain<V> nonNulls = SetDomain<V>.TopValue;
 103
 104                         SetDomain<V> oldNulls = state.Nulls;
 105                         SetDomain<V> nulls = SetDomain<V>.TopValue;
 106                         foreach (V variable in data.Keys) {
 107                                 bool nonNullContains = oldNonNulls.Contains (variable);
 108                                 bool nullContains = oldNulls.Contains (variable);
 109
 110                                 if (nonNullContains || nullContains) {
 111                                         foreach (V anotherVariable in data [variable].AsEnumerable ()) {
 112                                                 if (nonNullContains)
 113                                                         nonNulls = nonNulls.With (anotherVariable);
 114                                                 if (nullContains)
 115                                                         nulls = nulls.With (anotherVariable);
 116                                         }
 117                                 }
 118                         }
 119
 120                         return new NonNullDomain<V> (nonNulls, nulls);
 121                 }
 122
 123                 public bool IsBottom (APC pc, NonNullDomain<V> state)
 124                 {
 125                         return state.NonNulls.IsBottom;
 126                 }
 127
 128                 public Predicate<APC> SaveFixPointInfo (IFixPointInfo<APC, NonNullDomain<V>> fixPointInfo)
 129                 {
 130                         this.fix_point_info = fixPointInfo;
 131
 132                         //todo: implement this
 133                         return pc => true;
 134                 }
 135
 136                 public void Dump (Pair<NonNullDomain<V>, TextWriter> pair)
 137                 {
 138                         TextWriter tw = pair.Value;
 139                         tw.Write ("NonNulls: ");
 140                         pair.Key.NonNulls.Dump (tw);
 141                         tw.Write ("Nulls: ");
 142                         pair.Key.Nulls.Dump (tw);
 143                 }
 144                 #endregion
 145
 146                 #region IFactBase<V> Members
 147         public FlatDomain<bool> IsNull(APC pc, V variable)
 148                 {
 149                         if (ContextProvider.ValueContext.IsZero (pc, variable))
 150                                 return ProofOutcome.True;
 151
 152                         NonNullDomain<V> domain;
 153                         if (!PreStateLookup (pc, out domain) || domain.NonNulls.IsBottom)
 154                                 return ProofOutcome.Bottom;
 155                         if (domain.IsNonNull (variable))
 156                                 return ProofOutcome.False;
 157                         if (domain.IsNull (variable))
 158                                 return ProofOutcome.True;
 159
 160                         return ProofOutcome.Top;
 161                 }
 162
 163         public FlatDomain<bool> IsNonNull(APC pc, V variable)
 164                 {
 165                         NonNullDomain<V> domain;
 166                         if (!PreStateLookup (pc, out domain) || domain.NonNulls.IsBottom)
 167                                 return ProofOutcome.Bottom;
 168                         if (domain.IsNonNull (variable))
 169                                 return ProofOutcome.True;
 170                         if (ContextProvider.ValueContext.IsZero (pc, variable) || domain.IsNull (variable))
 171                                 return ProofOutcome.False;
 172
 173                         FlatDomain<TypeNode> aType = ContextProvider.ValueContext.GetType (pc, variable);
 174                         if (aType.IsNormal() && MetaDataProvider.IsManagedPointer (aType.Value))
 175                                 return ProofOutcome.True;
 176
 177                         return ProofOutcome.Top;
 178                 }
 179
 180                 public bool IsUnreachable (APC pc)
 181                 {
 182                         NonNullDomain<V> domain;
 183                         if (!PreStateLookup (pc, out domain) || domain.NonNulls.IsBottom)
 184                                 return true;
 185
 186                         return false;
 187                 }
 188                 #endregion
 189
 190                 public override NonNullDomain<V> DefaultVisit (APC pc, NonNullDomain<V> data)
 191                 {
 192                         return data;
 193                 }
 194
 195                 public static NonNullDomain<V> AssumeNonNull (V dest, NonNullDomain<V> domain)
 196                 {
 197                         if (!domain.NonNulls.Contains (dest))
 198                                 return new NonNullDomain<V> (domain.NonNulls.With (dest), domain.Nulls);
 199
 200                         return domain;
 201                 }
 202
 203                 public static NonNullDomain<V> AssumeNull (V dest, NonNullDomain<V> before)
 204                 {
 205                         if (!before.Nulls.Contains (dest))
 206                                 return new NonNullDomain<V> (before.NonNulls, before.Nulls.With (dest));
 207
 208                         return before;
 209                 }
 210
 211         public override NonNullDomain<V> Assert(APC pc, EdgeTag tag, V condition, NonNullDomain<V> data)
 212         {
 213             return ContextProvider.ExpressionContext.Decode
 214                 <Pair<bool, NonNullDomain<V>>, NonNullDomain<V>, ExpressionAssumeDecoder<E, V>>
 215                 (
 216                     ContextProvider.ExpressionContext.Refine (pc, condition),
 217                     new ExpressionAssumeDecoder<E, V> (ContextProvider),
 218                     new Pair<bool, NonNullDomain<V>> (true, data));
 219         }
 220
 221             public override NonNullDomain<V> Assume (APC pc, EdgeTag tag, V condition, NonNullDomain<V> data)
 222                 {
 223                         IExpressionContext<E, V> exprCtx = ContextProvider.ExpressionContext;
 224                         E expr = exprCtx.Refine (pc, condition);
 225
 226                         return exprCtx.Decode<Pair<bool, NonNullDomain<V>>, NonNullDomain<V>, ExpressionAssumeDecoder<E, V>>
 227                                 (expr, new ExpressionAssumeDecoder<E, V> (ContextProvider),
 228                                  new Pair<bool, NonNullDomain<V>> (tag != EdgeTag.False, data));
 229                 }
 230
 231                 public override NonNullDomain<V> Unary (APC pc, UnaryOperator op, bool unsigned, V dest, V source, NonNullDomain<V> data)
 232                 {
 233                         switch (op) {
 234                         case UnaryOperator.Conv_i:
 235                         case UnaryOperator.Conv_u:
 236                                 if (data.IsNonNull (source))
 237                                         return AssumeNonNull (dest, data);
 238                                 break;
 239                         }
 240                         return data;
 241                 }
 242
 243                 public override NonNullDomain<V> Call<TypeList, ArgList> (APC pc, Method method, bool virt, TypeList extraVarargs, V dest, ArgList args, NonNullDomain<V> data)
 244                 {
 245                         this.callSiteCache [pc] = data;
 246                         if (!MetaDataProvider.IsStatic (method))
 247                                 return AssumeNonNull (args [0], data);
 248
 249                         return data;
 250                 }
 251
 252                 public override NonNullDomain<V> CastClass (APC pc, TypeNode type, V dest, V obj, NonNullDomain<V> data)
 253                 {
 254                         if (data.NonNulls.Contains (obj))
 255                                 return AssumeNonNull (dest, data);
 256
 257                         return data;
 258                 }
 259
 260                 public override NonNullDomain<V> Entry (APC pc, Method method, NonNullDomain<V> data)
 261                 {
 262                         APC at = ContextProvider.MethodContext.CFG.Next (pc);
 263                         NonNullDomain<V> domain = data;
 264                         IIndexable<Parameter> parameters = MetaDataProvider.Parameters (method);
 265                         TypeNode eventArgsType;
 266                         bool systemType = MetaDataProvider.TryGetSystemType ("System.EventArgs", out eventArgsType);
 267                         for (int i = 0; i < parameters.Count; i++) {
 268                                 Parameter p = parameters [i];
 269                                 TypeNode pType = MetaDataProvider.ParameterType (p);
 270                                 if (MetaDataProvider.IsManagedPointer (pType)) {
 271                                         V sv;
 272                                         if (ContextProvider.ValueContext.TryParameterValue (at, p, out sv))
 273                                                 domain = AssumeNonNull (sv, domain);
 274                                 } else {
 275                                         V sv;
 276                                         if (i == 0 && parameters.Count == 1 && MetaDataProvider.IsArray (pType)
 277                                             && MetaDataProvider.Name (method) == "Main" && MetaDataProvider.IsStatic (method) &&
 278                                             ContextProvider.ValueContext.TryParameterValue (pc, p, out sv))
 279                                                 domain = AssumeNonNull (sv, domain);
 280                                 }
 281                         }
 282                         V sv1;
 283                         if (systemType && parameters.Count == 2 && MetaDataProvider.Equal (MetaDataProvider.System_Object, MetaDataProvider.ParameterType (parameters [0])) &&
 284                             MetaDataProvider.DerivesFrom (MetaDataProvider.ParameterType (parameters [1]), eventArgsType)
 285                             && ContextProvider.ValueContext.TryParameterValue (pc, parameters [1], out sv1))
 286                                 domain = AssumeNonNull (sv1, domain);
 287                         if (!MetaDataProvider.IsStatic (method) && ContextProvider.ValueContext.TryParameterValue (pc, MetaDataProvider.This (method), out sv1))
 288                                 domain = AssumeNonNull (sv1, domain);
 289
 290                         return domain;
 291                 }
 292
 293                 public override NonNullDomain<V> LoadStack (APC pc, int offset, V dest, V source, bool isOld, NonNullDomain<V> data)
 294                 {
 295                         NonNullDomain<V> old;
 296                         if (isOld && TryFindOldState (pc, out old)) {
 297                                 if (old.IsNonNull (source))
 298                                         return AssumeNonNull (dest, data);
 299                                 if (old.IsNull (source))
 300                                         return AssumeNull (dest, data);
 301                         }
 302
 303                         return data;
 304                 }
 305
 306                 public override NonNullDomain<V> Isinst (APC pc, TypeNode type, V dest, V obj, NonNullDomain<V> data)
 307                 {
 308                         if (data.IsNonNull (obj)) {
 309                                 FlatDomain<TypeNode> aType = ContextProvider.ValueContext.GetType (pc, obj);
 310                                 if (aType.IsNormal() && MetaDataProvider.DerivesFrom (aType.Value, type))
 311                                         return AssumeNonNull (dest, data);
 312                         }
 313                         return data;
 314                 }
 315
 316                 public override NonNullDomain<V> LoadArgAddress (APC pc, Parameter argument, bool isOld, V dest, NonNullDomain<V> data)
 317                 {
 318                         return AssumeNonNull (dest, data);
 319                 }
 320
 321                 public override NonNullDomain<V> LoadConst (APC pc, TypeNode type, object constant, V dest, NonNullDomain<V> data)
 322                 {
 323                         if (constant is string)
 324                                 return AssumeNonNull (dest, data);
 325
 326                         return data;
 327                 }
 328
 329                 public override NonNullDomain<V> LoadElement (APC pc, TypeNode type, V dest, V array, V index, NonNullDomain<V> data)
 330                 {
 331                         return AssumeNonNull (array, data);
 332                 }
 333
 334                 public override NonNullDomain<V> LoadField (APC pc, Field field, V dest, V obj, NonNullDomain<V> data)
 335                 {
 336                         NonNullDomain<V> domain = AssumeNonNull (obj, data);
 337                         FlatDomain<TypeNode> aType = ContextProvider.ValueContext.GetType (ContextProvider.MethodContext.CFG.Next (pc), dest);
 338                         if (aType.IsNormal() && MetaDataProvider.IsManagedPointer (aType.Value))
 339                                 domain = AssumeNonNull (dest, domain);
 340
 341                         return domain;
 342                 }
 343
 344                 public override NonNullDomain<V> LoadFieldAddress (APC pc, Field field, V dest, V obj, NonNullDomain<V> data)
 345                 {
 346                         NonNullDomain<V> domain = AssumeNonNull (obj, data);
 347                         return AssumeNonNull (dest, domain);
 348                 }
 349
 350                 public override NonNullDomain<V> LoadStaticFieldAddress (APC pc, Field field, V dest, NonNullDomain<V> data)
 351                 {
 352                         return AssumeNonNull (dest, data);
 353                 }
 354
 355                 public override NonNullDomain<V> LoadLength (APC pc, V dest, V array, NonNullDomain<V> data)
 356                 {
 357                         return AssumeNonNull (array, data);
 358                 }
 359
 360                 public override NonNullDomain<V> NewArray<ArgList> (APC pc, TypeNode type, V dest, ArgList lengths, NonNullDomain<V> data)
 361                 {
 362                         return AssumeNonNull (dest, data);
 363                 }
 364
 365                 public override NonNullDomain<V> NewObj<ArgList> (APC pc, Method ctor, V dest, ArgList args, NonNullDomain<V> data)
 366                 {
 367                         return AssumeNonNull (dest, data);
 368                 }
 369
 370                 public override NonNullDomain<V> StoreElement (APC pc, TypeNode type, V array, V index, V value, NonNullDomain<V> data)
 371                 {
 372                         return AssumeNonNull (array, data);
 373                 }
 374
 375                 public override NonNullDomain<V> StoreField (APC pc, Field field, V obj, V value, NonNullDomain<V> data)
 376                 {
 377                         return AssumeNonNull (obj, data);
 378                 }
 379
 380                 private bool TryFindOldState (APC pc, out NonNullDomain<V> old)
 381                 {
 382                         if (pc.SubroutineContext.AsEnumerable().Any (edge => edge.Tag.Is (EdgeTag.AfterMask)))
 383                                 return this.callSiteCache.TryGetValue (pc, out old);
 384
 385                         return false.Without (out old);
 386                 }
 387
 388                 public NonNullDomain<V> InitialValue (Func<V, int> keyConverter)
 389                 {
 390                         return new NonNullDomain<V> (new SetDomain<V> (keyConverter), new SetDomain<V> (keyConverter));
 391                 }
 392
 393                 #region Implementation of IMethodResult<Variable>
 394                 public IMethodAnalysis MethodAnalysis { get; set; }
 395
 396                 public void ValidateImplicitAssertions (IFactQuery<BoxedExpression, V> facts, List<string> proofResults)
 397                 {
 398                 }
 399
 400                 public IFactQuery<BoxedExpression, V> FactQuery
 401                 {
 402                         get { return new SimpleLogicInference<E, V> (ContextProvider, this, this.method_driver.BasicFacts.IsUnreachable); }
 403                 }
 404
 405         public FlatDomain<bool> ValidateExplicitAssertion(APC pc, V value)
 406                 {
 407                         NonNullDomain<V> domain;
 408                         if (PreStateLookup (pc, out domain) && !domain.NonNulls.IsBottom) {
 409                                 IExpressionContext<E, V> exprCtx = ContextProvider.ExpressionContext;
 410                 return exprCtx.Decode<bool, FlatDomain<bool>, ExpressionAssertDischarger<E, V>>(exprCtx.Refine(pc, value), new ExpressionAssertDischarger<E, V>(this, pc), true);
 411                         }
 412                         return ProofOutcome.Bottom;
 413                 }
 414
 415                 private bool PreStateLookup (APC pc, out NonNullDomain<V> domain)
 416                 {
 417                         return this.fix_point_info.PreStateLookup (pc, out domain);
 418                 }
 419                 #endregion
 420                 }
 421 }