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

   1 //
   2 // DisInterval.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 using System.Text;
  34
  35 using Mono.CodeContracts.Static.DataStructures;
  36 using Mono.CodeContracts.Static.Lattices;
  37
  38 namespace Mono.CodeContracts.Static.Analysis.Numerical {
  39         class DisInterval : IntervalBase<DisInterval, Rational> {
  40                 public static readonly DisInterval NotZero =
  41                         For (Sequence<Interval>.From (Interval.For (Rational.MinusInfinity, -1L),
  42                                                       Interval.For (1L, Rational.PlusInfinity)));
  43
  44                 static DisInterval cached_bottom;
  45                 static DisInterval cached_top;
  46
  47                 readonly Sequence<Interval> intervals;
  48                 readonly Interval join_interval;
  49                 readonly State state;
  50
  51                 DisInterval (Interval interval)
  52                         : base (interval.LowerBound, interval.UpperBound)
  53                 {
  54                         var list = Sequence<Interval>.Empty;
  55                         if (interval.IsTop)
  56                                 state = State.Top;
  57                         else if (interval.IsBottom)
  58                                 state = State.Bottom;
  59                         else {
  60                                 state = State.Normal;
  61                                 list = list.Cons (interval);
  62                         }
  63
  64                         intervals = list;
  65                         join_interval = interval;
  66                 }
  67
  68                 DisInterval (Sequence<Interval> intervals)
  69                         : base (Rational.MinusInfinity, Rational.PlusInfinity)
  70                 {
  71                         bool isBottom;
  72                         this.intervals = Normalize (intervals, out isBottom);
  73
  74                         if (isBottom) {
  75                                 join_interval = Interval.BottomValue;
  76                                 state = State.Bottom;
  77
  78                                 return;
  79                         }
  80
  81                         join_interval = JoinAll (intervals);
  82                         if (join_interval.IsBottom)
  83                                 state = State.Bottom;
  84                         else if (join_interval.IsTop)
  85                                 state = intervals.Length () <= 1 ? State.Top : State.Normal;
  86                         else {
  87                                 LowerBound = join_interval.LowerBound;
  88                                 UpperBound = join_interval.UpperBound;
  89                                 state = State.Normal;
  90                         }
  91                 }
  92
  93                 DisInterval (State state)
  94                         : base (Rational.MinusInfinity, Rational.PlusInfinity)
  95                 {
  96                         this.state = state;
  97                         join_interval = state == State.Bottom ? Interval.BottomValue : Interval.TopValue;
  98                         intervals = Sequence<Interval>.Empty;
  99                 }
 100
 101                 public static DisInterval BottomValue { get { return cached_bottom ?? (cached_bottom = new DisInterval (State.Bottom)); } }
 102
 103                 public static DisInterval TopValue { get { return cached_top ?? (cached_top = new DisInterval (State.Top)); } }
 104
 105                 public Interval AsInterval { get { return join_interval; } }
 106
 107                 public override DisInterval Top { get { return TopValue; } }
 108
 109                 public override DisInterval Bottom { get { return BottomValue; } }
 110
 111                 public override bool IsTop { get { return state == State.Top; } }
 112
 113                 public override bool IsBottom { get { return state == State.Bottom; } }
 114
 115                 public bool IsNotZero
 116                 {
 117                         get
 118                         {
 119                                 if (!this.IsNormal ())
 120                                         return false;
 121
 122                                 return intervals.All (intv => !intv.Includes (0));
 123                         }
 124                 }
 125
 126                 public bool IsPositiveOrZero { get { return this.IsNormal () && LowerBound >= 0L; } }
 127
 128                 public override bool Equals (object other)
 129                 {
 130                         if (ReferenceEquals (this, other))
 131                                 return true;
 132                         var that = other as DisInterval;
 133
 134                         if (that == null) {
 135                                 var intv = other as Interval;
 136                                 if (intv == null)
 137                                         return false;
 138
 139                                 return Equals (For (intv));
 140                         }
 141
 142                         if (state == that.state && join_interval.Equals (that.join_interval))
 143                                 return HaveSameIntervals (intervals, that.intervals);
 144
 145                         return false;
 146                 }
 147
 148                 static bool HaveSameIntervals (Sequence<Interval> left, Sequence<Interval> right)
 149                 {
 150                         if (left.Length () != right.Length ())
 151                                 return false;
 152
 153                         var curLeft = left;
 154                         var curRight = right;
 155
 156                         while (!curLeft.IsEmpty ()) {
 157                                 if (!curLeft.Head.Equals (curRight.Head))
 158                                         return false;
 159                                 curLeft = curLeft.Tail;
 160                                 curRight = curRight.Tail;
 161                         }
 162
 163                         return true;
 164                 }
 165
 166                 public override int GetHashCode ()
 167                 {
 168                         unchecked {
 169                                 return (state.GetHashCode () * 397) ^
 170                                        (join_interval != null ? join_interval.GetHashCode () : 0);
 171                         }
 172                 }
 173
 174                 public static Sequence<Interval> Normalize (Sequence<Interval> intervals, out bool isBottom)
 175                 {
 176                         if (intervals.Length () == 0) {
 177                                 isBottom = false;
 178                                 return intervals;
 179                         }
 180
 181                         Comparison<Interval> comparison =
 182                                 (a, b) => a.Equals (b) ? 0 : a.UpperBound <= b.UpperBound ? -1 : 1;
 183
 184                         var intervalList = new List<Interval> (intervals.AsEnumerable ());
 185                         intervalList.Sort (comparison);
 186
 187                         var list = Sequence<Interval>.Empty;
 188
 189                         var bottomCnt = 0;
 190                         Interval last = null;
 191
 192                         foreach (var t in intervalList) {
 193                                 var cur = t;
 194
 195                                 if (cur.IsBottom)
 196                                         bottomCnt++;
 197                                 else if (cur.IsTop) {
 198                                         isBottom = false;
 199                                         return Sequence<Interval>.Empty;
 200                                 }
 201                                 else if (!cur.Equals (last)) {
 202                                         if (last != null) {
 203                                                 while (list != null) {
 204                                                         last = list.Head;
 205                                                         if (Interval.AreConsecutiveIntegers (last, cur)) {
 206                                                                 list = list.Tail;
 207                                                                 cur = last.Join (cur);
 208                                                         }
 209                                                         else if (last.LessEqual (cur))
 210                                                                 list = list.Tail;
 211                                                         else if (last.OverlapsWith (cur)) {
 212                                                                 list = list.Tail;
 213                                                                 cur = cur.Join (last);
 214                                                         }
 215                                                         else
 216                                                                 break;
 217                                                 }
 218                                         }
 219
 220                                         last = cur;
 221                                         list = list.Cons (cur);
 222                                 }
 223                         }
 224
 225                         isBottom = bottomCnt == intervals.Length ();
 226                         return list.Reverse ();
 227                 }
 228
 229                 public static Interval JoinAll (Sequence<Interval> list)
 230                 {
 231                         if (list == null)
 232                                 return Interval.TopValue;
 233
 234                         var res = list.Head;
 235
 236                         var cur = list.Tail;
 237                         while (cur != null) {
 238                                 res = res.Join (cur.Head);
 239                                 cur = cur.Tail;
 240                         }
 241
 242                         return res;
 243                 }
 244
 245                 protected override bool IsFiniteBound (Rational n)
 246                 {
 247                         return !n.IsInfinity;
 248                 }
 249
 250                 public static DisInterval operator + (DisInterval left, DisInterval right)
 251                 {
 252                         return OperatorLifting (left, right, (a, b) => a + b, true);
 253                 }
 254
 255                 public static DisInterval operator * (DisInterval left, DisInterval right)
 256                 {
 257                         return OperatorLifting (left, right, (a, b) => a * b, true);
 258                 }
 259
 260                 public static DisInterval operator / (DisInterval left, DisInterval right)
 261                 {
 262                         return OperatorLifting (left, right, (a, b) => a / b, true);
 263                 }
 264
 265                 public static DisInterval operator - (DisInterval left, DisInterval right)
 266                 {
 267                         return OperatorLifting (left, right, (a, b) => a - b, true);
 268                 }
 269
 270                 public static DisInterval operator - (DisInterval left)
 271                 {
 272                         if (left.IsBottom || left.IsTop)
 273                                 return left;
 274
 275                         return For (left.intervals.Select (i => -i).Reverse ());
 276                 }
 277
 278                 static DisInterval OperatorLifting (DisInterval left, DisInterval right,
 279                                                     Func<Interval, Interval, Interval> binop, bool propagateTop)
 280                 {
 281                         if (left.IsBottom || right.IsBottom)
 282                                 return BottomValue;
 283
 284                         if ((propagateTop && (left.IsTop || right.IsTop)) || (left.IsTop && right.IsTop))
 285                                 return TopValue;
 286
 287                         var intervals = Sequence<Interval>.Empty;
 288
 289                         var hasNoNormals = true;
 290
 291                         if (propagateTop || (left.IsNormal () && right.IsNormal ()))
 292                                 foreach (var leftIntv in left.intervals.AsEnumerable ())
 293                                         foreach (var rightIntv in right.intervals.AsEnumerable ()) {
 294                                                 var res = binop (leftIntv, rightIntv);
 295                                                 if (res.IsTop)
 296                                                         return TopValue;
 297                                                 if (res.IsBottom)
 298                                                         continue;
 299
 300                                                 hasNoNormals = false;
 301                                                 intervals = intervals.Cons (res);
 302                                         }
 303                         else {
 304                                 var notTop = left.IsTop ? right : left;
 305                                 var rightIsTop = !left.IsTop;
 306
 307                                 foreach (var intv in notTop.intervals.AsEnumerable ()) {
 308                                         var res = rightIsTop
 309                                                           ? binop (intv, Interval.TopValue)
 310                                                           : binop (Interval.TopValue, intv);
 311
 312                                         if (res.IsTop)
 313                                                 return TopValue;
 314                                         if (res.IsBottom)
 315                                                 continue;
 316
 317                                         hasNoNormals = false;
 318                                         intervals = intervals.Cons (res);
 319                                 }
 320                         }
 321
 322                         return hasNoNormals ? BottomValue : For (intervals.Reverse ());
 323                 }
 324
 325                 public override DisInterval Widen (DisInterval that)
 326                 {
 327                         if (IsTop || that.IsTop)
 328                                 return TopValue;
 329
 330                         return new DisInterval (Widen (intervals, that.intervals));
 331                 }
 332
 333                 static Sequence<Interval> Widen (Sequence<Interval> left, Sequence<Interval> right)
 334                 {
 335                         if (left.IsEmpty () || right.IsEmpty ())
 336                                 return right;
 337                         if (left.Length () == 1 && right.Length () == 1)
 338                                 return Sequence<Interval>.Singleton (left.Head.Widen (right.Head));
 339
 340                         if (left.Length () == 1) {
 341                                 if (left.Head.LessEqual (right.Head))
 342                                         return right;
 343                                 return Sequence<Interval>.Singleton (left.Head.Widen (right.Head.Join (right.Last ())));
 344                         }
 345
 346                         if (right.Length () == 1)
 347                                 return Sequence<Interval>.Singleton (left.Head.Join (left.Last ()).Widen (right.Head));
 348
 349                         var l = left.Head.Widen (right.Head);
 350                         var r = left.Last ().Widen (right.Last ());
 351
 352                         var list = Sequence<Interval>.Singleton (l);
 353
 354                         var curRight = right.Tail;
 355                         while (curRight != null && curRight.Tail != null) {
 356                                 var curLeft = left.Tail;
 357                                 while (curLeft != null && curRight.Tail != null)
 358                                         if (curLeft.Head.LessEqual (curRight.Head)) {
 359                                                 list = list.Cons (curRight.Head);
 360                                                 break;
 361                                         }
 362                         }
 363                         list = list.Cons (r);
 364
 365                         return list.Reverse ();
 366                 }
 367
 368                 public override DisInterval Meet (DisInterval that)
 369                 {
 370                         DisInterval result;
 371                         if (this.TryTrivialMeet (that, out result))
 372                                 return result;
 373
 374                         bool isBottom;
 375                         var meetIntervals = Meet (intervals, that.intervals, out isBottom);
 376
 377                         if (isBottom)
 378                                 return BottomValue;
 379                         if (meetIntervals.Length () == 0)
 380                                 return TopValue;
 381
 382                         return For (meetIntervals);
 383                 }
 384
 385                 static Sequence<Interval> Meet (Sequence<Interval> left, Sequence<Interval> right, out bool isBottom)
 386                 {
 387                         isBottom = true;
 388                         var list = Sequence<Interval>.Empty;
 389                         foreach (var leftIntv in left.AsEnumerable ()) {
 390                                 foreach (var rightIntv in right.AsEnumerable ()) {
 391                                         var res = leftIntv.Meet (rightIntv);
 392                                         if (res.IsNormal ()) {
 393                                                 isBottom = false;
 394                                                 list = list.Cons (res);
 395                                         }
 396                                 }
 397                         }
 398
 399                         return list.Reverse ();
 400                 }
 401
 402                 public override DisInterval ImmutableVersion ()
 403                 {
 404                         return this;
 405                 }
 406
 407                 public override DisInterval Clone ()
 408                 {
 409                         return this;
 410                 }
 411
 412                 public override void Dump (TextWriter tw)
 413                 {
 414                 }
 415
 416                 public override bool LessEqual (DisInterval that)
 417                 {
 418                         bool result;
 419                         if (this.TryTrivialLessEqual (that, out result))
 420                                 return result;
 421
 422                         if (!join_interval.LessEqual (that.join_interval))
 423                                 return false;
 424
 425                         return intervals.AsEnumerable ().All (inv => that.intervals.Any (inv.LessEqual));
 426                 }
 427
 428                 public override DisInterval Join (DisInterval that, bool widening, out bool weaker)
 429                 {
 430                         weaker = false;
 431                         return Join (that);
 432                 }
 433
 434                 public override DisInterval Join (DisInterval that)
 435                 {
 436                         DisInterval result;
 437                         if (this.TryTrivialJoin (that, out result))
 438                                 return result;
 439
 440                         var join = Join (intervals, that.intervals);
 441                         if (join.IsEmpty ())
 442                                 return TopValue;
 443
 444                         return For (join);
 445                 }
 446
 447                 static Sequence<Interval> Join (Sequence<Interval> left, Sequence<Interval> right)
 448                 {
 449                         var list = Sequence<Interval>.Empty;
 450
 451                         var curLeft = left;
 452                         var curRight = right;
 453
 454                         while (!curLeft.IsEmpty () && !curRight.IsEmpty ()) {
 455                                 var l = curLeft.Head;
 456                                 var r = curRight.Head;
 457
 458                                 if (l.IsTop || r.IsTop)
 459                                         return Sequence<Interval>.Empty;
 460
 461                                 if (l.IsBottom)
 462                                         curLeft = curLeft.Tail;
 463                                 else if (r.IsBottom)
 464                                         curRight = curRight.Tail;
 465                                 else if (l.LessEqual (r)) {
 466                                         list = list.Cons (r);
 467                                         curLeft = curLeft.Tail;
 468                                         curRight = curRight.Tail;
 469                                 }
 470                                 else if (r.LessEqual (l)) {
 471                                         list = list.Cons (l);
 472                                         curLeft = curLeft.Tail;
 473                                         curRight = curRight.Tail;
 474                                 }
 475                                 else if (r.OverlapsWith (l)) {
 476                                         list = list.Cons (l.Join (r));
 477                                         curLeft = curLeft.Tail;
 478                                         curRight = curRight.Tail;
 479                                 }
 480                                 else if (l.OnTheLeftOf (r)) {
 481                                         list = list.Cons (l);
 482                                         curLeft = curLeft.Tail;
 483                                 }
 484                                 else if (r.OnTheLeftOf (l)) {
 485                                         list = list.Cons (r);
 486                                         curRight = curRight.Tail;
 487                                 }
 488                         }
 489
 490                         while (!curLeft.IsEmpty ()) {
 491                                 list = list.Cons (curLeft.Head);
 492                                 curLeft = curLeft.Tail;
 493                         }
 494
 495                         while (!curRight.IsEmpty ()) {
 496                                 list = list.Cons (curRight.Head);
 497                                 curRight = curRight.Tail;
 498                         }
 499
 500                         return list.Reverse ();
 501                 }
 502
 503                 public static DisInterval For (Interval interval)
 504                 {
 505                         return new DisInterval (interval);
 506                 }
 507
 508                 public static DisInterval For (Sequence<Interval> intervals)
 509                 {
 510                         return new DisInterval (intervals);
 511                 }
 512
 513                 public override string ToString ()
 514                 {
 515                         if (IsTop)
 516                                 return "Top";
 517                         if (IsBottom)
 518                                 return this.BottomSymbolIfAny ();
 519                         if (intervals != null && intervals.Length () == 1)
 520                                 return intervals.Head.ToString ();
 521
 522                         return string.Format ("({0})", ToString (intervals));
 523                 }
 524
 525                 string ToString (Sequence<Interval> list)
 526                 {
 527                         if (list == null)
 528                                 return "null";
 529
 530                         var sb = new StringBuilder ();
 531                         var first = true;
 532
 533                         foreach (var intv in list.AsEnumerable ()) {
 534                                 if (first)
 535                                         first = false;
 536                                 else
 537                                         sb.Append (" ");
 538
 539                                 sb.Append (intv);
 540                         }
 541
 542                         return sb.ToString ();
 543                 }
 544
 545                 public DisInterval Select (Func<Interval, Interval> selector)
 546                 {
 547                         if (IsBottom)
 548                                 return this;
 549                         if (IsTop)
 550                                 return new DisInterval (selector (Interval.TopValue));
 551
 552                         var list = Sequence<Interval>.Empty;
 553
 554                         for (var cur = intervals; cur != null; cur = cur.Tail) {
 555                                 var intv = selector (cur.Head);
 556                                 if (intv.IsBottom)
 557                                         return Bottom;
 558                                 if (intv.IsTop)
 559                                         return Top;
 560
 561                                 list = list.Cons (intv);
 562                         }
 563
 564                         return new DisInterval (list.Reverse ());
 565                 }
 566
 567                 public static DisInterval EverythingExcept (DisInterval interval)
 568                 {
 569                         var left = Interval.For (Rational.MinusInfinity, interval.LowerBound - 1L);
 570                         var right = Interval.For (interval.UpperBound + 1L, Rational.PlusInfinity);
 571
 572                         if (left.IsNormal () && right.IsNormal ())
 573                                 return new DisInterval (Sequence<Interval>.From (left, right));
 574
 575                         if (left.IsNormal ())
 576                                 return new DisInterval (left);
 577
 578                         if (right.IsNormal ())
 579                                 return new DisInterval (right);
 580
 581                         return TopValue;
 582                 }
 583
 584                 #region Nested type: State
 585
 586                 enum State {
 587                         Normal = 0,
 588                         Top,
 589                         Bottom
 590                 }
 591
 592                 #endregion
 593         }
 594 }