Changeset 2667 for src


Ignore:
Timestamp:
Feb 14, 2013, 7:10:23 PM (7 years ago)
Author:
garnier
Message:

Clight to Cminor, statements: some cases down. Subset of the simulation relation defined and seems to work.
Some cosmetic changes in toCminorCorrectnessExpr in order to clarify things in toCminorCorrectness.

Location:
src/Clight
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Clight_abstract.ma

    r2601 r2667  
    4747definition cl_eval_expr ≝ eval_expr.
    4848
     49(* creating aliases constructors for states and continuations *)
    4950definition ClState ≝ State.
     51
     52definition ClKseq ≝ Kseq.
  • src/Clight/toCminorCorrectness.ma

    r2601 r2667  
    209209] qed.
    210210
    211 
    212211lemma clight_to_cminor_matches : ∀p,p'.
    213212  clight_to_cminor p = OK ? p' →
     
    242241  (* current function (defines local environment) *)
    243242  ∀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.
     243  ∀data       : clight_cminor_data f cl_cm_inv.
    261244  (* clight expr to cminor expr *)
    262245  (∀(e:expr).
    263246   ∀(e':CMexpr (typ_of_type (typeof e))).
    264247   ∀Hexpr_vars.
    265    translate_expr alloctype e = OK ? («e', Hexpr_vars») →
     248   translate_expr (alloc_type ?? data) e = OK ? («e', Hexpr_vars») →
    266249   ∀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) ∧
     250   exec_expr (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) e = OK ? 〈cl_val, trace〉 →
     251   ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧
     252            value_eq (E ?? data) cl_val cm_val) ∧
    270253   (* clight /lvalue/ to cminor /expr/ *)
    271254  (∀ed,ty.
    272255   ∀(e':CMexpr ASTptr).
    273256   ∀Hexpr_vars.
    274    translate_addr alloctype (Expr ed ty) = OK ? («e', Hexpr_vars») →
     257   translate_addr (alloc_type ?? data) (Expr ed ty) = OK ? («e', Hexpr_vars») →
    275258   ∀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).   
     259   exec_lvalue' (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
     260   ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧
     261            value_eq (E ?? data) (Vptr (mk_pointer cl_blo cl_off)) cm_val).
    279262*)
    280263
    281 
    282 (* TODO: relate Clight continuations and Cminor ones. *)
    283 (*
    284 axiom clight_cminor_cont_rel :
    285   clight_cminor_inv → cl_cont → cm_cont → block → stack → Prop.
    286 
     264definition foo ≝ 3.
     265
     266(* relate Clight continuations and Cminor ones. *)
     267inductive clight_cminor_cont_rel :
     268  ∀INV:  clight_cminor_inv.  (* stuff on global variables and functions (matching between CL and CM) *)
     269  ∀cl_f: function.           (* current Clight function *)
     270  internal_function →        (* current Cminor function *)
     271  clight_cminor_data cl_f INV → (* data for the current stack frame in CL and CM *)
     272  option typ →               (* optional target type - uniform over a given function *)
     273  cl_cont →                  (* CL cont *)
     274  cm_cont →                  (* CM cont *)
     275  Prop ≝
     276| ClCm_cont_stop:
     277  ∀INV, cl_f, cm_f, frame_data, target_type.
     278  clight_cminor_cont_rel INV cl_f cm_f frame_data target_type Kstop Kend
     279| ClCm_cont_seq:
     280  ∀INV, cl_f, cm_f, frame_data, target_type.
     281  ∀cl_s: statement.
     282  ∀cm_s: stmt.
     283  ∀cl_k':  cl_cont.
     284  ∀cm_k':  cm_cont.
     285  ∀stmt_univ, stmt_univ'.
     286  ∀lbl_univ, lbl_univ'.
     287  ∀lbls.
     288  ∀flag.
     289  ∀Htranslate_inv.
     290  translate_statement (alloc_type ?? frame_data) stmt_univ lbl_univ lbls flag target_type cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
     291  clight_cminor_cont_rel INV cl_f cm_f frame_data target_type cl_k' cm_k' →
     292  clight_cminor_cont_rel INV cl_f cm_f frame_data target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k')
     293| ClCm_cont_while:
     294  (* Inductive family parameters *)
     295  ∀INV, cl_f, cm_f, frame_data, target_type.
     296
     297  (* sub-continuations *)
     298  ∀cl_k': cl_cont.
     299  ∀cm_k': cm_cont.
     300
     301  (* elements of the source while statement *)
     302  ∀sz,sg.
     303  ∀cl_cond_desc.
     304  ∀cl_body.
     305
     306  (* elements of the converted while statement *)
     307  ∀cm_cond: CMexpr (ASTint sz sg).
     308  ∀cm_body.
     309  ∀entry,exit: identifier Label.
     310 
     311  (* universes used to generate fresh labels and variables *) 
     312  ∀stmt_univ, stmt_univ'.
     313  ∀lbl_univ, lbl_univ', lbl_univ''.
     314  ∀lbls: lenv.
     315  ∀Htranslate_inv.
     316
     317  (* relate CL and CM expressions *)
     318  ∀Hexpr_vars.
     319  translate_expr (alloc_type ?? frame_data) (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») →
     320
     321  (* Parameters and results to find_label_always *)
     322  ∀sInv: stmt_inv cm_f (cm_env ?? frame_data) (f_body cm_f).
     323  ∀Hinv.
     324
     325  (* Specify how the labels for the while-replacing gotos are produced *)
     326  mklabels lbl_univ = 〈〈entry, exit〉, lbl_univ'〉 →
     327  translate_statement (alloc_type ?? frame_data) stmt_univ lbl_univ' lbls (ConvertTo entry exit) target_type cl_body = OK ? «〈stmt_univ',lbl_univ'',cm_body〉, Htranslate_inv» →
     328  find_label_always entry (f_body cm_f) Kend (proj2 … (proj1 … (proj1 … Hinv))) cm_f (cm_env ?? frame_data) sInv I =
     329    «〈St_label entry
     330          (St_seq
     331            (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
     332            (St_label exit St_skip)), cm_k'〉, Hinv» →
     333  clight_cminor_cont_rel INV cl_f cm_f frame_data target_type cl_k' cm_k' →
     334  clight_cminor_cont_rel INV cl_f cm_f frame_data target_type (Kwhile (Expr cl_cond_desc (Tint sz sg)) cl_body cl_k') (Kseq (St_goto entry) (Kseq (St_label exit St_skip) cm_k')).
     335 
     336
     337(* The type of maps from labels to Clight continuations *)
     338(* definition label_map ≝ identifier_map SymbolTag cont. *)
     339
     340(* Definition of the simulation relation on states. The orders of the parameters is dictated by
     341 * the necessity of performing an inversion on the continuation sim relation without having to
     342 * play the usual game of lapplying all previous dependent arguments.  *)
    287343inductive clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop ≝
    288344| CMR_normal :
    289   (* relates globals to globals and functions to functions *)
     345  (* Relates globals to globals and functions to functions. *)
    290346  ∀INV:  clight_cminor_inv.
    291 
    292   (* ---- Clight variables ---- *)
    293   ∀cl_f: function.                               (* Clight enclosing function *) 
     347 
     348  (* ---- Statements ---- *)
    294349  ∀cl_s: statement.                                       (* Clight statement *) 
     350  ∀cm_s: stmt.                                            (* Cminor statement *)
     351
     352  (* ---- Continuations ---- *)
    295353  ∀cl_k: cl_cont.                                      (* Clight continuation *)
    296   ∀cl_e: cl_env.                                        (* Clight environment *)
    297 
    298   (* ---- Cminor variables ---- *) 
    299   ∀cl_m: mem.                                                (* Clight memory *)
     354  ∀cm_k: cm_cont.                                      (* Cminor continuation *)
     355  ∀cm_st: stack.                                              (* Cminor stack *)
     356 
     357  ∀cl_f: function.                               (* Clight enclosing function *)
    300358  ∀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 →
     359  ∀frame_data: clight_cminor_data cl_f INV.
     360  (*∀alloctype:  var_types.*)                       (* map from var to alloc type *)
     361  ∀rettyp.                                     (* return type of the function *)
     362 
     363  (* ---- Relate Clight continuation to Cminor continuation ---- *)
     364  clight_cminor_cont_rel INV cl_f cm_f frame_data rettyp cl_k cm_k →
     365
     366  (* ---- Other Cminor variables ---- *)
     367  ∀fInv: stmt_inv cm_f (cm_env ?? frame_data) (f_body cm_f).             (* Cminor invariants *)
     368  ∀sInv: stmt_inv cm_f (cm_env ?? frame_data) cm_s.
     369  ∀kInv: cont_inv cm_f (cm_env ?? frame_data) cm_k.
     370
     371  (* ---- Relate return type variable to actual return type ---- *)
     372  rettyp = opttyp_of_type (fn_return cl_f) →
    320373
    321374  (* ---- 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  
     375
    325376  (* ---- relate Clight and Cminor functions ---- *)
    326377  ∀func_univ: universe SymbolTag.
     
    329380  translate_function func_univ (globals INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
    330381
    331   (* ---- relate Clight and Cminor statements ---- *) 
    332   ∀stmt_univ: tmpgen alloctype.
    333   ∀lbl_univ:  labgen.
     382  (* ---- relate Clight and Cminor statements ---- *)
     383  ∀stmt_univ,stmt_univ': tmpgen (alloc_type ?? frame_data).
     384  ∀lbl_univ,lbl_univ':   labgen.
    334385  ∀lbls:      lenv.
    335386  ∀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 →
     387  ∀Htranslate_inv.
     388  translate_statement (alloc_type ?? frame_data) stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
    342389   
    343390  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 
    348 axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
     391    (ClState cl_f cl_s cl_k (cl_env ?? frame_data) (cl_m ?? frame_data))
     392    (CmState cm_f cm_s (cm_env ?? frame_data) fInv sInv (cm_m ?? frame_data) (stackptr ?? frame_data) cm_k kInv cm_st).
     393
     394lemma invert_assert :
     395  ∀b. ∀P. assert b P → b = true ∧ P.
     396* #P whd in ⊢ (% → ?); #H
     397[ @conj try @refl @H
     398| @False_ind @H ]
     399qed.
     400
     401lemma res_to_io :
     402  ∀A,B:Type[0]. ∀C.
     403  ∀x: res A. ∀y.
     404  match x with
     405  [ OK v ⇒  Value B C ? v
     406  | Error m ⇒ Wrong … m ] = return y →
     407  x = OK ? y.
     408#A #B #C *
     409[ #x #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) @refl
     410| #err #y normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
     411qed.
     412
     413
     414(* axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop. *)
    349415
    350416(* Conjectured simulation results
     
    368434λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
    369435
    370 axiom clight_cminor_normal :
     436
     437lemma clight_cminor_normal :
    371438  ∀INV:clight_cminor_inv.
    372439  ∀s1,s1',s2,tr.
    373440  clight_cminor_rel INV s1 s1' →
    374   clight_normal s1
     441  clight_normal s1 = true
    375442  ¬ Clight_labelled s1 →
    376443  ∃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〉) →
     
    379446    clight_cminor_rel INV s2 s2'
    380447  ).
     448#INV #s1 #s1' #s2 #tr #Hstate_rel #Hclight_normal #Hnot_labeleld
     449inversion Hstate_rel
     450#INV' #cl_s
     451(* case analysis on Clight statement *)
     452cases cl_s
     453[ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
     454| 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
     455| 14: #lab | 15: #cost #body ]
     456[ 1: (* Skip *)
     457     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
     458     (* case analysis on continuation *)
     459     inversion Hcont_rel
     460     [ (* Kstop continuation *)
     461       (* simplifying the goal using outcome of the inversion *)
     462       #kINV #kcl_f #kcm_f #kframe_data #ktarget_type #Heq_INV
     463       #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k  #_
     464       (* get rid of jmeqs and destruct *)
     465       lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
     466       lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
     467       destruct (Heq_INV Heq_cl_f)
     468       lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
     469       lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
     470       lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettypv
     471       lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
     472       lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k
     473       destruct (Heq_frame Heq_cl_k Heq_cm_k Heq_cm_f Heq_rettyp)
     474       (* introduce everything *)
     475       #fInv #sInv #kInv
     476       #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     477       #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
     478       #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
     479       #Hreturn_ok #Hlabel_wf
     480       (* reduce statement translation function *)
     481       whd in ⊢ ((??%?) → ?);
     482       #Heq_translate
     483       (* In this simple case, trivial translation *)
     484       destruct (Heq_translate)
     485       #Heq_INV' #Heq_s1 #Heq_s1'
     486       lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
     487       lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
     488       lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1'
     489       destruct (Heq_INV' Heq_s1 Heq_s1') #_
     490       (* unfold the clight execution *)
     491       %{0}
     492       whd in ⊢ (% → ?); whd in match (step io_out io_in clight_exec ??);
     493       inversion (fn_return kcl_f) normalize nodelta
     494       [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     495       | #structname #fieldspec | #unionname #fieldspec | #id ]
     496       #Hfn_return
     497       whd in ⊢ (% → ?);
     498       @False_ind
     499    | (* KSeq continuation *)
     500      #kINV #kcl_f #kcm_f #kframe_data #ktarget_type #kcl_s #kcm_s #kcl_k' #kcm_k'
     501      #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
     502      * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
     503      #kHreturn_ok #kHlabel_wf #kHeq_translate #kHcont_rel #_
     504      #Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k  #_
     505      (* get rid of jmeqs and destruct *)
     506      lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
     507      lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
     508      destruct (Heq_INV Heq_cl_f)
     509      lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
     510      lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
     511      lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettypv
     512      lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
     513      lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k
     514      destruct (Heq_frame Heq_cl_k Heq_cm_k Heq_cm_f Heq_rettyp)   
     515      #fInv #sInv #kInv #Hktarget_type
     516      #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     517      #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
     518      #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
     519      #Hreturn_ok #Hlabel_wf
     520      (* reduce translation function and eliminate result *)
     521      (* In this simple case, trivial translation *)
     522      whd in ⊢ ((??%?) → ?); #Heq_translate
     523      destruct (Heq_translate)
     524      #Heq_INV' #Heq_s1 #Heq_s1'
     525      lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
     526      lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
     527      lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1' #_
     528      (* unfold the clight execution *)
     529      %{0}
     530      whd in ⊢ (% → ?); #Hassert
     531      cases (invert_assert ?? Hassert) -Hassert #Hclight_class
     532      cases (andb_inversion … Hclight_class) -Hclight_class
     533      #_ #Hnot_labelled whd in ⊢ (% → ?); #Heq destruct (Heq)
     534      %{0} whd in ⊢ %; @conj try @refl
     535      (* close simulation *)
     536      %1{kINV kHcont_rel ? ? Hfresh_globals Hfresh_function
     537         Htranslate_function kstmt_univ kstmt_univ' klbl_univ klbl_univ' klbls kflag}
     538      [ 3: @kHeq_translate | assumption ]
     539    | (* Kwhile continuation *)
     540      #kINV #kcl_f #kcm_f #kframe_data #ktarget_type
     541      #kcl_k' #kcm_k' #ksz #ksg #kcl_cond_desc #kcl_body #kcm_cond #kcm_body
     542      #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ''
     543      #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv
     544      * * * * #kHentry_declared * * * *
     545      * * * #kHcond_vars_declared * * * *
     546      * * * #kHbody_inv * * *
     547      whd in ⊢ (% → ?); #kHentry_declared'
     548      * * * * * * * * *
     549      whd in ⊢ (% → ?); #kHexit_declared *
     550      * * * *
     551      #kHcont_inv #kHmklabels #kHeq_translate #kHfind_label #kHcont_rel #_
     552      #Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cm_k #Heq_cl_k
     553      lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
     554      lapply (jmeq_to_eq ??? Heq_cl_f) -Heq_cl_f #Heq_cl_f
     555      destruct (Heq_INV Heq_cl_f)     
     556      lapply (jmeq_to_eq ??? Heq_cm_f) -Heq_cm_f #Heq_cm_f
     557      lapply (jmeq_to_eq ??? Heq_frame) -Heq_frame #Heq_frame
     558      lapply (jmeq_to_eq ??? Heq_rettyp) -Heq_rettyp #Heq_rettyp
     559      lapply (jmeq_to_eq ??? Heq_cm_k) -Heq_cm_k #Heq_cm_k
     560      lapply (jmeq_to_eq ??? Heq_cl_k) -Heq_cl_k #Heq_cl_k #_
     561      destruct (Heq_cl_k Heq_cm_k Heq_cm_f Heq_frame Heq_rettyp)
     562      (* introduce state relation contents *)
     563      #fInv #sInv * whd in ⊢ (% → ?); * *
     564      whd in ⊢ (% → ?); * whd in ⊢ (% → ?); #Hlabel_defined * #kInv
     565      #Heq_rettyp
     566      #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     567      #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
     568      #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
     569      #Hreturn_ok #Hlabel_wf
     570      (* reduce translation function and eliminate result *)
     571      (* In this simple case, trivial translation *)
     572      whd in ⊢ ((??%?) → ?); #Heq_translate
     573      destruct (Heq_translate)
     574      #Heq_INV' #Heq_s1 #Heq_s1'
     575      lapply (jmeq_to_eq ??? Heq_INV') -Heq_INV' #Heq_INV'
     576      lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
     577      lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1' #_
     578      (* unfold the clight execution *)
     579      %{1} whd in ⊢ (% → ?); #Hawait
     580      cases (await_value_bind_inv … Hawait) -Hawait
     581      * #cl_val #cl_trace * #Hexec_cond #Hawait
     582      cases (await_value_bind_inv … Hawait) -Hawait
     583      #cond_outcome * #Hcond_outcome
     584      cases (eval_expr_sim … kframe_data) #Hsim_expr #_
     585      (* use simulation lemma on expressions *)
     586      lapply (Hsim_expr … kHtranslate_expr … kHcond_vars_declared … Hexec_cond) -Hsim_expr
     587      whd in match (typeof ?) in Hcond_outcome; cases cond_outcome in Hcond_outcome;
     588      #Hcond_outcome lapply (exec_bool_of_val_inversion … Hcond_outcome)
     589      * [ 2,4: * #ptr * #ty' * * #_ #Habsurd destruct (Habsurd) ]
     590      * [ 2,4: * #ty' * * #_ #Habsurd destruct (Habsurd) ]
     591      * #vsz * #vsg * #i * * #Hcl_val #Htype_eq destruct (Hcl_val Htype_eq)
     592      normalize nodelta #Hi_eq
     593      * #cm_val * #Hexec_cond_cm #Hvalue_eq #Hassert
     594      cases (invert_assert … Hassert) -Hassert #Handb
     595      cases (andb_inversion … Handb) -Handb #_ #HClight_not_labelled
     596      whd in ⊢ (% → ?); #Heq destruct (Heq)
     597      [ %{5} whd whd in ⊢ (??%?); normalize nodelta
     598        >kHfind_label -kHfind_label normalize nodelta
     599        whd in match (proj1 ???);
     600        whd in match (proj2 ???);
     601        whd whd in ⊢ (??%?); normalize nodelta
     602        >Hexec_cond_cm normalize nodelta
     603        whd in match (m_bind ?????);
     604        >(value_eq_int_inversion … Hvalue_eq)
     605        whd in match (eval_bool_of_val ?); normalize nodelta
     606        <Hi_eq normalize nodelta
     607        whd @conj [ normalize >append_nil try @refl ]
     608        whd in match (proj1 ???);
     609        whd in match (proj2 ???);
     610        whd whd in ⊢ (??%?); normalize nodelta
     611        %{??????? kframe_data ktarget_type Hcont_rel Heq_rettyp ??? Htranslate_function
     612          ??????? kHeq_translate}
     613      | %{6} whd whd in ⊢ (??%?); normalize nodelta
     614        >kHfind_label -kHfind_label normalize nodelta
     615        whd in match (proj1 ???);
     616        whd in match (proj2 ???);
     617        whd whd in ⊢ (??%?); normalize nodelta
     618        >Hexec_cond_cm normalize nodelta
     619        whd in match (m_bind ?????);
     620        >(value_eq_int_inversion … Hvalue_eq)
     621        whd in match (eval_bool_of_val ?); normalize nodelta
     622        <Hi_eq normalize nodelta
     623        whd @conj [ normalize >append_nil >append_nil try @refl ]
     624        whd in match (proj1 ???);
     625        whd in match (proj2 ???);
     626        whd whd in ⊢ (??%?); normalize nodelta
     627        %{??????? kframe_data ktarget_type kHcont_rel Heq_rettyp ??? Htranslate_function}
     628        try assumption
     629        [ @conj try @conj try @conj try @conj //
     630        | @refl ]
     631      ]
     632  (*| TODO: other continuations *)
     633    ]
     634| 2: (* Assign *)
     635     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
     636     #fInv #sInv #kInv #Hrettyp #func_univ #Hfresh_globals #Hfresh_function
     637     #Htranslate_function #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls #flag
     638     * * * * #Hstmt_inv_cm #Huseless_hypothesis
     639      #Htmps_preserved #Hreturn_ok #Hlabel_wf     
     640     (* case-split on lhs in order to reduce lvalue production in Cminor *)
     641     cases lhs #lhs_ed #lhs_ty
     642     cases lhs_ed
     643     (* intro expr contents *)
     644     [ #sz #i | #var_id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
     645     | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
     646     [ 2: #Htranslate_statement
     647          cases (bind_inversion ????? Htranslate_statement)
     648          * #cm_rhs #Hexpr_vars_rhs * #Htranslate_rhs #Htranslate_statement'
     649          cases (bind_inversion ????? Htranslate_statement')
     650          #lhs_dest * #Htranslate_lhs
     651          cases (bind2_eq_inversion ?????? Htranslate_lhs) -Htranslate_lhs
     652          #alloctype * #type_of_var * #Hlookup_var_success
     653          cases alloctype in Hlookup_var_success;
     654          normalize nodelta
     655          [ 1: (* Global *) #r
     656               #Hlookup_var_success whd in ⊢ ((???%) → ?); #Hlhs_dest_eq
     657               destruct (Hlhs_dest_eq) normalize nodelta
     658               whd in match (proj1 ???); whd in match (proj2 ???);
     659               whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     660               #Heq_INV #Heq_s1 #Heq_s1'
     661               lapply (jmeq_to_eq ??? Heq_INV) -Heq_INV #Heq_INV
     662               lapply (jmeq_to_eq ??? Heq_s1) -Heq_s1 #Heq_s1
     663               lapply (jmeq_to_eq ??? Heq_s1') -Heq_s1' #Heq_s1'
     664               destruct (Heq_INV Heq_s1 Heq_s1') #_
     665               %{1} whd in ⊢ (% → ?); #Hawait
     666               cases (await_value_bind_inv … Hawait) -Hawait
     667               * * #cl_blo #cl_off #cl_tr * whd in ⊢ ((??%?) → ?);
     668               #Hexec_lvalue
     669               lapply (res_to_io ????? Hexec_lvalue) -Hexec_lvalue #Hexec_lvalue
     670               #Hawait
     671               cases (await_value_bind_inv … Hawait) -Hawait
     672               * #rhs_val #rhs_trace * #Hexec_rhs_trace #Hawait
     673               cases (await_value_bind_inv … Hawait) -Hawait
     674               #mem_after_store * #Hstore_value #Hawait
     675               lapply (opt_to_io_Value ?????? Hstore_value) -Hstore_value #Hstore_value
     676               -Htranslate_statement' -Htranslate_statement
     677               cases (invert_assert … Hawait) -Hawait #Handb
     678               cases (andb_inversion … Handb) -Handb #_ #HClight_not_labelled #Hawait               
     679               (* TODO: use the memory injection to handle the store,
     680                  use INV contents to match up CL global with CM one.
     681                  Note to self: globals should be exactly matched in CL and CM,
     682                  maybe memory_injection is not useful in this particular case,
     683                  only in Stack and Local cases.
     684                * *)
     685               @cthulhu
     686          | 2: (* Stack *) #n @cthulhu
     687          | 3: (* Local *) @cthulhu
     688          ]
     689     | *: (* memdest *) @cthulhu ]     
     690| *: @cthulhu
     691] qed.
    381692
    382693axiom clight_cminor_call_return :
  • src/Clight/toCminorCorrectnessExpr.ma

    r2608 r2667  
    389389qed.
    390390
     391record clight_cminor_data (f : function) (INV : clight_cminor_inv) : Type[0] ≝
     392{ alloc_type  : var_types;
     393  stacksize   : ℕ;
     394  alloc_hyp   : characterise_vars (globals INV) f = 〈alloc_type, stacksize〉;
     395  (* environments *)
     396  cl_env      : cl_env;
     397  cm_env      : cm_env;
     398  (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local.  *)
     399  cl_env_hyp  : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉;
     400  (* CL and CM memories *)
     401  cl_m        : mem;
     402  cm_m        : mem;
     403  (* memory injection and matching *)
     404  E           : embedding;
     405  injection   : memory_inj E cl_m cm_m;
     406  stackptr    : block;
     407  matching    : memory_matching E cl_m cm_m cl_env cm_env INV stackptr alloc_type
     408}.
    391409
    392410(* -------------------------------------------------------------------- *)
     
    398416  (* current function (defines local environment) *)
    399417  ∀f          : function.
    400   (* [alloctype] maps variables to their allocation type (global, stack, register) *)
    401   ∀alloctype  : var_types.
    402   ∀stacksize  : ℕ.
    403   ∀alloc_hyp  : characterise_vars (globals cl_cm_inv) f = 〈alloctype, stacksize〉.
    404   (* environments *)
    405   ∀cl_env     : cl_env.
    406   ∀cm_env     : cm_env.
    407   (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local.  *)
    408   ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉.
    409   (* CL and CM memories *)
    410   ∀cl_m       : mem.
    411   ∀cm_m       : mem.
    412   (* memory injection and matching *)
    413   ∀embed      : embedding.
    414   ∀injection  : memory_inj embed cl_m cm_m.
    415   ∀stackptr   : block.
    416   ∀matching   : memory_matching embed cl_m cm_m cl_env cm_env cl_cm_inv stackptr alloctype.
     418  ∀data       : clight_cminor_data f cl_cm_inv.
    417419  (* clight expr to cminor expr *)
    418420  (∀(e:expr).
    419421   ∀(e':CMexpr (typ_of_type (typeof e))).
    420422   ∀Hexpr_vars.
    421    translate_expr alloctype e = OK ? («e', Hexpr_vars») →
     423   translate_expr (alloc_type ?? data) e = OK ? («e', Hexpr_vars») →
    422424   ∀cl_val,trace,Hyp_present.
    423    exec_expr (ge_cl … cl_cm_inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
    424    ∃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〉 ∧
    425             value_eq embed cl_val cm_val) ∧
     425   exec_expr (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) e = OK ? 〈cl_val, trace〉 →
     426   ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧
     427            value_eq (E ?? data) cl_val cm_val) ∧
    426428   (* clight /lvalue/ to cminor /expr/ *)
    427429  (∀ed,ty.
    428430   ∀(e':CMexpr ASTptr).
    429431   ∀Hexpr_vars.
    430    translate_addr alloctype (Expr ed ty) = OK ? («e', Hexpr_vars») →
     432   translate_addr (alloc_type ?? data) (Expr ed ty) = OK ? («e', Hexpr_vars») →
    431433   ∀cl_blo,cl_off,trace,Hyp_present.
    432    exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
    433    ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
    434             value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val).
    435 #inv #f #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching
     434   exec_lvalue' (ge_cl … cl_cm_inv) (cl_env ?? data) (cl_m ?? data) ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
     435   ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' (cm_env ?? data) Hyp_present (stackptr ?? data) (cm_m ?? data) = OK ? 〈trace, cm_val〉 ∧
     436            value_eq (E ?? data) (Vptr (mk_pointer cl_blo cl_off)) cm_val).
     437#inv #f * #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching
    436438@expr_lvalue_ind_combined
    437439[ 7: (* binary ops *)
Note: See TracChangeset for help on using the changeset viewer.