From: Florian Deljarry Date: Fri, 19 Apr 2019 21:41:23 +0000 (-0400) Subject: contracts: Adding all contract generation mechanism X-Git-Url: http://nitlanguage.org contracts: Adding all contract generation mechanism Signed-off-by: Florian Deljarry --- diff --git a/src/contracts.nit b/src/contracts.nit new file mode 100644 index 0000000..156bb53 --- /dev/null +++ b/src/contracts.nit @@ -0,0 +1,849 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +# Module to build contract +# This module provide extension of the modele to add contracts, the building phase and the "re-driving" to call the contract. +# +# FIXME Split the module in three parts: extension of the modele, building phase and the "re-driving" +module contracts + +import astbuilder +import parse_annotations +import phase +import semantize +intrude import modelize_property +intrude import scope +intrude import typing + +redef class ToolContext + # Parses contracts annotations. + var contracts_phase: Phase = new ContractsPhase(self, [modelize_property_phase,typing_phase]) +end + +private class ContractsPhase + super Phase + + # The entry point of the contract phase + # In reality, the contract phase is executed on each module + # FIXME: Actually all method is checked to add method if any contract is inherited + redef fun process_nmodule(nmodule)do + # Check if the contracts are disabled + if toolcontext.opt_no_contract.value then return + nmodule.do_contracts(self.toolcontext) + end +end + +redef class AModule + # Compile all contracts + # + # The implementation of the contracts is done in two visits. + # + # - First step, the visitor analyzes and constructs the contracts + # for each class (invariant) and method (expects, ensures). + # + # - Second step the visitor analyzes each `ASendExpr` to see + # if the callsite calls a method with a contract. If this is + # the case the callsite is replaced by another callsite to the contract method. + fun do_contracts(toolcontext: ToolContext) do + # + var contract_visitor = new ContractsVisitor(toolcontext, toolcontext.modelbuilder.identified_modules.first, self, new ASTBuilder(mmodule.as(not null))) + contract_visitor.enter_visit(self) + # + var callsite_visitor = new CallSiteVisitor(toolcontext) + callsite_visitor.enter_visit(self) + end +end + +# This visitor checks the `AMethPropdef` and the `AClassDef` to check if they have a contract annotation or it's a redefinition with a inheritance contract +private class ContractsVisitor + super Visitor + + var toolcontext: ToolContext + + # The main module + # It's strore to define if the contract need to be build depending on the selected policy `--no-contract` `--full-contract` or default + var mainmodule: MModule + + # Actual visited module + var visited_module: AModule + + var ast_builder: ASTBuilder + + # The `ASignature` of the actual build contract + var n_signature: ASignature is noinit + + # The `MSignature` of the actual build contract + var m_signature: MSignature is noinit + + # The `current_location` can corresponding of the annotation or method location. + var current_location: Location is noinit + + # Is the contrat is an introduction or not? + var is_intro_contract: Bool is noinit + + # Actual visited class + var visited_class: nullable AClassdef + + # is `no_contract` annotation was found + var find_no_contract = false + + redef fun visit(node) + do + node.create_contracts(self) + node.visit_all(self) + end + + # Method use to define the signature part of the method `ASignature` and `MSignature` + # The given `mcontract` provided `adapt_nsignature` and `adapt_msignature` to copy and adapt the given signature (`nsignature` and `msignature`) + fun define_signature(mcontract: MContract, nsignature: nullable ASignature, msignature: nullable MSignature) + do + if nsignature != null and msignature != null then nsignature.ret_type = msignature.return_mtype + self.n_signature = mcontract.adapt_nsignature(nsignature) + self.m_signature = mcontract.adapt_msignature(msignature) + end + + # Define the new contract take in consideration that an old contract exist or not + private fun build_contract(n_annotation: AAnnotation, mcontract: MContract, mclassdef: MClassDef): MMethodDef + do + self.current_location = n_annotation.location + # Retrieving the expression provided in the annotation + var n_condition = n_annotation.construct_condition(self) + var m_contractdef: AMethPropdef + if is_intro_contract then + # Create new contract method + m_contractdef = mcontract.create_intro_contract(self, n_condition, mclassdef) + else + # Create a redef of contract to take in consideration the new condition + m_contractdef = mcontract.create_subcontract(self, n_condition, mclassdef) + end + var contract_propdef = m_contractdef.mpropdef + # The contract has a null mpropdef, this should never happen + assert contract_propdef != null + return contract_propdef + end +end + +# This visitor checks the `callsite` to see if the target `mpropdef` has a contract. +private class CallSiteVisitor + super Visitor + + var toolcontext: ToolContext + + # Actual visited method + var visited_method: APropdef is noinit + + redef fun visit(node) + do + node.check_callsite(self) + node.visit_all(self) + end + + # Check if the callsite calls a method with a contract. + # If it's the case the callsite is replaced by another callsite to the contract method. + private fun drive_method_contract(callsite: CallSite): CallSite + do + if callsite.mpropdef.has_contract then + var contract_facet = callsite.mproperty.mcontract_facet + var visited_mpropdef = visited_method.mpropdef + assert contract_facet != null and visited_mpropdef != null + + var unsafe_mtype = callsite.recv.resolve_for(callsite.recv, callsite.anchor, visited_mpropdef.mclassdef.mmodule, false) + + # This check is needed because the contract can appear after the introduction. + if unsafe_mtype.has_mproperty(visited_method.mpropdef.mclassdef.mmodule, contract_facet) then + var type_visitor = new TypeVisitor(toolcontext.modelbuilder, visited_mpropdef) + var drived_callsite = type_visitor.build_callsite_by_property(visited_method, callsite.recv, contract_facet, callsite.recv_is_self) + # This never happen this check is here for debug + assert drived_callsite != null + return drived_callsite + end + end + return callsite + end +end + +redef class ANode + private fun create_contracts(v: ContractsVisitor) do end + private fun check_callsite(v: CallSiteVisitor) do end +end + +redef class AAnnotation + + # Returns the conditions of annotation parameters in the form of and expr + # exemple: + # the contract ensures(true, i == 10, f >= 1.0) + # return this condition (true and i == 10 and f >= 1.0) + private fun construct_condition(v : ContractsVisitor): AExpr + do + var n_condition = n_args.first + n_args.remove_at(0) + for n_arg in n_args do n_condition = v.ast_builder.make_and(n_condition, n_arg) + return n_condition + end +end + +# The root of all contracts +# +# The objective of this class is to provide the set +# of services must be implemented or provided by a contract +abstract class MContract + super MMethod + + # Define the name of the contract + fun contract_name: String is abstract + + # Checking if the use of the contract is necessary + private fun check_usage(v: ContractsVisitor, actual_mmodule: MModule): Bool is abstract + + # Method use to diplay warning when the contract is not present at the introduction + private fun no_intro_contract(v: ContractsVisitor, a: AAnnotation)do end + + # Creating specific inheritance block contract + private fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr is abstract + + # Method to adapt the `n_mpropdef.n_block` to the contract + private fun adapt_block_to_contract(v: ContractsVisitor, n_mpropdef: AMethPropdef) is abstract + + # Adapt the msignature specifically for the contract method + private fun adapt_specific_msignature(m_signature: MSignature): MSignature do return m_signature.adapt_to_condition + + # Adapt the nsignature specifically for the contract method + private fun adapt_specific_nsignature(n_signature: ASignature): ASignature do return n_signature.adapt_to_condition(null) + + # Adapt the `m_signature` to the contract + # If it is not null call the specific adapt `m_signature` for the contract + private fun adapt_msignature(m_signature: nullable MSignature): MSignature + do + if m_signature == null then return new MSignature(new Array[MParameter]) + return adapt_specific_msignature(m_signature) + end + + # Adapt the `n_signature` to the contract + # If it is not null call the specific adapt `n_signature` for the contract + private fun adapt_nsignature(n_signature: nullable ASignature): ASignature + do + if n_signature == null then return new ASignature + return adapt_specific_nsignature(n_signature) + end + + # Create a new empty contract + private fun create_empty_contract(v: ContractsVisitor, mclassdef: MClassDef, msignature: nullable MSignature, n_signature: ASignature) + do + var n_contract_def = intro_mclassdef.mclass.create_empty_method(v, self, mclassdef, msignature, n_signature) + n_contract_def.do_all(v.toolcontext) + end + + # Create the initial contract (intro) + # All contracts have the same implementation for the introduction. + # + # fun contrat([...]) + # do + # assert contract_condition + # end + # + private fun create_intro_contract(v: ContractsVisitor, n_condition: nullable AExpr, mclassdef: MClassDef): AMethPropdef + do + var n_block = v.ast_builder.make_block + if n_condition != null then + # Create a new tid to set the name of the assert for more explicit error + var tid = new TId.init_tk(self.location) + tid.text = "{self.contract_name}" + n_block.add v.ast_builder.make_assert(tid, n_condition, null) + end + return make_contract(v, n_block, mclassdef) + end + + # Create a contract with old (super) and the new conditions + private fun create_subcontract(v: ContractsVisitor, ncondition: nullable AExpr, mclassdef: MClassDef): AMethPropdef + do + var args = v.n_signature.make_parameter_read(v.ast_builder) + var n_block = v.ast_builder.make_block + if ncondition != null then n_block = self.create_nblock(v, ncondition, args) + return make_contract(v, n_block, mclassdef) + end + + # Build a method with a specific block `n_block` in a specified `mclassdef` + private fun make_contract(v: ContractsVisitor, n_block: AExpr, mclassdef: MClassDef): AMethPropdef + do + var n_contractdef = intro_mclassdef.mclass.create_empty_method(v, self, mclassdef, v.m_signature, v.n_signature) + n_contractdef.n_block = n_block + # Define the location of the new method for corresponding of the annotation location + n_contractdef.location = v.current_location + n_contractdef.do_all(v.toolcontext) + return n_contractdef + end +end + +# A expect (precondition) contract representation +# This method check if the requirements of the called method is true. +class MExpect + super MContract + + # Define the name of the contract + redef fun contract_name: String do return "expects" + + # Verification if the construction of the contract is necessary. + # Three cases are checked for `expects`: + # + # - Is the `--full-contract` option it's use? + # - Is the method is in the main package + # - Is the method is in a direct imported package. + # + redef fun check_usage(v: ContractsVisitor, actual_mmodule: MModule): Bool + do + var main_package = v.mainmodule.mpackage + var actual_package = actual_mmodule.mpackage + if main_package != null and actual_package != null then + var condition_direct_arc = v.toolcontext.modelbuilder.model.mpackage_importation_graph.has_arc(main_package, actual_package) + return v.toolcontext.opt_full_contract.value or condition_direct_arc or main_package == actual_package + end + return false + end + + # Display warning if no contract is defined at introduction `expect`, + # because if no contract is defined at the introduction the added + # contracts will not cause any error even if they are not satisfied. + # + # exemple + # ~~~nitish + # class A + # fun bar [...] + # fun _bar_expects([...]) + # do + # [empty contract] + # end + # end + # + # redef class A + # redef fun bar is expects(contract_condition) + # redef fun _bar_expects([...]) + # do + # if not (contract_condition) then super + # end + # end + # ~~~~ + # + redef fun no_intro_contract(v: ContractsVisitor, a: AAnnotation) + do + v.toolcontext.warning(a.location,"","Useless contract: No contract defined at the introduction of the method") + end + + redef fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr + do + # Creating the if expression with the new condition + var if_block = v.ast_builder.make_if(n_condition, n_condition.mtype) + # Creating and adding return expr to the then case + if_block.n_then = v.ast_builder.make_return(null) + # Creating the super call to the contract and adding this to else case + if_block.n_else = v.ast_builder.make_super_call(args,null) + var n_block = v.ast_builder.make_block + n_block.add if_block + return n_block + end + + redef fun adapt_block_to_contract(v: ContractsVisitor, n_mpropdef: AMethPropdef) + do + var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, self, true) + var n_self = new ASelfExpr + var args = n_mpropdef.n_signature.make_parameter_read(v.ast_builder) + var n_callexpect = v.ast_builder.make_call(n_self,callsite,args) + # Creation of the new instruction block with the call to expect condition + var actual_expr = n_mpropdef.n_block + var new_block = new ABlockExpr + new_block.n_expr.push n_callexpect + if actual_expr isa ABlockExpr then + new_block.n_expr.add_all(actual_expr.n_expr) + else if actual_expr != null then + new_block.n_expr.push(actual_expr) + end + n_mpropdef.n_block = new_block + end +end + +# The root of all contracts where the call is after the execution of the original method (`invariants` and `ensures`). +abstract class BottomMContract + super MContract + + # Verification if the construction of the contract is necessary. + # Two cases are checked for `expects`: + # + # - Is the `--full-contract` option it's use? + # - Is the method is in the main package + # + redef fun check_usage(v: ContractsVisitor, actual_mmodule: MModule): Bool + do + return v.toolcontext.opt_full_contract.value or v.mainmodule.mpackage == actual_mmodule.mpackage + end + + redef fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr + do + var tid = new TId.init_tk(v.current_location) + tid.text = "{contract_name}" + # Creating the assert expression with the new condition + var assert_block = v.ast_builder.make_assert(tid,n_condition,null) + # Creating the super call to the contract + var super_call = v.ast_builder.make_super_call(args,null) + # Define contract block + var n_block = v.ast_builder.make_block + # Adding the expressions to the block + n_block.add super_call + n_block.add assert_block + return n_block + end + + # Inject the result variable in the `n_block` of the given `n_mpropdef`. + private fun inject_result(v: ContractsVisitor, n_mpropdef: AMethPropdef, ret_type: MType): Variable + do + var actual_block = n_mpropdef.n_block + # never happen. If it's the case the problem is in the contract facet building + assert actual_block isa ABlockExpr + + var return_var: nullable Variable = null + + var return_expr = actual_block.n_expr.last.as(AReturnExpr) + + var returned_expr = return_expr.n_expr + # The return node has no returned expression + assert returned_expr != null + + # Check if the result variable already exit + if returned_expr isa AVarExpr then + if returned_expr.variable.name == "result" then + return_var = returned_expr.variable + end + end + + return_var = new Variable("result") + # Creating a new variable to keep the old return of the method + var assign_result = v.ast_builder.make_var_assign(return_var, returned_expr) + # Remove the actual return + actual_block.n_expr.pop + # Set the return type + return_var.declared_type = ret_type + # Adding the reading expr of result variable to the block + actual_block.add assign_result + # Expr to read the result variable + var read_result = v.ast_builder.make_var_read(return_var, ret_type) + # Definition of the new return + return_expr = v.ast_builder.make_return(read_result) + actual_block.add return_expr + return return_var + end +end + +# A ensure (postcondition) representation +# This method check if the called method respects the expectations of the caller. +class MEnsure + super BottomMContract + + # Define the name of the contract + redef fun contract_name: String do return "ensures" + + redef fun adapt_specific_msignature(m_signature: MSignature): MSignature + do + return m_signature.adapt_to_ensurecondition + end + + redef fun adapt_specific_nsignature(n_signature: ASignature): ASignature + do + return n_signature.adapt_to_ensurecondition + end + + redef fun adapt_block_to_contract(v: ContractsVisitor, n_mpropdef: AMethPropdef) + do + var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, self, true) + var n_self = new ASelfExpr + # argument to call the contract method + var args = n_mpropdef.n_signature.make_parameter_read(v.ast_builder) + # Inject the variable result + # The cast is always safe because the online adapted method is the contract facet + + var actual_block = n_mpropdef.n_block + # never happen. If it's the case the problem is in the contract facet building + assert actual_block isa ABlockExpr + + var ret_type = n_mpropdef.mpropdef.mproperty.intro.msignature.return_mtype + if ret_type != null then + var result_var = inject_result(v, n_mpropdef, ret_type) + # Expr to read the result variable + var read_result = v.ast_builder.make_var_read(result_var, ret_type) + var return_expr = actual_block.n_expr.pop + # Adding the read return to argument + args.add(read_result) + var n_callcontract = v.ast_builder.make_call(n_self,callsite,args) + actual_block.add_all([n_callcontract,return_expr]) + else + # build the call to the contract method + var n_callcontract = v.ast_builder.make_call(n_self,callsite,args) + actual_block.add n_callcontract + end + end +end + +redef class MClass + + # This method create an abstract method representation with this MMethodDef an this AMethoddef + private fun create_abstract_method(v: ContractsVisitor, mproperty: MMethod, mclassdef: MClassDef, msignature: nullable MSignature, n_signature: ASignature): AMethPropdef + do + # new methoddef definition + var m_def = new MMethodDef(mclassdef, mproperty, v.current_location) + # set the signature + if msignature != null then m_def.msignature = msignature.clone + # set the abstract flag + m_def.is_abstract = true + # Build the new node method + var n_def = v.ast_builder.make_method(null,null,m_def,n_signature,null,null,null,null) + # Define the location of the new method for corresponding of the actual method + n_def.location = v.current_location + # Association new npropdef to mpropdef + v.toolcontext.modelbuilder.unsafe_add_mpropdef2npropdef(m_def,n_def) + return n_def + end + + # Create method with an empty block + # the `mproperty` i.e the global property definition. The mclassdef to set where the method is declared and it's model `msignature` and ast `n_signature` signature + private fun create_empty_method(v: ContractsVisitor, mproperty: MMethod, mclassdef: MClassDef, msignature: nullable MSignature, n_signature: ASignature): AMethPropdef + do + var n_def = create_abstract_method(v, mproperty, mclassdef, msignature, n_signature) + n_def.mpropdef.is_abstract = false + n_def.n_block = v.ast_builder.make_block + return n_def + end +end + +redef class MMethod + + # The contract facet of the method + # it's representing the method with contract + # This method call the contract and the method + var mcontract_facet: nullable MMethod = null + + # The expected contract method + var mexpect: nullable MExpect = null + + # The ensure contract method + var mensure: nullable MEnsure = null + + # Check if the MMethod has no ensure contract + # if this is the case returns false and built it + # else return true + private fun check_exist_ensure: Bool + do + if self.mensure != null then return true + # build a new `MEnsure` contract + self.mensure = new MEnsure(intro_mclassdef, "_ensures_{name}", intro_mclassdef.location, public_visibility) + return false + end + + # Check if the MMethod has no expect contract + # if this is the case returns false and built it + # else return true + private fun check_exist_expect: Bool + do + if self.mexpect != null then return true + # build a new `MExpect` contract + self.mexpect = new MExpect(intro_mclassdef, "_expects_{name}", intro_mclassdef.location, public_visibility) + return false + end + + # Check if the MMethod has an contract facet + # If the method has no contract facet she create it + private fun check_exist_contract_facet(mpropdef : MMethodDef): Bool + do + if self.mcontract_facet != null then return true + # build a new `MMethod` contract + self.mcontract_facet = new MMethod(mpropdef.mclassdef, "_contract_{name}", mpropdef.mclassdef.location, public_visibility) + return false + end +end + +redef class MMethodDef + + # Verification of the contract facet + # Check if a contract facet already exists to use it again or if it is necessary to create it. + private fun check_contract_facet(v: ContractsVisitor, n_signature: ASignature, mcontract: MContract, exist_contract: Bool) + do + var exist_contract_facet = mproperty.check_exist_contract_facet(self) + if exist_contract_facet and exist_contract then return + + var contract_facet: AMethPropdef + if not exist_contract_facet then + # If has no contract facet just create it + contract_facet = create_contract_facet(v, n_signature) + else + # Check if the contract facet already exist in this context (in this mclassdef) + if mclassdef.mpropdefs_by_property.has_key(mproperty.mcontract_facet) then + # get the define + contract_facet = v.toolcontext.modelbuilder.mpropdef2node(mclassdef.mpropdefs_by_property[mproperty.mcontract_facet]).as(AMethPropdef) + else + # create a new contract facet definition + contract_facet = create_contract_facet(v, n_signature) + var block = v.ast_builder.make_block + # super call to the contract facet + var n_super_call = v.ast_builder.make_super_call(n_signature.make_parameter_read(v.ast_builder), null) + # verification for add a return or not + if contract_facet.mpropdef.msignature.return_mtype != null then + block.add(v.ast_builder.make_return(n_super_call)) + else + block.add(n_super_call) + end + contract_facet.n_block = block + end + end + contract_facet.adapt_block_to_contract(v, mcontract, contract_facet) + contract_facet.location = v.current_location + contract_facet.do_all(v.toolcontext) + end + + # Method to create a contract facet of the method + private fun create_contract_facet(v: ContractsVisitor, n_signature: ASignature): AMethPropdef + do + var contract_facet = mproperty.mcontract_facet + assert contract_facet != null + # Defines the contract phase is an init or not + # it is necessary to use the contracts on constructor + contract_facet.is_init = self.mproperty.is_init + + # check if the method has an `msignature` to copy it. + var m_signature: nullable MSignature = null + if mproperty.intro.msignature != null then m_signature = mproperty.intro.msignature.clone + + var n_contractdef = mclassdef.mclass.create_empty_method(v, contract_facet, mclassdef, m_signature, n_signature) + # FIXME set the location because the callsite creation need the node location + n_contractdef.location = v.current_location + n_contractdef.validate + + var block = v.ast_builder.make_block + var n_self = new ASelfExpr + var args = n_contractdef.n_signature.make_parameter_read(v.ast_builder) + var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_contractdef, mproperty, true) + var n_call = v.ast_builder.make_call(n_self, callsite, args) + + if m_signature.return_mtype == null then + block.add(n_call) + else + block.add(v.ast_builder.make_return(n_call)) + end + + n_contractdef.n_block = block + n_contractdef.do_all(v.toolcontext) + return n_contractdef + end + + # Entry point to build contract (define the contract facet and define the contract method verification) + private fun construct_contract(v: ContractsVisitor, n_signature: ASignature, n_annotation: AAnnotation, mcontract: MContract, exist_contract: Bool) + do + if check_same_contract(v, n_annotation, mcontract) then return + # Check if the contract is necessary + if not mcontract.check_usage(v, mclassdef.mmodule) then return + if not exist_contract and not is_intro then no_intro_contract(v, n_signature, mcontract, n_annotation) + v.define_signature(mcontract, n_signature, mproperty.intro.msignature) + + var conditiondef = v.build_contract(n_annotation, mcontract, mclassdef) + check_contract_facet(v, n_signature.clone, mcontract, exist_contract) + has_contract = true + end + + # Create a contract on the introduction classdef of the property. + # Display an warning message if necessary + private fun no_intro_contract(v: ContractsVisitor, n_signature: ASignature, mcontract: MContract, n_annotation: AAnnotation) + do + mcontract.create_empty_contract(v, mcontract.intro_mclassdef, mcontract.adapt_msignature(self.mproperty.intro.msignature), mcontract.adapt_nsignature(n_signature)) + mcontract.no_intro_contract(v, n_annotation) + mproperty.intro.has_contract = true + end + + # Is the contract already defined in the context + # + # Exemple : + # fun foo is expects([...]), expects([...]) + # + # Here `check_same_contract` display an error when the second expects is processed + private fun check_same_contract(v: ContractsVisitor, n_annotation: AAnnotation ,mcontract: MContract): Bool + do + if self.mclassdef.mpropdefs_by_property.has_key(mcontract) then + v.toolcontext.error(n_annotation.location, "The method already has a defined `{mcontract.contract_name}` contract at line {self.mclassdef.mpropdefs_by_property[mcontract].location.line_start}") + return true + end + return false + end +end + +redef class MPropDef + # flag to indicate is the `MPropDef` has a contract + var has_contract = false +end + +redef class APropdef + redef fun check_callsite(v) + do + v.visited_method = self + end +end + +redef class AMethPropdef + + # Execute all method verification scope flow and typing. + # It also execute an ast validation to define all parents and all locations + private fun do_all(toolcontext: ToolContext) + do + self.validate + # FIXME: The `do_` usage it is maybe to much (verification...). Solution: Cut the `do_` methods into simpler parts + self.do_scope(toolcontext) + self.do_flow(toolcontext) + self.do_typing(toolcontext.modelbuilder) + end + + # Entry point to create a contract (verification of inheritance, or new contract). + redef fun create_contracts(v) + do + v.ast_builder.check_mmodule(mpropdef.mclassdef.mmodule) + + v.current_location = self.location + v.is_intro_contract = mpropdef.is_intro + + if n_annotations != null then + for n_annotation in n_annotations.n_items do + check_annotation(v,n_annotation) + end + end + + if not mpropdef.is_intro and not v.find_no_contract then + self.check_redef(v) + end + + # reset the flag + v.find_no_contract = false + end + + # Verification of the annotation to know if it is a contract annotation. + # If this is the case, we built the appropriate contract. + private fun check_annotation(v: ContractsVisitor, n_annotation: AAnnotation) + do + if n_annotation.name == "expects" then + var exist_contract = mpropdef.mproperty.check_exist_expect + mpropdef.construct_contract(v, self.n_signature.as(not null), n_annotation, mpropdef.mproperty.mexpect.as(not null), exist_contract) + else if n_annotation.name == "ensures" then + var exist_contract = mpropdef.mproperty.check_exist_ensure + mpropdef.construct_contract(v, self.n_signature.as(not null), n_annotation, mpropdef.mproperty.mensure.as(not null), exist_contract) + else if n_annotation.name == "no_contract" then + # no_contract found set the flag to true + v.find_no_contract = true + end + end + + # Verification if the method have an inherited contract to apply it. + private fun check_redef(v: ContractsVisitor) + do + # Check if the method has an attached contract + if not mpropdef.has_contract then + if mpropdef.mproperty.intro.has_contract then + mpropdef.has_contract = true + end + end + end + + # Adapt the block to use the contracts + private fun adapt_block_to_contract(v: ContractsVisitor, contract: MContract, n_mpropdef: AMethPropdef) + do + contract.adapt_block_to_contract(v, n_mpropdef) + mpropdef.has_contract = true + n_mpropdef.do_all(v.toolcontext) + end +end + +redef class MSignature + + # Adapt signature for a expect condition + # Removed the return type is it not necessary + private fun adapt_to_condition: MSignature do return new MSignature(mparameters.to_a, null) + + # Adapt signature for a ensure condition + # + # Create new parameter with the return type + private fun adapt_to_ensurecondition: MSignature + do + var rtype = return_mtype + var msignature = adapt_to_condition + if rtype != null then + msignature.mparameters.add(new MParameter("result", rtype, false)) + end + return msignature + end + + # Adapt signature for a expect condition + # Removed the return type is it not necessary + private fun clone: MSignature do return new MSignature(mparameters.to_a, return_mtype) +end + +redef class ASignature + + # Create an array of AVarExpr representing the read of every parameters + private fun make_parameter_read(ast_builder: ASTBuilder): Array[AVarExpr] + do + var args = new Array[AVarExpr] + for n_param in self.n_params do + var mtype = n_param.variable.declared_type + var variable = n_param.variable + if variable != null and mtype != null then + args.push ast_builder.make_var_read(variable, mtype) + end + end + return args + end + + # Return a copy of self adapted for the expect condition + # npropdef it is use to define the parent of the parameters + private fun adapt_to_condition(return_type: nullable AType): ASignature + do + var adapt_nsignature = self.clone + adapt_nsignature.n_type = return_type + return adapt_nsignature + end + + # Return a copy of self adapted for postcondition on npropdef + private fun adapt_to_ensurecondition: ASignature do + var nsignature = adapt_to_condition(null) + if ret_type != null then + var n_id = new TId + n_id.text = "result" + var new_param = new AParam + new_param.n_id = n_id + new_param.variable = new Variable(n_id.text) + new_param.variable.declared_type = ret_type + nsignature.n_params.add new_param + end + return nsignature + end +end + +redef class ASendExpr + redef fun check_callsite(v) + do + var actual_callsite = callsite + if actual_callsite != null then + callsite = v.drive_method_contract(actual_callsite) + end + end +end + +redef class ANewExpr + redef fun check_callsite(v) + do + var actual_callsite = callsite + if actual_callsite != null then + callsite = v.drive_method_contract(actual_callsite) + end + end +end