Changeset 1451 for src/LIN


Ignore:
Timestamp:
Oct 22, 2011, 4:18:11 AM (8 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
Location:
src/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1415 r1451  
    55definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
    66
    7 (*CSC: re-organize to take succ_pc out of lin_more_sem_params? *)
    8 definition ltl_lin_more_sem_params: ∀succT,succ,pointer_of_label. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
    9  λsuccT,succ,pointer_of_label.
     7definition ltl_lin_more_sem_params: ∀succT. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
     8 λsuccT.
    109 mk_more_sem_params ?
    11   unit it hw_register_env init_hw_register_env 0 it succ
     10  unit it hw_register_env init_hw_register_env 0 it
    1211   hw_reg_store hw_reg_retrieve (λ_.hw_reg_store RegisterA) (λe.λ_.hw_reg_retrieve e RegisterA)
    1312    (λ_.hw_reg_store RegisterB) (λe.λ_.hw_reg_retrieve e RegisterB)
     
    2120       | to_acc reg ⇒
    2221          do v ← hw_reg_retrieve locals reg ;
    23           hw_reg_store RegisterA v locals ])
    24      pointer_of_label.
     22          hw_reg_store RegisterA v locals ]).
    2523
    26 definition ltl_lin_sem_params:
    27  ∀succT,succ,pointer_of_label. sem_params ≝
    28  λsuccT,succ,pointer_of_label.mk_sem_params … (ltl_lin_more_sem_params succT succ pointer_of_label).
     24definition ltl_lin_sem_params: ∀succT. sem_params ≝
     25 λsuccT.mk_sem_params … (ltl_lin_more_sem_params succT).
    2926
    3027
    3128definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    3229definition ltl_lin_pop_frame:
    33  ∀succT,succ,pointer_of_label,codeT,lookup.
     30 ∀succT,codeT,lookup.
    3431 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
    35  state … (ltl_lin_sem_params succT succ pointer_of_label) → res (state … (ltl_lin_sem_params … succ pointer_of_label)) ≝
    36  λ_.λ_.λ_.λ_.λ_.λ_.λ_.λt.OK … t.
     32 state … (ltl_lin_sem_params succT) → res (state … (ltl_lin_sem_params …)) ≝
     33 λ_.λ_.λ_.λ_.λ_.λt.OK … t.
    3734definition ltl_lin_save_frame:
    38  ∀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)) ≝
    39  λ_.λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
     35 ∀succT. address → nat → unit → nat → unit → state … (ltl_lin_sem_params succT) → res (state … (ltl_lin_sem_params …)) ≝
     36 λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    4037
    4138(* The following implementation only works for functions that return 32 bits *)
    4239definition ltl_lin_result_regs:
    43  ∀succT,succ,pointer_of_label,codeT,lookup.
     40 ∀succT,codeT,lookup.
    4441 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
    45  state (ltl_lin_sem_params succT succ pointer_of_label) → res (list Register) ≝
    46  λ_.λ_.λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets.
     42 state (ltl_lin_sem_params succT) → res (list Register) ≝
     43 λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets.
    4744
    4845(*CSC: XXXX, for external functions only*)
    49 axiom ltl_lin_fetch_external_args: ∀succT,succ,pointer_of_label.external_function → state (ltl_lin_sem_params succT succ pointer_of_label) → res (list val).
    50 axiom ltl_lin_set_result: ∀succT,succ,pointer_of_label.list val → state (ltl_lin_sem_params succT succ pointer_of_label) → res (state (ltl_lin_sem_params … succ pointer_of_label)).
     46axiom ltl_lin_fetch_external_args: ∀succT.external_function → state (ltl_lin_sem_params succT) → res (list val).
     47axiom ltl_lin_set_result: ∀succT.list val → state (ltl_lin_sem_params succT) → res (state (ltl_lin_sem_params succT)).
    5148
    52 definition ltl_lin_exec_extended: ∀succT,succ,pointer_of_label.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params succT succ pointer_of_label) → IO io_out io_in (trace × (state (ltl_lin_sem_params … succ pointer_of_label)))
    53  ≝ λsuccT,succ,pointer_of_label,p,globals,ge,abs. ⊥.
     49definition ltl_lin_exec_extended: ∀succT.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params succT) → IO io_out io_in (trace × (state (ltl_lin_sem_params succT)))
     50 ≝ λsuccT,p,globals,ge,abs. ⊥.
    5451@abs qed.
    5552
    5653definition ltl_lin_more_sem_params2:
    57  ∀succT,succ,pointer_of_label,codeT,lookup,fetch.
     54 ∀succT,codeT,lookup.∀succ: succT → address → res address.∀fetch.
     55 ∀pointer_of_label: ∀globals. genv globals
     56  (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals))
     57  →pointer→label→res (Σp0:pointer.ptype p0=Code).
    5858 ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
    59  λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
     59 λsuccT,codeT,lookup,succ,fetch,pointer_of_label,globals.
    6060  mk_more_sem_params2 …
    61    (mk_more_sem_params1 … (ltl_lin_more_sem_params … succ pointer_of_label)
    62     (fetch globals) (load_ra …) (ltl_lin_result_regs …)
     61   (mk_more_sem_params1 … (ltl_lin_more_sem_params …)
     62    succ (pointer_of_label …) (fetch globals) (load_ra …) (ltl_lin_result_regs …)
    6363    ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
    6464    (ltl_lin_fetch_external_args …) (ltl_lin_set_result …)) (ltl_lin_exec_extended …).
    6565
    6666definition ltl_lin_fullexec ≝
    67  λsuccT,succ,pointer_of_label,codeT,lookup,fetch.
    68   joint_fullexec … (λp. ltl_lin_more_sem_params2 succT succ pointer_of_label codeT lookup fetch (prog_var_names … p)).
     67 λsuccT,codeT,lookup,succ,fetch,pointer_of_label.
     68  joint_fullexec … (λp. ltl_lin_more_sem_params2 succT codeT lookup succ fetch pointer_of_label (prog_var_names … p)).
  • 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.