Changeset 1327 for src/ERTL/semantics.ma
- Timestamp:
- Oct 7, 2011, 4:15:42 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/semantics.ma
r1324 r1327 65 65 axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params). 66 66 67 axiom ertl_exec_extended: ∀globals. genv globals (ertl_params globals) → ertl_statement_extension → label → state ertl_sem_params → IO io_out io_in (trace × (state ertl_sem_params)). 67 (*CSC: XXXX *) 68 axiom framesize: list ident → state ertl_sem_params → res nat. (* ≝ 69 λglobals: list ident. 70 λst. 71 do f ← fetch_function globals st ; 72 OK ? (joint_if_stacksize globals … f).*) 73 74 definition get_hwsp : state ertl_sem_params → res address ≝ 75 λst. 76 do spl ← hwreg_retrieve (\snd (regs … st)) RegisterSPL ; 77 do sph ← hwreg_retrieve (\snd (regs … st)) RegisterSPH ; 78 OK ? 〈spl,sph〉. 79 80 definition set_hwsp : address → state ertl_sem_params → res (state ertl_sem_params) ≝ 81 λsp,st. 82 let 〈spl,sph〉 ≝ sp in 83 do hwregs ← hwreg_store RegisterSPL spl (\snd (regs … st)) ; 84 do hwregs ← hwreg_store RegisterSPH sph hwregs ; 85 OK ? (set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st). 86 87 definition ertl_exec_extended: 88 ∀globals. genv globals (ertl_params globals) → 89 ertl_statement_extension → label → state ertl_sem_params → 90 IO io_out io_in (trace × (state ertl_sem_params)) ≝ 91 λglobals,ge,stm,l,st. 92 match stm with 93 [ ertl_st_ext_new_frame ⇒ 94 ! v ← framesize globals st; 95 ! sp ← get_hwsp st; 96 let newsp ≝ ?(*addr_sub sp v*) in 97 ! st ← set_hwsp newsp st; 98 ret ? 〈E0,goto … l st〉 99 | ertl_st_ext_del_frame ⇒ 100 ! v ← framesize globals st; 101 ! sp ← get_hwsp st; 102 let newsp ≝ ?(*addr_add sp v*) in 103 ! st ← set_hwsp newsp st; 104 ret ? 〈E0,goto … l st〉 105 | ertl_st_ext_frame_size dst ⇒ 106 ! v ← framesize globals st; 107 ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st; 108 ret ? 〈E0, goto … l st〉 109 ]. 110 qed. 68 111 69 112 definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
Note: See TracChangeset
for help on using the changeset viewer.