Commit 2f848c4b authored by Eva Darulova's avatar Eva Darulova
Browse files

Fix abs-errors for fixed-points and regression tests

parent a76dcc9a
......@@ -129,7 +129,7 @@ object CodeGenerationPhase extends DaisyPhase {
* @param fixed the (uniform) fixed-point precision to use
// TODO: we also need to adjust the types, no?
*/
private def toFixedPointCode(expr: Expr, fixed: Fixed): Expr = (expr: @unchecked) match {
def toFixedPointCode(expr: Expr, fixed: Fixed): Expr = (expr: @unchecked) match {
case x @ Variable(id) => fixed match {
case Fixed(16) => Variable(id.changeType(Int32Type))
case Fixed(32) => Variable(id.changeType(Int64Type))
......
......@@ -15,36 +15,38 @@ object FinitePrecision {
// if it's an integer, it's definitely representable
if (r.isWhole) {
true
} else if (prec == DoubleDouble || prec == QuadDouble) {
// don't want to deal with those huge number here right now,
// so return the safe answer
false
} else {
val nominator = r.n.abs
val denominator = r.d.abs
val (nomBound, denomBound) = (prec: @unchecked) match {
case Float32 =>
// 2^23 - 1, 2^8 -1
(8388607l, 255l)
case Float64 =>
// 2^52 - 1, 2^11 -1
(4503599627370496l, 2047l)
}
prec match {
case DoubleDouble | QuadDouble => false
case Fixed(_) => false
case Float32 | Float64 =>
val nominator = r.n.abs
val denominator = r.d.abs
val (nomBound, denomBound) = (prec: @unchecked) match {
case Float32 =>
// 2^23 - 1, 2^8 -1
(8388607l, 255l)
case Float64 =>
// 2^52 - 1, 2^11 -1
(4503599627370496l, 2047l)
}
if (nominator <= nomBound && denominator <= denomBound) {
val exponent: Double = math.log(denominator.toDouble) / math.log(2)
if (nominator <= nomBound && denominator <= denomBound) {
val exponent: Double = math.log(denominator.toDouble) / math.log(2)
if (exponent.isWhole) {
// maybe the log computations isn't sound due to roundoffs, let's sanity check:
assert(math.pow(2, exponent) == denominator)
true
} else {
false
}
if (exponent.isWhole) {
// maybe the log computations isn't sound due to roundoffs, let's sanity check:
assert(math.pow(2, exponent) == denominator)
true
} else {
false
}
} else {
false
}
}
}
......
......@@ -106,6 +106,41 @@ object RangeRegressionFunctions {
}
def kepler0(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real): Real = {
require(4 <= x1 && x1 <= 6.36 && 4 <= x2 && x2 <= 6.36 && 4 <= x3 && x3 <= 6.36 &&
4 <= x4 && x4 <= 6.36 && 4 <= x5 && x5 <= 6.36 && 4 <= x6 && x6 <= 6.36)
x2 * x5 + x3 * x6 - x2 * x3 - x5 * x6 + x1 * (-x1 + x2 + x3 - x4 + x5 + x6)
} // 1.15e-15
def kepler1(x1: Real, x2: Real, x3: Real, x4: Real): Real = {
require(4 <= x1 && x1 <= 6.36 && 4 <= x2 && x2 <= 6.36 && 4 <= x3 && x3 <= 6.36 &&
4 <= x4 && x4 <= 6.36)
x1 * x4 * (-x1 + x2 + x3 - x4) + x2 * (x1 - x2 + x3 + x4) + x3 * (x1 + x2 - x3 + x4) -
x2 * x3 * x4 - x1 * x3 - x1 * x2 - x4
} // 4.50e–13
def kepler2(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real): Real = {
require(4 <= x1 && x1 <= 6.36 && 4 <= x2 && x2 <= 6.36 && 4 <= x3 && x3 <= 6.36 &&
4 <= x4 && x4 <= 6.36 && 4 <= x5 && x5 <= 6.36 && 4 <= x6 && x6 <= 6.36)
x1 * x4 * (-x1 + x2 + x3 - x4 + x5 + x6) + x2 * x5 * (x1 - x2 + x3 + x4 - x5 + x6) +
x3* x6 * (x1 + x2 - x3 + x4 + x5 - x6) - x2 * x3 * x4 -
x1* x3* x5 - x1 * x2 * x6 - x4 * x5 * x6
} //2.08e–12
def himmilbeau(x1: Real, x2: Real) = {
require(-5 <= x1 && x1 <= 5 && -5 <= x2 && x2 <= 5)
(x1*x1 + x2 - 11)*(x1 * x1 + x2 - 11) + (x1 + x2*x2 - 7)*(x1 + x2*x2 - 7)
} //1.43e–12
/*def jetEngine(x1: Real, x2: Real) = {
require(-5 <= x1 && x1 <= 5 && -20 <= x2 && x2 <= 5)
x1 + (
......
......@@ -7,6 +7,9 @@ import org.scalatest.FunSuite
import lang.Trees.{Expr, Let}
import lang.NumAnnotation
/**
Regression test for the basic absolute error and range computations.
*/
class AbsErrorAnalysisRegressionTest extends FunSuite {
val inputFile: String = "src/test/resources/AbsErrorRegressionFunctions.scala"
......@@ -17,13 +20,58 @@ class AbsErrorAnalysisRegressionTest extends FunSuite {
files = List(inputFile)
)
// default analysis: IA - AA
val inputPrg = frontend.ExtractionPhase(context)
val pipeline = analysis.SpecsProcessingPhase andThen analysis.RangeErrorPhase
// Regression results
// fnc.id -> (abs error, range)
val intAA: Map[String, (String, String)] = Map(
val intAA_Fixed32: Map[String, (String, String)] = Map(
("doppler", ("1.75791622644632e-06", "[-158.7191444098274, -0.02944244059231351]")),
("sine", ("5.172930285837377e-09", "[-2.3011348046703466, 2.3011348046703466]")),
("sineOrder3", ("7.483225706087375e-09", "[-2.9419084189651277, 2.9419084189651277]")),
("sqroot", ("4.015397284953641e-06", "[-402.125, 68.5]")),
("bspline0", ("8.537123605701497e-10", "[0.0, 0.16666666666666666]")),
("bspline1", ("3.337239226446336e-09", "[-0.3333333333333333, 1.1666666666666667]")),
("bspline2", ("3.104408582665976e-09", "[-0.3333333333333333, 1.1666666666666667]")),
("bspline3", ("6.208817165548793e-10", "[-0.16666666666666666, 0.0]")),
("rigidBody1", ("1.3485550881126018e-06", "[-705.0, 705.0]")),
("rigidBody2", ("0.0001531802118132919", "[-58740.0, 58740.0]")),
("verhulst", ("3.009066920607247e-09", "[0.3148936170212766, 1.1008264462809918]")),
("predatorPrey", ("1.647071564900709e-09", "[0.03727705922396188, 0.35710168263424846]")),
("carbonGas", ("17.69469347003061", "[2097409.2, 3.434323E7]")),
("turbine1", ("5.059999504388075e-07", "[-58.32912689020381, -1.5505285721480735]")),
("turbine2", ("6.241048750415222e-07", "[-29.43698909090909, 80.993]")),
("turbine3", ("3.6766172442271937e-07", "[0.4660958448753463, 40.375126890203816]")),
("kepler0", ("4.379078746518522e-07", "[-35.7792, 159.8176]")),
("kepler1", ("2.021807432895287e-06", "[-490.320768, 282.739712]")),
("kepler2", ("1.037595868540202e-05", "[-871.597824, 1860.323072]")),
("himmilbeau", ("9.75281000696604e-06", "[-1630.0, 3050.0]"))
)
val intAA_Float32: Map[String, (String, String)] = Map(
("doppler", ("0.0002250138141196529", "[-158.7191444098274, -0.02944244059231351]")),
("sine", ("6.064885588214318e-07", "[-2.3011348046703466, 2.3011348046703466]")),
("sineOrder3", ("7.790389913381473e-07", "[-2.9419084189651277, 2.9419084189651277]")),
("sqroot", ("0.00016796589915202306", "[-402.125, 68.5]")),
("bspline0", ("8.69234485871102e-08", "[0.0, 0.16666666666666666]")),
("bspline1", ("4.2716663302873797e-07", "[-0.3333333333333333, 1.1666666666666667]")),
("bspline2", ("3.973643085686263e-07", "[-0.3333333333333333, 1.1666666666666667]")),
("bspline3", ("5.712112027822517e-08", "[-0.16666666666666666, 0.0]")),
("rigidBody1", ("0.00017261505240639963", "[-705.0, 705.0]")),
("rigidBody2", ("0.01960706761337861", "[-58740.0, 58740.0]")),
("verhulst", ("3.199529347654797e-07", "[0.3148936170212766, 1.1008264462809918]")),
("predatorPrey", ("1.3291118406629398e-07", "[0.03727705922396188, 0.35710168263424846]")),
("carbonGas", ("22.995233482473232", "[2097409.2, 3.434323E7]")),
("turbine1", ("5.095029323813888e-05", "[-58.32912689020381, -1.5505285721480735]")),
("turbine2", ("7.46823932469574e-05", "[-29.43698909090909, 80.993]")),
("turbine3", ("3.797059491586537e-05", "[0.4660958448753463, 40.375126890203816]")),
("kepler0", ("5.605220905522401e-05", "[-35.7792, 159.8176]")),
("kepler1", ("0.0002587913631247376", "[-490.320768, 282.739712]")),
("kepler2", ("0.0013281227815583414", "[-871.597824, 1860.323072]")),
("himmilbeau", ("0.0012483597718073725", "[-1630.0, 3050.0]"))
)
val intAA_Float64: Map[String, (String, String)] = Map(
("doppler", ("4.1911988101104756e-13", "[-158.7191444098274, -0.02944244059231351]")),
("sine", ("1.1296729607621835e-15", "[-2.3011348046703466, 2.3011348046703466]")),
("sineOrder3", ("1.4510731312549944e-15", "[-2.9419084189651277, 2.9419084189651277]")),
......@@ -39,10 +87,64 @@ class AbsErrorAnalysisRegressionTest extends FunSuite {
("carbonGas", ("4.2831938128927477e-08", "[2097409.2, 3.434323E7]")),
("turbine1", ("9.490226544267962e-14", "[-58.32912689020381, -1.5505285721480735]")),
("turbine2", ("1.3910672706969435e-13", "[-29.43698909090909, 80.993]")),
("turbine3", ("7.072570725135768e-14", "[0.4660958448753463, 40.375126890203816]"))
("turbine3", ("7.072570725135768e-14", "[0.4660958448753463, 40.375126890203816]")),
("kepler0", ("1.0440537323574973e-13", "[-35.7792, 159.8176]")),
("kepler1", ("4.820364551960666e-13", "[-490.320768, 282.739712]")),
("kepler2", ("2.4738213255659507e-12", "[-871.597824, 1860.323072]")),
("himmilbeau", ("2.3252511027749283e-12", "[-1630.0, 3050.0]"))
)
val aaAA: Map[String, (String, String)] = Map(
val aaAA_Fixed32: Map[String, (String, String)] = Map(
("doppler", ("5.390735253968273e-06", "[-282.4762120545625, 133.53913086064713]")),
("sine", ("3.584103919585346e-09", "[-1.6540002686363373, 1.6540002686363373]")),
("sineOrder3", ("6.536979105441602e-09", "[-1.909859317102744, 1.909859317102744]")),
("sqroot", ("4.004454244697572e-06", "[-365.875, 195.04296875]")),
("bspline0", ("8.537123605701497e-10", "[-0.0625, 0.16666666666666666]")),
("bspline1", ("3.162616243705934e-09", "[-0.08333333333333333, 0.9791666666666666]")),
("bspline2", ("2.8521753853742843e-09", "[-0.020833333333333332, 0.9166666666666666]")),
("bspline3", ("6.208817165548793e-10", "[-0.16666666666666666, 0.0625]")),
("rigidBody1", ("1.3485550881126018e-06", "[-705.0, 705.0]")),
("rigidBody2", ("0.0001531802118132919", "[-57390.0, 58740.0]")),
("verhulst", ("2.7762362769533775e-09", "[0.35217660784145, 0.9891620430819574]")),
("predatorPrey", ("1.6642254365978505e-09", "[-0.0021029110350001693, 0.34533842311741914]")),
("carbonGas", ("17.682124422310654", "[-6856426.768, 3.159230584E7]")),
("turbine1", ("5.10646976567985e-07", "[-55.55054339020381, 38.36885388122605]")),
("turbine2", ("6.32628951442167e-07", "[-80.18793076923077, 63.665174692307694]")),
("turbine3", ("3.723087505520185e-07", "[-27.227529265841437, 38.719203390203816]")),
("kepler0", ("3.8016587502569254e-07", "[3.0664, 102.8708]")),
("kepler1", ("1.842993498569115e-06", "[-288.15184, 89.927712]")),
("kepler2", ("9.235736732009992e-06", "[-337.61856, 850.310096]")),
("himmilbeau", ("4.194676880030224e-06", "[-775.0, 890.0]"))
)
val aaAA_Float32: Map[String, (String, String)] = Map(
("doppler", ("0.0006900171033357679", "[-282.4762120545625, 133.53913086064713]")),
("sine", ("4.03118783827322e-07", "[-1.6540002686363373, 1.6540002686363373]")),
("sineOrder3", ("6.579194264554884e-07", "[-1.909859317102744, 1.909859317102744]")),
("sqroot", ("0.0001665651899287471", "[-365.875, 195.04296875]")),
("bspline0", ("8.69234485871102e-08", "[-0.0625, 0.16666666666666666]")),
("bspline1", ("4.048148912379665e-07", "[-0.08333333333333333, 0.9791666666666666]")),
("bspline2", ("3.6507845931528976e-07", "[-0.020833333333333332, 0.9166666666666666]")),
("bspline3", ("5.712112027822517e-08", "[-0.16666666666666666, 0.0625]")),
("rigidBody1", ("0.00017261505240639963", "[-705.0, 705.0]")),
("rigidBody2", ("0.01960706761337861", "[-57390.0, 58740.0]")),
("verhulst", ("2.901506123777844e-07", "[0.35217660784145, 0.9891620430819574]")),
("predatorPrey", ("1.342975706563773e-07", "[-0.0021029110350001693, 0.34533842311741914]")),
("carbonGas", ("21.386395374318933", "[-6856426.768, 3.159230584E7]")),
("turbine1", ("5.15451126475071e-05", "[-55.55054339020381, 38.36885388122605]")),
("turbine2", ("7.577347502149163e-05", "[-80.18793076923077, 63.665174692307694]")),
("turbine3", ("3.856541432722763e-05", "[-27.227529265841437, 38.719203390203816]")),
("kepler0", ("4.866123310307557e-05", "[3.0664, 102.8708]")),
("kepler1", ("0.00023590317953098758", "[-288.15184, 89.927712]")),
("kepler2", ("0.0011821743715241617", "[-337.61856, 850.310096]")),
("himmilbeau", ("0.0005369187050519044", "[-775.0, 890.0]"))
)
val aaAA_Float64: Map[String, (String, String)] = Map(
("doppler", ("1.2852513956990104e-12", "[-282.4762120545625, 133.53913086064713]")),
("sine", ("7.508672360829453e-16", "[-1.6540002686363373, 1.6540002686363373]")),
("sineOrder3", ("1.2254703612493457e-15", "[-1.909859317102744, 1.909859317102744]")),
......@@ -58,40 +160,175 @@ class AbsErrorAnalysisRegressionTest extends FunSuite {
("carbonGas", ("3.983524363087597e-08", "[-6856426.768, 3.159230584E7]")),
("turbine1", ("9.601020280849505e-14", "[-55.55054339020381, 38.36885388122605]")),
("turbine2", ("1.4113902525335888e-13", "[-80.18793076923077, 63.665174692307694]")),
("turbine3", ("7.183364461717313e-14", "[-27.227529265841437, 38.719203390203816]"))
)
("turbine3", ("7.183364461717313e-14", "[-27.227529265841437, 38.719203390203816]")),
("kepler0", ("9.063860773039779e-14", "[3.0664, 102.8708]")),
("kepler1", ("4.394038910504606e-13", "[-288.15184, 89.927712]")),
("kepler2", ("2.201971227577815e-12", "[-337.61856, 850.310096]")),
("himmilbeau", ("1.0000889005823412e-12", "[-775.0, 890.0]"))
)
val smtAA_Fixed32: Map[String, (String, String)] = Map(
("doppler", ("1.75791622644632e-06", "[-137.64316836703838, -0.02944244059231351]")),
("sine", ("3.350232349298144e-09", "[-1.0043283753002443, 1.0043283753002443]")),
("sineOrder3", ("6.536979105441602e-09", "[-1.0055351041384715, 1.0055351041384715]")),
("sqroot", ("3.998633478610562e-06", "[-334.7934013614431, 1.6171710207127035]")),
("bspline0", ("8.537123605701497e-10", "[0.0, 0.16666666666666666]")),
("bspline1", ("2.949188153689887e-09", "[0.16617838541666666, 0.6671549479166666]")),
("bspline2", ("2.599942188082592e-09", "[0.16666666666666666, 0.6668650309244791]")),
("bspline3", ("6.208817165548793e-10", "[-0.16666666666666666, 0.0]")),
("rigidBody1", ("1.3485550881126018e-06", "[-705.0, 705.0]")),
("rigidBody2", ("0.0001531802118132919", "[-56049.1667175293, 58740.0]")),
("verhulst", ("2.7762362769533775e-09", "[0.3640144188500088, 0.9473239405662036]")),
("predatorPrey", ("1.647071564900709e-09", "[0.03727705922396188, 0.33711264367110555]")),
("carbonGas", ("17.67125597003061", "[4301713.35625, 1.6740286809375E7]")),
("turbine1", ("4.799229183495741e-07", "[-18.536291471169722, -1.986569412987437]")),
("turbine2", ("5.570496496692077e-07", "[-28.564652726384942, 3.8296552477598733]")),
("turbine3", ("3.3413411173656214e-07", "[0.5626821330545027, 11.434005458108444]")),
("kepler0", ("3.8016587502569254e-07", "[20.802505677616598, 95.98217598131895]")),
("kepler1", ("1.7833888537937244e-06", "[-278.40975267291554, -31.98171302891623]")),
("kepler2", ("9.42228436899577e-06", "[-645.8671575, 1288.34451875]")),
("himmilbeau", ("4.194676880030224e-06", "[-0.1416015625, 890.0]"))
)
val smtAA: Map[String, (String, String)] = Map(
val smtAA_Float32: Map[String, (String, String)] = Map(
("doppler", ("0.0002250138141196529", "[-137.64316836703838, -0.02944244059231351]")),
("sine", ("3.7318322294440997e-07", "[-1.0043283753002443, 1.0043283753002443]")),
("sineOrder3", ("6.579194264554884e-07", "[-1.0055351041384715, 1.0055351041384715]")),
("sqroot", ("0.000165820131940109", "[-334.7934013614431, 1.6171710207127035]")),
("bspline0", ("8.69234485871102e-08", "[0.0, 0.16666666666666666]")),
("bspline1", ("3.774960957159124e-07", "[0.16617838541666666, 0.6671549479166666]")),
("bspline2", ("3.3030908319631186e-07", "[0.16666666666666666, 0.6668650309244791]")),
("bspline3", ("5.712112027822517e-08", "[-0.16666666666666666, 0.0]")),
("rigidBody1", ("0.00017261505240639963", "[-705.0, 705.0]")),
("rigidBody2", ("0.01960706761337861", "[-56049.1667175293, 58740.0]")),
("verhulst", ("2.901506123777844e-07", "[0.3640144188500088, 0.9473239405662036]")),
("predatorPrey", ("1.3291118406629398e-07", "[0.03727705922396188, 0.33711264367110555]")),
("carbonGas", ("19.995233482473232", "[4301713.35625, 1.6740286809375E7]")),
("turbine1", ("4.7612433130717006e-05", "[-18.536291471169722, -1.986569412987437]")),
("turbine2", ("6.609932439930116e-05", "[-28.564652726384942, 3.8296552477598733]")),
("turbine3", ("3.367906049203724e-05", "[0.5626821330545027, 11.434005458108444]")),
("kepler0", ("4.866123310307557e-05", "[20.802505677616598, 95.98217598131895]")),
("kepler1", ("0.00021301499593723758", "[-248.33198742510353, -31.775362835450746]")),
("kepler2", ("0.0012060524690583414", "[-645.8671575, 1288.34451875]")),
("himmilbeau", ("0.0005369187050519044", "[-0.1416015625, 890.0]"))
)
val smtAA_Float64: Map[String, (String, String)] = Map(
("doppler", ("4.1911988101104756e-13", "[-137.64316836703838, -0.02944244059231351]")),
("sine", ("7.410949021433787e-16", "[-1.0043283753002443, 1.0043283753002443]")),
("sineOrder3", ("1.3400508287924788e-15", "[-1.0055351041384715, 1.0055351041384715]")),
("sqroot", ("3.208544541166703e-13", "[-334.7934013614431, 1.6171710207127035]")),
("sine", ("6.951079086011496e-16", "[-1.0043283753002443, 1.0043283753002443]")),
("sineOrder3", ("1.2254703612493457e-15", "[-1.0055351041384715, 1.0055351041384715]")),
("sqroot", ("3.088640454507186e-13", "[-334.7934013614431, 1.6171710207127035]")),
("bspline0", ("1.6190752442450204e-16", "[0.0, 0.16666666666666666]")),
("bspline1", ("8.141635513917815e-16", "[0.16617838541666666, 0.6671549479166666]")),
("bspline2", ("7.262708952756233e-16", "[0.16666666666666666, 0.6668650309244791]")),
("bspline1", ("7.031412489292659e-16", "[0.16617838541666666, 0.6671549479166666]")),
("bspline2", ("6.152485928131076e-16", "[0.16666666666666666, 0.6668650309244791]")),
("bspline3", ("1.0639637319324417e-16", "[-0.16666666666666666, 0.0]")),
("rigidBody1", ("3.2152058793144533e-13", "[-705.0, 705.0]")),
("rigidBody2", ("3.652100843964945e-11", "[-56049.1667175293, 58740.0]")),
("verhulst", ("5.741159583498406e-16", "[0.3640144188500088, 0.9473239405662036]")),
("predatorPrey", ("2.511128651395663e-16", "[0.03727705922396188, 0.33711264367110555]")),
("verhulst", ("5.404475598160268e-16", "[0.3640144188500088, 0.9473239405662036]")),
("predatorPrey", ("2.4756633989832674e-16", "[0.03727705922396188, 0.33711264367110555]")),
("carbonGas", ("3.7244002681234605e-08", "[4301713.35625, 1.6740286809375E7]")),
("turbine1", ("9.140869202455534e-14", "[-18.536291471169722, -1.986569412987437]")),
("turbine2", ("1.285668665546453e-13", "[-28.564652726384942, 3.8296552477598733]")),
("turbine3", ("6.545577699383315e-14", "[0.5626821330545027, 11.434005458108444]"))
("turbine1", ("8.868501650477874e-14", "[-18.536291471169722, -1.986569412987437]")),
("turbine2", ("1.231195155150921e-13", "[-28.564652726384942, 3.8296552477598733]")),
("turbine3", ("6.273210147405655e-14", "[0.5626821330545027, 11.434005458108444]")),
("kepler0", ("9.063860773039779e-14", "[20.802505677616598, 95.98217598131895]")),
("kepler1", ("4.251930363352586e-13", "[-278.40975267291554, -31.96861380296662]")),
("kepler2", ("2.2464476501227186e-12", "[-645.8671575, 1288.34451875]")),
("himmilbeau", ("1.0000889005823412e-12", "[-0.1416015625, 890.0]"))
)
test("interval-affine") {
test("warm-up: interval-affine") {
val ctx = context.copy(options=Seq(ChoiceOption("rangeMethod", "interval")))
val (_, program) = pipeline.run(ctx, inputPrg.deepCopy)
ctx.reporter.info("time taken (for all benchmarks): " + ctx.timers.analysis)
for (fnc <- program.defs) {
getLastExpression(fnc.body.get) match {
case x: NumAnnotation if x.hasError =>
val absError = x.absError
val range = x.interval
assert(intAA_Float64(fnc.id.toString)._1 === absError.toString, fnc.id)
assert(intAA_Float64(fnc.id.toString)._2 === range.toString, fnc.id)
//println(s"${fnc.id} abs error: ${x.absError}", "${x.interval}")
// if there is no error, then this is a bug
case x: NumAnnotation =>
assert(false)
}
}
}
ignore("interval-interval") {
//TODO
}
test("interval-affine-fixed32") {
val ctx = context.copy(options=Seq(ChoiceOption("rangeMethod", "interval"),
ChoiceOption("precision", "Fixed32")))
val (_, program) = pipeline.run(ctx, inputPrg.deepCopy)
ctx.reporter.info("time taken (for all benchmarks): " + ctx.timers.analysis)
for (fnc <- program.defs) {
getLastExpression(fnc.body.get) match {
case x: NumAnnotation if x.hasError =>
val absError = x.absError
val range = x.interval
assert(intAA_Fixed32(fnc.id.toString)._1 === absError.toString, fnc.id)
assert(intAA_Fixed32(fnc.id.toString)._2 === range.toString, fnc.id)
//println(s"${fnc.id} abs error: ${x.absError}", "${x.interval}")
// if there is no error, then this is a bug
case x: NumAnnotation =>
assert(false)
}
}
}
test("interval-affine-float32") {
val ctx = context.copy(options=Seq(ChoiceOption("rangeMethod", "interval"),
ChoiceOption("precision", "Float32")))
val (_, program) = pipeline.run(ctx, inputPrg.deepCopy)
ctx.reporter.info("time taken (for all benchmarks): " + ctx.timers.analysis)
for (fnc <- program.defs) {
getLastExpression(fnc.body.get) match {
case x: NumAnnotation if x.hasError =>
val absError = x.absError
val range = x.interval
assert(intAA_Float32(fnc.id.toString)._1 === absError.toString, fnc.id)
assert(intAA_Float32(fnc.id.toString)._2 === range.toString, fnc.id)
//println(s"${fnc.id} abs error: ${x.absError}", "${x.interval}")
// if there is no error, then this is a bug
case x: NumAnnotation =>
assert(false)
}
}
}
test("interval-affine-float64") {
val ctx = context.copy(options=Seq(ChoiceOption("rangeMethod", "interval"),
ChoiceOption("precision", "Float64")))
val (_, program) = pipeline.run(ctx, inputPrg.deepCopy)
ctx.reporter.info("time taken (for all benchmarks): " + ctx.timers.analysis)
for (fnc <- program.defs) {
getLastExpression(fnc.body.get) match {
case x: NumAnnotation if x.hasError =>
val absError = x.absError
val range = x.interval
assert(intAA(fnc.id.toString)._1 === absError.toString, fnc.id)
assert(intAA(fnc.id.toString)._2 === range.toString, fnc.id)
//println(s"${fnc.id} abs error: ${x.absError}, range: ${x.interval}")
assert(intAA_Float64(fnc.id.toString)._1 === absError.toString, fnc.id)
assert(intAA_Float64(fnc.id.toString)._2 === range.toString, fnc.id)
//println(s"${fnc.id} abs error: ${x.absError}", "${x.interval}")
// if there is no error, then this is a bug
case x: NumAnnotation =>
......@@ -101,18 +338,20 @@ class AbsErrorAnalysisRegressionTest extends FunSuite {
}
test("affine-affine") {
val ctx = context.copy(options=Seq(ChoiceOption("rangeMethod", "affine")))
test("affine-affine-fixed32") {
val ctx = context.copy(options=Seq(ChoiceOption("rangeMethod", "affine"),
ChoiceOption("precision", "Fixed32")))
val (_, program) = pipeline.run(ctx, inputPrg.deepCopy)
ctx.reporter.info("time taken (for all benchmarks): " + ctx.timers.analysis)
for (fnc <- program.defs) {
getLastExpression(fnc.body.get) match {
case x: NumAnnotation if x.hasError =>
val absError = x.absError
val range = x.interval
assert(aaAA(fnc.id.toString)._1 === absError.toString, fnc.id)
assert(aaAA(fnc.id.toString)._2 === range.toString, fnc.id)
//println(s"${fnc.id} abs error: ${x.absError}, range: ${x.interval}")
assert(aaAA_Fixed32(fnc.id.toString)._1 === absError.toString, fnc.id)
assert(aaAA_Fixed32(fnc.id.toString)._2 === range.toString, fnc.id)
//println(s"${fnc.id} abs error: ${x.absError}", "${x.interval}")
// if there is no error, then this is a bug
case x: NumAnnotation =>
......@@ -121,28 +360,121 @@ class AbsErrorAnalysisRegressionTest extends FunSuite {
}
}
// TODO: there seems to be an issue with the classpath,
// we get a NullpointerException at Solver.scala, line 37
test("affine-affine-float32") {
val ctx = context.copy(options=Seq(ChoiceOption("rangeMethod", "affine"),
ChoiceOption("precision", "Float32")))
val (_, program) = pipeline.run(ctx, inputPrg.deepCopy)
ctx.reporter.info("time taken (for all benchmarks): " + ctx.timers.analysis)
for (fnc <- program.defs) {
getLastExpression(fnc.body.get) match {
case x: NumAnnotation if x.hasError =>
val absError = x.absError
val range = x.interval
assert(aaAA_Float32(fnc.id.toString)._1 === absError.toString, fnc.id)
assert(aaAA_Float32(fnc.id.toString)._2 === range.toString, fnc.id)
//println(s"${fnc.id} abs error: ${x.absError}", "${x.interval}")
// if there is no error, then this is a bug
case x: NumAnnotation =>
assert(false)
}
}
}
ignore("smt-affine") {
val ctx = context.copy(options=Seq(ChoiceOption("rangeMethod", "smt")))
test("affine-affine-float64") {
val ctx = context.copy(options=Seq(ChoiceOption("rangeMethod", "affine"),
ChoiceOption("precision", "Float64")))
val (_, program) = pipeline.run(ctx, inputPrg.deepCopy)
ctx.reporter.info("time taken (for all benchmarks): " + ctx.timers.analysis)
for (fnc <- program.defs) {
getLastExpression(fnc.body.get) match {
case x: NumAnnotation if x.hasError =>
val absError = x.absError
val range = x.interval
//assert(aaAA(fnc.id.toString)._1 === absError.toString)
//assert(aaAA(fnc.id.toString)._2 === range.toString)
//println(s"${fnc.id} abs error: ${x.absError}, range: ${x.interval}")
assert(aaAA_Float64(fnc.id.toString)._1 === absError.toString, fnc.id)
assert(aaAA_Float64(fnc.id.toString)._2 === range.toString, fnc.id)
//println(s"${fnc.id} abs error: ${x.absError}", "${x.interval}")
// if there is no error, then this is a bug
case x: NumAnnotation =>
assert(false)
}
}
}
test("smt-affine-fixed32") {
val ctx = context.copy(options=Seq(ChoiceOption("rangeMethod", "smt"),
ChoiceOption("precision", "Fixed32")))
val (_, program) = pipeline.run(ctx, inputPrg.deepCopy)
ctx.reporter.info("time taken (for all benchmarks): " + ctx.timers.analysis)
for (fnc <- program.defs) {
// kepler1 sometimes returns a different result, presumably because of a Z3 timeout
if (fnc.id.toString != "kepler1")
getLastExpression(fnc.body.get) match {
case x: NumAnnotation if x.hasError =>
val absError = x.absError
val range = x.interval
assert(smtAA_Fixed32(fnc.id.toString)._1 === absError.toString, fnc.id)
assert(smtAA_Fixed32(fnc.id.toString)._2 === range.toString, fnc.id)
//println(s"${fnc.id} abs error: ${x.absError}", "${x.interval}")
// if there is no error, then this is a bug
case x: NumAnnotation =>
}
}
}
test("smt-affine-float32") {
val ctx = context.copy(options=Seq(ChoiceOption("rangeMethod", "smt"),
ChoiceOption("precision", "Float32")))
val (_, program) = pipeline.run(ctx, inputPrg.deepCopy)
ctx.reporter.info("time taken (for all benchmarks): " + ctx.timers.analysis)
for (fnc <- program.defs) {
// kepler1 sometimes returns a different result, presumably because of a Z3 timeout
if (fnc.id.toString != "kepler1")
getLastExpression(fnc.body.get) match {
case x: NumAnnotation if x.hasError =>
val absError = x.absError
val range = x.interval
assert(smtAA_Float32(fnc.id.toString)._1 === absError.toString, fnc.id)