Changeset 1390


Ignore:
Timestamp:
Oct 17, 2011, 11:43:52 AM (8 years ago)
Author:
sacerdot
Message:

All fetch_result implementations have been factorized out, leaving only a
result_regs function. All axioms in joint_LTL_LIN_semantics but the ones for
external functions have been implemented.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1389 r1390  
    6060    (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)).
    6161
    62 definition ertl_fetch_result:
    63  ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list beval) ≝
     62definition ertl_result_regs:
     63 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list register) ≝
    6464 λglobals,ge,st.
    6565  do fn ← graph_fetch_function … globals ge st ;
    66   let ret_val_regs ≝ joint_if_result … fn in
    67    mmap … (λreg.greg_retrieve ertl_sem_params st reg) ret_val_regs.
     66  OK … (joint_if_result … fn).
    6867
    6968(*CSC: XXXX, for external functions only*)
     
    117116 λglobals.
    118117  mk_more_sem_params2 … ertl_more_sem_params
    119    (graph_fetch_statement …) (load_ra …) (ertl_fetch_result …)
     118   (graph_fetch_statement …) (load_ra …) (ertl_result_regs …)
    120119   ertl_init_locals ertl_save_frame (ertl_pop_frame …)
    121120   ertl_fetch_external_args ertl_set_result (ertl_exec_extended …).
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1386 r1390  
    3636 λ_.λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    3737
    38 (*CSC: XXXXX, for is_final only *)
    39 axiom ltl_lin_fetch_result:
     38(* The following implementation only works for functions that return 32 bits *)
     39definition ltl_lin_result_regs:
    4040 ∀succT,succ,pointer_of_label,codeT,lookup.
    4141 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
    42  state (ltl_lin_sem_params succT succ pointer_of_label) → res (list beval).
     42 state (ltl_lin_sem_params succT succ pointer_of_label) → res (list Register) ≝
     43 λ_.λ_.λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets.
    4344
    4445(*CSC: XXXX, for external functions only*)
     
    5556 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
    5657  mk_more_sem_params2 … (ltl_lin_more_sem_params … succ pointer_of_label)
    57    (fetch globals) (load_ra …) (ltl_lin_fetch_result …)
     58   (fetch globals) (load_ra …) (ltl_lin_result_regs …)
    5859   ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
    5960   (ltl_lin_fetch_external_args …) (ltl_lin_set_result …) (ltl_lin_exec_extended …).
  • src/RTL/semantics.ma

    r1386 r1390  
    3939  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
    4040
    41 definition rtl_fetch_result:
    42  ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list beval) ≝
     41definition rtl_result_regs:
     42 ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list register) ≝
    4343 λglobals,ge,st.
    4444  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.
     45  OK … (joint_if_result … fn).
    4746
    4847(*CSC: we could use a dependent type here: the list of return values should have
     
    5251 ∀globals. genv … (rtl_params globals) → state … rtl_sem_params → res (state … rtl_sem_params) ≝
    5352 λglobals,ge,st.
    54   do ret_vals ← rtl_fetch_result … ge st ;
     53  do ret_regs ← rtl_result_regs … ge st ;
     54  do ret_vals ← mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_regs ;
    5555  match st_frms ? st with
    5656  [ nil ⇒ Error ? [MSG EmptyStack]
     
    114114 λglobals.
    115115  mk_more_sem_params2 … rtl_more_sem_params
    116    (graph_fetch_statement …) rtl_fetch_ra (rtl_fetch_result …)
     116   (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
    117117   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
    118118   rtl_fetch_external_args rtl_set_result (rtl_exec_extended …).
  • src/joint/semantics.ma

    r1387 r1390  
    5656
    5757 ; fetch_ra: state (mk_sem_params … more_sparams1) → res ((state (mk_sem_params … more_sparams1)) × address)
    58  ; fetch_result: genv globals p → state (mk_sem_params … more_sparams1) → res (list beval)
     58 ; result_regs: genv globals p → state (mk_sem_params … more_sparams1) → res (list (generic_reg p))
    5959
    6060 ; init_locals : localsT p → regsT … more_sparams1 → regsT … more_sparams1
     
    328328      do 〈st,ra〉 ← fetch_ra … st;
    329329      if eq_address ra exit then
    330        do vals ← fetch_result … ge st ;
     330       do regs ← result_regs … ge st ;
     331       do vals ← mmap … (λreg.greg_retrieve … st reg) regs ;
    331332       Word_of_list_beval vals
    332333      else
Note: See TracChangeset for help on using the changeset viewer.