Changeset 1263


Ignore:
Timestamp:
Sep 23, 2011, 5:12:24 PM (8 years ago)
Author:
mulligan
Message:

changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1260 r1263  
    179179  λsrc: decision.
    180180  λl: label.
    181   λoriginal_label.
     181  λoriginal_label: label.
    182182  match dest with
    183183  [ decision_colour dest_hwr ⇒
     
    245245      〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l) graph, luniv〉.
    246246
    247 definition translate_statement ≝
     247definition translate_statement:
     248  ∀globals: list ident. ertl_internal_function globals → ∀v: valuation.
     249    coloured_graph v → ltl_statement_graph globals → ertl_statement globals →
     250      label → ((ltl_statement_graph globals) × (universe LabelTag)) ≝
    248251  λglobals: list ident.
    249252  λint_fun.
     
    258261    match seq with
    259262    [ joint_instr_comment c ⇒
    260       〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_comment … globals c) l) graph, luniv〉
     263      〈add_graph globals original_label (joint_st_sequential … (joint_instr_comment … c) l) graph, luniv〉
    261264    | joint_instr_cost_label cost_lbl ⇒
    262       〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l) graph, luniv〉
     265      〈add_graph globals original_label (joint_st_sequential … (joint_instr_cost_label … cost_lbl) l) graph, luniv〉
    263266    | joint_instr_pop r ⇒
    264       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    265       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    266         〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_pop … globals it) l) graph, luniv〉
     267      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     268      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     269      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
     270      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
     271        〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_pop … it) l) graph, luniv〉
    267272    | joint_instr_push r ⇒
    268       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in
     273      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_push … it) l) in
     274      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     275      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     276      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     277      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
     278        〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
     279    | joint_instr_cond srcr lbl_true ⇒
     280      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_cond … it lbl_true) l) in
    269281      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    270282      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    271283      let int_fun' ≝ set_luniverse globals ? int_fun luniv in
    272       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l frees) in
    273         〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
    274     | _ ⇒ ?
    275     ]
    276   | _ ⇒ ?
    277   ].
    278     | joint_instr_cond srcr lbl_true ⇒
    279       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
    280       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    281       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    282         〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
    283     | joint_instr_call_id f ignore ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l) graph, luniv〉
     284      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
     285        〈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〉
    284287    | joint_instr_store addr1 addr2 srcr ⇒
    285       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
    286       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST1)) l) in
    287       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    288       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
    289       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    290       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    291       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    292       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
    293       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    294       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    295       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
    296       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    297         〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
     288      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_store … it it it) l) in
     289      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST1)) l) in
     290      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPH)) l) in
     291      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST0)) l) in
     292      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPL)) l) in
     293      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     294      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     295      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     296      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
     297      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST0)) fresh_lbl) in
     298      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     299      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     300      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     301      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
     302      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST1)) fresh_lbl) in
     303      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     304      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     305      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
     306        〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
    298307    | joint_instr_load destr addr1 addr2 ⇒
    299       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
    300       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    301       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
    302       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
    303       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
    304       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
    305       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    306       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    307       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
    308       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    309       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    310         〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
    311     | joint_instr_clear_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) graph, luniv〉
    312     | joint_instr_set_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … globals (joint_instr_set_carry … globals) l) graph, luniv〉
     308      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     309      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     310      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
     311      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
     312      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_load … it it it) l) in
     313      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPH)) l) in
     314      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterST0)) l) in
     315      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterDPL)) l) in
     316      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     317      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     318      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     319      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr1 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
     320      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterST0)) fresh_lbl) in
     321      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     322      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     323      let int_fun ≝ set_luniverse globals ? int_fun luniv in
     324      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph addr2 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
     325        〈add_graph globals original_label (joint_st_goto … fresh_lbl) graph, luniv〉
     326    | joint_instr_clear_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_clear_carry …) l) graph, luniv〉
     327    | joint_instr_set_carry ⇒ 〈add_graph globals original_label (joint_st_sequential … (joint_instr_set_carry …) l) graph, luniv〉
    313328    | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
    314       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
    315       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    316       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it it RegisterB) l) in
    317       let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    318       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    319       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    320       let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    321       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    322         〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
    323     | joint_instr_op1 op1 destr srcr  ⇒
    324       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l in
    325       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    326       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it it) l) in
    327       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    328       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    329         〈add_graph globals original_label (joint_st_goto (ltl_params globals) globals l) graph, luniv〉
     329      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     330      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     331      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
     332      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
     333      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_op2 … op2 it it RegisterB) l) in
     334      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     335      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     336      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr1 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
     337      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterB)) fresh_lbl) in
     338      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     339      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     340      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph srcr2 (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
     341        〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
     342    | joint_instr_op1 op1 destr srcr ⇒
     343      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     344      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     345      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph destr l fresh_lbl in
     346      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
     347      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_op1 … op1 it it) l) in
     348      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     349      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     350      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     351      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
     352        〈add_graph globals original_label (joint_st_goto … l) graph, luniv〉
    330353    | joint_instr_int r i ⇒
    331       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    332         〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw i) l) graph, luniv〉
    333     | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
    334       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l in
    335       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    336       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
    337       let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    338       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    339       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    340       let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    341       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    342       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in
    343       let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    344       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l in
    345       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
    346       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in
    347       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
    348       let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    349       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    350       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
    351       let luniv ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    352       let 〈l, graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
    353         〈add_graph globals original_label (joint_st_goto … globals l) graph, luniv〉
     354      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     355      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     356      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
     357        〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_int … hdw i) l) graph, luniv〉
    354358    | joint_instr_move pair_regs ⇒
    355359      let regl ≝ \fst pair_regs in
     
    357361      match regl with
    358362      [ pseudo p1  ⇒
    359         match regr with
     363        match regr with 
    360364        [ pseudo p2  ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (colouring valuation coloured_graph (inl … p2)) l original_label
    361365        | hardware h ⇒ move globals int_fun graph (colouring valuation coloured_graph (inl … p1)) (decision_colour h) l original_label
     
    365369        [ pseudo p    ⇒ move globals int_fun graph (decision_colour h1) (colouring valuation coloured_graph (inl … p)) l original_label
    366370        | hardware h2 ⇒
    367           let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc h1)) l) in
    368             〈add_graph globals original_label (joint_st_sequential (ltl_params globals) globals (joint_instr_move (ltl_params globals) globals (to_acc h2)) l) graph, luniv〉
     371          let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc h1)) l) in
     372            〈add_graph globals original_label (joint_st_sequential ltl_params_ … (joint_instr_move … (to_acc h2)) l) graph, luniv〉
    369373        ]
    370374      ]
    371       | _ ⇒ ?
    372     ]
    373   | _ ⇒ ?
    374   ].
    375    
    376375    | joint_instr_address lbl prf dpl dph ⇒
    377       let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l in
     376      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     377      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     378      let 〈hdw1, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dph l fresh_lbl in
    378379      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw1)) l) in
    379380      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPH)) l) in
    380381      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_address … globals lbl prf it it) l) in
    381382      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    382       let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l in
     383      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     384      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     385      let 〈hdw2, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dpl l fresh_lbl in
    383386      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw2)) l) in
    384387      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
    385         〈joint_st_sequential (ltl_params globals) globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
     388        〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_address … lbl prf it it) l) graph, luniv〉
    386389    | joint_instr_extension ext ⇒
    387390      match ext with
    388       [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l
    389       | ertl_st_ext_del_frame ⇒ delframe globals int_fun graph l
     391      [ ertl_st_ext_new_frame ⇒ newframe globals int_fun graph l original_label
     392      | ertl_st_ext_del_frame ⇒ delframe globals int_fun graph l original_label
    390393      | ertl_st_ext_frame_size r ⇒
    391         let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    392           〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     394        let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     395        let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     396        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l fresh_lbl in
     397          〈add_graph globals original_label (joint_st_sequential ltl_params_ globals (joint_instr_int … hdw (bitvector_of_nat … (stacksize … int_fun))) l) graph, luniv〉
    393398      ]
     399    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
     400      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     401      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     402      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l fresh_lbl in
     403      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
     404      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_opaccs … opaccs it it) l) in
     405      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     406      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     407      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     408      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
     409      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterB)) fresh_lbl) in
     410      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     411      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     412      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     413      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
     414      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … fresh_lbl) in
     415      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     416      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     417      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     418      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l fresh_lbl in
     419      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
     420      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterB)) l) in
     421      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_opaccs … opaccs it it) l) in
     422      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     423      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     424      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     425      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) fresh_lbl in
     426      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) fresh_lbl) in
     427      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     428      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     429      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     430      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) fresh_lbl in
     431        〈add_graph globals original_label (joint_st_goto … globals fresh_lbl) graph, luniv〉
    394432    ]
    395   | joint_st_return ⇒ 〈joint_st_return … globals, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    396   | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
     433  | joint_st_return ⇒ 〈add_graph globals original_label (joint_st_return ltl_params_ globals) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
     434  | joint_st_goto l ⇒ 〈add_graph globals original_label (joint_st_goto ltl_params_ globals l) graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    397435  ].
    398436
Note: See TracChangeset for help on using the changeset viewer.