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

regression/cbmc/Variadic1/test.desc

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

regression/cbmc/va_list3/test.desc

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

src/ansi-c/expr2c.cpp

@@ -3668,8 +3668,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", precedence=16);
+    else if(statement == ID_gcc_builtin_va_start)
+      return convert_function(src, "gcc_builtin_va_start", precedence = 16);
     else
       return convert_norep(src, precedence);
   }

src/goto-instrument/goto_program2code.cpp

@@ -105,9 +105,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_gcc_builtin_va_start)
       {
         assert(r.has_operands());
         va_list_expr.insert(r.op0());
@@ -327,17 +328,18 @@ 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_gcc_builtin_va_start)
   {
     code_function_callt f(
       symbol_exprt("va_start", code_typet({}, empty_typet())),
-      {this_va_list_expr, to_address_of_expr(r).object()});
+      {this_va_list_expr, to_address_of_expr(skip_typecast(r.op0())).object()});
     f.arguments().front().type().id(ID_gcc_builtin_va_list);
 
     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())),

src/goto-programs/builtin_functions.cpp

@@ -1100,26 +1100,20 @@ 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());
-      goto_programt::targett t1=dest.add_instruction(ASSIGN);
-      t1->source_location=function.source_location();
-      t1->code=code_assignt(list_arg, rhs);
-    }
+    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()));
 
     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();
-      goto_programt::targett t2=dest.add_instruction(ASSIGN);
-      t2->source_location=function.source_location();
-      t2->code=code_assignt(lhs, rhs);
+      dest.add(goto_programt::make_assignment(
+        lhs, std::move(rhs), function.source_location()));
     }
   }
   else if(identifier=="__builtin_va_copy")
@@ -1159,8 +1153,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))
     {
@@ -1169,9 +1161,13 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
-    goto_programt::targett t=dest.add_instruction(ASSIGN);
-    t->source_location=function.source_location();
-    t->code=code_assignt(dest_expr, src_expr);
+    side_effect_exprt rhs{
+      ID_gcc_builtin_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(
+      std::move(dest_expr), std::move(rhs), function.source_location()));
   }
   else if(identifier=="__builtin_va_end")
   {

src/goto-symex/goto_symex.h

@@ -374,8 +374,10 @@ 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 &, const exprt &lhs, const side_effect_exprt &);
+  virtual void symex_gcc_builtin_va_start(
+    statet &,
+    const exprt &lhs,
+    const side_effect_exprt &);
   virtual void symex_allocate(
     statet &, const exprt &lhs, const side_effect_exprt &);
   virtual void symex_cpp_delete(statet &, const codet &);

src/goto-symex/goto_symex_state.h

@@ -90,6 +90,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();

src/goto-symex/symex_assign.cpp

@@ -51,8 +51,8 @@ void goto_symext::symex_assign(
       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_gcc_builtin_va_start)
+      symex_gcc_builtin_va_start(state, lhs, side_effect_expr);
     else
       UNREACHABLE;
   }

src/goto-symex/symex_builtin_functions.cpp

@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #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>
@@ -203,24 +205,7 @@ void goto_symext::symex_allocate(
     code_assignt(lhs, typecast_exprt::conditional_cast(rhs, lhs.type())));
 }
 
-irep_idt get_symbol(const exprt &src)
-{
-  if(src.id()==ID_typecast)
-    return get_symbol(to_typecast_expr(src).op());
-  else if(src.id()==ID_address_of)
-  {
-    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();
-  }
-  else
-    return irep_idt();
-}
-
-void goto_symext::symex_gcc_builtin_va_arg_next(
+void goto_symext::symex_gcc_builtin_va_start(
   statet &state,
   const exprt &lhs,
   const side_effect_exprt &code)
@@ -230,42 +215,48 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
   if(lhs.is_nil())
     return; // ignore
 
-  exprt tmp=code.op0();
-  state.rename(tmp, ns); // to allow constant propagation
-  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 with 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_symbol_expr(to_address_of_expr(op).object()).get_identifier();
 
-  if(!id.empty())
+  exprt::operandst va_arg_operands;
+  bool parameter_id_found = false;
+  for(auto &parameter : state.top().parameter_names)
   {
-    // strip last name off id to get function name
-    std::size_t pos=id2string(id).rfind("::");
-    if(pos!=std::string::npos)
-    {
-      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());
-      }
-    }
-  }
+    if(!parameter_id_found && parameter == start_parameter)
+      parameter_id_found = true;
 
-  symex_assign(state, code_assignt(lhs, rhs));
+    va_arg_operands.push_back(typecast_exprt::conditional_cast(
+      address_of_exprt{ns.lookup(parameter).symbol_expr()},
+      pointer_type(empty_typet{})));
+  }
+  const std::size_t va_arg_size = va_arg_operands.size();
+  array_exprt array{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;
+
+  state.rename(array, ns);
+  do_simplify(array);
+  symex_assign(state, code_assignt{va_array.symbol_expr(), std::move(array)});
+
+  address_of_exprt rhs{
+    index_exprt{va_array.symbol_expr(), from_integer(0, index_type())}};
+  state.rename(rhs, ns);
+  symex_assign(
+    state,
+    code_assignt{lhs, typecast_exprt::conditional_cast(rhs, lhs.type())});
 }
 
 irep_idt get_string_argument_rec(const exprt &src)

src/goto-symex/symex_function_call.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
+#include <util/fresh_symbol.h>
 #include <util/invariant.h>
 
 static void locality(
@@ -60,6 +61,7 @@ void goto_symext::parameter_assignments(
     INVARIANT(
       !identifier.empty(),
       "function pointer parameter must have an identifier");
+    state.top().parameter_names.push_back(identifier);
 
     const symbolt &symbol=ns.lookup(identifier);
     symbol_exprt lhs=symbol.symbol_expr();
@@ -156,30 +158,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.top().parameter_names.push_back(va_arg.name);
+
+      symex_assign(state, code_assignt{va_arg.symbol_expr(), *it1});
     }
   }
   else if(it1!=arguments.end())