5 // Alexander Chebaturkin (chebaturkin@gmail.com)
7 // Copyright (C) 2011 Alexander Chebaturkin
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:
17 // The above copyright notice and this permission notice shall be
18 // included in all copies or substantial portions of the Software.
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.
30 using System.Collections.Generic;
33 using Mono.CodeContracts.Static.AST;
34 using Mono.CodeContracts.Static.AST.Visitors;
35 using Mono.CodeContracts.Static.ControlFlow.Blocks;
36 using Mono.CodeContracts.Static.ControlFlow.Subroutines.Builders;
37 using Mono.CodeContracts.Static.DataStructures;
38 using Mono.CodeContracts.Static.Providers;
40 namespace Mono.CodeContracts.Static.ControlFlow.Subroutines {
41 class SubroutineFacade : IMethodCodeConsumer<Dummy, Subroutine> {
42 public readonly IContractProvider ContractProvider;
43 public readonly IMetaDataProvider MetaDataProvider;
45 // private readonly EnsuresFactory ensures_factory;
46 private readonly Dictionary<Method, ICFG> method_cache = new Dictionary<Method, ICFG> ();
47 private readonly RequiresFactory requires_factory;
49 public SubroutineFacade (IMetaDataProvider metaDataProvider,
50 IContractProvider contractProvider)
52 this.MetaDataProvider = metaDataProvider;
53 this.ContractProvider = contractProvider;
54 this.requires_factory = new RequiresFactory (this);
55 // this.ensures_factory = new EnsuresFactory (this);
58 #region IMethodCodeConsumer<Dummy,Subroutine> Members
59 Subroutine IMethodCodeConsumer<Dummy, Subroutine>.Accept<Label, Handler> (
60 IMethodCodeProvider<Label, Handler> codeProvider,
65 var builder = new SubroutineWithHandlersBuilder<Label, Handler> (codeProvider, this, method, entry);
66 return new MethodSubroutine<Label, Handler> (this, method, entry, builder);
70 public TResult ForwardDecode<TData, TResult, TVisitor> (APC pc, TVisitor visitor, TData data)
71 where TVisitor : IILVisitor<APC, Dummy, Dummy, TData, TResult>
73 var block = pc.Block as BlockBase;
75 return block.ForwardDecode<TData, TResult, TVisitor> (pc, visitor, data);
77 return visitor.Nop (pc, data);
80 public Subroutine GetRequires (Method method)
82 method = this.MetaDataProvider.Unspecialized (method);
83 return this.requires_factory.Get (method);
86 public Subroutine GetEnsures (Method method)
89 //todo: implement handling this in MethodSubroutine and uncomment lines below
91 // method = this.MetaDataProvider.Unspecialized (method);
92 // return this.ensures_factory.Get (method);
95 public Subroutine GetInvariant (TypeNode type)
97 //todo: implement this
101 public ICFG GetControlFlowGraph (Method method)
103 if (this.method_cache.ContainsKey (method))
104 return this.method_cache [method];
106 if (!this.MetaDataProvider.HasBody (method))
107 throw new InvalidOperationException ("Method has no body");
109 return new ControlFlowGraph (this.MetaDataProvider.AccessMethodBody (method, this, Dummy.Value), this);
112 public void AddReads (Method method, Field field)
114 throw new NotImplementedException ();
117 public IEnumerable<Method> GetAffectedGetters (Field field)
119 //todo: implement this
121 return new Method[0];
124 public IEnumerable<Field> GetModifies (Method method)
126 //todo: implement this
127 return Enumerable.Empty<Field> ();