2 // CodeContractsAnalysisDriver.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 Mono.CodeContracts.Static.AST;
31 using Mono.CodeContracts.Static.Analysis.ExpressionAnalysis;
32 using Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding;
33 using Mono.CodeContracts.Static.Analysis.HeapAnalysis;
34 using Mono.CodeContracts.Static.ControlFlow;
35 using Mono.CodeContracts.Static.DataStructures;
36 using Mono.CodeContracts.Static.Lattices;
37 using Mono.CodeContracts.Static.Providers;
38 using Mono.CodeContracts.Static.Proving;
40 namespace Mono.CodeContracts.Static.Analysis.Drivers {
41 class CodeContractsAnalysisDriver<MethodResult>
42 : AnalysisDriver<LabeledSymbol<APC, SymbolicValue>, SymbolicValue> {
43 public CodeContractsAnalysisDriver (IBasicAnalysisDriver basicDriver)
48 public override IMethodDriver<LabeledSymbol<APC, SymbolicValue>, SymbolicValue> CreateMethodDriver (Method method)
50 return new MethodDriver (method, this);
53 #region Nested type: MethodDriver
54 private class MethodDriver : BasicMethodDriver,
55 IMethodDriver<LabeledSymbol<APC, SymbolicValue>, SymbolicValue>,
56 IFactBase<SymbolicValue> {
57 private Func<LabeledSymbol<APC, SymbolicValue>, string> expr2String;
58 private IFullExpressionDecoder<SymbolicValue, LabeledSymbol<APC, SymbolicValue>> expression_decoder;
59 private HeapAnalysis.HeapAnalysis heap_analysis;
61 public MethodDriver (Method method,
62 CodeContractsAnalysisDriver<MethodResult> parent)
63 : base (method, parent)
67 private new AnalysisDriver<LabeledSymbol<APC, SymbolicValue>, SymbolicValue> AnalysisDriver
69 get { return (AnalysisDriver<LabeledSymbol<APC, SymbolicValue>, SymbolicValue>) base.AnalysisDriver; }
72 #region IFactBase<SymbolicValue> Members
73 public FlatDomain<bool> IsNull (APC pc, SymbolicValue variable)
75 return ProofOutcome.Top;
78 public FlatDomain<bool> IsNonNull(APC pc, SymbolicValue variable)
80 return ProofOutcome.Top;
83 public bool IsUnreachable (APC pc)
85 return this.heap_analysis.IsUnreachable (pc);
89 #region IMethodDriver<LabeledSymbol<APC,SymbolicValue>,SymbolicValue> Members
90 public ICodeLayer<SymbolicValue, SymbolicValue,
91 IValueContextProvider<SymbolicValue>,
92 IImmutableMap<SymbolicValue, Sequence<SymbolicValue>>> ValueLayer { get; private set; }
94 public ICodeLayer<LabeledSymbol<APC, SymbolicValue>, SymbolicValue,
95 IExpressionContextProvider<LabeledSymbol<APC, SymbolicValue>, SymbolicValue>,
96 IImmutableMap<SymbolicValue, Sequence<SymbolicValue>>> ExpressionLayer { get; private set; }
98 public ICodeLayer<SymbolicValue, SymbolicValue,
99 IValueContextProvider<SymbolicValue>,
100 IImmutableMap<SymbolicValue, Sequence<SymbolicValue>>> HybridLayer { get; private set; }
102 public IExpressionContextProvider<LabeledSymbol<APC, SymbolicValue>, SymbolicValue> ContextProvider
104 get { return ExpressionLayer.ILDecoder.ContextProvider; }
107 public IMetaDataProvider MetaDataProvider
109 get { return RawLayer.MetaDataProvider; }
112 public IFactBase<SymbolicValue> BasicFacts
117 public IFullExpressionDecoder<SymbolicValue, LabeledSymbol<APC, SymbolicValue>> ExpressionDecoder
121 if (this.expression_decoder == null)
122 this.expression_decoder =
123 new FullExpressionDecoder<SymbolicValue, LabeledSymbol<APC, SymbolicValue>>(MetaDataProvider, ContextProvider);
124 return this.expression_decoder;
128 public void RunHeapAndExpressionAnalyses ()
130 if (this.heap_analysis != null)
133 this.heap_analysis = new HeapAnalysis.HeapAnalysis (StackLayer);
134 StackLayer.CreateForward (this.heap_analysis) (this.heap_analysis.InitialValue ());
136 ValueLayer = CodeLayerFactory.Create (
137 this.heap_analysis.GetDecoder (StackLayer.ILDecoder), StackLayer.MetaDataProvider, StackLayer.ContractProvider,
138 source => source.ToString (), dest => dest.ToString ());
139 var expressionAnalysis = new ExpressionAnalysisFacade<SymbolicValue, IValueContextProvider<SymbolicValue>, IImmutableMap<SymbolicValue, Sequence<SymbolicValue>>>
140 (ValueLayer, this.heap_analysis.IsUnreachable);
141 ValueLayer.CreateForward (expressionAnalysis.CreateExpressionAnalysis ()) (expressionAnalysis.InitialValue (SymbolicValue.GetUniqueKey));
143 if (DebugOptions.Debug)
145 Console.WriteLine ("------------Value based CFG-----------------");
146 ValueLayer.ILDecoder.ContextProvider.MethodContext.CFG.Print (Console.Out, ValueLayer.Printer, null, null);
150 <APC, LabeledSymbol<APC, SymbolicValue>, SymbolicValue, IExpressionContextProvider<LabeledSymbol<APC, SymbolicValue>, SymbolicValue>, IImmutableMap<SymbolicValue, Sequence<SymbolicValue>>>
151 decoder = expressionAnalysis.GetDecoder (ValueLayer.ILDecoder);
152 this.expr2String = ExpressionPrinterFactory.Printer (decoder.ContextProvider, this);
153 ExpressionLayer = CodeLayerFactory.Create (decoder, ValueLayer.MetaDataProvider, ValueLayer.ContractProvider,
154 this.expr2String, ValueLayer.VariableToString);
156 if (DebugOptions.Debug)
158 Console.WriteLine ("------------Expression based CFG-------------");
159 ExpressionLayer.ILDecoder.ContextProvider.MethodContext.CFG.Print (Console.Out, ExpressionLayer.Printer, null, null);
162 HybridLayer = CodeLayerFactory.Create (ValueLayer.ILDecoder, ValueLayer.MetaDataProvider, ValueLayer.ContractProvider,
163 ValueLayer.ExpressionToString,
164 ValueLayer.VariableToString, ExpressionLayer.Printer);
167 public int KeyConverter (SymbolicValue var)
169 return SymbolicValue.GetUniqueKey (var);