Add minimal example demonstrating -fno-strict-aliasing

.gitignore

@@ -62,6 +62,15 @@ compcert/doc/html/
 compcert/extraction/
 compcert/test/
 
+progs/alias
+progs/alias.compcert.c
+progs/alias.i
+progs/alias.parsed.c
+progs64/alias
+progs64/alias.compcert.c
+progs64/alias.i
+progs64/alias.parsed.c
+
 *.vo
 *.vos
 *.vok

Makefile

@@ -499,7 +499,8 @@ PROGS32_FILES= \
   libglob.v verif_libglob.v peel.v verif_peel.v \
   printf.v stackframe_demo.v verif_stackframe_demo.v \
 	rotate.v verif_rotate.v \
-  verif_objectSelf.v verif_objectSelfFancy.v verif_objectSelfFancyOverriding.v
+  verif_objectSelf.v verif_objectSelfFancy.v verif_objectSelfFancyOverriding.v \
+  alias.v verif_alias.v
 # verif_insertion_sort.v
 
 C64_ORDINARY = reverse.c revarray.c sumarray.c append.c bin_search.c \
@@ -513,7 +514,8 @@ V64_ORDINARY = verif_reverse2.v verif_revarray.v verif_sumarray.v \
     verif_bst.v verif_field_loadstore.v verif_float.v verif_object.v \
     verif_global.v verif_min.v verif_min64.v verif_nest2.v verif_nest3.v \
     verif_logical_compare.v \
-    verif_strlib.v verif_switch.v verif_union.v verif_message.v verif_incr.v
+    verif_strlib.v verif_switch.v verif_union.v verif_message.v verif_incr.v \
+    alias.v verif_alias.v
 
 SHA_FILES= \
   general_lemmas.v SHA256.v common_lemmas.v pure_lemmas.v sha_lemmas.v functional_prog.v \

progs/alias.c

@@ -0,0 +1,77 @@
+long foo(long *p, void **q) {
+  *p = 1;
+  *q = 0;
+  return *p;
+}
+int main() {
+  long x;
+  return foo(&x, &x);
+}
+
+/*
+The usage in this canonical example is essential to systems programming but has
+undefined behavior according to ISO C due to the strict aliasing restriction.
+
+From the perspective that pointers are addresses and memory maps addresses to
+bytes, we have two writes and one read of the same 4-byte memory region, and
+main returns 0. Yet ISO C17 § 6.5.7 limits the lvalue types through which the
+value of a declared object can be accessed to a fixed list of variations on the
+declared type plus char. Here the declared type is long, so the modification
+through *p is consistent with these rules, but the modification through *q (of
+type void*) is not, even though long and void* have the same size and alignment.
+The ubiquitous compiler flag -fno-strict-aliasing lifts these restrictions.
+
+VST is proved sound only for CompCert, which always uses -fno-strict-aliasing.
+While VST also enforces many other additional requirements of the C standard,
+it is not sound for use with other compilers without -fno-strict-aliasing.
+
+To show that this complication is relevant in practice, the example was tested
+using clang 14.0.6, gcc 12.2.0, and CompCert a1f01c84 (3.11++).
+
+It returns 0 in the following invocations:
+
+clang -m32 -O0 -w alias.c -o alias && ./alias; echo $?
+gcc   -m32 -O0 -w alias.c -o alias && ./alias; echo $?
+gcc   -m32 -O1 -w alias.c -o alias && ./alias; echo $?
+clang -m32 -fno-strict-aliasing -O1 -w alias.c -o alias && ./alias; echo $?
+clang -m32 -fno-strict-aliasing -O2 -w alias.c -o alias && ./alias; echo $?
+clang -m32 -fno-strict-aliasing -O3 -w alias.c -o alias && ./alias; echo $?
+gcc   -m32 -fno-strict-aliasing -O2 -w alias.c -o alias && ./alias; echo $?
+gcc   -m32 -fno-strict-aliasing -O3 -w alias.c -o alias && ./alias; echo $?
+
+It also returns 0 with CompCert:
+
+../../CompCert/ccomp alias.c -c alias.o && gcc -m32 alias.o -o alias && ./alias; echo $?
+../../CompCert/ccomp -interp alias.c
+
+It returns 1 in the following invocations:
+
+clang -m32 -O1 -w alias.c -o alias && ./alias; echo $?
+clang -m32 -O2 -w alias.c -o alias && ./alias; echo $?
+clang -m32 -O3 -w alias.c -o alias && ./alias; echo $?
+gcc   -m32 -O2 -w alias.c -o alias && ./alias; echo $?
+gcc   -m32 -O3 -w alias.c -o alias && ./alias; echo $?
+
+alias.v was generated using the following invocation:
+
+../../CompCert/clightgen -dclight -normalize -nostdinc -P -std=c11 alias.c
+
+The corresponding clight file returns 0 in all invocations where the input file returned 0:
+
+clang -m32 -O0 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -m32 -O0 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -m32 -O1 -w alias.light.c -o alias && ./alias; echo $?
+clang -m32 -fno-strict-aliasing -O1 -w alias.light.c -o alias && ./alias; echo $?
+clang -m32 -fno-strict-aliasing -O2 -w alias.light.c -o alias && ./alias; echo $?
+clang -m32 -fno-strict-aliasing -O3 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -m32 -fno-strict-aliasing -O2 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -m32 -fno-strict-aliasing -O3 -w alias.light.c -o alias && ./alias; echo $?
+
+... and returns 1 in all invocations where the input file returned 1:
+
+clang -m32 -O1 -w alias.light.c -o alias && ./alias; echo $?
+clang -m32 -O2 -w alias.light.c -o alias && ./alias; echo $?
+clang -m32 -O3 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -m32 -O2 -w alias.light.c -o alias && ./alias; echo $?
+gcc   -m32 -O3 -w alias.light.c -o alias && ./alias; echo $?
+*/

progs/alias.light.c

@@ -0,0 +1,41 @@
+extern unsigned int __compcert_va_int32(void *);
+extern unsigned long long __compcert_va_int64(void *);
+extern double __compcert_va_float64(void *);
+extern void *__compcert_va_composite(void *, unsigned int);
+extern long long __compcert_i64_dtos(double);
+extern unsigned long long __compcert_i64_dtou(double);
+extern double __compcert_i64_stod(long long);
+extern double __compcert_i64_utod(unsigned long long);
+extern float __compcert_i64_stof(long long);
+extern float __compcert_i64_utof(unsigned long long);
+extern long long __compcert_i64_sdiv(long long, long long);
+extern unsigned long long __compcert_i64_udiv(unsigned long long, unsigned long long);
+extern long long __compcert_i64_smod(long long, long long);
+extern unsigned long long __compcert_i64_umod(unsigned long long, unsigned long long);
+extern long long __compcert_i64_shl(long long, int);
+extern unsigned long long __compcert_i64_shr(unsigned long long, int);
+extern long long __compcert_i64_sar(long long, int);
+extern long long __compcert_i64_smulh(long long, long long);
+extern unsigned long long __compcert_i64_umulh(unsigned long long, unsigned long long);
+extern void __builtin_debug(int, ...);
+int foo(int *, void **);
+int main(void);
+int foo(int *$p, void **$q)
+{
+  register int $128;
+  *$p = 1;
+  *$q = 0;
+  $128 = *$p;
+  return $128;
+}
+
+int main(void)
+{
+  int x;
+  register int $128;
+  $128 = foo(&x, &x);
+  return $128;
+  return 0;
+}
+
+