diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-27 09:24:23 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-27 09:24:23 +0200 |
| commit | f3d0622f2dc0c3398ec9f81d9367fbb70e40bbff (patch) | |
| tree | 01038086feb272f5cad23430868faf92d51621e7 /aarch64 | |
| parent | 29a44f107a88ea41f9791a5398823304b84aa958 (diff) | |
| download | compcert-kvx-f3d0622f2dc0c3398ec9f81d9367fbb70e40bbff.tar.gz compcert-kvx-f3d0622f2dc0c3398ec9f81d9367fbb70e40bbff.zip | |
Playing around with find_instr_bblock's base case
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/Asmgenproof.v | 32 |
1 files changed, 25 insertions, 7 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index a9f88991..9e12655a 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -530,21 +530,25 @@ Qed. Lemma unfold_car_cdr bb bbs tc: unfold (bb :: bbs) = OK tc -> - exists tbb tc', unfold_bblock bb = OK tbb /\ unfold bbs = OK tc'. + exists tbb tc', unfold_bblock bb = OK tbb + /\ unfold bbs = OK tc' + /\ unfold (bb :: bbs) = OK (tbb ++ tc'). Proof. intros UNFOLD. + assert (UF := UNFOLD). unfold unfold in UNFOLD. apply bind_inversion in UNFOLD. destruct UNFOLD as (? & UBB). destruct UBB as (UBB & REST). apply bind_inversion in REST. destruct REST as (? & UNFOLD'). - fold unfold in UNFOLD'. destruct UNFOLD'. - eexists; eauto. + fold unfold in UNFOLD'. destruct UNFOLD' as (UNFOLD' & UNFOLD). + rewrite <- UNFOLD in UF. + eauto. Qed. Lemma unfold_cdr bb bbs tc: unfold (bb :: bbs) = OK tc -> exists tc', unfold bbs = OK tc'. Proof. - intros; exploit unfold_car_cdr; eauto. intros (_ & ? & _ & ?). + intros; exploit unfold_car_cdr; eauto. intros (_ & ? & _ & ? & _). eexists; eauto. Qed. @@ -552,7 +556,7 @@ Lemma unfold_car bb bbs tc: unfold (bb :: bbs) = OK tc -> exists tbb, unfold_bblock bb = OK tbb. Proof. - intros; exploit unfold_car_cdr; eauto. intros (? & _ & ? & _). + intros; exploit unfold_car_cdr; eauto. intros (? & _ & ? & _ & _). eexists; eauto. Qed. @@ -567,7 +571,7 @@ Proof. - intros ? UNFOLD ? IN. (* unfold proceeds by unfolding the basic block at the head of the list and * then recurring *) - exploit unfold_car_cdr; eauto. intros (? & ? & ? & ?). + exploit unfold_car_cdr; eauto. intros (? & ? & ? & ? & _). (* basic block is either in head or tail *) inversion IN as [EQ | NEQ]. + rewrite <- EQ; eexists; eauto. @@ -643,7 +647,21 @@ Proof. - intros. inversion FINDBB. - intros pos bb tlb FINDBB UNFOLD SIZE. destruct pos. - + admit. + + inv FINDBB. simpl. + exploit unfold_car_cdr; eauto. intros (tbb & tlb' & UNFOLD_BBLOCK & UNFOLD' & UNFOLD_cons). + unfold unfold_bblock in UNFOLD_BBLOCK. + destruct (zle (list_length_z (header bb)) 1). 2: { inversion UNFOLD_BBLOCK. } + apply bind_inversion in UNFOLD_BBLOCK. + destruct UNFOLD_BBLOCK as (? & UNFOLD_BODY & H). + inversion H as (UNFOLD_BBLOCK). + + remember (list_nth_z (header bb) n) as label_opt eqn:LBL. destruct label_opt. + * (* nth instruction is a label *) + eexists; split. { eapply is_nth_label; eauto. } + rewrite UNFOLD in UNFOLD_cons. inversion UNFOLD_cons. + admit. + * admit. + + unfold find_bblock in FINDBB; simpl in FINDBB; fold find_bblock in FINDBB. inversion UNFOLD as (UNFOLD'). apply bind_inversion in UNFOLD'. destruct UNFOLD' as (? & (UNFOLD_BBLOCK' & UNFOLD')). |