diff options
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 65 |
1 files changed, 64 insertions, 1 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 2ee33568..5092d99b 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -913,10 +913,73 @@ Proof. eapply plus_star; eauto. Qed. +Lemma exec_arith_instr_dont_move_PC ai rs rs': forall + (BASIC: exec_arith_instr lk ai rs = rs'), + rs PC = rs' PC. +Proof. + destruct ai; simpl; intros; + try (rewrite <- BASIC; rewrite Pregmap.gso; auto; discriminate). + - destruct i; simpl in BASIC. + + unfold compare_long in BASIC; rewrite <- BASIC. + repeat rewrite Pregmap.gso; try discriminate. reflexivity. + + unfold compare_long in BASIC; rewrite <- BASIC. + repeat rewrite Pregmap.gso; try discriminate. reflexivity. + + destruct sz; + try (unfold compare_single in BASIC || unfold compare_float in BASIC); + destruct (rs r1), (rs r2); + try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)). + - destruct i; simpl in BASIC; destruct is; + try (unfold compare_int in BASIC || unfold compare_long in BASIC); + try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)). + - destruct i; simpl in BASIC; destruct sz; + try (unfold compare_single in BASIC || unfold compare_float in BASIC); + destruct (rs r1); + try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)). + - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity). + - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity). +Qed. + +Lemma exec_basic_dont_move_PC bi rs m rs' m': forall + (BASIC: exec_basic lk ge bi rs m = Next rs' m'), + rs PC = rs' PC. +Proof. + destruct bi; simpl; intros. + - inv BASIC. exploit exec_arith_instr_dont_move_PC; eauto. + - unfold exec_load in BASIC. + destruct Mem.loadv. 2: { discriminate BASIC. } + inv BASIC. rewrite Pregmap.gso; try discriminate; auto. + - unfold exec_store in BASIC. + destruct Mem.storev. 2: { discriminate BASIC. } + inv BASIC; reflexivity. + - destruct Mem.alloc, Mem.store. 2: { discriminate BASIC. } + inv BASIC. repeat (rewrite Pregmap.gso; try discriminate). reflexivity. + - destruct Mem.loadv. 2: { discriminate BASIC. } + destruct rs, Mem.free; try discriminate BASIC. + inv BASIC; rewrite Pregmap.gso; try discriminate; auto. + - inv BASIC; rewrite Pregmap.gso; try discriminate; auto. + - inv BASIC; rewrite Pregmap.gso; try discriminate; auto. + - inv BASIC; rewrite Pregmap.gso; try discriminate; auto. + - inv BASIC; rewrite Pregmap.gso; try discriminate; auto. +Qed. + +Lemma exec_body_dont_move_PC_aux: + forall bis rs m rs' m' + (BODY: exec_body lk ge bis rs m = Next rs' m'), + rs PC = rs' PC. +Proof. + induction bis. + - intros; inv BODY; reflexivity. + - simpl; intros. + remember (exec_basic lk ge a rs m) as bi eqn:BI; destruct bi. 2: { discriminate BODY. } + symmetry in BI; destruct s in BODY, BI; simpl in BODY, BI. + exploit exec_basic_dont_move_PC; eauto; intros AGPC; rewrite AGPC. + eapply IHbis; eauto. +Qed. + Lemma exec_body_dont_move_PC bb rs m rs' m': forall (BODY: exec_body lk ge (body bb) rs m = Next rs' m'), rs PC = rs' PC. -Admitted. +Proof. apply exec_body_dont_move_PC_aux. Qed. Lemma list_nth_z_range_exceeded A (l : list A) n: n >= list_length_z l -> |