Library Cshmgenproof2

Correctness of the C front end, part 2: Csharpminor construction functions





Require Import Coqlib.

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

Require Import Csyntax.

Require Import Csem.

Require Import Ctyping.

Require Import Cminor.

Require Import Csharpminor.

Require Import Cshmgen.

Require Import Cshmgenproof1.




Section CONSTRUCTORS.




Variable globenv : genv * gvarenv.

Let ge := fst globenv.

Correctness of Csharpminor construction functions





Lemma make_intconst_correct:

  forall n e m,

  eval_expr globenv e m (make_intconst n) (Vint n).






Lemma make_floatconst_correct:

  forall n e m,

  eval_expr globenv e m (make_floatconst n) (Vfloat n).






Hint Resolve make_intconst_correct make_floatconst_correct

             eval_Eunop eval_Ebinop: cshm.

Hint Extern 2 (@eq trace _ _) => traceEq: cshm.




Remark Vtrue_is_true: Val.is_true Vtrue.






Remark Vfalse_is_false: Val.is_false Vfalse.






Lemma make_boolean_correct_true:

 forall e m a v ty,

  eval_expr globenv e m a v ->

  is_true v ty ->

  exists vb,

    eval_expr globenv e m (make_boolean a ty) vb

    /\ Val.is_true vb.






Lemma make_boolean_correct_false:

 forall e m a v ty,

  eval_expr globenv e m a v ->

  is_false v ty ->

  exists vb,

    eval_expr globenv e m (make_boolean a ty) vb

    /\ Val.is_false vb.






Lemma make_neg_correct:

  forall a tya c va v e m,

  sem_neg va tya = Some v ->

  make_neg a tya = OK c ->  

  eval_expr globenv e m a va ->

  eval_expr globenv e m c v.






Lemma make_notbool_correct:

  forall a tya c va v e m,

  sem_notbool va tya = Some v ->

  make_notbool a tya = c ->  

  eval_expr globenv e m a va ->

  eval_expr globenv e m c v.






Lemma make_notint_correct:

  forall a tya c va v e m,

  sem_notint va = Some v ->

  make_notint a tya = c ->  

  eval_expr globenv e m a va ->

  eval_expr globenv e m c v.






Definition binary_constructor_correct

    (make: expr -> type -> expr -> type -> res expr)

    (sem: val -> type -> val -> type -> option val): Prop :=

  forall a tya b tyb c va vb v e m,

  sem va tya vb tyb = Some v ->

  make a tya b tyb = OK c ->  

  eval_expr globenv e m a va ->

  eval_expr globenv e m b vb ->

  eval_expr globenv e m c v.




Definition binary_constructor_correct'

    (make: expr -> type -> expr -> type -> res expr)

    (sem: val -> val -> option val): Prop :=

  forall a tya b tyb c va vb v e m,

  sem va vb = Some v ->

  make a tya b tyb = OK c ->  

  eval_expr globenv e m a va ->

  eval_expr globenv e m b vb ->

  eval_expr globenv e m c v.




Lemma make_add_correct: binary_constructor_correct make_add sem_add.






Lemma make_sub_correct: binary_constructor_correct make_sub sem_sub.






Lemma make_mul_correct: binary_constructor_correct make_mul sem_mul.






Lemma make_div_correct: binary_constructor_correct make_div sem_div.






Lemma make_mod_correct: binary_constructor_correct make_mod sem_mod.

  red; intros until m. intro SEM. unfold make_mod.

  functional inversion SEM; rewrite H0; intros.

  inversion H8. eapply eval_Ebinop; eauto with cshm.

  simpl. rewrite H7; auto.

  inversion H8. eapply eval_Ebinop; eauto with cshm.

  simpl. rewrite H7; auto.






Lemma make_and_correct: binary_constructor_correct' make_and sem_and.






Lemma make_or_correct: binary_constructor_correct' make_or sem_or.






Lemma make_xor_correct: binary_constructor_correct' make_xor sem_xor.






Lemma make_shl_correct: binary_constructor_correct' make_shl sem_shl.






Lemma make_shr_correct: binary_constructor_correct make_shr sem_shr.






Lemma make_cmp_correct:

  forall cmp a tya b tyb c va vb v e m,

  sem_cmp cmp va tya vb tyb m = Some v ->

  make_cmp cmp a tya b tyb = OK c ->  

  eval_expr globenv e m a va ->

  eval_expr globenv e m b vb ->

  eval_expr globenv e m c v.






Lemma transl_unop_correct:

  forall op a tya c va v e m, 

  transl_unop op a tya = OK c ->

  sem_unary_operation op va tya = Some v ->

  eval_expr globenv e m a va ->

  eval_expr globenv e m c v.






Lemma transl_binop_correct:

  forall op a tya b tyb c va vb v e m,

  transl_binop op a tya b tyb = OK c ->  

  sem_binary_operation op va tya vb tyb m = Some v ->

  eval_expr globenv e m a va ->

  eval_expr globenv e m b vb ->

  eval_expr globenv e m c v.






Lemma make_cast_correct:

  forall e m a v ty1 ty2 v',

   eval_expr globenv e m a v ->

   cast v ty1 ty2 v' ->

   eval_expr globenv e m (make_cast ty1 ty2 a) v'.






Lemma make_load_correct:

  forall addr ty code b ofs v e m,

  make_load addr ty = OK code ->

  eval_expr globenv e m addr (Vptr b ofs) ->

  load_value_of_type ty m b ofs = Some v ->

  eval_expr globenv e m code v.






Lemma make_store_correct:

  forall addr ty rhs code e m b ofs v m' f k,

  make_store addr ty rhs = OK code ->

  eval_expr globenv e m addr (Vptr b ofs) ->

  eval_expr globenv e m rhs v ->

  store_value_of_type ty m b ofs v = Some m' ->

  step globenv (State f code k e m) E0 (State f Sskip k e m').






End CONSTRUCTORS.