From a3924f657b36abfad0448d0fe7d30fd40e0068de Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 12 Dec 2021 22:10:22 +0100 Subject: some more fixed etc. constructs --- backend/ValueDomain.v | 156 ++++++++++++++++++++++++++++++++++++++++ kvx/Asmblockdeps.v | 4 ++ kvx/NeedOp.v | 2 + kvx/Op.v | 30 ++++++++ kvx/PostpassSchedulingOracle.ml | 19 ++--- kvx/ValueAOp.v | 4 ++ 6 files changed, 206 insertions(+), 9 deletions(-) diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 5a7cfc12..8c58e32e 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2269,6 +2269,24 @@ Proof. inv H; simpl; auto with va. rewrite E; constructor. Qed. +Definition intofsingle_ne (x: aval) := + match x with + | FS f => + match Float32.to_int_ne f with + | Some i => I i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma intofsingle_ne_sound: + forall v x w, vmatch v x -> Val.intofsingle_ne v = Some w -> vmatch w (intofsingle_ne x). +Proof. + unfold Val.intofsingle_ne; intros. destruct v; try discriminate. + destruct (Float32.to_int_ne f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + Definition intuofsingle (x: aval) := match x with | FS f => @@ -2287,6 +2305,24 @@ Proof. inv H; simpl; auto with va. rewrite E; constructor. Qed. +Definition intuofsingle_ne (x: aval) := + match x with + | FS f => + match Float32.to_intu_ne f with + | Some i => I i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma intuofsingle_ne_sound: + forall v x w, vmatch v x -> Val.intuofsingle_ne v = Some w -> vmatch w (intuofsingle_ne x). +Proof. + unfold Val.intuofsingle_ne; intros. destruct v; try discriminate. + destruct (Float32.to_intu_ne f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + Definition singleofint (x: aval) := match x with | I i => FS(Float32.of_int i) @@ -2349,6 +2385,42 @@ Proof. inv H; simpl; auto with va. rewrite E; constructor. Qed. +Definition longoffloat_ne (x: aval) := + match x with + | F f => + match Float.to_long_ne f with + | Some i => L i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma longoffloat_ne_sound: + forall v x w, vmatch v x -> Val.longoffloat_ne v = Some w -> vmatch w (longoffloat_ne x). +Proof. + unfold Val.longoffloat_ne; intros. destruct v; try discriminate. + destruct (Float.to_long_ne f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + +Definition longuoffloat_ne (x: aval) := + match x with + | F f => + match Float.to_longu_ne f with + | Some i => L i + | None => if va_strict tt then Vbot else ntop + end + | _ => ntop1 x + end. + +Lemma longuoffloat_ne_sound: + forall v x w, vmatch v x -> Val.longuoffloat_ne v = Some w -> vmatch w (longuoffloat_ne x). +Proof. + unfold Val.longuoffloat_ne; intros. destruct v; try discriminate. + destruct (Float.to_longu_ne f) as [i|] eqn:E; simpl in H0; inv H0. + inv H; simpl; auto with va. rewrite E; constructor. +Qed. + Definition floatoflong (x: aval) := match x with | L i => F(Float.of_long i) @@ -2566,6 +2638,46 @@ Definition longuofsingle_total (x: aval) := | _ => ntop1 x end. +Definition intofsingle_ne_total (x: aval) := + match x with + | FS f => + match Float32.to_int_ne f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition intuofsingle_ne_total (x: aval) := + match x with + | FS f => + match Float32.to_intu_ne f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longoffloat_ne_total (x: aval) := + match x with + | F f => + match Float.to_long_ne f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longuoffloat_ne_total (x: aval) := + match x with + | F f => + match Float.to_longu_ne f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + Lemma intoffloat_total_sound: forall v x (MATCH : vmatch v x), @@ -2606,6 +2718,26 @@ Proof. all: destruct (Float32.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor]. Qed. +Lemma intofsingle_ne_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (Val.maketotal (Val.intofsingle_ne v)) (intofsingle_ne_total x). +Proof. + unfold Val.intofsingle_ne, intofsingle_ne_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_int_ne f) as [i|] eqn:E; simpl; [auto with va | constructor]. +Qed. + +Lemma intuofsingle_ne_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (Val.maketotal (Val.intuofsingle_ne v)) (intuofsingle_ne_total x). +Proof. + unfold Val.intofsingle, intofsingle_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_intu_ne f) as [i|] eqn:E; simpl; [auto with va | constructor]. +Qed. + Lemma singleofint_total_sound: forall v x, vmatch v x -> vmatch (Val.maketotal (Val.singleofint v)) (singleofint x). @@ -2648,6 +2780,26 @@ Proof. all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor]. Qed. +Lemma longoffloat_ne_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (Val.maketotal (Val.longoffloat_ne v)) (longoffloat_ne_total x). +Proof. + unfold Val.longoffloat_ne, longoffloat_ne_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_long_ne f) as [i|] eqn:E; simpl; [auto with va | constructor]. +Qed. + +Lemma longuoffloat_ne_total_sound: + forall v x + (MATCH : vmatch v x), + vmatch (Val.maketotal (Val.longuoffloat_ne v)) (longuoffloat_ne_total x). +Proof. + unfold Val.longoffloat_ne, longoffloat_ne_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_longu_ne f) as [i|] eqn:E; simpl; [auto with va | constructor]. +Qed. + Lemma longofsingle_total_sound: forall v x (MATCH : vmatch v x), @@ -5200,6 +5352,10 @@ Global Hint Resolve cnot_sound symbol_address_sound intofsingle_sound intuofsingle_sound singleofint_sound singleofintu_sound longoffloat_sound longuoffloat_sound floatoflong_sound floatoflongu_sound longofsingle_sound longuofsingle_sound singleoflong_sound singleoflongu_sound + intofsingle_ne_sound intuofsingle_ne_sound + longoffloat_ne_sound longuoffloat_ne_sound + intofsingle_ne_total_sound intuofsingle_ne_total_sound + longoffloat_ne_total_sound longuoffloat_ne_total_sound longofwords_sound loword_sound hiword_sound intoffloat_total_sound intuoffloat_total_sound diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v index a9786e0a..ac0b359e 100644 --- a/kvx/Asmblockdeps.v +++ b/kvx/Asmblockdeps.v @@ -1537,6 +1537,10 @@ Definition string_of_name_rr (n: arith_name_rr): pstring := | Pfixedudrzz => "Pfixedudrzz" | Pfixeddrzz_i32 => "Pfixeddrzz_i32" | Pfixedudrzz_i32 => "Pfixedudrzz_i32" + | Pfixedwrne => "Pfixedwrne" + | Pfixeduwrne => "Pfixeduwrne" + | Pfixeddrne => "Pfixeddrne" + | Pfixedudrne => "Pfixedudrne" end. Definition string_of_name_ri32 (n: arith_name_ri32): pstring := diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v index 4578b4e8..455af70e 100644 --- a/kvx/NeedOp.v +++ b/kvx/NeedOp.v @@ -131,6 +131,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => op1 (default nv) | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv) + | Ointofsingle_ne | Ointuofsingle_ne => op1 (default nv) + | Olongoffloat_ne | Olonguoffloat_ne => op1 (default nv) | Ocmp c => needs_of_condition c | Oextfz _ _ | Oextfs _ _ | Oextfzl _ _ | Oextfsl _ _ => op1 (default nv) | Oinsf _ _ | Oinsfl _ _ => op2 (default nv) diff --git a/kvx/Op.v b/kvx/Op.v index 4458adb3..8549fc38 100644 --- a/kvx/Op.v +++ b/kvx/Op.v @@ -209,6 +209,11 @@ Inductive operation : Type := | Olonguofsingle (**r [rd = unsigned_long_of_float32(r1)] *) | Osingleoflong (**r [rd = float32_of_signed_long(r1)] *) | Osingleoflongu (**r [rd = float32_of_unsigned_int(r1)] *) + | Ointofsingle_ne (**r [rd = signed_int_of_float64(r1)] *) + | Ointuofsingle_ne (**r [rd = unsigned_int_of_float64(r1)] *) + | Olongoffloat_ne (**r [rd = signed_long_of_float64(r1)] *) + | Olonguoffloat_ne (**r [rd = unsigned_long_of_float64(r1)] *) + (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) | Oextfz (stop : Z) (start : Z) @@ -466,6 +471,11 @@ Definition eval_operation | Olonguofsingle, v1::nil => Some (Val.maketotal (Val.longuofsingle v1)) | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1)) | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1)) + | Ointofsingle_ne, v1::nil => Some (Val.maketotal (Val.intofsingle_ne v1)) + | Ointuofsingle_ne, v1::nil => Some (Val.maketotal (Val.intuofsingle_ne v1)) + | Olongoffloat_ne, v1::nil => Some (Val.maketotal (Val.longoffloat_ne v1)) + | Olonguoffloat_ne, v1::nil => Some (Val.maketotal (Val.longuoffloat_ne v1)) + | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) | (Oextfz stop start), v0::nil => Some (extfz stop start v0) | (Oextfs stop start), v0::nil => Some (extfs stop start v0) @@ -683,6 +693,12 @@ Definition type_of_operation (op: operation) : list typ * typ := | Olonguofsingle => (Tsingle :: nil, Tlong) | Osingleoflong => (Tlong :: nil, Tsingle) | Osingleoflongu => (Tlong :: nil, Tsingle) + + | Ointofsingle_ne => (Tsingle :: nil, Tint) + | Ointuofsingle_ne => (Tsingle :: nil, Tint) + | Olongoffloat_ne => (Tfloat :: nil, Tlong) + | Olonguoffloat_ne => (Tfloat :: nil, Tlong) + | Ocmp c => (type_of_condition c, Tint) | Oextfz _ _ | Oextfs _ _ => (Tint :: nil, Tint) | Oextfzl _ _ | Oextfsl _ _ => (Tlong :: nil, Tlong) @@ -980,6 +996,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* singleoflong, singleoflongu *) - destruct v0; cbn... - destruct v0; cbn... + (* intofsingle_ne, intuofsingle_ne *) + - destruct v0; cbn... destruct (Float32.to_int_ne f); cbn; trivial. + - destruct v0; cbn... destruct (Float32.to_intu_ne f); cbn; trivial. + (* longoffloat_ne, longuoffloat_ne *) + - destruct v0; cbn... destruct (Float.to_long_ne f); cbn; trivial. + - destruct v0; cbn... destruct (Float.to_longu_ne f); cbn; trivial. (* cmp *) - destruct (eval_condition cond vl m)... destruct b... (* extfz *) @@ -1669,6 +1691,14 @@ Proof. (* singleoflong, singleoflongu *) - inv H4; cbn; auto. - inv H4; cbn; auto. + + (* intofsingle_ne, intuofsingle_ne *) + - inv H4; cbn; auto. destruct (Float32.to_int_ne f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float32.to_intu_ne f0); cbn; auto. + (* longoffloat_ne, longuoffloat_ne *) + - inv H4; cbn; auto. destruct (Float.to_long_ne f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float.to_longu_ne f0); cbn; auto. + (* cmp *) - subst v1. destruct (eval_condition cond vl1 m1) eqn:?. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. diff --git a/kvx/PostpassSchedulingOracle.ml b/kvx/PostpassSchedulingOracle.ml index 3f4520a6..f53da14b 100644 --- a/kvx/PostpassSchedulingOracle.ml +++ b/kvx/PostpassSchedulingOracle.ml @@ -47,7 +47,8 @@ type real_instruction = | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw | Fmind | Fminw | Fmaxd | Fmaxw | Finvw | Ffmaw | Ffmad | Ffmsw | Ffmsd - | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeduwz | Fixeddz | Fixedudz + | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz + | Fixedw | Fixeduw | Fixedd | Fixedud | Fcompw | Fcompd type ab_inst_rec = { @@ -86,12 +87,12 @@ let arith_rr_real = function | Pfloatuwrnsz -> Floatuwz | Pfloatudrnsz -> Floatudz | Pfloatdrnsz -> Floatdz - | Pfixedwrzz -> Fixedwz - | Pfixeduwrzz -> Fixeduwz - | Pfixeddrzz -> Fixeddz - | Pfixedudrzz -> Fixedudz - | Pfixeddrzz_i32 -> Fixeddz - | Pfixedudrzz_i32 -> Fixedudz + | Pfixedwrzz | Pfixedwrne -> Fixedw + | Pfixeduwrzz | Pfixeduwrne -> Fixeduw + | Pfixeddrzz | Pfixeddrne -> Fixedd + | Pfixedudrzz| Pfixedudrne -> Fixedud + | Pfixeddrzz_i32 -> Fixedd + | Pfixedudrzz_i32 -> Fixedud let arith_rrr_real = function | Pcompw it -> Compw @@ -643,7 +644,7 @@ let rec_to_usage r = (* TODO: check *) | Srsw | Srsd | Rorw -> (match encoding with None | Some U6 -> alu_lite | _ -> raise InvalidEncoding) | Extfz | Extfs | Insf -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding) - | Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau + | Fixeduw | Fixedw | Floatwz | Floatuwz | Fixedd | Fixedud | Floatdz | Floatudz -> mau | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> (match encoding with None | Some U6 | Some S10 -> lsu_auxw | Some U27L5 | Some U27L10 -> lsu_auxw_x @@ -681,7 +682,7 @@ let real_inst_to_latency = function | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved | Addxw | Addxd | Fmind | Fmaxd | Fminw | Fmaxw -> 1 - | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 + | Floatwz | Floatuwz | Fixeduw | Fixedw | Floatdz | Floatudz | Fixedd | Fixedud -> 4 | Mulw | Muld | Maddw | Maddd | Msbfw | Msbfd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> 3 | Sb | Sh | Sw | Sd | Sq | So -> 1 (* See kvx-Optimization.pdf page 19 *) diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index 87554258..4909a25b 100644 --- a/kvx/ValueAOp.v +++ b/kvx/ValueAOp.v @@ -298,6 +298,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Olonguofsingle, v1::nil => longuofsingle_total v1 | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 + | Ointofsingle_ne, v1::nil => intofsingle_ne_total v1 + | Ointuofsingle_ne, v1::nil => intuofsingle_ne_total v1 + | Olongoffloat_ne, v1::nil => longoffloat_ne_total v1 + | Olonguoffloat_ne, v1::nil => longuoffloat_ne_total v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) | (Oextfz stop start), v0::nil => eval_static_extfz stop start v0 | (Oextfs stop start), v0::nil => eval_static_extfs stop start v0 -- cgit