--- /dev/null
+# 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
nitlanguage / nit.git / commitdiff