source: src/RTLabs/RTLAbstoRTL.ma @ 1054

include "RTLabs/syntax.ma".
include "RTL/RTL.ma".
include "common/AssocList.ma".
include "common/Graphs.ma".
include "common/Maps.ma".
include "utilities/HMap.ma".

definition add_graph ≝
  λl: label.
  λstmt.
  λp.
  let rtl_if_luniverse' ≝ rtl_if_luniverse p in
  let rtl_if_runiverse' ≝ rtl_if_runiverse p in
  let rtl_if_sig' ≝ rtl_if_sig p in
  let rtl_if_result' ≝ rtl_if_result p in
  let rtl_if_params' ≝ rtl_if_params p in
  let rtl_if_locals' ≝ rtl_if_locals p in
  let rtl_if_stacksize' ≝ rtl_if_stacksize p in
  let rtl_if_graph' ≝ add ? ? (rtl_if_graph p) l stmt in
  let rtl_if_entry' ≝ rtl_if_entry p in
  let rtl_if_exit' ≝ rtl_if_exit p in
    mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig'
                             rtl_if_params' rtl_if_params' rtl_if_locals'
                             rtl_if_stacksize' rtl_if_graph' rtl_if_entry'
                             rtl_if_exit'.
      
definition fresh_label ≝
  λdef.
    match fresh LabelTag (rtl_if_luniverse def) with
    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
    | Error _ ⇒ None ?
    ].

axiom register_fresh: universe RegisterTag → register.

definition fresh_reg: rtl_internal_function → rtl_internal_function × register ≝
  λdef.
    let r ≝ register_fresh (rtl_if_runiverse def) in
    let locals ≝ r :: rtl_if_locals def in
    let rtl_if_luniverse' ≝ rtl_if_luniverse def in
    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
    let rtl_if_sig' ≝ rtl_if_sig def in
    let rtl_if_result' ≝ rtl_if_result def in
    let rtl_if_params' ≝ rtl_if_params def in
    let rtl_if_locals' ≝ locals in
    let rtl_if_stacksize' ≝ rtl_if_stacksize def in
    let rtl_if_graph' ≝ rtl_if_graph def in
    let rtl_if_entry' ≝ rtl_if_entry def in
    let rtl_if_exit' ≝ rtl_if_exit def in
      〈mk_rtl_internal_function
        rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig' rtl_if_result'
        rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
        rtl_if_entry' rtl_if_exit', r〉.
        
let rec fresh_regs (def: rtl_internal_function) (n: nat) on n ≝
  match n with
  [ O   ⇒ 〈def, [ ]〉
  | S n ⇒
    let 〈def, res〉 ≝ fresh_regs def n in
    let 〈def, r〉 ≝ fresh_reg def in
      〈def, r :: res〉
  ].

definition addr_regs ≝
  λregs.
  match regs with
  [ cons hd tl ⇒
    match tl with
    [ cons hd' tl' ⇒ Some (register × register) 〈hd, hd'〉
    | nil          ⇒ None (register × register)
    ]
  | nil ⇒ None (register × register) (* registers are not an address *)
  ].

let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
  match n with
  [ O ⇒ [ ]
  | S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n')
  ].

definition choose_rest ≝
  λA: Type[0].
  λleft, right: list A.
  match left with
  [ nil ⇒
    match right with
    [ nil ⇒ None ?
    | _ ⇒ Some ? right
    ]
  | _ ⇒ Some ? left
  ].

definition complete_regs ≝
  λdef.
  λsrcrs1.
  λsrcrs2.
  let nb_added ≝ abs ((length ? srcrs1) - (length ? srcrs2)) in
  let 〈def, added_regs〉 ≝ fresh_regs def nb_added in
    if gtb nb_added 0 then
      〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
    else
      〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.

definition size_of_sig_type ≝
  λsig.
  match sig with
  [ ASTint isize sign ⇒
    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
      isize' ÷ (nat_of_bitvector ? int_size)
  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
  | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
  ].
  cases not_implemented;
qed.

inductive register_type: Type[0] ≝
  | register_int: register → register_type
  | register_ptr: register → register → register_type.

definition local_env ≝ BitVectorTrie (list register).

definition mem_local_env ≝
  λr: register.
  match r with
  [ an_identifier w ⇒ member (list register) 16 w
  ].

definition add_local_env ≝
  λr: register.
  match r with
  [ an_identifier w ⇒ insert (list register) 16 w
  ].

definition find_local_env ≝
  λr: register.
  λbvt.
  match r with
  [ an_identifier w ⇒ lookup (list register) 16 w bvt [ ]
  ].

definition initialize_local_env_internal ≝
  λruniverse.
  λlenv.
  λr_sig.
  let 〈r, sig〉 ≝ r_sig in
  let size ≝ size_of_sig_type sig in
  let rs ≝ register_freshes runiverse size in
    add_local_env r rs lenv.

definition initialize_local_env ≝
  λruniverse.
  λregisters.
  λresult.
  let registers ≝ registers @
    match result with
    [ None ⇒ [ ]
    | Some rt ⇒ [ rt ]
    ]
  in
    foldl ? ? (initialize_local_env_internal runiverse) (Stub …) registers.
  
definition map_list_local_env_internal ≝
  λlenv.
  λres.
  λr.
    res @ (find_local_env r lenv).
    
definition map_list_local_env ≝
  λlenv.
  λregs.
    foldl ? ? (map_list_local_env_internal lenv) [ ] regs.

definition make_addr ≝
  λA.
  λlst: list A.
  λprf: length A lst = 2. (* do not use on arguments other than those of length 2 *)
  match lst return λx. length A x = 2 → A × A with
  [ nil ⇒ λlst_nil_prf. ?
  | cons hd tl ⇒ λprf.
    match tl return λx. length A x = 1 → A × A with
    [ nil ⇒ λtl_nil_prf. ?
    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
    ] ?
  ] prf.
  [1: normalize in lst_nil_prf;
      destruct(lst_nil_prf);
  |2: normalize in prf;
      destruct(prf)
      @e0
  |3: normalize in tl_nil_prf;
      destruct(tl_nil_prf);
  ]
qed.

definition find_and_addr ≝
  λr.
  λlenv.
    make_addr ? (find_local_env r lenv).

definition rtl_args ≝
  λregs_list.
  λlenv.
    flatten ? (map ? ? (
      λr. find_local_env r lenv) regs_list).

definition change_label ≝
  λlbl.
  λstmt: rtl_statement.
  match stmt with
  [ rtl_st_skip _ ⇒ rtl_st_skip lbl
  | rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl
  | rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl
  | rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl
  | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
  | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
  | rtl_st_opaccs opaccs d s1 s2 _ ⇒ rtl_st_opaccs opaccs d s1 s2 lbl
  | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
  | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
  | rtl_st_clear_carry _ ⇒ rtl_st_clear_carry lbl
  | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl
  | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl
  | rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl
  | rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl
  | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a
  | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
  | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2
  | rtl_st_return r ⇒ rtl_st_return r
  ].

(* Ack! Should generating a fresh label ever fail?  This seems to be a side-effect
   of implementing everything as a bitvector, which is bounded.  If we implemented
   labels as unbounded nats then this function will never fail.
*)
let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝
  match stmt_list with
  [ nil ⇒ Some ? def
  | cons hd tl ⇒
    match tl with
    [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
    | cons hd' tl' ⇒
      let tmp_lbl ≝ fresh_label def in
      match tmp_lbl with
      [ None ⇒ None ?
      | Some tmp_lbl ⇒
        let stmt ≝ change_label tmp_lbl hd in
        let def ≝ add_graph start_lbl stmt def in
          adds_graph tl tmp_lbl dest_lbl def
      ]
    ]
  ].

(* dpm: had to lift this into option *)
let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
                       (def: ?) on translate_list ≝
  match translate_list with
  [ nil ⇒ Some ? def
  | cons hd tl ⇒
    match tl with
    [ nil ⇒ hd start_lbl dest_lbl def
    | cons hd' tl' ⇒
      let tmp_lbl ≝ fresh_label def in
      match tmp_lbl with
      [ None ⇒ None ?
      | Some tmp_lbl ⇒
        match hd start_lbl tmp_lbl def with
        [ None ⇒ None ?
        | Some def ⇒ add_translates tl tmp_lbl dest_lbl def
        ]
      ]
    ]
  ].

definition translate_cst ≝
  λcst.
  λdestrs.
  λstart_lbl.
  λdest_lbl.
  λdef.
  match cst with
  [ cast_int i ⇒
    match destrs with
    [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
    | cons hd tl ⇒
      match tl with
      [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_int hd i dest_lbl) def)
      | cons hd' tl' ⇒ None ?
      ]
    ]
  | cast_addrsymbol id ⇒
    match destrs with
    [ nil ⇒ None ?
    | cons hd tl ⇒
      match tl with
      [ nil ⇒ None ?
      | cons hd' tl' ⇒
        Some ? (add_graph start_lbl (rtl_st_addr hd hd' id dest_lbl) def)
      ]
    ]
  | cast_offset off ⇒
    match destrs with
    [ nil ⇒ None ?
    | cons hd tl ⇒
      match tl with
      [ nil ⇒ None ?
      | cons hd' tl' ⇒
        let 〈def, tmpr〉 ≝ fresh_reg def in
        adds_graph [
          rtl_st_stack_addr hd hd' start_lbl;
          rtl_st_int tmpr off start_lbl;
          rtl_st_op2 Add hd hd tmpr start_lbl;
          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
          rtl_st_op2 Addc hd' hd' tmpr start_lbl
        ] start_lbl dest_lbl def
      ]
    ]
  | cast_stack ⇒ ?
  | cast_sizeof size ⇒ ?
  (* | cast_float f ⇒ None ? *) (* what are we doing with floats? *)
  ].

definition filter_and_to_list_local_env_internal ≝
  λlenv.
  λl.
  λr.
  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
  [ Some entry ⇒
    match entry with
    [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ])
    | register_int r ⇒ (l @ [ r ])
    ]
  | None       ⇒ [ ] (* dpm: should this be none? *)
  ].

definition filter_and_to_list_local_env ≝
  λlenv.
  λregisters.
    foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers.

definition list_of_register_type ≝
  λrt.
  match rt with
  [ register_ptr r1 r2 ⇒ [ r1; r2 ]
  | register_int r ⇒ [ r ]
  ].

definition find_and_list ≝
  λr.
  λlenv.
  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
  [ None      ⇒ [ ] (* dpm: should this be none? *)
  | Some lkup ⇒ list_of_register_type lkup
  ].

definition find_and_list_args ≝
  λargs.
  λlenv.
    map ? ? (λr. find_and_list r lenv) args.
  
(* dpm: horrendous, use dependent types.
  length destr = length srcrs *)
let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label)
                       (dest_lbl: label) (def: ?) ≝
  match destrs with
  [ nil ⇒
    match srcrs with
    [ nil        ⇒ Some ? def
    | cons hd tl ⇒ None ?
    ]
  | cons hd tl ⇒
    match srcrs with
    [ nil        ⇒ None ?
    | cons hd' tl' ⇒
      match tl with
      [ nil            ⇒
        match tl' with
        (* one element lists *)
        [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def)
        | cons hd'' tl'' ⇒ None ?
        ]
      | cons hd'' tl'' ⇒
        match tl' with
        [ nil ⇒ None ?
        (* multielement lists *)
        | cons hd''' tl''' ⇒
          let tmp_lbl ≝ fresh_label def in
          match tmp_lbl with
          [ None ⇒ None ?
          | Some tmp_lbl ⇒
            let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in
              translate_move tl tl' tmp_lbl dest_lbl def
          ]
        ]
      ]
    ]
  ].

definition extract_singleton ≝
  λA: Type[0].
  λl: list A.
  match l with
  [ nil ⇒ None ?
  | cons hd tl ⇒
    match tl with
    [ nil ⇒ Some ? hd
    | cons hd tl ⇒ None ?
    ]
  ].

definition extract_pair ≝
  λA: Type[0].
  λl: list A.
  match l with
  [ nil ⇒ None ?
  | cons hd tl ⇒
    match tl with
    [ nil ⇒ None ?
    | cons hd' tl' ⇒
      match tl' with
      [ nil ⇒ Some ? 〈hd, hd'〉
      | cons hd'' tl'' ⇒ None ?
      ]
    ]
  ].

definition translate_op1 ≝
  λop1.
  λdestrs.
  λsrcrs.
  λstart_lbl.
  λdest_lbl.
  λdef.
  match op1 with
  [ op_cast8_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
  | op_cast8_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
  | op_cast16_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def
  | op_cast16_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def
  | op_neg_int ⇒
    let dstr ≝ extract_singleton ? destrs in
    let srcr ≝ extract_singleton ? srcrs in
    match dstr with
    [ None ⇒ None ?
    | Some dstr ⇒
      match srcr with
      [ None ⇒ None ?
      | Some srcr ⇒
        adds_graph [
          rtl_st_op1 Cmpl dstr srcr start_lbl;
          rtl_st_op1 Inc dstr dstr start_lbl
        ] start_lbl dest_lbl def
      ]
    ]
  | op_not_int ⇒
    let dstr ≝ extract_singleton ? destrs in
    let srcr ≝ extract_singleton ? srcrs in
    match dstr with
    [ None ⇒ None ?
    | Some dstr ⇒
      match srcr with
      [ None ⇒ None ?
      | Some srcr ⇒
        adds_graph [
          rtl_st_op1 Cmpl dstr srcr start_lbl
        ] start_lbl dest_lbl def
      ]
    ]
  | op_id ⇒ translate_move destrs srcrs start_lbl dest_lbl def
  | op_ptr_of_int ⇒
    let destr12 ≝ extract_pair ? destrs in
    let srcr ≝ extract_singleton ? srcrs in
    match destr12 with
    [ None ⇒ None ?
    | Some destr12 ⇒
      let 〈destr1, destr2〉 ≝ destr12 in
      match srcr with
      [ None ⇒ None ?
      | Some srcr ⇒
        adds_graph [
          rtl_st_move destr1 srcr dest_lbl;
          rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl
        ] start_lbl dest_lbl def
      ]
    ]
  | op_int_of_ptr ⇒
    let destr ≝ extract_singleton ? destrs in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcrs with
      [ nil ⇒ None ?
      | cons srcr tl ⇒
        Some ? (add_graph start_lbl (rtl_st_move destr srcr dest_lbl) def)
      ]
    ]
  | op_not_bool ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcrs ≝ extract_singleton ? srcrs in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcrs with
      [ None ⇒ None ?
      | Some srcr ⇒
        let 〈def, tmpr〉 ≝ fresh_reg def in
        adds_graph [
          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
          rtl_st_clear_carry start_lbl;
          rtl_st_op2 Sub destr tmpr srcr start_lbl;
          rtl_st_int destr (bitvector_of_nat ? 0) dest_lbl;
          rtl_st_op2 Addc destr destr destr start_lbl;
          rtl_st_int tmpr (bitvector_of_nat ? 1) dest_lbl;
          rtl_st_op2 Xor destr destr tmpr start_lbl
        ] start_lbl dest_lbl def
      ]
    ]
  | _ ⇒ None ? (* error float *)
  ].

definition translate_condptr ≝
  λr1.
  λr2.
  λstart_lbl: label.
  λlbl_true: label.
  λlbl_false: label.
  λdef.
  let 〈def, tmpr〉 ≝ fresh_reg def in
    adds_graph [
      rtl_st_op2 Or tmpr r1 r2 start_lbl;
      rtl_st_cond_acc tmpr lbl_true lbl_false
    ] start_lbl start_lbl def.

(*
let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?)
                      (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝
  match op2 with
  [ op_add ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_op2 Add destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_sub ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_clear_carry start_lbl;
            rtl_st_op2 Sub destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_mul ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_opaccs Mul destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_div ⇒ None ? (* signed div not supported *)
  | op_divu ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_opaccs Divu destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_modu ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_opaccs Modu destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_mod ⇒ None ? (* signed mod not supported *)
  | op_and ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_op2 And destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_or ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_op2 Or destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_xor ⇒
    let destr ≝ extract_singleton ? destrs in
    let srcr1 ≝ extract_singleton ? srcrs1 in
    let srcr2 ≝ extract_singleton ? srcrs2 in
    match destr with
    [ None ⇒ None ?
    | Some destr ⇒
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          adds_graph [
            rtl_st_op2 Xor destr srcr1 srcr2 start_lbl
          ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_shru ⇒ None ? (* shifts not supported *)
  | op_shr ⇒ None ?
  | op_shl ⇒ None ?
  | op_addf ⇒ None ? (* floats not supported *)
  | op_subf ⇒ None ?
  | op_mulf ⇒ None ?
  | op_divf ⇒ None ?
  | op_cmpf _ ⇒ None ?
  | op_addp ⇒
    let destr12 ≝ extract_pair ? destrs in
    match destr12 with
    [ None         ⇒ None ?
    | Some destr12 ⇒
      let 〈destr1, destr2〉 ≝ destr12 in
      let srcr12 ≝ extract_pair ? srcrs1 in
      match srcr12 with
      [ None ⇒
        let srcr2 ≝ extract_singleton ? srcrs1 in
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          let srcr12 ≝ extract_pair ? srcrs2 in
          match srcr12 with
          [ None ⇒ None ?
          | Some srcr12 ⇒
            let 〈srcr11, srcr12〉 ≝ srcr12 in
            let 〈def, tmpr1〉 ≝ fresh_reg def in
            let 〈def, tmpr2〉 ≝ fresh_reg def in
              adds_graph [
                rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
                rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
                rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
                rtl_st_move destr1 tmpr1 start_lbl
              ] start_lbl dest_lbl def
          ]
        ]
      | Some srcr12 ⇒
        let 〈srcr11, srcr12〉 ≝ srcr12 in
        let srcr2 ≝ extract_singleton ? srcrs2 in
        match srcr2 with
        [ None       ⇒ None ?
        | Some srcr2 ⇒
          let 〈def, tmpr1〉 ≝ fresh_reg def in
          let 〈def, tmpr2〉 ≝ fresh_reg def in
            adds_graph [
              rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
              rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
              rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
              rtl_st_move destr1 tmpr1 start_lbl
            ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_subp ⇒
    let destr ≝ extract_singleton ? destrs in
    match destr with
    [ None ⇒
      let destr12 ≝ extract_pair ? destrs in
      match destr12 with
      [ None ⇒ None ?
      | Some destr12 ⇒
        let 〈destr1, destr2〉 ≝ destr12 in
        let srcr12 ≝ extract_pair ? srcrs1 in
        match srcr12 with
        [ None ⇒ None ?
        | Some srcr12 ⇒
          let 〈srcr11, srcr12〉 ≝ srcr12 in
          let srcr2 ≝ extract_singleton ? srcrs2 in
          match srcr2 with
          [ None ⇒ None ?
          | Some srcr2 ⇒
            adds_graph [
              rtl_st_clear_carry start_lbl;
              rtl_st_op2 Sub destr1 srcr11 srcr2 start_lbl;
              rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl;
              rtl_st_op2 Sub destr2 srcr12 destr2 start_lbl
            ] start_lbl dest_lbl def
          ]
        ] 
      ]
    | Some destr ⇒
      match srcrs1 with
      [ nil ⇒ None ?
      | cons srcr1 tl ⇒
        match srcrs2 with
        [ nil ⇒ None ?
        | cons srcr2 tl' ⇒
          let 〈def, tmpr1〉 ≝ fresh_reg def in
          let 〈def, tmpr2〉 ≝ fresh_reg def in
            adds_graph [
              rtl_st_op1 Cmpl tmpr1 srcr2 start_lbl;
              rtl_st_int tmpr2 (bitvector_of_nat ? 1) start_lbl;
              rtl_st_op2 Add tmpr1 tmpr1 tmpr2 start_lbl;
              rtl_st_op2 Add destr srcr1 tmpr1 start_lbl
            ] start_lbl dest_lbl def
        ]
      ]
    ]
  | op_cmp cmp ⇒
    match cmp with
    [ Compare_Equal ⇒
      add_translates [
        translate_op2 op_sub destrs srcrs1 srcrs2;
        translate_op1 op_not_bool destrs destrs
      ] start_lbl dest_lbl def
    | Compare_NotEqual ⇒
      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    | _ ⇒ None ?
    ]
  | op_cmpu cmp ⇒
    match cmp with
    [ Compare_Equal ⇒
      add_translates [
        translate_op2 op_sub destrs srcrs1 srcrs2;
        translate_op1 op_not_bool destrs destrs
      ] start_lbl dest_lbl def
    | Compare_NotEqual ⇒
      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    | Compare
    | _ ⇒ None ?
    ]
  | _ ⇒ ?
  ].

    | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
      let (def, tmpr) = fresh_reg def in
      adds_graph
        [RTL.St_clear_carry start_lbl ;
         RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
         RTL.St_int (destr, 0, start_lbl) ;
         RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
        start_lbl dest_lbl def

    | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
        destrs srcrs2 srcrs1 start_lbl dest_lbl def

    | AST.Op_cmpu AST.Cmp_le, _, _, _ ->
      add_translates
        [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ;
         translate_op1 AST.Op_notbool destrs destrs]
        start_lbl dest_lbl def

    | AST.Op_cmpu AST.Cmp_ge, _, _, _ ->
      add_translates
        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
         translate_op1 AST.Op_notbool destrs destrs]
        start_lbl dest_lbl def

    | AST.Op_cmp cmp, _, _, _ ->
      let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
      let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
      add_translates
        [translate_cst (AST.Cst_int 128) tmprs1 ;
         translate_cst (AST.Cst_int 128) tmprs2 ;
         translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ;
         translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ;
         translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2] 
        start_lbl dest_lbl def

    | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
      let (def, tmpr) = fresh_reg def in
      add_translates
        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ;
         translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ;
         translate_op2 AST.Op_or [destr] [destr] [tmpr] ;
         adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ;
         translate_op2 AST.Op_xor [destr] [destr] [tmpr]]
        start_lbl dest_lbl def

    | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
      let (def, tmpr1) = fresh_reg def in
      let (def, tmpr2) = fresh_reg def in
      add_translates
        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
         translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
         translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
        start_lbl dest_lbl def

    | AST.Op_cmpp AST.Cmp_gt, _, _, _ ->
      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
        destrs srcrs2 srcrs1 start_lbl dest_lbl def

    | AST.Op_cmpp AST.Cmp_le, _, _, _ ->
      add_translates
        [translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ;
         translate_op1 AST.Op_notbool destrs destrs]
        start_lbl dest_lbl def

    | AST.Op_cmpp AST.Cmp_ge, _, _, _ ->
      add_translates
        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
         translate_op1 AST.Op_notbool destrs destrs]
        start_lbl dest_lbl def

    | _ -> assert false (* wrong number of arguments *)
*)

definition translate_condcst ≝
  λcst.
  λstart_lbl: label.
  λlbl_true: label.
  λlbl_false: label.
  λdef.
  match cst with
  [ cast_int i ⇒
    let 〈def, tmpr〉 ≝ fresh_reg def in
    adds_graph [
      rtl_st_int tmpr i start_lbl;
      rtl_st_cond_acc tmpr lbl_true lbl_false
    ] start_lbl start_lbl def
  | cast_addr_symbol x ⇒
    let 〈def, r1〉 ≝ fresh_reg def in
    let 〈def, r2〉 ≝ fresh_reg def in
    let lbl ≝ fresh_label def in
    match lbl with
    [ None ⇒ None ?
    | Some lbl ⇒
      let def ≝ add_graph start_lbl (rtl_st_addr r1 r2 x lbl) def in
        translate_condptr r1 r2 lbl lbl_true lbl_false def
    ]
  | cast_stack_offset off ⇒
    let 〈def, r1〉 ≝ fresh_reg def in
    let 〈def, r2〉 ≝ fresh_reg def in
    let tmp_lbl ≝ fresh_label def in
    match tmp_lbl with
    [ None ⇒ None ?
    | Some tmp_lbl ⇒
      let def ≝ translate_cst (cast_stack_offset off) [r1; r2] start_lbl tmp_lbl def in
      match def with
      [ None ⇒ None ?
      | Some def ⇒ translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def
      ]
    ]
  | cast_float f ⇒ None ? (* error_float *)
  ].

definition size_of_op1_ret ≝
  λop.
  match op with
  [ op_cast8_unsigned ⇒ Some ? 1
  | op_cast8_signed ⇒ Some ? 1
  | op_cast16_unsigned ⇒ Some ? 1
  | op_cast16_signed ⇒ Some ? 1
  | op_neg_int ⇒ Some ? 1
  | op_not_int ⇒ Some ? 1
  | op_int_of_ptr ⇒ Some ? 1
  | op_ptr_of_int ⇒ Some ? 2
  | op_id ⇒ None ? (* invalid_argument *)
  | _ ⇒ None ? (* error_float *)
  ].

definition translate_cond1 ≝
  λop1.
  λsrcrs: list register.
  λstart_lbl: label.
  λlbl_true: label.
  λlbl_false: label.
  λdef.
  match op1 with
  [ op_id ⇒
    let srcr ≝ extract_singleton ? srcrs in
    match srcr with
    [ None ⇒
      let srcr12 ≝ extract_pair ? srcrs in
      match srcr12 with
      [ None ⇒ None ?
      | Some srcr12 ⇒
        let 〈srcr1, srcr2〉 ≝ srcr12 in
          translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def
      ]
    | Some srcr ⇒
      adds_graph [
        rtl_st_cond_acc srcr lbl_true lbl_false
      ] start_lbl start_lbl def
    ]
  | _     ⇒
    let size ≝ size_of_op1_ret op1 in
    match size with
    [ None ⇒ None ?
    | Some size ⇒
      let 〈def, destrs〉 ≝ fresh_regs def size in
      let lbl ≝ fresh_label def in
      match lbl with
      [ None ⇒ None ?
      | Some lbl ⇒
        let def ≝ translate_op1 op1 destrs srcrs start_lbl lbl def in
        match def with
        [ None ⇒ None ?
        | Some def ⇒
          let destr ≝ extract_singleton ? destrs in
          match destr with
          [ None ⇒
            let destr12 ≝ extract_pair ? destrs in
            match destr12 with
            [ None ⇒ None ?
            | Some destr12 ⇒
              let 〈destr1, destr2〉 ≝ destr12 in
                translate_condptr destr1 destr2 start_lbl lbl_true lbl_false def
            ]
          | Some destr ⇒
            adds_graph [
              rtl_st_cond_acc destr lbl_true lbl_false
            ] start_lbl start_lbl def
          ]
        ]
      ]
    ]
  ].

definition size_of_op2_ret ≝
  λn: nat.
  λop2.
  match op2 with
  [ op_add ⇒ Some ? 1
  | op_sub ⇒ Some ? 1
  | op_mul ⇒ Some ? 1
  | op_div ⇒ Some ? 1
  | op_divu ⇒ Some ? 1
  | op_mod ⇒ Some ? 1
  | op_modu ⇒ Some ? 1
  | op_and ⇒ Some ? 1
  | op_or ⇒ Some ? 1
  | op_xor ⇒ Some ? 1
  | op_shl ⇒ Some ? 1
  | op_shr ⇒ Some ? 1
  | op_shru ⇒ Some ? 1
  | op_cmp _ ⇒ Some ? 1
  | op_cmpu _ ⇒ Some ? 1
  | op_cmpp _ ⇒ Some ? 1
  | op_addp ⇒ Some ? 2
  | op_subp ⇒
    if eq_nat n 4 then
      Some ? 1
    else
      Some ? 2
  | _ ⇒ None ? (* error_float *)
  ].

axiom translate_op2:
  op2 → list register → list register → list register → label → label → rtl_internal_function → option rtl_internal_function.

definition translate_cond2 ≝
  λop2.
  λsrcrs1: list register.
  λsrcrs2: list register.
  λstart_lbl: label.
  λlbl_true: label.
  λlbl_false: label.
  λdef.
  match op2 with
  [ op_cmp cmp ⇒
    match cmp with
    [ Compare_Equal ⇒
      let srcr1 ≝ extract_singleton ? srcrs1 in
      match srcr1 with
      [ None ⇒ None ?
      | Some srcr1 ⇒
        let srcr2 ≝ extract_singleton ? srcrs2 in
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          let 〈def, tmpr〉 ≝ fresh_reg def in
          adds_graph [
            rtl_st_clear_carry start_lbl;
            rtl_st_op2 Sub tmpr srcr1 srcr2 start_lbl;
            rtl_st_cond_acc tmpr lbl_false lbl_true
          ] start_lbl start_lbl def
        ]
      ]
    | _ ⇒
      let n ≝ length ? srcrs1 + length ? srcrs2 in
      match size_of_op2_ret n op2 with
      [ None ⇒ None ?
      | Some size ⇒
        let 〈def, destrs〉 ≝ fresh_regs def size in
        let lbl ≝ fresh_label def in
        match lbl with
        [ None ⇒ None ?
        | Some lbl ⇒
          match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
          [ None ⇒ None ?
          | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
          ]
        ]
      ]
    ]
  | _ ⇒
    let n ≝ length ? srcrs1 + length ? srcrs2 in
    match size_of_op2_ret n op2 with
    [ None ⇒ None ?
    | Some size ⇒
      let 〈def, destrs〉 ≝ fresh_regs def size in
      let lbl ≝ fresh_label def in
      match lbl with
      [ None ⇒ None ?
      | Some lbl ⇒
        match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
        [ None ⇒ None ?
        | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
        ]
      ]
    ]
  ].

let rec addressing_pointer (mode: ?) (args: ?) (destr1: ?)
                           (destr2: ?) (start_lbl: label)
                           (dest_lbl: label) (def: rtl_internal_function) ≝
  let destrs ≝ [ destr1; destr2 ] in
  match mode with
  [ Aindexed off ⇒
    let srcr12 ≝ extract_singleton ? args in
    match srcr12 with
    [ None ⇒ None ?
    | Some srcr12 ⇒
      let srcr12 ≝ extract_pair ? srcr12 in
      match srcr12 with
      [ None ⇒ None ?
      | Some srcr12 ⇒
        let 〈srcr1, srcr2〉 ≝ srcr12 in
        let 〈def, tmpr〉 ≝ fresh_reg def in
        add_translates [
          adds_graph [
            rtl_st_int tmpr off start_lbl
          ];
          translate_op2 op_addp destrs [ srcr1 ; srcr2 ] [tmpr]
        ] start_lbl dest_lbl def
      ]
    ]
  | Aindexed2 ⇒
    let args_pair ≝ extract_pair ? args in
    match args_pair with
    [ None ⇒ None ?
    | Some args_pair ⇒
      let 〈lft, rgt〉 ≝ args_pair in
      let srcr1112 ≝ extract_pair ? lft in
      let srcr2 ≝ extract_singleton ? rgt in
      match srcr1112 with
      [ None ⇒
        let srcr2 ≝ extract_singleton ? rgt in
        let srcr1112 ≝ extract_pair ? lft in
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          match srcr1112 with
          [ None ⇒ None ?
          | Some srcr1112 ⇒
            let 〈srcr11, srcr12〉 ≝ srcr1112 in
            translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
          ]
        ]
      | Some srcr1112 ⇒
        let 〈srcr11, srcr12〉 ≝ srcr1112 in
        match srcr2 with
        [ None ⇒ None ?
        | Some srcr2 ⇒
          translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
        ]
      ]
    ]
  | Aglobal x off ⇒ 
    let 〈def, tmpr〉 ≝ fresh_reg def in
    add_translates [
      adds_graph [
        rtl_st_int tmpr off start_lbl;
        rtl_st_addr destr1 destr2 x start_lbl
      ];
      translate_op2 op_addp destrs destrs [ tmpr ]
    ] start_lbl dest_lbl def
  | Abased x off ⇒
    let srcrs ≝ extract_singleton ? args in
    match srcrs with
    [ None ⇒ None ?
    | Some srcrs ⇒
      let 〈def, tmpr1〉 ≝ fresh_reg def in
      let 〈def, tmpr2〉 ≝ fresh_reg def in
      (* mode, args, destr1, destr2, start_lbl, dest_lbl, def *)
      (* addressing_pointer (Aglobal x off) [ ] tmpr1 tmpr2; *)
      let address_unfold ≝
        let 〈def, tmpr〉 ≝ fresh_reg def in
          add_translates [
            adds_graph [
              rtl_st_int tmpr off start_lbl;
              rtl_st_addr tmpr1 tmpr2 x start_lbl
           ];
            translate_op2 op_addp destrs destrs [ tmpr ]
         ]
      in
      add_translates [
        address_unfold;
        translate_op2 op_addp destrs [ tmpr1; tmpr2 ] srcrs
      ] start_lbl dest_lbl def
    ]
  | Ainstack off ⇒
    let 〈def, tmpr〉 ≝ fresh_reg def in
    add_translates [
      adds_graph [
        rtl_st_int tmpr off start_lbl;
        rtl_st_stack_addr destr1 destr2 start_lbl
      ];
      translate_op2 op_addp destrs destrs [ tmpr ]
    ] start_lbl dest_lbl def
  | _ ⇒ None ? (* wrong number of arguments *)
  ].

definition translate_load ≝
  λq.
  λmode.
  λargs.
  λdestrs.
  λstart_lbl: label.
  λdest_lbl: label.
  λdef.
  match q with
  [ q_int b ⇒
    if eq_bv ? b (bitvector_of_nat ? 1) then
      match extract_singleton ? destrs with
      [ None ⇒ None ? (* error: size error in load *)
      | Some destr ⇒
        let 〈def, addr1〉 ≝ fresh_reg def in
        let 〈def, addr2〉 ≝ fresh_reg def in
          Some ? (add_translates [
            addressing_pointer mode args addr1 addr2;
            adds_graph [
              rtl_st_load destr addr1 addr2 start_lbl
            ]
          ] start_lbl dest_lbl def)
      ]
    else
      None ? (* error: size error in load *)
  | q_ptr ⇒
    match extract_pair ? destrs with
    [ None ⇒ None ? (* error: size error in load *)
    | Some destr12 ⇒
      let 〈destr1, destr2〉 ≝ destr12 in
      let 〈def, addr1〉 ≝ fresh_reg def in
      let 〈def, addr2〉 ≝ fresh_reg def in
      let addr ≝ [ addr1; addr2 ] in
      let 〈def, tmpr〉 ≝ fresh_reg def in
        Some ? (
          add_translates [
            addressing_pointer mode args addr1 addr2;
            adds_graph [
              rtl_st_load destr1 addr1 addr2 start_lbl;
              rtl_st_int tmpr (bitvector_of_nat ? 1) start_lbl
            ];
            translate_op2 op_addp addr addr [ tmpr ];
            adds_graph [
              rtl_st_load destr2 addr1 addr2 start_lbl
            ]
          ] start_lbl dest_lbl def
        )
    ]
  | _ ⇒ None ? (* error: size error in load *)
  ].
  
definition make_addr ≝
  λA: Type[0].
  λlst: list A.
  match lst with
  [ cons hd tl ⇒
    match tl with
    [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
    | _ ⇒ None ? (* do not use on these arguments *)
    ]
  | _ ⇒ None ? (* do not use on these arguments *)
  ].
  
definition translate_store_internal ≝
  λaddr.
  λtmp_addr.
  λtmpr.
  λstart_lbl.
  λdest_lbl.
  λtmp_addr1.
  λtmp_addr2.
  λtranslates_off.
  λsrcr.
    let 〈translates, off〉 ≝ translates_off in
    let translates ≝ translates @
      [ adds_graph [
          rtl_st_int tmpr off start_lbl
        ];
        translate_op2 op_addp tmp_addr addr [ tmpr ];
        adds_graph [
          rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
        ]
      ]
    in
    let 〈ignore, result〉 ≝ half_add ? off int_size in
      〈translates, result〉.
  
definition translate_store ≝
  λaddr.
  λsrcrs.
  λstart_lbl.
  λdest_lbl.
  λdef.
    let 〈def, tmp_addr〉 ≝ fresh_regs def (length ? addr) in
    match make_addr ? tmp_addr with
    [ None ⇒ None ?
    | Some tmp_addr12 ⇒
      let 〈tmp_addr1, tmp_addr2〉 ≝ tmp_addr12 in
      let 〈def, tmpr〉 ≝ fresh_reg def in
      let f ≝ translate_store_internal addr tmp_addr tmpr start_lbl dest_lbl tmp_addr1 tmp_addr2 in
      let 〈translates, ignore〉 ≝ foldl ? ? f 〈[], zero ?〉 srcrs in
        add_translates translates start_lbl dest_lbl def
    ].

definition translate_stmt ≝
  λlenv.
  λlbl.
  λstmt.
  λdef.
  match stmt with
  [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
  | St_cast destr cst lbl' ⇒
      translate_cst cst (find_local_env destr lenv) lbl lbl' def
  | _ ⇒ ?
  ].

let translate_stmt lenv lbl stmt def = match stmt with

  | RTLabs.St_skip lbl' ->
    add_graph lbl (RTL.St_skip lbl') def

  | RTLabs.St_cost (cost_lbl, lbl') ->
    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def

  | RTLabs.St_cst (destr, cst, lbl') ->
    translate_cst cst (find_local_env destr lenv) lbl lbl' def

  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
      lbl lbl' def

  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
    translate_op2 op2 (find_local_env destr lenv)
      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def

  | RTLabs.St_load (_, addr, destr, lbl') ->
    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
      lbl lbl' def

  | RTLabs.St_store (_, addr, srcr, lbl') ->
    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
      lbl lbl' def

  | RTLabs.St_call_id (f, args, None, _, lbl') ->
    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def

  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
                                   find_local_env retr lenv, lbl')) def

  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
    let (f1, f2) = find_and_addr f lenv in
    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def

  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
    let (f1, f2) = find_and_addr f lenv in
    add_graph lbl
      (RTL.St_call_ptr
         (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def

  | RTLabs.St_tailcall_id (f, args, _) ->
    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def

  | RTLabs.St_tailcall_ptr (f, args, _) ->
    let (f1, f2) = find_and_addr f lenv in
    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def

  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def

  | RTLabs.St_jumptable _ ->
    error "Jump tables not supported yet."

  | RTLabs.St_return None ->
    add_graph lbl (RTL.St_return []) def

  | RTLabs.St_return (Some r) ->
    add_graph lbl (RTL.St_return (find_local_env r lenv)) def