Commit b6798c3e authored by Eva Darulova's avatar Eva Darulova

adding mixed-precision support, at least for floats

parent 8423994c
......@@ -8,7 +8,8 @@ import scala.reflect.ClassTag
import lang.Trees.Expr
import lang.Identifiers._
import tools.{Interval, PartialInterval, Rational}
import tools.{Interval, PartialInterval, Rational, FinitePrecision}
import FinitePrecision.Precision
case class Context(
reporter: Reporter,
......@@ -25,6 +26,10 @@ case class Context(
// indexed by FunDef.id
specInputRanges: Map[Identifier, Map[Identifier, Interval]] = Map(),
specInputErrors: Map[Identifier, Map[Identifier, Rational]] = Map(),
specMixedPrecisions: Map[Identifier, Map[Identifier, Precision]] = Map(),
specInferredReturnTypes: Map[Identifier, Precision] = Map(),
fixedPoint: Boolean = false,
// for now we only support a single result value, i.e. no tuples
// this map is indexed by fnc.id -> potentially partial interval bound of result
// and similar for the errors
......
......@@ -20,6 +20,19 @@ object Main {
val optionAnalysis = ChoiceOptionDef("analysis", "Which analysis method to use.",
Set("dataflow", "opt", "dataflowSubdiv", "relative"), "dataflow")
val optionMixedPrecFile = ParamOptionDef("mixed-precision", """File with type assignment for all variables.
The format is the following:
function_name = {
variable_name_1: prec_1
variable_name_2: prec_2
... }
function_name_2 = {
variable_name_i: prec_i }
The precision is Float, Double or DoubleDouble.
The file can give only a partial precision map.""", "")
val globalOptions: Set[CmdLineOptionDef[Any]] = Set(
FlagOptionDef("help", "Show this message."),
ListOptionDef("debug", "For which sections to print debug info.",
......@@ -33,7 +46,8 @@ object Main {
optionAnalysis,
optionFunctions,
optionPrintToughSMTCalls,
optionSolver
optionSolver,
optionMixedPrecFile
)
/*
......@@ -95,6 +109,7 @@ object Main {
var validOptions: List[CmdLineOption[Any]] = List()
var debugSections = Set[DebugSection]()
var fixedPoints: Boolean = false
for (opt <- options) {
opt.drop(2).split("=", 2).toList match {
......@@ -144,13 +159,18 @@ object Main {
case FlagOption("help") =>
showHelp(initReporter)
case ChoiceOption("precision", "Fixed16") | ChoiceOption("precision", "Fixed32") =>
fixedPoints = true
case _ =>
}
Context(
reporter = new DefaultReporter(debugSections),
files = inputFiles,
options = validOptions
options = validOptions,
fixedPoint = fixedPoints
)
}
......@@ -175,11 +195,7 @@ object Main {
private def computePipeline(ctx: Context): Pipeline[Program, Program] = {
val ssaNeeded = ctx.findOption(analysis.RangeErrorPhase.optionPrecision) match {
case Some("Fixed16") | Some("Fixed32") =>
ctx.hasFlag("codegen")
case _ => false
}
val ssaNeeded = ctx.fixedPoint && ctx.hasFlag("codegen")
val beginning = analysis.SpecsProcessingPhase
......
......@@ -52,6 +52,7 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
var trackInitialErrs = true
var trackRoundoffErrs = true
var mixedPrecision: Boolean = false
var uniformPrecision: Precision = Float64
// process relevant options
......@@ -85,9 +86,12 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
case _ =>
reporter.warning(s"Unknown precision specified: $s, choosing default ($uniformPrecision)!")
}
case ParamOption("mixed-precision", _) => mixedPrecision = true
case _ =>
}
val fncsToConsider: Seq[String] = functionsToConsider(ctx, prg)
// returns (abs error, result range, interm. errors, interm. ranges)
......@@ -99,6 +103,12 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
reporter.info("analyzing fnc: " + fnc.id)
val inputValMap: Map[Identifier, Interval] = ctx.specInputRanges(fnc.id)
val precisionMap: Map[Identifier, Precision] = if (mixedPrecision) {
ctx.specMixedPrecisions(fnc.id)
} else {
allVariablesOf(fnc.body.get).map(id => (id -> uniformPrecision)).toMap
}
// 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.
......@@ -108,7 +118,7 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
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 -> precisionMap(id).absRoundoff(inputValMap(id))))
} else if (trackInitialErrs) {
......@@ -120,7 +130,7 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
} else if (trackRoundoffErrs) {
val allIDs = fnc.params.map(_.id)
allIDs.map(id => (id -> uniformPrecision.absRoundoff(inputValMap(id)))).toMap
allIDs.map(id => (id -> precisionMap(id).absRoundoff(inputValMap(id)))).toMap
} else {
......@@ -140,7 +150,7 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
val (resRange, intermediateRanges) = evalRange[Interval](fncBody, inputValMap, Interval.apply)
val (resRoundoff, allErrors) = evalRoundoff[AffineForm](fncBody, intermediateRanges,
allVariablesOf(fncBody).map(id => (id -> uniformPrecision)).toMap,
precisionMap,
inputErrorMap.map(x => (x._1 -> AffineForm.fromError(x._2))),
zeroError = AffineForm.zero,
fromError = AffineForm.fromError,
......@@ -162,7 +172,7 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
val (resRoundoff, allErrors) = evalRoundoff[AffineForm](fncBody,
intermediateRanges.map(x => (x._1 -> x._2.toInterval)),
allVariablesOf(fncBody).map(id => (id -> uniformPrecision)).toMap,
precisionMap,
inputErrorMap.map(x => (x._1 -> AffineForm.fromError(x._2))),
zeroError = AffineForm.zero,
fromError = AffineForm.fromError,
......@@ -185,7 +195,7 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
val (resRoundoff, allErrors) = evalRoundoff[AffineForm](fncBody,
intermediateRanges.map(x => (x._1 -> x._2.toInterval)),
allVariablesOf(fncBody).map(id => (id -> uniformPrecision)).toMap,
precisionMap,
inputErrorMap.map(x => (x._1 -> AffineForm.fromError(x._2))),
zeroError = AffineForm.zero,
fromError = AffineForm.fromError,
......
......@@ -3,10 +3,14 @@
package daisy
package analysis
import scala.util.parsing.combinator._
import lang.Trees._
import tools.{Interval, PartialInterval, Rational}
import tools.{Interval, PartialInterval, Rational, FinitePrecision}
import FinitePrecision._
import lang.Identifiers._
import lang.TreeOps.preTraversal
import lang.Extractors._
import lang.TreeOps.{preTraversal, allVariablesOf}
import lang.Trees.Program
/**
......@@ -26,7 +30,7 @@ import lang.Trees.Program
Prerequisite:
None
*/
object SpecsProcessingPhase extends DaisyPhase {
object SpecsProcessingPhase extends DaisyPhase with PrecisionsParser {
override val name = "Specs processing"
override val description = "Processes the specifications for later phases."
......@@ -36,11 +40,48 @@ object SpecsProcessingPhase extends DaisyPhase {
var reporter: Reporter = null
val defaultPrecision = Float64
def run(ctx: Context, prg: Program): (Context, Program) = {
reporter = ctx.reporter
// reporter.info("\nStarting specs preprocessing phase")
val timer = ctx.timers.preprocess.start
//
val precisionMap: Map[Identifier, (Map[Identifier, Precision], Precision)] = ctx.findOption(Main.optionMixedPrecFile) match {
case Some(file) =>
// maps from fnc/variable names to their respective identifiers
val (fncIdMap, varIdMap) = buildIdentifierMap(prg)
// a mixed-precision assignment file has been provided, parse it
val precMapsParsed = parseMixedPrecisionFile(file, fncIdMap, varIdMap)
prg.defs.map(fnc => {
(precMapsParsed.get(fnc.id), fnc.body) match {
case (None, None) =>
(fnc.id -> (Map[Identifier, Precision](), defaultPrecision))
case (None, Some(body)) =>
// no spec is given, so assign default precision
(fnc.id -> (allVariablesOf(body).map(v => (v -> defaultPrecision)).toMap,
defaultPrecision))
case (Some(precMap), None) =>
(fnc.id -> (precMap, defaultPrecision))
case (Some(precMap), Some(body)) =>
val (completePrecMap, returnPrec) = typecheck(body, precMap, defaultPrecision)
(fnc.id -> (completePrecMap, returnPrec))
}
}).toMap
case None =>
Map()
}
// println("precision map:")
// println(precisionMap)
var allRanges: Map[Identifier, Map[Identifier, Interval]] = Map()
var allErrors: Map[Identifier, Map[Identifier, Rational]] = Map()
var resRanges: Map[Identifier, PartialInterval] = Map()
......@@ -120,12 +161,11 @@ object SpecsProcessingPhase extends DaisyPhase {
reporter.debug("error bounds: " + resErrors.mkString("\n"))
(ctx.copy(specInputRanges = allRanges, specInputErrors = allErrors,
specResultRangeBounds = resRanges, specResultErrorBounds = resErrors), prg)
specResultRangeBounds = resRanges, specResultErrorBounds = resErrors,
specMixedPrecisions = precisionMap.mapValues(_._1),
specInferredReturnTypes = precisionMap.mapValues(_._2)), prg)
}
def extractPreCondition(expr: Expr): (Map[Identifier, (Rational, Rational)],
Map[Identifier, Rational]) = {
......@@ -188,8 +228,98 @@ object SpecsProcessingPhase extends DaisyPhase {
(lowerBound, upperBound, absError)
}
def buildIdentifierMap(prg: Program): (Map[String, Identifier], Map[String, Map[String, Identifier]]) = {
def buildIdentifierMapFunction(f: FunDef): Map[String, Identifier] = {
allVariablesOf(f.body.get).map(id => ((id.toString) -> id)).toMap
}
(prg.defs.map(fnc => (fnc.id.name -> fnc.id)).toMap,
prg.defs.map(fnc => (fnc.id.name -> buildIdentifierMapFunction(fnc))).toMap)
}
private def parseMixedPrecisionFile(f: String, fncIdMap: Map[String, Identifier],
varIdMap: Map[String, Map[String, Identifier]]): Map[Identifier, Map[Identifier, Precision]] = {
def treeToMap(p: List[FunAssign]): Map[Identifier, Map[Identifier, Precision]] = {
def typeAssignsToMap(l: List[TypeAssign], funcId: String): Map[Identifier, Precision] = {
l.foldLeft[Map[Identifier, Precision]](Map())((m, tA) => tA match {
case TypeAssign(varName, precision) => m + (varIdMap(funcId)(varName) -> precision) })
}
p.foldLeft[Map[Identifier, Map[Identifier, Precision]]](Map())((m, fA) => fA match {
case FunAssign(funName, types) => m + (fncIdMap(funName) -> typeAssignsToMap(types, funName))
})
}
}
\ No newline at end of file
val bufferedSource = io.Source.fromFile(f)
val sourceText = bufferedSource.mkString
bufferedSource.close
parse(overall_function, sourceText) match {
case Success(precisionsTree, _) => treeToMap(precisionsTree)
case Failure(msg, _) => reporter.fatalError("Failure during the parsing of the type assignment file: " + msg)
case Error(msg, _) => reporter.fatalError("Error during the parsing of the type assignment file: " + msg)
}
}
def typecheck(expr: Expr, precisionMap: Map[Identifier, Precision], defaultPrec: Precision): (Map[Identifier, Precision], Precision) = {
def eval(e: Expr, precMap: Map[Identifier, Precision]): (Map[Identifier, Precision], Precision) = e match {
case Variable(id) =>
precMap.get(id) match {
case Some(m) => (precMap, m)
case None => (precMap + (id -> defaultPrecision), defaultPrecision)
}
case RealLiteral(r) => (precMap, defaultPrecision)
case ArithOperator(Seq(l, r), recons) =>
val (mapLeft, precLeft) = eval(l, precMap)
val (mapRight, precRight) = eval(r, mapLeft)
val precResult = getUpperBound(precLeft, precRight)
(mapRight, precResult)
case ArithOperator(Seq(u), recons) =>
eval(u, precMap)
case Let(id, value, body) =>
val (mapValue, precValue) = eval(value, precMap)
precMap.get(id) match {
// precision of assigned variable is given
case Some(m) =>
eval(body, mapValue)
case None =>
eval(body, mapValue + (id -> precValue))
}
}
eval(expr, precisionMap)
}
}
trait PrecisionsParser extends RegexParsers with JavaTokenParsers {
def identifier: Parser[String] = """[a-zA-Z_][a-zA-Z0-9_]*""".r ^^ {x: String => x }
def float256: Parser[Precision] = "QuadDouble" ^^ { case _ => QuadDouble }
def float128: Parser[Precision] = "DoubleDouble" ^^ { case _ => DoubleDouble }
def float64: Parser[Precision] = "Double" ^^ { case _ => Float64 }
def float32: Parser[Precision] = "Float" ^^ { case _ => Float32 }
def type_var: Parser[TypeAssign] = identifier ~ ":" ~ (float256 | float128 | float64 | float32) ^^ { case i ~ _ ~ p => TypeAssign(i, p) }
def typemap_function: Parser[FunAssign] = identifier ~ "=" ~ "{" ~ rep1(type_var) ~ "}" ^^ { case i ~ _ ~ _ ~ types ~ _ => FunAssign(i, types) }
def overall_function: Parser[List[FunAssign]] = rep1(typemap_function) ^^ { case l => l }
}
abstract class Precisions
case class TypeAssign(f: String, p: Precision) extends Precisions
case class FunAssign(f: String, s: List[TypeAssign]) extends Precisions
\ No newline at end of file
......@@ -3,12 +3,16 @@
package daisy
package backend
import scala.collection.immutable.Seq
import daisy.lang.{ScalaPrinter, PrettyPrinter}
import lang.Trees._
import lang.TreeOps.allVariablesOf
import tools.FinitePrecision._
import lang.Types._
import lang.Extractors.ArithOperator
import tools.{Rational, Interval}
import lang.Identifiers.Identifier
object CodeGenerationPhase extends DaisyPhase {
......@@ -27,6 +31,7 @@ object CodeGenerationPhase extends DaisyPhase {
reporter.info(s"\nStarting $name")
val timer = ctx.timers.rangeError.start
var mixedPrecision: Boolean = false
var uniformPrecision: Precision = Float64
/* Process relevant options */
......@@ -44,40 +49,70 @@ object CodeGenerationPhase extends DaisyPhase {
case _ =>
ctx.reporter.warning(s"Unknown precision specified: $s, choosing default ($uniformPrecision)!")
}
case ParamOption("mixed-precision", _) => mixedPrecision = true
case _ => ;
}
val newProgram = uniformPrecision match {
case Fixed(b) =>
// if we have fixed-point code, we need to generate it first
val newDefs = prg.defs.map(fnc => if (!fnc.body.isEmpty && !fnc.precondition.isEmpty) {
val newBody = toFixedPointCode(fnc.body.get, Fixed(b),
ctx.intermediateRanges(fnc.id), ctx.intermediateAbsErrors(fnc.id))
val valDefType = if (b == 16) Int32Type else Int64Type
fnc.copy(
params = fnc.params.map(vd => ValDef(vd.id.changeType(valDefType))),
body = Some(newBody),
returnType = valDefType)
} else {
fnc
})
val newPrg = Program(prg.id, newDefs)
val fileLocation = "./output/" + prg.id + ".scala"
ctx.reporter.info("generating code in " + fileLocation)
writeScalaFile(fileLocation, newPrg)
newPrg
case _ =>
// if we have floating-point code, we need to just change the types
val fileLocation = "./output/" + prg.id + ".scala"
ctx.reporter.info("generating code in " + fileLocation)
val typedPrg = assignFloatType(prg, FinitePrecisionType(uniformPrecision))
writeScalaFile(fileLocation, typedPrg)
typedPrg
val newProgram = if (ctx.fixedPoint) {
if (mixedPrecision) {
reporter.error("Mixed-precision code generation is currently not supported for fixed-points.")
}
(uniformPrecision: @unchecked) match {
case Fixed(b) =>
// if we have fixed-point code, we need to generate it first
val newDefs = prg.defs.map(fnc => if (!fnc.body.isEmpty && !fnc.precondition.isEmpty) {
val newBody = toFixedPointCode(fnc.body.get, Fixed(b),
ctx.intermediateRanges(fnc.id), ctx.intermediateAbsErrors(fnc.id))
val valDefType = if (b == 16) Int32Type else Int64Type
fnc.copy(
params = fnc.params.map(vd => ValDef(vd.id.changeType(valDefType))),
body = Some(newBody),
returnType = valDefType)
} else {
fnc
})
val newPrg = Program(prg.id, newDefs)
val fileLocation = "./output/" + prg.id + ".scala"
ctx.reporter.info("generating code in " + fileLocation)
writeScalaFile(fileLocation, newPrg)
newPrg
}
} else {
val precisionMap: Map[Identifier, Map[Identifier, Precision]] = if (mixedPrecision) {
ctx.specMixedPrecisions //.mapValues(_.mapValues(FinitePrecisionType(_)))
} else {
prg.defs.map(fnc =>
if (fnc.body.isEmpty) {
(fnc.id -> Map[Identifier, Precision]())
} else {
(fnc.id -> allVariablesOf(fnc.body.get).map(id => (id -> uniformPrecision)).toMap)
}
).toMap
}
val returnPrecisionMap: Map[Identifier, Precision] = if (mixedPrecision) {
ctx.specInferredReturnTypes //.mapValues(FinitePrecisionType(_))
} else {
prg.defs.map(fnc => (fnc.id -> uniformPrecision)).toMap
}
// if we have floating-point code, we need to just change the types
val fileLocation = "./output/" + prg.id + ".scala"
ctx.reporter.info("generating code in " + fileLocation)
val typedPrg = assignFloatType(prg, precisionMap, returnPrecisionMap, uniformPrecision)
writeScalaFile(fileLocation, typedPrg)
typedPrg
}
timer.stop
ctx.reporter.info(s"Finished $name")
(ctx, newProgram)
......@@ -92,29 +127,52 @@ object CodeGenerationPhase extends DaisyPhase {
out.close
}
private def assignFloatType(prg: Program, tpe: FinitePrecisionType): Program = {
private def assignFloatType(prg: Program, typeMaps: Map[Identifier, Map[Identifier, Precision]],
returnTypes: Map[Identifier, Precision], defaultPrecision: Precision): Program = {
def changeType(e: Expr, tpeMap: Map[Identifier, Precision]): (Expr, Precision) = e match {
case Variable(id) =>
(Variable(id.changeType(FinitePrecisionType(tpeMap(id)))), tpeMap(id))
def changeType(e: Expr): Expr = e match {
case Variable(id) => Variable(id.changeType(tpe))
case x @ RealLiteral(r) =>
val tmp = FinitePrecisionLiteral(r, tpe.prec)
val tmp = FinitePrecisionLiteral(r, defaultPrecision)
tmp.stringValue = x.stringValue
tmp
case ArithOperator(args, recons) =>
recons(args.map(changeType))
(tmp, defaultPrecision)
case ArithOperator(Seq(l, r), recons) =>
val (eLeft, pLeft) = changeType(l, tpeMap)
val (eRight, pRight) = changeType(r, tpeMap)
val prec = getUpperBound(pLeft, pRight)
(recons(Seq(eLeft, eRight)), prec)
case ArithOperator(Seq(t), recons) =>
val (e, p) = changeType(t, tpeMap)
(recons(Seq(e)), p)
case Let(id, value, body) =>
Let(id.changeType(tpe), changeType(value), changeType(body))
val (eValue, valuePrec) = changeType(value, tpeMap)
val (eBody, bodyPrec) = changeType(body, tpeMap)
val idPrec = tpeMap(id)
if (idPrec >= valuePrec) {
(Let(id.changeType(FinitePrecisionType(tpeMap(id))), eValue, eBody), bodyPrec)
} else {
val newValue = Downcast(eValue, FinitePrecisionType(idPrec))
(Let(id.changeType(FinitePrecisionType(tpeMap(id))), newValue, eBody), bodyPrec)
}
}
val newDefs = prg.defs.map({
case FunDef(id, returnType, params, pre, body, post, isField) =>
FunDef(id, tpe,
params.map(vd => ValDef(vd.id.changeType(tpe))),
FunDef(id, FinitePrecisionType(returnTypes(id)),
params.map(vd => ValDef(vd.id.changeType(FinitePrecisionType(typeMaps(id)(vd.id))))),
// this should really be changed too
pre,
body.map(changeType(_)),
body.map(changeType(_, typeMaps(id))._1),
post,
isField
)
......
......@@ -163,7 +163,7 @@ class PrettyPrinter(val sb: StringBuffer = new StringBuffer, printUniqueIds: Boo
sb.append(x.stringValue + "f")
case x @ FinitePrecisionLiteral(r, _) =>
sb.append(x.stringValue)
case Downcast(expr, tpe) => ppUnary(expr, "downcast(", ", " + tpe + ")")
case FunctionInvocation(fdId, _, args, _) =>
pp(fdId, p)
......
......@@ -5,7 +5,8 @@ package daisy
package lang
import Trees._
import daisy.lang.Types.RealType
import daisy.lang.Types._
import tools.FinitePrecision._
object ScalaPrinter {
......@@ -44,6 +45,9 @@ class ScalaPrinter extends PrettyPrinter {
case RealType =>
throw new Exception("RealType found in ScalaPrinter")
case Downcast(expr, FinitePrecisionType(Float32)) => ppUnary(expr, "", ".toFloat")
case Downcast(expr, FinitePrecisionType(Float64)) => ppUnary(expr, "", ".toDouble")
case Downcast(expr, FinitePrecisionType(DoubleDouble)) => ppUnary(expr, "DblDouble(", ")")
case Program(id, defs) =>
......
......@@ -335,7 +335,12 @@ object Trees {
}
}
case class Downcast(expr: Expr, newType: TypeTree) extends Expr {
val getType = newType
def deepCopy = {
Downcast(expr.deepCopy, newType)
}
}
/* Propositional logic */
......
doppler = {
u: Double
v: Double
T: Float
t1: Float
}
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