Library hoare_tactics
The key tactic "hoare forward" is used to generate veification conditions
for the refinement judgements, which always applies seq_rule or forward_rule
on a hoare triple and applies some primitive lemma depending on the current
statement to make a forward-step reasoning.
Users need to unfold the preconditions to make sure that they
contain all the resources required by the current statement before
using this tactic.
Usually users can use tactic 'hoare_unfold', which is defined below, to
get the resources required by the current statement.
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 hoare_assign.
Require Import hoare_lemmas.
Require Import BaseAsrtDef.
Require Import inv_prop.
Require Import InternalFunSpec.
Require Import IntLib.
Require Import List.
Require Import can_change_aop_proof.
Require Import os_code_defs.
Require Import type_val_match.
Require Import cancel_absdata.
Require Import sep_pure.
Set Implicit Arguments.
Lemma array´_length_intro: forall n vl s b i t P,
s |= Aarray´ (b,i) n t vl ** P -> length vl = n.
Lemma array_length_intro: forall s t n x vl P,
s |= Aarray x (Tarray t n) vl ** P -> length vl = n.
Lemma dllseg_head_isptr :
forall l v1 v2 v3 t n p P s, s |= dllseg v1 v2 v3 Vnull l t n p ** P -> isptr v1.
Lemma qblkfsllseg_head_isptr:
forall l v1 t n P s, s |= qblkf_sllseg
v1 Vnull l t n ** P -> isptr v1.
Lemma qblkfsll_head_isptr : forall v l t n P s, s |= qblkf_sll
v l t n ** P -> isptr v.
Lemma ecbfsllseg_head_isptr:
forall l v1 t n P s, s |= ecbf_sllseg
v1 Vnull l t n ** P -> isptr v1.
Lemma ecbfsll_head_isptr : forall v l t n P s, s |= ecbf_sll
v l t n ** P -> isptr v.
Lemma sll_head_isptr : forall v´ s v t n P, s |= sll v v´ t n ** P -> isptr v.
Lemma sllseg_head_isptr : forall vl l t n s P,
s |= sllseg l Vnull vl t n ** P -> isptr l.
Lemma evsllseg_head_isptr : forall s head l x P,
s|= evsllseg head Vnull l x ** P ->
isptr head.
Lemma pure_ex_intro_rule :
forall Spec I r ri {tp:Type} (P:tp->Prop) p s q sc,
{| Spec, sc, I, r, ri |} |- {{ EX x, [| P x |] ** p }} s {{ q }} ->
{| Spec, sc, I, r, ri |} |- {{ [| exists x, P x |] ** p }} s {{ q }}.
Lemma prop_elim_rule1 :
forall Spec I r ri (P:Prop) p s q sc,
{| Spec, sc, I, r, ri |} |- {{ [| P |] ** p }} s {{ q }} ->
(forall s0 : RstateOP, s0 |= p -> P) ->
{| Spec, sc, I, r, ri |} |- {{ p }} s {{ q }}.
Lemma prop_elim_rule2 :
forall Spec I r ri (P:Prop) p s q sc,
(forall s0 : RstateOP, s0 |= p -> P) ->
{| Spec, sc, I, r, ri |} |- {{ [| P |] ** p }} s {{ q }} ->
{| Spec, sc, I, r, ri |} |- {{ p }} s {{ q }}.
Lemma empisr_isr_is_prop:forall is, isr_is_prop empisr is.
Lemma empisr_isr_is_prop_P:
forall s P,
getisr (gettaskst s) = empisr ->
s |= P ->
s |= (([|empisr
2%nat = true|] //\\ Aisr empisr) \\//
([|empisr 2%nat = false|] //\\ Aisr empisr) ** aemp_isr_is) ** P.
Lemma atoy_inv_elim:
forall P, OSInv ** atoy_inv ** P ==> OSInv ** atoy_inv´ ** P.
Lemma atoy_inv_add:
forall P, OSInv ** atoy_inv´ ** P ==> OSInv ** atoy_inv ** P.
Lemma simpl_inv_encrit´:
forall P,
Aisr empisr ** invlth_isr I 0%nat INUM ** P ==> Aisr empisr ** OSInv ** atoy_inv ** P.
Lemma simpl_inv_encrit:
forall P,
Aisr empisr ** invlth_isr I 0%nat INUM ** P ==> Aisr empisr ** OSInv ** atoy_inv´ ** P.
Lemma simpl_inv_excrit´ :
forall P,
Aisr empisr ** OSInv ** atoy_inv ** P ==> Aisr empisr ** invlth_isr I 0%nat INUM ** P.
Lemma simpl_inv_excrit :
forall P,
Aisr empisr ** OSInv ** atoy_inv´ ** P ==> Aisr empisr ** invlth_isr I 0%nat INUM ** P.
Lemma encrit1_rule´_ISnil :
forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri : asrt) (frm : asrt) isr cs
(aop : absop) (p : asrt) sc,
p ==> Aisr isr ** Aie true ** Ais nil ** Acs cs ** frm ->
GoodI I sc->
GoodFrm frm ->
{|Spec, sc, I, r, ri|}|- {{ <|| aop ||> ** p}}
sprim encrit
{{ <|| aop ||> **
Aisr isr ** Aie false **
Ais nil ** Acs (true::cs) ** invlth_isr I 0%nat INUM ** frm}}.
Lemma excrit1_rule´_ISnil :
forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri : asrt) (isr : isr)
(cs : list bool) (frm : asrt) (aop : absop)
(p : asrt) sc,
p ==> Aisr isr ** Aie false ** Ais nil ** Acs (true::cs) ** invlth_isr I 0%nat INUM ** frm ->
GoodI I sc->
GoodFrm frm ->
{|Spec, sc, I, r, ri|}|- {{ <|| aop ||> ** p}}
sprim excrit
{{ <|| aop ||> ** Aisr isr ** Aie true ** Ais nil ** Acs cs ** frm}}.
Lemma OSInv_prop :
forall o O O´ aop,
(o, O, aop) |= OSInv -> OSAbstMod.disj O O´ -> O´ = empabst.
Lemma disj_star_elim_disj:
forall p q r, ( p \\// q )** r ==> (p ** r) \\// (q ** r).
Lemma aemp_isr_elim:
forall o O ab P,
(o, O , ab) |= aemp_isr_is ** P -> (o, O, ab) |= P.
Lemma atoy_abst_elim :
forall o O ab P,
(o,O,ab) |= atoy_inv ** P ->
exists o´, (o´,O,ab) |= P.
Lemma osq_inv_in:
forall n e e0 m x i1 c O ab,
(forall i : hid, x i = false)->
(e, e0, m, x, (false, i1, c), O, ab)
|= invlth_isr I 0%nat n ->
(e, e0, m, x, (false, i1, c), O, ab) |=
EX p1 p2 tcbl1 tcbcur tcbl2 ct tcbls rtbl,
(AOSTCBList p1 p2 tcbl1 (tcbcur :: tcbl2) rtbl ct tcbls) ** HCurTCB ct** Atrue.
Require Import absop.
Lemma join_join_disj_copy :
forall m1 m2 m3 m4 m5,
TcbMod.join m1 m2 m3 -> TcbMod.join m4 m5 m2 -> TcbMod.disj m1 m4.
Lemma TCBList_P_combine_copy :
forall {l1 l2 v1 v2 rtbl tcbls1 tcbls2 tcbls},
TcbMod.join tcbls1 tcbls2 tcbls ->
TCBList_P v1 l1 rtbl tcbls1 ->
TCBList_P v2 l2 rtbl tcbls2 ->
l1 <> nil ->
V_OSTCBNext (last l1 nil) = Some v2 ->
TCBList_P v1 (l1++l2) rtbl tcbls.
Lemma TCBList_P_split_by_tcbls :
forall l tls tid htcb s head hprev tail tnext rtbl P,
TcbMod.get tls tid = Some htcb ->
TCBList_P head l rtbl tls ->
s |= tcbdllseg head hprev tail tnext l ** P ->
(exists l1 tcbnode l2 tls1 tls2 tail1,
s |= tcbdllseg head hprev tail1 (Vptr tid) l1 **
tcbdllseg (Vptr tid) tail1 tail tnext (tcbnode :: l2) ** P /\
TCBList_P head l1 rtbl tls1 /\
TCBList_P (Vptr tid) (tcbnode :: l2) rtbl tls2 /\
TcbMod.join tls1 tls2 tls).
Lemma starinv_isr_osabst_emp :
forall n i e e0 M isr st O ab,
(i > 0)%nat ->
(forall i0, isr i0 = false) ->
(e, e0, M, isr, st, O, ab) |= starinv_isr I i n ->
O = OSAbstMod.emp.
Lemma tcbdllseg_last_nextptr :
forall l s head hprev tail tid h P,
s |= tcbdllseg head hprev tail (Vptr tid) (h::l) ** P ->
V_OSTCBNext (last (h :: l) nil) = Some (Vptr tid).
Lemma AOSTCBList_set_curtid :
forall e e0 M M´ is st O ab b tp p1 p2 l1 curtcb l2 rtbl hcurt hcurt´ tcbls,
RH_CurTCB hcurt´ tcbls ->
EnvMod.get e OSTCBCur = Some (b, Tptr tp) ->
store (Tptr tp) M (b, 0) (Vptr hcurt´) = Some M´ ->
(e, e0, M, is, st, O, ab) |= AOSTCBList p1 p2 l1 (curtcb :: l2) rtbl hcurt tcbls ->
exists p2´ l1´ curtcb´ l2´, (e, e0, M´, is, st, O, ab) |= AOSTCBList p1 p2´ l1´ (curtcb´ :: l2´) rtbl hcurt´ tcbls.
Lemma OSInv_set_curtid :
forall e e0 M M´ isr st O ab b tp tid,
EnvMod.get e OSTCBCur = Some (b, Tptr tp) ->
store (Tptr tp) M (b, 0) (Vptr tid) = Some M´ ->
(e, e0, M, isr, st, O, ab) |= AHprio GetHPrio tid ** Atrue ->
(e, e0, M, isr, st, O, ab) |= OSInv ->
(e, e0, M´, isr, st, OSAbstMod.set O curtid (oscurt tid), ab) |= OSInv.
Ltac join_get_solver :=
match goal with
| H: MemMod.join (MemMod.sig ?x ?y) _ ?O |- MemMod.get ?O ?x = Some ?y =>
eapply MemMod.join_get_get_l; eauto
| H: MemMod.join ?O1 ?O2 ?O |- MemMod.get ?O ?x = Some ?y =>
eapply MemMod.join_get_get_r; [eauto | join_get_solver]
end.
Lemma atoy_inv_osabst_emp :
forall e e0 M isr st o ab,
(e, e0, M, isr, st, o, ab) |= atoy_inv ->
o = OSAbstMod.emp.
Lemma AHprio_starinv_isr_atoy_inv_false :
forall e e0 M M1 M2 isr st O o1 o2 ab n i tid,
OSAbstMod.join o1 o2 O -> (i > 0)%nat -> (forall i : hid, isr i = false) ->
(e, e0, M, isr, st, O, ab) |= AHprio GetHPrio tid ** Atrue ->
(e, e0, M1, isr, st, o2, ab) |= starinv_isr I i n ->
(e, e0, M2, isr, st, o1, ab) |= atoy_inv ->
False.
Lemma starinv_isr_set_highest_tid :
forall n low i0 e e0 m c O ab tid b tp M´ x11,
(forall i : hid, x11 i = false) ->
EnvMod.get e OSTCBCur = Some (b, Tptr tp) ->
store (Tptr tp) m (b, 0) (Vptr tid) = Some M´ ->
(e, e0, m, x11, (false, i0, c), O, ab) |= AHprio GetHPrio tid ** Atrue ->
(e, e0, m, x11, (false, i0, c), O, ab) |= starinv_isr I low n ->
(e, e0, M´, x11, (false, i0, c), OSAbstMod.set O curtid (oscurt tid), ab) |= starinv_isr I low n.
Lemma GoodSched_GetHPrio : GoodSched GetHPrio.
Lemma GoodI_I :
GoodI I GetHPrio.
Lemma encrit1_rule´_ISnil_ISRemp :
forall (Spec : funspec) (r : retasrt)
(ri : asrt) (frm : asrt) cs
(aop : absop) (p : asrt),
p ==> Aisr empisr ** Aie true ** Ais nil ** Acs cs ** frm ->
GoodFrm frm ->
{|Spec, GetHPrio, I, r, ri|}|- {{ <|| aop ||> ** p}}
sprim encrit
{{ <|| aop ||> **
Aisr empisr ** Aie false **
Ais nil ** Acs (true::cs) ** OSInv ** atoy_inv´ ** frm}}.
Lemma excrit1_rule´_ISnil_ISRemp :
forall (Spec : funspec) (r : retasrt)
(ri : asrt)
(cs : list bool) (frm : asrt) (aop : absop)
(p : asrt),
p ==> Aisr empisr ** Aie false ** Ais nil ** Acs (true::cs) ** OSInv ** atoy_inv´ ** frm ->
GoodFrm frm ->
{|Spec , GetHPrio, I, r, ri|}|- {{ <|| aop ||> ** p}}
sprim excrit
{{ <|| aop ||> ** Aisr empisr ** Aie true ** Ais nil ** Acs cs ** frm}}.
Lemma ift_rule_general :
forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri : asrt) (p q1 q2 : asrt) (e : expr)
(tp : type) (s : stmts) sc,
p ==> EX v : val, Rv e @ tp == v ->
p //\\ Aisfalse e ==> q2 ->
{|Spec, sc, I, r, ri|}|- {{p //\\ Aistrue e}}s {{q1}} ->
{|Spec, sc, I, r, ri|}|- {{p}}sifthen e s {{q1 \\// q2}}.
Lemma ift_rule´ :
forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri : asrt) (p q : asrt) (e : expr)
(tp : type) (s : stmts) (v:val) sc,
p ==> Rv e @ tp == v ->
{|Spec, sc, I, r, ri|}|- {{ p ** [|v <> Vint32 Int.zero /\ v <> Vnull /\ v <> Vundef|] }}s {{ q }} ->
{|Spec, sc, I, r, ri|}|- {{ p }}sifthen e s {{ q \\// (p ** [|v = Vint32 Int.zero \/ v = Vnull|]) }}.
Lemma ift_rule´´ :
forall (Spec : funspec) (I : Inv) (r : retasrt)
(ri : asrt) (p q : asrt) (e : expr)
(tp : type) (s : stmts) (v:val) sc,
p ==> Rv e @ tp == v ->
{|Spec, sc, I, r, ri|}|- {{ p ** [|v <> Vint32 Int.zero /\ v <> Vnull /\ v <> Vundef|] }}s {{ q }} ->
{|Spec, sc, I, r, ri|}|- {{ p }}sifthen e s {{ (q ** [|v <> Vint32 Int.zero /\ v <> Vnull /\ v <> Vundef|])\\// (p ** [|v = Vint32 Int.zero \/ v = Vnull|]) }}.
Lemma excrit1_rule´_ISnil_ISRemp´
: forall (Spec : funspec) (r : retasrt) (ri : asrt)
(cs : list bool) (frm : asrt) (aop : absop)
(p: asrt),
p ==>
OSInv ** atoy_inv´ **
Aisr empisr **
Aie false ** Ais nil ** Acs (true :: cs) ** frm ->
GoodFrm frm ->
{|Spec, GetHPrio, I, r, ri|}|- {{ <|| aop ||> ** p}}
(sprim excrit)
{{ <|| aop ||> ** Aisr empisr ** Aie true ** Ais nil ** Acs cs ** frm }}.
Lemma calle_rule_lvar:
forall (f : fid) x
Spec
(I : Inv) (r : retasrt) (ri : asrt) (pre : fpre)
(post : fpost) (p P: asrt) (el : exprlist)
(v´ : val) (vl : vallist) (aop : absop) (tp : type)
(tl : typelist) logicl sc,
Spec f = Some (pre, post, (tp, tl)) ->
P <==> PRE [pre, vl, logicl] ** LV x @ tp |-> v´ ** p ->
GoodFrm p ->
retpost post ->
P ==> Rvl el @ tl == vl ->
tl_vl_match tl vl = true ->
{|Spec, sc, I, r, ri|}|-
{{ P}}
scalle (evar x) f el
{{EX v : val,
POST [post, vl, Some v, logicl] ** LV x @ tp |-> v ** p}}.
Lemma rvl_elim:forall s e el v vl t tl,
s |= Rv e @ t == v -> s|= Rvl el @ tl == vl ->
s |= Rvl (e::el) @ (t::tl) == (v::vl).
Lemma rvl_nil: forall s, s |= Rvl nil @ nil == nil.
Lemma hoare_disj_afalse_l_pre :
forall Spec I r ri P s Q sc,
{| Spec, sc, I, r, ri |} |- {{ P }} s {{ Q }} ->
{| Spec, sc, I, r, ri |} |- {{ Afalse \\// P }} s {{ Q }}.
Lemma hoare_disj_afalseP_r_pre :
forall Spec I r ri P s Q P´ sc,
{| Spec, sc, I, r, ri |} |- {{ P }} s {{ Q }} ->
{| Spec, sc, I, r, ri |} |- {{ P \\// Afalse ** P´ }} s {{ Q }}.
Lemma hoare_disj_afalseP_l_pre :
forall Spec I r ri P s Q P´ sc,
{| Spec, sc, I, r, ri |} |- {{ P }} s {{ Q }} ->
{| Spec, sc, I, r, ri |} |- {{ Afalse ** P´ \\// P }} s {{ Q }}.
Lemma hoare_disj_afalse_r_pre :
forall Spec I r ri P s Q sc,
{| Spec, sc, I, r, ri |} |- {{ P }} s {{ Q }} ->
{| Spec, sc, I, r, ri |} |- {{ P \\// Afalse }} s {{ Q }}.
Ltac unfold_dll :=
try unfold tcbdllseg;
try unfold dllseg;
try fold dllseg;
try unfold node.
Ltac unfold_sll :=
try unfold sll;
try unfold sllseg;
try fold sllseg;
try unfold node.
Ltac unfold_qblkfsll :=
try unfold qblkf_sll;
try unfold qblkf_sllseg;
try fold qblkf_sllseg;
try unfold node.
Ltac unfold_msgslleg :=
try unfold evsllseg;
try fold evsllseg;
try unfold AEventNode;
try unfold node.
Ltac unfold_ecbfsll :=
try unfold ecbf_sll;
try unfold ecbf_sllseg;
try fold ecbf_sllseg;
try unfold node.
Ltac unfold_gvar_array :=
try unfold AOSTCBPrioTbl in *;
try unfold AOSMapTbl in *;
try unfold AOSUnMapTbl in *;
try unfold AOSRdyTblGrp in *;
try unfold AOSRdyTbl in *;
try unfold AOSRdyGrp in *;
try unfold AOSTime in *;
try unfold AGVars in *;
try unfold AOSIntNesting in *.
Ltac destr_event :=
match goal with
| H : _ |- context [match ?d with
| DMsgQ _ _ _ _ => _
| DSem _ => _
end] => destruct d
|_ => fail
end.
Ltac unfold_msg :=
try unfold AEventNode;
try destr_event;
try unfold AMsgData;
try unfold AOSEvent;
try unfold AOSEventTbl;
try unfold AOSQCtr;
try unfold AOSQBlk;
try unfold node.
Ltac find_first_stmt´ stmts :=
match stmts with
| sseq ?s _ => find_first_stmt´ s
| _ => constr:(stmts)
end.
Ltac find_first_stmt :=
match goal with
| |- {|_ , _, _, _, _|}|- {{_}}?s {{_}} => find_first_stmt´ s
end.
Ltac find_first_exprs :=
match find_first_stmt with
| sif ?e _ _ => constr:((e::nil)%list)
| sifthen ?e _ => constr:((e::nil)%list)
| swhile ?e _ => constr:((e::nil)%list)
| sret _ ?e => constr:((e::nil)%list)
| scall _ ?el => constr: ((el)%list)
| scall ?e ?el => constr:((e::el)%list)
| sassign ?e1 ?e2 => constr:((e1::e2::nil)%list)
| _ => constr:(@nil expr)%list
end.
Ltac unfold_var x :=
match x with
| OSQFreeBlk => try unfold OSInv; try unfold AOSQFreeBlk; unfold_qblkfsll
| OSQFreeList => try unfold OSInv; try unfold AOSQFreeList; unfold_sll
| OSEventFreeList => try unfold OSInv; try unfold AOSEventFreeList; unfold_ecbfsll
| OSEventList => try unfold OSInv; try unfold AECBList; unfold_msgslleg
| OSTCBCur => try unfold OSInv; try unfold AOSTCBList;unfold_dll
| OSTCBList => try unfold OSInv; try unfold AOSTCBList
| OSRdyTbl => try unfold OSInv; try unfold AOSRdyTblGrp; try unfold AOSRdyTbl
| OSRdyGrp => try unfold OSInv; try unfold AOSRdyTblGrp; try unfold AOSRdyGrp
| OSTCBPrioTbl => try unfold OSInv; try unfold AOSTCBPrioTbl
| OSTime => try unfold OSInv; try unfold AOSTime
| 999%Z => unfold_msg
| OSIntNesting => try unfold OSInv; try unfold AOSIntNesting
| OSRunning => try unfold OSInv; try unfold AGVars
| _ => idtac
end.
Ltac unfold_exprlist ls :=
match ls with
| ((eunop _ ?e) :: ?l)%list => unfold_exprlist ((e::l)%list)
| ((ebinop _ ?e1 ?e2) :: ?l)%list => unfold_exprlist ((e1::e2::l)%list)
| ((ederef ?e) :: ?l)%list => unfold_exprlist ((e::l)%list)
| ((eaddrof ?e) :: ?l)%list => unfold_exprlist ((e::l)%list)
| ((efield ?e ?id) :: ?l)%list => unfold_exprlist ((e::(evar 999%Z) :: l)%list)
| ((ecast ?e _) :: ?l)%list => unfold_exprlist ((e::l)%list)
| ((earrayelem ?e1 ?e2) :: ?l)%list => unfold_exprlist ((e1::e2::l)%list)
| ((evar ?x) ::?l)%list => unfold_var x; unfold_exprlist l
| (enull:: ?l)%list => unfold_exprlist l
| ((econst32 _) :: ?l) => unfold_exprlist l
| (@nil expr)%list => idtac
end.
Ltac unfold_field_fun :=
try unfold V_OSQPtr in *;
try unfold V_OSEventListPtr in *;
try unfold V_OSTCBNext in *;
try unfold V_OSTCBPrev in *;
try unfold V_OSTCBEventPtr in *;
try unfold V_OSTCBMsg in *;
try unfold V_OSTCBDly in *;
try unfold V_OSTCBStat in *;
try unfold V_OSTCBPrio in *;
try unfold V_OSTCBX in *;
try unfold V_OSTCBY in *;
try unfold V_OSTCBBitX in *;
try unfold V_OSTCBBitY in *;
try unfold V_OSEventType in *;
try unfold V_OSEventGrp in *;
try unfold V_OSEventCnt in *;
try unfold V_OSEventPtr in *;
try unfold V_OSQStart in *;
try unfold V_OSQEnd in *;
try unfold V_OSQIn in *;
try unfold V_OSQOut in *;
try unfold V_OSQSize in *;
try unfold V_OSQEntries in *;
try unfold V_qfreeblk in *;
try unfold V_nextblk in *;
try unfold V_next in *;
try unfold V_qeventptr in *.
Ltac try_unfold_funspecs :=
try (unfold OS_EventSearch_spec).
Ltac sep_unfold´ :=
match goal with
| H : ?s |= ?p |- ?s |= ?q =>
match p with
| context [OSTCBCur] =>
match q with
| context [AOSTCBList] =>
try unfold AOSTCBList;
unfold_dll
| _ => fail
end
| context [OSEventFreeList] =>
match q with
| context [AOSEventFreeList] =>
try unfold AOSEventFreeList;
unfold_sll
| _ => fail
end
| context [OSQFreeList] =>
match q with
| context [AOSQFreeList] =>
try unfold AOSQFreeList;
unfold_sll
| _ => fail
end
| context [OSQFreeBlk] =>
match q with
| context [AOSQFreeBlk] =>
try unfold AOSQFreeBlk;
unfold_sll
| _ => fail
end
| _ => idtac
end
end.
Ltac sep_unfold :=
intros;
try unfold OSInv;
unfold_gvar_array;
repeat progress sep_unfold´.
Tactic Notation "sep" "semiauto" :=
first [ solve [ sep_unfold; sep_semiauto; sep_pure ]
| sep_unfold; sep_semiauto ].
Tactic Notation "sep" "auto" :=
first [ solve [ sep_unfold; sep_auto; sep_pure ]
| sep_unfold; sep_auto ].
Tactic Notation "sep" "pauto" :=
first [ solve [ sep_semiauto_nosplit; sep_pure ]
| sep_semiauto_nosplit ].
Ltac hoare_split_pure n :=
hoare lift n pre;
apply pure_split_rule´; intro.
Ltac hoare_intro_pure n :=
hoare lift n pre;
apply pure_intro_rule´; intro;
hoare lower 1%nat pre.
Ltac hoare_cut_pure x :=
apply prop_elim_rule1 with x;
[ repeat (apply pure_ex_intro_rule; first [ apply ex_intro_rule´ | apply ex_intro_rule ]; intro)
| intros; idtac ].
Ltac hoare_split_pure_all´ :=
match goal with
| |- {| _, _, _, _, _ |} |- {{ ?P }} _ {{ _ }} =>
match find_apure P with
| some ?n => hoare_split_pure n; hoare_split_pure_all´
| none _ => idtac
end
end.
Ltac hoare_ex_intro :=
repeat match goal with
| |- {| _, _, _, _, _ |} |- {{ EX _, _ }} _ {{ _ }} =>
first [ apply ex_intro_rule´ ; intros
| apply ex_intro_rule; intros ]
end.
Ltac hoare_split_pure_all :=
hoare normal pre; hoare_ex_intro; hoare_split_pure_all´.
Ltac seg_isptr :=
match goal with
| H : _ |= evsllseg ?v Vnull _ _ ** ?A |- isptr ?v =>
apply evsllseg_head_isptr in H; auto
| H : _ |= ecbf_sllseg ?v Vnull _ _ _ ** ?A |- isptr ?v =>
apply ecbfsllseg_head_isptr in H; auto
| H : _ |= qblkf_sllseg ?v Vnull _ _ _ ** ?A |- isptr ?v =>
apply qblkfsllseg_head_isptr in H; auto
| H : _ |= sllseg ?v Vnull _ _ _ ** ?A |- isptr ?v =>
apply sllseg_head_isptr in H; auto
| H : _ |= dllseg ?v _ _ Vnull _ _ _ _ ** ?A |- isptr ?v =>
apply dllseg_head_isptr in H; auto
| H : isptr ?v |- isptr ?v => exact H; clear H
| H : _ |= ?A ** ?B |- isptr _ => sep lower 1%nat in H; seg_isptr
| _ => fail 1
end.
Ltac hoare_assert_pure x :=
apply prop_elim_rule2 with x;
[ intros; idtac
| repeat (apply pure_ex_intro_rule; first [ apply ex_intro_rule´ | apply ex_intro_rule ]; intro) ].
Ltac array_leneq :=
match goal with
| H:_ |- {|_ , _, _, _, _|}|- {{?p}}_ {{_}} =>
match p with
| Aarray _ (Tarray ?t ?n) ?vl ** ?A =>
first [ let x:= fresh in
assert (length vl = n) as x by auto;
clear x
| hoare_assert_pure (length vl = n);
[ eapply array_length_intro; eauto
| hoare_split_pure_all]]
|_ => idtac
end; hoare lower 1%nat pre
end.
Ltac array_leneq_n n :=
match n with
| S ?n´ => array_leneq; array_leneq_n n´
| _ => idtac
end.
Ltac array_leneq_intro :=
match goal with
| H:_ |- {|_ , _, _, _, _|}|- {{?p}}_ {{_}} =>
let lg := asrt_to_list p in
let n:= (eval compute in (length lg)) in array_leneq_n n
end.
Ltac isptr_intro_evsllseg :=
match goal with
| H:_
|- {|_ , _, _, _, _|}|- {{?p}}_ {{_}} =>
match p with
| context [evsllseg ?v Vnull _ _] =>
first [ let x:= fresh in
assert (isptr v) as x by auto; clear x
| hoare_assert_pure (isptr v); [ seg_isptr | idtac ]]
end
| _ => idtac
end.
Ltac isptr_intro_qblkf :=
match goal with
| H:_
|- {|_ , _, _, _, _|}|- {{?p}}_ {{_}} =>
match p with
| context [qblkf_sllseg ?v Vnull _ _ _ ] =>
first [ let x:= fresh in
assert (isptr v) as x by auto; clear x
| hoare_assert_pure (isptr v); [ seg_isptr | idtac ]]
end
| _ => idtac
end.
Ltac isptr_intro_ecbf :=
match goal with
| H:_
|- {|_ , _, _, _, _|}|- {{?p}}_ {{_}} =>
match p with
| context [ecbf_sllseg ?v Vnull _ _ _ ] =>
first [ let x:= fresh in
assert (isptr v) as x by auto; clear x
| hoare_assert_pure (isptr v); [ seg_isptr | idtac ]]
end
| _ => idtac
end.
Ltac isptr_intro_sll :=
match goal with
| H:_
|- {|_ , _, _, _, _|}|- {{?p}}_ {{_}} =>
match p with
| context [sllseg ?v Vnull _ _ _] =>
first [ let x:= fresh in
assert (isptr v) as x by auto; clear x
| hoare_assert_pure (isptr v); [ seg_isptr | idtac ]]
end
| _ => idtac
end.
Ltac isptr_intro_dll :=
match goal with
| H:_
|- {|_ , _, _, _, _|}|- {{?p}}_ {{_}} =>
match p with
| context [dllseg ?v _ _ Vnull _ _ _ _] =>
first [ let x:= fresh in
assert (isptr v) as x by auto; clear x
| hoare_assert_pure (isptr v); [ seg_isptr | idtac ]]
end
| _ => idtac
end.
Ltac isptr_intro´ :=
isptr_intro_evsllseg;
isptr_intro_qblkf;
isptr_intro_ecbf;
isptr_intro_sll;
isptr_intro_dll.
Ltac isptr_intro :=
match goal with
| H:_
|- {|_ , _, _, _, _|}|- {{?p}}_ {{_}} =>
match p with
| context [evsllseg ?v Vnull _ _] =>
first [ let x:= fresh in
assert (isptr v) as x by auto; clear x
| hoare_assert_pure (isptr v); [ seg_isptr | idtac ]]
| context [qblkf_sllseg ?v Vnull _ _ _ ] =>
first [ let x:= fresh in
assert (isptr v) as x by auto; clear x
| hoare_assert_pure (isptr v); [ seg_isptr | idtac ]]
| context [ecbf_sllseg ?v Vnull _ _ _ ] =>
first [ let x:= fresh in
assert (isptr v) as x by auto; clear x
| hoare_assert_pure (isptr v); [ seg_isptr | idtac ]]
| context [sllseg ?v Vnull _ _ _] =>
first [ let x:= fresh in
assert (isptr v) as x by auto; clear x
| hoare_assert_pure (isptr v); [ seg_isptr | idtac ]]
| context [dllseg ?v _ _ Vnull _ _ _ _] =>
first [ let x:= fresh in
assert (isptr v) as x by auto; clear x
| hoare_assert_pure (isptr v); [ seg_isptr | idtac ]]
end
| _ => idtac
end.
Ltac simpl_field_eq :=
unfold_field_fun; simpl nth_val in *;
repeat match goal with
| H : Some _ = Some _ |- _ => inverts H
| H : Vptr _ = Vptr _ |- _ => inverts H
| H : Vint32 _ = Vint32 _ |- _ => inverts H
| _ => idtac
end.
Ltac pure_intro := hoare_split_pure_all;
isptr_intro;
array_leneq_intro;
hoare_split_pure_all;
mytac;
struct_type_vallist_match_elim ;
simpl_field_eq.
Ltac pure_intro2 := hoare_split_pure_all;
isptr_intro´;
array_leneq_intro;
hoare_split_pure_all;
mytac;
struct_type_vallist_match_elim ;
simpl_field_eq.
Tactic Notation "pure" "intro" := pure_intro.
Ltac unfold_funpost :=
match goal with
| H:_
|- {|_ , _, _, _, _|}|- {{?p}}_ {{_}} =>
match p with
| EX _, POST [?t, _, _ ,_] ** _=>
unfold getasrt;unfold t;
match goal with
| H:_
|- {|_ , _, _, _, _|}|- {{?p}}_ {{_}} =>
match p with
| EX _, (?t _ _ _) ** _=>
unfold t
end
end
end
end.
Ltac hoare_unfold´ :=
try unfold OSInv; try unfold_funpost;
match goal with
| H: _ |- {|_ , _, _, _, _|}|- {{_}} _ {{_}} =>
hoare_split_pure_all;
let x := find_first_exprs in
unfold_exprlist x; pure_intro2
| _ => idtac
end.
Ltac hoare_unfold :=
try unfold OSInv; try unfold_funpost;
match goal with
| H: _ |- {|_ , _, _, _, _|}|- {{_}} _ {{_}} =>
hoare_split_pure_all;
let x := find_first_exprs in
unfold_exprlist x; pure_intro
| _ => idtac
end.
Ltac elim_nil :=
match goal with
| H : (length ?v > 0)%nat |- _ => destruct v; simpl in H;
[false; inverts H | idtac]
| H : nth_val 0 ?v = Some _ |- _ => destruct v;
[simpl in H ; false; inverts H | idtac]
| _ => idtac
end.
Tactic Notation "elim" "nil" := elim_nil.
Ltac find_aisr´ Hp :=
match Hp with
| ?A ** ?B =>
match find_aisr´ A with
| some ?a => constr:(some a)
| none ?a =>
match find_aisr´ B with
| some ?b => constr:(some (a + b)%nat)
| none ?b => constr:(none (a + b)%nat)
end
end
| Aisr _ => constr:(some 1%nat)
| _ => constr:(none 1%nat)
end.
Ltac find_aisr Hp :=
let y := find_aisr´ Hp in
eval compute in y.
Ltac find_aie´ Hp :=
match Hp with
| ?A ** ?B =>
match find_aie´ A with
| some ?a => constr:(some a)
| none ?a =>
match find_aie´ B with
| some ?b => constr:(some (a + b)%nat)
| none ?b => constr:(none (a + b)%nat)
end
end
| Aie _ => constr:(some 1%nat)
| _ => constr:(none 1%nat)
end.
Ltac find_aie Hp :=
let y := find_aie´ Hp in
eval compute in y.
Ltac find_ais´ Hp :=
match Hp with
| ?A ** ?B =>
match find_ais´ A with
| some ?a => constr:(some a)
| none ?a =>
match find_ais´ B with
| some ?b => constr:(some (a + b)%nat)
| none ?b => constr:(none (a + b)%nat)
end
end
| Ais _ => constr:(some 1%nat)
| _ => constr:(none 1%nat)
end.
Ltac find_ais Hp :=
let y := find_ais´ Hp in
eval compute in y.
Ltac find_acs´ Hp :=
match Hp with
| ?A ** ?B =>
match find_acs´ A with
| some ?a => constr:(some a)
| none ?a =>
match find_acs´ B with
| some ?b => constr:(some (a + b)%nat)
| none ?b => constr:(none (a + b)%nat)
end
end
| Acs _ => constr:(some 1%nat)
| _ => constr:(none 1%nat)
end.
Ltac find_acs Hp :=
let y := find_acs´ Hp in
eval compute in y.
Ltac hoare_enter_critical :=
let s := fresh in
let H := fresh in
match goal with
| |- {|_ , _, _, _, _|}|- {{?P}} (sprim encrit) {{_}} =>
match find_aop P with
| none _ => idtac 1 "no absop in the pre condition"; fail 1
| some ?a =>
match find_aisr P with
| none _ => idtac 2 "no isr in the pre condition"; fail 2
| some ?b =>
match find_aie P with
| none _ => idtac 3 "no ie in the pre condition"; fail 3
| some ?c =>
match find_ais P with
| none _ => idtac 4 "no is in the pre condition"; fail 4
| some ?d =>
match find_acs P with
| none _ => idtac 5 "no cs in the pre condition"; fail 5
| some ?e =>
hoare lifts (a::b::c::d::e::nil) pre;
eapply encrit1_rule´_ISnil_ISRemp;
[ intros s H; exact H
| good_frm_sovler ]
end
end
end
end
end
end.
Ltac hoare_if :=
let s := fresh in
let H := fresh in
match goal with
| |- {| _ , _, _, _, _ |}|- {{ _ }} (sif _ _ _) {{ _ }} =>
eapply if_rule2´;
[ symbolic execution
| idtac
| idtac ]
| |- {| _ , _, _, _, _ |}|- {{ _ }} (sifthen _ _) {{ _ }} =>
eapply ift_rule´´;
[ symbolic execution
| idtac ]
end.
Ltac hoare_ret :=
match goal with
| |- {| _, _, _, _, _ |} |- {{ _ }} sret {{ _ }} =>
apply ret_rule´; sep semiauto
| |- {| _, _, _, _, _|} |- {{ _ }} (sprim exint) {{ _ }} =>
apply iret_rule´;sep semiauto
| |- {| ?spec, _, _, _, _|} |- {{ _ }} (srete _) {{ _ }} =>
eapply rete_rule´;
[symbolic execution
| sep semiauto
]
end.
Ltac find_OSInv´ P :=
match P with
| ?A ** ?B =>
match find_OSInv´ A with
| some ?m => constr:(some m)
| none ?m =>
match find_OSInv´ B with
| some ?n => constr:(some (m + n)%nat)
| none ?n => constr:(none (m + n)%nat)
end
end
| OSInv => constr:(some 1%nat)
| _ => constr:(none 1%nat)
end.
Ltac find_OSInv P :=
let y := find_OSInv´ P in
eval compute in y.
Ltac trycancel := try
(sep cancel Aisr;sep cancel Aie;
sep cancel Ais;
sep cancel Acs);
try sep cancel AOSEventFreeList;
try sep cancel AOSQFreeList;
try sep cancel AOSQFreeBlk;
try sep cancel AOSTCBFreeList;
try sep cancel AECBList;
try sep cancel AOSMapTbl;
try sep cancel AOSUnMapTbl;
try sep cancel AOSTCBPrioTbl;
try sep cancel AOSIntNesting;
try sep cancel AOSTCBList;
try sep cancel AOSRdyTblGrp;
try sep cancel AOSTime;
try sep cancel AGVars;
try sep cancel AOSRdyTbl;
try sep cancel AOSRdyGrp.
Ltac hoare_exit_critical :=
match goal with
| |- {|_ , _, _, _, _|}|- {{?P}} (sprim excrit) {{_}} =>
match find_aop P with
| some ?n =>
hoare lifts (n::nil) pre;
eapply excrit1_rule´_ISnil_ISRemp´;
[ intros; try unfold OSInv; sep pauto;trycancel
| simpl;auto ]
| _ => fail 1
end
end.
Ltac find_pre´ Hp :=
match Hp with
| ?A ** ?B =>
match find_pre´ A with
| some ?a => constr:(some a)
| none ?a =>
match find_pre´ B with
| some ?b => constr:(some (a + b)%nat)
| none ?b => constr:(none (a + b)%nat)
end
end
| getasrt _ => constr:(some 1%nat)
| _ => constr:(none 1%nat)
end.
Ltac find_pre Hp :=
let y := find_pre´ Hp in
eval compute in y.
Ltac hoare_abscsq :=
match goal with
| |- {| _, _, _, _, _ |} |- {{ ?P }} _ {{ _ }} =>
match find_aop P with
| none _ =>
idtac 1 "no absop in the pre-condition"; fail 1
| some ?a =>
match find_absdata P absecblsid with
| none _ =>
idtac;
hoare lift a pre;eapply abscsq_rule´
| some ?b =>
match find_absdata P abstcblsid with
| none _ =>
idtac 3 ; fail 3
| some ?c =>
match find_absdata P ostmid with
| none _ =>
idtac 4 "no HTime in the pre-condition"; fail 4
| some ?e =>
match find_absdata P curtid with
| none _ =>
idtac 5 "no HCurTCB in the pre-condition"; fail 5
| some ?f =>
hoare lifts (a::b::c::e::f::nil) pre;
eapply abscsq_rule´
end
end
end
end
end
end.
Ltac hoare_abscsq´ :=
match goal with
| |- {| _, _, _, _, _ |} |- {{ _ }} _ {{ ?P }} =>
match find_aop P with
| none _ =>
idtac 1 "no absop in the pre-condition"; fail 1
| some ?a =>
match find_absdata P absecblsid with
| none _ =>
idtac;
hoare lift a post;eapply abscsq_rule´´
| some ?b =>
match find_absdata P abstcblsid with
| none _ =>
idtac 3; fail 3
| some ?c =>
match find_absdata P ostmid with
| none _ =>
idtac 4 "no HTime in the pre-condition"; fail 4
| some ?e =>
match find_absdata P curtid with
| none _ =>
idtac 5 "no HCurTCB in the pre-condition"; fail 5
| some ?f =>
hoare lifts (a::b::c::e::f::nil) post;
eapply abscsq_rule´
end
end
end
end
end
end.
Tactic Notation "hoare" "abscsq" := hoare_abscsq.
Tactic Notation "hoare" "abscsq" "post" := hoare_abscsq´.
Ltac unfold_spec:=
match goal with
| H :_ |- ?s |= PRE
[?t,_,_] ** _ => unfold getasrt;unfold t
| _ => idtac
end;
match goal with
| H : _ |- ?s |= (?t _ _) ** _ => unfold t
| _ => idtac
end.
Ltac hoare_calle_lvar :=
match goal with
| |- {| _, _, _, _, _ |} |- {{ ?P }} scalle (evar ?x) _ ?el {{ _ }} =>
match find_aop P with
| some ?n =>
hoare lifts (n::nil)%nat pre;
eapply calle_rule_lvar´;
[ intuition eauto |
intros; do 5 try
(apply rvl_elim;[ symbolic_execution | ]);
first [apply rvl_nil | simpl;auto] |
intros; unfold_spec;
sep pauto; trycancel;
(try simpl nth_val); auto
|idtac | idtac | simpl;eauto ]
| none _ => idtac
end
end.
Ltac hoare_call :=
match goal with
| |- {| _, _, _, _, _ |} |- {{ ?P }} scall _ ?el {{ _ }} =>
match find_aop P with
| some ?n =>
hoare lifts (n::nil)%nat pre;
eapply call_rule´;
[intuition eauto |
intros;
do 5 try (apply rvl_elim;[ symbolic_execution | ]);
first [apply rvl_nil | simpl;auto] |
intros; unfold_spec;
sep pauto; trycancel |
idtac |
simpl;eauto
]
| none _ => idtac
end
end.
Tactic Notation "hoare" "unfold" :=
hoare_unfold.
Tactic Notation "hoare" "unfold" "pre" :=
hoare_unfold´.
Ltac hoare_forward_first :=
first [ hoare_assign
| hoare_if
| hoare_enter_critical
| hoare_ret
| hoare_exit_critical
| hoare_call
| hoare_calle_lvar
| idtac ].
Ltac hoare_forward_stmts´ :=
let s := fresh in
let H := fresh in
match goal with
| |- {| _, _, _, _, _ |} |- {{ _ }} (sseq _ _) {{ _ }} =>
eapply seq_rule; [ hoare_forward_stmts´
| idtac ]
| |- {| _, _, _, _, _ |} |- {{ _ }} _ {{ _ }} =>
eapply forward_rule2; [ hoare_forward_first
| first [ intros s H; exact H
| sep pauto ] ]
end.
Ltac hoare_forward_stmts :=
match goal with
| |- {| _, _, _, _, _ |} |- {{ Afalse \\// _ }} _ {{ _ }} =>
apply hoare_disj_afalse_l_pre
| |- {| _, _, _, _, _ |} |- {{ _ \\// Afalse }} _ {{ _ }} =>
apply hoare_disj_afalse_r_pre
| |- {| _, _, _, _, _ |} |- {{ Afalse ** ?P \\// _ }} _ {{ _ }} =>
apply hoare_disj_afalseP_l_pre
| |- {| _, _, _, _, _ |} |- {{ _ \\// Afalse **?P }} _ {{ _ }} =>
apply hoare_disj_afalseP_r_pre
| |- {| _, _, _, _, _ |} |- {{ _ \\// _ }} _ {{ _ }} =>
eapply disj_rule
| _ => hoare normal pre; hoare_ex_intro; hoare_forward_stmts´
end.
Ltac hoare_forward_stmts´_nsepauto :=
let s := fresh in
let H := fresh in
match goal with
| |- {| _, _, _, _, _ |} |- {{ _ }} (sseq _ _) {{ _ }} =>
eapply seq_rule; [ hoare_forward_stmts´_nsepauto
| idtac ]
| |- {| _, _, _, _, _ |} |- {{ _ }} _ {{ _ }} =>
eapply forward_rule2; [ hoare_forward_first
| ]
end.
Ltac hoare_forward_stmts_nsepauto :=
match goal with
| |- {| _, _, _, _, _ |} |- {{ Afalse \\// _ }} _ {{ _ }} =>
apply hoare_disj_afalse_l_pre
| |- {| _, _, _, _, _ |} |- {{ _ \\// Afalse }} _ {{ _ }} =>
apply hoare_disj_afalse_r_pre
| |- {| _, _, _, _, _ |} |- {{ Afalse ** ?P \\// _ }} _ {{ _ }} =>
apply hoare_disj_afalseP_l_pre
| |- {| _, _, _, _, _ |} |- {{ _ \\// Afalse **?P }} _ {{ _ }} =>
apply hoare_disj_afalseP_r_pre
| |- {| _, _, _, _, _ |} |- {{ _ \\// _ }} _ {{ _ }} =>
eapply disj_rule
| _ => hoare normal pre; hoare_ex_intro; hoare_forward_stmts´_nsepauto
end.
Tactic Notation "hoare" "forward" := hoare_forward_stmts.