Module AbEnvironment

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 IntervalDomain.

Set Implicit Arguments.
Section nexpr.
  Variable var : Type.

  Inductive nconstant : Type :=
  | NOintconst: int -> nconstant
  | NOintunknown : nconstant.

  Inductive nexpr : Type :=
  | NEvar : var -> nexpr
  | NEconst : nconstant -> nexpr
  | NEunop : unary_operation -> nexpr -> nexpr
  | NEbinop : binary_operation -> nexpr -> nexpr -> nexpr
  | NEcondition : nexpr -> nexpr -> nexpr -> nexpr
  .

  Section eval_nexpr.
    Variable ρ: var -> int.

    Inductive eval_nconstant : nconstant -> int -> Prop :=
    | eval_nconstant_NOintconst: forall n,
      eval_nconstant (NOintconst n) n
    | eval_nconstant_NOintunknown: forall n,
      eval_nconstant NOintunknown n.

    Inductive is_bool : int -> Prop :=
    | is_bool_false: is_bool Int.zero
    | is_bool_true: is_bool Int.one.

    Definition Ntrue: int := Int.one.
    Definition Nfalse: int := Int.zero.

    Definition of_bool (b: bool): int :=
      if b then Ntrue else Nfalse.

    Inductive eval_nunop : unary_operation -> int -> int -> Prop :=
    | eval_nunop_Ocast8unsigned: forall i,
      eval_nunop Ocast8unsigned i (Int.zero_ext 8 i)
    | eval_nunop_Ocast8signed: forall i,
      eval_nunop Ocast8signed i (Int.sign_ext 8 i)
    | eval_nunop_Ocast16unsigned: forall i,
      eval_nunop Ocast16unsigned i (Int.zero_ext 16 i)
    | eval_nunop_Ocast16signed: forall i,
      eval_nunop Ocast16signed i (Int.sign_ext 16 i)
    | eval_nunop_Oboolval : forall i,
      eval_nunop Oboolval i (of_bool (negb (Int.eq i Int.zero)))
    | eval_numop_Onegint : forall i,
      eval_nunop Onegint i (Int.neg i)
    | eval_nunop_Onotbool : forall i,
      eval_nunop Onotbool i (of_bool (Int.eq i Int.zero))
    | eval_numop_Onotint : forall i,
      eval_nunop Onotint i (Int.not i).

    Inductive eval_nbinop : binary_operation -> int -> int -> int -> Prop :=
    | eval_nbinop_Oadd : forall i1 i2,
      eval_nbinop Oadd i1 i2 (Int.add i1 i2)
    | eval_nbinop_Osub : forall i1 i2,
      eval_nbinop Osub i1 i2 (Int.sub i1 i2)
    | eval_nbinop_Omul : forall i1 i2,
      eval_nbinop Omul i1 i2 (Int.mul i1 i2)
    | eval_nbinop_Odiv : forall i1 i2,
      Int.eq i2 Int.zero = false ->
      (Int.eq i1 (Int.repr Int.min_signed) = false
        \/ Int.eq i2 Int.mone = false) ->
      eval_nbinop Odiv i1 i2 (Int.divs i1 i2)
    | eval_nbinop_Odivu : forall i1 i2,
      Int.eq i2 Int.zero = false ->
      eval_nbinop Odivu i1 i2 (Int.divu i1 i2)
    | eval_nbinop_Omod : forall i1 i2,
      Int.eq i2 Int.zero = false ->
      (Int.eq i1 (Int.repr Int.min_signed) = false \/
        Int.eq i2 Int.mone = false) ->
      eval_nbinop Omod i1 i2 (Int.mods i1 i2)
    | eval_nbinop_Omodu : forall i1 i2,
      Int.eq i2 Int.zero = false ->
      eval_nbinop Omodu i1 i2 (Int.modu i1 i2)
    | eval_nbinop_Oand : forall i1 i2,
      eval_nbinop Oand i1 i2 (Int.and i1 i2)
    | eval_nbinop_Oor : forall i1 i2,
      eval_nbinop Oor i1 i2 (Int.or i1 i2)
    | eval_nbinop_Oxor : forall i1 i2,
      eval_nbinop Oxor i1 i2 (Int.xor i1 i2)
    | eval_nbinop_Oshl_ok : forall i1 i2,
      Int.ltu i2 Int.iwordsize = true ->
      eval_nbinop Oshl i1 i2 (Int.shl i1 i2)
    | eval_nbinop_Oshl_ko : forall i1 i2 i,
      Int.ltu i2 Int.iwordsize = false ->
      eval_nbinop Oshl i1 i2 i
    | eval_nbinop_Oshr_ok : forall i1 i2,
      Int.ltu i2 Int.iwordsize = true ->
      eval_nbinop Oshr i1 i2 (Int.shr i1 i2)
    | eval_nbinop_Oshr_ko : forall i1 i2 i,
      Int.ltu i2 Int.iwordsize = false ->
      eval_nbinop Oshr i1 i2 i
    | eval_nbinop_Oshru_ok : forall i1 i2,
      Int.ltu i2 Int.iwordsize = true ->
      eval_nbinop Oshru i1 i2 (Int.shru i1 i2)
    | eval_nbinop_Oshru_ko : forall i1 i2 i,
      Int.ltu i2 Int.iwordsize = false ->
      eval_nbinop Oshru i1 i2 i
    | eval_nbinop_Ocmp : forall c i1 i2,
      eval_nbinop (Ocmp c) i1 i2 (of_bool (Int.cmp c i1 i2))
    | eval_nbinop_Ocmpu : forall c i1 i2,
      eval_nbinop (Ocmpu c) i1 i2 (of_bool (Int.cmpu c i1 i2)).

    Inductive eval_nexpr: nexpr -> int -> Prop :=
    | eval_NEvar: forall id i,
      ρ id = i ->
      eval_nexpr (NEvar id) i
    | eval_NEconst: forall cst i,
      eval_nconstant cst i ->
      eval_nexpr (NEconst cst) i
    | eval_NEunop: forall op a1 n1 n,
      eval_nexpr a1 n1 ->
      eval_nunop op n1 n ->
      eval_nexpr (NEunop op a1) n
    | eval_Ebinop: forall op a1 a2 n1 n2 n,
      eval_nexpr a1 n1 ->
      eval_nexpr a2 n2 ->
      eval_nbinop op n1 n2 n ->
      eval_nexpr (NEbinop op a1 a2) n
    | eval_NEcondition b bv r l k res:
      eval_nexpr b k ->
      (k <> Int.zero <-> bv = true) ->
      eval_nexpr (if bv then l else r) res ->
      eval_nexpr (NEcondition b l r) res
    .
    
  End eval_nexpr.

End nexpr.

Unset Elimination Schemes.
Class int_dom (var t: Type) `{EqDec var} : Type := {
  id_adom:> Adom.adom t (var->int);
  get_itv: nexpr var -> t -> sign_flag -> Interval.itv+⊥;
  assign: var -> nexpr var -> t -> t;
  assume: nexpr var -> t -> t;
  
  get_itv_correct: forall e ρ ab,
    ρ ∈ γ ab ->
    eval_nexpr ρ e ⊆ ints_in_range (get_itv e ab);
  assign_correct: forall x e ρ n ab,
    ρ ∈ γ ab ->
    n ∈ eval_nexpr ρ e ->
    (upd ρ x n) ∈ γ (assign x e ab);
  assume_correct: forall e ρ ab,
    ρ ∈ γ ab ->
    Ntrue ∈ eval_nexpr ρ e ->
    ρ ∈ γ (assume e ab)
}.