mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Numerical/EvaluateExpressionVisitor.cs

   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
  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
  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
  78                 public override TInterval VisitConstant (TExpr expr, Counter<TEnv> data)
  79                 {
  80                         return constToIntv.Visit (expr, data.Env.Context);
  81                 }
  82
  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
  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
  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
  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
 103                 public override TInterval VisitEqual (TExpr left, TExpr right, TExpr original, Counter<TEnv> data)
 104                 {
 105                         return DefaultComparisons (left, right, data);
 106                 }
 107
 108                 public override TInterval VisitLessThan (TExpr left, TExpr right, TExpr original, Counter<TEnv> data)
 109                 {
 110                         return DefaultComparisons (left, right, data);
 111                 }
 112
 113                 public override TInterval VisitGreaterEqualThan (TExpr left, TExpr right, TExpr original,
 114                                                                  Counter<TEnv> data)
 115                 {
 116                         return DefaultComparisons (left, right, data);
 117                 }
 118
 119                 public override TInterval VisitLessEqualThan (TExpr left, TExpr right, TExpr original,
 120                                                               Counter<TEnv> data)
 121                 {
 122                         return DefaultComparisons (left, right, data);
 123                 }
 124
 125                 public override TInterval VisitGreaterThan (TExpr left, TExpr right, TExpr original, Counter<TEnv> data)
 126                 {
 127                         return DefaultComparisons (left, right, data);
 128                 }
 129
 130                 public override TInterval VisitUnknown (TExpr expr, Counter<TEnv> data)
 131                 {
 132                         occurences.Add (expr);
 133
 134                         return Default (data);
 135                 }
 136
 137                 protected override TInterval Default (Counter<TEnv> data)
 138                 {
 139                         return data.Env.Context.TopValue;
 140                 }
 141
 142                 delegate TInterval BinaryEvaluator (Counter<TEnv> env, TInterval left, TInterval right);
 143
 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
 155                 TInterval DefaultComparisons (TExpr left, TExpr right, Counter<TEnv> data)
 156                 {
 157                         occurences.Add (left, right);
 158
 159                         return Default (data);
 160                 }
 161
 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
 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
 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
 202                         public void Add (TExpr e)
 203                         {
 204                                 Add (decoder.UnderlyingVariable (e));
 205                         }
 206
 207                         public void Add (params TExpr[] exprs)
 208                         {
 209                                 foreach (var expr in exprs)
 210                                         Add (expr);
 211                         }
 212
 213                         public override string ToString ()
 214                         {
 215                                 return occurences.ToString ();
 216                         }
 217                 }
 218                 }
 219 }