aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asm.v2
-rw-r--r--mppa_k1c/Asmblock.v3
-rw-r--r--mppa_k1c/Asmblockgen.v6
-rw-r--r--mppa_k1c/Asmblockgenproof.v22
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml8
-rw-r--r--mppa_k1c/TargetPrinter.ml2
-rw-r--r--test/mppa/instr/indirect_call.c33
7 files changed, 69 insertions, 7 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index eef5f39c..0f6f2b8b 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -59,6 +59,7 @@ Inductive instruction : Type :=
| Pset (rd: preg) (rs: ireg) (**r set system register *)
| Pret (**r return *)
| Pcall (l: label) (**r function call *)
+ | Picall (rs: ireg) (**r function call on register *)
(* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *)
| Pgoto (l: label) (**r goto *)
| Pj_l (l: label) (**r jump to label *)
@@ -156,6 +157,7 @@ Definition control_to_instruction (c: control) :=
| PExpand (Asmblock.Pbuiltin ef args res) => Pbuiltin ef args res
| PCtlFlow Asmblock.Pret => Pret
| PCtlFlow (Asmblock.Pcall l) => Pcall l
+ | PCtlFlow (Asmblock.Picall r) => Picall r
| PCtlFlow (Asmblock.Pgoto l) => Pgoto l
| PCtlFlow (Asmblock.Pj_l l) => Pj_l l
| PCtlFlow (Asmblock.Pcb bt r l) => Pcb bt r l
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 282723f1..300ab0fc 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -220,6 +220,7 @@ table: .long table[0], table[1], ...
Inductive cf_instruction : Type :=
| Pret (**r return *)
| Pcall (l: label) (**r function call *)
+ | Picall (r: ireg) (**r function call on register value *)
(* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *)
| Pgoto (l: label) (**r goto *)
@@ -1148,6 +1149,8 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem)
Next (rs#PC <- (rs#RA)) m
| Pcall s =>
Next (rs#RA <- (rs#PC) #PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
+ | Picall r =>
+ Next (rs#RA <- (rs#PC) #PC <- (rs#r)) m
| Pgoto s =>
Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
| Pj_l l =>
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index e32748f8..d051697f 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -789,9 +789,9 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co
| None => OK nil
| Some i =>
match i with
-(*| Mcall sig (inl r) =>
- do r1 <- ireg_of r; OK (Pjal_r r1 sig :: k)
-*) | MBcall sig (inr symb) =>
+ | MBcall sig (inl r) =>
+ do r1 <- ireg_of r; OK ((Picall r1) ::g nil)
+ | MBcall sig (inr symb) =>
OK ((Pcall symb) ::g nil)
(*| Mtailcall sig (inl r) =>
do r1 <- ireg_of r;
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 686e8349..5a3ab5e1 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -1162,7 +1162,27 @@ Proof.
assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
eapply transf_function_no_overflow; eauto.
destruct s1 as [rf|fid]; simpl in H7.
- * (* Indirect call *) inv H1.
+ * (* Indirect call *)
+ monadInv H1.
+ assert (ms' rf = Vptr f' Ptrofs.zero).
+ { unfold find_function_ptr in H14. destruct (ms' rf); try discriminate.
+ revert H14; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
+ assert (rs2 x = Vptr f' Ptrofs.zero).
+ { exploit ireg_val; eauto. rewrite H; intros LD; inv LD; auto. }
+ generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1.
+ remember (Ptrofs.add _ _) as ofs'.
+ assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc).
+ { econstructor; eauto. }
+ assert (f1 = f) by congruence. subst f1.
+ exploit return_address_offset_correct; eauto. intros; subst ra.
+
+ repeat eexists.
+ rewrite H6. econstructor; eauto.
+ rewrite H7. econstructor; eauto.
+ econstructor; eauto.
+ econstructor; eauto. eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. Simpl.
+ simpl. Simpl. rewrite PCeq. rewrite Heqofs'. simpl. auto.
+
* (* Direct call *)
monadInv H1.
generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 4d7c8636..5c155540 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -159,6 +159,7 @@ let expand_rec = function
let ctl_flow_rec = function
| Pret -> { inst = "Pret"; write_locs = []; read_locs = [Reg RA]; imm = None ; is_control = true}
| Pcall lbl -> { inst = "Pcall"; write_locs = [Reg RA]; read_locs = []; imm = None ; is_control = true}
+ | Picall r -> { inst = "Picall"; write_locs = [Reg RA]; read_locs = [Reg (IR r)]; imm = None; is_control = true}
| Pgoto lbl -> { inst = "Pcall"; write_locs = []; read_locs = []; imm = None ; is_control = true}
| Pj_l lbl -> { inst = "Pj_l"; write_locs = []; read_locs = []; imm = None ; is_control = true}
| Pcb (bt, rs, lbl) -> { inst = "Pcb"; write_locs = []; read_locs = [Reg (IR rs)]; imm = None ; is_control = true}
@@ -332,7 +333,7 @@ type real_instruction =
| Lbs | Lbz | Lhs | Lhz | Lws | Ld
| Sb | Sh | Sw | Sd
(* BCU *)
- | Call | Cb | Goto | Ret | Get | Set
+ | Icall | Call | Cb | Goto | Ret | Get | Set
(* FPU *)
| Fnegd
@@ -376,6 +377,7 @@ let ab_inst_to_real = function
| "Pcb" | "Pcbu" -> Cb
| "Pcall" -> Call
+ | "Picall" -> Icall
| "Pgoto" | "Pj_l" -> Goto
| "Pget" -> Get
| "Pret" -> Ret
@@ -428,7 +430,7 @@ let rec_to_usage r =
(match encoding with None | Some U6 | Some S10 -> lsu_acc
| Some U27L5 | Some U27L10 -> lsu_acc_x
| Some E27U27L10 -> lsu_acc_y)
- | Call | Cb | Goto | Ret | Set -> bcu
+ | Icall | Call | Cb | Goto | Ret | Set -> bcu
| Get -> bcu_tiny_tiny_mau_xnop
| Fnegd -> alu_lite
@@ -444,7 +446,7 @@ let real_inst_to_latency = function
-> 3 (* FIXME - random value *)
| Get -> 1
| Set -> 3
- | Call | Cb | Goto | Ret -> 42 (* Should not matter since it's the final instruction of the basic block *)
+ | Icall | Call | Cb | Goto | Ret -> 42 (* Should not matter since it's the final instruction of the basic block *)
| Fnegd -> 1
let rec_to_info r : inst_info =
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 36fab151..0d357962 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -237,6 +237,8 @@ module Target (*: TARGET*) =
fprintf oc " ret \n"
| Pcall(s) ->
fprintf oc " call %a\n" symbol s
+ | Picall(rs) ->
+ fprintf oc " icall %a\n" ireg rs
| Pgoto(s) ->
fprintf oc " goto %a\n" symbol s
| Pj_l(s) ->
diff --git a/test/mppa/instr/indirect_call.c b/test/mppa/instr/indirect_call.c
new file mode 100644
index 00000000..3a45ce52
--- /dev/null
+++ b/test/mppa/instr/indirect_call.c
@@ -0,0 +1,33 @@
+#include "framework.h"
+
+long long sum(long long a, long long b){
+ return a+b;
+}
+
+long long diff(long long a, long long b){
+ return a-b;
+}
+
+long long mul(long long a, long long b){
+ return a*b;
+}
+
+long long make(long long a){
+ return a;
+}
+
+BEGIN_TEST(long long)
+{
+ long long d = 3;
+ long long (*op)(long long, long long);
+
+ if (a % d == 0)
+ op = sum;
+ else if (a % d == 1)
+ op = diff;
+ else
+ op = mul;
+
+ c += op(make(a), make(b));
+}
+END_TEST()
generated by cgit (git 2.34.1) at 2024-07-01 23:42:56 +0000