Library lab
Require Import ruleLib.
Require Import include.
Require Import memory.
Require Import memdata.
Require Import assertion.
Require Import absop.
Require Import simulation.
Require Import language.
Require Import opsem.
Require Import os_program.
Require Import os_spec.
Require Import inferules.
Require Import os_code_notations.
Require Import os_code_defs.
Require Import os_ucos_h.
Require Import os_time.
Require Import baseTac.
Require Import auxdef.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Require Import derivedrules.
Require Import hoare_conseq.
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 cancel_absdata.
Require Import hoare_tactics.
Require Import type_val_match.
Require Import init_spec.
Require Import sep_pure.
Require Import absop_rules.
Require Import mathsolver.
Open Scope code_scope.
Lemma isptr_is_definitely_ptr : forall x, isptr x -> match x with
| Vundef => false
| Vnull => true
| Vint32 _ => false
| Vptr _ => true
end = true.
Lemma os_stat_mbox_and_le255 : forall v´37, Int.unsigned ($ OS_STAT_MBOX& v´37) <= 255.
Lemma le255_and_le255 : forall x v´37,Int.unsigned x<=255 -> Int.unsigned (x& v´37) <= 255.
Lemma ptr_isptr : forall x, isptr (Vptr x).
Lemma Vnull_is_ptr : isptr Vnull.
Lemma struct_type_vallist_match_os_tcb : forall xx v´82 v´80 v´37 v´75 v´76 v´77 v´78 v´79 xxx yyy,
isptr xxx ->
isptr yyy ->
isptr v´82 ->
isptr v´80 ->
Int.unsigned v´37 <= 255 ->
Int.unsigned v´75 <= 255 ->
Int.unsigned v´76 <= 255 ->
Int.unsigned v´77 <= 255 ->
Int.unsigned v´78 <= 255 ->
Int.unsigned v´79 <= 255 ->
Int.unsigned xx <= 65535->
struct_type_vallist_match OS_TCB
(v´82
:: v´80
:: xxx
:: yyy
:: Vint32 xx
:: Vint32 v´37
:: Vint32 v´75
:: Vint32 v´76
:: Vint32 v´77
:: Vint32 v´78 :: Vint32 v´79 :: nil).
Ltac tmpltac v´37 := let adfas := fresh in
remember ( Int.unsigned v´37 <=? Byte.max_unsigned) as b eqn:eqn;
destruct b;[
auto|
lets adfas :Zle_cases (Int.unsigned v´37) (Byte.max_unsigned);
rewrite <- eqn in adfas;
unfold Byte.max_unsigned in adfas;
unfold Byte.modulus in adfas;
unfold Byte.wordsize in adfas;
simpl in adfas;
omega].
Lemma struct_type_vallist_match_os_event_mbox: forall v´51 v´52 v´49 v´50 v´55, isptr v´50 -> isptr v´51 -> Int.unsigned v´52 <= 255 -> Int.unsigned v´49 <= 65535-> struct_type_vallist_match OS_EVENT (V$OS_EVENT_TYPE_MBOX
:: Vint32 v´52 :: Vint32 v´49 :: v´50 :: v´55 :: v´51 :: nil).
Lemma struct_type_vallist_match_os_event: forall v´51 v´52 v´49 v´50 v´55 xx, isptr v´50 -> isptr v´51 ->Int.unsigned xx <=255 -> Int.unsigned v´52 <= 255 -> Int.unsigned v´49 <= 65535-> struct_type_vallist_match OS_EVENT (Vint32 xx
:: Vint32 v´52 :: Vint32 v´49 :: v´50 :: v´55 :: v´51 :: nil).
Hint Resolve le255_and_le255 : struct_type_match_side_lib.
Hint Resolve ptr_isptr : struct_type_match_side_lib.
Hint Resolve Vnull_is_ptr : struct_type_match_side_lib.
Ltac const_le_solver := match goal with
| |- Int.unsigned ($ ?e ) <= _ => try solve [clear; unfold e; int auto]
end.
Ltac struct_type_match_solver := match goal with
| |- struct_type_vallist_match OS_EVENT _ => apply struct_type_vallist_match_os_event
| |- struct_type_vallist_match OS_TCB _ => apply struct_type_vallist_match_os_tcb
end; try solve [ auto 3 with struct_type_match_side_lib | unfolds; auto 3 with struct_type_match_side_lib | const_le_solver].
Lemma absinfer_tri_choice2: forall (p : asrt) (s1 s2 : spec_code),
assertion.can_change_aop p ->
⊢ <|| s1 ?? s2 ||> ** p ⇒ <|| s2 ||> ** p.
Lemma absinfer_tri_choice1: forall (p : asrt) (s1 s2 : spec_code),
assertion.can_change_aop p ->
⊢ <|| s1 ?? s2 ||> ** p ⇒ <|| s1 ||> ** p.
Ltac infer_branchl := eapply absinfer_trans;[ eapply absinfer_tri_choice1; can_change_aop_solver| idtac].
Ltac infer_branchr := eapply absinfer_trans;[ eapply absinfer_tri_choice2; can_change_aop_solver| idtac].
Ltac infer_branch_first :=
match goal with
| [ |- context [ <|| _ ?? _ ||> ] ] => infer_branchl
| _ => idtac
end.
Ltac infer_branch n := match n with
| O => infer_branch_first
| S ?n´ => infer_branchr; infer_branch n´
end.
Ltac exgamma :=
match goal with
| [ |- context [ <|| ?aa ||> ]] => eexists aa
end.
Ltac multi_step_handler := match goal with
| [ |- ⊢ <|| _ (| _ |) ||> ** _
⇒ <|| END _ ||> ** _] => idtac
| [ |- ⊢ <|| _ ;; _ ||> ** _
⇒ <|| _ ||> ** _ ] => eapply absinfer_trans; [idtac| eapply absinfer_seq_end;[ .. | sep auto];can_change_aop_solver]; eapply absinfer_seq; [can_change_aop_solver..| idtac]
end.
Ltac tri_infer_prim:= eapply absinfer_prim; [can_change_aop_solver.. | idtac]; unfolds; intros.
Ltac tri_api_mstep:= idtac.
Ltac simpl_subst_gamma := match goal with
| [ H : ( _, _, _) |= <|| _ ||> ** _ |- _] => sep split in H
end;
match goal with
| [ H : getabsop (_, _, ?gamma) = _ |- _] => simpl in H; subst gamma
end.
Lemma tidsame_trans : forall o o1 o2, tidsame o o1 -> tidsame o1 o2 -> tidsame o o2.
Ltac eqdomtls_solver := unfolds; solve[ auto| eapply tls_get_set_indom; eauto].
Ltac eqdomO_solver1 := first [ apply eqdom_same| eapply eqdomO_trans; [idtac| eapply abst_get_set_eqdom; [absdata_solver| eqdomtls_solver]]].
Ltac eqdomO_solver := repeat eqdomO_solver1.
Ltac tidsame_solver:=solve[auto | eapply tidsame_set; auto | eapply tidsame_trans; eapply tidsame_set; auto].
Ltac tri_spec_step:=
eapply specstep_merge_emp;
constructors; [idtac| eqdomO_solver| tidsame_solver| auto..].
Ltac infer_part1 n:=
try match goal with
| [ |- context[<|| ?x _ ||>] ] => unfold x
end;
intros;
infer_branch n;
multi_step_handler;
tri_infer_prim.
Ltac tri_exists_and_solver :=match goal with
| |- exists _ , _ => eexists; tri_exists_and_solver
| |-_ /\ _ => splits; tri_exists_and_solver
| |-_ => solve [eauto| eauto; absdata_solver]
end.
Ltac tri_exists_and_solver1 :=match goal with
| |- exists _ , _ => eexists
| |-_ /\ _ => splits
| |-_ => solve [eauto| eauto; absdata_solver]
end.
Ltac tmp := eapply specstep_merge_emp;
constructors;[
unfolds;mytac;
try tri_exists_and_solver|eqdomO_solver|tidsame_solver|auto..].
Ltac infer_part2_0 :=
splits; [ tri_api_mstep;
simpl_subst_gamma;
[idtac..|tmp]|idtac].
Ltac osabst_clever_rewrite := match goal with
| [ |- context[OSAbstMod.get (OSAbstMod.set _ ?x _ ) ?x] ]=> erewrite (@OSAbstMod.set_a_get_a _ _ _ _ (@absdataidspec.eq_beq_true _ _ (@eq_refl _ curtid)))
| [ |- context[OSAbstMod.get (OSAbstMod.set _ ?x _ ) ?y] ]=> erewrite OSAbstMod.set_a_get_a´;[idtac| apply absdataidspec.neq_beq_false; clear;intro; tryfalse]
end.
Ltac simpl_absdata_sep := match goal with
| |- (?s, OSAbstMod.set ?O ?id _, _) |= ?P =>
match get_absdata_number P id with
| some ?n => sep lift n; eapply cancel_absdata_p´
| _ => idtac
end
end.
Ltac tcblistdomsubeq_solver := idtac.
Ltac infer_part2 := eexists;exgamma; first [infer_part2_0; repeat simpl_absdata_sep; sep auto | idtac].
Ltac infer_part2´:= match goal with
| [ H : ( _, ?O, _) |= <|| _ ||> ** _ |- _] =>exists O; exgamma; simpl in H
end; mytac;[
eapply hmstep_merge_emp;
constructor;
constructor; eauto;
unfolds;
try tri_exists_and_solver|
simpl;
do 6 eexists; splits; eauto;[ idtac| splits; eauto| eapply change_aop_rule; eauto| idtac..]; mytac].
Ltac infer_solver n := infer_part1 n; match goal with
| _ : (_, _, _) |= _ ** HECBList _ ** _ |- _ => infer_part2
| _ : (_, _, _) |= _ ** HTCBList _ ** _ |- _ => infer_part2
| _ : (_, _, _) |= _ ** HTime _ ** _ |- _ => infer_part2
| _ : (_, _, _) |= _ ** HCurTCB _ ** _ |- _ => infer_part2
| _ => infer_part2
end.
Lemma tcbmod_joinsig_get : forall x y mqls mqls´,
TcbMod.joinsig x y mqls mqls´ -> TcbMod.get mqls´ x = Some y.
Lemma ecbmod_joinsig_get : forall x y mqls mqls´,
EcbMod.joinsig x y mqls mqls´ -> EcbMod.get mqls´ x = Some y.
Ltac ecbget_joins_sig_solver´ :=
eauto 1; let aaa:= fresh in
match goal with
| H : EcbMod.join (EcbMod.sig ?key ?val) ?mb ?mab |- EcbMod.get ?a ?key = Some _ => lets aaa: ecbmod_joinsig_get H; clear H
| H : EcbMod.get ?ma ?key = Some _ |- EcbMod.get ?a ?key = Some _ => match goal with
| H´ : EcbMod.join ma ?mb ?mab |- _ => lets aaa: EcbMod.join_get_get_l H´ H; clear H
| H´ : EcbMod.join ?mb ma ?mab |- _ => lets aaa: EcbMod.join_get_get_r H´ H; clear H
end
end; ecbget_joins_sig_solver´.
Ltac ecbget_joins_sig_solver := unfold EcbMod.joinsig in *; ecbget_joins_sig_solver´.
Ltac tcbget_joins_sig_solver´ :=
eauto 1;
let aaa:= fresh in
match goal with
| H : TcbMod.join (TcbMod.sig ?key ?val) ?mb ?mab |- TcbMod.get ?a ?key = Some _ => lets aaa: tcbmod_joinsig_get H; clear H
| H : TcbMod.get ?ma ?key = Some _ |- TcbMod.get ?a ?key = Some _ => match goal with
| H´ : TcbMod.join ma ?mb ?mab |- _ => lets aaa: TcbMod.join_get_get_l H´ H; clear H
| H´ : TcbMod.join ?mb ma ?mab |- _ => lets aaa: TcbMod.join_get_get_r H´ H; clear H
end
end; tcbget_joins_sig_solver´.
Ltac tcbget_joins_sig_solver := unfold TcbJoin in *; unfold TcbMod.joinsig in *; tcbget_joins_sig_solver´.
Ltac joinsig_solver := match goal with
| |- EcbMod.get _ _ = Some _ => ecbget_joins_sig_solver
| |- TcbMod.get _ _ = Some _ => tcbget_joins_sig_solver
end.
Ltac go := match goal with
| |- struct_type_vallist_match _ _ => struct_type_match_solver
| |- GoodFrm _ => pauto
| |- can_change_aop _ => clear; can_change_aop_solver
| |- tidspec.beq _ _ = true =>apply CltEnvMod.beq_refl
| |- tidspec.beq _ _ = false => apply tidspec.neq_beq_false; auto
| |- EcbMod.get _ _ = Some _ => ecbget_joins_sig_solver
| |- TcbMod.get _ _ = Some _ => tcbget_joins_sig_solver
| |- _ /\ _ => split; go
| |- _ = _ => try unfolds; simpl; auto 1
| |- _ => eauto 1
end.
Close Scope code_scope.