1 # This file is part of NIT ( http://www.nitlanguage.org ).
3 # Licensed under the Apache License, Version 2.0 (the "License");
4 # you may not use this file except in compliance with the License.
5 # You may obtain a copy of the License at
7 # http://www.apache.org/licenses/LICENSE-2.0
9 # Unless required by applicable law or agreed to in writing, software
10 # distributed under the License is distributed on an "AS IS" BASIS,
11 # WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12 # See the License for the specific language governing permissions and
13 # limitations under the License.
15 # Module to build contract
16 # This module provide extension of the modele to add contracts, the building phase and the "re-driving" to call the contract.
18 # FIXME Split the module in three parts: extension of the modele, building phase and the "re-driving"
21 import parse_annotations
24 intrude import model_contract
25 intrude import astbuilder
26 intrude import modelize_property
30 redef class ToolContext
31 # Parses contracts annotations.
32 var contracts_phase
: Phase = new ContractsPhase(self, [modelize_property_phase
,typing_phase
])
35 private class ContractsPhase
38 redef fun process_nmodule
(nmodule
)do
39 # Check if the contracts are disabled
40 if toolcontext
.opt_no_contract
.value
then return
41 nmodule
.do_contracts
(self.toolcontext
)
44 redef fun process_mainmodule
(mainmodule
: MModule, given_mmodules
: SequenceRead[MModule]) do
45 # Visit all loaded modules `toolcontext.nmodules` to do contract weaving
46 for nmodule
in toolcontext
.modelbuilder
.nmodules
do
47 nmodule
.do_weaving_contracts
(self.toolcontext
)
54 # Entry point to generate the entire contract infrastructure.
55 # Once this method is called we must call the `do_weaving_contracts` method (see it for more information).
56 fun do_contracts
(toolcontext
: ToolContext) do
57 var ast_builder
= new ASTBuilder(mmodule
.as(not null))
59 var contract_visitor
= new ContractsVisitor(toolcontext
, toolcontext
.modelbuilder
.identified_modules
.first
, self, ast_builder
)
60 contract_visitor
.enter_visit
(self)
63 # Entry point to execute the weaving in order to redirect the calls to the contract sides if it's needed.
64 fun do_weaving_contracts
(toolcontext
: ToolContext)
66 var ast_builder
= new ASTBuilder(mmodule
.as(not null))
67 var callsite_visitor
= new CallSiteVisitor(toolcontext
, ast_builder
)
68 callsite_visitor
.enter_visit
(self)
72 # Visitor to build all contracts.
73 private class ContractsVisitor
76 # Instance of the toolcontext
77 var toolcontext
: ToolContext
80 # It's strore to define if the contract need to be build depending on the selected policy `--no-contract` `--full-contract` or default
81 var mainmodule
: MModule
83 # Actual visited module
84 var visited_module
: AModule
86 var ast_builder
: ASTBuilder
88 # The `ASignature` of the actual build contract
89 var n_signature
: ASignature is noinit
91 # The `MSignature` of the actual build contract
92 var m_signature
: MSignature is noinit
94 # The `current_location` can corresponding of the annotation or method location.
95 var current_location
: Location is noinit
97 # Is the contrat is an introduction or not?
98 # This attribute has the same value as the `is_intro` of the propdef attached to the contract.
99 # 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.
100 var is_intro_contract
: Bool is noinit
102 # Actual visited class
103 var visited_class
: nullable AClassdef
105 # is `no_contract` annotation was found
106 var find_no_contract
= false
108 # The reference to the `in_contract` attribute.
109 # This attribute is used to disable contract verification when you are already in a contract verification.
110 # Keep the `in_contract` attribute to avoid searching at each contrat
111 var in_contract_attribute
: nullable MAttribute = null
113 redef fun visit
(node
)
115 node
.create_contracts
(self)
119 # Method use to define the signature part of the method `ASignature` and `MSignature`
120 # The given `mcontract` provided `adapt_nsignature` and `adapt_msignature` to copy and adapt the given signature (`nsignature` and `msignature`)
121 fun define_signature
(mcontract
: MContract, nsignature
: nullable ASignature, msignature
: nullable MSignature)
123 if nsignature
!= null and msignature
!= null then nsignature
.ret_type
= msignature
.return_mtype
124 self.n_signature
= mcontract
.adapt_nsignature
(nsignature
)
125 self.m_signature
= mcontract
.adapt_msignature
(msignature
)
128 # Define the new contract take in consideration that an old contract exist or not
129 private fun build_contract
(n_annotations
: Array[AAnnotation], mcontract
: MContract, mclassdef
: MClassDef)
131 var n_conditions
= new Array[AExpr]
132 # Retrieving the expression provided in the annotation
133 for n_annotation
in n_annotations
do n_conditions
.add n_annotation
.construct_condition
(self)
134 if is_intro_contract
then
135 # Create new contract method
136 mcontract
.create_intro_contract
(self, n_conditions
, mclassdef
)
138 # Create a redef of contract to take in consideration the new condition
139 mcontract
.create_subcontract
(self, n_conditions
, mclassdef
)
143 # Inject the incontract attribute (`_in_contract_`) in the `Sys` class
144 # This attribute allows to check if the contract need to be executed
145 private fun inject_incontract_in_sys
147 # If the `in_contract_attribute` already know just return
148 if in_contract_attribute
!= null then return
150 var sys_class
= toolcontext
.modelbuilder
.get_mclass_by_name
(visited_module
, mainmodule
, "Sys")
152 # Try to get the `in_contract` property, if it has already defined in a previously visited module.
153 var in_contract_property
= toolcontext
.modelbuilder
.try_get_mproperty_by_name
(visited_module
, sys_class
.intro
, "__in_contract_")
154 if in_contract_property
!= null then
155 self.in_contract_attribute
= in_contract_property
.as(MAttribute)
159 var bool_false
= new AFalseExpr.make
(mainmodule
.bool_type
)
160 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
)
162 in_contract_attribute
= n_in_contract_attribute
.mpropdef
.mproperty
165 # Return the `_in_contract_` attribute.
166 # If the attribute `_in_contract_` does not exist it's injected with `inject_incontract_in_sys`
167 private fun get_incontract
: MAttribute
169 if self.in_contract_attribute
== null then inject_incontract_in_sys
170 return in_contract_attribute
.as(not null)
173 # Return an `AIfExpr` with the contract encapsulated by an `if` to check if it's already in a contract verification.
178 # fun bar([...]) is except([...])
180 # fun _contract_bar([...])
182 # if not sys._in_contract_ then
183 # sys._in_contract_ = true
185 # sys._in_contract_ = false
190 # fun _bar_expect([...])
194 private fun encapsulated_contract_call
(visited_method
: AMethPropdef, call_to_contracts
: Array[ACallExpr]): AIfExpr
196 var sys_property
= toolcontext
.modelbuilder
.model
.get_mproperties_by_name
("sys").first
.as(MMethod)
197 var callsite_sys
= ast_builder
.create_callsite
(toolcontext
.modelbuilder
, visited_method
, sys_property
, true)
199 var incontract_attribute
= get_incontract
201 var callsite_get_incontract
= ast_builder
.create_callsite
(toolcontext
.modelbuilder
, visited_method
, incontract_attribute
.getter
.as(MMethod), false)
202 var callsite_set_incontract
= ast_builder
.create_callsite
(toolcontext
.modelbuilder
, visited_method
, incontract_attribute
.setter
.as(MMethod), false)
204 var n_condition
= ast_builder
.make_not
(ast_builder
.make_call
(ast_builder
.make_call
(new ASelfExpr, callsite_sys
, null), callsite_get_incontract
, null))
206 var n_if
= ast_builder
.make_if
(n_condition
, null)
208 var if_then_block
= n_if
.n_then
.as(ABlockExpr)
210 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
)]))
211 if_then_block
.add_all
(call_to_contracts
)
212 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
)]))
218 # This visitor checks the `callsite` to see if the target `mpropdef` has a contract.
219 private class CallSiteVisitor
222 # Instance of the toolcontext
223 var toolcontext
: ToolContext
225 var ast_builder
: ASTBuilder
227 # Actual visited method
228 var visited_propdef
: APropdef is noinit
230 redef fun visit
(node
)
232 node
.check_callsite
(self)
236 # Check if the callsite is bound on a property with a contract.
237 # If the property is linked to a contract a new callsite will be created towards the correct facet,
238 # in the other case the returned callsite wall be the same as the given `callsite`
239 private fun drive_callsite_to_contract
(callsite
: CallSite): CallSite
241 var contract_facet
= callsite
.mproperty
.mcontract_facet
242 var visited_mpropdef
= visited_propdef
.mpropdef
244 if visited_mpropdef
isa MContract or visited_mpropdef
isa MFacet then return callsite
245 if visited_mpropdef
== null or contract_facet
== null then return callsite
247 return ast_builder
.create_callsite
(toolcontext
.modelbuilder
, visited_propdef
, contract_facet
, callsite
.recv_is_self
)
252 private fun create_contracts
(v
: ContractsVisitor) do end
253 private fun check_callsite
(v
: CallSiteVisitor) do end
256 redef class AAnnotation
258 # Returns the conditions of annotation parameters. If there are several parameters, the result is an `AAndExpr`
260 # the contract `ensure(true, i == 10, f >= 1.0)`
261 # return this condition `(true and i == 10 and f >= 1.0)`
262 private fun construct_condition
(v
: ContractsVisitor): AExpr
264 var n_condition
= n_args
.first
266 for n_arg
in n_args
do n_condition
= v
.ast_builder
.make_and
(n_condition
, n_arg
)
267 n_condition
.location
= self.location
272 redef class MContract
274 # Should contract be called?
275 # return `true` if the contract needs to be called.
276 private fun is_called
(v
: ContractsVisitor, mpropdef
: MPropDef): Bool
278 return v
.toolcontext
.opt_full_contract
.value
281 # Method use to diplay warning when the contract is not present at the introduction
282 private fun no_intro_contract
(v
: ContractsVisitor, a
: Array[AAnnotation])do end
284 # Creating specific inheritance block contract
286 # `super_args` : Correspond to the `super` call arguments
287 private fun create_inherit_nblock
(v
: ContractsVisitor, n_conditions
: Array[AExpr], super_args
: Array[AExpr]): ABlockExpr is abstract
289 # Method to adapt the given `n_mpropdef.n_block` to the contract
290 private fun adapt_method_to_contract
(v
: ContractsVisitor, mfacet
: MFacet, n_mpropdef
: AMethPropdef) is abstract
292 # Create and return an adapted `MSignature` specifically for the contract in fonction of the given `m_signature`
293 private fun adapt_specific_msignature
(m_signature
: MSignature): MSignature do return m_signature
.adapt_to_contract
295 # Create and return an adapted `ASignature` specifically for the contract in fonction of the given `n_signature`
296 private fun adapt_specific_nsignature
(n_signature
: ASignature): ASignature do return n_signature
.adapt_to_contract
298 # Adapt the `m_signature` to the contract
299 # If `m_signature == null` return a new `MSignature` else it calls a specific adapt method see `adapt_specific_msignature`
300 private fun adapt_msignature
(m_signature
: nullable MSignature): MSignature
302 if m_signature
== null then return new MSignature(new Array[MParameter])
303 return adapt_specific_msignature
(m_signature
)
306 # Adapt the `n_signature` to the contract
307 # If `n_signature == null` return a new `ASignature` else it calls a specific adapt method see `adapt_specific_nsignature`
308 private fun adapt_nsignature
(n_signature
: nullable ASignature): ASignature
310 if n_signature
== null then return new ASignature
311 return adapt_specific_nsignature
(n_signature
)
314 # Create the initial contract (intro)
315 # All contracts have the same implementation for the introduction.
321 # assert contract_condition
325 private fun create_intro_contract
(v
: ContractsVisitor, n_conditions
: Array[AExpr], mclassdef
: MClassDef)
327 var n_block
= v
.ast_builder
.make_block
328 for n_condition
in n_conditions
do
329 # Create a new tid to set the name of the assert for more explicit error
330 var tid
= new TId.init_tk
(n_condition
.location
)
331 tid
.text
= "{n_condition.location.text}"
332 var n_assert
= v
.ast_builder
.make_assert
(tid
, n_condition
, null)
333 # Define the assert location to reference the annoation
334 n_assert
.location
= n_condition
.location
337 make_contract
(v
, n_block
, mclassdef
)
340 # Create a contract to check the old (super call) and the new conditions
346 # super # Call the old contracts
347 # assert new_condition
351 private fun create_subcontract
(v
: ContractsVisitor, n_conditions
: Array[AExpr], mclassdef
: MClassDef)
353 var args
= v
.n_signature
.make_parameter_read
(v
.ast_builder
)
354 var n_block
= v
.ast_builder
.make_block
355 n_block
= self.create_inherit_nblock
(v
, n_conditions
, args
)
356 make_contract
(v
, n_block
, mclassdef
)
359 # Build a new contract method with a specific block `n_block` in a specified `mclassdef`
360 private fun make_contract
(v
: ContractsVisitor, n_block
: AExpr, mclassdef
: MClassDef)
362 var n_contractdef
= v
.toolcontext
.modelbuilder
.create_method_from_property
(self, mclassdef
, false, v
.m_signature
)
363 # Set the signature to keep the same variable
364 n_contractdef
.n_signature
= v
.n_signature
365 n_contractdef
.n_block
= n_block
366 # Define the location of the new method for corresponding of the annotation location
367 n_contractdef
.location
= v
.current_location
368 n_contractdef
.do_all
(v
.toolcontext
)
374 redef fun is_called
(v
: ContractsVisitor, mpropdef
: MPropDef): Bool
376 var main_package
= v
.mainmodule
.mpackage
377 var actual_package
= mpropdef
.mclassdef
.mmodule
.mpackage
378 if main_package
!= null and actual_package
!= null then
379 var condition_direct_arc
= v
.toolcontext
.modelbuilder
.model
.mpackage_importation_graph
.has_arc
(main_package
, actual_package
)
380 return super or main_package
== actual_package
or condition_direct_arc
385 # Display warning if no contract is defined at introduction `expect`,
386 # because if no contract is defined at the introduction the added
387 # contracts will not cause any error even if they are not satisfied.
393 # fun _bar_expect([...])
400 # redef fun bar is expect(contract_condition)
401 # redef fun _bar_expect([...])
403 # if (contract_condition) then return
409 redef fun no_intro_contract
(v
: ContractsVisitor, a
: Array[AAnnotation])
411 v
.toolcontext
.warning
(a
.first
.location
,"useless_contract","Useless contract: No contract defined at the introduction of the method")
414 redef fun create_inherit_nblock
(v
: ContractsVisitor, n_conditions
: Array[AExpr], super_args
: Array[AExpr]): ABlockExpr
416 var n_block
= v
.ast_builder
.make_block
417 for n_condition
in n_conditions
do
418 # Creating the if expression with the new condition
419 var if_block
= v
.ast_builder
.make_if
(n_condition
, n_condition
.mtype
)
420 # Creating and adding return expr to the then case
421 if_block
.n_then
= v
.ast_builder
.make_return
422 if_block
.location
= n_condition
.location
425 n_block
.add v
.ast_builder
.make_super_call
(super_args
)
429 redef fun adapt_method_to_contract
(v
: ContractsVisitor, mfacet
: MFacet, n_mpropdef
: AMethPropdef)
431 var callsite
= v
.ast_builder
.create_callsite
(v
.toolcontext
.modelbuilder
, n_mpropdef
, self, true)
432 var args
= n_mpropdef
.n_signature
.make_parameter_read
(v
.ast_builder
)
433 var n_callexpect
= v
.ast_builder
.make_call
(new ASelfExpr, callsite
,args
)
434 # Creation of the new instruction block with the call to expect condition
435 var actual_expr
= n_mpropdef
.n_block
436 var new_block
= new ABlockExpr
437 new_block
.n_expr
.push v
.encapsulated_contract_call
(n_mpropdef
, [n_callexpect
])
438 if actual_expr
isa ABlockExpr then
439 new_block
.n_expr
.add_all
(actual_expr
.n_expr
)
440 else if actual_expr
!= null then
441 new_block
.n_expr
.push
(actual_expr
)
443 n_mpropdef
.n_block
= new_block
444 mfacet
.has_applied_expect
= true
448 redef class BottomMContract
450 redef fun is_called
(v
: ContractsVisitor, mpropdef
: MPropDef): Bool
452 return super or v
.mainmodule
.mpackage
== mpropdef
.mclassdef
.mmodule
.mpackage
455 redef fun create_inherit_nblock
(v
: ContractsVisitor, n_conditions
: Array[AExpr], super_args
: Array[AExpr]): ABlockExpr
457 # Define contract block
458 var n_block
= v
.ast_builder
.make_block
460 var super_call
= v
.ast_builder
.make_super_call
(super_args
)
462 n_block
.add super_call
463 for n_condition
in n_conditions
do
464 var tid
= new TId.init_tk
(n_condition
.location
)
465 tid
.text
= "{n_condition.location.text}"
466 # Creating the assert expression with the new condition
467 var n_assert
= v
.ast_builder
.make_assert
(tid
, n_condition
)
468 n_assert
.location
= n_condition
.location
474 # Inject the `result` variable into the `n_block` of the given n_mpropdef`.
476 # The purpose of the variable is to capture return values to use it in contracts.
477 private fun inject_result
(v
: ContractsVisitor, n_mpropdef
: AMethPropdef, ret_type
: MType): Variable
479 expect
(n_mpropdef
.n_signature
.n_type
!= null)
481 var actual_block
= n_mpropdef
.n_block
482 # never happen. If it's the case the problem is in the contract facet building
483 assert actual_block
isa ABlockExpr
485 var return_expr
= actual_block
.n_expr
.last
.as(AReturnExpr)
487 var returned_expr
= return_expr
.n_expr
488 # The return node has no returned expression
489 assert returned_expr
!= null
491 var return_var
= new Variable("result")
492 # Creating a new variable to keep the old return of the method
493 var assign_result
= v
.ast_builder
.make_var_assign
(return_var
, returned_expr
)
494 # Remove the actual return
495 actual_block
.n_expr
.pop
496 # Set the return type
497 return_var
.declared_type
= ret_type
498 # Adding the reading expr of result variable to the block
499 actual_block
.add assign_result
500 # Expr to read the result variable
501 var read_result
= v
.ast_builder
.make_var_read
(return_var
, ret_type
)
502 # Definition of the new return
503 return_expr
= v
.ast_builder
.make_return
(read_result
)
504 actual_block
.add return_expr
511 redef fun adapt_specific_msignature
(m_signature
: MSignature): MSignature
513 return m_signature
.adapt_to_ensurecondition
516 redef fun adapt_specific_nsignature
(n_signature
: ASignature): ASignature
518 return n_signature
.adapt_to_ensurecondition
521 redef fun adapt_method_to_contract
(v
: ContractsVisitor, mfacet
: MFacet, n_mpropdef
: AMethPropdef)
523 var callsite
= v
.ast_builder
.create_callsite
(v
.toolcontext
.modelbuilder
, n_mpropdef
, self, true)
524 var n_self
= new ASelfExpr
525 # argument to call the contract method
526 var args
= n_mpropdef
.n_signature
.make_parameter_read
(v
.ast_builder
)
528 var actual_block
= n_mpropdef
.n_block
529 # never happen. If it's the case the problem is in the contract facet building
530 assert actual_block
isa ABlockExpr
532 var ret_type
= n_mpropdef
.mpropdef
.mproperty
.intro
.msignature
.return_mtype
533 if ret_type
!= null then
534 # Inject the variable result
535 var result_var
= inject_result
(v
, n_mpropdef
, ret_type
)
536 # Expr to read the result variable
537 var read_result
= v
.ast_builder
.make_var_read
(result_var
, ret_type
)
538 var return_expr
= actual_block
.n_expr
.pop
539 # Adding the read return to argument
540 args
.add
(read_result
)
541 var n_call_contract
= v
.ast_builder
.make_call
(n_self
, callsite
, args
)
542 actual_block
.add_all
([v
.encapsulated_contract_call
(n_mpropdef
, [n_call_contract
]), return_expr
])
544 # build the call to the contract method
545 var n_call_contract
= v
.ast_builder
.make_call
(n_self
, callsite
, args
)
546 actual_block
.add v
.encapsulated_contract_call
(n_mpropdef
, [n_call_contract
])
548 n_mpropdef
.do_all
(v
.toolcontext
)
549 mfacet
.has_applied_ensure
= true
555 # Define contract facet for MMethod in the given mclassdef. The facet represents the entry point with contracts (expect, ensure) of the method.
556 # If a contract is given adapt the contract facet.
558 # `classdef`: Indicates the class where we want to introduce our facet
559 # `exist_contract`: Indicates if it is necessary to define a new facet for the contract. If `exist_contract_facet and exist_contract` it's not necessary to add a facet.
566 # fun add_one is ensure(old(i) + 1 == i)
570 # fun add_one is ensure(old(i) + 1 == i)
572 # # The contract facet
573 # fun contract_add_one do
575 # ensure_add_one(old_add_one)
579 private fun define_contract_facet
(v
: ContractsVisitor, classdef
: MClassDef, mcontract
: nullable MContract)
581 var exist_contract_facet
= has_contract_facet
582 var contract_facet
= build_contract_facet
583 # Do nothing the contract and the contract facet already exist
584 if mcontract
!= null and mcontract
.is_already_applied
(contract_facet
) then return
586 var n_contract_facet
: AMethPropdef
587 if not exist_contract_facet
then
588 # If has no contract facet in intro just create it
589 if classdef
!= intro_mclassdef
then
590 var n_intro_face
= create_facet
(v
, intro_mclassdef
, contract_facet
, self)
591 n_intro_face
.location
= self.intro
.location
592 n_intro_face
.do_all
(v
.toolcontext
)
594 n_contract_facet
= create_facet
(v
, classdef
, contract_facet
, self)
596 # Check if the contract facet already exist in this context (in this classdef)
597 if classdef
.mpropdefs_by_property
.has_key
(contract_facet
) then
599 n_contract_facet
= v
.toolcontext
.modelbuilder
.mpropdef2node
(classdef
.mpropdefs_by_property
[contract_facet
]).as(AMethPropdef)
601 # create a new contract facet definition
602 n_contract_facet
= create_facet
(v
, classdef
, contract_facet
, self)
603 var block
= v
.ast_builder
.make_block
604 # super call to the contract facet
605 var args
= n_contract_facet
.n_signature
.make_parameter_read
(v
.ast_builder
)
606 var n_super_call
= v
.ast_builder
.make_super_call
(args
)
607 # verification for add a return or not
608 if self.intro
.msignature
.return_mtype
!= null then
609 block
.add
(v
.ast_builder
.make_return
(n_super_call
))
611 block
.add
(n_super_call
)
613 n_contract_facet
.n_block
= block
616 if mcontract
!= null then mcontract
.adapt_method_to_contract
(v
, contract_facet
, n_contract_facet
)
618 n_contract_facet
.location
= v
.current_location
619 n_contract_facet
.do_all
(v
.toolcontext
)
622 # Method to create a facet of the method.
623 # See `define_contract_facet` for more information about two types of facets.
625 # `called` : is the property to call in this facet.
626 private fun create_facet
(v
: ContractsVisitor, classdef
: MClassDef, facet
: MFacet, called
: MMethod): AMethPropdef
628 expect
( called
.is_same_instance
(self) or called
.is_same_instance
(self.mcontract_facet
) )
630 # Defines the contract facet is an init or not
631 # it is necessary to use the contracts with in a constructor
632 facet
.is_init
= is_init
633 var n_contractdef
= v
.toolcontext
.modelbuilder
.create_method_from_property
(facet
, classdef
, false, self.intro
.msignature
)
634 # FIXME set the location because the callsite creation need the node location
635 n_contractdef
.location
= v
.current_location
636 n_contractdef
.validate
638 var block
= v
.ast_builder
.make_block
640 # Arguments to call the `called` property
641 var args
: Array[AExpr]
642 args
= n_contractdef
.n_signature
.make_parameter_read
(v
.ast_builder
)
644 var callsite
= v
.ast_builder
.create_callsite
(v
.toolcontext
.modelbuilder
, n_contractdef
, called
, true)
645 var n_call
= v
.ast_builder
.make_call
(new ASelfExpr, callsite
, args
)
647 if self.intro
.msignature
.return_mtype
== null then
650 block
.add
(v
.ast_builder
.make_return
(n_call
))
653 n_contractdef
.n_block
= block
654 n_contractdef
.do_all
(v
.toolcontext
)
659 redef class MMethodDef
661 # Entry point to build contract (define the contract facet and define the contract method verification)
662 private fun construct_contract
(v
: ContractsVisitor, n_signature
: ASignature, n_annotations
: Array[AAnnotation], mcontract
: MContract, exist_contract
: Bool)
664 v
.define_signature
(mcontract
, n_signature
, mproperty
.intro
.msignature
)
665 if not exist_contract
and not is_intro
then no_intro_contract
(v
, mcontract
, n_annotations
)
666 v
.build_contract
(n_annotations
, mcontract
, mclassdef
)
667 # Check if the contract must be called to know if it's needed to construct the facet
668 if mcontract
.is_called
(v
, self) then mproperty
.define_contract_facet
(v
, mclassdef
, mcontract
)
671 # Create a contract on the introduction classdef of the property.
672 # Display an warning message if necessary
673 private fun no_intro_contract
(v
: ContractsVisitor, mcontract
: MContract, n_annotations
: Array[AAnnotation])
675 v
.toolcontext
.modelbuilder
.create_method_from_property
(mcontract
, mcontract
.intro_mclassdef
, false, v
.m_signature
)
676 mcontract
.no_intro_contract
(v
, n_annotations
)
679 # Apply the `no_contract` annotation to the contract. This method removes the inheritance by adding an empty contract method.
680 # Display a warning if the annotation is not needed
681 private fun no_contract_apply
(v
: ContractsVisitor, n_signature
: ASignature)
683 var mensure
= mproperty
.mensure
684 var mexpect
= mproperty
.mexpect
685 if mensure
== null and mexpect
== null then
686 v
.toolcontext
.warning
(location
, "useless_nocontract", "Useless `no_contract`, no contract was declared for `{name}`. Remove the `no_contract`")
688 if mensure
!= null then
689 # Add an empty ensure method to replace the actual definition
690 v
.toolcontext
.modelbuilder
.create_method_from_property
(mensure
, mclassdef
, false, mensure
.intro
.msignature
)
692 if mexpect
!= null then
693 # Add an empty expect method to replace the actual definition
694 v
.toolcontext
.modelbuilder
.create_method_from_property
(mexpect
, mclassdef
, false, mexpect
.intro
.msignature
)
700 redef fun check_callsite
(v
)
702 v
.visited_propdef
= self
706 redef class AMethPropdef
708 # Entry point to create a contract (verification of inheritance, or new contract).
709 redef fun create_contracts
(v
)
711 v
.ast_builder
.check_mmodule
(mpropdef
.mclassdef
.mmodule
)
712 v
.current_location
= self.location
713 v
.is_intro_contract
= mpropdef
.is_intro
715 if not mpropdef
.is_intro
then check_redef
(v
)
718 # Verification of the annotation to know if it is a contract annotation.
719 # If this is the case, we built the appropriate contract.
720 private fun check_annotation
(v
: ContractsVisitor)
722 var annotations_expect
= get_annotations
("expect")
723 var annotations_ensure
= get_annotations
("ensure")
724 var annotation_no_contract
= get_annotations
("no_contract")
726 if (not annotations_expect
.is_empty
or not annotations_ensure
.is_empty
) and not annotation_no_contract
.is_empty
then
727 v
.toolcontext
.error
(location
, "The new contract definition is not correct when using `no_contract`. Remove the contract definition or the `no_contract`")
731 var nsignature
= n_signature
or else new ASignature
733 if not annotation_no_contract
.is_empty
then
734 mpropdef
.no_contract_apply
(v
, nsignature
.clone
)
738 if not annotations_expect
.is_empty
then
739 var exist_contract
= mpropdef
.mproperty
.has_expect
740 mpropdef
.construct_contract
(v
, nsignature
.clone
, annotations_expect
, mpropdef
.mproperty
.build_expect
, exist_contract
)
743 if not annotations_ensure
.is_empty
then
744 var exist_contract
= mpropdef
.mproperty
.has_ensure
745 mpropdef
.construct_contract
(v
, nsignature
.clone
, annotations_ensure
, mpropdef
.mproperty
.build_ensure
, exist_contract
)
749 # Verification if the method have an inherited contract to apply it.
750 private fun check_redef
(v
: ContractsVisitor)
752 var mexpect
= mpropdef
.mproperty
.mexpect
753 var mensure
= mpropdef
.mproperty
.mensure
754 var mcontract_facet
= mpropdef
.mproperty
.mcontract_facet
756 if mexpect
!= null then
757 if mcontract_facet
!= null and mcontract_facet
.has_applied_expect
then return
758 if mexpect
.is_called
(v
, mpropdef
.as(not null)) then mpropdef
.mproperty
.define_contract_facet
(v
, mpropdef
.mclassdef
, mexpect
)
760 if mensure
!= null then
761 if mcontract_facet
!= null and mcontract_facet
.has_applied_ensure
then return
762 if mensure
.is_called
(v
, mpropdef
.as(not null)) then mpropdef
.mproperty
.define_contract_facet
(v
, mpropdef
.mclassdef
, mensure
)
767 redef class MSignature
769 # Adapt signature for an contract
771 # The returned `MSignature` is the copy of `self` without return type.
772 private fun adapt_to_contract
: MSignature do return new MSignature(mparameters
.to_a
, null)
774 # Adapt signature for a ensure contract
776 # The returned `MSignature` is the copy of `self` without return type.
777 # The return type is replaced by a new parameter `result`
778 private fun adapt_to_ensurecondition
: MSignature
780 var rtype
= return_mtype
781 var msignature
= adapt_to_contract
782 if rtype
!= null then
783 msignature
.mparameters
.add
(new MParameter("result", rtype
, false))
788 # The returned `MSignature` is the exact copy of `self`.
789 private fun clone
: MSignature do return new MSignature(mparameters
.to_a
, return_mtype
)
792 redef class ASignature
794 # Create an array of AVarExpr representing the read of every parameters
795 private fun make_parameter_read
(ast_builder
: ASTBuilder): Array[AVarExpr]
797 var args
= new Array[AVarExpr]
798 for n_param
in self.n_params
do
799 var mtype
= n_param
.variable
.declared_type
800 var variable
= n_param
.variable
801 if variable
!= null and mtype
!= null then
802 args
.push ast_builder
.make_var_read
(variable
, mtype
)
808 # Create a new ASignature adapted for contract
810 # The returned `ASignature` is the copy of `self` without return type.
811 private fun adapt_to_contract
: ASignature
813 var adapt_nsignature
= self.clone
814 if adapt_nsignature
.n_type
!= null then adapt_nsignature
.n_type
.detach
815 return adapt_nsignature
818 # Create a new ASignature adapted for ensure
820 # The returned `ASignature` is the copy of `self` without return type.
821 # The return type is replaced by a new parameter `result`
822 private fun adapt_to_ensurecondition
: ASignature do
823 var nsignature
= adapt_to_contract
824 if ret_type
!= null then
825 var variable
= new Variable("result")
826 variable
.declared_type
= ret_type
827 nsignature
.n_params
.add
new AParam.make
(variable
, ret_type
.create_ast_representation
)
833 redef class ASendExpr
834 redef fun check_callsite
(v
)
836 var actual_callsite
= callsite
837 if actual_callsite
!= null then
838 callsite
= v
.drive_callsite_to_contract
(actual_callsite
)
839 # Set the signature mapping with the old value, this avoids having to re-check the callsite.
840 callsite
.signaturemap
= actual_callsite
.signaturemap
846 redef fun check_callsite
(v
)
848 var actual_callsite
= callsite
849 if actual_callsite
!= null then
850 callsite
= v
.drive_callsite_to_contract
(actual_callsite
)
851 # Set the signature mapping with the old value, this avoids having to re-check the callsite
852 callsite
.signaturemap
= actual_callsite
.signaturemap