source: src/joint/SemanticUtils.ma @ 1383

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

Potential bug fixed and bug found: the way pointers and labels are put in
bijection must be different between LIN and graph-like languages (bug fixed).
Moreover, in both cases it must be possible to retrieve the function from the
address and the easiest (only?) way to do that is to use the block of the
address to store the block of the function, and put the offsets in bijection
with labels/offsets, preventing pointer mangling since the pointer is in
the Code region (found, to be fixed).

File size: 3.0 KB
Line 
1include "joint/semantics.ma".
2include alias "common/Identifiers.ma".
3
4(*** Store/retrieve on pseudo-registers ***)
5
6axiom BadRegister : String.
7
8definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
9
10definition reg_retrieve : register_env beval → register → res beval ≝
11 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
12
13(*** Store/retrieve on hardware registers ***)
14
15axiom hw_register_env: Type[0]. (* CSC: use the one in I8051? *)
16axiom hwreg_retrieve : hw_register_env → Register → res beval.
17axiom hwreg_store : Register → beval → hw_register_env → res hw_register_env.
18
19(****************************************************************************)
20
21(*CSC: XXXXXXXXXXXXXXXXX bug here; we need to change the encoding so that
22  the block is the one of the function and the offset corresponds to the
23  label. Code pointer arithmetics must be prevented in another way, i.e.
24  by not allowing any increment/decrement on Code regions (with the
25  exception of LIN's succ_pc function). If we don't do that, then the
26  find_funct_ptr (e.g. in graph_fetch_statement) are not correct! *)
27(*CSC: XXXX; do we need to create a brand new chunk per label, so that
28  pointer operations on labels are not semantically valid?
29  ATM, the pointers are not valid (they do not point to allocated regions)
30  and, moreover, they conflict with function blocks and with other pointers
31  in other functions. However, there could be simpler ways to invalidate
32  pointer arithmetics on Code pointers.
33*)
34definition pointer_of_label: label → Σp:pointer. ptype p = Code ≝
35 λl.
36  mk_pointer Code
37   (mk_block Code (Zopp (nat_of_bitvector ? (word_of_identifier … l))))
38   ? (mk_offset OZ).
39// qed.
40
41(*CSC: XXXX; inverse of the previous function, but it does not check that
42  the offset is zero and thus it never fails. *)
43definition label_of_pointer: pointer → res label ≝
44 λp. OK … (an_identifier ? (bitvector_of_nat … (abs (block_id (pblock p))))).
45
46(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
47  Maybe there is a better way to organize the code!!! *)
48definition graph_succ_p: label → address → res address.
49 #l #_ generalize in match (refl … (address_of_pointer (pointer_of_label l)))
50 cases (address_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
51  [ #res #_ @(OK … res)
52  | #msg cases (pointer_of_label l) * * #q #com #off #E1 destruct #E2 normalize in E2; destruct ]
53qed.
54
55axiom BadProgramCounter: String.
56definition graph_fetch_statement:
57 ∀params1,sem_params,globals.
58  genv … (graph_params params1 globals) →
59   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
60 λparams1,sem_params,globals,ge,st.
61  do p ← pointer_of_address (pc … st) ;
62  let b ≝ pblock p in
63  do l ← label_of_pointer p;
64  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
65  match def with
66  [ Internal def' ⇒
67     opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … def') l)
68  | External _ ⇒ Error … [MSG BadProgramCounter]].
Note: See TracBrowser for help on using the repository browser.