From ab938902230026ff5c0da9623721c5f2fe10d5bd Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 1 Feb 2024 12:42:41 +0000
Subject: [PATCH] argc/argv modelling: argument string must remain in scope

We previously produced an argument string that was marked DEAD before
entering main, making accesses to argv[i] ones to a dead object.
---
 regression/goto-instrument/argc-argv1/main.c |  4 ++++
 src/goto-instrument/dump_c.cpp               | 10 +++++++---
 src/goto-instrument/model_argc_argv.cpp      | 15 ++++++++++-----
 3 files changed, 21 insertions(+), 8 deletions(-)

diff --git a/regression/goto-instrument/argc-argv1/main.c b/regression/goto-instrument/argc-argv1/main.c
index 73fa03e3e52..9c233f4b5a5 100644
--- a/regression/goto-instrument/argc-argv1/main.c
+++ b/regression/goto-instrument/argc-argv1/main.c
@@ -3,7 +3,11 @@
 int main(int argc, char* argv[])
 {
   if(argc>=2)
+  {
     assert(argv[1]!=0);
+    // we can access at least one character (might be a string-terminating zero)
+    char first_char = *argv[1];
+  }
 
   return 0;
 }
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index e1bc37c9509..6cca3e3952f 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -208,10 +208,14 @@ void dump_ct::operator()(std::ostream &os)
 
     // we don't want to dump in full all definitions; in particular
     // do not dump anonymous types that are defined in system headers
-    if((!tag_added || symbol.is_type) &&
-       system_symbols.is_symbol_internal_symbol(symbol, system_headers) &&
-       symbol.name!=goto_functions.entry_point())
+    if(
+      (!tag_added || symbol.is_type) &&
+      system_symbols.is_symbol_internal_symbol(symbol, system_headers) &&
+      symbol.name != goto_functions.entry_point() &&
+      symbol.name != CPROVER_PREFIX "arg_string") // model for argc/argv
+    {
       continue;
+    }
 
     bool inserted=symbols_sorted.insert(name_str).second;
     CHECK_RETURN(inserted);
diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp
index 1875f2e2495..70d9e209208 100644
--- a/src/goto-instrument/model_argc_argv.cpp
+++ b/src/goto-instrument/model_argc_argv.cpp
@@ -85,20 +85,22 @@ bool model_argc_argv(
   std::ostringstream oss;
   oss << "int ARGC;\n"
       << "char *ARGV[1];\n"
+      << "extern char " CPROVER_PREFIX "arg_string[4096];\n"
       << "void " << goto_model.goto_functions.entry_point() << "()\n"
       << "{\n"
       << "  unsigned next=0u;\n"
       << "  " CPROVER_PREFIX "assume(ARGC>=1);\n"
       << "  " CPROVER_PREFIX "assume(ARGC<=" << max_argc << ");\n"
-      << "  char arg_string[4096];\n"
-      << "  " CPROVER_PREFIX "input(\"arg_string\", &arg_string[0]);\n"
+      << "  " CPROVER_PREFIX "input(\"arg_string\", \n"
+      << "    &" CPROVER_PREFIX "arg_string[0]);\n"
       << "  for(int i=0; i<ARGC && i<" << max_argc << "; ++i)\n"
       << "  {\n"
       << "    unsigned len;\n"
       << "    " CPROVER_PREFIX "assume(len<4096);\n"
       << "    " CPROVER_PREFIX "assume(next+len<4096);\n"
-      << "    " CPROVER_PREFIX "assume(arg_string[next+len]==0);\n"
-      << "    ARGV[i]=&(arg_string[next]);\n"
+      << "    " CPROVER_PREFIX "assume(\n"
+      << "       " CPROVER_PREFIX "arg_string[next+len]==0);\n"
+      << "    ARGV[i]=&(" CPROVER_PREFIX "arg_string[next]);\n"
       << "    next+=len+1;\n"
       << "  }\n"
       << "}";
@@ -124,8 +126,11 @@ bool model_argc_argv(
     // add __CPROVER_assume if necessary (it might exist already)
     if(
       symbol_pair.first == CPROVER_PREFIX "assume" ||
-      symbol_pair.first == CPROVER_PREFIX "input")
+      symbol_pair.first == CPROVER_PREFIX "input" ||
+      symbol_pair.first == CPROVER_PREFIX "arg_string")
+    {
       goto_model.symbol_table.add(symbol_pair.second);
+    }
     else if(symbol_pair.first == goto_model.goto_functions.entry_point())
     {
       value = symbol_pair.second.value;