Potential bug in mixed-tuning settings

[alpylmz]

Hi, I am considering to use this library for my fixed-precision application. I was experimenting with some settings, and I guess I got an unexpected error. I'd really appreciate it if you can help.

My command is:
./daisy --mixed-tuning --rangeMethod=smt --apfixed --lang=C --precision=Fixed64 --choosePrecision=fixed "testcases/mixed-precision/my_cases/${file}.scala"

I have only one file, and one simple function.

object Sqrt {
def sqroot_32(x: Real): Real = {
require(x >= 0.0 && x < 1.0)
1.0 + 0.5*x
} ensuring(res => res +/- 1)
}

With these settings, I get the following error:

daisy.tools.OverflowException
at daisy.tools.FinitePrecision$Precision.absRoundoff(FinitePrecision.scala:20)
at daisy.tools.RoundoffEvaluators.$anonfun$evalRoundoff$3(RoundoffEvaluators.scala:163)
at daisy.tools.RoundoffEvaluators._computeNewError$1(RoundoffEvaluators.scala:171)
at daisy.tools.RoundoffEvaluators.computeNewError$1(RoundoffEvaluators.scala:163)
at daisy.tools.RoundoffEvaluators.$anonfun$evalRoundoff$5(RoundoffEvaluators.scala:526)
at daisy.utils.CachingMap.getOrAdd(CachingMap.scala:17)
at daisy.tools.RoundoffEvaluators.eval$1(RoundoffEvaluators.scala:180)
at daisy.tools.RoundoffEvaluators.$anonfun$evalRoundoff$5(RoundoffEvaluators.scala:471)
at daisy.utils.CachingMap.getOrAdd(CachingMap.scala:17)
at daisy.tools.RoundoffEvaluators.eval$1(RoundoffEvaluators.scala:180)
at daisy.tools.RoundoffEvaluators.$anonfun$evalRoundoff$5(RoundoffEvaluators.scala:482)
at daisy.utils.CachingMap.getOrAdd(CachingMap.scala:17)
at daisy.tools.RoundoffEvaluators.eval$1(RoundoffEvaluators.scala:180)
at daisy.tools.RoundoffEvaluators.$anonfun$evalRoundoff$5(RoundoffEvaluators.scala:482)
at daisy.utils.CachingMap.getOrAdd(CachingMap.scala:17)
at daisy.tools.RoundoffEvaluators.eval$1(RoundoffEvaluators.scala:180)
at daisy.tools.RoundoffEvaluators.evalRoundoff(RoundoffEvaluators.scala:547)
at daisy.tools.RoundoffEvaluators.evalRoundoff$(RoundoffEvaluators.scala:140)
at daisy.opt.MixedPrecisionOptimizationPhase$.evalRoundoff(MixedPrecisionOptimizationPhase.scala:32)
at daisy.opt.MixedPrecisionOptimizationPhase$.computeAbsError(MixedPrecisionOptimizationPhase.scala:241)
at daisy.opt.MixedPrecisionOptimizationPhase$.$anonfun$runPhase$16(MixedPrecisionOptimizationPhase.scala:145)
at daisy.opt.MixedPrecisionOptimizationPhase$.deltaDebug$1(MixedPrecisionOptimizationPhase.scala:397)
at daisy.opt.MixedPrecisionOptimizationPhase$.deltaDebug$1(MixedPrecisionOptimizationPhase.scala:460)
at daisy.opt.MixedPrecisionOptimizationPhase$.deltaDebuggingSearch(MixedPrecisionOptimizationPhase.scala:495)
at daisy.opt.MixedPrecisionOptimizationPhase$.$anonfun$runPhase$4(MixedPrecisionOptimizationPhase.scala:146)
at scala.collection.immutable.List.map(List.scala:246)
at scala.collection.immutable.List.map(List.scala:79)
at daisy.opt.MixedPrecisionOptimizationPhase$.$anonfun$runPhase$3(MixedPrecisionOptimizationPhase.scala:85)
at scala.collection.immutable.List.map(List.scala:246)
at scala.collection.immutable.List.map(List.scala:79)
at daisy.opt.MixedPrecisionOptimizationPhase$.runPhase(MixedPrecisionOptimizationPhase.scala:75)
at daisy.DaisyPhase.run(DaisyPhase.scala:28)
at daisy.DaisyPhase.run$(DaisyPhase.scala:24)
at daisy.opt.MixedPrecisionOptimizationPhase$.run(MixedPrecisionOptimizationPhase.scala:32)
at daisy.opt.MixedPrecisionOptimizationPhase$.run(MixedPrecisionOptimizationPhase.scala:32)
at daisy.Pipeline$$anon$1.run(Pipeline.scala:13)
at daisy.Pipeline$$anon$1.run(Pipeline.scala:13)
at daisy.Pipeline$$anon$1.run(Pipeline.scala:11)
at daisy.Main$.interfaceMain(Main.scala:171)
at daisy.Main$.main(Main.scala:212)
at daisy.Main.main(Main.scala)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(Method.java:498)
at scala.reflect.internal.util.ScalaClassLoader.$anonfun$run$2(ScalaClassLoader.scala:105)
at scala.reflect.internal.util.ScalaClassLoader.asContext(ScalaClassLoader.scala:40)
at scala.reflect.internal.util.ScalaClassLoader.asContext$(ScalaClassLoader.scala:37)
at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:130)
at scala.reflect.internal.util.ScalaClassLoader.run(ScalaClassLoader.scala:105)
at scala.reflect.internal.util.ScalaClassLoader.run$(ScalaClassLoader.scala:97)
at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:130)
at scala.tools.nsc.CommonRunner.run(ObjectRunner.scala:29)
at scala.tools.nsc.CommonRunner.run$(ObjectRunner.scala:28)
at scala.tools.nsc.ObjectRunner$.run(ObjectRunner.scala:43)
at scala.tools.nsc.CommonRunner.runAndCatch(ObjectRunner.scala:35)
at scala.tools.nsc.CommonRunner.runAndCatch$(ObjectRunner.scala:34)
at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:70)
at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:91)
at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:103)
at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:108)
at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

When I remove the mixed-tuning flag, everything seems to work okay. Is this expected behaviour?

[malyzajko]

Thank you for reporting!

This is indeed a bug. Mixed-precision tuning works if you choose a smaller error bound, e.g. with ensuring(res => res +/- 0.1) it works fine.

What is happening: Because the error bound of 1 is so loose, Daisy tries too small precisions, which then overflow. Of course, it would be nice if Daisy would catch this itself.

I will try to fix it, but I won't be able to do that before next week.

Btw. the --choosePrecision option will do nothing when you use --mixed-tuning; this option will choose a uniform precision. That is, you can skip it. (But I am also aware that the flags can be super confusing.)