From 47a4ccade6f73e95be34cd2d55be3655302fff97 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 21 Mar 2019 20:29:57 +0100 Subject: begin jumptables (does not work) --- mppa_k1c/Asm.v | 2 ++ mppa_k1c/Asmblock.v | 11 +++++++++++ mppa_k1c/Asmblockdeps.v | 42 +++++++++++++++++++++++++++++++++++++++++- mppa_k1c/Asmblockgen.v | 5 +++-- 4 files changed, 57 insertions(+), 3 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 493f4a05..8c918c2d 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -69,6 +69,7 @@ Inductive instruction : Type := | Pj_l (l: label) (**r jump to label *) | Pcb (bt: btest) (r: ireg) (l: label) (**r branch based on btest *) | Pcbu (bt: btest) (r: ireg) (l: label) (**r branch based on btest with unsigned semantics *) + | Pjumptable (r: ireg) (labels: list label) | Ploopdo (count: ireg) (loopend: label) (** Loads **) @@ -228,6 +229,7 @@ Definition control_to_instruction (c: control) := | PCtlFlow (Asmblock.Pj_l l) => Pj_l l | PCtlFlow (Asmblock.Pcb bt r l) => Pcb bt r l | PCtlFlow (Asmblock.Pcbu bt r l) => Pcbu bt r l + | PCtlFlow (Asmblock.Pjumptable r label) => Pjumptable r label end. Definition basic_to_instruction (b: basic) := diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index d335801e..dfe46e04 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -233,6 +233,7 @@ Inductive cf_instruction : Type := | Pret (**r return *) | Pcall (l: label) (**r function call *) | Picall (r: ireg) (**r function call on register value *) + | Pjumptable (r: ireg) (labels: list label) (**r N-way branch through a jump table (pseudo) *) (* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *) | Pgoto (l: label) (**r goto *) @@ -1470,6 +1471,16 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) Next (rs#PC <- (rs#r)) m | Pj_l l => goto_label f l rs m + | Pjumptable r tbl => + match rs#r with + | Vint n => + match list_nth_z tbl (Int.unsigned n) with + | None => Stuck + | Some lbl => goto_label f lbl (rs #GPR62 <- Vundef #GPR63 <- Vundef) m + end + | _ => Stuck + end + | Pcb bt r l => match cmp_for_btest bt with | (Some c, Int) => eval_branch f l rs m (Val.cmp_bool c rs#r (Vint (Int.repr 0))) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 501ec212..8c799927 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -42,6 +42,7 @@ Inductive control_op := | Odivu | OError | OIncremPC (sz: Z) + | Ojumptable (l: list label) . Inductive arith_op := @@ -180,6 +181,15 @@ Definition eval_branch_deps (f: function) (l: label) (vpc: val) (res: option boo Definition control_eval (o: control_op) (l: list value) := let (ge, fn) := Ge in match o, l with + | (Ojumptable tbl), [Val index; Val vpc] => + match index with + | Vint n => + match list_nth_z tbl (Int.unsigned n) with + | None => None + | Some lbl => goto_label_deps fn lbl vpc + end + | _ => None + end | Oj_l l, [Val vpc] => goto_label_deps fn l vpc | Ocb bt l, [Val v; Val vpc] => match cmp_for_btest bt with @@ -540,6 +550,7 @@ Definition trans_control (ctl: control) : macro := | Pj_l l => [(#PC, Op (Control (Oj_l l)) (Name (#PC) @ Enil))] | Pcb bt r l => [(#PC, Op (Control (Ocb bt l)) (Name (#r) @ Name (#PC) @ Enil))] | Pcbu bt r l => [(#PC, Op (Control (Ocbu bt l)) (Name (#r) @ Name (#PC) @ Enil))] + | Pjumptable r labels => [(#PC, Op (Control (Ojumptable labels)) (Name (#r) @ Name (#PC) @ Enil)) ] | Pdiv => [(#GPR0, Op (Control Odiv) (Name (#GPR0) @ Name (#GPR1) @ Enil)); (#RA, Name (#RA))] | Pdivu => [(#GPR0, Op (Control Odivu) (Name (#GPR0) @ Name (#GPR1) @ Enil)); (#RA, Name (#RA))] | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)] @@ -879,8 +890,37 @@ Proof. Simpl. * Simpl. * intros rr; destruct rr; Simpl. destruct (preg_eq GPR0 g); Simpl. rewrite e. Simpl. + (* Pjumptable *) + + unfold goto_label in *. + destruct (nextblock b rs r) eqn:NB_r in *; try discriminate. + destruct (list_nth_z _ _) eqn:LI in *; try discriminate. + destruct (label_pos _ _ _) eqn:LPOS in *; try discriminate. + rewrite Pregmap.gso in H0; try discriminate. + rewrite Pregmap.gso in H0; try discriminate. + eexists; split; try split. + * simpl control_eval. + rewrite (H3 PC). + simpl. + unfold goto_label_deps. + Simpl. + rewrite H3. + destruct (rs r); try discriminate. + ++ + destruct (nextblock b rs PC) eqn:NB_PC in *; try discriminate. + inv H0. + + destruct (s (# PC)) eqn:sPC in *; try discriminate. + rewrite Pregmap.gso; try discriminate. + destruct (nextblock b rs r) eqn:NB_r in *; try discriminate. + destruct (list_nth_z _ _) eqn:LI in *; try discriminate. + destruct (label_pos _ _ _) eqn:LPOS in *; try discriminate. + destruct (nextblock b rs PC) eqn:NB_PC in *; try discriminate. + inv H1; try discriminate. + assumption. (* Pj_l *) - + unfold goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (nextblock _ _ _) eqn:NB; try discriminate. inv H0. + + unfold goto_label in H0. + destruct (label_pos _ _ _) eqn:LPOS; try discriminate. + destruct (nextblock _ _ _) eqn:NB; try discriminate. inv H0. eexists; split; try split. * simpl control_eval. pose (H3 PC); simpl in e; rewrite e. simpl. unfold goto_label_deps. rewrite LPOS. rewrite nextblock_pc in NB. rewrite NB. reflexivity. diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 5b00a64f..f3b4b921 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -911,8 +911,9 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co | MBreturn => OK (make_epilogue f (Pret ::g nil)) (*OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k))*) - | MBjumptable _ _ => - Error (msg "Asmblockgen.transl_instr_control MBjumptable") + | MBjumptable arg tbl => + do r <- ireg_of arg; + OK (Pjumptable r tbl ::g nil) end end. -- cgit