X-Git-Url: http://nitlanguage.org diff --git a/src/contracts.nit b/src/contracts.nit index 3a3c3a7..7c174fe 100644 --- a/src/contracts.nit +++ b/src/contracts.nit @@ -21,6 +21,7 @@ module contracts import parse_annotations import phase import semantize +intrude import model_contract intrude import astbuilder intrude import modelize_property intrude import scope @@ -56,11 +57,12 @@ redef class AModule # 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 ast_builder = new ASTBuilder(mmodule.as(not null)) # - var contract_visitor = new ContractsVisitor(toolcontext, toolcontext.modelbuilder.identified_modules.first, self, new ASTBuilder(mmodule.as(not null))) + var contract_visitor = new ContractsVisitor(toolcontext, toolcontext.modelbuilder.identified_modules.first, self, ast_builder) contract_visitor.enter_visit(self) # - var callsite_visitor = new CallSiteVisitor(toolcontext) + var callsite_visitor = new CallSiteVisitor(toolcontext, ast_builder) callsite_visitor.enter_visit(self) end end @@ -122,23 +124,18 @@ private class ContractsVisitor 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 + private fun build_contract(n_annotations: Array[AAnnotation], mcontract: MContract, mclassdef: MClassDef) do - self.current_location = n_annotation.location + var n_conditions = new Array[AExpr] # Retrieving the expression provided in the annotation - var n_condition = n_annotation.construct_condition(self) - var m_contractdef: AMethPropdef + for n_annotation in n_annotations do n_conditions.add n_annotation.construct_condition(self) if is_intro_contract then # Create new contract method - m_contractdef = mcontract.create_intro_contract(self, n_condition, mclassdef) + mcontract.create_intro_contract(self, n_conditions, mclassdef) else # Create a redef of contract to take in consideration the new condition - m_contractdef = mcontract.create_subcontract(self, n_condition, mclassdef) + mcontract.create_subcontract(self, n_conditions, 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 # Verification if the construction of the contract is necessary. @@ -249,12 +246,13 @@ end private class CallSiteVisitor super Visitor - # Instance of the toolcontext var toolcontext: ToolContext + var ast_builder: ASTBuilder + # Actual visited method - var visited_method: APropdef is noinit + var visited_propdef: APropdef is noinit redef fun visit(node) do @@ -266,18 +264,13 @@ private class CallSiteVisitor # 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.mproperty.mcontract_facet != null then - var contract_facet = callsite.mproperty.mcontract_facet - var visited_mpropdef = visited_method.mpropdef - assert contract_facet != null and visited_mpropdef != null + var contract_facet = callsite.mproperty.mcontract_facet + var visited_mpropdef = visited_propdef.mpropdef - 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 - return callsite + if visited_mpropdef isa MContract or visited_mpropdef isa MFacet then return callsite + if visited_mpropdef == null or contract_facet == null then return callsite + + return ast_builder.create_callsite(toolcontext.modelbuilder, visited_propdef, contract_facet, callsite.recv_is_self) end end @@ -301,21 +294,15 @@ redef class AAnnotation 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 +redef class MContract # 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 + private fun no_intro_contract(v: ContractsVisitor, a: Array[AAnnotation])do end # Creating specific inheritance block contract - private fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr is abstract + # + # `super_args` : Correspond to the `super` call arguments + private fun create_inherit_nblock(v: ContractsVisitor, n_conditions: Array[AExpr], super_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 @@ -360,46 +347,52 @@ abstract class MContract # end # ~~~ # - private fun create_intro_contract(v: ContractsVisitor, n_condition: nullable AExpr, mclassdef: MClassDef): AMethPropdef + private fun create_intro_contract(v: ContractsVisitor, n_conditions: Array[AExpr], mclassdef: MClassDef) do var n_block = v.ast_builder.make_block - if n_condition != null then + for n_condition in n_conditions do # 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) + var tid = new TId.init_tk(n_condition.location) + tid.text = "{n_condition.location.text}" + var n_assert = v.ast_builder.make_assert(tid, n_condition, null) + # Define the assert location to reference the annoation + n_assert.location = n_condition.location + n_block.add n_assert end - return make_contract(v, n_block, mclassdef) + 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 + # Create a contract to check the old (super call) and the new conditions + # + # Example: + # ~~~nitish + # fun contrat([...]) + # do + # super # Call the old contracts + # assert new_condition + # end + # ~~~ + # + private fun create_subcontract(v: ContractsVisitor, n_conditions: Array[AExpr], mclassdef: MClassDef) 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) + n_block = self.create_inherit_nblock(v, n_conditions, args) + 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 + private fun make_contract(v: ContractsVisitor, n_block: AExpr, mclassdef: MClassDef) 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 "expect" +redef class MExpect # Display warning if no contract is defined at introduction `expect`, # because if no contract is defined at the introduction the added @@ -425,21 +418,23 @@ class MExpect # end # ~~~~ # - redef fun no_intro_contract(v: ContractsVisitor, a: AAnnotation) + redef fun no_intro_contract(v: ContractsVisitor, a: Array[AAnnotation]) do - v.toolcontext.warning(a.location,"","Useless contract: No contract defined at the introduction of the method") + v.toolcontext.warning(a.first.location,"useless_contract","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 + redef fun create_inherit_nblock(v: ContractsVisitor, n_conditions: Array[AExpr], super_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 + for n_condition in n_conditions 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 + if_block.location = n_condition.location + n_block.add if_block + end + n_block.add v.ast_builder.make_super_call(super_args) return n_block end @@ -462,23 +457,24 @@ class MExpect end end -# The root of all contracts where the call is after the execution of the original method (`invariant` and `ensure`). -abstract class BottomMContract - super MContract +redef class BottomMContract - redef fun create_nblock(v: ContractsVisitor, n_condition: AExpr, args: Array[AExpr]): ABlockExpr + redef fun create_inherit_nblock(v: ContractsVisitor, n_conditions: Array[AExpr], super_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 + + var super_call = v.ast_builder.make_super_call(super_args) + n_block.add super_call - n_block.add assert_block + for n_condition in n_conditions do + var tid = new TId.init_tk(n_condition.location) + tid.text = "{n_condition.location.text}" + # Creating the assert expression with the new condition + var n_assert = v.ast_builder.make_assert(tid, n_condition) + n_assert.location = n_condition.location + n_block.add n_assert + end return n_block end @@ -524,13 +520,7 @@ abstract class BottomMContract 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 "ensure" +redef class MEnsure redef fun adapt_specific_msignature(m_signature: MSignature): MSignature do @@ -604,59 +594,13 @@ redef class MClass 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, "_ensure_{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, "_expect_{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(intro_mclassdef, "_contract_{name}", intro_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, classdef: MClassDef, mcontract: MContract, exist_contract: Bool) do - var exist_contract_facet = mproperty.check_exist_contract_facet(self) + var exist_contract_facet = mproperty.has_contract_facet if exist_contract_facet and exist_contract then return var contract_facet: AMethPropdef @@ -693,8 +637,7 @@ redef class MMethodDef # Method to create a contract facet of the method private fun create_contract_facet(v: ContractsVisitor, classdef: MClassDef, n_signature: ASignature): AMethPropdef do - var contract_facet = mproperty.mcontract_facet - assert contract_facet != null + var contract_facet = mproperty.build_contract_facet # 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 @@ -726,39 +669,41 @@ redef class MMethodDef 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) + private fun construct_contract(v: ContractsVisitor, n_signature: ASignature, n_annotations: Array[AAnnotation], mcontract: MContract, exist_contract: Bool) do - if check_same_contract(v, n_annotation, mcontract) then return - if not exist_contract and not is_intro then no_intro_contract(v, n_signature, mcontract, n_annotation) + if not exist_contract and not is_intro then no_intro_contract(v, mcontract, n_annotations) v.define_signature(mcontract, n_signature, mproperty.intro.msignature) - var conditiondef = v.build_contract(n_annotation, mcontract, mclassdef) + v.build_contract(n_annotations, mcontract, mclassdef) check_contract_facet(v, n_signature.clone, mclassdef, 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) + private fun no_intro_contract(v: ContractsVisitor, mcontract: MContract, n_annotations: Array[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 + v.toolcontext.modelbuilder.create_method_from_property(mcontract, mcontract.intro_mclassdef, false, v.m_signature) + mcontract.no_intro_contract(v, n_annotations) end - # Is the contract already defined in the context - # - # Exemple : - # fun foo is expect([...]), expect([...]) - # - # Here `check_same_contract` display an error when the second expect is processed - private fun check_same_contract(v: ContractsVisitor, n_annotation: AAnnotation ,mcontract: MContract): Bool + # Apply the `no_contract` annotation to the contract. This method removes the inheritance by adding an empty contract method. + # Display a warning if the annotation is not needed + private fun no_contract_apply(v: ContractsVisitor, n_signature: ASignature) 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 + var mensure = mproperty.mensure + var mexpect = mproperty.mexpect + if mensure == null and mexpect == null then + v.toolcontext.warning(location, "useless_nocontract", "Useless `no_contract`, no contract was declared for `{name}`. Remove the `no_contract`") + end + if mensure != null then + # Add an empty ensure method to replace the actual definition + v.toolcontext.modelbuilder.create_method_from_property(mensure, mclassdef, false, mensure.intro.msignature) + end + if mexpect != null then + # Add an empty expect method to replace the actual definition + v.toolcontext.modelbuilder.create_method_from_property(mexpect, mclassdef, false, mexpect.intro.msignature) end - return false end end @@ -770,60 +715,50 @@ end redef class APropdef redef fun check_callsite(v) do - v.visited_method = self + v.visited_propdef = 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 + check_annotation(v) + if not mpropdef.is_intro then check_redef(v) + end - if n_annotations != null then - for n_annotation in n_annotations.n_items do - check_annotation(v,n_annotation) - 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) + do + var annotations_expect = get_annotations("expect") + var annotations_ensure = get_annotations("ensure") + var annotation_no_contract = get_annotations("no_contract") + + if (not annotations_expect.is_empty or not annotations_ensure.is_empty) and not annotation_no_contract.is_empty then + v.toolcontext.error(location, "The new contract definition is not correct when using `no_contract`. Remove the contract definition or the `no_contract`") + return end - if not mpropdef.is_intro and not v.find_no_contract then - self.check_redef(v) + var nsignature = n_signature or else new ASignature + + if not annotation_no_contract.is_empty then + mpropdef.no_contract_apply(v, nsignature.clone) + return end - # reset the flag - v.find_no_contract = false - end + if not annotations_expect.is_empty then + var exist_contract = mpropdef.mproperty.has_expect + mpropdef.construct_contract(v, nsignature.clone, annotations_expect, mpropdef.mproperty.build_expect, exist_contract) + 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 == "expect" then - if not v.check_usage_expect(mpropdef.mclassdef.mmodule) then return - 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 == "ensure" then - if not v.check_usage_ensure(mpropdef.mclassdef.mmodule) then return - 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 + if not annotations_ensure.is_empty then + var exist_contract = mpropdef.mproperty.has_ensure + mpropdef.construct_contract(v, nsignature.clone, annotations_ensure, mpropdef.mproperty.build_ensure, exist_contract) end end