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

Remove isExactinFloat check, since it is not supported in CC, make Downcast...

Remove isExactinFloat check, since it is not supported in CC, make Downcast error memoization explicit and add type casting function to certificate generation
parent faf90b7f
package daisy package daisy
package backend package backend
import scala.collection.immutable.Seq
import daisy.lang.{ScalaPrinter, PrettyPrinter} import daisy.lang.{ScalaPrinter, PrettyPrinter}
import lang.Trees._ import lang.Trees._
import lang.Types._ import lang.Types._
...@@ -8,6 +10,7 @@ import lang.Identifiers._ ...@@ -8,6 +10,7 @@ import lang.Identifiers._
import tools.{Interval, Rational} import tools.{Interval, Rational}
import tools.FinitePrecision._ import tools.FinitePrecision._
import analysis.SpecsProcessingPhase import analysis.SpecsProcessingPhase
import lang.Extractors.ArithOperator
import lang.TreeOps.allVariablesOf import lang.TreeOps.allVariablesOf
object CertificatePhase extends DaisyPhase { object CertificatePhase extends DaisyPhase {
...@@ -20,6 +23,7 @@ object CertificatePhase extends DaisyPhase { ...@@ -20,6 +23,7 @@ object CertificatePhase extends DaisyPhase {
//Map tracking which theorem prover name is associated with a subexpression //Map tracking which theorem prover name is associated with a subexpression
var expressionNames :Map [Expr, String] = Map[Expr, String] () var expressionNames :Map [Expr, String] = Map[Expr, String] ()
var reporter:Reporter = null var reporter:Reporter = null
val defaultPrecision = Float64
def run(ctx: Context, prg: Program): (Context, Program) = { def run(ctx: Context, prg: Program): (Context, Program) = {
...@@ -83,7 +87,7 @@ object CertificatePhase extends DaisyPhase { ...@@ -83,7 +87,7 @@ object CertificatePhase extends DaisyPhase {
//first retrieve the values //first retrieve the values
//these should be defined, otherwise the generation will fail //these should be defined, otherwise the generation will fail
val thePrecondition = fnc.precondition.get val thePrecondition = fnc.precondition.get
val theBody = fnc.body.get val theBody = (changeType (fnc.body.get, precisionMap))._1
val errorMap = ctx.intermediateAbsErrors.get(fnc.id).get val errorMap = ctx.intermediateAbsErrors.get(fnc.id).get
val rangeMap = ctx.intermediateRanges.get(fnc.id).get val rangeMap = ctx.intermediateRanges.get(fnc.id).get
...@@ -99,7 +103,7 @@ object CertificatePhase extends DaisyPhase { ...@@ -99,7 +103,7 @@ object CertificatePhase extends DaisyPhase {
//generate the final evaluation statement //generate the final evaluation statement
val functionCall = getComputeExpr(lastGenName, analysisResultName, functionName, defVarsName, fnc.id.toString, prover) val functionCall = getComputeExpr(lastGenName, analysisResultName, functionName, defVarsName, fnc.id.toString, prover)
//compose the strings and append to certificate //compose the strings and append to certificate
fullCertificate ++= theDefinitions + "\n\n" + thePreconditionFunction + "\n\n" + analysisResultText fullCertificate ++= theDefinitions + "\n\n" + defVars + "\n" + thePreconditionFunction + "\n\n" + analysisResultText
//spacing //spacing
fullCertificate ++= "\n\n" fullCertificate ++= "\n\n"
fullCertificate ++= functionCall fullCertificate ++= functionCall
...@@ -134,8 +138,8 @@ object CertificatePhase extends DaisyPhase { ...@@ -134,8 +138,8 @@ object CertificatePhase extends DaisyPhase {
p match { p match {
case Float32 => "M32" case Float32 => "M32"
case Float64 => "M64" case Float64 => "M64"
case DoubleDouble => "M128" // case DoubleDouble => "M128"
case QuadDouble => "M256" // case QuadDouble => "M256"
case _ => reporter.fatalError ("In precisionToString, unknown precision.") case _ => reporter.fatalError ("In precisionToString, unknown precision.")
} }
} }
...@@ -237,7 +241,7 @@ object CertificatePhase extends DaisyPhase { ...@@ -237,7 +241,7 @@ object CertificatePhase extends DaisyPhase {
s"UMin${nameOp}") s"UMin${nameOp}")
private def getValues(e: Expr, precisions: Map[Identifier, Precision], constPrecision: Precision, prv: String): (String, String) = { private def getValues(e: Expr, precisions: Map[Identifier, Precision], constPrecision: Precision, prv: String): (String, String) = {
reporter.info(s"$e\n\n")
//if the expression has already been defined before //if the expression has already been defined before
if (expressionNames.contains(e)){ if (expressionNames.contains(e)){
("", expressionNames(e)) ("", expressionNames(e))
...@@ -378,6 +382,7 @@ object CertificatePhase extends DaisyPhase { ...@@ -378,6 +382,7 @@ object CertificatePhase extends DaisyPhase {
} }
private def getCmd(e: Expr, precisions: Map[Identifier, Precision], constPrecision: Precision, prv: String): (String, String) = { private def getCmd(e: Expr, precisions: Map[Identifier, Precision], constPrecision: Precision, prv: String): (String, String) = {
reporter.info(s"$e\n")
e match { e match {
case e @ Let(x, exp, g) => case e @ Let(x, exp, g) =>
//first compute expression AST //first compute expression AST
...@@ -554,7 +559,9 @@ object CertificatePhase extends DaisyPhase { ...@@ -554,7 +559,9 @@ object CertificatePhase extends DaisyPhase {
val nameE = expressionNames(e) val nameE = expressionNames(e)
val intvE = coqInterval((rangeMap(x).xlo, rangeMap(x).xhi)) val intvE = e match{ case x @Downcast (e,t) => coqInterval((rangeMap(e).xlo, rangeMap(e).xhi))
case x @ _ => coqInterval ((rangeMap(x).xlo, rangeMap(x).xhi))}
val errE = errorMap(x).toFractionString.replace("/", "#") val errE = errorMap(x).toFractionString.replace("/", "#")
val continuation = val continuation =
...@@ -625,7 +632,9 @@ object CertificatePhase extends DaisyPhase { ...@@ -625,7 +632,9 @@ object CertificatePhase extends DaisyPhase {
val nameE = expressionNames(e) val nameE = expressionNames(e)
val intvE = hol4Interval((rangeMap(x).xlo, rangeMap(x).xhi)) val intvE = e match{ case x @Downcast (e,t) => hol4Interval((rangeMap(e).xlo, rangeMap(e).xhi))
case x @ _ => hol4Interval ((rangeMap(x).xlo, rangeMap(x).xhi))}
val errE = errorMap(x).toFractionString val errE = errorMap(x).toFractionString
val continuation = val continuation =
...@@ -684,7 +693,9 @@ object CertificatePhase extends DaisyPhase { ...@@ -684,7 +693,9 @@ object CertificatePhase extends DaisyPhase {
val nameE = expressionNames(e) val nameE = expressionNames(e)
val intvE = binaryInterval((rangeMap(x).xlo,rangeMap(x).xhi)) val intvE = e match{ case x @Downcast (e,t) => binaryInterval((rangeMap(e).xlo, rangeMap(e).xhi))
case x @ _ => binaryInterval ((rangeMap(x).xlo, rangeMap(x).xhi))}
val errE = errorMap(x).toFractionString.replace("(","").replace(")","").replace("/","#") val errE = errorMap(x).toFractionString.replace("(","").replace(")","").replace("/","#")
val continuation = val continuation =
...@@ -775,4 +786,40 @@ object CertificatePhase extends DaisyPhase { ...@@ -775,4 +786,40 @@ object CertificatePhase extends DaisyPhase {
else "" else ""
} }
def changeType(e: Expr, tpeMap: Map[Identifier, Precision]): (Expr, Precision) = e match {
case Variable(id) =>
// (Variable(id.changeType(FinitePrecisionType(tpeMap(id)))), tpeMap(id))
(e, tpeMap(id))
case x @ RealLiteral(r) =>
// val tmp = FinitePrecisionLiteral(r, defaultPrecision)
// tmp.stringValue = x.stringValue
(x, defaultPrecision)
case ArithOperator(Seq(l, r), recons) =>
val (eLeft, pLeft) = changeType(l, tpeMap)
val (eRight, pRight) = changeType(r, tpeMap)
val prec = getUpperBound(pLeft, pRight)
(recons(Seq(eLeft, eRight)), prec)
case ArithOperator(Seq(t), recons) =>
val (e, p) = changeType(t, tpeMap)
(recons(Seq(e)), p)
case Let(id, value, body) =>
val (eValue, valuePrec) = changeType(value, tpeMap)
val (eBody, bodyPrec) = changeType(body, tpeMap)
val idPrec = tpeMap(id)
if (idPrec >= valuePrec) {
(Let(id.changeType(FinitePrecisionType(tpeMap(id))), eValue, eBody), bodyPrec)
} else {
val newValue = Downcast(eValue, FinitePrecisionType(idPrec))
(Let(id.changeType(FinitePrecisionType(tpeMap(id))), newValue, eBody), bodyPrec)
}
}
} }
...@@ -7,6 +7,7 @@ import scala.collection.immutable.Seq ...@@ -7,6 +7,7 @@ import scala.collection.immutable.Seq
import lang.Trees._ import lang.Trees._
import lang.Identifiers._ import lang.Identifiers._
import lang.Types._
import lang.TreeOps.allVariablesOf import lang.TreeOps.allVariablesOf
import FinitePrecision._ import FinitePrecision._
import Rational.{min, abs, sqrtDown, one} import Rational.{min, abs, sqrtDown, one}
...@@ -150,11 +151,12 @@ trait RoundoffEvaluators extends RangeEvaluators { ...@@ -150,11 +151,12 @@ trait RoundoffEvaluators extends RangeEvaluators {
def eval(e: Expr, errorMap: Map[Identifier, T]): (T, Precision) = (e: @unchecked) match { def eval(e: Expr, errorMap: Map[Identifier, T]): (T, Precision) = (e: @unchecked) match {
case x @ RealLiteral(r) => case x @ RealLiteral(r) =>
val rndoff = if (isExactInFloats(r, constantsPrecision) || !trackRoundoffErrors) { val rndoff =
zeroError //if (isExactInFloats(r, constantsPrecision) || !trackRoundoffErrors) {
} else { //zeroError
//} else {
fromError(constantsPrecision.absRoundoff(r)) fromError(constantsPrecision.absRoundoff(r))
} //}
intermediateErrors += (x -> rndoff) intermediateErrors += (x -> rndoff)
(rndoff, constantsPrecision) (rndoff, constantsPrecision)
...@@ -269,11 +271,13 @@ trait RoundoffEvaluators extends RangeEvaluators { ...@@ -269,11 +271,13 @@ trait RoundoffEvaluators extends RangeEvaluators {
val idPrec = precisionMap(id) val idPrec = precisionMap(id)
val rndoff = if (idPrec < valuePrec) { // we need to cast down val rndoff = if (idPrec < valuePrec) { // we need to cast down
val valueRange = rangeMap(value) val valueRange = rangeMap(value)
computeNewError(valueRange, valueRndoff, idPrec) val err = computeNewError(valueRange, valueRndoff, idPrec)
val _ = intermediateErrors += (Downcast(value,FinitePrecisionType(idPrec)) -> err)
err
} else { } else {
valueRndoff valueRndoff
} }
intermediateErrors += (Variable(id) -> rndoff)
eval(body, errorMap + (id -> rndoff)) eval(body, errorMap + (id -> rndoff))
} }
......
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