SYNTHESIZER: Add dump-loop-contracts into loop-contracts synthesizer

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

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

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.

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.

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.

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.

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.

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 \

src/goto-synthesizer/dump_loop_contracts.cpp

@@ -0,0 +1,128 @@
+/*******************************************************************\
+
+Module: Dump Loop Contracts as JSON
+
+Author: Qinheping Hu, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Dump Loop Contracts as JSON
+
+#include "dump_loop_contracts.h"
+
+#include <util/json_stream.h>
+#include <util/simplify_expr.h>
+
+#include <ansi-c/expr2c.h>
+
+void dump_loop_contracts(
+  goto_modelt &goto_model,
+  const std::map<loop_idt, exprt> &invariant_map,
+  const std::map<loop_idt, std::set<exprt>> &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<std::string> sources_set;
+
+  // Map from function name to LOOP_CONTRACTS_ARRAY json array of the function.
+  std::map<std::string, json_arrayt> 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);
+}

src/goto-synthesizer/dump_loop_contracts.h

@@ -0,0 +1,36 @@
+/*******************************************************************\
+
+Module: Dump Loop Contracts as JSON
+
+Author: Qinheping Hu, [email protected]
+
+\*******************************************************************/
+
+/// \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 <iosfwd>
+#include <string>
+
+void dump_loop_contracts(
+  goto_modelt &goto_model,
+  const std::map<loop_idt, exprt> &invariant_map,
+  const std::map<loop_idt, std::set<exprt>> &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 <file>          specify the output destination of the dumped loop contracts\n" // NOLINT(*)
+
+// clang-format on
+
+#endif // CPROVER_GOTO_SYNTHESIZER_DUMP_LOOP_CONTRACTS_H

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;
 }

src/goto-synthesizer/goto_synthesizer_parse_options.cpp

@@ -21,8 +21,13 @@ Author: Qinheping Hu
 
 #include "enumerative_loop_contracts_synthesizer.h"
 
+#include <fstream>
 #include <iostream>
 
+#ifdef _MSC_VER
+#  include <util/unicode.h>
+#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<std::string> 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<std::string> 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"

src/goto-synthesizer/goto_synthesizer_parse_options.h

@@ -13,8 +13,11 @@ Author: Qinheping Hu
 
 #include <goto-programs/goto_model.h>
 
+#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