Rearchitect var args support (making it actually work)

Previously all the logic to access values of variable argument lists was put
into our va_arg() implementation. This required guessing what the parameters
could have been, and did not take into account the initial value passed to
va_start.

Now va_start triggers constructing an array of pointers to parameters, the first
of which is the original argument to va_start. The va_list is then just a
pointer to the first element of the array. va_arg just increments the pointer.
goto_program conversion places a side_effect_exprt where va_start was, and
goto-symex populates the array with the actual values applicable for a
particular invocation of the function.

Author: tautschnig

Diff for: regression/cbmc/Variadic1/test.desc

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 main.c
 
 ^EXIT=0$

Diff for: regression/cbmc/va_list3/test.desc

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

Diff for: regression/cbmc/va_list3/windows-preprocessed.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE broken-smt-backend
 windows-preprocessed.i
 --winx64
 ^EXIT=0$

Diff for: src/ansi-c/expr2c.cpp

@@ -3617,8 +3617,8 @@ std::string expr2ct::convert_with_precedence(
       return convert_prob_uniform(src, precedence=16);
     else if(statement==ID_statement_expression)
       return convert_statement_expression(src, precedence=15);
-    else if(statement==ID_gcc_builtin_va_arg_next)
-      return convert_function(src, "gcc_builtin_va_arg_next");
+    else if(statement == ID_va_start)
+      return convert_function(src, CPROVER_PREFIX "va_start");
     else
       return convert_norep(src, precedence);
   }

Diff for: src/goto-instrument/goto_program2code.cpp

@@ -104,9 +104,10 @@ void goto_program2codet::scan_for_varargs()
       const exprt &l = target->get_assign().lhs();
       const exprt &r = target->get_assign().rhs();
 
-      // find va_arg_next
-      if(r.id()==ID_side_effect &&
-         to_side_effect_expr(r).get_statement()==ID_gcc_builtin_va_arg_next)
+      // find va_start
+      if(
+        r.id() == ID_side_effect &&
+        to_side_effect_expr(r).get_statement() == ID_va_start)
       {
         assert(r.has_operands());
         va_list_expr.insert(r.op0());
@@ -308,16 +309,17 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
 
     dest.add(std::move(f));
   }
-  else if(r.id()==ID_address_of)
+  else if(
+    r.id() == ID_side_effect &&
+    to_side_effect_expr(r).get_statement() == ID_va_start)
   {
     code_function_callt f(
-      symbol_exprt("va_start", code_typet({}, empty_typet())),
-      {this_va_list_expr, to_address_of_expr(r).object()});
+      symbol_exprt(ID_va_start, code_typet({}, empty_typet())),
+      {this_va_list_expr, to_address_of_expr(skip_typecast(r.op0())).object()});
 
     dest.add(std::move(f));
   }
-  else if(r.id()==ID_side_effect &&
-          to_side_effect_expr(r).get_statement()==ID_gcc_builtin_va_arg_next)
+  else if(r.id() == ID_plus)
   {
     code_function_callt f(
       symbol_exprt("va_arg", code_typet({}, empty_typet())),

Diff for: src/goto-programs/builtin_functions.cpp

@@ -1080,10 +1080,10 @@ void goto_convertt::do_function_call_symbol(
   else if(identifier==ID_gcc_builtin_va_arg)
   {
     // This does two things.
-    // 1) Move list pointer to next argument.
-    //    Done by gcc_builtin_va_arg_next.
-    // 2) Return value of argument.
+    // 1) Return value of argument.
     //    This is just dereferencing.
+    // 2) Move list pointer to next argument.
+    //    This is just an increment.
 
     if(arguments.size()!=1)
     {
@@ -1095,25 +1095,21 @@ void goto_convertt::do_function_call_symbol(
 
     exprt list_arg=make_va_list(arguments[0]);
 
-    {
-      side_effect_exprt rhs(
-        ID_gcc_builtin_va_arg_next,
-        list_arg.type(),
-        function.source_location());
-      rhs.copy_to_operands(list_arg);
-      rhs.set(ID_C_va_arg_type, to_code_type(function.type()).return_type());
-      dest.add(goto_programt::make_assignment(
-        list_arg, rhs, function.source_location()));
-    }
-
     if(lhs.is_not_nil())
     {
       typet t=pointer_type(lhs.type());
-      dereference_exprt rhs(typecast_exprt(list_arg, t), lhs.type());
+      dereference_exprt rhs{typecast_exprt(dereference_exprt{list_arg}, t)};
       rhs.add_source_location()=function.source_location();
       dest.add(
         goto_programt::make_assignment(lhs, rhs, function.source_location()));
     }
+
+    code_assignt assign{
+      list_arg, plus_exprt{list_arg, from_integer(1, pointer_diff_type())}};
+    assign.rhs().set(
+      ID_C_va_arg_type, to_code_type(function.type()).return_type());
+    dest.add(goto_programt::make_assignment(
+      std::move(assign), function.source_location()));
   }
   else if(identifier=="__builtin_va_copy")
   {
@@ -1138,7 +1134,7 @@ void goto_convertt::do_function_call_symbol(
     dest.add(goto_programt::make_assignment(
       dest_expr, src_expr, function.source_location()));
   }
-  else if(identifier=="__builtin_va_start")
+  else if(identifier == "__builtin_va_start" || identifier == "__va_start")
   {
     // Set the list argument to be the address of the
     // parameter argument.
@@ -1151,8 +1147,6 @@ void goto_convertt::do_function_call_symbol(
     }
 
     exprt dest_expr=make_va_list(arguments[0]);
-    const typecast_exprt src_expr(
-      address_of_exprt(arguments[1]), dest_expr.type());
 
     if(!is_lvalue(dest_expr))
     {
@@ -1161,8 +1155,13 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
+    side_effect_exprt rhs{
+      ID_va_start, dest_expr.type(), function.source_location()};
+    rhs.add_to_operands(
+      typecast_exprt{address_of_exprt{arguments[1]}, dest_expr.type()});
+
     dest.add(goto_programt::make_assignment(
-      dest_expr, src_expr, function.source_location()));
+      std::move(dest_expr), std::move(rhs), function.source_location()));
   }
   else if(identifier=="__builtin_va_end")
   {

Diff for: src/goto-symex/frame.h

@@ -26,6 +26,7 @@ struct framet
   irep_idt function_identifier;
   std::map<goto_programt::const_targett, goto_state_listt> goto_state_map;
   symex_targett::sourcet calling_location;
+  std::vector<irep_idt> parameter_names;
 
   goto_programt::const_targett end_of_function;
   exprt return_value = nil_exprt();

Diff for: src/goto-symex/goto_symex.h

@@ -610,10 +610,9 @@ class goto_symext
   /// \return The resulting expression
   static exprt add_to_lhs(const exprt &lhs, const exprt &what);
 
-  virtual void symex_gcc_builtin_va_arg_next(
-    statet &state,
-    const exprt &lhs,
-    const side_effect_exprt &code);
+  virtual void
+  symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &);
+
   /// Symbolically execute an assignment instruction that has an `allocate` on
   /// the right hand side
   /// \param state: Symbolic execution state for current instruction

Diff for: src/goto-symex/symex_assign.cpp

@@ -52,8 +52,8 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
       PRECONDITION(lhs.is_nil());
       symex_printf(state, side_effect_expr);
     }
-    else if(statement==ID_gcc_builtin_va_arg_next)
-      symex_gcc_builtin_va_arg_next(state, lhs, side_effect_expr);
+    else if(statement == ID_va_start)
+      symex_va_start(state, lhs, side_effect_expr);
     else
       UNREACHABLE;
   }

Diff for: src/goto-symex/symex_builtin_functions.cpp

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
+#include <util/expr_util.h>
+#include <util/fresh_symbol.h>
 #include <util/invariant_utils.h>
 #include <util/optional.h>
 #include <util/pointer_offset_size.h>
@@ -206,24 +208,44 @@ void goto_symext::symex_allocate(
     code_assignt(lhs, typecast_exprt::conditional_cast(rhs, lhs.type())));
 }
 
-irep_idt get_symbol(const exprt &src)
+/// Construct an entry for the var args array. Visual Studio complicates this as
+/// we need to put immediate values or pointers in there, depending on the size
+/// of the parameter.
+static exprt va_list_entry(
+  const irep_idt &parameter,
+  const pointer_typet &lhs_type,
+  const namespacet &ns)
 {
-  if(src.id()==ID_typecast)
-    return get_symbol(to_typecast_expr(src).op());
-  else if(src.id()==ID_address_of)
+  static const pointer_typet void_ptr_type = pointer_type(empty_typet{});
+
+  symbol_exprt parameter_expr = ns.lookup(parameter).symbol_expr();
+
+  // Visual Studio has va_list == char* and stores parameters of size no
+  // greater than the size of a pointer as immediate values
+  if(lhs_type.subtype().id() != ID_pointer)
   {
-    exprt op=to_address_of_expr(src).object();
-    if(op.id()==ID_symbol &&
-       op.get_bool(ID_C_SSA_symbol))
-      return to_ssa_expr(op).get_object_name();
-    else
-      return irep_idt();
+    auto parameter_size = size_of_expr(parameter_expr.type(), ns);
+    CHECK_RETURN(parameter_size.has_value());
+
+    binary_predicate_exprt fits_slot{
+      *parameter_size,
+      ID_le,
+      from_integer(lhs_type.get_width(), parameter_size->type())};
+
+    return if_exprt{
+      fits_slot,
+      typecast_exprt::conditional_cast(parameter_expr, void_ptr_type),
+      typecast_exprt::conditional_cast(
+        address_of_exprt{parameter_expr}, void_ptr_type)};
   }
   else
-    return irep_idt();
+  {
+    return typecast_exprt::conditional_cast(
+      address_of_exprt{std::move(parameter_expr)}, void_ptr_type);
+  }
 }
 
-void goto_symext::symex_gcc_builtin_va_arg_next(
+void goto_symext::symex_va_start(
   statet &state,
   const exprt &lhs,
   const side_effect_exprt &code)
@@ -233,42 +255,52 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
   if(lhs.is_nil())
     return; // ignore
 
-  // to allow constant propagation
-  exprt tmp = state.rename(code.op0(), ns).get();
-  do_simplify(tmp);
-  irep_idt id=get_symbol(tmp);
-
-  const auto zero = zero_initializer(lhs.type(), code.source_location(), ns);
-  CHECK_RETURN(zero.has_value());
-  exprt rhs(*zero);
+  // create an array holding pointers to the parameters, starting after the
+  // parameter that the operand points to
+  const exprt &op = skip_typecast(code.op0());
+  // this must be the address of a symbol
+  const irep_idt start_parameter =
+    to_ssa_expr(to_address_of_expr(op).object()).get_object_name();
 
-  if(!id.empty())
+  exprt::operandst va_arg_operands;
+  bool parameter_id_found = false;
+  for(auto &parameter : state.call_stack().top().parameter_names)
   {
-    // strip last name off id to get function name
-    std::size_t pos=id2string(id).rfind("::");
-    if(pos!=std::string::npos)
+    if(!parameter_id_found)
     {
-      irep_idt function_identifier=std::string(id2string(id), 0, pos);
-      std::string base=id2string(function_identifier)+"::va_arg";
-
-      if(has_prefix(id2string(id), base))
-        id=base+std::to_string(
-          safe_string2unsigned(
-            std::string(id2string(id), base.size(), std::string::npos))+1);
-      else
-        id=base+"0";
-
-      const symbolt *symbol;
-      if(!ns.lookup(id, symbol))
-      {
-        const symbol_exprt symbol_expr(symbol->name, symbol->type);
-        rhs = typecast_exprt::conditional_cast(
-          address_of_exprt(symbol_expr), lhs.type());
-      }
+      parameter_id_found = parameter == start_parameter;
+      continue;
     }
-  }
 
-  symex_assign(state, code_assignt(lhs, rhs));
+    va_arg_operands.push_back(
+      va_list_entry(parameter, to_pointer_type(lhs.type()), ns));
+  }
+  const std::size_t va_arg_size = va_arg_operands.size();
+  exprt array =
+    array_exprt{std::move(va_arg_operands),
+                array_typet{pointer_type(empty_typet{}),
+                            from_integer(va_arg_size, size_type())}};
+
+  symbolt &va_array = get_fresh_aux_symbol(
+    array.type(),
+    id2string(state.source.function_id),
+    "va_args",
+    state.source.pc->source_location,
+    ns.lookup(state.source.function_id).mode,
+    state.symbol_table);
+  va_array.value = array;
+
+  clean_expr(array, state, false);
+  array = state.rename(std::move(array), ns).get();
+  do_simplify(array);
+  symex_assign(state, code_assignt{va_array.symbol_expr(), std::move(array)});
+
+  exprt rhs = address_of_exprt{
+    index_exprt{va_array.symbol_expr(), from_integer(0, index_type())}};
+  rhs = state.rename(std::move(rhs), ns).get();
+  symex_assign(
+    state,
+    code_assignt{lhs, typecast_exprt::conditional_cast(rhs, lhs.type())});
 }
 
 irep_idt get_string_argument_rec(const exprt &src)

Diff for: src/goto-symex/symex_function_call.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
+#include <util/fresh_symbol.h>
 #include <util/invariant.h>
 #include <util/prefix.h>
 #include <util/range.h>
@@ -47,6 +48,7 @@ void goto_symext::parameter_assignments(
   {
     INVARIANT(
       !identifier.empty(), "function parameter must have an identifier");
+    state.call_stack().top().parameter_names.push_back(identifier);
 
     const symbolt &symbol=ns.lookup(identifier);
     symbol_exprt lhs=symbol.symbol_expr();
@@ -147,30 +149,20 @@ void goto_symext::parameter_assignments(
   if(function_type.has_ellipsis())
   {
     // These are va_arg arguments; their types may differ from call to call
-    std::size_t va_count=0;
-    const symbolt *va_sym=nullptr;
-    while(!ns.lookup(
-        id2string(function_identifier)+"::va_arg"+std::to_string(va_count),
-        va_sym))
-      ++va_count;
-
-    for( ; it1!=arguments.end(); it1++, va_count++)
+    for(; it1 != arguments.end(); it1++)
     {
-      irep_idt id=
-        id2string(function_identifier)+"::va_arg"+std::to_string(va_count);
-
-      // add to symbol table
-      symbolt symbol;
-      symbol.name=id;
-      symbol.base_name="va_arg"+std::to_string(va_count);
-      symbol.mode=ID_C;
-      symbol.type=it1->type();
-
-      state.symbol_table.insert(std::move(symbol));
-
-      symbol_exprt lhs=symbol_exprt(id, it1->type());
-
-      symex_assign(state, code_assignt(lhs, *it1));
+      symbolt &va_arg = get_fresh_aux_symbol(
+        it1->type(),
+        id2string(function_identifier),
+        "va_arg",
+        state.source.pc->source_location,
+        ns.lookup(function_identifier).mode,
+        state.symbol_table);
+      va_arg.is_parameter = true;
+
+      state.call_stack().top().parameter_names.push_back(va_arg.name);
+
+      symex_assign(state, code_assignt{va_arg.symbol_expr(), *it1});
     }
   }
   else if(it1!=arguments.end())

Diff for: src/util/irep_ids.def

@@ -303,7 +303,7 @@ IREP_ID_ONE(alignof)
 IREP_ID_ONE(clang_builtin_convertvector)
 IREP_ID_ONE(gcc_builtin_va_arg)
 IREP_ID_ONE(gcc_builtin_types_compatible_p)
-IREP_ID_ONE(gcc_builtin_va_arg_next)
+IREP_ID_ONE(va_start)
 IREP_ID_ONE(gcc_float16)
 IREP_ID_ONE(gcc_float32)
 IREP_ID_ONE(gcc_float32x)