mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Analysis.ExpressionAnalysis/ValueAnalysis.cs

   1 using System;
   2 using System.IO;
   3 using Mono.CodeContracts.Static.AST.Visitors;
   4 using Mono.CodeContracts.Static.Analysis.ExpressionAnalysis.Expressions;
   5 using Mono.CodeContracts.Static.ControlFlow;
   6 using Mono.CodeContracts.Static.DataFlowAnalysis;
   7 using Mono.CodeContracts.Static.DataStructures;
   8 using Mono.CodeContracts.Static.Lattices;
   9
  10 namespace Mono.CodeContracts.Static.Analysis.ExpressionAnalysis {
  11         class ValueAnalysis<SymbolicValue, Context, EdgeData> : IAnalysis<APC, ExprDomain<SymbolicValue>,
  12                                                                          IILVisitor<APC, SymbolicValue, SymbolicValue, ExprDomain<SymbolicValue>, ExprDomain<SymbolicValue>>, EdgeData>
  13                         where SymbolicValue : IEquatable<SymbolicValue>
  14                         where Context : IValueContextProvider<SymbolicValue>
  15                         where EdgeData : IImmutableMap<SymbolicValue, LispList<SymbolicValue>> {
  16                 private readonly ExpressionAnalysisFacade<SymbolicValue, Context, EdgeData> parent;
  17
  18                 public ValueAnalysis (ExpressionAnalysisFacade<SymbolicValue, Context, EdgeData> parent)
  19                 {
  20                         this.parent = parent;
  21                 }
  22
  23                 #region Implementation of IAnalysis<APC,ExpressionAnalysis<Local,Parameter,Method,Field,Property,Event,Type,Attribute,Assembly,SymbolicValue,contextProvider,EdgeData>.Domain,IILVisitor<APC,Local,Parameter,Method,Field,Type,SymbolicValue,SymbolicValue,ExpressionAnalysis<Local,Parameter,Method,Field,Property,Event,Type,Attribute,Assembly,SymbolicValue,contextProvider,EdgeData>.Domain,ExpressionAnalysis<Local,Parameter,Method,Field,Property,Event,Type,Attribute,Assembly,SymbolicValue,contextProvider,EdgeData>.Domain>,EdgeData>
  24                 public ExprDomain<SymbolicValue> EdgeConversion (APC @from, APC to, bool isJoinPoint, EdgeData sourceTargetMap, ExprDomain<SymbolicValue> originalState)
  25                 {
  26                         if (sourceTargetMap == null)
  27                                 return originalState;
  28
  29                         if (DebugOptions.Debug)
  30                         {
  31                                 Console.WriteLine ("====Expression analysis Parallel assign====");
  32                                 DumpMap (sourceTargetMap);
  33                                 DumpExpressions ("original expressions", originalState);
  34                         }
  35
  36                         ExprDomain<SymbolicValue> result = originalState.Empty ();
  37                         ExprDomain<SymbolicValue> domain = originalState.Empty ();
  38
  39                         foreach (SymbolicValue sv in originalState.Keys) {
  40                                 Expr<SymbolicValue> expression = originalState [sv].Concrete.Substitute (sourceTargetMap);
  41                                 if (expression != null)
  42                                         domain = domain.Add (sv, expression);
  43                         }
  44
  45                         foreach (SymbolicValue sv in sourceTargetMap.Keys) {
  46                                 FlatDomain<Expr<SymbolicValue>> expressionDomain = domain [sv];
  47                                 if (expressionDomain.IsNormal) {
  48                                         Expr<SymbolicValue> expression = expressionDomain.Concrete;
  49                                         foreach (SymbolicValue sub in sourceTargetMap [sv].AsEnumerable ())
  50                                                 result = result.Add (sub, expression);
  51                                 }
  52                         }
  53
  54                         if (DebugOptions.Debug)
  55                         {
  56                                 DumpExpressions ("new expressions", result);
  57                         }
  58                         return result;
  59                 }
  60
  61                 public IILVisitor<APC, SymbolicValue, SymbolicValue, ExprDomain<SymbolicValue>, ExprDomain<SymbolicValue>> GetVisitor ()
  62                 {
  63                         return new AnalysisDecoder<SymbolicValue> ();
  64                 }
  65
  66                 public ExprDomain<SymbolicValue> Join (Pair<APC, APC> edge, ExprDomain<SymbolicValue> newstate, ExprDomain<SymbolicValue> prevstate, out bool weaker, bool widen)
  67                 {
  68                         return prevstate.Join (newstate, widen, out weaker);
  69                 }
  70
  71                 public ExprDomain<SymbolicValue> ImmutableVersion (ExprDomain<SymbolicValue> arg)
  72                 {
  73                         return arg;
  74                 }
  75
  76                 public ExprDomain<SymbolicValue> MutableVersion (ExprDomain<SymbolicValue> arg)
  77                 {
  78                         return arg;
  79                 }
  80
  81                 public bool IsBottom (APC pc, ExprDomain<SymbolicValue> state)
  82                 {
  83                         return state.IsBottom;
  84                 }
  85
  86                 public Predicate<APC> SaveFixPointInfo (IFixPointInfo<APC, ExprDomain<SymbolicValue>> fixPointInfo)
  87                 {
  88                         this.parent.SaveFixPointInfo (fixPointInfo);
  89                         return pc => true;
  90                 }
  91
  92                 public void Dump (Pair<ExprDomain<SymbolicValue>, TextWriter> pair)
  93                 {
  94                         pair.Key.Dump (pair.Value);
  95                 }
  96
  97                 private void DumpMap (IImmutableMap<SymbolicValue, LispList<SymbolicValue>> sourceTargetMap)
  98                 {
  99                         Console.WriteLine ("Source-Target assignment");
 100                         foreach (SymbolicValue key in sourceTargetMap.Keys) {
 101                                 foreach (SymbolicValue value in sourceTargetMap [key].AsEnumerable ())
 102                                         Console.Write ("{0} ", value);
 103                                 Console.WriteLine (" := {0}", key);
 104                         }
 105                 }
 106
 107                 private void DumpExpressions (string header, ExprDomain<SymbolicValue> state)
 108                 {
 109                         Console.WriteLine ("--- {0} ---", header);
 110                         foreach (SymbolicValue index in state.Keys) {
 111                                 FlatDomain<Expr<SymbolicValue>> domain = state [index];
 112                                 if (domain.IsNormal)
 113                                         Console.WriteLine ("{0} -> {1}", index, domain.Concrete);
 114                                 else if (domain.IsTop)
 115                                         Console.WriteLine ("{0} -> (Top)", index);
 116                                 else if (domain.IsBottom)
 117                                         Console.WriteLine ("{0} -> (Bot)", index);
 118                         }
 119                 }
 120                 #endregion
 121         }
 122 }