Module IntervalDomain

Abstract domain of intervals of machine integers.

Require Import Coqlib.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Op.
Require Import Utils.
Require Import LatticeSignatures.
Require Import CfgIterator.

Module Interval.

  Record itv : Type := ITV { min: Z; max: Z }.
  Definition t := itv.

  Definition order (i1 i2: itv) : bool :=
    match i1, i2 with
      | (ITV min1 max1), (ITV min2 max2) =>
        zle min2 min1 && zle max1 max2
    end.

  Definition join (i1 i2: itv) : itv :=
    match i1, i2 with
      | (ITV min1 max1), (ITV min2 max2) =>
        (ITV (Zmin min1 min2) (Zmax max1 max2))
    end.

  Definition widen_classic (i1 i2: itv) : itv :=
    match i1, i2 with
      | (ITV min1 max1), (ITV min2 max2) =>
        ITV
        (if zle min1 min2 then min1 else Int.min_signed)
(if zle max2 max1 then max1 else Int.max_signed)
    end.

  Fixpoint next_pow2_pos (p:positive) :=
    match p with
    | xH => xH
    | xI p
    | xO p => xI (next_pow2_pos p)
    end.

  Definition previous_pow2_pos p :=
    let p' := next_pow2_pos p in
     match p' with
       | xI p => p
       | _ => p'
     end.

  Definition next_threshold (z:Z) :=
    match z with
      | Z0 => Z0
      | Zpos xH => Zpos xH
      | Zneg xH => Zneg xH
      | Zpos p => Zpos (next_pow2_pos p)
      | Zneg p => Zneg (previous_pow2_pos p)
    end.

  Definition previous_threshold (z:Z) :=
    match z with
      | Z0 => Z0
      | Zpos xH => Zpos xH
      | Zneg xH => Zneg xH
      | Zpos p => Zpos (previous_pow2_pos p)
      | Zneg p => Zneg (next_pow2_pos p)
    end.

  Definition widen (i1 i2: itv) : itv :=
    match i1, i2 with
      | (ITV min1 max1), (ITV min2 max2) =>
        ITV
        (if zle min1 min2 then min1
          else previous_threshold (Zmin min1 min2))
(if zle max2 max1 then max1
          else next_threshold (Zmax max1 max2))
    end.

  Definition top : itv := (ITV Int.min_signed Int.max_signed).

  Definition gamma (i:itv) (v:val) : Prop :=
    match v with
      | Vint n => min i <= Int.signed n <= max i
      | _ => True
    end.

  Lemma gamma_top : forall v,
    gamma top v.

Proof.

    destruct v; simpl; auto.
    apply Int.signed_range.
  Qed.

Lemma gamma_monotone : forall ab1 ab2,
order ab1 ab2 = true -> forall v, gamma ab1 v -> gamma ab2 v.

Proof.

    destruct ab1 as [min1 max1].
    destruct ab2 as [min2 max2]; simpl in *.
    destruct v; simpl in *; auto.
    rewrite andb_true_iff in *; repeat rewrite zle_true_iff in *; try omega.
  Qed.

  Definition wlat : WLattice.t itv val :=
   (WLattice.make _ _
    order
    top
    join
    widen
    gamma
    gamma_monotone
    gamma_top ).

  Definition itvbot := option itv.

  Definition bwlat : BWLattice.t itvbot val := BWLattice.from_wlattice wlat.

  Definition reduce (min max : Z) : option itv :=
    if zle min max then Some (ITV min max) else None.

  Definition meet (i1: itv) (i2:itvbot) : itvbot :=
    match i2 with
      | None => None
      | Some i2 =>
        match i1, i2 with
          | (ITV min1 max1), (ITV min2 max2) =>
            reduce (Zmax min1 min2) (Zmin max1 max2)
        end
    end.

  Definition repr (i:itv) : itv :=
    if WLattice.leb wlat i (WLattice.top wlat) then i else (WLattice.top wlat).

  Definition signed (n:int) : itv :=
    let z := Int.signed n in
      (ITV z z).

  Definition neg (i:itv) : itv :=
    match i with
      | (ITV min max) =>
        repr (ITV (-max) (-min))
    end.

  Definition mult (i1 i2:itv) : itv :=
    let min1 := min i1 in
    let min2 := min i2 in
    let max1 := max i1 in
    let max2 := max i2 in
    let b1 := min1 * min2 in
    let b2 := min1 * max2 in
    let b3 := max1 * min2 in
    let b4 := max1 * max2 in
      repr (ITV
               (Zmin (Zmin b1 b4) (Zmin b3 b2))
               (Zmax (Zmax b1 b4) (Zmax b3 b2))).

  Definition add (i1 i2:itv) : itv :=
    repr (ITV ((min i1)+(min i2)) ((max i1)+(max i2))).

  Definition sub (i1 i2:itv) : itv :=
    repr (ITV ((min i1)-(max i2)) ((max i1)-(min i2))).

  Definition backward_eq (i1 i2:itv) : itvbot * itvbot :=
    (meet i1 (Some i2), meet i1 (Some i2)).

  Definition backward_lt (i1 i2:itv) : itvbot * itvbot :=
        (meet i1 (reduce Int.min_signed ((max i2)-1)),
          meet i2 (reduce ((min i1)+1) Int.max_signed))
    .

  Definition backward_ne (i1 i2:itv) : itvbot * itvbot :=
    let (i1',i2') := backward_lt i1 i2 in
      let (i2'',i1'') := backward_lt i2 i1 in
        (BWLattice.join bwlat i1' i1'',BWLattice.join bwlat i2' i2'').

  Definition backward_le (i1 i2:itv) : itvbot * itvbot :=
    (meet i1 (reduce Int.min_signed (max i2)),
      meet i2 (reduce (min i1) Int.max_signed))
    .

  Definition is_in_interval (a b : Z) (ab:itv) : bool :=
    WLattice.leb wlat ab (ITV a b).

  Definition cast_int16u : Interval.t-> bool := is_in_interval 0 65535.

  Definition backward_leu (i1 i2:itv) : itvbot * itvbot :=
    if cast_int16u i1 && cast_int16u i2
      then backward_le i1 i2
      else (Some i1, Some i2).

  Definition backward_ltu (i1 i2:itv) : itvbot * itvbot :=
    if cast_int16u i1 && cast_int16u i2
      then backward_lt i1 i2
      else (Some i1, Some i2).

  Definition booleans :=
    join (signed Int.zero) (signed Int.one).

  Definition gamma' := BWLattice.gamma bwlat.

  Lemma meet_correct: forall ab1 ab2 i,
    gamma ab1 (Vint i) -> gamma' ab2 (Vint i) -> gamma' (meet ab1 ab2) (Vint i).

Proof.

    unfold meet, gamma'.
    destruct ab1; simpl; try (intuition; fail).
    destruct i; simpl.
    destruct ab2; simpl; try (intuition; fail).
    destruct i; simpl.
    assert (TT:Int.min_signed <= Int.max_signed).
    intro H; inv H.
    apply Zmax_case_strong; apply Zmin_case_strong; unfold reduce; simpl; repeat (destruct zle; simpl);
      intros; omega.
  Qed.

  Lemma join_correct : forall i1 i2 i,
    gamma' i1 (Vint i) \/ gamma' i2 (Vint i) ->
    gamma' (BWLattice.join bwlat i1 i2) (Vint i).

Proof.

    unfold join, gamma'.
    destruct i1; simpl; try (intuition; fail).
    destruct i; simpl.
    destruct i2; simpl; try (intuition; fail).
    destruct i; simpl.
    intros.
    apply Zmax_case_strong; apply Zmin_case_strong;
      omega.
  Qed.

  Lemma neg_correct : forall ab i,
    gamma ab (Vint i) ->
    gamma (neg ab) (Vint (Int.neg i)).

Proof.

    destruct ab; simpl; auto; intros.
    unfold gamma.
    destruct i; simpl in *.
    unfold repr; simpl.
    case_eq (zle Int.min_signed (- max0) && zle (- min0) Int.max_signed); auto.
    repeat rewrite andb_true_iff; repeat rewrite zle_true_iff; intros [T1 T2].
    simpl.
    unfold Int.neg; rewrite <- neg_signed_unsigned.
    rewrite Int.signed_repr; omega.
    intros; apply Int.signed_range.
  Qed.

Lemma signed_correct: forall i, gamma (signed i) (Vint i).

Proof.

unfold signed, gamma'; simpl; intros; omega.
Qed.

Lemma bool_correct_zero : gamma booleans (Vint Int.zero).

Proof.

    unfold booleans.
    apply (join_correct (Some (signed Int.zero)) (Some (signed Int.one))); simpl.
    left; unfold gamma', signed; simpl; omega.
  Qed.

Lemma bool_correct_one : gamma booleans (Vint Int.one).

Proof.

    unfold booleans.
    apply (join_correct (Some (signed Int.zero)) (Some (signed Int.one))); simpl.
    right; unfold gamma', signed; simpl; omega.
  Qed.

  Lemma is_in_interval_correct : forall a b ab,
    is_in_interval a b ab = true ->
    forall i, gamma ab (Vint i) -> a <= Int.signed i <= b.

Proof.

    unfold is_in_interval; simpl; intros.
    destruct ab; simpl in *.
    repeat rewrite andb_true_iff in *; repeat rewrite zle_true_iff in *; destruct H; omega.
  Qed.

  Lemma add_correct : forall ab1 ab2 i1 i2,
    gamma ab1 (Vint i1) -> gamma ab2 (Vint i2) ->
    gamma (add ab1 ab2) (Vint (Int.add i1 i2)).

Proof.

    unfold gamma', gamma, add, repr; simpl.
    destruct ab1; destruct ab2; simpl; intros; auto.
    unfold gamma', gamma, add, repr; simpl.
    case_eq (zle Int.min_signed (min0 + min1)
      && zle (max0 + max1) Int.max_signed); simpl; auto.
    repeat rewrite andb_true_iff; repeat rewrite zle_true_iff; intros [T1 T2].
    unfold Int.add.
    rewrite <- add_signed_unsigned.
    rewrite Int.signed_repr; try omega.
    intros; apply Int.signed_range.
  Qed.

  Lemma sub_correct : forall ab1 ab2 i1 i2,
    gamma ab1 (Vint i1) -> gamma ab2 (Vint i2) ->
    gamma (sub ab1 ab2) (Vint (Int.sub i1 i2)).

Proof.

    unfold gamma'.
    destruct ab1; destruct ab2; simpl; intros; auto.
    unfold gamma, sub, repr; simpl.
    case_eq (zle Int.min_signed (min0 - max1)
      && zle (max0 - min1) Int.max_signed); simpl; auto.
    repeat rewrite andb_true_iff; repeat rewrite zle_true_iff; intros [T1 T2].
    unfold Int.sub.
    rewrite <- sub_signed_unsigned.
    rewrite Int.signed_repr; try omega.
    intros; apply Int.signed_range.
  Qed.

  Lemma mul_correct : forall ab1 ab2 i1 i2,
    gamma ab1 (Vint i1) -> gamma ab2 (Vint i2) ->
    gamma (mult ab1 ab2) (Vint (Int.mul i1 i2)).

Proof.

    unfold gamma'.
    destruct ab1; destruct ab2; simpl; intros; auto.
    unfold gamma, mult, repr; simpl.
    case_eq (zle Int.min_signed
           (Zmin (Zmin (min0 * min1) (max0 * max1))
              (Zmin (max0 * min1) (min0 * max1))) &&
         zle
           (Zmax (Zmax (min0 * min1) (max0 * max1))
              (Zmax (max0 * min1) (min0 * max1))) Int.max_signed); simpl; auto.
    repeat rewrite andb_true_iff; repeat rewrite zle_true_iff; intros [T1 T2].
    unfold Int.mul.
    rewrite <- mult_signed_unsigned.
    assert (HZ:=Mult_interval_correct_min_max _ _ _ _ _ _ H H0).
    rewrite Int.signed_repr; try omega.
    intros; apply Int.signed_range.
  Qed.

  Lemma gamma_backward_eq: forall ab1 ab2 ab1' ab2' i1 i2,
    backward_eq ab1 ab2 = (ab1',ab2') ->
    gamma ab1 (Vint i1) ->
    gamma ab2 (Vint i2) ->
    Int.eq i1 i2 = true ->
    gamma' ab1' (Vint i1) /\ gamma' ab2' (Vint i2).

Proof.

    Opaque meet.
    unfold gamma', backward_eq; simpl; intros.
    destruct ab1; simpl in *; try (intuition; fail);
      destruct ab2; simpl in *; try (intuition; fail).
    generalize (Int.eq_spec i1 i2); rewrite H2; intros; subst.
    unfold backward_eq in H; inv H.
    split; apply meet_correct; simpl; auto.
  Qed.

Transparent meet.

Lemma max_signed_unsigned: Int.max_unsigned = 2*Int.max_signed + 1.

Proof.

  unfold Int.max_signed, Int.max_unsigned.
  generalize Int.half_modulus_modulus; intros HH1.
  omega.
Qed.

  Lemma gamma_backward_lt: forall ab1 ab2 ab1' ab2' i1 i2,
    backward_lt ab1 ab2 = (ab1',ab2') ->
    gamma ab1 (Vint i1) ->
    gamma ab2 (Vint i2) ->
    Int.lt i1 i2 = true ->
    gamma' ab1' (Vint i1) /\ gamma' ab2' (Vint i2).

Proof.

    unfold gamma', backward_lt; simpl; intros.
    unfold gamma.
    destruct ab1; destruct ab2; simpl in *.
    assert (I1:=Int.signed_range i1).
    assert (I2:=Int.signed_range i2).
    unfold Int.lt in H2; destruct zlt; try congruence.
    unfold reduce in *.
    assert (M:=max_signed_unsigned).
    repeat destruct zle; simpl in *; inv H; simpl; try (split; omega);
    unfold reduce in *; repeat destruct zle; simpl; try (split; omega).
    generalize dependent z2; generalize dependent z3.
    repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; try omega.
    generalize dependent z2; generalize dependent z3.
    repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; try omega.
    generalize dependent z2; generalize dependent z3.
    repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; try omega.
    generalize dependent z2; generalize dependent z3.
    repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; try omega.
  Qed.

  Lemma gamma_backward_ne: forall ab1 ab2 ab1' ab2' i1 i2,
    backward_ne ab1 ab2 = (ab1',ab2') ->
    gamma ab1 (Vint i1) ->
    gamma ab2 (Vint i2) ->
    negb (Int.eq i1 i2) = true ->
    gamma' ab1' (Vint i1) /\ gamma' ab2' (Vint i2).

Proof.

    unfold backward_ne; intros.
    case_eq (backward_lt ab1 ab2); intros i1' i2' G1; rewrite G1 in *.
    case_eq (backward_lt ab2 ab1); intros i1'' i2'' G2; rewrite G2 in *.
    inv H.
    assert (H2':Int.eq i1 i2=false).
      destruct (Int.eq i1 i2); inv H2; auto.
    generalize (Int.eq_spec i1 i2); rewrite H2'; intros; subst.
    assert (Int.signed i1 <> Int.signed i2).
      apply Int.eq_false in H.
      unfold Int.eq in H.
      destruct zeq; try congruence.
      red; intro; elim n.
      unfold Int.signed in *.
      generalize Int.half_modulus_modulus; intros HH1.
      generalize (Int.unsigned_range i1); intros R1.
      generalize (Int.unsigned_range i2); intros R2.
      do 2 destruct zlt; try omega.
    assert (Int.signed i1 < Int.signed i2 \/ Int.signed i2 < Int.signed i1) by omega.
    destruct H4.
    exploit (gamma_backward_lt ab1 ab2 i1' i2'); eauto.
    unfold Int.lt; destruct zlt; auto.
    generalize (join_correct i1' i2''); simpl; intros J1.
    generalize (join_correct i2' i1''); simpl; intros J2.
    split.
    apply J1; intuition.
    apply J2; intuition.
    exploit (gamma_backward_lt ab2 ab1 i1'' i2''); eauto.
    unfold Int.lt; destruct zlt; auto.
    generalize (join_correct i1' i2''); simpl; intros J1.
    generalize (join_correct i2' i1''); simpl; intros J2.
    split; intuition.
  Qed.

  Lemma gamma_backward_le: forall ab1 ab2 ab1' ab2' i1 i2,
    backward_le ab1 ab2 = (ab1',ab2') ->
    gamma ab1 (Vint i1) ->
    gamma ab2 (Vint i2) ->
    negb (Int.lt i2 i1) = true ->
    gamma' ab1' (Vint i1) /\ gamma' ab2' (Vint i2).

Proof.

    unfold gamma', backward_le; simpl; intros.
    destruct ab1; simpl in *; try (intuition; fail);
      destruct ab2; simpl in *; try (intuition; fail).
    assert (I1:=Int.signed_range i1).
    assert (I2:=Int.signed_range i2).
    unfold Int.lt in H2; destruct zlt; simpl in H2; try congruence.
    unfold reduce in *.
    repeat destruct zle; simpl in *; inv H; simpl; try (split; omega);
    unfold reduce in *;
    repeat destruct zle; simpl; try (split; omega).
    generalize dependent z2; generalize dependent z3.
    repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; try omega.
    generalize dependent z2; generalize dependent z3.
    repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; try omega.
    generalize dependent z2; generalize dependent z3.
    repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; try omega.
    generalize dependent z2; generalize dependent z3.
    repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; try omega.
  Qed.

  Lemma cast_int16u_correct: forall ab i,
    cast_int16u ab = true ->
    gamma ab (Vint i) ->
    Int.signed i = Int.unsigned i.

Proof.

    unfold cast_int16u; destruct ab ;simpl; intros.
    assert (I1:=Int.intrange i).
    assert (HI:=is_in_interval_correct _ _ _ H _ H0); clear H.
    unfold Int.signed, Int.unsigned in *.
    destruct zlt; try omega.
  Qed.

  Lemma gamma_backward_leu: forall ab1 ab2 ab1' ab2' i1 i2,
    backward_leu ab1 ab2 = (ab1',ab2') ->
    gamma ab1 (Vint i1) ->
    gamma ab2 (Vint i2) ->
    negb (Int.ltu i2 i1) = true ->
    gamma' ab1' (Vint i1) /\ gamma' ab2' (Vint i2).

Proof.

    unfold backward_leu; simpl; intros.
    case_eq (cast_int16u ab1); intros; rewrite H3 in H; simpl in *.
    case_eq (cast_int16u ab2); intros; rewrite H4 in H; simpl in *.
    assert (negb (Int.lt i2 i1) = true).
    unfold Int.ltu in H2; destruct zlt; simpl in H2; try congruence.
    unfold Int.lt; destruct zlt; simpl; try congruence.
    rewrite (cast_int16u_correct ab1 i1) in z0; auto.
    rewrite (cast_int16u_correct ab2 i2) in z0; auto.
    eapply gamma_backward_le; eauto.
    unfold gamma'; simpl; intros; inv H; split; auto.
    unfold gamma'; simpl; intros; inv H; split; auto.
  Qed.

  Lemma gamma_backward_ltu: forall ab1 ab2 ab1' ab2' i1 i2,
    backward_ltu ab1 ab2 = (ab1',ab2') ->
    gamma ab1 (Vint i1) ->
    gamma ab2 (Vint i2) ->
    Int.ltu i1 i2 = true ->
    gamma' ab1' (Vint i1) /\ gamma' ab2' (Vint i2).

Proof.

    unfold backward_ltu; simpl; intros.
    case_eq (cast_int16u ab1); intros; rewrite H3 in H; simpl in *.
    case_eq (cast_int16u ab2); intros; rewrite H4 in H; simpl in *.
    assert (Int.lt i1 i2 = true).
    unfold Int.ltu in H2; destruct zlt; simpl in H2; try congruence.
    unfold Int.lt; destruct zlt; simpl; try congruence.
    rewrite (cast_int16u_correct ab1 i1) in z0; auto.
    rewrite (cast_int16u_correct ab2 i2) in z0; auto.
    eapply gamma_backward_lt; eauto.
    unfold gamma'; simpl; intros; inv H; split; auto.
    unfold gamma'; simpl; intros; inv H; split; auto.
  Qed.

Lemma gamma_contains_Vundef : forall ab, gamma ab Vundef.

Proof.

destruct ab; simpl; auto.
Qed.

Hint Resolve gamma_top signed_correct gamma_contains_Vundef.

End Interval.