Changeset 2693 for src


Ignore:
Timestamp:
Feb 22, 2013, 11:39:03 AM (7 years ago)
Author:
sacerdot
Message:
  1. Stuff moved to correct places.
  2. ERTLptr pass added
Location:
src
Files:
2 edited
3 moved

Legend:

Unmodified
Added
Removed
  • src/BACKEND_BROKEN_FILES

    r2661 r2693  
    1010LIN/LINToASM.ma:                  FCOND rotto, deve fare cose diverse ora?
    1111
    12 ERTL/liveness.ma:                 FCOND rotto
    13  ERTL/Interference.ma
    14   ERTL/ERTLToLTL.ma
    15 
    1612RTL/RTL_semantics.ma:             parametri
    17 RTL/RTLToERTL.ma:                 parametri (??)
    18 
    19 RTLabs/RTLabsToRTL.ma             prova rotta (Ferruccio?) ci sta lavorando Paolo
    2013
    2114ASM/AssemblyProofSplit.ma         working, just veeery slow
  • src/ERTLptr/ERTLptrToLTL.ma

    r2690 r2693  
    1 
    21include "LTL/LTL.ma".
    3 include "ERTL/Interference.ma".
     2include "ERTLptr/Interference.ma".
    43include "ASM/Arithmetic.ma".
    54include "joint/TranslateUtils.ma".
     
    300299  ∀globals.∀after : valuation register_lattice.
    301300  coloured_graph after →
    302   ℕ → label → joint_step ERTL globals → bind_step_block LTL globals ≝
     301  ℕ → label → joint_step ERTLptr globals → bind_step_block LTL globals ≝
    303302  λglobals,after,grph,stack_sz,lbl,s.
    304303  bret … (
     
    362361    | extension_seq ext ⇒
    363362      match ext with
    364       [ ertl_new_frame ⇒ newframe ? stack_sz
    365       | ertl_del_frame ⇒ delframe ? stack_sz
    366       | ertl_frame_size r ⇒
    367         move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    368       ]
     363        [ ertlptr_ertl ext' ⇒
     364          match ext' with
     365          [ ertl_new_frame ⇒ newframe ? stack_sz
     366          | ertl_del_frame ⇒ delframe ? stack_sz
     367          | ertl_frame_size r ⇒
     368            move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
     369          ]
     370        | LOW_ADDRESS r1 l ⇒
     371           translate_low_address ? carry_lives_after (lookup_arg r1) l
     372        | HIGH_ADDRESS r1 l ⇒
     373           translate_high_address ? carry_lives_after (lookup_arg r1) l       
     374        ]
    369375    ]
    370376  | COST_LABEL cost_lbl ⇒ 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉
     
    383389
    384390definition translate_fin_step:
    385   ∀globals.label → joint_fin_step ERTL → bind_fin_block LTL globals ≝
     391  ∀globals.label → joint_fin_step ERTLptr → bind_fin_block LTL globals ≝
    386392  λglobals,lbl,s.
    387393  bret … (〈[ ],
     
    393399
    394400definition translate_data : ∀globals.
    395   joint_closed_internal_function ERTL globals →
    396   bind_new register (b_graph_translate_data ERTL LTL globals) ≝
     401  joint_closed_internal_function ERTLptr globals →
     402  bind_new register (b_graph_translate_data ERTLptr LTL globals) ≝
    397403λglobals,int_fun.
    398404(* colour registers *)
     
    402408let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
    403409bret …
    404   (mk_b_graph_translate_data ERTL LTL globals
     410  (mk_b_graph_translate_data ERTLptr LTL globals
    405411    (* init_ret ≝ *) it
    406412    (* init_params ≝ *) it
  • src/ERTLptr/Interference.ma

    r2690 r2693  
    1 include "ERTL/liveness.ma".
     1include "ERTLptr/liveness.ma".
    22
    33inductive decision: Type[0] ≝
  • src/ERTLptr/liveness.ma

    r2690 r2693  
    1 
    21include "ASM/Util.ma".
    3 include "ERTL/ERTL.ma".
     2include "ERTLptr/ERTLptr.ma".
    43include "utilities/adt/set_adt.ma".
    54include "utilities/fixpoints.ma".
     
    4342definition defined ≝
    4443  λglobals: list ident.
    45   λs: joint_statement ERTL globals.
     44  λs: joint_statement ERTLptr globals.
    4645  match s with
    4746  [ sequential seq l ⇒
     
    6261                                    (rl_psingleton dr2))
    6362                      (rl_hsingleton RegisterCarry)
    64       | OP1 op1 r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
     63      | OP1 op1 r1 r2 ⇒ rl_psingleton r1
    6564      | POP r ⇒ rl_psingleton r
    6665      | ADDRESS _ _ r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
     
    7776      | extension_seq ext ⇒
    7877        match ext with
    79         [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    80         | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    81         | ertl_frame_size r ⇒ rl_psingleton r
     78        [ ertlptr_ertl ext' ⇒
     79           match ext' with
     80           [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     81           | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     82           | ertl_frame_size r ⇒ rl_psingleton r
     83           ]
     84        | LOW_ADDRESS r1 l ⇒ rl_psingleton r1
     85        | HIGH_ADDRESS r1 l ⇒ rl_psingleton r1
    8286        ]
    8387      (* Potentially destroys all caller-save hardware registers. *)
     
    101105definition used ≝
    102106  λglobals: list ident.
    103   λs: joint_statement ERTL globals.
     107  λs: joint_statement ERTLptr globals.
    104108  match s with
    105109  [ sequential seq l ⇒
     
    134138      | extension_seq ext ⇒
    135139        match ext with
    136         [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    137         | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    138         | ertl_frame_size r ⇒ rl_bottom
    139         ]
     140        [ ertlptr_ertl ext' ⇒
     141           match ext' with
     142           [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     143           | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
     144           | ertl_frame_size r ⇒ rl_bottom ]
     145        | LOW_ADDRESS r1 l ⇒ rl_bottom
     146        | HIGH_ADDRESS r1 l ⇒ rl_bottom
     147        ]       
    140148      (* Reads the hardware registers that are used to pass parameters. *)
    141149      | _ ⇒ rl_bottom
     
    157165  λglobals: list ident.
    158166  λl: register_lattice.
    159   λs: joint_statement ERTL globals.
     167  λs: joint_statement ERTLptr globals.
    160168  let pliveafter ≝ \fst l in
    161169  let hliveafter ≝ \snd l in
     
    211219      | extension_seq ext ⇒
    212220        match ext with
    213         [ ertl_new_frame ⇒ None ?
    214         | ertl_del_frame ⇒ None ?
    215         | ertl_frame_size r ⇒
    216           if set_member ? (eq_identifier RegisterTag) r pliveafter then
    217             None ?
    218           else
    219             Some ? l
    220         ]
     221        [ ertlptr_ertl ext' ⇒
     222           match ext' with
     223           [ ertl_new_frame ⇒ None ?
     224           | ertl_del_frame ⇒ None ?
     225           | ertl_frame_size r ⇒
     226             if set_member ? (eq_identifier RegisterTag) r pliveafter then
     227               None ?
     228             else
     229               Some ? l]
     230        | LOW_ADDRESS r1 l' ⇒
     231           if set_member ? (eq_identifier RegisterTag) r1 pliveafter then
     232             None ?
     233           else
     234             Some ? l
     235        | HIGH_ADDRESS r1 l' ⇒
     236           if set_member ? (eq_identifier RegisterTag) r1 pliveafter then
     237             None ?
     238           else
     239             Some ? l
     240        ]       
    221241      | _ ⇒ None ?
    222242      ]
     
    227247
    228248definition statement_semantics: ∀globals: list ident.
    229   joint_statement ERTL globals → register_lattice → register_lattice ≝
     249  joint_statement ERTLptr globals → register_lattice → register_lattice ≝
    230250  λglobals.
    231251  λstmt.
     
    238258definition livebefore ≝
    239259  λglobals: list ident.
    240   λint_fun: joint_internal_function ERTL globals.
     260  λint_fun: joint_internal_function ERTLptr globals.
    241261  λlabel.
    242262  λliveafter: valuation register_lattice.
     
    248268definition liveafter ≝
    249269   λglobals: list ident.
    250   λint_fun: joint_internal_function ERTL globals.
     270  λint_fun: joint_internal_function ERTLptr globals.
    251271  λlabel.
    252272  λliveafter: valuation register_lattice.
  • src/compiler.ma

    r2645 r2693  
    1616  return 〈init_cost,p',p〉.
    1717
    18 (*
    1918include "RTLabs/RTLabsToRTL.ma".
    2019include "RTL/RTLToERTL.ma".
    2120include "ERTL/ERTLToLTL.ma".
     21(*
    2222include "LTL/LTLToLIN.ma".
    2323include "LIN/LINToASM.ma".
     24*) include "ASM/ASM.ma". include "LIN/LIN.ma".
     25   axiom ltl_to_lin: ltl_program → lin_program.
     26   axiom lin_to_asm: lin_program → pseudo_assembly_program.
    2427
    2528(* these are already defined in utilities/fixpoint.ma and ERTL/Interference.ma
     
    3538  let p ≝ ltl_to_lin p in
    3639          lin_to_asm p.
    37 *)
    38 include "ASM/ASM.ma".
    39 axiom back_end : RTLabs_program → pseudo_assembly_program.
    4040
    4141(* JHM: minimum needed for assembler axiom to typecheck *)
Note: See TracChangeset for help on using the changeset viewer.