2 // Analysis.GenericValueAnalysis.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.
30 using System.Collections.Generic;
33 using Mono.CodeContracts.Static.AST;
34 using Mono.CodeContracts.Static.AST.Visitors;
35 using Mono.CodeContracts.Static.Analysis.Drivers;
36 using Mono.CodeContracts.Static.ControlFlow;
37 using Mono.CodeContracts.Static.DataFlowAnalysis;
38 using Mono.CodeContracts.Static.DataStructures;
39 using Mono.CodeContracts.Static.Lattices;
40 using Mono.CodeContracts.Static.Providers;
41 using Mono.CodeContracts.Static.Proving;
43 namespace Mono.CodeContracts.Static.Analysis.Numerical {
44 static partial class AnalysisFacade {
45 static partial class Bind<TVar, TExpr> where TExpr : IEquatable<TExpr> where TVar : IEquatable<TVar> {
46 abstract class GenericValueAnalysis<TDomain> :
47 ILVisitorBase<APC, TVar, TVar, TDomain, TDomain>,
48 IAbstractAnalysis<TDomain, TVar>,
50 where TDomain : IEnvironmentDomain<TDomain, BoxedVariable<TVar>, BoxedExpression> {
51 readonly IMethodDriver<TExpr, TVar> method_driver;
52 //readonly string method_name;
54 protected ConstantEvaluator EvaluatorOfConstants;
56 protected IFixPointInfo<APC, TDomain> FixPointInfo;
57 BoxedExpressionDecoder<TVar, TExpr> expression_decoder;
59 protected GenericValueAnalysis (string methodName,
60 IMethodDriver<TExpr, TVar> methodDriver)
63 BoxedVariable<TVar>.ResetFreshVariableCounter ();
65 // method_name = methodName;
66 method_driver = methodDriver;
68 EvaluatorOfConstants = new ConstantEvaluator (ContextProvider,
72 protected IExpressionContextProvider<TExpr, TVar> ContextProvider { get { return method_driver.ContextProvider; } }
73 protected IMetaDataProvider MetaDataProvider { get { return method_driver.MetaDataProvider; } }
75 protected BoxedExpressionDecoder<TVar, TExpr> ExpressionDecoder
79 if (expression_decoder == null)
81 new BoxedExpressionDecoder<TVar, TExpr> (
82 new ValueExpressionDecoder<TVar, TExpr> (
85 return expression_decoder;
89 public IILVisitor<APC, TVar, TVar, TDomain, TDomain> GetVisitor ()
94 public TDomain Join (Pair<APC, APC> edge, TDomain newstate, TDomain prevstate,
95 out bool weaker, bool widen)
99 result = Join (newstate, prevstate, edge);
103 result = Widen (newstate, prevstate, edge);
104 weaker = !result.LessEqual (prevstate);
110 public TDomain ImmutableVersion (TDomain arg)
115 public TDomain MutableVersion (TDomain arg)
120 public virtual TDomain EdgeConversion (APC @from, APC to, bool isJoinPoint,
121 IImmutableMap<TVar, Sequence<TVar>>
122 sourceTargetMap, TDomain state)
127 public bool IsBottom (APC pc, TDomain state)
129 return state.IsBottom;
132 public Predicate<APC> SaveFixPointInfo (IFixPointInfo<APC, TDomain> fixPointInfo)
134 FixPointInfo = fixPointInfo;
138 public void Dump (Pair<TDomain, TextWriter> pair)
140 pair.Value.WriteLine (pair.Key.ToString ());
143 public abstract TDomain TopValue ();
145 public TDomain BottomValue ()
147 return TopValue ().Bottom;
150 public abstract IFactQuery<BoxedExpression, TVar> FactQuery (
151 IFixPointInfo<APC, TDomain> fixpoint);
153 IFactQuery<BoxedExpression, TVar> IMethodAnalysisFixPoint<TVar>.FactQuery { get { return FactQuery (FixPointInfo); } }
155 public FlatDomain<bool> ValidateExplicitAssertion (APC pc, TVar value)
157 return FlatDomain<bool>.TopValue;
160 public IMethodAnalysis MethodAnalysis { get; set; }
162 public void ValidateImplicitAssertions (IFactQuery<BoxedExpression, TVar> facts,
163 List<string> proofResults)
167 protected virtual TDomain Widen (TDomain newState, TDomain prevState,
170 return newState.Widen (prevState);
173 protected virtual TDomain Join (TDomain newState, TDomain prevState, Pair<APC, APC> edge)
175 return newState.Join (prevState);
178 public override TDomain Assume (APC pc, EdgeTag tag, TVar condition, TDomain data)
180 var boxed = ToBoxedExpression (pc, condition);
181 if (tag != EdgeTag.False) {
183 if (boxed.IsTrivialCondition (out value))
184 return !value ? data.Bottom : data;
187 List<int> thresholds;
188 if (ThresholdDB.TryGetAThreshold (boxed, expression_decoder, out thresholds))
189 ThresholdDB.Add (thresholds);
194 case EdgeTag.Requires:
196 case EdgeTag.Invariant:
197 result = data.AssumeTrue (boxed);
200 result = data.AssumeFalse (boxed);
207 if (tag != EdgeTag.False) {
209 ContextProvider.ValueContext.GetType (
210 ContextProvider.MethodContext.CFG.Post (pc), condition);
211 if (abstractType.IsNormal () &&
212 MetaDataProvider.Equal (abstractType.Value,
213 MetaDataProvider.System_Boolean)) {
215 BoxedExpression.Binary (BinaryOperator.Ceq, boxed,
216 BoxedExpression.Const (1,
221 result = result.AssumeTrue (guard);
228 public override TDomain Assert (APC pc, EdgeTag tag, TVar condition, TDomain data)
230 var boxed = ToBoxedExpression (pc, condition);
233 if (boxed.IsTrivialCondition (out result))
234 return result ? data : data.Bottom;
236 data = data.AssumeTrue (boxed);
239 ContextProvider.ValueContext.GetType (
240 ContextProvider.MethodContext.CFG.Post (pc), condition);
241 if (type.IsNormal () &&
242 MetaDataProvider.Equal (type.Value, MetaDataProvider.System_Boolean)) {
244 BoxedExpression.Binary (BinaryOperator.Ceq, boxed,
245 BoxedExpression.Const (1,
249 data = data.AssumeTrue (guard);
255 public override TDomain DefaultVisit (APC pc, TDomain data)
260 protected BoxedExpression ToBoxedExpression (APC pc, TVar condition)
263 BoxedExpression.For (
264 ContextProvider.ExpressionContext.Refine (pc, condition),
265 ExpressionDecoder.ExternalDecoder);
268 public IFactQuery<BoxedExpression, TVar> FactQuery ()
270 return FactQuery (FixPointInfo);