mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.Drivers/CodeContractsAnalysisDriver.cs

   1 using System;
   2 using Mono.CodeContracts.Static.AST;
   3 using Mono.CodeContracts.Static.Analysis.ExpressionAnalysis;
   4 using Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Decoding;
   5 using Mono.CodeContracts.Static.Analysis.HeapAnalysis;
   6 using Mono.CodeContracts.Static.ControlFlow;
   7 using Mono.CodeContracts.Static.DataStructures;
   8 using Mono.CodeContracts.Static.Providers;
   9 using Mono.CodeContracts.Static.Proving;
  10
  11 namespace Mono.CodeContracts.Static.Analysis.Drivers {
  12         class CodeContractsAnalysisDriver<MethodResult>
  13                 : AnalysisDriver<LabeledSymbol<APC, SymbolicValue>, SymbolicValue> {
  14                 public CodeContractsAnalysisDriver (IBasicAnalysisDriver basicDriver)
  15                         : base (basicDriver)
  16                 {
  17                 }
  18
  19                 public override IMethodDriver<LabeledSymbol<APC, SymbolicValue>, SymbolicValue> CreateMethodDriver (Method method)
  20                 {
  21                         return new MethodDriver (method, this);
  22                 }
  23
  24                 #region Nested type: MethodDriver
  25                 private class MethodDriver : BasicMethodDriver,
  26                                              IMethodDriver<LabeledSymbol<APC, SymbolicValue>, SymbolicValue>,
  27                                              IFactBase<SymbolicValue> {
  28                         private Func<LabeledSymbol<APC, SymbolicValue>, string> expr2String;
  29                         private IFullExpressionDecoder<SymbolicValue, LabeledSymbol<APC, SymbolicValue>> expression_decoder;
  30                         private HeapAnalysis.HeapAnalysis heap_analysis;
  31
  32                         public MethodDriver (Method method,
  33                                              CodeContractsAnalysisDriver<MethodResult> parent)
  34                                 : base (method, parent)
  35                         {
  36                         }
  37
  38                         private new AnalysisDriver<LabeledSymbol<APC, SymbolicValue>, SymbolicValue> AnalysisDriver
  39                         {
  40                                 get { return (AnalysisDriver<LabeledSymbol<APC, SymbolicValue>, SymbolicValue>) base.AnalysisDriver; }
  41                         }
  42
  43                         #region IFactBase<SymbolicValue> Members
  44                         public ProofOutcome IsNull (APC pc, SymbolicValue variable)
  45                         {
  46                                 return ProofOutcome.Top;
  47                         }
  48
  49                         public ProofOutcome IsNonNull (APC pc, SymbolicValue variable)
  50                         {
  51                                 return ProofOutcome.Top;
  52                         }
  53
  54                         public bool IsUnreachable (APC pc)
  55                         {
  56                                 return this.heap_analysis.IsUnreachable (pc);
  57                         }
  58                         #endregion
  59
  60                         #region IMethodDriver<LabeledSymbol<APC,SymbolicValue>,SymbolicValue> Members
  61                         public ICodeLayer<SymbolicValue, SymbolicValue,
  62                                 IValueContextProvider<SymbolicValue>,
  63                                 IImmutableMap<SymbolicValue, LispList<SymbolicValue>>> ValueLayer { get; private set; }
  64
  65                         public ICodeLayer<LabeledSymbol<APC, SymbolicValue>, SymbolicValue,
  66                                 IExpressionContextProvider<LabeledSymbol<APC, SymbolicValue>, SymbolicValue>,
  67                                 IImmutableMap<SymbolicValue, LispList<SymbolicValue>>> ExpressionLayer { get; private set; }
  68
  69                         public ICodeLayer<SymbolicValue, SymbolicValue,
  70                                 IValueContextProvider<SymbolicValue>,
  71                                 IImmutableMap<SymbolicValue, LispList<SymbolicValue>>> HybridLayer { get; private set; }
  72
  73                         public IExpressionContextProvider<LabeledSymbol<APC, SymbolicValue>, SymbolicValue> ContextProvider
  74                         {
  75                                 get { return ExpressionLayer.ILDecoder.ContextProvider; }
  76                         }
  77
  78                         public IMetaDataProvider MetaDataProvider
  79                         {
  80                                 get { return RawLayer.MetaDataProvider; }
  81                         }
  82
  83                         public IFactBase<SymbolicValue> BasicFacts
  84                         {
  85                                 get { return this; }
  86                         }
  87
  88                         public IFullExpressionDecoder<SymbolicValue, LabeledSymbol<APC, SymbolicValue>> ExpressionDecoder
  89                         {
  90                                 get
  91                                 {
  92                                         if (this.expression_decoder == null)
  93                                                 this.expression_decoder =
  94                                                         new FullExpressionDecoder<SymbolicValue, LabeledSymbol<APC, SymbolicValue>>(MetaDataProvider, ContextProvider);
  95                                         return this.expression_decoder;
  96                                 }
  97                         }
  98
  99                         public void RunHeapAndExpressionAnalyses ()
 100                         {
 101                                 if (this.heap_analysis != null)
 102                                         return;
 103
 104                                 this.heap_analysis = new HeapAnalysis.HeapAnalysis (StackLayer);
 105                                 StackLayer.CreateForward (this.heap_analysis) (this.heap_analysis.InitialValue ());
 106
 107                                 ValueLayer = CodeLayerFactory.Create (
 108                                                                       this.heap_analysis.GetDecoder (StackLayer.ILDecoder), StackLayer.MetaDataProvider, StackLayer.ContractProvider,
 109                                                                       source => source.ToString (), dest => dest.ToString ());
 110                                 var expressionAnalysis = new ExpressionAnalysisFacade<SymbolicValue, IValueContextProvider<SymbolicValue>, IImmutableMap<SymbolicValue, LispList<SymbolicValue>>>
 111                                         (ValueLayer, this.heap_analysis.IsUnreachable);
 112                                 ValueLayer.CreateForward (expressionAnalysis.CreateExpressionAnalysis ()) (expressionAnalysis.InitialValue (SymbolicValue.GetUniqueKey));
 113
 114                                 if (DebugOptions.Debug)
 115                                 {
 116                                         Console.WriteLine ("------------Value based CFG-----------------");
 117                                         ValueLayer.ILDecoder.ContextProvider.MethodContext.CFG.Print (Console.Out, ValueLayer.Printer, null, null);
 118                                 }
 119
 120                                 IILDecoder
 121                                         <APC, LabeledSymbol<APC, SymbolicValue>, SymbolicValue, IExpressionContextProvider<LabeledSymbol<APC, SymbolicValue>, SymbolicValue>, IImmutableMap<SymbolicValue, LispList<SymbolicValue>>>
 122                                         decoder = expressionAnalysis.GetDecoder (ValueLayer.ILDecoder);
 123                                 this.expr2String = ExpressionPrinterFactory.Printer (decoder.ContextProvider, this);
 124                                 ExpressionLayer = CodeLayerFactory.Create (decoder, ValueLayer.MetaDataProvider, ValueLayer.ContractProvider,
 125                                                                            this.expr2String, ValueLayer.VariableToString);
 126
 127                                 if (DebugOptions.Debug)
 128                                 {
 129                                         Console.WriteLine ("------------Expression based CFG-------------");
 130                                         ExpressionLayer.ILDecoder.ContextProvider.MethodContext.CFG.Print (Console.Out, ExpressionLayer.Printer, null, null);
 131                                 }
 132
 133                                 HybridLayer = CodeLayerFactory.Create (ValueLayer.ILDecoder, ValueLayer.MetaDataProvider, ValueLayer.ContractProvider,
 134                                                                        ValueLayer.ExpressionToString,
 135                                                                        ValueLayer.VariableToString, ExpressionLayer.Printer);
 136                         }
 137
 138                         public int KeyConverter (SymbolicValue var)
 139                         {
 140                                 return SymbolicValue.GetUniqueKey (var);
 141                         }
 142                         #endregion
 143                                              }
 144                 #endregion
 145                 }
 146 }