From 6a098e4215ac7c3cf2eb51bc1438db31a5d0f59d Mon Sep 17 00:00:00 2001 From: Andrew Appel Date: Wed, 15 Jan 2025 11:40:50 -0500 Subject: [PATCH] VSTlib compatibility with 'nans' branch of VCFloat --- lib/proof/spec_math.v | 24 ++++++++++------ lib/proof/spec_threads.v | 28 +++++++++++++++++- lib/proof/src/math_extern.c | 6 ++++ lib/proof/verif_SC_atomics.v | 56 +++++++++++++++++++++++------------- lib/proof/verif_locks.v | 5 ++++ lib/proof/verif_math.v | 19 +++--------- lib/test/testmath.c | 6 ++++ 7 files changed, 99 insertions(+), 45 deletions(-) diff --git a/lib/proof/spec_math.v b/lib/proof/spec_math.v index 2a14fd28ec..8ea1761ca2 100644 --- a/lib/proof/spec_math.v +++ b/lib/proof/spec_math.v @@ -212,7 +212,8 @@ simpl in H. rewrite andb_true_iff in H. destruct H as [H H']. unfold BSQRT, UNOP . -destruct (Binary.Bsqrt_correct (fprec t) (femax t) (fprec_gt_0 t) (fprec_lt_femax t) (sqrt_nan t) +destruct (Binary.Bsqrt_correct (fprec t) (femax t) (fprec_gt_0 t) (fprec_lt_femax t) + (sqrt_nan (fprec t) (femax t) (fprec_gt_one t)) BinarySingleNaN.mode_NE (float_of_ftype x)) as [? [??]]. (*rewrite <- FT2R_ftype_of_float in H0.*) @@ -311,7 +312,8 @@ split3; [ tauto | intro Hx; inv Hx | ]. rewrite ?FT2R_ftype_of_float in *. rewrite ?float_of_ftype_of_float in *. set (y := float_of_ftype x) in *. clearbody y. clear x. - pose proof (Binary.B2R_Babs (fprec t) (femax t) (FPCore.abs_nan t) + pose proof (Binary.B2R_Babs (fprec t) (femax t) + (FPCore.abs_nan (fprec t) (femax t) (fprec_gt_one t)) y). rewrite H1; clear H1. exists 0%R, 0%R. @@ -464,7 +466,8 @@ Lemma fma_ff_aux1: (fun x y z : ftype' t => ftype_of_float (Binary.Bfma (fprec t) (femax t) (fprec_gt_0 t) (fprec_lt_femax t) - (fma_nan t) BinarySingleNaN.mode_NE (float_of_ftype x) + (fma_nan (fprec t) (femax t) (fprec_gt_one t)) + BinarySingleNaN.mode_NE (float_of_ftype x) (float_of_ftype y) (float_of_ftype z))). Proof. intros. @@ -477,7 +480,8 @@ intros FIN. simpl. apply finite_bnds_e in H,H0,H1. rewrite is_finite_Binary in *. -pose proof (Binary.Bfma_correct (fprec t) (femax t) (fprec_gt_0 t) (fprec_lt_femax t) (fma_nan t) +pose proof (Binary.Bfma_correct (fprec t) (femax t) (fprec_gt_0 t) (fprec_lt_femax t) + (fma_nan (fprec t) (femax t) (fprec_gt_one t)) BinarySingleNaN.mode_NE (float_of_ftype x) (float_of_ftype y) (float_of_ftype z) H H0 H1). cbv zeta in H2. pose proof ( @@ -493,7 +497,8 @@ pose proof ( destruct H3. + destruct H2 as [? [? ?]]. -change (FMA_NAN.fma_nan_pl t) with (fma_nan t). +change (FMA_NAN.fma_nan_pl (fprec t) (femax t) (fprec_gt_one t)) with + (fma_nan (fprec t) (femax t) (fprec_gt_one t)). rewrite H2. rewrite !Rmult_1_l. split; auto. @@ -514,7 +519,7 @@ Lemma fma_ff_aux2: (fun x y z : ftype' t => ftype_of_float (Binary.Bfma (fprec t) (femax t) (fprec_gt_0 t) (fprec_lt_femax t) - (@fma_nan nans t STD) BinarySingleNaN.mode_NE (@float_of_ftype t STD x) + (@fma_nan _ (fprec t) (femax t) (fprec_gt_one t)) BinarySingleNaN.mode_NE (@float_of_ftype t STD x) (@float_of_ftype t STD y) (@float_of_ftype t STD z))). Proof. intros; hnf; intros. @@ -544,7 +549,7 @@ Qed. Definition fma_ff (t: type) `{STD: is_standard t} : floatfunc [ t;t;t ] t (fma_bnds t) (fun x y z => x*y+z)%R. apply (Build_floatfunc [t;t;t] t _ _ (fun x y z => ftype_of_float (Binary.Bfma (fprec t) (femax t) (fprec_gt_0 t) (fprec_lt_femax t) - (fma_nan t) BinarySingleNaN.mode_NE + (fma_nan (fprec t) (femax t) (fprec_gt_one t)) BinarySingleNaN.mode_NE (float_of_ftype x) (float_of_ftype y) (float_of_ftype z))) 1%N 1%N). apply fma_ff_aux1. @@ -583,7 +588,8 @@ Definition frexp_spec' (t: type) `{STD: is_standard t} := Definition bogus_nan t `(STD: is_standard t) := (* This is probably not the right NaN to use, wherever you see it used *) - FMA_NAN.quiet_nan t (FMA_NAN.default_nan t). + FMA_NAN.quiet_nan (fprec t) (femax t) (fprec_gt_one t) + (FMA_NAN.default_nan (fprec t)). Definition nextafter (t: type) `{STD: is_standard t} (x y: ftype t) : ftype t := match Binary.Bcompare (fprec t) (femax t) (float_of_ftype x) (float_of_ftype y) with @@ -835,7 +841,7 @@ assert (H0: Binary.is_finite _ _ (ff_func (sqrt_ff Tdouble) x) = true). { - unfold BSQRT, UNOP; simpl. destruct (Binary.Bsqrt_correct (fprec Tdouble) 1024 (fprec_gt_0 Tdouble) (fprec_lt_femax Tdouble) (fun _ : Binary.binary_float (fprec Tdouble) 1024 => - any_nan Tdouble) BinarySingleNaN.mode_NE + any_nan (fprec Tdouble) (femax Tdouble) (fprec_gt_one Tdouble)) BinarySingleNaN.mode_NE (Binary.B754_finite (fprec Tdouble) 1024 false m e e0)). apply H1. } diff --git a/lib/proof/spec_threads.v b/lib/proof/spec_threads.v index 1426542567..44676ba1ce 100644 --- a/lib/proof/spec_threads.v +++ b/lib/proof/spec_threads.v @@ -115,7 +115,33 @@ Proof. destruct x as [[[]] pre]; auto. Qed. -Definition spawned_funtype := Tfunction (tptr tvoid :: nil) tint cc_default. +(* The following hack is to achieve compatibility between CompCert <= 3.14 and CompCert >= 3.15 *) + +Local Fixpoint get_def [T] (al: list (ident * T)) (i: ident) : option T := + match al with + | nil => None + | (j,x)::r => if ident_eq i j then Some x else get_def r i + end. +Local Definition get_extfun (i: ident) := + match get_def global_definitions i with + | Some (Gfun (External _ t _ _)) => Some t + | _ => None + end. + +Local Definition Tcons := + ltac:(let x := constr:(get_extfun _pthread_exit) in + let x := eval compute in x in + match x with Some (?y _ ?z) => exact y end). + + +Local Definition Tnil := + ltac:(let x := constr:(get_extfun _pthread_exit) in + let x := eval compute in x in + match x with Some (?y _ ?z) => exact z end). + +(* END of hack *) + +Definition spawned_funtype := Tfunction (Tcons (tptr tvoid) Tnil) tint cc_default. Definition spawn_spec := mk_funspec ((tptr spawned_funtype) :: (tptr tvoid) :: nil, tvoid) diff --git a/lib/proof/src/math_extern.c b/lib/proof/src/math_extern.c index 3b12d5a13c..ec76985e78 100644 --- a/lib/proof/src/math_extern.c +++ b/lib/proof/src/math_extern.c @@ -1,3 +1,9 @@ +#ifdef COMPCERT +/* still Starting with CompCert 3.15 (and VST 2.15), don't need this hack + any more, but still here for VSTlib compatibility with older versions + of CompCert/VST */ +typedef float _Float16; /* _Float16 is a MacOS thing that CompCert doesn't support */ +#endif #include /* Note regard 'long double': diff --git a/lib/proof/verif_SC_atomics.v b/lib/proof/verif_SC_atomics.v index 66684c8a86..4f5d544553 100644 --- a/lib/proof/verif_SC_atomics.v +++ b/lib/proof/verif_SC_atomics.v @@ -9,62 +9,78 @@ Definition Vprog : varspecs. mk_varspecs prog. Defined. #[export] Declare Instance M: AtomicsAPD. +Local Fixpoint get_def [T] (al: list (ident * T)) (i: ident) : option T := + match al with + | nil => None + | (j,x)::r => if ident_eq i j then Some x else get_def r i + end. + +Local Definition get_extfun (i: ident) : external_function := + match get_def SC_atomics_extern.global_definitions i with + | Some (Gfun (External x _ _ _)) => x + | _ => EF_annot 1%positive "error: extfun not found" nil + end. + + Parameter body_make_atomic: forall {Espec: OracleKind} , - VST.floyd.library.body_lemma_of_funspec - (EF_external "make_atomic" (mksignature (Xint :: nil) Xptr cc_default)) + VST.floyd.library.body_lemma_of_funspec (get_extfun _make_atomic) +(* (EF_external "make_atomic" (mksignature (Xint :: nil) Xptr cc_default))*) make_atomic_spec. Parameter body_make_atomic_ptr: forall {Espec: OracleKind} , - VST.floyd.library.body_lemma_of_funspec - (EF_external "make_atomic_ptr" - (mksignature (Xptr :: nil) Xptr cc_default)) + VST.floyd.library.body_lemma_of_funspec (get_extfun _make_atomic_ptr) +(* (EF_external "make_atomic_ptr" + (mksignature (Xptr :: nil) Xptr cc_default))*) make_atomic_ptr_spec. Parameter body_free_atomic: forall {Espec: OracleKind} , - VST.floyd.library.body_lemma_of_funspec - (EF_external "free_atomic" - (mksignature (Xptr :: nil) Xvoid cc_default)) + VST.floyd.library.body_lemma_of_funspec (get_extfun _free_atomic) +(* (EF_external "free_atomic" + (mksignature (Xptr :: nil) Xvoid cc_default))*) free_atomic_int_spec. Parameter body_free_atomic_ptr: forall {Espec: OracleKind} , - VST.floyd.library.body_lemma_of_funspec - (EF_external "free_atomic_ptr" - (mksignature (Xptr :: nil) Xvoid cc_default)) + VST.floyd.library.body_lemma_of_funspec (get_extfun _free_atomic_ptr) +(* (EF_external "free_atomic_ptr" + (mksignature (Xptr :: nil) Xvoid cc_default))*) free_atomic_ptr_spec. Parameter body_atom_load: forall {Espec: OracleKind} , - VST.floyd.library.body_lemma_of_funspec - (EF_external "atom_load" - (mksignature (Xptr :: nil) Xint cc_default)) + VST.floyd.library.body_lemma_of_funspec (get_extfun _atom_load) +(* (EF_external "atom_load" + (mksignature (Xptr :: nil) Xint cc_default))*) atomic_load_spec. Parameter body_atom_store: forall {Espec: OracleKind} , - VST.floyd.library.body_lemma_of_funspec - (EF_external "atom_store" + VST.floyd.library.body_lemma_of_funspec (get_extfun _atom_store) +(* (EF_external "atom_store" (mksignature (Xptr :: Xint :: nil) Xvoid cc_default)) +*) atomic_store_spec. Parameter body_atom_CAS: forall {Espec: OracleKind} , - VST.floyd.library.body_lemma_of_funspec - (EF_external "atom_CAS" + VST.floyd.library.body_lemma_of_funspec (get_extfun _atom_CAS) +(* (EF_external "atom_CAS" (mksignature (Xptr :: Xptr :: Xint :: nil) Xint cc_default)) +*) atomic_CAS_spec. Parameter body_atom_exchange: forall {Espec: OracleKind} , - VST.floyd.library.body_lemma_of_funspec - (EF_external "atom_exchange" + VST.floyd.library.body_lemma_of_funspec (get_extfun _atom_exchange) +(* (EF_external "atom_exchange" (mksignature (Xptr :: Xint :: nil) Xint cc_default)) +*) atomic_exchange_spec. Definition SC_atomics_placeholder_spec := diff --git a/lib/proof/verif_locks.v b/lib/proof/verif_locks.v index bfdc4dce53..aafdbc876e 100755 --- a/lib/proof/verif_locks.v +++ b/lib/proof/verif_locks.v @@ -210,6 +210,11 @@ Opaque inv_for_lock. - Intros r. if_tac; forward_if; try discriminate; try contradiction. + forward. simpl spec_locks.lock_inv; entailer!. + forward. simpl spec_locks.lock_inv; entailer!. +Unshelve. (* This part is for compatibility with VST < 2.15 *) +all: apply Build_change_composite_env with (coeq := Maps.PTree.empty bool); + [intros; inv H1 | + intros; unfold cenv_cs; simpl; rewrite !Maps.PTree.gempty; + split; intros [? ?]; discriminate]. Qed. #[global] Opaque M. diff --git a/lib/proof/verif_math.v b/lib/proof/verif_math.v index 22c3edbe78..19825b6bed 100644 --- a/lib/proof/verif_math.v +++ b/lib/proof/verif_math.v @@ -62,20 +62,8 @@ assert (match ret with | Some v => tc_val t v | None => False end); [ | destruct t; try contradiction; auto]. -assert (match rettype_of_type t with - | Xvoid => - mkEnviron gx (Map.empty (block * type)) - (Map.empty val) - | _ => - match ret with - | Some v' => - mkEnviron gx (Map.empty (block * type)) - (Map.set 1 v' (Map.empty val)) - | None => - mkEnviron gx (Map.empty (block * type)) - (Map.empty val) - end - end = match ret with +match type of H with context [te_of ?A] => + assert (A = match ret with | Some v' => mkEnviron gx (Map.empty (block * type)) (Map.set 1 v' (Map.empty val)) @@ -83,7 +71,8 @@ assert (match rettype_of_type t with mkEnviron gx (Map.empty (block * type)) (Map.empty val) end) - by (destruct (rettype_of_type t); auto; discriminate H). + by (destruct (rettype_of_type t); auto; discriminate H) + end. rewrite H1 in *; clear H1. destruct ret; [ | discriminate H]. simpl in H. diff --git a/lib/test/testmath.c b/lib/test/testmath.c index a6ba824916..1022dd5b20 100644 --- a/lib/test/testmath.c +++ b/lib/test/testmath.c @@ -1,3 +1,9 @@ +#ifdef COMPCERT +/* still Starting with CompCert 3.15 (and VST 2.15), don't need this hack + any more, but still here for VSTlib compatibility with older versions + of CompCert/VST */ +typedef float _Float16; /* _Float16 is a MacOS thing that CompCert doesn't support */ +#endif #include double f(double t) {