Changeset 1327 for src/ERTL/semantics.ma

Timestamp:

Oct 7, 2011, 4:15:42 PM (10 years ago)

Author:

sacerdot

Message:

More progress in the implementation of the ERTL specific statements.
The file does not compile ATM because of unimplemented addr_sub and addr_add.

File:

• src/ERTL/semantics.ma (modified) (1 diff)

src/ERTL/semantics.ma

@@ -65 +65 @@
 axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).
 
-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)).
+(*CSC: XXXX *)
+axiom framesize: list ident → state ertl_sem_params → res nat. (* ≝
+  λglobals: list ident.
+  λst.
+   do f ← fetch_function globals st ;
+   OK ? (joint_if_stacksize globals … f).*)
+
+definition get_hwsp : state ertl_sem_params → res address ≝
+ λst.
+  do spl ← hwreg_retrieve (\snd (regs … st)) RegisterSPL ;
+  do sph ← hwreg_retrieve (\snd (regs … st)) RegisterSPH ;
+  OK ? 〈spl,sph〉.
+
+definition set_hwsp : address → state ertl_sem_params → res (state ertl_sem_params) ≝
+ λsp,st.
+  let 〈spl,sph〉 ≝ sp in
+  do hwregs ← hwreg_store RegisterSPL spl (\snd (regs … st)) ;
+  do hwregs ← hwreg_store RegisterSPH sph hwregs ;
+  OK ? (set_regs ertl_sem_params 〈\fst (regs … st),hwregs〉 st).
+
+definition 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)) ≝
+ λglobals,ge,stm,l,st.
+  match stm with
+   [ ertl_st_ext_new_frame ⇒
+      ! v ← framesize globals st;
+      ! sp ← get_hwsp st;
+        let newsp ≝ ?(*addr_sub sp v*) in
+      ! st ← set_hwsp newsp st;
+        ret ? 〈E0,goto … l st〉
+   | ertl_st_ext_del_frame ⇒
+      ! v ← framesize globals st;
+      ! sp ← get_hwsp st;
+        let newsp ≝ ?(*addr_add sp v*) in
+      ! st ← set_hwsp newsp st;
+        ret ? 〈E0,goto … l st〉
+   | ertl_st_ext_frame_size dst ⇒
+      ! v ← framesize globals st;
+      ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st;
+        ret ? 〈E0, goto … l st〉
+   ].
+qed.
 
 definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝