WIP Add regression test for struct with const members

Author: hannes-steffenhagen-diffblue

regression/goto-instrument/replace-function-body-struct-with-const-member/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+
+struct WithConstMember
+{
+  int non_const;
+  const int is_const;
+};
+
+struct WithConstMember globalStruct = {10, 20};
+void havoc_struct(struct WithConstMember *s);
+
+int main(void)
+{
+  struct WithConstMember paramStruct = {11, 21};
+  havoc_struct(&paramStruct);
+  assert(globalStruct.non_const == 10);
+  assert(globalStruct.is_const == 20);
+  assert(paramStruct.non_const == 11);
+  assert(paramStruct.is_const == 21);
+  return 0;
+}

regression/goto-instrument/replace-function-body-struct-with-const-member/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--replace-function-body 'havoc_struct' --replace-function-body-options 'havoc,params:.*,globals:(?!__).*'
+^SIGNAL=0$
+^EXIT=0$
+^VERIFICATION SUCCESSFUL$

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1452,8 +1452,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     cmdline.isset("replace-function-body") ||
     cmdline.isset("generate-function-body"))
   {
-    auto replace_options =
-      parse_replace_function_body_optionst(cmdline, goto_model.symbol_table);
+    auto replace_options = parse_replace_function_body_optionst(
+      cmdline, goto_model.symbol_table, *message_handler);
     status() << (replace_options.only_generate ? "Generating" : "Replacing")
              << " function bodies" << eom;
     replace_function_bodies(goto_model, replace_options, *message_handler);

src/goto-programs/replace_function_bodies.cpp

@@ -160,13 +160,17 @@ class empty_replace_function_bodiest : public replace_function_bodiest
   }
 };
 
-class havoc_replace_function_bodiest : public replace_function_bodiest
+class havoc_replace_function_bodiest : public replace_function_bodiest,
+                                       private messaget
 {
 public:
   havoc_replace_function_bodiest(
     std::vector<irep_idt> globals_to_havoc,
-    std::regex parameters_to_havoc)
-    : globals_to_havoc(std::move(globals_to_havoc)),
+    std::regex parameters_to_havoc,
+    message_handlert &message_handler)
+    : replace_function_bodiest(),
+      messaget(message_handler),
+      globals_to_havoc(std::move(globals_to_havoc)),
       parameters_to_havoc(std::move(parameters_to_havoc))
   {
   }
@@ -190,26 +194,35 @@ class havoc_replace_function_bodiest : public replace_function_bodiest
     {
       if(
         parameter.type().id() == ID_pointer &&
-        !is_constant_or_has_constant_components(
-          parameter.type().subtype(), ns) &&
         std::regex_match(
           id2string(parameter.get_base_name()), parameters_to_havoc))
       {
-        // if (param != nullptr) { *param = nondet(); }
-        auto goto_instruction = add_instruction();
-        auto assign_instruction = add_instruction();
-        auto label_instruction = add_instruction();
-        goto_instruction->make_goto(
-          label_instruction,
-          equal_exprt(
-            symbol_exprt(parameter.get_identifier(), parameter.type()),
-            null_pointer_exprt(to_pointer_type(parameter.type()))));
-        assign_instruction->make_assignment();
-        assign_instruction->code = code_assignt(
-          dereference_exprt(
-            symbol_exprt(parameter.get_identifier(), parameter.type())),
-          side_effect_expr_nondett(parameter.type().subtype()));
-        label_instruction->make_skip();
+        if(
+          !is_constant_or_has_constant_components(
+            parameter.type().subtype(), ns))
+        {
+          // if (param != nullptr) { *param = nondet(); }
+          auto goto_instruction = add_instruction();
+          auto assign_instruction = add_instruction();
+          auto label_instruction = add_instruction();
+          goto_instruction->make_goto(
+            label_instruction,
+            equal_exprt(
+              symbol_exprt(parameter.get_identifier(), parameter.type()),
+              null_pointer_exprt(to_pointer_type(parameter.type()))));
+          assign_instruction->make_assignment();
+          assign_instruction->code = code_assignt(
+            dereference_exprt(
+              symbol_exprt(parameter.get_identifier(), parameter.type())),
+            side_effect_expr_nondett(parameter.type().subtype()));
+          label_instruction->make_skip();
+        }
+        else if(!parameter.type().subtype().get_bool(ID_C_constant))
+        {
+          warning() << "warning: not havoccing non-const pointer parameter '"
+                    << parameter.get_base_name() << "' of " << function_name
+                    << " because it has const members" << messaget::eom;
+        }
       }
     }
 
@@ -249,12 +262,13 @@ class replace_function_bodies_errort : public std::runtime_error
 
 std::unique_ptr<replace_function_bodiest> replace_function_body_options_factory(
   const std::string &options,
-  const symbol_tablet &symbol_table)
+  const symbol_tablet &symbol_table,
+  message_handlert &message_handler)
 {
   if(options.empty() || options == "nondet-return")
   {
     return util_make_unique<havoc_replace_function_bodiest>(
-      std::vector<irep_idt>{}, std::regex{});
+      std::vector<irep_idt>{}, std::regex{}, message_handler);
   }
 
   if(options == "assume-false")
@@ -308,18 +322,27 @@ std::unique_ptr<replace_function_bodiest> replace_function_body_options_factory(
     }
     std::vector<irep_idt> globals_to_havoc;
     namespacet ns(symbol_table);
+    messaget messages(message_handler);
     for(auto const &symbol : symbol_table.symbols)
     {
       if(
         symbol.second.is_lvalue && symbol.second.is_static_lifetime &&
-        !is_constant_or_has_constant_components(symbol.second.type, ns) &&
         std::regex_match(id2string(symbol.first), globals_regex))
       {
-        globals_to_havoc.push_back(symbol.first);
+        if(!is_constant_or_has_constant_components(symbol.second.type, ns))
+        {
+          globals_to_havoc.push_back(symbol.first);
+        }
+        else if(!symbol.second.type.get_bool(ID_C_constant))
+        {
+          messages.warning() << "warning: not havoccing non-const global '"
+                             << symbol.first << "' because it has const members"
+                             << messaget::eom;
+        }
       }
     }
     return util_make_unique<havoc_replace_function_bodiest>(
-      std::move(globals_to_havoc), std::move(params_regex));
+      std::move(globals_to_havoc), std::move(params_regex), message_handler);
   }
   throw replace_function_bodies_errort("Can't parse \"" + options + "\"");
 }
@@ -328,7 +351,8 @@ std::unique_ptr<replace_function_bodiest> replace_function_body_options_factory(
 /// \see replace_function_bodies() for information of how the cmdline is parsed
 replace_function_body_optionst parse_replace_function_body_optionst(
   const cmdlinet &cmdline,
-  const symbol_tablet &symbol_table)
+  const symbol_tablet &symbol_table,
+  message_handlert &message_handler)
 {
   if(
     cmdline.isset("replace-function-body") &&
@@ -343,7 +367,9 @@ replace_function_body_optionst parse_replace_function_body_optionst(
     only_generate ? cmdline.get_value("generate-function-body")
                   : cmdline.get_value("replace-function-body"));
   auto replace_function_bodies = replace_function_body_options_factory(
-    cmdline.get_value("replace-function-body-options"), symbol_table);
+    cmdline.get_value("replace-function-body-options"),
+    symbol_table,
+    message_handler);
   return {function_regex, only_generate, std::move(replace_function_bodies)};
 }
 
@@ -430,7 +456,7 @@ void replace_function_bodies(
   {
     messaget messages(message_handler);
     messages.warning()
-      << "Replace function bodies: No function name matched regex"
+      << "warning: Replace function bodies: No function name matched regex"
       << messaget::eom;
   }
 }

src/goto-programs/replace_function_bodies.h

@@ -90,7 +90,8 @@ struct replace_function_body_optionst
 
 replace_function_body_optionst parse_replace_function_body_optionst(
   const cmdlinet &cmdline,
-  const symbol_tablet &symbol_table);
+  const symbol_tablet &symbol_table,
+  message_handlert &message_handler);
 
 void replace_function_bodies(
   goto_modelt &model,