From e27fdd1190cd83fa2b14bb76ad4779e8cd2e1a57 Mon Sep 17 00:00:00 2001
From: schaeff <thibaut@schaeff.fr>
Date: Sun, 10 Dec 2017 00:03:39 +0100
Subject: [PATCH] add semantic analysis

---
 src/absy.rs      |   4 +-
 src/main.rs      |   6 ++
 src/semantics.rs | 151 +++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 159 insertions(+), 2 deletions(-)
 create mode 100644 src/semantics.rs

diff --git a/src/absy.rs b/src/absy.rs
index 34fa8334..f4a50253 100644
--- a/src/absy.rs
+++ b/src/absy.rs
@@ -9,7 +9,7 @@ use std::fmt;
 use std::collections::HashMap;
 use field::Field;
 
-#[derive(Serialize, Deserialize)]
+#[derive(Serialize, Deserialize, Clone)]
 pub struct Prog<T: Field> {
     /// Functions of the program
     pub functions: Vec<Function<T>>,
@@ -55,7 +55,7 @@ impl<T: Field> fmt::Debug for Prog<T> {
     }
 }
 
-#[derive(Serialize, Deserialize)]
+#[derive(Serialize, Deserialize, Clone)]
 pub struct Function<T: Field> {
     /// Name of the program
     pub id: String,
diff --git a/src/main.rs b/src/main.rs
index e52d11ca..b8169a57 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -18,6 +18,7 @@ extern crate regex;
 
 mod absy;
 mod parser;
+mod semantics;
 mod flatten;
 mod r1cs;
 mod field;
@@ -33,6 +34,7 @@ use std::io::prelude::*;
 use field::{Field, FieldPrime};
 use absy::Prog;
 use parser::parse_program;
+use semantics::Checker;
 use flatten::Flattener;
 use r1cs::r1cs_program;
 use clap::{App, AppSettings, Arg, SubCommand};
@@ -209,6 +211,10 @@ fn main() {
                 }
             };
 
+            // check semantics
+            let semantics_ok = Checker::new().check_program(program_ast.clone());
+            println!("Semantics ok? {:?}", semantics_ok);
+
             // flatten input program
             let program_flattened =
                 Flattener::new(FieldPrime::get_required_bits()).flatten_program(program_ast);
diff --git a/src/semantics.rs b/src/semantics.rs
new file mode 100644
index 00000000..41aad115
--- /dev/null
+++ b/src/semantics.rs
@@ -0,0 +1,151 @@
+//! Module containing semantic analysis tools to run at compile time
+//!
+//! @file flatten.rs
+//! @author Dennis Kuhnert <dennis.kuhnert@campus.tu-berlin.de>
+//! @author Jacob Eberhardt <jacob.eberhardt@tu-berlin.de>
+//! @date 2017
+
+use std::collections::{HashMap, HashSet};
+use absy::*;
+use field::Field;
+
+#[derive(Clone, PartialEq, Eq, Hash)]
+pub struct Symbol {
+	id: String,
+	level: usize
+}
+
+// Checker, checks the semantics of a program.
+pub struct Checker {
+	scope: HashSet<Symbol>,
+	level: usize
+}
+
+impl Checker {
+	pub fn new() -> Checker {
+		Checker {
+			scope: HashSet::new(),
+			level: 0
+		}
+	}
+
+	pub fn new_with_args(scope: HashSet<Symbol>, level: usize) -> Checker {
+		Checker {
+			scope: scope,
+			level: level
+		}
+	}
+
+	pub fn check_program<T: Field>(&mut self, prog: Prog<T>) -> bool {
+		let mut res = true;
+		for func in prog.functions {
+			let function_checked = self.check_function(func);
+			res = res && function_checked;
+		}
+		res
+	}
+
+	fn check_function<T: Field>(&mut self, funct: Function<T>) -> bool {
+		self.level += 1;
+		for arg in funct.arguments {
+			self.scope.insert(Symbol {
+				id: arg.id.to_string(),
+				level: 0
+			});
+		}
+		let mut res = true;
+		for stat in funct.statements {
+			let statement_checked = self.check_statement(
+				stat
+			);
+			res = res && statement_checked;
+		}
+		self.level -= 1;
+		// TODO: cleanup scope of all symbols of level i
+		res
+	}
+
+	fn check_statement<T: Field>(&mut self, stat: Statement<T>) -> bool {
+		match stat {
+			Statement::Return(expr) => {
+				self.check_expression(expr)
+			}
+			Statement::Definition(id, expr) => {
+				let expr_checked = self.check_expression(expr);
+				self.scope.insert(Symbol {
+					id: id.to_string(),
+					level: 0
+				});
+				expr_checked
+
+			}
+			Statement::Condition(lhs, rhs) => {
+				self.check_expression(lhs) && self.check_expression(rhs)
+			}
+			_ => true,
+		}
+	}
+
+	fn check_expression<T: Field>(&mut self, expr: Expression<T>) -> bool {
+		match expr {
+			Expression::Identifier(id) => {
+				self.scope.contains(&Symbol {id: id.to_string(), level: 0})
+			}
+			Expression::Add(box e1, box e2) | Expression::Sub(box e1, box e2) | Expression::Mult(box e1, box e2) |
+			Expression::Div(box e1, box e2) | Expression::Pow(box e1, box e2) => {
+				self.check_expression(e1) && self.check_expression(e2)
+			}
+			Expression::IfElse(box condition, box consequent, box alternative) => {
+				self.check_condition(condition) && self.check_expression(consequent) && self.check_expression(alternative)
+			}
+			_ => true,
+		}
+	}
+
+	fn check_condition<T: Field>(&mut self, cond: Condition<T>) -> bool {
+		match cond {
+			Condition::Lt(e1, e2) |
+			Condition::Le(e1, e2) |
+			Condition::Eq(e1, e2) |
+			Condition::Ge(e1, e2) |
+			Condition::Gt(e1, e2) => {
+				self.check_expression(e1) && self.check_expression(e2)
+			}
+		}
+	}
+}
+
+#[cfg(test)]
+mod tests {
+	use super::*;
+	use field::FieldPrime;
+
+	#[test]
+	fn undefined_variable_in_statement() {
+		// a = b
+		// b undefined
+		let statement: Statement<FieldPrime> = Statement::Definition(
+			String::from("a"),
+			Expression::Identifier(String::from("b"))
+		);
+		let mut checker = Checker::new();
+		assert_eq!(checker.check_statement(statement), false);
+	}
+
+	#[test]
+	fn defined_variable_in_statement() {
+		// a = b
+		// b undefined
+		let statement: Statement<FieldPrime> = Statement::Definition(
+			String::from("a"),
+			Expression::Identifier(String::from("b"))
+		);
+		let mut scope = HashSet::new();
+		scope.insert(Symbol {
+			id: String::from("b"),
+			level: 0
+		});
+		let mut checker = Checker::new_with_args(scope, 1);
+		assert_eq!(checker.check_statement(statement), true);
+	}
+}
\ No newline at end of file