source: src/joint/SemanticUtils.ma @ 1451

Last change on this file since 1451 was 1451, checked in by sacerdot, 9 years ago
  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 size: 3.7 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
15definition init_hw_register_env: address → hw_register_env ≝
16 λaddr.
17  let 〈dpl,dph〉 ≝ addr in
18  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
19   hwreg_store RegisterDPL dpl env.
20
21(****************************************************************************)
22
23(*CSC: XXXXXXXXXXXXXXXXX bug here; we need to change the encoding so that
24  the block is the one of the function and the offset corresponds to the
25  label. Code pointer arithmetics must be prevented in another way, i.e.
26  by not allowing any increment/decrement on Code regions (with the
27  exception of LIN's succ_pc function). If we don't do that, then the
28  find_funct_ptr (e.g. in graph_fetch_statement) are not correct! *)
29(*CSC: XXXX; do we need to create a brand new chunk per label, so that
30  pointer operations on labels are not semantically valid?
31  ATM, the pointers are not valid (they do not point to allocated regions)
32  and, moreover, they conflict with function blocks and with other pointers
33  in other functions. However, there could be simpler ways to invalidate
34  pointer arithmetics on Code pointers.
35*)
36definition graph_pointer_of_label0:
37 pointer → label → Σp:pointer. ptype p = Code ≝
38 λoldpc,l.
39  mk_pointer Code
40   (mk_block Code (Zopp (nat_of_bitvector ? (word_of_identifier … l))))
41   ? (mk_offset OZ).
42// qed.
43
44definition graph_pointer_of_label:
45 ∀params1.∀globals. genv … (graph_params params1 globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
46 λ_.λ_.λ_.λoldpc,l.
47  OK ? (graph_pointer_of_label0 oldpc l).
48
49(*CSC: XXXX; inverse of the previous function, but it does not check that
50  the offset is zero and thus it never fails. *)
51definition graph_label_of_pointer: pointer → res label ≝
52 λp. OK … (an_identifier ? (bitvector_of_nat … (abs (block_id (pblock p))))).
53
54(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
55 But I can't use it directly because this one uses a concrete definition of
56 pointer_of_label and it is used to istantiate the more_sem_params record
57 where the abstract version is declared as a field. Is there a better way
58 to organize the code? *)
59definition graph_succ_p: label → address → res address ≝
60 λl,old.
61  do ptr ← pointer_of_address old ;
62  let newptr ≝ graph_pointer_of_label0 ptr l in
63  address_of_pointer newptr.
64
65axiom BadProgramCounter: String.
66
67definition graph_fetch_function:
68 ∀params1,sem_params,globals.
69  genv … (graph_params params1 globals) →
70   state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝
71 λparams1,sem_params,globals,ge,st.
72  do p ← code_pointer_of_address (pc … st) ;
73  let b ≝ pblock p in
74  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
75  match def with
76  [ Internal def' ⇒ OK … def'
77  | External _ ⇒ Error … [MSG BadProgramCounter]].
78
79definition graph_fetch_statement:
80 ∀params1,sem_params,globals.
81  genv … (graph_params params1 globals) →
82   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
83 λparams1,sem_params,globals,ge,st.
84  do p ← code_pointer_of_address (pc … st) ;
85  do f ← graph_fetch_function … ge st ;
86  do l ← graph_label_of_pointer p;
87  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
Note: See TracBrowser for help on using the repository browser.