progress on inlining

Author: kroening

src/cprover/cprover_parse_options.cpp

@@ -106,7 +106,7 @@ int cprover_parse_optionst::main()
 
     label_properties(goto_model);
 
-    bool perform_inlining = true;
+    bool perform_inlining = !cmdline.isset("no-inline");
     // bool perform_inlining = false;
 
     if(perform_inlining)

src/cprover/cprover_parse_options.h

@@ -19,7 +19,7 @@ Author: Daniel Kroening, [email protected]
   "(smt2)(text)(outfile):"                                                     \
   "(safety)"                                                                   \
   "(solve)"                                                                    \
-  "(inline)"                                                                   \
+  "(inline)(no-inline)"                                                        \
   "(show-goto-functions)(show-loops)"                                          \
   "(validate-goto-model)"                                                      \
   "(verbose)"

src/cprover/state_encoding.cpp

@@ -33,12 +33,13 @@ class state_encodingt
   }
 
   void operator()(
-    const goto_functiont &,
+    const goto_functionst::function_mapt::const_iterator,
     encoding_targett &);
 
   void encode(
     const goto_functiont &,
     const std::string &state_prefix,
+    const std::string &annotation,
     const symbol_exprt &entry_state,
     const exprt &return_lhs,
     encoding_targett &);
@@ -73,6 +74,7 @@ class state_encodingt
     encoding_targett &);
 
   std::string state_prefix;
+  std::string annotation;
   loct first_loc;
   symbol_exprt entry_state = symbol_exprt(irep_idt(), typet());
   exprt return_lhs = nil_exprt();
@@ -378,6 +380,9 @@ void state_encodingt::function_call_symbol(
   const auto &type = to_code_type(function.type());
   auto identifier = function.get_identifier();
 
+  auto new_annotation = annotation + u8" \u2192 " + id2string(identifier);
+  dest.annotation(new_annotation);
+
   // malloc is special-cased
   if(identifier == "malloc")
   {
@@ -436,54 +441,12 @@ void state_encodingt::function_call_symbol(
   auto new_state_prefix =
     state_prefix + std::to_string(loc->location_number) + ".";
   body_state_encoding.encode(
-    f->second, new_state_prefix, function_entry_state, nil_exprt(), dest);
-
-  // Function return state (suffix PostReturn).
-  // This is the state after exiting the function but prior to
-  // assigning the LHS of the function call.
-  //  auto return_state = state_expr_with_suffix(loc, "PostReturn");
-
-  /*
-  constraints.push_back(
-    multi_ary_exprt(
-      ID_goto_contract,
-      {loc->call_function(), in_state, return_state, arguments_evaluated},
-      bool_typet()));
-  */
-
-  // assign the return value, if any
-  if(loc->call_lhs().is_not_nil())
-  {
-    //    exprt equality_rhs = return_state;
-
-    /*
-    auto &return_type = loc->call_lhs().type();
-    auto rhs_evaluated =
-      evaluate_expr(
-        loc,
-        return_state,
-        symbol_exprt("return_value", return_type));
-
-    multi_ary_exprt designator(ID_designator, { loc->call_lhs() }, typet());
-
-    auto lhs = out_state_expr(source);
-
-    auto rhs = update_exprt(
-      return_state,
-      designator,
-      rhs_evaluated);
-
-    // 'out state' equality
-    constraints.push_back(equal_exprt(lhs, rhs));
-*/
-  }
-/*
-  else
-  {
-    // 'out state' equality
-    dest << equal_exprt(out_state_expr(loc), return_state);
-  }
-*/
+    f->second,
+    new_state_prefix,
+    new_annotation,
+    function_entry_state,
+    nil_exprt(),
+    dest);
 }
 
 void state_encodingt::function_call(
@@ -510,9 +473,11 @@ void state_encodingt::function_call(
 }
 
 void state_encodingt::operator()(
-  const goto_functiont &goto_function,
+  goto_functionst::function_mapt::const_iterator f_entry,
   encoding_targett &dest)
 {
+  const auto &goto_function = f_entry->second;
+
   if(goto_function.body.instructions.empty())
     return;
 
@@ -524,18 +489,22 @@ void state_encodingt::operator()(
     implies_exprt(
       true_exprt(), function_application_exprt(in_state, {state_expr()})));
 
-  encode(goto_function, "S", in_state, nil_exprt(), dest);
+  auto annotation = id2string(f_entry->first);
+
+  encode(goto_function, "S", annotation, in_state, nil_exprt(), dest);
 }
 
 void state_encodingt::encode(
   const goto_functiont &goto_function,
   const std::string &state_prefix,
+  const std::string &annotation,
   const symbol_exprt &entry_state,
   const exprt &return_lhs,
   encoding_targett &dest)
 {
   first_loc = goto_function.body.instructions.begin();
   this->state_prefix = state_prefix;
+  this->annotation = annotation;
   this->entry_state = entry_state;
   this->return_lhs = return_lhs;
 
@@ -673,30 +642,15 @@ void state_encoding(
   bool program_is_inlined,
   encoding_targett &dest)
 {
-  if(program_is_inlined)
-  {
-    auto f_entry = goto_model.goto_functions.function_map.find(
-      goto_functionst::entry_point());
+  auto f_entry =
+    goto_model.goto_functions.function_map.find(goto_functionst::entry_point());
 
-    if(f_entry == goto_model.goto_functions.function_map.end())
-      throw incorrect_goto_program_exceptiont("The program has no entry point");
+  if(f_entry == goto_model.goto_functions.function_map.end())
+    throw incorrect_goto_program_exceptiont("The program has no entry point");
 
-    state_encodingt{goto_model.goto_functions}(f_entry->second, dest);
-  }
-  else
-  {
-    // output alphabetically
-    const auto sorted = goto_model.goto_functions.sorted();
+  dest.annotation("function " + id2string(f_entry->first));
 
-    for(const auto &f : sorted)
-    {
-      if(f->second.body_available())
-      {
-        dest.annotation("function " + id2string(f->first));
-        state_encodingt{goto_model.goto_functions}(f->second, dest);
-      }
-    }
-  }
+  state_encodingt{goto_model.goto_functions}(f_entry, dest);
 }
 
 void format_hooks();