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:
1 deleted
5 edited

Legend:

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

  • Deliverables/D3.3/id-lookup-branch/RTL/RTL.ma

    r1153 r1311  
    1 include "basics/list.ma".
    2 include "common/Registers.ma".
    3 include "common/AST.ma".
    4 include "common/Graphs.ma".
    5 include "common/CostLabel.ma".
     1include "joint/Joint.ma".
    62
    7 definition registers ≝ list register.
     3(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
     4  are not sequential. Thus there is a dummy label at the moment in the code.
     5  To be fixed once we understand exactly what to do with tail calls. *)
     6inductive rtl_statement_extension: Type[0] ≝
     7  | rtl_st_ext_address: register → register → rtl_statement_extension
     8  | rtl_st_ext_call_ptr: register → register → list register → list register → rtl_statement_extension
     9  | rtl_st_ext_tailcall_id: ident → list register → rtl_statement_extension
     10  | rtl_st_ext_tailcall_ptr: register → register → list register → rtl_statement_extension.
    811
    9 inductive rtl_statement: Type[0] ≝
    10   | rtl_st_skip: label → rtl_statement
    11   | rtl_st_cost: costlabel → label → rtl_statement
    12                 (* ldest, hdest, symbol, next *)
    13   | rtl_st_addr: register → register → ident → label → rtl_statement
    14                 (* ldest, hdest, next *)
    15   | rtl_st_stack_addr: register → register → label → rtl_statement
    16   | rtl_st_int: register → Byte → label → rtl_statement
    17                 (* dest, src, next *)
    18   | rtl_st_move: register → register → label → rtl_statement
    19   | rtl_st_clear_carry: label → rtl_statement
    20                 (* op, acc dest, bacc dest, acc src, bacc src, next *)
    21   | rtl_st_opaccs: OpAccs → register → register → register → register → label → rtl_statement
    22                 (* op, dest, src, next *)
    23   | rtl_st_op1: Op1 → register → register → label → rtl_statement
    24                 (* op, dest, src1, src2, next *)
    25   | rtl_st_op2: Op2 → register → register → register → label → rtl_statement
    26   | rtl_st_load: register → register → register → label → rtl_statement
    27   | rtl_st_store: register → register → register → label → rtl_statement
    28   | rtl_st_call_id: ident → registers → registers → label → rtl_statement
    29   | rtl_st_call_ptr: register → register → registers → registers → label → rtl_statement
    30   | rtl_st_tailcall_id: ident → registers → rtl_statement
    31   | rtl_st_tailcall_ptr: register → register → registers → rtl_statement
    32   | rtl_st_cond: register → label → label → rtl_statement
    33   | rtl_st_set_carry: label → rtl_statement
    34   | rtl_st_return: rtl_statement.
    35  
    36 definition rtl_statement_graph ≝ graph rtl_statement.
     12definition rtl_params__: params__ ≝
     13 mk_params__ register register register register (register × register) register
     14  (list register) (list register) rtl_statement_extension.
     15definition rtl_params_: params_ ≝ graph_params_ rtl_params__.
     16definition rtl_params0: params0 ≝ mk_params0 rtl_params__ (list register) (list register).
     17definition rtl_params1: params1 ≝ rtl_ertl_params1 rtl_params0.
     18definition rtl_params: ∀globals. params globals ≝ rtl_ertl_params rtl_params0.
    3719
    38 record rtl_internal_function: Type[0] ≝
    39 {
    40   rtl_if_luniverse: universe LabelTag;
    41   rtl_if_runiverse: universe RegisterTag;
    42 (*  rtl_if_sig: signature;  -- dropped in front end *)
    43   rtl_if_result   : registers;
    44   rtl_if_params   : registers;
    45   rtl_if_locals   : registers;
    46   rtl_if_stacksize: nat;
    47   rtl_if_graph    : rtl_statement_graph;
    48   rtl_if_entry    : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?;
    49   rtl_if_exit     : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?
    50 }.
     20definition rtl_statement ≝ joint_statement rtl_params_.
    5121
    52 definition rtl_function_definition ≝ fundef rtl_internal_function.
    53  
    54 record rtl_program: Type[0] ≝
    55 {
    56   rtl_pr_vars: list (ident × nat);
    57   rtl_pr_functs: list (ident × rtl_function_definition);
    58   rtl_pr_main: option ident
    59 }.
     22definition rtl_internal_function ≝
     23  λglobals. joint_internal_function … (rtl_params globals).
     24
     25definition rtl_program ≝ joint_program rtl_params.
     26
     27(************ Same without tail calls ****************)
     28
     29(*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
     30  are not sequential. Thus there is a dummy label at the moment in the code.
     31  To be fixed once we understand exactly what to do with tail calls. *)
     32inductive rtlntc_statement_extension: Type[0] ≝
     33  | rtlntc_st_ext_address: register → register → rtlntc_statement_extension
     34  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
     35
     36definition rtlntc_params__: params__ ≝
     37 mk_params__ register register register register (register × register) register
     38  (list register) (list register) rtlntc_statement_extension.
     39definition rtlntc_params_: params_ ≝ graph_params_ rtlntc_params__.
     40definition rtlntc_params0: params0 ≝ mk_params0 rtlntc_params__ (list register) (list register).
     41definition rtlntc_params1: params1 ≝ rtl_ertl_params1 rtlntc_params0.
     42definition rtlntc_params: ∀globals. params globals ≝ rtl_ertl_params rtlntc_params0.
     43
     44definition rtlntc_statement ≝ joint_statement rtlntc_params_.
     45
     46definition rtlntc_internal_function ≝
     47  λglobals. joint_internal_function … (rtlntc_params globals).
     48
     49definition rtlntc_program ≝ joint_program rtlntc_params.
  • Deliverables/D3.3/id-lookup-branch/RTL/RTLTailcall.ma

    r1081 r1311  
    22
    33definition simplify_stmt ≝
     4  λglobals.
    45  λexit: label.
    56  λlbl: label.
    6   λstmt.
    7   λgraph: rtl_statement_graph.
     7  λstmt: rtl_statement globals.
     8  λgraph: codeT … (rtlntc_params globals).
    89  match stmt with
    9   [ rtl_st_tailcall_id f args ⇒
    10       add ? ? graph lbl (rtl_st_call_id f args [ ] exit)
    11   | rtl_st_tailcall_ptr f1 f2 args ⇒
    12       add ? ? graph lbl (rtl_st_call_ptr f1 f2 args [ ] exit)
    13   | _ ⇒ graph
    14   ].
     10  [ sequential seq DUMMY ⇒
     11     match seq with
     12      [ extension ext ⇒
     13         match ext with
     14          [ rtl_st_ext_tailcall_id f args ⇒
     15              add ? ? graph lbl (sequential … (CALL_ID … f args [ ]) exit)
     16          | rtl_st_ext_tailcall_ptr f1 f2 args ⇒
     17              add ? ? graph lbl (sequential … (extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)
     18          | _ ⇒ graph ]
     19      | _ ⇒ graph ]
     20  | _ ⇒ graph ].
    1521
    1622definition simplify_graph ≝
     23  λglobals.
    1724  λexit: label.
    18   λgraph: rtl_statement_graph.
    19     foldi ? ? ? (simplify_stmt exit) graph graph.
     25  λgraph: codeT … (rtl_params globals).
     26    foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
    2027
    2128axiom simplify_graph_preserves_labels:
    22   ∀g: rtl_statement_graph.
     29  ∀globals.
     30  ∀g: codeT … (rtl_params globals).
    2331  ∀l: label.
    2432  ∀exit: label.
    25     lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph exit g) l ≠ None ?.
     33    lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph globals exit g) l ≠ None ?.
    2634   
    27 definition simplify_internal ≝
    28   λdef.
    29     let rtl_if_luniverse' ≝ rtl_if_luniverse def in
    30     let rtl_if_runiverse' ≝ rtl_if_runiverse def in
    31     let rtl_if_result' ≝ rtl_if_result def in
    32     let rtl_if_params' ≝ rtl_if_params def in
    33     let rtl_if_locals' ≝ rtl_if_locals def in
    34     let rtl_if_stacksize' ≝ rtl_if_stacksize def in
    35     let rtl_if_graph' ≝ simplify_graph (rtl_if_exit def) (rtl_if_graph def) in
    36     let rtl_if_entry' ≝ rtl_if_entry def in
    37     let rtl_if_exit' ≝ rtl_if_exit def in
    38       mk_rtl_internal_function
    39         rtl_if_luniverse' rtl_if_runiverse'
    40         rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize'
    41         rtl_if_graph' ? ?.
    42   normalize nodelta
    43   [1: cases rtl_if_entry'
    44       #ENTRY #ENTRY_PRF
    45       %
    46       [1: @ENTRY
    47       |2: @simplify_graph_preserves_labels
    48           @ENTRY_PRF
    49       ]
    50   |2: cases rtl_if_exit'
    51       #EXIT #EXIT_PRF
    52       %
    53       [1: @EXIT
    54       |2: @simplify_graph_preserves_labels
    55           @EXIT_PRF
    56       ]
    57   ]
     35definition simplify_internal :
     36 ∀globals.
     37  joint_internal_function … (rtl_params globals) →
     38   joint_internal_function … (rtlntc_params globals)
     39
     40  λglobals,def.
     41    let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in
     42      mk_joint_internal_function …
     43       (joint_if_luniverse … def) (joint_if_runiverse … def)
     44       (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def)
     45       (joint_if_stacksize … def) graph
     46       (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)).
     47 [ cases (joint_if_entry … def) | cases (joint_if_exit … def) ]
     48 #l #IH @simplify_graph_preserves_labels @IH
    5849qed.
    5950
    60 definition simplify_funct ≝
    61   λid_def: ident × ?.
    62   let 〈id, def〉 ≝ id_def in
    63   let def' ≝
    64     match def with
    65     [ Internal def ⇒ Internal ? (simplify_internal def)
    66     | External def ⇒ External ? def
    67     ]
    68   in
    69     〈id, def'〉.
    70  
    71 definition tailcall_simplify ≝
    72   λp.
    73   let rtl_pr_vars' ≝ rtl_pr_vars p in
    74   let rtl_pr_functs' ≝ map ? ? simplify_funct (rtl_pr_functs p) in
    75   let rtl_pr_main' ≝ rtl_pr_main p in
    76     mk_rtl_program rtl_pr_vars' rtl_pr_functs' rtl_pr_main'.
     51definition tailcall_simplify : rtl_program → rtlntc_program ≝
     52 λp. transform_program … p (transf_fundef … (simplify_internal …)).
  • Deliverables/D3.3/id-lookup-branch/RTL/RTLtoERTL.ma

    r1153 r1311  
    1 include "RTL/RTL.ma".
    21include "RTL/RTLTailcall.ma".
    32include "utilities/RegisterSet.ma".
    43include "common/Identifiers.ma".
    54include "ERTL/ERTL.ma".
    6 
    7 definition change_exit_label ≝
    8   λl: label.
    9   λp: ertl_internal_function.
    10   λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?.
    11   let ertl_if_luniverse' ≝ ertl_if_luniverse p in
    12   let ertl_if_runiverse' ≝ ertl_if_runiverse p in
    13   let ertl_if_params' ≝ ertl_if_params p in
    14   let ertl_if_locals' ≝ ertl_if_locals p in
    15   let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    16   let ertl_if_graph' ≝ ertl_if_graph p in
    17   let ertl_if_entry' ≝ ertl_if_entry p in
    18   let ertl_if_exit' ≝ l in
    19     mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    20                               ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    21                               ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    22   @prf
    23 qed.
    24 
    25 definition change_entry_label ≝
    26   λl: label.
    27   λp: ertl_internal_function.
    28   λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?.
    29   let ertl_if_luniverse' ≝ ertl_if_luniverse p in
    30   let ertl_if_runiverse' ≝ ertl_if_runiverse p in
    31   let ertl_if_params' ≝ ertl_if_params p in
    32   let ertl_if_locals' ≝ ertl_if_locals p in
    33   let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    34   let ertl_if_graph' ≝ ertl_if_graph p in
    35   let ertl_if_entry' ≝ l in
    36   let ertl_if_exit' ≝ ertl_if_exit p in
    37     mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    38                               ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    39                               ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    40   @prf
    41 qed.
    42                              
    43 definition add_graph ≝
    44   λl: label.
    45   λstmt.
    46   λp.
    47   let ertl_if_luniverse' ≝ ertl_if_luniverse p in
    48   let ertl_if_runiverse' ≝ ertl_if_runiverse p in
    49   let ertl_if_params' ≝ ertl_if_params p in
    50   let ertl_if_locals' ≝ ertl_if_locals p in
    51   let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    52   let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in
    53   let ertl_if_entry' ≝ ertl_if_entry p in
    54   let ertl_if_exit' ≝ ertl_if_exit p in
    55     mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    56                               ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    57                               ertl_if_graph' ? ?.
    58   normalize nodelta;
    59   [1: generalize in match ertl_if_entry';
    60       #HYP
    61       cases HYP
    62       #LBL #LBL_PRF
    63       %
    64       [1: @LBL
    65       |2: @graph_add_lookup
    66           @LBL_PRF
    67       ]
    68   |2: generalize in match ertl_if_exit';
    69       #HYP
    70       cases HYP
    71       #LBL #LBL_PRF
    72       %
    73       [1: @LBL
    74       |2: @graph_add_lookup
    75           @LBL_PRF
    76       ]
    77   ]
    78 qed.
    79                              
    80 definition fresh_label ≝
    81   λdef.
    82     fresh LabelTag (ertl_if_luniverse def).
    83    
    84 definition change_label ≝
    85   λl.
    86   λe: ertl_statement.
    87   match e with
    88   [ ertl_st_skip _ ⇒ ertl_st_skip l
    89   | ertl_st_comment s _ ⇒ ertl_st_comment s l
    90   | ertl_st_cost c _ ⇒ ertl_st_cost c l
    91   | ertl_st_get_hdw r1 r2 _ ⇒ ertl_st_get_hdw r1 r2 l
    92   | ertl_st_set_hdw r1 r2 _ ⇒ ertl_st_set_hdw r1 r2 l
    93   | ertl_st_hdw_to_hdw r1 r2 _ ⇒ ertl_st_hdw_to_hdw r1 r2 l
    94   | ertl_st_new_frame _ ⇒ ertl_st_new_frame l
    95   | ertl_st_del_frame _ ⇒ ertl_st_del_frame l
    96   | ertl_st_frame_size r _ ⇒ ertl_st_frame_size r l
    97   | ertl_st_pop r _ ⇒ ertl_st_pop r l
    98   | ertl_st_push r _ ⇒ ertl_st_push r l
    99   | ertl_st_addr r1 r2 x _ ⇒ ertl_st_addr r1 r2 x l
    100   | ertl_st_int r i _ ⇒ ertl_st_int r i l
    101   | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
    102   | ertl_st_opaccs opaccs d1 d2 s1 s2 _ ⇒ ertl_st_opaccs opaccs d1 s1 s1 s2 l
    103   | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
    104   | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
    105   | ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l
    106   | ertl_st_set_carry _ ⇒ ertl_st_set_carry l
    107   | ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l
    108   | ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l
    109   | ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l
    110   | ertl_st_cond a i1 i2 ⇒ ertl_st_cond a i1 i2
    111   | ertl_st_return ⇒ ertl_st_return
    112   ].
    113  
    114 let rec adds_graph
    115   (stmt_list: list ertl_statement) (start_lbl: label)
    116   (dest_lbl: label) (def: ertl_internal_function)
    117     on stmt_list ≝
    118   match stmt_list with
    119   [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
    120   | cons stmt stmt_list ⇒
    121     match stmt_list with
    122     [ nil ⇒ add_graph start_lbl (change_label dest_lbl stmt) def
    123     | _ ⇒
    124       let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
    125       let stmt ≝ change_label tmp_lbl stmt in
    126       let def ≝ add_graph start_lbl stmt def in
    127         adds_graph stmt_list tmp_lbl dest_lbl def
    128     ]
    129   ].
    130 
    131 let rec add_translates
    132   (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
    133   (def: ertl_internal_function)
    134     on translate_list ≝
    135   match translate_list with
    136   [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
    137   | cons trans translate_list ⇒
    138     match translate_list with
    139     [ nil ⇒ trans start_lbl dest_lbl def
    140     | _ ⇒
    141       let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
    142       let def ≝ trans start_lbl tmp_lbl def in
    143         add_translates translate_list tmp_lbl dest_lbl def
    144     ]
    145   ].
    146 
    147 axiom register_fresh: universe RegisterTag → register.
    148 
    149 definition fresh_reg: ertl_internal_function → ertl_internal_function × register ≝
    150   λdef.
    151     let r ≝ register_fresh (ertl_if_runiverse def) in
    152     let locals ≝ r :: ertl_if_locals def in
    153     let ertl_if_luniverse' ≝ ertl_if_luniverse def in
    154     let ertl_if_runiverse' ≝ ertl_if_runiverse def in
    155     let ertl_if_params' ≝ ertl_if_params def in
    156     let ertl_if_locals' ≝ locals in
    157     let ertl_if_stacksize' ≝ ertl_if_stacksize def in
    158     let ertl_if_graph' ≝ ertl_if_graph def in
    159     let ertl_if_entry' ≝ ertl_if_entry def in
    160     let ertl_if_exit' ≝ ertl_if_exit def in
    161       〈mk_ertl_internal_function
    162         ertl_if_luniverse' ertl_if_runiverse' ertl_if_params'
    163         ertl_if_locals' ertl_if_stacksize' ertl_if_graph'
    164         ertl_if_entry' ertl_if_exit', r〉.
    165 
    166 let rec fresh_regs
    167   (def: ertl_internal_function) (n: nat)
    168     on n ≝
    169   match n with
    170   [ O ⇒ 〈def, [ ]〉
    171   | S n' ⇒
    172     let 〈def', regs'〉 ≝ fresh_regs def n' in
    173     let 〈def', reg〉 ≝ fresh_reg def' in
    174       〈def', reg :: regs'〉
    175   ].
    176  
    177 axiom fresh_regs_length:
    178   ∀def: ertl_internal_function.
    179   ∀n: nat.
    180     |(\snd (fresh_regs def n))| = n.
    181 
    182 definition fresh_regs_strong: ? → ∀n: nat. Σregs: ertl_internal_function × (list register). |\snd regs| = n ≝
    183   λdef: ertl_internal_function.
    184   λn: nat.
    185     fresh_regs def n.
    186   @fresh_regs_length
    187 qed.
    188  
    189 definition save_hdws_internal ≝
    190   λdestr_srcr: register × Register.
    191   λstart_lbl: label.
     5include "joint/TranslateUtils.ma".
     6
     7definition save_hdws ≝
     8 λglobals,l.
     9  let save_hdws_internal ≝
     10   λdestr_srcr.λstart_lbl.
    19211    let 〈destr, srcr〉 ≝ destr_srcr in
    193       adds_graph [ ertl_st_get_hdw destr srcr start_lbl ] start_lbl.
    194  
    195 definition save_hdws ≝
    196   λl.
    197     map ? ? save_hdws_internal l.
    198    
    199 definition restore_hdws_internal ≝
    200   λdestr_srcr: Register × register.
    201   λstart_lbl: label.
    202     let 〈destr, srcr〉 ≝ destr_srcr in
    203     adds_graph [ ertl_st_set_hdw destr srcr start_lbl ] start_lbl.
    204    
    205 definition swap_components ≝
    206   λA, B: Type[0].
    207   λp: A × B.
    208   let 〈l, r〉 ≝ p in
    209   〈r, l〉.
    210    
     12     adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈pseudo destr,hardware srcr〉) ] start_lbl
     13  in
     14   map ? ? save_hdws_internal l.
     15
    21116definition restore_hdws ≝
    212   λl.
    213     map ? ? restore_hdws_internal (map ? ? (swap_components ? ?) l).
    214 
    215 definition get_params_hdw_internal ≝
    216   λstart_lbl: label.
    217     adds_graph [ ertl_st_skip start_lbl ] start_lbl.
     17  λglobals,l.
     18   let restore_hdws_internal ≝
     19    λsrcr_destr: register × Register.
     20    λstart_lbl: label.
     21     let 〈srcr, destr〉 ≝ srcr_destr in
     22     adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈hardware destr, pseudo srcr〉) ] start_lbl
     23   in
     24    map ? ? restore_hdws_internal l.
    21825
    21926definition get_params_hdw ≝
     27  λglobals.
    22028  λparams: list register.
    22129  match params with
    222   [ nil ⇒ [get_params_hdw_internal]
     30  [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … ] start_lbl]
    22331  | _ ⇒
    22432    let l ≝ zip_pottier ? ? params RegisterParams in
    225       save_hdws l
    226   ].
     33      save_hdws globals l ].
    22734
    22835definition get_param_stack ≝
     36  λglobals.
    22937  λoff: nat.
    23038  λdestr.
    23139  λstart_lbl, dest_lbl: label.
    23240  λdef.
    233   let 〈def, addr1〉 ≝ fresh_reg def in
    234   let 〈def, addr2〉 ≝ fresh_reg def in
    235   let 〈def, tmpr〉 ≝ fresh_reg def in
     41  let 〈def, addr1〉 ≝ fresh_reg def in
     42  let 〈def, addr2〉 ≝ fresh_reg def in
     43  let 〈def, tmpr〉 ≝ fresh_reg def in
    23644  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
    237   adds_graph [
    238     ertl_st_frame_size addr1 start_lbl;
    239     ertl_st_int tmpr int_offset start_lbl;
    240     ertl_st_op2 Sub addr1 addr1 tmpr start_lbl;
    241     ertl_st_get_hdw tmpr RegisterSPL start_lbl;
    242     ertl_st_op2 Add addr1 addr1 tmpr start_lbl;
    243     ertl_st_int addr2 (bitvector_of_nat 8 0) start_lbl;
    244     ertl_st_get_hdw tmpr RegisterSPH start_lbl;
    245     ertl_st_op2 Addc addr2 addr2 tmpr start_lbl;
    246     ertl_st_load destr addr1 addr2 start_lbl
     45  adds_graph ertl_params1 globals [
     46    sequential ertl_params_ … (extension … (ertl_st_ext_frame_size addr1));
     47    sequential ertl_params_ … (INT … tmpr int_offset);
     48    sequential ertl_params_ … (OP2 … Sub addr1 addr1 tmpr);
     49    sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
     50    sequential ertl_params_ … (OP2 … Add addr1 addr1 tmpr);
     51    sequential ertl_params_ … (INT … addr2 (bitvector_of_nat 8 0));
     52    sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
     53    sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr);
     54    sequential ertl_params_ … (LOAD … destr addr1 addr2)
    24755  ] start_lbl dest_lbl def.
    24856 
    24957definition get_params_stack ≝
    250   λparams.
     58  λglobals,params.
    25159  match params with
    252   [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl ]
    253   | _ ⇒
    254     let f ≝ λi. λr. get_param_stack i r in
    255       mapi ? ? f params
    256   ].
     60  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl ]
     61  | _ ⇒ mapi ? ? (get_param_stack globals) params ].
    25762
    25863definition get_params ≝
    259   λparams.
    260   let n ≝ min (length ? params) (length ? RegisterParams) in
    261   let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
    262   let hdw_params ≝ get_params_hdw hdw_params in
    263     hdw_params @ (get_params_stack stack_params).
    264  
     64  λglobals,params.
     65  let n ≝ min (length … params) (length … RegisterParams) in
     66  let 〈hdw_params, stack_params〉 ≝ list_split n params in
     67  let hdw_params ≝ get_params_hdw globals hdw_params in
     68    hdw_params @ (get_params_stack stack_params).
     69
    26570definition add_prologue ≝
     71  λglobals.
    26672  λparams: list register.
    26773  λsral.
     
    26975  λsregs.
    27076  λdef.
    271   let start_lbl ≝ ertl_if_entry def in
    272   let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
    273   match lookup ? ? (ertl_if_graph def) start_lbl
    274     return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ertl_internal_function with
    275   [ None ⇒ λnone_absrd. ?
     77  let start_lbl ≝ joint_if_entry … (ertl_params globals) def in
     78  let 〈tmp_lbl, def〉 ≝ fresh_label … def in
     79  match lookup … (joint_if_code … def) start_lbl
     80    return λx. x ≠ None ? → ertl_internal_function globals with
     81  [ None ⇒ λnone_absrd.
    27682  | Some last_stmt ⇒ λsome_prf.
    27783    let def ≝
    278       add_translates
    279          ((adds_graph [
    280                      ertl_st_new_frame start_lbl
     84      add_translates …
     85         ((adds_graph ertl_params1 … [
     86                     sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame)
    28187                   ]) ::
    282          (adds_graph [
    283                       ertl_st_pop sral start_lbl;
    284                       ertl_st_pop srah start_lbl
     88         (adds_graph ertl_params1 … [
     89                      sequential ertl_params_ … (POP … sral);
     90                      sequential ertl_params_ … (POP … srah)
    28591                   ]) ::
    286          (save_hdws sregs) @
    287          (get_params params))
     92         (save_hdws sregs) @
     93         (get_params params))
    28894        start_lbl tmp_lbl def
    28995    in
    290       add_graph tmp_lbl last_stmt def
     96      add_graph tmp_lbl last_stmt def
    29197  ] ?.
    292   cases not_implemented (* dep. types here *)
     98[ cases start_lbl #x #H cases daemon (* @H *) (*CSC: XXXX, no Russell *)
     99| cases (none_absrd) /2/ ]
    293100qed.
    294101
    295102definition save_return ≝
     103  λglobals.
    296104  λret_regs.
    297105  λstart_lbl: label.
    298106  λdest_lbl: label.
    299   λdef: ertl_internal_function.
    300   let 〈def, tmpr〉 ≝ fresh_reg def in
     107  λdef: ertl_internal_function globals.
     108  let 〈def, tmpr〉 ≝ fresh_reg def in
    301109  match reduce_strong ? ? RegisterSTS ret_regs with
    302110  [ dp crl crl_proof ⇒
     
    305113    let restl ≝ \snd (\fst crl) in
    306114    let restr ≝ \snd (\snd crl) in
    307     let init_tmpr ≝ ertl_st_int tmpr (zero ?) start_lbl in
    308     let f_save ≝ λst. λr. ertl_st_set_hdw st r start_lbl in
    309     let saves ≝ map2 ? ? ? f_save commonl commonr crl_proof in
    310     let f_default ≝ λst. ertl_st_set_hdw st tmpr start_lbl in
    311     let defaults ≝ map ? ? f_default restl in
    312       adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
     115    let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) in
     116    let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) in
     117    let saves ≝ map2 f_save commonl commonr crl_proof in
     118    let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) in
     119    let defaults ≝ map f_default restl in
     120      adds_graph ertl_params1 … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
    313121  ].
    314122
    315123definition assign_result ≝
    316   λstart_lbl: label.
     124  λglobals.λstart_lbl: label.
    317125  match reduce_strong ? ? RegisterRets RegisterSTS with
    318126  [ dp crl crl_proof ⇒
    319127    let commonl ≝ \fst (\fst crl) in
    320128    let commonr ≝ \fst (\snd crl) in
    321     let f ≝ λret. λst. ertl_st_hdw_to_hdw ret st start_lbl in
     129    let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) in
    322130    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
    323       adds_graph insts start_lbl
     131      adds_graph ertl_params1 … insts start_lbl
    324132  ].
    325133
    326134definition add_epilogue ≝
     135  λglobals.
    327136  λret_regs.
    328137  λsral.
     
    330139  λsregs.
    331140  λdef.
    332   let start_lbl ≝ ertl_if_exit def in
    333   let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
    334   match lookup ? ? (ertl_if_graph def) start_lbl
    335     return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ? with
    336   [ None ⇒ λnone_absd. ?
     141  let start_lbl ≝ joint_if_exit … (ertl_params globals) def in
     142  let 〈tmp_lbl, def〉 ≝ fresh_label … def in
     143  match lookup … (joint_if_code … def) start_lbl
     144    return λx. x ≠ None ? → ertl_internal_function globals with
     145  [ None ⇒ λnone_absrd. ⊥
    337146  | Some last_stmt ⇒ λsome_prf.
    338147    let def ≝
    339       add_translates (
    340         [save_return ret_regs] @
    341         restore_hdws sregs @
    342         [adds_graph [
    343           ertl_st_push srah start_lbl;
    344           ertl_st_push sral start_lbl
     148      add_translates ertl_params1 … (
     149        [save_return globals ret_regs] @
     150        restore_hdws sregs @
     151        [adds_graph ertl_params1 … [
     152          sequential ertl_params_ … (PUSH … srah);
     153          sequential ertl_params_ … (PUSH … sral)
    345154        ]] @
    346         [adds_graph [
    347           ertl_st_del_frame start_lbl
     155        [adds_graph ertl_params1 … [
     156          sequential ertl_params_ … (extension … ertl_st_ext_del_frame)
    348157        ]] @
    349         [assign_result]
     158        [assign_result globals]
    350159      ) start_lbl tmp_lbl def
    351160    in
    352     let def ≝ add_graph tmp_lbl last_stmt def in
    353       change_exit_label tmp_lbl def ?
     161    let def' ≝ add_graph … tmp_lbl last_stmt def in
     162      set_joint_if_exit … tmp_lbl def' ?
    354163  ] ?.
    355   cases not_implemented (* dep types here, bug in matita too! *)
     164[ cases start_lbl #x #H cases daemon (* @H *) (* CSC: XXXX *)
     165| cases (none_absrd) /2/
     166| cases daemon (* CSC: XXXXX *)
     167]
    356168qed.
    357169 
    358 definition allocate_regs_internal ≝
    359   λr: Register.
    360   λdef_sregs.
    361   let 〈def, sregs〉 ≝ def_sregs in
    362   let 〈def, r'〉 ≝ fresh_reg def in
    363     〈def, 〈r', r〉 :: sregs〉.
    364  
     170
    365171definition allocate_regs ≝
     172  λglobals.
    366173  λrs.
    367174  λsaved: rs_set rs.
    368175  λdef.
     176   let allocate_regs_internal ≝
     177    λr: Register.
     178    λdef_sregs.
     179    let 〈def, sregs〉 ≝ def_sregs in
     180    let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in
     181      〈def, 〈r', r〉 :: sregs〉
     182   in
    369183    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
    370184   
    371185definition add_pro_and_epilogue ≝
     186  λglobals.
    372187  λparams.
    373188  λret_regs.
    374189  λdef.
    375   match fresh_regs_strong def 2 with
     190  match fresh_regs_strong … globals def 2 with
    376191  [ dp def_sra def_sra_proof ⇒
    377192    let def ≝ \fst def_sra in
     
    379194    let sral ≝ nth_safe ? 0 sra ? in
    380195    let srah ≝ nth_safe ? 1 sra ? in
    381     let 〈def, sregs〉 ≝ allocate_regs register_list_set RegisterCalleeSaved def in
    382     let def ≝ add_prologue params sral srah sregs def in
    383     let def ≝ add_epilogue ret_regs sral srah sregs def in
     196    let 〈def, sregs〉 ≝ allocate_regs register_list_set RegisterCalleeSaved def in
     197    let def ≝ add_prologue params sral srah sregs def in
     198    let def ≝ add_epilogue ret_regs sral srah sregs def in
    384199      def
    385200  ].
    386   [1: >def_sra_proof //
    387   |2: >def_sra_proof //
    388   ]
     201>def_sra_proof //
    389202qed.
    390203
    391204definition set_params_hdw ≝
    392   λparams.
     205  λglobals,params.
    393206  match params with
    394   [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
     207  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl]
    395208  | _ ⇒
    396209    let l ≝ zip_pottier ? ? params RegisterParams in
    397       restore_hdws l
     210      restore_hdws globals l
    398211  ].
    399212
    400213definition set_param_stack ≝
     214  λglobals.
    401215  λoff.
    402216  λsrcr.
    403217  λstart_lbl: label.
    404218  λdest_lbl: label.
    405   λdef: ertl_internal_function.
    406   let 〈def, addr1〉 ≝ fresh_reg def in
    407   let 〈def, addr2〉 ≝ fresh_reg def in
    408   let 〈def, tmpr〉 ≝ fresh_reg def in
     219  λdef: ertl_internal_function globals.
     220  let 〈def, addr1〉 ≝ fresh_reg def in
     221  let 〈def, addr2〉 ≝ fresh_reg def in
     222  let 〈def, tmpr〉 ≝ fresh_reg def in
    409223  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
    410     adds_graph [
    411       ertl_st_int addr1 int_off start_lbl;
    412       ertl_st_get_hdw tmpr RegisterSPL start_lbl;
    413       ertl_st_clear_carry start_lbl;
    414       ertl_st_op2 Sub addr1 tmpr addr1 start_lbl;
    415       ertl_st_get_hdw tmpr RegisterSPH start_lbl;
    416       ertl_st_int addr2 (zero ?) start_lbl;
    417       ertl_st_op2 Sub addr2 tmpr addr2 start_lbl;
    418       ertl_st_store addr1 addr2 srcr start_lbl
     224    adds_graph ertl_params1 … [
     225      sequential ertl_params_ … (INT … addr1 int_off);
     226      sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
     227      sequential ertl_params_ … (CLEAR_CARRY …);
     228      sequential ertl_params_ … (OP2 … Sub addr1 tmpr addr1);
     229      sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
     230      sequential ertl_params_ … (INT … addr2 (zero ?));
     231      sequential ertl_params_ … (OP2 … Sub addr2 tmpr addr2);
     232      sequential ertl_params_ … (STORE … addr1 addr2 srcr)
    419233    ] start_lbl dest_lbl def.   
    420234
    421235definition set_params_stack ≝
    422   λparams.
     236  λglobals,params.
    423237  match params with
    424   [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
     238  [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO …] start_lbl]
    425239  | _ ⇒
    426     let f ≝ λi. λr. set_param_stack (bitvector_of_nat ? i) r in
    427       mapi ? ? f params
    428   ].
    429 
    430 axiom min_fst:
    431   ∀m, n: nat.
    432     min m n ≤ m.
     240    let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in
     241      mapi ? ? f params].
    433242
    434243definition set_params ≝
    435   λparams.
     244  λglobals,params.
    436245  let n ≝ min (|params|) (|RegisterParams|) in
    437246  let hdw_stack_params ≝ split ? params n ? in
    438247  let hdw_params ≝ \fst hdw_stack_params in
    439248  let stack_params ≝ \snd hdw_stack_params in
    440     set_params_hdw hdw_params @ set_params_stack stack_params.
    441   @min_fst
     249    set_params_hdw globals hdw_params @ set_params_stack globals stack_params.
     250/2/
    442251qed.
    443252
    444253definition fetch_result ≝
     254  λglobals.
    445255  λret_regs.
    446256  λstart_lbl: label.
     
    449259    let commonl ≝ \fst (\fst crl) in
    450260    let commonr ≝ \fst (\snd crl) in
    451     let f_save ≝ λst. λret. ertl_st_hdw_to_hdw st ret start_lbl in
     261    let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) in
    452262    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
    453263    match reduce_strong ? ? ret_regs RegisterSTS with
     
    455265      let commonl ≝ \fst (\fst crl) in
    456266      let commonr ≝ \fst (\snd crl) in
    457       let f_restore ≝ λr. λst. ertl_st_get_hdw r st start_lbl in
     267      let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) in
    458268      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
    459         adds_graph (saves @ restores) start_lbl
    460     ]
    461   ].
    462   [ normalize nodelta; @second_crl_proof
    463   | @first_crl_proof
    464   ]
     269        adds_graph ertl_params1 … (saves @ restores) start_lbl]].
     270[@second_crl_proof | @first_crl_proof]
    465271qed.
    466272
    467273definition translate_call_id ≝
    468   λf.
     274  λglobals,f.
    469275  λargs.
    470276  λret_regs.
     
    473279  λdef.
    474280  let nb_args ≝ |args| in
    475     add_translates (
    476       set_params args @ [
    477       adds_graph [ ertl_st_call_id f nb_args start_lbl ];
    478       fetch_result ret_regs
     281    add_translates ertl_params1 globals (
     282      set_params args @ [
     283      adds_graph ertl_params1 … [ sequential ertl_params_ … (CALL_ID … f nb_args it) ];
     284      fetch_result ret_regs
    479285      ]
    480286    ) start_lbl dest_lbl def.
    481287
    482 definition translate_stmt ≝
     288definition translate_stmt :
     289 ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals
     290 ≝
     291  λglobals.
    483292  λlbl.
    484293  λstmt.
    485294  λdef.
    486295  match stmt with
    487   [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def
    488   | rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def
    489   | rtl_st_addr r1 r2 x lbl' ⇒ add_graph lbl (ertl_st_addr r1 r2 x lbl') def
    490   | rtl_st_stack_addr r1 r2 lbl' ⇒
    491     adds_graph [
    492       ertl_st_get_hdw r1 RegisterSPL lbl;
    493       ertl_st_get_hdw r2 RegisterSPH lbl
    494     ] lbl lbl' def
    495   | rtl_st_int r i lbl' ⇒  add_graph lbl (ertl_st_int r i lbl') def
    496   | rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def
    497   | rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒
    498       add_graph lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def
    499 (* XXX: change from o'caml
    500     adds_graph [
    501       ertl_st_opaccs_a op destr1 srcr1 srcr2 lbl;
    502       ertl_st_opaccs_b op destr2 srcr1 srcr2 lbl
    503       ] lbl lbl' def
    504 *)
    505   | rtl_st_op1 op1 destr srcr lbl' ⇒
    506     add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def
    507   | rtl_st_op2 op2 destr srcr1 srcr2 lbl' ⇒
    508     add_graph lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def
    509   | rtl_st_clear_carry lbl' ⇒
    510     add_graph lbl (ertl_st_clear_carry lbl') def
    511   | rtl_st_set_carry lbl' ⇒
    512     add_graph lbl (ertl_st_set_carry lbl') def
    513   | rtl_st_load destr addr1 addr2 lbl' ⇒
    514     add_graph lbl (ertl_st_load destr addr1 addr2 lbl') def
    515   | rtl_st_store addr1 addr2 srcr lbl' ⇒
    516     add_graph lbl (ertl_st_store addr1 addr2 srcr lbl') def
    517   | rtl_st_call_id f args ret_regs lbl' ⇒
    518     translate_call_id f args ret_regs lbl lbl' def
    519   | rtl_st_cond srcr lbl_true lbl_false ⇒
    520     add_graph lbl (ertl_st_cond srcr lbl_true lbl_false) def
    521   | rtl_st_return ⇒
    522     add_graph lbl ertl_st_return def
    523   | _ ⇒ ? (* assert false: not implemented or should not happen *)
    524   ].
    525   cases not_implemented
    526 qed.   
     296  [ GOTO lbl' ⇒ add_graph … lbl (GOTO … lbl') def
     297  | RETURN ⇒ add_graph … lbl (RETURN …) def
     298  | sequential seq lbl' ⇒
     299     match seq with
     300      [ PUSH _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
     301      | POP _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
     302      | CALL_ID f args ret_regs ⇒
     303         translate_call_id … f args ret_regs lbl lbl' def
     304      | MOVE rs ⇒
     305         let 〈r1,r2〉 ≝ rs in
     306         let rs ≝ 〈pseudo r1, pseudo r2〉 in
     307          add_graph ertl_params1 ? lbl (sequential … (MOVE … rs) lbl') def
     308      | extension ext ⇒
     309         match ext with
     310          [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
     311          | rtlntc_st_ext_address r1 r2 ⇒
     312             adds_graph ertl_params1 … [
     313              sequential ertl_params_ … (MOVE … 〈pseudo r1, hardware RegisterSPL〉);
     314              sequential ertl_params_ … (MOVE … 〈pseudo r2, hardware RegisterSPH〉)
     315             ] lbl lbl' def]
     316      (*CSC: everything is just copied to re-type it from now on;
     317        the problem is call_id that takes different parameters, but that is pattern-matched
     318        above. It could be made nicer at the cost of making all the rest of the code uglier *)
     319      | COST_LABEL cost_lbl ⇒ add_graph ertl_params1 … lbl (sequential … (COST_LABEL … cost_lbl) lbl') def
     320      | ADDRESS x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (sequential … (ADDRESS … x prf r1 r2) lbl') def
     321      | INT r i ⇒  add_graph ertl_params1 … lbl (sequential … (INT … r i) lbl') def
     322      | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
     323          add_graph ertl_params1 … lbl (sequential … (OPACCS … op destr1 destr2 srcr1 srcr2) lbl') def
     324      | OP1 op1 destr srcr ⇒
     325        add_graph ertl_params1 … lbl (sequential … (OP1 … op1 destr srcr) lbl') def
     326      | OP2 op2 destr srcr1 srcr2 ⇒
     327        add_graph ertl_params1 … lbl (sequential … (OP2 … op2 destr srcr1 srcr2) lbl') def
     328      | CLEAR_CARRY ⇒
     329        add_graph ertl_params1 … lbl (sequential … (CLEAR_CARRY …) lbl') def
     330      | SET_CARRY ⇒
     331        add_graph ertl_params1 … lbl (sequential … (SET_CARRY …) lbl') def
     332      | LOAD destr addr1 addr2 ⇒
     333        add_graph ertl_params1 … lbl (sequential … (LOAD … destr addr1 addr2) lbl') def
     334      | STORE addr1 addr2 srcr ⇒
     335        add_graph ertl_params1 … lbl (sequential … (STORE … addr1 addr2 srcr) lbl') def
     336      | COND srcr lbl_true ⇒
     337        add_graph ertl_params1 … lbl (sequential … (COND … srcr lbl_true) lbl') def
     338      | COMMENT msg ⇒
     339        add_graph ertl_params1 … lbl (sequential … (COMMENT … msg) lbl') def
     340      ]].
     341  @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
     342qed.
    527343
    528344(* hack with empty graphs used here *)
    529345definition translate_funct_internal ≝
    530   λdef.
    531   let nb_params ≝ |rtl_if_params def| in
     346  λglobals.λdef:rtlntc_internal_function globals.
     347  let nb_params ≝ |joint_if_params ?? def| in
    532348  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
    533   let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
    534   let entry' ≝ rtl_if_entry def in
    535   let exit' ≝ rtl_if_exit def in
    536   let graph' ≝ add ? ? (empty_map ? ?) entry' (ertl_st_skip entry') in
    537   let graph' ≝ add ? ? graph' exit' (ertl_st_skip exit') in
     349  let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in
     350  let entry' ≝ joint_if_entry … def in
     351  let exit' ≝ joint_if_exit … def in
     352  let graph' ≝ add ? ? (empty_map ? ?) entry' (GOTO … entry') in
     353  let graph' ≝ add ? ? graph' exit' (GOTO … exit') in
    538354  let def' ≝
    539     mk_ertl_internal_function
    540       (rtl_if_luniverse def) (rtl_if_runiverse def)
    541       nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
     355    mk_joint_internal_function globals (ertl_params globals)
     356      (joint_if_luniverse … def) (joint_if_runiverse … def) it
     357      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
    542358      graph' ? ? in
    543   let def' ≝ foldi ? ? ? translate_stmt (rtl_if_graph def) def' in
    544   let def' ≝ add_pro_and_epilogue (rtl_if_params def) (rtl_if_result def) def' in
    545     def'.
    546   [1: %
    547       [1: @entry'
    548       |2: normalize nodelta
    549           @graph_add_lookup
    550           @graph_add
    551       ]
    552   |2: %
    553       [1: @exit'
    554       |2: normalize nodelta
    555           @graph_add
    556       ]
     359  let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in
     360   add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
     361whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction
     362                                 makes the next application fail. Why? *)   
     363%
     364 [ @entry' | @graph_add_lookup @graph_add
     365 | @exit'  | @graph_add ]
     366qed.
     367
     368definition generate ≝
     369  λglobals.
     370  λstmt.
     371  λdef: joint_internal_function … (ertl_params globals).
     372  let 〈entry, def〉 ≝ fresh_label … def in
     373  let graph ≝ add … (joint_if_code … def) entry stmt in
     374   set_joint_if_graph … (ertl_params globals) graph def ??.
     375  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
     376  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
     377    *) cases daemon (*CSC: XXX *)
    557378  ]
    558379qed.
    559    
    560 definition translate_funct ≝
    561   λid_def: ident × ?.
    562   let 〈id, def〉 ≝ id_def in
    563   let def' ≝
    564     match def with
    565     [ Internal def ⇒ Internal ? (translate_funct_internal def)
    566     | External def ⇒ External ? def
    567     ] in
    568   〈id, def'〉.
    569 
    570 definition generate ≝
    571   λstmt.
    572   λdef.
    573   let 〈entry, nuniv〉 ≝ fresh_label def in
    574   let graph ≝ add ? ? (ertl_if_graph def) entry stmt in
    575     mk_ertl_internal_function
    576       nuniv (ertl_if_runiverse def) (ertl_if_params def)
    577       (ertl_if_locals def) (ertl_if_stacksize def) graph
    578       ? ?.
    579   [1: %
    580     [1: @entry
    581     |2: normalize nodelta;
    582         @graph_add
    583     ]
    584   |2: generalize in match (ertl_if_exit def)
    585       #HYP
    586       cases HYP
    587       #LBL #LBL_PRF
    588       %
    589       [1: @LBL
    590       |2: normalize nodelta;
    591           @graph_add_lookup
    592           @LBL_PRF
    593       ]
    594   ]
    595 qed.
    596    
    597 let rec find_and_remove_first_cost_label_internal
    598   (def: ertl_internal_function) (lbl: label) (num_nodes: nat)
     380
     381let rec find_and_remove_first_cost_label_internal (globals: list ident)
     382  (def: ertl_internal_function globals) (lbl: label) (num_nodes: nat)
    599383    on num_nodes ≝
    600384  match num_nodes with
    601385  [ O ⇒ 〈None ?, def〉
    602386  | S num_nodes' ⇒
    603     match lookup ? ? (ertl_if_graph def) lbl with
     387    match lookup … (joint_if_code … def) lbl with
    604388    [ None ⇒ 〈None ?, def〉
    605     | Some stmt ⇒
     389    | Some stmt ⇒ 
    606390      match stmt with
    607       [ ertl_st_cost cost_lbl next_lbl ⇒
    608           〈Some ? cost_lbl, add_graph lbl (ertl_st_skip next_lbl) def〉
    609       | ertl_st_cond _ _ _ ⇒ 〈None ?, def〉
    610       | ertl_st_return ⇒ 〈None ?, def〉
    611       | ertl_st_skip lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    612       | ertl_st_comment _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    613       | ertl_st_get_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    614       | ertl_st_set_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    615       | ertl_st_hdw_to_hdw _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    616       | ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    617       | ertl_st_push _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    618       | ertl_st_addr _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    619       | ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    620       | ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    621       | ertl_st_opaccs _ _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    622       | ertl_st_op1 _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    623       | ertl_st_op2 _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    624       | ertl_st_clear_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    625       | ertl_st_set_carry lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    626       | ertl_st_load _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    627       | ertl_st_store _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    628       | ertl_st_call_id _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    629       | ertl_st_new_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    630       | ertl_st_del_frame lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    631       | ertl_st_frame_size _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    632       ]
    633     ]
    634   ].
     391      [ sequential inst lbl ⇒
     392         match inst with
     393          [ COST_LABEL cost_lbl ⇒
     394             〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉
     395          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
     396      | RETURN ⇒ 〈None …, def〉
     397      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
     398      ]]].
    635399   
    636400definition find_and_remove_first_cost_label ≝
    637   λdef. 
    638     find_and_remove_first_cost_label_internal def (ertl_if_entry def) (graph_num_nodes ? (ertl_if_graph def)).
     401  λglobals,def. 
     402    find_and_remove_first_cost_label_internal globals def (joint_if_entry … def) (graph_num_nodes ? (joint_if_code … def)).
    639403
    640404definition move_first_cost_label_up_internal ≝
    641   λdef.
    642   let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label def in
     405  λglobals,def.
     406  let 〈cost_label, def〉 ≝ find_and_remove_first_cost_label def in
    643407  match cost_label with
    644408  [ None ⇒ def
    645   | Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entry def)) def
     409  | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
    646410  ].
    647411
    648 definition move_first_cost_label_up ≝
    649   λA: Type[0].
    650   λid_def: A × ?.
    651   let 〈id, def〉 ≝ id_def in
    652   let def' ≝
    653     match def with
    654     [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal int_fun)
    655     | External ext ⇒ def
    656     ]
    657   in
    658     〈id, def'〉.
    659 
    660 definition translate ≝
    661   λp.
     412definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
     413
     414definition translate : rtl_program → ertl_program ≝
     415 λp.
    662416  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
    663   let f ≝ λfunct. move_first_cost_label_up ? (translate_funct funct) in
    664   let vars ≝ map ? ? f (rtl_pr_functs p) in
    665     mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p).
     417    transform_program ??? p (transf_fundef ?? (translate_funct …)).
  • Deliverables/D3.3/id-lookup-branch/RTL/semantics.ma

    r1153 r1311  
    264264     [ nil ⇒ Some ? (smerge2 v)
    265265     | _ ⇒ None ? ]].
    266 
     266(*
    267267definition RTL_exec : execstep io_out io_in ≝
    268268  mk_execstep … ? is_final mem_of_state eval_statement.
    269 
     269*)
    270270(* CSC: XXX the program type does not fit with the globalenv and init_mem
    271271definition make_initial_state : rtl_program → res (genv × state) ≝
Note: See TracChangeset for help on using the changeset viewer.