CertificatePhase.scala 14.7 KB
Newer Older
1
2
3
4
5
6
7
8
package daisy
package backend

import daisy.lang.{ScalaPrinter, PrettyPrinter}
import lang.Trees._
import lang.Identifiers._
import lang.NumAnnotation
import utils.Interval._
9
10
import utils.Rational
import analysis.SpecsProcessingPhase
11
12
13
14
15
16

object CertificatePhase extends DaisyPhase {

  override val name = "Certificate Creation"
  override val description = "Generates certificate for chosen theorem prover to check"

17
18
  var identifierNums :Map [Identifier, Int] = Map[Identifier, Int] ()
  var expressionNames :Map [Expr, String] = Map[Expr, String] ()
19
20
21
22
23
24

  def run(ctx: Context, prg: Program): (Context, Program) = {

    val reporter = ctx.reporter
    val proverToUse = ctx.findOption(Main.optionValidators)

25
26
27
    def writeToFile (fileContent:String, prover:String, fname:String){
      import java.io.FileWriter
      import java.io.BufferedWriter
28
      val fileLocation =
29
        if (prover == "coq")
30
          "./coq/output/certificate_" + prg.id + "_" + fname + ".v"
31
        else
32
33
          "./hol/output/certificate_" + prg.id + "_" + fname + ".hl"
      val fstream = new FileWriter(fileLocation)
34
35
36
37
      val out = new BufferedWriter(fstream)
      out.write(fileContent)
      out.close
    }
38
39

    for (fnc <- prg.defs) if (!fnc.precondition.isEmpty && !fnc.body.isEmpty){
40
      reporter.info(s"Generating certificate for ${fnc.id}")
41
42
43
44
      val thePrecondition = fnc.precondition
      val theBody = fnc.body

      proverToUse match {
45
        case Some(prv) =>
46
47
          thePrecondition match {
            case Some (pre) =>
48
              //First write the imports
49
              val prelude = getPrelude(prv)
50
              //the definitions for the whole expression
51
              val (theDefinitions, lastGenName) = getValues(theBody.get,reporter,prv)
52
53
54
55
56
57
58
59
60
61
              //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)
62
63
            case None => reporter.fatalError ("No Precondition specified")
          }
64
        case None => reporter.fatalError ("Failure")
65
66
67
      }

    }
68
    //generate definitions for "program"
69
70
71
72
73
74
75
76
77
78

    //obtain analysis result from ctx?
    //generate abstract environment for analysis result

    (ctx, prg)
  }

  private val nextConstantId = { var i = 0; () => { i += 1; i} }
  private val nextFreshVariable = { var i = 0; () => { i += 1; i} }

79
80
81
82
83
  private def getPrelude(prover:String) :String=
    if (prover == "coq")
      "Require Import Daisy.CertificateChecker."
    else
      "needs \"CertificateChecker.hl\";;"
84

85
  private def coqVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
86
    {
87
      val theValue = s"Definition $vname :nat := $id.\n"
88
      val theExpr = s"Definition ExpVar$vname :exp Q := Param Q $vname.\n"
89
      (theValue + theExpr,s"ExpVar$vname")
90
91
    }

92
  private def holVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
93
    {
94
      val theValue = s"let $vname = define `$vname:num = $id`;;\n"
95
      val theExpr = s"let ExpVar$vname = define `ExpVar$vname:(real)exp = Param $vname`;;\n"
96
      (theValue + theExpr, s"ExpVar$vname")
97
98
    }

99
  private def coqConstant(r:RealLiteral, id:Int, reporter:Reporter) :(String, String) =
100
101
    r match {
      case RealLiteral(v) =>
Heiko Becker's avatar
Heiko Becker committed
102
        val rationalStr = v.toFractionString
103
        val coqRational = rationalStr.replace('/','#')
104
        val theValue = s"Definition cst$id :Q := ${coqRational}.\n"
105
        val theExpr = s"Definition ExpCst$id :exp Q := Const cst$id.\n"
106
        (theValue + theExpr, s"ExpCst$id")
107
108
    }

109
  private def holConstant(r:RealLiteral, id:Int, reporter:Reporter) :(String, String) =
110
111
    r match {
      case RealLiteral(v) =>
Heiko Becker's avatar
Heiko Becker committed
112
        val rationalStr = v.toFractionString
113
        val holRational = rationalStr.replace("(","(&")
114
115
116
        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")
117
118
    }

119
120
121
  private def coqBinOp (e: Expr, nameLHS:String, nameRHS:String, reporter:Reporter) :(String, String) =
    e match {
      case x @ Plus(lhs, rhs) =>
122
123
        ("Definition Plus"+ nameLHS + nameRHS + s" :exp Q := Binop Plus $nameLHS $nameRHS.\n",
          "Plus"+ nameLHS + nameRHS)
124
       case x @ Minus(lhs, rhs) =>
125
126
        ("Definition Sub"+ nameLHS + nameRHS + s" :exp Q := Binop Sub $nameLHS $nameRHS.\n",
          "Sub"+ nameLHS + nameRHS)
127
       case x @ Times(lhs, rhs) =>
Heiko Becker's avatar
Heiko Becker committed
128
        ("Definition Mult"+ nameLHS + nameRHS + s" :exp Q := Binop Mult $nameLHS $nameRHS.\n",
129
          "Mult"+ nameLHS + nameRHS)
130
131
132
       case x @ _ =>
       reporter.fatalError("Unsupported value")
    }
133

134
135
136
    private def holBinOp (e: Expr, nameLHS:String, nameRHS:String, reporter:Reporter) :(String, String) =
    e match {
      case x @ Plus(lhs, rhs) =>
137
138
        ("let Plus"+ nameLHS + nameRHS + " = define `Plus"+ nameLHS + nameRHS + s":(real)exp = Binop Plus $nameLHS $nameRHS`;;\n",
          "Plus"+ nameLHS + nameRHS)
139
      case x @ Minus(lhs, rhs) =>
140
141
        ("let Sub"+ nameLHS + nameRHS + " = define `Sub"+ nameLHS + nameRHS + s":(real)exp = Binop Sub $nameLHS $nameRHS`;;\n",
          "Sub"+ nameLHS + nameRHS)
142
      case x @ Times(lhs, rhs) =>
Heiko Becker's avatar
Heiko Becker committed
143
144
        ("let Mult"+ nameLHS + nameRHS + " = define `Mul"+ nameLHS + nameRHS + s":(real)exp = Binop Mult $nameLHS $nameRHS`;;\n",
          "Mult"+ nameLHS + nameRHS)
145
146
147
148
       case x @ _ =>
       reporter.fatalError("Unsupported value")
    }

149
  private def getValues(e: Expr,reporter:Reporter,prv:String): (String, String) = e match {
150
151

    case x @ Variable(id) =>
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
      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)
168
169

    case x @ RealLiteral(r) =>
170
171
172
173
174
175
176
      val (definition, name) =
        if (prv == "coq")
          coqConstant (x,nextConstantId(),reporter)
        else
          holConstant (x,nextConstantId(),reporter)
      expressionNames += (e -> name)
      (definition,name)
177
178

    case x @ Plus(lhs, rhs) =>
179
180
      val (lhsText, lhsName) = getValues(lhs,reporter,prv)
      val (rhsText, rhsName) = getValues(rhs,reporter,prv)
181
182
183
184
185
186
187
188
189
190
      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)
191
192

    case x @ Minus(lhs, rhs) =>
193
194
      val (lhsText, lhsName) = getValues(lhs,reporter,prv)
      val (rhsText, rhsName) = getValues(rhs,reporter,prv)
195
196
197
198
199
200
201
202
203
204
      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)
205
206

    case x @ Times(lhs, rhs) =>
207
208
      val (lhsText, lhsName) = getValues(lhs,reporter,prv)
      val (rhsText, rhsName) = getValues(rhs,reporter,prv)
209
210
211
212
213
214
215
216
217
218
      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)
219
220

    case x @ _ =>
Heiko Becker's avatar
Heiko Becker committed
221
      reporter.fatalError(s"Unsupported operation")
222
223
224

  }

225
226
227
228

  private def coqInterval(intv:(Rational,Rational)) :String =
    intv match {
      case (lowerBound, upperBound) =>
Heiko Becker's avatar
Heiko Becker committed
229
230
        val lowerBoundCoq = lowerBound.toFractionString.replace('/','#')
        val upperBoundCoq = upperBound.toFractionString.replace('/','#')
231
232
233
234
235
236
        "( " + lowerBoundCoq + ", " + upperBoundCoq + ")"
    }

  private def holInterval(intv:(Rational,Rational)) :String =
    intv match {
      case (lowerBound, upperBound) =>
Heiko Becker's avatar
Heiko Becker committed
237
238
        val lowerBoundHol = lowerBound.toFractionString.replace("(","(&")
        val upperBoundHol = upperBound.toFractionString.replace("(","(&")
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
        "( " + 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))
Heiko Becker's avatar
Heiko Becker committed
286
            val errE = x.absError.toFractionString.replace("/","#")
287
288
289
290
291
292
            "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))
Heiko Becker's avatar
Heiko Becker committed
293
          val errE = x.absError.toFractionString.replace("/","#")
294
295
296
297
298
299
300
301
          "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))
Heiko Becker's avatar
Heiko Becker committed
302
          val errE = x.absError.toFractionString.replace("/","#")
303
304
305
306
307
308
309
310
          "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))
Heiko Becker's avatar
Heiko Becker committed
311
          val errE = x.absError.toFractionString.replace("/","#")
312
313
314
315
316
317
318
319
          "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))
Heiko Becker's avatar
Heiko Becker committed
320
          val errE = x.absError.toFractionString.replace("/","#")
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
          "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))
Heiko Becker's avatar
Heiko Becker committed
337
          val errE = x.absError.toFractionString.replace("(","(&")
338
339
340
341
342
343
          "if e = " + nameE +
          " then (" + intvE + "," + errE + ")\n" +
          " else " + cont

        case x @ RealLiteral(r) =>
          val intvE = holInterval((x.interval.xlo,x.interval.xhi))
Heiko Becker's avatar
Heiko Becker committed
344
          val errE = x.absError.toFractionString.replace("(","(&")
345
346
347
348
349
350
351
352
          "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))
Heiko Becker's avatar
Heiko Becker committed
353
          val errE = x.absError.toFractionString.replace("(","(&")
354
355
356
357
358
359
360
361
          "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))
Heiko Becker's avatar
Heiko Becker committed
362
          val errE = x.absError.toFractionString.replace("(","(&")
363
364
365
366
367
368
369
370
          "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))
Heiko Becker's avatar
Heiko Becker committed
371
          val errE = x.absError.toFractionString.replace("(","(&")
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
          "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 + "`;;"
394
}