Contract with threaded method

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

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

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

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)

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