Changeset 1385 for src/joint


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/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • 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.