Commit 03f23dab authored by Léon Gondelman's avatar Léon Gondelman

add optimize, infrastructure, test file

parent 8a4c5082
......@@ -10,10 +10,11 @@ theories/c_translation/proofmode.v
theories/c_translation/translation.v
theories/c_translation/derived.v
theories/vcgen/dcexpr.v
theories/vcgen/env.v
# theories/vcgen/env.v
theories/vcgen/denv.v
theories/vcgen/splitenv.v
theories/vcgen/vcgen.v
theories/vcgen/test.v
# theories/vcgen/test.v
# theories/heap_lang_vcgen/dval.v
# theories/heap_lang_vcgen/vcgen.v
......
......@@ -246,3 +246,9 @@ From iris_c.c_translation Require Import monad translation proofmode.
IntoDCexpr E e2 de2
IntoDCexpr E (a_store e1 e2) (dCStore de1 de2).
Proof. by rewrite /IntoDCexpr=> -> ->. Qed.
Global Instance into_dcexpr_binop E e1 e2 op de1 de2:
IntoDCexpr E e1 de1
IntoDCexpr E e2 de2
IntoDCexpr E (a_bin_op op e1 e2) (dCBinOp op de1 de2).
Proof. by rewrite /IntoDCexpr=> -> ->. Qed.
\ No newline at end of file
......@@ -6,7 +6,6 @@ From iris_c.c_translation Require Import monad.
From iris.algebra Require Import frac.
Section denv.
Definition known_locs := list loc.
Definition is_dloc (E: known_locs) (dv: dval) : option nat :=
......@@ -15,14 +14,24 @@ Section denv.
| _ => None
end.
Record penv_item := PenvItem {
penv_loc : loc;
penv_level : level;
penv_frac : frac;
penv_val : val
}.
Record denv_item := DenvItem {
denv_level : level;
denv_frac : frac;
denv_dval : dval
}.
Definition penv := list penv_item.
Definition denv := list (option denv_item).
Definition penv_to_known_locs : penv known_locs := fmap penv_loc.
Definition denv_item_opt_merge (dio1 dio2 : option denv_item) : option denv_item :=
match dio1, dio2 with
| None, dio | dio, None => dio
......@@ -118,5 +127,13 @@ Section denv_spec.
Definition denv_interp (L : known_locs) (m : denv) : iProp Σ :=
([ list] i dio m,
from_option (λ '(DenvItem lv q dv),
dloc_interp L (dLoc i) (lv, q) dval_interp L dv) True dio)%I.
dloc_interp L (dLoc i) (lv, q) dval_interp L dv) True dio)%I.
Definition penv_interp (m : penv) : iProp Σ :=
([ list] p m, penv_loc p (penv_level p, penv_frac p) penv_val p)%I.
Lemma denv_insert_interp E m i x q dv :
denv_interp E (denv_insert i x q dv m) denv_interp E m dloc_interp E (dLoc i) (x, q) dval_interp E dv.
Proof. Admitted.
End denv_spec.
From iris.proofmode Require Import environments coq_tactics.
Import env_notations.
From iris_c.vcgen Require Import dcexpr env denv.
From iris_c.vcgen Require Import dcexpr denv.
From iris_c.lib Require Import U locking_heap.
From iris_c.c_translation Require Import monad.
From iris.algebra Require Import frac.
......@@ -8,29 +8,18 @@ From iris.algebra Require Import frac.
Section splitenv.
Context `{amonadG Σ}.
(* TODO: use
Record env_item := DenvItem {
denv_level : level;
denv_frac : frac;
denv_dval : val
}.
Definition env := list (option env_item).
*)
Notation "l ↦( x , q ) v" :=
(mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l ↦( x , q ) v").
Definition env_to_known_locs (Γls : env_ps) : known_locs := map fst Γls.
Class MapstoListFromEnv (Γin Γout : env (iProp Σ)) (Γls : env_ps) := {
Class MapstoListFromEnv (Γin Γout : env (iProp Σ)) (Γls : penv) := {
mapsto_list_from_env :
[] Γin [] Γout env_ps_interp Γls;
[] Γin [] Γout penv_interp Γls;
mapsto_list_from_env_wf : env_wf Γin env_wf Γout;
mapsto_list_from_env_lookup_None i: Γin !! i = None Γout !! i = None
}.
Global Instance mapsto_list_from_env_nil : MapstoListFromEnv Enil Enil nil.
Proof. split; unfold env_ps_interp; eauto. Qed.
Proof. split; unfold penv_interp; eauto. Qed.
Global Instance mapsto_list_from_env_snoc_Γout Γin Γout Γls i P :
MapstoListFromEnv Γin Γout Γls
......@@ -46,7 +35,9 @@ Section splitenv.
Global Instance mapsto_list_from_env_snoc_Γls Γin Γout Γls i l q v lvl :
MapstoListFromEnv Γin Γout Γls
MapstoListFromEnv (Esnoc Γin i (l (lvl, q) v)) Γout ((l,((lvl, q),v))::Γls).
MapstoListFromEnv (Esnoc Γin i (l (lvl, q) v))
Γout
((PenvItem l lvl q v)::Γls).
Proof.
destruct 1.
split.
......@@ -58,39 +49,43 @@ Section splitenv.
by rewrite env_lookup_snoc_ne in Hsnoc.
Qed.
Class ListOfMapsto (Γls : env_ps) (E : known_locs) (ps : env_ps_dv) :=
list_of_mapsto : env_ps_interp Γls env_ps_dv_interp E ps.
Class ListOfMapsto (Γls : penv) (E : known_locs) (ps : denv) :=
list_of_mapsto : penv_interp Γls denv_interp E ps.
Global Instance list_of_mapsto_Nil E : ListOfMapsto [] E [].
Proof. unfold ListOfMapsto. simpl. eauto. Qed.
Global Instance list_of_mapsto_cons_dLitV E Γls ps lit dlit i l xq:
Global Instance list_of_mapsto_cons_dLitV E Γls ps lit dlit i l x q :
BaseLitQuote E lit dlit
LocLookup E l i
ListOfMapsto Γls E ps
ListOfMapsto ((l,(xq,LitV lit))::Γls) E ((i,(xq, dLitV dlit))::ps).
ListOfMapsto ((PenvItem l x q (LitV lit))::Γls) E
(denv_insert i x q (dLitV dlit) ps).
Proof.
rewrite /BaseLitQuote /LocLookup => Hlit Hi.
rewrite /ListOfMapsto => HΓls /=.
iDestruct 1 as "[Hl H]". cbn.
rewrite Hi Hlit. unfold env_ps_interp in *. rewrite HΓls. iFrame.
rewrite Hlit. unfold penv_interp in *. rewrite HΓls.
rewrite denv_insert_interp. iFrame. simpl. rewrite Hi. done.
Qed.
Global Instance list_of_mapsto_cons_dValUnknown E Γls ps v i l xq :
Global Instance list_of_mapsto_cons_dValUnknown E Γls ps v i l x q :
LocLookup E l i
ListOfMapsto Γls E ps
ListOfMapsto ((l,(xq,v))::Γls) E ((i,(xq,dValUnknown v))::ps) | 100.
ListOfMapsto ((PenvItem l x q v)::Γls) E
(denv_insert i x q (dValUnknown v) ps) | 100.
Proof.
rewrite /BaseLitQuote /LocLookup => Hi.
rewrite /ListOfMapsto => HΓls /=.
iDestruct 1 as "[Hl H]". cbn.
unfold env_ps_interp in *. rewrite Hi HΓls. iFrame.
unfold penv_interp in *. rewrite HΓls.
rewrite denv_insert_interp. iFrame. simpl. rewrite Hi. done.
Qed.
Lemma tac_envs_split_mapsto Γs_in Γs_out Γls Γp c ps P:
MapstoListFromEnv Γs_in Γs_out Γls
ListOfMapsto Γls (env_to_known_locs Γls) ps
envs_entails (Envs Γp Γs_out c) (env_ps_dv_interp (env_to_known_locs Γls) ps - P)%I
ListOfMapsto Γls (penv_to_known_locs Γls) ps
envs_entails (Envs Γp Γs_out c) (denv_interp (penv_to_known_locs Γls) ps - P)%I
envs_entails (Envs Γp Γs_in c) P.
Proof.
intros Hsplit. rewrite /ListOfMapsto coq_tactics.envs_entails_eq=> Hexhale.
......
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.
Ltac vcg_solver :=
eapply tac_vcg_opt_sound;
[ apply _ (* MapstoListFromEnv Γs_in Γs_out Γls *)
| compute; reflexivity (* E = penv_to_known_locs Γls *)
| apply _ (* ListOfMapsto Γls E m *)
| apply _ (* IntoDCexpr E e dce *)
| simpl ].
Section Tests_vcg.
Context `{amonadG Σ}.
Notation "l ↦( x , q ) v" :=
(mapsto l x q%Qp v%V) (at level 20, q at level 50, format "l ↦( x , q ) v").
Lemma test1 (l : loc) :
l U #1 -
awp (a_load (a_ret #l))%E True (fun v => v = #1 l U #1).
Proof.
iIntros "Hl".
vcg_solver. compute[denv_interp]. simpl. eauto with iFrame.
Qed.
Lemma test2 (l : loc) :
l U #1 -
awp (a_store (a_ret #l) (a_ret #3))%E True (fun v => v = #3 l L #3).
Proof.
iIntros "Hl".
vcg_solver. compute[denv_interp]. simpl.
eauto 1000 with iFrame.
Qed.
Lemma test3 (l : loc) :
l U #1 -
awp (a_bin_op PlusOp (a_store (a_ret #l) (a_ret #2))
(a_store (a_ret #l) (a_ret #2)))%E True (λ v, True).
Proof. iIntros "Hl". vcg_solver. Abort.
End Tests_vcg.
\ No newline at end of file
......@@ -38,11 +38,7 @@ Section vcg.
| MapstoWand : dloc dval level frac wp_expr wp_expr
| IsSome {A} : doption A (A wp_expr) wp_expr
| IsLoc : dval (dloc wp_expr) wp_expr
| UMod : wp_expr wp_expr
| Par :
((val iProp Σ) wp_expr)
((val iProp Σ) wp_expr)
(dval dval wp_expr) wp_expr.
| UMod : wp_expr wp_expr.
Arguments Base _%I.
......@@ -59,10 +55,6 @@ Section vcg.
| IsLoc dv Φ =>
dl : dloc, dval_interp E dv = #(dloc_interp E dl) wp_interp E (Φ dl)
| UMod P => U (wp_interp E P)
| Par P1 P2 P3 => (Ψ1 Ψ2 : val iProp Σ),
wp_interp E (P1 Ψ1)
wp_interp E (P2 Ψ2)
(v1 v2 : val), Ψ1 v1 - Ψ2 v2 - wp_interp E (P3 (dValUnknown v1) (dValUnknown v2))
end%I.
Fixpoint wp_interp_sane (E : known_locs) (a : wp_expr) : iProp Σ :=
......@@ -79,11 +71,7 @@ Section vcg.
| IsLoc dv Φ =>
l : loc, dval_interp E dv = #l wp_interp_sane E (Φ (dLocUnknown l))
| UMod P => U (wp_interp_sane E P)
| Par P1 P2 P3 => Ψ1 Ψ2 : val iProp Σ,
wp_interp_sane E (P1 Ψ1)
wp_interp_sane E (P2 Ψ2)
v1 v2, Ψ1 v1 - Ψ2 v2 - wp_interp_sane E (P3 (dValUnknown v1) (dValUnknown v2))
end%I.
end%I.
Fixpoint mapsto_wand_list_aux (m : denv) (Φ : wp_expr) (i : nat) : wp_expr :=
......@@ -144,12 +132,14 @@ Section vcg.
match vcg_sp E m de1 with
| Some (mIn, mOut, dv1) =>
mapsto_star_list m (vcg_wp E mIn de2 R (λ dv2,
IsLoc dv1 (λ dl, MapstoStar dl 1%Qp (λ _, mapsto_wand_list mOut (MapstoWand dl dv2 LLvl 1%Qp (Φ dv2))))))
mapsto_wand_list (denv_merge mIn mOut)
(IsLoc dv1 (λ dl, MapstoStar dl 1%Qp (λ _, (MapstoWand dl dv2 LLvl 1%Qp (Φ dv2)))))))
| None =>
match vcg_sp E m de2 with
| Some (mIn, mOut, dv2) =>
mapsto_star_list m (vcg_wp E mIn de1 R (λ dv1,
IsLoc dv1 (λ dl, MapstoStar dl 1%Qp (λ _, mapsto_wand_list mOut (MapstoWand dl dv2 LLvl 1%Qp (Φ dv2))))))
mapsto_wand_list (denv_merge mIn mOut)
(IsLoc dv1 (λ dl, MapstoStar dl 1%Qp (λ _, MapstoWand dl dv2 LLvl 1%Qp (Φ dv2))))))
| None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
end
end
......@@ -157,17 +147,72 @@ Section vcg.
match vcg_sp E m de1 with
| Some (mIn, mOut, dv1) =>
mapsto_star_list m (vcg_wp E mIn de2 R (λ dv2,
mapsto_wand_list mOut (IsSome (dbin_op_eval E op dv1 dv2) Φ)))
mapsto_wand_list (denv_merge mIn mOut) (IsSome (dbin_op_eval E op dv1 dv2) Φ)))
| None =>
match vcg_sp E m de2 with
| Some (mIn, mOut, dv2) =>
mapsto_star_list m (vcg_wp E mIn de1 R (λ dv1,
mapsto_wand_list mOut (IsSome (dbin_op_eval E op dv1 dv2) Φ)))
mapsto_wand_list (denv_merge mIn mOut) (IsSome (dbin_op_eval E op dv1 dv2) Φ)))
| None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
end
end
end.
Fixpoint optimize (m : denv) (Φ : wp_expr) : wp_expr :=
match Φ with
| Base Φ1 => mapsto_wand_list m Φ
| MapstoStar (dLoc i) q Φ1 =>
if bool_decide (q = 1%Qp)
then
match denv_delete_full i m with
| Some (m1, dv) => optimize m1 (Φ1 dv)
| None => MapstoStar (dLoc i) 1%Qp (λ dv, optimize m (Φ1 dv))
end
else
(*TODO: this is an issue related to the repr. of fractions *)
match denv_delete_frac i m with
| Some (m1, q1, dv) =>
if (bool_decide (q = q1)) then optimize m1 (Φ1 dv)
else MapstoStar (dLoc i) q (λ dv, optimize m (Φ1 dv))
| None => MapstoStar (dLoc i) q (λ dv, optimize m (Φ1 dv))
end
| MapstoStar dl q Φ1 => MapstoStar dl q (λ dv, optimize m (Φ1 dv))
| MapstoStarKnown (dLoc i) dv x q Φ1 =>
if (bool_decide (q = 1%Qp))
then
match denv_delete_full i m with
| Some (m1, dv1) =>
if (bool_decide (dv = dv1)) then optimize m1 Φ1
else MapstoStarKnown (dLoc i) dv x Qp_one (optimize m1 Φ1)
| None => MapstoStarKnown (dLoc i) dv x 1%Qp (optimize m Φ1)
end
else
match denv_delete_frac i m with
| Some (m1, q1, dv1) =>
if (bool_decide (q = q1) && bool_decide (dv = dv1))
then optimize m1 Φ1
else MapstoStarKnown (dLoc i) dv x q (optimize m Φ1)
| None => MapstoStarKnown (dLoc i) dv x q (optimize m Φ1)
end
| MapstoStarKnown dl dv x q Φ1 => MapstoStarKnown dl dv x q (optimize m Φ1)
| MapstoWand (dLoc i) dv x q Φ1 => optimize (denv_insert i x q dv m) Φ1
| MapstoWand dl w x q Φ1 => MapstoWand dl w x q (optimize m Φ1)
| IsSome dmx Φ1 =>
match dmx with
| dNone => Base False
| dSome x => optimize m (Φ1 x)
| _ => IsSome dmx (λ v, optimize m (Φ1 v))
end
| IsLoc dv Φ1 =>
match dv with
| dLitV (dLitLoc l) => optimize m (Φ1 l)
| dLitV (dLitUnknown _) | dValUnknown _ =>
IsLoc dv (λ v, optimize m (Φ1 v))
| _ => Base False
end
| UMod Φ => optimize (denv_unlock m) Φ
end.
End vcg.
Section vcg_spec.
......@@ -187,13 +232,6 @@ Section vcg_spec.
- simpl. iIntros (E) "He". iDestruct "He" as (l) "[H1 H2]".
iExists (dLocUnknown l). simpl. iFrame. by iApply H0.
- simpl. intros E. by apply U_mono.
- simpl. intros E.
iDestruct 1 as (Ψ1 Ψ2) "(HΨ1 & HΨ2 & HΦ)".
iExists _,_.
iSplitL "HΨ1". by iApply H0.
iSplitL "HΨ2". by iApply H1.
iIntros (v1 v2) "Hv1 Hv2". iApply H2.
iApply ("HΦ" with "Hv1 Hv2").
Qed.
......@@ -328,24 +366,43 @@ Section vcg_spec.
eauto with iFrame.
Qed. *)
(*Todo: adapt this to denv *)
(* Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
Lemma optimize_sound (m: denv) E (Φ: wp_expr) :
wp_interp E (optimize m Φ) -
denv_interp E m - (wp_interp E Φ).
Proof. Admitted.
Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
MapstoListFromEnv Γs_in Γs_out Γls
E = env_to_known_locs Γls →
ListOfMapsto Γls E ps
E = penv_to_known_locs Γls
ListOfMapsto Γls E m
IntoDCexpr E e dce
coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_out c)
(denv_interp E m -∗ wp_interp_sane E (vcg_wp E m dce R (λ dv, Base (Φ (dval_interp E dv))))) →
(denv_interp E m - wp_interp E (vcg_wp E m dce R (λ dv, Base (Φ (dval_interp E dv)))))
coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_in c) (awp e R Φ).
Proof.
rewrite /IntoDCexpr /=. intros Hsplit ->.
rewrite /ListOfMapsto. intros Hexhale -> Hgoal.
eapply tac_envs_split_mapsto; try eassumption.
revert Hgoal. rewrite coq_tactics.envs_entails_eq.
rewrite wp_interp_sane_sound (vcg_wp_correct R).
rewrite (vcg_wp_correct R).
intros ->. iIntros "H1 H2".
iSpecialize ("H1" with "H2"). iApply (awp_wand with "H1").
iIntros (v) "H". by iDestruct "H" as (dv) "[-> $]".
Qed. *)
Qed.
Lemma tac_vcg_opt_sound Γs_in Γs_out Γls Γp m c e R Φ E dce :
MapstoListFromEnv Γs_in Γs_out Γls
E = penv_to_known_locs Γls
ListOfMapsto Γls E m
IntoDCexpr E e dce
coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_out c)
(wp_interp_sane E (optimize m (vcg_wp E m dce R (λ dv, Base (Φ (dval_interp E dv))))))
coq_tactics.envs_entails (coq_tactics.Envs Γp Γs_in c) (awp e R Φ).
Proof.
intros ???? Hgoal. eapply tac_vcg_sound; try eassumption.
revert Hgoal. rewrite coq_tactics.envs_entails_eq. intros ->.
rewrite wp_interp_sane_sound optimize_sound. done.
Qed.
End vcg_spec.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment