Adding a Viper plugin #2
Conversation
… line. Also added a rel(e, i) expression to refer to expression e in execution i, where i is 0 or 1.
| "-feature", // Warn on features that requires explicit import | ||
| "-Wunused", // Warn on unused imports | ||
| "-Ypatmat-exhaust-depth", "40", // Increase depth of pattern matching analysis | ||
| // "-Xfatal-warnings", // Treat Warnings as errors to guarantee code quality in future changes |
|
|
||
| override def typ: Type = exp.typ | ||
|
|
||
| override def verifyExtExp(): VerificationResult = ??? |
There was a problem hiding this comment.
Would be good to comment why this can be unimplemented or instead throw some error message.
| @@ -125,6 +125,21 @@ case class SIFLowExp(exp: Exp, comparator: Option[String] = None, typVarMap: Map | |||
| override val extensionIsPure: Boolean = exp.isPure | |||
| } | |||
|
|
|||
| case class SIFRelExp(exp: Exp, i: IntLit) | |||
There was a problem hiding this comment.
Are you using IntLit instead of Int so that Viper's rewriter is not breaking? Does it make sense to document this? Also, you should comment which index corresponds to which execution.
| p.copy(domains = newDomains, fields = newFields, functions = newFunctions, predicates = newPredicates, | ||
| val res = p.copy(domains = newDomains, fields = newFields, functions = newFunctions, predicates = newPredicates, | ||
| methods = newMethods)(p.pos, p.info, p.errT) | ||
| res |
| // License, v. 2.0. If a copy of the MPL was not distributed with this | ||
| // file, You can obtain one at http://mozilla.org/MPL/2.0/. | ||
| // | ||
| // Copyright (c) 2011-2020 ETH Zurich. |
| // License, v. 2.0. If a copy of the MPL was not distributed with this | ||
| // file, You can obtain one at http://mozilla.org/MPL/2.0/. | ||
| // | ||
| // Copyright (c) 2011-2020 ETH Zurich. |
| if (expected == TypeHelper.Bool) | ||
| None | ||
| else | ||
| Some(Seq(s"Expected type ${expected}, but got Bool")) |
There was a problem hiding this comment.
Just making sure that all error messages intentionally do not end with a period.
| override def beforeVerify(input: Program): Program = { | ||
| SIFExtendedTransformer.transform(input, false) | ||
| } |
There was a problem hiding this comment.
I am not familiar with how we deal with these things in plugins. To my knowledge, the plugin does not support magic wands or gotos jumping outside of loops. Should programs containing unsupported features cause a warning?
|
As expected using function get(v: Ref, idx: Int): Bool { true }
method t(r: Ref)
{ assert forall i: Int :: {get(rel(r,0), i)} get(rel(r,0), i) }Carbon: Silicon: |
SIFRelExp(e, i)expression that refers to the value of expressionein executioni, whereiis 0 or 1. @JonasAlaif asked for this.