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.
31 using Mono.CodeContracts.Static.AST;
32 using Mono.CodeContracts.Static.Lattices;
34 namespace Mono.CodeContracts.Static.Analysis.HeapAnalysis {
35 struct AbstractType : IAbstractDomainForEGraph<AbstractType>, IEquatable<AbstractType> {
36 public static AbstractType TopValue = new AbstractType (FlatDomain<TypeNode>.TopValue, false);
37 public static AbstractType BottomValue = new AbstractType (FlatDomain<TypeNode>.BottomValue, true);
39 private FlatDomain<TypeNode> value;
41 public AbstractType (FlatDomain<TypeNode> value, bool isZero) : this ()
47 public bool IsZero { get; private set; }
49 public FlatDomain<TypeNode> Type
51 get { return this.value; }
54 public TypeNode ConcreteType
56 get { return this.value.Value; }
59 private static AbstractType ForManifestedFieldValue
61 get { return TopValue; }
64 public AbstractType ButZero
66 get { return new AbstractType (this.value, true); }
68 public AbstractType With (FlatDomain<TypeNode> type)
70 return new AbstractType (type, this.IsZero);
73 #region IAbstractDomainForEGraph<AbstractType> Members
74 public AbstractType Top
76 get { return new AbstractType (FlatDomain<TypeNode>.TopValue, false); }
79 public AbstractType Bottom
81 get { return new AbstractType (FlatDomain<TypeNode>.BottomValue, true); }
86 get { return !IsZero && this.value.IsTop; }
91 get { return IsZero && this.value.IsBottom; }
94 public AbstractType Join(AbstractType that)
96 throw new NotImplementedException();
99 public AbstractType Join (AbstractType that, bool widening, out bool weaker)
103 if (this.value.IsBottom)
104 return new AbstractType (that.value, IsZero);
109 if (that.value.IsBottom)
110 return new AbstractType (this.value, that.IsZero);
114 FlatDomain<TypeNode> resultType = this.value.Join (that.value, widening, out weaker);
115 return new AbstractType (resultType, false);
118 public AbstractType Widen(AbstractType that)
120 throw new NotImplementedException();
123 public AbstractType Meet (AbstractType that)
125 return new AbstractType (this.value.Meet (that.value), IsZero || that.IsZero);
128 public bool LessEqual (AbstractType that)
135 return this.value.LessEqual (that.value);
138 public AbstractType ImmutableVersion ()
143 public AbstractType Clone ()
148 public void Dump (TextWriter tw)
151 tw.Write ("(Zero) ");
153 this.value.Dump (tw);
156 public bool HasAllBottomFields
158 get { return IsZero; }
161 public AbstractType ForManifestedField ()
163 return ForManifestedFieldValue;
167 #region IEquatable<AbstractType> Members
168 public bool Equals (AbstractType that)
170 return this.IsZero == that.IsZero && this.value.Equals (that.value);
174 public override string ToString ()
176 return (IsZero ? "(Zero) " : "") + this.value;