# 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
# 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)
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 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
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
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
#
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
# 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
# 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
nitlanguage / nit.git / blobdiff