X-Git-Url: http://nitlanguage.org diff --git a/src/contracts.nit b/src/contracts.nit index d80abee..0055c45 100644 --- a/src/contracts.nit +++ b/src/contracts.nit @@ -18,10 +18,10 @@ # 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 astbuilder intrude import modelize_property intrude import scope intrude import typing @@ -50,7 +50,7 @@ redef class AModule # 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). + # for each class (invariant) and method (expect, ensure). # # - Second step the visitor analyzes each `ASendExpr` to see # if the callsite calls a method with a contract. If this is @@ -65,10 +65,11 @@ redef class AModule 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 +# Visitor to build all contracts. private class ContractsVisitor super Visitor + # Instance of the toolcontext var toolcontext: ToolContext # The main module @@ -90,6 +91,8 @@ private class ContractsVisitor var current_location: Location is noinit # Is the contrat is an introduction or not? + # This attribute has the same value as the `is_intro` of the propdef attached to the contract. + # Note : For MClassDef `is_intro_contract == false`. This is due to the fact that a method for checking invariants is systematically added to the root object class. var is_intro_contract: Bool is noinit # Actual visited class @@ -98,6 +101,11 @@ private class ContractsVisitor # is `no_contract` annotation was found var find_no_contract = false + # The reference to the `in_contract` attribute. + # This attribute is used to disable contract verification when you are already in a contract verification. + # Keep the `in_contract` attribute to avoid searching at each contrat + var in_contract_attribute: nullable MAttribute = null + redef fun visit(node) do node.create_contracts(self) @@ -134,13 +142,13 @@ private class ContractsVisitor end # Verification if the construction of the contract is necessary. - # Three cases are checked for `expects`: + # Three cases are checked for `expect`: # - # - 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. + # - Was the `--full-contract` option passed? + # - Is the method is in the main package? + # - Is the method is in a direct imported package? # - fun check_usage_expects(actual_mmodule: MModule): Bool + fun check_usage_expect(actual_mmodule: MModule): Bool do var main_package = mainmodule.mpackage var actual_package = actual_mmodule.mpackage @@ -152,22 +160,97 @@ private class ContractsVisitor end # Verification if the construction of the contract is necessary. - # Two cases are checked for `ensures`: + # Two cases are checked for `ensure`: # - # - Is the `--full-contract` option it's use? - # - Is the method is in the main package + # - Was the `--full-contract` option passed? + # - Is the method is in the main package? # - fun check_usage_ensures(actual_mmodule: MModule): Bool + fun check_usage_ensure(actual_mmodule: MModule): Bool do return toolcontext.opt_full_contract.value or mainmodule.mpackage == actual_mmodule.mpackage end + # Inject the incontract attribute (`_in_contract_`) in the `Sys` class + # This attribute allows to check if the contract need to be executed + private fun inject_incontract_in_sys + do + # If the `in_contract_attribute` already know just return + if in_contract_attribute != null then return + + var sys_class = toolcontext.modelbuilder.get_mclass_by_name(visited_module, mainmodule, "Sys") + + # Try to get the `in_contract` property, if it has already defined in a previously visited module. + var in_contract_property = toolcontext.modelbuilder.try_get_mproperty_by_name(visited_module, sys_class.intro, "__in_contract_") + if in_contract_property != null then + self.in_contract_attribute = in_contract_property.as(MAttribute) + return + end + + var bool_false = new AFalseExpr.make(mainmodule.bool_type) + var n_in_contract_attribute = toolcontext.modelbuilder.create_attribute_from_name("__in_contract_", sys_class.intro, mainmodule.bool_type, public_visibility).create_setter(toolcontext.modelbuilder, true).define_default(bool_false) + + in_contract_attribute = n_in_contract_attribute.mpropdef.mproperty + end + + # Return the `_in_contract_` attribute. + # If the attribute `_in_contract_` does not exist it's injected with `inject_incontract_in_sys` + private fun get_incontract: MAttribute + do + if self.in_contract_attribute == null then inject_incontract_in_sys + return in_contract_attribute.as(not null) + end + + # Return an `AIfExpr` with the contract encapsulated by an `if` to check if it's already in a contract verification. + # + # Example: + # ~~~nitish + # class A + # fun bar([...]) is except([...]) + # + # fun _contract_bar([...]) + # do + # if not sys._in_contract_ then + # sys._in_contract_ = true + # _bar_expect([...]) + # sys._in_contract_ = false + # end + # bar([...]) + # end + # + # fun _bar_expect([...]) + # end + # ~~~~ + # + private fun encapsulated_contract_call(visited_method: AMethPropdef, call_to_contracts: Array[ACallExpr]): AIfExpr + do + var sys_property = toolcontext.modelbuilder.model.get_mproperties_by_name("sys").first.as(MMethod) + var callsite_sys = ast_builder.create_callsite(toolcontext.modelbuilder, visited_method, sys_property, true) + + var incontract_attribute = get_incontract + + var callsite_get_incontract = ast_builder.create_callsite(toolcontext.modelbuilder, visited_method, incontract_attribute.getter.as(MMethod), false) + var callsite_set_incontract = ast_builder.create_callsite(toolcontext.modelbuilder, visited_method, incontract_attribute.setter.as(MMethod), false) + + var n_condition = ast_builder.make_not(ast_builder.make_call(ast_builder.make_call(new ASelfExpr, callsite_sys, null), callsite_get_incontract, null)) + + var n_if = ast_builder.make_if(n_condition, null) + + var if_then_block = n_if.n_then.as(ABlockExpr) + + if_then_block.add(ast_builder.make_call(ast_builder.make_call(new ASelfExpr, callsite_sys, null), callsite_set_incontract, [new ATrueExpr.make(mainmodule.bool_type)])) + if_then_block.add_all(call_to_contracts) + if_then_block.add(ast_builder.make_call(ast_builder.make_call(new ASelfExpr, callsite_sys, null), callsite_set_incontract, [new AFalseExpr.make(mainmodule.bool_type)])) + + return n_if + end end # This visitor checks the `callsite` to see if the target `mpropdef` has a contract. private class CallSiteVisitor super Visitor + + # Instance of the toolcontext var toolcontext: ToolContext # Actual visited method @@ -183,21 +266,16 @@ 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.mpropdef.has_contract then + 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 unsafe_mtype = callsite.recv.resolve_for(visited_mpropdef.mclassdef.bound_mtype, callsite.anchor, visited_mpropdef.mclassdef.mmodule, true) - - # 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 + 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 end @@ -210,10 +288,10 @@ 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) + # Returns the conditions of annotation parameters. If there are several parameters, the result is an `AAndExpr` + # Example: + # the contract `ensure(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 @@ -243,10 +321,10 @@ abstract class MContract 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 + private fun adapt_specific_msignature(m_signature: MSignature): MSignature do return m_signature.adapt_to_contract # 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) + private fun adapt_specific_nsignature(n_signature: ASignature): ASignature do return n_signature.adapt_to_contract # Adapt the `m_signature` to the contract # If it is not null call the specific adapt `m_signature` for the contract @@ -274,10 +352,13 @@ abstract class MContract # Create the initial contract (intro) # All contracts have the same implementation for the introduction. # + # Example: + # ~~~nitish # fun contrat([...]) # do # assert contract_condition # end + # ~~~ # private fun create_intro_contract(v: ContractsVisitor, n_condition: nullable AExpr, mclassdef: MClassDef): AMethPropdef do @@ -318,27 +399,28 @@ class MExpect super MContract # Define the name of the contract - redef fun contract_name: String do return "expects" + redef fun contract_name: String do return "expect" # 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 + # Example: # ~~~nitish # class A # fun bar [...] - # fun _bar_expects([...]) + # fun _bar_expect([...]) # do # [empty contract] # end # end # # redef class A - # redef fun bar is expects(contract_condition) - # redef fun _bar_expects([...]) + # redef fun bar is expect(contract_condition) + # redef fun _bar_expect([...]) # do - # if not (contract_condition) then super + # if (contract_condition) then return + # super # end # end # ~~~~ @@ -380,7 +462,7 @@ class MExpect end end -# The root of all contracts where the call is after the execution of the original method (`invariants` and `ensures`). +# The root of all contracts where the call is after the execution of the original method (`invariant` and `ensure`). abstract class BottomMContract super MContract @@ -400,7 +482,9 @@ abstract class BottomMContract return n_block end - # Inject the result variable in the `n_block` of the given `n_mpropdef`. + # Inject the `result` variable into the `n_block` of the given n_mpropdef`. + # + # The purpose of the variable is to capture return values to use it in contracts. private fun inject_result(v: ContractsVisitor, n_mpropdef: AMethPropdef, ret_type: MType): Variable do var actual_block = n_mpropdef.n_block @@ -446,7 +530,7 @@ class MEnsure super BottomMContract # Define the name of the contract - redef fun contract_name: String do return "ensures" + redef fun contract_name: String do return "ensure" redef fun adapt_specific_msignature(m_signature: MSignature): MSignature do @@ -540,7 +624,7 @@ redef class MMethod 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) + self.mensure = new MEnsure(intro_mclassdef, "_ensure_{name}", intro_mclassdef.location, public_visibility) return false end @@ -551,7 +635,7 @@ redef class MMethod 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) + self.mexpect = new MExpect(intro_mclassdef, "_expect_{name}", intro_mclassdef.location, public_visibility) return false end @@ -561,7 +645,7 @@ redef class MMethod 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) + self.mcontract_facet = new MMethod(intro_mclassdef, "_contract_{name}", intro_mclassdef.location, public_visibility) return false end end @@ -570,23 +654,25 @@ 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) + 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) if exist_contract_facet and exist_contract then return var contract_facet: AMethPropdef if not exist_contract_facet then + # If has no contract facet in intro just create it + if classdef != mproperty.intro_mclassdef then create_contract_facet(v, mproperty.intro_mclassdef, n_signature) # If has no contract facet just create it - contract_facet = create_contract_facet(v, n_signature) + contract_facet = create_contract_facet(v, classdef, 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 + # Check if the contract facet already exist in this context (in this classdef) + if classdef.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) + contract_facet = v.toolcontext.modelbuilder.mpropdef2node(classdef.mpropdefs_by_property[mproperty.mcontract_facet]).as(AMethPropdef) else # create a new contract facet definition - contract_facet = create_contract_facet(v, n_signature) + contract_facet = create_contract_facet(v, classdef, 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) @@ -605,7 +691,7 @@ redef class MMethodDef end # Method to create a contract facet of the method - private fun create_contract_facet(v: ContractsVisitor, n_signature: ASignature): AMethPropdef + private fun create_contract_facet(v: ContractsVisitor, classdef: MClassDef, n_signature: ASignature): AMethPropdef do var contract_facet = mproperty.mcontract_facet assert contract_facet != null @@ -617,7 +703,7 @@ redef class MMethodDef 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) + var n_contractdef = classdef.mclass.create_empty_method(v, contract_facet, classdef, 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 @@ -647,7 +733,7 @@ redef class MMethodDef 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) + check_contract_facet(v, n_signature.clone, mclassdef, mcontract, exist_contract) has_contract = true end @@ -663,9 +749,9 @@ redef class MMethodDef # Is the contract already defined in the context # # Exemple : - # fun foo is expects([...]), expects([...]) + # fun foo is expect([...]), expect([...]) # - # Here `check_same_contract` display an error when the second expects is processed + # 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 do if self.mclassdef.mpropdefs_by_property.has_key(mcontract) then @@ -690,17 +776,6 @@ 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 @@ -727,12 +802,12 @@ redef class AMethPropdef # 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 - if not v.check_usage_expects(mpropdef.mclassdef.mmodule) then return + 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 == "ensures" then - if not v.check_usage_ensures(mpropdef.mclassdef.mmodule) then return + 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 @@ -763,25 +838,26 @@ 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 an contract + # + # The returned `MSignature` is the copy of `self` without return type. + private fun adapt_to_contract: MSignature do return new MSignature(mparameters.to_a, null) - # Adapt signature for a ensure condition + # Adapt signature for a ensure contract # - # Create new parameter with the return type + # The returned `MSignature` is the copy of `self` without return type. + # The return type is replaced by a new parameter `result` private fun adapt_to_ensurecondition: MSignature do var rtype = return_mtype - var msignature = adapt_to_condition + var msignature = adapt_to_contract 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 + # The returned `MSignature` is the exact copy of `self`. private fun clone: MSignature do return new MSignature(mparameters.to_a, return_mtype) end @@ -801,26 +877,26 @@ redef class ASignature 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 + # Create a new ASignature adapted for contract + # + # The returned `ASignature` is the copy of `self` without return type. + private fun adapt_to_contract: ASignature do var adapt_nsignature = self.clone - adapt_nsignature.n_type = return_type + if adapt_nsignature.n_type != null then adapt_nsignature.n_type.detach return adapt_nsignature end - # Return a copy of self adapted for postcondition on npropdef + # Create a new ASignature adapted for ensure + # + # The returned `ASignature` is the copy of `self` without return type. + # The return type is replaced by a new parameter `result` private fun adapt_to_ensurecondition: ASignature do - var nsignature = adapt_to_condition(null) + var nsignature = adapt_to_contract 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 + var variable = new Variable("result") + variable.declared_type = ret_type + nsignature.n_params.add new AParam.make(variable, ret_type.create_ast_representation) end return nsignature end