Changeset 1084 for src/ERTL


Ignore:
Timestamp:
Jul 21, 2011, 5:00:47 PM (9 years ago)
Author:
mulligan
Message:

more added on ertl pass: not sure how much should be axiomatised wrt register colouring

Location:
src/ERTL
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1082 r1084  
    3232  | ertl_st_load: register → register → register → label → ertl_statement
    3333  | ertl_st_store: register → register → register → label → ertl_statement
    34   | ertl_st_call_id: ident → Byte → label → ertl_statement
     34  | ertl_st_call_id: label → Byte → label → ertl_statement
    3535  | ertl_st_cond: register → label → label → ertl_statement
    36   | ertl_st_return: ertl_statement. (* XXX: change from o'caml *)
     36  | ertl_st_return: label → ertl_statement.
    3737
    3838definition ertl_statement_graph ≝ graph ertl_statement.
  • src/ERTL/ERTLToLTL.ma

    r1082 r1084  
    11include "ERTL/ERTL.ma".
     2include "ERTL/ERTLToLTLI.ma".
    23include "LTL/LTL.ma".
     4
     5definition translate_funct ≝
     6  λname_def.
     7  let 〈name, def〉 ≝ name_def in
     8  let def' ≝
     9    match def with
     10    [ Internal def ⇒ Internal ? (translate_internal name def)
     11    | External def ⇒ External ? def
     12    ]
     13  in
     14    〈name, def'〉.
     15
     16definition translate ≝
     17  λp.
     18  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
     19    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
  • src/ERTL/ERTLToLTLI.ma

    r1083 r1084  
    156156    let l ≝ read globals r (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
    157157      joint_st_sequential ? globals (joint_instr_skip globals) l
    158   | _ ⇒ ?
    159   ].
    160 
    161   let translate_statement (stmt : ERTL.statement) : LTL.statement =
    162     match stmt with
    163 
    164       | ERTL.St_addrH (r, x, l) ->
    165         let (hdw, l) = write r l in
    166         let l = generate (LTL.St_from_acc (hdw, l)) in
    167         let l = generate (LTL.St_to_acc (I8051.dph, l)) in
    168         LTL.St_addr (x, l)
    169 
    170       | ERTL.St_addrL (r, x, l) ->
    171         let (hdw, l) = write r l in
    172         let l = generate (LTL.St_from_acc (hdw, l)) in
    173         let l = generate (LTL.St_to_acc (I8051.dpl, l)) in
    174         LTL.St_addr (x, l)
    175 
    176       | ERTL.St_int (r, i, l) ->
    177         let (hdw, l) = write r l in
    178         LTL.St_int (hdw, i, l)
    179 
    180       | ERTL.St_move (r1, r2, l) ->
    181         move (lookup r1) (lookup r2) l
    182 
    183       | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) ->
    184         let (hdw, l) = write destr l in
    185         let l = generate (LTL.St_from_acc (hdw, l)) in
    186         let l = generate (LTL.St_opaccs (opaccs, l)) in
    187         let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    188         let l = generate (LTL.St_from_acc (I8051.b, l)) in
    189         let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    190         LTL.St_skip l
    191 
    192       | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) ->
    193         let (hdw, l) = write destr l in
    194         let l = generate (LTL.St_from_acc (hdw, l)) in
    195         let l = generate (LTL.St_to_acc (I8051.b, l)) in
    196         let l = generate (LTL.St_opaccs (opaccs, l)) in
    197         let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    198         let l = generate (LTL.St_from_acc (I8051.b, l)) in
    199         let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    200         LTL.St_skip l
    201 
    202       | ERTL.St_op1 (op1, destr, srcr, l) ->
    203         let (hdw, l) = write destr l in
    204         let l = generate (LTL.St_from_acc (hdw, l)) in
    205         let l = generate (LTL.St_op1 (op1, l)) in
    206         let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
    207         LTL.St_skip l
    208 
    209       | ERTL.St_op2 (op2, destr, srcr1, srcr2, l) ->
    210         let (hdw, l) = write destr l in
    211         let l = generate (LTL.St_from_acc (hdw, l)) in
    212         let l = generate (LTL.St_op2 (op2, I8051.b, l)) in
    213         let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    214         let l = generate (LTL.St_from_acc (I8051.b, l)) in
    215         let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    216         LTL.St_skip l
    217 
    218       | ERTL.St_clear_carry l ->
    219         LTL.St_clear_carry l
    220 
    221       | ERTL.St_set_carry l ->
    222         LTL.St_set_carry l
    223 
    224       | ERTL.St_load (destr, addr1, addr2, l) ->
    225         let (hdw, l) = write destr l in
    226         let l = generate (LTL.St_from_acc (hdw, l)) in
    227         let l = generate (LTL.St_load l) in
    228         let l = generate (LTL.St_from_acc (I8051.dph, l)) in
    229         let l = generate (LTL.St_to_acc (I8051.st0, l)) in
    230         let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
    231         let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    232         let l = generate (LTL.St_from_acc (I8051.st0, l)) in
    233         let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    234         LTL.St_skip l
    235 
    236       | ERTL.St_store (addr1, addr2, srcr, l) ->
    237         let l = generate (LTL.St_store l) in
    238         let l = generate (LTL.St_to_acc (I8051.st1, l)) in
    239         let l = generate (LTL.St_from_acc (I8051.dph, l)) in
    240         let l = generate (LTL.St_to_acc (I8051.st0, l)) in
    241         let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
    242         let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    243         let l = generate (LTL.St_from_acc (I8051.st0, l)) in
    244         let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
    245         let l = generate (LTL.St_from_acc (I8051.st1, l)) in
    246         let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
    247         LTL.St_skip l
    248 
    249       | ERTL.St_call_id (f, _, l) ->
    250         LTL.St_call_id (f, l)
    251 
    252       | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
    253         let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
    254         let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
    255         LTL.St_skip l
    256 
    257       | ERTL.St_return _ ->
    258         LTL.St_return
     158  | ertl_st_addr_h r x l ⇒
     159    let 〈hdw, l〉 ≝ write globals r l in
     160    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     161    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPH) l) in
     162      joint_st_sequential ? globals (joint_instr_address globals x ?) l
     163  | ertl_st_addr_l r x l ⇒
     164    let 〈hdw, l〉 ≝ write globals r l in
     165    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     166    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterDPL) l) in
     167      joint_st_sequential ? globals (joint_instr_address globals x ?) l
     168  | ertl_st_int r i l ⇒
     169    let 〈hdw, l〉 ≝ write globals r l in
     170      joint_st_sequential ? globals (joint_instr_int globals hdw i) l
     171  | ertl_st_move r1 r2 l ⇒ move globals (lookup r1) (lookup r2) l
     172  | ertl_st_opaccs_a opaccs destr srcr1 srcr2 l ⇒
     173    let 〈hdw, l〉 ≝ write globals destr l in
     174    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     175    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     176    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     177    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     178    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     179      joint_st_sequential ? globals (joint_instr_skip globals) l
     180  | ertl_st_opaccs_b opaccs destr srcr1 srcr2 l ⇒
     181    let 〈hdw, l〉 ≝ write globals destr l in
     182    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     183    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterB) l) in
     184    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_opaccs globals opaccs) l) in
     185    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     186    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     187    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     188      joint_st_sequential ? globals (joint_instr_skip globals) l
     189  | ertl_st_op1 op1 destr srcr l ⇒
     190    let 〈hdw, l〉 ≝ write globals destr l in
     191    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     192    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op1 globals op1) l) in
     193    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     194      joint_st_sequential ? globals (joint_instr_skip globals) l
     195  | ertl_st_op2 op2 destr srcr1 srcr2 l ⇒
     196    let 〈hdw, l〉 ≝ write globals destr l in
     197    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     198    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_op2 globals op2 RegisterB) l) in
     199    let l ≝ read globals srcr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     200    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterB) l) in
     201    let l ≝ read globals srcr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     202      joint_st_sequential ? globals (joint_instr_skip globals) l
     203  | ertl_st_clear_carry l ⇒ joint_st_sequential ? globals (joint_instr_clear_carry globals) l
     204  | ertl_st_set_carry l ⇒ joint_st_sequential ? globals (joint_instr_set_carry globals) l
     205  | ertl_st_load destr addr1 addr2 l ⇒
     206    let 〈hdw, l〉 ≝ write globals destr l in
     207    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals hdw) l) in
     208    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_load globals) l) in
     209    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     210    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
     211    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     212    let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     213    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
     214    let l ≝ read globals addr2 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     215      joint_st_sequential ? globals (joint_instr_skip globals) l
     216  | ertl_st_store addr1 addr2 srcr l ⇒
     217    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_store globals) l) in
     218    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST1) l) in
     219    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
     220    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_to_acc globals RegisterST0) l) in
     221    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPL) l) in
     222    let l ≝ read globals addr1 (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     223    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterST0) l) in
     224    let l ≝ read globals addr2 (λ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 RegisterST1) l) in
     226    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     227      joint_st_sequential ? globals (joint_instr_skip globals) l
     228  | ertl_st_call_id f ignore l ⇒  joint_st_sequential ? globals (joint_instr_call_id globals f) l
     229  | ertl_st_cond srcr lbl_true lbl_false ⇒
     230    let l ≝ generate globals (joint_st_sequential ? globals (joint_instr_cond_acc globals lbl_true) lbl_false) in
     231    let l ≝ read globals srcr (λhdw. joint_st_sequential ? globals (joint_instr_to_acc globals hdw) l) in
     232      joint_st_sequential ? globals (joint_instr_skip globals) l
     233  | ertl_st_return l ⇒ joint_st_return ? globals
     234  ].
     235  cases daemon (* XXX: todo -- proofs regarding gvars *)
     236qed.
Note: See TracChangeset for help on using the changeset viewer.