Changeset 1451 for src/LIN/semantics.ma

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:

• src/LIN/semantics.ma (modified) (1 diff)

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 BadOldPointer: String.
+(*CSC: XXX factorize the code with graph_fetch_function!!! *)
+definition lin_fetch_function:
+ ∀globals. genv … (lin_params globals) → pointer → res (joint_internal_function globals (lin_params globals)) ≝
+ λglobals,ge,old.
+  let b ≝ pblock old in
+  do def ← opt_to_res ? [MSG BadOldPointer] (find_funct_ptr … ge b);
+  match def with
+  [ Internal fn ⇒ OK … fn
+  | External _ ⇒ Error … [MSG BadOldPointer]].
 
-(*CSC: XXX factorize code with graph_fetch_statement!!!!!*)
+axiom BadLabel: String.
+definition lin_pointer_of_label:
+ ∀globals. genv … (lin_params globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
+ λglobals,ge,old,l.
+  do fn ← lin_fetch_function … ge old ;
+  do pos ←
+   opt_to_res ? [MSG BadLabel]
+    (position_of ?
+      (λs. let 〈l',x〉 ≝ s in
+        match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false])
+     (joint_if_code … (lin_params …) fn)) ;
+  OK … (inject … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
+// qed.
+
+(*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.
-  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_fetch_statement:
+ ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params unit) → res (pre_lin_statement globals) ≝
+ λglobals,ge,st.
+  do ppc ← pointer_of_address (pc … st) ;
+  do fn ← lin_fetch_function … ge ppc ;
+  let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
+  do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ;
+  OK … (\snd found).
 
-definition lin_fullexec ≝ ltl_lin_fullexec … lin_succ_pc lin_pointer_of_label … lin_fetch_statement.
+definition lin_fullexec: fullexec io_out io_in ≝
+ ltl_lin_fullexec … lin_succ_pc … lin_fetch_statement lin_pointer_of_label.