Ignore:
Timestamp:
Feb 18, 2013, 5:48:19 PM (7 years ago)
Author:
tranquil
Message:
  • another change in block definition
  • RTLabs -> RTL and ERTL -> ERTLptr passes fixed, others stil broken
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r2595 r2674  
    2828     〈set_runiverse … def runiverse, r〉.
    2929
    30 (* insert into a graph a block of instructions *)
    31 let rec adds_graph_list
     30definition state_update : ∀S.(S → S) → state_monad S unit ≝
     31λS,f,s.〈f s, it〉.
     32
     33(* insert into a graph a list of instructions *)
     34let rec adds_graph_pre
     35  X
    3236  (g_pars: graph_params)
    3337  (globals: list ident)
    34   (insts: list (joint_step g_pars globals))
    35   (src : label) (dst : label) on insts : joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
    36   λdef.match insts with
    37   [ nil ⇒ add_graph … src (sequential … (NOOP …) dst) def
    38   | cons instr others ⇒
    39     match others with
    40     [ nil ⇒ add_graph … src (sequential … instr dst) def
    41     | _ ⇒
    42       let 〈def', mid〉 ≝ fresh_label … def in
    43       let def'' ≝ add_graph … src (sequential … instr mid) def' in
    44       adds_graph_list … others mid dst def''
    45     ]
     38  (* for ERTLptr: the label parameter is filled by the last label *)
     39  (pre_process : label → X → joint_seq g_pars globals)
     40  (insts: list X)
     41  (src : label) on insts :
     42  state_monad (joint_internal_function g_pars globals) label ≝
     43  match insts with
     44  [ nil ⇒ return src
     45  | cons i rest ⇒
     46    ! mid ← fresh_label … ;
     47    ! dst ← adds_graph_pre … pre_process rest mid ;
     48    !_ state_update … (add_graph … src (sequential … (pre_process dst i) mid)) ;
     49    return dst
     50  ].
     51
     52let rec adds_graph_post
     53  (g_pars: graph_params)
     54  (globals: list ident)
     55  (insts: list (joint_seq g_pars globals))
     56  (dst : label) on insts :
     57  state_monad (joint_internal_function g_pars globals) label ≝
     58  match insts with
     59  [ nil ⇒ return dst
     60  | cons i rest ⇒
     61    ! src ← fresh_label … ;
     62    ! mid ← adds_graph_post … rest dst ;
     63    !_ state_update … (add_graph … src (sequential … i mid)) ;
     64    return src
    4665  ].
    4766
     
    5372  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
    5473  λg_pars,globals,insts,src,dst,def.
    55   let 〈pref, last〉 ≝ split_on_last_ne … insts in
    56   match pref with
    57   [ nil ⇒ add_graph … src (sequential … (last src) dst) def
    58   | _ ⇒
    59     let 〈def', lbl〉 ≝ fresh_label … def in
    60     let def'' ≝ adds_graph_list … (map_eval … pref lbl) src lbl def' in
    61     add_graph … lbl (sequential … (last lbl) dst) def''
    62   ].
     74  let pref ≝ \fst (\fst insts) in
     75  let op ≝ \snd (\fst insts) in
     76  let post ≝ \snd insts in
     77  let 〈def, mid〉 ≝ adds_graph_pre … (λlbl,inst.inst lbl) pref src def in
     78  let 〈def, mid'〉 ≝ adds_graph_post … post dst def in
     79  add_graph … mid (sequential … (op mid) mid') def.
    6380
    6481definition fin_adds_graph :
     
    6986  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
    7087  λg_pars,globals,insts,src,def.
    71   let 〈pref, last〉 ≝ insts in
    72   match pref with
    73   [ nil ⇒ add_graph … src (final … last) def
    74   | _ ⇒
    75     let 〈def', lbl〉 ≝ fresh_label … def in
    76     let def'' ≝ adds_graph_list … pref src lbl def' in
    77     add_graph … lbl (final … last) def''
    78   ].
     88  let pref ≝ \fst insts in
     89  let last ≝ \snd insts in
     90  let 〈def, mid〉 ≝ adds_graph_pre … (λ_.λi.i) pref src def in
     91  add_graph … mid (final … last) def.
    7992
    8093(* ignoring register allocation for now *)
     
    120133qed.
    121134
     135(*
    122136lemma adds_graph_list_fresh_preserve :
    123137  ∀g_pars,globals,b,src,dst,def.
     
    227241]
    228242qed.
     243*)
    229244
    230245axiom adds_graph_ok :
     
    368383  ∀src_g_pars,dst_g_pars : graph_params.
    369384  ∀globals: list ident.
    370   (* initialized function definition with empty graph *)
    371   joint_internal_function dst_g_pars globals →
     385  (* initialization info *)
     386  call_dest dst_g_pars → (* joint_if_result *)
     387  paramsT dst_g_pars → (* joint_if_params *)
     388  ℕ → (* joint_if_stacksize *)
    372389  (* functions dictating the translation *)
    373390  (label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) →
     
    377394  (* destination function *)
    378395  joint_internal_function dst_g_pars globals ≝
    379   λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
     396  λsrc_g_pars,dst_g_pars,globals,
     397   init_ret,init_params,init_stack_size,trans_step,trans_fin_step,def.
     398  let init ≝
     399    mk_joint_internal_function dst_g_pars globals
     400    (joint_if_luniverse … def)
     401    (joint_if_runiverse … def)
     402    init_ret init_params init_stack_size
     403    (add ?? (empty_map ? (joint_statement ??)) (joint_if_entry … def) (RETURN …))
     404    (pi1 … (joint_if_entry … def)) in
    380405  let f : label → joint_statement (src_g_pars : params) globals →
    381406    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
     
    388413    | FCOND abs _ _ _ ⇒ Ⓧabs
    389414    ] in
    390   foldi … f (joint_if_code … def) empty.
     415  foldi … f (joint_if_code … def) init.
     416@hide_prf >graph_code_has_point @mem_set_add_id qed.
    391417
    392418definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝
     
    421447*)
    422448
     449
    423450axiom b_graph_translate_ok :
    424451  ∀src_g_pars,dst_g_pars : graph_params.
    425   ∀globals: list ident.∀empty.∀f_step,f_fin,def_in.
     452  ∀globals: list ident.
     453  ∀init_ret,init_params,init_stack_size.
     454  ∀f_step,f_fin,def_in.
    426455  luniverse_ok ?? def_in →
     456  code_closed … (joint_if_code … def_in) →
    427457  let def_out ≝
    428     b_graph_translate src_g_pars dst_g_pars globals empty f_step f_fin def_in in
     458    b_graph_translate src_g_pars dst_g_pars globals
     459      init_ret init_params init_stack_size f_step f_fin def_in in
    429460  luniverse_ok … def_out ∧
    430   joint_if_result … def_out = joint_if_result … empty ∧
    431   joint_if_params … def_out = joint_if_params … empty ∧
    432   joint_if_stacksize … def_out = joint_if_stacksize … empty ∧
     461  code_closed … (joint_if_code … def_out) ∧
     462  joint_if_result … def_out = init_ret ∧
     463  joint_if_params … def_out = init_params ∧
     464  joint_if_stacksize … def_out = init_stack_size ∧
    433465  pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in) ∧
    434466  ∃f_lbls : label → option (list label).
     
    469501  ∀src_g_pars,dst_g_pars : graph_params.
    470502  ∀globals: list ident.
    471   (* initialized function definition with empty graph *)
    472   joint_internal_function dst_g_pars globals →
     503  (* initialization info *)
     504  call_dest dst_g_pars → (* joint_if_result *)
     505  paramsT dst_g_pars → (* joint_if_params *)
     506  ℕ → (* joint_if_stacksize *)
    473507  (* functions dictating the translation *)
    474508  (label → joint_step src_g_pars globals → step_block dst_g_pars globals) →
     
    478512  (* destination function *)
    479513  joint_internal_function dst_g_pars globals ≝
    480   λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step.
    481   b_graph_translate … empty
     514  λsrc_g_pars,dst_g_pars,globals,init1,init2,init3,trans_step,trans_fin_step.
     515  b_graph_translate … init1 init2 init3
    482516    (λl,s.return trans_step l s)
    483517    (λl,s.return trans_fin_step l s).
    484 
    485 (* helper for initializing a valid init graph (with a valid entry) *)
    486 definition init_graph_if ≝
    487   λg_pars : graph_params.λglobals.
    488   λluniverse,runiverse,ret,params,stack_size,entry.
    489   let graph ≝ add ?? (empty_map ? (joint_statement ??)) entry (RETURN …) in
    490   mk_joint_internal_function g_pars globals
    491     luniverse runiverse ret params stack_size
    492     graph entry.
    493 @hide_prf >graph_code_has_point @map_mem_prop @graph_add
    494 qed.
    495 
    496518
    497519(*
Note: See TracChangeset for help on using the changeset viewer.