Changeset 1154


Ignore:
Timestamp:
Aug 31, 2011, 11:26:33 AM (8 years ago)
Author:
mulligan
Message:

changes to ertl files: in process of removing ertltoltli.ma in favour or merge with ertltoltl.ma due to constraints imposed by functorised o'caml code

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1152 r1154  
    33include "LTL/LTL.ma".
    44include "ERTL/spill.ma".
     5
     6include "ERTL/ERTL.ma".
     7include "LTL/LTL.ma".
     8include "ASM/Arithmetic.ma".
     9
     10(* XXX: change from O'Caml: former contents of ERTLToLTLI.ma *)
     11
     12inductive decision: Type[0] ≝
     13  | decision_spill: Byte → decision
     14  | decision_colour: Register → decision.
     15 
     16axiom lookup: register → decision.
     17axiom generate: ∀globals: list ident. ltl_statement globals → label.
     18axiom fresh_label: ∀globals: list ident. ltl_function_definition globals → ltl_function_definition globals × label.
     19axiom add_graph: ∀globals. label → ltl_statement globals → ltl_statement_graph globals → ltl_statement_graph globals.
     20axiom num_locals: nat.
     21
     22definition num_locals ≝
     23  λint_fun.
     24    colour_locals + (ertl_if_stacksize int_fun).
     25
     26definition stacksize ≝
     27  λint_fun.
     28    colour_locals + (ertl_if_stacksize int_fun).
     29
     30definition adjust_off ≝
     31  λoff.
     32  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
     33  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? num_locals) int_off false in
     34    sub.
     35
     36definition get_stack ≝
     37  λglobals.
     38  λr.
     39  λoff.
     40  λl.
     41    let off ≝ adjust_off off in
     42    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in
     43    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
     44    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     45    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     46    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     47    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     48    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
     49      joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
     50
     51definition set_stack ≝
     52  λglobals.
     53  λoff.
     54  λr.
     55  λl.
     56  let off ≝ adjust_off off in
     57  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
     58  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals r) l) in
     59  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     60  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     61  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     62  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     63  let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
     64    joint_st_sequential ? globals (joint_instr_int globals RegisterA off) l.
     65
     66definition write ≝
     67  λglobals.
     68  λr: register.
     69  λl: label.
     70  match lookup r with
     71  [ decision_spill off ⇒ 〈RegisterSST, generate globals (set_stack globals off RegisterSST l)〉
     72  | decision_colour hwr ⇒ 〈hwr, l〉
     73  ].
     74
     75definition read ≝
     76  λglobals.
     77  λr: register.
     78  λstmt: Register → ltl_statement globals.
     79  match lookup r with
     80  [ decision_colour hwr ⇒ generate globals (stmt hwr)
     81  | decision_spill off ⇒
     82    let temphwr ≝ RegisterSST in
     83    let l ≝ generate globals (stmt temphwr) in
     84      generate globals (get_stack globals temphwr off l)
     85  ].
     86
     87definition move ≝
     88  λglobals: list ident.
     89  λdest: decision.
     90  λsrc: decision.
     91  λl: label.
     92  match dest with
     93  [ decision_colour dest_hwr ⇒
     94    match src with
     95    [ decision_colour src_hwr ⇒
     96      if eq_Register dest_hwr src_hwr then
     97        joint_st_goto ? globals l
     98      else
     99        let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals dest_hwr) l) in
     100          joint_st_sequential ? globals (joint_instr_to_acc globals src_hwr) l
     101    | decision_spill src_off ⇒ get_stack globals dest_hwr src_off l
     102    ]
     103  | decision_spill dest_off ⇒
     104    match src with
     105    [ decision_colour src_hwr ⇒ set_stack globals dest_off src_hwr l
     106    | decision_spill src_off ⇒
     107      if eq_bv ? dest_off src_off then
     108        joint_st_goto ? globals l
     109      else
     110        let temp_hwr ≝ RegisterSST in
     111        let l ≝ generate globals (set_stack globals dest_off temp_hwr l) in
     112          get_stack globals temp_hwr src_off l
     113    ]
     114  ].
     115
     116definition newframe ≝
     117  λglobals.
     118  λl.
     119  if eq_nat stacksize 0 then
     120    joint_st_goto ? globals l
     121  else
     122    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
     123    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPH) l) in
     124    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPH (zero ?)) l) in
     125    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPH) l) in
     126    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
     127    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Sub RegisterDPL) l) in
     128    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_clear_carry globals) l) in
     129    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterDPL (bitvector_of_nat ? stacksize)) l) in
     130      joint_st_sequential ? globals (joint_instr_to_acc globals RegisterSPL) l.
     131
     132definition delframe ≝
     133  λglobals.
     134  λl.
     135  if eq_nat stacksize 0 then
     136    joint_st_goto ? globals l
     137  else
     138    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPH) l) in
     139    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Addc RegisterSPH) l) in
     140    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_int globals RegisterA (zero ?)) l) in
     141    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterSPL) l) in
     142    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals Add RegisterSPL) l) in
     143      joint_st_sequential ? globals (joint_instr_int globals RegisterA (bitvector_of_nat ? stacksize)) l.
     144
     145definition translate_statement ≝
     146  λglobals: list ident.
     147  λstmt: ertl_statement.
     148  match stmt with
     149  [ ertl_st_skip l ⇒ joint_st_goto ? globals l
     150  | ertl_st_comment s l ⇒ joint_st_sequential ? globals (joint_instr_comment globals s) l
     151  | ertl_st_cost cost_lbl l ⇒ joint_st_sequential ? globals (joint_instr_cost_label globals cost_lbl) l
     152  | ertl_st_get_hdw destr sourcehwr l ⇒ move globals (lookup destr) (decision_colour sourcehwr) l
     153  | ertl_st_set_hdw desthwr srcr l ⇒ move globals (decision_colour desthwr) (lookup srcr) l
     154  | ertl_st_hdw_to_hdw r1 r2 l ⇒
     155    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals r1) l) in
     156      joint_st_sequential ? globals (joint_instr_to_acc globals r2) l
     157  | ertl_st_new_frame l ⇒ newframe globals l
     158  | ertl_st_del_frame l ⇒ delframe globals l
     159  | ertl_st_frame_size r l ⇒
     160    let 〈hdw, l〉 ≝ write globals r l in
     161      joint_st_sequential ? globals (joint_instr_int globals hdw (bitvector_of_nat ? stacksize)) l
     162  | ertl_st_pop r l ⇒
     163    let 〈hdw, l〉 ≝ write globals r l in
     164    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     165      joint_st_sequential ? globals (joint_instr_pop globals) l
     166  | ertl_st_push r l ⇒
     167    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_push globals) l) in
     168    let l ≝ read globals r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     169      joint_st_goto ? globals l
     170  | ertl_st_addr rl rh x l ⇒
     171    let 〈hdw1, l〉 ≝ write globals rh l in
     172    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw1) l) in
     173    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
     174    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l) in
     175    let 〈hdw2, l〉 ≝ write globals rl l in
     176    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw2) l) in
     177    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
     178      joint_st_sequential ? globals (joint_instr_address globals x ?) l
     179(*  | ertl_st_addr_h r x l ⇒
     180    let 〈hdw, l〉 ≝ write globals r l in
     181    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     182    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l)) in
     183      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
     184  | ertl_st_addr_l r x l ⇒
     185    let 〈hdw, l〉 ≝ write globals r l in
     186    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l)) in
     187    let l ≝ generate globals (ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l)) in
     188      ltl_st_lift globals (joint_st_sequential ? globals (joint_instr_address globals x ?) l)
     189*)
     190  | ertl_st_int r i l ⇒
     191    let 〈hdw, l〉 ≝ write globals r l in
     192      joint_st_sequential ? globals (joint_instr_int globals hdw i) l
     193  | ertl_st_move r1 r2 l ⇒ move globals (lookup r1) (lookup r2) l
     194  | ertl_st_opaccs opaccs destr1 destr2 srcr1 srcr2 l ⇒
     195    let 〈hdw, l〉 ≝ write globals destr1 l in
     196    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     197    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     198    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     199    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     200    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     201    let l ≝ generate globals (joint_st_goto ? globals l) in
     202    let 〈hdw, l〉 ≝ write globals destr2 l in
     203    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     204    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
     205    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     206    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     207    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     208    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     209      joint_st_goto ? globals l
     210(*
     211  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
     212    let 〈hdw, l〉 ≝ write globals destr l in
     213    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     214    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     215    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     216    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     217    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     218      joint_st_goto ? globals l
     219  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
     220    let 〈hdw, l〉 ≝ write globals destr l in
     221    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     222    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
     223    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     224    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     225    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     226    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     227      joint_st_goto ? globals l
     228*)
     229  | ertl_st_op1 op1 destr srcr l ⇒
     230    let 〈hdw, l〉 ≝ write globals destr l in
     231    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     232    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
     233    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     234      joint_st_goto ? globals l
     235  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
     236    let 〈hdw, l〉 ≝ write globals destr l in
     237    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     238    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
     239    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     240    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     241    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     242      joint_st_goto ? globals l
     243  | ertl_st_clear_carry l ⇒ joint_st_sequential ? globals (joint_instr_clear_carry globals) l
     244  | ertl_st_set_carry l ⇒ joint_st_sequential ? globals (joint_instr_set_carry globals) l
     245  | ertl_st_load destr addr1 addr2 l ⇒
     246    let 〈hdw, l〉 ≝ write globals destr l in
     247    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     248    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
     249    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     250    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
     251    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     252    let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     253    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
     254    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     255      joint_st_goto ? globals l
     256  | ertl_st_store addr1 addr2 srcr l ⇒
     257    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
     258    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
     259    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     260    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
     261    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     262    let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     263    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
     264    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     265    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST1) l) in
     266    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     267      joint_st_goto ? globals l
     268  | ertl_st_call_id f ignore l ⇒ joint_st_sequential ? globals (joint_instr_call_id globals f) l
     269  | ertl_st_cond srcr lbl_true lbl_false ⇒
     270    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
     271    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     272      joint_st_goto ? globals l
     273  | ertl_st_return ⇒ joint_st_return ? globals
     274  ].
     275  cases daemon (* XXX: todo -- proofs regarding gvars *)
     276qed.
     277
     278(* **** *)
    5279
    6280definition translate_internal ≝
  • src/ERTL/ERTLToLTLI.ma

    r1138 r1154  
    1313axiom add_graph: ∀globals. label → ltl_statement globals → ltl_statement_graph globals → ltl_statement_graph globals.
    1414axiom num_locals: nat.
    15 axiom stacksize: nat.
     15
     16definition num_locals ≝
     17  λint_fun.
     18    colour_locals + (ertl_if_stacksize int_fun).
     19
     20definition stacksize ≝
     21  λint_fun.
     22    colour_locals + (ertl_if_stacksize int_fun).
    1623(* *** *)
    1724
Note: See TracChangeset for help on using the changeset viewer.