1 // 2 // StackToSymbolicAdapter.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 using System.Collections.Generic; 29 using Mono.CodeContracts.Static.AST; 30 using Mono.CodeContracts.Static.AST.Visitors; 31 using Mono.CodeContracts.Static.ControlFlow; 32 using Mono.CodeContracts.Static.DataStructures; 33 34 namespace Mono.CodeContracts.Static.Analysis.HeapAnalysis { 35 struct StackToSymbolicAdapter<Data, Result, Visitor> : IILVisitor<APC, int, int, Data, Result> 36 where Visitor : IILVisitor<APC, SymbolicValue, SymbolicValue, Data, Result> { 37 private readonly Visitor delegatee; 38 private readonly HeapAnalysis parent; 39 StackToSymbolicAdapterMono.CodeContracts.Static.Analysis.HeapAnalysis.StackToSymbolicAdapter40 public StackToSymbolicAdapter (HeapAnalysis parent, Visitor delegatee) 41 { 42 this.parent = parent; 43 this.delegatee = delegatee; 44 } 45 PreStateLookupMono.CodeContracts.Static.Analysis.HeapAnalysis.StackToSymbolicAdapter46 private bool PreStateLookup (APC pc, out Domain domain) 47 { 48 return this.parent.PreStateLookup (pc, out domain); 49 } 50 PostStateLookupMono.CodeContracts.Static.Analysis.HeapAnalysis.StackToSymbolicAdapter51 private bool PostStateLookup (APC pc, out Domain domain) 52 { 53 return this.parent.PostStateLookup (pc, out domain); 54 } 55 ConvertSourceMono.CodeContracts.Static.Analysis.HeapAnalysis.StackToSymbolicAdapter56 private SymbolicValue ConvertSource (APC pc, int source) 57 { 58 Domain domain; 59 if (!PreStateLookup (pc, out domain) || domain.IsBottom) 60 return new SymbolicValue (); 61 if (source < 0) 62 return new SymbolicValue (domain.VoidAddr); 63 64 SymbolicValue sv; 65 domain.TryGetCorrespondingValueAbstraction (source, out sv); 66 return sv; 67 } 68 ConvertOldSourceMono.CodeContracts.Static.Analysis.HeapAnalysis.StackToSymbolicAdapter69 private SymbolicValue ConvertOldSource (APC pc, int source) 70 { 71 Domain domain; 72 if (!PreStateLookup (pc, out domain) || domain.IsBottom) 73 return new SymbolicValue (); 74 75 if (source < 0) 76 return new SymbolicValue (domain.VoidAddr); 77 78 Domain oldDomain = AnalysisDecoder.FindOldState (pc, domain); 79 if (oldDomain == null) 80 return new SymbolicValue (domain.VoidAddr); 81 82 SymbolicValue sv; 83 oldDomain.TryGetCorrespondingValueAbstraction (source, out sv); 84 return sv; 85 } 86 ConvertDestMono.CodeContracts.Static.Analysis.HeapAnalysis.StackToSymbolicAdapter87 private SymbolicValue ConvertDest (APC pc, int dest) 88 { 89 Domain domain; 90 if (!PostStateLookup (pc, out domain)) 91 return new SymbolicValue (); 92 93 SymbolicValue sv; 94 domain.TryGetCorrespondingValueAbstraction (dest, out sv); 95 return sv; 96 } 97 ConvertOldDestMono.CodeContracts.Static.Analysis.HeapAnalysis.StackToSymbolicAdapter98 private SymbolicValue ConvertOldDest (APC pc, int dest) 99 { 100 SymbolicValue sv = default(SymbolicValue); 101 Domain domain; 102 if (!PostStateLookup (pc, out domain)) 103 return sv; 104 105 domain.OldDomain.TryGetCorrespondingValueAbstraction (dest, out sv); 106 return sv; 107 } 108 ConvertSourceDerefMono.CodeContracts.Static.Analysis.HeapAnalysis.StackToSymbolicAdapter109 private SymbolicValue ConvertSourceDeref (APC pc, int source) 110 { 111 Domain domain; 112 if (!PreStateLookup (pc, out domain)) 113 return new SymbolicValue (); 114 if (source < 0) 115 return new SymbolicValue (domain.VoidAddr); 116 117 SymValue addr = domain.LoadValue (source); 118 if (!PostStateLookup (pc, out domain)) 119 return new SymbolicValue (); 120 121 return domain.TryLoadValue (addr); 122 } 123 TryConvertUnboxMono.CodeContracts.Static.Analysis.HeapAnalysis.StackToSymbolicAdapter124 private SymbolicValue TryConvertUnbox (APC pc, int source) 125 { 126 Domain domain; 127 if (!PreStateLookup (pc, out domain)) 128 return new SymbolicValue (); 129 130 if (source < 0) 131 return new SymbolicValue (domain.VoidAddr); 132 133 SymbolicValue sv; 134 if (!domain.TryGetUnboxedValue (source, out sv)) 135 domain.TryGetCorrespondingValueAbstraction (source, out sv); 136 return sv; 137 } 138 139 private ArgumentSourceWrapper<ArgList> ConvertSources<ArgList> (APC pc, ArgList args) 140 where ArgList : IIndexable<int> 141 { this.parent.GetPreStateMono.CodeContracts.Static.Analysis.HeapAnalysis.StackToSymbolicAdapter142 return new ArgumentSourceWrapper<ArgList> (args, this.parent.GetPreState (pc)); 143 } 144 InsideOld(APC pc)145 private bool InsideOld (APC pc) 146 { 147 Domain domain; 148 return PreStateLookup (pc, out domain) && domain.OldDomain != null; 149 } 150 151 #region Implementation of IExpressionILVisitor<APC,int,int,Data,Result> Binary(APC pc, BinaryOperator op, int dest, int operand1, int operand2, Data data)152 public Result Binary (APC pc, BinaryOperator op, int dest, int operand1, int operand2, Data data) 153 { 154 if (op != BinaryOperator.Cobjeq) { 155 return this.delegatee.Binary (pc, op, ConvertDest (pc, dest), 156 ConvertSource (pc, operand1), ConvertSource (pc, operand2), 157 data); 158 } 159 160 SymbolicValue op1 = TryConvertUnbox (pc, operand1); 161 SymbolicValue op2 = TryConvertUnbox (pc, operand2); 162 163 return this.delegatee.Binary (pc, op, ConvertDest (pc, dest), op1, op2, data); 164 } 165 Isinst(APC pc, TypeNode type, int dest, int obj, Data data)166 public Result Isinst (APC pc, TypeNode type, int dest, int obj, Data data) 167 { 168 return this.delegatee.Isinst (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data); 169 } 170 LoadNull(APC pc, int dest, Data polarity)171 public Result LoadNull (APC pc, int dest, Data polarity) 172 { 173 return this.delegatee.LoadNull (pc, ConvertDest (pc, dest), polarity); 174 } 175 LoadConst(APC pc, TypeNode type, object constant, int dest, Data data)176 public Result LoadConst (APC pc, TypeNode type, object constant, int dest, Data data) 177 { 178 return this.delegatee.LoadConst (pc, type, constant, ConvertDest (pc, dest), data); 179 } 180 Sizeof(APC pc, TypeNode type, int dest, Data data)181 public Result Sizeof (APC pc, TypeNode type, int dest, Data data) 182 { 183 return this.delegatee.Sizeof (pc, type, ConvertDest (pc, dest), data); 184 } 185 Unary(APC pc, UnaryOperator op, bool unsigned, int dest, int source, Data data)186 public Result Unary (APC pc, UnaryOperator op, bool unsigned, int dest, int source, Data data) 187 { 188 return this.delegatee.Unary (pc, op, unsigned, ConvertDest (pc, dest), ConvertSource (pc, source), data); 189 } 190 #endregion 191 192 #region Implementation of ISyntheticILVisitor<APC,int,int,Data,Result> Entry(APC pc, Method method, Data data)193 public Result Entry (APC pc, Method method, Data data) 194 { 195 return this.delegatee.Entry (pc, method, data); 196 } 197 Assume(APC pc, EdgeTag tag, int source, Data data)198 public Result Assume (APC pc, EdgeTag tag, int source, Data data) 199 { 200 return this.delegatee.Assume (pc, tag, ConvertSource (pc, source), data); 201 } 202 Assert(APC pc, EdgeTag tag, int source, Data data)203 public Result Assert (APC pc, EdgeTag tag, int source, Data data) 204 { 205 return this.delegatee.Assert (pc, tag, ConvertSource (pc, source), data); 206 } 207 BeginOld(APC pc, APC matchingEnd, Data data)208 public Result BeginOld (APC pc, APC matchingEnd, Data data) 209 { 210 return this.delegatee.BeginOld (pc, matchingEnd, data); 211 } 212 EndOld(APC pc, APC matchingBegin, TypeNode type, int dest, int source, Data data)213 public Result EndOld (APC pc, APC matchingBegin, TypeNode type, int dest, int source, Data data) 214 { 215 return this.delegatee.Nop (pc, data); 216 } 217 LoadStack(APC pc, int offset, int dest, int source, bool isOld, Data data)218 public Result LoadStack (APC pc, int offset, int dest, int source, bool isOld, Data data) 219 { 220 SymbolicValue src = isOld ? ConvertOldSource (pc, source) : ConvertSource (pc, source); 221 return this.delegatee.LoadStack (pc, offset, ConvertDest (pc, dest), src, isOld, data); 222 } 223 LoadStackAddress(APC pc, int offset, int dest, int source, TypeNode type, bool isOld, Data data)224 public Result LoadStackAddress (APC pc, int offset, int dest, int source, TypeNode type, bool isOld, Data data) 225 { 226 return this.delegatee.LoadStackAddress (pc, offset, ConvertDest (pc, dest), ConvertSource (pc, source), type, isOld, data); 227 } 228 LoadResult(APC pc, TypeNode type, int dest, int source, Data data)229 public Result LoadResult (APC pc, TypeNode type, int dest, int source, Data data) 230 { 231 return this.delegatee.LoadResult (pc, type, ConvertDest (pc, dest), ConvertSource (pc, source), data); 232 } 233 #endregion 234 235 #region Implementation of IILVisitor<APC,int,int,Data,Result> Arglist(APC pc, int dest, Data data)236 public Result Arglist (APC pc, int dest, Data data) 237 { 238 return this.delegatee.Arglist (pc, ConvertDest (pc, dest), data); 239 } 240 Branch(APC pc, APC target, bool leavesExceptionBlock, Data data)241 public Result Branch (APC pc, APC target, bool leavesExceptionBlock, Data data) 242 { 243 return this.delegatee.Branch (pc, target, leavesExceptionBlock, data); 244 } 245 BranchCond(APC pc, APC target, BranchOperator bop, int value1, int value2, Data data)246 public Result BranchCond (APC pc, APC target, BranchOperator bop, int value1, int value2, Data data) 247 { 248 return this.delegatee.BranchCond (pc, target, bop, ConvertSource (pc, value1), ConvertSource (pc, value2), data); 249 } 250 BranchTrue(APC pc, APC target, int cond, Data data)251 public Result BranchTrue (APC pc, APC target, int cond, Data data) 252 { 253 return this.delegatee.BranchTrue (pc, target, ConvertSource (pc, cond), data); 254 } 255 BranchFalse(APC pc, APC target, int cond, Data data)256 public Result BranchFalse (APC pc, APC target, int cond, Data data) 257 { 258 return this.delegatee.BranchFalse (pc, target, ConvertSource (pc, cond), data); 259 } 260 Break(APC pc, Data data)261 public Result Break (APC pc, Data data) 262 { 263 return this.delegatee.Break (pc, data); 264 } 265 266 public Result Call<TypeList, ArgList> (APC pc, Method method, bool virt, TypeList extraVarargs, int dest, ArgList args, Data data) 267 where TypeList : IIndexable<TypeNode> 268 where ArgList : IIndexable<int> 269 { 270 if (!this.parent.MetaDataProvider.IsVoidMethod (method) && InsideOld (pc)) 271 return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data); 272 273 return DelegateCall (pc, method, virt, extraVarargs, dest, args, data); 274 } 275 276 public Result Calli<TypeList, ArgList> (APC pc, TypeNode returnType, TypeList argTypes, bool instance, int dest, int functionPointer, ArgList args, Data data) 277 where TypeList : IIndexable<TypeNode> 278 where ArgList : IIndexable<int> 279 { 280 if (!this.parent.MetaDataProvider.IsVoid (returnType) && InsideOld (pc)) 281 return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data); 282 283 return this.delegatee.Calli (pc, returnType, argTypes, instance, 284 ConvertDest (pc, dest), ConvertSource (pc, functionPointer), 285 ConvertSources (pc, args), data); 286 } 287 CheckFinite(APC pc, int dest, int source, Data data)288 public Result CheckFinite (APC pc, int dest, int source, Data data) 289 { 290 return this.delegatee.CheckFinite (pc, ConvertDest (pc, dest), ConvertSource (pc, source), data); 291 } 292 CopyBlock(APC pc, int destAddress, int srcAddress, int len, Data data)293 public Result CopyBlock (APC pc, int destAddress, int srcAddress, int len, Data data) 294 { 295 return this.delegatee.CopyBlock (pc, ConvertSource (pc, destAddress), ConvertSource (pc, srcAddress), ConvertSource (pc, len), data); 296 } 297 EndFilter(APC pc, int decision, Data data)298 public Result EndFilter (APC pc, int decision, Data data) 299 { 300 return this.delegatee.EndFilter (pc, ConvertSource (pc, decision), data); 301 } 302 EndFinally(APC pc, Data data)303 public Result EndFinally (APC pc, Data data) 304 { 305 return this.delegatee.EndFinally (pc, data); 306 } 307 Jmp(APC pc, Method method, Data data)308 public Result Jmp (APC pc, Method method, Data data) 309 { 310 return this.delegatee.Jmp (pc, method, data); 311 } 312 LoadArg(APC pc, Parameter argument, bool isOld, int dest, Data data)313 public Result LoadArg (APC pc, Parameter argument, bool isOld, int dest, Data data) 314 { 315 return this.delegatee.LoadArg (pc, argument, isOld, ConvertDest (pc, dest), data); 316 } 317 LoadArgAddress(APC pc, Parameter argument, bool isOld, int dest, Data data)318 public Result LoadArgAddress (APC pc, Parameter argument, bool isOld, int dest, Data data) 319 { 320 return this.delegatee.LoadArgAddress (pc, argument, isOld, ConvertDest (pc, dest), data); 321 } 322 LoadLocal(APC pc, Local local, int dest, Data data)323 public Result LoadLocal (APC pc, Local local, int dest, Data data) 324 { 325 return this.delegatee.LoadLocal (pc, local, ConvertDest (pc, dest), data); 326 } 327 LoadLocalAddress(APC pc, Local local, int dest, Data data)328 public Result LoadLocalAddress (APC pc, Local local, int dest, Data data) 329 { 330 return this.delegatee.LoadLocalAddress (pc, local, ConvertDest (pc, dest), data); 331 } 332 Nop(APC pc, Data data)333 public Result Nop (APC pc, Data data) 334 { 335 return this.delegatee.Nop (pc, data); 336 } 337 Pop(APC pc, int source, Data data)338 public Result Pop (APC pc, int source, Data data) 339 { 340 return this.delegatee.Pop (pc, ConvertSource (pc, source), data); 341 } 342 Return(APC pc, int source, Data data)343 public Result Return (APC pc, int source, Data data) 344 { 345 return this.delegatee.Return (pc, ConvertSource (pc, source), data); 346 } 347 StoreArg(APC pc, Parameter argument, int source, Data data)348 public Result StoreArg (APC pc, Parameter argument, int source, Data data) 349 { 350 return this.delegatee.StoreArg (pc, argument, ConvertSource (pc, source), data); 351 } 352 StoreLocal(APC pc, Local local, int source, Data data)353 public Result StoreLocal (APC pc, Local local, int source, Data data) 354 { 355 return this.delegatee.StoreLocal (pc, local, ConvertSource (pc, source), data); 356 } 357 Switch(APC pc, TypeNode type, IEnumerable<Pair<object, APC>> cases, int value, Data data)358 public Result Switch (APC pc, TypeNode type, IEnumerable<Pair<object, APC>> cases, int value, Data data) 359 { 360 return this.delegatee.Switch (pc, type, cases, ConvertSource (pc, value), data); 361 } 362 Box(APC pc, TypeNode type, int dest, int source, Data data)363 public Result Box (APC pc, TypeNode type, int dest, int source, Data data) 364 { 365 return this.delegatee.Box (pc, type, ConvertDest (pc, dest), ConvertSource (pc, source), data); 366 } 367 368 public Result ConstrainedCallvirt<TypeList, ArgList> (APC pc, Method method, TypeNode constraint, 369 TypeList extraVarargs, int dest, ArgList args, Data data) 370 where TypeList : IIndexable<TypeNode> 371 where ArgList : IIndexable<int> 372 { 373 return this.delegatee.ConstrainedCallvirt (pc, method, constraint, extraVarargs, 374 ConvertDest (pc, dest), ConvertSources (pc, args), data); 375 } 376 CastClass(APC pc, TypeNode type, int dest, int obj, Data data)377 public Result CastClass (APC pc, TypeNode type, int dest, int obj, Data data) 378 { 379 return this.delegatee.CastClass (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data); 380 } 381 CopyObj(APC pc, TypeNode type, int destPtr, int sourcePtr, Data data)382 public Result CopyObj (APC pc, TypeNode type, int destPtr, int sourcePtr, Data data) 383 { 384 return this.delegatee.CopyObj (pc, type, ConvertSource (pc, destPtr), ConvertSource (pc, sourcePtr), data); 385 } 386 Initobj(APC pc, TypeNode type, int ptr, Data data)387 public Result Initobj (APC pc, TypeNode type, int ptr, Data data) 388 { 389 return this.delegatee.Initobj (pc, type, ConvertSource (pc, ptr), data); 390 } 391 LoadElement(APC pc, TypeNode type, int dest, int array, int index, Data data)392 public Result LoadElement (APC pc, TypeNode type, int dest, int array, int index, Data data) 393 { 394 if (InsideOld (pc)) 395 return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data); 396 return this.delegatee.LoadElement (pc, type, ConvertDest (pc, dest), ConvertSource (pc, array), ConvertSource (pc, index), data); 397 } 398 LoadField(APC pc, Field field, int dest, int obj, Data data)399 public Result LoadField (APC pc, Field field, int dest, int obj, Data data) 400 { 401 if (InsideOld (pc)) 402 return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data); 403 404 return this.delegatee.LoadField (pc, field, ConvertDest (pc, dest), ConvertSource (pc, obj), data); 405 } 406 LoadFieldAddress(APC pc, Field field, int dest, int obj, Data data)407 public Result LoadFieldAddress (APC pc, Field field, int dest, int obj, Data data) 408 { 409 return this.delegatee.LoadFieldAddress (pc, field, ConvertDest (pc, dest), ConvertSource (pc, obj), data); 410 } 411 LoadLength(APC pc, int dest, int array, Data data)412 public Result LoadLength (APC pc, int dest, int array, Data data) 413 { 414 return this.delegatee.LoadLength (pc, ConvertDest (pc, dest), ConvertSource (pc, array), data); 415 } 416 LoadStaticField(APC pc, Field field, int dest, Data data)417 public Result LoadStaticField (APC pc, Field field, int dest, Data data) 418 { 419 if (InsideOld (pc)) 420 return this.delegatee.LoadStack (pc, 0, ConvertDest (pc, dest), ConvertOldDest (pc, dest), true, data); 421 422 return this.delegatee.LoadStaticField (pc, field, ConvertDest (pc, dest), data); 423 } 424 LoadStaticFieldAddress(APC pc, Field field, int dest, Data data)425 public Result LoadStaticFieldAddress (APC pc, Field field, int dest, Data data) 426 { 427 return this.delegatee.LoadStaticFieldAddress (pc, field, ConvertDest (pc, dest), data); 428 } 429 LoadTypeToken(APC pc, TypeNode type, int dest, Data data)430 public Result LoadTypeToken (APC pc, TypeNode type, int dest, Data data) 431 { 432 return this.delegatee.LoadTypeToken (pc, type, ConvertDest (pc, dest), data); 433 } 434 LoadFieldToken(APC pc, Field type, int dest, Data data)435 public Result LoadFieldToken (APC pc, Field type, int dest, Data data) 436 { 437 return this.delegatee.LoadFieldToken (pc, type, ConvertDest (pc, dest), data); 438 } 439 LoadMethodToken(APC pc, Method type, int dest, Data data)440 public Result LoadMethodToken (APC pc, Method type, int dest, Data data) 441 { 442 return this.delegatee.LoadMethodToken (pc, type, ConvertDest (pc, dest), data); 443 } 444 445 public Result NewArray<ArgList> (APC pc, TypeNode type, int dest, ArgList lengths, Data data) where ArgList : IIndexable<int> 446 { 447 return this.delegatee.NewArray (pc, type, ConvertDest (pc, dest), ConvertSources (pc, lengths), data); 448 } 449 450 public Result NewObj<ArgList> (APC pc, Method ctor, int dest, ArgList args, Data data) where ArgList : IIndexable<int> 451 { 452 return this.delegatee.NewObj (pc, ctor, ConvertDest (pc, dest), ConvertSources (pc, args), data); 453 } 454 MkRefAny(APC pc, TypeNode type, int dest, int obj, Data data)455 public Result MkRefAny (APC pc, TypeNode type, int dest, int obj, Data data) 456 { 457 return this.delegatee.MkRefAny (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data); 458 } 459 RefAnyType(APC pc, int dest, int source, Data data)460 public Result RefAnyType (APC pc, int dest, int source, Data data) 461 { 462 return this.delegatee.RefAnyType (pc, ConvertDest (pc, dest), ConvertSource (pc, source), data); 463 } 464 RefAnyVal(APC pc, TypeNode type, int dest, int source, Data data)465 public Result RefAnyVal (APC pc, TypeNode type, int dest, int source, Data data) 466 { 467 return this.delegatee.RefAnyVal (pc, type, ConvertDest (pc, dest), ConvertSource (pc, source), data); 468 } 469 Rethrow(APC pc, Data data)470 public Result Rethrow (APC pc, Data data) 471 { 472 return this.delegatee.Rethrow (pc, data); 473 } 474 StoreElement(APC pc, TypeNode type, int array, int index, int value, Data data)475 public Result StoreElement (APC pc, TypeNode type, int array, int index, int value, Data data) 476 { 477 return this.delegatee.StoreElement (pc, type, ConvertSource (pc, array), ConvertSource (pc, index), ConvertSource (pc, value), data); 478 } 479 StoreField(APC pc, Field field, int obj, int value, Data data)480 public Result StoreField (APC pc, Field field, int obj, int value, Data data) 481 { 482 return this.delegatee.StoreField (pc, field, ConvertSource (pc, obj), ConvertSource (pc, value), data); 483 } 484 StoreStaticField(APC pc, Field field, int value, Data data)485 public Result StoreStaticField (APC pc, Field field, int value, Data data) 486 { 487 return this.delegatee.StoreStaticField (pc, field, ConvertSource (pc, value), data); 488 } 489 Throw(APC pc, int exception, Data data)490 public Result Throw (APC pc, int exception, Data data) 491 { 492 return this.delegatee.Throw (pc, ConvertSource (pc, exception), data); 493 } 494 Unbox(APC pc, TypeNode type, int dest, int obj, Data data)495 public Result Unbox (APC pc, TypeNode type, int dest, int obj, Data data) 496 { 497 return this.delegatee.Unbox (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data); 498 } 499 UnboxAny(APC pc, TypeNode type, int dest, int obj, Data data)500 public Result UnboxAny (APC pc, TypeNode type, int dest, int obj, Data data) 501 { 502 return this.delegatee.UnboxAny (pc, type, ConvertDest (pc, dest), ConvertSource (pc, obj), data); 503 } 504 505 private Result DelegateCall<TypeList, ArgList> (APC pc, Method method, bool virt, TypeList extraVarargs, int dest, ArgList args, Data data) 506 where TypeList : IIndexable<TypeNode> 507 where ArgList : IIndexable<int> 508 { 509 TypeNode declaringType = this.parent.MetaDataProvider.DeclaringType (method); 510 if (args.Count == 2) { 511 string name = this.parent.MetaDataProvider.Name (method); 512 if (name == "Equals") { 513 return this.delegatee.Binary (pc, BinaryOperator.Cobjeq, 514 ConvertDest (pc, dest), 515 TryConvertUnbox (pc, args [0]), TryConvertUnbox (pc, args [1]), data); 516 } 517 518 if (this.parent.MetaDataProvider.IsReferenceType (declaringType)) { 519 if (name == "op_Inequality") { 520 return this.delegatee.Binary (pc, BinaryOperator.Cne_Un, 521 ConvertDest (pc, dest), 522 ConvertSource (pc, args [0]), ConvertSource (pc, args [1]), data); 523 } 524 if (name == "op_Equality") { 525 return this.delegatee.Binary (pc, BinaryOperator.Cobjeq, 526 ConvertDest (pc, dest), 527 ConvertSource (pc, args [0]), ConvertSource (pc, args [1]), data); 528 } 529 } 530 } 531 532 return this.delegatee.Call (pc, method, virt, extraVarargs, ConvertDest (pc, dest), ConvertSources (pc, args), data); 533 } 534 #endregion 535 536 #region Nested type: ArgumentSourceWrapper 537 private struct ArgumentSourceWrapper<ArgList> : IIndexable<SymbolicValue> 538 where ArgList : IIndexable<int> { 539 private readonly Domain state; 540 private readonly ArgList underlying; 541 ArgumentSourceWrapperMono.CodeContracts.Static.Analysis.HeapAnalysis.ArgumentSourceWrapper542 public ArgumentSourceWrapper (ArgList underlying, Domain state) 543 { 544 this.underlying = underlying; 545 this.state = state; 546 } 547 548 #region Implementation of IIndexable<SymbolicValue> 549 public int Count 550 { 551 get { return this.underlying.Count; } 552 } 553 554 public SymbolicValue this [int index] 555 { 556 get { return Map (this.underlying [index]); } 557 } 558 MapMono.CodeContracts.Static.Analysis.HeapAnalysis.ArgumentSourceWrapper559 private SymbolicValue Map (int i) 560 { 561 SymbolicValue sv = default(SymbolicValue); 562 if (this.state == null) 563 return sv; 564 565 this.state.TryGetCorrespondingValueAbstraction (i, out sv); 566 return sv; 567 } 568 #endregion 569 } 570 #endregion 571 } 572 } 573