Changeset 1302


Ignore:
Timestamp:
Oct 5, 2011, 11:36:03 PM (8 years ago)
Author:
sacerdot
Message:

ERTL/semantics.ma ported to joint/SemanticUtils (in progress)

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1221 r1302  
    1 
    2 (* XXX NB: I haven't checked all of these semantics against the prototype
    3            compilers yet! *)
    4 
    5 include "utilities/lists.ma".
    6 
    7 include "common/Errors.ma".
    8 include "common/Globalenvs.ma".
    9 include "common/IO.ma".
    10 include "common/SmallstepExec.ma".
    11 
     1include "joint/SemanticUtils.ma".
    122include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
    133
     4(*CSC: XXXXX *)
     5axiom ertl_init_locals : list register → (register_env beval) × hw_register_env.
     6axiom ertl_pop_frame: unit → res unit.
     7axiom ertl_save_frame: unit → (register_env beval) × hw_register_env → unit.
     8
     9definition ps_reg_store ≝
     10 λr,v.λlocal_env:(register_env beval) × hw_register_env.
     11  do res ← reg_store r v (\fst local_env) ;
     12  OK … 〈res, \snd local_env〉.
     13
     14definition ps_reg_retrieve ≝
     15 λlocal_env:(register_env beval) × hw_register_env. reg_retrieve … (\fst local_env).
     16
     17definition hw_reg_store ≝
     18 λr,v.λlocal_env:(register_env beval) × hw_register_env.
     19  do res ← hwreg_store r v (\snd local_env) ;
     20  OK … 〈\fst local_env,res〉.
     21
     22definition hw_reg_retrieve ≝
     23 λlocal_env:(register_env beval) × hw_register_env. hwreg_retrieve … (\snd local_env).
     24
     25definition ertl_more_sem_params: more_sem_params ertl_params_ :=
     26 mk_more_sem_params ertl_params_
     27  unit(*framesT*) ((register_env beval) × hw_register_env) graph_succ_p ertl_pop_frame ertl_save_frame
     28   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
     29    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
     30     (λlocals,dest_src.
     31       do v ←
     32        match \snd dest_src with
     33        [ pseudo reg ⇒ ps_reg_retrieve locals reg
     34        | hardware reg ⇒ hw_reg_retrieve locals reg] ;
     35       match \fst dest_src with
     36       [ pseudo reg ⇒ ps_reg_store reg v locals
     37       | hardware reg ⇒ hw_reg_store reg v locals])
     38     pointer_of_label.
     39definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params.
     40
     41(*CSC: XXXXX, for is_final only *)
     42axiom ertl_fetch_result: state ertl_sem_params → nat → res val.
     43
     44(*CSC: XXXX, for external functions only*)
     45axiom ertl_fetch_external_args: external_function → state ertl_sem_params → res (list val).
     46axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params).
     47
     48axiom ertl_exec_extended: ∀globals. genv globals (ertl_params globals) → ertl_statement_extension → state ertl_sem_params → IO io_out io_in (trace × (state ertl_sem_params)).
     49
     50definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
     51 λglobals.
     52  mk_more_sem_params2 … ertl_more_sem_params ertl_init_locals
     53   (graph_fetch_statement …) ertl_fetch_result ertl_fetch_external_args ertl_set_result
     54    (ertl_exec_extended …).
     55
     56definition ertl_fullexec ≝
     57 joint_fullexec … (λp. ertl_more_sem_params2 (prog_var_names … p)).
     58
     59(*
    1460(* CSC: external functions never fail (??) and always return something of the
    1561   size of one register, both in the frontend and in the backend.
     
    424470  mk_fullexec … RTL_exec ? make_initial_state.
    425471*)
     472*)
  • src/joint/SemanticUtils.ma

    r1300 r1302  
    11include "joint/semantics.ma".
    22
    3 (*** Store/retrieve on registers ***)
     3(*** Store/retrieve on pseudo-registers ***)
    44
    55axiom BadRegister : String.
     
    99definition reg_retrieve : register_env beval → register → res beval ≝
    1010 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
     11
     12(*** Store/retrieve on hardware registers ***)
     13
     14axiom hw_register_env: Type[0]. (* CSC: use the one in I8051? *)
     15axiom hwreg_retrieve : hw_register_env → Register → res beval.
     16axiom hwreg_store : Register → beval → hw_register_env → res hw_register_env.
    1117
    1218(****************************************************************************)
Note: See TracChangeset for help on using the changeset viewer.