diff options
| -rw-r--r-- | mppa_k1c/Asmgen.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 6 | ||||
| -rw-r--r-- | mppa_k1c/Asmgenproof1.v | 19 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 20 |
4 files changed, 23 insertions, 26 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 98253ab3..9025a00d 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -267,11 +267,11 @@ Definition transl_op OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero) then Ploadsymbol rd s Ptrofs.zero :: addptrofs rd rd ofs k else Ploadsymbol rd s ofs :: k) - | Oaddrstack n, nil => +*)| Oaddrstack n, nil => do rd <- ireg_of res; OK (addptrofs rd SP n k) - | Ocast8signed, a1 :: nil => +(*| Ocast8signed, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pslliw rd rs (Int.repr 24) :: Psraiw rd rd (Int.repr 24) :: k) | Ocast16signed, a1 :: nil => diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 60616311..4150cba8 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -159,15 +159,15 @@ Proof. (*unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.*) Qed. Hint Resolve opimm64_label: labels. -(* + Remark addptrofs_label: forall r1 r2 n k, tail_nolabel k (addptrofs r1 r2 n k). Proof. unfold addptrofs; intros. destruct (Ptrofs.eq_dec n Ptrofs.zero). TailNoLabel. - destruct Archi.ptr64. apply opimm64_label; TailNoLabel. apply opimm32_label; TailNoLabel. + apply opimm64_label; TailNoLabel. Qed. Hint Resolve addptrofs_label: labels. - +(* Remark transl_cond_float_nolabel: forall c r1 r2 r3 insn normal, transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn. diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v index 62c3bb49..77643b8b 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -247,7 +247,7 @@ Proof. Qed. (** Add offset to pointer *) -(* + Lemma addptrofs_correct: forall rd r1 n k rs m, r1 <> GPR31 -> @@ -262,19 +262,13 @@ Proof. apply exec_straight_one. simpl; eauto. auto. split. Simpl. destruct (rs r1); simpl; auto. rewrite Ptrofs.add_zero; auto. intros; Simpl. -- destruct Archi.ptr64 eqn:SF. -+ unfold addimm64. +- unfold addimm64. exploit (opimm64_correct Paddl Paddil Val.addl); eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. split; auto. - rewrite B. simpl. destruct (rs r1); simpl; auto. rewrite SF. + rewrite B. unfold getw. destruct (rs r1); simpl; auto. rewrite Ptrofs.of_int64_to_int64 by auto. auto. -+ unfold addimm32. - exploit (opimm32_correct Paddw Paddiw Val.add); eauto. intros (rs' & A & B & C). - exists rs'; split. eexact A. split; auto. - rewrite B. simpl. destruct (rs r1); simpl; auto. rewrite SF. - rewrite Ptrofs.of_int_to_int by auto. auto. Qed. - +(* Lemma addptrofs_correct_2: forall rd r1 n k (rs: regset) m b ofs, r1 <> GPR31 -> rs#r1 = Vptr b of @@ -1202,8 +1196,11 @@ Proof. Opaque Int.eq. intros until c; intros TR EV. unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl. -- (* move *) +- (* Omove *) destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl. +- (* Oaddrstack *) + exploit addptrofs_correct. instantiate (1 := GPR12); auto with asmgen. intros (rs' & A & B & C). + exists rs'; split; eauto. auto with asmgen. - (* Ocast32signed *) exploit cast32signed_correct; eauto. intros (rs' & A & B & C). exists rs'; split; eauto. split. apply B. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 977d3019..cb3b558c 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -340,16 +340,16 @@ module Target : TARGET = fprintf oc "%s end pseudoinstr btbl\n" comment *)| Pbuiltin(ef, args, res) -> begin match ef with - (*| EF_annot(kind,txt, targs) -> - begin match (P.to_int kind) with - | 1 -> let annot = annot_text preg_annot "x2" (camlstring_of_coqstring txt) args in - fprintf oc "%s annotation: %S\n" comment annot - | 2 -> let lbl = new_label () in - fprintf oc "%a: " label lbl; - add_ais_annot lbl preg_annot "x2" (camlstring_of_coqstring txt) args - | _ -> assert false - end - *)| EF_debug(kind, txt, targs) -> + | EF_annot(kind,txt, targs) -> + begin match (P.to_int kind) with + | 1 -> let annot = annot_text preg_annot "x2" (camlstring_of_coqstring txt) args in + fprintf oc "%s annotation: %S\n" comment annot + (*| 2 -> let lbl = new_label () in + fprintf oc "%a: " label lbl; + add_ais_annot lbl preg_annot "x2" (camlstring_of_coqstring txt) args + *)| _ -> assert false + end + | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg_annot "sp" oc (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> |