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

   1 //
   2 // SimpleLogicInference.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 Mono.CodeContracts.Static.AST;
  31 using Mono.CodeContracts.Static.Analysis;
  32 using Mono.CodeContracts.Static.ControlFlow;
  33
  34 namespace Mono.CodeContracts.Static.Proving {
  35         class SimpleLogicInference<Expression, Variable> : BasicFacts<Expression, Variable> {
  36                 public SimpleLogicInference (IExpressionContextProvider<Expression, Variable> contextProvider, IFactBase<Variable> factBase, Predicate<APC> isUnreachable)
  37                         : base (contextProvider, factBase, isUnreachable)
  38                 {
  39                 }
  40
  41                 public override ProofOutcome IsNull (APC pc, BoxedExpression expr)
  42                 {
  43                         Variable v;
  44                         if (TryVariable (expr, out v)) {
  45                                 ProofOutcome proofOutcome = this.FactBase.IsNull (pc, v);
  46                                 if (proofOutcome != ProofOutcome.Top)
  47                                         return proofOutcome;
  48                         }
  49
  50                         if (expr.IsConstant) {
  51                                 object constant = expr.Constant;
  52                                 if (constant == null)
  53                                         return ProofOutcome.True;
  54                                 if (constant is string)
  55                                         return ProofOutcome.False;
  56                                 var convertible = constant as IConvertible;
  57                                 if (convertible != null) {
  58                                         try {
  59                                                 return (convertible.ToInt64 (null) == 0) ? ProofOutcome.True : ProofOutcome.False;
  60                                         } catch {
  61                                                 return ProofOutcome.Top;
  62                                         }
  63                                 }
  64                         }
  65
  66                         BinaryOperator op;
  67                         BoxedExpression left;
  68                         BoxedExpression right;
  69                         if (expr.IsBinaryExpression (out op, out left, out right)) {
  70                                 if ((op == BinaryOperator.Ceq || op == BinaryOperator.Cobjeq) && IsNull (pc, right) == ProofOutcome.True)
  71                                         return IsNonNull (pc, left);
  72                                 if (op == BinaryOperator.Cne_Un && IsNull (pc, right) == ProofOutcome.True)
  73                                         return IsNull (pc, left);
  74                         }
  75                         return ProofOutcome.Top;
  76                 }
  77
  78                 public override ProofOutcome IsNonNull (APC pc, BoxedExpression expr)
  79                 {
  80                         Variable v;
  81                         if (TryVariable (expr, out v)) {
  82                                 ProofOutcome proofOutcome = this.FactBase.IsNonNull (pc, v);
  83                                 if (proofOutcome != ProofOutcome.Top)
  84                                         return proofOutcome;
  85                         }
  86
  87                         if (expr.IsConstant) {
  88                                 object constant = expr.Constant;
  89                                 if (constant == null)
  90                                         return ProofOutcome.False;
  91                                 if (constant is string)
  92                                         return ProofOutcome.True;
  93                                 var convertible = constant as IConvertible;
  94                                 if (convertible != null) {
  95                                         try {
  96                                                 return (convertible.ToInt64 (null) == 0) ? ProofOutcome.False : ProofOutcome.True;
  97                                         } catch {
  98                                                 return ProofOutcome.Top;
  99                                         }
 100                                 }
 101                         }
 102
 103                         BinaryOperator op;
 104                         BoxedExpression left;
 105                         BoxedExpression right;
 106                         if (expr.IsBinaryExpression (out op, out left, out right)) {
 107                                 if ((op == BinaryOperator.Ceq || op == BinaryOperator.Cobjeq) && IsNull (pc, right) == ProofOutcome.True)
 108                                         return IsNull (pc, left);
 109                                 if (op == BinaryOperator.Cne_Un && IsNull (pc, right) == ProofOutcome.True)
 110                                         return IsNonNull (pc, left);
 111                         }
 112                         return ProofOutcome.Top;
 113                 }
 114         }
 115 }