Changeset 1294 for src/RTL


Ignore:
Timestamp:
Oct 5, 2011, 3:19:40 PM (9 years ago)
Author:
sacerdot
Message:

RTL semantics: porting to joint semantics started.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1233 r1294  
    1 
    2 (* XXX NB: I haven't checked all of these semantics against the prototype
    3            compilers yet! *)
    4 
     1include "joint/semantics.ma".
     2(*
    53include "utilities/lists.ma".
    6 
    74include "common/Errors.ma".
    85include "common/Globalenvs.ma".
    96include "common/IO.ma".
    107include "common/SmallstepExec.ma".
    11 
     8*)
    129include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
    1310
     11(*CSC: XXXX *)
     12axiom rtl_succ_p: label → address → address.
     13axiom rtl_pointer_of_label: label → Σp:pointer. ptype p = Code.
     14
     15axiom rtl_pop_frame: unit → res unit.
     16axiom rtl_save_frame: unit → register_env beval → unit.
     17
     18
     19axiom BadRegister : String.
     20definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
     21definition reg_retrieve : register_env beval → register → res beval ≝
     22 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
     23
     24definition rtl_more_sem_params: more_sem_params rtl_params_ :=
     25 mk_more_sem_params rtl_params_
     26  unit(*framesT*) (register_env beval) rtl_succ_p rtl_pop_frame rtl_save_frame
     27   reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
     28    reg_store reg_retrieve reg_store reg_retrieve
     29     (λlocals,dest_src.
     30       do v ← reg_retrieve locals (\snd dest_src) ;
     31       reg_store (\fst dest_src) v locals)
     32     rtl_pointer_of_label.
     33definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
     34
     35(*CSC: XXXXX *)
     36axiom rtl_init_locals : list register → register_env beval.
     37axiom rtl_fetch_statement: ∀globals. state rtl_sem_params → res (rtl_statement globals).
     38axiom rtl_fetch_result: state rtl_sem_params → nat → res val.
     39
     40(*CSC: XXXX, for external functions only*)
     41axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val).
     42axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).
     43
     44axiom rtl_exec_extended: ∀globals. genv globals (rtl_params globals) → rtl_statement_extension → state rtl_sem_params → IO io_out io_in (trace × (state rtl_sem_params)).
     45
     46definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) :=
     47 λglobals.
     48  mk_more_sem_params2 … rtl_more_sem_params rtl_init_locals
     49   (rtl_fetch_statement …) rtl_fetch_result rtl_fetch_external_args rtl_set_result
     50    (rtl_exec_extended …).
     51
     52definition rtl_fullexec ≝
     53 joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)).
     54
     55(*
    1456(* CSC: external functions never fail (??) and always return something of the
    1557   size of one register, both in the frontend and in the backend.
     
    281323  mk_fullexec … RTL_exec ? make_initial_state.
    282324*)
     325*)
Note: See TracChangeset for help on using the changeset viewer.