Remove progs/alias and rename alias2 to alias

.gitignore

@@ -66,10 +66,6 @@ progs/alias
 progs/alias.compcert.c
 progs/alias.i
 progs/alias.parsed.c
-progs/alias2
-progs/alias2.compcert.c
-progs/alias2.i
-progs/alias2.parsed.c
 
 *.vo
 *.vos

Makefile

@@ -500,7 +500,7 @@ PROGS32_FILES= \
   printf.v stackframe_demo.v verif_stackframe_demo.v \
 	rotate.v verif_rotate.v \
   verif_objectSelf.v verif_objectSelfFancy.v verif_objectSelfFancyOverriding.v \
-  alias.v verif_alias.v alias2.v verif_alias2.v
+  alias.v verif_alias.v
 # verif_insertion_sort.v
 
 C64_ORDINARY = reverse.c revarray.c sumarray.c append.c bin_search.c \

progs/alias.c

@@ -1,27 +1,31 @@
-int foo(int *p, long *q) {
+int foo(int *p, void **q) {
   *p = 1;
   *q = 0;
   return *p;
 }
 int main() {
-  long x;
+  int x;
   return foo(&x, &x);
 }
 
 /*
-The usage in this example is essential systems programming but has undefined
-behavior according to ISO C due to the strict aliasing restriction.
+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.
 
-It returns 0 in the following invocations of clang 14.0.6 and gcc 12.2.0:
+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 int, so the modification
+through *p is consistent with these rules, but the modification through *q (of
+type void *) is not, even though int and void * have size and alignment. The
+ubiquitous compiler flag -fno-strict-aliasing lifts these restrictions.
+
+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 -O0 -w alias.c -o alias && ./alias; echo $?
-gcc   -O0 -w alias.c -o alias && ./alias; echo $?
-gcc   -O1 -w alias.c -o alias && ./alias; echo $?
-clang -fno-strict-aliasing -O1 -w alias.c -o alias && ./alias; echo $?
-clang -fno-strict-aliasing -O2 -w alias.c -o alias && ./alias; echo $?
-clang -fno-strict-aliasing -O3 -w alias.c -o alias && ./alias; echo $?
-gcc   -fno-strict-aliasing -O2 -w alias.c -o alias && ./alias; echo $?
-gcc   -fno-strict-aliasing -O3 -w alias.c -o alias && ./alias; echo $?
 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 $?
@@ -31,17 +35,12 @@ 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 a1f01c844aaa0ff41aa9095e9d5d01606a0e90c9 (3.11++):
+It also returns 0 with CompCert:
 
 ../../CompCert/ccomp alias.c -c alias.o && gcc -m32 alias.o -o alias && ./alias; echo $?
 
-It returns 1 in the following invocations of clang 14.0.6 and gcc 12.2.0:
+It returns 1 in the following invocations:
 
-clang -O1 -w alias.c -o alias && ./alias; echo $?
-clang -O2 -w alias.c -o alias && ./alias; echo $?
-clang -O3 -w alias.c -o alias && ./alias; echo $?
-gcc   -O2 -w alias.c -o alias && ./alias; echo $?
-gcc   -O3 -w alias.c -o alias && ./alias; echo $?
 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 $?
@@ -50,18 +49,10 @@ gcc   -m32 -O3 -w alias.c -o alias && ./alias; echo $?
 
 alias.v was generated using the following invocation:
 
-../../CompCert/clightgen -dall -normalize -nostdinc -P -std=c11 alias.c
+../../CompCert/clightgen -dclight -normalize -nostdinc -P -std=c11 alias.c
 
-The corresponding clight file returns 0 in all tested invocations:
+The corresponding clight file returns 0 in all invocations where the input file returned 0:
 
-clang -O0 -w alias.light.c -o alias && ./alias; echo $?
-gcc   -O0 -w alias.light.c -o alias && ./alias; echo $?
-gcc   -O1 -w alias.light.c -o alias && ./alias; echo $?
-clang -fno-strict-aliasing -O1 -w alias.light.c -o alias && ./alias; echo $?
-clang -fno-strict-aliasing -O2 -w alias.light.c -o alias && ./alias; echo $?
-clang -fno-strict-aliasing -O3 -w alias.light.c -o alias && ./alias; echo $?
-gcc   -fno-strict-aliasing -O2 -w alias.light.c -o alias && ./alias; echo $?
-gcc   -fno-strict-aliasing -O3 -w alias.light.c -o alias && ./alias; echo $?
 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 $?
@@ -70,11 +61,9 @@ 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 $?
-clang -O1 -w alias.light.c -o alias && ./alias; echo $?
-clang -O2 -w alias.light.c -o alias && ./alias; echo $?
-clang -O3 -w alias.light.c -o alias && ./alias; echo $?
-gcc   -O2 -w alias.light.c -o alias && ./alias; echo $?
-gcc   -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 $?

progs/alias.light.c

@@ -18,9 +18,9 @@ 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 *, int *);
+int foo(int *, void **);
 int main(void);
-int foo(int *$p, int *$q)
+int foo(int *$p, void **$q)
 {
   register int $128;
   *$p = 1;

progs/alias.v

@@ -85,15 +85,15 @@ Definition _t'1 : ident := 128%positive.
 Definition f_foo := {|
   fn_return := tint;
   fn_callconv := cc_default;
-  fn_params := ((_p, (tptr tint)) :: (_q, (tptr tint)) :: nil);
+  fn_params := ((_p, (tptr tint)) :: (_q, (tptr (tptr tvoid))) :: nil);
   fn_vars := nil;
   fn_temps := ((_t'1, tint) :: nil);
   fn_body :=
 (Ssequence
   (Sassign (Ederef (Etempvar _p (tptr tint)) tint)
     (Econst_int (Int.repr 1) tint))
   (Ssequence
-    (Sassign (Ederef (Etempvar _q (tptr tint)) tint)
+    (Sassign (Ederef (Etempvar _q (tptr (tptr tvoid))) (tptr tvoid))
       (Econst_int (Int.repr 0) tint))
     (Ssequence
       (Sset _t'1 (Ederef (Etempvar _p (tptr tint)) tint))
@@ -110,7 +110,8 @@ Definition f_main := {|
 (Ssequence
   (Ssequence
     (Scall (Some _t'1)
-      (Evar _foo (Tfunction (Tcons (tptr tint) (Tcons (tptr tint) Tnil)) tint
+      (Evar _foo (Tfunction
+                   (Tcons (tptr tint) (Tcons (tptr (tptr tvoid)) Tnil)) tint
                    cc_default))
       ((Eaddrof (Evar _x tint) (tptr tint)) ::
        (Eaddrof (Evar _x tint) (tptr tint)) :: nil))