diff --git a/doc/man/goto-synthesizer.1 b/doc/man/goto-synthesizer.1 index edbf4138740..da4e654b03b 100644 --- a/doc/man/goto-synthesizer.1 +++ b/doc/man/goto-synthesizer.1 @@ -16,6 +16,12 @@ perform synthesis and loop-contracts transformation program transformation for the synthesized contracts, and then writes the resulting program as GOTO binary on disk. .SH OPTIONS +.TP +\fB\-\-dump\-loop\-contracts +Dump the synthesized loop contracts as JSON. +.TP +\fB\-\-json-\output\fR \fIfile\fR +Specify the output destination of the loop-contracts JSON. .SS "User-interface options:" .TP \fB\-\-xml\-ui\fR diff --git a/regression/goto-synthesizer/chain.sh b/regression/goto-synthesizer/chain.sh index 49e9c85f91d..fdf9e6288eb 100755 --- a/regression/goto-synthesizer/chain.sh +++ b/regression/goto-synthesizer/chain.sh @@ -15,10 +15,10 @@ args=${*:6:$#-6} if [[ "$args" != *" _ "* ]] then args_inst=$args - args_cbmc="" + args_synthesizer="" else args_inst="${args%%" _ "*}" - args_cbmc="${args#*" _ "}" + args_synthesizer="${args#*" _ "}" fi if [[ "${is_windows}" == "true" ]]; then @@ -45,6 +45,10 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then rm "${name}-mod.c" fi echo "Running goto-synthesizer: " -$goto_synthesizer "${name}-mod.gb" "${name}-mod-2.gb" -echo "Running CBMC: " -$cbmc "${name}-mod-2.gb" ${args_cbmc} +if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then + $goto_synthesizer ${args_synthesizer} "${name}-mod.gb" +else + $goto_synthesizer "${name}-mod.gb" "${name}-mod-2.gb" + echo "Running CBMC: " + $cbmc "${name}-mod-2.gb" +fi diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_01/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_01/test_dump.desc new file mode 100644 index 00000000000..363f91f24e6 --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_01/test_dump.desc @@ -0,0 +1,10 @@ +CORE +main.c +--pointer-check _ --dump-loop-contracts --json-output main.c +^EXIT=0$ +^SIGNAL=0$ +\"sources"\: \[ \"main\.c\" \] +\"main\"\: \[ \"loop 1 invariant 1\", \"loop 1 assigns result\,i\"\, \"loop 3 invariant 1\"\, \"loop 3 assigns result\,i\" \] +\"output\"\: \"main\.c\" +-- +This test case checks if synthesized contracts are correctly dumped. diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc new file mode 100644 index 00000000000..4344f2ea81c --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc @@ -0,0 +1,9 @@ +CORE +main.c +--pointer-check _ --dump-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +\"sources"\: \[ \"main\.c\" \] +\"main\"\: \[ \"loop 1 invariant i \>\= 80u \|\| \_\_CPROVER\_POINTER\_OFFSET\(array\) +-- +This test case checks if synthesized contracts are correctly dumped. diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_03/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_03/test_dump.desc new file mode 100644 index 00000000000..08d4cad81ff --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_03/test_dump.desc @@ -0,0 +1,9 @@ +CORE +main.c +--pointer-check _ --dump-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +\"sources"\: \[ \"main\.c\" \] +\"main\"\: \[ \"loop 1 invariant array \=\= end +-- +This test case checks if synthesized contracts are correctly dumped. diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_04/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_04/test_dump.desc new file mode 100644 index 00000000000..41399773eff --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_04/test_dump.desc @@ -0,0 +1,9 @@ +CORE +main.c +--pointer-check _ --dump-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +\"sources"\: \[ \"main\.c\" \] +i \=\= .*j.*loop 1 assigns +-- +This test case checks if synthesized contracts are correctly dumped. diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_05/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_05/test_dump.desc new file mode 100644 index 00000000000..c8563ee7bdb --- /dev/null +++ b/regression/goto-synthesizer/loop_contracts_synthesis_05/test_dump.desc @@ -0,0 +1,8 @@ +CORE +main.c +--pointer-check _ --dump-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +assigns \_\_CPROVER\_POINTER\_OBJECT\(b\-\>data\) +-- +This test case checks if synthesized contracts are correctly dumped. diff --git a/src/goto-synthesizer/Makefile b/src/goto-synthesizer/Makefile index 4893078ffdf..4098f531296 100644 --- a/src/goto-synthesizer/Makefile +++ b/src/goto-synthesizer/Makefile @@ -1,4 +1,5 @@ SRC = cegis_verifier.cpp \ + dump_loop_contracts.cpp \ enumerative_loop_contracts_synthesizer.cpp \ expr_enumerator.cpp \ goto_synthesizer_languages.cpp \ diff --git a/src/goto-synthesizer/dump_loop_contracts.cpp b/src/goto-synthesizer/dump_loop_contracts.cpp new file mode 100644 index 00000000000..f679b5ac52d --- /dev/null +++ b/src/goto-synthesizer/dump_loop_contracts.cpp @@ -0,0 +1,128 @@ +/*******************************************************************\ + +Module: Dump Loop Contracts as JSON + +Author: Qinheping Hu, qinhh@amazon.com + +\*******************************************************************/ + +/// \file +/// Dump Loop Contracts as JSON + +#include "dump_loop_contracts.h" + +#include +#include + +#include + +void dump_loop_contracts( + goto_modelt &goto_model, + const std::map &invariant_map, + const std::map> &assigns_map, + const std::string &json_output_str, + std::ostream &out) +{ + // { + // "source" : [SOURCE_NAME_ARRAY], + // "functions" : [{ + // FUN_NAME_1 : [LOOP_CONTRACTS_ARRAY], + // FUN_NAME_2 : [LOOP_CONTRACTS_ARRAY], + // ... + // }], + // "output" : OUTPUT + // } + + INVARIANT(!invariant_map.empty(), "No synthesized loop contracts to dump"); + + namespacet ns(goto_model.symbol_table); + + // Set of names of source files. + std::set sources_set; + + // Map from function name to LOOP_CONTRACTS_ARRAY json array of the function. + std::map function_map; + + json_arrayt json_sources; + + for(const auto &invariant_entry : invariant_map) + { + const auto head = get_loop_head( + invariant_entry.first.loop_number, + goto_model.goto_functions + .function_map[invariant_entry.first.function_id]); + + const auto source_file = id2string(head->source_location().get_file()); + // Add source files. + if(sources_set.insert(source_file).second) + json_sources.push_back(json_stringt(source_file)); + + // Get the LOOP_CONTRACTS_ARRAY for the function from the map. + auto it_function = + function_map.find(id2string(head->source_location().get_function())); + if(it_function == function_map.end()) + { + std::string function_name = + id2string(head->source_location().get_function()); + + // New LOOP_CONTRACTS_ARRAY + json_arrayt loop_contracts_array; + it_function = + function_map.emplace(function_name, loop_contracts_array).first; + } + json_arrayt &loop_contracts_array = it_function->second; + + // Adding loop invariants + // The loop number in Crangler is 1-indexed instead of 0-indexed. + std::string inv_string = + "loop " + std::to_string(invariant_entry.first.loop_number + 1) + + " invariant " + + expr2c( + simplify_expr(invariant_entry.second, ns), + ns, + expr2c_configurationt::clean_configuration); + loop_contracts_array.push_back(json_stringt(inv_string)); + + // Adding loop assigns + const auto it_assigns = assigns_map.find(invariant_entry.first); + if(it_assigns != assigns_map.end()) + { + std::string assign_string = + "loop " + std::to_string(invariant_entry.first.loop_number + 1) + + " assigns "; + + bool in_fisrt_iter = true; + for(const auto &a : it_assigns->second) + { + if(!in_fisrt_iter) + { + assign_string += ","; + } + else + { + in_fisrt_iter = false; + } + assign_string += expr2c( + simplify_expr(a, ns), ns, expr2c_configurationt::clean_configuration); + } + loop_contracts_array.push_back(json_stringt(assign_string)); + } + } + + json_stream_objectt json_stream(out); + json_stream.push_back("sources", json_sources); + + // Initialize functions object. + json_arrayt json_functions; + json_objectt json_functions_object; + for(const auto &loop_contracts : function_map) + { + json_functions_object[loop_contracts.first] = loop_contracts.second; + } + json_functions.push_back(json_functions_object); + json_stream.push_back("functions", json_functions); + + // Destination of the Crangler output. + json_stringt json_output(json_output_str); + json_stream.push_back("output", json_output); +} diff --git a/src/goto-synthesizer/dump_loop_contracts.h b/src/goto-synthesizer/dump_loop_contracts.h new file mode 100644 index 00000000000..47bf5056881 --- /dev/null +++ b/src/goto-synthesizer/dump_loop_contracts.h @@ -0,0 +1,36 @@ +/*******************************************************************\ + +Module: Dump Loop Contracts as JSON + +Author: Qinheping Hu, qinhh@amazon.com + +\*******************************************************************/ + +/// \file +/// Dump Loop Contracts as JSON + +#ifndef CPROVER_GOTO_SYNTHESIZER_DUMP_LOOP_CONTRACTS_H +#define CPROVER_GOTO_SYNTHESIZER_DUMP_LOOP_CONTRACTS_H + +#include "synthesizer_utils.h" + +#include +#include + +void dump_loop_contracts( + goto_modelt &goto_model, + const std::map &invariant_map, + const std::map> &assigns_map, + const std::string &json_output_str, + std::ostream &out); + +#define OPT_DUMP_LOOP_CONTRACTS "(json-output):(dump-loop-contracts)" + +// clang-format off +#define HELP_DUMP_LOOP_CONTRACTS \ + " --dump-loop-contracts dump synthesized loop contracts as JSON\n" /* NOLINT(whitespace/line_length) */ \ + " --json-output specify the output destination of the dumped loop contracts\n" // NOLINT(*) + +// clang-format on + +#endif // CPROVER_GOTO_SYNTHESIZER_DUMP_LOOP_CONTRACTS_H diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp index 985919c7830..cf27ef17b91 100644 --- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp +++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp @@ -424,8 +424,8 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all() return_cex = verifier.verify(); } - log.result() << "result : " << log.green << "PASS" << messaget::eom - << log.reset; + log.result() << "result : " << log.green << "PASS" << log.reset + << messaget::eom; return combined_invariant; } diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp index 685088d7419..ca84601e276 100644 --- a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp +++ b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp @@ -21,8 +21,13 @@ Author: Qinheping Hu #include "enumerative_loop_contracts_synthesizer.h" +#include #include +#ifdef _MSC_VER +# include +#endif + /// invoke main modules int goto_synthesizer_parse_optionst::doit() { @@ -47,22 +52,65 @@ int goto_synthesizer_parse_optionst::doit() if(result_get_goto_program != CPROVER_EXIT_SUCCESS) return result_get_goto_program; - // TODO - // Migrate synthesizer and tests from goto-instrument to goto-synthesizer + // Synthesize loop invariants and annotate them into `goto_model` + enumerative_loop_contracts_synthesizert synthesizer(goto_model, log); + const auto &invariant_map = synthesizer.synthesize_all(); + const auto &assigns_map = synthesizer.get_assigns_map(); + if(cmdline.isset("dump-loop-contracts")) { - // Synthesize loop invariants and annotate them into `goto_model` - enumerative_loop_contracts_synthesizert synthesizer(goto_model, log); - annotate_invariants(synthesizer.synthesize_all(), goto_model); - annotate_assigns(synthesizer.get_assigns_map(), goto_model); - - // Apply loop contracts. - std::set to_exclude_from_nondet_static( - cmdline.get_values("nondet-static-exclude").begin(), - cmdline.get_values("nondet-static-exclude").end()); - code_contractst contracts(goto_model, log); - contracts.apply_loop_contracts(to_exclude_from_nondet_static); + // Default output destination is stdout. + // Crangler will print the result to screen when the output destination + // is "stdout". + std::string json_output_str = "stdout"; + if(cmdline.isset("json-output")) + { + json_output_str = cmdline.get_value("json-output"); + } + + namespacet ns(goto_model.symbol_table); + // Output file specified + if(cmdline.args.size() == 2) + { +#ifdef _MSC_VER + std::ofstream out(widen(cmdline.args[1])); +#else + std::ofstream out(cmdline.args[1]); +#endif + if(!out) + { + log.error() << "failed to write to '" << cmdline.args[1] << "'"; + return CPROVER_EXIT_CONVERSION_FAILED; + } + dump_loop_contracts( + goto_model, invariant_map, assigns_map, json_output_str, out); + } + // No output file specified. Print synthesized contracts with std::cout + else + { + dump_loop_contracts( + goto_model, invariant_map, assigns_map, json_output_str, std::cout); + } + + return CPROVER_EXIT_SUCCESS; } + else if(cmdline.isset("json-output")) + { + throw invalid_command_line_argument_exceptiont( + "Incompatible option detected", + "--json-output must be used with --dump-loop-contracts"); + } + + // Annotate loop contracts. + annotate_invariants(invariant_map, goto_model); + annotate_assigns(assigns_map, goto_model); + + // Apply loop contracts. + std::set to_exclude_from_nondet_static( + cmdline.get_values("nondet-static-exclude").begin(), + cmdline.get_values("nondet-static-exclude").end()); + code_contractst contracts(goto_model, log); + contracts.apply_loop_contracts(to_exclude_from_nondet_static); // recalculate numbers, etc. goto_model.goto_functions.update(); @@ -134,6 +182,7 @@ void goto_synthesizer_parse_optionst::help() " goto-synthesizer in out synthesize and apply loop invariants.\n" // NOLINT(*) "\n" "Main options:\n" + HELP_DUMP_LOOP_CONTRACTS "\n" "Other options:\n" " --version show version and exit\n" diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.h b/src/goto-synthesizer/goto_synthesizer_parse_options.h index 8d12624e277..fd29a7edf54 100644 --- a/src/goto-synthesizer/goto_synthesizer_parse_options.h +++ b/src/goto-synthesizer/goto_synthesizer_parse_options.h @@ -13,8 +13,11 @@ Author: Qinheping Hu #include +#include "dump_loop_contracts.h" + // clang-format off #define GOTO_SYNTHESIZER_OPTIONS \ + OPT_DUMP_LOOP_CONTRACTS \ "(verbosity):(version)(xml-ui)(json-ui)" \ // empty last line