progress on inlining

Author: kroening

src/cprover/state_encoding.cpp

@@ -27,25 +27,31 @@ Module: State Encoding
 class state_encodingt
 {
 public:
+  state_encodingt(const goto_functionst &__goto_functions)
+    : goto_functions(__goto_functions)
+  {
+  }
+
   void operator()(
-    const goto_functionst &,
     const goto_functiont &,
     encoding_targett &);
 
   void encode(
-    const goto_functionst &,
     const goto_functiont &,
+    const std::string &state_prefix,
     const symbol_exprt &entry_state,
+    const exprt &return_lhs,
     encoding_targett &);
 
 protected:
   using loct = goto_programt::const_targett;
+  const goto_functionst &goto_functions;
 
   symbol_exprt out_state_expr(loct) const;
   symbol_exprt state_expr_with_suffix(loct, const std::string &suffix) const;
   symbol_exprt out_state_expr(loct, bool taken) const;
   symbol_exprt in_state_expr(loct) const;
-  std::vector<irep_idt> incoming_symbols(loct) const;
+  std::vector<symbol_exprt> incoming_symbols(loct) const;
   exprt evaluate_expr(loct, const exprt &, const exprt &) const;
   exprt evaluate_expr_rec(
     loct,
@@ -60,16 +66,16 @@ class state_encodingt
   void setup_incoming(const goto_functiont &);
   exprt assignment_constraint(loct, exprt lhs, exprt rhs) const;
   void function_call(
-    const goto_functionst &,
     goto_programt::const_targett,
     encoding_targett &);
   void function_call_symbol(
-    const goto_functionst &,
     goto_programt::const_targett,
     encoding_targett &);
 
+  std::string state_prefix;
   loct first_loc;
   symbol_exprt entry_state = symbol_exprt(irep_idt(), typet());
+  exprt return_lhs = nil_exprt();
   using incomingt = std::map<loct, std::vector<loct>>;
   incomingt incoming;
 };
@@ -84,7 +90,7 @@ symbol_exprt state_encodingt::state_expr_with_suffix(
   const std::string &suffix) const
 {
   irep_idt identifier =
-    std::string("S") + std::to_string(loc->location_number) + suffix;
+    state_prefix + std::to_string(loc->location_number) + suffix;
   return symbol_exprt(identifier, state_predicate_type());
 }
 
@@ -93,13 +99,13 @@ symbol_exprt state_encodingt::out_state_expr(loct loc, bool taken) const
   return state_expr_with_suffix(loc, taken ? "T" : "");
 }
 
-std::vector<irep_idt> state_encodingt::incoming_symbols(loct loc) const
+std::vector<symbol_exprt> state_encodingt::incoming_symbols(loct loc) const
 {
   auto incoming_it = incoming.find(loc);
 
   DATA_INVARIANT(incoming_it != incoming.end(), "incoming is complete");
 
-  std::vector<irep_idt> symbols;
+  std::vector<symbol_exprt> symbols;
   symbols.reserve(incoming_it->second.size());
 
   for(auto &loc_in : incoming_it->second)
@@ -114,7 +120,7 @@ std::vector<irep_idt> state_encodingt::incoming_symbols(loct loc) const
       suffix = "T";
     }
 
-    symbols.push_back("S" + std::to_string(loc_in->location_number) + suffix);
+    symbols.push_back(state_expr_with_suffix(loc_in, suffix));
   }
 
   return symbols;
@@ -128,10 +134,9 @@ symbol_exprt state_encodingt::in_state_expr(loct loc) const
   auto incoming_symbols = this->incoming_symbols(loc);
 
   if(incoming_symbols.size() == 1)
-    return symbol_exprt(incoming_symbols.front(), state_predicate_type());
-
-  return symbol_exprt(
-    "S" + std::to_string(loc->location_number) + "in", state_predicate_type());
+    return incoming_symbols.front();
+  else
+    return state_expr_with_suffix(loc, "in");
 }
 
 exprt state_encodingt::evaluate_expr(
@@ -366,7 +371,6 @@ static exprt simplifying_not(exprt src)
 }
 
 void state_encodingt::function_call_symbol(
-  const goto_functionst &goto_functions,
   goto_programt::const_targett loc,
   encoding_targett &dest)
 {
@@ -428,9 +432,11 @@ void state_encodingt::function_call_symbol(
     loc, function_application_exprt(function_entry_state, {arguments_state}));
 
   // now do the body, recursively
-  state_encodingt body_state_encoding;
+  state_encodingt body_state_encoding(goto_functions);
+  auto new_state_prefix =
+    state_prefix + std::to_string(loc->location_number) + ".";
   body_state_encoding.encode(
-    goto_functions, f->second, function_entry_state, dest);
+    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
@@ -481,7 +487,6 @@ void state_encodingt::function_call_symbol(
 }
 
 void state_encodingt::function_call(
-  const goto_functionst &goto_functions,
   goto_programt::const_targett loc,
   encoding_targett &dest)
 {
@@ -495,7 +500,7 @@ void state_encodingt::function_call(
   }
   else if(function.id() == ID_symbol)
   {
-    function_call_symbol(goto_functions, loc, dest);
+    function_call_symbol(loc, dest);
   }
   else
   {
@@ -505,7 +510,6 @@ void state_encodingt::function_call(
 }
 
 void state_encodingt::operator()(
-  const goto_functionst &goto_functions,
   const goto_functiont &goto_function,
   encoding_targett &dest)
 {
@@ -520,17 +524,20 @@ void state_encodingt::operator()(
     implies_exprt(
       true_exprt(), function_application_exprt(in_state, {state_expr()})));
 
-  encode(goto_functions, goto_function, in_state, dest);
+  encode(goto_function, "S", in_state, nil_exprt(), dest);
 }
 
 void state_encodingt::encode(
-  const goto_functionst &goto_functions,
   const goto_functiont &goto_function,
+  const std::string &state_prefix,
   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->entry_state = entry_state;
+  this->return_lhs = return_lhs;
 
   setup_incoming(goto_function);
 
@@ -549,13 +556,10 @@ void state_encodingt::encode(
         auto s = state_expr();
         for(auto incoming_symbol : incoming_symbols)
         {
-          auto incoming_state =
-            symbol_exprt(incoming_symbol, state_predicate_type());
-
           dest << forall_exprt(
             {s},
             implies_exprt(
-              function_application_exprt(std::move(incoming_state), {s}),
+              function_application_exprt(incoming_symbol, {s}),
               function_application_exprt(in_state_expr(loc), {s})));
         }
       }
@@ -645,14 +649,21 @@ void state_encodingt::encode(
     }
     else if(loc->is_function_call())
     {
-      function_call(goto_functions, loc, dest);
+      function_call(loc, dest);
     }
     else if(loc->is_set_return_value())
     {
-      // treat these as assignments to a special symbol named 'return_value'
-      auto rhs = loc->return_value();
-      auto lhs = symbol_exprt("return_value", rhs.type());
-      dest << assignment_constraint(loc, std::move(lhs), std::move(rhs));
+      const auto &rhs = loc->return_value();
+
+      if(return_lhs.is_nil())
+      {
+        // treat these as assignments to a special symbol named 'return_value'
+        auto lhs = symbol_exprt("return_value", rhs.type());
+        dest << assignment_constraint(loc, std::move(lhs), std::move(rhs));
+      }
+      else
+      {
+      }
     }
   }
 }
@@ -670,7 +681,7 @@ void state_encoding(
     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);
+    state_encodingt{goto_model.goto_functions}(f_entry->second, dest);
   }
   else
   {
@@ -682,7 +693,7 @@ void state_encoding(
       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->second, dest);
       }
     }
   }