source: src/joint/SemanticUtils.ma @ 1467

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

Bug fixed: labels MUST be represented as pointers whose block is the block of
the function the label is defined in. This invariant is used later everywhere to
retrieve the function given the pointer.

File size: 2.8 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
23definition graph_pointer_of_label0:
24 pointer → label → Σp:pointer. ptype p = Code ≝
25 λoldpc,l.
26  mk_pointer Code
27   (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (nat_of_bitvector ? (word_of_identifier … l))).
28// qed.
29
30definition graph_pointer_of_label:
31 ∀params1.∀globals. genv … (graph_params params1 globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
32 λ_.λ_.λ_.λoldpc,l.
33  OK ? (graph_pointer_of_label0 oldpc l).
34
35definition graph_label_of_pointer: pointer → res label ≝
36 λp. OK … (an_identifier ? (bitvector_of_nat … (abs (offv (poff p))))).
37
38(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
39 But I can't use it directly because this one uses a concrete definition of
40 pointer_of_label and it is used to istantiate the more_sem_params record
41 where the abstract version is declared as a field. Is there a better way
42 to organize the code? *)
43definition graph_succ_p: label → address → res address ≝
44 λl,old.
45  do ptr ← pointer_of_address old ;
46  let newptr ≝ graph_pointer_of_label0 ptr l in
47  address_of_pointer newptr.
48
49axiom BadProgramCounter: String.
50
51definition graph_fetch_function:
52 ∀params1,sem_params,globals.
53  genv … (graph_params params1 globals) →
54   state sem_params → res (joint_internal_function … (graph_params params1 globals)) ≝
55 λparams1,sem_params,globals,ge,st.
56  do p ← code_pointer_of_address (pc … st) ;
57  let b ≝ pblock p in
58  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
59  match def with
60  [ Internal def' ⇒ OK … def'
61  | External _ ⇒ Error … [MSG BadProgramCounter]].
62
63definition graph_fetch_statement:
64 ∀params1,sem_params,globals.
65  genv … (graph_params params1 globals) →
66   state sem_params → res (joint_statement (graph_params_ params1) globals) ≝
67 λparams1,sem_params,globals,ge,st.
68  do p ← code_pointer_of_address (pc … st) ;
69  do f ← graph_fetch_function … ge st ;
70  do l ← graph_label_of_pointer p;
71  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
Note: See TracBrowser for help on using the repository browser.