2 // AssumeFalseVisitor.cs
5 // Alexander Chebaturkin (chebaturkin@gmail.com)
7 // Copyright (C) 2012 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.
29 namespace Mono.CodeContracts.Static.Analysis.Numerical {
30 abstract class AssumeFalseVisitor<TDomain, TVar, TExpr> :
31 GenericExpressionVisitor<TDomain, TDomain, TVar, TExpr>
32 where TDomain : IEnvironmentDomain<TDomain, TVar, TExpr> {
33 protected AssumeFalseVisitor (IExpressionDecoder<TVar, TExpr> decoder)
38 public AssumeTrueVisitor<TDomain, TVar, TExpr> TrueVisitor { get; set; }
40 protected override TDomain Default (TDomain data)
45 public override TDomain VisitConstant (TExpr left, TDomain data)
48 if (Decoder.TryValueOf (left, ExpressionType.Bool, out boolValue))
49 return boolValue ? data : data.Bottom;
52 if (Decoder.TryValueOf (left, ExpressionType.Int32, out intValue))
53 return intValue != 0 ? data : data.Bottom;
58 public override TDomain VisitNot (TExpr expr, TDomain data)
60 return TrueVisitor.Visit (expr, data);
63 public override TDomain VisitEqual (TExpr left, TExpr right, TExpr original, TDomain data)
66 if (Decoder.TryValueOf (right, ExpressionType.Int32, out value) && value == 0)
67 // test (left :neq: 0) ==> test (left)
68 return TrueVisitor.Visit (left, data);
70 return TrueVisitor.VisitNotEqual (left, right, original, data);
73 public override TDomain VisitLessThan (TExpr left, TExpr right, TExpr original, TDomain data)
75 // !(left < right) ==> right <= left
76 return TrueVisitor.VisitLessEqualThan (right, left, original, data);
79 public override TDomain VisitLessEqualThan (TExpr left, TExpr right, TExpr original, TDomain data)
81 // !(left <= right) ==> right < left
82 return TrueVisitor.VisitLessThan (right, left, original, data);