aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asm.v2
-rw-r--r--mppa_k1c/Asmblock.v7
-rw-r--r--mppa_k1c/Asmblockgen.v6
-rw-r--r--mppa_k1c/Asmblockgenproof.v22
-rw-r--r--mppa_k1c/Asmblockgenproof1.v78
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml8
-rw-r--r--mppa_k1c/PostpassSchedulingproof.v178
-rw-r--r--mppa_k1c/TargetPrinter.ml2
-rw-r--r--test/mppa/instr/indirect_call.c33
9 files changed, 258 insertions, 78 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 14ceb082..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 *)
@@ -958,14 +959,14 @@ Definition eval_offset (ofs: offset) : ptrofs :=
end.
Definition exec_load (chunk: memory_chunk) (rs: regset) (m: mem)
- (d: preg) (a: ireg) (ofs: offset) :=
+ (d: ireg) (a: ireg) (ofs: offset) :=
match Mem.loadv chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) with
| None => Stuck
| Some v => Next (rs#d <- v) m
end.
Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem)
- (s: preg) (a: ireg) (ofs: offset) :=
+ (s: ireg) (a: ireg) (ofs: offset) :=
match Mem.storev chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) (rs s) with
| None => Stuck
| Some m' => Next rs m'
@@ -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/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 02301161..bf3be247 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1318,13 +1318,13 @@ Lemma indexed_load_access_correct:
exec_basic_instr ge (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs) ->
forall (base: ireg) ofs k (rs: regset) v,
Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v ->
- base <> RTMP -> rd <> PC ->
+ base <> RTMP ->
exists rs',
exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m
/\ rs'#rd = v
/\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
Proof.
- intros until m; intros EXEC; intros until v; intros LOAD NOT31 NOTPC.
+ intros until m; intros EXEC; intros until v; intros LOAD NOT31.
exploit indexed_memory_access_correct; eauto.
intros (base' & ofs' & rs' & A & B & C).
econstructor; split.
@@ -1339,18 +1339,22 @@ Lemma indexed_store_access_correct:
exec_basic_instr ge (mk_instr base ofs) rs m = exec_store ge chunk rs m r1 base ofs) ->
forall (base: ireg) ofs k (rs: regset) m',
Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' ->
- base <> RTMP -> r1 <> RTMP -> r1 <> PC ->
+ base <> RTMP -> r1 <> RTMP ->
exists rs',
exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m'
/\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
- intros until m; intros EXEC; intros until m'; intros STORE NOT31 NOT31' NOTPC.
+ intros until m; intros EXEC; intros until m'; intros STORE NOT31 NOT31'.
exploit indexed_memory_access_correct. instantiate (1 := base). eauto.
intros (base' & ofs' & rs' & A & B & C).
econstructor; split.
eapply exec_straight_opt_right. eapply A. apply exec_straight_one. rewrite EXEC.
- unfold exec_store. rewrite B, C, STORE. eauto. eauto. auto.
- intros; Simpl. rewrite C; auto.
+ unfold exec_store. rewrite B, C, STORE.
+ eauto.
+ discriminate.
+ { intro. inv H. contradiction. }
+ auto.
+(* intros; Simpl. rewrite C; auto. *)
Qed.
Lemma loadind_correct:
@@ -1364,14 +1368,15 @@ Lemma loadind_correct:
/\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
intros until v; intros TR LOAD NOT31.
- assert (A: exists mk_instr,
- c = indexed_memory_access mk_instr base ofs :: k
+ assert (A: exists mk_instr rd,
+ preg_of dst = IR rd
+ /\ c = indexed_memory_access mk_instr base ofs :: k
/\ forall base' ofs' rs',
exec_basic_instr ge (mk_instr base' ofs') rs' m =
- exec_load ge (chunk_of_type ty) rs' m (preg_of dst) base' ofs').
+ exec_load ge (chunk_of_type ty) rs' m rd base' ofs').
{ unfold loadind in TR.
- destruct ty, (preg_of dst); inv TR; econstructor; split; eauto. }
- destruct A as (mk_instr & B & C). subst c.
+ destruct ty, (preg_of dst); inv TR; econstructor; esplit; eauto. }
+ destruct A as (mk_instr & rd & rdEq & B & C). subst c. rewrite rdEq.
eapply indexed_load_access_correct; eauto with asmgen.
Qed.
@@ -1385,14 +1390,17 @@ Lemma storeind_correct:
/\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros until m'; intros TR STORE NOT31.
- assert (A: exists mk_instr,
- c = indexed_memory_access mk_instr base ofs :: k
+ assert (A: exists mk_instr rr,
+ preg_of src = IR rr
+ /\ c = indexed_memory_access mk_instr base ofs :: k
/\ forall base' ofs' rs',
exec_basic_instr ge (mk_instr base' ofs') rs' m =
- exec_store ge (chunk_of_type ty) rs' m (preg_of src) base' ofs').
- { unfold storeind in TR. destruct ty, (preg_of src); inv TR; econstructor; split; eauto. }
- destruct A as (mk_instr & B & C). subst c.
- eapply indexed_store_access_correct; eauto with asmgen.
+ exec_store ge (chunk_of_type ty) rs' m rr base' ofs').
+ { unfold storeind in TR. destruct ty, (preg_of src); inv TR; econstructor; esplit; eauto. }
+ destruct A as (mk_instr & rr & rsEq & B & C). subst c.
+ eapply indexed_store_access_correct; eauto with asmgen.
+ congruence.
+ destruct rr; try discriminate. destruct src; try discriminate.
Qed.
Ltac bsimpl := unfold exec_bblock; simpl.
@@ -1492,13 +1500,12 @@ Lemma transl_load_access_correct:
transl_memory_access mk_instr addr args k = OK c ->
eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
Mem.loadv chunk m v = Some v' ->
- rd <> PC ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
/\ rs'#rd = v'
/\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
Proof.
- intros until v'; intros INSTR TR EV LOAD NOTPC.
+ intros until v'; intros INSTR TR EV LOAD.
exploit transl_memory_access_correct; eauto.
intros (base & ofs & rs' & A & B & C).
econstructor; split.
@@ -1514,17 +1521,19 @@ Lemma transl_store_access_correct:
transl_memory_access mk_instr addr args k = OK c ->
eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
Mem.storev chunk m v rs#r1 = Some m' ->
- r1 <> PC -> r1 <> RTMP ->
+ r1 <> RTMP ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
/\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
- intros until m'; intros INSTR TR EV STORE NOTPC NOT31.
+ intros until m'; intros INSTR TR EV STORE NOT31.
exploit transl_memory_access_correct; eauto.
intros (base & ofs & rs' & A & B & C).
econstructor; split.
eapply exec_straight_opt_right. eexact A. apply exec_straight_one.
- rewrite INSTR. unfold exec_store. rewrite B, C, STORE by auto. reflexivity. auto.
+ rewrite INSTR. unfold exec_store. rewrite B. rewrite C; try discriminate. rewrite STORE. auto.
+ intro. inv H. contradiction.
+ auto.
Qed.
Lemma transl_load_correct:
@@ -1538,12 +1547,13 @@ Lemma transl_load_correct:
/\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
intros until v; intros TR EV LOAD.
- assert (A: exists mk_instr,
- transl_memory_access mk_instr addr args k = OK c
+ assert (A: exists mk_instr rd,
+ preg_of dst = IR rd
+ /\ transl_memory_access mk_instr addr args k = OK c
/\ forall base ofs rs,
- exec_basic_instr ge (mk_instr base ofs) rs m = exec_load ge chunk rs m (preg_of dst) base ofs).
- { unfold transl_load in TR; destruct chunk; ArgsInv; econstructor; (split; [eassumption|auto]). }
- destruct A as (mk_instr & B & C).
+ exec_basic_instr ge (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs).
+ { unfold transl_load in TR; destruct chunk; ArgsInv; econstructor; (esplit; eauto). }
+ destruct A as (mk_instr & rd & rdEq & B & C). rewrite rdEq.
eapply transl_load_access_correct; eauto with asmgen.
Qed.
@@ -1557,19 +1567,21 @@ Lemma transl_store_correct:
/\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
intros until m'; intros TR EV STORE.
- assert (A: exists mk_instr chunk',
- transl_memory_access mk_instr addr args k = OK c
+ assert (A: exists mk_instr chunk' rr,
+ preg_of src = IR rr
+ /\ transl_memory_access mk_instr addr args k = OK c
/\ (forall base ofs rs,
- exec_basic_instr ge (mk_instr base ofs) rs m = exec_store ge chunk' rs m (preg_of src) base ofs)
+ exec_basic_instr ge (mk_instr base ofs) rs m = exec_store ge chunk' rs m rr base ofs)
/\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src)).
{ unfold transl_store in TR; destruct chunk; ArgsInv;
- (econstructor; econstructor; split; [eassumption | split; [ intros; simpl; reflexivity | auto]]).
+ (econstructor; econstructor; econstructor; split; [eauto | split; [eassumption | split; [ intros; simpl; reflexivity | auto]]]).
destruct a; auto. apply Mem.store_signed_unsigned_8.
destruct a; auto. apply Mem.store_signed_unsigned_16.
}
- destruct A as (mk_instr & chunk' & B & C & D).
+ destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D).
rewrite D in STORE; clear D.
- eapply transl_store_access_correct; eauto with asmgen.
+ eapply transl_store_access_correct; eauto with asmgen. congruence.
+ destruct rr; try discriminate. destruct src; try discriminate.
Qed.
Lemma make_epilogue_correct:
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/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index ef9f5f0d..35936303 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -17,6 +17,7 @@ Require Import Op Locations Machblock Conventions Asmblock.
Require Import Asmblockgenproof0.
Require Import PostpassScheduling.
Require Import Asmblockgenproof.
+Require Import Axioms.
Local Open Scope error_monad_scope.
@@ -173,13 +174,86 @@ Proof.
erewrite exec_basic_instr_pc; eauto.
Qed.
-(* Lemma exec_basic_instr_pc_var:
+Lemma next_eq {A: Type}:
+ forall (rs rs':A) m m',
+ rs = rs' -> m = m' -> Next rs m = Next rs' m'.
+Proof.
+ intros. congruence.
+Qed.
+
+Lemma regset_double_set:
+ forall r1 r2 (rs: regset) v1 v2,
+ r1 <> r2 ->
+ (rs # r1 <- v1 # r2 <- v2) = (rs # r2 <- v2 # r1 <- v1).
+Proof.
+ intros. apply functional_extensionality. intros r. destruct (preg_eq r r1).
+ - subst. rewrite Pregmap.gso; auto. repeat (rewrite Pregmap.gss). auto.
+ - destruct (preg_eq r r2).
+ + subst. rewrite Pregmap.gss. rewrite Pregmap.gso; auto. rewrite Pregmap.gss. auto.
+ + repeat (rewrite Pregmap.gso; auto).
+Qed.
+
+Lemma regset_double_set_id:
+ forall r (rs: regset) v1 v2,
+ (rs # r <- v1 # r <- v2) = (rs # r <- v2).
+Proof.
+ intros. apply functional_extensionality. intros. destruct (preg_eq r x).
+ - subst r. repeat (rewrite Pregmap.gss; auto).
+ - repeat (rewrite Pregmap.gso); auto.
+Qed.
+
+Lemma exec_load_pc_var:
+ forall ge t rs m rd ra ofs rs' m' v,
+ exec_load ge t rs m rd ra ofs = Next rs' m' ->
+ exec_load ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+ intros. unfold exec_load in *. rewrite Pregmap.gso; try discriminate.
+ destruct (Mem.loadv _ _ _).
+ - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
+ - discriminate.
+Qed.
+
+Lemma exec_store_pc_var:
+ forall ge t rs m rd ra ofs rs' m' v,
+ exec_store ge t rs m rd ra ofs = Next rs' m' ->
+ exec_store ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+ intros. unfold exec_store in *. rewrite Pregmap.gso; try discriminate.
+ destruct (Mem.storev _ _ _).
+ - inv H. apply next_eq; auto.
+ - discriminate.
+Qed.
+
+Lemma exec_basic_instr_pc_var:
forall ge i rs m rs' m' v,
exec_basic_instr ge i rs m = Next rs' m' ->
exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.
Proof.
- intros. unfold exec_basic_instr in *. exploreInst.
- - inv H. unfold exec_arith_instr. exploreInst. Search (_ # _ <- _).
+ intros. unfold exec_basic_instr in *. destruct i.
+ - unfold exec_arith_instr in *. exploreInst.
+ all: try (inv H; apply next_eq; auto;
+ apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
+ - exploreInst; apply exec_load_pc_var; auto.
+ - exploreInst; apply exec_store_pc_var; auto.
+ - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate).
+ destruct (Mem.storev _ _ _ _); try discriminate.
+ inv H. apply next_eq; auto. apply functional_extensionality. intros.
+ rewrite (regset_double_set GPR32 PC); try discriminate.
+ rewrite (regset_double_set GPR12 PC); try discriminate.
+ rewrite (regset_double_set GPR14 PC); try discriminate. reflexivity.
+ - repeat (rewrite Pregmap.gso; try discriminate).
+ destruct (Mem.loadv _ _ _); try discriminate.
+ destruct (rs GPR12); try discriminate.
+ destruct (Mem.free _ _ _ _); try discriminate.
+ inv H. apply next_eq; auto.
+ rewrite (regset_double_set GPR32 PC).
+ rewrite (regset_double_set GPR12 PC). reflexivity.
+ all: discriminate.
+ - destruct rs0; try discriminate. inv H. apply next_eq; auto.
+ repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
+ - destruct rd; try discriminate. inv H. apply next_eq; auto.
+ repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
+ - inv H. apply next_eq; auto.
Qed.
Lemma exec_body_pc_var:
@@ -190,13 +264,30 @@ Proof.
induction l.
- intros. simpl. simpl in H. inv H. auto.
- intros. simpl in *.
- destruct (exec_basic_instr ge a rs m) eqn:EXEBI.
- +
-Qed. *)
+ destruct (exec_basic_instr ge a rs m) eqn:EXEBI; try discriminate.
+ erewrite exec_basic_instr_pc_var; eauto.
+Qed.
+Lemma pc_set_add:
+ forall rs v r x y,
+ 0 <= x <= Ptrofs.max_unsigned ->
+ 0 <= y <= Ptrofs.max_unsigned ->
+ rs # r <- (Val.offset_ptr v (Ptrofs.repr (x + y))) = rs # r <- (Val.offset_ptr (rs # r <- (Val.offset_ptr v (Ptrofs.repr x)) r) (Ptrofs.repr y)).
+Proof.
+ intros. apply functional_extensionality. intros r0. destruct (preg_eq r r0).
+ - subst. repeat (rewrite Pregmap.gss); auto.
+ destruct v; simpl; auto.
+ rewrite Ptrofs.add_assoc.
+ cutrewrite (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)); auto.
+ unfold Ptrofs.add.
+ cutrewrite (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)); auto.
+ repeat (rewrite Ptrofs.unsigned_repr); auto.
+ - repeat (rewrite Pregmap.gso; auto).
+Qed.
Lemma concat2_straight:
forall a b bb rs m rs'' m'' f ge,
+ size a <= Ptrofs.max_unsigned -> size b <= Ptrofs.max_unsigned ->
concat2 a b = OK bb ->
exec_bblock ge f bb rs m = Next rs'' m'' ->
exists rs' m',
@@ -204,21 +295,30 @@ Lemma concat2_straight:
/\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a))
/\ exec_bblock ge f b rs' m' = Next rs'' m''.
Proof.
- intros.
- exploit concat2_noexit; eauto. intros.
- exploit concat2_decomp; eauto. intros. inv H2.
-(* destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bd ex WF]. *)
- unfold exec_bblock in H0. destruct (exec_body ge (body bb) rs m) eqn:EXEB.
- - rewrite H3 in EXEB. apply exec_body_app in EXEB. destruct EXEB as (rs1 & m1 & EXEB1 & EXEB2).
- repeat eexists.
- unfold exec_bblock. rewrite EXEB1. rewrite H1. simpl. eauto.
- exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H2. auto.
- unfold exec_bblock.
-Admitted.
+ intros until ge. intros LTA LTB CONC2 EXEB.
+ exploit concat2_noexit; eauto. intros EXA.
+ exploit concat2_decomp; eauto. intros. inv H.
+ unfold exec_bblock in EXEB. destruct (exec_body ge (body bb) rs m) eqn:EXEB'; try discriminate.
+ rewrite H0 in EXEB'. apply exec_body_app in EXEB'. destruct EXEB' as (rs1 & m1 & EXEB1 & EXEB2).
+ repeat eexists.
+ unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto.
+ exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto.
+ unfold exec_bblock. unfold nextblock. erewrite exec_body_pc_var; eauto.
+ rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id.
+ assert (size bb = size a + size b).
+ { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r.
+ repeat (rewrite Nat2Z.inj_add). omega. }
+ clear EXA H0 H1. rewrite H in EXEB.
+ assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. }
+ rewrite H0. rewrite <- pc_set_add; auto.
+ exploit AB.size_positive. instantiate (1 := a). intro. omega.
+ exploit AB.size_positive. instantiate (1 := b). intro. omega.
+Qed.
+Axiom TODO: False.
-Lemma concat_exec_bblock_nonil (ge: Genv.t fundef unit) (f: function) :
- forall a bb rs m lbb rs'' m'',
+Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) :
+ forall a bb rs m lbb rs'' m'',
lbb <> nil ->
concat_all (a :: lbb) = OK bb ->
exec_bblock ge f bb rs m = Next rs'' m'' ->
@@ -231,29 +331,33 @@ Proof.
intros until m''. intros Hnonil CONC EXEB.
simpl in CONC.
destruct lbb as [|b lbb]; try contradiction. clear Hnonil.
- monadInv CONC. exists x.
+ monadInv CONC. exploit concat2_straight; eauto. 1-2: destruct TODO. intros (rs' & m' & EXEB1 & PCeq & EXEB2).
+ exists x. repeat econstructor. all: eauto.
Admitted.
+Lemma concat2_size:
+ forall a b bb, concat2 a b = OK bb -> size bb = size a + size b.
+Proof.
+ intros. unfold concat2 in H.
+ destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bdy ex WF]; simpl in *.
+ destruct exa; try discriminate. destruct hdb; try discriminate. destruct exb; try discriminate.
+ - destruct c.
+ + destruct i; try discriminate.
+ + inv H. unfold size; simpl. rewrite app_length. rewrite Nat.add_0_r. rewrite <- Nat2Z.inj_add. rewrite Nat.add_assoc. reflexivity.
+ - inv H. unfold size; simpl. rewrite app_length. repeat (rewrite Nat.add_0_r). rewrite <- Nat2Z.inj_add. reflexivity.
+Qed.
Lemma concat_all_size :
- forall a lbb bb bb',
+ forall lbb a bb bb',
concat_all (a :: lbb) = OK bb ->
concat_all lbb = OK bb' ->
size bb = size a + size bb'.
Proof.
-Admitted.
-
-Lemma concat_all_equiv_cons:
- forall tge tf bb lbb tbb rs m rs'' m'',
- concat_all (bb::lbb) = OK tbb ->
- exec_bblock tge tf tbb rs m = Next rs'' m'' ->
- exists tbb' rs' m',
- exec_bblock tge tf bb rs m = Next rs' m'
- /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size bb))
- /\ concat_all lbb = OK tbb'
- /\ exec_bblock tge tf tbb' rs' m' = Next rs'' m''.
-Proof.
-Admitted.
+ intros. unfold concat_all in H. fold concat_all in H.
+ destruct lbb; try discriminate.
+ monadInv H. rewrite H0 in EQ. inv EQ.
+ apply concat2_size. assumption.
+Qed.
Lemma ptrofs_add_repr :
forall a b,
@@ -376,8 +480,10 @@ Proof.
induction lbb.
- intros until m'. simpl. intros. discriminate.
- intros until m'. intros GFIND SIZE PCeq TAIL CONC EXEB.
- exploit concat_all_equiv_cons; eauto.
- intros (tbb0 & rs0 & m0 & EXEB0 & PCeq' & CONC0 & EXEB1).
+ destruct lbb.
+ + simpl in *. clear IHlbb. inv CONC. eapply plus_one. econstructor; eauto. eapply find_bblock_tail; eauto.
+ + exploit concat_all_exec_bblock; eauto; try discriminate.
+ intros (tbb0 & rs0 & m0 & CONC0 & EXEB0 & PCeq' & EXEB1).
eapply plus_left.
econstructor.
3: eapply find_bblock_tail. rewrite <- app_comm_cons in TAIL. 3: eauto.
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-11 22:44:36 +0000