Changeset 1175


Ignore:
Timestamp:
Sep 2, 2011, 5:58:01 PM (8 years ago)
Author:
mulligan
Message:

changes to ertl pass

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1171 r1175  
    3737}.
    3838
     39definition set_luniverse ≝
     40  λglobals  : list ident.
     41  λint_fun  : ertl_internal_function globals.
     42  λluniverse: universe LabelTag.
     43  let runiverse ≝ ertl_if_runiverse globals int_fun in
     44  let params    ≝ ertl_if_params globals int_fun in
     45  let locals    ≝ ertl_if_locals globals int_fun in
     46  let stacksize ≝ ertl_if_stacksize globals int_fun in
     47  let graph     ≝ ertl_if_graph globals int_fun in
     48  let entry     ≝ ertl_if_entry globals int_fun in
     49  let exit      ≝ ertl_if_exit globals int_fun in
     50    mk_ertl_internal_function globals
     51      luniverse runiverse params locals
     52      stacksize graph entry exit.
     53
    3954definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
    4055 
  • src/ERTL/ERTLToLTL.ma

    r1172 r1175  
    202202  λstmt: ertl_statement globals.
    203203  match stmt with
    204   [ ertl_st_lift_pre pre ⇒
    205     match pre with
    206     [ joint_st_sequential seq l ⇒
    207       match seq with
    208       [ joint_instr_comment c ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉
    209       | _ ⇒ ?
    210       ]
    211     | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉
    212     | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉
     204  [ joint_st_sequential seq l ⇒
     205    let luniv ≝ ertl_if_luniverse globals int_fun in
     206    match seq with
     207    [ joint_instr_comment c ⇒
     208      〈joint_st_sequential label unit ltl_params globals (joint_instr_comment … globals c) l, graph, luniv〉
     209    | joint_instr_cost_label cost_lbl ⇒
     210      〈joint_st_sequential … globals (joint_instr_cost_label … globals cost_lbl) l, graph, luniv〉
     211    | joint_instr_pop r ⇒
     212      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     213      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     214        〈joint_st_sequential … globals (joint_instr_pop ltl_params globals it) l, graph, luniv〉
     215    | joint_instr_push r ⇒
     216      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_push … globals it) l) in
     217      let int_fun ≝ set_luniverse globals int_fun luniv in
     218      let 〈l, graph, luniv〉 ≝ read globals int_fun graph r (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     219        〈joint_st_goto … globals l, graph, luniv〉
     220    | joint_instr_cond srcr lbl_true ⇒
     221      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_cond … globals it lbl_true) l) in
     222      let int_fun ≝ set_luniverse globals int_fun luniv in
     223      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     224        〈joint_st_goto … globals l, graph, luniv〉
     225    | joint_instr_call_id f ignore ⇒ 〈joint_st_sequential … globals (joint_instr_call_id … globals f ignore) l, graph, luniv〉
     226    | joint_instr_store addr1 addr2 srcr ⇒
     227      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_store … globals it it it) l) in
     228      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST1)) l) in
     229      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     230      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
     231      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
     232      let int_fun ≝ set_luniverse globals int_fun luniv in
     233      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     234      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
     235      let int_fun ≝ set_luniverse globals int_fun luniv in
     236      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     237      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST1)) l) in
     238      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     239        〈joint_st_goto … globals l, graph, luniv〉
     240    | joint_instr_load destr addr1 addr2 ⇒
     241      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
     242      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     243      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_load … globals it it it) l) in
     244      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPH)) l) in
     245      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterST0)) l) in
     246      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterDPL)) l) in
     247      let int_fun ≝ set_luniverse globals int_fun luniv in
     248      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr1 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     249      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterST0)) l) in
     250      let int_fun ≝ set_luniverse globals int_fun luniv in
     251      let 〈l, graph, luniv〉 ≝ read globals int_fun graph addr2 (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     252        〈joint_st_goto … globals l, graph, luniv〉
     253    | joint_instr_clear_carry ⇒ 〈joint_st_sequential … globals (joint_instr_clear_carry … globals) l, graph, luniv〉
     254    | joint_instr_set_carry ⇒ 〈joint_st_sequential … globals (joint_instr_set_carry … globals) l, graph, luniv〉
     255    | joint_instr_op2 op2 destr srcr ⇒
     256      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph destr l in
     257      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     258      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals op2 it RegisterB) l) in
     259      let luniv ≝ set_luniverse globals int_fun luniv in
     260      let 〈l, graph, luniv〉 ≝ read globals int_fun graph destr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     261      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
     262      let luniv ≝ set_luniverse globals int_fun luniv in
     263      let 〈l, graph, luniv〉 ≝ read globals int_fun graph srcr (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     264        〈joint_st_goto … globals l, graph, luniv〉
     265    | joint_instr_op1 op1 acc_a ⇒
     266      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a l in
     267      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     268      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op1 … globals op1 it) l) in
     269      let int_fun ≝ set_luniverse globals int_fun luniv in
     270      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     271        〈joint_st_goto … globals l, graph, luniv〉
     272    | joint_instr_int r i ⇒
     273      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     274        〈joint_st_sequential label unit ltl_params globals (joint_instr_int … globals hdw i) l, graph, luniv〉
     275    | joint_instr_opaccs opaccs acc_a_reg acc_b_reg ⇒
     276      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_a_reg l in
     277      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     278      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
     279      let luniv ≝ set_luniverse globals int_fun luniv in
     280      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     281      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) l) in
     282      let luniv ≝ set_luniverse globals int_fun luniv in
     283      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     284      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … globals l) in
     285      let luniv ≝ set_luniverse globals int_fun luniv in
     286      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph acc_b_reg l in
     287      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc hdw)) l) in
     288      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterB)) l) in
     289      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_opaccs … globals opaccs it it) l) in
     290      let luniv ≝ set_luniverse globals int_fun luniv in
     291      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_a_reg (λ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 RegisterB)) l) in
     293      let luniv ≝ set_luniverse globals int_fun luniv in
     294      let 〈l, graph, luniv〉 ≝ read globals int_fun graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) in
     295        〈joint_st_goto … globals l, graph, luniv〉
     296    | _ ⇒ ?
    213297    ]
    214   | ertl_st_new_frame l ⇒ newframe globals int_fun graph l
    215   | ertl_st_del_frame l ⇒ delframe globals int_fun graph l
    216   | ertl_st_frame_size r l ⇒
    217     let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
    218       〈joint_st_sequential … globals (joint_instr_int ltl_params … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     298  | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉
     299  | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉
     300  | joint_st_extension ext ⇒
     301    match ext with
     302    [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
     303    | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
     304    | ertl_st_ext_frame_size r l ⇒
     305      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     306        〈joint_st_sequential … globals (joint_instr_int ltl_params … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     307    ]
    219308  ].
    220309 
    221310  match stmt with
    222   | ertl_st_comment s l ⇒
    223   | ertl_st_cost cost_lbl l ⇒ 〈joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l, graph〉
    224311  | ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l
    225312  | ertl_st_set_hdw desthwr srcr l ⇒ move int_fun globals graph (decision_colour desthwr) (lookup srcr) l
     
    227314    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
    228315      〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉
    229   | ertl_st_new_frame l ⇒
    230   | ertl_st_del_frame l ⇒
    231   | ertl_st_frame_size r l ⇒
    232   | ertl_st_pop r l ⇒
    233     let 〈hdw, l〉 ≝ write int_fun globals graph r l in
    234     let 〈l, graph〉 ≝ l in
    235     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    236       〈joint_st_sequential ? globals (joint_instr_pop globals) l, graph〉
    237   | ertl_st_push r l ⇒
    238     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_push globals) l) in
    239     let 〈l, graph〉 ≝ read int_fun globals graph r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    240       〈joint_st_goto ? globals l, graph〉
    241316  | ertl_st_addr rl rh x l ⇒
    242317    let 〈hdw1, l〉 ≝ write int_fun globals graph rh l in
     
    261336      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
    262337*)
    263   | ertl_st_int r i l ⇒
    264     let 〈hdw, l〉 ≝ write int_fun globals graph r l in
    265     let 〈l, graph〉 ≝ l in
    266       〈joint_st_sequential ? globals (joint_instr_int globals hdw i) l, graph〉
    267338  | ertl_st_move r1 r2 l ⇒ move int_fun globals graph (lookup r1) (lookup r2) l
    268   | ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒
    269     let 〈hdw, l〉 ≝ write int_fun globals graph destr1 l in
    270     let 〈l, graph〉 ≝ l in
    271     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    272     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    273     let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    274     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    275     let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    276     let 〈l, graph〉 ≝ generate globals graph (joint_st_goto ? globals l) in
    277     let 〈hdw, l〉 ≝ write int_fun globals graph destr2 l in
    278     let 〈l, graph〉 ≝ l in
    279     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    280     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
    281     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
    282     let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    283     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    284     let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    285       〈joint_st_goto ? globals l, graph〉
    286339(*
    287340  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
     
    303356      joint_st_goto ? globals l
    304357*)
    305   | ertl_st_op1 op1 destr srcr l ⇒
    306     let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
    307     let 〈l, graph〉 ≝ l in
    308     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    309     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
    310     let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    311       〈joint_st_goto ? globals l, graph〉
    312   | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
    313     let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
    314     let 〈l, graph〉 ≝ l in
    315     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    316     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
    317     let 〈l, graph〉 ≝ read int_fun globals graph srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    318     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
    319     let 〈l, graph〉 ≝ read int_fun globals graph srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    320       〈joint_st_goto ? globals l, graph〉
    321   | ertl_st_clear_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_clear_carry globals) l, graph〉
    322   | ertl_st_set_carry l ⇒ 〈joint_st_sequential ? globals (joint_instr_set_carry globals) l, graph〉
    323   | ertl_st_load destr addr1 addr2 l ⇒
    324     let 〈hdw, l〉 ≝ write int_fun globals graph destr l in
    325     let 〈l, graph〉 ≝ l in
    326     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
    327     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
    328     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    329     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
    330     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    331     let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    332     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
    333     let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    334       〈joint_st_goto ? globals l, graph〉
    335   | ertl_st_store addr1 addr2 srcr l ⇒
    336     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_store globals) l) in
    337     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
    338     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
    339     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
    340     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
    341     let 〈l, graph〉 ≝ read int_fun globals graph addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    342     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
    343     let 〈l, graph〉 ≝ read int_fun globals graph addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    344     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
    345     let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    346       〈joint_st_goto ? globals l, graph〉
    347   | ertl_st_call_id f ignore l ⇒ 〈joint_st_sequential ? globals (joint_instr_call_id globals f) l, graph〉
    348   | ertl_st_cond srcr lbl_true lbl_false ⇒
    349     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
    350     let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    351       〈joint_st_goto ? globals l, graph〉
    352358  ].
    353359  cases daemon (* XXX: todo -- proofs regarding gvars *)
Note: See TracChangeset for help on using the changeset viewer.