mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/BoxedExpressionExtensions.cs

   1 //
   2 // BoxedExpressionExtensions.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
  31 using Mono.CodeContracts.Static.AST;
  32 using Mono.CodeContracts.Static.DataStructures;
  33
  34 namespace Mono.CodeContracts.Static.Proving
  35 {
  36         static class BoxedExpressionExtensions
  37         {
  38                 public static bool IsConstantIntOrNull(this BoxedExpression e, out int res)
  39                 {
  40                         res = 0;
  41                         if (e.IsConstant) {
  42                                 IConvertible convertible = e.Constant as IConvertible;
  43                                 if (convertible != null) {
  44                                         if (e.Constant is string || e.Constant is float || e.Constant is double)
  45                                                 return false;
  46
  47                                         try {
  48                                                 res = convertible.ToInt32 (null);
  49                                                 return true;
  50                                         } catch {
  51                                         }
  52                                 }
  53                                 if (e.Constant == null)
  54                                         return true;
  55                         }
  56                         return false;
  57                 }
  58
  59                 public static bool IsConstantBool(this BoxedExpression e, out bool result)
  60                 {
  61                         if (e.IsConstant && e.Constant is bool)
  62                                 return true.With ((bool) e.Constant, out result);
  63
  64                         return false.Without (out result);
  65                 }
  66
  67                 public static bool IsTrivialCondition(this BoxedExpression e, out bool result)
  68                 {
  69                         int value;
  70                         if (e.IsConstantIntOrNull (out value))
  71                                 return true.With (value != 0, out result);
  72                         if (e.IsConstantBool (out result))
  73                                 return true;
  74
  75                         BinaryOperator bop;
  76                         BoxedExpression left;
  77                         BoxedExpression right;
  78                         if (e.IsBinaryExpression (out bop, out left, out right)) {
  79                                 int l, r;
  80                                 var isLeftInt = left.IsConstantIntOrNull (out l);
  81                                 var isRightInt = right.IsConstantIntOrNull (out r);
  82                                 if (bop == BinaryOperator.Ceq) {
  83                                         if (isLeftInt && isRightInt)
  84                                                 return true.With (l == r, out result);
  85                                         bool leftResult;
  86                                         if (isRightInt && r == 0 && left.IsTrivialCondition (out leftResult))
  87                                                 return true.With (!leftResult, out result);
  88
  89                                         bool rightResult;
  90                                         if (isLeftInt && l == 0 && right.IsTrivialCondition (out rightResult))
  91                                                 return true.With (!rightResult, out result);
  92
  93                                         return false.Without (out result);
  94                                 }
  95
  96                                 switch (bop) {
  97                                         case BinaryOperator.Add:
  98                                         case BinaryOperator.Add_Ovf:
  99                                         case BinaryOperator.Add_Ovf_Un:
 100                                                 return true.With (l + r != 0, out result);
 101                                         case BinaryOperator.And:
 102                                                 return true.With ((l & r) != 0, out result);
 103                                         case BinaryOperator.Cne_Un:
 104                                                 return true.With (l != r, out result);
 105                                         case BinaryOperator.Cge:
 106                                                 return true.With (l >= r, out result);
 107                                         case BinaryOperator.Cge_Un:
 108                                                 return true.With ((uint) l >= (uint) r, out result);
 109                                         case BinaryOperator.Cgt:
 110                                                 return true.With (l > r, out result);
 111                                         case BinaryOperator.Cgt_Un:
 112                                                 return true.With ((uint) l > (uint) r, out result);
 113                                         case BinaryOperator.Cle:
 114                                                 return true.With (l <= r, out result);
 115                                         case BinaryOperator.Cle_Un:
 116                                                 return true.With ((uint) l <= (uint) r, out result);
 117                                         case BinaryOperator.Clt:
 118                                                 return true.With (l < r, out result);
 119                                         case BinaryOperator.Clt_Un:
 120                                                 return true.With ((uint) l < (uint) r, out result);
 121                                         case BinaryOperator.Div:
 122                                                 if (r == 0)
 123                                                         return false.Without (out result);
 124                                                 return true.With (l / r != 0, out result);
 125                                         case BinaryOperator.Div_Un:
 126                                                 if (r == 0)
 127                                                         return false.Without (out result);
 128                                                 return true.With ((uint) l / (uint) r != 0, out result);
 129                                         case BinaryOperator.LogicalAnd:
 130                                                 return true.With (l != 0 && r != 0, out result);
 131                                         case BinaryOperator.LogicalOr:
 132                                                 return true.With (l != 0 || r != 0, out result);
 133                                         case BinaryOperator.Mul:
 134                                         case BinaryOperator.Mul_Ovf:
 135                                         case BinaryOperator.Mul_Ovf_Un:
 136                                                 return true.With (l * r != 0, out result);
 137                                         case BinaryOperator.Or:
 138                                                 return true.With ((l | r) != 0, out result);
 139                                         case BinaryOperator.Rem:
 140                                                 if (r == 0)
 141                                                         return false.Without (out result);
 142                                                 return true.With (l % r != 0, out result);
 143                                         case BinaryOperator.Rem_Un:
 144                                                 if (r == 0)
 145                                                         return false.Without (out result);
 146                                                 return true.With (((uint) l) % ((uint) r) != 0, out result);
 147                                         case BinaryOperator.Shl:
 148                                                 return true.With (l << r != 0, out result);
 149                                         case BinaryOperator.Shr:
 150                                                 return true.With (l >> r != 0, out result);
 151                                         case BinaryOperator.Shr_Un:
 152                                                 return true.With (((uint) l) >> r != 0, out result);
 153                                         case BinaryOperator.Sub:
 154                                         case BinaryOperator.Sub_Ovf:
 155                                         case BinaryOperator.Sub_Ovf_Un:
 156                                                 return true.With (l - r != 0, out result);
 157                                         case BinaryOperator.Xor:
 158                                                 return true.With ((l ^ r) != 0, out result);
 159                                         default:
 160                                                 return false.Without (out result);
 161                                 }
 162                         }
 163
 164                         return false.Without (out result);
 165                 }
 166         }
 167 }