Strength reduction for operators and conditions. This is the machine-dependent part of Constprop.

Require Archi.
Require Import Coqlib Compopts.
Require Import AST Integers Floats Values.
Require Import Op Registers.
Require Import ZIntervalDomain.

Converting known values to constants

Definition const_for_result (a: ival) : option operation :=
  match option_val_of_ival a with
  | Some (Vint n) => Some(Ointconst n)
  | Some (Vlong n) => if Archi.ptr64 then Some(Olongconst n) else None
  | _ => None
  end.

Original definition:

Nondetfunction op_strength_reduction 
               (op: operation) (args: list reg) (vl: list ival) :=
  match op, args, vl with
  | Oshrximm n, a1::nil, iv1::nil =>
      if (int_is_nonnegative iv1)
      then ((Oshruimm n), args)
      else (op, args)
  | Oshrxlimm n, a1::nil, iv1::nil =>
      if (long_is_nonnegative iv1)
      then ((Oshrluimm n), args)
      else (op, args)
  | Ocast32unsigned, a1::nil, iv1::nil =>
      if int_is_nonnegative iv1
      then (Ocast32signed, args)
      else (op, args)
  | _, _, _ => (op, args)
  end.

Inductive op_strength_reduction_cases: forall (op: operation) (args: list reg) (vl: list ival), Type :=
  | op_strength_reduction_case1: forall n a1 iv1, op_strength_reduction_cases (Oshrximm n) (a1::nil) (iv1::nil)
  | op_strength_reduction_case2: forall n a1 iv1, op_strength_reduction_cases (Oshrxlimm n) (a1::nil) (iv1::nil)
  | op_strength_reduction_case3: forall a1 iv1, op_strength_reduction_cases (Ocast32unsigned) (a1::nil) (iv1::nil)
  | op_strength_reduction_default: forall (op: operation) (args: list reg) (vl: list ival), op_strength_reduction_cases op args vl.

Definition op_strength_reduction_match (op: operation) (args: list reg) (vl: list ival) :=
  match op as zz1, args as zz2, vl as zz3 return op_strength_reduction_cases zz1 zz2 zz3 with
  | Oshrximm n, a1::nil, iv1::nil => op_strength_reduction_case1 n a1 iv1
  | Oshrxlimm n, a1::nil, iv1::nil => op_strength_reduction_case2 n a1 iv1
  | Ocast32unsigned, a1::nil, iv1::nil => op_strength_reduction_case3 a1 iv1
  | op, args, vl => op_strength_reduction_default op args vl
  end.

Definition op_strength_reduction (op: operation) (args: list reg) (vl: list ival) :=
  match op_strength_reduction_match op args vl with
  | op_strength_reduction_case1 n a1 iv1 =>
      if (int_is_nonnegative iv1) then ((Oshruimm n), args) else (op, args)
  | op_strength_reduction_case2 n a1 iv1 =>
      if (long_is_nonnegative iv1) then ((Oshrluimm n), args) else (op, args)
  | op_strength_reduction_case3 a1 iv1 =>
      if int_is_nonnegative iv1 then (Ocast32signed, args) else (op, args)
  | op_strength_reduction_default op args vl =>
      (op, args)
  end.

Original definition:

Nondetfunction addr_strength_reduction
           (addr: addressing) (args: list reg) (vl: list ival) :=
  match addr, args, vl with
  | (Aindexed n), a1::nil, iv1::nil => (addr, args)
  | _, _, _ => (addr, args)
  end.

Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg) (vl: list ival), Type :=
  | addr_strength_reduction_case1: forall n a1 iv1, addr_strength_reduction_cases ((Aindexed n)) (a1::nil) (iv1::nil)
  | addr_strength_reduction_default: forall (addr: addressing) (args: list reg) (vl: list ival), addr_strength_reduction_cases addr args vl.

Definition addr_strength_reduction_match (addr: addressing) (args: list reg) (vl: list ival) :=
  match addr as zz1, args as zz2, vl as zz3 return addr_strength_reduction_cases zz1 zz2 zz3 with
  | (Aindexed n), a1::nil, iv1::nil => addr_strength_reduction_case1 n a1 iv1
  | addr, args, vl => addr_strength_reduction_default addr args vl
  end.

Definition addr_strength_reduction (addr: addressing) (args: list reg) (vl: list ival) :=
  match addr_strength_reduction_match addr args vl with
  | addr_strength_reduction_case1 n a1 iv1 =>
      (addr, args)
  | addr_strength_reduction_default addr args vl =>
      (addr, args)
  end.

Original definition:

Nondetfunction cond_strength_reduction
           (cond: condition) (args: list reg) (vl: list ival) :=
  match cond, args, vl with
  | (Ccomp Cle), a1::a2::nil, iv1::iv2::nil =>
      if (int_is_nonnegative iv1) && (int_is_nonnegative iv2)
      then ((Ccompu Cle), args)
      else (cond, args)
  | _ => (cond, args)
  end.

Inductive cond_strength_reduction_cases: forall (cond: condition) (args: list reg) (vl: list ival), Type :=
  | cond_strength_reduction_case1: forall a1 a2 iv1 iv2, cond_strength_reduction_cases ((Ccomp Cle)) (a1::a2::nil) (iv1::iv2::nil)
  | cond_strength_reduction_default: forall (cond: condition) (args: list reg) (vl: list ival), cond_strength_reduction_cases cond args vl.

Definition cond_strength_reduction_match (cond: condition) (args: list reg) (vl: list ival) :=
  match cond as zz1, args as zz2, vl as zz3 return cond_strength_reduction_cases zz1 zz2 zz3 with
  | (Ccomp Cle), a1::a2::nil, iv1::iv2::nil => cond_strength_reduction_case1 a1 a2 iv1 iv2
  | cond, args, vl => cond_strength_reduction_default cond args vl
  end.

Definition cond_strength_reduction (cond: condition) (args: list reg) (vl: list ival) :=
  match cond_strength_reduction_match cond args vl with
  | cond_strength_reduction_case1 a1 a2 iv1 iv2 =>
      if (int_is_nonnegative iv1) && (int_is_nonnegative iv2) then ((Ccompu Cle), args) else (cond, args)
  | cond_strength_reduction_default cond args vl =>
      (cond, args)
  end.

Module IntervalpropOp

Converting known values to constants