Initialize shadow memory for string constants

or static variables.

Author: peterschrammel

src/goto-symex/symex_assign.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/byte_operators.h>
 #include <util/expr_util.h>
+#include <util/pointer_expr.h>
 #include <util/range.h>
 
 #include "expr_skeleton.h"
@@ -33,6 +34,27 @@ constexpr bool use_update()
 #endif
 }
 
+/// Determine whether the RHS expression is a string constant initialization
+/// \param rhs The RHS expression
+/// \return True if the expression points to the first character of a string
+///    constant
+static bool is_string_constant_initialization(const exprt &rhs)
+{
+  if(const auto &address_of = expr_try_dynamic_cast<address_of_exprt>(rhs))
+  {
+    if(
+      const auto &index =
+        expr_try_dynamic_cast<index_exprt>(address_of->object()))
+    {
+      if(index->array().id() == ID_string_constant && index->index().is_zero())
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
 void symex_assignt::assign_rec(
   const exprt &lhs,
   const expr_skeletont &full_lhs,
@@ -42,6 +64,21 @@ void symex_assignt::assign_rec(
   if(is_ssa_expr(lhs))
   {
     assign_symbol(to_ssa_expr(lhs), full_lhs, rhs, guard);
+
+    // Allocate shadow memory
+    if(shadow_memory.has_value())
+    {
+      bool is_string_constant_init = is_string_constant_initialization(rhs);
+      if(is_string_constant_init)
+      {
+        shadow_memory->symex_field_static_init_string_constant(
+          state, to_ssa_expr(lhs), rhs);
+      }
+      else
+      {
+        shadow_memory->symex_field_static_init(state, to_ssa_expr(lhs));
+      }
+    }
   }
   else if(lhs.id() == ID_index)
     assign_array<use_update()>(to_index_expr(lhs), full_lhs, rhs, guard);