Changeset 2737


Ignore:
Timestamp:
Feb 26, 2013, 7:37:41 PM (7 years ago)
Author:
garnier
Message:

Commit of current proof state for Clight to Cminor translation.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Clight_abstract.ma

    r2677 r2737  
    5050definition ClState ≝ State.
    5151
     52definition ClReturnstate ≝ Returnstate.
     53
     54definition ClCallstate ≝ Callstate.
     55
    5256definition ClKseq ≝ Kseq.
  • src/Clight/toCminorCorrectness.ma

    r2667 r2737  
    55include "Clight/Clight_abstract.ma".
    66include "Cminor/Cminor_abstract.ma".
     7include "common/Measurable.ma".
    78
    89(* Expr simulation. Contains important definitions for statements, too.  *)
    910include "Clight/toCminorCorrectnessExpr.ma".
    1011
    11 
    1212(* When we characterise the local Clight variables, those that are stack
    1313   allocated are given disjoint regions of the stack. *)
    14 
    1514lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
    1615  characterise_vars globals f = 〈vartypes, stacksize〉 →
     
    233232] qed.
    234233
    235 
    236 (* This is the statement for expression simulation copied from toCminorCorrectnessExpr.ma,
    237    for easier reference.
    238 lemma eval_expr_sim :
    239   (* [cl_cm_inv] maps CL globals to CM globals, including functions *)
    240   ∀cl_cm_inv  : clight_cminor_inv.
    241   (* current function (defines local environment) *)
    242   ∀f          : function.
    243   ∀data       : clight_cminor_data f cl_cm_inv.
    244   (* clight expr to cminor expr *)
    245   (∀(e:expr).
    246    ∀(e':CMexpr (typ_of_type (typeof e))).
    247    ∀Hexpr_vars.
    248    translate_expr (alloc_type ?? data) e = OK ? («e', Hexpr_vars») →
    249    ∀cl_val,trace,Hyp_present.
    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) ∧
    253    (* clight /lvalue/ to cminor /expr/ *)
    254   (∀ed,ty.
    255    ∀(e':CMexpr ASTptr).
    256    ∀Hexpr_vars.
    257    translate_addr (alloc_type ?? data) (Expr ed ty) = OK ? («e', Hexpr_vars») →
    258    ∀cl_blo,cl_off,trace,Hyp_present.
    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).
    262 *)
    263 
    264 definition foo ≝ 3.
     234(* A measure on Clight states that is decreasing along execution sequences *)
     235
     236(* statements *)
     237let rec measure_Clight_statement (s : statement) : ℕ ≝
     238match s with
     239[ Sskip ⇒ 0
     240| Ssequence s1 s2 ⇒
     241  measure_Clight_statement s1 + measure_Clight_statement s2 + 1
     242| Sifthenelse e s1 s2 =>
     243  measure_Clight_statement s1 + measure_Clight_statement s2 + 1
     244| Swhile e s =>
     245  measure_Clight_statement s + 1
     246| Sdowhile e s =>
     247  measure_Clight_statement s + 1
     248| Sfor s1 e s2 s3 =>
     249  measure_Clight_statement s1 +
     250  measure_Clight_statement s2 +
     251  measure_Clight_statement s3 + 1
     252| Sswitch e ls =>
     253  measure_Clight_ls ls + 1
     254| Slabel l s =>
     255  measure_Clight_statement s + 1
     256| Scost cl s =>
     257  measure_Clight_statement s + 1
     258| _ => 1
     259]
     260and measure_Clight_ls (ls : labeled_statements) : ℕ :=
     261match ls with
     262[ LSdefault s =>
     263  measure_Clight_statement s
     264| LScase sz i s ls =>
     265  measure_Clight_statement s +
     266  measure_Clight_ls ls
     267].
     268
     269(* continuations *)
     270let rec measure_Clight_cont (cont : cl_cont) : ℕ ≝
     271match cont with
     272[ Kstop => 0
     273| Kseq s k =>
     274  measure_Clight_statement s +
     275  measure_Clight_cont k + 1
     276| Kwhile e s k =>
     277  measure_Clight_statement s +
     278  measure_Clight_cont k + 1
     279| Kdowhile e s k =>
     280  measure_Clight_statement s +
     281  measure_Clight_cont k + 1
     282| Kfor2 e s1 s2 k =>
     283  measure_Clight_statement s1 +
     284  measure_Clight_statement s2 +
     285  measure_Clight_cont k + 1
     286| Kfor3 e s1 s2 k =>
     287  measure_Clight_statement s1 +
     288  measure_Clight_statement s2 +
     289  measure_Clight_cont k + 1
     290| Kswitch k =>
     291  measure_Clight_cont k + 1
     292| Kcall retaddr f e k =>
     293  measure_Clight_statement (fn_body f) +
     294  measure_Clight_cont k + 1
     295].
     296
     297(* Shamelessly copying Compcert. *)
     298definition measure_Clight : Clight_state → ℕ × ℕ ≝
     299λstate.
     300match state with
     301[ State f s k e m ⇒
     302  〈measure_Clight_statement s + measure_Clight_cont k + 1, measure_Clight_statement s + 1〉
     303| Callstate fb fd args k m ⇒ 〈0, 0〉
     304| Returnstate res k m ⇒ 〈0, 0〉
     305| Finalstate r ⇒ 〈0, 0〉
     306].
     307
     308(* Stuff on lexicographic orders *)
     309definition lexicographic : ∀A:Type[0]. (A → A → Prop) → A × A → A × A → Prop ≝
     310λA,Ord, x, y.
     311  let 〈xa, xb〉 ≝ x in
     312  let 〈ya, yb〉 ≝ y in
     313  Ord xa ya ∨ (xa = ya ∧ Ord xb yb).
     314
     315definition lex_lt ≝ lexicographic nat lt.
     316
    265317
    266318(* relate Clight continuations and Cminor ones. *)
    267319inductive 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 *)
     320  ∀cl_ge, cm_ge.
     321  ∀INV:  clight_cminor_inv cl_ge cm_ge.     (* stuff on global variables and functions (matching between CL and CM) *)
     322  ∀cl_f: function.                          (* current Clight function *)
     323  internal_function →                       (* current Cminor function *)
     324  clight_cminor_data cl_f cl_ge cm_ge INV → (* data for the current stack frame in CL and CM *)
     325  option typ →                              (* optional target type - uniform over a given function *)
     326  cl_cont →                                 (* CL cont *)
     327  cm_cont →                                 (* CM cont *)
    275328  Prop ≝
    276329| 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
     330  ∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type.
     331  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type Kstop Kend
    279332| ClCm_cont_seq:
    280   ∀INV, cl_f, cm_f, frame_data, target_type.
     333  ∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type.
    281334  ∀cl_s: statement.
    282335  ∀cm_s: stmt.
     
    288341  ∀flag.
    289342  ∀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')
     343  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» →
     344  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type cl_k' cm_k' →
     345  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type (ClKseq cl_s cl_k') (Kseq cm_s cm_k')
    293346| ClCm_cont_while:
    294347  (* Inductive family parameters *)
    295   ∀INV, cl_f, cm_f, frame_data, target_type.
     348  ∀cl_ge, cm_ge, INV, cl_f, cm_f, frame_data, target_type.
    296349
    297350  (* sub-continuations *)
     
    317370  (* relate CL and CM expressions *)
    318371  ∀Hexpr_vars.
    319   translate_expr (alloc_type ?? frame_data) (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») →
     372  translate_expr (alloc_type frame_data) (Expr cl_cond_desc (Tint sz sg)) = OK ? («cm_cond, Hexpr_vars») →
    320373
    321374  (* Parameters and results to find_label_always *)
    322   ∀sInv: stmt_inv cm_f (cm_env ?? frame_data) (f_body cm_f).
     375  ∀sInv: stmt_inv cm_f (cm_env frame_data) (f_body cm_f).
    323376  ∀Hinv.
    324377
    325378  (* Specify how the labels for the while-replacing gotos are produced *)
    326379  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 =
     380  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» →
     381  find_label_always entry (f_body cm_f) Kend (proj2 … (proj1 … (proj1 … Hinv))) cm_f (cm_env frame_data) sInv I =
    329382    «〈St_label entry
    330383          (St_seq
    331384            (St_ifthenelse ?? cm_cond (St_seq cm_body (St_goto entry)) St_skip)
    332385            (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. *)
     386  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data target_type cl_k' cm_k' →
     387  clight_cminor_cont_rel cl_ge cm_ge 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')).
    339388
    340389(* Definition of the simulation relation on states. The orders of the parameters is dictated by
    341390 * the necessity of performing an inversion on the continuation sim relation without having to
    342391 * play the usual game of lapplying all previous dependent arguments.  *)
    343 inductive clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop ≝
     392inductive clight_cminor_rel : ∀cl_ge, cm_ge. clight_cminor_inv cl_ge cm_ge → Clight_state → Cminor_state → Prop ≝
    344393| CMR_normal :
     394  ∀cl_ge, cm_ge.
    345395  (* Relates globals to globals and functions to functions. *)
    346   ∀INV:  clight_cminor_inv.
     396  ∀INV:  clight_cminor_inv cl_ge cm_ge.
    347397 
    348398  (* ---- Statements ---- *)
     
    357407  ∀cl_f: function.                               (* Clight enclosing function *)
    358408  ∀cm_f: internal_function.                             (* enclosing function *)
    359   ∀frame_data: clight_cminor_data cl_f INV.
    360   (*∀alloctype:  var_types.*)                       (* map from var to alloc type *)
     409  ∀frame_data: clight_cminor_data cl_f ?? INV.
    361410  ∀rettyp.                                     (* return type of the function *)
    362411 
    363412  (* ---- Relate Clight continuation to Cminor continuation ---- *)
    364   clight_cminor_cont_rel INV cl_f cm_f frame_data rettyp cl_k cm_k →
     413  clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data rettyp cl_k cm_k →
    365414
    366415  (* ---- 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.
     416  ∀fInv: stmt_inv cm_f (cm_env frame_data) (f_body cm_f).             (* Cminor invariants *)
     417  ∀sInv: stmt_inv cm_f (cm_env frame_data) cm_s.
     418  ∀kInv: cont_inv cm_f (cm_env frame_data) cm_k.
    370419
    371420  (* ---- Relate return type variable to actual return type ---- *)
     
    376425  (* ---- relate Clight and Cminor functions ---- *)
    377426  ∀func_univ: universe SymbolTag.
    378   ∀Hfresh_globals: globals_fresh_for_univ ? (globals INV) func_univ.
     427  ∀Hfresh_globals: globals_fresh_for_univ ? (globals ?? INV) func_univ.
    379428  ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
    380   translate_function func_univ (globals INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
     429  translate_function func_univ (globals ?? INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
    381430
    382431  (* ---- relate Clight and Cminor statements ---- *)
    383   ∀stmt_univ,stmt_univ': tmpgen (alloc_type ?? frame_data).
     432  ∀stmt_univ,stmt_univ': tmpgen (alloc_type frame_data).
    384433  ∀lbl_univ,lbl_univ':   labgen.
    385434  ∀lbls:      lenv.
    386435  ∀flag:      convert_flag.
    387436  ∀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» →
     437  translate_statement (alloc_type frame_data) stmt_univ lbl_univ lbls flag rettyp cl_s = OK ? «〈stmt_univ',lbl_univ',cm_s〉, Htranslate_inv» →
    389438   
    390   clight_cminor_rel INV
    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).
     439  clight_cminor_rel cl_ge cm_ge INV
     440    (ClState cl_f cl_s cl_k (cl_env … frame_data) (cl_m … frame_data))
     441    (CmState cm_f cm_s (cm_env … frame_data) fInv sInv (cm_m … frame_data) (stackptr … frame_data) cm_k kInv cm_st)
     442
     443| CMR_return :
     444  ∀cl_ge, cm_ge, cl_f.
     445  ∀INV:  clight_cminor_inv cl_ge cm_ge.
     446  ∀frame_data: clight_cminor_data cl_f ?? INV.
     447  ∀cl_mem, cm_mem.
     448  cl_mem = cl_m … frame_data →
     449  cm_mem = cm_m … frame_data →
     450  ∀cm_st: stack.                                              (* Cminor stack *)
     451  clight_cminor_rel cl_ge cm_ge INV
     452    (ClReturnstate Vundef Kstop cl_mem)
     453    (CmReturnstate (None val) cm_mem cm_st)
     454   
     455| CMR_call :
     456 ∀cl_ge, cm_ge, cl_f, cm_f.
     457 ∀INV: clight_cminor_inv cl_ge cm_ge.
     458 ∀frame_data: clight_cminor_data cl_f cl_ge cm_ge INV.
     459 ∀u: universe SymbolTag.
     460 ∀cl_fundef, cm_fundef.
     461 ∀Hglobals_fresh: globals_fresh_for_univ type (globals cl_ge cm_ge INV) u.
     462 ∀Hfundef_fresh:  fd_fresh_for_univ cl_fundef u.
     463 ∀rettyp. rettyp = opttyp_of_type (fn_return cl_f) →
     464 ∀cl_k, cm_k.
     465 clight_cminor_cont_rel cl_ge cm_ge INV cl_f cm_f frame_data rettyp cl_k cm_k →
     466 ∀fblock.
     467 match cl_fundef with
     468 [ CL_Internal cl_function ⇒
     469   find_funct clight_fundef cl_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? (CL_Internal cl_function) ∧
     470   find_funct (fundef internal_function) cm_ge (Vptr (mk_pointer fblock zero_offset)) = Some ? cm_fundef ∧
     471   translate_fundef u (globals ?? INV) Hglobals_fresh cl_fundef Hfundef_fresh = OK ? cm_fundef
     472 | CL_External name argtypes rettype ⇒
     473   True
     474 ] →
     475 ∀fptr_block.
     476 ∀sInv, fInv, kInv.
     477 ∀cl_args_values, cm_args_values.
     478 (* TODO: add invariant All2 value_eq cl_args_values cm_args_values *)
     479 ∀cm_stack.
     480 clight_cminor_rel cl_ge cm_ge INV
     481  (ClCallstate (Vptr (mk_pointer fptr_block zero_offset))
     482   cl_fundef cl_args_values
     483   (Kcall (None (block×offset×type)) cl_f (cl_env ???? frame_data) cl_k)
     484   (cl_m ???? frame_data))
     485  (CmCallstate (Vptr (mk_pointer fptr_block zero_offset)) cm_fundef
     486   cm_args_values (cm_m ???? frame_data)
     487   (Scall (None (ident×typ)) cm_f (stackptr ???? frame_data) (cm_env ???? frame_data) sInv fInv cm_k kInv cm_stack)).
     488
     489definition clight_normal : Clight_state → bool ≝
     490λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
     491
     492definition cminor_normal : Cminor_state → bool ≝
     493λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
     494
     495definition cl_pre : preclassified_system ≝
     496  mk_preclassified_system
     497    clight_fullexec
     498    (λg. Clight_labelled)
     499    (λg. Clight_classify)
     500    (λf,g,s,H. 0). (* XXX TODO *)
     501
     502definition cm_pre : preclassified_system ≝
     503  mk_preclassified_system
     504    Cminor_fullexec
     505    (λg. Cminor_labelled)
     506    (λg. Cminor_classify)
     507    (λf,g,s,H. 0).   (* XXX TODO *)
     508
     509(* Auxilliary lemmas. *)
    393510
    394511lemma invert_assert :
     
    411528qed.
    412529
    413 
    414 (* axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop. *)
     530lemma jmeq_absorb : ∀A:Type[0]. ∀a,b: A. ∀P:Prop. (a = b → P) → a ≃ b → P.
     531#A #a #b #P #H #Heq lapply (jmeq_to_eq ??? Heq) #Heq' @H @Heq' qed.
     532
     533(* wrap up some trivial bit of reasoning to alleviate strange destruct behaviour *)
     534lemma pair_eq_split :
     535  ∀A,B:Type[0]. ∀a1,a2:A. ∀b1,b2:B.
     536  〈a1,b1〉 = 〈a2, b2〉 →
     537  a1 = a2 ∧ b1 = b2.
     538#A #B #a1 #a2 #b1 #b2 #Heq destruct (Heq) @conj try @refl
     539qed.
     540
     541lemma ok_eq_ok_destruct :
     542  ∀A:Type[0]. ∀a,b:A. OK ? a = OK ? b → a = b.
     543#H1 #H2 #H3 #H4 destruct @refl qed.
     544
     545lemma sigma_eq_destruct  : ∀A:Type[0]. ∀a,b:A. ∀P: A → Prop. ∀Ha: P a. ∀Hb: P b.  «a, Ha» = «b,Hb» → a = b ∧ Ha ≃ Hb.
     546#A #a #b #P #Ha #Hb #Heq destruct (Heq)
     547@conj try %
     548qed.
     549
     550(* inverting find_funct and find_funct_ptr *)
     551lemma find_funct_inversion :
     552  ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀res: F.
     553      find_funct F ge v = Some ? res →
     554      (∃ptr. v = Vptr ptr ∧
     555            (poff ptr) = zero_offset ∧
     556            block_region (pblock ptr) = Code ∧
     557            (∃p. block_id (pblock ptr) = neg p ∧
     558                 lookup_opt … p (functions … ge) = Some ? res)).
     559#F #ge #v #res
     560cases v
     561[ | #sz #i | | #ptr ]
     562whd in ⊢ ((??%?) → ?);
     563#Heq destruct (Heq)
     564%{ptr} @conj try @conj try @conj try @refl
     565lapply Heq -Heq
     566@(eq_offset_elim … (poff ptr) zero_offset) //
     567normalize nodelta
     568[ 1,3,5: #_ #Habsurd destruct (Habsurd) ]
     569#Heq destruct (Heq)
     570whd in ⊢ ((??%?) → ?);
     571cases ptr #blo #off cases (block_region blo) normalize nodelta
     572[ 1,3: #Habsurd destruct (Habsurd) ]
     573[ // ]
     574cases (block_id blo) normalize nodelta
     575[ #Habsurd destruct (Habsurd) | #p #Habsurd destruct (Habsurd) ]
     576#p #Hlookup %{p} @conj try @refl assumption
     577qed.
     578
     579(* We should be able to prove that ty = ty' with some more hypotheses, if needed. *)
     580lemma translate_dest_id_inversion :
     581  ∀var_types, e, var_id, ty,H.
     582   translate_dest var_types e = return IdDest var_types var_id ty H →
     583   e = Expr (Evar var_id) (typeof e).
     584@cthulhu
     585(*   
     586#vars #e #var_id #ty #H
     587cases e #ed #ty'
     588cases ed
     589[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
     590| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
     591whd in ⊢ ((??%%) → ?);
     592#Heq
     593[ 1,4,5,6,7,8,9,10,11,13: destruct (Heq)
     594| 3,12: cases (bind_inversion ????? Heq) * #H1 #H2 #H3 cases H3
     595        #_ whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
     596lapply Heq -Heq
     597change with (bind2_eq ????? ) in ⊢ ((??%?) → ?); #Heq
     598cases (bind2_eq_inversion ?????? Heq)
     599#alloctype
     600(* * #alloctype *) * #typ' *
     601cases alloctype
     602[ #r | #n | ] normalize nodelta #Hlookup'
     603[ 1,2: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
     604whd in ⊢ ((??%%) → ?); #Heq' destruct (Heq')
     605@refl*)
     606qed.
     607
     608
     609(* Note: duplicate in switchRemoval.ma *)
     610lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed.
     611
     612lemma breakup_dependent_match_on_pairs :
     613 ∀A,B,C: Type[0].
     614 ∀term: A × B.
     615 ∀F: ∀x,y. 〈x, y〉 = term → C.
     616 ∀z:C.
     617 match term
     618 return λx.x = term → ? with
     619 [ mk_Prod x y ⇒ λEq. F x y Eq ] (refl ? term) = z →
     620 ∃xa,xb,H. term = 〈xa, xb〉 ∧
     621           F xa xb H = z.
     622#A #B #C * #xa #xb #F #z normalize nodelta #H %{xa} %{xb} %{(refl ??)} @conj try @conj
     623// qed.
     624
     625
     626lemma translate_expr_sigma_welltyped : ∀vars, cl_expr, cm_expr.
     627  translate_expr_sigma vars cl_expr = OK ? cm_expr →
     628  dpi1 ?? (pi1 ?? cm_expr) = typ_of_type (typeof cl_expr).
     629#vars #cl_expr * * #typ #cm_expr normalize nodelta #Hexpr_vars
     630whd in ⊢ ((??%?) → ?); #H
     631cases (bind_inversion ????? H) -H * #cm_expr' #Hexpr_vars' *
     632#Htranslate_expr
     633whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @refl
     634qed.
     635
     636lemma translate_exprlist_sigma_welltyped :
     637  ∀vars, cl_exprs, cm_exprs.
     638  mmap_sigma ??? (translate_expr_sigma vars) cl_exprs = OK ? cm_exprs →
     639  All2 ?? (λcl, cm. dpi1 ?? cm = typ_of_type (typeof cl)) cl_exprs (pi1 ?? cm_exprs).
     640#vars #cl_exprs
     641elim cl_exprs
     642[ * #cm_exprs #Hall whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) @I
     643| #hd #tl #Hind * #cm_exprs #Hall #H
     644  cases (bind_inversion ????? H) -H
     645  * * #cm_typ #cm_expr normalize nodelta
     646  #Hexpr_vars_cm * #Htranslate_hd
     647  lapply (translate_expr_sigma_welltyped … Htranslate_hd)
     648  #Heq_cm_typ #H
     649  cases (bind_inversion ????? H) -H
     650  #cm_tail lapply (Hind cm_tail) cases cm_tail
     651  #cm_tail_expr #Hall_tail -Hind #Hind * #Heq_cm_tail normalize nodelta
     652   whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj
     653   [ @Heq_cm_typ
     654   | @Hind assumption ]
     655] qed.
     656
     657lemma translate_dest_MemDest_simulation :
     658  ∀f.
     659  ∀cl_ge : genv_t clight_fundef.
     660  ∀cm_ge : genv_t (fundef internal_function).
     661  ∀INV   : clight_cminor_inv cl_ge cm_ge.
     662  ∀frame_data : clight_cminor_data f cl_ge cm_ge INV.
     663  ∀cl_expr. ∀cm_expr.
     664  ∀cl_block, cl_offset, trace.
     665  ∀Hyp_present.
     666     translate_dest (alloc_type … frame_data) cl_expr = OK ? (MemDest ? cm_expr) →
     667     exec_lvalue cl_ge (cl_env … frame_data) (cl_m … frame_data) cl_expr = OK ? 〈〈cl_block, cl_offset〉, trace〉 →
     668     ∃cm_val. eval_expr cm_ge ASTptr cm_expr (cm_env … frame_data) Hyp_present (stackptr … frame_data) (cm_m … frame_data) = OK ? 〈trace, cm_val〉 ∧
     669              value_eq (Em … frame_data) (Vptr (mk_pointer cl_block cl_offset)) cm_val.     
     670#f #cl_ge #cm_ge #INV #frame_data #cl_expr * #cm_expr #Hexpr_vars #cl_block #cl_offset #trace #Hyp_present
     671whd in match (translate_dest ??); cases cl_expr #cl_desc #cl_typ normalize nodelta
     672cases cl_desc normalize nodelta
     673[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
     674| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
     675#Htranslate
     676[ 2:
     677| *: cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr' #Hexpr_vars' *
     678     #Htranslate_addr
     679     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) #Hexec_lvalue
     680     cases (eval_expr_sim cl_ge cm_ge INV ? frame_data) #_ #Hsim
     681     @(Hsim ??? Hexpr_vars … Htranslate_addr ??? ? Hexec_lvalue) ]
     682cases (bind2_eq_inversion ?????? Htranslate) -Htranslate *
     683[ #r | #n | ]
     684* #cl_type * #Heq_lookup normalize nodelta
     685whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     686whd in ⊢ ((??%?) → ?);
     687@(match lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id
     688  return λx. (lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id = x) → ?
     689  with
     690  [ None ⇒ ?
     691  | Some loc ⇒ ?
     692  ] (refl ? (lookup SymbolTag block (cl_env f cl_ge cm_ge INV frame_data) id ))) normalize nodelta
     693#Hlookup_eq
     694[ 2,4: #Heq destruct (Heq) whd in match (eval_expr ???????);
     695  [ 2: %{(Vptr (mk_pointer (stackptr f cl_ge cm_ge INV frame_data)
     696               (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 n))))}
     697       @conj try @refl
     698       lapply (matching … frame_data id) 
     699       >Hlookup_eq normalize nodelta
     700       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
     701       #Hembed %4 whd in ⊢ (??%?); >Hembed @refl
     702  | 1: whd in match (eval_constant ????);
     703       lapply (matching … frame_data id)
     704       >Hlookup_eq normalize nodelta 
     705       >(opt_to_res_inversion ???? Heq_lookup) normalize nodelta
     706       @False_ind
     707  ]
     708| 1,3: #Hfind_symbol
     709  cases (bind_inversion ????? Hfind_symbol) -Hfind_symbol #block *
     710  whd in ⊢ ((??%%) → ?); #Hfind_symbol
     711  lapply (opt_to_res_inversion ???? Hfind_symbol) #Hfind_symbol_eq
     712  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     713  whd in match (eval_expr ???????);
     714  whd in match (eval_constant ????);
     715  lapply (matching … frame_data id)
     716  [ >Hlookup_eq normalize nodelta >Hfind_symbol_eq normalize nodelta
     717    #Hembed
     718    <(eq_sym … INV id) >Hfind_symbol_eq normalize nodelta
     719     %{(Vptr
     720         (mk_pointer cl_block
     721          (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
     722     @conj try @refl
     723     %4 whd in ⊢ (??%?); >Hembed try @refl
     724  | (* A stack variable is not in the local environment but in the global one. *)
     725    (* we have a contradiction somewhere in the context *)
     726    (* TODO *)
     727    @cthulhu
     728  ]
     729] qed.
     730 
     731(* lift simulation result to eval_exprlist *)
     732lemma eval_exprlist_simulation :
     733  ∀f.
     734  ∀cl_ge : genv_t clight_fundef.
     735  ∀cm_ge : genv_t (fundef internal_function).
     736  ∀INV   : clight_cminor_inv cl_ge cm_ge.
     737  ∀frame_data : clight_cminor_data f cl_ge cm_ge INV.
     738  ∀cl_exprs,cm_exprs.
     739  ∀cl_results,trace.
     740  exec_exprlist cl_ge (cl_env … frame_data) (cl_m … frame_data) cl_exprs = OK ? 〈cl_results, trace〉 →
     741  mmap_sigma ??? (translate_expr_sigma (alloc_type … frame_data)) cl_exprs = OK ? cm_exprs →
     742  ∀H:All ? (λx:𝚺t:typ.expr t.
     743             match x with
     744             [ mk_DPair ty e ⇒
     745                    (expr_vars ty e
     746                     (λid:ident.λty:typ.present SymbolTag val (cm_env … frame_data) id)) ]) cm_exprs.
     747  ∃cm_results.
     748  trace_map_inv … (λe. match e return λe.
     749                         match e with
     750                         [ mk_DPair _ _ ⇒ ? ] → ?
     751                       with
     752                       [ mk_DPair ty e ⇒ λp. eval_expr cm_ge ? e (cm_env … frame_data) p (stackptr … frame_data) (cm_m … frame_data) ]) cm_exprs H = OK ? 〈trace, cm_results〉 ∧
     753  All2 ?? (λcl_val, cm_val. value_eq (Em … frame_data) cl_val cm_val) cl_results cm_results.
     754#f #cl_ge #cm_ge #INV #frame_data #cl_exprs
     755elim cl_exprs
     756[ #cm_exprs #cl_results #trace
     757  whd in ⊢ ((??%?) → ?);
     758  #Heq destruct (Heq)
     759  whd in ⊢ ((??%?) → ?);
     760  #Heq destruct (Heq) #H %{[]}
     761  @conj try @refl try @I
     762| #cl_hd #cl_tl #Hind #cm_exprs #cl_results #trace
     763  #Heq cases (bind_inversion ????? Heq) -Heq
     764  * #hd_val #hd_trace * #Hexec_expr_cl
     765  #Heq cases (bind_inversion ????? Heq) -Heq 
     766  * #cl_tl_vals #cl_tl_trace * #Hexec_expr_tl
     767  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     768  #Htranslate
     769  lapply (translate_exprlist_sigma_welltyped … Htranslate)
     770  #Htype_eq_all #Hall
     771  cases (bind_inversion ????? Htranslate) -Htranslate
     772  * * #cmtype #cmexpr normalize nodelta
     773  #Hexpr_vars_local_cm * #Htranslate_expr_sigma #Htranslate
     774  cases (bind_inversion ????? Htranslate) -Htranslate
     775  * #cm_tail #Hexpr_vars_local_cm_tail * #Htranslate_tail
     776  normalize nodelta
     777  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     778  cases Htype_eq_all -Htype_eq_all #Hcm_type_eq #Htype_eq_all
     779  lapply (Hind cm_tail cl_tl_vals cl_tl_trace Hexec_expr_tl)
     780  [ assumption ] -Hind #Hind
     781  lapply (Hind Htranslate_tail (proj2 ?? Hall)) -Hind
     782  * #cm_results_tl * #Hcm_exec_tl #Hvalues_eq_tl
     783  cases (eval_expr_sim cl_ge cm_ge INV ? frame_data) #Hsim #_
     784  cases (bind_inversion ????? Htranslate_expr_sigma)
     785  * #cmexpr' #Hexpr_vars_local_cm' * #Htranslate
     786  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     787  lapply (Hsim cl_hd cmexpr ??????) -Hsim try assumption
     788  [ @(proj1 ?? Hall) ]
     789  * #cm_val_hd * #Heval_expr_cm #Hvalue_eq     
     790  %{(cm_val_hd :: cm_results_tl)} @conj
     791  [ 2: @conj try assumption
     792  | 1: whd in ⊢ (??%?); normalize nodelta >Heval_expr_cm
     793       normalize nodelta >Hcm_exec_tl @refl
     794  ]
     795] qed. 
    415796
    416797(* Conjectured simulation results
     
    428809 *)
    429810
    430 definition clight_normal : Clight_state → bool ≝
    431 λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
    432 
    433 definition cminor_normal : Cminor_state → bool ≝
    434 λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
    435 
    436 
    437811lemma clight_cminor_normal :
    438   ∀INV:clight_cminor_inv.
    439   ∀s1,s1',s2,tr.
    440   clight_cminor_rel INV s1 s1' →
    441   clight_normal s1 = true →
    442   ¬ Clight_labelled s1 →
    443   ∃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〉) →
    444   ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
    445     tr = tr' ∧
    446     clight_cminor_rel INV s2 s2'
    447   ).
    448 #INV #s1 #s1' #s2 #tr #Hstate_rel #Hclight_normal #Hnot_labeleld
     812    ∀g1,g2.
     813    ∀INV:clight_cminor_inv g1 g2.
     814    ∀s1,s1'.
     815    clight_cminor_rel g1 g2 INV s1 s1' →
     816    clight_normal s1 →
     817    ¬ pcs_labelled cl_pre g1 s1 →
     818    ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr,s2〉 →   
     819    ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'.
     820      tr = tr' ∧
     821      clight_cminor_rel g1 g2 INV s2 s2' ∧
     822      (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1))
     823    ).
     824#g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_normal #Hnot_labeleld
    449825inversion Hstate_rel
    450 #INV' #cl_s
     826#cl_ge #cm_ge #INV' #cl_s
    451827(* case analysis on Clight statement *)
    452828cases cl_s
     
    454830| 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
    455831| 14: #lab | 15: #cost #body ]
     832[ 3: (* Call *)
     833     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
     834     (* introduce everything *)
     835     #fInv #sInv #kInv
     836     #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function
     837     #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls
     838     #flag * * * * #Hstmt_inv #Hlabels_translated #Htmps_preserved
     839     #Hreturn_ok #Hlabel_wf
     840     (* generalize away ugly proof *)
     841     generalize in ⊢ (∀_:(???(??(????%))).?); #Hugly
     842     #Htranslate
     843     @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     844     destruct (HA HB)
     845     @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     846     destruct (HC HD HE) #_
     847     (* back to unfolding Clight execution *)
     848     cases (bind_inversion ????? Htranslate) -Htranslate *
     849     #ef #Hexpr_vars_ef * #Htranslate_ef normalize nodelta #Htranslate
     850     cases (bind_inversion ????? Htranslate) -Htranslate *
     851     #ef' #Hexpr_vars_local_ef' * #Htyp_should_eq_ef
     852     cases (typ_should_eq_inversion (typ_of_type (typeof func)) ASTptr … Htyp_should_eq_ef)
     853     -Htyp_should_eq_ef #Htyp_equality_ef
     854     #Heq_ef_ef' #Htranslate
     855     cases (bind_inversion ????? Htranslate) -Htranslate *
     856     #args #Hall_variables_from_args_local *
     857     whd in ⊢ ((???%) → ?); #Hargs_spec
     858     cases retv normalize nodelta
     859     [ 2: (* return something *)
     860       #lhs #Hdest
     861       cases (bind_inversion ????? Hdest) -Hdest #dest *
     862       inversion dest normalize nodelta
     863       [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest       
     864         #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     865         (* make explicit the nature of lhs, allowing to prove that no trace is emitted *)
     866         lapply (translate_dest_id_inversion  … Htranslate_dest) #Hlhs_eq
     867       | * #cm_expr #Hexpr_vars_cm #Hdest #Htranslate_dest #Hgensym
     868         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
     869         * #ret_var * #new_gensym * #Heq_alloc_tmp * #Halloc_tmp #Hgensym
     870         lapply (breakup_dependent_match_on_pairs ?????? Hgensym) -Hgensym
     871         * #tmp_var * #new_gensym' * #Heq_alloc_tmp' * #Halloc_tmp'         
     872         generalize in ⊢ ((??(?? (????%) )?) → ?); #Hstmt_inv_after_gensym
     873         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     874       ]
     875     | 1: (* return void *)
     876          generalize in ⊢ ((??(??(????%))?) → ?); #Hugly2
     877          whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ]
     878     #s2 #tr #Htranslate
     879     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
     880     #func_ptr_val #func_trace * #Hexec_func_ptr normalize nodelta
     881     whd in ⊢ ((???%) → ?); #Htranslate
     882     cases (bindIO_inversion ??????? Htranslate) -Htranslate *
     883     #args_values #args_trace * #Hexec_arglist #Htranslate
     884     cases (bindIO_inversion ??????? Htranslate) -Htranslate
     885     #cl_fundef * #Hfind_funct
     886     lapply (opt_to_io_Value ?????? Hfind_funct) -Hfind_funct #Hfind_funct
     887     cases (find_funct_inversion ???? Hfind_funct)
     888     #func_ptr * * * #Hfunc_ptr_eq destruct (Hfunc_ptr_eq)
     889     #Hpoff_eq_zero #Hregion_is_code
     890     * #block_id * #Hblock_id_neg #Hlookup
     891     #Htranslate
     892     cases (bindIO_inversion ??????? Htranslate) -Htranslate #Htype_of_fundef *
     893     #Hassert_type_eq
     894     [ 1,2: #Htranslate
     895            cases (bindIO_inversion ??????? Htranslate) -Htranslate * *
     896            #lblock #loffset #ltrace *
     897            #Hexec_lvalue
     898            [ 1: (* empty trace *) @cthulhu (* TODO wip *)
     899            | 2: @cthulhu (* TODO wip *)
     900            ]
     901     | 3: @cthulhu ]
     902     (* TODO wip  *)
     903 (*     
     904     whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
     905       [ 1: >Hlhs_eq in Hexec_lvalue; #Hexec_lvalue %{1}
     906       | 2: (* Execute Cminor part: evaluate lhs, evaluate assign *)
     907            %{2} whd whd in ⊢ (??%?); normalize nodelta
     908            whd in match (eval_expr ???????);
     909            whd in match (m_bind ?????);
     910            lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr)
     911            -Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func
     912           
     913       | 3:
     914       ]
     915       (* execute Cminor part *)
     916       [ %{1} | %{2} | %{1} ]
     917       whd whd in ⊢ (??%?); normalize nodelta
     918       [ 1: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
     919       | 2: generalize in match (proj2 (present ????) (expr_vars ???) (proj1 ???));
     920       | 3: generalize in match (proj2 True ??); ]
     921       #Hexpr_vars_present_ef'
     922       cases (eval_expr_sim … frame_data) #Hsim_expr #_
     923       cut (expr_vars (typ_of_type (typeof func)) ef
     924             (λid:ident.λty:typ.present SymbolTag val (cm_env cl_f cl_ge cm_ge INV' frame_data) id))
     925       [ 1,3,5: lapply Heq_ef_ef' lapply Hexpr_vars_ef lapply ef >Htyp_equality_ef
     926                #ef #Hexpr_vars_ef @(jmeq_absorb ?????) #Heq destruct (Heq)
     927                @Hexpr_vars_present_ef' ]
     928       #Hexpr_vars_present_ef           
     929       (* use simulation lemma on expressions for function *)
     930       lapply (Hsim_expr … Htranslate_ef … Hexpr_vars_present_ef … Hexec_func_ptr)
     931       -Hsim_expr * #cm_func_ptr_val * #Heval_func #Hvalue_eq_func
     932       cut (eval_expr cm_ge ASTptr ef'
     933             (cm_env cl_f cl_ge cm_ge INV' frame_data) Hexpr_vars_present_ef'
     934             (stackptr cl_f cl_ge cm_ge INV' frame_data)
     935             (cm_m cl_f cl_ge cm_ge INV' frame_data)
     936               =OK (trace×val) 〈func_trace,cm_func_ptr_val〉)
     937       [ 1,3,5:
     938         lapply Heq_ef_ef' lapply Heval_func lapply Hexpr_vars_ef lapply Hexpr_vars_local_ef'
     939         lapply Hexpr_vars_present_ef lapply ef lapply Hexpr_vars_present_ef' lapply ef'
     940         <Htyp_equality_ef #ef' #HA #ef #HB #HC #HD #HE
     941         @(jmeq_absorb ?????) #Heq destruct (Heq) @HE ]
     942       -Heval_func #Heval_func >Heval_func
     943       whd in match (m_bind ?????);
     944       lapply (trans_fn … INV' … Hfind_funct)
     945       * #tmp_u * #cminor_fundef * #Hglobals_fresh_for_tmp_u * #Hfundef_fresh_for_tmp_u *
     946       #Htranslate_fundef #Hfind_funct_cm
     947       lapply (value_eq_ptr_inversion … Hvalue_eq_func) * #cm_func_ptr * #Hcm_func_ptr
     948       whd in ⊢ ((??%?) → ?); cases func_ptr in Hfind_funct Hfind_funct_cm Hregion_is_code Hpoff_eq_zero;
     949       #cm_block #cm_off #Hfind_funct #Hfind_funct_cm #Hregion_is_code #Hpoff_eq_zero destruct (Hpoff_eq_zero)
     950       whd in ⊢ ((??%?) → ?); >(Em_fn_id … frame_data … cm_block Hregion_is_code)
     951       normalize nodelta cases cm_func_ptr in Hcm_func_ptr; #cm_block' #cm_off'
     952       #Hcm_func_ptr #Heq destruct (Hcm_func_ptr Heq) >addition_n_0
     953       >Hfind_funct_cm
     954       whd in match (opt_to_res ???); normalize nodelta
     955       cut (All (𝚺t:typ.CMexpr t)
     956              (λx:𝚺t:typ.expr t.(
     957                match x with
     958                [ mk_DPair ty e ⇒
     959                 expr_vars ty e
     960                   (λid:ident
     961                    .λty0:typ.present SymbolTag val (cm_env cl_f cl_ge cm_ge INV' frame_data) id)])) args)
     962       [ 1: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall
     963       | 3: cases sInv * * * * * * * normalize nodelta * #_ #_ #Hall #_ #_ #_ @Hall
     964       | 5: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
     965       #Hall
     966       cases (eval_exprlist_simulation … frame_data ???? Hexec_arglist Hargs_spec Hall)
     967       #cm_values * #Hcm_exec_list #Hcl_cm_values_eq >Hcm_exec_list
     968       whd in match (m_bind ?????); normalize nodelta whd  (* TODO here bug in toCminor to be fixed before going on *) @conj
     969       [ 2,4,6: #Habsurd destruct (Habsurd) ]
     970       @conj try @refl
     971       generalize in match (proj1 True (expr_vars ???) (proj1 ???));
     972       * @(CMR_call … tmp_u) try assumption normalize nodelta
     973       (* a dependency somewhere prevents case analysis *)
     974       lapply Hfind_funct lapply Hfind_funct_cm lapply Htranslate_fundef lapply Hfundef_fresh_for_tmp_u
     975       cases cl_fundef
     976       [ 2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 @I
     977       | 1: #H9 #H10 #H11 #H12 #H13 @conj try @conj try // ]
     978     | (* return something *)
     979       #lhs #Hdest
     980       cases (bind_inversion ????? Hdest) -Hdest #dest *
     981       inversion dest normalize nodelta
     982       [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest
     983         #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     984          generalize in match (conj ???);
     985     ]
     986   
     987         
     988         whd in match (proj1 ???); whd in match (proj2 ???);
     989         
     990         
     991         [ 2: cases sInv * * normalize nodelta * #_ #_ #Hall #_ #_ @Hall ]
     992         
     993         >Hfind_funct_cm
     994         (* case split away the invariants *)
     995         cases sInv * * normalize nodelta * * #Hexpr_vars_ef' #Hall_args_present
     996         whd in ⊢ (% → ?); * * normalize nodelta * #Heval_expr #Hvalue_eq
     997         >Heval_expr
     998         *
     999   
    4561000[ 1: (* Skip *)
    4571001     #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #frame_data #rettyp #Hcont_rel
     
    4601004     [ (* Kstop continuation *)
    4611005       (* 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)
     1006       #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #kframe_data #ktarget_type
     1007       @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1008       destruct (HA HB)
     1009       @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     1010       destruct (HC HD HE)
     1011       @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI
     1012       destruct (HF HG HH HI) #_
    4741013       (* introduce everything *)
    4751014       #fInv #sInv #kInv
     
    4831022       (* In this simple case, trivial translation *)
    4841023       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') #_
     1024       @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1025       destruct (HA HB)
     1026       @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     1027       destruct (HC HD HE) #_
    4901028       (* unfold the clight execution *)
    491        %{0}
    492        whd in ⊢ (% → ?); whd in match (step io_out io_in clight_exec ??);
     1029       #s2 #tr whd in ⊢ ((??%?) → ?);
    4931030       inversion (fn_return kcl_f) normalize nodelta
     1031       normalize nodelta
    4941032       [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
    4951033       | #structname #fieldspec | #unionname #fieldspec | #id ]
    496        #Hfn_return
    497        whd in ⊢ (% → ?);
    498        @False_ind
     1034       #Hfn_return whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     1035       %{1} whd @conj try @conj try @refl
     1036       [ 2: #Habsurd destruct (Habsurd) ]
     1037       %2{kcl_f}
     1038       [ %{ (alloc_type … kframe_data)
     1039            (stacksize … kframe_data)
     1040            (alloc_hyp … kframe_data)
     1041            (cl_env … kframe_data)
     1042            (cm_env … kframe_data)
     1043            (cl_env_hyp … kframe_data)
     1044            (free_list (cl_m … kframe_data) (blocks_of_env (cl_env … kframe_data)))
     1045            (free (cm_m … kframe_data) (stackptr … kframe_data))
     1046            (Em … kframe_data)
     1047            ? (* injection *)
     1048            (stackptr … kframe_data)
     1049            ? (* matching *)}
     1050         [ @(freelist_memory_inj_m1_m2 … (injection … kframe_data) (blocks_of_env (cl_env … kframe_data)) (stackptr … kframe_data))
     1051           [ 2,3: @refl
     1052           |
     1053 
     1054     @cthulhu
    4991055    | (* KSeq continuation *)
    500       #kINV #kcl_f #kcm_f #kframe_data #ktarget_type #kcl_s #kcm_s #kcl_k' #kcm_k'
     1056      #gcl_ge #kcm_ge #kINV #kcl_f #kcm_f #kframe_data #ktarget_type #kcl_s #kcm_s #kcl_k' #kcm_k'
    5011057      #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag
    5021058      * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved
    5031059      #kHreturn_ok #kHlabel_wf #kHeq_translate #kHcont_rel #_
     1060      @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB
     1061      destruct (HA HB)
     1062      @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE
     1063      destruct (HC HD HE)
     1064      @(jmeq_absorb ?????) #HF
     1065     
    5041066      #Heq_INV #Heq_cl_f #Heq_cm_f #Heq_frame #Heq_rettyp #Heq_cl_k #Heq_cm_k  #_
    5051067      (* get rid of jmeqs and destruct *)
     
    6871249          | 3: (* Local *) @cthulhu
    6881250          ]
    689      | *: (* memdest *) @cthulhu ]    
     1251     | *: (* memdest *) @cthulhu ]   *) 
    6901252| *: @cthulhu
    6911253] qed.
    6921254
     1255(* TODO: adapt the following to the new goal shape. *)
    6931256axiom clight_cminor_call_return :
    6941257  ∀INV:clight_cminor_inv.
  • src/Cminor/Cminor_abstract.ma

    r2677 r2737  
    3838definition CmState ≝ State.
    3939
     40definition CmReturnstate ≝ Returnstate.
     41
     42definition CmCallstate ≝ Callstate.
     43
Note: See TracChangeset for help on using the changeset viewer.