Changeset 1118


Ignore:
Timestamp:
Aug 26, 2011, 7:08:07 PM (8 years ago)
Author:
sacerdot
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1117 r1118  
    1818(* CSC: I have a byte, I need a value, but it is complex to do so *)
    1919axiom val_of_Byte: Byte → val.
     20(* Map from the front-end memory model to the back-end memory model *)
     21axiom represent_block: block → val × val.
    2022(* CSC: fixed size chunk *)
    2123axiom chunk: memory_chunk.
     
    170172      ! locals ← reg_store dst v' (locals f);
    171173      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉 *)
     174
    172175  (* CSC: Removed: St_jumptable *)
    173176  (* CSC: Added: *)
    174   | rtl_st_addr ldest hdest id l ⇒ ?
    175   | rtl_st_stack_addr ldest hdest l ⇒ ?
    176   (* CSC: St_const splitted into rtl_st_int *)
     177 
     178  (* CSC: St_const splitted into rtl_st_int, rtl_st_addr and rt_st_stack_addr; *)
     179  | rtl_st_addr ldest hdest id l ⇒
     180     ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
     181     let 〈laddr,haddr〉 ≝ represent_block addr in
     182     ! locals ← reg_store ldest laddr (locals f);
     183     ! locals ← reg_store hdest haddr locals;
     184     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
     185  | rtl_st_stack_addr ldest hdest l ⇒
     186     let 〈laddr,haddr〉 ≝ represent_block (sp f) in
     187     ! locals ← reg_store ldest laddr (locals f);
     188     ! locals ← reg_store hdest haddr locals;
     189     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
    177190  | rtl_st_int dest v l ⇒
    178191     ! locals ← reg_store dest (val_of_Byte v) (locals f);
    179192     ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉
     193     
    180194  | rtl_st_move dreg sreg l ⇒ ?
    181195  | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒ ?
Note: See TracChangeset for help on using the changeset viewer.