SMV: avoid some expression copies

References are changed to rvalue references to avoid some copying when
populating the parse tree.

Author: kroening

src/smvlang/parser.y

@@ -486,17 +486,15 @@ assignments: assignment
 
 assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
            {
-             binary($$, $3, ID_equal, $6);
-
              if(stack_expr($1).id()==ID_smv_next)
              {
-               exprt &op=to_binary_expr(stack_expr($$)).op0();
+               exprt &op=stack_expr($3);
                unary_exprt tmp(ID_smv_next, std::move(op));
                tmp.swap(op);
-               PARSER.module->add_assign_next(to_equal_expr(stack_expr($$)));
+               PARSER.module->add_assign_next(std::move(stack_expr($3)), std::move(stack_expr($6)));
              }
              else
-               PARSER.module->add_assign_init(to_equal_expr(stack_expr($$)));
+               PARSER.module->add_assign_init(std::move(stack_expr($3)), std::move(stack_expr($6)));
            }
            | assignment_var BECOMES_Token formula ';'
            {
@@ -528,8 +526,7 @@ assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
                DATA_INVARIANT(false, "unexpected variable class");
              }
 
-             binary($$, $1, ID_equal, $3);
-             PARSER.module->add_assign_current(to_equal_expr(stack_expr($$)));
+             PARSER.module->add_assign_current(std::move(stack_expr($1)), std::move(stack_expr($3)));
            }
            ;
 
@@ -575,8 +572,7 @@ define     : assignment_var BECOMES_Token formula ';'
                DATA_INVARIANT(false, "unexpected variable class");
              }
 
-             binary($$, $1, ID_equal, $3);
-             PARSER.module->add_define(to_equal_expr(stack_expr($$)));
+             PARSER.module->add_define(std::move(stack_expr($1)), std::move(stack_expr($3)));
            }
            ;
 

src/smvlang/smv_parse_tree.h

@@ -118,100 +118,110 @@ class smv_parse_treet
     typedef std::list<itemt> item_listt;
     item_listt items;
 
-    void add_item(
-      itemt::item_typet item_type,
-      const exprt &expr,
-      const source_locationt &location)
+    void
+    add_item(itemt::item_typet item_type, exprt expr, source_locationt location)
     {
-      items.push_back(itemt());
+      items.push_back(itemt{});
       items.back().item_type=item_type;
-      items.back().expr=expr;
-      items.back().location=location;
+      items.back().expr = std::move(expr);
+      items.back().location = std::move(location);
     }
 
-    void add_assign_current(const equal_exprt &expr)
+    void add_assign_current(exprt lhs, exprt rhs)
     {
-      add_item(itemt::ASSIGN_CURRENT, expr, source_locationt::nil());
+      add_item(
+        itemt::ASSIGN_CURRENT,
+        binary_exprt{std::move(lhs), ID_equal, std::move(rhs)},
+        source_locationt::nil());
     }
 
-    void add_assign_init(const equal_exprt &expr)
+    void add_assign_init(exprt lhs, exprt rhs)
     {
-      add_item(itemt::ASSIGN_INIT, expr, source_locationt::nil());
+      add_item(
+        itemt::ASSIGN_INIT,
+        binary_exprt{std::move(lhs), ID_equal, std::move(rhs)},
+        source_locationt::nil());
     }
 
-    void add_assign_next(const equal_exprt &expr)
+    void add_assign_next(exprt lhs, exprt rhs)
     {
-      add_item(itemt::ASSIGN_NEXT, expr, source_locationt::nil());
+      add_item(
+        itemt::ASSIGN_NEXT,
+        binary_exprt{std::move(lhs), ID_equal, std::move(rhs)},
+        source_locationt::nil());
     }
 
-    void add_invar(const exprt &expr)
+    void add_invar(exprt expr)
     {
-      add_item(itemt::INVAR, expr, source_locationt::nil());
+      add_item(itemt::INVAR, std::move(expr), source_locationt::nil());
     }
 
-    void add_ctlspec(const exprt &expr)
+    void add_ctlspec(exprt expr)
     {
-      add_item(itemt::CTLSPEC, expr, source_locationt::nil());
+      add_item(itemt::CTLSPEC, std::move(expr), source_locationt::nil());
     }
 
-    void add_ltlspec(const exprt &expr)
+    void add_ltlspec(exprt expr)
     {
-      add_item(itemt::LTLSPEC, expr, source_locationt::nil());
+      add_item(itemt::LTLSPEC, std::move(expr), source_locationt::nil());
     }
 
-    void add_define(const equal_exprt &expr)
+    void add_define(exprt lhs, exprt rhs)
     {
-      add_item(itemt::DEFINE, expr, source_locationt::nil());
+      add_item(
+        itemt::DEFINE,
+        binary_exprt{std::move(lhs), ID_equal, std::move(rhs)},
+        source_locationt::nil());
     }
-    
-    void add_fairness(const exprt &expr)
+
+    void add_fairness(exprt expr)
     {
-      add_item(itemt::FAIRNESS, expr, source_locationt::nil());
+      add_item(itemt::FAIRNESS, std::move(expr), source_locationt::nil());
     }
-    
-    void add_init(const exprt &expr)
+
+    void add_init(exprt expr)
     {
-      add_item(itemt::INIT, expr, source_locationt::nil());
+      add_item(itemt::INIT, std::move(expr), source_locationt::nil());
     }
-    
-    void add_trans(const exprt &expr)
+
+    void add_trans(exprt expr)
     {
-      add_item(itemt::TRANS, expr, source_locationt::nil());
+      add_item(itemt::TRANS, std::move(expr), source_locationt::nil());
     }
-    
-    void add_invar(const exprt &expr, const source_locationt &location)
+
+    void add_invar(exprt expr, source_locationt location)
     {
-      add_item(itemt::INVAR, expr, location);
+      add_item(itemt::INVAR, std::move(expr), location);
     }
 
-    void add_ctlspec(const exprt &expr, const source_locationt &location)
+    void add_ctlspec(exprt expr, source_locationt location)
     {
-      add_item(itemt::CTLSPEC, expr, location);
+      add_item(itemt::CTLSPEC, std::move(expr), std::move(location));
     }
 
-    void add_ltlspec(const exprt &expr, const source_locationt &location)
+    void add_ltlspec(exprt expr, source_locationt location)
     {
-      add_item(itemt::LTLSPEC, expr, location);
+      add_item(itemt::LTLSPEC, std::move(expr), location);
     }
-    
-    void add_define(const exprt &expr, const source_locationt &location)
+
+    void add_define(exprt expr, source_locationt location)
     {
-      add_item(itemt::DEFINE, expr, location);
+      add_item(itemt::DEFINE, std::move(expr), std::move(location));
     }
-    
-    void add_fairness(const exprt &expr, const source_locationt &location)
+
+    void add_fairness(exprt expr, source_locationt location)
     {
-      add_item(itemt::FAIRNESS, expr, location);
+      add_item(itemt::FAIRNESS, std::move(expr), std::move(location));
     }
-    
-    void add_init(const exprt &expr, const source_locationt &location)
+
+    void add_init(exprt expr, source_locationt location)
     {
-      add_item(itemt::INIT, expr, location);
+      add_item(itemt::INIT, std::move(expr), std::move(location));
     }
-    
-    void add_trans(const exprt &expr, const source_locationt &location)
+
+    void add_trans(exprt expr, source_locationt location)
     {
-      add_item(itemt::TRANS, expr, location);
+      add_item(itemt::TRANS, std::move(expr), std::move(location));
     }
 
     mc_varst vars;