2 // ExpressionDecoder.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 Mono.CodeContracts.Static.AST;
31 using Mono.CodeContracts.Static.AST.Visitors;
32 using Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions;
33 using Mono.CodeContracts.Static.Analysis.HeapAnalysis;
34 using Mono.CodeContracts.Static.ControlFlow;
35 using Mono.CodeContracts.Static.DataStructures;
36 using Mono.CodeContracts.Static.Lattices;
37 using Mono.CodeContracts.Static.Providers;
39 namespace Mono.CodeContracts.Static.Analysis.ExpressionAnalysis {
40 class ExpressionDecoder<TSymbolicValue, TContext, TEdgeData> :
41 IILDecoder<APC, LabeledSymbol<APC, TSymbolicValue>, TSymbolicValue, IExpressionContextProvider<LabeledSymbol<APC, TSymbolicValue>, TSymbolicValue>, TEdgeData>,
42 IExpressionContextProvider<LabeledSymbol<APC, TSymbolicValue>, TSymbolicValue>,
43 IExpressionContext<LabeledSymbol<APC, TSymbolicValue>, TSymbolicValue>
44 where TSymbolicValue : IEquatable<TSymbolicValue>
45 where TContext : IValueContextProvider<TSymbolicValue>
46 where TEdgeData : IImmutableMap<TSymbolicValue, LispList<TSymbolicValue>> {
47 private readonly IILDecoder<APC, TSymbolicValue, TSymbolicValue, IValueContextProvider<TSymbolicValue>, TEdgeData> value_decoder;
48 private readonly ExpressionAnalysisFacade<TSymbolicValue, TContext, TEdgeData> parent;
49 private readonly IValueContextProvider<TSymbolicValue> underlying;
51 public ExpressionDecoder (IILDecoder<APC, TSymbolicValue, TSymbolicValue, IValueContextProvider<TSymbolicValue>, TEdgeData> valueDecoder,
52 ExpressionAnalysisFacade<TSymbolicValue, TContext, TEdgeData> parent)
54 this.value_decoder = valueDecoder;
56 this.underlying = valueDecoder.ContextProvider;
59 #region IExpressionContext<LabeledSymbol<APC,SymbolicValue>,SymbolicValue> Members
60 public LabeledSymbol<APC, TSymbolicValue> Refine (APC pc, TSymbolicValue variable)
62 return new LabeledSymbol<APC, TSymbolicValue> (pc, variable);
65 public TSymbolicValue Unrefine (LabeledSymbol<APC, TSymbolicValue> expression)
67 return expression.Symbol;
70 public Result Decode<Data, Result, Visitor> (LabeledSymbol<APC, TSymbolicValue> expr, Visitor visitor, Data data)
71 where Visitor : ISymbolicExpressionVisitor<LabeledSymbol<APC, TSymbolicValue>, LabeledSymbol<APC, TSymbolicValue>, TSymbolicValue, Data, Result>
73 ExprDomain<TSymbolicValue> ifFound;
74 if (!this.parent.PreStateLookup (expr.ReadAt, out ifFound) || ifFound.IsBottom)
75 return visitor.SymbolicConstant (expr, expr.Symbol, data);
77 FlatDomain<Expr<TSymbolicValue>> aExpr = ifFound [expr.Symbol];
79 return aExpr.Concrete.Decode<Data, Result, ExpressionDecoderAdapter<TSymbolicValue, Data, Result, Visitor>>
80 (expr.ReadAt, expr.Symbol,
81 new ExpressionDecoderAdapter<TSymbolicValue, Data, Result, Visitor> (visitor), data);
86 if (this.parent.ValueLayer.ILDecoder.ContextProvider.ValueContext.IsConstant (expr.ReadAt, expr.Symbol, out type, out constant))
87 return visitor.LoadConst (expr, type, constant, expr.Symbol, data);
89 return visitor.SymbolicConstant (expr, expr.Symbol, data);
92 public FlatDomain<TypeNode> GetType (LabeledSymbol<APC, TSymbolicValue> expr)
94 return this.underlying.ValueContext.GetType (expr.ReadAt, expr.Symbol);
97 public APC GetPC (LabeledSymbol<APC, TSymbolicValue> pc)
102 public LabeledSymbol<APC, TSymbolicValue> For (TSymbolicValue variable)
104 return new LabeledSymbol<APC, TSymbolicValue> (MethodContext.CFG.Entry, variable);
107 public bool IsZero (LabeledSymbol<APC, TSymbolicValue> expression)
109 return ValueContext.IsZero (expression.ReadAt, expression.Symbol);
113 #region IILDecoder<APC,LabeledSymbol<APC,SymbolicValue>,SymbolicValue,IExpressionContextProvider<LabeledSymbol<APC,SymbolicValue>,SymbolicValue>,EdgeData> Members
114 public IExpressionContextProvider<LabeledSymbol<APC, TSymbolicValue>, TSymbolicValue> ContextProvider
119 public Result ForwardDecode<Data, Result, Visitor> (APC pc, Visitor visitor, Data state)
120 where Visitor : IILVisitor<APC, LabeledSymbol<APC, TSymbolicValue>, TSymbolicValue, Data, Result>
122 return this.value_decoder.ForwardDecode<Data, Result, ILDecoderAdapter<TSymbolicValue, Data, Result, Visitor>>
123 (pc, new ILDecoderAdapter<TSymbolicValue, Data, Result, Visitor> (visitor), state);
126 public bool IsUnreachable (APC pc)
128 return this.parent.IsUnreachable (pc);
131 public TEdgeData EdgeData (APC from, APC to)
133 return this.parent.ValueLayer.ILDecoder.EdgeData (from, to);
137 #region Implementation of IMethodContextProvider<Field,Method>
138 public IMethodContext MethodContext
140 get { return this.underlying.MethodContext; }
144 #region Implementation of IStackContextProvider<Field,Method>
145 public IStackContext StackContext
147 get { return this.underlying.StackContext; }
151 #region Implementation of IValueContextProvider<Local,Parameter,Method,Field,Type,SymbolicValue>
152 public IValueContext<TSymbolicValue> ValueContext
154 get { return this.underlying.ValueContext; }
158 #region Implementation of IExpressionContextProvider<Local,Parameter,Method,Field,Type,ExternalExpression<APC,SymbolicValue>,SymbolicValue>
159 public IExpressionContext<LabeledSymbol<APC, TSymbolicValue>, TSymbolicValue> ExpressionContext