Changeset 1294


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

RTL semantics: porting to joint semantics started.

Location:
src
Files:
2 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*)
  • src/joint/semantics.ma

    r1289 r1294  
    3434 ; dph_store_: dph_reg p → beval → regsT → res regsT
    3535 ; dph_retrieve_: regsT → dph_reg p → res beval
    36  ; pair_reg_move_: regsT → pair_reg p → regsT
     36 ; pair_reg_move_: regsT → pair_reg p → res regsT
    3737 
    3838 ; pointer_of_label: label → Σp:pointer. ptype p = Code
     
    6161 
    6262 ; fetch_statement: state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
     63 ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
     64
    6365 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
    6466 ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    65  ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
    6667
    6768 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams)))
     
    155156 λp,st,dst.dph_retrieve_ … (regs … st) dst.
    156157
    157 definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → state p ≝
    158  λp,st,rs.set_regs … (pair_reg_move_ … (regs … st) rs) st.
     158definition pair_reg_move: ∀p:sem_params. state p → pair_reg p → res (state p) ≝
     159 λp,st,rs.
     160  do regs ← pair_reg_move_ … (regs … st) rs;
     161  OK … (set_regs … regs st).
    159162
    160163definition save_frame: ∀p:sem_params. state p → state p ≝
     
    276279          ret ? 〈E0, next … l st〉
    277280      | MOVE dst_src ⇒
    278           ret ? 〈E0, next … l (pair_reg_move … st dst_src)〉
     281        ! st ← pair_reg_move … st dst_src ;
     282          ret ? 〈E0, next … l st〉
    279283      (*CSC: XXX bug here dest unused *)
    280284      | CALL_ID id argsno dest ⇒
Note: See TracChangeset for help on using the changeset viewer.