Ignore:
Timestamp:
Mar 6, 2013, 12:09:52 PM (7 years ago)
Author:
piccolo
Message:

modified joint_closed_internal_function definition (added condition on pseudo-registers)
added new record for parameters
modified state definition with option for framesT

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_semantics.ma

    r2674 r2783  
    3737definition ERTL_state : sem_state_params ≝
    3838  mk_sem_state_params
    39  (* framesT ≝ *) (list (register_env beval × ident))
     39 (* framesT ≝ *) (list (register_env beval × (Σb:block.block_region b=Code)))
    4040 (* empty_framesT ≝ *) [ ]
    4141 (* regsT ≝ *) ertl_reg_env
     
    6464  〈 add … (\fst lenv) reg BVundef, \snd lenv〉.
    6565
     66(* TODO move into ErrorMessage *)
     67axiom FramesEmptyOnPop : ErrorMessage.
     68axiom BlockInFramesCorrupted : ErrorMessage.
     69axiom FrameErrorOnPush : ErrorMessage.
     70axiom FrameErrorOnPop : ErrorMessage.
    6671
    6772definition ertl_save_frame:
    68  call_kind → unit → ident → state_pc ERTL_state → res (state … ERTL_state) ≝
    69  λ_.λ_.λid.λst.
    70   do st ← push_ra … st (pc … st) ;
    71   OK …
    72    (set_frms ERTL_state (〈\fst (regs ERTL_state st),id〉 :: (st_frms … st))
    73     (set_regs ERTL_state 〈empty_map …,\snd (regs … st)〉 st)).
     73 call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
     74 λ_.λ_.λst.
     75  ! st' ← push_ra … st (pc … st) ;
     76  ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st);
     77  return
     78  (set_frms ERTL_state
     79  (〈\fst (regs ERTL_state st'),(pc_block (pc ? st))〉 :: frms)
     80    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
     81
     82
     83definition ertl_pop_frame:
     84 state ERTL_state →
     85   res (state ERTL_state × program_counter) ≝
     86 λst.
     87 ! frms ← opt_to_res ? [MSG FrameErrorOnPop] (st_frms … st);
     88 match frms with
     89 [ nil ⇒ Error ? [MSG FramesEmptyOnPop]
     90 | cons hd tl ⇒
     91   let 〈local_mem, bl〉 ≝ hd in
     92   let st' ≝ set_regs ERTL_state 〈local_mem, \snd (regs … st)〉
     93      (set_frms ERTL_state tl st) in
     94   ! 〈st'', pc〉 ← pop_ra … st' ;
     95   if eq_block bl (pc_block pc) then
     96     OK … 〈st'', pc〉
     97   else Error ? [MSG BlockInFramesCorrupted]
     98 ].
    7499
    75100(*CSC: XXXX, for external functions only*)
     
    85110  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
    86111
    87 axiom FunctionNotFound: errmsg.
    88 
    89112(*CSC: here we should use helper_def_store from Joint/semantics.ma,
    90113  but it is not visible *)
     
    95118  ! env' ← ps_reg_store dst v env ;
    96119  return set_regs ERTL_state env' st.
     120
     121axiom FunctionNotFound : errmsg.
    97122
    98123definition eval_ertl_seq:
     
    141166     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    142167  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertl_seq F gl ge stm id)
    143   (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …).
     168  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame).
    144169
    145170definition ERTL_semantics ≝
Note: See TracChangeset for help on using the changeset viewer.