Changeset 3037


Ignore:
Timestamp:
Mar 29, 2013, 5:19:53 PM (4 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
Files:
15 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r2952 r3037  
    125125  on _s : ertl_seq to joint_seq ERTL ?.
    126126
    127 definition ERTL_premain : ∀p : ertl_program.joint_closed_internal_function ERTL (prog_var_names ?? p) ≝
     127definition ERTL_premain : ∀p : ertl_program.
     128  joint_closed_internal_function ERTL (prog_names … p) ≝
    128129λp.
    129130let l1 : label ≝ an_identifier … one in
     
    131132let l3 : label ≝ an_identifier … (p1 one) in
    132133let res ≝
    133   mk_joint_internal_function ERTL (prog_var_names … p)
     134  mk_joint_internal_function ERTL (prog_names … p)
    134135  (mk_universe … (p0 (p0 one)))
    135136  (mk_universe … one)
  • src/ERTL/ERTLToLTL.ma

    r3014 r3037  
    291291
    292292definition translate_address :
    293   ∀globals.nat → bool → ∀i.i ∈ globals → decision → decision →
     293  ∀globals.nat → bool → ∀i.i ∈ globals → Word → decision → decision →
    294294  list (joint_seq LTL globals) ≝
    295   λglobals,localss,carry_lives_after,id,prf,addr1,addr2.
     295  λglobals,localss,carry_lives_after,id,prf,off,addr1,addr2.
    296296  preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2))
    297     (ADDRESS LTL ? id prf it it ::
     297    (ADDRESS LTL ? id prf off it it ::
    298298     move ? localss false addr1 RegisterDPL @
    299299     move ? localss false addr2 RegisterDPH).
     
    356356        ] in
    357357      move dst src
    358     | ADDRESS lbl prf dpl dph ⇒
     358    | ADDRESS lbl prf off dpl dph ⇒
    359359      translate_address ? localss carry_lives_after
    360         lbl prf (lookup dpl) (lookup dph)
     360        lbl prf off (lookup dpl) (lookup dph)
    361361    | OPACCS op dst1 dst2 arg1 arg2 ⇒
    362362      translate_opaccs ? localss carry_lives_after op
     
    384384          λ_.PUSH LTL ? it;
    385385          λl.HIGH_ADDRESS l;
    386           λ_.PUSH LTL ? it],
     386          λ_.PUSH LTL ? it ;
     387          (* necessary as ptr CALL will be JMP A+DPTR *)
     388          λ_.A ← zero_byte ],
    387389         λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉
    388390      ]
  • src/ERTL/liveness.ma

    r3014 r3037  
    6161      | OP1 op1 r1 r2 ⇒ rl_psingleton r1
    6262      | POP r ⇒ rl_psingleton r
    63       | ADDRESS _ _ r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
     63      | ADDRESS _ _ _ r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
    6464      | LOAD r _ _ ⇒ rl_psingleton r
    6565      | COMMENT c ⇒ rl_bottom
     
    176176  | OP1 op1 r1 r2 ⇒
    177177    ¬set_member … (eq_identifier …) r1 pliveafter
    178   | ADDRESS _ _ r1 r2 ⇒
     178  | ADDRESS _ _ _ r1 r2 ⇒
    179179    ¬(set_member … (eq_identifier …) r1 pliveafter ∨
    180180      set_member … (eq_identifier …) r2 pliveafter)
  • src/ERTL/uses.ma

    r3014 r3037  
    4747         match s with
    4848         [ COMMENT _ ⇒ map
    49          | ADDRESS _ _ _ _ ⇒ map
     49         | ADDRESS _ _ _ _ _ ⇒ map
    5050         | CLEAR_CARRY ⇒ map
    5151         | SET_CARRY ⇒ map
  • src/LIN/LIN.ma

    r2952 r3037  
    2929unification hint 0 ≔ ⊢ lin_program ≡ joint_program LIN.
    3030
    31 definition LIN_premain : ∀p : lin_program.joint_closed_internal_function LIN (prog_var_names ?? p) ≝
     31definition LIN_premain : ∀p : lin_program.
     32  joint_closed_internal_function LIN (prog_names … p) ≝
    3233λp.
    3334let l3 : label ≝ an_identifier … (p1 one) in
     
    3637   〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 0 it) it〉 ;
    3738   〈Some ? l3, GOTO ? l3〉 ] in
    38 mk_joint_internal_function LIN (prog_var_names … p)
     39mk_joint_internal_function LIN (prog_names … p)
    3940  (mk_universe … (p0 (p0 one)))
    4041  (mk_universe … one)
  • src/LIN/joint_LTL_LIN_semantics.ma

    r3014 r3037  
    3838call_kind → unit → state_pc LTL_LIN_state → res(state LTL_LIN_state) ≝
    3939λk.λ_.λst. match k with
    40 [ PTR ⇒ return (st_no_pc … st)
     40[ PTR ⇒
     41  ! v ← Byte_of_val BadFunction
     42    (hwreg_retrieve (regs … st) RegisterA) ;
     43  if eq_bv … v (bv_zero …) then return (st_no_pc … st)
     44  else Error … [MSG BadFunction; MSG BadPointer]
    4145| ID ⇒ push_ra … st (pc … st)
    4246].
  • src/LTL/LTL.ma

    r2952 r3037  
    3434  hdw_argument_from_reg on _r : Register to snd_arg LTL.
    3535
    36 definition LTL_premain : ∀p : ltl_program.joint_closed_internal_function LTL (prog_var_names ?? p) ≝
     36definition LTL_premain : ∀p : ltl_program.
     37  joint_closed_internal_function LTL (prog_names … p) ≝
    3738λp.
    3839let l1 : label ≝ an_identifier … one in
     
    4041let l3 : label ≝ an_identifier … (p1 one) in
    4142let res ≝
    42   mk_joint_internal_function LTL (prog_var_names … p)
     43  mk_joint_internal_function LTL (prog_names … p)
    4344  (mk_universe … (p0 (p0 one)))
    4445  (mk_universe … one)
  • src/RTL/RTL.ma

    r2975 r3037  
    9393
    9494(* parameters for main need to be passed to the premain *)
    95 definition RTL_premain : ∀p : rtl_program.joint_closed_internal_function RTL (prog_var_names ?? p) ≝
     95definition RTL_premain : ∀p : rtl_program.
     96  joint_closed_internal_function RTL (prog_names … p) ≝
    9697λp.
    9798let l1 : label ≝ an_identifier … one in
     
    104105    an_identifier … (p0 (p0 one)) ] in
    105106let res ≝
    106   mk_joint_internal_function RTL (prog_var_names … p)
     107  mk_joint_internal_function RTL (prog_names … p)
    107108  (mk_universe … (p0 (p0 one)))
    108109  (mk_universe … (p1 (p0 one)))
  • src/RTL/RTLToERTL.ma

    r2876 r3037  
    226226    | POP _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
    227227    | MOVE rs ⇒ [PSD (\fst rs) ← \snd rs]
    228     | ADDRESS x prf r1 r2 ⇒
    229       [ADDRESS ERTL ? x prf r1 r2]
     228    | ADDRESS x prf off r1 r2 ⇒
     229      [ADDRESS ERTL ? x prf off r1 r2]
    230230    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
    231231      [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
  • src/RTLabs/RTLabsToRTL.ma

    r3004 r3037  
    327327  | Oaddrsymbol id offset ⇒ λcst_prf,prf.
    328328    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    329     ADDRESS RTL globals id ? r1 r2 ::
    330     if eqb offset 0 then [ ] else
    331     translate_op … Add
    332       [r1 ; r2 ] [ r1 ; r2 ] [ byte_of_nat … offset ; zero_byte ]
    333       (refl …) (refl …)
     329    let off ≝ bitvector_of_nat 16 offset in
     330    [ ADDRESS RTL globals id ? off r1 r2 ]
    334331  | Oaddrstack offset ⇒ λcst_prf,prf.
    335332    let 〈r1, r2〉 ≝ make_addr … destrs ? in
     
    11091106 λinit_cost, p.
    11101107  mk_joint_program …
    1111     (transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)))
    1112     init_cost.
     1108    (prog_funct_names \ldots p)
     1109    (transform_program … p (λvarnames. transf_fundef … (translate_internal ?)))
     1110    init_cost
     1111    ?.
     1112@hide_prf @transform_prog_funct_names qed.
  • 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.