source: src/Clight/toCminorCorrectness.ma @ 2598

Last change on this file since 2598 was 2598, checked in by garnier, 7 years ago

Tentative, partial draft for the definition of Clight-Cminor simulation for statements. Commented out for now.
Also, some stuff on memory injections, and some more aliases on abstract.ma.

File size: 15.7 KB
Line 
1include "Clight/toCminor.ma".
2include "Clight/CexecInd.ma".
3include "common/Globalenvs.ma".
4include "Clight/memoryInjections.ma".
5include "Clight/abstract.ma".
6include "Cminor/abstract.ma".
7
8(* Expr simulation. Contains important definitions for statements, too.  *)
9include "Clight/toCminorCorrectnessExpr.ma".
10
11
12(* When we characterise the local Clight variables, those that are stack
13   allocated are given disjoint regions of the stack. *)
14
15lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
16  characterise_vars globals f = 〈vartypes, stacksize〉 →
17  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
18  ∀id',n',ty'. id ≠ id' →
19  lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
20  n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
21#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
22whd in ⊢ (??%? → ?);
23generalize in match vartypes; -vartypes
24generalize in match stacksize; -stacksize
25elim (args@vars)
26[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
27  elim globals in L;
28  [ normalize #L destruct
29  | * * #id' #r #ty' #tl #IH
30    whd in match (foldr ?????);
31    #L cases (lookup_add_cases ??????? L)
32    [ * #E1 #E2 destruct
33    | @IH
34    ]
35  ]
36| * #id1 #ty1 #tl #IH #stacksize #vartypes
37  whd in match (foldr ?????);
38  (* Avoid writing out the definition again *)
39  letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
40  lapply (refl ? ih) whd in match ih; -ih
41  cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
42  #vartypes' #stack' #FOLD #IH
43  whd in ⊢ (??(match % with [_⇒?])? → ?);
44  cases (orb ??)
45  #CHAR whd in CHAR:(??%?); destruct
46  #L cases (lookup_add_cases ??????? L)
47  [ 1,3: * #E1 #E2 destruct
48    #id' #n' #ty' #NE >lookup_add_miss /2/
49    #L' %1 -L -IH
50    generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
51    generalize in match stack'; -stack'
52    elim tl
53    [ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
54      elim globals in L';
55      [ normalize #E destruct
56      | * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
57        #L cases (lookup_add_cases ??????? L)
58        [ * #E1 #E2 destruct
59        | @IH
60        ]
61      ]
62    | * #id2 #ty2 #tl2 #IH #stack' #vartypes'
63      whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
64      #vartypes2 #stack2 #IH
65      whd in ⊢ (??%? → ?);
66      cases (orb ??)
67      [ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
68        [ * #E1 #E2 destruct //
69        | #L'' lapply (IH ?? (refl ??) L'') /2/
70        ]
71      | #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
72        [ * #E1 #E2 destruct
73        | #L'' lapply (IH ?? (refl ??) L'') /2/
74        ]
75      ]
76    ]
77  | -L #L #id' #n' #ty' #NE #L'
78    cases (lookup_add_cases ??????? L')
79    [ * #E1 #E2 destruct
80      %2 -IH -L'
81      generalize in match vartypes' in FOLD L; -vartypes'
82      generalize in match stack'; -stack'
83      elim tl
84      [ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
85        elim globals in L;
86        [ normalize #E destruct
87        | * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
88          #L cases (lookup_add_cases ??????? L)
89          [ * #E1 #E2 destruct
90          | @IH
91          ]
92        ]
93      | * #id1 #ty1 #tl1 #IH #stack' #vartypes'
94        whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
95        #vartypes2 #stack2 #IH
96        whd in ⊢ (??%? → ?);
97        cases (orb ??)
98        #E whd in E:(??%?); destruct
99        #L cases (lookup_add_cases ??????? L)
100        [ 1,3: * #E1 #E2 destruct //
101        | 2,4: #L' lapply (IH ?? (refl ??) L') /2/
102        ]
103      ]
104    | @(IH … (refl ??) L … NE)
105    ]
106  | -L #L #id' #n' #ty' #NE #L'
107    cases (lookup_add_cases ??????? L')
108    [ * #E1 #E2 destruct
109    | @(IH … (refl ??) L … NE)
110    ]
111  ]
112] qed.
113
114(* And everything is in the stack frame. *)
115
116lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
117  characterise_vars globals f = 〈vartypes, stacksize〉 →
118  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
119  n + sizeof ty ≤ stacksize.
120#globals * #ret #args #vars #body whd in match (characterise_vars ??);
121elim (args@vars)
122[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
123  whd in FOLD:(??%?); destruct elim globals in L;
124  [ #E normalize in E; destruct
125  | * * #id' #r' #ty' #tl' #IH
126    whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
127    [ * #E1 #E2 destruct
128    | @IH
129    ]
130  ]
131| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
132  whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
133  #vartypes' #stackspace' #IH
134  whd in ⊢ (??(match % with [_⇒?])? → ?);
135  cases (orb ??) whd in ⊢ (??%? → ?);
136  #E destruct #L cases (lookup_add_cases ??????? L)
137  [ 1,3: * #E1 #E2 destruct //
138  | 2,4: #L' lapply (IH … (refl ??) L') /2/
139  ]
140] qed.
141
142
143
144(* Put knowledge that Globals are global into a more useful form than the
145   one used for the invariant. *)   
146(* XXX superfluous lemma ? Commenting it for now.
147       if not superfluous : move to toCminorCorrectnessExpr.ma, after
148       [characterise_vars_localid] *)
149(*
150lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
151  characterise_vars globals f = 〈vartypes, stacksize〉 →
152  ∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
153  Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
154  ¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
155#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
156cases (characterise_vars_src … CHAR id ?)
157[ * #r' * #ty' >L
158  * #E1 destruct (E1) #EX
159  %
160  [ @EX
161  | % #EX' cases (characterise_vars_localid … CHAR EX')
162    #ty' whd in ⊢ (% → ?); >L *
163  ]
164| * #ty' whd in ⊢ (% → ?); >L *
165| whd >(opt_eq_from_res ???? L) % #E destruct
166] qed. *)
167
168(* Show how the global environments match up. *)
169
170lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
171  map_partial_All A B P f l H = OK ? l' →
172  All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
173#A #B #P #f #l
174elim l
175[ #H #l' #MAP normalize in MAP; destruct //
176| #h #t #IH * #p #H #l'
177  whd in ⊢ (??%? → ?);
178  lapply (refl ? (f h p)) whd in match (proj1 ???);
179  cases (f h p) in ⊢ (???% → %);
180  [ #b #E #MAP cases (bind_inversion ????? MAP)
181    #tl' * #MAP' #E' normalize in E'; destruct
182    % [ %{p} @E | @IH [ @H | @MAP' ] ]
183  | #m #_ #X normalize in X; destruct
184  ]
185] qed.
186 
187
188definition clight_cminor_matching : clight_program → matching ≝
189λp.
190  let tmpuniverse ≝ universe_for_program p in
191  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
192  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
193  let globals ≝ fun_globals @ var_globals in
194  mk_matching
195    ?? (list init_data × type) (list init_data)
196    (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
197    (λv,w. \fst v = w).
198
199lemma clight_to_cminor_varnames : ∀p,p'.
200  clight_to_cminor p = OK ? p' →
201  prog_var_names … p = prog_var_names … p'.
202* #vars #fns #main * #vars' #fns' #main'
203#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
204whd in E:(??%%); destruct
205-MAP normalize
206elim vars
207[ //
208| * * #id #r * #d #t #tl #IH normalize >IH //
209] qed.
210
211
212lemma clight_to_cminor_matches : ∀p,p'.
213  clight_to_cminor p = OK ? p' →
214  match_program (clight_cminor_matching p) p p'.
215* #vars #fns #main * #vars' #fns' #main'
216#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
217whd in E:(??%%); destruct
218%
219[ -MAP whd in match (m_V ?); whd in match (m_W ?);
220  elim vars
221  [ //
222  | * * #id #r * #init #ty #tl #IH %
223    [ % //
224    | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
225    ]
226  ]
227| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
228  * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
229  normalize in E; destruct
230  <(clight_to_cminor_varnames … TO)
231  % whd
232  % [2: % [2: @TRANSF | skip ] | skip ]
233| %
234] qed.
235
236
237(* This is the statement for expression simulation copied from toCminorCorrectnessExpr.ma,
238   for easier reference.
239lemma eval_expr_sim :
240  (* [cl_cm_inv] maps CL globals to CM globals, including functions *)
241  ∀cl_cm_inv  : clight_cminor_inv.
242  (* current function (defines local environment) *)
243  ∀f          : function.
244  (* [alloctype] maps variables to their allocation type (global, stack, register) *)
245  ∀alloctype  : var_types.
246  ∀stacksize  : ℕ.
247  ∀alloc_hyp  : characterise_vars (globals cl_cm_inv) f = 〈alloctype, stacksize〉.
248  (* environments *)
249  ∀cl_env     : cl_env.
250  ∀cm_env     : cm_env.
251  (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local.  *)
252  ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉.
253  (* CL and CM memories *)
254  ∀cl_m       : mem.
255  ∀cm_m       : mem.
256  (* memory injection and matching *)
257  ∀embed      : embedding.
258  ∀injection  : memory_inj embed cl_m cm_m.
259  ∀stackptr   : block.
260  ∀matching   : memory_matching embed cl_m cm_m cl_env cm_env cl_cm_inv stackptr alloctype.
261  (* clight expr to cminor expr *)
262  (∀(e:expr).
263   ∀(e':CMexpr (typ_of_type (typeof e))).
264   ∀Hexpr_vars.
265   translate_expr alloctype e = OK ? («e', Hexpr_vars») →
266   ∀cl_val,trace,Hyp_present.
267   exec_expr (ge_cl … cl_cm_inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
268   ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
269            value_eq embed cl_val cm_val) ∧
270   (* clight /lvalue/ to cminor /expr/ *)
271  (∀ed,ty.
272   ∀(e':CMexpr ASTptr).
273   ∀Hexpr_vars.
274   translate_addr alloctype (Expr ed ty) = OK ? («e', Hexpr_vars») →
275   ∀cl_blo,cl_off,trace,Hyp_present.
276   exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
277   ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
278            value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val).   
279*)
280
281
282(* TODO: relate Clight continuations and Cminor ones. *)
283(*
284axiom clight_cminor_cont_rel :
285  clight_cminor_inv → cl_cont → cm_cont → block → stack → Prop.
286
287inductive clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop ≝
288| CMR_normal :
289  (* relates globals to globals and functions to functions *)
290  ∀INV:  clight_cminor_inv.
291
292  (* ---- Clight variables ---- *)
293  ∀cl_f: function.                               (* Clight enclosing function *) 
294  ∀cl_s: statement.                                       (* Clight statement *) 
295  ∀cl_k: cl_cont.                                      (* Clight continuation *)
296  ∀cl_e: cl_env.                                        (* Clight environment *)
297
298  (* ---- Cminor variables ---- *) 
299  ∀cl_m: mem.                                                (* Clight memory *)
300  ∀cm_f: internal_function.                             (* enclosing function *)
301  ∀cm_s: stmt.                                            (* Cminor statement *)
302  ∀cm_k: cm_cont.                                       (* Cminor contiuation *)
303  ∀cm_sp: block.                                      (* Cminor stack pointer *)
304  ∀cm_st: stack.                                              (* Cminor stack *)
305  ∀cm_e: cm_env.                                        (* Cminor environment *)
306  ∀cm_m: mem.                                                (* Cminor memory *)
307  ∀fInv: stmt_inv cm_f cm_e (f_body cm_f).               (* Cminor invariants *)
308  ∀sInv: stmt_inv cm_f cm_e cm_s.
309  ∀kInv: cont_inv cm_f cm_e cm_k.
310
311  (* ---- specify the mapping from variables to their alloc type (global, stack, register) ---- *)
312  ∀alloctype:  var_types.                       (* map from var to alloc type *) 
313  ∀stack_cons: ℕ.                              (* stack consumption of [cl_f] *)
314  characterise_vars (globals INV) cl_f = 〈alloctype, stack_cons〉 →  (* spec of [alloctype] *)
315
316  (* ---- linking Clight and Cminor memories ---- *)
317  ∀E: embedding.
318  memory_inj E cl_m cm_m →
319  memory_matching E cl_m cm_m cl_e cm_e INV cm_sp alloctype →
320
321  (* ---- specification of the contents of clight environment (needed for expr sim) ---- *)
322  (* the two memories are those at function entry time. *)
323  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_e,m'〉) → 
324 
325  (* ---- relate Clight and Cminor functions ---- *)
326  ∀func_univ: universe SymbolTag.
327  ∀Hfresh_globals: globals_fresh_for_univ ? (globals INV) func_univ.
328  ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
329  translate_function func_univ (globals INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
330
331  (* ---- relate Clight and Cminor statements ---- *) 
332  ∀stmt_univ: tmpgen alloctype.
333  ∀lbl_univ:  labgen.
334  ∀lbls:      lenv.
335  ∀flag:      convert_flag.
336  ∀outcome:   (Σsu:(tmpgen alloctype)×labgen×stmt.trans_inv alloctype lbls cl_s stmt_univ flag (opttyp_of_type (fn_return cl_f)) su).
337  translate_statement alloctype stmt_univ lbl_univ lbls flag (opttyp_of_type (fn_return cl_f)) cl_s = OK ? outcome →
338  (* TODO decompose outcome *)
339
340  (* ---- relate Clight continuation to Cminor continuation + stack pointer + stack ---- *)
341  clight_cminor_cont_rel INV cl_k cm_k cm_sp cm_st →
342   
343  clight_cminor_rel INV
344    (ClState cl_f cl_s cl_k cl_e cl_m)
345    (CmState cm_f cm_s cm_e fInv sInv cm_m cm_sp cm_k kInv cm_st).
346*)
347
348axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
349
350(* Conjectured simulation results
351
352   We split these based on the start state:
353   
354   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
355      normal steps in Cminor;
356   2. call and return steps are simulated by a call/return step plus [m] normal
357      steps (to copy stack allocated parameters / results); and
358   3. lone cost label steps are simulates by a lone cost label step
359   
360   These should allow us to maintain enough structure to identify the Cminor
361   subtrace corresponding to a measurable Clight subtrace.
362 *)
363
364definition clight_normal : Clight_state → bool ≝
365λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
366
367definition cminor_normal : Cminor_state → bool ≝
368λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
369
370axiom clight_cminor_normal :
371  ∀INV:clight_cminor_inv.
372  ∀s1,s1',s2,tr.
373  clight_cminor_rel INV s1 s1' →
374  clight_normal s1 →
375  ¬ Clight_labelled s1 →
376  ∃n. after_n_steps (S n) … clight_exec (ge_cl INV) s1 (λs.clight_normal s ∧ ¬ Clight_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
377  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
378    tr = tr' ∧
379    clight_cminor_rel INV s2 s2'
380  ).
381
382axiom clight_cminor_call_return :
383  ∀INV:clight_cminor_inv.
384  ∀s1,s1',s2,tr.
385  clight_cminor_rel INV s1 s1' →
386  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
387  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
388  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
389    tr = tr' ∧
390    clight_cminor_rel INV s2 s2'
391  ).
392
393axiom clight_cminor_cost :
394  ∀INV:clight_cminor_inv.
395  ∀s1,s1',s2,tr.
396  clight_cminor_rel INV s1 s1' →
397  Clight_labelled s1 →
398  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
399  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
400    tr = tr' ∧
401    clight_cminor_rel INV s2 s2'
402  ).
403
404axiom clight_cminor_init : ∀cl_program,cm_program,s,s'.
405  clight_to_cminor cl_program = OK ? cm_program →
406  make_initial_state ?? clight_fullexec cl_program = OK ? s →
407  make_initial_state ?? Cminor_fullexec cm_program = OK ? s' →
408  ∃INV. clight_cminor_rel INV s s'.
Note: See TracBrowser for help on using the repository browser.