Changeset 1408 for src/LIN

Timestamp:

Oct 19, 2011, 11:30:24 AM (9 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:

• joint_LTL_LIN_semantics.ma (modified) (1 diff)
• semantics.ma (modified) (1 diff)

src/LIN/joint_LTL_LIN_semantics.ma

@@ -6 +6 @@
  λsuccT,succ,pointer_of_label.
  mk_more_sem_params ?
-  unit hw_register_env succ
+  unit it hw_register_env empty_hw_register_env 0 it succ
    hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
     (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)

src/LIN/semantics.ma

@@ -5 +5 @@
  λ_.λaddr. addr_add addr 1.
 
+(*CSC: XXXX here re-use the code for the lookup argument of LIN params__ *)
 axiom lin_pointer_of_label: label → Σp:pointer. ptype p = Code.
 
-axiom NotFound: String.
+(*CSC: XXX factorize code with graph_fetch_statement!!!!!*)
+axiom BadProgramCounter: String.
 axiom lin_fetch_statement:
- ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc lin_pointer_of_label) → res (pre_lin_statement globals).(* ≝
- λglobals,ge,st.
-  let pc ≝ pc … st in
- ?.
-  let fn ≝ ? in
-  opt_to_res ? [MSG NotFound] (lookup … (lin_params …) (joint_if_code … fn) ?(*label???*)).
-*)
+ ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc lin_pointer_of_label) → res (pre_lin_statement globals).
+(* λglobals,ge,st.
+  do p ← pointer_of_address (pc … st) ;
+  let b ≝ pblock p in
+  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
+  [ Internal def' ⇒
+     let off ≝ poff p in
+     opt_to_res ? [MSG BadProgramCounter] (\snd (nth ?? (joint_if_code … def') off))
+  | External _ ⇒ Error … [MSG BadProgramCounter]].*)
 
 definition lin_fullexec ≝ ltl_lin_fullexec … lin_succ_pc lin_pointer_of_label … lin_fetch_statement.