Module PedraZ

This module offers an abstract domain of polyhedra which takes as inputs linear integer expressions (LinExpr.ZExpr).

Require String.
Require Import ZNoneItv.
Require Import Itv.
Require Import ASAtomicCond.
Require Import PedraQ.
Require Import AssignD.
Import ZCond.

Module BasicD.

  Definition t:= BasicD.t.

  Definition gamma (a:t) m
    := BasicD.gamma a (Mem.lift ZtoQ.ofZ m).

   Instance gamma_ext: Proper (Logic.eq ==> pointwise_relation PVar.t Logic.eq ==> iff) gamma.

Proof.

     unfold gamma.
     intros x y H m1 m2 H0. subst; rewrite H0; tauto.
   Qed.

  Definition isIncl:=BasicD.isIncl.
  Global Opaque BasicD.isIncl.

  Lemma isIncl_correct: forall a1 a2, If isIncl a1 a2 THEN forall m, gamma a1 m -> gamma a2 m.

Proof.

unfold gamma. VPLAsimplify.
Qed.

  Definition top:= BasicD.top.

  Lemma top_correct: forall m, gamma top m.
    simpl; auto.
  Qed.

  Hint Resolve top_correct: vpl.

  Definition bottom: t := BasicD.bottom.

  Lemma bottom_correct: forall m, ~(gamma bottom m).

Proof.

simpl; auto.
Qed.

  Definition isBottom : t -> imp bool
    := fun p => BasicD.isBottom p.

  Lemma isBottom_correct : forall a, If isBottom a THEN forall m, gamma a m -> False.

Proof.

    unfold isBottom.
    unfold gamma.
    VPLAsimplify.
    intro.
    eapply (BasicD.isBottom_correct a true Hexta).
  Qed.

  Definition widen:= BasicD.widen.

  Definition join:= BasicD.join.

  Lemma join_correct a1 a2: WHEN p <- join a1 a2 THEN forall m, gamma a1 m \/ gamma a2 m -> gamma p m.

Proof.

unfold gamma; VPLAsimplify.
Qed.

  Definition project (a:t) (x:PVar.t) : imp t :=
    BasicD.project a x.

  Lemma project_correct: forall a x, WHEN p <- project a x THEN forall m v, gamma a m -> gamma p (Mem.assign x v m).

Proof.

    unfold gamma. VPLAsimplify.
    simpl. intros; autorewrite with vpl; auto.
  Qed.

  Definition rename (x y: PVar.t) (a:t): imp t :=
    Rename.rename x y a.

  Lemma rename_correct: forall x y a, WHEN p <- (rename x y a) THEN
    forall m, gamma a (Mem.assign x (m y) m) -> gamma p m.

Proof.

    unfold gamma. VPLAsimplify.
    simpl; intros H m; autorewrite with vpl; auto.
  Qed.

  Definition pr: t -> String.string
    := fun ab => BasicD.pr ab.

  Import LinTerm.
  Import String.
  Definition get_itv_msg :="get_itv: non-affine term "%string.

  Definition get_itv: ZTerm.t -> t -> imp ZItv.t
    := fun a ab =>
     let (te,aft) := ZTerm.affineDecompose a in
     if ZTerm.pseudoIsZero te then
       BIND qitv <- ItvD.getItv ab (LinQ.lift (ZAffTerm.lin aft)) -;
          pure (proj1_sig (ZItv.fromQItv (QItv.shift qitv (ZtoQ.ofZ (ZAffTerm.cte aft)))))
     else
          pure (trace DEBUG (get_itv_msg ++ (ZTerm.pr a)) (projT1 (ZItv.mk ZItv.Infty ZItv.Infty))).

  Import ZNum.

  Lemma get_itv_correct t a:
    WHEN i <- get_itv t a THEN forall m, gamma a m -> ZItv.sat i (ZTerm.eval t m).

Proof.

    unfold get_itv.
    xasimplify ltac: (eauto with pedraQ vpl). simpl in * |- *.
    intros m X. apply (proj2_sig (ZItv.fromQItv _)).
    generalize (ZTerm.affineDecompose_correct t m).
    rewrite H. intros X0; ring_simplify in X0. rewrite <- X0.
    unfold ZAffTerm.eval; autorewrite with num.
    rewrite QNum.AddComm.
    apply QItv.Shift_correct.
    rewrite <- LinQ.lift_correct.
    auto.
  Qed.

End BasicD.

Module ZNItvD <: HasGetItvMode ZNum ZTerm ZNoneItv.ZNItv BasicD.

  Import LinTerm.
  Import ZNItv.
  Import BasicD.

  Definition getItvMode mo te a :=
     let (te,aft) := ZTerm.affineDecompose te in
     if ZTerm.pseudoIsZero te then
          BIND qitv <- ItvD.getItvMode mo (LinQ.lift (ZAffTerm.lin aft)) a -;
          pure (add BOTH (fromQItv qitv) (single (ZAffTerm.cte aft)))
     else
          pure (failwith "get_itv: non-affine term" ZNItv.top).
  Extraction Inline getItvMode.

  Local Opaque ZNItv.add.
  Import ZNum.

  Lemma getItvMode_correct mo t a:
    WHEN i <- getItvMode mo t a THEN forall m, gamma a m -> ZNItv.sat i (ZTerm.eval t m).

Proof.

    unfold getItvMode.
    xasimplify ltac: (eauto with pedraQ vpl zn). simpl in * |- *.
    intros m X.
    generalize (ZTerm.affineDecompose_correct t m).
    rewrite H. intros X0; ring_simplify in X0. rewrite <- X0.
    unfold ZAffTerm.eval; autorewrite with num.
    apply add_correct; auto with zn.
    apply fromQItv_correct.
    rewrite <- LinQ.lift_correct.
    auto.
  Qed.

  Global Hint Resolve getItvMode_correct: vpl.
  Opaque getItvMode.

End ZNItvD.

Module CstrD <: HasAssume ZNum ZtoQCstr BasicD.

  Import BasicD.

  Definition assume (c:ZtoQCstr.t) (a:t) : imp t :=
    CstrD.assume c a.

  Lemma assume_correct: forall c a, WHEN p <- assume c a THEN forall m, ZtoQCstr.sat c m -> gamma a m -> gamma p m.

Proof.

unfold gamma. VPLAsimplify.
Qed.

End CstrD.

Module AtomicD := BasicD <+ ZAtomicCondAssume BasicD CstrD ZNItvD.

Module Dom <: AbstractDomain ZNum ZCond
  := BasicD <+ ZCondAssume BasicD AtomicD <+ ASCondAssert ZNum ZCond.

Module FullDom <: FullItvAbstractDomain ZNum ZCond ZItv
  := MakeAssign ZNum ZCond Dom Dom <+ AssignLiftItv ZNum ZCond ZItv Dom Dom Dom
                                   <+ AssignSimplePrinting ZNum ZCond Dom Dom Dom
  .