From c3860c1bf17c42745e4011e65114b39595a22950 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Sun, 9 Feb 2020 10:22:08 +0700
Subject: [PATCH] Check variable declaration stack before using it

---
 src/ast.rs                              | 156 ------------------------
 src/translate/verify_properties.rs      |   7 +-
 src/utils/variable_declaration_stack.rs |  12 +-
 3 files changed, 15 insertions(+), 160 deletions(-)
 delete mode 100644 src/ast.rs

diff --git a/src/ast.rs b/src/ast.rs
deleted file mode 100644
index 4890bcd..0000000
--- a/src/ast.rs
+++ /dev/null
@@ -1,156 +0,0 @@
-// Operators
-
-pub enum BinaryOperator
-{
-	Plus,
-	Minus,
-	Multiplication,
-	Division,
-	Modulo,
-	Power,
-}
-
-pub enum ComparisonOperator
-{
-	GreaterThan,
-	LessThan,
-	LessEqual,
-	GreaterEqual,
-	NotEqual,
-	Equal,
-}
-
-pub enum UnaryOperator
-{
-	AbsoluteValue,
-	Minus,
-}
-
-// Primitives
-
-pub struct FunctionDeclaration
-{
-	pub name: String,
-	pub arity: usize,
-}
-
-pub struct PredicateDeclaration
-{
-	pub name: String,
-	pub arity: usize,
-}
-
-pub struct VariableDeclaration
-{
-	pub name: String,
-}
-
-// Terms
-
-pub struct BinaryOperation
-{
-	pub operator: BinaryOperator,
-	pub left: Box<Term>,
-	pub right: Box<Term>,
-}
-
-pub struct Function
-{
-	pub declaration: std::rc::Rc<FunctionDeclaration>,
-	pub arguments: Vec<Box<Term>>,
-}
-
-pub struct Interval
-{
-	pub from: Box<Term>,
-	pub to: Box<Term>,
-}
-
-pub enum SpecialInteger
-{
-	Infimum,
-	Supremum,
-}
-
-pub struct UnaryOperation
-{
-	pub operator: UnaryOperator,
-	pub argument: Box<Term>,
-}
-
-pub struct Variable
-{
-	pub declaration: std::rc::Rc<VariableDeclaration>,
-}
-
-// Formulas
-
-pub struct Biconditional
-{
-	pub left: Box<Formula>,
-	pub right: Box<Formula>,
-}
-
-pub struct Comparison
-{
-	pub operator: ComparisonOperator,
-	pub left: Box<Term>,
-	pub right: Box<Term>,
-}
-
-pub struct Exists
-{
-	pub parameters: Vec<std::rc::Rc<VariableDeclaration>>,
-	pub argument: Box<Formula>,
-}
-
-pub struct ForAll
-{
-	pub parameters: Vec<std::rc::Rc<VariableDeclaration>>,
-	pub argument: Box<Formula>,
-}
-
-pub struct Implies
-{
-	pub left: Box<Formula>,
-	pub right: Box<Formula>,
-}
-
-pub struct Predicate
-{
-	pub declaration: std::rc::Rc<PredicateDeclaration>,
-	pub arguments: Vec<Box<Term>>,
-}
-
-// Variants
-
-pub enum Term
-{
-	BinaryOperation(BinaryOperation),
-	Boolean(bool),
-	Function(Function),
-	Integer(i32),
-	Interval(Interval),
-	SpecialInteger(SpecialInteger),
-	String(String),
-	UnaryOperation(UnaryOperation),
-	Variable(Variable),
-}
-
-pub type Terms = Vec<Box<Term>>;
-
-pub enum Formula
-{
-	And(Formulas),
-	Biconditional(Biconditional),
-	Boolean(bool),
-	Comparison(Comparison),
-	Exists(Exists),
-	ForAll(ForAll),
-	Implies(Implies),
-	Not(Box<Formula>),
-	Or(Formulas),
-	Predicate(Predicate),
-}
-
-pub type Formulas = Vec<Box<Formula>>;
diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs
index f3f8c84..9e43508 100644
--- a/src/translate/verify_properties.rs
+++ b/src/translate/verify_properties.rs
@@ -333,6 +333,11 @@ where
 
 fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::Error>
 {
+	if !context.variable_declaration_stack.borrow().is_empty()
+	{
+		return Err(crate::Error::new_logic("variable declaration stack in unexpected state"));
+	}
+
 	let head_type = determine_head_type(rule.head(), context)?;
 
 	match &head_type
@@ -396,7 +401,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
 				definition_arguments.push(Box::new(translated_head_term));
 			}
 
-			context.variable_declaration_stack.borrow_mut().pop();
+			context.variable_declaration_stack.borrow_mut().pop()?;
 
 			let free_variable_declarations = std::mem::replace(
 				&mut context.variable_declaration_stack.borrow_mut().free_variable_declarations,
diff --git a/src/utils/variable_declaration_stack.rs b/src/utils/variable_declaration_stack.rs
index a17f8c4..7728cec 100644
--- a/src/utils/variable_declaration_stack.rs
+++ b/src/utils/variable_declaration_stack.rs
@@ -51,14 +51,20 @@ impl VariableDeclarationStack
 		variable_declaration
 	}
 
+	pub fn is_empty(&self) -> bool
+	{
+		self.free_variable_declarations.is_empty()
+			&& self.bound_variable_declaration_stack.is_empty()
+	}
+
 	pub fn push(&mut self, bound_variable_declarations: std::rc::Rc<foliage::VariableDeclarations>)
 	{
 		self.bound_variable_declaration_stack.push(bound_variable_declarations);
 	}
 
-	pub fn pop(&mut self)
+	pub fn pop(&mut self) -> Result<(), crate::Error>
 	{
-		// TODO: return error instead
-		self.bound_variable_declaration_stack.pop().expect("bound variable is empty, cannot pop last element");
+		self.bound_variable_declaration_stack.pop().map(|_| ())
+			.ok_or(crate::Error::new_logic("variable stack not in expected state"))
 	}
 }