RangeErrorPhase.scala 5.27 KB
Newer Older
1
2
3
4

package daisy
package analysis

Eva Darulova's avatar
Eva Darulova committed
5
import lang.NumAnnotation
6
7
8
9
10
11
12
13
14
15
16
17
18
import lang.Trees._
import utils._
import FinitePrecision._
import Rational._
import lang.Identifiers._

/**
  ??? Description goes here


  Prerequisites:
    - SpecsProcessingPhase
 */
19
object RangeErrorPhase extends DaisyPhase with ErrorFunctions {
20
21
22

  override val name = "range-error phase"
  override val description = "Computes ranges and absolute errors"
23
  override val definedOptions: Set[CmdLineOptionDef[Any]] = Set(
24
25
26
    ChoiceOptionDef("rangeMethod", "Method to use for range analysis",
      Set("affine", "interval", "smt", "subdiv"), "interval"),
    FlagOptionDef("noInitialErrors", "do not track initial errors specified by user"),
27
28
    FlagOptionDef("noRoundoff", "do not track roundoff errors"),
    ChoiceOptionDef("precision", "Type of precision to use",
29
30
      Set("Float32", "Float64", "DoubleDouble", "QuadDouble",
        "Fixed16", "Fixed32", "Fixed64"), "Float64")
31
32
33
34
35
36
    )

  implicit val debugSection = DebugSectionAnalysis

  var reporter: Reporter = null

37
  // Var for error functions
Einar Horn's avatar
Einar Horn committed
38
  // trackRoundoffErrs and uniformPrecision assigned below in run
39
40
  attachToTree = true

41
42
43
44
45
46
47
  override def run(ctx: Context, prg: Program): (Context, Program) = {
    reporter = ctx.reporter
    reporter.info(s"\nStarting $name")
    val timer = ctx.timers.rangeError.start

    // default range method: intervals
    var rangeMethod = "interval"
Eva Darulova's avatar
Eva Darulova committed
48
    var errorMethod = "affine"   // only one supported so far
49
50

    var trackInitialErrs = true
Einar Horn's avatar
Einar Horn committed
51
52

    // setting trait variables
Einar Horn's avatar
Einar Horn committed
53
    trackRoundoffErrs = true
54
    var uniformPrecision: Precision = Float64
55

56
57
58
59
60
61
62
63
64
65
66
    // process relevant options
    for (opt <- ctx.options) opt match {
      case ChoiceOption("rangeMethod", s) => s match {
        case "interval" | "affine" | "smt" | "subdiv" =>
          rangeMethod = s
          reporter.info(s"using $s")
        case _ =>
          reporter.warning(s"Unknown range method: $s, choosing default (interval)!")
      }
      case FlagOption("noInitialErrors") => trackInitialErrs = false
      case FlagOption("noRoundoff") => trackRoundoffErrs = false
67
68
      case ChoiceOption("precision", s) => s match {
        case "Float32" =>
Einar Horn's avatar
Einar Horn committed
69
          uniformPrecision = Float32
70
71
          reporter.info(s"using $s")
        case "Float64" =>
Einar Horn's avatar
Einar Horn committed
72
          uniformPrecision = Float64
73
74
          reporter.info(s"using $s")
        case "DoubleDouble" =>
Einar Horn's avatar
Einar Horn committed
75
          uniformPrecision = DoubleDouble
76
77
          reporter.info(s"using $s")
        case "QuadDouble" =>
Einar Horn's avatar
Einar Horn committed
78
          uniformPrecision = QuadDouble
79
          reporter.info(s"using $s")
80
81
82
83
84
85
        case "Fixed16" =>
          uniformPrecision = Fixed(16)
        case "Fixed32" =>
          uniformPrecision = Fixed(32)
        case "Fixed64" =>
          uniformPrecision = Fixed(64)
86
87
88
        case _ =>
          reporter.warning(s"Unknown precision specified: $s, choosing default (Float64)!")
      }
89
90
91
      case _ =>
    }

92
93
94
95
    val fncsToConsider: Seq[String] = functionsToConsider(ctx, prg)

    for (fnc <- prg.defs)
      if (!fnc.precondition.isEmpty && !fnc.body.isEmpty && fncsToConsider.contains(fnc.id.toString)){
96

97
      reporter.info("analyzing fnc: " + fnc.id)
98
99
100
101
102
103
104
105
106
107
108
      val inputValMap: Map[Identifier, Interval] = ctx.inputRanges(fnc.id)

      // If we track both input and roundoff errors, then we pre-compute
      // the roundoff errors for those variables that do not have a user-defined
      // error, in order to keep correlations.
      val inputErrorMap: Map[Identifier, Rational] =
        if (trackInitialErrs && trackRoundoffErrs){

          val inputErrs = ctx.inputErrors(fnc.id)
          val allIDs = fnc.params.map(_.id).toSet
          val missingIDs = allIDs -- inputErrs.keySet
Einar Horn's avatar
Einar Horn committed
109
          inputErrs ++ missingIDs.map( id => (id -> uniformPrecision.absRoundoff(inputValMap(id))))
110
111
112
113
114
115
116
117
118
119
120

        } else if(trackInitialErrs) {

          val inputErrs = ctx.inputErrors(fnc.id)
          val allIDs = fnc.params.map(_.id).toSet
          val missingIDs = allIDs -- inputErrs.keySet
          inputErrs ++ missingIDs.map( id => (id -> zero))

        } else if (trackRoundoffErrs) {

          val allIDs = fnc.params.map(_.id)
Einar Horn's avatar
Einar Horn committed
121
          allIDs.map( id => (id -> uniformPrecision.absRoundoff(inputValMap(id)))).toMap
122
123
124
125
126
127
128
129
130
131
132
133
134

        } else {

          val allIDs = fnc.params.map(_.id)
          allIDs.map( id => (id -> zero)).toMap

        }

      // TODO: Interval-only based error estimation; should be a very quick fix


      (rangeMethod, errorMethod) match {
        case ("interval", "affine") =>
135
          errorIntervalAffine(fnc.body.get, inputValMap, inputErrorMap, uniformPrecision)
136
137

        case ("affine", "affine") =>
138
          errorAffineAffine(fnc.body.get, inputValMap, inputErrorMap, uniformPrecision)
139
140

        case ("smt", "affine") =>
141
          errorSMTAffine(fnc.body.get, inputValMap, inputErrorMap, uniformPrecision)
142

Eva Darulova's avatar
Eva Darulova committed
143
144
145
146
147
148
        // default is to use the method that attaches the info to trees.
        case ("subdiv", _) =>
            evaluateSubdiv(
              fnc.body.get,
              inputValMap,
              inputErrorMap,
149
              trackRoundoffErrs,
Einar Horn's avatar
Einar Horn committed
150
              uniformPrecision)
151
152
153
154
155
156
157
158
159
160
161
162
163

        case _ =>
          reporter.fatalError(s"Your combination of $rangeMethod and $errorMethod" +
            "for computing ranges and errors is not supported.")
      }

    }

    timer.stop
    ctx.reporter.info(s"Finished $name")
    (ctx, prg)
  }

Eva Darulova's avatar
Eva Darulova committed
164

165
}