Changeset 1118 for src/RTL

Timestamp:

Aug 26, 2011, 7:08:07 PM (10 years ago)

Author:

sacerdot

Message:

All derivatives of St_const implemented (up to axioms to match the two
memory models).

File:

• src/RTL/semantics.ma (modified) (2 diffs)

src/RTL/semantics.ma

@@ -18 +18 @@
 (* CSC: I have a byte, I need a value, but it is complex to do so *)
 axiom val_of_Byte: Byte → val.
+(* Map from the front-end memory model to the back-end memory model *)
+axiom represent_block: block → val × val.
 (* CSC: fixed size chunk *)
 axiom chunk: memory_chunk.
@@ -170 +172 @@
       ! locals ← reg_store dst v' (locals f);
       ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉 *)
+
   (* CSC: Removed: St_jumptable *)
   (* CSC: Added: *)
-  | rtl_st_addr ldest hdest id l ⇒ ?
-  | rtl_st_stack_addr ldest hdest l ⇒ ?
-  (* CSC: St_const splitted into rtl_st_int *)
+  
+  (* CSC: St_const splitted into rtl_st_int, rtl_st_addr and rt_st_stack_addr; *)
+  | rtl_st_addr ldest hdest id l ⇒
+     ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
+     let 〈laddr,haddr〉 ≝ represent_block addr in
+     ! locals ← reg_store ldest laddr (locals f);
+     ! locals ← reg_store hdest haddr locals;
+     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
+  | rtl_st_stack_addr ldest hdest l ⇒
+     let 〈laddr,haddr〉 ≝ represent_block (sp f) in
+     ! locals ← reg_store ldest laddr (locals f);
+     ! locals ← reg_store hdest haddr locals;
+     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
   | rtl_st_int dest v l ⇒
      ! locals ← reg_store dest (val_of_Byte v) (locals f);
      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
+     
   | rtl_st_move dreg sreg l ⇒ ?
   | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒ ?