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

@@ -10,6 +10,7 @@
 * GOTO-INSTRUMENT: New option --remove-function-body
 * GOTO-INSTRUMENT: New option --use-all-headers, changed --use-system-headers to
   --no-system-headers
+* 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

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

src/goto-instrument/dump_c.cpp

@@ -21,6 +21,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>
@@ -149,7 +150,8 @@ 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))
+       system_symbols.is_symbol_internal_symbol(symbol, system_headers) &&
+       symbol.name!=goto_functions.entry_point())
       continue;
 
     bool inserted=symbols_sorted.insert(name_str).second;
@@ -198,7 +200,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)))
@@ -946,6 +949,63 @@ void dump_ct::convert_global_variable(
   }
 }
 
+/// Replace CPROVER internal symbols in b by printable values and generate
+/// necessary declarations.
+/// \param b: Code block to be cleaned
+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);
+}
+
 void dump_ct::convert_function_declaration(
     const symbolt &symbol,
     const bool skip_main,
@@ -1001,9 +1061,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 << '\n';
     os_body << "// " << symbol.location << '\n';
-    os_body << make_decl(symbol.name, symbol.type) << '\n';
+    if(symbol.name==goto_functions.entry_point())
+      os_body << make_decl(ID_main, symbol.type) << '\n';
+    else if(!harness || symbol.name!=ID_main)
+      os_body << make_decl(symbol.name, symbol.type) << '\n';
+    else if(harness && symbol.name==ID_main)
+    {
+      os_body << make_decl(CPROVER_PREFIX+id2string(symbol.name), symbol.type)
+              << '\n';
+    }
     os_body << expr_to_string(b);
     os_body << "\n\n";
 
@@ -1017,6 +1088,13 @@ void dump_ct::convert_function_declaration(
     os_decl << "// " << symbol.location << '\n';
     os_decl << make_decl(symbol.name, symbol.type) << ";\n";
   }
+  else if(harness && symbol.name==ID_main)
+  {
+    os_decl << "// " << symbol.name << '\n';
+    os_decl << "// " << symbol.location << '\n';
+    os_decl << make_decl(CPROVER_PREFIX+id2string(symbol.name), symbol.type)
+            << ";\n";
+  }
 
   // make sure typedef names used in the function declaration are
   // available
@@ -1368,22 +1446,34 @@ void dump_c(
   const goto_functionst &src,
   const bool use_system_headers,
   const bool use_all_headers,
+  const bool include_harness,
   const namespacet &ns,
   std::ostream &out)
 {
   dump_ct goto2c(
-    src, use_system_headers, use_all_headers, ns, new_ansi_c_language);
+    src,
+    use_system_headers,
+    use_all_headers,
+    include_harness,
+    ns,
+    new_ansi_c_language);
   out << goto2c;
 }
 
 void dump_cpp(
   const goto_functionst &src,
   const bool use_system_headers,
   const bool use_all_headers,
+  const bool include_harness,
   const namespacet &ns,
   std::ostream &out)
 {
   dump_ct goto2cpp(
-    src, use_system_headers, use_all_headers, ns, new_cpp_language);
+    src,
+    use_system_headers,
+    use_all_headers,
+    include_harness,
+    ns,
+    new_cpp_language);
   out << goto2cpp;
 }

src/goto-instrument/dump_c.h

@@ -18,13 +18,15 @@ void dump_c(
   const goto_functionst &src,
   const bool use_system_headers,
   const bool use_all_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 use_all_headers,
+  const bool include_harness,
   const namespacet &ns,
   std::ostream &out);
 

src/goto-instrument/dump_c_class.h

@@ -28,12 +28,14 @@ class dump_ct
     const goto_functionst &_goto_functions,
     const bool use_system_headers,
     const bool use_all_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)
       system_symbols=system_library_symbolst();
@@ -49,6 +51,7 @@ class dump_ct
   symbol_tablet copied_symbol_table;
   const namespacet ns;
   std::unique_ptr<languaget> language;
+  const bool harness;
 
   typedef std::unordered_set<irep_idt, irep_id_hash> convertedt;
   convertedt converted_compound, converted_global, converted_enum;
@@ -158,6 +161,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

@@ -624,6 +624,7 @@ int goto_instrument_parse_optionst::doit()
       const bool is_cpp=cmdline.isset("dump-cpp");
       const bool h_libc=!cmdline.isset("no-system-headers");
       const bool h_all=cmdline.isset("use-all-headers");
+      const bool harness=cmdline.isset("harness");
       namespacet ns(symbol_table);
 
       // restore RETURN instructions in case remove_returns had been
@@ -642,11 +643,22 @@ 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_libc, h_all, ns, out);
+        (is_cpp ? dump_cpp : dump_c)(
+          goto_functions,
+          h_libc,
+          h_all,
+          harness,
+          ns,
+          out);
       }
       else
         (is_cpp ? dump_cpp : dump_c)(
-          goto_functions, h_libc, h_all, ns, std::cout);
+          goto_functions,
+          h_libc,
+          h_all,
+          harness,
+          ns,
+          std::cout);
 
       return 0;
     }
@@ -1545,6 +1557,7 @@ void goto_instrument_parse_optionst::help()
     "Other options:\n"
     " --no-system-headers          with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)
     " --use-all-headers            with --dump-c/--dump-cpp: generate C source with all 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

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