1 //
2 // ExpressionAssertDischarger.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 Mono.CodeContracts.Static.AST;
31 using Mono.CodeContracts.Static.AST.Visitors;
32 using Mono.CodeContracts.Static.ControlFlow;
33 using Mono.CodeContracts.Static.Lattices;
34 
35 namespace Mono.CodeContracts.Static.Analysis.NonNull {
36 	struct ExpressionAssertDischarger<E, V>
37         : ISymbolicExpressionVisitor<E, E, V, bool, FlatDomain<bool>>
38 		where E : IEquatable<E>
39 		where V : IEquatable<V> {
40 		private readonly Analysis<E, V> analysis;
41 		private readonly APC pc;
42 
ExpressionAssertDischargerMono.CodeContracts.Static.Analysis.NonNull.ExpressionAssertDischarger43 		public ExpressionAssertDischarger(Analysis<E, V> analysis, APC pc)
44 		{
45 			this.analysis = analysis;
46 			this.pc = pc;
47 		}
48 
49 		private IExpressionContextProvider<E, V> ContextProvider
50 		{
51 			get { return this.analysis.ContextProvider; }
52 		}
53 
54 		#region Implementation of IExpressionILVisitor<Expression,Expression,Variable,bool,ProofOutcome>
RecurseMono.CodeContracts.Static.Analysis.NonNull.ExpressionAssertDischarger55         private FlatDomain<bool> Recurse(bool polarity, E expr)
56 		{
57             return this.ContextProvider.ExpressionContext.Decode<bool, FlatDomain<bool>, ExpressionAssertDischarger<E, V>>(expr, this, polarity);
58 		}
59 
BinaryMono.CodeContracts.Static.Analysis.NonNull.ExpressionAssertDischarger60         public FlatDomain<bool> Binary(E orig, BinaryOperator op, V dest, E operand1, E operand2, bool polarity)
61 		{
62 			switch (op) {
63 			case BinaryOperator.Ceq:
64 			case BinaryOperator.Cobjeq:
65 				if (this.ContextProvider.ExpressionContext.IsZero (operand2) || this.ContextProvider.ExpressionContext.IsZero (operand1))
66 					return this.Recurse (!polarity, operand1);
67 				return ProofOutcome.Top;
68 			case BinaryOperator.Cne_Un:
69 				if (this.ContextProvider.ExpressionContext.IsZero(operand2) || this.ContextProvider.ExpressionContext.IsZero(operand1))
70 					return this.Recurse (polarity, operand1);
71 				return ProofOutcome.Top;
72 			default:
73 				return this.SymbolicConstant (orig, this.ContextProvider.ExpressionContext.Unrefine (orig), polarity);
74 			}
75 		}
76 
IsinstMono.CodeContracts.Static.Analysis.NonNull.ExpressionAssertDischarger77         public FlatDomain<bool> Isinst(E orig, TypeNode type, V dest, E obj, bool polarity)
78 		{
79 			if (!polarity)
80 				return this.analysis.IsNull (this.pc, dest);
81             FlatDomain<bool> outcome = this.analysis.IsNonNull(this.pc, dest);
82 
83 			return outcome.IsTrue() ? outcome : this.Recurse (true, obj);
84 		}
85 
LoadNullMono.CodeContracts.Static.Analysis.NonNull.ExpressionAssertDischarger86         public FlatDomain<bool> LoadNull(E orig, V dest, bool polarity)
87 		{
88 			return polarity ? ProofOutcome.False : ProofOutcome.True;
89 		}
90 
LoadConstMono.CodeContracts.Static.Analysis.NonNull.ExpressionAssertDischarger91         public FlatDomain<bool> LoadConst(E orig, TypeNode type, object constant, V dest, bool polarity)
92 		{
93 			var isConstantEqualZero = constant is int && (int) constant == 0;
94 
95 			return (isConstantEqualZero != polarity) ? ProofOutcome.True : ProofOutcome.False;
96 		}
97 
SizeofMono.CodeContracts.Static.Analysis.NonNull.ExpressionAssertDischarger98         public FlatDomain<bool> Sizeof(E pc, TypeNode type, V dest, bool polarity)
99 		{
100 			return polarity ? ProofOutcome.True : ProofOutcome.False;
101 		}
102 
UnaryMono.CodeContracts.Static.Analysis.NonNull.ExpressionAssertDischarger103         public FlatDomain<bool> Unary(E orig, UnaryOperator op, bool unsigned, V dest, E source, bool polarity)
104 		{
105 			switch (op) {
106 			case UnaryOperator.Conv_i:
107 			case UnaryOperator.Conv_i1:
108 			case UnaryOperator.Conv_i2:
109 			case UnaryOperator.Conv_i4:
110 			case UnaryOperator.Conv_i8:
111 			case UnaryOperator.Conv_u:
112 			case UnaryOperator.Conv_u1:
113 			case UnaryOperator.Conv_u2:
114 			case UnaryOperator.Conv_u4:
115 			case UnaryOperator.Conv_u8:
116 				return this.Recurse (polarity, source);
117 			case UnaryOperator.Neg:
118 				return this.Recurse(polarity, source);
119 			case UnaryOperator.Not:
120 				return this.Recurse(!polarity, source);
121 			default:
122 				return this.SymbolicConstant (orig, this.ContextProvider.ExpressionContext.Unrefine (orig), polarity);
123 			}
124 		}
125 		#endregion
126 
127 		#region Implementation of ISymbolicExpressionVisitor<Expression,Expression,Variable,bool,ProofOutcome>
SymbolicConstantMono.CodeContracts.Static.Analysis.NonNull.ExpressionAssertDischarger128         public FlatDomain<bool> SymbolicConstant(E pc, V variable, bool polarity)
129 		{
130 			return polarity ? this.analysis.IsNonNull (this.pc, variable) : this.analysis.IsNull(this.pc, variable);
131 		}
132 		#endregion
133 	}
134 }