Use c nondet object factory in function body generation

This removes the existing code in the function body generation for havoc-ing
objects (in havoc_expr_rec()) and replaces it with calls to the c nondet symbol
factory (gen_nondet_init()).

Author: danpoe

src/goto-instrument/generate_function_bodies.cpp

@@ -68,7 +68,7 @@ class assume_false_generate_function_bodiest : public generate_function_bodiest
 protected:
   void generate_function_body_impl(
     goto_functiont &function,
-    const symbol_tablet &symbol_table,
+    symbol_tablet &symbol_table,
     const irep_idt &function_name) const override
   {
     auto const &function_symbol = symbol_table.lookup_ref(function_name);
@@ -91,7 +91,7 @@ class assert_false_generate_function_bodiest : public generate_function_bodiest
 protected:
   void generate_function_body_impl(
     goto_functiont &function,
-    const symbol_tablet &symbol_table,
+    symbol_tablet &symbol_table,
     const irep_idt &function_name) const override
   {
     auto const &function_symbol = symbol_table.lookup_ref(function_name);
@@ -122,7 +122,7 @@ class assert_false_then_assume_false_generate_function_bodiest
 protected:
   void generate_function_body_impl(
     goto_functiont &function,
-    const symbol_tablet &symbol_table,
+    symbol_tablet &symbol_table,
     const irep_idt &function_name) const override
   {
     auto const &function_symbol = symbol_table.lookup_ref(function_name);
@@ -150,8 +150,7 @@ class assert_false_then_assume_false_generate_function_bodiest
   }
 };
 
-class havoc_generate_function_bodiest : public generate_function_bodiest,
-                                        private messaget
+class havoc_generate_function_bodiest : public generate_function_bodiest
 {
 public:
   havoc_generate_function_bodiest(
@@ -160,107 +159,52 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
     const c_object_factory_parameterst &object_factory_parameters,
     message_handlert &message_handler)
     : generate_function_bodiest(),
-      messaget(message_handler),
       globals_to_havoc(std::move(globals_to_havoc)),
       parameters_to_havoc(std::move(parameters_to_havoc)),
-      object_factory_parameters(object_factory_parameters)
+      object_factory_parameters(object_factory_parameters),
+      message(message_handler)
   {
   }
 
 private:
   void havoc_expr_rec(
     const exprt &lhs,
-    const namespacet &ns,
-    const std::function<goto_programt::targett(void)> &add_instruction,
-    const irep_idt &function_name) const
+    const std::size_t initial_depth,
+    const source_locationt &source_location,
+    symbol_tablet &symbol_table,
+    goto_programt &dest) const
   {
-    // resolve type symbols
-    auto const lhs_type = ns.follow(lhs.type());
-    // skip constants
-    if(!lhs_type.get_bool(ID_C_constant))
-    {
-      // expand arrays, structs and union, everything else gets
-      // assigned nondet
-      if(lhs_type.id() == ID_struct || lhs_type.id() == ID_union)
-      {
-        // Note: In the case of unions it's often enough to assign
-        // just one member; However consider a case like
-        // union { struct { const int x; int y; } a;
-        //         struct {  int x; const int y; } b;};
-        // in this case both a.y and b.x must be assigned
-        // otherwise these parts stay constant even though
-        // they could've changed (note that type punning through
-        // unions is allowed in the C standard but forbidden in C++)
-        // so we're assigning all members even in the case of
-        // unions just to be safe
-        auto const lhs_struct_type = to_struct_union_type(lhs_type);
-        for(auto const &component : lhs_struct_type.components())
-        {
-          havoc_expr_rec(
-            member_exprt(lhs, component.get_name(), component.type()),
-            ns,
-            add_instruction,
-            function_name);
-        }
-      }
-      else if(lhs_type.id() == ID_array)
-      {
-        auto const lhs_array_type = to_array_type(lhs_type);
-        if(!lhs_array_type.subtype().get_bool(ID_C_constant))
-        {
-          bool constant_known_array_size = lhs_array_type.size().is_constant();
-          if(!constant_known_array_size)
-          {
-            warning() << "Cannot havoc non-const array " << format(lhs)
-                      << " in function " << function_name
-                      << ": Unknown array size" << eom;
-          }
-          else
-          {
-            auto const array_size =
-              numeric_cast<mp_integer>(lhs_array_type.size());
-            INVARIANT(
-              array_size.has_value(),
-              "Array size should be known constant integer");
-            if(array_size.value() == 0)
-            {
-              // Pretty much the same thing as a unknown size array
-              // Technically not allowed by the C standard, but we model
-              // unknown size arrays in structs this way
-              warning() << "Cannot havoc non-const array " << format(lhs)
-                        << " in function " << function_name << ": Array size 0"
-                        << eom;
-            }
-            else
-            {
-              for(mp_integer i = 0; i < array_size.value(); ++i)
-              {
-                auto const index =
-                  from_integer(i, lhs_array_type.size().type());
-                havoc_expr_rec(
-                  index_exprt(lhs, index, lhs_array_type.subtype()),
-                  ns,
-                  add_instruction,
-                  function_name);
-              }
-            }
-          }
-        }
-      }
-      else
-      {
-        auto assign_instruction = add_instruction();
-        assign_instruction->make_assignment(
-          code_assignt(
-            lhs, side_effect_expr_nondett(lhs_type, lhs.source_location())));
-      }
-    }
+    symbol_factoryt symbol_factory(
+      symbol_table,
+      source_location,
+      object_factory_parameters,
+      lifetimet::DYNAMIC);
+
+    code_blockt assignments;
+
+    symbol_factory.gen_nondet_init(
+      assignments,
+      lhs,
+      initial_depth,
+      symbol_factoryt::recursion_sett(),
+      false); // do not initialize const objects at the top level
+
+    code_blockt init_code;
+
+    symbol_factory.declare_created_symbols(init_code);
+    init_code.append(assignments);
+
+    goto_programt tmp_dest;
+    goto_convert(
+      init_code, symbol_table, tmp_dest, message.get_message_handler(), ID_C);
+
+    dest.destructive_append(tmp_dest);
   }
 
 protected:
   void generate_function_body_impl(
     goto_functiont &function,
-    const symbol_tablet &symbol_table,
+    symbol_tablet &symbol_table,
     const irep_idt &function_name) const override
   {
     auto const &function_symbol = symbol_table.lookup_ref(function_name);
@@ -276,18 +220,29 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
     {
       if(
         parameter.type().id() == ID_pointer &&
+        !parameter.type().subtype().get_bool(ID_C_constant) &&
         std::regex_match(
           id2string(parameter.get_base_name()), parameters_to_havoc))
       {
-        // if (param != nullptr) { *param = nondet(); }
         auto goto_instruction = add_instruction();
+
+        const irep_idt base_name = parameter.get_base_name();
+        CHECK_RETURN(!base_name.empty());
+
+        dereference_exprt dereference_expr(
+          symbol_exprt(parameter.get_identifier(), parameter.type()),
+          parameter.type().subtype());
+
+        goto_programt dest;
         havoc_expr_rec(
-          dereference_exprt(
-            symbol_exprt(parameter.get_identifier(), parameter.type()),
-            parameter.type().subtype()),
-          ns,
-          add_instruction,
-          function_name);
+          dereference_expr,
+          1, // depth 1 since we pass the dereferenced pointer
+          function_symbol.location,
+          symbol_table,
+          dest);
+
+        function.body.destructive_append(dest);
+
         auto label_instruction = add_instruction();
         goto_instruction->make_goto(
           label_instruction,
@@ -301,12 +256,19 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
     for(auto const &global_id : globals_to_havoc)
     {
       auto const &global_sym = symbol_table.lookup_ref(global_id);
+
+      goto_programt dest;
+
       havoc_expr_rec(
         symbol_exprt(global_sym.name, global_sym.type),
-        ns,
-        add_instruction,
-        function_name);
+        0,
+        function_symbol.location,
+        symbol_table,
+        dest);
+
+      function.body.destructive_append(dest);
     }
+
     if(function.type.return_type() != void_typet())
     {
       auto return_instruction = add_instruction();
@@ -324,6 +286,7 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
   const std::vector<irep_idt> globals_to_havoc;
   std::regex parameters_to_havoc;
   const c_object_factory_parameterst &object_factory_parameters;
+  mutable messaget message;
 };
 
 class generate_function_bodies_errort : public std::runtime_error

src/goto-instrument/generate_function_bodies.h

@@ -32,7 +32,7 @@ class generate_function_bodiest
   /// \param function_name: Identifier of function
   virtual void generate_function_body_impl(
     goto_functiont &function,
-    const symbol_tablet &symbol_table,
+    symbol_tablet &symbol_table,
     const irep_idt &function_name) const = 0;
 
 public: