2 // BoxedExpressionEncoder.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.
31 using Mono.CodeContracts.Static.AST;
32 using Mono.CodeContracts.Static.Providers;
33 using Mono.CodeContracts.Static.Proving;
35 namespace Mono.CodeContracts.Static.Analysis.Numerical {
36 class BoxedExpressionEncoder<TVar> : IExpressionEncoder<BoxedVariable<TVar>, BoxedExpression> {
37 readonly IMetaDataProvider metadata;
39 public BoxedExpressionEncoder (IMetaDataProvider metadata)
41 this.metadata = metadata;
44 public void ResetFreshVariableCounter ()
46 BoxedVariable<TVar>.ResetFreshVariableCounter ();
49 public BoxedVariable<TVar> FreshVariable ()
51 return BoxedVariable<TVar>.SlackVariable ();
54 public BoxedExpression VariableFor (BoxedVariable<TVar> var)
56 return BoxedExpression.Var (var);
59 public BoxedExpression ConstantFor (object value)
62 return BoxedExpression.Const (value, metadata.System_Int32);
65 var val = (long) value;
66 return val < int.MaxValue && val > int.MinValue
67 ? BoxedExpression.Const (val, metadata.System_Int32)
68 : BoxedExpression.Const (val, metadata.System_Int64);
72 return BoxedExpression.Const (value, metadata.System_Int16);
74 return BoxedExpression.Const (value, metadata.System_Int8);
76 return BoxedExpression.Const (value, metadata.System_Boolean);
78 throw new NotSupportedException ();
81 public BoxedExpression CompoundFor (ExpressionType type, ExpressionOperator op, BoxedExpression arg)
83 return BoxedExpression.Unary (ToUnaryOperator (op), arg);
86 public BoxedExpression CompoundFor (ExpressionType type, ExpressionOperator op, BoxedExpression left,
87 BoxedExpression right)
89 return BoxedExpression.Binary (ToBinaryOperator (op), left, right);
92 public static IExpressionEncoder<BoxedVariable<TVar>, BoxedExpression> Encoder (
93 IMetaDataProvider provider)
95 return new BoxedExpressionEncoder<TVar> (provider);
98 BinaryOperator ToBinaryOperator (ExpressionOperator op)
101 case ExpressionOperator.And:
102 return BinaryOperator.And;
103 case ExpressionOperator.Or:
104 return BinaryOperator.Or;
105 case ExpressionOperator.Xor:
106 return BinaryOperator.Xor;
107 case ExpressionOperator.Equal:
108 return BinaryOperator.Ceq;
109 case ExpressionOperator.Equal_Obj:
110 return BinaryOperator.Cobjeq;
111 case ExpressionOperator.NotEqual:
112 return BinaryOperator.Cne_Un;
113 case ExpressionOperator.LessThan:
114 return BinaryOperator.Clt;
115 case ExpressionOperator.LessEqualThan:
116 return BinaryOperator.Cle_Un;
117 case ExpressionOperator.GreaterThan:
118 return BinaryOperator.Cgt;
119 case ExpressionOperator.GreaterEqualThan:
120 return BinaryOperator.Cge;
121 case ExpressionOperator.Add:
122 return BinaryOperator.Add;
123 case ExpressionOperator.Sub:
124 return BinaryOperator.Sub;
125 case ExpressionOperator.Mult:
126 return BinaryOperator.Mul;
127 case ExpressionOperator.Div:
128 return BinaryOperator.Div;
129 case ExpressionOperator.Mod:
130 return BinaryOperator.Rem;
133 throw new ArgumentOutOfRangeException ("op");
137 UnaryOperator ToUnaryOperator (ExpressionOperator op)
140 case ExpressionOperator.Not:
141 return UnaryOperator.Not;
142 case ExpressionOperator.UnaryMinus:
143 return UnaryOperator.Neg;
145 throw new ArgumentOutOfRangeException ("op");