Added test generation stubs.

regression/test_gen/java1/TestGenTest.java

@@ -0,0 +1,55 @@
+class A
+{
+  public int a_field_0;
+  public int a_field_1;
+
+  public A(int a_field_0)
+  {
+    this.a_field_0=a_field_0;
+  }
+}
+
+class B extends A
+{
+  public int b_field_0;
+
+  public B()
+  {
+    super(999);
+  }
+}
+
+class C
+{
+  public int c_field_0;
+  public B c_field_1;
+
+  public C(int c_field_0, B c_field_1)
+  {
+    this.c_field_0=c_field_0;
+    this.c_field_1=c_field_1;
+  }
+}
+
+public class TestGenTest
+{
+  public static void f(B param0, C param1, int param2)
+  {
+    int a_field_0=param0.a_field_0;
+    int a_field_1=param0.a_field_1;
+    int b_field_0=param0.b_field_0;
+    int c_field_0=param1.c_field_0;
+    int c_field_1_a_field_0=param1.c_field_1.a_field_0;
+    int c_field_1_a_field_1=param1.c_field_1.a_field_1;
+    int c_field_1_b_field_0=param1.c_field_1.b_field_0;
+
+    assert a_field_0           != 499 ||
+           a_field_1           != 498 ||
+           b_field_0           != 497 ||
+           c_field_0           != 496 ||
+           c_field_1_a_field_0 != 495 ||
+           c_field_1_a_field_1 != 494 ||
+           c_field_1_b_field_0 != 493 ||
+           param2              != 492;
+  }
+}

regression/test_gen/java1/test.desc

@@ -0,0 +1,9 @@
+CORE
+TestGenTest.class
+--gen-java-test-case --function TestGenTest.f
+^EXIT=0$
+^SIGNAL=0$
+^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
+--
+^warning: ignoring

regression/test_gen/primitive1/TestGenTest.java

@@ -0,0 +1,7 @@
+public class TestGenTest
+{
+  public static void main(int param_0, int param_1)
+  {
+    assert param_0 != 499 && param_1 != 498;
+  }
+}

regression/test_gen/primitive1/test.desc

@@ -0,0 +1,9 @@
+CORE
+TestGenTest.class
+--gen-java-test-case
+^EXIT=0$
+^SIGNAL=0$
+^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
+--
+^warning: ignoring

src/Makefile

@@ -1,7 +1,7 @@
 DIRS = ansi-c big-int cbmc cpp goto-cc goto-instrument goto-programs \
        goto-symex langapi pointer-analysis solvers util linking xmllang \
        assembler analyses java_bytecode aa-path-symex path-symex musketeer \
-       json cegis goto-analyzer jsil symex
+       json cegis goto-analyzer jsil symex test_gen
 
 all: cbmc.dir goto-cc.dir goto-instrument.dir symex.dir goto-analyzer.dir
 
@@ -29,7 +29,7 @@ musketeer.dir: goto-instrument.dir
 
 cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
           pointer-analysis.dir goto-programs.dir linking.dir \
-          goto-instrument.dir
+          goto-instrument.dir test_gen.dir
 
 goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \
                    json.dir goto-instrument.dir

src/cbmc/Makefile

@@ -25,6 +25,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../solvers/solvers$(LIBEXT) \
+      ../test_gen/test_gen$(LIBEXT) \
       ../util/util$(LIBEXT)
 
 INCLUDES= -I ..

src/cbmc/cbmc_parse_options.cpp

@@ -46,6 +46,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <pointer-analysis/add_failed_symbols.h>
 
+#include <test_gen/java_test_case_generator.h>
+
 #include <analyses/goto_check.h>
 
 #include <langapi/mode.h>
@@ -445,6 +447,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("graphml-cex"))
     options.set_option("graphml-cex", cmdline.get_value("graphml-cex"));
+
+  if(cmdline.isset("gen-java-test-case"))
+    options.set_option("gen-java-test-case", true);
 }
 
 /*******************************************************************\
@@ -561,6 +566,9 @@ int cbmc_parse_optionst::doit()
   if(set_properties(goto_functions))
     return 7;
 
+  if(options.get_bool_option("gen-java-test-case"))
+    return generate_java_test_case(options, symbol_table, goto_functions, bmc);
+
   // do actual BMC
   return do_bmc(bmc, goto_functions);
 }

src/cbmc/cbmc_parse_options.h

@@ -53,6 +53,7 @@ class optionst;
   "(string-abstraction)(no-arch)(arch):" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   "(graphml-cex):" \
+  "(gen-java-test-case)(test_case_file):"\
   "(floatbv)(all-claims)(all-properties)(decide)" // legacy, and will eventually disappear
 
 class cbmc_parse_optionst:

src/test_gen/Makefile

@@ -0,0 +1,16 @@
+SRC = java_test_case_generator.cpp java_test_source_factory.cpp
+
+INCLUDES= -I ..
+
+include ../config.inc
+include ../common
+
+CLEANFILES = test_gen$(LIBEXT)
+
+all: test_gen$(LIBEXT)
+
+###############################################################################
+
+test_gen$(LIBEXT): $(OBJ)
+	$(LINKLIB)
+

src/test_gen/java_test_case_generator.cpp

@@ -0,0 +1,107 @@
+#include <iostream>
+#include <functional>
+
+#include <util/message.h>
+#include <cbmc/bmc.h>
+
+#include <java_bytecode/java_entry_point.h>
+#include <test_gen/java_test_source_factory.h>
+#include <test_gen/java_test_case_generator.h>
+
+namespace
+{
+bool is_meta(const irep_idt &id)
+{
+  const std::string &n=id2string(id);
+  return std::string::npos != n.find("$assertionsDisabled")
+      || std::string::npos != n.find("tmp_struct_init$");
+}
+
+inputst generate_inputs(const symbol_tablet &st, const goto_functionst &gf,
+    const goto_tracet &trace)
+{
+  std::map<const irep_idt, exprt> result;
+  for (const goto_trace_stept &step : trace.steps)
+  {
+    if (goto_trace_stept::ASSIGNMENT == step.type)
+    {
+      const exprt &lhs=step.full_lhs;
+      if (ID_symbol == lhs.id())
+      {
+        const irep_idt &id=to_symbol_expr(lhs).get_identifier();
+        if (st.has_symbol(id) && !is_meta(id))
+        {
+          const exprt &value=step.full_lhs_value;
+          result.insert(std::make_pair(id, value));
+        }
+      }
+    }
+  }
+  return result;
+}
+
+const irep_idt &get_entry_function_id(const goto_functionst &gf)
+{
+  typedef goto_functionst::function_mapt function_mapt;
+  const function_mapt &fm=gf.function_map;
+  const irep_idt start(goto_functionst::entry_point());
+  const function_mapt::const_iterator entry_func=fm.find(start);
+  assert(fm.end() != entry_func);
+  const goto_programt::instructionst &in=entry_func->second.body.instructions;
+  typedef goto_programt::instructionst::const_reverse_iterator reverse_target;
+  const reverse_target last=in.rbegin();
+  const reverse_target end=in.rend();
+  assert(end != last);
+  const reverse_target call=std::next(last);
+  assert(end != call);
+  const code_function_callt &func_call=to_code_function_call(call->code);
+  const exprt &func_expr=func_call.function();
+  return to_symbol_expr(func_expr).get_identifier();
+}
+
+typedef std::function<
+    std::string(const symbol_tablet &, const irep_idt &, const inputst &)> test_case_generatort;
+
+int generate_test_case(optionst &options, const symbol_tablet &st,
+    const goto_functionst &gf, bmct &bmc, const test_case_generatort generate)
+{
+  options.set_option("stop-on-fail", true);
+  switch (bmc(gf))
+  {
+  case safety_checkert::SAFE:
+    return TEST_CASE_FAIL;
+  case safety_checkert::ERROR:
+    return TEST_CASE_ERROR;
+  case safety_checkert::UNSAFE:
+  default:
+  {
+    const goto_tracet &trace=bmc.safety_checkert::error_trace;
+    const inputst inputs(generate_inputs(st, gf, trace));
+    const irep_idt &entry_func_id=get_entry_function_id(gf);
+    const std::string source(generate(st, entry_func_id, inputs));
+    const std::string file(options.get_option("test_case_file"));
+    if (file.empty()) std::cout << source;
+    else
+    {
+      std::ofstream ofs(file.c_str());
+      ofs << source;
+    }
+    return TEST_CASE_SUCCESS;
+  }
+  }
+}
+}
+
+int generate_java_test_case(optionst &o, const symbol_tablet &st,
+    const goto_functionst &gf, bmct &bmc)
+{
+  try
+  {
+    return generate_test_case(o, st, gf, bmc,
+        generate_java_test_case_from_inputs);
+  } catch (const std::string &ex)
+  {
+    std::cerr << ex << std::endl;
+    throw;
+  }
+}

src/test_gen/java_test_case_generator.h

@@ -0,0 +1,33 @@
+/*******************************************************************
+
+ Module: Counterexample-Guided Inductive Synthesis
+
+ Author: Daniel Kroening, [email protected]
+         Pascal Kesseli, [email protected]
+
+\*******************************************************************/
+
+#ifndef JAVA_TEST_CASE_GENERATOR_H_
+#define JAVA_TEST_CASE_GENERATOR_H_
+
+#define TEST_CASE_SUCCESS 0
+#define TEST_CASE_FAIL 1
+#define TEST_CASE_ERROR 10
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param options
+ * @param st
+ * @param gf
+ * @param bmc
+ */
+int generate_java_test_case(
+    class optionst &options,
+    const class symbol_tablet &st,
+    const class goto_functionst &gf,
+    class bmct &bmc);
+
+#endif /* JAVA_TEST_CASE_GENERATOR_H_ */