Commit 1d6e6eb6 authored by Heiko Becker's avatar Heiko Becker
Browse files

Add SSA phase to certificate generation again and add support for let certificates

parent 939af786
......@@ -190,6 +190,7 @@ object Main {
backend.CodeGenerationPhase
} else if (ctx.findOption(optionValidators) != None) {
analysis.SpecsProcessingPhase andThen
transform.SSATransformerPhase andThen
analysis.RangeErrorPhase andThen
InfoPhase andThen
backend.CertificatePhase andThen
......
......@@ -56,7 +56,7 @@ object CertificatePhase extends DaisyPhase {
//First write the imports
val prelude = getPrelude(prv, "certificate_" + prg.id + "_" + fnc.id.toString)
//the definitions for the whole expression
val (theDefinitions, lastGenName) = getValues(theBody.get,reporter,prv)
val (theDefinitions, lastGenName) = getCmd(theBody.get,reporter,prv)
//generate the precondition
val (thePreconditionFunction, functionName) = getPrecondFunction(pre, reporter, prv)
//the analysis result function
......@@ -196,9 +196,12 @@ object CertificatePhase extends DaisyPhase {
}
private def getValues(e: Expr,reporter:Reporter,prv:String): (String, String) = {
if (expressionNames.contains(e)){
("",expressionNames(e))
}else{
} else {
e match {
case x @ Variable(id) =>
if (identifierNums.contains(id)){
......@@ -303,6 +306,44 @@ object CertificatePhase extends DaisyPhase {
}
}
private def getCmd (e: Expr,reporter:Reporter,prv:String): (String, String) = {
e match {
case e @ Let(x,exp,g) =>
//first compute expression AST
val (expDef, expName) = getValues (exp,reporter,prv)
//now allocate a new variable
val varId = nextFreshVariable()
identifierNums += (x -> varId)
val (varDef, varName) =
if (prv == "coq"){
coqVariable (x,varId,reporter)
}else{
hol4Variable (x, varId, reporter)
}
expressionNames += (Variable(x) -> varName)
//now recursively compute the command
val (cmdDef, cmdName) = getCmd (g, reporter,prv)
val letName = "Let"+varName+expName+cmdName
val letDef =
if (prv == "coq"){
s"Definition $letName := Let $varId $expName $cmdName.\n"
}else {
s"val ${letName}_def = Define `$letName = Let $varId $expName $cmdName`;\n"
}
(expDef + varDef + cmdDef + letDef, letName)
case e @ _ =>
//return statement necessary
val (expDef, expName) = getValues (e, reporter, prv)
val retName = s"Ret$expName"
if (prv == "coq"){
(expDef + s"Definition $retName := Ret $expName.\n", retName)
} else {
(expDef + s"val ${retName}_def = Define `$retName = Ret $expName`;\n", retName)
}
}
}
private def coqInterval(intv:(Rational,Rational)) :String =
intv match {
case (lowerBound, upperBound) =>
......@@ -377,62 +418,83 @@ object CertificatePhase extends DaisyPhase {
}
}
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], cont:String) :String =
{
//must be set TODO:Assert?
//since we already generated the AST, we can be sure to have generated the name
assert (expressionNames(e) != None)
val nameE = expressionNames(e)
//FIXME: Only happens for let Bindings!
val nameE = expressionNames.getOrElse(e,"FOO")
e match {
case x @ Variable(id) =>
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
"if expEqBool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ RealLiteral(r) =>
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
"if expEqBool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Plus(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = coqAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
"if expEqBool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Minus(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = coqAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
"if expEqBool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Times(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = coqAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
"if expEqBool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Division(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = coqAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
"if expEqBool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Let (y,exp, g) =>
val expFun = coqAbsEnv (exp, errorMap, rangeMap, cont)
val gFun = coqAbsEnv (g, errorMap, rangeMap, 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"( expEqBool e Var ${identifierNums(y)} )",
"(" + intvY + ", " + errY + ")",
cont)
case x @ _ =>
"" //TODO Can this happen?
}
......@@ -446,52 +508,69 @@ object CertificatePhase extends DaisyPhase {
case x @ Variable(id) =>
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ RealLiteral(r) =>
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Plus(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = hol4AbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Minus(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = hol4AbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Times(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = hol4AbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Division(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = hol4AbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Let (y,exp, g) =>
val expFun = coqAbsEnv (exp, errorMap, rangeMap, cont)
val gFun = coqAbsEnv (g, errorMap, rangeMap, 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"( e = Var ${identifierNums(y)} )",
"(" + intvY + ", " + errY + ")",
cont)
case x @ _ =>
"" //TODO Can this happen?
......@@ -564,7 +643,7 @@ object CertificatePhase extends DaisyPhase {
coqAbsEnv(e, errorMap, rangeMap, "((0#1,0#1),0#1)") + ".",
"absenv")
else if (prv == "hol4")
("val absenv_def = Define `absenv:analysisResult = \n\\e. \n" +
("val absenv_def = Define `\n absenv:analysisResult = \n\\e. \n" +
hol4AbsEnv(e, errorMap, rangeMap, "((0,1),1)") + "`;",
"absenv")
else
......@@ -574,11 +653,11 @@ object CertificatePhase extends DaisyPhase {
private def getComputeExpr (lastGenName:String, analysisResultName:String,precondName:String, prover:String) :String=
if (prover == "coq")
"Theorem ErrorBoundSound :\n CertificateChecker " + lastGenName + " " +
"Theorem ErrorBoundSound :\n CertificateCheckerCmd " + lastGenName + " " +
analysisResultName + " " + precondName + " = true.\n" +
"Proof.\n cbv; auto.\nQed."
else if (prover == "hol4")
"val _ = store_thm (\"ErrorBoundSound\",\n ``CertificateChecker " +
"val _ = store_thm (\"ErrorBoundSound\",\n ``CertificateCheckerCmd " +
lastGenName + " " + analysisResultName + " " + precondName + " = T``,\n EVAL_TAC);"
else
"DAISY_CONV CertificateChecker thePrecondition theRewrites `CertificateChecker " + lastGenName + " " + analysisResultName + " " + precondName + "`;;"
......
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