Merge pull request #5833 from thomasspriggs/tas/format_initialisation

Bug fix using `format` function on `code_declt` containing initialization

Author: thomasspriggs

src/goto-instrument/dump_c.cpp

@@ -650,19 +650,14 @@ void dump_ct::cleanup_decl(
   std::list<irep_idt> &local_static,
   std::list<irep_idt> &local_type_decls)
 {
-  exprt value=nil_exprt();
-
-  if(decl.operands().size()==2)
-  {
-    value=decl.op1();
-    decl.operands().resize(1);
-  }
-
   goto_programt tmp;
   tmp.add(goto_programt::make_decl(decl.symbol()));
 
-  if(value.is_not_nil())
-    tmp.add(goto_programt::make_assignment(decl.symbol(), value));
+  if(optionalt<exprt> value = decl.initial_value())
+  {
+    decl.set_initial_value({});
+    tmp.add(goto_programt::make_assignment(decl.symbol(), std::move(*value)));
+  }
 
   tmp.add(goto_programt::make_end_function());
 

src/goto-instrument/goto_program2code.cpp

@@ -477,7 +477,7 @@ goto_programt::const_targett goto_program2codet::convert_decl(
     {
       if(next->is_assign())
       {
-        d.copy_to_operands(next->get_assign().rhs());
+        d.set_initial_value({next->get_assign().rhs()});
       }
       else
       {

src/goto-programs/goto_program.h

@@ -199,13 +199,21 @@ class goto_programt
     const code_declt &get_decl() const
     {
       PRECONDITION(is_decl());
-      return to_code_decl(code);
+      const auto &decl = expr_checked_cast<code_declt>(code);
+      INVARIANT(
+        !decl.initial_value(),
+        "code_declt in goto program may not contain initialization.");
+      return decl;
     }
 
     /// Set the declaration for DECL
     void set_decl(code_declt c)
     {
       PRECONDITION(is_decl());
+      INVARIANT(
+        !c.initial_value(),
+        "Initialization must be separated from code_declt before adding to "
+        "goto_instructiont.");
       code = std::move(c);
     }
 

src/goto-programs/wp.cpp

@@ -226,6 +226,7 @@ exprt wp_decl(
   const exprt &post,
   const namespacet &ns)
 {
+  PRECONDITION(!code.initial_value());
   // Model decl(var) as var = nondet()
   const exprt &var = code.symbol();
   side_effect_expr_nondett nondet(var.type(), source_locationt());

src/util/format_expr.cpp

@@ -422,11 +422,14 @@ void format_expr_configt::setup()
     {
       return os << "dead " << format(to_code_dead(code).symbol()) << ";";
     }
-    else if(statement == ID_decl)
+    else if(const auto decl = expr_try_dynamic_cast<code_declt>(code))
     {
-      const auto &declaration_symb = to_code_decl(code).symbol();
-      return os << "decl " << format(declaration_symb.type()) << " "
-                << format(declaration_symb) << ";";
+      const auto &declaration_symb = decl->symbol();
+      os << "decl " << format(declaration_symb.type()) << " "
+         << format(declaration_symb);
+      if(const optionalt<exprt> initial_value = decl->initial_value())
+        os << " = " << format(*initial_value);
+      return os << ";";
     }
     else if(statement == ID_function_call)
     {

src/util/std_code.h

@@ -420,6 +420,38 @@ class code_declt:public codet
     return symbol().get_identifier();
   }
 
+  /// Returns the initial value to which the declared variable is initialized,
+  /// or empty in the case where no initialisation is included.
+  /// \note: Initial values may be present in the front end but they must be
+  ///   separated into a separate assignment when used in a `goto_instructiont`.
+  optionalt<exprt> initial_value() const
+  {
+    if(operands().size() < 2)
+      return {};
+    return {op1()};
+  }
+
+  /// Sets the value to which this declaration initializes the declared
+  /// variable. Empty optional maybe passed to remove existing initialisation.
+  /// \note: Initial values may be present in the front end but they must be
+  ///   separated into a separate assignment when used in a `goto_instructiont`.
+  void set_initial_value(optionalt<exprt> initial_value)
+  {
+    if(!initial_value)
+    {
+      operands().resize(1);
+    }
+    else if(operands().size() < 2)
+    {
+      PRECONDITION(operands().size() == 1);
+      add_to_operands(std::move(*initial_value));
+    }
+    else
+    {
+      op1() = std::move(*initial_value);
+    }
+  }
+
   static void check(
     const codet &code,
     const validation_modet vm = validation_modet::INVARIANT)

unit/Makefile

@@ -90,6 +90,7 @@ SRC += analyses/ai/ai.cpp \
        util/expr.cpp \
        util/expr_iterator.cpp \
        util/file_util.cpp \
+       util/format.cpp \
        util/format_number_range.cpp \
        util/get_base_name.cpp \
        util/graph.cpp \

unit/util/format.cpp

@@ -0,0 +1,22 @@
+/*******************************************************************\
+
+ Module: Unit tests for `format` function.
+
+ Author: DiffBlue Limited.
+
+\*******************************************************************/
+
+#include <util/format.h>
+#include <util/format_expr.h>
+#include <util/std_code.h>
+
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("Format a declaration statement.", "[core][util][format]")
+{
+  const signedbv_typet int_type{32};
+  code_declt declaration{symbol_exprt{"foo", int_type}};
+  REQUIRE(format_to_string(declaration) == "decl signedbv[32] foo;");
+  declaration.set_initial_value({int_type.zero_expr()});
+  REQUIRE(format_to_string(declaration) == "decl signedbv[32] foo = 0;");
+}