From a7c6cf8d4d59e29ed73f9eb8bfc015b0384672a1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:33:05 +0000 Subject: Revu la repartition des sources Coq en sous-repertoires git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@73 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgen.v | 433 ++++++++ cfrontend/Cminorgenproof.v | 2595 ++++++++++++++++++++++++++++++++++++++++++++ cfrontend/Csharpminor.v | 563 ++++++++++ 3 files changed, 3591 insertions(+) create mode 100644 cfrontend/Cminorgen.v create mode 100644 cfrontend/Cminorgenproof.v create mode 100644 cfrontend/Csharpminor.v (limited to 'cfrontend') diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v new file mode 100644 index 00000000..4c611b44 --- /dev/null +++ b/cfrontend/Cminorgen.v @@ -0,0 +1,433 @@ +(** Translation from Csharpminor to Cminor. *) + +Require Import Coqlib. +Require Import Maps. +Require Import Sets. +Require Import AST. +Require Import Integers. +Require Mem. +Require Import Csharpminor. +Require Import Op. +Require Import Cminor. +Require Cmconstr. + +(** The main task in translating Csharpminor to Cminor is to explicitly + stack-allocate local variables whose address is taken: these local + variables become sub-blocks of the Cminor stack data block for the + current function. Taking the address of such a variable becomes + a [Oaddrstack] operation with the corresponding offset. Accessing + or assigning such a variable becomes a load or store operation at + that address. Only scalar local variables whose address is never + taken in the Csharpminor code can be mapped to Cminor local + variable, since the latter do not reside in memory. + + Other tasks performed during the translation to Cminor: +- Transformation of Csharpminor's standard set of operators and + trivial addressing modes to Cminor's processor-dependent operators + and addressing modes. This is done using the optimizing Cminor + constructor functions provided in file [Cmconstr], therefore performing + instruction selection on the fly. +- Insertion of truncation, zero- and sign-extension operations when + assigning to a Csharpminor local variable of ``small'' type + (e.g. [Mfloat32] or [Mint8signed]). This is necessary to preserve + the ``normalize at assignment-time'' semantics of Csharpminor. +*) + +(** Translation of operators. *) + +Definition make_op (op: Csharpminor.operation) (el: exprlist): option expr := + match el with + | Enil => + match op with + | Csharpminor.Ointconst n => Some(Eop (Ointconst n) Enil) + | Csharpminor.Ofloatconst n => Some(Eop (Ofloatconst n) Enil) + | _ => None + end + | Econs e1 Enil => + match op with + | Csharpminor.Ocast8unsigned => Some(Cmconstr.cast8unsigned e1) + | Csharpminor.Ocast8signed => Some(Cmconstr.cast8signed e1) + | Csharpminor.Ocast16unsigned => Some(Cmconstr.cast16unsigned e1) + | Csharpminor.Ocast16signed => Some(Cmconstr.cast16signed e1) + | Csharpminor.Onotint => Some(Cmconstr.notint e1) + | Csharpminor.Onegf => Some(Cmconstr.negfloat e1) + | Csharpminor.Oabsf => Some(Cmconstr.absfloat e1) + | Csharpminor.Osingleoffloat => Some(Cmconstr.singleoffloat e1) + | Csharpminor.Ointoffloat => Some(Cmconstr.intoffloat e1) + | Csharpminor.Ofloatofint => Some(Cmconstr.floatofint e1) + | Csharpminor.Ofloatofintu => Some(Cmconstr.floatofintu e1) + | _ => None + end + | Econs e1 (Econs e2 Enil) => + match op with + | Csharpminor.Oadd => Some(Cmconstr.add e1 e2) + | Csharpminor.Osub => Some(Cmconstr.sub e1 e2) + | Csharpminor.Omul => Some(Cmconstr.mul e1 e2) + | Csharpminor.Odiv => Some(Cmconstr.divs e1 e2) + | Csharpminor.Odivu => Some(Cmconstr.divu e1 e2) + | Csharpminor.Omod => Some(Cmconstr.mods e1 e2) + | Csharpminor.Omodu => Some(Cmconstr.modu e1 e2) + | Csharpminor.Oand => Some(Cmconstr.and e1 e2) + | Csharpminor.Oor => Some(Cmconstr.or e1 e2) + | Csharpminor.Oxor => Some(Cmconstr.xor e1 e2) + | Csharpminor.Oshl => Some(Cmconstr.shl e1 e2) + | Csharpminor.Oshr => Some(Cmconstr.shr e1 e2) + | Csharpminor.Oshru => Some(Cmconstr.shru e1 e2) + | Csharpminor.Oaddf => Some(Cmconstr.addf e1 e2) + | Csharpminor.Osubf => Some(Cmconstr.subf e1 e2) + | Csharpminor.Omulf => Some(Cmconstr.mulf e1 e2) + | Csharpminor.Odivf => Some(Cmconstr.divf e1 e2) + | Csharpminor.Ocmp c => Some(Cmconstr.cmp c e1 e2) + | Csharpminor.Ocmpu c => Some(Cmconstr.cmpu c e1 e2) + | Csharpminor.Ocmpf c => Some(Cmconstr.cmpf c e1 e2) + | _ => None + end + | _ => None + end. + +(** [make_cast chunk e] returns a Cminor expression that normalizes + the value of Cminor expression [e] as prescribed by the memory chunk + [chunk]. For instance, 8-bit sign extension is performed if + [chunk] is [Mint8signed]. *) + +Definition make_cast (chunk: memory_chunk) (e: expr): expr := + match chunk with + | Mint8signed => Cmconstr.cast8signed e + | Mint8unsigned => Cmconstr.cast8unsigned e + | Mint16signed => Cmconstr.cast16signed e + | Mint16unsigned => Cmconstr.cast16unsigned e + | Mint32 => e + | Mfloat32 => Cmconstr.singleoffloat e + | Mfloat64 => e + end. + +Definition make_load (chunk: memory_chunk) (e: expr): expr := + Cmconstr.load chunk e. + +Definition store_arg (chunk: memory_chunk) (e: expr) : expr := + match e with + | Eop op (Econs e1 Enil) => + match op with + | Ocast8signed => + match chunk with Mint8signed => e1 | _ => e end + | Ocast8unsigned => + match chunk with Mint8unsigned => e1 | _ => e end + | Ocast16signed => + match chunk with Mint16signed => e1 | _ => e end + | Ocast16unsigned => + match chunk with Mint16unsigned => e1 | _ => e end + | Osingleoffloat => + match chunk with Mfloat32 => e1 | _ => e end + | _ => e + end + | _ => e + end. + +Definition make_store (chunk: memory_chunk) (e1 e2: expr): stmt := + Sexpr(Cmconstr.store chunk e1 (store_arg chunk e2)). + +Definition make_stackaddr (ofs: Z): expr := + Eop (Oaddrstack (Int.repr ofs)) Enil. + +Definition make_globaladdr (id: ident): expr := + Eop (Oaddrsymbol id Int.zero) Enil. + +(** Compile-time information attached to each Csharpminor + variable: global variables, local variables, function parameters. + [Var_local] denotes a scalar local variable whose address is not + taken; it will be translated to a Cminor local variable of the + same name. [Var_stack_scalar] and [Var_stack_array] denote + local variables that are stored as sub-blocks of the Cminor stack + data block. [Var_global_scalar] and [Var_global_array] denote + global variables, stored in the global symbols with the same names. *) + +Inductive var_info: Set := + | Var_local: memory_chunk -> var_info + | Var_stack_scalar: memory_chunk -> Z -> var_info + | Var_stack_array: Z -> var_info + | Var_global_scalar: memory_chunk -> var_info + | Var_global_array: var_info. + +Definition compilenv := PMap.t var_info. + +(** Generation of Cminor code corresponding to accesses to Csharpminor + local variables: reads, assignments, and taking the address of. *) + +Definition var_get (cenv: compilenv) (id: ident): option expr := + match PMap.get id cenv with + | Var_local chunk => + Some(Evar id) + | Var_stack_scalar chunk ofs => + Some(make_load chunk (make_stackaddr ofs)) + | Var_global_scalar chunk => + Some(make_load chunk (make_globaladdr id)) + | _ => + None + end. + +Definition var_set (cenv: compilenv) (id: ident) (rhs: expr): option stmt := + match PMap.get id cenv with + | Var_local chunk => + Some(Sexpr(Eassign id (make_cast chunk rhs))) + | Var_stack_scalar chunk ofs => + Some(make_store chunk (make_stackaddr ofs) rhs) + | Var_global_scalar chunk => + Some(make_store chunk (make_globaladdr id) rhs) + | _ => + None + end. + +Definition var_addr (cenv: compilenv) (id: ident): option expr := + match PMap.get id cenv with + | Var_local chunk => None + | Var_stack_scalar chunk ofs => Some (make_stackaddr ofs) + | Var_stack_array ofs => Some (make_stackaddr ofs) + | _ => Some (make_globaladdr id) + end. + +(** The translation from Csharpminor to Cminor can fail, which we + encode by returning option types ([None] denotes error). + Propagation of errors is done in monadic style, using the following + [bind] monadic composition operator, and a [do] notation inspired + by Haskell's. *) + +Definition bind (A B: Set) (a: option A) (b: A -> option B): option B := + match a with + | None => None + | Some x => b x + end. + +Notation "'do' X <- A ; B" := (bind _ _ A (fun X => B)) + (at level 200, X ident, A at level 100, B at level 200). + +(** Translation of expressions. All the hard work is done by the + [make_*] and [var_*] functions defined above. *) + +Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr) + {struct e}: option expr := + match e with + | Csharpminor.Evar id => var_get cenv id + | Csharpminor.Eaddrof id => var_addr cenv id + | Csharpminor.Eop op el => + do tel <- transl_exprlist cenv el; make_op op tel + | Csharpminor.Eload chunk e => + do te <- transl_expr cenv e; Some (make_load chunk te) + | Csharpminor.Ecall sig e el => + do te <- transl_expr cenv e; + do tel <- transl_exprlist cenv el; + Some (Ecall sig te tel) + | Csharpminor.Econdition e1 e2 e3 => + do te1 <- transl_expr cenv e1; + do te2 <- transl_expr cenv e2; + do te3 <- transl_expr cenv e3; + Some (Cmconstr.conditionalexpr te1 te2 te3) + | Csharpminor.Elet e1 e2 => + do te1 <- transl_expr cenv e1; + do te2 <- transl_expr cenv e2; + Some (Elet te1 te2) + | Csharpminor.Eletvar n => + Some (Eletvar n) + | Csharpminor.Ealloc e => + do te <- transl_expr cenv e; + Some (Ealloc te) + end + +with transl_exprlist (cenv: compilenv) (el: Csharpminor.exprlist) + {struct el}: option exprlist := + match el with + | Csharpminor.Enil => + Some Enil + | Csharpminor.Econs e1 e2 => + do te1 <- transl_expr cenv e1; + do te2 <- transl_exprlist cenv e2; + Some (Econs te1 te2) + end. + +(** Translation of statements. Entirely straightforward. *) + +Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt) + {struct s}: option stmt := + match s with + | Csharpminor.Sskip => + Some Sskip + | Csharpminor.Sexpr e => + do te <- transl_expr cenv e; Some(Sexpr te) + | Csharpminor.Sassign id e => + do te <- transl_expr cenv e; var_set cenv id te + | Csharpminor.Sstore chunk e1 e2 => + do te1 <- transl_expr cenv e1; + do te2 <- transl_expr cenv e2; + Some (make_store chunk te1 te2) + | Csharpminor.Sseq s1 s2 => + do ts1 <- transl_stmt cenv s1; + do ts2 <- transl_stmt cenv s2; + Some (Sseq ts1 ts2) + | Csharpminor.Sifthenelse e s1 s2 => + do te <- transl_expr cenv e; + do ts1 <- transl_stmt cenv s1; + do ts2 <- transl_stmt cenv s2; + Some (Cmconstr.ifthenelse te ts1 ts2) + | Csharpminor.Sloop s => + do ts <- transl_stmt cenv s; + Some (Sloop ts) + | Csharpminor.Sblock s => + do ts <- transl_stmt cenv s; + Some (Sblock ts) + | Csharpminor.Sexit n => + Some (Sexit n) + | Csharpminor.Sswitch e cases default => + do te <- transl_expr cenv e; Some(Sswitch te cases default) + | Csharpminor.Sreturn None => + Some (Sreturn None) + | Csharpminor.Sreturn (Some e) => + do te <- transl_expr cenv e; Some (Sreturn (Some te)) + end. + +(** Computation of the set of variables whose address is taken in + a piece of Csharpminor code. *) + +Module Identset := MakeSet(PTree). + +Fixpoint addr_taken_expr (e: Csharpminor.expr): Identset.t := + match e with + | Csharpminor.Evar id => Identset.empty + | Csharpminor.Eaddrof id => Identset.add id Identset.empty + | Csharpminor.Eop op el => addr_taken_exprlist el + | Csharpminor.Eload chunk e => addr_taken_expr e + | Csharpminor.Ecall sig e el => + Identset.union (addr_taken_expr e) (addr_taken_exprlist el) + | Csharpminor.Econdition e1 e2 e3 => + Identset.union (addr_taken_expr e1) + (Identset.union (addr_taken_expr e2) (addr_taken_expr e3)) + | Csharpminor.Elet e1 e2 => + Identset.union (addr_taken_expr e1) (addr_taken_expr e2) + | Csharpminor.Eletvar n => Identset.empty + | Csharpminor.Ealloc e => addr_taken_expr e + end + +with addr_taken_exprlist (e: Csharpminor.exprlist): Identset.t := + match e with + | Csharpminor.Enil => Identset.empty + | Csharpminor.Econs e1 e2 => + Identset.union (addr_taken_expr e1) (addr_taken_exprlist e2) + end. + +Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t := + match s with + | Csharpminor.Sskip => Identset.empty + | Csharpminor.Sexpr e => addr_taken_expr e + | Csharpminor.Sassign id e => addr_taken_expr e + | Csharpminor.Sstore chunk e1 e2 => + Identset.union (addr_taken_expr e1) (addr_taken_expr e2) + | Csharpminor.Sseq s1 s2 => + Identset.union (addr_taken_stmt s1) (addr_taken_stmt s2) + | Csharpminor.Sifthenelse e s1 s2 => + Identset.union (addr_taken_expr e) + (Identset.union (addr_taken_stmt s1) (addr_taken_stmt s2)) + | Csharpminor.Sloop s => addr_taken_stmt s + | Csharpminor.Sblock s => addr_taken_stmt s + | Csharpminor.Sexit n => Identset.empty + | Csharpminor.Sswitch e cases default => addr_taken_expr e + | Csharpminor.Sreturn None => Identset.empty + | Csharpminor.Sreturn (Some e) => addr_taken_expr e + end. + +(** Layout of the Cminor stack data block and construction of the + compilation environment. Csharpminor local variables that are + arrays or whose address is taken are allocated a slot in the Cminor + stack data. While this is not important for correctness, sufficient + padding is inserted to ensure adequate alignment of addresses. *) + +Definition assign_variable + (atk: Identset.t) + (id_lv: ident * var_kind) + (cenv_stacksize: compilenv * Z) : compilenv * Z := + let (cenv, stacksize) := cenv_stacksize in + match id_lv with + | (id, Varray sz) => + let ofs := align stacksize 8 in + (PMap.set id (Var_stack_array ofs) cenv, ofs + Zmax 0 sz) + | (id, Vscalar chunk) => + if Identset.mem id atk then + let sz := Mem.size_chunk chunk in + let ofs := align stacksize sz in + (PMap.set id (Var_stack_scalar chunk ofs) cenv, ofs + sz) + else + (PMap.set id (Var_local chunk) cenv, stacksize) + end. + +Fixpoint assign_variables + (atk: Identset.t) + (id_lv_list: list (ident * var_kind)) + (cenv_stacksize: compilenv * Z) + {struct id_lv_list}: compilenv * Z := + match id_lv_list with + | nil => cenv_stacksize + | id_lv :: rem => + assign_variables atk rem (assign_variable atk id_lv cenv_stacksize) + end. + +Definition build_compilenv + (globenv: compilenv) (f: Csharpminor.function) : compilenv * Z := + assign_variables + (addr_taken_stmt f.(Csharpminor.fn_body)) + (fn_variables f) + (globenv, 0). + +Definition assign_global_variable + (ce: compilenv) (info: ident * var_kind * list init_data) : compilenv := + match info with + | (id, Vscalar chunk, _) => PMap.set id (Var_global_scalar chunk) ce + | (id, Varray _, _) => PMap.set id Var_global_array ce + end. + +Definition build_global_compilenv (p: Csharpminor.program) : compilenv := + List.fold_left assign_global_variable + p.(prog_vars) (PMap.init Var_global_array). + +(** Function parameters whose address is taken must be stored in their + stack slots at function entry. (Cminor passes these parameters in + local variables.) *) + +Fixpoint store_parameters + (cenv: compilenv) (params: list (ident * memory_chunk)) + {struct params} : stmt := + match params with + | nil => Sskip + | (id, chunk) :: rem => + match PMap.get id cenv with + | Var_local chunk => + Sseq (Sexpr (Eassign id (make_cast chunk (Evar id)))) + (store_parameters cenv rem) + | Var_stack_scalar chunk ofs => + Sseq (make_store chunk (make_stackaddr ofs) (Evar id)) + (store_parameters cenv rem) + | _ => + Sskip (* should never happen *) + end + end. + +(** Translation of a Csharpminor function. We must check that the + required Cminor stack block is no bigger than [Int.max_signed], + otherwise address computations within the stack block could + overflow machine arithmetic and lead to incorrect code. *) + +Definition transl_function + (gce: compilenv) (f: Csharpminor.function): option function := + let (cenv, stacksize) := build_compilenv gce f in + if zle stacksize Int.max_signed then + do tbody <- transl_stmt cenv f.(Csharpminor.fn_body); + Some (mkfunction + (Csharpminor.fn_sig f) + (Csharpminor.fn_params_names f) + (Csharpminor.fn_vars_names f) + stacksize + (Sseq (store_parameters cenv f.(Csharpminor.fn_params)) tbody)) + else None. + +Definition transl_fundef (gce: compilenv) (f: Csharpminor.fundef): option fundef := + transf_partial_fundef (transl_function gce) f. + +Definition transl_program (p: Csharpminor.program) : option program := + let gce := build_global_compilenv p in + transform_partial_program (transl_fundef gce) (program_of_program p). diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v new file mode 100644 index 00000000..7820095a --- /dev/null +++ b/cfrontend/Cminorgenproof.v @@ -0,0 +1,2595 @@ +(** Correctness proof for Cminor generation. *) + +Require Import Coqlib. +Require Import Maps. +Require Import Sets. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Events. +Require Import Globalenvs. +Require Import Csharpminor. +Require Import Op. +Require Import Cminor. +Require Cmconstr. +Require Import Cminorgen. +Require Import Cmconstrproof. + +Section TRANSLATION. + +Variable prog: Csharpminor.program. +Variable tprog: program. +Hypothesis TRANSL: transl_program prog = Some tprog. +Let ge : Csharpminor.genv := Genv.globalenv (program_of_program prog). +Let tge: genv := Genv.globalenv tprog. +Let gce : compilenv := build_global_compilenv prog. + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + intro. unfold ge, tge. + apply Genv.find_symbol_transf_partial with (transl_fundef gce). + exact TRANSL. +Qed. + +Lemma function_ptr_translated: + forall (b: block) (f: Csharpminor.fundef), + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef gce f = Some tf. +Proof. + intros. + generalize + (Genv.find_funct_ptr_transf_partial (transl_fundef gce) TRANSL H). + case (transl_fundef gce f). + intros tf [A B]. exists tf. tauto. + intros [A B]. elim B. reflexivity. +Qed. + +Lemma functions_translated: + forall (v: val) (f: Csharpminor.fundef), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transl_fundef gce f = Some tf. +Proof. + intros. + generalize + (Genv.find_funct_transf_partial (transl_fundef gce) TRANSL H). + case (transl_fundef gce f). + intros tf [A B]. exists tf. tauto. + intros [A B]. elim B. reflexivity. +Qed. + +Lemma sig_preserved: + forall f tf, + transl_fundef gce f = Some tf -> + Cminor.funsig tf = Csharpminor.funsig f. +Proof. + intros until tf; destruct f; simpl. + unfold transl_function. destruct (build_compilenv gce f). + case (zle z Int.max_signed); try congruence. + intro. case (transl_stmt c (Csharpminor.fn_body f)); simpl; try congruence. + intros. inversion H. reflexivity. + intro. inversion H; reflexivity. +Qed. + +Definition global_compilenv_match (ce: compilenv) (gv: gvarenv) : Prop := + forall id, + match ce!!id with + | Var_global_scalar chunk => gv!id = Some (Vscalar chunk) + | Var_global_array => True + | _ => False + end. + +Lemma global_compilenv_charact: + global_compilenv_match gce (global_var_env prog). +Proof. + set (mkgve := fun gv (vars: list (ident * var_kind * list init_data)) => + List.fold_left + (fun gve x => match x with (id, k, init) => PTree.set id k gve end) + vars gv). + assert (forall vars gv ce, + global_compilenv_match ce gv -> + global_compilenv_match (List.fold_left assign_global_variable vars ce) + (mkgve gv vars)). + induction vars; simpl; intros. + auto. + apply IHvars. intro id1. unfold assign_global_variable. + destruct a as [[id2 lv2] init2]. destruct lv2; simpl; rewrite PMap.gsspec; rewrite PTree.gsspec. + case (peq id1 id2); intro. auto. apply H. + case (peq id1 id2); intro. auto. apply H. + + change (global_var_env prog) with (mkgve (PTree.empty var_kind) prog.(Csharpminor.prog_vars)). + unfold gce, build_global_compilenv. apply H. + intro. rewrite PMap.gi. auto. +Qed. + +(** * Correspondence between Csharpminor's and Cminor's environments and memory states *) + +(** In Csharpminor, every variable is stored in a separate memory block. + In the corresponding Cminor code, some of these variables reside in + the local variable environment; others are sub-blocks of the stack data + block. We capture these changes in memory via a memory injection [f]: +- [f b = None] means that the Csharpminor block [b] no longer exist + in the execution of the generated Cminor code. This corresponds to + a Csharpminor local variable translated to a Cminor local variable. +- [f b = Some(b', ofs)] means that Csharpminor block [b] corresponds + to a sub-block of Cminor block [b] at offset [ofs]. + + A memory injection [f] defines a relation [val_inject f] between + values and a relation [mem_inject f] between memory states. + These relations, defined in file [Memory], will be used intensively + in our proof of simulation between Csharpminor and Cminor executions. + + In the remainder of this section, we define relations between + Csharpminor and Cminor environments and call stacks. *) + +(** Matching for a Csharpminor variable [id]. +- If this variable is mapped to a Cminor local variable, the + corresponding Csharpminor memory block [b] must no longer exist in + Cminor ([f b = None]). Moreover, the content of block [b] must + match the value of [id] found in the Cminor local environment [te]. +- If this variable is mapped to a sub-block of the Cminor stack data + at offset [ofs], the address of this variable in Csharpminor [Vptr b + Int.zero] must match the address of the sub-block [Vptr sp (Int.repr + ofs)]. +*) + +Inductive match_var (f: meminj) (id: ident) + (e: Csharpminor.env) (m: mem) (te: env) (sp: block) : + var_info -> Prop := + | match_var_local: + forall chunk b v v', + PTree.get id e = Some (b, Vscalar chunk) -> + Mem.load chunk m b 0 = Some v -> + f b = None -> + PTree.get id te = Some v' -> + val_inject f v v' -> + match_var f id e m te sp (Var_local chunk) + | match_var_stack_scalar: + forall chunk ofs b, + PTree.get id e = Some (b, Vscalar chunk) -> + val_inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) -> + match_var f id e m te sp (Var_stack_scalar chunk ofs) + | match_var_stack_array: + forall ofs sz b, + PTree.get id e = Some (b, Varray sz) -> + val_inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) -> + match_var f id e m te sp (Var_stack_array ofs) + | match_var_global_scalar: + forall chunk, + PTree.get id e = None -> + PTree.get id (global_var_env prog) = Some (Vscalar chunk) -> + match_var f id e m te sp (Var_global_scalar chunk) + | match_var_global_array: + PTree.get id e = None -> + match_var f id e m te sp (Var_global_array). + +(** Matching between a Csharpminor environment [e] and a Cminor + environment [te]. The [lo] and [hi] parameters delimit the range + of addresses for the blocks referenced from [te]. *) + +Record match_env (f: meminj) (cenv: compilenv) + (e: Csharpminor.env) (m: mem) (te: env) (sp: block) + (lo hi: Z) : Prop := + mk_match_env { + +(** Each variable mentioned in the compilation environment must match + as defined above. *) + me_vars: + forall id, match_var f id e m te sp (PMap.get id cenv); + +(** The range [lo, hi] must not be empty. *) + me_low_high: + lo <= hi; + +(** Every block appearing in the Csharpminor environment [e] must be + in the range [lo, hi]. *) + me_bounded: + forall id b lv, PTree.get id e = Some(b, lv) -> lo <= b < hi; + +(** Distinct Csharpminor local variables must be mapped to distinct blocks. *) + me_inj: + forall id1 b1 lv1 id2 b2 lv2, + PTree.get id1 e = Some(b1, lv1) -> + PTree.get id2 e = Some(b2, lv2) -> + id1 <> id2 -> b1 <> b2; + +(** All blocks mapped to sub-blocks of the Cminor stack data must be in + the range [lo, hi]. *) + me_inv: + forall b delta, + f b = Some(sp, delta) -> lo <= b < hi; + +(** All Csharpminor blocks below [lo] (i.e. allocated before the blocks + referenced from [e]) must map to blocks that are below [sp] + (i.e. allocated before the stack data for the current Cminor function). *) + me_incr: + forall b tb delta, + f b = Some(tb, delta) -> b < lo -> tb < sp + }. + +(** Global environments match if the memory injection [f] leaves unchanged + the references to global symbols and functions. *) + +Record match_globalenvs (f: meminj) : Prop := + mk_match_globalenvs { + mg_symbols: + forall id b, + Genv.find_symbol ge id = Some b -> + f b = Some (b, 0) /\ Genv.find_symbol tge id = Some b; + mg_functions: + forall b, b < 0 -> f b = Some(b, 0) + }. + +(** Call stacks represent abstractly the execution state of the current + Csharpminor and Cminor functions, as well as the states of the + calling functions. A call stack is a list of frames, each frame + collecting information on the current execution state of a Csharpminor + function and its Cminor translation. *) + +Record frame : Set := + mkframe { + fr_cenv: compilenv; + fr_e: Csharpminor.env; + fr_te: env; + fr_sp: block; + fr_low: Z; + fr_high: Z + }. + +Definition callstack : Set := list frame. + +(** Matching of call stacks imply matching of environments for each of + the frames, plus matching of the global environments, plus disjointness + conditions over the memory blocks allocated for local variables + and Cminor stack data. *) + +Inductive match_callstack: meminj -> callstack -> Z -> Z -> mem -> Prop := + | mcs_nil: + forall f bound tbound m, + match_globalenvs f -> + match_callstack f nil bound tbound m + | mcs_cons: + forall f cenv e te sp lo hi cs bound tbound m, + hi <= bound -> + sp < tbound -> + match_env f cenv e m te sp lo hi -> + match_callstack f cs lo sp m -> + match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m. + +(** The remainder of this section is devoted to showing preservation + of the [match_callstack] invariant under various assignments and memory + stores. First: preservation by memory stores to ``mapped'' blocks + (block that have a counterpart in the Cminor execution). *) + +Lemma match_env_store_mapped: + forall f cenv e m1 m2 te sp lo hi chunk b ofs v, + f b <> None -> + store chunk m1 b ofs v = Some m2 -> + match_env f cenv e m1 te sp lo hi -> + match_env f cenv e m2 te sp lo hi. +Proof. + intros. inversion H1. constructor; auto. + (* vars *) + intros. generalize (me_vars0 id); intro. + inversion H2; econstructor; eauto. + rewrite <- H5. eapply load_store_other; eauto. + left. congruence. +Qed. + +Lemma match_callstack_mapped: + forall f cs bound tbound m1, + match_callstack f cs bound tbound m1 -> + forall chunk b ofs v m2, + f b <> None -> + store chunk m1 b ofs v = Some m2 -> + match_callstack f cs bound tbound m2. +Proof. + induction 1; intros; econstructor; eauto. + eapply match_env_store_mapped; eauto. +Qed. + +(** Preservation by assignment to a Csharpminor variable that is + translated to a Cminor local variable. The value being assigned + must be normalized with respect to the memory chunk of the variable, + in the following sense. *) + +(* +Definition val_normalized (chunk: memory_chunk) (v: val) : Prop := + exists v0, v = Val.load_result chunk v0. + +Lemma load_result_idem: + forall chunk v, + Val.load_result chunk (Val.load_result chunk v) = + Val.load_result chunk v. +Proof. + destruct chunk; destruct v; simpl; auto. + rewrite Int.cast8_signed_idem; auto. + rewrite Int.cast8_unsigned_idem; auto. + rewrite Int.cast16_signed_idem; auto. + rewrite Int.cast16_unsigned_idem; auto. + rewrite Float.singleoffloat_idem; auto. +Qed. + +Lemma load_result_normalized: + forall chunk v, + val_normalized chunk v -> Val.load_result chunk v = v. +Proof. + intros chunk v [v0 EQ]. rewrite EQ. apply load_result_idem. +Qed. +*) +Lemma match_env_store_local: + forall f cenv e m1 m2 te sp lo hi id b chunk v tv, + e!id = Some(b, Vscalar chunk) -> + val_inject f (Val.load_result chunk v) tv -> + store chunk m1 b 0 v = Some m2 -> + match_env f cenv e m1 te sp lo hi -> + match_env f cenv e m2 (PTree.set id tv te) sp lo hi. +Proof. + intros. inversion H2. constructor; auto. + intros. generalize (me_vars0 id0); intro. + inversion H3; subst. + (* var_local *) + case (peq id id0); intro. + (* the stored variable *) + subst id0. + change Csharpminor.var_kind with var_kind in H4. + rewrite H in H5. injection H5; clear H5; intros; subst b0 chunk0. + econstructor. eauto. + eapply load_store_same; eauto. auto. + rewrite PTree.gss. reflexivity. + auto. + (* a different variable *) + econstructor; eauto. + rewrite <- H6. eapply load_store_other; eauto. + rewrite PTree.gso; auto. + (* var_stack_scalar *) + econstructor; eauto. + (* var_stack_array *) + econstructor; eauto. + (* var_global_scalar *) + econstructor; eauto. + (* var_global_array *) + econstructor; eauto. +Qed. + +Lemma match_env_store_above: + forall f cenv e m1 m2 te sp lo hi chunk b v, + store chunk m1 b 0 v = Some m2 -> + hi <= b -> + match_env f cenv e m1 te sp lo hi -> + match_env f cenv e m2 te sp lo hi. +Proof. + intros. inversion H1; constructor; auto. + intros. generalize (me_vars0 id); intro. + inversion H2; econstructor; eauto. + rewrite <- H5. eapply load_store_other; eauto. + left. generalize (me_bounded0 _ _ _ H4). unfold block in *. omega. +Qed. + +Lemma match_callstack_store_above: + forall f cs bound tbound m1, + match_callstack f cs bound tbound m1 -> + forall chunk b v m2, + store chunk m1 b 0 v = Some m2 -> + bound <= b -> + match_callstack f cs bound tbound m2. +Proof. + induction 1; intros; econstructor; eauto. + eapply match_env_store_above with (b := b); eauto. omega. + eapply IHmatch_callstack; eauto. + inversion H1. omega. +Qed. + +Lemma match_callstack_store_local: + forall f cenv e te sp lo hi cs bound tbound m1 m2 id b chunk v tv, + e!id = Some(b, Vscalar chunk) -> + val_inject f (Val.load_result chunk v) tv -> + store chunk m1 b 0 v = Some m2 -> + match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m1 -> + match_callstack f (mkframe cenv e (PTree.set id tv te) sp lo hi :: cs) bound tbound m2. +Proof. + intros. inversion H2. constructor; auto. + eapply match_env_store_local; eauto. + eapply match_callstack_store_above; eauto. + inversion H16. + generalize (me_bounded0 _ _ _ H). omega. +Qed. + +(** A variant of [match_callstack_store_local] where the Cminor environment + [te] already associates to [id] a value that matches the assigned value. + In this case, [match_callstack] is preserved even if no assignment + takes place on the Cminor side. *) + +Lemma match_env_extensional: + forall f cenv e m te1 sp lo hi, + match_env f cenv e m te1 sp lo hi -> + forall te2, + (forall id, te2!id = te1!id) -> + match_env f cenv e m te2 sp lo hi. +Proof. + induction 1; intros; econstructor; eauto. + intros. generalize (me_vars0 id); intro. + inversion H0; econstructor; eauto. + rewrite H. auto. +Qed. + +Lemma match_callstack_store_local_unchanged: + forall f cenv e te sp lo hi cs bound tbound m1 m2 id b chunk v tv, + e!id = Some(b, Vscalar chunk) -> + val_inject f (Val.load_result chunk v) tv -> + store chunk m1 b 0 v = Some m2 -> + te!id = Some tv -> + match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m1 -> + match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m2. +Proof. + intros. inversion H3. constructor; auto. + apply match_env_extensional with (PTree.set id tv te). + eapply match_env_store_local; eauto. + intros. rewrite PTree.gsspec. + case (peq id0 id); intros. congruence. auto. + eapply match_callstack_store_above; eauto. + inversion H17. + generalize (me_bounded0 _ _ _ H). omega. +Qed. + +(** Preservation of [match_callstack] by freeing all blocks allocated + for local variables at function entry (on the Csharpminor side). *) + +Lemma match_callstack_incr_bound: + forall f cs bound tbound m, + match_callstack f cs bound tbound m -> + forall bound' tbound', + bound <= bound' -> tbound <= tbound' -> + match_callstack f cs bound' tbound' m. +Proof. + intros. inversion H; constructor; auto. omega. omega. +Qed. + +Lemma load_freelist: + forall fbl chunk m b ofs, + (forall b', In b' fbl -> b' <> b) -> + load chunk (free_list m fbl) b ofs = load chunk m b ofs. +Proof. + induction fbl; simpl; intros. + auto. + rewrite load_free. apply IHfbl. + intros. apply H. tauto. + apply sym_not_equal. apply H. tauto. +Qed. + +Lemma match_env_freelist: + forall f cenv e m te sp lo hi fbl, + match_env f cenv e m te sp lo hi -> + (forall b, In b fbl -> hi <= b) -> + match_env f cenv e (free_list m fbl) te sp lo hi. +Proof. + intros. inversion H. econstructor; eauto. + intros. generalize (me_vars0 id); intro. + inversion H1; econstructor; eauto. + rewrite <- H4. apply load_freelist. + intros. generalize (H0 _ H8); intro. + generalize (me_bounded0 _ _ _ H3). unfold block; omega. +Qed. + +Lemma match_callstack_freelist_rec: + forall f cs bound tbound m, + match_callstack f cs bound tbound m -> + forall fbl, + (forall b, In b fbl -> bound <= b) -> + match_callstack f cs bound tbound (free_list m fbl). +Proof. + induction 1; intros; constructor; auto. + eapply match_env_freelist; eauto. + intros. generalize (H3 _ H4). omega. + apply IHmatch_callstack. intros. + generalize (H3 _ H4). inversion H1. omega. +Qed. + +Lemma match_callstack_freelist: + forall f cenv e te sp lo hi cs bound tbound m fbl, + (forall b, In b fbl -> lo <= b) -> + match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m -> + match_callstack f cs bound tbound (free_list m fbl). +Proof. + intros. inversion H0. inversion H14. + apply match_callstack_incr_bound with lo sp. + apply match_callstack_freelist_rec. auto. + assumption. + omega. omega. +Qed. + +(** Preservation of [match_callstack] when allocating a block for + a local variable on the Csharpminor side. *) + +Lemma load_from_alloc_is_undef: + forall m1 chunk m2 b, + alloc m1 0 (size_chunk chunk) = (m2, b) -> + load chunk m2 b 0 = Some Vundef. +Proof. + intros. + assert (valid_block m2 b). eapply valid_new_block; eauto. + assert (low_bound m2 b <= 0). + generalize (low_bound_alloc _ _ b _ _ _ H). rewrite zeq_true. omega. + assert (0 + size_chunk chunk <= high_bound m2 b). + generalize (high_bound_alloc _ _ b _ _ _ H). rewrite zeq_true. omega. + elim (load_in_bounds _ _ _ _ H0 H1 H2). intros v LOAD. + assert (v = Vundef). eapply load_alloc_same; eauto. + congruence. +Qed. + +Lemma match_env_alloc_same: + forall m1 lv m2 b info f1 cenv1 e1 te sp lo id data tv, + alloc m1 0 (sizeof lv) = (m2, b) -> + match info with + | Var_local chunk => data = None /\ lv = Vscalar chunk + | Var_stack_scalar chunk pos => data = Some(sp, pos) /\ lv = Vscalar chunk + | Var_stack_array pos => data = Some(sp, pos) /\ exists sz, lv = Varray sz + | Var_global_scalar chunk => False + | Var_global_array => False + end -> + match_env f1 cenv1 e1 m1 te sp lo m1.(nextblock) -> + te!id = Some tv -> + let f2 := extend_inject b data f1 in + let cenv2 := PMap.set id info cenv1 in + let e2 := PTree.set id (b, lv) e1 in + inject_incr f1 f2 -> + match_env f2 cenv2 e2 m2 te sp lo m2.(nextblock). +Proof. + intros. + assert (b = m1.(nextblock)). + injection H; intros. auto. + assert (m2.(nextblock) = Zsucc m1.(nextblock)). + injection H; intros. rewrite <- H6; reflexivity. + inversion H1. constructor. + (* me_vars *) + intros id0. unfold cenv2. rewrite PMap.gsspec. case (peq id0 id); intros. + (* same var *) + subst id0. destruct info. + (* info = Var_local chunk *) + elim H0; intros. + apply match_var_local with b Vundef tv. + unfold e2; rewrite PTree.gss. congruence. + eapply load_from_alloc_is_undef; eauto. + rewrite H7 in H. unfold sizeof in H. eauto. + unfold f2, extend_inject, eq_block. rewrite zeq_true. auto. + auto. + constructor. + (* info = Var_stack_scalar chunk ofs *) + elim H0; intros. + apply match_var_stack_scalar with b. + unfold e2; rewrite PTree.gss. congruence. + eapply val_inject_ptr. + unfold f2, extend_inject, eq_block. rewrite zeq_true. eauto. + rewrite Int.add_commut. rewrite Int.add_zero. auto. + (* info = Var_stack_array z *) + elim H0; intros A [sz B]. + apply match_var_stack_array with sz b. + unfold e2; rewrite PTree.gss. congruence. + eapply val_inject_ptr. + unfold f2, extend_inject, eq_block. rewrite zeq_true. eauto. + rewrite Int.add_commut. rewrite Int.add_zero. auto. + (* info = Var_global *) + contradiction. + contradiction. + (* other vars *) + generalize (me_vars0 id0); intros. + inversion H6; econstructor; eauto. + unfold e2; rewrite PTree.gso; auto. + unfold f2, extend_inject, eq_block; rewrite zeq_false; auto. + generalize (me_bounded0 _ _ _ H8). unfold block in *; omega. + unfold e2; rewrite PTree.gso; eauto. + unfold e2; rewrite PTree.gso; eauto. + unfold e2; rewrite PTree.gso; eauto. + unfold e2; rewrite PTree.gso; eauto. + (* lo <= hi *) + unfold block in *; omega. + (* me_bounded *) + intros until lv0. unfold e2; rewrite PTree.gsspec. + case (peq id0 id); intros. + subst id0. inversion H6. subst b0. unfold block in *; omega. + generalize (me_bounded0 _ _ _ H6). rewrite H5. omega. + (* me_inj *) + intros until lv2. unfold e2; repeat rewrite PTree.gsspec. + case (peq id1 id); case (peq id2 id); intros. + congruence. + inversion H6. subst b1. rewrite H4. + generalize (me_bounded0 _ _ _ H7). unfold block; omega. + inversion H7. subst b2. rewrite H4. + generalize (me_bounded0 _ _ _ H6). unfold block; omega. + eauto. + (* me_inv *) + intros until delta. unfold f2, extend_inject, eq_block. + case (zeq b0 b); intros. + subst b0. rewrite H4; rewrite H5. omega. + generalize (me_inv0 _ _ H6). rewrite H5. omega. + (* me_incr *) + intros until delta. unfold f2, extend_inject, eq_block. + case (zeq b0 b); intros. + subst b0. unfold block in *; omegaContradiction. + eauto. +Qed. + +Lemma match_env_alloc_other: + forall f1 cenv e m1 m2 te sp lo hi chunk b data, + alloc m1 0 (sizeof chunk) = (m2, b) -> + match data with None => True | Some (b', delta') => sp < b' end -> + hi <= m1.(nextblock) -> + match_env f1 cenv e m1 te sp lo hi -> + let f2 := extend_inject b data f1 in + inject_incr f1 f2 -> + match_env f2 cenv e m2 te sp lo hi. +Proof. + intros. + assert (b = m1.(nextblock)). injection H; auto. + rewrite <- H4 in H1. + inversion H2. constructor; auto. + (* me_vars *) + intros. generalize (me_vars0 id); intro. + inversion H5; econstructor; eauto. + unfold f2, extend_inject, eq_block. rewrite zeq_false. auto. + generalize (me_bounded0 _ _ _ H7). unfold block in *; omega. + (* me_bounded *) + intros until delta. unfold f2, extend_inject, eq_block. + case (zeq b0 b); intros. rewrite H5 in H0. omegaContradiction. + eauto. + (* me_incr *) + intros until delta. unfold f2, extend_inject, eq_block. + case (zeq b0 b); intros. subst b0. omegaContradiction. + eauto. +Qed. + +Lemma match_callstack_alloc_other: + forall f1 cs bound tbound m1, + match_callstack f1 cs bound tbound m1 -> + forall lv m2 b data, + alloc m1 0 (sizeof lv) = (m2, b) -> + match data with None => True | Some (b', delta') => tbound <= b' end -> + bound <= m1.(nextblock) -> + let f2 := extend_inject b data f1 in + inject_incr f1 f2 -> + match_callstack f2 cs bound tbound m2. +Proof. + induction 1; intros. + constructor. + inversion H. constructor. + intros. auto. + intros. elim (mg_symbols0 _ _ H4); intros. + split; auto. elim (H3 b0); intros; congruence. + intros. generalize (mg_functions0 _ H4). elim (H3 b0); congruence. + constructor. auto. auto. + unfold f2; eapply match_env_alloc_other; eauto. + destruct data; auto. destruct p. omega. omega. + unfold f2; eapply IHmatch_callstack; eauto. + destruct data; auto. destruct p. omega. + inversion H1; omega. +Qed. + +Lemma match_callstack_alloc_left: + forall m1 lv m2 b info f1 cenv1 e1 te sp lo id data cs tv tbound, + alloc m1 0 (sizeof lv) = (m2, b) -> + match info with + | Var_local chunk => data = None /\ lv = Vscalar chunk + | Var_stack_scalar chunk pos => data = Some(sp, pos) /\ lv = Vscalar chunk + | Var_stack_array pos => data = Some(sp, pos) /\ exists sz, lv = Varray sz + | Var_global_scalar chunk => False + | Var_global_array => False + end -> + match_callstack f1 (mkframe cenv1 e1 te sp lo m1.(nextblock) :: cs) m1.(nextblock) tbound m1 -> + te!id = Some tv -> + let f2 := extend_inject b data f1 in + let cenv2 := PMap.set id info cenv1 in + let e2 := PTree.set id (b, lv) e1 in + inject_incr f1 f2 -> + match_callstack f2 (mkframe cenv2 e2 te sp lo m2.(nextblock) :: cs) m2.(nextblock) tbound m2. +Proof. + intros. inversion H1. constructor. omega. auto. + unfold f2, cenv2, e2. eapply match_env_alloc_same; eauto. + unfold f2; eapply match_callstack_alloc_other; eauto. + destruct info. + elim H0; intros. rewrite H19. auto. + elim H0; intros. rewrite H19. omega. + elim H0; intros. rewrite H19. omega. + contradiction. + contradiction. + inversion H17; omega. +Qed. + +Lemma match_callstack_alloc_right: + forall f cs bound tm1 m tm2 lo hi b, + alloc tm1 lo hi = (tm2, b) -> + match_callstack f cs bound tm1.(nextblock) m -> + match_callstack f cs bound tm2.(nextblock) m. +Proof. + intros. eapply match_callstack_incr_bound; eauto. omega. + injection H; intros. rewrite <- H2; simpl. omega. +Qed. + +Lemma match_env_alloc: + forall m1 l h m2 b tm1 tm2 tb f1 ce e te sp lo hi, + alloc m1 l h = (m2, b) -> + alloc tm1 l h = (tm2, tb) -> + match_env f1 ce e m1 te sp lo hi -> + hi <= m1.(nextblock) -> + sp < tm1.(nextblock) -> + let f2 := extend_inject b (Some(tb, 0)) f1 in + inject_incr f1 f2 -> + match_env f2 ce e m2 te sp lo hi. +Proof. + intros. + assert (BEQ: b = m1.(nextblock)). injection H; auto. + assert (TBEQ: tb = tm1.(nextblock)). injection H0; auto. + inversion H1. constructor; auto. + (* me_vars *) + intros. generalize (me_vars0 id); intro. inversion H5. + (* var_local *) + econstructor; eauto. + generalize (me_bounded0 _ _ _ H7). intro. + unfold f2, extend_inject. case (eq_block b0 b); intro. + subst b0. rewrite BEQ in H12. omegaContradiction. + auto. + (* var_stack_scalar *) + econstructor; eauto. + (* var_stack_array *) + econstructor; eauto. + (* var_global_scalar *) + econstructor; eauto. + (* var_global_array *) + econstructor; eauto. + (* me_bounded *) + intros until delta. unfold f2, extend_inject. case (eq_block b0 b); intro. + intro. injection H5; clear H5; intros. + rewrite H6 in TBEQ. rewrite TBEQ in H3. omegaContradiction. + eauto. + (* me_inj *) + intros until delta. unfold f2, extend_inject. case (eq_block b0 b); intros. + injection H5; clear H5; intros; subst b0 tb0 delta. + rewrite BEQ in H6. omegaContradiction. + eauto. +Qed. + +Lemma match_callstack_alloc_rec: + forall f1 cs bound tbound m1, + match_callstack f1 cs bound tbound m1 -> + forall l h m2 b tm1 tm2 tb, + alloc m1 l h = (m2, b) -> + alloc tm1 l h = (tm2, tb) -> + bound <= m1.(nextblock) -> + tbound <= tm1.(nextblock) -> + let f2 := extend_inject b (Some(tb, 0)) f1 in + inject_incr f1 f2 -> + match_callstack f2 cs bound tbound m2. +Proof. + induction 1; intros. + constructor. + inversion H. constructor. + intros. elim (mg_symbols0 _ _ H5); intros. + split; auto. elim (H4 b0); intros; congruence. + intros. generalize (mg_functions0 _ H5). elim (H4 b0); congruence. + constructor. auto. auto. + unfold f2. eapply match_env_alloc; eauto. omega. omega. + unfold f2; eapply IHmatch_callstack; eauto. + inversion H1; omega. + omega. +Qed. + +Lemma match_callstack_alloc: + forall f1 cs m1 tm1 l h m2 b tm2 tb, + match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1 -> + alloc m1 l h = (m2, b) -> + alloc tm1 l h = (tm2, tb) -> + let f2 := extend_inject b (Some(tb, 0)) f1 in + inject_incr f1 f2 -> + match_callstack f2 cs m2.(nextblock) tm2.(nextblock) m2. +Proof. + intros. unfold f2 in *. + apply match_callstack_incr_bound with m1.(nextblock) tm1.(nextblock). + eapply match_callstack_alloc_rec; eauto. omega. omega. + injection H0; intros; subst m2; simpl; omega. + injection H1; intros; subst tm2; simpl; omega. +Qed. + +(** [match_callstack] implies [match_globalenvs]. *) + +Lemma match_callstack_match_globalenvs: + forall f cs bound tbound m, + match_callstack f cs bound tbound m -> + match_globalenvs f. +Proof. + induction 1; eauto. +Qed. + +(** * Correctness of Cminor construction functions *) + +Hint Resolve eval_negint eval_negfloat eval_absfloat eval_intoffloat + eval_floatofint eval_floatofintu eval_notint eval_notbool + eval_cast8signed eval_cast8unsigned eval_cast16signed + eval_cast16unsigned eval_singleoffloat eval_add eval_add_ptr + eval_add_ptr_2 eval_sub eval_sub_ptr_int eval_sub_ptr_ptr + eval_mul eval_divs eval_mods eval_divu eval_modu + eval_and eval_or eval_xor eval_shl eval_shr eval_shru + eval_addf eval_subf eval_mulf eval_divf + eval_cmp eval_cmp_null_r eval_cmp_null_l eval_cmp_ptr + eval_cmpu eval_cmpf: evalexpr. + +Remark val_inject_val_of_bool: + forall f b, val_inject f (Val.of_bool b) (Val.of_bool b). +Proof. + intros; destruct b; unfold Val.of_bool, Vtrue, Vfalse; constructor. +Qed. + +Ltac TrivialOp := + match goal with + | [ |- exists x, _ /\ val_inject _ (Vint ?x) _ ] => + exists (Vint x); split; + [eauto with evalexpr | constructor] + | [ |- exists x, _ /\ val_inject _ (Vfloat ?x) _ ] => + exists (Vfloat x); split; + [eauto with evalexpr | constructor] + | [ |- exists x, _ /\ val_inject _ (Val.of_bool ?x) _ ] => + exists (Val.of_bool x); split; + [eauto with evalexpr | apply val_inject_val_of_bool] + | _ => idtac + end. + +Remark eval_compare_null_inv: + forall c i v, + Csharpminor.eval_compare_null c i = Some v -> + i = Int.zero /\ (c = Ceq /\ v = Vfalse \/ c = Cne /\ v = Vtrue). +Proof. + intros until v. unfold Csharpminor.eval_compare_null. + predSpec Int.eq Int.eq_spec i Int.zero. + case c; intro EQ; simplify_eq EQ; intro; subst v; tauto. + congruence. +Qed. + +(** Correctness of [make_op]. The generated Cminor code evaluates + to a value that matches the result value of the Csharpminor operation, + provided arguments match pairwise ([val_list_inject f] hypothesis). *) + +Lemma make_op_correct: + forall al a op vl m2 v sp le te1 tm1 t te2 tm2 tvl f, + make_op op al = Some a -> + Csharpminor.eval_operation op vl m2 = Some v -> + eval_exprlist tge (Vptr sp Int.zero) le te1 tm1 al t te2 tm2 tvl -> + val_list_inject f vl tvl -> + mem_inject f m2 tm2 -> + exists tv, + eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 tv + /\ val_inject f v tv. +Proof. + intros. + destruct al as [ | a1 al]; + [idtac | destruct al as [ | a2 al]; + [idtac | destruct al as [ | a3 al]]]; + simpl in H; try discriminate. + (* Constant operators *) + inversion H1. subst sp0 le0 e m te2 tm1 tvl. + inversion H2. subst vl. + destruct op; simplify_eq H; intro; subst a; + simpl in H0; injection H0; intro; subst v. + (* intconst *) + TrivialOp. econstructor. constructor. reflexivity. + (* floatconst *) + TrivialOp. econstructor. constructor. reflexivity. + (* Unary operators *) + inversion H1; clear H1; subst. + inversion H11; clear H11; subst. + rewrite E0_right. + inversion H2; clear H2; subst. inversion H8; clear H8; subst. + destruct op; simplify_eq H; intro; subst a; + simpl in H0; destruct v1; simplify_eq H0; intro; subst v; + inversion H7; subst v0; + TrivialOp. + change (Vint (Int.cast8unsigned i)) with (Val.cast8unsigned (Vint i)). eauto with evalexpr. + change (Vint (Int.cast8signed i)) with (Val.cast8signed (Vint i)). eauto with evalexpr. + change (Vint (Int.cast16unsigned i)) with (Val.cast16unsigned (Vint i)). eauto with evalexpr. + change (Vint (Int.cast16signed i)) with (Val.cast16signed (Vint i)). eauto with evalexpr. + change (Vfloat (Float.singleoffloat f0)) with (Val.singleoffloat (Vfloat f0)). eauto with evalexpr. + (* Binary operations *) + inversion H1; clear H1; subst. inversion H11; clear H11; subst. + inversion H12; clear H12; subst. rewrite E0_right. + inversion H2; clear H2; subst. inversion H9; clear H9; subst. + inversion H10; clear H10; subst. + destruct op; simplify_eq H; intro; subst a; + simpl in H0; destruct v2; destruct v3; simplify_eq H0; intro; try subst v; + inversion H7; inversion H8; subst v0; subst v1; + TrivialOp. + (* add int ptr *) + exists (Vptr b2 (Int.add ofs2 i)); split. + eauto with evalexpr. apply val_inject_ptr with x. auto. + subst ofs2. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + (* add ptr int *) + exists (Vptr b2 (Int.add ofs2 i0)); split. + eauto with evalexpr. apply val_inject_ptr with x. auto. + subst ofs2. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + (* sub ptr int *) + exists (Vptr b2 (Int.sub ofs2 i0)); split. + eauto with evalexpr. apply val_inject_ptr with x. auto. + subst ofs2. apply Int.sub_add_l. + (* sub ptr ptr *) + destruct (eq_block b b0); simplify_eq H0; intro; subst v; subst b0. + assert (b4 = b2). congruence. subst b4. + exists (Vint (Int.sub ofs3 ofs2)); split. + eauto with evalexpr. + subst ofs2 ofs3. replace x0 with x. rewrite Int.sub_shifted. constructor. + congruence. + (* divs *) + generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro; + simplify_eq H0; intro; subst v. TrivialOp. + (* divu *) + generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro; + simplify_eq H0; intro; subst v. TrivialOp. + (* mods *) + generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro; + simplify_eq H0; intro; subst v. TrivialOp. + (* modu *) + generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro; + simplify_eq H0; intro; subst v. TrivialOp. + (* shl *) + caseEq (Int.ltu i0 (Int.repr 32)); intro EQ; rewrite EQ in H0; + simplify_eq H0; intro; subst v. TrivialOp. + (* shr *) + caseEq (Int.ltu i0 (Int.repr 32)); intro EQ; rewrite EQ in H0; + simplify_eq H0; intro; subst v. TrivialOp. + (* shru *) + caseEq (Int.ltu i0 (Int.repr 32)); intro EQ; rewrite EQ in H0; + simplify_eq H0; intro; subst v. TrivialOp. + (* cmp int ptr *) + elim (eval_compare_null_inv _ _ _ H0); intros; subst i1 i. + exists v; split. eauto with evalexpr. + elim H12; intros [A B]; subst v; unfold Vtrue, Vfalse; constructor. + (* cmp ptr int *) + elim (eval_compare_null_inv _ _ _ H0); intros; subst i1 i0. + exists v; split. eauto with evalexpr. + elim H12; intros [A B]; subst v; unfold Vtrue, Vfalse; constructor. + (* cmp ptr ptr *) + caseEq (valid_pointer m2 b (Int.signed i) && valid_pointer m2 b0 (Int.signed i0)); + intro EQ; rewrite EQ in H0; try discriminate. + destruct (eq_block b b0); simplify_eq H0; intro; subst v b0. + assert (b4 = b2); [congruence|subst b4]. + assert (x0 = x); [congruence|subst x0]. + elim (andb_prop _ _ EQ); intros. + exists (Val.of_bool (Int.cmp c ofs3 ofs2)); split. + eauto with evalexpr. + subst ofs2 ofs3. rewrite Int.translate_cmp. + apply val_inject_val_of_bool. + eapply valid_pointer_inject_no_overflow; eauto. + eapply valid_pointer_inject_no_overflow; eauto. +Qed. + +(** Correctness of [make_cast]. Note that the resulting Cminor value is + normalized according to the given memory chunk. *) + +Lemma make_cast_correct: + forall f sp le te1 tm1 a t te2 tm2 v chunk tv, + eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 tv -> + val_inject f v tv -> + exists tv', + eval_expr tge (Vptr sp Int.zero) le + te1 tm1 (make_cast chunk a) + t te2 tm2 tv' + /\ val_inject f (Val.load_result chunk v) tv'. +Proof. + intros. destruct chunk. + + exists (Val.cast8signed tv). + split. apply eval_cast8signed; auto. + inversion H0; simpl; constructor. + + exists (Val.cast8unsigned tv). + split. apply eval_cast8unsigned; auto. + inversion H0; simpl; constructor. + + exists (Val.cast16signed tv). + split. apply eval_cast16signed; auto. + inversion H0; simpl; constructor. + + exists (Val.cast16unsigned tv). + split. apply eval_cast16unsigned; auto. + inversion H0; simpl; constructor. + + exists tv. + split. simpl; auto. + inversion H0; simpl; econstructor; eauto. + + exists (Val.singleoffloat tv). + split. apply eval_singleoffloat; auto. + inversion H0; simpl; constructor. + + exists tv. + split. simpl; auto. + inversion H0; simpl; constructor. +Qed. + +Lemma make_stackaddr_correct: + forall sp le te tm ofs, + eval_expr tge (Vptr sp Int.zero) le + te tm (make_stackaddr ofs) + E0 te tm (Vptr sp (Int.repr ofs)). +Proof. + intros; unfold make_stackaddr. + eapply eval_Eop. econstructor. simpl. decEq. decEq. + rewrite Int.add_commut. apply Int.add_zero. +Qed. + +Lemma make_globaladdr_correct: + forall sp le te tm id b, + Genv.find_symbol tge id = Some b -> + eval_expr tge (Vptr sp Int.zero) le + te tm (make_globaladdr id) + E0 te tm (Vptr b Int.zero). +Proof. + intros; unfold make_globaladdr. + eapply eval_Eop. econstructor. simpl. rewrite H. auto. +Qed. + +(** Correctness of [make_load] and [make_store]. *) + +Lemma make_load_correct: + forall sp le te1 tm1 a t te2 tm2 va chunk v, + eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 va -> + Mem.loadv chunk tm2 va = Some v -> + eval_expr tge (Vptr sp Int.zero) le + te1 tm1 (make_load chunk a) + t te2 tm2 v. +Proof. + intros; unfold make_load. + eapply eval_load; eauto. +Qed. + +Lemma store_arg_content_inject: + forall f sp le te1 tm1 a t te2 tm2 v va chunk, + eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 va -> + val_inject f v va -> + exists vb, + eval_expr tge (Vptr sp Int.zero) le te1 tm1 (store_arg chunk a) t te2 tm2 vb + /\ val_content_inject f (mem_chunk chunk) v vb. +Proof. + intros. + assert (exists vb, + eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 vb + /\ val_content_inject f (mem_chunk chunk) v vb). + exists va; split. assumption. constructor. assumption. + inversion H; clear H; subst; simpl; trivial. + inversion H2; clear H2; subst; trivial. + inversion H4; clear H4; subst; trivial. + rewrite E0_right. rewrite E0_right in H1. + destruct op; trivial; destruct chunk; trivial; + exists v0; (split; [auto| + simpl in H3; inversion H3; clear H3; subst va; + destruct v0; simpl in H0; inversion H0; subst; try (constructor; constructor)]). + apply val_content_inject_8. apply Int.cast8_unsigned_signed. + apply val_content_inject_8. apply Int.cast8_unsigned_idem. + apply val_content_inject_16. apply Int.cast16_unsigned_signed. + apply val_content_inject_16. apply Int.cast16_unsigned_idem. + apply val_content_inject_32. apply Float.singleoffloat_idem. +Qed. + +Lemma make_store_correct: + forall f sp te1 tm1 addr te2 tm2 tvaddr rhs te3 tm3 tvrhs + chunk vrhs m3 vaddr m4 t1 t2, + eval_expr tge (Vptr sp Int.zero) nil + te1 tm1 addr t1 te2 tm2 tvaddr -> + eval_expr tge (Vptr sp Int.zero) nil + te2 tm2 rhs t2 te3 tm3 tvrhs -> + Mem.storev chunk m3 vaddr vrhs = Some m4 -> + mem_inject f m3 tm3 -> + val_inject f vaddr tvaddr -> + val_inject f vrhs tvrhs -> + exists tm4, + exec_stmt tge (Vptr sp Int.zero) + te1 tm1 (make_store chunk addr rhs) + (t1**t2) te3 tm4 Out_normal + /\ mem_inject f m4 tm4 + /\ nextblock tm4 = nextblock tm3. +Proof. + intros. unfold make_store. + exploit store_arg_content_inject. eexact H0. eauto. + intros [tv [EVAL VCINJ]]. + exploit storev_mapped_inject_1; eauto. + intros [tm4 [STORE MEMINJ]]. + exploit eval_store. eexact H. eexact EVAL. eauto. + intro EVALSTORE. + exists tm4. + split. apply exec_Sexpr with tv. auto. + split. auto. + unfold storev in STORE; destruct tvaddr; try discriminate. + exploit store_inv; eauto. simpl. tauto. +Qed. + +(** Correctness of the variable accessors [var_get], [var_set] + and [var_addr]. *) + +Lemma var_get_correct: + forall cenv id a f e te sp lo hi m cs tm b chunk v le, + var_get cenv id = Some a -> + match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> + mem_inject f m tm -> + eval_var_ref prog e id b chunk -> + load chunk m b 0 = Some v -> + exists tv, + eval_expr tge (Vptr sp Int.zero) le te tm a E0 te tm tv /\ + val_inject f v tv. +Proof. + unfold var_get; intros. + assert (match_var f id e m te sp cenv!!id). + inversion H0. inversion H17. auto. + inversion H4; subst; rewrite <- H5 in H; inversion H; subst. + (* var_local *) + inversion H2; [subst|congruence]. + exists v'; split. + apply eval_Evar. auto. + replace v with v0. auto. congruence. + (* var_stack_scalar *) + inversion H2; [subst|congruence]. + assert (b0 = b). congruence. subst b0. + assert (chunk0 = chunk). congruence. subst chunk0. + exploit loadv_inject; eauto. + unfold loadv. eexact H3. + intros [tv [LOAD INJ]]. + exists tv; split. + eapply make_load_correct; eauto. eapply make_stackaddr_correct; eauto. + auto. + (* var_global_scalar *) + inversion H2; [congruence|subst]. + assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. + inversion H11. destruct (mg_symbols0 _ _ H9) as [A B]. + assert (chunk0 = chunk). congruence. subst chunk0. + assert (loadv chunk m (Vptr b Int.zero) = Some v). assumption. + assert (val_inject f (Vptr b Int.zero) (Vptr b Int.zero)). + econstructor; eauto. + generalize (loadv_inject _ _ _ _ _ _ _ H1 H12 H13). + intros [tv [LOAD INJ]]. + exists tv; split. + eapply make_load_correct; eauto. eapply make_globaladdr_correct; eauto. + auto. +Qed. + +Lemma var_addr_correct: + forall cenv id a f e te sp lo hi m cs tm b le, + match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> + var_addr cenv id = Some a -> + eval_var_addr prog e id b -> + exists tv, + eval_expr tge (Vptr sp Int.zero) le te tm a E0 te tm tv /\ + val_inject f (Vptr b Int.zero) tv. +Proof. + unfold var_addr; intros. + assert (match_var f id e m te sp cenv!!id). + inversion H. inversion H15. auto. + inversion H2; subst; rewrite <- H3 in H0; inversion H0; subst; clear H0. + (* var_stack_scalar *) + inversion H1; [subst|congruence]. + exists (Vptr sp (Int.repr ofs)); split. + eapply make_stackaddr_correct. + replace b with b0. auto. congruence. + (* var_stack_array *) + inversion H1; [subst|congruence]. + exists (Vptr sp (Int.repr ofs)); split. + eapply make_stackaddr_correct. + replace b with b0. auto. congruence. + (* var_global_scalar *) + inversion H1; [congruence|subst]. + assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. + inversion H7. destruct (mg_symbols0 _ _ H6) as [A B]. + exists (Vptr b Int.zero); split. + eapply make_globaladdr_correct. eauto. + econstructor; eauto. + (* var_global_array *) + inversion H1; [congruence|subst]. + assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. + inversion H6. destruct (mg_symbols0 _ _ H5) as [A B]. + exists (Vptr b Int.zero); split. + eapply make_globaladdr_correct. eauto. + econstructor; eauto. +Qed. + +Lemma var_set_correct: + forall cenv id rhs a f e te2 sp lo hi m2 cs tm2 te1 tm1 tv b chunk v m3 t, + var_set cenv id rhs = Some a -> + match_callstack f (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2 -> + eval_expr tge (Vptr sp Int.zero) nil te1 tm1 rhs t te2 tm2 tv -> + val_inject f v tv -> + mem_inject f m2 tm2 -> + eval_var_ref prog e id b chunk -> + store chunk m2 b 0 v = Some m3 -> + exists te3, exists tm3, + exec_stmt tge (Vptr sp Int.zero) te1 tm1 a t te3 tm3 Out_normal /\ + mem_inject f m3 tm3 /\ + match_callstack f (mkframe cenv e te3 sp lo hi :: cs) m3.(nextblock) tm3.(nextblock) m3. +Proof. + unfold var_set; intros. + assert (NEXTBLOCK: nextblock m3 = nextblock m2). + exploit store_inv; eauto. simpl; tauto. + inversion H0. subst f0 cenv0 e0 te sp0 lo0 hi0 cs0 bound tbound m. + assert (match_var f id e m2 te2 sp cenv!!id). inversion H19; auto. + inversion H6; subst; rewrite <- H7 in H; inversion H; subst; clear H. + (* var_local *) + inversion H4; [subst|congruence]. + assert (b0 = b). congruence. subst b0. + assert (chunk0 = chunk). congruence. subst chunk0. + exploit make_cast_correct; eauto. + intros [tv' [EVAL INJ]]. + exists (PTree.set id tv' te2); exists tm2. + split. eapply exec_Sexpr. eapply eval_Eassign. eauto. + split. eapply store_unmapped_inject; eauto. + rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto. + (* var_stack_scalar *) + inversion H4; [subst|congruence]. + assert (b0 = b). congruence. subst b0. + assert (chunk0 = chunk). congruence. subst chunk0. + assert (storev chunk m2 (Vptr b Int.zero) v = Some m3). assumption. + exploit make_store_correct. + eapply make_stackaddr_correct. + eauto. eauto. eauto. eauto. eauto. + rewrite E0_left. intros [tm3 [EVAL [MEMINJ TNEXTBLOCK]]]. + exists te2; exists tm3. + split. auto. split. auto. + rewrite NEXTBLOCK; rewrite TNEXTBLOCK. + eapply match_callstack_mapped; eauto. + inversion H9; congruence. + (* var_global_scalar *) + inversion H4; [congruence|subst]. + assert (chunk0 = chunk). congruence. subst chunk0. + assert (storev chunk m2 (Vptr b Int.zero) v = Some m3). assumption. + assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. + inversion H13. destruct (mg_symbols0 _ _ H10) as [A B]. + exploit make_store_correct. + eapply make_globaladdr_correct; eauto. + eauto. eauto. eauto. eauto. eauto. + rewrite E0_left. intros [tm3 [EVAL [MEMINJ TNEXTBLOCK]]]. + exists te2; exists tm3. + split. auto. split. auto. + rewrite NEXTBLOCK; rewrite TNEXTBLOCK. + eapply match_callstack_mapped; eauto. congruence. +Qed. + +(** * Correctness of stack allocation of local variables *) + +(** This section shows the correctness of the translation of Csharpminor + local variables, either as Cminor local variables or as sub-blocks + of the Cminor stack data. This is the most difficult part of the proof. *) + +Remark assign_variables_incr: + forall atk vars cenv sz cenv' sz', + assign_variables atk vars (cenv, sz) = (cenv', sz') -> sz <= sz'. +Proof. + induction vars; intros until sz'; simpl. + intro. replace sz' with sz. omega. congruence. + destruct a. destruct v. case (Identset.mem i atk); intros. + generalize (IHvars _ _ _ _ H). + generalize (size_chunk_pos m). intro. + generalize (align_le sz (size_chunk m) H0). omega. + eauto. + intro. generalize (IHvars _ _ _ _ H). + assert (8 > 0). omega. generalize (align_le sz 8 H0). + assert (0 <= Zmax 0 z). apply Zmax_bound_l. omega. + omega. +Qed. + +Lemma match_callstack_alloc_variables_rec: + forall tm sp cenv' sz' te lo cs atk, + valid_block tm sp -> + low_bound tm sp = 0 -> + high_bound tm sp = sz' -> + sz' <= Int.max_signed -> + forall e m vars e' m' lb, + alloc_variables e m vars e' m' lb -> + forall f cenv sz, + assign_variables atk vars (cenv, sz) = (cenv', sz') -> + match_callstack f (mkframe cenv e te sp lo m.(nextblock) :: cs) + m.(nextblock) tm.(nextblock) m -> + mem_inject f m tm -> + 0 <= sz -> + (forall b delta, f b = Some(sp, delta) -> high_bound m b + delta <= sz) -> + (forall id lv, In (id, lv) vars -> te!id <> None) -> + exists f', + inject_incr f f' + /\ mem_inject f' m' tm + /\ match_callstack f' (mkframe cenv' e' te sp lo m'.(nextblock) :: cs) + m'.(nextblock) tm.(nextblock) m'. +Proof. + intros until atk. intros VB LB HB NOOV. + induction 1. + (* base case *) + intros. simpl in H. inversion H; subst cenv sz. + exists f. split. apply inject_incr_refl. split. auto. auto. + (* inductive case *) + intros until sz. + change (assign_variables atk ((id, lv) :: vars) (cenv, sz)) + with (assign_variables atk vars (assign_variable atk (id, lv) (cenv, sz))). + caseEq (assign_variable atk (id, lv) (cenv, sz)). + intros cenv1 sz1 ASV1 ASVS MATCH MINJ SZPOS BOUND DEFINED. + assert (DEFINED1: forall id0 lv0, In (id0, lv0) vars -> te!id0 <> None). + intros. eapply DEFINED. simpl. right. eauto. + assert (exists tv, te!id = Some tv). + assert (te!id <> None). eapply DEFINED. simpl; left; auto. + destruct (te!id). exists v; auto. congruence. + elim H1; intros tv TEID; clear H1. + generalize ASV1. unfold assign_variable. + caseEq lv. + (* 1. lv = LVscalar chunk *) + intros chunk LV. case (Identset.mem id atk). + (* 1.1 info = Var_stack_scalar chunk ... *) + set (ofs := align sz (size_chunk chunk)). + intro EQ; injection EQ; intros; clear EQ. + set (f1 := extend_inject b1 (Some (sp, ofs)) f). + generalize (size_chunk_pos chunk); intro SIZEPOS. + generalize (align_le sz (size_chunk chunk) SIZEPOS). fold ofs. intro SZOFS. + assert (mem_inject f1 m1 tm /\ inject_incr f f1). + assert (Int.min_signed < 0). compute; auto. + generalize (assign_variables_incr _ _ _ _ _ _ ASVS). intro. + unfold f1; eapply alloc_mapped_inject; eauto. + omega. omega. omega. omega. unfold sizeof; rewrite LV. omega. + intros. left. generalize (BOUND _ _ H5). omega. + elim H3; intros MINJ1 INCR1; clear H3. + exploit IHalloc_variables; eauto. + unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. + rewrite <- H1. omega. + intros until delta; unfold f1, extend_inject, eq_block. + rewrite (high_bound_alloc _ _ b _ _ _ H). + case (zeq b b1); intros. + inversion H3. unfold sizeof; rewrite LV. omega. + generalize (BOUND _ _ H3). omega. + intros [f' [INCR2 [MINJ2 MATCH2]]]. + exists f'; intuition. eapply inject_incr_trans; eauto. + (* 1.2 info = Var_local chunk *) + intro EQ; injection EQ; intros; clear EQ. subst sz1. + exploit alloc_unmapped_inject; eauto. + set (f1 := extend_inject b1 None f). intros [MINJ1 INCR1]. + exploit IHalloc_variables; eauto. + unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. + intros until delta; unfold f1, extend_inject, eq_block. + rewrite (high_bound_alloc _ _ b _ _ _ H). + case (zeq b b1); intros. discriminate. + eapply BOUND; eauto. + intros [f' [INCR2 [MINJ2 MATCH2]]]. + exists f'; intuition. eapply inject_incr_trans; eauto. + (* 2. lv = LVarray dim, info = Var_stack_array *) + intros dim LV EQ. injection EQ; clear EQ; intros. + assert (0 <= Zmax 0 dim). apply Zmax1. + assert (8 > 0). omega. + generalize (align_le sz 8 H4). intro. + set (ofs := align sz 8) in *. + set (f1 := extend_inject b1 (Some (sp, ofs)) f). + assert (mem_inject f1 m1 tm /\ inject_incr f f1). + assert (Int.min_signed < 0). compute; auto. + generalize (assign_variables_incr _ _ _ _ _ _ ASVS). intro. + unfold f1; eapply alloc_mapped_inject; eauto. + omega. omega. omega. omega. unfold sizeof; rewrite LV. omega. + intros. left. generalize (BOUND _ _ H8). omega. + destruct H6 as [MINJ1 INCR1]. + exploit IHalloc_variables; eauto. + unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. + rewrite <- H1. omega. + intros until delta; unfold f1, extend_inject, eq_block. + rewrite (high_bound_alloc _ _ b _ _ _ H). + case (zeq b b1); intros. + inversion H6. unfold sizeof; rewrite LV. omega. + generalize (BOUND _ _ H6). omega. + intros [f' [INCR2 [MINJ2 MATCH2]]]. + exists f'; intuition. eapply inject_incr_trans; eauto. +Qed. + +Lemma set_params_defined: + forall params args id, + In id params -> (set_params args params)!id <> None. +Proof. + induction params; simpl; intros. + elim H. + destruct args. + rewrite PTree.gsspec. case (peq id a); intro. + congruence. eapply IHparams. elim H; intro. congruence. auto. + rewrite PTree.gsspec. case (peq id a); intro. + congruence. eapply IHparams. elim H; intro. congruence. auto. +Qed. + +Lemma set_locals_defined: + forall e vars id, + In id vars \/ e!id <> None -> (set_locals vars e)!id <> None. +Proof. + induction vars; simpl; intros. + tauto. + rewrite PTree.gsspec. case (peq id a); intro. + congruence. + apply IHvars. assert (a <> id). congruence. tauto. +Qed. + +Lemma set_locals_params_defined: + forall args params vars id, + In id (params ++ vars) -> + (set_locals vars (set_params args params))!id <> None. +Proof. + intros. apply set_locals_defined. + elim (in_app_or _ _ _ H); intro. + right. apply set_params_defined; auto. + left; auto. +Qed. + +(** Preservation of [match_callstack] by simultaneous allocation + of Csharpminor local variables and of the Cminor stack data block. *) + +Lemma match_callstack_alloc_variables: + forall fn cenv sz m e m' lb tm tm' sp f cs targs, + build_compilenv gce fn = (cenv, sz) -> + sz <= Int.max_signed -> + alloc_variables Csharpminor.empty_env m (fn_variables fn) e m' lb -> + Mem.alloc tm 0 sz = (tm', sp) -> + match_callstack f cs m.(nextblock) tm.(nextblock) m -> + mem_inject f m tm -> + let tparams := List.map (@fst ident memory_chunk) fn.(Csharpminor.fn_params) in + let tvars := List.map (@fst ident var_kind) fn.(Csharpminor.fn_vars) in + let te := set_locals tvars (set_params targs tparams) in + exists f', + inject_incr f f' + /\ mem_inject f' m' tm' + /\ match_callstack f' (mkframe cenv e te sp m.(nextblock) m'.(nextblock) :: cs) + m'.(nextblock) tm'.(nextblock) m'. +Proof. + intros. + assert (SP: sp = nextblock tm). injection H2; auto. + unfold build_compilenv in H. + eapply match_callstack_alloc_variables_rec with (sz' := sz); eauto. + eapply valid_new_block; eauto. + rewrite (low_bound_alloc _ _ sp _ _ _ H2). apply zeq_true. + rewrite (high_bound_alloc _ _ sp _ _ _ H2). apply zeq_true. + (* match_callstack *) + constructor. omega. change (valid_block tm' sp). eapply valid_new_block; eauto. + constructor. + (* me_vars *) + intros. generalize (global_compilenv_charact id). + destruct (gce!!id); intro; try contradiction. + constructor. + unfold Csharpminor.empty_env. apply PTree.gempty. auto. + constructor. + unfold Csharpminor.empty_env. apply PTree.gempty. + (* me_low_high *) + omega. + (* me_bounded *) + intros until lv. unfold Csharpminor.empty_env. rewrite PTree.gempty. congruence. + (* me_inj *) + intros until lv2. unfold Csharpminor.empty_env; rewrite PTree.gempty; congruence. + (* me_inv *) + intros. exploit mi_mappedblocks; eauto. intros [A B]. + elim (fresh_block_alloc _ _ _ _ _ H2 A). + (* me_incr *) + intros. exploit mi_mappedblocks; eauto. intros [A B]. + rewrite SP; auto. + rewrite SP; auto. + eapply alloc_right_inject; eauto. + omega. + intros. exploit mi_mappedblocks; eauto. intros [A B]. + unfold block in SP; omegaContradiction. + (* defined *) + intros. unfold te. apply set_locals_params_defined. + unfold tparams, tvars. unfold fn_variables in H5. + change Csharpminor.fn_params with Csharpminor.fn_params in H5. + change Csharpminor.fn_vars with Csharpminor.fn_vars in H5. + elim (in_app_or _ _ _ H5); intros. + elim (list_in_map_inv _ _ _ H6). intros x [A B]. + apply in_or_app; left. inversion A. apply List.in_map. auto. + apply in_or_app; right. + change id with (fst (id, lv)). apply List.in_map; auto. +Qed. + +(** Characterization of the range of addresses for the blocks allocated + to hold Csharpminor local variables. *) + +Lemma alloc_variables_nextblock_incr: + forall e1 m1 vars e2 m2 lb, + alloc_variables e1 m1 vars e2 m2 lb -> + nextblock m1 <= nextblock m2. +Proof. + induction 1; intros. + omega. + inversion H; subst m1; simpl in IHalloc_variables. omega. +Qed. + +Lemma alloc_variables_list_block: + forall e1 m1 vars e2 m2 lb, + alloc_variables e1 m1 vars e2 m2 lb -> + forall b, m1.(nextblock) <= b < m2.(nextblock) <-> In b lb. +Proof. + induction 1; intros. + simpl; split; intro. omega. contradiction. + elim (IHalloc_variables b); intros A B. + assert (nextblock m = b1). injection H; intros. auto. + assert (nextblock m1 = Zsucc (nextblock m)). + injection H; intros; subst m1; reflexivity. + simpl; split; intro. + assert (nextblock m = b \/ nextblock m1 <= b < nextblock m2). + unfold block; rewrite H2; omega. + elim H4; intro. left; congruence. right; auto. + elim H3; intro. subst b b1. + generalize (alloc_variables_nextblock_incr _ _ _ _ _ _ H0). + rewrite H2. omega. + generalize (B H4). rewrite H2. omega. +Qed. + +(** Correctness of the code generated by [store_parameters] + to store in memory the values of parameters that are stack-allocated. *) + +Inductive vars_vals_match: + meminj -> list (ident * memory_chunk) -> list val -> env -> Prop := + | vars_vals_nil: + forall f te, + vars_vals_match f nil nil te + | vars_vals_cons: + forall f te id chunk vars v vals tv, + te!id = Some tv -> + val_inject f v tv -> + vars_vals_match f vars vals te -> + vars_vals_match f ((id, chunk) :: vars) (v :: vals) te. + +Lemma vars_vals_match_extensional: + forall f vars vals te, + vars_vals_match f vars vals te -> + forall te', + (forall id lv, In (id, lv) vars -> te'!id = te!id) -> + vars_vals_match f vars vals te'. +Proof. + induction 1; intros. + constructor. + econstructor; eauto. rewrite <- H. eapply H2. left. reflexivity. + apply IHvars_vals_match. intros. eapply H2; eauto. right. eauto. +Qed. + +Lemma store_parameters_correct: + forall e m1 params vl m2, + bind_parameters e m1 params vl m2 -> + forall f te1 cenv sp lo hi cs tm1, + vars_vals_match f params vl te1 -> + list_norepet (List.map (@fst ident memory_chunk) params) -> + mem_inject f m1 tm1 -> + match_callstack f (mkframe cenv e te1 sp lo hi :: cs) m1.(nextblock) tm1.(nextblock) m1 -> + exists te2, exists tm2, + exec_stmt tge (Vptr sp Int.zero) + te1 tm1 (store_parameters cenv params) + E0 te2 tm2 Out_normal + /\ mem_inject f m2 tm2 + /\ match_callstack f (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2. +Proof. + induction 1. + (* base case *) + intros; simpl. exists te1; exists tm1. split. constructor. tauto. + (* inductive case *) + intros until tm1. intros VVM NOREPET MINJ MATCH. simpl. + inversion VVM. subst f0 id0 chunk0 vars v vals te. + inversion MATCH. subst f0 cenv0 e0 te sp0 lo0 hi0 cs0 bound tbound m0. + inversion H18. + inversion NOREPET. subst hd tl. + assert (NEXT: nextblock m1 = nextblock m). + exploit store_inv; eauto. simpl; tauto. + generalize (me_vars0 id). intro. inversion H2; subst. + (* cenv!!id = Var_local chunk *) + assert (b0 = b). congruence. subst b0. + assert (chunk0 = chunk). congruence. subst chunk0. + assert (v' = tv). congruence. subst v'. + exploit make_cast_correct. + apply eval_Evar with (id := id). eauto. + eexact H10. + intros [tv' [EVAL1 VINJ1]]. + set (te2 := PTree.set id tv' te1). + assert (VVM2: vars_vals_match f params vl te2). + apply vars_vals_match_extensional with te1; auto. + intros. unfold te2; apply PTree.gso. red; intro; subst id0. + elim H4. change id with (fst (id, lv)). apply List.in_map; auto. + exploit store_unmapped_inject; eauto. intro MINJ2. + exploit match_callstack_store_local; eauto. + fold te2; rewrite <- NEXT; intro MATCH2. + exploit IHbind_parameters; eauto. + intros [te3 [tm3 [EXEC3 [MINJ3 MATCH3]]]]. + exists te3; exists tm3. + (* execution *) + split. apply exec_Sseq_continue with E0 te2 tm1 E0. + econstructor. unfold te2. constructor. eassumption. + assumption. traceEq. + (* meminj & match_callstack *) + tauto. + + (* cenv!!id = Var_stack_scalar *) + assert (b0 = b). congruence. subst b0. + assert (chunk0 = chunk). congruence. subst chunk0. + exploit make_store_correct. + eapply make_stackaddr_correct. + apply eval_Evar with (id := id). + eauto. 2:eauto. 2:eauto. unfold storev; eexact H0. eauto. + intros [tm2 [EVAL3 [MINJ2 NEXT1]]]. + exploit match_callstack_mapped. + eexact MATCH. 2:eauto. inversion H7. congruence. + rewrite <- NEXT; rewrite <- NEXT1; intro MATCH2. + exploit IHbind_parameters; eauto. + intros [te3 [tm3 [EVAL4 [MINJ3 MATCH3]]]]. + exists te3; exists tm3. + (* execution *) + split. apply exec_Sseq_continue with (E0**E0) te1 tm2 E0. + auto. assumption. traceEq. + (* meminj & match_callstack *) + tauto. + + (* Impossible cases on cenv!!id *) + congruence. + congruence. + congruence. +Qed. + +Lemma vars_vals_match_holds_1: + forall f params args targs, + list_norepet (List.map (@fst ident memory_chunk) params) -> + List.length params = List.length args -> + val_list_inject f args targs -> + vars_vals_match f params args + (set_params targs (List.map (@fst ident memory_chunk) params)). +Proof. + induction params; destruct args; simpl; intros; try discriminate. + constructor. + inversion H1. subst v0 vl targs. + inversion H. subst hd tl. + destruct a as [id chunk]. econstructor. + simpl. rewrite PTree.gss. reflexivity. + auto. + apply vars_vals_match_extensional + with (set_params vl' (map (@fst ident memory_chunk) params)). + eapply IHparams; eauto. + intros. simpl. apply PTree.gso. red; intro; subst id0. + elim H5. change (fst (id, chunk)) with (fst (id, lv)). + apply List.in_map; auto. +Qed. + +Lemma vars_vals_match_holds: + forall f params args targs, + List.length params = List.length args -> + val_list_inject f args targs -> + forall vars, + list_norepet (List.map (@fst ident var_kind) vars + ++ List.map (@fst ident memory_chunk) params) -> + vars_vals_match f params args + (set_locals (List.map (@fst ident var_kind) vars) + (set_params targs (List.map (@fst ident memory_chunk) params))). +Proof. + induction vars; simpl; intros. + eapply vars_vals_match_holds_1; eauto. + inversion H1. subst hd tl. + eapply vars_vals_match_extensional; eauto. + intros. apply PTree.gso. red; intro; subst id; elim H4. + apply in_or_app. right. change (fst a) with (fst (fst a, lv)). + apply List.in_map; auto. +Qed. + +Lemma bind_parameters_length: + forall e m1 params args m2, + bind_parameters e m1 params args m2 -> + List.length params = List.length args. +Proof. + induction 1; simpl; eauto. +Qed. + +(** The final result in this section: the behaviour of function entry + in the generated Cminor code (allocate stack data block and store + parameters whose address is taken) simulates what happens at function + entry in the original Csharpminor (allocate one block per local variable + and initialize the blocks corresponding to function parameters). *) + +Lemma function_entry_ok: + forall fn m e m1 lb vargs m2 f cs tm cenv sz tm1 sp tvargs, + alloc_variables empty_env m (fn_variables fn) e m1 lb -> + bind_parameters e m1 fn.(Csharpminor.fn_params) vargs m2 -> + match_callstack f cs m.(nextblock) tm.(nextblock) m -> + build_compilenv gce fn = (cenv, sz) -> + sz <= Int.max_signed -> + Mem.alloc tm 0 sz = (tm1, sp) -> + let te := + set_locals (fn_vars_names fn) (set_params tvargs (fn_params_names fn)) in + val_list_inject f vargs tvargs -> + mem_inject f m tm -> + list_norepet (fn_params_names fn ++ fn_vars_names fn) -> + exists f2, exists te2, exists tm2, + exec_stmt tge (Vptr sp Int.zero) + te tm1 (store_parameters cenv fn.(Csharpminor.fn_params)) + E0 te2 tm2 Out_normal + /\ mem_inject f2 m2 tm2 + /\ inject_incr f f2 + /\ match_callstack f2 + (mkframe cenv e te2 sp m.(nextblock) m1.(nextblock) :: cs) + m2.(nextblock) tm2.(nextblock) m2 + /\ (forall b, m.(nextblock) <= b < m1.(nextblock) <-> In b lb). +Proof. + intros. + exploit bind_parameters_length; eauto. intro LEN1. + exploit match_callstack_alloc_variables; eauto. + intros [f1 [INCR1 [MINJ1 MATCH1]]]. + exploit vars_vals_match_holds. + eauto. apply val_list_inject_incr with f. eauto. eauto. + apply list_norepet_append_commut. + unfold fn_vars_names in H7. eexact H7. + intro VVM. + exploit store_parameters_correct. + eauto. eauto. + unfold fn_params_names in H7. eapply list_norepet_append_left; eauto. + eexact MINJ1. eauto. + intros [te2 [tm2 [EXEC [MINJ2 MATCH2]]]]. + exists f1; exists te2; exists tm2. + split; auto. split; auto. split; auto. split; auto. + intros; eapply alloc_variables_list_block; eauto. +Qed. + +(** * Semantic preservation for the translation *) + +(** These tactics simplify hypotheses of the form [f ... = Some x]. *) + +Ltac monadSimpl1 := + match goal with + | [ |- (bind _ _ ?F ?G = Some ?X) -> _ ] => + unfold bind at 1; + generalize (refl_equal F); + pattern F at -1 in |- *; + case F; + [ (let EQ := fresh "EQ" in + (intro; intro EQ; + try monadSimpl1)) + | intros; discriminate ] + | [ |- (None = Some _) -> _ ] => + intro; discriminate + | [ |- (Some _ = Some _) -> _ ] => + let h := fresh "H" in + (intro h; injection h; intro; clear h) + end. + +Ltac monadSimpl := + match goal with + | [ |- (bind _ _ ?F ?G = Some ?X) -> _ ] => monadSimpl1 + | [ |- (None = Some _) -> _ ] => monadSimpl1 + | [ |- (Some _ = Some _) -> _ ] => monadSimpl1 + | [ |- (?F _ _ _ _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 + | [ |- (?F _ _ _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 + | [ |- (?F _ _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 + | [ |- (?F _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 + | [ |- (?F _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 + | [ |- (?F _ _ = Some _) -> _ ] => simpl F; monadSimpl1 + | [ |- (?F _ = Some _) -> _ ] => simpl F; monadSimpl1 + end. + +Ltac monadInv H := + generalize H; monadSimpl. + +(** The proof of semantic preservation uses simulation diagrams of the + following form: +<< + le, e, m1, a --------------- tle, sp, te1, tm1, ta + | | + | | + v v + le, e, m2, v --------------- tle, sp, te2, tm2, tv +>> + where [ta] is the Cminor expression obtained by translating the + Csharpminor expression [a]. The left vertical arrow is an evaluation + of a Csharpminor expression. The right vertical arrow is an evaluation + of a Cminor expression. The precondition (top vertical bar) + includes a [mem_inject] relation between the memory states [m1] and [tm1], + a [val_list_inject] relation between the let environments [le] and [tle], + and a [match_callstack] relation for any callstack having + [e], [te1], [sp] as top frame. The postcondition (bottom vertical bar) + is the existence of a memory injection [f2] that extends the injection + [f1] we started with, preserves the [match_callstack] relation for + the transformed callstack at the final state, and validates a + [val_inject] relation between the result values [v] and [tv]. + + We capture these diagrams by the following predicates, parameterized + over the Csharpminor executions, which will serve as induction + hypotheses in the proof of simulation. *) + +Definition eval_expr_prop + (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (a: Csharpminor.expr) (t: trace) (m2: mem) (v: val) : Prop := + forall cenv ta f1 tle te1 tm1 sp lo hi cs + (TR: transl_expr cenv a = Some ta) + (LINJ: val_list_inject f1 le tle) + (MINJ: mem_inject f1 m1 tm1) + (MATCH: match_callstack f1 + (mkframe cenv e te1 sp lo hi :: cs) + m1.(nextblock) tm1.(nextblock) m1), + exists f2, exists te2, exists tm2, exists tv, + eval_expr tge (Vptr sp Int.zero) tle te1 tm1 ta t te2 tm2 tv + /\ val_inject f2 v tv + /\ mem_inject f2 m2 tm2 + /\ inject_incr f1 f2 + /\ match_callstack f2 + (mkframe cenv e te2 sp lo hi :: cs) + m2.(nextblock) tm2.(nextblock) m2. + +Definition eval_exprlist_prop + (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (al: Csharpminor.exprlist) (t: trace) (m2: mem) (vl: list val) : Prop := + forall cenv tal f1 tle te1 tm1 sp lo hi cs + (TR: transl_exprlist cenv al = Some tal) + (LINJ: val_list_inject f1 le tle) + (MINJ: mem_inject f1 m1 tm1) + (MATCH: match_callstack f1 + (mkframe cenv e te1 sp lo hi :: cs) + m1.(nextblock) tm1.(nextblock) m1), + exists f2, exists te2, exists tm2, exists tvl, + eval_exprlist tge (Vptr sp Int.zero) tle te1 tm1 tal t te2 tm2 tvl + /\ val_list_inject f2 vl tvl + /\ mem_inject f2 m2 tm2 + /\ inject_incr f1 f2 + /\ match_callstack f2 + (mkframe cenv e te2 sp lo hi :: cs) + m2.(nextblock) tm2.(nextblock) m2. + +Definition eval_funcall_prop + (m1: mem) (fn: Csharpminor.fundef) (args: list val) (t: trace) (m2: mem) (res: val) : Prop := + forall tfn f1 tm1 cs targs + (TR: transl_fundef gce fn = Some tfn) + (MINJ: mem_inject f1 m1 tm1) + (MATCH: match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1) + (ARGSINJ: val_list_inject f1 args targs), + exists f2, exists tm2, exists tres, + eval_funcall tge tm1 tfn targs t tm2 tres + /\ val_inject f2 res tres + /\ mem_inject f2 m2 tm2 + /\ inject_incr f1 f2 + /\ match_callstack f2 cs m2.(nextblock) tm2.(nextblock) m2. + +Inductive outcome_inject (f: meminj) : Csharpminor.outcome -> outcome -> Prop := + | outcome_inject_normal: + outcome_inject f Csharpminor.Out_normal Out_normal + | outcome_inject_exit: + forall n, outcome_inject f (Csharpminor.Out_exit n) (Out_exit n) + | outcome_inject_return_none: + outcome_inject f (Csharpminor.Out_return None) (Out_return None) + | outcome_inject_return_some: + forall v1 v2, + val_inject f v1 v2 -> + outcome_inject f (Csharpminor.Out_return (Some v1)) (Out_return (Some v2)). + +Definition exec_stmt_prop + (e: Csharpminor.env) (m1: mem) (s: Csharpminor.stmt) (t: trace) (m2: mem) (out: Csharpminor.outcome): Prop := + forall cenv ts f1 te1 tm1 sp lo hi cs + (TR: transl_stmt cenv s = Some ts) + (MINJ: mem_inject f1 m1 tm1) + (MATCH: match_callstack f1 + (mkframe cenv e te1 sp lo hi :: cs) + m1.(nextblock) tm1.(nextblock) m1), + exists f2, exists te2, exists tm2, exists tout, + exec_stmt tge (Vptr sp Int.zero) te1 tm1 ts t te2 tm2 tout + /\ outcome_inject f2 out tout + /\ mem_inject f2 m2 tm2 + /\ inject_incr f1 f2 + /\ match_callstack f2 + (mkframe cenv e te2 sp lo hi :: cs) + m2.(nextblock) tm2.(nextblock) m2. + +(** There are as many cases in the inductive proof as there are evaluation + rules in the Csharpminor semantics. We treat each case as a separate + lemma. *) + +Lemma transl_expr_Evar_correct: + forall (le : Csharpminor.letenv) + (e : Csharpminor.env) (m : mem) (id : positive) + (b : block) (chunk : memory_chunk) (v : val), + eval_var_ref prog e id b chunk -> + load chunk m b 0 = Some v -> + eval_expr_prop le e m (Csharpminor.Evar id) E0 m v. +Proof. + intros; red; intros. unfold transl_expr in TR. + exploit var_get_correct; eauto. + intros [tv [EVAL VINJ]]. + exists f1; exists te1; exists tm1; exists tv; intuition eauto. +Qed. + +Lemma transl_expr_Eaddrof_correct: + forall (le : Csharpminor.letenv) + (e : Csharpminor.env) (m : mem) (id : positive) + (b : block), + eval_var_addr prog e id b -> + eval_expr_prop le e m (Eaddrof id) E0 m (Vptr b Int.zero). +Proof. + intros; red; intros. simpl in TR. + exploit var_addr_correct; eauto. + intros [tv [EVAL VINJ]]. + exists f1; exists te1; exists tm1; exists tv. intuition eauto. +Qed. + +Lemma transl_expr_Eop_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (op : Csharpminor.operation) (al : Csharpminor.exprlist) + (t: trace) (m1 : mem) (vl : list val) (v : val), + Csharpminor.eval_exprlist prog le e m al t m1 vl -> + eval_exprlist_prop le e m al t m1 vl -> + Csharpminor.eval_operation op vl m1 = Some v -> + eval_expr_prop le e m (Csharpminor.Eop op al) t m1 v. +Proof. + intros; red; intros. monadInv TR; intro EQ0. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tvl [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. + exploit make_op_correct; eauto. + intros [tv [EVAL2 VINJ2]]. + exists f2; exists te2; exists tm2; exists tv. intuition. +Qed. + +Lemma transl_expr_Eload_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (chunk : memory_chunk) (a : Csharpminor.expr) (t: trace) (m1 : mem) + (v1 v : val), + Csharpminor.eval_expr prog le e m a t m1 v1 -> + eval_expr_prop le e m a t m1 v1 -> + loadv chunk m1 v1 = Some v -> + eval_expr_prop le e m (Csharpminor.Eload chunk a) t m1 v. +Proof. + intros; red; intros. + monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]]. + exploit loadv_inject; eauto. + intros [tv [TLOAD VINJ]]. + exists f2; exists te2; exists tm2; exists tv. + intuition. + subst ta. eapply make_load_correct; eauto. +Qed. + +Lemma transl_expr_Ecall_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (sig : signature) (a : Csharpminor.expr) (bl : Csharpminor.exprlist) + (t1: trace) (m1: mem) (t2: trace) (m2: mem) (t3: trace) (m3: mem) + (vf : val) (vargs : list val) (vres : val) + (f : Csharpminor.fundef) (t: trace), + Csharpminor.eval_expr prog le e m a t1 m1 vf -> + eval_expr_prop le e m a t1 m1 vf -> + Csharpminor.eval_exprlist prog le e m1 bl t2 m2 vargs -> + eval_exprlist_prop le e m1 bl t2 m2 vargs -> + Genv.find_funct ge vf = Some f -> + Csharpminor.funsig f = sig -> + Csharpminor.eval_funcall prog m2 f vargs t3 m3 vres -> + eval_funcall_prop m2 f vargs t3 m3 vres -> + t = t1 ** t2 ** t3 -> + eval_expr_prop le e m (Csharpminor.Ecall sig a bl) t m3 vres. +Proof. + intros;red;intros. monadInv TR. subst ta. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. + exploit H2. + eauto. eapply val_list_inject_incr; eauto. eauto. eauto. + intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]]. + assert (tv1 = vf). + elim (Genv.find_funct_inv H3). intros bf VF. rewrite VF in H3. + rewrite Genv.find_funct_find_funct_ptr in H3. + generalize (Genv.find_funct_ptr_inv H3). intro. + assert (match_globalenvs f2). eapply match_callstack_match_globalenvs; eauto. + generalize (mg_functions _ H9 _ H8). intro. + rewrite VF in VINJ1. inversion VINJ1. subst vf. + decEq. congruence. + subst ofs2. replace x with 0. reflexivity. congruence. + subst tv1. elim (functions_translated _ _ H3). intros tf [FIND TRF]. + exploit H6; eauto. + intros [f4 [tm4 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]]. + exists f4; exists te3; exists tm4; exists tres. intuition. + eapply eval_Ecall; eauto. + rewrite <- H4. apply sig_preserved; auto. + apply inject_incr_trans with f2; auto. + apply inject_incr_trans with f3; auto. +Qed. + +Lemma transl_expr_Econdition_true_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (a b c : Csharpminor.expr) (t1: trace) (m1 : mem) (v1 : val) + (t2: trace) (m2 : mem) (v2 : val) (t: trace), + Csharpminor.eval_expr prog le e m a t1 m1 v1 -> + eval_expr_prop le e m a t1 m1 v1 -> + Val.is_true v1 -> + Csharpminor.eval_expr prog le e m1 b t2 m2 v2 -> + eval_expr_prop le e m1 b t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr_prop le e m (Csharpminor.Econdition a b c) t m2 v2. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. + exploit H3. + eauto. eapply val_list_inject_incr; eauto. eauto. eauto. + intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exists f3; exists te3; exists tm3; exists tv2. + intuition. + rewrite <- H6. subst t; eapply eval_conditionalexpr_true; eauto. + inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto. + eapply inject_incr_trans; eauto. +Qed. + +Lemma transl_expr_Econdition_false_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (a b c : Csharpminor.expr) (t1: trace) (m1 : mem) (v1 : val) + (t2: trace) (m2 : mem) (v2 : val) (t: trace), + Csharpminor.eval_expr prog le e m a t1 m1 v1 -> + eval_expr_prop le e m a t1 m1 v1 -> + Val.is_false v1 -> + Csharpminor.eval_expr prog le e m1 c t2 m2 v2 -> + eval_expr_prop le e m1 c t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr_prop le e m (Csharpminor.Econdition a b c) t m2 v2. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. + exploit H3. + eauto. eapply val_list_inject_incr; eauto. eauto. eauto. + intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exists f3; exists te3; exists tm3; exists tv2. + intuition. + rewrite <- H6. subst t; eapply eval_conditionalexpr_false; eauto. + inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto. + eapply inject_incr_trans; eauto. +Qed. + +Lemma transl_expr_Elet_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (a b : Csharpminor.expr) (t1: trace) (m1 : mem) (v1 : val) + (t2: trace) (m2 : mem) (v2 : val) (t: trace), + Csharpminor.eval_expr prog le e m a t1 m1 v1 -> + eval_expr_prop le e m a t1 m1 v1 -> + Csharpminor.eval_expr prog (v1 :: le) e m1 b t2 m2 v2 -> + eval_expr_prop (v1 :: le) e m1 b t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr_prop le e m (Csharpminor.Elet a b) t m2 v2. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. + exploit H2. + eauto. + constructor. eauto. eapply val_list_inject_incr; eauto. + eauto. eauto. + intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exists f3; exists te3; exists tm3; exists tv2. + intuition. + subst ta; eapply eval_Elet; eauto. + eapply inject_incr_trans; eauto. +Qed. + +Remark val_list_inject_nth: + forall f l1 l2, val_list_inject f l1 l2 -> + forall n v1, nth_error l1 n = Some v1 -> + exists v2, nth_error l2 n = Some v2 /\ val_inject f v1 v2. +Proof. + induction 1; destruct n; simpl; intros. + discriminate. discriminate. + injection H1; intros; subst v. exists v'; split; auto. + eauto. +Qed. + +Lemma transl_expr_Eletvar_correct: + forall (le : list val) (e : Csharpminor.env) (m : mem) (n : nat) + (v : val), + nth_error le n = Some v -> + eval_expr_prop le e m (Csharpminor.Eletvar n) E0 m v. +Proof. + intros; red; intros. monadInv TR. + exploit val_list_inject_nth; eauto. intros [tv [A B]]. + exists f1; exists te1; exists tm1; exists tv. + intuition. + subst ta. eapply eval_Eletvar; auto. +Qed. + +Lemma transl_expr_Ealloc_correct: + forall (le: list val) (e: Csharpminor.env) (m1: mem) (a: Csharpminor.expr) + (t: trace) (m2: mem) (n: int) (m3: mem) (b: block), + Csharpminor.eval_expr prog le e m1 a t m2 (Vint n) -> + eval_expr_prop le e m1 a t m2 (Vint n) -> + Mem.alloc m2 0 (Int.signed n) = (m3, b) -> + eval_expr_prop le e m1 (Csharpminor.Ealloc a) t m3 (Vptr b Int.zero). +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + inversion VINJ1. subst tv1 i. + caseEq (alloc tm2 0 (Int.signed n)). intros tm3 tb TALLOC. + assert (LB: Int.min_signed <= 0). compute. congruence. + assert (HB: Int.signed n <= Int.max_signed). + generalize (Int.signed_range n); omega. + exploit alloc_parallel_inject; eauto. + intros [MINJ3 INCR3]. + exists (extend_inject b (Some (tb, 0)) f2); + exists te2; exists tm3; exists (Vptr tb Int.zero). + split. subst ta; econstructor; eauto. + split. econstructor. unfold extend_inject, eq_block. rewrite zeq_true. reflexivity. + reflexivity. + split. assumption. + split. eapply inject_incr_trans; eauto. + eapply match_callstack_alloc; eauto. +Qed. + +Lemma transl_exprlist_Enil_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem), + eval_exprlist_prop le e m Csharpminor.Enil E0 m nil. +Proof. + intros; red; intros. monadInv TR. + exists f1; exists te1; exists tm1; exists (@nil val). + intuition. subst tal; constructor. +Qed. + +Lemma transl_exprlist_Econs_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (a : Csharpminor.expr) (bl : Csharpminor.exprlist) + (t1: trace) (m1 : mem) (v : val) + (t2: trace) (m2 : mem) (vl : list val) (t: trace), + Csharpminor.eval_expr prog le e m a t1 m1 v -> + eval_expr_prop le e m a t1 m1 v -> + Csharpminor.eval_exprlist prog le e m1 bl t2 m2 vl -> + eval_exprlist_prop le e m1 bl t2 m2 vl -> + t = t1 ** t2 -> + eval_exprlist_prop le e m (Csharpminor.Econs a bl) t m2 (v :: vl). +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exploit H2. + eauto. eapply val_list_inject_incr; eauto. eauto. eauto. + intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. + exists f3; exists te3; exists tm3; exists (tv1 :: tv2). + intuition. subst tal; econstructor; eauto. + constructor. eapply val_inject_incr; eauto. auto. + eapply inject_incr_trans; eauto. +Qed. + +Lemma transl_funcall_internal_correct: + forall (m : mem) (f : Csharpminor.function) (vargs : list val) + (e : Csharpminor.env) (m1 : mem) (lb : list block) (m2: mem) + (t: trace) (m3 : mem) (out : Csharpminor.outcome) (vres : val), + list_norepet (fn_params_names f ++ fn_vars_names f) -> + alloc_variables empty_env m (fn_variables f) e m1 lb -> + bind_parameters e m1 (Csharpminor.fn_params f) vargs m2 -> + Csharpminor.exec_stmt prog e m2 (Csharpminor.fn_body f) t m3 out -> + exec_stmt_prop e m2 (Csharpminor.fn_body f) t m3 out -> + Csharpminor.outcome_result_value out (sig_res (Csharpminor.fn_sig f)) vres -> + eval_funcall_prop m (Internal f) vargs t (free_list m3 lb) vres. +Proof. + intros; red. intros tfn f1 tm; intros. + generalize TR; clear TR. + unfold transl_fundef, transf_partial_fundef. + caseEq (transl_function gce f); try congruence. + intros tf TR EQ. inversion EQ; clear EQ; subst tfn. + unfold transl_function in TR. + caseEq (build_compilenv gce f); intros cenv stacksize CENV. + rewrite CENV in TR. + destruct (zle stacksize Int.max_signed); try discriminate. + monadInv TR. clear TR. + caseEq (alloc tm 0 stacksize). intros tm1 sp ALLOC. + exploit function_entry_ok; eauto. + intros [f2 [te2 [tm2 [STOREPARAM [MINJ2 [INCR12 [MATCH2 BLOCKS]]]]]]]. + red in H3; exploit H3; eauto. + intros [f3 [te3 [tm3 [tout [EXECBODY [OUTINJ [MINJ3 [INCR23 MATCH3]]]]]]]]. + assert (exists tvres, + outcome_result_value tout f.(Csharpminor.fn_sig).(sig_res) tvres /\ + val_inject f3 vres tvres). + generalize H4. unfold Csharpminor.outcome_result_value, outcome_result_value. + inversion OUTINJ. + destruct (sig_res (Csharpminor.fn_sig f)); intro. contradiction. + exists Vundef; split. auto. subst vres; constructor. + tauto. + destruct (sig_res (Csharpminor.fn_sig f)); intro. contradiction. + exists Vundef; split. auto. subst vres; constructor. + destruct (sig_res (Csharpminor.fn_sig f)); intro. + exists v2; split. auto. subst vres; auto. + contradiction. + destruct H5 as [tvres [TOUT VINJRES]]. + exists f3; exists (Mem.free tm3 sp); exists tvres. + (* execution *) + split. rewrite <- H6; econstructor; simpl; eauto. + apply exec_Sseq_continue with E0 te2 tm2 t. + exact STOREPARAM. + eexact EXECBODY. + traceEq. + (* val_inject *) + split. assumption. + (* mem_inject *) + split. apply free_inject; auto. + intros. elim (BLOCKS b1); intros B1 B2. apply B1. inversion MATCH3. inversion H20. + eapply me_inv0. eauto. + (* inject_incr *) + split. eapply inject_incr_trans; eauto. + (* match_callstack *) + assert (forall bl mm, nextblock (free_list mm bl) = nextblock mm). + induction bl; intros. reflexivity. simpl. auto. + unfold free; simpl nextblock. rewrite H5. + eapply match_callstack_freelist; eauto. + intros. elim (BLOCKS b); intros B1 B2. generalize (B2 H7). omega. +Qed. + +Lemma transl_funcall_external_correct: + forall (m : mem) (ef : external_function) (vargs : list val) + (t : trace) (vres : val), + event_match ef vargs t vres -> + eval_funcall_prop m (External ef) vargs t m vres. +Proof. + intros; red; intros. + simpl in TR. inversion TR; clear TR; subst tfn. + exploit event_match_inject; eauto. intros [A B]. + exists f1; exists tm1; exists vres; intuition. + constructor; auto. +Qed. + +Lemma transl_stmt_Sskip_correct: + forall (e : Csharpminor.env) (m : mem), + exec_stmt_prop e m Csharpminor.Sskip E0 m Csharpminor.Out_normal. +Proof. + intros; red; intros. monadInv TR. + exists f1; exists te1; exists tm1; exists Out_normal. + intuition. subst ts; constructor. constructor. +Qed. + +Lemma transl_stmt_Sexpr_correct: + forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) + (t: trace) (m1 : mem) (v : val), + Csharpminor.eval_expr prog nil e m a t m1 v -> + eval_expr_prop nil e m a t m1 v -> + exec_stmt_prop e m (Csharpminor.Sexpr a) t m1 Csharpminor.Out_normal. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exists f2; exists te2; exists tm2; exists Out_normal. + intuition. subst ts. econstructor; eauto. + constructor. +Qed. + +Lemma transl_stmt_Sassign_correct: + forall (e : Csharpminor.env) (m : mem) + (id : ident) (a : Csharpminor.expr) (t: trace) (m1 : mem) (b : block) + (chunk : memory_chunk) (v : val) (m2 : mem), + Csharpminor.eval_expr prog nil e m a t m1 v -> + eval_expr_prop nil e m a t m1 v -> + eval_var_ref prog e id b chunk -> + store chunk m1 b 0 v = Some m2 -> + exec_stmt_prop e m (Csharpminor.Sassign id a) t m2 Csharpminor.Out_normal. +Proof. + intros; red; intros. monadInv TR; intro EQ0. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR12 MATCH1]]]]]]]]. + exploit var_set_correct; eauto. + intros [te3 [tm3 [EVAL2 [MINJ2 MATCH2]]]]. + exists f2; exists te3; exists tm3; exists Out_normal. + intuition. constructor. +Qed. + +Lemma transl_stmt_Sstore_correct: + forall (e : Csharpminor.env) (m : mem) + (chunk : memory_chunk) (a b : Csharpminor.expr) (t1: trace) (m1 : mem) + (v1 : val) (t2: trace) (m2 : mem) (v2 : val) + (t3: trace) (m3 : mem), + Csharpminor.eval_expr prog nil e m a t1 m1 v1 -> + eval_expr_prop nil e m a t1 m1 v1 -> + Csharpminor.eval_expr prog nil e m1 b t2 m2 v2 -> + eval_expr_prop nil e m1 b t2 m2 v2 -> + storev chunk m2 v1 v2 = Some m3 -> + t3 = t1 ** t2 -> + exec_stmt_prop e m (Csharpminor.Sstore chunk a b) t3 m3 Csharpminor.Out_normal. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exploit H2. + eauto. + eapply val_list_inject_incr; eauto. + eauto. eauto. + intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. + exploit make_store_correct. + eexact EVAL1. eexact EVAL2. eauto. eauto. + eapply val_inject_incr; eauto. eauto. + intros [tm4 [EVAL [MINJ4 NEXTBLOCK]]]. + exists f3; exists te3; exists tm4; exists Out_normal. + rewrite <- H6. subst t3. intuition. + constructor. + eapply inject_incr_trans; eauto. + assert (val_inject f3 v1 tv1). eapply val_inject_incr; eauto. + unfold storev in H3; destruct v1; try discriminate. + inversion H4. + rewrite NEXTBLOCK. replace (nextblock m3) with (nextblock m2). + eapply match_callstack_mapped; eauto. congruence. + exploit store_inv; eauto. simpl; symmetry; tauto. +Qed. + +Lemma transl_stmt_Sseq_continue_correct: + forall (e : Csharpminor.env) (m : mem) (s1 s2 : Csharpminor.stmt) + (t1 t2: trace) (m1 m2 : mem) (t: trace) (out : Csharpminor.outcome), + Csharpminor.exec_stmt prog e m s1 t1 m1 Csharpminor.Out_normal -> + exec_stmt_prop e m s1 t1 m1 Csharpminor.Out_normal -> + Csharpminor.exec_stmt prog e m1 s2 t2 m2 out -> + exec_stmt_prop e m1 s2 t2 m2 out -> + t = t1 ** t2 -> + exec_stmt_prop e m (Csharpminor.Sseq s1 s2) t m2 out. +Proof. + intros; red; intros; monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exploit H2; eauto. + intros [f3 [te3 [tm3 [tout2 [EXEC2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. + exists f3; exists te3; exists tm3; exists tout2. + intuition. subst ts; eapply exec_Sseq_continue; eauto. + inversion OINJ1. subst tout1. auto. + eapply inject_incr_trans; eauto. +Qed. + +Lemma transl_stmt_Sseq_stop_correct: + forall (e : Csharpminor.env) (m : mem) (s1 s2 : Csharpminor.stmt) + (t1: trace) (m1 : mem) (out : Csharpminor.outcome), + Csharpminor.exec_stmt prog e m s1 t1 m1 out -> + exec_stmt_prop e m s1 t1 m1 out -> + out <> Csharpminor.Out_normal -> + exec_stmt_prop e m (Csharpminor.Sseq s1 s2) t1 m1 out. +Proof. + intros; red; intros; monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exists f2; exists te2; exists tm2; exists tout1. + intuition. subst ts; eapply exec_Sseq_stop; eauto. + inversion OINJ1; subst out tout1; congruence. +Qed. + +Lemma transl_stmt_Sifthenelse_true_correct: + forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) + (sl1 sl2 : Csharpminor.stmt) + (t1: trace) (m1 : mem) (v1 : val) (t2: trace) (m2 : mem) + (out : Csharpminor.outcome) (t: trace), + Csharpminor.eval_expr prog nil e m a t1 m1 v1 -> + eval_expr_prop nil e m a t1 m1 v1 -> + Val.is_true v1 -> + Csharpminor.exec_stmt prog e m1 sl1 t2 m2 out -> + exec_stmt_prop e m1 sl1 t2 m2 out -> + t = t1 ** t2 -> + exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) t m2 out. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exploit H3; eauto. + intros [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]]. + exists f3; exists te3; exists tm3; exists tout. + intuition. + subst ts t. eapply exec_ifthenelse_true; eauto. + inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto. + eapply inject_incr_trans; eauto. +Qed. + +Lemma transl_stmt_Sifthenelse_false_correct: + forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) + (sl1 sl2 : Csharpminor.stmt) + (t1: trace) (m1 : mem) (v1 : val) (t2: trace) (m2 : mem) + (out : Csharpminor.outcome) (t: trace), + Csharpminor.eval_expr prog nil e m a t1 m1 v1 -> + eval_expr_prop nil e m a t1 m1 v1 -> + Val.is_false v1 -> + Csharpminor.exec_stmt prog e m1 sl2 t2 m2 out -> + exec_stmt_prop e m1 sl2 t2 m2 out -> + t = t1 ** t2 -> + exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) t m2 out. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exploit H3; eauto. + intros [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]]. + exists f3; exists te3; exists tm3; exists tout. + intuition. + subst ts t. eapply exec_ifthenelse_false; eauto. + inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto. + eapply inject_incr_trans; eauto. +Qed. + +Lemma transl_stmt_Sloop_loop_correct: + forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) + (t1: trace) (m1: mem) (t2: trace) (m2 : mem) + (out : Csharpminor.outcome) (t: trace), + Csharpminor.exec_stmt prog e m sl t1 m1 Csharpminor.Out_normal -> + exec_stmt_prop e m sl t1 m1 Csharpminor.Out_normal -> + Csharpminor.exec_stmt prog e m1 (Csharpminor.Sloop sl) t2 m2 out -> + exec_stmt_prop e m1 (Csharpminor.Sloop sl) t2 m2 out -> + t = t1 ** t2 -> + exec_stmt_prop e m (Csharpminor.Sloop sl) t m2 out. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exploit H2; eauto. + intros [f3 [te3 [tm3 [tout2 [EVAL2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. + exists f3; exists te3; exists tm3; exists tout2. + intuition. + subst ts. eapply exec_Sloop_loop; eauto. + inversion OINJ1; subst tout1; eauto. + eapply inject_incr_trans; eauto. +Qed. + +Lemma transl_stmt_Sloop_exit_correct: + forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) + (t1: trace) (m1 : mem) (out : Csharpminor.outcome), + Csharpminor.exec_stmt prog e m sl t1 m1 out -> + exec_stmt_prop e m sl t1 m1 out -> + out <> Csharpminor.Out_normal -> + exec_stmt_prop e m (Csharpminor.Sloop sl) t1 m1 out. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exists f2; exists te2; exists tm2; exists tout1. + intuition. subst ts; eapply exec_Sloop_stop; eauto. + inversion OINJ1; subst out tout1; congruence. +Qed. + +Lemma transl_stmt_Sblock_correct: + forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) + (t1: trace) (m1 : mem) (out : Csharpminor.outcome), + Csharpminor.exec_stmt prog e m sl t1 m1 out -> + exec_stmt_prop e m sl t1 m1 out -> + exec_stmt_prop e m (Csharpminor.Sblock sl) t1 m1 + (Csharpminor.outcome_block out). +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exists f2; exists te2; exists tm2; exists (outcome_block tout1). + intuition. subst ts; eapply exec_Sblock; eauto. + inversion OINJ1; subst out tout1; simpl. + constructor. + destruct n; constructor. + constructor. + constructor; auto. +Qed. + +Lemma transl_stmt_Sexit_correct: + forall (e : Csharpminor.env) (m : mem) (n : nat), + exec_stmt_prop e m (Csharpminor.Sexit n) E0 m (Csharpminor.Out_exit n). +Proof. + intros; red; intros. monadInv TR. + exists f1; exists te1; exists tm1; exists (Out_exit n). + intuition. subst ts; constructor. constructor. +Qed. + +Lemma transl_stmt_Sswitch_correct: + forall (e : Csharpminor.env) (m : mem) + (a : Csharpminor.expr) (cases : list (int * nat)) (default : nat) + (t1 : trace) (m1 : mem) (n : int), + Csharpminor.eval_expr prog nil e m a t1 m1 (Vint n) -> + eval_expr_prop nil e m a t1 m1 (Vint n) -> + exec_stmt_prop e m (Csharpminor.Sswitch a cases default) t1 m1 + (Csharpminor.Out_exit (Csharpminor.switch_target n default cases)). +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]]. + exists f2; exists te2; exists tm2; + exists (Out_exit (switch_target n default cases)). intuition. + subst ts. constructor. inversion VINJ1. subst tv1. assumption. + constructor. +Qed. + +Lemma transl_stmt_Sreturn_none_correct: + forall (e : Csharpminor.env) (m : mem), + exec_stmt_prop e m (Csharpminor.Sreturn None) E0 m + (Csharpminor.Out_return None). +Proof. + intros; red; intros. monadInv TR. + exists f1; exists te1; exists tm1; exists (Out_return None). + intuition. subst ts; constructor. constructor. +Qed. + +Lemma transl_stmt_Sreturn_some_correct: + forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) + (t1: trace) (m1 : mem) (v : val), + Csharpminor.eval_expr prog nil e m a t1 m1 v -> + eval_expr_prop nil e m a t1 m1 v -> + exec_stmt_prop e m (Csharpminor.Sreturn (Some a)) t1 m1 + (Csharpminor.Out_return (Some v)). +Proof. + intros; red; intros; monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]]. + exists f2; exists te2; exists tm2; exists (Out_return (Some tv1)). + intuition. subst ts; econstructor; eauto. constructor; auto. +Qed. + +(** We conclude by an induction over the structure of the Csharpminor + evaluation derivation, using the lemmas above for each case. *) + +Lemma transl_function_correct: + forall m1 f vargs t m2 vres, + Csharpminor.eval_funcall prog m1 f vargs t m2 vres -> + eval_funcall_prop m1 f vargs t m2 vres. +Proof + (eval_funcall_ind4 prog + eval_expr_prop + eval_exprlist_prop + eval_funcall_prop + exec_stmt_prop + + transl_expr_Evar_correct + transl_expr_Eaddrof_correct + transl_expr_Eop_correct + transl_expr_Eload_correct + transl_expr_Ecall_correct + transl_expr_Econdition_true_correct + transl_expr_Econdition_false_correct + transl_expr_Elet_correct + transl_expr_Eletvar_correct + transl_expr_Ealloc_correct + transl_exprlist_Enil_correct + transl_exprlist_Econs_correct + transl_funcall_internal_correct + transl_funcall_external_correct + transl_stmt_Sskip_correct + transl_stmt_Sexpr_correct + transl_stmt_Sassign_correct + transl_stmt_Sstore_correct + transl_stmt_Sseq_continue_correct + transl_stmt_Sseq_stop_correct + transl_stmt_Sifthenelse_true_correct + transl_stmt_Sifthenelse_false_correct + transl_stmt_Sloop_loop_correct + transl_stmt_Sloop_exit_correct + transl_stmt_Sblock_correct + transl_stmt_Sexit_correct + transl_stmt_Sswitch_correct + transl_stmt_Sreturn_none_correct + transl_stmt_Sreturn_some_correct). + +(** The [match_globalenvs] relation holds for the global environments + of the source program and the transformed program. *) + +Lemma match_globalenvs_init: + let m := Genv.init_mem (program_of_program prog) in + let tm := Genv.init_mem tprog in + let f := fun b => if zlt b m.(nextblock) then Some(b, 0) else None in + match_globalenvs f. +Proof. + intros. constructor. + (* globalvars *) + (* symbols *) + intros. split. + unfold f. rewrite zlt_true. auto. unfold m. + eapply Genv.find_symbol_inv; eauto. + rewrite <- H. apply symbols_preserved. + intros. unfold f. rewrite zlt_true. auto. + generalize (nextblock_pos m). omega. +Qed. + +(** The correctness of the translation of a whole Csharpminor program + follows. *) + +Theorem transl_program_correct: + forall t n, + Csharpminor.exec_program prog t (Vint n) -> + exec_program tprog t (Vint n). +Proof. + intros t n [b [fn [m [FINDS [FINDF [SIG EVAL]]]]]]. + elim (function_ptr_translated _ _ FINDF). intros tfn [TFIND TR]. + set (m0 := Genv.init_mem (program_of_program prog)) in *. + set (f := fun b => if zlt b m0.(nextblock) then Some(b, 0) else None). + assert (MINJ0: mem_inject f m0 m0). + unfold f; constructor; intros. + apply zlt_false; auto. + destruct (zlt b0 (nextblock m0)); try discriminate. + inversion H; subst b' delta. + split. auto. + constructor. compute. split; congruence. left; auto. + intros; omega. + generalize (Genv.initmem_block_init (program_of_program prog) b0). fold m0. intros [idata EQ]. + rewrite EQ. simpl. apply Mem.contents_init_data_inject. + destruct (zlt b1 (nextblock m0)); try discriminate. + destruct (zlt b2 (nextblock m0)); try discriminate. + left; congruence. + assert (MATCH0: match_callstack f nil m0.(nextblock) m0.(nextblock) m0). + constructor. unfold f; apply match_globalenvs_init. + fold ge in EVAL. + exploit transl_function_correct; eauto. + intros [f1 [tm1 [tres [TEVAL [VINJ [MINJ1 [INCR MATCH1]]]]]]]. + exists b; exists tfn; exists tm1. + split. fold tge. rewrite <- FINDS. + replace (prog_main prog) with (AST.prog_main tprog). fold ge. apply symbols_preserved. + transitivity (AST.prog_main (program_of_program prog)). + apply transform_partial_program_main with (transl_fundef gce). assumption. + reflexivity. + split. assumption. + split. rewrite <- SIG. apply sig_preserved; auto. + rewrite (Genv.init_mem_transf_partial (transl_fundef gce) _ TRANSL). + inversion VINJ; subst tres. assumption. +Qed. + +End TRANSLATION. diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v new file mode 100644 index 00000000..246ebf53 --- /dev/null +++ b/cfrontend/Csharpminor.v @@ -0,0 +1,563 @@ +(** Abstract syntax and semantics for the Csharpminor language. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Events. +Require Import Globalenvs. + +(** Abstract syntax *) + +(** Csharpminor is a low-level imperative language structured in expressions, + statements, functions and programs. Expressions include + reading global or local variables, reading store locations, + arithmetic operations, function calls, and conditional expressions + (similar to [e1 ? e2 : e3] in C). The [Elet] and [Eletvar] constructs + enable sharing the computations of subexpressions. De Bruijn notation + is used: [Eletvar n] refers to the value bound by then [n+1]-th enclosing + [Elet] construct. + + Unlike in Cminor (the next intermediate language of the back-end), + Csharpminor local variables reside in memory, and their address can + be taken using [Eaddrof] expressions. + + Another difference with Cminor is that Csharpminor is entirely + processor-neutral. In particular, Csharpminor uses a standard set of + operations: it does not reflect processor-specific operations nor + addressing modes. *) + +Inductive operation : Set := + | Ointconst: int -> operation (**r integer constant *) + | Ofloatconst: float -> operation (**r floating-point constant *) + | Ocast8unsigned: operation (**r 8-bit zero extension *) + | Ocast8signed: operation (**r 8-bit sign extension *) + | Ocast16unsigned: operation (**r 16-bit zero extension *) + | Ocast16signed: operation (**r 16-bit sign extension *) + | Onotint: operation (**r bitwise complement *) + | Oadd: operation (**r integer addition *) + | Osub: operation (**r integer subtraction *) + | Omul: operation (**r integer multiplication *) + | Odiv: operation (**r integer signed division *) + | Odivu: operation (**r integer unsigned division *) + | Omod: operation (**r integer signed modulus *) + | Omodu: operation (**r integer unsigned modulus *) + | Oand: operation (**r bitwise ``and'' *) + | Oor: operation (**r bitwise ``or'' *) + | Oxor: operation (**r bitwise ``xor'' *) + | Oshl: operation (**r left shift *) + | Oshr: operation (**r right signed shift *) + | Oshru: operation (**r right unsigned shift *) + | Onegf: operation (**r float opposite *) + | Oabsf: operation (**r float absolute value *) + | Oaddf: operation (**r float addition *) + | Osubf: operation (**r float subtraction *) + | Omulf: operation (**r float multiplication *) + | Odivf: operation (**r float division *) + | Osingleoffloat: operation (**r float truncation *) + | Ointoffloat: operation (**r integer to float *) + | Ofloatofint: operation (**r float to signed integer *) + | Ofloatofintu: operation (**r float to unsigned integer *) + | Ocmp: comparison -> operation (**r integer signed comparison *) + | Ocmpu: comparison -> operation (**r integer unsigned comparison *) + | Ocmpf: comparison -> operation. (**r float comparison *) + +Inductive expr : Set := + | Evar : ident -> expr (**r reading a scalar variable *) + | Eaddrof : ident -> expr (**r taking the address of a variable *) + | Eop : operation -> exprlist -> expr (**r arithmetic operation *) + | Eload : memory_chunk -> expr -> expr (**r memory read *) + | Ecall : signature -> expr -> exprlist -> expr (**r function call *) + | Econdition : expr -> expr -> expr -> expr (**r conditional expression *) + | Elet : expr -> expr -> expr (**r let binding *) + | Eletvar : nat -> expr (**r reference to a let-bound variable *) + | Ealloc : expr -> expr (**r memory allocation *) + +with exprlist : Set := + | Enil: exprlist + | Econs: expr -> exprlist -> exprlist. + +(** Statements include expression evaluation, variable assignment, + memory stores, an if/then/else conditional, + infinite loops, blocks and early block exits, and early function returns. + [Sexit n] terminates prematurely the execution of the [n+1] enclosing + [Sblock] statements. *) + +Inductive stmt : Set := + | Sskip: stmt + | Sexpr: expr -> stmt + | Sassign : ident -> expr -> stmt + | Sstore : memory_chunk -> expr -> expr -> stmt + | Sseq: stmt -> stmt -> stmt + | Sifthenelse: expr -> stmt -> stmt -> stmt + | Sloop: stmt -> stmt + | Sblock: stmt -> stmt + | Sexit: nat -> stmt + | Sswitch: expr -> list (int * nat) -> nat -> stmt + | Sreturn: option expr -> stmt. + +(** The variables can be either scalar variables + (whose type, size and signedness are given by a [memory_chunk] + or array variables (of the indicated sizes). The only operation + permitted on an array variable is taking its address. *) + +Inductive var_kind : Set := + | Vscalar: memory_chunk -> var_kind + | Varray: Z -> var_kind. + +(** Functions are composed of a signature, a list of parameter names + with associated memory chunks (parameters must be scalar), a list of + local variables with associated [var_kind] description, and a + statement representing the function body. *) + +Record function : Set := mkfunction { + fn_sig: signature; + fn_params: list (ident * memory_chunk); + fn_vars: list (ident * var_kind); + fn_body: stmt +}. + +Definition fundef := AST.fundef function. + +Record program : Set := mkprogram { + prog_funct: list (ident * fundef); + prog_main: ident; + prog_vars: list (ident * var_kind * list init_data) +}. + +Definition funsig (fd: fundef) := + match fd with + | Internal f => f.(fn_sig) + | External ef => ef.(ef_sig) + end. + +(** * Operational semantics *) + +(** The operational semantics for Csharpminor is given in big-step operational + style. Expressions evaluate to values, and statements evaluate to + ``outcomes'' indicating how execution should proceed afterwards. *) + +Inductive outcome: Set := + | Out_normal: outcome (**r continue in sequence *) + | Out_exit: nat -> outcome (**r terminate [n+1] enclosing blocks *) + | Out_return: option val -> outcome. (**r return immediately to caller *) + +Definition outcome_result_value + (out: outcome) (ot: option typ) (v: val) : Prop := + match out, ot with + | Out_normal, None => v = Vundef + | Out_return None, None => v = Vundef + | Out_return (Some v'), Some ty => v = v' + | _, _ => False + end. + +Definition outcome_block (out: outcome) : outcome := + match out with + | Out_normal => Out_normal + | Out_exit O => Out_normal + | Out_exit (S n) => Out_exit n + | Out_return optv => Out_return optv + end. + +Fixpoint switch_target (n: int) (dfl: nat) (cases: list (int * nat)) + {struct cases} : nat := + match cases with + | nil => dfl + | (n1, lbl1) :: rem => if Int.eq n n1 then lbl1 else switch_target n dfl rem + end. + +(** Four kinds of evaluation environments are involved: +- [genv]: global environments, define symbols and functions; +- [gvarenv]: map global variables to var info; +- [env]: local environments, map local variables to memory blocks + var info; +- [lenv]: let environments, map de Bruijn indices to values. +*) +Definition genv := Genv.t fundef. +Definition gvarenv := PTree.t var_kind. +Definition env := PTree.t (block * var_kind). +Definition empty_env : env := PTree.empty (block * var_kind). +Definition letenv := list val. + +Definition sizeof (lv: var_kind) : Z := + match lv with + | Vscalar chunk => size_chunk chunk + | Varray sz => Zmax 0 sz + end. + +Definition program_of_program (p: program): AST.program fundef := + AST.mkprogram + p.(prog_funct) + p.(prog_main) + (List.map (fun x => match x with (id, k, init) => (id, init) end) p.(prog_vars)). + +Definition fn_variables (f: function) := + List.map + (fun id_chunk => (fst id_chunk, Vscalar (snd id_chunk))) f.(fn_params) + ++ f.(fn_vars). + +Definition fn_params_names (f: function) := + List.map (@fst ident memory_chunk) f.(fn_params). + +Definition fn_vars_names (f: function) := + List.map (@fst ident var_kind) f.(fn_vars). + +Definition global_var_env (p: program): gvarenv := + List.fold_left + (fun gve x => match x with (id, k, init) => PTree.set id k gve end) + p.(prog_vars) (PTree.empty var_kind). + +(** Evaluation of operator applications. *) + +Definition eval_compare_null (c: comparison) (n: int) : option val := + if Int.eq n Int.zero + then match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end + else None. + +Definition eval_operation (op: operation) (vl: list val) (m: mem): option val := + match op, vl with + | Ointconst n, nil => Some (Vint n) + | Ofloatconst n, nil => Some (Vfloat n) + | Ocast8unsigned, Vint n1 :: nil => Some (Vint (Int.cast8unsigned n1)) + | Ocast8signed, Vint n1 :: nil => Some (Vint (Int.cast8signed n1)) + | Ocast16unsigned, Vint n1 :: nil => Some (Vint (Int.cast16unsigned n1)) + | Ocast16signed, Vint n1 :: nil => Some (Vint (Int.cast16signed n1)) + | Onotint, Vint n1 :: nil => Some (Vint (Int.not n1)) + | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2)) + | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1)) + | Oadd, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2)) + | Osub, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub n1 n2)) + | Osub, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.sub n1 n2)) + | Osub, Vptr b1 n1 :: Vptr b2 n2 :: nil => + if eq_block b1 b2 then Some (Vint (Int.sub n1 n2)) else None + | Omul, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.mul n1 n2)) + | Odiv, Vint n1 :: Vint n2 :: nil => + if Int.eq n2 Int.zero then None else Some (Vint (Int.divs n1 n2)) + | Odivu, Vint n1 :: Vint n2 :: nil => + if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2)) + | Omod, Vint n1 :: Vint n2 :: nil => + if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2)) + | Omodu, Vint n1 :: Vint n2 :: nil => + if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2)) + | Oand, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 n2)) + | Oor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.or n1 n2)) + | Oxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.xor n1 n2)) + | Oshl, Vint n1 :: Vint n2 :: nil => + if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None + | Oshr, Vint n1 :: Vint n2 :: nil => + if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None + | Oshru, Vint n1 :: Vint n2 :: nil => + if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None + | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1)) + | Oabsf, Vfloat f1 :: nil => Some (Vfloat (Float.abs f1)) + | Oaddf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.add f1 f2)) + | Osubf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.sub f1 f2)) + | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2)) + | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2)) + | Osingleoffloat, Vfloat f1 :: nil => + Some (Vfloat (Float.singleoffloat f1)) + | Ointoffloat, Vfloat f1 :: nil => + Some (Vint (Float.intoffloat f1)) + | Ofloatofint, Vint n1 :: nil => + Some (Vfloat (Float.floatofint n1)) + | Ofloatofintu, Vint n1 :: nil => + Some (Vfloat (Float.floatofintu n1)) + | Ocmp c, Vint n1 :: Vint n2 :: nil => + Some (Val.of_bool(Int.cmp c n1 n2)) + | Ocmp c, Vptr b1 n1 :: Vptr b2 n2 :: nil => + if valid_pointer m b1 (Int.signed n1) + && valid_pointer m b2 (Int.signed n2) then + if eq_block b1 b2 then Some(Val.of_bool(Int.cmp c n1 n2)) else None + else + None + | Ocmp c, Vptr b1 n1 :: Vint n2 :: nil => eval_compare_null c n2 + | Ocmp c, Vint n1 :: Vptr b2 n2 :: nil => eval_compare_null c n1 + | Ocmpu c, Vint n1 :: Vint n2 :: nil => + Some (Val.of_bool(Int.cmpu c n1 n2)) + | Ocmpf c, Vfloat f1 :: Vfloat f2 :: nil => + Some (Val.of_bool (Float.cmp c f1 f2)) + | _, _ => None + end. + +(** Allocation of local variables at function entry. Each variable is + bound to the reference to a fresh block of the appropriate size. *) + +Inductive alloc_variables: env -> mem -> + list (ident * var_kind) -> + env -> mem -> list block -> Prop := + | alloc_variables_nil: + forall e m, + alloc_variables e m nil e m nil + | alloc_variables_cons: + forall e m id lv vars m1 b1 m2 e2 lb, + Mem.alloc m 0 (sizeof lv) = (m1, b1) -> + alloc_variables (PTree.set id (b1, lv) e) m1 vars e2 m2 lb -> + alloc_variables e m ((id, lv) :: vars) e2 m2 (b1 :: lb). + +(** Initialization of local variables that are parameters. The value + of the corresponding argument is stored into the memory block + bound to the parameter. *) + +Inductive bind_parameters: env -> + mem -> list (ident * memory_chunk) -> list val -> + mem -> Prop := + | bind_parameters_nil: + forall e m, + bind_parameters e m nil nil m + | bind_parameters_cons: + forall e m id chunk params v1 vl b m1 m2, + PTree.get id e = Some (b, Vscalar chunk) -> + Mem.store chunk m b 0 v1 = Some m1 -> + bind_parameters e m1 params vl m2 -> + bind_parameters e m ((id, chunk) :: params) (v1 :: vl) m2. + +Section RELSEM. + +Variable prg: program. +Let ge := Genv.globalenv (program_of_program prg). + +(* Evaluation of the address of a variable: + [eval_var_addr prg ge e id b] states that variable [id] + in environment [e] evaluates to block [b]. *) + +Inductive eval_var_addr: env -> ident -> block -> Prop := + | eval_var_addr_local: + forall e id b vi, + PTree.get id e = Some (b, vi) -> + eval_var_addr e id b + | eval_var_addr_global: + forall e id b, + PTree.get id e = None -> + Genv.find_symbol ge id = Some b -> + eval_var_addr e id b. + +(* Evaluation of a reference to a scalar variable: + [eval_var_ref prg ge e id b chunk] states + that variable [id] in environment [e] evaluates to block [b] + and is associated with the memory chunk [chunk]. *) + +Inductive eval_var_ref: env -> ident -> block -> memory_chunk -> Prop := + | eval_var_ref_local: + forall e id b chunk, + PTree.get id e = Some (b, Vscalar chunk) -> + eval_var_ref e id b chunk + | eval_var_ref_global: + forall e id b chunk, + PTree.get id e = None -> + Genv.find_symbol ge id = Some b -> + PTree.get id (global_var_env prg) = Some (Vscalar chunk) -> + eval_var_ref e id b chunk. + +(** Evaluation of an expression: [eval_expr prg le e m a m' v] states + that expression [a], in initial memory state [m], evaluates to value + [v]. [m'] is the final memory state, respectively, reflecting + memory stores possibly performed by [a]. [e] and [le] are the + local environment and let environment respectively. *) + +Inductive eval_expr: + letenv -> env -> + mem -> expr -> trace -> mem -> val -> Prop := + | eval_Evar: + forall le e m id b chunk v, + eval_var_ref e id b chunk -> + Mem.load chunk m b 0 = Some v -> + eval_expr le e m (Evar id) E0 m v + | eval_Eaddrof: + forall le e m id b, + eval_var_addr e id b -> + eval_expr le e m (Eaddrof id) E0 m (Vptr b Int.zero) + | eval_Eop: + forall le e m op al t m1 vl v, + eval_exprlist le e m al t m1 vl -> + eval_operation op vl m1 = Some v -> + eval_expr le e m (Eop op al) t m1 v + | eval_Eload: + forall le e m chunk a t m1 v1 v, + eval_expr le e m a t m1 v1 -> + Mem.loadv chunk m1 v1 = Some v -> + eval_expr le e m (Eload chunk a) t m1 v + | eval_Ecall: + forall le e m sig a bl t1 m1 t2 m2 t3 m3 vf vargs vres f t, + eval_expr le e m a t1 m1 vf -> + eval_exprlist le e m1 bl t2 m2 vargs -> + Genv.find_funct ge vf = Some f -> + funsig f = sig -> + eval_funcall m2 f vargs t3 m3 vres -> + t = t1 ** t2 ** t3 -> + eval_expr le e m (Ecall sig a bl) t m3 vres + | eval_Econdition_true: + forall le e m a b c t1 m1 v1 t2 m2 v2 t, + eval_expr le e m a t1 m1 v1 -> + Val.is_true v1 -> + eval_expr le e m1 b t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr le e m (Econdition a b c) t m2 v2 + | eval_Econdition_false: + forall le e m a b c t1 m1 v1 t2 m2 v2 t, + eval_expr le e m a t1 m1 v1 -> + Val.is_false v1 -> + eval_expr le e m1 c t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr le e m (Econdition a b c) t m2 v2 + | eval_Elet: + forall le e m a b t1 m1 v1 t2 m2 v2 t, + eval_expr le e m a t1 m1 v1 -> + eval_expr (v1::le) e m1 b t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr le e m (Elet a b) t m2 v2 + | eval_Eletvar: + forall le e m n v, + nth_error le n = Some v -> + eval_expr le e m (Eletvar n) E0 m v + | eval_Ealloc: + forall le e m a t m1 n m2 b, + eval_expr le e m a t m1 (Vint n) -> + Mem.alloc m1 0 (Int.signed n) = (m2, b) -> + eval_expr le e m (Ealloc a) t m2 (Vptr b Int.zero) + +(** Evaluation of a list of expressions: + [eval_exprlist prg le al m a m' vl] + states that the list [al] of expressions evaluate + to the list [vl] of values. + The other parameters are as in [eval_expr]. +*) + +with eval_exprlist: + letenv -> env -> + mem -> exprlist -> trace -> + mem -> list val -> Prop := + | eval_Enil: + forall le e m, + eval_exprlist le e m Enil E0 m nil + | eval_Econs: + forall le e m a bl t1 m1 v t2 m2 vl t, + eval_expr le e m a t1 m1 v -> + eval_exprlist le e m1 bl t2 m2 vl -> + t = t1 ** t2 -> + eval_exprlist le e m (Econs a bl) t m2 (v :: vl) + +(** Evaluation of a function invocation: [eval_funcall prg m f args m' res] + means that the function [f], applied to the arguments [args] in + memory state [m], returns the value [res] in modified memory state [m']. +*) +with eval_funcall: + mem -> fundef -> list val -> trace -> + mem -> val -> Prop := + | eval_funcall_internal: + forall m f vargs e m1 lb m2 t m3 out vres, + list_norepet (fn_params_names f ++ fn_vars_names f) -> + alloc_variables empty_env m (fn_variables f) e m1 lb -> + bind_parameters e m1 f.(fn_params) vargs m2 -> + exec_stmt e m2 f.(fn_body) t m3 out -> + outcome_result_value out f.(fn_sig).(sig_res) vres -> + eval_funcall m (Internal f) vargs t (Mem.free_list m3 lb) vres + | eval_funcall_external: + forall m ef vargs t vres, + event_match ef vargs t vres -> + eval_funcall m (External ef) vargs t m vres + +(** Execution of a statement: [exec_stmt prg e m s m' out] + means that statement [s] executes with outcome [out]. + The other parameters are as in [eval_expr]. *) + +with exec_stmt: + env -> + mem -> stmt -> trace -> + mem -> outcome -> Prop := + | exec_Sskip: + forall e m, + exec_stmt e m Sskip E0 m Out_normal + | exec_Sexpr: + forall e m a t m1 v, + eval_expr nil e m a t m1 v -> + exec_stmt e m (Sexpr a) t m1 Out_normal + | eval_Sassign: + forall e m id a t m1 b chunk v m2, + eval_expr nil e m a t m1 v -> + eval_var_ref e id b chunk -> + Mem.store chunk m1 b 0 v = Some m2 -> + exec_stmt e m (Sassign id a) t m2 Out_normal + | eval_Sstore: + forall e m chunk a b t1 m1 v1 t2 m2 v2 t3 m3, + eval_expr nil e m a t1 m1 v1 -> + eval_expr nil e m1 b t2 m2 v2 -> + Mem.storev chunk m2 v1 v2 = Some m3 -> + t3 = t1 ** t2 -> + exec_stmt e m (Sstore chunk a b) t3 m3 Out_normal + | exec_Sseq_continue: + forall e m s1 s2 t1 t2 m1 m2 t out, + exec_stmt e m s1 t1 m1 Out_normal -> + exec_stmt e m1 s2 t2 m2 out -> + t = t1 ** t2 -> + exec_stmt e m (Sseq s1 s2) t m2 out + | exec_Sseq_stop: + forall e m s1 s2 t1 m1 out, + exec_stmt e m s1 t1 m1 out -> + out <> Out_normal -> + exec_stmt e m (Sseq s1 s2) t1 m1 out + | exec_Sifthenelse_true: + forall e m a sl1 sl2 t1 m1 v1 t2 m2 out t, + eval_expr nil e m a t1 m1 v1 -> + Val.is_true v1 -> + exec_stmt e m1 sl1 t2 m2 out -> + t = t1 ** t2 -> + exec_stmt e m (Sifthenelse a sl1 sl2) t m2 out + | exec_Sifthenelse_false: + forall e m a sl1 sl2 t1 m1 v1 t2 m2 out t, + eval_expr nil e m a t1 m1 v1 -> + Val.is_false v1 -> + exec_stmt e m1 sl2 t2 m2 out -> + t = t1 ** t2 -> + exec_stmt e m (Sifthenelse a sl1 sl2) t m2 out + | exec_Sloop_loop: + forall e m sl t1 m1 t2 m2 out t, + exec_stmt e m sl t1 m1 Out_normal -> + exec_stmt e m1 (Sloop sl) t2 m2 out -> + t = t1 ** t2 -> + exec_stmt e m (Sloop sl) t m2 out + | exec_Sloop_stop: + forall e m sl t1 m1 out, + exec_stmt e m sl t1 m1 out -> + out <> Out_normal -> + exec_stmt e m (Sloop sl) t1 m1 out + | exec_Sblock: + forall e m sl t1 m1 out, + exec_stmt e m sl t1 m1 out -> + exec_stmt e m (Sblock sl) t1 m1 (outcome_block out) + | exec_Sexit: + forall e m n, + exec_stmt e m (Sexit n) E0 m (Out_exit n) + | exec_Sswitch: + forall e m a cases default t1 m1 n, + eval_expr nil e m a t1 m1 (Vint n) -> + exec_stmt e m (Sswitch a cases default) + t1 m1 (Out_exit (switch_target n default cases)) + | exec_Sreturn_none: + forall e m, + exec_stmt e m (Sreturn None) E0 m (Out_return None) + | exec_Sreturn_some: + forall e m a t1 m1 v, + eval_expr nil e m a t1 m1 v -> + exec_stmt e m (Sreturn (Some a)) t1 m1 (Out_return (Some v)). + +Scheme eval_expr_ind4 := Minimality for eval_expr Sort Prop + with eval_exprlist_ind4 := Minimality for eval_exprlist Sort Prop + with eval_funcall_ind4 := Minimality for eval_funcall Sort Prop + with exec_stmt_ind4 := Minimality for exec_stmt Sort Prop. + +End RELSEM. + +(** Execution of a whole program: [exec_program p r] + holds if the application of [p]'s main function to no arguments + in the initial memory state for [p] eventually returns value [r]. *) + +Definition exec_program (p: program) (t: trace) (r: val) : Prop := + let ge := Genv.globalenv (program_of_program p) in + let m0 := Genv.init_mem (program_of_program p) in + exists b, exists f, exists m, + Genv.find_symbol ge p.(prog_main) = Some b /\ + Genv.find_funct_ptr ge b = Some f /\ + funsig f = mksignature nil (Some Tint) /\ + eval_funcall p m0 f nil t m r. -- cgit