Changeset 1451 for src/LIN/semantics.ma


Ignore:
Timestamp:
Oct 22, 2011, 4:18:11 AM (9 years ago)
Author:
sacerdot
Message:
  1. All axioms in LIN/semantics.ma closed
  2. succ_pc and pointer_of_label moved to more_sem_params1; their type have been changed too to implement LIN/semantics.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/semantics.ma

    r1408 r1451  
    55 λ_.λaddr. addr_add addr 1.
    66
    7 (*CSC: XXXX here re-use the code for the lookup argument of LIN params__ *)
    8 axiom lin_pointer_of_label: label → Σp:pointer. ptype p = Code.
     7axiom BadOldPointer: String.
     8(*CSC: XXX factorize the code with graph_fetch_function!!! *)
     9definition lin_fetch_function:
     10 ∀globals. genv … (lin_params globals) → pointer → res (joint_internal_function globals (lin_params globals)) ≝
     11 λglobals,ge,old.
     12  let b ≝ pblock old in
     13  do def ← opt_to_res ? [MSG BadOldPointer] (find_funct_ptr … ge b);
     14  match def with
     15  [ Internal fn ⇒ OK … fn
     16  | External _ ⇒ Error … [MSG BadOldPointer]].
    917
    10 (*CSC: XXX factorize code with graph_fetch_statement!!!!!*)
     18axiom BadLabel: String.
     19definition lin_pointer_of_label:
     20 ∀globals. genv … (lin_params globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
     21 λglobals,ge,old,l.
     22  do fn ← lin_fetch_function … ge old ;
     23  do pos ←
     24   opt_to_res ? [MSG BadLabel]
     25    (position_of ?
     26      (λs. let 〈l',x〉 ≝ s in
     27        match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false])
     28     (joint_if_code … (lin_params …) fn)) ;
     29  OK … (inject … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
     30// qed.
     31
     32(*CSC: XXX factorize code with graph_fetch_statement?*)
    1133axiom BadProgramCounter: String.
    12 axiom lin_fetch_statement:
    13  ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc lin_pointer_of_label) → res (pre_lin_statement globals).
    14 (* λglobals,ge,st.
    15   do p ← pointer_of_address (pc … st) ;
    16   let b ≝ pblock p in
    17   do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    18   [ Internal def' ⇒
    19      let off ≝ poff p in
    20      opt_to_res ? [MSG BadProgramCounter] (\snd (nth ?? (joint_if_code … def') off))
    21   | External _ ⇒ Error … [MSG BadProgramCounter]].*)
     34definition lin_fetch_statement:
     35 ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params unit) → res (pre_lin_statement globals) ≝
     36 λglobals,ge,st.
     37  do ppc ← pointer_of_address (pc … st) ;
     38  do fn ← lin_fetch_function … ge ppc ;
     39  let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
     40  do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ;
     41  OK … (\snd found).
    2242
    23 definition lin_fullexec ≝ ltl_lin_fullexec … lin_succ_pc lin_pointer_of_label … lin_fetch_statement.
     43definition lin_fullexec: fullexec io_out io_in ≝
     44 ltl_lin_fullexec … lin_succ_pc … lin_fetch_statement lin_pointer_of_label.
Note: See TracChangeset for help on using the changeset viewer.