Commit 3c4b0cb0 authored by Eva Darulova's avatar Eva Darulova

adding scripts and fixing option naming

parent 382562aa
#!/bin/bash --posix
#
# This script
# 'Standard' benchmark set
declare -a files=("testcases/rosa/Bsplines.scala" \
"testcases/rosa/Doppler.scala" \
"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 --analysis=dataflow ${file}
done
\ No newline at end of file
#!/bin/bash --posix
#
# This script
# 'Standard' benchmark set
declare -a files=("testcases/rosa/Bsplines.scala" \
"testcases/rosa/Doppler.scala" \
"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 --analysis=opt ${file}
done
\ No newline at end of file
#!/bin/bash --posix
#
# This script
# 'Standard' benchmark set
declare -a files=("testcases/rosa/Bsplines.scala" \
"testcases/rosa/Doppler.scala" \
"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 --analysis=relative ${file}
done
\ No newline at end of file
#!/bin/bash --posix
#
# This script
# 'Standard' benchmark set
declare -a files=("testcases/rosa/Bsplines.scala" \
"testcases/rosa/Doppler.scala" \
"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 --analysis=dataflowSubdiv ${file}
done
\ No newline at end of file
#!/bin/bash --posix
#
# This script
# 'Standard' benchmark set
declare -a files=("testcases/rosa/Bsplines.scala" \
"testcases/rosa/Doppler.scala" \
"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 --codegen --precision=Fixed32 ${file}
done
\ No newline at end of file
......@@ -15,18 +15,22 @@ object Main {
"If enabled, will print those SMT queries to file which take longer.")
val optionSolver = ChoiceOptionDef("solver", "smt solver to use for smt range analysis",
Set("dreal", "dReal", "z3"), "z3")
Set("dReal", "z3"), "z3")
val optionAnalysis = ChoiceOptionDef("analysis", "Which analysis method to use.",
Set("dataflow", "opt", "dataflowSubdiv", "relative"), "dataflow")
val globalOptions: Set[CmdLineOptionDef[Any]] = Set(
FlagOptionDef("help", "Show this message."),
FlagOptionDef("dynamic", "Run dynamic analysis."),
FlagOptionDef("relative", "Run experimental relative phase"),
FlagOptionDef("taylor", "Run experimental taylor simplification phase"),
FlagOptionDef("absSubdiv", "Run experimental relative through absolute error phase"),
// ParamOptionDef("timeout", "Timeout in ms.", "1000"),
ListOptionDef("debug", "For which sections to print debug info.",
FlagOptionDef("help", "Show this message."),
ListOptionDef("debug", "For which sections to print debug info.",
List("analysis","solver")),
FlagOptionDef("dynamic", "Run dynamic analysis."),
FlagOptionDef("codegen", "Generate code (as opposed to just doing analysis)."),
// FlagOptionDef("relative", "Run experimental relative phase"),
// FlagOptionDef("taylor", "Run experimental taylor simplification phase"),
// FlagOptionDef("absSubdiv", "Run experimental relative through absolute error phase"),
// ParamOptionDef("timeout", "Timeout in ms.", "1000"),
optionAnalysis,
optionFunctions,
optionPrintToughSMTCalls,
optionSolver
......@@ -41,7 +45,7 @@ object Main {
analysis.RangeErrorPhase,
analysis.RelativeErrorPhase,
analysis.TaylorErrorPhase,
analysis.RelThroughAbsPhase,
analysis.DataflowSubdivisionPhase,
backend.CodeGenerationPhase,
transform.SSATransformerPhase,
analysis.DynamicPhase,
......@@ -64,6 +68,7 @@ object Main {
val pipeline = computePipeline(ctx)
try { // for debugging it's better to have these off.
ctx.reporter.info("\n************ Starting Daisy ************")
pipeline.run(ctx, inputPrg)
} catch {
case e: DaisyFatalError => ctx. reporter.info("Something really bad happened. Cannot continue.")
......@@ -170,43 +175,85 @@ object Main {
private def computePipeline(ctx: Context): Pipeline[Program, Program] = {
val fixedPointArith = ctx.findOption(analysis.RangeErrorPhase.optionPrecision) match {
case Some("Fixed16") => true
case Some("Fixed32") => true
val ssaNeeded = ctx.findOption(analysis.RangeErrorPhase.optionPrecision) match {
case Some("Fixed16") | Some("Fixed32") =>
ctx.hasFlag("codegen")
case _ => false
}
// this is not ideal, using 'magic' strings
val beginning = analysis.SpecsProcessingPhase
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
beginning andThen analysis.DynamicPhase
} else {
analysis.SpecsProcessingPhase andThen
analysis.RangeErrorPhase andThen
backend.InfoPhase
val analysisPipeline = ((ssaNeeded, ctx.findOption(optionAnalysis)): @unchecked) match {
case (true, Some("dataflow")) =>
transform.SSATransformerPhase andThen analysis.RangeErrorPhase
case (false, Some("dataflow")) =>
analysis.RangeErrorPhase
case (_, Some("opt")) =>
analysis.TaylorErrorPhase
case (_, Some("dataflowSubdiv")) =>
analysis.DataflowSubdivisionPhase
case (_, Some("relative")) =>
analysis.RelativeErrorPhase
case (true, None) =>
ctx.reporter.info("No analysis method specified, choosing default.")
transform.SSATransformerPhase andThen analysis.RangeErrorPhase
case (false, None) =>
ctx.reporter.info("No analysis method specified, choosing default.")
analysis.RangeErrorPhase
}
if (ctx.hasFlag("codegen")) {
beginning andThen analysisPipeline andThen backend.InfoPhase andThen
backend.CodeGenerationPhase
} else {
beginning andThen analysisPipeline andThen backend.InfoPhase
}
}
// 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
// }
}
}
......@@ -31,7 +31,7 @@ import scala.util.control.Breaks._
*Prerequisites:
*- SpecsProcessingPhase
*/
object RelThroughAbsPhase extends DaisyPhase with Subdivision with RoundoffEvaluators {
object DataflowSubdivisionPhase extends DaisyPhase with Subdivision with RoundoffEvaluators {
override val name = "forward dataflow with subdivision"
override val description = "computes relative errors directly"
......
......@@ -21,8 +21,8 @@ import Rational._
*/
object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalSubdivision {
override val name = "range-error phase"
override val description = "Computes ranges and absolute errors"
override val name = "dataflow error phase"
override val description = "Computes ranges and absolute errors via dataflow analysis"
val optionPrecision = ChoiceOptionDef("precision", "Type of precision to use",
Set("Float32", "Float64", "DoubleDouble", "QuadDouble",
......
......@@ -51,26 +51,39 @@ object InfoPhase extends DaisyPhase {
reporter.info(fnc.id)
val absError = ctx.resultAbsoluteErrors(fnc.id)
val range = ctx.resultRealRanges(fnc.id)
val absError = ctx.resultAbsoluteErrors.get(fnc.id)
val range = ctx.resultRealRanges.get(fnc.id)
val absErrorString = absError match {
case Some(x) => x.toString
case None => "-"
}
val rangeString = range match {
case Some(x) => x.toString
case None => "-"
}
// if a relative error was already computed print it, otherwise compute here
val relError: String = ctx.resultRelativeErrors.get(fnc.id) match {
val relErrorString: String = ctx.resultRelativeErrors.get(fnc.id) match {
case Some(Some(x)) =>
x.toString
case Some(None) =>
"n/a"
case None =>
val range = ctx.resultRealRanges(fnc.id) // at this point it has to have been computed
if (range.xlo <= zero && zero <= range.xhi) {
"n/a"
} else {
max(abs(absError / range.xlo), abs(absError / range.xhi)).toString
(absError, range) match {
case (Some(e), Some(r)) =>
if (r.xlo <= zero && zero <= r.xhi) {
"n/a"
} else {
max(abs(e / r.xlo), abs(e / r.xhi)).toString
}
case _ => "-"
}
}
val infoString: String =
s"abs-error: ${absError}, real range: ${range},\nrel-error: ${relError}"
s"abs-error: ${absErrorString}, real range: ${rangeString},\nrel-error: ${relErrorString}"
reporter.info(infoString)
if (out != null) {
......
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