From 3837729b0912aef309efe4167890641edc4adfef Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 22 Oct 2022 19:05:09 -0400 Subject: [PATCH 1/6] Add minimal example of -fno-strict-aliasing --- .gitignore | 2 + Makefile | 3 +- progs/alias.c | 54 ++++++ progs/alias.v | 419 ++++++++++++++++++++++++++++++++++++++++++++ progs/verif_alias.v | 27 +++ 5 files changed, 504 insertions(+), 1 deletion(-) create mode 100644 progs/alias.c create mode 100644 progs/alias.v create mode 100644 progs/verif_alias.v diff --git a/.gitignore b/.gitignore index ab10834be6..3edbd228b0 100644 --- a/.gitignore +++ b/.gitignore @@ -62,6 +62,8 @@ compcert/doc/html/ compcert/extraction/ compcert/test/ +progs/alias + *.vo *.vos *.vok diff --git a/Makefile b/Makefile index e9fc375d3b..677f8dfc3d 100644 --- a/Makefile +++ b/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 \ diff --git a/progs/alias.c b/progs/alias.c new file mode 100644 index 0000000000..6e93b117aa --- /dev/null +++ b/progs/alias.c @@ -0,0 +1,54 @@ +int foo(int *p, long *q) { + *p = 1; + *q = 0; + return *p; +} +int main() { + long 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. + +It returns 0 in the following invocations of clang 14.0.6 and gcc 12.2.0: + +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 $? +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 a1f01c844aaa0ff41aa9095e9d5d01606a0e90c9 (3.11++): + +../../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: + +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 $? +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 -normalize -nostdinc -P -std=c11 alias.c +*/ diff --git a/progs/alias.v b/progs/alias.v new file mode 100644 index 0000000000..37b532124f --- /dev/null +++ b/progs/alias.v @@ -0,0 +1,419 @@ +From Coq Require Import String List ZArith. +From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs. +Import Clightdefs.ClightNotations. +Local Open Scope Z_scope. +Local Open Scope string_scope. +Local Open Scope clight_scope. + +Module Info. + Definition version := "3.11". + Definition build_number := "". + Definition build_tag := "". + Definition build_branch := "". + Definition arch := "x86". + Definition model := "32sse2". + Definition abi := "standard". + Definition bitsize := 32. + Definition big_endian := false. + Definition source_file := "alias.c". + Definition normalized := true. +End Info. + +Definition ___builtin_ais_annot : ident := $"__builtin_ais_annot". +Definition ___builtin_annot : ident := $"__builtin_annot". +Definition ___builtin_annot_intval : ident := $"__builtin_annot_intval". +Definition ___builtin_bswap : ident := $"__builtin_bswap". +Definition ___builtin_bswap16 : ident := $"__builtin_bswap16". +Definition ___builtin_bswap32 : ident := $"__builtin_bswap32". +Definition ___builtin_bswap64 : ident := $"__builtin_bswap64". +Definition ___builtin_clz : ident := $"__builtin_clz". +Definition ___builtin_clzl : ident := $"__builtin_clzl". +Definition ___builtin_clzll : ident := $"__builtin_clzll". +Definition ___builtin_ctz : ident := $"__builtin_ctz". +Definition ___builtin_ctzl : ident := $"__builtin_ctzl". +Definition ___builtin_ctzll : ident := $"__builtin_ctzll". +Definition ___builtin_debug : ident := $"__builtin_debug". +Definition ___builtin_expect : ident := $"__builtin_expect". +Definition ___builtin_fabs : ident := $"__builtin_fabs". +Definition ___builtin_fabsf : ident := $"__builtin_fabsf". +Definition ___builtin_fmadd : ident := $"__builtin_fmadd". +Definition ___builtin_fmax : ident := $"__builtin_fmax". +Definition ___builtin_fmin : ident := $"__builtin_fmin". +Definition ___builtin_fmsub : ident := $"__builtin_fmsub". +Definition ___builtin_fnmadd : ident := $"__builtin_fnmadd". +Definition ___builtin_fnmsub : ident := $"__builtin_fnmsub". +Definition ___builtin_fsqrt : ident := $"__builtin_fsqrt". +Definition ___builtin_membar : ident := $"__builtin_membar". +Definition ___builtin_memcpy_aligned : ident := $"__builtin_memcpy_aligned". +Definition ___builtin_read16_reversed : ident := $"__builtin_read16_reversed". +Definition ___builtin_read32_reversed : ident := $"__builtin_read32_reversed". +Definition ___builtin_sel : ident := $"__builtin_sel". +Definition ___builtin_sqrt : ident := $"__builtin_sqrt". +Definition ___builtin_unreachable : ident := $"__builtin_unreachable". +Definition ___builtin_va_arg : ident := $"__builtin_va_arg". +Definition ___builtin_va_copy : ident := $"__builtin_va_copy". +Definition ___builtin_va_end : ident := $"__builtin_va_end". +Definition ___builtin_va_start : ident := $"__builtin_va_start". +Definition ___builtin_write16_reversed : ident := $"__builtin_write16_reversed". +Definition ___builtin_write32_reversed : ident := $"__builtin_write32_reversed". +Definition ___compcert_i64_dtos : ident := $"__compcert_i64_dtos". +Definition ___compcert_i64_dtou : ident := $"__compcert_i64_dtou". +Definition ___compcert_i64_sar : ident := $"__compcert_i64_sar". +Definition ___compcert_i64_sdiv : ident := $"__compcert_i64_sdiv". +Definition ___compcert_i64_shl : ident := $"__compcert_i64_shl". +Definition ___compcert_i64_shr : ident := $"__compcert_i64_shr". +Definition ___compcert_i64_smod : ident := $"__compcert_i64_smod". +Definition ___compcert_i64_smulh : ident := $"__compcert_i64_smulh". +Definition ___compcert_i64_stod : ident := $"__compcert_i64_stod". +Definition ___compcert_i64_stof : ident := $"__compcert_i64_stof". +Definition ___compcert_i64_udiv : ident := $"__compcert_i64_udiv". +Definition ___compcert_i64_umod : ident := $"__compcert_i64_umod". +Definition ___compcert_i64_umulh : ident := $"__compcert_i64_umulh". +Definition ___compcert_i64_utod : ident := $"__compcert_i64_utod". +Definition ___compcert_i64_utof : ident := $"__compcert_i64_utof". +Definition ___compcert_va_composite : ident := $"__compcert_va_composite". +Definition ___compcert_va_float64 : ident := $"__compcert_va_float64". +Definition ___compcert_va_int32 : ident := $"__compcert_va_int32". +Definition ___compcert_va_int64 : ident := $"__compcert_va_int64". +Definition _foo : ident := $"foo". +Definition _main : ident := $"main". +Definition _p : ident := $"p". +Definition _q : ident := $"q". +Definition _x : ident := $"x". +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_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) + (Econst_int (Int.repr 0) tint)) + (Ssequence + (Sset _t'1 (Ederef (Etempvar _p (tptr tint)) tint)) + (Sreturn (Some (Etempvar _t'1 tint)))))) +|}. + +Definition f_main := {| + fn_return := tint; + fn_callconv := cc_default; + fn_params := nil; + fn_vars := ((_x, tint) :: nil); + fn_temps := ((_t'1, tint) :: nil); + fn_body := +(Ssequence + (Ssequence + (Scall (Some _t'1) + (Evar _foo (Tfunction (Tcons (tptr tint) (Tcons (tptr tint) Tnil)) tint + cc_default)) + ((Eaddrof (Evar _x tint) (tptr tint)) :: + (Eaddrof (Evar _x tint) (tptr tint)) :: nil)) + (Sreturn (Some (Etempvar _t'1 tint)))) + (Sreturn (Some (Econst_int (Int.repr 0) tint)))) +|}. + +Definition composites : list composite_definition := +nil. + +Definition global_definitions : list (ident * globdef fundef type) := +((___compcert_va_int32, + Gfun(External (EF_runtime "__compcert_va_int32" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons (tptr tvoid) Tnil) tuint cc_default)) :: + (___compcert_va_int64, + Gfun(External (EF_runtime "__compcert_va_int64" + (mksignature (AST.Tint :: nil) AST.Tlong cc_default)) + (Tcons (tptr tvoid) Tnil) tulong cc_default)) :: + (___compcert_va_float64, + Gfun(External (EF_runtime "__compcert_va_float64" + (mksignature (AST.Tint :: nil) AST.Tfloat cc_default)) + (Tcons (tptr tvoid) Tnil) tdouble cc_default)) :: + (___compcert_va_composite, + Gfun(External (EF_runtime "__compcert_va_composite" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint + cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil)) + (tptr tvoid) cc_default)) :: + (___compcert_i64_dtos, + Gfun(External (EF_runtime "__compcert_i64_dtos" + (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default)) + (Tcons tdouble Tnil) tlong cc_default)) :: + (___compcert_i64_dtou, + Gfun(External (EF_runtime "__compcert_i64_dtou" + (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default)) + (Tcons tdouble Tnil) tulong cc_default)) :: + (___compcert_i64_stod, + Gfun(External (EF_runtime "__compcert_i64_stod" + (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default)) + (Tcons tlong Tnil) tdouble cc_default)) :: + (___compcert_i64_utod, + Gfun(External (EF_runtime "__compcert_i64_utod" + (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default)) + (Tcons tulong Tnil) tdouble cc_default)) :: + (___compcert_i64_stof, + Gfun(External (EF_runtime "__compcert_i64_stof" + (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default)) + (Tcons tlong Tnil) tfloat cc_default)) :: + (___compcert_i64_utof, + Gfun(External (EF_runtime "__compcert_i64_utof" + (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default)) + (Tcons tulong Tnil) tfloat cc_default)) :: + (___compcert_i64_sdiv, + Gfun(External (EF_runtime "__compcert_i64_sdiv" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong + cc_default)) :: + (___compcert_i64_udiv, + Gfun(External (EF_runtime "__compcert_i64_udiv" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong + cc_default)) :: + (___compcert_i64_smod, + Gfun(External (EF_runtime "__compcert_i64_smod" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong + cc_default)) :: + (___compcert_i64_umod, + Gfun(External (EF_runtime "__compcert_i64_umod" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong + cc_default)) :: + (___compcert_i64_shl, + Gfun(External (EF_runtime "__compcert_i64_shl" + (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong + cc_default)) :: + (___compcert_i64_shr, + Gfun(External (EF_runtime "__compcert_i64_shr" + (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong + cc_default)) (Tcons tulong (Tcons tint Tnil)) tulong + cc_default)) :: + (___compcert_i64_sar, + Gfun(External (EF_runtime "__compcert_i64_sar" + (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong + cc_default)) :: + (___compcert_i64_smulh, + Gfun(External (EF_runtime "__compcert_i64_smulh" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong + cc_default)) :: + (___compcert_i64_umulh, + Gfun(External (EF_runtime "__compcert_i64_umulh" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong + cc_default)) :: + (___builtin_ais_annot, + Gfun(External (EF_builtin "__builtin_ais_annot" + (mksignature (AST.Tint :: nil) AST.Tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) + (Tcons (tptr tschar) Tnil) tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: + (___builtin_bswap64, + Gfun(External (EF_builtin "__builtin_bswap64" + (mksignature (AST.Tlong :: nil) AST.Tlong cc_default)) + (Tcons tulong Tnil) tulong cc_default)) :: + (___builtin_bswap, + Gfun(External (EF_builtin "__builtin_bswap" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tuint cc_default)) :: + (___builtin_bswap32, + Gfun(External (EF_builtin "__builtin_bswap32" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tuint cc_default)) :: + (___builtin_bswap16, + Gfun(External (EF_builtin "__builtin_bswap16" + (mksignature (AST.Tint :: nil) AST.Tint16unsigned + cc_default)) (Tcons tushort Tnil) tushort cc_default)) :: + (___builtin_clz, + Gfun(External (EF_builtin "__builtin_clz" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tint cc_default)) :: + (___builtin_clzl, + Gfun(External (EF_builtin "__builtin_clzl" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tint cc_default)) :: + (___builtin_clzll, + Gfun(External (EF_builtin "__builtin_clzll" + (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) + (Tcons tulong Tnil) tint cc_default)) :: + (___builtin_ctz, + Gfun(External (EF_builtin "__builtin_ctz" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tint cc_default)) :: + (___builtin_ctzl, + Gfun(External (EF_builtin "__builtin_ctzl" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tint cc_default)) :: + (___builtin_ctzll, + Gfun(External (EF_builtin "__builtin_ctzll" + (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) + (Tcons tulong Tnil) tint cc_default)) :: + (___builtin_fabs, + Gfun(External (EF_builtin "__builtin_fabs" + (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) + (Tcons tdouble Tnil) tdouble cc_default)) :: + (___builtin_fabsf, + Gfun(External (EF_builtin "__builtin_fabsf" + (mksignature (AST.Tsingle :: nil) AST.Tsingle cc_default)) + (Tcons tfloat Tnil) tfloat cc_default)) :: + (___builtin_fsqrt, + Gfun(External (EF_builtin "__builtin_fsqrt" + (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) + (Tcons tdouble Tnil) tdouble cc_default)) :: + (___builtin_sqrt, + Gfun(External (EF_builtin "__builtin_sqrt" + (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) + (Tcons tdouble Tnil) tdouble cc_default)) :: + (___builtin_memcpy_aligned, + Gfun(External (EF_builtin "__builtin_memcpy_aligned" + (mksignature + (AST.Tint :: AST.Tint :: AST.Tint :: AST.Tint :: nil) + AST.Tvoid cc_default)) + (Tcons (tptr tvoid) + (Tcons (tptr tvoid) (Tcons tuint (Tcons tuint Tnil)))) tvoid + cc_default)) :: + (___builtin_sel, + Gfun(External (EF_builtin "__builtin_sel" + (mksignature (AST.Tint :: nil) AST.Tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) + (Tcons tbool Tnil) tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: + (___builtin_annot, + Gfun(External (EF_builtin "__builtin_annot" + (mksignature (AST.Tint :: nil) AST.Tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) + (Tcons (tptr tschar) Tnil) tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: + (___builtin_annot_intval, + Gfun(External (EF_builtin "__builtin_annot_intval" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint + cc_default)) (Tcons (tptr tschar) (Tcons tint Tnil)) + tint cc_default)) :: + (___builtin_membar, + Gfun(External (EF_builtin "__builtin_membar" + (mksignature nil AST.Tvoid cc_default)) Tnil tvoid + cc_default)) :: + (___builtin_va_start, + Gfun(External (EF_builtin "__builtin_va_start" + (mksignature (AST.Tint :: nil) AST.Tvoid cc_default)) + (Tcons (tptr tvoid) Tnil) tvoid cc_default)) :: + (___builtin_va_arg, + Gfun(External (EF_builtin "__builtin_va_arg" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid + cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil)) + tvoid cc_default)) :: + (___builtin_va_copy, + Gfun(External (EF_builtin "__builtin_va_copy" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid + cc_default)) + (Tcons (tptr tvoid) (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) :: + (___builtin_va_end, + Gfun(External (EF_builtin "__builtin_va_end" + (mksignature (AST.Tint :: nil) AST.Tvoid cc_default)) + (Tcons (tptr tvoid) Tnil) tvoid cc_default)) :: + (___builtin_unreachable, + Gfun(External (EF_builtin "__builtin_unreachable" + (mksignature nil AST.Tvoid cc_default)) Tnil tvoid + cc_default)) :: + (___builtin_expect, + Gfun(External (EF_builtin "__builtin_expect" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint + cc_default)) (Tcons tint (Tcons tint Tnil)) tint + cc_default)) :: + (___builtin_fmax, + Gfun(External (EF_builtin "__builtin_fmax" + (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat + cc_default)) (Tcons tdouble (Tcons tdouble Tnil)) + tdouble cc_default)) :: + (___builtin_fmin, + Gfun(External (EF_builtin "__builtin_fmin" + (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat + cc_default)) (Tcons tdouble (Tcons tdouble Tnil)) + tdouble cc_default)) :: + (___builtin_fmadd, + Gfun(External (EF_builtin "__builtin_fmadd" + (mksignature + (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) + AST.Tfloat cc_default)) + (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble + cc_default)) :: + (___builtin_fmsub, + Gfun(External (EF_builtin "__builtin_fmsub" + (mksignature + (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) + AST.Tfloat cc_default)) + (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble + cc_default)) :: + (___builtin_fnmadd, + Gfun(External (EF_builtin "__builtin_fnmadd" + (mksignature + (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) + AST.Tfloat cc_default)) + (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble + cc_default)) :: + (___builtin_fnmsub, + Gfun(External (EF_builtin "__builtin_fnmsub" + (mksignature + (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) + AST.Tfloat cc_default)) + (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble + cc_default)) :: + (___builtin_read16_reversed, + Gfun(External (EF_builtin "__builtin_read16_reversed" + (mksignature (AST.Tint :: nil) AST.Tint16unsigned + cc_default)) (Tcons (tptr tushort) Tnil) tushort + cc_default)) :: + (___builtin_read32_reversed, + Gfun(External (EF_builtin "__builtin_read32_reversed" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons (tptr tuint) Tnil) tuint cc_default)) :: + (___builtin_write16_reversed, + Gfun(External (EF_builtin "__builtin_write16_reversed" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid + cc_default)) (Tcons (tptr tushort) (Tcons tushort Tnil)) + tvoid cc_default)) :: + (___builtin_write32_reversed, + Gfun(External (EF_builtin "__builtin_write32_reversed" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid + cc_default)) (Tcons (tptr tuint) (Tcons tuint Tnil)) + tvoid cc_default)) :: + (___builtin_debug, + Gfun(External (EF_external "__builtin_debug" + (mksignature (AST.Tint :: nil) AST.Tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) + (Tcons tint Tnil) tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: + (_foo, Gfun(Internal f_foo)) :: (_main, Gfun(Internal f_main)) :: nil). + +Definition public_idents : list ident := +(_main :: _foo :: ___builtin_debug :: ___builtin_write32_reversed :: + ___builtin_write16_reversed :: ___builtin_read32_reversed :: + ___builtin_read16_reversed :: ___builtin_fnmsub :: ___builtin_fnmadd :: + ___builtin_fmsub :: ___builtin_fmadd :: ___builtin_fmin :: + ___builtin_fmax :: ___builtin_expect :: ___builtin_unreachable :: + ___builtin_va_end :: ___builtin_va_copy :: ___builtin_va_arg :: + ___builtin_va_start :: ___builtin_membar :: ___builtin_annot_intval :: + ___builtin_annot :: ___builtin_sel :: ___builtin_memcpy_aligned :: + ___builtin_sqrt :: ___builtin_fsqrt :: ___builtin_fabsf :: + ___builtin_fabs :: ___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz :: + ___builtin_clzll :: ___builtin_clzl :: ___builtin_clz :: + ___builtin_bswap16 :: ___builtin_bswap32 :: ___builtin_bswap :: + ___builtin_bswap64 :: ___builtin_ais_annot :: ___compcert_i64_umulh :: + ___compcert_i64_smulh :: ___compcert_i64_sar :: ___compcert_i64_shr :: + ___compcert_i64_shl :: ___compcert_i64_umod :: ___compcert_i64_smod :: + ___compcert_i64_udiv :: ___compcert_i64_sdiv :: ___compcert_i64_utof :: + ___compcert_i64_stof :: ___compcert_i64_utod :: ___compcert_i64_stod :: + ___compcert_i64_dtou :: ___compcert_i64_dtos :: ___compcert_va_composite :: + ___compcert_va_float64 :: ___compcert_va_int64 :: ___compcert_va_int32 :: + nil). + +Definition prog : Clight.program := + mkprogram composites global_definitions public_idents _main Logic.I. + + diff --git a/progs/verif_alias.v b/progs/verif_alias.v new file mode 100644 index 0000000000..2515829bcf --- /dev/null +++ b/progs/verif_alias.v @@ -0,0 +1,27 @@ +Require Import VST.floyd.proofauto. +Require Import VST.progs.alias. + +#[export] Instance CompSpecs : compspecs. +Proof. make_compspecs prog. Defined. +Definition Vprog : varspecs. mk_varspecs prog. Defined. + +Definition foo_spec := DECLARE _foo WITH p : val + PRE [ tptr tint, tptr tint ] PROP() PARAMS(p; p) SEP(data_at_ Tsh tint p) + POST [ tint ] PROP() RETURN(Vint Int.zero) SEP(data_at_ Tsh tint p). + +Definition main_spec := DECLARE _main WITH gv : globals + PRE [] main_pre prog tt gv + POST [ tint ] PROP() RETURN (Vint Int.zero) SEP(has_ext tt). + +Definition Gprog : funspecs := ltac:(with_library prog [foo_spec; main_spec]). + +Lemma body_main : semax_body Vprog Gprog f_main main_spec. +Proof. start_function. forward_call. forward. entailer!. Qed. + +Lemma body_foo : semax_body Vprog Gprog f_foo foo_spec. +Proof. start_function. repeat forward. entailer!. Qed. + +Definition Espec := add_funspecs NullExtension.Espec (ext_link_prog prog) Gprog. +#[export] Existing Instance Espec. +Lemma prog_correct: semax_prog prog tt Vprog Gprog. +Proof. prove_semax_prog. semax_func_cons body_foo. semax_func_cons body_main. Qed. From 7b1b3d1b13e76775a973d2c3db83e0ba59226e03 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 23 Oct 2022 02:14:19 -0400 Subject: [PATCH 2/6] Add example of -fno-strict-aliasing in Clight --- .gitignore | 7 + Makefile | 2 +- progs/alias.c | 31 +++- progs/alias.light.c | 41 +++++ progs/alias2.c | 60 +++++++ progs/alias2.light.c | 41 +++++ progs/alias2.v | 420 +++++++++++++++++++++++++++++++++++++++++++ progs/verif_alias2.v | 64 +++++++ 8 files changed, 664 insertions(+), 2 deletions(-) create mode 100644 progs/alias.light.c create mode 100644 progs/alias2.c create mode 100644 progs/alias2.light.c create mode 100644 progs/alias2.v create mode 100644 progs/verif_alias2.v diff --git a/.gitignore b/.gitignore index 3edbd228b0..3a07a5cf39 100644 --- a/.gitignore +++ b/.gitignore @@ -63,6 +63,13 @@ compcert/extraction/ compcert/test/ 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 diff --git a/Makefile b/Makefile index 677f8dfc3d..35cd0a60b1 100644 --- a/Makefile +++ b/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 + alias.v verif_alias.v alias2.v verif_alias2.v # verif_insertion_sort.v C64_ORDINARY = reverse.c revarray.c sumarray.c append.c bin_search.c \ diff --git a/progs/alias.c b/progs/alias.c index 6e93b117aa..148e4d7839 100644 --- a/progs/alias.c +++ b/progs/alias.c @@ -50,5 +50,34 @@ gcc -m32 -O3 -w alias.c -o alias && ./alias; echo $? alias.v was generated using the following invocation: -../../CompCert/clightgen -normalize -nostdinc -P -std=c11 alias.c +../../CompCert/clightgen -dall -normalize -nostdinc -P -std=c11 alias.c + +The corresponding clight file returns 0 in all tested invocations: + +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 $? +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 $? +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 $? +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 $? */ diff --git a/progs/alias.light.c b/progs/alias.light.c new file mode 100644 index 0000000000..78e575c5ac --- /dev/null +++ b/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 *, int *); +int main(void); +int foo(int *$p, int *$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; +} + + diff --git a/progs/alias2.c b/progs/alias2.c new file mode 100644 index 0000000000..932f114317 --- /dev/null +++ b/progs/alias2.c @@ -0,0 +1,60 @@ +int foo(int *p, void **q) { + *p = 1; + *q = 0; + return *p; +} +int main() { + 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. + +It returns 0 in the following invocations of clang 14.0.6 and gcc 12.2.0: + +clang -m32 -O0 -w alias2.c -o alias2 && ./alias2; echo $? +gcc -m32 -O0 -w alias2.c -o alias2 && ./alias2; echo $? +gcc -m32 -O1 -w alias2.c -o alias2 && ./alias2; echo $? +clang -m32 -fno-strict-aliasing -O1 -w alias2.c -o alias2 && ./alias2; echo $? +clang -m32 -fno-strict-aliasing -O2 -w alias2.c -o alias2 && ./alias2; echo $? +clang -m32 -fno-strict-aliasing -O3 -w alias2.c -o alias2 && ./alias2; echo $? +gcc -m32 -fno-strict-aliasing -O2 -w alias2.c -o alias2 && ./alias2; echo $? +gcc -m32 -fno-strict-aliasing -O3 -w alias2.c -o alias2 && ./alias2; echo $? + +It also returns 0 with CompCert a1f01c844aaa0ff41aa9095e9d5d01606a0e90c9 (3.11++): + +../../CompCert/ccomp alias2.c -c alias2.o && gcc -m32 alias2.o -o alias2 && ./alias2; echo $? + +It returns 1 in the following invocations of clang 14.0.6 and gcc 12.2.0: + +clang -m32 -O1 -w alias2.c -o alias2 && ./alias2; echo $? +clang -m32 -O2 -w alias2.c -o alias2 && ./alias2; echo $? +clang -m32 -O3 -w alias2.c -o alias2 && ./alias2; echo $? +gcc -m32 -O2 -w alias2.c -o alias2 && ./alias2; echo $? +gcc -m32 -O3 -w alias2.c -o alias2 && ./alias2; echo $? + +alias2.v was generated using the following invocation: + +../../CompCert/clightgen -dall -normalize -nostdinc -P -std=c11 alias2.c + +The corresponding clight file returns 0 in all invocations where the input file returned 0: + +clang -m32 -O0 -w alias2.light.c -o alias2 && ./alias2; echo $? +gcc -m32 -O0 -w alias2.light.c -o alias2 && ./alias2; echo $? +gcc -m32 -O1 -w alias2.light.c -o alias2 && ./alias2; echo $? +clang -m32 -fno-strict-aliasing -O1 -w alias2.light.c -o alias2 && ./alias2; echo $? +clang -m32 -fno-strict-aliasing -O2 -w alias2.light.c -o alias2 && ./alias2; echo $? +clang -m32 -fno-strict-aliasing -O3 -w alias2.light.c -o alias2 && ./alias2; echo $? +gcc -m32 -fno-strict-aliasing -O2 -w alias2.light.c -o alias2 && ./alias2; echo $? +gcc -m32 -fno-strict-aliasing -O3 -w alias2.light.c -o alias2 && ./alias2; echo $? + +... and returns 1 in all invocations where the input file returned 1: + +clang -m32 -O1 -w alias2.light.c -o alias2 && ./alias2; echo $? +clang -m32 -O2 -w alias2.light.c -o alias2 && ./alias2; echo $? +clang -m32 -O3 -w alias2.light.c -o alias2 && ./alias2; echo $? +gcc -m32 -O2 -w alias2.light.c -o alias2 && ./alias2; echo $? +gcc -m32 -O3 -w alias2.light.c -o alias2 && ./alias2; echo $? +*/ diff --git a/progs/alias2.light.c b/progs/alias2.light.c new file mode 100644 index 0000000000..2b87ed581f --- /dev/null +++ b/progs/alias2.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; +} + + diff --git a/progs/alias2.v b/progs/alias2.v new file mode 100644 index 0000000000..c32f82290b --- /dev/null +++ b/progs/alias2.v @@ -0,0 +1,420 @@ +From Coq Require Import String List ZArith. +From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs. +Import Clightdefs.ClightNotations. +Local Open Scope Z_scope. +Local Open Scope string_scope. +Local Open Scope clight_scope. + +Module Info. + Definition version := "3.11". + Definition build_number := "". + Definition build_tag := "". + Definition build_branch := "". + Definition arch := "x86". + Definition model := "32sse2". + Definition abi := "standard". + Definition bitsize := 32. + Definition big_endian := false. + Definition source_file := "alias2.c". + Definition normalized := true. +End Info. + +Definition ___builtin_ais_annot : ident := $"__builtin_ais_annot". +Definition ___builtin_annot : ident := $"__builtin_annot". +Definition ___builtin_annot_intval : ident := $"__builtin_annot_intval". +Definition ___builtin_bswap : ident := $"__builtin_bswap". +Definition ___builtin_bswap16 : ident := $"__builtin_bswap16". +Definition ___builtin_bswap32 : ident := $"__builtin_bswap32". +Definition ___builtin_bswap64 : ident := $"__builtin_bswap64". +Definition ___builtin_clz : ident := $"__builtin_clz". +Definition ___builtin_clzl : ident := $"__builtin_clzl". +Definition ___builtin_clzll : ident := $"__builtin_clzll". +Definition ___builtin_ctz : ident := $"__builtin_ctz". +Definition ___builtin_ctzl : ident := $"__builtin_ctzl". +Definition ___builtin_ctzll : ident := $"__builtin_ctzll". +Definition ___builtin_debug : ident := $"__builtin_debug". +Definition ___builtin_expect : ident := $"__builtin_expect". +Definition ___builtin_fabs : ident := $"__builtin_fabs". +Definition ___builtin_fabsf : ident := $"__builtin_fabsf". +Definition ___builtin_fmadd : ident := $"__builtin_fmadd". +Definition ___builtin_fmax : ident := $"__builtin_fmax". +Definition ___builtin_fmin : ident := $"__builtin_fmin". +Definition ___builtin_fmsub : ident := $"__builtin_fmsub". +Definition ___builtin_fnmadd : ident := $"__builtin_fnmadd". +Definition ___builtin_fnmsub : ident := $"__builtin_fnmsub". +Definition ___builtin_fsqrt : ident := $"__builtin_fsqrt". +Definition ___builtin_membar : ident := $"__builtin_membar". +Definition ___builtin_memcpy_aligned : ident := $"__builtin_memcpy_aligned". +Definition ___builtin_read16_reversed : ident := $"__builtin_read16_reversed". +Definition ___builtin_read32_reversed : ident := $"__builtin_read32_reversed". +Definition ___builtin_sel : ident := $"__builtin_sel". +Definition ___builtin_sqrt : ident := $"__builtin_sqrt". +Definition ___builtin_unreachable : ident := $"__builtin_unreachable". +Definition ___builtin_va_arg : ident := $"__builtin_va_arg". +Definition ___builtin_va_copy : ident := $"__builtin_va_copy". +Definition ___builtin_va_end : ident := $"__builtin_va_end". +Definition ___builtin_va_start : ident := $"__builtin_va_start". +Definition ___builtin_write16_reversed : ident := $"__builtin_write16_reversed". +Definition ___builtin_write32_reversed : ident := $"__builtin_write32_reversed". +Definition ___compcert_i64_dtos : ident := $"__compcert_i64_dtos". +Definition ___compcert_i64_dtou : ident := $"__compcert_i64_dtou". +Definition ___compcert_i64_sar : ident := $"__compcert_i64_sar". +Definition ___compcert_i64_sdiv : ident := $"__compcert_i64_sdiv". +Definition ___compcert_i64_shl : ident := $"__compcert_i64_shl". +Definition ___compcert_i64_shr : ident := $"__compcert_i64_shr". +Definition ___compcert_i64_smod : ident := $"__compcert_i64_smod". +Definition ___compcert_i64_smulh : ident := $"__compcert_i64_smulh". +Definition ___compcert_i64_stod : ident := $"__compcert_i64_stod". +Definition ___compcert_i64_stof : ident := $"__compcert_i64_stof". +Definition ___compcert_i64_udiv : ident := $"__compcert_i64_udiv". +Definition ___compcert_i64_umod : ident := $"__compcert_i64_umod". +Definition ___compcert_i64_umulh : ident := $"__compcert_i64_umulh". +Definition ___compcert_i64_utod : ident := $"__compcert_i64_utod". +Definition ___compcert_i64_utof : ident := $"__compcert_i64_utof". +Definition ___compcert_va_composite : ident := $"__compcert_va_composite". +Definition ___compcert_va_float64 : ident := $"__compcert_va_float64". +Definition ___compcert_va_int32 : ident := $"__compcert_va_int32". +Definition ___compcert_va_int64 : ident := $"__compcert_va_int64". +Definition _foo : ident := $"foo". +Definition _main : ident := $"main". +Definition _p : ident := $"p". +Definition _q : ident := $"q". +Definition _x : ident := $"x". +Definition _t'1 : ident := 128%positive. + +Definition f_foo := {| + fn_return := tint; + fn_callconv := cc_default; + 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 (tptr tvoid))) (tptr tvoid)) + (Econst_int (Int.repr 0) tint)) + (Ssequence + (Sset _t'1 (Ederef (Etempvar _p (tptr tint)) tint)) + (Sreturn (Some (Etempvar _t'1 tint)))))) +|}. + +Definition f_main := {| + fn_return := tint; + fn_callconv := cc_default; + fn_params := nil; + fn_vars := ((_x, tint) :: nil); + fn_temps := ((_t'1, tint) :: nil); + fn_body := +(Ssequence + (Ssequence + (Scall (Some _t'1) + (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)) + (Sreturn (Some (Etempvar _t'1 tint)))) + (Sreturn (Some (Econst_int (Int.repr 0) tint)))) +|}. + +Definition composites : list composite_definition := +nil. + +Definition global_definitions : list (ident * globdef fundef type) := +((___compcert_va_int32, + Gfun(External (EF_runtime "__compcert_va_int32" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons (tptr tvoid) Tnil) tuint cc_default)) :: + (___compcert_va_int64, + Gfun(External (EF_runtime "__compcert_va_int64" + (mksignature (AST.Tint :: nil) AST.Tlong cc_default)) + (Tcons (tptr tvoid) Tnil) tulong cc_default)) :: + (___compcert_va_float64, + Gfun(External (EF_runtime "__compcert_va_float64" + (mksignature (AST.Tint :: nil) AST.Tfloat cc_default)) + (Tcons (tptr tvoid) Tnil) tdouble cc_default)) :: + (___compcert_va_composite, + Gfun(External (EF_runtime "__compcert_va_composite" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint + cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil)) + (tptr tvoid) cc_default)) :: + (___compcert_i64_dtos, + Gfun(External (EF_runtime "__compcert_i64_dtos" + (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default)) + (Tcons tdouble Tnil) tlong cc_default)) :: + (___compcert_i64_dtou, + Gfun(External (EF_runtime "__compcert_i64_dtou" + (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default)) + (Tcons tdouble Tnil) tulong cc_default)) :: + (___compcert_i64_stod, + Gfun(External (EF_runtime "__compcert_i64_stod" + (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default)) + (Tcons tlong Tnil) tdouble cc_default)) :: + (___compcert_i64_utod, + Gfun(External (EF_runtime "__compcert_i64_utod" + (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default)) + (Tcons tulong Tnil) tdouble cc_default)) :: + (___compcert_i64_stof, + Gfun(External (EF_runtime "__compcert_i64_stof" + (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default)) + (Tcons tlong Tnil) tfloat cc_default)) :: + (___compcert_i64_utof, + Gfun(External (EF_runtime "__compcert_i64_utof" + (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default)) + (Tcons tulong Tnil) tfloat cc_default)) :: + (___compcert_i64_sdiv, + Gfun(External (EF_runtime "__compcert_i64_sdiv" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong + cc_default)) :: + (___compcert_i64_udiv, + Gfun(External (EF_runtime "__compcert_i64_udiv" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong + cc_default)) :: + (___compcert_i64_smod, + Gfun(External (EF_runtime "__compcert_i64_smod" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong + cc_default)) :: + (___compcert_i64_umod, + Gfun(External (EF_runtime "__compcert_i64_umod" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong + cc_default)) :: + (___compcert_i64_shl, + Gfun(External (EF_runtime "__compcert_i64_shl" + (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong + cc_default)) :: + (___compcert_i64_shr, + Gfun(External (EF_runtime "__compcert_i64_shr" + (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong + cc_default)) (Tcons tulong (Tcons tint Tnil)) tulong + cc_default)) :: + (___compcert_i64_sar, + Gfun(External (EF_runtime "__compcert_i64_sar" + (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong + cc_default)) :: + (___compcert_i64_smulh, + Gfun(External (EF_runtime "__compcert_i64_smulh" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong + cc_default)) :: + (___compcert_i64_umulh, + Gfun(External (EF_runtime "__compcert_i64_umulh" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong + cc_default)) :: + (___builtin_ais_annot, + Gfun(External (EF_builtin "__builtin_ais_annot" + (mksignature (AST.Tint :: nil) AST.Tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) + (Tcons (tptr tschar) Tnil) tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: + (___builtin_bswap64, + Gfun(External (EF_builtin "__builtin_bswap64" + (mksignature (AST.Tlong :: nil) AST.Tlong cc_default)) + (Tcons tulong Tnil) tulong cc_default)) :: + (___builtin_bswap, + Gfun(External (EF_builtin "__builtin_bswap" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tuint cc_default)) :: + (___builtin_bswap32, + Gfun(External (EF_builtin "__builtin_bswap32" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tuint cc_default)) :: + (___builtin_bswap16, + Gfun(External (EF_builtin "__builtin_bswap16" + (mksignature (AST.Tint :: nil) AST.Tint16unsigned + cc_default)) (Tcons tushort Tnil) tushort cc_default)) :: + (___builtin_clz, + Gfun(External (EF_builtin "__builtin_clz" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tint cc_default)) :: + (___builtin_clzl, + Gfun(External (EF_builtin "__builtin_clzl" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tint cc_default)) :: + (___builtin_clzll, + Gfun(External (EF_builtin "__builtin_clzll" + (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) + (Tcons tulong Tnil) tint cc_default)) :: + (___builtin_ctz, + Gfun(External (EF_builtin "__builtin_ctz" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tint cc_default)) :: + (___builtin_ctzl, + Gfun(External (EF_builtin "__builtin_ctzl" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tint cc_default)) :: + (___builtin_ctzll, + Gfun(External (EF_builtin "__builtin_ctzll" + (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) + (Tcons tulong Tnil) tint cc_default)) :: + (___builtin_fabs, + Gfun(External (EF_builtin "__builtin_fabs" + (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) + (Tcons tdouble Tnil) tdouble cc_default)) :: + (___builtin_fabsf, + Gfun(External (EF_builtin "__builtin_fabsf" + (mksignature (AST.Tsingle :: nil) AST.Tsingle cc_default)) + (Tcons tfloat Tnil) tfloat cc_default)) :: + (___builtin_fsqrt, + Gfun(External (EF_builtin "__builtin_fsqrt" + (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) + (Tcons tdouble Tnil) tdouble cc_default)) :: + (___builtin_sqrt, + Gfun(External (EF_builtin "__builtin_sqrt" + (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) + (Tcons tdouble Tnil) tdouble cc_default)) :: + (___builtin_memcpy_aligned, + Gfun(External (EF_builtin "__builtin_memcpy_aligned" + (mksignature + (AST.Tint :: AST.Tint :: AST.Tint :: AST.Tint :: nil) + AST.Tvoid cc_default)) + (Tcons (tptr tvoid) + (Tcons (tptr tvoid) (Tcons tuint (Tcons tuint Tnil)))) tvoid + cc_default)) :: + (___builtin_sel, + Gfun(External (EF_builtin "__builtin_sel" + (mksignature (AST.Tint :: nil) AST.Tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) + (Tcons tbool Tnil) tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: + (___builtin_annot, + Gfun(External (EF_builtin "__builtin_annot" + (mksignature (AST.Tint :: nil) AST.Tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) + (Tcons (tptr tschar) Tnil) tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: + (___builtin_annot_intval, + Gfun(External (EF_builtin "__builtin_annot_intval" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint + cc_default)) (Tcons (tptr tschar) (Tcons tint Tnil)) + tint cc_default)) :: + (___builtin_membar, + Gfun(External (EF_builtin "__builtin_membar" + (mksignature nil AST.Tvoid cc_default)) Tnil tvoid + cc_default)) :: + (___builtin_va_start, + Gfun(External (EF_builtin "__builtin_va_start" + (mksignature (AST.Tint :: nil) AST.Tvoid cc_default)) + (Tcons (tptr tvoid) Tnil) tvoid cc_default)) :: + (___builtin_va_arg, + Gfun(External (EF_builtin "__builtin_va_arg" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid + cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil)) + tvoid cc_default)) :: + (___builtin_va_copy, + Gfun(External (EF_builtin "__builtin_va_copy" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid + cc_default)) + (Tcons (tptr tvoid) (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) :: + (___builtin_va_end, + Gfun(External (EF_builtin "__builtin_va_end" + (mksignature (AST.Tint :: nil) AST.Tvoid cc_default)) + (Tcons (tptr tvoid) Tnil) tvoid cc_default)) :: + (___builtin_unreachable, + Gfun(External (EF_builtin "__builtin_unreachable" + (mksignature nil AST.Tvoid cc_default)) Tnil tvoid + cc_default)) :: + (___builtin_expect, + Gfun(External (EF_builtin "__builtin_expect" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint + cc_default)) (Tcons tint (Tcons tint Tnil)) tint + cc_default)) :: + (___builtin_fmax, + Gfun(External (EF_builtin "__builtin_fmax" + (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat + cc_default)) (Tcons tdouble (Tcons tdouble Tnil)) + tdouble cc_default)) :: + (___builtin_fmin, + Gfun(External (EF_builtin "__builtin_fmin" + (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat + cc_default)) (Tcons tdouble (Tcons tdouble Tnil)) + tdouble cc_default)) :: + (___builtin_fmadd, + Gfun(External (EF_builtin "__builtin_fmadd" + (mksignature + (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) + AST.Tfloat cc_default)) + (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble + cc_default)) :: + (___builtin_fmsub, + Gfun(External (EF_builtin "__builtin_fmsub" + (mksignature + (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) + AST.Tfloat cc_default)) + (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble + cc_default)) :: + (___builtin_fnmadd, + Gfun(External (EF_builtin "__builtin_fnmadd" + (mksignature + (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) + AST.Tfloat cc_default)) + (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble + cc_default)) :: + (___builtin_fnmsub, + Gfun(External (EF_builtin "__builtin_fnmsub" + (mksignature + (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) + AST.Tfloat cc_default)) + (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble + cc_default)) :: + (___builtin_read16_reversed, + Gfun(External (EF_builtin "__builtin_read16_reversed" + (mksignature (AST.Tint :: nil) AST.Tint16unsigned + cc_default)) (Tcons (tptr tushort) Tnil) tushort + cc_default)) :: + (___builtin_read32_reversed, + Gfun(External (EF_builtin "__builtin_read32_reversed" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons (tptr tuint) Tnil) tuint cc_default)) :: + (___builtin_write16_reversed, + Gfun(External (EF_builtin "__builtin_write16_reversed" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid + cc_default)) (Tcons (tptr tushort) (Tcons tushort Tnil)) + tvoid cc_default)) :: + (___builtin_write32_reversed, + Gfun(External (EF_builtin "__builtin_write32_reversed" + (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid + cc_default)) (Tcons (tptr tuint) (Tcons tuint Tnil)) + tvoid cc_default)) :: + (___builtin_debug, + Gfun(External (EF_external "__builtin_debug" + (mksignature (AST.Tint :: nil) AST.Tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) + (Tcons tint Tnil) tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: + (_foo, Gfun(Internal f_foo)) :: (_main, Gfun(Internal f_main)) :: nil). + +Definition public_idents : list ident := +(_main :: _foo :: ___builtin_debug :: ___builtin_write32_reversed :: + ___builtin_write16_reversed :: ___builtin_read32_reversed :: + ___builtin_read16_reversed :: ___builtin_fnmsub :: ___builtin_fnmadd :: + ___builtin_fmsub :: ___builtin_fmadd :: ___builtin_fmin :: + ___builtin_fmax :: ___builtin_expect :: ___builtin_unreachable :: + ___builtin_va_end :: ___builtin_va_copy :: ___builtin_va_arg :: + ___builtin_va_start :: ___builtin_membar :: ___builtin_annot_intval :: + ___builtin_annot :: ___builtin_sel :: ___builtin_memcpy_aligned :: + ___builtin_sqrt :: ___builtin_fsqrt :: ___builtin_fabsf :: + ___builtin_fabs :: ___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz :: + ___builtin_clzll :: ___builtin_clzl :: ___builtin_clz :: + ___builtin_bswap16 :: ___builtin_bswap32 :: ___builtin_bswap :: + ___builtin_bswap64 :: ___builtin_ais_annot :: ___compcert_i64_umulh :: + ___compcert_i64_smulh :: ___compcert_i64_sar :: ___compcert_i64_shr :: + ___compcert_i64_shl :: ___compcert_i64_umod :: ___compcert_i64_smod :: + ___compcert_i64_udiv :: ___compcert_i64_sdiv :: ___compcert_i64_utof :: + ___compcert_i64_stof :: ___compcert_i64_utod :: ___compcert_i64_stod :: + ___compcert_i64_dtou :: ___compcert_i64_dtos :: ___compcert_va_composite :: + ___compcert_va_float64 :: ___compcert_va_int64 :: ___compcert_va_int32 :: + nil). + +Definition prog : Clight.program := + mkprogram composites global_definitions public_idents _main Logic.I. + + diff --git a/progs/verif_alias2.v b/progs/verif_alias2.v new file mode 100644 index 0000000000..63ea16816d --- /dev/null +++ b/progs/verif_alias2.v @@ -0,0 +1,64 @@ +Require Import VST.floyd.proofauto. +Require Import VST.progs.alias2. + +Lemma field_compatible_void_int cs p : @field_compatible cs (tptr Tvoid) [] p = @field_compatible cs tint [] p. +Proof. + eapply PropExtensionality.propositional_extensionality. + destruct p; + cbv [field_compatible align_compatible size_compatible]; + intuition idtac; + repeat match goal with + | H : align_compatible_rec _ _ _ |- _ => inversion H; clear H; subst end. + all : econstructor; eauto. +Qed. + +Lemma data_at__void_int cs sh p : @data_at_ cs sh (tptr Tvoid) p = @data_at_ cs sh tint p. +Proof. rewrite 2data_at__memory_block, field_compatible_void_int; trivial. Qed. + +Lemma data_at_void_int_null cs sh p : @data_at cs sh (tptr Tvoid) (Vint Int.zero) p = @data_at cs sh tint (Vint Int.zero) p. +Proof. + cbv [data_at field_at at_offset nested_field_type tptr]. + simpl data_at_rec. + unfold data_at_rec. + simpl rank_type. + simpl type_induction.type_func. + rewrite field_compatible_void_int; f_equal. + change (Tint I32 Signed noattr) with tint. + erewrite mapsto_null_mapsto_pointer; reflexivity. +Qed. + + +#[export] Instance CompSpecs : compspecs. +Proof. make_compspecs prog. Defined. +Definition Vprog : varspecs. mk_varspecs prog. Defined. + +Definition foo_spec := DECLARE _foo WITH p : val + PRE [ tptr tint, tptr (tptr Tvoid) ] PROP() PARAMS(p; p) SEP(data_at_ Tsh tint p) + POST [ tint ] PROP() RETURN(Vint Int.zero) SEP(data_at_ Tsh tint p). + +Definition main_spec := DECLARE _main WITH gv : globals + PRE [] main_pre prog tt gv + POST [ tint ] PROP() RETURN (Vint Int.zero) SEP(has_ext tt). + +Definition Gprog : funspecs := ltac:(with_library prog [foo_spec; main_spec]). + +Lemma body_main : semax_body Vprog Gprog f_main main_spec. +Proof. start_function. forward_call. forward. entailer!. Qed. + +Lemma body_foo : semax_body Vprog Gprog f_foo foo_spec. +Proof. + start_function. + forward. + match goal with | |- context[data_at ?sh ?t ?Vs ?op] => sep_apply (data_at_data_at_ sh t Vs op) end. + erewrite <-data_at__void_int. + forward. + rewrite data_at_void_int_null. + forward. + forward. + entailer!. +Qed. + +Definition Espec := add_funspecs NullExtension.Espec (ext_link_prog prog) Gprog. +#[export] Existing Instance Espec. +Lemma prog_correct: semax_prog prog tt Vprog Gprog. +Proof. prove_semax_prog. semax_func_cons body_foo. semax_func_cons body_main. Qed. From 23ac6390d185fb1d62d37de1ff094499a6843c01 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 23 Oct 2022 17:43:52 -0400 Subject: [PATCH 3/6] Remove progs/alias and rename alias2 to alias --- .gitignore | 4 - Makefile | 2 +- progs/alias.c | 59 +++--- progs/alias.light.c | 4 +- progs/alias.v | 7 +- progs/alias2.c | 60 ------- progs/alias2.light.c | 41 ----- progs/alias2.v | 420 ------------------------------------------- progs/verif_alias.v | 41 ++++- progs/verif_alias2.v | 64 ------- 10 files changed, 70 insertions(+), 632 deletions(-) delete mode 100644 progs/alias2.c delete mode 100644 progs/alias2.light.c delete mode 100644 progs/alias2.v delete mode 100644 progs/verif_alias2.v diff --git a/.gitignore b/.gitignore index 3a07a5cf39..ceedd115df 100644 --- a/.gitignore +++ b/.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 diff --git a/Makefile b/Makefile index 35cd0a60b1..677f8dfc3d 100644 --- a/Makefile +++ b/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 \ diff --git a/progs/alias.c b/progs/alias.c index 148e4d7839..734df51296 100644 --- a/progs/alias.c +++ b/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 $? diff --git a/progs/alias.light.c b/progs/alias.light.c index 78e575c5ac..2b87ed581f 100644 --- a/progs/alias.light.c +++ b/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; diff --git a/progs/alias.v b/progs/alias.v index 37b532124f..ec5b54ac71 100644 --- a/progs/alias.v +++ b/progs/alias.v @@ -85,7 +85,7 @@ 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 := @@ -93,7 +93,7 @@ Definition f_foo := {| (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)) diff --git a/progs/alias2.c b/progs/alias2.c deleted file mode 100644 index 932f114317..0000000000 --- a/progs/alias2.c +++ /dev/null @@ -1,60 +0,0 @@ -int foo(int *p, void **q) { - *p = 1; - *q = 0; - return *p; -} -int main() { - 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. - -It returns 0 in the following invocations of clang 14.0.6 and gcc 12.2.0: - -clang -m32 -O0 -w alias2.c -o alias2 && ./alias2; echo $? -gcc -m32 -O0 -w alias2.c -o alias2 && ./alias2; echo $? -gcc -m32 -O1 -w alias2.c -o alias2 && ./alias2; echo $? -clang -m32 -fno-strict-aliasing -O1 -w alias2.c -o alias2 && ./alias2; echo $? -clang -m32 -fno-strict-aliasing -O2 -w alias2.c -o alias2 && ./alias2; echo $? -clang -m32 -fno-strict-aliasing -O3 -w alias2.c -o alias2 && ./alias2; echo $? -gcc -m32 -fno-strict-aliasing -O2 -w alias2.c -o alias2 && ./alias2; echo $? -gcc -m32 -fno-strict-aliasing -O3 -w alias2.c -o alias2 && ./alias2; echo $? - -It also returns 0 with CompCert a1f01c844aaa0ff41aa9095e9d5d01606a0e90c9 (3.11++): - -../../CompCert/ccomp alias2.c -c alias2.o && gcc -m32 alias2.o -o alias2 && ./alias2; echo $? - -It returns 1 in the following invocations of clang 14.0.6 and gcc 12.2.0: - -clang -m32 -O1 -w alias2.c -o alias2 && ./alias2; echo $? -clang -m32 -O2 -w alias2.c -o alias2 && ./alias2; echo $? -clang -m32 -O3 -w alias2.c -o alias2 && ./alias2; echo $? -gcc -m32 -O2 -w alias2.c -o alias2 && ./alias2; echo $? -gcc -m32 -O3 -w alias2.c -o alias2 && ./alias2; echo $? - -alias2.v was generated using the following invocation: - -../../CompCert/clightgen -dall -normalize -nostdinc -P -std=c11 alias2.c - -The corresponding clight file returns 0 in all invocations where the input file returned 0: - -clang -m32 -O0 -w alias2.light.c -o alias2 && ./alias2; echo $? -gcc -m32 -O0 -w alias2.light.c -o alias2 && ./alias2; echo $? -gcc -m32 -O1 -w alias2.light.c -o alias2 && ./alias2; echo $? -clang -m32 -fno-strict-aliasing -O1 -w alias2.light.c -o alias2 && ./alias2; echo $? -clang -m32 -fno-strict-aliasing -O2 -w alias2.light.c -o alias2 && ./alias2; echo $? -clang -m32 -fno-strict-aliasing -O3 -w alias2.light.c -o alias2 && ./alias2; echo $? -gcc -m32 -fno-strict-aliasing -O2 -w alias2.light.c -o alias2 && ./alias2; echo $? -gcc -m32 -fno-strict-aliasing -O3 -w alias2.light.c -o alias2 && ./alias2; echo $? - -... and returns 1 in all invocations where the input file returned 1: - -clang -m32 -O1 -w alias2.light.c -o alias2 && ./alias2; echo $? -clang -m32 -O2 -w alias2.light.c -o alias2 && ./alias2; echo $? -clang -m32 -O3 -w alias2.light.c -o alias2 && ./alias2; echo $? -gcc -m32 -O2 -w alias2.light.c -o alias2 && ./alias2; echo $? -gcc -m32 -O3 -w alias2.light.c -o alias2 && ./alias2; echo $? -*/ diff --git a/progs/alias2.light.c b/progs/alias2.light.c deleted file mode 100644 index 2b87ed581f..0000000000 --- a/progs/alias2.light.c +++ /dev/null @@ -1,41 +0,0 @@ -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; -} - - diff --git a/progs/alias2.v b/progs/alias2.v deleted file mode 100644 index c32f82290b..0000000000 --- a/progs/alias2.v +++ /dev/null @@ -1,420 +0,0 @@ -From Coq Require Import String List ZArith. -From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs. -Import Clightdefs.ClightNotations. -Local Open Scope Z_scope. -Local Open Scope string_scope. -Local Open Scope clight_scope. - -Module Info. - Definition version := "3.11". - Definition build_number := "". - Definition build_tag := "". - Definition build_branch := "". - Definition arch := "x86". - Definition model := "32sse2". - Definition abi := "standard". - Definition bitsize := 32. - Definition big_endian := false. - Definition source_file := "alias2.c". - Definition normalized := true. -End Info. - -Definition ___builtin_ais_annot : ident := $"__builtin_ais_annot". -Definition ___builtin_annot : ident := $"__builtin_annot". -Definition ___builtin_annot_intval : ident := $"__builtin_annot_intval". -Definition ___builtin_bswap : ident := $"__builtin_bswap". -Definition ___builtin_bswap16 : ident := $"__builtin_bswap16". -Definition ___builtin_bswap32 : ident := $"__builtin_bswap32". -Definition ___builtin_bswap64 : ident := $"__builtin_bswap64". -Definition ___builtin_clz : ident := $"__builtin_clz". -Definition ___builtin_clzl : ident := $"__builtin_clzl". -Definition ___builtin_clzll : ident := $"__builtin_clzll". -Definition ___builtin_ctz : ident := $"__builtin_ctz". -Definition ___builtin_ctzl : ident := $"__builtin_ctzl". -Definition ___builtin_ctzll : ident := $"__builtin_ctzll". -Definition ___builtin_debug : ident := $"__builtin_debug". -Definition ___builtin_expect : ident := $"__builtin_expect". -Definition ___builtin_fabs : ident := $"__builtin_fabs". -Definition ___builtin_fabsf : ident := $"__builtin_fabsf". -Definition ___builtin_fmadd : ident := $"__builtin_fmadd". -Definition ___builtin_fmax : ident := $"__builtin_fmax". -Definition ___builtin_fmin : ident := $"__builtin_fmin". -Definition ___builtin_fmsub : ident := $"__builtin_fmsub". -Definition ___builtin_fnmadd : ident := $"__builtin_fnmadd". -Definition ___builtin_fnmsub : ident := $"__builtin_fnmsub". -Definition ___builtin_fsqrt : ident := $"__builtin_fsqrt". -Definition ___builtin_membar : ident := $"__builtin_membar". -Definition ___builtin_memcpy_aligned : ident := $"__builtin_memcpy_aligned". -Definition ___builtin_read16_reversed : ident := $"__builtin_read16_reversed". -Definition ___builtin_read32_reversed : ident := $"__builtin_read32_reversed". -Definition ___builtin_sel : ident := $"__builtin_sel". -Definition ___builtin_sqrt : ident := $"__builtin_sqrt". -Definition ___builtin_unreachable : ident := $"__builtin_unreachable". -Definition ___builtin_va_arg : ident := $"__builtin_va_arg". -Definition ___builtin_va_copy : ident := $"__builtin_va_copy". -Definition ___builtin_va_end : ident := $"__builtin_va_end". -Definition ___builtin_va_start : ident := $"__builtin_va_start". -Definition ___builtin_write16_reversed : ident := $"__builtin_write16_reversed". -Definition ___builtin_write32_reversed : ident := $"__builtin_write32_reversed". -Definition ___compcert_i64_dtos : ident := $"__compcert_i64_dtos". -Definition ___compcert_i64_dtou : ident := $"__compcert_i64_dtou". -Definition ___compcert_i64_sar : ident := $"__compcert_i64_sar". -Definition ___compcert_i64_sdiv : ident := $"__compcert_i64_sdiv". -Definition ___compcert_i64_shl : ident := $"__compcert_i64_shl". -Definition ___compcert_i64_shr : ident := $"__compcert_i64_shr". -Definition ___compcert_i64_smod : ident := $"__compcert_i64_smod". -Definition ___compcert_i64_smulh : ident := $"__compcert_i64_smulh". -Definition ___compcert_i64_stod : ident := $"__compcert_i64_stod". -Definition ___compcert_i64_stof : ident := $"__compcert_i64_stof". -Definition ___compcert_i64_udiv : ident := $"__compcert_i64_udiv". -Definition ___compcert_i64_umod : ident := $"__compcert_i64_umod". -Definition ___compcert_i64_umulh : ident := $"__compcert_i64_umulh". -Definition ___compcert_i64_utod : ident := $"__compcert_i64_utod". -Definition ___compcert_i64_utof : ident := $"__compcert_i64_utof". -Definition ___compcert_va_composite : ident := $"__compcert_va_composite". -Definition ___compcert_va_float64 : ident := $"__compcert_va_float64". -Definition ___compcert_va_int32 : ident := $"__compcert_va_int32". -Definition ___compcert_va_int64 : ident := $"__compcert_va_int64". -Definition _foo : ident := $"foo". -Definition _main : ident := $"main". -Definition _p : ident := $"p". -Definition _q : ident := $"q". -Definition _x : ident := $"x". -Definition _t'1 : ident := 128%positive. - -Definition f_foo := {| - fn_return := tint; - fn_callconv := cc_default; - 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 (tptr tvoid))) (tptr tvoid)) - (Econst_int (Int.repr 0) tint)) - (Ssequence - (Sset _t'1 (Ederef (Etempvar _p (tptr tint)) tint)) - (Sreturn (Some (Etempvar _t'1 tint)))))) -|}. - -Definition f_main := {| - fn_return := tint; - fn_callconv := cc_default; - fn_params := nil; - fn_vars := ((_x, tint) :: nil); - fn_temps := ((_t'1, tint) :: nil); - fn_body := -(Ssequence - (Ssequence - (Scall (Some _t'1) - (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)) - (Sreturn (Some (Etempvar _t'1 tint)))) - (Sreturn (Some (Econst_int (Int.repr 0) tint)))) -|}. - -Definition composites : list composite_definition := -nil. - -Definition global_definitions : list (ident * globdef fundef type) := -((___compcert_va_int32, - Gfun(External (EF_runtime "__compcert_va_int32" - (mksignature (AST.Tint :: nil) AST.Tint cc_default)) - (Tcons (tptr tvoid) Tnil) tuint cc_default)) :: - (___compcert_va_int64, - Gfun(External (EF_runtime "__compcert_va_int64" - (mksignature (AST.Tint :: nil) AST.Tlong cc_default)) - (Tcons (tptr tvoid) Tnil) tulong cc_default)) :: - (___compcert_va_float64, - Gfun(External (EF_runtime "__compcert_va_float64" - (mksignature (AST.Tint :: nil) AST.Tfloat cc_default)) - (Tcons (tptr tvoid) Tnil) tdouble cc_default)) :: - (___compcert_va_composite, - Gfun(External (EF_runtime "__compcert_va_composite" - (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint - cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil)) - (tptr tvoid) cc_default)) :: - (___compcert_i64_dtos, - Gfun(External (EF_runtime "__compcert_i64_dtos" - (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default)) - (Tcons tdouble Tnil) tlong cc_default)) :: - (___compcert_i64_dtou, - Gfun(External (EF_runtime "__compcert_i64_dtou" - (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default)) - (Tcons tdouble Tnil) tulong cc_default)) :: - (___compcert_i64_stod, - Gfun(External (EF_runtime "__compcert_i64_stod" - (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default)) - (Tcons tlong Tnil) tdouble cc_default)) :: - (___compcert_i64_utod, - Gfun(External (EF_runtime "__compcert_i64_utod" - (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default)) - (Tcons tulong Tnil) tdouble cc_default)) :: - (___compcert_i64_stof, - Gfun(External (EF_runtime "__compcert_i64_stof" - (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default)) - (Tcons tlong Tnil) tfloat cc_default)) :: - (___compcert_i64_utof, - Gfun(External (EF_runtime "__compcert_i64_utof" - (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default)) - (Tcons tulong Tnil) tfloat cc_default)) :: - (___compcert_i64_sdiv, - Gfun(External (EF_runtime "__compcert_i64_sdiv" - (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong - cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong - cc_default)) :: - (___compcert_i64_udiv, - Gfun(External (EF_runtime "__compcert_i64_udiv" - (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong - cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong - cc_default)) :: - (___compcert_i64_smod, - Gfun(External (EF_runtime "__compcert_i64_smod" - (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong - cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong - cc_default)) :: - (___compcert_i64_umod, - Gfun(External (EF_runtime "__compcert_i64_umod" - (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong - cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong - cc_default)) :: - (___compcert_i64_shl, - Gfun(External (EF_runtime "__compcert_i64_shl" - (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong - cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong - cc_default)) :: - (___compcert_i64_shr, - Gfun(External (EF_runtime "__compcert_i64_shr" - (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong - cc_default)) (Tcons tulong (Tcons tint Tnil)) tulong - cc_default)) :: - (___compcert_i64_sar, - Gfun(External (EF_runtime "__compcert_i64_sar" - (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong - cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong - cc_default)) :: - (___compcert_i64_smulh, - Gfun(External (EF_runtime "__compcert_i64_smulh" - (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong - cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong - cc_default)) :: - (___compcert_i64_umulh, - Gfun(External (EF_runtime "__compcert_i64_umulh" - (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong - cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong - cc_default)) :: - (___builtin_ais_annot, - Gfun(External (EF_builtin "__builtin_ais_annot" - (mksignature (AST.Tint :: nil) AST.Tvoid - {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) - (Tcons (tptr tschar) Tnil) tvoid - {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: - (___builtin_bswap64, - Gfun(External (EF_builtin "__builtin_bswap64" - (mksignature (AST.Tlong :: nil) AST.Tlong cc_default)) - (Tcons tulong Tnil) tulong cc_default)) :: - (___builtin_bswap, - Gfun(External (EF_builtin "__builtin_bswap" - (mksignature (AST.Tint :: nil) AST.Tint cc_default)) - (Tcons tuint Tnil) tuint cc_default)) :: - (___builtin_bswap32, - Gfun(External (EF_builtin "__builtin_bswap32" - (mksignature (AST.Tint :: nil) AST.Tint cc_default)) - (Tcons tuint Tnil) tuint cc_default)) :: - (___builtin_bswap16, - Gfun(External (EF_builtin "__builtin_bswap16" - (mksignature (AST.Tint :: nil) AST.Tint16unsigned - cc_default)) (Tcons tushort Tnil) tushort cc_default)) :: - (___builtin_clz, - Gfun(External (EF_builtin "__builtin_clz" - (mksignature (AST.Tint :: nil) AST.Tint cc_default)) - (Tcons tuint Tnil) tint cc_default)) :: - (___builtin_clzl, - Gfun(External (EF_builtin "__builtin_clzl" - (mksignature (AST.Tint :: nil) AST.Tint cc_default)) - (Tcons tuint Tnil) tint cc_default)) :: - (___builtin_clzll, - Gfun(External (EF_builtin "__builtin_clzll" - (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) - (Tcons tulong Tnil) tint cc_default)) :: - (___builtin_ctz, - Gfun(External (EF_builtin "__builtin_ctz" - (mksignature (AST.Tint :: nil) AST.Tint cc_default)) - (Tcons tuint Tnil) tint cc_default)) :: - (___builtin_ctzl, - Gfun(External (EF_builtin "__builtin_ctzl" - (mksignature (AST.Tint :: nil) AST.Tint cc_default)) - (Tcons tuint Tnil) tint cc_default)) :: - (___builtin_ctzll, - Gfun(External (EF_builtin "__builtin_ctzll" - (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) - (Tcons tulong Tnil) tint cc_default)) :: - (___builtin_fabs, - Gfun(External (EF_builtin "__builtin_fabs" - (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) - (Tcons tdouble Tnil) tdouble cc_default)) :: - (___builtin_fabsf, - Gfun(External (EF_builtin "__builtin_fabsf" - (mksignature (AST.Tsingle :: nil) AST.Tsingle cc_default)) - (Tcons tfloat Tnil) tfloat cc_default)) :: - (___builtin_fsqrt, - Gfun(External (EF_builtin "__builtin_fsqrt" - (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) - (Tcons tdouble Tnil) tdouble cc_default)) :: - (___builtin_sqrt, - Gfun(External (EF_builtin "__builtin_sqrt" - (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) - (Tcons tdouble Tnil) tdouble cc_default)) :: - (___builtin_memcpy_aligned, - Gfun(External (EF_builtin "__builtin_memcpy_aligned" - (mksignature - (AST.Tint :: AST.Tint :: AST.Tint :: AST.Tint :: nil) - AST.Tvoid cc_default)) - (Tcons (tptr tvoid) - (Tcons (tptr tvoid) (Tcons tuint (Tcons tuint Tnil)))) tvoid - cc_default)) :: - (___builtin_sel, - Gfun(External (EF_builtin "__builtin_sel" - (mksignature (AST.Tint :: nil) AST.Tvoid - {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) - (Tcons tbool Tnil) tvoid - {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: - (___builtin_annot, - Gfun(External (EF_builtin "__builtin_annot" - (mksignature (AST.Tint :: nil) AST.Tvoid - {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) - (Tcons (tptr tschar) Tnil) tvoid - {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: - (___builtin_annot_intval, - Gfun(External (EF_builtin "__builtin_annot_intval" - (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint - cc_default)) (Tcons (tptr tschar) (Tcons tint Tnil)) - tint cc_default)) :: - (___builtin_membar, - Gfun(External (EF_builtin "__builtin_membar" - (mksignature nil AST.Tvoid cc_default)) Tnil tvoid - cc_default)) :: - (___builtin_va_start, - Gfun(External (EF_builtin "__builtin_va_start" - (mksignature (AST.Tint :: nil) AST.Tvoid cc_default)) - (Tcons (tptr tvoid) Tnil) tvoid cc_default)) :: - (___builtin_va_arg, - Gfun(External (EF_builtin "__builtin_va_arg" - (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid - cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil)) - tvoid cc_default)) :: - (___builtin_va_copy, - Gfun(External (EF_builtin "__builtin_va_copy" - (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid - cc_default)) - (Tcons (tptr tvoid) (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) :: - (___builtin_va_end, - Gfun(External (EF_builtin "__builtin_va_end" - (mksignature (AST.Tint :: nil) AST.Tvoid cc_default)) - (Tcons (tptr tvoid) Tnil) tvoid cc_default)) :: - (___builtin_unreachable, - Gfun(External (EF_builtin "__builtin_unreachable" - (mksignature nil AST.Tvoid cc_default)) Tnil tvoid - cc_default)) :: - (___builtin_expect, - Gfun(External (EF_builtin "__builtin_expect" - (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint - cc_default)) (Tcons tint (Tcons tint Tnil)) tint - cc_default)) :: - (___builtin_fmax, - Gfun(External (EF_builtin "__builtin_fmax" - (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat - cc_default)) (Tcons tdouble (Tcons tdouble Tnil)) - tdouble cc_default)) :: - (___builtin_fmin, - Gfun(External (EF_builtin "__builtin_fmin" - (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat - cc_default)) (Tcons tdouble (Tcons tdouble Tnil)) - tdouble cc_default)) :: - (___builtin_fmadd, - Gfun(External (EF_builtin "__builtin_fmadd" - (mksignature - (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) - AST.Tfloat cc_default)) - (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble - cc_default)) :: - (___builtin_fmsub, - Gfun(External (EF_builtin "__builtin_fmsub" - (mksignature - (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) - AST.Tfloat cc_default)) - (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble - cc_default)) :: - (___builtin_fnmadd, - Gfun(External (EF_builtin "__builtin_fnmadd" - (mksignature - (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) - AST.Tfloat cc_default)) - (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble - cc_default)) :: - (___builtin_fnmsub, - Gfun(External (EF_builtin "__builtin_fnmsub" - (mksignature - (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) - AST.Tfloat cc_default)) - (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble - cc_default)) :: - (___builtin_read16_reversed, - Gfun(External (EF_builtin "__builtin_read16_reversed" - (mksignature (AST.Tint :: nil) AST.Tint16unsigned - cc_default)) (Tcons (tptr tushort) Tnil) tushort - cc_default)) :: - (___builtin_read32_reversed, - Gfun(External (EF_builtin "__builtin_read32_reversed" - (mksignature (AST.Tint :: nil) AST.Tint cc_default)) - (Tcons (tptr tuint) Tnil) tuint cc_default)) :: - (___builtin_write16_reversed, - Gfun(External (EF_builtin "__builtin_write16_reversed" - (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid - cc_default)) (Tcons (tptr tushort) (Tcons tushort Tnil)) - tvoid cc_default)) :: - (___builtin_write32_reversed, - Gfun(External (EF_builtin "__builtin_write32_reversed" - (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid - cc_default)) (Tcons (tptr tuint) (Tcons tuint Tnil)) - tvoid cc_default)) :: - (___builtin_debug, - Gfun(External (EF_external "__builtin_debug" - (mksignature (AST.Tint :: nil) AST.Tvoid - {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) - (Tcons tint Tnil) tvoid - {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: - (_foo, Gfun(Internal f_foo)) :: (_main, Gfun(Internal f_main)) :: nil). - -Definition public_idents : list ident := -(_main :: _foo :: ___builtin_debug :: ___builtin_write32_reversed :: - ___builtin_write16_reversed :: ___builtin_read32_reversed :: - ___builtin_read16_reversed :: ___builtin_fnmsub :: ___builtin_fnmadd :: - ___builtin_fmsub :: ___builtin_fmadd :: ___builtin_fmin :: - ___builtin_fmax :: ___builtin_expect :: ___builtin_unreachable :: - ___builtin_va_end :: ___builtin_va_copy :: ___builtin_va_arg :: - ___builtin_va_start :: ___builtin_membar :: ___builtin_annot_intval :: - ___builtin_annot :: ___builtin_sel :: ___builtin_memcpy_aligned :: - ___builtin_sqrt :: ___builtin_fsqrt :: ___builtin_fabsf :: - ___builtin_fabs :: ___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz :: - ___builtin_clzll :: ___builtin_clzl :: ___builtin_clz :: - ___builtin_bswap16 :: ___builtin_bswap32 :: ___builtin_bswap :: - ___builtin_bswap64 :: ___builtin_ais_annot :: ___compcert_i64_umulh :: - ___compcert_i64_smulh :: ___compcert_i64_sar :: ___compcert_i64_shr :: - ___compcert_i64_shl :: ___compcert_i64_umod :: ___compcert_i64_smod :: - ___compcert_i64_udiv :: ___compcert_i64_sdiv :: ___compcert_i64_utof :: - ___compcert_i64_stof :: ___compcert_i64_utod :: ___compcert_i64_stod :: - ___compcert_i64_dtou :: ___compcert_i64_dtos :: ___compcert_va_composite :: - ___compcert_va_float64 :: ___compcert_va_int64 :: ___compcert_va_int32 :: - nil). - -Definition prog : Clight.program := - mkprogram composites global_definitions public_idents _main Logic.I. - - diff --git a/progs/verif_alias.v b/progs/verif_alias.v index 2515829bcf..5e56a8f079 100644 --- a/progs/verif_alias.v +++ b/progs/verif_alias.v @@ -1,12 +1,39 @@ Require Import VST.floyd.proofauto. Require Import VST.progs.alias. +Lemma field_compatible_void_int cs p : @field_compatible cs (tptr Tvoid) [] p = @field_compatible cs tint [] p. +Proof. + eapply PropExtensionality.propositional_extensionality. + destruct p; + cbv [field_compatible align_compatible size_compatible]; + intuition idtac; + repeat match goal with + | H : align_compatible_rec _ _ _ |- _ => inversion H; clear H; subst end. + all : econstructor; eauto. +Qed. + +Lemma data_at__void_int cs sh p : @data_at_ cs sh (tptr Tvoid) p = @data_at_ cs sh tint p. +Proof. rewrite 2data_at__memory_block, field_compatible_void_int; trivial. Qed. + +Lemma data_at_void_int_null cs sh p : @data_at cs sh (tptr Tvoid) (Vint Int.zero) p = @data_at cs sh tint (Vint Int.zero) p. +Proof. + cbv [data_at field_at at_offset nested_field_type tptr]. + simpl data_at_rec. + unfold data_at_rec. + simpl rank_type. + simpl type_induction.type_func. + rewrite field_compatible_void_int; f_equal. + change (Tint I32 Signed noattr) with tint. + erewrite mapsto_null_mapsto_pointer; reflexivity. +Qed. + + #[export] Instance CompSpecs : compspecs. Proof. make_compspecs prog. Defined. Definition Vprog : varspecs. mk_varspecs prog. Defined. Definition foo_spec := DECLARE _foo WITH p : val - PRE [ tptr tint, tptr tint ] PROP() PARAMS(p; p) SEP(data_at_ Tsh tint p) + PRE [ tptr tint, tptr (tptr Tvoid) ] PROP() PARAMS(p; p) SEP(data_at_ Tsh tint p) POST [ tint ] PROP() RETURN(Vint Int.zero) SEP(data_at_ Tsh tint p). Definition main_spec := DECLARE _main WITH gv : globals @@ -19,7 +46,17 @@ Lemma body_main : semax_body Vprog Gprog f_main main_spec. Proof. start_function. forward_call. forward. entailer!. Qed. Lemma body_foo : semax_body Vprog Gprog f_foo foo_spec. -Proof. start_function. repeat forward. entailer!. Qed. +Proof. + start_function. + forward. + match goal with | |- context[data_at ?sh ?t ?Vs ?op] => sep_apply (data_at_data_at_ sh t Vs op) end. + erewrite <-data_at__void_int. + forward. + rewrite data_at_void_int_null. + forward. + forward. + entailer!. +Qed. Definition Espec := add_funspecs NullExtension.Espec (ext_link_prog prog) Gprog. #[export] Existing Instance Espec. diff --git a/progs/verif_alias2.v b/progs/verif_alias2.v deleted file mode 100644 index 63ea16816d..0000000000 --- a/progs/verif_alias2.v +++ /dev/null @@ -1,64 +0,0 @@ -Require Import VST.floyd.proofauto. -Require Import VST.progs.alias2. - -Lemma field_compatible_void_int cs p : @field_compatible cs (tptr Tvoid) [] p = @field_compatible cs tint [] p. -Proof. - eapply PropExtensionality.propositional_extensionality. - destruct p; - cbv [field_compatible align_compatible size_compatible]; - intuition idtac; - repeat match goal with - | H : align_compatible_rec _ _ _ |- _ => inversion H; clear H; subst end. - all : econstructor; eauto. -Qed. - -Lemma data_at__void_int cs sh p : @data_at_ cs sh (tptr Tvoid) p = @data_at_ cs sh tint p. -Proof. rewrite 2data_at__memory_block, field_compatible_void_int; trivial. Qed. - -Lemma data_at_void_int_null cs sh p : @data_at cs sh (tptr Tvoid) (Vint Int.zero) p = @data_at cs sh tint (Vint Int.zero) p. -Proof. - cbv [data_at field_at at_offset nested_field_type tptr]. - simpl data_at_rec. - unfold data_at_rec. - simpl rank_type. - simpl type_induction.type_func. - rewrite field_compatible_void_int; f_equal. - change (Tint I32 Signed noattr) with tint. - erewrite mapsto_null_mapsto_pointer; reflexivity. -Qed. - - -#[export] Instance CompSpecs : compspecs. -Proof. make_compspecs prog. Defined. -Definition Vprog : varspecs. mk_varspecs prog. Defined. - -Definition foo_spec := DECLARE _foo WITH p : val - PRE [ tptr tint, tptr (tptr Tvoid) ] PROP() PARAMS(p; p) SEP(data_at_ Tsh tint p) - POST [ tint ] PROP() RETURN(Vint Int.zero) SEP(data_at_ Tsh tint p). - -Definition main_spec := DECLARE _main WITH gv : globals - PRE [] main_pre prog tt gv - POST [ tint ] PROP() RETURN (Vint Int.zero) SEP(has_ext tt). - -Definition Gprog : funspecs := ltac:(with_library prog [foo_spec; main_spec]). - -Lemma body_main : semax_body Vprog Gprog f_main main_spec. -Proof. start_function. forward_call. forward. entailer!. Qed. - -Lemma body_foo : semax_body Vprog Gprog f_foo foo_spec. -Proof. - start_function. - forward. - match goal with | |- context[data_at ?sh ?t ?Vs ?op] => sep_apply (data_at_data_at_ sh t Vs op) end. - erewrite <-data_at__void_int. - forward. - rewrite data_at_void_int_null. - forward. - forward. - entailer!. -Qed. - -Definition Espec := add_funspecs NullExtension.Espec (ext_link_prog prog) Gprog. -#[export] Existing Instance Espec. -Lemma prog_correct: semax_prog prog tt Vprog Gprog. -Proof. prove_semax_prog. semax_func_cons body_foo. semax_func_cons body_main. Qed. From 32203923e7a8712d6dedf33b4d7ac84e27d46165 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 24 Oct 2022 17:57:01 -0400 Subject: [PATCH 4/6] use long instead of int in alias.c --- progs/alias.c | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/progs/alias.c b/progs/alias.c index 734df51296..b3d2beabe2 100644 --- a/progs/alias.c +++ b/progs/alias.c @@ -1,10 +1,10 @@ -int foo(int *p, void **q) { +long foo(long *p, void **q) { *p = 1; *q = 0; return *p; } int main() { - int x; + long x; return foo(&x, &x); } @@ -16,10 +16,10 @@ 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 +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 int and void * have size and alignment. The -ubiquitous compiler flag -fno-strict-aliasing lifts these restrictions. +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. 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++). @@ -38,6 +38,7 @@ 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: From a112012c689f7be8df5ce981d83a14af5c51415b Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 24 Oct 2022 18:38:12 -0400 Subject: [PATCH 5/6] add and prove progs64/alias.c --- .gitignore | 4 + Makefile | 3 +- progs64/alias.c | 73 ++++++++ progs64/alias.light.c | 41 +++++ progs64/alias.v | 420 ++++++++++++++++++++++++++++++++++++++++++ progs64/verif_alias.v | 65 +++++++ 6 files changed, 605 insertions(+), 1 deletion(-) create mode 100644 progs64/alias.c create mode 100644 progs64/alias.light.c create mode 100644 progs64/alias.v create mode 100644 progs64/verif_alias.v diff --git a/.gitignore b/.gitignore index ceedd115df..0b63894459 100644 --- a/.gitignore +++ b/.gitignore @@ -66,6 +66,10 @@ 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 diff --git a/Makefile b/Makefile index 677f8dfc3d..2cfd43c9b7 100644 --- a/Makefile +++ b/Makefile @@ -514,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 \ diff --git a/progs64/alias.c b/progs64/alias.c new file mode 100644 index 0000000000..3895ba9816 --- /dev/null +++ b/progs64/alias.c @@ -0,0 +1,73 @@ +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 8-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. + +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 $? + +It also returns 0 with CompCert: + +../../CompCert/ccomp alias.c -c alias.o && gcc alias.o -o alias && ./alias; echo $? +../../CompCert/ccomp -interp alias.c + +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 $? + +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 -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 $? + +... and returns 1 in all invocations where the input file returned 1: + +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 $? +*/ diff --git a/progs64/alias.light.c b/progs64/alias.light.c new file mode 100644 index 0000000000..c536a4bc9a --- /dev/null +++ b/progs64/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 long long); +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, ...); +long long foo(long long *, void **); +int main(void); +long long foo(long long *$p, void **$q) +{ + register long long $128; + *$p = 1; + *$q = 0; + $128 = *$p; + return $128; +} + +int main(void) +{ + long long x; + register long long $128; + $128 = foo(&x, &x); + return $128; + return 0; +} + + diff --git a/progs64/alias.v b/progs64/alias.v new file mode 100644 index 0000000000..942f95c4f4 --- /dev/null +++ b/progs64/alias.v @@ -0,0 +1,420 @@ +From Coq Require Import String List ZArith. +From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs. +Import Clightdefs.ClightNotations. +Local Open Scope Z_scope. +Local Open Scope string_scope. +Local Open Scope clight_scope. + +Module Info. + Definition version := "3.11". + Definition build_number := "". + Definition build_tag := "". + Definition build_branch := "". + Definition arch := "x86". + Definition model := "64". + Definition abi := "standard". + Definition bitsize := 64. + Definition big_endian := false. + Definition source_file := "alias.c". + Definition normalized := true. +End Info. + +Definition ___builtin_ais_annot : ident := $"__builtin_ais_annot". +Definition ___builtin_annot : ident := $"__builtin_annot". +Definition ___builtin_annot_intval : ident := $"__builtin_annot_intval". +Definition ___builtin_bswap : ident := $"__builtin_bswap". +Definition ___builtin_bswap16 : ident := $"__builtin_bswap16". +Definition ___builtin_bswap32 : ident := $"__builtin_bswap32". +Definition ___builtin_bswap64 : ident := $"__builtin_bswap64". +Definition ___builtin_clz : ident := $"__builtin_clz". +Definition ___builtin_clzl : ident := $"__builtin_clzl". +Definition ___builtin_clzll : ident := $"__builtin_clzll". +Definition ___builtin_ctz : ident := $"__builtin_ctz". +Definition ___builtin_ctzl : ident := $"__builtin_ctzl". +Definition ___builtin_ctzll : ident := $"__builtin_ctzll". +Definition ___builtin_debug : ident := $"__builtin_debug". +Definition ___builtin_expect : ident := $"__builtin_expect". +Definition ___builtin_fabs : ident := $"__builtin_fabs". +Definition ___builtin_fabsf : ident := $"__builtin_fabsf". +Definition ___builtin_fmadd : ident := $"__builtin_fmadd". +Definition ___builtin_fmax : ident := $"__builtin_fmax". +Definition ___builtin_fmin : ident := $"__builtin_fmin". +Definition ___builtin_fmsub : ident := $"__builtin_fmsub". +Definition ___builtin_fnmadd : ident := $"__builtin_fnmadd". +Definition ___builtin_fnmsub : ident := $"__builtin_fnmsub". +Definition ___builtin_fsqrt : ident := $"__builtin_fsqrt". +Definition ___builtin_membar : ident := $"__builtin_membar". +Definition ___builtin_memcpy_aligned : ident := $"__builtin_memcpy_aligned". +Definition ___builtin_read16_reversed : ident := $"__builtin_read16_reversed". +Definition ___builtin_read32_reversed : ident := $"__builtin_read32_reversed". +Definition ___builtin_sel : ident := $"__builtin_sel". +Definition ___builtin_sqrt : ident := $"__builtin_sqrt". +Definition ___builtin_unreachable : ident := $"__builtin_unreachable". +Definition ___builtin_va_arg : ident := $"__builtin_va_arg". +Definition ___builtin_va_copy : ident := $"__builtin_va_copy". +Definition ___builtin_va_end : ident := $"__builtin_va_end". +Definition ___builtin_va_start : ident := $"__builtin_va_start". +Definition ___builtin_write16_reversed : ident := $"__builtin_write16_reversed". +Definition ___builtin_write32_reversed : ident := $"__builtin_write32_reversed". +Definition ___compcert_i64_dtos : ident := $"__compcert_i64_dtos". +Definition ___compcert_i64_dtou : ident := $"__compcert_i64_dtou". +Definition ___compcert_i64_sar : ident := $"__compcert_i64_sar". +Definition ___compcert_i64_sdiv : ident := $"__compcert_i64_sdiv". +Definition ___compcert_i64_shl : ident := $"__compcert_i64_shl". +Definition ___compcert_i64_shr : ident := $"__compcert_i64_shr". +Definition ___compcert_i64_smod : ident := $"__compcert_i64_smod". +Definition ___compcert_i64_smulh : ident := $"__compcert_i64_smulh". +Definition ___compcert_i64_stod : ident := $"__compcert_i64_stod". +Definition ___compcert_i64_stof : ident := $"__compcert_i64_stof". +Definition ___compcert_i64_udiv : ident := $"__compcert_i64_udiv". +Definition ___compcert_i64_umod : ident := $"__compcert_i64_umod". +Definition ___compcert_i64_umulh : ident := $"__compcert_i64_umulh". +Definition ___compcert_i64_utod : ident := $"__compcert_i64_utod". +Definition ___compcert_i64_utof : ident := $"__compcert_i64_utof". +Definition ___compcert_va_composite : ident := $"__compcert_va_composite". +Definition ___compcert_va_float64 : ident := $"__compcert_va_float64". +Definition ___compcert_va_int32 : ident := $"__compcert_va_int32". +Definition ___compcert_va_int64 : ident := $"__compcert_va_int64". +Definition _foo : ident := $"foo". +Definition _main : ident := $"main". +Definition _p : ident := $"p". +Definition _q : ident := $"q". +Definition _x : ident := $"x". +Definition _t'1 : ident := 128%positive. + +Definition f_foo := {| + fn_return := tlong; + fn_callconv := cc_default; + fn_params := ((_p, (tptr tlong)) :: (_q, (tptr (tptr tvoid))) :: nil); + fn_vars := nil; + fn_temps := ((_t'1, tlong) :: nil); + fn_body := +(Ssequence + (Sassign (Ederef (Etempvar _p (tptr tlong)) tlong) + (Econst_int (Int.repr 1) tint)) + (Ssequence + (Sassign (Ederef (Etempvar _q (tptr (tptr tvoid))) (tptr tvoid)) + (Econst_int (Int.repr 0) tint)) + (Ssequence + (Sset _t'1 (Ederef (Etempvar _p (tptr tlong)) tlong)) + (Sreturn (Some (Etempvar _t'1 tlong)))))) +|}. + +Definition f_main := {| + fn_return := tint; + fn_callconv := cc_default; + fn_params := nil; + fn_vars := ((_x, tlong) :: nil); + fn_temps := ((_t'1, tlong) :: nil); + fn_body := +(Ssequence + (Ssequence + (Scall (Some _t'1) + (Evar _foo (Tfunction + (Tcons (tptr tlong) (Tcons (tptr (tptr tvoid)) Tnil)) + tlong cc_default)) + ((Eaddrof (Evar _x tlong) (tptr tlong)) :: + (Eaddrof (Evar _x tlong) (tptr tlong)) :: nil)) + (Sreturn (Some (Etempvar _t'1 tlong)))) + (Sreturn (Some (Econst_int (Int.repr 0) tint)))) +|}. + +Definition composites : list composite_definition := +nil. + +Definition global_definitions : list (ident * globdef fundef type) := +((___compcert_va_int32, + Gfun(External (EF_runtime "__compcert_va_int32" + (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) + (Tcons (tptr tvoid) Tnil) tuint cc_default)) :: + (___compcert_va_int64, + Gfun(External (EF_runtime "__compcert_va_int64" + (mksignature (AST.Tlong :: nil) AST.Tlong cc_default)) + (Tcons (tptr tvoid) Tnil) tulong cc_default)) :: + (___compcert_va_float64, + Gfun(External (EF_runtime "__compcert_va_float64" + (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default)) + (Tcons (tptr tvoid) Tnil) tdouble cc_default)) :: + (___compcert_va_composite, + Gfun(External (EF_runtime "__compcert_va_composite" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons (tptr tvoid) (Tcons tulong Tnil)) + (tptr tvoid) cc_default)) :: + (___compcert_i64_dtos, + Gfun(External (EF_runtime "__compcert_i64_dtos" + (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default)) + (Tcons tdouble Tnil) tlong cc_default)) :: + (___compcert_i64_dtou, + Gfun(External (EF_runtime "__compcert_i64_dtou" + (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default)) + (Tcons tdouble Tnil) tulong cc_default)) :: + (___compcert_i64_stod, + Gfun(External (EF_runtime "__compcert_i64_stod" + (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default)) + (Tcons tlong Tnil) tdouble cc_default)) :: + (___compcert_i64_utod, + Gfun(External (EF_runtime "__compcert_i64_utod" + (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default)) + (Tcons tulong Tnil) tdouble cc_default)) :: + (___compcert_i64_stof, + Gfun(External (EF_runtime "__compcert_i64_stof" + (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default)) + (Tcons tlong Tnil) tfloat cc_default)) :: + (___compcert_i64_utof, + Gfun(External (EF_runtime "__compcert_i64_utof" + (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default)) + (Tcons tulong Tnil) tfloat cc_default)) :: + (___compcert_i64_sdiv, + Gfun(External (EF_runtime "__compcert_i64_sdiv" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong + cc_default)) :: + (___compcert_i64_udiv, + Gfun(External (EF_runtime "__compcert_i64_udiv" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong + cc_default)) :: + (___compcert_i64_smod, + Gfun(External (EF_runtime "__compcert_i64_smod" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong + cc_default)) :: + (___compcert_i64_umod, + Gfun(External (EF_runtime "__compcert_i64_umod" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong + cc_default)) :: + (___compcert_i64_shl, + Gfun(External (EF_runtime "__compcert_i64_shl" + (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong + cc_default)) :: + (___compcert_i64_shr, + Gfun(External (EF_runtime "__compcert_i64_shr" + (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong + cc_default)) (Tcons tulong (Tcons tint Tnil)) tulong + cc_default)) :: + (___compcert_i64_sar, + Gfun(External (EF_runtime "__compcert_i64_sar" + (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong + cc_default)) :: + (___compcert_i64_smulh, + Gfun(External (EF_runtime "__compcert_i64_smulh" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong + cc_default)) :: + (___compcert_i64_umulh, + Gfun(External (EF_runtime "__compcert_i64_umulh" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong + cc_default)) :: + (___builtin_ais_annot, + Gfun(External (EF_builtin "__builtin_ais_annot" + (mksignature (AST.Tlong :: nil) AST.Tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) + (Tcons (tptr tschar) Tnil) tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: + (___builtin_bswap64, + Gfun(External (EF_builtin "__builtin_bswap64" + (mksignature (AST.Tlong :: nil) AST.Tlong cc_default)) + (Tcons tulong Tnil) tulong cc_default)) :: + (___builtin_bswap, + Gfun(External (EF_builtin "__builtin_bswap" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tuint cc_default)) :: + (___builtin_bswap32, + Gfun(External (EF_builtin "__builtin_bswap32" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tuint cc_default)) :: + (___builtin_bswap16, + Gfun(External (EF_builtin "__builtin_bswap16" + (mksignature (AST.Tint :: nil) AST.Tint16unsigned + cc_default)) (Tcons tushort Tnil) tushort cc_default)) :: + (___builtin_clz, + Gfun(External (EF_builtin "__builtin_clz" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tint cc_default)) :: + (___builtin_clzl, + Gfun(External (EF_builtin "__builtin_clzl" + (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) + (Tcons tulong Tnil) tint cc_default)) :: + (___builtin_clzll, + Gfun(External (EF_builtin "__builtin_clzll" + (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) + (Tcons tulong Tnil) tint cc_default)) :: + (___builtin_ctz, + Gfun(External (EF_builtin "__builtin_ctz" + (mksignature (AST.Tint :: nil) AST.Tint cc_default)) + (Tcons tuint Tnil) tint cc_default)) :: + (___builtin_ctzl, + Gfun(External (EF_builtin "__builtin_ctzl" + (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) + (Tcons tulong Tnil) tint cc_default)) :: + (___builtin_ctzll, + Gfun(External (EF_builtin "__builtin_ctzll" + (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) + (Tcons tulong Tnil) tint cc_default)) :: + (___builtin_fabs, + Gfun(External (EF_builtin "__builtin_fabs" + (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) + (Tcons tdouble Tnil) tdouble cc_default)) :: + (___builtin_fabsf, + Gfun(External (EF_builtin "__builtin_fabsf" + (mksignature (AST.Tsingle :: nil) AST.Tsingle cc_default)) + (Tcons tfloat Tnil) tfloat cc_default)) :: + (___builtin_fsqrt, + Gfun(External (EF_builtin "__builtin_fsqrt" + (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) + (Tcons tdouble Tnil) tdouble cc_default)) :: + (___builtin_sqrt, + Gfun(External (EF_builtin "__builtin_sqrt" + (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default)) + (Tcons tdouble Tnil) tdouble cc_default)) :: + (___builtin_memcpy_aligned, + Gfun(External (EF_builtin "__builtin_memcpy_aligned" + (mksignature + (AST.Tlong :: AST.Tlong :: AST.Tlong :: AST.Tlong :: + nil) AST.Tvoid cc_default)) + (Tcons (tptr tvoid) + (Tcons (tptr tvoid) (Tcons tulong (Tcons tulong Tnil)))) tvoid + cc_default)) :: + (___builtin_sel, + Gfun(External (EF_builtin "__builtin_sel" + (mksignature (AST.Tint :: nil) AST.Tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) + (Tcons tbool Tnil) tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: + (___builtin_annot, + Gfun(External (EF_builtin "__builtin_annot" + (mksignature (AST.Tlong :: nil) AST.Tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) + (Tcons (tptr tschar) Tnil) tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: + (___builtin_annot_intval, + Gfun(External (EF_builtin "__builtin_annot_intval" + (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tint + cc_default)) (Tcons (tptr tschar) (Tcons tint Tnil)) + tint cc_default)) :: + (___builtin_membar, + Gfun(External (EF_builtin "__builtin_membar" + (mksignature nil AST.Tvoid cc_default)) Tnil tvoid + cc_default)) :: + (___builtin_va_start, + Gfun(External (EF_builtin "__builtin_va_start" + (mksignature (AST.Tlong :: nil) AST.Tvoid cc_default)) + (Tcons (tptr tvoid) Tnil) tvoid cc_default)) :: + (___builtin_va_arg, + Gfun(External (EF_builtin "__builtin_va_arg" + (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tvoid + cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil)) + tvoid cc_default)) :: + (___builtin_va_copy, + Gfun(External (EF_builtin "__builtin_va_copy" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tvoid + cc_default)) + (Tcons (tptr tvoid) (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) :: + (___builtin_va_end, + Gfun(External (EF_builtin "__builtin_va_end" + (mksignature (AST.Tlong :: nil) AST.Tvoid cc_default)) + (Tcons (tptr tvoid) Tnil) tvoid cc_default)) :: + (___builtin_unreachable, + Gfun(External (EF_builtin "__builtin_unreachable" + (mksignature nil AST.Tvoid cc_default)) Tnil tvoid + cc_default)) :: + (___builtin_expect, + Gfun(External (EF_builtin "__builtin_expect" + (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong + cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong + cc_default)) :: + (___builtin_fmax, + Gfun(External (EF_builtin "__builtin_fmax" + (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat + cc_default)) (Tcons tdouble (Tcons tdouble Tnil)) + tdouble cc_default)) :: + (___builtin_fmin, + Gfun(External (EF_builtin "__builtin_fmin" + (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat + cc_default)) (Tcons tdouble (Tcons tdouble Tnil)) + tdouble cc_default)) :: + (___builtin_fmadd, + Gfun(External (EF_builtin "__builtin_fmadd" + (mksignature + (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) + AST.Tfloat cc_default)) + (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble + cc_default)) :: + (___builtin_fmsub, + Gfun(External (EF_builtin "__builtin_fmsub" + (mksignature + (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) + AST.Tfloat cc_default)) + (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble + cc_default)) :: + (___builtin_fnmadd, + Gfun(External (EF_builtin "__builtin_fnmadd" + (mksignature + (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) + AST.Tfloat cc_default)) + (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble + cc_default)) :: + (___builtin_fnmsub, + Gfun(External (EF_builtin "__builtin_fnmsub" + (mksignature + (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) + AST.Tfloat cc_default)) + (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble + cc_default)) :: + (___builtin_read16_reversed, + Gfun(External (EF_builtin "__builtin_read16_reversed" + (mksignature (AST.Tlong :: nil) AST.Tint16unsigned + cc_default)) (Tcons (tptr tushort) Tnil) tushort + cc_default)) :: + (___builtin_read32_reversed, + Gfun(External (EF_builtin "__builtin_read32_reversed" + (mksignature (AST.Tlong :: nil) AST.Tint cc_default)) + (Tcons (tptr tuint) Tnil) tuint cc_default)) :: + (___builtin_write16_reversed, + Gfun(External (EF_builtin "__builtin_write16_reversed" + (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tvoid + cc_default)) (Tcons (tptr tushort) (Tcons tushort Tnil)) + tvoid cc_default)) :: + (___builtin_write32_reversed, + Gfun(External (EF_builtin "__builtin_write32_reversed" + (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tvoid + cc_default)) (Tcons (tptr tuint) (Tcons tuint Tnil)) + tvoid cc_default)) :: + (___builtin_debug, + Gfun(External (EF_external "__builtin_debug" + (mksignature (AST.Tint :: nil) AST.Tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) + (Tcons tint Tnil) tvoid + {|cc_vararg:=(Some 1); cc_unproto:=false; cc_structret:=false|})) :: + (_foo, Gfun(Internal f_foo)) :: (_main, Gfun(Internal f_main)) :: nil). + +Definition public_idents : list ident := +(_main :: _foo :: ___builtin_debug :: ___builtin_write32_reversed :: + ___builtin_write16_reversed :: ___builtin_read32_reversed :: + ___builtin_read16_reversed :: ___builtin_fnmsub :: ___builtin_fnmadd :: + ___builtin_fmsub :: ___builtin_fmadd :: ___builtin_fmin :: + ___builtin_fmax :: ___builtin_expect :: ___builtin_unreachable :: + ___builtin_va_end :: ___builtin_va_copy :: ___builtin_va_arg :: + ___builtin_va_start :: ___builtin_membar :: ___builtin_annot_intval :: + ___builtin_annot :: ___builtin_sel :: ___builtin_memcpy_aligned :: + ___builtin_sqrt :: ___builtin_fsqrt :: ___builtin_fabsf :: + ___builtin_fabs :: ___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz :: + ___builtin_clzll :: ___builtin_clzl :: ___builtin_clz :: + ___builtin_bswap16 :: ___builtin_bswap32 :: ___builtin_bswap :: + ___builtin_bswap64 :: ___builtin_ais_annot :: ___compcert_i64_umulh :: + ___compcert_i64_smulh :: ___compcert_i64_sar :: ___compcert_i64_shr :: + ___compcert_i64_shl :: ___compcert_i64_umod :: ___compcert_i64_smod :: + ___compcert_i64_udiv :: ___compcert_i64_sdiv :: ___compcert_i64_utof :: + ___compcert_i64_stof :: ___compcert_i64_utod :: ___compcert_i64_stod :: + ___compcert_i64_dtou :: ___compcert_i64_dtos :: ___compcert_va_composite :: + ___compcert_va_float64 :: ___compcert_va_int64 :: ___compcert_va_int32 :: + nil). + +Definition prog : Clight.program := + mkprogram composites global_definitions public_idents _main Logic.I. + + diff --git a/progs64/verif_alias.v b/progs64/verif_alias.v new file mode 100644 index 0000000000..bf4e89906b --- /dev/null +++ b/progs64/verif_alias.v @@ -0,0 +1,65 @@ +Require Import VST.floyd.proofauto. +Require Import VST.progs64.alias. + +Lemma field_compatible_void_long cs p : @field_compatible cs (tptr Tvoid) [] p = @field_compatible cs tlong [] p. +Proof. + eapply PropExtensionality.propositional_extensionality. + destruct p; + cbv [field_compatible align_compatible size_compatible]; + intuition idtac; + repeat match goal with + | H : align_compatible_rec _ _ _ |- _ => inversion H; clear H; subst end. + all : econstructor; eauto. +Qed. + +Lemma data_at__void_long cs sh p : @data_at_ cs sh (tptr Tvoid) p = @data_at_ cs sh tlong p. +Proof. rewrite 2data_at__memory_block, field_compatible_void_long; trivial. Qed. + +Lemma data_at_void_long_null cs sh p : @data_at cs sh (tptr Tvoid) (Vlong Int64.zero) p = @data_at cs sh tlong (Vlong Int64.zero) p. +Proof. + cbv [data_at field_at at_offset nested_field_type tptr]. + simpl data_at_rec. + unfold data_at_rec. + simpl rank_type. + simpl type_induction.type_func. + rewrite field_compatible_void_long; f_equal. + change (Tlong Signed noattr) with tlong. + rewrite mapsto_tuint_tptr_nullval. + reflexivity. +Qed. + + +#[export] Instance CompSpecs : compspecs. +Proof. make_compspecs prog. Defined. +Definition Vprog : varspecs. mk_varspecs prog. Defined. + +Definition foo_spec := DECLARE _foo WITH p : val + PRE [ tptr tlong, tptr (tptr Tvoid) ] PROP() PARAMS(p; p) SEP(data_at_ Tsh tlong p) + POST [ tlong ] PROP() RETURN(Vlong Int64.zero) SEP(data_at_ Tsh tlong p). + +Definition main_spec := DECLARE _main WITH gv : globals + PRE [] main_pre prog tt gv + POST [ tint ] PROP() RETURN (Vint Int.zero) SEP(has_ext tt). + +Definition Gprog : funspecs := ltac:(with_library prog [foo_spec; main_spec]). + +Lemma body_main : semax_body Vprog Gprog f_main main_spec. +Proof. start_function. forward_call. forward. entailer!. Qed. + +Lemma body_foo : semax_body Vprog Gprog f_foo foo_spec. +Proof. + start_function. + forward. + match goal with | |- context[data_at ?sh ?t ?Vs ?op] => sep_apply (data_at_data_at_ sh t Vs op) end. + erewrite <-data_at__void_long. + forward. + rewrite data_at_void_long_null. + forward. + forward. + entailer!. +Qed. + +Definition Espec := add_funspecs NullExtension.Espec (ext_link_prog prog) Gprog. +#[export] Existing Instance Espec. +Lemma prog_correct: semax_prog prog tt Vprog Gprog. +Proof. prove_semax_prog. semax_func_cons body_foo. semax_func_cons body_main. Qed. From 7e9c9663c5657f3b8f90bb5188ee787c9ca0ba46 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 25 Oct 2022 10:40:40 -0400 Subject: [PATCH 6/6] comment on soundness in progs*/alias.C --- progs/alias.c | 4 ++++ progs64/alias.c | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/progs/alias.c b/progs/alias.c index b3d2beabe2..5748b7de52 100644 --- a/progs/alias.c +++ b/progs/alias.c @@ -21,6 +21,10 @@ 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++). diff --git a/progs64/alias.c b/progs64/alias.c index 3895ba9816..a99f9f0c7e 100644 --- a/progs64/alias.c +++ b/progs64/alias.c @@ -21,6 +21,10 @@ 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++).