diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-24 21:04:52 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-24 21:04:52 +0100 |
commit | f2e3e4398f2be4a44146a323f729af452721f249 (patch) | |
tree | a38dca1ac9a56114a6a3788efa76b1c93141b90e /mppa_k1c | |
parent | 061c1a394b0c540d2c8bf996b2ef2776549e74bf (diff) | |
parent | 52aeb8026a9d9d2675eebf965d4ff3f87a0e2346 (diff) | |
download | compcert-kvx-f2e3e4398f2be4a44146a323f729af452721f249.tar.gz compcert-kvx-f2e3e4398f2be4a44146a323f729af452721f249.zip |
Merge branch 'mppa-mul' into mppa-ternary
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asm.v | 5 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 16 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 29 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 12 | ||||
-rw-r--r-- | mppa_k1c/Asmexpand.ml | 35 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 1 | ||||
-rw-r--r-- | mppa_k1c/SelectLong.vp | 1 | ||||
-rw-r--r-- | mppa_k1c/SelectLongproof.v | 1 | ||||
-rw-r--r-- | mppa_k1c/SelectOp.vp | 35 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 82 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 4 |
11 files changed, 115 insertions, 106 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 493f4a05..0ca554ab 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -50,9 +50,6 @@ Inductive instruction : Type := | Psemi (**r semi colon separating bundles *)
| Pnop (**r instruction that does nothing *)
- | Pdiv (**r 32 bits integer division *)
- | Pdivu (**r 32 bits integer division *)
-
(** builtins *)
| Pclzll (rd rs: ireg)
| Pstsud (rd rs1 rs2: ireg)
@@ -218,8 +215,6 @@ Inductive instruction : Type := Definition control_to_instruction (c: control) :=
match c with
| PExpand (Asmblock.Pbuiltin ef args res) => Pbuiltin ef args res
- | PExpand (Asmblock.Pdiv) => Pdiv
- | PExpand (Asmblock.Pdivu) => Pdivu
| PCtlFlow Asmblock.Pret => Pret
| PCtlFlow (Asmblock.Pcall l) => Pcall l
| PCtlFlow (Asmblock.Picall r) => Picall r
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index d335801e..fdec8ed2 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -178,10 +178,7 @@ Inductive ex_instruction : Type := | Pbtbl (r: ireg) (tbl: list label) (**r N-way branch through a jump table *) *) | Pbuiltin: external_function -> list (builtin_arg preg) - -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *) - | Pdiv (**r 32 bits integer division, call to __divdi3 *) - | Pdivu (**r 32 bits integer division, call to __udivdi3 *) -. + -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *). (** FIXME: comment not up to date ! @@ -1486,17 +1483,6 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) (** Pseudo-instructions *) | Pbuiltin ef args res => Stuck (**r treated specially below *) - | Pdiv => - match Val.divs (rs GPR0) (rs GPR1) with - | Some v => Next (rs # GPR0 <- v # RA <- (rs RA)) m - | None => Stuck - end - - | Pdivu => - match Val.divu (rs GPR0) (rs GPR1) with - | Some v => Next (rs # GPR0 <- v # RA <- (rs RA)) m - | None => Stuck - end end | None => Next rs m end. diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 501ec212..ad96ae87 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -540,8 +540,6 @@ 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))] - | 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)] end. @@ -863,22 +861,6 @@ Proof. intros. destruct ex. - simpl in *. inv H1. destruct c; destruct i; try discriminate. all: try (inv H0; eexists; split; try split; [ simpl control_eval; pose (H3 PC); simpl in e; rewrite e; reflexivity | Simpl | intros rr; destruct rr; Simpl]). - (* Pdiv *) - + destruct (Val.divs _ _) eqn:DIVS; try discriminate. inv H0. unfold nextblock in DIVS. repeat (rewrite Pregmap.gso in DIVS; try discriminate). - eexists; split; try split. - * simpl control_eval. pose (H3 PC); simpl in e; rewrite e; clear e. simpl. - Simpl. pose (H3 GPR0); rewrite e; clear e. pose (H3 GPR1); rewrite e; clear e. rewrite DIVS. - Simpl. - * Simpl. - * intros rr; destruct rr; Simpl. destruct (preg_eq GPR0 g); Simpl. rewrite e. Simpl. - (* Pdivu *) - + destruct (Val.divu _ _) eqn:DIVU; try discriminate. inv H0. unfold nextblock in DIVU. repeat (rewrite Pregmap.gso in DIVU; try discriminate). - eexists; split; try split. - * simpl control_eval. pose (H3 PC); simpl in e; rewrite e; clear e. simpl. - Simpl. pose (H3 GPR0); rewrite e; clear e. pose (H3 GPR1); rewrite e; clear e. rewrite DIVU. - Simpl. - * Simpl. - * intros rr; destruct rr; Simpl. destruct (preg_eq GPR0 g); Simpl. rewrite e. Simpl. (* Pj_l *) + unfold goto_label in H0. destruct (label_pos _ _ _) eqn:LPOS; try discriminate. destruct (nextblock _ _ _) eqn:NB; try discriminate. inv H0. eexists; split; try split. @@ -1070,12 +1052,6 @@ Lemma exec_exit_none: Proof. intros. inv H0. destruct ex as [ctl|]; try discriminate. destruct ctl; destruct i; try reflexivity; try discriminate. -(* Pdiv *) - - simpl in *. pose (H3 GPR0); rewrite e in H1; clear e. pose (H3 GPR1); rewrite e in H1; clear e. - destruct (Val.divs _ _); try discriminate; auto. -(* Pdivu *) - - simpl in *. pose (H3 GPR0); rewrite e in H1; clear e. pose (H3 GPR1); rewrite e in H1; clear e. - destruct (Val.divu _ _); try discriminate; auto. (* Pj_l *) - simpl in *. pose (H3 PC); simpl in e; rewrite e in H1. clear e. unfold goto_label_deps in H1. unfold goto_label. @@ -1187,11 +1163,6 @@ Lemma forward_simu_exit_stuck: Proof. intros. inv H1. destruct ex as [ctl|]; try discriminate. destruct ctl; destruct i; try discriminate; try (simpl; reflexivity). -(* Pdiv *) - - simpl in *. pose (H3 GPR0); simpl in e; rewrite e; clear e. pose (H3 GPR1); simpl in e; rewrite e; clear e. - destruct (Val.divs _ _); try discriminate; auto. - - simpl in *. pose (H3 GPR0); simpl in e; rewrite e; clear e. pose (H3 GPR1); simpl in e; rewrite e; clear e. - destruct (Val.divu _ _); try discriminate; auto. (* Pj_l *) - simpl in *. pose (H3 PC); simpl in e; rewrite e. unfold goto_label_deps. unfold goto_label in H0. destruct (label_pos _ _ _); auto. clear e. destruct (rs PC); auto. discriminate. diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 5b00a64f..c03e319c 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -425,18 +425,6 @@ Definition transl_op OK (mulimm32 rd rs1 n ::i k) | Omulhs, _ => Error(msg "Asmblockgen.transl_op: Omulhs") (* Normalement pas émis *) | Omulhu, _ => Error(msg "Asmblockgen.transl_op: Omulhu") (* Normalement pas émis *) - | Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.") - (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pdivw rd rs1 rs2 :: k) *) - | Odivu, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odivu: 32-bits division not supported yet. Please use 64-bits.") - (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Pdivuw rd rs1 rs2 :: k) *) - | Omod, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Omod: 32-bits modulo not supported yet. Please use 64-bits.") - (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Premw rd rs1 rs2 :: k) *) - | Omodu, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Omodu: 32-bits modulo not supported yet. Please use 64-bits.") - (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (Premuw rd rs1 rs2 :: k) *) | Oand, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pandw rd rs1 rs2 ::i k) diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index 1c9e4e4c..f1528389 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -124,9 +124,6 @@ let expand_annot_val kind txt targ args res = assert false (* Handling of memcpy *) -let offset_in_range ofs = - let ofs = Z.to_int64 ofs in -2048L <= ofs && ofs < 2048L - let emit_move dst r = if dst <> r then emit (Paddil(dst, r, Z.zero));; @@ -175,7 +172,7 @@ let expand_builtin_memcpy sz al args = | _ -> assert false;; (* Handling of volatile reads and writes *) - +(* FIXME probably need to check for size of displacement *) let expand_builtin_vload_common chunk base ofs res = match chunk, res with | Mint8unsigned, BR(Asmblock.IR res) -> @@ -211,21 +208,9 @@ let expand_builtin_vload chunk args res = | [BA(Asmblock.IR addr)] -> expand_builtin_vload_common chunk addr _0 res | [BA_addrstack ofs] -> - if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then - expand_builtin_vload_common chunk stack_pointer ofs res - else begin - assert false (* FIXME - expand_addptrofs Asmblock.GPR32 stack_pointer ofs; (* X31 <- sp + ofs *) - expand_builtin_vload_common chunk GPR32 _0 res *) - end + expand_builtin_vload_common chunk stack_pointer ofs res | [BA_addptr(BA(Asmblock.IR addr), (BA_int ofs | BA_long ofs))] -> - if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then - expand_builtin_vload_common chunk addr ofs res - else begin - assert false (* FIXME - expand_addptrofs Asmblock.GPR32 addr ofs; (* X31 <- addr + ofs *) - expand_builtin_vload_common chunk Asmblock.GPR32 _0 res *) - end + expand_builtin_vload_common chunk addr ofs res | _ -> assert false @@ -256,19 +241,9 @@ let expand_builtin_vstore chunk args = | [BA(Asmblock.IR addr); src] -> expand_builtin_vstore_common chunk addr _0 src | [BA_addrstack ofs; src] -> - if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then - expand_builtin_vstore_common chunk stack_pointer ofs src - else begin (* FIXME - expand_addptrofs X31 X2 ofs; (* X31 <- sp + ofs *) - expand_builtin_vstore_common chunk X31 _0 src *) - end + expand_builtin_vstore_common chunk stack_pointer ofs src | [BA_addptr(BA(Asmblock.IR addr), (BA_int ofs | BA_long ofs)); src] -> - if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then - expand_builtin_vstore_common chunk addr ofs src - else begin (* FIXME - expand_addptrofs X31 addr ofs; (* X31 <- addr + ofs *) - expand_builtin_vstore_common chunk X31 _0 src *) - end + expand_builtin_vstore_common chunk addr ofs src | _ -> assert false diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 2c39e342..56b00c7e 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -222,7 +222,6 @@ let basic_rec i = | Pnop -> { inst = "nop"; write_locs = []; read_locs = []; imm = None ; is_control = false} let expand_rec = function - | Pdiv | Pdivu -> { inst = "Pdiv"; write_locs = [Reg (IR GPR0)]; read_locs = [Reg (IR GPR0); Reg (IR GPR1)]; imm = None; is_control = true } | Pbuiltin _ -> raise OpaqueInstruction let ctl_flow_rec = function diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 3a17ab17..0c3618d7 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -21,6 +21,7 @@ Require Import Coqlib. Require Import Compopts. Require Import AST Integers Floats. Require Import Op CminorSel. +Require Import OpHelpers. Require Import SelectOp SplitLong. Local Open Scope cminorsel_scope. diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 4723278a..79187338 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -21,6 +21,7 @@ Require Import String Coqlib Maps Integers Floats Errors. Require Archi. Require Import AST Values Memory Globalenvs Events. Require Import Cminor Op CminorSel. +Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong SplitLongproof. Require Import SelectLong. diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index e4d65ced..f6605c11 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -15,6 +15,7 @@ (* *) (* *********************************************************************) + (** Instruction selection for operators *) (** The instruction selection pass recognizes opportunities for using @@ -49,9 +50,17 @@ Require Import Integers. Require Import Floats. Require Import Op. Require Import CminorSel. +Require Import OpHelpers. Local Open Scope cminorsel_scope. +Local Open Scope string_scope. +Local Open Scope error_monad_scope. + +Section SELECT. + +Context {hf: helper_functions}. + (** ** Constants **) Definition addrsymbol (id: ident) (ofs: ptrofs) := @@ -302,10 +311,17 @@ Nondetfunction notint (e: expr) := (** ** Integer division and modulus *) -Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). -Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil). -Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil). -Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil). +Definition divs_base (e1: expr) (e2: expr) := + Eexternal i32_sdiv sig_ii_i (e1 ::: e2 ::: Enil). + +Definition mods_base (e1: expr) (e2: expr) := + Eexternal i32_smod sig_ii_i (e1 ::: e2 ::: Enil). + +Definition divu_base (e1: expr) (e2: expr) := + Eexternal i32_udiv sig_ii_i (e1 ::: e2 ::: Enil). + +Definition modu_base (e1: expr) (e2: expr) := + Eexternal i32_umod sig_ii_i (e1 ::: e2 ::: Enil). Definition shrximm (e1: expr) (n2: int) := if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil). @@ -485,3 +501,14 @@ Nondetfunction builtin_arg (e: expr) := if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e | _ => BA e end. + +(* float division *) + +Definition divf_base (e1: expr) (e2: expr) := + (* Eop Odivf (e1 ::: e2 ::: Enil). *) + Eexternal f64_div sig_ff_f (e1 ::: e2 ::: Enil). + +Definition divfs_base (e1: expr) (e2: expr) := + (* Eop Odivf (e1 ::: e2 ::: Enil). *) + Eexternal f32_div sig_ss_s (e1 ::: e2 ::: Enil). +End SELECT. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 94d162a2..89af39ee 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -29,8 +29,13 @@ Require Import Cminor. Require Import Op. Require Import CminorSel. Require Import SelectOp. +Require Import Events. +Require Import OpHelpers. +Require Import OpHelpersproof. Local Open Scope cminorsel_scope. +Local Open Scope string_scope. + (** * Useful lemmas and tactics *) @@ -80,12 +85,53 @@ Ltac TrivialExists := (** * Correctness of the smart constructors *) Section CMCONSTR. - -Variable ge: genv. +Variable prog: program. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared prog hf. +Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. +(* Helper lemmas - from SplitLongproof.v *) + +Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto. +Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto. + +Lemma eval_helper: + forall le id name sg args vargs vres, + eval_exprlist ge sp e m le args vargs -> + helper_declared prog id name sg -> + external_implements name sg vargs vres -> + eval_expr ge sp e m le (Eexternal id sg args) vres. +Proof. + intros. + red in H0. apply Genv.find_def_symbol in H0. destruct H0 as (b & P & Q). + rewrite <- Genv.find_funct_ptr_iff in Q. + econstructor; eauto. +Qed. + +Corollary eval_helper_1: + forall le id name sg arg1 varg1 vres, + eval_expr ge sp e m le arg1 varg1 -> + helper_declared prog id name sg -> + external_implements name sg (varg1::nil) vres -> + eval_expr ge sp e m le (Eexternal id sg (arg1 ::: Enil)) vres. +Proof. + intros. eapply eval_helper; eauto. constructor; auto. constructor. +Qed. + +Corollary eval_helper_2: + forall le id name sg arg1 arg2 varg1 varg2 vres, + eval_expr ge sp e m le arg1 varg1 -> + eval_expr ge sp e m le arg2 varg2 -> + helper_declared prog id name sg -> + external_implements name sg (varg1::varg2::nil) vres -> + eval_expr ge sp e m le (Eexternal id sg (arg1 ::: arg2 ::: Enil)) vres. +Proof. + intros. eapply eval_helper; eauto. constructor; auto. constructor; auto. constructor. +Qed. + (** We now show that the code generated by "smart constructor" functions such as [Selection.notint] behaves as expected. Continuing the [notint] example, we show that if the expression [e] @@ -557,7 +603,8 @@ Theorem eval_divs_base: Val.divs x y = Some z -> exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold divs_base. exists z; split. EvalOp. auto. + intros; unfold divs_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_mods_base: @@ -567,7 +614,8 @@ Theorem eval_mods_base: Val.mods x y = Some z -> exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold mods_base. exists z; split. EvalOp. auto. + intros; unfold mods_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_divu_base: @@ -577,7 +625,8 @@ Theorem eval_divu_base: Val.divu x y = Some z -> exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold divu_base. exists z; split. EvalOp. auto. + intros; unfold divu_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_modu_base: @@ -587,7 +636,8 @@ Theorem eval_modu_base: Val.modu x y = Some z -> exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold modu_base. exists z; split. EvalOp. auto. + intros; unfold modu_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_shrximm: @@ -968,4 +1018,24 @@ Proof. - constructor; auto. Qed. +(* floating-point division *) +Theorem eval_divf_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v. +Proof. + intros; unfold divf_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. +Qed. + +Theorem eval_divfs_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v. +Proof. + intros; unfold divfs_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. +Qed. End CMCONSTR. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 9ab7ccd9..41a6622a 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -258,10 +258,6 @@ module Target (*: TARGET*) = fprintf oc " goto %a\n" symbol s | Pigoto(rs) -> fprintf oc " igoto %a\n" ireg rs - | Pdiv -> - fprintf oc " call __divdi3\n" - | Pdivu -> - fprintf oc " call __udivdi3\n" | Pj_l(s) -> fprintf oc " goto %a\n" print_label s | Pcb (bt, r, lbl) | Pcbu (bt, r, lbl) -> |