Changeset 3037 for src/joint


Ignore:
Timestamp:
Mar 29, 2013, 5:19:53 PM (7 years ago)
Author:
tranquil
Message:
  • ADDRESS joint instruction now has also an offset
  • corrected call to pointer (needed to clear the accumulator)
  • now we make sure globals contain also function names

LINToASM will be fixed in an upcoming commit

Location:
src/joint
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2946 r3037  
    119119  | POP: acc_a_reg p → joint_seq p globals
    120120  | PUSH: acc_a_arg p → joint_seq p globals
    121   | ADDRESS: ∀i: ident. i ∈ globals → dpl_reg p → dph_reg p → joint_seq p globals
     121  | ADDRESS: ∀i: ident. i ∈ globals → Word → dpl_reg p → dph_reg p → joint_seq p globals
    122122  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
    123123  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
     
    139139| POP r ⇒ acc_a_regs … functs r
    140140| PUSH r ⇒ acc_a_args … functs r
    141 | ADDRESS i prf r1 r2 ⇒ (dpl_regs … functs r1) @ (dph_regs … functs r2)
     141| ADDRESS _ _ _ r1 r2 ⇒ (dpl_regs … functs r1) @ (dph_regs … functs r2)
    142142| OPACCS o r1 r2 r3 r4 ⇒ (acc_a_regs … functs r1) @ (acc_b_regs … functs r2)
    143143       @ (acc_a_args … functs r3) @ (acc_b_args … functs r4)
     
    592592     (*(pi1 … (joint_if_exit … p))*).
    593593
    594 definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
     594definition joint_function ≝ λp,functions,globals.
     595  fundef (joint_closed_internal_function p (globals @ functions)).
    595596
    596597record joint_program (p : params) : Type[0] ≝
    597 { joint_prog :> program (joint_function p) (list init_data)
     598{ jp_functions : list ident
     599; joint_prog :> program (joint_function p jp_functions) (list init_data)
    598600; init_cost_label : costlabel
    599601(* here we can have global invariants (like injectivity of cost labels) *)
     602; functions_ok : (prog_funct_names … joint_prog) = jp_functions
    600603}.
     604
     605definition prog_names ≝ λpars.λp : joint_program pars.
     606  prog_var_names … p @ jp_functions … p.
     607
     608lemma transform_prog_funct_names : ∀A,B,V.∀p : program A V.
     609∀trans: ∀vars.A vars → B vars.
     610prog_funct_names … (transform_program A B V p trans) =
     611prog_funct_names … p.
     612#A #B #V * #vars #functs #main #trans elim functs //
     613* #id #f #tl #IH whd in ⊢ (??%%); @eq_f @IH qed.
     614
     615definition transform_joint_program :
     616 ∀src,dst : params.
     617 (∀globals.joint_closed_internal_function src globals →
     618  joint_closed_internal_function dst globals) →
     619 joint_program src → joint_program dst ≝
     620 λsrc,dst,trans,prog_in.
     621 mk_joint_program dst
     622  (jp_functions … prog_in)
     623  (transform_program … prog_in (λvars.transf_fundef … (trans ?)))
     624  (init_cost_label … prog_in)
     625  ?.
     626@hide_prf
     627>transform_prog_funct_names @functions_ok qed.
    601628
    602629(* The cost model for stack consumption *)
  • src/joint/TranslateUtils.ma

    r2980 r3037  
    621621  joint_program src_g_pars →
    622622  joint_program dst_g_pars ≝
    623   λsrc,dst,init,p.
    624   mk_joint_program ?
    625     (transform_program ??? p
    626       (λvarnames.transf_fundef ?? (λdef_in.
    627         b_graph_translate … (init varnames def_in) def_in)))
    628     (init_cost_label … p).
     623  λsrc,dst,init.
     624  transform_joint_program …
     625        (λvarnames,def_in.b_graph_translate … (init varnames def_in) … def_in).
    629626
    630627definition added_registers :
  • src/joint/joint_semantics.ma

    r2954 r3037  
    1313
    1414(* Paolo: I'll put in this record the property about genv we need *)
    15 record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝
     15record genv_gen (F : list ident → Type[0])
     16  (globals : list ident) : Type[0] ≝
    1617{ ge :> genv_t (fundef (F globals))
    1718; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ?
     
    7778
    7879definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
    79 coercion genv_to_genv_t :
    80   ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝
    81   λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?.
     80unification hint 0 ≔ p, globals ⊢
     81genv p globals ≡ genv_gen (joint_closed_internal_function p) globals.
    8282
    8383record sem_state_params : Type[1] ≝
     
    314314record sem_params : Type[1] ≝
    315315  { spp' :> serialized_params
    316   ; pre_main_generator : ∀p : joint_program spp'.joint_closed_internal_function spp' (prog_var_names … p)
     316  ; pre_main_generator : ∀p : joint_program spp'.joint_closed_internal_function spp' (prog_names … p)
    317317  }.
    318318
     
    467467    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    468468    return set_m … m' st
    469   | ADDRESS id prf ldest hdest ⇒
     469  | ADDRESS id prf off ldest hdest ⇒
     470    (* to be changed when globals will be already in stack? *)
    470471    let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in
    471     let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in
     472    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block (mk_offset off)) in
    472473    ! st' ← dpl_store … ldest laddr st;
    473474    dph_store … hdest haddr st'
     
    511512
    512513definition block_of_call ≝ λp : sem_params.
    513   λglobals.λge: genv_t (joint_function p globals).λf.λst : state p.
     514  λglobals.λge: genv p globals.
     515    λf.λst : state p.
    514516  ! bl ← match f with
    515517    [ inl id ⇒
  • src/joint/linearise.ma

    r2950 r3037  
    887887   ≝
    888888  λp,pr.(*transform_program ??? pr*)
    889    mk_joint_program ?
    890     (transform_program ??? pr
    891      (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))))
    892     (init_cost_label ? pr).
     889   transform_joint_program … (λglobals,f_in.\fst (linearise_int_fun p globals f_in)) pr.
    893890   
    894891(*    mk_joint_program
  • src/joint/semanticsUtils.ma

    r2973 r3037  
    5959; graph_pre_main_generator :
    6060  ∀p : joint_program (mk_graph_params sgp_pars).
    61   joint_closed_internal_function (mk_graph_params sgp_pars) (prog_var_names … p)
     61  joint_closed_internal_function (mk_graph_params sgp_pars) (prog_names … p)
    6262}.
    6363
     
    103103; lin_pre_main_generator :
    104104  ∀p : joint_program (mk_lin_params slp_pars).
    105   joint_closed_internal_function (mk_lin_params slp_pars) (prog_var_names … p)
     105  joint_closed_internal_function (mk_lin_params slp_pars) (prog_names … p)
    106106}.
    107107
     
    235235{ symbols_eq : symbols … ge1 = symbols … ge2
    236236; nextfunction_eq : nextfunction … ge1 = nextfunction … ge2
    237 ; functions_match : pm_P (match_fundef M ?) (functions … ge1) (functions … ge2)
     237; functions_match : pm_P ?? (match_fundef M ?) (functions … ge1) (functions … ge2)
    238238}.
    239239
     
    402402definition joint_globalenv :
    403403  ∀p : sem_params.∀pr:joint_program p.
    404     (ident → option ℕ) → genv p (prog_var_names … pr) ≝
     404    (ident → option ℕ) → genv p (prog_names … pr) ≝
    405405λp,prog,stacksizes.
    406406let genv ≝ globalenv … (λx.x) prog in
     
    410410mk_genv_gen ?? genv ? stacksizes (pre_main_generator … p prog) pc_from_lbl.
    411411#s #H
    412 elim (find_symbol_exists ?? (λx.x) … prog s ?)
     412cases (find_symbol_exists ?? (λx.x) … prog s ?)
    413413[ #bl #EQ >EQ % #ABS destruct ]
    414 @Exists_append_r
    415 @(Exists_mp … H) @sym_eq
     414cases (Exists_append … H) -H #H
     415[ @Exists_append_r | @Exists_append_l ]
     416[ @(Exists_mp … H) @sym_eq ]
     417cases prog in H; #functs * #vars #functs' #main #init_cost
     418whd in match prog_funct_names; normalize nodelta #EQ
     419>map_ext_eq [ >EQ @Exists_mp @sym_eq | // ] skip
    416420qed.
    417421
     
    422426lemma fetch_function_transf:
    423427 ∀src,dst : sem_params.∀prog_in : joint_program src.
    424  ∀stacksizes.
    425  ∀trans : ∀vars.joint_function src vars → joint_function dst vars.
    426  let prog_out ≝
    427   mk_joint_program dst
    428     (transform_program … prog_in trans) (init_cost_label … prog_in) in
     428 ∀stacksizes,trans.
     429 let prog_out ≝ transform_joint_program src dst trans prog_in in
    429430 ∀bl.
    430431 fetch_function … (joint_globalenv … prog_out stacksizes) bl =
     
    433434 else
    434435   ! 〈id, f〉 ← fetch_function … (joint_globalenv … prog_in stacksizes) bl ;
    435    return 〈id, trans … f〉.
     436   return 〈id, transf_fundef ?? (trans ?) f〉.
    436437#src #dst #p #sizes #tf whd
    437 lapply (transform_program_match … tf p)
     438lapply (transform_program_match … (λvars.transf_fundef … (tf ?)) p)
    438439#MATCH
    439440whd in match fetch_function;
    440441whd in match joint_globalenv; normalize nodelta
    441442#bl @eqZb_elim #Hbl normalize nodelta [ % ]
     443whd in match transform_joint_program;
     444whd in match prog_names; normalize nodelta
    442445>symbol_for_block_transf
    443446>opt_to_res_bind >opt_to_res_bind in ⊢ (???%); >m_bind_bind
     
    457460lemma fetch_internal_function_transf :
    458461 ∀src,dst : sem_params.∀prog_in : joint_program src.
    459  ∀stacksizes.
    460  ∀trans : ∀vars.joint_closed_internal_function src vars → joint_closed_internal_function dst vars.
    461  let prog_out ≝
    462   mk_joint_program dst
    463     (transform_program … prog_in (λvars.transf_fundef … (trans vars))) (init_cost_label … prog_in) in
     462 ∀stacksizes,trans.
     463 let prog_out ≝ transform_joint_program src dst trans prog_in in
    464464 ∀bl.
    465465 fetch_internal_function … (joint_globalenv … prog_out stacksizes) bl =
     
    682682whd in match fetch_function; normalize nodelta
    683683>Hbl normalize nodelta
     684whd in match joint_globalenv; normalize nodelta
     685whd in match prog_names; normalize nodelta
    684686>symbol_for_block_transf >EQ1 >m_return_bind
    685687>H1 %
Note: See TracChangeset for help on using the changeset viewer.