Commit 8f53156d authored by Eva Darulova's avatar Eva Darulova

removing NumAnnotation

parent 5fac5f68
......@@ -38,7 +38,7 @@
</check>
<check level="warning" class="org.scalastyle.scalariform.MethodNamesChecker" enabled="true">
<parameters>
<parameter name="regex"><![CDATA[^[a-z][A-Za-z0-9]*$]]></parameter>
<parameter name="regex"><![CDATA[^[a-z_][A-Za-z0-9]*$]]></parameter>
</parameters>
</check>
<check enabled="true" class="org.scalastyle.scalariform.ClassTypeParameterChecker" level="warning">
......
......@@ -6,6 +6,7 @@ package daisy
import scala.collection.immutable.Seq
import scala.reflect.ClassTag
import lang.Trees.Expr
import lang.Identifiers._
import tools.{Interval, PartialInterval, Rational}
......@@ -32,7 +33,12 @@ case class Context(
// the analysed/computed roundoff errors for each function
resultAbsoluteErrors: Map[Identifier, Rational] = Map(),
resultRealRanges: Map[Identifier, Interval] = Map()
resultRealRanges: Map[Identifier, Interval] = Map(),
// intermediate ranges and errors, which are needed e.g. for fixed-point codegen
intermediateAbsErrors: Map[Identifier, Map[Expr, Rational]] = Map(),
// real-valued ranges
intermediateRanges: Map[Identifier, Map[Expr, Interval]] = Map()
) {
// on the first creation of a context, we also update the context variable
......
......@@ -3,12 +3,13 @@
package daisy
package analysis
import lang.NumAnnotation
import lang.Trees._
import lang.TreeOps.allVariablesOf
import lang.Identifiers._
import tools._
import FinitePrecision._
import Rational._
import lang.Identifiers._
/**
??? Description goes here
......@@ -23,8 +24,8 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
override val description = "Computes ranges and absolute errors"
val optionPrecision = ChoiceOptionDef("precision", "Type of precision to use",
Set("Float32", "Float64", "DoubleDouble", "QuadDouble",
"Fixed16", "Fixed32"), "Float64")
Set("Float32", "Float64", "DoubleDouble", "QuadDouble",
"Fixed16", "Fixed32"), "Float64")
override val definedOptions: Set[CmdLineOptionDef[Any]] = Set(
ChoiceOptionDef("rangeMethod", "Method to use for range analysis",
......@@ -88,7 +89,8 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
val fncsToConsider: Seq[String] = functionsToConsider(ctx, prg)
val res: Map[Identifier, (Rational, Interval)] = prg.defs.filter(fnc =>
// returns (abs error, result range, interm. errors, interm. ranges)
val res: Map[Identifier, (Rational, Interval, Map[Expr, Rational], Map[Expr, Interval])] = prg.defs.filter(fnc =>
!fnc.precondition.isEmpty &&
!fnc.body.isEmpty &&
fncsToConsider.contains(fnc.id.toString)).map(fnc => {
......@@ -100,67 +102,129 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
// 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){
if (trackInitialErrs && trackRoundoffErrs) {
val inputErrs = ctx.specInputErrors(fnc.id)
val allIDs = fnc.params.map(_.id).toSet
val missingIDs = allIDs -- inputErrs.keySet
inputErrs ++ missingIDs.map( id => (id -> uniformPrecision.absRoundoff(inputValMap(id))))
inputErrs ++ missingIDs.map(id => (id -> uniformPrecision.absRoundoff(inputValMap(id))))
} else if(trackInitialErrs) {
} else if (trackInitialErrs) {
val inputErrs = ctx.specInputErrors(fnc.id)
val allIDs = fnc.params.map(_.id).toSet
val missingIDs = allIDs -- inputErrs.keySet
inputErrs ++ missingIDs.map( id => (id -> zero))
inputErrs ++ missingIDs.map(id => (id -> zero))
} else if (trackRoundoffErrs) {
val allIDs = fnc.params.map(_.id)
allIDs.map( id => (id -> uniformPrecision.absRoundoff(inputValMap(id)))).toMap
allIDs.map(id => (id -> uniformPrecision.absRoundoff(inputValMap(id)))).toMap
} else {
val allIDs = fnc.params.map(_.id)
allIDs.map( id => (id -> zero)).toMap
allIDs.map(id => (id -> zero)).toMap
}
// TODO: Interval-only based error estimation; should be a very quick fix
val fncBody = fnc.body.get
val (resError: Rational, resRange: Interval) = (rangeMethod, errorMethod) match {
// val (resError: Rational, resRange: Interval) =
// returns (abs error, result range, interm. errors, interm. ranges)
(rangeMethod, errorMethod) match {
case ("interval", "affine") =>
uniformRoundoff_IA_AA(fnc.body.get, inputValMap, inputErrorMap, uniformPrecision, trackRoundoffErrs)
val (resRange, intermediateRanges) = evalRange[Interval](fncBody, inputValMap, Interval.apply)
val (resRoundoff, allErrors) = evalRoundoff[AffineForm](fncBody, intermediateRanges,
allVariablesOf(fncBody).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,
trackRoundoffErrs)
val resError = Interval.maxAbs(resRoundoff.toInterval)
(fnc.id -> ((resError, resRange,
allErrors.map({
case (e, aa) => (e -> Interval.maxAbs(aa.toInterval))
}),
intermediateRanges)))
case ("affine", "affine") =>
uniformRoundoff_AA_AA(fnc.body.get, inputValMap, inputErrorMap, uniformPrecision, trackRoundoffErrs)
val (resRange, intermediateRanges) = evalRange[AffineForm](fncBody,
inputValMap.map(x => (x._1 -> AffineForm(x._2))), AffineForm.apply)
val (resRoundoff, allErrors) = evalRoundoff[AffineForm](fncBody,
intermediateRanges.map(x => (x._1 -> x._2.toInterval)),
allVariablesOf(fncBody).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,
trackRoundoffErrs)
val resError = Interval.maxAbs(resRoundoff.toInterval)
(fnc.id -> ((resError, resRange.toInterval,
allErrors.map({
case (e, aa) => (e -> Interval.maxAbs(aa.toInterval))
}),
intermediateRanges.mapValues(_.toInterval))))
case ("smt", "affine") =>
uniformRoundoff_SMT_AA(fnc.body.get, inputValMap, inputErrorMap, uniformPrecision, trackRoundoffErrs)
// default is to use the method that attaches the info to trees.
case ("subdiv", _) =>
val tmp = doIntervalSubdivision( //evaluateSubdiv(
fnc.body.get, lang.TreeOps.freeVariablesOf(fnc.body.get),
inputValMap,
inputErrorMap,
trackRoundoffErrs,
uniformPrecision)
(tmp._2, tmp._1)
val (resRange, intermediateRanges) = evalRange[SMTRange](fncBody,
inputValMap.map({ case (id, int) => (id -> SMTRange(Variable(id), int)) }),
SMTRange.apply)
val (resRoundoff, allErrors) = evalRoundoff[AffineForm](fncBody,
intermediateRanges.map(x => (x._1 -> x._2.toInterval)),
allVariablesOf(fncBody).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,
trackRoundoffErrs)
val resError = Interval.maxAbs(resRoundoff.toInterval)
(fnc.id -> ((resError, resRange.toInterval,
allErrors.map({
case (e, aa) => (e -> Interval.maxAbs(aa.toInterval))
}),
intermediateRanges.mapValues(_.toInterval))))
// TODO: interval subdivision; compare with what Anastasiia did
// case ("subdiv", _) =>
// val tmp = doIntervalSubdivision( //evaluateSubdiv(
// fnc.body.get, lang.TreeOps.freeVariablesOf(fnc.body.get),
// inputValMap,
// inputErrorMap,
// trackRoundoffErrs,
// uniformPrecision)
// (tmp._2, tmp._1)
// (fnc.id -> (resError, resRange))
case _ =>
reporter.fatalError(s"Your combination of $rangeMethod and $errorMethod" +
"for computing ranges and errors is not supported.")
null
}
(fnc.id -> (resError, resRange))
}).toMap
timer.stop
//ctx.reporter.info(s"Finished $name")
(ctx.copy(resultAbsoluteErrors = res.map(x => (x._1 -> x._2._1)),
resultRealRanges = res.map(x => (x._1 -> x._2._2))), prg)
// ctx.reporter.info(s"Finished $name")
(ctx.copy(resultAbsoluteErrors = res.mapValues(_._1),
resultRealRanges = res.mapValues(_._2),
intermediateAbsErrors = res.mapValues(_._3),
intermediateRanges = res.mapValues(_._4)), prg)
}
......
......@@ -25,7 +25,7 @@ import lang.Trees.Program
Prerequisite:
None
*/
*/
object SpecsProcessingPhase extends DaisyPhase {
override val name = "Specs processing"
......@@ -36,17 +36,17 @@ object SpecsProcessingPhase extends DaisyPhase {
var reporter: Reporter = null
def run(ctx:Context, prg: Program): (Context, Program) = {
def run(ctx: Context, prg: Program): (Context, Program) = {
reporter = ctx.reporter
//reporter.info("\nStarting specs preprocessing phase")
// reporter.info("\nStarting specs preprocessing phase")
val timer = ctx.timers.preprocess.start
var allRanges: Map[Identifier, Map[Identifier, Interval]] = Map()
var allErrors: Map[Identifier, Map[Identifier, Rational]] = Map()
var resRanges: Map[Identifier, PartialInterval] = Map()
var resErrors: Map[Identifier, Rational] = Map()
//var requiredOutputRanges: Map[Identifier, Map[Identifier, PartialInterval]] = Map()
//var requiredOutputErrors: Map[Identifier, Map[Identifier, Rational]] = Map()
// var requiredOutputRanges: Map[Identifier, Map[Identifier, PartialInterval]] = Map()
// var requiredOutputErrors: Map[Identifier, Map[Identifier, Rational]] = Map()
for (fnc <- prg.defs) {
......@@ -55,7 +55,7 @@ object SpecsProcessingPhase extends DaisyPhase {
// TODO: additional constraints
val (ranges, errors) = extractPreCondition(pre)
allRanges += (fnc.id -> ranges.map( x => (x._1 -> Interval(x._2._1, x._2._2) )))
allRanges += (fnc.id -> ranges.map(x => (x._1 -> Interval(x._2._1, x._2._2))))
allErrors += (fnc.id -> errors)
// annotate the variables in the function body directly
......@@ -100,23 +100,22 @@ object SpecsProcessingPhase extends DaisyPhase {
reporter.error("Tuples are not supported.")
}
//requiredOutputRanges += (fnc.id -> ranges.map( x =>
// requiredOutputRanges += (fnc.id -> ranges.map( x =>
// (x._1 -> PartialInterval(x._2._1, x._2._2) )))
//requiredOutputErrors += (fnc.id -> errors)
// requiredOutputErrors += (fnc.id -> errors)
case _ =>
//reporter.info("No post-condition found\n")
// reporter.info("No post-condition found\n")
}
}
timer.stop
//reporter.info("Finished specs preprocessing phase\n")
// reporter.info("Finished specs preprocessing phase\n")
reporter.debug(lang.RangePrinter(prg))
reporter.debug("range bounds: " + resRanges.mkString("\n"))
reporter.debug("error bounds: " + resErrors.mkString("\n"))
......@@ -128,7 +127,7 @@ object SpecsProcessingPhase extends DaisyPhase {
def extractPreCondition(expr: Expr): (Map[Identifier, (Rational, Rational)],
Map[Identifier, Rational]) = {
Map[Identifier, Rational]) = {
val (lowerBound, upperBound, absError) = extractCondition(expr)
......@@ -139,7 +138,7 @@ object SpecsProcessingPhase extends DaisyPhase {
}
def extractPostCondition(expr: Expr): (Map[Identifier, (Option[Rational], Option[Rational])],
Map[Identifier, Rational]) = {
Map[Identifier, Rational]) = {
val (lowerBound, upperBound, absError) = extractCondition(expr)
......@@ -157,8 +156,7 @@ object SpecsProcessingPhase extends DaisyPhase {
}
def extractCondition(e: Expr): (Map[Identifier, Rational],
Map[Identifier, Rational],
Map[Identifier, Rational]) = {
Map[Identifier, Rational], Map[Identifier, Rational]) = {
var lowerBound: Map[Identifier, Rational] = Map.empty
var upperBound: Map[Identifier, Rational] = Map.empty
......@@ -182,7 +180,7 @@ object SpecsProcessingPhase extends DaisyPhase {
case GreaterEquals(RealLiteral(r), Variable(id)) => upperBound += (id -> r)
case _ => ;
//reporter.warning(s"Unexpected expression in spec: $e.")
// reporter.warning(s"Unexpected expression in spec: $e.")
}
extract(e)
......
......@@ -10,7 +10,6 @@ import java.text.SimpleDateFormat
import java.util.Date
import lang.Trees.{Program, Let, Expr}
import lang.NumAnnotation
import tools.Rational
import Rational._
......
// Copyright 2017 MPI-SWS, Saarbruecken, Germany
package daisy
package lang
import tools.{Interval, Rational}
/**
This trait has a number of write-once fields which are to be populated
by certain analyses.
The idea is that this is easily extensible,
not openly mutable for sanity's sake,
and does not necessitate duplicating the AST trees.
This is a trait and not an abstract class, because we have a lot of methods
Expr => Expr, which cannot distinguish between 'NumExpr' and 'Expr'.
Hence, the annotation has to be non-intrusive.
*/
trait NumAnnotation {
private var _interval: Option[Interval] = None
private var _absError: Option[Rational] = None
// PERF: @inline?
def interval_=(i: Interval): Unit = {
if (_interval.isEmpty) {
_interval = Some(i)
} else {
throw new WriteTwiceException("Trying to write to 'interval', " +
"but it's already defined.")
}
}
def interval: Interval = _interval.get
def hasInterval: Boolean = !_interval.isEmpty
def absError_=(e: Rational): Unit = {
require(e >= Rational.zero)
if (_absError.isEmpty) {
_absError = Some(e)
} else {
throw new WriteTwiceException("Trying to write to 'absError', " +
"but it's already defined.")
}
}
def absError: Rational = _absError.get
def hasError: Boolean = !_absError.isEmpty
}
// Copyright 2017 MPI-SWS, Saarbruecken, Germany
package daisy
package lang
import Trees._
object RangePrinter {
def apply(t: Tree): String = {
val printer = new RangePrinter
printer.pp(t, None)(0)
printer.toString
}
}
class RangePrinter extends PrettyPrinter {
override def pp(tree: Tree, parent: Option[Tree])(implicit lvl: Int): Unit = {
implicit val p = Some(tree)
def appendInterval(x: NumAnnotation): Unit = {
if (x.hasInterval && x.hasError) {
sb.append(s"#${x.interval},${x.absError}#")
} else if (x.hasInterval) {
sb.append(s"#${x.interval}#")
} else {
sb.append("##")
}
}
tree match {
case x @ Variable(id) =>
pp(id, p)
appendInterval(x)
case x @ Plus(l,r) =>
ppBinary(l, r, " + ")
appendInterval(x)
case x @ Minus(l,r) =>
ppBinary(l, r, " - ")
appendInterval(x)
case x @ Times(l,r) =>
ppBinary(l, r, " * ")
appendInterval(x)
case x @ Division(l,r) =>
ppBinary(l, r, " / ")
appendInterval(x)
case _ => super.pp(tree, parent)
}
}
}
\ No newline at end of file
......@@ -172,7 +172,7 @@ object Trees {
/** Variable
* @param id The identifier of this variable
*/
case class Variable(id: Identifier) extends Expr with Terminal with NumAnnotation {
case class Variable(id: Identifier) extends Expr with Terminal {
val getType = id.getType
def deepCopy = Variable(id)
}
......@@ -184,7 +184,7 @@ object Trees {
* @param body The expression following the ``val ... = ... ;`` construct
* @see [[purescala.Constructors#let purescala's constructor let]]
*/
case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr with NumAnnotation {
case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr {
val getType = {
// We can't demand anything sticter here, because some binders are
// typed context-wise
......@@ -267,7 +267,7 @@ object Trees {
}
// the string is exactly what the user wrote
case class RealLiteral(value: Rational) extends Literal[Rational] with NumAnnotation {
case class RealLiteral(value: Rational) extends Literal[Rational] {
val getType = RealType
private var _stringValue: String = null
......@@ -286,7 +286,7 @@ object Trees {
}
}
case class FinitePrecisionLiteral(value: Rational, prec: Precision) extends Literal[Rational] with NumAnnotation {
case class FinitePrecisionLiteral(value: Rational, prec: Precision) extends Literal[Rational] {
val getType = FinitePrecisionType(prec)
private var _stringValue: String = null
......@@ -388,36 +388,36 @@ object Trees {
/* Arithmetic */
/** $encodingof `... + ...` */
case class Plus(lhs: Expr, rhs: Expr) extends Expr with NumAnnotation {
case class Plus(lhs: Expr, rhs: Expr) extends Expr {
val getType = lhs.getType
def deepCopy = Plus(lhs.deepCopy, rhs.deepCopy)
}
/** $encodingof `... - ...` */
case class Minus(lhs: Expr, rhs: Expr) extends Expr with NumAnnotation {
case class Minus(lhs: Expr, rhs: Expr) extends Expr {
val getType = lhs.getType
def deepCopy = Minus(lhs.deepCopy, rhs.deepCopy)
}
/** $encodingof `- ... for BigInts`*/
case class UMinus(expr: Expr) extends Expr with NumAnnotation {
case class UMinus(expr: Expr) extends Expr {
val getType = expr.getType
def deepCopy = UMinus(expr.deepCopy)
}
/** $encodingof `... * ...` */
case class Times(lhs: Expr, rhs: Expr) extends Expr with NumAnnotation {
case class Times(lhs: Expr, rhs: Expr) extends Expr {
val getType = lhs.getType
def deepCopy = Times(lhs.deepCopy, rhs.deepCopy)
}
/** $encodingof `... / ...` */
case class Division(lhs: Expr, rhs: Expr) extends Expr with NumAnnotation {
case class Division(lhs: Expr, rhs: Expr) extends Expr {
val getType = lhs.getType
def deepCopy = Division(lhs.deepCopy, rhs.deepCopy)
}
case class Pow(lhs: Expr, rhs: Expr) extends Expr with NumAnnotation {
case class Pow(lhs: Expr, rhs: Expr) extends Expr {
assert(lhs.getType == rhs.getType)
val getType = {
if (lhs.getType == RealType) RealType
......@@ -427,39 +427,38 @@ object Trees {
def deepCopy = Pow(lhs.deepCopy, rhs.deepCopy)
}
case class Sqrt(t: Expr) extends Expr with NumAnnotation {
case class Sqrt(t: Expr) extends Expr {
require(t.getType == RealType)
assert(t.isInstanceOf[NumAnnotation])
// TODO: this operation may not be available for Float32
val getType = t.getType
def deepCopy = Sqrt(t.deepCopy)
}
case class Sin(t: Expr) extends Expr with NumAnnotation {
case class Sin(t: Expr) extends Expr {
require(t.getType == RealType)
val getType = RealType
def deepCopy = Sin(t.deepCopy)
}
case class Cos(t: Expr) extends Expr with NumAnnotation {
case class Cos(t: Expr) extends Expr {
require(t.getType == RealType)
val getType = RealType
def deepCopy = Cos(t.deepCopy)
}
case class Tan(t: Expr) extends Expr with NumAnnotation {
case class Tan(t: Expr) extends Expr {
require(t.getType == RealType)
val getType = RealType
def deepCopy = Tan(t.deepCopy)
}
case class Exp(t: Expr) extends Expr with NumAnnotation {
case class Exp(t: Expr) extends Expr {
require(t.getType == RealType)
val getType = RealType
def deepCopy = Exp(t.deepCopy)
}
case class Log(t: Expr) extends Expr with NumAnnotation {
case class Log(t: Expr) extends Expr {
require(t.getType == RealType)
val getType = RealType
def deepCopy = Log(t.deepCopy)
......
......@@ -7,7 +7,7 @@ import analysis._
import analysis.DynamicPhase._
import lang.Trees._
import lang.Identifiers._
import lang.NumAnnotation
//import lang.NumAnnotation
import Interval._
import Rational._
import FinitePrecision._
......
......@@ -11,17 +11,11 @@ import lang.Identifiers._
// used by a regression test
object Evaluators {
def evalAffine(expr: Expr, _valMap: Map[Identifier, AffineForm] = Map.empty): AffineForm = {
var valMap: Map[Identifier, AffineForm] = _valMap
def eval(e: Expr): AffineForm = e match {
// TODO should this ignore annotations?
case x @ Variable(id) if x.hasInterval =>
AffineForm(x.interval)
case Variable(id) => valMap(id)
case RealLiteral(r) => AffineForm(r)
case Plus(x, y) => eval(x) + eval(y)
......@@ -44,10 +38,6 @@ object Evaluators {
var valMap: Map[Identifier, Interval] = _valMap
def eval(e: Expr): Interval = e match {
case x @ Variable(id) if x.hasInterval =>
x.interval
case Variable(id) => valMap(id)
case RealLiteral(r) => Interval(r)
case Plus(x, y) => eval(x) + eval(y)
......@@ -71,10 +61,6 @@ object Evaluators {
var valMap: Map[Identifier, SMTRange] = _valMap
def eval(e: Expr): SMTRange = e match {
case x @ Variable(id) if x.hasInterval =>
SMTRange(x, x.interval)
case Variable(id) => valMap(id)
case RealLiteral(r) => SMTRange(r)
case Plus(x, y) => eval(x) + eval(y)
......
......@@ -7,7 +7,7 @@ import analysis._
import analysis.DynamicPhase._
import lang.Trees._
import lang.Identifiers._
import lang.NumAnnotation
//import lang.NumAnnotation
import Interval._
import Rational._
import FinitePrecision._
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment