Changeset 2843 for src/joint


Ignore:
Timestamp:
Mar 11, 2013, 1:02:02 PM (7 years ago)
Author:
piccolo
Message:

1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof in place

Location:
src/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2824 r2843  
    190190match step with
    191191[ COST_LABEL c ⇒ [ ]
    192 | CALL id args dest ⇒ (f_call_args … functs args) @ (f_call_dest … functs dest)
     192| CALL id args dest ⇒
     193     let r_id ≝  match id with
     194                   [ inl _ ⇒ [ ]
     195                   | inr ptr ⇒ ((dpl_args … functs) (\fst ptr)) @
     196                                                 ((dph_args … functs) (\snd ptr))
     197                   ] in
     198    r_id @ (f_call_args … functs args) @ (f_call_dest … functs dest)
    193199| COND r lbl ⇒  acc_a_regs … functs r
    194200| step_seq s ⇒ get_used_registers_from_seq … functs s
  • src/joint/TranslateUtils.ma

    r2823 r2843  
    606606definition added_registers :
    607607  ∀p : graph_params.∀g.
    608   joint_internal_function p g → (label → option (list register)) → list register ≝
     608  joint_internal_function p g → (label → list register) → list register ≝
    609609  λp,g,def,f_regs.
    610   let f ≝ λlbl : label.λ_.λacc.
    611     match f_regs lbl with [ None ⇒ acc | Some regs ⇒ regs@acc ] in
     610  let f ≝ λlbl : label.λ_.λacc.(f_regs lbl)@acc in
    612611  foldi … f (joint_if_code p g def) [ ].
    613612
     
    615614  ∀p,g,def,f_regs.
    616615  ∀l,s.stmt_at … (joint_if_code … def) l = Some ? s →
    617   opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l).
     616  (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs)) (f_regs l)).
    618617
    619618(*(* translation without register allocation (more or less an alias) *)
  • src/joint/semanticsUtils.ma

    r2816 r2843  
    633633| % [2: % [2: % [% %]] | skip] @(multi_fetch_ok … H3 … EQstmt_at) ]
    634634qed.
     635
     636lemma b_graph_transform_program_fetch_statement_plus :
     637 ∀src,dst:sem_graph_params.
     638 ∀data : ∀globals.joint_closed_internal_function src globals →
     639  bound_b_graph_translate_data src dst globals.
     640 ∀prog_in : joint_program src.
     641 ∀init_regs : block → list register.
     642 ∀f_lbls : block → label → list label.
     643 ∀f_regs : block → label → list register.
     644 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
     645 let prog_out ≝ b_graph_transform_program … data prog_in in
     646 let src_genv ≝ globalenv_noinit ? prog_in in
     647 let dst_genv ≝ globalenv_noinit ? prog_out in
     648 ∀pc,id,def_in,s.
     649 fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
     650 ∃init_data,def_out.
     651 let bl ≝ pc_block pc in
     652 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
     653 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
     654 let l ≝ point_of_pc dst pc in
     655 ∃lbls,regs.
     656 f_lbls bl l = lbls ∧
     657 f_regs bl l = regs ∧
     658 joint_if_entry … def_out = joint_if_entry … def_in ∧
     659 partial_partition … (f_lbls bl) ∧
     660 partial_partition … (f_regs bl) ∧
     661 (∀l.All …
     662    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
     663           fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls bl l)) ∧
     664  (∀l.All …
     665    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
     666           fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs bl l)) ∧
     667  match s with
     668  [ sequential s' nxt ⇒
     669    let block ≝
     670      if eq_identifier … (joint_if_entry … def_in) l then
     671        append_seq_list … (f_step … init_data l s') (added_prologue … init_data)
     672      else
     673        f_step … init_data l s' in
     674    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
     675  | final s' ⇒
     676    l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
     677  | FCOND abs _ _ _ ⇒ Ⓧabs
     678  ].
     679#src #dst #data #prog_in
     680#init_regs #f_lbls #f_regs #props
     681#pc #id #def_in #s
     682#H @('bind_inversion H) * #id' #def_in' -H
     683#EQfif
     684#H @('bind_inversion H) -H #s
     685#H lapply (opt_eq_from_res ???? H) -H
     686#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
     687cases (b_graph_transform_program_fetch_internal_function … props … EQfif)
     688#a * #b ** #H1 #H2 #H3 %{a} %{b} %
     689[ %{H1 H2}
     690| %
     691   [2:
     692      %
     693        [2: %
     694            [%
     695               [%
     696                  [%
     697                     [%
     698                        [%
     699                           [%
     700                              %
     701                            | @(entry_eq … H3)
     702                            ]
     703                        | @(partition_lbls … H3)
     704                        ]
     705                     |  @(partition_regs … H3)
     706                     ]
     707                  | @(freshness_lbls … H3)
     708                  ]
     709               |  @(freshness_regs … H3)
     710               ]
     711            |  @(multi_fetch_ok … H3 … EQstmt_at)
     712            ]
     713        |
     714        ]
     715   |
     716   ]
     717]         
     718qed.
Note: See TracChangeset for help on using the changeset viewer.