From 688adfa1f614a390a2835b62dfecfec685ee3b35 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 10 Jan 2021 12:18:05 +0100 Subject: fix for KVX --- kvx/ValueAOpSSA.v | 326 ++++-------------------------------------------------- 1 file changed, 19 insertions(+), 307 deletions(-) diff --git a/kvx/ValueAOpSSA.v b/kvx/ValueAOpSSA.v index 85d39c0d..8b76f77e 100644 --- a/kvx/ValueAOpSSA.v +++ b/kvx/ValueAOpSSA.v @@ -15,89 +15,7 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats Values Memory Globalenvs. -Require Import Op SSA ValueDomainSSA. -Require Import ExtFloats ExtValues. - -Definition intoffloat_total (x: aval) := - match x with - | F f => - match Float.to_int f with - | Some i => I i - | None => ntop - end - | _ => ntop1 x - end. - -Definition intuoffloat_total (x: aval) := - match x with - | F f => - match Float.to_intu f with - | Some i => I i - | None => ntop - end - | _ => ntop1 x - end. - -Definition intofsingle_total (x: aval) := - match x with - | FS f => - match Float32.to_int f with - | Some i => I i - | None => ntop - end - | _ => ntop1 x - end. - -Definition intuofsingle_total (x: aval) := - match x with - | FS f => - match Float32.to_intu f with - | Some i => I i - | None => ntop - end - | _ => ntop1 x - end. - -Definition longoffloat_total (x: aval) := - match x with - | F f => - match Float.to_long f with - | Some i => L i - | None => ntop - end - | _ => ntop1 x - end. - -Definition longuoffloat_total (x: aval) := - match x with - | F f => - match Float.to_longu f with - | Some i => L i - | None => ntop - end - | _ => ntop1 x - end. - -Definition longofsingle_total (x: aval) := - match x with - | FS f => - match Float32.to_long f with - | Some i => L i - | None => ntop - end - | _ => ntop1 x - end. - -Definition longuofsingle_total (x: aval) := - match x with - | FS f => - match Float32.to_longu f with - | Some i => L i - | None => ntop - end - | _ => ntop1 x - end. - +Require Import Op ExtValues ExtFloats RTL ValueDomainSSA. Definition minf := binop_float ExtFloat.min. Definition maxf := binop_float ExtFloat.max. Definition minfs := binop_single ExtFloat32.min. @@ -153,7 +71,7 @@ Definition eval_static_addressing (addr: addressing) (vl: list aval): aval := | Aindexed2, v1::v2::nil => addl v1 v2 | Aindexed2XS scale, v1::v2::nil => addl v1 (shll v2 (I (Int.repr scale))) | Aglobal s ofs, nil => Ptr (Gl s ofs) - | Ainstack ofs, nil => Vtop + | Ainstack ofs, nil => Ptr (Stk ofs) | _, _ => Vbot end. @@ -246,7 +164,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ofloatconst n, nil => if propagate_float_constants tt then F n else ntop | Osingleconst n, nil => if propagate_float_constants tt then FS n else ntop | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs) - | Oaddrstack ofs, nil => Vtop + | Oaddrstack ofs, nil => Ptr (Stk ofs) | Ocast8signed, v1 :: nil => sign_ext 8 v1 | Ocast16signed, v1 :: nil => sign_ext 16 v1 | Oadd, v1::v2::nil => add v1 v2 @@ -396,200 +314,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := Section SOUNDNESS. Variable bc: block_classification. -Variable ge: genv. +Variable ge: SSA.genv. Hypothesis GENV: genv_match bc ge. Variable sp: block. -Hypothesis STACK: bc sp <> BCinvalid. - -Lemma intoffloat_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.intoffloat v)) (intoffloat_total x). -Proof. - unfold Val.intoffloat, intoffloat_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve intoffloat_total_sound : va. - -Lemma intuoffloat_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.intuoffloat v)) (intuoffloat_total x). -Proof. - unfold Val.intoffloat, intoffloat_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve intuoffloat_total_sound : va. - -Lemma intofsingle_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.intofsingle v)) (intofsingle_total x). -Proof. - unfold Val.intofsingle, intofsingle_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float32.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve intofsingle_total_sound : va. - -Lemma intuofsingle_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.intuofsingle v)) (intuofsingle_total x). -Proof. - unfold Val.intofsingle, intofsingle_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float32.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve intuofsingle_total_sound : va. - -Lemma singleofint_total_sound: - forall v x, vmatch bc v x -> - vmatch bc (Val.maketotal (Val.singleofint v)) (singleofint x). -Proof. - unfold Val.singleofint, singleofint; intros. - inv H; simpl. - all: auto with va. - all: unfold ntop1, provenance. - all: try constructor. -Qed. - -Hint Resolve singleofint_total_sound : va. - -Lemma singleofintu_total_sound: - forall v x, vmatch bc v x -> - vmatch bc (Val.maketotal (Val.singleofintu v)) (singleofintu x). -Proof. - unfold Val.singleofintu, singleofintu; intros. - inv H; simpl. - all: auto with va. - all: unfold ntop1, provenance. - all: try constructor. -Qed. - -Hint Resolve singleofintu_total_sound : va. - -Lemma longoffloat_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.longoffloat v)) (longoffloat_total x). -Proof. - unfold Val.longoffloat, longoffloat_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve longoffloat_total_sound : va. - -Lemma longuoffloat_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.longuoffloat v)) (longuoffloat_total x). -Proof. - unfold Val.longoffloat, longoffloat_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve longuoffloat_total_sound : va. - -Lemma longofsingle_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.longofsingle v)) (longofsingle_total x). -Proof. - unfold Val.longofsingle, longofsingle_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float32.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve longofsingle_total_sound : va. - -Lemma longuofsingle_total_sound: - forall v x - (MATCH : vmatch bc v x), - vmatch bc (Val.maketotal (Val.longuofsingle v)) (longuofsingle_total x). -Proof. - unfold Val.longofsingle, longofsingle_total. intros. - inv MATCH; simpl in *; try constructor. - all: destruct (Float32.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor]. - unfold ntop1, provenance. - destruct (va_strict tt); constructor. -Qed. - -Hint Resolve longuofsingle_total_sound : va. - -Lemma singleoflong_total_sound: - forall v x, vmatch bc v x -> - vmatch bc (Val.maketotal (Val.singleoflong v)) (singleoflong x). -Proof. - unfold Val.singleoflong, singleoflong; intros. - inv H; simpl. - all: auto with va. - all: unfold ntop1, provenance. - all: try constructor. -Qed. - -Hint Resolve singleoflong_total_sound : va. - -Lemma singleoflongu_total_sound: - forall v x, vmatch bc v x -> - vmatch bc (Val.maketotal (Val.singleoflongu v)) (singleoflongu x). -Proof. - unfold Val.singleoflongu, singleoflongu; intros. - inv H; simpl. - all: auto with va. - all: unfold ntop1, provenance. - all: try constructor. -Qed. - -Hint Resolve singleoflongu_total_sound : va. - -Lemma floatoflong_total_sound: - forall v x, vmatch bc v x -> - vmatch bc (Val.maketotal (Val.floatoflong v)) (floatoflong x). -Proof. - unfold Val.floatoflong, floatoflong; intros. - inv H; simpl. - all: auto with va. - all: unfold ntop1, provenance. - all: try constructor. -Qed. - -Hint Resolve floatoflong_total_sound : va. - -Lemma floatoflongu_total_sound: - forall v x, vmatch bc v x -> - vmatch bc (Val.maketotal (Val.floatoflongu v)) (floatoflongu x). -Proof. - unfold Val.floatoflongu, floatoflongu; intros. - inv H; simpl. - all: auto with va. - all: unfold ntop1, provenance. - all: try constructor. -Qed. - -Hint Resolve floatoflongu_total_sound : va. +Hypothesis STACK: bc sp = BCstack. Lemma minf_sound: forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y). @@ -621,7 +349,7 @@ Proof. intros v x; intro MATCH; inversion MATCH; - simpl; + cbn; constructor. Qed. @@ -633,9 +361,9 @@ Lemma triple_op_float_sound: Proof. intros until z. intros Hax Hby Hcz. - inv Hax; simpl; try constructor; - inv Hby; simpl; try constructor; - inv Hcz; simpl; try constructor. + inv Hax; cbn; try constructor; + inv Hby; cbn; try constructor; + inv Hcz; cbn; try constructor. Qed. Lemma triple_op_single_sound: @@ -646,9 +374,9 @@ Lemma triple_op_single_sound: Proof. intros until z. intros Hax Hby Hcz. - inv Hax; simpl; try constructor; - inv Hby; simpl; try constructor; - inv Hcz; simpl; try constructor. + inv Hax; cbn; try constructor; + inv Hby; cbn; try constructor; + inv Hcz; cbn; try constructor. Qed. Lemma fmaddf_sound : @@ -692,9 +420,9 @@ Proof. intros until aargs; intros VM. inv VM. destruct cond; auto with va. inv H0. - destruct cond; simpl; eauto with va. + destruct cond; cbn; eauto with va. inv H2. - destruct cond; simpl; eauto with va. + destruct cond; cbn; eauto with va. destruct cond; auto with va. Qed. @@ -704,7 +432,7 @@ Theorem eval_static_condition0_sound: cmatch (eval_condition0 cond varg m) (eval_static_condition0 cond aarg). Proof. intros until aarg; intro VM. - destruct cond; simpl; eauto with va. + destruct cond; cbn; eauto with va. Qed. Lemma symbol_address_sound: @@ -744,7 +472,6 @@ Proof. unfold eval_addressing, eval_static_addressing; intros; destruct addr; InvHyps; eauto with va. rewrite Ptrofs.add_zero_l; eauto with va. - constructor; constructor; auto. Qed. Theorem eval_static_addressing_sound_none: @@ -796,7 +523,6 @@ Proof. - destruct (propagate_float_constants tt); constructor. - destruct (propagate_float_constants tt); constructor. - rewrite Ptrofs.add_zero_l; eauto with va. - constructor; constructor; auto. - replace(match Val.shl a1 (Vint (int_of_shift1_4 shift)) with | Vint n2 => Vint (Int.add n n2) | Vptr b2 ofs2 => @@ -815,19 +541,9 @@ Proof. + eauto with va. + destruct n; destruct shift; reflexivity. - (* shrx *) - inv H1; simpl; try constructor. - all: destruct Int.ltu; [simpl | constructor; fail]. + inv H1; cbn; try constructor. + all: destruct Int.ltu; [cbn | constructor; fail]. all: auto with va. - - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with - | Vlong n2 => Vlong (Int64.add n n2) - | Vptr b2 ofs2 => - if Archi.ptr64 - then Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int64 n)) - else Vundef - | _ => Vundef - end) with (Val.addl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))). - + eauto with va. - + destruct a1; destruct shift; reflexivity. - inv H1; constructor. - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with | Vlong n2 => Vlong (Int64.sub n n2) @@ -835,10 +551,6 @@ Proof. end) with (Val.subl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))). + eauto with va. + destruct a1; destruct shift; reflexivity. - - (* shrxl *) - inv H1; simpl; try constructor. - all: destruct Int.ltu; [simpl | constructor; fail]. - all: auto with va. - apply of_optbool_sound. eapply eval_static_condition_sound; eauto. (* extfz *) @@ -868,12 +580,12 @@ Proof. (* insf *) - unfold insf, eval_static_insf. destruct (is_bitfield _ _). - + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + inv H1; inv H0; cbn; try constructor; destruct (Int.ltu _ _); cbn; constructor. + constructor. (* insfl *) - unfold insfl, eval_static_insfl. destruct (is_bitfieldl _ _). - + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + inv H1; inv H0; cbn; try constructor; destruct (Int.ltu _ _); cbn; constructor. + constructor. (* select *) - apply select_sound; auto. eapply eval_static_condition0_sound; eauto. -- cgit