Require Import Axioms.
Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import AST.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Ctypes.
Require Import Cop.
Require Import Csyntax.
Require Import Csem.

Section STRATEGY.

Variable ge: genv.

Definition of the strategy

Fixpoint simple (a: expr) : bool :=
  match a with
  | Eloc _ _ _ => true
  | Evar _ _ => true
  | Ederef r _ => simple r
  | Efield r _ _ => simple r
  | Eval _ _ => true
  | Evalof l _ => simple l && negb(type_is_volatile (typeof l))
  | Eaddrof l _ => simple l
  | Eunop _ r1 _ => simple r1
  | Ebinop _ r1 r2 _ => simple r1 && simple r2
  | Ecast r1 _ => simple r1
  | Eseqand _ _ _ => false
  | Eseqor _ _ _ => false
  | Econdition _ _ _ _ => false
  | Esizeof _ _ => true
  | Ealignof _ _ => true
  | Eassign _ _ _ => false
  | Eassignop _ _ _ _ _ => false
  | Epostincr _ _ _ => false
  | Ecomma _ _ _ => false
  | Ecall _ _ _ => false
  | Ebuiltin _ _ _ _ => false
  | Eparen _ _ _ => false
  end.

Fixpoint simplelist (rl: exprlist) : bool :=
  match rl with Enil => true | Econs r rl' => simple r && simplelist rl' end.


Section SIMPLE_EXPRS.

Variable e: env.
Variable m: mem.

Inductive eval_simple_lvalue: expr -> block -> int -> Prop :=
  | esl_loc: forall b ofs ty,
      eval_simple_lvalue (Eloc b ofs ty) b ofs
  | esl_var_local: forall x ty b,
      e!x = Some(b, ty) ->
      eval_simple_lvalue (Evar x ty) b Int.zero
  | esl_var_global: forall x ty b,
      e!x = None ->
      Genv.find_symbol ge x = Some b ->
      eval_simple_lvalue (Evar x ty) b Int.zero
  | esl_deref: forall r ty b ofs,
      eval_simple_rvalue r (Vptr b ofs) ->
      eval_simple_lvalue (Ederef r ty) b ofs
  | esl_field_struct: forall r f ty b ofs id co a delta,
      eval_simple_rvalue r (Vptr b ofs) ->
      typeof r = Tstruct id a ->
      ge.(genv_cenv)!id = Some co ->
      field_offset ge f (co_members co) = OK delta ->
      eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta))
  | esl_field_union: forall r f ty b ofs id co a,
      eval_simple_rvalue r (Vptr b ofs) ->
      typeof r = Tunion id a ->
      ge.(genv_cenv)!id = Some co ->
      eval_simple_lvalue (Efield r f ty) b ofs

with eval_simple_rvalue: expr -> val -> Prop :=
  | esr_val: forall v ty,
      eval_simple_rvalue (Eval v ty) v
  | esr_rvalof: forall b ofs l ty v,
      eval_simple_lvalue l b ofs ->
      ty = typeof l -> type_is_volatile ty = false ->
      deref_loc ge ty m b ofs E0 v ->
      eval_simple_rvalue (Evalof l ty) v
  | esr_addrof: forall b ofs l ty,
      eval_simple_lvalue l b ofs ->
      eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs)
  | esr_unop: forall op r1 ty v1 v,
      eval_simple_rvalue r1 v1 ->
      sem_unary_operation op v1 (typeof r1) m = Some v ->
      eval_simple_rvalue (Eunop op r1 ty) v
  | esr_binop: forall op r1 r2 ty v1 v2 v,
      eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 ->
      sem_binary_operation ge op v1 (typeof r1) v2 (typeof r2) m = Some v ->
      eval_simple_rvalue (Ebinop op r1 r2 ty) v
  | esr_cast: forall ty r1 v1 v,
      eval_simple_rvalue r1 v1 ->
      sem_cast v1 (typeof r1) ty = Some v ->
      eval_simple_rvalue (Ecast r1 ty) v
  | esr_sizeof: forall ty1 ty,
      eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1)))
  | esr_alignof: forall ty1 ty,
      eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))).

Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop :=
  | esrl_nil:
      eval_simple_list Enil Tnil nil
  | esrl_cons: forall r rl ty tyl v vl v',
      eval_simple_rvalue r v' -> sem_cast v' (typeof r) ty = Some v ->
      eval_simple_list rl tyl vl ->
      eval_simple_list (Econs r rl) (Tcons ty tyl) (v :: vl).

Scheme eval_simple_rvalue_ind2 := Minimality for eval_simple_rvalue Sort Prop
  with eval_simple_lvalue_ind2 := Minimality for eval_simple_lvalue Sort Prop.
Combined Scheme eval_simple_rvalue_lvalue_ind from eval_simple_rvalue_ind2, eval_simple_lvalue_ind2.

End SIMPLE_EXPRS.


Inductive leftcontext: kind -> kind -> (expr -> expr) -> Prop :=
  | lctx_top: forall k,
      leftcontext k k (fun x => x)
  | lctx_deref: forall k C ty,
      leftcontext k RV C -> leftcontext k LV (fun x => Ederef (C x) ty)
  | lctx_field: forall k C f ty,
      leftcontext k RV C -> leftcontext k LV (fun x => Efield (C x) f ty)
  | lctx_rvalof: forall k C ty,
      leftcontext k LV C -> leftcontext k RV (fun x => Evalof (C x) ty)
  | lctx_addrof: forall k C ty,
      leftcontext k LV C -> leftcontext k RV (fun x => Eaddrof (C x) ty)
  | lctx_unop: forall k C op ty,
      leftcontext k RV C -> leftcontext k RV (fun x => Eunop op (C x) ty)
  | lctx_binop_left: forall k C op e2 ty,
      leftcontext k RV C -> leftcontext k RV (fun x => Ebinop op (C x) e2 ty)
  | lctx_binop_right: forall k C op e1 ty,
      simple e1 = true -> leftcontext k RV C ->
      leftcontext k RV (fun x => Ebinop op e1 (C x) ty)
  | lctx_cast: forall k C ty,
      leftcontext k RV C -> leftcontext k RV (fun x => Ecast (C x) ty)
  | lctx_seqand: forall k C r2 ty,
      leftcontext k RV C -> leftcontext k RV (fun x => Eseqand (C x) r2 ty)
  | lctx_seqor: forall k C r2 ty,
      leftcontext k RV C -> leftcontext k RV (fun x => Eseqor (C x) r2 ty)
  | lctx_condition: forall k C r2 r3 ty,
      leftcontext k RV C -> leftcontext k RV (fun x => Econdition (C x) r2 r3 ty)
  | lctx_assign_left: forall k C e2 ty,
      leftcontext k LV C -> leftcontext k RV (fun x => Eassign (C x) e2 ty)
  | lctx_assign_right: forall k C e1 ty,
      simple e1 = true -> leftcontext k RV C ->
      leftcontext k RV (fun x => Eassign e1 (C x) ty)
  | lctx_assignop_left: forall k C op e2 tyres ty,
      leftcontext k LV C -> leftcontext k RV (fun x => Eassignop op (C x) e2 tyres ty)
  | lctx_assignop_right: forall k C op e1 tyres ty,
      simple e1 = true -> leftcontext k RV C ->
      leftcontext k RV (fun x => Eassignop op e1 (C x) tyres ty)
  | lctx_postincr: forall k C id ty,
      leftcontext k LV C -> leftcontext k RV (fun x => Epostincr id (C x) ty)
  | lctx_call_left: forall k C el ty,
      leftcontext k RV C -> leftcontext k RV (fun x => Ecall (C x) el ty)
  | lctx_call_right: forall k C e1 ty,
      simple e1 = true -> leftcontextlist k C ->
      leftcontext k RV (fun x => Ecall e1 (C x) ty)
  | lctx_builtin: forall k C ef tyargs ty,
      leftcontextlist k C ->
      leftcontext k RV (fun x => Ebuiltin ef tyargs (C x) ty)
  | lctx_comma: forall k C e2 ty,
      leftcontext k RV C -> leftcontext k RV (fun x => Ecomma (C x) e2 ty)
  | lctx_paren: forall k C tycast ty,
      leftcontext k RV C -> leftcontext k RV (fun x => Eparen (C x) tycast ty)

with leftcontextlist: kind -> (expr -> exprlist) -> Prop :=
  | lctx_list_head: forall k C el,
      leftcontext k RV C -> leftcontextlist k (fun x => Econs (C x) el)
  | lctx_list_tail: forall k C e1,
      simple e1 = true -> leftcontextlist k C ->
      leftcontextlist k (fun x => Econs e1 (C x)).

Lemma leftcontext_context:
  forall k1 k2 C, leftcontext k1 k2 C -> context k1 k2 C
with leftcontextlist_contextlist:
  forall k C, leftcontextlist k C -> contextlist k C.

Hint Resolve leftcontext_context.


Inductive estep: state -> trace -> state -> Prop :=

  | step_expr: forall f r k e m v ty,
      eval_simple_rvalue e m r v ->
      match r with Eval _ _ => False | _ => True end ->
      ty = typeof r ->
      estep (ExprState f r k e m)
         E0 (ExprState f (Eval v ty) k e m)

  | step_rvalof_volatile: forall f C l ty k e m b ofs t v,
      leftcontext RV RV C ->
      eval_simple_lvalue e m l b ofs ->
      deref_loc ge ty m b ofs t v ->
      ty = typeof l -> type_is_volatile ty = true ->
      estep (ExprState f (C (Evalof l ty)) k e m)
          t (ExprState f (C (Eval v ty)) k e m)

  | step_seqand_true: forall f C r1 r2 ty k e m v,
      leftcontext RV RV C ->
      eval_simple_rvalue e m r1 v ->
      bool_val v (typeof r1) m = Some true ->
      estep (ExprState f (C (Eseqand r1 r2 ty)) k e m)
         E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m)
  | step_seqand_false: forall f C r1 r2 ty k e m v,
      leftcontext RV RV C ->
      eval_simple_rvalue e m r1 v ->
      bool_val v (typeof r1) m = Some false ->
      estep (ExprState f (C (Eseqand r1 r2 ty)) k e m)
         E0 (ExprState f (C (Eval (Vint Int.zero) ty)) k e m)

  | step_seqor_true: forall f C r1 r2 ty k e m v,
      leftcontext RV RV C ->
      eval_simple_rvalue e m r1 v ->
      bool_val v (typeof r1) m = Some true ->
      estep (ExprState f (C (Eseqor r1 r2 ty)) k e m)
         E0 (ExprState f (C (Eval (Vint Int.one) ty)) k e m)
  | step_seqor_false: forall f C r1 r2 ty k e m v,
      leftcontext RV RV C ->
      eval_simple_rvalue e m r1 v ->
      bool_val v (typeof r1) m = Some false ->
      estep (ExprState f (C (Eseqor r1 r2 ty)) k e m)
         E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m)

  | step_condition: forall f C r1 r2 r3 ty k e m v b,
      leftcontext RV RV C ->
      eval_simple_rvalue e m r1 v ->
      bool_val v (typeof r1) m = Some b ->
      estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m)
         E0 (ExprState f (C (Eparen (if b then r2 else r3) ty ty)) k e m)

  | step_assign: forall f C l r ty k e m b ofs v v' t m',
      leftcontext RV RV C ->
      eval_simple_lvalue e m l b ofs ->
      eval_simple_rvalue e m r v ->
      sem_cast v (typeof r) (typeof l) = Some v' ->
      assign_loc ge (typeof l) m b ofs v' t m' ->
      ty = typeof l ->
      estep (ExprState f (C (Eassign l r ty)) k e m)
          t (ExprState f (C (Eval v' ty)) k e m')

  | step_assignop: forall f C op l r tyres ty k e m b ofs v1 v2 v3 v4 t1 t2 m' t,
      leftcontext RV RV C ->
      eval_simple_lvalue e m l b ofs ->
      deref_loc ge (typeof l) m b ofs t1 v1 ->
      eval_simple_rvalue e m r v2 ->
      sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m = Some v3 ->
      sem_cast v3 tyres (typeof l) = Some v4 ->
      assign_loc ge (typeof l) m b ofs v4 t2 m' ->
      ty = typeof l ->
      t = t1 ** t2 ->
      estep (ExprState f (C (Eassignop op l r tyres ty)) k e m)
          t (ExprState f (C (Eval v4 ty)) k e m')

  | step_assignop_stuck: forall f C op l r tyres ty k e m b ofs v1 v2 t,
      leftcontext RV RV C ->
      eval_simple_lvalue e m l b ofs ->
      deref_loc ge (typeof l) m b ofs t v1 ->
      eval_simple_rvalue e m r v2 ->
      match sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m with
      | None => True
      | Some v3 =>
          match sem_cast v3 tyres (typeof l) with
          | None => True
          | Some v4 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v4 t2 m')
          end
      end ->
      ty = typeof l ->
      estep (ExprState f (C (Eassignop op l r tyres ty)) k e m)
          t Stuckstate

  | step_postincr: forall f C id l ty k e m b ofs v1 v2 v3 t1 t2 m' t,
      leftcontext RV RV C ->
      eval_simple_lvalue e m l b ofs ->
      deref_loc ge ty m b ofs t1 v1 ->
      sem_incrdecr ge id v1 ty = Some v2 ->
      sem_cast v2 (incrdecr_type ty) ty = Some v3 ->
      assign_loc ge ty m b ofs v3 t2 m' ->
      ty = typeof l ->
      t = t1 ** t2 ->
      estep (ExprState f (C (Epostincr id l ty)) k e m)
          t (ExprState f (C (Eval v1 ty)) k e m')

  | step_postincr_stuck: forall f C id l ty k e m b ofs v1 t,
      leftcontext RV RV C ->
      eval_simple_lvalue e m l b ofs ->
      deref_loc ge ty m b ofs t v1 ->
      match sem_incrdecr ge id v1 ty with
      | None => True
      | Some v2 =>
          match sem_cast v2 (incrdecr_type ty) ty with
          | None => True
          | Some v3 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v3 t2 m')
          end
      end ->
      ty = typeof l ->
      estep (ExprState f (C (Epostincr id l ty)) k e m)
          t Stuckstate

  | step_comma: forall f C r1 r2 ty k e m v,
      leftcontext RV RV C ->
      eval_simple_rvalue e m r1 v ->
      ty = typeof r2 ->
      estep (ExprState f (C (Ecomma r1 r2 ty)) k e m)
         E0 (ExprState f (C r2) k e m)

  | step_paren: forall f C r tycast ty k e m v1 v,
      leftcontext RV RV C ->
      eval_simple_rvalue e m r v1 ->
      sem_cast v1 (typeof r) tycast = Some v ->
      estep (ExprState f (C (Eparen r tycast ty)) k e m)
         E0 (ExprState f (C (Eval v ty)) k e m)

  | step_call: forall f C rf rargs ty k e m targs tres cconv vf vargs fd,
      leftcontext RV RV C ->
      classify_fun (typeof rf) = fun_case_f targs tres cconv ->
      eval_simple_rvalue e m rf vf ->
      eval_simple_list e m rargs targs vargs ->
      Genv.find_funct ge vf = Some fd ->
      type_of_fundef fd = Tfunction targs tres cconv ->
      estep (ExprState f (C (Ecall rf rargs ty)) k e m)
         E0 (Callstate fd vargs (Kcall f e C ty k) m)

  | step_builtin: forall f C ef tyargs rargs ty k e m vargs t vres m',
      leftcontext RV RV C ->
      eval_simple_list e m rargs tyargs vargs ->
      external_call ef ge vargs m t vres m' ->
      estep (ExprState f (C (Ebuiltin ef tyargs rargs ty)) k e m)
          t (ExprState f (C (Eval vres ty)) k e m').

Definition step (S: state) (t: trace) (S': state) : Prop :=
  estep S t S' \/ sstep ge S t S'.


Lemma context_compose:
  forall k2 k3 C2, context k2 k3 C2 ->
  forall k1 C1, context k1 k2 C1 ->
  context k1 k3 (fun x => C2(C1 x))
with contextlist_compose:
  forall k2 C2, contextlist k2 C2 ->
  forall k1 C1, context k1 k2 C1 ->
  contextlist k1 (fun x => C2(C1 x)).

Hint Constructors context contextlist.
Hint Resolve context_compose contextlist_compose.

Safe executions.

Definition safe (s: Csem.state) : Prop :=
  forall s', star Csem.step ge s E0 s' ->
  (exists r, final_state s' r) \/ (exists t, exists s'', Csem.step ge s' t s'').

Lemma safe_steps:
  forall s s',
  safe s -> star Csem.step ge s E0 s' -> safe s'.

Lemma star_safe:
  forall s1 s2 t s3,
  safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> star Csem.step ge s2 t s3) ->
  star Csem.step ge s1 t s3.

Lemma plus_safe:
  forall s1 s2 t s3,
  safe s1 -> star Csem.step ge s1 E0 s2 -> (safe s2 -> plus Csem.step ge s2 t s3) ->
  plus Csem.step ge s1 t s3.

Require Import Classical.

Lemma safe_imm_safe:
  forall f C a k e m K,
  safe (ExprState f (C a) k e m) ->
  context K RV C ->
  imm_safe ge e K a m.


Definition expr_kind (a: expr) : kind :=
  match a with
  | Eloc _ _ _ => LV
  | Evar _ _ => LV
  | Ederef _ _ => LV
  | Efield _ _ _ => LV
  | _ => RV
  end.

Lemma lred_kind:
  forall e a m a' m', lred ge e a m a' m' -> expr_kind a = LV.

Lemma rred_kind:
  forall a m t a' m', rred ge a m t a' m' -> expr_kind a = RV.

Lemma callred_kind:
  forall a fd args ty, callred ge a fd args ty -> expr_kind a = RV.

Lemma context_kind:
  forall a from to C, context from to C -> expr_kind a = from -> expr_kind (C a) = to.

Lemma imm_safe_kind:
  forall e k a m, imm_safe ge e k a m -> expr_kind a = k.

Lemma safe_expr_kind:
  forall from C f a k e m,
  context from RV C ->
  safe (ExprState f (C a) k e m) ->
  expr_kind a = from.


Section INVERSION_LEMMAS.

Variable e: env.

Fixpoint exprlist_all_values (rl: exprlist) : Prop :=
  match rl with
  | Enil => True
  | Econs (Eval v ty) rl' => exprlist_all_values rl'
  | Econs _ _ => False
  end.

Definition invert_expr_prop (a: expr) (m: mem) : Prop :=
  match a with
  | Eloc b ofs ty => False
  | Evar x ty =>
      exists b,
      e!x = Some(b, ty)
      \/ (e!x = None /\ Genv.find_symbol ge x = Some b)
  | Ederef (Eval v ty1) ty =>
      exists b, exists ofs, v = Vptr b ofs
  | Efield (Eval v ty1) f ty =>
      exists b, exists ofs, v = Vptr b ofs /\
      match ty1 with
      | Tstruct id _ => exists co delta, ge.(genv_cenv)!id = Some co /\ field_offset ge f (co_members co) = Errors.OK delta
      | Tunion id _ => exists co, ge.(genv_cenv)!id = Some co
      | _ => False
      end
  | Eval v ty => False
  | Evalof (Eloc b ofs ty') ty =>
      ty' = ty /\ exists t, exists v, deref_loc ge ty m b ofs t v
  | Eunop op (Eval v1 ty1) ty =>
      exists v, sem_unary_operation op v1 ty1 m = Some v
  | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty =>
      exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v
  | Ecast (Eval v1 ty1) ty =>
      exists v, sem_cast v1 ty1 ty = Some v
  | Eseqand (Eval v1 ty1) r2 ty =>
      exists b, bool_val v1 ty1 m = Some b
  | Eseqor (Eval v1 ty1) r2 ty =>
      exists b, bool_val v1 ty1 m = Some b
  | Econdition (Eval v1 ty1) r1 r2 ty =>
      exists b, bool_val v1 ty1 m = Some b
  | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty =>
      exists v, exists m', exists t,
      ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m'
  | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty =>
      exists t, exists v1,
      ty = ty1
      /\ deref_loc ge ty1 m b ofs t v1
  | Epostincr id (Eloc b ofs ty1) ty =>
      exists t, exists v1,
      ty = ty1
      /\ deref_loc ge ty m b ofs t v1
  | Ecomma (Eval v ty1) r2 ty =>
      typeof r2 = ty
  | Eparen (Eval v1 ty1) ty2 ty =>
      exists v, sem_cast v1 ty1 ty2 = Some v
  | Ecall (Eval vf tyf) rargs ty =>
      exprlist_all_values rargs ->
      exists tyargs tyres cconv fd vl,
         classify_fun tyf = fun_case_f tyargs tyres cconv
      /\ Genv.find_funct ge vf = Some fd
      /\ cast_arguments rargs tyargs vl
      /\ type_of_fundef fd = Tfunction tyargs tyres cconv
  | Ebuiltin ef tyargs rargs ty =>
      exprlist_all_values rargs ->
      exists vargs, exists t, exists vres, exists m',
         cast_arguments rargs tyargs vargs
      /\ external_call ef ge vargs m t vres m'
  | _ => True
  end.

Lemma lred_invert:
  forall l m l' m', lred ge e l m l' m' -> invert_expr_prop l m.

Lemma rred_invert:
  forall r m t r' m', rred ge r m t r' m' -> invert_expr_prop r m.

Lemma callred_invert:
  forall r fd args ty m,
  callred ge r fd args ty ->
  invert_expr_prop r m.

Scheme context_ind2 := Minimality for context Sort Prop
  with contextlist_ind2 := Minimality for contextlist Sort Prop.
Combined Scheme context_contextlist_ind from context_ind2, contextlist_ind2.

Lemma invert_expr_context:
  (forall from to C, context from to C ->
   forall a