Commit 8bdfa912 authored by Cyril SIX's avatar Cyril SIX
Browse files

MPPA - Added Mload

parent 67a5ffd5
......@@ -222,11 +222,16 @@ Inductive instruction : Type :=
(* Conditional branches *)
| Pcb (bt: btest) (r: ireg) (l: label) (**r branch based on btest *)
| Plb (rd: ireg) (ra: ireg) (ofs: offset) (**r load byte *)
| Plbu (rd: ireg) (ra: ireg) (ofs: offset) (**r load byte unsigned *)
| Plh (rd: ireg) (ra: ireg) (ofs: offset) (**r load half word *)
| Plhu (rd: ireg) (ra: ireg) (ofs: offset) (**r load half word unsigned *)
| Plw (rd: ireg) (ra: ireg) (ofs: offset) (**r load int32 *)
| Plw_a (rd: ireg) (ra: ireg) (ofs: offset) (**r load any32 *)
| Pld (rd: ireg) (ra: ireg) (ofs: offset) (**r load int64 *)
| Pld_a (rd: ireg) (ra: ireg) (ofs: offset) (**r load any64 *)
| Psb (rd: ireg) (ra: ireg) (ofs: offset) (**r store byte *)
| Psh (rd: ireg) (ra: ireg) (ofs: offset) (**r store half byte *)
| Psw (rs: ireg) (ra: ireg) (ofs: offset) (**r store int32 *)
| Psw_a (rs: ireg) (ra: ireg) (ofs: offset) (**r store any32 *)
| Psd (rs: ireg) (ra: ireg) (ofs: offset) (**r store int64 *)
......@@ -319,8 +324,8 @@ Inductive instruction : Type :=
| Pallocframe (sz: Z) (pos: ptrofs) (**r allocate new stack frame *)
| Pfreeframe (sz: Z) (pos: ptrofs) (**r deallocate stack frame and restore previous frame *)
| Plabel (lbl: label) (**r define a code label *)
(*| Ploadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the address of a symbol *)
| Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *)
| Ploadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the address of a symbol *)
(*| Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *)
| Ploadli (rd: ireg) (i: int64) (**r load an immediate int64 *)
| Ploadfi (rd: freg) (f: float) (**r load an immediate float *)
| Ploadsi (rd: freg) (f: float32) (**r load an immediate single *)
......@@ -806,7 +811,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
eval_branch f l rs m (Val.cmplu_bool (Mem.valid_pointer m) Cge rs###s1 rs###s2)
(** Loads and stores *)
| Plb d a ofs =>
*)| Plb d a ofs =>
exec_load Mint8signed rs m d a ofs
| Plbu d a ofs =>
exec_load Mint8unsigned rs m d a ofs
......@@ -814,7 +819,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
exec_load Mint16signed rs m d a ofs
| Plhu d a ofs =>
exec_load Mint16unsigned rs m d a ofs
*)| Plw d a ofs =>
| Plw d a ofs =>
exec_load Mint32 rs m d a ofs
| Plw_a d a ofs =>
exec_load Many32 rs m d a ofs
......@@ -822,11 +827,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
exec_load Mint64 rs m d a ofs
| Pld_a d a ofs =>
exec_load Many64 rs m d a ofs
(*| Psb s a ofs =>
| Psb s a ofs =>
exec_store Mint8unsigned rs m s a ofs
| Psh s a ofs =>
exec_store Mint16unsigned rs m s a ofs
*)| Psw s a ofs =>
| Psw s a ofs =>
exec_store Mint32 rs m s a ofs
| Psw_a s a ofs =>
exec_store Many32 rs m s a ofs
......@@ -959,9 +964,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
end
| Plabel lbl =>
Next (nextinstr rs) m
(*| Ploadsymbol rd s ofs =>
| Ploadsymbol rd s ofs =>
Next (nextinstr (rs#rd <- (Genv.symbol_address ge s ofs))) m
| Ploadsymbol_high rd s ofs =>
(*| Ploadsymbol_high rd s ofs =>
Next (nextinstr (rs#rd <- (high_half ge s ofs))) m
| Ploadli rd i =>
Next (nextinstr (rs#GPR31 <- Vundef #rd <- (Vlong i))) m
......
......@@ -567,21 +567,21 @@ Definition transl_memory_access
(mk_instr: ireg -> offset -> instruction)
(addr: addressing) (args: list mreg) (k: code) : res (list instruction) :=
match addr, args with
(*| Aindexed ofs, a1 :: nil =>
| Aindexed ofs, a1 :: nil =>
do rs <- ireg_of a1;
OK (indexed_memory_access mk_instr rs ofs k)
| Aglobal id ofs, nil =>
OK (Ploadsymbol_high GPR31 id ofs :: mk_instr GPR31 (Ofslow id ofs) :: k)
OK (Ploadsymbol GPR31 id ofs :: mk_instr GPR31 (Ofsimm Ptrofs.zero) :: k)
| Ainstack ofs, nil =>
OK (indexed_memory_access mk_instr SP ofs k)
*)| _, _ =>
| _, _ =>
Error(msg "Asmgen.transl_memory_access")
end.
Definition transl_load (chunk: memory_chunk) (addr: addressing)
(args: list mreg) (dst: mreg) (k: code) : res (list instruction) :=
match chunk with
(*| Mint8signed =>
| Mint8signed =>
do r <- ireg_of dst;
transl_memory_access (Plb r) addr args k
| Mint8unsigned =>
......@@ -605,7 +605,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
| Mfloat64 =>
do r <- freg_of dst;
transl_memory_access (Pfld r) addr args k
*)| _ =>
| _ =>
Error (msg "Asmgen.transl_load")
end.
......
......@@ -401,7 +401,10 @@ Proof.
- eapply loadind_label; eauto.
(* storeind *)
- eapply storeind_label; eauto.
(* transl_op *)
- eapply transl_op_label; eauto.
(* transl_load *)
- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
- destruct s0; monadInv H; TailNoLabel.
- destruct s0; monadInv H; eapply tail_nolabel_trans
; [eapply make_epilogue_label|TailNoLabel].
......@@ -776,13 +779,13 @@ Local Transparent destroyed_by_op.
exploit Mem.loadv_extends; eauto. intros [v' [C D]].
left; eapply exec_straight_steps; eauto; intros. simpl in TR.
inversion TR.
(*exploit transl_load_correct; eauto.
exploit transl_load_correct; eauto.
intros [rs2 [P [Q R]]].
exists rs2; split. eauto.
split. eapply agree_set_undef_mreg; eauto. congruence.
intros; auto with asmgen.
simpl; congruence.
*)
- (* Mstore *)
assert (eval_addressing tge sp addr (map rs args) = Some a).
......
......@@ -1431,16 +1431,27 @@ Lemma transl_memory_access_correct:
Proof.
intros until v; intros TR EV.
unfold transl_memory_access in TR; destruct addr; ArgsInv.
(*
- (* indexed *)
inv EV. apply indexed_memory_access_correct; eauto with asmgen.
- (* global *)
simpl in EV. inv EV. inv TR. econstructor; econstructor; econstructor; split.
constructor. apply exec_straight_one. simpl; eauto. auto.
split; intros; Simpl. unfold eval_offset. apply low_high_half.
split; intros; Simpl. unfold eval_offset.
assert (Val.lessdef (Val.offset_ptr (Genv.symbol_address ge i i0) Ptrofs.zero) (Genv.symbol_address ge i i0)).
{ apply Val.offset_ptr_zero. }
remember (Genv.symbol_address ge i i0) as symbol.
destruct symbol; auto.
+ contradict Heqsymbol; unfold Genv.symbol_address;
destruct (Genv.find_symbol ge i); discriminate.
+ contradict Heqsymbol; unfold Genv.symbol_address;
destruct (Genv.find_symbol ge i); discriminate.
+ contradict Heqsymbol; unfold Genv.symbol_address;
destruct (Genv.find_symbol ge i); discriminate.
+ contradict Heqsymbol; unfold Genv.symbol_address;
destruct (Genv.find_symbol ge i); discriminate.
+ simpl. rewrite Ptrofs.add_zero; auto.
- (* stack *)
inv TR. inv EV. apply indexed_memory_access_correct; eauto with asmgen.
*)
Qed.
Lemma transl_load_access_correct:
......
......@@ -124,17 +124,14 @@ module Target : TARGET =
(* Generate code to load the address of id + ofs in register r *)
(*let loadsymbol oc r id ofs =
let loadsymbol oc r id ofs =
if Archi.pic_code () then begin
assert (ofs = Integers.Ptrofs.zero);
fprintf oc " la %a, %s\n" ireg r (extern_atom id)
fprintf oc " make %a = %s\n;;\n" ireg r (extern_atom id)
end else begin
fprintf oc " lui %a, %%hi(%a)\n"
ireg r symbol_offset (id, ofs);
fprintf oc " addi %a, %a, %%lo(%a)\n"
ireg r ireg r symbol_offset (id, ofs)
fprintf oc " make %a = %a\n;;\n" ireg r symbol_offset (id, ofs)
end
*)
(* Emit .file / .loc debugging directives *)
let print_file_line oc file line =
......@@ -250,10 +247,22 @@ module Target : TARGET =
| Pcb (bt, r, lbl) ->
fprintf oc " cb.%a %a?%a\n;;\n" bcond bt ireg r print_label lbl
| Plb(rd, ra, ofs) ->
fprintf oc " lbs %a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
| Plbu(rd, ra, ofs) ->
fprintf oc " lbz %a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
| Plh(rd, ra, ofs) ->
fprintf oc " lhs %a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
| Plhu(rd, ra, ofs) ->
fprintf oc " lhz %a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
| Plw(rd, ra, ofs) | Plw_a(rd, ra, ofs) | Pfls(rd, ra, ofs) ->
fprintf oc " lws %a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
| Pld(rd, ra, ofs) | Pfld(rd, ra, ofs) | Pld_a(rd, ra, ofs) -> assert Archi.ptr64;
fprintf oc " ld %a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
| Psb(rd, ra, ofs) ->
fprintf oc " sb %a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
| Psh(rd, ra, ofs) ->
fprintf oc " sh %a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
| Psw(rd, ra, ofs) | Psw_a(rd, ra, ofs) | Pfss(rd, ra, ofs) ->
fprintf oc " sw %a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
| Psd(rd, ra, ofs) | Psd_a(rd, ra, ofs) | Pfsd(rd, ra, ofs) -> assert Archi.ptr64;
......@@ -269,10 +278,10 @@ module Target : TARGET =
(* Pseudo-instructions that remain *)
| Plabel lbl ->
fprintf oc "%a:\n" print_label lbl
(*| Ploadsymbol(rd, id, ofs) ->
| Ploadsymbol(rd, id, ofs) ->
loadsymbol oc rd id ofs
| Ploadsymbol_high(rd, id, ofs) ->
fprintf oc " lui %a, %%hi(%a)\n" ireg rd symbol_offset (id, ofs)
(*| Ploadsymbol_high(rd, id, ofs) ->
fprintf oc " lui %a, %%hi[%a]\n" ireg rd symbol_offset (id, ofs)
| Ploadli(rd, n) ->
let d = camlint64_of_coqint n in
let lbl = label_literal64 d in
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment