Skip to content

Commit

Permalink
Convert FailureE to using print_msg. Prove FailureE case in model_E1E…
Browse files Browse the repository at this point in the history 
…2_L3_orutt_strict.
  • Loading branch information
@Chobbes
Chobbes committed Jul 3, 2023
1 parent f8803b5 commit bf31587
Show file tree
Hide file tree
Showing 7 changed files with 3,298 additions and 1,010 deletions.
4,129 changes: 3,243 additions & 886 deletions src/coq/Semantics/InfiniteToFinite.v
View file

Large diffs are not rendered by default.

89 changes: 9 additions & 80 deletions src/coq/Semantics/InfiniteToFinite/Conversions/DvalueConversions.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3124,7 +3124,7 @@ Lemma dvalue_refine_lazy_dvalue_convert_lazy :
forall uv1 uv2 s,
uvalue_refine_strict uv1 uv2 ->
DV1.uvalue_to_dvalue uv1 = inl s ->
DV2.uvalue_to_dvalue uv2 = inl s.
exists s', DV2.uvalue_to_dvalue uv2 = inl s'.
Proof.
induction uv1 using DV1.uvalue_ind';
intros uv2 dv1 CONV UV1;
Expand All @@ -3137,28 +3137,28 @@ Lemma dvalue_refine_lazy_dvalue_convert_lazy :
[ cbn in *;
inv UV1;
try (break_match_hyp; inv CONV);
cbn; split; eauto;
eexists; cbn; split; eauto;
unfold_dvalue_refine_strict; cbn; try rewrite Heqo; auto
])
| unfold_uvalue_refine_strict;
cbn in *;
break_match_hyp; inv CONV;
break_match_hyp; inv H0;
cbn;
eauto
eexists; eauto
| cbn in *;
unfold_uvalue_refine_strict;
cbn in *;
break_match_hyp; inv CONV;
break_match_hyp; inv H1;
cbn; eauto
cbn; eexists; eauto
| cbn in *;
unfold_uvalue_refine_strict;
cbn in *;
break_match_hyp; inv CONV;
break_match_hyp; inv H0;
break_match_hyp; inv H1;
cbn; eauto
cbn; eexists; eauto
].

- (* Structures *)
Expand All @@ -3182,27 +3182,18 @@ Lemma dvalue_refine_lazy_dvalue_convert_lazy :

cbn in *.
specialize (IHuv1 u dv1 Heqo0 eq_refl).
rewrite IHuv1.
destruct IHuv1.
exists x. rewrite H.
reflexivity.
+ break_match_hyp; inv H0.
break_match_hyp; inv CONV.
break_match_hyp; inv Heqo.
break_match_hyp; inv H0.
cbn.
eapply uvalue_to_dvalue_dvalue_refine_strict in Heqs0.
2: unfold_uvalue_refine_strict; eauto.
destruct Heqs0 as (?&?&?).
rewrite H.
destruct (DV2.uvalue_to_dvalue u) eqn:HU.
eexists; reflexivity.

destruct (map_monad DV2.uvalue_to_dvalue l0) eqn:Hl0.
2: {
exfalso.
eapply map_monad_err_forall2 in Hl0.
pose proof uvalue_to_dvalue_dvalue_refine_strict.
}

rewrite (map_monad_err_twin_fail' Heqs Hl0); eauto.
rewrite
eexists; reflexivity.

exfalso.
Expand All @@ -3221,68 +3212,6 @@ Lemma dvalue_refine_lazy_dvalue_convert_lazy :
rewrite Hl0 in H.
destruct H.
inv H.



admit.
admit.
admit.
admit.
{

}
admit.
admit.
admit.



admit.
admit.
admit.
- unfold_uvalue_refine_strict.
rewrite map_monad_InT_cons in CONV.
cbn in *.
repeat break_match_hyp_inv.
+ cbn.
erewrite IHuv1; eauto.
+ cbn.
clear IHuv1.
eapply uvalue_to_dvalue_dvalue_refine_strict in Heqs0.
2: unfold_uvalue_refine_strict; eauto.
destruct Heqs0 as (?&?&?).
rewrite H.
specialize (IHuv0 (DV2.UVALUE_Struct l0) dv1).
forward IHuv0.
{ unfold_uvalue_refine_strict. cbn.
rewrite Heqo; auto.
}
specialize (IHuv0 eq_refl).

break_inner_match.
2: {
exfalso.
apply map_monad_err_forall2 in Heqs0.

}

cbn.
erewrite IHuv0.

cbn.
rewrite Heqs0.
cbn.
erewrite IHuv1; eauto.

cbn.
solve_uvalue_refine_strict.
cbn.
cbn in *.
repeat break_match_hyp_inv.
break_match_hyp_inv.
repeat break_match_hyp_inv.


- (* Packed structures *)
unfold_uvalue_refine_strict.
rewrite map_monad_InT_cons in CONV.
Expand Down
10 changes: 5 additions & 5 deletions src/coq/Semantics/InfiniteToFinite/Conversions/EventConversions.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -193,7 +193,7 @@ Module Type EventConvert (LP1 : LLVMParams) (LP2 : LLVMParams) (AC : AddrConvert

(* FailureE *)
{ inversion e0.
apply (raise_error H).
apply (raise_error "").
}
Defined.

Expand Down Expand Up @@ -317,7 +317,7 @@ Module Type EventConvert (LP1 : LLVMParams) (LP2 : LLVMParams) (AC : AddrConvert

(* FailureE *)
{ inversion e0.
apply (raise_error H).
apply (raise_error "").
}
Defined.

Expand Down Expand Up @@ -413,7 +413,7 @@ Module Type EventConvert (LP1 : LLVMParams) (LP2 : LLVMParams) (AC : AddrConvert

(* FailureE *)
{ inversion e0.
apply (raise_error H).
apply (raise_error "").
}
Defined.

Expand Down Expand Up @@ -479,7 +479,7 @@ Module Type EventConvert (LP1 : LLVMParams) (LP2 : LLVMParams) (AC : AddrConvert

(* FailureE *)
{ inversion e0.
apply (raise_error H).
apply (raise_error "").
}
Defined.

Expand Down Expand Up @@ -531,7 +531,7 @@ Module Type EventConvert (LP1 : LLVMParams) (LP2 : LLVMParams) (AC : AddrConvert

(* FailureE *)
{ inversion e0.
apply (raise_error H).
apply (raise_error "").
}
Defined.

Expand Down
64 changes: 33 additions & 31 deletions src/coq/Semantics/InfiniteToFinite/LangRefine.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -668,11 +668,10 @@ Module Type LangRefine (IS1 : InterpreterStack) (IS2 : InterpreterStack) (AC1 :
rewrite H0. cbn. rewrite interp_bind.
rewrite interp_trigger. cbn. unfold LLVMEvents.raise.
do 2 rewrite bind_trigger. rewrite bind_vis.
apply eqit_Vis; intros; inv u.

apply eqit_Vis.
intros [].
Unshelve.
all : eauto.
all : inv x.
Admitted.

Lemma refine_OOM_h_L1_convert_tree_strict :
Expand Down Expand Up @@ -1366,7 +1365,8 @@ Module Type LangRefine (IS1 : InterpreterStack) (IS2 : InterpreterStack) (AC1 :
rewrite H0. cbn. rewrite interp_bind.
rewrite interp_trigger. cbn. unfold LLVMEvents.raise.
do 2 rewrite bind_trigger. rewrite bind_vis.
apply eqit_Vis; intros; inv u.
apply eqit_Vis.
intros [].

Unshelve.
all : eauto.
Expand Down Expand Up @@ -5706,9 +5706,6 @@ Module Type LangRefine (IS1 : InterpreterStack) (IS2 : InterpreterStack) (AC1 :
unfold denote_exp, IS1.LLVM.D.denote_exp.
cbn.
repeat break_match; cbn; inv Heqs0; inv Heqs; try solve_orutt_raise.
* pose proof default_dvalue_of_dtyp_dv1_dv2_same_error.
pose proof map_monad_err_twin_fail Heqs2 Heqs1 H; subst.
solve_orutt_raise.
* apply map_monad_err_fail in Heqs2.
destruct Heqs2 as [a [IN Heqs2]].
apply map_monad_err_forall2 in Heqs1.
Expand Down Expand Up @@ -5785,9 +5782,6 @@ Module Type LangRefine (IS1 : InterpreterStack) (IS2 : InterpreterStack) (AC1 :
unfold denote_exp, IS1.LLVM.D.denote_exp.
cbn.
repeat break_match; cbn; inv Heqs0; inv Heqs; try solve_orutt_raise.
* pose proof default_dvalue_of_dtyp_dv1_dv2_same_error.
pose proof map_monad_err_twin_fail Heqs2 Heqs1 H; subst.
solve_orutt_raise.
* apply map_monad_err_fail in Heqs2.
destruct Heqs2 as [a [IN Heqs2]].
apply map_monad_err_forall2 in Heqs1.
Expand Down Expand Up @@ -5864,11 +5858,6 @@ Module Type LangRefine (IS1 : InterpreterStack) (IS2 : InterpreterStack) (AC1 :
unfold denote_exp, IS1.LLVM.D.denote_exp.
cbn.
repeat break_match; cbn; inv Heqs0; inv Heqs; try solve_orutt_raise.
* pose proof default_dvalue_of_dtyp_dv1_dv2_same_error (DTYPE_I sz0) s.
cbn in H.
apply H in Heqs2.
rewrite Heqs2 in Heqs1; inv Heqs1.
solve_orutt_raise.
* apply default_dvalue_of_dtyp_i_dv1_dv2_same_error in Heqs2.
rewrite Heqs2 in Heqs1; inv Heqs1.
* apply default_dvalue_of_dtyp_i_dv1_dv2_same_error in Heqs1.
Expand Down Expand Up @@ -7360,22 +7349,6 @@ Module Type LangRefine (IS1 : InterpreterStack) (IS2 : InterpreterStack) (AC1 :
destruct H as [s' H].
break_match_hyp; inv H.

assert (s = s') as S.
{ pose proof map_monad_err_twin_fail' Heqs Heqs0.
eapply H.
intros n x y s0 H0 H1.
eapply map_monad_InT_OOM_Nth in Heqo; eauto.
destruct Heqo as (?&?&?&?).
cbn in *.
rewrite H0 in H3.
symmetry in H3; inv H3.
split; intros UVDV.
- eapply DVC.uvalue_to_dvalue_dvalue_refine_strict_error in UVDV.
2: rewrite uvalue_refine_strict_equation; eauto.
destruct UVDV as (s''&UVDV).
}
subst.

cbn.
apply rutt_raise.
constructor.
Expand Down Expand Up @@ -10015,6 +9988,35 @@ Module Type LangRefine (IS1 : InterpreterStack) (IS2 : InterpreterStack) (AC1 :
pstep; red; cbn.
rewrite subevent_subevent.
eapply EqVisOOM.
- cbn in REF;
destruct e2; try inv REF;
repeat (break_match_hyp; try inv REF).
cbn.
repeat rewrite bind_trigger.
pfold. red.
cbn.
constructor; cbn; auto.
intros [] [] _.
left.
pstep; red; cbn.
constructor.
split; auto.
red in LSR.
destruct ls1, ls2.
constructor; tauto.
intros o CONTRA.
inv CONTRA.
- cbn in REF;
destruct e2; try inv REF;
repeat (break_match_hyp; try inv REF).
cbn.
repeat rewrite bind_trigger.
pfold. red.
cbn.
constructor; cbn; auto.
intros [].
intros o CONTRA.
inv CONTRA.
Qed.

Lemma model_E1E2_12_orutt_strict :
Expand Down
12 changes: 6 additions & 6 deletions src/coq/Semantics/LLVMEvents.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,10 @@ Set Contextual Implicit.
{ raise_ub := fun A e => raiseUB e
}.

(* This function can be replaced with print_string during extraction
to print the error messages of Throw and (indirectly) ThrowUB. *)
Definition print_msg (msg : string) : unit := tt.

(* Out of memory / abort. Carries a string for a message. *)
Variant OOME : Type -> Type :=
| ThrowOOM : string -> OOME void.
Expand All @@ -117,14 +121,10 @@ Set Contextual Implicit.

(* Failure. Carries a string for a message. *)
Variant FailureE : Type -> Type :=
| Throw : string -> FailureE void.

(* This function can be replaced with print_string during extraction
to print the error messages of Throw and (indirectly) ThrowUB. *)
Definition print_msg (msg : string) : unit := tt.
| Throw : unit -> FailureE void.

Definition raise {E} {A} `{FailureE -< E} (msg : string) : itree E A :=
v <- trigger (Throw msg);; match v: void with end.
v <- trigger (Throw (print_msg msg));; match v: void with end.

#[global] Instance RAISE_ERR_ITREE_FAILUREE {E : Type -> Type} `{FailureE -< E} : RAISE_ERROR (itree E) :=
{ raise_error := fun A e => raise e
Expand Down
2 changes: 1 addition & 1 deletion src/coq/Utils/OOMRuttProps.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -566,7 +566,7 @@ Lemma orutt_raise :
{PRE : prerel E1 E2} {POST : postrel E1 E2} {R1R2 : R1 -> R2 -> Prop}
msg1 msg2,
(forall msg (o : OOM _), @subevent FailureE E2 FAIL2 void (Throw msg) <> @subevent OOM E2 OOME void o) ->
PRE void void (subevent void (Throw msg1)) (subevent void (Throw msg2)) ->
PRE void void (subevent void (Throw tt)) (subevent void (Throw tt)) ->
orutt PRE POST R1R2 (LLVMEvents.raise msg1) (LLVMEvents.raise msg2) (OOM:=OOM) (OOME:=OOME).
Proof.
intros E1 E2 OOM OOME R1 R2 FAIL1 FAIL2 PRE POST R1R2 msg1 msg2 OOM_NOT_FAIL PRETHROW.
Expand Down
2 changes: 1 addition & 1 deletion src/coq/Utils/RuttPropsExtra.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ Lemma rutt_raise :
forall {E1 E2 : Type -> Type} {R1 R2 : Type} `{FailureE -< E1} `{FailureE -< E2}
{PRE : prerel E1 E2} {POST : postrel E1 E2} {R1R2 : R1 -> R2 -> Prop}
msg1 msg2,
PRE void void (subevent void (Throw msg1)) (subevent void (Throw msg2)) ->
PRE void void (subevent void (Throw tt)) (subevent void (Throw tt)) ->
rutt PRE POST R1R2 (LLVMEvents.raise msg1) (LLVMEvents.raise msg2).
Proof.
intros E1 E2 R1 R2 FAIL1 FAIL2 PRE POST R1R2 msg1 msg2 PRETHROW.
Expand Down

0 comments on commit bf31587

Please sign in to comment.