Module BoxDomain

Require Import Coqlib Utf8.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Cminor.
Require Import Memory.
Require Import DLib.
Require Import LatticeSignatures.
Require Import AbEnvironment.
Require Import AbNumDomain.
Require Import IntervalDomain.

Module Box.

  Module AbTree := WPFun PTree.

  Section S.
    Context {Val: Type} (Dval: num_dom Val).
    Context (Dval_cor: num_dom_correct Dval).
    Local Notation var := positive.

  Definition t := @AbTree.t Val.
  Instance numd : Adom.adom Val int := @as_adom _ Dval.
  Instance adom : Adom.adom AbTree.t (var->int) := AbTree.makebot _.

  Definition ab_eval_constant (cst:nconstant) : Val+⊥ :=
    match cst with
      | NOintconst i => NotBot (const i)
      | NOintunknown => ⊤
    end.

  Lemma ab_eval_constant_correct: forall cst n,
    eval_nconstant cst n ->
    γ (ab_eval_constant cst) n.

  Definition cast_int7 : Val -> bool := is_in_itv Int.zero (Int.repr 127).
  Definition cast_int8s : Val -> bool := is_in_itv (Int.repr (-128)) (Int.repr 127).
  Definition cast_int8u : Val -> bool := is_in_itv Int.zero (Int.repr 255).
  Definition cast_int15 : Val -> bool := is_in_itv Int.zero (Int.repr 32767).
  Definition cast_int16s : Val -> bool := is_in_itv (Int.repr (-32768)) (Int.repr 32767).
  Definition cast_int16u : Val -> bool := is_in_itv Int.zero (Int.repr 65535).

  Definition eval_nunop (op:unary_operation) (v:Val) : Val+⊥ :=
    match op with
      | Ocast8unsigned => if cast_int8u v then NotBot v else ⊤
      | Ocast8signed => if cast_int8s v then NotBot v else ⊤
      | Ocast16unsigned => if cast_int16u v then NotBot v else ⊤
      | Ocast16signed => if cast_int16s v then NotBot v else ⊤
      | Onotbool => notbool v
      | Oboolval => boolval v
      | Onegint => neg v
      | Onotint => not v
      | Onegf
      | Oabsf
      | Osingleoffloat
      | Ointoffloat
      | Ointuoffloat
      | Ofloatofint
      | Ofloatofintu => ⊤
    end.

  Lemma ab_eval_nunop_correct: forall op n1 n ab,
    AbEnvironment.eval_nunop op n1 n ->
    γ ab n1 ->
    γ (eval_nunop op ab) n.

  Definition eval_nbinop (op:binary_operation) (v1 v2:Val) : Val+⊥ :=
    match op with
      | Oadd => add v1 v2
      | Osub => sub v1 v2
      | Omul => mul v1 v2
      | Odiv => divs v1 v2
      | Odivu => ⊤
      | Omod => ⊤
      | Omodu => ⊤
      | Oshl => if is_in_itv Int.zero (Int.sub Int.iwordsize Int.one) v2 then shl v1 v2 else ⊤
      | Oshr => ⊤
      | Oshru => ⊤
      | Ocmp c => NotBot booleans
      | Ocmpu c => NotBot booleans
      | Oand => and v1 v2
      | Oor => or v1 v2
      | Oxor => xor v1 v2
      | Oaddf
      | Osubf
      | Omulf
      | Odivf
      | Ocmpf _ => ⊤
    end.

  Lemma ab_eval_nbinop_correct: forall op n1 n2 n ab1 ab2,
    AbEnvironment.eval_nbinop op n1 n2 n ->
    γ ab1 n1 ->
    γ ab2 n2 ->
    γ (eval_nbinop op ab1 ab2) n.

  Fixpoint eval_expr (e:nexpr var) (ab:t) : Val+⊥ :=
    match e with
      | NEvar x => AbTree.get _ ab x
      | NEconst cst => ab_eval_constant cst
      | NEunop op e => botbind (eval_nunop op) (eval_expr e ab)
      | NEbinop op e1 e2 =>
        botbind2 (eval_nbinop op) (eval_expr e1 ab) (eval_expr e2 ab)
      | NEcondition b l r =>
        botbind
          (fun k =>
             if is_in_itv Nfalse Nfalse k then eval_expr r ab
             else match meet k (NotBot (const Nfalse)) with
                    | Bot => eval_expr l ab
                    | NotBot _ => eval_expr r ab ⊔ eval_expr l ab
                  end)
          (eval_expr b ab)
    end.

  Lemma eval_expr_correct : forall ρ ab e n,
    γ ab ρ ->
    eval_nexpr ρ e n ->
    γ (eval_expr e ab) n.

  Definition get_itv e (ab: AbTree.t) (s: sign_flag) :=
    botbind (fun x => range x s) (eval_expr e ab).

  Lemma get_itv_correct: forall e ρ (ab: AbTree.t),
    γ ab ρ ->
    eval_nexpr ρ e ⊆ ints_in_range (get_itv e ab).

  Definition assign (x:var) (e:nexpr var) (ab:t) : t :=
    AbTree.set ab x (eval_expr e ab).

  Existing Instance adom.
  Lemma assign_correct : forall x e ρ n ab,
    ρ ∈ γ ab ->
    eval_nexpr ρ e n ->
    (upd ρ x n) ∈ γ (assign x e ab).

  Definition lift1 {A B:Type} (f:A->B+⊥) (a:A+⊥) : B+⊥ :=
    match a with
      | Bot => Bot
      | NotBot a => f a
    end.

  Definition lift2 {A B:Type} (f:A->A->B+⊥) (a:(A+⊥)*(A+⊥)) : B+⊥ :=
    match a with
      | (Bot, _) => Bot
      | (_, Bot) => Bot
      | (NotBot a1, NotBot a2) => f a1 a2
    end.


  Instance numdb : Adom.adom (Val+⊥) int := lift_bot numd.

  Fixpoint backward_expr (e:nexpr var) (ab:t) (itv:Val) : t :=
    match e with
      | NEvar x =>
        AbTree.set ab x (meet itv (AbTree.get numd ab x))
      | NEconst cst =>
        if leb (meet itv (ab_eval_constant cst)) Bot
          then Bot
          else ab
      | NEunop op e =>
        lift1
        (fun i =>
          match op with
            | Oboolval => lift1 (backward_expr e ab) (backward_boolval i itv)
            | Onegint => lift1 (backward_expr e ab) (backward_neg i itv)
            | Onotbool => lift1 (backward_expr e ab) (backward_notbool i itv)
            | Onotint => lift1 (backward_expr e ab) (backward_not i itv)
            | _ => ab
          end)
        (eval_expr e ab)
      | NEbinop op e1 e2 =>
        lift2
        (fun i1 i2 =>
          match op with
            | Oadd =>
              lift2 (fun itv1 itv2 =>
                backward_expr e2 (backward_expr e1 ab itv1) itv2)
              (backward_add i1 i2 itv)
            | Osub =>
              lift2 (fun itv1 itv2 =>
                backward_expr e2 (backward_expr e1 ab itv1) itv2)
              (backward_sub i1 i2 itv)
            | Ocmp c =>
              lift2 (fun itv1 itv2 =>
                backward_expr e2 (backward_expr e1 ab itv1) itv2)
              (backward_cmp c i1 i2 itv)
            | Ocmpu c =>
              lift2 (fun itv1 itv2 =>
                backward_expr e2 (backward_expr e1 ab itv1) itv2)
              (backward_cmpu c i1 i2 itv)
            | Oand =>
              union_list Bot (join (adom:=adom))
              (map
                (lift2 (fun itv1 itv2 =>
                  backward_expr e2 (backward_expr e1 ab itv1) itv2))
                (backward_and i1 i2 itv))
            | Oor =>
              union_list Bot (join (adom:=adom))
              (map
                (lift2 (fun itv1 itv2 =>
                  backward_expr e2 (backward_expr e1 ab itv1) itv2))
                (backward_or i1 i2 itv))
            | _ => ab
          end)
        (eval_expr e1 ab, eval_expr e2 ab)
      | NEcondition b l r =>
          backward_expr b (backward_expr r ab itv) (const Nfalse)
        ⊔ lift1 (fun i => lift1
                            (backward_expr b (backward_expr l ab itv))
                            (backward_boolval i (const Ntrue)))
                (eval_expr b ab)
    end.

  Lemma backward_expr_correct: forall ρ e i,
    eval_nexpr ρ e i -> forall ab,
    γ ab ρ -> forall itv,
    γ itv i ->
    γ (backward_expr e ab itv) ρ.

  Definition assume_once (e:nexpr var) (ab:t) : t :=
    backward_expr e ab (const Int.one).

  Fixpoint assume' (fuel: nat) (e: nexpr var) (ab: t) : t :=
    match fuel with
      | O => ab
      | S fuel' =>
        let ab' := assume_once e ab in
        if leb ab ab' then ab else assume' fuel' e ab'
    end.

  Definition assume := assume' 12.

  Lemma assume_once_correct: forall e ρ ab,
    eval_nexpr ρ e Ntrue ->
    γ ab ρ ->
    γ (assume_once e ab) ρ.

  Lemma assume'_correct: forall fuel e ρ ab,
    ρ ∈ γ ab ->
    Ntrue ∈ eval_nexpr ρ e ->
    ρ ∈ γ (assume' fuel e ab).

  Lemma assume_correct: forall e ρ ab,
    ρ ∈ γ ab ->
    Ntrue ∈ eval_nexpr ρ e ->
    ρ ∈ γ (assume e ab).

  Definition abdom : int_dom t := Build_int_dom _
    adom
    get_itv
    assign
    assume
    get_itv_correct
    assign_correct
    assume_correct.

End S.

End Box.