source: src/joint/SemanticUtils.ma @ 1299

Last change on this file since 1299 was 1299, checked in by sacerdot, 9 years ago

Functions from RTL/semantics.ma generalized to work on every graph language
and moved into joint/SemanticUtils.ma.

File size: 1.5 KB
Line 
1include "joint/semantics.ma".
2
3(*CSC: XXXX; we need to create a brand new chunk per label, so that
4  pointer operations on labels are not semantically valid!! *)
5axiom rtl_pointer_of_label: label → Σp:pointer. ptype p = Code.
6axiom rtl_label_of_pointer: pointer → res label.
7
8(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
9  Maybe there is a better way to organize the code!!! *)
10definition rtl_succ_p: label → address → address.
11 #l #_ generalize in match (refl … (beval_pair_of_pointer (rtl_pointer_of_label l)))
12 cases (beval_pair_of_pointer (rtl_pointer_of_label l)) in ⊢ (???% → ?)
13  [ #res #_ @res
14  | #msg cases (rtl_pointer_of_label l) * * #q #com #off #E1 #E2 destruct ]
15qed.
16
17axiom BadProgramCounter: String.
18definition graph_fetch_statement:
19 ∀params1,sem_params,globals.
20  genv … (graph_params params1 globals) →
21   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
22 λparams1,sem_params,globals,ge,st.
23  (*CSC: the next two lines implement pointer_of_address;
24    duplicated twice in joint/semantics.ma *)
25  let 〈v1,v2〉 ≝ pc … st in
26  do p ← pointer_of_bevals [v1;v2] ;
27
28  let b ≝ pblock p in
29  do l ← rtl_label_of_pointer p;
30  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
31  match def with
32  [ Internal def' ⇒
33     opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … def') l)
34  | External _ ⇒ Error … [MSG BadProgramCounter]].
Note: See TracBrowser for help on using the repository browser.