From b2fc9b55d9c59a9c507786a650377e2f0a1ddad8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 29 Sep 2020 16:22:18 +0200 Subject: simpl -> cbn --- kvx/Op.v | 484 +++++++++++++++++++++++++++++++-------------------------------- 1 file changed, 240 insertions(+), 244 deletions(-) (limited to 'kvx/Op.v') diff --git a/kvx/Op.v b/kvx/Op.v index 544bb081..e2ffa3e5 100644 --- a/kvx/Op.v +++ b/kvx/Op.v @@ -508,9 +508,9 @@ Qed. Ltac FuncInv := match goal with | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ => - destruct x; simpl in H; FuncInv + destruct x; cbn in H; FuncInv | H: (match ?v with Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ _ => _ end = Some _) |- _ => - destruct v; simpl in H; FuncInv + destruct v; cbn in H; FuncInv | H: (if Archi.ptr64 then _ else _) = Some _ |- _ => destruct Archi.ptr64 eqn:?; FuncInv | H: (Some _ = Some _) |- _ => @@ -727,27 +727,27 @@ Qed. Remark type_sub: forall v1 v2, Val.has_type (Val.sub v1 v2) Tint. Proof. - intros. unfold Val.has_type, Val.sub. destruct Archi.ptr64, v1, v2; simpl; auto. + intros. unfold Val.has_type, Val.sub. destruct Archi.ptr64, v1, v2; cbn; auto. destruct (eq_block _ _); auto. Qed. Remark type_subl: forall v1 v2, Val.has_type (Val.subl v1 v2) Tlong. Proof. - intros. unfold Val.has_type, Val.subl. destruct Archi.ptr64, v1, v2; simpl; auto. + intros. unfold Val.has_type, Val.subl. destruct Archi.ptr64, v1, v2; cbn; auto. destruct (eq_block _ _); auto. Qed. Remark type_shl: forall v1 v2, Val.has_type (Val.shl v1 v2) Tint. Proof. - destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial. + destruct v1, v2; cbn; trivial; destruct (Int.ltu _ _); cbn; trivial. Qed. Remark type_shll: forall v1 v2, Val.has_type (Val.shll v1 v2) Tlong. Proof. - destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial. + destruct v1, v2; cbn; trivial; destruct (Int.ltu _ _); cbn; trivial. Qed. Lemma type_of_operation_sound: @@ -757,7 +757,7 @@ Lemma type_of_operation_sound: Val.has_type v (snd (type_of_operation op)). Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). intros. - destruct op; simpl; simpl in H0; FuncInv; subst; simpl. + destruct op; cbn; cbn in H0; FuncInv; subst; cbn. (* move *) - congruence. (* intconst, longconst, floatconst, singleconst *) @@ -777,30 +777,30 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - apply type_add. (* addx, addximm *) - apply type_add. - - destruct v0; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + - destruct v0; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. (* neg, sub *) - destruct v0... - apply type_sub. (* revsubimm, revsubx, revsubximm *) - destruct v0... - apply type_sub. - - destruct v0; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + - destruct v0; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. (* mul, mulimm, mulhs, mulhu *) - destruct v0; destruct v1... - destruct v0... - destruct v0; destruct v1... - destruct v0; destruct v1... (* div, divu *) - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2... - - destruct v0; destruct v1; simpl in *; inv H0. + - destruct v0; destruct v1; cbn in *; inv H0. + destruct (_ || _); inv H2... + - destruct v0; destruct v1; cbn in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2... (* mod, modu *) - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2... - - destruct v0; destruct v1; simpl in *; inv H0. + - destruct v0; destruct v1; cbn in *; inv H0. + destruct (_ || _); inv H2... + - destruct v0; destruct v1; cbn in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2... (* and, andimm *) - destruct v0; destruct v1... @@ -829,18 +829,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1... - destruct v0... (* shl, shlimm *) - - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... - - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)... + - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int.iwordsize)... + - destruct v0; cbn... destruct (Int.ltu n Int.iwordsize)... (* shr, shrimm *) - - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... - - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)... + - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int.iwordsize)... + - destruct v0; cbn... destruct (Int.ltu n Int.iwordsize)... (* shru, shruimm *) - - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... - - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)... + - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int.iwordsize)... + - destruct v0; cbn... destruct (Int.ltu n Int.iwordsize)... (* shrx *) - - destruct v0; simpl... destruct (Int.ltu n (Int.repr 31)); simpl; trivial. + - destruct v0; cbn... destruct (Int.ltu n (Int.repr 31)); cbn; trivial. (* shrimm *) - - destruct v0; simpl... + - destruct v0; cbn... (* madd *) - apply type_add. - apply type_add. @@ -858,13 +858,13 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - apply type_addl. (* addxl addxlimm *) - apply type_addl. - - destruct v0; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + - destruct v0; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. (* negl, subl *) - destruct v0... - apply type_subl. - - destruct v0; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + - destruct v0; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. - destruct v0... - apply type_subl. (* mull, mullhs, mullhu *) @@ -873,14 +873,14 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1... - destruct v0; destruct v1... (* divl, divlu *) - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2... - - destruct v0; destruct v1; simpl in *; inv H0. + - destruct v0; destruct v1; cbn in *; inv H0. + destruct (_ || _); inv H2... + - destruct v0; destruct v1; cbn in *; inv H0. destruct (Int64.eq i0 Int64.zero); inv H2... (* modl, modlu *) - - destruct v0; destruct v1; simpl in *; inv H0. - destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2... - - destruct v0; destruct v1; simpl in *; inv H0. + - destruct v0; destruct v1; cbn in *; inv H0. + destruct (_ || _); inv H2... + - destruct v0; destruct v1; cbn in *; inv H0. destruct (Int64.eq i0 Int64.zero); inv H2... (* andl, andlimm *) - destruct v0; destruct v1... @@ -909,16 +909,16 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1... - destruct v0... (* shll, shllimm *) - - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... - - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... + - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int64.iwordsize')... + - destruct v0; cbn... destruct (Int.ltu n Int64.iwordsize')... (* shr, shrimm *) - - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... - - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... + - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int64.iwordsize')... + - destruct v0; cbn... destruct (Int.ltu n Int64.iwordsize')... (* shru, shruimm *) - - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... - - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... + - destruct v0; destruct v1; cbn... destruct (Int.ltu i0 Int64.iwordsize')... + - destruct v0; cbn... destruct (Int.ltu n Int64.iwordsize')... (* shrxl *) - - destruct v0; simpl... destruct (Int.ltu n (Int.repr 63)); simpl; trivial. + - destruct v0; cbn... destruct (Int.ltu n (Int.repr 63)); cbn; trivial. (* maddl, maddlim *) - apply type_addl. - apply type_addl. @@ -960,59 +960,59 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0... - destruct v0... (* intoffloat, intuoffloat *) - - destruct v0; simpl... destruct (Float.to_int f); simpl; trivial. - - destruct v0; simpl... destruct (Float.to_intu f); simpl; trivial. + - destruct v0; cbn... destruct (Float.to_int f); cbn; trivial. + - destruct v0; cbn... destruct (Float.to_intu f); cbn; trivial. (* intofsingle, intuofsingle *) - - destruct v0; simpl... destruct (Float32.to_int f); simpl; trivial. - - destruct v0; simpl... destruct (Float32.to_intu f); simpl; trivial. + - destruct v0; cbn... destruct (Float32.to_int f); cbn; trivial. + - destruct v0; cbn... destruct (Float32.to_intu f); cbn; trivial. (* singleofint, singleofintu *) - - destruct v0; simpl... - - destruct v0; simpl... + - destruct v0; cbn... + - destruct v0; cbn... (* longoffloat, longuoffloat *) - - destruct v0; simpl... destruct (Float.to_long f); simpl; trivial. - - destruct v0; simpl... destruct (Float.to_longu f); simpl; trivial. + - destruct v0; cbn... destruct (Float.to_long f); cbn; trivial. + - destruct v0; cbn... destruct (Float.to_longu f); cbn; trivial. (* floatoflong, floatoflongu *) - - destruct v0; simpl... - - destruct v0; simpl... + - destruct v0; cbn... + - destruct v0; cbn... (* longofsingle, longuofsingle *) - - destruct v0; simpl... destruct (Float32.to_long f); simpl; trivial. - - destruct v0; simpl... destruct (Float32.to_longu f); simpl; trivial. + - destruct v0; cbn... destruct (Float32.to_long f); cbn; trivial. + - destruct v0; cbn... destruct (Float32.to_longu f); cbn; trivial. (* singleoflong, singleoflongu *) - - destruct v0; simpl... - - destruct v0; simpl... + - destruct v0; cbn... + - destruct v0; cbn... (* cmp *) - destruct (eval_condition cond vl m)... destruct b... (* extfz *) - unfold extfz. destruct (is_bitfield _ _). - + destruct v0; simpl; trivial. + + destruct v0; cbn; trivial. + constructor. (* extfs *) - unfold extfs. destruct (is_bitfield _ _). - + destruct v0; simpl; trivial. + + destruct v0; cbn; trivial. + constructor. (* extfzl *) - unfold extfzl. destruct (is_bitfieldl _ _). - + destruct v0; simpl; trivial. + + destruct v0; cbn; trivial. + constructor. (* extfsl *) - unfold extfsl. destruct (is_bitfieldl _ _). - + destruct v0; simpl; trivial. + + destruct v0; cbn; trivial. + constructor. (* insf *) - unfold insf, bitfield_mask. destruct (is_bitfield _ _). - + destruct v0; destruct v1; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + + destruct v0; destruct v1; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. + constructor. (* insf *) - unfold insfl, bitfield_mask. destruct (is_bitfieldl _ _). - + destruct v0; destruct v1; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + + destruct v0; destruct v1; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. + constructor. (* Osel *) - unfold Val.select. destruct (eval_condition0 _ _ m). @@ -1047,7 +1047,7 @@ Lemma is_trapping_op_sound: eval_operation genv sp op vl m <> None. Proof. unfold args_of_operation. - destruct op; destruct eq_operation; intros; simpl in *; try congruence. + destruct op; destruct eq_operation; intros; cbn in *; try congruence. all: try (destruct vl as [ | vh1 vl1]; try discriminate). all: try (destruct vl1 as [ | vh2 vl2]; try discriminate). all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). @@ -1101,7 +1101,7 @@ Lemma eval_negate_condition: forall cond vl m, eval_condition (negate_condition cond) vl m = option_map negb (eval_condition cond vl m). Proof. - intros. destruct cond; simpl. + intros. destruct cond; cbn. repeat (destruct vl; auto). apply Val.negate_cmp_bool. repeat (destruct vl; auto). apply Val.negate_cmpu_bool. repeat (destruct vl; auto). apply Val.negate_cmp_bool. @@ -1147,7 +1147,7 @@ Lemma eval_shift_stack_addressing: eval_addressing ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl = eval_addressing ge (Vptr sp (Ptrofs.repr delta)) addr vl. Proof. - intros. destruct addr; simpl; auto. destruct vl; auto. + intros. destruct addr; cbn; auto. destruct vl; auto. rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto. Qed. @@ -1156,7 +1156,7 @@ Lemma eval_shift_stack_operation: eval_operation ge (Vptr sp Ptrofs.zero) (shift_stack_operation delta op) vl m = eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m. Proof. - intros. destruct op; simpl; auto. destruct vl; auto. + intros. destruct op; cbn; auto. destruct vl; auto. rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto. Qed. @@ -1183,12 +1183,12 @@ Proof. assert (A: forall x n, Val.offset_ptr x (Ptrofs.add n (Ptrofs.repr delta)) = Val.add (Val.offset_ptr x n) (Vint (Int.repr delta))). - { intros; destruct x; simpl; auto. rewrite H1. + { intros; destruct x; cbn; auto. rewrite H1. rewrite Ptrofs.add_assoc. f_equal; f_equal; f_equal. symmetry; auto with ptrofs. } - destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst. + destruct addr; cbn in H; inv H; cbn in *; FuncInv; subst. - rewrite A; auto. - unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. - simpl. rewrite H1. f_equal; f_equal; f_equal. symmetry; auto with ptrofs. + cbn. rewrite H1. f_equal; f_equal; f_equal. symmetry; auto with ptrofs. - rewrite A; auto. Qed. @@ -1223,17 +1223,17 @@ Lemma op_depends_on_memory_correct: op_depends_on_memory op = false -> eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. - intros until m2. destruct op; simpl; try congruence. - - destruct cond; simpl; try congruence; + intros until m2. destruct op; cbn; try congruence. + - destruct cond; cbn; try congruence; intros SF; auto; rewrite ? negb_false_iff in SF; unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. - - destruct c0; simpl; try congruence; + - destruct c0; cbn; try congruence; intros SF; auto; rewrite ? negb_false_iff in SF; unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. - - destruct c0; simpl; try congruence; + - destruct c0; cbn; try congruence; intros SF; auto; rewrite ? negb_false_iff in SF; unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. - - destruct c0; simpl; try congruence; + - destruct c0; cbn; try congruence; intros SF; auto; rewrite ? negb_false_iff in SF; unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. Qed. @@ -1348,19 +1348,19 @@ Lemma eval_condition_inj: eval_condition cond vl1 m1 = Some b -> eval_condition cond vl2 m2 = Some b. Proof. - intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. + intros. destruct cond; cbn in H0; FuncInv; InvInject; cbn; auto. +- inv H3; inv H2; cbn in H0; inv H0; auto. - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. -- inv H3; simpl in H0; inv H0; auto. +- inv H3; cbn in H0; inv H0; auto. - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. -- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; inv H2; cbn in H0; inv H0; auto. - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. -- inv H3; simpl in H0; inv H0; auto. +- inv H3; cbn in H0; inv H0; auto. - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; inv H2; cbn in H0; inv H0; auto. +- inv H3; inv H2; cbn in H0; inv H0; auto. +- inv H3; inv H2; cbn in H0; inv H0; auto. +- inv H3; inv H2; cbn in H0; inv H0; auto. Qed. Lemma eval_condition0_inj: @@ -1369,10 +1369,10 @@ Lemma eval_condition0_inj: eval_condition0 cond v1 m1 = Some b -> eval_condition0 cond v2 m2 = Some b. Proof. - intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. - - inv H; simpl in *; congruence. + intros. destruct cond; cbn in H0; FuncInv; InvInject; cbn; auto. + - inv H; cbn in *; congruence. - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. - - inv H; simpl in *; congruence. + - inv H; cbn in *; congruence. - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. Qed. @@ -1393,248 +1393,244 @@ Lemma eval_operation_inj: eval_operation ge1 sp1 op vl1 m1 = Some v1 -> exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ Val.inject f v1 v2. Proof. - intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + intros until v1; intros GL; intros. destruct op; cbn in H1; cbn; FuncInv; InvInject; TrivialExists. (* addrsymbol *) - - apply GL; simpl; auto. + - apply GL; cbn; auto. (* addrstack *) - apply Val.offset_ptr_inject; auto. (* castsigned *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* add, addimm *) - apply Val.add_inject; auto. - apply Val.add_inject; auto. (* addx, addximm *) - apply Val.add_inject; trivial. - inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto. - - inv H4; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + inv H4; inv H2; cbn; try destruct (Int.ltu _ _); cbn; auto. + - inv H4; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. (* neg, sub *) - - inv H4; simpl; auto. + - inv H4; cbn; auto. - apply Val.sub_inject; auto. (* revsubimm, revsubx, revsubximm *) - - inv H4; simpl; trivial. + - inv H4; cbn; trivial. - apply Val.sub_inject; trivial. - inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto. - - inv H4; simpl; try destruct (Int.ltu _ _); simpl; auto. + inv H4; inv H2; cbn; try destruct (Int.ltu _ _); cbn; auto. + - inv H4; cbn; try destruct (Int.ltu _ _); cbn; auto. (* mul, mulimm, mulhs, mulhu *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* div, divu *) - - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. + - inv H4; inv H3; cbn in H1; inv H1. cbn. + destruct (_ || _); inv H2. TrivialExists. - - inv H4; inv H3; simpl in H1; inv H1. simpl. + - inv H4; inv H3; cbn in H1; inv H1. cbn. destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. (* mod, modu *) - - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. + - inv H4; inv H3; cbn in H1; inv H1. cbn. + destruct (_ || _); inv H2. TrivialExists. - - inv H4; inv H3; simpl in H1; inv H1. simpl. + - inv H4; inv H3; cbn in H1; inv H1. cbn. destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. (* and, andimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* nand, nandimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* or, orimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* nor, norimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* xor, xorimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* nxor, nxorimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* not *) - - inv H4; simpl; auto. + - inv H4; cbn; auto. (* andn, andnimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* orn, ornimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* shl, shlimm *) - - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. - - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. + - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int.iwordsize); auto. + - inv H4; cbn; auto. destruct (Int.ltu n Int.iwordsize); auto. (* shr, shrimm *) - - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. - - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. + - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int.iwordsize); auto. + - inv H4; cbn; auto. destruct (Int.ltu n Int.iwordsize); auto. (* shru, shruimm *) - - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. - - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. + - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int.iwordsize); auto. + - inv H4; cbn; auto. destruct (Int.ltu n Int.iwordsize); auto. (* shrx *) - - inv H4; simpl; auto. - destruct (Int.ltu n (Int.repr 31)); inv H; simpl; auto. + - inv H4; cbn; auto. + destruct (Int.ltu n (Int.repr 31)); inv H; cbn; auto. (* rorimm *) - - inv H4; simpl; auto. + - inv H4; cbn; auto. (* madd, maddim *) - - inv H2; inv H3; inv H4; simpl; auto. - - inv H2; inv H4; simpl; auto. + - inv H2; inv H3; inv H4; cbn; auto. + - inv H2; inv H4; cbn; auto. (* msub *) - apply Val.sub_inject; auto. - inv H3; inv H2; simpl; auto. + inv H3; inv H2; cbn; auto. (* makelong, highlong, lowlong *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* cast32 *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* addl, addlimm *) - apply Val.addl_inject; auto. - apply Val.addl_inject; auto. (* addxl, addxlimm *) - apply Val.addl_inject; auto. - inv H4; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. - - inv H4; simpl; trivial. - destruct (Int.ltu _ _); simpl; trivial. + inv H4; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. + - inv H4; cbn; trivial. + destruct (Int.ltu _ _); cbn; trivial. (* negl, subl *) - - inv H4; simpl; auto. + - inv H4; cbn; auto. - apply Val.subl_inject; auto. - inv H4; inv H2; simpl; trivial; - destruct (Int.ltu _ _); simpl; trivial. - - inv H4; simpl; trivial; - destruct (Int.ltu _ _); simpl; trivial. - - inv H4; simpl; auto. + inv H4; inv H2; cbn; trivial; + destruct (Int.ltu _ _); cbn; trivial. + - inv H4; cbn; trivial; + destruct (Int.ltu _ _); cbn; trivial. + - inv H4; cbn; auto. - apply Val.subl_inject; auto. (* mull, mullhs, mullhu *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* divl, divlu *) - - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int64.eq i0 Int64.zero - || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. + - inv H4; inv H3; cbn in H1; inv H1. cbn. + destruct (_ || _); inv H2. TrivialExists. - - inv H4; inv H3; simpl in H1; inv H1. simpl. + - inv H4; inv H3; cbn in H1; inv H1. cbn. destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists. (* modl, modlu *) - - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int64.eq i0 Int64.zero - || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. + - inv H4; inv H3; cbn in H1; inv H1. cbn. + destruct (_ || _); inv H2. TrivialExists. - - inv H4; inv H3; simpl in H1; inv H1. simpl. + - inv H4; inv H3; cbn in H1; inv H1. cbn. destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists. (* andl, andlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* nandl, nandlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* orl, orlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* norl, norlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* xorl, xorlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* nxorl, nxorlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* notl *) - - inv H4; simpl; auto. + - inv H4; cbn; auto. (* andnl, andnlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* ornl, ornlimm *) - - inv H4; inv H2; simpl; auto. - - inv H4; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; cbn; auto. (* shll, shllimm *) - - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. - - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. + - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. + - inv H4; cbn; auto. destruct (Int.ltu n Int64.iwordsize'); auto. (* shr, shrimm *) - - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. - - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. + - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. + - inv H4; cbn; auto. destruct (Int.ltu n Int64.iwordsize'); auto. (* shru, shruimm *) - - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. - - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. + - inv H4; inv H2; cbn; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. + - inv H4; cbn; auto. destruct (Int.ltu n Int64.iwordsize'); auto. (* shrx *) - - inv H4; simpl; auto. - destruct (Int.ltu n (Int.repr 63)); simpl; auto. + - inv H4; cbn; auto. + destruct (Int.ltu n (Int.repr 63)); cbn; auto. (* maddl, maddlimm *) - apply Val.addl_inject; auto. - inv H2; inv H3; inv H4; simpl; auto. + inv H2; inv H3; inv H4; cbn; auto. - apply Val.addl_inject; auto. - inv H4; inv H2; simpl; auto. + inv H4; inv H2; cbn; auto. (* msubl, msublimm *) - apply Val.subl_inject; auto. - inv H2; inv H3; inv H4; simpl; auto. + inv H2; inv H3; inv H4; cbn; auto. (* negf, absf *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* addf, subf *) - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* mulf, divf *) - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* minf, maxf *) - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* fmaddf, fmsubf *) - - inv H4; inv H3; inv H2; simpl; auto. - - inv H4; inv H3; inv H2; simpl; auto. + - inv H4; inv H3; inv H2; cbn; auto. + - inv H4; inv H3; inv H2; cbn; auto. (* negfs, absfs *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* addfs, subfs *) - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* mulfs, divfs *) - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* minfs, maxfs *) - - inv H4; inv H2; simpl; auto. - - inv H4; inv H2; simpl; auto. + - inv H4; inv H2; cbn; auto. + - inv H4; inv H2; cbn; auto. (* invfs *) - - inv H4; simpl; auto. + - inv H4; cbn; auto. (* fmaddfs, fmsubfs *) - - inv H4; inv H3; inv H2; simpl; auto. - - inv H4; inv H3; inv H2; simpl; auto. + - inv H4; inv H3; inv H2; cbn; auto. + - inv H4; inv H3; inv H2; cbn; auto. (* singleoffloat, floatofsingle *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* intoffloat, intuoffloat *) - - inv H4; simpl; auto. destruct (Float.to_int f0); simpl; auto. - - inv H4; simpl; auto. destruct (Float.to_intu f0); simpl; auto. + - inv H4; cbn; auto. destruct (Float.to_int f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float.to_intu f0); cbn; auto. (* intofsingle, intuofsingle *) - - inv H4; simpl; auto. destruct (Float32.to_int f0); simpl; auto. - - inv H4; simpl; auto. destruct (Float32.to_intu f0); simpl; auto. + - inv H4; cbn; auto. destruct (Float32.to_int f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float32.to_intu f0); cbn; auto. (* singleofint, singleofintu *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* longoffloat, longuoffloat *) - - inv H4; simpl; auto. destruct (Float.to_long f0); simpl; auto. - - inv H4; simpl; auto. destruct (Float.to_longu f0); simpl; auto. + - inv H4; cbn; auto. destruct (Float.to_long f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float.to_longu f0); cbn; auto. (* floatoflong, floatoflongu *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* longofsingle, longuofsingle *) - - inv H4; simpl; auto. destruct (Float32.to_long f0); simpl; auto. - - inv H4; simpl; auto. destruct (Float32.to_longu f0); simpl; auto. + - inv H4; cbn; auto. destruct (Float32.to_long f0); cbn; auto. + - inv H4; cbn; auto. destruct (Float32.to_longu f0); cbn; auto. (* singleoflong, singleoflongu *) - - inv H4; simpl; auto. - - inv H4; simpl; auto. + - inv H4; cbn; auto. + - inv H4; cbn; auto. (* cmp *) - subst v1. destruct (eval_condition cond vl1 m1) eqn:?. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. - destruct b; simpl; constructor. - simpl; constructor. + destruct b; cbn; constructor. + cbn; constructor. (* extfz *) - unfold extfz. @@ -1664,16 +1660,16 @@ Proof. - unfold insf. destruct (is_bitfield _ _). + inv H4; inv H2; trivial. - simpl. destruct (Int.ltu _ _); trivial. - simpl. trivial. + cbn. destruct (Int.ltu _ _); trivial. + cbn. trivial. + trivial. (* insfl *) - unfold insfl. destruct (is_bitfieldl _ _). + inv H4; inv H2; trivial. - simpl. destruct (Int.ltu _ _); trivial. - simpl. trivial. + cbn. destruct (Int.ltu _ _); trivial. + cbn. trivial. + trivial. (* Osel *) @@ -1711,13 +1707,13 @@ Lemma eval_addressing_inj: eval_addressing ge1 sp1 addr vl1 = Some v1 -> exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. Proof. - intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists. + intros. destruct addr; cbn in H2; cbn; FuncInv; InvInject; TrivialExists. - apply Val.addl_inject; trivial. - destruct v0; destruct v'0; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial; inv H3. + destruct v0; destruct v'0; cbn; trivial; destruct (Int.ltu _ _); cbn; trivial; inv H3. apply Val.inject_long. - apply Val.addl_inject; auto. - apply Val.offset_ptr_inject; auto. - - apply H; simpl; auto. + - apply H; cbn; auto. - apply Val.offset_ptr_inject; auto. Qed. @@ -1732,7 +1728,7 @@ Lemma eval_addressing_inj_none: eval_addressing ge2 sp2 addr vl2 = None. Proof. intros until vl2. intros Hglobal Hinjsp Hinjvl. - destruct addr; simpl in *. + destruct addr; cbn in *. 1,2: inv Hinjvl; trivial; inv H0; trivial; inv H2; trivial; @@ -1856,7 +1852,7 @@ Lemma eval_addressing_lessdef_none: eval_addressing genv sp addr vl2 = None. Proof. intros until vl2. intros Hlessdef Heval1. - destruct addr; simpl in *. + destruct addr; cbn in *. 1, 2, 4, 5: inv Hlessdef; trivial; inv H0; trivial; inv H2; trivial; @@ -1941,7 +1937,7 @@ Lemma eval_operation_inject: /\ Val.inject f v1 v2. Proof. intros. - rewrite eval_shift_stack_operation. simpl. + rewrite eval_shift_stack_operation. cbn. eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. -- cgit