Library hoare_assign
this file defines a tactic called 'hoare_assign' which tries to solve the
hoare triple with the assignment statements.
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 symbolic_execution.
Require Import IntLib.
Set Implicit Arguments.
Open Scope nat_scope.
assign_rules
Lemma assign_rule_general´ :
forall Spec I r ri p p´ e1 e2 l v1 v2 tp1 tp2 aop sc,
assign_type_match tp1 tp2 ->
p ==> Lv e1 @ tp1 == l ->
p <==> PV l @ tp1|-> v1 ** p´ ->
p ==> Rv e2 @ tp2 == v2 ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p }} (sassign e1 e2) {{ <|| aop ||> ** PV l @ tp1|-> v2 ** p´ }}.
Lemma addrof_rv_to_lv :
forall e t l,
Rv eaddrof e @ Tptr t == Vptr l ==> Lv e @ t == l.
Theorem assign_rule_general :
forall Spec I r ri p p´ e1 e2 l v1 v2 tp1 tp2 aop sc,
p ==> Rv (eaddrof e1) @ Tptr tp1 == Vptr l ->
p <==> PV l @ tp1|-> v1 ** p´ ->
p ==> Rv e2 @ tp2 == v2 ->
assign_type_match tp1 tp2 ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p }} (sassign e1 e2) {{ <|| aop ||> ** PV l @ tp1|-> v2 ** p´ }}.
Theorem assign_rule_lvar :
forall Spec I r ri p p´ x e v1 v2 tp1 tp2 aop sc,
p <==> LV x @ tp1|-> v1 ** p´ ->
p ==> Rv e @ tp2 == v2 ->
assign_type_match tp1 tp2 ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p}} (sassign (evar x) e) {{ <|| aop ||> ** LV x @ tp1|-> v2 ** p´ }}.
Theorem assign_rule_gvar :
forall Spec I r ri p p´ x e l v1 v2 tp1 tp2 aop sc,
p <==> A_dom_lenv l ** GV x @ tp1|-> v1 ** p´ ->
var_notin_dom x l = true ->
p ==> Rv e @ tp2 == v2 ->
assign_type_match tp1 tp2 ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p }} (sassign (evar x) e) {{ <|| aop ||> ** A_dom_lenv l ** GV x @ tp1|-> v2 ** p´ }}.
Lemma assign_rule´´ :
forall Spec I r ri p p´ e1 e2 l v1 v2 tp1 tp2 aop sc,
assign_type_match tp1 tp2 ->
p ==> Lv e1 @ tp1 == l ->
p <==> PV l @ tp1|-> v1 ** p´ ->
p ==> Rv e2 @ tp2 == v2 ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign e1 e2) {{ PV l @ tp1|-> v2 ** p´ //\\ <| aop |> }}.
Lemma assign_rule´´´ :
forall Spec I r ri p p´ e1 e2 l v1 v2 tp1 tp2 aop sc,
assign_type_match tp1 tp2 ->
p ==> Lv e1 @ tp1 == l ->
p <==> PV l @ tp1|-> v1 ** p´ ->
p ==> Rv e2 @ tp2 == v2 ->
{| Spec, sc, I, r, ri |} |- {{ p ** <|| aop ||> }} (sassign e1 e2) {{ PV l @ tp1|-> v2 ** p´ ** <|| aop ||> }}.
Lemma assign_rule_deref_ptr :
forall Spec I r ri aop p p´ tp1 tp2 l v1 v2 e1 e2 sc,
p ==> Rv e1 @ (Tptr tp1) == Vptr l ->
p <==> PV l @ tp1 |-> v1 ** p´ ->
p ==> Rv e2 @ tp2 == v2 ->
assign_type_match tp1 tp2 ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p }} (sassign (ederef e1) e2) {{ <|| aop ||> ** PV l @ tp1 |-> v2 ** p´ }}.
Lemma assign_rule_struct´ :
forall Spec I r ri p p´ x id e tid decl n l vl vl´ vi v tp1 tp1´ tp2 aop sc,
(forall ids dl, tp1´ <> Tstruct ids dl) ->
(forall (t´0 : type) (n0 : nat), tp1´ <> Tarray t´0 n0) ->
good_decllist decl = true ->
p <==> LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** p´ ->
tp1 = Tstruct tid decl ->
nth_val n vl = Some vi ->
nth_id n decl = Some id ->
ftype id decl = Some tp1´ ->
p ==> Rv e @ tp2 == v ->
assign_type_match tp1´ tp2 ->
vl´ = update_nth_val n vl v ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (efield (ederef (evar x)) id) e)
{{(LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl´ ** p´ //\\ <| aop |>)}}.
Lemma assign_rule_struct´´ :
forall Spec I r ri p p´ x id e tid decl n l vl vl´ vi v tp1 tp1´ tp2 aop sc,
(forall ids dl, tp1´ <> Tstruct ids dl) ->
(forall (t´0 : type) (n0 : nat), tp1´ <> Tarray t´0 n0) ->
good_decllist decl = true ->
p <==> LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** p´ ->
tp1 = Tstruct tid decl ->
nth_val n vl = Some vi ->
nth_id n decl = Some id ->
ftype id decl = Some tp1´ ->
p ==> Rv e @ tp2 == v ->
assign_type_match tp1´ tp2 ->
vl´ = update_nth_val n vl v ->
{| Spec, sc, I, r, ri |} |- {{ p ** <|| aop ||> }} (sassign (efield (ederef (evar x)) id) e)
{{(LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl´ ** p´ ** <|| aop ||>)}}.
Lemma field_array_asrt_impl:
forall p p´ b i t m id e2 x decl n n´ te2 sid off,
field_offset id decl = Some off ->
nth_id n´ decl = Some id ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z.of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
ftype id decl = Some (Tarray t n) ->
p ==>
LV x @ Tptr (Tstruct sid decl) |-> Vptr (b,i) ** p´ ->
p ==> Lv earrayelem (efield (ederef (evar x)) id) e2 @ t ==
(b,
Int.add (Int.add i off)
(Int.mul (Int.repr (BinInt.Z.of_nat (typelen t)))
(Int.repr (BinInt.Z.of_nat m)))).
Lemma field_array_asrt_impl_g:
forall p p´ b i t m id e2 x decl n´ n te2 sid off,
field_offset id decl = Some off ->
nth_id n´ decl = Some id ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z.of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
ftype id decl = Some (Tarray t n) ->
p ==>
A_notin_lenv x ** GV x @ Tptr (Tstruct sid decl) |-> Vptr (b,i) ** p´ ->
p ==> Lv earrayelem (efield (ederef (evar x)) id) e2 @ t ==
(b,
Int.add (Int.add i off)
(Int.mul (Int.repr (BinInt.Z.of_nat (typelen t)))
(Int.repr (BinInt.Z.of_nat m)))).
Lemma asrt_rep_4:forall p q r s t u v, p <==> q ** r ** s ** t -> s <==> u ** v -> p <==> u ** q ** v ** r ** t.
Lemma asrt_rep_4´:forall p q r s t u v, p <==> q ** r ** s ** t -> r <==> u ** v -> p <==> u ** v ** q ** s ** t.
Lemma asrt_rep_5:forall p f q r s t u v, p <==> f ** q ** r ** s ** t -> s <==> u ** v -> p <==> u ** f ** q ** v ** r ** t.
Lemma asrt_rep_5´:forall x p q r s t u v, p <==> x ** q ** r ** s ** t -> r <==> u ** v -> p <==> u ** v ** x ** q ** s ** t.
Lemma field_deref_asrt_impl:
forall p b i off tp1´ lv decl id tid x n p´,
(
p <==>
PV (b, Int.add i off) @ Tptr tp1´ |-> Vptr lv **
LV x @ Tptr (Tstruct tid decl) |-> Vptr (b, i) ** p´
) ->
ftype id decl = Some (Tptr tp1´) ->
nth_id n decl = Some id ->
field_offset id decl = Some off ->
( p ==> (Lv (ederef (efield (ederef (evar x)) id)) @ tp1´ == lv)).
Lemma field_deref_asrt_impl_g:
forall p b i off tp1´ lv decl id tid x n p´,
(
p <==>
PV (b, Int.add i off) @ Tptr tp1´ |-> Vptr lv **
A_notin_lenv x** GV x @ Tptr (Tstruct tid decl) |-> Vptr (b, i) ** p´
) ->
ftype id decl = Some (Tptr tp1´) ->
nth_id n decl = Some id ->
field_offset id decl = Some off ->
( p ==> (Lv (ederef (efield (ederef (evar x)) id)) @ tp1´ == lv)).
Require Import Coq.Bool.IfProp.
Lemma assign_rule_deref_struct´ :
forall Spec I r ri p p´ x id e tid decl n l vl v tp1 tp1´ tp2 aop lv vi sc,
(forall (t´0 : type) (n0 : nat), tp1´ <> Tarray t´0 n0) ->
good_decllist decl = true ->
p <==> LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** PV lv @ tp1´ |-> vi ** p´ ->
tp1 = Tstruct tid decl ->
nth_val n vl = Some (Vptr lv) ->
nth_id n decl = Some id ->
ftype id decl = Some (Tptr tp1´) ->
p ==> Rv e @ tp2 == v ->
assign_type_match tp1´ tp2 ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (ederef (efield (ederef (evar x)) id)) e)
{{(LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** PV lv @ tp1´ |-> v ** p´ //\\ <| aop |>)}}.
Lemma assign_rule_deref_struct_g´ :
forall Spec I r ri p p´ x id e tid decl n l vl v tp1 tp1´ tp2 aop lv vi sc,
(forall (t´0 : type) (n0 : nat), tp1´ <> Tarray t´0 n0) ->
good_decllist decl = true ->
p <==> A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** PV lv @ tp1´ |-> vi ** p´ ->
tp1 = Tstruct tid decl ->
nth_val n vl = Some (Vptr lv) ->
nth_id n decl = Some id ->
ftype id decl = Some (Tptr tp1´) ->
p ==> Rv e @ tp2 == v ->
assign_type_match tp1´ tp2 ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (ederef (efield (ederef (evar x)) id)) e)
{{(A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** PV lv @ tp1´ |-> v ** p´ //\\ <| aop |>)}}.
Lemma assign_rule_struct_g´ :
forall Spec I r ri p p´ x id e tid decl n l vl vl´ vi v tp1 tp1´ tp2 aop sc,
(forall ids dl, tp1´ <> Tstruct ids dl) ->
(forall (t´0 : type) (n0 : nat), tp1´ <> Tarray t´0 n0) ->
good_decllist decl = true ->
p <==> (A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr l) ** Astruct l tp1 vl ** p´ ->
tp1 = Tstruct tid decl ->
nth_val n vl = Some vi ->
nth_id n decl = Some id ->
ftype id decl = Some tp1´ ->
p ==> Rv e @ tp2 == v ->
assign_type_match tp1´ tp2 ->
vl´ = update_nth_val n vl v ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (efield (ederef (evar x)) id) e)
{{((A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr l) ** Astruct l tp1 vl´ ** p´ //\\ <| aop |>)}}.
Theorem assign_rule_array´ :
forall Spec I r ri t te2 p p´ x e e2 n m l vl vl´ v vi tp2 aop sc,
p <==> Alvarenv x (Tarray t n) (addrval_to_addr l) ** Aarray l (Tarray t n) vl ** p´ ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
nth_val m vl = Some vi ->
m<n ->
assign_type_match t tp2 ->
update_nth_val m vl v = vl´ ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (earrayelem (evar x) e2) e)
{{(Alvarenv x (Tarray t n) (addrval_to_addr l) ** Aarray l (Tarray t n) vl´ ** p´ //\\ <| aop |>)}}.
Theorem assign_rule_ptr_array´ :
forall Spec I r ri t te1 te2 p p´ e e1 e2 n m l vl vl´ v vi tp2 aop sc,
p ==> Rv e1 @ te1 == Vptr l ->
p <==> Aarray l (Tarray t n) vl ** p´ ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te1 = Tarray t n \/ te1 = Tptr t ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
nth_val m vl = Some vi ->
m<n ->
assign_type_match t tp2 ->
update_nth_val m vl v = vl´ ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (earrayelem e1 e2) e)
{{( Aarray l (Tarray t n) vl´ ** p´ //\\ <| aop |>)}}.
Theorem assign_rule_array_g´ :
forall Spec I r ri t p p´ x e e2 n m l vl vl´ v vi tp2 aop te2 sc,
p <==> (A_notin_lenv x ** Agvarenv x (Tarray t n) (addrval_to_addr l)) ** Aarray l (Tarray t n) vl ** p´ ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
nth_val m vl = Some vi ->
m<n->
assign_type_match t tp2 ->
update_nth_val m vl v = vl´ ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (earrayelem (evar x) e2) e)
{{((A_notin_lenv x ** Agvarenv x (Tarray t n) (addrval_to_addr l)) ** Aarray l (Tarray t n) vl´ ** p´ //\\ <| aop |>)}}.
Theorem assign_rule_struct_array´ :
forall Spec I r ri t p p´ decl x e e2 n´ n m off vl vl´ v vi tp2 aop id vla b i te2 tp1 sid sc,
good_decllist decl = true ->
p <==> LV x @ (Tptr tp1) |-> Vptr (b,i) ** Astruct (b,i) tp1 vl ** Aarray (b,Int.add i off) (Tarray t n) vla ** p´ ->
tp1 = Tstruct sid decl ->
nth_id n´ decl = Some id ->
field_offset id decl = Some off ->
ftype id decl = Some (Tarray t n) ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
nth_val m vla = Some vi ->
m<n ->
assign_type_match t tp2 ->
update_nth_val m vla v = vl´ ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (earrayelem (efield (ederef (evar x)) id) e2) e)
{{(LV x @ (Tptr tp1) |-> Vptr (b,i) ** Astruct (b,i) tp1 vl ** Aarray (b,Int.add i off) (Tarray t n) vl´ ** p´ //\\ <| aop |>)}}.
Theorem assign_rule_struct_array_g´ :
forall Spec I r ri t p p´ decl x e e2 n´ n m off vl vl´ v vi tp2 aop id vla b i te2 tp1 sid sc,
good_decllist decl = true ->
p <==> A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr (b,i) ** Astruct (b,i) tp1 vl ** Aarray (b,Int.add i off) (Tarray t n) vla ** p´ ->
tp1 = Tstruct sid decl ->
nth_id n´ decl = Some id ->
field_offset id decl = Some off ->
ftype id decl = Some (Tarray t n) ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
nth_val m vla = Some vi ->
m<n ->
assign_type_match t tp2 ->
update_nth_val m vla v = vl´ ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (earrayelem (efield (ederef (evar x)) id) e2) e)
{{(A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr (b,i) ** Astruct (b,i) tp1 vl ** Aarray (b,Int.add i off) (Tarray t n) vl´ ** p´ //\\ <| aop |>)}}.
Theorem assign_rule_struct:
forall Spec I r ri p p´ x id e tid decl n l vl vl´ v tp1 tp1´ tp2 aop sc,
(forall ids dl, tp1´ <> Tstruct ids dl) ->
(forall (t´0 : type) (n0 : nat), tp1´ <> Tarray t´0 n0) ->
good_decllist decl = true ->
p <==> LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** p´ ->
tp1 = Tstruct tid decl ->
id_nth id decl = Some n ->
ftype id decl = Some tp1´ ->
p ==> Rv e @ tp2 == v ->
assign_type_match tp1´ tp2 ->
update_nth_val_op n vl v = Some vl´->
{| Spec, sc, I, r, ri |} |-{{ p //\\ <| aop |> }} (sassign (efield (ederef (evar x)) id) e)
{{(LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl´ ** p´ //\\ <| aop |>)}}.
Theorem assign_rule_struct_aop:
forall Spec I r ri p p´ x id e tid decl n l vl vl´ v tp1 tp1´ tp2 aop sc,
p <==> LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** p´ ->
tp1 = Tstruct tid decl ->
good_decllist decl = true ->
id_nth id decl = Some n ->
ftype id decl = Some tp1´ ->
(forall ids dl, tp1´ <> Tstruct ids dl) ->
(forall (t´0 : type) (n0 : nat), tp1´ <> Tarray t´0 n0) ->
p ==> Rv e @ tp2 == v ->
assign_type_match tp1´ tp2 ->
n < length vl ->
update_nth_val n vl v = vl´ ->
{| Spec, sc, I, r, ri |} |-{{ <|| aop ||> ** p }} (sassign (efield (ederef (evar x)) id) e)
{{ <|| aop ||> ** LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl´ ** p´ }}.
Theorem assign_rule_struct_g:
forall Spec I r ri p p´ x id e tid decl n l vl vl´ v tp1 tp1´ tp2 aop sc,
(forall ids dl, tp1´ <> Tstruct ids dl) ->
(forall (t´0 : type) (n0 : nat), tp1´ <> Tarray t´0 n0) ->
good_decllist decl = true ->
p <==> (A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr l) ** Astruct l tp1 vl ** p´ ->
tp1 = Tstruct tid decl ->
id_nth id decl = Some n ->
ftype id decl = Some tp1´ ->
p ==> Rv e @ tp2 == v ->
assign_type_match tp1´ tp2 ->
update_nth_val_op n vl v = Some vl´->
{| Spec, sc, I, r, ri |} |-{{ p //\\ <| aop |> }} (sassign (efield (ederef (evar x)) id) e)
{{((A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr l) ** Astruct l tp1 vl´ ** p´ //\\ <| aop |>)}}.
Theorem assign_rule_struct_g_aop:
forall Spec I r ri p p´ ls x id e tid decl n l vl vl´ v tp1 tp1´ tp2 aop sc,
p <==> A_dom_lenv ls ** GV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** p´ ->
var_notin_dom x ls = true ->
tp1 = Tstruct tid decl ->
good_decllist decl = true ->
id_nth id decl = Some n ->
ftype id decl = Some tp1´ ->
(forall ids dl, tp1´ <> Tstruct ids dl) ->
(forall (t´0 : type) (n0 : nat), tp1´ <> Tarray t´0 n0) ->
p ==> Rv e @ tp2 == v ->
assign_type_match tp1´ tp2 ->
n < length vl ->
update_nth_val n vl v = vl´->
{| Spec, sc, I, r, ri |} |-{{ <|| aop ||> ** p }} (sassign (efield (ederef (evar x)) id) e)
{{ <|| aop ||> ** A_dom_lenv ls ** GV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl´ ** p´ }}.
Theorem assign_rule_array :
forall Spec I r ri t p p´ x e e2 n m l vl vl´ v tp2 aop te2 sc,
p <==> Alvarenv x (Tarray t n) (addrval_to_addr l) ** Aarray l (Tarray t n) vl ** p´ ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
m<n->
assign_type_match t tp2 ->
update_nth_val_op m vl v = Some vl´ ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (earrayelem (evar x) e2) e)
{{(Alvarenv x (Tarray t n) (addrval_to_addr l) ** Aarray l (Tarray t n) vl´ ** p´ //\\ <| aop |>)}}.
Theorem assign_rule_array_aop´ :
forall Spec I r ri t p p´ x e e2 n m vl vl´ v tp2 aop te2 sc,
p <==> LAarray x (Tarray t n) vl ** p´ ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
m < n ->
assign_type_match t tp2 ->
update_nth_val_op m vl v = Some vl´ ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p}}
(sassign (earrayelem (evar x) e2) e)
{{ <|| aop ||> ** LAarray x (Tarray t n) vl´ ** p´ }}.
Lemma update_nth_val_len_eq: forall vl v x, length (update_nth_val x vl v) = length vl.
Lemma len_lt_update_get_eq:forall x vl v, (Int.unsigned x < Z.of_nat (length vl))%Z -> nth_val´ (Z.to_nat (Int.unsigned x))
(update_nth_val (Z.to_nat (Int.unsigned x)) vl v) = v.
Theorem assign_rule_ptr_array :
forall Spec I r ri t p p´ e e1 e2 n m l vl vl´ v tp2 aop te1 te2 sc,
p ==> Rv e1 @ te1 == Vptr l ->
p <==> Aarray l (Tarray t n) vl ** p´ ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te1 = Tarray t n \/ te1 = Tptr t ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
m<n->
assign_type_match t tp2 ->
update_nth_val_op m vl v = Some vl´ ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (earrayelem e1 e2) e)
{{ Aarray l (Tarray t n) vl´ ** p´ //\\ <| aop |>}}.
Theorem assign_rule_ptr_array_aop :
forall Spec I r ri t te1 te2 p p´ e e1 e2 n m l vl v tp2 aop sc,
p ==> Rv e1 @ te1 == Vptr l ->
p <==> Aarray l (Tarray t n) vl ** p´ ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 m ->
te1 = Tarray t n \/ te1 = Tptr t ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
((Int.unsigned m) < Z.of_nat n)%Z ->
assign_type_match t tp2 ->
(Int.unsigned m < Z.of_nat (length vl))%Z ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p}} (sassign (earrayelem e1 e2) e)
{{( <|| aop ||> ** Aarray l (Tarray t n) (update_nth_val (Z.to_nat (Int.unsigned m)) vl v) ** p´)}}.
Theorem assign_rule_array_aop :
forall Spec I r ri t p p´ x e e2 n m vl v tp2 aop te2 sc,
p <==> LAarray x (Tarray t n) vl ** p´ ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 m ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
((Int.unsigned m) < Z.of_nat n)%Z ->
assign_type_match t tp2 ->
(Int.unsigned m < Z.of_nat (length vl))%Z ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p}}
(sassign (earrayelem (evar x) e2) e)
{{ <|| aop ||> ** LAarray x (Tarray t n) (update_nth_val (Z.to_nat (Int.unsigned m)) vl v) ** p´ }}.
Theorem assign_rule_deref_array_elem_aop´ :
forall Spec I r ri t n te p p´ x e e1 b i i0 vl v aop sc,
p <==> Aarray (b,i0) (Tarray t n) vl ** p´ ->
p ==> Rv e1 @ (Tptr t) == Vptr(b,i) ->
p ==> Rv e @ te == v ->
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 ->
assign_type_match t te ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p}}
(sassign (ederef e1) e)
{{ <|| aop ||> ** Aarray (b,i0) (Tarray t n) (update_nth_val (Z.to_nat (Int.unsigned x)) vl v) ** p´ }}.
Theorem assign_rule_deref_array_elem_aop´´ :
forall Spec I r ri t t´ n te p p´ x e e1 l l´ vl vl´ v aop sc,
p <==> Aarray l´ t´ vl ** p´ ->
t´ = Tarray t n ->
(Z.of_nat n < 4294967295)%Z ->
p ==> Rv e1 @ (Tptr t) == Vptr l ->
typelen t <> 0 ->
(Z.of_nat (typelen t) < 4294967295)%Z ->
fst l = fst l´ ->
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 ->
p ==> Rv e @ te == v ->
(Int.unsigned (snd l´) <= Int.unsigned (snd l))%Z ->
(Int.unsigned x < Z.of_nat n)%Z ->
(forall s, s |= p -> (Int.unsigned x < Z.of_nat (length vl))%Z) ->
assign_type_match t te ->
update_nth_val (Z.to_nat (Int.unsigned x)) vl v = vl´ ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p}}
(sassign (ederef e1) e)
{{ <|| aop ||> ** Aarray l´ t´ vl´ ** p´ }}.
Theorem assign_rule_deref_array_elem_aop´´´ :
forall Spec I r ri t t´ n te p p´ x e e1 l l´ vl vl´ v aop sc,
p <==> Aarray l´ t´ vl ** p´ ->
t´ = Tarray t n ->
(Z.of_nat n < 4294967295)%Z ->
p ==> Rv e1 @ (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.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 ->
p ==> Rv e @ te == v ->
(x < Z.of_nat n)%Z ->
(forall s, s |= p -> (x < Z.of_nat (length vl))%Z) ->
assign_type_match t te ->
update_nth_val (Z.to_nat x) vl v = vl´ ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p}}
(sassign (ederef e1) e)
{{ <|| aop ||> ** Aarray l´ t´ vl´ ** p´ }}.
Theorem assign_rule_deref_array_elem_aop :
forall Spec I r ri t t´ n te p p´ x e e1 b i i´ vl vl´ v aop sc,
p ==> Rv e1 @ (Tptr t) == Vptr (b,i) ->
p <==> 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 ->
p ==> Rv e @ te == v ->
(x < Z.of_nat n)%Z ->
(forall s, s |= p -> (x < Z.of_nat (length vl))%Z) ->
assign_type_match t te ->
update_nth_val (Z.to_nat x) vl v = vl´ ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p}}
(sassign (ederef e1) e)
{{ <|| aop ||> ** Aarray (b,i´) t´ vl´ ** p´ }}.
Theorem assign_rule_array_g :
forall Spec I r ri t p p´ x e e2 n m l vl vl´ v tp2 aop te2 sc,
p <==> (A_notin_lenv x ** Agvarenv x (Tarray t n) (addrval_to_addr l)) ** Aarray l (Tarray t n) vl ** p´ ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
m<n->
assign_type_match t tp2 ->
update_nth_val_op m vl v = Some vl´ ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (earrayelem (evar x) e2) e)
{{((A_notin_lenv x ** Agvarenv x (Tarray t n) (addrval_to_addr l)) ** Aarray l (Tarray t n) vl´ ** p´ //\\ <| aop |>)}}.
Theorem assign_rule_array_g_aop´ :
forall Spec I r ri t p p´ ls x e e2 n m vl vl´ v tp2 aop te2 sc,
p <==> A_dom_lenv ls ** GAarray x (Tarray t n) vl ** p´ ->
var_notin_dom x ls = true ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
m < n->
assign_type_match t tp2 ->
update_nth_val_op m vl v = Some vl´ ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p }} (sassign (earrayelem (evar x) e2) e)
{{ <|| aop ||> ** A_dom_lenv ls ** GAarray x (Tarray t n) vl´ ** p´ }}.
Theorem assign_rule_array_g_aop :
forall Spec I r ri t p p´ ls x e e2 n m vl v tp2 aop te2 sc,
p <==> A_dom_lenv ls ** GAarray x (Tarray t n) vl ** p´ ->
var_notin_dom x ls = true ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 m ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
(Int.unsigned m < Z.of_nat n)%Z ->
assign_type_match t tp2 ->
(Int.unsigned m < Z.of_nat (length vl))%Z ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p }} (sassign (earrayelem (evar x) e2) e)
{{ <|| aop ||> ** A_dom_lenv ls ** GAarray x (Tarray t n) (update_nth_val (Z.to_nat (Int.unsigned m)) vl v) ** p´ }}.
Lemma assign_rule_deref_struct:
forall Spec I r ri p p´ x id e tid decl n l vl v tp1 tp1´ tp2 aop lv vi sc,
(forall ids dl, tp1´ <> Tstruct ids dl) ->
(forall (t´0 : type) (n0 : nat), tp1´ <> Tarray t´0 n0) ->
good_decllist decl = true ->
p <==> LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** PV lv @ tp1´ |-> vi ** p´ ->
tp1 = Tstruct tid decl ->
id_nth id decl = Some n ->
ftype id decl = Some (Tptr tp1´) ->
nth_val n vl = Some (Vptr lv) ->
p ==> Rv e @ tp2 == v ->
assign_type_match tp1´ tp2 ->
{| Spec, sc, I, r, ri |} |-{{ p //\\ <| aop |> }} (sassign (ederef (efield (ederef (evar x)) id)) e)
{{(LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** PV lv @ tp1´ |-> v ** p´ //\\ <| aop |>)}}.
Lemma assign_rule_deref_struct_aop:
forall Spec I r ri p p´ x id e tid decl n l vl v tp1 tp1´ tp2 aop lv vi sc,
(forall ids dl, tp1´ <> Tstruct ids dl) ->
(forall (t´0 : type) (n0 : nat), tp1´ <> Tarray t´0 n0) ->
good_decllist decl = true ->
p <==> LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** PV lv @ tp1´ |-> vi ** p´ ->
tp1 = Tstruct tid decl ->
id_nth id decl = Some n ->
ftype id decl = Some (Tptr tp1´) ->
nth_val n vl = Some (Vptr lv) ->
p ==> Rv e @ tp2 == v ->
assign_type_match tp1´ tp2 ->
{| Spec, sc, I, r, ri |} |-{{ p ** <|| aop ||> }} (sassign (ederef (efield (ederef (evar x)) id)) e)
{{(LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** PV lv @ tp1´ |-> v ** p´ ** <|| aop ||>)}}.
Lemma assign_rule_deref_struct_g:
forall Spec I r ri p p´ x id e tid decl n l vl v tp1 tp1´ tp2 aop lv vi sc,
(forall ids dl, tp1´ <> Tstruct ids dl) ->
(forall (t´0 : type) (n0 : nat), tp1´ <> Tarray t´0 n0) ->
good_decllist decl = true ->
p <==> A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** PV lv @ tp1´ |-> vi ** p´ ->
tp1 = Tstruct tid decl ->
id_nth id decl = Some n ->
ftype id decl = Some (Tptr tp1´) ->
nth_val n vl = Some (Vptr lv) ->
p ==> Rv e @ tp2 == v ->
assign_type_match tp1´ tp2 ->
{| Spec, sc, I, r, ri |} |-{{ p //\\ <| aop |> }} (sassign (ederef (efield (ederef (evar x)) id)) e)
{{(A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** PV lv @ tp1´ |-> v ** p´ //\\ <| aop |>)}}.
Lemma assign_rule_deref_struct_g_aop:
forall Spec I r ri p p´ x id e tid decl n l vl v tp1 tp1´ tp2 aop lv vi sc,
(forall ids dl, tp1´ <> Tstruct ids dl) ->
(forall (t´0 : type) (n0 : nat), tp1´ <> Tarray t´0 n0) ->
good_decllist decl = true ->
p <==> A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** PV lv @ tp1´ |-> vi ** p´ ->
tp1 = Tstruct tid decl ->
id_nth id decl = Some n ->
ftype id decl = Some (Tptr tp1´) ->
nth_val n vl = Some (Vptr lv) ->
p ==> Rv e @ tp2 == v ->
assign_type_match tp1´ tp2 ->
{| Spec, sc, I, r, ri |} |-{{ p ** <|| aop ||> }} (sassign (ederef (efield (ederef (evar x)) id)) e)
{{(A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** PV lv @ tp1´ |-> v ** p´ ** <|| aop ||>)}}.
Theorem assign_rule_struct_array :
forall Spec I r ri t p p´ decl x e e2 n´ n m off vl vl´ v vi tp2 aop id vla b i te2 tp1 sid sc,
good_decllist decl = true ->
p <==> LV x @ (Tptr tp1) |-> Vptr (b,i) ** Astruct (b,i) tp1 vl ** Aarray (b,Int.add i off) (Tarray t n) vla ** p´ ->
tp1 = Tstruct sid decl ->
id_nth id decl = Some n´ ->
ftype id decl = Some (Tarray t n) ->
field_offset id decl = Some off ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
nth_val m vla = Some vi ->
m<n ->
assign_type_match t tp2 ->
update_nth_val m vla v = vl´ ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (earrayelem (efield (ederef (evar x)) id) e2) e)
{{(LV x @ (Tptr tp1) |-> Vptr (b,i) ** Astruct (b,i) tp1 vl ** Aarray (b,Int.add i off) (Tarray t n) vl´ ** p´ //\\ <| aop |>)}}.
Theorem assign_rule_struct_array_aop´ :
forall Spec I r ri t p p´ decl x e e2 n´ n m off vl vl´ v vi tp2 aop id vla b i te2 tp1 sid sc,
p <==> LV x @ (Tptr tp1) |-> Vptr (b,i) ** Astruct (b,i) tp1 vl ** Aarray (b,Int.add i off) (Tarray t n) vla ** p´ ->
tp1 = Tstruct sid decl ->
good_decllist decl = true ->
id_nth id decl = Some n´ ->
ftype id decl = Some (Tarray t n) ->
field_offset id decl = Some off ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
nth_val m vla = Some vi ->
m < n ->
assign_type_match t tp2 ->
update_nth_val m vla v = vl´ ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p }} (sassign (earrayelem (efield (ederef (evar x)) id) e2) e)
{{ <|| aop ||> ** LV x @ (Tptr tp1) |-> Vptr (b,i) ** Astruct (b,i) tp1 vl ** Aarray (b,Int.add i off) (Tarray t n) vl´ ** p´ }}.
Theorem assign_rule_struct_array_aop :
forall Spec I r ri t t´ t´´ p p´ p´´ decl x e e2 n´ n m off vl vl´ v vi tp2 aop id vla l te2 tp1 sid sc,
p <==> LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** p´ ->
tp1 = Tstruct sid decl ->
good_decllist decl = true ->
id_nth id decl = Some n´ ->
ftype id decl = Some t´ ->
t´ = Tarray t n ->
field_offset id decl = Some off ->
p´ <==> Aarray (fst l,Int.add (snd l) off) t´´ vla ** p´´ ->
t´´ = Tarray t n ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
m < n ->
nth_val m vla = Some vi ->
update_nth_val m vla v = vl´ ->
assign_type_match t tp2 ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p }} (sassign (earrayelem (efield (ederef (evar x)) id) e2) e)
{{ <|| aop ||> ** LV x @ (Tptr tp1) |-> Vptr l ** Astruct l tp1 vl ** Aarray (fst l,Int.add (snd l) off) t´´ vl´ ** p´´ }}.
Theorem assign_rule_struct_array_g :
forall Spec I r ri t p p´ decl x e e2 n´ n m off vl vl´ v vi tp2 aop id vla b i te2 tp1 sid sc,
good_decllist decl = true ->
p <==> A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr (b,i) ** Astruct (b,i) tp1 vl ** Aarray (b,Int.add i off) (Tarray t n) vla ** p´ ->
tp1 = Tstruct sid decl ->
id_nth id decl = Some n´ ->
ftype id decl = Some (Tarray t n) ->
field_offset id decl = Some off ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
nth_val m vla = Some vi ->
m<n ->
assign_type_match t tp2 ->
update_nth_val m vla v = vl´ ->
{| Spec, sc, I, r, ri |} |- {{ p //\\ <| aop |> }} (sassign (earrayelem (efield (ederef (evar x)) id) e2) e)
{{(A_notin_lenv x ** GV x @ (Tptr tp1) |-> Vptr (b,i) ** Astruct (b,i) tp1 vl ** Aarray (b,Int.add i off) (Tarray t n) vl´ ** p´ //\\ <| aop |>)}}.
Theorem assign_rule_struct_array_g_aop :
forall Spec I r ri t p l p´ decl x e e2 n n´ m off vl vl´ v vi tp2 aop id vla b i te2 tp1 sid sc,
p <==> A_dom_lenv l ** GV x @ (Tptr tp1) |-> Vptr (b,i) ** Astruct (b,i) tp1 vl ** Aarray (b,Int.add i off) (Tarray t n) vla ** p´ ->
var_notin_dom x l = true ->
tp1 = Tstruct sid decl ->
good_decllist decl = true ->
id_nth id decl = Some n´ ->
ftype id decl = Some (Tarray t n) ->
field_offset id decl = Some off ->
p ==> Rv e @ tp2 == v ->
p ==> Rv e2 @ te2 == Vint32 (Int.repr (BinInt.Z_of_nat m)) ->
te2 = Tint8 \/ te2 = Tint16 \/ te2 = Tint32 ->
nth_val m vla = Some vi ->
m<n ->
assign_type_match t tp2 ->
update_nth_val m vla v = vl´ ->
{| Spec, sc, I, r, ri |} |- {{ <|| aop ||> ** p }} (sassign (earrayelem (efield (ederef (evar x)) id) e2) e)
{{ <|| aop ||> ** A_dom_lenv l ** GV x @ (Tptr tp1) |-> Vptr (b,i) ** Astruct (b,i) tp1 vl ** Aarray (b,Int.add i off) (Tarray t n) vl´ ** p´ }}.
Ltac find_aop´ Hp :=
match Hp with
| ?A ** ?B =>
match find_aop´ A with
| some ?a => constr:(some a)
| none ?a =>
match find_aop´ B with
| some ?b => constr:(some (a + b)%nat)
| none ?b => constr:(none (a + b)%nat)
end
end
| Aop´ ?l => constr:(some 1%nat)
| _ => constr:(none 1%nat)
end.
Ltac find_aop Hp :=
let x := find_aop´ Hp in
eval compute in x.
Ltac hoare_assign_var :=
let s := fresh in
let H := fresh in
match goal with
| |- {| _, _, _, _, _ |} |- {{ ?P }} (sassign (evar ?x) _) {{ _ }} =>
match find_lvarmapsto P x with
| some ?m =>
match find_aop P with
| none _ => fail 1
| some ?n =>
hoare lifts (n::m::nil)%list pre;
eapply assign_rule_lvar;
[ intro s; split; intro H; exact H
| symbolic execution
| apply assign_type_match_true; simpl; auto ]
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_aop P with
| none _ => fail 1
| some ?n =>
match find_gvarmapsto P x with
| none _ => fail 3
| some ?o =>
hoare lifts (n::m::o::nil)%list pre;
eapply assign_rule_gvar;
[ intro s; split; intro H; exact H
| simpl; auto
| symbolic execution
| apply assign_type_match_true; simpl; auto ]
end
end
| false => fail
end
end
end
end.
Ltac hoare_assign_struct :=
let s := fresh in
let H := fresh in
match goal with
| |- {| _, _, _, _, _ |} |- {{ ?P }} (sassign (efield (ederef (evar ?x)) _) _) {{ _ }} =>
match find_lvarmapsto P x with
| some ?m =>
match find_aop P with
| none _ => fail 1
| some ?n =>
hoare lifts (n::m::nil)%list pre;
match goal with
| |- {| _, _, _, _, _ |} |- {{ <|| _ ||> ** LV x @ Tptr _ |-> Vptr ?l ** ?P´ }} _ {{ _ }} =>
match find_ptrstruct P´ l with
| none _ => fail 2
| some ?o =>
hoare lifts (1::2::(S (S o))::nil)%list pre;
eapply assign_rule_struct_aop;
[ intro s; split; intro H; exact H
| (match goal with |- ?tp = Tstruct _ _ => try unfold tp end); auto
| simpl; auto
| unfold id_nth; simpl; auto
| simpl; auto
| intros; auto
| intros; auto
| symbolic execution
| apply assign_type_match_true; simpl; auto
| simpl; try omega
| simpl; auto ]
end
end
end
| none _ =>
match find_dom_lenv P with
| (none _, _) => fail 3
| (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_aop P with
| none _ => fail 1
| some ?n =>
match find_gvarmapsto P x with
| none _ => fail 4
| some ?o =>
hoare lifts (n::m::o::nil)%list pre;
match goal with
| |- {| _, _, _, _, _ |} |- {{ <|| _ ||> ** A_dom_lenv _ ** GV x @ Tptr _ |-> Vptr ?l ** ?P´ }} _ {{ _ }} =>
match find_ptrstruct P´ l with
| none _ => fail 5
| some ?p =>
hoare lifts (1::2::3::(S (S (S p)))::nil)%list pre;
eapply assign_rule_struct_g_aop;
[ intro s; split; intro H; exact H
| simpl; auto
| (match goal with |- ?tp = Tstruct _ _ => try unfold tp end); auto
| simpl; auto
| unfold id_nth; simpl; auto
| simpl; auto
| intros; auto
| intros; auto
| symbolic execution
| apply assign_type_match_true; simpl; auto
| simpl; try omega
| simpl; auto ]
end
end
end
end
| false => fail 6
end
end
end
end.
Ltac hoare_assign_array :=
let s := fresh in
let H := fresh in
match goal with
| |- {| _, _, _, _, _ |} |- {{ ?P }} (sassign (earrayelem (evar ?x) _) _) {{ _ }} =>
match find_lvararray P x with
| some ?m =>
match find_aop P with
| none _ => fail 1
| some ?n =>
hoare lifts (n::m::nil)%list pre;
eapply assign_rule_array_aop;
[ intro s; split; intro H; exact H
| symbolic execution
| symbolic execution
| intuition auto
| try omega
| apply assign_type_match_true; simpl; auto
| try omega ]
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_aop P with
| none _ => fail 1
| some ?n =>
match find_gvararray P x with
| none _ => fail 3
| some ?o =>
hoare lifts (n::m::o::nil)%list pre;
eapply assign_rule_array_g_aop;
[ intro s; split; intro H; exact H
| simpl; auto
| symbolic execution
| symbolic execution
| intuition auto
| try omega
| apply assign_type_match_true; simpl; auto
| try omega ]
end
end
| false => fail
end
end
end
| |- {| _, _, _, _, _ |} |- {{ ?P }} (sassign (earrayelem _ _) _) {{ _ }} =>
eapply assign_rule_ptr_array_aop;
[ symbolic execution;try solve [eauto | simpl;eauto]
| intro s;split;intro H;
[
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
| match goal with
| H´: ?s |= Aarray ?l _ _ ** _ |- ?s |= ?P =>
match find_ptrarray P l with
| (some ?n) => sep lift n ; try exact H´
| _ => fail 4
end
end
]
| symbolic execution
| symbolic execution
| intuition auto
| intuition auto
| simpl;try omega
| simpl;auto
| simpl;try omega
]
end.
Ltac hoare_assign_deref_ptr :=
match goal with
| |- {| _, _, _, _, _ |} |- {{ ?P }} (sassign (ederef _) _) {{ _ }} =>
match find_aop P with
| none _ => fail 1
| some ?a =>
hoare lift a pre;
eapply assign_rule_deref_ptr;
[ symbolic execution
| match goal with
| |- ?P´ <==> PV ?l @ _ |-> _ ** _ =>
match find_ptrmapsto P´ l with
| none _ => fail 2
| some ?b =>
intros until s; split; intro H;
[ sep lift b; exact H
| sep lift b in H; exact H ]
end
end
| symbolic execution
| apply assign_type_match_true; simpl; auto ]
end
end.
Ltac hoare_assign_deref_array_elem :=
let s := fresh in
let H := fresh in
match goal with
| |- {| _, _, _, _, _ |} |- {{ ?P }} (sassign (ederef _) _) {{ _ }} =>
match find_aop P with
| none _ => fail 1
| some ?a =>
hoare lift a pre;
eapply assign_rule_deref_array_elem_aop;
[ symbolic execution
| match goal with
| |- ?P´ <==> Aarray (?b,_) _ _ ** _ =>
match find_ptrarray_by_block P´ b with
| none _ => fail 2
| some ?b =>
intros; split; intro H;
[ sep lift b in H; exact H |
sep lift b; exact H]
end
end
| match goal with
| |- ?t = Tarray _ _ => try unfold t; auto
end
| simpl; try omega
| simpl; auto
| simpl; try omega
| try (simpl typelen;simpl Z.of_nat);try omega
| try (simpl typelen;simpl Z.of_nat);try omega
| try (simpl typelen;simpl Z.of_nat);try omega
| symbolic execution
| simpl; try omega
| intros s H; try omega
| apply assign_type_match_true; simpl; auto
| simpl; auto ]
end
end.
Ltac hoare_assign :=
first [ hoare_assign_var
| hoare_assign_struct
| hoare_assign_array
| hoare_assign_deref_ptr
| hoare_assign_deref_array_elem ].
Close Scope nat_scope.