Ignore:
Timestamp:
Sep 7, 2011, 12:10:27 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
1 deleted
7 edited

Legend:

Unmodified
Added
Removed

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

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

    r1153 r1197  
    11include "ASM/I8051.ma".
     2include "joint/Joint.ma".
    23include "utilities/BitVectorTrieSet.ma".
    34include "utilities/IdentifierTools.ma".
    … …  
    89definition registers ≝ list register.
    910
    10 inductive ertl_statement: Type[0] ≝
    11   | ertl_st_skip: label → ertl_statement
    12   | ertl_st_comment: String → label → ertl_statement
    13   | ertl_st_cost: costlabel → label → ertl_statement
    14   | ertl_st_get_hdw: register → Register → label → ertl_statement
    15   | ertl_st_set_hdw: Register → register → label → ertl_statement
    16   | ertl_st_hdw_to_hdw: Register → Register → label → ertl_statement
    17   | ertl_st_new_frame: label → ertl_statement
    18   | ertl_st_del_frame: label → ertl_statement
    19   | ertl_st_frame_size: register → label → ertl_statement
    20   | ertl_st_pop: register → label → ertl_statement
    21   | ertl_st_push: register → label → ertl_statement
    22   | ertl_st_addr: register → register → ident → label → ertl_statement
    23 (* XXX: changed from O'Caml
    24   | ertl_st_addr_h: register → ident → label → ertl_statement
    25   | ertl_st_addr_l: register → ident → label → ertl_statement
    26 *)
    27   | ertl_st_int: register → Byte → label → ertl_statement
    28   | ertl_st_move: register → register → label → ertl_statement
    29   | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
    30 (* XXX: changed from O'Caml
    31   | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
    32   | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
    33 *)
    34   | ertl_st_op1: Op1 → register → register → label → ertl_statement
    35   | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
    36   | ertl_st_clear_carry: label → ertl_statement
    37   | ertl_st_set_carry: label → ertl_statement
    38   | ertl_st_load: register → register → register → label → ertl_statement
    39   | ertl_st_store: register → register → register → label → ertl_statement
    40   | ertl_st_call_id: ident → nat → label → ertl_statement
    41   | ertl_st_cond: register → label → label → ertl_statement
    42   | ertl_st_return: ertl_statement.
     11inductive move_registers: Type[0] ≝
     12  | pseudo: register → move_registers
     13  | hardware: Register → move_registers.
     14                 
     15inductive ertl_statement_extension: Type[0] ≝
     16  | ertl_st_ext_new_frame: label → ertl_statement_extension
     17  | ertl_st_ext_del_frame: label → ertl_statement_extension
     18  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
    4319
    44 definition ertl_statement_graph ≝ graph ertl_statement.
     20definition ertl_params: params ≝
     21 mk_params
     22   register register register register
     23     (move_registers × move_registers) register
     24       ertl_statement_extension unit (list register) nat.
    4525
    46 record ertl_internal_function: Type[0] ≝
     26definition ertl_statement ≝ joint_statement ertl_params.
     27
     28definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
     29
     30record ertl_internal_function (globals: list ident): Type[0] ≝
    4731{
    4832  ertl_if_luniverse: universe LabelTag;
    … …  
    5135  ertl_if_locals: registers;
    5236  ertl_if_stacksize: nat;
    53   ertl_if_graph: ertl_statement_graph;
     37  ertl_if_graph: ertl_statement_graph globals;
    5438  ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
    5539  ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
    5640}.
    5741
    58 definition ertl_function ≝ fundef ertl_internal_function.
     42definition set_luniverse ≝
     43  λglobals  : list ident.
     44  λint_fun  : ertl_internal_function globals.
     45  λluniverse: universe LabelTag.
     46  let runiverse ≝ ertl_if_runiverse globals int_fun in
     47  let params    ≝ ertl_if_params globals int_fun in
     48  let locals    ≝ ertl_if_locals globals int_fun in
     49  let stacksize ≝ ertl_if_stacksize globals int_fun in
     50  let graph     ≝ ertl_if_graph globals int_fun in
     51  let entry     ≝ ertl_if_entry globals int_fun in
     52  let exit      ≝ ertl_if_exit globals int_fun in
     53    mk_ertl_internal_function globals
     54      luniverse runiverse params locals
     55      stacksize graph entry exit.
     56
     57definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
    5958 
    60 record ertl_program: Type[0] ≝
     59record ertl_program (globals: list ident): Type[0] ≝
    6160{
    6261  ertl_pr_vars: list (ident × nat);
    63   ertl_pr_funcs: list (ident × ertl_function);
     62  ertl_pr_funcs: list (ident × (ertl_function globals));
    6463  ertl_pr_main: option ident
    6564}.
     65
     66
     67(* XXX: changed from O'Caml
     68  | ertl_st_addr_h: register → ident → label → ertl_statement
     69  | ertl_st_addr_l: register → ident → label → ertl_statement
     70*)
     71
     72(* XXX: changed from O'Caml
     73  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
     74  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
     75*)

  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma

    r1153 r1197  
    11include "ERTL/ERTL.ma".
    2 include "ERTL/ERTLToLTLI.ma".
    32include "LTL/LTL.ma".
    43include "ERTL/spill.ma".
     4include "ERTL/build.ma".
     5include "utilities/Interference.ma".
     6include "ASM/Arithmetic.ma".
     7
     8(* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *)
     9
     10inductive decision: Type[0] ≝
     11  | decision_spill: Byte → decision
     12  | decision_colour: Register → decision.
     13 
     14definition interference_lookup ≝
     15  λglobals.
     16  λint_fun.
     17  λr.
     18  let 〈liveafter, graph〉 ≝ build globals int_fun in
     19  let lkup ≝ ig_lookup graph r in
     20    vm_find lkup colour_colouring.
     21 
     22definition lookup: register → decision ≝
     23  λr.
     24  match ? r with
     25  [ colour_spill
     26 
     27axiom lookup: register → decision.
     28
     29definition fresh_label ≝
     30  λglobals: list ident.
     31  λluniv.
     32    fresh LabelTag luniv.
     33
     34definition add_graph ≝
     35  λglobals.
     36  λlabel.
     37  λstmt: ltl_statement globals.
     38  λgraph: ltl_statement_graph globals.
     39    add LabelTag ? graph label stmt.
     40
     41definition generate ≝
     42  λglobals: list ident.
     43  λluniv.
     44  λgraph: ltl_statement_graph globals.
     45  λstmt: ltl_statement globals.
     46  let 〈l, luniv〉 ≝ fresh_label globals luniv in
     47  let graph ≝ add_graph globals l stmt graph in
     48    〈l, graph, luniv〉.
     49
     50definition num_locals ≝
     51  λglobals.
     52  λint_fun.
     53    colour_locals + (ertl_if_stacksize globals int_fun).
     54
     55definition stacksize ≝
     56  λglobals.
     57  λint_fun.
     58    colour_locals + (ertl_if_stacksize globals int_fun).
     59
     60definition adjust_off ≝
     61  λglobals.
     62  λint_fun.
     63  λoff.
     64  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
     65  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in
     66    sub.
     67
     68definition get_stack:
     69 ∀globals. ertl_internal_function globals → graph (ltl_statement globals) → Register → Byte → label →
     70  ltl_statement globals × (graph (ltl_statement globals)) × (universe LabelTag)
     71≝
     72  λglobals: list ident.
     73  λint_fun.
     74  λgraph: graph (ltl_statement (globals)).
     75  λr.
     76  λoff.
     77  λl.
     78    let off ≝ adjust_off globals int_fun off in
     79    let luniv ≝ ertl_if_luniverse globals int_fun in
     80    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc r)) l) in
     81    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
     82    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     83    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     84    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
     85    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
     86    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
     87      〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
     88
     89definition set_stack:
     90  ∀globals. ertl_internal_function globals → ltl_statement_graph globals → Byte
     91    → Register → label → ((ltl_statement globals) × (ltl_statement_graph globals) × (universe LabelTag)) ≝
     92  λglobals: list ident.
     93  λint_fun.
     94  λgraph: graph (ltl_statement (globals)).
     95  λoff.
     96  λr.
     97  λl.
     98  let off ≝ adjust_off globals int_fun off in
     99  let luniv ≝ ertl_if_luniverse globals int_fun in
     100  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store ltl_params … globals it it it) l) in
     101  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc r)) l) in
     102  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     103  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     104  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
     105  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
     106  let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
     107    〈joint_st_sequential … ltl_params globals (joint_instr_int ? globals RegisterA off) l, graph, luniv〉.
     108
     109definition write:
     110  ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register → label →
     111    ? ≝
     112  λglobals: list ident.
     113  λint_fun.
     114  λgraph.
     115  λr.
     116  λl.
     117  match lookup r with
     118  [ decision_spill off ⇒
     119    let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph off RegisterSST l in
     120    let 〈l, graph, int_fun〉 ≝ generate globals luniv graph stmt in
     121      〈RegisterSST, l, graph, luniv〉
     122  | decision_colour hwr ⇒
     123    let luniv ≝ ertl_if_luniverse globals int_fun in
     124      〈hwr, l, graph, luniv〉
     125  ].
     126
     127definition read:
     128  ∀globals: list ident. ertl_internal_function globals → ltl_statement_graph globals → register
     129    → (Register → ltl_statement globals) → ? ≝
     130  λglobals.
     131  λint_fun.
     132  λgraph.
     133  λr.
     134  λstmt.
     135  match lookup r with
     136  [ decision_colour hwr ⇒ generate globals (ertl_if_luniverse globals int_fun) graph (stmt hwr)
     137  | decision_spill off ⇒
     138    let temphwr ≝ RegisterSST in
     139    let 〈l, graph, luniv〉 ≝ generate globals (ertl_if_luniverse globals int_fun) graph (stmt temphwr) in
     140    let 〈stmt, graph, luniv〉 ≝ get_stack globals int_fun graph temphwr off l in
     141      generate globals luniv graph stmt
     142  ].
     143
     144definition move ≝
     145  λglobals: list ident.
     146  λint_fun.
     147  λgraph: graph (ltl_statement globals).
     148  λdest: decision.
     149  λsrc: decision.
     150  λl: label.
     151  match dest with
     152  [ decision_colour dest_hwr ⇒
     153    match src with
     154    [ decision_colour src_hwr ⇒
     155      let luniv ≝ ertl_if_luniverse globals int_fun in
     156      if eq_Register dest_hwr src_hwr then
     157        〈joint_st_goto … globals l, graph, luniv〉
     158      else
     159        let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc dest_hwr)) l) in
     160          〈joint_st_sequential … globals (joint_instr_move … ltl_params globals (to_acc src_hwr)) l, graph, luniv〉
     161    | decision_spill src_off ⇒ get_stack globals int_fun graph dest_hwr src_off l
     162    ]
     163  | decision_spill dest_off ⇒
     164    match src with
     165    [ decision_colour src_hwr ⇒ set_stack globals int_fun graph dest_off src_hwr l
     166    | decision_spill src_off ⇒
     167      let luniv ≝ ertl_if_luniverse globals int_fun in
     168      if eq_bv ? dest_off src_off then
     169        〈joint_st_goto … globals l, graph, luniv〉
     170      else
     171        let temp_hwr ≝ RegisterSST in
     172        let 〈stmt, graph, luniv〉 ≝ set_stack globals int_fun graph dest_off temp_hwr l in
     173        let 〈l, graph, luniv〉 ≝ generate globals luniv graph stmt in
     174          get_stack globals int_fun graph temp_hwr src_off l
     175    ]
     176  ].
     177
     178definition newframe ≝
     179  λglobals: list ident.
     180  λint_fun: ertl_internal_function globals.
     181  λgraph: ltl_statement_graph globals.
     182  λl: label.
     183  if eq_nat (stacksize globals int_fun) 0 then
     184    〈joint_st_goto ltl_params globals l, graph, (ertl_if_luniverse globals int_fun)〉
     185  else
     186    let luniv ≝ ertl_if_luniverse globals int_fun in
     187    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
     188    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
     189    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
     190    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
     191    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
     192    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
     193    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_clear_carry … globals) l) in
     194    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
     195      〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc RegisterSPL)) l, graph, luniv〉.
     196
     197definition delframe ≝
     198  λglobals.
     199  λint_fun.
     200  λgraph: graph (ltl_statement globals).
     201  λl.
     202  if eq_nat (stacksize globals int_fun) 0 then
     203    〈joint_st_goto ltl_params globals l, graph, ertl_if_luniverse globals int_fun〉
     204  else
     205    let luniv ≝ ertl_if_luniverse globals int_fun in
     206    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
     207    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     208    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_int … globals RegisterA (zero ?)) l) in
     209    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
     210    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ltl_params globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
     211      〈joint_st_sequential ltl_params globals (joint_instr_int ltl_params globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
     212
     213definition translate_statement ≝
     214  λglobals: list ident.
     215  λint_fun.
     216  λgraph: ltl_statement_graph globals.
     217  λstmt: ertl_statement globals.
     218  match stmt with
     219  [ joint_st_sequential seq l ⇒
     220    let luniv ≝ ertl_if_luniverse globals int_fun in
     221    match seq with
     222    [ joint_instr_comment c ⇒
     223      〈joint_st_sequential ltl_params globals (joint_instr_comment … globals c) l, graph, luniv〉
     224    | joint_instr_cost_label cost_lbl ⇒
     225      〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉
     226    | joint_instr_pop r ⇒
     227      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     228      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     229        〈joint_st_sequential … globals (joint_instr_pop ltl_params globals it) l, graph, luniv〉
     230    | joint_instr_push r ⇒
     231      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in
     232      let int_fun ≝ set_luniverse globals int_fun luniv in
     233      let 〈l, graph, luniv〉 ≝ read globals int_fun graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     234        〈joint_st_goto ltl_params globals l, graph, luniv〉
     235    | joint_instr_cond srcr lbl_true ⇒
     236      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
     237      let int_fun ≝ set_luniverse globals int_fun luniv in
     238      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     239        〈joint_st_goto ltl_params globals l, graph, luniv〉
     240    | joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉
     241    | joint_instr_store addr1 addr2 srcr ⇒
     242      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
     243      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST1)) l) in
     244      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     245      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
     246      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
     247      let int_fun ≝ set_luniverse globals int_fun luniv in
     248      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     249      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
     250      let int_fun ≝ set_luniverse globals int_fun luniv in
     251      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     252      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
     253      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     254        〈joint_st_goto ltl_params globals l, graph, luniv〉
     255    | joint_instr_load destr addr1 addr2 ⇒
     256      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
     257      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     258      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
     259      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     260      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
     261      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
     262      let int_fun ≝ set_luniverse globals int_fun luniv in
     263      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     264      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
     265      let int_fun ≝ set_luniverse globals int_fun luniv in
     266      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     267        〈joint_st_goto ltl_params globals l, graph, luniv〉
     268    | joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉
     269    | joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉
     270    | joint_instr_op2 op2 destr srcr ⇒
     271      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
     272      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     273      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in
     274      let luniv ≝ set_luniverse globals int_fun luniv in
     275      let 〈l, graph, luniv〉 ≝ read globals int_fun graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     276      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
     277      let luniv ≝ set_luniverse globals int_fun luniv in
     278      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     279        〈joint_st_goto ltl_params globals l, graph, luniv〉
     280    | joint_instr_op1 op1 acc_a ⇒
     281      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a l in
     282      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     283      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in
     284      let int_fun ≝ set_luniverse globals int_fun luniv in
     285      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     286        〈joint_st_goto ltl_params globals l, graph, luniv〉
     287    | joint_instr_int r i ⇒
     288      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     289        〈joint_st_sequential ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉
     290    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
     291      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a_reg l in
     292      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     293      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
     294      let luniv ≝ set_luniverse globals int_fun luniv in
     295      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     296      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
     297      let luniv ≝ set_luniverse globals int_fun luniv in
     298      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     299      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in
     300      let luniv ≝ set_luniverse globals int_fun luniv in
     301      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_b_reg l in
     302      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     303      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in
     304      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
     305      let luniv ≝ set_luniverse globals int_fun luniv in
     306      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     307      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
     308      let luniv ≝ set_luniverse globals int_fun luniv in
     309      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     310        〈joint_st_goto ltl_params globals l, graph, luniv〉
     311    | joint_instr_move pair_regs ⇒
     312      let regl ≝ \fst pair_regs in
     313      let regr ≝ \snd pair_regs in
     314      match regl with
     315      [ pseudo p1  ⇒
     316        match regr with
     317        [ pseudo p2  ⇒ move globals int_fun graph (lookup p1) (lookup p2) l
     318        | hardware h ⇒ move globals int_fun graph (lookup p1) (decision_colour h) l
     319        ]
     320      | hardware h1 ⇒
     321        match regr with
     322        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (lookup p) l
     323        | hardware h2 ⇒
     324          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in
     325            〈joint_st_sequential ltl_params globals (joint_instr_move ltl_params globals (to_acc h2)) l, graph, luniv〉
     326        ]
     327      ]
     328    | joint_instr_address lbl prf dpl dph ⇒
     329      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun graph dph l in
     330      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in
     331      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
     332      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in
     333      let int_fun ≝ set_luniverse globals int_fun luniv in
     334      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun graph dpl l in
     335      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
     336      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
     337        〈joint_st_sequential ltl_params globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
     338    ]
     339  | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉
     340  | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉
     341  | joint_st_extension ext ⇒
     342    match ext with
     343    [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
     344    | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
     345    | ertl_st_ext_frame_size r l ⇒
     346      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     347        〈joint_st_sequential … globals (joint_instr_int ltl_params globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     348    ]
     349  ].
    5350
    6351definition translate_internal ≝
     352  λglobals: list ident.
    7353  λf.
    8354  λint_fun: ertl_internal_function.
    9 
    10   let fresh_label () = Label.Gen.fresh int_fun.ERTL.f_luniverse in
    11 
    12   let add_graph lbl stmt = graph := Label.Map.add lbl stmt !graph in
    13 
    14   let generate stmt =
    15     let l = fresh_label () in
    16     add_graph l stmt ;
    17     l in
    18 
    19   (* Build an interference graph for this function, and color
    20      it. Define a function that allows consulting the coloring. *)
    21 
    22   let module G = struct
    23     let liveafter, graph = Build.build int_fun
    24     let uses = Uses.examine_internal int_fun
    25     let verbose = false
    26     let () =
    27       if verbose then
    28         Printf.printf "Starting hardware register allocation for %s.\n" f
    29   end in
    30 
    31   let module C = Coloring.Color (G) in
    32 
    33   let lookup r =
    34     Interference.Vertex.Map.find (Interference.lookup G.graph r) C.coloring
    35   in
    36 
    37   (* Restrict the interference graph to concern spilled vertices only,
    38      and color it again, this time using stack slots as colors. *)
    39 
    40   let module H = struct
    41     let graph = Interference.droph (Interference.restrict G.graph (fun v ->
    42       match Interference.Vertex.Map.find v C.coloring with
    43       | Coloring.Spill ->
    44           true
    45       | Coloring.Color _ ->
    46           false
    47     ))
    48     let verbose = false
    49     let () =
    50       if verbose then
    51         Printf.printf "Starting stack slot allocation for %s.\n" f
    52   end in
    53 
    54   let module S = Spill.Color (H) in
    55 
    56   (* Define a new function that consults both colorings at once. *)
    57 
    58   let lookup r =
     355  let lookup ≝ λr.
    59356    match lookup r with
    60     | Coloring.Spill ->
     357    | colour_spill ->
    61358        ERTLToLTLI.Spill (Interference.Vertex.Map.find (Interference.lookup H.graph r) S.coloring)
    62     | Coloring.Color color ->
     359    | colour_colour color ->
    63360        ERTLToLTLI.Color color
    64361  in
    65 
    66   (* We are now ready to instantiate the functor that deals with the
    67      translation of instructions. The reason why we make this a
    68      separate functor is purely pedagogical. Smaller modules are
    69      easier to understand. *)
    70 
    71   (* We add the additional stack size required for spilled register to the stack
    72      size previously required for the function: this is the final stack size
    73      required for the locals. *)
    74 
    75   let locals = S.locals + int_fun.ERTL.f_stacksize in
    76 
    77   (* The full stack size is then the size of the locals in the stack plus the
    78      size of the formal parameters of the function. *)
    79 
    80   let stacksize = int_fun.ERTL.f_params + locals in
    81 
    82   let module I = ERTLToLTLI.Make (struct
    83     let lookup = lookup
    84     let generate = generate
    85     let fresh_label = fresh_label
    86     let add_graph = add_graph
    87     let locals = locals
    88     let stacksize = stacksize
    89   end) in
    90 
    91   (* Translate the instructions in the existing control flow graph.
    92      Pure instructions whose destination pseudo-register is dead are
    93      eliminated on the fly. *)
     362  let locals ≝ colour_locals + (ertl_if_stacksize int_fun) in
     363  let stacksize ≝ (ertl_if_params int_fun) + locals in
     364    mk_ltl_internal_function
     365      globals
     366      (ertl_if_luniverse int_fun)
     367      (ertl_if_runiverse int_fun)
     368      stacksize.
    94369
    95370  let () =
    … …  
    106381  in
    107382
    108   (* Build a [LTL] function. *)
    109 
    110   {
    111     LTL.f_luniverse = int_fun.ERTL.f_luniverse;
    112     LTL.f_stacksize = stacksize ;
    113     LTL.f_entry = int_fun.ERTL.f_entry;
    114     LTL.f_exit = int_fun.ERTL.f_exit;
    115     LTL.f_graph = !graph
    116   }
    117 
    118383definition translate_funct ≝
    119384  λname_def.

  • Deliverables/D3.3/id-lookup-branch/ERTL/build.ma

    r1153 r1197  
    33
    44definition build ≝
    5   λint_fun: ertl_internal_function.
    6   let liveafter ≝ analyse int_fun in
    7   let graph ≝ ig_create (ertl_if_locals int_fun) in
    8   let graph ≝ ig_mkiph graph (ertl_if_locals int_fun) forbidden_registers in
     5  λglobals: list ident.
     6  λint_fun: ertl_internal_function globals.
     7  let liveafter ≝ analyse globals int_fun in
     8  let graph ≝ ig_create (ertl_if_locals globals int_fun) in
     9  let graph ≝ ig_mkiph graph (ertl_if_locals globals int_fun) RegistersForbidden in
    910  let graph ≝
    1011    foldi ? ? ? (λlabel. λstmt. λgraph.
    1112      let live ≝ liveafter label in
    12       match eliminable live stmt with
     13      match eliminable globals live stmt with
    1314      [ Some _ ⇒ graph
    1415      | None   ⇒
    15         let defined ≝ defined stmt in
     16        let defined ≝ defined globals stmt in
    1617        let exceptions ≝
    1718          match stmt with
    18           [ ertl_st_move _ sr _    ⇒ lattice_psingleton sr
    19           | ertl_st_set_hdw _ sr _ ⇒ lattice_psingleton sr
    20           | ertl_st_get_hdw _ sr _ ⇒ lattice_hsingleton sr
    21           | _                      ⇒ ?
     19          [ joint_st_sequential seq l ⇒
     20            match seq with
     21            [ joint_instr_move pair_reg ⇒
     22              let reg_r ≝ \snd pair_reg in
     23              match reg_r with
     24              [ hardware hw ⇒ lattice_hsingleton hw
     25              | pseudo   ps ⇒ lattice_psingleton ps
     26              ]
     27            | _                         ⇒ ?
     28            ]
     29          | _ ⇒ ?
    2230          ]
    2331        in
    … …  
    2533        let graph ≝
    2634          match stmt with
    27           [ ertl_st_move r1 r2 _    ⇒ ig_mkppp graph r1 r2
    28           | ertl_st_get_hdw r hwr _ ⇒ ig_mkpph graph r hwr
    29           | ertl_st_set_hdw hwr r _ ⇒ ig_mkpph graph r hwr
    30           | _                       ⇒ graph
     35          [ joint_st_sequential seq l ⇒
     36            match seq with
     37            [ joint_instr_move pair_reg ⇒
     38              let reg_l ≝ \fst pair_reg in
     39              let reg_r ≝ \snd pair_reg in
     40              match reg_l with
     41              [ pseudo ps1 ⇒
     42                match reg_r with
     43                [ pseudo ps2  ⇒ ig_mkppp graph ps1 ps2
     44                | hardware hw ⇒ ig_mkpph graph ps1 hw
     45                ]
     46              | hardware hw1 ⇒
     47                match reg_r with
     48                [ pseudo ps    ⇒ ig_mkpph graph ps hw1
     49                | hardware hw2 ⇒ graph
     50                ]
     51              ]
     52            | _ ⇒ graph
     53            ]
     54          | _ ⇒ graph
    3155          ]
    3256        in graph
    33       ]) (ertl_if_graph int_fun) graph
     57      ]) (ertl_if_graph globals int_fun) graph
    3458  in
    3559    〈liveafter, graph〉.

  • Deliverables/D3.3/id-lookup-branch/ERTL/liveness.ma

    r1153 r1197  
    3535
    3636definition statement_successors ≝
    37   λs: ertl_statement.
     37  λglobals: list ident.
     38  λs: ertl_statement globals.
    3839  match s with
    39   [ ertl_st_return ⇒ [ ]
    40   | ertl_st_skip l ⇒ [ l ]
    41   | ertl_st_comment c l ⇒ [ l ]
    42   | ertl_st_cost c l ⇒ [ l ]
    43   | ertl_st_set_hdw _ _ l ⇒ [ l ]
    44   | ertl_st_get_hdw _ _ l ⇒ [ l ]
    45   | ertl_st_hdw_to_hdw _ _ l ⇒ [ l ]
    46   | ertl_st_new_frame l ⇒ [ l ]
    47   | ertl_st_del_frame l ⇒ [ l ]
    48   | ertl_st_frame_size _ l ⇒ [ l ]
    49   | ertl_st_push _ l ⇒ [ l ]
    50   | ertl_st_pop _ l ⇒ [ l ]
    51   | ertl_st_addr _ _ _ l ⇒ [ l ]
    52   | ertl_st_int _ _ l ⇒ [ l ]
    53   | ertl_st_move _ _ l ⇒ [ l ]
    54   | ertl_st_opaccs _ _ _ _ _ l ⇒ [ l ]
    55   | ertl_st_op1 _ _ _ l ⇒ [ l ]
    56   | ertl_st_op2 _ _ _ _ l ⇒ [ l ]
    57   | ertl_st_clear_carry l ⇒ [ l ]
    58   | ertl_st_set_carry l ⇒ [ l ]
    59   | ertl_st_load _ _ _ l ⇒ [ l ]
    60   | ertl_st_store _ _ _ l ⇒ [ l ]
    61   | ertl_st_call_id _ _ l ⇒ [ l ]
    62   | ertl_st_cond _ l1 l2 ⇒
    63       list_set_add ? (eq_identifier ?) l1 [ l2 ]
     40  [ joint_st_sequential seq l ⇒
     41    match seq with
     42    [ joint_instr_cond acc_a_reg lbl_true ⇒
     43        list_set_add ? (eq_identifier ?) lbl_true [ l ]
     44    | _ ⇒ [ l ]
     45    ]
     46  | joint_st_extension ext ⇒
     47    match ext with
     48    [ ertl_st_ext_new_frame l ⇒ [ l ]
     49    | ertl_st_ext_del_frame l ⇒ [ l ]
     50    | ertl_st_ext_frame_size r l ⇒ [ l ]
     51    ]
     52  | joint_st_goto l ⇒ [ l ]
     53  | joint_st_return ⇒ [ ]
    6454  ].
    6555
    … …  
    122112    lattice_is_maximal.
    123113
    124 definition defined: ertl_statement → register_lattice ≝
    125   λs.
     114definition defined ≝
     115  λglobals: list ident.
     116  λs: ertl_statement globals.
    126117  match s with
    127   [ ertl_st_skip _ ⇒ lattice_bottom
    128   | ertl_st_comment _ _ ⇒ lattice_bottom
    129   | ertl_st_cost _ _ ⇒ lattice_bottom
    130   | ertl_st_push _ _⇒ lattice_bottom
    131   | ertl_st_store _ _ _ _ ⇒ lattice_bottom
    132   | ertl_st_cond _ _ _ ⇒ lattice_bottom
    133   | ertl_st_return ⇒ lattice_bottom
    134   | ertl_st_clear_carry _ ⇒ lattice_hsingleton RegisterCarry
    135   | ertl_st_set_carry _ ⇒ lattice_hsingleton RegisterCarry
    136   | ertl_st_op2 op2 r _ _ _ ⇒
    137     match op2 with
    138     [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    139     | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    140     | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
    141     | _ ⇒ lattice_psingleton r
    142     ]
    143   | ertl_st_op1 op1 r _ _ ⇒ lattice_psingleton r
    144   | ertl_st_get_hdw r _ _ ⇒ lattice_psingleton r
    145   | ertl_st_frame_size r _ ⇒ lattice_psingleton r
    146   | ertl_st_pop r _ ⇒ lattice_psingleton r
    147   | ertl_st_int r _ _ ⇒ lattice_psingleton r
    148   | ertl_st_addr r1 r2 _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    149   | ertl_st_move r _ _ ⇒ lattice_psingleton r
    150   (* XXX: change from o'caml *)
    151   | ertl_st_opaccs _ r1 r2 _ _ _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    152   | ertl_st_load r _ _ _ ⇒ lattice_psingleton r
    153   | ertl_st_set_hdw r _ _ ⇒ lattice_hsingleton r
    154   | ertl_st_hdw_to_hdw r _ _ ⇒ lattice_hsingleton r
    155   (* Potentially destroys all caller-save hardware registers. *)
    156   | ertl_st_call_id _ _ _ ⇒ 〈[ ], RegisterCallerSaved〉
    157   | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    158   | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     118  [ joint_st_sequential seq l ⇒
     119    match seq with
     120    [ joint_instr_op2 op2 r _ ⇒
     121      match op2 with
     122      [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     123      | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     124      | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
     125      | _ ⇒ lattice_psingleton r
     126      ]
     127    | joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry
     128    | joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry
     129    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     130    | joint_instr_op1 op1 r ⇒ lattice_psingleton r
     131    | joint_instr_pop r ⇒ lattice_psingleton r
     132    | joint_instr_int r _ ⇒ lattice_psingleton r
     133    | joint_instr_address _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     134    | joint_instr_load r _ _ ⇒ lattice_psingleton r
     135    (* Potentially destroys all caller-save hardware registers. *)
     136    | joint_instr_call_id _ _ ⇒ 〈[ ], RegisterCallerSaved〉
     137    | joint_instr_comment c ⇒ lattice_bottom
     138    | joint_instr_cond r lbl_true ⇒ lattice_bottom
     139    | joint_instr_store acc_a dpl dph ⇒ lattice_bottom
     140    | joint_instr_cost_label clabel ⇒ lattice_bottom
     141    | joint_instr_push r ⇒ lattice_bottom
     142    | joint_instr_move pair_reg ⇒
     143      (* first register relevant only *)
     144      let r1 ≝ \fst pair_reg in
     145      match r1 with
     146      [ pseudo p ⇒ lattice_psingleton p
     147      | hardware h ⇒ lattice_hsingleton h
     148      ]
     149    ]
     150  | joint_st_return ⇒ lattice_bottom
     151  | joint_st_extension ext ⇒
     152    match ext with
     153    [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     154    | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     155    | ertl_st_ext_frame_size r l ⇒ lattice_psingleton r
     156    ]
     157  | joint_st_goto l ⇒ lattice_bottom
    159158  ].
    160159
    … …  
    169168definition ret_regs ≝ list_set_of_list RegisterRets.
    170169
    171 definition used: ertl_statement → register_lattice ≝
    172   λstmt.
    173   match stmt with
    174   [ ertl_st_skip _ ⇒ lattice_bottom
    175   | ertl_st_cost _ _ ⇒ lattice_bottom
    176   | ertl_st_comment _ _ ⇒ lattice_bottom
    177   | ertl_st_frame_size _ _ ⇒ lattice_bottom
    178   | ertl_st_pop _ _ ⇒ lattice_bottom
    179   | ertl_st_addr _ _ _ _ ⇒ lattice_bottom
    180   | ertl_st_int _ _ _ ⇒ lattice_bottom
    181   | ertl_st_clear_carry _ ⇒ lattice_bottom
    182   | ertl_st_set_carry _ ⇒ lattice_bottom
     170definition used ≝
     171  λglobals: list ident.
     172  λs: ertl_statement globals.
     173  match s with
     174  [ joint_st_sequential seq l ⇒
     175    match seq with
     176    [ joint_instr_op2 op2 acc_a r ⇒
     177      match op2 with
     178      [ Addc ⇒
     179        lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)) (lattice_hsingleton RegisterCarry)
     180      | _ ⇒ lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)
     181      ]
     182    | joint_instr_clear_carry ⇒ lattice_bottom
     183    | joint_instr_set_carry ⇒ lattice_bottom
     184    (* acc_a and acc_b *)
     185    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
     186    | joint_instr_op1 op1 r ⇒ lattice_psingleton r
     187    | joint_instr_pop r ⇒ lattice_bottom
     188    | joint_instr_int r _ ⇒ lattice_bottom
     189    | joint_instr_address _ _ r1 r2 ⇒ lattice_bottom
     190    | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
    183191    (* Reads the hardware registers that are used to pass parameters. *)
    184   | ertl_st_call_id _ nparams _ ⇒
    185     〈[ ], list_set_of_list (prefix ? nparams RegisterParameters)〉
    186   | ertl_st_get_hdw _ r _ ⇒ lattice_hsingleton r
    187   | ertl_st_hdw_to_hdw _ r _ ⇒ lattice_hsingleton r
    188   | ertl_st_set_hdw _ r _ ⇒ lattice_psingleton r
    189   | ertl_st_push r _ ⇒ lattice_psingleton r
    190   | ertl_st_move _ r _ ⇒ lattice_psingleton r
    191   | ertl_st_op1 _ _ r _ ⇒ lattice_psingleton r
    192   | ertl_st_cond r _ _ ⇒ lattice_psingleton r
    193   | ertl_st_op2 op2 _ r1 r2 _ ⇒
    194     match op2 with
    195     [ Addc ⇒
    196       lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_hsingleton RegisterCarry)
    197     | _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    198     ]
    199   | ertl_st_opaccs _ d1 d2 s1 s2 _ ⇒ lattice_join (lattice_psingleton s1) (lattice_psingleton s2)
    200   | ertl_st_load _ r1 r2 _ ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    201   | ertl_st_store r1 r2 r3 _ ⇒
    202     lattice_join (lattice_join (lattice_psingleton r1) (lattice_psingleton r2)) (lattice_psingleton r3)
    203   | ertl_st_new_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    204   | ertl_st_del_frame _ ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    205   | ertl_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
    206   ].
    207 
    208 definition eliminable: register_lattice → ertl_statement → option label ≝
    209   λl.
    210   λstmt.
     192    | joint_instr_call_id _ nparams ⇒ 〈[ ], list_set_of_list (prefix ? nparams RegisterParams)〉
     193    | joint_instr_comment c ⇒ lattice_bottom
     194    | joint_instr_cond r lbl_true ⇒ lattice_psingleton r
     195    | joint_instr_store acc_a dpl dph ⇒
     196      lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph)
     197    | joint_instr_cost_label clabel ⇒ lattice_bottom
     198    | joint_instr_push r ⇒ lattice_psingleton r
     199    | joint_instr_move pair_reg ⇒
     200      (* only second reg in pair relevant *)
     201      let r2 ≝ \snd pair_reg in
     202      match r2 with
     203      [ pseudo p ⇒ lattice_psingleton p
     204      | hardware h ⇒ lattice_hsingleton h
     205      ]
     206    ]
     207  | joint_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉
     208  | joint_st_goto l ⇒ lattice_bottom
     209  | joint_st_extension ext ⇒
     210    match ext with
     211    [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     212    | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     213    | ertl_st_ext_frame_size r l ⇒ lattice_bottom
     214    ]
     215  ].
     216
     217definition eliminable ≝
     218  λglobals: list ident.
     219  λl: register_lattice.
     220  λs: ertl_statement globals.
    211221  let 〈pliveafter, hliveafter〉 ≝ l in
    212   match stmt with
    213   [ ertl_st_skip _ ⇒ None ?
    214   | ertl_st_comment _ _ ⇒ None ?
    215   | ertl_st_cost _ _ ⇒ None ?
    216   | ertl_st_new_frame _ ⇒ None ?
    217   | ertl_st_del_frame _ ⇒ None ?
    218   | ertl_st_pop _ _ ⇒ None ?
    219   | ertl_st_push _ _ ⇒ None ?
    220   | ertl_st_clear_carry _  ⇒ None ?
    221   | ertl_st_set_carry _  ⇒ None ?
    222   | ertl_st_store _ _ _ _ ⇒ None ?
    223   | ertl_st_call_id _ _ _ ⇒ None ?
    224   | ertl_st_cond _ _ _ ⇒ None ?
    225   | ertl_st_return ⇒ None ?
    226   | ertl_st_get_hdw r _ l ⇒
    227     if list_set_member register (eq_identifier ?) r pliveafter ∨
    228        list_set_member Register eq_Register RegisterCarry hliveafter then
    229       None ?
    230     else
    231       Some ? l
    232   | ertl_st_frame_size r l ⇒
    233     if list_set_member register (eq_identifier ?) r pliveafter ∨
    234        list_set_member Register eq_Register RegisterCarry hliveafter then
    235       None ?
    236     else
    237       Some ? l
    238   | ertl_st_int r _ l ⇒
    239     if list_set_member register (eq_identifier ?) r pliveafter ∨
    240        list_set_member Register eq_Register RegisterCarry hliveafter then
    241       None ?
    242     else
    243       Some ? l
    244   | ertl_st_addr r1 r2 _ l ⇒
    245     if list_set_member register (eq_identifier ?) r1 pliveafter ∨
    246        list_set_member register (eq_identifier ?) r2 pliveafter ∨
    247        list_set_member Register eq_Register RegisterCarry hliveafter then
    248       None ?
    249     else
    250       Some ? l
    251   | ertl_st_move r _ l ⇒
    252     if list_set_member register (eq_identifier ?) r pliveafter ∨
    253        list_set_member Register eq_Register RegisterCarry hliveafter then
    254       None ?
    255     else
    256       Some ? l
    257   | ertl_st_opaccs _ d1 d2 _ _ l ⇒
    258     if list_set_member register (eq_identifier ?) d1 pliveafter ∨
    259        list_set_member register (eq_identifier ?) d2 pliveafter ∨
    260        list_set_member Register eq_Register RegisterCarry hliveafter then
    261       None ?
    262     else
    263       Some ? l
    264   | ertl_st_op1 _ r _ l ⇒
    265     if list_set_member register (eq_identifier ?) r pliveafter ∨
    266        list_set_member Register eq_Register RegisterCarry hliveafter then
    267       None ?
    268     else
    269       Some ? l
    270   | ertl_st_op2 _ r _ _ l ⇒
    271     if list_set_member register (eq_identifier ?) r pliveafter ∨
    272        list_set_member Register eq_Register RegisterCarry hliveafter then
    273       None ?
    274     else
    275       Some ? l
    276   | ertl_st_load r _ _ l ⇒
    277     if list_set_member register (eq_identifier ?) r pliveafter ∨
    278        list_set_member Register eq_Register RegisterCarry hliveafter then
    279       None ?
    280     else
    281       Some ? l
    282   | ertl_st_set_hdw r _ l ⇒
    283     if list_set_member Register eq_Register r hliveafter then
    284       None ?
    285     else
    286       Some ? l
    287   | ertl_st_hdw_to_hdw r _ l ⇒
    288     if list_set_member Register eq_Register r hliveafter then
    289       None ?
    290     else
    291       Some ? l
    292   ].
    293 
    294 definition statement_semantics: ertl_statement → register_lattice → register_lattice ≝
     222  match s with
     223  [ joint_st_sequential seq l ⇒
     224    match seq with
     225    [ joint_instr_op2 op2 acc_a r ⇒
     226      if list_set_member register (eq_identifier ?) acc_a pliveafter ∨
     227         list_set_member Register eq_Register RegisterCarry hliveafter then
     228        None ?
     229      else
     230        Some ? l
     231    | joint_instr_clear_carry ⇒ None ?
     232    | joint_instr_set_carry ⇒ None ?
     233    | joint_instr_opaccs opaccs r1 r2 ⇒
     234      if list_set_member register (eq_identifier ?) r1 pliveafter ∨
     235         list_set_member register (eq_identifier ?) r2 pliveafter ∨
     236         list_set_member Register eq_Register RegisterCarry hliveafter then
     237        None ?
     238      else
     239        Some ? l
     240    | joint_instr_op1 op1 r ⇒
     241      if list_set_member register (eq_identifier ?) r pliveafter ∨
     242         list_set_member Register eq_Register RegisterCarry hliveafter then
     243        None ?
     244      else
     245        Some ? l
     246    | joint_instr_pop r ⇒ None ?
     247    | joint_instr_int r _ ⇒
     248      if list_set_member register (eq_identifier ?) r pliveafter ∨
     249         list_set_member Register eq_Register RegisterCarry hliveafter then
     250        None ?
     251      else
     252        Some ? l
     253    | joint_instr_address _ _ r1 r2 ⇒
     254      if list_set_member register (eq_identifier ?) r1 pliveafter ∨
     255         list_set_member register (eq_identifier ?) r2 pliveafter ∨
     256         list_set_member Register eq_Register RegisterCarry hliveafter then
     257        None ?
     258      else
     259        Some ? l
     260    | joint_instr_load acc_a dpl dph ⇒
     261      if list_set_member register (eq_identifier ?) acc_a pliveafter ∨
     262         list_set_member Register eq_Register RegisterCarry hliveafter then
     263        None ?
     264      else
     265        Some ? l
     266    | joint_instr_call_id _ nparams ⇒ None ?
     267    | joint_instr_comment c ⇒ None ?
     268    | joint_instr_cond r lbl_true ⇒ None ?
     269    | joint_instr_store acc_a dpl dph ⇒ None ?
     270    | joint_instr_cost_label clabel ⇒ None ?
     271    | joint_instr_push r ⇒ None ?
     272    | joint_instr_move pair_reg ⇒
     273      let r1 ≝ \fst pair_reg in
     274      let r2 ≝ \snd pair_reg in
     275      match r1 with
     276      [ pseudo p1 ⇒
     277        if list_set_member register (eq_identifier ?) p1 pliveafter ∨
     278           list_set_member Register eq_Register RegisterCarry hliveafter then
     279          None ?
     280        else
     281          Some ? l
     282      | hardware h1 ⇒
     283        if list_set_member Register eq_Register h1 hliveafter then
     284          None ?
     285        else
     286          Some ? l
     287      ]
     288    ]
     289  | joint_st_goto l ⇒ None ?
     290  | joint_st_return ⇒ None ?
     291  | joint_st_extension ext ⇒
     292    match ext with
     293    [ ertl_st_ext_new_frame l ⇒ None ?
     294    | ertl_st_ext_del_frame l ⇒ None ?
     295    | ertl_st_ext_frame_size r l ⇒
     296      if list_set_member register (eq_identifier ?) r pliveafter ∨
     297        list_set_member Register eq_Register RegisterCarry hliveafter then
     298        None ?
     299      else
     300        Some ? l
     301    ]
     302  ].
     303
     304definition statement_semantics: ∀globals: list ident. ertl_statement globals → register_lattice → register_lattice ≝
     305  λglobals.
    295306  λstmt.
    296307  λliveafter.
    297   match eliminable liveafter stmt with
    298   [ None ⇒ lattice_join (lattice_diff liveafter (defined stmt)) (used stmt)
     308  match eliminable globals liveafter stmt with
     309  [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt)
    299310  | Some l ⇒ liveafter
    300311  ].
    … …  
    307318
    308319definition livebefore ≝
     320  λglobals: list ident.
    309321  λint_fun.
    310322  λlabel.
    311323  λliveafter: valuation.
    312   match lookup ? ? (ertl_if_graph int_fun) label with
     324  match lookup ? ? (ertl_if_graph globals int_fun) label with
    313325  [ None      ⇒ ?
    314   | Some stmt ⇒ statement_semantics stmt (liveafter label)
     326  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
    315327  ].
    316328  cases not_implemented (* XXX *)
    … …  
    318330
    319331definition liveafter ≝
     332  λglobals.
    320333  λint_fun.
    321334  λlivebefore.
    322335  λlabel.
    323336  λliveafter: valuation.
    324   match lookup ? ? (ertl_if_graph int_fun) label with
     337  match lookup … (ertl_if_graph globals int_fun) label with
    325338  [ None      ⇒ ?
    326   | Some stmt ⇒ list_set_fold ? ? (λsuccessor. λaccu.
     339  | Some stmt ⇒ list_set_fold … (λsuccessor. λaccu: register_lattice.
    327340      lattice_join (livebefore successor liveafter) accu)
    328       lattice_bottom (statement_successors stmt)
     341      lattice_bottom (statement_successors globals stmt)
    329342  ].
    330343  cases not_implemented (* XXX *)
    331344qed.
    332345
    333 definition analyse: ertl_internal_function → valuation ≝
     346definition analyse ≝
     347  λglobals.
    334348  λint_fun.
    335     fix_lfp (liveafter int_fun (livebefore int_fun)).
     349    fix_lfp (liveafter globals int_fun (livebefore globals int_fun)).

  • Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma

    r1153 r1197  
    2121(* CSC: ???????????? *)
    2222axiom smerge: val → val → res val.
    23 (*
    2423(* CSC: ???????????? In OCaml: IntValue.Int32.merge
    2524   Note also that the translation can fail; so it should be a res int! *)
    2625axiom smerge2: list val → int.
    27 *)
    2826(* CSC: I have a byte, I need a value, but it is complex to do so *)
    2927axiom val_of_Byte: Byte → val.
    3028axiom Byte_of_val: val → res Byte.
     29axiom val_of_nat: nat → val.
    3130(* Map from the front-end memory model to the back-end memory model *)
    3231axiom represent_block: block → val × val.
    … …  
    3837axiom val_of_address: address → val. (* CSC: only to shift the sp *)
    3938axiom address_of_val: val → address. (* CSC: only to shift the sp *)
     39axiom addr_sub: address → nat → address.
     40axiom addr_add: address → nat → address.
    4041(* CSC: ??? *)
    4142axiom address_of_label: mem → label → address.
    … …  
    4344axiom label_of_address_chunks: Byte → Byte → label.
    4445axiom address_of_address_chunks: Byte → Byte → address.
     46axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
    4547axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
    4648axiom hwreg_retrieve : mRegisterMap → Register → res val.
    4749axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
    4850
    49 definition genv ≝ (genv_t Genv) (fundef ertl_internal_function).
     51definition genv ≝ λglobals. (genv_t Genv) (fundef (ertl_internal_function globals)).
    5052
    5153(* CSC: frame reduced to this *)
    5254definition frame: Type[0] ≝ register_env val.
    5355
     56(* CSC: exit not put in the state, like in OCaml. It is constant througout
     57   execution *)
    5458record state : Type[0] ≝
    5559 { st_frms: list frame
    5660 ; pc: address
    5761 ; sp: address
    58 (* ; exit: address *)
    5962 ; locals: register_env val
    6063 ; carry: val
    … …  
    134137
    135138(*CSC: To be implemented *)
    136 axiom fetch_statement: state → res ertl_statement.
     139
     140axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals).
     141axiom fetch_function: ∀globals: list ident. state → res (ertl_internal_function globals).
    137142
    138143definition init_locals : list register → register_env val ≝
    … …  
    142147λreg,v,locals. update RegisterTag val locals reg v.
    143148
    144 (*
    145 axiom WrongNumberOfParameters : String.
    146 
    147 (* CSC: modified to take in input a list of registers (untyped) *)
    148 let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    149 match rs with
    150 [ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
    151 | cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
    152   let locals' ≝ add RegisterTag val locals r v in
    153   params_store rst vst locals'
    154 ] ].
    155 *)
    156 
    157149axiom BadRegister : String.
    158150
    … …  
    160152λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
    161153
    162 (*
    163 axiom FailedOp : String.
    164 *)
    165154axiom MissingSymbol : String.
    166 (*
    167 axiom MissingStatement : String.
    168 axiom FailedConstant : String. *)
    169155axiom FailedLoad : String.
    170156axiom BadFunction : String.
    171 (*axiom BadJumpTable : String.
    172 axiom BadJumpValue : String.
    173 axiom FinalState : String.
    174 axiom ReturnMismatch : String.
    175 *)
    176157
    177158(*CSC: to be implemented *)
    … …  
    200181  (λregs.OK ? (set_regs regs st)).
    201182
    202 definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
    203 λge,st.
    204   ! s ← fetch_statement st;
     183definition fetch_result: state → nat → res (list val) ≝
     184 λst,registersno.
     185  let retregs ≝ prefix … registersno RegisterRets in
     186  mmap … (λr. hwreg_retrieve (regs st) r) retregs.
     187
     188definition framesize: list ident → state → res nat ≝
     189  λglobals: list ident.
     190  λst.
     191  (* CSC: monadic notation missing here *)
     192    bind ?? (fetch_function globals st) (λf.
     193    OK ? (ertl_if_stacksize globals f)).
     194
     195definition get_hwsp : state → res address ≝
     196 λst.
     197  (* CSC: monadic notation missing here *)
     198  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl.
     199  (* CSC: monadic notation missing here *)
     200  bind ?? (Byte_of_val spl) (λspl.
     201  (* CSC: monadic notation missing here *)
     202  bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph.
     203  (* CSC: monadic notation missing here *)
     204  bind ?? (Byte_of_val sph) (λsph.
     205  OK ? (address_of_address_chunks spl sph))))).
     206
     207definition set_hwsp : address → state → res state ≝
     208 λsp,st.
     209  let 〈spl,sph〉 ≝ address_chunks_of_address sp in
     210  (* CSC: monadic notation missing here *) 
     211  bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs.
     212  (* CSC: monadic notation missing here *) 
     213  bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
     214  OK ? (set_regs regs st))).
     215
     216definition retrieve: state → move_registers → res val ≝
     217  λst.
     218  λr.
     219  match r with
     220  [ pseudo   src ⇒ reg_retrieve (locals st) src
     221  | hardware src ⇒ hwreg_retrieve (regs st) src
     222  ].
     223
     224definition store ≝
     225  λst.
     226  λv.
     227  λr.
     228  match r with
     229  [ pseudo   dst ⇒
     230    ! locals ← reg_store dst v (locals st);
     231      ret ? (set_locals locals st)
     232  | hardware dst ⇒
     233    ! regs ← hwreg_store dst v (regs st);
     234      ret ? (set_regs regs st)
     235  ].
     236
     237definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝
     238  λglobals. λge,st.
     239  ! s ← fetch_statement globals st;
    205240  match s with
    206   [ ertl_st_skip l ⇒ ret ? 〈E0, goto l st〉
    207   | ertl_st_cost cl l ⇒ ret ? 〈Echarge cl, goto l st〉
    208   | ertl_st_int dest v l ⇒
    209      ! locals ← reg_store dest (val_of_Byte v) (locals st);
    210      ret ? 〈E0, goto l (set_locals locals st)〉
    211   | ertl_st_load addrl addrh dst l ⇒
    212       ! vaddrh ← reg_retrieve (locals st) addrh;
    213       ! vaddrl ← reg_retrieve (locals st) addrl;
    214       ! vaddr ← smerge vaddrl vaddrh;
    215       ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
    216       ! locals ← reg_store dst v (locals st);
     241  [ ertl_st_lift_pre pre ⇒
     242    match pre with
     243    [ joint_st_goto l ⇒ ret ? 〈E0, goto l st〉
     244    | joint_st_sequential seq l ⇒
     245      match seq with
     246      [ joint_instr_cost_label cl ⇒ ret ? 〈Echarge cl, goto l st〉
     247      | joint_instr_comment c ⇒ ret ? 〈E0, goto l st〉
     248      | joint_instr_int dest v ⇒
     249        ! locals ← reg_store dest (val_of_Byte v) (locals st);
     250          ret ? 〈E0, goto l (set_locals locals st)〉
     251      | joint_instr_load addrl addrh dst ⇒
     252        ! vaddrh ← reg_retrieve (locals st) addrh;
     253        ! vaddrl ← reg_retrieve (locals st) addrl;
     254        ! vaddr ← smerge vaddrl vaddrh;
     255        ! v ← opt_to_res … (msg FailedLoad) (loadv chunk (m st) vaddr);
     256        ! locals ← reg_store dst v (locals st);
     257          ret ? 〈E0, goto l (set_locals locals st)〉
     258      | joint_instr_store addrl addrh src ⇒
     259        ! vaddrh ← reg_retrieve (locals st) addrh;
     260        ! vaddrl ← reg_retrieve (locals st) addrl;
     261        ! vaddr ← smerge vaddrl vaddrh;
     262        ! v ← reg_retrieve (locals st) src;
     263        ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
     264          ret ? 〈E0, goto l (set_m m' st)〉
     265      | joint_instr_cond src ltrue ⇒
     266        ! v ← reg_retrieve (locals st) src;
     267        ! b ← eval_bool_of_val v;
     268          ret ? 〈E0, goto (if b then ltrue else l) st〉
     269      | joint_instr_address ident prf ldest hdest ⇒
     270        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
     271          let 〈laddr,haddr〉 ≝ represent_block addr in
     272        ! locals ← reg_store ldest laddr (locals st);
     273        ! locals ← reg_store hdest haddr locals;
     274          ret ? 〈E0, goto l (set_locals locals st)〉
     275      | joint_instr_op1 op acc_a ⇒
     276        ! v ← reg_retrieve (locals st) acc_a;
     277        ! v ← Byte_of_val v;
     278          let v' ≝ val_of_Byte (op1 eval op v) in
     279        ! locals ← reg_store acc_a v' (locals st);
     280          ret ? 〈E0, goto l (set_locals locals st)〉
     281      | joint_instr_op2 op acc_a_reg dest ⇒
     282        ! v1 ← reg_retrieve (locals st) acc_a_reg;
     283        ! v1 ← Byte_of_val v1;
     284        ! v2 ← reg_retrieve (locals st) acc_a_reg;
     285        ! v2 ← Byte_of_val v2;
     286        ! carry ← eval_bool_of_val (carry st);
     287          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
     288          let v' ≝ val_of_Byte v' in
     289          let carry ≝ of_bool carry in
     290        ! locals ← reg_store dest v' (locals st);
     291          ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
     292      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
     293      | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
     294      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
     295        ! v1 ← reg_retrieve (locals st) acc_a_reg;
     296        ! v1 ← Byte_of_val v1;
     297        ! v2 ← reg_retrieve (locals st) acc_b_reg;
     298        ! v2 ← Byte_of_val v2;
     299          let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
     300          let v1' ≝ val_of_Byte v1' in
     301          let v2' ≝ val_of_Byte v2' in
     302        ! locals ← reg_store acc_a_reg v1' (locals st);
     303        ! locals ← reg_store acc_b_reg v2' locals;
     304          ret ? 〈E0, goto l (set_locals locals st)〉
     305      | joint_instr_pop dst ⇒
     306        ! 〈st,v〉 ← pop st;
     307        ! locals ← reg_store dst (val_of_Byte v) (locals st);
     308          ret ? 〈E0, goto l (set_locals locals st)〉
     309      | joint_instr_push src ⇒
     310        ! v ← reg_retrieve (locals st) src;
     311        ! v ← Byte_of_val v;
     312        ! st ← push st v;
     313          ret ? 〈E0, goto l st〉
     314      | joint_instr_move dst_src ⇒
     315        let 〈dst, src〉 ≝ dst_src in
     316        ! v ← retrieve st src;
     317        ! st ← store st v dst;
     318          ret ? 〈E0, goto l st〉
     319      (* CSC: changed, where the meat is *)
     320      | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
     321        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     322        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
     323          match fd with
     324          [ Internal fn ⇒
     325            ! st ← save_ra st l;
     326              let st ≝ save_frame st in
     327              let locals ≝ init_locals (ertl_if_locals globals fn) in
     328              let l' ≝ ertl_if_entry globals fn in
     329              ret ? 〈 E0, goto l' (set_locals locals st)〉
     330          | External fn ⇒
     331            ! params ← fetch_external_args fn st;
     332            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
     333            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     334            (* CSC: XXX bug here; I think I should split it into Byte-long
     335               components; instead I am making a singleton out of it *)
     336              let vs ≝ [mk_val ? evres] in
     337            ! st ← set_result vs st;
     338              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
     339          ]
     340      ]
     341    (* CSC: changed, where the meat is *)
     342    | joint_st_return ⇒
     343      ! st ← pop_frame st;
     344      ! 〈st,pch〉 ← pop st;
     345      ! 〈st,pcl〉 ← pop st;
     346        let pc ≝ address_of_address_chunks pcl pch in
     347        ret ? 〈E0,set_pc pc st〉
     348    | _ ⇒ ?
     349    ]
     350  | ertl_st_new_frame l ⇒
     351    ! v ← framesize globals st;
     352    ! sp ← get_hwsp st;
     353      let newsp ≝ addr_sub sp v in
     354    ! st ← set_hwsp newsp st;
     355      ret ? 〈E0,goto l st〉
     356  | ertl_st_del_frame l ⇒
     357    ! v ← framesize globals st;
     358    ! sp ← get_hwsp st;
     359      let newsp ≝ addr_add sp v in
     360    ! st ← set_hwsp newsp st;
     361      ret ? 〈E0,goto l st〉
     362  | ertl_st_frame_size dst l ⇒
     363    ! v ← framesize globals st;
     364    ! locals ← reg_store dst (val_of_nat v) (locals st);
    217365      ret ? 〈E0, goto l (set_locals locals st)〉
    218   | ertl_st_store addrl addrh src l ⇒
    219       ! vaddrh ← reg_retrieve (locals st) addrh;
    220       ! vaddrl ← reg_retrieve (locals st) addrl;
    221       ! vaddr ← smerge vaddrl vaddrh;
    222       ! v ← reg_retrieve (locals st) src;
    223       ! m' ← opt_to_res … (msg FailedStore) (storev chunk (m st) vaddr v);
    224       ret ? 〈E0, goto l (set_m m' st)〉
    225   | ertl_st_cond src ltrue lfalse ⇒
    226       ! v ← reg_retrieve (locals st) src;
    227       ! b ← eval_bool_of_val v;
    228       ret ? 〈E0, goto (if b then ltrue else lfalse) st〉
    229   | ertl_st_addr ldest hdest id l ⇒
    230      ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
    231      let 〈laddr,haddr〉 ≝ represent_block addr in
    232      ! locals ← reg_store ldest laddr (locals st);
    233      ! locals ← reg_store hdest haddr locals;
    234      ret ? 〈E0, goto l (set_locals locals st)〉
    235   | ertl_st_op1 op dst src l ⇒
    236      ! v ← reg_retrieve (locals st) src;
    237      ! v ← Byte_of_val v;
    238      let v' ≝ val_of_Byte (op1 eval op v) in
    239      ! locals ← reg_store dst v' (locals st);
    240      ret ? 〈E0, goto l (set_locals locals st)〉
    241   | ertl_st_op2 op dst src1 src2 l ⇒
    242      ! v1 ← reg_retrieve (locals st) src1;
    243      ! v1 ← Byte_of_val v1;
    244      ! v2 ← reg_retrieve (locals st) src2;
    245      ! v2 ← Byte_of_val v2;
    246      ! carry ← eval_bool_of_val (carry st);
    247      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
    248      let v' ≝ val_of_Byte v' in
    249      let carry ≝ of_bool carry in
    250      ! locals ← reg_store dst v' (locals st);
    251      ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
    252   | ertl_st_opaccs op dacc dbacc sacc sbacc l ⇒
    253      ! v1 ← reg_retrieve (locals st) sacc;
    254      ! v1 ← Byte_of_val v1;
    255      ! v2 ← reg_retrieve (locals st) sbacc;
    256      ! v2 ← Byte_of_val v2;
    257      let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
    258      let v1' ≝ val_of_Byte v1' in
    259      let v2' ≝ val_of_Byte v2' in
    260      ! locals ← reg_store dacc v1' (locals st);
    261      ! locals ← reg_store dbacc v2' locals;
    262      ret ? 〈E0, goto l (set_locals locals st)〉
    263   | ertl_st_clear_carry l ⇒
    264     ret ? 〈E0, goto l (set_carry Vfalse st)〉
    265   | ertl_st_set_carry l ⇒
    266     ret ? 〈E0, goto l (set_carry Vtrue st)〉
    267      
    268   (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
    269          ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would
    270          be more than enough... *)
    271   | ertl_st_move dst src l ⇒
    272      ! v ← reg_retrieve (locals st) src;
    273      ! locals ← reg_store dst v (locals st);
    274      ret ? 〈E0, goto l (set_locals locals st)〉
    275   | ertl_st_hdw_to_hdw dst src l ⇒
    276      ! v ← hwreg_retrieve (regs st) src;
    277      ! regs ← hwreg_store dst v (regs st);
    278      ret ? 〈E0, goto l (set_regs regs st)〉
    279   | ertl_st_get_hdw dst src l ⇒
    280      ! v ← hwreg_retrieve (regs st) src;
    281      ! locals ← reg_store dst v (locals st);
    282      ret ? 〈E0, goto l (set_locals locals st)〉
    283   | ertl_st_set_hdw dst src l ⇒
    284      ! v ← reg_retrieve (locals st) src;
    285      ! regs ← hwreg_store dst v (regs st);
    286      ret ? 〈E0, goto l (set_regs regs st)〉
    287 
    288366  (* CSC: Dropped:
    289367      - rtl_st_stackaddr (becomes two get_hdw)
    290368      - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM)
    291369      - rtl_st_call_ptr (unimplemented ATM) *)
     370  ].
    292371     
    293   (* CSC: changed, where the meat is *)
    294   | ertl_st_call_id id argsno l ⇒ (* CSC: only the number of args kept, no return reg *)
    295       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    296       ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    297       match fd with
    298       [ Internal fn ⇒
    299         ! st ← save_ra st l;
    300         let st ≝ save_frame st in
    301         let locals ≝ init_locals (ertl_if_locals fn) in
    302         let l' ≝ ertl_if_entry fn in
    303          ret ? 〈 E0, goto l' (set_locals locals st)〉
    304       | External fn ⇒
    305         ! params ← fetch_external_args fn st;
    306         ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    307         ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    308         (* CSC: XXX bug here; I think I should split it into Byte-long
    309            components; instead I am making a singleton out of it *)
    310         let vs ≝ [mk_val ? evres] in
    311         ! st ← set_result vs st;
    312         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
     372axiom WrongReturnValueType: String.
     373
     374definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝
     375  λglobals: list ident.
     376  λexit.
     377  λregistersno.
     378  λst.
     379 (* CSC: monadic notation missing here *)
     380  match fetch_statement globals st with
     381  [ Error _ ⇒ None ?
     382  | OK s ⇒
     383    match s with
     384    [ ertl_st_lift_pre pre ⇒
     385      match pre with
     386      [ joint_st_return ⇒
     387        match fetch_ra st with
     388         [ Error _ ⇒ None ?
     389         | OK st_l ⇒
     390           let 〈st,l〉 ≝ st_l in
     391           match label_eq l exit with
     392           [ inl _ ⇒
     393             (* CSC: monadic notation missing here *)
     394             match fetch_result st registersno with
     395             [ Error _ ⇒ None ?
     396             | OK vals ⇒ Some ? (smerge2 vals)
     397             ]
     398           | inr _ ⇒ None ?
     399           ]
     400         ]
     401      | _ ⇒ None ?
    313402      ]
    314   | ertl_st_return ⇒
    315       ! st ← pop_frame st;
    316       ! 〈st,pch〉 ← pop st;
    317       ! 〈st,pcl〉 ← pop st;
    318       let pc ≝ address_of_address_chunks pcl pch in
    319       ret ? 〈E0,set_pc pc st〉
    320  
    321   (* CSC: new stuff *)
    322   | ertl_st_comment _ l ⇒ ret ? 〈E0, goto l st〉
    323   | ertl_st_new_frame _ ⇒ ?
    324   | ertl_st_del_frame _ ⇒ ?
    325   | ertl_st_frame_size _ _ ⇒ ?
    326   | ertl_st_pop dst l ⇒
    327      ! 〈st,v〉 ← pop st;
    328      ! locals ← reg_store dst (val_of_Byte v) (locals st);
    329      ret ? 〈E0, goto l (set_locals locals st)〉
    330   | ertl_st_push src l ⇒
    331      ! v ← reg_retrieve (locals st) src;
    332      ! v ← Byte_of_val v;
    333      ! st ← push st v;
    334      ret ? 〈E0, goto l st〉
     403    | _ ⇒ None ?
     404    ]
    335405  ].
    336406
    337 axiom WrongReturnValueType: String.
    338 
    339 definition is_final : state → option ((*CSC: why not res*) int) ≝
    340 λs. match s with
    341 [ State _ _ _ ⇒ None ?
    342 | Callstate _ _ _ _ _ ⇒ None ?
    343 | Returnstate v _ fs _ ⇒
    344     match fs with
    345      [ nil ⇒ Some ? (smerge2 v)
    346      | _ ⇒ None ? ]].
    347 
    348 definition RTL_exec : execstep io_out io_in ≝
    349   mk_execstep … ? is_final mem_of_state eval_statement.
     407definition ERTL_exec: list ident → label → nat → execstep io_out io_in ≝
     408  λglobals.
     409  λexit.
     410  λregistersno.
     411  mk_execstep ? ? ? ? (is_final globals exit registersno) m (eval_statement globals).
    350412
    351413(* CSC: XXX the program type does not fit with the globalenv and init_mem

  • Deliverables/D3.3/id-lookup-branch/ERTL/uses.ma

    r1153 r1197  
    1818  λr.
    1919    assoc_list_find register nat (eq_identifier ?) uses 0 r.
    20 
    21 definition count ≝
    22   λr.
    23   λuses.
    24     (r,
    25 
    26 let count r uses = Register.Map.add r (lookup uses r + 1) uses
Note: See TracChangeset for help on using the changeset viewer.