mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.DataFlowAnalysis/ForwardAnalysis.cs

   1 //
   2 // ForwardAnalysis.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.IO;
  31 using Mono.CodeContracts.Static.AST.Visitors;
  32 using Mono.CodeContracts.Static.Analysis;
  33 using Mono.CodeContracts.Static.ControlFlow;
  34 using Mono.CodeContracts.Static.DataStructures;
  35 using Mono.CodeContracts.Static.Providers;
  36
  37 namespace Mono.CodeContracts.Static.DataFlowAnalysis {
  38         class ForwardAnalysis<AState, EdgeData> :
  39                 ForwardDataFlowAnalysisBase<AState>,
  40                 IFixPointInfo<APC, AState> {
  41                 private readonly Action<Pair<AState, TextWriter>> dumper;
  42                 private readonly EdgeConverter<APC, AState, EdgeData> edge_converter;
  43                 private readonly Func<APC, APC, EdgeData> edge_data_getter;
  44                 private readonly Func<AState, AState> immutable_version;
  45                 private readonly Func<APC, AState, bool> is_bottom;
  46                 private readonly Joiner<APC, AState> joiner;
  47                 private readonly Func<AState, AState> mutable_version;
  48                 private readonly Func<APC, AState, AState> transfer;
  49
  50                 public ForwardAnalysis (ICFG cfg,
  51                                         Func<APC, AState, AState> transfer,
  52                                         Joiner<APC, AState> joiner,
  53                                         Func<AState, AState> immutableVersion,
  54                                         Func<AState, AState> mutableVersion,
  55                                         EdgeConverter<APC, AState, EdgeData> edgeConverter,
  56                                         Func<APC, APC, EdgeData> edgeDataGetter,
  57                                         Func<APC, AState, bool> isBottom,
  58                                         Action<Pair<AState, TextWriter>> dumper) : base (cfg)
  59                 {
  60                         this.transfer = transfer;
  61                         this.joiner = joiner;
  62                         this.immutable_version = immutableVersion;
  63                         this.mutable_version = mutableVersion;
  64                         this.edge_converter = edgeConverter;
  65                         this.edge_data_getter = edgeDataGetter;
  66                         this.is_bottom = isBottom;
  67                         this.dumper = dumper;
  68                 }
  69
  70                 #region IFixPointInfo<APC,AbstractState> Members
  71                 public bool PreStateLookup (APC pc, out AState state)
  72                 {
  73                         return GetPreState (pc, out state);
  74                 }
  75
  76                 public bool PostStateLookup (APC pc, out AState state)
  77                 {
  78                         return GetPostState (pc, out state);
  79                 }
  80                 #endregion
  81
  82                 public static ForwardAnalysis<AState, EdgeData> Make<Source, Dest, Context> (
  83                         IILDecoder<APC, Source, Dest, Context, EdgeData> decoder,
  84                         IAnalysis<APC, AState, IILVisitor<APC, Source, Dest, AState, AState>, EdgeData> analysis)
  85                         where Context : IMethodContextProvider
  86                 {
  87                         IILVisitor<APC, Source, Dest, AState, AState> visitor = analysis.GetVisitor ();
  88                         var forwardAnalysisSolver = new ForwardAnalysis<AState, EdgeData> (
  89                                 decoder.ContextProvider.MethodContext.CFG,
  90                                 (pc, state) => decoder.ForwardDecode<AState, AState, IILVisitor<APC, Source, Dest, AState, AState>> (pc, visitor, state),
  91                                 analysis.Join,
  92                                 analysis.ImmutableVersion,
  93                                 analysis.MutableVersion,
  94                                 analysis.EdgeConversion,
  95                                 decoder.EdgeData,
  96                                 (pc, state) => {
  97                                         if (!decoder.IsUnreachable (pc))
  98                                                 return analysis.IsBottom (pc, state);
  99
 100                                         return true;
 101                                 },
 102                                 analysis.Dump
 103                                 );
 104
 105                         analysis.SaveFixPointInfo (forwardAnalysisSolver);
 106                         return forwardAnalysisSolver;
 107                 }
 108
 109                 protected override void Dump (AState state)
 110                 {
 111                         this.dumper (new Pair<AState, TextWriter> (state, Console.Out));
 112                 }
 113
 114                 protected override void PushState (APC from, APC next, AState state)
 115                 {
 116                         EdgeData data = this.edge_data_getter (from, next);
 117                         AState pushState = this.edge_converter (from, next, RequiresJoining (next), data, state);
 118                         base.PushState (from, next, pushState);
 119                 }
 120
 121                 protected override bool Join (Pair<APC, APC> edge, AState newState, AState existingState, out AState joinedState, bool widen)
 122                 {
 123                         bool weaker;
 124                         joinedState = this.joiner (edge, newState, existingState, out weaker, widen);
 125
 126                         return weaker;
 127                 }
 128
 129                 protected override bool IsBottom (APC pc, AState state)
 130                 {
 131                         return this.is_bottom (pc, state);
 132                 }
 133
 134                 protected override AState Transfer (APC pc, AState state)
 135                 {
 136                         AState resultState = this.transfer (pc, state);
 137
 138                         return resultState;
 139                 }
 140
 141                 protected override AState MutableVersion (AState state, APC at)
 142                 {
 143                         return this.mutable_version (state);
 144                 }
 145
 146                 protected override AState ImmutableVersion (AState state, APC at)
 147                 {
 148                         return this.immutable_version (state);
 149                 }
 150         }
 151 }