1 // 2 // EvaluateExpressionVisitor.cs 3 // 4 // Authors: 5 // Alexander Chebaturkin (chebaturkin@gmail.com) 6 // 7 // Copyright (C) 2012 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 32 using Mono.CodeContracts.Static.DataStructures; 33 34 namespace Mono.CodeContracts.Static.Analysis.Numerical { 35 class EvaluateExpressionVisitor<TEnv, TVar, TExpr, TInterval, TNumeric> : 36 GenericExpressionVisitor<Counter<TEnv>, TInterval, TVar, TExpr> 37 where TEnv : IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> 38 where TVar : IEquatable<TVar> 39 where TInterval : IntervalBase<TInterval, TNumeric> { 40 readonly 41 ConstToIntervalEvaluator 42 <IntervalContextBase<TInterval, TNumeric>, TVar, TExpr, TInterval, TNumeric> constToIntv; 43 44 readonly VariableOccurences occurences; 45 46 public Sequence<TVar> DuplicatedOccurences { get { return occurences.Duplicated; } } 47 EvaluateExpressionVisitor(IExpressionDecoder<TVar, TExpr> decoder)48 public EvaluateExpressionVisitor (IExpressionDecoder<TVar, TExpr> decoder) 49 : base (decoder) 50 { 51 occurences = new VariableOccurences (decoder); 52 constToIntv = 53 new ConstToIntervalEvaluator 54 <IntervalContextBase<TInterval, TNumeric>, TVar, TExpr, TInterval, TNumeric> ( 55 decoder); 56 } 57 Visit(TExpr expr, Counter<TEnv> data)58 public override TInterval Visit (TExpr expr, Counter<TEnv> data) 59 { 60 if (data.Count >= 10) // to avoid recursion if any 61 return Default (data); 62 63 var intv = base.Visit (expr, data.Incremented ()); 64 if (intv == null) 65 return Default (data); 66 67 intv = RefineWithTypeRanges (intv, expr, data.Env); 68 69 var var = Decoder.UnderlyingVariable (expr); 70 71 TInterval current; 72 if (data.Env.TryGetValue (var, out current)) 73 intv = intv.Meet (current); 74 75 return intv; 76 } 77 VisitConstant(TExpr expr, Counter<TEnv> data)78 public override TInterval VisitConstant (TExpr expr, Counter<TEnv> data) 79 { 80 return constToIntv.Visit (expr, data.Env.Context); 81 } 82 VisitAddition(TExpr left, TExpr right, TExpr original, Counter<TEnv> data)83 public override TInterval VisitAddition (TExpr left, TExpr right, TExpr original, Counter<TEnv> data) 84 { 85 return DefaultBinary (left, right, data, (d, l, r) => d.Env.Context.Add (l, r)); 86 } 87 VisitDivision(TExpr left, TExpr right, TExpr original, Counter<TEnv> data)88 public override TInterval VisitDivision (TExpr left, TExpr right, TExpr original, Counter<TEnv> data) 89 { 90 return DefaultBinary (left, right, data, (d, l, r) => d.Env.Context.Div (l, r)); 91 } 92 VisitMultiply(TExpr left, TExpr right, TExpr original, Counter<TEnv> data)93 public override TInterval VisitMultiply (TExpr left, TExpr right, TExpr original, Counter<TEnv> data) 94 { 95 return DefaultBinary (left, right, data, (d, l, r) => d.Env.Context.Mul (l, r)); 96 } 97 VisitSubtraction(TExpr left, TExpr right, TExpr original, Counter<TEnv> data)98 public override TInterval VisitSubtraction (TExpr left, TExpr right, TExpr original, Counter<TEnv> data) 99 { 100 return DefaultBinary (left, right, data, (d, l, r) => d.Env.Context.Sub (l, r)); 101 } 102 VisitEqual(TExpr left, TExpr right, TExpr original, Counter<TEnv> data)103 public override TInterval VisitEqual (TExpr left, TExpr right, TExpr original, Counter<TEnv> data) 104 { 105 return DefaultComparisons (left, right, data); 106 } 107 VisitLessThan(TExpr left, TExpr right, TExpr original, Counter<TEnv> data)108 public override TInterval VisitLessThan (TExpr left, TExpr right, TExpr original, Counter<TEnv> data) 109 { 110 return DefaultComparisons (left, right, data); 111 } 112 VisitGreaterEqualThan(TExpr left, TExpr right, TExpr original, Counter<TEnv> data)113 public override TInterval VisitGreaterEqualThan (TExpr left, TExpr right, TExpr original, 114 Counter<TEnv> data) 115 { 116 return DefaultComparisons (left, right, data); 117 } 118 VisitLessEqualThan(TExpr left, TExpr right, TExpr original, Counter<TEnv> data)119 public override TInterval VisitLessEqualThan (TExpr left, TExpr right, TExpr original, 120 Counter<TEnv> data) 121 { 122 return DefaultComparisons (left, right, data); 123 } 124 VisitGreaterThan(TExpr left, TExpr right, TExpr original, Counter<TEnv> data)125 public override TInterval VisitGreaterThan (TExpr left, TExpr right, TExpr original, Counter<TEnv> data) 126 { 127 return DefaultComparisons (left, right, data); 128 } 129 VisitUnknown(TExpr expr, Counter<TEnv> data)130 public override TInterval VisitUnknown (TExpr expr, Counter<TEnv> data) 131 { 132 occurences.Add (expr); 133 134 return Default (data); 135 } 136 Default(Counter<TEnv> data)137 protected override TInterval Default (Counter<TEnv> data) 138 { 139 return data.Env.Context.TopValue; 140 } 141 BinaryEvaluator(Counter<TEnv> env, TInterval left, TInterval right)142 delegate TInterval BinaryEvaluator (Counter<TEnv> env, TInterval left, TInterval right); 143 DefaultBinary(TExpr left, TExpr right, Counter<TEnv> data, BinaryEvaluator binop)144 TInterval DefaultBinary (TExpr left, TExpr right, Counter<TEnv> data, BinaryEvaluator binop) 145 { 146 occurences.Add (left, right); 147 148 var incremented = data.Incremented (); 149 var leftIntv = Visit (left, incremented); 150 var rightIntv = Visit (right, incremented); 151 152 return binop (data, leftIntv, rightIntv); 153 } 154 DefaultComparisons(TExpr left, TExpr right, Counter<TEnv> data)155 TInterval DefaultComparisons (TExpr left, TExpr right, Counter<TEnv> data) 156 { 157 occurences.Add (left, right); 158 159 return Default (data); 160 } 161 RefineWithTypeRanges(TInterval intv, TExpr expr, TEnv env)162 TInterval RefineWithTypeRanges (TInterval intv, TExpr expr, TEnv env) 163 { 164 switch (Decoder.TypeOf (expr)) { 165 case ExpressionType.Int32: 166 return env.Context.ApplyConversion (ExpressionOperator.ConvertToInt32, intv); 167 case ExpressionType.Bool: 168 return env.Context.ApplyConversion (ExpressionOperator.ConvertToInt32, intv); 169 default: 170 return intv; 171 } 172 } 173 174 class VariableOccurences { 175 readonly Dictionary<TVar, int> occurences; 176 177 readonly IExpressionDecoder<TVar, TExpr> decoder; 178 179 Sequence<TVar> duplicated; 180 VariableOccurences(IExpressionDecoder<TVar, TExpr> decoder)181 public VariableOccurences (IExpressionDecoder<TVar, TExpr> decoder) 182 { 183 this.decoder = decoder; 184 occurences = new Dictionary<TVar, int> (); 185 duplicated = Sequence<TVar>.Empty; 186 } 187 188 public Sequence<TVar> Duplicated { get { return duplicated; } } 189 Add(TVar var)190 void Add (TVar var) 191 { 192 int cnt; 193 if (!occurences.TryGetValue (var, out cnt)) 194 cnt = 0; 195 196 occurences[var] = cnt + 1; 197 198 if (cnt == 1) // if already was occurence 199 duplicated = duplicated.Cons (var); 200 } 201 Add(TExpr e)202 public void Add (TExpr e) 203 { 204 Add (decoder.UnderlyingVariable (e)); 205 } 206 Add(params TExpr[] exprs)207 public void Add (params TExpr[] exprs) 208 { 209 foreach (var expr in exprs) 210 Add (expr); 211 } 212 ToString()213 public override string ToString () 214 { 215 return occurences.ToString (); 216 } 217 } 218 } 219 }