Changeset 1385


Ignore:
Timestamp:
Oct 17, 2011, 1:40:13 AM (8 years ago)
Author:
sacerdot
Message:
  1. fetch_result and pop_frame now takes the genv in input
  2. implementation of fetch_result for RTL completed All RTL axioms but the ones related to external functions are now closed.
Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1384 r1385  
    4343(*CSC: could we use here a dependent type to avoid the Error case? *)
    4444axiom EmptyStack: String.
    45 definition ertl_pop_frame: state … ertl_sem_params → res (state … ertl_sem_params) ≝
    46  λst.
     45definition ertl_pop_frame:
     46 ∀globals. genv … (ertl_params globals) → state … ertl_sem_params → res (state … ertl_sem_params) ≝
     47 λglobals,ge,st.
    4748  let frms ≝ st_frms ? st in
    4849  match frms with
     
    6162definition ertl_more_sem_params1 : more_sem_params1 … ertl_params1 ≝
    6263 mk_more_sem_params1 ? ertl_params1 ertl_more_sem_params
    63   ertl_init_locals ertl_pop_frame ertl_save_frame.
     64  ertl_init_locals ertl_save_frame.
    6465
    6566(*CSC: XXXXX, for is_final only *)
    66 axiom ertl_fetch_result: state ertl_sem_params → res (list beval).
     67axiom ertl_fetch_result:
     68 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list beval).
    6769
    6870(*CSC: XXXX, for external functions only*)
     
    117119 λglobals.
    118120  mk_more_sem_params2 … ertl_more_sem_params1
    119    (graph_fetch_statement …) (load_ra …) ertl_fetch_result
    120     ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
     121   (graph_fetch_statement …) (load_ra …) (ertl_fetch_result …)
     122   (ertl_pop_frame …) ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
    121123
    122124definition ertl_fullexec ≝
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1384 r1385  
    2828definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    2929definition ltl_lin_pop_frame:
    30  ∀succT,succ,pointer_of_label. state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
    31  λ_.λ_.λ_.λt.OK … t.
     30 ∀succT,succ,pointer_of_label,codeT,lookup.
     31 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
     32 state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
     33 λ_.λ_.λ_.λ_.λ_.λ_.λ_.λt.OK … t.
    3234definition ltl_lin_save_frame:
    3335 ∀succT,succ,pointer_of_label. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
     
    3739 λsuccT,succ,pointer_of_label.
    3840 mk_more_sem_params1 ? ltl_lin_params1 (ltl_lin_more_sem_params succT succ pointer_of_label)
    39   ltl_lin_init_locals (ltl_lin_pop_frame …) (ltl_lin_save_frame …).
     41  ltl_lin_init_locals (ltl_lin_save_frame …).
    4042
    4143(*CSC: XXXXX, for is_final only *)
    42 axiom ltl_lin_fetch_result: ∀succT,succ,pointer_of_label.state (ltl_lin_sem_params succT succ pointer_of_label) → res (list beval).
     44axiom ltl_lin_fetch_result:
     45 ∀succT,succ,pointer_of_label,codeT,lookup.
     46 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
     47 state (ltl_lin_sem_params succT succ pointer_of_label) → res (list beval).
    4348
    4449(*CSC: XXXX, for external functions only*)
     
    5560 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
    5661  mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ pointer_of_label)
    57    (fetch globals) (load_ra …) (ltl_lin_fetch_result …)
    58    (ltl_lin_fetch_external_args …)
    59    (ltl_lin_set_result …) (ltl_lin_exec_extended …).
     62   (fetch globals) (load_ra …) (ltl_lin_fetch_result …) (ltl_lin_pop_frame …)
     63   (ltl_lin_fetch_external_args …) (ltl_lin_set_result …) (ltl_lin_exec_extended …).
    6064
    6165definition ltl_lin_fullexec ≝
  • src/RTL/semantics.ma

    r1384 r1385  
    3939  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
    4040
    41 
    42 (*CSC: XXXXX, for is_final only *)
    43 axiom rtl_fetch_result: state rtl_sem_params → res (list beval).
    44 (*  let ret_vals ≝ map … (λreg.greg_retrieve rtl_sem_params st reg) ret_val_regs in
    45 *)
     41definition rtl_fetch_result:
     42 ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list beval) ≝
     43 λglobals,ge,st.
     44  do fn ← graph_fetch_function … globals ge st ;
     45  let ret_val_regs ≝ joint_if_result … fn in
     46   mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_val_regs.
    4647
    4748(*CSC: we could use a dependent type here: the list of return values should have
     
    4950  saves the OutOfBounds exception *)
    5051definition rtl_pop_frame:
    51  state … rtl_sem_params → res (state … rtl_sem_params) ≝
    52  λst.
    53   do ret_vals ← rtl_fetch_result … st ;
    54   let frms ≝ st_frms ? st in
    55   match frms with
     52 ∀globals. genv … (rtl_params globals) → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     53 λglobals,ge,st.
     54  do ret_vals ← rtl_fetch_result … ge st ;
     55  match st_frms ? st with
    5656  [ nil ⇒ Error ? [MSG EmptyStack]
    5757  | cons hd tl ⇒
     
    9090definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
    9191 mk_more_sem_params1 ? rtl_params1 rtl_more_sem_params
    92   rtl_init_locals rtl_pop_frame rtl_save_frame.
     92  rtl_init_locals rtl_save_frame.
    9393
    9494(*CSC: XXXX, for external functions only*)
     
    118118 λglobals.
    119119  mk_more_sem_params2 … rtl_more_sem_params1
    120    (graph_fetch_statement …) rtl_fetch_ra rtl_fetch_result rtl_fetch_external_args
    121     rtl_set_result (rtl_exec_extended …).
     120   (graph_fetch_statement …) rtl_fetch_ra (rtl_fetch_result …)
     121   (rtl_pop_frame …) rtl_fetch_external_args rtl_set_result (rtl_exec_extended …).
    122122
    123123definition rtl_fullexec ≝
  • src/joint/SemanticUtils.ma

    r1384 r1385  
    5454
    5555axiom BadProgramCounter: String.
     56
     57definition graph_fetch_function:
     58 ∀params1,sem_params,globals.
     59  genv … (graph_params params1 globals) →
     60   state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝
     61 λparams1,sem_params,globals,ge,st.
     62  do p ← pointer_of_address (pc … st) ;
     63  let b ≝ pblock p in
     64  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
     65  match def with
     66  [ Internal def' ⇒ OK … def'
     67  | External _ ⇒ Error … [MSG BadProgramCounter]].
     68
    5669definition graph_fetch_statement:
    5770 ∀params1,sem_params,globals.
     
    6073 λparams1,sem_params,globals,ge,st.
    6174  do p ← pointer_of_address (pc … st) ;
    62   let b ≝ pblock p in
    63   do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    64   match def with
    65   [ Internal def' ⇒
    66      do l ← label_of_pointer p;
    67      opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … def') l)
    68   | External _ ⇒ Error … [MSG BadProgramCounter]].
     75  do f ← graph_fetch_function … ge st ;
     76  do l ← label_of_pointer p;
     77  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
  • src/joint/semantics.ma

    r1384 r1385  
    5252
    5353 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    54  ; pop_frame: state (mk_sem_params … more_sparams) → res ((state (mk_sem_params … more_sparams)))
    5554   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
    5655     type of arguments. To be fixed using a dependent type *)
     
    7675
    7776 ; fetch_ra: state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)) × address)
    78  ; fetch_result: state (mk_sem_params … more_sparams1) → res (list beval)
     77 ; fetch_result: genv globals p → state (mk_sem_params … more_sparams1) → res (list beval)
     78
     79 ; pop_frame: genv globals p → state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)))
    7980
    8081 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams1) → res (list val)
     
    341342    | RETURN ⇒
    342343      ! 〈st,ra〉 ← fetch_ra … st;
    343       ! st ← pop_frame … st;
     344      ! st ← pop_frame … ge st;
    344345        ret ? 〈E0,set_pc … ra st〉].
    345346cases addr //
     
    353354      do 〈st,ra〉 ← fetch_ra … st;
    354355      if eq_address ra exit then
    355        do vals ← fetch_result … st ;
     356       do vals ← fetch_result … ge st ;
    356357       Word_of_list_beval vals
    357358      else
Note: See TracChangeset for help on using the changeset viewer.