progress on inlining

Author: kroening

src/cprover/cprover_parse_options.cpp

@@ -107,6 +107,7 @@ int cprover_parse_optionst::main()
     label_properties(goto_model);
 
     bool perform_inlining = true;
+    // bool perform_inlining = false;
 
     if(perform_inlining)
     {

src/cprover/state_encoding.cpp

@@ -32,6 +32,12 @@ class state_encodingt
     const goto_functiont &,
     encoding_targett &);
 
+  void encode(
+    const goto_functionst &,
+    const goto_functiont &,
+    const symbol_exprt &entry_state,
+    encoding_targett &);
+
 protected:
   using loct = goto_programt::const_targett;
 
@@ -63,6 +69,7 @@ class state_encodingt
     encoding_targett &);
 
   loct first_loc;
+  symbol_exprt entry_state = symbol_exprt(irep_idt(), typet());
   using incomingt = std::map<loct, std::vector<loct>>;
   incomingt incoming;
 };
@@ -116,7 +123,7 @@ std::vector<irep_idt> state_encodingt::incoming_symbols(loct loc) const
 symbol_exprt state_encodingt::in_state_expr(loct loc) const
 {
   if(loc == first_loc)
-    return symbol_exprt("SInitial", state_predicate_type());
+    return entry_state;
 
   auto incoming_symbols = this->incoming_symbols(loc);
 
@@ -363,8 +370,9 @@ void state_encodingt::function_call_symbol(
   goto_programt::const_targett loc,
   encoding_targett &dest)
 {
-  const auto &function = loc->call_function();
-  auto identifier = to_symbol_expr(function).get_identifier();
+  const auto &function = to_symbol_expr(loc->call_function());
+  const auto &type = to_code_type(function.type());
+  auto identifier = function.get_identifier();
 
   // malloc is special-cased
   if(identifier == "malloc")
@@ -403,25 +411,31 @@ void state_encodingt::function_call_symbol(
   }
 
   // Evaluate the arguments of the call in the 'in state'
-  multi_ary_exprt arguments_evaluated(ID_tuple, {}, typet(ID_tuple));
-  arguments_evaluated.reserve_operands(loc->call_arguments().size());
-
-  const auto in_state = in_state_expr(loc);
+  exprt arguments_state = state_expr();
 
-  for(auto &argument : loc->call_arguments())
-    arguments_evaluated.add_to_operands(
-      evaluate_expr(loc, in_state, argument));
+  for(std::size_t i = 0; i < type.parameters().size(); i++)
+  {
+    auto address = object_address_exprt(symbol_exprt(
+      f->second.parameter_identifiers[i], type.parameters()[i].type()));
+    auto argument = loc->call_arguments()[i];
+    auto value = evaluate_expr(loc, state_expr(), argument);
+    arguments_state = update_state_exprt(arguments_state, address, value);
+  }
 
+  // Now assign them
   auto function_entry_state = state_expr_with_suffix(loc, "Entry");
-
   dest << forall_states_expr(
-    loc,
-    function_application_exprt(function_entry_state, {state_expr()}));
+    loc, function_application_exprt(function_entry_state, {arguments_state}));
+
+  // now do the body, recursively
+  state_encodingt body_state_encoding;
+  body_state_encoding.encode(
+    goto_functions, f->second, function_entry_state, 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");
+  //  auto return_state = state_expr_with_suffix(loc, "PostReturn");
 
   /*
   constraints.push_back(
@@ -434,7 +448,7 @@ void state_encodingt::function_call_symbol(
   // assign the return value, if any
   if(loc->call_lhs().is_not_nil())
   {
-    exprt equality_rhs = return_state;
+    //    exprt equality_rhs = return_state;
 
     /*
     auto &return_type = loc->call_lhs().type();
@@ -498,16 +512,27 @@ void state_encodingt::operator()(
   if(goto_function.body.instructions.empty())
     return;
 
-  first_loc = goto_function.body.instructions.begin();
-
-  setup_incoming(goto_function);
-
   // initial state
+  auto in_state = symbol_exprt("SInitial", state_predicate_type());
+
   dest << forall_exprt(
     {state_expr()},
     implies_exprt(
-      true_exprt(),
-      function_application_exprt(in_state_expr(first_loc), {state_expr()})));
+      true_exprt(), function_application_exprt(in_state, {state_expr()})));
+
+  encode(goto_functions, goto_function, in_state, dest);
+}
+
+void state_encodingt::encode(
+  const goto_functionst &goto_functions,
+  const goto_functiont &goto_function,
+  const symbol_exprt &entry_state,
+  encoding_targett &dest)
+{
+  first_loc = goto_function.body.instructions.begin();
+  this->entry_state = entry_state;
+
+  setup_incoming(goto_function);
 
   // constraints for each instruction
   forall_goto_program_instructions(loc, goto_function.body)