Module NoError

Require Import
  Utf8 Coqlib Util
  AST Globalenvs Maps
  Values Memory Integers Floats
  Cminor
  Csharpminor.

Set Implicit Arguments.

Section EEI.
Context (ge: genv) (e: env) (t: temp_env) (m: Mem.mem).

Lemma eval_expr_Evar_inv id v :
  eval_expr ge e t m (Evar id) v →
  t ! id = Some v.

Lemma eval_expr_Econst_inv c v :
  eval_expr ge e t m (Econst c) v →
  eval_constant c = Some v.

Lemma eval_expr_Eaddrof_inv id v :
  eval_expr ge e t m (Eaddrof id) v →
  ∃ b, eval_var_addr ge e id b ∧ v = Vptr b Int.zero.

Lemma eval_expr_Eunop_inv op a v :
  eval_expr ge e t m (Eunop op a) v →
  ∃ v', eval_expr ge e t m a v' ∧
        eval_unop op v' = Some v.

Lemma eval_expr_Ebinop_inv op a1 a2 v :
  eval_expr ge e t m (Ebinop op a1 a2) v →
  ∃ v1 v2,
    eval_expr ge e t m a1 v1 ∧
    eval_expr ge e t m a2 v2 ∧
    eval_binop op v1 v2 m = Some v.

Lemma eval_expr_Eload_inv κ a v :
  eval_expr ge e t m (Eload κ a) v →
  ∃ v', eval_expr ge e t m a v' ∧ Mem.loadv κ m v' = Some v.

End EEI.

Ltac eval_expr_inv :=
  repeat
  match goal with
  | H : eval_expr _ _ _ _ (Evar _) _ |- _ =>
    apply eval_expr_Evar_inv in H
  | H : eval_expr _ _ _ _ (Eaddrof _) _ |- _ =>
    apply eval_expr_Eaddrof_inv in H;
    let b := fresh "b" in
    let EQ := fresh "EQ" in
    destruct H as (b & H & EQ)
  | H : eval_expr _ _ _ _ (Econst _) _ |- _ =>
    apply eval_expr_Econst_inv in H
  | H : eval_expr _ _ _ _ (Eunop _ _) _ |- _ =>
    apply eval_expr_Eunop_inv in H;
    let v1 := fresh "v1" in
    destruct H as (v1 & ? & H)
  | H : eval_expr _ _ _ _ (Ebinop _ _ _) _ |- _ =>
    apply eval_expr_Ebinop_inv in H;
    let v1 := fresh "v1" in
    let v2 := fresh "v2" in
    destruct H as (v1 & v2 & ? & ? & H)
  | H : eval_expr _ _ _ _ (Eload _ _) _ |- _ =>
    apply eval_expr_Eload_inv in H;
    let v1 := fresh "v1" in
    destruct H as (v1 & ? & H)
  end.

Section GE.

Context (ge: genv) (e: env) (t: temp_env) (m: Mem.mem).

Let valid_ptr : block → Z → bool := Mem.valid_pointer m.
Let weak_valid_ptr := λ b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1).

Section B.
Local Unset Elimination Schemes.
Definition i_unop : unary_operation → Prop :=
  λ o, match o with
       | Ocast8unsigned
       | Ocast16unsigned
       | Ocast8signed
       | Ocast16signed
       | Onegint
       | Onotint
       | Ofloatofint
       | Ofloatofintu
       | Osingleofint
       | Osingleofintu
       | Olongofint
       | Olongofintu => True
       | _ => False
       end.

Definition f_unop : unary_operation → Prop :=
  λ o, match o with
       | Onegf
       | Oabsf
       | Osingleoffloat
       | Ointoffloat
       | Ointuoffloat
       | Olongoffloat
       | Olonguoffloat
         => True
       | _ => False
       end.

Definition s_unop : unary_operation → Prop :=
  λ o, match o with
       | Onegfs
       | Oabsfs
       | Ofloatofsingle
       | Ointofsingle
       | Ointuofsingle
       | Olongofsingle
       | Olonguofsingle
         => True
       | _ => False
       end.

Definition l_unop : unary_operation → Prop :=
  λ o, match o with
       | Ointoflong
       | Ofloatoflong
       | Ofloatoflongu
       | Osingleoflong
       | Osingleoflongu
       | Onegl
       | Onotl
         => True
       | _ => False
       end.

Inductive error_unop : unary_operation → val → Prop :=
| error_int o v :
    match v with Vint _ => False | _ => True end →
    i_unop o →
    error_unop o v
| error_float o v :
    match v with Vfloat _ => False | _ => True end →
    f_unop o →
    error_unop o v
| error_single o v :
    match v with Vsingle _ => False | _ => True end →
    s_unop o →
    error_unop o v
| error_long o v :
    match v with Vlong _ => False | _ => True end →
    l_unop o →
    error_unop o v
| error_Ointoffloat f :
    Float.to_int f = None →
    error_unop Ointoffloat (Vfloat f)
| error_Ointuoffloat f :
    Float.to_intu f = None →
    error_unop Ointuoffloat (Vfloat f)
| error_Olongoffloat f :
    Float.to_long f = None →
    error_unop Olongoffloat (Vfloat f)
| error_Olonguoffloat f :
    Float.to_longu f = None →
    error_unop Olonguoffloat (Vfloat f)
| error_Ointofsingle f :
    Float32.to_int f = None →
    error_unop Ointofsingle (Vsingle f)
| error_Ointuofsingle f :
    Float32.to_intu f = None →
    error_unop Ointuofsingle (Vsingle f)
| error_Olongofsingle f :
    Float32.to_long f = None →
    error_unop Olongofsingle (Vsingle f)
| error_Olonguofsingle f :
    Float32.to_longu f = None →
    error_unop Olonguofsingle (Vsingle f)
.

Inductive error_binop : binary_operation → val → val → Prop :=
| error_Oadd v w :
    match v, w with
      | Vint _, (Vint _ | Vptr _ _)
      | Vptr _ _, Vint _
        => False
      | _, _ => True
    end →
    error_binop Oadd v w
| error_Osub v w :
    match v, w with
      | (Vint _ | Vptr _ _), Vint _ => False
      | Vptr b _, Vptr b' _ => b ≠ b'
      | _, _ => True
    end →
    error_binop Osub v w
| error_int_int o v w :
    match v, w with
      | Vint _, Vint _ => False
      | _, _ => True
    end →
    match o with
    | Omul | Oand | Oor | Oxor | Odiv | Odivu | Omod | Omodu | Oshl | Oshr | Oshru | Ocmp _ => True
    | _ => False
    end →
    error_binop o v w
| error_float_float o v w :
    match v, w with
      | Vfloat _, Vfloat _ => False
      | _, _ => True
    end →
    match o with Oaddf | Osubf | Omulf | Odivf | Ocmpf _ => True | _ => False end →
    error_binop o v w
| error_single_single o v w :
    match v, w with
      | Vsingle _, Vsingle _ => False
      | _, _ => True
    end →
    match o with Oaddfs | Osubfs | Omulfs | Odivfs | Ocmpfs _ => True | _ => False end →
    error_binop o v w
| error_long_long o v w :
    match v, w with
    | Vlong _, Vlong _ => False
    | _, _ => True
    end →
    match o with
    | Oaddl | Osubl | Omull | Oandl | Oorl | Oxorl
    | Odivl | Odivlu | Omodl | Omodlu | Ocmpl _ | Ocmplu _ => True
    | _ => False end →
    error_binop o v w
| error_long_int o v w :
    match v, w with
      | Vlong _, Vint _ => False
      | _, _ => True
    end →
    match o with Oshll | Oshrl | Oshrlu => True | _ => False end →
    error_binop o v w
| error_Odiv_zero o i :
    match o with Odiv | Omod => True | _ => False end →
    error_binop o (Vint i) (Vint Int.zero)
| error_Odiv_min_s o :
    match o with Odiv | Omod => True | _ => False end →
    error_binop o (Vint (Int.repr Int.min_signed)) (Vint Int.mone)
| error_Odivu_zero o i :
    match o with Odivu | Omodu => True | _ => False end →
    error_binop o (Vint i) (Vint Int.zero)
| error_Oshift o i j :
    Int.ltu j Int.iwordsize = false →
    match o with Oshl | Oshr | Oshru => True | _ => False end →
    error_binop o (Vint i) (Vint j)
| error_Odivl_zero o l :
    match o with Odivl | Omodl => True | _ => False end →
    error_binop o (Vlong l) (Vlong Int64.zero)
| error_Odivl_min_s o :
    match o with Odivl | Omodl => True | _ => False end →
    error_binop o (Vlong (Int64.repr Int64.min_signed)) (Vlong Int64.mone)
| error_Odivlu_zero o l :
    match o with Odivlu | Omodlu => True | _ => False end →
    error_binop o (Vlong l) (Vlong Int64.zero)
| error_Oshiftl o l i :
    Int.ltu i Int64.iwordsize' = false →
    match o with Oshll | Oshrl | Oshrlu => True | _ => False end →
    error_binop o (Vlong l) (Vint i)
| error_Ocmpu c v w :
    match v, w with
      | Vint _, Vint _
      | Vint _, Vptr _ _
      | Vptr _ _, Vint _
      | Vptr _ _, Vptr _ _
        => False
      | _, _ => True
    end →
    error_binop (Ocmpu c) v w
| error_Ocmpu_ip_z c i b j :
    Int.eq i Int.zero = false →
    error_binop (Ocmpu c) (Vint i) (Vptr b j)
| error_Ocmpu_ip_invalid c i b j :
    weak_valid_ptr b (Int.unsigned j) = false →
    error_binop (Ocmpu c) (Vint i) (Vptr b j)
| error_Ocmpu_ip_cmp c i b j :
    match c with Ceq | Cne => False | _ => True end →
    error_binop (Ocmpu c) (Vint i) (Vptr b j)
| error_Ocmpu_pi_z c i b j :
    Int.eq i Int.zero = false →
    error_binop (Ocmpu c) (Vptr b j) (Vint i)
| error_Ocmpu_pi_invalid c i b j :
    weak_valid_ptr b (Int.unsigned j) = false →
    error_binop (Ocmpu c) (Vptr b j) (Vint i)
| error_Ocmpu_pi_cmp c i b j :
    match c with Ceq | Cne => False | _ => True end →
    error_binop (Ocmpu c) (Vptr b j) (Vint i)
| error_Ocmpu_pp_cmp c b i b' i' :
    match c with Ceq | Cne => False | _ => True end →
    b ≠ b' →
    error_binop (Ocmpu c) (Vptr b i) (Vptr b' i')
| error_Ocmpu_pp_invalid c b i b' i' :
    b ≠ b' →
    valid_ptr b (Int.unsigned i) = false ∨
    valid_ptr b' (Int.unsigned i') = false →
    error_binop (Ocmpu c) (Vptr b i) (Vptr b' i')
| error_Ocmpu_pp_winvalid c b i i' :
    weak_valid_ptr b (Int.unsigned i) = false ∨
    weak_valid_ptr b (Int.unsigned i') = false →
    error_binop (Ocmpu c) (Vptr b i) (Vptr b i')
.

Inductive error_load (κ: memory_chunk) : val → Prop :=
| error_load_not_ptr v :
    match v with Vptr _ _ => False | _ => True end →
    error_load κ v
| error_load_None b i :
    Mem.load κ m b (Int.unsigned i) = None →
    error_load κ (Vptr b i)
| error_load_undef b i :
    Mem.load κ m b (Int.unsigned i) = Some Vundef →
    error_load κ (Vptr b i)
.

End B.

Inductive error_expr : expr → Prop :=
| error_Evar_None i :
    t ! i = None →
    error_expr (Evar i)
| error_Evar_Vundef i :
    t ! i = Some Vundef →
    error_expr (Evar i)
| error_Eaddrof i :
    e ! i = None →
    Genv.find_symbol ge i = None →
    error_expr (Eaddrof i)
| error_Eunop u q v :
    eval_expr ge e t m q v →
    error_unop u v →
    error_expr (Eunop u q)
| error_Eunop_rec u q :
    error_expr q →
    error_expr (Eunop u q)
| error_Ebinop b q r v w :
    eval_expr ge e t m q v →
    eval_expr ge e t m r w →
    error_binop b v w →
    error_expr (Ebinop b q r)
| error_Ebinop_rec_l b q r :
    error_expr q →
    error_expr (Ebinop b q r)
| error_Ebinop_rec_r b q r v :
    eval_expr ge e t m q v →
    error_expr r →
    error_expr (Ebinop b q r)
| error_Eload κ q v :
    eval_expr ge e t m q v →
    error_load κ v →
    error_expr (Eload κ q)
| error_Eload_rec κ q :
    error_expr q →
    error_expr (Eload κ q)
.

Lemma error_expr_Unop_inv u q :
  error_expr (Eunop u q) →
  (∃ v, eval_expr ge e t m q v ∧ error_unop u v)
∨ (error_expr q).

Lemma error_expr_Binop_inv b q r :
  error_expr (Ebinop b q r) →
  (∃ v w, eval_expr ge e t m q v ∧ eval_expr ge e t m r w ∧ error_binop b v w)
∨ (error_expr q)
∨ (∃ v, eval_expr ge e t m q v ∧ error_expr r).

Lemma error_expr_Load_inv κ q :
  error_expr (Eload κ q) →
  (∃ v, eval_expr ge e t m q v ∧ error_load κ v)
∨ (error_expr q).

Lemma val_cmp_ii_def c i j :
  Val.cmp c (Vint i) (Vint j) = Vundef → False.
Lemma val_cmpf_ff_def c f g :
  Val.cmpf c (Vfloat f) (Vfloat g) = Vundef → False.
Lemma val_cmpfs_ss_def c f g :
  Val.cmpfs c (Vsingle f) (Vsingle g) = Vundef → False.
Lemma val_of_bool_def b :
  Val.of_bool b = Vundef → False.
Hint Resolve val_cmp_ii_def val_cmpf_ff_def val_cmpfs_ss_def val_of_bool_def.

Lemma noerror_def (q: expr) :
  ¬ error_expr q →
  ∀ v, eval_expr ge e t m q v → v ≠ Vundef.

Lemma noerror_eval_expr (q: expr) :
  ¬ error_expr q →
  ∃ v, eval_expr ge e t m q v.

Corollary noerror_eval_expr_def (q: expr) :
  ¬ error_expr q →
  ∃ v, v ≠ Vundef ∧ eval_expr ge e t m q v.

Section PE.

  Require Import PExpr.

  Context (var: Type) (ρ: var → val) (ε: ident → option block).

  Let eval_pexpr := eval_pexpr ge m ρ ε.

  Definition error_pbinop b v w :=
    match b, v, w with
    | Ocmpu _, Vptr _ _, Vint _
    | Ocmpu _, Vint _, Vptr _ _ => True
    | Ocmpu _, Vptr p i, Vptr q j =>
      p ≠ q ∨ Mem.weak_valid_pointer m p (Int.unsigned i) || Mem.weak_valid_pointer m q (Int.unsigned j) = false
    | _, _, _ => error_binop b v w
    end.

  Fixpoint error_pexpr (pe: pexpr var) : Prop :=
    match pe with
    | PEvar i _ => ρ(i) = Vundef
    | PElocal i => ε(i) = None
    | PEconst (Some (Oaddrsymbol s _)) _ =>
      Genv.find_symbol ge s = None
    | PEunop u q _ =>
      error_pexpr q ∨ ∃ v, eval_pexpr q v ∧ error_unop u v
    | PEbinop b q r _ =>
      error_pexpr q ∨
      ∃ v, eval_pexpr q v ∧
      (error_pexpr r ∨
       ∃ w, eval_pexpr r w ∧
            error_binop b v w)
    | _ => False
    end.

  Lemma error_pexpr_def (pe: pexpr var) :
    ¬ error_pexpr pe →
    ∀ v, eval_pexpr pe v → v ≠ Vundef.

End PE.

End GE.