source: src/joint/Joint_paolo.ma @ 1882

Last change on this file since 1882 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 17.7 KB
Line 
1include "ASM/I8051.ma".
2include "common/CostLabel.ma".
3include "common/AST.ma".
4include "common/Registers.ma".
5include "common/Graphs.ma".
6include "utilities/lists.ma".
7include "common/LabelledObjects.ma".
8include "ASM/Util.ma".
9
10(* Here is the structure of parameter records (downward edges are coercions,
11   the ↓ edges are the only explicitly defined coercions). lin_params and
12   graph_params are simple wrappers of unserialized_params, and the coercions
13   from them to params instantiate the missing bits with values for linarized
14   programs and graph programs respectively.
15
16        lin_params      graph_params
17              |   \_____ /____   |
18              |         /     \  |
19              |        /      ↓  ↓
20              |       |      params
21              |       |        |
22              |       |   stmt_params
23              |       |    /   
24          unserialized_params             
25            |            \       
26            |             \     
27            |         local_params
28            |              |   
29    step_params       funct_params
30
31step_params : types needed to define steps (stmts with a default fallthrough)
32stmt_params : adds successor type needed to define statements
33funct_params : types of result register and parameters of function
34local_params : adds types of local registers
35params : adds type of code and related properties *)
36
37record step_params : Type[1] ≝
38 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
39 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
40 ; acc_a_arg: Type[0] (* arguments that will eventually need to be A *)
41 ; acc_b_arg: Type[0] (* arguments that will eventually need to be B *)
42 ; dpl_reg: Type[0]   (* low address registers *)
43 ; dph_reg: Type[0]   (* high address registers *)
44 ; dpl_arg: Type[0]   (* low address registers *)
45 ; dph_arg: Type[0]   (* high address registers *)
46 ; snd_arg : Type[0]  (* second argument of binary op *)
47 ; pair_move: Type[0] (* argument of move instructions *)
48 ; call_args: Type[0] (* arguments of function calls *)
49 ; call_dest: Type[0] (* possible destination of function computation *)
50 ; ext_step: Type[0] (* other instructions not fitting in the general framework *)
51 ; ext_step_labels : ext_step → list label
52 ; ext_fin_stmt: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
53 ; ext_fin_stmt_labels : ext_fin_stmt → list label
54 }.
55 
56inductive joint_step (p:step_params) (globals: list ident): Type[0] ≝
57  | COMMENT: String → joint_step p globals
58  | COST_LABEL: costlabel → joint_step p globals
59  | MOVE: pair_move p → joint_step p globals
60  | POP: acc_a_reg p → joint_step p globals
61  | PUSH: acc_a_arg p → joint_step p globals
62  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_step p globals
63  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_step p globals
64  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_step p globals
65  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_step p globals
66  (* int done with generic move *)
67(*| INT: generic_reg p → Byte → joint_step p globals *)
68  | CLEAR_CARRY: joint_step p globals
69  | SET_CARRY: joint_step p globals
70  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_step p globals
71  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_step p globals
72  | CALL_ID: ident → call_args p → call_dest p → joint_step p globals
73  | COND: acc_a_reg p → label → joint_step p globals
74  | extension: ext_step p → joint_step p globals.
75
76notation "r ← a1 .op. a2" with precedence 55 for
77  @{'op2 $op $r $a1 $a2}.
78notation "r ← . op . a" with precedence 55 for
79  @{'op1 $op $r $a}.
80notation "r ← a" with precedence 55 for
81  @{'mov $r $a}. (* to be set in individual languages *)
82notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
83  @{'opaccs $op $r $s $a1 $a2}.
84
85interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
86interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
87interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
88
89coercion extension_to_step : ∀p,globals.∀s : ext_step p.joint_step p globals ≝
90  extension on _s : ext_step ? to joint_step ??.
91
92definition step_labels ≝
93  λp, globals.λs : joint_step p globals.
94    match s with
95    [ COND _ l ⇒ [l]
96    | extension ext_s ⇒ ext_step_labels ? ext_s
97    | _ ⇒ [ ]
98    ].
99
100definition step_forall_labels : ∀p : step_params.∀globals.
101    (label → Prop) → joint_step p globals → Prop ≝
102λp,g,P,inst. All … P (step_labels … inst).
103 
104record funct_params : Type[1] ≝
105  { resultT : Type[0]
106  ; paramsT : Type[0]
107  }.
108 
109record local_params : Type[1] ≝
110 { funct_pars :> funct_params
111 ; localsT: Type[0]
112 }.
113
114
115record unserialized_params : Type[1] ≝
116 { u_inst_pars :> step_params
117 ; u_local_pars :> local_params
118 }.
119
120record stmt_params : Type[1] ≝
121  { uns_pars :> unserialized_params
122  ; succ : Type[0]
123  ; succ_label : succ → option label
124  }.
125
126inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
127  | sequential: joint_step p globals → succ p → joint_statement p globals
128  | GOTO: label → joint_statement p globals
129  | RETURN: joint_statement p globals
130  | extension_fin : ext_fin_stmt p → joint_statement p globals.
131
132coercion extension_fin_to_stmt : ∀p : stmt_params.∀globals.∀s : ext_fin_stmt p.joint_statement p globals ≝
133  extension_fin on _s : ext_fin_stmt ? to joint_statement ??.
134
135definition no_seq ≝ λp : stmt_params.λglobals.λs : joint_statement p globals.
136  match s with
137  [ sequential _ _ ⇒ False
138  | _ ⇒ True
139  ].
140
141record params : Type[1] ≝
142 { stmt_pars :> stmt_params
143 ; codeT: list ident → Type[0]
144 ; code_point : Type[0]
145 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
146 ; point_of_label : ∀globals.codeT globals → label → option code_point
147 ; point_of_succ : code_point → succ stmt_pars → code_point
148 }.
149
150definition code_has_point ≝
151  λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false].
152
153interpretation "code membership" 'mem p c = (code_has_point ?? c p).
154
155definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
156unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)).
157
158definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code.
159  match pt with
160  [ mk_Sig pt' pt_prf ⇒
161    match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with
162    [ Some x ⇒ λ_.x
163    | None ⇒ λabs.⊥
164    ] (refl …)
165  ]. normalize in pt_prf;
166    >abs in pt_prf; // qed.
167
168definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals)  ≝
169  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s.
170
171definition forall_statements_i :
172  ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) →
173    codeT p globals → Prop  ≝
174  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s.
175
176lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals).
177#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
178
179lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) →
180  ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c.
181#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
182
183definition code_has_label ≝ λp,globals,c,l.
184  match point_of_label p globals c l with
185  [ Some pt ⇒ code_has_point … c pt
186  | None ⇒ false
187  ].
188
189definition stmt_explicit_labels :
190  ∀p,globals.
191  joint_statement p globals → list label ≝
192  λp,globals,stmt. match stmt with
193  [ sequential c _ ⇒ step_labels … c
194  | GOTO l ⇒ [ l ]
195  | RETURN ⇒ [ ]
196  | extension_fin c ⇒ ext_fin_stmt_labels … c
197  ].
198
199definition stmt_implicit_label : ∀p,globals.joint_statement p globals →
200  option label ≝
201 λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?].
202 
203definition stmt_labels : ∀p : stmt_params.∀globals.
204    joint_statement p globals → list label ≝
205  λp,g,stmt.
206  (match stmt_implicit_label … stmt with
207     [ Some l ⇒ [l]
208     | None ⇒ [ ]
209     ]) @ stmt_explicit_labels … stmt.
210
211definition stmt_forall_labels ≝
212  λp, globals.λ P : label → Prop.λs : joint_statement p globals.
213  All … P (stmt_labels … s).
214
215lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals.
216  stmt_forall_labels … P s → All … P (stmt_explicit_labels … s).
217#p#globals#P #s
218whd in ⊢ (% → ?);
219whd in ⊢ (???% → ?);
220elim (stmt_implicit_label ???) [2: #next * #_] //
221qed.
222
223lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals.
224  stmt_forall_labels … P s →
225    opt_All … P (stmt_implicit_label … s).
226#p#globals#P#s
227whd in ⊢ (% → ?);
228whd in ⊢ (???% → ?);
229elim (stmt_implicit_label ???)
230[ //
231| #next * #Pnext #_ @Pnext
232]
233qed.
234
235definition code_forall_labels ≝
236  λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c.
237
238lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) →
239  ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝
240  λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?).
241
242record lin_params : Type[1] ≝
243  { l_u_pars :> unserialized_params }.
244 
245lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
246#tag #A #lbl #l elim l [*]
247** [2: #id] #a #tl #IH
248[ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????);
249  change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????);
250  @eq_identifier_elim #Heq normalize nodelta
251  [ #_ normalize / by /]
252| whd in ⊢ (?%→?%?);
253]
254#H >(index_of_label_from_internal … H)
255@le_S_S @(IH H)
256qed.
257
258(* mv *)
259lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|.
260#A #l elim l normalize [ #n #x #ABS destruct(ABS)]
261#hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by /
262qed.
263
264lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|.
265#A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)]
266#n' #H @le_S_S @(IH … H)
267qed.
268
269lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf).
270#A #l elim l
271[ #n #ABS @⊥ /2 by absurd/
272| #hd #tl #IH * normalize //
273]
274qed.
275
276definition lin_params_to_params ≝
277  λlp : lin_params.
278     mk_params
279      (mk_stmt_params lp unit (λ_.None ?))
280    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
281    (* code_point ≝ *)ℕ
282    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
283    (* point_of_label ≝ *)(λglobals,c,lbl.
284      If occurs_exactly_once ?? lbl c then with prf do
285        return index_of_label ?? lbl c
286      else
287        None ?)
288    (* point_of_succ ≝ *)(λcurrent.λ_.S (current)).
289
290coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
291  on _lp : lin_params to params.
292 
293lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
294  ∀pt.pt ∈ code = leb (S pt) (|code|).
295#lp #globals #code elim code
296[ #pt %
297| #hd #tl #IH * [%]
298  #n @IH
299]qed.
300
301lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
302  ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code.
303#lp #globals #code #lbl
304whd in match (code_has_label ????);
305whd in match (point_of_label ????);
306elim (true_or_false_Prop (occurs_exactly_once ?? lbl code))
307#Heq >Heq normalize nodelta
308[ >lin_code_has_point @(leb_elim (S ?)) [#_ |
309  #ABS elim(absurd ?? ABS) -ABS
310  @index_of_label_length assumption ]] %
311qed.
312
313record graph_params : Type[1] ≝
314  { g_u_pars :> unserialized_params }.
315
316(* move *)
317definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i ∈ m → A ≝
318  λtag,A,m.match m return λx : identifier_map tag A.∀i.i ∈ x → ? with
319  [ an_id_map m' ⇒ λi.match i return λx.x ∈ an_id_map ?? m' → ? with
320    [ an_identifier i' ⇒
321      match lookup_opt … i' m' return λx.match x with [Some y ⇒ true | None ⇒ false] → ? with
322      [ Some y ⇒ λ_.y
323      | None ⇒ Ⓧ
324      ]
325    ]
326  ].
327 
328lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf.
329  (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf).
330#tag #A #P *#m *#i normalize elim (lookup_opt A i m) normalize
331[ * ]
332#s * #H @H %
333qed.
334
335(* One common instantiation of params via Graphs of joint_statements
336   (all languages but LIN) *)
337definition graph_params_to_params ≝
338  λgp : graph_params.
339     mk_params
340      (mk_stmt_params gp label (Some ?))
341    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
342    (* code_point ≝ *)label
343    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
344    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
345    (* point_of_succ ≝ *)(λ_.λlbl.lbl).
346
347coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
348on _gp : graph_params to params.
349
350lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
351  ∀pt.code_has_point … code pt = mem_set … code pt.
352#gp#globals*#m*#i % qed.
353
354lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
355  ∀lbl.code_has_label … code lbl = mem_set … code lbl.
356#gp #globals * #m * #i % qed.
357
358definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop.
359  λs : joint_statement p globals.
360  match s with
361  [ sequential _ n ⇒ P n
362  | _ ⇒ True
363  ].
364
365definition statement_closed : ∀globals.∀p : params.
366  codeT p globals → code_point p → (joint_statement p globals) → Prop ≝
367λglobals,p,code,pt,s.
368  All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧
369  stmt_forall_succ … (λn.bool_to_Prop (point_of_succ ? pt n ∈ code)) s.
370
371definition code_closed : ∀p : params.∀globals.
372  codeT p globals → Prop ≝ λp,globals,code.
373    forall_statements_i … (statement_closed … code) code.
374
375(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
376definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
377  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).
378
379record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
380{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
381  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
382  (* Paolo: if we want this machinery to work for RTLabs too, we will need the
383     following, right? *)
384(*  joint_if_sig: signature;  -- dropped in front end *)
385  joint_if_result   : resultT p;
386  joint_if_params   : paramsT p;
387  joint_if_locals   : list (localsT p); (* use void where no locals are present *)
388(*CSC: XXXXX stacksize unused for LTL-...*)
389  joint_if_stacksize: nat;
390  joint_if_code     : codeT p globals ;
391  joint_if_entry : point_in_code … joint_if_code ;
392  joint_if_exit : point_in_code … joint_if_code
393}.
394
395definition joint_closed_internal_function ≝
396  λglobals,p.
397    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
398
399definition set_joint_code ≝
400  λglobals: list ident.
401  λpars: params.
402  λint_fun: joint_internal_function globals pars.
403  λgraph: codeT pars globals.
404  λentry.
405  λexit.
406    mk_joint_internal_function globals pars
407      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
408      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
409      graph entry exit.
410
411definition set_joint_if_graph ≝
412  λglobals.λpars : graph_params.
413  λgraph.
414  λp:joint_internal_function globals pars.
415  λentry_prf.
416  λexit_prf.
417    set_joint_code globals pars p
418      graph
419      (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
420      (mk_Sig … (joint_if_exit ?? p) exit_prf).
421
422definition set_luniverse ≝
423  λglobals,pars.
424  λp : joint_internal_function globals pars.
425  λluniverse: universe LabelTag.
426   mk_joint_internal_function globals pars
427    luniverse (joint_if_runiverse … p) (joint_if_result … p)
428    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
429    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
430
431definition set_runiverse ≝
432  λglobals,pars.
433  λp : joint_internal_function globals pars.
434  λruniverse: universe RegisterTag.
435   mk_joint_internal_function globals pars
436    (joint_if_luniverse … p) runiverse (joint_if_result … p)
437    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
438    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
439   
440(* Specialized for graph_params *)
441definition add_graph ≝
442  λg_pars : graph_params.λglobals.λl:label.λstmt.
443    λp:joint_internal_function globals g_pars.
444   let code ≝ add … (joint_if_code … p) l stmt in
445    mk_joint_internal_function ? g_pars
446     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
447     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
448     code
449     (pi1 … (joint_if_entry … p))
450     (pi1 … (joint_if_exit … p)).
451>graph_code_has_point whd in match code; >mem_set_add
452@orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ]
453#x #H <graph_code_has_point @H
454qed.
455
456definition set_locals ≝
457  λglobals,pars.
458  λp : joint_internal_function globals pars.
459  λlocals.
460   mk_joint_internal_function globals pars
461    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
462    (joint_if_params … p) locals (joint_if_stacksize … p)
463    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
464
465definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
466
467definition joint_program ≝
468 λp:params. program (λglobals. joint_function globals p) nat.
Note: See TracBrowser for help on using the repository browser.