Library symbolic_execution

Define a tactic called 'symbolic_execution' which tries to solve goals like s |= Rv n @ T == v. The tactic tries to recursively apply bop, uop and other lemmas about operation to solve such a goal.

NOTE : This tactic may leave some pure lemmas unsolved.

Require Import Coq.Bool.IfProp.
Require Import Coq.Logic.Classical_Prop.
Require Import Recdef.
Require Import Coq.Init.Wf.
Require Import Coq.Arith.Wf_nat.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import inferules.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Require Import memdata.
Require Import memory.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import hoare_conseq.
Require Import Integers.
Require Import baseTac.
Require Import LibTactics.
Require Import val.
Require Import derivedrules.
Require Import BaseAsrtDef.
Require Import simulation.
Require Import aux_for_hoare_lemmas.
Require Import IntLib.

Open Scope nat_scope.

Set Implicit Arguments.

Lemma id_nth_ge:forall decl n id m, id_nth´ id decl n = Some m -> m >= n.

Lemma id_nth´_suc: forall id decl n m, id_nth´ id decl (S n) = Some (S m) ->
                                       id_nth´ id decl n = Some m .

Lemma id_nth_eq:
  forall n id decl,
    good_decllist decl = true -> id_nth id decl = Some n -> nth_id n decl = Some id.

Lemma eval_type_addr_eq :
  forall e ge le m t,
    evaltype (eaddrof e) (ge , le , m ) = Some (Tptr t) -> evaltype e (ge , le , m ) = Some t.

Lemma eval_addr_eq:
  forall e ge le m b i,
    evalval (eaddrof e) (ge , le , m ) = Some (Vptr (b , i )) -> evaladdr e (ge ,le ,m ) = Some (Vptr (b ,i )).

Lemma nth_id_Some_imply_in_decllist :
  forall n id dls,
    nth_id n dls = Some id ->
    in_decllist id dls = true.

Lemma gooddecl_gettype:
  forall i t dls n t´ id,
    good_decllist (dcons i t dls)=true -> nth_id n dls = Some id -> ftype id (dcons i t dls) = Some t´ -> ftype id dls = Some t´.

Lemma gooddecl_neq:
  forall i t dls n id,
    good_decllist (dcons i t dls)=true -> nth_id n dls = Some id ->
    Zbool.Zeq_bool id i = false.

Lemma insert_star:
  forall s p r q l, p <==> q ** r -> (s |= l ** p <-> s |= q ** l **r).

Lemma asrt_eq_trans:
  forall p q r, p <==> q -> q <==> r -> p <==> r.

Lemma star_star_eq_rep:
  forall p q r q´ A,
    (A <==> p ** q ** r) -> (q <==> q´) -> (A <==> p ** q´ ** r).

Lemma star_star_comm: forall p q r, p ** q ** r <==> q ** p ** r.

Lemma field_asrt_impl:
  forall p id x tid decl b i off tp,
    ftype id decl = Some tp ->
    field_offset id decl = Some off ->
    ((LV x @ Tptr (Tstruct tid decl) |-> Vptr (b , i )) ** p ) ==> (Lv (efield (ederef (evar x)) id ) @ tp == (b ,Int.add i off )).

Lemma field_asrt_impl_g:
  forall p id x tid decl b i off tp,
    ftype id decl = Some tp ->
    field_offset id decl = Some off ->
    ((A_notin_lenv x ** GV x @ Tptr (Tstruct tid decl) |-> Vptr (b , i )) ** p ) ==> (Lv (efield (ederef (evar x)) id ) @ tp == (b ,Int.add i off )).

Lemma eq_impl_trans: forall p q r, p <==> q -> q ==> r -> p ==> r.

Lemma star3_comm: forall p q r l, p ** (q ** l ) ** r <==> q ** p ** l ** r.

Lemma star3_comm´:forall s p q r l, s |= p ** q ** r ** l -> s |= (p ** r ) ** q ** l.

Lemma struct_rm_update_eq:
  forall s b i decl vl id v vi n,
    good_decllist decl =true -> nth_id n decl = Some id -> nth_val n vl = Some vi -> s |= Astruct_rm (b ,i ) decl vl id -> s |= Astruct_rm (b ,i ) decl (update_nth_val n vl v) id.

Lemma update_nth: forall vl n v vi, nth_val n vl = Some vi -> nth_val n (update_nth_val n vl v) = Some v.

Lemma array_rm_update_eq: forall s b i vl v vi n m t, m < n -> nth_val m vl = Some vi -> s |= Aarray_rm (b ,i ) n t vl m -> s |= Aarray_rm (b ,i ) n t (update_nth_val m vl v) m.

Lemma array_rm_update_eq´: forall s b i vl v vi n m t, m < n -> nth_val m vl = Some vi -> s |= Aarray_rm (b ,i ) n t (update_nth_val m vl v) m -> s |= Aarray_rm (b ,i ) n t vl m.

Lemma arrayelem_asrt_impl:
  forall n m p p´ b i t e2 x te2,
    te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
    p <==>
      Alvarenv x (Tarray t n) (addrval_to_addr (b , i )) ** p´ ->
    p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z.of_nat m)) ->
    p ==>
      (Lv (earrayelem (evar x) e2 ) @ t == (b ,Int.add i (Int.mul (Int.repr (BinInt.Z.of_nat (typelen t))) (Int.repr (BinInt.Z.of_nat m))))).

Lemma arrayelem_asrt_impl_g:
  forall n m p p´ b i t e2 x te2,
    te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
    p <==>
      (A_notin_lenv x ** Agvarenv x (Tarray t n) (addrval_to_addr (b , i ))) ** p´ ->
    p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z.of_nat m)) ->
    p ==>
      (Lv (earrayelem (evar x) e2 ) @ t == (b ,Int.add i (Int.mul (Int.repr (BinInt.Z.of_nat (typelen t))) (Int.repr (BinInt.Z.of_nat m))))).

Lemma array_asrt_eq:
  forall n vl b i v t m,
    m < n ->
    nth_val m vl = Some v ->
    Aarray´ (b ,i ) n t vl <==> PV (b ,Int.add i (Int.mul (Int.repr (BinInt.Z.of_nat (typelen t))) (Int.repr (BinInt.Z.of_nat m)))) @ t |-> v ** (Aarray_rm (b ,i ) n t vl m ).

Lemma struct_asrt_eq:
  forall n dls vl id off b i v t,
    (forall ids dl, t <> Tstruct ids dl)->
    (forall t´ n, t <> Tarray t´ n)->
    nth_id n dls = Some id ->
    nth_val n vl = Some v ->
    ftype id dls = Some t ->
    good_decllist dls = true ->
    field_offset id dls = Some off ->
    Astruct´ (b ,i ) dls vl <==> PV (b ,Int.add i off ) @ t |-> v ** (Astruct_rm (b ,i ) dls vl id ).

sep get rv

Theorem lvar_to_lv :
  forall x l t P,
    L & x @ t == l ** P ==> Lv (evar x ) @ t == l.

Theorem gvar_to_lv :
  forall x l t P,
    A_notin_lenv x ** G & x @ t == l ** P ==> Lv (evar x ) @ t == l.

Lemma rule_type_val_match_nvundef:forall v t, rule_type_val_match t v = true -> v <> Vundef.

Lemma lv_mapsto_to_rv :
  forall l t e s P v,
    rule_type_val_match t v = true ->

    s |= Lv e @ t == l ->
    s |= PV l @ t |-> v ** P ->
    s |= Rv e @ t == v.

Definition val_inj (v : option val) : val :=
  match v with
    | Some v´ => v´
    | None => Vundef
  end.

Theorem cast_rv_tptr :
  forall s e v t1 t2,
    s |= Rv e @ (Tptr t1 ) == v ->
    rule_type_val_match (Tptr t1) v = true ->
    s |= Rv (ecast e (Tptr t2)) @ (Tptr t2 ) == v.

Theorem cast_rv_struct_tptr :
  forall s e v t1 t2,
    s |= Rv e @ (Tcom_ptr t1 ) == v ->
    rule_type_val_match (Tcom_ptr t1) v = true ->
    s |= Rv (ecast e (Tptr t2)) @ (Tptr t2 ) == v.

Theorem cast_rv_tnull :
  forall s e v t,
    s |= Rv e @ Tnull == v ->
    rule_type_val_match Tnull v = true ->
    s |= Rv (ecast e (Tptr t)) @ (Tptr t ) == v.

Theorem cast_rv_tint32_tint8 :
  forall s e v v´,
    s |= Rv e @ Tint32 == (Vint32 v ) ->
    cast_eval v Tint32 Tint8 = Some v´ ->
    s |= Rv (ecast e (Tint8)) @ (Tint8 ) == (Vint32 v´).

Theorem cast_rv_tint8_tint16 :
  forall s e v v´,
    s |= Rv e @ Tint8 == (Vint32 v ) ->
    cast_eval v Tint8 Tint16 = Some v´ ->
    s |= Rv (ecast e (Tint16)) @ (Tint16 ) == (Vint32 v´).

Theorem bop_rv :
  forall s bop e1 e2 v1 t1 v2 t2 v t,
    s |= Rv e1 @ t1 == v1 ->
    s |= Rv e2 @ t2 == v2 ->
    val_inj (bop_eval v1 v2 t1 t2 bop) = v ->
    v <> Vundef ->
    bop_type t1 t2 bop = Some t ->
    s |= Rv (ebinop bop e1 e2 ) @ t == v.

Theorem uop_rv :
  forall s uop e v t v´ t´,
    s |= Rv e @ t == v ->
    val_inj (uop_eval v uop) = v´ ->
    v´ <> Vundef ->
    uop_type t uop = Some t´ ->
    s |= Rv (eunop uop e ) @ t´ == v´.

Lemma nth_val_imp_nth_val´_1 :
  forall m vl,
    (Int.unsigned m < Z.of_nat (length vl))%Z ->
    nth_val (Z.abs_nat (Int.unsigned m)) vl = Some (nth_val´ (Z.to_nat (Int.unsigned m)) vl).

Lemma nth_val_imp_nth_val´_2 :
  forall n vl,
    n < length vl ->
    nth_val n vl = Some (nth_val´ n vl).

Theorem deref_rv :
  forall s e l t v´ P,
    s |= Rv e @ Tptr t == Vptr l ->
    s |= PV l @ t |-> v´ ** P ->
    rule_type_val_match t v´ = true ->

    s |= Rv (ederef e ) @ t == v´.

Lemma array_type_vallist_match_imp_rule_type_val_match :
  forall vl n t,
    n < length vl ->
    array_type_vallist_match t vl ->
    rule_type_val_match t (nth_val´ n vl) = true.

Lemma ge0_z_nat_le:
  forall z n,
    (0<=z)%Z ->
    (z < Z.of_nat n)%Z ->
    ((Z.to_nat z ) < n)%nat.

Lemma sub_mul_eq_add_mul:
  forall i i0 x n,
    Int.sub i i0 = Int.mul x (Int.repr (Z.of_nat n)) ->
    (0 <= Int.unsigned i - Int.unsigned i0 <= Int.max_unsigned)%Z ->
    i = Int.add i0 (Int.mul (Int.repr (Z.of_nat n))
                            (Int.repr (Int.unsigned x))).

Theorem deref_ptr_of_array_member_rv´:
  forall P s t´ t vl e i0 b i x v n,
    s |= Aarray (b ,i0 ) t´ vl ** P->
    t´ = Tarray t n ->
    s |= Rv e @ (Tptr t ) == Vptr (b ,i ) ->
    Int.sub i i0 = Int.mul x (Int.repr (Z_of_nat (typelen t )))->
    (0 <= Int.unsigned i - Int.unsigned i0 <= 4294967295)%Z ->
    (Z.of_nat n < 4294967295)%Z ->
    (Int.unsigned x < Z.of_nat n)%Z ->
    (Int.unsigned x < Z.of_nat (length vl))%Z ->
    rule_type_val_match t v = true ->
    nth_val´ (Z.to_nat (Int.unsigned x)) vl = v ->
    s |= Rv (ederef e ) @ t == v.
Lemma unsigned_minus_le_max :
  forall a b,
    (Int.unsigned a - Int.unsigned b <= 4294967295)%Z.

Lemma sub_zero_eq :
  forall i1 i2,
    Int.sub i1 i2 = Int.zero ->
    i1 = i2.

Theorem deref_ptr_of_array_member_rv´´ :
  forall P s t´ t vl e l l´ x v n,
    s |= Aarray l t´ vl ** P->
    t´ = Tarray t n ->
    (Z.of_nat n < 4294967295)%Z ->
    s |= Rv e @ (Tptr t ) == Vptr l´ ->
    typelen t <> 0 ->
    (Z.of_nat (typelen t) < 4294967295)%Z ->
    fst l = fst l´ ->
    (Int.unsigned (snd l) <= Int.unsigned (snd l´))%Z ->
    Int.divu (Int.sub (snd l´) (snd l)) (Int.repr (Z_of_nat (typelen t))) = x ->
    Int.modu (Int.sub (snd l´) (snd l)) (Int.repr (Z_of_nat (typelen t))) = Int.zero ->
    (Int.unsigned x < Z.of_nat n)%Z ->
    (Int.unsigned x < Z.of_nat (length vl))%Z ->
    rule_type_val_match t v = true ->
    nth_val´ (Z.to_nat (Int.unsigned x)) vl = v ->
    s |= Rv (ederef e ) @ t == v.

Lemma Int_div_to_Z_div :
  forall i1 i2 z1 z2,
    (Int.unsigned i2 <= Int.unsigned i1)%Z ->
    (0 < z1)%Z ->
    (z1 < 4294967295)%Z ->
    (Int.unsigned i1 - Int.unsigned i2 ) / z1 = z2 ->
    Int.unsigned (Int.divu (Int.sub i1 i2) (Int.repr z1)) = z2.

Lemma Int_modu_to_Z_mod :
  forall i1 i2 z1 z2,
    (Int.unsigned i2 <= Int.unsigned i1)%Z ->
    (0 < z1)%Z ->
    (z1 < 4294967295)%Z ->
    (0 <= z2)%Z ->
    (z2 <= 4294967295)%Z ->
    (Int.unsigned i1 - Int.unsigned i2 ) mod z1 = z2 ->
    Int.modu (Int.sub i1 i2) (Int.repr z1) = Int.repr z2.

Theorem deref_ptr_of_array_member_rv´´´ :
  forall P s t´ t vl e l l´ x v n,
    s |= Aarray l t´ vl ** P->
    t´ = Tarray t n ->
    (Z.of_nat n < 4294967295)%Z ->
    s |= Rv e @ (Tptr t ) == Vptr l´ ->
    typelen t <> 0 ->
    fst l = fst l´ ->
    (Z.of_nat (typelen t) < 4294967295)%Z ->
    fst l = fst l´ ->
    (Int.unsigned (snd l) <= Int.unsigned (snd l´))%Z ->
    ((Int.unsigned (snd l´) - Int.unsigned (snd l)) / (Z_of_nat (typelen t)) = x)%Z ->
    ((Int.unsigned (snd l´) - Int.unsigned (snd l)) mod (Z_of_nat (typelen t)) = 0)%Z ->
    (x < Z.of_nat n)%Z ->
    (x < Z.of_nat (length vl))%Z ->
    rule_type_val_match t v = true ->
    nth_val´ (Z.to_nat x) vl = v ->
    s |= Rv (ederef e ) @ t == v.

Theorem deref_ptr_of_array_member_rv :
  forall P s t´ t vl e b i i´ x v n,
    s |= Rv e @ (Tptr t ) == Vptr (b ,i´) ->
    s |= Aarray (b ,i ) t´ vl ** P->
    t´ = Tarray t n ->
    (Z.of_nat n < 4294967295)%Z ->
    typelen t <> 0 ->
    (Z.of_nat (typelen t) < 4294967295)%Z ->
    (Int.unsigned i <= Int.unsigned i´)%Z ->
    ((Int.unsigned i´ - Int.unsigned i ) / (Z_of_nat (typelen t)) = x)%Z ->
    (Z_of_nat (typelen t) * x = (Int.unsigned i´ - Int.unsigned i ))%Z ->
    (x < Z.of_nat n)%Z ->
    (x < Z.of_nat (length vl))%Z ->
    rule_type_val_match t v = true ->
    nth_val´ (Z.to_nat x) vl = v ->
    s |= Rv (ederef e ) @ t == v.

Theorem var_rv :
  forall s x t l v P,
    s |= Rv (eaddrof (evar x)) @ Tptr t == Vptr l ->
    s |= PV l @ t |-> v ** P ->

    rule_type_val_match t v = true->
    s |= Rv (evar x ) @ t == v.

Axiom expr_struct_rv : forall s e t l id t' v' P, s |= Rv (eaddrof e) @ Tptr t == Vptr l -> s |= SP l @ t id @ t' |-> v' ** P -> s |= Rv (efield e id) @ t' == v'. *) Theorem addrof_deref_rv : forall s e t l, s |= Rv e @ (Tptr t) == (Vptr l) -> s |= Rv (eaddrof (ederef e)) @ (Tptr t) == (Vptr l). Proof. intros. destruct s as [[]]. destruct t0 as [[[[]]]]. simpl in *. destruct H. destruct H0. rewrite H0. destruct t;auto;tryfalse. Qed. Theorem addrof_lvar_rv : forall s x t l P, s |= L& x @ t == l ** P -> s |= Rv (eaddrof (evar x)) @ Tptr t == Vptr l. Proof. intros. destruct s as [[]]. destruct t0 as [[[[]]]]. simpl in *;mytac. rewrite H3. destruct l. simpl in H5. inverts H5. rewrite <- Int.unsigned_zero in H1. apply aux_for_hoare_lemmas.unsigned_zero in H1. subst. auto. rewrite H3. auto. intro. inverts H. Qed. Theorem addrof_array_elem_rv : forall s e1 e2 t1 t2 b i j t, s |= Rv e1 @ t1 == (Vptr (b,i)) -> s |= Rv e2 @ t2 == Vint32 j -> t2 = Tint8 \/ t2 = Tint16 \/ t2 = Tint32 -> (t1 = Tptr t \/ exists n, t1 = Tarray t n) -> s |= Rv (eaddrof (earrayelem e1 e2)) @ (Tptr t) == (Vptr (b,(Int.add i (Int.mul (Int.repr (Z.of_nat (typelen t))) j)))). Proof. intros. destruct s as [[]]. destruct t0 as [[[[]]]]. destruct H2. simpl in *;mytac. rewrite H5. rewrite H0. rewrite H3. destruct t2;destruct H1;tryfalse;destruct H1;tryfalse. rewrite H. auto. rewrite H;auto. rewrite H;auto. rewrite H5. rewrite H3. destruct t2;destruct H1;tryfalse;destruct H1;tryfalse;auto. auto. simpl in *;mytac. rewrite H5. rewrite H0. rewrite H3. destruct t2;destruct H1;tryfalse;destruct H1;tryfalse. rewrite H. auto. rewrite H;auto. rewrite H;auto. rewrite H5. rewrite H3. destruct t2;destruct H1;tryfalse;destruct H1;tryfalse;auto. auto. Qed. Theorem lvar_rv : forall s x t v P, s |= LV x @ t |-> v ** P -> (* v <> Vundef ->*) rule_type_val_match t v = true -> s |= Rv (evar x) @ t == v. Proof. intros. unfold Alvarmapsto in H. sep normal in H. sep_destruct H. eapply var_rv; auto. eapply addrof_lvar_rv. eauto. sep lift 2 in H; eauto. Qed. Theorem addrof_gvar_rv : forall s x t l P, s |= A_notin_lenv x ** G& x @ t == l ** P -> s |= Rv (eaddrof (evar x)) @ Tptr t == Vptr l. Proof. intros. destruct s as [[]]. destruct t0 as [[[[]]]]. simpl in *;mytac. lets H100 : EnvMod.nindom_get H3. rewrite H100. rewrite H8. destruct l. simpl in H10. inverts H10. rewrite <- Int.unsigned_zero in H1. apply aux_for_hoare_lemmas.unsigned_zero in H1. subst. auto. lets H100 : EnvMod.nindom_get H3. rewrite H100. rewrite H8. auto. intro. inverts H. Qed. Theorem gvar_rv' : forall s x t v P, s |= A_notin_lenv x ** GV x @ t |-> v ** P -> (*v <> Vundef ->*) rule_type_val_match t v = true -> s |= Rv (evar x) @ t == v. Proof. intros. unfold Agvarmapsto in H. sep normal in H; sep_destruct H. eapply var_rv; auto. eapply addrof_gvar_rv. sep lifts (3::1::nil)%list in H; eauto. sep lift 2 in H; eauto. Qed. Open Scope list_scope. Fixpoint var_notin_dom (x:var) (l:edom) := match l with | nil => true | (y,t)::l' => if BinInt.Z.eqb x y then false else (var_notin_dom x l') end. Close Scope list_scope. Lemma dom_lenv_imp_notin_lenv : forall l P x, var_notin_dom x l = true -> A_dom_lenv l ** P ==> A_notin_lenv x ** P. Proof. intros. simpl in *; mytac. destruct_s s; simpl in *; mytac. do 6 eexists; mytac; eauto. unfold eq_dom_env in *. intro. apply EnvMod.indom_get in H0. mytac. destruct x0. assert (exists b, EnvMod.get e0 x = Some (b, t)) by eauto. apply H4 in H1. gen H H1; clear; intros. induction l; simpl in *. auto. destruct a. remember (BinInt.Z.eqb x v) as bool; destruct bool. tryfalse. symmetry in Heqbool; apply BinInt.Z.eqb_neq in Heqbool. destruct H1. inverts H0; tryfalse. lets IHl1 : IHl H H0; auto. Qed. Theorem gvar_rv : forall s x t v l P, s |= A_dom_lenv l ** GV x @ t |-> v ** P -> var_notin_dom x l = true -> (* v <> Vundef ->*) rule_type_val_match t v = true -> s |= Rv (evar x) @ t == v. Proof. intros. eapply gvar_rv'; auto. eapply dom_lenv_imp_notin_lenv; eauto. Qed. Theorem null_rv : forall s, s |= Rv enull @ Tnull == Vnull. Proof. intros. destruct s as [ [ [ [ [ [ ] ] ] ] ] ]; simpl. auto. Qed. Theorem const_rv : forall s i, s |= Rv econst32 i @ Tint32 == Vint32 i. Proof. intros. destruct s as [ [ [ [ [ [ ] ] ] ] ] ]; simpl. auto. Qed. Lemma struct_member_rv': forall s x t l vl tid decl n id t' v P, (forall ids dl, t' <> Tstruct ids dl) -> (forall (t'0 : type) (n0 : nat), t' <> Tarray t'0 n0) -> rule_type_val_match t' v =true-> (*v<> Vundef ->*) good_decllist decl = true -> s |= LV x @ (Tptr t) |-> Vptr l ** Astruct l t vl ** P-> t = Tstruct tid decl -> nth_id n decl = Some id -> ftype id decl = Some t' -> nth_val n vl = Some v -> s |= Rv (efield (ederef (evar x)) id) @ t' == v. Proof. introv Hnstr. introv Hnarr. introv Htv. assert (v<> Vundef) as Hvn. eapply rule_type_val_match_nvundef;eauto. introv Hgooddecl. intros. destruct s as ((o&O)&aop). unfold sat in *;fold sat in *;mytac. unfold substmo in *. destruct o as [[[[]]]]. unfold substaskst in *. unfold getsmem in *. unfold getmem in *. unfold get_smem in *. unfold get_mem in *. simpl in *;mytac. rewrite H8. rewrite H2. rewrite Int.unsigned_zero in H10. lets Hf: mapstoval_loadbytes H10. simpl;auto. destruct Hf. destruct H. lets Hf: loadbytes_local H4 H. assert ( loadbytes m (x15, BinNums.Z0) (typelen (Tptr (Tstruct tid decl))) = Some x2);auto. unfold load;unfold loadm. rewrite H5. rewrite H0. clear H. destruct l. unfold getoff. unfold evaltype. rewrite H8. lets Hoff: nth_id_exists_off H1. destruct Hoff. rewrite H. assert (load t' x6 (addrval_to_addr (b, Int.add (Int.repr (Int.unsigned i0)) x3)) = Some v). unfold addrval_to_addr. rewrite struct_asrt_eq with (n:=n) in H12;eauto. unfold sat in H12;fold sat in H12;mytac. simpl in H15. rewrite Int.repr_unsigned. simpl in H7. eapply load_local;eauto. apply mapstoval_load;auto. simpl;auto. destruct H15;auto. auto. apply MemMod.join_comm in H4. eapply load_local;eauto. eapply load_local;eauto. destruct o as [[[[]]]]. simpl in *;mytac. rewrite H8. auto. auto. Qed. Theorem struct_member_rv'': forall s x t l vl tid decl n id t' v P, s |= LV x @ (Tptr t) |-> Vptr l ** Astruct l t vl ** P-> t = Tstruct tid decl -> good_decllist decl = true -> ftype id decl = Some t' -> (forall ids dl, t' <> Tstruct ids dl) -> (forall (t'0 : type) (n0 : nat), t' <> Tarray t'0 n0) -> id_nth id decl = Some n -> nth_val n vl = Some v -> (*v <> Vundef ->*) rule_type_val_match t' v = true -> s |= Rv (efield (ederef (evar x)) id) @ t' == v. Proof. intros. eapply struct_member_rv';eauto. eapply id_nth_eq;eauto. Qed. Lemma id_nth_eq_0 : forall id i t decl, id_nth id (dcons i t decl) = Some 0 -> Zeq_bool id i = true. Proof. intros. unfold id_nth in *. unfold1 id_nth' in *. remember (Zeq_bool id i) as X. destruct X;tryfalse. auto. apply id_nth_ge in H. omega. Qed. Lemma id_nth_ueq_0 : forall id i t n decl, id_nth id (dcons i t decl) = Some (S n) -> Zeq_bool id i = false /\ id_nth id decl = Some n. Proof. intros. unfold id_nth in *. assert (Zeq_bool id i = false). unfold1 id_nth' in *. remember (Zeq_bool id i ) as X. destruct X. inverts H. auto. split;auto. clear -H. unfold1 id_nth' in H. remember (Zeq_bool id i) as X. destruct X;tryfalse. apply id_nth'_suc;auto. Qed. Theorem struct_member_rv: forall s x t l vl tid decl n id t' v P, s |= LV x @ (Tptr t) |-> Vptr l ** Astruct l t vl ** P -> t = Tstruct tid decl -> good_decllist decl = true -> ftype id decl = Some t' -> (forall ids dl, t' <> Tstruct ids dl) -> (forall (t'0 : type) (n0 : nat), t' <> Tarray t'0 n0) -> id_nth id decl = Some n -> n < length vl -> struct_type_vallist_match t vl -> nth_val' n vl = v -> s |= Rv (efield (ederef (evar x)) id) @ t' == v. Proof. intros. subst v. assert (rule_type_val_match t' (nth_val' n vl) = true). subst t. unfold struct_type_vallist_match in H7. clear l x s H P tid. gen vl decl n id t'. induction vl,decl, n; intros; simpl in *; tryfalse. apply id_nth_eq_0 in H5; subst. rewrite H5 in H2. inverts H2. destruct t'; intuition auto. false. exact (H4 t' n eq_refl). false. eapply H3; eauto. eapply IHvl; eauto. 4 : instantiate (1 := decl). 4 : instantiate (1 := id). apply andb_true_iff in H1; mytac; auto. destruct t; intuition auto. omega. apply id_nth_ueq_0 in H5; intuition auto. apply id_nth_ueq_0 in H5; mytac. rewrite H in H2. auto. eapply struct_member_rv''; eauto. apply nth_val_imp_nth_val'_2; auto. Qed. Lemma struct_member_rv_g': forall s x t l vl tid decl n id t' v P, (forall ids dl, t' <> Tstruct ids dl) -> (forall (t'0 : type) (n0 : nat), t' <> Tarray t'0 n0) -> rule_type_val_match t' v =true-> (*v<> Vundef ->*) good_decllist decl = true -> s |= (A_notin_lenv x ** GV x @ (Tptr t) |-> Vptr l) ** Astruct l t vl ** P-> t = Tstruct tid decl -> nth_id n decl = Some id -> ftype id decl = Some t' -> nth_val n vl = Some v -> s |= Rv (efield (ederef (evar x)) id) @ t' == v. Proof. introv Hnstr. introv Hnarr. introv Htv. assert (v<> Vundef) as Hvn. eapply rule_type_val_match_nvundef;eauto. introv Hgooddecl. intros. destruct s as ((o&O)&aop). unfold sat in *;fold sat in *;mytac. unfold substmo in *. destruct o as [[[[]]]]. unfold substaskst in *. unfold getsmem in *. unfold getmem in *. unfold get_smem in *. unfold get_mem in *. simpl in *;mytac. apply EnvMod.nindom_get in H17. rewrite H17. rewrite H8. rewrite Int.unsigned_zero in H10. lets Hf: mapstoval_loadbytes H10. simpl;auto. destruct Hf. destruct H. lets Hf: loadbytes_local H4 H. assert ( loadbytes m (x19, BinNums.Z0) (typelen (Tptr (Tstruct tid decl))) = Some x2);auto. unfold load;unfold loadm. rewrite H2. rewrite H5. rewrite H0. clear H. destruct l. unfold getoff. unfold evaltype. rewrite H17. rewrite H8. lets Hoff: nth_id_exists_off H1. destruct Hoff. rewrite H. assert (load t' x1 (addrval_to_addr (b, Int.add (Int.repr (Int.unsigned i0)) x3)) = Some v). unfold addrval_to_addr. rewrite struct_asrt_eq with (n:=n) in H12;eauto. unfold sat in H12;fold sat in H12;mytac. simpl in H7. rewrite Int.repr_unsigned. simpl in H15. eapply load_local;eauto. eapply load_local;eauto. apply mapstoval_load;auto. destruct H15;auto. apply MemMod.join_comm in H4. eapply load_local;eauto. destruct o as [[[[]]]]. simpl in *;mytac. apply EnvMod.nindom_get in H17. rewrite H17. rewrite H8. auto. auto. Qed. Theorem struct_member_rv_g'': forall s x t l vl tid decl n id t' v P, s |= (A_notin_lenv x ** GV x @ (Tptr t) |-> Vptr l) ** Astruct l t vl ** P -> t = Tstruct tid decl -> good_decllist decl = true -> ftype id decl = Some t' -> (forall ids dl, t' <> Tstruct ids dl) -> (forall (t'0 : type) (n0 : nat), t' <> Tarray t'0 n0) -> id_nth id decl = Some n -> nth_val n vl = Some v -> (*v <> Vundef ->*) rule_type_val_match t' v = true -> s |= Rv (efield (ederef (evar x)) id) @ t' == v. Proof. intros. eapply struct_member_rv_g';eauto. eapply id_nth_eq;eauto. Qed. Theorem struct_member_rv_g''': forall s ls x t l vl tid decl n id t' v P, s |= A_dom_lenv ls ** GV x @ (Tptr t) |-> Vptr l ** Astruct l t vl ** P-> var_notin_dom x ls = true -> t = Tstruct tid decl -> good_decllist decl = true -> ftype id decl = Some t' -> (forall ids dl, t' <> Tstruct ids dl) -> (forall (t'0 : type) (n0 : nat), t' <> Tarray t'0 n0) -> id_nth id decl = Some n -> nth_val n vl = Some v -> (*v <> Vundef ->*) rule_type_val_match t' v = true -> s |= Rv (efield (ederef (evar x)) id) @ t' == v. Proof. intros. eapply struct_member_rv_g''; eauto. sep normal. eapply dom_lenv_imp_notin_lenv; eauto. Qed. Theorem struct_member_rv_g: forall s ls x t l vl tid decl n id t' v P, s |= A_dom_lenv ls ** GV x @ (Tptr t) |-> Vptr l ** Astruct l t vl ** P-> var_notin_dom x ls = true -> t = Tstruct tid decl -> good_decllist decl = true -> ftype id decl = Some t' -> (forall ids dl, t' <> Tstruct ids dl) -> (forall (t'0 : type) (n0 : nat), t' <> Tarray t'0 n0) -> id_nth id decl = Some n -> n < length vl -> struct_type_vallist_match t vl -> nth_val' n vl = v -> s |= Rv (efield (ederef (evar x)) id) @ t' == v. Proof. intros. subst v. assert (rule_type_val_match t' (nth_val' n vl) = true). subst t. unfold struct_type_vallist_match in H8. clear l x s H H0 P tid ls. gen vl decl n id t'. induction vl,decl, n; intros; simpl in *; tryfalse. apply id_nth_eq_0 in H6; subst. rewrite H6 in H3. inverts H3. destruct t'; intuition auto. false. exact (H5 t' n eq_refl). false. eapply H4; eauto. eapply IHvl; eauto. 4 : instantiate (1 := decl). 4 : instantiate (1 := id). apply andb_true_iff in H2; mytac; auto. destruct t; intuition auto. omega. apply id_nth_ueq_0 in H6; intuition auto. apply id_nth_ueq_0 in H6; mytac. rewrite H in H3. auto. eapply struct_member_rv_g'''; eauto. apply nth_val_imp_nth_val'_2; auto. Qed. Theorem struct_member_array_rv_g: forall s ls x t l vl tid decl id t' n P ad, s |= A_dom_lenv ls ** GV x @ (Tptr t) |-> Vptr l ** Astruct l t vl ** P-> var_notin_dom x ls = true -> t = Tstruct tid decl -> good_decllist decl = true -> ftype id decl = Some (Tarray t' n) -> id_addrval l id t = Some ad -> s |= Rv (efield (ederef (evar x)) id) @ (Tarray t' n) == Vptr ad. Proof. intros. destruct_s s. eapply dom_lenv_imp_notin_lenv in H; eauto. simpl in *;mytac. apply EnvMod.nindom_get in H8;auto. rewrite H8. rewrite H23. rewrite H3. unfold load;unfold loadm. rewrite Int.unsigned_zero in H24. lets Hf: mapstoval_loadbytes H24. simpl;auto. destruct Hf. destruct H. lets Hf: loadbytes_local H10 H. assert ( loadbytes m (x25, 0%Z) (typelen (Tptr (Tstruct tid decl))) = Some x0);auto. rewrite H5. rewrite H1. destruct l. unfold getoff. unfold evaltype. rewrite H8;rewrite H23. unfold id_addrval in H4. remember (field_offset id decl ) as X. destruct X;tryfalse. rewrite Int.repr_unsigned. simpl. rewrite Int.repr_unsigned. inverts H4;auto. apply EnvMod.nindom_get in H8;auto. rewrite H8;rewrite H23. auto. auto. Qed. Definition isarray_type t:= exists t'' n, t = Tarray t'' n. Theorem struct_member_rv_g_general: forall s ls x t l vl tid decl id P v t', s |= A_dom_lenv ls ** GV x @ (Tptr t) |-> Vptr l ** Astruct l t vl ** P-> var_notin_dom x ls = true -> t = Tstruct tid decl -> good_decllist decl = true -> ftype id decl = Some t' -> ( isarray_type t'-> exists ad, id_addrval l id t = Some ad /\ v = Vptr ad ) -> ( ~ isarray_type t' -> ( exists n, (forall a b, t' <> Tstruct a b) /\ id_nth id decl = Some n /\ n < length vl /\ struct_type_vallist_match t vl /\ nth_val' n vl = v ) ) -> s |= Rv (efield (ederef (evar x)) id) @ t' == v. Proof. intros. mytac. assert (isarray_type t' \/ ~isarray_type t' ). tauto. destruct H1. lets Hx: H4 H1. mytac. unfolds in H1;mytac. eapply struct_member_array_rv_g;eauto. lets Hx : H5 H1. mytac. eapply struct_member_rv_g;eauto. unfold isarray_type in H1. intros. introv. introv Hf. apply H1;eauto. Qed. Theorem struct_member_array_rv: forall s x t l vl tid decl id t' n P ad, s |= LV x @ (Tptr t) |-> Vptr l ** Astruct l t vl ** P-> t = Tstruct tid decl -> good_decllist decl = true -> ftype id decl = Some (Tarray t' n) -> id_addrval l id t = Some ad -> s |= Rv (efield (ederef (evar x)) id) @ (Tarray t' n) == Vptr ad. Proof. intros. destruct_s s. simpl in *;mytac. rewrite H17. rewrite H2. unfold load;unfold loadm. rewrite Int.unsigned_zero in H18. lets Hf: mapstoval_loadbytes H18. simpl;auto. destruct Hf. destruct H. lets Hf: loadbytes_local H4 H. assert ( loadbytes m (x19, 0%Z) (typelen (Tptr (Tstruct tid decl))) = Some x2);auto. rewrite H5. rewrite H0. destruct l. unfold getoff. unfold evaltype. rewrite H17. unfold id_addrval in H3. remember (field_offset id decl ) as X. destruct X;tryfalse. rewrite Int.repr_unsigned. simpl. rewrite Int.repr_unsigned. inverts H3;auto. rewrite H17. auto. auto. Qed. Theorem struct_offset_rv : forall s e t tid decl a id t' off, s |= Rv eaddrof e @ Tptr t == Vptr a -> t = Tstruct tid decl -> field_offset id decl = Some off -> ftype id decl = Some t' -> s |= Rv eaddrof (efield e id) @ Tptr t' == Vptr (fst a, Int.add (snd a) off). Proof. intros. unfold sat in *. destruct H. destruct H3. subst t. destruct s as [[]]. destruct t as [[[[]]]]. unfold getsmem in *. unfold get_smem in *. splits;auto. assert (evaltype e (e0, e1, m) = Some (Tstruct tid decl)). eapply eval_type_addr_eq;eauto. simpl. rewrite H0. rewrite H2. destruct a. apply eval_addr_eq in H. rewrite H. simpl. unfold getoff. rewrite H0. rewrite H1. simpl. assert (Int.repr (Int.unsigned i0)=i0). apply Int.repr_unsigned. rewrite H5. auto. simpl. assert (evaltype e (e0, e1, m) = Some (Tstruct tid decl)). eapply eval_type_addr_eq;eauto. rewrite H0. rewrite H2. auto. Qed. Theorem struct_member_rv_general: forall s x t l vl tid decl id P v t', s |= LV x @ (Tptr t) |-> Vptr l ** Astruct l t vl ** P-> t = Tstruct tid decl -> good_decllist decl = true -> ftype id decl = Some t' -> ( isarray_type t'-> exists ad, id_addrval l id t = Some ad /\ v = Vptr ad ) -> ( ~ isarray_type t' -> ( exists n, (forall a b, t' <> Tstruct a b) /\ id_nth id decl = Some n /\ n < length vl /\ struct_type_vallist_match t vl /\ nth_val' n vl = v ) ) -> s |= Rv (efield (ederef (evar x)) id) @ t' == v. Proof. intros. mytac. assert (isarray_type t' \/ ~isarray_type t' ). tauto. destruct H0. lets Hx: H3 H0. mytac. unfolds in H0;mytac. eapply struct_member_array_rv;eauto. lets Hx : H4 H0. mytac. eapply struct_member_rv;eauto. unfold isarray_type in H0. intros. introv. introv Hf. apply H0;eauto. Qed. Lemma int_Z_ltu: forall m n, Int.ltu m (Int.repr (Z.of_nat n)) = true-> BinInt.Z.abs_nat (Int.unsigned m) < n. Proof. intros. unfold Int.ltu in H. destruct (Coqlib.zlt (Int.unsigned m) (Int.unsigned (Int.repr (Z.of_nat n)))); tryfalse. clear H. rewrite Zabs2Nat.abs_nat_nonneg. rewrite Int.unsigned_repr_eq in l. pose proof Zmod_le (Z.of_nat n) Int.modulus. assert (0 < Int.modulus)%Z. unfold Int.modulus. unfold Int.wordsize. unfold Wordsize_32.wordsize. unfold two_power_nat. unfold shift_nat. simpl. omega. assert (0 <= Z.of_nat n)%Z. omega. pose proof H H0 H1; clear H H0 H1. assert (Int.unsigned m < Z.of_nat n)%Z. omega. rewrite <- Nat2Z.id. apply Z2Nat.inj_lt. pose proof Int.unsigned_range m. destruct H0. auto. omega. auto. pose proof Int.unsigned_range m. destruct H. auto. Qed. Theorem array_member_rv' : forall s x t te2 l vl n m v e2 P, s |= Alvarenv x (Tarray t n) (addrval_to_addr l) ** Aarray l (Tarray t n) vl ** P -> s |= Rv e2 @ te2 == Vint32 m -> te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 -> Int.ltu m Int.zero = false -> Int.ltu m (Int.repr (BinInt.Z_of_nat n)) = true -> (* Int.cmp Cge m Int.zero = true -> Int.cmp Clt m (Int.repr (BinInt.Z_of_nat n)) =true ->*) nth_val (BinInt.Z.abs_nat (Int.unsigned m)) vl = Some v -> (*v<> Vundef ->*) rule_type_val_match t v =true-> s |= Rv (earrayelem (evar x) e2) @ t == v. Proof. intros. rename H5 into Htv. assert (v<> Vundef). eapply rule_type_val_match_nvundef;eauto. destruct s as ((o&O)&aop). destruct l as (b&i). unfold sat in *;fold sat in *;mytac. unfold substmo in *. destruct o as [[[[]]]]. unfold substaskst in *. unfold getsmem in *. unfold getmem in *. unfold get_smem in *. unfold get_mem in *. simpl in *;mytac. rewrite H11. rewrite H6. destruct H1. rewrite H. rewrite H0. erewrite array_asrt_eq in H16;eauto. unfold sat in H16;fold sat in H16;mytac. simpl in H16. destruct H14. rewrite <- Int.unsigned_zero in H12. apply aux_for_hoare_lemmas.unsigned_zero in H12. subst i. assert (Int.repr (BinInt.Z.of_nat (BinInt.Z.abs_nat (Int.unsigned m))) = m). rewrite Nat2Z.inj_abs_nat. rewrite Z.abs_eq. apply Int.repr_unsigned. lets H100:Int.unsigned_range m. omega. rewrite H9 in H. lets Hf: mapstoval_loadbytes H. auto. destruct Hf. destruct H12. assert (loadbytes m0 (x12, Int.unsigned (Int.add Int.zero (Int.mul (Int.repr (BinInt.Z.of_nat (typelen t))) m))) (typelen t) = Some x2). eapply loadbytes_local;eauto. eapply loadbytes_local;eauto. unfold load;unfold loadm. simpl addr_to_addrval. simpl. rewrite Int.repr_unsigned. rewrite H18. destruct t;auto;simpl in Htv;tryfalse; rewrite H14;auto. eapply int_Z_ltu;eauto. destruct H. rewrite H. rewrite H0. erewrite array_asrt_eq in H16;eauto. unfold sat in H16;fold sat in H16;mytac. simpl in H16. destruct H14. rewrite <- Int.unsigned_zero in H12. apply aux_for_hoare_lemmas.unsigned_zero in H12. subst i. assert (Int.repr (BinInt.Z.of_nat (BinInt.Z.abs_nat (Int.unsigned m))) = m). rewrite Nat2Z.inj_abs_nat. rewrite Z.abs_eq. apply Int.repr_unsigned. lets H100:Int.unsigned_range m. omega. rewrite H9 in H. lets Hf: mapstoval_loadbytes H. auto. destruct Hf. destruct H12. assert (loadbytes m0 (x12, Int.unsigned (Int.add Int.zero (Int.mul (Int.repr (BinInt.Z.of_nat (typelen t))) m))) (typelen t) = Some x2). eapply loadbytes_local;eauto. eapply loadbytes_local;eauto. unfold load;unfold loadm. simpl addr_to_addrval. simpl. rewrite Int.repr_unsigned. rewrite H18. destruct t;auto;simpl in Htv;tryfalse; rewrite H14;auto. eapply int_Z_ltu;eauto. rewrite H. rewrite H0. erewrite array_asrt_eq in H16;eauto. unfold sat in H16;fold sat in H16;mytac. simpl in H16. destruct H14. rewrite <- Int.unsigned_zero in H12. apply aux_for_hoare_lemmas.unsigned_zero in H12. subst i. assert (Int.repr (BinInt.Z.of_nat (BinInt.Z.abs_nat (Int.unsigned m))) = m). rewrite Nat2Z.inj_abs_nat. rewrite Z.abs_eq. apply Int.repr_unsigned. lets H100:Int.unsigned_range m. omega. rewrite H9 in H. lets Hf: mapstoval_loadbytes H. auto. destruct Hf. destruct H12. assert (loadbytes m0 (x12, Int.unsigned (Int.add Int.zero (Int.mul (Int.repr (BinInt.Z.of_nat (typelen t))) m))) (typelen t) = Some x2). eapply loadbytes_local;eauto. eapply loadbytes_local;eauto. unfold load;unfold loadm. simpl addr_to_addrval. simpl. rewrite Int.repr_unsigned. rewrite H18. destruct t;auto;simpl in Htv;tryfalse; rewrite H14;auto. eapply int_Z_ltu;eauto. destruct o as [[[[]]]]. simpl in *;mytac. rewrite H11. rewrite H6. destruct H1. rewrite H. auto. destruct H;rewrite H;auto. auto. Qed. Theorem array_member_rv'' : forall s x t t' te2 vl n m v e2 P, s |= LAarray x t' vl ** P -> t' = Tarray t n -> s |= Rv e2 @ te2 == Vint32 m -> te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 -> Int.ltu m (Int.repr (BinInt.Z_of_nat n)) = true -> nth_val (BinInt.Z.abs_nat (Int.unsigned m)) vl = Some v -> (*v<> Vundef ->*) rule_type_val_match t v =true-> s |= Rv (earrayelem (evar x) e2) @ t == v. Proof. intros. unfold LAarray in H. unfold Alvarenv' in H. sep normal in H; sep destruct H. subst t'. eapply array_member_rv'; eauto. unfold Int.ltu. rewrite Int.unsigned_zero. remember (zlt (Int.unsigned m) 0 ) as X. destruct X. clear -l. lets H100:Int.unsigned_range m. omega. auto. Qed. Theorem array_member_rv : forall s x t t' te2 vl n m e2 v P, s |= LAarray x t' vl ** P -> t' = Tarray t n -> s |= Rv e2 @ te2 == Vint32 m -> te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 -> (Z.of_nat n < 4294967295)%Z -> (Int.unsigned m < Z.of_nat n)%Z -> (Int.unsigned m < Z.of_nat (length vl))%Z -> rule_type_val_match t v = true -> nth_val' (Z.to_nat (Int.unsigned m)) vl = v -> s |= Rv (earrayelem (evar x) e2) @ t == v. Proof. intros. subst v. eapply array_member_rv''; eauto. unfold Int.ltu. rewrite Int.unsigned_repr. apply zlt_true. auto. split; try omega. unfold Int.max_unsigned. unfold Int.modulus. unfold two_power_nat, Int.wordsize. unfold shift_nat, Wordsize_32.wordsize. unfold nat_iter. omega. apply nth_val_imp_nth_val'_1; auto. Qed. (* apply array_type_vallist_match_imp_rule_type_val_match; auto. apply Nat2Z.inj_lt. rewrite Z2Nat.id. auto. lets H100 : Int.unsigned_range m. omega. Qed. *) Theorem array_member_rv_g' : forall s x t te2 l vl n m v e2 P, s |= (A_notin_lenv x ** Agvarenv x (Tarray t n) (addrval_to_addr l)) ** Aarray l (Tarray t n) vl ** P-> s |= Rv e2 @ te2 == Vint32 m -> te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 -> Int.ltu m Int.zero = false -> Int.ltu m (Int.repr (BinInt.Z_of_nat n)) =true -> nth_val (BinInt.Z.abs_nat (Int.unsigned m)) vl = Some v -> (* v<> Vundef -> *) rule_type_val_match t v = true-> s |= Rv (earrayelem (evar x) e2) @ t == v. Proof. intros. rename H5 into Htv. assert (v<>Vundef). eapply rule_type_val_match_nvundef;eauto. destruct s as ((o&O)&aop). destruct l as (b&i). unfold sat in *;fold sat in *;mytac. unfold substmo in *. destruct o as [[[[]]]]. unfold substaskst in *. unfold getsmem in *. unfold getmem in *. unfold get_smem in *. unfold get_mem in *. simpl in *;mytac. apply EnvMod.nindom_get in H21. rewrite H21. rewrite H22. rewrite H6. destruct H1. rewrite H. rewrite H0. erewrite array_asrt_eq in H16;eauto. unfold sat in H16;fold sat in H16;mytac. simpl in H12. destruct H12. rewrite <- Int.unsigned_zero in H9. apply aux_for_hoare_lemmas.unsigned_zero in H9. subst i. assert (Int.repr (BinInt.Z.of_nat (BinInt.Z.abs_nat (Int.unsigned m))) = m). rewrite Nat2Z.inj_abs_nat. rewrite Z.abs_eq. apply Int.repr_unsigned. lets H100:Int.unsigned_range m. omega. rewrite H9 in H. lets Hf: mapstoval_loadbytes H. auto. destruct Hf. destruct H10. assert (loadbytes m0 (x18, Int.unsigned (Int.add Int.zero (Int.mul (Int.repr (BinInt.Z.of_nat (typelen t))) m))) (typelen t) = Some x2). eapply loadbytes_local;eauto. eapply loadbytes_local;eauto. unfold load;unfold loadm. simpl addr_to_addrval. simpl. rewrite Int.repr_unsigned. rewrite H16. destruct t;auto;simpl in Htv;tryfalse; rewrite H12;auto. eapply int_Z_ltu;eauto. destruct H. rewrite H. rewrite H0. erewrite array_asrt_eq in H16;eauto. unfold sat in H16;fold sat in H16;mytac. simpl in H12. destruct H12. rewrite <- Int.unsigned_zero in H9. apply aux_for_hoare_lemmas.unsigned_zero in H9. subst i. assert (Int.repr (BinInt.Z.of_nat (BinInt.Z.abs_nat (Int.unsigned m))) = m). rewrite Nat2Z.inj_abs_nat. rewrite Z.abs_eq. apply Int.repr_unsigned. lets H100:Int.unsigned_range m. omega. rewrite H9 in H. lets Hf: mapstoval_loadbytes H. auto. destruct Hf. destruct H10. assert (loadbytes m0 (x18, Int.unsigned (Int.add Int.zero (Int.mul (Int.repr (BinInt.Z.of_nat (typelen t))) m))) (typelen t) = Some x2). eapply loadbytes_local;eauto. eapply loadbytes_local;eauto. unfold load;unfold loadm. simpl addr_to_addrval. simpl. rewrite Int.repr_unsigned. rewrite H16. destruct t;auto;simpl in Htv;tryfalse; rewrite H12;auto. eapply int_Z_ltu;eauto. rewrite H. rewrite H0. erewrite array_asrt_eq in H16;eauto. unfold sat in H16;fold sat in H16;mytac. simpl in H12. destruct H12. rewrite <- Int.unsigned_zero in H9. apply aux_for_hoare_lemmas.unsigned_zero in H9. subst i. assert (Int.repr (BinInt.Z.of_nat (BinInt.Z.abs_nat (Int.unsigned m))) = m). rewrite Nat2Z.inj_abs_nat. rewrite Z.abs_eq. apply Int.repr_unsigned. lets H100:Int.unsigned_range m. omega. rewrite H9 in H. lets Hf: mapstoval_loadbytes H. auto. destruct Hf. destruct H10. assert (loadbytes m0 (x18, Int.unsigned (Int.add Int.zero (Int.mul (Int.repr (BinInt.Z.of_nat (typelen t))) m))) (typelen t) = Some x2). eapply loadbytes_local;eauto. eapply loadbytes_local;eauto. unfold load;unfold loadm. simpl addr_to_addrval. simpl. rewrite Int.repr_unsigned. rewrite H16. destruct t;auto;simpl in Htv;tryfalse; rewrite H12;auto. eapply int_Z_ltu;eauto. destruct o as [[[[]]]]. simpl in *;mytac. apply EnvMod.nindom_get in H21. rewrite H21. rewrite H22. rewrite H6. destruct H1. rewrite H. auto. destruct H;rewrite H;auto. auto. Qed. Theorem array_member_rv_g'' : forall s ls x t t' te2 vl n m v e2 P, s |= A_dom_lenv ls ** GAarray x t' vl ** P-> var_notin_dom x ls = true -> t' = Tarray t n -> s |= Rv e2 @ te2 == Vint32 m -> te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 -> Int.ltu m (Int.repr (BinInt.Z_of_nat n)) =true -> nth_val (BinInt.Z.abs_nat (Int.unsigned m)) vl = Some v -> (*v<> Vundef ->*) rule_type_val_match t v = true-> s |= Rv (earrayelem (evar x) e2) @ t == v. Proof. intros. unfold GAarray in H; unfold Agvarenv' in H. sep normal in H; sep destruct H. subst t'. eapply array_member_rv_g'; eauto. sep normal. eapply dom_lenv_imp_notin_lenv; eauto. sep auto. unfold Int.ltu. rewrite Int.unsigned_zero. remember (zlt (Int.unsigned m) 0 ) as X. destruct X. clear -l. lets H100:Int.unsigned_range m. omega. auto. Qed. Theorem array_member_rv_g : forall s ls x t t' te2 vl n m e2 v P vm, s |= A_dom_lenv ls ** GAarray x t' vl ** P-> var_notin_dom x ls = true -> t' = Tarray t n -> s |= Rv e2 @ te2 == vm -> vm = Vint32 m -> te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 -> (Z.of_nat n < 4294967295)%Z -> (Int.unsigned m < Z.of_nat n)%Z -> (Int.unsigned m < Z.of_nat (length vl))%Z -> rule_type_val_match t v = true -> nth_val' (Z.to_nat (Int.unsigned m)) vl = v -> s |= Rv (earrayelem (evar x) e2) @ t == v. Proof. intros. subst vm. subst v. eapply array_member_rv_g''; eauto. unfold Int.ltu. rewrite Int.unsigned_repr. apply zlt_true. auto. auto. split; try omega. unfold Int.max_unsigned. unfold Int.modulus. unfold two_power_nat, Int.wordsize. unfold shift_nat, Wordsize_32.wordsize. unfold nat_iter. omega. apply nth_val_imp_nth_val'_1; auto. Qed. (* apply array_type_vallist_match_imp_rule_type_val_match; auto. apply Nat2Z.inj_lt. rewrite Z2Nat.id. auto. lets H100 : Int.unsigned_range m. omega. Qed. *) Theorem expr_array_member_rv' : forall s e1 t te1 te2 l vl n m v e2 P, s |= Aarray l (Tarray t n) vl ** P -> s |= Rv e1 @ te1 == Vptr l -> s |= Rv e2 @ te2 == Vint32 m -> te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 -> Int.ltu m Int.zero = false -> Int.ltu m (Int.repr (BinInt.Z_of_nat n)) = true -> nth_val (BinInt.Z.abs_nat (Int.unsigned m)) vl = Some v -> rule_type_val_match t v =true-> te1 = Tarray t n \/ te1 = Tptr t -> s |= Rv (earrayelem e1 e2) @ t == v. Proof. intros. rename H6 into Htv. rename H7 into Hte1. assert (v<> Vundef). eapply rule_type_val_match_nvundef;eauto. destruct s as ((o&O)&aop). destruct l as (b&i). unfold sat in *;fold sat in *;mytac. unfold substmo in *. destruct o as [[[[]]]]. unfold substaskst in *. unfold getsmem in *. unfold getmem in *. unfold get_smem in *. unfold get_mem in *. simpl in *;mytac. rewrite H9. rewrite H7. rewrite H0. rewrite H1. destruct Hte1;destruct te1;tryfalse. destruct H2. subst te2. inverts H. erewrite array_asrt_eq in H14;eauto. unfold sat in H14;fold sat in H14;mytac. simpl in H17. destruct H16. simpl in H. lets Hf: mapstoval_loadbytes H. auto. destruct Hf. destruct H16. assert (loadbytes m0 (b, Int.unsigned (Int.add i (Int.mul (Int.repr (Z.of_nat (typelen t))) (Int.repr (Z.of_nat (Z.abs_nat (Int.unsigned m))))))) (typelen t) = Some x5 ). eapply loadbytes_local;eauto. eapply loadbytes_local;eauto. rewrite Nat2Z.inj_abs_nat in H19. rewrite Z.abs_eq in H19. rewrite Int.repr_unsigned in H19. unfold load;unfold loadm. simpl addr_to_addrval. simpl. rewrite Int.repr_unsigned. rewrite H19. destruct t;auto;simpl in Htv;tryfalse; rewrite H18;auto. lets H100:Int.unsigned_range m. omega. eapply int_Z_ltu;eauto. destruct H2;subst te2. inverts H. erewrite array_asrt_eq in H14;eauto. unfold sat in H14;fold sat in H14;mytac. simpl in H17. destruct H16. simpl in H. lets Hf: mapstoval_loadbytes H. auto. destruct Hf. destruct H16. assert (loadbytes m0 (b, Int.unsigned (Int.add i (Int.mul (Int.repr (Z.of_nat (typelen t))) (Int.repr (Z.of_nat (Z.abs_nat (Int.unsigned m))))))) (typelen t) = Some x5 ). eapply loadbytes_local;eauto. eapply loadbytes_local;eauto. rewrite Nat2Z.inj_abs_nat in H19. rewrite Z.abs_eq in H19. rewrite Int.repr_unsigned in H19. unfold load;unfold loadm. simpl addr_to_addrval. simpl. rewrite Int.repr_unsigned. rewrite H19. destruct t;auto;simpl in Htv;tryfalse; rewrite H18;auto. lets H100:Int.unsigned_range m. omega. eapply int_Z_ltu;eauto. inverts H. erewrite array_asrt_eq in H14;eauto. unfold sat in H14;fold sat in H14;mytac. simpl in H17. destruct H16. simpl in H. lets Hf: mapstoval_loadbytes H. auto. destruct Hf. destruct H16. assert (loadbytes m0 (b, Int.unsigned (Int.add i (Int.mul (Int.repr (Z.of_nat (typelen t))) (Int.repr (Z.of_nat (Z.abs_nat (Int.unsigned m))))))) (typelen t) = Some x5 ). eapply loadbytes_local;eauto. eapply loadbytes_local;eauto. rewrite Nat2Z.inj_abs_nat in H19. rewrite Z.abs_eq in H19. rewrite Int.repr_unsigned in H19. unfold load;unfold loadm. simpl addr_to_addrval. simpl. rewrite Int.repr_unsigned. rewrite H19. destruct t;auto;simpl in Htv;tryfalse; rewrite H18;auto. lets H100:Int.unsigned_range m. omega. eapply int_Z_ltu;eauto. destruct H2. subst te2. inverts H. erewrite array_asrt_eq in H14;eauto. unfold sat in H14;fold sat in H14;mytac. simpl in H17. destruct H16. simpl in H. lets Hf: mapstoval_loadbytes H. auto. destruct Hf. destruct H16. assert (loadbytes m0 (b, Int.unsigned (Int.add i (Int.mul (Int.repr (Z.of_nat (typelen t))) (Int.repr (Z.of_nat (Z.abs_nat (Int.unsigned m))))))) (typelen t) = Some x5 ). eapply loadbytes_local;eauto. eapply loadbytes_local;eauto. rewrite Nat2Z.inj_abs_nat in H19. rewrite Z.abs_eq in H19. rewrite Int.repr_unsigned in H19. unfold load;unfold loadm. simpl addr_to_addrval. simpl. rewrite Int.repr_unsigned. rewrite H19. destruct t;auto;simpl in Htv;tryfalse; rewrite H18;auto. lets H100:Int.unsigned_range m. omega. eapply int_Z_ltu;eauto. destruct H2;subst te2. inverts H. erewrite array_asrt_eq in H14;eauto. unfold sat in H14;fold sat in H14;mytac. simpl in H17. destruct H16. simpl in H. lets Hf: mapstoval_loadbytes H. auto. destruct Hf. destruct H16. assert (loadbytes m0 (b, Int.unsigned (Int.add i (Int.mul (Int.repr (Z.of_nat (typelen t))) (Int.repr (Z.of_nat (Z.abs_nat (Int.unsigned m))))))) (typelen t) = Some x5 ). eapply loadbytes_local;eauto. eapply loadbytes_local;eauto. rewrite Nat2Z.inj_abs_nat in H19. rewrite Z.abs_eq in H19. rewrite Int.repr_unsigned in H19. unfold load;unfold loadm. simpl addr_to_addrval. simpl. rewrite Int.repr_unsigned. rewrite H19. destruct t;auto;simpl in Htv;tryfalse; rewrite H18;auto. lets H100:Int.unsigned_range m. omega. eapply int_Z_ltu;eauto. inverts H. erewrite array_asrt_eq in H14;eauto. unfold sat in H14;fold sat in H14;mytac. simpl in H17. destruct H16. simpl in H. lets Hf: mapstoval_loadbytes H. auto. destruct Hf. destruct H16. assert (loadbytes m0 (b, Int.unsigned (Int.add i (Int.mul (Int.repr (Z.of_nat (typelen t))) (Int.repr (Z.of_nat (Z.abs_nat (Int.unsigned m))))))) (typelen t) = Some x5 ). eapply loadbytes_local;eauto. eapply loadbytes_local;eauto. rewrite Nat2Z.inj_abs_nat in H19. rewrite Z.abs_eq in H19. rewrite Int.repr_unsigned in H19. unfold load;unfold loadm. simpl addr_to_addrval. simpl. rewrite Int.repr_unsigned. rewrite H19. destruct t;auto;simpl in Htv;tryfalse; rewrite H18;auto. lets H100:Int.unsigned_range m. omega. eapply int_Z_ltu;eauto. destruct o as [[[[]]]]. simpl in *;mytac. rewrite H9. rewrite H7. destruct Hte1;destruct H2;subst;auto. destruct H2;subst;auto. destruct H2;subst;auto. auto. Qed. Theorem expr_array_member_rv : forall s e1 t te1 te2 l vl n m v e2 P, s |= Rv e1 @ te1 == Vptr l -> s |= Aarray l (Tarray t n) vl ** P -> s |= Rv e2 @ te2 == Vint32 m -> te1 = Tarray t n \/ te1 = Tptr t -> te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 -> (Z.of_nat n < 4294967295)%Z -> (Int.unsigned m < Z.of_nat n)%Z -> (Int.unsigned m < Z.of_nat (length vl))%Z -> rule_type_val_match t v = true -> nth_val' (Z.to_nat (Int.unsigned m)) vl = v -> s |= Rv (earrayelem e1 e2) @ t == v. Proof. intros. subst v. eapply expr_array_member_rv'; eauto. unfold Int.ltu. rewrite Int.unsigned_zero. apply zlt_false. lets Hx:Int.unsigned_range m. omega. unfold Int.ltu. apply zlt_true. rewrite Int.unsigned_repr;auto. split; try omega. unfold Int.max_unsigned. unfold Int.modulus. unfold two_power_nat, Int.wordsize. unfold shift_nat, Wordsize_32.wordsize. unfold nat_iter. omega. apply nth_val_imp_nth_val'_1; auto. Qed. (* apply array_type_vallist_match_imp_rule_type_val_match; auto. apply Nat2Z.inj_lt. rewrite Z2Nat.id. auto. lets H100 : Int.unsigned_range m. omega. Qed. *) (* tactics symbolic execution *) Ltac find_dom_lenv' Hp := match Hp with | ?A ** ?B => match find_dom_lenv' A with | (some ?a, Some ?l) => constr:(some a, Some l) | (none ?a, _) => match find_dom_lenv' B with | (some ?b, Some ?l) => constr:(some (a + b)%nat, Some l) | (none ?b, _) => constr:(none (a + b)%nat, @None) end end | A_dom_lenv ?l => constr:(some 1%nat, Some l) | _ => constr:(none 1%nat, @None) end. Ltac find_dom_lenv Hp := let x := find_dom_lenv' Hp in eval compute in x. Ltac find_ptrarray_by_block' Hp b := match Hp with | ?A ** ?B => match find_ptrarray_by_block' A b with | (some ?m) => constr:(some m) | (none ?m) => match find_ptrarray_by_block' B b with | (some ?n) => constr:(some (m + n)%nat) | (none ?n) => constr:(none (m + n)%nat) end end | Aarray (b, _) _ _ => constr:(some 1%nat) | _ => constr:(none 1%nat) end. Ltac find_ptrarray_by_block Hp b := let x := find_ptrarray_by_block' Hp b in eval compute in x. Ltac sep_get_rv := match goal with | |- _ |= Rv (ebinop ?bop ?e1 ?e2) @ _ == _ => eapply bop_rv; [ sep_get_rv | sep_get_rv | simpl; auto | auto | simpl; auto ] | |- _ |= Rv (eunop ?uop ?e) @ _ == _ => eapply uop_rv; [ sep_get_rv | simpl; auto | auto | simpl; auto ] | |- _ |= Rv (ecast _ (Tptr _)) @ _ == _ => first [ eapply cast_rv_tptr ; [ sep_get_rv | simpl;eauto;tryfalse ] | eapply cast_rv_tnull; [ sep_get_rv | simpl;eauto;tryfalse ] | eapply cast_rv_struct_tptr; [ sep_get_rv | simpl;eauto;tryfalse ] ] | |- _ |= Rv (ecast _ (Tint8)) @ _ == _ => eapply cast_rv_tint32_tint8 ; [ sep_get_rv | simpl;auto ] | |- _ |= Rv (ecast _ (Tint16)) @ _ == _ => eapply cast_rv_tint8_tint16 ; [ sep_get_rv | simpl;auto ] | |- _ |= Rv (ederef _) @ _ == _ => first [ eapply deref_rv; [ sep_get_rv | match goal with | H : ?s |= ?P |- ?s |= PV ?l @ _ |-> _ ** _ => match find_ptrmapsto P l with | (some ?n) => sep lift n in H; try exact H end end | simpl; auto ] | eapply deref_ptr_of_array_member_rv; [ sep_get_rv | match goal with | H : ?s |= ?P |- ?s |= Aarray (?b, _) _ _ ** _ => match find_ptrarray_by_block P b with | some ?n => sep lift n in H; try exact H end end | match goal with |- ?t = Tarray _ _ => try unfold t; simpl; auto end | simpl; try omega | simpl; try omega | simpl; try omega | try omega | (*unfold Z.div; simpl;*) try (simpl typelen;simpl Z.of_nat); auto | try (simpl typelen;simpl Z.of_nat);try omega | simpl;try omega | try omega | auto | simpl; auto ] ] | H: ?s |= ?P |- ?s |= Rv (evar ?x) @ _ == _ => match find_lvarmapsto P x with | some ?m => eapply lvar_rv; [ sep lift m in H; exact H (*| auto*) | simpl; auto ] | none _ => match find_dom_lenv P with | (none _, _) => fail 1 | (some ?m, Some ?l) => let ret1 := constr:(var_notin_dom x l) in let ret2 := (eval compute in ret1) in match ret2 with | true => match find_gvarmapsto P x with | none _ => fail 2 | some ?n => eapply gvar_rv; [ sep lifts (m::n::nil)%list in H; exact H | simpl; auto (*| auto*) | simpl; auto ] end | false => fail 3 end end end | H: ?s |= ?P |- ?s |= Rv (efield (ederef (evar ?x)) _) @ _ == _ => match find_lvarmapsto P x with | some ?m => sep lift m in H; match type of H with | _ |= LV x @ Tptr _ |-> Vptr ?l ** ?P' => match find_ptrstruct P' l with | none _ => fail 1 | some ?n => sep lifts (1::(S n)::nil)%list in H; eapply struct_member_rv_general; [ exact H | (match goal with|- ?t' = Tstruct _ _ => try unfold t' end); auto | simpl; auto | simpl; auto | unfold isarray_type;intros;mytac; tryfalse;eexists;splits;auto | unfold isarray_type; let X:=fresh in intro X; try solve [ (destruct X;do 2 eexists;eauto) ]; try ( eexists;splits; [ intros;auto | unfold id_nth; simpl; auto | simpl; try omega | auto | simpl;auto] ) ] end end | none _ => match find_dom_lenv P with | (none _, _) => fail 2 | (some ?m, Some ?ls) => let ret1 := constr:(var_notin_dom x ls) in let ret2 := (eval compute in ret1) in match ret2 with | true => match find_gvarmapsto P x with | none _ => fail 3 | some ?n => sep lifts (m::n::nil)%list in H; match type of H with | _ |= A_dom_lenv _ ** GV x @ Tptr _ |-> Vptr ?l ** ?P' => match find_ptrstruct P' l with | none _ => fail 4 | some ?o => sep lifts (1::2::(S (S o))::nil)%list in H; eapply struct_member_rv_g_general; [ exact H | simpl; auto | (match goal with|- ?t' = Tstruct _ _ => try unfold t' end); auto | simpl; auto | simpl; auto | unfold isarray_type;intros;mytac; tryfalse;eexists;splits;auto | unfold isarray_type;let X:=fresh in intro X; try solve [ destruct X;do 2 eexists;eauto]; try ( eexists;splits; [ intros;auto | unfold id_nth; simpl; auto | simpl; try omega | auto | simpl;auto ] ) ] end end end | false => fail 5 end end end | H: ?s |= ?P |- ?s |= Rv (earrayelem (evar ?x) _) @ _ == _ => match find_lvararray P x with | some ?m => sep lift m in H; eapply array_member_rv; [ exact H | auto | sep_get_rv | intuition auto | simpl; try omega | simpl; try omega | simpl; try omega | auto | simpl; auto ] | none _ => match find_dom_lenv P with | (none _, _) => fail 1 | (some ?m, Some ?ls) => let ret1 := constr:(var_notin_dom x ls) in let ret2 := (eval compute in ret1) in match ret2 with | true => match find_gvararray P x with | none _ => fail 2 | some ?n => sep lifts (m::n::nil)%list in H; eapply array_member_rv_g; [ exact H | simpl; auto | auto | sep_get_rv | intuition auto | intuition auto | simpl; try omega | simpl; try omega | simpl; try omega | auto | simpl; auto ] end | false => fail 3 end end end | |- _ |= Rv (earrayelem _ _) @ _ == _ => eapply expr_array_member_rv; [ sep_get_rv;try solve [eauto;simpl;auto] | match goal with | H : ?s |= ?P |- ?s |= Aarray ?l _ _ ** _ => match find_ptrarray P l with | (some ?n) => sep lift n in H; try exact H | _ => fail 4 end end | sep_get_rv | intuition auto | intuition auto | simpl; try omega | simpl; try omega | simpl; try omega | auto | simpl; auto ] | |- _ |= Rv (eaddrof (ederef ?e)) @ _ == _ => eapply addrof_deref_rv; sep_get_rv | |- _ |= Rv (eaddrof (earrayelem ?e1 ?e2)) @ _ == _ => eapply addrof_array_elem_rv; [ sep_get_rv | sep_get_rv | intuition auto | intuition auto ] | |- _ |= Rv enull @ _ == _ => apply null_rv | |- _ |= Rv econst32 _ @ _ == _ => apply const_rv end. Ltac sep_get_rv_in H := let H' := fresh in let Hp := type of H in assert Hp as H' by exact H; clear H; rename H' into H; sep_get_rv. Tactic Notation "sep" "get" "rv" := sep_get_rv. Tactic Notation "sep" "get" "rv" "in" hyp (H) := sep_get_rv_in H. Ltac symbolic_execution := intros; match goal with | H : ?s |= _ |- ?s |= Rv enull @ _ == _ => apply null_rv | H : ?s |= _ |- ?s |= Rv econst32 _ @ _ == _ => apply const_rv | H : ?s |= _ |- ?s |= _ => sep normal in H; sep destruct H; ssplit_apure_in H; subst; sep normal; sep eexists; sep get rv | |- ?s |= Rv _ @ _ == _ => sep normal; sep eexists; sep get rv end. Tactic Notation "symbolic" "execution" := symbolic_execution. Close Scope nat_scope.