Changeset 1176


Ignore:
Timestamp:
Sep 3, 2011, 4:17:48 AM (8 years ago)
Author:
sacerdot
Message:

...

Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1171 r1176  
    1 include "ASM/String.ma".
    21include "ASM/I8051.ma".
    32include "common/CostLabel.ma".
    4 include "common/Graphs.ma".
    53include "common/AST.ma".
    64include "common/Registers.ma".
     5include "common/Graphs.ma".
    76
    87record params: Type[1] ≝
    9  { acc_a_reg: Type[0]
     8 { next: Type[0]
     9 
     10 ; acc_a_reg: Type[0]
    1011 ; acc_b_reg: Type[0]
    1112 ; dpl_reg: Type[0]
     
    1314 ; pair_reg: Type[0]
    1415 ; generic_reg: Type[0]
     16 
     17 ; extend_statements: Type[0]
     18 
     19 ; resultT: Type[0]
     20 ; localsT: Type[0]
     21 ; paramsT: Type[0]
    1522 }.
    1623
     
    3138  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
    3239  | joint_instr_call_id: ident → nat → joint_instruction p globals
    33   | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
     40  | joint_instr_cond: acc_a_reg p → next p → joint_instruction p globals.
    3441
    35 inductive joint_statement (next: Type[0]) (extend: Type[0]) (p:params) (globals: list ident): Type[0] ≝
    36   | joint_st_sequential: joint_instruction p globals → next → joint_statement next extend p globals
    37   | joint_st_goto: label → joint_statement next extend p globals
    38   | joint_st_return: joint_statement next extend p globals
    39   | joint_st_extension: extend → joint_statement next extend p globals.
     42inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
     43  | joint_st_sequential: joint_instruction p globals → next p → joint_statement p globals
     44  | joint_st_goto: next p → joint_statement p globals
     45  | joint_st_return: joint_statement p globals
     46  | joint_st_extension: extend_statements p → joint_statement p globals.
     47
     48record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝
     49 { pmemoryT: Type[0]
     50 ; lookup: pmemoryT → next preparams → option (joint_statement preparams globals)
     51 }.
     52
     53record joint_internal_function (globals: list ident) (pre) (p:sem_params_ pre globals): Type[0] ≝
     54{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
     55  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
     56(*  joint_if_sig: signature;  -- dropped in front end *)
     57  joint_if_result   : resultT pre;
     58  joint_if_params   : paramsT pre;
     59  joint_if_locals   : localsT pre;
     60  joint_if_stacksize: nat;
     61  joint_if_graph    : pmemoryT … p;
     62  joint_if_entry    : Σl: next pre. lookup … p joint_if_graph l ≠ None ?;
     63  joint_if_exit     : Σl: next pre. lookup … p joint_if_graph l ≠ None ?
     64}.
     65
     66definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p).
     67
     68record joint_program (globals: list ident) (pre) (p:sem_params_ pre globals) : Type[0] ≝
     69{
     70  joint_pr_vars: list (ident × nat);
     71  joint_pr_functs: list (ident × (joint_function … p));
     72  joint_pr_main: option ident
     73}.
     74
     75(****************************************************************************)
    4076
    4177(* Used in LTL and LIN *) 
  • src/joint/semantics.ma

    r1174 r1176  
    1 
    2 (* XXX NB: I haven't checked all of these semantics against the prototype
    3            compilers yet! *)
    4 
    51include "utilities/lists.ma".
    6 
    7 include "common/Errors.ma".
    82include "common/Globalenvs.ma".
    93include "common/IO.ma".
    104include "common/SmallstepExec.ma".
    11 
    125include "joint/Joint.ma".
    136(*
     
    4639*)
    4740(* CSC: ??? *)
    48 axiom address_of_label: mem → label → address.
    49 axiom address_chunks_of_label: mem → label → Byte × Byte.
    50 (*
     41axiom address_of_label: ∀p. mem → next p → address.
     42axiom address_chunks_of_label: ∀p. mem → next p → Byte × Byte.
    5143axiom label_of_address_chunks: Byte → Byte → label.
    52 *)
    5344axiom address_of_address_chunks: Byte → Byte → address.
    5445(*
    5546axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
    5647*)
     48(*
    5749axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
    5850axiom hwreg_retrieve : mRegisterMap → Register → res val.
    5951axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
    60 (*
    61 definition genv ≝ λglobals. (genv_t Genv) (fundef (ltl_internal_function globals)).
    62 *)
    63 (* CSC: frame reduced to this
    64 definition frame: Type[0] ≝ unit.
    6552*)
    6653
     
    6956 ; framesT: Type[0]
    7057 ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
     58 
    7159 ; pop_frame_: framesT → res framesT
    7260 ; save_frame_: framesT → regsT → framesT
     
    9381 }.
    9482
     83definition genv ≝ λglobals,pre,p. (genv_t Genv) (joint_function globals pre p).
     84
     85record sem_params2 (globals: list ident): Type[1] ≝
     86 { sparams:> sem_params
     87 ; pre_sem_params:> sem_params_ sparams globals
     88 ; exec_extended: genv … pre_sem_params → extend_statements sparams → state sparams → IO io_out io_in (trace × (state sparams))
     89 }.
     90
    9591definition set_m: ∀p. mem → state p → state p ≝
    9692 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.
     
    112108
    113109(* CSC: was build_state in RTL *)
    114 definition goto: ∀p. label → state p → state p ≝
    115  λp,l,st. set_pc … (address_of_label (m … st) l) st.
     110definition goto: ∀p:sem_params. next p → state p → state p ≝
     111 λp,l,st. set_pc … (address_of_label (m … st) l) st.
    116112
    117113definition greg_store: ∀p:sem_params. generic_reg p → val → state p → res (state p) ≝
     
    194190   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
    195191
    196 definition save_ra : ∀p. state p → label → res (state p) ≝
     192definition save_ra : ∀p. state p → next p → res (state p) ≝
    197193 λp,st,l.
    198   let 〈addrl,addrh〉 ≝ address_chunks_of_label (m … st) l in
     194  let 〈addrl,addrh〉 ≝ address_chunks_of_label (m … st) l in
    199195  (* No monadic notation here *)
    200196  bind ?? (push … st addrl) (λst.push … st addrh).
    201197
    202 (*
    203 (*CSC: unused now
    204 definition fetch_ra : state → res (state × label) ≝
    205  λst.
     198definition fetch_ra : ∀p.state p → res (state p × label) ≝
     199 λp,st.
    206200  (* No monadic notation here *)
    207   bind ?? (pop st) (λres. let 〈st,addrh〉 ≝ res in
    208   bind ?? (pop st) (λres. let 〈st,addrl〉 ≝ res in
    209    OK ? 〈st, label_of_address_chunks addrl addrh〉)). *)
    210 *)
     201  bind ?? (pop st) (λres. let 〈st,addrh〉 ≝ res in
     202  bind ?? (pop st) (λres. let 〈st,addrl〉 ≝ res in
     203   OK ? 〈st, label_of_address_chunks addrl addrh〉)).
     204
    211205(*CSC: To be implemented *)
    212 
    213 (*
    214 axiom fetch_statement: ∀globals: list ident. state → res (ltl_statement globals). (* CSC *)
     206axiom fetch_statement: ∀p.∀globals: list ident. state p → res (joint_statement p globals).
     207(*
    215208axiom fetch_function: ∀globals: list ident. state → res (ltl_internal_function globals). (* CSC *)
    216209*)
    217210
     211(*
    218212definition init_locals : ∀p.list register → regsT p ≝
    219213foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
     214*)
    220215
    221216(*
     
    235230axiom BadFunction : String.
    236231
    237 (*
    238232(*CSC: to be implemented *)
    239 axiom fetch_external_args: external_function → state → res (list val).(* ≝
     233axiom fetch_external_args: ∀p. external_function → state p → res (list val). (* ≝
    240234 λfn,st.
    241235  let registerno ≝ ? fn in
     
    244238    (λr. hwreg_retrieve (regs st) r) (prefix … registersno RegisterParameters);
    245239  (* CSC: HERE WE NEED TO RETRIEVE THE REMAINING REGISTERS FROM THE STACK! *)
    246   ?.*)
     240  ?.
     241*)
     242
    247243
    248244(*CSC: to be implemented; fails if the first list is longer *)
     
    253249
    254250(* CSC: the list should be a vector or have an upper bounded length *)
    255 definition set_result: list val → state → res state ≝
    256  λvs,st.
     251(*CSC: XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX *)
     252axiom set_result: ∀p. list val → state p → res (state p).
     253(* λp,vs,st.
    257254  (* CSC: monadic notation not used *)
    258255  bind ?? (
    259256   fold_left2_first_not_longer …
    260     (λregs,v,reg. hwreg_store reg v regs) (regs st) vs RegisterRets)
    261   (λregs.OK ? (set_regs regs st)).
    262 
     257    (λregs,v,reg. hwreg_store reg v regs) (regs … st) vs RegisterRets)
     258  (λregs.OK ? (set_regs … regs st)).
     259*)
     260
     261(*
    263262definition fetch_result: state → nat → res (list val) ≝
    264263 λst,registersno.
     
    295294*)
    296295
    297 definition eval_statement : ∀p:sem_params.∀globals: list ident. ?(*(genv globals)*) → state p → joint_statement … p globals → IO io_out io_in (trace × (state p)) ≝
    298   λp,globals. λge,st,s.
    299 (* CSC: fixme
    300   ! s ← fetch_statement globals st;
    301 *)
     296(*CSC: move elsewhere *)
     297definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
     298 λA,P,c. match c with [ dp w _ ⇒ w ].
     299coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
     300
     301definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv … (pre_sem_params … p) → state p → IO io_out io_in (trace × (state p)) ≝
     302  λglobals,p. λge,st.
     303  ! s ← fetch_statement p globals st;
    302304  match s with
    303305    [ joint_st_goto l ⇒ ret ? 〈E0, goto … l st〉
     
    342344        ! v1 ← acca_retrieve … st acc_a;
    343345        ! v1 ← Byte_of_val v1;
    344         ! v2 ← greg_retrieve … src;
     346        ! v2 ← greg_retrieve … st src;
    345347        ! v2 ← Byte_of_val v2;
    346348        ! carry ← eval_bool_of_val (carry … st);
     
    374376      | joint_instr_move dst_src ⇒
    375377          ret ? 〈E0, goto … l (pair_reg_move … st dst_src)〉
    376       | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
     378      | joint_instr_call_id id argsno ⇒
    377379        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    378380        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    379381          match fd with
    380382          [ Internal fn ⇒
    381             ! st ← save_ra st l;
     383            ! st ← save_ra st l;
    382384              let st ≝ save_frame … st in
    383               let regs ≝ init_locals … (ertl_if_locals globals fn) in
    384               let l' ≝ ertl_if_entry globals fn in
    385               ret ? 〈 E0, goto … l' (set_regs … regs st)〉
     385              (*CSC: XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
     386              let regs ≝ init_locals … (ertl_if_locals globals fn) in *) let regs ≝ regs … st in
     387              let l' ≝ joint_if_entry … fn in
     388             ret ? 〈 E0, goto … l' (set_regs … regs st)〉
    386389          | External fn ⇒
    387             ! params ← fetch_external_args fn st;
     390            ! params ← fetch_external_args fn st;
    388391            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    389392            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     
    391394               components; instead I am making a singleton out of it *)
    392395              let vs ≝ [mk_val ? evres] in
    393             ! st ← set_result vs st;
    394               ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
     396            ! st ← set_result vs st;
     397              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
    395398          ]
    396399      ]
     
    401404        let pc ≝ address_of_address_chunks pcl pch in
    402405        ret ? 〈E0,set_pc … pc st〉
    403     | _ ⇒ ?
     406    | joint_st_extension c ⇒ exec_extended … p ge c st
    404407    ].
    405      
    406 axiom WrongReturnValueType: String.
    407408
    408409definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝
     
    412413  λst.
    413414 (* CSC: monadic notation missing here *)
    414   match fetch_statement globals st with
     415  match fetch_statement p globals st with
    415416  [ Error _ ⇒ None ?
    416417  | OK s ⇒
    417418    match s with
    418     [ ertl_st_lift_pre pre ⇒
    419       match pre with
    420419      [ joint_st_return ⇒
    421420        match fetch_ra st with
     
    435434      | _ ⇒ None ?
    436435      ]
    437     | _ ⇒ None ?
    438     ]
    439436  ].
    440437
Note: See TracChangeset for help on using the changeset viewer.