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) => Some(Olongconst n)
  | _ => None
  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 (Ocast32signed) (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
  | Ocast32signed, 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 (Ocast32unsigned, args) else (op, args)
  | op_strength_reduction_default op args vl =>
      (op, args)
  end.


Definition addr_strength_reduction
           (addr: addressing) (args: list reg) (vl: list ival) :=
  match addr with
  | Aindexed _ => (addr, args)
  | _ => (addr, args)
  end.

Definition cond_strength_reduction
           (cond: condition) (args: list reg) (vl: list ival) :=
  match cond with
  | Ccomp _ => (cond, args)
  | _ => (cond, args)
  end.