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

   1 //
   2 // IntervalEnvironmentBase.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 using System.IO;
  32
  33 using Mono.CodeContracts.Static.DataStructures;
  34 using Mono.CodeContracts.Static.Lattices;
  35
  36 namespace Mono.CodeContracts.Static.Analysis.Numerical {
  37         abstract class IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> : IIntervalEnvironment<TVar, TExpr, TInterval, TNumeric>,
  38                                                                                    IEnvironmentDomain<IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric>, TVar, TExpr>
  39                 where TInterval : IntervalBase<TInterval, TNumeric>
  40                 where TVar : IEquatable<TVar> {
  41                 public abstract IntervalAssumerBase<TVar, TExpr, TInterval, TNumeric> Assumer { get; }
  42                 public abstract IntervalContextBase<TInterval, TNumeric> Context { get; }
  43
  44                 public readonly IExpressionDecoder<TVar, TExpr> Decoder;
  45                 readonly EnvironmentDomain<TVar, TInterval> vars_to_intervals;
  46
  47                 public IEnumerable<TVar> Variables { get { return vars_to_intervals.Keys; } }
  48
  49                 protected IntervalEnvironmentBase
  50                         (IExpressionDecoder<TVar, TExpr> decoder,
  51                          EnvironmentDomain<TVar, TInterval> varsToInterval)
  52                 {
  53                         Decoder = decoder;
  54                         vars_to_intervals = varsToInterval;
  55                 }
  56
  57                 protected IntervalEnvironmentBase (IExpressionDecoder<TVar, TExpr> decoder)
  58                         : this (decoder, EnvironmentDomain<TVar, TInterval>.TopValue (null))
  59                 {
  60                 }
  61
  62                 public TInterval Eval (TExpr expr)
  63                 {
  64                         int intValue;
  65                         if (Decoder.IsConstantInt (expr, out intValue))
  66                                 return Context.For (intValue);
  67
  68                         var evaluator = new EvaluateExpressionVisitor<IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric>, TVar, TExpr, TInterval, TNumeric> (Decoder);
  69                         var interval = evaluator.Visit (expr, new Counter<IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric>> (this));
  70
  71                         if (evaluator.DuplicatedOccurences.Length () >= 1) {
  72                                 var noDuplicates = true;
  73                                 TInterval result = null;
  74                                 foreach (var var in evaluator.DuplicatedOccurences.AsEnumerable ()) {
  75                                         TInterval intv;
  76                                         if (TryGetValue (var, out intv) && intv.IsFinite &&
  77                                             Context.IsGreaterEqualThanZero (intv.LowerBound)) {
  78                                                 var extreme = EvalWithExtremes (expr, var, intv);
  79                                                 if (noDuplicates) {
  80                                                         noDuplicates = false;
  81                                                         result = extreme;
  82                                                 }
  83                                                 else
  84                                                         result = result.Join (extreme);
  85                                         }
  86                                 }
  87
  88                                 if (!noDuplicates)
  89                                         interval = result;
  90                         }
  91
  92                         return interval;
  93                 }
  94
  95                 public TInterval Eval (TVar var)
  96                 {
  97                         TInterval intv;
  98                         if (TryGetValue (var, out intv))
  99                                 return intv;
 100
 101                         return Context.TopValue;
 102                 }
 103
 104                 /// <summary>
 105                 /// Evaluates expression with variable equal to var's lowerbound or upperbound.
 106                 /// </summary>
 107                 /// <param name="expr"></param>
 108                 /// <param name="var"></param>
 109                 /// <param name="intv"></param>
 110                 /// <returns></returns>
 111                 TInterval EvalWithExtremes (TExpr expr, TVar var, TInterval intv)
 112                 {
 113                         var evaluator = new EvaluateExpressionVisitor<IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric>, TVar, TExpr, TInterval, TNumeric> (Decoder);
 114
 115                         var envLowerBound = With (var, Context.For (intv.LowerBound));
 116                         // replace current intv with it's only lowerbound
 117                         var withLowerBound = evaluator.Visit (expr, new Counter<IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric>> (envLowerBound));
 118
 119                         var envUpperBound = With (var, Context.For (intv.UpperBound));
 120                         // replace current intv with it's only upperBound
 121                         var withUpperBound = evaluator.Visit (expr, new Counter<IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric>> (envUpperBound));
 122
 123                         return withLowerBound.Join (withUpperBound);
 124                 }
 125
 126                 public string ToString (TExpr expr)
 127                 {
 128                         if (IsBottom)
 129                                 return "_|_";
 130                         if (IsTop)
 131                                 return "Top";
 132
 133                         var list = new List<string> ();
 134                         foreach (var variable in Variables) {
 135                                 var intv = vars_to_intervals[variable];
 136                                 if (!intv.IsTop) {
 137                                         var name = Decoder != null
 138                                                            ? Decoder.NameOf (variable)
 139                                                            : variable.ToString ();
 140                                         list.Add (name + ": " + intv);
 141                                 }
 142                         }
 143                         list.Sort ();
 144                         return string.Join (", ", list);
 145                 }
 146
 147                 public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> AssumeTrue (TExpr guard)
 148                 {
 149                         Assumer.AssumeNotEqualToZero (Decoder.UnderlyingVariable (guard), this);
 150                         return new IntervalTestVisitor (Decoder).VisitTrue (guard, this);
 151                 }
 152
 153                 public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> AssumeFalse (TExpr guard)
 154                 {
 155                         return Assumer.AssumeEqualToZero (Decoder.UnderlyingVariable (guard), this);
 156                 }
 157
 158                 public FlatDomain<bool> CheckIfHolds (TExpr expr)
 159                 {
 160                         return FlatDomain<bool>.TopValue;
 161                 }
 162
 163                 public bool Contains (TVar v)
 164                 {
 165                         return vars_to_intervals.Contains (v);
 166                 }
 167
 168                 public bool TryGetValue (TVar v, out TInterval interval)
 169                 {
 170                         return vars_to_intervals.TryGetValue (v, out interval);
 171                 }
 172
 173                 public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> With (TVar var, TInterval interval)
 174                 {
 175                         return NewInstance (vars_to_intervals.With (var, interval));
 176                 }
 177
 178                 public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> RefineVariable (TVar var, TInterval interval)
 179                 {
 180                         TInterval current;
 181                         if (TryGetValue (var, out current))
 182                                 interval = interval.Meet (current);
 183
 184                         if (interval.IsBottom)
 185                                 return Bottom;
 186
 187                         return With (var, interval);
 188                 }
 189
 190                 #region Implementation of IAbstractDomain<T>
 191
 192                 public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> Top { get { return NewInstance (EnvironmentDomain<TVar, TInterval>.TopValue (null)); } }
 193
 194                 public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> Bottom { get { return NewInstance (EnvironmentDomain<TVar, TInterval>.BottomValue ()); } }
 195
 196                 public bool IsTop { get { return vars_to_intervals.IsTop; } }
 197
 198                 public bool IsBottom { get { return vars_to_intervals.IsBottom; } }
 199
 200                 public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> Join (IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> that)
 201                 {
 202                         return NewInstance (vars_to_intervals.Join (that.vars_to_intervals));
 203                 }
 204
 205                 public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> Join (IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> that, bool widen, out bool weaker)
 206                 {
 207                         return NewInstance (vars_to_intervals.Join (that.vars_to_intervals, widen, out weaker));
 208                 }
 209
 210                 public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> Widen (IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> that)
 211                 {
 212                         return NewInstance (vars_to_intervals.Widen (that.vars_to_intervals));
 213                 }
 214
 215                 public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> Meet (IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> that)
 216                 {
 217                         return NewInstance (vars_to_intervals.Meet (that.vars_to_intervals));
 218                 }
 219
 220                 public bool LessEqual (IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> that)
 221                 {
 222                         return vars_to_intervals.LessEqual (that.vars_to_intervals);
 223                 }
 224
 225                 public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> ImmutableVersion ()
 226                 {
 227                         return this;
 228                 }
 229
 230                 public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> Clone ()
 231                 {
 232                         return this;
 233                 }
 234
 235                 public void Dump (TextWriter tw)
 236                 {
 237                         vars_to_intervals.Dump (tw);
 238                 }
 239
 240                 #endregion
 241
 242                 protected abstract IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> NewInstance (EnvironmentDomain<TVar, TInterval> varsToIntervals);
 243
 244                 class IntervalTestVisitor {
 245                         readonly IntervalAssumeTrueVisitor<TVar, TExpr, TInterval, TNumeric> true_visitor;
 246                         readonly IntervalAssumeFalseVisitor<TVar, TExpr, TInterval, TNumeric> false_visitor;
 247
 248                         public IntervalTestVisitor (IExpressionDecoder<TVar, TExpr> decoder)
 249                         {
 250                                 true_visitor =
 251                                         new IntervalAssumeTrueVisitor<TVar, TExpr, TInterval, TNumeric> (decoder);
 252                                 false_visitor =
 253                                         new IntervalAssumeFalseVisitor<TVar, TExpr, TInterval, TNumeric> (decoder);
 254
 255                                 true_visitor.FalseVisitor = false_visitor;
 256                                 false_visitor.TrueVisitor = true_visitor;
 257                         }
 258
 259                         public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> VisitTrue (TExpr guard, IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> data)
 260                         {
 261                                 return true_visitor.Visit (guard, data);
 262                         }
 263
 264                         public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> VisitFalse (TExpr guard, IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> data)
 265                         {
 266                                 return false_visitor.Visit (guard, data);
 267                         }
 268                 }
 269
 270                 public abstract IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> AssumeVariableIn (TVar var, Interval interval);
 271
 272                 public IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric> AssumeLessEqualThan (TExpr left, TExpr right)
 273                 {
 274                         return Assumer.AssumeLessEqualThan (left, right, this);
 275                 }
 276
 277                 INumericalEnvironmentDomain<TVar, TExpr> IAbstractDomain<INumericalEnvironmentDomain<TVar, TExpr>>.Top { get { return Top; } }
 278
 279                 INumericalEnvironmentDomain<TVar, TExpr> IAbstractDomain<INumericalEnvironmentDomain<TVar, TExpr>>.Bottom { get { return Bottom; } }
 280
 281                 INumericalEnvironmentDomain<TVar, TExpr> IAbstractDomain<INumericalEnvironmentDomain<TVar, TExpr>>.Join (INumericalEnvironmentDomain<TVar, TExpr> that)
 282                 {
 283                         return Join (that as IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric>);
 284                 }
 285
 286                 INumericalEnvironmentDomain<TVar, TExpr> IAbstractDomain<INumericalEnvironmentDomain<TVar, TExpr>>.Join
 287                         (INumericalEnvironmentDomain<TVar, TExpr> that, bool widen, out bool weaker)
 288                 {
 289                         return Join (that as IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric>, widen,
 290                                      out weaker);
 291                 }
 292
 293                 INumericalEnvironmentDomain<TVar, TExpr> IAbstractDomain<INumericalEnvironmentDomain<TVar, TExpr>>.Widen (INumericalEnvironmentDomain<TVar, TExpr> that)
 294                 {
 295                         return Widen (that as IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric>);
 296                 }
 297
 298                 INumericalEnvironmentDomain<TVar, TExpr> IAbstractDomain<INumericalEnvironmentDomain<TVar, TExpr>>.Meet (INumericalEnvironmentDomain<TVar, TExpr> that)
 299                 {
 300                         return Meet (that as IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric>);
 301                 }
 302
 303                 bool IAbstractDomain<INumericalEnvironmentDomain<TVar, TExpr>>.LessEqual (INumericalEnvironmentDomain<TVar, TExpr> that)
 304                 {
 305                         return LessEqual (that as IntervalEnvironmentBase<TVar, TExpr, TInterval, TNumeric>);
 306                 }
 307
 308                 INumericalEnvironmentDomain<TVar, TExpr> IAbstractDomain<INumericalEnvironmentDomain<TVar, TExpr>>.ImmutableVersion ()
 309                 {
 310                         return ImmutableVersion ();
 311                 }
 312
 313                 INumericalEnvironmentDomain<TVar, TExpr> IAbstractDomain<INumericalEnvironmentDomain<TVar, TExpr>>.Clone ()
 314                 {
 315                         return Clone ();
 316                 }
 317
 318                 INumericalEnvironmentDomain<TVar, TExpr> IEnvironmentDomain<INumericalEnvironmentDomain<TVar, TExpr>, TVar, TExpr>.AssumeTrue (TExpr guard)
 319                 {
 320                         return AssumeTrue (guard);
 321                 }
 322
 323                 INumericalEnvironmentDomain<TVar, TExpr> IEnvironmentDomain<INumericalEnvironmentDomain<TVar, TExpr>, TVar, TExpr>.AssumeFalse (TExpr guard)
 324                 {
 325                         return AssumeFalse (guard);
 326                 }
 327
 328                 INumericalEnvironmentDomain<TVar, TExpr> INumericalEnvironmentDomain<TVar, TExpr>.AssumeVariableIn (TVar var, Interval interval)
 329                 {
 330                         return AssumeVariableIn (var, interval);
 331                 }
 332
 333                 INumericalEnvironmentDomain<TVar, TExpr> INumericalEnvironmentDomain<TVar, TExpr>.AssumeLessEqualThan (TExpr left, TExpr right)
 334                 {
 335                         return AssumeLessEqualThan (left, right);
 336                 }
 337                 }
 338 }