Ignore:
Timestamp:
Oct 6, 2011, 6:45:54 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
6 edited
1 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/RTLabs/RTLAbstoRTL.ma

    r1077 r1311  
    44include "common/FrontEndOps.ma".
    55include "common/Graphs.ma".
    6 
    7 definition add_graph ≝
    8   λl: label.
    9   λstmt.
    10   λp.
    11   let rtl_if_luniverse' ≝ rtl_if_luniverse p in
    12   let rtl_if_runiverse' ≝ rtl_if_runiverse p in
    13   let rtl_if_result' ≝ rtl_if_result p in
    14   let rtl_if_params' ≝ rtl_if_params p in
    15   let rtl_if_locals' ≝ rtl_if_locals p in
    16   let rtl_if_stacksize' ≝ rtl_if_stacksize p in
    17   let rtl_if_graph' ≝ add ? ? (rtl_if_graph p) l stmt in
    18   let rtl_if_entry' ≝ rtl_if_entry p in
    19   let rtl_if_exit' ≝ rtl_if_exit p in
    20     mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse'
    21                              rtl_if_params' rtl_if_params' rtl_if_locals'
    22                              rtl_if_stacksize' rtl_if_graph' ? ?.
    23   [1: cases(rtl_if_entry')
    24       #LABEL #HYP %
    25       [1: @LABEL
    26       |2: cases(HYP)
    27           generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l);
    28           normalize nodelta;
    29           /2/
    30       ]
    31   |2: cases(rtl_if_exit')
    32       #LABEL #HYP %
    33       [1: @LABEL
    34       |2: cases(HYP)
    35           generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l);
    36           normalize nodelta;
    37           /2/
    38       ]
    39   ]
    40 qed.
    41      
    42 definition fresh_label: rtl_internal_function → rtl_internal_function × label ≝
    43   λdef.
    44     let 〈lbl, new_univ〉 ≝ fresh LabelTag (rtl_if_luniverse def) in
    45     let locals ≝ rtl_if_locals def in
    46     let rtl_if_luniverse' ≝ new_univ in
    47     let rtl_if_runiverse' ≝ rtl_if_runiverse def in
    48     let rtl_if_result' ≝ rtl_if_result def in
    49     let rtl_if_params' ≝ rtl_if_params def in
    50     let rtl_if_locals' ≝ rtl_if_locals def in
    51     let rtl_if_stacksize' ≝ rtl_if_stacksize def in
    52     let rtl_if_graph' ≝ rtl_if_graph def in
    53     let rtl_if_entry' ≝ rtl_if_entry def in
    54     let rtl_if_exit' ≝ rtl_if_exit def in
    55       〈mk_rtl_internal_function
    56         rtl_if_luniverse' rtl_if_runiverse' rtl_if_result'
    57         rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
    58         rtl_if_entry' rtl_if_exit', lbl〉.
    59 
    60 axiom register_fresh: universe RegisterTag → register.
    61 
    62 definition fresh_reg: rtl_internal_function → rtl_internal_function × register ≝
    63   λdef.
    64     let r ≝ register_fresh (rtl_if_runiverse def) in
    65     let locals ≝ r :: rtl_if_locals def in
    66     let rtl_if_luniverse' ≝ rtl_if_luniverse def in
    67     let rtl_if_runiverse' ≝ rtl_if_runiverse def in
    68     let rtl_if_result' ≝ rtl_if_result def in
    69     let rtl_if_params' ≝ rtl_if_params def in
    70     let rtl_if_locals' ≝ locals in
    71     let rtl_if_stacksize' ≝ rtl_if_stacksize def in
    72     let rtl_if_graph' ≝ rtl_if_graph def in
    73     let rtl_if_entry' ≝ rtl_if_entry def in
    74     let rtl_if_exit' ≝ rtl_if_exit def in
    75       〈mk_rtl_internal_function
    76         rtl_if_luniverse' rtl_if_runiverse' rtl_if_result'
    77         rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
    78         rtl_if_entry' rtl_if_exit', r〉.
    79        
    80 let rec fresh_regs (def: rtl_internal_function) (n: nat) on n ≝
    81   match n with
    82   [ O   ⇒ 〈def, [ ]〉
    83   | S n ⇒
    84     let 〈def, res〉 ≝ fresh_regs def n in
    85     let 〈def, r〉 ≝ fresh_reg def in
    86       〈def, r :: res〉
    87   ].
    88 
    89 axiom fresh_regs_length:
    90   ∀def: rtl_internal_function.
    91   ∀n: nat.
    92     |(\snd (fresh_regs def n))| = n.
    93    
    94 definition addr_regs ≝
    95   λregs.
    96   match regs with
    97   [ cons hd tl ⇒
    98     match tl with
    99     [ cons hd' tl' ⇒ Some (register × register) 〈hd, hd'〉
    100     | nil          ⇒ None (register × register)
    101     ]
    102   | nil ⇒ None (register × register) (* registers are not an address *)
    103   ].
     6include "joint/TranslateUtils.ma".
    1047
    1058let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
    1069  match n with
    107   [ O ⇒ [ ]
    108   | S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n')
    109   ].
     10  [ O ⇒ 〈[],runiverse〉
     11  | S n' ⇒
     12     let 〈r,runiverse〉 ≝ fresh … runiverse in
     13     let 〈res,runiverse〉 ≝ register_freshes runiverse n' in
     14      〈r::res,runiverse〉 ].
    11015
    11116definition choose_rest ≝
     
    12934
    13035definition complete_regs ≝
     36  λglobals.
    13137  λdef.
    13238  λsrcrs1.
    13339  λsrcrs2.
    134   let nb_added ≝ abs ((length ? srcrs1) - (length ? srcrs2)) in
    135   let 〈def, added_regs〉 ≝ fresh_regs def nb_added in
    136     if gtb nb_added 0 then
    137       〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
    138     else
    139       〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
    140 
    141 (* obvious, but proof doesn't look easy! *)
    142 axiom complete_regs_length:
    143   ∀def.
    144   ∀left.
    145   ∀right.
    146     |\fst (\fst (complete_regs def left right))| = |\snd (\fst (complete_regs def left right))|.
     40  if leb (length … srcrs2) (length … srcrs1) then
     41   let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs1) (length ? srcrs2)) in
     42    〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
     43  else
     44   let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs2) (length ? srcrs1)) in
     45    〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
     46
     47lemma complete_regs_length:
     48  ∀globals,def,left,right.
     49   |\fst (\fst (complete_regs globals def left right))| = |\snd (\fst (complete_regs globals def left right))|.
     50 #globals #def #left #right
     51 whd in match complete_regs normalize nodelta
     52 @leb_elim normalize nodelta #H
     53 [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right)))
     54 | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)))]
     55 cases (fresh_regs ????) #def' #fresh normalize >append_length
     56 generalize in match H -H;
     57 generalize in match (length … left) generalize in match (length … right) generalize in match (length … fresh)
     58 [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H) -H #H #E >E >commutative_plus
     59         <plus_minus_m_m /2/ ]
     60qed.
    14761
    14862definition size_of_sig_type ≝
     
    16276  | register_ptr: register → register → register_type.
    16377
    164 definition local_env ≝ BitVectorTrie (list register).
    165 
    166 definition mem_local_env ≝
    167   λr: register.
    168   match r with
    169   [ an_identifier w ⇒ member (list register) 16 w
    170   ].
    171 
    172 definition add_local_env ≝
    173   λr: register.
    174   match r with
    175   [ an_identifier w ⇒ insert (list register) 16 w
    176   ].
    177 
    178 definition find_local_env ≝
    179   λr: register.
    180   λbvt.
    181   match r with
    182   [ an_identifier w ⇒ lookup (list register) 16 w bvt [ ]
    183   ].
     78definition local_env ≝ BitVectorTrie (list register) 16.
     79
     80definition mem_local_env : register → local_env → bool ≝
     81  λr. member … (word_of_identifier … r).
     82
     83definition add_local_env : register → list register → local_env → local_env ≝
     84  λr. insert … (word_of_identifier … r).
     85
     86definition find_local_env : register → local_env → list register ≝
     87  λr: register.λbvt. lookup … (word_of_identifier … r) bvt [].
    18488
    18589definition initialize_local_env_internal ≝
    186   λruniverse.
    187   λlenv.
     90  λlenv_runiverse.
    18891  λr_sig.
     92  let 〈lenv,runiverse〉 ≝ lenv_runiverse in
    18993  let 〈r, sig〉 ≝ r_sig in
    19094  let size ≝ size_of_sig_type sig in
    191   let rs ≝ register_freshes runiverse size in
    192     add_local_env r rs lenv.
     95  let 〈rs,runiverse〉 ≝ register_freshes runiverse size in
     96    〈add_local_env r rs lenv,runiverse〉.
    19397
    19498definition initialize_local_env ≝
     
    202106    ]
    203107  in
    204     foldl ? ? (initialize_local_env_internal runiverse) (Stub …) registers.
    205  
     108    foldl ? ? initialize_local_env_internal 〈Stub …,runiverse〉 registers.
     109
    206110definition map_list_local_env_internal ≝
    207   λlenv.
    208   λres.
    209   λr.
    210     res @ (find_local_env r lenv).
     111  λlenv,res,r. res @ (find_local_env r lenv).
    211112   
    212113definition map_list_local_env ≝
    213   λlenv.
    214   λregs.
    215     foldl ? ? (map_list_local_env_internal lenv) [ ] regs.
     114  λlenv,regs. foldl … (map_list_local_env_internal lenv) [ ] regs.
    216115
    217116definition make_addr ≝
     
    235134  |3: normalize in tl_nil_prf;
    236135      cases(not_le_Sn_O 0)
    237       #HYP cases(HYP tl_nil_prf)
    238   ]
     136      #HYP cases(HYP tl_nil_prf)]
    239137qed.
    240138
    241139definition find_and_addr ≝
    242   λr.
    243   λlenv.
    244     make_addr ? (find_local_env r lenv).
     140  λr,lenv. make_addr ? (find_local_env r lenv).
    245141
    246142definition rtl_args ≝
    247   λregs_list.
    248   λlenv.
    249     flatten ? (map ? ? (
    250       λr. find_local_env r lenv) regs_list).
    251 
    252 definition change_label ≝
    253   λlbl.
    254   λstmt: rtl_statement.
    255   match stmt with
    256   [ rtl_st_skip _ ⇒ rtl_st_skip lbl
    257   | rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl
    258   | rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl
    259   | rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl
    260   | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
    261   | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
    262   | rtl_st_opaccs opaccs d s1 s2 s3 _ ⇒ rtl_st_opaccs opaccs d s1 s2 s3 lbl
    263   | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
    264   | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
    265   | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl
    266   | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl
    267   | rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl
    268   | rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl
    269   | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a
    270   | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
    271   | rtl_st_cond r l1 l2 ⇒ rtl_st_cond r l1 l2
    272   | rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl
    273   | rtl_st_set_carry l ⇒ rtl_st_set_carry lbl
    274   | rtl_st_return ⇒ rtl_st_return
    275   ].
    276 
    277 (* Ack! Should generating a fresh label ever fail?  This seems to be a side-effect
    278    of implementing everything as a bitvector, which is bounded.  If we implemented
    279    labels as unbounded nats then this function will never fail.
    280 *)
    281 (* Fixed with changes to label generation.
    282 *)
    283 let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝
    284   match stmt_list with
    285   [ nil ⇒ def
    286   | cons hd tl ⇒
    287     match tl with
    288     [ nil ⇒ add_graph start_lbl (change_label dest_lbl hd) def
    289     | cons hd' tl' ⇒
    290       let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
    291       let stmt ≝ change_label tmp_lbl hd in
    292       let def ≝ add_graph start_lbl stmt new_def in
    293         adds_graph tl tmp_lbl dest_lbl new_def
    294     ]
    295   ].
    296 
    297 let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
    298                        (def: ?) on translate_list ≝
    299   match translate_list with
    300   [ nil ⇒ def
    301   | cons hd tl ⇒
    302     match tl with
    303     [ nil ⇒ hd start_lbl dest_lbl def
    304     | cons hd' tl' ⇒
    305       let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
    306       let applied ≝ hd start_lbl tmp_lbl new_def in
    307         add_translates tl tmp_lbl dest_lbl applied
    308     ]
    309   ].
     143  λregs_list,lenv. flatten … (map … (λr. find_local_env r lenv) regs_list).
    310144
    311145definition translate_cst_int_internal ≝
    312   λdest_lbl.
    313   λr.
    314   λi.
    315     rtl_st_int r i dest_lbl.
    316 
     146  λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl.
     147
     148(*CSC: XXXXX *)
    317149axiom translate_cst:
     150  ∀globals.
    318151  ∀cst: constant.
    319152  ∀destrs: list register.
    320153  ∀start_lbl: label.
    321154  ∀dest_lbl: label.
    322   ∀def: rtl_internal_function.
    323     rtl_internal_function.
     155  ∀def: rtl_internal_function globals.
     156    rtl_internal_function globals.
    324157
    325158definition translate_move_internal ≝
    326   λstart_lbl: label.
     159  λglobals.
    327160  λdestr: register.
    328161  λsrcr: register.
    329     rtl_st_move destr srcr start_lbl.
     162    sequential rtl_params_ globals (MOVE … 〈destr,srcr〉).
    330163
    331164definition translate_move ≝
     165  λglobals.
    332166  λdestrs: list register.
    333167  λsrcrs: list register.
     
    339173      let restl ≝ \snd (\fst crl_crr) in
    340174      let restr ≝ \snd (\snd crl_crr) in
    341       let f_common ≝ translate_move_internal start_lbl in
    342       let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
    343       let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
    344         add_translates [ translate1 ; translate2 ] start_lbl
     175      let f_common ≝ translate_move_internal globals in
     176      let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in
     177      let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
     178        add_translates [ translate1 ; translate2 ] start_lbl
    345179    ].
    346180    @len_proof
     
    368202
    369203definition translate_cast_unsigned ≝
     204  λglobals.
    370205  λdestrs.
    371206  λstart_lbl.
    372207  λdest_lbl.
    373   λdef.
    374   let 〈def, tmp_zero〉 ≝ fresh_reg def in
    375   let zeros ≝ make ? tmp_zero (length ? destrs) in
    376     add_translates [
    377       adds_graph [
    378         rtl_st_int tmp_zero (bitvector_of_nat ? 0) start_lbl
     208  λdef: joint_internal_function … (rtl_params globals).
     209  let 〈def, tmp_zero〉 ≝ fresh_reg def in
     210  let zeros ≝ make … tmp_zero (length … destrs) in
     211    add_translates [
     212      adds_graph rtl_params1 … [
     213        sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0))
    379214        ];
    380       translate_move destrs zeros
     215      translate_move globals destrs zeros
    381216    ] start_lbl dest_lbl def.
    382217
    383 definition translate_cast_signed ≝
     218definition translate_cast_signed:
     219    ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
     220  λglobals: list ident.
    384221  λdestrs.
    385222  λsrcr.
     
    387224  λdest_lbl.
    388225  λdef.
    389   let 〈def, tmp_128〉 ≝ fresh_reg def in
    390   let 〈def, tmp_255〉 ≝ fresh_reg def in
    391   let 〈def, tmpr〉 ≝ fresh_reg def in
    392   let 〈def, dummy〉 ≝ fresh_reg def in
     226  let 〈def, tmp_128〉 ≝ fresh_reg def in
     227  let 〈def, tmp_255〉 ≝ fresh_reg def in
     228  let 〈def, tmpr〉 ≝ fresh_reg def in
     229  let 〈def, dummy〉 ≝ fresh_reg def in
    393230  let insts ≝ [
    394     rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl;
    395     rtl_st_op2 And tmpr tmp_128 srcr start_lbl;
    396     rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl;
    397     rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl;
    398     rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl
    399   ] in
    400   let srcrs ≝ make ? tmpr (length ? destrs) in
    401     add_translates [
    402       adds_graph insts;
    403       translate_move destrs srcrs
     231    sequential  … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128));
     232    sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr);
     233    sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128);
     234    sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255));
     235    sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255)
     236  ]
     237  in
     238  let srcrs ≝ make … tmpr (length … destrs) in
     239    add_translates rtl_params1 globals [
     240      adds_graph rtl_params1 globals insts;
     241      translate_move globals destrs srcrs
    404242    ] start_lbl dest_lbl def.
    405243
    406244definition translate_cast ≝
    407   λsrc_size.
    408   λsrc_sign.
    409   λdest_size.
    410   λdestrs.
    411   λsrcrs.
     245  λglobals: list ident.
     246  λsrc_size: nat.
     247  λsrc_sign: signedness.
     248  λdest_size: nat.
     249  λdestrs: list register.
     250  λsrcrs: list register.
    412251  match |srcrs| return λx. |srcrs| = x → ? with
    413   [ O ⇒ λzero_prf. adds_graph [ ]
     252  [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ]
    414253  | S n' ⇒ λsucc_prf.
    415254    if ltb dest_size src_size then
    416       translate_move destrs srcrs
     255      translate_move globals destrs srcrs
    417256    else
    418257      match reduce_strong register register destrs srcrs with
     
    422261        let restl ≝ \snd (\fst crl) in
    423262        let restr ≝ \snd (\snd crl) in
    424         let insts_common ≝ translate_move commonl commonr in
     263        let insts_common ≝ translate_move globals commonl commonr in
    425264        let sign_reg ≝ last_safe ? srcrs ? in
    426265        let insts_sign ≝
    427266          match src_sign with
    428           [ Unsigned ⇒ translate_cast_unsigned restl
    429           | Signed ⇒ translate_cast_signed restl sign_reg
     267          [ Unsigned ⇒ translate_cast_unsigned globals restl
     268          | Signed ⇒ translate_cast_signed globals restl sign_reg
    430269          ]
    431270        in
    432           add_translates [ insts_common; insts_sign ]
     271          add_translates rtl_params1 globals [ insts_common; insts_sign ]
    433272      ]
    434273  ] (refl ? (|srcrs|)).
     
    437276
    438277definition translate_negint ≝
    439   λdestrs.
    440   λsrcrs.
    441   λstart_lbl.
    442   λdest_lbl.
    443   λdef.
    444   λprf: | destrs | = | srcrs |. (* assert in caml code *)
    445   let 〈def, tmpr〉 ≝ fresh_reg def in
    446   let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
    447   let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in
     278  λglobals: list ident.
     279  λdestrs: list register.
     280  λsrcrs: list register.
     281  λstart_lbl: label.
     282  λdest_lbl: label.
     283  λdef: rtl_internal_function globals.
     284  λprf: |destrs| = |srcrs|. (* assert in caml code *)
     285  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     286  let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in
     287  let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in
    448288  let insts_init ≝ [
    449     rtl_st_set_carry start_lbl;
    450     rtl_st_int tmpr (zero ?) start_lbl
     289    sequential … (SET_CARRY …);
     290    sequential … (INT rtl_params_ globals tmpr (zero ?))
    451291  ] in
    452   let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lbl in
     292  let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in
    453293  let insts_add ≝ map … f_add destrs in
    454     adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
    455 
    456 definition translate_notbool ≝
    457   λdestrs.
    458   λsrcrs.
    459   λstart_lbl.
    460   λdest_lbl.
    461   λdef.
     294    adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
     295
     296definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
     297  λglobals: list ident.
     298  λdestrs: list register.
     299  λsrcrs: list register.
     300  λstart_lbl: label.
     301  λdest_lbl: label.
     302  λdef: rtl_internal_function globals.
    462303  match destrs with
    463   [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     304  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def
    464305  | cons destr destrs ⇒
    465     let 〈def, tmpr〉 ≝ fresh_reg def in
    466     let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in
    467     let save_srcrs ≝ translate_move tmp_srcrs srcrs in
    468     let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lbl in
     306    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     307    let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in
     308    let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in
     309    let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in
    469310    let f ≝ λtmp_srcr. [
    470       rtl_st_clear_carry start_lbl;
    471       rtl_st_int tmpr (zero ?) start_lbl;
    472       rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl;
    473       rtl_st_int tmpr (zero ?) start_lbl;
    474       rtl_st_op2 Addc tmpr tmpr tmpr start_lbl;
    475       rtl_st_op2 Xor destr destr tmpr start_lbl
     311      sequential … (CLEAR_CARRY rtl_params_ globals);
     312      sequential … (INT rtl_params_ globals tmpr (zero ?));
     313      sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr);
     314      sequential … (INT rtl_params_ globals tmpr (zero ?));
     315      sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr);
     316      sequential … (OP2 rtl_params_ globals Xor destr destr tmpr)
    476317    ] in
    477     let insts ≝ init_destr :: (flatten ? (map … f tmp_srcrs)) in
    478     let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in
    479       add_translates [
    480         save_srcrs; adds_graph insts; epilogue
     318    let insts ≝ init_destr :: (flatten (map … f tmp_srcrs)) in
     319    let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
     320      add_translates rtl_params1 globals [
     321        save_srcrs; adds_graph rtl_params1 globals insts; epilogue
    481322      ] start_lbl dest_lbl def
    482323  ].
     
    488329*)
    489330definition translate_op1 ≝
     331  λglobals: list ident.
    490332  λop1: unary_operation.
    491333  λdestrs: list register.
     
    494336  λstart_lbl: label.
    495337  λdest_lbl: label.
    496   λdef: rtl_internal_function.
     338  λdef: rtl_internal_function globals.
    497339  match op1 with
    498340  [ Ocastint src_sign src_size ⇒
    499341    let dest_size ≝ |destrs| * 8 in
    500342    let src_size ≝ bitsize_of_intsize src_size in
    501       translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
     343      translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
    502344  | Onegint ⇒
    503       translate_negint destrs srcrs start_lbl dest_lbl def prf
     345      translate_negint globals destrs srcrs start_lbl dest_lbl def prf
    504346  | Onotbool ⇒
    505       translate_notbool destrs srcrs start_lbl dest_lbl def
     347      translate_notbool globals destrs srcrs start_lbl dest_lbl def
    506348  | Onotint ⇒
    507     let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
     349    let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in
    508350    let l ≝ map2 … f destrs srcrs prf in
    509       adds_graph l start_lbl dest_lbl def
     351      adds_graph rtl_params1 globals l start_lbl dest_lbl def
    510352  | Optrofint r ⇒
    511       translate_move destrs srcrs start_lbl dest_lbl def
     353      translate_move globals destrs srcrs start_lbl dest_lbl def
    512354  | Ointofptr r ⇒
    513       translate_move destrs srcrs start_lbl dest_lbl def
     355      translate_move globals destrs srcrs start_lbl dest_lbl def
    514356  | Oid ⇒
    515       translate_move destrs srcrs start_lbl dest_lbl def
     357      translate_move globals destrs srcrs start_lbl dest_lbl def
    516358  | _ ⇒ ? (* float operations implemented in runtime *)
    517359  ].
     
    519361qed.
    520362 
    521 definition translate_op ≝
     363definition translate_op: ∀globals. ? → list register → list register → list register →
     364  label → label → rtl_internal_function globals → rtl_internal_function globals ≝
     365  λglobals: list ident.
    522366  λop.
    523   λdestrs.
    524   λsrcrs1.
    525   λsrcrs2.
    526   λstart_lbl.
    527   λdest_lbl.
    528   λdef.
     367  λdestrs: list register.
     368  λsrcrs1: list register.
     369  λsrcrs2: list register.
     370  λstart_lbl: label.
     371  λdest_lbl: label.
     372  λdef: rtl_internal_function globals.
    529373  match reduce_strong register register srcrs1 srcrs2 with
    530374  [ dp reduced first_reduced_proof ⇒
     
    543387        let destrs_rest ≝ \snd (\fst reduced) in
    544388        let srcrs_cted ≝ \fst (\snd reduced) in
    545         let 〈def, tmpr〉 ≝ fresh_reg def in
     389        let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    546390        let insts_init ≝ [
    547           rtl_st_clear_carry start_lbl;
    548           rtl_st_int tmpr (zero ?) start_lbl
     391          sequential … (CLEAR_CARRY …);
     392          sequential … (INT rtl_params_ globals tmpr (zero …))
    549393        ] in
    550         let f_add ≝ λdestr. λsrcr1. λsrcr2. rtl_st_op2 op destr srcr1 srcr2 start_lbl in
    551         let insts_add ≝ map3 f_add destrs_common srcrsl_common srcrsr_common ? ? in
    552         let f_add_cted ≝ λdestr. λsrcr. rtl_st_op2 op destr srcr tmpr start_lbl in
    553         let insts_add_cted ≝ map2 ? ? ? f_add_cted destrs_cted srcrs_cted ? in
    554         let f_rest ≝ λdestr. rtl_st_op2 op destr tmpr tmpr start_lbl in
     394        let f_add ≝ λdestr. λsrcr1. λsrcr2. sequential … (OP2 rtl_params_ globals op destr srcr1 srcr2) in
     395        let insts_add ≝ map3 ? ? ? ? f_add destrs_common srcrsl_common srcrsr_common ? ? in
     396        let f_add_cted ≝ λdestr. λsrcr. sequential … (OP2 rtl_params_ globals op destr srcr tmpr) in
     397        let insts_add_cted ≝ map2 f_add_cted destrs_cted srcrs_cted ? in
     398        let f_rest ≝ λdestr. sequential … (OP2 rtl_params_ globals op destr tmpr tmpr) in
    555399        let insts_rest ≝ map … f_rest destrs_rest in
    556           adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
     400          adds_graph rtl_params1 globals (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
    557401      ]
    558402    ]
     
    560404  [1: @third_reduced_proof
    561405  |3: @first_reduced_proof
    562   |*: cases daemon (* TODO *)
     406  |*: cases daemon (* XXX: some of these look like they may be false *)
    563407  ]
    564408qed.
    565409
    566410let rec translate_mul1
    567   (dummy: register) (tmpr: register) (destrs: list register)
    568   (srcrs1: list register) (srcr2: register) (start_lbl: label)
    569     on srcrs1 ≝
     411  (globals: list ident) (dummy: register) (tmpr: register)
     412    (destrs: list register) (srcrs1: list register) (srcr2: register)
     413      (start_lbl: label)
     414        on srcrs1 ≝
    570415  match destrs with
    571   [ nil ⇒ adds_graph [ rtl_st_skip start_lbl ] start_lbl
     416  [ nil ⇒ adds_graph rtl_params1 globals [ GOTO … ] start_lbl
    572417  | cons destr tl ⇒
    573418    match tl with
     
    575420      match srcrs1 with
    576421      [ nil ⇒
    577         adds_graph [
    578           rtl_st_int tmpr (zero ?) start_lbl;
    579           rtl_st_op2 Addc destr destr tmpr start_lbl
     422        adds_graph rtl_params1 globals [
     423          sequential … (INT rtl_params_ globals tmpr (zero …));
     424          sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
    580425        ] start_lbl
    581426      | cons srcr1 tl' ⇒
    582         adds_graph [
    583           rtl_st_opaccs Mul tmpr dummy srcr2 srcr1 start_lbl;
    584           rtl_st_op2 Addc destr destr tmpr start_lbl
     427        adds_graph rtl_params1 globals [
     428          sequential … (OPACCS rtl_params_ globals Mul tmpr dummy srcr2 srcr1);
     429          sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
    585430        ] start_lbl
    586431      ]
     
    588433      match srcrs1 with
    589434      [ nil ⇒
    590         add_translates [
    591           adds_graph [
    592             rtl_st_int tmpr (zero ?) start_lbl;
    593             rtl_st_op2 Addc destr destr tmpr start_lbl;
    594             rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
     435        add_translates rtl_params1 globals [
     436          adds_graph rtl_params1 globals [
     437            sequential … (INT rtl_params_ globals tmpr (zero …));
     438            sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
     439            sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
    595440          ];
    596           translate_cst (Ointconst I8 (zero ?)) destrs
     441          translate_cst globals (Ointconst I8 (zero …)) destrs
    597442        ] start_lbl
    598443      | cons srcr1 srcrs1 ⇒
    599444        match destrs with
    600445        [ nil ⇒
    601           add_translates [
    602             adds_graph [
    603               rtl_st_int tmpr (zero ?) start_lbl;
    604               rtl_st_op2 Addc destr destr tmpr start_lbl;
    605               rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
     446          add_translates rtl_params1 globals [
     447            adds_graph rtl_params1 globals [
     448              sequential … (INT rtl_params_ globals tmpr (zero …));
     449              sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
     450              sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
    606451            ];
    607             translate_cst (Ointconst I8 (zero ?)) destrs
     452            translate_cst globals (Ointconst I8 (zero ?)) destrs
    608453          ] start_lbl
    609454        | cons destr2 destrs ⇒
    610           add_translates [
    611             adds_graph [
    612               rtl_st_opaccs Mul tmpr destr2 srcr2 srcr1 start_lbl;
    613               rtl_st_op2 Addc destr destr tmpr start_lbl
     455          add_translates rtl_params1 globals [
     456            adds_graph rtl_params1 globals [
     457              sequential … (OPACCS rtl_params_ globals Mul tmpr destr2 srcr2 srcr1);
     458              sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
    614459            ];
    615             translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2
     460            translate_mul1 globals dummy tmpr (destr2 :: destrs) srcrs1 srcr2
    616461          ] start_lbl
    617462        ]
     
    621466
    622467definition translate_muli ≝
     468  λglobals: list ident.
    623469  λdummy: register.
    624470  λtmpr: register.
     
    631477  λtranslates: list ?.
    632478  λsrcr2i: register.
    633   let 〈tmp_destrs1, tmp_destrs2〉 ≝ split ? tmp_destrs i i_prf in
     479  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split tmp_destrs i i_prf in
    634480  let tmp_destrs2' ≝
    635481    match tmp_destrs2 with
    636482    [ nil ⇒ [ ]
    637483    | cons tmp_destr2 tmp_destrs2 ⇒ [
    638         adds_graph [
    639           rtl_st_clear_carry dummy_lbl;
    640           rtl_st_int tmp_destr2 (zero ?) dummy_lbl
     484        adds_graph rtl_params1 globals [
     485          sequential rtl_params_ globals (CLEAR_CARRY …);
     486          sequential … (INT rtl_params_ globals tmp_destr2 (zero …))
    641487        ];
    642         translate_mul1 dummy tmpr tmp_destrs2 srcrs1 srcr2i;
    643         translate_cst (Ointconst I8 (zero ?)) tmp_destrs1;
    644         adds_graph [
    645           rtl_st_clear_carry dummy_lbl
     488        translate_mul1 globals dummy tmpr tmp_destrs2 srcrs1 srcr2i;
     489        translate_cst globals (Ointconst I8 (zero …)) tmp_destrs1;
     490        adds_graph rtl_params1 globals [
     491          sequential rtl_params_ globals (CLEAR_CARRY …)
    646492        ];
    647         translate_op Addc destrs destrs tmp_destrs
     493        translate_op globals Addc destrs destrs tmp_destrs
    648494      ]
    649495    ]
     
    652498
    653499axiom translate_mul:
     500  ∀globals: list ident.
    654501  ∀destrs: list register.
    655502  ∀srcrs1: list register.
     
    657504  ∀start_lbl: label.
    658505  ∀dest_lbl: label.
    659   ∀def: rtl_internal_function.
    660     rtl_internal_function.
     506  ∀def: rtl_internal_function globals.
     507    rtl_internal_function globals.
    661508
    662509(*
    663510definition translate_mul ≝
     511  λglobals: list ident.
    664512  λdestrs: list register.
    665513  λsrcrs1: list register.
     
    667515  λstart_lbl: label.
    668516  λdest_lbl: label.
    669   λdef: rtl_internal_function.
    670   let 〈def, dummy〉 ≝ fresh_reg def in
    671   let 〈def, tmpr〉 ≝ fresh_reg def in
    672   let 〈def, tmp_destrs〉 ≝ fresh_regs def (|destrs|) in
    673   let 〈def, fresh_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
    674   let 〈def, fresh_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
     517  λdef: rtl_internal_function globals.
     518  let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
     519  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     520  let 〈def, tmp_destrs〉 ≝ fresh_regs rtl_params0 globals def (|destrs|) in
     521  let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
     522  let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
    675523  let insts_init ≝ [
    676     translate_move fresh_srcrs1 srcrs1;
    677     translate_move fresh_srcrs2 srcrs2;
    678     translate_cst (Ointconst I8 (zero ?)) destrs
     524    translate_move globals fresh_srcrs1 srcrs1;
     525    translate_move globals fresh_srcrs2 srcrs2;
     526    translate_cst globals (Ointconst I8 (zero …)) destrs
    679527  ]
    680528  in
    681   let f ≝ λi. translate_muli dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in
    682   let insts_mul ≝ foldi ? ? [ ] srcrs2 in ?. [5: check insts_init.
     529  let f ≝ λi. translate_muli globals dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in
     530  let insts_mul ≝ foldi [ ] srcrs2 in ?. [5: check insts_init.
    683531    add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
    684532*)
    685533
    686534definition translate_divumodu8 ≝
     535  λglobals: list ident.
    687536  λorder: bool.
    688537  λdestrs: list register.
     
    691540  λstart_lbl: label.
    692541  λdest_lbl: label.
    693   λdef: rtl_internal_function.
     542  λdef: rtl_internal_function globals.
    694543  match destrs with
    695   [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     544  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
    696545  | cons destr destrs ⇒
    697     let 〈def, dummy〉 ≝ fresh_reg def in
     546    let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
    698547    let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉 | _ ⇒ 〈dummy, destr〉 ] in
    699     let inst_div ≝ adds_graph [
    700       rtl_st_opaccs DivuModu destr1 destr2 srcr1 srcr2 start_lbl
     548    let inst_div ≝ adds_graph rtl_params1 globals [
     549      sequential rtl_params_ globals (OPACCS … DivuModu destr1 destr2 srcr1 srcr2)
    701550    ]
    702551    in
    703     let insts_rest ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
    704       add_translates [ inst_div; insts_rest ] start_lbl dest_lbl def
    705   ].
    706 
    707 definition translate_ne: ? → ? → ? → ? → ? → ? → rtl_internal_function ≝
     552    let insts_rest ≝ translate_cst globals (Ointconst I8 (zero ?)) destrs in
     553      add_translates rtl_params1 globals [ inst_div; insts_rest ] start_lbl dest_lbl def
     554  ].
     555
     556definition translate_ne: ∀globals: list ident. ? → ? → ? → ? → ? → ? → rtl_internal_function globals ≝
     557  λglobals: list ident.
    708558  λdestrs: list register.
    709559  λsrcrs1: list register.
     
    711561  λstart_lbl: label.
    712562  λdest_lbl: label.
    713   λdef: rtl_internal_function.
     563  λdef: rtl_internal_function globals.
    714564  match destrs with
    715   [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     565  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
    716566  | cons destr destrs ⇒
    717     let 〈def, tmpr〉 ≝ fresh_reg def in
    718     let 〈def, tmp_zero〉 ≝ fresh_reg def in
    719     let 〈def, tmp_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
    720     let save_srcrs1 ≝ translate_move tmp_srcrs1 srcrs1 in
    721     let 〈def, tmp_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
    722     let save_srcrs2 ≝ translate_move tmp_srcrs2 srcrs2 in
     567    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     568    let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params0 globals def in
     569    let 〈def, tmp_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
     570    let save_srcrs1 ≝ translate_move globals tmp_srcrs1 srcrs1 in
     571    let 〈def, tmp_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
     572    let save_srcrs2 ≝ translate_move globals tmp_srcrs2 srcrs2 in
    723573    match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
    724574    [ dp crl their_proof ⇒
     
    729579      let rest ≝ choose_rest ? restl restr ? ? in
    730580      let inits ≝ [
    731         rtl_st_int destr (zero ?) start_lbl;
    732         rtl_st_int tmp_zero (zero ?) start_lbl
     581        sequential … (INT rtl_params_ globals destr (zero …));
     582        sequential … (INT rtl_params_ globals tmp_zero (zero …))
    733583      ]
    734584      in
    735585      let f_common ≝ λtmp_srcr1. λtmp_srcr2. [
    736         rtl_st_clear_carry start_lbl;
    737         rtl_st_op2 Sub tmpr tmp_srcr1 tmp_srcr2 start_lbl;
    738         rtl_st_op2 Or destr destr tmpr start_lbl
     586        sequential … (CLEAR_CARRY …);
     587        sequential … (OP2 rtl_params_ globals Sub tmpr tmp_srcr1 tmp_srcr2);
     588        sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
    739589      ]
    740590      in
    741       let insts_common ≝ flatten ? (map2 … f_common commonl commonr ?) in
     591      let insts_common ≝ flatten (map2 … f_common commonl commonr ?) in
    742592      let f_rest ≝ λtmp_srcr. [
    743         rtl_st_clear_carry start_lbl;
    744         rtl_st_op2 Sub tmpr tmp_zero tmp_srcr start_lbl;
    745         rtl_st_op2 Or destr destr tmpr start_lbl
     593        sequential … (CLEAR_CARRY …);
     594        sequential … (OP2 rtl_params_ globals Sub tmpr tmp_zero tmp_srcr);
     595        sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
    746596      ]
    747597      in
    748       let insts_rest ≝ flatten ? (map ? ? f_rest rest) in
     598      let insts_rest ≝ flatten … (map … f_rest rest) in
    749599      let insts ≝ inits @ insts_common @ insts_rest in
    750       let epilogue ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
    751         add_translates [
    752           save_srcrs1; save_srcrs2; adds_graph insts; epilogue
     600      let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
     601        add_translates rtl_params1 globals [
     602          save_srcrs1; save_srcrs2; adds_graph rtl_params1 globals insts; epilogue
    753603        ] start_lbl dest_lbl def
    754604    ]
     
    762612
    763613definition translate_eq_reg ≝
     614  λglobals: list ident.
    764615  λtmp_zero: register.
    765616  λtmp_one: register.
     
    770621  λsrcr12: register × register.
    771622  let 〈srcr1, srcr2〉 ≝ srcr12 in
    772   [ rtl_st_clear_carry dummy_lbl;
    773     rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
    774     rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
    775     rtl_st_op2 Sub tmpr2 srcr2 srcr1 dummy_lbl;
    776     rtl_st_op2 Addc tmpr2 tmp_zero tmp_zero dummy_lbl;
    777     rtl_st_op2 Or tmpr1 tmpr1 tmpr2 dummy_lbl;
    778     rtl_st_op2 Xor tmpr1 tmpr1 tmp_one dummy_lbl;
    779     rtl_st_op2 And destr destr tmpr1 dummy_lbl ].
     623  [ sequential … (CLEAR_CARRY …);
     624    sequential rtl_params_ globals (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
     625    sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
     626    sequential … (OP2 rtl_params_ globals Sub tmpr2 srcr2 srcr1);
     627    sequential … (OP2 rtl_params_ globals Addc tmpr2 tmp_zero tmp_zero);
     628    sequential … (OP2 rtl_params_ globals Or tmpr1 tmpr1 tmpr2);
     629    sequential … (OP2 rtl_params_ globals Xor tmpr1 tmpr1 tmp_one);
     630    sequential … (OP2 rtl_params_ globals And destr destr tmpr1) ].
    780631
    781632definition translate_eq_list ≝
     633  λglobals: list ident.
    782634  λtmp_zero: register.
    783635  λtmp_one: register.
     
    787639  λleq: list (register × register).
    788640  λdummy_lbl: label.
    789   let f ≝ translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
    790     (rtl_st_int destr (bitvector_of_nat ? 1) dummy_lbl) ::
    791       flatten ? (map ? ? f leq).
     641  let f ≝ translate_eq_reg globals tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
     642    (sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1))) ::
     643      flatten … (map … f leq).
    792644
    793645definition translate_atom ≝
     646  λglobals: list ident.
    794647  λtmp_zero: register.
    795648  λtmp_one: register.
     
    802655  λsrcr1: register.
    803656  λsrcr2: register.
    804     translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
    805     [ rtl_st_clear_carry dummy_lbl;
    806       rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
    807       rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
    808       rtl_st_op2 And tmpr3 tmpr3 tmpr1 dummy_lbl;
    809       rtl_st_op2 Or destr destr tmpr3 dummy_lbl ].
     657    translate_eq_list globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
     658    [ sequential … (CLEAR_CARRY …);
     659      sequential … (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
     660      sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
     661      sequential … (OP2 rtl_params_ globals And tmpr3 tmpr3 tmpr1);
     662      sequential … (OP2 rtl_params_ globals Or destr destr tmpr3) ].
    810663
    811664definition translate_lt_main ≝
     665  λglobals: list ident.
    812666  λtmp_zero: register.
    813667  λtmp_one: register.
     
    822676  let f ≝ λinsts_leq. λsrcr1. λsrcr2.
    823677    let 〈insts, leq〉 ≝ insts_leq in
    824     let added_insts ≝ translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
     678    let added_insts ≝ translate_atom globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
    825679      〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉
    826680  in
    827     \fst (fold_left2 ? ? ? f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).
     681    \fst (fold_left2 f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).
    828682
    829683definition fresh_regs_strong:
    830   rtl_internal_function → ∀n: nat. Σfresh: rtl_internal_function × (list register). |\snd fresh| = n ≝
     684  ∀globals. rtl_internal_function globals → ∀n: nat. Σfresh: (rtl_internal_function globals) × (list register). |\snd fresh| = n ≝
     685  λglobals: list ident.
    831686  λdef.
    832687  λn.
    833     fresh_regs def n.
     688    fresh_regs rtl_params0 globals def n.
    834689  @fresh_regs_length
    835690qed.
    836691
    837692definition complete_regs_strong:
    838   rtl_internal_function → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
     693  ∀globals: list ident. rtl_internal_function globals → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
     694  λglobals: list ident.
    839695  λdef.
    840696  λleft.
    841697  λright.
    842     complete_regs def left right.
     698    complete_regs globals def left right.
    843699  @complete_regs_length
    844700qed.
    845701
    846702definition translate_lt ≝
     703  λglobals: list ident.
    847704  λdestrs: list register.
    848705  λprf_destrs: lt 0 (|destrs|).
     
    851708  λstart_lbl: label.
    852709  λdest_lbl: label.
    853   λdef: rtl_internal_function.
     710  λdef: rtl_internal_function globals.
    854711  match destrs with
    855   [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     712  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
    856713  | _ ⇒
    857     match fresh_regs_strong def (|destrs|) with
     714    match fresh_regs_strong globals def (|destrs|) with
    858715    [ dp def_tmp_destrs tmp_destrs_proof ⇒
    859716      let def ≝ \fst def_tmp_destrs in
    860717      let tmp_destrs ≝ \snd def_tmp_destrs in
    861718      let tmp_destr ≝ hd_safe ? tmp_destrs ? in
    862       let 〈def, tmp_zero〉 ≝ fresh_reg def in
    863       let 〈def, tmp_one〉 ≝ fresh_reg def in
    864       let 〈def, tmpr1〉 ≝ fresh_reg def in
    865       let 〈def, tmpr2〉 ≝ fresh_reg def in
    866       let 〈def, tmpr3〉 ≝ fresh_reg def in
    867       match complete_regs_strong def srcrs1 srcrs2 with
     719      let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params1 globals def in
     720      let 〈def, tmp_one〉 ≝ fresh_reg rtl_params1 globals def in
     721      let 〈def, tmpr1〉 ≝ fresh_reg rtl_params1 globals def in
     722      let 〈def, tmpr2〉 ≝ fresh_reg rtl_params1 globals def in
     723      let 〈def, tmpr3〉 ≝ fresh_reg rtl_params1 globals def in
     724      match complete_regs_strong globals def srcrs1 srcrs2 with
    868725      [ dp srcrs12_added srcrs12_proof ⇒
    869726        let srcrs1 ≝ \fst (\fst srcrs12_added) in
    870727        let srcrs2 ≝ \snd (\fst srcrs12_added) in
    871728        let added ≝ \snd srcrs12_added in
    872         let srcrs1' ≝ rev ? srcrs1 in
    873         let srcrs2' ≝ rev ? srcrs2 in
     729        let srcrs1' ≝ rev srcrs1 in
     730        let srcrs2' ≝ rev srcrs2 in
    874731        let insts_init ≝ [
    875           translate_cst (Ointconst I8 (zero ?)) tmp_destrs;
    876           translate_cst (Ointconst I8 (zero ?)) added;
    877           adds_graph [
    878             rtl_st_int tmp_zero (zero ?) start_lbl;
    879             rtl_st_int tmp_one (bitvector_of_nat ? 1) start_lbl
     732          translate_cst globals (Ointconst I8 (zero ?)) tmp_destrs;
     733          translate_cst globals (Ointconst I8 (zero ?)) added;
     734          adds_graph rtl_params1 globals [
     735            sequential rtl_params_ globals (INT rtl_params_ globals tmp_zero (zero …));
     736            sequential rtl_params_ globals (INT rtl_params_ globals tmp_one (bitvector_of_nat … 1))
    880737          ]
    881738        ]
    882739        in
    883740        let insts_main ≝
    884           translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
    885           let insts_main ≝ [ adds_graph insts_main ] in
    886           let insts_exit ≝ [ translate_move destrs tmp_destrs ] in
    887             add_translates (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
     741          translate_lt_main globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
     742          let insts_main ≝ [ adds_graph rtl_params1 globals insts_main ] in
     743          let insts_exit ≝ [ translate_move globals destrs tmp_destrs ] in
     744            add_translates rtl_params1 globals (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
    888745      ]
    889746    ]
     
    897754
    898755definition add_128_to_last ≝
     756  λglobals: list ident.
    899757  λtmp_128: register.
    900758  λrs.
     
    902760  λstart_lbl: label.
    903761  match rs with
    904   [ nil ⇒ adds_graph [ ] start_lbl
     762  [ nil ⇒ adds_graph rtl_params1 globals [ ] start_lbl
    905763  | _ ⇒
    906     let r ≝ last_safe ? rs prf in
    907       adds_graph [
    908         rtl_st_op2 Add r r tmp_128 start_lbl
     764    let r ≝ last_safe rs prf in
     765      adds_graph rtl_params1 globals [
     766        sequential rtl_params_ globals (OP2 rtl_params_ globals Add r r tmp_128)
    909767      ] start_lbl
    910768  ].
    911769
    912770definition translate_lts ≝
     771  λglobals: list ident.
    913772  λdestrs: list register.
    914773  λdestrs_prf: lt 0 (|destrs|).
     
    919778  λstart_lbl: label.
    920779  λdest_lbl: label.
    921   λdef: rtl_internal_function.
    922   match fresh_regs_strong def (|srcrs1|) with
     780  λdef: rtl_internal_function globals.
     781  match fresh_regs_strong globals def (|srcrs1|) with
    923782  [ dp def_tmp_srcrs1 srcrs1_prf ⇒
    924783    let def ≝ \fst def_tmp_srcrs1 in
    925784    let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
    926     match fresh_regs_strong def (|srcrs2|) with
     785    match fresh_regs_strong globals def (|srcrs2|) with
    927786    [ dp def_tmp_srcrs2 srcrs2_prf ⇒
    928787      let def ≝ \fst def_tmp_srcrs2 in
    929788      let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
    930       let 〈def, tmp_128〉 ≝ fresh_reg def in
    931         add_translates [
    932           translate_move tmp_srcrs1 srcrs1;
    933           translate_move tmp_srcrs2 srcrs2;
    934           adds_graph [
    935             rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl
     789      let 〈def, tmp_128〉 ≝ fresh_reg rtl_params0 globals def in
     790        add_translates rtl_params1 globals [
     791          translate_move globals tmp_srcrs1 srcrs1;
     792          translate_move globals tmp_srcrs2 srcrs2;
     793          adds_graph rtl_params1 globals [
     794            sequential rtl_params_ globals (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128))
    936795          ];
    937           add_128_to_last tmp_128 tmp_srcrs1 ?;
    938           add_128_to_last tmp_128 tmp_srcrs2 ?;
    939           translate_lt destrs destrs_prf tmp_srcrs1 tmp_srcrs2
     796          add_128_to_last globals tmp_128 tmp_srcrs1 ?;
     797          add_128_to_last globals tmp_128 tmp_srcrs2 ?;
     798          translate_lt globals destrs destrs_prf tmp_srcrs1 tmp_srcrs2
    940799        ] start_lbl dest_lbl def
    941800    ]
     
    947806
    948807definition translate_op2 ≝
     808  λglobals: list ident.
    949809  λop2.
    950810  λdestrs: list register.
     
    958818  λstart_lbl: label.
    959819  λdest_lbl: label.
    960   λdef: rtl_internal_function.
     820  λdef: rtl_internal_function globals.
    961821  match op2 with
    962822  [ Oadd ⇒
    963     translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
     823    translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
    964824  | Oaddp ⇒
    965     translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
     825    translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
    966826  | Osub ⇒
    967     translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     827    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    968828  | Osubpi ⇒
    969     translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     829    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    970830  | Osubpp sz ⇒
    971     translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     831    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    972832  | Omul ⇒
    973     translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def
     833    translate_mul globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
    974834  | Odivu ⇒
    975     match srcrs1 return λx. 0 < |x| → rtl_internal_function with
     835    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
    976836    [ cons hd tl ⇒ λcons_prf.
    977837      match tl with
    978       [ nil ⇒ translate_divumodu8 true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
     838      [ nil ⇒ translate_divumodu8 globals true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
    979839      | _ ⇒ ? (* not implemented *)
    980840      ]
     
    982842    ] srcrs1_prf
    983843  | Omodu ⇒
    984     match srcrs1 return λx. 0 < |x| → rtl_internal_function with
     844    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
    985845    [ cons hd tl ⇒ λcons_prf.
    986846      match tl with
    987       [ nil ⇒ translate_divumodu8 false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
     847      [ nil ⇒ translate_divumodu8 globals false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
    988848      | _ ⇒ ? (* not implemented *)
    989849      ]
     
    991851    ] srcrs1_prf
    992852  | Oand ⇒
    993     translate_op And destrs srcrs1 srcrs2 start_lbl dest_lbl def
     853    translate_op globals And destrs srcrs1 srcrs2 start_lbl dest_lbl def
    994854  | Oor ⇒
    995     translate_op Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
     855    translate_op globals Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
    996856  | Oxor ⇒
    997     translate_op Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
     857    translate_op globals Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
    998858  | Ocmp c ⇒
    999859    match c with
    1000860    [ Ceq ⇒
    1001       add_translates [
    1002         translate_ne destrs srcrs1 srcrs2;
    1003         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     861      add_translates rtl_params1 globals [
     862        translate_ne globals destrs srcrs1 srcrs2;
     863        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    1004864      ] start_lbl dest_lbl def
    1005     | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
    1006     | Clt ⇒ translate_lts destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def
    1007     | Cgt ⇒ translate_lts destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def
     865    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
     866    | Clt ⇒ translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def
     867    | Cgt ⇒ translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def
    1008868    | Cle ⇒
    1009       add_translates [
    1010         translate_lts destrs destrs_prf srcrs2 srcrs1 ? ?;
    1011         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     869      add_translates rtl_params1 globals [
     870        translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ?;
     871        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    1012872      ] start_lbl dest_lbl def
    1013873    | Cge ⇒
    1014       add_translates [
    1015         translate_lts destrs destrs_prf srcrs1 srcrs2 ? ?;
    1016         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     874      add_translates rtl_params1 globals [
     875        translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ?;
     876        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    1017877      ] start_lbl dest_lbl def
    1018878    ]
     
    1020880    match c with
    1021881    [ Ceq ⇒
    1022       add_translates [
    1023         translate_ne destrs srcrs1 srcrs2;
    1024         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     882      add_translates rtl_params1 globals [
     883        translate_ne globals destrs srcrs1 srcrs2;
     884        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    1025885      ] start_lbl dest_lbl def
    1026     | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
    1027     | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
    1028     | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
     886    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
     887    | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
     888    | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
    1029889    | Cle ⇒
    1030       add_translates [
    1031         translate_lt destrs destrs_prf srcrs2 srcrs1;
    1032         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     890      add_translates rtl_params1 globals [
     891        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
     892        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    1033893      ] start_lbl dest_lbl def
    1034894    | Cge ⇒
    1035       add_translates [
    1036         translate_lt destrs destrs_prf srcrs1 srcrs2;
    1037         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     895      add_translates rtl_params1 globals [
     896        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
     897        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    1038898      ] start_lbl dest_lbl def
    1039899    ]
     
    1041901    match c with
    1042902    [ Ceq ⇒
    1043       add_translates [
    1044         translate_ne destrs srcrs1 srcrs2;
    1045         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     903      add_translates rtl_params1 globals [
     904        translate_ne globals destrs srcrs1 srcrs2;
     905        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    1046906      ] start_lbl dest_lbl def
    1047     | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
    1048     | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
    1049     | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
     907    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
     908    | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
     909    | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
    1050910    | Cle ⇒
    1051       add_translates [
    1052         translate_lt destrs destrs_prf srcrs2 srcrs1;
    1053         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     911      add_translates rtl_params1 globals [
     912        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
     913        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    1054914      ] start_lbl dest_lbl def
    1055915    | Cge ⇒
    1056       add_translates [
    1057         translate_lt destrs destrs_prf srcrs1 srcrs2;
    1058         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     916      add_translates rtl_params1 globals [
     917        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
     918        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    1059919      ] start_lbl dest_lbl def
    1060920    ]
     
    1070930qed.
    1071931
    1072 definition translate_cond ≝
     932definition translate_cond: ∀globals: list ident. list register → label → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
     933  λglobals: list ident.
    1073934  λsrcrs: list register.
    1074935  λstart_lbl: label.
    1075936  λlbl_true: label.
    1076937  λlbl_false: label.
    1077   λdef: rtl_internal_function.
    1078   let 〈def, tmpr〉 ≝ fresh_reg def in
    1079   let 〈def, tmp_lbl〉 ≝ fresh_label def in
    1080   let init ≝ rtl_st_int tmpr (zero ?) start_lbl in
    1081   let f ≝ λsrcr. rtl_st_op2 Or tmpr tmpr srcr start_lbl in
    1082   let def ≝ adds_graph (init :: (map … f srcrs)) start_lbl tmp_lbl def in
    1083     add_graph tmp_lbl (rtl_st_cond tmpr lbl_true lbl_false) def. 
     938  λdef: rtl_internal_function globals.
     939  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     940  let 〈tmp_lbl, def〉 ≝ fresh_label rtl_params1 globals def in
     941  let init ≝ sequential rtl_params_ globals (INT rtl_params_ globals tmpr (zero …)) in
     942  let f ≝ λsrcr. sequential rtl_params_ globals (OP2 rtl_params_ globals Or tmpr tmpr srcr) in
     943  let def ≝ adds_graph rtl_params1 globals (init :: (map ? ? f srcrs)) start_lbl tmp_lbl def in
     944    add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true) lbl_false) def.
    1084945
    1085946definition translate_load ≝
     947  λglobals: list ident.
    1086948  λaddr.
    1087949  λaddr_prf: 2 ≤ |addr|.
     
    1089951  λstart_lbl: label.
    1090952  λdest_lbl: label.
    1091   λdef: rtl_internal_function.
    1092   match fresh_regs_strong def (|addr|) with
     953  λdef: rtl_internal_function globals.
     954  match fresh_regs_strong rtl_params0 globals def (|addr|) with
    1093955  [ dp def_save_addr save_addr_prf ⇒
    1094956    let def ≝ \fst def_save_addr in
    1095957    let save_addr ≝ \snd def_save_addr in
    1096     match fresh_regs_strong def (|addr|) with
     958    match fresh_regs_strong rtl_params0 globals def (|addr|) with
    1097959    [ dp def_tmp_addr tmp_addr_prf ⇒
    1098960      let def ≝ \fst def_tmp_addr in
    1099961      let tmp_addr ≝ \snd def_tmp_addr in
    1100       let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
    1101       let 〈def, tmpr〉 ≝ fresh_reg def in
    1102       let insts_save_addr ≝ translate_move save_addr addr in
     962      let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr tmp_addr ? in
     963      let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     964      let insts_save_addr ≝ translate_move globals save_addr addr in
    1103965      let f ≝ λtranslates_off. λr.
    1104966        let 〈translates, off〉 ≝ translates_off in
    1105967        let translates ≝ translates @ [
    1106           adds_graph [
    1107             rtl_st_int tmpr off start_lbl
     968          adds_graph rtl_params1 globals [
     969            sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
    1108970          ];
    1109           translate_op2 Oaddp tmp_addr ? save_addr [tmpr] ? ?;
    1110           adds_graph [
    1111             rtl_st_load r tmp_addr1 tmp_addr2 dest_lbl
     971          translate_op2 globals Oaddp tmp_addr ? save_addr [tmpr] ? ?;
     972          adds_graph rtl_params1 globals [
     973            sequential rtl_params_ globals (LOAD rtl_params_ globals r tmp_addr1 tmp_addr2)
    1112974          ]
    1113975        ]
    1114976        in
    1115         let 〈carry, result〉 ≝ half_add ? off int_size in
     977        let 〈carry, result〉 ≝ half_add off int_size in
    1116978          〈translates, result〉
    1117979      in
    1118       let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], (zero ?)〉 destrs in
    1119         add_translates (insts_save_addr :: translates) start_lbl dest_lbl def
     980      let 〈translates, ignore〉 ≝ foldl f 〈[ ], (zero ?)〉 destrs in
     981        add_translates rtl_params1 globals (insts_save_addr :: translates) start_lbl dest_lbl def
    1120982    ]
    1121983  ].
     
    1130992
    1131993definition translate_store ≝
     994  λglobals: list ident.
    1132995  λaddr.
    1133996  λaddr_prf: 2 ≤ |addr|.
     
    1135998  λstart_lbl: label.
    1136999  λdest_lbl: label.
    1137   λdef: rtl_internal_function.
    1138   match fresh_regs_strong def (|addr|) with
     1000  λdef: rtl_internal_function globals.
     1001  match fresh_regs_strong rtl_params0 globals def (|addr|) with
    11391002  [ dp def_tmp_addr tmp_addr_prf ⇒
    11401003    let def ≝ \fst def_tmp_addr in
    11411004    let tmp_addr ≝ \snd def_tmp_addr in
    1142     let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
    1143     let 〈def, tmpr〉 ≝ fresh_reg def in
     1005    let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr tmp_addr ? in
     1006    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    11441007    let f ≝ λtranslate_off. λsrcr.
    11451008      let 〈translates, off〉 ≝ translate_off in
    11461009      let translates ≝ translates @ [
    1147         adds_graph [
    1148           rtl_st_int tmpr off start_lbl
     1010        adds_graph rtl_params1 globals [
     1011          sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
    11491012        ];
    1150         translate_op2 Oaddp tmp_addr ? addr [tmpr] ? ?;
    1151         adds_graph [
    1152           rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
     1013        translate_op2 globals Oaddp tmp_addr ? addr [tmpr] ? ?;
     1014        adds_graph rtl_params1 globals [
     1015          sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr)
    11531016        ]
    11541017      ]
    11551018      in
    1156         let 〈carry, result〉 ≝ half_add ? off int_size in
     1019        let 〈carry, result〉 ≝ half_add off int_size in
    11571020          〈translates, result〉
    11581021    in
    1159     let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], zero ?〉 srcrs in
    1160       add_translates translates start_lbl dest_lbl def
     1022    let 〈translates, ignore〉 ≝ foldl f 〈[ ], zero ?〉 srcrs in
     1023      add_translates rtl_params1 globals translates start_lbl dest_lbl def
    11611024  ].
    11621025  [1: normalize //
     
    11701033
    11711034definition translate_stmt ≝
    1172   λlenv.
     1035  λglobals: list ident.
     1036  λlenv: local_env.
    11731037  λlbl: label.
    11741038  λstmt.
    1175   λdef: rtl_internal_function.
     1039  λdef: rtl_internal_function globals.
    11761040  match stmt with
    1177   [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
    1178   | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
     1041  [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
     1042  | St_cost cost_lbl lbl' ⇒ add_graph lbl (sequential rtl_params_ globals (COST_LABEL … cost_lbl lbl')) def
    11791043  | St_const destr cst lbl' ⇒
    11801044    translate_cst cst (find_local_env destr lenv) lbl lbl' def
    11811045  | St_op1 op1 destr srcr lbl' ⇒
    1182     translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) ? lbl lbl' def
     1046    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) lbl lbl' def
    11831047  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
    1184     translate_op2 op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
     1048    translate_op2 op2 (find_local_env destr lenv) (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
    11851049  | St_load ignore addr destr lbl' ⇒
    1186     translate_load (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
     1050    translate_load (find_local_env addr lenv) (find_local_env destr lenv) lbl lbl' def
    11871051  | St_store ignore addr srcr lbl' ⇒
    1188     translate_store (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
     1052    translate_store (find_local_env addr lenv) (find_local_env srcr lenv) lbl lbl' def
    11891053  | St_call_id f args retr lbl' ⇒
    11901054    match retr with
    11911055    [ Some retr ⇒
    1192       add_graph lbl (rtl_st_call_id f (rtl_args args lenv) (find_local_env retr lenv) lbl') def
    1193     | None ⇒ add_graph lbl (rtl_st_call_id f (rtl_args args lenv) [ ] lbl') def
     1056      add_graph rtl_params1 globals lbl (sequential … (CALL_ID … f (rtl_args args lenv) (find_local_env retr lenv) lbl')) def
     1057    | None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID … f (rtl_args args lenv) [ ] lbl')) def
    11941058    ]
    11951059  | St_call_ptr f args retr lbl' ⇒
     
    11971061    [ None ⇒
    11981062      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    1199         add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) [ ] lbl') def
     1063        add_graph lbl rtl_params1 globals (sequential … (extension … (rtl_st_ext_call_ptr … f1 f2 (rtl_args args lenv) [ ] lbl'))) def
    12001064    | Some retr ⇒
    12011065      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    1202         add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv) lbl') def
     1066        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv) lbl'))) def
    12031067    ]
    12041068  | St_tailcall_id f args ⇒
    1205     add_graph lbl (rtl_st_tailcall_id f (rtl_args args lenv)) def
     1069    add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params_ globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) lbl) def
    12061070  | St_tailcall_ptr f args ⇒
    12071071    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    1208       add_graph lbl (rtl_st_tailcall_ptr f1 f2 (rtl_args args lenv)) def
     1072      add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params1 globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) lbl) def
    12091073  | St_cond r lbl_true lbl_false ⇒
    1210     translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
     1074    translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def
    12111075  | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
    1212   | St_return ⇒ add_graph lbl rtl_st_return def
     1076  | St_return ⇒ add_graph rtl_params1 globals lbl (RETURN …) def
    12131077  ].
    12141078  [10: cases not_implemented (* jtable case *)
     
    12221086   skip instructions at these nodes. *)
    12231087definition translate_internal ≝
    1224   λdef.
     1088  λglobals,def.
    12251089  let runiverse ≝ f_reggen def in
    1226   let lenv ≝ initialize_local_env runiverse
     1090  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
    12271091    (f_params def @ f_locals def) (f_result def) in
    1228   let params ≝ map_list_local_env lenv (map ? ? \fst (f_params def)) in
    1229   let locals ≝ map_list_local_env lenv (map ? ? \fst (f_locals def)) in
     1092  let params ≝ map_list_local_env lenv (map \fst (f_params def)) in
     1093  let locals ≝ map_list_local_env lenv (map \fst (f_locals def)) in
    12301094  let result ≝
    12311095    match (f_result def) with
     
    12441108  let entry' ≝ f_entry def in
    12451109  let exit' ≝ f_exit def in
    1246   let graph' ≝ add ? ? (empty_map ? ?) entry' (rtl_st_skip entry') in
    1247   let graph' ≝ add ? ? graph' exit' (rtl_st_skip exit') in
     1110  let graph' ≝ add … (empty_map ? ?) entry' (GOTO … entry') in
     1111  let graph' ≝ add … graph' exit' (GOTO … exit') in
    12481112  let res ≝
    1249     mk_rtl_internal_function luniverse' runiverse' result' params'
    1250                          locals' stack_size' graph' ? ? in
    1251     foldi ? ? ? (translate_stmt lenv) (f_graph def) res.
    1252   [1: %
    1253       [1: @entry'
    1254       |2: normalize nodelta;
    1255           @graph_add_lookup
    1256           @graph_add
    1257       ]
    1258   |2: %
    1259       [1: @exit'
    1260       |2: normalize nodelta;
    1261           @graph_add
    1262       ]
    1263   ]
    1264 qed.
    1265 
    1266 definition translate_fun_def ≝
    1267   λfdef: fundef internal_function.
    1268   match fdef with
    1269   [ Internal f ⇒ Internal ? (translate_internal f)
    1270   | External e ⇒ External ? e
    1271   ].
    1272 
    1273 (* XXX: change, we need to propagate the region information, not ignore it *)
    1274 definition init_data_to_nat ≝
    1275   λi: init_data.
    1276   match i with
    1277   [ Init_int8 i8 ⇒ 8
    1278   | Init_int16 i16 ⇒ 16
    1279   | Init_int32 i32 ⇒ 32
    1280   | Init_float32 f32 ⇒ 32
    1281   | Init_float64 f64 ⇒ 64
    1282   | Init_space s ⇒ s
    1283   | Init_null r ⇒ 0
    1284   | Init_addrof r i o ⇒ 8 (* XXX: not at all sure about this one *)
    1285   ].
    1286 
    1287 definition translate ≝
    1288   λp: program (fundef internal_function) unit.
    1289   let f_funct ≝ λid_fun_def.
    1290     let 〈id, fun_def〉 ≝ id_fun_def in
    1291       〈id, translate_fun_def fun_def〉
    1292   in
    1293   let vars' ≝ map ? ? (λx.
    1294     let 〈id_init_ignore, ignore〉 ≝ x in
    1295     let 〈id_init, ignore〉 ≝ id_init_ignore in
    1296     let 〈id, init〉 ≝ id_init in
    1297     let init_total ≝ foldr ? ? plus 0 (map ? ? init_data_to_nat init) in
    1298       〈id, init_total〉) (prog_vars ? ? p)
    1299   in
    1300   let functs' ≝ map ? ? f_funct (prog_funct ? ? p) in
    1301   let main' ≝ prog_main ? ? p in
    1302     mk_rtl_program vars' functs' (Some ? main').
     1113    mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
     1114     locals' stack_size' graph' ? ? in
     1115    foldi … (translate_stmt … lenv) (f_graph def) res.
     1116[ % [@entry' | @graph_add_lookup @graph_add]
     1117| % [@exit'  | @graph_add]]
     1118qed.
     1119
     1120(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
     1121  because of CompCert heritage *)
     1122definition rtlabs_to_rtl : RTLabs_program → rtl_program ≝
     1123 λp. transform_program ??? p (transf_fundef … (translate_internal (prog_var_names …))).
  • Deliverables/D3.3/id-lookup-branch/RTLabs/RTLabsMatitaPrinter.ml

    r1197 r1311  
    312312
    313313let print_program p =
    314   Printf.sprintf "include \"RTLabs/import.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n\n%s\n\ndefinition prog : res RTLabs_program :=\n%s\nOK ? (mk_program ??\n(%s)\n%s\n%s\n).\n"
     314  Printf.sprintf "include \"RTLabs/import.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n\n%s\n\ndefinition prog : res RTLabs_program :=\n%s\nOK ? (mk_program ??\n%s\n(%s)\n%s\n).\n"
    315315    (define_var_ids p.RTLabs.vars)
    316316    (print_fun_decls 2 p.RTLabs.functs)
    317317    (print_fun 2 p.RTLabs.functs)
     318    (print_globals 2 p.RTLabs.vars)
    318319    (print_fun' 2 p.RTLabs.functs)
    319320    (print_main 2 p.RTLabs.main)
    320     (print_globals 2 p.RTLabs.vars)
  • Deliverables/D3.3/id-lookup-branch/RTLabs/semantics.ma

    r1153 r1311  
    204204].
    205205
    206 definition RTLabs_exec : execstep io_out io_in ≝
    207   mk_execstep … ? is_final mem_of_state eval_statement.
    208 
    209 definition make_initial_state : RTLabs_program → res (genv × state) ≝
     206definition RTLabs_exec : trans_system io_out io_in ≝
     207  mk_trans_system … ? (λ_.is_final) eval_statement.
     208
     209definition make_global : RTLabs_program → genv ≝
     210λp. globalenv Genv ?? (λx.[Init_space x]) p.
     211
     212definition make_initial_state : RTLabs_program → res state ≝
    210213λp.
    211   do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     214  let ge ≝ make_global p in
    212215  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
    213216  let main ≝ prog_main ?? p in
    214217  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    215218  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    216   OK ? 〈ge,Callstate f (nil ?) (None ?) (nil ?) m〉.
     219  OK ? (Callstate f (nil ?) (None ?) (nil ?) m).
    217220
    218221definition RTLabs_fullexec : fullexec io_out io_in ≝
    219   mk_fullexec … RTLabs_exec ? make_initial_state.
    220 
     222  mk_fullexec … RTLabs_exec make_global make_initial_state.
     223
  • Deliverables/D3.3/id-lookup-branch/RTLabs/syntax.ma

    r1153 r1311  
    7373   allocate. *)
    7474
    75 definition RTLabs_program ≝ program (fundef internal_function) nat.
    76 
     75definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
  • Deliverables/D3.3/id-lookup-branch/RTLabs/test/search.RTLabs.ma

    r1197 r1311  
    428428
    429429OK ? (mk_program ??
     430  (*globals:*)
     431  []
    430432(  (pair ?? id_main f_main)::
    431433  (pair ?? id_search f_search)::
     
    434436(nil ?))
    435437  id_main
    436   (*globals:*)
    437   []
    438438).
    439 
    440    example exec: finishes_with (repr I32 3) ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 1000 [ ]; OK ? r).
    441    normalize  (* you can examine the result here *)
    442    @refl qed.
Note: See TracChangeset for help on using the changeset viewer.