diff options
Diffstat (limited to 'aarch64/Asmgenproof1.v')
| -rw-r--r-- | aarch64/Asmgenproof1.v | 54 |
1 files changed, 39 insertions, 15 deletions
diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v index 6d44bcc8..6f296f56 100644 --- a/aarch64/Asmgenproof1.v +++ b/aarch64/Asmgenproof1.v @@ -754,16 +754,28 @@ Lemma exec_shrx32: forall (rd r1: ireg) (n: int) k v (rs: regset) m, /\ rs'#rd = v /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. - unfold shrx32; intros. apply Val.shrx_shr_2 in H. + unfold shrx32; intros. apply Val.shrx_shr_3 in H. destruct (Int.eq n Int.zero) eqn:E. - econstructor; split. apply exec_straight_one; [simpl;eauto|auto]. split. Simpl. subst v; auto. intros; Simpl. -- econstructor; split. eapply exec_straight_three. - unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto. - simpl; eauto. - unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto. - auto. auto. auto. - split. subst v; Simpl. intros; Simpl. +- generalize (Int.eq_spec n Int.one). + destruct (Int.eq n Int.one); intro ONE. + * subst n. + econstructor; split. eapply exec_straight_two. + all: simpl; auto. + split. + ** subst v; Simpl. + destruct (Val.add _ _); simpl; trivial. + change (Int.ltu Int.one Int.iwordsize) with true; simpl. + rewrite Int.or_zero_l. + reflexivity. + ** intros; Simpl. + * econstructor; split. eapply exec_straight_three. + unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto. + simpl; eauto. + unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto. + auto. auto. auto. + split. subst v; Simpl. intros; Simpl. Qed. Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m, @@ -774,16 +786,28 @@ Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m, /\ rs'#rd = v /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. - unfold shrx64; intros. apply Val.shrxl_shrl_2 in H. + unfold shrx64; intros. apply Val.shrxl_shrl_3 in H. destruct (Int.eq n Int.zero) eqn:E. - econstructor; split. apply exec_straight_one; [simpl;eauto|auto]. split. Simpl. subst v; auto. intros; Simpl. -- econstructor; split. eapply exec_straight_three. - unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto. - simpl; eauto. - unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto. - auto. auto. auto. - split. subst v; Simpl. intros; Simpl. +- generalize (Int.eq_spec n Int.one). + destruct (Int.eq n Int.one); intro ONE. + * subst n. + econstructor; split. eapply exec_straight_two. + all: simpl; auto. + split. + ** subst v; Simpl. + destruct (Val.addl _ _); simpl; trivial. + change (Int.ltu Int.one Int64.iwordsize') with true; simpl. + rewrite Int64.or_zero_l. + reflexivity. + ** intros; Simpl. + * econstructor; split. eapply exec_straight_three. + unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto. + simpl; eauto. + unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto. + auto. auto. auto. + split. subst v; Simpl. intros; Simpl. Qed. (** Condition bits *) @@ -1620,7 +1644,7 @@ Qed. Lemma transl_load_correct: forall chunk addr args dst k c (rs: regset) m vaddr v, - transl_load chunk addr args dst k = OK c -> + transl_load TRAP chunk addr args dst k = OK c -> Op.eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some vaddr -> Mem.loadv chunk m vaddr = Some v -> exists rs', |