| 1 | include "LIN/joint_LTL_LIN_semantics.ma". |
|---|
| 2 | include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *) |
|---|
| 3 | |
|---|
| 4 | definition lin_succ_pc: unit → address → res address := |
|---|
| 5 | λ_.λaddr. addr_add addr 1. |
|---|
| 6 | |
|---|
| 7 | axiom BadOldPointer: String. |
|---|
| 8 | (*CSC: XXX factorize the code with graph_fetch_function!!! *) |
|---|
| 9 | definition 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]]. |
|---|
| 17 | |
|---|
| 18 | axiom BadLabel: String. |
|---|
| 19 | definition 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?*) |
|---|
| 33 | axiom BadProgramCounter: String. |
|---|
| 34 | definition 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). |
|---|
| 42 | |
|---|
| 43 | definition lin_fullexec: fullexec io_out io_in ≝ |
|---|
| 44 | ltl_lin_fullexec … lin_succ_pc … lin_fetch_statement lin_pointer_of_label. |
|---|
