source: src/joint/Joint.ma @ 2490

Last change on this file since 2490 was 2490, checked in by tranquil, 7 years ago

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

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