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 astbuilder
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 (expect, ensure).
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 # Visitor to build all contracts.
69 private class ContractsVisitor
72 # Instance of the toolcontext
73 var toolcontext
: ToolContext
76 # It's strore to define if the contract need to be build depending on the selected policy `--no-contract` `--full-contract` or default
77 var mainmodule
: MModule
79 # Actual visited module
80 var visited_module
: AModule
82 var ast_builder
: ASTBuilder
84 # The `ASignature` of the actual build contract
85 var n_signature
: ASignature is noinit
87 # The `MSignature` of the actual build contract
88 var m_signature
: MSignature is noinit
90 # The `current_location` can corresponding of the annotation or method location.
91 var current_location
: Location is noinit
93 # Is the contrat is an introduction or not?
94 # This attribute has the same value as the `is_intro` of the propdef attached to the contract.
95 # 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.
96 var is_intro_contract
: Bool is noinit
98 # Actual visited class
99 var visited_class
: nullable AClassdef
101 # is `no_contract` annotation was found
102 var find_no_contract
= false
104 # The reference to the `in_contract` attribute.
105 # This attribute is used to disable contract verification when you are already in a contract verification.
106 # Keep the `in_contract` attribute to avoid searching at each contrat
107 var in_contract_attribute
: nullable MAttribute = null
109 redef fun visit
(node
)
111 node
.create_contracts
(self)
115 # Method use to define the signature part of the method `ASignature` and `MSignature`
116 # The given `mcontract` provided `adapt_nsignature` and `adapt_msignature` to copy and adapt the given signature (`nsignature` and `msignature`)
117 fun define_signature
(mcontract
: MContract, nsignature
: nullable ASignature, msignature
: nullable MSignature)
119 if nsignature
!= null and msignature
!= null then nsignature
.ret_type
= msignature
.return_mtype
120 self.n_signature
= mcontract
.adapt_nsignature
(nsignature
)
121 self.m_signature
= mcontract
.adapt_msignature
(msignature
)
124 # Define the new contract take in consideration that an old contract exist or not
125 private fun build_contract
(n_annotation
: AAnnotation, mcontract
: MContract, mclassdef
: MClassDef): MMethodDef
127 self.current_location
= n_annotation
.location
128 # Retrieving the expression provided in the annotation
129 var n_condition
= n_annotation
.construct_condition
(self)
130 var m_contractdef
: AMethPropdef
131 if is_intro_contract
then
132 # Create new contract method
133 m_contractdef
= mcontract
.create_intro_contract
(self, n_condition
, mclassdef
)
135 # Create a redef of contract to take in consideration the new condition
136 m_contractdef
= mcontract
.create_subcontract
(self, n_condition
, mclassdef
)
138 var contract_propdef
= m_contractdef
.mpropdef
139 # The contract has a null mpropdef, this should never happen
140 assert contract_propdef
!= null
141 return contract_propdef
144 # Verification if the construction of the contract is necessary.
145 # Three cases are checked for `expect`:
147 # - Was the `--full-contract` option passed?
148 # - Is the method is in the main package?
149 # - Is the method is in a direct imported package?
151 fun check_usage_expect
(actual_mmodule
: MModule): Bool
153 var main_package
= mainmodule
.mpackage
154 var actual_package
= actual_mmodule
.mpackage
155 if main_package
!= null and actual_package
!= null then
156 var condition_direct_arc
= toolcontext
.modelbuilder
.model
.mpackage_importation_graph
.has_arc
(main_package
, actual_package
)
157 return toolcontext
.opt_full_contract
.value
or condition_direct_arc
or main_package
== actual_package
162 # Verification if the construction of the contract is necessary.
163 # Two cases are checked for `ensure`:
165 # - Was the `--full-contract` option passed?
166 # - Is the method is in the main package?
168 fun check_usage_ensure
(actual_mmodule
: MModule): Bool
170 return toolcontext
.opt_full_contract
.value
or mainmodule
.mpackage
== actual_mmodule
.mpackage
173 # Inject the incontract attribute (`_in_contract_`) in the `Sys` class
174 # This attribute allows to check if the contract need to be executed
175 private fun inject_incontract_in_sys
177 # If the `in_contract_attribute` already know just return
178 if in_contract_attribute
!= null then return
180 var sys_class
= toolcontext
.modelbuilder
.get_mclass_by_name
(visited_module
, mainmodule
, "Sys")
182 # Try to get the `in_contract` property, if it has already defined in a previously visited module.
183 var in_contract_property
= toolcontext
.modelbuilder
.try_get_mproperty_by_name
(visited_module
, sys_class
.intro
, "__in_contract_")
184 if in_contract_property
!= null then
185 self.in_contract_attribute
= in_contract_property
.as(MAttribute)
189 var bool_false
= new AFalseExpr.make
(mainmodule
.bool_type
)
190 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
)
192 in_contract_attribute
= n_in_contract_attribute
.mpropdef
.mproperty
195 # Return the `_in_contract_` attribute.
196 # If the attribute `_in_contract_` does not exist it's injected with `inject_incontract_in_sys`
197 private fun get_incontract
: MAttribute
199 if self.in_contract_attribute
== null then inject_incontract_in_sys
200 return in_contract_attribute
.as(not null)
203 # Return an `AIfExpr` with the contract encapsulated by an `if` to check if it's already in a contract verification.
208 # fun bar([...]) is except([...])
210 # fun _contract_bar([...])
212 # if not sys._in_contract_ then
213 # sys._in_contract_ = true
215 # sys._in_contract_ = false
220 # fun _bar_expect([...])
224 private fun encapsulated_contract_call
(visited_method
: AMethPropdef, call_to_contracts
: Array[ACallExpr]): AIfExpr
226 var sys_property
= toolcontext
.modelbuilder
.model
.get_mproperties_by_name
("sys").first
.as(MMethod)
227 var callsite_sys
= ast_builder
.create_callsite
(toolcontext
.modelbuilder
, visited_method
, sys_property
, true)
229 var incontract_attribute
= get_incontract
231 var callsite_get_incontract
= ast_builder
.create_callsite
(toolcontext
.modelbuilder
, visited_method
, incontract_attribute
.getter
.as(MMethod), false)
232 var callsite_set_incontract
= ast_builder
.create_callsite
(toolcontext
.modelbuilder
, visited_method
, incontract_attribute
.setter
.as(MMethod), false)
234 var n_condition
= ast_builder
.make_not
(ast_builder
.make_call
(ast_builder
.make_call
(new ASelfExpr, callsite_sys
, null), callsite_get_incontract
, null))
236 var n_if
= ast_builder
.make_if
(n_condition
, null)
238 var if_then_block
= n_if
.n_then
.as(ABlockExpr)
240 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
)]))
241 if_then_block
.add_all
(call_to_contracts
)
242 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
)]))
248 # This visitor checks the `callsite` to see if the target `mpropdef` has a contract.
249 private class CallSiteVisitor
253 # Instance of the toolcontext
254 var toolcontext
: ToolContext
256 # Actual visited method
257 var visited_method
: APropdef is noinit
259 redef fun visit
(node
)
261 node
.check_callsite
(self)
265 # Check if the callsite calls a method with a contract.
266 # If it's the case the callsite is replaced by another callsite to the contract method.
267 private fun drive_method_contract
(callsite
: CallSite): CallSite
269 if callsite
.mproperty
.mcontract_facet
!= null then
270 var contract_facet
= callsite
.mproperty
.mcontract_facet
271 var visited_mpropdef
= visited_method
.mpropdef
272 assert contract_facet
!= null and visited_mpropdef
!= null
274 var type_visitor
= new TypeVisitor(toolcontext
.modelbuilder
, visited_mpropdef
)
275 var drived_callsite
= type_visitor
.build_callsite_by_property
(visited_method
, callsite
.recv
, contract_facet
, callsite
.recv_is_self
)
276 # This never happen this check is here for debug
277 assert drived_callsite
!= null
278 return drived_callsite
285 private fun create_contracts
(v
: ContractsVisitor) do end
286 private fun check_callsite
(v
: CallSiteVisitor) do end
289 redef class AAnnotation
291 # Returns the conditions of annotation parameters. If there are several parameters, the result is an `AAndExpr`
293 # the contract `ensure(true, i == 10, f >= 1.0)`
294 # return this condition `(true and i == 10 and f >= 1.0)`
295 private fun construct_condition
(v
: ContractsVisitor): AExpr
297 var n_condition
= n_args
.first
299 for n_arg
in n_args
do n_condition
= v
.ast_builder
.make_and
(n_condition
, n_arg
)
304 # The root of all contracts
306 # The objective of this class is to provide the set
307 # of services must be implemented or provided by a contract
308 abstract class MContract
311 # Define the name of the contract
312 fun contract_name
: String is abstract
314 # Method use to diplay warning when the contract is not present at the introduction
315 private fun no_intro_contract
(v
: ContractsVisitor, a
: AAnnotation)do end
317 # Creating specific inheritance block contract
318 private fun create_nblock
(v
: ContractsVisitor, n_condition
: AExpr, args
: Array[AExpr]): ABlockExpr is abstract
320 # Method to adapt the `n_mpropdef.n_block` to the contract
321 private fun adapt_block_to_contract
(v
: ContractsVisitor, n_mpropdef
: AMethPropdef) is abstract
323 # Adapt the msignature specifically for the contract method
324 private fun adapt_specific_msignature
(m_signature
: MSignature): MSignature do return m_signature
.adapt_to_contract
326 # Adapt the nsignature specifically for the contract method
327 private fun adapt_specific_nsignature
(n_signature
: ASignature): ASignature do return n_signature
.adapt_to_contract
329 # Adapt the `m_signature` to the contract
330 # If it is not null call the specific adapt `m_signature` for the contract
331 private fun adapt_msignature
(m_signature
: nullable MSignature): MSignature
333 if m_signature
== null then return new MSignature(new Array[MParameter])
334 return adapt_specific_msignature
(m_signature
)
337 # Adapt the `n_signature` to the contract
338 # If it is not null call the specific adapt `n_signature` for the contract
339 private fun adapt_nsignature
(n_signature
: nullable ASignature): ASignature
341 if n_signature
== null then return new ASignature
342 return adapt_specific_nsignature
(n_signature
)
345 # Create a new empty contract
346 private fun create_empty_contract
(v
: ContractsVisitor, mclassdef
: MClassDef, msignature
: nullable MSignature, n_signature
: ASignature)
348 var n_contract_def
= intro_mclassdef
.mclass
.create_empty_method
(v
, self, mclassdef
, msignature
, n_signature
)
349 n_contract_def
.do_all
(v
.toolcontext
)
352 # Create the initial contract (intro)
353 # All contracts have the same implementation for the introduction.
359 # assert contract_condition
363 private fun create_intro_contract
(v
: ContractsVisitor, n_condition
: nullable AExpr, mclassdef
: MClassDef): AMethPropdef
365 var n_block
= v
.ast_builder
.make_block
366 if n_condition
!= null then
367 # Create a new tid to set the name of the assert for more explicit error
368 var tid
= new TId.init_tk
(self.location
)
369 tid
.text
= "{self.contract_name}"
370 n_block
.add v
.ast_builder
.make_assert
(tid
, n_condition
, null)
372 return make_contract
(v
, n_block
, mclassdef
)
375 # Create a contract with old (super) and the new conditions
376 private fun create_subcontract
(v
: ContractsVisitor, ncondition
: nullable AExpr, mclassdef
: MClassDef): AMethPropdef
378 var args
= v
.n_signature
.make_parameter_read
(v
.ast_builder
)
379 var n_block
= v
.ast_builder
.make_block
380 if ncondition
!= null then n_block
= self.create_nblock
(v
, ncondition
, args
)
381 return make_contract
(v
, n_block
, mclassdef
)
384 # Build a method with a specific block `n_block` in a specified `mclassdef`
385 private fun make_contract
(v
: ContractsVisitor, n_block
: AExpr, mclassdef
: MClassDef): AMethPropdef
387 var n_contractdef
= intro_mclassdef
.mclass
.create_empty_method
(v
, self, mclassdef
, v
.m_signature
, v
.n_signature
)
388 n_contractdef
.n_block
= n_block
389 # Define the location of the new method for corresponding of the annotation location
390 n_contractdef
.location
= v
.current_location
391 n_contractdef
.do_all
(v
.toolcontext
)
396 # A expect (precondition) contract representation
397 # This method check if the requirements of the called method is true.
401 # Define the name of the contract
402 redef fun contract_name
: String do return "expect"
404 # Display warning if no contract is defined at introduction `expect`,
405 # because if no contract is defined at the introduction the added
406 # contracts will not cause any error even if they are not satisfied.
412 # fun _bar_expect([...])
419 # redef fun bar is expect(contract_condition)
420 # redef fun _bar_expect([...])
422 # if (contract_condition) then return
428 redef fun no_intro_contract
(v
: ContractsVisitor, a
: AAnnotation)
430 v
.toolcontext
.warning
(a
.location
,"","Useless contract: No contract defined at the introduction of the method")
433 redef fun create_nblock
(v
: ContractsVisitor, n_condition
: AExpr, args
: Array[AExpr]): ABlockExpr
435 # Creating the if expression with the new condition
436 var if_block
= v
.ast_builder
.make_if
(n_condition
, n_condition
.mtype
)
437 # Creating and adding return expr to the then case
438 if_block
.n_then
= v
.ast_builder
.make_return
(null)
439 # Creating the super call to the contract and adding this to else case
440 if_block
.n_else
= v
.ast_builder
.make_super_call
(args
,null)
441 var n_block
= v
.ast_builder
.make_block
446 redef fun adapt_block_to_contract
(v
: ContractsVisitor, n_mpropdef
: AMethPropdef)
448 var callsite
= v
.ast_builder
.create_callsite
(v
.toolcontext
.modelbuilder
, n_mpropdef
, self, true)
449 var n_self
= new ASelfExpr
450 var args
= n_mpropdef
.n_signature
.make_parameter_read
(v
.ast_builder
)
451 var n_callexpect
= v
.ast_builder
.make_call
(n_self
,callsite
,args
)
452 # Creation of the new instruction block with the call to expect condition
453 var actual_expr
= n_mpropdef
.n_block
454 var new_block
= new ABlockExpr
455 new_block
.n_expr
.push n_callexpect
456 if actual_expr
isa ABlockExpr then
457 new_block
.n_expr
.add_all
(actual_expr
.n_expr
)
458 else if actual_expr
!= null then
459 new_block
.n_expr
.push
(actual_expr
)
461 n_mpropdef
.n_block
= new_block
465 # The root of all contracts where the call is after the execution of the original method (`invariant` and `ensure`).
466 abstract class BottomMContract
469 redef fun create_nblock
(v
: ContractsVisitor, n_condition
: AExpr, args
: Array[AExpr]): ABlockExpr
471 var tid
= new TId.init_tk
(v
.current_location
)
472 tid
.text
= "{contract_name}"
473 # Creating the assert expression with the new condition
474 var assert_block
= v
.ast_builder
.make_assert
(tid
,n_condition
,null)
475 # Creating the super call to the contract
476 var super_call
= v
.ast_builder
.make_super_call
(args
,null)
477 # Define contract block
478 var n_block
= v
.ast_builder
.make_block
479 # Adding the expressions to the block
480 n_block
.add super_call
481 n_block
.add assert_block
485 # Inject the `result` variable into the `n_block` of the given n_mpropdef`.
487 # The purpose of the variable is to capture return values to use it in contracts.
488 private fun inject_result
(v
: ContractsVisitor, n_mpropdef
: AMethPropdef, ret_type
: MType): Variable
490 var actual_block
= n_mpropdef
.n_block
491 # never happen. If it's the case the problem is in the contract facet building
492 assert actual_block
isa ABlockExpr
494 var return_var
: nullable Variable = null
496 var return_expr
= actual_block
.n_expr
.last
.as(AReturnExpr)
498 var returned_expr
= return_expr
.n_expr
499 # The return node has no returned expression
500 assert returned_expr
!= null
502 # Check if the result variable already exit
503 if returned_expr
isa AVarExpr then
504 if returned_expr
.variable
.name
== "result" then
505 return_var
= returned_expr
.variable
509 return_var
= new Variable("result")
510 # Creating a new variable to keep the old return of the method
511 var assign_result
= v
.ast_builder
.make_var_assign
(return_var
, returned_expr
)
512 # Remove the actual return
513 actual_block
.n_expr
.pop
514 # Set the return type
515 return_var
.declared_type
= ret_type
516 # Adding the reading expr of result variable to the block
517 actual_block
.add assign_result
518 # Expr to read the result variable
519 var read_result
= v
.ast_builder
.make_var_read
(return_var
, ret_type
)
520 # Definition of the new return
521 return_expr
= v
.ast_builder
.make_return
(read_result
)
522 actual_block
.add return_expr
527 # A ensure (postcondition) representation
528 # This method check if the called method respects the expectations of the caller.
530 super BottomMContract
532 # Define the name of the contract
533 redef fun contract_name
: String do return "ensure"
535 redef fun adapt_specific_msignature
(m_signature
: MSignature): MSignature
537 return m_signature
.adapt_to_ensurecondition
540 redef fun adapt_specific_nsignature
(n_signature
: ASignature): ASignature
542 return n_signature
.adapt_to_ensurecondition
545 redef fun adapt_block_to_contract
(v
: ContractsVisitor, n_mpropdef
: AMethPropdef)
547 var callsite
= v
.ast_builder
.create_callsite
(v
.toolcontext
.modelbuilder
, n_mpropdef
, self, true)
548 var n_self
= new ASelfExpr
549 # argument to call the contract method
550 var args
= n_mpropdef
.n_signature
.make_parameter_read
(v
.ast_builder
)
551 # Inject the variable result
552 # The cast is always safe because the online adapted method is the contract facet
554 var actual_block
= n_mpropdef
.n_block
555 # never happen. If it's the case the problem is in the contract facet building
556 assert actual_block
isa ABlockExpr
558 var ret_type
= n_mpropdef
.mpropdef
.mproperty
.intro
.msignature
.return_mtype
559 if ret_type
!= null then
560 var result_var
= inject_result
(v
, n_mpropdef
, ret_type
)
561 # Expr to read the result variable
562 var read_result
= v
.ast_builder
.make_var_read
(result_var
, ret_type
)
563 var return_expr
= actual_block
.n_expr
.pop
564 # Adding the read return to argument
565 args
.add
(read_result
)
566 var n_callcontract
= v
.ast_builder
.make_call
(n_self
,callsite
,args
)
567 actual_block
.add_all
([n_callcontract
,return_expr
])
569 # build the call to the contract method
570 var n_callcontract
= v
.ast_builder
.make_call
(n_self
,callsite
,args
)
571 actual_block
.add n_callcontract
578 # This method create an abstract method representation with this MMethodDef an this AMethoddef
579 private fun create_abstract_method
(v
: ContractsVisitor, mproperty
: MMethod, mclassdef
: MClassDef, msignature
: nullable MSignature, n_signature
: ASignature): AMethPropdef
581 # new methoddef definition
582 var m_def
= new MMethodDef(mclassdef
, mproperty
, v
.current_location
)
584 if msignature
!= null then m_def
.msignature
= msignature
.clone
585 # set the abstract flag
586 m_def
.is_abstract
= true
587 # Build the new node method
588 var n_def
= v
.ast_builder
.make_method
(null,null,m_def
,n_signature
,null,null,null,null)
589 # Define the location of the new method for corresponding of the actual method
590 n_def
.location
= v
.current_location
591 # Association new npropdef to mpropdef
592 v
.toolcontext
.modelbuilder
.unsafe_add_mpropdef2npropdef
(m_def
,n_def
)
596 # Create method with an empty block
597 # 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
598 private fun create_empty_method
(v
: ContractsVisitor, mproperty
: MMethod, mclassdef
: MClassDef, msignature
: nullable MSignature, n_signature
: ASignature): AMethPropdef
600 var n_def
= create_abstract_method
(v
, mproperty
, mclassdef
, msignature
, n_signature
)
601 n_def
.mpropdef
.is_abstract
= false
602 n_def
.n_block
= v
.ast_builder
.make_block
609 # The contract facet of the method
610 # it's representing the method with contract
611 # This method call the contract and the method
612 var mcontract_facet
: nullable MMethod = null
614 # The expected contract method
615 var mexpect
: nullable MExpect = null
617 # The ensure contract method
618 var mensure
: nullable MEnsure = null
620 # Check if the MMethod has no ensure contract
621 # if this is the case returns false and built it
623 private fun check_exist_ensure
: Bool
625 if self.mensure
!= null then return true
626 # build a new `MEnsure` contract
627 self.mensure
= new MEnsure(intro_mclassdef
, "_ensure_{name}", intro_mclassdef
.location
, public_visibility
)
631 # Check if the MMethod has no expect contract
632 # if this is the case returns false and built it
634 private fun check_exist_expect
: Bool
636 if self.mexpect
!= null then return true
637 # build a new `MExpect` contract
638 self.mexpect
= new MExpect(intro_mclassdef
, "_expect_{name}", intro_mclassdef
.location
, public_visibility
)
642 # Check if the MMethod has an contract facet
643 # If the method has no contract facet she create it
644 private fun check_exist_contract_facet
(mpropdef
: MMethodDef): Bool
646 if self.mcontract_facet
!= null then return true
647 # build a new `MMethod` contract
648 self.mcontract_facet
= new MMethod(intro_mclassdef
, "_contract_{name}", intro_mclassdef
.location
, public_visibility
)
653 redef class MMethodDef
655 # Verification of the contract facet
656 # Check if a contract facet already exists to use it again or if it is necessary to create it.
657 private fun check_contract_facet
(v
: ContractsVisitor, n_signature
: ASignature, classdef
: MClassDef, mcontract
: MContract, exist_contract
: Bool)
659 var exist_contract_facet
= mproperty
.check_exist_contract_facet
(self)
660 if exist_contract_facet
and exist_contract
then return
662 var contract_facet
: AMethPropdef
663 if not exist_contract_facet
then
664 # If has no contract facet in intro just create it
665 if classdef
!= mproperty
.intro_mclassdef
then create_contract_facet
(v
, mproperty
.intro_mclassdef
, n_signature
)
666 # If has no contract facet just create it
667 contract_facet
= create_contract_facet
(v
, classdef
, n_signature
)
669 # Check if the contract facet already exist in this context (in this classdef)
670 if classdef
.mpropdefs_by_property
.has_key
(mproperty
.mcontract_facet
) then
672 contract_facet
= v
.toolcontext
.modelbuilder
.mpropdef2node
(classdef
.mpropdefs_by_property
[mproperty
.mcontract_facet
]).as(AMethPropdef)
674 # create a new contract facet definition
675 contract_facet
= create_contract_facet
(v
, classdef
, n_signature
)
676 var block
= v
.ast_builder
.make_block
677 # super call to the contract facet
678 var n_super_call
= v
.ast_builder
.make_super_call
(n_signature
.make_parameter_read
(v
.ast_builder
), null)
679 # verification for add a return or not
680 if contract_facet
.mpropdef
.msignature
.return_mtype
!= null then
681 block
.add
(v
.ast_builder
.make_return
(n_super_call
))
683 block
.add
(n_super_call
)
685 contract_facet
.n_block
= block
688 contract_facet
.adapt_block_to_contract
(v
, mcontract
, contract_facet
)
689 contract_facet
.location
= v
.current_location
690 contract_facet
.do_all
(v
.toolcontext
)
693 # Method to create a contract facet of the method
694 private fun create_contract_facet
(v
: ContractsVisitor, classdef
: MClassDef, n_signature
: ASignature): AMethPropdef
696 var contract_facet
= mproperty
.mcontract_facet
697 assert contract_facet
!= null
698 # Defines the contract phase is an init or not
699 # it is necessary to use the contracts on constructor
700 contract_facet
.is_init
= self.mproperty
.is_init
702 # check if the method has an `msignature` to copy it.
703 var m_signature
: nullable MSignature = null
704 if mproperty
.intro
.msignature
!= null then m_signature
= mproperty
.intro
.msignature
.clone
706 var n_contractdef
= classdef
.mclass
.create_empty_method
(v
, contract_facet
, classdef
, m_signature
, n_signature
)
707 # FIXME set the location because the callsite creation need the node location
708 n_contractdef
.location
= v
.current_location
709 n_contractdef
.validate
711 var block
= v
.ast_builder
.make_block
712 var n_self
= new ASelfExpr
713 var args
= n_contractdef
.n_signature
.make_parameter_read
(v
.ast_builder
)
714 var callsite
= v
.ast_builder
.create_callsite
(v
.toolcontext
.modelbuilder
, n_contractdef
, mproperty
, true)
715 var n_call
= v
.ast_builder
.make_call
(n_self
, callsite
, args
)
717 if m_signature
.return_mtype
== null then
720 block
.add
(v
.ast_builder
.make_return
(n_call
))
723 n_contractdef
.n_block
= block
724 n_contractdef
.do_all
(v
.toolcontext
)
728 # Entry point to build contract (define the contract facet and define the contract method verification)
729 private fun construct_contract
(v
: ContractsVisitor, n_signature
: ASignature, n_annotation
: AAnnotation, mcontract
: MContract, exist_contract
: Bool)
731 if check_same_contract
(v
, n_annotation
, mcontract
) then return
732 if not exist_contract
and not is_intro
then no_intro_contract
(v
, n_signature
, mcontract
, n_annotation
)
733 v
.define_signature
(mcontract
, n_signature
, mproperty
.intro
.msignature
)
735 var conditiondef
= v
.build_contract
(n_annotation
, mcontract
, mclassdef
)
736 check_contract_facet
(v
, n_signature
.clone
, mclassdef
, mcontract
, exist_contract
)
740 # Create a contract on the introduction classdef of the property.
741 # Display an warning message if necessary
742 private fun no_intro_contract
(v
: ContractsVisitor, n_signature
: ASignature, mcontract
: MContract, n_annotation
: AAnnotation)
744 mcontract
.create_empty_contract
(v
, mcontract
.intro_mclassdef
, mcontract
.adapt_msignature
(self.mproperty
.intro
.msignature
), mcontract
.adapt_nsignature
(n_signature
))
745 mcontract
.no_intro_contract
(v
, n_annotation
)
746 mproperty
.intro
.has_contract
= true
749 # Is the contract already defined in the context
752 # fun foo is expect([...]), expect([...])
754 # Here `check_same_contract` display an error when the second expect is processed
755 private fun check_same_contract
(v
: ContractsVisitor, n_annotation
: AAnnotation ,mcontract
: MContract): Bool
757 if self.mclassdef
.mpropdefs_by_property
.has_key
(mcontract
) then
758 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}")
766 # flag to indicate is the `MPropDef` has a contract
767 var has_contract
= false
771 redef fun check_callsite
(v
)
773 v
.visited_method
= self
777 redef class AMethPropdef
779 # Entry point to create a contract (verification of inheritance, or new contract).
780 redef fun create_contracts
(v
)
782 v
.ast_builder
.check_mmodule
(mpropdef
.mclassdef
.mmodule
)
784 v
.current_location
= self.location
785 v
.is_intro_contract
= mpropdef
.is_intro
787 if n_annotations
!= null then
788 for n_annotation
in n_annotations
.n_items
do
789 check_annotation
(v
,n_annotation
)
793 if not mpropdef
.is_intro
and not v
.find_no_contract
then
798 v
.find_no_contract
= false
801 # Verification of the annotation to know if it is a contract annotation.
802 # If this is the case, we built the appropriate contract.
803 private fun check_annotation
(v
: ContractsVisitor, n_annotation
: AAnnotation)
805 if n_annotation
.name
== "expect" then
806 if not v
.check_usage_expect
(mpropdef
.mclassdef
.mmodule
) then return
807 var exist_contract
= mpropdef
.mproperty
.check_exist_expect
808 mpropdef
.construct_contract
(v
, self.n_signature
.as(not null), n_annotation
, mpropdef
.mproperty
.mexpect
.as(not null), exist_contract
)
809 else if n_annotation
.name
== "ensure" then
810 if not v
.check_usage_ensure
(mpropdef
.mclassdef
.mmodule
) then return
811 var exist_contract
= mpropdef
.mproperty
.check_exist_ensure
812 mpropdef
.construct_contract
(v
, self.n_signature
.as(not null), n_annotation
, mpropdef
.mproperty
.mensure
.as(not null), exist_contract
)
813 else if n_annotation
.name
== "no_contract" then
814 # no_contract found set the flag to true
815 v
.find_no_contract
= true
819 # Verification if the method have an inherited contract to apply it.
820 private fun check_redef
(v
: ContractsVisitor)
822 # Check if the method has an attached contract
823 if not mpropdef
.has_contract
then
824 if mpropdef
.mproperty
.intro
.has_contract
then
825 mpropdef
.has_contract
= true
830 # Adapt the block to use the contracts
831 private fun adapt_block_to_contract
(v
: ContractsVisitor, contract
: MContract, n_mpropdef
: AMethPropdef)
833 contract
.adapt_block_to_contract
(v
, n_mpropdef
)
834 mpropdef
.has_contract
= true
835 n_mpropdef
.do_all
(v
.toolcontext
)
839 redef class MSignature
841 # Adapt signature for an contract
843 # The returned `MSignature` is the copy of `self` without return type.
844 private fun adapt_to_contract
: MSignature do return new MSignature(mparameters
.to_a
, null)
846 # Adapt signature for a ensure contract
848 # The returned `MSignature` is the copy of `self` without return type.
849 # The return type is replaced by a new parameter `result`
850 private fun adapt_to_ensurecondition
: MSignature
852 var rtype
= return_mtype
853 var msignature
= adapt_to_contract
854 if rtype
!= null then
855 msignature
.mparameters
.add
(new MParameter("result", rtype
, false))
860 # The returned `MSignature` is the exact copy of `self`.
861 private fun clone
: MSignature do return new MSignature(mparameters
.to_a
, return_mtype
)
864 redef class ASignature
866 # Create an array of AVarExpr representing the read of every parameters
867 private fun make_parameter_read
(ast_builder
: ASTBuilder): Array[AVarExpr]
869 var args
= new Array[AVarExpr]
870 for n_param
in self.n_params
do
871 var mtype
= n_param
.variable
.declared_type
872 var variable
= n_param
.variable
873 if variable
!= null and mtype
!= null then
874 args
.push ast_builder
.make_var_read
(variable
, mtype
)
880 # Create a new ASignature adapted for contract
882 # The returned `ASignature` is the copy of `self` without return type.
883 private fun adapt_to_contract
: ASignature
885 var adapt_nsignature
= self.clone
886 if adapt_nsignature
.n_type
!= null then adapt_nsignature
.n_type
.detach
887 return adapt_nsignature
890 # Create a new ASignature adapted for ensure
892 # The returned `ASignature` is the copy of `self` without return type.
893 # The return type is replaced by a new parameter `result`
894 private fun adapt_to_ensurecondition
: ASignature do
895 var nsignature
= adapt_to_contract
896 if ret_type
!= null then
897 var variable
= new Variable("result")
898 variable
.declared_type
= ret_type
899 nsignature
.n_params
.add
new AParam.make
(variable
, ret_type
.create_ast_representation
)
905 redef class ASendExpr
906 redef fun check_callsite
(v
)
908 var actual_callsite
= callsite
909 if actual_callsite
!= null then
910 callsite
= v
.drive_method_contract
(actual_callsite
)
916 redef fun check_callsite
(v
)
918 var actual_callsite
= callsite
919 if actual_callsite
!= null then
920 callsite
= v
.drive_method_contract
(actual_callsite
)