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 Analysis(IMethodDriver<E, V> mdriver)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 GetVisitor()71 public IILVisitor<APC, V, V, NonNullDomain<V>, NonNullDomain<V>> GetVisitor () 72 { 73 return this; 74 } 75 Join(Pair<APC, APC> edge, NonNullDomain<V> newstate, NonNullDomain<V> prevstate, out bool weaker, bool widen)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 ImmutableVersion(NonNullDomain<V> state)87 public NonNullDomain<V> ImmutableVersion (NonNullDomain<V> state) 88 { 89 return state; 90 } 91 MutableVersion(NonNullDomain<V> state)92 public NonNullDomain<V> MutableVersion (NonNullDomain<V> state) 93 { 94 return state; 95 } 96 EdgeConversion(APC from, APC to, bool isJoinPoint, IImmutableMap<V, Sequence<V>> data, NonNullDomain<V> state)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 IsBottom(APC pc, NonNullDomain<V> state)123 public bool IsBottom (APC pc, NonNullDomain<V> state) 124 { 125 return state.NonNulls.IsBottom; 126 } 127 SaveFixPointInfo(IFixPointInfo<APC, NonNullDomain<V>> fixPointInfo)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 Dump(Pair<NonNullDomain<V>, TextWriter> pair)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 IsNull(APC pc, V variable)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 IsNonNull(APC pc, V variable)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 IsUnreachable(APC pc)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 DefaultVisit(APC pc, NonNullDomain<V> data)190 public override NonNullDomain<V> DefaultVisit (APC pc, NonNullDomain<V> data) 191 { 192 return data; 193 } 194 AssumeNonNull(V dest, NonNullDomain<V> domain)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 AssumeNull(V dest, NonNullDomain<V> before)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 Assert(APC pc, EdgeTag tag, V condition, NonNullDomain<V> data)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 Assume(APC pc, EdgeTag tag, V condition, NonNullDomain<V> data)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 Unary(APC pc, UnaryOperator op, bool unsigned, V dest, V source, NonNullDomain<V> data)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 Call(APC pc, Method method, bool virt, TypeList extraVarargs, V dest, ArgList args, NonNullDomain<V> data)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 CastClass(APC pc, TypeNode type, V dest, V obj, NonNullDomain<V> data)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 Entry(APC pc, Method method, NonNullDomain<V> data)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 LoadStack(APC pc, int offset, V dest, V source, bool isOld, NonNullDomain<V> data)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 Isinst(APC pc, TypeNode type, V dest, V obj, NonNullDomain<V> data)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 LoadArgAddress(APC pc, Parameter argument, bool isOld, V dest, NonNullDomain<V> data)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 LoadConst(APC pc, TypeNode type, object constant, V dest, NonNullDomain<V> data)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 LoadElement(APC pc, TypeNode type, V dest, V array, V index, NonNullDomain<V> data)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 LoadField(APC pc, Field field, V dest, V obj, NonNullDomain<V> data)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 LoadFieldAddress(APC pc, Field field, V dest, V obj, NonNullDomain<V> data)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 LoadStaticFieldAddress(APC pc, Field field, V dest, NonNullDomain<V> data)350 public override NonNullDomain<V> LoadStaticFieldAddress (APC pc, Field field, V dest, NonNullDomain<V> data) 351 { 352 return AssumeNonNull (dest, data); 353 } 354 LoadLength(APC pc, V dest, V array, NonNullDomain<V> data)355 public override NonNullDomain<V> LoadLength (APC pc, V dest, V array, NonNullDomain<V> data) 356 { 357 return AssumeNonNull (array, data); 358 } 359 NewArray(APC pc, TypeNode type, V dest, ArgList lengths, NonNullDomain<V> data)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 NewObj(APC pc, Method ctor, V dest, ArgList args, NonNullDomain<V> data)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 StoreElement(APC pc, TypeNode type, V array, V index, V value, NonNullDomain<V> data)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 StoreField(APC pc, Field field, V obj, V value, NonNullDomain<V> data)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 TryFindOldState(APC pc, out NonNullDomain<V> old)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 InitialValue(Func<V, int> keyConverter)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 ValidateImplicitAssertions(IFactQuery<BoxedExpression, V> facts, List<string> proofResults)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 ValidateExplicitAssertion(APC pc, V value)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 PreStateLookup(APC pc, out NonNullDomain<V> domain)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 } 422