calls to functions without body

Author: kroening

regression/cprover/function_calls/call_no_body1.c

@@ -0,0 +1,7 @@
+int function_without_body();
+
+int main()
+{
+  int x = function_without_body();
+  return 0;
+}

regression/cprover/function_calls/call_no_body1.desc

@@ -0,0 +1,8 @@
+CORE
+call_no_body1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet22\]\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$
+--

src/cprover/state_encoding.cpp

@@ -47,7 +47,10 @@ mathematical_function_typet state_predicate_type()
 class state_encodingt
 {
 public:
-  void operator()(const goto_functiont &, encoding_targett &);
+  void operator()(
+    const goto_functionst &,
+    const goto_functiont &,
+    encoding_targett &);
 
 protected:
   using loct = goto_programt::const_targett;
@@ -245,6 +248,7 @@ void state_encodingt::setup_incoming(const goto_functiont &goto_function)
 }
 
 void state_encodingt::operator()(
+  const goto_functionst &goto_functions,
   const goto_functiont &goto_function,
   encoding_targett &dest)
 {
@@ -353,63 +357,103 @@ void state_encodingt::operator()(
     }
     else if(loc->is_function_call())
     {
-      // 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_expr(loc, in_state, argument));
-
-      auto function_entry_state = state_expr_with_suffix(loc, "Entry");
-
-      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 = 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())
+      // Function pointer?
+      const auto &function = loc->call_function();
+      if(function.id() == ID_dereference)
       {
-        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));
+        // TBD.
+        PRECONDITION(false);
+      }
+      else if(function.id() == ID_symbol)
+      {
+        // Do we have a function body?
+        auto identifier = to_symbol_expr(function).get_identifier();
+        auto f = goto_functions.function_map.find(identifier);
+        if(f == goto_functions.function_map.end())
+          DATA_INVARIANT(false, "failed find function in function_map");
+        if(f->second.body_available())
+        {
+          // 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());
 
-        multi_ary_exprt designator(ID_designator, { loc->call_lhs() }, typet());
+          const auto in_state = in_state_expr(loc);
 
-        auto lhs = out_state_expr(source);
+          for(auto &argument : loc->call_arguments())
+            arguments_evaluated.add_to_operands(
+              evaluate_expr(loc, in_state, argument));
 
-        auto rhs = update_exprt(
-          return_state,
-          designator,
-          rhs_evaluated);
+          auto function_entry_state = state_expr_with_suffix(loc, "Entry");
 
-        // 'out state' equality
-        constraints.push_back(equal_exprt(lhs, rhs));
-*/
+          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 = 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);
+          }
+        }
+        else
+        {
+          // no function body -- do LHS assignment nondeterministically, if any
+          if(loc->call_lhs().is_not_nil())
+          {
+            auto rhs = side_effect_expr_nondett(
+              loc->call_lhs().type(), loc->source_location());
+            dest << assignment_constraint(loc, loc->call_lhs(), std::move(rhs));
+          }
+          else
+          {
+            // This is a SKIP.
+            dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
+          }
+        }
       }
       else
       {
-        // 'out state' equality
-        dest << equal_exprt(out_state_expr(loc), return_state);
+        DATA_INVARIANT(
+          false, "got function that's neither a symbol nor a function pointer");
       }
     }
     else if(loc->is_set_return_value())
@@ -433,7 +477,7 @@ void state_encoding(
       goto_functionst::entry_point());
     PRECONDITION(f_entry != goto_model.goto_functions.function_map.end());
 
-    state_encodingt{}(f_entry->second, dest);
+    state_encodingt{}(goto_model.goto_functions, f_entry->second, dest);
   }
   else
   {
@@ -445,7 +489,7 @@ void state_encoding(
       if(f->second.body_available())
       {
         dest.annotation("function " + id2string(f->first));
-        state_encodingt{}(f->second, dest);
+        state_encodingt{}(goto_model.goto_functions, f->second, dest);
       }
     }
   }