Changeset 2214 for src/RTLabs


Ignore:
Timestamp:
Jul 19, 2012, 2:42:02 PM (7 years ago)
Author:
tranquil
Message:
  • changed order of parameters of joint_internal_function and genv in semantics
  • in semantics, unified more_sem_unserialized_params and more_sem_genv_params
  • renamed all <language>_params to <LANGUAGE>
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r2208 r2214  
    133133  ∀srcrs2 : list psd_argument.
    134134  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
    135   list (joint_seq rtl_params globals)
     135  list (joint_seq RTL globals)
    136136  ≝
    137137  λglobals: list ident.
     
    146146  | Sub ⇒ [CLEAR_CARRY ??]
    147147  | _ ⇒ [ ]
    148   ] @ map3 ???? (OP2 rtl_params globals op) destrs srcrs1 srcrs2 prf1 prf2.
     148  ] @ map3 ???? (OP2 RTL globals op) destrs srcrs1 srcrs2 prf1 prf2.
    149149
    150150let rec nat_to_args (size : nat) (k : nat) on size : Σl : list psd_argument.|l| = size ≝
     
    174174  ∀destrs: list register.
    175175  |destrs| = size_of_cst ? cst_sig →
    176   list (joint_seq rtl_params globals)
     176  list (joint_seq RTL globals)
    177177 ≝
    178178  λty,globals,cst_sig,destrs.
     
    186186  | Oaddrsymbol id offset ⇒ λcst_prf,prf.
    187187    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    188     [ADDRESS rtl_params globals id ? r1 r2]
     188    [ADDRESS RTL globals id ? r1 r2]
    189189  | Oaddrstack offset ⇒ λcst_prf,prf.
    190190    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    191     [(rtl_stack_address r1 r2 : joint_seq rtl_params globals)]
     191    [(rtl_stack_address r1 r2 : joint_seq RTL globals)]
    192192  ] (pi2 … cst_sig).
    193193  [2: cases not_implemented
     
    203203  ∀destrs: list register.
    204204  ∀srcrs: list psd_argument.
    205   |destrs| = |srcrs| → list (joint_seq rtl_params globals) ≝
     205  |destrs| = |srcrs| → list (joint_seq RTL globals) ≝
    206206  λglobals,destrs,srcrs,length_eq.
    207207  map2 … (λdst,src.dst ← src) destrs srcrs length_eq.
     
    216216
    217217definition sign_mask : ∀globals.register → register →
    218   list (joint_seq rtl_params globals) ≝
     218  list (joint_seq RTL globals) ≝
    219219    (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that:
    220220       byte in destr if srcr is: neg   |  pos
     
    234234  ∀globals : list ident.
    235235  list register → register →
    236   bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     236  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    237237  λglobals,destrs,srcr.
    238238  ν tmp in
     
    242242definition translate_fill_with_zero :
    243243  ∀globals : list ident.
    244   list register → list (joint_seq rtl_params globals) ≝
     244  list register → list (joint_seq RTL globals) ≝
    245245  λglobals,destrs.
    246246  match nat_to_args (|destrs|) 0 with
     
    270270  ∀globals: list ident.
    271271  signedness → list register → list register →
    272     bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     272    bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    273273  λglobals,src_sign,destrs,srcrs.
    274274  match reduce_strong ?? destrs srcrs with
     
    299299  ∀destrs : list register.
    300300  ∀srcrs_arg : list register.
    301   |destrs| = |srcrs_arg| → list (joint_seq rtl_params globals) ≝
     301  |destrs| = |srcrs_arg| → list (joint_seq RTL globals) ≝
    302302  λglobals, destrs, srcrs, prf.
    303   map2 ??? (OP1 rtl_params globals Cmpl) destrs srcrs prf.
    304 
    305 definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     303  map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf.
     304
     305definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    306306  λglobals: list ident.
    307307  λdestrs: list register.
     
    318318  ∀globals : list ident.
    319319  list register → list register →
    320     bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     320    bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    321321  λglobals,destrs,srcrs.
    322322  match destrs with
     
    328328    | cons srcr srcrs' ⇒
    329329      (destr ← srcr) :::
    330       map register (joint_seq rtl_params globals) (λr. destr ← destr .Or. r) srcrs' @@
     330      map register (joint_seq RTL globals) (λr. destr ← destr .Or. r) srcrs' @@
    331331      (* now destr is non-null iff srcrs was non-null *)
    332332      CLEAR_CARRY ?? :::
     
    341341
    342342definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? →
    343   bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     343  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    344344  λglobals.
    345345  λty, ty'.
     
    351351  match op1
    352352  return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' →
    353     bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) with
     353    bind_new (localsT RTL) (list (joint_seq RTL globals)) with
    354354  [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2.
    355355    translate_cast globals src_sign destrs srcrs
     
    410410  (Σi.i<S k) →
    411411  (* the accumulator *)
    412   list (joint_seq rtl_params globals) →
    413     list (joint_seq rtl_params globals) ≝
     412  list (joint_seq RTL globals) →
     413    list (joint_seq RTL globals) ≝
    414414  λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
    415415    tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
     
    456456] qed.
    457457
    458 definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     458definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    459459λglobals : list ident.
    460460λdestrs : list register.
     
    472472(* the step calculating all products with least significant byte going in the
    473473   k-th position of the result *)
    474 let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq rtl_params globals) →
    475   list (joint_seq rtl_params globals) ≝
     474let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq RTL globals) →
     475  list (joint_seq RTL globals) ≝
    476476  λk_sig,acc.match k_sig with
    477477  [ mk_Sig k k_prf ⇒
     
    496496
    497497definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→
    498     bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     498    bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    499499  λglobals: list ident.
    500500  λdiv_not_mod: bool.
     
    543543
    544544definition translate_ne: ∀globals: list ident.?→?→?→?→
    545   bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     545  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    546546  λglobals: list ident.
    547547  λdestrs: list register.
     
    559559      | cons srcr2 srcrs2' ⇒ λEQ.
    560560        νtmpr in
    561         let f : psd_argument → psd_argument → list (joint_seq rtl_params globals) → list (joint_seq rtl_params globals) ≝
     561        let f : psd_argument → psd_argument → list (joint_seq RTL globals) → list (joint_seq RTL globals) ≝
    562562          λs1,s2,acc.
    563563          tmpr  ← s1 .Xor. s2 ::
    564564          destr ← destr .Or. tmpr ::
    565565          acc in
    566         let epilogue : list (joint_seq rtl_params globals) ≝
     566        let epilogue : list (joint_seq RTL globals) ≝
    567567          [ CLEAR_CARRY ?? ;
    568568            tmpr ← zero_byte .Sub. destr ;
     
    577577(* if destrs is 0 or 1, it inverses it. To be used after operations that
    578578   ensure this. *)
    579 definition translate_toggle_bool : ∀globals.?→list (joint_seq rtl_params globals) ≝
     579definition translate_toggle_bool : ∀globals.?→list (joint_seq RTL globals) ≝
    580580  λglobals: list ident.
    581581  λdestrs: list register.
     
    591591  ∀srcrs2: list psd_argument.
    592592  |srcrs1| = |srcrs2| →
    593   bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     593  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    594594  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
    595595  match destrs with
     
    609609  (tmp : register)
    610610  (srcrs : list psd_argument) on srcrs :
    611   Σt : (list psd_argument) × (list (joint_seq rtl_params globals)).|\fst t| = |srcrs| ≝
     611  Σt : (list psd_argument) × (list (joint_seq RTL globals)).|\fst t| = |srcrs| ≝
    612612  let byte_128 : Byte ≝ true ::: bv_zero ? in
    613613  match srcrs with
     
    631631  ∀srcrs2: list psd_argument.
    632632  |srcrs1| = |srcrs2| →
    633   bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     633  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    634634  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
    635635  νtmp_last_s1 in
     
    649649qed.
    650650
    651 definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     651definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    652652  λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs_prf.
    653653  if is_unsigned then
     
    684684  |srcrs1| = size_of_sig_type ty1 →
    685685  |srcrs2| = size_of_sig_type ty2 →
    686   bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     686  bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝
    687687  λglobals,ty1,ty2,ty3,op2,destrs,srcrs1,srcrs2.
    688688  match op2 return λty1,ty2,ty3.λx : binary_operation ty1 ty2 ty3.
     
    728728
    729729definition translate_cond: ∀globals: list ident. list register → label →
    730   bind_seq_block rtl_params globals (joint_step rtl_params globals) ≝
     730  bind_seq_block RTL globals (joint_step RTL globals) ≝
    731731  λglobals: list ident.
    732732  λsrcrs: list register.
    733733  λlbl_true: label.
    734   match srcrs return λ_.bind_seq_block rtl_params ? (joint_step ??) with
     734  match srcrs return λ_.bind_seq_block RTL ? (joint_step ??) with
    735735  [ nil ⇒ bret … 〈[ ], NOOP ??〉
    736736  | cons srcr srcrs' ⇒
    737737    ν tmpr in
    738     let f : register → joint_seq rtl_params globals ≝
     738    let f : register → joint_seq RTL globals ≝
    739739      λr. tmpr ← tmpr .Or. r in
    740     bret … 〈MOVE rtl_params globals 〈tmpr,srcr〉 ::
     740    bret … 〈MOVE RTL globals 〈tmpr,srcr〉 ::
    741741    map ?? f srcrs', (COND … tmpr lbl_true : joint_step ??) 〉
    742742  ].
    743743
    744744(* Paolo: to be controlled (original seemed overly complex) *)
    745 definition translate_load : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝
     745definition translate_load : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝
    746746  λglobals: list ident.
    747747  λaddr : list psd_argument.
     
    750750  ν tmp_addr_l in
    751751  ν tmp_addr_h in
    752   let f ≝ λdestr : register.λacc : list (joint_seq rtl_params globals).
    753     LOAD rtl_params globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) ::
     752  let f ≝ λdestr : register.λacc : list (joint_seq RTL globals).
     753    LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) ::
    754754    translate_op ? Add
    755755      [tmp_addr_l ; tmp_addr_h]
     
    761761] // qed.
    762762 
    763 definition translate_store : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝
     763definition translate_store : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝
    764764  λglobals: list ident.
    765765  λaddr : list psd_argument.
     
    768768  ν tmp_addr_l in
    769769  ν tmp_addr_h in
    770   let f ≝ λsrcr : psd_argument.λacc : list (joint_seq rtl_params globals).
    771     STORE rtl_params globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr ::
     770  let f ≝ λsrcr : psd_argument.λacc : list (joint_seq RTL globals).
     771    STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr ::
    772772    translate_op … Add
    773773      [tmp_addr_l ; tmp_addr_h]
     
    780780definition translate_statement : ∀globals.local_env → statement →
    781781  𝚺b :
    782   bind_seq_block rtl_params globals (joint_step rtl_params globals) +
    783   bind_seq_block rtl_params globals (joint_fin_step rtl_params).
     782  bind_seq_block RTL globals (joint_step RTL globals) +
     783  bind_seq_block RTL globals (joint_fin_step RTL).
    784784  if is_inl … b then label else unit ≝
    785785  λglobals,lenv,stmt.
     
    812812    ❬(match retr with
    813813      [ Some retr ⇒
    814         CALL_ID rtl_params ? f (rtl_args args lenv ?) (find_local_env retr lenv ?)
     814        CALL_ID RTL ? f (rtl_args args lenv ?) (find_local_env retr lenv ?)
    815815      | None ⇒
    816         CALL_ID rtl_params ? f (rtl_args args lenv ?) [ ]
     816        CALL_ID RTL ? f (rtl_args args lenv ?) [ ]
    817817      ] : bind_seq_block ???), lbl'❭
    818818  | St_call_ptr f args retr lbl' ⇒
     
    882882  let entry' ≝ f_entry def in
    883883  let exit' ≝ f_exit def in
    884   let graph' ≝ empty_map LabelTag (joint_statement rtl_params globals) in
     884  let graph' ≝ empty_map LabelTag (joint_statement RTL globals) in
    885885  let graph' ≝ add LabelTag ? graph' entry'
    886886    (GOTO … exit') in
     
    891891    b_adds_graph … (rtl_ertl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in
    892892  let res ≝
    893     mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'
     893    mk_joint_internal_function RTL globals luniverse' runiverse' result' params'
    894894     locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in
    895895    foldi … f_trans (f_graph def) res. 
Note: See TracChangeset for help on using the changeset viewer.