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.)