Changeset 2876


Ignore:
Timestamp:
Mar 15, 2013, 10:58:03 AM (4 years ago)
Author:
tranquil
Message:

corrected another endianess bug in joint_semantics. Switched some names in RTLToERTL.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL.ma

    r2862 r2876  
    106106  save_return … (map … (Reg ?) ret_regs) @
    107107  restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @
    108   [ PUSH ERTL ? srah ;
    109     PUSH … sral ;
     108  [ PUSH ERTL ? sral ;
     109    PUSH … srah ;
    110110    ertl_del_frame ] @
    111111  assign_result globals.
     
    135135  λglobals,params,sral,srah,tmpr,addr1,addr2,sregs.
    136136  [ (ertl_new_frame : joint_seq ??) ;
    137     POP … sral ;
    138     POP … srah
     137    POP … srah ;
     138    POP … sral
    139139  ] @ save_hdws … sregs @ get_params … tmpr addr1 addr2 params.
    140140
  • src/joint/joint_semantics.ma

    r2821 r2876  
    55include "joint/Joint.ma".
    66include "ASM/I8051bis.ma".
    7 include "common/extraGlobalenvs.ma". 
     7include "common/extraGlobalenvs.ma".
    88
    99(* CSC: external functions never fail (??) and always return something of the
     
    2929 ; empty_framesT: framesT
    3030 ; regsT : Type[0]
     31 (* empty_regsT called at the start of each function call *)
    3132 ; empty_regsT: xpointer → regsT (* initial stack pointer *)
    3233 ; load_sp : regsT → res xpointer
     
    5859 ; carry: bebit
    5960 ; regs: regsT semp
     61 ; stack_usage : ℕ
    6062 ; m: bemem
    6163 }.
     
    7880
    7981definition set_m: ∀p. bemem → state p → state p ≝
    80  λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m.
     82 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st)
     83  (stack_usage … st) m.
    8184
    8285definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
    83  λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st).
     86 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs
     87  (stack_usage … st) (m … st).
    8488
    8589definition set_sp: ∀p. ? → state p → state p ≝
    8690 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
    87  mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st).
     91 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (stack_usage … st) (m … st).
    8892
    8993definition set_carry: ∀p. bebit → state p → state p ≝
    90  λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st).
     94 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st)
     95 (stack_usage … st) (m … st).
    9196
    9297definition set_istack: ∀p. internal_stack → state p → state p ≝
    93  λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st).
     98 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st)
     99 (stack_usage … st)  (m … st).
    94100
    95101definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     
    103109
    104110definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    105  λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st).
     111 λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st)
     112 (stack_usage … st) (m … st).
    106113
    107114(*
     
    263270  ! 〈addrh, st'〉 ← pop … st;
    264271  ! 〈addrl, st''〉 ← pop … st';
    265   ! pr ← pc_of_bevals [addrh; addrl];
     272  ! pr ← pc_of_bevals [addrl; addrh];
    266273  return 〈st'',pr〉.
    267274
     
    512519      set_result … p vs dest st.
    513520
     521definition increment_stack_usage : ∀p.ℕ → state p → state p ≝
     522λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st)
     523  (stack_usage … st + n) (m … st).
     524
     525definition decrement_stack_usage : ∀p.ℕ → state p → state p ≝
     526λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st)
     527  (stack_usage … st - n) (m … st).
     528
    514529definition eval_internal_call ≝
    515530λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
    516531λst : state p.
    517532! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
    518 setup_call … stack_size (joint_if_params … globals fn) args st.
     533! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
     534return increment_stack_usage … stack_size st'.
    519535
    520536definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
    521 
    522537
    523538definition eval_call ≝
     
    556571λst : state p.
    557572! st' ← pop_frame … ge curr_id curr_ret st ;
     573! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_id] (stack_sizes … ge curr_id) ;
     574let st'' ≝ decrement_stack_usage … stack_size (\fst st') in
    558575! nxt ← next_of_call_pc … ge (\snd … st') ;
    559576return
    560   next … nxt (set_last_pop … (\snd … st') st') (* now address pushed on stack are calling ones! *).
     577  next … nxt (set_last_pop … (\snd … st') 〈st'', \snd st'〉) (* now address pushed on stack are calling ones! *).
    561578
    562579definition eval_tailcall ≝
     
    568585match fd with
    569586[ Internal ifd ⇒
    570   ! st' ← eval_internal_call p globals ge i ifd args st ;
     587  ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_f] (stack_sizes … ge curr_f) ;
     588  let st' ≝ decrement_stack_usage … stack_size st in
     589  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
    571590  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
    572   return mk_state_pc … st' pc (last_pop … st)
     591  return mk_state_pc … st'' pc (last_pop … st)
    573592| External efd ⇒
    574593  ! st' ← eval_external_call … efd args curr_ret st ;
Note: See TracChangeset for help on using the changeset viewer.