# Module CombineOp

Recognition of combined operations, addressing modes and conditions during the CSE phase.

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Op.
Require Import CSEdomain.

Section COMBINE.

Variable get: valnum -> option rhs.

Function combine_compimm_ne_0 (x: valnum) : option(condition * list valnum) :=
match get x with
| Some(Op (Ocmp c) ys) => Some (c, ys)
| _ => None
end.

Function combine_compimm_eq_0 (x: valnum) : option(condition * list valnum) :=
match get x with
| Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
| _ => None
end.

Function combine_compimm_eq_1 (x: valnum) : option(condition * list valnum) :=
match get x with
| Some(Op (Ocmp c) ys) => Some (c, ys)
| _ => None
end.

Function combine_compimm_ne_1 (x: valnum) : option(condition * list valnum) :=
match get x with
| Some(Op (Ocmp c) ys) => Some (negate_condition c, ys)
| _ => None
end.

Function combine_cond (cond: condition) (args: list valnum) : option(condition * list valnum) :=
match cond, args with
| Ccompimm Cne n, x::nil =>
if Int.eq_dec n Int.zero then combine_compimm_ne_0 x
else if Int.eq_dec n Int.one then combine_compimm_ne_1 x
else None
| Ccompimm Ceq n, x::nil =>
if Int.eq_dec n Int.zero then combine_compimm_eq_0 x
else if Int.eq_dec n Int.one then combine_compimm_eq_1 x
else None
| Ccompuimm Cne n, x::nil =>
if Int.eq_dec n Int.zero then combine_compimm_ne_0 x
else if Int.eq_dec n Int.one then combine_compimm_ne_1 x
else None
| Ccompuimm Ceq n, x::nil =>
if Int.eq_dec n Int.zero then combine_compimm_eq_0 x
else if Int.eq_dec n Int.one then combine_compimm_eq_1 x
else None
| _, _ => None
end.

Definition combine_cond' (cond: condition) (args: list valnum) : option bool :=
match cond, args with
| (Ccomp c | Ccompu c | Ccompl c | Ccomplu c), x :: y :: nil => combine_comparison c x y
| _, _ => None
end.

| Aindexed n, x::nil =>
match get x with
| Some(Op (Oaddimm m) ys) =>
if Archi.ptr64 then None else Some(Aindexed (Ptrofs.add (Ptrofs.of_int m) n), ys)
| Some(Op (Oaddlimm m) ys) =>
if Archi.ptr64 then Some(Aindexed (Ptrofs.add (Ptrofs.of_int64 m) n), ys) else None
| _ => None
end
| _, _ => None
end.

Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) :=
match op, args with
| Oaddimm n, x :: nil =>
match get x with
| _ => None
end
| Oandimm n, x :: nil =>
match get x with
| Some(Op (Oandimm m) ys) =>
Some(let p := Int.and m n in
if Int.eq p m then (Omove, x :: nil) else (Oandimm p, ys))
| _ => None
end
| Oorimm n, x :: nil =>
match get x with
| Some(Op (Oorimm m) ys) => Some(Oorimm (Int.or m n), ys)
| _ => None
end
| Oxorimm n, x :: nil =>
match get x with
| Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys)
| _ => None
end
| Oaddlimm n, x :: nil =>
match get x with
| _ => None
end
| Oandlimm n, x :: nil =>
match get x with
| Some(Op (Oandlimm m) ys) =>
Some(let p := Int64.and m n in
if Int64.eq p m then (Omove, x :: nil) else (Oandlimm p, ys))
| _ => None
end
| Oorlimm n, x :: nil =>
match get x with
| Some(Op (Oorlimm m) ys) => Some(Oorlimm (Int64.or m n), ys)
| _ => None
end
| Oxorlimm n, x :: nil =>
match get x with
| Some(Op (Oxorlimm m) ys) => Some(Oxorlimm (Int64.xor m n), ys)
| _ => None
end
| Ocmp cond, _ =>
match combine_cond cond args with
| Some(cond', args') => Some(Ocmp cond', args')
| None => None
end
| _, _ => None
end.

End COMBINE.