mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.ControlFlow.Subroutines/EnsuresSubroutine.cs

   1 //
   2 // EnsuresSubroutine.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.ControlFlow.Blocks;
  33 using Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders;
  34 using Mono.CodeContracts.Static.DataStructures;
  35
  36 namespace Mono.CodeContracts.Static.ControlFlow.Subroutines {
  37         sealed class EnsuresSubroutine<Label> : MethodContractSubroutine<Label>, IEquatable<EnsuresSubroutine<Label>> {
  38                 private readonly Dictionary<int, Pair<CFGBlock, TypeNode>> inferred_old_label_reverse_map;
  39
  40                 public EnsuresSubroutine (SubroutineFacade subroutineFacade,
  41                                           Method method, IImmutableSet<Subroutine> inherited) : base (subroutineFacade, method)
  42                 {
  43                         this.inferred_old_label_reverse_map = new Dictionary<int, Pair<CFGBlock, TypeNode>> ();
  44                         AddSuccessor (Entry, EdgeTag.Entry, Exit);
  45                         AddBaseEnsures (Entry, Exit, inherited);
  46                         Commit ();
  47                 }
  48
  49                 public EnsuresSubroutine (SubroutineFacade subroutineFacade,
  50                                           Method method,
  51                                           SimpleSubroutineBuilder<Label> builder, Label startLabel, IImmutableSet<Subroutine> inherited)
  52                         : base (subroutineFacade, method, builder, startLabel)
  53                 {
  54                         this.inferred_old_label_reverse_map = new Dictionary<int, Pair<CFGBlock, TypeNode>> ();
  55                         AddBaseEnsures (Entry, GetTargetBlock (startLabel), inherited);
  56                 }
  57
  58                 public override SubroutineKind Kind
  59                 {
  60                         get { return SubroutineKind.Ensures; }
  61                 }
  62
  63                 public override bool IsEnsures
  64                 {
  65                         get { return true; }
  66                 }
  67
  68                 public override bool IsContract
  69                 {
  70                         get { return true; }
  71                 }
  72
  73                 #region IEquatable<EnsuresSubroutine<Label>> Members
  74                 public bool Equals (EnsuresSubroutine<Label> other)
  75                 {
  76                         return Id == other.Id;
  77                 }
  78                 #endregion
  79
  80                 private void AddBaseEnsures (CFGBlock from, CFGBlock to, IImmutableSet<Subroutine> inherited)
  81                 {
  82                         if (inherited == null)
  83                                 return;
  84                         foreach (Subroutine subroutine in inherited.Elements)
  85                                 AddEdgeSubroutine (from, to, subroutine, EdgeTag.Inherited);
  86                 }
  87
  88                 public override void Initialize ()
  89                 {
  90                         if (Builder == null)
  91                                 return;
  92                         Builder.BuildBlocks (this.StartLabel, this);
  93                         Commit ();
  94                         Builder = null;
  95                 }
  96
  97                 public override BlockWithLabels<Label> NewBlock ()
  98                 {
  99                         return new EnsuresBlock<Label> (this, ref this.BlockIdGenerator);
 100                 }
 101
 102                 public override void Commit ()
 103                 {
 104                         base.Commit ();
 105
 106                         var visitor = new OldScanStateMachine<Label> (this);
 107                         EnsuresBlock<Label> priorBlock = null;
 108
 109                         foreach (CFGBlock block in Blocks) {
 110                                 var ensuresBlock = block as EnsuresBlock<Label>;
 111                                 if (ensuresBlock != null) {
 112                                         priorBlock = ensuresBlock;
 113                                         int count = ensuresBlock.Count;
 114                                         visitor.StartBlock (ensuresBlock);
 115
 116                                         for (int i = 0; i < count; i++) {
 117                                                 if (ensuresBlock.OriginalForwardDecode<int, Boolean, OldScanStateMachine<Label>> (i, visitor, i))
 118                                                         ensuresBlock.AddInstruction (i);
 119                                         }
 120                                 } else
 121                                         visitor.HandlePotentialCallBlock (block as MethodCallBlock<Label>, priorBlock);
 122                                 foreach (CFGBlock succ in SuccessorBlocks (block))
 123                                         visitor.SetStartState (succ);
 124                         }
 125                 }
 126
 127                 public void AddInferredOldMap (int blockIndex, int instructionIndex, CFGBlock otherBlock, TypeNode endOldType)
 128                 {
 129                         this.inferred_old_label_reverse_map.Add (OverlayInstructionKey (blockIndex, instructionIndex), new Pair<CFGBlock, TypeNode> (otherBlock, endOldType));
 130                 }
 131
 132                 private static int OverlayInstructionKey (int blockIndex, int instructionIndex)
 133                 {
 134                         return (instructionIndex << 16) + blockIndex;
 135                 }
 136
 137                 public CFGBlock InferredBeginEndBijection (APC pc)
 138                 {
 139                         TypeNode endOldType;
 140                         return InferredBeginEndBijection (pc, out endOldType);
 141                 }
 142
 143                 public CFGBlock InferredBeginEndBijection (APC pc, out TypeNode endOldType)
 144                 {
 145                         Pair<CFGBlock, TypeNode> pair;
 146                         if (!this.inferred_old_label_reverse_map.TryGetValue (OverlayInstructionKey (pc.Block.Index, pc.Index), out pair))
 147                                 throw new InvalidOperationException ("Fatal bug in ensures CFG begin/end old map");
 148                         endOldType = pair.Value;
 149                         return pair.Key;
 150                 }
 151         }
 152 }