source: src/joint/semanticsUtils_paolo.ma @ 1651

Last change on this file since 1651 was 1641, checked in by tranquil, 8 years ago
  • semanticsUtils_paolo.ma contains code to generate both graph and linear semantics parameters (partially migrated from LIN/semantics.ma)
  • fetch_function is now common to both graph and linear
  • started porting RTL's semantics
File size: 4.1 KB
Line 
1include "joint/semantics_paolo.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(******************************** GRAPHS **************************************)
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 (pos (word_of_identifier … l))).
28// qed.
29
30definition graph_pointer_of_label :
31  ∀pars : graph_params.∀globals. genv globals pars → pointer → label →
32    res (Σp:pointer. ptype p = Code) ≝
33 λ_.λ_.λ_.λoldpc,l.
34  OK ? (graph_pointer_of_label0 oldpc l).
35
36definition graph_label_of_pointer: pointer → res label ≝
37 λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])).
38
39(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
40 But I can't use it directly because this one uses a concrete definition of
41 pointer_of_label and it is used to istantiate the more_sem_params record
42 where the abstract version is declared as a field. Is there a better way
43 to organize the code? *)
44definition graph_succ_p: label → address → res address ≝
45 λl,old.
46  do ptr ← pointer_of_address old ;
47  let newptr ≝ graph_pointer_of_label0 ptr l in
48  address_of_pointer newptr.
49
50definition graph_fetch_statement:
51 ∀pars : graph_params.
52 ∀sem_pars : sem_state_params.
53 ∀globals.
54  genv globals pars →
55  state sem_pars →
56  res (joint_statement pars globals) ≝
57 λpars,sem_pars,globals,ge,st.
58  do p ← code_pointer_of_address (pc … st) ;
59  do f ← fetch_function … ge p ;
60  do l ← graph_label_of_pointer p;
61  opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l).
62
63definition make_sem_graph_params :
64  ∀pars : graph_params.
65  ∀g_pars : more_sem_genv_params pars.
66  sem_params ≝
67  λpars,g_pars.
68  mk_sem_params
69    pars
70    (mk_more_sem_params
71      pars
72      g_pars
73      graph_succ_p
74      (graph_pointer_of_label ?)
75      (graph_fetch_statement ? ?)
76    ).
77   
78(******************************** LINEAR **************************************)
79
80definition lin_succ_p: unit → address → res address :=
81 λ_.λaddr. addr_add addr 1.
82
83
84axiom BadLabel: String.
85
86definition lin_pointer_of_label:
87 ∀pars : lin_params.
88 ∀globals. genv globals pars → pointer → label →
89  res (Σp:pointer. ptype p = Code) ≝
90 λpars,globals,ge,old,l.
91  do fn ← fetch_function … ge old ;
92  do pos ←
93   opt_to_res ? [MSG BadLabel]
94    (position_of ?
95      (λs. let 〈l',x〉 ≝ s in
96        match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false])
97     (joint_if_code … pars fn)) ;
98  OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
99// qed.
100
101definition lin_fetch_statement:
102 ∀pars : lin_params.
103 ∀sem_pars : sem_state_params.
104 ∀globals.
105 genv globals pars → state sem_pars → res (joint_statement pars globals) ≝
106 λpars,sem_pars,globals,ge,st.
107  do ppc ← pointer_of_address (pc … st) ;
108  do fn ← fetch_function … ge ppc ;
109  let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
110  do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ;
111  return (\snd found).
112
113definition make_sem_lin_params :
114  ∀pars : lin_params.
115  ∀g_pars : more_sem_genv_params pars.
116  sem_params ≝
117  λpars,g_pars.
118  mk_sem_params
119    pars
120    (mk_more_sem_params
121      pars
122      g_pars
123      lin_succ_p
124      (lin_pointer_of_label ?)
125      (lin_fetch_statement ? ?)
126    ).
127   
128
Note: See TracBrowser for help on using the repository browser.