From 62b9e2da048726cda7d71762fd227a8b546a3a0f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Fri, 17 Apr 2020 01:22:42 +0200
Subject: [PATCH] Make variable declaration stack safer with guards

---
 src/parse/formulas.rs |  7 ++----
 src/parse/terms.rs    | 18 ++++++++++------
 src/utils.rs          | 50 ++++++++++++++++++++++++++++++++++++++-----
 3 files changed, 58 insertions(+), 17 deletions(-)

diff --git a/src/parse/formulas.rs b/src/parse/formulas.rs
index 979275f..b052984 100644
--- a/src/parse/formulas.rs
+++ b/src/parse/formulas.rs
@@ -259,14 +259,11 @@ fn quantified_formula<'a, 'b>(i: &'a str, d: &Declarations, keyword: &'b str)
 					return Err(nom::Err::Failure((i, nom::error::ErrorKind::Many1)));
 				}
 
-				d.variable_declaration_stack.borrow_mut().push(std::rc::Rc::clone(&variable_declarations));
+				let _guard = crate::VariableDeclarationStack::push(&d.variable_declaration_stack,
+					std::rc::Rc::clone(&variable_declarations));
 
 				let (i, argument) = formula_precedence_0(i, d)?;
 
-				// TODO: report logic errors more appropriately
-				d.variable_declaration_stack.borrow_mut().pop()
-					.map_err(|_| nom::Err::Failure((i, nom::error::ErrorKind::Verify)))?;
-
 				Ok((i, crate::QuantifiedFormula::new(variable_declarations, Box::new(argument))))
 			}
 		),
diff --git a/src/parse/terms.rs b/src/parse/terms.rs
index b329ad8..d34f691 100644
--- a/src/parse/terms.rs
+++ b/src/parse/terms.rs
@@ -94,7 +94,7 @@ pub(crate) fn function_or_predicate<'i>(i: &'i str, d: &Declarations)
 	)(i)
 }
 
-pub fn function<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Function>
+fn function<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Function>
 {
 	map
 	(
@@ -133,7 +133,7 @@ pub fn function<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Fun
 	)(i)
 }
 
-pub fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
+pub(crate) fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
 {
 	map
 	(
@@ -142,7 +142,7 @@ pub fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration
 	)(i)
 }
 
-pub fn variable<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Variable>
+fn variable<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Variable>
 {
 	map
 	(
@@ -801,7 +801,8 @@ mod tests
 		assert_ne!(x1.declaration, y1.declaration);
 		assert_ne!(x2.declaration, y1.declaration);
 
-		declarations.variable_declaration_stack.borrow_mut().push(layer_1);
+		let _guard
+			= VariableDeclarationStack::push(&declarations.variable_declaration_stack, layer_1);
 
 		let x3 = variable("X");
 		assert_eq!(number_of_free_variable_declarations(), 2);
@@ -816,7 +817,8 @@ mod tests
 		assert_eq!(number_of_free_variable_declarations(), 2);
 		assert_eq!(y1.declaration, y2.declaration);
 
-		declarations.variable_declaration_stack.borrow_mut().push(layer_2);
+		let _guard
+			= VariableDeclarationStack::push(&declarations.variable_declaration_stack, layer_2);
 
 		let x5 = variable("X");
 		assert_eq!(number_of_free_variable_declarations(), 2);
@@ -829,7 +831,8 @@ mod tests
 		assert_eq!(number_of_free_variable_declarations(), 2);
 		assert_eq!(a1.declaration, a2.declaration);
 
-		declarations.variable_declaration_stack.borrow_mut().push(layer_3);
+		let _guard
+			= VariableDeclarationStack::push(&declarations.variable_declaration_stack, layer_3);
 
 		let x7 = variable("X");
 		assert_eq!(number_of_free_variable_declarations(), 2);
@@ -838,7 +841,8 @@ mod tests
 		assert_eq!(number_of_free_variable_declarations(), 2);
 		assert_ne!(y2.declaration, y3.declaration);
 
-		declarations.variable_declaration_stack.borrow_mut().push(layer_4);
+		let _guard
+			= VariableDeclarationStack::push(&declarations.variable_declaration_stack, layer_4);
 
 		let x8 = variable("X");
 		assert_eq!(number_of_free_variable_declarations(), 2);
diff --git a/src/utils.rs b/src/utils.rs
index 18f6bdd..4147807 100644
--- a/src/utils.rs
+++ b/src/utils.rs
@@ -1,3 +1,20 @@
+pub trait FindFunctionDeclaration
+{
+	fn find_function_declaration(&self, name: &str, arity: usize)
+		-> std::rc::Rc<crate::FunctionDeclaration>;
+}
+
+pub trait FindPredicateDeclaration
+{
+	fn find_predicate_declaration(&self, name: &str, arity: usize)
+		-> std::rc::Rc<crate::PredicateDeclaration>;
+}
+
+pub trait FindVariableDeclaration
+{
+	fn find_variable_declaration(&self, name: &str) -> std::rc::Rc<crate::VariableDeclaration>;
+}
+
 pub struct VariableDeclarationStack
 {
 	pub free_variable_declarations: crate::VariableDeclarations,
@@ -59,14 +76,37 @@ impl VariableDeclarationStack
 			&& self.bound_variable_declaration_stack.is_empty()
 	}
 
-	pub fn push(&mut self, bound_variable_declarations: std::rc::Rc<crate::VariableDeclarations>)
+	pub fn push<'v>(variable_declaration_stack: &'v std::cell::RefCell<VariableDeclarationStack>,
+		bound_variable_declarations: std::rc::Rc<crate::VariableDeclarations>)
+		-> VariableDeclarationStackGuard
 	{
-		self.bound_variable_declaration_stack.push(bound_variable_declarations);
+		variable_declaration_stack.borrow_mut()
+			.bound_variable_declaration_stack.push(bound_variable_declarations);
+
+		VariableDeclarationStackGuard
+		{
+			variable_declaration_stack: variable_declaration_stack,
+		}
 	}
 
-	pub fn pop(&mut self) -> Result<(), crate::Error>
+	pub(self) fn pop(&mut self)
 	{
-		self.bound_variable_declaration_stack.pop().map(|_| ())
-			.ok_or_else(|| crate::Error::new_logic("variable stack not in expected state"))
+		if let None = self.bound_variable_declaration_stack.pop()
+		{
+			unreachable!()
+		}
+	}
+}
+
+pub struct VariableDeclarationStackGuard<'v>
+{
+	variable_declaration_stack: &'v std::cell::RefCell<VariableDeclarationStack>,
+}
+
+impl<'v> Drop for VariableDeclarationStackGuard<'v>
+{
+	fn drop(&mut self)
+	{
+		self.variable_declaration_stack.borrow_mut().pop();
 	}
 }