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;
31 using Mono.CodeContracts.Static.AST;
32 using Mono.CodeContracts.Static.AST.Visitors;
33 using Mono.CodeContracts.Static.Analysis.HeapAnalysis;
34 using Mono.CodeContracts.Static.ControlFlow;
35 using Mono.CodeContracts.Static.DataStructures;
37 namespace Mono.CodeContracts.Static.Analysis.ExpressionAnalysis {
39 /// This class performs translation from (source) SymbolicValue to LabeledSymbol
41 struct ILDecoderAdapter<SymbolicValue, Data, Result, Visitor>
42 : IILVisitor<APC, SymbolicValue, SymbolicValue, Data, Result>
43 where SymbolicValue : IEquatable<SymbolicValue>
44 where Visitor : IILVisitor<APC, LabeledSymbol<APC, SymbolicValue>, SymbolicValue, Data, Result> {
45 private readonly Visitor visitor;
47 public ILDecoderAdapter (Visitor visitor)
49 this.visitor = visitor;
52 #region IILVisitor<APC,SymbolicValue,SymbolicValue,Data,Result> Members
53 public Result Binary (APC pc, BinaryOperator op, SymbolicValue dest, SymbolicValue operand1, SymbolicValue operand2, Data data)
55 return this.visitor.Binary (pc, op, dest, Convert (pc, operand1), Convert (pc, operand2), data);
58 public Result Isinst (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue obj, Data data)
60 return this.visitor.Isinst (pc, type, dest, Convert (pc, obj), data);
63 public Result LoadNull (APC pc, SymbolicValue dest, Data polarity)
65 return this.visitor.LoadNull (pc, dest, polarity);
68 public Result LoadConst (APC pc, TypeNode type, object constant, SymbolicValue dest, Data data)
70 return this.visitor.LoadConst (pc, type, constant, dest, data);
73 public Result Sizeof (APC pc, TypeNode type, SymbolicValue dest, Data data)
75 return this.visitor.Sizeof (pc, type, dest, data);
78 public Result Unary (APC pc, UnaryOperator op, bool unsigned, SymbolicValue dest, SymbolicValue source, Data data)
80 return this.visitor.Unary (pc, op, unsigned, dest, Convert (pc, source), data);
83 public Result Entry (APC pc, Method method, Data data)
85 return this.visitor.Entry (pc, method, data);
88 public Result Assume (APC pc, EdgeTag tag, SymbolicValue condition, Data data)
90 return this.visitor.Assume (pc, tag, Convert (pc, condition), data);
93 public Result Assert (APC pc, EdgeTag tag, SymbolicValue condition, Data data)
95 return this.visitor.Assert (pc, tag, Convert (pc, condition), data);
98 public Result BeginOld (APC pc, APC matchingEnd, Data data)
100 return this.visitor.BeginOld (pc, matchingEnd, data);
103 public Result EndOld (APC pc, APC matchingBegin, TypeNode type, SymbolicValue dest, SymbolicValue source, Data data)
105 return this.visitor.EndOld (pc, matchingBegin, type, dest, Convert (pc, source), data);
108 public Result LoadStack (APC pc, int offset, SymbolicValue dest, SymbolicValue source, bool isOld, Data data)
110 return this.visitor.LoadStack (pc, offset, dest, Convert (pc, source), isOld, data);
113 public Result LoadStackAddress (APC pc, int offset, SymbolicValue dest, SymbolicValue source, TypeNode type, bool isOld, Data data)
115 return this.visitor.LoadStackAddress (pc, offset, dest, Convert (pc, source), type, isOld, data);
118 public Result LoadResult (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue source, Data data)
120 return this.visitor.LoadResult (pc, type, dest, Convert (pc, source), data);
123 public Result Arglist (APC pc, SymbolicValue dest, Data data)
125 return this.visitor.Arglist (pc, dest, data);
128 public Result Branch (APC pc, APC target, bool leavesExceptionBlock, Data data)
130 throw new Exception ("Should not get branches at this level of abstraction.");
133 public Result BranchCond (APC pc, APC target, BranchOperator bop, SymbolicValue value1, SymbolicValue value2, Data data)
135 throw new Exception ("Should not get branches at this level of abstraction.");
138 public Result BranchTrue (APC pc, APC target, SymbolicValue cond, Data data)
140 throw new Exception ("Should not get branches at this level of abstraction.");
143 public Result BranchFalse (APC pc, APC target, SymbolicValue cond, Data data)
145 throw new Exception ("Should not get branches at this level of abstraction.");
148 public Result Break (APC pc, Data data)
150 return this.visitor.Break (pc, data);
153 public Result Call<TypeList, ArgList> (APC pc, Method method, bool virt, TypeList extraVarargs, SymbolicValue dest, ArgList args, Data data)
154 where TypeList : IIndexable<TypeNode>
155 where ArgList : IIndexable<SymbolicValue>
157 return this.visitor.Call (pc, method, virt, extraVarargs, dest, Convert (pc, args), data);
160 public Result Calli<TypeList, ArgList> (APC pc, TypeNode returnType, TypeList argTypes, bool instance, SymbolicValue dest, SymbolicValue functionPointer, ArgList args, Data data)
161 where TypeList : IIndexable<TypeNode> where ArgList : IIndexable<SymbolicValue>
163 return this.visitor.Calli (pc, returnType, argTypes, instance, dest, Convert (pc, functionPointer), Convert (pc, args), data);
166 public Result CheckFinite (APC pc, SymbolicValue dest, SymbolicValue source, Data data)
168 return this.visitor.CheckFinite (pc, dest, Convert (pc, source), data);
171 public Result CopyBlock (APC pc, SymbolicValue destAddress, SymbolicValue srcAddress, SymbolicValue len, Data data)
173 return this.visitor.CopyBlock (pc, Convert (pc, destAddress), Convert (pc, srcAddress), Convert (pc, len), data);
176 public Result EndFilter (APC pc, SymbolicValue decision, Data data)
178 return this.visitor.EndFilter (pc, Convert (pc, decision), data);
181 public Result EndFinally (APC pc, Data data)
183 return this.visitor.EndFinally (pc, data);
186 public Result Jmp (APC pc, Method method, Data data)
188 return this.visitor.Jmp (pc, method, data);
191 public Result LoadArg (APC pc, Parameter argument, bool isOld, SymbolicValue dest, Data data)
193 return this.visitor.LoadArg (pc, argument, isOld, dest, data);
196 public Result LoadArgAddress (APC pc, Parameter argument, bool isOld, SymbolicValue dest, Data data)
198 return this.visitor.LoadArgAddress (pc, argument, isOld, dest, data);
201 public Result LoadLocal (APC pc, Local local, SymbolicValue dest, Data data)
203 return this.visitor.LoadLocal (pc, local, dest, data);
206 public Result LoadLocalAddress (APC pc, Local local, SymbolicValue dest, Data data)
208 return this.visitor.LoadLocalAddress (pc, local, dest, data);
211 public Result Nop (APC pc, Data data)
213 return this.visitor.Nop (pc, data);
216 public Result Pop (APC pc, SymbolicValue source, Data data)
218 return this.visitor.Pop (pc, Convert (pc, source), data);
221 public Result Return (APC pc, SymbolicValue source, Data data)
223 return this.visitor.Return (pc, Convert (pc, source), data);
226 public Result StoreArg (APC pc, Parameter argument, SymbolicValue source, Data data)
228 return this.visitor.StoreArg (pc, argument, Convert (pc, source), data);
231 public Result StoreLocal (APC pc, Local local, SymbolicValue source, Data data)
233 return this.visitor.StoreLocal (pc, local, Convert (pc, source), data);
236 public Result Switch (APC pc, TypeNode type, IEnumerable<Pair<object, APC>> cases, SymbolicValue value, Data data)
238 throw new Exception ("Should not get branches at this level of abstraction.");
241 public Result Box (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue source, Data data)
243 return this.visitor.Box (pc, type, dest, Convert (pc, source), data);
246 public Result ConstrainedCallvirt<TypeList, ArgList> (APC pc, Method method, TypeNode constraint, TypeList extraVarargs, SymbolicValue dest, ArgList args, Data data)
247 where TypeList : IIndexable<TypeNode>
248 where ArgList : IIndexable<SymbolicValue>
250 return this.visitor.ConstrainedCallvirt (pc, method, constraint, extraVarargs, dest, Convert (pc, args), data);
253 public Result CastClass (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue obj, Data data)
255 return this.visitor.CastClass (pc, type, dest, Convert (pc, obj), data);
258 public Result CopyObj (APC pc, TypeNode type, SymbolicValue destPtr, SymbolicValue sourcePtr, Data data)
260 return this.visitor.CopyObj (pc, type, Convert (pc, destPtr), Convert (pc, sourcePtr), data);
263 public Result Initobj (APC pc, TypeNode type, SymbolicValue ptr, Data data)
265 return this.visitor.Initobj (pc, type, Convert (pc, ptr), data);
268 public Result LoadElement (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue array, SymbolicValue index, Data data)
270 return this.visitor.LoadElement (pc, type, dest, Convert (pc, array), Convert (pc, index), data);
273 public Result LoadField (APC pc, Field field, SymbolicValue dest, SymbolicValue obj, Data data)
275 return this.visitor.LoadField (pc, field, dest, Convert (pc, obj), data);
278 public Result LoadFieldAddress (APC pc, Field field, SymbolicValue dest, SymbolicValue obj, Data data)
280 return this.visitor.LoadFieldAddress (pc, field, dest, Convert (pc, obj), data);
283 public Result LoadLength (APC pc, SymbolicValue dest, SymbolicValue array, Data data)
285 return this.visitor.LoadLength (pc, dest, Convert (pc, array), data);
288 public Result LoadStaticField (APC pc, Field field, SymbolicValue dest, Data data)
290 return this.visitor.LoadStaticField (pc, field, dest, data);
293 public Result LoadStaticFieldAddress (APC pc, Field field, SymbolicValue dest, Data data)
295 return this.visitor.LoadStaticFieldAddress (pc, field, dest, data);
298 public Result LoadTypeToken (APC pc, TypeNode type, SymbolicValue dest, Data data)
300 return this.visitor.LoadTypeToken (pc, type, dest, data);
303 public Result LoadFieldToken (APC pc, Field type, SymbolicValue dest, Data data)
305 return this.visitor.LoadFieldToken (pc, type, dest, data);
308 public Result LoadMethodToken (APC pc, Method type, SymbolicValue dest, Data data)
310 return this.visitor.LoadMethodToken (pc, type, dest, data);
313 public Result NewArray<ArgList> (APC pc, TypeNode type, SymbolicValue dest, ArgList lengths, Data data) where ArgList : IIndexable<SymbolicValue>
315 return this.visitor.NewArray (pc, type, dest, Convert (pc, lengths), data);
318 public Result NewObj<ArgList> (APC pc, Method ctor, SymbolicValue dest, ArgList args, Data data) where ArgList : IIndexable<SymbolicValue>
320 return this.visitor.NewObj (pc, ctor, dest, Convert (pc, args), data);
323 public Result MkRefAny (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue obj, Data data)
325 return this.visitor.MkRefAny (pc, type, dest, Convert (pc, obj), data);
328 public Result RefAnyType (APC pc, SymbolicValue dest, SymbolicValue source, Data data)
330 return this.visitor.RefAnyType (pc, dest, Convert (pc, source), data);
333 public Result RefAnyVal (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue source, Data data)
335 return this.visitor.RefAnyVal (pc, type, dest, Convert (pc, source), data);
338 public Result Rethrow (APC pc, Data data)
340 return this.visitor.Rethrow (pc, data);
343 public Result StoreElement (APC pc, TypeNode type, SymbolicValue array, SymbolicValue index, SymbolicValue value, Data data)
345 return this.visitor.StoreElement (pc, type, Convert (pc, array), Convert (pc, index), Convert (pc, value), data);
348 public Result StoreField (APC pc, Field field, SymbolicValue obj, SymbolicValue value, Data data)
350 return this.visitor.StoreField (pc, field, Convert (pc, obj), Convert (pc, value), data);
353 public Result StoreStaticField (APC pc, Field field, SymbolicValue value, Data data)
355 return this.visitor.StoreStaticField (pc, field, Convert (pc, value), data);
358 public Result Throw (APC pc, SymbolicValue exception, Data data)
360 return this.visitor.Throw (pc, Convert (pc, exception), data);
363 public Result Unbox (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue obj, Data data)
365 return this.visitor.Unbox (pc, type, dest, Convert (pc, obj), data);
368 public Result UnboxAny (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue obj, Data data)
370 return this.visitor.UnboxAny (pc, type, dest, Convert (pc, obj), data);
374 private static LabeledSymbol<APC, SymbolicValue> Convert (APC pc, SymbolicValue value)
376 return new LabeledSymbol<APC, SymbolicValue> (pc, value);
379 private static ArgumentWrapper<ArgList> Convert<ArgList> (APC pc, ArgList value)
380 where ArgList : IIndexable<SymbolicValue>
382 return new ArgumentWrapper<ArgList> (value, pc);
385 #region Nested type: ArgumentWrapper
386 private struct ArgumentWrapper<ArgList> : IIndexable<LabeledSymbol<APC, SymbolicValue>>
387 where ArgList : IIndexable<SymbolicValue> {
388 private readonly APC readAt;
389 private readonly ArgList underlying;
391 public ArgumentWrapper (ArgList underlying, APC readAt)
393 this.underlying = underlying;
394 this.readAt = readAt;
397 #region Implementation of IIndexable<ExternalExpression<APC,SymbolicValue>>
400 get { return this.underlying.Count; }
403 public LabeledSymbol<APC, SymbolicValue> this [int index]
405 get { return new LabeledSymbol<APC, SymbolicValue> (this.readAt, this.underlying [index]); }