2 // ValueContextProvider.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.
29 using System.Collections.Generic;
31 using Mono.CodeContracts.Static.AST;
32 using Mono.CodeContracts.Static.Analysis.HeapAnalysis.Paths;
33 using Mono.CodeContracts.Static.ControlFlow;
34 using Mono.CodeContracts.Static.DataStructures;
35 using Mono.CodeContracts.Static.Lattices;
37 namespace Mono.CodeContracts.Static.Analysis.HeapAnalysis {
38 class ValueContextProvider<TContext> : IValueContextProvider<SymbolicValue>, IValueContext<SymbolicValue>
39 where TContext : IStackContextProvider {
40 private readonly HeapAnalysis parent;
41 private readonly TContext underlying;
43 public ValueContextProvider (HeapAnalysis parent, TContext underlying)
46 this.underlying = underlying;
49 #region Implementation of IMethodContextProvider
50 public IMethodContext MethodContext
52 get { return this.underlying.MethodContext; }
56 #region Implementation of IStackContextProvider
57 public IStackContext StackContext
59 get { return this.underlying.StackContext; }
63 #region Implementation of IValueContextProvider<SymbolicValue>
64 IValueContext<SymbolicValue> IValueContextProvider<SymbolicValue>.ValueContext
70 #region Implementation of IValueContext<SymbolicValue>
71 public FlatDomain<TypeNode> GetType (APC pc, SymbolicValue value)
74 if (!this.parent.PreStateLookup (pc, out domain) || domain.IsBottom)
75 return FlatDomain<TypeNode>.TopValue;
77 return domain.GetType (value.Symbol).Type;
80 public bool IsZero (APC at, SymbolicValue value)
83 if (!this.parent.PreStateLookup (at, out domain))
86 return domain.IsZero (value.Symbol);
89 public bool TryLocalValue (APC at, Local local, out SymbolicValue sv)
92 if (this.parent.PreStateLookup (at, out domain))
93 return domain.TryGetCorrespondingValueAbstraction (local, out sv);
95 sv = new SymbolicValue ();
99 public bool TryParameterValue (APC at, Parameter p, out SymbolicValue sv)
102 if (this.parent.PreStateLookup (at, out domain))
103 return domain.TryGetCorrespondingValueAbstraction (p, out sv);
105 sv = new SymbolicValue ();
109 public bool TryGetArrayLength (APC at, SymbolicValue array, out SymbolicValue length)
112 if (!this.parent.PreStateLookup (at, out domain))
113 throw new ArgumentException ("pc wasn't visited");
114 SymValue lengthValue;
115 bool arrayLength = domain.TryGetArrayLength (array.Symbol, out lengthValue);
117 length = new SymbolicValue (lengthValue);
121 public LispList<PathElement> AccessPathList (APC at, SymbolicValue sv, bool allowLocal, bool preferLocal)
124 if (!this.parent.PreStateLookup (at, out domain))
125 throw new ArgumentException ("pc wasn't visited");
127 AccessPathFilter<Method> filter = AccessPathFilter<Method>.IsVisibleFrom (MethodContext.CurrentMethod);
128 return domain.GetAccessPathList (sv.Symbol, filter, allowLocal, preferLocal);
131 public bool IsConstant (APC at, SymbolicValue symbol, out TypeNode type, out object constant)
134 if (!this.parent.PreStateLookup (at, out domain))
135 throw new ArgumentException ("pc wasn't visited");
137 return domain.IsConstant (symbol.Symbol, out type, out constant);
140 public bool TryStackValue (APC at, int stackIndex, out SymbolicValue sv)
143 if (this.parent.PreStateLookup (at, out domain))
144 return domain.TryGetCorrespondingValueAbstraction (stackIndex, out sv);
146 sv = new SymbolicValue ();
150 public bool IsValid (SymbolicValue sv)
152 return sv.Symbol != null;
155 public string AccessPath (APC at, SymbolicValue sv)
158 if (!this.parent.PreStateLookup (at, out domain))
159 throw new ArgumentException ("pc wasn't visited");
161 return domain.GetAccessPath (sv.Symbol);
164 public IEnumerable<LispList<PathElement>> AccessPaths (APC at, SymValue value, AccessPathFilter<Method> filter)
167 if (!this.parent.PreStateLookup (at, out domain))
168 throw new ArgumentException ("pc wasn't visited");
170 return domain.GetAccessPathsFiltered (value, filter, true).Select (path => path.Coerce<PathElementBase, PathElement> ());
173 public LispList<PathElement> VisibleAccessPathList (APC at, SymbolicValue value)
176 if (!this.parent.PreStateLookup (at, out domain))
177 throw new ArgumentException ("pc wasn't visited");
179 AccessPathFilter<Method> filter = AccessPathFilter<Method>.FromPrecondition (MethodContext.CurrentMethod);
180 return domain.GetAccessPathList (value.Symbol, filter, false, false);