diff --git a/CHANGELOG b/CHANGELOG index e497b1cadc2..35df4513382 100644 --- a/CHANGELOG +++ b/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 diff --git a/regression/goto-instrument/harness1/main.c b/regression/goto-instrument/harness1/main.c new file mode 100644 index 00000000000..0840c4d8365 --- /dev/null +++ b/regression/goto-instrument/harness1/main.c @@ -0,0 +1,8 @@ +#include + +int main(int argc, char* argv[]) +{ + assert(argc<2 || argv[1]!=0); + + return 0; +} diff --git a/regression/goto-instrument/harness1/test.desc b/regression/goto-instrument/harness1/test.desc new file mode 100644 index 00000000000..307044e9ed4 --- /dev/null +++ b/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 diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 66fc8fb6896..b0859362be9 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/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; diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index f3c156ac8ae..0b210d966d1 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -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,11 +1446,17 @@ 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; } @@ -1380,10 +1464,16 @@ 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; } diff --git a/src/goto-instrument/dump_c.h b/src/goto-instrument/dump_c.h index afac58b9007..d0f15c60489 100644 --- a/src/goto-instrument/dump_c.h +++ b/src/goto-instrument/dump_c.h @@ -18,6 +18,7 @@ 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); @@ -25,6 +26,7 @@ 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); diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h index 26a89242aa5..bddb1cdeda2 100644 --- a/src/goto-instrument/dump_c_class.h +++ b/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 language; + const bool harness; typedef std::unordered_set convertedt; convertedt converted_compound, converted_global, converted_enum; @@ -158,6 +161,7 @@ class dump_ct code_declt &decl, std::list &local_static, std::list &local_type_decls); + void cleanup_harness(code_blockt &b); }; #endif // CPROVER_GOTO_INSTRUMENT_DUMP_C_CLASS_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 8991ab985d3..4c591b77f8e 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/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" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index e2c4bf4fbc0..25ed2ce4cee 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com "(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)" \ diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp index 319acf8674c..13d8de6c0b3 100644 --- a/src/goto-instrument/model_argc_argv.cpp +++ b/src/goto-instrument/model_argc_argv.cpp @@ -16,6 +16,7 @@ Date: April 2016 #include #include +#include #include #include #include @@ -29,6 +30,12 @@ Date: April 2016 #include #include +/// Set up argv with up to max_argc pointers into an array of 4096 bytes. +/// \param symbol_table: Input program's symbol table +/// \param goto_functions: Input program's intermediate representation +/// \param max_argc: User-specified maximum number of arguments to be modelled +/// \param message_handler: message logging +/// \return True, if and only if modelling succeeded bool model_argc_argv( symbol_tablet &symbol_table, goto_functionst &goto_functions, @@ -38,37 +45,23 @@ bool model_argc_argv( messaget message(message_handler); const namespacet ns(symbol_table); - const symbolt *init_symbol=nullptr; - if(ns.lookup(CPROVER_PREFIX "initialize", init_symbol)) + if(!symbol_table.has_symbol(goto_functions.entry_point())) { message.error() << "Linking not done, missing " - << CPROVER_PREFIX "initialize" << messaget::eom; + << goto_functions.entry_point() << messaget::eom; return true; } - if(init_symbol->mode!=ID_C) + const symbolt &main_symbol= + ns.lookup(config.main.empty()?ID_main:config.main); + + if(main_symbol.mode!=ID_C) { message.error() << "argc/argv modelling is C specific" << messaget::eom; return true; } - goto_functionst::function_mapt::iterator init_entry= - goto_functions.function_map.find(CPROVER_PREFIX "initialize"); - assert( - init_entry!=goto_functions.function_map.end() && - init_entry->second.body_available()); - - goto_programt &init=init_entry->second.body; - goto_programt::targett init_end=init.instructions.end(); - --init_end; - assert(init_end->is_end_function()); - assert(init_end!=init.instructions.begin()); - --init_end; - - const symbolt &main_symbol= - ns.lookup(config.main.empty()?ID_main:config.main); - const code_typet::parameterst ¶meters= to_code_type(main_symbol.type).parameters(); if(parameters.size()!=2 && @@ -86,13 +79,14 @@ bool model_argc_argv( std::ostringstream oss; oss << "int ARGC;\n" << "char *ARGV[1];\n" - << "void " CPROVER_PREFIX "initialize()\n" + << "void " << goto_functions.entry_point() << "()\n" << "{\n" << " unsigned next=0u;\n" << " " CPROVER_PREFIX "assume(ARGC>=1);\n" << " " CPROVER_PREFIX "assume(ARGC<=" << max_argc << ");\n" - << " " CPROVER_PREFIX "thread_local static char arg_string[4096];\n" - << " for(unsigned i=0u; i"); - goto_programt tmp; + goto_programt init_instructions; exprt value=nil_exprt(); - // locate the body of the newly built initialize function as well - // as any additional declarations we might need; the body will then - // be converted and appended to the existing initialize function + // locate the body of the newly built start function as well as any + // additional declarations we might need; the body will then be + // converted and inserted into the start function forall_symbols(it, tmp_symbol_table.symbols) { // add __CPROVER_assume if necessary (it might exist already) - if(it->first==CPROVER_PREFIX "assume") + if(it->first==CPROVER_PREFIX "assume" || + it->first==CPROVER_PREFIX "input") symbol_table.add(it->second); - else if(it->first==CPROVER_PREFIX "initialize") + else if(it->first==goto_functions.entry_point()) { value=it->second.value; @@ -134,29 +129,53 @@ bool model_argc_argv( replace(value); } else if(has_prefix(id2string(it->first), - CPROVER_PREFIX "initialize::") && + id2string(goto_functions.entry_point())+"::") && symbol_table.add(it->second)) UNREACHABLE; } + POSTCONDITION(value.is_not_nil()); - assert(value.is_not_nil()); goto_convert( to_code(value), symbol_table, - tmp, + init_instructions, message_handler); - Forall_goto_program_instructions(it, tmp) + Forall_goto_program_instructions(it, init_instructions) { it->source_location.set_file(""); - it->function=CPROVER_PREFIX "initialize"; + it->function=goto_functions.entry_point(); } - init.insert_before_swap(init_end, tmp); + + goto_functionst::function_mapt::iterator start_entry= + goto_functions.function_map.find(goto_functions.entry_point()); + DATA_INVARIANT( + start_entry!=goto_functions.function_map.end() && + start_entry->second.body_available(), + "entry point expected to have a body"); + + goto_programt &start=start_entry->second.body; + goto_programt::targett main_call=start.instructions.begin(); + for(goto_programt::targett end=start.instructions.end(); + main_call!=end; + ++main_call) + { + if(main_call->is_function_call()) + { + const exprt &func= + to_code_function_call(main_call->code).function(); + if(func.id()==ID_symbol && + to_symbol_expr(func).get_identifier()==main_symbol.name) + break; + } + } + POSTCONDITION(main_call!=start.instructions.end()); + + start.insert_before_swap(main_call, init_instructions); // update counters etc. - remove_skip(init); - init.compute_loop_numbers(); + remove_skip(start); + start.compute_loop_numbers(); goto_functions.update(); return false; } -