Adapt VSTlib to 'Nans' branch of VCFloat

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.
 }  

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)

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 <math.h>
 
 /* Note regard 'long double':

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 :=

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.

lib/proof/verif_math.v

@@ -62,28 +62,17 @@ 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))
                    | None =>
                        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.

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 <math.h>
 
 double f(double t) {