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

   1 //
   2 // SetDomain.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 using Mono.CodeContracts.Static.DataStructures;
  33
  34 namespace Mono.CodeContracts.Static.Lattices {
  35         struct SetDomain<T> : IAbstractDomain<SetDomain<T>>
  36                 where T : IEquatable<T> {
  37                 public static readonly SetDomain<T> TopValue = new SetDomain<T> (ImmutableSet<T>.Empty ());
  38                 public static readonly SetDomain<T> BottomValue = new SetDomain<T> ((IImmutableSet<T>) null);
  39
  40                 readonly IImmutableSet<T> set;
  41
  42                 SetDomain (IImmutableSet<T> set)
  43                 {
  44                         this.set = set;
  45                 }
  46
  47                 public SetDomain (Func<T, int> keyConverter)
  48                 {
  49                         set = ImmutableSet<T>.Empty (keyConverter);
  50                 }
  51
  52                 public SetDomain<T> Top { get { return TopValue; } }
  53
  54                 public SetDomain<T> Bottom { get { return BottomValue; } }
  55
  56                 public bool IsTop { get { return set != null && set.Count == 0; } }
  57
  58                 public bool IsBottom { get { return set == null; } }
  59
  60                 public SetDomain<T> Join (SetDomain<T> that)
  61                 {
  62                         SetDomain<T> result;
  63                         if (this.TryTrivialJoin (that, out result))
  64                                 return result;
  65
  66                         return new SetDomain<T> (set.Intersect (that.set));
  67                 }
  68
  69                 public SetDomain<T> Join (SetDomain<T> that, bool widening, out bool weaker)
  70                 {
  71                         if (set == that.set) {
  72                                 weaker = false;
  73                                 return this;
  74                         }
  75                         if (IsBottom) {
  76                                 weaker = !that.IsBottom;
  77                                 return that;
  78                         }
  79                         if (that.IsBottom || IsTop) {
  80                                 weaker = false;
  81                                 return this;
  82                         }
  83                         if (that.IsTop) {
  84                                 weaker = !IsTop;
  85                                 return that;
  86                         }
  87
  88                         var join = set.Intersect (that.set);
  89
  90                         weaker = join.Count < set.Count;
  91                         return new SetDomain<T> (join);
  92                 }
  93
  94                 public SetDomain<T> Widen (SetDomain<T> that)
  95                 {
  96                         //no widening - finite lattice
  97
  98                         return Join (that);
  99                 }
 100
 101                 public SetDomain<T> Meet (SetDomain<T> that)
 102                 {
 103                         SetDomain<T> result;
 104                         if (this.TryTrivialMeet (that, out result))
 105                                 return result;
 106
 107                         return new SetDomain<T> (set.Union (that.set));
 108                 }
 109
 110                 public bool LessEqual (SetDomain<T> that)
 111                 {
 112                         if (IsBottom)
 113                                 return true;
 114                         if (that.IsBottom)
 115                                 return false;
 116
 117                         return that.set.IsContainedIn (set);
 118                 }
 119
 120                 public SetDomain<T> ImmutableVersion ()
 121                 {
 122                         return this;
 123                 }
 124
 125                 public SetDomain<T> Clone ()
 126                 {
 127                         return this;
 128                 }
 129
 130                 public SetDomain<T> With (T elem)
 131                 {
 132                         return new SetDomain<T> (set.Add (elem));
 133                 }
 134
 135                 public SetDomain<T> Without (T elem)
 136                 {
 137                         return new SetDomain<T> (set.Remove (elem));
 138                 }
 139
 140                 public bool Contains (T item)
 141                 {
 142                         return set.Contains (item);
 143                 }
 144
 145                 public void Dump (TextWriter tw)
 146                 {
 147                         if (IsBottom)
 148                                 tw.WriteLine ("Bot");
 149                         else if (IsTop)
 150                                 tw.WriteLine ("Top");
 151                         else
 152                                 set.Dump (tw);
 153                 }
 154                 }
 155 }