Changeset 1284


Ignore:
Timestamp:
Oct 3, 2011, 8:35:23 AM (8 years ago)
Author:
sacerdot
Message:

Bugs fixed: fresh_label changes the label universe, but this was not propagated
correctly. Fixed in RTLtoERTL. To be fixed in RTLAbsToRTL and (maybe) in
ERTLtoRTL.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1283 r1284  
    5252    sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
    5353    sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr);
    54     sequential ertl_params_… (LOAD … destr addr1 addr2)
     54    sequential ertl_params_ … (LOAD … destr addr1 addr2)
    5555  ] start_lbl dest_lbl def.
    5656 
     
    6767  let hdw_params ≝ get_params_hdw globals hdw_params in
    6868    hdw_params @ (get_params_stack … stack_params).
    69  
     69
    7070definition add_prologue ≝
    7171  λglobals.
     
    7676  λdef.
    7777  let start_lbl ≝ joint_if_entry … (ertl_params globals) def in
    78   let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
     78  let 〈tmp_lbl, def〉 ≝ fresh_label … def in
    7979  match lookup … (joint_if_code … def) start_lbl
    8080    return λx. x ≠ None ? → ertl_internal_function globals with
     
    9696      add_graph … tmp_lbl last_stmt def
    9797  ] ?.
    98 [ cases start_lbl #x #H @H
     98[ cases start_lbl #x #H cases daemon (* @H *) (*CSC: XXXX, no Russell *)
    9999| cases (none_absrd) /2/ ]
    100100qed.
     
    140140  λdef.
    141141  let start_lbl ≝ joint_if_exit … (ertl_params globals) def in
    142   let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
     142  let 〈tmp_lbl, def〉 ≝ fresh_label … def in
    143143  match lookup … (joint_if_code … def) start_lbl
    144144    return λx. x ≠ None ? → ertl_internal_function globals with
     
    162162      set_joint_if_exit … tmp_lbl def' ?
    163163  ] ?.
    164 [ cases start_lbl #x #H @H
     164[ cases start_lbl #x #H cases daemon (* @H *) (* CSC: XXXX *)
    165165| cases (none_absrd) /2/
    166166| cases daemon (* CSC: XXXXX *)
     
    370370  λstmt.
    371371  λdef: joint_internal_function … (ertl_params globals).
    372   let 〈entry, nuniv〉 ≝ fresh_label … def in
    373   let graph ≝ add ? ? (joint_if_code … def) entry stmt in
    374     mk_joint_internal_function ? (ertl_params globals)
    375       nuniv (joint_if_runiverse … def) it (joint_if_params … def)
    376       (joint_if_locals … def) (joint_if_stacksize … def) graph
    377       ? ?.     
    378   [ % [ @entry | @graph_add ]
    379   | cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF ]
     372  let 〈entry, def〉 ≝ fresh_label … def in
     373  let graph ≝ add … (joint_if_code … def) entry stmt in
     374   set_joint_if_graph … (ertl_params globals) graph def ??.
     375  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
     376  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
     377    *) cases daemon (*CSC: XXX *)
     378  ]
    380379qed.
    381380
  • src/joint/TranslateUtils.ma

    r1283 r1284  
    3535qed.
    3636
    37 definition fresh_label ≝
    38   λglobals,params. λdef: joint_internal_function globals params.
    39     fresh LabelTag (joint_if_luniverse … def).
    40 
    41 let rec adds_graph
    42   (pars1: params1) (globals: list ident)
    43   (stmt_list: list (label → joint_statement (graph_params_ pars1) globals))
    44   (start_lbl: label) (dest_lbl: label)
    45   (def: joint_internal_function … (graph_params pars1 globals))
    46     on stmt_list ≝
    47   match stmt_list with
    48   [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
    49   | cons stmt stmt_list ⇒
    50     match stmt_list with
    51     [ nil ⇒ add_graph … start_lbl (stmt dest_lbl) def
    52     | _ ⇒
    53       let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
    54       let def ≝ add_graph … start_lbl (stmt tmp_lbl) def in
    55         adds_graph pars1 globals stmt_list tmp_lbl dest_lbl def]].
     37definition fresh_label:
     38 ∀pars0,globals. joint_internal_function … (graph_params pars0 globals) → label × (joint_internal_function … (graph_params pars0 globals)) ≝
     39  λpars0,globals,def.
     40    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
     41     〈r,set_luniverse … def luniverse〉.
    5642
    5743let rec add_translates
     
    6652    [ nil ⇒ trans start_lbl dest_lbl def
    6753    | _ ⇒
    68       let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
     54      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
    6955      let def ≝ trans start_lbl tmp_lbl def in
    7056        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
     57
     58definition adds_graph ≝
     59 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
     60  add_translates … (map … (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
Note: See TracChangeset for help on using the changeset viewer.