Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Collections: Add contract usage #2796

Open
wants to merge 85 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
85 commits
Select commit Hold shift + click to select a range
03d4515
abstract_collection: Add contracts usage
Delja Sep 29, 2019
f6f08c9
collection/array: Add contracts usage
Delja Sep 29, 2019
f7c591d
collection/circular_array: Add contracts usage
Delja Sep 29, 2019
0cda002
collection/hash_collection: Add contracts usage
Delja Sep 29, 2019
8393ae2
collection/list: Add contracts usage
Delja Sep 29, 2019
d603aba
collection/union_find: Add contracts usage
Delja Sep 29, 2019
add16cb
tests: Update tests for collection contract
Delja Oct 3, 2019
202b022
concurrent_collections: Remove contracts
Delja Oct 24, 2019
d394075
pthread/collection: Remove contracts
Delja Oct 24, 2019
ca58d81
model_contract: Add model representation of class invariant
Delja Jul 14, 2020
3b0a52a
model_contract: Improve comment
Delja Jul 14, 2020
a02e442
astbuilder: Use the `is_fictive` flag
Delja Jul 14, 2020
5d919fd
check_annotation: Add `invariant` annotation
Delja Jul 14, 2020
6ee632e
toolcontext: Move the contract options
Delja Jul 14, 2020
8c12fde
contrats: Add `invariant` usage
Delja Jul 14, 2020
3315fab
tests: Add invariant contract tests
Delja Jul 14, 2020
27948de
man/nitc: Update man page
Delja Jul 14, 2020
36113e8
tests: Update annotation syntax test result
Delja Jul 15, 2020
1bbd98d
Merge remote-tracking branch 'origin/contract_refactoring' into old_p…
Delja Jul 27, 2020
dc16cdf
contracts: Add `old` usage
Delja Jul 27, 2020
f98614f
model_contract: Add `old` representation
Delja Jul 27, 2020
5a7c8ef
tests: Add ensure `old` tests
Delja Jul 27, 2020
924813b
tests: Update actual test result
Delja Jul 27, 2020
b85f9b4
abstract_collection: Add first contract
Delja Dec 5, 2019
049e492
collection/range: Fix the infinite loop in the contract of `first`
Delja May 28, 2020
1f88009
abstract_compiler: Add `in_assertion` flag
Delja Jul 29, 2020
35df9d8
naive_interpreter: Change the contract lock mechanism
Delja Jul 29, 2020
64fe967
contracts: Change the assertion lock mechanism
Delja Aug 2, 2020
4375990
tests: Add a test to show contracts in parallel execution
Delja Aug 2, 2020
370aff6
model/model_contract: Fix invariant
Delja Aug 20, 2020
388ac4a
model_contract: Improve comment
Delja Jul 14, 2020
200427c
astbuilder: Use the `is_fictive` flag
Delja Jul 14, 2020
7a3512a
check_annotation: Add `invariant` annotation
Delja Jul 14, 2020
bb19ec4
toolcontext: Move the contract options
Delja Jul 14, 2020
66231ed
contrats: Add `invariant` usage
Delja Jul 14, 2020
658c975
contract: error
Delja Aug 20, 2020
032ec1f
tests: Add invariant contract tests
Delja Jul 14, 2020
6a6c1df
man/nitc: Update man page
Delja Jul 14, 2020
fb61a9c
tests: Update annotation syntax test result
Delja Jul 15, 2020
30c9098
Merge branch 'contract_multy_thread'
Delja Aug 20, 2020
c6ccdfb
Merge branch 'old_post_contract'
Delja Aug 20, 2020
6f2b398
contracts: Add contract invocation counter
Delja Aug 20, 2020
a265057
abstract_compiler: Add contract invocation counter
Delja Aug 20, 2020
31a4483
src/contracts: Fix `null` omit argument error
Delja Aug 14, 2020
9be96a1
tests: Add contract test
Delja Aug 16, 2020
f924d10
Merge branch 'contract_fix_error'
Delja Aug 20, 2020
6e843ca
concurrent_collections: Fix `no_contract` warning
Delja Aug 21, 2020
afa7cda
share/man: Add `--contract-metrics` in man
Delja Aug 21, 2020
848e747
contracts: Remove weaving callsite on AAnnotation
Delja Aug 21, 2020
c15a931
circular_list: Add `[]` implementation
Delja Aug 21, 2020
1fbf342
contracts: Fix error on `=` method signature check
Delja Aug 21, 2020
88b6601
contracts: Improve old class set and get attribut
Delja Aug 22, 2020
c72128e
contracts: Add option to keep old instance
Delja Aug 22, 2020
77ca7ed
contracts: Fix if duplicate object class
Delja Aug 22, 2020
2e1c86d
share/man: Add `--keep-old-instance` option
Delja Aug 22, 2020
24dcd54
contracts: Fix Error
Delja Aug 22, 2020
7790547
model_contract: Add model representation of class invariant
Delja Jul 14, 2020
ba13320
model_contract: Improve comment
Delja Jul 14, 2020
6df2861
astbuilder: Use the `is_fictive` flag
Delja Jul 14, 2020
84d90f0
check_annotation: Add `invariant` annotation
Delja Jul 14, 2020
fff2fa1
toolcontext: Move the contract options
Delja Jul 14, 2020
66425fc
contrats: Add `invariant` usage
Delja Jul 14, 2020
ffde08c
tests: Add invariant contract tests
Delja Jul 14, 2020
c77fb03
man/nitc: Update man page
Delja Jul 14, 2020
dbe708a
tests: Update annotation syntax test result
Delja Jul 15, 2020
c4d491b
model: Replace `assert` by contract
Delja Aug 22, 2020
046565d
abstract_compiler: Add contract
Delja Aug 22, 2020
40e00f8
separate_compiler: Replace `assert` by contract
Delja Aug 22, 2020
47790ec
java_compiler: Replace `assert` by contract
Delja Aug 22, 2020
af813cb
global_compiler: Replace `assert` by contract
Delja Aug 22, 2020
9f63a9a
compiler_fii: Replace `assert` by contract
Delja Aug 22, 2020
266bdd7
compiler/coloring: Replace `assert` by contract
Delja Aug 22, 2020
b01fcf9
tests: Update tests result
Delja Aug 22, 2020
cea6b80
nitcc/grammar: Tmp fix
Delja Aug 22, 2020
8b7aff4
tests: Update test result for invariant attribute
Delja Aug 23, 2020
f09d020
tests/sav: Update test result error_class_glob
Delja Aug 24, 2020
b616453
astbuilder: Add parameter to get correct type
Delja Aug 24, 2020
8dcf67c
contract: Modify callsite creation to give recv type
Delja Aug 24, 2020
0f1b74a
contract: Replace parameter of `is_called` method
Delja Sep 5, 2020
9a63daf
contracts: Add contract options
Delja Aug 24, 2020
0f60e23
contract: Add fast exit for `null` mpropdef
Delja Sep 5, 2020
235530c
man: Add options documentation
Delja Sep 5, 2020
703d32b
Merge branch 'contract_refactoring'
Delja Sep 5, 2020
df5090b
Merge branch 'contract_in_nitc'
Delja Sep 6, 2020
da051de
Merge branch 'master' into collections_contract
Delja Sep 6, 2020
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
contrats: Add invariant usage
Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
  • Loading branch information
Delja committed Aug 20, 2020
commit 66231ed6a11c7e58d70fa674e293683c0064dbdc
234 changes: 233 additions & 1 deletion src/contracts.nit
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ module contracts
import parse_annotations
import phase
import semantize
import mclassdef_collect
intrude import model_contract
intrude import astbuilder
intrude import modelize_property
Expand Down Expand Up @@ -125,6 +126,9 @@ private class ContractsVisitor
# Keep the `in_contract` attribute to avoid searching at each contrat
var in_contract_attribute: nullable MAttribute = null

# Keep the invariant property to avoid searching at each invariant
var global_invariant: nullable MInvariant = null

redef fun visit(node)
do
node.create_contracts(self)
Expand Down Expand Up @@ -185,6 +189,37 @@ private class ContractsVisitor
return in_contract_attribute.as(not null)
end

# Inject the invariant method (`_invariant_`) verification in the root `Object` class
# By default the method is empty.
# Note the method is not abstract because the implementation of this method makes a super call to resolve multiple inheritance problem
private fun inject_invariant_in_object
do
# If the global_invariant already know just return
if global_invariant != null then return
# Get the object class from the modelbuilder
var object_class = toolcontext.modelbuilder.get_mclass_by_name(visited_module, mainmodule, "Object")

# Try to get a global invariant if it's already defined in a previously visited module.
var invariant_property = toolcontext.modelbuilder.try_get_mproperty_by_name(visited_module, object_class.intro, "_invariant_")
if invariant_property != null then
global_invariant = invariant_property.as(MInvariant)
return
end

var m_invariant = new MInvariant(object_class.intro, "_invariant_", object_class.intro.location, public_visibility)
global_invariant = m_invariant

toolcontext.modelbuilder.create_method_from_property(m_invariant, object_class.intro, false, new MSignature(new Array[MParameter]))
end

# Return the invariant property `_invariant_`
# If the `_invariant_` does not exist it's injected this with `inject_invariant_in_object`
private fun get_global_invariant: MInvariant
do
if self.global_invariant == null then inject_invariant_in_object
return global_invariant.as(not null)
end

# Return an `AIfExpr` with the contract encapsulated by an `if` to check if it's already in a contract verification.
#
# Example:
Expand Down Expand Up @@ -254,12 +289,20 @@ private class CallSiteVisitor
private fun drive_callsite_to_contract(callsite: CallSite): CallSite
do
var contract_facet = callsite.mproperty.mcontract_facet
var invariant_facet = callsite.mproperty.minvariant_facet
var visited_mpropdef = visited_propdef.mpropdef

if visited_mpropdef isa MContract or visited_mpropdef isa MFacet then return callsite
if visited_mpropdef == null or contract_facet == null then return callsite

return ast_builder.create_callsite(toolcontext.modelbuilder, visited_propdef, contract_facet, callsite.recv_is_self)
var facet: MFacet
if not callsite.recv_is_self and invariant_facet != null then
facet = invariant_facet
else
facet = contract_facet
end

return ast_builder.create_callsite(toolcontext.modelbuilder, visited_propdef, facet, callsite.recv_is_self)
end
end

Expand Down Expand Up @@ -565,8 +608,189 @@ redef class MEnsure
end
end

redef class MInvariant
super BottomMContract

redef fun adapt_method_to_contract(v: ContractsVisitor, mfacet: MFacet, n_mpropdef: AMethPropdef)
do
var callsite = v.ast_builder.create_callsite(v.toolcontext.modelbuilder, n_mpropdef, self, true)
var n_self = new ASelfExpr
# build the call to the contract method
var n_call = v.ast_builder.make_call(n_self, callsite, null)
var actual_block = n_mpropdef.n_block
# never happen. If it's the case the problem is in the contract facet building
assert actual_block isa ABlockExpr

var new_block = v.ast_builder.make_block

if v.toolcontext.opt_in_out_invariant.value and not n_mpropdef.mpropdef.mproperty.is_init then new_block.add n_call

new_block.n_expr.add_all(actual_block.n_expr)

n_mpropdef.n_block = new_block

var ret_type = n_mpropdef.mpropdef.mproperty.intro.msignature.return_mtype
if ret_type != null then
# Inject the variable result (the injection of the result is necessary even if the invariants cannot take `result` as an argument)
# In this case the result variable is here to keep the return value of the original method.
# exemple
# ~~~nitish
# class A
# fun bar([...]): Bool is invariant([...])
#
# fun _contract_bar([...])
# do
# var result = bar([...])
# # Check if the invariant check call is necessary and execute it.
# [...]
# return result
# end
#
# fun _bar_expect([...])
# end
# ~~~~
var result_var = inject_result(v, n_mpropdef, ret_type)
var return_expr = new_block.n_expr.pop
new_block.add_all([n_call, return_expr])
else
new_block.add(n_call)
end
end
end

redef class MClass

# Build the invariant verification property `_invariant` if is not exist and return it
private fun build_invariant(v: ContractsVisitor): MInvariant
do
var m_invariant = self.minvariant
if m_invariant != null then return m_invariant
# get a invariant property from the `ContractsVisitor`
m_invariant = v.get_global_invariant
self.minvariant = m_invariant
return m_invariant
end
end

redef class MClassDef

# Is there an inherited invariant contract?
private fun has_inherited_invariant: Bool
do
var super_classes = self.in_hierarchy.direct_greaters
for super_class in super_classes do
if super_class.mclass.has_invariant then return true
end
return false
end
end

redef class AClassdef

# Entry point to create a contract (verification of inheritance, or new contract).
redef fun create_contracts(v)
do
v.ast_builder.check_mmodule(mclassdef.mmodule)
v.current_location = self.location
# Invariants are always considered to be a redefinition of contract.
# This is due to an empty invariant method which is added to the root `object` class.
v.is_intro_contract = false
check_annotation(v)
if not mclass.has_invariant then check_redef(v)
end

# Verification if the class has an inherited contract to apply it.
private fun check_redef(v: ContractsVisitor)
do
# Check if the method has an attached contract (Inherited)
if mclassdef.has_inherited_invariant then mclass.minvariant = v.global_invariant
end

# Verification of the annotation to know if it is a contract annotation.
# If this is the case, we built the appropriate contract.
private fun check_annotation(v: ContractsVisitor)
do
var annotation_invariants = get_annotations("invariant")
var annotation_no_contract = get_annotations("no_contract")

if not annotation_invariants.is_empty and not annotation_no_contract.is_empty then
v.toolcontext.error(location, "The new contract definition is not correct when using `no_contract`. Remove the `invariant` definition or the `no_contract`")
return
end

if not annotation_no_contract.is_empty then
var minvariant = mclass.minvariant
if minvariant == null then
v.toolcontext.warning(location, "useless_nocontract", "Useless `no_contract`, no invariant was declared or inherited for `{mclass.name}`. Remove the `no_contract`")
else
# Add an empty invariant method to replace the actual definition
v.toolcontext.modelbuilder.create_method_from_property(minvariant, mclassdef.as(not null), false, minvariant.intro.msignature)
end
return
end

if not annotation_invariants.is_empty then

var minvariant = mclass.build_invariant(v)

v.define_signature(minvariant, null, null)
v.build_contract(annotation_invariants, minvariant, mclassdef.as(not null))

add_invariant_in_super_def(v)
# Construct invariant facet for the `default_init`
mclassdef.default_init.mproperty.define_invariant_facet(v, mclassdef.as(not null), mclass.minvariant.as(not null))
end
end

# Create all contract facet for each inherited property definition of the class to take in consideration the invariant
# Redefine or introduced properties will be processed later
private fun add_invariant_in_super_def(v: ContractsVisitor)
do
var mpropertys = mclassdef.collect_inherited_mmethods(v.mainmodule, new ModelFilter)
for mproperty in mpropertys do
if mproperty isa MFacet or mproperty isa MContract or mproperty.has_invariant_facet then continue

# All property defined in Object is considered as a pure property (without side effect)
# TO-DO add an option to manage it. Take care with `!=` and `==` on MNullableType you can't do a call to invariant facet because the object might be null.
if mproperty.intro.mclassdef.name == "Object" then continue

# Check if the actual class definition redef this property definition. if it's the case do nothing the visit of the method will do the job
if mclassdef.mpropdefs_by_property.has_key(mproperty) then continue

if mproperty.intro.is_intern then continue
# Do not generate invariant facet with inherited `defaultinit`
if not mproperty.name == "defaultinit" then mproperty.define_invariant_facet(v, mclassdef.as(not null), mclass.minvariant.as(not null))
end
end
end

redef class MMethod

# Define invariant facet for the MMethod in the given mclassdef.
# This method also defines the contract facet.
private fun define_invariant_facet(v: ContractsVisitor, classdef: MClassDef, minvariant: MInvariant)
do
# Do nothing the invariant facet already exist
if has_invariant_facet then return

# Make a contract facet if it's not exist
if not self.has_contract_facet then define_contract_facet(v, classdef)

# Make invariant mproperty facet
var invariant_facet = build_invariant_facet

# Check if the MMethod has a invariant facet in the intro_mclassdef
if classdef != intro_mclassdef then
create_facet(v, intro_mclassdef, invariant_facet, self.mcontract_facet.as(not null))
end

# Create an ast definition for the invariant facet
var n_invariant_facet = create_facet(v, classdef, invariant_facet, self.mcontract_facet.as(not null))
minvariant.adapt_method_to_contract(v, invariant_facet, n_invariant_facet)
n_invariant_facet.location = v.current_location
n_invariant_facet.do_all(v.toolcontext)
end

# Define contract facet for MMethod in the given mclassdef. The facet represents the entry point with contracts (expect, ensure) of the method.
# If a contract is given adapt the contract facet.
#
Expand Down Expand Up @@ -726,6 +950,7 @@ redef class AMethPropdef
v.is_intro_contract = mpropdef.is_intro
check_annotation(v)
if not mpropdef.is_intro then check_redef(v)
check_invariant(v)
end

# Verification of the annotation to know if it is a contract annotation.
Expand Down Expand Up @@ -775,6 +1000,13 @@ redef class AMethPropdef
if mensure.is_called(v, mpropdef.as(not null)) then mpropdef.mproperty.define_contract_facet(v, mpropdef.mclassdef, mensure)
end
end

# Check if the class has an invariant to apply it on the property
private fun check_invariant(v: ContractsVisitor)
do
var minvariant = mpropdef.mclassdef.mclass.minvariant
if minvariant != null and not mpropdef.mproperty.has_invariant_facet then mpropdef.mproperty.define_invariant_facet(v, mpropdef.mclassdef, minvariant)
end
end

redef class MSignature
Expand Down