Skip to content

GitLab

Commit b62b0ee7 authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix remaining bugs in CertificatePhase

parent 6af55eb9
Hide whitespace changes
Inline Side-by-side
Showing with 43 additions and 73 deletions
src/main/scala/daisy/Main.scala
View file @ b62b0ee7
......@@ -165,23 +165,31 @@ object Main {
pipeline >>= analysis.SpecsProcessingPhase
if (ctx.hasFlag("rewrite")) {
pipeline >>= opt.RewritingOptimizationPhase
}
(ctx.options.get("certificate")) match {
case x @ Some(_) =>
pipeline >>= ctx.option[DaisyPhase]("analysis")
pipeline >>= backend.CertificatePhase
case x @ _ =>
if (ctx.hasFlag("dynamic")) {
pipeline >>= analysis.DynamicPhase
pipeline >>= backend.InfoPhase
} else {
if (ctx.hasFlag("three-address") || (ctx.fixedPoint && ctx.hasFlag("codegen"))) {
pipeline >>= transform.TACTransformerPhase
if (ctx.hasFlag("rewrite")) {
pipeline >>= opt.RewritingOptimizationPhase
}
// TODO: this is very ugly
if (ctx.hasFlag("subdiv") && ctx.option[DaisyPhase]("analysis") == analysis.DataflowPhase) {
pipeline >>= analysis.DataflowSubdivisionPhase
if (ctx.hasFlag("dynamic")) {
pipeline >>= analysis.DynamicPhase
pipeline >>= backend.InfoPhase
} else {
pipeline >>= ctx.option[DaisyPhase]("analysis")
if (ctx.hasFlag("three-address") || (ctx.fixedPoint && ctx.hasFlag("codegen"))) {
pipeline >>= transform.TACTransformerPhase
}
// TODO: this is very ugly
if (ctx.hasFlag("subdiv") && ctx.option[DaisyPhase]("analysis") == analysis.DataflowPhase) {
pipeline >>= analysis.DataflowSubdivisionPhase
} else {
pipeline >>= ctx.option[DaisyPhase]("analysis")
}
}
pipeline >>= backend.InfoPhase
......
src/main/scala/daisy/backend/CertificatePhase.scala
View file @ b62b0ee7
......@@ -3,13 +3,11 @@ package backend
import scala.collection.immutable.Seq
import daisy.utils.{ScalaPrinter, PrettyPrinter}
import lang.Trees._
import lang.Types._
import lang.Identifiers._
import tools.{Interval, Rational}
import tools.FinitePrecision._
import analysis.SpecsProcessingPhase
import lang.Extractors.ArithOperator
import lang.TreeOps.allVariablesOf
......@@ -33,14 +31,14 @@ object CertificatePhase extends DaisyPhase {
//must be set when entering this phase --> should not crash
val prover = ctx.option[String]("certificate")
val errorMap = ctx.resultAbsoluteErrors
val rangeMap = ctx.resultRealRanges
//val errorMap = ctx.resultAbsoluteErrors
//val rangeMap = ctx.resultRealRanges
//val precisions = ctx.specMixedPrecisions
val constPrecision = Float64 //ctx.constantPrecision
val mixedPrecision: Boolean = ctx.option[Boolean]("mixedPrecision")
val mixedPrecision: Boolean = !(ctx.option[Option[String]]("mixed-precision") == "")
//The full certificate as a string
var fullCertificate = new StringBuilder();
val fullCertificate = new StringBuilder();
reporter.info(s"\nStarting $name")
......@@ -124,7 +122,7 @@ object CertificatePhase extends DaisyPhase {
if (prover == "coq")
"Require Import Daisy.CertificateChecker."
else if (prover == "hol4")
"open preamble DaisyTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory;\nopen simpLib realTheory realLib RealArith;\n\n" +
"open preamble DaisyTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory DaisyMapTheory;\nopen simpLib realTheory realLib RealArith;\n\n" +
"val _ = new_theory \"" + fname +"\";\n\n"
else
""
......@@ -150,11 +148,6 @@ object CertificatePhase extends DaisyPhase {
case _ => reporter.fatalError ("In precisionToString, unknown precision.")
}
}
private def ocamlVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
val theExpr = s"let ExpVar$vname${vname.globalId} = Var $id.\n"
(theExpr,s"ExpVar$vname${vname.globalId}")
}
private def coqVariable(vname: Identifier): (String, String) =
{
......@@ -548,7 +541,6 @@ object CertificatePhase extends DaisyPhase {
private def binaryDefVars (fnc: FunDef, precMap: Map[Identifier, Precision]): (String, String) =
{
val fName = fnc.id.toString
var theFunction = "GAMMA "
for (variable <- allVariablesOf(fnc.body.get)) {
//DVAR :: DCONST n :: MTYPE m
......@@ -558,27 +550,17 @@ object CertificatePhase extends DaisyPhase {
(theFunction, s"")
}
private def conditional (condition: String, thenC: String, elseC: String): String =
"if " + condition + "\n" +
"then " + thenC + "\n" +
"else " + elseC
private def coqAbsEnv (e: Expr, errorMap: Map[Expr, Rational], rangeMap: Map[Expr, Interval], precisions: Map[Identifier, Precision], cont: String): String =
{
// Let bindings do not have names, so these are a special case here:
e match {
case x @ Let (y, exp, g) =>
val prec = precisionToString(precisions(y))
val expFun = coqAbsEnv (exp, errorMap, rangeMap, precisions, cont)
val gFun = coqAbsEnv (g, errorMap, rangeMap, precisions, expFun)
val intvY = coqInterval((rangeMap(Variable(y)).xlo, rangeMap(Variable(y)).xhi))
val errY = errorMap(Variable(y)).toFractionString.replace("/", "#")
val nameY = expressionNames(Variable(y))
conditional (
s"( expEq e (Var Q ${identifierNums(y)}) )",
"(" + intvY + ", " + errY + ")",
gFun)
//val nameY = expressionNames(Variable(y))
s"DaisyMap.add (Var Q ${identifierNums(y)}) ($intvY, $errY ) ($gFun)"
case x @ _ =>
......@@ -621,10 +603,7 @@ object CertificatePhase extends DaisyPhase {
case x @ _ =>
reporter.fatalError(s"Unsupported operation $e while generating absenv")
}
conditional (
"( expEq e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
continuation)
s"DaisyMap.add $nameE ($intvE, $errE) ($continuation)"
}
}
......@@ -633,25 +612,12 @@ object CertificatePhase extends DaisyPhase {
e match {
case x @ Let (y, exp, g) =>
// val expFun = hol4AbsEnv (exp, errorMap, rangeMap, cont)
// val gFun = hol4AbsEnv (g, errorMap, rangeMap, expFun)
// val intvY = hol4Interval((rangeMap(Variable(y)).xlo, rangeMap(Variable(y)).xhi))
// val errY = errorMap(Variable (y)).toFractionString
// val nameY = expressionNames(Variable(y))
// conditional (
// s"( e = Var ${identifierNums(y)} )",
// "(" + intvY + ", " + errY + ")",
// gFun)
val prec = precisionToString(precisions(y))
val expFun = hol4AbsEnv (exp, errorMap, rangeMap, precisions, cont)
val gFun = hol4AbsEnv (g, errorMap, rangeMap, precisions, expFun)
val intvY = hol4Interval((rangeMap(Variable(y)).xlo, rangeMap(Variable(y)).xhi))
val errY = errorMap(Variable(y)).toFractionString
val nameY = expressionNames(Variable(y))
conditional (
s"( e = Var ${identifierNums(y)} )",
"(" + intvY + ", " + errY + ")",
gFun)
//val nameY = expressionNames(Variable(y))
s"DaisyMapTree_insert (Var ${identifierNums(y)}) ($intvY , $errY) ($gFun)"
case x @ _ =>
......@@ -690,14 +656,10 @@ object CertificatePhase extends DaisyPhase {
case x @ Downcast(e, t) =>
hol4AbsEnv (e, errorMap, rangeMap, precisions, cont)
case x @ _ =>
reporter.fatalError(s"Unsupported operation $e while generating absenv")
case x @ _ =>
reporter.fatalError(s"Unsupported operation $e while generating absenv")
}
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
continuation)
s"DaisyMapTree_insert $nameE ($intvE, $errE) ($continuation)"
}
}
......@@ -711,7 +673,7 @@ object CertificatePhase extends DaisyPhase {
val intvY = binaryInterval((rangeMap(Variable(y)).xlo, rangeMap(Variable(y)).xhi))
// should not be necessary: .replace("-","~")
val errY = errorMap(Variable (y)).toFractionString.replace("(","").replace(")","").replace("/","#")
val nameY = expressionNames(Variable(y))
//val nameY = expressionNames(Variable(y))
s"? Var ${identifierNums(y)} $intvY $errY $expFun $gFun"
case x @ _ =>
......@@ -760,12 +722,12 @@ object CertificatePhase extends DaisyPhase {
private def getAbsEnvDef(e: Expr, errorMap: Map[Expr, Rational], rangeMap: Map[Expr, Interval], precision: Map[Identifier, Precision], fName: String, prv: String): (String, String)=
if (prv == "coq")
(s"Definition absenv_${fName} :analysisResult := \nfun (e:exp Q) =>\n" +
coqAbsEnv(e, errorMap, rangeMap, precision, "((0#1,0#1),0#1)") + ".",
(s"Definition absenv_${fName} :analysisResult := \n" +
coqAbsEnv(e, errorMap, rangeMap, precision, "DaisyMap.empty (intv * error)") + ".",
s"absenv_${fName}")
else if (prv == "hol4")
(s"val absenv_${fName}_def = Define `\n absenv_${fName}:analysisResult = \n\\e. \n" +
hol4AbsEnv(e, errorMap, rangeMap, precision, "((0,1),1)") + "`;",
(s"val absenv_${fName}_def = Define `\n absenv_${fName}:analysisResult = \n" +
hol4AbsEnv(e, errorMap, rangeMap, precision, "DaisyMap_empty") + "`;",
s"absenv_${fName}")
else
("ABS " + binaryAbsEnv(e, errorMap, rangeMap, reporter), "")
......
src/main/scala/daisy/tools/FinitePrecision.scala
View file @ b62b0ee7
......@@ -124,8 +124,8 @@ object FinitePrecision {
// also potential error: math.ulp(float.minNormal)/2 = 0.0
override def _absRoundoff(i: Interval): Rational =
//TODO: Change if certification does not work
//Rational.fromDouble(math.ulp(1.0.floatValue)/2)*Rational.abs(r)
Rational.fromDouble(math.ulp(Math.nextUp(Interval.maxAbs(i).floatValue))) / Rational(2)
Rational.fromDouble(math.ulp(1.0.floatValue)/2)*Interval.maxAbs(i)
//Rational.fromDouble(math.ulp(Math.nextUp(Interval.maxAbs(i).floatValue))) / Rational(2)
}
case object Float64 extends FloatPrecision(64) with DenormalCheck {
......@@ -142,8 +142,8 @@ object FinitePrecision {
override def _absRoundoff(i: Interval): Rational =
//TODO change if certification broken
///Rational.fromDouble(math.ulp(1.0)/2)*Rational.abs(r)
Rational.fromDouble(math.ulp(Math.nextUp(Interval.maxAbs(i).doubleValue))) / Rational(2)
Rational.fromDouble(math.ulp(1.0)/2)*Interval.maxAbs(i)
//Rational.fromDouble(math.ulp(Math.nextUp(Interval.maxAbs(i).doubleValue))) / Rational(2)
}
......
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