Improve printf formatter

.github/workflows/pull-request-checks.yaml

@@ -540,7 +540,7 @@ jobs:
           cd ../regression/cbmc
           sed -i '1s/^CORE\(.*\)broken-smt-backend/KNOWNBUG\1broken-smt-backend/' */*.desc
           # the following tests fail on Windows only
-          git checkout -- memory_allocation1 printf1 union12 va_list3
+          git checkout -- memory_allocation1 printf1 printf3 union12 va_list3
           ../test.pl -c "cbmc --cprover-smt2" -I broken-smt-backend -K
 
   # This job takes approximately 8 to 30 minutes

regression/cbmc/printf2/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+#include <stdio.h>
+
+int main()
+{
+  printf("results: %s, %d", "five", 5);
+  assert(0);
+}

regression/cbmc/printf2/test.desc

@@ -0,0 +1,8 @@
+CORE no-new-smt
+main.c
+--trace
+^results: five, 5$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/printf3/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdio.h>
+
+int main()
+{
+  printf("%ld", 10);
+  printf("%llu", 11);
+  printf("%hhd", 12);
+  printf("%lf", 10.0);
+  printf("%Lf", 11.0);
+  assert(0);
+}

regression/cbmc/printf3/test.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend no-new-smt
+main.c
+--trace
+^10$
+^11$
+^12$
+^10.0+$
+^11.0+$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-programs/printf_formatter.cpp

@@ -11,14 +11,15 @@
 
 #include "printf_formatter.h"
 
-#include <sstream>
-
 #include <util/c_types.h>
+#include <util/expr_util.h>
 #include <util/format_constant.h>
 #include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
+#include <sstream>
+
 const exprt printf_formattert::make_type(
   const exprt &src, const typet &dest)
 {
@@ -66,6 +67,8 @@
   format_constant.min_width=0;
   format_constant.zero_padding=false;
 
+  std::string length_modifier;
+
   char ch=next();
 
   if(ch=='0') // leading zeros
@@ -94,6 +97,56 @@
     }
   }
 
+  switch(ch)
+  {
+  case 'h':
+    ch = next();
+    if(ch == 'h')
+    {
+      length_modifier = "hh";
+      ch = next();
+    }
+    else
+    {
+      length_modifier = "h";
+    }
+    break;
+
+  case 'l':
+    ch = next();
+    if(ch == 'l')
+    {
+      length_modifier = "ll";
+      ch = next();
+    }
+    else
+    {
+      length_modifier = "l";
+    }
+    break;
+
+  case 'q':
+    ch = next();
+    length_modifier = "ll";
+    break;
+
+  case 'L':
+  case 'j':
+  case 'z':
+  case 't':
+    length_modifier = ch;
+    ch = next();
+    break;
+
+  case 'Z':
+    ch = next();
+    length_modifier = "z";
+    break;
+
+  default:
+    break;
+  }
+
   switch(ch)
   {
   case '%':
@@ -105,17 +158,23 @@
     format_constant.style=format_spect::stylet::SCIENTIFIC;
     if(next_operand==operands.end())
       break;
-    out << format_constant(
-      make_type(*(next_operand++), double_type()));
+    if(length_modifier == "L")
+      out << format_constant(make_type(*(next_operand++), long_double_type()));
+    else
+      out << format_constant(make_type(*(next_operand++), double_type()));
     break;
 
+  case 'a': // TODO: hexadecimal output
+  case 'A': // TODO: hexadecimal output
   case 'f':
   case 'F':
     format_constant.style=format_spect::stylet::DECIMAL;
     if(next_operand==operands.end())
       break;
-    out << format_constant(
-      make_type(*(next_operand++), double_type()));
+    if(length_modifier == "L")
+      out << format_constant(make_type(*(next_operand++), long_double_type()));
+    else
+      out << format_constant(make_type(*(next_operand++), double_type()));
     break;
 
   case 'g':
@@ -125,58 +184,130 @@
       format_constant.precision=1;
     if(next_operand==operands.end())
       break;
-    out << format_constant(
-      make_type(*(next_operand++), double_type()));
+    if(length_modifier == "L")
+      out << format_constant(make_type(*(next_operand++), long_double_type()));
+    else
+      out << format_constant(make_type(*(next_operand++), double_type()));
     break;
 
+  case 'S':
+    length_modifier = 'l';
   case 's':
     {
       if(next_operand==operands.end())
         break;
       // this is the address of a string
       const exprt &op=*(next_operand++);
       if(
-        op.id() == ID_address_of &&
-        to_address_of_expr(op).object().id() == ID_index &&
-        to_index_expr(to_address_of_expr(op).object()).array().id() ==
-          ID_string_constant)
+        auto pointer_constant =
+          expr_try_dynamic_cast<annotated_pointer_constant_exprt>(op))
       {
-        out << format_constant(
-          to_index_expr(to_address_of_expr(op).object()).array());
+        if(
+          auto address_of = expr_try_dynamic_cast<address_of_exprt>(
+            skip_typecast(pointer_constant->symbolic_pointer())))
+        {
+          if(address_of->object().id() == ID_string_constant)
+          {
+            out << format_constant(address_of->object());
+          }
+          else if(
+            auto index_expr =
+              expr_try_dynamic_cast<index_exprt>(address_of->object()))
+          {
+            if(
+              index_expr->index().is_zero() &&
+              index_expr->array().id() == ID_string_constant)
+            {
+              out << format_constant(index_expr->array());
+            }
+          }
+        }
       }
     }
     break;
 
   case 'd':
+  case 'i':
+  {
     if(next_operand==operands.end())
       break;
-    out << format_constant(
-      make_type(*(next_operand++), signed_int_type()));
+    typet conversion_type;
+    if(length_modifier == "hh")
+      conversion_type = signed_char_type();
+    else if(length_modifier == "h")
+      conversion_type = signed_short_int_type();
+    else if(length_modifier == "l")
+      conversion_type = signed_long_int_type();
+    else if(length_modifier == "ll")
+      conversion_type = signed_long_long_int_type();
+    else if(length_modifier == "j") // intmax_t
+      conversion_type = signed_long_long_int_type();
+    else if(length_modifier == "z")
+      conversion_type = signed_size_type();
+    else if(length_modifier == "t")
+      conversion_type = pointer_diff_type();
+    else
+      conversion_type = signed_int_type();
+    out << format_constant(make_type(*(next_operand++), conversion_type));
+  }
     break;
 
-  case 'D':
-    if(next_operand==operands.end())
-      break;
-    out << format_constant(
-      make_type(*(next_operand++), signed_long_int_type()));
+    case 'o': // TODO: octal output
+    case 'x': // TODO: hexadecimal output
+    case 'X': // TODO: hexadecimal output
+    case 'u':
+    {
+      if(next_operand == operands.end())
+        break;
+      typet conversion_type;
+      if(length_modifier == "hh")
+        conversion_type = unsigned_char_type();
+      else if(length_modifier == "h")
+        conversion_type = unsigned_short_int_type();
+      else if(length_modifier == "l")
+        conversion_type = unsigned_long_int_type();
+      else if(length_modifier == "ll")
+        conversion_type = unsigned_long_long_int_type();
+      else if(length_modifier == "j") // intmax_t
+        conversion_type = unsigned_long_long_int_type();
+      else if(length_modifier == "z")
+        conversion_type = size_type();
+      else if(length_modifier == "t")
+        conversion_type = pointer_diff_type();
+      else
+        conversion_type = unsigned_int_type();
+      out << format_constant(make_type(*(next_operand++), conversion_type));
+    }
     break;
 
-  case 'u':
-    if(next_operand==operands.end())
+    case 'C':
+      length_modifier = 'l';
+    case 'c':
+      if(next_operand == operands.end())
+        break;
+      if(length_modifier == "l")
+        out << format_constant(make_type(*(next_operand++), wchar_t_type()));
+      else
+        out << format_constant(
+          make_type(*(next_operand++), unsigned_char_type()));
       break;
-    out << format_constant(
-      make_type(*(next_operand++), unsigned_int_type()));
-    break;
 
-  case 'U':
-    if(next_operand==operands.end())
+    case 'p':
+      // TODO: hexadecimal output
+      out << format_constant(make_type(*(next_operand++), size_type()));
       break;
-    out << format_constant(
-      make_type(*(next_operand++), unsigned_long_int_type()));
-    break;
 
-  default:
-    out << '%' << ch;
+    case 'n':
+      if(next_operand == operands.end())
+        break;
+      // printf would store the number of characters written so far in the
+      // object pointed to by this operand. We do not implement this side-effect
+      // here, and just skip one operand.
+      ++next_operand;
+      break;
+
+    default:
+      out << '%' << ch;
   }
 }
 

src/goto-symex/symex_builtin_functions.cpp

@@ -397,10 +397,16 @@ void goto_symext::symex_printf(
       return;
     }
 
+    // Visual Studio has va_list == char*, else we have va_list == void** and
+    // need to add dereferencing
+    const bool need_deref =
+      operands.back().type().id() == ID_pointer &&
+      to_pointer_type(operands.back().type()).base_type().id() == ID_pointer;
+
     for(const auto &op : va_args->operands())
     {
       exprt parameter = skip_typecast(op);
-      if(parameter.id() == ID_address_of)
+      if(need_deref && 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();