mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static/Checker.cs

   1 //
   2 // Checker.cs
   3 //
   4 // Authors:
   5 //      Alexander Chebaturkin (chebaturkin@gmail.com)
   6 //
   7 // Copyright (C) 2011 Alexander Chebaturkin
   8 //
   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:
  16 //
  17 // The above copyright notice and this permission notice shall be
  18 // included in all copies or substantial portions of the Software.
  19 //
  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.
  27 //
  28
  29 using System;
  30 using System.Collections.Generic;
  31 using Mono.CodeContracts.Static.AST;
  32 using Mono.CodeContracts.Static.Analysis.Drivers;
  33 using Mono.CodeContracts.Static.Analysis.HeapAnalysis;
  34 using Mono.CodeContracts.Static.Analysis.NonNull;
  35 using Mono.CodeContracts.Static.Analysis.Numerical;
  36 using Mono.CodeContracts.Static.ControlFlow;
  37 using Mono.CodeContracts.Static.Providers;
  38 using Mono.CodeContracts.Static.Proving;
  39
  40 namespace Mono.CodeContracts.Static {
  41         public class Checker {
  42                 private readonly CheckOptions options;
  43                 private CodeContractsAnalysisDriver<IMethodResult<SymbolicValue>> analysis_driver;
  44                 private Dictionary<string, IMethodAnalysis> analyzers;
  45
  46                 private Checker (CheckOptions options)
  47                 {
  48                         this.options = options;
  49                 }
  50
  51                 public static CheckResults Check (CheckOptions options)
  52                 {
  53                         var checker = new Checker (options);
  54                         return checker.Analyze ();
  55                 }
  56
  57                 private CheckResults Analyze ()
  58                 {
  59                         if (this.options.Assembly == null)
  60                                 return CheckResults.Error ("No assembly given to check");
  61
  62                         DebugOptions.Debug = this.options.ShowDebug;
  63
  64                         this.analyzers = new Dictionary<string, IMethodAnalysis> {
  65                                 {"non-null", new NonNullAnalysisFacade ()},
  66                                 {"arithmetic", new Analysers.Arithmetic ()}
  67                         };
  68
  69                         this.analysis_driver = new CodeContractsAnalysisDriver<IMethodResult<SymbolicValue>> (
  70                                 new BasicAnalysisDriver (MetaDataProvider.Instance, CodeContractDecoder.Instance));
  71
  72                         return AnalyzeAssembly (this.options.Assembly);
  73                 }
  74
  75                 private CheckResults AnalyzeAssembly (string assemblyPath)
  76                 {
  77                         IMetaDataProvider metadataDecoder = this.analysis_driver.MetaDataProvider;
  78                         AssemblyNode assembly;
  79                         string reason;
  80                         if (!metadataDecoder.TryLoadAssembly (assemblyPath, out assembly, out reason))
  81                                 return CheckResults.Error (string.Format ("Cannot load assembly: {0}", reason));
  82
  83                         var proofResults = new Dictionary<string, ICollection<string>> ();
  84                         foreach (Method method in metadataDecoder.Methods (assembly))
  85                                 AnalyzeMethod (method, proofResults);
  86                         if (proofResults.Count == 0)
  87                                 return CheckResults.Error ("No methods found.");
  88
  89                         return new CheckResults (null, null, proofResults);
  90                 }
  91
  92                 private void AnalyzeMethod (Method method, Dictionary<string, ICollection<string>> proofResults)
  93                 {
  94                         IMetaDataProvider metadataDecoder = this.analysis_driver.MetaDataProvider;
  95                         if (!metadataDecoder.HasBody (method))
  96                                 return;
  97                         if (this.options.Method != null && !metadataDecoder.FullName (method).Contains (this.options.Method))
  98                                 return;
  99
 100                         var results = new List<string> ();
 101                         proofResults.Add (method.FullName, results);
 102                         try {
 103                                 AnalyzeMethodInternal (method, results);
 104                         } catch (Exception e) {
 105                                 results.Add ("Exception: " + e.Message);
 106                                 return;
 107                         }
 108
 109                         results.Add (string.Format ("Checked {0} assertions", results.Count));
 110                 }
 111
 112                 private void AnalyzeMethodInternal (Method method, List<string> proofResults)
 113                 {
 114                         string fullMethodName = method.FullName;
 115                         IMethodDriver<LabeledSymbol<APC, SymbolicValue>, SymbolicValue> methodDriver = this.analysis_driver.CreateMethodDriver (method);
 116
 117                         methodDriver.RunHeapAndExpressionAnalyses ();
 118
 119                         var results = new List<IMethodResult<SymbolicValue>> (this.analyzers.Values.Count);
 120                         foreach (IMethodAnalysis analysis in this.analyzers.Values) {
 121                                 IMethodResult<SymbolicValue> result = analysis.Analyze (fullMethodName, methodDriver);
 122                                 results.Add (result);
 123                         }
 124
 125                         ComposedFactQuery<SymbolicValue> facts = CreateFactQuery (methodDriver.BasicFacts.IsUnreachable, results);
 126                         foreach (var methodResult in results)
 127                                 methodResult.ValidateImplicitAssertions (facts, proofResults);
 128
 129                         AssertionFinder.ValidateAssertions (facts, methodDriver, proofResults);
 130                 }
 131
 132                 private ComposedFactQuery<Variable> CreateFactQuery<Variable> (Predicate<APC> isUnreachable, IEnumerable<IMethodResult<Variable>> results)
 133                 {
 134                         var res = new ComposedFactQuery<Variable> (isUnreachable);
 135                         res.Add (new ConstantPropagationFactQuery<Variable> ());
 136                         foreach (var methodResult in results)
 137                                 res.Add (methodResult.FactQuery);
 138                         return res;
 139                 }
 140         }
 141 }