source: src/joint/Joint.ma @ 2645

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