From bdd3b6734690100a7c696cf57bfe52963ec2c6ef Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 26 May 2020 12:04:59 +0100 Subject: Finished second pass and fixed bug --- src/translation/HTLgen.v | 2 +- src/translation/HTLgenspec.v | 53 ++++++++++++++++++++++++++++++-------------- 2 files changed, 37 insertions(+), 18 deletions(-) (limited to 'src/translation') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 714cf98..670dcd4 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -272,7 +272,7 @@ Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit := | Inop n' => add_instr n n' Vskip | Iop op args dst n' => do instr <- translate_instr op args; - add_instr n n' (block dst instr) + add_instr n n' (nonblock dst instr) | Iload _ _ _ _ _ => error (Errors.msg "Loads are not implemented.") | Istore _ _ _ _ _ => error (Errors.msg "Stores are not implemented.") | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index f01ab1c..c8f1751 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -222,6 +222,12 @@ Ltac rewrite_states := remember (?x ?s) as c1; remember (?x ?s') as c2; try subst end. +Lemma translate_instr_tr_op : + forall op args s s' e i, + translate_instr op args s = OK e s' i -> + tr_op op args e. +Admitted. + Lemma iter_expand_instr_spec : forall l fin rtrn s s' i x, HTLMonadExtra.collectlist (transf_instr fin rtrn) l s = OK x s' i -> @@ -236,30 +242,43 @@ Proof. + subst. destruct instr1 eqn:?. - econstructor. - unfold add_instr in EQ. - destruct (check_empty_node_datapath s1 pc1); try discriminate. - destruct (check_empty_node_controllogic s1 pc1); try discriminate. - inversion EQ. - destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. - unfold add_instr in EQ. - destruct (check_empty_node_datapath s1 pc1); try discriminate. - destruct (check_empty_node_controllogic s1 pc1); try discriminate. - inversion EQ. - destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; - [ discriminate | apply H7 ]. + * unfold add_instr in EQ. + destruct (check_empty_node_datapath s1 pc1); try discriminate. + destruct (check_empty_node_controllogic s1 pc1); try discriminate. + inversion EQ. + econstructor. + destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + + destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + + inversion H1. inversion H7. rewrite H. apply tr_instr_Inop. + eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + + * monadInv EQ. + inv_incr. + unfold add_instr in EQ2. + destruct (check_empty_node_datapath s0 pc1); try discriminate. + destruct (check_empty_node_controllogic s0 pc1); try discriminate. + inversion EQ2. + econstructor. + destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. - inversion H1. inversion H7. rewrite H. apply tr_instr_Inop. - eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7; + [ discriminate | apply H7 ]. + + inversion H1. inversion H7. unfold nonblock. rewrite <- e2. rewrite H. constructor. + eapply translate_instr_tr_op. apply EQ1. + + eapply in_map with (f := fst) in H7. simpl in H7. contradiction. + eapply IHl. apply EQ0. assumption. destruct H1. inversion H1. subst. contradiction. assumption. - - Qed. Theorem transl_module_correct : -- cgit