Changeset 1171


Ignore:
Timestamp:
Sep 2, 2011, 2:51:20 PM (8 years ago)
Author:
mulligan
Message:

changes made on claudio's request: changed order of nesting in the joint-ertl statements to make the semantics easier to write. big changes required...

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1168 r1171  
    1515definition ertl_params: params ≝
    1616 mk_params register register register register (move_registers × move_registers) register.
     17                 
     18inductive ertl_statement_extension: Type[0] ≝
     19  | ertl_st_ext_new_frame: label → ertl_statement_extension
     20  | ertl_st_ext_del_frame: label → ertl_statement_extension
     21  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
    1722
    18 definition pre_ertl_statement ≝ joint_statement label ertl_params.
    19                  
    20 inductive ertl_statement (globals: list ident): Type[0] ≝
    21   | ertl_st_lift_pre: pre_ertl_statement globals → ertl_statement globals
    22   | ertl_st_new_frame: label → ertl_statement globals
    23   | ertl_st_del_frame: label → ertl_statement globals
    24   | ertl_st_frame_size: register → label → ertl_statement globals.
     23definition ertl_statement ≝ joint_statement label ertl_statement_extension ertl_params.
    2524
    2625definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
  • src/ERTL/ERTLToLTL.ma

    r1170 r1171  
    167167  λl.
    168168  if eq_nat (stacksize globals int_fun) 0 then
    169     〈joint_st_goto ? globals l, graph
     169    〈joint_st_goto … globals l, graph, (ertl_if_luniverse globals int_fun)
    170170  else
    171171    let luniv ≝ ertl_if_luniverse globals int_fun in
    172     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
    173     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
    174     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
    175     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
    176     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
    177     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
    178     let 〈l, graph, lunive〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
    179     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? (stacksize int_fun))) l) in
    180       〈joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l, graph, luniv〉.
     172    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? ? globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
     173    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it RegisterDPH) l) in
     174    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPH (zero ?)) l) in
     175    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterSPH)) l) in
     176    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
     177    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Sub it RegisterDPL) l) in
     178    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_clear_carry … globals) l) in
     179    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterDPL (bitvector_of_nat ? (stacksize globals int_fun))) l) in
     180      〈joint_st_sequential … globals (joint_instr_move ltl_params … globals (to_acc RegisterSPL)) l, graph, luniv〉.
    181181
    182182definition delframe ≝
    183   λint_fun.
    184   λglobals.
     183  λglobals.
     184  λint_fun.
    185185  λgraph: graph (ltl_statement globals).
    186186  λl.
    187   if eq_nat (stacksize int_fun) 0 then
    188     〈joint_st_goto ? globals l, graph
     187  if eq_nat (stacksize globals int_fun) 0 then
     188    〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun
    189189  else
    190     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
    191     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
    192     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
    193     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
    194     let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
    195       〈joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? (stacksize int_fun))) l, graph〉.
     190    let luniv ≝ ertl_if_luniverse globals int_fun in
     191    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPH)) l) in
     192    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Addc it RegisterSPH) l) in
     193    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_int … globals RegisterA (zero ?)) l) in
     194    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterSPL)) l) in
     195    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_op2 … globals Add it RegisterSPL) l) in
     196      〈joint_st_sequential … globals (joint_instr_int ltl_params … globals RegisterA (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉.
     197
     198check joint_st_sequential.
    196199
    197200definition translate_statement ≝
    198   λint_fun.
    199   λglobals: list ident.
    200   λgraph: graph (ltl_statement globals).
    201   λstmt: ertl_statement.
     201  λglobals: list ident.
     202  λint_fun.
     203  λgraph: ltl_statement_graph globals.
     204  λstmt: ertl_statement globals.
    202205  match stmt with
    203   [ ertl_st_skip l ⇒ 〈joint_st_goto ? globals l, graph〉
    204   | ertl_st_comment s l ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉
     206  [ ertl_st_lift_pre pre ⇒
     207    match pre with
     208    [ joint_st_sequential seq l ⇒
     209      match seq with
     210      [ joint_instr_comment c ⇒ 〈joint_st_sequential ? globals (joint_instr_comment globals s) l, graph〉
     211      | _ ⇒ ?
     212      ]
     213    | joint_st_return ⇒ 〈joint_st_return … globals, graph, ertl_if_luniverse globals int_fun〉
     214    | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, ertl_if_luniverse globals int_fun〉
     215    ]
     216  | ertl_st_new_frame l ⇒ newframe globals int_fun graph l
     217  | ertl_st_del_frame l ⇒ delframe globals int_fun graph l
     218  | ertl_st_frame_size r l ⇒
     219    let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun graph r l in
     220      〈joint_st_sequential … globals (joint_instr_int ltl_params … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     221  ].
     222 
     223  match stmt with
     224  | ertl_st_comment s l ⇒
    205225  | ertl_st_cost cost_lbl l ⇒ 〈joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l, graph〉
    206226  | ertl_st_get_hdw destr sourcehwr l ⇒ move int_fun globals graph (lookup destr) (decision_colour sourcehwr) l
     
    209229    let 〈l, graph〉 ≝ generate globals graph (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
    210230      〈joint_st_sequential ? globals (joint_instr_to_acc globals r2) l, graph〉
    211   | ertl_st_new_frame l ⇒ newframe int_fun globals graph l
    212   | ertl_st_del_frame l ⇒ delframe int_fun globals graph l
     231  | ertl_st_new_frame l ⇒
     232  | ertl_st_del_frame l ⇒
    213233  | ertl_st_frame_size r l ⇒
    214     let 〈hdw, l〉 ≝ write int_fun globals graph r l in
    215     let 〈l, graph〉 ≝ l in
    216       〈joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? (stacksize int_fun))) l, graph〉
    217234  | ertl_st_pop r l ⇒
    218235    let 〈hdw, l〉 ≝ write int_fun globals graph r l in
     
    335352    let 〈l, graph〉 ≝ read int_fun globals graph srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    336353      〈joint_st_goto ? globals l, graph〉
    337   | ertl_st_return ⇒ 〈joint_st_return ? globals, graph〉
    338354  ].
    339355  cases daemon (* XXX: todo -- proofs regarding gvars *)
  • src/LIN/LIN.ma

    r1168 r1171  
    55
    66definition pre_lin_statement ≝
    7  λglobals: list ident. joint_statement unit lin_params globals.
     7 λglobals: list ident. joint_statement unit unit lin_params globals.
    88
    99definition lin_statement ≝
  • src/LTL/LTL.ma

    r1168 r1171  
    66 mk_params unit unit unit unit registers_move Register.
    77
    8 definition ltl_statement ≝ λglobals: list ident. joint_statement label ltl_params globals.
     8definition ltl_statement ≝ λglobals: list ident. joint_statement label unit ltl_params globals.
    99 
    1010definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
  • src/LTL/LTLToLIN.ma

    r1166 r1171  
    1010  λs: ltl_statement globals.
    1111  match s with
    12   [ ltl_st_lift_joint joint ⇒
    13     match joint with
    14     [ joint_st_return ⇒ joint_st_return … globals
    15     | joint_st_sequential instr _ ⇒ joint_st_sequential … globals instr it
    16     | joint_st_goto l ⇒ joint_st_goto … globals l
    17     ]
     12  [ joint_st_return ⇒ joint_st_return … globals
     13  | joint_st_sequential instr _ ⇒ joint_st_sequential … globals instr it
     14  | joint_st_goto l ⇒ joint_st_goto … globals l
     15  | joint_st_extension ext ⇒ joint_st_extension … ext
    1816  ].
    1917   
     
    8179      let generated'' ≝ translated_statement :: generated in
    8280      match statement with
    83       [ ltl_st_lift_joint joint ⇒
    84         match joint with
    85         [ joint_st_sequential instr l2 ⇒
    86           match instr with
    87           [ joint_instr_cond acc_a_reg l1 ⇒
    88                 let required' ≝
    89                   if marked l2 visited' then
    90                     require l2 required
    91                   else
    92                     required in
    93                 let 〈required', generated''〉 ≝
    94                  foo l2 visited' required' globals generated'' g n' visit (*
    95                   if marked l2 visited' then
    96                     〈required', (Joint_St_Goto ? globals l2) :: generated''〉
    97                   else
    98                     visit globals g required' visited' generated'' l2 n'*) in
    99                 let required'' ≝ require l1 required' in
    100                   if ¬(marked l1 visited') then
    101                     visit globals g required'' visited' generated'' l1 n'
    102                   else
    103                     〈required', generated''〉
    104             | _ ⇒
     81      [ joint_st_sequential instr l2 ⇒
     82        match instr with
     83        [ joint_instr_cond acc_a_reg l1 ⇒
    10584              let required' ≝
    10685                if marked l2 visited' then
     
    10887                else
    10988                  required in
     89              let 〈required', generated''〉 ≝
     90               foo l2 visited' required' globals generated'' g n' visit (*
     91                if marked l2 visited' then
     92                  〈required', (Joint_St_Goto ? globals l2) :: generated''〉
     93                else
     94                  visit globals g required' visited' generated'' l2 n'*) in
     95              let required'' ≝ require l1 required' in
     96                if ¬(marked l1 visited') then
     97                  visit globals g required'' visited' generated'' l1 n'
     98                else
     99                  〈required', generated''〉
     100          | _ ⇒
     101            let required' ≝
    110102              if marked l2 visited' then
    111                 〈required', joint_st_goto … globals l2 :: generated''〉
     103                require l2 required
    112104              else
    113                 visit globals g required' visited' generated'' l2 n'
    114             ]
    115           | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    116       | joint_st_goto l ⇒
    117         let required' ≝
    118            if marked l visited' then
    119              require l required
    120            else
    121              required
    122          in
    123            if marked l visited' then
    124              〈required', joint_st_goto … globals l :: generated''〉
    125            else
    126              visit globals g required' visited' generated'' l n'
    127       ]
     105                required in
     106            if marked l2 visited' then
     107              〈required', joint_st_goto … globals l2 :: generated''〉
     108            else
     109              visit globals g required' visited' generated'' l2 n'
     110          ]
     111    | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
     112    | joint_st_goto l ⇒
     113      let required' ≝
     114        if marked l visited' then
     115         require l required
     116        else
     117         required
     118      in
     119        if marked l visited' then
     120          〈required', joint_st_goto … globals l :: generated''〉
     121        else
     122          visit globals g required' visited' generated'' l n'
     123    | joint_st_extension ext ⇒ 〈required, generated〉
    128124    ]
    129125  ]
  • src/joint/Joint.ma

    r1169 r1171  
    3333  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
    3434
    35 inductive joint_statement (next: Type[0]) (p:params) (globals: list ident): Type[0] ≝
    36   | joint_st_sequential: joint_instruction p globals → next → joint_statement next p globals
    37   | joint_st_goto: label → joint_statement next p globals
    38   | joint_st_return: joint_statement next p globals.
     35inductive joint_statement (next: Type[0]) (extend: Type[0]) (p:params) (globals: list ident): Type[0] ≝
     36  | joint_st_sequential: joint_instruction p globals → next → joint_statement next extend p globals
     37  | joint_st_goto: label → joint_statement next extend p globals
     38  | joint_st_return: joint_statement next extend p globals
     39  | joint_st_extension: extend → joint_statement next extend p globals.
    3940
    4041(* Used in LTL and LIN *) 
Note: See TracChangeset for help on using the changeset viewer.