Changeset 3014 for src/ERTL


Ignore:
Timestamp:
Mar 28, 2013, 4:58:26 PM (8 years ago)
Author:
tranquil
Message:

ERTL to ERTLptr pass suppressed (it introduced a bug in the later ERTLptr to LTL), and integrated in a single ERTToLTL pass like before

Location:
src/ERTL
Files:
5 moved

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r3012 r3014  
    11include "LTL/LTL.ma".
    2 include "ERTLptr/Interference.ma".
     2include "ERTL/Interference.ma".
    33include "ASM/Arithmetic.ma".
    44include "joint/TranslateUtils.ma".
     
    299299     move ? localss false addr2 RegisterDPH).
    300300
    301 definition translate_low_address :
    302   ∀globals.nat → bool → decision → label →
    303   list (joint_seq LTL globals) ≝
    304   λglobals,localss,carry_lives_after,dst,lbl.
    305   match dst return λ_.list (joint_seq LTL globals) with
    306   [ decision_colour r ⇒ [LOW_ADDRESS r lbl]
    307   | _ ⇒
    308     LOW_ADDRESS RegisterA lbl :: move ? localss carry_lives_after dst RegisterA
    309   ].
    310 
    311 definition translate_high_address :
    312   ∀globals.nat → bool → decision → label →
    313   list (joint_seq LTL globals) ≝
    314   λglobals,localss,carry_lives_after,dst,lbl.
    315   match dst return λ_.list (joint_seq LTL globals) with
    316   [ decision_colour r ⇒ [HIGH_ADDRESS r lbl]
    317   | _ ⇒
    318     HIGH_ADDRESS RegisterA lbl :: move ? localss carry_lives_after dst RegisterA
    319   ].
    320 
    321301definition translate_step:
    322302  ∀globals,fn.nat → ∀after : valuation register_lattice.
    323303  coloured_graph (livebefore globals fn after) →
    324   ℕ → label → joint_step ERTLptr globals → bind_step_block LTL globals ≝
     304  ℕ → label → joint_step ERTL globals → bind_step_block LTL globals ≝
    325305  λglobals,fn,localss,after,grph,stack_sz,lbl,s.
    326306  bret … (
     
    385365    | extension_seq ext ⇒
    386366      match ext with
    387         [ ertlptr_ertl ext' ⇒
    388           match ext' with
    389           [ ertl_new_frame ⇒ newframe ? stack_sz
    390           | ertl_del_frame ⇒ delframe ? stack_sz
    391           | ertl_frame_size r ⇒
    392             move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    393           ]
    394         | LOW_ADDRESS r1 l ⇒
    395            translate_low_address ? localss carry_lives_after (lookup r1) l
    396         | HIGH_ADDRESS r1 l ⇒
    397            translate_high_address ? localss carry_lives_after (lookup r1) l       
    398         ]
     367      [ ertl_new_frame ⇒ newframe ? stack_sz
     368      | ertl_del_frame ⇒ delframe ? stack_sz
     369      | ertl_frame_size r ⇒
     370        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
     371      ]
    399372    ]
    400373  | COST_LABEL cost_lbl ⇒ 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉
     
    407380      | inr dp ⇒
    408381        let 〈dpl, dph〉 ≝ dp in
    409         〈add_dummy_variance … (move_to_dp ? localss (lookup_arg dpl) (lookup_arg dph)),
     382        〈add_dummy_variance … (move_to_dp ? localss (lookup_arg dpl) (lookup_arg dph)) @
     383         [λl.(LOW_ADDRESS l : joint_seq ??);
     384          λ_.PUSH LTL ? it;
     385          λl.HIGH_ADDRESS l;
     386          λ_.PUSH LTL ? it],
    410387         λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉
    411388      ]
     
    413390
    414391definition translate_fin_step:
    415   ∀globals.label → joint_fin_step ERTLptr → bind_fin_block LTL globals ≝
     392  ∀globals.label → joint_fin_step ERTL → bind_fin_block LTL globals ≝
    416393  λglobals,lbl,s.
    417394  bret … (〈[ ],
     
    425402 fixpoint_computer → coloured_graph_computer →
    426403 ∀globals.
    427   joint_closed_internal_function ERTLptr globals →
    428   bind_new register (b_graph_translate_data ERTLptr LTL globals) ≝
     404  joint_closed_internal_function ERTL globals →
     405  bind_new register (b_graph_translate_data ERTL LTL globals) ≝
    429406λthe_fixpoint,build,globals,int_fun.
    430407(* colour registers *)
     
    434411let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
    435412bret …
    436   (mk_b_graph_translate_data ERTLptr LTL globals
     413  (mk_b_graph_translate_data ERTL LTL globals
    437414    (* init_ret ≝ *) it
    438415    (* init_params ≝ *) it
     
    452429   when it is an info easily available from any program in the back end?
    453430   Also, is it really 2^16 - |globals|, or should there also be a -1? *)
    454 definition ertlptr_to_ltl:
    455  fixpoint_computer → coloured_graph_computer → ertlptr_program →
     431definition ertl_to_ltl:
     432 fixpoint_computer → coloured_graph_computer → ertl_program →
    456433  ltl_program × stack_cost_model × nat ≝
    457434  λthe_fixpoint,build,pr.
  • src/ERTL/ERTLToLTLAxiom.ma

    r3012 r3014  
    1 include "ERTLptr/ERTLptrToLTL.ma".
    2 include "ERTLptr/ERTLptr_semantics.ma".
     1include "ERTL/ERTLToLTL.ma".
     2include "ERTL/ERTL_semantics.ma".
    33include "LTL/LTL_semantics.ma".
    44include "joint/Traces.ma".
     
    1111  assoc_list_lookup ? ℕ id (eq_identifier …) p.
    1212
    13 axiom ERTLptrToLTL_ok :
     13axiom ERTLToLTL_ok :
    1414∀fix_comp : fixpoint_computer.
    1515∀colour : coloured_graph_computer.
    16 ∀p_in : ertlptr_program.
    17 let 〈p_out, m, n〉 ≝ ertlptr_to_ltl fix_comp colour p_in in
     16∀p_in : ertl_program.
     17let 〈p_out, m, n〉 ≝ ertl_to_ltl fix_comp colour p_in in
    1818(* what should we do with n? *)
    1919let stacksizes ≝ lookup_stack_cost m in
    2020∃[1] R.
    2121  status_simulation
    22     (joint_status ERTLptr_semantics p_in stacksizes)
     22    (joint_status ERTL_semantics p_in stacksizes)
    2323    (joint_status LTL_semantics p_out stacksizes)
    2424    R ∧
    2525  ∀init_in.make_initial_state
    26     (mk_prog_params ERTLptr_semantics p_in stacksizes) = OK … init_in →
     26    (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in →
    2727  ∃init_out.
    2828    make_initial_state
  • src/ERTL/Interference.ma

    r3012 r3014  
    1 include "ERTLptr/liveness.ma".
     1include "ERTL/liveness.ma".
    22
    33inductive decision: Type[0] ≝
     
    1919definition coloured_graph_computer ≝
    2020 ∀globals.
    21   ∀fn:joint_internal_function ERTLptr globals.
     21  ∀fn:joint_internal_function ERTL globals.
    2222   ∀liveafter.
    2323    coloured_graph (livebefore globals fn liveafter).
  • src/ERTL/liveness.ma

    r3012 r3014  
    11include "ASM/Util.ma".
    2 include "ERTLptr/ERTLptr.ma".
     2include "ERTL/ERTL.ma".
    33include "utilities/adt/set_adt.ma".
    44include "utilities/fixpoints.ma".
     
    4040definition defined ≝
    4141  λglobals: list ident.
    42   λs: joint_statement ERTLptr globals.
     42  λs: joint_statement ERTL globals.
    4343  match s with
    4444  [ sequential seq l ⇒
     
    7474      | extension_seq ext ⇒
    7575        match ext with
    76         [ ertlptr_ertl ext' ⇒
    77            match ext' with
    78            [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    79            | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    80            | ertl_frame_size r ⇒ rl_psingleton r
    81            ]
    82         | LOW_ADDRESS r1 l ⇒ rl_psingleton r1
    83         | HIGH_ADDRESS r1 l ⇒ rl_psingleton r1
    84         ]
     76         [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     77         | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     78         | ertl_frame_size r ⇒ rl_psingleton r
     79         ]
    8580      (* Potentially destroys all caller-save hardware registers. *)
    8681      ]
     
    10398definition used ≝
    10499  λglobals: list ident.
    105   λs: joint_statement ERTLptr globals.
     100  λs: joint_statement ERTL globals.
    106101  match s with
    107102  [ sequential seq l ⇒
     
    136131      | extension_seq ext ⇒
    137132        match ext with
    138         [ ertlptr_ertl ext' ⇒
    139            match ext' with
    140            [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    141            | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    142            | ertl_frame_size r ⇒ rl_bottom ]
    143         | LOW_ADDRESS r1 l ⇒ rl_bottom
    144         | HIGH_ADDRESS r1 l ⇒ rl_bottom
    145         ]       
     133         [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     134         | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     135         | ertl_frame_size r ⇒ rl_bottom ]
    146136      (* Reads the hardware registers that are used to pass parameters. *)
    147137      | _ ⇒ rl_bottom
     
    167157λglobals: list ident.
    168158λl: register_lattice.
    169 λs: joint_step ERTLptr globals.
     159λs: joint_step ERTL globals.
    170160let pliveafter ≝ \fst l in
    171161let hliveafter ≝ \snd l in
     
    200190  | extension_seq ext ⇒
    201191    match ext with
    202     [ ertlptr_ertl ext' ⇒
    203        match ext' with
    204        [ ertl_new_frame ⇒ false
    205        | ertl_del_frame ⇒ false
    206        | ertl_frame_size r ⇒
    207          ¬set_member ? (eq_identifier RegisterTag) r pliveafter
    208        ]
    209     | LOW_ADDRESS r1 l' ⇒
    210        ¬set_member ? (eq_identifier RegisterTag) r1 pliveafter
    211     | HIGH_ADDRESS r1 l' ⇒
    212        ¬set_member ? (eq_identifier RegisterTag) r1 pliveafter
    213     ]       
     192     [ ertl_new_frame ⇒ false
     193     | ertl_del_frame ⇒ false
     194     | ertl_frame_size r ⇒
     195       ¬set_member ? (eq_identifier RegisterTag) r pliveafter
     196     ]
    214197  | _ ⇒ false
    215198  ]
     
    220203  λglobals: list ident.
    221204  λl: register_lattice.
    222   λs: joint_statement ERTLptr globals.
     205  λs: joint_statement ERTL globals.
    223206  let pliveafter ≝ \fst l in
    224207  let hliveafter ≝ \snd l in
     
    229212
    230213definition statement_semantics: ∀globals: list ident.
    231   joint_statement ERTLptr globals → register_lattice → register_lattice ≝
     214  joint_statement ERTL globals → register_lattice → register_lattice ≝
    232215  λglobals.
    233216  λstmt.
     
    240223definition livebefore:
    241224  ∀globals: list ident.
    242    joint_internal_function ERTLptr globals →
     225   joint_internal_function ERTL globals →
    243226     valuation register_lattice → valuation register_lattice
    244227
    245228  λglobals: list ident.
    246   λint_fun: joint_internal_function ERTLptr globals.
     229  λint_fun: joint_internal_function ERTL globals.
    247230  λliveafter: valuation register_lattice.
    248231  λlabel.
     
    254237definition liveafter ≝
    255238   λglobals: list ident.
    256   λint_fun: joint_internal_function ERTLptr globals.
     239  λint_fun: joint_internal_function ERTL globals.
    257240  λlabel.
    258241  λliveafter: valuation register_lattice.
  • src/ERTL/uses.ma

    r3012 r3014  
    1313(**************************************************************************)
    1414
    15 include "ERTLptr/ERTLptr.ma".
     15include "ERTL/ERTL.ma".
    1616
    1717(* This file is used only by untrusted code. We write it in Matita to
     
    1919
    2020definition examine_internal:
    21  ∀globals. joint_internal_function ERTLptr globals →
     21 ∀globals. joint_internal_function ERTL globals →
    2222  identifier_map RegisterTag Pos ≝
    2323λglobals,fun.
     
    7070         | extension_seq s ⇒
    7171            match s with
    72             [ ertlptr_ertl s ⇒
    73                match s with
    74                [ ertl_new_frame ⇒ map
    75                | ertl_del_frame ⇒ map
    76                | ertl_frame_size r ⇒ incr r map ]
    77             | LOW_ADDRESS r _ ⇒ incr r map
    78             | HIGH_ADDRESS r _ ⇒ incr r map ]]]
     72             [ ertl_new_frame ⇒ map
     73             | ertl_del_frame ⇒ map
     74             | ertl_frame_size r ⇒ incr r map ]]]
    7975   | final _ ⇒ map
    80    | FCOND (abs : has_fcond ERTLptr) _ _ _ ⇒ Ⓧabs ]
     76   | FCOND (abs : has_fcond ERTL) _ _ _ ⇒ Ⓧabs ]
    8177 in
    8278 foldi … f (joint_if_code … fun) (empty_map …).
Note: See TracChangeset for help on using the changeset viewer.