Ignore:
Timestamp:
Feb 14, 2013, 7:10:23 PM (8 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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.