source: src/Clight/toCminorCorrectness.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 15.7 KB
Line 
1include "Clight/toCminor.ma".
2include "Clight/CexecInd.ma".
3include "common/Globalenvs.ma".
4include "Clight/memoryInjections.ma".
5include "Clight/Clight_abstract.ma".
6include "Cminor/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.