Skip to content

Commit da663c7

Browse files
jcp19jcp19
authored
Iota (#456)
* Hacky version * Hacky version * Major simplification * Cleanup * Fix bug * Refactoring stuff * Improve and cleanup * Reduce diff size * Reduce diff size * Add missing cases in case splits * Cleanup * Reduce diff size yet again * Reduce diff size yet again * add tests * add tests * Fix typos
1 parent 0b31ff9 commit da663c7

27 files changed

+271
-58
lines changed

‎src/main/scala/viper/gobra/ast/frontend/Ast.scala‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -140,7 +140,9 @@ sealed trait PCodeRootWithResult extends PCodeRoot {
140140
def result: PResult
141141
}
142142

143-
case class PConstDecl(typ: Option[PType], right: Vector[PExpression], left: Vector[PDefLikeId]) extends PActualMember with PActualStatement with PGhostifiableStatement with PGhostifiableMember with PDeclaration
143+
case class PConstDecl(specs: Vector[PConstSpec]) extends PActualMember with PActualStatement with PGhostifiableStatement with PGhostifiableMember with PDeclaration
144+
145+
case class PConstSpec(typ: Option[PType], right: Vector[PExpression], left: Vector[PDefLikeId]) extends PNode
144146

145147
case class PVarDecl(typ: Option[PType], right: Vector[PExpression], left: Vector[PDefLikeId], addressable: Vector[Boolean]) extends PActualMember with PActualStatement with PGhostifiableStatement with PGhostifiableMember with PDeclaration
146148

@@ -325,6 +327,8 @@ case class PBlankIdentifier() extends PAssignee
325327

326328
case class PNamedOperand(id: PIdnUse) extends PActualExpression with PActualType with PExpressionAndType with PAssignee with PLiteralType with PUnqualifiedTypeName with PNameOrDot
327329

330+
case class PIota() extends PActualExpression
331+
328332
sealed trait PLiteral extends PActualExpression
329333

330334
object PLiteral {

‎src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
4343
case n: PIfClause => showIfClause(n)
4444
case n: PExprSwitchClause => showExprSwitchClause(n)
4545
case n: PTypeSwitchClause => showTypeSwitchClause(n)
46+
case n: PConstSpec => showConstSpec(n)
4647
case n: PSelectClause => showSelectClause(n)
4748
case n: PStructClause => showStructClause(n)
4849
case n: PInterfaceClause => showInterfaceClause(n)
@@ -163,8 +164,13 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
163164
"var" <+> showList(left zip addressable){ case (v, a) => showAddressable(a, v) } <> opt(typ)(space <> showType(_)) <> rhs
164165
}
165166

166-
def showConstDecl(decl: PConstDecl): Doc = decl match {
167-
case PConstDecl(typ, right, left) => "const" <+> showIdList(left) <> opt(typ)(space <> showType(_)) <+> "=" <+> showExprList(right)
167+
def showConstDecl(decl: PConstDecl): Doc = {
168+
val lines = decl.specs.map(showConstSpec).foldLeft(emptyDoc)(_ <@> _)
169+
"const" <+> parens(nest(lines) <> line)
170+
}
171+
172+
def showConstSpec(spec: PConstSpec): Doc = spec match {
173+
case PConstSpec(typ, right, left) => showIdList(left) <> opt(typ)(space <> showType(_)) <+> "=" <+> showExprList(right)
168174
}
169175

170176
def showTypeDecl(decl: PTypeDecl): Doc = decl match {
@@ -447,6 +453,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
447453
case PShiftLeft(left, right) => showExpr(left) <+> "<<" <+> showExpr(right)
448454
case PShiftRight(left, right) => showExpr(left) <+> ">>" <+> showExpr(right)
449455
case PBitNegation(exp) => "^" <> showExpr(exp)
456+
case PIota() => "iota"
450457
}
451458
case expr: PGhostExpression => expr match {
452459
case POld(e) => "old" <> parens(showExpr(e))

‎src/main/scala/viper/gobra/frontend/Desugar.scala‎

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -377,7 +377,9 @@ object Desugar {
377377

378378
def varDeclGD(decl: PVarDecl): Vector[in.GlobalVarDecl] = ???
379379

380-
def constDeclD(decl: PConstDecl): Vector[in.GlobalConstDecl] = decl.left.flatMap(l => info.regular(l) match {
380+
def constDeclD(block: PConstDecl): Vector[in.GlobalConstDecl] = block.specs.flatMap(constSpecD)
381+
382+
def constSpecD(decl: PConstSpec): Vector[in.GlobalConstDecl] = decl.left.flatMap(l => info.regular(l) match {
381383
case sc@st.SingleConstant(_, id, _, _, _, _) =>
382384
val src = meta(id)
383385
val gVar = globalConstD(sc)(src)
@@ -394,12 +396,11 @@ object Desugar {
394396
case _ => ???
395397
}
396398
Vector(in.GlobalConstDecl(gVar, lit)(src))
397-
398-
// Constants defined with the blank identifier can be safely ignored as they
399-
// must be computable statically (and thus do not have side effects) and
400-
// they can never be read
401-
case st.Wildcard(_, _) => Vector()
402-
399+
case st.Wildcard(_, _) =>
400+
// Constants defined with the blank identifier can be safely ignored as they
401+
// must be computable statically (and thus do not have side effects) and
402+
// they can never be read
403+
Vector()
403404
case _ => ???
404405
})
405406

‎src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala‎

Lines changed: 38 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -378,7 +378,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
378378
*/
379379
override def visitResult(ctx: GobraParser.ResultContext): PResult = {
380380
super.visitResult(ctx) match {
381-
case res: Vector[Vector[PParameter]] => PResult(res.flatten).at(ctx)
381+
case res: Vector[Vector[PParameter]@unchecked] => PResult(res.flatten).at(ctx)
382382
case typ: PType => PResult(Vector(PUnnamedParameter(typ).at(typ))).at(ctx)
383383
}
384384
}
@@ -590,10 +590,34 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
590590
* {@link #visitChildren} on {@code ctx}.</p>
591591
*/
592592
override def visitConstDecl(ctx: GobraParser.ConstDeclContext): Vector[PConstDecl] = {
593-
visitListNode[PConstDecl](ctx.constSpec()) match {
594-
// Make sure the first expression list is not empty
595-
case Vector(PConstDecl(_, Vector(), _), _*) => fail(ctx)
596-
case decls => decls
593+
visitListNode[PConstSpec](ctx.constSpec()) match {
594+
case specs =>
595+
val expandedDecls = specs.zipWithIndex.map { case (spec, idx) =>
596+
// In constant declarations, whenever a type AND the init expression of a constant are not provided, the Go
597+
// compiler chooses the type and init expression of the previous constant which has either an initialization
598+
// expression or type. If an init expression cannot be found for a constant, Gobra reports an error during
599+
// type-checking, regardless of whether a type has been specified for it or not. This behavior mimics what
600+
// the Go compiler does.
601+
if (spec.right.isEmpty && spec.typ.isEmpty) {
602+
// When the type and init expression of a constant are not specified, we search for the latest constant C
603+
// (in declaration order) which has either a type or init expression. Then, we update the parsed node
604+
// of type PConstSpec node to contain a copy of both the type and the init expression of C. Doing so here
605+
// makes it easier to evaluate constant expressions that contain `iota`, as it allows us to infer from
606+
// context the intended value of `iota`. If we don't do this, the best we could do when evaluating an
607+
// expression containing `iota` would be to pass the intended value of `iota` as a param to the constant
608+
// evaluator, which requires significant refactoring of the type checker.
609+
val lastValidSpec = specs.take(idx).findLast(d => d.right.nonEmpty || d.typ.nonEmpty)
610+
val rhs = lastValidSpec match {
611+
case Some(s) => s.right.map(_.copy)
612+
case None => Vector()
613+
}
614+
val typ = lastValidSpec.flatMap(_.typ.map(_.copy))
615+
PConstSpec(typ = typ, left = spec.left, right = rhs).at(spec)
616+
} else {
617+
spec
618+
}
619+
}
620+
Vector(PConstDecl(expandedDecls))
597621
}
598622
}
599623

@@ -603,13 +627,13 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
603627
* <p>The default implementation returns the result of calling
604628
* {@link #visitChildren} on {@code ctx}.</p>
605629
*/
606-
override def visitConstSpec(ctx: GobraParser.ConstSpecContext): PConstDecl = {
630+
override def visitConstSpec(ctx: GobraParser.ConstSpecContext): PConstSpec = {
607631
val typ = if (ctx.type_() != null) Some(visitNode[PType](ctx.type_())) else None
608632

609633
val idnDefLikeList(left) = visitIdentifierList(ctx.identifierList())
610634
val right = visitExpressionList(ctx.expressionList())
611635

612-
PConstDecl(typ, right, left).at(ctx)
636+
PConstSpec(typ, right, left).at(ctx)
613637
}
614638

615639

@@ -723,9 +747,9 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
723747
}
724748

725749
override def visitSpecMember(ctx: SpecMemberContext): AnyRef = super.visitSpecMember(ctx) match {
726-
case Vector(spec : PFunctionSpec, (id: PIdnDef, args: Vector[PParameter], result: PResult, body: Option[(PBodyParameterInfo, PBlock)]))
750+
case Vector(spec : PFunctionSpec, (id: PIdnDef, args: Vector[PParameter@unchecked], result: PResult, body: Option[(PBodyParameterInfo, PBlock)@unchecked]))
727751
=> PFunctionDecl(id, args, result, spec, body)
728-
case Vector(spec : PFunctionSpec, (id: PIdnDef, receiver: PReceiver, args: Vector[PParameter], result: PResult, body: Option[(PBodyParameterInfo, PBlock)]))
752+
case Vector(spec : PFunctionSpec, (id: PIdnDef, receiver: PReceiver, args: Vector[PParameter@unchecked], result: PResult, body: Option[(PBodyParameterInfo, PBlock)@unchecked]))
729753
=> PMethodDecl(id, receiver, args, result, spec, body)
730754
}
731755

@@ -930,7 +954,10 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
930954
override def visitOperandName(ctx: GobraParser.OperandNameContext): PExpression = {
931955
visitChildren(ctx) match {
932956
case idnUseLike(id) => id match {
933-
case id@PIdnUse(_) => PNamedOperand(id).at(id)
957+
case id@PIdnUse(name) => name match {
958+
case "iota" => PIota().at(id)
959+
case _ => PNamedOperand(id).at(id)
960+
}
934961
case PWildcard() => PBlankIdentifier().at(ctx)
935962
case _ => unexpected(ctx)
936963
}
@@ -1244,7 +1271,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
12441271
*/
12451272
override def visitQuantification(ctx: QuantificationContext): AnyRef = super.visitQuantification(ctx) match {
12461273
case Vector(quantifier: String,
1247-
vars : Vector[PBoundVariable], ":", ":", triggers : Vector[PTrigger], body : PExpression) =>
1274+
vars : Vector[PBoundVariable@unchecked], ":", ":", triggers : Vector[PTrigger@unchecked], body : PExpression) =>
12481275
(quantifier match {
12491276
case "forall" => PForall
12501277
case "exists" => PExists

‎src/main/scala/viper/gobra/frontend/info/base/SymbolTable.scala‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -75,12 +75,12 @@ object SymbolTable extends Environments[Entity] {
7575
}
7676

7777
sealed trait Constant extends DataEntity {
78-
def decl: PConstDecl
78+
def decl: PConstSpec
7979
}
8080

8181
sealed trait ActualConstant extends Constant with ActualDataEntity
8282

83-
case class SingleConstant(decl: PConstDecl, idDef: PIdnDef, exp: PExpression, opt: Option[PType], ghost: Boolean, context: ExternalTypeInfo) extends ActualConstant {
83+
case class SingleConstant(decl: PConstSpec, idDef: PIdnDef, exp: PExpression, opt: Option[PType], ghost: Boolean, context: ExternalTypeInfo) extends ActualConstant {
8484
override def rep: PNode = decl
8585
}
8686

‎src/main/scala/viper/gobra/frontend/info/implementation/property/Addressability.scala‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,7 @@ trait Addressability extends BaseProperty { this: TypeInfoImpl =>
7575
case p => Violation.violation(s"Unexpected dot resolve, got $p")
7676
}
7777
case _: PLiteral => AddrMod.literal
78+
case _: PIota => AddrMod.iota
7879
case n: PInvoke => resolve(n) match {
7980
case Some(_: ap.Conversion) => AddrMod.conversionResult
8081
case Some(_: ap.FunctionCall) => AddrMod.callResult

‎src/main/scala/viper/gobra/frontend/info/implementation/property/Assignability.scala‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl =>
2222

2323
lazy val multiAssignableTo: Property[(Vector[Type], Vector[Type])] = createProperty[(Vector[Type], Vector[Type])] {
2424
case (right, left) =>
25-
StrictAssignModi(left.size, right.size) match {
25+
StrictAssignMode(left.size, right.size) match {
2626
case AssignMode.Single =>
2727
right match {
2828
// To support Go's function chaining when a tuple with the results of a function call are passed to the
@@ -50,7 +50,7 @@ trait Assignability extends BaseProperty { this: TypeInfoImpl =>
5050

5151
lazy val variadicAssignableTo: Property[(Vector[Type], Vector[Type])] = createProperty[(Vector[Type], Vector[Type])] {
5252
case (right, left) =>
53-
StrictAssignModi(left.size, right.size) match {
53+
StrictAssignMode(left.size, right.size) match {
5454
case AssignMode.Variadic => left.lastOption match {
5555
case Some(VariadicT(elem)) =>
5656
val dummyFill = UnknownType

‎src/main/scala/viper/gobra/frontend/info/implementation/property/ConstantEvaluation.scala‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -148,6 +148,16 @@ trait ConstantEvaluation { this: TypeInfoImpl =>
148148
case _ => None
149149
}
150150

151+
case p: PIota =>
152+
// obtains the intended value for iota from the context
153+
val res = for {
154+
constBlock <- enclosingPConstBlock(p)
155+
constClause <- enclosingPConstDecl(p)
156+
iota = constBlock.specs.indexOf(constClause)
157+
} yield BigInt(iota)
158+
violation(res.nonEmpty, "iota expression could not be found in a constant declaration")
159+
res
160+
151161
case _ => None
152162
}
153163

src/main/scala/viper/gobra/frontend/info/implementation/property/StrictAssignModi.scala renamed to src/main/scala/viper/gobra/frontend/info/implementation/property/StrictAssignMode.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ object AssignMode {
1515
case object Error extends AssignMode
1616
}
1717

18-
object StrictAssignModi {
18+
object StrictAssignMode {
1919
def apply(left: Int, right: Int): AssignMode =
2020
if (left > 0 && left == right) AssignMode.Single
2121
else if (left > right && right == 1) AssignMode.Multi
@@ -24,7 +24,7 @@ object StrictAssignModi {
2424
else AssignMode.Error
2525
}
2626

27-
object NonStrictAssignModi {
27+
object NonStrictAssignMode {
2828
def apply(left: Int, right: Int): AssignMode =
2929
if (left >= 0 && left == right) AssignMode.Single
3030
else if (left > right && right == 1) AssignMode.Multi

‎src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,12 @@ trait Enclosing { this: TypeInfoImpl =>
5454
lazy val enclosingStruct: PNode => Option[PStructType] =
5555
down[Option[PStructType]](None) { case x: PStructType => Some(x) }
5656

57+
lazy val enclosingPConstBlock: PNode => Option[PConstDecl] =
58+
down[Option[PConstDecl]](None) { case x: PConstDecl => Some(x) }
59+
60+
lazy val enclosingPConstDecl: PNode => Option[PConstSpec] =
61+
down[Option[PConstSpec]](None) { case x: PConstSpec => Some(x) }
62+
5763
def typeSwitchConstraints(id: PIdnNode): Vector[PExpressionOrType] =
5864
typeSwitchConstraintsLookup(id)(id)
5965

@@ -85,7 +91,7 @@ trait Enclosing { this: TypeInfoImpl =>
8591
def aux(n: PNode): Option[Type] = {
8692
n match {
8793
case tree.parent(p) => p match {
88-
case PConstDecl(t, _, _) => t.map(symbType)
94+
case PConstSpec(t, _, _) => t.map(symbType)
8995
case PVarDecl(t, _, _, _) => t.map(symbType)
9096
case _: PExpressionStmt => None
9197
case PSendStmt(channel, `n`) => Some(typ(channel).asInstanceOf[Type.ChannelT].elem)

0 commit comments

Comments
 (0)