Correctness of the C front end, part 2: simulation of binops and casts

Require Import Coqlib.
Require Import Libtactics.
Require Import Errors.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import Ast.
Require Import Values.
Require Import Events.

Require Import Mem.
Require Import Memcomp.
Require Import Globalenvs.
Require Import Pointers.
Require Import Csyntax.
Require Import Csem.
Require Import Ctyping.
Require Import Cminorops.
Require Import Csharpminor.
Require Import Cshmgen.
Require Import Cshmgenproof1.
Require Import Simulations.

Section CLIGHT_DEFS.

Variable prog: Csyntax.program.
Variable tprog: Csharpminor.program.
Hypothesis WTPROG: wt_program prog.
Hypothesis TRANSL: transl_program prog = OK tprog.

Variables (ge : Clight.cl_sem.(SEM_GE)) (tge : cs_sem.(SEM_GE)).

Let lts := (mklts thread_labels (Clight.step ge)).
Let tlts := (mklts thread_labels (cs_step tge)).

Notation match_states := (match_states prog tge).


Ltac simp_inv X := eby inv X; econstructor; try edone; constructor.

Ltac odone := abstract (solve [done|simpl;omega]).
 
Ltac clarify' :=
  clarify;
  repeat match goal with
    | H1: ?x = Some _, H2: ?x = None |- _ => rewrite H2 in H1; clarify
    | H1: ?x = Some _, H2: ?x = Some _ |- _ => rewrite H2 in H1; clarify
  end.

Ltac rewrite_discriminate :=
  match goal with
   | H : ?a = ?b, H' : ?a = ?c |- _ => rewrite H in H'; discriminate
   | H : ?a = ?b, H' : ?a = ?c \/ ?a = ?d |- _ =>
       rewrite H in H'; destruct H'; discriminate
  end.

Ltac sim_binop2_simp H2 :=
 try (left; eexists; split;
      try (eapply step_weakstep; simpl);
      try (eapply StepBinop; inv H2; edone);
      try (eapply match_val; [ edone | done | eassumption ])).

Ltac sim_binop2 v1 v2 H2 :=
 try (destruct v1; destruct v2; try done;
      sim_binop2_simp H2).

Ltac sim_binop2_cmp H1 H2 v1 v2 :=
  unfold cmp in H2; unfold Clight.sem_cmp in H1; try (destruct classify_cmp; try done);
  try (sim_binop2 v1 v2 H2).

Ltac sim_binop EQ2 WT C :=
  try (left; eexists; split;
       try (eapply step_weakstep; simpl);
       inv EQ2;
       try (eapply StepBinop1);
       try (eapply match_expr; inv WT; try edone; try done);
       try discriminate;
       try (eapply match_EKbinop1; unfold match_binop;
            try (rewrite C); try reflexivity);
       try (unfold cmp);
       simpl; try rewrite C; try edone).

Ltac sim_binop_logical e1 e2 EQ2 WT C :=
  unfold make_cmp in EQ2;
  try destruct (classify_cmp (typeof e1) (typeof e2)) as []_eqn : C; try done;
  sim_binop EQ2 WT C.

Ltac sim_cast1 WT :=
  left; eexists; split;
  try (eapply step_weakstep; simpl);
  try eapply StepUnop1;
  eapply match_expr;
     [ edone | done |
       eapply match_EKcast; [ edone | edone | done ] |
       inv WT; done | done ].

Ltac sim_cast1_measure e t WT :=
  right; split; [|split]; try done;
  destruct e; try done;
    [try destruct e; simpl; omega
    |try eapply match_expr; try eapply match_EKcast; try edone;
      [by destruct t | |]; inv WT; try edone;
      try by destruct e; try done; destruct t].

Ltac sim_cast2 :=
   try ( left; eexists; split;
         try (eapply steptau_weakstep; simpl);
         try (eapply StepUnop; edone);
         try (eapply step_weakstep; simpl);
         try (eapply StepUnop; edone);
         eapply match_val; edone);
   try ( left; eexists; split;
         try (eapply step_weakstep; simpl);
         try (eapply StepUnop; edone);
         eapply match_val; edone).

Lemma Sim_StepBinop1:
  forall
   (st1 : Clight.state)
   (t : thread_event)
   (st2: Clight.state)
   (H : Clight.cl_step ge st1 t st2),
   forall (e1 : Csyntax.expr) (op2 : Csyntax.binary_operation)
          (e2 : Csyntax.expr) (ty : type) (ek : Clight.expr_cont)
          (env : Clight.env) (st1' : state),
   match_states
      (Clight.SKexpr (Expr (Csyntax.Ebinop op2 e1 e2) ty) env ek) st1' ->
   (exists st2' : St tlts,
      weakstep tlts st1' TEtau st2' /\
      match_states
                   (Clight.SKexpr e1 env
                     (Clight.EKbinop1 op2 (typeof e1) (typeof e2) ty e2 ek))
                   st2') \/
   (measure
      (Clight.SKexpr e1 env
         (Clight.EKbinop1 op2 (typeof e1) (typeof e2) ty e2 ek)) <
    measure (Clight.SKexpr (Expr (Csyntax.Ebinop op2 e1 e2) ty) env ek))%nat /\
   TEtau = TEtau /\
   match_states
     (Clight.SKexpr e1 env
        (Clight.EKbinop1 op2 (typeof e1) (typeof e2) ty e2 ek))
     st1'.


Lemma Sim_StepBinop2:
  forall
   (st1 : Clight.state)
   (t : thread_event)
   (st2: Clight.state)
   (H : Clight.cl_step ge st1 t st2),
   forall (v : val) (op2 : Csyntax.binary_operation)
     (ty1 ty2 ty : type) (e2 : Csyntax.expr) (ek : Clight.expr_cont)
     (env : Clight.env),
   Clight.valid_arg op2 ty1 ty2 v = true ->
   forall st1' : state,
          match_states
             (Clight.SKval v env (Clight.EKbinop1 op2 ty1 ty2 ty e2 ek)) st1' ->
     (exists st2' : St tlts,
        weakstep tlts st1' TEtau st2' /\
        match_states
          (Clight.SKexpr e2 env (Clight.EKbinop2 op2 ty1 ty2 ty v ek)) st2') \/
        (measure (Clight.SKexpr e2 env (Clight.EKbinop2 op2 ty1 ty2 ty v ek)) <
         measure (Clight.SKval v env (Clight.EKbinop1 op2 ty1 ty2 ty e2 ek)))%nat /\
       TEtau = TEtau /\
       match_states
         (Clight.SKexpr e2 env (Clight.EKbinop2 op2 ty1 ty2 ty v ek)) st1'.

Lemma Sim_StepBinop:
  forall
   (st1 : Clight.state)
   (t : thread_event)
   (st2: Clight.state)
   (H : Clight.cl_step ge st1 t st2),
   forall (v2 v1 : val) (op2 : Csyntax.binary_operation)
     (ty1 ty2 ty : type) (ek : Clight.expr_cont) (env : Clight.env)
     (v : val),
   Clight.sem_binary_operation op2 v1 ty1 v2 ty2 = Some v ->
   forall st1' : state,
   match_states
      (Clight.SKval v2 env (Clight.EKbinop2 op2 ty1 ty2 ty v1 ek)) st1' ->
   (exists st2' : St tlts,
      weakstep tlts st1' TEtau st2' /\
      match_states (Clight.SKval v env ek) st2') \/
   (measure (Clight.SKval v env ek) <
    measure (Clight.SKval v2 env (Clight.EKbinop2 op2 ty1 ty2 ty v1 ek)))%nat /\
   TEtau = TEtau /\ match_states (Clight.SKval v env ek) st1'.

Lemma Sim_StepCast1:
  forall
   (st1 : Clight.state)
   (t : thread_event)
   (st2: Clight.state)
   (H : Clight.cl_step ge st1 t st2),
  forall (ty : type) (e : Csyntax.expr) (ty' : type)
         (ek : Clight.expr_cont) (env : Clight.env) (st1' : state),
     match_states
       (Clight.SKexpr (Expr (Ecast ty e) ty') env ek) st1' ->
     (exists st2' : St tlts,
        weakstep tlts st1' TEtau st2' /\
        match_states
          (Clight.SKexpr e env (Clight.EKcast (typeof e) ty ek)) st2') \/
     (measure (Clight.SKexpr e env (Clight.EKcast (typeof e) ty ek)) <
      measure (Clight.SKexpr (Expr (Ecast ty e) ty') env ek))%nat /\
     TEtau = TEtau /\
     match_states
      (Clight.SKexpr e env (Clight.EKcast (typeof e) ty ek)) st1'.

Lemma intsize_dec (a b: intsize) : {a = b} + {a <> b}.


Lemma Sim_StepCast2:
 forall
  (st1 : Clight.state)
  (t : thread_event)
  (st2 : Clight.state)
  (H : Clight.cl_step ge st1 t st2),
   forall (v : val) (ty ty' : type) (ek : Clight.expr_cont)
     (env : Clight.env) (v' : val),
   Clight.cast v ty' ty v' ->
   forall st1' : state,
   match_states
     (Clight.SKval v env (Clight.EKcast ty' ty ek)) st1' ->
   (exists st2' : St tlts,
     weakstep tlts st1' TEtau st2' /\
     match_states (Clight.SKval v' env ek) st2') \/
   (measure (Clight.SKval v' env ek) <
    measure (Clight.SKval v env (Clight.EKcast ty' ty ek)))%nat /\
   TEtau = TEtau /\ match_states (Clight.SKval v' env ek) st1'.


End CLIGHT_DEFS.