Skip to content

Commit

Permalink
Generalize abstract interpretation over cast assum
Browse files Browse the repository at this point in the history 
It's now possible to pass in an argument at a higher level specifying
whether or not casts are assumed to truncate.

This should help with
mit-plv#833 (comment)
  • Loading branch information
@JasonGross
JasonGross committed Jul 8, 2020
1 parent 3b0b815 commit bcc5086
Show file tree
Hide file tree
Showing 6 changed files with 159 additions and 63 deletions.
26 changes: 13 additions & 13 deletions src/AbstractInterpretation/AbstractInterpretation.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -485,9 +485,8 @@ Module Compilers.
Definition strip_all_annotations strip_annotations_under {var} {t} (e : @expr var t) : @expr var t
:= @ident.strip_all_annotations var (@annotation_to_cast _) strip_annotations_under t e.

Definition eval_with_bound (skip_annotations_under : forall t, ident t -> bool) (strip_preexisting_annotations : bool) {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
:= let assume_cast_truncates := false in
let annotate_with_state := true in
Definition eval_with_bound (assume_cast_truncates : bool) (skip_annotations_under : forall t, ident t -> bool) (strip_preexisting_annotations : bool) {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
:= let annotate_with_state := true in
(@partial.ident.eval_with_bound)
var abstract_domain' annotate_expr bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state is_annotated_for (strip_annotation assume_cast_truncates strip_preexisting_annotations) skip_annotations_under annotate_with_state t e bound.

Expand All @@ -499,15 +498,14 @@ Module Compilers.
Definition StripAllAnnotations strip_annotations_under {t} (e : Expr t) : Expr t
:= fun var => strip_all_annotations strip_annotations_under (e _).

Definition EvalWithBound (skip_annotations_under : forall t, ident t -> bool) (strip_preexisting_annotations : bool) {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
:= fun var => eval_with_bound skip_annotations_under strip_preexisting_annotations (e _) bound.
Definition EvalWithBound (assume_cast_truncates : bool) (skip_annotations_under : forall t, ident t -> bool) (strip_preexisting_annotations : bool) {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
:= fun var => eval_with_bound assume_cast_truncates skip_annotations_under strip_preexisting_annotations (e _) bound.
Definition EtaExpandWithBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
:= fun var => eta_expand_with_bound (e _) bound.
End with_relax.

Definition strip_annotations {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
:= let assume_cast_truncates := false in
let strip_preexisting_annotations := true in
Definition strip_annotations (assume_cast_truncates : bool) {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
:= let strip_preexisting_annotations := true in
let annotate_with_state := false in
let skip_annotations_under := fun _ _ => false in
(@partial.ident.eval_with_bound)
Expand All @@ -516,8 +514,8 @@ Module Compilers.
(* N.B. We insert [GeneralizeVar] so that we can assume [Wf e]
and get [Wf3 (GeneralizeVar e)], rather than needing to
assume [Wf3 e] *)
Definition StripAnnotations {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
:= fun var => strip_annotations (GeneralizeVar.GeneralizeVar (e _) _) bound.
Definition StripAnnotations (assume_cast_truncates : bool) {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
:= fun var => strip_annotations assume_cast_truncates (GeneralizeVar.GeneralizeVar (e _) _) bound.

Definition eval {var} {t} (e : @expr _ t) : expr t
:= let assume_cast_truncates := false in
Expand Down Expand Up @@ -556,19 +554,21 @@ Module Compilers.

Definition PartialEvaluateWithBounds
(relax_zrange : zrange -> option zrange)
(assume_cast_truncates : bool)
(skip_annotations_under : forall t, ident t -> bool)
(strip_preexisting_annotations : bool)
{t} (e : Expr t)
(bound : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
: Expr t
:= partial.EvalWithBound relax_zrange skip_annotations_under strip_preexisting_annotations (GeneralizeVar.GeneralizeVar (e _)) bound.
:= partial.EvalWithBound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations (GeneralizeVar.GeneralizeVar (e _)) bound.
Definition PartialEvaluateWithListInfoFromBounds {t} (e : Expr t)
(bound : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
: Expr t
:= partial.EtaExpandWithListInfoFromBound (GeneralizeVar.GeneralizeVar (e _)) bound.

Definition CheckedPartialEvaluateWithBounds
(relax_zrange : zrange -> option zrange)
(assume_cast_truncates : bool)
(skip_annotations_under : forall t, ident t -> bool)
(strip_preexisting_annotations : bool)
{t} (E : Expr t)
Expand All @@ -577,12 +577,12 @@ Module Compilers.
: Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t + list { t : _ & forall var, @expr var t })
:= dlet_nd e := GeneralizeVar.ToFlat E in
let E := GeneralizeVar.FromFlat e in
let b_computed := partial.Extract false E b_in in
let b_computed := partial.Extract assume_cast_truncates E b_in in
let unsupported_casts := if strip_preexisting_annotations
then nil
else CheckCasts.GetUnsupportedCasts E in
match unsupported_casts with
| nil => (let E := PartialEvaluateWithBounds relax_zrange skip_annotations_under strip_preexisting_annotations E b_in in
| nil => (let E := PartialEvaluateWithBounds relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations E b_in in
if ZRange.type.base.option.is_tighter_than b_computed b_out
then @inl (Expr t) _ E
else inr (@inl (ZRange.type.base.option.interp (type.final_codomain t) * Expr t) _ (b_computed, E)))
Expand Down
56 changes: 34 additions & 22 deletions src/AbstractInterpretation/Proofs.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1189,6 +1189,12 @@ Module Compilers.
= partial.Extract assume_cast_truncates e b_in.
Proof using Type. apply Extract_FromFlat_ToFlat'; assumption. Qed.

Lemma Extract_GeneralizeVar {assume_cast_truncates : bool} {t} (e : Expr t) (Hwf : Wf e) b_in
(Hb : Proper (type.and_for_each_lhs_of_arrow (fun t => type.eqv)) b_in)
: partial.Extract assume_cast_truncates (GeneralizeVar.GeneralizeVar (e _)) b_in
= partial.Extract assume_cast_truncates e b_in.
Proof using Type. apply Extract_FromFlat_ToFlat; assumption. Qed.

Section with_relax.
Context {relax_zrange : zrange -> option zrange}
(Hrelax : forall r r' z, is_tighter_than_bool z r = true
Expand Down Expand Up @@ -1234,6 +1240,7 @@ Module Compilers.
Local Hint Resolve interp_annotate_expr abstract_interp_ident_related : core.

Lemma interp_eval_with_bound
{assume_cast_truncates : bool}
{skip_annotations_under : forall t, ident t -> bool}
{strip_preexisting_annotations : bool}
{t} (e_st e1 e2 : expr t)
Expand All @@ -1244,14 +1251,14 @@ Module Compilers.
: (forall arg1 arg2
(Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
(Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
type.app_curried (expr.interp (@ident.interp) (eval_with_bound relax_zrange skip_annotations_under strip_preexisting_annotations e1 st)) arg1
type.app_curried (expr.interp (@ident.interp) (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e1 st)) arg1
= type.app_curried (expr.interp (@ident.interp) e2) arg2)
/\ (forall arg1
(Harg11 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg1)
(Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
abstraction_relation'
(extract false e_st st)
(type.app_curried (expr.interp (@ident.interp) (eval_with_bound relax_zrange skip_annotations_under strip_preexisting_annotations e1 st)) arg1)).
(extract assume_cast_truncates e_st st)
(type.app_curried (expr.interp (@ident.interp) (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e1 st)) arg1)).
Proof using Hrelax.
cbv [eval_with_bound]; split;
[ intros arg1 arg2 Harg12 Harg1
Expand Down Expand Up @@ -1279,6 +1286,7 @@ Module Compilers.
Qed.

Lemma Interp_EvalWithBound
{assume_cast_truncates : bool}
{skip_annotations_under : forall t, ident t -> bool}
{strip_preexisting_annotations : bool}
{t} (e : Expr t)
Expand All @@ -1290,14 +1298,14 @@ Module Compilers.
: (forall arg1 arg2
(Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
(Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
type.app_curried (expr.Interp (@ident.interp) (EvalWithBound relax_zrange skip_annotations_under strip_preexisting_annotations e st)) arg1
type.app_curried (expr.Interp (@ident.interp) (EvalWithBound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e st)) arg1
= type.app_curried (expr.Interp (@ident.interp) e) arg2)
/\ (forall arg1
(Harg11 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg1)
(Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
abstraction_relation'
(Extract false e st)
(type.app_curried (expr.Interp (@ident.interp) (EvalWithBound relax_zrange skip_annotations_under strip_preexisting_annotations e st)) arg1)).
(Extract assume_cast_truncates e st)
(type.app_curried (expr.Interp (@ident.interp) (EvalWithBound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e st)) arg1)).
Proof using Hrelax. cbv [Extract EvalWithBound]; apply interp_eval_with_bound; auto. Qed.

Lemma Interp_EtaExpandWithBound
Expand Down Expand Up @@ -1356,6 +1364,7 @@ Module Compilers.
Qed.

Lemma interp_strip_annotations
{assume_cast_truncates : bool}
{t} (e_st e1 e2 : expr t)
(Hwf : expr.wf3 nil e_st e1 e2)
(Hwf' : expr.wf nil e2 e2)
Expand All @@ -1364,14 +1373,14 @@ Module Compilers.
: (forall arg1 arg2
(Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
(Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
type.app_curried (expr.interp (@ident.interp) (strip_annotations e1 st)) arg1
type.app_curried (expr.interp (@ident.interp) (strip_annotations assume_cast_truncates e1 st)) arg1
= type.app_curried (expr.interp (@ident.interp) e2) arg2)
/\ (forall arg1
(Harg11 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg1)
(Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
abstraction_relation'
(extract false e_st st)
(type.app_curried (expr.interp (@ident.interp) (strip_annotations e1 st)) arg1)).
(extract assume_cast_truncates e_st st)
(type.app_curried (expr.interp (@ident.interp) (strip_annotations assume_cast_truncates e1 st)) arg1)).
Proof using Type.
cbv [strip_annotations]; split;
[ intros arg1 arg2 Harg12 Harg1
Expand All @@ -1382,27 +1391,29 @@ Module Compilers.
Qed.

Lemma Interp_StripAnnotations
{assume_cast_truncates : bool}
{t} (E : Expr t)
(Hwf : Wf E)
(Ht : type.is_not_higher_order t = true)
(b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
: forall arg1 arg2
(Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
(Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
type.app_curried (expr.Interp (@ident.interp) (StripAnnotations E b_in)) arg1
type.app_curried (expr.Interp (@ident.interp) (StripAnnotations assume_cast_truncates E b_in)) arg1
= type.app_curried (expr.Interp (@ident.interp) E) arg2.
Proof using Type.
cbv [StripAnnotations].
intros *; rewrite <- (GeneralizeVar.Interp_gen1_GeneralizeVar E) by assumption.
apply (let E := GeneralizeVar.GeneralizeVar (E _) in
@interp_strip_annotations t (E _) (E _) (E _));
@interp_strip_annotations assume_cast_truncates t (E _) (E _) (E _));
try assumption;
try apply GeneralizeVar.Wf_GeneralizeVar;
try apply GeneralizeVar.Wf3_GeneralizeVar;
try apply Hwf.
Qed.

Lemma Interp_StripAnnotations_bounded
{assume_cast_truncates : bool}
{t} (E : Expr t)
(Hwf : expr.Wf E)
(Ht : type.is_not_higher_order t = true)
Expand All @@ -1411,14 +1422,14 @@ Module Compilers.
(Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1)
(Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
ZRange.type.base.option.is_bounded_by
(partial.Extract false E b_in)
(type.app_curried (expr.Interp (@ident.interp) (StripAnnotations E b_in)) arg1)
(partial.Extract assume_cast_truncates E b_in)
(type.app_curried (expr.Interp (@ident.interp) (StripAnnotations assume_cast_truncates E b_in)) arg1)
= true.
Proof using Type.
cbv [StripAnnotations].
intros; rewrite <- Extract_FromFlat_ToFlat by auto with wf typeclass_instances.
apply (let E := GeneralizeVar.GeneralizeVar (E _) in
@interp_strip_annotations t (E _) (E _) (E _));
@interp_strip_annotations assume_cast_truncates t (E _) (E _) (E _));
try assumption;
try apply GeneralizeVar.Wf_GeneralizeVar;
try apply GeneralizeVar.Wf3_GeneralizeVar;
Expand All @@ -1445,7 +1456,7 @@ Module Compilers.
Import API.

Lemma Interp_PartialEvaluateWithBounds
relax_zrange skip_annotations_under strip_preexisting_annotations
relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations
(Hrelax : forall r r' z, is_tighter_than_bool z r = true
-> relax_zrange r = Some r'
-> is_tighter_than_bool z r' = true)
Expand All @@ -1456,7 +1467,7 @@ Module Compilers.
: forall arg1 arg2
(Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
(Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
type.app_curried (expr.Interp (@ident.interp) (PartialEvaluateWithBounds relax_zrange skip_annotations_under strip_preexisting_annotations E b_in)) arg1
type.app_curried (expr.Interp (@ident.interp) (PartialEvaluateWithBounds relax_zrange skip_annotations_under strip_preexisting_annotations assume_cast_truncates E b_in)) arg1
= type.app_curried (expr.Interp (@ident.interp) E) arg2.
Proof.
cbv [PartialEvaluateWithBounds].
Expand All @@ -1470,7 +1481,7 @@ Module Compilers.
Qed.

Lemma Interp_PartialEvaluateWithBounds_bounded
relax_zrange skip_annotations_under strip_preexisting_annotations
relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations
(Hrelax : forall r r' z, is_tighter_than_bool z r = true
-> relax_zrange r = Some r'
-> is_tighter_than_bool z r' = true)
Expand All @@ -1482,14 +1493,14 @@ Module Compilers.
(Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1)
(Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
ZRange.type.base.option.is_bounded_by
(partial.Extract false E b_in)
(type.app_curried (expr.Interp (@ident.interp) (PartialEvaluateWithBounds relax_zrange skip_annotations_under strip_preexisting_annotations E b_in)) arg1)
(partial.Extract assume_cast_truncates E b_in)
(type.app_curried (expr.Interp (@ident.interp) (PartialEvaluateWithBounds relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations E b_in)) arg1)
= true.
Proof.
cbv [PartialEvaluateWithBounds].
intros arg1 Harg11 Harg1.
rewrite <- Extract_FromFlat_ToFlat by auto with wf typeclass_instances.
eapply Interp_EvalWithBound; eauto with wf typeclass_instances.
rewrite <- Extract_GeneralizeVar by auto with wf typeclass_instances.
eapply @Interp_EvalWithBound; eauto with wf typeclass_instances.
Qed.

Lemma Interp_PartialEvaluateWithListInfoFromBounds
Expand All @@ -1513,6 +1524,7 @@ Module Compilers.

Theorem CheckedPartialEvaluateWithBounds_Correct
(relax_zrange : zrange -> option zrange)
(assume_cast_truncates : bool)
(skip_annotations_under : forall t, ident t -> bool)
(strip_preexisting_annotations : bool)
(Hrelax : forall r r' z, is_tighter_than_bool z r = true
Expand All @@ -1523,7 +1535,7 @@ Module Compilers.
(Ht : type.is_not_higher_order t = true)
(b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
(b_out : ZRange.type.base.option.interp (type.final_codomain t))
rv (Hrv : CheckedPartialEvaluateWithBounds relax_zrange skip_annotations_under strip_preexisting_annotations E b_in b_out = inl rv)
rv (Hrv : CheckedPartialEvaluateWithBounds relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations E b_in b_out = inl rv)
: (forall arg1 arg2
(Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
(Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
Expand Down
Loading

0 comments on commit bcc5086

Please sign in to comment.