Commit eb1e95b5 authored by Eva Darulova's avatar Eva Darulova

adding rewriting optimization

parent b6798c3e
#!/bin/bash --posix
#
# This script
# 'Standard' benchmark set
declare -a files=("testcases/rosa/Bsplines.scala" \
# "testcases/rosa/Doppler.scala" \ // needs to be inlined
"testcases/real2float/Himmilbeau.scala" \
"testcases/control/InvertedPendulum.scala" \
"testcases/real2float/Kepler.scala" \
"testcases/rosa/RigidBody.scala" \
"testcases/trigApprox/Sine.scala" \
"testcases/trigApprox/Sqrt.scala" \
"testcases/control/Traincar4.scala" \
"testcases/rosa/Turbine.scala")
# Make sure the code is compiled
sbt compile
# generate daisy script
if [ ! -e daisy ]
then
sbt script
fi
# Run daisy on each testfile
for file in "${files[@]}"
do
./daisy --rewrite --analysis=dataflow ${file}
done
\ No newline at end of file
......@@ -43,6 +43,7 @@ object Main {
// FlagOptionDef("taylor", "Run experimental taylor simplification phase"),
// FlagOptionDef("absSubdiv", "Run experimental relative through absolute error phase"),
// ParamOptionDef("timeout", "Timeout in ms.", "1000"),
FlagOptionDef("rewrite", "Rewrite expression to improve accuracy ."),
optionAnalysis,
optionFunctions,
optionPrintToughSMTCalls,
......@@ -63,6 +64,7 @@ object Main {
backend.CodeGenerationPhase,
transform.SSATransformerPhase,
analysis.DynamicPhase,
opt.RewritingOptimizationPhase,
backend.InfoPhase)
def main(args: Array[String]): Unit = {
......@@ -197,7 +199,11 @@ object Main {
private def computePipeline(ctx: Context): Pipeline[Program, Program] = {
val ssaNeeded = ctx.fixedPoint && ctx.hasFlag("codegen")
val beginning = analysis.SpecsProcessingPhase
val beginning = if (ctx.hasFlag("rewrite")) {
analysis.SpecsProcessingPhase andThen opt.RewritingOptimizationPhase
} else {
analysis.SpecsProcessingPhase
}
if (ctx.hasFlag("dynamic")) {
......@@ -239,37 +245,5 @@ object Main {
}
// this is not ideal, using 'magic' strings
// if (ctx.hasFlag("dynamic")) {
// analysis.SpecsProcessingPhase andThen
// analysis.DynamicPhase
// } else if (ctx.hasFlag("codegen") && fixedPointArith) {
// analysis.SpecsProcessingPhase andThen
// transform.SSATransformerPhase andThen
// analysis.RangeErrorPhase andThen
// backend.InfoPhase andThen
// backend.CodeGenerationPhase
// } else if (ctx.hasFlag("codegen")) {
// analysis.SpecsProcessingPhase andThen
// analysis.RangeErrorPhase andThen
// backend.InfoPhase andThen
// backend.CodeGenerationPhase
// } else if (ctx.hasFlag("relative")) {
// analysis.SpecsProcessingPhase andThen
// analysis.RelativeErrorPhase
// } else if (ctx.hasFlag("taylor")) {
// analysis.SpecsProcessingPhase andThen
// analysis.TaylorErrorPhase andThen
// backend.InfoPhase
// } else if (ctx.hasFlag("absSubdiv")) {
// analysis.SpecsProcessingPhase andThen
// analysis.RelThroughAbsPhase andThen
// backend.InfoPhase
// } else {
// analysis.SpecsProcessingPhase andThen
// analysis.RangeErrorPhase andThen
// backend.InfoPhase
// }
}
}
This diff is collapsed.
// Copyright 2017 MPI-SWS, Saarbruecken, Germany
package daisy
package opt
import scala.collection.immutable.Seq
import java.io.FileWriter
import java.io.BufferedWriter
import util.Random
import lang.Trees.{Program, Expr, Terminal}
import search.GeneticSearch
import tools._
import lang.Identifiers._
import FinitePrecision._
import lang.TreeOps._
/**
Optimizes the order of expressions.
Prerequisites:
- SpecsProcessingPhase
*/
object RewritingOptimizationPhase extends DaisyPhase with GeneticSearch[Expr] with RewritingOps with
RoundoffEvaluatorsApprox with DynamicEvaluators {
override val name = "rewriting-optimization phase"
override val description = "optimization by rewriting"
override val definedOptions: Set[CmdLineOptionDef[Any]] = Set(
ParamOptionDef("rewrite-generations", "Number of generations to search for",
maxGenerations.toString),
ParamOptionDef("rewrite-population-size", "Size of the population for genetic search",
populationSize.toString),
// ChoiceOptionDef("rewrite-fitness-fnc", "Fitness function to be used during search",
// Set("interval-affine", "affine-affine", "smt-affine", "dynamic-256"), "interval-affine"),
FlagOptionDef("rewrite-baseline", "Compute baseline errors dynamically (expensive!)"),
// this could be just one option: rewrite-seed and allow the option 'systemmillis'
FlagOptionDef("rewrite-seed-system-millis", "Use the system time for random seed"),
ParamOptionDef("rewrite-custom-seed", "Use the given seed" ,"4781")
)
implicit val debugSection = DebugSectionOptimization
override var reporter: Reporter = null
var seed: Long = 4781l //System.currentTimeMillis //1469010147126l
var rand: Random = null
var computeBaseline: Boolean = false
val baselineDynamicSamples = 100000
// ridiculously high value to signify that an expression is VERY bad,
// e.g. due to division by zero
val fitnessOnFail = Rational(1000)
val uniformPrecision = Float64
val activeRules = commRules ++ assocRules ++ distRules ++ idReduceRules ++
fracTransRules ++ fracDistRules
override def run(ctx: Context, prg: Program): (Context, Program) = {
reporter = ctx.reporter
reporter.info(s"\nStarting $name")
val timer = ctx.timers.rewriting.start
var fitnessFunction: (Expr, Map[Identifier, Interval], Map[Identifier, Rational]) => Rational =
uniformRoundoffApprox_IA_AA(_, _, _, uniformPrecision)._1
var fitnessFunctionName = "interval-affine"
// var logFile: BufferedWriter = null
/* Process relevant options */
for (opt <- ctx.options) opt match {
case ParamOption("rewrite-generations", value) =>
maxGenerations = value.toInt
case ParamOption("rewrite-population-size", value) =>
populationSize = value.toInt
// case ChoiceOption("rewrite-fitness-fnc", value) =>
// fitnessFunction = value match {
// case "interval-affine" => uniformRoundoff_IA_AA(_, _, _, uniformPrecision)._1
// case "affine-affine" => uniformRoundoff_AA_AA(_, _, _, uniformPrecision)._1
// case "smt-affine" => uniformRoundoff_SMT_AA(_, _, _, uniformPrecision)._1
// // this does not conform to the interface of the static analyses,
// // so we need to do an outer anonymous function
// case "dynamic-256" =>
// (e: Expr, in: Map[Identifier, Interval], err: Map[Identifier, Rational]) =>
// errorDynamicWithInputRoundoff(e, in, 256)
// }
// fitnessFunctionName = value
case FlagOption("rewrite-baseline") =>
computeBaseline = true
case FlagOption("rewrite-seed-system-millis") =>
seed = System.currentTimeMillis
case ParamOption("rewrite-custom-seed", value) =>
seed = value.toLong
case _ => ;
}
val infoString = s"fitness function: $fitnessFunctionName, # generations: $maxGenerations, " +
s"population size: $populationSize, seed: $seed"
reporter.info(infoString)
val newDefs = for (fnc <- prg.defs) yield
if (!fnc.precondition.isEmpty && !fnc.body.isEmpty) {
reporter.info(s"\nGoing to rewrite ${fnc.id}")
val allIDs = fnc.params.map(_.id)
val inputValMap: Map[Identifier, Interval] = ctx.specInputRanges(fnc.id)
var inputErrors = allIDs.map {
id => (id -> uniformPrecision.absRoundoff(inputValMap(id)))
}.toMap
val newBody = rewriteExpression(fnc.body.get, fitnessFunction, inputValMap, inputErrors)
reporter.info("error after: " + fitnessFunction(newBody, inputValMap, inputErrors))
reporter.debug("expr after: " + newBody)
if(computeBaseline) {
val dynamicErrorBefore = errorDynamicWithInputRoundoff(fnc.body.get, inputValMap, baselineDynamicSamples)
val dynamicErrorAfter = errorDynamicWithInputRoundoff(newBody, inputValMap, baselineDynamicSamples)
reporter.info(s"dynamic error before: $dynamicErrorBefore, after: $dynamicErrorAfter")
val improvement = (dynamicErrorBefore - dynamicErrorAfter) / dynamicErrorBefore
reporter.info(s"improvement: $improvement")
}
fnc.copy(body = Some(newBody))
} else {
fnc
}
timer.stop
ctx.reporter.info(s"Finished $name")
(ctx, Program(prg.id, newDefs.toSeq))
}
// refactor as we need to call this several times
def rewriteExpression(initExpr: Expr,
roundoffFunction: (Expr, Map[Identifier, Interval], Map[Identifier, Rational]) => Rational,
inputValMap: Map[Identifier, Interval],
inputErrors: Map[Identifier, Rational]): Expr = {
val fitnessBefore = roundoffFunction(initExpr, inputValMap, inputErrors)
reporter.info(s"error before: $fitnessBefore")
reporter.debug("expr before: " + initExpr)
var bestErrorExpr = initExpr
var bestError = fitnessBefore
rand = new Random(seed) //reset generator to obtain deterministic search
// we assign a very high fitness to signal that something is wrong
// the offending expression should be filtered out "naturally"
val (bestExprFound, _) = runGenetic(initExpr,
(e: Expr) => e.deepCopy,
(e: Expr) => {
try {
val fitness = roundoffFunction(e, inputValMap, inputErrors)
//saves the expression with smallest error, which does not increase the initial cost
if (fitness < bestError) {
bestErrorExpr = e
bestError = fitness
}
fitness
} catch {
case e: daisy.tools.DivisionByZeroException =>
fitnessOnFail
}
})
bestExprFound
}
def mutate(expr: Expr) = _mutate(expr, rand.nextInt(sizeWithoutTerminals(expr)), activeRules)
}
......@@ -70,6 +70,7 @@ object FinitePrecision {
/* The range of values that are representable by this precision. */
def range: (Rational, Rational)
val isFloatingPoint: Boolean
/* The smallest (absolute) value representable by this precision,
for floating-point precisions, it's the smallest normal (and not denormal) */
//def minNormal: Rational
......@@ -81,6 +82,14 @@ object FinitePrecision {
def absRoundoff(i: Interval): Rational = {
absRoundoff(max(abs(i.xlo), abs(i.xhi)))
}
def absRoundoffApprox(r: Rational): Rational
def absRoundoffApprox(i: Interval): Rational = {
absRoundoffApprox(max(abs(i.xlo), abs(i.xhi)))
}
}
case object Float32 extends Precision {
......@@ -88,6 +97,9 @@ object FinitePrecision {
val rationalMaxValue = double2Fraction(Float.MaxValue)
(-Rational(rationalMaxValue._1, rationalMaxValue._2), Rational(rationalMaxValue._1, rationalMaxValue._2))
}
val isFloatingPoint = true
val minNormal: Rational = {
val rationalMinNormal = double2Fraction(java.lang.Float.MIN_NORMAL)
Rational(rationalMinNormal._1, rationalMinNormal._2)
......@@ -96,6 +108,8 @@ object FinitePrecision {
// PERFORMANCE: this may not be the fastest way
Rational.fromDouble(math.ulp(Rational.abs(r).floatValue)/2)
}
// TODO: nothing approx. here
def absRoundoffApprox(r: Rational): Rational = absRoundoff(r)
val machineEpsilon: Rational =
Rational(new BigInt(new BigInteger("1")), new BigInt(new BigInteger("2")).pow(24))
......@@ -116,6 +130,8 @@ object FinitePrecision {
(-Rational(rationalMaxValue._1, rationalMaxValue._2), Rational(rationalMaxValue._1, rationalMaxValue._2))
}
val isFloatingPoint = true
val minNormal: Rational = {
val rationalMinNormal = double2Fraction(java.lang.Double.MIN_NORMAL)
Rational(rationalMinNormal._1, rationalMinNormal._2)
......@@ -124,6 +140,8 @@ object FinitePrecision {
def absRoundoff(r: Rational): Rational = {
Rational.fromDouble(math.ulp(Rational.abs(r).doubleValue)/2)
}
def absRoundoffApprox(r: Rational): Rational = absRoundoff(r)
// TODO: machine epsilon representation will be huge?! Can we approximate it, without much loss of accuracy? It is worth it?
val machineEpsilon: Rational =
......@@ -146,6 +164,9 @@ object FinitePrecision {
val rationalMaxValue = double2Fraction(Double.MaxValue)
(-Rational(rationalMaxValue._1, rationalMaxValue._2), Rational(rationalMaxValue._1, rationalMaxValue._2))
}
val isFloatingPoint = true
val minNormal: Rational = {
val rationalMinNormal = double2Fraction(math.pow(2, -969))
Rational(rationalMinNormal._1, rationalMinNormal._2)
......@@ -156,6 +177,16 @@ object FinitePrecision {
doubleDoubleEps * Rational.abs(r)
}
def absRoundoffApprox(r: Rational): Rational = {
var rndoff = doubleDoubleEps * Rational.abs(r) // do this in Double already?
if (rndoff.n.bitLength > 100) { // won't this always hold?
//rndoff = Rational.fromString(rndoff.toString) // too slow
rndoff = Rational.fromDouble(rndoff.doubleValue)
}
rndoff
}
def compare(that: Precision): Int = (that: @unchecked) match {
case Float32 => 1
case Float64 => 1
......@@ -170,6 +201,9 @@ object FinitePrecision {
val rationalMaxValue = double2Fraction(Double.MaxValue)
(-Rational(rationalMaxValue._1, rationalMaxValue._2), Rational(rationalMaxValue._1, rationalMaxValue._2))
}
val isFloatingPoint = true
val minNormal: Rational = {
val rationalMinNormal = double2Fraction(math.pow(2, -863))
Rational(rationalMinNormal._1, rationalMinNormal._2)
......@@ -179,6 +213,10 @@ object FinitePrecision {
def absRoundoff(r: Rational): Rational = {
quadDoubleEps * Rational.abs(r)
}
// TODO: nothing approx. here
def absRoundoffApprox(r: Rational): Rational = absRoundoff(r)
def compare(that: Precision): Int = ???
}
......@@ -192,12 +230,15 @@ object FinitePrecision {
(Rational(-math.pow(2, bitlength - 1).toLong, 1l),
Rational(math.pow(2, bitlength - 1).toLong - 1, 1l))
val isFloatingPoint = false
//val minNormal: Rational = ???
def absRoundoff(r: Rational): Rational = {
val fracBits = fractionalBits(r)
Rational(1, math.pow(2, fracBits).toLong)
}
def absRoundoffApprox(r: Rational): Rational = absRoundoff(r)
def fractionalBits(i: Interval): Int = {
fractionalBits(max(abs(i.xlo), abs(i.xhi)))
......
// Copyright 2017 MPI-SWS, Saarbruecken, Germany
package daisy
package tools
import scala.collection.immutable.Seq
import lang.Trees._
import lang.Identifiers._
import lang.TreeOps.allVariablesOf
import FinitePrecision._
import Rational.{min, abs, sqrtDown, one}
trait RoundoffEvaluatorsApprox extends RangeEvaluators {
/**
* 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)
*/
def uniformRoundoffApprox_IA_AA(
expr: Expr,
inputValMap: Map[Identifier, Interval],
inputErrorMap: Map[Identifier, Rational],
uniformPrecision: Precision,
trackRoundoffErrors: Boolean = true): (Rational, Interval) = {
val (resRange, intermediateRanges) = evalRange[Interval](expr, inputValMap, Interval.apply)
val (resRoundoff, _, allErrors) = evalRoundoff[AffineForm](expr, intermediateRanges,
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)
(Interval.maxAbs(resRoundoff.toInterval), resRange)
}
/**
* 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
*/
def uniformRoundoffApprox_AA_AA(
expr: Expr,
inputValMap: Map[Identifier, Interval],
inputErrorMap: Map[Identifier, Rational],
uniformPrecision: Precision,
trackRoundoffErrors: Boolean = true): (Rational, Interval) = {
val (resRange, intermediateRanges) = evalRange[AffineForm](expr,
inputValMap.map(x => (x._1 -> AffineForm(x._2))), AffineForm.apply)
val (resRoundoff, _, allErrors) = evalRoundoff[AffineForm](expr,
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)
(Interval.maxAbs(resRoundoff.toInterval), resRange.toInterval)
}
/**
* 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
*/
def uniformRoundoffApprox_SMT_AA(
expr: Expr,
inputValMap: Map[Identifier, Interval],
inputErrorMap: Map[Identifier, Rational],
uniformPrecision: Precision,
trackRoundoffErrors: Boolean = true): (Rational, Interval) = {
val (resRange, intermediateRanges) = evalRange[SMTRange](expr,
inputValMap.map({ case (id, int) => (id -> SMTRange(Variable(id), int)) }),
SMTRange.apply)
val (resRoundoff, _, allErrors) = evalRoundoff[AffineForm](expr,
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)
(Interval.maxAbs(resRoundoff.toInterval), resRange.toInterval)
}
/**
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.
*/
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,
trackRoundoffErrors: Boolean // if false, propagate only initial errors
): (T, Precision, Map[Expr, T]) = {
var intermediateErrors: Map[Expr, T] = Map.empty
// TODO: check the effectiveness of this
@inline
def computeNewError(range: Interval, propagatedError: T, prec: Precision): T =
if (trackRoundoffErrors) {
val actualRange: Interval = range + propagatedError.toInterval
// this roundoff is not guaranteed to be sound
val rndoff = prec.absRoundoffApprox(actualRange)
propagatedError +/- rndoff
} else {
propagatedError
}
def eval(e: Expr, errorMap: Map[Identifier, T]): (T, Precision) = (e: @unchecked) match {
case x @ RealLiteral(r) =>
val rndoff = if (isExactInFloats(r, constantsPrecision) || !trackRoundoffErrors) {
zeroError
} else {
fromError(constantsPrecision.absRoundoff(r))
}
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)
val (rndoffLhs, precLhs) = eval(lhs, errorMap)
val (rndoffRhs, precRhs) = eval(rhs, errorMap)
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)
val (rndoffLhs, precLhs) = eval(lhs, errorMap)
val (rndoffRhs, precRhs) = eval(rhs, errorMap)
val propagatedError = rndoffLhs - rndoffRhs
val prec = getUpperBound(precLhs, precRhs)
val rndoff = computeNewError(range, propagatedError, prec)
intermediateErrors += (x -> rndoff)