Changeset 1271


Ignore:
Timestamp:
Sep 26, 2011, 4:24:32 PM (8 years ago)
Author:
mulligan
Message:

finished, kind of

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1263 r1271  
    22include "LTL/LTL.ma".
    33include "ERTL/spill.ma".
    4 include "ERTL/build.ma".
    54include "ERTL/uses.ma".
    65include "ASM/Arithmetic.ma".
     
    284283      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    285284        〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
    286     | joint_instr_call_id f ignore ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_call_id … f ignore) l) graph, luniv〉
     285    | joint_instr_call_id f ignore ignore' ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_call_id … f ignore ignore') l) graph, luniv〉
    287286    | joint_instr_store addr1 addr2 srcr ⇒
    288287      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_store … it it it) l) in
     
    441440qed.
    442441
    443 let rec mapi_aux
    444   (a: Type[0]) (b: Type[0]) (f: BitVector 16 → a → b) (n: nat)
    445     on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n
    446   match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → BitVectorTrie b n with
    447   [ O ⇒ λinvariant. λtrie: BitVectorTrie a 0. λaccu: BitVector 16.
    448     match trie return λx: nat. λtrie: BitVectorTrie a x. ∀prf: x = 0. BitVectorTrie b x with
    449     [ Leaf l ⇒ λprf. Leaf … (f accu l)
    450     | Stub s ⇒ λprf. Stub … s
     442let rec fold_aux
     443  (a, b: Type[0]) (f: BitVector 16 → a → b → b) (seed: b) (n: nat)
     444    on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b
     445  match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b with
     446  [ O    ⇒ λinvariant: 0 ≤ 16. λtrie: BitVectorTrie a 0. λpath: BitVector 16.
     447    match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = 0. b with
     448    [ Leaf l      ⇒ λproof. f path l seed
     449    | Stub s      ⇒ λproof. seed
    451450    | Node n' l r ⇒ λabsrd. ⊥
    452     ] (refl … 0)
    453   | S n' ⇒ λinvariant. λtrie: BitVectorTrie a (S n'). λaccu: BitVector (16 - (S n')).
    454     match trie return λx: nat. λtrie: BitVectorTrie a x. ∀prf: x = S n'. BitVectorTrie b x with
    455     [ Leaf l ⇒ λabsrd. ⊥
    456     | Stub s ⇒ λprf. Stub … s
    457     | Node n'' l r ⇒ λprf.
    458       Node ? n'' ? ?
    459     ] (refl nat (S n'))
     451    ] (refl … 0) 
     452  | S n' ⇒ λinvariant: S n' ≤ 16. λtrie: BitVectorTrie a (S n'). λpath: BitVector (16 - S n').
     453    match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = S n'. b with
     454    [ Leaf l      ⇒ λabsrd. ⊥
     455    | Stub s      ⇒ λproof. seed
     456    | Node n'' l r ⇒ λproof.
     457        fold_aux a b f (fold_aux a b f seed n' ? (l⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((false:::path)⌈S (16 - S n') ↦ 16 - n'⌉)) n' ? (r⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((true:::path)⌈S (16 - S n') ↦ 16 - n'⌉)
     458    ] (refl (S n'))
    460459  ].
    461   [ 1,2: destruct(absrd)
    462   | 3  : destruct(prf)
    463          @(mapi_aux a b f n' ? l ((false ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
    464          [ 1: @Sm_leq_n_m_leq_n
    465               assumption
    466          | 2: <minus_Sn_m
    467               [ 1: >minus_S_S %
    468               | 2: assumption
    469               ]
    470          ]
    471   | 4  : destruct(prf)
    472          @(mapi_aux a b f n' ? r ((true ::: accu)⌈S (16 - S n') ↦ 16 - n'⌉))
    473          [ 1: @Sm_leq_n_m_leq_n
    474               assumption
    475          | 2: <minus_Sn_m
    476               [ 1: >minus_S_S %
    477               | 2: assumption
    478               ]
    479          ]
    480   ]
     460  [ 1, 2: destruct(absrd)
     461  | 3,8: >minus_S_S <minus_Sn_m // @le_S_S_to_le //
     462  | 4,7: destruct(proof) %
     463  | 5,6: @Sm_leq_n_m_leq_n // ]
    481464qed.
    482465
    483 definition mapi
     466definition bvt_fold
    484467  λa, b: Type[0].
    485   λf: label → a → b.
     468  λf: label → a → b → b.
    486469  λtrie: BitVectorTrie a 16.
    487     let f' ≝ λbv: BitVector 16. λa.
    488       f (an_identifier LabelTag bv) a
     470  λseed: b.
     471    let f' ≝ λbv: BitVector 16. λa. λb.
     472      f (an_identifier LabelTag bv) a b
    489473    in
    490       mapi_aux a b f' 16 ? trie [[]].
     474      fold_aux a b f' seed 16 ? trie [[]].
    491475  //
    492476qed.
    493  
    494 definition translate_internal ≝
    495   λglobals.
    496   λint_fun.
    497   let graph ≝ ((empty_map …) : ltl_statement_graph globals) in
     477
     478definition graph_fold ≝
     479  λglobals.
     480  λb : Type[0].
     481  λf    : label → ertl_statement globals → b → b.
     482  λgraph: graph (ertl_statement globals).
     483  λseed : b.
     484  match graph with
     485  [ an_id_map tree ⇒ bvt_fold (ertl_statement globals) b f tree seed
     486  ]. 
     487
     488definition translate_internal: ∀globals: list ident.
     489  ertl_internal_function globals → ltl_internal_function globals ≝
     490  λglobals: list ident.
     491  λint_fun: ertl_internal_function globals.
     492  let graph ≝ (empty_map … : ltl_statement_graph globals) in
    498493  let valuation ≝ analyse globals int_fun in
    499494  let coloured_graph ≝ build valuation in
    500   let liveafter ≝ analyse globals int_fun in
    501   let blah ≝ mapi … (λlabel. λstmt_graph_luniv.
    502     let stmt ≝
    503       match eliminable globals (liveafter label) stmt with
    504       [ Some successor ⇒ 〈joint_st_goto … successor, graph, joint_if_luniverse … int_fun〉
    505       | None           ⇒ translate_statement globals int_fun valuation coloured_graph graph stmt
    506       ]
    507     in
    508       ?) (joint_if_code … int_fun)
    509   in ?.
    510  
    511  
    512  
    513       let stmt =
    514         match Liveness.eliminable (G.liveafter label) stmt with
    515         | Some successor ->
    516             LTL.St_skip successor
    517         | None ->
    518             I.translate_statement stmt
    519       in
    520       graph := Label.Map.add label stmt !graph
    521     ) int_fun.ERTL.f_graph
    522 
    523 definition translate_funct ≝
    524   λname_def.
    525   let 〈name, def〉 ≝ name_def in
    526   let def' ≝
    527     match def with
    528     [ Internal def ⇒ Internal ? (translate_internal name def)
    529     | External def ⇒ External ? def
    530     ]
     495  let 〈graph, luniv〉 ≝ graph_fold globals ((ltl_statement_graph globals) × (universe LabelTag)) (λlabel: label. λstmt: ertl_statement globals. λgraph_luniv: (? × (universe LabelTag)).
     496    let 〈graph, luniv〉 ≝ graph_luniv in
     497      match eliminable globals (valuation label) stmt with
     498      [ Some successor ⇒ 〈add_graph globals label (joint_st_goto … successor) graph, luniv〉
     499      | None           ⇒
     500        translate_statement globals int_fun valuation coloured_graph graph stmt label
     501      ]) (joint_if_code globals (ertl_params globals) int_fun) 〈graph, joint_if_luniverse … int_fun〉
    531502  in
    532     〈name, def'〉.
    533 
    534 definition translate ≝
    535   λp.
    536   let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
    537     mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
     503    mk_joint_internal_function globals (ltl_params globals)
     504      luniv (joint_if_runiverse … int_fun)
     505        it it it (joint_if_stacksize … int_fun)
     506          graph ? ?.
     507  cases daemon (* XXX *)
     508qed.
     509
     510definition ertl_to_ltl : ertl_program → ltl_program ≝
     511 λp. transform_program … p (transf_fundef … (translate_internal …)).
  • src/ERTL/liveness.ma

    r1260 r1271  
    9696    | joint_instr_load r _ _ ⇒ lattice_psingleton r
    9797    (* Potentially destroys all caller-save hardware registers. *)
    98     | joint_instr_call_id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
     98    | joint_instr_call_id id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    9999    | joint_instr_comment c ⇒ lattice_bottom
    100100    | joint_instr_cond r lbl_true ⇒ lattice_bottom
     
    142142    | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
    143143    (* Reads the hardware registers that are used to pass parameters. *)
    144     | joint_instr_call_id _ nparams ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
     144    | joint_instr_call_id _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    145145    | joint_instr_comment c ⇒ lattice_bottom
    146146    | joint_instr_cond r lbl_true ⇒ lattice_psingleton r
     
    214214      else
    215215        Some ? l
    216     | joint_instr_call_id _ nparams ⇒ None ?
     216    | joint_instr_call_id _ nparams _ ⇒ None ?
    217217    | joint_instr_comment c ⇒ None ?
    218218    | joint_instr_cond r lbl_true ⇒ None ?
  • src/ERTL/uses.ma

    r1260 r1271  
    3535    | joint_instr_clear_carry ⇒ uses
    3636    | joint_instr_set_carry ⇒ uses
    37     | joint_instr_call_id _ _ ⇒ uses
     37    | joint_instr_call_id _ _ _ ⇒ uses
    3838    | joint_instr_pop r ⇒ count r uses
    3939    | joint_instr_push r ⇒ count r uses
  • src/LTL/LTL.ma

    r1270 r1271  
    99
    1010definition ltl_program ≝ joint_program ltl_params.
     11
     12definition ltl_internal_function ≝ λglobals. joint_internal_function globals (ltl_params globals).
  • src/joint/Joint.ma

    r1270 r1271  
    9292    (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
    9393
     94definition set_joint_if_graph ≝
     95  λglobals,pars.
     96  λgraph.
     97  λp:joint_internal_function globals pars.
     98  λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
     99  λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
     100   mk_joint_internal_function globals pars
     101    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     102    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     103    graph (dp … (joint_if_entry … p) entry_prf) (dp … (joint_if_exit … p) exit_prf).
     104
    94105definition set_luniverse ≝
    95106  λglobals,pars.
Note: See TracChangeset for help on using the changeset viewer.