Merge pull request #5868 from diffblue/avoid_symex_code_assignt

symex: use lhs/rhs instead of code_assignt

Author: tautschnig

src/goto-symex/auto_objects.cpp

@@ -69,8 +69,7 @@ void goto_symext::initialize_auto_object(const exprt &expr, statet &state)
         null_pointer_exprt(pointer_type),
         address_of_expr);
 
-      code_assignt assignment(expr, rhs);
-      symex_assign(state, assignment);
+      symex_assign(state, expr, rhs);
     }
   }
 }

src/goto-symex/goto_symex.cpp

@@ -36,10 +36,13 @@ void goto_symext::do_simplify(exprt &expr)
     simplify(expr, ns);
 }
 
-void goto_symext::symex_assign(statet &state, const code_assignt &code)
+void goto_symext::symex_assign(
+  statet &state,
+  const exprt &o_lhs,
+  const exprt &o_rhs)
 {
-  exprt lhs = clean_expr(code.lhs(), state, true);
-  exprt rhs = clean_expr(code.rhs(), state, false);
+  exprt lhs = clean_expr(o_lhs, state, true);
+  exprt rhs = clean_expr(o_rhs, state, false);
 
   DATA_INVARIANT(
     lhs.type() == rhs.type(), "assignments must be type consistent");

src/goto-symex/goto_symex.h

@@ -508,8 +508,9 @@ class goto_symext
   /// Symbolically execute an ASSIGN instruction or simulate such an execution
   /// for a synthetic assignment
   /// \param state: Symbolic execution state for current instruction
-  /// \param code: The assignment to execute
-  void symex_assign(statet &state, const code_assignt &code);
+  /// \param lhs: The lhs of the assignment to execute
+  /// \param rhs: The rhs of the assignment to execute
+  void symex_assign(statet &state, const exprt &lhs, const exprt &rhs);
 
   /// Attempt to constant propagate side effects of the assignment (if any)
   ///

src/goto-symex/symex_builtin_functions.cpp

@@ -150,10 +150,10 @@ void goto_symext::symex_allocate(
 
       state.symbol_table.add(size_symbol);
 
-      code_assignt assignment(size_symbol.symbol_expr(), array_size);
-      array_size = assignment.lhs();
+      auto array_size_rhs = array_size;
+      array_size = size_symbol.symbol_expr();
 
-      symex_assign(state, assignment);
+      symex_assign(state, size_symbol.symbol_expr(), array_size_rhs);
     }
   }
 
@@ -181,15 +181,14 @@ void goto_symext::symex_allocate(
     const auto zero_value =
       zero_initializer(*object_type, code.source_location(), ns);
     CHECK_RETURN(zero_value.has_value());
-    code_assignt assignment(value_symbol.symbol_expr(), *zero_value);
-    symex_assign(state, assignment);
+    symex_assign(state, value_symbol.symbol_expr(), *zero_value);
   }
   else
   {
-    const code_assignt assignment{
-      value_symbol.symbol_expr(),
-      path_storage.build_symex_nondet(*object_type, code.source_location())};
-    symex_assign(state, assignment);
+    auto lhs = value_symbol.symbol_expr();
+    auto rhs =
+      path_storage.build_symex_nondet(*object_type, code.source_location());
+    symex_assign(state, lhs, rhs);
   }
 
   exprt rhs;
@@ -207,9 +206,7 @@ void goto_symext::symex_allocate(
       value_symbol.symbol_expr(), pointer_type(value_symbol.type));
   }
 
-  symex_assign(
-    state,
-    code_assignt(lhs, typecast_exprt::conditional_cast(rhs, lhs.type())));
+  symex_assign(state, lhs, typecast_exprt::conditional_cast(rhs, lhs.type()));
 }
 
 /// Construct an entry for the var args array. Visual Studio complicates this as
@@ -297,14 +294,12 @@ void goto_symext::symex_va_start(
   array = clean_expr(std::move(array), state, false);
   array = state.rename(std::move(array), ns).get();
   do_simplify(array);
-  symex_assign(state, code_assignt{va_array.symbol_expr(), std::move(array)});
+  symex_assign(state, va_array.symbol_expr(), std::move(array));
 
   exprt rhs = address_of_exprt{
     index_exprt{va_array.symbol_expr(), from_integer(0, index_type())}};
   rhs = state.rename(std::move(rhs), ns).get();
-  symex_assign(
-    state,
-    code_assignt{lhs, typecast_exprt::conditional_cast(rhs, lhs.type())});
+  symex_assign(state, lhs, typecast_exprt::conditional_cast(rhs, lhs.type()));
 }
 
 static irep_idt get_string_argument_rec(const exprt &src)
@@ -533,7 +528,7 @@ void goto_symext::symex_cpp_new(
   else
     rhs.copy_to_operands(symbol.symbol_expr());
 
-  symex_assign(state, code_assignt(lhs, rhs));
+  symex_assign(state, lhs, rhs);
 }
 
 void goto_symext::symex_cpp_delete(

src/goto-symex/symex_function_call.cpp

@@ -165,7 +165,7 @@ void goto_symext::parameter_assignments(
 
       state.call_stack().top().parameter_names.push_back(va_arg.name);
 
-      symex_assign(state, code_assignt{va_arg.symbol_expr(), *it1});
+      symex_assign(state, va_arg.symbol_expr(), *it1);
     }
   }
   else if(it1!=arguments.end())
@@ -287,8 +287,7 @@ void goto_symext::symex_function_call_code(
     {
       const auto rhs =
         side_effect_expr_nondett(call.lhs().type(), call.source_location());
-      code_assignt code(call.lhs(), rhs);
-      symex_assign(state, code);
+      symex_assign(state, call.lhs(), rhs);
     }
 
     if(symex_config.havoc_undefined_functions)

src/goto-symex/symex_main.cpp

@@ -667,7 +667,8 @@ void goto_symext::execute_next_instruction(
 
   case ASSIGN:
     if(state.reachable)
-      symex_assign(state, instruction.get_assign());
+      symex_assign(
+        state, instruction.get_assign().lhs(), instruction.get_assign().rhs());
 
     symex_transition(state);
     break;

src/goto-symex/symex_other.cpp

@@ -31,12 +31,10 @@ void goto_symext::havoc_rec(
       lhs=if_exprt(
         guard.as_expr(), dest, exprt(ID_null_object, dest.type()));
 
-    code_assignt assignment;
-    assignment.lhs()=lhs;
-    assignment.rhs() =
+    auto rhs =
       side_effect_expr_nondett(dest.type(), state.source.pc->source_location);
 
-    symex_assign(state, assignment);
+    symex_assign(state, lhs, rhs);
   }
   else if(dest.id()==ID_byte_extract_little_endian ||
           dest.id()==ID_byte_extract_big_endian)
@@ -167,8 +165,7 @@ void goto_symext::symex_other(
       }
     }
 
-    code_assignt assignment(dest_array, src_array);
-    symex_assign(state, assignment);
+    symex_assign(state, dest_array, src_array);
   }
   else if(statement==ID_array_set)
   {
@@ -211,8 +208,7 @@ void goto_symext::symex_other(
     if(array_type.subtype() != value.type())
       value = typecast_exprt(value, array_type.subtype());
 
-    code_assignt assignment(array_expr, array_of_exprt(value, array_type));
-    symex_assign(state, assignment);
+    symex_assign(state, array_expr, array_of_exprt(value, array_type));
   }
   else if(statement==ID_array_equal)
   {
@@ -236,13 +232,13 @@ void goto_symext::symex_other(
     process_array_expr(state, array1);
     process_array_expr(state, array2);
 
-    code_assignt assignment(code.op2(), equal_exprt(array1, array2));
+    exprt rhs = equal_exprt(array1, array2);
 
     // check for size (or type) mismatch
     if(array1.type() != array2.type())
-      assignment.rhs() = false_exprt();
+      rhs = false_exprt();
 
-    symex_assign(state, assignment);
+    symex_assign(state, code.op2(), rhs);
   }
   else if(statement==ID_user_specified_predicate ||
           statement==ID_user_specified_parameter_predicates ||