SMV: add lhs() and rhs() helper methods

This adds lhs() and rhs() helper methods to the SMV parse tree node class.

Author: kroening

src/smvlang/smv_parse_tree.h

@@ -141,20 +141,37 @@ class smv_parse_treet
       }
 
       // for ASSIGN_CURRENT, ASSIGN_INIT, ASSIGN_NEXT, DEFINE
-      const equal_exprt &equal_expr() const
+      const exprt &lhs() const
       {
         PRECONDITION(
           is_assign_current() || is_assign_init() || is_assign_next() ||
           is_define());
-        return to_equal_expr(expr);
+        return to_equal_expr(expr).lhs();
       }
 
-      equal_exprt &equal_expr()
+      exprt &lhs()
       {
         PRECONDITION(
           is_assign_current() || is_assign_init() || is_assign_next() ||
           is_define());
-        return to_equal_expr(expr);
+        return to_equal_expr(expr).lhs();
+      }
+
+      // for ASSIGN_CURRENT, ASSIGN_INIT, ASSIGN_NEXT, DEFINE
+      const exprt &rhs() const
+      {
+        PRECONDITION(
+          is_assign_current() || is_assign_init() || is_assign_next() ||
+          is_define());
+        return to_equal_expr(expr).rhs();
+      }
+
+      exprt &rhs()
+      {
+        PRECONDITION(
+          is_assign_current() || is_assign_init() || is_assign_next() ||
+          is_define());
+        return to_equal_expr(expr).rhs();
       }
 
       void show(std::ostream &) const;

src/smvlang/smv_typecheck.cpp

@@ -63,7 +63,7 @@ class smv_typecheckt:public typecheckt
 
   void create_var_symbols(const smv_parse_treet::modulet::element_listt &);
 
-  void collect_define(const equal_exprt &);
+  void collect_define(const exprt &lhs, const exprt &rhs);
   void convert_defines(exprt::operandst &invar);
   void convert_define(const irep_idt &identifier);
 
@@ -1959,32 +1959,25 @@ void smv_typecheckt::typecheck(smv_parse_treet::modulet::elementt &element)
     return;
 
   case smv_parse_treet::modulet::elementt::ASSIGN_CURRENT:
-    typecheck(element.equal_expr().lhs(), OTHER);
-    typecheck(element.equal_expr().rhs(), OTHER);
-    convert_expr_to(
-      element.equal_expr().rhs(), element.equal_expr().lhs().type());
-    element.equal_expr().type() = bool_typet{};
+    typecheck(element.lhs(), OTHER);
+    typecheck(element.rhs(), OTHER);
+    convert_expr_to(element.rhs(), element.lhs().type());
     return;
 
   case smv_parse_treet::modulet::elementt::ASSIGN_INIT:
-    typecheck(element.equal_expr().lhs(), INIT);
-    typecheck(element.equal_expr().rhs(), INIT);
-    convert_expr_to(
-      element.equal_expr().rhs(), element.equal_expr().lhs().type());
-    element.equal_expr().type() = bool_typet{};
+    typecheck(element.lhs(), INIT);
+    typecheck(element.rhs(), INIT);
+    convert_expr_to(element.rhs(), element.lhs().type());
     return;
 
   case smv_parse_treet::modulet::elementt::ASSIGN_NEXT:
-    typecheck(element.equal_expr().lhs(), TRANS);
-    typecheck(element.equal_expr().rhs(), TRANS);
-    convert_expr_to(
-      element.equal_expr().rhs(), element.equal_expr().lhs().type());
-    element.equal_expr().type() = bool_typet{};
+    typecheck(element.lhs(), TRANS);
+    typecheck(element.rhs(), TRANS);
+    convert_expr_to(element.rhs(), element.lhs().type());
     return;
 
   case smv_parse_treet::modulet::elementt::DEFINE:
     typecheck(element.expr, OTHER);
-    element.equal_expr().type() = bool_typet{};
     return;
 
   case smv_parse_treet::modulet::elementt::ENUM:
@@ -2069,8 +2062,7 @@ void smv_typecheckt::variable_checks(const smv_parse_treet::modulet &module)
     }
     else if(element.is_define())
     {
-      const auto &identifier_expr =
-        to_smv_identifier_expr(to_equal_expr(element.expr).lhs());
+      const auto &identifier_expr = to_smv_identifier_expr(element.lhs());
       irep_idt base_name = identifier_expr.identifier();
 
       // already used as enum?
@@ -2194,8 +2186,7 @@ void smv_typecheckt::create_var_symbols(
     }
     else if(element.is_define())
     {
-      const auto &identifier_expr =
-        to_smv_identifier_expr(to_equal_expr(element.expr).lhs());
+      const auto &identifier_expr = to_smv_identifier_expr(element.lhs());
       irep_idt base_name = identifier_expr.identifier();
       irep_idt identifier = module + "::var::" + id2string(base_name);
 
@@ -2256,11 +2247,8 @@ Function: smv_typecheckt::collect_define
 
 \*******************************************************************/
 
-void smv_typecheckt::collect_define(const equal_exprt &expr)
+void smv_typecheckt::collect_define(const exprt &lhs, const exprt &rhs)
 {
-  const exprt &lhs = expr.lhs();
-  const exprt &rhs = expr.rhs();
-
   if(lhs.id() != ID_symbol)
     throw errort() << "collect_define expects symbol on left hand side";
 
@@ -2286,9 +2274,9 @@ void smv_typecheckt::collect_define(const equal_exprt &expr)
 
   if(!result.second)
   {
-    throw errort().with_location(expr.find_source_location())
+    throw errort().with_location(lhs.source_location())
       << "variable `" << symbol.display_name() << "' already defined";
-  }  
+  }
 }
 
 /*******************************************************************\
@@ -2416,7 +2404,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
     for(auto &element : smv_module.elements)
     {
       if(element.is_define() || element.is_assign_current())
-        collect_define(element.equal_expr());
+        collect_define(element.lhs(), element.rhs());
     }
     // now turn them into INVARs
     convert_defines(trans_invar);