Ignore:
Timestamp:
Jan 31, 2013, 12:56:03 PM (8 years ago)
Author:
garnier
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2597 r2598  
    235235
    236236
    237 (* This is the statement for expression simulation copied fro toCminorCorrectnessExpr.ma,
     237(* This is the statement for expression simulation copied from toCminorCorrectnessExpr.ma,
    238238   for easier reference.
    239239lemma eval_expr_sim :
     
    280280
    281281
    282 
     282(* TODO: relate Clight continuations and Cminor ones. *)
     283(*
     284axiom clight_cminor_cont_rel :
     285  clight_cminor_inv → cl_cont → cm_cont → block → stack → Prop.
     286
     287inductive clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop ≝
     288| CMR_normal :
     289  (* relates globals to globals and functions to functions *)
     290  ∀INV:  clight_cminor_inv.
     291
     292  (* ---- Clight variables ---- *)
     293  ∀cl_f: function.                               (* Clight enclosing function *) 
     294  ∀cl_s: statement.                                       (* Clight statement *) 
     295  ∀cl_k: cl_cont.                                      (* Clight continuation *)
     296  ∀cl_e: cl_env.                                        (* Clight environment *)
     297
     298  (* ---- Cminor variables ---- *) 
     299  ∀cl_m: mem.                                                (* Clight memory *)
     300  ∀cm_f: internal_function.                             (* enclosing function *)
     301  ∀cm_s: stmt.                                            (* Cminor statement *)
     302  ∀cm_k: cm_cont.                                       (* Cminor contiuation *)
     303  ∀cm_sp: block.                                      (* Cminor stack pointer *)
     304  ∀cm_st: stack.                                              (* Cminor stack *)
     305  ∀cm_e: cm_env.                                        (* Cminor environment *)
     306  ∀cm_m: mem.                                                (* Cminor memory *)
     307  ∀fInv: stmt_inv cm_f cm_e (f_body cm_f).               (* Cminor invariants *)
     308  ∀sInv: stmt_inv cm_f cm_e cm_s.
     309  ∀kInv: cont_inv cm_f cm_e cm_k.
     310
     311  (* ---- specify the mapping from variables to their alloc type (global, stack, register) ---- *)
     312  ∀alloctype:  var_types.                       (* map from var to alloc type *) 
     313  ∀stack_cons: ℕ.                              (* stack consumption of [cl_f] *)
     314  characterise_vars (globals INV) cl_f = 〈alloctype, stack_cons〉 →  (* spec of [alloctype] *)
     315
     316  (* ---- linking Clight and Cminor memories ---- *)
     317  ∀E: embedding.
     318  memory_inj E cl_m cm_m →
     319  memory_matching E cl_m cm_m cl_e cm_e INV cm_sp alloctype →
     320
     321  (* ---- specification of the contents of clight environment (needed for expr sim) ---- *)
     322  (* the two memories are those at function entry time. *)
     323  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_e,m'〉) → 
     324 
     325  (* ---- relate Clight and Cminor functions ---- *)
     326  ∀func_univ: universe SymbolTag.
     327  ∀Hfresh_globals: globals_fresh_for_univ ? (globals INV) func_univ.
     328  ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
     329  translate_function func_univ (globals INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
     330
     331  (* ---- relate Clight and Cminor statements ---- *) 
     332  ∀stmt_univ: tmpgen alloctype.
     333  ∀lbl_univ:  labgen.
     334  ∀lbls:      lenv.
     335  ∀flag:      convert_flag.
     336  ∀outcome:   (Σsu:(tmpgen alloctype)×labgen×stmt.trans_inv alloctype lbls cl_s stmt_univ flag (opttyp_of_type (fn_return cl_f)) su).
     337  translate_statement alloctype stmt_univ lbl_univ lbls flag (opttyp_of_type (fn_return cl_f)) cl_s = OK ? outcome →
     338  (* TODO decompose outcome *)
     339
     340  (* ---- relate Clight continuation to Cminor continuation + stack pointer + stack ---- *)
     341  clight_cminor_cont_rel INV cl_k cm_k cm_sp cm_st →
     342   
     343  clight_cminor_rel INV
     344    (ClState cl_f cl_s cl_k cl_e cl_m)
     345    (CmState cm_f cm_s cm_e fInv sInv cm_m cm_sp cm_k kInv cm_st).
     346*)
    283347
    284348axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
Note: See TracChangeset for help on using the changeset viewer.