Changeset 2692


Ignore:
Timestamp:
Feb 22, 2013, 11:27:15 AM (6 years ago)
Author:
garnier
Message:

Add some more constraints in clight_cminor_data.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectnessExpr.ma

    r2667 r2692  
    77include "Cminor/Cminor_abstract.ma".
    88
    9 record clight_cminor_inv : Type[0] ≝ {
     9record clight_cminor_inv (ge_cl : genv_t clight_fundef) (ge_cm : genv_t (fundef internal_function)) : Type[0] ≝
     10{
    1011  globals : list (ident × region × type);
    11   ge_cl : genv_t clight_fundef;
    12   ge_cm : genv_t (fundef internal_function);
    1312  eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s;
    1413  trans_fn : ∀v,f. find_funct … ge_cl v = Some ? f →
     
    2322definition memory_matching ≝
    2423  λE:embedding.
     24  λge_cl, ge_cm.
    2525  λm,m':mem.
    2626  λen:cl_env.
    2727  λvenv:cm_env.
    28   λcminv:clight_cminor_inv.
     28  λcminv:clight_cminor_inv ge_cl ge_cm.
    2929  λsp:block.
    3030  λvars:var_types.
     
    3232    match lookup SymbolTag ? en id with
    3333    [ None ⇒
    34       match find_symbol ? (ge_cl cminv) id with
     34      match find_symbol ? ge_cl id with
    3535      [ None ⇒ True
    3636      | Some cl_blo ⇒
     
    389389qed.
    390390
    391 record clight_cminor_data (f : function) (INV : clight_cminor_inv) : Type[0] ≝
     391record clight_cminor_data
     392  (f : function)
     393  (ge_cl : genv_t clight_fundef)
     394  (ge_cm : genv_t (fundef internal_function))
     395  (INV : clight_cminor_inv ge_cl ge_cm) : Type[0] ≝
    392396{ alloc_type  : var_types;
    393397  stacksize   : ℕ;
    394   alloc_hyp   : characterise_vars (globals INV) f = 〈alloc_type, stacksize〉;
     398  alloc_hyp   : characterise_vars (globals ?? INV) f = 〈alloc_type, stacksize〉;
    395399  (* environments *)
    396400  cl_env      : cl_env;
     
    401405  cl_m        : mem;
    402406  cm_m        : mem;
    403   (* memory injection and matching *)
    404   E           : embedding;
    405   injection   : memory_inj E cl_m cm_m;
     407  (* Memory injection and matching *)
     408  Em          : embedding; (* using "E" clashes with something in jmeq *)
     409  injection   : memory_inj Em cl_m cm_m;
    406410  stackptr    : block;
    407   matching    : memory_matching E cl_m cm_m cl_env cm_env INV stackptr alloc_type
     411  matching    : memory_matching Em ge_cl ge_cm cl_m cm_m cl_env cm_env INV stackptr alloc_type;
     412  (* Force embedding to compute identity on functions *)
     413  Em_fn_id    : ∀b. block_region b = Code → Em b = Some ? 〈b, zero_offset〉
    408414}.
    409415
     
    413419lemma eval_expr_sim :
    414420  (* [cl_cm_inv] maps CL globals to CM globals, including functions *)
    415   ∀cl_cm_inv  : clight_cminor_inv.
     421  ∀ge_cl : genv_t clight_fundef.
     422  ∀ge_cm : genv_t (fundef internal_function).
     423  ∀cl_cm_inv  : clight_cminor_inv ge_cl ge_cm.
    416424  (* current function (defines local environment) *)
    417425  ∀f          : function.
    418   ∀data       : clight_cminor_data f cl_cm_inv.
     426  ∀data       : clight_cminor_data f ge_cl ge_cm cl_cm_inv.
    419427  (* clight expr to cminor expr *)
    420428  (∀(e:expr).
    421429   ∀(e':CMexpr (typ_of_type (typeof e))).
    422430   ∀Hexpr_vars.
    423    translate_expr (alloc_type ?? data) e = OK ? («e', Hexpr_vars») →
     431   translate_expr (alloc_type data) e = OK ? («e', Hexpr_vars») →
    424432   ∀cl_val,trace,Hyp_present.
    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) ∧
     433   exec_expr ge_cl (cl_env … data) (cl_m … data) e = OK ? 〈cl_val, trace〉 →
     434   ∃cm_val. eval_expr ge_cm (typ_of_type (typeof e)) e' (cm_env … data) Hyp_present (stackptr … data) (cm_m … data) = OK ? 〈trace, cm_val〉 ∧
     435            value_eq (Em … data) cl_val cm_val) ∧
    428436   (* clight /lvalue/ to cminor /expr/ *)
    429437  (∀ed,ty.
    430438   ∀(e':CMexpr ASTptr).
    431439   ∀Hexpr_vars.
    432    translate_addr (alloc_type ?? data) (Expr ed ty) = OK ? («e', Hexpr_vars») →
     440   translate_addr (alloc_type data) (Expr ed ty) = OK ? («e', Hexpr_vars») →
    433441   ∀cl_blo,cl_off,trace,Hyp_present.
    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
     442   exec_lvalue' ge_cl (cl_env … data) (cl_m … data) ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
     443   ∃cm_val. eval_expr ge_cm ASTptr e' (cm_env … data) Hyp_present (stackptr … data) (cm_m … data) = OK ? 〈trace, cm_val〉 ∧
     444            value_eq (Em … data) (Vptr (mk_pointer cl_blo cl_off)) cm_val).
     445#ge_cl #ge_cm #inv #f * #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching #_
    438446@expr_lvalue_ind_combined
    439447[ 7: (* binary ops *)
     
    16391647          whd in match (eval_expr ???????);
    16401648          whd in match (eval_constant ????);
    1641           <(eq_sym inv var) >Hfind_symbol normalize nodelta
     1649          <(eq_sym ?? inv var) >Hfind_symbol normalize nodelta
    16421650          %{(Vptr (mk_pointer cl_blo (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
    16431651          @conj try @refl %4 whd in match (pointer_translation ??);
Note: See TracChangeset for help on using the changeset viewer.