From c4877832826fa26aea9c236f16bdc2de16c98150 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 15 Jan 2012 08:57:09 +0000 Subject: Added volatile_read_global and volatile_store_global builtins. Finished updating IA32 and ARM ports. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1792 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/ConstpropOp.v | 800 ------------------------------ arm/ConstpropOp.vp | 301 ++++++++++++ arm/ConstpropOpproof.v | 14 + arm/PrintOp.ml | 4 - arm/SelectOp.v | 1169 -------------------------------------------- arm/SelectOp.vp | 444 +++++++++++++++++ backend/Constprop.v | 3 + backend/Constpropproof.v | 10 +- cfrontend/Cexec.v | 90 +++- common/AST.v | 10 + common/Events.v | 176 +++++++ common/PrintAST.ml | 6 + ia32/ConstpropOp.v | 805 ------------------------------ ia32/ConstpropOp.vp | 314 ++++++++++++ ia32/ConstpropOpproof.v | 19 + ia32/PrintAsm.ml | 97 ++-- powerpc/ConstpropOp.vp | 11 + powerpc/ConstpropOpproof.v | 19 + powerpc/PrintAsm.ml | 94 ++-- 19 files changed, 1528 insertions(+), 2858 deletions(-) delete mode 100644 arm/ConstpropOp.v create mode 100644 arm/ConstpropOp.vp delete mode 100644 arm/SelectOp.v create mode 100644 arm/SelectOp.vp delete mode 100644 ia32/ConstpropOp.v create mode 100644 ia32/ConstpropOp.vp diff --git a/arm/ConstpropOp.v b/arm/ConstpropOp.v deleted file mode 100644 index 9e51e251..00000000 --- a/arm/ConstpropOp.v +++ /dev/null @@ -1,800 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Static analysis and strength reduction for operators - and conditions. This is the machine-dependent part of [Constprop]. *) - -Require Import Coqlib. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Op. -Require Import Registers. - -(** * 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. *) - | 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. *) - - -(** 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. - - 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. *) - -Definition eval_static_shift (s: shift) (n: int) : int := - match s with - | Slsl x => Int.shl n x - | Slsr x => Int.shru n x - | Sasr x => Int.shr n x - | Sror x => Int.ror n x - end. - -(** Original definition: -<< -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)) - | _, _ => None - end. ->> -*) - -Inductive eval_static_condition_cases: forall (cond: condition) (vl: list approx), Type := - | eval_static_condition_case1: forall c n1 n2, eval_static_condition_cases (Ccomp c) (I n1 :: I n2 :: nil) - | eval_static_condition_case2: forall c n1 n2, eval_static_condition_cases (Ccompu c) (I n1 :: I n2 :: nil) - | eval_static_condition_case3: forall c s n1 n2, eval_static_condition_cases (Ccompshift c s) (I n1 :: I n2 :: nil) - | eval_static_condition_case4: forall c s n1 n2, eval_static_condition_cases (Ccompushift c s) (I n1 :: I n2 :: nil) - | eval_static_condition_case5: forall c n n1, eval_static_condition_cases (Ccompimm c n) (I n1 :: nil) - | eval_static_condition_case6: forall c n n1, eval_static_condition_cases (Ccompuimm c n) (I n1 :: nil) - | eval_static_condition_case7: forall c n1 n2, eval_static_condition_cases (Ccompf c) (F n1 :: F n2 :: nil) - | eval_static_condition_case8: forall c n1 n2, eval_static_condition_cases (Cnotcompf c) (F n1 :: F n2 :: nil) - | eval_static_condition_default: forall (cond: condition) (vl: list approx), eval_static_condition_cases cond vl. - -Definition eval_static_condition_match (cond: condition) (vl: list approx) := - match cond as zz1, vl as zz2 return eval_static_condition_cases zz1 zz2 with - | Ccomp c, I n1 :: I n2 :: nil => eval_static_condition_case1 c n1 n2 - | Ccompu c, I n1 :: I n2 :: nil => eval_static_condition_case2 c n1 n2 - | Ccompshift c s, I n1 :: I n2 :: nil => eval_static_condition_case3 c s n1 n2 - | Ccompushift c s, I n1 :: I n2 :: nil => eval_static_condition_case4 c s n1 n2 - | Ccompimm c n, I n1 :: nil => eval_static_condition_case5 c n n1 - | Ccompuimm c n, I n1 :: nil => eval_static_condition_case6 c n n1 - | Ccompf c, F n1 :: F n2 :: nil => eval_static_condition_case7 c n1 n2 - | Cnotcompf c, F n1 :: F n2 :: nil => eval_static_condition_case8 c n1 n2 - | cond, vl => eval_static_condition_default cond vl - end. - -Definition eval_static_condition (cond: condition) (vl: list approx) := - match eval_static_condition_match cond vl with - | eval_static_condition_case1 c n1 n2 => (* Ccomp c, I n1 :: I n2 :: nil *) - Some(Int.cmp c n1 n2) - | eval_static_condition_case2 c n1 n2 => (* Ccompu c, I n1 :: I n2 :: nil *) - Some(Int.cmpu c n1 n2) - | eval_static_condition_case3 c s n1 n2 => (* Ccompshift c s, I n1 :: I n2 :: nil *) - Some(Int.cmp c n1 (eval_static_shift s n2)) - | eval_static_condition_case4 c s n1 n2 => (* Ccompushift c s, I n1 :: I n2 :: nil *) - Some(Int.cmpu c n1 (eval_static_shift s n2)) - | eval_static_condition_case5 c n n1 => (* Ccompimm c n, I n1 :: nil *) - Some(Int.cmp c n1 n) - | eval_static_condition_case6 c n n1 => (* Ccompuimm c n, I n1 :: nil *) - Some(Int.cmpu c n1 n) - | eval_static_condition_case7 c n1 n2 => (* Ccompf c, F n1 :: F n2 :: nil *) - Some(Float.cmp c n1 n2) - | eval_static_condition_case8 c n1 n2 => (* Cnotcompf c, F n1 :: F n2 :: nil *) - Some(negb(Float.cmp c n1 n2)) - | eval_static_condition_default cond vl => - 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. - -(** Original definition: -<< -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 => F n - | 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) - | Odiv, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero 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 => F(Float.floatofint n1) - | Ofloatofintu, I n1 :: nil => F(Float.floatofintu n1) - | Ocmp c, vl => eval_static_condition_val c vl - | _, _ => Unknown - end. ->> -*) - -Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), Type := - | eval_static_operation_case1: forall v1, eval_static_operation_cases (Omove) (v1::nil) - | eval_static_operation_case2: forall n, eval_static_operation_cases (Ointconst n) (nil) - | eval_static_operation_case3: forall n, eval_static_operation_cases (Ofloatconst n) (nil) - | eval_static_operation_case4: forall s n, eval_static_operation_cases (Oaddrsymbol s n) (nil) - | eval_static_operation_case5: forall n, eval_static_operation_cases (Oaddrstack n) (nil) - | eval_static_operation_case6: forall n1 n2, eval_static_operation_cases (Oadd) (I n1 :: I n2 :: nil) - | eval_static_operation_case7: forall s n1 n2, eval_static_operation_cases (Oaddshift s) (I n1 :: I n2 :: nil) - | eval_static_operation_case8: forall s1 n1 n2, eval_static_operation_cases (Oadd) (G s1 n1 :: I n2 :: nil) - | eval_static_operation_case9: forall s s1 n1 n2, eval_static_operation_cases (Oaddshift s) (G s1 n1 :: I n2 :: nil) - | eval_static_operation_case10: forall n1 n2, eval_static_operation_cases (Oadd) (S n1 :: I n2 :: nil) - | eval_static_operation_case11: forall s n1 n2, eval_static_operation_cases (Oaddshift s) (S n1 :: I n2 :: nil) - | eval_static_operation_case12: forall n1 s2 n2, eval_static_operation_cases (Oadd) (I n1 :: G s2 n2 :: nil) - | eval_static_operation_case13: forall n1 n2, eval_static_operation_cases (Oadd) (I n1 :: S n2 :: nil) - | eval_static_operation_case14: forall n n1, eval_static_operation_cases (Oaddimm n) (I n1 :: nil) - | eval_static_operation_case15: forall n s1 n1, eval_static_operation_cases (Oaddimm n) (G s1 n1 :: nil) - | eval_static_operation_case16: forall n n1, eval_static_operation_cases (Oaddimm n) (S n1 :: nil) - | eval_static_operation_case17: forall n1 n2, eval_static_operation_cases (Osub) (I n1 :: I n2 :: nil) - | eval_static_operation_case18: forall s n1 n2, eval_static_operation_cases (Osubshift s) (I n1 :: I n2 :: nil) - | eval_static_operation_case19: forall s1 n1 n2, eval_static_operation_cases (Osub) (G s1 n1 :: I n2 :: nil) - | eval_static_operation_case20: forall n1 n2, eval_static_operation_cases (Osub) (S n1 :: I n2 :: nil) - | eval_static_operation_case21: forall s s1 n1 n2, eval_static_operation_cases (Osubshift s) (G s1 n1 :: I n2 :: nil) - | eval_static_operation_case22: forall s n1 n2, eval_static_operation_cases (Orsubshift s) (I n1 :: I n2 :: nil) - | eval_static_operation_case23: forall n n1, eval_static_operation_cases (Orsubimm n) (I n1 :: nil) - | eval_static_operation_case24: forall n1 n2, eval_static_operation_cases (Omul) (I n1 :: I n2 :: nil) - | eval_static_operation_case25: forall n1 n2, eval_static_operation_cases (Odiv) (I n1 :: I n2 :: nil) - | eval_static_operation_case26: forall n1 n2, eval_static_operation_cases (Odivu) (I n1 :: I n2 :: nil) - | eval_static_operation_case27: forall n1 n2, eval_static_operation_cases (Oand) (I n1 :: I n2 :: nil) - | eval_static_operation_case28: forall s n1 n2, eval_static_operation_cases (Oandshift s) (I n1 :: I n2 :: nil) - | eval_static_operation_case29: forall n n1, eval_static_operation_cases (Oandimm n) (I n1 :: nil) - | eval_static_operation_case30: forall n1 n2, eval_static_operation_cases (Oor) (I n1 :: I n2 :: nil) - | eval_static_operation_case31: forall s n1 n2, eval_static_operation_cases (Oorshift s) (I n1 :: I n2 :: nil) - | eval_static_operation_case32: forall n n1, eval_static_operation_cases (Oorimm n) (I n1 :: nil) - | eval_static_operation_case33: forall n1 n2, eval_static_operation_cases (Oxor) (I n1 :: I n2 :: nil) - | eval_static_operation_case34: forall s n1 n2, eval_static_operation_cases (Oxorshift s) (I n1 :: I n2 :: nil) - | eval_static_operation_case35: forall n n1, eval_static_operation_cases (Oxorimm n) (I n1 :: nil) - | eval_static_operation_case36: forall n1 n2, eval_static_operation_cases (Obic) (I n1 :: I n2 :: nil) - | eval_static_operation_case37: forall s n1 n2, eval_static_operation_cases (Obicshift s) (I n1 :: I n2 :: nil) - | eval_static_operation_case38: forall n1, eval_static_operation_cases (Onot) (I n1 :: nil) - | eval_static_operation_case39: forall s n1, eval_static_operation_cases (Onotshift s) (I n1 :: nil) - | eval_static_operation_case40: forall n1 n2, eval_static_operation_cases (Oshl) (I n1 :: I n2 :: nil) - | eval_static_operation_case41: forall n1 n2, eval_static_operation_cases (Oshr) (I n1 :: I n2 :: nil) - | eval_static_operation_case42: forall n1 n2, eval_static_operation_cases (Oshru) (I n1 :: I n2 :: nil) - | eval_static_operation_case43: forall s n1, eval_static_operation_cases (Oshift s) (I n1 :: nil) - | eval_static_operation_case44: forall n1, eval_static_operation_cases (Onegf) (F n1 :: nil) - | eval_static_operation_case45: forall n1, eval_static_operation_cases (Oabsf) (F n1 :: nil) - | eval_static_operation_case46: forall n1 n2, eval_static_operation_cases (Oaddf) (F n1 :: F n2 :: nil) - | eval_static_operation_case47: forall n1 n2, eval_static_operation_cases (Osubf) (F n1 :: F n2 :: nil) - | eval_static_operation_case48: forall n1 n2, eval_static_operation_cases (Omulf) (F n1 :: F n2 :: nil) - | eval_static_operation_case49: forall n1 n2, eval_static_operation_cases (Odivf) (F n1 :: F n2 :: nil) - | eval_static_operation_case50: forall n1, eval_static_operation_cases (Osingleoffloat) (F n1 :: nil) - | eval_static_operation_case51: forall n1, eval_static_operation_cases (Ointoffloat) (F n1 :: nil) - | eval_static_operation_case52: forall n1, eval_static_operation_cases (Ointuoffloat) (F n1 :: nil) - | eval_static_operation_case53: forall n1, eval_static_operation_cases (Ofloatofint) (I n1 :: nil) - | eval_static_operation_case54: forall n1, eval_static_operation_cases (Ofloatofintu) (I n1 :: nil) - | eval_static_operation_case55: forall c vl, eval_static_operation_cases (Ocmp c) (vl) - | eval_static_operation_default: forall (op: operation) (vl: list approx), eval_static_operation_cases op vl. - -Definition eval_static_operation_match (op: operation) (vl: list approx) := - match op as zz1, vl as zz2 return eval_static_operation_cases zz1 zz2 with - | Omove, v1::nil => eval_static_operation_case1 v1 - | Ointconst n, nil => eval_static_operation_case2 n - | Ofloatconst n, nil => eval_static_operation_case3 n - | Oaddrsymbol s n, nil => eval_static_operation_case4 s n - | Oaddrstack n, nil => eval_static_operation_case5 n - | Oadd, I n1 :: I n2 :: nil => eval_static_operation_case6 n1 n2 - | Oaddshift s, I n1 :: I n2 :: nil => eval_static_operation_case7 s n1 n2 - | Oadd, G s1 n1 :: I n2 :: nil => eval_static_operation_case8 s1 n1 n2 - | Oaddshift s, G s1 n1 :: I n2 :: nil => eval_static_operation_case9 s s1 n1 n2 - | Oadd, S n1 :: I n2 :: nil => eval_static_operation_case10 n1 n2 - | Oaddshift s, S n1 :: I n2 :: nil => eval_static_operation_case11 s n1 n2 - | Oadd, I n1 :: G s2 n2 :: nil => eval_static_operation_case12 n1 s2 n2 - | Oadd, I n1 :: S n2 :: nil => eval_static_operation_case13 n1 n2 - | Oaddimm n, I n1 :: nil => eval_static_operation_case14 n n1 - | Oaddimm n, G s1 n1 :: nil => eval_static_operation_case15 n s1 n1 - | Oaddimm n, S n1 :: nil => eval_static_operation_case16 n n1 - | Osub, I n1 :: I n2 :: nil => eval_static_operation_case17 n1 n2 - | Osubshift s, I n1 :: I n2 :: nil => eval_static_operation_case18 s n1 n2 - | Osub, G s1 n1 :: I n2 :: nil => eval_static_operation_case19 s1 n1 n2 - | Osub, S n1 :: I n2 :: nil => eval_static_operation_case20 n1 n2 - | Osubshift s, G s1 n1 :: I n2 :: nil => eval_static_operation_case21 s s1 n1 n2 - | Orsubshift s, I n1 :: I n2 :: nil => eval_static_operation_case22 s n1 n2 - | Orsubimm n, I n1 :: nil => eval_static_operation_case23 n n1 - | Omul, I n1 :: I n2 :: nil => eval_static_operation_case24 n1 n2 - | Odiv, I n1 :: I n2 :: nil => eval_static_operation_case25 n1 n2 - | Odivu, I n1 :: I n2 :: nil => eval_static_operation_case26 n1 n2 - | Oand, I n1 :: I n2 :: nil => eval_static_operation_case27 n1 n2 - | Oandshift s, I n1 :: I n2 :: nil => eval_static_operation_case28 s n1 n2 - | Oandimm n, I n1 :: nil => eval_static_operation_case29 n n1 - | Oor, I n1 :: I n2 :: nil => eval_static_operation_case30 n1 n2 - | Oorshift s, I n1 :: I n2 :: nil => eval_static_operation_case31 s n1 n2 - | Oorimm n, I n1 :: nil => eval_static_operation_case32 n n1 - | Oxor, I n1 :: I n2 :: nil => eval_static_operation_case33 n1 n2 - | Oxorshift s, I n1 :: I n2 :: nil => eval_static_operation_case34 s n1 n2 - | Oxorimm n, I n1 :: nil => eval_static_operation_case35 n n1 - | Obic, I n1 :: I n2 :: nil => eval_static_operation_case36 n1 n2 - | Obicshift s, I n1 :: I n2 :: nil => eval_static_operation_case37 s n1 n2 - | Onot, I n1 :: nil => eval_static_operation_case38 n1 - | Onotshift s, I n1 :: nil => eval_static_operation_case39 s n1 - | Oshl, I n1 :: I n2 :: nil => eval_static_operation_case40 n1 n2 - | Oshr, I n1 :: I n2 :: nil => eval_static_operation_case41 n1 n2 - | Oshru, I n1 :: I n2 :: nil => eval_static_operation_case42 n1 n2 - | Oshift s, I n1 :: nil => eval_static_operation_case43 s n1 - | Onegf, F n1 :: nil => eval_static_operation_case44 n1 - | Oabsf, F n1 :: nil => eval_static_operation_case45 n1 - | Oaddf, F n1 :: F n2 :: nil => eval_static_operation_case46 n1 n2 - | Osubf, F n1 :: F n2 :: nil => eval_static_operation_case47 n1 n2 - | Omulf, F n1 :: F n2 :: nil => eval_static_operation_case48 n1 n2 - | Odivf, F n1 :: F n2 :: nil => eval_static_operation_case49 n1 n2 - | Osingleoffloat, F n1 :: nil => eval_static_operation_case50 n1 - | Ointoffloat, F n1 :: nil => eval_static_operation_case51 n1 - | Ointuoffloat, F n1 :: nil => eval_static_operation_case52 n1 - | Ofloatofint, I n1 :: nil => eval_static_operation_case53 n1 - | Ofloatofintu, I n1 :: nil => eval_static_operation_case54 n1 - | Ocmp c, vl => eval_static_operation_case55 c vl - | op, vl => eval_static_operation_default op vl - end. - -Definition eval_static_operation (op: operation) (vl: list approx) := - match eval_static_operation_match op vl with - | eval_static_operation_case1 v1 => (* Omove, v1::nil *) - v1 - | eval_static_operation_case2 n => (* Ointconst n, nil *) - I n - | eval_static_operation_case3 n => (* Ofloatconst n, nil *) - F n - | eval_static_operation_case4 s n => (* Oaddrsymbol s n, nil *) - G s n - | eval_static_operation_case5 n => (* Oaddrstack n, nil *) - S n - | eval_static_operation_case6 n1 n2 => (* Oadd, I n1 :: I n2 :: nil *) - I(Int.add n1 n2) - | eval_static_operation_case7 s n1 n2 => (* Oaddshift s, I n1 :: I n2 :: nil *) - I(Int.add n1 (eval_static_shift s n2)) - | eval_static_operation_case8 s1 n1 n2 => (* Oadd, G s1 n1 :: I n2 :: nil *) - G s1 (Int.add n1 n2) - | eval_static_operation_case9 s s1 n1 n2 => (* Oaddshift s, G s1 n1 :: I n2 :: nil *) - G s1 (Int.add n1 (eval_static_shift s n2)) - | eval_static_operation_case10 n1 n2 => (* Oadd, S n1 :: I n2 :: nil *) - S (Int.add n1 n2) - | eval_static_operation_case11 s n1 n2 => (* Oaddshift s, S n1 :: I n2 :: nil *) - S (Int.add n1 (eval_static_shift s n2)) - | eval_static_operation_case12 n1 s2 n2 => (* Oadd, I n1 :: G s2 n2 :: nil *) - G s2 (Int.add n1 n2) - | eval_static_operation_case13 n1 n2 => (* Oadd, I n1 :: S n2 :: nil *) - S (Int.add n1 n2) - | eval_static_operation_case14 n n1 => (* Oaddimm n, I n1 :: nil *) - I (Int.add n1 n) - | eval_static_operation_case15 n s1 n1 => (* Oaddimm n, G s1 n1 :: nil *) - G s1 (Int.add n1 n) - | eval_static_operation_case16 n n1 => (* Oaddimm n, S n1 :: nil *) - S (Int.add n1 n) - | eval_static_operation_case17 n1 n2 => (* Osub, I n1 :: I n2 :: nil *) - I(Int.sub n1 n2) - | eval_static_operation_case18 s n1 n2 => (* Osubshift s, I n1 :: I n2 :: nil *) - I(Int.sub n1 (eval_static_shift s n2)) - | eval_static_operation_case19 s1 n1 n2 => (* Osub, G s1 n1 :: I n2 :: nil *) - G s1 (Int.sub n1 n2) - | eval_static_operation_case20 n1 n2 => (* Osub, S n1 :: I n2 :: nil *) - S (Int.sub n1 n2) - | eval_static_operation_case21 s s1 n1 n2 => (* Osubshift s, G s1 n1 :: I n2 :: nil *) - G s1 (Int.sub n1 (eval_static_shift s n2)) - | eval_static_operation_case22 s n1 n2 => (* Orsubshift s, I n1 :: I n2 :: nil *) - I(Int.sub (eval_static_shift s n2) n1) - | eval_static_operation_case23 n n1 => (* Orsubimm n, I n1 :: nil *) - I (Int.sub n n1) - | eval_static_operation_case24 n1 n2 => (* Omul, I n1 :: I n2 :: nil *) - I(Int.mul n1 n2) - | eval_static_operation_case25 n1 n2 => (* Odiv, I n1 :: I n2 :: nil *) - if Int.eq n2 Int.zero then Unknown else I(Int.divs n1 n2) - | eval_static_operation_case26 n1 n2 => (* Odivu, I n1 :: I n2 :: nil *) - if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2) - | eval_static_operation_case27 n1 n2 => (* Oand, I n1 :: I n2 :: nil *) - I(Int.and n1 n2) - | eval_static_operation_case28 s n1 n2 => (* Oandshift s, I n1 :: I n2 :: nil *) - I(Int.and n1 (eval_static_shift s n2)) - | eval_static_operation_case29 n n1 => (* Oandimm n, I n1 :: nil *) - I(Int.and n1 n) - | eval_static_operation_case30 n1 n2 => (* Oor, I n1 :: I n2 :: nil *) - I(Int.or n1 n2) - | eval_static_operation_case31 s n1 n2 => (* Oorshift s, I n1 :: I n2 :: nil *) - I(Int.or n1 (eval_static_shift s n2)) - | eval_static_operation_case32 n n1 => (* Oorimm n, I n1 :: nil *) - I(Int.or n1 n) - | eval_static_operation_case33 n1 n2 => (* Oxor, I n1 :: I n2 :: nil *) - I(Int.xor n1 n2) - | eval_static_operation_case34 s n1 n2 => (* Oxorshift s, I n1 :: I n2 :: nil *) - I(Int.xor n1 (eval_static_shift s n2)) - | eval_static_operation_case35 n n1 => (* Oxorimm n, I n1 :: nil *) - I(Int.xor n1 n) - | eval_static_operation_case36 n1 n2 => (* Obic, I n1 :: I n2 :: nil *) - I(Int.and n1 (Int.not n2)) - | eval_static_operation_case37 s n1 n2 => (* Obicshift s, I n1 :: I n2 :: nil *) - I(Int.and n1 (Int.not (eval_static_shift s n2))) - | eval_static_operation_case38 n1 => (* Onot, I n1 :: nil *) - I(Int.not n1) - | eval_static_operation_case39 s n1 => (* Onotshift s, I n1 :: nil *) - I(Int.not (eval_static_shift s n1)) - | eval_static_operation_case40 n1 n2 => (* Oshl, I n1 :: I n2 :: nil *) - if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown - | eval_static_operation_case41 n1 n2 => (* Oshr, I n1 :: I n2 :: nil *) - if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown - | eval_static_operation_case42 n1 n2 => (* Oshru, I n1 :: I n2 :: nil *) - if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown - | eval_static_operation_case43 s n1 => (* Oshift s, I n1 :: nil *) - I(eval_static_shift s n1) - | eval_static_operation_case44 n1 => (* Onegf, F n1 :: nil *) - F(Float.neg n1) - | eval_static_operation_case45 n1 => (* Oabsf, F n1 :: nil *) - F(Float.abs n1) - | eval_static_operation_case46 n1 n2 => (* Oaddf, F n1 :: F n2 :: nil *) - F(Float.add n1 n2) - | eval_static_operation_case47 n1 n2 => (* Osubf, F n1 :: F n2 :: nil *) - F(Float.sub n1 n2) - | eval_static_operation_case48 n1 n2 => (* Omulf, F n1 :: F n2 :: nil *) - F(Float.mul n1 n2) - | eval_static_operation_case49 n1 n2 => (* Odivf, F n1 :: F n2 :: nil *) - F(Float.div n1 n2) - | eval_static_operation_case50 n1 => (* Osingleoffloat, F n1 :: nil *) - F(Float.singleoffloat n1) - | eval_static_operation_case51 n1 => (* Ointoffloat, F n1 :: nil *) - eval_static_intoffloat n1 - | eval_static_operation_case52 n1 => (* Ointuoffloat, F n1 :: nil *) - eval_static_intuoffloat n1 - | eval_static_operation_case53 n1 => (* Ofloatofint, I n1 :: nil *) - F(Float.floatofint n1) - | eval_static_operation_case54 n1 => (* Ofloatofintu, I n1 :: nil *) - F(Float.floatofintu n1) - | eval_static_operation_case55 c vl => (* Ocmp c, vl *) - eval_static_condition_val c vl - | eval_static_operation_default op vl => - 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. - -(** Original definition: -<< -Nondetfunction cond_strength_reduction - (cond: condition) (args: list reg) (vl: list approx) := - match cond, args, vl with - | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => - (Ccompimm (swap_comparison c) n1, r2 :: nil) - | Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Ccompimm c n2, r1 :: nil) - | Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil => - (Ccompuimm (swap_comparison c) n1, r2 :: nil) - | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Ccompuimm c n2, r1 :: nil) - | Ccompshift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Ccompimm c (eval_static_shift s n2), r1 :: nil) - | Ccompushift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Ccompuimm c (eval_static_shift s n2), r1 :: nil) - | _, _, _ => - (cond, args) - end. ->> -*) - -Inductive cond_strength_reduction_cases: forall (cond: condition) (args: list reg) (vl: list approx), Type := - | cond_strength_reduction_case1: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | cond_strength_reduction_case2: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | cond_strength_reduction_case3: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccompu c) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | cond_strength_reduction_case4: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccompu c) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | cond_strength_reduction_case5: forall c s r1 r2 v1 n2, cond_strength_reduction_cases (Ccompshift c s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | cond_strength_reduction_case6: forall c s r1 r2 v1 n2, cond_strength_reduction_cases (Ccompushift c s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | cond_strength_reduction_default: forall (cond: condition) (args: list reg) (vl: list approx), cond_strength_reduction_cases cond args vl. - -Definition cond_strength_reduction_match (cond: condition) (args: list reg) (vl: list approx) := - match cond as zz1, args as zz2, vl as zz3 return cond_strength_reduction_cases zz1 zz2 zz3 with - | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => cond_strength_reduction_case1 c r1 r2 n1 v2 - | Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case2 c r1 r2 v1 n2 - | Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil => cond_strength_reduction_case3 c r1 r2 n1 v2 - | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case4 c r1 r2 v1 n2 - | Ccompshift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case5 c s r1 r2 v1 n2 - | Ccompushift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case6 c s r1 r2 v1 n2 - | cond, args, vl => cond_strength_reduction_default cond args vl - end. - -Definition cond_strength_reduction (cond: condition) (args: list reg) (vl: list approx) := - match cond_strength_reduction_match cond args vl with - | cond_strength_reduction_case1 c r1 r2 n1 v2 => (* Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - (Ccompimm (swap_comparison c) n1, r2 :: nil) - | cond_strength_reduction_case2 c r1 r2 v1 n2 => (* Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Ccompimm c n2, r1 :: nil) - | cond_strength_reduction_case3 c r1 r2 n1 v2 => (* Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - (Ccompuimm (swap_comparison c) n1, r2 :: nil) - | cond_strength_reduction_case4 c r1 r2 v1 n2 => (* Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Ccompuimm c n2, r1 :: nil) - | cond_strength_reduction_case5 c s r1 r2 v1 n2 => (* Ccompshift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Ccompimm c (eval_static_shift s n2), r1 :: nil) - | cond_strength_reduction_case6 c s r1 r2 v1 n2 => (* Ccompushift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Ccompuimm c (eval_static_shift s n2), r1 :: nil) - | cond_strength_reduction_default cond args vl => - (cond, args) - end. - - -Definition make_addimm (n: int) (r: reg) := - if Int.eq n Int.zero - then (Omove, r :: nil) - else (Oaddimm n, r :: nil). - -Definition make_shlimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then - (Omove, r1 :: nil) - else if Int.ltu n Int.iwordsize then - (Oshift (Slsl (mk_shift_amount n)), r1 :: nil) - else - (Oshl, r1 :: r2 :: nil). - -Definition make_shrimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then - (Omove, r1 :: nil) - else if Int.ltu n Int.iwordsize then - (Oshift (Sasr (mk_shift_amount n)), r1 :: nil) - else - (Oshr, r1 :: r2 :: nil). - -Definition make_shruimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then - (Omove, r1 :: nil) - else if Int.ltu n Int.iwordsize then - (Oshift (Slsr (mk_shift_amount n)), r1 :: nil) - else - (Oshru, r1 :: r2 :: nil). - -Definition make_mulimm (n: int) (r1 r2: reg) := - if Int.eq n Int.zero then - (Ointconst Int.zero, nil) - else if Int.eq n Int.one then - (Omove, r1 :: nil) - else - match Int.is_power2 n with - | Some l => (Oshift (Slsl (mk_shift_amount l)), r1 :: nil) - | None => (Omul, r1 :: r2 :: nil) - end. - -Definition make_divimm (n: int) (r1 r2: reg) := - match Int.is_power2 n with - | Some l => if Int.ltu l (Int.repr 31) - then (Oshrximm l, r1 :: nil) - else (Odiv, r1 :: r2 :: nil) - | None => (Odiv, r1 :: r2 :: nil) - end. - -Definition make_divuimm (n: int) (r1 r2: reg) := - match Int.is_power2 n with - | Some l => (Oshift (Slsr (mk_shift_amount l)), r1 :: nil) - | None => (Odivu, r1 :: r2 :: nil) - end. - -Definition make_andimm (n: int) (r: reg) := - if Int.eq n Int.zero then (Ointconst Int.zero, nil) - else if Int.eq n Int.mone then (Omove, r :: nil) - else (Oandimm n, r :: nil). - -Definition make_orimm (n: int) (r: reg) := - if Int.eq n Int.zero then (Omove, r :: nil) - else if Int.eq n Int.mone then (Ointconst Int.mone, nil) - else (Oorimm n, r :: nil). - -Definition make_xorimm (n: int) (r: reg) := - if Int.eq n Int.zero then (Omove, r :: nil) - else if Int.eq n Int.mone then (Onot, r :: nil) - else (Oxorimm n, r :: nil). - -(** Original definition: -<< -Nondetfunction op_strength_reduction - (op: operation) (args: list reg) (vl: list approx) := - match op, args, vl with - | 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 - | Osub, r1 :: r2 :: nil, I n1 :: v2 :: nil => (Orsubimm n1, r2 :: nil) - | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg n2) r1 - | Osubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg (eval_static_shift s n2)) r1 - | Orsubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Orsubimm (eval_static_shift s n2), r1 :: nil) - | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_mulimm n1 r2 r1 - | 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 - | 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 - | 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 - | Ocmp c, args, vl => - let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args') - | _, _, _ => (op, args) - end. ->> -*) - -Inductive op_strength_reduction_cases: forall (op: operation) (args: list reg) (vl: list approx), Type := - | op_strength_reduction_case1: forall r1 r2 n1 v2, op_strength_reduction_cases (Oadd) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case2: forall r1 r2 v1 n2, op_strength_reduction_cases (Oadd) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case3: forall s r1 r2 v1 n2, op_strength_reduction_cases (Oaddshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case4: forall r1 r2 n1 v2, op_strength_reduction_cases (Osub) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case5: forall r1 r2 v1 n2, op_strength_reduction_cases (Osub) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case6: forall s r1 r2 v1 n2, op_strength_reduction_cases (Osubshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case7: forall s r1 r2 v1 n2, op_strength_reduction_cases (Orsubshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case8: forall r1 r2 n1 v2, op_strength_reduction_cases (Omul) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case9: forall r1 r2 v1 n2, op_strength_reduction_cases (Omul) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case10: forall r1 r2 v1 n2, op_strength_reduction_cases (Odiv) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case11: forall r1 r2 v1 n2, op_strength_reduction_cases (Odivu) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case12: forall r1 r2 n1 v2, op_strength_reduction_cases (Oand) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case13: forall r1 r2 v1 n2, op_strength_reduction_cases (Oand) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case14: forall s r1 r2 v1 n2, op_strength_reduction_cases (Oandshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case15: forall r1 r2 n1 v2, op_strength_reduction_cases (Oor) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case16: forall r1 r2 v1 n2, op_strength_reduction_cases (Oor) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case17: forall s r1 r2 v1 n2, op_strength_reduction_cases (Oorshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case18: forall r1 r2 n1 v2, op_strength_reduction_cases (Oxor) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | op_strength_reduction_case19: forall r1 r2 v1 n2, op_strength_reduction_cases (Oxor) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case20: forall s r1 r2 v1 n2, op_strength_reduction_cases (Oxorshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case21: forall r1 r2 v1 n2, op_strength_reduction_cases (Obic) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case22: forall s r1 r2 v1 n2, op_strength_reduction_cases (Obicshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case23: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshl) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case24: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshr) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case25: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshru) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case26: forall c args vl, op_strength_reduction_cases (Ocmp c) (args) (vl) - | op_strength_reduction_default: forall (op: operation) (args: list reg) (vl: list approx), op_strength_reduction_cases op args vl. - -Definition op_strength_reduction_match (op: operation) (args: list reg) (vl: list approx) := - match op as zz1, args as zz2, vl as zz3 return op_strength_reduction_cases zz1 zz2 zz3 with - | Oadd, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case1 r1 r2 n1 v2 - | Oadd, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case2 r1 r2 v1 n2 - | Oaddshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case3 s r1 r2 v1 n2 - | Osub, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case4 r1 r2 n1 v2 - | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case5 r1 r2 v1 n2 - | Osubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case6 s r1 r2 v1 n2 - | Orsubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case7 s r1 r2 v1 n2 - | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case8 r1 r2 n1 v2 - | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case9 r1 r2 v1 n2 - | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case10 r1 r2 v1 n2 - | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case11 r1 r2 v1 n2 - | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case12 r1 r2 n1 v2 - | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case13 r1 r2 v1 n2 - | Oandshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case14 s r1 r2 v1 n2 - | Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case15 r1 r2 n1 v2 - | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case16 r1 r2 v1 n2 - | Oorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case17 s r1 r2 v1 n2 - | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case18 r1 r2 n1 v2 - | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case19 r1 r2 v1 n2 - | Oxorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case20 s r1 r2 v1 n2 - | Obic, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case21 r1 r2 v1 n2 - | Obicshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case22 s r1 r2 v1 n2 - | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case23 r1 r2 v1 n2 - | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case24 r1 r2 v1 n2 - | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case25 r1 r2 v1 n2 - | Ocmp c, args, vl => op_strength_reduction_case26 c args vl - | op, args, vl => op_strength_reduction_default op args vl - end. - -Definition op_strength_reduction (op: operation) (args: list reg) (vl: list approx) := - match op_strength_reduction_match op args vl with - | op_strength_reduction_case1 r1 r2 n1 v2 => (* Oadd, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_addimm n1 r2 - | op_strength_reduction_case2 r1 r2 v1 n2 => (* Oadd, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_addimm n2 r1 - | op_strength_reduction_case3 s r1 r2 v1 n2 => (* Oaddshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_addimm (eval_static_shift s n2) r1 - | op_strength_reduction_case4 r1 r2 n1 v2 => (* Osub, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - (Orsubimm n1, r2 :: nil) - | op_strength_reduction_case5 r1 r2 v1 n2 => (* Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_addimm (Int.neg n2) r1 - | op_strength_reduction_case6 s r1 r2 v1 n2 => (* Osubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_addimm (Int.neg (eval_static_shift s n2)) r1 - | op_strength_reduction_case7 s r1 r2 v1 n2 => (* Orsubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Orsubimm (eval_static_shift s n2), r1 :: nil) - | op_strength_reduction_case8 r1 r2 n1 v2 => (* Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_mulimm n1 r2 r1 - | op_strength_reduction_case9 r1 r2 v1 n2 => (* Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_mulimm n2 r1 r2 - | op_strength_reduction_case10 r1 r2 v1 n2 => (* Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_divimm n2 r1 r2 - | op_strength_reduction_case11 r1 r2 v1 n2 => (* Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_divuimm n2 r1 r2 - | op_strength_reduction_case12 r1 r2 n1 v2 => (* Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_andimm n1 r2 - | op_strength_reduction_case13 r1 r2 v1 n2 => (* Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_andimm n2 r1 - | op_strength_reduction_case14 s r1 r2 v1 n2 => (* Oandshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_andimm (eval_static_shift s n2) r1 - | op_strength_reduction_case15 r1 r2 n1 v2 => (* Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_orimm n1 r2 - | op_strength_reduction_case16 r1 r2 v1 n2 => (* Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_orimm n2 r1 - | op_strength_reduction_case17 s r1 r2 v1 n2 => (* Oorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_orimm (eval_static_shift s n2) r1 - | op_strength_reduction_case18 r1 r2 n1 v2 => (* Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - make_xorimm n1 r2 - | op_strength_reduction_case19 r1 r2 v1 n2 => (* Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_xorimm n2 r1 - | op_strength_reduction_case20 s r1 r2 v1 n2 => (* Oxorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_xorimm (eval_static_shift s n2) r1 - | op_strength_reduction_case21 r1 r2 v1 n2 => (* Obic, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_andimm (Int.not n2) r1 - | op_strength_reduction_case22 s r1 r2 v1 n2 => (* Obicshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_andimm (Int.not (eval_static_shift s n2)) r1 - | op_strength_reduction_case23 r1 r2 v1 n2 => (* Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shlimm n2 r1 r2 - | op_strength_reduction_case24 r1 r2 v1 n2 => (* Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shrimm n2 r1 r2 - | op_strength_reduction_case25 r1 r2 v1 n2 => (* Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shruimm n2 r1 r2 - | op_strength_reduction_case26 c args vl => (* Ocmp c, args, vl *) - let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args') - | op_strength_reduction_default op args vl => - (op, args) - end. - - - -(** Original definition: -<< -Nondetfunction addr_strength_reduction - (addr: addressing) (args: list reg) (vl: list approx) := - match addr, args, vl with - | Aindexed2, r1 :: r2 :: nil, S n1 :: I n2 :: nil => - (Ainstack (Int.add n1 n2), nil) - | Aindexed2, r1 :: r2 :: nil, I n1 :: S 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 => - (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 => - (Ainstack (Int.add n1 n), nil) - | _, _, _ => - (addr, args) - end. ->> -*) - -Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg) (vl: list approx), Type := - | addr_strength_reduction_case1: forall r1 r2 n1 n2, addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil) (S n1 :: I n2 :: nil) - | addr_strength_reduction_case2: forall r1 r2 n1 n2, addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil) (I n1 :: S n2 :: nil) - | addr_strength_reduction_case3: forall r1 r2 n1 v2, addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | addr_strength_reduction_case4: forall r1 r2 v1 n2, addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | addr_strength_reduction_case5: forall s r1 r2 n1 n2, addr_strength_reduction_cases (Aindexed2shift s) (r1 :: r2 :: nil) (S n1 :: I n2 :: nil) - | addr_strength_reduction_case6: forall s r1 r2 v1 n2, addr_strength_reduction_cases (Aindexed2shift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | addr_strength_reduction_case7: forall n r1 n1, addr_strength_reduction_cases (Aindexed n) (r1 :: nil) (S n1 :: nil) - | addr_strength_reduction_default: forall (addr: addressing) (args: list reg) (vl: list approx), addr_strength_reduction_cases addr args vl. - -Definition addr_strength_reduction_match (addr: addressing) (args: list reg) (vl: list approx) := - match addr as zz1, args as zz2, vl as zz3 return addr_strength_reduction_cases zz1 zz2 zz3 with - | Aindexed2, r1 :: r2 :: nil, S n1 :: I n2 :: nil => addr_strength_reduction_case1 r1 r2 n1 n2 - | Aindexed2, r1 :: r2 :: nil, I n1 :: S n2 :: nil => addr_strength_reduction_case2 r1 r2 n1 n2 - | Aindexed2, r1 :: r2 :: nil, I n1 :: v2 :: nil => addr_strength_reduction_case3 r1 r2 n1 v2 - | Aindexed2, r1 :: r2 :: nil, v1 :: I n2 :: nil => addr_strength_reduction_case4 r1 r2 v1 n2 - | Aindexed2shift s, r1 :: r2 :: nil, S n1 :: I n2 :: nil => addr_strength_reduction_case5 s r1 r2 n1 n2 - | Aindexed2shift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => addr_strength_reduction_case6 s r1 r2 v1 n2 - | Aindexed n, r1 :: nil, S n1 :: nil => addr_strength_reduction_case7 n r1 n1 - | addr, args, vl => addr_strength_reduction_default addr args vl - end. - -Definition addr_strength_reduction (addr: addressing) (args: list reg) (vl: list approx) := - match addr_strength_reduction_match addr args vl with - | addr_strength_reduction_case1 r1 r2 n1 n2 => (* Aindexed2, r1 :: r2 :: nil, S n1 :: I n2 :: nil *) - (Ainstack (Int.add n1 n2), nil) - | addr_strength_reduction_case2 r1 r2 n1 n2 => (* Aindexed2, r1 :: r2 :: nil, I n1 :: S n2 :: nil *) - (Ainstack (Int.add n1 n2), nil) - | addr_strength_reduction_case3 r1 r2 n1 v2 => (* Aindexed2, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - (Aindexed n1, r2 :: nil) - | addr_strength_reduction_case4 r1 r2 v1 n2 => (* Aindexed2, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Aindexed n2, r1 :: nil) - | addr_strength_reduction_case5 s r1 r2 n1 n2 => (* Aindexed2shift s, r1 :: r2 :: nil, S n1 :: I n2 :: nil *) - (Ainstack (Int.add n1 (eval_static_shift s n2)), nil) - | addr_strength_reduction_case6 s r1 r2 v1 n2 => (* Aindexed2shift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Aindexed (eval_static_shift s n2), r1 :: nil) - | addr_strength_reduction_case7 n r1 n1 => (* Aindexed n, r1 :: nil, S n1 :: nil *) - (Ainstack (Int.add n1 n), nil) - | addr_strength_reduction_default addr args vl => - (addr, args) - end. - - -End STRENGTH_REDUCTION. diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp new file mode 100644 index 00000000..031ec32c --- /dev/null +++ b/arm/ConstpropOp.vp @@ -0,0 +1,301 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Static analysis and strength reduction for operators + and conditions. This is the machine-dependent part of [Constprop]. *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Op. +Require Import Registers. + +(** * 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. *) + | 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. *) + + +(** 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. + + 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. *) + +Definition eval_static_shift (s: shift) (n: int) : int := + match s with + | Slsl x => Int.shl n x + | Slsr x => Int.shru n x + | Sasr x => Int.shr n x + | 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)) + | _, _ => 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. + +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 => F n + | 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) + | Odiv, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero 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 => F(Float.floatofint n1) + | Ofloatofintu, I n1 :: nil => F(Float.floatofintu n1) + | Ocmp c, vl => eval_static_condition_val c vl + | _, _ => 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) := + match cond, args, vl with + | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => + (Ccompimm (swap_comparison c) n1, r2 :: nil) + | Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil => + (Ccompimm c n2, r1 :: nil) + | Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil => + (Ccompuimm (swap_comparison c) n1, r2 :: nil) + | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil => + (Ccompuimm c n2, r1 :: nil) + | Ccompshift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil => + (Ccompimm c (eval_static_shift s n2), r1 :: nil) + | Ccompushift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil => + (Ccompuimm c (eval_static_shift s n2), r1 :: nil) + | _, _, _ => + (cond, args) + end. + +Definition make_addimm (n: int) (r: reg) := + if Int.eq n Int.zero + then (Omove, r :: nil) + else (Oaddimm n, r :: nil). + +Definition make_shlimm (n: int) (r1 r2: reg) := + if Int.eq n Int.zero then + (Omove, r1 :: nil) + else if Int.ltu n Int.iwordsize then + (Oshift (Slsl (mk_shift_amount n)), r1 :: nil) + else + (Oshl, r1 :: r2 :: nil). + +Definition make_shrimm (n: int) (r1 r2: reg) := + if Int.eq n Int.zero then + (Omove, r1 :: nil) + else if Int.ltu n Int.iwordsize then + (Oshift (Sasr (mk_shift_amount n)), r1 :: nil) + else + (Oshr, r1 :: r2 :: nil). + +Definition make_shruimm (n: int) (r1 r2: reg) := + if Int.eq n Int.zero then + (Omove, r1 :: nil) + else if Int.ltu n Int.iwordsize then + (Oshift (Slsr (mk_shift_amount n)), r1 :: nil) + else + (Oshru, r1 :: r2 :: nil). + +Definition make_mulimm (n: int) (r1 r2: reg) := + if Int.eq n Int.zero then + (Ointconst Int.zero, nil) + else if Int.eq n Int.one then + (Omove, r1 :: nil) + else + match Int.is_power2 n with + | Some l => (Oshift (Slsl (mk_shift_amount l)), r1 :: nil) + | None => (Omul, r1 :: r2 :: nil) + end. + +Definition make_divimm (n: int) (r1 r2: reg) := + match Int.is_power2 n with + | Some l => if Int.ltu l (Int.repr 31) + then (Oshrximm l, r1 :: nil) + else (Odiv, r1 :: r2 :: nil) + | None => (Odiv, r1 :: r2 :: nil) + end. + +Definition make_divuimm (n: int) (r1 r2: reg) := + match Int.is_power2 n with + | Some l => (Oshift (Slsr (mk_shift_amount l)), r1 :: nil) + | None => (Odivu, r1 :: r2 :: nil) + end. + +Definition make_andimm (n: int) (r: reg) := + if Int.eq n Int.zero then (Ointconst Int.zero, nil) + else if Int.eq n Int.mone then (Omove, r :: nil) + else (Oandimm n, r :: nil). + +Definition make_orimm (n: int) (r: reg) := + if Int.eq n Int.zero then (Omove, r :: nil) + else if Int.eq n Int.mone then (Ointconst Int.mone, nil) + else (Oorimm n, r :: nil). + +Definition make_xorimm (n: int) (r: reg) := + if Int.eq n Int.zero then (Omove, r :: nil) + else if Int.eq n Int.mone then (Onot, r :: nil) + else (Oxorimm n, r :: nil). + +Nondetfunction op_strength_reduction + (op: operation) (args: list reg) (vl: list approx) := + match op, args, vl with + | 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 + | Osub, r1 :: r2 :: nil, I n1 :: v2 :: nil => (Orsubimm n1, r2 :: nil) + | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg n2) r1 + | Osubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg (eval_static_shift s n2)) r1 + | Orsubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Orsubimm (eval_static_shift s n2), r1 :: nil) + | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_mulimm n1 r2 r1 + | 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 + | 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 + | 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 + | Ocmp c, args, vl => + let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args') + | _, _, _ => (op, args) + end. + + +Nondetfunction addr_strength_reduction + (addr: addressing) (args: list reg) (vl: list approx) := + match addr, args, vl with + | Aindexed2, r1 :: r2 :: nil, S n1 :: I n2 :: nil => + (Ainstack (Int.add n1 n2), nil) + | Aindexed2, r1 :: r2 :: nil, I n1 :: S 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 => + (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 => + (Ainstack (Int.add n1 n), nil) + | _, _, _ => + (addr, args) + end. + +Definition builtin_strength_reduction + (ef: external_function) (args: list reg) (vl: list approx) := + (ef, args). + +End STRENGTH_REDUCTION. diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 0e60796a..711bb33b 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -19,6 +19,7 @@ Require Import Floats. Require Import Values. Require Import Memory. Require Import Globalenvs. +Require Import Events. Require Import Op. Require Import Registers. Require Import RTL. @@ -417,6 +418,19 @@ Proof. auto. Qed. +Lemma builtin_strength_reduction_correct: + forall ef args vl m t vres m', + vl = approx_regs app args -> + external_call ef ge rs##args m t vres m' -> + let (ef', args') := builtin_strength_reduction ef args vl in + external_call ef' ge rs##args' m t vres m'. +Proof. + (* force MATCH to be used *) + assert (val_match_approx (approx_reg app 1%positive) rs#(1%positive)) + by (apply MATCH). + unfold builtin_strength_reduction; intros; simpl; auto. +Qed. + End STRENGTH_REDUCTION. End ANALYSIS. diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml index dff4e4f9..9ebce979 100644 --- a/arm/PrintOp.ml +++ b/arm/PrintOp.ml @@ -59,10 +59,6 @@ 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 - | Ocast8unsigned, [r1] -> fprintf pp "int8unsigned(%a)" reg r1 - | Ocast16signed, [r1] -> fprintf pp "int16signed(%a)" reg r1 - | Ocast16unsigned, [r1] -> fprintf pp "int16unsigned(%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.v b/arm/SelectOp.v deleted file mode 100644 index 64d15cbc..00000000 --- a/arm/SelectOp.v +++ /dev/null @@ -1,1169 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Instruction selection for operators *) - -(** The instruction selection pass recognizes opportunities for using - combined arithmetic and logical operations and addressing modes - offered by the target processor. For instance, the expression [x + 1] - can take advantage of the "immediate add" instruction of the processor, - and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned - into a "rotate and mask" instruction. - - This file defines functions for building CminorSel expressions and - statements, especially expressions consisting of operator - applications. These functions examine their arguments to choose - cheaper forms of operators whenever possible. - - For instance, [add e1 e2] will return a CminorSel expression semantically - equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a - [Oaddimm] operator if one of the arguments is an integer constant, - or suppress the addition altogether if one of the arguments is the - null integer. In passing, we perform operator reassociation - ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount - of constant propagation. - - On top of the "smart constructor" functions defined below, - module [Selection] implements the actual instruction selection pass. -*) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Cminor. -Require Import Op. -Require Import CminorSel. - -Open Local Scope cminorsel_scope. - -(** ** Constants **) - -Definition addrsymbol (id: ident) (ofs: int) := - Eop (Oaddrsymbol id ofs) Enil. - -Definition addrstack (ofs: int) := - Eop (Oaddrstack ofs) Enil. - -(** ** Integer logical negation *) - -(** Original definition: -<< -Nondetfunction notint (e: expr) := - match e with - | Eop (Oshift s) (t1:::Enil) => Eop (Onotshift s) (t1:::Enil) - | Eop Onot (t1:::Enil) => t1 - | Eop (Onotshift s) (t1:::Enil) => Eop (Oshift s) (t1:::Enil) - | _ => Eop Onot (e:::Enil) - end. ->> -*) - -Inductive notint_cases: forall (e: expr), Type := - | notint_case1: forall s t1, notint_cases (Eop (Oshift s) (t1:::Enil)) - | notint_case2: forall t1, notint_cases (Eop Onot (t1:::Enil)) - | notint_case3: forall s t1, notint_cases (Eop (Onotshift s) (t1:::Enil)) - | notint_default: forall (e: expr), notint_cases e. - -Definition notint_match (e: expr) := - match e as zz1 return notint_cases zz1 with - | Eop (Oshift s) (t1:::Enil) => notint_case1 s t1 - | Eop Onot (t1:::Enil) => notint_case2 t1 - | Eop (Onotshift s) (t1:::Enil) => notint_case3 s t1 - | e => notint_default e - end. - -Definition notint (e: expr) := - match notint_match e with - | notint_case1 s t1 => (* Eop (Oshift s) (t1:::Enil) *) - Eop (Onotshift s) (t1:::Enil) - | notint_case2 t1 => (* Eop Onot (t1:::Enil) *) - t1 - | notint_case3 s t1 => (* Eop (Onotshift s) (t1:::Enil) *) - Eop (Oshift s) (t1:::Enil) - | notint_default e => - Eop Onot (e:::Enil) - end. - - -(** ** Boolean negation *) - -Fixpoint notbool (e: expr) {struct e} : expr := - let default := Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil) in - match e with - | Eop (Ointconst n) Enil => - Eop (Ointconst (if Int.eq n Int.zero then Int.one else Int.zero)) Enil - | Eop (Ocmp cond) args => - Eop (Ocmp (negate_condition cond)) args - | Econdition e1 e2 e3 => - Econdition e1 (notbool e2) (notbool e3) - | _ => - default - end. - -(** ** Integer addition and pointer addition *) - -(** Original definition: -<< -Nondetfunction addimm (n: int) (e: expr) := - if Int.eq n Int.zero then e else - match e with - | Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil - | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Int.add n m)) Enil - | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Int.add n m)) Enil - | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil) - | _ => Eop (Oaddimm n) (e ::: Enil) - end. ->> -*) - -Inductive addimm_cases: forall (e: expr), Type := - | addimm_case1: forall m, addimm_cases (Eop (Ointconst m) Enil) - | addimm_case2: forall s m, addimm_cases (Eop (Oaddrsymbol s m) Enil) - | addimm_case3: forall m, addimm_cases (Eop (Oaddrstack m) Enil) - | addimm_case4: forall m t, addimm_cases (Eop (Oaddimm m) (t ::: Enil)) - | addimm_default: forall (e: expr), addimm_cases e. - -Definition addimm_match (e: expr) := - match e as zz1 return addimm_cases zz1 with - | Eop (Ointconst m) Enil => addimm_case1 m - | Eop (Oaddrsymbol s m) Enil => addimm_case2 s m - | Eop (Oaddrstack m) Enil => addimm_case3 m - | Eop (Oaddimm m) (t ::: Enil) => addimm_case4 m t - | e => addimm_default e - end. - -Definition addimm (n: int) (e: expr) := - if Int.eq n Int.zero then e else match addimm_match e with - | addimm_case1 m => (* Eop (Ointconst m) Enil *) - Eop (Ointconst(Int.add n m)) Enil - | addimm_case2 s m => (* Eop (Oaddrsymbol s m) Enil *) - Eop (Oaddrsymbol s (Int.add n m)) Enil - | addimm_case3 m => (* Eop (Oaddrstack m) Enil *) - Eop (Oaddrstack (Int.add n m)) Enil - | addimm_case4 m t => (* Eop (Oaddimm m) (t ::: Enil) *) - Eop (Oaddimm(Int.add n m)) (t ::: Enil) - | addimm_default e => - Eop (Oaddimm n) (e ::: Enil) - end. - - -(** Original definition: -<< -Nondetfunction add (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => - addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) - | Eop(Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil)) - | t1, Eop (Ointconst n2) Enil => addimm n2 t1 - | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) - | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil) - | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil) - | _, _ => Eop Oadd (e1:::e2:::Enil) - end. ->> -*) - -Inductive add_cases: forall (e1: expr) (e2: expr), Type := - | add_case1: forall n1 t2, add_cases (Eop (Ointconst n1) Enil) (t2) - | add_case2: forall n1 t1 n2 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil)) - | add_case3: forall n1 t1 t2, add_cases (Eop(Oaddimm n1) (t1:::Enil)) (t2) - | add_case4: forall t1 n2, add_cases (t1) (Eop (Ointconst n2) Enil) - | add_case5: forall t1 n2 t2, add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil)) - | add_case6: forall s t1 t2, add_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | add_case7: forall t1 s t2, add_cases (t1) (Eop (Oshift s) (t2:::Enil)) - | add_default: forall (e1: expr) (e2: expr), add_cases e1 e2. - -Definition add_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return add_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => add_case1 n1 t2 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => add_case2 n1 t1 n2 t2 - | Eop(Oaddimm n1) (t1:::Enil), t2 => add_case3 n1 t1 t2 - | t1, Eop (Ointconst n2) Enil => add_case4 t1 n2 - | t1, Eop (Oaddimm n2) (t2:::Enil) => add_case5 t1 n2 t2 - | Eop (Oshift s) (t1:::Enil), t2 => add_case6 s t1 t2 - | t1, Eop (Oshift s) (t2:::Enil) => add_case7 t1 s t2 - | e1, e2 => add_default e1 e2 - end. - -Definition add (e1: expr) (e2: expr) := - match add_match e1 e2 with - | add_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - addimm n1 t2 - | add_case2 n1 t1 n2 t2 => (* Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) *) - addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) - | add_case3 n1 t1 t2 => (* Eop(Oaddimm n1) (t1:::Enil), t2 *) - addimm n1 (Eop Oadd (t1:::t2:::Enil)) - | add_case4 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - addimm n2 t1 - | add_case5 t1 n2 t2 => (* t1, Eop (Oaddimm n2) (t2:::Enil) *) - addimm n2 (Eop Oadd (t1:::t2:::Enil)) - | add_case6 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) - Eop (Oaddshift s) (t2:::t1:::Enil) - | add_case7 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) - Eop (Oaddshift s) (t1:::t2:::Enil) - | add_default e1 e2 => - Eop Oadd (e1:::e2:::Enil) - end. - - -(** ** Integer and pointer subtraction *) - -(** Original definition: -<< -Nondetfunction sub (e1: expr) (e2: expr) := - match e1, e2 with - | t1, Eop (Ointconst n2) Enil => addimm (Int.neg n2) t1 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => - addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil)) - | Eop (Oaddimm n1) (t1:::Enil), t2 => - addimm n1 (Eop Osub (t1:::t2:::Enil)) - | t1, Eop (Oaddimm n2) (t2:::Enil) => - addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) - | Eop (Ointconst n1) Enil, t2 => Eop (Orsubimm n1) (t2:::Enil) - | Eop (Oshift s) (t1:::Enil), t2 => Eop (Orsubshift s) (t2:::t1:::Enil) - | t1, Eop (Oshift s) (t2:::Enil) => Eop (Osubshift s) (t1:::t2:::Enil) - | _, _ => Eop Osub (e1:::e2:::Enil) - end. ->> -*) - -Inductive sub_cases: forall (e1: expr) (e2: expr), Type := - | sub_case1: forall t1 n2, sub_cases (t1) (Eop (Ointconst n2) Enil) - | sub_case2: forall n1 t1 n2 t2, sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil)) - | sub_case3: forall n1 t1 t2, sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2) - | sub_case4: forall t1 n2 t2, sub_cases (t1) (Eop (Oaddimm n2) (t2:::Enil)) - | sub_case5: forall n1 t2, sub_cases (Eop (Ointconst n1) Enil) (t2) - | sub_case6: forall s t1 t2, sub_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | sub_case7: forall t1 s t2, sub_cases (t1) (Eop (Oshift s) (t2:::Enil)) - | sub_default: forall (e1: expr) (e2: expr), sub_cases e1 e2. - -Definition sub_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return sub_cases zz1 zz2 with - | t1, Eop (Ointconst n2) Enil => sub_case1 t1 n2 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => sub_case2 n1 t1 n2 t2 - | Eop (Oaddimm n1) (t1:::Enil), t2 => sub_case3 n1 t1 t2 - | t1, Eop (Oaddimm n2) (t2:::Enil) => sub_case4 t1 n2 t2 - | Eop (Ointconst n1) Enil, t2 => sub_case5 n1 t2 - | Eop (Oshift s) (t1:::Enil), t2 => sub_case6 s t1 t2 - | t1, Eop (Oshift s) (t2:::Enil) => sub_case7 t1 s t2 - | e1, e2 => sub_default e1 e2 - end. - -Definition sub (e1: expr) (e2: expr) := - match sub_match e1 e2 with - | sub_case1 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - addimm (Int.neg n2) t1 - | sub_case2 n1 t1 n2 t2 => (* Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) *) - addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil)) - | sub_case3 n1 t1 t2 => (* Eop (Oaddimm n1) (t1:::Enil), t2 *) - addimm n1 (Eop Osub (t1:::t2:::Enil)) - | sub_case4 t1 n2 t2 => (* t1, Eop (Oaddimm n2) (t2:::Enil) *) - addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) - | sub_case5 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - Eop (Orsubimm n1) (t2:::Enil) - | sub_case6 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) - Eop (Orsubshift s) (t2:::t1:::Enil) - | sub_case7 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) - Eop (Osubshift s) (t1:::t2:::Enil) - | sub_default e1 e2 => - Eop Osub (e1:::e2:::Enil) - end. - - -Definition negint (e: expr) := Eop (Orsubimm Int.zero) (e ::: Enil). - -(** ** Immediate shifts *) - -(** Original definition: -<< -Nondetfunction shlimm (e1: expr) (n: int) := - if Int.eq n Int.zero then - e1 - else if negb (Int.ltu n Int.iwordsize) then - Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil) - else match e1 with - | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shl n1 n)) Enil - | Eop (Oshift (Slsl n1)) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int.iwordsize - then Eop (Oshift (Slsl (mk_shift_amount(Int.add n n1)))) (t1:::Enil) - else Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil) - | _ => Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil) - end. ->> -*) - -Inductive shlimm_cases: forall (e1: expr) , Type := - | shlimm_case1: forall n1, shlimm_cases (Eop (Ointconst n1) Enil) - | shlimm_case2: forall n1 t1, shlimm_cases (Eop (Oshift (Slsl n1)) (t1:::Enil)) - | shlimm_default: forall (e1: expr) , shlimm_cases e1. - -Definition shlimm_match (e1: expr) := - match e1 as zz1 return shlimm_cases zz1 with - | Eop (Ointconst n1) Enil => shlimm_case1 n1 - | Eop (Oshift (Slsl n1)) (t1:::Enil) => shlimm_case2 n1 t1 - | e1 => shlimm_default e1 - end. - -Definition shlimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shlimm_match e1 with - | shlimm_case1 n1 => (* Eop (Ointconst n1) Enil *) - Eop (Ointconst(Int.shl n1 n)) Enil - | shlimm_case2 n1 t1 => (* Eop (Oshift (Slsl n1)) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Slsl (mk_shift_amount(Int.add n n1)))) (t1:::Enil) else Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil) - | shlimm_default e1 => - Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shruimm (e1: expr) (n: int) := - if Int.eq n Int.zero then - e1 - else if negb (Int.ltu n Int.iwordsize) then - Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil) - else match e1 with - | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shru n1 n)) Enil - | Eop (Oshift (Slsr n1)) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int.iwordsize - then Eop (Oshift (Slsr (mk_shift_amount (Int.add n n1)))) (t1:::Enil) - else Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil) - | _ => Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil) - end. ->> -*) - -Inductive shruimm_cases: forall (e1: expr) , Type := - | shruimm_case1: forall n1, shruimm_cases (Eop (Ointconst n1) Enil) - | shruimm_case2: forall n1 t1, shruimm_cases (Eop (Oshift (Slsr n1)) (t1:::Enil)) - | shruimm_default: forall (e1: expr) , shruimm_cases e1. - -Definition shruimm_match (e1: expr) := - match e1 as zz1 return shruimm_cases zz1 with - | Eop (Ointconst n1) Enil => shruimm_case1 n1 - | Eop (Oshift (Slsr n1)) (t1:::Enil) => shruimm_case2 n1 t1 - | e1 => shruimm_default e1 - end. - -Definition shruimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shruimm_match e1 with - | shruimm_case1 n1 => (* Eop (Ointconst n1) Enil *) - Eop (Ointconst(Int.shru n1 n)) Enil - | shruimm_case2 n1 t1 => (* Eop (Oshift (Slsr n1)) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Slsr (mk_shift_amount (Int.add n n1)))) (t1:::Enil) else Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil) - | shruimm_default e1 => - Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shrimm (e1: expr) (n: int) := - if Int.eq n Int.zero then - e1 - else if negb (Int.ltu n Int.iwordsize) then - Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil) - else - match e1 with - | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shr n1 n)) Enil - | Eop (Oshift (Sasr n1)) (t1:::Enil) => - if Int.ltu (Int.add n n1) Int.iwordsize - then Eop (Oshift (Sasr (mk_shift_amount (Int.add n n1)))) (t1:::Enil) - else Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil) - | _ => Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil) - end. ->> -*) - -Inductive shrimm_cases: forall (e1: expr) , Type := - | shrimm_case1: forall n1, shrimm_cases (Eop (Ointconst n1) Enil) - | shrimm_case2: forall n1 t1, shrimm_cases (Eop (Oshift (Sasr n1)) (t1:::Enil)) - | shrimm_default: forall (e1: expr) , shrimm_cases e1. - -Definition shrimm_match (e1: expr) := - match e1 as zz1 return shrimm_cases zz1 with - | Eop (Ointconst n1) Enil => shrimm_case1 n1 - | Eop (Oshift (Sasr n1)) (t1:::Enil) => shrimm_case2 n1 t1 - | e1 => shrimm_default e1 - end. - -Definition shrimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shrimm_match e1 with - | shrimm_case1 n1 => (* Eop (Ointconst n1) Enil *) - Eop (Ointconst(Int.shr n1 n)) Enil - | shrimm_case2 n1 t1 => (* Eop (Oshift (Sasr n1)) (t1:::Enil) *) - if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Sasr (mk_shift_amount (Int.add n n1)))) (t1:::Enil) else Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil) - | shrimm_default e1 => - Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil) - end. - - -(** ** Integer multiply *) - -Definition mulimm_base (n1: int) (e2: expr) := - match Int.one_bits n1 with - | i :: nil => - shlimm e2 i - | i :: j :: nil => - Elet e2 - (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j)) - | _ => - Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil) - end. - -(** Original definition: -<< -Nondetfunction mulimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil - else if Int.eq n1 Int.one then e2 - else match e2 with - | Eop (Ointconst n2) Enil => Eop (Ointconst(Int.mul n1 n2)) Enil - | Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.mul n1 n2) (mulimm_base n1 t2) - | _ => mulimm_base n1 e2 - end. ->> -*) - -Inductive mulimm_cases: forall (e2: expr), Type := - | mulimm_case1: forall n2, mulimm_cases (Eop (Ointconst n2) Enil) - | mulimm_case2: forall n2 t2, mulimm_cases (Eop (Oaddimm n2) (t2:::Enil)) - | mulimm_default: forall (e2: expr), mulimm_cases e2. - -Definition mulimm_match (e2: expr) := - match e2 as zz1 return mulimm_cases zz1 with - | Eop (Ointconst n2) Enil => mulimm_case1 n2 - | Eop (Oaddimm n2) (t2:::Enil) => mulimm_case2 n2 t2 - | e2 => mulimm_default e2 - end. - -Definition mulimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.one then e2 else match mulimm_match e2 with - | mulimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst(Int.mul n1 n2)) Enil - | mulimm_case2 n2 t2 => (* Eop (Oaddimm n2) (t2:::Enil) *) - addimm (Int.mul n1 n2) (mulimm_base n1 t2) - | mulimm_default e2 => - mulimm_base n1 e2 - end. - - -(** Original definition: -<< -Nondetfunction mul (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => mulimm n1 t2 - | t1, Eop (Ointconst n2) Enil => mulimm n2 t1 - | _, _ => Eop Omul (e1:::e2:::Enil) - end. ->> -*) - -Inductive mul_cases: forall (e1: expr) (e2: expr), Type := - | mul_case1: forall n1 t2, mul_cases (Eop (Ointconst n1) Enil) (t2) - | mul_case2: forall t1 n2, mul_cases (t1) (Eop (Ointconst n2) Enil) - | mul_default: forall (e1: expr) (e2: expr), mul_cases e1 e2. - -Definition mul_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return mul_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => mul_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => mul_case2 t1 n2 - | e1, e2 => mul_default e1 e2 - end. - -Definition mul (e1: expr) (e2: expr) := - match mul_match e1 e2 with - | mul_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - mulimm n1 t2 - | mul_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - mulimm n2 t1 - | mul_default e1 e2 => - Eop Omul (e1:::e2:::Enil) - end. - - -(** ** Bitwise and, or, xor *) - -(** Original definition: -<< -Nondetfunction andimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else - match e2 with - | Eop (Ointconst n2) Enil => - Eop (Ointconst (Int.and n1 n2)) Enil - | Eop (Oandimm n2) (t2:::Enil) => - Eop (Oandimm (Int.and n1 n2)) (t2:::Enil) - | _ => - Eop (Oandimm n1) (e2:::Enil) - end. ->> -*) - -Inductive andimm_cases: forall (e2: expr), Type := - | andimm_case1: forall n2, andimm_cases (Eop (Ointconst n2) Enil) - | andimm_case2: forall n2 t2, andimm_cases (Eop (Oandimm n2) (t2:::Enil)) - | andimm_default: forall (e2: expr), andimm_cases e2. - -Definition andimm_match (e2: expr) := - match e2 as zz1 return andimm_cases zz1 with - | Eop (Ointconst n2) Enil => andimm_case1 n2 - | Eop (Oandimm n2) (t2:::Enil) => andimm_case2 n2 t2 - | e2 => andimm_default e2 - end. - -Definition andimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else match andimm_match e2 with - | andimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.and n1 n2)) Enil - | andimm_case2 n2 t2 => (* Eop (Oandimm n2) (t2:::Enil) *) - Eop (Oandimm (Int.and n1 n2)) (t2:::Enil) - | andimm_default e2 => - Eop (Oandimm n1) (e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction and (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => andimm n1 t2 - | t1, Eop (Ointconst n2) Enil => andimm n2 t1 - | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oandshift s) (t2:::t1:::Enil) - | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oandshift s) (t1:::t2:::Enil) - | Eop (Onotshift s) (t1:::Enil), t2 => Eop (Obicshift s) (t2:::t1:::Enil) - | t1, Eop (Onotshift s) (t2:::Enil) => Eop (Obicshift s) (t1:::t2:::Enil) - | Eop Onot (t1:::Enil), t2 => Eop Obic (t2:::t1:::Enil) - | t1, Eop Onot (t2:::Enil) => Eop Obic (t1:::t2:::Enil) - | _, _ => Eop Oand (e1:::e2:::Enil) - end. ->> -*) - -Inductive and_cases: forall (e1: expr) (e2: expr), Type := - | and_case1: forall n1 t2, and_cases (Eop (Ointconst n1) Enil) (t2) - | and_case2: forall t1 n2, and_cases (t1) (Eop (Ointconst n2) Enil) - | and_case3: forall s t1 t2, and_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | and_case4: forall t1 s t2, and_cases (t1) (Eop (Oshift s) (t2:::Enil)) - | and_case5: forall s t1 t2, and_cases (Eop (Onotshift s) (t1:::Enil)) (t2) - | and_case6: forall t1 s t2, and_cases (t1) (Eop (Onotshift s) (t2:::Enil)) - | and_case7: forall t1 t2, and_cases (Eop Onot (t1:::Enil)) (t2) - | and_case8: forall t1 t2, and_cases (t1) (Eop Onot (t2:::Enil)) - | and_default: forall (e1: expr) (e2: expr), and_cases e1 e2. - -Definition and_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return and_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => and_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => and_case2 t1 n2 - | Eop (Oshift s) (t1:::Enil), t2 => and_case3 s t1 t2 - | t1, Eop (Oshift s) (t2:::Enil) => and_case4 t1 s t2 - | Eop (Onotshift s) (t1:::Enil), t2 => and_case5 s t1 t2 - | t1, Eop (Onotshift s) (t2:::Enil) => and_case6 t1 s t2 - | Eop Onot (t1:::Enil), t2 => and_case7 t1 t2 - | t1, Eop Onot (t2:::Enil) => and_case8 t1 t2 - | e1, e2 => and_default e1 e2 - end. - -Definition and (e1: expr) (e2: expr) := - match and_match e1 e2 with - | and_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - andimm n1 t2 - | and_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - andimm n2 t1 - | and_case3 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) - Eop (Oandshift s) (t2:::t1:::Enil) - | and_case4 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) - Eop (Oandshift s) (t1:::t2:::Enil) - | and_case5 s t1 t2 => (* Eop (Onotshift s) (t1:::Enil), t2 *) - Eop (Obicshift s) (t2:::t1:::Enil) - | and_case6 t1 s t2 => (* t1, Eop (Onotshift s) (t2:::Enil) *) - Eop (Obicshift s) (t1:::t2:::Enil) - | and_case7 t1 t2 => (* Eop Onot (t1:::Enil), t2 *) - Eop Obic (t2:::t1:::Enil) - | and_case8 t1 t2 => (* t1, Eop Onot (t2:::Enil) *) - Eop Obic (t1:::t2:::Enil) - | and_default e1 e2 => - Eop Oand (e1:::e2:::Enil) - end. - - -Definition same_expr_pure (e1 e2: expr) := - match e1, e2 with - | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false - | _, _ => false - end. - -(** Original definition: -<< -Nondetfunction orimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else - match e2 with - | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil - | Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil) - | _ => Eop (Oorimm n1) (e2:::Enil) - end. ->> -*) - -Inductive orimm_cases: forall (e2: expr), Type := - | orimm_case1: forall n2, orimm_cases (Eop (Ointconst n2) Enil) - | orimm_case2: forall n2 t2, orimm_cases (Eop (Oorimm n2) (t2:::Enil)) - | orimm_default: forall (e2: expr), orimm_cases e2. - -Definition orimm_match (e2: expr) := - match e2 as zz1 return orimm_cases zz1 with - | Eop (Ointconst n2) Enil => orimm_case1 n2 - | Eop (Oorimm n2) (t2:::Enil) => orimm_case2 n2 t2 - | e2 => orimm_default e2 - end. - -Definition orimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else match orimm_match e2 with - | orimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.or n1 n2)) Enil - | orimm_case2 n2 t2 => (* Eop (Oorimm n2) (t2:::Enil) *) - Eop (Oorimm (Int.or n1 n2)) (t2:::Enil) - | orimm_default e2 => - Eop (Oorimm n1) (e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction or (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => orimm n1 t2 - | t1, Eop (Ointconst n2) Enil => orimm n2 t1 - | Eop (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) => - if Int.eq (Int.add n1 n2) Int.iwordsize - && same_expr_pure t1 t2 - then Eop (Oshift (Sror n2)) (t1:::Enil) - else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil) - | Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) => - if Int.eq (Int.add n2 n1) Int.iwordsize - && same_expr_pure t1 t2 - then Eop (Oshift (Sror n1)) (t1:::Enil) - else Eop (Oorshift (Slsl n2)) (e1:::t2:::Enil) - | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oorshift s) (t2:::t1:::Enil) - | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oorshift s) (t1:::t2:::Enil) - | _, _ => Eop Oor (e1:::e2:::Enil) - end. ->> -*) - -Inductive or_cases: forall (e1: expr) (e2: expr), Type := - | or_case1: forall n1 t2, or_cases (Eop (Ointconst n1) Enil) (t2) - | or_case2: forall t1 n2, or_cases (t1) (Eop (Ointconst n2) Enil) - | or_case3: forall n1 t1 n2 t2, or_cases (Eop (Oshift (Slsl n1)) (t1:::Enil)) (Eop (Oshift (Slsr n2)) (t2:::Enil)) - | or_case4: forall n1 t1 n2 t2, or_cases (Eop (Oshift (Slsr n1)) (t1:::Enil)) (Eop (Oshift (Slsl n2)) (t2:::Enil)) - | or_case5: forall s t1 t2, or_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | or_case6: forall t1 s t2, or_cases (t1) (Eop (Oshift s) (t2:::Enil)) - | or_default: forall (e1: expr) (e2: expr), or_cases e1 e2. - -Definition or_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return or_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => or_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => or_case2 t1 n2 - | Eop (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) => or_case3 n1 t1 n2 t2 - | Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) => or_case4 n1 t1 n2 t2 - | Eop (Oshift s) (t1:::Enil), t2 => or_case5 s t1 t2 - | t1, Eop (Oshift s) (t2:::Enil) => or_case6 t1 s t2 - | e1, e2 => or_default e1 e2 - end. - -Definition or (e1: expr) (e2: expr) := - match or_match e1 e2 with - | or_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - orimm n1 t2 - | or_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - orimm n2 t1 - | or_case3 n1 t1 n2 t2 => (* Eop (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) *) - if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 then Eop (Oshift (Sror n2)) (t1:::Enil) else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil) - | or_case4 n1 t1 n2 t2 => (* Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) *) - if Int.eq (Int.add n2 n1) Int.iwordsize && same_expr_pure t1 t2 then Eop (Oshift (Sror n1)) (t1:::Enil) else Eop (Oorshift (Slsl n2)) (e1:::t2:::Enil) - | or_case5 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) - Eop (Oorshift s) (t2:::t1:::Enil) - | or_case6 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) - Eop (Oorshift s) (t1:::t2:::Enil) - | or_default e1 e2 => - Eop Oor (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction xorimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else - match e2 with - | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil - | Eop (Oxorimm n2) (t2:::Enil) => Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil) - | _ => Eop (Oxorimm n1) (e2:::Enil) - end. ->> -*) - -Inductive xorimm_cases: forall (e2: expr), Type := - | xorimm_case1: forall n2, xorimm_cases (Eop (Ointconst n2) Enil) - | xorimm_case2: forall n2 t2, xorimm_cases (Eop (Oxorimm n2) (t2:::Enil)) - | xorimm_default: forall (e2: expr), xorimm_cases e2. - -Definition xorimm_match (e2: expr) := - match e2 as zz1 return xorimm_cases zz1 with - | Eop (Ointconst n2) Enil => xorimm_case1 n2 - | Eop (Oxorimm n2) (t2:::Enil) => xorimm_case2 n2 t2 - | e2 => xorimm_default e2 - end. - -Definition xorimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then e2 else match xorimm_match e2 with - | xorimm_case1 n2 => (* Eop (Ointconst n2) Enil *) - Eop (Ointconst (Int.xor n1 n2)) Enil - | xorimm_case2 n2 t2 => (* Eop (Oxorimm n2) (t2:::Enil) *) - Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil) - | xorimm_default e2 => - Eop (Oxorimm n1) (e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction xor (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => xorimm n1 t2 - | t1, Eop (Ointconst n2) Enil => xorimm n2 t1 - | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oxorshift s) (t2:::t1:::Enil) - | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oxorshift s) (t1:::t2:::Enil) - | _, _ => Eop Oxor (e1:::e2:::Enil) - end. ->> -*) - -Inductive xor_cases: forall (e1: expr) (e2: expr), Type := - | xor_case1: forall n1 t2, xor_cases (Eop (Ointconst n1) Enil) (t2) - | xor_case2: forall t1 n2, xor_cases (t1) (Eop (Ointconst n2) Enil) - | xor_case3: forall s t1 t2, xor_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | xor_case4: forall t1 s t2, xor_cases (t1) (Eop (Oshift s) (t2:::Enil)) - | xor_default: forall (e1: expr) (e2: expr), xor_cases e1 e2. - -Definition xor_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return xor_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => xor_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => xor_case2 t1 n2 - | Eop (Oshift s) (t1:::Enil), t2 => xor_case3 s t1 t2 - | t1, Eop (Oshift s) (t2:::Enil) => xor_case4 t1 s t2 - | e1, e2 => xor_default e1 e2 - end. - -Definition xor (e1: expr) (e2: expr) := - match xor_match e1 e2 with - | xor_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - xorimm n1 t2 - | xor_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - xorimm n2 t1 - | xor_case3 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) - Eop (Oxorshift s) (t2:::t1:::Enil) - | xor_case4 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) - Eop (Oxorshift s) (t1:::t2:::Enil) - | xor_default e1 e2 => - Eop Oxor (e1:::e2:::Enil) - end. - - -(** ** Integer division and modulus *) - -Definition mod_aux (divop: operation) (e1 e2: expr) := - Elet e1 - (Elet (lift e2) - (Eop Osub (Eletvar 1 ::: - Eop Omul (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) ::: - Eletvar 0 ::: - Enil) ::: - Enil))). - -Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). - -Definition mods := mod_aux Odiv. - -Definition divuimm (e: expr) (n: int) := - match Int.is_power2 n with - | Some l => shruimm e l - | None => Eop Odivu (e ::: Eop (Ointconst n) Enil ::: Enil) - end. - -(** Original definition: -<< -Nondetfunction divu (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => divuimm e1 n2 - | _ => Eop Odivu (e1:::e2:::Enil) - end. ->> -*) - -Inductive divu_cases: forall (e2: expr), Type := - | divu_case1: forall n2, divu_cases (Eop (Ointconst n2) Enil) - | divu_default: forall (e2: expr), divu_cases e2. - -Definition divu_match (e2: expr) := - match e2 as zz1 return divu_cases zz1 with - | Eop (Ointconst n2) Enil => divu_case1 n2 - | e2 => divu_default e2 - end. - -Definition divu (e1: expr) (e2: expr) := - match divu_match e2 with - | divu_case1 n2 => (* Eop (Ointconst n2) Enil *) - divuimm e1 n2 - | divu_default e2 => - Eop Odivu (e1:::e2:::Enil) - end. - - -Definition moduimm (e: expr) (n: int) := - match Int.is_power2 n with - | Some l => Eop (Oandimm (Int.sub n Int.one)) (e ::: Enil) - | None => mod_aux Odivu e (Eop (Ointconst n) Enil) - end. - -(** Original definition: -<< -Nondetfunction modu (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => moduimm e1 n2 - | _ => mod_aux Odivu e1 e2 - end. ->> -*) - -Inductive modu_cases: forall (e2: expr), Type := - | modu_case1: forall n2, modu_cases (Eop (Ointconst n2) Enil) - | modu_default: forall (e2: expr), modu_cases e2. - -Definition modu_match (e2: expr) := - match e2 as zz1 return modu_cases zz1 with - | Eop (Ointconst n2) Enil => modu_case1 n2 - | e2 => modu_default e2 - end. - -Definition modu (e1: expr) (e2: expr) := - match modu_match e2 with - | modu_case1 n2 => (* Eop (Ointconst n2) Enil *) - moduimm e1 n2 - | modu_default e2 => - mod_aux Odivu e1 e2 - end. - - -(** ** General shifts *) - -(** Original definition: -<< -Nondetfunction shl (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => shlimm e1 n2 - | _ => Eop Oshl (e1:::e2:::Enil) - end. ->> -*) - -Inductive shl_cases: forall (e2: expr), Type := - | shl_case1: forall n2, shl_cases (Eop (Ointconst n2) Enil) - | shl_default: forall (e2: expr), shl_cases e2. - -Definition shl_match (e2: expr) := - match e2 as zz1 return shl_cases zz1 with - | Eop (Ointconst n2) Enil => shl_case1 n2 - | e2 => shl_default e2 - end. - -Definition shl (e1: expr) (e2: expr) := - match shl_match e2 with - | shl_case1 n2 => (* Eop (Ointconst n2) Enil *) - shlimm e1 n2 - | shl_default e2 => - Eop Oshl (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shr (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => shrimm e1 n2 - | _ => Eop Oshr (e1:::e2:::Enil) - end. ->> -*) - -Inductive shr_cases: forall (e2: expr), Type := - | shr_case1: forall n2, shr_cases (Eop (Ointconst n2) Enil) - | shr_default: forall (e2: expr), shr_cases e2. - -Definition shr_match (e2: expr) := - match e2 as zz1 return shr_cases zz1 with - | Eop (Ointconst n2) Enil => shr_case1 n2 - | e2 => shr_default e2 - end. - -Definition shr (e1: expr) (e2: expr) := - match shr_match e2 with - | shr_case1 n2 => (* Eop (Ointconst n2) Enil *) - shrimm e1 n2 - | shr_default e2 => - Eop Oshr (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction shru (e1: expr) (e2: expr) := - match e2 with - | Eop (Ointconst n2) Enil => shruimm e1 n2 - | _ => Eop Oshru (e1:::e2:::Enil) - end. ->> -*) - -Inductive shru_cases: forall (e2: expr), Type := - | shru_case1: forall n2, shru_cases (Eop (Ointconst n2) Enil) - | shru_default: forall (e2: expr), shru_cases e2. - -Definition shru_match (e2: expr) := - match e2 as zz1 return shru_cases zz1 with - | Eop (Ointconst n2) Enil => shru_case1 n2 - | e2 => shru_default e2 - end. - -Definition shru (e1: expr) (e2: expr) := - match shru_match e2 with - | shru_case1 n2 => (* Eop (Ointconst n2) Enil *) - shruimm e1 n2 - | shru_default e2 => - Eop Oshru (e1:::e2:::Enil) - end. - - -(** ** Floating-point arithmetic *) - -Definition negf (e: expr) := Eop Onegf (e ::: Enil). -Definition absf (e: expr) := Eop Oabsf (e ::: Enil). -Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). -Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). -Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). -Definition divf (e1 e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). - -(** ** Comparisons *) - -(** Original definition: -<< -Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => - Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil) - | t1, Eop (Ointconst n2) Enil => - Eop (Ocmp (Ccompimm c n2)) (t1:::Enil) - | Eop (Oshift s) (t1:::Enil), t2 => - Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil) - | t1, Eop (Oshift s) (t2:::Enil) => - Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil) - | _, _ => - Eop (Ocmp (Ccomp c)) (e1:::e2:::Enil) - end. ->> -*) - -Inductive comp_cases: forall (e1: expr) (e2: expr), Type := - | comp_case1: forall n1 t2, comp_cases (Eop (Ointconst n1) Enil) (t2) - | comp_case2: forall t1 n2, comp_cases (t1) (Eop (Ointconst n2) Enil) - | comp_case3: forall s t1 t2, comp_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | comp_case4: forall t1 s t2, comp_cases (t1) (Eop (Oshift s) (t2:::Enil)) - | comp_default: forall (e1: expr) (e2: expr), comp_cases e1 e2. - -Definition comp_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return comp_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => comp_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => comp_case2 t1 n2 - | Eop (Oshift s) (t1:::Enil), t2 => comp_case3 s t1 t2 - | t1, Eop (Oshift s) (t2:::Enil) => comp_case4 t1 s t2 - | e1, e2 => comp_default e1 e2 - end. - -Definition comp (c: comparison) (e1: expr) (e2: expr) := - match comp_match e1 e2 with - | comp_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil) - | comp_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - Eop (Ocmp (Ccompimm c n2)) (t1:::Enil) - | comp_case3 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) - Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil) - | comp_case4 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) - Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil) - | comp_default e1 e2 => - Eop (Ocmp (Ccomp c)) (e1:::e2:::Enil) - end. - - -(** Original definition: -<< -Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => - Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2:::Enil) - | t1, Eop (Ointconst n2) Enil => - Eop (Ocmp (Ccompuimm c n2)) (t1:::Enil) - | Eop (Oshift s) (t1:::Enil), t2 => - Eop (Ocmp (Ccompushift (swap_comparison c) s)) (t2:::t1:::Enil) - | t1, Eop (Oshift s) (t2:::Enil) => - Eop (Ocmp (Ccompushift c s)) (t1:::t2:::Enil) - | _, _ => - Eop (Ocmp (Ccompu c)) (e1:::e2:::Enil) - end. ->> -*) - -Inductive compu_cases: forall (e1: expr) (e2: expr), Type := - | compu_case1: forall n1 t2, compu_cases (Eop (Ointconst n1) Enil) (t2) - | compu_case2: forall t1 n2, compu_cases (t1) (Eop (Ointconst n2) Enil) - | compu_case3: forall s t1 t2, compu_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | compu_case4: forall t1 s t2, compu_cases (t1) (Eop (Oshift s) (t2:::Enil)) - | compu_default: forall (e1: expr) (e2: expr), compu_cases e1 e2. - -Definition compu_match (e1: expr) (e2: expr) := - match e1 as zz1, e2 as zz2 return compu_cases zz1 zz2 with - | Eop (Ointconst n1) Enil, t2 => compu_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => compu_case2 t1 n2 - | Eop (Oshift s) (t1:::Enil), t2 => compu_case3 s t1 t2 - | t1, Eop (Oshift s) (t2:::Enil) => compu_case4 t1 s t2 - | e1, e2 => compu_default e1 e2 - end. - -Definition compu (c: comparison) (e1: expr) (e2: expr) := - match compu_match e1 e2 with - | compu_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) - Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2:::Enil) - | compu_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) - Eop (Ocmp (Ccompuimm c n2)) (t1:::Enil) - | compu_case3 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) - Eop (Ocmp (Ccompushift (swap_comparison c) s)) (t2:::t1:::Enil) - | compu_case4 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) - Eop (Ocmp (Ccompushift c s)) (t1:::t2:::Enil) - | compu_default e1 e2 => - Eop (Ocmp (Ccompu c)) (e1:::e2:::Enil) - end. - - -Definition compf (c: comparison) (e1: expr) (e2: expr) := - Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). - -(** ** Integer conversions *) - -Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e. - -Definition cast8signed (e: expr) := shrimm (shlimm e (Int.repr 24)) (Int.repr 24). - -Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e. - -Definition cast16signed (e: expr) := shrimm (shlimm e (Int.repr 16)) (Int.repr 16). - -(** ** Floating-point conversions *) - -Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). -Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). -Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). -Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). -Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil). - -(** ** Recognition of addressing modes for load and store operations *) - -(** We do not recognize the [Aindexed2] and [Aindexed2shift] modes - for floating-point accesses, since these are not supported - by the hardware and emulated inefficiently in [Asmgen]. - Likewise, [Aindexed2shift] are not supported for halfword - and signed byte accesses. *) - -Definition can_use_Aindexed2 (chunk: memory_chunk): bool := - match chunk with - | Mint8signed => true - | Mint8unsigned => true - | Mint16signed => true - | Mint16unsigned => true - | Mint32 => true - | Mfloat32 => false - | Mfloat64 => false - end. - -Definition can_use_Aindexed2shift (chunk: memory_chunk): bool := - match chunk with - | Mint8signed => false - | Mint8unsigned => true - | Mint16signed => false - | Mint16unsigned => false - | Mint32 => true - | Mfloat32 => false - | Mfloat64 => false - end. - -(** Original definition: -<< -Nondetfunction addressing (chunk: memory_chunk) (e: expr) := - match e with - | Eop (Oaddrstack n) Enil => (Ainstack n, Enil) - | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil) - | Eop (Oaddshift s) (e1:::e2:::Enil) => - if can_use_Aindexed2shift chunk - then (Aindexed2shift s, e1:::e2:::Enil) - else (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil) - | Eop Oadd (e1:::e2:::Enil) => - if can_use_Aindexed2 chunk - then (Aindexed2, e1:::e2:::Enil) - else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil) - | _ => (Aindexed Int.zero, e:::Enil) - end. ->> -*) - -Inductive addressing_cases: forall (e: expr), Type := - | addressing_case1: forall n, addressing_cases (Eop (Oaddrstack n) Enil) - | addressing_case2: forall n e1, addressing_cases (Eop (Oaddimm n) (e1:::Enil)) - | addressing_case3: forall s e1 e2, addressing_cases (Eop (Oaddshift s) (e1:::e2:::Enil)) - | addressing_case4: forall e1 e2, addressing_cases (Eop Oadd (e1:::e2:::Enil)) - | addressing_default: forall (e: expr), addressing_cases e. - -Definition addressing_match (e: expr) := - match e as zz1 return addressing_cases zz1 with - | Eop (Oaddrstack n) Enil => addressing_case1 n - | Eop (Oaddimm n) (e1:::Enil) => addressing_case2 n e1 - | Eop (Oaddshift s) (e1:::e2:::Enil) => addressing_case3 s e1 e2 - | Eop Oadd (e1:::e2:::Enil) => addressing_case4 e1 e2 - | e => addressing_default e - end. - -Definition addressing (chunk: memory_chunk) (e: expr) := - match addressing_match e with - | addressing_case1 n => (* Eop (Oaddrstack n) Enil *) - (Ainstack n, Enil) - | addressing_case2 n e1 => (* Eop (Oaddimm n) (e1:::Enil) *) - (Aindexed n, e1:::Enil) - | addressing_case3 s e1 e2 => (* Eop (Oaddshift s) (e1:::e2:::Enil) *) - if can_use_Aindexed2shift chunk then (Aindexed2shift s, e1:::e2:::Enil) else (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil) - | addressing_case4 e1 e2 => (* Eop Oadd (e1:::e2:::Enil) *) - if can_use_Aindexed2 chunk then (Aindexed2, e1:::e2:::Enil) else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil) - | addressing_default e => - (Aindexed Int.zero, e:::Enil) - end. - - - diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp new file mode 100644 index 00000000..432db948 --- /dev/null +++ b/arm/SelectOp.vp @@ -0,0 +1,444 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Instruction selection for operators *) + +(** The instruction selection pass recognizes opportunities for using + combined arithmetic and logical operations and addressing modes + offered by the target processor. For instance, the expression [x + 1] + can take advantage of the "immediate add" instruction of the processor, + and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned + into a "rotate and mask" instruction. + + This file defines functions for building CminorSel expressions and + statements, especially expressions consisting of operator + applications. These functions examine their arguments to choose + cheaper forms of operators whenever possible. + + For instance, [add e1 e2] will return a CminorSel expression semantically + equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a + [Oaddimm] operator if one of the arguments is an integer constant, + or suppress the addition altogether if one of the arguments is the + null integer. In passing, we perform operator reassociation + ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount + of constant propagation. + + On top of the "smart constructor" functions defined below, + module [Selection] implements the actual instruction selection pass. +*) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Cminor. +Require Import Op. +Require Import CminorSel. + +Open Local Scope cminorsel_scope. + +(** ** Constants **) + +Definition addrsymbol (id: ident) (ofs: int) := + Eop (Oaddrsymbol id ofs) Enil. + +Definition addrstack (ofs: int) := + Eop (Oaddrstack ofs) Enil. + +(** ** Integer logical negation *) + +Nondetfunction notint (e: expr) := + match e with + | Eop (Oshift s) (t1:::Enil) => Eop (Onotshift s) (t1:::Enil) + | Eop Onot (t1:::Enil) => t1 + | Eop (Onotshift s) (t1:::Enil) => Eop (Oshift s) (t1:::Enil) + | _ => Eop Onot (e:::Enil) + end. + +(** ** Boolean negation *) + +Fixpoint notbool (e: expr) {struct e} : expr := + let default := Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil) in + match e with + | Eop (Ointconst n) Enil => + Eop (Ointconst (if Int.eq n Int.zero then Int.one else Int.zero)) Enil + | Eop (Ocmp cond) args => + Eop (Ocmp (negate_condition cond)) args + | Econdition e1 e2 e3 => + Econdition e1 (notbool e2) (notbool e3) + | _ => + default + end. + +(** ** Integer addition and pointer addition *) + +Nondetfunction addimm (n: int) (e: expr) := + if Int.eq n Int.zero then e else + match e with + | Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil + | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Int.add n m)) Enil + | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Int.add n m)) Enil + | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil) + | _ => Eop (Oaddimm n) (e ::: Enil) + end. + +Nondetfunction add (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 + | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => + addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) + | Eop(Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil)) + | t1, Eop (Ointconst n2) Enil => addimm n2 t1 + | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil) + | _, _ => Eop Oadd (e1:::e2:::Enil) + end. + +(** ** Integer and pointer subtraction *) + +Nondetfunction sub (e1: expr) (e2: expr) := + match e1, e2 with + | t1, Eop (Ointconst n2) Enil => addimm (Int.neg n2) t1 + | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => + addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil)) + | Eop (Oaddimm n1) (t1:::Enil), t2 => + addimm n1 (Eop Osub (t1:::t2:::Enil)) + | t1, Eop (Oaddimm n2) (t2:::Enil) => + addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) + | Eop (Ointconst n1) Enil, t2 => Eop (Orsubimm n1) (t2:::Enil) + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Orsubshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Osubshift s) (t1:::t2:::Enil) + | _, _ => Eop Osub (e1:::e2:::Enil) + end. + +Definition negint (e: expr) := Eop (Orsubimm Int.zero) (e ::: Enil). + +(** ** Immediate shifts *) + +Nondetfunction shlimm (e1: expr) (n: int) := + if Int.eq n Int.zero then + e1 + else if negb (Int.ltu n Int.iwordsize) then + Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil) + else match e1 with + | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shl n1 n)) Enil + | Eop (Oshift (Slsl n1)) (t1:::Enil) => + if Int.ltu (Int.add n n1) Int.iwordsize + then Eop (Oshift (Slsl (mk_shift_amount(Int.add n n1)))) (t1:::Enil) + else Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil) + | _ => Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil) + end. + +Nondetfunction shruimm (e1: expr) (n: int) := + if Int.eq n Int.zero then + e1 + else if negb (Int.ltu n Int.iwordsize) then + Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil) + else match e1 with + | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shru n1 n)) Enil + | Eop (Oshift (Slsr n1)) (t1:::Enil) => + if Int.ltu (Int.add n n1) Int.iwordsize + then Eop (Oshift (Slsr (mk_shift_amount (Int.add n n1)))) (t1:::Enil) + else Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil) + | _ => Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil) + end. + +Nondetfunction shrimm (e1: expr) (n: int) := + if Int.eq n Int.zero then + e1 + else if negb (Int.ltu n Int.iwordsize) then + Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil) + else + match e1 with + | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shr n1 n)) Enil + | Eop (Oshift (Sasr n1)) (t1:::Enil) => + if Int.ltu (Int.add n n1) Int.iwordsize + then Eop (Oshift (Sasr (mk_shift_amount (Int.add n n1)))) (t1:::Enil) + else Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil) + | _ => Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil) + end. + +(** ** Integer multiply *) + +Definition mulimm_base (n1: int) (e2: expr) := + match Int.one_bits n1 with + | i :: nil => + shlimm e2 i + | i :: j :: nil => + Elet e2 + (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j)) + | _ => + Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil) + end. + +Nondetfunction mulimm (n1: int) (e2: expr) := + if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil + else if Int.eq n1 Int.one then e2 + else match e2 with + | Eop (Ointconst n2) Enil => Eop (Ointconst(Int.mul n1 n2)) Enil + | Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.mul n1 n2) (mulimm_base n1 t2) + | _ => mulimm_base n1 e2 + end. + +Nondetfunction mul (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => mulimm n1 t2 + | t1, Eop (Ointconst n2) Enil => mulimm n2 t1 + | _, _ => Eop Omul (e1:::e2:::Enil) + end. + +(** ** Bitwise and, or, xor *) + +Nondetfunction andimm (n1: int) (e2: expr) := + if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else + match e2 with + | Eop (Ointconst n2) Enil => + Eop (Ointconst (Int.and n1 n2)) Enil + | Eop (Oandimm n2) (t2:::Enil) => + Eop (Oandimm (Int.and n1 n2)) (t2:::Enil) + | _ => + Eop (Oandimm n1) (e2:::Enil) + end. + +Nondetfunction and (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => andimm n1 t2 + | t1, Eop (Ointconst n2) Enil => andimm n2 t1 + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oandshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oandshift s) (t1:::t2:::Enil) + | Eop (Onotshift s) (t1:::Enil), t2 => Eop (Obicshift s) (t2:::t1:::Enil) + | t1, Eop (Onotshift s) (t2:::Enil) => Eop (Obicshift s) (t1:::t2:::Enil) + | Eop Onot (t1:::Enil), t2 => Eop Obic (t2:::t1:::Enil) + | t1, Eop Onot (t2:::Enil) => Eop Obic (t1:::t2:::Enil) + | _, _ => Eop Oand (e1:::e2:::Enil) + end. + +Definition same_expr_pure (e1 e2: expr) := + match e1, e2 with + | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false + | _, _ => false + end. + +Nondetfunction orimm (n1: int) (e2: expr) := + if Int.eq n1 Int.zero then e2 else + match e2 with + | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil + | Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil) + | _ => Eop (Oorimm n1) (e2:::Enil) + end. + +Nondetfunction or (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => orimm n1 t2 + | t1, Eop (Ointconst n2) Enil => orimm n2 t1 + | Eop (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) => + if Int.eq (Int.add n1 n2) Int.iwordsize + && same_expr_pure t1 t2 + then Eop (Oshift (Sror n2)) (t1:::Enil) + else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil) + | Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) => + if Int.eq (Int.add n2 n1) Int.iwordsize + && same_expr_pure t1 t2 + then Eop (Oshift (Sror n1)) (t1:::Enil) + else Eop (Oorshift (Slsl n2)) (e1:::t2:::Enil) + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oorshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oorshift s) (t1:::t2:::Enil) + | _, _ => Eop Oor (e1:::e2:::Enil) + end. + +Nondetfunction xorimm (n1: int) (e2: expr) := + if Int.eq n1 Int.zero then e2 else + match e2 with + | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil + | Eop (Oxorimm n2) (t2:::Enil) => Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil) + | _ => Eop (Oxorimm n1) (e2:::Enil) + end. + +Nondetfunction xor (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => xorimm n1 t2 + | t1, Eop (Ointconst n2) Enil => xorimm n2 t1 + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oxorshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oxorshift s) (t1:::t2:::Enil) + | _, _ => Eop Oxor (e1:::e2:::Enil) + end. + +(** ** Integer division and modulus *) + +Definition mod_aux (divop: operation) (e1 e2: expr) := + Elet e1 + (Elet (lift e2) + (Eop Osub (Eletvar 1 ::: + Eop Omul (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) ::: + Eletvar 0 ::: + Enil) ::: + Enil))). + +Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). + +Definition mods := mod_aux Odiv. + +Definition divuimm (e: expr) (n: int) := + match Int.is_power2 n with + | Some l => shruimm e l + | None => Eop Odivu (e ::: Eop (Ointconst n) Enil ::: Enil) + end. + +Nondetfunction divu (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => divuimm e1 n2 + | _ => Eop Odivu (e1:::e2:::Enil) + end. + +Definition moduimm (e: expr) (n: int) := + match Int.is_power2 n with + | Some l => Eop (Oandimm (Int.sub n Int.one)) (e ::: Enil) + | None => mod_aux Odivu e (Eop (Ointconst n) Enil) + end. + +Nondetfunction modu (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => moduimm e1 n2 + | _ => mod_aux Odivu e1 e2 + end. + +(** ** General shifts *) + +Nondetfunction shl (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => shlimm e1 n2 + | _ => Eop Oshl (e1:::e2:::Enil) + end. + +Nondetfunction shr (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => shrimm e1 n2 + | _ => Eop Oshr (e1:::e2:::Enil) + end. + +Nondetfunction shru (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => shruimm e1 n2 + | _ => Eop Oshru (e1:::e2:::Enil) + end. + +(** ** Floating-point arithmetic *) + +Definition negf (e: expr) := Eop Onegf (e ::: Enil). +Definition absf (e: expr) := Eop Oabsf (e ::: Enil). +Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). +Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). +Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). +Definition divf (e1 e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). + +(** ** Comparisons *) + +Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => + Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil) + | t1, Eop (Ointconst n2) Enil => + Eop (Ocmp (Ccompimm c n2)) (t1:::Enil) + | Eop (Oshift s) (t1:::Enil), t2 => + Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => + Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil) + | _, _ => + Eop (Ocmp (Ccomp c)) (e1:::e2:::Enil) + end. + +Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => + Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2:::Enil) + | t1, Eop (Ointconst n2) Enil => + Eop (Ocmp (Ccompuimm c n2)) (t1:::Enil) + | Eop (Oshift s) (t1:::Enil), t2 => + Eop (Ocmp (Ccompushift (swap_comparison c) s)) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => + Eop (Ocmp (Ccompushift c s)) (t1:::t2:::Enil) + | _, _ => + Eop (Ocmp (Ccompu c)) (e1:::e2:::Enil) + end. + +Definition compf (c: comparison) (e1: expr) (e2: expr) := + Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). + +(** ** Integer conversions *) + +Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e. + +Definition cast8signed (e: expr) := shrimm (shlimm e (Int.repr 24)) (Int.repr 24). + +Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e. + +Definition cast16signed (e: expr) := shrimm (shlimm e (Int.repr 16)) (Int.repr 16). + +(** ** Floating-point conversions *) + +Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). +Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). +Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). +Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). +Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil). + +(** ** Recognition of addressing modes for load and store operations *) + +(** We do not recognize the [Aindexed2] and [Aindexed2shift] modes + for floating-point accesses, since these are not supported + by the hardware and emulated inefficiently in [Asmgen]. + Likewise, [Aindexed2shift] are not supported for halfword + and signed byte accesses. *) + +Definition can_use_Aindexed2 (chunk: memory_chunk): bool := + match chunk with + | Mint8signed => true + | Mint8unsigned => true + | Mint16signed => true + | Mint16unsigned => true + | Mint32 => true + | Mfloat32 => false + | Mfloat64 => false + end. + +Definition can_use_Aindexed2shift (chunk: memory_chunk): bool := + match chunk with + | Mint8signed => false + | Mint8unsigned => true + | Mint16signed => false + | Mint16unsigned => false + | Mint32 => true + | Mfloat32 => false + | Mfloat64 => false + end. + +Nondetfunction addressing (chunk: memory_chunk) (e: expr) := + match e with + | Eop (Oaddrstack n) Enil => (Ainstack n, Enil) + | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil) + | Eop (Oaddshift s) (e1:::e2:::Enil) => + if can_use_Aindexed2shift chunk + then (Aindexed2shift s, e1:::e2:::Enil) + else (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil) + | Eop Oadd (e1:::e2:::Enil) => + if can_use_Aindexed2 chunk + then (Aindexed2, e1:::e2:::Enil) + else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil) + | _ => (Aindexed Int.zero, e:::Enil) + end. + + diff --git a/backend/Constprop.v b/backend/Constprop.v index 4c303ac4..c3b98634 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -199,6 +199,9 @@ Definition transf_instr (app: D.t) (instr: instruction) := Icall sig (transf_ros app ros) args res s | Itailcall sig ros args => Itailcall sig (transf_ros app ros) args + | Ibuiltin ef args res s => + let (ef', args') := builtin_strength_reduction ef args (approx_regs app args) in + Ibuiltin ef' args' res s | Icond cond args s1 s2 => match eval_static_condition cond (approx_regs app args) with | Some b => diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 7ac43391..9affea88 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -416,12 +416,16 @@ Proof. constructor; auto. apply regs_lessdef_regs; auto. (* Ibuiltin *) +Opaque builtin_strength_reduction. + destruct (builtin_strength_reduction ef args (approx_regs (analyze f)#pc args)) as [ef' args']_eqn. + generalize (builtin_strength_reduction_correct ge sp (analyze f)!!pc rs + MATCH ef args (approx_regs (analyze f) # pc args) _ _ _ _ (refl_equal _) H0). + rewrite Heqp. intros P. exploit external_call_mem_extends; eauto. - instantiate (1 := rs'##args). apply regs_lessdef_regs; auto. + instantiate (1 := rs'##args'). apply regs_lessdef_regs; auto. intros [v' [m2' [A [B [C D]]]]]. - TransfInstr. intro. exists (State s' (transf_function f) sp pc' (rs'#res <- v') m2'); split. - eapply exec_Ibuiltin; eauto. + eapply exec_Ibuiltin. TransfInstr. rewrite Heqp. eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index e3b57c51..4bce5355 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -1270,6 +1270,20 @@ Definition do_ef_volatile_store (chunk: memory_chunk) | _ => None end. +Definition do_ef_volatile_load_global (chunk: memory_chunk) (id: ident) (ofs: int) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match Genv.find_symbol genv id with + | Some b => do_ef_volatile_load chunk w (Vptr b ofs :: vargs) m + | None => None + end. + +Definition do_ef_volatile_store_global (chunk: memory_chunk) (id: ident) (ofs: int) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match Genv.find_symbol genv id with + | Some b => do_ef_volatile_store chunk w (Vptr b ofs :: vargs) m + | None => None + end. + Definition do_ef_malloc (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := match vargs with @@ -1358,6 +1372,8 @@ Definition do_external (ef: external_function): | EF_builtin name sg => do_ef_external name sg | EF_vload chunk => do_ef_volatile_load chunk | EF_vstore chunk => do_ef_volatile_store chunk + | EF_vload_global chunk id ofs => do_ef_volatile_load_global chunk id ofs + | EF_vstore_global chunk id ofs => do_ef_volatile_store_global chunk id ofs | EF_malloc => do_ef_malloc | EF_free => do_ef_free | EF_memcpy sz al => do_ef_memcpy sz al @@ -1389,25 +1405,45 @@ Proof with try congruence. apply val_of_eventval_sound; auto. econstructor. constructor; eauto. constructor. - destruct ef; simpl. -(* EF_external *) - auto. -(* EF_builtin *) - auto. -(* EF_vload *) - unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... + assert (VLOAD: forall chunk vargs, + do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m') -> + volatile_load_sem chunk genv vargs m t vres m' /\ possible_trace w t w'). + intros chunk vargs'. + unfold do_ef_volatile_load. destruct vargs'... destruct v... destruct vargs'... mydestr. destruct p as [res w'']; mydestr. split. constructor. apply Genv.invert_find_symbol; auto. auto. apply val_of_eventval_sound; auto. econstructor. constructor; eauto. constructor. split. constructor; auto. constructor. -(* EF_vstore *) - unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs... + + assert (VSTORE: forall chunk vargs, + do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m') -> + volatile_store_sem chunk genv vargs m t vres m' /\ possible_trace w t w'). + intros chunk vargs'. + unfold do_ef_volatile_store. destruct vargs'... destruct v... destruct vargs'... destruct vargs'... mydestr. split. constructor. apply Genv.invert_find_symbol; auto. auto. apply eventval_of_val_sound; auto. econstructor. constructor; eauto. constructor. split. constructor; auto. constructor. + + destruct ef; simpl. +(* EF_external *) + auto. +(* EF_builtin *) + auto. +(* EF_vload *) + auto. +(* EF_vstore *) + auto. +(* EF_vload_global *) + rewrite volatile_load_global_charact. + unfold do_ef_volatile_load_global. destruct (Genv.find_symbol genv)... + intros. exploit VLOAD; eauto. intros [A B]. split; auto. exists b; auto. +(* EF_vstore_global *) + rewrite volatile_store_global_charact. + unfold do_ef_volatile_store_global. destruct (Genv.find_symbol genv)... + intros. exploit VSTORE; eauto. intros [A B]. split; auto. exists b; auto. (* EF_malloc *) unfold do_ef_malloc. destruct vargs... destruct v... destruct vargs... destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b]_eqn. mydestr. @@ -1443,23 +1479,39 @@ Proof. unfold do_ef_external. rewrite (list_eventval_of_val_complete _ _ _ H2). rewrite H8. rewrite (val_of_eventval_complete _ _ _ H3). auto. + assert (VLOAD: forall chunk vargs, + volatile_load_sem chunk genv vargs m t vres m' -> + do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m')). + intros. inv H1; unfold do_ef_volatile_load. + inv H0. inv H9. inv H7. + rewrite H3. rewrite (Genv.find_invert_symbol _ _ H2). rewrite H10. + rewrite (val_of_eventval_complete _ _ _ H4). auto. + inv H0. rewrite H2. rewrite H3. auto. + + assert (VSTORE: forall chunk vargs, + volatile_store_sem chunk genv vargs m t vres m' -> + do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m')). + intros. inv H1; unfold do_ef_volatile_store. + inv H0. inv H9. inv H7. + rewrite H3. rewrite (Genv.find_invert_symbol _ _ H2). + rewrite (eventval_of_val_complete _ _ _ H4). rewrite H10. auto. + inv H0. rewrite H2. rewrite H3. auto. + destruct ef; simpl in *. (* EF_external *) auto. (* EF_builtin *) auto. (* EF_vload *) - inv H; unfold do_ef_volatile_load. - inv H0. inv H8. inv H6. - rewrite H2. rewrite (Genv.find_invert_symbol _ _ H1). rewrite H9. - rewrite (val_of_eventval_complete _ _ _ H3). auto. - inv H0. rewrite H1. rewrite H2. auto. + auto. (* EF_vstore *) - inv H; unfold do_ef_volatile_store. - inv H0. inv H8. inv H6. - rewrite H2. rewrite (Genv.find_invert_symbol _ _ H1). - rewrite (eventval_of_val_complete _ _ _ H3). rewrite H9. auto. - inv H0. rewrite H1. rewrite H2. auto. + auto. +(* EF_vload_global *) + rewrite volatile_load_global_charact in H. destruct H as [b [P Q]]. + unfold do_ef_volatile_load_global. rewrite P. auto. +(* EF_vstore *) + rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. + unfold do_ef_volatile_store_global. rewrite P. auto. (* EF_malloc *) inv H; unfold do_ef_malloc. inv H0. rewrite H1. rewrite H2. auto. diff --git a/common/AST.v b/common/AST.v index 4f113c79..becf4e42 100644 --- a/common/AST.v +++ b/common/AST.v @@ -418,6 +418,12 @@ Inductive external_function : Type := (** A volatile store operation. If the adress given as first argument points within a volatile global variable, generate an event. Otherwise, produce no event and behave like a regular memory store. *) + | EF_vload_global (chunk: memory_chunk) (id: ident) (ofs: int) + (** A volatile load operation from a global variable. + Specialized version of [EF_vload]. *) + | EF_vstore_global (chunk: memory_chunk) (id: ident) (ofs: int) + (** A volatile store operation in a global variable. + Specialized version of [EF_vstore]. *) | EF_malloc (** Dynamic memory allocation. Takes the requested size in bytes as argument; returns a pointer to a fresh block of the given size. @@ -446,6 +452,8 @@ Definition ef_sig (ef: external_function): signature := | EF_builtin name sg => sg | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None + | EF_vload_global chunk _ _ => mksignature nil (Some (type_of_chunk chunk)) + | EF_vstore_global chunk _ _ => mksignature (type_of_chunk chunk :: nil) None | EF_malloc => mksignature (Tint :: nil) (Some Tint) | EF_free => mksignature (Tint :: nil) None | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None @@ -461,6 +469,8 @@ Definition ef_inline (ef: external_function) : bool := | EF_builtin name sg => true | EF_vload chunk => true | EF_vstore chunk => true + | EF_vload_global chunk id ofs => true + | EF_vstore_global chunk id ofs => true | EF_malloc => false | EF_free => false | EF_memcpy sz al => true diff --git a/common/Events.v b/common/Events.v index f18c091e..018314e1 100644 --- a/common/Events.v +++ b/common/Events.v @@ -725,6 +725,104 @@ Proof. split. constructor. intuition congruence. Qed. +Inductive volatile_load_global_sem (chunk: memory_chunk) (id: ident) (ofs: int) + (F V: Type) (ge: Genv.t F V): + list val -> mem -> trace -> val -> mem -> Prop := + | volatile_load_global_sem_vol: forall b m ev v, + Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true -> + eventval_match ge ev (type_of_chunk chunk) v -> + volatile_load_global_sem chunk id ofs ge + nil m + (Event_vload chunk id ofs ev :: nil) + (Val.load_result chunk v) m + | volatile_load_global_sem_nonvol: forall b m v, + Genv.find_symbol ge id = Some b -> block_is_volatile ge b = false -> + Mem.load chunk m b (Int.unsigned ofs) = Some v -> + volatile_load_global_sem chunk id ofs ge + nil m + E0 + v m. + +Remark volatile_load_global_charact: + forall chunk id ofs (F V: Type) (ge: Genv.t F V) vargs m t vres m', + volatile_load_global_sem chunk id ofs ge vargs m t vres m' <-> + exists b, Genv.find_symbol ge id = Some b /\ volatile_load_sem chunk ge (Vptr b ofs :: vargs) m t vres m'. +Proof. + intros; split. + intros. inv H; exists b; split; auto; constructor; auto. + intros [b [P Q]]. inv Q. + assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0. econstructor; eauto. + econstructor; eauto. +Qed. + +Lemma volatile_load_global_ok: + forall chunk id ofs, + extcall_properties (volatile_load_global_sem chunk id ofs) + (mksignature nil (Some (type_of_chunk chunk))). +Proof. + intros; constructor; intros. +(* well typed *) + unfold proj_sig_res; simpl. destruct H. + destruct chunk; destruct v; simpl; constructor. + eapply Mem.load_type; eauto. +(* arity *) + destruct H; simpl; auto. +(* symbols *) + destruct H1. + econstructor; eauto. rewrite H; auto. eapply eventval_match_preserved; eauto. + econstructor; eauto. rewrite H; auto. +(* valid blocks *) + destruct H; auto. +(* bounds *) + destruct H; auto. +(* mem extends *) + destruct H. + inv H1. + exists (Val.load_result chunk v); exists m1'; intuition. + econstructor; eauto. + red; auto. + inv H1. + exploit Mem.load_extends; eauto. intros [v' [A B]]. + exists v'; exists m1'; intuition. + econstructor; eauto. + red; auto. +(* mem injects *) + destruct H0. + inv H2. + exists f; exists (Val.load_result chunk v); exists m1'; intuition. + econstructor; eauto. + apply val_load_result_inject. eapply eventval_match_inject_2; eauto. + red; auto. + red; auto. + red; intros. congruence. + inv H2. destruct H as [P [Q R]]. exploit P; eauto. intros EQ. + exploit Mem.load_inject; eauto. rewrite Zplus_0_r. intros [v1 [A B]]. + exists f; exists v1; exists m1'; intuition. + econstructor; eauto. + red; auto. + red; auto. + red; intros. congruence. +(* trace length *) + inv H; simpl; omega. +(* receptive *) + inv H; inv H0. + exploit eventval_match_valid; eauto. intros [A B]. + exploit eventval_valid_match. eexact H9. rewrite <- H10; eauto. + intros [v' EVM]. exists (Val.load_result chunk v'); exists m1. + eapply volatile_load_global_sem_vol; eauto. + exists vres1; exists m1; eapply volatile_load_global_sem_nonvol; eauto. +(* determ *) + inv H; inv H0; try congruence. + assert (b = b0) by congruence. subst b0. + exploit eventval_match_valid. eexact H3. intros [V1 T1]. + exploit eventval_match_valid. eexact H5. intros [V2 T2]. + split. constructor; auto. congruence. + intros EQ; inv EQ. + assert (v = v0) by (eapply eventval_match_determ_1; eauto). subst v0. + auto. + split. constructor. intuition congruence. +Qed. + (** ** Semantics of volatile stores *) Inductive volatile_store_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V): @@ -835,6 +933,80 @@ Proof. split. constructor. intuition congruence. Qed. +Inductive volatile_store_global_sem (chunk: memory_chunk) (id: ident) (ofs: int) + (F V: Type) (ge: Genv.t F V): + list val -> mem -> trace -> val -> mem -> Prop := + | volatile_store_global_sem_vol: forall b m ev v, + Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true -> + eventval_match ge ev (type_of_chunk chunk) v -> + volatile_store_global_sem chunk id ofs ge + (v :: nil) m + (Event_vstore chunk id ofs ev :: nil) + Vundef m + | volatile_store_global_sem_nonvol: forall b m v m', + Genv.find_symbol ge id = Some b -> block_is_volatile ge b = false -> + Mem.store chunk m b (Int.unsigned ofs) v = Some m' -> + volatile_store_global_sem chunk id ofs ge + (v :: nil) m + E0 + Vundef m'. + +Remark volatile_store_global_charact: + forall chunk id ofs (F V: Type) (ge: Genv.t F V) vargs m t vres m', + volatile_store_global_sem chunk id ofs ge vargs m t vres m' <-> + exists b, Genv.find_symbol ge id = Some b /\ volatile_store_sem chunk ge (Vptr b ofs :: vargs) m t vres m'. +Proof. + intros; split. + intros. inv H; exists b; split; auto; econstructor; eauto. + intros [b [P Q]]. inv Q. + assert (id0 = id) by (eapply Genv.genv_vars_inj; eauto). subst id0. econstructor; eauto. + econstructor; eauto. +Qed. + +Lemma volatile_store_global_ok: + forall chunk id ofs, + extcall_properties (volatile_store_global_sem chunk id ofs) + (mksignature (type_of_chunk chunk :: nil) None). +Proof. + intros; constructor; intros. +(* well typed *) + unfold proj_sig_res; simpl. inv H; constructor. +(* arity *) + inv H; simpl; auto. +(* symbols preserved *) + inv H1. + econstructor. rewrite H; eauto. rewrite H0; auto. eapply eventval_match_preserved; eauto. + econstructor; eauto. rewrite H; auto. +(* valid block *) + inv H. auto. eauto with mem. +(* bounds *) + inv H. auto. eapply Mem.bounds_store; eauto. +(* mem extends*) + rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. + exploit ec_mem_extends. eapply volatile_store_ok. eexact Q. eauto. eauto. + intros [vres' [m2' [A [B [C D]]]]]. + exists vres'; exists m2'; intuition. rewrite volatile_store_global_charact. exists b; auto. +(* mem inject *) + rewrite volatile_store_global_charact in H0. destruct H0 as [b [P Q]]. + exploit (proj1 H). eauto. intros EQ. + assert (val_inject f (Vptr b ofs) (Vptr b ofs)). econstructor; eauto. rewrite Int.add_zero; auto. + exploit ec_mem_inject. eapply volatile_store_ok. eauto. eexact Q. eauto. eauto. + intros [f' [vres' [m2' [A [B [C [D [E G]]]]]]]]. + exists f'; exists vres'; exists m2'; intuition. + rewrite volatile_store_global_charact. exists b; auto. +(* trace length *) + inv H; simpl; omega. +(* receptive *) + assert (t1 = t2). inv H; inv H0; auto. + exists vres1; exists m1; congruence. +(* determ *) + inv H; inv H0; try congruence. + assert (b = b0) by congruence. subst b0. + assert (ev = ev0) by (eapply eventval_match_determ_2; eauto). subst ev0. + split. constructor. auto. + split. constructor. intuition congruence. +Qed. + (** ** Semantics of dynamic memory allocation (malloc) *) Inductive extcall_malloc_sem (F V: Type) (ge: Genv.t F V): @@ -1289,6 +1461,8 @@ Definition external_call (ef: external_function): extcall_sem := | EF_builtin name sg => extcall_io_sem name sg | EF_vload chunk => volatile_load_sem chunk | EF_vstore chunk => volatile_store_sem chunk + | EF_vload_global chunk id ofs => volatile_load_global_sem chunk id ofs + | EF_vstore_global chunk id ofs => volatile_store_global_sem chunk id ofs | EF_malloc => extcall_malloc_sem | EF_free => extcall_free_sem | EF_memcpy sz al => extcall_memcpy_sem sz al @@ -1305,6 +1479,8 @@ Proof. apply extcall_io_ok. apply volatile_load_ok. apply volatile_store_ok. + apply volatile_load_global_ok. + apply volatile_store_global_ok. apply extcall_malloc_ok. apply extcall_free_ok. apply extcall_memcpy_ok. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index e0659766..baa5578c 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -32,6 +32,12 @@ let name_of_external = function | EF_builtin(name, sg) -> extern_atom name | EF_vload chunk -> sprintf "volatile load %s" (name_of_chunk chunk) | EF_vstore chunk -> sprintf "volatile store %s" (name_of_chunk chunk) + | EF_vload_global(chunk, id, ofs) -> + sprintf "volatile load %s global %s %ld" + (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) + | EF_vstore_global(chunk, id, ofs) -> + sprintf "volatile store %s global %s %ld" + (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) | EF_malloc -> "malloc" | EF_free -> "free" | EF_memcpy(sz, al) -> diff --git a/ia32/ConstpropOp.v b/ia32/ConstpropOp.v deleted file mode 100644 index 3d07a4d4..00000000 --- a/ia32/ConstpropOp.v +++ /dev/null @@ -1,805 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Static analysis and strength reduction for operators - and conditions. This is the machine-dependent part of [Constprop]. *) - -Require Import Coqlib. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Op. -Require Import Registers. - -(** * 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. *) - | 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. *) - -(** 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 [Vfloat f] - and [Vfloat g] respectively, and [Unknown] otherwise. - - 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. *) - -(** Original definition: -<< -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) - | 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)) - | Cmaskzero n, I n1 :: nil => Some(Int.eq (Int.and n1 n) Int.zero) - | Cmasknotzero n, I n1::nil => Some(negb(Int.eq (Int.and n1 n) Int.zero)) - | _, _ => None - end. ->> -*) - -Inductive eval_static_condition_cases: forall (cond: condition) (vl: list approx), Type := - | eval_static_condition_case1: forall c n1 n2, eval_static_condition_cases (Ccomp c) (I n1 :: I n2 :: nil) - | eval_static_condition_case2: forall c n1 n2, eval_static_condition_cases (Ccompu c) (I n1 :: I n2 :: nil) - | eval_static_condition_case3: forall c n n1, eval_static_condition_cases (Ccompimm c n) (I n1 :: nil) - | eval_static_condition_case4: forall c n n1, eval_static_condition_cases (Ccompuimm c n) (I n1 :: nil) - | eval_static_condition_case5: forall c n1 n2, eval_static_condition_cases (Ccompf c) (F n1 :: F n2 :: nil) - | eval_static_condition_case6: forall c n1 n2, eval_static_condition_cases (Cnotcompf c) (F n1 :: F n2 :: nil) - | eval_static_condition_case7: forall n n1, eval_static_condition_cases (Cmaskzero n) (I n1 :: nil) - | eval_static_condition_case8: forall n n1, eval_static_condition_cases (Cmasknotzero n) (I n1::nil) - | eval_static_condition_default: forall (cond: condition) (vl: list approx), eval_static_condition_cases cond vl. - -Definition eval_static_condition_match (cond: condition) (vl: list approx) := - match cond as zz1, vl as zz2 return eval_static_condition_cases zz1 zz2 with - | Ccomp c, I n1 :: I n2 :: nil => eval_static_condition_case1 c n1 n2 - | Ccompu c, I n1 :: I n2 :: nil => eval_static_condition_case2 c n1 n2 - | Ccompimm c n, I n1 :: nil => eval_static_condition_case3 c n n1 - | Ccompuimm c n, I n1 :: nil => eval_static_condition_case4 c n n1 - | Ccompf c, F n1 :: F n2 :: nil => eval_static_condition_case5 c n1 n2 - | Cnotcompf c, F n1 :: F n2 :: nil => eval_static_condition_case6 c n1 n2 - | Cmaskzero n, I n1 :: nil => eval_static_condition_case7 n n1 - | Cmasknotzero n, I n1::nil => eval_static_condition_case8 n n1 - | cond, vl => eval_static_condition_default cond vl - end. - -Definition eval_static_condition (cond: condition) (vl: list approx) := - match eval_static_condition_match cond vl with - | eval_static_condition_case1 c n1 n2 => (* Ccomp c, I n1 :: I n2 :: nil *) - Some(Int.cmp c n1 n2) - | eval_static_condition_case2 c n1 n2 => (* Ccompu c, I n1 :: I n2 :: nil *) - Some(Int.cmpu c n1 n2) - | eval_static_condition_case3 c n n1 => (* Ccompimm c n, I n1 :: nil *) - Some(Int.cmp c n1 n) - | eval_static_condition_case4 c n n1 => (* Ccompuimm c n, I n1 :: nil *) - Some(Int.cmpu c n1 n) - | eval_static_condition_case5 c n1 n2 => (* Ccompf c, F n1 :: F n2 :: nil *) - Some(Float.cmp c n1 n2) - | eval_static_condition_case6 c n1 n2 => (* Cnotcompf c, F n1 :: F n2 :: nil *) - Some(negb(Float.cmp c n1 n2)) - | eval_static_condition_case7 n n1 => (* Cmaskzero n, I n1 :: nil *) - Some(Int.eq (Int.and n1 n) Int.zero) - | eval_static_condition_case8 n n1 => (* Cmasknotzero n, I n1::nil *) - Some(negb(Int.eq (Int.and n1 n) Int.zero)) - | eval_static_condition_default cond vl => - 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. - -(** Original definition: -<< -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 n, I n1::I n2::nil => I (Int.add (Int.add n1 n2) n) - | Aindexed2 n, G id ofs::I n2::nil => G id (Int.add (Int.add ofs n2) n) - | Aindexed2 n, I n1::G id ofs::nil => G id (Int.add (Int.add ofs n1) n) - | Aindexed2 n, S ofs::I n2::nil => S (Int.add (Int.add ofs n2) n) - | Aindexed2 n, I n1::S ofs::nil => S (Int.add (Int.add ofs n1) n) - | Ascaled sc n, I n1::nil => I (Int.add (Int.mul n1 sc) n) - | Aindexed2scaled sc n, I n1::I n2::nil => I (Int.add n1 (Int.add (Int.mul n2 sc) n)) - | Aindexed2scaled sc n, G id ofs::I n2::nil => G id (Int.add ofs (Int.add (Int.mul n2 sc) n)) - | Aindexed2scaled sc n, S ofs::I n2::nil => S (Int.add ofs (Int.add (Int.mul n2 sc) n)) - | Aglobal id ofs, nil => G id ofs - | Abased id ofs, I n1::nil => G id (Int.add ofs n1) - | Abasedscaled sc id ofs, I n1::nil => G id (Int.add ofs (Int.mul sc n1)) - | Ainstack ofs, nil => S ofs - | _, _ => Unknown - end. ->> -*) - -Inductive eval_static_addressing_cases: forall (addr: addressing) (vl: list approx), Type := - | eval_static_addressing_case1: forall n n1, eval_static_addressing_cases (Aindexed n) (I n1::nil) - | eval_static_addressing_case2: forall n id ofs, eval_static_addressing_cases (Aindexed n) (G id ofs::nil) - | eval_static_addressing_case3: forall n ofs, eval_static_addressing_cases (Aindexed n) (S ofs::nil) - | eval_static_addressing_case4: forall n n1 n2, eval_static_addressing_cases (Aindexed2 n) (I n1::I n2::nil) - | eval_static_addressing_case5: forall n id ofs n2, eval_static_addressing_cases (Aindexed2 n) (G id ofs::I n2::nil) - | eval_static_addressing_case6: forall n n1 id ofs, eval_static_addressing_cases (Aindexed2 n) (I n1::G id ofs::nil) - | eval_static_addressing_case7: forall n ofs n2, eval_static_addressing_cases (Aindexed2 n) (S ofs::I n2::nil) - | eval_static_addressing_case8: forall n n1 ofs, eval_static_addressing_cases (Aindexed2 n) (I n1::S ofs::nil) - | eval_static_addressing_case9: forall sc n n1, eval_static_addressing_cases (Ascaled sc n) (I n1::nil) - | eval_static_addressing_case10: forall sc n n1 n2, eval_static_addressing_cases (Aindexed2scaled sc n) (I n1::I n2::nil) - | eval_static_addressing_case11: forall sc n id ofs n2, eval_static_addressing_cases (Aindexed2scaled sc n) (G id ofs::I n2::nil) - | eval_static_addressing_case12: forall sc n ofs n2, eval_static_addressing_cases (Aindexed2scaled sc n) (S ofs::I n2::nil) - | eval_static_addressing_case13: forall id ofs, eval_static_addressing_cases (Aglobal id ofs) (nil) - | eval_static_addressing_case14: forall id ofs n1, eval_static_addressing_cases (Abased id ofs) (I n1::nil) - | eval_static_addressing_case15: forall sc id ofs n1, eval_static_addressing_cases (Abasedscaled sc id ofs) (I n1::nil) - | eval_static_addressing_case16: forall ofs, eval_static_addressing_cases (Ainstack ofs) (nil) - | eval_static_addressing_default: forall (addr: addressing) (vl: list approx), eval_static_addressing_cases addr vl. - -Definition eval_static_addressing_match (addr: addressing) (vl: list approx) := - match addr as zz1, vl as zz2 return eval_static_addressing_cases zz1 zz2 with - | Aindexed n, I n1::nil => eval_static_addressing_case1 n n1 - | Aindexed n, G id ofs::nil => eval_static_addressing_case2 n id ofs - | Aindexed n, S ofs::nil => eval_static_addressing_case3 n ofs - | Aindexed2 n, I n1::I n2::nil => eval_static_addressing_case4 n n1 n2 - | Aindexed2 n, G id ofs::I n2::nil => eval_static_addressing_case5 n id ofs n2 - | Aindexed2 n, I n1::G id ofs::nil => eval_static_addressing_case6 n n1 id ofs - | Aindexed2 n, S ofs::I n2::nil => eval_static_addressing_case7 n ofs n2 - | Aindexed2 n, I n1::S ofs::nil => eval_static_addressing_case8 n n1 ofs - | Ascaled sc n, I n1::nil => eval_static_addressing_case9 sc n n1 - | Aindexed2scaled sc n, I n1::I n2::nil => eval_static_addressing_case10 sc n n1 n2 - | Aindexed2scaled sc n, G id ofs::I n2::nil => eval_static_addressing_case11 sc n id ofs n2 - | Aindexed2scaled sc n, S ofs::I n2::nil => eval_static_addressing_case12 sc n ofs n2 - | Aglobal id ofs, nil => eval_static_addressing_case13 id ofs - | Abased id ofs, I n1::nil => eval_static_addressing_case14 id ofs n1 - | Abasedscaled sc id ofs, I n1::nil => eval_static_addressing_case15 sc id ofs n1 - | Ainstack ofs, nil => eval_static_addressing_case16 ofs - | addr, vl => eval_static_addressing_default addr vl - end. - -Definition eval_static_addressing (addr: addressing) (vl: list approx) := - match eval_static_addressing_match addr vl with - | eval_static_addressing_case1 n n1 => (* Aindexed n, I n1::nil *) - I (Int.add n1 n) - | eval_static_addressing_case2 n id ofs => (* Aindexed n, G id ofs::nil *) - G id (Int.add ofs n) - | eval_static_addressing_case3 n ofs => (* Aindexed n, S ofs::nil *) - S (Int.add ofs n) - | eval_static_addressing_case4 n n1 n2 => (* Aindexed2 n, I n1::I n2::nil *) - I (Int.add (Int.add n1 n2) n) - | eval_static_addressing_case5 n id ofs n2 => (* Aindexed2 n, G id ofs::I n2::nil *) - G id (Int.add (Int.add ofs n2) n) - | eval_static_addressing_case6 n n1 id ofs => (* Aindexed2 n, I n1::G id ofs::nil *) - G id (Int.add (Int.add ofs n1) n) - | eval_static_addressing_case7 n ofs n2 => (* Aindexed2 n, S ofs::I n2::nil *) - S (Int.add (Int.add ofs n2) n) - | eval_static_addressing_case8 n n1 ofs => (* Aindexed2 n, I n1::S ofs::nil *) - S (Int.add (Int.add ofs n1) n) - | eval_static_addressing_case9 sc n n1 => (* Ascaled sc n, I n1::nil *) - I (Int.add (Int.mul n1 sc) n) - | eval_static_addressing_case10 sc n n1 n2 => (* Aindexed2scaled sc n, I n1::I n2::nil *) - I (Int.add n1 (Int.add (Int.mul n2 sc) n)) - | eval_static_addressing_case11 sc n id ofs n2 => (* Aindexed2scaled sc n, G id ofs::I n2::nil *) - G id (Int.add ofs (Int.add (Int.mul n2 sc) n)) - | eval_static_addressing_case12 sc n ofs n2 => (* Aindexed2scaled sc n, S ofs::I n2::nil *) - S (Int.add ofs (Int.add (Int.mul n2 sc) n)) - | eval_static_addressing_case13 id ofs => (* Aglobal id ofs, nil *) - G id ofs - | eval_static_addressing_case14 id ofs n1 => (* Abased id ofs, I n1::nil *) - G id (Int.add ofs n1) - | eval_static_addressing_case15 sc id ofs n1 => (* Abasedscaled sc id ofs, I n1::nil *) - G id (Int.add ofs (Int.mul sc n1)) - | eval_static_addressing_case16 ofs => (* Ainstack ofs, nil *) - S ofs - | eval_static_addressing_default addr vl => - Unknown - end. - - -(** Original definition: -<< -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 => F n - | Ocast8signed, I n1 :: nil => I(Int.sign_ext 8 n1) - | Ocast8unsigned, I n1 :: nil => I(Int.zero_ext 8 n1) - | Ocast16signed, I n1 :: nil => I(Int.sign_ext 16 n1) - | Ocast16unsigned, I n1 :: nil => I(Int.zero_ext 16 n1) - | Oneg, I n1 :: nil => I(Int.neg n1) - | Osub, I n1 :: I n2 :: nil => I(Int.sub n1 n2) - | Osub, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 n2) - | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2) - | Omulimm n, I n1 :: nil => I(Int.mul n1 n) - | Odiv, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero 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) - | Omod, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.mods n1 n2) - | Omodu, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.modu n1 n2) - | Oand, I n1 :: I n2 :: nil => I(Int.and n1 n2) - | Oandimm n, I n1 :: nil => I(Int.and n1 n) - | Oor, I n1 :: I n2 :: nil => I(Int.or n1 n2) - | Oorimm n, I n1 :: nil => I(Int.or n1 n) - | Oxor, I n1 :: I n2 :: nil => I(Int.xor n1 n2) - | Oxorimm n, I n1 :: nil => I(Int.xor n1 n) - | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown - | Oshlimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shl n1 n) else Unknown - | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown - | Oshrimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shr n1 n) else Unknown - | Oshrximm n, I n1 :: nil => if Int.ltu n (Int.repr 31) then I(Int.shrx n1 n) else Unknown - | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown - | Oshruimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shru n1 n) else Unknown - | Ororimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.ror n1 n) else Unknown - | Olea mode, vl => eval_static_addressing mode vl - | 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 - | Ofloatofint, I n1 :: nil => F(Float.floatofint n1) - | Ocmp c, vl => eval_static_condition_val c vl - | _, _ => Unknown - end. ->> -*) - -Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), Type := - | eval_static_operation_case1: forall v1, eval_static_operation_cases (Omove) (v1::nil) - | eval_static_operation_case2: forall n, eval_static_operation_cases (Ointconst n) (nil) - | eval_static_operation_case3: forall n, eval_static_operation_cases (Ofloatconst n) (nil) - | eval_static_operation_case4: forall n1, eval_static_operation_cases (Ocast8signed) (I n1 :: nil) - | eval_static_operation_case5: forall n1, eval_static_operation_cases (Ocast8unsigned) (I n1 :: nil) - | eval_static_operation_case6: forall n1, eval_static_operation_cases (Ocast16signed) (I n1 :: nil) - | eval_static_operation_case7: forall n1, eval_static_operation_cases (Ocast16unsigned) (I n1 :: nil) - | eval_static_operation_case8: forall n1, eval_static_operation_cases (Oneg) (I n1 :: nil) - | eval_static_operation_case9: forall n1 n2, eval_static_operation_cases (Osub) (I n1 :: I n2 :: nil) - | eval_static_operation_case10: forall s1 n1 n2, eval_static_operation_cases (Osub) (G s1 n1 :: I n2 :: nil) - | eval_static_operation_case11: forall n1 n2, eval_static_operation_cases (Omul) (I n1 :: I n2 :: nil) - | eval_static_operation_case12: forall n n1, eval_static_operation_cases (Omulimm n) (I n1 :: nil) - | eval_static_operation_case13: forall n1 n2, eval_static_operation_cases (Odiv) (I n1 :: I n2 :: nil) - | eval_static_operation_case14: forall n1 n2, eval_static_operation_cases (Odivu) (I n1 :: I n2 :: nil) - | eval_static_operation_case15: forall n1 n2, eval_static_operation_cases (Omod) (I n1 :: I n2 :: nil) - | eval_static_operation_case16: forall n1 n2, eval_static_operation_cases (Omodu) (I n1 :: I n2 :: nil) - | eval_static_operation_case17: forall n1 n2, eval_static_operation_cases (Oand) (I n1 :: I n2 :: nil) - | eval_static_operation_case18: forall n n1, eval_static_operation_cases (Oandimm n) (I n1 :: nil) - | eval_static_operation_case19: forall n1 n2, eval_static_operation_cases (Oor) (I n1 :: I n2 :: nil) - | eval_static_operation_case20: forall n n1, eval_static_operation_cases (Oorimm n) (I n1 :: nil) - | eval_static_operation_case21: forall n1 n2, eval_static_operation_cases (Oxor) (I n1 :: I n2 :: nil) - | eval_static_operation_case22: forall n n1, eval_static_operation_cases (Oxorimm n) (I n1 :: nil) - | eval_static_operation_case23: forall n1 n2, eval_static_operation_cases (Oshl) (I n1 :: I n2 :: nil) - | eval_static_operation_case24: forall n n1, eval_static_operation_cases (Oshlimm n) (I n1 :: nil) - | eval_static_operation_case25: forall n1 n2, eval_static_operation_cases (Oshr) (I n1 :: I n2 :: nil) - | eval_static_operation_case26: forall n n1, eval_static_operation_cases (Oshrimm n) (I n1 :: nil) - | eval_static_operation_case27: forall n n1, eval_static_operation_cases (Oshrximm n) (I n1 :: nil) - | eval_static_operation_case28: forall n1 n2, eval_static_operation_cases (Oshru) (I n1 :: I n2 :: nil) - | eval_static_operation_case29: forall n n1, eval_static_operation_cases (Oshruimm n) (I n1 :: nil) - | eval_static_operation_case30: forall n n1, eval_static_operation_cases (Ororimm n) (I n1 :: nil) - | eval_static_operation_case31: forall mode vl, eval_static_operation_cases (Olea mode) (vl) - | eval_static_operation_case32: forall n1, eval_static_operation_cases (Onegf) (F n1 :: nil) - | eval_static_operation_case33: forall n1, eval_static_operation_cases (Oabsf) (F n1 :: nil) - | eval_static_operation_case34: forall n1 n2, eval_static_operation_cases (Oaddf) (F n1 :: F n2 :: nil) - | eval_static_operation_case35: forall n1 n2, eval_static_operation_cases (Osubf) (F n1 :: F n2 :: nil) - | eval_static_operation_case36: forall n1 n2, eval_static_operation_cases (Omulf) (F n1 :: F n2 :: nil) - | eval_static_operation_case37: forall n1 n2, eval_static_operation_cases (Odivf) (F n1 :: F n2 :: nil) - | eval_static_operation_case38: forall n1, eval_static_operation_cases (Osingleoffloat) (F n1 :: nil) - | eval_static_operation_case39: forall n1, eval_static_operation_cases (Ointoffloat) (F n1 :: nil) - | eval_static_operation_case40: forall n1, eval_static_operation_cases (Ofloatofint) (I n1 :: nil) - | eval_static_operation_case41: forall c vl, eval_static_operation_cases (Ocmp c) (vl) - | eval_static_operation_default: forall (op: operation) (vl: list approx), eval_static_operation_cases op vl. - -Definition eval_static_operation_match (op: operation) (vl: list approx) := - match op as zz1, vl as zz2 return eval_static_operation_cases zz1 zz2 with - | Omove, v1::nil => eval_static_operation_case1 v1 - | Ointconst n, nil => eval_static_operation_case2 n - | Ofloatconst n, nil => eval_static_operation_case3 n - | Ocast8signed, I n1 :: nil => eval_static_operation_case4 n1 - | Ocast8unsigned, I n1 :: nil => eval_static_operation_case5 n1 - | Ocast16signed, I n1 :: nil => eval_static_operation_case6 n1 - | Ocast16unsigned, I n1 :: nil => eval_static_operation_case7 n1 - | Oneg, I n1 :: nil => eval_static_operation_case8 n1 - | Osub, I n1 :: I n2 :: nil => eval_static_operation_case9 n1 n2 - | Osub, G s1 n1 :: I n2 :: nil => eval_static_operation_case10 s1 n1 n2 - | Omul, I n1 :: I n2 :: nil => eval_static_operation_case11 n1 n2 - | Omulimm n, I n1 :: nil => eval_static_operation_case12 n n1 - | Odiv, I n1 :: I n2 :: nil => eval_static_operation_case13 n1 n2 - | Odivu, I n1 :: I n2 :: nil => eval_static_operation_case14 n1 n2 - | Omod, I n1 :: I n2 :: nil => eval_static_operation_case15 n1 n2 - | Omodu, I n1 :: I n2 :: nil => eval_static_operation_case16 n1 n2 - | Oand, I n1 :: I n2 :: nil => eval_static_operation_case17 n1 n2 - | Oandimm n, I n1 :: nil => eval_static_operation_case18 n n1 - | Oor, I n1 :: I n2 :: nil => eval_static_operation_case19 n1 n2 - | Oorimm n, I n1 :: nil => eval_static_operation_case20 n n1 - | Oxor, I n1 :: I n2 :: nil => eval_static_operation_case21 n1 n2 - | Oxorimm n, I n1 :: nil => eval_static_operation_case22 n n1 - | Oshl, I n1 :: I n2 :: nil => eval_static_operation_case23 n1 n2 - | Oshlimm n, I n1 :: nil => eval_static_operation_case24 n n1 - | Oshr, I n1 :: I n2 :: nil => eval_static_operation_case25 n1 n2 - | Oshrimm n, I n1 :: nil => eval_static_operation_case26 n n1 - | Oshrximm n, I n1 :: nil => eval_static_operation_case27 n n1 - | Oshru, I n1 :: I n2 :: nil => eval_static_operation_case28 n1 n2 - | Oshruimm n, I n1 :: nil => eval_static_operation_case29 n n1 - | Ororimm n, I n1 :: nil => eval_static_operation_case30 n n1 - | Olea mode, vl => eval_static_operation_case31 mode vl - | Onegf, F n1 :: nil => eval_static_operation_case32 n1 - | Oabsf, F n1 :: nil => eval_static_operation_case33 n1 - | Oaddf, F n1 :: F n2 :: nil => eval_static_operation_case34 n1 n2 - | Osubf, F n1 :: F n2 :: nil => eval_static_operation_case35 n1 n2 - | Omulf, F n1 :: F n2 :: nil => eval_static_operation_case36 n1 n2 - | Odivf, F n1 :: F n2 :: nil => eval_static_operation_case37 n1 n2 - | Osingleoffloat, F n1 :: nil => eval_static_operation_case38 n1 - | Ointoffloat, F n1 :: nil => eval_static_operation_case39 n1 - | Ofloatofint, I n1 :: nil => eval_static_operation_case40 n1 - | Ocmp c, vl => eval_static_operation_case41 c vl - | op, vl => eval_static_operation_default op vl - end. - -Definition eval_static_operation (op: operation) (vl: list approx) := - match eval_static_operation_match op vl with - | eval_static_operation_case1 v1 => (* Omove, v1::nil *) - v1 - | eval_static_operation_case2 n => (* Ointconst n, nil *) - I n - | eval_static_operation_case3 n => (* Ofloatconst n, nil *) - F n - | eval_static_operation_case4 n1 => (* Ocast8signed, I n1 :: nil *) - I(Int.sign_ext 8 n1) - | eval_static_operation_case5 n1 => (* Ocast8unsigned, I n1 :: nil *) - I(Int.zero_ext 8 n1) - | eval_static_operation_case6 n1 => (* Ocast16signed, I n1 :: nil *) - I(Int.sign_ext 16 n1) - | eval_static_operation_case7 n1 => (* Ocast16unsigned, I n1 :: nil *) - I(Int.zero_ext 16 n1) - | eval_static_operation_case8 n1 => (* Oneg, I n1 :: nil *) - I(Int.neg n1) - | eval_static_operation_case9 n1 n2 => (* Osub, I n1 :: I n2 :: nil *) - I(Int.sub n1 n2) - | eval_static_operation_case10 s1 n1 n2 => (* Osub, G s1 n1 :: I n2 :: nil *) - G s1 (Int.sub n1 n2) - | eval_static_operation_case11 n1 n2 => (* Omul, I n1 :: I n2 :: nil *) - I(Int.mul n1 n2) - | eval_static_operation_case12 n n1 => (* Omulimm n, I n1 :: nil *) - I(Int.mul n1 n) - | eval_static_operation_case13 n1 n2 => (* Odiv, I n1 :: I n2 :: nil *) - if Int.eq n2 Int.zero then Unknown else I(Int.divs n1 n2) - | eval_static_operation_case14 n1 n2 => (* Odivu, I n1 :: I n2 :: nil *) - if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2) - | eval_static_operation_case15 n1 n2 => (* Omod, I n1 :: I n2 :: nil *) - if Int.eq n2 Int.zero then Unknown else I(Int.mods n1 n2) - | eval_static_operation_case16 n1 n2 => (* Omodu, I n1 :: I n2 :: nil *) - if Int.eq n2 Int.zero then Unknown else I(Int.modu n1 n2) - | eval_static_operation_case17 n1 n2 => (* Oand, I n1 :: I n2 :: nil *) - I(Int.and n1 n2) - | eval_static_operation_case18 n n1 => (* Oandimm n, I n1 :: nil *) - I(Int.and n1 n) - | eval_static_operation_case19 n1 n2 => (* Oor, I n1 :: I n2 :: nil *) - I(Int.or n1 n2) - | eval_static_operation_case20 n n1 => (* Oorimm n, I n1 :: nil *) - I(Int.or n1 n) - | eval_static_operation_case21 n1 n2 => (* Oxor, I n1 :: I n2 :: nil *) - I(Int.xor n1 n2) - | eval_static_operation_case22 n n1 => (* Oxorimm n, I n1 :: nil *) - I(Int.xor n1 n) - | eval_static_operation_case23 n1 n2 => (* Oshl, I n1 :: I n2 :: nil *) - if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown - | eval_static_operation_case24 n n1 => (* Oshlimm n, I n1 :: nil *) - if Int.ltu n Int.iwordsize then I(Int.shl n1 n) else Unknown - | eval_static_operation_case25 n1 n2 => (* Oshr, I n1 :: I n2 :: nil *) - if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown - | eval_static_operation_case26 n n1 => (* Oshrimm n, I n1 :: nil *) - if Int.ltu n Int.iwordsize then I(Int.shr n1 n) else Unknown - | eval_static_operation_case27 n n1 => (* Oshrximm n, I n1 :: nil *) - if Int.ltu n (Int.repr 31) then I(Int.shrx n1 n) else Unknown - | eval_static_operation_case28 n1 n2 => (* Oshru, I n1 :: I n2 :: nil *) - if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown - | eval_static_operation_case29 n n1 => (* Oshruimm n, I n1 :: nil *) - if Int.ltu n Int.iwordsize then I(Int.shru n1 n) else Unknown - | eval_static_operation_case30 n n1 => (* Ororimm n, I n1 :: nil *) - if Int.ltu n Int.iwordsize then I(Int.ror n1 n) else Unknown - | eval_static_operation_case31 mode vl => (* Olea mode, vl *) - eval_static_addressing mode vl - | eval_static_operation_case32 n1 => (* Onegf, F n1 :: nil *) - F(Float.neg n1) - | eval_static_operation_case33 n1 => (* Oabsf, F n1 :: nil *) - F(Float.abs n1) - | eval_static_operation_case34 n1 n2 => (* Oaddf, F n1 :: F n2 :: nil *) - F(Float.add n1 n2) - | eval_static_operation_case35 n1 n2 => (* Osubf, F n1 :: F n2 :: nil *) - F(Float.sub n1 n2) - | eval_static_operation_case36 n1 n2 => (* Omulf, F n1 :: F n2 :: nil *) - F(Float.mul n1 n2) - | eval_static_operation_case37 n1 n2 => (* Odivf, F n1 :: F n2 :: nil *) - F(Float.div n1 n2) - | eval_static_operation_case38 n1 => (* Osingleoffloat, F n1 :: nil *) - F(Float.singleoffloat n1) - | eval_static_operation_case39 n1 => (* Ointoffloat, F n1 :: nil *) - eval_static_intoffloat n1 - | eval_static_operation_case40 n1 => (* Ofloatofint, I n1 :: nil *) - F(Float.floatofint n1) - | eval_static_operation_case41 c vl => (* Ocmp c, vl *) - eval_static_condition_val c vl - | eval_static_operation_default op vl => - 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. - -Variable app: reg -> approx. - -(** Original definition: -<< -Nondetfunction cond_strength_reduction - (cond: condition) (args: list reg) (vl: list approx) := - match cond, args, vl with - | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => - (Ccompimm (swap_comparison c) n1, r2 :: nil) - | Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Ccompimm c n2, r1 :: nil) - | Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil => - (Ccompuimm (swap_comparison c) n1, r2 :: nil) - | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Ccompuimm c n2, r1 :: nil) - | _, _, _ => - (cond, args) - end. ->> -*) - -Inductive cond_strength_reduction_cases: forall (cond: condition) (args: list reg) (vl: list approx), Type := - | cond_strength_reduction_case1: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | cond_strength_reduction_case2: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | cond_strength_reduction_case3: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccompu c) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | cond_strength_reduction_case4: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccompu c) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | cond_strength_reduction_default: forall (cond: condition) (args: list reg) (vl: list approx), cond_strength_reduction_cases cond args vl. - -Definition cond_strength_reduction_match (cond: condition) (args: list reg) (vl: list approx) := - match cond as zz1, args as zz2, vl as zz3 return cond_strength_reduction_cases zz1 zz2 zz3 with - | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => cond_strength_reduction_case1 c r1 r2 n1 v2 - | Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case2 c r1 r2 v1 n2 - | Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil => cond_strength_reduction_case3 c r1 r2 n1 v2 - | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case4 c r1 r2 v1 n2 - | cond, args, vl => cond_strength_reduction_default cond args vl - end. - -Definition cond_strength_reduction (cond: condition) (args: list reg) (vl: list approx) := - match cond_strength_reduction_match cond args vl with - | cond_strength_reduction_case1 c r1 r2 n1 v2 => (* Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - (Ccompimm (swap_comparison c) n1, r2 :: nil) - | cond_strength_reduction_case2 c r1 r2 v1 n2 => (* Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Ccompimm c n2, r1 :: nil) - | cond_strength_reduction_case3 c r1 r2 n1 v2 => (* Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - (Ccompuimm (swap_comparison c) n1, r2 :: nil) - | cond_strength_reduction_case4 c r1 r2 v1 n2 => (* Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Ccompuimm c n2, r1 :: nil) - | cond_strength_reduction_default cond args vl => - (cond, args) - end. - - -(** Original definition: -<< -Nondetfunction addr_strength_reduction - (addr: addressing) (args: list reg) (vl: list approx) := - match addr, args, vl with - - | Aindexed ofs, r1 :: nil, G symb n :: nil => - (Aglobal symb (Int.add n ofs), nil) - | Aindexed ofs, r1 :: nil, S n :: nil => - (Ainstack (Int.add n ofs), nil) - - | Aindexed2 ofs, r1 :: r2 :: nil, G symb n1 :: I n2 :: nil => - (Aglobal symb (Int.add (Int.add n1 n2) ofs), nil) - | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: G symb n2 :: nil => - (Aglobal symb (Int.add (Int.add n1 n2) ofs), nil) - | Aindexed2 ofs, r1 :: r2 :: nil, S n1 :: I n2 :: nil => - (Ainstack (Int.add (Int.add n1 n2) ofs), nil) - | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: S n2 :: nil => - (Ainstack (Int.add (Int.add n1 n2) ofs), nil) - | Aindexed2 ofs, r1 :: r2 :: nil, G symb n1 :: v2 :: nil => - (Abased symb (Int.add n1 ofs), r2 :: nil) - | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: G symb n2 :: nil => - (Abased symb (Int.add n2 ofs), r1 :: nil) - | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: v2 :: nil => - (Aindexed (Int.add n1 ofs), r2 :: nil) - | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Aindexed (Int.add n2 ofs), r1 :: nil) - - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, G symb n1 :: I n2 :: nil => - (Aglobal symb (Int.add (Int.add n1 (Int.mul n2 sc)) ofs), nil) - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, G symb n1 :: v2 :: nil => - (Abasedscaled sc symb (Int.add n1 ofs), r2 :: nil) - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil => - (Aindexed (Int.add (Int.mul n2 sc) ofs), r1 :: nil) - - | Abased id ofs, r1 :: nil, I n1 :: nil => - (Aglobal id (Int.add ofs n1), nil) - - | Abasedscaled sc id ofs, r1 :: nil, I n1 :: nil => - (Aglobal id (Int.add ofs (Int.mul sc n1)), nil) - - | _, _ => - (addr, args) - end. ->> -*) - -Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg) (vl: list approx), Type := - | addr_strength_reduction_case1: forall ofs r1 symb n, addr_strength_reduction_cases (Aindexed ofs) (r1 :: nil) (G symb n :: nil) - | addr_strength_reduction_case2: forall ofs r1 n, addr_strength_reduction_cases (Aindexed ofs) (r1 :: nil) (S n :: nil) - | addr_strength_reduction_case3: forall ofs r1 r2 symb n1 n2, addr_strength_reduction_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (G symb n1 :: I n2 :: nil) - | addr_strength_reduction_case4: forall ofs r1 r2 n1 symb n2, addr_strength_reduction_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (I n1 :: G symb n2 :: nil) - | addr_strength_reduction_case5: forall ofs r1 r2 n1 n2, addr_strength_reduction_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (S n1 :: I n2 :: nil) - | addr_strength_reduction_case6: forall ofs r1 r2 n1 n2, addr_strength_reduction_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (I n1 :: S n2 :: nil) - | addr_strength_reduction_case7: forall ofs r1 r2 symb n1 v2, addr_strength_reduction_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (G symb n1 :: v2 :: nil) - | addr_strength_reduction_case8: forall ofs r1 r2 v1 symb n2, addr_strength_reduction_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (v1 :: G symb n2 :: nil) - | addr_strength_reduction_case9: forall ofs r1 r2 n1 v2, addr_strength_reduction_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (I n1 :: v2 :: nil) - | addr_strength_reduction_case10: forall ofs r1 r2 v1 n2, addr_strength_reduction_cases (Aindexed2 ofs) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | addr_strength_reduction_case11: forall sc ofs r1 r2 symb n1 n2, addr_strength_reduction_cases (Aindexed2scaled sc ofs) (r1 :: r2 :: nil) (G symb n1 :: I n2 :: nil) - | addr_strength_reduction_case12: forall sc ofs r1 r2 symb n1 v2, addr_strength_reduction_cases (Aindexed2scaled sc ofs) (r1 :: r2 :: nil) (G symb n1 :: v2 :: nil) - | addr_strength_reduction_case13: forall sc ofs r1 r2 v1 n2, addr_strength_reduction_cases (Aindexed2scaled sc ofs) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | addr_strength_reduction_case14: forall id ofs r1 n1, addr_strength_reduction_cases (Abased id ofs) (r1 :: nil) (I n1 :: nil) - | addr_strength_reduction_case15: forall sc id ofs r1 n1, addr_strength_reduction_cases (Abasedscaled sc id ofs) (r1 :: nil) (I n1 :: nil) - | addr_strength_reduction_default: forall (addr: addressing) (args: list reg) (vl: list approx), addr_strength_reduction_cases addr args vl. - -Definition addr_strength_reduction_match (addr: addressing) (args: list reg) (vl: list approx) := - match addr as zz1, args as zz2, vl as zz3 return addr_strength_reduction_cases zz1 zz2 zz3 with - | Aindexed ofs, r1 :: nil, G symb n :: nil => addr_strength_reduction_case1 ofs r1 symb n - | Aindexed ofs, r1 :: nil, S n :: nil => addr_strength_reduction_case2 ofs r1 n - | Aindexed2 ofs, r1 :: r2 :: nil, G symb n1 :: I n2 :: nil => addr_strength_reduction_case3 ofs r1 r2 symb n1 n2 - | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: G symb n2 :: nil => addr_strength_reduction_case4 ofs r1 r2 n1 symb n2 - | Aindexed2 ofs, r1 :: r2 :: nil, S n1 :: I n2 :: nil => addr_strength_reduction_case5 ofs r1 r2 n1 n2 - | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: S n2 :: nil => addr_strength_reduction_case6 ofs r1 r2 n1 n2 - | Aindexed2 ofs, r1 :: r2 :: nil, G symb n1 :: v2 :: nil => addr_strength_reduction_case7 ofs r1 r2 symb n1 v2 - | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: G symb n2 :: nil => addr_strength_reduction_case8 ofs r1 r2 v1 symb n2 - | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: v2 :: nil => addr_strength_reduction_case9 ofs r1 r2 n1 v2 - | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil => addr_strength_reduction_case10 ofs r1 r2 v1 n2 - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, G symb n1 :: I n2 :: nil => addr_strength_reduction_case11 sc ofs r1 r2 symb n1 n2 - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, G symb n1 :: v2 :: nil => addr_strength_reduction_case12 sc ofs r1 r2 symb n1 v2 - | Aindexed2scaled sc ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil => addr_strength_reduction_case13 sc ofs r1 r2 v1 n2 - | Abased id ofs, r1 :: nil, I n1 :: nil => addr_strength_reduction_case14 id ofs r1 n1 - | Abasedscaled sc id ofs, r1 :: nil, I n1 :: nil => addr_strength_reduction_case15 sc id ofs r1 n1 - | addr, args, vl => addr_strength_reduction_default addr args vl - end. - -Definition addr_strength_reduction (addr: addressing) (args: list reg) (vl: list approx) := - match addr_strength_reduction_match addr args vl with - | addr_strength_reduction_case1 ofs r1 symb n => (* Aindexed ofs, r1 :: nil, G symb n :: nil *) - (Aglobal symb (Int.add n ofs), nil) - | addr_strength_reduction_case2 ofs r1 n => (* Aindexed ofs, r1 :: nil, S n :: nil *) - (Ainstack (Int.add n ofs), nil) - | addr_strength_reduction_case3 ofs r1 r2 symb n1 n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, G symb n1 :: I n2 :: nil *) - (Aglobal symb (Int.add (Int.add n1 n2) ofs), nil) - | addr_strength_reduction_case4 ofs r1 r2 n1 symb n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: G symb n2 :: nil *) - (Aglobal symb (Int.add (Int.add n1 n2) ofs), nil) - | addr_strength_reduction_case5 ofs r1 r2 n1 n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, S n1 :: I n2 :: nil *) - (Ainstack (Int.add (Int.add n1 n2) ofs), nil) - | addr_strength_reduction_case6 ofs r1 r2 n1 n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: S n2 :: nil *) - (Ainstack (Int.add (Int.add n1 n2) ofs), nil) - | addr_strength_reduction_case7 ofs r1 r2 symb n1 v2 => (* Aindexed2 ofs, r1 :: r2 :: nil, G symb n1 :: v2 :: nil *) - (Abased symb (Int.add n1 ofs), r2 :: nil) - | addr_strength_reduction_case8 ofs r1 r2 v1 symb n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, v1 :: G symb n2 :: nil *) - (Abased symb (Int.add n2 ofs), r1 :: nil) - | addr_strength_reduction_case9 ofs r1 r2 n1 v2 => (* Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: v2 :: nil *) - (Aindexed (Int.add n1 ofs), r2 :: nil) - | addr_strength_reduction_case10 ofs r1 r2 v1 n2 => (* Aindexed2 ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Aindexed (Int.add n2 ofs), r1 :: nil) - | addr_strength_reduction_case11 sc ofs r1 r2 symb n1 n2 => (* Aindexed2scaled sc ofs, r1 :: r2 :: nil, G symb n1 :: I n2 :: nil *) - (Aglobal symb (Int.add (Int.add n1 (Int.mul n2 sc)) ofs), nil) - | addr_strength_reduction_case12 sc ofs r1 r2 symb n1 v2 => (* Aindexed2scaled sc ofs, r1 :: r2 :: nil, G symb n1 :: v2 :: nil *) - (Abasedscaled sc symb (Int.add n1 ofs), r2 :: nil) - | addr_strength_reduction_case13 sc ofs r1 r2 v1 n2 => (* Aindexed2scaled sc ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - (Aindexed (Int.add (Int.mul n2 sc) ofs), r1 :: nil) - | addr_strength_reduction_case14 id ofs r1 n1 => (* Abased id ofs, r1 :: nil, I n1 :: nil *) - (Aglobal id (Int.add ofs n1), nil) - | addr_strength_reduction_case15 sc id ofs r1 n1 => (* Abasedscaled sc id ofs, r1 :: nil, I n1 :: nil *) - (Aglobal id (Int.add ofs (Int.mul sc n1)), nil) - | addr_strength_reduction_default addr args vl => - (addr, args) - end. - - -Definition make_addimm (n: int) (r: reg) := - if Int.eq n Int.zero - then (Omove, r :: nil) - else (Oaddimm n, r :: nil). - -Definition make_shlimm (n: int) (r: reg) := - if Int.eq n Int.zero - then (Omove, r :: nil) - else (Oshlimm n, r :: nil). - -Definition make_shrimm (n: int) (r: reg) := - if Int.eq n Int.zero - then (Omove, r :: nil) - else (Oshrimm n, r :: nil). - -Definition make_shruimm (n: int) (r: reg) := - if Int.eq n Int.zero - then (Omove, r :: nil) - else (Oshruimm n, r :: nil). - -Definition make_mulimm (n: int) (r: reg) := - if Int.eq n Int.zero then - (Ointconst Int.zero, nil) - else if Int.eq n Int.one then - (Omove, r :: nil) - else - match Int.is_power2 n with - | Some l => make_shlimm l r - | None => (Omulimm n, r :: nil) - end. - -Definition make_andimm (n: int) (r: reg) := - if Int.eq n Int.zero - then (Ointconst Int.zero, nil) - else if Int.eq n Int.mone then (Omove, r :: nil) - else (Oandimm n, r :: nil). - -Definition make_orimm (n: int) (r: reg) := - if Int.eq n Int.zero then (Omove, r :: nil) - else if Int.eq n Int.mone then (Ointconst Int.mone, nil) - else (Oorimm n, r :: nil). - -Definition make_xorimm (n: int) (r: reg) := - if Int.eq n Int.zero - then (Omove, r :: nil) - else (Oxorimm n, r :: nil). - -Definition make_divimm n (r1 r2: reg) := - match Int.is_power2 n with - | Some l => if Int.ltu l (Int.repr 31) - then (Oshrximm l, r1 :: nil) - else (Odiv, r1 :: r2 :: nil) - | None => (Odiv, r1 :: r2 :: nil) - end. - -Definition make_divuimm n (r1 r2: reg) := - match Int.is_power2 n with - | Some l => make_shruimm l r1 - | None => (Odivu, r1 :: r2 :: nil) - end. - -Definition make_moduimm n (r1 r2: reg) := - match Int.is_power2 n with - | Some l => (Oandimm (Int.sub n Int.one), r1 :: nil) - | None => (Omodu, r1 :: r2 :: nil) - end. - -(** We must be careful to preserve 2-address constraints over the - RTL code, which means that commutative operations cannot - be specialized if their first argument is a constant. *) - -(** Original definition: -<< -Nondetfunction op_strength_reduction - (op: operation) (args: list reg) (vl: list approx) := - match op, args, vl with - | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg n2) r1 - | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_mulimm n2 r1 - | 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 - | Omodu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_moduimm n2 r1 r2 - | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm n2 r1 - | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm n2 r1 - | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm n2 r1 - | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 - | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 - | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 - | Olea addr, args, vl => - let (addr', args') := addr_strength_reduction addr args vl in - (Olea addr', args') - | Ocmp c, args, vl => - let (c', args') := cond_strength_reduction c args vl in - (Ocmp c', args') - | _, _, _ => (op, args) - end. ->> -*) - -Inductive op_strength_reduction_cases: forall (op: operation) (args: list reg) (vl: list approx), Type := - | op_strength_reduction_case1: forall r1 r2 v1 n2, op_strength_reduction_cases (Osub) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case2: forall r1 r2 v1 n2, op_strength_reduction_cases (Omul) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case3: forall r1 r2 v1 n2, op_strength_reduction_cases (Odiv) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case4: forall r1 r2 v1 n2, op_strength_reduction_cases (Odivu) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case5: forall r1 r2 v1 n2, op_strength_reduction_cases (Omodu) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case6: forall r1 r2 v1 n2, op_strength_reduction_cases (Oand) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case7: forall r1 r2 v1 n2, op_strength_reduction_cases (Oor) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case8: forall r1 r2 v1 n2, op_strength_reduction_cases (Oxor) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case9: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshl) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case10: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshr) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case11: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshru) (r1 :: r2 :: nil) (v1 :: I n2 :: nil) - | op_strength_reduction_case12: forall addr args vl, op_strength_reduction_cases (Olea addr) (args) (vl) - | op_strength_reduction_case13: forall c args vl, op_strength_reduction_cases (Ocmp c) (args) (vl) - | op_strength_reduction_default: forall (op: operation) (args: list reg) (vl: list approx), op_strength_reduction_cases op args vl. - -Definition op_strength_reduction_match (op: operation) (args: list reg) (vl: list approx) := - match op as zz1, args as zz2, vl as zz3 return op_strength_reduction_cases zz1 zz2 zz3 with - | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case1 r1 r2 v1 n2 - | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case2 r1 r2 v1 n2 - | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case3 r1 r2 v1 n2 - | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case4 r1 r2 v1 n2 - | Omodu, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case5 r1 r2 v1 n2 - | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case6 r1 r2 v1 n2 - | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case7 r1 r2 v1 n2 - | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case8 r1 r2 v1 n2 - | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case9 r1 r2 v1 n2 - | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case10 r1 r2 v1 n2 - | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case11 r1 r2 v1 n2 - | Olea addr, args, vl => op_strength_reduction_case12 addr args vl - | Ocmp c, args, vl => op_strength_reduction_case13 c args vl - | op, args, vl => op_strength_reduction_default op args vl - end. - -Definition op_strength_reduction (op: operation) (args: list reg) (vl: list approx) := - match op_strength_reduction_match op args vl with - | op_strength_reduction_case1 r1 r2 v1 n2 => (* Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_addimm (Int.neg n2) r1 - | op_strength_reduction_case2 r1 r2 v1 n2 => (* Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_mulimm n2 r1 - | op_strength_reduction_case3 r1 r2 v1 n2 => (* Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_divimm n2 r1 r2 - | op_strength_reduction_case4 r1 r2 v1 n2 => (* Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_divuimm n2 r1 r2 - | op_strength_reduction_case5 r1 r2 v1 n2 => (* Omodu, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_moduimm n2 r1 r2 - | op_strength_reduction_case6 r1 r2 v1 n2 => (* Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_andimm n2 r1 - | op_strength_reduction_case7 r1 r2 v1 n2 => (* Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_orimm n2 r1 - | op_strength_reduction_case8 r1 r2 v1 n2 => (* Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_xorimm n2 r1 - | op_strength_reduction_case9 r1 r2 v1 n2 => (* Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shlimm n2 r1 - | op_strength_reduction_case10 r1 r2 v1 n2 => (* Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shrimm n2 r1 - | op_strength_reduction_case11 r1 r2 v1 n2 => (* Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil *) - make_shruimm n2 r1 - | op_strength_reduction_case12 addr args vl => (* Olea addr, args, vl *) - let (addr', args') := addr_strength_reduction addr args vl in (Olea addr', args') - | op_strength_reduction_case13 c args vl => (* Ocmp c, args, vl *) - let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args') - | op_strength_reduction_default op args vl => - (op, args) - end. - - -End STRENGTH_REDUCTION. diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp new file mode 100644 index 00000000..b8611075 --- /dev/null +++ b/ia32/ConstpropOp.vp @@ -0,0 +1,314 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Static analysis and strength reduction for operators + and conditions. This is the machine-dependent part of [Constprop]. *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Op. +Require Import Registers. + +(** * 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. *) + | 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. *) + +(** 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 [Vfloat f] + and [Vfloat g] respectively, and [Unknown] otherwise. + + 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. *) + +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) + | 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)) + | Cmaskzero n, I n1 :: nil => Some(Int.eq (Int.and n1 n) Int.zero) + | Cmasknotzero n, I n1::nil => Some(negb(Int.eq (Int.and n1 n) Int.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. + +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 n, I n1::I n2::nil => I (Int.add (Int.add n1 n2) n) + | Aindexed2 n, G id ofs::I n2::nil => G id (Int.add (Int.add ofs n2) n) + | Aindexed2 n, I n1::G id ofs::nil => G id (Int.add (Int.add ofs n1) n) + | Aindexed2 n, S ofs::I n2::nil => S (Int.add (Int.add ofs n2) n) + | Aindexed2 n, I n1::S ofs::nil => S (Int.add (Int.add ofs n1) n) + | Ascaled sc n, I n1::nil => I (Int.add (Int.mul n1 sc) n) + | Aindexed2scaled sc n, I n1::I n2::nil => I (Int.add n1 (Int.add (Int.mul n2 sc) n)) + | Aindexed2scaled sc n, G id ofs::I n2::nil => G id (Int.add ofs (Int.add (Int.mul n2 sc) n)) + | Aindexed2scaled sc n, S ofs::I n2::nil => S (Int.add ofs (Int.add (Int.mul n2 sc) n)) + | Aglobal id ofs, nil => G id ofs + | Abased id ofs, I n1::nil => G id (Int.add ofs n1) + | Abasedscaled sc id ofs, I n1::nil => G id (Int.add ofs (Int.mul sc n1)) + | Ainstack ofs, nil => S ofs + | _, _ => Unknown + end. + +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 => F n + | Ocast8signed, I n1 :: nil => I(Int.sign_ext 8 n1) + | Ocast8unsigned, I n1 :: nil => I(Int.zero_ext 8 n1) + | Ocast16signed, I n1 :: nil => I(Int.sign_ext 16 n1) + | Ocast16unsigned, I n1 :: nil => I(Int.zero_ext 16 n1) + | Oneg, I n1 :: nil => I(Int.neg n1) + | Osub, I n1 :: I n2 :: nil => I(Int.sub n1 n2) + | Osub, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 n2) + | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2) + | Omulimm n, I n1 :: nil => I(Int.mul n1 n) + | Odiv, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero 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) + | Omod, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.mods n1 n2) + | Omodu, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.modu n1 n2) + | Oand, I n1 :: I n2 :: nil => I(Int.and n1 n2) + | Oandimm n, I n1 :: nil => I(Int.and n1 n) + | Oor, I n1 :: I n2 :: nil => I(Int.or n1 n2) + | Oorimm n, I n1 :: nil => I(Int.or n1 n) + | Oxor, I n1 :: I n2 :: nil => I(Int.xor n1 n2) + | Oxorimm n, I n1 :: nil => I(Int.xor n1 n) + | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown + | Oshlimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shl n1 n) else Unknown + | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown + | Oshrimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shr n1 n) else Unknown + | Oshrximm n, I n1 :: nil => if Int.ltu n (Int.repr 31) then I(Int.shrx n1 n) else Unknown + | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown + | Oshruimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shru n1 n) else Unknown + | Ororimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.ror n1 n) else Unknown + | Olea mode, vl => eval_static_addressing mode vl + | 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 + | Ofloatofint, I n1 :: nil => F(Float.floatofint n1) + | Ocmp c, vl => eval_static_condition_val c vl + | _, _ => 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. + +Variable app: reg -> approx. + +Nondetfunction cond_strength_reduction + (cond: condition) (args: list reg) (vl: list approx) := + match cond, args, vl with + | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => + (Ccompimm (swap_comparison c) n1, r2 :: nil) + | Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil => + (Ccompimm c n2, r1 :: nil) + | Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil => + (Ccompuimm (swap_comparison c) n1, r2 :: nil) + | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil => + (Ccompuimm c n2, r1 :: nil) + | _, _, _ => + (cond, args) + end. + +Nondetfunction addr_strength_reduction + (addr: addressing) (args: list reg) (vl: list approx) := + match addr, args, vl with + + | Aindexed ofs, r1 :: nil, G symb n :: nil => + (Aglobal symb (Int.add n ofs), nil) + | Aindexed ofs, r1 :: nil, S n :: nil => + (Ainstack (Int.add n ofs), nil) + + | Aindexed2 ofs, r1 :: r2 :: nil, G symb n1 :: I n2 :: nil => + (Aglobal symb (Int.add (Int.add n1 n2) ofs), nil) + | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: G symb n2 :: nil => + (Aglobal symb (Int.add (Int.add n1 n2) ofs), nil) + | Aindexed2 ofs, r1 :: r2 :: nil, S n1 :: I n2 :: nil => + (Ainstack (Int.add (Int.add n1 n2) ofs), nil) + | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: S n2 :: nil => + (Ainstack (Int.add (Int.add n1 n2) ofs), nil) + | Aindexed2 ofs, r1 :: r2 :: nil, G symb n1 :: v2 :: nil => + (Abased symb (Int.add n1 ofs), r2 :: nil) + | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: G symb n2 :: nil => + (Abased symb (Int.add n2 ofs), r1 :: nil) + | Aindexed2 ofs, r1 :: r2 :: nil, I n1 :: v2 :: nil => + (Aindexed (Int.add n1 ofs), r2 :: nil) + | Aindexed2 ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil => + (Aindexed (Int.add n2 ofs), r1 :: nil) + + | Aindexed2scaled sc ofs, r1 :: r2 :: nil, G symb n1 :: I n2 :: nil => + (Aglobal symb (Int.add (Int.add n1 (Int.mul n2 sc)) ofs), nil) + | Aindexed2scaled sc ofs, r1 :: r2 :: nil, G symb n1 :: v2 :: nil => + (Abasedscaled sc symb (Int.add n1 ofs), r2 :: nil) + | Aindexed2scaled sc ofs, r1 :: r2 :: nil, v1 :: I n2 :: nil => + (Aindexed (Int.add (Int.mul n2 sc) ofs), r1 :: nil) + + | Abased id ofs, r1 :: nil, I n1 :: nil => + (Aglobal id (Int.add ofs n1), nil) + + | Abasedscaled sc id ofs, r1 :: nil, I n1 :: nil => + (Aglobal id (Int.add ofs (Int.mul sc n1)), nil) + + | _, _ => + (addr, args) + end. + +Definition make_addimm (n: int) (r: reg) := + if Int.eq n Int.zero + then (Omove, r :: nil) + else (Oaddimm n, r :: nil). + +Definition make_shlimm (n: int) (r: reg) := + if Int.eq n Int.zero + then (Omove, r :: nil) + else (Oshlimm n, r :: nil). + +Definition make_shrimm (n: int) (r: reg) := + if Int.eq n Int.zero + then (Omove, r :: nil) + else (Oshrimm n, r :: nil). + +Definition make_shruimm (n: int) (r: reg) := + if Int.eq n Int.zero + then (Omove, r :: nil) + else (Oshruimm n, r :: nil). + +Definition make_mulimm (n: int) (r: reg) := + if Int.eq n Int.zero then + (Ointconst Int.zero, nil) + else if Int.eq n Int.one then + (Omove, r :: nil) + else + match Int.is_power2 n with + | Some l => make_shlimm l r + | None => (Omulimm n, r :: nil) + end. + +Definition make_andimm (n: int) (r: reg) := + if Int.eq n Int.zero + then (Ointconst Int.zero, nil) + else if Int.eq n Int.mone then (Omove, r :: nil) + else (Oandimm n, r :: nil). + +Definition make_orimm (n: int) (r: reg) := + if Int.eq n Int.zero then (Omove, r :: nil) + else if Int.eq n Int.mone then (Ointconst Int.mone, nil) + else (Oorimm n, r :: nil). + +Definition make_xorimm (n: int) (r: reg) := + if Int.eq n Int.zero + then (Omove, r :: nil) + else (Oxorimm n, r :: nil). + +Definition make_divimm n (r1 r2: reg) := + match Int.is_power2 n with + | Some l => if Int.ltu l (Int.repr 31) + then (Oshrximm l, r1 :: nil) + else (Odiv, r1 :: r2 :: nil) + | None => (Odiv, r1 :: r2 :: nil) + end. + +Definition make_divuimm n (r1 r2: reg) := + match Int.is_power2 n with + | Some l => make_shruimm l r1 + | None => (Odivu, r1 :: r2 :: nil) + end. + +Definition make_moduimm n (r1 r2: reg) := + match Int.is_power2 n with + | Some l => (Oandimm (Int.sub n Int.one), r1 :: nil) + | None => (Omodu, r1 :: r2 :: nil) + end. + +(** We must be careful to preserve 2-address constraints over the + RTL code, which means that commutative operations cannot + be specialized if their first argument is a constant. *) + +Nondetfunction op_strength_reduction + (op: operation) (args: list reg) (vl: list approx) := + match op, args, vl with + | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg n2) r1 + | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_mulimm n2 r1 + | 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 + | Omodu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_moduimm n2 r1 r2 + | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm n2 r1 + | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm n2 r1 + | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm n2 r1 + | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 + | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 + | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 + | Olea addr, args, vl => + let (addr', args') := addr_strength_reduction addr args vl in + (Olea addr', args') + | Ocmp c, args, vl => + let (c', args') := cond_strength_reduction c args vl in + (Ocmp c', args') + | _, _, _ => (op, args) + end. + +Nondetfunction builtin_strength_reduction + (ef: external_function) (args: list reg) (vl: list approx) := + match ef, args, vl with + | EF_vload chunk, r1 :: nil, G symb n1 :: nil => + (EF_vload_global chunk symb n1, nil) + | EF_vstore chunk, r1 :: r2 :: nil, G symb n1 :: v2 :: nil => + (EF_vstore_global chunk symb n1, r2 :: nil) + | _, _, _ => + (ef, args) + end. + +End STRENGTH_REDUCTION. diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v index afb284af..04a17251 100644 --- a/ia32/ConstpropOpproof.v +++ b/ia32/ConstpropOpproof.v @@ -19,6 +19,7 @@ Require Import Floats. Require Import Values. Require Import Memory. Require Import Globalenvs. +Require Import Events. Require Import Op. Require Import Registers. Require Import RTL. @@ -418,6 +419,24 @@ Proof. exists v; auto. Qed. +Lemma builtin_strength_reduction_correct: + forall ef args vl m t vres m', + vl = approx_regs app args -> + external_call ef ge rs##args m t vres m' -> + let (ef', args') := builtin_strength_reduction ef args vl in + external_call ef' ge rs##args' m t vres m'. +Proof. + intros until m'. unfold builtin_strength_reduction. + destruct (builtin_strength_reduction_match ef args vl); simpl; intros; InvApproxRegs; SimplVMA. + unfold symbol_address in H. destruct (Genv.find_symbol ge symb) as [b|]_eqn; rewrite H in H0. + rewrite volatile_load_global_charact. exists b; auto. + inv H0. + unfold symbol_address in H1. destruct (Genv.find_symbol ge symb) as [b|]_eqn; rewrite H1 in H0. + rewrite volatile_store_global_charact. exists b; auto. + inv H0. + auto. +Qed. + End STRENGTH_REDUCTION. End ANALYSIS. diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 5ca56d72..3ee0c6eb 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -348,52 +348,85 @@ let print_builtin_memcpy oc sz al args = (* Handling of volatile reads and writes *) +let print_builtin_vload_common oc chunk addr res = + match chunk, res with + | Mint8unsigned, IR res -> + fprintf oc " movzbl %a, %a\n" addressing addr ireg res + | Mint8signed, IR res -> + fprintf oc " movsbl %a, %a\n" addressing addr ireg res + | Mint16unsigned, IR res -> + fprintf oc " movzwl %a, %a\n" addressing addr ireg res + | Mint16signed, IR res -> + fprintf oc " movswl %a, %a\n" addressing addr ireg res + | Mint32, IR res -> + fprintf oc " movl %a, %a\n" addressing addr ireg res + | Mfloat32, FR res -> + fprintf oc " cvtss2sd %a, %a\n" addressing addr freg res + | Mfloat64, FR res -> + fprintf oc " movsd %a, %a\n" addressing addr freg res + | _ -> + assert false + let print_builtin_vload oc chunk args res = fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; - begin match chunk, args, res with - | Mint8unsigned, [IR addr], IR res -> - fprintf oc " movzbl 0(%a), %a\n" ireg addr ireg res - | Mint8signed, [IR addr], IR res -> - fprintf oc " movsbl 0(%a), %a\n" ireg addr ireg res - | Mint16unsigned, [IR addr], IR res -> - fprintf oc " movzwl 0(%a), %a\n" ireg addr ireg res - | Mint16signed, [IR addr], IR res -> - fprintf oc " movswl 0(%a), %a\n" ireg addr ireg res - | Mint32, [IR addr], IR res -> - fprintf oc " movl 0(%a), %a\n" ireg addr ireg res - | Mfloat32, [IR addr], FR res -> - fprintf oc " cvtss2sd 0(%a), %a\n" ireg addr freg res - | Mfloat64, [IR addr], FR res -> - fprintf oc " movsd 0(%a), %a\n" ireg addr freg res + begin match args with + | [IR addr] -> + print_builtin_vload_common oc chunk + (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) res | _ -> assert false end; fprintf oc "%s end builtin __builtin_volatile_read\n" comment -let print_builtin_vstore oc chunk args = - fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; - begin match chunk, args with - | (Mint8signed | Mint8unsigned), [IR addr; IR src] -> +let print_builtin_vload_global oc chunk id ofs args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + print_builtin_vload_common oc chunk + (Addrmode(None, None, Coq_inr(id,ofs))) res; + fprintf oc "%s end builtin __builtin_volatile_read\n" comment + +let print_builtin_vstore_common oc chunk addr src = + match chunk, src with + | (Mint8signed | Mint8unsigned), IR src -> if Asmgen.low_ireg src then - fprintf oc " movb %a, 0(%a)\n" ireg8 src ireg addr + fprintf oc " movb %a, %a\n" ireg8 src addressing addr else begin fprintf oc " movl %a, %%ecx\n" ireg src; - fprintf oc " movb %%cl, 0(%a)\n" ireg addr + fprintf oc " movb %%cl, %a\n" addressing addr end - | (Mint16signed | Mint16unsigned), [IR addr; IR src] -> + | (Mint16signed | Mint16unsigned), IR src -> if Asmgen.low_ireg src then - fprintf oc " movw %a, 0(%a)\n" ireg16 src ireg addr + fprintf oc " movw %a, %a\n" ireg16 src addressing addr else begin fprintf oc " movl %a, %%ecx\n" ireg src; - fprintf oc " movw %%cx, 0(%a)\n" ireg addr + fprintf oc " movw %%cx, %a\n" addressing addr end - | Mint32, [IR addr; IR src] -> - fprintf oc " movl %a, 0(%a)\n" ireg src ireg addr - | Mfloat32, [IR addr; FR src] -> + | Mint32, IR src -> + fprintf oc " movl %a, %a\n" ireg src addressing addr + | Mfloat32, FR src -> fprintf oc " cvtsd2ss %a, %%xmm7\n" freg src; - fprintf oc " movss %%xmm7, 0(%a)\n" ireg addr - | Mfloat64, [IR addr; FR src] -> - fprintf oc " movsd %a, 0(%a)\n" freg src ireg addr + fprintf oc " movss %%xmm7, %a\n" addressing addr + | Mfloat64, FR src -> + fprintf oc " movsd %a, %a\n" freg src addressing addr + | _ -> + assert false + +let print_builtin_vstore oc chunk args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + begin match args with + | [IR addr; src] -> + print_builtin_vstore_common oc chunk + (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src + | _ -> + assert false + end; + fprintf oc "%s end builtin __builtin_volatile_write\n" comment + +let print_builtin_vstore_global oc chunk id ofs args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + begin match args with + | [src] -> + print_builtin_vstore_common oc chunk + (Addrmode(None, None, Coq_inr(id,ofs))) src | _ -> assert false end; @@ -677,6 +710,10 @@ let print_instruction oc = function print_builtin_vload oc chunk args res | EF_vstore chunk -> print_builtin_vstore oc chunk args + | EF_vload_global(chunk, id, ofs) -> + print_builtin_vload_global oc chunk id ofs args res + | EF_vstore_global(chunk, id, ofs) -> + print_builtin_vstore_global oc chunk id ofs args | EF_memcpy(sz, al) -> print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz)) (Int32.to_int (camlint_of_coqint al)) args diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 22e89e31..cb958d44 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -274,4 +274,15 @@ Nondetfunction addr_strength_reduction (addr, args) end. +Nondetfunction builtin_strength_reduction + (ef: external_function) (args: list reg) (vl: list approx) := + match ef, args, vl with + | EF_vload chunk, r1 :: nil, G symb n1 :: nil => + (EF_vload_global chunk symb n1, nil) + | EF_vstore chunk, r1 :: r2 :: nil, G symb n1 :: v2 :: nil => + (EF_vstore_global chunk symb n1, r2 :: nil) + | _, _, _ => + (ef, args) + end. + End STRENGTH_REDUCTION. diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 36444b3e..3b5021e2 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -19,6 +19,7 @@ Require Import Floats. Require Import Values. Require Import Memory. Require Import Globalenvs. +Require Import Events. Require Import Op. Require Import Registers. Require Import RTL. @@ -404,6 +405,24 @@ Proof. auto. Qed. +Lemma builtin_strength_reduction_correct: + forall ef args vl m t vres m', + vl = approx_regs app args -> + external_call ef ge rs##args m t vres m' -> + let (ef', args') := builtin_strength_reduction ef args vl in + external_call ef' ge rs##args' m t vres m'. +Proof. + intros until m'. unfold builtin_strength_reduction. + destruct (builtin_strength_reduction_match ef args vl); simpl; intros; InvApproxRegs; SimplVMA. + unfold symbol_address in H. destruct (Genv.find_symbol ge symb) as [b|]_eqn; rewrite H in H0. + rewrite volatile_load_global_charact. exists b; auto. + inv H0. + unfold symbol_address in H1. destruct (Genv.find_symbol ge symb) as [b|]_eqn; rewrite H1 in H0. + rewrite volatile_store_global_charact. exists b; auto. + inv H0. + auto. +Qed. + End STRENGTH_REDUCTION. End ANALYSIS. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 91dd686a..d79735a6 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -375,43 +375,77 @@ let print_builtin_memcpy oc sz al args = (* Handling of volatile reads and writes *) +let print_builtin_vload_shared oc chunk base offset res = + match chunk, res with + | Mint8unsigned, IR res -> + fprintf oc " lbz %a, %a(%a)\n" ireg res constant offset ireg base + | Mint8signed, IR res -> + fprintf oc " lbz %a, %a(%a)\n" ireg res constant offset ireg base; + fprintf oc " extsb %a, %a\n" ireg res ireg res + | Mint16unsigned, IR res -> + fprintf oc " lhz %a, %a(%a)\n" ireg res constant offset ireg base + | Mint16signed, IR res -> + fprintf oc " lha %a, %a(%a)\n" ireg res constant offset ireg base + | Mint32, IR res -> + fprintf oc " lwz %a, %a(%a)\n" ireg res constant offset ireg base + | Mfloat32, FR res -> + fprintf oc " lfs %a, %a(%a)\n" freg res constant offset ireg base + | Mfloat64, FR res -> + fprintf oc " lfs %a, %a(%a)\n" freg res constant offset ireg base + | _ -> + assert false + let print_builtin_vload oc chunk args res = fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; - begin match chunk, args, res with - | Mint8unsigned, [IR addr], IR res -> - fprintf oc " lbz %a, 0(%a)\n" ireg res ireg addr - | Mint8signed, [IR addr], IR res -> - fprintf oc " lbz %a, 0(%a)\n" ireg res ireg addr; - fprintf oc " extsb %a, %a\n" ireg res ireg res - | Mint16unsigned, [IR addr], IR res -> - fprintf oc " lhz %a, 0(%a)\n" ireg res ireg addr - | Mint16signed, [IR addr], IR res -> - fprintf oc " lha %a, 0(%a)\n" ireg res ireg addr - | Mint32, [IR addr], IR res -> - fprintf oc " lwz %a, 0(%a)\n" ireg res ireg addr - | Mfloat32, [IR addr], FR res -> - fprintf oc " lfs %a, 0(%a)\n" freg res ireg addr - | Mfloat64, [IR addr], FR res -> - fprintf oc " lfd %a, 0(%a)\n" freg res ireg addr + begin match args with + | [IR addr] -> + print_builtin_vload_shared oc chunk addr (Cint Integers.Int.zero) res | _ -> assert false end; fprintf oc "%s end builtin __builtin_volatile_read\n" comment +let print_builtin_vload_global oc chunk id ofs args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + fprintf oc " addis %a, %a, %a\n" + ireg GPR11 ireg_or_zero GPR0 constant (Csymbol_high(id, ofs)); + print_builtin_vload_shared oc chunk GPR11 (Csymbol_low(id, ofs)) res; + fprintf oc "%s end builtin __builtin_volatile_read\n" comment + +let print_builtin_vstore_shared oc chunk base offset src = + match chunk, src with + | (Mint8signed | Mint8unsigned), IR src -> + fprintf oc " stb %a, %a(%a)\n" ireg src ireg base constant offset + | (Mint16signed | Mint16unsigned), IR src -> + fprintf oc " sth %a, %a(%a)\n" ireg src ireg base constant offset + | Mint32, IR src -> + fprintf oc " stw %a, %a(%a)\n" ireg src ireg base constant offset + | Mfloat32, FR src -> + fprintf oc " frsp %a, %a\n" freg FPR13 freg src; + fprintf oc " stfs %a, %a(%a)\n" freg FPR13 ireg base constant offset + | Mfloat64, FR src -> + fprintf oc " stfd %a, %a(%a)\n" freg src ireg base constant offset + | _ -> + assert false + let print_builtin_vstore oc chunk args = fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; - begin match chunk, args with - | (Mint8signed | Mint8unsigned), [IR addr; IR src] -> - fprintf oc " stb %a, 0(%a)\n" ireg src ireg addr - | (Mint16signed | Mint16unsigned), [IR addr; IR src] -> - fprintf oc " sth %a, 0(%a)\n" ireg src ireg addr - | Mint32, [IR addr; IR src] -> - fprintf oc " stw %a, 0(%a)\n" ireg src ireg addr - | Mfloat32, [IR addr; FR src] -> - fprintf oc " frsp %a, %a\n" freg FPR13 freg src; - fprintf oc " stfs %a, 0(%a)\n" freg FPR13 ireg addr - | Mfloat64, [IR addr; FR src] -> - fprintf oc " stfd %a, 0(%a)\n" freg src ireg addr + begin match args with + | [IR addr; src] -> + print_builtin_vstore_shared oc chunk addr (Cint Integers.Int.zero) src + | _ -> + assert false + end; + fprintf oc "%s end builtin __builtin_volatile_write\n" comment + +let print_builtin_vstore_global oc chunk id ofs args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + begin match args with + | [src] -> + let tmp = if src = IR GPR11 then GPR12 else GPR11 in + fprintf oc " addis %a, %a, %a\n" + ireg tmp ireg_or_zero GPR0 constant (Csymbol_high(id, ofs)); + print_builtin_vstore_shared oc chunk tmp (Csymbol_low(id, ofs)) src | _ -> assert false end; @@ -717,6 +751,10 @@ let print_instruction oc = function print_builtin_vload oc chunk args res | EF_vstore chunk -> print_builtin_vstore oc chunk args + | EF_vload_global(chunk, id, ofs) -> + print_builtin_vload_global oc chunk id ofs args res + | EF_vstore_global(chunk, id, ofs) -> + print_builtin_vstore_global oc chunk id ofs args | EF_memcpy(sz, al) -> print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz)) (Int32.to_int (camlint_of_coqint al)) args -- cgit