source: src/LIN/semantics.ma @ 2182

Last change on this file since 2182 was 1601, checked in by sacerdot, 8 years ago

Files ported to new version of the standard library.

File size: 1.9 KB
Line 
1include "LIN/joint_LTL_LIN_semantics.ma".
2include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)
3
4definition lin_succ_pc: unit → address → res address :=
5 λ_.λaddr. addr_add addr 1.
6
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]].
17
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 … (mk_Sig … (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?*)
33axiom BadProgramCounter: String.
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).
42
43definition lin_fullexec: fullexec io_out io_in ≝
44 ltl_lin_fullexec … lin_succ_pc … lin_fetch_statement lin_pointer_of_label.
Note: See TracBrowser for help on using the repository browser.