diff options
Diffstat (limited to 'kvx/ValueAOp.v')
| -rw-r--r-- | kvx/ValueAOp.v | 313 |
1 files changed, 14 insertions, 299 deletions
diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index e634fdc0..87554258 100644 --- a/kvx/ValueAOp.v +++ b/kvx/ValueAOp.v @@ -16,87 +16,6 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats Values Memory Globalenvs. Require Import Op ExtValues ExtFloats RTL ValueDomain. - -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. - Definition minf := binop_float ExtFloat.min. Definition maxf := binop_float ExtFloat.max. Definition minfs := binop_single ExtFloat32.min. @@ -400,196 +319,6 @@ Hypothesis GENV: genv_match bc ge. Variable sp: block. Hypothesis STACK: bc sp = BCstack. -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. - 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). Proof. @@ -620,7 +349,7 @@ Proof. intros v x; intro MATCH; inversion MATCH; - simpl; + cbn; constructor. Qed. @@ -632,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: @@ -645,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 : @@ -691,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. @@ -703,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: @@ -812,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) @@ -832,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 *) @@ -865,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. |