Changeset 1463


Ignore:
Timestamp:
Oct 25, 2011, 5:33:53 PM (8 years ago)
Author:
mulligan
Message:

added erasure for lin

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Erase.ma

    r1461 r1463  
    9494    let 〈label, instruction〉 ≝ hd in
    9595    let relabelled ≝ relabel_pseudo_instruction instruction map in
     96    let label ≝
     97      match label with
     98      [ None ⇒ None …
     99      | Some label ⇒ Some … (lookup … ident map ident)
     100      ]
     101    in
    96102      〈label, relabelled〉 :: relabel tl map
    97103  ].
  • src/ERTL/liveness.ma

    r1425 r1463  
    152152    | PUSH r ⇒ lattice_psingleton r
    153153    | MOVE pair_reg ⇒
    154       (* only second reg in pair relevant *)
     154      (* only second reg in paidefinition liveafter ≝
     155  λglobals: list ident.
     156  λint_fun: ertl_internal_function globals.
     157  λlivebefore: label → ?.
     158  λlabel.
     159  λliveafter: valuation.
     160  match lookup … (joint_if_code … int_fun) label with
     161  [ None      ⇒ ?
     162  | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
     163      lattice_join (livebefore successor liveafter) accu)
     164      (statement_successors globals stmt) lattice_bottom
     165  ].
     166  cases not_implemented (* XXX *)
     167qed.r relevant *)
    155168      let r2 ≝ \snd pair_reg in
    156169      match r2 with
     
    264277definition equations ≝ label → rhs.
    265278
    266 record fixpoint: Type[0] ≝
    267 {
    268   fix_lfp    :1> equations → valuation;
    269   fix_correct:   ∀f: equations.
    270                  ∀v: label.
    271                    lattice_equal (f v (fix_lfp f)) (fix_lfp f v)
    272 }.
    273 
    274 axiom the_fixpoint: fixpoint.
    275 
    276279definition livebefore ≝
    277280  λglobals: list ident.
     
    301304qed.
    302305
     306record fixpoint: Type[0] ≝
     307{
     308  (* XXX: this never fails to compute a fixed point as in any program we will
     309          only ever use a finite number of pseudoregisters, therefore no chain
     310          conditions, etc. are necessary for this to terminate with a correct
     311          solution. *)
     312  fix_lfp    :1> equations → valuation;
     313  fix_correct:
     314    ∀globals: list ident.
     315    ∀int_fun.
     316    let f ≝ liveafter globals int_fun (livebefore globals int_fun) in
     317      ∀v: label.
     318        lattice_equal (f v (fix_lfp f)) (fix_lfp f v)
     319}.
     320
     321axiom the_fixpoint: fixpoint.
     322
    303323definition analyse ≝
    304324  λglobals.
  • src/joint/ProofUtils.ma

    r1458 r1463  
     1include "joint/Joint.ma".
     2include "LIN/LIN.ma".
     3
     4let rec pre_erase_lin_internal_function'
     5  (globals: list ident) (the_program: list (lin_statement globals))
     6    (labels: list label)
     7      on the_program: ((BitVectorTrie Word 16) × (list (lin_statement globals))) ≝
     8  match the_program with
     9  [ nil        ⇒
     10    match labels with
     11    [ nil ⇒ 〈Stub Word 16, [ ]〉 (* XXX: labels should be empty *)
     12    | _   ⇒ ⊥
     13    ]
     14  | cons hd tl ⇒
     15    let 〈lbl, instr〉 ≝ hd in
     16      match lbl with
     17      [ None ⇒
     18        let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
     19          match instr with
     20          [ sequential seq l ⇒
     21            match seq with
     22            [ COST_LABEL cost ⇒ 〈maps, instructions〉
     23            | _ ⇒ 〈maps, 〈None …, instr〉 :: instructions〉
     24            ]
     25          | _ ⇒ 〈maps, 〈None …, instr〉 :: instructions〉
     26          ]
     27      | Some lbl ⇒
     28        let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
     29        match instr with
     30        [ sequential seq l ⇒
     31          match seq with
     32          [ COST_LABEL cost ⇒ pre_erase_lin_internal_function' globals tl (lbl :: labels)
     33          | _ ⇒
     34            let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
     35            let maps ≝ foldr ? ? (λl. λmap.
     36              match l with
     37              [ an_identifier l ⇒ insert … l lbl' map
     38              ]) maps (lbl :: labels)
     39            in
     40              〈maps, instructions〉
     41          ]
     42        | _ ⇒
     43          let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
     44          let maps ≝ foldr ? ? (λl. λmap.
     45            match l with
     46            [ an_identifier l ⇒ insert … l lbl' map
     47            ]) maps (lbl :: labels)
     48          in
     49            〈maps, instructions〉
     50        ]
     51      ]
     52  ].
     53  @daemon
     54qed.
     55
     56definition relabel_lin_instruction:
     57    ∀globals: list ident. BitVectorTrie Word 16 → joint_instruction lin_params_ globals → joint_instruction lin_params_ globals ≝
     58  λglobals: list ident.
     59  λmap.
     60  λinstr.
     61  match instr with
     62  [ COND acc_a lbl ⇒
     63    let lbl ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
     64    let located ≝ an_identifier LabelTag (lookup … lbl map lbl) in
     65      COND lin_params_ globals acc_a located
     66  | _ ⇒ instr
     67  ].
     68
     69definition relabel_lin_statement:
     70    ∀globals: list ident. BitVectorTrie Word 16 → pre_lin_statement globals → pre_lin_statement globals ≝
     71  λglobals: list ident.
     72  λmap: BitVectorTrie Word 16.
     73  λstmt: pre_lin_statement globals.
     74  match stmt with
     75  [ sequential seq l ⇒
     76    let relabelled ≝ relabel_lin_instruction globals map seq in
     77      sequential lin_params_ globals relabelled it
     78  | RETURN ⇒ RETURN lin_params_ globals
     79  | GOTO l ⇒
     80    let l ≝ match l with [ an_identifier l ⇒ l ] in
     81    let located ≝ an_identifier LabelTag (lookup … l map l) in
     82      GOTO lin_params_ globals located
     83  ].
     84
     85let rec relabel
     86  (globals: list ident) (map: BitVectorTrie Word 16)
     87    (program: list (lin_statement globals))
     88      on program: list (lin_statement globals) ≝
     89  match program with
     90  [ nil        ⇒ [ ]
     91  | cons hd tl ⇒
     92    let 〈label, stmt〉 ≝ hd in
     93    let relabelled ≝ relabel_lin_statement globals map stmt in
     94    let label ≝
     95      match label with
     96      [ None ⇒ None …
     97      | Some label ⇒
     98        let label ≝ match label with [ an_identifier l ⇒ l ] in
     99          Some … (an_identifier LabelTag (lookup … label map label))
     100      ]
     101    in
     102      〈label, relabelled〉 :: relabel globals map tl
     103  ].
     104
     105definition pre_erase_lin_internal_function:
     106    ∀globals: list ident. joint_internal_function globals (lin_params globals) → joint_internal_function globals (lin_params globals) ≝
     107  λglobals.
     108  λfunction.
     109    let luniverse ≝ joint_if_luniverse … function in
     110    let runiverse ≝ joint_if_runiverse … function in
     111    let result ≝ joint_if_result … function in
     112    let params ≝ joint_if_params … function in
     113    let locals ≝ joint_if_locals … function in
     114    let stacksize ≝ joint_if_stacksize … function in
     115    let code ≝ joint_if_code … function in
     116    let entry ≝ ? in
     117    let exit ≝ ? in
     118    let 〈maps, code〉 ≝ pre_erase_lin_internal_function' globals code [ ] in
     119    let code ≝ relabel globals maps code in
     120      mk_joint_internal_function …
     121        luniverse runiverse result params
     122        locals stacksize code entry exit.
     123  cases daemon (* XXX *)
     124qed.
     125
     126definition erase_lin_program: lin_program → lin_program ≝
     127  λprogram.
     128    transform_program … program (transf_fundef … (pre_erase_lin_internal_function …)).
  • src/utilities/adt/set_adt.ma

    r1223 r1463  
    55
    66axiom set: Type[0] → Type[0].
     7
     8inductive set (elt_type: Type[0]): Type[0] ≝
     9  | empty: set elt_type
     10  | node : nat → set elt_type → elt_type → set elt_type → set elt_type.
     11
    712axiom set_empty: ∀elt_type. set elt_type.
    813
Note: See TracChangeset for help on using the changeset viewer.