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