Commit e2b3a688 authored by Heiko Becker's avatar Heiko Becker

Implement certificate construction

parent b8cdcecd
......@@ -180,13 +180,18 @@ object Main {
transform.SSATransformerPhase andThen
analysis.RangeErrorPhase andThen
InfoPhase andThen
backend.CertificatePhase andThen
backend.CodeGenerationPhase
} else if (ctx.hasFlag("codegen")) {
analysis.SpecsProcessingPhase andThen
analysis.RangeErrorPhase andThen
InfoPhase andThen
backend.CodeGenerationPhase
} else if (ctx.findOption(optionValidators) != None) {
analysis.SpecsProcessingPhase andThen
transform.SSATransformerPhase andThen
analysis.RangeErrorPhase andThen
InfoPhase andThen
backend.CertificatePhase
} else {
analysis.SpecsProcessingPhase andThen
analysis.RangeErrorPhase andThen
......@@ -194,4 +199,4 @@ object Main {
}
}
}
\ No newline at end of file
}
......@@ -13,14 +13,9 @@ object CertificatePhase extends DaisyPhase {
override val name = "Certificate Creation"
override val description = "Generates certificate for chosen theorem prover to check"
// TODO: have this generate C code
override val definedOptions: Set[CmdLineOptionDef[Any]] = Set(
FlagOptionDef("printToFile", "print generated code to file")
)
var identifierNums : Map [Identifier, Int] = Map[Identifier, Int] ()
implicit val debugSection = DebugSectionBackend
var identifierNums :Map [Identifier, Int] = Map[Identifier, Int] ()
var expressionNames :Map [Expr, String] = Map[Expr, String] ()
def run(ctx: Context, prg: Program): (Context, Program) = {
......@@ -50,12 +45,20 @@ object CertificatePhase extends DaisyPhase {
case Some(prv) =>
thePrecondition match {
case Some (pre) =>
//First write the imports
val prelude = getPrelude(prv)
val (thePreconditionFunction, functionName) = getPrecondFunction(pre, reporter, prv)
//the definitions for the whole expression
val (theDefinitions, lastGenName) = getValues(theBody.get,reporter,prv)
val (analysisResultText, analysisResultName) = getAbsEnvDef(theBody.get, reporter, prv)
val functionCall = getComputeExpr(lastGenName,analysisResultName)
writeToFile(thePreconditionFunction + "\n" + theDefinitions,prv,fnc.id.toString)
//generate the precondition
val (thePreconditionFunction, functionName) = getPrecondFunction(pre, reporter, prv)
//the analysis result function
val (analysisResultText, analysisResultName) = getAbsEnvDef(theBody.get, prv)
//generate the final evaluation statement
val functionCall = getComputeExpr(lastGenName,analysisResultName,functionName,prv)
//compose the strings
val certificateText = prelude + "\n\n" + theDefinitions + "\n\n" + thePreconditionFunction + "\n" + analysisResultText + "\n\n" + functionCall
//write to the output file
writeToFile(certificateText,prv,fnc.id.toString)
case None => reporter.fatalError ("No Precondition specified")
}
case None => reporter.fatalError ("Failure")
......@@ -73,70 +76,23 @@ object CertificatePhase extends DaisyPhase {
private val nextConstantId = { var i = 0; () => { i += 1; i} }
private val nextFreshVariable = { var i = 0; () => { i += 1; i} }
private def getPrelude(prv:String) =
"ABC"
/* TOD: Make these tranlate the rationals to proper rationals in Coq, resp. HOL-Light */
private def coqPrecondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
{
var theFunction = "Definition thePrecondition:precond = fun (n:nat) ->\n"
for ((id,intv) <- ranges) {
intv match {
case (lowerBound, upperBound) =>
val freshBinder = nextFreshVariable()
identifierNums += (id -> freshBinder)
theFunction += "if n =? " + freshBinder + " then ("+lowerBound.toString + ","+upperBound.toString + ") else "
}
}
theFunction += "(0#0,0#0)."
(theFunction, "thePrecondition")
}
private def holPrecondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
{
var theFunction = "let thePrecondition = define ` \n thePrecondition (n:num) = \n"
for ((id,intv) <- ranges) {
intv match {
case (lowerBound, upperBound) =>
val freshBinder = nextFreshVariable()
identifierNums += (id -> freshBinder)
theFunction += "if n = " + freshBinder + " then ("+lowerBound.toString + ","+upperBound.toString + ") else "
}
}
theFunction += "(&0,&0)`;;"
(theFunction, "thePrecondition")
}
private def getPrecondFunction(pre:Expr,reporter:Reporter,prv:String) :(String,String) =
{
val (ranges, errors) = daisy.analysis.SpecsProcessingPhase.extractPreCondition(pre)
if (! errors.isEmpty){
reporter.fatalError("Errors on inputs are currently unsupported")
}
if (prv == "coq"){
coqPrecondition(ranges)
}else {
holPrecondition(ranges)
}
}
private def getAbsEnvDef (e:Expr,reporter:Reporter, prv:String) =
("ABC","ABC")
private def getComputeExpr (lastGenName:String, analysisResultName:String) =
"ABC"
private def getPrelude(prover:String) :String=
if (prover == "coq")
"Require Import Daisy.CertificateChecker."
else
"needs \"CertificateChecker.hl\";;"
private def coqVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
{
val theValue = s"Definition $vname :nat := $id.\n"
val theExpr = s"Definition ExpVar$vname :exp Q := Var Q $vname.\n"
val theExpr = s"Definition ExpVar$vname :exp Q := Param Q $vname.\n"
(theValue + theExpr,s"ExpVar$vname")
}
private def holVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
val theValue = s"let $vname = define `$vname:num = $id`;;\n"
val theExpr = s"let ExpVar$vname = define `ExpVar$vname:(real)exp = Var $vname`;;\n"
val theExpr = s"let ExpVar$vname = define `ExpVar$vname:(real)exp = Param $vname`;;\n"
(theValue + theExpr, s"ExpVar$vname")
}
......@@ -146,7 +102,7 @@ object CertificatePhase extends DaisyPhase {
val rationalStr = v.toString
val coqRational = rationalStr.replace('/','#')
val theValue = s"Definition cst$id :Q := ${coqRational}.\n"
val theExpr = s"Definition ExpCst$id :exp Q := Const cst$id\n"
val theExpr = s"Definition ExpCst$id :exp Q := Const cst$id.\n"
(theValue + theExpr, s"ExpCst$id")
}
......@@ -163,11 +119,14 @@ object CertificatePhase extends DaisyPhase {
private def coqBinOp (e: Expr, nameLHS:String, nameRHS:String, reporter:Reporter) :(String, String) =
e match {
case x @ Plus(lhs, rhs) =>
(s"Definition Plus$nameLHS$nameRHS :exp Q = Binop Plus $nameLHS $nameRHS.\n", "Plus$nameLHS$nameRHS")
("Definition Plus"+ nameLHS + nameRHS + s" :exp Q := Binop Plus $nameLHS $nameRHS.\n",
"Plus"+ nameLHS + nameRHS)
case x @ Minus(lhs, rhs) =>
(s"Definition Sub$nameLHS$nameRHS :exp Q = Binop Sub $nameLHS $nameRHS.\n", "Sub$nameLHS$nameRHS")
("Definition Sub"+ nameLHS + nameRHS + s" :exp Q := Binop Sub $nameLHS $nameRHS.\n",
"Sub"+ nameLHS + nameRHS)
case x @ Times(lhs, rhs) =>
(s"Definition Mul$nameLHS$nameRHS :exp Q = Binop Mult $nameLHS $nameRHS.\n", "Mult$nameLHS$nameRHS")
("Definition Mul"+ nameLHS + nameRHS + s" :exp Q := Binop Mult $nameLHS $nameRHS.\n",
"Mult"+ nameLHS + nameRHS)
case x @ _ =>
reporter.fatalError("Unsupported value")
}
......@@ -175,14 +134,14 @@ object CertificatePhase extends DaisyPhase {
private def holBinOp (e: Expr, nameLHS:String, nameRHS:String, reporter:Reporter) :(String, String) =
e match {
case x @ Plus(lhs, rhs) =>
(s"let Plus$nameLHS$nameRHS = define `Plus$nameLHS$nameRHS:(real)exp = Binop Plus $nameLHS $nameRHS`;;\n",
"Plus$nameLHS$nameRHS")
("let Plus"+ nameLHS + nameRHS + " = define `Plus"+ nameLHS + nameRHS + s":(real)exp = Binop Plus $nameLHS $nameRHS`;;\n",
"Plus"+ nameLHS + nameRHS)
case x @ Minus(lhs, rhs) =>
(s"let Sub$nameLHS$nameRHS = define `Sub$nameLHS$nameRHS:(real)exp = Binop Sub $nameLHS $nameRHS`;;\n",
"Sub$nameLHS$nameRHS")
("let Sub"+ nameLHS + nameRHS + " = define `Sub"+ nameLHS + nameRHS + s":(real)exp = Binop Sub $nameLHS $nameRHS`;;\n",
"Sub"+ nameLHS + nameRHS)
case x @ Times(lhs, rhs) =>
(s"let Mul$nameLHS$nameRHS = define `Mul$nameLHS$nameRHS:(real)exp = Binop Mult $nameLHS $nameRHS`;;\n",
"Mul$nameLHS$nameRHS")
("let Mul"+ nameLHS + nameRHS + " = define `Mul"+ nameLHS + nameRHS + s":(real)exp = Binop Mult $nameLHS $nameRHS`;;\n",
"Mul"+ nameLHS + nameRHS)
case x @ _ =>
reporter.fatalError("Unsupported value")
}
......@@ -190,57 +149,246 @@ object CertificatePhase extends DaisyPhase {
private def getValues(e: Expr,reporter:Reporter,prv:String): (String, String) = e match {
case x @ Variable(id) =>
// TODO: Make this use the global variable id map!
if (prv == "coq") {
coqVariable (id,nextFreshVariable(),reporter)
}else {
holVariable (id,nextFreshVariable(),reporter)
}
val varId =
if (identifierNums.contains(id))
identifierNums(id)
else{
val tmp = nextFreshVariable()
identifierNums += (id -> tmp)
tmp
}
val (definition,name) =
if (prv == "coq")
coqVariable (id,varId,reporter)
else
holVariable (id,varId,reporter)
expressionNames += (e -> name)
(definition,name)
case x @ RealLiteral(r) =>
if (prv == "coq") {
coqConstant (x,nextConstantId(),reporter)
}else {
holConstant (x,nextConstantId(),reporter)
}
//reporter.info(s"$x: ${x.interval},${x.absError}")
val (definition, name) =
if (prv == "coq")
coqConstant (x,nextConstantId(),reporter)
else
holConstant (x,nextConstantId(),reporter)
expressionNames += (e -> name)
(definition,name)
case x @ Plus(lhs, rhs) =>
val (lhsText, lhsName) = getValues(lhs,reporter,prv)
val (rhsText, rhsName) = getValues(rhs,reporter,prv)
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
val (definition, name) =
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
expressionNames += (e -> name)
(definition,name)
case x @ Minus(lhs, rhs) =>
val (lhsText, lhsName) = getValues(lhs,reporter,prv)
val (rhsText, rhsName) = getValues(rhs,reporter,prv)
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
val (definition, name) =
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
expressionNames += (e -> name)
(definition,name)
case x @ Times(lhs, rhs) =>
val (lhsText, lhsName) = getValues(lhs,reporter,prv)
val (rhsText, rhsName) = getValues(rhs,reporter,prv)
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
val (definition, name) =
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
expressionNames += (e -> name)
(definition,name)
case x @ _ =>
reporter.fatalError("Unsupported operation")
}
private def coqInterval(intv:(Rational,Rational)) :String =
intv match {
case (lowerBound, upperBound) =>
val lowerBoundCoq = lowerBound.toString.replace('/','#')
val upperBoundCoq = upperBound.toString.replace('/','#')
"( " + lowerBoundCoq + ", " + upperBoundCoq + ")"
}
private def holInterval(intv:(Rational,Rational)) :String =
intv match {
case (lowerBound, upperBound) =>
val lowerBoundHol = lowerBound.toString.replace("(","(&")
val upperBoundHol = upperBound.toString.replace("(","(&")
"( " + lowerBoundHol + ", " + upperBoundHol + ")"
}
private def coqPrecondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
{
var theFunction = "Definition thePrecondition:precond := fun (n:nat) =>\n"
for ((id,intv) <- ranges) {
val ivCoq = coqInterval (intv)
//variable must already have a binder here!
//TODO: assert it?
theFunction += "if n =? " + identifierNums(id) + " then "+ ivCoq + " else "
}
theFunction += "(0#1,0#1)."
(theFunction, "thePrecondition")
}
private def holPrecondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
{
var theFunction = "let thePrecondition = define ` \n thePrecondition (n:num) = \n"
for ((id,intv) <- ranges) {
val ivHol = holInterval(intv)
theFunction += "if n = " + identifierNums(id) + " then " + ivHol + " else "
}
theFunction += "(&0,&1)`;;"
(theFunction, "thePrecondition")
}
private def getPrecondFunction(pre:Expr,reporter:Reporter,prv:String) :(String,String) =
{
val (ranges, errors) = daisy.analysis.SpecsProcessingPhase.extractPreCondition(pre)
if (! errors.isEmpty){
reporter.fatalError("Errors on inputs are currently unsupported")
}
if (prv == "coq"){
coqPrecondition(ranges)
}else {
holPrecondition(ranges)
}
}
private def coqAbsEnv (e:Expr, cont:String) :String =
{
//must be set TODO:Assert?
val nameE = expressionNames(e)
e match {
case x @ Variable(id) =>
val intvE = coqInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toString.replace("/","#")
"if exp_eq_bool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
case x @ RealLiteral(r) =>
val intvE = coqInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toString.replace("/","#")
"if exp_eq_bool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
case x @ Plus(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, cont)
val rFun = coqAbsEnv (rhs, lFun)
val intvE = coqInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toString.replace("/","#")
"if exp_eq_bool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Minus(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, cont)
val rFun = coqAbsEnv (rhs, lFun)
val intvE = coqInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toString.replace("/","#")
"if exp_eq_bool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Times(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, cont)
val rFun = coqAbsEnv (rhs, lFun)
val intvE = coqInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toString.replace("/","#")
"if exp_eq_bool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ _ =>
"" //TODO Can this happen?
}
}
private def holAbsEnv (e:Expr, cont:String) :String =
{
//must be set TODO:Assert?
val nameE = expressionNames(e)
e match {
case x @ Variable(id) =>
val intvE = holInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
case x @ RealLiteral(r) =>
val intvE = holInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
case x @ Plus(lhs, rhs) =>
val lFun = holAbsEnv (lhs, cont)
val rFun = holAbsEnv (rhs, lFun)
val intvE = holInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Minus(lhs, rhs) =>
val lFun = holAbsEnv (lhs, cont)
val rFun = holAbsEnv (rhs, lFun)
val intvE = holInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Times(lhs, rhs) =>
val lFun = holAbsEnv (lhs, cont)
val rFun = holAbsEnv (rhs, lFun)
val intvE = holInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ _ =>
"" //TODO Can this happen?
}
}
private def getAbsEnvDef (e:Expr, prv:String) :(String,String)=
if (prv == "coq")
("Definition absenv :analysisResult := fun (e:exp Q) =>\n"+ coqAbsEnv(e, "((0#1,0#1),0#1)") + ".",
"absenv")
else
("let absenv = define `absenv:analysisResult = \n" + holAbsEnv(e, "((&0,&1),&1)") + "`;;",
"absenv")
private def getComputeExpr (lastGenName:String, analysisResultName:String,precondName:String, prover:String) :String=
if (prover == "coq")
"Eval compute in CertificateChecker " + lastGenName + " " + analysisResultName + " " + precondName + "."
else
"DEPTH_CONV `CertificateChecker " + lastGenName + " " + analysisResultName + " " + precondName + "`;;"
}
......@@ -27,7 +27,9 @@ trait ErrorFunctions {
var trackRoundoffErrs: Boolean = true
var attachToTree: Boolean = false
var dynamicSamplesDefault: Int = 100000
//FIXME: Why does this not compile without this?
//var defaultUniformPrecision: Precision = Float64
var uniformPrecision: Precision = Float64
var reporter: Reporter
val debugSection: DebugSection
......
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