source: src/Clight/toCminorCorrectness.ma @ 2496

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

Some tentative work on the simulation proof for expressions, in order to adjust the invariant
on memories.

File size: 17.2 KB
Line 
1include "Clight/toCminor.ma".
2
3(* When we characterise the local Clight variables, those that are stack
4   allocated are given disjoint regions of the stack. *)
5
6lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
7  characterise_vars globals f = 〈vartypes, stacksize〉 →
8  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
9  ∀id',n',ty'. id ≠ id' →
10  lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
11  n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
12#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
13whd in ⊢ (??%? → ?);
14generalize in match vartypes; -vartypes
15generalize in match stacksize; -stacksize
16elim (args@vars)
17[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
18  elim globals in L;
19  [ normalize #L destruct
20  | * * #id' #r #ty' #tl #IH
21    whd in match (foldr ?????);
22    #L cases (lookup_add_cases ??????? L)
23    [ * #E1 #E2 destruct
24    | @IH
25    ]
26  ]
27| * #id1 #ty1 #tl #IH #stacksize #vartypes
28  whd in match (foldr ?????);
29  (* Avoid writing out the definition again *)
30  letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
31  lapply (refl ? ih) whd in match ih; -ih
32  cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
33  #vartypes' #stack' #FOLD #IH
34  whd in ⊢ (??(match % with [_⇒?])? → ?);
35  cases (orb ??)
36  #CHAR whd in CHAR:(??%?); destruct
37  #L cases (lookup_add_cases ??????? L)
38  [ 1,3: * #E1 #E2 destruct
39    #id' #n' #ty' #NE >lookup_add_miss /2/
40    #L' %1 -L -IH
41    generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
42    generalize in match stack'; -stack'
43    elim tl
44    [ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
45      elim globals in L';
46      [ normalize #E destruct
47      | * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
48        #L cases (lookup_add_cases ??????? L)
49        [ * #E1 #E2 destruct
50        | @IH
51        ]
52      ]
53    | * #id2 #ty2 #tl2 #IH #stack' #vartypes'
54      whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
55      #vartypes2 #stack2 #IH
56      whd in ⊢ (??%? → ?);
57      cases (orb ??)
58      [ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
59        [ * #E1 #E2 destruct //
60        | #L'' lapply (IH ?? (refl ??) L'') /2/
61        ]
62      | #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
63        [ * #E1 #E2 destruct
64        | #L'' lapply (IH ?? (refl ??) L'') /2/
65        ]
66      ]
67    ]
68  | -L #L #id' #n' #ty' #NE #L'
69    cases (lookup_add_cases ??????? L')
70    [ * #E1 #E2 destruct
71      %2 -IH -L'
72      generalize in match vartypes' in FOLD L; -vartypes'
73      generalize in match stack'; -stack'
74      elim tl
75      [ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
76        elim globals in L;
77        [ normalize #E destruct
78        | * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
79          #L cases (lookup_add_cases ??????? L)
80          [ * #E1 #E2 destruct
81          | @IH
82          ]
83        ]
84      | * #id1 #ty1 #tl1 #IH #stack' #vartypes'
85        whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
86        #vartypes2 #stack2 #IH
87        whd in ⊢ (??%? → ?);
88        cases (orb ??)
89        #E whd in E:(??%?); destruct
90        #L cases (lookup_add_cases ??????? L)
91        [ 1,3: * #E1 #E2 destruct //
92        | 2,4: #L' lapply (IH ?? (refl ??) L') /2/
93        ]
94      ]
95    | @(IH … (refl ??) L … NE)
96    ]
97  | -L #L #id' #n' #ty' #NE #L'
98    cases (lookup_add_cases ??????? L')
99    [ * #E1 #E2 destruct
100    | @(IH … (refl ??) L … NE)
101    ]
102  ]
103] qed.
104
105(* And everything is in the stack frame. *)
106
107lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
108  characterise_vars globals f = 〈vartypes, stacksize〉 →
109  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
110  n + sizeof ty ≤ stacksize.
111#globals * #ret #args #vars #body whd in match (characterise_vars ??);
112elim (args@vars)
113[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
114  whd in FOLD:(??%?); destruct elim globals in L;
115  [ #E normalize in E; destruct
116  | * * #id' #r' #ty' #tl' #IH
117    whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
118    [ * #E1 #E2 destruct
119    | @IH
120    ]
121  ]
122| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
123  whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
124  #vartypes' #stackspace' #IH
125  whd in ⊢ (??(match % with [_⇒?])? → ?);
126  cases (orb ??) whd in ⊢ (??%? → ?);
127  #E destruct #L cases (lookup_add_cases ??????? L)
128  [ 1,3: * #E1 #E2 destruct //
129  | 2,4: #L' lapply (IH … (refl ??) L') /2/
130  ]
131] qed.
132
133(* Local variables show up in the variable characterisation as local. *)
134
135lemma characterise_vars_localid : ∀globals,f,vartypes,stacksize,id.
136  characterise_vars globals f = 〈vartypes, stacksize〉 →
137  Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f) →
138  ∃t. local_id vartypes id t.
139#globals * #ret #args #vars #body
140whd in match (characterise_vars ??); elim (args@vars)
141[ #vartypes #stacksize #id #_ *
142| * #hd #ty #tl #IH
143  #vartypes #stacksize #id
144  whd in match (foldr ?????);
145  cases (foldr ? (Prod ??) ???) in IH ⊢ %;
146  #vartypes' #stackspace' #IH
147  whd in ⊢ (??(match % with [_⇒?])? → ?);
148  cases (orb ??)
149  #E whd in E:(??%?); destruct *
150  [ 1,3: #E destruct %{(typ_of_type ty)}
151    whd whd in match (lookup' ??); >lookup_add_hit //
152  | 2,4: #TL cases (IH … (refl ??) TL) #ty' #LC
153    cases (identifier_eq ? id hd)
154    [ 1,3: #E destruct %{(typ_of_type ty)} whd whd in match (lookup' ??); >lookup_add_hit //
155    | 2,4: #NE %{ty'} whd whd in match (lookup' ??); >lookup_add_miss //
156    ]
157  ]
158] qed.
159
160(* Put knowledge that Globals are global into a more useful form than the
161   one used for the invariant. *)
162
163lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
164  characterise_vars globals f = 〈vartypes, stacksize〉 →
165  ∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
166  Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
167  ¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
168#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
169cases (characterise_vars_src … CHAR id ?)
170[ * #r' * #ty' >L
171  * #E1 destruct (E1) #EX
172  %
173  [ @EX
174  | % #EX' cases (characterise_vars_localid … CHAR EX')
175    #ty' whd in ⊢ (% → ?); >L *
176  ]
177| * #ty' whd in ⊢ (% → ?); >L *
178| whd >(opt_eq_from_res ???? L) % #E destruct
179] qed.
180
181
182(* Show how the global environments match up. *)
183
184lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
185  map_partial_All A B P f l H = OK ? l' →
186  All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
187#A #B #P #f #l
188elim l
189[ #H #l' #MAP normalize in MAP; destruct //
190| #h #t #IH * #p #H #l'
191  whd in ⊢ (??%? → ?);
192  lapply (refl ? (f h p)) whd in match (proj1 ???);
193  cases (f h p) in ⊢ (???% → %);
194  [ #b #E #MAP cases (bind_inversion ????? MAP)
195    #tl' * #MAP' #E' normalize in E'; destruct
196    % [ %{p} @E | @IH [ @H | @MAP' ] ]
197  | #m #_ #X normalize in X; destruct
198  ]
199] qed.
200 
201
202definition clight_cminor_matching : clight_program → matching ≝
203λp.
204  let tmpuniverse ≝ universe_for_program p in
205  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
206  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
207  let globals ≝ fun_globals @ var_globals in
208  mk_matching
209    ?? (list init_data × type) (list init_data)
210    (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
211    (λv,w. \fst v = w).
212
213lemma clight_to_cminor_varnames : ∀p,p'.
214  clight_to_cminor p = OK ? p' →
215  prog_var_names … p = prog_var_names … p'.
216* #vars #fns #main * #vars' #fns' #main'
217#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
218whd in E:(??%%); destruct
219-MAP normalize
220elim vars
221[ //
222| * * #id #r * #d #t #tl #IH normalize >IH //
223] qed.
224
225
226lemma clight_to_cminor_matches : ∀p,p'.
227  clight_to_cminor p = OK ? p' →
228  match_program (clight_cminor_matching p) p p'.
229* #vars #fns #main * #vars' #fns' #main'
230#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
231whd in E:(??%%); destruct
232%
233[ -MAP whd in match (m_V ?); whd in match (m_W ?);
234  elim vars
235  [ //
236  | * * #id #r * #init #ty #tl #IH %
237    [ % //
238    | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
239    ]
240  ]
241| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
242  * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
243  normalize in E; destruct
244  <(clight_to_cminor_varnames … TO)
245  % whd
246  % [2: % [2: @TRANSF | skip ] | skip ]
247| %
248] qed.
249
250include "Clight/Cexec.ma".
251include "Clight/abstract.ma".
252include "Cminor/abstract.ma".
253
254(* Invariants used in simulation *)
255
256record clight_cminor_inv : Type[0] ≝ {
257  globals : list (ident × region × type);
258  ge_cl : genv_t clight_fundef;
259  ge_cm : genv_t (fundef internal_function);
260  eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s;
261  trans_fn : ∀v,f. find_funct … ge_cl v = Some ? f →
262    ∃tmp_u,f',H1,H2.
263      translate_fundef tmp_u globals H1 f H2 = OK ? f' ∧
264      find_funct … ge_cm v = Some ? f'
265}.
266
267include "Clight/CexecInd.ma".
268include "Clight/frontend_misc.ma".
269include "Clight/memoryInjections.ma".
270
271lemma intsize_eq_inversion :
272  ∀sz,sz'.
273  ∀A:Type[0].
274  ∀ok,not_ok.
275  intsize_eq_elim' sz sz' (λsz,sz'. res A)
276                          (OK ? ok)
277                          (Error ? not_ok) = (OK ? ok) →
278  sz = sz'.
279* * try // normalize
280#A #ok #not_ok #Habsurd destruct
281qed.
282
283definition local_matching ≝
284  λE:embedding.
285  λm,m':mem.
286  λen:cl_env.
287  λvenv:cm_env.
288  λsp:block.
289  λvars:var_types.
290
291  ∀id,cl_blo. lookup SymbolTag ? en id = Some ? cl_blo →
292              match lookup ?? vars id with
293              [ Some kind ⇒
294                let 〈vtype, type〉 ≝ kind in
295                match vtype with
296                [ Stack n ⇒
297                  E cl_blo = Some ? 〈sp, offset_of_Z (Z_of_nat n)〉
298                | Local ⇒
299                  ∀v,v'. load_value_of_type type m cl_blo zero_offset = Some ? v →
300                         lookup ?? venv id = Some ? v' →
301                         value_eq E v v'
302                | _ ⇒ False ]
303              | None ⇒ False ].
304
305
306(* TODO : memory injections + link clight env+mem with local env+stack+mem *)
307lemma eval_expr_sim :
308  ∀(inv:clight_cminor_inv).
309
310  ∀(cl_env:cl_env).
311  ∀(cl_m:mem).
312
313  ∀(cm_env:cm_env).
314  ∀(sp:block).
315  ∀(cm_m:mem).
316  ∀(vars:var_types).
317
318  ∀E:embedding.
319  ∀minj:memory_inj E cl_m cm_m.
320  local_matching E cl_m cm_m cl_env cm_env sp vars →
321
322  (∀(e:expr).
323   ∀(e':CMexpr (typ_of_type (typeof e))).
324   (*vars = pi1 … (characterise_vars … [globals] [f]) →*)
325   (*local_matching en m venv sp m' →  *)
326   ∀Hexpr_vars.
327   translate_expr vars e = OK ? («e', Hexpr_vars») →
328   ∀val,trace,Hyp_present.
329   exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈val, trace〉 →
330   eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, val〉) ∧
331
332  (∀ed,ty.
333   ∀(e':CMexpr (typ_of_type ty)).
334   (*vars = pi1 … (characterise_vars … [globals] [f]) →*)
335   (*local_matching en m venv sp m' →  *)
336   ∀Hexpr_vars.
337   translate_expr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
338   ∀resblo,resoff,trace,Hyp_present.
339   exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈resblo, resoff, trace〉 →
340   eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, Vptr (mk_pointer resblo resoff)〉). 
341#inv #cl_env #cl_m #cm_env #sp #cm_m #vars #E #Hinj #Hlocal_matching
342@expr_lvalue_ind_combined
343[ 1: (* Integer constant *)
344  #csz #ty cases ty
345  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
346  | #structname #fieldspec | #unionname #fieldspec | #id ] 
347  #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
348  #val #trace #Hpresent #Hexec_cl
349  whd in Htranslate:(??%?);
350  [ 1,3,4,5,6,7,8: destruct ]
351  (* This intsize_eq_elim' is the proof-equivalent of eating a sandwich with
352     sand inside. *)
353  @cthulhu
354| 2: *
355  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
356  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
357  #ty whd in ⊢ (% → ?); #Hind try @I
358  whd in match (Plvalue ???);
359  whd in match (typeof ?);
360  #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
361  whd in Hexec:(??%?);
362  whd in match (exec_lvalue' ?????) in Hexec:(??%?);
363  cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
364  whd in Hcl_success:(???%);
365  [ 1: (* var case *)
366       lapply Hcl_success -Hcl_success
367       (* Peform case analysis on presence of variable in local Clight env.
368        * if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
369       @(match lookup SymbolTag block cl_env var_id
370         return λx.(lookup SymbolTag block cl_env var_id = x) → ?
371         with
372         [ None ⇒ λHcl_lookup. ?
373         | Some loc ⇒ λHcl_lookup. ?
374         ] (refl ? (lookup SymbolTag block cl_env var_id)))
375       normalize nodelta
376       [ 1: (* global case *)
377            @cthulhu (* TODO: case analysis on lookup in global, if so use Brian's invariant *)
378       | 2: (* local case *)
379            #Heq destruct (Heq)
380            lapply (bind2_eq_inversion ?????? Htranslate_expr)
381            * #var_alloc_type * #var_type *
382            generalize in match var_alloc_type; * normalize nodelta
383            [ 1: (* Global case. This should be contradictory, right ?
384                  * If lookup succeeded, then our local shadows any global with the same
385                  * name, and [characterise_vars] should say so. TODO, this lemma. *)
386                 @cthulhu
387            | 2: (* Stack local *)
388                 #stack_depth #Hlookup_vartype_success * #_
389                 lapply (Hlocal_matching … Hcl_lookup)
390                 whd in Hlookup_vartype_success:(??%?);
391                 lapply (res_inversion ?????? Hlookup_vartype_success)
392                 * * #var_alloc_type' #var_type' * #Hlookup' #Heq destruct (Heq)
393                 >Hlookup' normalize nodelta #Hembedding_eq
394                 (* TODO modify local_invariant to match the needs here *)
395                 @cthulhu
396            | 3: (* Register local *)
397                  #Hlookup_eq * #_
398                 (* TODO : elim type_should_eq, extract type equality, use local_matching *)
399                 @cthulhu
400            ]
401       ]
402  | 2: (* Deref case. Reduce the deref, exhibit the underlying load. *)
403       cases (bind_inversion ????? Hcl_success) -Hcl_success
404       * #cl_subexpr_val #cl_subexpr_trace *
405       whd in ⊢ (? → (???%) → ?);
406       @(match cl_subexpr_val
407         return λx. cl_subexpr_val = x → ?
408         with
409         [ Vundef ⇒ λHval_eq. ?
410         | Vint sz' i ⇒ λHval_eq. ?
411         | Vnull ⇒ λHval_eq. ?
412         | Vptr p ⇒ λHptr_eq. ? ] (refl ? cl_subexpr_val)) normalize nodelta
413       [ 1,2,3: #_ #Habsurd destruct ]
414       #Hcl_exec_to_pointer #Heq destruct (Heq)
415       (* Now that we have executed the Clight part, reduce the Cminor one *)
416       whd in Htranslate_expr:(??%?);
417       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
418       * #cm_expr #Hexpr_vars * #Htranslate_expr
419       whd (* ... *)   @cthulhu
420  | 3: @cthulhu ]
421| *: @cthulhu
422] qed. 
423
424
425
426axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
427
428(* Conjectured simulation results
429
430   We split these based on the start state:
431   
432   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
433      normal steps in Cminor;
434   2. call and return steps are simulated by a call/return step plus [m] normal
435      steps (to copy stack allocated parameters / results); and
436   3. lone cost label steps are simulates by a lone cost label step
437   
438   These should allow us to maintain enough structure to identify the Cminor
439   subtrace corresponding to a measurable Clight subtrace.
440 *)
441
442definition clight_normal : Clight_state → bool ≝
443λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
444
445definition cminor_normal : Cminor_state → bool ≝
446λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
447
448axiom clight_cminor_normal :
449  ∀INV:clight_cminor_inv.
450  ∀s1,s1',s2,tr.
451  clight_cminor_rel INV s1 s1' →
452  clight_normal s1 →
453  ¬ Clight_labelled s1 →
454  ∃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〉) →
455  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
456    tr = tr' ∧
457    clight_cminor_rel INV s2 s2'
458  ).
459
460axiom clight_cminor_call_return :
461  ∀INV:clight_cminor_inv.
462  ∀s1,s1',s2,tr.
463  clight_cminor_rel INV s1 s1' →
464  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
465  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
466  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
467    tr = tr' ∧
468    clight_cminor_rel INV s2 s2'
469  ).
470
471axiom clight_cminor_cost :
472  ∀INV:clight_cminor_inv.
473  ∀s1,s1',s2,tr.
474  clight_cminor_rel INV s1 s1' →
475  Clight_labelled s1 →
476  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
477  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
478    tr = tr' ∧
479    clight_cminor_rel INV s2 s2'
480  ).
481
Note: See TracBrowser for help on using the repository browser.