2 // Analysis.GenericNumericalAnalysis.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
.Analysis
.Drivers
;
33 using Mono
.CodeContracts
.Static
.ControlFlow
;
34 using Mono
.CodeContracts
.Static
.DataFlowAnalysis
;
35 using Mono
.CodeContracts
.Static
.DataStructures
;
36 using Mono
.CodeContracts
.Static
.Lattices
;
37 using Mono
.CodeContracts
.Static
.Proving
;
39 namespace Mono
.CodeContracts
.Static
.Analysis
.Numerical
{
40 static partial class AnalysisFacade
{
41 static partial class Bind
<TVar
, TExpr
> where TExpr
: IEquatable
<TExpr
> where TVar
: IEquatable
<TVar
> {
42 class GenericNumericalAnalysis
:
43 GenericValueAnalysis
<INumericalEnvironmentDomain
<BoxedVariable
<TVar
>, BoxedExpression
>> {
44 readonly Analysers
.ArithmeticEnvironmentKind env_kind
;
46 public GenericNumericalAnalysis (string methodName
,
47 IMethodDriver
<TExpr
, TVar
> methodDriver
,
48 Analysers
.ArithmeticEnvironmentKind envKind
)
49 : base (methodName
, methodDriver
)
54 public override INumericalEnvironmentDomain
<BoxedVariable
<TVar
>, BoxedExpression
>
58 case Analysers
.ArithmeticEnvironmentKind
.Intervals
:
60 new IntervalEnvironment
<BoxedVariable
<TVar
>, BoxedExpression
> (
62 case Analysers
.ArithmeticEnvironmentKind
.DisIntervals
:
64 new DisIntervalEnvironment
<BoxedVariable
<TVar
>, BoxedExpression
>
67 throw new AbstractInterpretationException (
68 "Unknown arithmetic environment kind.");
72 public override IFactQuery
<BoxedExpression
, TVar
> FactQuery
74 <APC
, INumericalEnvironmentDomain
<BoxedVariable
<TVar
>, BoxedExpression
>
77 return new ConstantPropagationFactQuery
<TVar
> ();
80 public override INumericalEnvironmentDomain
<BoxedVariable
<TVar
>, BoxedExpression
> Entry
81 (APC pc
, Method method
,
82 INumericalEnvironmentDomain
<BoxedVariable
<TVar
>, BoxedExpression
> data
)
84 foreach (var param
in MetaDataProvider
.Parameters (method
).AsEnumerable ()) {
86 var readAt
= ContextProvider
.MethodContext
.CFG
.Post (pc
);
87 if (!ContextProvider
.ValueContext
.TryParameterValue (readAt
, param
, out variable
))
90 var abstractType
= ContextProvider
.ValueContext
.GetType (readAt
,
92 if (abstractType
.IsNormal () && MetaDataProvider
.IsPrimitive (abstractType
.Value
))
93 data
= SetInitialRange (variable
, abstractType
.Value
, data
);
99 INumericalEnvironmentDomain
<BoxedVariable
<TVar
>, BoxedExpression
> SetInitialRange
100 (TVar variable
, TypeNode type
,
101 INumericalEnvironmentDomain
<BoxedVariable
<TVar
>, BoxedExpression
> data
)
103 var interval
= Interval
.Ranges
.GetIntervalForType (type
,
105 if (interval
.IsNormal ())
106 data
= data
.AssumeVariableIn (new BoxedVariable
<TVar
> (variable
),