From 29e0c9b2c99a437fc9dfab66e1abdd546a5308d6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Jan 2014 15:59:11 +0000 Subject: Updated ARM backend wrt new static analyses and optimizations. NeedOp, Deadcode: must have distinct needs per argument of an operator. This change remains to be propagated to IA32 and PPC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2399 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asmgen.v | 8 + arm/Asmgenproof1.v | 20 +++ arm/CombineOp.v | 12 +- arm/CombineOpproof.v | 53 +++--- arm/ConstpropOp.vp | 200 ++++------------------ arm/ConstpropOpproof.v | 442 +++++++++++++++++++++++-------------------------- arm/NeedOp.v | 204 +++++++++++++++++++++++ arm/Op.v | 10 ++ arm/PrintAsm.ml | 21 +-- arm/PrintOp.ml | 2 + arm/SelectOp.vp | 4 +- arm/SelectOpproof.v | 14 +- arm/ValueAOp.v | 193 +++++++++++++++++++++ 13 files changed, 728 insertions(+), 455 deletions(-) create mode 100644 arm/NeedOp.v create mode 100644 arm/ValueAOp.v (limited to 'arm') diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 3707b7f..b6cb2b3 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -267,6 +267,14 @@ Definition transl_op | Oaddrstack n, nil => do r <- ireg_of res; OK (addimm r IR13 n k) + | Ocast8signed, a1 :: nil => + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (Pmov r (SOlslimm r1 (Int.repr 24)) :: + Pmov r (SOasrimm r (Int.repr 24)) :: k) + | Ocast16signed, a1 :: nil => + do r <- ireg_of res; do r1 <- ireg_of a1; + OK (Pmov r (SOlslimm r1 (Int.repr 16)) :: + Pmov r (SOasrimm r (Int.repr 16)) :: k) | Oadd, a1 :: a2 :: nil => do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Padd r r1 (SOreg r2) :: k) diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 21d2b73..1e65d72 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -917,6 +917,26 @@ Proof. generalize (addimm_correct x IR13 i k rs m). intros [rs' [EX [RES OTH]]]. exists rs'; auto with asmgen. + (* Ocast8signed *) + set (rs1 := nextinstr (rs#x <- (Val.shl rs#x0 (Vint (Int.repr 24))))). + set (rs2 := nextinstr (rs1#x <- (Val.shr rs1#x (Vint (Int.repr 24))))). + exists rs2. + split. apply exec_straight_two with rs1 m; auto. + split. unfold rs2; Simpl. unfold rs1; Simpl. + unfold Val.shr, Val.shl; destruct (rs x0); auto. + change (Int.ltu (Int.repr 24) Int.iwordsize) with true; simpl. + f_equal. symmetry. apply (Int.sign_ext_shr_shl 8). compute; auto. + intros. unfold rs2, rs1; Simpl. + (* Ocast16signed *) + set (rs1 := nextinstr (rs#x <- (Val.shl rs#x0 (Vint (Int.repr 16))))). + set (rs2 := nextinstr (rs1#x <- (Val.shr rs1#x (Vint (Int.repr 16))))). + exists rs2. + split. apply exec_straight_two with rs1 m; auto. + split. unfold rs2; Simpl. unfold rs1; Simpl. + unfold Val.shr, Val.shl; destruct (rs x0); auto. + change (Int.ltu (Int.repr 16) Int.iwordsize) with true; simpl. + f_equal. symmetry. apply (Int.sign_ext_shr_shl 16). compute; auto. + intros. unfold rs2, rs1; Simpl. (* Oaddimm *) generalize (addimm_correct x x0 i k rs m). intros [rs' [A [B C]]]. diff --git a/arm/CombineOp.v b/arm/CombineOp.v index fd347c1..8da6e3a 100644 --- a/arm/CombineOp.v +++ b/arm/CombineOp.v @@ -17,13 +17,7 @@ Require Import Coqlib. Require Import AST. Require Import Integers. Require Import Op. -Require SelectOp. - -Definition valnum := positive. - -Inductive rhs : Type := - | Op: operation -> list valnum -> rhs - | Load: memory_chunk -> addressing -> list valnum -> rhs. +Require Import CSEdomain. Section COMBINE. @@ -104,7 +98,9 @@ Function combine_op (op: operation) (args: list valnum) : option(operation * lis end | Oandimm n, x :: nil => match get x with - | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys) + | Some(Op (Oandimm m) ys) => + Some(let p := Int.and m n in + if Int.eq p m then (Omove, x :: nil) else (Oandimm p, ys)) | _ => None end | Oorimm n, x :: nil => diff --git a/arm/CombineOpproof.v b/arm/CombineOpproof.v index c95b19c..485857b 100644 --- a/arm/CombineOpproof.v +++ b/arm/CombineOpproof.v @@ -21,8 +21,8 @@ Require Import Memory. Require Import Op. Require Import Registers. Require Import RTL. +Require Import CSEdomain. Require Import CombineOp. -Require Import CSE. Section COMBINE. @@ -31,8 +31,20 @@ Variable sp: val. Variable m: mem. Variable get: valnum -> option rhs. Variable valu: valnum -> val. -Hypothesis get_sound: forall v rhs, get v = Some rhs -> equation_holds valu ge sp m v rhs. +Hypothesis get_sound: forall v rhs, get v = Some rhs -> rhs_eval_to valu ge sp m rhs (valu v). +Lemma get_op_sound: + forall v op vl, get v = Some (Op op vl) -> eval_operation ge sp op (map valu vl) m = Some (valu v). +Proof. + intros. exploit get_sound; eauto. intros REV; inv REV; auto. +Qed. + +Ltac UseGetSound := + match goal with + | [ H: get _ = Some _ |- _ ] => + let x := fresh "EQ" in (generalize (get_op_sound _ _ _ H); intros x; simpl in x; FuncInv) + end. + Lemma combine_compimm_ne_0_sound: forall x cond args, combine_compimm_ne_0 get x = Some(cond, args) -> @@ -41,7 +53,7 @@ Lemma combine_compimm_ne_0_sound: Proof. intros until args. functional induction (combine_compimm_ne_0 get x); intros EQ; inv EQ. (* of cmp *) - exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. + UseGetSound. rewrite <- H. destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto. Qed. @@ -53,7 +65,7 @@ Lemma combine_compimm_eq_0_sound: Proof. intros until args. functional induction (combine_compimm_eq_0 get x); intros EQ; inv EQ. (* of cmp *) - exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. + UseGetSound. rewrite <- H. rewrite eval_negate_condition. destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto. Qed. @@ -66,7 +78,7 @@ Lemma combine_compimm_eq_1_sound: Proof. intros until args. functional induction (combine_compimm_eq_1 get x); intros EQ; inv EQ. (* of cmp *) - exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. + UseGetSound. rewrite <- H. destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto. Qed. @@ -78,7 +90,7 @@ Lemma combine_compimm_ne_1_sound: Proof. intros until args. functional induction (combine_compimm_ne_1 get x); intros EQ; inv EQ. (* of cmp *) - exploit get_sound; eauto. unfold equation_holds. simpl. intro EQ; inv EQ. + UseGetSound. rewrite <- H. rewrite eval_negate_condition. destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto. Qed. @@ -114,8 +126,7 @@ Theorem combine_addr_sound: Proof. intros. functional inversion H; subst. (* indexed - addimm *) - exploit get_sound; eauto. unfold equation_holds; simpl; intro EQ. FuncInv. - rewrite <- H0. rewrite Val.add_assoc. auto. + UseGetSound. simpl. rewrite <- H0. rewrite Val.add_assoc. auto. Qed. Theorem combine_op_sound: @@ -125,28 +136,28 @@ Theorem combine_op_sound: Proof. intros. functional inversion H; subst. (* addimm - addimm *) - exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. - rewrite <- H1. rewrite Val.add_assoc. auto. + UseGetSound. FuncInv. simpl. + rewrite <- H0. rewrite Val.add_assoc. auto. (* addimm - subimm *) Opaque Val.sub. - exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. - rewrite <- H1. change (Vint (Int.add m0 n)) with (Val.add (Vint m0) (Vint n)). - rewrite Val.sub_add_l. auto. + UseGetSound. FuncInv. simpl. + change (Vint (Int.add m0 n)) with (Val.add (Vint m0) (Vint n)). + rewrite <- H0. rewrite Val.sub_add_l. auto. (* subimm - addimm *) - exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. - rewrite <- H1. + UseGetSound. FuncInv. simpl. rewrite <- H0. Transparent Val.sub. destruct v; simpl; auto. repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. rewrite Int.neg_add_distr. decEq. decEq. decEq. apply Int.add_commut. (* andimm - andimm *) - exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. - rewrite <- H1. rewrite Val.and_assoc. auto. + UseGetSound; simpl. + generalize (Int.eq_spec p m0); rewrite H7; intros. + rewrite <- H0. rewrite Val.and_assoc. simpl. fold p. rewrite H1. auto. + UseGetSound; simpl. + rewrite <- H0. rewrite Val.and_assoc. auto. (* orimm - orimm *) - exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. - rewrite <- H1. rewrite Val.or_assoc. auto. + UseGetSound. simpl. rewrite <- H0. rewrite Val.or_assoc. auto. (* xorimm - xorimm *) - exploit get_sound; eauto. unfold equation_holds; simpl; intros. FuncInv. - rewrite <- H1. rewrite Val.xor_assoc. auto. + UseGetSound. simpl. rewrite <- H0. rewrite Val.xor_assoc. auto. (* cmp *) simpl. decEq; decEq. eapply combine_cond_sound; eauto. Qed. diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index 47d2086..0540781 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -19,35 +19,16 @@ Require Import Integers. Require Import Floats. Require Import Op. Require Import Registers. +Require Import ValueDomain. -(** * Static analysis *) - -(** To each pseudo-register at each program point, the static analysis - associates a compile-time approximation taken from the following set. *) - -Inductive approx : Type := - | Novalue: approx (** No value possible, code is unreachable. *) - | Unknown: approx (** All values are possible, - no compile-time information is available. *) - | I: int -> approx (** A known integer value. *) - | F: float -> approx (** A known floating-point value. *) - | L: int64 -> approx (** A know 64-bit integer value. *) - | G: ident -> int -> approx - (** The value is the address of the given global - symbol plus the given integer offset. *) - | S: int -> approx. (** The value is the stack pointer plus the offset. *) - +(** * Operator strength reduction *) -(** We now define the abstract interpretations of conditions and operators - over this set of approximations. For instance, the abstract interpretation - of the operator [Oaddf] applied to two expressions [a] and [b] is - [F(Float.add f g)] if [a] and [b] have static approximations [F f] - and [F g] respectively, and [Unknown] otherwise. +(** We now define auxiliary functions for strength reduction of + operators and addressing modes: replacing an operator with a cheaper + one if some of its arguments are statically known. These are again + large pattern-matchings expressed in indirect style. *) - The static approximations are defined by large pattern-matchings over - the approximations of the results. We write these matchings in the - indirect style described in file [SelectOp] to avoid excessive - duplication of cases in proofs. *) +Section STRENGTH_REDUCTION. Definition eval_static_shift (s: shift) (n: int) : int := match s with @@ -57,134 +38,8 @@ Definition eval_static_shift (s: shift) (n: int) : int := | Sror x => Int.ror n x end. -Nondetfunction eval_static_condition (cond: condition) (vl: list approx) := - match cond, vl with - | Ccomp c, I n1 :: I n2 :: nil => Some(Int.cmp c n1 n2) - | Ccompu c, I n1 :: I n2 :: nil => Some(Int.cmpu c n1 n2) - | Ccompshift c s, I n1 :: I n2 :: nil => Some(Int.cmp c n1 (eval_static_shift s n2)) - | Ccompushift c s, I n1 :: I n2 :: nil => Some(Int.cmpu c n1 (eval_static_shift s n2)) - | Ccompimm c n, I n1 :: nil => Some(Int.cmp c n1 n) - | Ccompuimm c n, I n1 :: nil => Some(Int.cmpu c n1 n) - | Ccompf c, F n1 :: F n2 :: nil => Some(Float.cmp c n1 n2) - | Cnotcompf c, F n1 :: F n2 :: nil => Some(negb(Float.cmp c n1 n2)) - | Ccompfzero c, F n1 :: nil => Some(Float.cmp c n1 Float.zero) - | Cnotcompfzero c, F n1 :: nil => Some(negb(Float.cmp c n1 Float.zero)) - | _, _ => None - end. - -Definition eval_static_condition_val (cond: condition) (vl: list approx) := - match eval_static_condition cond vl with - | None => Unknown - | Some b => I(if b then Int.one else Int.zero) - end. - -Definition eval_static_intoffloat (f: float) := - match Float.intoffloat f with Some x => I x | None => Unknown end. - -Definition eval_static_intuoffloat (f: float) := - match Float.intuoffloat f with Some x => I x | None => Unknown end. - -Parameter propagate_float_constants: unit -> bool. - -Nondetfunction eval_static_operation (op: operation) (vl: list approx) := - match op, vl with - | Omove, v1::nil => v1 - | Ointconst n, nil => I n - | Ofloatconst n, nil => if propagate_float_constants tt then F n else Unknown - | Oaddrsymbol s n, nil => G s n - | Oaddrstack n, nil => S n - | Oadd, I n1 :: I n2 :: nil => I(Int.add n1 n2) - | Oaddshift s, I n1 :: I n2 :: nil => I(Int.add n1 (eval_static_shift s n2)) - | Oadd, G s1 n1 :: I n2 :: nil => G s1 (Int.add n1 n2) - | Oaddshift s, G s1 n1 :: I n2 :: nil => G s1 (Int.add n1 (eval_static_shift s n2)) - | Oadd, S n1 :: I n2 :: nil => S (Int.add n1 n2) - | Oaddshift s, S n1 :: I n2 :: nil => S (Int.add n1 (eval_static_shift s n2)) - | Oadd, I n1 :: G s2 n2 :: nil => G s2 (Int.add n1 n2) - | Oadd, I n1 :: S n2 :: nil => S (Int.add n1 n2) - | Oaddimm n, I n1 :: nil => I (Int.add n1 n) - | Oaddimm n, G s1 n1 :: nil => G s1 (Int.add n1 n) - | Oaddimm n, S n1 :: nil => S (Int.add n1 n) - | Osub, I n1 :: I n2 :: nil => I(Int.sub n1 n2) - | Osubshift s, I n1 :: I n2 :: nil => I(Int.sub n1 (eval_static_shift s n2)) - | Osub, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 n2) - | Osub, S n1 :: I n2 :: nil => S (Int.sub n1 n2) - | Osubshift s, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 (eval_static_shift s n2)) - | Orsubshift s, I n1 :: I n2 :: nil => I(Int.sub (eval_static_shift s n2) n1) - | Orsubimm n, I n1 :: nil => I (Int.sub n n1) - | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2) - | Omla, I n1 :: I n2 :: I n3 :: nil => I(Int.add (Int.mul n1 n2) n3) - | Omulhs, I n1 :: I n2 :: nil => I(Int.mulhs n1 n2) - | Omulhu, I n1 :: I n2 :: nil => I(Int.mulhu n1 n2) - | Odiv, I n1 :: I n2 :: nil => - if Int.eq n2 Int.zero then Unknown else - if Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone then Unknown - else I(Int.divs n1 n2) - | Odivu, I n1 :: I n2 :: nil => - if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2) - | Oand, I n1 :: I n2 :: nil => I(Int.and n1 n2) - | Oandshift s, I n1 :: I n2 :: nil => I(Int.and n1 (eval_static_shift s n2)) - | Oandimm n, I n1 :: nil => I(Int.and n1 n) - | Oor, I n1 :: I n2 :: nil => I(Int.or n1 n2) - | Oorshift s, I n1 :: I n2 :: nil => I(Int.or n1 (eval_static_shift s n2)) - | Oorimm n, I n1 :: nil => I(Int.or n1 n) - | Oxor, I n1 :: I n2 :: nil => I(Int.xor n1 n2) - | Oxorshift s, I n1 :: I n2 :: nil => I(Int.xor n1 (eval_static_shift s n2)) - | Oxorimm n, I n1 :: nil => I(Int.xor n1 n) - | Obic, I n1 :: I n2 :: nil => I(Int.and n1 (Int.not n2)) - | Obicshift s, I n1 :: I n2 :: nil => I(Int.and n1 (Int.not (eval_static_shift s n2))) - | Onot, I n1 :: nil => I(Int.not n1) - | Onotshift s, I n1 :: nil => I(Int.not (eval_static_shift s n1)) - | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown - | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown - | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown - | Oshift s, I n1 :: nil => I(eval_static_shift s n1) - | Onegf, F n1 :: nil => F(Float.neg n1) - | Oabsf, F n1 :: nil => F(Float.abs n1) - | Oaddf, F n1 :: F n2 :: nil => F(Float.add n1 n2) - | Osubf, F n1 :: F n2 :: nil => F(Float.sub n1 n2) - | Omulf, F n1 :: F n2 :: nil => F(Float.mul n1 n2) - | Odivf, F n1 :: F n2 :: nil => F(Float.div n1 n2) - | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1) - | Ointoffloat, F n1 :: nil => eval_static_intoffloat n1 - | Ointuoffloat, F n1 :: nil => eval_static_intuoffloat n1 - | Ofloatofint, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofint n1) else Unknown - | Ofloatofintu, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofintu n1) else Unknown - | Omakelong, I n1 :: I n2 :: nil => L(Int64.ofwords n1 n2) - | Olowlong, L n :: nil => I(Int64.loword n) - | Ohighlong, L n :: nil => I(Int64.hiword n) - | Ocmp c, vl => eval_static_condition_val c vl - | _, _ => Unknown - end. - -Nondetfunction eval_static_addressing (addr: addressing) (vl: list approx) := - match addr, vl with - | Aindexed n, I n1::nil => I (Int.add n1 n) - | Aindexed n, G id ofs::nil => G id (Int.add ofs n) - | Aindexed n, S ofs::nil => S (Int.add ofs n) - | Aindexed2, I n1::I n2::nil => I (Int.add n1 n2) - | Aindexed2, G id ofs::I n2::nil => G id (Int.add ofs n2) - | Aindexed2, I n1::G id ofs::nil => G id (Int.add ofs n1) - | Aindexed2, S ofs::I n2::nil => S (Int.add ofs n2) - | Aindexed2, I n1::S ofs::nil => S (Int.add ofs n1) - | Aindexed2shift s, I n1::I n2::nil => I (Int.add n1 (eval_static_shift s n2)) - | Aindexed2shift s, G id ofs::I n2::nil => G id (Int.add ofs (eval_static_shift s n2)) - | Aindexed2shift s, S ofs::I n2::nil => S (Int.add ofs (eval_static_shift s n2)) - | Ainstack ofs, nil => S ofs - | _, _ => Unknown - end. - - -(** * Operator strength reduction *) - -(** We now define auxiliary functions for strength reduction of - operators and addressing modes: replacing an operator with a cheaper - one if some of its arguments are statically known. These are again - large pattern-matchings expressed in indirect style. *) - -Section STRENGTH_REDUCTION. - Nondetfunction cond_strength_reduction - (cond: condition) (args: list reg) (vl: list approx) := + (cond: condition) (args: list reg) (vl: list aval) := match cond, args, vl with | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => (Ccompimm (swap_comparison c) n1, r2 :: nil) @@ -272,9 +127,12 @@ Definition make_divuimm (n: int) (r1 r2: reg) := | None => (Odivu, r1 :: r2 :: nil) end. -Definition make_andimm (n: int) (r: reg) := +Definition make_andimm (n: int) (r: reg) (a: aval) := if Int.eq n Int.zero then (Ointconst Int.zero, nil) else if Int.eq n Int.mone then (Omove, r :: nil) + else if match a with Uns m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero + | _ => false end + then (Omove, r :: nil) else (Oandimm n, r :: nil). Definition make_orimm (n: int) (r: reg) := @@ -292,9 +150,20 @@ Definition make_mulfimm (n: float) (r r1 r2: reg) := then (Oaddf, r :: r :: nil) else (Omulf, r1 :: r2 :: nil). +Definition make_cast8signed (r: reg) (a: aval) := + if vincl a (Sgn 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). +Definition make_cast16signed (r: reg) (a: aval) := + if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). +Definition make_singleoffloat (r: reg) (a: aval) := + if vincl a Fsingle && generate_float_constants tt + then (Omove, r :: nil) + else (Osingleoffloat, r :: nil). + Nondetfunction op_strength_reduction - (op: operation) (args: list reg) (vl: list approx) := + (op: operation) (args: list reg) (vl: list aval) := match op, args, vl with + | Ocast8signed, r1 :: nil, v1 :: nil => make_cast8signed r1 v1 + | Ocast16signed, r1 :: nil, v1 :: nil => make_cast16signed r1 v1 | Oadd, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_addimm n1 r2 | Oadd, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm n2 r1 | Oaddshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (eval_static_shift s n2) r1 @@ -306,20 +175,21 @@ Nondetfunction op_strength_reduction | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_mulimm n2 r1 r2 | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divimm n2 r1 r2 | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divuimm n2 r1 r2 - | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_andimm n1 r2 - | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm n2 r1 - | Oandshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (eval_static_shift s n2) r1 + | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_andimm n1 r2 v2 + | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm n2 r1 v1 + | Oandshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (eval_static_shift s n2) r1 v1 | Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_orimm n1 r2 | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm n2 r1 | Oorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm (eval_static_shift s n2) r1 | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_xorimm n1 r2 | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm n2 r1 | Oxorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm (eval_static_shift s n2) r1 - | Obic, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (Int.not n2) r1 - | Obicshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (Int.not (eval_static_shift s n2)) r1 + | Obic, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (Int.not n2) r1 v1 + | Obicshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (Int.not (eval_static_shift s n2)) r1 v1 | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2 | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2 | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2 + | Osingleoffloat, r1 :: nil, v1 :: nil => make_singleoffloat r1 v1 | Ocmp c, args, vl => let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args') | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2 @@ -329,21 +199,21 @@ Nondetfunction op_strength_reduction Nondetfunction addr_strength_reduction - (addr: addressing) (args: list reg) (vl: list approx) := + (addr: addressing) (args: list reg) (vl: list aval) := match addr, args, vl with - | Aindexed2, r1 :: r2 :: nil, S n1 :: I n2 :: nil => + | Aindexed2, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil => (Ainstack (Int.add n1 n2), nil) - | Aindexed2, r1 :: r2 :: nil, I n1 :: S n2 :: nil => + | Aindexed2, r1 :: r2 :: nil, I n1 :: Ptr(Stk n2) :: nil => (Ainstack (Int.add n1 n2), nil) | Aindexed2, r1 :: r2 :: nil, I n1 :: v2 :: nil => (Aindexed n1, r2 :: nil) | Aindexed2, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Aindexed n2, r1 :: nil) - | Aindexed2shift s, r1 :: r2 :: nil, S n1 :: I n2 :: nil => + | Aindexed2shift s, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil => (Ainstack (Int.add n1 (eval_static_shift s n2)), nil) | Aindexed2shift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Aindexed (eval_static_shift s n2), r1 :: nil) - | Aindexed n, r1 :: nil, S n1 :: nil => + | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil => (Ainstack (Int.add n1 n), nil) | _, _, _ => (addr, args) diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index f0d6b7f..ad7dcd1 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -23,161 +23,8 @@ Require Import Events. Require Import Op. Require Import Registers. Require Import RTL. +Require Import ValueDomain. Require Import ConstpropOp. -Require Import Constprop. - -(** * Correctness of the static analysis *) - -Section ANALYSIS. - -Variable ge: genv. -Variable sp: val. - -(** We first show that the dataflow analysis is correct with respect - to the dynamic semantics: the approximations (sets of values) - of a register at a program point predicted by the static analysis - are a superset of the values actually encountered during concrete - executions. We formalize this correspondence between run-time values and - compile-time approximations by the following predicate. *) - -Definition val_match_approx (a: approx) (v: val) : Prop := - match a with - | Unknown => True - | I p => v = Vint p - | F p => v = Vfloat p - | L p => v = Vlong p - | G symb ofs => v = symbol_address ge symb ofs - | S ofs => v = Val.add sp (Vint ofs) - | Novalue => False - end. - -Inductive val_list_match_approx: list approx -> list val -> Prop := - | vlma_nil: - val_list_match_approx nil nil - | vlma_cons: - forall a al v vl, - val_match_approx a v -> - val_list_match_approx al vl -> - val_list_match_approx (a :: al) (v :: vl). - -Ltac SimplVMA := - match goal with - | H: (val_match_approx (I _) ?v) |- _ => - simpl in H; (try subst v); SimplVMA - | H: (val_match_approx (F _) ?v) |- _ => - simpl in H; (try subst v); SimplVMA - | H: (val_match_approx (L _) ?v) |- _ => - simpl in H; (try subst v); SimplVMA - | H: (val_match_approx (G _ _) ?v) |- _ => - simpl in H; (try subst v); SimplVMA - | H: (val_match_approx (S _) ?v) |- _ => - simpl in H; (try subst v); SimplVMA - | _ => - idtac - end. - -Ltac InvVLMA := - match goal with - | H: (val_list_match_approx nil ?vl) |- _ => - inv H - | H: (val_list_match_approx (?a :: ?al) ?vl) |- _ => - inv H; SimplVMA; InvVLMA - | _ => - idtac - end. - -(** We then show that [eval_static_operation] is a correct abstract - interpretations of [eval_operation]: if the concrete arguments match - the given approximations, the concrete results match the - approximations returned by [eval_static_operation]. *) - -Lemma eval_static_shift_correct: - forall s n, eval_shift s (Vint n) = Vint (eval_static_shift s n). -Proof. - intros. destruct s; simpl; rewrite s_range; auto. -Qed. - -Lemma eval_static_condition_correct: - forall cond al vl m b, - val_list_match_approx al vl -> - eval_static_condition cond al = Some b -> - eval_condition cond vl m = Some b. -Proof. - intros until b. - unfold eval_static_condition. - case (eval_static_condition_match cond al); intros; - InvVLMA; simpl; try (rewrite eval_static_shift_correct); congruence. -Qed. - -Remark shift_symbol_address: - forall symb ofs n, - symbol_address ge symb (Int.add ofs n) = Val.add (symbol_address ge symb ofs) (Vint n). -Proof. - unfold symbol_address; intros. destruct (Genv.find_symbol ge symb); auto. -Qed. - - -Lemma eval_static_operation_correct: - forall op al vl m v, - val_list_match_approx al vl -> - eval_operation ge sp op vl m = Some v -> - val_match_approx (eval_static_operation op al) v. -Proof. - intros until v. - unfold eval_static_operation. - case (eval_static_operation_match op al); intros; - InvVLMA; simpl in *; FuncInv; try (subst v); try (rewrite eval_static_shift_correct); auto. - destruct (propagate_float_constants tt); simpl; auto. - rewrite shift_symbol_address; auto. - rewrite shift_symbol_address; auto. - rewrite Val.add_assoc; auto. - rewrite Val.add_assoc; auto. - fold (Val.add (Vint n1) (symbol_address ge s2 n2)). - rewrite Int.add_commut. rewrite Val.add_commut. rewrite shift_symbol_address; auto. - fold (Val.add (Vint n1) (Val.add sp (Vint n2))). - rewrite Val.add_permut. auto. - rewrite shift_symbol_address. auto. - rewrite Val.add_assoc. auto. - rewrite Int.sub_add_opp. rewrite shift_symbol_address. rewrite Val.sub_add_opp. auto. - rewrite Val.sub_add_opp. rewrite Val.add_assoc. rewrite Int.sub_add_opp. auto. - rewrite Int.sub_add_opp. rewrite shift_symbol_address. rewrite Val.sub_add_opp. auto. - destruct (Int.eq n2 Int.zero). inv H0. - destruct (Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); inv H0; simpl; auto. - destruct (Int.eq n2 Int.zero); inv H0. simpl; auto. - destruct (Int.ltu n2 Int.iwordsize); simpl; auto. - destruct (Int.ltu n2 Int.iwordsize); simpl; auto. - destruct (Int.ltu n2 Int.iwordsize); simpl; auto. - unfold eval_static_intoffloat. destruct (Float.intoffloat n1); simpl in H0; inv H0; simpl; auto. - unfold eval_static_intuoffloat. destruct (Float.intuoffloat n1); simpl in H0; inv H0; simpl; auto. - destruct (propagate_float_constants tt); simpl; auto. - destruct (propagate_float_constants tt); simpl; auto. - unfold eval_static_condition_val, Val.of_optbool. - destruct (eval_static_condition c vl0) eqn:?. - rewrite (eval_static_condition_correct _ _ _ m _ H Heqo). - destruct b; simpl; auto. - simpl; auto. -Qed. - -Lemma eval_static_addressing_correct: - forall addr al vl v, - val_list_match_approx al vl -> - eval_addressing ge sp addr vl = Some v -> - val_match_approx (eval_static_addressing addr al) v. -Proof. - intros until v. unfold eval_static_addressing. - case (eval_static_addressing_match addr al); intros; - InvVLMA; simpl in *; FuncInv; try (subst v); try (rewrite eval_static_shift_correct); auto. - rewrite shift_symbol_address; auto. - rewrite Val.add_assoc. auto. - repeat rewrite shift_symbol_address. auto. - fold (Val.add (Vint n1) (symbol_address ge id ofs)). - repeat rewrite shift_symbol_address. apply Val.add_commut. - repeat rewrite Val.add_assoc. auto. - fold (Val.add (Vint n1) (Val.add sp (Vint ofs))). - rewrite Val.add_permut. decEq. rewrite Val.add_commut. auto. - rewrite shift_symbol_address. auto. - rewrite Val.add_assoc. auto. -Qed. (** * Correctness of strength reduction *) @@ -189,50 +36,99 @@ Qed. Section STRENGTH_REDUCTION. -Variable app: D.t. +Variable bc: block_classification. +Variable ge: genv. +Hypothesis GENV: genv_match bc ge. +Variable sp: block. +Hypothesis STACK: bc sp = BCstack. +Variable ae: AE.t. Variable rs: regset. Variable m: mem. -Hypothesis MATCH: forall r, val_match_approx (approx_reg app r) rs#r. +Hypothesis MATCH: ematch bc rs ae. + +Lemma match_G: + forall r id ofs, + AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#r (symbol_address ge id ofs). +Proof. + intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH. +Qed. + +Lemma match_S: + forall r ofs, + AE.get r ae = Ptr(Stk ofs) -> Val.lessdef rs#r (Vptr sp ofs). +Proof. + intros. apply vmatch_ptr_stk with bc; auto. rewrite <- H. apply MATCH. +Qed. Ltac InvApproxRegs := match goal with | [ H: _ :: _ = _ :: _ |- _ ] => injection H; clear H; intros; InvApproxRegs - | [ H: ?v = approx_reg app ?r |- _ ] => + | [ H: ?v = AE.get ?r ae |- _ ] => generalize (MATCH r); rewrite <- H; clear H; intro; InvApproxRegs | _ => idtac end. +Ltac SimplVM := + match goal with + | [ H: vmatch _ ?v (I ?n) |- _ ] => + let E := fresh in + assert (E: v = Vint n) by (inversion H; auto); + rewrite E in *; clear H; SimplVM + | [ H: vmatch _ ?v (F ?n) |- _ ] => + let E := fresh in + assert (E: v = Vfloat n) by (inversion H; auto); + rewrite E in *; clear H; SimplVM + | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] => + let E := fresh in + assert (E: Val.lessdef v (Op.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); + clear H; SimplVM + | [ H: vmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] => + let E := fresh in + assert (E: Val.lessdef v (Vptr sp ofs)) by (eapply vmatch_ptr_stk; eauto); + clear H; SimplVM + | _ => idtac + end. + +Lemma eval_static_shift_correct: + forall s n, eval_shift s (Vint n) = Vint (eval_static_shift s n). +Proof. + intros. destruct s; simpl; rewrite s_range; auto. +Qed. + Lemma cond_strength_reduction_correct: forall cond args vl, - vl = approx_regs app args -> + vl = map (fun r => AE.get r ae) args -> let (cond', args') := cond_strength_reduction cond args vl in eval_condition cond' rs##args' m = eval_condition cond rs##args m. Proof. intros until vl. unfold cond_strength_reduction. - case (cond_strength_reduction_match cond args vl); simpl; intros; InvApproxRegs; SimplVMA. - rewrite H0. apply Val.swap_cmp_bool. - rewrite H. auto. - rewrite H0. apply Val.swap_cmpu_bool. - rewrite H. auto. - rewrite H. rewrite eval_static_shift_correct. auto. - rewrite H. rewrite eval_static_shift_correct. auto. - auto. - destruct (Float.eq_dec n1 Float.zero); simpl; auto. - rewrite H0; subst n1. destruct (rs#r2); simpl; auto. rewrite Float.cmp_swap. auto. - destruct (Float.eq_dec n2 Float.zero); simpl; auto. - congruence. - destruct (Float.eq_dec n1 Float.zero); simpl; auto. - rewrite H0; subst n1. destruct (rs#r2); simpl; auto. rewrite Float.cmp_swap. auto. - destruct (Float.eq_dec n2 Float.zero); simpl; auto. - congruence. - auto. + case (cond_strength_reduction_match cond args vl); simpl; intros; InvApproxRegs; SimplVM. +- apply Val.swap_cmp_bool. +- auto. +- apply Val.swap_cmpu_bool. +- auto. +- rewrite eval_static_shift_correct. auto. +- rewrite eval_static_shift_correct. auto. +- destruct (Float.eq_dec n1 Float.zero). + subst n1. simpl. destruct (rs#r2); simpl; auto. rewrite Float.cmp_swap. auto. + simpl. rewrite H1; auto. +- destruct (Float.eq_dec n2 Float.zero). + subst n2. simpl. auto. + simpl. rewrite H1; auto. +- destruct (Float.eq_dec n1 Float.zero). + subst n1. simpl. destruct (rs#r2); simpl; auto. rewrite Float.cmp_swap. auto. + simpl. rewrite H1; auto. +- destruct (Float.eq_dec n2 Float.zero); simpl; auto. + subst n2; auto. + rewrite H1; auto. +- auto. Qed. Lemma make_addimm_correct: forall n r, let (op, args) := make_addimm n r in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v. Proof. intros. unfold make_addimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. @@ -244,7 +140,7 @@ Lemma make_shlimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_shlimm n r1 r2 in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v. Proof. Opaque mk_shift_amount. intros; unfold make_shlimm. @@ -259,7 +155,7 @@ Lemma make_shrimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_shrimm n r1 r2 in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v. Proof. intros; unfold make_shrimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -273,7 +169,7 @@ Lemma make_shruimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_shruimm n r1 r2 in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v. Proof. intros; unfold make_shruimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -287,7 +183,7 @@ Lemma make_mulimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_mulimm n r1 r2 in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v. Proof. intros; unfold make_mulimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -306,7 +202,7 @@ Lemma make_divimm_correct: Val.divs rs#r1 rs#r2 = Some v -> rs#r2 = Vint n -> let (op, args) := make_divimm n r1 r2 in - exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w. + exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divimm. destruct (Int.is_power2 n) eqn:?. @@ -321,7 +217,7 @@ Lemma make_divuimm_correct: Val.divu rs#r1 rs#r2 = Some v -> rs#r2 = Vint n -> let (op, args) := make_divuimm n r1 r2 in - exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w. + exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divuimm. destruct (Int.is_power2 n) eqn:?. @@ -333,22 +229,35 @@ Proof. Qed. Lemma make_andimm_correct: - forall n r, - let (op, args) := make_andimm n r in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v. + forall n r x, + vmatch bc rs#r x -> + let (op, args) := make_andimm n r x in + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v. Proof. intros; unfold make_andimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst n. exists (Vint Int.zero); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone; intros. subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_mone; auto. + destruct (match x with Uns k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero + | _ => false end) eqn:UNS. + destruct x; try congruence. + exists (rs#r); split; auto. + inv H; auto. simpl. replace (Int.and i n) with i; auto. + generalize (Int.eq_spec (Int.zero_ext n0 (Int.not n)) Int.zero); rewrite UNS; intro EQ. + Int.bit_solve. destruct (zlt i0 n0). + replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)). + rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. + rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. + rewrite Int.bits_not by auto. apply negb_involutive. + rewrite H5 by auto. auto. econstructor; split; eauto. auto. Qed. Lemma make_orimm_correct: forall n r, let (op, args) := make_orimm n r in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v. Proof. intros; unfold make_orimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. @@ -361,7 +270,7 @@ Qed. Lemma make_xorimm_correct: forall n r, let (op, args) := make_xorimm n r in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v. Proof. intros; unfold make_xorimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. @@ -376,7 +285,7 @@ Lemma make_mulfimm_correct: forall n r1 r2, rs#r2 = Vfloat n -> let (op, args) := make_mulfimm n r1 r1 r2 in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. Proof. intros; unfold make_mulfimm. destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. @@ -389,7 +298,7 @@ Lemma make_mulfimm_correct_2: forall n r1 r2, rs#r1 = Vfloat n -> let (op, args) := make_mulfimm n r2 r1 r2 in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. Proof. intros; unfold make_mulfimm. destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. @@ -399,92 +308,151 @@ Proof. simpl. econstructor; split; eauto. Qed. +Lemma make_cast8signed_correct: + forall r x, + vmatch bc rs#r x -> + let (op, args) := make_cast8signed r x in + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v. +Proof. + intros; unfold make_cast8signed. destruct (vincl x (Sgn 8)) eqn:INCL. + exists rs#r; split; auto. + assert (V: vmatch bc rs#r (Sgn 8)). + { eapply vmatch_ge; eauto. apply vincl_ge; auto. } + inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + econstructor; split; simpl; eauto. +Qed. + +Lemma make_cast16signed_correct: + forall r x, + vmatch bc rs#r x -> + let (op, args) := make_cast16signed r x in + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v. +Proof. + intros; unfold make_cast16signed. destruct (vincl x (Sgn 16)) eqn:INCL. + exists rs#r; split; auto. + assert (V: vmatch bc rs#r (Sgn 16)). + { eapply vmatch_ge; eauto. apply vincl_ge; auto. } + inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + econstructor; split; simpl; eauto. +Qed. + +Lemma make_singleoffloat_correct: + forall r x, + vmatch bc rs#r x -> + let (op, args) := make_singleoffloat r x in + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.singleoffloat rs#r) v. +Proof. + intros; unfold make_singleoffloat. + destruct (vincl x Fsingle && generate_float_constants tt) eqn:INCL. + InvBooleans. exists rs#r; split; auto. + assert (V: vmatch bc rs#r Fsingle). + { eapply vmatch_ge; eauto. apply vincl_ge; auto. } + inv V; simpl; auto. rewrite Float.singleoffloat_of_single by auto. auto. + econstructor; split; simpl; eauto. +Qed. + Lemma op_strength_reduction_correct: forall op args vl v, - vl = approx_regs app args -> - eval_operation ge sp op rs##args m = Some v -> + vl = map (fun r => AE.get r ae) args -> + eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v -> let (op', args') := op_strength_reduction op args vl in - exists w, eval_operation ge sp op' rs##args' m = Some w /\ Val.lessdef v w. + exists w, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some w /\ Val.lessdef v w. Proof. intros until v; unfold op_strength_reduction; case (op_strength_reduction_match op args vl); simpl; intros. +(* cast8signed *) + InvApproxRegs; SimplVM; inv H0. apply make_cast8signed_correct; auto. +(* cast8signed *) + InvApproxRegs; SimplVM; inv H0. apply make_cast16signed_correct; auto. (* add *) - InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.add_commut. apply make_addimm_correct. - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_addimm_correct. + InvApproxRegs; SimplVM. inv H0. + fold (Val.add (Vint n1) rs#r2). rewrite Val.add_commut. apply make_addimm_correct. + InvApproxRegs; SimplVM. inv H0. apply make_addimm_correct. (* addshift *) - InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_addimm_correct. + InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. apply make_addimm_correct. (* sub *) - InvApproxRegs; SimplVMA. inv H0. rewrite H1. econstructor; split; eauto. - InvApproxRegs; SimplVMA. inv H0. rewrite H. rewrite Val.sub_add_opp. apply make_addimm_correct. + InvApproxRegs; SimplVM. inv H0. econstructor; split; eauto. + InvApproxRegs; SimplVM. inv H0. rewrite Val.sub_add_opp. apply make_addimm_correct. (* subshift *) - InvApproxRegs; SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. rewrite Val.sub_add_opp. apply make_addimm_correct. + InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. rewrite Val.sub_add_opp. apply make_addimm_correct. (* rsubshift *) - InvApproxRegs; SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. econstructor; split; eauto. + InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. econstructor; split; eauto. (* mul *) - InvApproxRegs; SimplVMA. inv H0. rewrite H1. rewrite Val.mul_commut. apply make_mulimm_correct; auto. - InvApproxRegs; SimplVMA. inv H0. rewrite H. apply make_mulimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. fold (Val.mul (Vint n1) rs#r2). + rewrite Val.mul_commut. apply make_mulimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. apply make_mulimm_correct; auto. (* divs *) - assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto. + assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto. apply make_divimm_correct; auto. (* divu *) - assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto. + assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto. apply make_divuimm_correct; auto. (* and *) - InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.and_commut. apply make_andimm_correct. - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_andimm_correct. + InvApproxRegs; SimplVM. inv H0. fold (Val.and (Vint n1) rs#r2). rewrite Val.and_commut. apply make_andimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. apply make_andimm_correct; auto. (* andshift *) - InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_andimm_correct. + InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. apply make_andimm_correct; auto. (* or *) - InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.or_commut. apply make_orimm_correct. - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_orimm_correct. + InvApproxRegs; SimplVM. inv H0. fold (Val.or (Vint n1) rs#r2). rewrite Val.or_commut. apply make_orimm_correct. + InvApproxRegs; SimplVM. inv H0. apply make_orimm_correct. (* orshift *) - InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_orimm_correct. + InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. apply make_orimm_correct. (* xor *) - InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.xor_commut. apply make_xorimm_correct. - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_xorimm_correct. + InvApproxRegs; SimplVM. inv H0. fold (Val.xor (Vint n1) rs#r2). rewrite Val.xor_commut. apply make_xorimm_correct. + InvApproxRegs; SimplVM. inv H0. apply make_xorimm_correct. (* xorshift *) - InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_xorimm_correct. + InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. apply make_xorimm_correct. (* bic *) - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_andimm_correct. + InvApproxRegs; SimplVM. inv H0. apply make_andimm_correct; auto. (* bicshift *) - InvApproxRegs. SimplVMA. inv H0. rewrite H. rewrite eval_static_shift_correct. apply make_andimm_correct. + InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. apply make_andimm_correct; auto. (* shl *) - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_shlimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. apply make_shlimm_correct; auto. (* shr *) - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_shrimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. apply make_shrimm_correct; auto. (* shru *) - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_shruimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. apply make_shruimm_correct; auto. +(* singleoffloat *) + InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto. (* cmp *) generalize (cond_strength_reduction_correct c args0 vl0). destruct (cond_strength_reduction c args0 vl0) as [c' args']; intros. rewrite <- H1 in H0; auto. econstructor; split; eauto. (* mulf *) - inv H0. assert (rs#r2 = Vfloat n2). InvApproxRegs; SimplVMA; auto. - apply make_mulfimm_correct; auto. - inv H0. assert (rs#r1 = Vfloat n1). InvApproxRegs; SimplVMA; auto. - apply make_mulfimm_correct_2; auto. + InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) rs#r2). + rewrite <- H2. apply make_mulfimm_correct_2; auto. (* default *) exists v; auto. Qed. - + Lemma addr_strength_reduction_correct: - forall addr args vl, - vl = approx_regs app args -> + forall addr args vl res, + vl = map (fun r => AE.get r ae) args -> + eval_addressing ge (Vptr sp Int.zero) addr rs##args = Some res -> let (addr', args') := addr_strength_reduction addr args vl in - eval_addressing ge sp addr' rs##args' = eval_addressing ge sp addr rs##args. + exists res', eval_addressing ge (Vptr sp Int.zero) addr' rs##args' = Some res' /\ Val.lessdef res res'. Proof. - intros until vl. unfold addr_strength_reduction. - destruct (addr_strength_reduction_match addr args vl); simpl; intros; InvApproxRegs; SimplVMA. - rewrite H; rewrite H0. rewrite Val.add_assoc; auto. - rewrite H; rewrite H0. rewrite Val.add_permut; auto. - rewrite H0. rewrite Val.add_commut. auto. - rewrite H. auto. - rewrite H; rewrite H0. rewrite Val.add_assoc. rewrite eval_static_shift_correct. auto. - rewrite H. rewrite eval_static_shift_correct. auto. - rewrite H. rewrite Val.add_assoc. auto. - auto. + intros until res. unfold addr_strength_reduction. + destruct (addr_strength_reduction_match addr args vl); simpl; + intros VL EA; InvApproxRegs; SimplVM; try (inv EA). +- rewrite Int.add_zero_l. + change (Vptr sp (Int.add n1 n2)) with (Val.add (Vptr sp n1) (Vint n2)). + econstructor; split; eauto. apply Val.add_lessdef; auto. +- fold (Val.add (Vint n1) rs#r2). rewrite Int.add_zero_l. rewrite Int.add_commut. + change (Vptr sp (Int.add n2 n1)) with (Val.add (Vptr sp n2) (Vint n1)). + rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto. +- fold (Val.add (Vint n1) rs#r2). + rewrite Val.add_commut. econstructor; split; eauto. +- econstructor; split; eauto. +- rewrite eval_static_shift_correct. rewrite Int.add_zero_l. + change (Vptr sp (Int.add n1 (eval_static_shift s n2))) + with (Val.add (Vptr sp n1) (Vint (eval_static_shift s n2))). + econstructor; split; eauto. apply Val.add_lessdef; auto. +- rewrite eval_static_shift_correct. econstructor; split; eauto. +- rewrite Int.add_zero_l. change (Vptr sp (Int.add n1 n)) with (Val.add (Vptr sp n1) (Vint n)). + econstructor; split; eauto. apply Val.add_lessdef; auto. +- exists res; auto. Qed. End STRENGTH_REDUCTION. - -End ANALYSIS. diff --git a/arm/NeedOp.v b/arm/NeedOp.v new file mode 100644 index 0000000..3fb0d72 --- /dev/null +++ b/arm/NeedOp.v @@ -0,0 +1,204 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Op. +Require Import NeedDomain. +Require Import RTL. + +(** Neededness analysis for ARM operators *) + +Definition needs_of_condition (cond: condition): list nval := nil. + +Definition needs_of_shift (s: shift) (nv: nval): nval := + match s with + | Slsl x => shlimm nv x + | Slsr x => shruimm nv x + | Sasr x => shrimm nv x + | Sror x => ror nv x + end. + +Definition op1 (nv: nval) := nv :: nil. +Definition op2 (nv: nval) := nv :: nv :: nil. +Definition op2shift (s: shift) (nv: nval) := nv :: needs_of_shift s nv :: nil. + +Definition needs_of_operation (op: operation) (nv: nval): list nval := + match op with + | Omove => nv::nil + | Ointconst n => nil + | Ofloatconst n => nil + | Oaddrsymbol id ofs => nil + | Oaddrstack ofs => nil + | Ocast8signed => op1 (sign_ext 8 nv) + | Ocast16signed => op1 (sign_ext 16 nv) + | Oadd => op2 (modarith nv) + | Oaddshift s => op2shift s (modarith nv) + | Oaddimm _ => op1 (modarith nv) + | Osub => op2 (default nv) + | Osubshift s => op2shift s (default nv) + | Orsubshift s => op2shift s (default nv) + | Orsubimm _ => op1 (default nv) + | Omul => op2 (modarith nv) + | Omla => let n := modarith nv in let n2 := modarith n in n2::n2::n::nil + | Omulhu | Omulhs | Odiv | Odivu => let n := default nv in n::n::nil + | Oand => op2 (bitwise nv) + | Oandshift s => op2shift s (bitwise nv) + | Oandimm n => op1 (andimm nv n) + | Oor => op2 (bitwise nv) + | Oorshift s => op2shift s (bitwise nv) + | Oorimm n => op1 (orimm nv n) + | Oxor => op2 (bitwise nv) + | Oxorshift s => op2shift s (bitwise nv) + | Oxorimm n => op1 (bitwise nv) + | Obic => let n := bitwise nv in n::bitwise n::nil + | Obicshift s => let n := bitwise nv in n::needs_of_shift s (bitwise n)::nil + | Onot => op1 (bitwise nv) + | Onotshift s => op1 (needs_of_shift s (bitwise nv)) + | Oshl | Oshr | Oshru => op2 (default nv) + | Oshift s => op1 (needs_of_shift s nv) + | Oshrximm _ => op1 (default nv) + | Onegf | Oabsf => op1 (default nv) + | Oaddf | Osubf | Omulf | Odivf => op2 (default nv) + | Osingleoffloat => op1 (singleoffloat nv) + | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv) + | Omakelong => op2 (default nv) + | Olowlong | Ohighlong => op1 (default nv) + | Ocmp c => needs_of_condition c + end. + +Definition operation_is_redundant (op: operation) (nv: nval): bool := + match op with + | Ocast8signed => sign_ext_redundant 8 nv + | Ocast16signed => sign_ext_redundant 16 nv + | Oandimm n => andimm_redundant nv n + | Oorimm n => orimm_redundant nv n + | Osingleoffloat => singleoffloat_redundant nv + | _ => false + end. + +Ltac InvAgree := + match goal with + | [H: vagree_list nil _ _ |- _ ] => inv H; InvAgree + | [H: vagree_list (_::_) _ _ |- _ ] => inv H; InvAgree + | _ => idtac + end. + +Ltac TrivialExists := + match goal with + | [ |- exists v, Some ?x = Some v /\ _ ] => exists x; split; auto + | _ => idtac + end. + +Section SOUNDNESS. + +Variable ge: genv. +Variable sp: block. +Variables m m': mem. +Hypothesis PERM: forall b ofs k p, Mem.perm m b ofs k p -> Mem.perm m' b ofs k p. + +Lemma needs_of_condition_sound: + forall cond args b args', + eval_condition cond args m = Some b -> + vagree_list args args' (needs_of_condition cond) -> + eval_condition cond args' m' = Some b. +Proof. + intros. unfold needs_of_condition in H0. + eapply default_needs_of_condition_sound; eauto. +Qed. + +Lemma needs_of_shift_sound: + forall v v' s nv, + vagree v v' (needs_of_shift s nv) -> + vagree (eval_shift s v) (eval_shift s v') nv. +Proof. + intros. destruct s; simpl in *. + apply shlimm_sound; auto. + apply shruimm_sound; auto. + apply shrimm_sound; auto. + apply ror_sound; auto. +Qed. + +Lemma val_sub_lessdef: + forall v1 v1' v2 v2', + Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Val.lessdef (Val.sub v1 v2) (Val.sub v1' v2'). +Proof. + intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto. +Qed. + +Lemma needs_of_operation_sound: + forall op args v nv args', + eval_operation ge (Vptr sp Int.zero) op args m = Some v -> + vagree_list args args' (needs_of_operation op nv) -> + nv <> Nothing -> + exists v', + eval_operation ge (Vptr sp Int.zero) op args' m' = Some v' + /\ vagree v v' nv. +Proof. + unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail); + simpl in *; FuncInv; InvAgree; TrivialExists. +- apply sign_ext_sound; auto. compute; auto. +- apply sign_ext_sound; auto. compute; auto. +- apply add_sound; auto. +- apply add_sound; auto. apply needs_of_shift_sound; auto. +- apply add_sound; auto with na. +- replace (default nv) with All in *. + apply vagree_lessdef. apply val_sub_lessdef; auto with na. + apply lessdef_vagree. apply needs_of_shift_sound; auto with na. + destruct nv; simpl; congruence. +- replace (default nv) with All in *. + apply vagree_lessdef. apply val_sub_lessdef; auto with na. + apply lessdef_vagree. apply needs_of_shift_sound; auto with na. + destruct nv; simpl; congruence. +- apply mul_sound; auto. +- apply add_sound; auto. apply mul_sound; auto. +- apply and_sound; auto. +- apply and_sound; auto. apply needs_of_shift_sound; auto. +- apply andimm_sound; auto. +- apply or_sound; auto. +- apply or_sound; auto. apply needs_of_shift_sound; auto. +- apply orimm_sound; auto. +- apply xor_sound; auto. +- apply xor_sound; auto. apply needs_of_shift_sound; auto. +- apply xor_sound; auto with na. +- apply and_sound; auto. apply notint_sound; auto. +- apply and_sound; auto. apply notint_sound. apply needs_of_shift_sound; auto. +- apply notint_sound; auto. +- apply notint_sound. apply needs_of_shift_sound; auto. +- apply needs_of_shift_sound; auto. +- apply singleoffloat_sound; auto. +Qed. + +Lemma operation_is_redundant_sound: + forall op nv arg1 args v arg1' args', + operation_is_redundant op nv = true -> + eval_operation ge (Vptr sp Int.zero) op (arg1 :: args) m = Some v -> + vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) -> + vagree v arg1' nv. +Proof. + intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst. +- apply sign_ext_redundant_sound; auto. omega. +- apply sign_ext_redundant_sound; auto. omega. +- apply andimm_redundant_sound; auto. +- apply orimm_redundant_sound; auto. +- apply singleoffloat_redundant_sound; auto. +Qed. + +End SOUNDNESS. + + + diff --git a/arm/Op.v b/arm/Op.v index fe97d36..7323abc 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -73,6 +73,8 @@ Inductive operation : Type := | Oaddrsymbol: ident -> int -> operation (**r [rd] is set to the the address of the symbol plus the offset *) | Oaddrstack: int -> operation (**r [rd] is set to the stack pointer plus the given offset *) (*c Integer arithmetic: *) + | Ocast8signed: operation (**r [rd] is 8-bit sign extension of [r1] *) + | Ocast16signed: operation (**r [rd] is 16-bit sign extension of [r1] *) | Oadd: operation (**r [rd = r1 + r2] *) | Oaddshift: shift -> operation (**r [rd = r1 + shifted r2] *) | Oaddimm: int -> operation (**r [rd = r1 + n] *) @@ -219,6 +221,8 @@ Definition eval_operation | Ofloatconst n, nil => Some (Vfloat n) | Oaddrsymbol s ofs, nil => Some (symbol_address genv s ofs) | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs)) + | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1) + | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1) | Oadd, v1 :: v2 :: nil => Some (Val.add v1 v2) | Oaddshift s, v1 :: v2 :: nil => Some (Val.add v1 (eval_shift s v2)) | Oaddimm n, v1 :: nil => Some (Val.add v1 (Vint n)) @@ -314,6 +318,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ofloatconst f => (nil, if Float.is_single_dec f then Tsingle else Tfloat) | Oaddrsymbol _ _ => (nil, Tint) | Oaddrstack _ => (nil, Tint) + | Ocast8signed => (Tint :: nil, Tint) + | Ocast16signed => (Tint :: nil, Tint) | Oadd => (Tint :: Tint :: nil, Tint) | Oaddshift _ => (Tint :: Tint :: nil, Tint) | Oaddimm _ => (Tint :: nil, Tint) @@ -393,6 +399,8 @@ Proof with (try exact I). destruct (Float.is_single_dec f); red; auto. unfold symbol_address. destruct (Genv.find_symbol genv i)... destruct sp... + destruct v0... + destruct v0... destruct v0; destruct v1... generalize (S s v1). destruct v0; destruct (eval_shift s v1); simpl; tauto. destruct v0... @@ -820,6 +828,8 @@ Lemma eval_operation_inj: Proof. intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. apply Values.val_add_inject; auto. + inv H4; simpl; auto. + inv H4; simpl; auto. apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. apply eval_shift_inj; auto. apply Values.val_add_inject; auto. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 6398ba3..99dfa46 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -106,9 +106,9 @@ let movimm oc dst n = match Asmgen.decompose_int n with | [] -> assert false | hd::tl as l -> - fprintf oc " mov %s, #%a\n" dst coqint hd + fprintf oc " mov %s, #%a\n" dst coqint hd; List.iter - (fun n -> fprintf oc " orr %s, %s, #%a" dst dst coqint n) + (fun n -> fprintf oc " orr %s, %s, #%a\n" dst dst coqint n) tl; List.length l @@ -116,9 +116,9 @@ let addimm oc dst src n = match Asmgen.decompose_int n with | [] -> assert false | hd::tl as l -> - fprintf oc " add %s, %s, #%a\n" dst src coqint hd + fprintf oc " add %s, %s, #%a\n" dst src coqint hd; List.iter - (fun n -> fprintf oc " add %s, %s, #%a" dst dst coqint n) + (fun n -> fprintf oc " add %s, %s, #%a\n" dst dst coqint n) tl; List.length l @@ -126,9 +126,9 @@ let subimm oc dst src n = match Asmgen.decompose_int n with | [] -> assert false | hd::tl as l -> - fprintf oc " sub %s, %s, #%a\n" dst src coqint hd + fprintf oc " sub %s, %s, #%a\n" dst src coqint hd; List.iter - (fun n -> fprintf oc " sub %s, %s, #%a" dst dst coqint n) + (fun n -> fprintf oc " sub %s, %s, #%a\n" dst dst coqint n) tl; List.length l @@ -425,7 +425,7 @@ let print_builtin_va_start oc r = Int32.add (next_arg_location 0 0 (!current_function_sig).sig_args) !current_function_stacksize in - let n = addimm oc "r14" "sp" (coqint_of_camlint ofs); + let n = addimm oc "r14" "sp" (coqint_of_camlint ofs) in fprintf oc " str r14, [%a, #0]\n" ireg r; n + 1 @@ -716,10 +716,10 @@ let print_instruction oc = function fprintf oc " mov r12, sp\n"; if (!current_function_sig).sig_cc.cc_vararg then begin fprintf oc " push {r0, r1, r2, r3}\n"; - cfi_adjust oc 16 + cfi_adjust oc 16l end; let sz' = camlint_of_coqint sz in - let ninstr = subimm "sp" "sp" sz in + let ninstr = subimm oc "sp" "sp" sz in cfi_adjust oc sz'; fprintf oc " str r12, [sp, #%a]\n" coqint ofs; current_function_stacksize := sz'; @@ -727,7 +727,7 @@ let print_instruction oc = function | Pfreeframe(sz, ofs) -> let sz = if (!current_function_sig).sig_cc.cc_vararg - then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz) + then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz)) else sz in if Asmgen.is_immed_arith sz then fprintf oc " add sp, sp, #%a\n" coqint sz @@ -805,6 +805,7 @@ let rec print_instructions oc instrs = let print_function oc name fn = Hashtbl.clear current_function_labels; reset_constants(); + current_function_sig := fn.fn_sig; currpos := 0; let text = match C2C.atom_sections name with diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml index 4be41eb..96d1394 100644 --- a/arm/PrintOp.ml +++ b/arm/PrintOp.ml @@ -63,6 +63,8 @@ let print_operation reg pp = function fprintf pp "\"%s\" + %ld" (extern_atom id) (camlint_of_coqint ofs) | Oaddrstack ofs, [] -> fprintf pp "stack(%ld)" (camlint_of_coqint ofs) + | Ocast8signed, [r1] -> fprintf pp "int8signed(%a)" reg r1 + | Ocast16signed, [r1] -> fprintf pp "int16signed(%a)" reg r1 | Oadd, [r1;r2] -> fprintf pp "%a + %a" reg r1 reg r2 | Oaddshift s, [r1;r2] -> fprintf pp "%a + %a %a" reg r1 reg r2 shift s | Oaddimm n, [r1] -> fprintf pp "%a + %ld" reg r1 (camlint_of_coqint n) diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index 4cd09d1..767e747 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -369,11 +369,11 @@ Definition compf (c: comparison) (e1: expr) (e2: expr) := Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e. -Definition cast8signed (e: expr) := shrimm (shlimm e (Int.repr 24)) (Int.repr 24). +Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil). Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e. -Definition cast16signed (e: expr) := shrimm (shlimm e (Int.repr 16)) (Int.repr 16). +Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil). (** ** Floating-point conversions *) diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index 9beb1ad..9fbab44 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -716,12 +716,7 @@ Qed. Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8). Proof. - red; intros. unfold cast8signed. - exploit (eval_shlimm (Int.repr 24)); eauto. intros [v1 [A1 B1]]. - exploit (eval_shrimm (Int.repr 24)). eexact A1. intros [v2 [A2 B2]]. - exists v2; split; auto. - destruct x; simpl; auto. simpl in *. inv B1. simpl in *. inv B2. - rewrite Int.sign_ext_shr_shl. auto. compute; auto. + red; intros. unfold cast8signed. TrivialExists. Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). @@ -732,12 +727,7 @@ Qed. Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16). Proof. - red; intros. unfold cast16signed. - exploit (eval_shlimm (Int.repr 16)); eauto. intros [v1 [A1 B1]]. - exploit (eval_shrimm (Int.repr 16)). eexact A1. intros [v2 [A2 B2]]. - exists v2; split; auto. - destruct x; simpl; auto. simpl in *. inv B1. simpl in *. inv B2. - rewrite Int.sign_ext_shr_shl. auto. compute; auto. + red; intros. unfold cast16signed. TrivialExists. Qed. Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16). diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v new file mode 100644 index 0000000..c968213 --- /dev/null +++ b/arm/ValueAOp.v @@ -0,0 +1,193 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Op. +Require Import ValueDomain. +Require Import RTL. + +(** Value analysis for ARM operators *) + +Definition eval_static_shift (s: shift) (v: aval): aval := + match s with + | Slsl x => shl v (I x) + | Slsr x => shru v (I x) + | Sasr x => shr v (I x) + | Sror x => ror v (I x) + end. + +Definition eval_static_condition (cond: condition) (vl: list aval): abool := + match cond, vl with + | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2 + | Ccompu c, v1 :: v2 :: nil => cmpu_bool c v1 v2 + | Ccompshift c s, v1 :: v2 :: nil => cmp_bool c v1 (eval_static_shift s v2) + | Ccompushift c s, v1 :: v2 :: nil => cmpu_bool c v1 (eval_static_shift s v2) + | Ccompimm c n, v1 :: nil => cmp_bool c v1 (I n) + | Ccompuimm c n, v1 :: nil => cmpu_bool c v1 (I n) + | Ccompf c, v1 :: v2 :: nil => cmpf_bool c v1 v2 + | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) + | Ccompfzero c, v1 :: nil => cmpf_bool c v1 (F Float.zero) + | Cnotcompfzero c, v1 :: nil => cnot (cmpf_bool c v1 (F Float.zero)) + | _, _ => Bnone + end. + +Definition eval_static_addressing (addr: addressing) (vl: list aval): aval := + match addr, vl with + | Aindexed n, v1::nil => add v1 (I n) + | Aindexed2, v1::v2::nil => add v1 v2 + | Aindexed2shift s, v1::v2::nil => add v1 (eval_static_shift s v2) + | Ainstack ofs, nil => Ptr(Stk ofs) + | _, _ => Vbot + end. + +Definition eval_static_operation (op: operation) (vl: list aval): aval := + match op, vl with + | Omove, v1::nil => v1 + | Ointconst n, nil => I n + | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop + | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs) + | Oaddrstack ofs, nil => Ptr (Stk ofs) + | Ocast8signed, v1 :: nil => sign_ext 8 v1 + | Ocast16signed, v1 :: nil => sign_ext 16 v1 + | Oadd, v1::v2::nil => add v1 v2 + | Oaddshift s, v1::v2::nil => add v1 (eval_static_shift s v2) + | Oaddimm n, v1::nil => add v1 (I n) + | Osub, v1::v2::nil => sub v1 v2 + | Osubshift s, v1::v2::nil => sub v1 (eval_static_shift s v2) + | Orsubshift s, v1::v2::nil => sub (eval_static_shift s v2) v1 + | Orsubimm n, v1::nil => sub (I n) v1 + | Omul, v1::v2::nil => mul v1 v2 + | Omla, v1::v2::v3::nil => add (mul v1 v2) v3 + | Omulhs, v1::v2::nil => mulhs v1 v2 + | Omulhu, v1::v2::nil => mulhu v1 v2 + | Odiv, v1::v2::nil => divs v1 v2 + | Odivu, v1::v2::nil => divu v1 v2 + | Oand, v1::v2::nil => and v1 v2 + | Oandshift s, v1::v2::nil => and v1 (eval_static_shift s v2) + | Oandimm n, v1::nil => and v1 (I n) + | Oor, v1::v2::nil => or v1 v2 + | Oorshift s, v1::v2::nil => or v1 (eval_static_shift s v2) + | Oorimm n, v1::nil => or v1 (I n) + | Oxor, v1::v2::nil => xor v1 v2 + | Oxorshift s, v1::v2::nil => xor v1 (eval_static_shift s v2) + | Oxorimm n, v1::nil => xor v1 (I n) + | Obic, v1::v2::nil => and v1 (notint v2) + | Obicshift s, v1::v2::nil => and v1 (notint (eval_static_shift s v2)) + | Onot, v1::nil => notint v1 + | Onotshift s, v1::nil => notint (eval_static_shift s v1) + | Oshl, v1::v2::nil => shl v1 v2 + | Oshr, v1::v2::nil => shr v1 v2 + | Oshru, v1::v2::nil => shru v1 v2 + | Oshift s, v1::nil => eval_static_shift s v1 + | Oshrximm n, v1::nil => shrx v1 (I n) + | Onegf, v1::nil => negf v1 + | Oabsf, v1::nil => absf v1 + | Oaddf, v1::v2::nil => addf v1 v2 + | Osubf, v1::v2::nil => subf v1 v2 + | Omulf, v1::v2::nil => mulf v1 v2 + | Odivf, v1::v2::nil => divf v1 v2 + | Osingleoffloat, v1::nil => singleoffloat v1 + | Ointoffloat, v1::nil => intoffloat v1 + | Ointuoffloat, v1::nil => intuoffloat v1 + | Ofloatofint, v1::nil => floatofint v1 + | Ofloatofintu, v1::nil => floatofintu v1 + | Omakelong, v1::v2::nil => longofwords v1 v2 + | Olowlong, v1::nil => loword v1 + | Ohighlong, v1::nil => hiword v1 + | Ocmp c, _ => of_optbool (eval_static_condition c vl) + | _, _ => Vbot + end. + +Section SOUNDNESS. + +Variable bc: block_classification. +Variable ge: genv. +Hypothesis GENV: genv_match bc ge. +Variable sp: block. +Hypothesis STACK: bc sp = BCstack. + +Lemma eval_static_shift_sound: + forall s v a, + vmatch bc v a -> + vmatch bc (eval_shift s v) (eval_static_shift s a). +Proof. + intros. unfold eval_shift, eval_static_shift. destruct s; eauto with va. +Qed. + +Hint Resolve eval_static_shift_sound: va. + +Theorem eval_static_condition_sound: + forall cond vargs m aargs, + list_forall2 (vmatch bc) vargs aargs -> + cmatch (eval_condition cond vargs m) (eval_static_condition cond aargs). +Proof. + intros until aargs; intros VM. + inv VM. + destruct cond; auto with va. + inv H0. + destruct cond; simpl; eauto with va. + inv H2. + destruct cond; simpl; eauto with va. + destruct cond; auto with va. +Qed. + +Lemma symbol_address_sound: + forall id ofs, + vmatch bc (symbol_address ge id ofs) (Ptr (Gl id ofs)). +Proof. + intros; apply symbol_address_sound; apply GENV. +Qed. + +Hint Resolve symbol_address_sound: va. + +Ltac InvHyps := + match goal with + | [H: None = Some _ |- _ ] => discriminate + | [H: Some _ = Some _ |- _] => inv H + | [H1: match ?vl with nil => _ | _ :: _ => _ end = Some _ , + H2: list_forall2 _ ?vl _ |- _ ] => inv H2; InvHyps + | _ => idtac + end. + +Theorem eval_static_addressing_sound: + forall addr vargs vres aargs, + eval_addressing ge (Vptr sp Int.zero) addr vargs = Some vres -> + list_forall2 (vmatch bc) vargs aargs -> + vmatch bc vres (eval_static_addressing addr aargs). +Proof. + unfold eval_addressing, eval_static_addressing; intros; + destruct addr; InvHyps; eauto with va. + rewrite Int.add_zero_l; auto with va. +Qed. + +Theorem eval_static_operation_sound: + forall op vargs m vres aargs, + eval_operation ge (Vptr sp Int.zero) op vargs m = Some vres -> + list_forall2 (vmatch bc) vargs aargs -> + vmatch bc vres (eval_static_operation op aargs). +Proof. + unfold eval_operation, eval_static_operation; intros; + destruct op; InvHyps; eauto with va. + destruct (propagate_float_constants tt); constructor. + rewrite Int.add_zero_l; eauto with va. + fold (Val.sub (Vint i) a1). auto with va. + apply of_optbool_sound. eapply eval_static_condition_sound; eauto. +Qed. + +End SOUNDNESS. + -- cgit v1.2.3