5 // Alexander Chebaturkin (chebaturkin@gmail.com)
7 // Copyright (C) 2011 Alexander Chebaturkin
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:
17 // The above copyright notice and this permission notice shall be
18 // included in all copies or substantial portions of the Software.
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.
32 namespace Mono
.CodeContracts
.Static
.Lattices
{
34 /// Represents domain, where abstract values are disjunct, and their join/meet turns into Top/Bottom respectively
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
);
49 public readonly T Value
;
50 readonly DomainKind state
;
52 FlatDomain (DomainKind state
)
58 public FlatDomain (T
value)
60 state
= DomainKind
.Normal
;
64 public static implicit operator FlatDomain
<T
> (T
value)
66 return new FlatDomain
<T
> (value);
69 #region Implementation of IAbstractDomain<FlatDomain<T>>
71 public FlatDomain
<T
> Top { get { return TopValue; }
}
73 public FlatDomain
<T
> Bottom { get { return BottomValue; }
}
75 public bool IsTop { get { return state == DomainKind.Top; }
}
77 public bool IsBottom { get { return state == DomainKind.Bottom; }
}
79 public FlatDomain
<T
> Join (FlatDomain
<T
> that
, bool widening
, out bool weaker
)
81 if (IsTop
|| that
.IsBottom
) {
90 weaker
= !that
.IsBottom
;
93 if (Value
.Equals (that
.Value
)) {
102 public FlatDomain
<T
> Widen (FlatDomain
<T
> that
)
104 // no widening - it's finite lattice
109 public FlatDomain
<T
> Join (FlatDomain
<T
> that
)
111 FlatDomain
<T
> result
;
112 if (this.TryTrivialJoin (that
, out result
))
115 // this and that must be normal here
116 return Value
.Equals (that
.Value
) ? this : TopValue
;
119 public FlatDomain
<T
> Meet (FlatDomain
<T
> that
)
121 FlatDomain
<T
> result
;
122 if (this.TryTrivialMeet (that
, out result
))
125 return Value
.Equals (that
.Value
) ? this : BottomValue
;
128 public bool LessEqual (FlatDomain
<T
> that
)
131 if (this.TryTrivialLessEqual (that
, out result
))
134 return Value
.Equals (that
.Value
);
137 public FlatDomain
<T
> ImmutableVersion ()
142 public FlatDomain
<T
> Clone ()
147 public void Dump (TextWriter tw
)
150 tw
.WriteLine ("Top");
152 tw
.WriteLine (this.BottomSymbolIfAny ());
154 tw
.WriteLine ("<{0}>", Value
);
157 public override string ToString ()
162 return this.BottomSymbolIfAny ();
164 return string.Format ("<{0}>", Value
);
169 public bool Equals (FlatDomain
<T
> that
)
171 if (!this.IsNormal ())
172 return state
== that
.state
;
174 return that
.IsNormal () && Value
.Equals (that
.Value
);