Changeset 3014


Ignore:
Timestamp:
Mar 28, 2013, 4:58:26 PM (4 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

Files:
1 deleted
9 edited
5 moved

Legend:

Unmodified
Added
Removed
  • driver/acc.ml

    r3005 r3014  
    2626 | Extracted.Compiler.Rtl_uniq_pass              -> "Rtl_uniq_pass             "
    2727 | Extracted.Compiler.Ertl_pass                  -> "Ertl_pass                 "
    28  | Extracted.Compiler.Ertlptr_pass               -> "Ertlptr_pass              "
    2928 | Extracted.Compiler.Ltl_pass                   -> "Ltl_pass                  "
    3029 | Extracted.Compiler.Lin_pass                   -> "Lin_pass                  "
  • driver/printer.ml

    r3002 r3014  
    167167 }
    168168
    169 let eRTLptr_printing_params =
    170  { Extracted.Joint_printer.print_pass_ind = printing_pass_independent_params
    171  ; print_acc_a_reg = Obj.magic print_register
    172  ; print_acc_b_reg = Obj.magic print_register
    173  ; print_acc_a_arg = Obj.magic (print_argument print_register)
    174  ; print_acc_b_arg = Obj.magic (print_argument print_register)
    175  ; print_dpl_reg = Obj.magic print_register
    176  ; print_dph_reg = Obj.magic print_register
    177  ; print_dpl_arg = Obj.magic (print_argument print_register)
    178  ; print_dph_arg = Obj.magic (print_argument print_register)
    179  ; print_snd_arg = Obj.magic (print_argument print_register)
    180  ; print_pair_move = Obj.magic
    181     (fun {Extracted.Types.fst = dst; snd = src} ->
    182       print_move_dst dst ^ " " ^ print_argument print_move_dst src )
    183  ; print_call_args =
    184     Obj.magic (fun n -> string_of_int (Extracted.Glue.int_of_matitanat n))
    185  ; print_call_dest = (fun _ -> "")
    186  ; print_ext_seq = (fun ertl_seq -> "TODO")
    187  }
    188 
    189169let joint_LTL_LIN_printing_params =
    190170 { Extracted.Joint_printer.print_pass_ind = printing_pass_independent_params
     
    232212 | Extracted.Compiler.Rtl_uniq_pass              -> "rtl_u"
    233213 | Extracted.Compiler.Ertl_pass                  -> "ertl"
    234  | Extracted.Compiler.Ertlptr_pass               -> "ertlptr"
    235214 | Extracted.Compiler.Ltl_pass                   -> "ltl"
    236215 | Extracted.Compiler.Lin_pass                   -> "lin"
     
    258237   | Extracted.Compiler.Ertl_pass ->
    259238      beprint (Extracted.ERTL_printer.print_ERTL_program eRTL_printing_params)
    260    | Extracted.Compiler.Ertlptr_pass ->
    261       beprint
    262        (Extracted.ERTLptr_printer.print_ERTLptr_program eRTLptr_printing_params)
    263239   | Extracted.Compiler.Ltl_pass ->
    264240      beprint
  • driver/rTLabsPrinter.ml

    r3000 r3014  
    149149
    150150let print_fun_ident = print_identifier "fun"
    151 
    152151let print_ident = print_identifier "id"
    153 
    154152let print_label = print_identifier "l"
    155 
    156153let print_reg = print_identifier "r"
     154let print_cost = print_identifier "k"
    157155
    158156let print_nat n = string_of_int (Extracted.Glue.int_of_matitanat n)
     
    236234  | St_cost (cost_lbl, lbl) ->
    237235      Printf.sprintf "emit %s --> %s"
    238         (print_label cost_lbl)
     236        (print_cost cost_lbl)
    239237        (print_label lbl)
    240238  | St_const (_, destr, cst, lbl) ->
  • 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 …).
  • src/LIN/LINToASM.ma

    r2984 r3014  
    3737    let 〈x, region, data〉 ≝ x_size in
    3838      〈add … res x (bitvector_of_Z … offset), offset + Z_of_nat (size_init_data_list data)〉 in
    39   let addresses ≝ foldl ?? globals_addr_internal 〈empty_map …, -(globals_stacksize … p)〉 (prog_vars ?? p) in
     39      (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *)
     40  let addresses ≝ foldl ?? globals_addr_internal 〈empty_map …, -(S (globals_stacksize … p))〉 (prog_vars ?? p) in
    4041mk_ASM_universe ? (mk_universe … one)
    4142  (an_identifier … one (* dummy *))
     
    430431  ! main ← Identifier_of_ident … (prog_main … p) ;
    431432  ! u ← state_get … ;
    432   let start_sp : Z ≝ -(globals_stacksize … p) in
     433  (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *)
     434  let start_sp : Z ≝ -(S (globals_stacksize … p)) in
    433435  let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … start_sp) in
    434436  let data ≝ flatten ? (map ?? (λx.\snd x) (prog_vars … p)) in
  • src/LIN/joint_LTL_LIN.ma

    r2783 r3014  
    1111| SAVE_CARRY : ltl_lin_seq
    1212| RESTORE_CARRY : ltl_lin_seq
    13 | LOW_ADDRESS : Register → label → ltl_lin_seq
    14 | HIGH_ADDRESS : Register → label → ltl_lin_seq.
     13(* store low/high parts of label address in the accumulator *)
     14| LOW_ADDRESS : label → ltl_lin_seq
     15| HIGH_ADDRESS : label → ltl_lin_seq.
    1516
    1617definition ltl_lin_seq_labels ≝ λs.match s with
    17 [ LOW_ADDRESS _ lbl ⇒ [ lbl ]
    18 | HIGH_ADDRESS _ lbl ⇒ [ lbl ]
     18[ LOW_ADDRESS lbl ⇒ [ lbl ]
     19| HIGH_ADDRESS lbl ⇒ [ lbl ]
    1920| _ ⇒ [ ]
    2021].
  • src/LIN/joint_LTL_LIN_semantics.ma

    r2969 r3014  
    5252  let carry ≝ other_bit (regs … st) in
    5353  return set_carry LTL_LIN_state carry st
    54 | LOW_ADDRESS r l ⇒  ! pc_lab ← gen_pc_from_label … ge curr_id l;
     54| LOW_ADDRESS l ⇒  ! pc_lab ← gen_pc_from_label … ge curr_id l;
    5555                    let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in
    56                     let regs ≝ hwreg_store r addrl (regs … st) in
     56                    let regs ≝ hwreg_store RegisterA addrl (regs … st) in
    5757                    return set_regs LTL_LIN_state regs st
    58 | HIGH_ADDRESS r l ⇒ ! pc_lab ← gen_pc_from_label … ge curr_id l;
     58| HIGH_ADDRESS l ⇒ ! pc_lab ← gen_pc_from_label … ge curr_id l;
    5959                    let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
    60                     let regs ≝ hwreg_store r addrh (regs … st) in
     60                    let regs ≝ hwreg_store RegisterA addrh (regs … st) in
    6161                    return set_regs LTL_LIN_state regs st
    6262].
  • src/compiler.ma

    r2946 r3014  
    1111include "RTLabs/RTLabsToRTL.ma".
    1212include "RTL/RTLToERTL.ma".
    13 include "ERTL/ERTLToERTLptr.ma".
    14 include "ERTLptr/ERTLptrToLTL.ma".
     13include "ERTL/ERTLToLTL.ma".
    1514include "LTL/LTLToLIN.ma".
    1615include "LIN/LINToASM.ma".
     
    2726 | rtl_uniq_pass: pass
    2827 | ertl_pass: pass
    29  | ertlptr_pass: pass
    3028 | ltl_pass: pass
    3129 | lin_pass: pass
     
    4846  | rtl_uniq_pass ⇒ with_stack_model rtl_program
    4947  | ertl_pass ⇒ with_stack_model ertl_program
    50   | ertlptr_pass ⇒ with_stack_model ertlptr_program
    5148  | ltl_pass ⇒ with_stack_model ltl_program
    5249  | lin_pass ⇒ with_stack_model lin_program
     
    103100  let st ≝ lookup_stack_cost … p in 
    104101  let i ≝ observe ertl_pass 〈p,st〉 in
    105   let p ≝ ertl_to_ertlptr p in
    106   let st ≝ lookup_stack_cost … p in 
    107   let i ≝ observe ertlptr_pass 〈p,st〉 in
    108   let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in
     102  let 〈p,stack_cost,max_stack〉 ≝ ertl_to_ltl compute_fixpoint colour_graph p in
    109103  (* The two stack models are the same *)
    110104  let st ≝ lookup_stack_cost … p in
  • src/joint/Traces.ma

    r2991 r3014  
    3333     first call to main shuold bring it to 2^16 - |globals| - |main stack|
    3434     Also, on words 2^16 - |globals| = - |globals| *)
     35  (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *)
    3536  let spp : xpointer ≝
    36     «mk_pointer spb (mk_offset (bitvector_of_Z 16 (-globals_size))),
     37    «mk_pointer spb (mk_offset (bitvector_of_Z 16 (-S (globals_size)))),
    3738     pi2 … spb» in
    3839(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
  • src/semantics.ma

    r2905 r3014  
    66include "RTL/RTL_semantics.ma".
    77include "ERTL/ERTL_semantics.ma".
    8 include "ERTLptr/ERTLptr_semantics.ma".
    98include "LTL/LTL_semantics.ma".
    109include "LIN/LIN_semantics.ma".
     
    3231  | ertl_pass ⇒
    3332     λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …
    34   | ertlptr_pass ⇒
    35      λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) …
    3633  | ltl_pass ⇒
    3734     λ_.mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
Note: See TracChangeset for help on using the changeset viewer.