From b9833d87be7a747afa0685fac4defe1e6829335e Mon Sep 17 00:00:00 2001
From: Florian Deljarry <deljarry.florian@gmail.com>
Date: Mon, 20 Apr 2020 17:23:10 -0400
Subject: [PATCH] contracts: Add `in_contract` attribute

This attribute is used to disable contract verification when you are already in a contract verification.

Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
---
 src/contracts.nit |   80 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 79 insertions(+), 1 deletion(-)

diff --git a/src/contracts.nit b/src/contracts.nit
index 78803a2..3a3c3a7 100644
--- a/src/contracts.nit
+++ b/src/contracts.nit
@@ -18,10 +18,10 @@
 # FIXME Split the module in three parts: extension of the modele, building phase and the "re-driving"
 module contracts
 
-import astbuilder
 import parse_annotations
 import phase
 import semantize
+intrude import astbuilder
 intrude import modelize_property
 intrude import scope
 intrude import typing
@@ -101,6 +101,11 @@ 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)
@@ -165,6 +170,79 @@ private class ContractsVisitor
 		return toolcontext.opt_full_contract.value or mainmodule.mpackage == actual_mmodule.mpackage
 	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
+	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
+	end
 end
 
 # This visitor checks the `callsite` to see if the target `mpropdef` has a contract.
-- 
1.7.9.5