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

   1 //
   2 // Interval.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 using System.Linq;
  33
  34 using Mono.CodeContracts.Static.AST;
  35 using Mono.CodeContracts.Static.DataStructures;
  36 using Mono.CodeContracts.Static.Lattices;
  37 using Mono.CodeContracts.Static.Providers;
  38
  39 namespace Mono.CodeContracts.Static.Analysis.Numerical {
  40         /// <summary>
  41         /// Represents a closed interval of <see cref="Rational"/> values.
  42         /// </summary>
  43         public class Interval : IntervalBase<Interval, Rational>, IEquatable<Interval> {
  44                 static Interval cached_top_value;
  45                 static Interval cached_bottom_value;
  46
  47                 readonly bool is_bottom;
  48                 readonly bool is_top;
  49
  50                 Interval (Rational lowerBound, Rational upperBound)
  51                         : base (lowerBound, upperBound)
  52                 {
  53                         if (lowerBound.IsMinusInfinity && upperBound.IsPlusInfinity ||
  54                             lowerBound.IsMinusInfinity && upperBound.IsMinusInfinity ||
  55                             lowerBound.IsPlusInfinity && upperBound.IsPlusInfinity) {
  56                                 LowerBound = Rational.MinusInfinity;
  57                                 UpperBound = Rational.PlusInfinity;
  58                                 is_top = true;
  59                         }
  60
  61                         is_bottom = LowerBound > UpperBound;
  62                 }
  63
  64                 public static Interval TopValue
  65                 {
  66                         get
  67                         {
  68                                 if (ReferenceEquals (cached_top_value, null))
  69                                         cached_top_value = new Interval (Rational.MinusInfinity, Rational.PlusInfinity);
  70                                 return cached_top_value;
  71                         }
  72                 }
  73
  74                 public static Interval BottomValue
  75                 {
  76                         get
  77                         {
  78                                 if (ReferenceEquals (cached_bottom_value, null))
  79                                         cached_bottom_value = new Interval (Rational.PlusInfinity,
  80                                                                             Rational.MinusInfinity);
  81                                 return cached_bottom_value;
  82                         }
  83                 }
  84
  85                 public override Interval Top { get { return TopValue; } }
  86                 public override Interval Bottom { get { return BottomValue; } }
  87
  88                 public override bool IsTop { get { return is_top; } }
  89                 public override bool IsBottom { get { return is_bottom; } }
  90
  91                 public override bool LessEqual (Interval that)
  92                 {
  93                         bool result;
  94                         if (this.TryTrivialLessEqual (that, out result))
  95                                 return result;
  96
  97                         //less equal <==> is included in
  98                         return LowerBound >= that.LowerBound && UpperBound <= that.UpperBound;
  99                 }
 100
 101                 public bool LessEqual (IEnumerable<Interval> right)
 102                 {
 103                         return right.Any (LessEqual);
 104                 }
 105
 106                 public override Interval Join (Interval that, bool widening, out bool weaker)
 107                 {
 108                         weaker = false;
 109
 110                         return widening ? Widen (that) : Join (that);
 111                 }
 112
 113                 public override Interval Join (Interval that)
 114                 {
 115                         Interval result;
 116                         if (this.TryTrivialJoin (that, out result))
 117                                 return result;
 118
 119                         return For (Rational.Min (LowerBound, that.LowerBound),
 120                                     Rational.Max (UpperBound, that.UpperBound));
 121                 }
 122
 123                 public override Interval Widen (Interval that)
 124                 {
 125                         Interval result;
 126                         if (this.TryTrivialJoin (that, out result))
 127                                 return result;
 128
 129                         return For (LowerBound < that.LowerBound
 130                                             ? ThresholdDB.GetPrevious (LowerBound)
 131                                             : that.LowerBound,
 132                                     UpperBound > that.UpperBound
 133                                             ? ThresholdDB.GetNext (UpperBound)
 134                                             : that.UpperBound);
 135                 }
 136
 137                 public override Interval Meet (Interval that)
 138                 {
 139                         Interval result;
 140                         if (this.TryTrivialMeet (that, out result))
 141                                 return result;
 142
 143                         return For (
 144                                 Rational.Max (LowerBound, that.LowerBound),
 145                                 Rational.Min (UpperBound, that.UpperBound));
 146                 }
 147
 148                 public static Interval For (Rational lowerBound, Rational upperBound)
 149                 {
 150                         return new Interval (lowerBound, upperBound);
 151                 }
 152
 153                 public static Interval For (Rational lowerBound, long upperBound)
 154                 {
 155                         return For (lowerBound, Rational.For (upperBound));
 156                 }
 157
 158                 public static Interval For (long lowerBound, long upperBound)
 159                 {
 160                         return For (Rational.For (lowerBound), Rational.For (upperBound));
 161                 }
 162
 163                 public static Interval For (long lower, Rational upperBound)
 164                 {
 165                         return For (Rational.For (lower), upperBound);
 166                 }
 167
 168                 public static Interval For (Rational value)
 169                 {
 170                         return For (value, value);
 171                 }
 172
 173                 public static Interval For (long value)
 174                 {
 175                         return For (Rational.For (value));
 176                 }
 177
 178                 public static Interval operator + (Interval l, Interval r)
 179                 {
 180                         if (l.IsBottom || r.IsBottom)
 181                                 return BottomValue;
 182
 183                         Rational lower, upper;
 184                         if (l.IsTop || r.IsTop
 185                             || !Rational.TryAdd (l.LowerBound, r.LowerBound, out lower)
 186                             || !Rational.TryAdd (l.UpperBound, r.UpperBound, out upper))
 187                                 return TopValue;
 188
 189                         return For (lower, upper);
 190                 }
 191
 192                 public static Interval operator - (Interval l, Interval r)
 193                 {
 194                         if (l.IsBottom || r.IsBottom)
 195                                 return BottomValue;
 196
 197                         Rational lower, upper;
 198                         if (l.IsTop || r.IsTop
 199                             || !Rational.TrySubtract (l.LowerBound, r.UpperBound, out lower)
 200                             || !Rational.TrySubtract (l.UpperBound, r.LowerBound, out upper))
 201                                 return TopValue;
 202
 203                         return For (lower, upper);
 204                 }
 205
 206                 public static Interval operator / (Interval l, Interval r)
 207                 {
 208                         if (l.IsBottom || r.IsBottom)
 209                                 return BottomValue;
 210
 211                         Rational a, b, c, d;
 212                         if (l.IsTop || r.IsTop || r.Includes (0)
 213                             || !Rational.TryDivide (l.LowerBound, r.UpperBound, out a)
 214                             || !Rational.TryDivide (l.LowerBound, r.LowerBound, out b)
 215                             || !Rational.TryDivide (l.UpperBound, r.UpperBound, out c)
 216                             || !Rational.TryDivide (l.UpperBound, r.LowerBound, out d))
 217
 218                                 return TopValue;
 219
 220                         var lower = Rational.Min (Rational.Min (a, b), Rational.Min (c, d));
 221                         var upper = Rational.Max (Rational.Max (a, b), Rational.Max (c, d));
 222
 223                         return For (lower, upper);
 224                 }
 225
 226                 public static Interval operator * (Interval l, Interval r)
 227                 {
 228                         if (l.IsBottom || r.IsBottom)
 229                                 return BottomValue;
 230
 231                         Rational lower, upper;
 232                         if (l.IsTop || r.IsTop
 233                             || !Rational.TryMultiply (l.LowerBound, r.LowerBound, out lower)
 234                             || !Rational.TryMultiply (l.UpperBound, r.UpperBound, out upper))
 235                                 return TopValue;
 236
 237                         return For (lower, upper);
 238                 }
 239
 240                 public static Interval operator - (Interval l)
 241                 {
 242                         if (!l.IsNormal ())
 243                                 return l;
 244
 245                         Rational lower;
 246                         Rational upper;
 247                         if (!Rational.TryUnaryMinus (l.UpperBound, out lower) ||
 248                             !Rational.TryUnaryMinus (l.LowerBound, out upper))
 249                                 return TopValue;
 250
 251                         return For (lower, upper);
 252                 }
 253
 254                 public static bool AreConsecutiveIntegers (Interval prev, Interval next)
 255                 {
 256                         if (!prev.IsNormal () || !next.IsNormal () ||
 257                             !prev.UpperBound.IsInteger || !next.LowerBound.IsInteger)
 258                                 return false;
 259
 260                         return prev.UpperBound + Rational.One == next.LowerBound;
 261                 }
 262
 263                 public static Interval ApplyConversion (ExpressionOperator conv, Interval intv)
 264                 {
 265                         if (intv.is_bottom)
 266                                 return intv;
 267
 268                         switch (conv) {
 269                         case ExpressionOperator.ConvertToInt32:
 270                                 return intv.RefineWithTypeRanges (int.MinValue, int.MaxValue);
 271                         default:
 272                                 return intv;
 273                         }
 274                 }
 275
 276                 public bool TryGetSingletonFiniteInt32 (out int value)
 277                 {
 278                         int lower;
 279                         int upper;
 280                         if (IsFiniteAndInt32 (out lower, out upper) && lower == upper)
 281                                 return true.With (lower, out value);
 282
 283                         return false.Without (out value);
 284                 }
 285
 286                 public bool Includes (long x)
 287                 {
 288                         return this.IsNormal () && LowerBound <= x && x <= UpperBound;
 289                 }
 290
 291                 public bool Includes (int x)
 292                 {
 293                         return this.IsNormal () && LowerBound <= x && x <= UpperBound;
 294                 }
 295
 296                 public bool OverlapsWith (Interval that)
 297                 {
 298                         return !Meet (that).IsBottom;
 299                 }
 300
 301                 public bool OnTheLeftOf (Interval that)
 302                 {
 303                         if (!this.IsNormal () || !that.IsNormal ())
 304                                 return false;
 305
 306                         return UpperBound <= that.LowerBound;
 307                 }
 308
 309                 public override Interval ImmutableVersion ()
 310                 {
 311                         return this;
 312                 }
 313
 314                 public override Interval Clone ()
 315                 {
 316                         return this;
 317                 }
 318
 319                 public override bool Equals (object obj)
 320                 {
 321                         if (ReferenceEquals (null, obj))
 322                                 return false;
 323                         if (ReferenceEquals (this, obj))
 324                                 return true;
 325                         return Equals ((Interval) obj);
 326                 }
 327
 328                 public bool Equals (Interval that)
 329                 {
 330                         if (ReferenceEquals (this, that))
 331                                 return true;
 332                         if (ReferenceEquals (that, null))
 333                                 return false;
 334
 335                         return LowerBound == that.LowerBound && UpperBound == that.UpperBound;
 336                 }
 337
 338                 public override int GetHashCode ()
 339                 {
 340                         return (LowerBound.GetHashCode () * 397) ^ UpperBound.GetHashCode ();
 341                 }
 342
 343                 public override void Dump (TextWriter tw)
 344                 {
 345                         tw.WriteLine (ToString ());
 346                 }
 347
 348                 protected override bool IsFiniteBound (Rational n)
 349                 {
 350                         return n.IsInteger;
 351                 }
 352
 353                 bool IsFiniteAndInt32 (out int lower, out int upper)
 354                 {
 355                         if (IsFinite && LowerBound.IsInt32 && UpperBound.IsInt32) {
 356                                 try {
 357                                         lower = (int) LowerBound;
 358                                         upper = (int) UpperBound;
 359                                         return true;
 360                                 }
 361                                 catch (ArithmeticException) {
 362                                 }
 363                         }
 364
 365                         return false.With (0, out lower).
 366                                 With (0, out upper);
 367                 }
 368
 369                 Interval RefineWithTypeRanges (int min, int max)
 370                 {
 371                         var lower = LowerBound.IsInfinity || !LowerBound.IsInRange (min, max)
 372                                             ? Rational.MinusInfinity
 373                                             : LowerBound.PreviousInt32;
 374
 375                         var upper = UpperBound.IsInfinity || !UpperBound.IsInRange (min, max)
 376                                             ? Rational.PlusInfinity
 377                                             : UpperBound.NextInt32;
 378
 379                         return For (lower, upper);
 380                 }
 381
 382                 internal static class Ranges {
 383                         static Interval int8Range;
 384                         static Interval int32Range;
 385                         static Interval int64Range;
 386
 387                         public static Interval Int8Range { get { return int8Range ?? (int8Range = For (sbyte.MinValue, sbyte.MaxValue)); } }
 388                         public static Interval Int32Range { get { return int32Range ?? (int32Range = For (int.MinValue, int.MaxValue)); } }
 389                         public static Interval Int64Range { get { return int64Range ?? (int64Range = For (int.MinValue, int.MaxValue)); } }
 390
 391                         public static Interval GetIntervalForType (TypeNode type, IMetaDataProvider provider)
 392                         {
 393                                 if (provider.Equal (provider.System_Int8, type))
 394                                         return Int8Range;
 395                                 if (provider.Equal (provider.System_Int32, type))
 396                                         return Int32Range;
 397                                 if (provider.Equal (provider.System_Int64, type))
 398                                         return Int64Range;
 399
 400                                 return TopValue;
 401                         }
 402                 }
 403         }
 404 }