Merge pull request #9081 from rod-chapman/set-char-signedness-in-contracts

Set signedness of "char *" casts to avoid cross-platform differences.

Author: tautschnig

regression/contracts-dfcc/chain.sh

@@ -21,6 +21,17 @@ else
   args_cbmc="${args#*" _ "}"
 fi
 
+# When the first instrumentation argument is --char-signedness-stability,
+# compile and instrument the test a second time with the opposite signedness
+# of plain char, and require the resulting goto functions to be identical.
+check_char_signedness_stability=0
+if [[ "$args_inst" == "--char-signedness-stability"* ]]
+then
+  check_char_signedness_stability=1
+  args_inst="${args_inst#--char-signedness-stability}"
+  args_inst="${args_inst# }"
+fi
+
 # An optional pre-processing pass with goto-instrument can be requested by
 # separating its arguments from the main instrumentation arguments using
 # " __ ", as in: --drop-unused-functions __ --dfcc main
@@ -50,7 +61,11 @@ fi
 if [[ "${is_windows}" == "true" ]]; then
   $goto_cc "${name}.c" "/Fe${name}${dfcc_suffix}.gb"
 else
-  $goto_cc -o "${name}${dfcc_suffix}.gb" "${name}.c"
+  signedness_flag=""
+  if [[ "$check_char_signedness_stability" == "1" ]]; then
+    signedness_flag="-fsigned-char"
+  fi
+  $goto_cc ${signedness_flag} -o "${name}${dfcc_suffix}.gb" "${name}.c"
 fi
 
 if [[ -n "$args_pre" ]]; then
@@ -77,5 +92,19 @@ fi
 if ! echo "${args_cbmc}" | grep -q -- --function ; then
   $goto_instrument --drop-unused-functions "${name}${dfcc_suffix}-mod.gb" "${name}${dfcc_suffix}-mod.gb"
 fi
+if [[ "$check_char_signedness_stability" == "1" ]]
+then
+  $goto_cc -funsigned-char -o "${name}-uchar.gb" "${name}.c"
+  $goto_instrument ${args_inst} "${name}-uchar.gb" "${name}-uchar-mod.gb"
+  $goto_instrument --show-goto-functions "${name}${dfcc_suffix}-mod.gb" | \
+    grep -v '^Reading' > "${name}-default.txt"
+  $goto_instrument --show-goto-functions "${name}-uchar-mod.gb" | \
+    grep -v '^Reading' > "${name}-uchar.txt"
+  if diff "${name}-default.txt" "${name}-uchar.txt"
+  then
+    echo "GOTO FUNCTIONS IDENTICAL ACROSS CHAR SIGNEDNESS"
+  fi
+  rm "${name}-default.txt" "${name}-uchar.txt"
+fi
 $goto_instrument --show-goto-functions "${name}${dfcc_suffix}-mod.gb"
 $cbmc --sat-solver cadical "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}

regression/contracts-dfcc/char_signedness_stability/main.c

@@ -0,0 +1,25 @@
+#include <stdlib.h>
+#include <string.h>
+
+int x;
+
+void foo(int *p) __CPROVER_requires(__CPROVER_is_fresh(p, sizeof(int)))
+  __CPROVER_assigns(*p, x) __CPROVER_ensures(*p == 42)
+{
+  *p = 42;
+  x = 1;
+}
+
+int main()
+{
+  int a[4], b[4];
+  memset(a, 0, sizeof(a));
+  memcpy(b, a, sizeof(a));
+  memmove(a, b, sizeof(a));
+  __CPROVER_havoc_slice(a, 2 * sizeof(int));
+
+  int *q = malloc(sizeof(int));
+  if(q)
+    foo(q);
+  return 0;
+}

regression/contracts-dfcc/char_signedness_stability/test.desc

@@ -0,0 +1,16 @@
+CORE dfcc-only gcc-only
+main.c
+--char-signedness-stability --dfcc main --enforce-contract foo
+^GOTO FUNCTIONS IDENTICAL ACROSS CHAR SIGNEDNESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test checks that the goto functions generated by DFCC instrumentation do
+not depend on the signedness of plain char, which is implementation-defined
+and differs between platforms (e.g. between Linux/aarch64 and macOS). It
+covers the contracts library (write set construction), the models of memset,
+memcpy and memmove, and the expansion of __CPROVER_havoc_slice.
+See: https://github.com/diffblue/cbmc/issues/8991

src/ansi-c/goto-conversion/builtin_functions.cpp

@@ -676,9 +676,13 @@ void goto_convertt::do_havoc_slice(
   }
 
   // insert instructions
-  // assert(rw_ok(argument[0], argument[1]));
-  // char nondet_contents[argument[1]];
-  // __CPROVER_array_replace(p, nondet_contents);
+  //  assert(rw_ok(argument[0], argument[1]));
+  //  unsigned char nondet_contents[argument[1]];
+  //  __CPROVER_array_replace(p, nondet_contents);
+  //
+  // Note that we use "unsigned char" explicitly here to force stable
+  // output on platforms where plain "char" is implementation-defined and signed
+  // by default
 
   r_or_w_ok_exprt ok_expr(ID_w_ok, arguments[0], arguments[1]);
   ok_expr.add_source_location() = source_location;
@@ -689,7 +693,8 @@ void goto_convertt::do_havoc_slice(
     "assertion havoc_slice " + from_expr(ns, identifier, ok_expr));
   dest.add(goto_programt::make_assertion(ok_expr, annotated_location));
 
-  const array_typet array_type(char_type(), simplify_expr(arguments[1], ns));
+  const array_typet array_type(
+    unsigned_char_type(), simplify_expr(arguments[1], ns));
 
   const symbolt &nondet_contents =
     new_tmp_symbol(array_type, "nondet_contents", dest, source_location, mode);

src/ansi-c/library/cprover_contracts.c

@@ -138,7 +138,7 @@ __CPROVER_HIDE:;
     !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
     "no offset bits overflow on CAR upper bound computation");
   return (__CPROVER_contracts_car_t){
-    .is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (char *)ptr + size};
+    ptr != 0, size, ptr, (unsigned char *)ptr + size};
 }
 
 /// \brief Initialises a __CPROVER_contracts_car_set_ptr_t object
@@ -187,7 +187,7 @@ __CPROVER_HIDE:;
     "no offset bits overflow on CAR upper bound computation");
   __CPROVER_contracts_car_t *elem = set->elems + idx;
   *elem = (__CPROVER_contracts_car_t){
-    .is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (char *)ptr + size};
+    ptr != 0, size, ptr, (unsigned char *)ptr + size};
 }
 
 /// \brief Invalidates all cars in the \p set that point into the same object
@@ -547,7 +547,7 @@ __CPROVER_HIDE:;
   __CPROVER_contracts_car_set_insert(
     &(set->contract_assigns),
     idx,
-    ((char *)ptr) - __CPROVER_POINTER_OFFSET(ptr),
+    ((unsigned char *)ptr) - __CPROVER_POINTER_OFFSET(ptr),
     __CPROVER_OBJECT_SIZE(ptr));
 }
 
@@ -832,7 +832,7 @@ __CPROVER_HIDE:;
   __CPROVER_assert(
     !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
     "no offset bits overflow on CAR upper bound computation");
-  void *ub = (void *)((char *)ptr + size);
+  void *ub = (void *)((unsigned char *)ptr + size);
   __CPROVER_contracts_car_t *elem = set->contract_assigns.elems;
   __CPROVER_size_t idx = set->contract_assigns.max_elems;
   __CPROVER_bool incl = 0;
@@ -925,7 +925,7 @@ __CPROVER_HIDE:;
 /// \param[in] set The write set to check the operation against
 /// \param[in] ptr Pointer to the havoced object
 /// \return True iff the range of bytes starting at
-/// `(char *)ptr - __CPROVER_POINTER_OFFSET(ptr)` and of size
+/// `(unsigned char *)ptr - __CPROVER_POINTER_OFFSET(ptr)` and of size
 /// `__CPROVER_OBJECT_SIZE(ptr)` is contained in `set->contract_assigns` or
 /// `set->allocated`.
 __CPROVER_bool __CPROVER_contracts_write_set_check_havoc_object(
@@ -935,7 +935,7 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_havoc_object(
 __CPROVER_HIDE:;
   return __CPROVER_contracts_write_set_check_assignment(
     set,
-    (char *)ptr - __CPROVER_POINTER_OFFSET(ptr),
+    (unsigned char *)ptr - __CPROVER_POINTER_OFFSET(ptr),
     __CPROVER_OBJECT_SIZE(ptr));
 }
 
@@ -1527,7 +1527,7 @@ __CPROVER_HIDE:;
     // this cast is safe because we prove that ub and lb are ordered
     __CPROVER_size_t max_offset = ub_offset - lb_offset;
     __CPROVER_assume(offset <= max_offset);
-    *ptr = (char *)lb + offset;
+    *ptr = (unsigned char *)lb + offset;
     __CPROVER_assert(
       write_set->linked_ptr_pred_ctx->ptr_pred != ptr,
       "__CPROVER_pointer_in_range_dfcc does not conflict with other pointer "

src/ansi-c/library/string.c

@@ -634,8 +634,8 @@ __CPROVER_HIDE:;
 #else
   __CPROVER_precondition(
     __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
-      ((const char *)src >= (const char *)dst + n) ||
-      ((const char *)dst >= (const char *)src + n),
+      ((const unsigned char *)src >= (const unsigned char *)dst + n) ||
+      ((const unsigned char *)dst >= (const unsigned char *)src + n),
     "memcpy src/dst overlap");
   __CPROVER_precondition(
     __CPROVER_r_ok(src, n), "memcpy source region readable");
@@ -644,10 +644,11 @@ __CPROVER_HIDE:;
 
   if(n > 0)
   {
-    //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
-    char src_n[n];
-    __CPROVER_array_copy(src_n, (char *)src);
-    __CPROVER_array_replace((char *)dst, src_n);
+    //for(__CPROVER_size_t i=0; i<n ; i++)
+    //  ((unsigned char *)dst)[i]=((const unsigned char *)src)[i];
+    unsigned char src_n[n];
+    __CPROVER_array_copy(src_n, (unsigned char *)src);
+    __CPROVER_array_replace((unsigned char *)dst, src_n);
   }
 #endif
 
@@ -681,8 +682,8 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C
 #else
   __CPROVER_precondition(
     __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) ||
-      ((const char *)src >= (const char *)dst + n) ||
-      ((const char *)dst >= (const char *)src + n),
+      ((const unsigned char *)src >= (const unsigned char *)dst + n) ||
+      ((const unsigned char *)dst >= (const unsigned char *)src + n),
     "memcpy src/dst overlap");
   __CPROVER_precondition(
     __CPROVER_r_ok(src, n), "memcpy source region readable");
@@ -692,10 +693,11 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C
 
   if(n > 0)
   {
-    //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
-    char src_n[n];
-    __CPROVER_array_copy(src_n, (char *)src);
-    __CPROVER_array_replace((char *)dst, src_n);
+    //for(__CPROVER_size_t i=0; i<n ; i++)
+    //  ((unsigned char *)dst)[i]=((const unsigned char *)src)[i];
+    unsigned char src_n[n];
+    __CPROVER_array_copy(src_n, (unsigned char *)src);
+    __CPROVER_array_replace((unsigned char *)dst, src_n);
   }
 #endif
   return dst;
@@ -857,9 +859,9 @@ void *memmove(void *dest, const void *src, size_t n)
 
   if(n > 0)
   {
-    char src_n[n];
-    __CPROVER_array_copy(src_n, (char *)src);
-    __CPROVER_array_replace((char *)dest, src_n);
+    unsigned char src_n[n];
+    __CPROVER_array_copy(src_n, (unsigned char *)src);
+    __CPROVER_array_replace((unsigned char *)dest, src_n);
   }
   #endif
   return dest;
@@ -903,9 +905,9 @@ void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_s
 
   if(n > 0)
   {
-    char src_n[n];
-    __CPROVER_array_copy(src_n, (char *)src);
-    __CPROVER_array_replace((char *)dest, src_n);
+    unsigned char src_n[n];
+    __CPROVER_array_copy(src_n, (unsigned char *)src);
+    __CPROVER_array_replace((unsigned char *)dest, src_n);
   }
   #endif
   return dest;