diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-01-14 14:23:26 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-01-14 14:23:26 +0000 |
commit | a82c9c0e4a0b8e37c9c3ea5ae99714982563606f (patch) | |
tree | 93b9999698a4cd47ec4cb5fcdcdfd215d62f8e9e /backend | |
parent | bb8f49c419eb8205ef541edcbe17f4d14aa99564 (diff) |
Merge of the nonstrict-ops branch:
- Most RTL operators now evaluate to Some Vundef instead of None
when undefined behavior occurs.
- More aggressive instruction selection.
- "Bertotization" of pattern-matchings now implemented by a proper preprocessor.
- Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Allocproof.v | 17 | ||||
-rw-r--r-- | backend/CSEproof.v | 15 | ||||
-rw-r--r-- | backend/CastOptim.v | 276 | ||||
-rw-r--r-- | backend/CastOptimproof.v | 577 | ||||
-rw-r--r-- | backend/Cminor.v | 120 | ||||
-rw-r--r-- | backend/Constprop.v | 26 | ||||
-rw-r--r-- | backend/Constpropproof.v | 314 | ||||
-rw-r--r-- | backend/LTL.v | 15 | ||||
-rw-r--r-- | backend/Linearizeproof.v | 11 | ||||
-rw-r--r-- | backend/RTL.v | 15 | ||||
-rw-r--r-- | backend/RTLgenproof.v | 33 | ||||
-rw-r--r-- | backend/RTLtyping.v | 1 | ||||
-rw-r--r-- | backend/Reloadproof.v | 2 | ||||
-rw-r--r-- | backend/Selectionproof.v | 426 | ||||
-rw-r--r-- | backend/Tailcallproof.v | 13 | ||||
-rw-r--r-- | backend/Tunnelingproof.v | 9 |
16 files changed, 570 insertions, 1300 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index ae86ee8..a9477e0 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -705,22 +705,13 @@ Proof. eapply agree_assign_live; eauto. eapply agree_reg_list_live; eauto. - (* Icond, true *) - assert (COND: eval_condition cond (map ls (map assign args)) m = Some true). + (* Icond *) + assert (COND: eval_condition cond (map ls (map assign args)) m = Some b). replace (map ls (map assign args)) with (rs##args). auto. eapply agree_eval_regs; eauto. econstructor; split. - eapply exec_Lcond_true; eauto. TranslInstr. - MatchStates. - eapply agree_undef_temps; eauto. - eapply agree_reg_list_live. eauto. - (* Icond, false *) - assert (COND: eval_condition cond (map ls (map assign args)) m = Some false). - replace (map ls (map assign args)) with (rs##args). auto. - eapply agree_eval_regs; eauto. - econstructor; split. - eapply exec_Lcond_false; eauto. TranslInstr. - MatchStates. + eapply exec_Lcond; eauto. TranslInstr. + MatchStates. destruct b; simpl; auto. eapply agree_undef_temps; eauto. eapply agree_reg_list_live. eauto. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 77da538..c685ef6 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -899,21 +899,14 @@ Proof. apply add_unknown_satisfiable. apply wf_kill_loads. apply wf_analyze. eapply kill_load_satisfiable; eauto. - (* Icond true *) + (* Icond *) econstructor; split. - eapply exec_Icond_true; eauto. + eapply exec_Icond; eauto. econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H; auto. - - (* Icond false *) - econstructor; split. - eapply exec_Icond_false; eauto. - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; auto. + destruct b; eapply analysis_correct_1; eauto; simpl; auto; unfold transfer; rewrite H; auto. - (* Icond false *) + (* Ijumptable *) econstructor; split. eapply exec_Ijumptable; eauto. econstructor; eauto. diff --git a/backend/CastOptim.v b/backend/CastOptim.v deleted file mode 100644 index 19d0065..0000000 --- a/backend/CastOptim.v +++ /dev/null @@ -1,276 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Elimination of redundant conversions to small numerical types. *) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Globalenvs. -Require Import Op. -Require Import Registers. -Require Import RTL. -Require Import Lattice. -Require Import Kildall. - -(** * Static analysis *) - -(** Compile-time approximations *) - -Inductive approx : Type := - | Unknown (**r any value *) - | Int7 (**r [[0,127]] *) - | Int8s (**r [[-128,127]] *) - | Int8u (**r [[0,255]] *) - | Int15 (**r [[0,32767]] *) - | Int16s (**r [[-32768,32767]] *) - | Int16u (**r [[0,65535]] *) - | Single (**r single-precision float *) - | Novalue. (**r empty *) - -(** We equip this type of approximations with a semi-lattice structure. - The ordering is inclusion between the sets of values denoted by - the approximations. *) - -Module Approx <: SEMILATTICE_WITH_TOP. - Definition t := approx. - Definition eq (x y: t) := (x = y). - Definition eq_refl: forall x, eq x x := (@refl_equal t). - Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). - Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). - Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}. - Proof. - decide equality. - Qed. - Definition beq (x y: t) := if eq_dec x y then true else false. - Lemma beq_correct: forall x y, beq x y = true -> x = y. - Proof. - unfold beq; intros. destruct (eq_dec x y). auto. congruence. - Qed. - Definition ge (x y: t) : Prop := - match x, y with - | Unknown, _ => True - | _, Novalue => True - | Int7, Int7 => True - | Int8s, (Int7 | Int8s) => True - | Int8u, (Int7 | Int8u) => True - | Int15, (Int7 | Int8u | Int15) => True - | Int16s, (Int7 | Int8s | Int8u | Int15 | Int16s) => True - | Int16u, (Int7 | Int8u | Int15 | Int16u) => True - | Single, Single => True - | _, _ => False - end. - Lemma ge_refl: forall x y, eq x y -> ge x y. - Proof. - unfold eq, ge; intros. subst y. destruct x; auto. - Qed. - Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Proof. - unfold ge; intros. - destruct x; auto; (destruct y; auto; try contradiction; destruct z; auto). - Qed. - Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. - Proof. - unfold eq; intros. congruence. - Qed. - Definition bge (x y: t) : bool := - match x, y with - | Unknown, _ => true - | _, Novalue => true - | Int7, Int7 => true - | Int8s, (Int7 | Int8s) => true - | Int8u, (Int7 | Int8u) => true - | Int15, (Int7 | Int8u | Int15) => true - | Int16s, (Int7 | Int8s | Int8u | Int15 | Int16s) => true - | Int16u, (Int7 | Int8u | Int15 | Int16u) => true - | Single, Single => true - | _, _ => false - end. - Lemma bge_correct: forall x y, bge x y = true -> ge x y. - Proof. - destruct x; destruct y; simpl; auto || congruence. - Qed. - Definition bot := Novalue. - Definition top := Unknown. - Lemma ge_bot: forall x, ge x bot. - Proof. - unfold ge, bot. destruct x; auto. - Qed. - Lemma ge_top: forall x, ge top x. - Proof. - unfold ge, top. auto. - Qed. - Definition lub (x y: t) : t := - match x, y with - | Novalue, _ => y - | _, Novalue => x - | Int7, Int7 => Int7 - | Int7, Int8u => Int8u - | Int7, Int8s => Int8s - | Int7, Int15 => Int15 - | Int7, Int16u => Int16u - | Int7, Int16s => Int16s - | Int8u, (Int7|Int8u) => Int8u - | Int8u, Int15 => Int15 - | Int8u, Int16u => Int16u - | Int8u, Int16s => Int16s - | Int8s, (Int7|Int8s) => Int8s - | Int8s, (Int15|Int16s) => Int16s - | Int15, (Int7|Int8u|Int15) => Int15 - | Int15, Int16u => Int16u - | Int15, (Int8s|Int16s) => Int16s - | Int16u, (Int7|Int8u|Int15|Int16u) => Int16u - | Int16s, (Int7|Int8u|Int8s|Int15|Int16s) => Int16s - | Single, Single => Single - | _, _ => Unknown - end. - Lemma ge_lub_left: forall x y, ge (lub x y) x. - Proof. - unfold lub, ge; intros. - destruct x; destruct y; auto. - Qed. - Lemma ge_lub_right: forall x y, ge (lub x y) y. - Proof. - unfold lub, ge; intros. - destruct x; destruct y; auto. - Qed. -End Approx. - -Module D := LPMap Approx. - -(** Abstract interpretation of operators *) - -Definition approx_bitwise_op (v1 v2: approx) : approx := - if Approx.bge Int8u v1 && Approx.bge Int8u v2 then Int8u - else if Approx.bge Int16u v1 && Approx.bge Int16u v2 then Int16u - else Unknown. - -Function approx_operation (op: operation) (vl: list approx) : approx := - match op, vl with - | Omove, v1 :: nil => v1 - | Ointconst n, _ => - if Int.eq_dec n (Int.zero_ext 7 n) then Int7 - else if Int.eq_dec n (Int.zero_ext 8 n) then Int8u - else if Int.eq_dec n (Int.sign_ext 8 n) then Int8s - else if Int.eq_dec n (Int.zero_ext 15 n) then Int15 - else if Int.eq_dec n (Int.zero_ext 16 n) then Int16u - else if Int.eq_dec n (Int.sign_ext 16 n) then Int16s - else Unknown - | Ofloatconst n, _ => - if Float.eq_dec n (Float.singleoffloat n) then Single else Unknown - | Ocast8signed, _ => Int8s - | Ocast8unsigned, _ => Int8u - | Ocast16signed, _ => Int16s - | Ocast16unsigned, _ => Int16u - | Osingleoffloat, _ => Single - | Oand, v1 :: v2 :: nil => approx_bitwise_op v1 v2 - | Oor, v1 :: v2 :: nil => approx_bitwise_op v1 v2 - | Oxor, v1 :: v2 :: nil => approx_bitwise_op v1 v2 - (* Problem: what about and/or/xor immediate? and other - machine-specific operators? *) - | Ocmp c, _ => Int7 - | _, _ => Unknown - end. - -Definition approx_of_chunk (chunk: memory_chunk) := - match chunk with - | Mint8signed => Int8s - | Mint8unsigned => Int8u - | Mint16signed => Int16s - | Mint16unsigned => Int16u - | Mint32 => Unknown - | Mfloat32 => Single - | Mfloat64 => Unknown - end. - -(** Transfer function for the analysis *) - -Definition approx_reg (app: D.t) (r: reg) := - D.get r app. - -Definition approx_regs (app: D.t) (rl: list reg):= - List.map (approx_reg app) rl. - -Definition transfer (f: function) (pc: node) (before: D.t) := - match f.(fn_code)!pc with - | None => before - | Some i => - match i with - | Iop op args res s => - let a := approx_operation op (approx_regs before args) in - D.set res a before - | Iload chunk addr args dst s => - D.set dst (approx_of_chunk chunk) before - | Icall sig ros args res s => - D.set res Unknown before - | Ibuiltin ef args res s => - D.set res Unknown before - | _ => - before - end - end. - -(** The static analysis is a forward dataflow analysis. *) - -Module DS := Dataflow_Solver(D)(NodeSetForward). - -Definition analyze (f: RTL.function): PMap.t D.t := - match DS.fixpoint (successors f) (transfer f) - ((f.(fn_entrypoint), D.top) :: nil) with - | None => PMap.init D.top - | Some res => res - end. - -(** * Code transformation *) - -(** Cast operations that have no effect (because the argument is already - in the right range) are turned into moves. *) - -Function transf_operation (op: operation) (vl: list approx) : operation := - match op, vl with - | Ocast8signed, v :: nil => if Approx.bge Int8s v then Omove else op - | Ocast8unsigned, v :: nil => if Approx.bge Int8u v then Omove else op - | Ocast16signed, v :: nil => if Approx.bge Int16s v then Omove else op - | Ocast16unsigned, v :: nil => if Approx.bge Int16u v then Omove else op - | Osingleoffloat, v :: nil => if Approx.bge Single v then Omove else op - | _, _ => op - end. - -Definition transf_instr (app: D.t) (instr: instruction) := - match instr with - | Iop op args res s => - let op' := transf_operation op (approx_regs app args) in - Iop op' args res s - | _ => - instr - end. - -Definition transf_code (approxs: PMap.t D.t) (instrs: code) : code := - PTree.map (fun pc instr => transf_instr approxs!!pc instr) instrs. - -Definition transf_function (f: function) : function := - let approxs := analyze f in - mkfunction - f.(fn_sig) - f.(fn_params) - f.(fn_stacksize) - (transf_code approxs f.(fn_code)) - f.(fn_entrypoint). - -Definition transf_fundef (fd: fundef) : fundef := - AST.transf_fundef transf_function fd. - -Definition transf_program (p: program) : program := - transform_program transf_fundef p. diff --git a/backend/CastOptimproof.v b/backend/CastOptimproof.v deleted file mode 100644 index 0afc208..0000000 --- a/backend/CastOptimproof.v +++ /dev/null @@ -1,577 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Correctness proof for cast optimization. *) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Events. -Require Import Memory. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Op. -Require Import Registers. -Require Import RTL. -Require Import Lattice. -Require Import Kildall. -Require Import CastOptim. - -(** * Correctness of the static analysis *) - -Section ANALYSIS. - -Definition val_match_approx (a: approx) (v: val) : Prop := - match a with - | Novalue => False - | Int7 => v = Val.zero_ext 8 v /\ v = Val.sign_ext 8 v - | Int8u => v = Val.zero_ext 8 v - | Int8s => v = Val.sign_ext 8 v - | Int15 => v = Val.zero_ext 16 v /\ v = Val.sign_ext 16 v - | Int16u => v = Val.zero_ext 16 v - | Int16s => v = Val.sign_ext 16 v - | Single => v = Val.singleoffloat v - | Unknown => True - end. - -Definition regs_match_approx (a: D.t) (rs: regset) : Prop := - forall r, val_match_approx (D.get r a) rs#r. - -Lemma regs_match_approx_top: - forall rs, regs_match_approx D.top rs. -Proof. - intros. red; intros. simpl. rewrite PTree.gempty. - unfold Approx.top, val_match_approx. auto. -Qed. - -Lemma val_match_approx_increasing: - forall a1 a2 v, - Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v. -Proof. - assert (A: forall v, v = Val.zero_ext 8 v -> v = Val.zero_ext 16 v). - intros. rewrite H. - destruct v; simpl; auto. decEq. symmetry. - apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto. - assert (B: forall v, v = Val.sign_ext 8 v -> v = Val.sign_ext 16 v). - intros. rewrite H. - destruct v; simpl; auto. decEq. symmetry. - apply Int.sign_ext_widen. compute; auto. split. omega. compute; auto. - assert (C: forall v, v = Val.zero_ext 8 v -> v = Val.sign_ext 16 v). - intros. rewrite H. - destruct v; simpl; auto. decEq. symmetry. - apply Int.sign_zero_ext_widen. compute; auto. split. omega. compute; auto. - intros. destruct a1; destruct a2; simpl in *; intuition; auto. -Qed. - -Lemma regs_match_approx_increasing: - forall a1 a2 rs, - D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs. -Proof. - unfold D.ge, regs_match_approx. intros. - apply val_match_approx_increasing with (D.get r a2); auto. -Qed. - -Lemma regs_match_approx_update: - forall ra rs a v r, - val_match_approx a v -> - regs_match_approx ra rs -> - regs_match_approx (D.set r a ra) (rs#r <- v). -Proof. - intros; red; intros. rewrite Regmap.gsspec. - case (peq r0 r); intro. - subst r0. rewrite D.gss. auto. - rewrite D.gso; auto. -Qed. - -Lemma approx_regs_val_list: - forall ra rs rl, - regs_match_approx ra rs -> - list_forall2 val_match_approx (approx_regs ra rl) rs##rl. -Proof. - induction rl; simpl; intros. - constructor. - constructor. apply H. auto. -Qed. - -Lemma analyze_correct: - forall f pc rs pc' i, - f.(fn_code)!pc = Some i -> - In pc' (successors_instr i) -> - regs_match_approx (transfer f pc (analyze f)!!pc) rs -> - regs_match_approx (analyze f)!!pc' rs. -Proof. - intros until i. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer f) - ((fn_entrypoint f, D.top) :: nil)). - intros approxs; intros. - apply regs_match_approx_increasing with (transfer f pc approxs!!pc). - eapply DS.fixpoint_solution; eauto. - unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto. - auto. - intros. rewrite PMap.gi. apply regs_match_approx_top. -Qed. - -Lemma analyze_correct_start: - forall f rs, - regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs. -Proof. - intros. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer f) - ((fn_entrypoint f, D.top) :: nil)). - intros approxs; intros. - apply regs_match_approx_increasing with D.top. - eapply DS.fixpoint_entry; eauto. auto with coqlib. - apply regs_match_approx_top. - intros. rewrite PMap.gi. apply regs_match_approx_top. -Qed. - -Lemma approx_bitwise_correct: - forall (sem_op: int -> int -> int) a1 n1 a2 n2, - (forall a b c, sem_op (Int.and a c) (Int.and b c) = Int.and (sem_op a b) c) -> - val_match_approx a1 (Vint n1) -> val_match_approx a2 (Vint n2) -> - val_match_approx (approx_bitwise_op a1 a2) (Vint (sem_op n1 n2)). -Proof. - intros. - assert (forall N, 0 < N < Z_of_nat Int.wordsize -> - sem_op (Int.zero_ext N n1) (Int.zero_ext N n2) = - Int.zero_ext N (sem_op (Int.zero_ext N n1) (Int.zero_ext N n2))). - intros. repeat rewrite Int.zero_ext_and; auto. rewrite H. - rewrite Int.and_assoc. rewrite Int.and_idem. auto. - unfold approx_bitwise_op. - caseEq (Approx.bge Int8u a1 && Approx.bge Int8u a2); intro EQ1. - destruct (andb_prop _ _ EQ1). - assert (V1: val_match_approx Int8u (Vint n1)). - eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto. - assert (V2: val_match_approx Int8u (Vint n2)). - eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto. - simpl in *. inversion V1; inversion V2; decEq. apply H2. compute; auto. - caseEq (Approx.bge Int16u a1 && Approx.bge Int16u a2); intro EQ2. - destruct (andb_prop _ _ EQ2). - assert (V1: val_match_approx Int16u (Vint n1)). - eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto. - assert (V2: val_match_approx Int16u (Vint n2)). - eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto. - simpl in *. inversion V1; inversion V2; decEq. apply H2. compute; auto. - exact I. -Qed. - -Lemma approx_operation_correct: - forall app rs (ge: genv) sp op args m v, - regs_match_approx app rs -> - eval_operation ge sp op rs##args m = Some v -> - val_match_approx (approx_operation op (approx_regs app args)) v. -Proof. - intros. destruct op; simpl; try (exact I). -(* move *) - destruct args; try (exact I). destruct args; try (exact I). - simpl. simpl in H0. inv H0. apply H. -(* const int *) - destruct args; simpl in H0; inv H0. - destruct (Int.eq_dec i (Int.zero_ext 7 i)). red; simpl. - split. - decEq. rewrite e. symmetry. apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto. - decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. compute; auto. compute; auto. - destruct (Int.eq_dec i (Int.zero_ext 8 i)). red; simpl; congruence. - destruct (Int.eq_dec i (Int.sign_ext 8 i)). red; simpl; congruence. - destruct (Int.eq_dec i (Int.zero_ext 15 i)). red; simpl. - split. - decEq. rewrite e. symmetry. apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto. - decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. compute; auto. compute; auto. - destruct (Int.eq_dec i (Int.zero_ext 16 i)). red; simpl; congruence. - destruct (Int.eq_dec i (Int.sign_ext 16 i)). red; simpl; congruence. - exact I. -(* const float *) - destruct args; simpl in H0; inv H0. - destruct (Float.eq_dec f (Float.singleoffloat f)). red; simpl; congruence. - exact I. -(* cast8signed *) - destruct args; simpl in H0; try congruence. - destruct args; simpl in H0; try congruence. - inv H0. destruct (rs#p); simpl; auto. - decEq. symmetry. apply Int.sign_ext_idem. compute; auto. -(* cast8unsigned *) - destruct args; simpl in H0; try congruence. - destruct args; simpl in H0; try congruence. - inv H0. destruct (rs#p); simpl; auto. - decEq. symmetry. apply Int.zero_ext_idem. compute; auto. -(* cast16signed *) - destruct args; simpl in H0; try congruence. - destruct args; simpl in H0; try congruence. - inv H0. destruct (rs#p); simpl; auto. - decEq. symmetry. apply Int.sign_ext_idem. compute; auto. -(* cast16unsigned *) - destruct args; simpl in H0; try congruence. - destruct args; simpl in H0; try congruence. - inv H0. destruct (rs#p); simpl; auto. - decEq. symmetry. apply Int.zero_ext_idem. compute; auto. -(* and *) - destruct args; try (exact I). - destruct args; try (exact I). - destruct args; try (exact I). - generalize (H p) (H p0). simpl in *. FuncInv. subst. - apply approx_bitwise_correct; auto. - intros. repeat rewrite Int.and_assoc. decEq. - rewrite (Int.and_commut b c). rewrite <- Int.and_assoc. rewrite Int.and_idem. auto. -(* or *) - destruct args; try (exact I). - destruct args; try (exact I). - destruct args; try (exact I). - generalize (H p) (H p0). simpl in *. FuncInv. subst. - apply approx_bitwise_correct; auto. - intros. rewrite (Int.and_commut a c); rewrite (Int.and_commut b c). - rewrite <- Int.and_or_distrib. apply Int.and_commut. -(* xor *) - destruct args; try (exact I). - destruct args; try (exact I). - destruct args; try (exact I). - generalize (H p) (H p0). simpl in *. FuncInv. subst. - apply approx_bitwise_correct; auto. - intros. rewrite (Int.and_commut a c); rewrite (Int.and_commut b c). - rewrite <- Int.and_xor_distrib. apply Int.and_commut. -(* singleoffloat *) - destruct args; simpl in H0; try congruence. - destruct args; simpl in H0; try congruence. - inv H0. destruct (rs#p); simpl; auto. - decEq. rewrite Float.singleoffloat_idem; auto. -(* comparison *) - simpl in H0. destruct (eval_condition c rs##args); try discriminate. - destruct b; inv H0; compute; auto. -Qed. - -Lemma approx_of_chunk_correct: - forall chunk m a v, - Mem.loadv chunk m a = Some v -> - val_match_approx (approx_of_chunk chunk) v. -Proof. - intros. destruct a; simpl in H; try discriminate. - exploit Mem.load_cast; eauto. - destruct chunk; intros; simpl; auto. -Qed. - -End ANALYSIS. - -(** * Correctness of the code transformation *) - -Section PRESERVATION. - -Variable prog: program. -Let tprog := transf_program prog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - -Lemma symbols_preserved: - forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intros; unfold ge, tge, tprog, transf_program. - apply Genv.find_symbol_transf. -Qed. - -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof. - intros; unfold ge, tge, tprog, transf_program. - apply Genv.find_var_info_transf. -Qed. - -Lemma functions_translated: - forall (v: val) (f: fundef), - Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (transf_fundef f). -Proof. - intros. - exact (Genv.find_funct_transf transf_fundef _ _ H). -Qed. - -Lemma function_ptr_translated: - forall (b: block) (f: fundef), - Genv.find_funct_ptr ge b = Some f -> - Genv.find_funct_ptr tge b = Some (transf_fundef f). -Proof. - intros. - exact (Genv.find_funct_ptr_transf transf_fundef _ _ H). -Qed. - -Lemma sig_function_translated: - forall f, - funsig (transf_fundef f) = funsig f. -Proof. - intros. destruct f; reflexivity. -Qed. - -Lemma find_function_translated: - forall ros rs fd, - find_function ge ros rs = Some fd -> - find_function tge ros rs = Some (transf_fundef fd). -Proof. - intros. destruct ros; simpl in *. - apply functions_translated; auto. - rewrite symbols_preserved. destruct (Genv.find_symbol ge i); try congruence. - apply function_ptr_translated; auto. -Qed. - -(** Correctness of [transf_operation]. *) - -Lemma transf_operation_correct: - forall (ge: genv) app rs sp op args m v, - regs_match_approx app rs -> - eval_operation ge sp op rs##args m = Some v -> - eval_operation ge sp (transf_operation op (approx_regs app args)) rs##args m = Some v. -Proof. - intros until v. intro RMA. - assert (A: forall a r, Approx.bge a (approx_reg app r) = true -> val_match_approx a rs#r). - intros. eapply val_match_approx_increasing. apply Approx.bge_correct; eauto. apply RMA. -Opaque Approx.bge. - destruct op; simpl; auto. -(* cast8signed *) - destruct args; simpl; try congruence. destruct args; simpl; try congruence. - intros EQ; inv EQ. - caseEq (Approx.bge Int8s (approx_reg app p)); intros. - exploit A; eauto. unfold val_match_approx. simpl. congruence. - auto. -(* cast8unsigned *) - destruct args; simpl; try congruence. destruct args; simpl; try congruence. - intros EQ; inv EQ. - caseEq (Approx.bge Int8u (approx_reg app p)); intros. - exploit A; eauto. unfold val_match_approx. simpl. congruence. - auto. -(* cast8signed *) - destruct args; simpl; try congruence. destruct args; simpl; try congruence. - intros EQ; inv EQ. - caseEq (Approx.bge Int16s (approx_reg app p)); intros. - exploit A; eauto. unfold val_match_approx. simpl. congruence. - auto. -(* cast8unsigned *) - destruct args; simpl; try congruence. destruct args; simpl; try congruence. - intros EQ; inv EQ. - caseEq (Approx.bge Int16u (approx_reg app p)); intros. - exploit A; eauto. unfold val_match_approx. simpl. congruence. - auto. -(* singleoffloat *) - destruct args; simpl; try congruence. destruct args; simpl; try congruence. - intros EQ; inv EQ. - caseEq (Approx.bge Single (approx_reg app p)); intros. - exploit A; eauto. unfold val_match_approx. simpl. congruence. - auto. -Qed. - -(** Matching between states. *) - -Inductive match_stackframes: stackframe -> stackframe -> Prop := - match_stackframe_intro: - forall res sp pc rs f, - (forall v, regs_match_approx (analyze f)!!pc (rs#res <- v)) -> - match_stackframes - (Stackframe res f sp pc rs) - (Stackframe res (transf_function f) sp pc rs). - -Inductive match_states: state -> state -> Prop := - | match_states_intro: - forall s sp pc rs m f s' - (MATCH: regs_match_approx (analyze f)!!pc rs) - (STACKS: list_forall2 match_stackframes s s'), - match_states (State s f sp pc rs m) - (State s' (transf_function f) sp pc rs m) - | match_states_call: - forall s f args m s', - list_forall2 match_stackframes s s' -> - match_states (Callstate s f args m) - (Callstate s' (transf_fundef f) args m) - | match_states_return: - forall s s' v m, - list_forall2 match_stackframes s s' -> - match_states (Returnstate s v m) - (Returnstate s' v m). - -Ltac TransfInstr := - match goal with - | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ => - cut ((transf_function f).(fn_code)!pc = Some(transf_instr (analyze f)!!pc instr)); - [ simpl transf_instr - | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; - unfold option_map; rewrite H1; reflexivity ] - end. - -(** The proof of semantic preservation follows from the lock-step simulation lemma below. *) - -Lemma transf_step_correct: - forall s1 t s2, - step ge s1 t s2 -> - forall s1' (MS: match_states s1 s1'), - exists s2', step tge s1' t s2' /\ match_states s2 s2'. -Proof. - induction 1; intros; inv MS. - - (* Inop *) - econstructor; split. - TransfInstr; intro. eapply exec_Inop; eauto. - econstructor; eauto. - eapply analyze_correct with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. auto. - - (* Iop *) - exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split. - TransfInstr; intro. eapply exec_Iop; eauto. - apply transf_operation_correct; auto. - rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. - econstructor; eauto. - eapply analyze_correct with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. apply regs_match_approx_update; auto. - eapply approx_operation_correct; eauto. - - (* Iload *) - econstructor; split. - TransfInstr; intro. eapply exec_Iload with (a := a). eauto. - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eauto. - econstructor; eauto. - eapply analyze_correct with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. apply regs_match_approx_update; auto. - eapply approx_of_chunk_correct; eauto. - - (* Istore *) - econstructor; split. - TransfInstr; intro. eapply exec_Istore with (a := a). eauto. - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eauto. - econstructor; eauto. - eapply analyze_correct with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. auto. - - (* Icall *) - TransfInstr; intro. - econstructor; split. - eapply exec_Icall. eauto. apply find_function_translated; eauto. - apply sig_function_translated; auto. - constructor; auto. constructor; auto. - econstructor; eauto. - intros. eapply analyze_correct; eauto. simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. exact I. - - (* Itailcall *) - TransfInstr; intro. - econstructor; split. - eapply exec_Itailcall. eauto. apply find_function_translated; eauto. - apply sig_function_translated; auto. - simpl; eauto. - constructor; auto. - - (* Ibuiltin *) - TransfInstr. intro. - exists (State s' (transf_function f) sp pc' (rs#res <- v) m'); split. - eapply exec_Ibuiltin; eauto. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. - econstructor; eauto. - eapply analyze_correct; eauto. simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. exact I. - - (* Icond, true *) - exists (State s' (transf_function f) sp ifso rs m); split. - TransfInstr. intro. - eapply exec_Icond_true; eauto. - econstructor; eauto. - eapply analyze_correct; eauto. - simpl; auto. - unfold transfer; rewrite H; auto. - - (* Icond, false *) - exists (State s' (transf_function f) sp ifnot rs m); split. - TransfInstr. intro. - eapply exec_Icond_false; eauto. - econstructor; eauto. - eapply analyze_correct; eauto. - simpl; auto. - unfold transfer; rewrite H; auto. - - (* Ijumptable *) - exists (State s' (transf_function f) sp pc' rs m); split. - TransfInstr. intro. - eapply exec_Ijumptable; eauto. - constructor; auto. - eapply analyze_correct; eauto. - simpl. eapply list_nth_z_in; eauto. - unfold transfer; rewrite H; auto. - - (* Ireturn *) - exists (Returnstate s' (regmap_optget or Vundef rs) m'); split. - eapply exec_Ireturn; eauto. TransfInstr; auto. - constructor; auto. - - (* internal function *) - simpl. unfold transf_function. - econstructor; split. - eapply exec_function_internal; simpl; eauto. - simpl. econstructor; eauto. - apply analyze_correct_start; auto. - - (* external function *) - simpl. econstructor; split. - eapply exec_function_external; eauto. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. - constructor; auto. - - (* return *) - inv H3. inv H1. - econstructor; split. - eapply exec_return; eauto. - econstructor; eauto. -Qed. - -Lemma transf_initial_states: - forall st1, initial_state prog st1 -> - exists st2, initial_state tprog st2 /\ match_states st1 st2. -Proof. - intros. inversion H. - exploit function_ptr_translated; eauto. intro FIND. - exists (Callstate nil (transf_fundef f) nil m0); split. - econstructor; eauto. - apply Genv.init_mem_transf; auto. - replace (prog_main tprog) with (prog_main prog). - rewrite symbols_preserved. eauto. - reflexivity. - rewrite <- H3. apply sig_function_translated. - constructor. constructor. -Qed. - -Lemma transf_final_states: - forall st1 st2 r, - match_states st1 st2 -> final_state st1 r -> final_state st2 r. -Proof. - intros. inv H0. inv H. inv H4. constructor. -Qed. - -(** The preservation of the observable behavior of the program then - follows. *) - -Theorem transf_program_correct: - forward_simulation (RTL.semantics prog) (RTL.semantics tprog). -Proof. - eapply forward_simulation_step. - eexact symbols_preserved. - eexact transf_initial_states. - eexact transf_final_states. - exact transf_step_correct. -Qed. - -End PRESERVATION. - - diff --git a/backend/Cminor.v b/backend/Cminor.v index 45efdf9..c9ee5b5 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -216,93 +216,53 @@ Definition eval_constant (sp: val) (cst: constant) : option val := | Ointconst n => Some (Vint n) | Ofloatconst n => Some (Vfloat n) | Oaddrsymbol s ofs => - match Genv.find_symbol ge s with - | None => None - | Some b => Some (Vptr b ofs) - end - | Oaddrstack ofs => - match sp with - | Vptr b n => Some (Vptr b (Int.add n ofs)) - | _ => None - end + Some(match Genv.find_symbol ge s with + | None => Vundef + | Some b => Vptr b ofs end) + | Oaddrstack ofs => Some (Val.add sp (Vint ofs)) end. Definition eval_unop (op: unary_operation) (arg: val) : option val := - match op, arg with - | Ocast8unsigned, _ => Some (Val.zero_ext 8 arg) - | Ocast8signed, _ => Some (Val.sign_ext 8 arg) - | Ocast16unsigned, _ => Some (Val.zero_ext 16 arg) - | Ocast16signed, _ => Some (Val.sign_ext 16 arg) - | Onegint, Vint n1 => Some (Vint (Int.neg n1)) - | Onotbool, Vint n1 => Some (Val.of_bool (Int.eq n1 Int.zero)) - | Onotbool, Vptr b1 n1 => Some Vfalse - | Onotint, Vint n1 => Some (Vint (Int.not n1)) - | Onegf, Vfloat f1 => Some (Vfloat (Float.neg f1)) - | Oabsf, Vfloat f1 => Some (Vfloat (Float.abs f1)) - | Osingleoffloat, _ => Some (Val.singleoffloat arg) - | Ointoffloat, Vfloat f1 => option_map Vint (Float.intoffloat f1) - | Ointuoffloat, Vfloat f1 => option_map Vint (Float.intuoffloat f1) - | Ofloatofint, Vint n1 => Some (Vfloat (Float.floatofint n1)) - | Ofloatofintu, Vint n1 => Some (Vfloat (Float.floatofintu n1)) - | _, _ => None + match op with + | Ocast8unsigned => Some (Val.zero_ext 8 arg) + | Ocast8signed => Some (Val.sign_ext 8 arg) + | Ocast16unsigned => Some (Val.zero_ext 16 arg) + | Ocast16signed => Some (Val.sign_ext 16 arg) + | Onegint => Some (Val.negint arg) + | Onotbool => Some (Val.notbool arg) + | Onotint => Some (Val.notint arg) + | Onegf => Some (Val.negf arg) + | Oabsf => Some (Val.absf arg) + | Osingleoffloat => Some (Val.singleoffloat arg) + | Ointoffloat => Val.intoffloat arg + | Ointuoffloat => Val.intuoffloat arg + | Ofloatofint => Val.floatofint arg + | Ofloatofintu => Val.floatofintu arg end. -Definition eval_compare_mismatch (c: comparison) : option val := - match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end. - -Definition eval_compare_null (c: comparison) (n: int) : option val := - if Int.eq n Int.zero then eval_compare_mismatch c else None. - Definition eval_binop (op: binary_operation) (arg1 arg2: val) (m: mem): option val := - match op, arg1, arg2 with - | Oadd, Vint n1, Vint n2 => Some (Vint (Int.add n1 n2)) - | Oadd, Vint n1, Vptr b2 n2 => Some (Vptr b2 (Int.add n2 n1)) - | Oadd, Vptr b1 n1, Vint n2 => Some (Vptr b1 (Int.add n1 n2)) - | Osub, Vint n1, Vint n2 => Some (Vint (Int.sub n1 n2)) - | Osub, Vptr b1 n1, Vint n2 => Some (Vptr b1 (Int.sub n1 n2)) - | Osub, Vptr b1 n1, Vptr b2 n2 => - if eq_block b1 b2 then Some (Vint (Int.sub n1 n2)) else None - | Omul, Vint n1, Vint n2 => Some (Vint (Int.mul n1 n2)) - | Odiv, Vint n1, Vint n2 => - if Int.eq n2 Int.zero then None else Some (Vint (Int.divs n1 n2)) - | Odivu, Vint n1, Vint n2 => - if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2)) - | Omod, Vint n1, Vint n2 => - if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2)) - | Omodu, Vint n1, Vint n2 => - if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2)) - | Oand, Vint n1, Vint n2 => Some (Vint (Int.and n1 n2)) - | Oor, Vint n1, Vint n2 => Some (Vint (Int.or n1 n2)) - | Oxor, Vint n1, Vint n2 => Some (Vint (Int.xor n1 n2)) - | Oshl, Vint n1, Vint n2 => - if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shl n1 n2)) else None - | Oshr, Vint n1, Vint n2 => - if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None - | Oshru, Vint n1, Vint n2 => - if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None - | Oaddf, Vfloat f1, Vfloat f2 => Some (Vfloat (Float.add f1 f2)) - | Osubf, Vfloat f1, Vfloat f2 => Some (Vfloat (Float.sub f1 f2)) - | Omulf, Vfloat f1, Vfloat f2 => Some (Vfloat (Float.mul f1 f2)) - | Odivf, Vfloat f1, Vfloat f2 => Some (Vfloat (Float.div f1 f2)) - | Ocmp c, Vint n1, Vint n2 => - Some (Val.of_bool(Int.cmp c n1 n2)) - | Ocmpu c, Vint n1, Vint n2 => - Some (Val.of_bool(Int.cmpu c n1 n2)) - | Ocmpu c, Vptr b1 n1, Vptr b2 n2 => - if Mem.valid_pointer m b1 (Int.unsigned n1) - && Mem.valid_pointer m b2 (Int.unsigned n2) then - if eq_block b1 b2 - then Some(Val.of_bool(Int.cmpu c n1 n2)) - else eval_compare_mismatch c - else None - | Ocmpu c, Vptr b1 n1, Vint n2 => - eval_compare_null c n2 - | Ocmpu c, Vint n1, Vptr b2 n2 => - eval_compare_null c n1 - | Ocmpf c, Vfloat f1, Vfloat f2 => - Some (Val.of_bool (Float.cmp c f1 f2)) - | _, _, _ => None + match op with + | Oadd => Some (Val.add arg1 arg2) + | Osub => Some (Val.sub arg1 arg2) + | Omul => Some (Val.mul arg1 arg2) + | Odiv => Val.divs arg1 arg2 + | Odivu => Val.divu arg1 arg2 + | Omod => Val.mods arg1 arg2 + | Omodu => Val.modu arg1 arg2 + | Oand => Some (Val.and arg1 arg2) + | Oor => Some (Val.or arg1 arg2) + | Oxor => Some (Val.xor arg1 arg2) + | Oshl => Some (Val.shl arg1 arg2) + | Oshr => Some (Val.shr arg1 arg2) + | Oshru => Some (Val.shru arg1 arg2) + | Oaddf => Some (Val.addf arg1 arg2) + | Osubf => Some (Val.subf arg1 arg2) + | Omulf => Some (Val.mulf arg1 arg2) + | Odivf => Some (Val.divf arg1 arg2) + | Ocmp c => Some (Val.cmp c arg1 arg2) + | Ocmpu c => Some (Val.cmpu (Mem.valid_pointer m) c arg1 arg2) + | Ocmpf c => Some (Val.cmpf c arg1 arg2) end. (** Evaluation of an expression: [eval_expr ge sp e m a v] diff --git a/backend/Constprop.v b/backend/Constprop.v index 39568a3..4c303ac 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -50,14 +50,16 @@ Module Approx <: SEMILATTICE_WITH_TOP. apply Float.eq_dec. apply Int.eq_dec. apply ident_eq. + apply Int.eq_dec. Qed. Definition beq (x y: t) := if eq_dec x y then true else false. Lemma beq_correct: forall x y, beq x y = true -> x = y. Proof. unfold beq; intros. destruct (eq_dec x y). auto. congruence. Qed. - Definition ge (x y: t) : Prop := - x = Unknown \/ y = Novalue \/ x = y. + + Definition ge (x y: t) : Prop := x = Unknown \/ y = Novalue \/ x = y. + Lemma ge_refl: forall x y, eq x y -> ge x y. Proof. unfold eq, ge; tauto. @@ -165,7 +167,7 @@ Definition transf_ros (app: D.t) (ros: reg + ident) : reg + ident := match ros with | inl r => match D.get r app with - | S symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros + | G symb ofs => if Int.eq ofs Int.zero then inr _ symb else ros | _ => ros end | inr s => ros @@ -179,17 +181,19 @@ Definition transf_instr (app: D.t) (instr: instruction) := Iop (Ointconst n) nil res s | F n => Iop (Ofloatconst n) nil res s - | S symb ofs => + | G symb ofs => Iop (Oaddrsymbol symb ofs) nil res s + | S ofs => + Iop (Oaddrstack ofs) nil res s | _ => - let (op', args') := op_strength_reduction (approx_reg app) op args in + let (op', args') := op_strength_reduction op args (approx_regs app args) in Iop op' args' res s end | Iload chunk addr args dst s => - let (addr', args') := addr_strength_reduction (approx_reg app) addr args in + let (addr', args') := addr_strength_reduction addr args (approx_regs app args) in Iload chunk addr' args' dst s | Istore chunk addr args src s => - let (addr', args') := addr_strength_reduction (approx_reg app) addr args in + let (addr', args') := addr_strength_reduction addr args (approx_regs app args) in Istore chunk addr' args' src s | Icall sig ros args res s => Icall sig (transf_ros app ros) args res s @@ -200,17 +204,17 @@ Definition transf_instr (app: D.t) (instr: instruction) := | Some b => if b then Inop s1 else Inop s2 | None => - let (cond', args') := cond_strength_reduction (approx_reg app) cond args in + let (cond', args') := cond_strength_reduction cond args (approx_regs app args) in Icond cond' args' s1 s2 end | Ijumptable arg tbl => - match intval (approx_reg app) arg with - | Some n => + match approx_reg app arg with + | I n => match list_nth_z tbl (Int.unsigned n) with | Some s => Inop s | None => instr end - | None => instr + | _ => instr end | _ => instr diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 058d68e..7ac4339 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -36,9 +36,10 @@ Require Import ConstpropOpproof. Section ANALYSIS. Variable ge: genv. +Variable sp: val. Definition regs_match_approx (a: D.t) (rs: regset) : Prop := - forall r, val_match_approx ge (D.get r a) rs#r. + forall r, val_match_approx ge sp (D.get r a) rs#r. Lemma regs_match_approx_top: forall rs, regs_match_approx D.top rs. @@ -49,7 +50,7 @@ Qed. Lemma val_match_approx_increasing: forall a1 a2 v, - Approx.ge a1 a2 -> val_match_approx ge a2 v -> val_match_approx ge a1 v. + Approx.ge a1 a2 -> val_match_approx ge sp a2 v -> val_match_approx ge sp a1 v. Proof. intros until v. intros [A|[B|C]]. @@ -68,7 +69,7 @@ Qed. Lemma regs_match_approx_update: forall ra rs a v r, - val_match_approx ge a v -> + val_match_approx ge sp a v -> regs_match_approx ra rs -> regs_match_approx (D.set r a ra) (rs#r <- v). Proof. @@ -81,14 +82,13 @@ Qed. Lemma approx_regs_val_list: forall ra rs rl, regs_match_approx ra rs -> - val_list_match_approx ge (approx_regs ra rl) rs##rl. + val_list_match_approx ge sp (approx_regs ra rl) rs##rl. Proof. induction rl; simpl; intros. constructor. constructor. apply H. auto. Qed. - (** The correctness of the static analysis follows from the results of module [ConstpropOpproof] and the fact that the result of the static analysis is a solution of the forward dataflow inequations. *) @@ -178,26 +178,56 @@ Proof. intros. destruct f; reflexivity. Qed. +Definition regs_lessdef (rs1 rs2: regset) : Prop := + forall r, Val.lessdef (rs1#r) (rs2#r). + +Lemma regs_lessdef_regs: + forall rs1 rs2, regs_lessdef rs1 rs2 -> + forall rl, Val.lessdef_list rs1##rl rs2##rl. +Proof. + induction rl; constructor; auto. +Qed. + +Lemma set_reg_lessdef: + forall r v1 v2 rs1 rs2, + Val.lessdef v1 v2 -> regs_lessdef rs1 rs2 -> regs_lessdef (rs1#r <- v1) (rs2#r <- v2). +Proof. + intros; red; intros. repeat rewrite Regmap.gsspec. + destruct (peq r0 r); auto. +Qed. + +Lemma init_regs_lessdef: + forall rl vl1 vl2, + Val.lessdef_list vl1 vl2 -> + regs_lessdef (init_regs vl1 rl) (init_regs vl2 rl). +Proof. + induction rl; simpl; intros. + red; intros. rewrite Regmap.gi. auto. + inv H. red; intros. rewrite Regmap.gi. auto. + apply set_reg_lessdef; auto. +Qed. + Lemma transf_ros_correct: - forall ros rs f approx, - regs_match_approx ge approx rs -> + forall sp ros rs rs' f approx, + regs_match_approx ge sp approx rs -> find_function ge ros rs = Some f -> - find_function tge (transf_ros approx ros) rs = Some (transf_fundef f). + regs_lessdef rs rs' -> + find_function tge (transf_ros approx ros) rs' = Some (transf_fundef f). Proof. - intros until approx; intro MATCH. - destruct ros; simpl. - intro. - exploit functions_translated; eauto. intro FIND. - caseEq (D.get r approx); intros; auto. - generalize (Int.eq_spec i0 Int.zero); case (Int.eq i0 Int.zero); intros; auto. - generalize (MATCH r). rewrite H0. intros [b [A B]]. - rewrite <- symbols_preserved in A. - rewrite B in FIND. rewrite H1 in FIND. - rewrite Genv.find_funct_find_funct_ptr in FIND. - simpl. rewrite A. auto. - rewrite symbols_preserved. destruct (Genv.find_symbol ge i). - intro. apply function_ptr_translated. auto. - congruence. + intros. destruct ros; simpl in *. + generalize (H r); intro MATCH. generalize (H1 r); intro LD. + destruct (rs#r); simpl in H0; try discriminate. + destruct (Int.eq_dec i Int.zero); try discriminate. + inv LD. + assert (find_function tge (inl _ r) rs' = Some (transf_fundef f)). + simpl. rewrite <- H4. simpl. rewrite dec_eq_true. apply function_ptr_translated. auto. + destruct (D.get r approx); auto. + predSpec Int.eq Int.eq_spec i0 Int.zero; intros; auto. + simpl in *. unfold symbol_address in MATCH. rewrite symbols_preserved. + destruct (Genv.find_symbol ge i); try discriminate. + inv MATCH. apply function_ptr_translated; auto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge i); try discriminate. + apply function_ptr_translated; auto. Qed. (** The proof of semantic preservation is a simulation argument @@ -227,29 +257,37 @@ Qed. Inductive match_stackframes: stackframe -> stackframe -> Prop := match_stackframe_intro: - forall res sp pc rs f, - (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) -> + forall res sp pc rs f rs', + regs_lessdef rs rs' -> + (forall v, regs_match_approx ge sp (analyze f)!!pc (rs#res <- v)) -> match_stackframes (Stackframe res f sp pc rs) - (Stackframe res (transf_function f) sp pc rs). + (Stackframe res (transf_function f) sp pc rs'). Inductive match_states: state -> state -> Prop := | match_states_intro: - forall s sp pc rs m f s' - (MATCH: regs_match_approx ge (analyze f)!!pc rs) - (STACKS: list_forall2 match_stackframes s s'), + forall s sp pc rs m f s' rs' m' + (MATCH: regs_match_approx ge sp (analyze f)!!pc rs) + (STACKS: list_forall2 match_stackframes s s') + (REGS: regs_lessdef rs rs') + (MEM: Mem.extends m m'), match_states (State s f sp pc rs m) - (State s' (transf_function f) sp pc rs m) + (State s' (transf_function f) sp pc rs' m') | match_states_call: - forall s f args m s', - list_forall2 match_stackframes s s' -> + forall s f args m s' args' m' + (STACKS: list_forall2 match_stackframes s s') + (ARGS: Val.lessdef_list args args') + (MEM: Mem.extends m m'), match_states (Callstate s f args m) - (Callstate s' (transf_fundef f) args m) + (Callstate s' (transf_fundef f) args' m') | match_states_return: - forall s s' v m, + forall s v m s' v' m' + (STACKS: list_forall2 match_stackframes s s') + (RES: Val.lessdef v v') + (MEM: Mem.extends m m'), list_forall2 match_stackframes s s' -> match_states (Returnstate s v m) - (Returnstate s' v m). + (Returnstate s' v' m'). Ltac TransfInstr := match goal with @@ -272,7 +310,7 @@ Proof. induction 1; intros; inv MS. (* Inop *) - exists (State s' (transf_function f) sp pc' rs m); split. + exists (State s' (transf_function f) sp pc' rs' m'); split. TransfInstr; intro. eapply exec_Inop; eauto. econstructor; eauto. eapply analyze_correct_1 with (pc := pc); eauto. @@ -280,58 +318,78 @@ Proof. unfold transfer; rewrite H. auto. (* Iop *) - exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split. - TransfInstr. caseEq (op_strength_reduction (approx_reg (analyze f)!!pc) op args); - intros op' args' OSR. - assert (eval_operation tge sp op' rs##args' m = Some v). - rewrite (eval_operation_preserved _ _ symbols_preserved). - generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs m - MATCH op args v). - rewrite OSR; simpl. auto. - generalize (eval_static_operation_correct ge op sp - (approx_regs (analyze f)!!pc args) rs##args m v - (approx_regs_val_list _ _ _ args MATCH) H0). - case (eval_static_operation op (approx_regs (analyze f)!!pc args)); intros; - simpl in H2; - eapply exec_Iop; eauto; simpl. - congruence. - congruence. - elim H2; intros b [A B]. rewrite symbols_preserved. - rewrite A; rewrite B; auto. - econstructor; eauto. - eapply analyze_correct_1 with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. - eapply eval_static_operation_correct; eauto. - apply approx_regs_val_list; auto. + assert (MATCH': regs_match_approx ge sp (analyze f) # pc' rs # res <- v). + eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. + eapply eval_static_operation_correct; eauto. + apply approx_regs_val_list; auto. + TransfInstr. + exploit eval_static_operation_correct; eauto. eapply approx_regs_val_list; eauto. intros VM. + destruct (eval_static_operation op (approx_regs (analyze f) # pc args)); intros; simpl in VM. + (* Novalue *) + contradiction. + (* Unknown *) + exploit op_strength_reduction_correct. eexact MATCH. reflexivity. eauto. + destruct (op_strength_reduction op args (approx_regs (analyze f) # pc args)) as [op' args']. + intros [v' [EV' LD']]. + assert (EV'': exists v'', eval_operation ge sp op' rs'##args' m' = Some v'' /\ Val.lessdef v' v''). + eapply eval_operation_lessdef; eauto. eapply regs_lessdef_regs; eauto. + destruct EV'' as [v'' [EV'' LD'']]. + exists (State s' (transf_function f) sp pc' (rs'#res <- v'') m'); split. + econstructor. eauto. rewrite <- EV''. apply eval_operation_preserved. exact symbols_preserved. + econstructor; eauto. apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto. + (* I i *) + subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Vint i)) m'); split. + econstructor; eauto. + econstructor; eauto. apply set_reg_lessdef; auto. + (* F *) + subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Vfloat f0)) m'); split. + econstructor; eauto. + econstructor; eauto. apply set_reg_lessdef; auto. + (* G *) + subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (symbol_address tge i i0)) m'); split. + econstructor; eauto. + econstructor; eauto. apply set_reg_lessdef; auto. + unfold symbol_address. rewrite symbols_preserved; auto. + (* S *) + subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Val.add sp (Vint i))) m'); split. + econstructor; eauto. + econstructor; eauto. apply set_reg_lessdef; auto. (* Iload *) - caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args); - intros addr' args' ASR. - assert (eval_addressing tge sp addr' rs##args' = Some a). - rewrite (eval_addressing_preserved _ _ symbols_preserved). - generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs - MATCH addr args). - rewrite ASR; simpl. congruence. - TransfInstr. rewrite ASR. intro. - exists (State s' (transf_function f) sp pc' (rs#dst <- v) m); split. + TransfInstr. + generalize (addr_strength_reduction_correct ge sp (analyze f)!!pc rs + MATCH addr args (approx_regs (analyze f) # pc args) (refl_equal _)). + destruct (addr_strength_reduction addr args (approx_regs (analyze f) # pc args)) as [addr' args']. + intros P Q. rewrite H0 in P. + assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a'). + eapply eval_addressing_lessdef; eauto. eapply regs_lessdef_regs; eauto. + destruct ADDR' as [a' [A B]]. + assert (C: eval_addressing tge sp addr' rs'##args' = Some a'). + rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. + exploit Mem.loadv_extends; eauto. intros [v' [D E]]. + exists (State s' (transf_function f) sp pc' (rs'#dst <- v') m'); split. eapply exec_Iload; eauto. econstructor; eauto. eapply analyze_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. apply regs_match_approx_update; auto. simpl; auto. + apply set_reg_lessdef; auto. (* Istore *) - caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args); - intros addr' args' ASR. - assert (eval_addressing tge sp addr' rs##args' = Some a). - rewrite (eval_addressing_preserved _ _ symbols_preserved). - generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs - MATCH addr args). - rewrite ASR; simpl. congruence. - TransfInstr. rewrite ASR. intro. - exists (State s' (transf_function f) sp pc' rs m'); split. + TransfInstr. + generalize (addr_strength_reduction_correct ge sp (analyze f)!!pc rs + MATCH addr args (approx_regs (analyze f) # pc args) (refl_equal _)). + destruct (addr_strength_reduction addr args (approx_regs (analyze f) # pc args)) as [addr' args']. + intros P Q. rewrite H0 in P. + assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a'). + eapply eval_addressing_lessdef; eauto. eapply regs_lessdef_regs; eauto. + destruct ADDR' as [a' [A B]]. + assert (C: eval_addressing tge sp addr' rs'##args' = Some a'). + rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. + exploit Mem.storev_extends; eauto. intros [m2' [D E]]. + exists (State s' (transf_function f) sp pc' rs' m2'); split. eapply exec_Istore; eauto. econstructor; eauto. eapply analyze_correct_1; eauto. simpl; auto. @@ -347,17 +405,22 @@ Proof. intros. eapply analyze_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. apply regs_match_approx_update; auto. simpl. auto. + apply regs_lessdef_regs; auto. (* Itailcall *) + exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]]. exploit transf_ros_correct; eauto. intros FIND'. TransfInstr; intro. econstructor; split. eapply exec_Itailcall; eauto. apply sig_function_translated; auto. - constructor; auto. + constructor; auto. apply regs_lessdef_regs; auto. (* Ibuiltin *) + exploit external_call_mem_extends; eauto. + instantiate (1 := rs'##args). apply regs_lessdef_regs; auto. + intros [v' [m2' [A [B [C D]]]]]. TransfInstr. intro. - exists (State s' (transf_function f) sp pc' (rs#res <- v) m'); split. + exists (State s' (transf_function f) sp pc' (rs'#res <- v') m2'); split. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. @@ -365,72 +428,61 @@ Proof. eapply analyze_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. apply regs_match_approx_update; auto. simpl; auto. - - (* Icond, true *) - exists (State s' (transf_function f) sp ifso rs m); split. - caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); - intros cond' args' CSR. - assert (eval_condition cond' rs##args' m = Some true). - generalize (cond_strength_reduction_correct - ge (approx_reg (analyze f)!!pc) rs m MATCH cond args). - rewrite CSR. intro. congruence. - TransfInstr. rewrite CSR. - caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)). - intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ m _ - (approx_regs_val_list _ _ _ args MATCH) ESC); intro. - replace b with true. intro; eapply exec_Inop; eauto. congruence. - intros. eapply exec_Icond_true; eauto. - econstructor; eauto. - eapply analyze_correct_1; eauto. - simpl; auto. - unfold transfer; rewrite H; auto. - - (* Icond, false *) - exists (State s' (transf_function f) sp ifnot rs m); split. - caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); - intros cond' args' CSR. - assert (eval_condition cond' rs##args' m = Some false). - generalize (cond_strength_reduction_correct - ge (approx_reg (analyze f)!!pc) rs m MATCH cond args). - rewrite CSR. intro. congruence. - TransfInstr. rewrite CSR. - caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)). - intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ m _ - (approx_regs_val_list _ _ _ args MATCH) ESC); intro. - replace b with false. intro; eapply exec_Inop; eauto. congruence. - intros. eapply exec_Icond_false; eauto. - econstructor; eauto. - eapply analyze_correct_1; eauto. - simpl; auto. - unfold transfer; rewrite H; auto. + apply set_reg_lessdef; auto. + + (* Icond *) + TransfInstr. + generalize (cond_strength_reduction_correct ge sp (analyze f)#pc rs m + MATCH cond args (approx_regs (analyze f) # pc args) (refl_equal _)). + destruct (cond_strength_reduction cond args (approx_regs (analyze f) # pc args)) as [cond' args']. + intros EV1. + exists (State s' (transf_function f) sp (if b then ifso else ifnot) rs' m'); split. + destruct (eval_static_condition cond (approx_regs (analyze f) # pc args)) as []_eqn. + assert (eval_condition cond rs ## args m = Some b0). + eapply eval_static_condition_correct; eauto. eapply approx_regs_val_list; eauto. + assert (b = b0) by congruence. subst b0. + destruct b; eapply exec_Inop; eauto. + eapply exec_Icond; eauto. + eapply eval_condition_lessdef with (vl1 := rs##args'); eauto. eapply regs_lessdef_regs; eauto. congruence. + econstructor; eauto. + eapply analyze_correct_1; eauto. destruct b; simpl; auto. + unfold transfer; rewrite H. auto. (* Ijumptable *) - exists (State s' (transf_function f) sp pc' rs m); split. - caseEq (intval (approx_reg (analyze f)!!pc) arg); intros. - exploit intval_correct; eauto. eexact MATCH. intro VRS. - eapply exec_Inop; eauto. TransfInstr. rewrite H2. - replace i with n by congruence. rewrite H1. auto. - eapply exec_Ijumptable; eauto. TransfInstr. rewrite H2. auto. - constructor; auto. + assert (A: (fn_code (transf_function f))!pc = Some(Ijumptable arg tbl) + \/ (fn_code (transf_function f))!pc = Some(Inop pc')). + TransfInstr. destruct (approx_reg (analyze f) # pc arg) as []_eqn; auto. + generalize (MATCH arg). unfold approx_reg in Heqt. rewrite Heqt. rewrite H0. + simpl. intro EQ; inv EQ. rewrite H1. auto. + assert (B: rs'#arg = Vint n). + generalize (REGS arg); intro LD; inv LD; congruence. + exists (State s' (transf_function f) sp pc' rs' m'); split. + destruct A. eapply exec_Ijumptable; eauto. eapply exec_Inop; eauto. + econstructor; eauto. eapply analyze_correct_1; eauto. simpl. eapply list_nth_z_in; eauto. unfold transfer; rewrite H; auto. (* Ireturn *) - exists (Returnstate s' (regmap_optget or Vundef rs) m'); split. + exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]]. + exists (Returnstate s' (regmap_optget or Vundef rs') m2'); split. eapply exec_Ireturn; eauto. TransfInstr; auto. constructor; auto. + destruct or; simpl; auto. (* internal function *) + exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + intros [m2' [A B]]. simpl. unfold transf_function. econstructor; split. eapply exec_function_internal; simpl; eauto. simpl. econstructor; eauto. apply analyze_correct_3; auto. + apply init_regs_lessdef; auto. (* external function *) + exploit external_call_mem_extends; eauto. + intros [v' [m2' [A [B [C D]]]]]. simpl. econstructor; split. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. @@ -441,7 +493,7 @@ Proof. inv H3. inv H1. econstructor; split. eapply exec_return; eauto. - econstructor; eauto. + econstructor; eauto. apply set_reg_lessdef; auto. Qed. Lemma transf_initial_states: @@ -457,14 +509,14 @@ Proof. rewrite symbols_preserved. eauto. reflexivity. rewrite <- H3. apply sig_function_translated. - constructor. constructor. + constructor. constructor. constructor. apply Mem.extends_refl. Qed. Lemma transf_final_states: forall st1 st2 r, match_states st1 st2 -> final_state st1 r -> final_state st2 r. Proof. - intros. inv H0. inv H. inv H4. constructor. + intros. inv H0. inv H. inv STACKS. inv RES. constructor. Qed. (** The preservation of the observable behavior of the program then diff --git a/backend/LTL.v b/backend/LTL.v index 5ed0a8f..422b0e0 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -207,18 +207,13 @@ Inductive step: state -> trace -> state -> Prop := external_call ef ge (map rs args) m t v m' -> step (State s f sp pc rs m) t (State s f sp pc' (Locmap.set res v rs) m') - | exec_Lcond_true: - forall s f sp pc rs m cond args ifso ifnot, + | exec_Lcond: + forall s f sp pc rs m cond args ifso ifnot b pc', (fn_code f)!pc = Some(Lcond cond args ifso ifnot) -> - eval_condition cond (map rs args) m = Some true -> + eval_condition cond (map rs args) m = Some b -> + pc' = (if b then ifso else ifnot) -> step (State s f sp pc rs m) - E0 (State s f sp ifso (undef_temps rs) m) - | exec_Lcond_false: - forall s f sp pc rs m cond args ifso ifnot, - (fn_code f)!pc = Some(Lcond cond args ifso ifnot) -> - eval_condition cond (map rs args) m = Some false -> - step (State s f sp pc rs m) - E0 (State s f sp ifnot (undef_temps rs) m) + E0 (State s f sp pc' (undef_temps rs) m) | exec_Ljumptable: forall s f sp pc rs m arg tbl n pc', (fn_code f)!pc = Some(Ljumptable arg tbl) -> diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 2f96a09..50db0c6 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -629,12 +629,14 @@ Proof. traceEq. econstructor; eauto. - (* Lcond true *) + (* Lcond *) destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. simpl in EQ. subst c. + destruct b. + (* true *) assert (REACH': (reachable f)!!ifso = true). eapply reachable_successors; eauto. simpl; auto. - exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. + exploit find_label_lin_succ; eauto. inv WTI; eauto. intros [c'' AT']. destruct (starts_with ifso c'). econstructor; split. eapply plus_left'. @@ -648,10 +650,7 @@ Proof. econstructor; split. apply plus_one. eapply exec_Lcond_true; eauto. econstructor; eauto. - - (* Lcond false *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. + (* false *) assert (REACH': (reachable f)!!ifnot = true). eapply reachable_successors; eauto. simpl; auto. exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. diff --git a/backend/RTL.v b/backend/RTL.v index 10d4a3f..6a20941 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -255,18 +255,13 @@ Inductive step: state -> trace -> state -> Prop := external_call ef ge rs##args m t v m' -> step (State s f sp pc rs m) t (State s f sp pc' (rs#res <- v) m') - | exec_Icond_true: - forall s f sp pc rs m cond args ifso ifnot, + | exec_Icond: + forall s f sp pc rs m cond args ifso ifnot b pc', (fn_code f)!pc = Some(Icond cond args ifso ifnot) -> - eval_condition cond rs##args m = Some true -> + eval_condition cond rs##args m = Some b -> + pc' = (if b then ifso else ifnot) -> step (State s f sp pc rs m) - E0 (State s f sp ifso rs m) - | exec_Icond_false: - forall s f sp pc rs m cond args ifso ifnot, - (fn_code f)!pc = Some(Icond cond args ifso ifnot) -> - eval_condition cond rs##args m = Some false -> - step (State s f sp pc rs m) - E0 (State s f sp ifnot rs m) + E0 (State s f sp pc' rs m) | exec_Ijumptable: forall s f sp pc rs m arg tbl n pc', (fn_code f)!pc = Some(Ijumptable arg tbl) -> diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 55cdd6b..c5182db 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -427,22 +427,22 @@ Proof. (* ifeq *) caseEq (Int.eq i key); intro EQ; rewrite EQ in H5. inv H5. exists nfound; exists rs; intuition. - apply star_one. eapply exec_Icond_true; eauto. - simpl. rewrite H2. congruence. + apply star_one. eapply exec_Icond with (b := true); eauto. + simpl. rewrite H2. simpl. congruence. exploit IHtr_switch; eauto. intros [nd1 [rs1 [EX [NTH ME]]]]. exists nd1; exists rs1; intuition. - eapply star_step. eapply exec_Icond_false; eauto. - simpl. rewrite H2. congruence. eexact EX. traceEq. + eapply star_step. eapply exec_Icond with (b := false); eauto. + simpl. rewrite H2. simpl. congruence. eexact EX. traceEq. (* iflt *) caseEq (Int.ltu i key); intro EQ; rewrite EQ in H5. exploit IHtr_switch1; eauto. intros [nd1 [rs1 [EX [NTH ME]]]]. exists nd1; exists rs1; intuition. - eapply star_step. eapply exec_Icond_true; eauto. - simpl. rewrite H2. congruence. eexact EX. traceEq. + eapply star_step. eapply exec_Icond with (b := true); eauto. + simpl. rewrite H2. simpl. congruence. eexact EX. traceEq. exploit IHtr_switch2; eauto. intros [nd1 [rs1 [EX [NTH ME]]]]. exists nd1; exists rs1; intuition. - eapply star_step. eapply exec_Icond_false; eauto. - simpl. rewrite H2. congruence. eexact EX. traceEq. + eapply star_step. eapply exec_Icond with (b := false); eauto. + simpl. rewrite H2. simpl. congruence. eexact EX. traceEq. (* jumptable *) set (rs1 := rs#rt <- (Vint(Int.sub i ofs))). assert (ME1: match_env map e nil rs1). @@ -451,21 +451,21 @@ Proof. eapply exec_Iop; eauto. predSpec Int.eq Int.eq_spec ofs Int.zero; simpl. rewrite H10. rewrite Int.sub_zero_l. congruence. - rewrite H6. rewrite <- Int.sub_add_opp. auto. + rewrite H6. simpl. rewrite <- Int.sub_add_opp. auto. caseEq (Int.ltu (Int.sub i ofs) sz); intro EQ; rewrite EQ in H9. exploit H5; eauto. intros [nd [A B]]. exists nd; exists rs1; intuition. eapply star_step. eexact EX1. - eapply star_step. eapply exec_Icond_true; eauto. - simpl. unfold rs1. rewrite Regmap.gss. congruence. + eapply star_step. eapply exec_Icond with (b := true); eauto. + simpl. unfold rs1. rewrite Regmap.gss. simpl. congruence. apply star_one. eapply exec_Ijumptable; eauto. unfold rs1. apply Regmap.gss. reflexivity. traceEq. exploit (IHtr_switch rs1); eauto. unfold rs1. rewrite Regmap.gso; auto. intros [nd [rs' [EX [NTH ME]]]]. exists nd; exists rs'; intuition. eapply star_step. eexact EX1. - eapply star_step. eapply exec_Icond_false; eauto. - simpl. unfold rs1. rewrite Regmap.gss. congruence. + eapply star_step. eapply exec_Icond with (b := false); eauto. + simpl. unfold rs1. rewrite Regmap.gss. simpl. congruence. eexact EX. reflexivity. traceEq. Qed. @@ -739,11 +739,8 @@ Proof. exists rs1. (* Exec *) split. eapply star_right. eexact EX1. - destruct b. - eapply exec_Icond_true; eauto. - rewrite RES1. assumption. - eapply exec_Icond_false; eauto. - rewrite RES1. assumption. + eapply exec_Icond with (b := b); eauto. + rewrite RES1. auto. traceEq. (* Match-env *) split. assumption. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 02359b9..65506c8 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -565,7 +565,6 @@ Proof. rewrite H6. eapply external_call_well_typed; eauto. (* Icond *) econstructor; eauto. - econstructor; eauto. (* Ijumptable *) econstructor; eauto. (* Ireturn *) diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 6ee9263..75c7dad 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -1154,7 +1154,7 @@ Proof. eapply star_right. eauto. eapply exec_Lstore with (a := ta); eauto. simpl reglist. rewrite G. unfold ls3. rewrite Locmap.gss. simpl. - destruct ta; simpl in Y; try discriminate. rewrite Int.add_zero. auto. + destruct ta; simpl in Y; try discriminate. simpl; rewrite Int.add_zero; auto. reflexivity. reflexivity. traceEq. econstructor; eauto with coqlib. apply agree_undef_temps2. apply agree_exten with ls; auto. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index d6c850a..54d59b1 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -147,8 +147,9 @@ Proof. inv H0. simpl in H7. assert (eval_condition c vl m = Some b). - destruct (eval_condition c vl m); try discriminate. + destruct (eval_condition c vl m). destruct b0; inv H7; inversion H1; congruence. + inv H7. inv H1. assert (eval_condexpr ge sp e m le (CEcond c e0) b). eapply eval_CEcond; eauto. destruct e0; auto. destruct e1; auto. @@ -204,7 +205,7 @@ Lemma eval_sel_unop: forall le op a1 v1 v, eval_expr ge sp e m le a1 v1 -> eval_unop op v1 = Some v -> - eval_expr ge sp e m le (sel_unop op a1) v. + exists v', eval_expr ge sp e m le (sel_unop op a1) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_cast8unsigned; auto. @@ -212,19 +213,15 @@ Proof. apply eval_cast16unsigned; auto. apply eval_cast16signed; auto. apply eval_negint; auto. - generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intro. - change true with (negb false). eapply eval_notbool; eauto. subst i; constructor. - change false with (negb true). eapply eval_notbool; eauto. constructor; auto. - change Vfalse with (Val.of_bool (negb true)). - eapply eval_notbool; eauto. constructor. + apply eval_notbool; auto. apply eval_notint; auto. apply eval_negf; auto. apply eval_absf; auto. apply eval_singleoffloat; auto. - remember (Float.intoffloat f) as oi; destruct oi; inv H0. eapply eval_intoffloat; eauto. - remember (Float.intuoffloat f) as oi; destruct oi; inv H0. eapply eval_intuoffloat; eauto. - apply eval_floatofint; auto. - apply eval_floatofintu; auto. + eapply eval_intoffloat; eauto. + eapply eval_intuoffloat; eauto. + eapply eval_floatofint; eauto. + eapply eval_floatofintu; eauto. Qed. Lemma eval_sel_binop: @@ -232,48 +229,29 @@ Lemma eval_sel_binop: eval_expr ge sp e m le a1 v1 -> eval_expr ge sp e m le a2 v2 -> eval_binop op v1 v2 m = Some v -> - eval_expr ge sp e m le (sel_binop op a1 a2) v. + exists v', eval_expr ge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_add; auto. - apply eval_add_ptr_2; auto. - apply eval_add_ptr; auto. apply eval_sub; auto. - apply eval_sub_ptr_int; auto. - destruct (eq_block b b0); inv H1. - eapply eval_sub_ptr_ptr; eauto. - apply eval_mul; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_divs; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_divu; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_mods; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_modu; eauto. + apply eval_mul; auto. + eapply eval_divs; eauto. + eapply eval_divu; eauto. + eapply eval_mods; eauto. + eapply eval_modu; eauto. apply eval_and; auto. apply eval_or; auto. apply eval_xor; auto. - caseEq (Int.ltu i0 Int.iwordsize); intro; rewrite H2 in H1; inv H1. apply eval_shl; auto. - caseEq (Int.ltu i0 Int.iwordsize); intro; rewrite H2 in H1; inv H1. apply eval_shr; auto. - caseEq (Int.ltu i0 Int.iwordsize); intro; rewrite H2 in H1; inv H1. apply eval_shru; auto. apply eval_addf; auto. apply eval_subf; auto. apply eval_mulf; auto. apply eval_divf; auto. apply eval_comp; auto. - eapply eval_compu_int; eauto. - eapply eval_compu_int_ptr; eauto. - eapply eval_compu_ptr_int; eauto. - destruct (Mem.valid_pointer m b (Int.unsigned i) && - Mem.valid_pointer m b0 (Int.unsigned i0)) as [] _eqn; try congruence. - destruct (eq_block b b0); inv H1. - eapply eval_compu_ptr_ptr; eauto. - eapply eval_compu_ptr_ptr_2; eauto. - eapply eval_compf; eauto. + apply eval_compu; auto. + apply eval_compf; auto. Qed. End CMCONSTR. @@ -303,11 +281,46 @@ Proof. exploit expr_is_addrof_ident_correct; eauto. intro EQ; subst a. inv H1. inv H4. destruct (Genv.find_symbol ge i); try congruence. - inv H3. rewrite Genv.find_funct_find_funct_ptr in H2. rewrite H2 in H0. + rewrite Genv.find_funct_find_funct_ptr in H2. rewrite H2 in H0. destruct fd; try congruence. destruct (ef_inline e0); congruence. Qed. +(** Compatibility of evaluation functions with the "less defined than" relation. *) + +Ltac TrivialExists := + match goal with + | [ |- exists v, Some ?x = Some v /\ _ ] => exists x; split; auto + | _ => idtac + end. + +Lemma eval_unop_lessdef: + forall op v1 v1' v, + eval_unop op v1 = Some v -> Val.lessdef v1 v1' -> + exists v', eval_unop op v1' = Some v' /\ Val.lessdef v v'. +Proof. + intros until v; intros EV LD. inv LD. + exists v; auto. + destruct op; simpl in *; inv EV; TrivialExists. +Qed. + +Lemma eval_binop_lessdef: + forall op v1 v1' v2 v2' v m m', + eval_binop op v1 v2 m = Some v -> + Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Mem.extends m m' -> + exists v', eval_binop op v1' v2' m' = Some v' /\ Val.lessdef v v'. +Proof. + intros until m'; intros EV LD1 LD2 ME. + assert (exists v', eval_binop op v1' v2' m = Some v' /\ Val.lessdef v v'). + inv LD1. inv LD2. exists v; auto. + destruct op; destruct v1'; simpl in *; inv EV; TrivialExists. + destruct op; simpl in *; inv EV; TrivialExists. + destruct op; try (exact H). + simpl in *. TrivialExists. inv EV. apply Val.of_optbool_lessdef. + intros. apply Val.cmpu_bool_lessdef with (Mem.valid_pointer m) v1 v2; auto. + intros; eapply Mem.valid_pointer_extends; eauto. +Qed. + (** * Semantic preservation for instruction selection. *) Section PRESERVATION. @@ -318,7 +331,7 @@ Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. (** Relationship between the global environments for the original - CminorSel program and the generated RTL program. *) + Cminor program and the generated CminorSel program. *) Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -327,15 +340,6 @@ Proof. apply Genv.find_symbol_transf. Qed. -Lemma functions_translated: - forall (v: val) (f: Cminor.fundef), - Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (sel_fundef ge f). -Proof. - intros. - exact (Genv.find_funct_transf (sel_fundef ge) _ _ H). -Qed. - Lemma function_ptr_translated: forall (b: block) (f: Cminor.fundef), Genv.find_funct_ptr ge b = Some f -> @@ -345,6 +349,17 @@ Proof. exact (Genv.find_funct_ptr_transf (sel_fundef ge) _ _ H). Qed. +Lemma functions_translated: + forall (v v': val) (f: Cminor.fundef), + Genv.find_funct ge v = Some f -> + Val.lessdef v v' -> + Genv.find_funct tge v' = Some (sel_fundef ge f). +Proof. + intros. inv H0. + exact (Genv.find_funct_transf (sel_fundef ge) _ _ H). + simpl in H. discriminate. +Qed. + Lemma sig_function_translated: forall f, funsig (sel_fundef ge f) = Cminor.funsig f. @@ -359,113 +374,189 @@ Proof. apply Genv.find_var_info_transf. Qed. +(** Relationship between the local environments. *) + +Definition env_lessdef (e1 e2: env) : Prop := + forall id v1, e1!id = Some v1 -> exists v2, e2!id = Some v2 /\ Val.lessdef v1 v2. + +Lemma set_var_lessdef: + forall e1 e2 id v1 v2, + env_lessdef e1 e2 -> Val.lessdef v1 v2 -> + env_lessdef (PTree.set id v1 e1) (PTree.set id v2 e2). +Proof. + intros; red; intros. rewrite PTree.gsspec in *. destruct (peq id0 id). + exists v2; split; congruence. + auto. +Qed. + +Lemma set_params_lessdef: + forall il vl1 vl2, + Val.lessdef_list vl1 vl2 -> + env_lessdef (set_params vl1 il) (set_params vl2 il). +Proof. + induction il; simpl; intros. + red; intros. rewrite PTree.gempty in H0; congruence. + inv H; apply set_var_lessdef; auto. +Qed. + +Lemma set_locals_lessdef: + forall e1 e2, env_lessdef e1 e2 -> + forall il, env_lessdef (set_locals il e1) (set_locals il e2). +Proof. + induction il; simpl. auto. apply set_var_lessdef; auto. +Qed. + (** Semantic preservation for expressions. *) Lemma sel_expr_correct: forall sp e m a v, Cminor.eval_expr ge sp e m a v -> - forall le, - eval_expr tge sp e m le (sel_expr a) v. + forall e' le m', + env_lessdef e e' -> Mem.extends m m' -> + exists v', eval_expr tge sp e' m' le (sel_expr a) v' /\ Val.lessdef v v'. Proof. induction 1; intros; simpl. (* Evar *) - constructor; auto. + exploit H0; eauto. intros [v' [A B]]. exists v'; split; auto. constructor; auto. (* Econst *) - destruct cst; simpl; simpl in H; (econstructor; [constructor|simpl;auto]). - rewrite symbols_preserved. auto. + destruct cst; simpl in *; inv H. + exists (Vint i); split; auto. econstructor. constructor. auto. + exists (Vfloat f); split; auto. econstructor. constructor. auto. + rewrite <- symbols_preserved. fold (symbol_address tge i i0). apply eval_addrsymbol. + apply eval_addrstack. (* Eunop *) - eapply eval_sel_unop; eauto. + exploit IHeval_expr; eauto. intros [v1' [A B]]. + exploit eval_unop_lessdef; eauto. intros [v' [C D]]. + exploit eval_sel_unop; eauto. intros [v'' [E F]]. + exists v''; split; eauto. eapply Val.lessdef_trans; eauto. (* Ebinop *) - eapply eval_sel_binop; eauto. + exploit IHeval_expr1; eauto. intros [v1' [A B]]. + exploit IHeval_expr2; eauto. intros [v2' [C D]]. + exploit eval_binop_lessdef; eauto. intros [v' [E F]]. + exploit eval_sel_binop. eexact A. eexact C. eauto. intros [v'' [P Q]]. + exists v''; split; eauto. eapply Val.lessdef_trans; eauto. (* Eload *) - eapply eval_load; eauto. + exploit IHeval_expr; eauto. intros [vaddr' [A B]]. + exploit Mem.loadv_extends; eauto. intros [v' [C D]]. + exists v'; split; auto. eapply eval_load; eauto. (* Econdition *) + exploit IHeval_expr1; eauto. intros [v1' [A B]]. + exploit IHeval_expr2; eauto. intros [v2' [C D]]. + replace (sel_expr (if b1 then a2 else a3)) with (if b1 then sel_expr a2 else sel_expr a3) in C. + assert (Val.bool_of_val v1' b1). inv B. auto. inv H0. + exists v2'; split; auto. econstructor; eauto. eapply eval_condition_of_expr; eauto. destruct b1; auto. Qed. -Hint Resolve sel_expr_correct: evalexpr. - Lemma sel_exprlist_correct: forall sp e m a v, Cminor.eval_exprlist ge sp e m a v -> - forall le, - eval_exprlist tge sp e m le (sel_exprlist a) v. + forall e' le m', + env_lessdef e e' -> Mem.extends m m' -> + exists v', eval_exprlist tge sp e' m' le (sel_exprlist a) v' /\ Val.lessdef_list v v'. Proof. - induction 1; intros; simpl; constructor; auto with evalexpr. + induction 1; intros; simpl. + exists (@nil val); split; auto. constructor. + exploit sel_expr_correct; eauto. intros [v1' [A B]]. + exploit IHeval_exprlist; eauto. intros [vl' [C D]]. + exists (v1' :: vl'); split; auto. constructor; eauto. Qed. -Hint Resolve sel_exprlist_correct: evalexpr. - -(** Semantic preservation for terminating function calls and statements. *) - -Fixpoint sel_cont (k: Cminor.cont) : CminorSel.cont := - match k with - | Cminor.Kstop => Kstop - | Cminor.Kseq s1 k1 => Kseq (sel_stmt ge s1) (sel_cont k1) - | Cminor.Kblock k1 => Kblock (sel_cont k1) - | Cminor.Kcall id f sp e k1 => - Kcall id (sel_function ge f) sp e (sel_cont k1) - end. +(** Semantic preservation for functions and statements. *) + +Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop := + | match_cont_stop: + match_cont Cminor.Kstop Kstop + | match_cont_seq: forall s k k', + match_cont k k' -> + match_cont (Cminor.Kseq s k) (Kseq (sel_stmt ge s) k') + | match_cont_block: forall k k', + match_cont k k' -> + match_cont (Cminor.Kblock k) (Kblock k') + | match_cont_call: forall id f sp e k e' k', + match_cont k k' -> env_lessdef e e' -> + match_cont (Cminor.Kcall id f sp e k) (Kcall id (sel_function ge f) sp e' k'). Inductive match_states: Cminor.state -> CminorSel.state -> Prop := - | match_state: forall f s k s' k' sp e m, + | match_state: forall f s k s' k' sp e m e' m', s' = sel_stmt ge s -> - k' = sel_cont k -> + match_cont k k' -> + env_lessdef e e' -> + Mem.extends m m' -> match_states (Cminor.State f s k sp e m) - (State (sel_function ge f) s' k' sp e m) - | match_callstate: forall f args k k' m, - k' = sel_cont k -> + (State (sel_function ge f) s' k' sp e' m') + | match_callstate: forall f args args' k k' m m', + match_cont k k' -> + Val.lessdef_list args args' -> + Mem.extends m m' -> match_states (Cminor.Callstate f args k m) - (Callstate (sel_fundef ge f) args k' m) - | match_returnstate: forall v k k' m, - k' = sel_cont k -> + (Callstate (sel_fundef ge f) args' k' m') + | match_returnstate: forall v v' k k' m m', + match_cont k k' -> + Val.lessdef v v' -> + Mem.extends m m' -> match_states (Cminor.Returnstate v k m) - (Returnstate v k' m) - | match_builtin_1: forall ef args optid f sp e k m al k', - k' = sel_cont k -> - eval_exprlist tge sp e m nil al args -> + (Returnstate v' k' m') + | match_builtin_1: forall ef args args' optid f sp e k m al e' k' m', + match_cont k k' -> + Val.lessdef_list args args' -> + env_lessdef e e' -> + Mem.extends m m' -> + eval_exprlist tge sp e' m' nil al args' -> match_states (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m) - (State (sel_function ge f) (Sbuiltin optid ef al) k' sp e m) - | match_builtin_2: forall v optid f sp e k m k', - k' = sel_cont k -> + (State (sel_function ge f) (Sbuiltin optid ef al) k' sp e' m') + | match_builtin_2: forall v v' optid f sp e k m e' m' k', + match_cont k k' -> + Val.lessdef v v' -> + env_lessdef e e' -> + Mem.extends m m' -> match_states (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m) - (State (sel_function ge f) Sskip k' sp (set_optvar optid v e) m). + (State (sel_function ge f) Sskip k' sp (set_optvar optid v' e') m'). Remark call_cont_commut: - forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k). + forall k k', match_cont k k' -> match_cont (Cminor.call_cont k) (call_cont k'). Proof. - induction k; simpl; auto. + induction 1; simpl; auto. constructor. constructor; auto. Qed. Remark find_label_commut: - forall lbl s k, - find_label lbl (sel_stmt ge s) (sel_cont k) = - option_map (fun sk => (sel_stmt ge (fst sk), sel_cont (snd sk))) - (Cminor.find_label lbl s k). + forall lbl s k k', + match_cont k k' -> + match Cminor.find_label lbl s k, find_label lbl (sel_stmt ge s) k' with + | None, None => True + | Some(s1, k1), Some(s1', k1') => s1' = sel_stmt ge s1 /\ match_cont k1 k1' + | _, _ => False + end. Proof. induction s; intros; simpl; auto. - unfold store. destruct (addressing m (sel_expr e)); auto. - destruct (expr_is_addrof_builtin ge e); auto. - change (Kseq (sel_stmt ge s2) (sel_cont k)) - with (sel_cont (Cminor.Kseq s2 k)). - rewrite IHs1. rewrite IHs2. - destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)); auto. - rewrite IHs1. rewrite IHs2. - destruct (Cminor.find_label lbl s1 k); auto. - change (Kseq (Sloop (sel_stmt ge s)) (sel_cont k)) - with (sel_cont (Cminor.Kseq (Cminor.Sloop s) k)). - auto. - change (Kblock (sel_cont k)) - with (sel_cont (Cminor.Kblock k)). - auto. - destruct o; auto. - destruct (ident_eq lbl l); auto. +(* store *) + unfold store. destruct (addressing m (sel_expr e)); simpl; auto. +(* call *) + destruct (expr_is_addrof_builtin ge e); simpl; auto. +(* seq *) + exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. + destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ]; + destruct (find_label lbl (sel_stmt ge s1) (Kseq (sel_stmt ge s2) k')) as [[sy ky] | ]; + intuition. apply IHs2; auto. +(* ifthenelse *) + exploit (IHs1 k); eauto. + destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ]; + destruct (find_label lbl (sel_stmt ge s1) k') as [[sy ky] | ]; + intuition. apply IHs2; auto. +(* loop *) + apply IHs. constructor; auto. +(* block *) + apply IHs. constructor; auto. +(* return *) + destruct o; simpl; auto. +(* label *) + destruct (ident_eq lbl l). auto. apply IHs; auto. Qed. Definition measure (s: Cminor.state) : nat := @@ -481,66 +572,125 @@ Lemma sel_step_correct: (exists T2, step tge T1 t T2 /\ match_states S2 T2) \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat. Proof. - induction 1; intros T1 ME; inv ME; simpl; - try (left; econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail). - + induction 1; intros T1 ME; inv ME; simpl. + (* skip seq *) + inv H7. left; econstructor; split. econstructor. constructor; auto. + (* skip block *) + inv H7. left; econstructor; split. econstructor. constructor; auto. (* skip call *) + exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]]. left; econstructor; split. - econstructor. destruct k; simpl in H; simpl; auto. + econstructor. inv H10; simpl in H; simpl; auto. rewrite <- H0; reflexivity. - simpl. eauto. + eauto. constructor; auto. + (* assign *) + exploit sel_expr_correct; eauto. intros [v' [A B]]. + left; econstructor; split. + econstructor; eauto. + constructor; auto. apply set_var_lessdef; auto. (* store *) + exploit sel_expr_correct. eexact H. eauto. eauto. intros [vaddr' [A B]]. + exploit sel_expr_correct. eexact H0. eauto. eauto. intros [v' [C D]]. + exploit Mem.storev_extends; eauto. intros [m2' [P Q]]. left; econstructor; split. - eapply eval_store; eauto with evalexpr. + eapply eval_store; eauto. constructor; auto. (* Scall *) - case_eq (expr_is_addrof_builtin ge a). + exploit sel_expr_correct; eauto. intros [vf' [A B]]. + exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. + destruct (expr_is_addrof_builtin ge a) as [ef|]_eqn. (* Scall turned into Sbuiltin *) - intros ef EQ. exploit expr_is_addrof_builtin_correct; eauto. intro EQ1. subst fd. + exploit expr_is_addrof_builtin_correct; eauto. intro EQ1. subst fd. right; split. omega. split. auto. - econstructor; eauto with evalexpr. + econstructor; eauto. (* Scall preserved *) - intro EQ. left; econstructor; split. - econstructor; eauto with evalexpr. - apply functions_translated; eauto. + left; econstructor; split. + econstructor; eauto. + eapply functions_translated; eauto. apply sig_function_translated. - constructor; auto. + constructor; auto. constructor; auto. (* Stailcall *) + exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. + exploit sel_expr_correct; eauto. intros [vf' [A B]]. + exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. left; econstructor; split. - econstructor; eauto with evalexpr. - apply functions_translated; eauto. + econstructor; eauto. + eapply functions_translated; eauto. apply sig_function_translated. - constructor; auto. apply call_cont_commut. + constructor; auto. apply call_cont_commut; auto. + (* Seq *) + left; econstructor; split. constructor. constructor; auto. constructor; auto. (* Sifthenelse *) - left; exists (State (sel_function ge f) (if b then sel_stmt ge s1 else sel_stmt ge s2) (sel_cont k) sp e m); split. - constructor. eapply eval_condition_of_expr; eauto with evalexpr. + exploit sel_expr_correct; eauto. intros [v' [A B]]. + assert (Val.bool_of_val v' b). inv B. auto. inv H0. + left; exists (State (sel_function ge f) (if b then sel_stmt ge s1 else sel_stmt ge s2) k' sp e' m'); split. + constructor. eapply eval_condition_of_expr; eauto. constructor; auto. destruct b; auto. + (* Sloop *) + left; econstructor; split. constructor. constructor; auto. constructor; auto. + (* Sblock *) + left; econstructor; split. constructor. constructor; auto. constructor; auto. + (* Sexit seq *) + inv H7. left; econstructor; split. constructor. constructor; auto. + (* Sexit0 block *) + inv H7. left; econstructor; split. constructor. constructor; auto. + (* SexitS block *) + inv H7. left; econstructor; split. constructor. constructor; auto. + (* Sswitch *) + exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B. + left; econstructor; split. econstructor; eauto. constructor; auto. (* Sreturn None *) + exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. left; econstructor; split. econstructor. simpl; eauto. - constructor; auto. apply call_cont_commut. + constructor; auto. apply call_cont_commut; auto. (* Sreturn Some *) + exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. + exploit sel_expr_correct; eauto. intros [v' [A B]]. left; econstructor; split. - econstructor. simpl. eauto with evalexpr. simpl; eauto. - constructor; auto. apply call_cont_commut. + econstructor; eauto. + constructor; auto. apply call_cont_commut; auto. + (* Slabel *) + left; econstructor; split. constructor. constructor; auto. (* Sgoto *) + exploit (find_label_commut lbl (Cminor.fn_body f) (Cminor.call_cont k)). + apply call_cont_commut; eauto. + rewrite H. + destruct (find_label lbl (sel_stmt ge (Cminor.fn_body f)) (call_cont k'0)) + as [[s'' k'']|]_eqn; intros; try contradiction. + destruct H0. left; econstructor; split. - econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut. - rewrite H. simpl. reflexivity. + econstructor; eauto. constructor; auto. + (* internal function *) + exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + intros [m2' [A B]]. + left; econstructor; split. + econstructor; eauto. + constructor; auto. apply set_locals_lessdef. apply set_params_lessdef; auto. (* external call *) + exploit external_call_mem_extends; eauto. + intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. constructor; auto. (* external call turned into a Sbuiltin *) + exploit external_call_mem_extends; eauto. + intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. constructor; auto. + (* return *) + inv H2. + left; econstructor; split. + econstructor. + constructor; auto. destruct optid; simpl; auto. apply set_var_lessdef; auto. (* return of an external call turned into a Sbuiltin *) - right; split. omega. split. auto. constructor; auto. + right; split. omega. split. auto. constructor; auto. + destruct optid; simpl; auto. apply set_var_lessdef; auto. Qed. Lemma sel_initial_states: @@ -554,14 +704,14 @@ Proof. simpl. fold tge. rewrite symbols_preserved. eexact H0. apply function_ptr_translated. eauto. rewrite <- H2. apply sig_function_translated; auto. - constructor; auto. + constructor; auto. constructor. apply Mem.extends_refl. Qed. Lemma sel_final_states: forall S R r, match_states S R -> Cminor.final_state S r -> final_state R r. Proof. - intros. inv H0. inv H. simpl. constructor. + intros. inv H0. inv H. inv H3. inv H5. constructor. Qed. Theorem transf_program_correct: diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index f3dd9ed..02a6ca9 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -508,17 +508,10 @@ Proof. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. apply regset_set; auto. -(* cond true *) +(* cond *) TransfInstr. - left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifso rs' m'); split. - eapply exec_Icond_true; eauto. - apply eval_condition_lessdef with (rs##args) m; auto. apply regset_get_list; auto. - constructor; auto. - -(* cond false *) - TransfInstr. - left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifnot rs' m'); split. - eapply exec_Icond_false; eauto. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) (if b then ifso else ifnot) rs' m'); split. + eapply exec_Icond; eauto. apply eval_condition_lessdef with (rs##args) m; auto. apply regset_get_list; auto. constructor; auto. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 8ff7347..d589260 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -319,14 +319,9 @@ Proof. (* cond *) generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. - eapply exec_Lcond_true; eauto. + eapply exec_Lcond; eauto. rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto. - econstructor; eauto. - generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. - left; econstructor; split. - eapply exec_Lcond_false; eauto. - rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto. - econstructor; eauto. + destruct b; econstructor; eauto. (* jumptable *) generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. |