Changeset 1471 for src/joint


Ignore:
Timestamp:
Oct 28, 2011, 3:05:07 PM (8 years ago)
Author:
mulligan
Message:

finished erasure and generalised so as to work on arbitrary joint programs

Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1380 r1471  
    117117    (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
    118118
     119definition set_joint_code ≝
     120  λglobals: list ident.
     121  λpars: params globals.
     122  λint_fun: joint_internal_function globals pars.
     123  λgraph: codeT … pars.
     124  λentry.
     125  λexit.
     126    mk_joint_internal_function globals pars
     127      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
     128      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
     129      graph entry exit.
     130
    119131definition set_joint_if_graph ≝
    120132  λglobals,pars.
     
    123135  λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
    124136  λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
    125    mk_joint_internal_function globals pars
    126     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    127     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    128     graph (dp … (joint_if_entry … p) entry_prf) (dp … (joint_if_exit … p) exit_prf).
     137    set_joint_code globals pars p graph
     138      (dp … (joint_if_entry … p) entry_prf) (dp … (joint_if_exit … p) exit_prf).
    129139
    130140definition set_luniverse ≝
  • src/joint/ProofUtils.ma

    r1470 r1471  
    1 include "joint/Joint.ma".
    21include "LIN/LIN.ma".
     2include "joint/SemanticUtils.ma".
    33
    44let rec pre_erase_lin_internal_function'
     
    5454qed.
    5555
     56definition pre_erase_lin_internal_function ≝
     57  λglobals: list ident.
     58  λint_fun: joint_internal_function … (lin_params globals).
     59    pre_erase_lin_internal_function' … (joint_if_code … (lin_params …) int_fun) [ ].
     60
    5661definition relabel_joint_instruction:
    5762    ∀globals: list ident.
     
    8994  ].
    9095
    91 let rec relabel
     96let rec relabel_lin_internal_function'
    9297  (globals: list ident) (map: BitVectorTrie Word 16)
    9398    (program: list (lin_statement globals))
     
    106111      ]
    107112    in
    108       〈label, relabelled〉 :: relabel globals map tl
    109   ].
    110 
    111 definition pre_erase_lin_internal_function:
    112     ∀globals: list ident. joint_internal_function globals (lin_params globals) → joint_internal_function globals (lin_params globals) ≝
     113      〈label, relabelled〉 :: relabel_lin_internal_function' globals map tl
     114  ].
     115
     116definition relabel_lin_internal_function ≝
    113117  λglobals.
    114   λfunction.
    115     let luniverse ≝ joint_if_luniverse … function in
    116     let runiverse ≝ joint_if_runiverse … function in
    117     let result ≝ joint_if_result … function in
    118     let params ≝ joint_if_params … function in
    119     let locals ≝ joint_if_locals … function in
    120     let stacksize ≝ joint_if_stacksize … function in
    121     let code ≝ joint_if_code … function in
    122     let entry ≝ ? in
    123     let exit ≝ ? in
    124     let 〈maps, code〉 ≝ pre_erase_lin_internal_function' globals code [ ] in
    125     let code ≝ relabel globals maps code in
    126       mk_joint_internal_function …
    127         luniverse runiverse result params
    128         locals stacksize code entry exit.
    129   cases daemon (* XXX *)
    130 qed.
    131 
    132 definition erase_lin_program: lin_program → lin_program ≝
    133   λprogram.
    134     transform_program … program (transf_fundef … (pre_erase_lin_internal_function …)).
    135 
    136 include "joint/SemanticUtils.ma".
     118  λmap.
     119  λint_fun: joint_internal_function globals (lin_params globals).
     120    relabel_lin_internal_function' globals map (joint_if_code … int_fun).
    137121
    138122definition empty_graph ≝
     
    158142    [ None ⇒ ⊥ (* XXX: should not happen *)
    159143    | Some statement ⇒
    160       let entered_previously ≝ ? in
    161       let visited ≝ insert … entry_point' true visited in
     144      let entered_previously ≝ bvt_lookup … entry_point' visited false in
    162145      match entered_previously return λe: bool. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
    163146      [ true ⇒ 〈map, visited, the_graph〉
    164147      | false ⇒ (* XXX: never visited here before *)
     148        let visited ≝ insert … entry_point' true visited in
    165149        match statement return λs: joint_statement (graph_params params1 globals) globals. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
    166150        [ sequential seq l ⇒
     
    169153            pre_erase_graph_internal_function' params1 globals the_graph (entry_point :: labels) l size_counter map visited
    170154          | COND acc_a cond_label ⇒
    171             let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in
    172               match size_counter with
    173               [ O ⇒ ⊥ (* XXX: should never happen *)
    174               | S size_counter ⇒
    175                 let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels cond_label size_counter map visited in
    176                 let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
    177                   〈map, visited, the_graph〉
    178               ]
     155            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
     156            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] cond_label size_counter map visited in
     157            let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
     158              〈map, visited, the_graph〉
    179159          | _ ⇒
    180             let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in
     160            let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
    181161            let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
    182162              〈map, visited, the_graph〉
     
    186166            〈map, visited, the_graph〉
    187167        | GOTO l ⇒
    188           let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph labels l size_counter map visited in
     168          let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] l size_counter map visited in
    189169          let map ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l entry_point' map ]) map (entry_point :: labels) in
    190170            〈map, visited, the_graph〉
     
    193173    ]
    194174  ].
    195   [4: @(lookup … entry_point' visited false)
    196   |*: cases daemon
    197   ]
     175  cases daemon
    198176qed.
    199177
     
    201179  λparams1: params1.
    202180  λglobals: list ident.
    203   λthe_graph: codeT globals (graph_params params1 globals).
    204   λentry_point: label.
    205     let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals the_graph [ ] entry_point (graph_num_nodes … the_graph) (Stub …) (Stub …) in
    206       〈map, the_graph〉.
     181  λint_fun: joint_internal_function globals (graph_params params1 globals).
     182  match joint_if_entry … int_fun with
     183  [ dp entry entry_proof ⇒
     184    let code ≝ joint_if_code … int_fun in
     185    let 〈map, visited, the_graph〉 ≝ pre_erase_graph_internal_function' params1 globals code [ ] entry (graph_num_nodes … code) (Stub …) (Stub …) in
     186      〈map, the_graph〉
     187  ].
    207188
    208189let rec relabel_graph'
     
    215196  | S size_counter ⇒
    216197    let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in
    217     let relabelled_entry_point ≝ an_identifier LabelTag ? in
     198    let relabelled_entry_point ≝ an_identifier LabelTag (bvt_lookup … entry_point' map entry_point') in
    218199    let statement ≝ lookup LabelTag ? the_graph entry_point in
    219200    match statement return λs: option (joint_statement (graph_params params1 globals) globals). codeT globals (graph_params params1 globals) with
    220201    [ None ⇒ ⊥ (* XXX: should not happen *)
    221202    | Some statement ⇒
    222       let entered_previously ≝ ? in
    223       let visited ≝ insert … entry_point' true visited in
     203      let entered_previously ≝ (bvt_lookup … entry_point' visited false) in
    224204      match entered_previously return λe: bool. codeT globals (graph_params params1 globals) with
    225205      [ true ⇒ the_graph
    226206      | false ⇒ (* XXX: never visited here before *)
     207        let visited ≝ insert … entry_point' true visited in
    227208        match statement return λs: joint_statement (graph_params params1 globals) globals. codeT globals (graph_params params1 globals) with
    228209        [ sequential seq l ⇒
     
    232213            [ COND acc_a cond_label ⇒
    233214              let cond_label' ≝ match cond_label with [ an_identifier l ⇒ l ] in
    234               let relabelled ≝ an_identifier LabelTag ? in
     215              let relabelled ≝ an_identifier LabelTag (bvt_lookup … cond_label' map cond_label') in
    235216              let tail_graph ≝ relabel_graph' params1 globals the_graph map visited cond_label size_counter in
    236217                〈tail_graph, COND … acc_a relabelled〉
     
    238219            ]
    239220          in
    240             match size_counter with
    241             [ O ⇒ ⊥ (* XXX: impossible *)
    242             | S size_counter ⇒
    243               let tail_graph ≝ relabel_graph' params1 globals the_graph map visited l size_counter in
    244               let relabelled ≝ an_identifier LabelTag ? in
    245                 add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled)
    246             ]
     221            let tail_graph ≝ relabel_graph' params1 globals the_graph map visited l size_counter in
     222            let relabelled ≝ an_identifier LabelTag (bvt_lookup … l' map l') in
     223              add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled)
    247224        | RETURN ⇒ the_graph
    248225        | GOTO l ⇒
    249226          let l' ≝ match l with [ an_identifier l ⇒ l ] in
    250           let relabelled ≝ an_identifier LabelTag ? in
     227          let relabelled ≝ an_identifier LabelTag (bvt_lookup … l' map l') in
    251228            add LabelTag … the_graph relabelled_entry_point (GOTO … relabelled)         
    252229        ]
     
    254231    ]
    255232  ].
    256   [3: @(lookup … l' map l')
    257   |4: @(lookup … cond_label' map cond_label')
    258   |5: @(lookup … l' map l')
    259   |6: @(lookup … entry_point' visited false)
    260   |7: @(lookup … entry_point' map entry_point')
    261   |*: cases daemon
    262   ]
     233  cases daemon
    263234qed.
    264235
    265236definition relabel_graph ≝
     237  λglobals: list ident.
    266238  λparams1: params1.
    267   λglobals: list ident.
    268   λthe_graph: codeT globals (graph_params params1 globals).
    269   λentry_point: label.
    270239  λmap: BitVectorTrie Word 16.
    271     relabel_graph' params1 globals the_graph map (Stub …) entry_point (graph_num_nodes … the_graph).
    272 
    273 definition pre_erase_graph_joint_internal_function ≝
    274   λparams1: params1.
    275   λglobals: list ident.
    276240  λint_fun: joint_internal_function globals (graph_params params1 globals).
    277   let luniverse ≝ joint_if_luniverse globals (graph_params params1 globals) int_fun in
    278   let runiverse ≝ joint_if_runiverse … int_fun in
    279   let result ≝ joint_if_result … int_fun in
    280   let params ≝ joint_if_params … int_fun in
    281   let locals ≝ joint_if_locals … int_fun in
    282   let stacksize ≝ joint_if_stacksize … int_fun in
    283   let code ≝ joint_if_code … int_fun in
     241    match joint_if_entry … int_fun with
     242    [ dp entry entry_prf ⇒
     243      let code ≝ joint_if_code … int_fun in
     244        relabel_graph' … code map (Stub …) entry (graph_num_nodes … code)
     245    ].
     246   
     247definition pre_erase_joint_internal_function ≝
     248  λglobals: list ident.
     249  λpars: params globals.
     250  λerasure_function: joint_internal_function globals pars → (BitVectorTrie Word 16) × (codeT … pars).
     251  λrelabelling_function: BitVectorTrie Word 16 → joint_internal_function globals pars → codeT … pars.
     252  λint_fun: joint_internal_function globals pars.
    284253  match joint_if_entry … int_fun with
    285254  [ dp entry entry_prf ⇒
    286255    match joint_if_exit … int_fun with
    287256    [ dp exit exit_prf ⇒
    288       let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 globals code entry in
    289       let code ≝ relabel_graph params1 globals code entry maps in
    290         mk_joint_internal_function …
    291           luniverse runiverse result params
    292           locals stacksize code entry exit
     257      let exit' ≝ word_of_identifier … exit in
     258      let entry' ≝ word_of_identifier … entry in
     259      let 〈maps, code〉 ≝ erasure_function int_fun in
     260      let int_fun ≝ set_joint_code globals pars int_fun code entry exit in
     261      let code ≝ relabelling_function maps int_fun in
     262        set_joint_code globals pars int_fun code (an_identifier … (bvt_lookup … entry' maps entry'))
     263        (an_identifier … (bvt_lookup … exit' maps exit'))
    293264    ]
    294265  ].
    295266  cases daemon (* XXX *)
    296267qed.
     268
     269definition erase_graph_program:
     270    ∀params1: params1. joint_program (graph_params params1) → joint_program (graph_params params1) ≝
     271  λparams1.
     272  λprogram.
     273    transform_program … program (transf_fundef … (pre_erase_joint_internal_function … (pre_erase_graph_internal_function …) (relabel_graph …))).
     274
     275definition erase_lin_program: lin_program → lin_program ≝
     276  λprogram.
     277    transform_program … program (transf_fundef … (pre_erase_joint_internal_function … (pre_erase_lin_internal_function …) (relabel_lin_internal_function …))).
Note: See TracChangeset for help on using the changeset viewer.