dump-c: output a generated environment via --harness

dump-c previously would not print __CPROVER__start code as this is deemed
tool-internal. With increasing support for test-harness construction, the
harness code may be of interest to users, who may wish to tweak and use re-use
it.

Author: tautschnig

CHANGELOG

@@ -7,6 +7,7 @@
 * GOTO-INSTRUMENT: New option --print-path-lenghts
 * GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions
 * GOTO-INSTRUMENT: New option --undefined-function-is-assume-false
+* GOTO-INSTRUMENT: dump-c can output the generated environment via --harness
 
 
 5.7

regression/goto-instrument/harness1/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main(int argc, char* argv[])
+{
+  assert(argc<2 || argv[1]!=0);
+
+  return 0;
+}

regression/goto-instrument/harness1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--model-argc-argv 3 --dump-c --harness
+^EXIT=0$
+^SIGNAL=0$
+Adding up to 3 command line arguments
+--
+^warning: ignoring

src/clobber/clobber_parse_options.cpp

@@ -190,7 +190,7 @@ int clobber_parse_optionst::doit()
     if(!out)
       throw std::string("failed to create file simulator.c");
 
-    dump_c(goto_functions, true, ns, out);
+    dump_c(goto_functions, true, false, ns, out);
 
     status() << "instrumentation complete; compile and execute simulator.c"
              << eom;

src/goto-instrument/dump_c.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/find_symbols.h>
 #include <util/base_type.h>
 #include <util/cprover_prefix.h>
+#include <util/replace_symbol.h>
 
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
@@ -163,7 +164,9 @@ void dump_ct::operator()(std::ostream &os)
     }
 
     // we don't want to dump in full all definitions
-    if(!tag_added && ignore(symbol))
+    if(!tag_added &&
+       ignore(symbol) &&
+       symbol.name!=goto_functions.entry_point())
       continue;
 
     if(!symbols_sorted.insert(name_str).second)
@@ -206,7 +209,8 @@ void dump_ct::operator()(std::ostream &os)
       goto_functionst::function_mapt::const_iterator func_entry=
         goto_functions.function_map.find(symbol.name);
 
-      if(func_entry!=goto_functions.function_map.end() &&
+      if(!harness &&
+         func_entry!=goto_functions.function_map.end() &&
          func_entry->second.body_available() &&
          (symbol.name==ID_main ||
           (!config.main.empty() && symbol.name==config.main)))
@@ -990,6 +994,73 @@ void dump_ct::convert_global_variable(
 
 /*******************************************************************\
 
+Function: dump_ct::cleanup_harness
+
+Inputs: b  Code block to be cleaned
+
+Outputs:
+
+Purpose: Replace CPROVER internal symbols in b by printable values and
+         generate necessary declarations.
+
+\*******************************************************************/
+
+void dump_ct::cleanup_harness(code_blockt &b)
+{
+  replace_symbolt replace;
+  code_blockt decls;
+
+  const symbolt *argc_sym=nullptr;
+  if(!ns.lookup("argc'", argc_sym))
+  {
+    symbol_exprt argc("argc", argc_sym->type);
+    replace.insert(argc_sym->name, argc);
+    code_declt d(argc);
+    decls.add(d);
+  }
+  const symbolt *argv_sym=nullptr;
+  if(!ns.lookup("argv'", argv_sym))
+  {
+    symbol_exprt argv("argv", argv_sym->type);
+    replace.insert(argv_sym->name, argv);
+    code_declt d(argv);
+    decls.add(d);
+  }
+  const symbolt *return_sym=nullptr;
+  if(!ns.lookup("return'", return_sym))
+  {
+    symbol_exprt return_value("return_value", return_sym->type);
+    replace.insert(return_sym->name, return_value);
+    code_declt d(return_value);
+    decls.add(d);
+  }
+
+  Forall_operands(it, b)
+  {
+    codet &code=to_code(*it);
+
+    if(code.get_statement()==ID_function_call)
+    {
+      exprt &func=to_code_function_call(code).function();
+      if(func.id()==ID_symbol)
+      {
+        symbol_exprt &s=to_symbol_expr(func);
+        if(s.get_identifier()==ID_main)
+          s.set_identifier(CPROVER_PREFIX+id2string(ID_main));
+        else if(s.get_identifier()==CPROVER_PREFIX "initialize")
+          continue;
+      }
+    }
+
+    decls.add(code);
+  }
+
+  b.swap(decls);
+  replace(b);
+}
+
+/*******************************************************************\
+
 Function: dump_ct::convert_function_declarations
 
 Inputs:
@@ -1050,9 +1121,20 @@ void dump_ct::convert_function_declaration(
     converted_enum.swap(converted_e_bak);
     converted_compound.swap(converted_c_bak);
 
+    if(harness && symbol.name==goto_functions.entry_point())
+      cleanup_harness(b);
+
     os_body << "// " << symbol.name << std::endl;
     os_body << "// " << symbol.location << std::endl;
-    os_body << make_decl(symbol.name, symbol.type) << std::endl;
+    if(symbol.name==goto_functions.entry_point())
+      os_body << make_decl(ID_main, symbol.type) << std::endl;
+    else if(!harness || symbol.name!=ID_main)
+      os_body << make_decl(symbol.name, symbol.type) << std::endl;
+    else if(harness && symbol.name==ID_main)
+    {
+      os_body << make_decl(CPROVER_PREFIX+id2string(symbol.name), symbol.type)
+              << std::endl;
+    }
     os_body << expr_to_string(b);
     os_body << std::endl << std::endl;
 
@@ -1066,6 +1148,13 @@ void dump_ct::convert_function_declaration(
     os_decl << "// " << symbol.location << std::endl;
     os_decl << make_decl(symbol.name, symbol.type) << ";" << std::endl;
   }
+  else if(harness && symbol.name==ID_main)
+  {
+    os_decl << "// " << symbol.name << std::endl;
+    os_decl << "// " << symbol.location << std::endl;
+    os_decl << make_decl(CPROVER_PREFIX+id2string(symbol.name), symbol.type)
+            << ";" << std::endl;
+  }
 }
 
 /*******************************************************************\
@@ -1507,10 +1596,12 @@ Function: dump_c
 void dump_c(
   const goto_functionst &src,
   const bool use_system_headers,
+  const bool include_harness,
   const namespacet &ns,
   std::ostream &out)
 {
-  dump_ct goto2c(src, use_system_headers, ns, new_ansi_c_language);
+  dump_ct goto2c(
+    src, use_system_headers, include_harness, ns, new_ansi_c_language);
   out << goto2c;
 }
 
@@ -1529,9 +1620,11 @@ Function: dump_cpp
 void dump_cpp(
   const goto_functionst &src,
   const bool use_system_headers,
+  const bool include_harness,
   const namespacet &ns,
   std::ostream &out)
 {
-  dump_ct goto2cpp(src, use_system_headers, ns, new_cpp_language);
+  dump_ct goto2cpp(
+    src, use_system_headers, include_harness, ns, new_cpp_language);
   out << goto2cpp;
 }

src/goto-instrument/dump_c.h

@@ -14,12 +14,14 @@ Author: Daniel Kroening, [email protected]
 void dump_c(
   const goto_functionst &src,
   const bool use_system_headers,
+  const bool include_harness,
   const namespacet &ns,
   std::ostream &out);
 
 void dump_cpp(
   const goto_functionst &src,
   const bool use_system_headers,
+  const bool include_harness,
   const namespacet &ns,
   std::ostream &out);
 

src/goto-instrument/dump_c_class.h

@@ -22,12 +22,14 @@ class dump_ct
   dump_ct(
     const goto_functionst &_goto_functions,
     const bool use_system_headers,
+    const bool include_harness,
     const namespacet &_ns,
     language_factoryt factory):
     goto_functions(_goto_functions),
     copied_symbol_table(_ns.get_symbol_table()),
     ns(copied_symbol_table),
-    language(factory())
+    language(factory()),
+    harness(include_harness)
   {
     if(use_system_headers)
       init_system_library_map();
@@ -45,6 +47,7 @@ class dump_ct
   symbol_tablet copied_symbol_table;
   const namespacet ns;
   languaget *language;
+  const bool harness;
 
   typedef std::unordered_set<irep_idt, irep_id_hash> convertedt;
   convertedt converted_compound, converted_global, converted_enum;
@@ -133,6 +136,7 @@ class dump_ct
     code_declt &decl,
     std::list<irep_idt> &local_static,
     std::list<irep_idt> &local_type_decls);
+  void cleanup_harness(code_blockt &b);
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_DUMP_C_CLASS_H

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -649,7 +649,8 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("dump-c") || cmdline.isset("dump-cpp"))
     {
       const bool is_cpp=cmdline.isset("dump-cpp");
-      const bool h=cmdline.isset("use-system-headers");
+      const bool headers=cmdline.isset("use-system-headers");
+      const bool harness=cmdline.isset("harness");
       namespacet ns(symbol_table);
 
       // restore RETURN instructions in case remove_returns had been
@@ -668,10 +669,20 @@ int goto_instrument_parse_optionst::doit()
           error() << "failed to write to `" << cmdline.args[1] << "'";
           return 10;
         }
-        (is_cpp ? dump_cpp : dump_c)(goto_functions, h, ns, out);
+        (is_cpp ? dump_cpp : dump_c)(
+          goto_functions,
+          headers,
+          harness,
+          ns,
+          out);
       }
       else
-        (is_cpp ? dump_cpp : dump_c)(goto_functions, h, ns, std::cout);
+        (is_cpp ? dump_cpp : dump_c)(
+          goto_functions,
+          headers,
+          harness,
+          ns,
+          std::cout);
 
       return 0;
     }
@@ -1640,6 +1651,7 @@ void goto_instrument_parse_optionst::help()
     "\n"
     "Other options:\n"
     " --use-system-headers         with --dump-c/--dump-cpp: generate C source with includes\n" // NOLINT(*)
+    " --harness                    with --dump-c/--dump-cpp: include input generator in output\n" // NOLINT(*)
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
     " --json-ui                    use JSON-formatted output\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -23,7 +23,7 @@ Author: Daniel Kroening, [email protected]
   "(all)" \
   "(document-claims-latex)(document-claims-html)" \
   "(document-properties-latex)(document-properties-html)" \
-  "(dump-c)(dump-cpp)(use-system-headers)(dot)(xml)" \
+  "(dump-c)(dump-cpp)(use-system-headers)(harness)(dot)(xml)" \
   OPT_GOTO_CHECK \
   /* no-X-check are deprecated and ignored */ \
   "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \