Cumulative fix

Based on comments. Will be squashed.

Author: Petr Bauch

regression/snapshot-harness/pointer-to-array-char/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 first,second,array_size --harness-type initialise-with-memory-snapshot --initial-location main:4
 ^SIGNAL=0$

regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 first,second,string_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-location main:4 --havoc-variables prefix,prefix_size --size-of-array prefix:prefix_size --max-array-size 5
 ^SIGNAL=0$

src/goto-harness/function_call_harness_generator.cpp

@@ -95,6 +95,7 @@ void function_call_harness_generatort::handle_option(
 
   if(p_impl->recursive_initialization_config.handle_option(option, values))
   {
+    // the option belongs to recursive initialization
   }
   else if(option == FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT)
   {

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -25,6 +25,8 @@ Author: Daniel Poetzl
 
 #include <linking/static_lifetime_init.h>
 
+#include <algorithm>
+
 void memory_snapshot_harness_generatort::handle_option(
   const std::string &option,
   const std::list<std::string> &values)
@@ -33,6 +35,7 @@ void memory_snapshot_harness_generatort::handle_option(
     harness_options_parsert::require_exactly_one_value;
   if(recursive_initialization_config.handle_option(option, values))
   {
+    // the option belongs to recursive initialization
   }
   else if(option == MEMORY_SNAPSHOT_HARNESS_TREAT_POINTER_AS_ARRAY_OPT)
   {
@@ -103,7 +106,12 @@ void memory_snapshot_harness_generatort::handle_option(
   }
   else if(option == MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT)
   {
-    variables_to_havoc.insert(values.begin(), values.end());
+    std::vector<std::string> havoc_candidates;
+    split_string(values.front(), ',', havoc_candidates, true);
+    for(const auto &candidate : havoc_candidates)
+    {
+      variables_to_havoc.insert(candidate);
+    }
   }
   else
   {
@@ -256,20 +264,50 @@ const symbolt &memory_snapshot_harness_generatort::fresh_symbol_copy(
     snapshot_symbol.mode,
     symbol_table);
   tmp_symbol.is_static_lifetime = true;
+  tmp_symbol.is_auxiliary = false;
   tmp_symbol.value = snapshot_symbol.value;
 
   return tmp_symbol;
 }
 
+size_t memory_snapshot_harness_generatort::pointer_depth(const typet &t) const
+{
+  if(t.id() != ID_pointer)
+    return 0;
+  else
+    return pointer_depth(t.subtype()) + 1;
+}
+
 code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
   const symbol_tablet &snapshot,
   goto_modelt &goto_model) const
 {
   recursive_initializationt recursive_initialization{
     recursive_initialization_config, goto_model};
 
+  using snapshot_pairt = std::pair<irep_idt, symbolt>;
+  std::vector<snapshot_pairt> ordered_snapshot_symbols;
+  for(auto pair : snapshot)
+  {
+    const auto name = id2string(pair.first);
+    if(name.find(CPROVER_PREFIX) != 0)
+      ordered_snapshot_symbols.push_back(pair);
+  }
+
+  // sort the snapshot symbols so that the non-pointer symbols are first, then
+  // pointers, then pointers-to-pointers, etc. so that we don't assign
+  // uninitialized values
+  std::stable_sort(
+    ordered_snapshot_symbols.begin(),
+    ordered_snapshot_symbols.end(),
+    [this](const snapshot_pairt &left, const snapshot_pairt &right) {
+      return pointer_depth(left.second.symbol_expr().type()) <
+             pointer_depth(right.second.symbol_expr().type());
+    });
+
   code_blockt code;
-  for(const auto &pair : snapshot)
+  //  for(const auto &pair : snapshot)
+  for(const auto &pair : ordered_snapshot_symbols)
   {
     const symbolt &snapshot_symbol = pair.second;
     symbol_tablet &symbol_table = goto_model.symbol_table;

src/goto-harness/memory_snapshot_harness_generator.h

@@ -138,6 +138,11 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
     goto_modelt &goto_model,
     const symbolt &function) const;
 
+  /// Recursively compute the pointer depth
+  /// \param t: input type
+  /// \return pointer depth of type \p t
+  size_t pointer_depth(const typet &t) const;
+
   std::string memory_snapshot_file;
 
   irep_idt entry_function_name;

src/goto-harness/recursive_initialization.cpp

@@ -20,6 +20,59 @@ Author: Diffblue Ltd.
 
 #include <functional>
 
+bool recursive_initialization_configt::handle_option(
+  const std::string &option,
+  const std::list<std::string> &values)
+{
+  if(option == COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT)
+  {
+    auto const value = require_exactly_one_value(option, values);
+    auto const user_min_null_tree_depth =
+      string2optional<std::size_t>(value, 10);
+    if(user_min_null_tree_depth.has_value())
+    {
+      min_null_tree_depth = user_min_null_tree_depth.value();
+    }
+    else
+    {
+      throw invalid_command_line_argument_exceptiont{
+        "failed to convert `" + value + "' to integer",
+        "--" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT};
+    }
+    return true;
+  }
+  else if(option == COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT)
+  {
+    auto const value = require_exactly_one_value(option, values);
+    auto const user_max_nondet_tree_depth =
+      string2optional<std::size_t>(value, 10);
+    if(user_max_nondet_tree_depth.has_value())
+    {
+      max_nondet_tree_depth = user_max_nondet_tree_depth.value();
+    }
+    else
+    {
+      throw invalid_command_line_argument_exceptiont{
+        "failed to convert `" + value + "' to integer",
+        "--" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT};
+    }
+    return true;
+  }
+  else if(option == COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT)
+  {
+    max_dynamic_array_size = require_one_size_value(
+      COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT, values);
+    return true;
+  }
+  else if(option == COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT)
+  {
+    min_dynamic_array_size = require_one_size_value(
+      COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT, values);
+    return true;
+  }
+  return false;
+}
+
 recursive_initializationt::recursive_initializationt(
   recursive_initialization_configt initialization_config,
   goto_modelt &goto_model)
@@ -416,56 +469,3 @@ recursive_initializationt::cstring_member_initialization()
     }
   };
 }
-
-bool recursive_initialization_configt::handle_option(
-  const std::string &option,
-  const std::list<std::string> &values)
-{
-  if(option == COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT)
-  {
-    auto const value = require_exactly_one_value(option, values);
-    auto const user_min_null_tree_depth =
-      string2optional<std::size_t>(value, 10);
-    if(user_min_null_tree_depth.has_value())
-    {
-      min_null_tree_depth = user_min_null_tree_depth.value();
-    }
-    else
-    {
-      throw invalid_command_line_argument_exceptiont{
-        "failed to convert `" + value + "' to integer",
-        "--" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT};
-    }
-    return true;
-  }
-  else if(option == COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT)
-  {
-    auto const value = require_exactly_one_value(option, values);
-    auto const user_max_nondet_tree_depth =
-      string2optional<std::size_t>(value, 10);
-    if(user_max_nondet_tree_depth.has_value())
-    {
-      max_nondet_tree_depth = user_max_nondet_tree_depth.value();
-    }
-    else
-    {
-      throw invalid_command_line_argument_exceptiont{
-        "failed to convert `" + value + "' to integer",
-        "--" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT};
-    }
-    return true;
-  }
-  else if(option == COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT)
-  {
-    max_dynamic_array_size = require_one_size_value(
-      COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT, values);
-    return true;
-  }
-  else if(option == COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT)
-  {
-    min_dynamic_array_size = require_one_size_value(
-      COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT, values);
-    return true;
-  }
-  return false;
-}

src/goto-harness/recursive_initialization.h

@@ -39,6 +39,11 @@ struct recursive_initialization_configt : harness_options_parsert
 
   std::string to_string() const; // for debugging purposes
 
+  /// Parse the options specific for recursive initialisation
+  /// \param option: the user option name
+  /// \param values: the (one-or-more) values for this option
+  /// \return true if the option belonged to recursive initialisation and was
+  /// successfully parsed here
   bool handle_option(
     const std::string &option,
     const std::list<std::string> &values);

src/memory-analyzer/analyze_symbol.cpp

@@ -186,10 +186,13 @@ exprt symbol_analyzert::get_char_pointer_value(
 
     values.insert(std::make_pair(memory_location, new_symbol));
 
+    // check that we are returning objects of the right type
+    CHECK_RETURN(new_symbol.type().subtype() == expr.type().subtype());
     return new_symbol;
   }
   else
   {
+    CHECK_RETURN(it->second.type().subtype() == expr.type().subtype());
     return it->second;
   }
 }
@@ -200,7 +203,6 @@ exprt symbol_analyzert::get_pointer_to_member_value(
   const source_locationt &location)
 {
   PRECONDITION(expr.type().id() == ID_pointer);
-  PRECONDITION(!is_c_char(expr.type().subtype()));
   std::string memory_location = pointer_value.address;
   PRECONDITION(memory_location != "0x0");
   PRECONDITION(!pointer_value.pointee.empty());
@@ -221,14 +223,17 @@ exprt symbol_analyzert::get_pointer_to_member_value(
   }
 
   const symbolt *struct_symbol = symbol_table.lookup(struct_name);
+
   DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
 
   const auto maybe_member_expr = get_subexpression_at_offset(
     struct_symbol->symbol_expr(), member_offset, expr.type().subtype(), ns);
-  if(maybe_member_expr.has_value())
-    return *maybe_member_expr;
+  DATA_INVARIANT(
+    maybe_member_expr.has_value(), "structure doesn't have member");
 
-  UNREACHABLE;
+  // check that we return the right type
+  CHECK_RETURN(maybe_member_expr->type() == expr.type().subtype());
+  return *maybe_member_expr;
 }
 
 exprt symbol_analyzert::get_non_char_pointer_value(
@@ -315,7 +320,44 @@ exprt symbol_analyzert::get_pointer_value(
   {
     if(is_c_char(expr.type().subtype()))
     {
-      return get_char_pointer_value(expr, memory_location, location);
+      // pointers-to-char can point to members as well, e.g. char[]
+      if(points_to_member(value))
+      {
+        const auto target_expr =
+          get_pointer_to_member_value(expr, value, location);
+        if(target_expr.id() == ID_nil)
+        {
+          outstanding_assignments[expr] = memory_location;
+        }
+        else
+        {
+          const auto result_expr = address_of_exprt(target_expr);
+          CHECK_RETURN(result_expr.type() == zero_expr.type());
+          return result_expr;
+        }
+      }
+      INVARIANT(
+        !points_to_member(value),
+        "pointers-to-char shouldn't point to members");
+      const auto result_pointee_expr =
+        get_char_pointer_value(expr, memory_location, location);
+
+      // the pointee was (probably) dynamically allocated (but the allocation
+      // would not be visible in the snapshot) so we pretend it is statically
+      // allocated (we have the value) and return address to the first element
+      // of the array (instead of the array as char*)
+      if(result_pointee_expr.type().id() == ID_array)
+      {
+        const auto result_indexed_expr = get_subexpression_at_offset(
+          result_pointee_expr, 0, zero_expr.type().subtype(), ns);
+        CHECK_RETURN(result_indexed_expr.has_value());
+        const auto result_expr = address_of_exprt{*result_indexed_expr};
+        return result_expr;
+      }
+      // cast to expected type to prevent symex assign check failing
+      const auto maybe_cast_result =
+        typecast_exprt::conditional_cast(result_pointee_expr, zero_expr.type());
+      return maybe_cast_result;
     }
     else
     {
@@ -388,7 +430,15 @@ exprt symbol_analyzert::get_expr_value(
   {
     INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
 
-    return zero_expr; // currently left at 0
+    // check the char-value and return as bitvector-type value
+    std::string c_expr = c_converter.convert(expr);
+    const std::string value = gdb_api.get_value(c_expr);
+
+    if(value.empty())
+      return zero_expr;
+
+    const mp_integer int_rep = value[0];
+    return from_integer(int_rep, type);
   }
   else if(type.id() == ID_c_bool)
   {