C front-end: type check arguments to built-in functions

We only sometimes did this, effectively relying on all other cases not
requiring any modifications to the expression by the type checker. The
case of passing an array to __CPROVER_{r,w}_ok showed that this wasn't
sufficient. Now fixed for all built-in functions handled by the type
checker.

Author: tautschnig

regression/cbmc/r_w_ok4/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int A[1];
+
+  assert(__CPROVER_r_ok(A, sizeof(int)));
+}

regression/cbmc/r_w_ok4/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_expr.cpp

@@ -2052,6 +2052,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt same_object_expr=
       same_object(expr.arguments()[0], expr.arguments()[1]);
     same_object_expr.add_source_location()=source_location;
@@ -2101,6 +2103,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt same_object_expr = is_invalid_pointer_exprt{expr.arguments().front()};
     same_object_expr.add_source_location()=source_location;
 
@@ -2115,6 +2119,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt buffer_size_expr("buffer_size", size_type());
     buffer_size_expr.operands()=expr.arguments();
     buffer_size_expr.add_source_location()=source_location;
@@ -2130,6 +2136,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     predicate_exprt is_zero_string_expr("is_zero_string");
     is_zero_string_expr.operands()=expr.arguments();
     is_zero_string_expr.set(ID_C_lvalue, true); // make it an lvalue
@@ -2146,6 +2154,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt zero_string_length_expr("zero_string_length", size_type());
     zero_string_length_expr.operands()=expr.arguments();
     zero_string_length_expr.set(ID_C_lvalue, true); // make it an lvalue
@@ -2162,6 +2172,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt is_dynamic_object_expr = is_dynamic_object_exprt(expr.arguments()[0]);
     is_dynamic_object_expr.add_source_location() = source_location;
 
@@ -2176,6 +2188,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt pointer_offset_expr=pointer_offset(expr.arguments().front());
     pointer_offset_expr.add_source_location()=source_location;
 
@@ -2190,6 +2204,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     unary_exprt object_size_expr(
       ID_object_size, expr.arguments()[0], size_type());
     object_size_expr.add_source_location() = source_location;
@@ -2205,6 +2221,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt pointer_object_expr = pointer_object(expr.arguments().front());
     pointer_object_expr.add_source_location() = source_location;
 
@@ -2214,15 +2232,15 @@ exprt c_typecheck_baset::do_special_functions(
           identifier=="__builtin_bswap32" ||
           identifier=="__builtin_bswap64")
   {
-    typecheck_function_call_arguments(expr);
-
     if(expr.arguments().size()!=1)
     {
       error().source_location = f_op.source_location();
       error() << identifier << " expects one operand" << eom;
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     // these are hard-wired to 8 bits according to the gcc manual
     bswap_exprt bswap_expr(expr.arguments().front(), 8, expr.type());
     bswap_expr.add_source_location()=source_location;
@@ -2231,15 +2249,15 @@ exprt c_typecheck_baset::do_special_functions(
   }
   else if(identifier=="__builtin_nontemporal_load")
   {
-    typecheck_function_call_arguments(expr);
-
     if(expr.arguments().size()!=1)
     {
       error().source_location = f_op.source_location();
       error() << identifier << " expects one operand" << eom;
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     // these return the subtype of the argument
     exprt &ptr_arg=expr.arguments().front();
 
@@ -2265,6 +2283,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     // This gets 5 integers followed by a float or double.
     // The five integers are the return values for the cases
     // FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL and FP_ZERO.
@@ -2311,6 +2331,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     isnan_exprt isnan_expr(expr.arguments().front());
     isnan_expr.add_source_location()=source_location;
 
@@ -2327,6 +2349,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     isfinite_exprt isfinite_expr(expr.arguments().front());
     isfinite_expr.add_source_location()=source_location;
 
@@ -2374,6 +2398,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     abs_exprt abs_expr(expr.arguments().front());
     abs_expr.add_source_location()=source_location;
 
@@ -2388,6 +2414,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     side_effect_exprt malloc_expr(ID_allocate, expr.type(), source_location);
     malloc_expr.operands()=expr.arguments();
 
@@ -2403,6 +2431,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     irep_idt id = identifier == CPROVER_PREFIX "r_ok" ? ID_r_ok : ID_w_ok;
 
     binary_predicate_exprt ok_expr(
@@ -2423,6 +2453,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     isinf_exprt isinf_expr(expr.arguments().front());
     isinf_expr.add_source_location()=source_location;
 
@@ -2437,6 +2469,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     // returns 1 for +inf and -1 for -inf, and 0 otherwise
 
     const exprt &fp_value = expr.arguments().front();
@@ -2464,6 +2498,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     const exprt &fp_value = expr.arguments()[0];
 
     if(fp_value.type().id() != ID_floatbv)
@@ -2492,6 +2528,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     sign_exprt sign_expr(expr.arguments().front());
     sign_expr.add_source_location()=source_location;
 
@@ -2511,6 +2549,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     popcount_exprt popcount_expr(expr.arguments().front(), expr.type());
     popcount_expr.add_source_location()=source_location;
 
@@ -2525,6 +2565,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     equal_exprt equality_expr(
       expr.arguments().front(), expr.arguments().back());
     equality_expr.add_source_location()=source_location;
@@ -2553,6 +2595,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     return typecast_exprt(expr.arguments()[0], expr.type());
   }
   else if(identifier=="__builtin_object_size")
@@ -2568,6 +2612,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     make_constant(expr.arguments()[1]);
 
     mp_integer arg1;
@@ -2610,6 +2656,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt arg0 =
       typecast_exprt::conditional_cast(expr.arguments()[0], bool_typet());
     make_constant(arg0);
@@ -2630,6 +2678,9 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    // do not typecheck the argument - it is never evaluated, and thus side
+    // effects must not show up either
+
     // try to produce constant
     exprt tmp1=expr.arguments().front();
     simplify(tmp1, *this);
@@ -2667,6 +2718,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt object=expr.arguments()[0];
 
     // The value doesn't matter at all, we only care about the type.
@@ -2739,6 +2792,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
+    typecheck_function_call_arguments(expr);
+
     exprt &ptr_arg=expr.arguments().front();
 
     if(ptr_arg.type().id()!=ID_pointer)