binop_lemmas2.v

Timings for binop_lemmas2.v

/home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-vst.dev/./veric/binop_lemmas2.v.timing

/home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-vst.dev/./veric/binop_lemmas2.v.timing

Require Import VST.msl.msl_standard.

Require Import VST.veric.Clight_base.

Require Import VST.veric.compcert_rmaps.

Require Import VST.veric.Clight_lemmas.

Require Import VST.veric.mpred.

Require Import VST.veric.tycontext.

Require Import VST.veric.expr2.

Require Import VST.veric.Clight_Cop2.

Import Cop.

Import compcert.lib.Maps.

Lemma eval_expr_any: forall {CS: compspecs} rho e v, eval_expr e any_environ = v -> v <> Vundef -> eval_expr e rho = v with eval_lvalue_any: forall {CS: compspecs} rho e v, eval_lvalue e any_environ = v -> v <> Vundef -> eval_lvalue e rho = v.

Proof.

{

clear eval_expr_any.

intros ? ?.

induction e; simpl; intros; subst; unfold_lift; try reflexivity; unfold_lift in H0; cbv delta [eval_unop eval_binop force_val2 force_val1 deref_noload always Datatypes.id deref_noload force_ptr force_val eval_var eval_id ] in H0|-*; simpl in *; repeat match goal with | _ => reflexivity | |- match access_mode ?t with | _ => _ end _ = _ => destruct (access_mode t); simpl in * | |- context [match eval_expr ?e any_environ with _ => _ end] => destruct (eval_expr e any_environ) eqn:?; try congruence; rewrite (IHe _ (eq_refl _)); auto | _ => try congruence end.

*

apply IHe; auto.

*

apply eval_lvalue_any; auto.

*

destruct (eval_expr e any_environ) eqn:?; simpl in *; [exfalso; apply H0; clear; try destruct u; destruct (typeof e) as [ | [ | | | ] [ | ] | [ | ] | [ | ] | | | | | ]; try reflexivity | rewrite (IHe _ (eq_refl _)) by congruence; auto .. ].

simpl.

unfold Cop2.bool_val; simple_if_tac; reflexivity.

*

destruct (eval_expr e1 any_environ) eqn:?; simpl in *; [ exfalso; apply H0; clear | rewrite (IHe1 _ (eq_refl _)) by congruence; auto .. ].

{

destruct b; destruct (typeof e1) as [ | [ | | | ] [ | ] | [ | ] | [ | ] | | | | | ]; destruct (typeof e2) as [ | [ | | | ] [ | ] | [ | ] | [ | ] | | | | | ]; try reflexivity; cbv beta iota delta [ sem_binary_operation' Clight_Cop2.sem_add Clight_Cop2.sem_sub classify_add classify_sub sem_sub_pi sem_sub_pl sem_sub_pp Clight_Cop2.sem_add_ptr_int Clight_Cop2.sem_add_ptr_long sem_add_int_ptr sem_add_ptr_int sem_add_long_ptr sem_add_ptr_long Clight_Cop2.sem_cmp classify_cmp typeconv remove_attributes change_attributes ]; try (simple_if_tac; [ | reflexivity]); repeat match goal with |- context [eqb_type ?A ?B] => let J := fresh "J" in destruct (eqb_type A B) eqn:J; [apply eqb_type_true in J; try solve [inv J] | apply eqb_type_false in J] end; try reflexivity; destruct (eval_expr e2 any_environ); reflexivity.

}

all: destruct (eval_expr e2 any_environ) eqn:?; simpl in *; [ exfalso; apply H0; clear | rewrite (IHe2 _ (eq_refl _)) by congruence; auto .. ]; destruct b; destruct (typeof e1) as [ | [ | | | ] [ | ] | [ | ] | [ | ] | | | | | ]; destruct (typeof e2) as [ | [ | | | ] [ | ] | [ | ] | [ | ] | | | | | ]; try reflexivity; cbv beta iota delta [ sem_binary_operation' Clight_Cop2.sem_add Clight_Cop2.sem_sub classify_add classify_sub sem_sub_pi sem_sub_pl sem_sub_pp Clight_Cop2.sem_add_ptr_int Clight_Cop2.sem_add_ptr_long sem_add_int_ptr sem_add_ptr_int sem_add_long_ptr sem_add_ptr_long Clight_Cop2.sem_cmp classify_cmp typeconv remove_attributes change_attributes ]; try (simple_if_tac; [ | reflexivity]); repeat match goal with |- context [eqb_type ?A ?B] => let J := fresh "J" in destruct (eqb_type A B) eqn:J; [apply eqb_type_true in J; try solve [inv J] | apply eqb_type_false in J] end; reflexivity.

*

destruct t as [ | [ | | | ] [ | ] | [ | ] | [ | ] | | | | | ]; destruct (typeof e) as [ | [ | | | ] [ | ] | [ | ] | [ | ] | | | | | ]; (destruct (eval_expr e any_environ) eqn:?; simpl in *; [exfalso; apply H0; clear | try rewrite (IHe _ (eq_refl _)) by congruence; auto .. ]); auto; try (unfold Clight_Cop2.sem_cast, Clight_Cop2.classify_cast; repeat simple_if_tac; reflexivity).

*

destruct (typeof e) as [ | [ | | | ] [ | ] | [ | ] | [ | ] | | | | | ]; simpl in *; unfold always; auto; destruct (cenv_cs ! i0) as [co |]; auto.

-

destruct (field_offset cenv_cs i (co_members co)) as [[? [|]]|]; auto.

f_equal.

apply eval_lvalue_any; auto.

intro.

rewrite H in H0.

apply H0; reflexivity.

-

destruct (union_field_offset cenv_cs i (co_members co)) as [[? [|]]|]; auto.

destruct (eval_lvalue e any_environ) eqn:?; simpl in *; try congruence.

rewrite (eval_lvalue_any _ _ _ _ Heqv); auto.

congruence.

}

{

clear eval_lvalue_any.

intro.

induction e; simpl; intros; subst; unfold_lift; try reflexivity; unfold_lift in H0.

*

unfold eval_var in *; simpl in *; congruence.

*

apply eval_expr_any; auto.

*

destruct (typeof e) as [ | [ | | | ] [ | ] | [ | ] | [ | ] | | | | | ]; simpl in *; unfold always; auto; destruct (cenv_cs ! i0) as [co |]; auto.

-

destruct (field_offset cenv_cs i (co_members co)) as [[? [|]]|]; auto.

f_equal.

apply IHe; auto.

intro.

rewrite H in H0.

apply H0; reflexivity.

-

destruct (union_field_offset cenv_cs i (co_members co)) as [[? [|]]|]; auto.

destruct (eval_lvalue e any_environ) eqn:?; simpl in *; try congruence.

rewrite (IHe _ (eq_refl _)); auto.

congruence.

}

Qed.

Lemma denote_tc_assert_ilt': forall {CS: compspecs} e j, denote_tc_assert (tc_ilt e j) = denote_tc_assert (tc_ilt' e j).

Proof.

intros.

extensionality rho.

unfold tc_ilt; simpl.

unfold_lift.

destruct (eval_expr e any_environ) eqn:?; simpl; auto.

apply (eval_expr_any rho) in Heqv; try congruence.

rewrite Heqv; simpl.

destruct (Int.ltu i j) eqn:?; simpl; unfold_lift; simpl; rewrite ?Heqv; simpl; auto.

apply pred_ext; intuition.

apply Int.ltu_inv in Heqb.

intros ? ?.

simpl.

destruct Heqb.

auto.

Qed.

Lemma denote_tc_assert_llt': forall {CS: compspecs} e j, denote_tc_assert (tc_llt e j) = denote_tc_assert (tc_llt' e j).

Proof.

intros.

extensionality rho.

unfold tc_llt; simpl.

unfold_lift.

destruct (eval_expr e any_environ) eqn:?; simpl; auto.

apply (eval_expr_any rho) in Heqv; try congruence.

rewrite Heqv; simpl.

destruct (Int64.ltu i j) eqn:?; simpl; unfold_lift; simpl; rewrite ?Heqv; simpl; auto.

apply pred_ext; intuition.

apply Int64.ltu_inv in Heqb.

intros ? ?.

simpl.

destruct Heqb.

auto.

Qed.

Lemma tc_val_void: forall v, tc_val Tvoid v <-> False.

Proof.

destruct v; simpl; tauto.

Qed.

Definition denote_tc_assert' {CS: compspecs} (a: tc_assert) (rho: environ) : mpred.

pose (P := denote_tc_assert a rho).

unfold denote_tc_assert in P.

super_unfold_lift.

destruct a; apply P.

Defined.

Lemma denote_tc_assert'_eq{CS: compspecs}: denote_tc_assert' = denote_tc_assert.

Proof.

extensionality a rho.

destruct a; reflexivity.

Qed.

Lemma int_eq_true : forall x y, true = Int.eq x y -> x = y.

Proof.

intros.

assert (X := Int.eq_spec x y).

rewrite <- H in X; congruence.

Qed.

Lemma tc_andp_TT2: forall e, tc_andp e tc_TT = e.

Proof.

intros; unfold tc_andp.

destruct e; reflexivity.

Qed.

Lemma tc_andp_TT1: forall e, tc_andp tc_TT e = e.

Proof.

intros; unfold tc_andp; reflexivity.

Qed.

Lemma tc_orp_sound : forall {CS: compspecs} a1 a2 rho m, denote_tc_assert (tc_orp a1 a2) rho m <-> denote_tc_assert (tc_orp' a1 a2) rho m.

Proof.

intros.

unfold tc_orp.

assert (forall a t, denote_tc_assert (tc_orp' a (tc_FF t)) rho m <-> denote_tc_assert a rho m) by (intros; destruct a; simpl; unfold typecheck_error; tauto).

assert (forall a t, denote_tc_assert (tc_orp' (tc_FF t) a) rho m <-> denote_tc_assert a rho m) by (intros; destruct a; simpl; unfold typecheck_error; tauto).

assert (forall a, denote_tc_assert (tc_orp' a tc_TT) rho m <-> denote_tc_assert tc_TT rho m) by (intros; destruct a; simpl; unfold typecheck_error; tauto).

assert (forall a, denote_tc_assert (tc_orp' tc_TT a) rho m <-> denote_tc_assert tc_TT rho m) by (intros; destruct a; simpl; unfold typecheck_error; tauto).

destruct a1,a2; rewrite ?H, ?H0, ?H1, ?H2; apply iff_refl.

Qed.

Lemma denote_tc_assert_orp: forall {CS: compspecs} x y rho, denote_tc_assert (tc_orp x y) rho = orp (denote_tc_assert x rho) (denote_tc_assert y rho).

Proof.

intros.

apply pred_ext; intro m; rewrite tc_orp_sound; intro; assumption.

Qed.

Lemma is_true_true: is_true true = True.

Proof.

apply prop_ext; intuition.

Qed.

Lemma is_true_false: is_true false = False.

Proof.

apply prop_ext; intuition.

Qed.

Lemma denote_tc_assert_iszero: forall {CS: compspecs} e rho, denote_tc_assert (tc_iszero e) rho = match (eval_expr e rho) with | Vint i => prop (is_true (Int.eq i Int.zero)) | Vlong i => prop (is_true (Int64.eq i Int64.zero)) | _ => FF end.

Proof.

intros.

unfold tc_iszero.

destruct (eval_expr e any_environ) eqn:?; simpl; auto; rewrite (eval_expr_any rho e _ Heqv) by congruence.

destruct (Int.eq i Int.zero); reflexivity.

destruct (Int64.eq i Int64.zero); reflexivity.

Qed.

Lemma denote_tc_assert_iszero': forall {CS: compspecs} e, denote_tc_assert (tc_iszero e) = denote_tc_assert (tc_iszero' e).

Proof.

intros.

extensionality rho.

rewrite denote_tc_assert_iszero.

reflexivity.

Qed.

Lemma denote_tc_assert_nonzero: forall {CS: compspecs} e rho, denote_tc_assert (tc_nonzero e) rho = match (eval_expr e rho) with | Vint i => prop (i <> Int.zero) | Vlong i =>prop (i <> Int64.zero) | _ => FF end.

Proof.

intros.

unfold tc_nonzero.

destruct (eval_expr e any_environ) eqn:?; simpl; auto; try rewrite (eval_expr_any rho e _ Heqv) by congruence; unfold_lift.

+

destruct (Int.eq i Int.zero) eqn:?; simpl; unfold_lift; unfold denote_tc_nonzero; simpl; rewrite ?(eval_expr_any rho e _ Heqv) by congruence; auto.

apply pred_ext; auto; intros ? ? ?; subst; inv Heqb.

+

destruct (Int64.eq i Int64.zero) eqn:?; simpl; unfold_lift; unfold denote_tc_nonzero; simpl; rewrite ?(eval_expr_any rho e _ Heqv) by congruence; auto.

apply pred_ext; auto; intros ? ? ?; subst; inv Heqb.

Qed.

Lemma denote_tc_assert_nonzero': forall {CS: compspecs} e, denote_tc_assert (tc_nonzero e) = denote_tc_assert (tc_nonzero' e).

Proof.

intros.

extensionality rho.

rewrite denote_tc_assert_nonzero.

simpl.

unfold_lift.

destruct (eval_expr e rho); simpl; auto.

Qed.

Lemma denote_tc_assert_nodivover: forall {CS: compspecs} e1 e2 rho, denote_tc_assert (tc_nodivover e1 e2) rho = match eval_expr e1 rho, eval_expr e2 rho with | Vint n1, Vint n2 => prop (~(n1 = Int.repr Int.min_signed /\ n2 = Int.mone)) | Vlong n1, Vlong n2 => prop (~(n1 = Int64.repr Int64.min_signed /\ n2 = Int64.mone)) | Vint n1, Vlong n2 => TT | Vlong n1, Vint n2 => prop (~ (n1 = Int64.repr Int64.min_signed /\ n2 = Int.mone)) | _ , _ => FF end.

Proof.

intros.

unfold tc_nodivover.

destruct (eval_expr e1 any_environ) eqn:?; destruct (eval_expr e2 any_environ) eqn:?; simpl; auto; rewrite (eval_expr_any rho e1 _ Heqv) by congruence; rewrite (eval_expr_any rho e2 _ Heqv0) by congruence; auto.

+

destruct (negb (Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone)) eqn:?.

simpl; unfold_lift; apply pred_ext; auto; intros ? ? [? ?]; subst; inv Heqb.

simpl; unfold_lift; rewrite (eval_expr_any rho e1 _ Heqv) by congruence; rewrite (eval_expr_any rho e2 _ Heqv0) by congruence; reflexivity.

+

destruct (negb (Int64.eq i (Int64.repr Int64.min_signed) && Int.eq i0 Int.mone)) eqn:?.

simpl; unfold_lift; apply pred_ext; auto; intros ? ? [? ?]; subst; inv Heqb.

simpl; unfold_lift; rewrite (eval_expr_any rho e1 _ Heqv) by congruence; rewrite (eval_expr_any rho e2 _ Heqv0) by congruence; reflexivity.

+

destruct (negb (Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone)) eqn:?.

simpl; unfold_lift; apply pred_ext; auto; intros ? ? [? ?]; subst; inv Heqb.

simpl; unfold_lift; rewrite (eval_expr_any rho e1 _ Heqv) by congruence; rewrite (eval_expr_any rho e2 _ Heqv0) by congruence; reflexivity.

Qed.

Lemma denote_tc_assert_nodivover': forall {CS: compspecs} e1 e2, denote_tc_assert (tc_nodivover e1 e2) = denote_tc_assert (tc_nodivover' e1 e2).

Proof.

intros.

extensionality rho.

rewrite denote_tc_assert_nodivover; reflexivity.

Qed.

Lemma denote_tc_assert_andp'': forall {CS: compspecs} a b rho, denote_tc_assert (tc_andp' a b) rho = andp (denote_tc_assert a rho) (denote_tc_assert b rho).

Proof.

intros.

reflexivity.

Qed.

Lemma denote_tc_assert_orp'': forall {CS: compspecs} a b rho, denote_tc_assert (tc_orp' a b) rho = orp (denote_tc_assert a rho) (denote_tc_assert b rho).

Proof.

intros.

reflexivity.

Qed.

Lemma denote_tc_assert_andp': forall {CS: compspecs} a b, denote_tc_assert (tc_andp a b) = denote_tc_assert (tc_andp' a b).

Proof.

intros.

extensionality rho.

apply denote_tc_assert_andp.

Qed.

Lemma denote_tc_assert_orp': forall {CS: compspecs} a b, denote_tc_assert (tc_orp a b) = denote_tc_assert (tc_orp' a b).

Proof.

intros.

extensionality rho.

apply denote_tc_assert_orp.

Qed.

Lemma denote_tc_assert_test_eq': forall {CS: compspecs} a b, denote_tc_assert (tc_test_eq a b) = denote_tc_assert (tc_test_eq' a b).

Proof.

intros; extensionality rho.

unfold tc_test_eq.

simpl; unfold_lift; unfold denote_tc_test_eq.

destruct (Val.eq (eval_expr a any_environ) Vundef); [rewrite e; reflexivity | ].

rewrite <- (eval_expr_any rho _ _ (eq_refl _) n).

destruct (Val.eq (eval_expr b any_environ) Vundef).

rewrite e; destruct (eval_expr a rho) eqn:Ha; simpl; unfold_lift; rewrite Ha; reflexivity.

rewrite <- (eval_expr_any rho _ _ (eq_refl _) n0).

clear n n0.

destruct (eval_expr a rho) eqn:Ha; simpl; unfold_lift; try rewrite Ha; try reflexivity; destruct (eval_expr b rho) eqn:Hb; simpl; unfold_lift; rewrite ?Ha, ?Hb; try reflexivity.

*

destruct Archi.ptr64 eqn:Hp; simpl; unfold_lift.

+

rewrite Ha,Hb; simpl; rewrite Hp; reflexivity.

+

pose proof (Int.eq_spec i Int.zero); destruct (Int.eq i Int.zero).

pose proof (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero).

simpl.

rewrite !prop_true_andp by auto.

unfold_lift.

unfold TT.

apply f_equal.

apply prop_ext; intuition.

simpl.

unfold_lift.

rewrite Ha,Hb.

simpl.

rewrite Hp.

auto.

simpl.

unfold_lift.

rewrite Ha,Hb.

simpl.

rewrite Hp.

auto.

*

destruct Archi.ptr64 eqn:Hp; simpl; unfold_lift.

+

pose proof (Int64.eq_spec i Int64.zero); destruct (Int64.eq i Int64.zero).

pose proof (Int64.eq_spec i0 Int64.zero); destruct (Int64.eq i0 Int64.zero).

simpl.

rewrite !prop_true_andp by auto.

unfold_lift.

unfold TT.

apply f_equal.

apply prop_ext; intuition.

simpl.

unfold_lift.

rewrite Ha,Hb.

simpl.

rewrite Hp.

auto.

simpl.

unfold_lift.

rewrite Ha,Hb.

simpl.

rewrite Hp.

auto.

+

rewrite Ha,Hb; simpl; rewrite Hp; reflexivity.

Qed.

Lemma denote_tc_assert_test_order': forall {CS: compspecs} a b, denote_tc_assert (tc_test_order a b) = denote_tc_assert (tc_test_order' a b).

Proof.

intros; extensionality rho.

unfold tc_test_order.

simpl; unfold_lift; unfold denote_tc_test_order.

destruct (eval_expr a rho) eqn:Ha; destruct (eval_expr a any_environ) eqn:Ha'; simpl; unfold_lift; unfold denote_tc_test_order; rewrite ?Ha, ?Ha'; simpl; auto; try solve [ rewrite (eval_expr_any rho a _ Ha') in Ha by congruence; inv Ha]; destruct (eval_expr b rho) eqn:Hb; destruct (eval_expr b any_environ) eqn:Hb'; simpl; unfold_lift; unfold denote_tc_test_eq; rewrite ?Ha, ?Ha', ?Hb, ?Hb'; simpl; auto; rewrite (eval_expr_any rho b _ Hb') in Hb by congruence; inv Hb; rewrite (eval_expr_any rho a _ Ha') in Ha by congruence; inv Ha.

*

destruct Archi.ptr64 eqn:Hp.

+

simpl.

unfold_lift.

rewrite (eval_expr_any rho b _ Hb') by congruence; rewrite (eval_expr_any rho a _ Ha') by congruence.

simpl.

rewrite Hp.

auto.

+

simpl.

{

destruct (Int.eq_dec i Int.zero).

+

subst.

rewrite Int.eq_true.

destruct (Int.eq_dec i1 Int.zero).

-

subst.

rewrite Int.eq_true.

simpl.

rewrite !prop_true_andp by auto.

super_unfold_lift.

unfold TT.

f_equal.

apply prop_ext; intuition.

-

rewrite Int.eq_false by auto.

simpl.

simpl; unfold_lift; unfold denote_tc_test_eq.

rewrite (eval_expr_any rho a _ Ha') by congruence.

rewrite (eval_expr_any rho _ _ Hb') by congruence.

simpl.

rewrite Hp.

auto.

+

rewrite Int.eq_false by auto.

simpl.

simpl; unfold_lift; unfold denote_tc_test_eq.

rewrite (eval_expr_any rho a _ Ha') by congruence.

rewrite (eval_expr_any rho _ _ Hb') by congruence.

simpl.

rewrite Hp.

auto.

}

*

destruct Archi.ptr64 eqn:Hp.

+

simpl.

{

destruct (Int64.eq_dec i Int64.zero).

+

subst.

rewrite Int64.eq_true.

destruct (Int64.eq_dec i1 Int64.zero).

-

subst.

rewrite Int64.eq_true.

simpl.

rewrite !prop_true_andp by auto.

super_unfold_lift.

unfold TT.

f_equal.

apply prop_ext; intuition.

-

rewrite Int64.eq_false by auto.

simpl.

simpl; unfold_lift; unfold denote_tc_test_eq.

rewrite (eval_expr_any rho a _ Ha') by congruence.

rewrite (eval_expr_any rho _ _ Hb') by congruence.

simpl.

rewrite Hp.

auto.

+

rewrite Int64.eq_false by auto.

simpl.

simpl; unfold_lift; unfold denote_tc_test_eq.

rewrite (eval_expr_any rho a _ Ha') by congruence.

rewrite (eval_expr_any rho _ _ Hb') by congruence.

simpl.

rewrite Hp.

auto.

}

+

simpl.

unfold_lift.

rewrite (eval_expr_any rho b _ Hb') by congruence; rewrite (eval_expr_any rho a _ Ha') by congruence.

simpl.

rewrite Hp.

auto.

Qed.

Lemma denote_tc_assert_andp_andp'_eq: forall {CS: compspecs} x y x' y', denote_tc_assert x = denote_tc_assert x' -> denote_tc_assert y = denote_tc_assert y' -> denote_tc_assert (tc_andp x y) = denote_tc_assert (tc_andp' x' y').

Proof.

intros.

rewrite denote_tc_assert_andp'.

extensionality rho.

simpl.

unfold liftx, lift.

simpl.

congruence.

Qed.

Lemma denote_tc_assert_andp'_eq: forall {CS: compspecs} x y x' y', denote_tc_assert x = denote_tc_assert x' -> denote_tc_assert y = denote_tc_assert y' -> denote_tc_assert (tc_andp' x y) = denote_tc_assert (tc_andp' x' y').

Proof.

intros.

extensionality rho.

simpl.

unfold liftx, lift.

simpl.

congruence.

Qed.

Lemma denote_tc_assert_orp_orp'_eq: forall {CS: compspecs} x y x' y', denote_tc_assert x = denote_tc_assert x' -> denote_tc_assert y = denote_tc_assert y' -> denote_tc_assert (tc_orp x y) = denote_tc_assert (tc_orp' x' y').

Proof.

intros.

rewrite denote_tc_assert_orp'.

extensionality rho.

simpl.

unfold liftx, lift.

simpl.

congruence.

Qed.

Lemma denote_tc_assert_orp'_eq: forall {CS: compspecs} x y x' y', denote_tc_assert x = denote_tc_assert x' -> denote_tc_assert y = denote_tc_assert y' -> denote_tc_assert (tc_orp' x y) = denote_tc_assert (tc_orp' x' y').

Proof.

intros.

extensionality rho.

simpl.

unfold liftx, lift.

simpl.

congruence.

Qed.

Local Hint Resolve denote_tc_assert_andp_andp'_eq denote_tc_assert_andp'_eq denote_tc_assert_orp_orp'_eq denote_tc_assert_orp'_eq denote_tc_assert_iszero' denote_tc_assert_nonzero' denote_tc_assert_nodivover' denote_tc_assert_ilt' denote_tc_assert_llt' denote_tc_assert_test_eq' denote_tc_assert_test_order' : dtca.

Definition stupid_typeconv ty := match ty with | Tarray t _ a => Tpointer t a | Tfunction _ _ _ => Tpointer ty noattr | Tint _ _ _ => typeconv ty | _ => ty end.

Lemma classify_sub_eq : classify_sub = classify_sub'.

Proof.

unfold classify_sub, classify_sub'; extensionality t1 t2.

destruct t1, t2; simpl; auto; try destruct i,s; auto; try destruct i0,s0; auto.

Qed.

Definition classify_cmp' ty1 ty2 := match stupid_typeconv ty1, stupid_typeconv ty2 with | Tpointer _ _ , Tpointer _ _ => cmp_case_pp | Tpointer _ _ , Tint _ si _ => cmp_case_pi si | Tint _ si _, Tpointer _ _ => cmp_case_ip si | Tpointer _ _ , Tlong _ _ => cmp_case_pl | Tlong _ _ , Tpointer _ _ => cmp_case_lp | _, _ => cmp_default end.

Lemma classify_cmp_eq: classify_cmp = classify_cmp'.

Proof.

unfold classify_cmp, classify_cmp'; extensionality t1 t2.

destruct t1,t2; simpl; auto; try destruct i,s; auto; try destruct i0,s0; auto.

Qed.

Lemma classify_add_eq: classify_add = classify_add'.

Proof.

unfold classify_add; extensionality t1 t2.

destruct t1,t2; simpl; auto; try destruct i,s; auto; try destruct i0,s0; auto.

Qed.

Definition classify_shift' (ty1: type) (ty2: type) := match stupid_typeconv ty1, stupid_typeconv ty2 with | Tint sz sg _, Tint _ _ _ => shift_case_ii match sz, sg with | I32, Unsigned => Unsigned | _, _ => Signed end | Tint sz sg _, Tlong _ _ => shift_case_il match sz, sg with | I32, Unsigned => Unsigned | _, _ => Signed end | Tlong s _, Tint _ _ _ => shift_case_li s | Tlong s _, Tlong _ _ => shift_case_ll s | _,_ => shift_default end.

Lemma classify_shift_eq: classify_shift = classify_shift'.

Proof.

unfold classify_shift; extensionality t1 t2.

destruct t1,t2; simpl; auto; try destruct i,s; auto; try destruct i0,s0; auto.

Qed.

Definition binarithType' t1 t2 ty deferr reterr : tc_assert := match classify_binarith' t1 t2 with | Cop.bin_case_i sg => tc_bool (is_int32_type ty) reterr | Cop.bin_case_l sg => tc_bool (is_long_type ty) reterr | Cop.bin_case_f => tc_bool (is_float_type ty) reterr | Cop.bin_case_s => tc_bool (is_single_type ty) reterr | Cop.bin_default => tc_FF deferr end.

Lemma classify_binarith_eq: classify_binarith = classify_binarith'.

Proof.

unfold classify_binarith; extensionality t1 t2.

destruct t1,t2; simpl; auto; try destruct i,s; auto; try destruct i0,s0; auto; try destruct s; auto; try destruct s0; auto.

Qed.

Lemma binarithType_eq: binarithType = binarithType'.

Proof.

unfold binarithType, binarithType'; extensionality t1 t2 ty e1 e2.

rewrite classify_binarith_eq.

auto.

Qed.

Lemma den_isBinOpR: forall {CS: compspecs} op a1 a2 ty, denote_tc_assert (isBinOpResultType op a1 a2 ty) = let e := (Ebinop op a1 a2 ty) in let reterr := op_result_type e in let deferr := arg_type e in denote_tc_assert match op with | Cop.Oadd => match classify_add' (typeof a1) (typeof a2) with | Cop.add_case_pi t _ => tc_andp' (tc_andp' (tc_andp' (tc_isptr a1) (tc_bool (complete_type cenv_cs t) reterr)) (tc_int_or_ptr_type (typeof a1))) (tc_bool (is_pointer_type ty) reterr) | Cop.add_case_ip _ t => tc_andp' (tc_andp' (tc_andp' (tc_isptr a2) (tc_bool (complete_type cenv_cs t) reterr)) (tc_int_or_ptr_type (typeof a2))) (tc_bool (is_pointer_type ty) reterr) | Cop.add_case_pl t => tc_andp' (tc_andp' (tc_andp' (tc_isptr a1) (tc_bool (complete_type cenv_cs t) reterr)) (tc_int_or_ptr_type (typeof a1))) (tc_bool (is_pointer_type ty) reterr) | Cop.add_case_lp t => tc_andp' (tc_andp' (tc_andp' (tc_isptr a2) (tc_bool (complete_type cenv_cs t) reterr)) (tc_int_or_ptr_type (typeof a2))) (tc_bool (is_pointer_type ty) reterr) | Cop.add_default => tc_andp (binarithType' (typeof a1) (typeof a2) ty deferr reterr) (tc_nobinover Z.add a1 a2) end | Cop.Osub => match classify_sub' (typeof a1) (typeof a2) with | Cop.sub_case_pi t _ => tc_andp' (tc_andp' (tc_andp' (tc_isptr a1) (tc_bool (complete_type cenv_cs t) reterr)) (tc_int_or_ptr_type (typeof a1))) (tc_bool (is_pointer_type ty) reterr) | Cop.sub_case_pl t => tc_andp' (tc_andp' (tc_andp' (tc_isptr a1) (tc_bool (complete_type cenv_cs t) reterr)) (tc_int_or_ptr_type (typeof a1))) (tc_bool (is_pointer_type ty) reterr) | Cop.sub_case_pp t => tc_andp' (tc_andp' (tc_andp' (tc_andp' (tc_andp' (tc_andp' (tc_andp' (tc_andp' (tc_samebase a1 a2) (tc_isptr a1)) (tc_isptr a2)) (tc_int_or_ptr_type (typeof a1))) (tc_int_or_ptr_type (typeof a2))) (tc_bool (is_ptrofs_type ty) reterr)) (tc_bool (negb (Z.eqb (sizeof t) 0)) (pp_compare_size_0 t))) (tc_bool (complete_type cenv_cs t) reterr)) (tc_bool (Z.leb (sizeof t) Ptrofs.max_signed) (pp_compare_size_exceed t)) | Cop.sub_default => tc_andp (binarithType' (typeof a1) (typeof a2) ty deferr reterr) (tc_nobinover Z.sub a1 a2) end | Cop.Omul => tc_andp (binarithType' (typeof a1) (typeof a2) ty deferr reterr) (tc_nobinover Z.mul a1 a2) | Cop.Omod => match classify_binarith' (typeof a1) (typeof a2) with | Cop.bin_case_i Unsigned => tc_andp' (tc_nonzero' a2) (tc_bool (is_int32_type ty) reterr) | Cop.bin_case_l Unsigned => tc_andp' (tc_nonzero' a2) (tc_bool (is_long_type ty) reterr) | Cop.bin_case_i Signed => tc_andp' (tc_andp' (tc_nonzero' a2) (tc_nodivover' a1 a2)) (tc_bool (is_int32_type ty) reterr) | Cop.bin_case_l Signed => tc_andp' (tc_andp' (tc_nonzero' a2) (tc_nodivover' a1 a2)) (tc_bool (is_long_type ty) reterr) | _ => tc_FF deferr end | Cop.Odiv => match classify_binarith' (typeof a1) (typeof a2) with | Cop.bin_case_i Unsigned => tc_andp' (tc_nonzero' a2) (tc_bool (is_int32_type ty) reterr) | Cop.bin_case_l Unsigned => tc_andp' (tc_nonzero' a2) (tc_bool (is_long_type ty) reterr) | Cop.bin_case_i Signed => tc_andp' (tc_andp' (tc_nonzero' a2) (tc_nodivover' a1 a2)) (tc_bool (is_int32_type ty) reterr) | Cop.bin_case_l Signed => tc_andp' (tc_andp' (tc_nonzero' a2) (tc_nodivover' a1 a2)) (tc_bool (is_long_type ty) reterr) | Cop.bin_case_f => tc_bool (is_float_type ty) reterr | Cop.bin_case_s => tc_bool (is_single_type ty) reterr | Cop.bin_default => tc_FF deferr end | Cop.Oshl | Cop.Oshr => match classify_shift' (typeof a1) (typeof a2) with | Cop.shift_case_ii _ => tc_andp' (tc_ilt' a2 Int.iwordsize) (tc_bool (is_int32_type ty) reterr) | Cop.shift_case_il _ => tc_andp' (tc_llt' a2 (Int64.repr 32)) (tc_bool (is_int32_type ty) reterr) | Cop.shift_case_li _ => tc_andp' (tc_ilt' a2 Int64.iwordsize') (tc_bool (is_long_type ty) reterr) | Cop.shift_case_ll _ => tc_andp' (tc_llt' a2 Int64.iwordsize) (tc_bool (is_long_type ty) reterr) | _ => tc_FF deferr end | Cop.Oand | Cop.Oor | Cop.Oxor => match classify_binarith' (typeof a1) (typeof a2) with | Cop.bin_case_i _ =>tc_bool (is_int32_type ty) reterr | Cop.bin_case_l _ =>tc_bool (is_long_type ty) reterr | Cop.bin_case_f => tc_FF deferr | Cop.bin_case_s => tc_FF deferr | Cop.bin_default => tc_FF deferr end | Cop.Oeq | Cop.One | Cop.Olt | Cop.Ogt | Cop.Ole | Cop.Oge => match classify_cmp' (typeof a1) (typeof a2) with | Cop.cmp_default => tc_bool (is_numeric_type (typeof a1) && is_numeric_type (typeof a2) && is_int_type ty) deferr | Cop.cmp_case_pp => tc_andp' (tc_andp' (tc_int_or_ptr_type (typeof a1)) (tc_int_or_ptr_type (typeof a2))) (check_pp_int' a1 a2 op ty e) | Cop.cmp_case_pi si => tc_andp' (tc_int_or_ptr_type (typeof a1)) (check_pp_int' a1 (Ecast a2 size_t) op ty e) | Cop.cmp_case_ip si => tc_andp' (tc_int_or_ptr_type (typeof a2)) (check_pp_int' (Ecast a1 size_t) a2 op ty e) | Cop.cmp_case_pl => tc_andp' (tc_int_or_ptr_type (typeof a1)) (check_pp_int' a1 (Ecast a2 size_t) op ty e) | Cop.cmp_case_lp => tc_andp' (tc_int_or_ptr_type (typeof a2)) (check_pp_int' (Ecast a1 size_t) a2 op ty e) end end.

Proof.

intros.

rewrite <- classify_add_eq.

rewrite <- classify_sub_eq.

rewrite <- classify_shift_eq.

rewrite <- classify_cmp_eq.

rewrite <- classify_binarith_eq.

rewrite <- binarithType_eq.

unfold isBinOpResultType, classify_add, classify_sub, classify_binarith, classify_shift, classify_cmp, check_pp_int, check_pp_int', typeconv, remove_attributes, change_attributes; destruct op; auto; destruct (typeof a1) as [ | [ | | | ] [ | ] ? | [ | ] ? | [ | ] ? | | | | | ]; destruct (typeof a2) as [ | [ | | | ] [ | ] ? | [ | ] ? | [ | ] ? | | | | | ]; auto 50 with dtca.

Qed.

Lemma denote_tc_assert'_andp'_e: forall {CS: compspecs} a b rho m, denote_tc_assert' (tc_andp' a b) rho m -> denote_tc_assert' a rho m /\ denote_tc_assert' b rho m.

Proof.

intros.

rewrite denote_tc_assert'_eq in *.

apply H.

Qed.

Lemma cast_int_long_nonzero: forall s i, Int.eq i Int.zero = false -> Int64.eq (cast_int_long s i) Int64.zero = false.

Proof.

intros.

pose proof (Int.eq_spec i Int.zero).

rewrite H in H0.

clear H.

rewrite Int64.eq_false; auto.

unfold cast_int_long.

contradict H0.

unfold Int64.zero in H0.

destruct s.

assert (Int64.signed (Int64.repr (Int.signed i)) = Int64.signed (Int64.repr 0)) by (f_equal; auto).

rewrite Int64.signed_repr in H.

rewrite <- (Int.repr_signed i).

rewrite H.

reflexivity.

pose proof (Int64.signed_range Int64.zero).

rewrite Int64.signed_zero in H1.

auto.

pose proof (Int.signed_range i).

clear - H1.

destruct H1.

split.

apply Z.le_trans with Int.min_signed; auto.

compute; congruence.

apply Z.le_trans with Int.max_signed; auto.

compute; congruence.

assert (Int64.unsigned (Int64.repr (Int.unsigned i)) = Int64.unsigned (Int64.repr 0)) by (f_equal; auto).

rewrite Int64.unsigned_repr in H.

rewrite <- (Int.repr_unsigned i).

rewrite H.

reflexivity.

split; compute; congruence.

pose proof (Int.unsigned_range i).

clear - H1.

destruct H1.

split; auto.

unfold Int64.max_unsigned.

apply Z.le_trans with Int.modulus.

lia.

compute; congruence.

Qed.

Definition tc_numeric_val (v: val) (t: type) : Prop := match v,t with | Vint _, Tint _ _ _ => True | Vlong _, Tlong _ _ => True | Vfloat _, Tfloat F64 _ => True | _, _ => False end.

Lemma tc_val_of_bool: forall x i3 s3 a3, tc_val (Tint i3 s3 a3) (Val.of_bool x).

Proof.

intros.

destruct x, i3,s3; simpl; try split; auto; rewrite <- Z.leb_le; reflexivity.

Qed.

Lemma tc_bool2val: forall x i3 s3 a3, tc_val (Tint i3 s3 a3) (bool2val x).

Proof.

intros.

destruct x, i3,s3; simpl; try split; auto; rewrite <- Z.leb_le; reflexivity.

Qed.

Lemma tc_val_sem_cmp: forall op v1 t1 v2 t2 i3 s3 a3, tc_numeric_val v1 t1 -> tc_numeric_val v2 t2 -> tc_val (Tint i3 s3 a3) (force_val (Clight_Cop2.sem_cmp op t1 t2 v1 v2)).

Proof.

Opaque tc_val.

destruct op; intros; destruct v1; destruct t1 as [ | [ | | | ] [ | ] ? | [ | ] ? | [ | ] ? | | | | | ]; try contradiction H; destruct v2; destruct t2 as [ | [ | | | ] [ | ] ? | [ | ] ? | [ | ] ? | | | | | ]; try contradiction H0; apply tc_bool2val.

Transparent tc_val.

Qed.

Lemma tc_val'_sem_cmp_pp: forall cmp v1 v2 v i s a, sem_cmp_pp cmp v1 v2 = Some v -> tc_val' (Tint i s a) v.

Proof.

intros.

unfold sem_cmp_pp, option_map in H.

forget (if Archi.ptr64 then Val.cmplu_bool true2 cmp v1 v2 else Val.cmpu_bool true2 cmp v1 v2) as v0.

destruct v0; inv H.

intros _; apply tc_bool2val.

Qed.

Lemma tc_val'_sem_cmp: forall cmp t v1 v2 t1 t2, is_int_type t = true -> tc_val' t (force_val2 (Clight_Cop2.sem_cmp cmp t1 t2) v1 v2).

Proof.

intros.

destruct t; inv H.

unfold force_val2, force_val.

destruct (Clight_Cop2.sem_cmp cmp t1 t2 v1 v2) eqn:?H; [| intros ?; congruence].

unfold Clight_Cop2.sem_cmp in H.

Opaque tc_val.

destruct (Cop.classify_cmp t1 t2).

+

revert H; simple_if_tac; intros; [congruence |].

eapply tc_val'_sem_cmp_pp; eauto.

+

revert H; simple_if_tac; intros; [congruence |].

unfold sem_cmp_pi in H.

destruct v2; [ inv H | | inv H .. |].

-

eapply tc_val'_sem_cmp_pp; eauto.

-

destruct Archi.ptr64; inv H; try (eapply tc_val'_sem_cmp_pp; eauto).

+

revert H; simple_if_tac; intros; [congruence |].

unfold sem_cmp_ip in H.

destruct v1; [ inv H | | inv H .. |].

-

eapply tc_val'_sem_cmp_pp; eauto.

-

destruct Archi.ptr64; inv H; try (eapply tc_val'_sem_cmp_pp; eauto).

+

revert H; simple_if_tac; intros; [congruence |].

unfold sem_cmp_pl in H.

destruct v2; try congruence.

-

eapply tc_val'_sem_cmp_pp; eauto.

-

destruct Archi.ptr64; inv H.

eapply tc_val'_sem_cmp_pp; eauto.

+

revert H; simple_if_tac; intros; [congruence |].

unfold sem_cmp_lp in H.

destruct v1; try congruence.

-

eapply tc_val'_sem_cmp_pp; eauto.

-

destruct Archi.ptr64; inv H.

eapply tc_val'_sem_cmp_pp; eauto.

+

unfold sem_cmp_default, Clight_Cop2.sem_binarith in H.

destruct (Cop.classify_binarith t1 t2).

-

unfold both_int in H.

forget (Clight_Cop2.sem_cast t1 (Cop.binarith_type (Cop.bin_case_i s0)) v1) as v1'.

forget (Clight_Cop2.sem_cast t2 (Cop.binarith_type (Cop.bin_case_i s0)) v2) as v2'.

destruct v1'; [| inv H].

destruct v0; inv H.

destruct v2'; [| inv H1].

destruct v0; inv H1.

intros _; apply tc_bool2val.

-

unfold both_long in H.

forget (Clight_Cop2.sem_cast t1 (Cop.binarith_type (Cop.bin_case_l s0)) v1) as v1'.

forget (Clight_Cop2.sem_cast t2 (Cop.binarith_type (Cop.bin_case_l s0)) v2) as v2'.

destruct v1'; [| inv H].

destruct v0; inv H.

destruct v2'; [| inv H1].

destruct v0; inv H1.

intros _; apply tc_bool2val.

-

unfold both_float in H.

forget (Clight_Cop2.sem_cast t1 (Cop.binarith_type (Cop.bin_case_f)) v1) as v1'.

forget (Clight_Cop2.sem_cast t2 (Cop.binarith_type (Cop.bin_case_f)) v2) as v2'.

destruct v1'; [| inv H].

destruct v0; inv H.

destruct v2'; [| inv H1].

destruct v0; inv H1.

intros _; apply tc_bool2val.

-

unfold both_single in H.

forget (Clight_Cop2.sem_cast t1 (Cop.binarith_type (Cop.bin_case_s)) v1) as v1'.

forget (Clight_Cop2.sem_cast t2 (Cop.binarith_type (Cop.bin_case_s)) v2) as v2'.

destruct v1'; [| inv H].

destruct v0; inv H.

destruct v2'; [| inv H1].

destruct v0; inv H1.

intros _; apply tc_bool2val.

-

inv H.

Qed.

Lemma tc_val_cmp_eqne_ip: forall op v1 t1 v2 t0 a0 i2 s0 a1, match op with Ceq => True | Cne => True | _ => False end -> match v1,t1 with | Vint i, Tint _ _ _ => Int.eq i Int.zero = true | Vlong i, Tlong _ _ => Int64.eq (Int64.repr (Int64.unsigned i)) Int64.zero = true | _, _ => False end -> tc_val (Tpointer t0 a0) v2 -> tc_val (Tint i2 s0 a1) (force_val (Clight_Cop2.sem_cmp op t1 (Tpointer t0 a0) v1 v2)).

Proof.

Opaque tc_val.

intros until 1; rename H into CMP; intros; destruct op; try contradiction CMP; clear CMP; destruct v1, t1; try contradiction H; destruct v2; try (inv H0; try rewrite H2; try destruct i0; destruct s; unfold Clight_Cop2.sem_cmp, classify_cmp, typeconv, Clight_Cop2.sem_binarith, sem_cast, classify_cast, sem_cmp_lp, sem_cmp_pp; simpl; try rewrite H; try reflexivity; try apply tc_bool2val).

Transparent tc_val.

all: try solve [hnf in H0; destruct (eqb_type _ _); inv H0].

Abort.

Lemma tc_val_cmp_eqne_pi: forall op v1 t1 v2 t0 a0 i2 s0 a1, match op with Ceq => True | Cne => True | _ => False end -> match v1,t1 with | Vint i, Tint _ _ _ => Int.eq i Int.zero = true | Vlong i, Tlong _ _ => Int64.eq (Int64.repr (Int64.unsigned i)) Int64.zero = true | _, _ => False end -> tc_val (Tpointer t0 a0) v2 -> tc_val (Tint i2 s0 a1) (force_val (Clight_Cop2.sem_cmp op (Tpointer t0 a0) t1 v2 v1)).

Proof.

Opaque tc_val.

intros until 1; rename H into CMP; intros.

destruct op; try contradiction CMP; clear CMP; destruct v1, t1; try contradiction H; destruct v2; try (inv H0; try rewrite H2; try destruct i0; destruct s; unfold Clight_Cop2.sem_cmp, classify_cmp, typeconv, sem_binarith, sem_cast, classify_cast, sem_cmp_pl, sem_cmp_pp; simpl; try rewrite H; try reflexivity; try apply tc_bool2val).

Transparent tc_val.

Abort.