fx cprover

Author: kroening

src/cprover/cprover_parse_options.cpp

@@ -98,7 +98,15 @@ int cprover_parse_optionst::main()
       initialize_goto_model(cmdline.args, message_handler, options);
 
     adjust_float_expressions(goto_model);
-    goto_inline(goto_model, message_handler, true);
+
+    bool perform_inlining = true;
+
+    if(perform_inlining)
+    {
+      std::cout << "Performing inlining\n";
+      goto_inline(goto_model, message_handler, true);
+    }
+
     goto_model.goto_functions.compute_location_numbers();
 
     if(cmdline.isset("show-goto-functions"))
@@ -130,11 +138,11 @@ int cprover_parse_optionst::main()
 #else
       std::ofstream out(file_name);
 #endif
-      state_encoding(goto_model, format, out);
+      state_encoding(goto_model, format, perform_inlining, out);
       std::cout << "formula written to " << file_name << '\n';
     }
     else
-      state_encoding(goto_model, format, std::cout);
+      state_encoding(goto_model, format, perform_inlining, std::cout);
 
     return CPROVER_EXIT_SUCCESS;
   }
@@ -165,7 +173,9 @@ void cprover_parse_optionst::help()
     " {bcprover} {usource-file.c}    \t convert a given C program\n"
     "\n"
     "Other options:\n"
-    " {y--smt2} \t output formula in SMT-LIB2 format\n"
+    " {y--inline} \t perform function call inlining before\n"
+    " \t generating the formula\n"
     " {y--outfile} {ufile-name} \t set output file for formula\n"
+    " {y--smt2} \t output formula in SMT-LIB2 format\n"
     "\n");
 }

src/cprover/cprover_parse_options.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_OPTIONS                                                        \
   "(help)?h(version)"                                                          \
   "(smt2)(outfile):"                                                           \
+  "(inline)"                                                                   \
   "(show-goto-functions)(show-loops)"                                          \
   "(validate-goto-model)"                                                      \
   "(verbose)"

src/cprover/state_encoding.cpp

@@ -18,6 +18,19 @@ Module: State Encoding
 
 #include <solvers/smt2/smt2_conv.h>
 
+class encoding_targett
+{
+public:
+  virtual void annotation(const std::string &) = 0;
+  virtual void set_to_true(exprt) = 0;
+  virtual ~encoding_targett() = default;
+};
+
+void operator<<(encoding_targett &target, exprt constraint)
+{
+  target.set_to_true(std::move(constraint));
+}
+
 class state_typet : public typet
 {
 public:
@@ -34,7 +47,7 @@ mathematical_function_typet state_predicate_type()
 class state_encodingt
 {
 public:
-  void operator()(const goto_functiont &, decision_proceduret &);
+  void operator()(const goto_functiont &, encoding_targett &);
 
 protected:
   using loct = goto_programt::const_targett;
@@ -229,7 +242,7 @@ void state_encodingt::setup_incoming(const goto_functiont &goto_function)
 
 void state_encodingt::operator()(
   const goto_functiont &goto_function,
-  decision_proceduret &dest)
+  encoding_targett &dest)
 {
   if(goto_function.body.instructions.empty())
     return;
@@ -399,79 +412,90 @@ void state_encodingt::operator()(
   }
 }
 
-void state_encoding(const goto_modelt &goto_model, decision_proceduret &dest)
+void state_encoding(
+  const goto_modelt &goto_model,
+  bool program_is_inlined,
+  encoding_targett &dest)
 {
-  auto f_entry =
-    goto_model.goto_functions.function_map.find(goto_functionst::entry_point());
-  if(f_entry == goto_model.goto_functions.function_map.end())
+  if(program_is_inlined)
   {
+    auto f_entry = goto_model.goto_functions.function_map.find(
+      goto_functionst::entry_point());
+    PRECONDITION(f_entry != goto_model.goto_functions.function_map.end());
+
+    state_encodingt{}(f_entry->second, dest);
   }
   else
   {
-    state_encodingt{}(f_entry->second, dest);
+    // output alphabetically
+    const auto sorted = goto_model.goto_functions.sorted();
+
+    for(const auto &f : sorted)
+    {
+      if(f->second.body_available())
+      {
+        dest.annotation("function " + id2string(f->first));
+        state_encodingt{}(f->second, dest);
+      }
+    }
   }
 }
 
-class smt2_encodert : public smt2_convt
+class smt2_encoding_targett : public encoding_targett
 {
 public:
-  smt2_encodert(const namespacet &ns, std::ostream &out)
-    : smt2_convt(ns, "", "cprover", "", solvert::GENERIC, out)
+  smt2_encoding_targett(const namespacet &ns, std::ostream &__out)
+    : out(__out),
+      smt2_conv(ns, "", "cprover", "", smt2_convt::solvert::GENERIC, out)
   {
-    use_array_of_bool = true;
-    use_as_const = true;
+    smt2_conv.use_array_of_bool = true;
+    smt2_conv.use_as_const = true;
   }
-};
 
-class ascii_decision_proceduret : public decision_proceduret
-{
-public:
-  ascii_decision_proceduret(std::ostream &__out) : out(__out)
+  ~smt2_encoding_targett()
   {
+    // finish the conversion to SMT-LIB2
+    smt2_conv();
   }
 
-  void set_to(const exprt &expr, bool value)
+  void set_to_true(exprt expr) override
   {
-    counter++;
-    if(counter < 10)
-      out << ' ';
-    out << '(' << counter << ')' << ' ';
-    out << format(expr) << '\n';
+    smt2_conv.set_to_true(std::move(expr));
   }
 
-  exprt handle(const exprt &)
+  void annotation(const std::string &text) override
   {
-    UNIMPLEMENTED;
+    out << ';' << ' ' << text << '\n';
   }
 
-  exprt get(const exprt &) const
-  {
-    UNIMPLEMENTED;
-  }
+protected:
+  std::ostream &out;
+  smt2_convt smt2_conv;
+};
 
-  void print_assignment(std::ostream &) const
+class ascii_encoding_targett : public encoding_targett
+{
+public:
+  explicit ascii_encoding_targett(std::ostream &__out) : out(__out)
   {
-    UNIMPLEMENTED;
   }
 
-  std::string decision_procedure_text() const
+  void set_to_true(exprt expr) override
   {
-    UNIMPLEMENTED;
+    counter++;
+    if(counter < 10)
+      out << ' ';
+    out << '(' << counter << ')' << ' ';
+    out << format(expr) << '\n';
   }
 
-  std::size_t get_number_of_solver_calls() const
+  void annotation(const std::string &text) override
   {
-    UNIMPLEMENTED;
   }
 
 protected:
   std::ostream &out;
   std::size_t counter = 0;
-
-  resultt dec_solve()
-  {
-    UNIMPLEMENTED;
-  }
 };
 
 static void format_hooks()
@@ -514,6 +538,7 @@ static void format_hooks()
 void state_encoding(
   const goto_modelt &goto_model,
   state_encoding_formatt state_encoding_format,
+  bool program_is_inlined,
   std::ostream &out)
 {
   const namespacet ns(goto_model.symbol_table);
@@ -523,16 +548,15 @@ void state_encoding(
   case state_encoding_formatt::ASCII:
   {
     format_hooks();
-    ascii_decision_proceduret dest(out);
-    state_encoding(goto_model, dest);
+    ascii_encoding_targett dest(out);
+    state_encoding(goto_model, program_is_inlined, dest);
   }
   break;
 
   case state_encoding_formatt::SMT2:
   {
-    smt2_encodert dest(ns, out);
-    state_encoding(goto_model, dest);
-    dest(); // finish conversion
+    smt2_encoding_targett dest(ns, out);
+    state_encoding(goto_model, program_is_inlined, dest);
   }
   break;
   }

src/cprover/state_encoding.h

@@ -25,6 +25,7 @@ enum class state_encoding_formatt
 void state_encoding(
   const goto_modelt &,
   state_encoding_formatt,
+  bool program_is_inlined,
   std::ostream &out);
 
 #endif // CPROVER_GOTO_INSTRUMENT_STATE_ENCODING_H