Changeset 1430 for src/joint


Ignore:
Timestamp:
Oct 20, 2011, 3:55:50 PM (8 years ago)
Author:
sacerdot
Message:

Bug fixed: push/pop must work on the isp (now added).
Note: the sp is used only in RTL and it is spurious in all other languages;

the isp is spurious in RTL.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1415 r1430  
    4747 ; pc: address
    4848 ; sp: pointer
     49 ; isp: pointer
    4950 ; carry: beval
    5051 ; regs: regsT ? p
     
    104105
    105106definition set_m: ∀p. bemem → state p → state p ≝
    106  λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.
     107 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) m.
    107108
    108109definition set_regs: ∀p:sem_params. regsT ? p → state p → state p ≝
    109  λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) regs (m … st).
     110 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) regs (m … st).
    110111
    111112definition set_sp: ∀p. pointer → state p → state p ≝
    112  λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (carry … st) (regs … st) (m … st).
     113 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (isp … st) (carry … st) (regs … st) (m … st).
     114
     115definition set_isp: ∀p. pointer → state p → state p ≝
     116 λp,isp,st. mk_state … (st_frms … st) (pc … st) (sp … st) isp (carry … st) (regs … st) (m … st).
    113117
    114118definition set_carry: ∀p. beval → state p → state p ≝
    115  λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) carry (regs … st) (m … st).
     119 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) (isp … st) carry (regs … st) (m … st).
    116120
    117121definition set_pc: ∀p. address → state p → state p ≝
    118  λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (carry … st) (regs … st) (m … st).
     122 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
    119123
    120124definition set_frms: ∀p:sem_params. framesT ? p → state p → state p ≝
    121  λp,frms,st. mk_state … frms (pc … st) (sp … st) (carry … st) (regs … st) (m … st).
     125 λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
    122126
    123127definition goto: ∀p:sem_params. label → state p → state p ≝
     
    178182definition push: ∀p. state p → beval → res (state p) ≝
    179183 λp,st,v.
    180   let sp ≝ sp … st in
    181   do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) sp v);
    182   let sp ≝ shift_pointer … sp [[false;false;false;false;false;false;false;true]] in
    183   OK … (set_m … m (set_sp … sp st)).
     184  let isp ≝ isp … st in
     185  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
     186  let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
     187  OK … (set_m … m (set_sp … isp st)).
    184188
    185189definition pop: ∀p. state p → res (state p × beval) ≝
    186190 λp,st.
    187   let sp ≝ sp ? st in
    188   let sp ≝ neg_shift_pointer ? sp [[false;false;false;false;false;false;false;true]] in
    189   let st ≝ set_sp … sp st in
    190   do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) sp);
     191  let isp ≝ isp ? st in
     192  let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
     193  let ist ≝ set_sp … isp st in
     194  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
    191195  OK ? 〈st,v〉.
    192196
     
    398402  let m ≝ init_mem Genv … p in
    399403  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
     404  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
    400405  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
    401406  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
     407  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
    402408  do sp ← address_of_pointer spp ;
    403409  let main ≝ prog_main … p in
    404   let st0 ≝ mk_state … (empty_framesT …) sp dummy_pc BVfalse (empty_regsT … sp) m in
     410  let st0 ≝ mk_state … (empty_framesT …) sp ispp dummy_pc BVfalse (empty_regsT … sp) m in
    405411  let trace_state ≝
    406412   eval_call_id … (mk_sem_params1 … (sparams …)) ge st0 main (call_args_for_main … (sparams …))
     
    411417  | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
    412418  ].
    413 [2: % | cases spb *; #r #off #E >E %]
     419[3: % | cases ispb | cases spb] *; #r #off #E >E %
    414420qed.
    415421(*
Note: See TracChangeset for help on using the changeset viewer.