diff --git a/src/compiler/abstract_compiler.nit b/src/compiler/abstract_compiler.nit index e10be397b8..f31f7e9a27 100644 --- a/src/compiler/abstract_compiler.nit +++ b/src/compiler/abstract_compiler.nit @@ -803,6 +803,9 @@ abstract class AbstractCompiler self.header.add_decl("extern int glob_argc;") self.header.add_decl("extern char **glob_argv;") self.header.add_decl("extern val *glob_sys;") + + # Global fonction used by the contract infrastructure + self.header.add_decl("extern int *getInAssertion(); // Used to know if we are currently checking some assertions.") end # Stack stocking environment for longjumps @@ -942,6 +945,28 @@ extern void nitni_global_ref_decr( struct nitni_ref *ref ); } return data; } + + static pthread_key_t in_assertion_key; + static pthread_once_t in_assertion_key_created = PTHREAD_ONCE_INIT; + + static void create_in_assertion() + { + pthread_key_create(&in_assertion_key, NULL); + } + + //Flag used to know if we are currently checking some assertions. + int *getInAssertion() + { + pthread_once(&in_assertion_key_created, &create_in_assertion); + int* in_assertion = pthread_getspecific(in_assertion_key); + if (in_assertion == NULL) { + in_assertion = malloc(sizeof(int)); + *in_assertion = 0; + pthread_setspecific(in_assertion_key, in_assertion); + } + return in_assertion; + } + #else // Use __thread when available __thread struct catch_stack_t catchStack = {-1, 0, NULL}; @@ -950,6 +975,12 @@ extern void nitni_global_ref_decr( struct nitni_ref *ref ); { return &catchStack; } + + __thread int in_assertion = 0; // Flag used to know if we are currently checking some assertions. + + int *getInAssertion(){ + return &in_assertion; + } #endif """ @@ -3858,6 +3889,18 @@ redef class AIfExpr end end +redef class AIfInAssertion + + redef fun stmt(v) + do + v.add("if (!*getInAssertion())\{") + v.add("*getInAssertion() = 1;") + v.stmt(self.n_body) + v.add("*getInAssertion() = 0;") + v.add("\}") + end +end + redef class AIfexprExpr redef fun expr(v) do diff --git a/src/contracts.nit b/src/contracts.nit index f7b81faf56..28c0bc65ca 100644 --- a/src/contracts.nit +++ b/src/contracts.nit @@ -105,11 +105,6 @@ private class ContractsVisitor # is `no_contract` annotation was found var find_no_contract = false - # The reference to the `in_contract` attribute. - # This attribute is used to disable contract verification when you are already in a contract verification. - # Keep the `in_contract` attribute to avoid searching at each contrat - var in_contract_attribute: nullable MAttribute = null - redef fun visit(node) do node.create_contracts(self) @@ -140,78 +135,12 @@ private class ContractsVisitor end end - # Inject the incontract attribute (`_in_contract_`) in the `Sys` class - # This attribute allows to check if the contract need to be executed - private fun inject_incontract_in_sys - do - # If the `in_contract_attribute` already know just return - if in_contract_attribute != null then return - - var sys_class = toolcontext.modelbuilder.get_mclass_by_name(visited_module, mainmodule, "Sys") - - # Try to get the `in_contract` property, if it has already defined in a previously visited module. - var in_contract_property = toolcontext.modelbuilder.try_get_mproperty_by_name(visited_module, sys_class.intro, "__in_contract_") - if in_contract_property != null then - self.in_contract_attribute = in_contract_property.as(MAttribute) - return - end - - var bool_false = new AFalseExpr.make(mainmodule.bool_type) - 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) - - in_contract_attribute = n_in_contract_attribute.mpropdef.mproperty - end - - # Return the `_in_contract_` attribute. - # If the attribute `_in_contract_` does not exist it's injected with `inject_incontract_in_sys` - private fun get_incontract: MAttribute - do - if self.in_contract_attribute == null then inject_incontract_in_sys - return in_contract_attribute.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: - # ~~~nitish - # class A - # fun bar([...]) is except([...]) - # - # fun _contract_bar([...]) - # do - # if not sys._in_contract_ then - # sys._in_contract_ = true - # _bar_expect([...]) - # sys._in_contract_ = false - # end - # bar([...]) - # end - # - # fun _bar_expect([...]) - # end - # ~~~~ - # - private fun encapsulated_contract_call(visited_method: AMethPropdef, call_to_contracts: Array[ACallExpr]): AIfExpr + # Return an `AIfAssertion` with the contract encapsulated by an `if` to check if it's already in a contract verification. + private fun encapsulated_contract_call(visited_method: AMethPropdef, call_to_contracts: Array[ACallExpr]): AIfInAssertion do - var sys_property = toolcontext.modelbuilder.model.get_mproperties_by_name("sys").first.as(MMethod) - var callsite_sys = ast_builder.create_callsite(toolcontext.modelbuilder, visited_method, sys_property, true) - - var incontract_attribute = get_incontract - - var callsite_get_incontract = ast_builder.create_callsite(toolcontext.modelbuilder, visited_method, incontract_attribute.getter.as(MMethod), false) - var callsite_set_incontract = ast_builder.create_callsite(toolcontext.modelbuilder, visited_method, incontract_attribute.setter.as(MMethod), false) - - var n_condition = ast_builder.make_not(ast_builder.make_call(ast_builder.make_call(new ASelfExpr, callsite_sys, null), callsite_get_incontract, null)) - - var n_if = ast_builder.make_if(n_condition, null) - - var if_then_block = n_if.n_then.as(ABlockExpr) - - 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)])) - if_then_block.add_all(call_to_contracts) - 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)])) - - return n_if + var n_block = ast_builder.make_block + n_block.add_all(call_to_contracts) + return new AIfInAssertion(n_block) end end @@ -847,3 +776,31 @@ redef class ANewExpr end end end + +# Ast representation of the `in_assertion` checking +# Note, the node if is only composed with a then body (`n_body`) +class AIfInAssertion + super AExpr + + # The body of the if + var n_body: AExpr is writable + + redef fun accept_scope_visitor(v) + do + v.enter_visit_block(n_body, null) + end + + redef fun visit_all(v: Visitor) + do + v.enter_visit(n_body) + end + + redef fun accept_typing(v) + do + v.visit_stmt(n_body) + + self.is_typed = true + + self.mtype = n_body.mtype + end +end diff --git a/src/interpreter/naive_interpreter.nit b/src/interpreter/naive_interpreter.nit index 527f16eb9a..36b4a920ab 100644 --- a/src/interpreter/naive_interpreter.nit +++ b/src/interpreter/naive_interpreter.nit @@ -23,6 +23,7 @@ private import parser::tables import mixin private import model::serialize_model private import frontend::explain_assert_api +private import contracts redef class ToolContext # --discover-call-trace @@ -74,6 +75,9 @@ class NaiveInterpreter # Name of all supported functional names var routine_types: Set[String] = new HashSet[String] + # Flag used to know if we are currently checking some assertions. + var in_assertion: Bool = false + init do if mainmodule.model.get_mclasses_by_name("Bool") != null then @@ -1827,6 +1831,18 @@ redef class AIfexprExpr end end + +redef class AIfInAssertion + redef fun stmt(v) + do + if not v.in_assertion then + v.in_assertion = true + v.stmt(self.n_body) + v.in_assertion = false + end + end +end + redef class ADoExpr redef fun stmt(v) do diff --git a/tests/contracts_threaded.nit b/tests/contracts_threaded.nit new file mode 100644 index 0000000000..06dfbebd0b --- /dev/null +++ b/tests/contracts_threaded.nit @@ -0,0 +1,52 @@ +# This file is part of NIT ( http://www.nitlanguage.org ). +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. + +# This test shows the verification of contracts in a parallel execution. + +import pthreads + +fun foo is + threaded + expect(contract_foo) +do + print "Foo" + bar("Foo thread") +end + +fun bar(thread_name: String) +is + threaded + expect(contract_bar(thread_name)) +do + print "Bar called from {thread_name}" +end + +fun contract_foo: Bool +do + print("Foo contract") + return true +end + +fun contract_bar(thread_name: String): Bool +do + sys.nanosleep(3,0) + print("Bar contract called from {thread_name}") + return true +end + + +foo +sys.nanosleep(1,0) +bar("Main thread") +sys.nanosleep(5,0) diff --git a/tests/sav/contracts_threaded.res b/tests/sav/contracts_threaded.res new file mode 100644 index 0000000000..f823b0f69e --- /dev/null +++ b/tests/sav/contracts_threaded.res @@ -0,0 +1,6 @@ +Foo contract +Foo +Bar contract called from Foo thread +Bar called from Foo thread +Bar contract called from Main thread +Bar called from Main thread