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 create_facet
(v
, intro_mclassdef
, contract_facet
, self)
592 n_contract_facet
= create_facet
(v
, classdef
, contract_facet
, self)
594 # Check if the contract facet already exist in this context (in this classdef)
595 if classdef
.mpropdefs_by_property
.has_key
(contract_facet
) then
597 n_contract_facet
= v
.toolcontext
.modelbuilder
.mpropdef2node
(classdef
.mpropdefs_by_property
[contract_facet
]).as(AMethPropdef)
599 # create a new contract facet definition
600 n_contract_facet
= create_facet
(v
, classdef
, contract_facet
, self)
601 var block
= v
.ast_builder
.make_block
602 # super call to the contract facet
603 var args
= n_contract_facet
.n_signature
.make_parameter_read
(v
.ast_builder
)
604 var n_super_call
= v
.ast_builder
.make_super_call
(args
)
605 # verification for add a return or not
606 if self.intro
.msignature
.return_mtype
!= null then
607 block
.add
(v
.ast_builder
.make_return
(n_super_call
))
609 block
.add
(n_super_call
)
611 n_contract_facet
.n_block
= block
614 if mcontract
!= null then mcontract
.adapt_method_to_contract
(v
, contract_facet
, n_contract_facet
)
616 n_contract_facet
.location
= v
.current_location
617 n_contract_facet
.do_all
(v
.toolcontext
)
620 # Method to create a facet of the method.
621 # See `define_contract_facet` for more information about two types of facets.
623 # `called` : is the property to call in this facet.
624 private fun create_facet
(v
: ContractsVisitor, classdef
: MClassDef, facet
: MFacet, called
: MMethod): AMethPropdef
626 expect
( called
.is_same_instance
(self) or called
.is_same_instance
(self.mcontract_facet
) )
628 # Defines the contract facet is an init or not
629 # it is necessary to use the contracts with in a constructor
630 facet
.is_init
= is_init
631 var n_contractdef
= v
.toolcontext
.modelbuilder
.create_method_from_property
(facet
, classdef
, false, self.intro
.msignature
)
632 # FIXME set the location because the callsite creation need the node location
633 n_contractdef
.location
= v
.current_location
634 n_contractdef
.validate
636 var block
= v
.ast_builder
.make_block
638 # Arguments to call the `called` property
639 var args
: Array[AExpr]
640 args
= n_contractdef
.n_signature
.make_parameter_read
(v
.ast_builder
)
642 var callsite
= v
.ast_builder
.create_callsite
(v
.toolcontext
.modelbuilder
, n_contractdef
, called
, true)
643 var n_call
= v
.ast_builder
.make_call
(new ASelfExpr, callsite
, args
)
645 if self.intro
.msignature
.return_mtype
== null then
648 block
.add
(v
.ast_builder
.make_return
(n_call
))
651 n_contractdef
.n_block
= block
652 n_contractdef
.do_all
(v
.toolcontext
)
657 redef class MMethodDef
659 # Entry point to build contract (define the contract facet and define the contract method verification)
660 private fun construct_contract
(v
: ContractsVisitor, n_signature
: ASignature, n_annotations
: Array[AAnnotation], mcontract
: MContract, exist_contract
: Bool)
662 v
.define_signature
(mcontract
, n_signature
, mproperty
.intro
.msignature
)
663 if not exist_contract
and not is_intro
then no_intro_contract
(v
, mcontract
, n_annotations
)
664 v
.build_contract
(n_annotations
, mcontract
, mclassdef
)
665 # Check if the contract must be called to know if it's needed to construct the facet
666 if mcontract
.is_called
(v
, self) then mproperty
.define_contract_facet
(v
, mclassdef
, mcontract
)
669 # Create a contract on the introduction classdef of the property.
670 # Display an warning message if necessary
671 private fun no_intro_contract
(v
: ContractsVisitor, mcontract
: MContract, n_annotations
: Array[AAnnotation])
673 v
.toolcontext
.modelbuilder
.create_method_from_property
(mcontract
, mcontract
.intro_mclassdef
, false, v
.m_signature
)
674 mcontract
.no_intro_contract
(v
, n_annotations
)
677 # Apply the `no_contract` annotation to the contract. This method removes the inheritance by adding an empty contract method.
678 # Display a warning if the annotation is not needed
679 private fun no_contract_apply
(v
: ContractsVisitor, n_signature
: ASignature)
681 var mensure
= mproperty
.mensure
682 var mexpect
= mproperty
.mexpect
683 if mensure
== null and mexpect
== null then
684 v
.toolcontext
.warning
(location
, "useless_nocontract", "Useless `no_contract`, no contract was declared for `{name}`. Remove the `no_contract`")
686 if mensure
!= null then
687 # Add an empty ensure method to replace the actual definition
688 v
.toolcontext
.modelbuilder
.create_method_from_property
(mensure
, mclassdef
, false, mensure
.intro
.msignature
)
690 if mexpect
!= null then
691 # Add an empty expect method to replace the actual definition
692 v
.toolcontext
.modelbuilder
.create_method_from_property
(mexpect
, mclassdef
, false, mexpect
.intro
.msignature
)
698 redef fun check_callsite
(v
)
700 v
.visited_propdef
= self
704 redef class AMethPropdef
706 # Entry point to create a contract (verification of inheritance, or new contract).
707 redef fun create_contracts
(v
)
709 v
.ast_builder
.check_mmodule
(mpropdef
.mclassdef
.mmodule
)
710 v
.current_location
= self.location
711 v
.is_intro_contract
= mpropdef
.is_intro
713 if not mpropdef
.is_intro
then check_redef
(v
)
716 # Verification of the annotation to know if it is a contract annotation.
717 # If this is the case, we built the appropriate contract.
718 private fun check_annotation
(v
: ContractsVisitor)
720 var annotations_expect
= get_annotations
("expect")
721 var annotations_ensure
= get_annotations
("ensure")
722 var annotation_no_contract
= get_annotations
("no_contract")
724 if (not annotations_expect
.is_empty
or not annotations_ensure
.is_empty
) and not annotation_no_contract
.is_empty
then
725 v
.toolcontext
.error
(location
, "The new contract definition is not correct when using `no_contract`. Remove the contract definition or the `no_contract`")
729 var nsignature
= n_signature
or else new ASignature
731 if not annotation_no_contract
.is_empty
then
732 mpropdef
.no_contract_apply
(v
, nsignature
.clone
)
736 if not annotations_expect
.is_empty
then
737 var exist_contract
= mpropdef
.mproperty
.has_expect
738 mpropdef
.construct_contract
(v
, nsignature
.clone
, annotations_expect
, mpropdef
.mproperty
.build_expect
, exist_contract
)
741 if not annotations_ensure
.is_empty
then
742 var exist_contract
= mpropdef
.mproperty
.has_ensure
743 mpropdef
.construct_contract
(v
, nsignature
.clone
, annotations_ensure
, mpropdef
.mproperty
.build_ensure
, exist_contract
)
747 # Verification if the method have an inherited contract to apply it.
748 private fun check_redef
(v
: ContractsVisitor)
750 var mexpect
= mpropdef
.mproperty
.mexpect
751 var mensure
= mpropdef
.mproperty
.mensure
752 var mcontract_facet
= mpropdef
.mproperty
.mcontract_facet
754 if mexpect
!= null then
755 if mcontract_facet
!= null and mcontract_facet
.has_applied_expect
then return
756 if mexpect
.is_called
(v
, mpropdef
.as(not null)) then mpropdef
.mproperty
.define_contract_facet
(v
, mpropdef
.mclassdef
, mexpect
)
758 if mensure
!= null then
759 if mcontract_facet
!= null and mcontract_facet
.has_applied_ensure
then return
760 if mensure
.is_called
(v
, mpropdef
.as(not null)) then mpropdef
.mproperty
.define_contract_facet
(v
, mpropdef
.mclassdef
, mensure
)
765 redef class MSignature
767 # Adapt signature for an contract
769 # The returned `MSignature` is the copy of `self` without return type.
770 private fun adapt_to_contract
: MSignature do return new MSignature(mparameters
.to_a
, null)
772 # Adapt signature for a ensure contract
774 # The returned `MSignature` is the copy of `self` without return type.
775 # The return type is replaced by a new parameter `result`
776 private fun adapt_to_ensurecondition
: MSignature
778 var rtype
= return_mtype
779 var msignature
= adapt_to_contract
780 if rtype
!= null then
781 msignature
.mparameters
.add
(new MParameter("result", rtype
, false))
786 # The returned `MSignature` is the exact copy of `self`.
787 private fun clone
: MSignature do return new MSignature(mparameters
.to_a
, return_mtype
)
790 redef class ASignature
792 # Create an array of AVarExpr representing the read of every parameters
793 private fun make_parameter_read
(ast_builder
: ASTBuilder): Array[AVarExpr]
795 var args
= new Array[AVarExpr]
796 for n_param
in self.n_params
do
797 var mtype
= n_param
.variable
.declared_type
798 var variable
= n_param
.variable
799 if variable
!= null and mtype
!= null then
800 args
.push ast_builder
.make_var_read
(variable
, mtype
)
806 # Create a new ASignature adapted for contract
808 # The returned `ASignature` is the copy of `self` without return type.
809 private fun adapt_to_contract
: ASignature
811 var adapt_nsignature
= self.clone
812 if adapt_nsignature
.n_type
!= null then adapt_nsignature
.n_type
.detach
813 return adapt_nsignature
816 # Create a new ASignature adapted for ensure
818 # The returned `ASignature` is the copy of `self` without return type.
819 # The return type is replaced by a new parameter `result`
820 private fun adapt_to_ensurecondition
: ASignature do
821 var nsignature
= adapt_to_contract
822 if ret_type
!= null then
823 var variable
= new Variable("result")
824 variable
.declared_type
= ret_type
825 nsignature
.n_params
.add
new AParam.make
(variable
, ret_type
.create_ast_representation
)
831 redef class ASendExpr
832 redef fun check_callsite
(v
)
834 var actual_callsite
= callsite
835 if actual_callsite
!= null then
836 callsite
= v
.drive_callsite_to_contract
(actual_callsite
)
842 redef fun check_callsite
(v
)
844 var actual_callsite
= callsite
845 if actual_callsite
!= null then
846 callsite
= v
.drive_callsite_to_contract
(actual_callsite
)