mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Lattices/FlatDomain.cs

   1 //
   2 // FlatDomain.cs
   3 //
   4 // Authors:
   5 //      Alexander Chebaturkin (chebaturkin@gmail.com)
   6 //
   7 // Copyright (C) 2011 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.IO;
  31
  32 namespace Mono.CodeContracts.Static.Lattices {
  33         /// <summary>
  34         /// Represents domain, where abstract values are disjunct, and their join/meet turns into Top/Bottom respectively
  35         /// </summary>
  36         /// <example>
  37         ///       Top
  38         ///      / | \
  39         ///    v1 v2 v3
  40         ///      \ | /
  41         ///       Bot
  42         /// </example>
  43         /// <typeparam name="T"></typeparam>
  44         public struct FlatDomain<T> : IAbstractDomain<FlatDomain<T>>, IEquatable<FlatDomain<T>>
  45                 where T : IEquatable<T> {
  46                 public static readonly FlatDomain<T> BottomValue = new FlatDomain<T> (DomainKind.Bottom);
  47                 public static readonly FlatDomain<T> TopValue = new FlatDomain<T> (DomainKind.Top);
  48
  49                 public readonly T Value;
  50                 readonly DomainKind state;
  51
  52                 FlatDomain (DomainKind state)
  53                 {
  54                         this.state = state;
  55                         Value = default(T);
  56                 }
  57
  58                 public FlatDomain (T value)
  59                 {
  60                         state = DomainKind.Normal;
  61                         Value = value;
  62                 }
  63
  64                 public static implicit operator FlatDomain<T> (T value)
  65                 {
  66                         return new FlatDomain<T> (value);
  67                 }
  68
  69                 #region Implementation of IAbstractDomain<FlatDomain<T>>
  70
  71                 public FlatDomain<T> Top { get { return TopValue; } }
  72
  73                 public FlatDomain<T> Bottom { get { return BottomValue; } }
  74
  75                 public bool IsTop { get { return state == DomainKind.Top; } }
  76
  77                 public bool IsBottom { get { return state == DomainKind.Bottom; } }
  78
  79                 public FlatDomain<T> Join (FlatDomain<T> that, bool widening, out bool weaker)
  80                 {
  81                         if (IsTop || that.IsBottom) {
  82                                 weaker = false;
  83                                 return this;
  84                         }
  85                         if (that.IsTop) {
  86                                 weaker = !IsTop;
  87                                 return that;
  88                         }
  89                         if (IsBottom) {
  90                                 weaker = !that.IsBottom;
  91                                 return that;
  92                         }
  93                         if (Value.Equals (that.Value)) {
  94                                 weaker = false;
  95                                 return that;
  96                         }
  97
  98                         weaker = true;
  99                         return TopValue;
 100                 }
 101
 102                 public FlatDomain<T> Widen (FlatDomain<T> that)
 103                 {
 104                         // no widening - it's finite lattice
 105
 106                         return Join (that);
 107                 }
 108
 109                 public FlatDomain<T> Join (FlatDomain<T> that)
 110                 {
 111                         FlatDomain<T> result;
 112                         if (this.TryTrivialJoin (that, out result))
 113                                 return result;
 114
 115                         // this and that must be normal here
 116                         return Value.Equals (that.Value) ? this : TopValue;
 117                 }
 118
 119                 public FlatDomain<T> Meet (FlatDomain<T> that)
 120                 {
 121                         FlatDomain<T> result;
 122                         if (this.TryTrivialMeet (that, out result))
 123                                 return result;
 124
 125                         return Value.Equals (that.Value) ? this : BottomValue;
 126                 }
 127
 128                 public bool LessEqual (FlatDomain<T> that)
 129                 {
 130                         bool result;
 131                         if (this.TryTrivialLessEqual (that, out result))
 132                                 return result;
 133
 134                         return Value.Equals (that.Value);
 135                 }
 136
 137                 public FlatDomain<T> ImmutableVersion ()
 138                 {
 139                         return this;
 140                 }
 141
 142                 public FlatDomain<T> Clone ()
 143                 {
 144                         return this;
 145                 }
 146
 147                 public void Dump (TextWriter tw)
 148                 {
 149                         if (IsTop)
 150                                 tw.WriteLine ("Top");
 151                         else if (IsBottom)
 152                                 tw.WriteLine (this.BottomSymbolIfAny ());
 153                         else
 154                                 tw.WriteLine ("<{0}>", Value);
 155                 }
 156
 157                 public override string ToString ()
 158                 {
 159                         if (IsTop)
 160                                 return "Top";
 161                         if (IsBottom)
 162                                 return this.BottomSymbolIfAny ();
 163
 164                         return string.Format ("<{0}>", Value);
 165                 }
 166
 167                 #endregion
 168
 169                 public bool Equals (FlatDomain<T> that)
 170                 {
 171                         if (!this.IsNormal ())
 172                                 return state == that.state;
 173
 174                         return that.IsNormal () && Value.Equals (that.Value);
 175                 }
 176                 }
 177
 178         enum DomainKind {
 179                 Normal = 0,
 180                 Top,
 181                 Bottom
 182         }
 183 }