Added new statement (assert_eq)

- For issue #5, so transaction arguments can remain constant within body
- Implemented Serializability
- Implemented Type Checking
- Updated add_struct test case

Author: fpham0701

src/ir.rs

@@ -179,6 +179,7 @@ pub enum Stmt {
     Fork,
     While(ExprId, StmtId),
     IfElse(ExprId, StmtId, StmtId),
+    AssertEq(ExprId, ExprId),
 }
 
 #[derive(Clone, Copy, Hash, PartialEq, Eq, Default)]

src/serialize.rs

@@ -90,6 +90,15 @@ fn build_statements(
             build_statements(out, tr, st, elsebody, index + 1)?;
             writeln!(out, "{}}}", "  ".repeat(index))?;
         }
+        Stmt::AssertEq(exprid1, exprid2) => {
+            writeln!(
+                out,
+                "{}assert_eq({}, {});",
+                "  ".repeat(index),
+                serialize_expr(tr, st, exprid1),
+                serialize_expr(tr, st, exprid2)
+            )?;
+        }
     }
 
     Ok(())
@@ -228,6 +237,7 @@ pub mod tests {
         add.add_expr_loc(b_expr, 208, 209, add_fileid);
         let dut_s_expr = add.e(Expr::Sym(dut_s));
         add.add_expr_loc(dut_s_expr, 271, 276, add_fileid);
+        let s_expr = add.e(Expr::Sym(s));
 
         // 4) create statements
         let a_assign = add.s(Stmt::Assign(dut_a, a_expr));
@@ -246,6 +256,8 @@ pub mod tests {
         add.add_stmt_loc(s_assign, 266, 277, add_fileid);
         let dut_s_assign = add.s(Stmt::Assign(dut_s, a_expr));
         add.add_stmt_loc(dut_s_assign, 281, 292, add_fileid);
+        let assert = add.s(Stmt::AssertEq(s_expr, dut_s_expr));
+        add.add_stmt_loc(assert, 296, 316, add_fileid);
         let body = vec![
             a_assign,
             b_assign,
@@ -255,6 +267,7 @@ pub mod tests {
             dut_b_assign,
             s_assign,
             dut_s_assign,
+            assert,
         ];
         add.body = add.s(Stmt::Block(body));
 

src/typecheck.rs

@@ -148,6 +148,26 @@ fn check_stmt_types(
                 Ok(())
             }
         }
+        Stmt::AssertEq(exprid1, exprid2) => {
+            let expr1_type = check_expr_types(tr, st, handler, exprid1)?;
+            let expr2_type = check_expr_types(tr, st, handler, exprid2)?;
+            if expr1_type.is_equivalent(&expr2_type) {
+                Ok(())
+            } else {
+                let expr1_name = serialize_expr(tr, st, exprid1);
+                let expr2_name = serialize_expr(tr, st, exprid2);
+                handler.emit_diagnostic_stmt(
+                    tr,
+                    stmt_id,
+                    &format!(
+                        "Type mismatch in assert_eq: {} : {:?} and {} : {:?}.",
+                        expr1_name, expr1_type, expr2_name, expr2_type,
+                    ),
+                    Level::Error,
+                );
+                Ok(())
+            }
+        }
         Stmt::Block(stmts) => {
             for stmtid in stmts {
                 check_stmt_types(tr, st, handler, stmtid)?;

tests/addStruct.prot

@@ -14,4 +14,5 @@ fn add<DUT: Adder>(in a: u32, in b: u32, out s: u32) {
   DUT.b := X;
   s := DUT.s;
   DUT.s := a;
+  assert_eq(s, DUT.s);
 }