FPRangeValidator.v 8.92 KB
Newer Older
1 2 3
From Flover
     Require Import Expressions Commands Environments ssaPrgs Typing
     IntervalValidation ErrorValidation Infra.Ltacs Infra.RealRationalProps.
Heiko Becker's avatar
Heiko Becker committed
4

5
Fixpoint FPRangeValidator (e:expr Q) (A:analysisResult) typeMap dVars {struct e} : bool :=
6
  match FloverMap.find e typeMap, FloverMap.find e A with
Heiko Becker's avatar
Heiko Becker committed
7 8 9 10 11 12 13
  |Some m, Some (iv_e, err_e) =>
   let iv_e_float := widenIntv iv_e err_e in
   let recRes :=
       match e with
       | Binop b e1 e2 =>
         FPRangeValidator e1 A typeMap dVars &&
         FPRangeValidator e2 A typeMap dVars
14 15 16 17
       | Fma e1 e2 e3 =>
         FPRangeValidator e1 A typeMap dVars &&
         FPRangeValidator e2 A typeMap dVars &&
         FPRangeValidator e3 A typeMap dVars
Heiko Becker's avatar
Heiko Becker committed
18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
       | Unop u e =>
         FPRangeValidator e A typeMap dVars
       | Downcast m e => FPRangeValidator e A typeMap dVars
       | _ =>  true
       end
   in
   match e with
   | Var _ v =>
     if NatSet.mem v dVars
     then true
     else
       if (validValue (ivhi iv_e_float) m &&
           validValue (ivlo iv_e_float) m)
       then ((normal (ivlo iv_e_float) m) || (Qeq_bool (ivlo iv_e_float) 0)) &&
             (normal (ivhi iv_e_float) m || (Qeq_bool (ivhi iv_e_float) 0)) &&
              recRes
       else
         false
   | _ => if (validValue (ivhi iv_e_float) m &&
              validValue (ivlo iv_e_float) m)
         then ((normal (ivlo iv_e_float) m) || (Qeq_bool (ivlo iv_e_float) 0)) &&
               (normal (ivhi iv_e_float) m || (Qeq_bool (ivhi iv_e_float) 0)) && recRes
         else
           false
   end
  | _, _ => false
Heiko Becker's avatar
Heiko Becker committed
44 45
  end.

Heiko Becker's avatar
Heiko Becker committed
46 47 48 49 50 51 52
Fixpoint FPRangeValidatorCmd (f:cmd Q) (A:analysisResult) typeMap dVars :=
  match f with
  | Let m n e g =>
    if FPRangeValidator e A typeMap dVars
    then FPRangeValidatorCmd g A typeMap (NatSet.add n dVars)
     else false
| Ret e => FPRangeValidator e A typeMap dVars
53 54
  end.

55 56 57
Ltac prove_fprangeval m v L1 R:=
  destruct m eqn:?; try auto;
  unfold normal, Normal, validValue, Denormal in *; canonize_hyps;
58
  try rewrite orb_true_iff in *;
59 60 61 62 63 64 65 66
  destruct L1; destruct R; canonize_hyps;
  rewrite <- Rabs_eq_Qabs in *;
  Q2R_to_head;
  rewrite <- Q2R_minus, <- Q2R_plus in *;
  repeat (match goal with
          |H: _ = true |- _ => andb_to_prop H
          end);
  destruct (Req_dec v 0); try auto;
67
  destruct (Rle_lt_dec (Rabs v) (Q2R (minValue_pos m)))%R (* denormal case *);
68 69 70
  try auto;
  destruct (Rle_lt_dec (Rabs v) (Q2R (maxValue m)))%R; lra.

71
Theorem FPRangeValidator_sound:
72
  forall (e:expr Q) E1 E2 Gamma v m A tMap fVars dVars,
73
  approxEnv E1 Gamma A fVars dVars E2 ->
74
  eval_expr E2 Gamma (toRExp e) v m ->
75
  typeCheck e Gamma tMap = true ->
76
  validRanges e A E1 Gamma ->
77 78 79
  validErrorbound e tMap A dVars = true ->
  FPRangeValidator e A tMap dVars = true ->
  NatSet.Subset (NatSet.diff (usedVars e) dVars) fVars ->
Heiko Becker's avatar
Heiko Becker committed
80 81
  vars_typed (NatSet.union fVars dVars) Gamma ->
 (forall v, NatSet.In v dVars ->
82
        exists vF m, E2 v = Some vF /\ FloverMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) ->
83 84 85 86 87
  validFloatValue v m.
Proof.
  intros *.
  unfold FPRangeValidator.
  intros.
88
  assert (FloverMap.find e tMap = Some m)
89 90
    as type_e
      by (eapply typingSoundnessExp; eauto).
91
  unfold validFloatValue.
92 93
  pose proof (validRanges_single _ _ _ _ H2) as valid_e.
  destruct valid_e as [iv_e [err_e [vR[ map_e[eval_real vR_bounded]]]]].
Heiko Becker's avatar
Heiko Becker committed
94 95 96
  destruct iv_e as  [e_lo e_hi].
  assert (Rabs (vR - v) <= Q2R (err_e))%R.
  { eapply validErrorbound_sound; eauto. }
97 98 99
  destruct (distance_gives_iv (a:=vR) v (e:=Q2R err_e) (Q2R e_lo, Q2R e_hi))
    as [v_in_errIv];
    try auto.
Heiko Becker's avatar
Heiko Becker committed
100
  simpl in *.
101 102 103 104 105
  assert (Rabs v <= Rabs (Q2R e_hi + Q2R err_e) \/
          Rabs v <= Rabs (Q2R e_lo - Q2R err_e))%R
    as abs_bounded
    by (apply bounded_inAbs; auto).
  destruct e;
Heiko Becker's avatar
Heiko Becker committed
106 107
    unfold validFloatValue in *; cbn in *;
      rewrite type_e in *; cbn in *.
108
  - Flover_compute.
109 110 111 112 113 114 115
    destruct (n mem dVars) eqn:?.
    + set_tac. edestruct H7 as [? [? [? [? ?]]]]; eauto.
      rewrite H10 in type_e; inversion type_e; subst.
      inversion H0; subst.
      rewrite H14 in H3; inversion H3; subst.
      auto.
    + Flover_compute. prove_fprangeval m v L2 R.
116
  - Flover_compute; try congruence.
117 118 119
    type_conv; subst.
    prove_fprangeval m v L1 R.
  - Flover_compute; destruct u; Flover_compute; try congruence.
Heiko Becker's avatar
Heiko Becker committed
120 121
    type_conv; subst.
    prove_fprangeval m0 v L1 R.
122
  - Flover_compute; try congruence.
Heiko Becker's avatar
Heiko Becker committed
123 124
    type_conv; subst.
    prove_fprangeval (join m0 m1) v L1 R.
125
  - Flover_compute; try congruence.
Heiko Becker's avatar
Heiko Becker committed
126
    type_conv; subst.
127
    prove_fprangeval (join3 m0 m1 m2) v L1 R.
128
  - Flover_compute; try congruence.
129
    type_conv; subst.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
130
    prove_fprangeval m v L1 R.
131
Qed.
132

133
Lemma FPRangeValidatorCmd_sound (f:cmd Q):
134
  forall E1 E2 Gamma v vR m A tMap fVars dVars outVars,
135 136 137 138 139
  approxEnv E1 Gamma A fVars dVars E2 ->
  ssa f (NatSet.union fVars dVars) outVars ->
  bstep (toREvalCmd (toRCmd f)) E1 (toRMap Gamma) vR m ->
  bstep (toRCmd f) E2 Gamma v m ->
  typeCheckCmd f Gamma tMap = true ->
140
  validRangesCmd f A E1 Gamma ->
141 142 143
  validErrorboundCmd f tMap A dVars = true ->
  FPRangeValidatorCmd f A tMap dVars = true ->
  NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars ->
Heiko Becker's avatar
Heiko Becker committed
144 145
  vars_typed (NatSet.union fVars dVars) Gamma ->
 (forall v, NatSet.In v dVars ->
146
        exists vF m, E2 v = Some vF /\ FloverMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) ->
147 148 149 150 151 152 153 154 155
  validFloatValue v m.
Proof.
  induction f; intros;
    simpl in *;
    (match_pat (bstep _ _ (toRMap _) _ _) (fun H => inversion H; subst; simpl in *));
     (match_pat (bstep _ _ Gamma _ _) (fun H => inversion H; subst; simpl in *));
      repeat match goal with
             | H : _ = true |- _ => andb_to_prop H
             end.
156
      - assert (FloverMap.find e tMap = Some m)
157 158
          by(eapply typingSoundnessExp; eauto).
        match_pat (ssa _ _ _) (fun H => inversion H; subst; simpl in *).
159
        Flover_compute.
160 161 162 163 164 165 166 167 168
        destruct H4 as [[valid_e valid_rec] valid_single].
        pose proof (validRanges_single _ _ _ _ valid_e) as valid_e_single.
        destruct valid_e_single
          as [iv_e [err_e [vR_e [map_e [eval_e_real bounded_vR_e]]]]].
        destr_factorize.
        edestruct (validErrorbound_sound e (E1:=E1) (E2:=E2) (fVars:=fVars)
                                         (dVars := dVars) (A:=A) tMap
                                         (nR:=v0) (err:=err_e) (elo:=fst iv_e) (ehi:=snd iv_e))
          as [[vF_e [m_e eval_float_e]] err_bounded_e]; eauto.
169
        + set_tac. split; try auto.
Heiko Becker's avatar
Heiko Becker committed
170 171
          split; try auto.
          hnf; intros; subst; set_tac.
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191
        + destruct iv_e; auto.
        + rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H18) in *; try auto.
          apply (IHf (updEnv n vR_e E1) (updEnv n v1 E2)
                     (updDefVars n m Gamma) v vR m0 A tMap fVars
                     (NatSet.add n dVars) (outVars)); eauto.
          * eapply approxUpdBound; eauto.
            simpl in *.
            apply Rle_trans with (r2:= Q2R err_e); try lra.
            eapply err_bounded_e. eauto.
            apply Qle_Rle.
            rewrite Qeq_bool_iff in *.
            destruct i0; inversion Heqo0; subst.
            rewrite R2.
            lra.
          * eapply ssa_equal_set; eauto.
            hnf. intros a; split; intros in_set.
            { rewrite NatSet.add_spec, NatSet.union_spec;
                rewrite NatSet.union_spec, NatSet.add_spec in in_set.
              destruct in_set as [P1 | [ P2 | P3]]; auto. }
            { rewrite NatSet.add_spec, NatSet.union_spec in in_set;
192
                  rewrite NatSet.union_spec, NatSet.add_spec.
193 194 195 196 197 198 199 200 201 202 203 204
              destruct in_set as [P1 | [ P2 | P3]]; auto. }
          * eapply (swap_Gamma_bstep (Gamma1 := updDefVars n REAL (toRMap Gamma))); eauto.
            eauto using Rmap_updVars_comm.
          * apply validRangesCmd_swap with (Gamma1:=updDefVars n REAL Gamma).
            { intros x; unfold toRMap, updDefVars.
              destruct (x =? n) eqn:?; auto. }
            { eapply valid_rec. auto. }
          * set_tac; split.
            { split; try auto.
              hnf; intros; subst.
              apply H5; rewrite NatSet.add_spec; auto. }
            { hnf; intros.
205
                apply H5; rewrite NatSet.add_spec; auto. }
206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226
          * unfold vars_typed. intros.
            unfold updDefVars.
            destruct (v2 =? n) eqn:?; eauto.
            apply H8. rewrite NatSet.union_spec in *.
            destruct H4; try auto.
            rewrite NatSet.add_spec in H4.
            rewrite Nat.eqb_neq in *.
            destruct H4; subst; try congruence; auto.
          * intros. unfold updEnv.
            type_conv; subst.
            destruct (v2 =? n) eqn:?; try rewrite Nat.eqb_eq in *;
              try rewrite Nat.eqb_neq in *.
            { exists v1; subst. exists m1; repeat split; try auto.
              eapply FPRangeValidator_sound; eauto.
              set_tac. split; try auto.
              split; try auto.
              hnf; intros; subst; set_tac. }
            { apply H9.
              rewrite NatSet.add_spec in H4; destruct H4;
                auto; subst; congruence. }
  - destruct H4. eapply FPRangeValidator_sound; eauto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
227
Qed.