Changeset 1284 for src/RTL


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.

File:
1 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
Note: See TracChangeset for help on using the changeset viewer.