2 // AssumeTrueVisitor.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 using Mono.CodeContracts.Static.DataStructures;
30 using Mono.CodeContracts.Static.Lattices;
32 namespace Mono.CodeContracts.Static.Analysis.Numerical {
33 abstract class AssumeTrueVisitor<TDomain, TVar, TExpr> : GenericExpressionVisitor<TDomain, TDomain, TVar, TExpr>
34 where TDomain : IEnvironmentDomain<TDomain, TVar, TExpr> {
35 protected AssumeTrueVisitor (IExpressionDecoder<TVar, TExpr> decoder)
40 public AssumeFalseVisitor<TDomain, TVar, TExpr> FalseVisitor { get; set; }
42 protected override TDomain Default (TDomain data)
47 public override TDomain VisitConstant (TExpr left, TDomain data)
50 if (Decoder.TryValueOf (left, ExpressionType.Bool, out boolValue))
51 return boolValue ? data : data.Bottom;
54 if (Decoder.TryValueOf (left, ExpressionType.Int32, out intValue))
55 return intValue != 0 ? data : data.Bottom;
60 public override TDomain VisitLogicalAnd (TExpr left, TExpr right, TExpr original, TDomain data)
62 var leftIsVariable = Decoder.IsVariable (left);
63 var rightIsVariable = Decoder.IsVariable (right);
65 var leftIsConstant = Decoder.IsConstant (left);
66 var rightIsConstant = Decoder.IsConstant (right);
68 if (leftIsVariable && rightIsConstant || leftIsConstant && rightIsVariable)
71 return data.AssumeTrue (left).AssumeTrue (right);
74 public override TDomain VisitLogicalOr (TExpr left, TExpr right, TExpr original, TDomain data)
76 var leftIsVariable = Decoder.IsVariable (left);
77 var rightIsVariable = Decoder.IsVariable (right);
79 var leftIsConstant = Decoder.IsConstant (left);
80 var rightIsConstant = Decoder.IsConstant (right);
82 if (leftIsVariable && rightIsConstant || leftIsConstant && rightIsVariable)
85 var leftBranch = data.AssumeTrue (left);
86 var rightBranch = data.AssumeTrue (right);
88 return leftBranch.Join (rightBranch);
91 public override TDomain VisitNot (TExpr expr, TDomain data)
93 return FalseVisitor.Visit (expr, data);
96 protected override bool TryPolarity (TExpr expr, TDomain data, out bool shouldNegate)
98 if (base.TryPolarity (expr, data, out shouldNegate))
101 var holds = data.CheckIfHolds (expr);
102 if (!holds.IsNormal ())
103 return false.Without (out shouldNegate);
105 return true.With (!holds.Value, out shouldNegate);