progress on function calls

Author: kroening

src/cprover/state_encoding.cpp

@@ -53,6 +53,7 @@ class state_encodingt
   using loct = goto_programt::const_targett;
 
   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;
   exprt evaluate_expr(loct, const exprt &, const exprt &) const;
@@ -72,16 +73,19 @@ class state_encodingt
 
 symbol_exprt state_encodingt::out_state_expr(loct loc) const
 {
-  return symbol_exprt(
-    "S" + std::to_string(loc->location_number), state_predicate_type());
+  return state_expr_with_suffix(loc, "");
+}
+
+symbol_exprt state_encodingt::state_expr_with_suffix(loct loc, const std::string &suffix) const
+{
+  irep_idt identifier =
+    std::string("S") + std::to_string(loc->location_number) + suffix;
+  return symbol_exprt(identifier, state_predicate_type());
 }
 
 symbol_exprt state_encodingt::out_state_expr(loct loc, bool taken) const
 {
-  return symbol_exprt(
-    std::string("S") + std::to_string(loc->location_number) +
-      (taken ? "T" : ""),
-    state_predicate_type());
+  return state_expr_with_suffix(loc, taken ? "T" : "");
 }
 
 symbol_exprt state_encodingt::in_state_expr(loct loc) const
@@ -349,40 +353,43 @@ void state_encodingt::operator()(
     }
     else if(loc->is_function_call())
     {
-      /*
-      const sourcet source{loc->location_number};
-
-      // Evaluate the arguments in the 'in state'
-      const auto in_state = in_state_expr(source);
-
+      // 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);
+
       for(auto &argument : loc->call_arguments())
-        arguments_evaluated.add_to_operands(evaluate_exprt(in_state, argument));
+        arguments_evaluated.add_to_operands(evaluate_expr(loc, in_state, argument));
+
+      auto function_entry_state = state_expr_with_suffix(loc, "Entry");
 
-      // Function return state (suffix _R).
+      dest << forall_states_expr(loc,
+        function_application_exprt(function_entry_state, {state_expr()}));
+
+      // 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 = suffix_state_expr(source.location, "_R");
-
-      // Add the constraints for the callee -- if there is no
-      // contract, this is the full body, possibly transitively.
+      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_exprt(
+          evaluate_expr(
+            loc,
             return_state,
             symbol_exprt("return_value", return_type));
 
@@ -397,14 +404,13 @@ void state_encodingt::operator()(
 
         // 'out state' equality
         constraints.push_back(equal_exprt(lhs, rhs));
+*/
       }
       else
       {
         // 'out state' equality
-        auto lhs = out_state_expr(source);
-        constraints.push_back(equal_exprt(lhs, return_state));
+        dest << equal_exprt(out_state_expr(loc), return_state);
       }
-      */
     }
     else if(loc->is_set_return_value())
     {
@@ -495,6 +501,7 @@ class ascii_encoding_targett : public encoding_targett
 
   void annotation(const std::string &text) override
   {
+    out << '\n' << text << '\n';
   }
 
 protected: