diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-08-18 09:06:55 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-08-18 09:06:55 +0000 |
commit | a15858a0a8fcea82db02fe8c9bd2ed912210419f (patch) | |
tree | 5c0c19439f0d0f9e8873ce0dad2034cb9cafc4ba /backend | |
parent | adedca3a1ff17ff8ac66eb2bcd533a50df0927a0 (diff) | |
download | compcert-a15858a0a8fcea82db02fe8c9bd2ed912210419f.tar.gz compcert-a15858a0a8fcea82db02fe8c9bd2ed912210419f.zip |
Merge of branches/full-expr-4:
- Csyntax, Csem: source C language has side-effects within expressions,
performs implicit casts, and has nondeterministic reduction semantics
for expressions
- Cstrategy: deterministic red. sem. for the above
- Clight: the previous source C language, with pure expressions.
Added: temporary variables + implicit casts.
- New pass SimplExpr to pull side-effects out of expressions
(previously done in untrusted Caml code in cparser/)
- Csharpminor: added temporary variables to match Clight.
- Cminorgen: adapted, removed cast optimization (moved to back-end)
- CastOptim: RTL-level optimization of casts
- cparser: transformations Bitfields, StructByValue and StructAssign
now work on non-simplified expressions
- Added pretty-printers for several intermediate languages,
and matching -dxxx command-line flags.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CastOptim.v | 276 | ||||
-rw-r--r-- | backend/CastOptimproof.v | 577 | ||||
-rw-r--r-- | backend/Coloringaux.ml | 27 | ||||
-rw-r--r-- | backend/PrintCminor.ml | 285 | ||||
-rw-r--r-- | backend/PrintLTLin.ml | 130 | ||||
-rw-r--r-- | backend/PrintRTL.ml | 59 | ||||
-rw-r--r-- | backend/RTLgen.v | 40 | ||||
-rw-r--r-- | backend/RTLgenproof.v | 74 | ||||
-rw-r--r-- | backend/RTLgenspec.v | 104 |
9 files changed, 1404 insertions, 168 deletions
diff --git a/backend/CastOptim.v b/backend/CastOptim.v new file mode 100644 index 00000000..3ae5ab0b --- /dev/null +++ b/backend/CastOptim.v @@ -0,0 +1,276 @@ +(* *********************************************************************) +(* *) +(* 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 lub_commut: forall x y, eq (lub x y) (lub y x). + Proof. + unfold lub, eq; intros. + destruct x; destruct y; auto. + Qed. + Lemma ge_lub_left: forall x y, ge (lub x y) x. + 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 new file mode 100644 index 00000000..60b10c2c --- /dev/null +++ b/backend/CastOptimproof.v @@ -0,0 +1,577 @@ +(* *********************************************************************) +(* *) +(* 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.gmap. 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 v, + regs_match_approx app rs -> + eval_operation ge sp op rs##args = 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; 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 v, + regs_match_approx app rs -> + eval_operation ge sp op rs##args = Some v -> + eval_operation ge sp (transf_operation op (approx_regs app args)) rs##args = 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; eauto. + rewrite <- H0. apply eval_addressing_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_of_chunk_correct; eauto. + + (* Istore *) + econstructor; split. + TransfInstr; intro. eapply exec_Istore; eauto. + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + 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, using the generic preservation theorem + [Smallstep.simulation_step_preservation]. *) + +Theorem transf_program_correct: + forall (beh: program_behavior), not_wrong beh -> + exec_program prog beh -> exec_program tprog beh. +Proof. + unfold exec_program; intros. + eapply simulation_step_preservation; eauto. + eexact transf_initial_states. + eexact transf_final_states. + exact transf_step_correct. +Qed. + +End PRESERVATION. + + diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml index 63f21906..922506f0 100644 --- a/backend/Coloringaux.ml +++ b/backend/Coloringaux.ml @@ -39,6 +39,7 @@ open Conventions type node = { ident: int; (*r unique identifier *) typ: typ; (*r its type *) + regname: reg option; (*r the RTL register it comes from *) regclass: int; (*r identifier of register class *) mutable spillcost: float; (*r estimated cost of spilling *) mutable adjlist: node list; (*r all nodes it interferes with *) @@ -84,14 +85,15 @@ and movestate = (*i let name_of_node n = - match n.color with - | Some(R r) -> + match n.color, n.regname with + | Some(R r), _ -> begin match Machregsaux.name_of_register r with | None -> "fixed-reg" | Some s -> s end - | Some(S _) -> "fixed-slot" - | None -> string_of_int n.ident + | Some(S _), _ -> "fixed-slot" + | None, Some r -> Printf.sprintf "x%ld" (camlint_of_positive r) + | None, None -> "unknown-reg" *) (* The algorithm manipulates partitions of the nodes and of the moves @@ -106,7 +108,7 @@ module DLinkNode = struct type t = node let make state = let rec empty = - { ident = 0; typ = Tint; regclass = 0; + { ident = 0; typ = Tint; regname = None; regclass = 0; adjlist = []; degree = 0; spillcost = 0.0; movelist = []; alias = None; color = None; nstate = state; nprev = empty; nnext = empty } @@ -363,7 +365,8 @@ let checkInvariants () = let nodeOfReg r typenv spillcosts = let ty = typenv r in incr nextRegIdent; - { ident = !nextRegIdent; typ = ty; regclass = class_of_type ty; + { ident = !nextRegIdent; typ = ty; + regname = Some r; regclass = class_of_type ty; spillcost = float(spillcosts r); adjlist = []; degree = 0; movelist = []; alias = None; color = None; @@ -373,7 +376,8 @@ let nodeOfReg r typenv spillcosts = let nodeOfMreg mr = let ty = mreg_type mr in incr nextRegIdent; - { ident = !nextRegIdent; typ = ty; regclass = class_of_type ty; + { ident = !nextRegIdent; typ = ty; + regname = None; regclass = class_of_type ty; spillcost = 0.0; adjlist = []; degree = 0; movelist = []; alias = None; color = Some (R mr); @@ -521,8 +525,10 @@ let canCoalesceBriggs u v = try iterAdjacent (consider v) u; iterAdjacent (consider u) v; + (*i Printf.printf " Briggs: OK\n"; *) true with Exit -> + (*i Printf.printf " Briggs: no\n"; *) false (* George's conservative coalescing criterion: all high-degree neighbors @@ -537,8 +543,11 @@ let canCoalesceGeorge u v = if t.degree < k || interfere t u then () else raise Exit in try - iterAdjacent isOK v; true + iterAdjacent isOK v; + (*i Printf.printf " George: OK\n"; *) + true with Exit -> + (*i Printf.printf " George: no\n"; *) false (* The combined coalescing criterion. [u] can be precolored, but @@ -603,7 +612,7 @@ let coalesce () = let m = DLinkMove.pick worklistMoves in let x = getAlias m.src and y = getAlias m.dst in let (u, v) = if y.nstate = Colored then (y, x) else (x, y) in - (*i Printf.printf "Attempt coalescing %s and %s\n" (name_of_node u) (name_of_node v);*) + (*i Printf.printf "Attempt coalescing %s and %s\n" (name_of_node u) (name_of_node v); *) if u == v then begin DLinkMove.insert m coalescedMoves; addWorkList u diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml new file mode 100644 index 00000000..6a745060 --- /dev/null +++ b/backend/PrintCminor.ml @@ -0,0 +1,285 @@ +(* *********************************************************************) +(* *) +(* 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 GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Pretty-printer for Cminor *) + +open Format +open Camlcoq +open Datatypes +open BinPos +open Integers +open AST +open Cminor + +(* Precedences and associativity -- like those of C *) + +type associativity = LtoR | RtoL | NA + +let rec precedence = function + | Evar _ -> (16, NA) + | Econst _ -> (16, NA) + | Eunop _ -> (15, RtoL) + | Ebinop((Omul|Odiv|Odivu|Omod|Omodu|Omulf|Odivf), _, _) -> (13, LtoR) + | Ebinop((Oadd|Osub|Oaddf|Osubf), _, _) -> (12, LtoR) + | Ebinop((Oshl|Oshr|Oshru), _, _) -> (11, LtoR) + | Ebinop((Ocmp _|Ocmpu _|Ocmpf _), _, _) -> (10, LtoR) + | Ebinop(Oand, _, _) -> (8, LtoR) + | Ebinop(Oxor, _, _) -> (7, LtoR) + | Ebinop(Oor, _, _) -> (6, LtoR) + | Eload _ -> (15, RtoL) + | Econdition _ -> (3, RtoL) + +(* Naming idents. We assume we run after Cminorgen, which encoded idents. *) + +let ident_name id = + match id with + | Coq_xO n -> extern_atom n + | Coq_xI n -> Printf.sprintf "$%ld" (camlint_of_positive n) + | Coq_xH -> "$0" + +(* Naming operators *) + +let name_of_unop = function + | Ocast8unsigned -> "int8u" + | Ocast8signed -> "int8s" + | Ocast16unsigned -> "int16u" + | Ocast16signed -> "int16s" + | Onegint -> "-" + | Onotbool -> "!" + | Onotint -> "~" + | Onegf -> "-f" + | Oabsf -> "absf" + | Osingleoffloat -> "float32" + | Ointoffloat -> "intoffloat" + | Ointuoffloat -> "intuoffloat" + | Ofloatofint -> "floatofint" + | Ofloatofintu -> "floatofintu" + +let comparison_name = function + | Ceq -> "==" + | Cne -> "!=" + | Clt -> "<" + | Cle -> "<=" + | Cgt -> ">" + | Cge -> ">=" + +let name_of_binop = function + | Oadd -> "+" + | Osub -> "-" + | Omul -> "*" + | Odiv -> "/" + | Odivu -> "/u" + | Omod -> "%" + | Omodu -> "%u" + | Oand -> "&" + | Oor -> "|" + | Oxor -> "^" + | Oshl -> "<<" + | Oshr -> ">>" + | Oshru -> ">>u" + | Oaddf -> "+f" + | Osubf -> "-f" + | Omulf -> "*f" + | Odivf -> "/f" + | Ocmp c -> comparison_name c + | Ocmpu c -> comparison_name c ^ "u" + | Ocmpf c -> comparison_name c ^ "f" + +let name_of_chunk = function + | Mint8signed -> "int8signed" + | Mint8unsigned -> "int8unsigned" + | Mint16signed -> "int16signed" + | Mint16unsigned -> "int16unsigned" + | Mint32 -> "int32" + | Mfloat32 -> "float32" + | Mfloat64 -> "float64" + +(* Expressions *) + +let rec expr p (prec, e) = + let (prec', assoc) = precedence e in + let (prec1, prec2) = + if assoc = LtoR + then (prec', prec' + 1) + else (prec' + 1, prec') in + if prec' < prec + then fprintf p "@[<hov 2>(" + else fprintf p "@[<hov 2>"; + begin match e with + | Evar id -> + fprintf p "%s" (ident_name id) + | Econst(Ointconst n) -> + fprintf p "%ld" (camlint_of_coqint n) + | Econst(Ofloatconst f) -> + fprintf p "%F" f + | Econst(Oaddrsymbol(id, ofs)) -> + let ofs = camlint_of_coqint ofs in + if ofs = 0l + then fprintf p "\"%s\"" (extern_atom id) + else fprintf p "(\"%s\" + %ld)" (extern_atom id) ofs + | Econst(Oaddrstack n) -> + fprintf p "&%ld" (camlint_of_coqint n) + | Eunop(op, a1) -> + fprintf p "%s %a" (name_of_unop op) expr (prec', a1) + | Ebinop(op, a1, a2) -> + fprintf p "%a@ %s %a" + expr (prec1, a1) (name_of_binop op) expr (prec2, a2) + | Eload(chunk, a1) -> + fprintf p "%s[%a]" (name_of_chunk chunk) expr (0, a1) + | Econdition(a1, a2, a3) -> + fprintf p "%a@ ? %a@ : %a" expr (4, a1) expr (4, a2) expr (4, a3) + end; + if prec' < prec then fprintf p ")@]" else fprintf p "@]" + +let print_expr p e = expr p (0, e) + +let rec print_expr_list p (first, rl) = + match rl with + | [] -> () + | r :: rl -> + if not first then fprintf p ",@ "; + expr p (2, r); + print_expr_list p (false, rl) + +(* Types *) + +let name_of_type = function + | Tint -> "int" + | Tfloat -> "float" + +let rec print_sig p = function + | {sig_args = []; sig_res = None} -> fprintf p "void" + | {sig_args = []; sig_res = Some ty} -> fprintf p "%s" (name_of_type ty) + | {sig_args = t1 :: tl; sig_res = tres} -> + fprintf p "%s ->@ " (name_of_type t1); + print_sig p {sig_args = tl; sig_res = tres} + +(* Statements *) + +let rec print_stmt p s = + match s with + | Sskip -> + fprintf p "/*skip*/;" + | Sassign(id, e2) -> + fprintf p "@[<hv 2>%s =@ %a;@]" (ident_name id) print_expr e2 + | Sstore(chunk, a1, a2) -> + fprintf p "@[<hv 2>%s[%a] =@ %a;@]" + (name_of_chunk chunk) print_expr a1 print_expr a2 + | Scall(None, sg, e1, el) -> + fprintf p "@[<hv 2>%a@,(@[<hov 0>%a@])@ : @[<hov 0>%a@];@]" + print_expr e1 + print_expr_list (true, el) + print_sig sg + | Scall(Some id, sg, e1, el) -> + fprintf p "@[<hv 2>%s =@ %a@,(@[<hov 0>%a@]);@] : @[<hov 0>%a@]" + (ident_name id) + print_expr e1 + print_expr_list (true, el) + print_sig sg + | Stailcall(sg, e1, el) -> + fprintf p "@[<hv 2>tailcall %a@,(@[<hov 0>%a@])@ : @[<hov 0>%a@];@]" + print_expr e1 + print_expr_list (true, el) + print_sig sg + | Sseq(Sskip, s2) -> + print_stmt p s2 + | Sseq(s1, Sskip) -> + print_stmt p s1 + | Sseq(s1, s2) -> + fprintf p "%a@ %a" print_stmt s1 print_stmt s2 + | Sifthenelse(e, s1, Sskip) -> + fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s1 + | Sifthenelse(e, Sskip, s2) -> + fprintf p "@[<v 2>if (! %a) {@ %a@;<0 -2>}@]" + expr (15, e) + print_stmt s2 + | Sifthenelse(e, s1, s2) -> + fprintf p "@[<v 2>if (%a) {@ %a@;<0 -2>} else {@ %a@;<0 -2>}@]" + print_expr e + print_stmt s1 + print_stmt s2 + | Sloop(s) -> + fprintf p "@[<v 2>loop {@ %a@;<0 -2>}@]" + print_stmt s + | Sblock(s) -> + fprintf p "@[<v 3>{{ %a@;<0 -3>}}@]" + print_stmt s + | Sexit n -> + fprintf p "exit %d;" (camlint_of_nat n + 1) + | Sswitch(e, cases, dfl) -> + fprintf p "@[<v 2>switch (%a) {" print_expr e; + List.iter + (fun (Coq_pair(n, x)) -> + fprintf p "@ case %ld: exit %d;\n" + (camlint_of_coqint n) (camlint_of_nat x)) + cases; + fprintf p "@ default: exit %d;\n" (camlint_of_nat dfl); + fprintf p "@;<0 -2>}@]" + | Sreturn None -> + fprintf p "return;" + | Sreturn (Some e) -> + fprintf p "return %a;" print_expr e + | Slabel(lbl, s1) -> + fprintf p "%s:@ %a" (extern_atom lbl) print_stmt s1 + | Sgoto lbl -> + fprintf p "goto %s;" (extern_atom lbl) + +(* Functions *) + +let rec print_varlist p (vars, first) = + match vars with + | [] -> () + | v1 :: vl -> + if not first then fprintf p ",@ "; + fprintf p "%s" (ident_name v1); + print_varlist p (vl, false) + +let print_function p id f = + fprintf p "@[<hov 4>\"%s\"(@[<hov 0>%a@])@ : @[<hov 0>%a@]@]@ " + (extern_atom id) + print_varlist (f.fn_params, true) + print_sig f.fn_sig; + fprintf p "@[<v 2>{@ "; + let stksz = camlint_of_z f.fn_stackspace in + if stksz <> 0l then + fprintf p "stack %ld;@ " stksz; + if f.fn_vars <> [] then + fprintf p "var @[<hov 0>%a;@]@ " print_varlist (f.fn_vars, true); + print_stmt p f.fn_body; + fprintf p "@;<0 -2>}@]@ " + +let print_fundef p (Coq_pair(id, fd)) = + match fd with + | External ef -> + () (* Todo? *) + | Internal f -> + print_function p id f + +let print_program p prog = + fprintf p "@[<v 0>"; + List.iter (print_fundef p) prog.prog_funct; + fprintf p "@]@." + +let destination : string option ref = ref None + +let print_if prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out f in + print_program (formatter_of_out_channel oc) prog; + close_out oc diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml new file mode 100644 index 00000000..0f38a3f6 --- /dev/null +++ b/backend/PrintLTLin.ml @@ -0,0 +1,130 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Pretty-printer for LTLin code *) + +open Format +open Camlcoq +open Datatypes +open Maps +open AST +open Integers +open Locations +open Machregsaux +open LTLin +open PrintOp + +let name_of_chunk = function + | Mint8signed -> "int8signed" + | Mint8unsigned -> "int8unsigned" + | Mint16signed -> "int16signed" + | Mint16unsigned -> "int16unsigned" + | Mint32 -> "int32" + | Mfloat32 -> "float32" + | Mfloat64 -> "float64" + +let name_of_type = function + | Tint -> "int" + | Tfloat -> "float" + +let reg pp loc = + match loc with + | R r -> + begin match name_of_register r with + | Some s -> fprintf pp "%s" s + | None -> fprintf pp "<unknown reg>" + end + | S (Local(ofs, ty)) -> + fprintf pp "local(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs) + | S (Incoming(ofs, ty)) -> + fprintf pp "incoming(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs) + | S (Outgoing(ofs, ty)) -> + fprintf pp "outgoing(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs) + +let rec regs pp = function + | [] -> () + | [r] -> reg pp r + | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl + +let ros pp = function + | Coq_inl r -> reg pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let print_instruction pp i = + match i with + | Lop(op, args, res) -> + fprintf pp "%a = %a@ " + reg res (PrintOp.print_operation reg) (op, args) + | Lload(chunk, addr, args, dst) -> + fprintf pp "%a = %s[%a]@ " + reg dst (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + | Lstore(chunk, addr, args, src) -> + fprintf pp "%s[%a] = %a@ " + (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + reg src + | Lcall(sg, fn, args, res) -> + fprintf pp "%a = %a(%a)@ " + reg res ros fn regs args + | Ltailcall(sg, fn, args) -> + fprintf pp "tailcall %a(%a)@ " + ros fn regs args + | Lbuiltin(ef, args, res) -> + fprintf pp "%a = builtin \"%s\"(%a)@ " + reg res (extern_atom ef.ef_id) regs args + | Llabel lbl -> + fprintf pp "%5ld: " (camlint_of_positive lbl) + | Lgoto lbl -> + fprintf pp "goto %ld@ " (camlint_of_positive lbl) + | Lcond(cond, args, lbl) -> + fprintf pp "if (%a) goto %ld@ " + (PrintOp.print_condition reg) (cond, args) + (camlint_of_positive lbl) + | Ljumptable(arg, tbl) -> + let tbl = Array.of_list tbl in + fprintf pp "@[<v 2>jumptable (%a)" reg arg; + for i = 0 to Array.length tbl - 1 do + fprintf pp "@ case %d: goto %ld" i (camlint_of_positive tbl.(i)) + done; + fprintf pp "@]@ " + | Lreturn None -> + fprintf pp "return@ " + | Lreturn (Some arg) -> + fprintf pp "return %a@ " reg arg + +let print_function pp f = + fprintf pp "@[<v 2>f(%a) {@ " regs f.fn_params; + List.iter (print_instruction pp) f.fn_code; + fprintf pp "@;<0 -2>}@]@." + +let print_fundef pp fd = + match fd with + | Internal f -> print_function pp f + | External _ -> () + +let destination : string option ref = ref None +let currpp : formatter option ref = ref None + +let print_if fd = + match !destination with + | None -> () + | Some f -> + let pp = + match !currpp with + | Some pp -> pp + | None -> + let oc = open_out f in + let pp = formatter_of_out_channel oc in + currpp := Some pp; + pp + in print_fundef pp fd diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 6e8c5785..62ee2c99 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -21,6 +21,8 @@ open Integers open RTL open PrintOp +(* Printing of RTL code *) + let name_of_chunk = function | Mint8signed -> "int8signed" | Mint8unsigned -> "int8unsigned" @@ -55,15 +57,19 @@ let print_instruction pp (pc, i) = then fprintf pp "nop@ " else fprintf pp "goto %ld@ " s | Iop(op, args, res, s) -> - fprintf pp "%a = %a@ " reg res (print_operator reg) (op, args); + fprintf pp "%a = %a@ " + reg res (PrintOp.print_operation reg) (op, args); print_succ pp s (Int32.pred pc) | Iload(chunk, addr, args, dst, s) -> fprintf pp "%a = %s[%a]@ " - reg dst (name_of_chunk chunk) (print_addressing reg) (addr, args); + reg dst (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args); print_succ pp s (Int32.pred pc) | Istore(chunk, addr, args, src, s) -> fprintf pp "%s[%a] = %a@ " - (name_of_chunk chunk) (print_addressing reg) (addr, args) reg src; + (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + reg src; print_succ pp s (Int32.pred pc) | Icall(sg, fn, args, res, s) -> fprintf pp "%a = %a(%a)@ " @@ -72,9 +78,13 @@ let print_instruction pp (pc, i) = | Itailcall(sg, fn, args) -> fprintf pp "tailcall %a(%a)@ " ros fn regs args + | Ibuiltin(ef, args, res, s) -> + fprintf pp "%a = builtin \"%s\"(%a)@ " + reg res (extern_atom ef.ef_id) regs args; + print_succ pp s (Int32.pred pc) | Icond(cond, args, s1, s2) -> fprintf pp "if (%a) goto %ld else goto %ld@ " - (print_condition reg) (cond, args) + (PrintOp.print_condition reg) (cond, args) (camlint_of_positive s1) (camlint_of_positive s2) | Ijumptable(arg, tbl) -> let tbl = Array.of_list tbl in @@ -101,11 +111,42 @@ let print_function pp f = List.iter (print_instruction pp) instrs; fprintf pp "@;<0 -2>}@]@." -let print_fundef fd = - begin match fd with - | Internal f -> print_function std_formatter f +let print_fundef pp fd = + match fd with + | Internal f -> print_function pp f | External _ -> () - end; - fd +let print_if optdest currpp fd = + match !optdest with + | None -> () + | Some f -> + let pp = + match !currpp with + | Some pp -> pp + | None -> + let oc = open_out f in + let pp = formatter_of_out_channel oc in + currpp := Some pp; + pp + in print_fundef pp fd + +let destination_rtl : string option ref = ref None +let pp_rtl : formatter option ref = ref None +let print_rtl = print_if destination_rtl pp_rtl + +let destination_tailcall : string option ref = ref None +let pp_tailcall : formatter option ref = ref None +let print_tailcall = print_if destination_tailcall pp_tailcall + +let destination_castopt : string option ref = ref None +let pp_castopt : formatter option ref = ref None +let print_castopt = print_if destination_castopt pp_castopt + +let destination_constprop : string option ref = ref None +let pp_constprop : formatter option ref = ref None +let print_constprop = print_if destination_constprop pp_constprop + +let destination_cse : string option ref = ref None +let pp_cse : formatter option ref = ref None +let print_cse = print_if destination_cse pp_cse diff --git a/backend/RTLgen.v b/backend/RTLgen.v index aec2c867..b728829f 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -363,6 +363,16 @@ Fixpoint alloc_regs (map: mapping) (al: exprlist) ret (r :: rl) end. +(** [alloc_optreg] is used for function calls. If a destination is + specified for the call, it is returned. Otherwise, a fresh + register is returned. *) + +Definition alloc_optreg (map: mapping) (dest: option ident) : mon reg := + match dest with + | Some id => find_var map id + | None => new_reg + end. + (** * RTL generation **) (** Insertion of a register-to-register move instruction. *) @@ -440,20 +450,6 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node) error (Errors.msg "RTLgen.transl_exprlist") end. -(** Generation of code for variable assignments. *) - -Definition store_var - (map: mapping) (rs: reg) (id: ident) (nd: node) : mon node := - do rv <- find_var map id; - add_move rs rv nd. - -Definition store_optvar - (map: mapping) (rs: reg) (optid: option ident) (nd: node) : mon node := - match optid with - | None => ret nd - | Some id => store_var map rs id nd - end. - (** Auxiliary for branch prediction. When compiling an if/then/else statement, we have a choice between translating the ``then'' branch first or the ``else'' branch first. Linearization of RTL control-flow @@ -535,11 +531,10 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) | Scall optid sig b cl => do rf <- alloc_reg map b; do rargs <- alloc_regs map cl; - do r <- new_reg; - do n1 <- store_optvar map r optid nd; - do n2 <- add_instr (Icall sig (inl _ rf) rargs r n1); - do n3 <- transl_exprlist map cl rargs n2; - transl_expr map b rf n3 + do r <- alloc_optreg map optid; + do n1 <- add_instr (Icall sig (inl _ rf) rargs r nd); + do n2 <- transl_exprlist map cl rargs n1; + transl_expr map b rf n2 | Stailcall sig b cl => do rf <- alloc_reg map b; do rargs <- alloc_regs map cl; @@ -548,10 +543,9 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) transl_expr map b rf n2 | Sbuiltin optid ef al => do rargs <- alloc_regs map al; - do r <- new_reg; - do n1 <- store_optvar map r optid nd; - do n2 <- add_instr (Ibuiltin ef rargs r n1); - transl_exprlist map al rargs n2 + do r <- alloc_optreg map optid; + do n1 <- add_instr (Ibuiltin ef rargs r nd); + transl_exprlist map al rargs n1 | Sseq s1 s2 => do ns <- transl_stmt map s2 nd nexits ngoto nret rret; transl_stmt map s1 ns nexits ngoto nret rret diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index a1bd6618..12a8e2be 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -200,18 +200,12 @@ Qed. (** A variant of [match_env_update_var] where a variable is optionally assigned to, depending on the [dst] parameter. *) -Definition assign_dest (dst: option ident) (v: val) (e: Cminor.env) : Cminor.env := - match dst with - | None => e - | Some id => PTree.set id v e - end. - Lemma match_env_update_dest: forall map e le rs dst r v, map_wf map -> reg_map_ok map r dst -> match_env map e le rs -> - match_env map (assign_dest dst v e) le (rs#r <- v). + match_env map (set_optvar dst v e) le (rs#r <- v). Proof. intros. inv H0; simpl. eapply match_env_update_temp; eauto. @@ -410,43 +404,6 @@ Proof. split. apply Regmap.gss. intros; apply Regmap.gso; auto. Qed. -(** Correctness of the code generated by [store_var] and [store_optvar]. *) - -Lemma tr_store_var_correct: - forall rs cs f map r id ns nd e sp m, - tr_store_var f.(fn_code) map r id ns nd -> - map_wf map -> - match_env map e nil rs -> - exists rs', - star step tge (State cs f sp ns rs m) - E0 (State cs f sp nd rs' m) - /\ match_env map (PTree.set id rs#r e) nil rs'. -Proof. - intros. destruct H as [rv [A B]]. - exploit tr_move_correct; eauto. intros [rs' [EX [RES OTHER]]]. - exists rs'; split. eexact EX. - apply match_env_invariant with (rs#rv <- (rs#r)). - apply match_env_update_var; auto. - intros. rewrite Regmap.gsspec. destruct (peq r0 rv). - subst r0; auto. - auto. -Qed. - -Lemma tr_store_optvar_correct: - forall rs cs f map r optid ns nd e sp m, - tr_store_optvar f.(fn_code) map r optid ns nd -> - map_wf map -> - match_env map e nil rs -> - exists rs', - star step tge (State cs f sp ns rs m) - E0 (State cs f sp nd rs' m) - /\ match_env map (set_optvar optid rs#r e) nil rs'. -Proof. - intros. destruct optid; simpl in *. - eapply tr_store_var_correct; eauto. - exists rs; split. subst nd. apply star_refl. auto. -Qed. - (** Correctness of the translation of [switch] statements *) Lemma transl_switch_correct: @@ -558,7 +515,7 @@ Definition transl_expr_prop (ME: match_env map e le rs), exists rs', star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) - /\ match_env map (assign_dest dst v e) le rs' + /\ match_env map (set_optvar dst v e) le rs' /\ rs'#rd = v /\ (forall r, In r pr -> rs'#r = rs#r). @@ -1042,13 +999,12 @@ Inductive tr_cont: RTL.code -> mapping -> with match_stacks: CminorSel.cont -> list RTL.stackframe -> Prop := | match_stacks_stop: match_stacks Kstop nil - | match_stacks_call: forall optid f sp e k r tf n rs cs map nexits ngoto nret rret n', + | match_stacks_call: forall optid f sp e k r tf n rs cs map nexits ngoto nret rret, map_wf map -> tr_fun tf map f ngoto nret rret -> match_env map e nil rs -> - tr_store_optvar tf.(fn_code) map r optid n n' -> - ~reg_in_map map r -> - tr_cont tf.(fn_code) map k n' nexits ngoto nret rret cs -> + reg_map_ok map r optid -> + tr_cont tf.(fn_code) map k n nexits ngoto nret rret cs -> match_stacks (Kcall optid f sp e k) (Stackframe r tf sp n rs :: cs). Inductive match_states: CminorSel.state -> RTL.state -> Prop := @@ -1218,16 +1174,14 @@ Proof. inv TS. exploit transl_exprlist_correct; eauto. intros [rs' [E [F [G J]]]]. - exploit tr_store_optvar_correct. eauto. eauto. - apply match_env_update_temp. eexact F. eauto. - intros [rs'' [A B]]. econstructor; split. - left. eapply star_plus_trans. eexact E. eapply plus_left. + left. eapply plus_right. eexact E. eapply exec_Ibuiltin. eauto. rewrite G. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. - eexact A. reflexivity. traceEq. - econstructor; eauto. constructor. rewrite Regmap.gss in B. auto. + traceEq. + econstructor; eauto. constructor. + eapply match_env_update_dest; eauto. (* seq *) inv TS. @@ -1347,12 +1301,10 @@ Proof. (* return *) inv MS. - set (rs' := (rs#r <- v)). - assert (match_env map e nil rs'). unfold rs'; eauto with rtlg. - exploit tr_store_optvar_correct. eauto. eauto. eexact H. intros [rs'' [A B]]. - econstructor; split. - left; eapply plus_left. constructor. eexact A. traceEq. - econstructor; eauto. constructor. unfold rs' in B. rewrite Regmap.gss in B. auto. + econstructor; split. + left; apply plus_one; constructor. + econstructor; eauto. constructor. + eapply match_env_update_dest; eauto. Qed. Lemma transl_initial_states: diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 0b18a99b..22a1e79d 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -483,6 +483,27 @@ Proof. intros [A|B]. auto. right; eauto with rtlg. Qed. +Lemma alloc_optreg_valid: + forall dest s1 s2 map r i, + map_valid map s1 -> + alloc_optreg map dest s1 = OK r s2 i -> reg_valid r s2. +Proof. + intros until r. unfold alloc_reg. + case dest; eauto with rtlg. +Qed. +Hint Resolve alloc_optreg_valid: rtlg. + +Lemma alloc_optreg_fresh_or_in_map: + forall map dest s r s' i, + map_valid map s -> + alloc_optreg map dest s = OK r s' i -> + reg_in_map map r \/ reg_fresh r s. +Proof. + intros until s'. unfold alloc_optreg. destruct dest; intros. + left; eauto with rtlg. + right; eauto with rtlg. +Qed. + (** A register is an adequate target for holding the value of an expression if - either the register is associated with a Cminor let-bound variable @@ -736,19 +757,6 @@ with tr_exprlist (c: code): tr_exprlist c map (r1 :: pr) al n1 nd rl -> tr_exprlist c map pr (Econs a1 al) ns nd (r1 :: rl). -(** Auxiliary for the compilation of variable assignments. *) - -Definition tr_store_var (c: code) (map: mapping) - (rs: reg) (id: ident) (ns nd: node): Prop := - exists rv, map.(map_vars)!id = Some rv /\ tr_move c ns rs nd rv. - -Definition tr_store_optvar (c: code) (map: mapping) - (rs: reg) (optid: option ident) (ns nd: node): Prop := - match optid with - | None => ns = nd - | Some id => tr_store_var c map rs id ns nd - end. - (** Auxiliary for the compilation of [switch] statements. *) Definition tr_jumptable (nexits: list node) (tbl: list nat) (ttbl: list node) : Prop := @@ -804,23 +812,21 @@ Inductive tr_stmt (c: code) (map: mapping): tr_expr c map rl b n1 n2 rd None -> c!n2 = Some (Istore chunk addr rl rd nd) -> tr_stmt c map (Sstore chunk addr al b) ns nd nexits ngoto nret rret - | tr_Scall: forall optid sig b cl ns nd nexits ngoto nret rret rd n1 rf n2 n3 rargs, + | tr_Scall: forall optid sig b cl ns nd nexits ngoto nret rret rd n1 rf n2 rargs, tr_expr c map nil b ns n1 rf None -> tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> - c!n2 = Some (Icall sig (inl _ rf) rargs rd n3) -> - tr_store_optvar c map rd optid n3 nd -> - ~reg_in_map map rd -> + c!n2 = Some (Icall sig (inl _ rf) rargs rd nd) -> + reg_map_ok map rd optid -> tr_stmt c map (Scall optid sig b cl) ns nd nexits ngoto nret rret | tr_Stailcall: forall sig b cl ns nd nexits ngoto nret rret n1 rf n2 rargs, tr_expr c map nil b ns n1 rf None -> tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> c!n2 = Some (Itailcall sig (inl _ rf) rargs) -> tr_stmt c map (Stailcall sig b cl) ns nd nexits ngoto nret rret - | tr_Sbuiltin: forall optid ef al ns nd nexits ngoto nret rret rd n1 n2 rargs, + | tr_Sbuiltin: forall optid ef al ns nd nexits ngoto nret rret rd n1 rargs, tr_exprlist c map nil al ns n1 rargs -> - c!n1 = Some (Ibuiltin ef rargs rd n2) -> - tr_store_optvar c map rd optid n2 nd -> - ~reg_in_map map rd -> + c!n1 = Some (Ibuiltin ef rargs rd nd) -> + reg_map_ok map rd optid -> tr_stmt c map (Sbuiltin optid ef al) ns nd nexits ngoto nret rret | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n, tr_stmt c map s2 n nd nexits ngoto nret rret -> @@ -1077,25 +1083,15 @@ Proof. monadInv EQ1. Qed. -Lemma tr_store_var_incr: - forall s1 s2, state_incr s1 s2 -> - forall map rs id ns nd, - tr_store_var s1.(st_code) map rs id ns nd -> - tr_store_var s2.(st_code) map rs id ns nd. -Proof. - intros. destruct H0 as [rv [A B]]. - econstructor; split. eauto. eapply tr_move_incr; eauto. -Qed. - -Lemma tr_store_optvar_incr: - forall s1 s2, state_incr s1 s2 -> - forall map rs optid ns nd, - tr_store_optvar s1.(st_code) map rs optid ns nd -> - tr_store_optvar s2.(st_code) map rs optid ns nd. +Lemma alloc_optreg_map_ok: + forall map optid s1 r s2 i, + map_valid map s1 -> + alloc_optreg map optid s1 = OK r s2 i -> + reg_map_ok map r optid. Proof. - intros until nd. destruct optid; simpl. - apply tr_store_var_incr; auto. - auto. + unfold alloc_optreg; intros. destruct optid. + constructor. unfold find_var in H0. destruct (map_vars map)!i0; monadInv H0. auto. + constructor. eapply new_reg_not_in_map; eauto. Qed. Lemma tr_switch_incr: @@ -1116,32 +1112,10 @@ Proof. intros s1 s2 EXT. generalize tr_expr_incr tr_condition_incr tr_exprlist_incr; intros I1 I2 I3. pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). - pose (STV := tr_store_var_incr s1 s2 EXT). - pose (STOV := tr_store_optvar_incr s1 s2 EXT). induction 1; econstructor; eauto. eapply tr_switch_incr; eauto. Qed. -Lemma store_var_charact: - forall map rs id nd s ns s' incr, - store_var map rs id nd s = OK ns s' incr -> - tr_store_var s'.(st_code) map rs id ns nd. -Proof. - intros. monadInv H. generalize EQ. unfold find_var. - caseEq ((map_vars map)!id). 2: intros; discriminate. intros. monadInv EQ1. - exists x; split. auto. eapply add_move_charact; eauto. -Qed. - -Lemma store_optvar_charact: - forall map rs optid nd s ns s' incr, - store_optvar map rs optid nd s = OK ns s' incr -> - tr_store_optvar s'.(st_code) map rs optid ns nd. -Proof. - intros. destruct optid; simpl in H; simpl. - eapply store_var_charact; eauto. - monadInv H. auto. -Qed. - Lemma transl_exit_charact: forall nexits n s ne s' incr, transl_exit nexits n s = OK ne s' incr -> @@ -1218,15 +1192,14 @@ Proof. (* Scall *) econstructor; eauto 4 with rtlg. eapply transl_expr_charact; eauto 3 with rtlg. - apply tr_exprlist_incr with s6. auto. + apply tr_exprlist_incr with s5. auto. eapply transl_exprlist_charact; eauto 3 with rtlg. eapply alloc_regs_target_ok with (s1 := s1); eauto 3 with rtlg. apply regs_valid_cons; eauto 3 with rtlg. apply regs_valid_incr with s1; eauto 3 with rtlg. apply regs_valid_cons; eauto 3 with rtlg. apply regs_valid_incr with s2; eauto 3 with rtlg. - apply tr_store_optvar_incr with s4; auto. - eapply store_optvar_charact; eauto with rtlg. + eapply alloc_optreg_map_ok with (s1 := s2); eauto 3 with rtlg. (* Stailcall *) assert (RV: regs_valid (x :: nil) s1). apply regs_valid_cons; eauto 3 with rtlg. @@ -1237,8 +1210,7 @@ Proof. (* Sbuiltin *) econstructor; eauto 4 with rtlg. eapply transl_exprlist_charact; eauto 3 with rtlg. - apply tr_store_optvar_incr with s2; auto. - eapply store_optvar_charact; eauto with rtlg. + eapply alloc_optreg_map_ok with (s1 := s0); eauto with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. |