From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 08:54:56 +0000 Subject: Merge of "newspilling" branch: - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/C2C.ml | 18 ++- cfrontend/Cexec.v | 19 +-- cfrontend/Clight.v | 6 +- cfrontend/Cminorgen.v | 2 + cfrontend/Cminorgenproof.v | 24 +++- cfrontend/Cop.v | 274 ++++++++++++++++++++++++++++++------------ cfrontend/Csharpminor.v | 4 +- cfrontend/Cshmgen.v | 110 +++++++++++------ cfrontend/Cshmgenproof.v | 131 +++++++++++--------- cfrontend/Ctypes.v | 21 ++-- cfrontend/Initializers.v | 4 +- cfrontend/Initializersproof.v | 21 ++-- cfrontend/PrintClight.ml | 4 + cfrontend/PrintCsyntax.ml | 2 + cfrontend/SimplExpr.v | 3 + cfrontend/SimplExprspec.v | 4 + cfrontend/SimplLocals.v | 5 +- cfrontend/SimplLocalsproof.v | 57 ++++----- 18 files changed, 460 insertions(+), 249 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index d389d0a..e7d8337 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -441,7 +441,13 @@ let z_of_str hex str fst = let convertFloat f kind = let mant = z_of_str f.C.hex (f.C.intPart ^ f.C.fracPart) 0 in match mant with - | Z.Z0 -> Float.zero + | Z.Z0 -> + begin match kind with + | FFloat -> + Vsingle (Float.to_single Float.zero) + | FDouble | FLongDouble -> + Vfloat Float.zero + end | Z.Zpos mant -> let sgExp = match f.C.exp.[0] with '+' | '-' -> true | _ -> false in @@ -454,10 +460,10 @@ let convertFloat f kind = let base = P.of_int (if f.C.hex then 2 else 10) in begin match kind with - | FFloat -> - Float.build_from_parsed32 base mant exp - | FDouble | FLongDouble -> - Float.build_from_parsed64 base mant exp + | FFloat -> + Vsingle (Float32.from_parsed base mant exp) + | FDouble | FLongDouble -> + Vfloat (Float.from_parsed base mant exp) end | Z.Zneg _ -> assert false @@ -482,7 +488,7 @@ let rec convertExpr env e = | C.EConst(C.CFloat(f, k)) -> if k = C.FLongDouble && not !Clflags.option_flongdouble then unsupported "'long double' floating-point literal"; - Eval(Vfloat(convertFloat f k), ty) + Eval(convertFloat f k, ty) | C.EConst(C.CStr s) -> let ty = typeStringLiteral s in Evalof(Evar(name_for_string_literal env s, ty), ty) diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index b41902c..eea1997 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -104,7 +104,7 @@ Definition eventval_of_val (v: val) (t: typ) : option eventval := match v, t with | Vint i, AST.Tint => Some (EVint i) | Vfloat f, AST.Tfloat => Some (EVfloat f) - | Vfloat f, AST.Tsingle => if Float.is_single_dec f then Some (EVfloatsingle f) else None + | Vsingle f, AST.Tsingle => Some (EVsingle f) | Vlong n, AST.Tlong => Some (EVlong n) | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol ge b; Some (EVptr_global id ofs) | _, _ => None @@ -124,7 +124,7 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val := match ev, t with | EVint i, AST.Tint => Some (Vint i) | EVfloat f, AST.Tfloat => Some (Vfloat f) - | EVfloatsingle f, AST.Tsingle => if Float.is_single_dec f then Some (Vfloat f) else None + | EVsingle f, AST.Tsingle => Some (Vsingle f) | EVlong n, AST.Tlong => Some (Vlong n) | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol ge id; Some (Vptr b ofs) | _, _ => None @@ -133,11 +133,7 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val := Lemma eventval_of_val_sound: forall v t ev, eventval_of_val v t = Some ev -> eventval_match ge ev t v. Proof. - intros. destruct v; destruct t; simpl in H; inv H. - constructor. - constructor. - constructor. - destruct (Float.is_single_dec f); inv H1. constructor; auto. + intros. destruct v; destruct t; simpl in H; inv H; try constructor. destruct (Genv.invert_symbol ge b) as [id|] eqn:?; inv H1. constructor. apply Genv.invert_find_symbol; auto. Qed. @@ -146,7 +142,6 @@ Lemma eventval_of_val_complete: forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev. Proof. induction 1; simpl; auto. - rewrite pred_dec_true; auto. rewrite (Genv.find_invert_symbol _ _ H). auto. Qed. @@ -170,11 +165,7 @@ Qed. Lemma val_of_eventval_sound: forall ev t v, val_of_eventval ev t = Some v -> eventval_match ge ev t v. Proof. - intros. destruct ev; destruct t; simpl in H; inv H. - constructor. - constructor. - constructor. - destruct (Float.is_single_dec f); inv H1. constructor; auto. + intros. destruct ev; destruct t; simpl in H; inv H; try constructor. destruct (Genv.find_symbol ge i) as [b|] eqn:?; inv H1. constructor. auto. Qed. @@ -182,7 +173,7 @@ Qed. Lemma val_of_eventval_complete: forall ev t v, eventval_match ge ev t v -> val_of_eventval ev t = Some v. Proof. - induction 1; simpl; auto. rewrite pred_dec_true; auto. rewrite H; auto. + induction 1; simpl; auto. rewrite H; auto. Qed. (** Volatile memory accesses. *) diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index f2ba240..d9fb650 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -47,7 +47,8 @@ Require Import Cop. Inductive expr : Type := | Econst_int: int -> type -> expr (**r integer literal *) - | Econst_float: float -> type -> expr (**r float literal *) + | Econst_float: float -> type -> expr (**r double float literal *) + | Econst_single: float32 -> type -> expr (**r single float literal *) | Econst_long: int64 -> type -> expr (**r long integer literal *) | Evar: ident -> type -> expr (**r variable *) | Etempvar: ident -> type -> expr (**r temporary variable *) @@ -69,6 +70,7 @@ Definition typeof (e: expr) : type := match e with | Econst_int _ ty => ty | Econst_float _ ty => ty + | Econst_single _ ty => ty | Econst_long _ ty => ty | Evar _ ty => ty | Etempvar _ ty => ty @@ -352,6 +354,8 @@ Inductive eval_expr: expr -> val -> Prop := eval_expr (Econst_int i ty) (Vint i) | eval_Econst_float: forall f ty, eval_expr (Econst_float f ty) (Vfloat f) + | eval_Econst_single: forall f ty, + eval_expr (Econst_single f ty) (Vsingle f) | eval_Econst_long: forall i ty, eval_expr (Econst_long i ty) (Vlong i) | eval_Etempvar: forall id ty v, diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 8ecf498..ae6ec56 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -70,6 +70,8 @@ Definition transl_constant (cst: Csharpminor.constant): constant := Ointconst n | Csharpminor.Ofloatconst n => Ofloatconst n + | Csharpminor.Osingleconst n => + Osingleconst n | Csharpminor.Olongconst n => Olongconst n end. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index dba445d..3bf790c 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1299,8 +1299,15 @@ Proof. inv H; inv H0; simpl; TrivialExists. inv H; inv H0; simpl; TrivialExists. inv H; inv H0; simpl; TrivialExists. - inv H0; simpl in H; inv H. simpl. destruct (Float.intoffloat f0); simpl in *; inv H1. TrivialExists. - inv H0; simpl in H; inv H. simpl. destruct (Float.intuoffloat f0); simpl in *; inv H1. TrivialExists. + inv H; inv H0; simpl; TrivialExists. + inv H; inv H0; simpl; TrivialExists. + inv H; inv H0; simpl; TrivialExists. + inv H0; simpl in H; inv H. simpl. destruct (Float.to_int f0); simpl in *; inv H1. TrivialExists. + inv H0; simpl in H; inv H. simpl. destruct (Float.to_intu f0); simpl in *; inv H1. TrivialExists. + inv H0; simpl in H; inv H. simpl. TrivialExists. + inv H0; simpl in H; inv H. simpl. TrivialExists. + inv H0; simpl in H; inv H. simpl. destruct (Float32.to_int f0); simpl in *; inv H1. TrivialExists. + inv H0; simpl in H; inv H. simpl. destruct (Float32.to_intu f0); simpl in *; inv H1. TrivialExists. inv H0; simpl in H; inv H. simpl. TrivialExists. inv H0; simpl in H; inv H. simpl. TrivialExists. inv H; inv H0; simpl; TrivialExists. @@ -1308,10 +1315,12 @@ Proof. inv H; inv H0; simpl; TrivialExists. inv H; inv H0; simpl; TrivialExists. inv H; inv H0; simpl; TrivialExists. - inv H0; simpl in H; inv H. simpl. destruct (Float.longoffloat f0); simpl in *; inv H1. TrivialExists. - inv H0; simpl in H; inv H. simpl. destruct (Float.longuoffloat f0); simpl in *; inv H1. TrivialExists. + inv H0; simpl in H; inv H. simpl. destruct (Float.to_long f0); simpl in *; inv H1. TrivialExists. + inv H0; simpl in H; inv H. simpl. destruct (Float.to_longu f0); simpl in *; inv H1. TrivialExists. inv H0; simpl in H; inv H. simpl. TrivialExists. inv H0; simpl in H; inv H. simpl. TrivialExists. + inv H0; simpl in H; inv H. simpl. destruct (Float32.to_long f0); simpl in *; inv H1. TrivialExists. + inv H0; simpl in H; inv H. simpl. destruct (Float32.to_longu f0); simpl in *; inv H1. TrivialExists. inv H0; simpl in H; inv H. simpl. TrivialExists. inv H0; simpl in H; inv H. simpl. TrivialExists. Qed. @@ -1361,6 +1370,10 @@ Proof. inv H; inv H0; inv H1; TrivialExists. inv H; inv H0; inv H1; TrivialExists. inv H; inv H0; inv H1; TrivialExists. + inv H; inv H0; inv H1; TrivialExists. + inv H; inv H0; inv H1; TrivialExists. + inv H; inv H0; inv H1; TrivialExists. + inv H; inv H0; inv H1; TrivialExists. inv H0; try discriminate; inv H1; try discriminate. simpl in *. destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H; TrivialExists. @@ -1392,6 +1405,8 @@ Proof. simpl; auto. (* cmpf *) inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. +(* cmpfs *) + inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. (* cmpl *) unfold Val.cmpl in *. inv H0; inv H1; simpl in H; inv H. econstructor; split. simpl; eauto. apply val_inject_val_of_bool. @@ -1470,6 +1485,7 @@ Proof. destruct cst; simpl; intros; inv H. exists (Vint i); auto. exists (Vfloat f0); auto. + exists (Vsingle f0); auto. exists (Vlong i); auto. Qed. diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 83fe772..ff43cbd 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -74,17 +74,25 @@ Inductive incr_or_decr : Type := Incr | Decr. Inductive classify_cast_cases : Type := | cast_case_neutral (**r int|pointer -> int32|pointer *) | cast_case_i2i (sz2:intsize) (si2:signedness) (**r int -> int *) - | cast_case_f2f (sz2:floatsize) (**r float -> float *) - | cast_case_i2f (si1:signedness) (sz2:floatsize) (**r int -> float *) - | cast_case_f2i (sz2:intsize) (si2:signedness) (**r float -> int *) + | cast_case_f2f (**r double -> double *) + | cast_case_s2s (**r single -> single *) + | cast_case_f2s (**r double -> single *) + | cast_case_s2f (**r single -> double *) + | cast_case_i2f (si1: signedness) (**r int -> double *) + | cast_case_i2s (si1: signedness) (**r int -> single *) + | cast_case_f2i (sz2:intsize) (si2:signedness) (**r double -> int *) + | cast_case_s2i (sz2:intsize) (si2:signedness) (**r single -> int *) | cast_case_l2l (**r long -> long *) | cast_case_i2l (si1: signedness) (**r int -> long *) | cast_case_l2i (sz2: intsize) (si2: signedness) (**r long -> int *) - | cast_case_l2f (si1: signedness) (sz2: floatsize) (**r long -> float *) - | cast_case_f2l (si2: signedness) (**r float -> long *) - | cast_case_f2bool (**r float -> bool *) - | cast_case_l2bool (**r long -> bool *) - | cast_case_p2bool (**r pointer -> bool *) + | cast_case_l2f (si1: signedness) (**r long -> double *) + | cast_case_l2s (si1: signedness) (**r long -> single *) + | cast_case_f2l (si2:signedness) (**r double -> long *) + | cast_case_s2l (si2:signedness) (**r single -> long *) + | cast_case_f2bool (**r double -> bool *) + | cast_case_s2bool (**r single -> bool *) + | cast_case_l2bool (**r long -> bool *) + | cast_case_p2bool (**r pointer -> bool *) | cast_case_struct (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r struct -> struct *) | cast_case_union (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r union -> union *) | cast_case_void (**r any -> void *) @@ -93,19 +101,27 @@ Inductive classify_cast_cases : Type := Definition classify_cast (tfrom tto: type) : classify_cast_cases := match tto, tfrom with | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral - | Tint IBool _ _, Tfloat _ _ => cast_case_f2bool + | Tint IBool _ _, Tfloat F64 _ => cast_case_f2bool + | Tint IBool _ _, Tfloat F32 _ => cast_case_s2bool | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2 - | Tint sz2 si2 _, Tfloat sz1 _ => cast_case_f2i sz2 si2 - | Tfloat sz2 _, Tfloat sz1 _ => cast_case_f2f sz2 - | Tfloat sz2 _, Tint sz1 si1 _ => cast_case_i2f si1 sz2 + | Tint sz2 si2 _, Tfloat F64 _ => cast_case_f2i sz2 si2 + | Tint sz2 si2 _, Tfloat F32 _ => cast_case_s2i sz2 si2 + | Tfloat F64 _, Tfloat F64 _ => cast_case_f2f + | Tfloat F32 _, Tfloat F32 _ => cast_case_s2s + | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f + | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s + | Tfloat F64 _, Tint sz1 si1 _ => cast_case_i2f si1 + | Tfloat F32 _, Tint sz1 si1 _ => cast_case_i2s si1 | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral | Tlong _ _, Tlong _ _ => cast_case_l2l | Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1 | Tint IBool _ _, Tlong _ _ => cast_case_l2bool | Tint sz2 si2 _, Tlong _ _ => cast_case_l2i sz2 si2 - | Tlong si2 _, Tfloat sz1 _ => cast_case_f2l si2 - | Tfloat sz2 _, Tlong si1 _ => cast_case_l2f si1 sz2 + | Tlong si2 _, Tfloat F64 _ => cast_case_f2l si2 + | Tlong si2 _, Tfloat F32 _ => cast_case_s2l si2 + | Tfloat F64 _, Tlong si1 _ => cast_case_l2f si1 + | Tfloat F32 _, Tlong si1 _ => cast_case_l2s si1 | (Tpointer _ _ | Tcomp_ptr _ _), Tlong _ _ => cast_case_l2i I32 Unsigned | Tlong si2 _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2 | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2 @@ -128,24 +144,28 @@ Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int := | IBool, _ => if Int.eq i Int.zero then Int.zero else Int.one end. -Definition cast_int_float (si: signedness) (sz: floatsize) (i: int) : float := - match si, sz with - | Signed, F64 => Float.floatofint i - | Unsigned, F64 => Float.floatofintu i - | Signed, F32 => Float.singleofint i - | Unsigned, F32 => Float.singleofintu i +Definition cast_int_float (si: signedness) (i: int) : float := + match si with + | Signed => Float.of_int i + | Unsigned => Float.of_intu i end. Definition cast_float_int (si : signedness) (f: float) : option int := match si with - | Signed => Float.intoffloat f - | Unsigned => Float.intuoffloat f + | Signed => Float.to_int f + | Unsigned => Float.to_intu f end. -Definition cast_float_float (sz: floatsize) (f: float) : float := - match sz with - | F32 => Float.singleoffloat f - | F64 => f +Definition cast_int_single (si: signedness) (i: int) : float32 := + match si with + | Signed => Float32.of_int i + | Unsigned => Float32.of_intu i + end. + +Definition cast_single_int (si : signedness) (f: float32) : option int := + match si with + | Signed => Float32.to_int f + | Unsigned => Float32.to_intu f end. Definition cast_int_long (si: signedness) (i: int) : int64 := @@ -154,18 +174,28 @@ Definition cast_int_long (si: signedness) (i: int) : int64 := | Unsigned => Int64.repr (Int.unsigned i) end. -Definition cast_long_float (si: signedness) (sz: floatsize) (i: int64) : float := - match si, sz with - | Signed, F64 => Float.floatoflong i - | Unsigned, F64 => Float.floatoflongu i - | Signed, F32 => Float.singleoflong i - | Unsigned, F32 => Float.singleoflongu i +Definition cast_long_float (si: signedness) (i: int64) : float := + match si with + | Signed => Float.of_long i + | Unsigned => Float.of_longu i + end. + +Definition cast_long_single (si: signedness) (i: int64) : float32 := + match si with + | Signed => Float32.of_long i + | Unsigned => Float32.of_longu i end. Definition cast_float_long (si : signedness) (f: float) : option int64 := match si with - | Signed => Float.longoffloat f - | Unsigned => Float.longuoffloat f + | Signed => Float.to_long f + | Unsigned => Float.to_longu f + end. + +Definition cast_single_long (si : signedness) (f: float32) : option int64 := + match si with + | Signed => Float32.to_long f + | Unsigned => Float32.to_longu f end. Definition sem_cast (v: val) (t1 t2: type) : option val := @@ -180,14 +210,34 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := | Vint i => Some (Vint (cast_int_int sz2 si2 i)) | _ => None end - | cast_case_f2f sz2 => + | cast_case_f2f => + match v with + | Vfloat f => Some (Vfloat f) + | _ => None + end + | cast_case_s2s => + match v with + | Vsingle f => Some (Vsingle f) + | _ => None + end + | cast_case_s2f => match v with - | Vfloat f => Some (Vfloat (cast_float_float sz2 f)) + | Vsingle f => Some (Vfloat (Float.of_single f)) | _ => None end - | cast_case_i2f si1 sz2 => + | cast_case_f2s => match v with - | Vint i => Some (Vfloat (cast_int_float si1 sz2 i)) + | Vfloat f => Some (Vsingle (Float.to_single f)) + | _ => None + end + | cast_case_i2f si1 => + match v with + | Vint i => Some (Vfloat (cast_int_float si1 i)) + | _ => None + end + | cast_case_i2s si1 => + match v with + | Vint i => Some (Vsingle (cast_int_single si1 i)) | _ => None end | cast_case_f2i sz2 si2 => @@ -199,12 +249,27 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := end | _ => None end + | cast_case_s2i sz2 si2 => + match v with + | Vsingle f => + match cast_single_int si2 f with + | Some i => Some (Vint (cast_int_int sz2 si2 i)) + | None => None + end + | _ => None + end | cast_case_f2bool => match v with | Vfloat f => Some(Vint(if Float.cmp Ceq f Float.zero then Int.zero else Int.one)) | _ => None end + | cast_case_s2bool => + match v with + | Vsingle f => + Some(Vint(if Float32.cmp Ceq f Float32.zero then Int.zero else Int.one)) + | _ => None + end | cast_case_p2bool => match v with | Vint i => Some (Vint (cast_int_int IBool Signed i)) @@ -232,9 +297,14 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := Some(Vint(if Int64.eq n Int64.zero then Int.zero else Int.one)) | _ => None end - | cast_case_l2f si1 sz2 => + | cast_case_l2f si1 => + match v with + | Vlong i => Some (Vfloat (cast_long_float si1 i)) + | _ => None + end + | cast_case_l2s si1 => match v with - | Vlong i => Some (Vfloat (cast_long_float si1 sz2 i)) + | Vlong i => Some (Vsingle (cast_long_single si1 i)) | _ => None end | cast_case_f2l si2 => @@ -246,6 +316,15 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := end | _ => None end + | cast_case_s2l si2 => + match v with + | Vsingle f => + match cast_single_long si2 f with + | Some i => Some (Vlong i) + | None => None + end + | _ => None + end | cast_case_struct id1 fld1 id2 fld2 => match v with | Vptr b ofs => @@ -271,7 +350,8 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := Inductive classify_bool_cases : Type := | bool_case_i (**r integer *) - | bool_case_f (**r float *) + | bool_case_f (**r double float *) + | bool_case_s (**r single float *) | bool_case_p (**r pointer *) | bool_case_l (**r long *) | bool_default. @@ -280,7 +360,8 @@ Definition classify_bool (ty: type) : classify_bool_cases := match typeconv ty with | Tint _ _ _ => bool_case_i | Tpointer _ _ | Tcomp_ptr _ _ => bool_case_p - | Tfloat _ _ => bool_case_f + | Tfloat F64 _ => bool_case_f + | Tfloat F32 _ => bool_case_s | Tlong _ _ => bool_case_l | _ => bool_default end. @@ -302,6 +383,11 @@ Definition bool_val (v: val) (t: type) : option bool := | Vfloat f => Some (negb (Float.cmp Ceq f Float.zero)) | _ => None end + | bool_case_s => + match v with + | Vsingle f => Some (negb (Float32.cmp Ceq f Float32.zero)) + | _ => None + end | bool_case_p => match v with | Vint n => Some (negb (Int.eq n Int.zero)) @@ -333,6 +419,11 @@ Definition sem_notbool (v: val) (ty: type) : option val := | Vfloat f => Some (Val.of_bool (Float.cmp Ceq f Float.zero)) | _ => None end + | bool_case_s => + match v with + | Vsingle f => Some (Val.of_bool (Float32.cmp Ceq f Float32.zero)) + | _ => None + end | bool_case_p => match v with | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) @@ -351,7 +442,8 @@ Definition sem_notbool (v: val) (ty: type) : option val := Inductive classify_neg_cases : Type := | neg_case_i(s: signedness) (**r int *) - | neg_case_f(sz: floatsize) (**r float *) + | neg_case_f (**r double float *) + | neg_case_s (**r single float *) | neg_case_l(s: signedness) (**r long *) | neg_default. @@ -359,7 +451,8 @@ Definition classify_neg (ty: type) : classify_neg_cases := match ty with | Tint I32 Unsigned _ => neg_case_i Unsigned | Tint _ _ _ => neg_case_i Signed - | Tfloat sz _ => neg_case_f sz + | Tfloat F64 _ => neg_case_f + | Tfloat F32 _ => neg_case_s | Tlong si _ => neg_case_l si | _ => neg_default end. @@ -371,11 +464,16 @@ Definition sem_neg (v: val) (ty: type) : option val := | Vint n => Some (Vint (Int.neg n)) | _ => None end - | neg_case_f sz => + | neg_case_f => match v with | Vfloat f => Some (Vfloat (Float.neg f)) | _ => None end + | neg_case_s => + match v with + | Vsingle f => Some (Vsingle (Float32.neg f)) + | _ => None + end | neg_case_l sg => match v with | Vlong n => Some (Vlong (Int64.neg n)) @@ -388,17 +486,22 @@ Definition sem_absfloat (v: val) (ty: type) : option val := match classify_neg ty with | neg_case_i sg => match v with - | Vint n => Some (Vfloat (Float.abs (cast_int_float sg F64 n))) + | Vint n => Some (Vfloat (Float.abs (cast_int_float sg n))) | _ => None end - | neg_case_f sz => + | neg_case_f => match v with | Vfloat f => Some (Vfloat (Float.abs f)) | _ => None end + | neg_case_s => + match v with + | Vsingle f => Some (Vfloat (Float.abs (Float.of_single f))) + | _ => None + end | neg_case_l sg => match v with - | Vlong n => Some (Vfloat (Float.abs (cast_long_float sg F64 n))) + | Vlong n => Some (Vfloat (Float.abs (cast_long_float sg n))) | _ => None end | neg_default => None @@ -446,7 +549,8 @@ Definition sem_notint (v: val) (ty: type): option val := Inductive binarith_cases: Type := | bin_case_i (s: signedness) (**r at int type *) | bin_case_l (s: signedness) (**r at long int type *) - | bin_case_f (sz: floatsize) (**r at float type *) + | bin_case_f (**r at double float type *) + | bin_case_s (**r at single float type *) | bin_default. (**r error *) Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases := @@ -458,31 +562,24 @@ Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases := | Tlong _ _, Tlong _ _ => bin_case_l Unsigned | Tlong sg _, Tint _ _ _ => bin_case_l sg | Tint _ _ _, Tlong sg _ => bin_case_l sg - | Tfloat F32 _, Tfloat F32 _ => bin_case_f F32 - | Tfloat _ _, Tfloat _ _ => bin_case_f F64 - | Tfloat sz _, (Tint _ _ _ | Tlong _ _) => bin_case_f sz - | (Tint _ _ _ | Tlong _ _), Tfloat sz _ => bin_case_f sz + | Tfloat F32 _, Tfloat F32 _ => bin_case_s + | Tfloat _ _, Tfloat _ _ => bin_case_f + | Tfloat F64 _, (Tint _ _ _ | Tlong _ _) => bin_case_f + | (Tint _ _ _ | Tlong _ _), Tfloat F64 _ => bin_case_f + | Tfloat F32 _, (Tint _ _ _ | Tlong _ _) => bin_case_s + | (Tint _ _ _ | Tlong _ _), Tfloat F32 _ => bin_case_s | _, _ => bin_default end. -(** The static type of the result. *) - -Definition binarith_result_type (c: binarith_cases) : option type := - match c with - | bin_case_i sg => Some(Tint I32 sg noattr) - | bin_case_l sg => Some(Tlong sg noattr) - | bin_case_f sz => Some(Tfloat sz noattr) - | bin_default => None - end. - -(** The type at which the computation is done. Both arguments are - converted to this type before the actual computation. *) +(** The static type of the result. Both arguments are converted to this type + before the actual computation. *) Definition binarith_type (c: binarith_cases) : type := match c with | bin_case_i sg => Tint I32 sg noattr | bin_case_l sg => Tlong sg noattr - | bin_case_f sz => Tfloat F64 noattr + | bin_case_f => Tfloat F64 noattr + | bin_case_s => Tfloat F32 noattr | bin_default => Tvoid end. @@ -490,6 +587,7 @@ Definition sem_binarith (sem_int: signedness -> int -> int -> option val) (sem_long: signedness -> int64 -> int64 -> option val) (sem_float: float -> float -> option val) + (sem_single: float32 -> float32 -> option val) (v1: val) (t1: type) (v2: val) (t2: type) : option val := let c := classify_binarith t1 t2 in let t := binarith_type c in @@ -505,11 +603,16 @@ Definition sem_binarith | Vint n1, Vint n2 => sem_int sg n1 n2 | _, _ => None end - | bin_case_f sz => + | bin_case_f => match v1', v2' with | Vfloat n1, Vfloat n2 => sem_float n1 n2 | _, _ => None end + | bin_case_s => + match v1', v2' with + | Vsingle n1, Vsingle n2 => sem_single n1 n2 + | _, _ => None + end | bin_case_l sg => match v1', v2' with | Vlong n1, Vlong n2 => sem_long sg n1 n2 @@ -569,6 +672,7 @@ Definition sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val := (fun sg n1 n2 => Some(Vint(Int.add n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.add n1 n2))) (fun n1 n2 => Some(Vfloat(Float.add n1 n2))) + (fun n1 n2 => Some(Vsingle(Float32.add n1 n2))) v1 t1 v2 t2 end. @@ -617,6 +721,7 @@ Definition sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val := (fun sg n1 n2 => Some(Vint(Int.sub n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.sub n1 n2))) (fun n1 n2 => Some(Vfloat(Float.sub n1 n2))) + (fun n1 n2 => Some(Vsingle(Float32.sub n1 n2))) v1 t1 v2 t2 end. @@ -627,6 +732,7 @@ Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val := (fun sg n1 n2 => Some(Vint(Int.mul n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.mul n1 n2))) (fun n1 n2 => Some(Vfloat(Float.mul n1 n2))) + (fun n1 n2 => Some(Vsingle(Float32.mul n1 n2))) v1 t1 v2 t2. Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val := @@ -652,6 +758,7 @@ Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val := then None else Some(Vlong(Int64.divu n1 n2)) end) (fun n1 n2 => Some(Vfloat(Float.div n1 n2))) + (fun n1 n2 => Some(Vsingle(Float32.div n1 n2))) v1 t1 v2 t2. Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val := @@ -677,6 +784,7 @@ Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val := then None else Some(Vlong(Int64.modu n1 n2)) end) (fun n1 n2 => None) + (fun n1 n2 => None) v1 t1 v2 t2. Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val := @@ -684,6 +792,7 @@ Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val := (fun sg n1 n2 => Some(Vint(Int.and n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.and n1 n2))) (fun n1 n2 => None) + (fun n1 n2 => None) v1 t1 v2 t2. Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val := @@ -691,6 +800,7 @@ Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val := (fun sg n1 n2 => Some(Vint(Int.or n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.or n1 n2))) (fun n1 n2 => None) + (fun n1 n2 => None) v1 t1 v2 t2. Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val := @@ -698,6 +808,7 @@ Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val := (fun sg n1 n2 => Some(Vint(Int.xor n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.xor n1 n2))) (fun n1 n2 => None) + (fun n1 n2 => None) v1 t1 v2 t2. (** *** Shifts *) @@ -818,6 +929,8 @@ Definition sem_cmp (c:comparison) Some(Val.of_bool(match sg with Signed => Int64.cmp c n1 n2 | Unsigned => Int64.cmpu c n1 n2 end))) (fun n1 n2 => Some(Val.of_bool(Float.cmp c n1 n2))) + (fun n1 n2 => + Some(Val.of_bool(Float32.cmp c n1 n2))) v1 t1 v2 t2 end. @@ -946,7 +1059,9 @@ Proof. inv H0; inv H; TrivialInject. - econstructor; eauto. - destruct (cast_float_int si2 f0); inv H1; TrivialInject. +- destruct (cast_single_int si2 f0); inv H1; TrivialInject. - destruct (cast_float_long si2 f0); inv H1; TrivialInject. +- destruct (cast_single_long si2 f0); inv H1; TrivialInject. - destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto. - destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto. - econstructor; eauto. @@ -976,18 +1091,19 @@ Definition optval_self_injects (ov: option val) : Prop := end. Remark sem_binarith_inject: - forall sem_int sem_long sem_float v1 t1 v2 t2 v v1' v2', - sem_binarith sem_int sem_long sem_float v1 t1 v2 t2 = Some v -> + forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 v v1' v2', + sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 = Some v -> val_inject f v1 v1' -> val_inject f v2 v2' -> (forall sg n1 n2, optval_self_injects (sem_int sg n1 n2)) -> (forall sg n1 n2, optval_self_injects (sem_long sg n1 n2)) -> (forall n1 n2, optval_self_injects (sem_float n1 n2)) -> - exists v', sem_binarith sem_int sem_long sem_float v1' t1 v2' t2 = Some v' /\ val_inject f v v'. + (forall n1 n2, optval_self_injects (sem_single n1 n2)) -> + exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ val_inject f v v'. Proof. intros. assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> val_inject f v v). { - intros. subst ov; simpl in H6. destruct v0; contradiction || constructor. + intros. subst ov; simpl in H7. destruct v0; contradiction || constructor. } unfold sem_binarith in *. set (c := classify_binarith t1 t2) in *. @@ -1093,6 +1209,7 @@ Proof. || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); exact I. destruct (Int64.eq n2 Int64.zero); exact I. exact I. + exact I. - (* mod *) eapply sem_binarith_inject; eauto; intros. destruct sg. @@ -1104,6 +1221,7 @@ Proof. || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); exact I. destruct (Int64.eq n2 Int64.zero); exact I. exact I. + exact I. - (* and *) eapply sem_binarith_inject; eauto; intros; exact I. - (* or *) @@ -1168,7 +1286,8 @@ Proof. match t with | Tint _ _ _ => bool_case_i | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p - | Tfloat _ _ => bool_case_f + | Tfloat F64 _ => bool_case_f + | Tfloat F32 _ => bool_case_s | Tlong _ _ => bool_case_l | _ => bool_default end). @@ -1178,7 +1297,14 @@ Proof. unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto. destruct (Int.eq i0 Int.zero); auto. destruct (Int64.eq i Int64.zero); auto. + destruct f; auto. + destruct f; auto. + destruct f; auto. + destruct f; auto. destruct (Float.cmp Ceq f0 Float.zero); auto. + destruct f; auto. + destruct (Float32.cmp Ceq f0 Float32.zero); auto. + destruct f; auto. destruct (Int.eq i Int.zero); auto. destruct (Int.eq i Int.zero); auto. destruct (Int.eq i Int.zero); auto. @@ -1360,8 +1486,8 @@ Qed. Lemma classify_binarith_arithmetic_conversion: forall t1 t2, - binarith_result_type (classify_binarith (proj_type t1) (proj_type t2)) = - Some (proj_type (usual_arithmetic_conversion t1 t2)). + binarith_type (classify_binarith (proj_type t1) (proj_type t2)) = + proj_type (usual_arithmetic_conversion t1 t2). Proof. destruct t1; destruct t2; try reflexivity. - destruct it; destruct it0; reflexivity. diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 4b2e915..d37fa81 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -33,7 +33,8 @@ Require Import Smallstep. Inductive constant : Type := | Ointconst: int -> constant (**r integer constant *) - | Ofloatconst: float -> constant (**r floating-point constant *) + | Ofloatconst: float -> constant (**r double-precision floating-point constant *) + | Osingleconst: float32 -> constant (**r single-precision floating-point constant *) | Olongconst: int64 -> constant. (**r long integer constant *) Definition unary_operation : Type := Cminor.unary_operation. @@ -253,6 +254,7 @@ Definition eval_constant (cst: constant) : option val := match cst with | Ointconst n => Some (Vint n) | Ofloatconst n => Some (Vfloat n) + | Osingleconst n => Some (Vsingle n) | Olongconst n => Some (Vlong n) end. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 685fa71..cedfd8b 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -50,16 +50,25 @@ Open Local Scope error_monad_scope. Definition make_intconst (n: int) := Econst (Ointconst n). +Definition make_longconst (f: int64) := Econst (Olongconst f). + Definition make_floatconst (f: float) := Econst (Ofloatconst f). -Definition make_longconst (f: int64) := Econst (Olongconst f). +Definition make_singleconst (f: float32) := Econst (Osingleconst f). -Definition make_floatofint (e: expr) (sg: signedness) (sz: floatsize) := - match sg, sz with - | Signed, F64 => Eunop Ofloatofint e - | Unsigned, F64 => Eunop Ofloatofintu e - | Signed, F32 => Eunop Osingleoffloat (Eunop Ofloatofint e) - | Unsigned, F32 => Eunop Osingleoffloat (Eunop Ofloatofintu e) +Definition make_singleoffloat (e: expr) := Eunop Osingleoffloat e. +Definition make_floatofsingle (e: expr) := Eunop Ofloatofsingle e. + +Definition make_floatofint (e: expr) (sg: signedness) := + match sg with + | Signed => Eunop Ofloatofint e + | Unsigned => Eunop Ofloatofintu e + end. + +Definition make_singleofint (e: expr) (sg: signedness) := + match sg with + | Signed => Eunop Osingleofint e + | Unsigned => Eunop Osingleofintu e end. Definition make_intoffloat (e: expr) (sg: signedness) := @@ -68,18 +77,28 @@ Definition make_intoffloat (e: expr) (sg: signedness) := | Unsigned => Eunop Ointuoffloat e end. +Definition make_intofsingle (e: expr) (sg: signedness) := + match sg with + | Signed => Eunop Ointofsingle e + | Unsigned => Eunop Ointuofsingle e + end. + Definition make_longofint (e: expr) (sg: signedness) := match sg with | Signed => Eunop Olongofint e | Unsigned => Eunop Olongofintu e end. -Definition make_floatoflong (e: expr) (sg: signedness) (sz: floatsize) := - match sg, sz with - | Signed, F64 => Eunop Ofloatoflong e - | Unsigned, F64 => Eunop Ofloatoflongu e - | Signed, F32 => Eunop Osingleoflong e - | Unsigned, F32 => Eunop Osingleoflongu e +Definition make_floatoflong (e: expr) (sg: signedness) := + match sg with + | Signed => Eunop Ofloatoflong e + | Unsigned => Eunop Ofloatoflongu e + end. + +Definition make_singleoflong (e: expr) (sg: signedness) := + match sg with + | Signed => Eunop Osingleoflong e + | Unsigned => Eunop Osingleoflongu e end. Definition make_longoffloat (e: expr) (sg: signedness) := @@ -88,11 +107,18 @@ Definition make_longoffloat (e: expr) (sg: signedness) := | Unsigned => Eunop Olonguoffloat e end. +Definition make_longofsingle (e: expr) (sg: signedness) := + match sg with + | Signed => Eunop Olongofsingle e + | Unsigned => Eunop Olonguofsingle e + end. + Definition make_cmp_ne_zero (e: expr) := match e with | Ebinop (Ocmp c) e1 e2 => e | Ebinop (Ocmpu c) e1 e2 => e | Ebinop (Ocmpf c) e1 e2 => e + | Ebinop (Ocmpfs c) e1 e2 => e | Ebinop (Ocmpl c) e1 e2 => e | Ebinop (Ocmplu c) e1 e2 => e | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero) @@ -111,25 +137,27 @@ Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) := | IBool, _ => make_cmp_ne_zero e end. -Definition make_cast_float (e: expr) (sz: floatsize) := - match sz with - | F32 => Eunop Osingleoffloat e - | F64 => e - end. - Definition make_cast (from to: type) (e: expr) := match classify_cast from to with | cast_case_neutral => OK e | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2) - | cast_case_f2f sz2 => OK (make_cast_float e sz2) - | cast_case_i2f si1 sz2 => OK (make_floatofint e si1 sz2) + | cast_case_f2f => OK e + | cast_case_s2s => OK e + | cast_case_f2s => OK (make_singleoffloat e) + | cast_case_s2f => OK (make_floatofsingle e) + | cast_case_i2f si1 => OK (make_floatofint e si1) + | cast_case_i2s si1 => OK (make_singleofint e si1) | cast_case_f2i sz2 si2 => OK (make_cast_int (make_intoffloat e si2) sz2 si2) + | cast_case_s2i sz2 si2 => OK (make_cast_int (make_intofsingle e si2) sz2 si2) | cast_case_l2l => OK e | cast_case_i2l si1 => OK (make_longofint e si1) | cast_case_l2i sz2 si2 => OK (make_cast_int (Eunop Ointoflong e) sz2 si2) - | cast_case_l2f si1 sz2 => OK (make_floatoflong e si1 sz2) + | cast_case_l2f si1 => OK (make_floatoflong e si1) + | cast_case_l2s si1 => OK (make_singleoflong e si1) | cast_case_f2l si2 => OK (make_longoffloat e si2) + | cast_case_s2l si2 => OK (make_longofsingle e si2) | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)) + | cast_case_s2bool => OK (Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero)) | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero)) | cast_case_p2bool => OK (Ebinop (Ocmpu Cne) e (make_intconst Int.zero)) | cast_case_struct id1 fld1 id2 fld2 => OK e @@ -145,6 +173,7 @@ Definition make_boolean (e: expr) (ty: type) := match classify_bool ty with | bool_case_i => make_cmp_ne_zero e | bool_case_f => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero) + | bool_case_s => Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero) | bool_case_p => Ebinop (Ocmpu Cne) e (make_intconst Int.zero) | bool_case_l => Ebinop (Ocmpl Cne) e (make_longconst Int64.zero) | bool_default => e (**r should not happen *) @@ -156,6 +185,7 @@ Definition make_notbool (e: expr) (ty: type) := match classify_bool ty with | bool_case_i => OK (Ebinop (Ocmp Ceq) e (make_intconst Int.zero)) | bool_case_f => OK (Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero)) + | bool_case_s => OK (Ebinop (Ocmpfs Ceq) e (make_singleconst Float32.zero)) | bool_case_p => OK (Ebinop (Ocmpu Ceq) e (make_intconst Int.zero)) | bool_case_l => OK (Ebinop (Ocmpl Ceq) e (make_longconst Int64.zero)) | _ => Error (msg "Cshmgen.make_notbool") @@ -164,16 +194,18 @@ Definition make_notbool (e: expr) (ty: type) := Definition make_neg (e: expr) (ty: type) := match classify_neg ty with | neg_case_i _ => OK (Eunop Onegint e) - | neg_case_f _ => OK (Eunop Onegf e) + | neg_case_f => OK (Eunop Onegf e) + | neg_case_s => OK (Eunop Onegfs e) | neg_case_l _ => OK (Eunop Onegl e) | _ => Error (msg "Cshmgen.make_neg") end. Definition make_absfloat (e: expr) (ty: type) := match classify_neg ty with - | neg_case_i sg => OK (Eunop Oabsf (make_floatofint e sg F64)) - | neg_case_f _ => OK (Eunop Oabsf e) - | neg_case_l sg => OK (Eunop Oabsf (make_floatoflong e sg F64)) + | neg_case_i sg => OK (Eunop Oabsf (make_floatofint e sg)) + | neg_case_f => OK (Eunop Oabsf e) + | neg_case_s => OK (Eunop Oabsf (make_floatofsingle e)) + | neg_case_l sg => OK (Eunop Oabsf (make_floatoflong e sg)) | _ => Error (msg "Cshmgen.make_absfloat") end. @@ -186,7 +218,7 @@ Definition make_notint (e: expr) (ty: type) := (** Binary operators *) -Definition make_binarith (iop iopu fop lop lopu: binary_operation) +Definition make_binarith (iop iopu fop sop lop lopu: binary_operation) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := let c := classify_binarith ty1 ty2 in let ty := binarith_type c in @@ -195,7 +227,8 @@ Definition make_binarith (iop iopu fop lop lopu: binary_operation) match c with | bin_case_i Signed => OK (Ebinop iop e1' e2') | bin_case_i Unsigned => OK (Ebinop iopu e1' e2') - | bin_case_f _ => OK (Ebinop fop e1' e2') + | bin_case_f => OK (Ebinop fop e1' e2') + | bin_case_s => OK (Ebinop sop e1' e2') | bin_case_l Signed => OK (Ebinop lop e1' e2') | bin_case_l Unsigned => OK (Ebinop lopu e1' e2') | bin_default => Error (msg "Cshmgen.make_binarith") @@ -216,7 +249,7 @@ Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) := let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1))) | add_default => - make_binarith Oadd Oadd Oaddf Oaddl Oaddl e1 ty1 e2 ty2 + make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2 end. Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) := @@ -231,14 +264,14 @@ Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) := let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2))) | sub_default => - make_binarith Osub Osub Osubf Osubl Osubl e1 ty1 e2 ty2 + make_binarith Osub Osub Osubf Osubfs Osubl Osubl e1 ty1 e2 ty2 end. Definition make_mul (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - make_binarith Omul Omul Omulf Omull Omull e1 ty1 e2 ty2. + make_binarith Omul Omul Omulf Omulfs Omull Omull e1 ty1 e2 ty2. Definition make_div (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - make_binarith Odiv Odivu Odivf Odivl Odivlu e1 ty1 e2 ty2. + make_binarith Odiv Odivu Odivf Odivfs Odivl Odivlu e1 ty1 e2 ty2. Definition make_binarith_int (iop iopu lop lopu: binary_operation) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := @@ -251,7 +284,7 @@ Definition make_binarith_int (iop iopu lop lopu: binary_operation) | bin_case_i Unsigned => OK (Ebinop iopu e1' e2') | bin_case_l Signed => OK (Ebinop lop e1' e2') | bin_case_l Unsigned => OK (Ebinop lopu e1' e2') - | bin_case_f _ | bin_default => Error (msg "Cshmgen.make_binarith_int") + | bin_case_f | bin_case_s | bin_default => Error (msg "Cshmgen.make_binarith_int") end. Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) := @@ -294,7 +327,9 @@ Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type | cmp_case_pl => OK (Ebinop (Ocmpu c) e1 (Eunop Ointoflong e2)) | cmp_case_lp => OK (Ebinop (Ocmpu c) (Eunop Ointoflong e1) e2) | cmp_default => - make_binarith (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpl c) (Ocmplu c) e1 ty1 e2 ty2 + make_binarith + (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpfs c) (Ocmpl c) (Ocmplu c) + e1 ty1 e2 ty2 end. (** [make_load addr ty_res] loads a value of type [ty_res] from @@ -374,6 +409,8 @@ Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr := OK(make_intconst n) | Clight.Econst_float n _ => OK(make_floatconst n) + | Clight.Econst_single n _ => + OK(make_singleconst n) | Clight.Econst_long n _ => OK(make_longconst n) | Clight.Evar id ty => @@ -454,8 +491,9 @@ Fixpoint transl_arglist (al: list Clight.expr) (tyl: typelist) | a1 :: a2, Tnil => (* Tolerance for calls to K&R or variadic functions *) do ta1 <- transl_expr a1; + do ta1' <- make_cast (typeof a1) (default_argument_conversion (typeof a1)) ta1; do ta2 <- transl_arglist a2 Tnil; - OK (ta1 :: ta2) + OK (ta1' :: ta2) | _, _ => Error(msg "Cshmgen.transl_arglist: arity mismatch") end. @@ -470,7 +508,7 @@ Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: typelist) typ_of_type ty1 :: typlist_of_arglist a2 ty2 | a1 :: a2, Tnil => (* Tolerance for calls to K&R or variadic functions *) - typ_of_type_default (typeof a1) :: typlist_of_arglist a2 Tnil + typ_of_type (default_argument_conversion (typeof a1)) :: typlist_of_arglist a2 Tnil end. (** * Translation of statements *) diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 15c4e4c..a977e0f 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -159,6 +159,13 @@ Proof. intros. unfold make_floatconst. econstructor. reflexivity. Qed. +Lemma make_singleconst_correct: + forall n e le m, + eval_expr ge e le m (make_singleconst n) (Vsingle n). +Proof. + intros. unfold make_singleconst. econstructor. reflexivity. +Qed. + Lemma make_longconst_correct: forall n e le m, eval_expr ge e le m (make_longconst n) (Vlong n). @@ -166,62 +173,35 @@ Proof. intros. unfold make_floatconst. econstructor. reflexivity. Qed. -Lemma make_floatofint_correct: - forall a n sg sz e le m, - eval_expr ge e le m a (Vint n) -> - eval_expr ge e le m (make_floatofint a sg sz) (Vfloat(cast_int_float sg sz n)). +Lemma make_singleoffloat_correct: + forall a n e le m, + eval_expr ge e le m a (Vfloat n) -> + eval_expr ge e le m (make_singleoffloat a) (Vsingle (Float.to_single n)). Proof. - intros. unfold make_floatofint, cast_int_float. - destruct sz. - destruct sg. - rewrite Float.singleofint_floatofint. econstructor. econstructor; eauto. simpl; reflexivity. auto. - rewrite Float.singleofintu_floatofintu. econstructor. econstructor; eauto. simpl; reflexivity. auto. - destruct sg; econstructor; eauto. + intros. econstructor. eauto. auto. Qed. -Lemma make_intoffloat_correct: - forall e le m a sg f i, - eval_expr ge e le m a (Vfloat f) -> - cast_float_int sg f = Some i -> - eval_expr ge e le m (make_intoffloat a sg) (Vint i). +Lemma make_floatofsingle_correct: + forall a n e le m, + eval_expr ge e le m a (Vsingle n) -> + eval_expr ge e le m (make_floatofsingle a) (Vfloat (Float.of_single n)). Proof. - unfold cast_float_int, make_intoffloat; intros. - destruct sg; econstructor; eauto; simpl; rewrite H0; auto. + intros. econstructor. eauto. auto. Qed. -Lemma make_longofint_correct: +Lemma make_floatofint_correct: forall a n sg e le m, eval_expr ge e le m a (Vint n) -> - eval_expr ge e le m (make_longofint a sg) (Vlong(cast_int_long sg n)). + eval_expr ge e le m (make_floatofint a sg) (Vfloat(cast_int_float sg n)). Proof. - intros. unfold make_longofint, cast_int_long. + intros. unfold make_floatofint, cast_int_float. destruct sg; econstructor; eauto. Qed. -Lemma make_floatoflong_correct: - forall a n sg sz e le m, - eval_expr ge e le m a (Vlong n) -> - eval_expr ge e le m (make_floatoflong a sg sz) (Vfloat(cast_long_float sg sz n)). -Proof. - intros. unfold make_floatoflong, cast_int_long. - destruct sg; destruct sz; econstructor; eauto. -Qed. - -Lemma make_longoffloat_correct: - forall e le m a sg f i, - eval_expr ge e le m a (Vfloat f) -> - cast_float_long sg f = Some i -> - eval_expr ge e le m (make_longoffloat a sg) (Vlong i). -Proof. - unfold cast_float_long, make_longoffloat; intros. - destruct sg; econstructor; eauto; simpl; rewrite H0; auto. -Qed. - Hint Resolve make_intconst_correct make_floatconst_correct make_longconst_correct - make_floatofint_correct make_intoffloat_correct - make_longofint_correct - make_floatoflong_correct make_longoffloat_correct - eval_Eunop eval_Ebinop: cshm. + make_singleconst_correct make_singleoffloat_correct make_floatofsingle_correct + make_floatofint_correct: cshm. +Hint Constructors eval_expr eval_exprlist: cshm. Hint Extern 2 (@eq trace _ _) => traceEq: cshm. Lemma make_cmp_ne_zero_correct: @@ -248,6 +228,9 @@ Proof. inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. inv H6. unfold Val.cmp in H0. eauto. inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. unfold Val.cmpfs in H6. + destruct (Val.cmpfs_bool c v1 v2) as [[]|]; inv H6; reflexivity. + inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. unfold Val.cmpl in H6. destruct (Val.cmpl_bool c v1 v2) as [[]|]; inv H6; reflexivity. inv H. econstructor; eauto. rewrite H6. decEq. decEq. @@ -268,16 +251,7 @@ Proof. apply make_cmp_ne_zero_correct; auto. Qed. -Lemma make_cast_float_correct: - forall e le m a n sz, - eval_expr ge e le m a (Vfloat n) -> - eval_expr ge e le m (make_cast_float a sz) (Vfloat (cast_float_float sz n)). -Proof. - intros. unfold make_cast_float, cast_float_float. - destruct sz. eauto with cshm. auto. -Qed. - -Hint Resolve make_cast_int_correct make_cast_float_correct: cshm. +Hint Resolve make_cast_int_correct: cshm. Lemma make_cast_correct: forall e le m a b v ty1 ty2 v', @@ -288,14 +262,40 @@ Lemma make_cast_correct: Proof. intros. unfold make_cast, sem_cast in *; destruct (classify_cast ty1 ty2); inv H; destruct v; inv H1; eauto with cshm. + (* single -> int *) + unfold make_singleofint, cast_int_float. destruct si1; eauto with cshm. (* float -> int *) - destruct (cast_float_int si2 f) as [i|] eqn:E; inv H2. eauto with cshm. + destruct (cast_float_int si2 f) as [i|] eqn:E; inv H2. + apply make_cast_int_correct. + unfold cast_float_int in E. unfold make_intoffloat. + destruct si2; econstructor; eauto; simpl; rewrite E; auto. + (* single -> int *) + destruct (cast_single_int si2 f) as [i|] eqn:E; inv H2. + apply make_cast_int_correct. + unfold cast_single_int in E. unfold make_intofsingle. + destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto. + (* long -> int *) + unfold make_longofint, cast_int_long. destruct si1; eauto with cshm. + (* long -> float *) + unfold make_floatoflong, cast_long_float. destruct si1; eauto with cshm. + (* long -> single *) + unfold make_singleoflong, cast_long_single. destruct si1; eauto with cshm. (* float -> long *) - destruct (cast_float_long si2 f) as [i|] eqn:E; inv H2. eauto with cshm. + destruct (cast_float_long si2 f) as [i|] eqn:E; inv H2. + unfold cast_float_long in E. unfold make_longoffloat. + destruct si2; econstructor; eauto; simpl; rewrite E; auto. + (* single -> long *) + destruct (cast_single_long si2 f) as [i|] eqn:E; inv H2. + unfold cast_single_long in E. unfold make_longofsingle. + destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto. (* float -> bool *) econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f Float.zero); auto. + (* single -> bool *) + econstructor; eauto with cshm. + simpl. unfold Val.cmpfs, Val.cmpfs_bool. rewrite Float32.cmp_ne_eq. + destruct (Float32.cmp Ceq f Float32.zero); auto. (* long -> bool *) econstructor; eauto with cshm. simpl. unfold Val.cmpl, Val.cmpl_bool, Int64.cmp. @@ -327,6 +327,10 @@ Proof. econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpf, Val.cmpf_bool. simpl. rewrite <- Float.cmp_ne_eq. destruct (Float.cmp Cne f Float.zero); constructor. +(* single *) + econstructor; split. econstructor; eauto with cshm. simpl. eauto. + unfold Val.cmpfs, Val.cmpfs_bool. simpl. rewrite <- Float32.cmp_ne_eq. + destruct (Float32.cmp Cne f Float32.zero); constructor. (* pointer *) econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpu, Val.cmpu_bool. simpl. @@ -357,6 +361,9 @@ Lemma make_absfloat_correct: Proof. unfold sem_absfloat, make_absfloat; intros until m; intros SEM MAKE EV1; destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm. + unfold make_floatoflong, cast_long_float. destruct s. + econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto. + econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto. Qed. Lemma make_notbool_correct: @@ -396,7 +403,8 @@ Section MAKE_BIN. Variable sem_int: signedness -> int -> int -> option val. Variable sem_long: signedness -> int64 -> int64 -> option val. Variable sem_float: float -> float -> option val. -Variables iop iopu fop lop lopu: binary_operation. +Variable sem_single: float32 -> float32 -> option val. +Variables iop iopu fop sop lop lopu: binary_operation. Hypothesis iop_ok: forall x y m, eval_binop iop (Vint x) (Vint y) m = sem_int Signed x y. @@ -408,11 +416,13 @@ Hypothesis lopu_ok: forall x y m, eval_binop lopu (Vlong x) (Vlong y) m = sem_long Unsigned x y. Hypothesis fop_ok: forall x y m, eval_binop fop (Vfloat x) (Vfloat y) m = sem_float x y. +Hypothesis sop_ok: + forall x y m, eval_binop sop (Vsingle x) (Vsingle y) m = sem_single x y. Lemma make_binarith_correct: binary_constructor_correct - (make_binarith iop iopu fop lop lopu) - (sem_binarith sem_int sem_long sem_float). + (make_binarith iop iopu fop sop lop lopu) + (sem_binarith sem_int sem_long sem_float sem_single). Proof. red; unfold make_binarith, sem_binarith; intros until m; intros SEM MAKE EV1 EV2. @@ -429,12 +439,13 @@ Proof. - destruct s; inv H0; econstructor; eauto with cshm. rewrite lop_ok; auto. rewrite lopu_ok; auto. - erewrite <- fop_ok in SEM; eauto with cshm. +- erewrite <- sop_ok in SEM; eauto with cshm. Qed. Lemma make_binarith_int_correct: binary_constructor_correct (make_binarith_int iop iopu lop lopu) - (sem_binarith sem_int sem_long (fun x y => None)). + (sem_binarith sem_int sem_long (fun x y => None) (fun x y => None)). Proof. red; unfold make_binarith_int, sem_binarith; intros until m; intros SEM MAKE EV1 EV2. @@ -930,6 +941,8 @@ Proof. apply make_intconst_correct. (* const float *) apply make_floatconst_correct. +(* const single *) + apply make_singleconst_correct. (* const long *) apply make_longconst_correct. (* temp var *) diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 41d0dcb..c437a6b 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -196,6 +196,18 @@ Definition typeconv (ty: type) : type := | _ => remove_attributes ty end. +(** Default conversion for arguments to an unprototyped or variadic function. + Like [typeconv] but also converts single floats to double floats. *) + +Definition default_argument_conversion (ty: type) : type := + match ty with + | Tint (I8 | I16 | IBool) _ _ => Tint I32 Signed noattr + | Tfloat _ _ => Tfloat F64 noattr + | Tarray t sz a => Tpointer t noattr + | Tfunction _ _ _ => Tpointer ty noattr + | _ => remove_attributes ty + end. + (** * Operations over types *) (** Alignment of a type, in bytes. *) @@ -723,12 +735,3 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature := mksignature (typlist_of_typelist args) (opttyp_of_type res) cc. -(** Like [typ_of_type], but apply default argument promotion. *) - -Definition typ_of_type_default (t: type) : AST.typ := - match t with - | Tfloat _ _ => AST.Tfloat - | Tlong _ _ => AST.Tlong - | _ => AST.Tint - end. - diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 4054f6e..3454ddc 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -55,7 +55,7 @@ Fixpoint constval (a: expr) : res val := match a with | Eval v ty => match v with - | Vint _ | Vfloat _ | Vlong _ => OK v + | Vint _ | Vfloat _ | Vsingle _ | Vlong _ => OK v | Vptr _ _ | Vundef => Error(msg "illegal constant") end | Evalof l ty => @@ -156,7 +156,7 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data := | Vint n, Tpointer _ _ => OK(Init_int32 n) | Vint n, Tcomp_ptr _ _ => OK(Init_int32 n) | Vlong n, Tlong _ _ => OK(Init_int64 n) - | Vfloat f, Tfloat F32 _ => OK(Init_float32 f) + | Vsingle f, Tfloat F32 _ => OK(Init_float32 f) | Vfloat f, Tfloat F64 _ => OK(Init_float64 f) | Vptr id ofs, Tint I32 sg _ => OK(Init_addrof id ofs) | Vptr id ofs, Tpointer _ _ => OK(Init_addrof id ofs) diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index f11901d..16004fc 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -506,6 +506,9 @@ Proof. (* float *) destruct ty; try discriminate. destruct f1; inv EQ2; simpl in H2; inv H2; assumption. + (* single *) + destruct ty; try discriminate. + destruct f1; inv EQ2; simpl in H2; inv H2; assumption. (* pointer *) unfold inj in H. assert (data = Init_addrof b1 ofs1 /\ chunk = Mint32). @@ -525,20 +528,18 @@ Lemma transl_init_single_size: Genv.init_data_size data = sizeof ty. Proof. intros. monadInv H. destruct x0. - monadInv EQ2. - destruct ty; try discriminate. +- monadInv EQ2. +- destruct ty; try discriminate. destruct i0; inv EQ2; auto. inv EQ2; auto. inv EQ2; auto. - destruct ty; inv EQ2; auto. - destruct ty; try discriminate. +- destruct ty; inv EQ2; auto. +- destruct ty; try discriminate. destruct f0; inv EQ2; auto. - destruct ty; try discriminate. - destruct i0; auto. - inv EQ2. - inv EQ2. - inv EQ2; auto. - inv EQ2. +- destruct ty; try discriminate. + destruct f0; inv EQ2; auto. +- destruct ty; try discriminate. + destruct i0; inv EQ2; auto. inv EQ2; auto. inv EQ2; auto. Qed. diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 49705c4..c5a6e6e 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -43,6 +43,7 @@ let rec precedence = function | Efield _ -> (16, LtoR) | Econst_int _ -> (16, NA) | Econst_float _ -> (16, NA) + | Econst_single _ -> (16, NA) | Econst_long _ -> (16, NA) | Eunop _ -> (15, RtoL) | Eaddrof _ -> (15, RtoL) @@ -82,6 +83,8 @@ let rec expr p (prec, e) = fprintf p "%ld" (camlint_of_coqint n) | Econst_float(f, _) -> fprintf p "%F" (camlfloat_of_coqfloat f) + | Econst_single(f, _) -> + fprintf p "%Ff" (camlfloat_of_coqfloat32 f) | Econst_long(n, Tlong(Unsigned, _)) -> fprintf p "%LuLLU" (camlint64_of_coqint n) | Econst_long(n, _) -> @@ -269,6 +272,7 @@ let rec collect_expr e = match e with | Econst_int _ -> () | Econst_float _ -> () + | Econst_single _ -> () | Econst_long _ -> () | Evar _ -> () | Etempvar _ -> () diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 9441d71..4e0ee7f 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -191,6 +191,8 @@ let print_typed_value p v ty = fprintf p "%ld" (camlint_of_coqint n) | Vfloat f, _ -> fprintf p "%F" (camlfloat_of_coqfloat f) + | Vsingle f, _ -> + fprintf p "%Ff" (camlfloat_of_coqfloat32 f) | Vlong n, Tlong(Unsigned, _) -> fprintf p "%LuLLU" (camlint64_of_coqint n) | Vlong n, _ -> diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index f9aa8db..05d9c86 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -116,6 +116,7 @@ Function eval_simpl_expr (a: expr) : option val := match a with | Econst_int n _ => Some(Vint n) | Econst_float n _ => Some(Vfloat n) + | Econst_single n _ => Some(Vsingle n) | Econst_long n _ => Some(Vlong n) | Ecast b ty => match eval_simpl_expr b with @@ -242,6 +243,8 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement ret (finish dst nil (Econst_int n ty)) | Csyntax.Eval (Vfloat n) ty => ret (finish dst nil (Econst_float n ty)) + | Csyntax.Eval (Vsingle n) ty => + ret (finish dst nil (Econst_single n ty)) | Csyntax.Eval (Vlong n) ty => ret (finish dst nil (Econst_long n ty)) | Csyntax.Eval _ ty => diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 3dae7ab..1ef2e76 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -799,6 +799,10 @@ Opaque makeif. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. + intros. destruct dst; simpl in *; inv H2. + constructor. auto. intros; constructor. + constructor. + constructor. auto. intros; constructor. (* var *) monadInv H; econstructor; split; auto with gensym. UseFinish. constructor. (* field *) diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index 2956508..9c52928 100644 --- a/cfrontend/SimplLocals.v +++ b/cfrontend/SimplLocals.v @@ -45,7 +45,8 @@ Definition make_cast (a: expr) (tto: type) : expr := match classify_cast (typeof a) tto with | cast_case_neutral => a | cast_case_i2i I32 _ => a - | cast_case_f2f F64 => a + | cast_case_f2f => a + | cast_case_s2s => a | cast_case_l2l => a | cast_case_struct _ _ _ _ => a | cast_case_union _ _ _ _ => a @@ -59,6 +60,7 @@ Fixpoint simpl_expr (cenv: compilenv) (a: expr) : expr := match a with | Econst_int _ _ => a | Econst_float _ _ => a + | Econst_single _ _ => a | Econst_long _ _ => a | Evar id ty => if VSet.mem id cenv then Etempvar id ty else Evar id ty | Etempvar id ty => Etempvar id ty @@ -157,6 +159,7 @@ Fixpoint addr_taken_expr (a: expr): VSet.t := match a with | Econst_int _ _ => VSet.empty | Econst_float _ _ => VSet.empty + | Econst_single _ _ => VSet.empty | Econst_long _ _ => VSet.empty | Evar id ty => VSet.empty | Etempvar id ty => VSet.empty diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 6eec8cc..6024de4 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -189,9 +189,10 @@ Inductive val_casted: val -> type -> Prop := | val_casted_int: forall sz si attr n, cast_int_int sz si n = n -> val_casted (Vint n) (Tint sz si attr) - | val_casted_float: forall sz attr n, - cast_float_float sz n = n -> - val_casted (Vfloat n) (Tfloat sz attr) + | val_casted_float: forall attr n, + val_casted (Vfloat n) (Tfloat F64 attr) + | val_casted_single: forall attr n, + val_casted (Vsingle n) (Tfloat F32 attr) | val_casted_long: forall si attr n, val_casted (Vlong n) (Tlong si attr) | val_casted_ptr_ptr: forall b ofs ty attr, @@ -220,14 +221,6 @@ Proof. destruct (Int.eq i Int.zero); auto. Qed. -Remark cast_float_float_idem: - forall sz f, cast_float_float sz (cast_float_float sz f) = cast_float_float sz f. -Proof. - intros; destruct sz; simpl. - apply Float.singleoffloat_idem; auto. - auto. -Qed. - Lemma cast_val_is_casted: forall v ty ty' v', sem_cast v ty ty' = Some v' -> val_casted v' ty'. Proof. @@ -235,28 +228,32 @@ Proof. (* void *) constructor. (* int *) - destruct i; destruct ty; simpl in H; try discriminate; destruct v; inv H. + destruct i; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H. constructor. apply (cast_int_int_idem I8 s). constructor. apply (cast_int_int_idem I8 s). - destruct (cast_float_int s f0); inv H1. constructor. apply (cast_int_int_idem I8 s). + destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). + destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). constructor. apply (cast_int_int_idem I16 s). constructor. apply (cast_int_int_idem I16 s). - destruct (cast_float_int s f0); inv H1. constructor. apply (cast_int_int_idem I16 s). + destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). + destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). constructor. auto. constructor. constructor. auto. - destruct (cast_float_int s f0); inv H1. constructor. auto. - constructor. auto. - constructor. + destruct (cast_single_int s f); inv H1. constructor. auto. + destruct (cast_float_int s f); inv H1. constructor; auto. constructor; auto. constructor. constructor; auto. + constructor. constructor; auto. + constructor. constructor; auto. - constructor; auto. + constructor. constructor. simpl. destruct (Int.eq i0 Int.zero); auto. constructor. simpl. destruct (Int64.eq i Int64.zero); auto. - constructor. simpl. destruct (Float.cmp Ceq f0 Float.zero); auto. + constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto. + constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. @@ -266,23 +263,17 @@ Proof. constructor. simpl. destruct (Int.eq i0 Int.zero); auto. constructor; auto. (* long *) - destruct ty; try discriminate. + destruct ty; try (destruct f); try discriminate. destruct v; inv H. constructor. destruct v; inv H. constructor. - destruct v; try discriminate. destruct (cast_float_long s f0); inv H. constructor. + destruct v; try discriminate. destruct (cast_single_long s f); inv H. constructor. + destruct v; try discriminate. destruct (cast_float_long s f); inv H. constructor. destruct v; inv H. constructor. destruct v; inv H. constructor. destruct v; inv H. constructor. destruct v; inv H. constructor. (* float *) - destruct ty; simpl in H; try discriminate; destruct v; inv H. - constructor. unfold cast_float_float, cast_int_float. - destruct f; destruct s; auto. - rewrite Float.singleofint_floatofint. apply Float.singleoffloat_idem. - rewrite Float.singleofintu_floatofintu. apply Float.singleoffloat_idem. - constructor. unfold cast_float_float, cast_long_float. - destruct f; destruct s; auto. apply Float.singleoflong_idem. apply Float.singleoflongu_idem. - constructor. apply cast_float_float_idem. + destruct f; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H; constructor. (* pointer *) destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor. (* impossible cases *) @@ -310,7 +301,8 @@ Proof. clear H1. inv H0. auto. inversion H0; clear H0; subst chunk. simpl in *. destruct (Int.eq n Int.zero); subst n; reflexivity. - destruct sz; inversion H0; clear H0; subst chunk; simpl in *; congruence. + inv H0; auto. + inv H0; auto. inv H0; auto. inv H0; auto. inv H0; auto. @@ -327,7 +319,6 @@ Lemma cast_val_casted: Proof. intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto. destruct sz; congruence. - congruence. unfold proj_sumbool; repeat rewrite dec_eq_true; auto. unfold proj_sumbool; repeat rewrite dec_eq_true; auto. Qed. @@ -373,7 +364,8 @@ Proof. destruct (classify_cast (typeof a) tto); auto. destruct v1; inv H0; auto. destruct sz2; auto. destruct v1; inv H0; auto. - destruct sz2; auto. destruct v1; inv H0; auto. + destruct v1; inv H0; auto. + destruct v1; inv H0; auto. destruct v1; inv H0; auto. destruct v1; try discriminate. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto. @@ -1416,6 +1408,7 @@ Proof. (* const *) exists (Vint i); split; auto. constructor. exists (Vfloat f0); split; auto. constructor. + exists (Vsingle f0); split; auto. constructor. exists (Vlong i); split; auto. constructor. (* tempvar *) exploit me_temps; eauto. intros [[tv [A B]] C]. -- cgit v1.2.3