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"
22 import parse_annotations
25 intrude import modelize_property
29 redef class ToolContext
30 # Parses contracts annotations.
31 var contracts_phase
: Phase = new ContractsPhase(self, [modelize_property_phase
,typing_phase
])
34 private class ContractsPhase
37 # The entry point of the contract phase
38 # In reality, the contract phase is executed on each module
39 # FIXME: Actually all method is checked to add method if any contract is inherited
40 redef fun process_nmodule
(nmodule
)do
41 # Check if the contracts are disabled
42 if toolcontext
.opt_no_contract
.value
then return
43 nmodule
.do_contracts
(self.toolcontext
)
48 # Compile all contracts
50 # The implementation of the contracts is done in two visits.
52 # - First step, the visitor analyzes and constructs the contracts
53 # for each class (invariant) and method (expects, ensures).
55 # - Second step the visitor analyzes each `ASendExpr` to see
56 # if the callsite calls a method with a contract. If this is
57 # the case the callsite is replaced by another callsite to the contract method.
58 fun do_contracts
(toolcontext
: ToolContext) do
60 var contract_visitor
= new ContractsVisitor(toolcontext
, toolcontext
.modelbuilder
.identified_modules
.first
, self, new ASTBuilder(mmodule
.as(not null)))
61 contract_visitor
.enter_visit
(self)
63 var callsite_visitor
= new CallSiteVisitor(toolcontext
)
64 callsite_visitor
.enter_visit
(self)
68 # 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
69 private class ContractsVisitor
72 var toolcontext
: ToolContext
75 # It's strore to define if the contract need to be build depending on the selected policy `--no-contract` `--full-contract` or default
76 var mainmodule
: MModule
78 # Actual visited module
79 var visited_module
: AModule
81 var ast_builder
: ASTBuilder
83 # The `ASignature` of the actual build contract
84 var n_signature
: ASignature is noinit
86 # The `MSignature` of the actual build contract
87 var m_signature
: MSignature is noinit
89 # The `current_location` can corresponding of the annotation or method location.
90 var current_location
: Location is noinit
92 # Is the contrat is an introduction or not?
93 var is_intro_contract
: Bool is noinit
95 # Actual visited class
96 var visited_class
: nullable AClassdef
98 # is `no_contract` annotation was found
99 var find_no_contract
= false
101 redef fun visit
(node
)
103 node
.create_contracts
(self)
107 # Method use to define the signature part of the method `ASignature` and `MSignature`
108 # The given `mcontract` provided `adapt_nsignature` and `adapt_msignature` to copy and adapt the given signature (`nsignature` and `msignature`)
109 fun define_signature
(mcontract
: MContract, nsignature
: nullable ASignature, msignature
: nullable MSignature)
111 if nsignature
!= null and msignature
!= null then nsignature
.ret_type
= msignature
.return_mtype
112 self.n_signature
= mcontract
.adapt_nsignature
(nsignature
)
113 self.m_signature
= mcontract
.adapt_msignature
(msignature
)
116 # Define the new contract take in consideration that an old contract exist or not
117 private fun build_contract
(n_annotation
: AAnnotation, mcontract
: MContract, mclassdef
: MClassDef): MMethodDef
119 self.current_location
= n_annotation
.location
120 # Retrieving the expression provided in the annotation
121 var n_condition
= n_annotation
.construct_condition
(self)
122 var m_contractdef
: AMethPropdef
123 if is_intro_contract
then
124 # Create new contract method
125 m_contractdef
= mcontract
.create_intro_contract
(self, n_condition
, mclassdef
)
127 # Create a redef of contract to take in consideration the new condition
128 m_contractdef
= mcontract
.create_subcontract
(self, n_condition
, mclassdef
)
130 var contract_propdef
= m_contractdef
.mpropdef
131 # The contract has a null mpropdef, this should never happen
132 assert contract_propdef
!= null
133 return contract_propdef
137 # This visitor checks the `callsite` to see if the target `mpropdef` has a contract.
138 private class CallSiteVisitor
141 var toolcontext
: ToolContext
143 # Actual visited method
144 var visited_method
: APropdef is noinit
146 redef fun visit
(node
)
148 node
.check_callsite
(self)
152 # Check if the callsite calls a method with a contract.
153 # If it's the case the callsite is replaced by another callsite to the contract method.
154 private fun drive_method_contract
(callsite
: CallSite): CallSite
156 if callsite
.mpropdef
.has_contract
then
157 var contract_facet
= callsite
.mproperty
.mcontract_facet
158 var visited_mpropdef
= visited_method
.mpropdef
159 assert contract_facet
!= null and visited_mpropdef
!= null
161 var unsafe_mtype
= callsite
.recv
.resolve_for
(visited_mpropdef
.mclassdef
.bound_mtype
, callsite
.anchor
, visited_mpropdef
.mclassdef
.mmodule
, true)
163 # This check is needed because the contract can appear after the introduction.
164 if unsafe_mtype
.has_mproperty
(visited_method
.mpropdef
.mclassdef
.mmodule
, contract_facet
) then
165 var type_visitor
= new TypeVisitor(toolcontext
.modelbuilder
, visited_mpropdef
)
166 var drived_callsite
= type_visitor
.build_callsite_by_property
(visited_method
, callsite
.recv
, contract_facet
, callsite
.recv_is_self
)
167 # This never happen this check is here for debug
168 assert drived_callsite
!= null
169 return drived_callsite
177 private fun create_contracts
(v
: ContractsVisitor) do end
178 private fun check_callsite
(v
: CallSiteVisitor) do end
181 redef class AAnnotation
183 # Returns the conditions of annotation parameters in the form of and expr
185 # the contract ensures(true, i == 10, f >= 1.0)
186 # return this condition (true and i == 10 and f >= 1.0)
187 private fun construct_condition
(v
: ContractsVisitor): AExpr
189 var n_condition
= n_args
.first
191 for n_arg
in n_args
do n_condition
= v
.ast_builder
.make_and
(n_condition
, n_arg
)
196 # The root of all contracts
198 # The objective of this class is to provide the set
199 # of services must be implemented or provided by a contract
200 abstract class MContract
203 # Define the name of the contract
204 fun contract_name
: String is abstract
206 # Checking if the use of the contract is necessary
207 private fun check_usage
(v
: ContractsVisitor, actual_mmodule
: MModule): Bool is abstract
209 # Method use to diplay warning when the contract is not present at the introduction
210 private fun no_intro_contract
(v
: ContractsVisitor, a
: AAnnotation)do end
212 # Creating specific inheritance block contract
213 private fun create_nblock
(v
: ContractsVisitor, n_condition
: AExpr, args
: Array[AExpr]): ABlockExpr is abstract
215 # Method to adapt the `n_mpropdef.n_block` to the contract
216 private fun adapt_block_to_contract
(v
: ContractsVisitor, n_mpropdef
: AMethPropdef) is abstract
218 # Adapt the msignature specifically for the contract method
219 private fun adapt_specific_msignature
(m_signature
: MSignature): MSignature do return m_signature
.adapt_to_condition
221 # Adapt the nsignature specifically for the contract method
222 private fun adapt_specific_nsignature
(n_signature
: ASignature): ASignature do return n_signature
.adapt_to_condition
(null)
224 # Adapt the `m_signature` to the contract
225 # If it is not null call the specific adapt `m_signature` for the contract
226 private fun adapt_msignature
(m_signature
: nullable MSignature): MSignature
228 if m_signature
== null then return new MSignature(new Array[MParameter])
229 return adapt_specific_msignature
(m_signature
)
232 # Adapt the `n_signature` to the contract
233 # If it is not null call the specific adapt `n_signature` for the contract
234 private fun adapt_nsignature
(n_signature
: nullable ASignature): ASignature
236 if n_signature
== null then return new ASignature
237 return adapt_specific_nsignature
(n_signature
)
240 # Create a new empty contract
241 private fun create_empty_contract
(v
: ContractsVisitor, mclassdef
: MClassDef, msignature
: nullable MSignature, n_signature
: ASignature)
243 var n_contract_def
= intro_mclassdef
.mclass
.create_empty_method
(v
, self, mclassdef
, msignature
, n_signature
)
244 n_contract_def
.do_all
(v
.toolcontext
)
247 # Create the initial contract (intro)
248 # All contracts have the same implementation for the introduction.
252 # assert contract_condition
255 private fun create_intro_contract
(v
: ContractsVisitor, n_condition
: nullable AExpr, mclassdef
: MClassDef): AMethPropdef
257 var n_block
= v
.ast_builder
.make_block
258 if n_condition
!= null then
259 # Create a new tid to set the name of the assert for more explicit error
260 var tid
= new TId.init_tk
(self.location
)
261 tid
.text
= "{self.contract_name}"
262 n_block
.add v
.ast_builder
.make_assert
(tid
, n_condition
, null)
264 return make_contract
(v
, n_block
, mclassdef
)
267 # Create a contract with old (super) and the new conditions
268 private fun create_subcontract
(v
: ContractsVisitor, ncondition
: nullable AExpr, mclassdef
: MClassDef): AMethPropdef
270 var args
= v
.n_signature
.make_parameter_read
(v
.ast_builder
)
271 var n_block
= v
.ast_builder
.make_block
272 if ncondition
!= null then n_block
= self.create_nblock
(v
, ncondition
, args
)
273 return make_contract
(v
, n_block
, mclassdef
)
276 # Build a method with a specific block `n_block` in a specified `mclassdef`
277 private fun make_contract
(v
: ContractsVisitor, n_block
: AExpr, mclassdef
: MClassDef): AMethPropdef
279 var n_contractdef
= intro_mclassdef
.mclass
.create_empty_method
(v
, self, mclassdef
, v
.m_signature
, v
.n_signature
)
280 n_contractdef
.n_block
= n_block
281 # Define the location of the new method for corresponding of the annotation location
282 n_contractdef
.location
= v
.current_location
283 n_contractdef
.do_all
(v
.toolcontext
)
288 # A expect (precondition) contract representation
289 # This method check if the requirements of the called method is true.
293 # Define the name of the contract
294 redef fun contract_name
: String do return "expects"
296 # Verification if the construction of the contract is necessary.
297 # Three cases are checked for `expects`:
299 # - Is the `--full-contract` option it's use?
300 # - Is the method is in the main package
301 # - Is the method is in a direct imported package.
303 redef fun check_usage
(v
: ContractsVisitor, actual_mmodule
: MModule): Bool
305 var main_package
= v
.mainmodule
.mpackage
306 var actual_package
= actual_mmodule
.mpackage
307 if main_package
!= null and actual_package
!= null then
308 var condition_direct_arc
= v
.toolcontext
.modelbuilder
.model
.mpackage_importation_graph
.has_arc
(main_package
, actual_package
)
309 return v
.toolcontext
.opt_full_contract
.value
or condition_direct_arc
or main_package
== actual_package
314 # Display warning if no contract is defined at introduction `expect`,
315 # because if no contract is defined at the introduction the added
316 # contracts will not cause any error even if they are not satisfied.
322 # fun _bar_expects([...])
329 # redef fun bar is expects(contract_condition)
330 # redef fun _bar_expects([...])
332 # if not (contract_condition) then super
337 redef fun no_intro_contract
(v
: ContractsVisitor, a
: AAnnotation)
339 v
.toolcontext
.warning
(a
.location
,"","Useless contract: No contract defined at the introduction of the method")
342 redef fun create_nblock
(v
: ContractsVisitor, n_condition
: AExpr, args
: Array[AExpr]): ABlockExpr
344 # Creating the if expression with the new condition
345 var if_block
= v
.ast_builder
.make_if
(n_condition
, n_condition
.mtype
)
346 # Creating and adding return expr to the then case
347 if_block
.n_then
= v
.ast_builder
.make_return
(null)
348 # Creating the super call to the contract and adding this to else case
349 if_block
.n_else
= v
.ast_builder
.make_super_call
(args
,null)
350 var n_block
= v
.ast_builder
.make_block
355 redef fun adapt_block_to_contract
(v
: ContractsVisitor, n_mpropdef
: AMethPropdef)
357 var callsite
= v
.ast_builder
.create_callsite
(v
.toolcontext
.modelbuilder
, n_mpropdef
, self, true)
358 var n_self
= new ASelfExpr
359 var args
= n_mpropdef
.n_signature
.make_parameter_read
(v
.ast_builder
)
360 var n_callexpect
= v
.ast_builder
.make_call
(n_self
,callsite
,args
)
361 # Creation of the new instruction block with the call to expect condition
362 var actual_expr
= n_mpropdef
.n_block
363 var new_block
= new ABlockExpr
364 new_block
.n_expr
.push n_callexpect
365 if actual_expr
isa ABlockExpr then
366 new_block
.n_expr
.add_all
(actual_expr
.n_expr
)
367 else if actual_expr
!= null then
368 new_block
.n_expr
.push
(actual_expr
)
370 n_mpropdef
.n_block
= new_block
374 # The root of all contracts where the call is after the execution of the original method (`invariants` and `ensures`).
375 abstract class BottomMContract
378 # Verification if the construction of the contract is necessary.
379 # Two cases are checked for `expects`:
381 # - Is the `--full-contract` option it's use?
382 # - Is the method is in the main package
384 redef fun check_usage
(v
: ContractsVisitor, actual_mmodule
: MModule): Bool
386 return v
.toolcontext
.opt_full_contract
.value
or v
.mainmodule
.mpackage
== actual_mmodule
.mpackage
389 redef fun create_nblock
(v
: ContractsVisitor, n_condition
: AExpr, args
: Array[AExpr]): ABlockExpr
391 var tid
= new TId.init_tk
(v
.current_location
)
392 tid
.text
= "{contract_name}"
393 # Creating the assert expression with the new condition
394 var assert_block
= v
.ast_builder
.make_assert
(tid
,n_condition
,null)
395 # Creating the super call to the contract
396 var super_call
= v
.ast_builder
.make_super_call
(args
,null)
397 # Define contract block
398 var n_block
= v
.ast_builder
.make_block
399 # Adding the expressions to the block
400 n_block
.add super_call
401 n_block
.add assert_block
405 # Inject the result variable in the `n_block` of the given `n_mpropdef`.
406 private fun inject_result
(v
: ContractsVisitor, n_mpropdef
: AMethPropdef, ret_type
: MType): Variable
408 var actual_block
= n_mpropdef
.n_block
409 # never happen. If it's the case the problem is in the contract facet building
410 assert actual_block
isa ABlockExpr
412 var return_var
: nullable Variable = null
414 var return_expr
= actual_block
.n_expr
.last
.as(AReturnExpr)
416 var returned_expr
= return_expr
.n_expr
417 # The return node has no returned expression
418 assert returned_expr
!= null
420 # Check if the result variable already exit
421 if returned_expr
isa AVarExpr then
422 if returned_expr
.variable
.name
== "result" then
423 return_var
= returned_expr
.variable
427 return_var
= new Variable("result")
428 # Creating a new variable to keep the old return of the method
429 var assign_result
= v
.ast_builder
.make_var_assign
(return_var
, returned_expr
)
430 # Remove the actual return
431 actual_block
.n_expr
.pop
432 # Set the return type
433 return_var
.declared_type
= ret_type
434 # Adding the reading expr of result variable to the block
435 actual_block
.add assign_result
436 # Expr to read the result variable
437 var read_result
= v
.ast_builder
.make_var_read
(return_var
, ret_type
)
438 # Definition of the new return
439 return_expr
= v
.ast_builder
.make_return
(read_result
)
440 actual_block
.add return_expr
445 # A ensure (postcondition) representation
446 # This method check if the called method respects the expectations of the caller.
448 super BottomMContract
450 # Define the name of the contract
451 redef fun contract_name
: String do return "ensures"
453 redef fun adapt_specific_msignature
(m_signature
: MSignature): MSignature
455 return m_signature
.adapt_to_ensurecondition
458 redef fun adapt_specific_nsignature
(n_signature
: ASignature): ASignature
460 return n_signature
.adapt_to_ensurecondition
463 redef fun adapt_block_to_contract
(v
: ContractsVisitor, n_mpropdef
: AMethPropdef)
465 var callsite
= v
.ast_builder
.create_callsite
(v
.toolcontext
.modelbuilder
, n_mpropdef
, self, true)
466 var n_self
= new ASelfExpr
467 # argument to call the contract method
468 var args
= n_mpropdef
.n_signature
.make_parameter_read
(v
.ast_builder
)
469 # Inject the variable result
470 # The cast is always safe because the online adapted method is the contract facet
472 var actual_block
= n_mpropdef
.n_block
473 # never happen. If it's the case the problem is in the contract facet building
474 assert actual_block
isa ABlockExpr
476 var ret_type
= n_mpropdef
.mpropdef
.mproperty
.intro
.msignature
.return_mtype
477 if ret_type
!= null then
478 var result_var
= inject_result
(v
, n_mpropdef
, ret_type
)
479 # Expr to read the result variable
480 var read_result
= v
.ast_builder
.make_var_read
(result_var
, ret_type
)
481 var return_expr
= actual_block
.n_expr
.pop
482 # Adding the read return to argument
483 args
.add
(read_result
)
484 var n_callcontract
= v
.ast_builder
.make_call
(n_self
,callsite
,args
)
485 actual_block
.add_all
([n_callcontract
,return_expr
])
487 # build the call to the contract method
488 var n_callcontract
= v
.ast_builder
.make_call
(n_self
,callsite
,args
)
489 actual_block
.add n_callcontract
496 # This method create an abstract method representation with this MMethodDef an this AMethoddef
497 private fun create_abstract_method
(v
: ContractsVisitor, mproperty
: MMethod, mclassdef
: MClassDef, msignature
: nullable MSignature, n_signature
: ASignature): AMethPropdef
499 # new methoddef definition
500 var m_def
= new MMethodDef(mclassdef
, mproperty
, v
.current_location
)
502 if msignature
!= null then m_def
.msignature
= msignature
.clone
503 # set the abstract flag
504 m_def
.is_abstract
= true
505 # Build the new node method
506 var n_def
= v
.ast_builder
.make_method
(null,null,m_def
,n_signature
,null,null,null,null)
507 # Define the location of the new method for corresponding of the actual method
508 n_def
.location
= v
.current_location
509 # Association new npropdef to mpropdef
510 v
.toolcontext
.modelbuilder
.unsafe_add_mpropdef2npropdef
(m_def
,n_def
)
514 # Create method with an empty block
515 # 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
516 private fun create_empty_method
(v
: ContractsVisitor, mproperty
: MMethod, mclassdef
: MClassDef, msignature
: nullable MSignature, n_signature
: ASignature): AMethPropdef
518 var n_def
= create_abstract_method
(v
, mproperty
, mclassdef
, msignature
, n_signature
)
519 n_def
.mpropdef
.is_abstract
= false
520 n_def
.n_block
= v
.ast_builder
.make_block
527 # The contract facet of the method
528 # it's representing the method with contract
529 # This method call the contract and the method
530 var mcontract_facet
: nullable MMethod = null
532 # The expected contract method
533 var mexpect
: nullable MExpect = null
535 # The ensure contract method
536 var mensure
: nullable MEnsure = null
538 # Check if the MMethod has no ensure contract
539 # if this is the case returns false and built it
541 private fun check_exist_ensure
: Bool
543 if self.mensure
!= null then return true
544 # build a new `MEnsure` contract
545 self.mensure
= new MEnsure(intro_mclassdef
, "_ensures_{name}", intro_mclassdef
.location
, public_visibility
)
549 # Check if the MMethod has no expect contract
550 # if this is the case returns false and built it
552 private fun check_exist_expect
: Bool
554 if self.mexpect
!= null then return true
555 # build a new `MExpect` contract
556 self.mexpect
= new MExpect(intro_mclassdef
, "_expects_{name}", intro_mclassdef
.location
, public_visibility
)
560 # Check if the MMethod has an contract facet
561 # If the method has no contract facet she create it
562 private fun check_exist_contract_facet
(mpropdef
: MMethodDef): Bool
564 if self.mcontract_facet
!= null then return true
565 # build a new `MMethod` contract
566 self.mcontract_facet
= new MMethod(mpropdef
.mclassdef
, "_contract_{name}", mpropdef
.mclassdef
.location
, public_visibility
)
571 redef class MMethodDef
573 # Verification of the contract facet
574 # Check if a contract facet already exists to use it again or if it is necessary to create it.
575 private fun check_contract_facet
(v
: ContractsVisitor, n_signature
: ASignature, mcontract
: MContract, exist_contract
: Bool)
577 var exist_contract_facet
= mproperty
.check_exist_contract_facet
(self)
578 if exist_contract_facet
and exist_contract
then return
580 var contract_facet
: AMethPropdef
581 if not exist_contract_facet
then
582 # If has no contract facet just create it
583 contract_facet
= create_contract_facet
(v
, n_signature
)
585 # Check if the contract facet already exist in this context (in this mclassdef)
586 if mclassdef
.mpropdefs_by_property
.has_key
(mproperty
.mcontract_facet
) then
588 contract_facet
= v
.toolcontext
.modelbuilder
.mpropdef2node
(mclassdef
.mpropdefs_by_property
[mproperty
.mcontract_facet
]).as(AMethPropdef)
590 # create a new contract facet definition
591 contract_facet
= create_contract_facet
(v
, n_signature
)
592 var block
= v
.ast_builder
.make_block
593 # super call to the contract facet
594 var n_super_call
= v
.ast_builder
.make_super_call
(n_signature
.make_parameter_read
(v
.ast_builder
), null)
595 # verification for add a return or not
596 if contract_facet
.mpropdef
.msignature
.return_mtype
!= null then
597 block
.add
(v
.ast_builder
.make_return
(n_super_call
))
599 block
.add
(n_super_call
)
601 contract_facet
.n_block
= block
604 contract_facet
.adapt_block_to_contract
(v
, mcontract
, contract_facet
)
605 contract_facet
.location
= v
.current_location
606 contract_facet
.do_all
(v
.toolcontext
)
609 # Method to create a contract facet of the method
610 private fun create_contract_facet
(v
: ContractsVisitor, n_signature
: ASignature): AMethPropdef
612 var contract_facet
= mproperty
.mcontract_facet
613 assert contract_facet
!= null
614 # Defines the contract phase is an init or not
615 # it is necessary to use the contracts on constructor
616 contract_facet
.is_init
= self.mproperty
.is_init
618 # check if the method has an `msignature` to copy it.
619 var m_signature
: nullable MSignature = null
620 if mproperty
.intro
.msignature
!= null then m_signature
= mproperty
.intro
.msignature
.clone
622 var n_contractdef
= mclassdef
.mclass
.create_empty_method
(v
, contract_facet
, mclassdef
, m_signature
, n_signature
)
623 # FIXME set the location because the callsite creation need the node location
624 n_contractdef
.location
= v
.current_location
625 n_contractdef
.validate
627 var block
= v
.ast_builder
.make_block
628 var n_self
= new ASelfExpr
629 var args
= n_contractdef
.n_signature
.make_parameter_read
(v
.ast_builder
)
630 var callsite
= v
.ast_builder
.create_callsite
(v
.toolcontext
.modelbuilder
, n_contractdef
, mproperty
, true)
631 var n_call
= v
.ast_builder
.make_call
(n_self
, callsite
, args
)
633 if m_signature
.return_mtype
== null then
636 block
.add
(v
.ast_builder
.make_return
(n_call
))
639 n_contractdef
.n_block
= block
640 n_contractdef
.do_all
(v
.toolcontext
)
644 # Entry point to build contract (define the contract facet and define the contract method verification)
645 private fun construct_contract
(v
: ContractsVisitor, n_signature
: ASignature, n_annotation
: AAnnotation, mcontract
: MContract, exist_contract
: Bool)
647 if check_same_contract
(v
, n_annotation
, mcontract
) then return
648 # Check if the contract is necessary
649 if not mcontract
.check_usage
(v
, mclassdef
.mmodule
) then return
650 if not exist_contract
and not is_intro
then no_intro_contract
(v
, n_signature
, mcontract
, n_annotation
)
651 v
.define_signature
(mcontract
, n_signature
, mproperty
.intro
.msignature
)
653 var conditiondef
= v
.build_contract
(n_annotation
, mcontract
, mclassdef
)
654 check_contract_facet
(v
, n_signature
.clone
, mcontract
, exist_contract
)
658 # Create a contract on the introduction classdef of the property.
659 # Display an warning message if necessary
660 private fun no_intro_contract
(v
: ContractsVisitor, n_signature
: ASignature, mcontract
: MContract, n_annotation
: AAnnotation)
662 mcontract
.create_empty_contract
(v
, mcontract
.intro_mclassdef
, mcontract
.adapt_msignature
(self.mproperty
.intro
.msignature
), mcontract
.adapt_nsignature
(n_signature
))
663 mcontract
.no_intro_contract
(v
, n_annotation
)
664 mproperty
.intro
.has_contract
= true
667 # Is the contract already defined in the context
670 # fun foo is expects([...]), expects([...])
672 # Here `check_same_contract` display an error when the second expects is processed
673 private fun check_same_contract
(v
: ContractsVisitor, n_annotation
: AAnnotation ,mcontract
: MContract): Bool
675 if self.mclassdef
.mpropdefs_by_property
.has_key
(mcontract
) then
676 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}")
684 # flag to indicate is the `MPropDef` has a contract
685 var has_contract
= false
689 redef fun check_callsite
(v
)
691 v
.visited_method
= self
695 redef class AMethPropdef
697 # Execute all method verification scope flow and typing.
698 # It also execute an ast validation to define all parents and all locations
699 private fun do_all
(toolcontext
: ToolContext)
702 # FIXME: The `do_` usage it is maybe to much (verification...). Solution: Cut the `do_` methods into simpler parts
703 self.do_scope
(toolcontext
)
704 self.do_flow
(toolcontext
)
705 self.do_typing
(toolcontext
.modelbuilder
)
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
)
713 v
.current_location
= self.location
714 v
.is_intro_contract
= mpropdef
.is_intro
716 if n_annotations
!= null then
717 for n_annotation
in n_annotations
.n_items
do
718 check_annotation
(v
,n_annotation
)
722 if not mpropdef
.is_intro
and not v
.find_no_contract
then
727 v
.find_no_contract
= false
730 # Verification of the annotation to know if it is a contract annotation.
731 # If this is the case, we built the appropriate contract.
732 private fun check_annotation
(v
: ContractsVisitor, n_annotation
: AAnnotation)
734 if n_annotation
.name
== "expects" then
735 var exist_contract
= mpropdef
.mproperty
.check_exist_expect
736 mpropdef
.construct_contract
(v
, self.n_signature
.as(not null), n_annotation
, mpropdef
.mproperty
.mexpect
.as(not null), exist_contract
)
737 else if n_annotation
.name
== "ensures" then
738 var exist_contract
= mpropdef
.mproperty
.check_exist_ensure
739 mpropdef
.construct_contract
(v
, self.n_signature
.as(not null), n_annotation
, mpropdef
.mproperty
.mensure
.as(not null), exist_contract
)
740 else if n_annotation
.name
== "no_contract" then
741 # no_contract found set the flag to true
742 v
.find_no_contract
= true
746 # Verification if the method have an inherited contract to apply it.
747 private fun check_redef
(v
: ContractsVisitor)
749 # Check if the method has an attached contract
750 if not mpropdef
.has_contract
then
751 if mpropdef
.mproperty
.intro
.has_contract
then
752 mpropdef
.has_contract
= true
757 # Adapt the block to use the contracts
758 private fun adapt_block_to_contract
(v
: ContractsVisitor, contract
: MContract, n_mpropdef
: AMethPropdef)
760 contract
.adapt_block_to_contract
(v
, n_mpropdef
)
761 mpropdef
.has_contract
= true
762 n_mpropdef
.do_all
(v
.toolcontext
)
766 redef class MSignature
768 # Adapt signature for a expect condition
769 # Removed the return type is it not necessary
770 private fun adapt_to_condition
: MSignature do return new MSignature(mparameters
.to_a
, null)
772 # Adapt signature for a ensure condition
774 # Create new parameter with the return type
775 private fun adapt_to_ensurecondition
: MSignature
777 var rtype
= return_mtype
778 var msignature
= adapt_to_condition
779 if rtype
!= null then
780 msignature
.mparameters
.add
(new MParameter("result", rtype
, false))
785 # Adapt signature for a expect condition
786 # Removed the return type is it not necessary
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 # Return a copy of self adapted for the expect condition
807 # npropdef it is use to define the parent of the parameters
808 private fun adapt_to_condition
(return_type
: nullable AType): ASignature
810 var adapt_nsignature
= self.clone
811 adapt_nsignature
.n_type
= return_type
812 return adapt_nsignature
815 # Return a copy of self adapted for postcondition on npropdef
816 private fun adapt_to_ensurecondition
: ASignature do
817 var nsignature
= adapt_to_condition
(null)
818 if ret_type
!= null then
821 var new_param
= new AParam
822 new_param
.n_id
= n_id
823 new_param
.variable
= new Variable(n_id
.text
)
824 new_param
.variable
.declared_type
= ret_type
825 nsignature
.n_params
.add new_param
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_method_contract
(actual_callsite
)
842 redef fun check_callsite
(v
)
844 var actual_callsite
= callsite
845 if actual_callsite
!= null then
846 callsite
= v
.drive_method_contract
(actual_callsite
)