Skip to content

GitLab

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

Start working on backend for certificate generation

parent 3e5c79e4
Hide whitespace changes
Inline Side-by-side
.gitignore
View file @ f480aff7
......@@ -6,6 +6,7 @@ hol/.ocamlinit
dmtcp*
ckpt*
hol/run_hol.sh
coq/_CoqProject
coq/*.glob
coq/*.vo
coq/.*
......
src/main/scala/daisy/analysis/AbsErrorPhase.scala
View file @ f480aff7
......@@ -98,7 +98,7 @@ object AbsErrorPhase extends DaisyPhase {
} else {
// do nothing to x (which may get us inconsistent state,
// if x has already attached error )
x // if x has already attached error )
if (x.hasError) reporter.warning("Node has errors attached," +
"but you are asking me to ignore them.")
else {
......
src/main/scala/daisy/backend/CertificatePhase.scala
View file @ f480aff7
......@@ -24,101 +24,92 @@ object CertificatePhase extends DaisyPhase {
val reporter = ctx.reporter
val proverToUse = ctx.findOption(Main.optionValidators)
/* Process relevant options */
//for (opt <- ctx.options) opt match {
// case ChoiceOption("verify",prover) =>
// val proverToUse = prover
//case _ => ;
//}
def writeToFile (fileContent:String, prover:String, fname:String){
import java.io.FileWriter
import java.io.BufferedWriter
val fileLocation = "./output/certificate_" + fname
val fstream =
if (prover == "coq")
new FileWriter(fileLocation + ".v")
else
new FileWriter(fileLocation + ".hl")
val out = new BufferedWriter(fstream)
out.write(fileContent)
out.close
}
for (fnc <- prg.defs) if (!fnc.precondition.isEmpty && !fnc.body.isEmpty){
reporter.info(s"Generating certificate for ${fnc.id}")
reporter.info(s"Generating certificate for $fnc.id}")
val thePrecondition = fnc.precondition
val theBody = fnc.body
proverToUse match {
case Some(prv) => getValues(theBody.get,reporter,prv)
case None => reporter.info ("Failure")
case Some(prv) =>
val (theDefinitions, lastGenName) = getValues(theBody.get,reporter,prv)
writeToFile(theDefinitions,prv,fnc.id.toString)
case None => reporter.fatalError ("Failure")
}
}
//generate definitions for "program"
//obtain analysis result from ctx?
//generate definitions for "program"
//generate abstract environment for analysis result
//def writeScalaFile(filename: String) {
// import java.io.FileWriter
// import java.io.BufferedWriter
// val fstream = new FileWriter(filename)
// val out = new BufferedWriter(fstream)
// out.write(ScalaPrinter.apply(prg))
// out.close
// }
//println(ScalaPrinter.apply(prg))
// if (printToFile){
// val fileLocation = "./output/" + prg.id + ".scala"
// ctx.reporter.info("Generated code: " + fileLocation)
// writeScalaFile(fileLocation)
// }
(ctx, prg)
}
private val nextConstantId = { var i = 0; () => { i += 1; i} }
private val nextFreshVariable = { var i = 0; () => { i += 1; i} }
private def coqVariable(vname:Identifier, id:Int, reporter:Reporter) :String =
private def coqVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
reporter.info (s"Definition $vname :nat := $id.")
reporter.info (s"Definition ExpVar$vname :exp Q := Var Q $vname")
s"ExpVar$vname"
val theValue = s"Definition $vname :nat := $id.\n"
val theExpr = s"Definition ExpVar$vname :exp Q := Var Q $vname.\n"
(theValue + theExpr,s"ExpVar$vname")
}
private def holVariable(vname:Identifier, id:Int, reporter:Reporter) :String =
private def holVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
reporter.info (s"let $vname:num = define `$vname = $id`;;")
reporter.info (s"let ExpVar$vname = define `ExpVar$vname = Var $vname`;;")
s"ExpVar$vname"
val theValue = s"let $vname:num = define `$vname = $id`;;\n"
val theExpr = s"let ExpVar$vname = define `ExpVar$vname = Var $vname`;;\n"
(theValue + theExpr, s"ExpVar$vname")
}
private def coqConstant(r:RealLiteral, id:Int, reporter:Reporter) :String =
private def coqConstant(r:RealLiteral, id:Int, reporter:Reporter) :(String, String) =
r match {
case RealLiteral(v) =>
val rationalStr = v.toString
val coqRational = rationalStr.replace('/','#')
reporter.info (s"Definition cst$id :Q := ${coqRational}.")
reporter.info (s"Definition ExpCst$id :exp Q := Const cst$id")
s"ExpCst$id"
val theValue = s"Definition cst$id :Q := ${coqRational}.\n"
val theExpr = s"Definition ExpCst$id :exp Q := Const cst$id\n"
(theValue + theExpr, s"ExpCst$id")
}
private def holConstant(r:RealLiteral, id:Int, reporter:Reporter) :String =
private def holConstant(r:RealLiteral, id:Int, reporter:Reporter) :(String, String) =
r match {
case RealLiteral(v) =>
val rationalStr = v.toString
val holRational = rationalStr.replace("(","(&")
reporter.info (s"let cst$id = define `cst$id:real = ${holRational}`;;")
reporter.info (s"let ExpCst$id = define `ExpCst$id:(real)exp = Const cst$id`;;")
s"ExpCst$id"
val theValue = s"let cst$id = define `cst$id:real = ${holRational}`;;\n"
val theExpr = s"let ExpCst$id = define `ExpCst$id:(real)exp = Const cst$id`;;\n"
(theValue + theExpr, s"ExpCst$id")
}
(* TODO *)
private def coqBinOp (e: Expr, nameLHS:String, nameRHS:String, reporter:Reporter) :String = e match {
case x @ Plus(lhs, rhs) =>
case x @ Minus(lhs, rhs) =>
case x @ Times(lhs, rhs) =>
case x @ _ =>
reporter.fatalError("Unsupported value")
}
/* TODO */
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")
case x @ Minus(lhs, rhs) =>
(s"Definition Sub$nameLHS$nameRHS :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")
case x @ _ =>
reporter.fatalError("Unsupported value")
}
private def getValues(e: Expr,reporter:Reporter,prv:String): String = e match {
private def getValues(e: Expr,reporter:Reporter,prv:String): (String, String) = e match {
case x @ Variable(id) =>
if (prv == "coq") {
......@@ -138,22 +129,34 @@ object CertificatePhase extends DaisyPhase {
//reporter.info(s"$x: ${x.interval},${x.absError}")
case x @ Plus(lhs, rhs) =>
val lhsName = getValues(lhs,reporter,prv)
val rhsName = getValues(rhs,reporter,prv)
reporter.info(s"$x: ${x.interval},${x.absError}")
"Plus"
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 {
("A","B")
}
case x @ Minus(lhs, rhs) =>
val lhsName = getValues(lhs,reporter,prv)
val rhsName = getValues(rhs,reporter,prv)
reporter.info(s"$x: ${x.interval},${x.absError}")
"Minus"
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 {
("A","B")
}
case x @ Times(lhs, rhs) =>
val lhsName = getValues(lhs,reporter,prv)
val rhsName = getValues(rhs,reporter,prv)
reporter.info(s"$x: ${x.interval},${x.absError}")
"Times"
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 {
("A","B")
}
case x @ _ =>
reporter.fatalError("Unsupported operation")
......
src/main/scala/daisy/utils/ErrorFunctions.scala
View file @ f480aff7
......@@ -382,7 +382,6 @@ trait ErrorFunctions {
val rightRangeInS = t2s(rangeRHS)
val propagatedError = leftRangeInS * errorRHS + rightRangeInS * errorLHS +
errorLHS*errorRHS
// new roundoff
val newError = computeNewError(range, propagatedError)
......
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