function calls

Author: kroening

src/cprover/state_encoding.cpp

@@ -57,6 +57,10 @@ class state_encodingt
     const goto_functionst &,
     goto_programt::const_targett,
     encoding_targett &);
+  void function_call_symbol(
+    const goto_functionst &,
+    goto_programt::const_targett,
+    encoding_targett &);
 
   loct first_loc;
   using incomingt = std::map<loct, std::vector<loct>>;
@@ -354,121 +358,130 @@ static exprt simplifying_not(exprt src)
     return not_exprt(src);
 }
 
-void state_encodingt::function_call(
+void state_encodingt::function_call_symbol(
   const goto_functionst &goto_functions,
   goto_programt::const_targett loc,
   encoding_targett &dest)
 {
-  // Function pointer?
   const auto &function = loc->call_function();
-  if(function.id() == ID_dereference)
+  auto identifier = to_symbol_expr(function).get_identifier();
+
+  // malloc is special-cased
+  if(identifier == "malloc")
   {
-    // TBD.
-    throw incorrect_goto_program_exceptiont(
-      "can't do function pointers", loc->source_location());
+    auto state = state_expr();
+    PRECONDITION(loc->call_arguments().size() == 1);
+    auto size_evaluated = evaluate_expr(loc, state, loc->call_arguments()[0]);
+
+    auto lhs_address = address_rec(loc, state, loc->call_lhs());
+    exprt new_state = ternary_exprt(
+      ID_allocate, state, lhs_address, size_evaluated, state_typet());
+    dest << forall_states_expr(
+      loc, function_application_exprt(out_state_expr(loc), {new_state}));
+    return;
   }
-  else if(function.id() == ID_symbol)
-  {
-    auto identifier = to_symbol_expr(function).get_identifier();
 
-    // malloc is special-cased
-    if(identifier == "malloc")
-    {
-      auto state = state_expr();
-      PRECONDITION(loc->call_arguments().size() == 1);
-      auto size_evaluated = evaluate_expr(loc, state, loc->call_arguments()[0]);
+  // Do we have a function body?
+  auto f = goto_functions.function_map.find(identifier);
+  if(f == goto_functions.function_map.end())
+    DATA_INVARIANT(false, "failed find function in function_map");
 
-      auto lhs_address = address_rec(loc, state, loc->call_lhs());
-      exprt new_state = ternary_exprt(
-        ID_allocate, state, lhs_address, size_evaluated, state_typet());
-      dest << forall_states_expr(
-        loc, function_application_exprt(out_state_expr(loc), {new_state}));
+  if(!f->second.body_available())
+  {
+    // 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
     {
-      // Do we have a function body?
-      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());
+      // This is a SKIP.
+      dest << equal_exprt(out_state_expr(loc), in_state_expr(loc));
+    }
+  }
 
-        const auto in_state = in_state_expr(loc);
+  // 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());
 
-        for(auto &argument : loc->call_arguments())
-          arguments_evaluated.add_to_operands(
-            evaluate_expr(loc, in_state, argument));
+  const auto in_state = in_state_expr(loc);
 
-        auto function_entry_state = state_expr_with_suffix(loc, "Entry");
+  for(auto &argument : loc->call_arguments())
+    arguments_evaluated.add_to_operands(
+      evaluate_expr(loc, in_state, argument));
 
-        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 function_entry_state = state_expr_with_suffix(loc, "Entry");
 
-          /*
-          auto &return_type = loc->call_lhs().type();
-          auto rhs_evaluated =
-            evaluate_expr(
-              loc,
-              return_state,
-              symbol_exprt("return_value", return_type));
+  dest << forall_states_expr(
+    loc,
+    function_application_exprt(function_entry_state, {state_expr()}));
 
-          multi_ary_exprt designator(ID_designator, { loc->call_lhs() }, typet());
+  // 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 lhs = out_state_expr(source);
+  /*
+  constraints.push_back(
+    multi_ary_exprt(
+      ID_goto_contract,
+      {loc->call_function(), in_state, return_state, arguments_evaluated},
+      bool_typet()));
+  */
 
-          auto rhs = update_exprt(
-            return_state,
-            designator,
-            rhs_evaluated);
+  // assign the return value, if any
+  if(loc->call_lhs().is_not_nil())
+  {
+    exprt equality_rhs = return_state;
 
-          // '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));
-        }
-      }
-    }
+    /*
+    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);
+  }
+*/
+}
+
+void state_encodingt::function_call(
+  const goto_functionst &goto_functions,
+  goto_programt::const_targett loc,
+  encoding_targett &dest)
+{
+  // Function pointer?
+  const auto &function = loc->call_function();
+  if(function.id() == ID_dereference)
+  {
+    // TBD.
+    throw incorrect_goto_program_exceptiont(
+      "can't do function pointers", loc->source_location());
+  }
+  else if(function.id() == ID_symbol)
+  {
+    function_call_symbol(goto_functions, loc, dest);
   }
   else
   {