The base architecture for code-contracts analysis
[mono.git] / mcs / class / Mono.CodeContracts / Mono.CodeContracts.Static.Analysis.ExpressionAnalysis / ILDecoderAdapter.cs
1 // 
2 // ILDecoderAdapter.cs
3 // 
4 // Authors:
5 //      Alexander Chebaturkin (chebaturkin@gmail.com)
6 // 
7 // Copyright (C) 2011 Alexander Chebaturkin
8 // 
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:
16 // 
17 // The above copyright notice and this permission notice shall be
18 // included in all copies or substantial portions of the Software.
19 //  
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.
27 //
28
29 using System;
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;
36
37 namespace Mono.CodeContracts.Static.Analysis.ExpressionAnalysis {
38         /// <summary>
39         /// This class performs translation from (source) SymbolicValue to LabeledSymbol
40         /// </summary>
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;
46
47                 public ILDecoderAdapter (Visitor visitor)
48                 {
49                         this.visitor = visitor;
50                 }
51
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)
54                 {
55                         return this.visitor.Binary (pc, op, dest, Convert (pc, operand1), Convert (pc, operand2), data);
56                 }
57
58                 public Result Isinst (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue obj, Data data)
59                 {
60                         return this.visitor.Isinst (pc, type, dest, Convert (pc, obj), data);
61                 }
62
63                 public Result LoadNull (APC pc, SymbolicValue dest, Data polarity)
64                 {
65                         return this.visitor.LoadNull (pc, dest, polarity);
66                 }
67
68                 public Result LoadConst (APC pc, TypeNode type, object constant, SymbolicValue dest, Data data)
69                 {
70                         return this.visitor.LoadConst (pc, type, constant, dest, data);
71                 }
72
73                 public Result Sizeof (APC pc, TypeNode type, SymbolicValue dest, Data data)
74                 {
75                         return this.visitor.Sizeof (pc, type, dest, data);
76                 }
77
78                 public Result Unary (APC pc, UnaryOperator op, bool unsigned, SymbolicValue dest, SymbolicValue source, Data data)
79                 {
80                         return this.visitor.Unary (pc, op, unsigned, dest, Convert (pc, source), data);
81                 }
82
83                 public Result Entry (APC pc, Method method, Data data)
84                 {
85                         return this.visitor.Entry (pc, method, data);
86                 }
87
88                 public Result Assume (APC pc, EdgeTag tag, SymbolicValue condition, Data data)
89                 {
90                         return this.visitor.Assume (pc, tag, Convert (pc, condition), data);
91                 }
92
93                 public Result Assert (APC pc, EdgeTag tag, SymbolicValue condition, Data data)
94                 {
95                         return this.visitor.Assert (pc, tag, Convert (pc, condition), data);
96                 }
97
98                 public Result BeginOld (APC pc, APC matchingEnd, Data data)
99                 {
100                         return this.visitor.BeginOld (pc, matchingEnd, data);
101                 }
102
103                 public Result EndOld (APC pc, APC matchingBegin, TypeNode type, SymbolicValue dest, SymbolicValue source, Data data)
104                 {
105                         return this.visitor.EndOld (pc, matchingBegin, type, dest, Convert (pc, source), data);
106                 }
107
108                 public Result LoadStack (APC pc, int offset, SymbolicValue dest, SymbolicValue source, bool isOld, Data data)
109                 {
110                         return this.visitor.LoadStack (pc, offset, dest, Convert (pc, source), isOld, data);
111                 }
112
113                 public Result LoadStackAddress (APC pc, int offset, SymbolicValue dest, SymbolicValue source, TypeNode type, bool isOld, Data data)
114                 {
115                         return this.visitor.LoadStackAddress (pc, offset, dest, Convert (pc, source), type, isOld, data);
116                 }
117
118                 public Result LoadResult (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue source, Data data)
119                 {
120                         return this.visitor.LoadResult (pc, type, dest, Convert (pc, source), data);
121                 }
122
123                 public Result Arglist (APC pc, SymbolicValue dest, Data data)
124                 {
125                         return this.visitor.Arglist (pc, dest, data);
126                 }
127
128                 public Result Branch (APC pc, APC target, bool leavesExceptionBlock, Data data)
129                 {
130                         throw new Exception ("Should not get branches at this level of abstraction.");
131                 }
132
133                 public Result BranchCond (APC pc, APC target, BranchOperator bop, SymbolicValue value1, SymbolicValue value2, Data data)
134                 {
135                         throw new Exception ("Should not get branches at this level of abstraction.");
136                 }
137
138                 public Result BranchTrue (APC pc, APC target, SymbolicValue cond, Data data)
139                 {
140                         throw new Exception ("Should not get branches at this level of abstraction.");
141                 }
142
143                 public Result BranchFalse (APC pc, APC target, SymbolicValue cond, Data data)
144                 {
145                         throw new Exception ("Should not get branches at this level of abstraction.");
146                 }
147
148                 public Result Break (APC pc, Data data)
149                 {
150                         return this.visitor.Break (pc, data);
151                 }
152
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>
156                 {
157                         return this.visitor.Call (pc, method, virt, extraVarargs, dest, Convert (pc, args), data);
158                 }
159
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>
162                 {
163                         return this.visitor.Calli (pc, returnType, argTypes, instance, dest, Convert (pc, functionPointer), Convert (pc, args), data);
164                 }
165
166                 public Result CheckFinite (APC pc, SymbolicValue dest, SymbolicValue source, Data data)
167                 {
168                         return this.visitor.CheckFinite (pc, dest, Convert (pc, source), data);
169                 }
170
171                 public Result CopyBlock (APC pc, SymbolicValue destAddress, SymbolicValue srcAddress, SymbolicValue len, Data data)
172                 {
173                         return this.visitor.CopyBlock (pc, Convert (pc, destAddress), Convert (pc, srcAddress), Convert (pc, len), data);
174                 }
175
176                 public Result EndFilter (APC pc, SymbolicValue decision, Data data)
177                 {
178                         return this.visitor.EndFilter (pc, Convert (pc, decision), data);
179                 }
180
181                 public Result EndFinally (APC pc, Data data)
182                 {
183                         return this.visitor.EndFinally (pc, data);
184                 }
185
186                 public Result Jmp (APC pc, Method method, Data data)
187                 {
188                         return this.visitor.Jmp (pc, method, data);
189                 }
190
191                 public Result LoadArg (APC pc, Parameter argument, bool isOld, SymbolicValue dest, Data data)
192                 {
193                         return this.visitor.LoadArg (pc, argument, isOld, dest, data);
194                 }
195
196                 public Result LoadArgAddress (APC pc, Parameter argument, bool isOld, SymbolicValue dest, Data data)
197                 {
198                         return this.visitor.LoadArgAddress (pc, argument, isOld, dest, data);
199                 }
200
201                 public Result LoadLocal (APC pc, Local local, SymbolicValue dest, Data data)
202                 {
203                         return this.visitor.LoadLocal (pc, local, dest, data);
204                 }
205
206                 public Result LoadLocalAddress (APC pc, Local local, SymbolicValue dest, Data data)
207                 {
208                         return this.visitor.LoadLocalAddress (pc, local, dest, data);
209                 }
210
211                 public Result Nop (APC pc, Data data)
212                 {
213                         return this.visitor.Nop (pc, data);
214                 }
215
216                 public Result Pop (APC pc, SymbolicValue source, Data data)
217                 {
218                         return this.visitor.Pop (pc, Convert (pc, source), data);
219                 }
220
221                 public Result Return (APC pc, SymbolicValue source, Data data)
222                 {
223                         return this.visitor.Return (pc, Convert (pc, source), data);
224                 }
225
226                 public Result StoreArg (APC pc, Parameter argument, SymbolicValue source, Data data)
227                 {
228                         return this.visitor.StoreArg (pc, argument, Convert (pc, source), data);
229                 }
230
231                 public Result StoreLocal (APC pc, Local local, SymbolicValue source, Data data)
232                 {
233                         return this.visitor.StoreLocal (pc, local, Convert (pc, source), data);
234                 }
235
236                 public Result Switch (APC pc, TypeNode type, IEnumerable<Pair<object, APC>> cases, SymbolicValue value, Data data)
237                 {
238                         throw new Exception ("Should not get branches at this level of abstraction.");
239                 }
240
241                 public Result Box (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue source, Data data)
242                 {
243                         return this.visitor.Box (pc, type, dest, Convert (pc, source), data);
244                 }
245
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>
249                 {
250                         return this.visitor.ConstrainedCallvirt (pc, method, constraint, extraVarargs, dest, Convert (pc, args), data);
251                 }
252
253                 public Result CastClass (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue obj, Data data)
254                 {
255                         return this.visitor.CastClass (pc, type, dest, Convert (pc, obj), data);
256                 }
257
258                 public Result CopyObj (APC pc, TypeNode type, SymbolicValue destPtr, SymbolicValue sourcePtr, Data data)
259                 {
260                         return this.visitor.CopyObj (pc, type, Convert (pc, destPtr), Convert (pc, sourcePtr), data);
261                 }
262
263                 public Result Initobj (APC pc, TypeNode type, SymbolicValue ptr, Data data)
264                 {
265                         return this.visitor.Initobj (pc, type, Convert (pc, ptr), data);
266                 }
267
268                 public Result LoadElement (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue array, SymbolicValue index, Data data)
269                 {
270                         return this.visitor.LoadElement (pc, type, dest, Convert (pc, array), Convert (pc, index), data);
271                 }
272
273                 public Result LoadField (APC pc, Field field, SymbolicValue dest, SymbolicValue obj, Data data)
274                 {
275                         return this.visitor.LoadField (pc, field, dest, Convert (pc, obj), data);
276                 }
277
278                 public Result LoadFieldAddress (APC pc, Field field, SymbolicValue dest, SymbolicValue obj, Data data)
279                 {
280                         return this.visitor.LoadFieldAddress (pc, field, dest, Convert (pc, obj), data);
281                 }
282
283                 public Result LoadLength (APC pc, SymbolicValue dest, SymbolicValue array, Data data)
284                 {
285                         return this.visitor.LoadLength (pc, dest, Convert (pc, array), data);
286                 }
287
288                 public Result LoadStaticField (APC pc, Field field, SymbolicValue dest, Data data)
289                 {
290                         return this.visitor.LoadStaticField (pc, field, dest, data);
291                 }
292
293                 public Result LoadStaticFieldAddress (APC pc, Field field, SymbolicValue dest, Data data)
294                 {
295                         return this.visitor.LoadStaticFieldAddress (pc, field, dest, data);
296                 }
297
298                 public Result LoadTypeToken (APC pc, TypeNode type, SymbolicValue dest, Data data)
299                 {
300                         return this.visitor.LoadTypeToken (pc, type, dest, data);
301                 }
302
303                 public Result LoadFieldToken (APC pc, Field type, SymbolicValue dest, Data data)
304                 {
305                         return this.visitor.LoadFieldToken (pc, type, dest, data);
306                 }
307
308                 public Result LoadMethodToken (APC pc, Method type, SymbolicValue dest, Data data)
309                 {
310                         return this.visitor.LoadMethodToken (pc, type, dest, data);
311                 }
312
313                 public Result NewArray<ArgList> (APC pc, TypeNode type, SymbolicValue dest, ArgList lengths, Data data) where ArgList : IIndexable<SymbolicValue>
314                 {
315                         return this.visitor.NewArray (pc, type, dest, Convert (pc, lengths), data);
316                 }
317
318                 public Result NewObj<ArgList> (APC pc, Method ctor, SymbolicValue dest, ArgList args, Data data) where ArgList : IIndexable<SymbolicValue>
319                 {
320                         return this.visitor.NewObj (pc, ctor, dest, Convert (pc, args), data);
321                 }
322
323                 public Result MkRefAny (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue obj, Data data)
324                 {
325                         return this.visitor.MkRefAny (pc, type, dest, Convert (pc, obj), data);
326                 }
327
328                 public Result RefAnyType (APC pc, SymbolicValue dest, SymbolicValue source, Data data)
329                 {
330                         return this.visitor.RefAnyType (pc, dest, Convert (pc, source), data);
331                 }
332
333                 public Result RefAnyVal (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue source, Data data)
334                 {
335                         return this.visitor.RefAnyVal (pc, type, dest, Convert (pc, source), data);
336                 }
337
338                 public Result Rethrow (APC pc, Data data)
339                 {
340                         return this.visitor.Rethrow (pc, data);
341                 }
342
343                 public Result StoreElement (APC pc, TypeNode type, SymbolicValue array, SymbolicValue index, SymbolicValue value, Data data)
344                 {
345                         return this.visitor.StoreElement (pc, type, Convert (pc, array), Convert (pc, index), Convert (pc, value), data);
346                 }
347
348                 public Result StoreField (APC pc, Field field, SymbolicValue obj, SymbolicValue value, Data data)
349                 {
350                         return this.visitor.StoreField (pc, field, Convert (pc, obj), Convert (pc, value), data);
351                 }
352
353                 public Result StoreStaticField (APC pc, Field field, SymbolicValue value, Data data)
354                 {
355                         return this.visitor.StoreStaticField (pc, field, Convert (pc, value), data);
356                 }
357
358                 public Result Throw (APC pc, SymbolicValue exception, Data data)
359                 {
360                         return this.visitor.Throw (pc, Convert (pc, exception), data);
361                 }
362
363                 public Result Unbox (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue obj, Data data)
364                 {
365                         return this.visitor.Unbox (pc, type, dest, Convert (pc, obj), data);
366                 }
367
368                 public Result UnboxAny (APC pc, TypeNode type, SymbolicValue dest, SymbolicValue obj, Data data)
369                 {
370                         return this.visitor.UnboxAny (pc, type, dest, Convert (pc, obj), data);
371                 }
372                 #endregion
373
374                 private static LabeledSymbol<APC, SymbolicValue> Convert (APC pc, SymbolicValue value)
375                 {
376                         return new LabeledSymbol<APC, SymbolicValue> (pc, value);
377                 }
378
379                 private static ArgumentWrapper<ArgList> Convert<ArgList> (APC pc, ArgList value)
380                         where ArgList : IIndexable<SymbolicValue>
381                 {
382                         return new ArgumentWrapper<ArgList> (value, pc);
383                 }
384
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;
390
391                         public ArgumentWrapper (ArgList underlying, APC readAt)
392                         {
393                                 this.underlying = underlying;
394                                 this.readAt = readAt;
395                         }
396
397                         #region Implementation of IIndexable<ExternalExpression<APC,SymbolicValue>>
398                         public int Count
399                         {
400                                 get { return this.underlying.Count; }
401                         }
402
403                         public LabeledSymbol<APC, SymbolicValue> this [int index]
404                         {
405                                 get { return new LabeledSymbol<APC, SymbolicValue> (this.readAt, this.underlying [index]); }
406                         }
407                         #endregion
408                 }
409                 #endregion
410         }
411 }