RoundoffEvaluators.scala 10.1 KB
Newer Older
1
// Copyright 2017 MPI-SWS, Saarbruecken, Germany
2
3

package daisy
Eva Darulova's avatar
Eva Darulova committed
4
package tools
5
6
7
8
9

import scala.collection.immutable.Seq

import lang.Trees._
import lang.Identifiers._
10
import lang.Types._
11
12
13
14
15
import lang.TreeOps.allVariablesOf
import FinitePrecision._
import Rational.{min, abs, sqrtDown, one}

trait RoundoffEvaluators extends RangeEvaluators {
16

17
  /**
Eva Darulova's avatar
Eva Darulova committed
18
19
20
21
22
23
24
25
26
27
   * Calculates the roundoff error for a given uniform precision
   * using interval arithmetic for ranges and affine arithmetic for errors.
   *
   * @param expr expression for which to compute roundoff
   * @param inputValMap real-valued ranges of all input variables
   * @param inputErrorMap errors of all input variables (incl. roundoff)
   * @param uniformPrecision precision for the entire computation
   *
   * @return (max. absolute roundoff error bound, real-valued result interval)
   */
28
29
30
31
32
  def uniformRoundoff_IA_AA(
    expr: Expr,
    inputValMap: Map[Identifier, Interval],
    inputErrorMap: Map[Identifier, Rational],
    uniformPrecision: Precision,
Eva Darulova's avatar
Eva Darulova committed
33
    trackRoundoffErrors: Boolean = true): (Rational, Interval) = {
34
35
36

    val (resRange, intermediateRanges) = evalRange[Interval](expr, inputValMap, Interval.apply)

Eva Darulova's avatar
Eva Darulova committed
37
38
    // println(intermediateRanges.mkString("\n"))

39
    val (resRoundoff, allErrors) = evalRoundoff[AffineForm](expr, intermediateRanges,
Eva Darulova's avatar
Eva Darulova committed
40
41
42
43
44
45
46
      allVariablesOf(expr).map(id => (id -> uniformPrecision)).toMap,
      inputErrorMap.map(x => (x._1 -> AffineForm.fromError(x._2))),
      zeroError = AffineForm.zero,
      fromError = AffineForm.fromError,
      interval2T = AffineForm.apply,
      constantsPrecision = uniformPrecision,
      trackRoundoffErrors)
47

Eva Darulova's avatar
Eva Darulova committed
48
    (Interval.maxAbs(resRoundoff.toInterval), resRange)
49
50
  }

51
  /**
Eva Darulova's avatar
Eva Darulova committed
52
53
54
55
56
57
58
59
   * Calculates the roundoff error for a given uniform precision
   * using affine arithmetic for ranges and affine arithmetic for errors.
   *
   * @param expr expression for which to compute roundoff
   * @param inputValMap real-valued ranges of all input variables
   * @param inputErrorMap errors of all input variables (incl. roundoff)
   * @param uniformPrecision precision for the entire computation
   */
60
61
62
63
64
  def uniformRoundoff_AA_AA(
    expr: Expr,
    inputValMap: Map[Identifier, Interval],
    inputErrorMap: Map[Identifier, Rational],
    uniformPrecision: Precision,
Eva Darulova's avatar
Eva Darulova committed
65
    trackRoundoffErrors: Boolean = true): (Rational, Interval) = {
66
67

    val (resRange, intermediateRanges) = evalRange[AffineForm](expr,
Eva Darulova's avatar
Eva Darulova committed
68
      inputValMap.map(x => (x._1 -> AffineForm(x._2))), AffineForm.apply)
69
70

    val (resRoundoff, allErrors) = evalRoundoff[AffineForm](expr,
Eva Darulova's avatar
Eva Darulova committed
71
72
73
74
75
76
77
78
      intermediateRanges.map(x => (x._1 -> x._2.toInterval)),
      allVariablesOf(expr).map(id => (id -> uniformPrecision)).toMap,
      inputErrorMap.map(x => (x._1 -> AffineForm.fromError(x._2))),
      zeroError = AffineForm.zero,
      fromError = AffineForm.fromError,
      interval2T = AffineForm.apply,
      constantsPrecision = uniformPrecision,
      trackRoundoffErrors)
79

Eva Darulova's avatar
Eva Darulova committed
80
    (Interval.maxAbs(resRoundoff.toInterval), resRange.toInterval)
81
82
83
  }

  /**
Eva Darulova's avatar
Eva Darulova committed
84
85
86
87
88
89
90
91
   * Calculates the roundoff error for a given uniform precision
   * using SMTRange for ranges and affine arithmetic for errors.
   *
   * @param expr expression for which to compute roundoff
   * @param inputValMap real-valued ranges of all input variables
   * @param inputErrorMap errors of all input variables (incl. roundoff)
   * @param uniformPrecision precision for the entire computation
   */
92
93
94
95
96
  def uniformRoundoff_SMT_AA(
    expr: Expr,
    inputValMap: Map[Identifier, Interval],
    inputErrorMap: Map[Identifier, Rational],
    uniformPrecision: Precision,
Eva Darulova's avatar
Eva Darulova committed
97
    trackRoundoffErrors: Boolean = true): (Rational, Interval) = {
98
99

    val (resRange, intermediateRanges) = evalRange[SMTRange](expr,
Eva Darulova's avatar
Eva Darulova committed
100
101
      inputValMap.map({ case (id, int) => (id -> SMTRange(Variable(id), int)) }),
      SMTRange.apply)
102
103

    val (resRoundoff, allErrors) = evalRoundoff[AffineForm](expr,
Eva Darulova's avatar
Eva Darulova committed
104
105
106
107
108
109
110
111
      intermediateRanges.map(x => (x._1 -> x._2.toInterval)),
      allVariablesOf(expr).map(id => (id -> uniformPrecision)).toMap,
      inputErrorMap.map(x => (x._1 -> AffineForm.fromError(x._2))),
      zeroError = AffineForm.zero,
      fromError = AffineForm.fromError,
      interval2T = AffineForm.apply,
      constantsPrecision = uniformPrecision,
      trackRoundoffErrors)
112

Eva Darulova's avatar
Eva Darulova committed
113
    (Interval.maxAbs(resRoundoff.toInterval), resRange.toInterval)
114
115
116
117
118
119
120
121
122
123
  }

  /**
    Computes the absolute roundoff error for the given expression.

    The ranges of all the intermediate expressions have to be given in rangeMap.
    Allows mixed-precision by providing (possibly different) precisions for
    all declared variables (input parameters as well as locally defined variables.)
    Constants are assumed to be all in one precision, given by the user.

Eva Darulova's avatar
Eva Darulova committed
124
   */
125
126
127
128
129
130
131
132
133
  def evalRoundoff[T <: RangeArithmetic[T]](
    expr: Expr,
    rangeMap: Map[Expr, Interval],
    precisionMap: Map[Identifier, Precision],
    initErrorMap: Map[Identifier, T],
    zeroError: T,
    fromError: Rational => T,
    interval2T: Interval => T,
    constantsPrecision: Precision,
Eva Darulova's avatar
Eva Darulova committed
134
135
    trackRoundoffErrors: Boolean         // if false, propagate only initial errors
    ): (T, Map[Expr, T]) = {
136
137
138
139
140


    var intermediateErrors: Map[Expr, T] = Map.empty

    // TODO: check the effectiveness of this
Eva Darulova's avatar
Eva Darulova committed
141
    // @inline
142
143
144
145
146
147
148
149
150
    def computeNewError(range: Interval, propagatedError: T, prec: Precision): T =
      if (trackRoundoffErrors) {
        val actualRange: Interval = range + propagatedError.toInterval
        val rndoff = prec.absRoundoff(actualRange)
        propagatedError +/- rndoff
      } else {
        propagatedError
      }

='s avatar
= committed
151
    def eval(e: Expr, errorMap: Map[Identifier, T]): (T, Precision) = (e: @unchecked) match {
152
153

      case x @ RealLiteral(r) =>
154
155
156
157
        val rndoff =
          //if (isExactInFloats(r, constantsPrecision) || !trackRoundoffErrors) {
          //zeroError
          //} else {
158
          fromError(constantsPrecision.absRoundoff(r))
159
    //}
160
161
162
163
164
165
166
167
168
169
170
171
        intermediateErrors += (x -> rndoff)
        (rndoff, constantsPrecision)

      case x @ Variable(id) =>
        // TODO: if the error is just a roundoff, then we can also compute it here...
        val rndoff = errorMap(id)
        intermediateErrors += (x -> rndoff)
        (rndoff, precisionMap(id))

      case x @ Plus(lhs, rhs) =>
        val range = rangeMap(x)

='s avatar
= committed
172
173
        val (rndoffLhs, precLhs) = eval(lhs, errorMap)
        val (rndoffRhs, precRhs) = eval(rhs, errorMap)
174
175
176
177
178
179
180
181
182
183
        val propagatedError = rndoffLhs + rndoffRhs

        val prec = getUpperBound(precLhs, precRhs)  // Scala semantics
        val rndoff = computeNewError(range, propagatedError, prec)
        intermediateErrors += (x -> rndoff)
        (rndoff, prec)

      case x @ Minus(lhs, rhs) =>
        val range = rangeMap(x)

='s avatar
= committed
184
185
        val (rndoffLhs, precLhs) = eval(lhs, errorMap)
        val (rndoffRhs, precRhs) = eval(rhs, errorMap)
186
187
188
189
190
191
192
193
194
195
196
197
        val propagatedError = rndoffLhs - rndoffRhs

        val prec = getUpperBound(precLhs, precRhs)
        val rndoff = computeNewError(range, propagatedError, prec)
        intermediateErrors += (x -> rndoff)
        (rndoff, prec)

      case x @ Times(lhs, rhs) =>
        val range = rangeMap(x)
        val rangeLhs = rangeMap(lhs)
        val rangeRhs = rangeMap(rhs)

='s avatar
= committed
198
199
        val (rndoffLhs, precLhs) = eval(lhs, errorMap)
        val (rndoffRhs, precRhs) = eval(rhs, errorMap)
200

Eva Darulova's avatar
Eva Darulova committed
201
202
203
204
        val propagatedError =
          interval2T(rangeLhs) * rndoffRhs +
          interval2T(rangeRhs) * rndoffLhs +
          rndoffLhs * rndoffRhs
205
206
207
208
209
210
211
212
213
214
215
216

        val prec = getUpperBound(precLhs, precRhs)
        val rndoff = computeNewError(range, propagatedError, prec)
        intermediateErrors += (x -> rndoff)
        (rndoff, prec)


      case x @ Division(lhs, rhs) =>
        val range = rangeMap(x)
        val rangeLhs = rangeMap(lhs)
        val rangeRhs = rangeMap(rhs)

='s avatar
= committed
217
218
        val (rndoffLhs, precLhs) = eval(lhs, errorMap)
        val (rndoffRhs, precRhs) = eval(rhs, errorMap)
219
220
221
222

        // inverse, i.e. we are computing x * (1/y)
        val rightInterval = rangeRhs + rndoffRhs.toInterval // the actual interval, incl errors

Eva Darulova's avatar
Eva Darulova committed
223
224
225
226
        // the actual error interval can now contain 0, check this
        if (rightInterval.xlo <= 0 && rightInterval.xhi >= 0) {
          throw DivisionByZeroException("trying to divide by error interval containing 0")
        }
227
228
229
230
231
232
233
        val a = min(abs(rightInterval.xlo), abs(rightInterval.xhi))
        val errorMultiplier: Rational = -one / (a*a)
        val invErr = rndoffRhs * errorMultiplier

        // error propagation
        val inverse: Interval = rangeRhs.inverse

Eva Darulova's avatar
Eva Darulova committed
234
235
236
237
        var propagatedError =
          interval2T(rangeLhs) * invErr +
          interval2T(inverse) * rndoffLhs +
          rndoffLhs * invErr
238
239
240
241
242
243
244

        val prec = getUpperBound(precLhs, precRhs)
        val rndoff = computeNewError(range, propagatedError, prec)
        intermediateErrors += (x -> rndoff)
        (rndoff, prec)

      case x @ UMinus(t) =>
='s avatar
= committed
245
        val (rndoff, prec) = eval(t, errorMap)
246
247
248
249
250
251
252
        intermediateErrors += (x -> - rndoff)
        (- rndoff, prec)

      case x @ Sqrt(t) =>
        // TODO: needs to fail for fixed-point precision
        val range = rangeMap(x)
        val rangeT = rangeMap(t)
='s avatar
= committed
253
        val (errorT, prec) = eval(t, errorMap)
254
255
256
257
258
259
260
261
262
263
264
265
266
267

        val tInterval = rangeT
        val a = min(abs(tInterval.xlo), abs(tInterval.xhi))
        val errorMultiplier = Rational(1L, 2L) / sqrtDown(a)
        val propagatedError = errorT * errorMultiplier

        // TODO: check that this operation exists for this precision
        val rndoff = computeNewError(range, propagatedError, prec)

        intermediateErrors += (x -> rndoff)
        (rndoff, prec)


      case x @ Let(id, value, body) =>
='s avatar
= committed
268
        val (valueRndoff, valuePrec) = eval(value, errorMap)
269

Eva Darulova's avatar
Eva Darulova committed
270
        // downcast required
271
        val idPrec = precisionMap(id)
Eva Darulova's avatar
Eva Darulova committed
272
273
        val rndoff = if (idPrec < valuePrec) { // we need to cast down
          val valueRange = rangeMap(value)
274
275
276
          val err = computeNewError(valueRange, valueRndoff, idPrec)
          val _ = intermediateErrors += (Downcast(value,FinitePrecisionType(idPrec)) -> err)
          err
Eva Darulova's avatar
Eva Darulova committed
277
278
        } else {
          valueRndoff
='s avatar
= committed
279
        }
280
        intermediateErrors += (Variable(id) -> rndoff)
='s avatar
= committed
281
        eval(body, errorMap + (id -> rndoff))
282
283

    }
='s avatar
= committed
284
    val (resRndoff, resPrecision) = eval(expr, initErrorMap)
285
286
287
288
    (resRndoff, intermediateErrors)
  }


289
}