X-Git-Url: http://nitlanguage.org diff --git a/src/contracts.nit b/src/contracts.nit index 22e4df8..e8d440b 100644 --- a/src/contracts.nit +++ b/src/contracts.nit @@ -18,10 +18,11 @@ # 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 model_contract +intrude import astbuilder intrude import modelize_property intrude import scope intrude import typing @@ -101,6 +102,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) @@ -165,6 +171,79 @@ private class ContractsVisitor 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. @@ -223,12 +302,7 @@ 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 +redef class MContract # Define the name of the contract fun contract_name: String is abstract @@ -243,10 +317,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 @@ -315,10 +389,7 @@ abstract class MContract end end -# A expect (precondition) contract representation -# This method check if the requirements of the called method is true. -class MExpect - super MContract +redef class MExpect # Define the name of the contract redef fun contract_name: String do return "expect" @@ -384,9 +455,7 @@ 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 do @@ -446,10 +515,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 +redef class MEnsure # Define the name of the contract redef fun contract_name: String do return "ensure" @@ -526,59 +592,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 @@ -615,8 +635,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 @@ -698,17 +717,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 @@ -737,12 +745,12 @@ redef class AMethPropdef 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) + var exist_contract = mpropdef.mproperty.has_expect + mpropdef.construct_contract(v, self.n_signature.as(not null), n_annotation, mpropdef.mproperty.build_expect, 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) + var exist_contract = mpropdef.mproperty.has_ensure + mpropdef.construct_contract(v, self.n_signature.as(not null), n_annotation, mpropdef.mproperty.build_ensure, exist_contract) else if n_annotation.name == "no_contract" then # no_contract found set the flag to true v.find_no_contract = true @@ -771,9 +779,10 @@ 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 contract # @@ -782,7 +791,7 @@ redef class MSignature 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 @@ -812,10 +821,10 @@ redef class ASignature # Create a new ASignature adapted for contract # # The returned `ASignature` is the copy of `self` without return type. - private fun adapt_to_condition(return_type: nullable AType): ASignature + 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 @@ -824,15 +833,11 @@ redef class ASignature # 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