Changeset 1408 for src/LIN


Ignore:
Timestamp:
Oct 19, 2011, 11:30:24 AM (8 years ago)
Author:
sacerdot
Message:
  1. Added joint/BEGlobalenvs that is a modification of common/Globalenvs where
    • the memory used is the back-end one
    • no lookup via values is implemented
    • global variables are never initialized in the back-end
  2. Added to all semantics some default value to initialize the initial state
  3. Initial state initialization (in joint/semantics.ma) almost completed.
Location:
src/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1390 r1408  
    66 λsuccT,succ,pointer_of_label.
    77 mk_more_sem_params ?
    8   unit hw_register_env succ
     8  unit it hw_register_env empty_hw_register_env 0 it succ
    99   hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
    1010    (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
  • src/LIN/semantics.ma

    r1383 r1408  
    55 λ_.λaddr. addr_add addr 1.
    66
     7(*CSC: XXXX here re-use the code for the lookup argument of LIN params__ *)
    78axiom lin_pointer_of_label: label → Σp:pointer. ptype p = Code.
    89
    9 axiom NotFound: String.
     10(*CSC: XXX factorize code with graph_fetch_statement!!!!!*)
     11axiom BadProgramCounter: String.
    1012axiom lin_fetch_statement:
    11  ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc lin_pointer_of_label) → res (pre_lin_statement globals).(* ≝
    12  λglobals,ge,st.
    13   let pc ≝ pc … st in
    14  ?.
    15   let fn ≝ ? in
    16   opt_to_res ? [MSG NotFound] (lookup … (lin_params …) (joint_if_code … fn) ?(*label???*)).
    17 *)
     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]].*)
    1822
    1923definition lin_fullexec ≝ ltl_lin_fullexec … lin_succ_pc lin_pointer_of_label … lin_fetch_statement.
Note: See TracChangeset for help on using the changeset viewer.