Module IntPromotion

Require Import Coqlib.
Require Import Op.
Require Import Values Integers.
Require Import IntPromotionCommon.
Require Import ZIntervalDomain.
Require Import OptionMonad.
Import ListNotations.

Local Open Scope option_monad_scope.

Lemma int_unsigned_pos n:
  0 <=? Int.unsigned n = true.

Definition is_Iint (v : ival): bool :=
  match v with
  | Iint false _ => true
  | _ => false
  end.

Lemma inv_is_Iint v:
  is_Iint v = true -> exists i, v = Iint false i.

Definition mk_op_prom1 (op' : operation) (usg sgn : bool) (args : list bool) (res : bool) : op_promotion :=
  mk_op_prom (ASSERT usg IN Some op') (ASSERT sgn IN Some op') args res.

Definition promote_operation (op : operation) (args : list ival) : op_promotion :=
  match op, args with
  | Omove, [x] =>
      mk_op_prom (Some Omove) (Some Omove) [true] true
  | Ointconst n, [] =>
      mk_op_prom (Some (Olongconst (promote false n))) (Some (Olongconst (promote true n))) [] true
  | Oadd, [Iint b1 i1; Iint b2 i2] =>
      mk_op_prom1 Oaddl
        (is_in_unsigned_range (Itv.add (Itv32.mod_itv i1) (Itv32.mod_itv i2)))
        (is_in_signed_range (Itv.add (zinterval_sgn_of_usg i1) (zinterval_sgn_of_usg i2)))
        [true; true] true
  | Oaddimm n, [Iint b1 i1] =>
      mk_op_prom
        (if is_in_unsigned_range (Itv.add (Itv32.mod_itv i1) (Itv.intconst (Int.unsigned n)))
         then Some (Oaddlimm (promote false n))
         else if is_in_unsigned_range (Itv.add (Itv32.mod_itv i1) (Itv.intconst (Int.signed n)))
         then Some (Oaddlimm (promote true n))
         else None)
        (ASSERT (is_in_signed_range (Itv.add (zinterval_sgn_of_usg i1) (Itv.intconst (Int.signed n)))) IN
         Some (Oaddlimm (promote true n)))
        [true] true
  | Osub, [Iint b1 i1; Iint b2 i2] =>
      mk_op_prom1 Osubl
        (is_in_unsigned_range (Itv.sub (Itv32.mod_itv i1) (Itv32.mod_itv i2)))
        (is_in_signed_range (Itv.sub (zinterval_sgn_of_usg i1) (zinterval_sgn_of_usg i2)))
        [true; true] true
  | Oshl, [Iint b1 i1; Iint b2 i2] =>
      mk_op_prom
        (ASSERT (zlt (Itv.itv_hi (Itv32.mod_itv i2)) Int.zwordsize &&
                 is_in_unsigned_range (Itv.shl (Itv32.mod_itv i1) (Itv32.mod_itv i2)
                                 (Itv32.mod_lo i1) (Itv32.mod_lo i2))) IN
         Some Oshll)
        None
        [true; false] true
  | Oshlimm n, [Iint b1 i1] =>
      mk_op_prom
        (ASSERT (zlt (Int.unsigned n) Int.zwordsize &&
                 is_in_unsigned_range (Itv.shl (Itv32.mod_itv i1) (Itv.intconst (Int.unsigned n))
                                 (Itv32.mod_lo i1) (int_unsigned_pos _))) IN
         Some (Oshllimm n))
        None
        [true] true
  | Ocast32signed, [Iint b1 i1] =>
      mk_op_prom None (Some Omove) [true] false
  | Ocast32unsigned, [Iint b1 i1] =>
      mk_op_prom (Some Omove) None [true] false
  | _, _ =>
      op_prom_None
  end.

Definition promote_condition (cond : condition) (args : list ival) : cond_promotion :=
  match cond, args with
  | Ccomp c, [x1; x2] =>
      mk_cond_prom None (Some (Ccompl c))
  | Ccompu c, [x1; x2] =>
      mk_cond_prom
        (ASSERT (Archi.ptr64 || (is_Iint x1 && is_Iint x2)) IN
         Some (Ccomplu c))
        None
  | Ccompimm c n, [x1] =>
      mk_cond_prom None (Some (Ccomplimm c (promote true n)))
  | Ccompuimm c n, [x1] =>
      mk_cond_prom
        (ASSERT (Archi.ptr64 || is_Iint x1) IN
         Some (Ccompluimm c (promote false n)))
        None
  | _,_ =>
      cond_prom_None
  end.


Local Ltac inv_hypothesis :=
  match goal with
  | H : list_forall2 _ _ (_ :: _) |- _ => inv H
  | H : list_forall2 _ _ nil |- _ => inv H
  | H : is_Iint _ = true |- _ => apply inv_is_Iint in H as (? & ->)
  | H : vmatch _ (Iint _ _) |- _ => inv H
  | H : _ && _ = true |- _ => apply andb_prop in H as [? ?]
  | H : _ || _ = true |- _ => apply orb_prop in H as [?|?]
  | H : proj_sumbool _ = true |- _ => apply proj_sumbool_true in H
  end.

Local Hint Resolve zinterval_sgn_of_usg_correct Itv.zmatch_intconst
                   Itv.zmatch_add Itv.zmatch_sub Itv.zmatch_shl : itv.

Local Hint Resolve Int.eqm_signed_unsigned Int64.eqm_signed_unsigned Int.eqm_add Int64.eqm_add
                   Int.eqm_sub Int64.eqm_sub : eqm.

Lemma elim_hi_lt itv bd i
  (H : Itv.itv_hi itv < bd)
  (Z : Itv.zmatch i itv):
  i < bd.

Local Ltac inv_hypothesis_unsafe :=
  match goal with
  | H : is_in_unsigned_range _ = true |- _ =>
      eapply is_in_unsigned_range_sound in H; [|solve [eauto with itv]]
  | H : is_in_signed_range _ = true |- _ =>
      eapply is_in_signed_range_sound in H; [|solve [eauto with itv]]
  | H : Itv.itv_hi _ < _ |- _ =>
      eapply elim_hi_lt in H; [|solve [eauto with itv]]
  end.

Local Ltac unsigned_to_signed :=
  erewrite <- Int.eqm_samerepr, <- Int64.eqm_samerepr by (eauto with eqm).

Local Ltac slv_casts :=
  simpl; unfold promote; repeat f_equal;
  rewrite ?Int.unsigned_repr, ?Int.signed_repr, ?Int64.unsigned_repr, ?Int64.signed_repr
    by (auto using Int64.int_unsigned_range, int64_int_signed_range);
  reflexivity.

Lemma promote_operation_sound F V ge sp m op args iargs
  (MATCH : list_forall2 vmatch args iargs):
  sound_op_promotion (@promotable_op F V ge sp m) op (promote_operation op iargs) args.

Lemma promote_condition_sound m cond args iargs
  (MATCH : list_forall2 vmatch args iargs):
  sound_cond_promotion (@promotable_cond m) cond (promote_condition cond iargs) args.

Global Opaque promote_operation promote_condition.