2 // EnvironmentDomain.cs
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.
30 using System.Collections.Generic;
34 using Mono.CodeContracts.Static.DataStructures;
36 namespace Mono.CodeContracts.Static.Lattices {
37 class EnvironmentDomain<K, V> : IAbstractDomain<EnvironmentDomain<K, V>>
38 where V : IAbstractDomain<V>
39 where K : IEquatable<K> {
40 readonly IImmutableMapFactory<K, V> factory;
41 readonly IImmutableMap<K, V> map;
43 EnvironmentDomain (IImmutableMapFactory<K, V> factory)
44 : this (factory, factory.Empty)
48 EnvironmentDomain (IImmutableMap<K, V> map)
49 : this (map.Factory (), map)
53 EnvironmentDomain (IImmutableMapFactory<K, V> factory, IImmutableMap<K, V> map)
55 this.factory = factory;
59 public V this [K key] { get { return map == null ? default(V) : map[key]; } }
61 public IEnumerable<K> Keys { get { return map.Keys; } }
63 #region IAbstractDomain<EnvironmentDomain<K,V>> Members
65 public EnvironmentDomain<K, V> Top { get { return new EnvironmentDomain<K, V> (factory.Empty); } }
67 public EnvironmentDomain<K, V> Bottom { get { return new EnvironmentDomain<K, V> (factory, null); } }
69 public bool IsTop { get { return map != null && map.Count == 0; } }
71 public bool IsBottom { get { return map == null; } }
73 public EnvironmentDomain<K, V> Join (EnvironmentDomain<K, V> that)
75 return JoinOrWiden (that, (a, b) => a.Join (b));
78 public EnvironmentDomain<K, V> Widen (EnvironmentDomain<K, V> that)
80 return JoinOrWiden (that, (a, b) => a.Widen (b));
83 EnvironmentDomain<K, V> JoinOrWiden (EnvironmentDomain<K, V> that, Func<V, V, V> op)
85 if (ReferenceEquals (map, that.map) || IsBottom)
90 IImmutableMap<K, V> min;
91 IImmutableMap<K, V> max;
92 GetMinAndMaxByCount (map, that.map, out min, out max);
94 var result = min; // intersection of keys
95 foreach (var key in min.Keys) {
97 if (max.TryGetValue (key, out thatValue)) {
98 var join = op (min[key], thatValue);
102 result = join.IsTop ? result.Remove (key) : result.Add (key, join);
105 result = result.Remove (key);
108 return new EnvironmentDomain<K, V> (result);
111 public EnvironmentDomain<K, V> Join (EnvironmentDomain<K, V> that, bool widening, out bool weaker)
116 if (map == that.map || IsTop)
123 weaker = !that.IsBottom;
129 IImmutableMap<K, V> min;
130 IImmutableMap<K, V> max;
131 GetMinAndMaxByCount (map, that.map, out min, out max);
134 foreach (var key in min.Keys) {
135 if (!max.ContainsKey (key))
136 intersect = intersect.Remove (key);
139 var join = min[key].Join (max[key], widening, out keyWeaker);
142 intersect = join.IsTop ? intersect.Remove (key) : intersect.Add (key, join);
147 weaker |= intersect.Count < map.Count;
148 return new EnvironmentDomain<K, V> (intersect);
151 public EnvironmentDomain<K, V> Meet (EnvironmentDomain<K, V> that)
153 if (ReferenceEquals (map, that.map))
157 if (that.IsTop || IsBottom)
162 IImmutableMap<K, V> min;
163 IImmutableMap<K, V> max;
164 GetMinAndMaxByCount (map, that.map, out min, out max);
167 foreach (var key in min.Keys) {
168 if (!max.ContainsKey (key))
169 union = union.Add (key, min[key]);
171 var meet = min[key].Meet (max[key]);
172 union = union.Add (key, meet);
176 return new EnvironmentDomain<K, V> (union);
179 public bool LessEqual (EnvironmentDomain<K, V> that)
182 if (this.TryTrivialLessEqual (that, out result))
185 if (map.Count < that.map.Count)
188 return that.map.Keys.All (key => map.ContainsKey (key) && map[key].LessEqual (that.map[key]));
191 public EnvironmentDomain<K, V> ImmutableVersion ()
196 public EnvironmentDomain<K, V> Clone ()
201 public void Dump (TextWriter tw)
204 tw.WriteLine ("Top");
206 tw.WriteLine (this.BottomSymbolIfAny ());
208 map.Visit ((k, v) => {
209 tw.WriteLine ("{0} -> {1}", k, v);
210 return VisitStatus.ContinueVisit;
217 public static EnvironmentDomain<K, V> TopValue (Func<K, int> keyConverter)
219 if (keyConverter == null)
220 throw new ArgumentNullException ("keyConverter");
222 return new EnvironmentDomain<K, V> (ImmutableIntKeyMap<K, V>.Empty (keyConverter));
225 public static EnvironmentDomain<K, V> TopValue ()
227 return new EnvironmentDomain<K, V> (ImmutableMap<K, V>.Empty);
230 public static EnvironmentDomain<K, V> BottomValue (Func<K, int> keyConverter)
232 if (keyConverter == null)
233 throw new ArgumentNullException ("keyConverter");
235 return new EnvironmentDomain<K, V> (ImmutableIntKeyMap<K, V>.Empty (keyConverter).Factory (), null);
238 public static EnvironmentDomain<K, V> BottomValue ()
240 return new EnvironmentDomain<K, V> (ImmutableMap<K, V>.Empty.Factory (), null);
243 public EnvironmentDomain<K, V> With (K key, V value)
246 return Without (key);
248 return new EnvironmentDomain<K, V> (map.Add (key, value));
251 public EnvironmentDomain<K, V> RefineWith (K key, V value)
254 if (map.TryGetValue (key, out old))
255 value = value.Meet (old);
257 return With (key, value);
260 public EnvironmentDomain<K, V> Without (K key)
262 return new EnvironmentDomain<K, V> (map.Remove (key));
265 public bool Contains (K key)
267 return map != null && map.ContainsKey (key);
270 public bool TryGetValue (K key, out V value)
273 return false.Without (out value);
275 return map.TryGetValue (key, out value);
278 public EnvironmentDomain<K, V> Empty ()
280 return new EnvironmentDomain<K, V> (factory.Empty);
283 static bool GetMinAndMaxByCount
284 (IImmutableMap<K, V> a, IImmutableMap<K, V> b,
285 out IImmutableMap<K, V> min, out IImmutableMap<K, V> max)
287 if (a.Count < b.Count) {