Move printf to C library and support return values

Code using var = printf(...); (printf does return a value!) previously
resulted in a failing invariant as the symex_assign code assumed the lhs
always was nil.  Since symex does not know how to generate a proper
return value, make __CPROVER_printf a void-typed built-in and model
printf around it. Clean up the corresponding goto-convert code.

Author: tautschnig

doc/cprover-manual/api.md

@@ -62,6 +62,16 @@ using nondeterminism, as described [here](../modeling/nondeterminism/)). The
 string constant is followed by an arbitrary number of values of
 arbitrary types.
 
+#### \_\_CPROVER\_printf
+
+```C
+void __CPROVER_printf(const char *format, ...);
+```
+
+The function **\_\_CPROVER\_printf** implements the C `printf` function (without
+any return value). The observable effect is that its output is shown within a
+counterexample trace.
+
 #### \_\_CPROVER\_cover
 
 ```C

regression/cbmc-library/printf-01/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdio.h>
+
+int main()
+{
+  int x;
+  x = printf("x");
+  assert(x < 0);
+  return 0;
+}

regression/cbmc-library/printf-01/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=10$
+^SIGNAL=0$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/printf1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --trace
 ^EXIT=10$

src/ansi-c/cprover_builtin_headers.h

@@ -22,6 +22,7 @@ void __CPROVER_cleanup(const void *, const void *);
 __CPROVER_bool __CPROVER_get_must(const void *, const char *);
 __CPROVER_bool __CPROVER_get_may(const void *, const char *);
 
+void __CPROVER_printf(const char *format, ...);
 void __CPROVER_input(const char *id, ...);
 void __CPROVER_output(const char *id, ...);
 void __CPROVER_cover(__CPROVER_bool condition);

src/ansi-c/library/cprover.h

@@ -38,6 +38,8 @@ void __CPROVER_initialize(void);
 void __CPROVER_cover(__CPROVER_bool condition);
 #endif
 
+// NOLINTNEXTLINE(build/deprecated)
+void __CPROVER_printf(const char *format, ...);
 void __CPROVER_input(const char *id, ...);
 void __CPROVER_output(const char *id, ...);
 

src/ansi-c/library/stdio.c

@@ -22,7 +22,7 @@ inline int putchar(int c)
 {
   __CPROVER_HIDE:;
   __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
-  printf("%c", c);
+  __CPROVER_printf("%c", c);
   return (error?-1:c);
 }
 
@@ -41,7 +41,7 @@ inline int puts(const char *s)
   __CPROVER_HIDE:;
   __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
   int ret=__VERIFIER_nondet_int();
-  printf("%s\n", s);
+  __CPROVER_printf("%s\n", s);
   if(error) ret=-1; else __CPROVER_assume(ret>=0);
   return ret;
 }
@@ -768,7 +768,7 @@ void perror(const char *s)
     #endif
     // should go to stderr
     if(s[0]!=0)
-      printf("%s: ", s);
+      __CPROVER_printf("%s: ", s);
   }
 
   // TODO: print errno error
@@ -921,6 +921,31 @@ inline int vsscanf(const char *restrict s, const char *restrict format, va_list
   return result;
 }
 
+/* FUNCTION: printf */
+
+#ifndef __CPROVER_STDIO_H_INCLUDED
+#  include <stdio.h>
+#  define __CPROVER_STDIO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDARG_H_INCLUDED
+#  include <stdarg.h>
+#  define __CPROVER_STDARG_H_INCLUDED
+#endif
+
+int __VERIFIER_nondet_int();
+
+inline int printf(const char *format, ...)
+{
+__CPROVER_HIDE:;
+  int result = __VERIFIER_nondet_int();
+  va_list list;
+  va_start(list, format);
+  __CPROVER_printf(format, list);
+  va_end(list);
+  return result;
+}
+
 /* FUNCTION: fprintf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED

src/goto-programs/builtin_functions.cpp

@@ -203,33 +203,10 @@ void goto_convertt::do_printf(
 {
   const irep_idt &f_id = function.get_identifier();
 
-  if(f_id==CPROVER_PREFIX "printf" ||
-     f_id=="printf")
-  {
-    const typet &return_type = to_code_type(function.type()).return_type();
-    side_effect_exprt printf_code(
-      ID_printf, return_type, function.source_location());
-
-    printf_code.operands()=arguments;
-    printf_code.add_source_location()=function.source_location();
+  PRECONDITION(f_id == CPROVER_PREFIX "printf");
 
-    if(lhs.is_not_nil())
-    {
-      code_assignt assignment(lhs, printf_code);
-      assignment.add_source_location()=function.source_location();
-      copy(assignment, ASSIGN, dest);
-    }
-    else
-    {
-      printf_code.id(ID_code);
-      printf_code.type() = code_typet(
-        code_typet::parameterst(to_code_type(function.type()).parameters()),
-        empty_typet());
-      copy(to_code(printf_code), OTHER, dest);
-    }
-  }
-  else
-    UNREACHABLE;
+  codet printf_code(ID_printf, arguments, function.source_location());
+  copy(printf_code, OTHER, dest);
 }
 
 void goto_convertt::do_scanf(
@@ -927,15 +904,6 @@ void goto_convertt::do_function_call_symbol(
   {
     do_array_op(ID_array_replace, lhs, function, arguments, dest);
   }
-  else if(identifier=="printf")
-  /*
-          identifier=="fprintf" ||
-          identifier=="sprintf" ||
-          identifier=="snprintf")
-  */
-  {
-    do_printf(lhs, function, arguments, dest);
-  }
   else if(identifier=="__assert_fail" ||
           identifier=="_assert" ||
           identifier=="__assert_c99" ||

src/goto-symex/symex_assign.cpp

@@ -45,11 +45,6 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
       symex_cpp_new(state, lhs, side_effect_expr);
     else if(statement==ID_allocate)
       symex_allocate(state, lhs, side_effect_expr);
-    else if(statement==ID_printf)
-    {
-      PRECONDITION(lhs.is_nil());
-      symex_printf(state, side_effect_expr);
-    }
     else if(statement == ID_va_start)
       symex_va_start(state, lhs, side_effect_expr);
     else

src/goto-symex/symex_builtin_functions.cpp

@@ -303,19 +303,19 @@ void goto_symext::symex_va_start(
     code_assignt{lhs, typecast_exprt::conditional_cast(rhs, lhs.type())});
 }
 
-irep_idt get_string_argument_rec(const exprt &src)
+static irep_idt get_string_argument_rec(const exprt &src)
 {
   if(src.id()==ID_typecast)
   {
-    PRECONDITION(src.operands().size() == 1);
-    return get_string_argument_rec(src.op0());
+    return get_string_argument_rec(to_typecast_expr(src).op());
   }
   else if(src.id()==ID_address_of)
   {
-    PRECONDITION(src.operands().size() == 1);
-    if(src.op0().id()==ID_index)
+    const exprt &object = to_address_of_expr(src).object();
+
+    if(object.id() == ID_index)
     {
-      const auto &index_expr = to_index_expr(src.op0());
+      const auto &index_expr = to_index_expr(object);
 
       if(
         index_expr.array().id() == ID_string_constant &&
@@ -325,32 +325,91 @@ irep_idt get_string_argument_rec(const exprt &src)
         return to_string_constant(fmt_str).get_value();
       }
     }
+    else if(object.id() == ID_string_constant)
+    {
+      return to_string_constant(object).get_value();
+    }
   }
 
   return irep_idt();
 }
 
-irep_idt get_string_argument(const exprt &src, const namespacet &ns)
+static irep_idt get_string_argument(const exprt &src, const namespacet &ns)
 {
   exprt tmp=src;
   simplify(tmp, ns);
   return get_string_argument_rec(tmp);
 }
 
+/// Return an expression if \p operands fulfills all criteria that we expect of
+/// the expression to be a variable argument list.
+static optionalt<exprt> get_va_args(const exprt::operandst &operands)
+{
+  if(operands.size() != 2)
+    return {};
+
+  const exprt &second_op = skip_typecast(operands.back());
+  if(second_op.id() != ID_address_of)
+    return {};
+
+  if(second_op.type() != pointer_type(pointer_type(empty_typet{})))
+    return {};
+
+  const exprt &object = to_address_of_expr(second_op).object();
+  if(object.id() != ID_index)
+    return {};
+
+  const index_exprt &index_expr = to_index_expr(object);
+  if(!index_expr.index().is_zero())
+    return {};
+  else
+    return index_expr.array();
+}
+
 void goto_symext::symex_printf(
   statet &state,
   const exprt &rhs)
 {
   PRECONDITION(!rhs.operands().empty());
 
-  exprt tmp_rhs = state.rename(rhs, ns).get();
+  exprt tmp_rhs = rhs;
+  clean_expr(tmp_rhs, state, false);
+  tmp_rhs = state.rename(std::move(tmp_rhs), ns).get();
   do_simplify(tmp_rhs);
 
   const exprt::operandst &operands=tmp_rhs.operands();
   std::list<exprt> args;
 
-  for(std::size_t i=1; i<operands.size(); i++)
-    args.push_back(operands[i]);
+  // we either have any number of operands or a va_list as second operand
+  optionalt<exprt> va_args = get_va_args(operands);
+
+  if(!va_args.has_value())
+  {
+    args.insert(args.end(), std::next(operands.begin()), operands.end());
+  }
+  else
+  {
+    clean_expr(*va_args, state, false);
+    *va_args = state.rename(*va_args, ns).get();
+    if(va_args->id() != ID_array)
+    {
+      // we were not able to constant-propagate va_args, and thus don't have
+      // sufficient information to generate printf -- give up
+      return;
+    }
+
+    for(const auto &op : va_args->operands())
+    {
+      exprt parameter = skip_typecast(op);
+      if(parameter.id() == ID_address_of)
+        parameter = to_address_of_expr(parameter).object();
+      clean_expr(parameter, state, false);
+      parameter = state.rename(std::move(parameter), ns).get();
+      do_simplify(parameter);
+
+      args.push_back(std::move(parameter));
+    }
+  }
 
   const irep_idt format_string=
     get_string_argument(operands[0], ns);