Module Sexpr

Require Import Extra.
Require Op.
Import Utf8 Coqlib.
Import AST Globalenvs.
Import Integers Values.

Set Implicit Arguments.
Unset Elimination Schemes.
Local Coercion is_true : bool >-> Sortclass.

Section EVAL.
  Context (find_symbol: ident → option block) (sp: val).
  Definition symbol_address (s: ident) (o: int) : val :=
    match find_symbol s with
    | Some b => Vptr b o
    | None => Vundef
    end.
  Context (valid_pointer : block → Z → bool).

Definition eval_condition (cond: Op.condition) (args: list val) : option bool :=
  match cond, args with
  | Op.Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2
  | Op.Ccompu c, v1 :: v2 :: nil => Val.cmpu_bool valid_pointer c v1 v2
  | Op.Ccompimm c n, v1 :: nil => Val.cmp_bool c v1 (Vint n)
  | Op.Ccompuimm c n, v1 :: nil => Val.cmpu_bool valid_pointer c v1 (Vint n)
  | Op.Ccompf c, v1 :: v2 :: nil => Val.cmpf_bool c v1 v2
  | Op.Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2)
  | Op.Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2
  | Op.Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2)
  | Op.Cmaskzero n, v1 :: nil => Val.maskzero_bool v1 n
  | Op.Cmasknotzero n, v1 :: nil => option_map negb (Val.maskzero_bool v1 n)
  | _, _ => None
  end.

  Remark op_eval_condition m :
    (∀ b o, Memory.Mem.valid_pointer m b o = valid_pointer b o) →
    ∀ cond args,
      eval_condition cond args = Op.eval_condition cond args m.

Definition eval_addressing
    (addr: Op.addressing) (vl: list val) : option val :=
  match addr, vl with
  | Op.Aindexed n, v1::nil =>
      Some (Val.add v1 (Vint n))
  | Op.Aindexed2 n, v1::v2::nil =>
      Some (Val.add (Val.add v1 v2) (Vint n))
  | Op.Ascaled sc ofs, v1::nil =>
      Some (Val.add (Val.mul v1 (Vint sc)) (Vint ofs))
  | Op.Aindexed2scaled sc ofs, v1::v2::nil =>
      Some(Val.add v1 (Val.add (Val.mul v2 (Vint sc)) (Vint ofs)))
  | Op.Aglobal s ofs, nil =>
      Some (symbol_address s ofs)
  | Op.Abased s ofs, v1::nil =>
      Some (Val.add (symbol_address s ofs) v1)
  | Op.Abasedscaled sc s ofs, v1::nil =>
      Some (Val.add (symbol_address s ofs) (Val.mul v1 (Vint sc)))
  | Op.Ainstack ofs, nil =>
      Some(Val.add sp (Vint ofs))
  | _, _ => None
  end.


Definition eval_operation (op: Op.operation) (args: list val) : option val :=
  match op, args with
  | Op.Omove, v1::nil => Some v1
  | Op.Ointconst n, nil => Some (Vint n)
  | Op.Ofloatconst n, nil => Some (Vfloat n)
  | Op.Osingleconst n, nil => Some (Vsingle n)
  | Op.Oindirectsymbol id, nil => Some (symbol_address id Int.zero)
  | Op.Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1)
  | Op.Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1)
  | Op.Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1)
  | Op.Ocast16unsigned, v1 :: nil => Some (Val.zero_ext 16 v1)
  | Op.Oneg, v1::nil => Some (Val.neg v1)
  | Op.Osub, v1::v2::nil => Some (Val.sub v1 v2)
  | Op.Omul, v1::v2::nil => Some (Val.mul v1 v2)
  | Op.Omulimm n, v1::nil => Some (Val.mul v1 (Vint n))
  | Op.Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2)
  | Op.Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2)
  | Op.Odiv, v1::v2::nil => Val.divs v1 v2
  | Op.Odivu, v1::v2::nil => Val.divu v1 v2
  | Op.Omod, v1::v2::nil => Val.mods v1 v2
  | Op.Omodu, v1::v2::nil => Val.modu v1 v2
  | Op.Oand, v1::v2::nil => Some(Val.and v1 v2)
  | Op.Oandimm n, v1::nil => Some (Val.and v1 (Vint n))
  | Op.Oor, v1::v2::nil => Some(Val.or v1 v2)
  | Op.Oorimm n, v1::nil => Some (Val.or v1 (Vint n))
  | Op.Oxor, v1::v2::nil => Some(Val.xor v1 v2)
  | Op.Oxorimm n, v1::nil => Some (Val.xor v1 (Vint n))
  | Op.Onot, v1::nil => Some(Val.notint v1)
  | Op.Oshl, v1::v2::nil => Some (Val.shl v1 v2)
  | Op.Oshlimm n, v1::nil => Some (Val.shl v1 (Vint n))
  | Op.Oshr, v1::v2::nil => Some (Val.shr v1 v2)
  | Op.Oshrimm n, v1::nil => Some (Val.shr v1 (Vint n))
  | Op.Oshrximm n, v1::nil => Val.shrx v1 (Vint n)
  | Op.Oshru, v1::v2::nil => Some (Val.shru v1 v2)
  | Op.Oshruimm n, v1::nil => Some (Val.shru v1 (Vint n))
  | Op.Ororimm n, v1::nil => Some (Val.ror v1 (Vint n))
  | Op.Oshldimm n, v1::v2::nil => Some (Val.or (Val.shl v1 (Vint n))
                                               (Val.shru v2 (Vint (Int.sub Int.iwordsize n))))
  | Op.Olea addr, _ => eval_addressing addr args
  | Op.Onegf, v1::nil => Some(Val.negf v1)
  | Op.Oabsf, v1::nil => Some(Val.absf v1)
  | Op.Oaddf, v1::v2::nil => Some(Val.addf v1 v2)
  | Op.Osubf, v1::v2::nil => Some(Val.subf v1 v2)
  | Op.Omulf, v1::v2::nil => Some(Val.mulf v1 v2)
  | Op.Odivf, v1::v2::nil => Some(Val.divf v1 v2)
  | Op.Onegfs, v1::nil => Some(Val.negfs v1)
  | Op.Oabsfs, v1::nil => Some(Val.absfs v1)
  | Op.Oaddfs, v1::v2::nil => Some(Val.addfs v1 v2)
  | Op.Osubfs, v1::v2::nil => Some(Val.subfs v1 v2)
  | Op.Omulfs, v1::v2::nil => Some(Val.mulfs v1 v2)
  | Op.Odivfs, v1::v2::nil => Some(Val.divfs v1 v2)
  | Op.Osingleoffloat, v1::nil => Some(Val.singleoffloat v1)
  | Op.Ofloatofsingle, v1::nil => Some(Val.floatofsingle v1)
  | Op.Ointoffloat, v1::nil => Val.intoffloat v1
  | Op.Ofloatofint, v1::nil => Val.floatofint v1
  | Op.Ointofsingle, v1::nil => Val.intofsingle v1
  | Op.Osingleofint, v1::nil => Val.singleofint v1
  | Op.Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2)
  | Op.Olowlong, v1::nil => Some(Val.loword v1)
  | Op.Ohighlong, v1::nil => Some(Val.hiword v1)
  | Op.Ocmp c, _ => Some(Val.of_optbool (eval_condition c args))
  | _, _ => None
  end.


End EVAL.

Section REGISTER.

Variable reg : Type.
Context (reg_dec: EqDec reg).

Inductive sexpr :=
| Reg `(reg)
| Name `(ident)
| Oper (op: Op.operation) (args: list sexpr)
.

Theorem sexpr_ind (P: sexpr → Prop) :
  (∀ r, P (Reg r)) →
  (∀ n, P (Name n)) →
  (∀ op args, (∀ a, In a args → P a) → P (Oper op args)) →
  ∀ e, P e.

Instance sexpr_dec : EqDec sexpr.

  Definition oper op args : sexpr :=
  match op, args with
  | Op.Omove, a :: nil => a
  | Op.Osub, x :: Oper (Op.Ointconst n) nil :: nil =>
    Oper (Op.Olea (Op.Aindexed (Int.neg n))) (x :: nil)
  | _, _ => Oper op args
  end.

  Fixpoint map_sexpr fr (e: sexpr) : sexpr :=
    match e with
    | Reg r => fr r e
    | Name _ => e
    | Oper op args => oper op (List.map (map_sexpr fr) args)
    end.

  Definition subst_reg (r: reg) (n: sexpr) (e: sexpr) : sexpr :=
    map_sexpr (λ x e, if reg_dec x r then n else e) e.

  Definition comp {X} c (f: X → reg) a : sexpr :=
    oper (Op.Ocmp c) (List.map (λ r, Reg (f r)) a).

  Definition addr {X} p (f: X → reg) a : sexpr :=
    oper (Op.Olea p) (List.map (λ r, Reg (f r)) a).

  Set Elimination Schemes.
  Inductive assertion : Type :=
  | True
  | Assert `(sexpr)
  | AssertEQ (_ _: sexpr)
  | Implies (_ _: assertion)
  | Negate `(assertion)
  | ForAll `(reg) `(assertion)
  .

  Global Instance assertion_eq_dec : EqDec assertion.
  
  Fixpoint is_free (x: reg) (e: sexpr) {struct e} : bool :=
    match e with
    | Reg r => reg_dec r x
    | Name _ => false
    | Oper _ args => list_exists (is_free x) args
    end.

  Fixpoint is_free' (x: reg) (a: assertion) : bool :=
    match a with
    | True => false
    | Assert e => is_free x e
    | AssertEQ e e' => if is_free x e then true else is_free x e'
    | Implies p q => if is_free' x p then true else is_free' x q
    | Negate p => is_free' x p
    | ForAll x' p => if reg_dec x' x then false else is_free' x p
    end.

  Variable (reg_max: reg → reg → reg).

  Fixpoint sexpr_max_reg (m: reg) (e: sexpr) : reg :=
    match e with
    | Reg r => reg_max r m
    | Name _ => m
    | Oper _ args => List.fold_left sexpr_max_reg args m
    end.

  Fixpoint assertion_max_reg (m: reg) (a: assertion) : reg :=
    match a with
    | True => m
    | Assert e => sexpr_max_reg m e
    | AssertEQ x y => sexpr_max_reg (sexpr_max_reg m x) y
    | Implies p q => assertion_max_reg (assertion_max_reg m p) q
    | Negate p => assertion_max_reg m p
    | ForAll x p => assertion_max_reg (reg_max x m) p
    end.

  Lemma pos_max_le : ∀ x y z, Pos.le z x ∨ Pos.le z y → Pos.le z (Pos.max x y).

  Lemma pos_succ_le_ne : ∀ x y, Pos.le x y → x ≠ Pos.succ y.

  Variable reg_succ: reg → reg.
  Variable (reg_le: reg → reg → Prop).
  Hypothesis reg_le_refl : ∀ x, reg_le x x.
  Hypothesis reg_le_trans : ∀ x y z, reg_le x y → reg_le y z → reg_le x z.
  Hypothesis reg_max_le : ∀ x y z, reg_le z x ∨ reg_le z y → reg_le z (reg_max x y).
  Hypothesis reg_succ_le_ne : ∀ x y, reg_le x y → x ≠ reg_succ y.

  Lemma sexpr_max_reg_le e :
    ∀ r x, is_free x e ∨ reg_le x r → reg_le x (sexpr_max_reg r e).
  Arguments sexpr_max_reg_le : clear implicits.

  Lemma assertion_max_reg_le a :
    ∀ r x, is_free' x a ∨ reg_le x r → reg_le x (assertion_max_reg r a).
  Arguments assertion_max_reg_le : clear implicits.

  Definition fresh (r : reg) (e : sexpr) (a: assertion) : reg :=
    reg_succ (assertion_max_reg (sexpr_max_reg r e) a).

  Lemma fresh_correct r e a :
    let x := fresh r e a in
    x ≠ r ∧ is_free x e = false ∧ is_free' x a = false.
  Opaque fresh.

  Fixpoint assign_measure (a: assertion) : nat :=
    match a with
    | True
    | Assert _
    | AssertEQ _ _ => O
    | Implies p q => S (Peano.max (assign_measure p) (assign_measure q))
    | ForAll _ p
    | Negate p => S (assign_measure p)
    end.

  Definition assign_rel x y : Prop :=
    (assign_measure x < assign_measure y)%nat.

  Definition assign_rel_w x y : bool :=
    NPeano.leb (assign_measure y) (assign_measure x).

  Remark assign_rel_wf : well_founded assign_rel.

  Fixpoint assign (r: reg) (n: sexpr) (a: assertion) (H: Acc assign_rel a) {struct H} : sig (assign_rel_w a).
  refine (
    let 'Acc_intro H'' := H in
    match a return (∀ y : assertion, assign_rel y a → Acc assign_rel y) → sig (assign_rel_w a) with
    | True => λ H', exist _ True _
    | Assert e => λ H', exist _ (Assert (subst_reg r n e)) _
    | AssertEQ x y => λ H', exist _ (AssertEQ (subst_reg r n x) (subst_reg r n y)) _
    | Implies p q =>
      λ H',
      let 'exist p' Hp' := assign r n p _ in
      let 'exist q' Hq' := assign r n q _ in
      exist _ (Implies p' q') _
    | Negate p =>
      λ H',
      let 'exist p' Hp' := assign r n p _ in
      exist _ (Negate p') _
    | ForAll x p =>
      λ H',
      if reg_dec x r
      then exist _ (ForAll x p) _
      else
        if is_free x n
        then
          let x' := fresh r n p in
          let 'exist p' Hp' := assign x (Reg x') p _ in
          let 'exist q Hq := assign r n p' _ in
          exist _ (ForAll x' q) _
        else
          let 'exist q Hq := assign r n p _ in
          exist _ (ForAll x q) _
    end H'');
    try exact eq_refl.

  Definition assign' r n a :=
    if is_free' r a
    then proj1_sig (@assign r n a (assign_rel_wf a))
    else a.

  Definition assert_eq_reg (p q: reg) : assertion :=
    AssertEQ (Reg p) (Reg q).

  Definition boolexpr c x :=
      let cnz := Op.Ccompuimm Cne Int.zero in
      if Op.eq_condition c cnz
      then x
      else oper (Op.Ocmp cnz) (x :: nil).

  Definition assert_iff (x x': sexpr) : option assertion :=
    match x, x' with
    | Oper (Op.Ocmp c) _, Oper (Op.Ocmp c') _ =>
      Some (AssertEQ (boolexpr c x) (boolexpr c' x'))
    | _, _ => None
    end.

  Context (find_symbol: ident → option block) (sp: val).
  Let env : Type := reg → val.

  Section EVAL.
  Context (valid_pointer : block → Z → bool).
  Context (ε: env).

  Fixpoint eval_sexpr (e: sexpr) : option val :=
    match e with
    | Reg x => Some (ε x)
    | Name n =>
      do b <- find_symbol n;
      Some (Vptr b Int.zero)
    | Oper op args =>
      do vargs <- map_o eval_sexpr args;
      eval_operation find_symbol sp valid_pointer op vargs
    end.

  Lemma oper_eval op args :
    eval_sexpr (oper op args) = eval_sexpr (Oper op args).

  Lemma eval_boolexpr {X} cond (f: X → _) args :
    eval_sexpr (boolexpr cond (comp cond f args)) = Some (Val.of_optbool (eval_condition valid_pointer cond (map ε (map f args)))).


  End EVAL.

  Lemma eval_condition_m vp' vp cond args :
    (∀ b o, vp b o = vp' b o) →
    eval_condition vp cond args = eval_condition vp' cond args.

  Lemma eval_operation_m vp' vp op args :
    (∀ b o, vp b o = vp' b o) →
    eval_operation find_symbol sp vp op args = eval_operation find_symbol sp vp' op args.

  Fixpoint eval_assertion vp (ε: env) (a: assertion) : Prop :=
    match a with
    | True => Logic.True
    | Assert b =>
      eval_sexpr vp ε b = Some Vtrue
    | AssertEQ x x' => eval_sexpr vp ε x = eval_sexpr vp ε x'
    | Implies x y => eval_assertion vp ε x → eval_assertion vp ε y
    | Negate x => ¬ eval_assertion vp ε x
    | ForAll k x => ∀ v, eval_assertion vp (ε +[ k => v ]) x
    end.


  Fixpoint simplify_measure (a: assertion) : nat :=
    match a with
    | True
    | Assert _
    | AssertEQ _ _ => O
    | ForAll _ p
    | Implies _ p => S (simplify_measure p)
    | Negate p => simplify_measure p
    end.

  Fixpoint simplify_measure_assign r e p H :
    simplify_measure (proj1_sig (@assign r e p H)) = simplify_measure p.

  Corollary simplify_measure_assign' r e p :
    simplify_measure (assign' r e p) = simplify_measure p.

  Function simplify (a: assertion) {measure simplify_measure a} : assertion :=
    match a with
    | Assert e => a
    | AssertEQ x y => if sexpr_dec x y then True else a
    | Implies (AssertEQ (Reg r) e) p => simplify (assign' r e p)
    | Implies _ p => match simplify p with True => True | _ => a end
    | ForAll _ p => match simplify p with True => True | _ => a end
    | _ => a
    end.

  Lemma eval_sexpr_m {ε ε': env} :
    (∀ r, ε r = ε' r) →
    ∀ vp e, eval_sexpr vp ε e = eval_sexpr vp ε' e.

  Lemma eval_assertion_m {ε ε': env} :
    (∀ r, ε r = ε' r) →
    ∀ vp p, eval_assertion vp ε p ↔ eval_assertion vp ε' p.

  Lemma map_simpl {A B} (f: A → B) (m: list A) :
    map f m = match m with nil => nil | a :: m' => f a :: map f m' end.

  Lemma map_o_simpl {A B} (f: A → option B) (m: list A) :
    map_o f m = match m with nil => Some nil | a :: m' => do b <- f a; do bs <- map_o f m'; Some (b :: bs) end.

  Lemma eval_subst_reg {vp ε e v} :
    eval_sexpr vp ε e = Some v →
    ∀ r e',
    eval_sexpr vp ε (subst_reg r e e') = eval_sexpr vp (ε +[r => v]) e'.

  Lemma upd_stutter {A B} `{EqDec A} (f: A → B) x v v' y :
    f +[x => v'] +[x => v] y = f +[x => v] y.

  Lemma upd_comm {A B} `{EqDec A} (f: A → B) x v x' v' :
    x ≠ x' →
    ∀ y,
    f +[x' => v'] +[x => v] y = f +[x => v] +[x' => v'] y.

  Lemma eval_sexpr_is_free x e :
    is_free x e = false →
    ∀ vp ε v, eval_sexpr vp (ε +[x => v]) e = eval_sexpr vp ε e.

  Lemma eval_assertion_is_free x a :
    is_free' x a = false →
    ∀ vp ε v, eval_assertion vp (ε +[x => v]) a ↔ eval_assertion vp ε a.

  Section S.
  Context (vp : block → Z → bool).
  Fixpoint eval_assertion_assign r e p H :
    ∀ ε v,
      eval_sexpr vp ε e = Some v →
      (eval_assertion vp ε (proj1_sig (@assign r e p H)) ↔ eval_assertion vp (ε+[ r => v]) p).
  End S.

  Corollary eval_assertion_assign' vp ε r e p :
    ∀ v,
      eval_sexpr vp ε e = Some v →
      (eval_assertion vp ε (assign' r e p) ↔ eval_assertion vp (ε+[ r => v]) p).

  Lemma simplify_correct a :
    ∀ vp ε, eval_assertion vp ε (simplify a) → eval_assertion vp ε a.

End REGISTER.

Arguments Reg {reg} _.
Arguments Name {reg} _.
Arguments True {reg}.