From 8cf2805e82dab10a61328e60a8e4779bd958d5f5 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 25 Feb 2022 12:45:21 +0100 Subject: [PATCH 01/50] Implement PAST nodes for ADT Declaration -Added a node for the declaration -Added a node for the constructors in the declarations body -Both nodes have high resemblance with the definitions for Domains --- .../standard/adt/AdtPASTExtension.scala | 44 +++++++++++++ .../plugin/standard/adt/AdtPlugin.scala | 62 +++++++++++++++++++ 2 files changed, 106 insertions(+) create mode 100644 src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala create mode 100644 src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala new file mode 100644 index 000000000..33fe9389b --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -0,0 +1,44 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// 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-2022 ETH Zurich. + +package viper.silver.plugin.standard.adt + +import viper.silver.ast.{Member, Position} +import viper.silver.parser.{NameAnalyser, PAnyFormalArgDecl, PExtender, PGlobalDeclaration, PIdnDef, PIdnUse, PMember, PNode, PTypeVarDecl, Translator, TypeChecker} + + +case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[PAdtConstructor])(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { + + override val getSubnodes: Seq[PNode] = Seq(idndef) ++ typVars ++ constructors + + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { + None + } + + // TODO: Implement + override def translateMemberSignature(t: Translator): Member = ??? + + // TODO: Implement + override def translateMember(t: Translator): Member = ??? +} + +case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])(val adtName: PIdnUse)(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { + + override val getSubnodes: Seq[PNode] = Seq(idndef) ++ formalArgs + + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { + None + } + + // TODO: Implement + override def translateMemberSignature(t: Translator): Member = ??? + + // TODO: Implement + override def translateMember(t: Translator): Member = ??? + +} + +case class PAdtConstructor1(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])(val pos: (Position, Position)) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala new file mode 100644 index 000000000..eed85c044 --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -0,0 +1,62 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// 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-2022 ETH Zurich. + +package viper.silver.plugin.standard.adt + +import fastparse._ +import viper.silver.parser.FastParser.{FP, anyFormalArgList, idndef, whitespace} +import viper.silver.parser.{PAnyFormalArgDecl, PIdnDef, PIdnUse, PTypeVarDecl, ParserExtension} +import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} + + +class AdtPlugin extends SilverPlugin with ParserPluginTemplate { + + /** + * Keyword used to define ADT's + */ + private val AdtKeyword: String = "adt" + + /** + * Parser for ADT declaration. + * + * Example of a List: + * + * adt List[T] { + * Nil() + * Cons(value: T, tail: List[T]) + * } + * + */ + def adtDecl[_: P]: P[PAdt] = FP(AdtKeyword ~/ idndef ~ ("[" ~ adtTypeVarDecl.rep(sep = ",") ~ "]").? ~ "{" ~ adtConstructorDecl.rep ~ + "}").map { + case (pos, (name, typparams, constructors)) => + PAdt( + name, + typparams.getOrElse(Nil), + constructors map (c => PAdtConstructor(c.idndef, c.formalArgs)(PIdnUse(name.name)(name.pos))(c.pos)))(pos) + } + + def adtTypeVarDecl[_: P]: P[PTypeVarDecl] = FP(idndef).map{ case (pos, i) => PTypeVarDecl(i)(pos) } + + def adtConstructorDecl[_: P]: P[PAdtConstructor1] = FP(adtConstructorSignature ~ ";".?).map { + case (pos, cdecl) => cdecl match { + case (name, formalArgs) => PAdtConstructor1(name, formalArgs)(pos) + } + } + + def adtConstructorSignature[_: P]: P[(PIdnDef, Seq[PAnyFormalArgDecl])] = P(idndef ~ "(" ~ anyFormalArgList ~ ")") + + override def beforeParse(input: String, isImported: Boolean): String = { + // Add new keyword + ParserExtension.addNewKeywords(Set[String](AdtKeyword)) + // Add new declaration + ParserExtension.addNewDeclAtEnd(adtDecl(_)) + // TODO: Add custom parsers + input + } + +} + From a726400b927a6d550b717e53e1a655b9bc0422b5 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 25 Feb 2022 12:45:21 +0100 Subject: [PATCH 02/50] Add AST nodes for ADT Declaration -Added an AST node for the declaration -Added an AST node for the constructors in the declarations body -Both nodes have high resemblance with the definitions for Domains --- .../plugin/standard/adt/AdtASTExtension.scala | 44 +++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala new file mode 100644 index 000000000..a899581ce --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala @@ -0,0 +1,44 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// 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-2022 ETH Zurich. + +package viper.silver.plugin.standard.adt + +import viper.silver.ast.{AnyLocalVarDecl, Declaration, ErrorTrafo, ExtensionMember, Info, LocalVarDecl, NoInfo, NoPosition, NoTrafos, Node, Position, TypeVar} + +/** + * This class represents a user-defined ADT. + * + * @param name name of the ADT + * @param constructors sequence of corresponding constructors + * @param typVars sequence of type variables (generics) + */ +case class Adt(name: String, constructors: Seq[AdtConstructor], typVars: Seq[TypeVar] = Nil) + (val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionMember { + val scopedDecls: Seq[Declaration] = Seq() + + override def extensionSubnodes: Seq[Node] = constructors ++ typVars +} + +/** + * This class represents an ADT constructor + * + * @param name name of the ADT constructor + * @param formalArgs sequence of arguments of the constructor + * @param adtName the name corresponding of the corresponding ADT + */ +case class AdtConstructor(name: String, formalArgs: Seq[AnyLocalVarDecl]) + (val pos: Position = NoPosition, val info: Info = NoInfo, val adtName : String, val errT: ErrorTrafo = NoTrafos) + extends ExtensionMember { + + override def getMetadata:Seq[Any] = { + Seq(pos, info, errT) + } + val scopedDecls: Seq[Declaration] = formalArgs.filter(p => p.isInstanceOf[LocalVarDecl]).asInstanceOf[Seq[LocalVarDecl]] + + override def extensionSubnodes: Seq[Node] = formalArgs +} + + From 8084defbe1f8f3a3e3911058173ee4f584d8da56 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 25 Feb 2022 12:45:21 +0100 Subject: [PATCH 03/50] Implement translation of ADT declaration and ADT constructors to AST Nodes -Note the ADT top-level declaration might be translated before its constructors, since we might need that information. We will handle this in a later step --- .../standard/adt/AdtPASTExtension.scala | 53 +++++++++++++++---- .../plugin/standard/adt/AdtPlugin.scala | 8 ++- 2 files changed, 50 insertions(+), 11 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 33fe9389b..3a1528f35 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -6,8 +6,9 @@ package viper.silver.plugin.standard.adt -import viper.silver.ast.{Member, Position} -import viper.silver.parser.{NameAnalyser, PAnyFormalArgDecl, PExtender, PGlobalDeclaration, PIdnDef, PIdnUse, PMember, PNode, PTypeVarDecl, Translator, TypeChecker} +import viper.silver.ast.{Member, NoInfo, Position, TypeVar} +import viper.silver.parser.{NameAnalyser, PAnyFormalArgDecl, PExtender, PGlobalDeclaration, PIdentifier, PIdnDef, PIdnUse, PMember, PNode, PTypeVarDecl, Translator, TypeChecker} +import viper.silver.plugin.standard.adt.PAdtConstructor.findAdtConstructor case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[PAdtConstructor])(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { @@ -15,14 +16,33 @@ case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[P override val getSubnodes: Seq[PNode] = Seq(idndef) ++ typVars ++ constructors override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { + // TODO: Implement type checking None } - // TODO: Implement - override def translateMemberSignature(t: Translator): Member = ??? + override def translateMemberSignature(t: Translator): Adt = { + Adt(idndef.name, null, typVars map (t => TypeVar(t.idndef.name)))(t.liftPos(this)) + } + + override def translateMember(t: Translator): Member = { + val a = PAdt.findAdt(idndef, t) + val aa = a.copy(constructors = constructors map (c => PAdtConstructor.findAdtConstructor(c.idndef, t)))(a.pos, a.info, a.errT) + t.getMembers()(a.name) = aa + aa + } + +} + +object PAdt { + /** + * This is a helper method helper that can be called if one knows which 'id' refers to an ADT + * + * @param id identifier of the ADT + * @param t translator unit + * @return the corresponding ADT object + */ + def findAdt(id: PIdentifier, t: Translator): Adt = t.getMembers()(id.name).asInstanceOf[Adt] - // TODO: Implement - override def translateMember(t: Translator): Member = ??? } case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])(val adtName: PIdnUse)(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { @@ -30,15 +50,28 @@ case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])( override val getSubnodes: Seq[PNode] = Seq(idndef) ++ formalArgs override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { + // TODO: Implement type checking None } - // TODO: Implement - override def translateMemberSignature(t: Translator): Member = ??? + override def translateMemberSignature(t: Translator): AdtConstructor = { + AdtConstructor(idndef.name, formalArgs map t.liftAnyVarDecl)(t.liftPos(this), NoInfo, adtName.name) + } - // TODO: Implement - override def translateMember(t: Translator): Member = ??? + override def translateMember(t: Translator): Member = { + findAdtConstructor(idndef, t) + } +} +object PAdtConstructor { + /** + * This is a helper method helper that can be called if one knows which 'id' refers to an ADTConstructor + * + * @param id identifier of the ADT constructor + * @param t translator unit + * @return the corresponding ADTConstructor object + */ + def findAdtConstructor(id: PIdentifier, t: Translator): AdtConstructor = t.getMembers()(id.name).asInstanceOf[AdtConstructor] } case class PAdtConstructor1(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])(val pos: (Position, Position)) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index eed85c044..168700ba0 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -8,7 +8,7 @@ package viper.silver.plugin.standard.adt import fastparse._ import viper.silver.parser.FastParser.{FP, anyFormalArgList, idndef, whitespace} -import viper.silver.parser.{PAnyFormalArgDecl, PIdnDef, PIdnUse, PTypeVarDecl, ParserExtension} +import viper.silver.parser.{PAnyFormalArgDecl, PIdnDef, PIdnUse, PProgram, PTypeVarDecl, ParserExtension} import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} @@ -58,5 +58,11 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { input } + override def beforeTranslate(input: PProgram): PProgram = { + // TODO: Implement translation to AST nodes + System.exit(-1) + input + } + } From a3d5c7a562b259e295c70e265fb7d0f887e3d36c Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 25 Feb 2022 12:45:21 +0100 Subject: [PATCH 04/50] Extend PAST with a new type for ADT's -As for the PDomainType we specify different kind of type. Namely Unresolved, Adt and Undeclared, which we need for resolving -Most of the implementation is borrowed from PDomainType, since they are similar --- .../standard/adt/AdtPASTExtension.scala | 53 ++++++++++++++++++- 1 file changed, 51 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 3a1528f35..5f103773a 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -6,8 +6,8 @@ package viper.silver.plugin.standard.adt -import viper.silver.ast.{Member, NoInfo, Position, TypeVar} -import viper.silver.parser.{NameAnalyser, PAnyFormalArgDecl, PExtender, PGlobalDeclaration, PIdentifier, PIdnDef, PIdnUse, PMember, PNode, PTypeVarDecl, Translator, TypeChecker} +import viper.silver.ast.{Member, NoInfo, NoPosition, Position, TypeVar} +import viper.silver.parser.{NameAnalyser, PAnyFormalArgDecl, PExtender, PGenericType, PGlobalDeclaration, PIdentifier, PIdnDef, PIdnUse, PMember, PNode, PType, PTypeSubstitution, PTypeVarDecl, Translator, TypeChecker} import viper.silver.plugin.standard.adt.PAdtConstructor.findAdtConstructor @@ -75,3 +75,52 @@ object PAdtConstructor { } case class PAdtConstructor1(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])(val pos: (Position, Position)) + +case class PAdtType(adt: PIdnUse, args: Seq[PType])(val pos: (Position, Position)) extends PExtender with PGenericType { + + var kind: PAdtTypeKinds.Kind = PAdtTypeKinds.Unresolved + + override def genericName: String = adt.name + + override def typeArguments: Seq[PType] = args + + override def isValidOrUndeclared: Boolean = (kind==PAdtTypeKinds.Adt || isUndeclared) && args.forall(_.isValidOrUndeclared) + + override def substitute(ts: PTypeSubstitution): PType = { + require(kind==PAdtTypeKinds.Adt || isUndeclared) + + val newArgs = args map (a=>a.substitute(ts)) + if (args==newArgs) + return this + + val newAdtType = PAdtType(adt,newArgs)((NoPosition, NoPosition)) + newAdtType.kind = PAdtTypeKinds.Adt + newAdtType + } + + override def getSubnodes(): Seq[PNode] = Seq(adt) ++ args + + def isResolved: Boolean = kind != PAdtTypeKinds.Unresolved + + def isUndeclared: Boolean = kind == PAdtTypeKinds.Undeclared + + override def subNodes: Seq[PType] = args + + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { + // TODO: Implement type checking + None + } + + // TODO: Implement signature translation + override def translateMemberSignature(t: Translator): Member = ??? + + // TODO: Implement translation + override def translateMember(t: Translator): Member = ??? +} + +object PAdtTypeKinds { + trait Kind + case object Unresolved extends Kind + case object Adt extends Kind + case object Undeclared extends Kind +} \ No newline at end of file From e0d78f65ea7c174f26600c451d7b448f45675724 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 25 Feb 2022 12:45:21 +0100 Subject: [PATCH 05/50] Properly implement the method withChildren for PAdtConstructor -As for PDomainFunction we have to make some adaptions to the method withChildren such that it can properly be used. (e.g needed if we use some StrategyBuilder) -Basically we have to make sure that 'adtName' is handled correctly -Currently, the only way it works, is with the Reflection approach. A simplified implementation is desired and provided in a later step --- .../standard/adt/AdtPASTExtension.scala | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 5f103773a..760622b8e 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -7,9 +7,11 @@ package viper.silver.plugin.standard.adt import viper.silver.ast.{Member, NoInfo, NoPosition, Position, TypeVar} +import viper.silver.parser.Transformer.ParseTreeDuplicationError import viper.silver.parser.{NameAnalyser, PAnyFormalArgDecl, PExtender, PGenericType, PGlobalDeclaration, PIdentifier, PIdnDef, PIdnUse, PMember, PNode, PType, PTypeSubstitution, PTypeVarDecl, Translator, TypeChecker} import viper.silver.plugin.standard.adt.PAdtConstructor.findAdtConstructor +import scala.reflect.runtime.{universe => reflection} case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[PAdtConstructor])(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { @@ -61,6 +63,50 @@ case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])( override def translateMember(t: Translator): Member = { findAdtConstructor(idndef, t) } + + override def withChildren(children: Seq[Any], pos: Option[(Position, Position)] = None, forceRewrite: Boolean = false): this.type = { + if (!forceRewrite && this.children == children && pos.isEmpty) + this + else { + + // TODO: Why can we not simplify with following code? => results in an Exception, is reflection really the only way? + /* + val first = children.head.asInstanceOf[PIdnDef] + val others = children.tail.asInstanceOf[Seq[PAnyFormalArgDecl]] + + + PAdtConstructor(first, others)(this.adtName)(pos.getOrElse(this.pos)).asInstanceOf[this.type] + */ + + // Infer constructor from type + val mirror = reflection.runtimeMirror(reflection.getClass.getClassLoader) + val instanceMirror = mirror.reflect(this) + val classSymbol = instanceMirror.symbol + val classMirror = mirror.reflectClass(classSymbol) + val constructorSymbol = instanceMirror.symbol.primaryConstructor.asMethod + val constructorMirror = classMirror.reflectConstructor(constructorSymbol) + + // Add additional arguments to constructor call, besides children + val firstArgList = children + var secondArgList = Seq.empty[Any] + + this match { + case pd: PAdtConstructor => secondArgList = Seq(pd.adtName) ++ Seq(pos.getOrElse(pd.pos)) + case _ => + } + + // Call constructor + val newNode = try { + constructorMirror(firstArgList ++ secondArgList: _*) + } + catch { + case _: Exception if this.isInstanceOf[PNode] => + throw ParseTreeDuplicationError(this.asInstanceOf[PNode], children) + } + + newNode.asInstanceOf[this.type] + } + } } object PAdtConstructor { From c35850580092603341eb3c1695d21272e3273896 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 25 Feb 2022 12:45:21 +0100 Subject: [PATCH 06/50] Translate PDomainType to PAdtType if necessary -Since the syntax of domain types is identical to the syntax of adt types they can not be distinguished, hence we translate each PDomainType to an PAdtDomain type if a corresponding ADT declaration exists -Currently we do this for occurences in signatures of functions, adt constructors and method. In later step we also need to do this for variable declarations, built-in type declarations, etc. --- .../plugin/standard/adt/AdtPlugin.scala | 26 +++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index 168700ba0..385338e0a 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -7,8 +7,9 @@ package viper.silver.plugin.standard.adt import fastparse._ +import viper.silver.ast.utility.rewriter.StrategyBuilder import viper.silver.parser.FastParser.{FP, anyFormalArgList, idndef, whitespace} -import viper.silver.parser.{PAnyFormalArgDecl, PIdnDef, PIdnUse, PProgram, PTypeVarDecl, ParserExtension} +import viper.silver.parser.{PAnyFormalArgDecl, PDomainType, PFormalArgDecl, PFunction, PIdnDef, PIdnUse, PMethod, PNode, PProgram, PTypeVarDecl, ParserExtension} import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} @@ -58,8 +59,29 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { input } + override def beforeResolve(input: PProgram): PProgram = { + // Replace PDomainType by PAdtType if a corresponding ADT exists, since they are automatically parsed as an PDomainType + // and there is no way to extend the parser to avoid this. + val declaredAdtNames = input.extensions.collect { case a: PAdt => a.idndef }.toSet + // TODO: With the current strategy occurrences of PDomainTypes in constructor, function and method signatures + // are handled (especially they are converted to an PAdtType if there is an corresponding declaration). + // Handling of AdtTypes in variable declarations, built-in type declarations, etc. must be implemented in a later step. + val newProgram: PProgram = StrategyBuilder.Slim[PNode]({ + case pa@PDomainType(idnuse, args) if declaredAdtNames.exists(_.name == idnuse.name) => PAdtType(idnuse, args)(pa.pos) + case d => d + }).recurseFunc({ + case PProgram(_, _, _, _, functions, _, methods, extensions, _) => Seq(extensions) ++ Seq(functions) ++ Seq(methods) + case PMethod(_, formalArgs, formalReturns, _, _, _) => Seq(formalArgs) ++ Seq(formalReturns) + case PFunction(_, formalArgs, typ, _, _, _) => Seq(formalArgs) ++ Seq(typ) + case PAdt(_, _, constructors) => Seq(constructors) + case PAdtConstructor(_, formalArgs) => Seq(formalArgs) + case PFormalArgDecl(_, typ) => Seq(typ) + }).execute(input) + newProgram + } + override def beforeTranslate(input: PProgram): PProgram = { - // TODO: Implement translation to AST nodes + // TODO: Finish the translation to AST nodes and remove the following statement System.exit(-1) input } From 48326cd56bc3445fb5fb4515c7f63a9f5a63e407 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 25 Feb 2022 12:45:21 +0100 Subject: [PATCH 07/50] Implement type-checking for ADT declaration, ADT constructors and ADT types -For ADT types we have to check if there is a corresponding declaration (this is currently redundant because we transform PDomainTypes to PAdtTypes only if there is a corresponding declaration, anyway this might change) -For ADT constructors we have to type check all its arguments -For ADT declarations we have to type check all its constructors --- .../standard/adt/AdtPASTExtension.scala | 34 ++++++++++++++++--- 1 file changed, 30 insertions(+), 4 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 760622b8e..d245e5122 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -18,7 +18,9 @@ case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[P override val getSubnodes: Seq[PNode] = Seq(idndef) ++ typVars ++ constructors override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { - // TODO: Implement type checking + t.checkMember(this) { + this.constructors foreach (_.typecheck(t, n)) + } None } @@ -52,7 +54,7 @@ case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])( override val getSubnodes: Seq[PNode] = Seq(idndef) ++ formalArgs override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { - // TODO: Implement type checking + this.formalArgs foreach (a => t.check(a.typ)) None } @@ -153,8 +155,32 @@ case class PAdtType(adt: PIdnUse, args: Seq[PType])(val pos: (Position, Position override def subNodes: Seq[PType] = args override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { - // TODO: Implement type checking - None + this match { + case at@PAdtType(_, _) if at.isResolved => None + /* Already resolved, nothing left to do */ + case at@PAdtType(adt, args) => + assert(!at.isResolved, "Only yet-unresolved adt types should be type-checked and resolved") + + args foreach t.check + + var x: Any = null + + try { + x = t.names.definition(t.curMember)(adt) + } catch { + case _: Throwable => + } + + x match { + case PAdt(_, typVars, _) => + t.ensure(args.length == typVars.length, this, "wrong number of type arguments") + at.kind = PAdtTypeKinds.Adt + None + case _ => + at.kind = PAdtTypeKinds.Undeclared + Option(Seq(s"found undeclared type ${at.adt.name}")) + } + } } // TODO: Implement signature translation From 9fc8beeb3e16695cc73c156e6d9dfc89544cea1b Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 25 Feb 2022 12:45:21 +0100 Subject: [PATCH 08/50] Add an AST node for the ADT type -Create a class for the ADT type that hold the necessary information we need in a later step to encode the ADT type as a domain type --- .../plugin/standard/adt/AdtASTExtension.scala | 38 ++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala index a899581ce..b912bc45b 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala @@ -6,7 +6,7 @@ package viper.silver.plugin.standard.adt -import viper.silver.ast.{AnyLocalVarDecl, Declaration, ErrorTrafo, ExtensionMember, Info, LocalVarDecl, NoInfo, NoPosition, NoTrafos, Node, Position, TypeVar} +import viper.silver.ast.{AnyLocalVarDecl, Declaration, ErrorTrafo, ExtensionMember, ExtensionType, Info, LocalVarDecl, NoInfo, NoPosition, NoTrafos, Node, Position, Type, TypeVar} /** * This class represents a user-defined ADT. @@ -41,4 +41,40 @@ case class AdtConstructor(name: String, formalArgs: Seq[AnyLocalVarDecl]) override def extensionSubnodes: Seq[Node] = formalArgs } +/** + * This class represents an user-defined ADT type. See also the companion object below, which allows passing a + * Adt - this should be used in general for creation (so that typeParameters is guaranteed to + * be set correctly) + * + * @param adtName The name of the underlying adt. + * @param partialTypVarsMap Maps type parameters to (possibly concrete) types. May not map all + * type parameters, may even be empty. + * @param typeParameters The type variables of the ADT type. + */ +case class AdtType(adtName: String, partialTypVarsMap: Map[TypeVar, Type]) + (val typeParameters: Seq[TypeVar]) extends ExtensionType { + + /** + * Map each type parameter `A` to `partialTypVarsMap(A)`, if defined, otherwise to `A` itself. + * `typVarsMap` thus contains a mapping for each type parameter. + */ + val typVarsMap: Map[TypeVar, Type] = + typeParameters.map(tp => tp -> partialTypVarsMap.getOrElse(tp, tp)).to(implicitly) + + /** + * Takes a mapping of type variables to types and substitutes all + * occurrences of those type variables with the corresponding type. + */ + override def substitute(typVarsMap: Map[TypeVar, Type]): Type = ??? + + /** Is this a concrete type (i.e. no uninstantiated type variables)? */ + override def isConcrete: Boolean = typVarsMap.values.forall(_.isConcrete) + +} + +object AdtType{ + def apply(adt: Adt, typVarsMap: Map[TypeVar, Type]): AdtType = + AdtType(adt.name, typVarsMap)(adt.typVars) +} + From 20b0ab9473018529846302fb7acf9aa86100e7f6 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Thu, 24 Feb 2022 16:19:09 +0100 Subject: [PATCH 09/50] Enhance PrettyPrinter -Handle ExtensionMember in showMember -Handle ExtensionType in showType -This enhancement allows the plugin developer to implement an own prettyPrint also for ExtensionMember and ExtensionType. Previusoly this was only possible for ExtensionStmt and ExtensionExp --- src/main/scala/viper/silver/ast/Program.scala | 3 ++- src/main/scala/viper/silver/ast/Type.scala | 2 ++ src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala | 7 ++++--- .../scala/viper/silver/plugin/ParserPluginTemplate.scala | 1 + 4 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala index 445f410e0..0bad5133e 100644 --- a/src/main/scala/viper/silver/ast/Program.scala +++ b/src/main/scala/viper/silver/ast/Program.scala @@ -6,7 +6,7 @@ package viper.silver.ast -import viper.silver.ast.pretty.{Fixity, Infix, LeftAssociative, NonAssociative, Prefix, RightAssociative} +import viper.silver.ast.pretty.{Fixity, Infix, LeftAssociative, NonAssociative, Prefix, PrettyPrintPrimitives, RightAssociative} import utility.{Consistency, DomainInstances, Nodes, Types, Visitor} import viper.silver.ast.MagicWandStructure.MagicWandStructure import viper.silver.ast.utility.rewriter.StrategyBuilder @@ -779,4 +779,5 @@ case class BackendFunc(name: String, smtName: String, override val typ: Type, ov */ trait ExtensionMember extends Member{ def extensionSubnodes: Seq[Node] + def prettyPrint: PrettyPrintPrimitives#Cont } diff --git a/src/main/scala/viper/silver/ast/Type.scala b/src/main/scala/viper/silver/ast/Type.scala index 0f58aaf87..28c1ed931 100644 --- a/src/main/scala/viper/silver/ast/Type.scala +++ b/src/main/scala/viper/silver/ast/Type.scala @@ -7,6 +7,7 @@ package viper.silver.ast import utility.Types +import viper.silver.ast.pretty.PrettyPrintPrimitives import viper.silver.verifier.ConsistencyError /** Silver types. */ @@ -203,4 +204,5 @@ case class BackendType(boogieName: String, smtName: String) extends AtomicType trait ExtensionType extends Type{ def getAstType: Type = ??? + def prettyPrint: PrettyPrintPrimitives#Cont = ??? } diff --git a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala index b34cb211f..d4337250f 100644 --- a/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala +++ b/src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala @@ -490,9 +490,9 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter /** Show a program. */ def showProgram(p: Program): Cont = { - val Program(domains, fields, functions, predicates, methods, _) = p + val Program(domains, fields, functions, predicates, methods, extensions) = p showComment(p) <@> - ssep((domains ++ fields ++ functions ++ predicates ++ methods) map show, line <> line) + ssep((domains ++ fields ++ functions ++ predicates ++ methods ++ extensions) map show, line <> line) } /** Show a domain member. */ @@ -564,7 +564,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter }) case d: Domain => showDomain(d) - case _:ExtensionMember => nil + case e:ExtensionMember => e.prettyPrint } showComment(m) <@> memberDoc } @@ -627,6 +627,7 @@ object FastPrettyPrinter extends FastPrettyPrinterBase with BracketPrettyPrinter text(domainName) <> (if (typArgs.isEmpty) nil else brackets(ssep(typArgs, char (',') <> space))) case BackendType(boogieName, _) if boogieName != null => boogieName case BackendType(_, smtName) => smtName + case et: ExtensionType => et.prettyPrint } } diff --git a/src/main/scala/viper/silver/plugin/ParserPluginTemplate.scala b/src/main/scala/viper/silver/plugin/ParserPluginTemplate.scala index ad0b4edaa..a9a0e27f7 100644 --- a/src/main/scala/viper/silver/plugin/ParserPluginTemplate.scala +++ b/src/main/scala/viper/silver/plugin/ParserPluginTemplate.scala @@ -125,6 +125,7 @@ trait ParserPluginTemplate { override def name: String = ??? override def errT: ErrorTrafo = ??? override def info: Info = ??? + override def prettyPrint: PrettyPrintPrimitives#Cont = ??? } /** From cbcd1d0595e7b8d8f224aa6dc484a822b3c80f51 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Thu, 24 Feb 2022 16:21:01 +0100 Subject: [PATCH 10/50] Change order of member signature translation -Observe that we need to translate the domain signatures first, since other members like domain functions, methods and ordinary functions might depend on the domain signatures -Signatures of extensions need to be treated similarly as domain signatures, as they might introduce a new top-level declaration that behaves similar as domains (e.g ADTs). Accordingly, their signatures must be translated before signatures of domain functions, methods, functions, etc. -Note that we translate extensions signatures after domain signatures since there might be extensions that work like methods and functions, and hence might need the domain signatures. --- src/main/scala/viper/silver/parser/Translator.scala | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala index 1f5348d4f..4ff4c2cbc 100644 --- a/src/main/scala/viper/silver/parser/Translator.scala +++ b/src/main/scala/viper/silver/parser/Translator.scala @@ -31,10 +31,12 @@ case class Translator(program: PProgram) { program match { case PProgram(_, _, pdomains, pfields, pfunctions, ppredicates, pmethods, pextensions, _) => - (pdomains ++ pfields ++ pfunctions ++ ppredicates ++ - pmethods ++ (pdomains flatMap (_.funcs))) foreach translateMemberSignature + pdomains foreach translateMemberSignature pextensions foreach translateMemberSignature + pdomains flatMap (_.funcs) foreach translateMemberSignature + (pfields ++ pfunctions ++ ppredicates ++ pmethods) foreach translateMemberSignature + val extensions = pextensions map translate val domain = (pdomains map translate) ++ extensions filter (t => t.isInstanceOf[Domain]) val fields = (pfields map translate) ++ extensions filter (t => t.isInstanceOf[Field]) From 01e67e2b642b66a4e58d6b253d5466b746289651 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 25 Feb 2022 12:50:14 +0100 Subject: [PATCH 11/50] Add prettyPrinting for extension AST nodes --- .../plugin/standard/adt/AdtASTExtension.scala | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala index b912bc45b..8f10be694 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala @@ -6,6 +6,8 @@ package viper.silver.plugin.standard.adt +import viper.silver.ast.pretty.FastPrettyPrinter.{ContOps, braces, brackets, char, defaultIndent, line, nest, nil, parens, show, showVars, space, ssep, text} +import viper.silver.ast.pretty.PrettyPrintPrimitives import viper.silver.ast.{AnyLocalVarDecl, Declaration, ErrorTrafo, ExtensionMember, ExtensionType, Info, LocalVarDecl, NoInfo, NoPosition, NoTrafos, Node, Position, Type, TypeVar} /** @@ -20,6 +22,15 @@ case class Adt(name: String, constructors: Seq[AdtConstructor], typVars: Seq[Typ val scopedDecls: Seq[Declaration] = Seq() override def extensionSubnodes: Seq[Node] = constructors ++ typVars + + override def prettyPrint: PrettyPrintPrimitives#Cont = { + text("adt") <+> name <> + (if (typVars.isEmpty) nil else text("[") <> ssep(typVars map show, char (',') <> space) <> "]") <+> + braces(nest(defaultIndent, + line <> line <> + ssep(constructors map show, line <> line) + ) <> line) + } } /** @@ -39,6 +50,8 @@ case class AdtConstructor(name: String, formalArgs: Seq[AnyLocalVarDecl]) val scopedDecls: Seq[Declaration] = formalArgs.filter(p => p.isInstanceOf[LocalVarDecl]).asInstanceOf[Seq[LocalVarDecl]] override def extensionSubnodes: Seq[Node] = formalArgs + + override def prettyPrint: PrettyPrintPrimitives#Cont = text(name) <> parens(showVars(formalArgs)) } /** @@ -70,6 +83,11 @@ case class AdtType(adtName: String, partialTypVarsMap: Map[TypeVar, Type]) /** Is this a concrete type (i.e. no uninstantiated type variables)? */ override def isConcrete: Boolean = typVarsMap.values.forall(_.isConcrete) + override def prettyPrint: PrettyPrintPrimitives#Cont = { + val typArgs = typeParameters map (t => show(typVarsMap.getOrElse(t, t))) + text(adtName) <> (if (typArgs.isEmpty) nil else brackets(ssep(typArgs, char (',') <> space))) + } + } object AdtType{ From e9737c45ec151f650e0cd222633d920e8128e099 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 25 Feb 2022 12:55:19 +0100 Subject: [PATCH 12/50] Finalize translation of PAST nodes to AST nodes for ADT declarations -Implement the translation for PAdtType to AdtType -Adjust translation flow to respect changes of the plugin infrastructure --- .../standard/adt/AdtPASTExtension.scala | 27 +++++++++++++------ .../plugin/standard/adt/AdtPlugin.scala | 5 ++-- 2 files changed, 22 insertions(+), 10 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index d245e5122..3465c62cb 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -6,7 +6,7 @@ package viper.silver.plugin.standard.adt -import viper.silver.ast.{Member, NoInfo, NoPosition, Position, TypeVar} +import viper.silver.ast.{Member, NoInfo, NoPosition, Position, Type, TypeVar} import viper.silver.parser.Transformer.ParseTreeDuplicationError import viper.silver.parser.{NameAnalyser, PAnyFormalArgDecl, PExtender, PGenericType, PGlobalDeclaration, PIdentifier, PIdnDef, PIdnUse, PMember, PNode, PType, PTypeSubstitution, PTypeVarDecl, Translator, TypeChecker} import viper.silver.plugin.standard.adt.PAdtConstructor.findAdtConstructor @@ -29,8 +29,15 @@ case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[P } override def translateMember(t: Translator): Member = { + + // In a first step translate constructor signatures + constructors map ( c => { + val cc = c.translateMemberSignature(t) + t.getMembers().put(c.idndef.name, cc) + }) + val a = PAdt.findAdt(idndef, t) - val aa = a.copy(constructors = constructors map (c => PAdtConstructor.findAdtConstructor(c.idndef, t)))(a.pos, a.info, a.errT) + val aa = a.copy(constructors = constructors map (_.translateMember(t)))(a.pos, a.info, a.errT) t.getMembers()(a.name) = aa aa } @@ -62,7 +69,7 @@ case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])( AdtConstructor(idndef.name, formalArgs map t.liftAnyVarDecl)(t.liftPos(this), NoInfo, adtName.name) } - override def translateMember(t: Translator): Member = { + override def translateMember(t: Translator): AdtConstructor = { findAdtConstructor(idndef, t) } @@ -183,11 +190,15 @@ case class PAdtType(adt: PIdnUse, args: Seq[PType])(val pos: (Position, Position } } - // TODO: Implement signature translation - override def translateMemberSignature(t: Translator): Member = ??? - - // TODO: Implement translation - override def translateMember(t: Translator): Member = ??? + override def translateType(t: Translator): Type = { + t.getMembers().get(adt.name) match { + case Some(d) => + val adt = d.asInstanceOf[Adt] + val typVarMapping = adt.typVars zip (args map t.ttyp) + AdtType(adt, typVarMapping.toMap) + case None => sys.error("undeclared adt type") + } + } } object PAdtTypeKinds { diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index 385338e0a..8ff678a83 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -7,6 +7,7 @@ package viper.silver.plugin.standard.adt import fastparse._ +import viper.silver.ast.Program import viper.silver.ast.utility.rewriter.StrategyBuilder import viper.silver.parser.FastParser.{FP, anyFormalArgList, idndef, whitespace} import viper.silver.parser.{PAnyFormalArgDecl, PDomainType, PFormalArgDecl, PFunction, PIdnDef, PIdnUse, PMethod, PNode, PProgram, PTypeVarDecl, ParserExtension} @@ -80,8 +81,8 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { newProgram } - override def beforeTranslate(input: PProgram): PProgram = { - // TODO: Finish the translation to AST nodes and remove the following statement + override def beforeVerify(input: Program): Program = { + // TODO: remove the following statement System.exit(-1) input } From 9e193c2add50d97fde72b02bde10252e277549d8 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 25 Feb 2022 13:27:20 +0100 Subject: [PATCH 13/50] Resolve TODO -Implement a much simpler solution for withChildren --- .../standard/adt/AdtPASTExtension.scala | 41 ++----------------- 1 file changed, 3 insertions(+), 38 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 3465c62cb..9dd77cbc1 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -7,11 +7,9 @@ package viper.silver.plugin.standard.adt import viper.silver.ast.{Member, NoInfo, NoPosition, Position, Type, TypeVar} -import viper.silver.parser.Transformer.ParseTreeDuplicationError import viper.silver.parser.{NameAnalyser, PAnyFormalArgDecl, PExtender, PGenericType, PGlobalDeclaration, PIdentifier, PIdnDef, PIdnUse, PMember, PNode, PType, PTypeSubstitution, PTypeVarDecl, Translator, TypeChecker} import viper.silver.plugin.standard.adt.PAdtConstructor.findAdtConstructor -import scala.reflect.runtime.{universe => reflection} case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[PAdtConstructor])(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { @@ -77,43 +75,10 @@ case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])( if (!forceRewrite && this.children == children && pos.isEmpty) this else { - - // TODO: Why can we not simplify with following code? => results in an Exception, is reflection really the only way? - /* + assert(children.length == 2, s"PAdtConstructor : expected length 2 but got ${children.length}") val first = children.head.asInstanceOf[PIdnDef] - val others = children.tail.asInstanceOf[Seq[PAnyFormalArgDecl]] - - - PAdtConstructor(first, others)(this.adtName)(pos.getOrElse(this.pos)).asInstanceOf[this.type] - */ - - // Infer constructor from type - val mirror = reflection.runtimeMirror(reflection.getClass.getClassLoader) - val instanceMirror = mirror.reflect(this) - val classSymbol = instanceMirror.symbol - val classMirror = mirror.reflectClass(classSymbol) - val constructorSymbol = instanceMirror.symbol.primaryConstructor.asMethod - val constructorMirror = classMirror.reflectConstructor(constructorSymbol) - - // Add additional arguments to constructor call, besides children - val firstArgList = children - var secondArgList = Seq.empty[Any] - - this match { - case pd: PAdtConstructor => secondArgList = Seq(pd.adtName) ++ Seq(pos.getOrElse(pd.pos)) - case _ => - } - - // Call constructor - val newNode = try { - constructorMirror(firstArgList ++ secondArgList: _*) - } - catch { - case _: Exception if this.isInstanceOf[PNode] => - throw ParseTreeDuplicationError(this.asInstanceOf[PNode], children) - } - - newNode.asInstanceOf[this.type] + val second = children.tail.head.asInstanceOf[Seq[PAnyFormalArgDecl]] + PAdtConstructor(first, second)(this.adtName)(pos.getOrElse(this.pos)).asInstanceOf[this.type] } } } From 7e4bb7ab6192e56812cc8656697933978b4b031c Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Wed, 2 Mar 2022 14:23:15 +0100 Subject: [PATCH 14/50] Implement method withChildren for AdtConstructor and AdtType -Since both classes have a special second argument list, we need to handle them correctly --- .../plugin/standard/adt/AdtASTExtension.scala | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala index 8f10be694..d83e8352c 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala @@ -52,6 +52,18 @@ case class AdtConstructor(name: String, formalArgs: Seq[AnyLocalVarDecl]) override def extensionSubnodes: Seq[Node] = formalArgs override def prettyPrint: PrettyPrintPrimitives#Cont = text(name) <> parens(showVars(formalArgs)) + + override def withChildren(children: Seq[Any], pos: Option[(Position, Position)], forceRewrite: Boolean): this.type = { + if (!forceRewrite && this.children == children && pos.isEmpty) + this + else { + assert(children.length == 2, s"AdtConstructor : expected length 2 but got ${children.length}") + val first = children.head.asInstanceOf[String] + val second = children.tail.head.asInstanceOf[Seq[AnyLocalVarDecl]] + AdtConstructor(first, second)(this.pos, this.info, this.adtName, this.errT).asInstanceOf[this.type] + } + + } } /** @@ -88,6 +100,17 @@ case class AdtType(adtName: String, partialTypVarsMap: Map[TypeVar, Type]) text(adtName) <> (if (typArgs.isEmpty) nil else brackets(ssep(typArgs, char (',') <> space))) } + override def withChildren(children: Seq[Any], pos: Option[(Position, Position)], forceRewrite: Boolean): this.type = { + if (!forceRewrite && this.children == children && pos.isEmpty) + this + else { + assert(children.length == 2, s"AdtType : expected length 2 but got ${children.length}") + val first = children.head.asInstanceOf[String] + val second = children.tail.head.asInstanceOf[Map[TypeVar, Type]] + AdtType(first, second)(this.typeParameters).asInstanceOf[this.type] + } + } + } object AdtType{ From 1952c7fb4d78fc6f387a100f919a399b927ed1a4 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Wed, 2 Mar 2022 14:17:37 +0100 Subject: [PATCH 15/50] Fix issue in rewriting strategy -Despite handling the case when node is a Map, the rewriting of Maps does not work correctly. This is because Tuple's are not handled, which stops the recursion and prevents rewriting. -Added a case for Tuple, that solves the described issue. --- .../scala/viper/silver/ast/utility/rewriter/Strategy.scala | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala b/src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala index 35e9f09cc..76a2de8e8 100644 --- a/src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala +++ b/src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala @@ -400,6 +400,8 @@ class Strategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, C node match { case map: Map[_, _] => map.map(rewriteTopDown(_, context)).asInstanceOf[A] + case (t1, t2) => (rewriteTopDown(t1, context), rewriteTopDown(t2, context)).asInstanceOf[A] + case Some(value) => Some(rewriteTopDown(value, context)).asInstanceOf[A] case node: N @unchecked => @@ -431,6 +433,8 @@ class Strategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, C node match { case map: Map[_, _] => map.map(rewriteBottomUp(_, context)).asInstanceOf[A] + case (t1, t2) => (rewriteBottomUp(t1, context), rewriteBottomUp(t2, context)).asInstanceOf[A] + case Some(value) => Some(rewriteBottomUp(value, context)).asInstanceOf[A] case node: N @unchecked => @@ -460,6 +464,8 @@ class Strategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, C node match { case map: Map[_, _] => map.map(rewriteInnermost(_, context)).asInstanceOf[A] + case (t1, t2) => (rewriteInnermost(t1, context), rewriteInnermost(t2, context)).asInstanceOf[A] + case Some(value) => Some(rewriteInnermost(value, context)).asInstanceOf[A] case node: N @unchecked => From ecaf1c62718c883e794c573e72eb28167ba50da3 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Wed, 2 Mar 2022 15:17:51 +0100 Subject: [PATCH 16/50] Resolve TODO -Make use of the fact that all nodes are Rewritable's, so we can traverse the entire tree using a StrategyBuilder --- .../silver/plugin/standard/adt/AdtPlugin.scala | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index 8ff678a83..e27aaea17 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -10,7 +10,7 @@ import fastparse._ import viper.silver.ast.Program import viper.silver.ast.utility.rewriter.StrategyBuilder import viper.silver.parser.FastParser.{FP, anyFormalArgList, idndef, whitespace} -import viper.silver.parser.{PAnyFormalArgDecl, PDomainType, PFormalArgDecl, PFunction, PIdnDef, PIdnUse, PMethod, PNode, PProgram, PTypeVarDecl, ParserExtension} +import viper.silver.parser._ import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} @@ -64,21 +64,11 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { // Replace PDomainType by PAdtType if a corresponding ADT exists, since they are automatically parsed as an PDomainType // and there is no way to extend the parser to avoid this. val declaredAdtNames = input.extensions.collect { case a: PAdt => a.idndef }.toSet - // TODO: With the current strategy occurrences of PDomainTypes in constructor, function and method signatures - // are handled (especially they are converted to an PAdtType if there is an corresponding declaration). - // Handling of AdtTypes in variable declarations, built-in type declarations, etc. must be implemented in a later step. - val newProgram: PProgram = StrategyBuilder.Slim[PNode]({ + StrategyBuilder.Slim[PNode]({ case pa@PDomainType(idnuse, args) if declaredAdtNames.exists(_.name == idnuse.name) => PAdtType(idnuse, args)(pa.pos) - case d => d }).recurseFunc({ - case PProgram(_, _, _, _, functions, _, methods, extensions, _) => Seq(extensions) ++ Seq(functions) ++ Seq(methods) - case PMethod(_, formalArgs, formalReturns, _, _, _) => Seq(formalArgs) ++ Seq(formalReturns) - case PFunction(_, formalArgs, typ, _, _, _) => Seq(formalArgs) ++ Seq(typ) - case PAdt(_, _, constructors) => Seq(constructors) - case PAdtConstructor(_, formalArgs) => Seq(formalArgs) - case PFormalArgDecl(_, typ) => Seq(typ) + case d: PNode => d.children.collect {case ar: AnyRef => ar} }).execute(input) - newProgram } override def beforeVerify(input: Program): Program = { From 72cb46a0e730189f737831de8c00356ee035b405 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Wed, 2 Mar 2022 15:34:01 +0100 Subject: [PATCH 17/50] Created a new class for the AdtEncoder -Add functionality to encode ADT declarations, constructors and types --- .../standard/adt/encoding/AdtEncoder.scala | 79 +++++++++++++++++++ 1 file changed, 79 insertions(+) create mode 100644 src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala new file mode 100644 index 000000000..3b0f5022e --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala @@ -0,0 +1,79 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// 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-2022 ETH Zurich. + +package viper.silver.plugin.standard.adt.encoding + +import viper.silver.ast.utility.rewriter.StrategyBuilder +import viper.silver.ast._ +import viper.silver.plugin.standard.adt.{Adt, AdtConstructor, AdtType} + + + + +class AdtEncoder (val program: Program) { + + /** + * This method encodes all ADT related AST nodes to normal AST nodes. + * + * @return + */ + def encode(): Program = { + + // In a first step encode all adt top level declarations + val encodedAdts: Seq[Domain] = program.extensions map {case a: Adt => encodeAdtAsDomain(a)} + val newProgram: Program = program.copy(domains = program.domains ++ encodedAdts, extensions = Seq())(program.pos, program.info, program.errT) + + // In a second step encode all occurrences of AdtType's as DomainType's + encodeAllAdtTypeAsDomainType(newProgram) + } + + /** + * This method takes an ADT and encodes it as a Domain + * + * @param adt the ADT to encode + * @return an the encoded ADT as a domain + */ + private def encodeAdtAsDomain(adt: Adt): Domain = { + adt match { + case Adt(name, constructors, typVars) => + val domain = Domain(name, null, null, typVars)(adt.pos, adt.info, adt.errT) + // TODO: Add injectivity, exclusivity, destructors, etc. + val functions = constructors map encodeAdtConstructorAsDomainFunc(domain) + val axioms = Seq() + domain.copy(functions = functions, axioms = axioms)(adt.pos, adt.info, adt.errT) + } + } + + /** + * This method encodes an ADT constructor as a domain function + * + * @param domain the domain the encoded constructor belongs to + * @param ac the ADT constructor to encode + * @return an encoded ADT constructor as a domain function + */ + private def encodeAdtConstructorAsDomainFunc(domain: Domain)(ac: AdtConstructor): DomainFunc = { + ac match { + case a@AdtConstructor(name, formalArgs) => DomainFunc(name, formalArgs, DomainType(domain, Map.empty))(a.pos, a.info, domain.name, a.errT) + } + } + + /** + * This method traverses the entire AST an encodes any occurrences of an AdtType as a DomainType + * + * @param program The program to encode + * @return a program free of AdtType's + */ + private def encodeAllAdtTypeAsDomainType(program: Program): Program = { + StrategyBuilder.Slim[Node]({ + case at@AdtType(adtName, partialTypVarsMap) => DomainType(adtName, partialTypVarsMap)(at.typeParameters) + }).recurseFunc({ + case fa@FuncApp(_, args) => Seq(args, fa.typ) + case df@DomainFuncApp(_, args, typVarMap) => Seq(args, typVarMap, df.typ) + case d: Node => d.children.collect {case ar: AnyRef => ar} + }).execute(program) + } + +} From 22a56b94bf31f02391b27fbb6e8e1562fe40d631 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Wed, 2 Mar 2022 15:35:23 +0100 Subject: [PATCH 18/50] Use the AdtEncoder -Use the AdtEncoder to encode ADT related AST nodes to normal AST nodes before the AST is passed to the verifier --- .../scala/viper/silver/plugin/standard/adt/AdtPlugin.scala | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index e27aaea17..da4f98bc8 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -11,6 +11,7 @@ import viper.silver.ast.Program import viper.silver.ast.utility.rewriter.StrategyBuilder import viper.silver.parser.FastParser.{FP, anyFormalArgList, idndef, whitespace} import viper.silver.parser._ +import viper.silver.plugin.standard.adt.encoding.AdtEncoder import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} @@ -72,9 +73,7 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { } override def beforeVerify(input: Program): Program = { - // TODO: remove the following statement - System.exit(-1) - input + new AdtEncoder(input).encode() } } From c960afc44a37721f715158d8ea4edc2b84e0cb00 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Thu, 3 Mar 2022 16:28:39 +0100 Subject: [PATCH 19/50] Add a PAST node for an ADT constructor call -Implement first version of type checking for ADT operation applications --- .../standard/adt/AdtPASTExtension.scala | 131 +++++++++++++++++- 1 file changed, 129 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 9dd77cbc1..731483e56 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -6,8 +6,8 @@ package viper.silver.plugin.standard.adt -import viper.silver.ast.{Member, NoInfo, NoPosition, Position, Type, TypeVar} -import viper.silver.parser.{NameAnalyser, PAnyFormalArgDecl, PExtender, PGenericType, PGlobalDeclaration, PIdentifier, PIdnDef, PIdnUse, PMember, PNode, PType, PTypeSubstitution, PTypeVarDecl, Translator, TypeChecker} +import viper.silver.ast._ +import viper.silver.parser._ import viper.silver.plugin.standard.adt.PAdtConstructor.findAdtConstructor @@ -40,6 +40,21 @@ case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[P aa } + /** + * This is a helper method that creates an AdtType from the ADT's signature. + * + * @return An AdtType that corresponds to the ADTs signature + */ + def getAdtType: PAdtType = { + val adtType = PAdtType(PIdnUse(idndef.name)(NoPosition, NoPosition), typVars map { t => + val typeVar = PDomainType(PIdnUse(t.idndef.name)(NoPosition, NoPosition), Nil)(NoPosition, NoPosition) + typeVar.kind = PDomainTypeKinds.TypeVar + typeVar + })(NoPosition, NoPosition) + adtType.kind = PAdtTypeKinds.Adt + adtType + } + } object PAdt { @@ -164,6 +179,9 @@ case class PAdtType(adt: PIdnUse, args: Seq[PType])(val pos: (Position, Position case None => sys.error("undeclared adt type") } } + + override def toString: String = adt.name + (if (args.isEmpty) "" else s"[${args.mkString(", ")}]") + } object PAdtTypeKinds { @@ -171,4 +189,113 @@ object PAdtTypeKinds { case object Unresolved extends Kind case object Adt extends Kind case object Undeclared extends Kind +} + +/** Common trait for ADT operator applications **/ +sealed trait PAdtOpApp extends PExtender with POpApp + +object PAdtOpApp { + /** + * This method mirrors the functionality in Resolver.scala that handle operation applications, except that it is + * adapted to work for ADT operator applications. + */ + def typecheck(poa: PAdtOpApp)(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { + + def getFreshTypeSubstitution(tvs : Seq[PDomainType]) : PTypeRenaming = + PTypeVar.freshTypeSubstitutionPTVs(tvs) + + // Checks that a substitution is fully reduced (idempotent) + def refreshWith(ts: PTypeSubstitution, rts : PTypeRenaming) : PTypeSubstitution = { + require(ts.isFullyReduced) + require(rts.isFullyReduced) + // require(rts.values.forall { case pdt: PDomainType if pdt.isTypeVar => true case _ => false }) + new PTypeSubstitution(ts map (kv => rts.rename(kv._1) -> kv._2.substitute(rts))) + } + + var extraReturnTypeConstraint : Option[PType] = None + + if (poa.typeSubstitutions.isEmpty) { + poa.args.foreach(t.checkInternal) + var nestedTypeError = !poa.args.forall(a => a.typ.isValidOrUndeclared) + if (!nestedTypeError) { + poa match { + case pcc@PConstructorCall(constr, args, typeAnnotated) => + typeAnnotated match { + case Some(ta) => + t.check(ta) + if (!ta.isValidOrUndeclared) nestedTypeError = true + case None => + } + + if (!nestedTypeError) { + val ad = t.names.definition(t.curMember)(constr).asInstanceOf[PAdtConstructor] + pcc.constructor = ad + t.ensure(ad.formalArgs.size == args.size, pcc, "wrong number of arguments") + val adt = t.names.definition(t.curMember)(ad.adtName).asInstanceOf[PAdt] + pcc.adt = adt + val fdtv = PTypeVar.freshTypeSubstitution((adt.typVars map (tv => tv.idndef.name)).distinct) //fresh domain type variables + pcc.adtTypeRenaming = Some(fdtv) + pcc._extraLocalTypeVariables = (adt.typVars map (tv => PTypeVar(tv.idndef.name))).toSet + extraReturnTypeConstraint = pcc.typeAnnotated + } + case _ => // TODO: Handle the remaining ADT operation applications (e.g discriminators, destructors) here + } + + if (poa.signatures.nonEmpty && poa.args.forall(_.typeSubstitutions.nonEmpty) && !nestedTypeError) { + val ltr = getFreshTypeSubstitution(poa.localScope.toList) //local type renaming - fresh versions + val rlts = poa.signatures map (ts => refreshWith(ts, ltr)) //local substitutions refreshed + assert(rlts.nonEmpty) + val rrt: PDomainType = POpApp.pRes.substitute(ltr).asInstanceOf[PDomainType] // return type (which is a dummy type variable) replaced with fresh type + val flat = poa.args.indices map (i => POpApp.pArg(i).substitute(ltr)) //fresh local argument types + // the triples below are: (fresh argument type, argument type as used in domain of substitutions, substitutions) + poa.typeSubstitutions ++= t.unifySequenceWithSubstitutions(rlts, flat.indices.map(i => (flat(i), poa.args(i).typ, poa.args(i).typeSubstitutions.distinct.toSeq)) ++ + ( + extraReturnTypeConstraint match { + case None => Nil + case Some(t) => Seq((rrt, t, List(PTypeSubstitution.id))) + } + ) + ) + val ts = poa.typeSubstitutions.distinct + if (ts.isEmpty) + t.typeError(poa) + poa.typ = if (ts.size == 1) rrt.substitute(ts.head) else rrt + } else { + poa.typeSubstitutions.clear() + poa.typ = PUnknown()() + } + } + } + None + } +} + +case class PConstructorCall(constr: PIdnUse, args: Seq[PExp], typeAnnotated : Option[PType] = None)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PAdtOpApp with PLocationAccess { + override def opName: String = constr.name + override def idnuse: PIdnUse = constr + + override def getSubnodes(): Seq[PNode] = Seq(constr) ++ args ++ (typeAnnotated match { case Some(t) => Seq(t) case None => Nil}) + + override def signatures: List[PTypeSubstitution] = { + if (adt != null && constructor != null) { + List( + new PTypeSubstitution( + args.indices.map(i => POpApp.pArg(i).domain.name -> constructor.formalArgs(i).typ.substitute(adtTypeRenaming.get)) :+ + (POpApp.pRes.domain.name -> adt.getAdtType.substitute(adtTypeRenaming.get))) + ) + } else List() + } + + // Following fields are set during resolving, respectively in the typecheck method below + var adt: PAdt = null + var constructor: PAdtConstructor = null + var adtTypeRenaming: Option[PTypeRenaming] = None + var _extraLocalTypeVariables: Set[PDomainType] = Set() + + override def extraLocalTypeVariables: Set[PDomainType] = _extraLocalTypeVariables + + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = PAdtOpApp.typecheck(this)(t,n) + + override def translateExp(t: Translator): Exp = ??? // TODO: Implement + } \ No newline at end of file From ff73fe5281c8415f32d9b533d4cc1bda45274cf3 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 4 Mar 2022 14:31:23 +0100 Subject: [PATCH 20/50] Add return type to AdtConstructor -Additionally we add a companion object s.t the return type is set correctly --- .../plugin/standard/adt/AdtASTExtension.scala | 17 +++++++++++++---- .../plugin/standard/adt/AdtPASTExtension.scala | 3 ++- 2 files changed, 15 insertions(+), 5 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala index d83e8352c..96e65039b 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala @@ -8,7 +8,7 @@ package viper.silver.plugin.standard.adt import viper.silver.ast.pretty.FastPrettyPrinter.{ContOps, braces, brackets, char, defaultIndent, line, nest, nil, parens, show, showVars, space, ssep, text} import viper.silver.ast.pretty.PrettyPrintPrimitives -import viper.silver.ast.{AnyLocalVarDecl, Declaration, ErrorTrafo, ExtensionMember, ExtensionType, Info, LocalVarDecl, NoInfo, NoPosition, NoTrafos, Node, Position, Type, TypeVar} +import viper.silver.ast._ /** * This class represents a user-defined ADT. @@ -34,14 +34,17 @@ case class Adt(name: String, constructors: Seq[AdtConstructor], typVars: Seq[Typ } /** - * This class represents an ADT constructor + * This class represents an ADT constructor. See also the companion object below, which allows passing a + * Adt - this should be used in general for creation (so that typ is guaranteed to + * be set correctly) * * @param name name of the ADT constructor * @param formalArgs sequence of arguments of the constructor + * @param typ the return type of the constructor * @param adtName the name corresponding of the corresponding ADT */ case class AdtConstructor(name: String, formalArgs: Seq[AnyLocalVarDecl]) - (val pos: Position = NoPosition, val info: Info = NoInfo, val adtName : String, val errT: ErrorTrafo = NoTrafos) + (val pos: Position, val info: Info, typ: AdtType, val adtName : String, val errT: ErrorTrafo) extends ExtensionMember { override def getMetadata:Seq[Any] = { @@ -60,12 +63,18 @@ case class AdtConstructor(name: String, formalArgs: Seq[AnyLocalVarDecl]) assert(children.length == 2, s"AdtConstructor : expected length 2 but got ${children.length}") val first = children.head.asInstanceOf[String] val second = children.tail.head.asInstanceOf[Seq[AnyLocalVarDecl]] - AdtConstructor(first, second)(this.pos, this.info, this.adtName, this.errT).asInstanceOf[this.type] + AdtConstructor(first, second)(this.pos, this.info, this.typ, this.adtName, this.errT).asInstanceOf[this.type] } } } +object AdtConstructor { + def apply(adt: Adt, name: String, formalArgs: Seq[AnyLocalVarDecl])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): AdtConstructor = { + AdtConstructor(name, formalArgs)(pos, info, AdtType(adt, Map.empty), adt.name, errT) + } +} + /** * This class represents an user-defined ADT type. See also the companion object below, which allows passing a * Adt - this should be used in general for creation (so that typeParameters is guaranteed to diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 731483e56..95642baf9 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -79,7 +79,8 @@ case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])( } override def translateMemberSignature(t: Translator): AdtConstructor = { - AdtConstructor(idndef.name, formalArgs map t.liftAnyVarDecl)(t.liftPos(this), NoInfo, adtName.name) + val adt = PAdt.findAdt(adtName, t) + AdtConstructor(adt, idndef.name, formalArgs map t.liftAnyVarDecl)(t.liftPos(this)) } override def translateMember(t: Translator): AdtConstructor = { From 5faa7c00c7405db57966ed757c75fb4b9a45228c Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 4 Mar 2022 17:43:11 +0100 Subject: [PATCH 21/50] Add an AST node for an ADT constructor application -Additionally, missing methods of AdtType are implemented --- .../plugin/standard/adt/AdtASTExtension.scala | 68 ++++++++++++++++++- 1 file changed, 65 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala index 96e65039b..c06507c8b 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala @@ -6,9 +6,11 @@ package viper.silver.plugin.standard.adt +import viper.silver.ast._ import viper.silver.ast.pretty.FastPrettyPrinter.{ContOps, braces, brackets, char, defaultIndent, line, nest, nil, parens, show, showVars, space, ssep, text} import viper.silver.ast.pretty.PrettyPrintPrimitives -import viper.silver.ast._ +import viper.silver.ast.utility.Consistency +import viper.silver.verifier.{ConsistencyError, Failure, VerificationResult} /** * This class represents a user-defined ADT. @@ -44,7 +46,7 @@ case class Adt(name: String, constructors: Seq[AdtConstructor], typVars: Seq[Typ * @param adtName the name corresponding of the corresponding ADT */ case class AdtConstructor(name: String, formalArgs: Seq[AnyLocalVarDecl]) - (val pos: Position, val info: Info, typ: AdtType, val adtName : String, val errT: ErrorTrafo) + (val pos: Position, val info: Info, val typ: AdtType, val adtName : String, val errT: ErrorTrafo) extends ExtensionMember { override def getMetadata:Seq[Any] = { @@ -88,6 +90,10 @@ object AdtConstructor { case class AdtType(adtName: String, partialTypVarsMap: Map[TypeVar, Type]) (val typeParameters: Seq[TypeVar]) extends ExtensionType { + override lazy val check: Seq[ConsistencyError] = if(!(typeParameters.toSet == typVarsMap.keys.toSet)) { + Seq(ConsistencyError(s"${typeParameters.toSet} doesn't equal ${typVarsMap.keys.toSet}", NoPosition)) + } else Seq() + /** * Map each type parameter `A` to `partialTypVarsMap(A)`, if defined, otherwise to `A` itself. * `typVarsMap` thus contains a mapping for each type parameter. @@ -99,7 +105,11 @@ case class AdtType(adtName: String, partialTypVarsMap: Map[TypeVar, Type]) * Takes a mapping of type variables to types and substitutes all * occurrences of those type variables with the corresponding type. */ - override def substitute(typVarsMap: Map[TypeVar, Type]): Type = ??? + override def substitute(newTypVarsMap: Map[TypeVar, Type]): Type = { + assert (typVarsMap.keys.toSet equals this.typeParameters.toSet) + val newTypeMap = typVarsMap.map(kv=>kv._1 -> kv._2.substitute(newTypVarsMap)) + AdtType(adtName, newTypeMap)(typeParameters) + } /** Is this a concrete type (i.e. no uninstantiated type variables)? */ override def isConcrete: Boolean = typVarsMap.values.forall(_.isConcrete) @@ -128,3 +138,55 @@ object AdtType{ } +/** + * This class represents a user-defined adt constructor application. See also the companion object below, which allows passing a + * Adt constructor - this should be used in general for creation (so that typ is guaranteed to + * be set correctly) + * + * @param name The name of the ADT constructor + * @param args A sequence of expressions passed as arguments to the constructor + * @param typVarMap Maps type parameters to (possibly concrete) types. May not map all + * type parameters, may even be empty. + * @param typ The return type of the constructor + * @param adtName The corresponding ADT name + */ +case class AdtConstructorApp(name: String, args: Seq[Exp], typVarMap: Map[TypeVar, Type]) + (val pos: Position, val info: Info, override val typ: Type, val adtName:String, val errT: ErrorTrafo) + extends ExtensionExp { + override lazy val check : Seq[ConsistencyError] = args.flatMap(Consistency.checkPure) + + override def prettyPrint: PrettyPrintPrimitives#Cont = { + if (typVarMap.nonEmpty) + // Type may be under-constrained, so to be safe we explicitly print out the type. + parens(text(name) <> parens(ssep(args map show, char (',') <> space)) <> char(':') <+> show(typ)) + else + text(name) <> parens(ssep(args map show, char (',') <> space)) + } + + override def extensionIsPure: Boolean = true + + override def extensionSubnodes: Seq[Node] = args ++ typVarMap.keys ++ typVarMap.values + + override def verifyExtExp(): VerificationResult = { + assert(assertion = false, "AdtConstructorApp: verifyExtExp has not been implemented.") + Failure(Seq(ConsistencyError("AdtConstructorApp: verifyExtExp has not been implemented.", pos))) + } + + override def withChildren(children: Seq[Any], pos: Option[(Position, Position)], forceRewrite: Boolean): AdtConstructorApp.this.type = { + if (!forceRewrite && this.children == children && pos.isEmpty) + this + else { + assert(children.length == 3, s"AdtConstructorApp : expected length 3 but got ${children.length}") + val first = children.head.asInstanceOf[String] + val second = children(1).asInstanceOf[Seq[Exp]] + val third = children(2).asInstanceOf[Map[TypeVar, Type]] + AdtConstructorApp(first, second, third)(this.pos, this.info, this.typ, this.adtName, this.errT).asInstanceOf[this.type] + } + } +} +object AdtConstructorApp { + def apply(constructor : AdtConstructor, args: Seq[Exp], typVarMap: Map[TypeVar, Type])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos) : AdtConstructorApp = + AdtConstructorApp(constructor.name, args, typVarMap)(pos, info, constructor.typ.substitute(typVarMap), constructor.adtName, errT) +} + + From 947694250f3589d3316b8662709b53e4cb3ea46e Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 4 Mar 2022 17:49:00 +0100 Subject: [PATCH 22/50] Fix type checking for constructor call and add implement transaltion --- .../standard/adt/AdtPASTExtension.scala | 38 +++++++++++++++++-- 1 file changed, 35 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 95642baf9..4a2460943 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -197,7 +197,7 @@ sealed trait PAdtOpApp extends PExtender with POpApp object PAdtOpApp { /** - * This method mirrors the functionality in Resolver.scala that handle operation applications, except that it is + * This method mirrors the functionality in Resolver.scala that handles operation applications, except that it is * adapted to work for ADT operator applications. */ def typecheck(poa: PAdtOpApp)(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { @@ -209,7 +209,6 @@ object PAdtOpApp { def refreshWith(ts: PTypeSubstitution, rts : PTypeRenaming) : PTypeSubstitution = { require(ts.isFullyReduced) require(rts.isFullyReduced) - // require(rts.values.forall { case pdt: PDomainType if pdt.isTypeVar => true case _ => false }) new PTypeSubstitution(ts map (kv => rts.rename(kv._1) -> kv._2.substitute(rts))) } @@ -292,11 +291,44 @@ case class PConstructorCall(constr: PIdnUse, args: Seq[PExp], typeAnnotated : Op var constructor: PAdtConstructor = null var adtTypeRenaming: Option[PTypeRenaming] = None var _extraLocalTypeVariables: Set[PDomainType] = Set() + var adtSubstitution: Option[PTypeSubstitution] = None override def extraLocalTypeVariables: Set[PDomainType] = _extraLocalTypeVariables override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = PAdtOpApp.typecheck(this)(t,n) - override def translateExp(t: Translator): Exp = ??? // TODO: Implement + override def forceSubstitution(ots: PTypeSubstitution): Unit = { + + val ts = adtTypeRenaming match { + case Some(dtr) => + val s3 = PTypeSubstitution(dtr.mm.map(kv => kv._1 -> (ots.get(kv._2) match { + case Some(pt) => pt + case None => PTypeSubstitution.defaultType + }))) + assert(s3.m.keySet==dtr.mm.keySet) + assert(s3.m.forall(_._2.isGround)) + adtSubstitution = Some(s3) + dtr.mm.values.foldLeft(ots)( + (tss,s)=> if (tss.contains(s)) tss else tss.add(s, PTypeSubstitution.defaultType).get) + case _ => ots + } + super.forceSubstitution(ts) + } + + override def translateExp(t: Translator): Exp = { + val constructor = PAdtConstructor.findAdtConstructor(constr, t) + val actualArgs = args map t.exp + val so : Option[Map[TypeVar, Type]] = adtSubstitution match{ + case Some(ps) => Some(ps.m.map(kv=>TypeVar(kv._1)->t.ttyp(kv._2))) + case None => None + } + so match { + case Some(s) => + val adt = t.getMembers()(constructor.adtName).asInstanceOf[Adt] + assert(s.keys.toSet == adt.typVars.toSet) + AdtConstructorApp(constructor, actualArgs, s)(t.liftPos(this)) + case _ => sys.error("type unification error - should report and not crash") + } + } } \ No newline at end of file From 22453025e87ce5c37396b2c85137b693a49735b7 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 11 Mar 2022 09:59:48 +0100 Subject: [PATCH 23/50] Add an AdtNameManager - Contains utility to avoid name conflicts when adding tag function declarations and destructor function declarations. --- .../adt/encoding/AdtNameManager.scala | 99 +++++++++++++++++++ 1 file changed, 99 insertions(+) create mode 100644 src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala new file mode 100644 index 000000000..b9a0da6dc --- /dev/null +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala @@ -0,0 +1,99 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// 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-2022 ETH Zurich. + +package viper.silver.plugin.standard.adt.encoding + + +import viper.silver.ast.Program + +import scala.collection.mutable + + + +/** + * A simple interface to transform/extend a program. + * Contains utility functions to avoid name conflicts (e.g. when adding a new domain functions to a domain) + */ +trait AdtNameManager { + + /** + * This field holds the original program + */ + val program: Program + + /** + * This field hold a set that contains all global names of the original program + */ + private val usedNames: mutable.Set[String] = collection.mutable.Set(program.transitiveScopedDecls.map(_.name): _*) + + /** + * This field stores the mappings generated by getName(...) + */ + private val adtNameMappings: mutable.Map[String, String] = mutable.Map() + + /** + * This method returns the name of the destructor given the name of the ADT and the name of a constructor argument + * + * @param adtName The name of the ADT the destructor belongs to + * @param argument The name of a constructor argument for which we want the corresponding destructor + * @return The name of the queried constructor + */ + def getDestructorName(adtName: String, argument: String): String = getName(s"get_${adtName}_$argument") + + /** + * This method will return the name of the tag function given the ADT name + * + * @param adtName The name of the ADT for which we want the name of the tag function + * @return The name of the tag function + */ + def getTagName(adtName: String): String = getName(s"${adtName}_tag") + + /** + * This method returns an unique name and adds the new generated name to the adtNameMappings. If the method is + * called again with the same argument, the corresponding unique name is looked ap in adtNameMappings and returned. + * + * @param trueName A potential name to be unique + * @return + */ + private def getName(trueName: String): String = { + + var newName = trueName + if (!adtNameMappings.contains(trueName) && containsName(trueName)) { + newName = uniqueName(trueName) + } + adtNameMappings.addOne((trueName, newName)) + adtNameMappings(trueName) + } + + + /** + * Checks if a name already occurs in the program. + * + * @param name to be checked + * @return true iff the name is used in the program. + */ + private def containsName(name: String): Boolean = { + usedNames.contains(name) + } + + /** + * Creates a unique name for the program and adds it to the names already used in the program. + * + * @param name which is wanted + * @return a name which is unique in the program + */ + private def uniqueName(name: String): String = { + var i = 1 + var newName = name + while (containsName(newName)) { + newName = name + i + i += 1 + } + usedNames.add(newName) + newName + } + +} From a5b0856dcd530c1c07e17c862b99772b00823e24 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 11 Mar 2022 10:03:01 +0100 Subject: [PATCH 24/50] Finalize main encoding of ADTs as domain functions -This includes adding injectivity and exclusivity axioms, adding an encoding for destructors and a tag function for discrimination --- .../standard/adt/encoding/AdtEncoder.scala | 298 ++++++++++++++++-- 1 file changed, 275 insertions(+), 23 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala index 3b0f5022e..91ea5bce7 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala @@ -6,14 +6,17 @@ package viper.silver.plugin.standard.adt.encoding -import viper.silver.ast.utility.rewriter.StrategyBuilder import viper.silver.ast._ -import viper.silver.plugin.standard.adt.{Adt, AdtConstructor, AdtType} +import viper.silver.ast.utility.rewriter.{StrategyBuilder, Traverse} +import viper.silver.plugin.standard.adt.{Adt, AdtConstructor, AdtConstructorApp, AdtType} - - -class AdtEncoder (val program: Program) { +/** + * This class implement the encoder used to encode ADT AST nodes to ordinary AST nodes. + * + * @param program The program containing ADT AST nodes, we want to encode. + */ +class AdtEncoder (val program: Program) extends AdtNameManager { /** * This method encodes all ADT related AST nodes to normal AST nodes. @@ -31,49 +34,298 @@ class AdtEncoder (val program: Program) { } /** - * This method takes an ADT and encodes it as a Domain + * This method takes an ADT and encodes it as a Domain. Especially it does + * 1. Maps Adt to Domain + * 2. Maps AdtConstructor -> DomainFunc + * 3. Adds destructor declarations encoded as domain functions + * 4. Adds a tag functions encoded as domain functions + * 5. Generates corresponding axioms for injectivity, exclusivity and the tag function * - * @param adt the ADT to encode - * @return an the encoded ADT as a domain + * @param adt The ADT to encode + * @return An the encoded ADT as a domain */ private def encodeAdtAsDomain(adt: Adt): Domain = { adt match { case Adt(name, constructors, typVars) => val domain = Domain(name, null, null, typVars)(adt.pos, adt.info, adt.errT) - // TODO: Add injectivity, exclusivity, destructors, etc. - val functions = constructors map encodeAdtConstructorAsDomainFunc(domain) - val axioms = Seq() + val functions: Seq[DomainFunc] = (constructors map encodeAdtConstructorAsDomainFunc(domain)) ++ + (constructors flatMap generateDestructorDeclarations(domain)) ++ Seq(generateTagDeclaration(domain)) + val axioms = (constructors flatMap generateInjectivityAxiom(domain)) ++ + (constructors.zipWithIndex map { case (c, i) => generateTagAxiom(domain)(c, i) }) ++ Seq(generateExclusivityAxiom(domain)(constructors)) domain.copy(functions = functions, axioms = axioms)(adt.pos, adt.info, adt.errT) } } + /** + * This method creates a local variable given a type. One can specify the name of the local variable via the optional + * argument 'name'. By default the name is 't'. + * + * @param typ The type for which one wants to generate a local variable + * @param name Optional argument specifying the name og the local variable + * @return A local variable typed as 'typ' and with name 'name', if specified + */ + private def localVarTFromType(typ:Type, name: Option[String] = None) = { + name match { + case Some(str) => LocalVar(str, typ)(_,_,_) + case None => LocalVar("t", typ)(_,_,_) + } + } + + /** + * This method creates a local variable declaration given a type. One can specify the name of the local variable via the optional + * argument 'name'. By default the name is 't'. + * + * @param typ The type for which one wants to generate a local variable declaration + * @param name Optional argument specifying the name og the local variable declaration + * @return A local variable declaration typed as 'typ' and with name 'name', if specified + */ + private def localVarTDeclFromType(typ:Type, name: Option[String] = None) = { + name match { + case Some(str) => LocalVarDecl(str, typ)(_,_,_) + case None => LocalVarDecl("t", typ)(_,_,_) + } + } + /** * This method encodes an ADT constructor as a domain function * - * @param domain the domain the encoded constructor belongs to - * @param ac the ADT constructor to encode - * @return an encoded ADT constructor as a domain function + * @param domain The domain the encoded constructor belongs to + * @param ac The ADT constructor to encode + * @return An encoded ADT constructor as a domain function */ private def encodeAdtConstructorAsDomainFunc(domain: Domain)(ac: AdtConstructor): DomainFunc = { ac match { - case a@AdtConstructor(name, formalArgs) => DomainFunc(name, formalArgs, DomainType(domain, Map.empty))(a.pos, a.info, domain.name, a.errT) + case AdtConstructor(name, formalArgs) => DomainFunc(name, formalArgs, encodeAdtTypeAsDomainType(ac.typ))(ac.pos, ac.info, domain.name, ac.errT) + } + } + + /** + * This methods encode an ADT constructor application as a domain function application + * + * @param aca The constructor application + * @return The constructor application encoded as a domain function application + */ + private def encodeAdtConstructorApp(aca: AdtConstructorApp) = { + DomainFuncApp( + aca.name, + aca.args, + aca.typVarMap + )(_,_,aca.typ, aca.adtName, _) + } + + + /** + * This method generates destructor declarations for a corresponding ADT constructor + * + * @param domain the domain the encoded constructor belongs to + * @param ac the adt constructor for which we want to generate destructor declarations + * @return A sequence of destructor declarations, empty if constructor has no arguments + */ + private def generateDestructorDeclarations(domain:Domain)(ac: AdtConstructor): Seq[DomainFunc] = { + assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.") + ac.formalArgs.map { + case LocalVarDecl(name, typ) => + val args = Seq(localVarTDeclFromType(encodeAdtTypeAsDomainType(ac.typ))(ac.pos, ac.info, ac.errT)) + val ttyp = typ match { + case a:AdtType => encodeAdtTypeAsDomainType(a) + case d => d + } + DomainFunc( + getDestructorName(ac.adtName, name), + args, + ttyp + )(ac.pos, ac.info, ac.adtName, ac.errT) + case _ => sys.error("AdtEncoder : Only LocalVarDecl are allowed as arguments of an Adt constructor") } } /** - * This method traverses the entire AST an encodes any occurrences of an AdtType as a DomainType + * This method generates the corresponding injectivity axiom for an ADT constructor. + * + * axiom { + * forall p_1: T_1, ..., p_n: T_n :: {C(p_1, ..., p_n)} p_i == D_Ci(C(p_1, ..., p_n)) + * } + * + * where C is the ADT constructor, D_i the destructor for i-th argument of C + * + * + * @param domain The domain the encoded constructor belongs to + * @param ac The adt constructor for which we want to generate the injectivity axioms + * @return A sequence of injectivity axiom + */ + private def generateInjectivityAxiom(domain: Domain)(ac: AdtConstructor): Seq[AnonymousDomainAxiom] = { + assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.") + val localVarDecl = ac.formalArgs.collect {case l:LocalVarDecl => l } + val localVars = ac.formalArgs.map { + case LocalVarDecl(name, typ) => + typ match { + case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(name))(ac.pos, ac.info, ac.errT) + case d => localVarTFromType(d, Some(name))(ac.pos, ac.info, ac.errT) + } + } + assert(localVarDecl.size == localVars.size, "AdtEncoder: An error in the ADT encoding occurred.") + + val constructorApp = DomainFuncApp( + ac.name, + localVars, + defaultTypeVarsFromDomain(domain) // TODO: not sure about that + )(ac.pos, ac.info, encodeAdtTypeAsDomainType(ac.typ), ac.adtName, ac.errT) + val trigger = Trigger(Seq(constructorApp))(ac.pos, ac.info, ac.errT) + + localVars.map { lv => + val right = DomainFuncApp( + getDestructorName(ac.adtName, lv.name), + Seq(constructorApp), + defaultTypeVarsFromDomain(domain) // TODO: not sure about that + )(ac.pos, ac.info, lv.typ, ac.adtName, ac.errT) + val eq = EqCmp(lv, right)(ac.pos, ac.info, ac.errT) + val forall = Forall(localVarDecl, Seq(trigger), eq)(ac.pos, ac.info, ac.errT) + AnonymousDomainAxiom(forall)(ac.pos, ac.info, ac.adtName, ac.errT) + } + } + + /** + * This method generates the corresponding exclusivity axioms for a sequence of constructors. + * + * axiom { + * forall t: AdtType :: {tag(t)}{D_11(t)}...{D_nn(t)} + * t == C_1(D_11(t), D_1n(t)) || ... || t == C_n(D_n1(t), D_nn(t)) + * } + * + * where D_ij is the destructor of the j-th argument of constructor C_i + * + * @param domain The domain the encoded ADT constructors belongs to + * @param acs The sequence adt constructor for which we want to generate the exclusivity axioms + * @return The exclusivity axiom + */ + private def generateExclusivityAxiom(domain: Domain)(acs: Seq[AdtConstructor]): AnonymousDomainAxiom = { + assert(acs.map(domain.name == _.adtName).forall(identity), "AdtEncoder: An error in the ADT encoding occurred.") + + val localVarDecl = localVarTDeclFromType(domainTypeFromDomain(domain))(domain.pos, domain.info, domain.errT) + val localVar = localVarTFromType(domainTypeFromDomain(domain))(domain.pos, domain.info, domain.errT) + val tagApp = DomainFuncApp( + getTagName(domain.name), + Seq(localVar), + (domain.typVars zip domain.typVars).toMap // TODO: not sure about that + )(domain.pos, domain.info, Int, domain.name, domain.errT) + + var destructorCalls: Seq[DomainFuncApp] = Seq() + val rhss = acs.map { ac => + destructorCalls = ac.formalArgs.map { + case LocalVarDecl(name, typ) => + DomainFuncApp( + getDestructorName(domain.name, name), + Seq(localVar), + defaultTypeVarsFromDomain(domain) // TODO: not sure about that + )(domain.pos, domain.info, typ, domain.name, domain.errT) + } + DomainFuncApp( + ac.name, + destructorCalls, + defaultTypeVarsFromDomain(domain) // TODO: not sure about that + )(domain.pos, domain.info, ac.typ, domain.name, domain.errT) + } + + val equalities = rhss.map { rhs => + EqCmp(localVar, rhs)(rhs.pos, rhs.info, rhs.errT) + } + .foldLeft(TrueLit()(domain.pos, domain.info, domain.errT) : Exp)({ + (acc, next) => Or(acc, next)(domain.pos, domain.info, domain.errT) + }) + + val triggers = (Seq(tagApp) ++ destructorCalls).map { t => Trigger(Seq(t))(domain.pos, domain.info, domain.errT)} + + AnonymousDomainAxiom( + Forall(Seq(localVarDecl), triggers, equalities)(domain.pos, domain.info, domain.errT) + )(domain.pos, domain.info, domain.name, domain.errT) + } + + /** + * This method generates the corresponding tag function for an ADT encoded as a domain + * + * @param domain The domain that encodes the ADT for which we want a tag function + * @return The tag function encoded as a domain function + */ + private def generateTagDeclaration(domain: Domain): DomainFunc = { + DomainFunc( + getTagName(domain.name), + Seq(localVarTDeclFromType(domainTypeFromDomain(domain))(domain.pos, domain.info, domain.errT)), + Int + )(domain.pos, domain.info, domain.name, domain.errT) + } + + /** + * This method generates the corresponding tag axiom for a ADT constructor + * + * axiom { + * forall p_1: T1 , p_2: T2 ,..., p_n: Tn :: {C(p_1,..,p_n)} tag(C(p_1,..,p_n)) = i + * } + * + * where i is specified by the parameter 'tag'. + * + * @param domain The domain that encodes the ADT and the ADT constructor belongs to for which we want a tag axiom + * @param ac An ADT constructor + * @param tag The assigned tag + * @return The generated tag axiom + */ + private def generateTagAxiom(domain:Domain)(ac: AdtConstructor, tag: Int): AnonymousDomainAxiom = { + assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.") + + val localVarDecl = ac.formalArgs.collect {case l:LocalVarDecl => l } + val localVars = ac.formalArgs.map { + case LocalVarDecl(name, typ) => + typ match { + case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(name))(ac.pos, ac.info, ac.errT) + case d => localVarTFromType(d, Some(name))(ac.pos, ac.info, ac.errT) + } + } + assert(localVarDecl.size == localVars.size, "AdtEncoder: An error in the ADT encoding occurred.") + + val constructorApp = DomainFuncApp( + ac.name, + localVars, + defaultTypeVarsFromDomain(domain) // TODO: not sure about that + )(ac.pos, ac.info, encodeAdtTypeAsDomainType(ac.typ), ac.adtName, ac.errT) + + val trigger = Trigger(Seq(constructorApp))(ac.pos, ac.info, ac.errT) + + val tagApp = DomainFuncApp( + getTagName(ac.adtName), + Seq(constructorApp), + defaultTypeVarsFromDomain(domain) // TODO: not sure about that + )(ac.pos, ac.info, Int, ac.adtName, ac.errT) + + val right = IntLit(tag)(ac.pos, ac.info, ac.errT) + val eq = EqCmp(tagApp, right)(ac.pos, ac.info, ac.errT) + val forall = Forall(localVarDecl, Seq(trigger), eq)(ac.pos, ac.info, ac.errT) + + if (ac.formalArgs.nonEmpty) { + AnonymousDomainAxiom(forall)(ac.pos, ac.info, ac.adtName, ac.errT) + } else { + AnonymousDomainAxiom(eq)(ac.pos, ac.info, ac.adtName, ac.errT) + } + + } + + /** + * This method traverses the entire AST and encodes any occurrences of an AdtType as a DomainType. Additionaly + * it handles DomainFuncApp and FuncApp specially since the argument 'typ' could also be an AdtType. * * @param program The program to encode * @return a program free of AdtType's */ - private def encodeAllAdtTypeAsDomainType(program: Program): Program = { + private def encodeAllAdtTypeAsDomainType[A <: Node](program: A, shouldForceCopy: Boolean = true): A = { StrategyBuilder.Slim[Node]({ - case at@AdtType(adtName, partialTypVarsMap) => DomainType(adtName, partialTypVarsMap)(at.typeParameters) - }).recurseFunc({ - case fa@FuncApp(_, args) => Seq(args, fa.typ) - case df@DomainFuncApp(_, args, typVarMap) => Seq(args, typVarMap, df.typ) - case d: Node => d.children.collect {case ar: AnyRef => ar} - }).execute(program) + case at@AdtType(name, partialTypVarsMap) => DomainType(name, partialTypVarsMap)(at.typeParameters) + case dfa@DomainFuncApp(name, args, typVarMap) => + DomainFuncApp(name, args, typVarMap)(dfa.pos, dfa.info, encodeAllAdtTypeAsDomainType(dfa.typ, shouldForceCopy = false), dfa.domainName, dfa.errT) + case fa@FuncApp(funcname, args) => + FuncApp(funcname, args)(fa.pos, fa.info, encodeAllAdtTypeAsDomainType(fa.typ, shouldForceCopy = false), fa.errT) + }, Traverse.BottomUp).forceCopy(shouldForceCopy).execute(program) } + /** Several helper methods */ + private def encodeAdtTypeAsDomainType(adtType: AdtType): DomainType = DomainType(adtType.adtName, adtType.partialTypVarsMap)(adtType.typeParameters) + private def domainTypeFromDomain(domain:Domain): DomainType = DomainType(domain, defaultTypeVarsFromDomain(domain)) + private def defaultTypeVarsFromDomain(domain:Domain): Map[TypeVar, Type] = (domain.typVars zip domain.typVars).toMap } From 2432860e6d33d4223d3f241c2e2368fd794d29d8 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 11 Mar 2022 10:23:53 +0100 Subject: [PATCH 25/50] The type variable mapping should be set if there are type variables --- .../viper/silver/plugin/standard/adt/AdtASTExtension.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala index c06507c8b..10a59c7ae 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala @@ -73,7 +73,7 @@ case class AdtConstructor(name: String, formalArgs: Seq[AnyLocalVarDecl]) object AdtConstructor { def apply(adt: Adt, name: String, formalArgs: Seq[AnyLocalVarDecl])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): AdtConstructor = { - AdtConstructor(name, formalArgs)(pos, info, AdtType(adt, Map.empty), adt.name, errT) + AdtConstructor(name, formalArgs)(pos, info, AdtType(adt, (adt.typVars zip adt.typVars).toMap), adt.name, errT) } } From ac8429c854468bee338bcf6fef3fd0f2ed06da61 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Fri, 11 Mar 2022 10:26:16 +0100 Subject: [PATCH 26/50] Extend ADT type checker -Disallow duplicate argument identifiers of constructors, otherwise we destructors can not be distinguished with the current design of ADT's --- .../plugin/standard/adt/AdtPASTExtension.scala | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 4a2460943..08db3484c 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -17,9 +17,18 @@ case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[P override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { t.checkMember(this) { - this.constructors foreach (_.typecheck(t, n)) + constructors foreach (_.typecheck(t, n)) + } + // Check that formalArg identifiers among all constructors are unique + val allFormalArgsIdentifier = constructors flatMap (_.formalArgs map { + case fad:PFormalArgDecl => fad.idndef.name + case _ => sys.error("AdtEncoder : Only PFormalArgDecl are allowed as arguments of an Adt constructor") + }) + if (allFormalArgsIdentifier.distinct != allFormalArgsIdentifier) { + Some(Seq("duplicate argument identifier in adt constructors")) + } else { + None } - None } override def translateMemberSignature(t: Translator): Adt = { From d3146c35c83dc4c45b0318cd5d7a342aecbcbb85 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Wed, 16 Mar 2022 09:41:34 +0100 Subject: [PATCH 27/50] Enable ADT constructor calls --- .../silver/plugin/standard/adt/AdtPlugin.scala | 8 ++++---- .../plugin/standard/adt/encoding/AdtEncoder.scala | 15 ++++++++++----- 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index da4f98bc8..a0ef1c76d 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -62,13 +62,13 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { } override def beforeResolve(input: PProgram): PProgram = { - // Replace PDomainType by PAdtType if a corresponding ADT exists, since they are automatically parsed as an PDomainType - // and there is no way to extend the parser to avoid this. + // Syntax of adt types and adt constructor calls can not be distinguished from ordinary viper syntax, hence we need + // the following transforming step before resolving. val declaredAdtNames = input.extensions.collect { case a: PAdt => a.idndef }.toSet + val declaredConstructorNames = input.extensions.collect { case a: PAdt => a.constructors.map(c => c.idndef) }.flatten.toSet StrategyBuilder.Slim[PNode]({ case pa@PDomainType(idnuse, args) if declaredAdtNames.exists(_.name == idnuse.name) => PAdtType(idnuse, args)(pa.pos) - }).recurseFunc({ - case d: PNode => d.children.collect {case ar: AnyRef => ar} + case pc@PCall(idnuse, args, typeAnnotated) if declaredConstructorNames.exists(_.name == idnuse.name) => PConstructorCall(idnuse, args, typeAnnotated)(pc.pos) }).execute(input) } diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala index 91ea5bce7..02bbc9360 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala @@ -25,9 +25,14 @@ class AdtEncoder (val program: Program) extends AdtNameManager { */ def encode(): Program = { - // In a first step encode all adt top level declarations - val encodedAdts: Seq[Domain] = program.extensions map {case a: Adt => encodeAdtAsDomain(a)} - val newProgram: Program = program.copy(domains = program.domains ++ encodedAdts, extensions = Seq())(program.pos, program.info, program.errT) + // In a first step encode all adt top level declarations and constructor calls + val newProgram: Program = StrategyBuilder.Slim[Node]({ + case p@Program(domains, fields, functions, predicates, methods, extensions) => + val remainingExtensions = extensions filter { case _:Adt => false; case _ => true } + val encodedAdtsAsDomains: Seq[Domain] = extensions collect { case a:Adt => encodeAdtAsDomain(a) } + Program(domains ++ encodedAdtsAsDomains, fields, functions, predicates, methods, remainingExtensions)(p.pos, p.info, p.errT) + case aca: AdtConstructorApp => encodeAdtConstructorApp(aca) + }, Traverse.BottomUp).execute(program) // In a second step encode all occurrences of AdtType's as DomainType's encodeAllAdtTypeAsDomainType(newProgram) @@ -105,12 +110,12 @@ class AdtEncoder (val program: Program) extends AdtNameManager { * @param aca The constructor application * @return The constructor application encoded as a domain function application */ - private def encodeAdtConstructorApp(aca: AdtConstructorApp) = { + private def encodeAdtConstructorApp(aca: AdtConstructorApp): DomainFuncApp = { DomainFuncApp( aca.name, aca.args, aca.typVarMap - )(_,_,aca.typ, aca.adtName, _) + )(aca.pos, aca.info, aca.typ, aca.adtName, aca.errT) } From 7c1f1710e1da8402568d826de87045bc02396ed8 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Wed, 16 Mar 2022 10:01:45 +0100 Subject: [PATCH 28/50] Adjust to updated plugin infrastructure -For expressions introduced by an extension there is now an overloaded method typecheck to check against an expected type --- .../viper/silver/plugin/standard/adt/AdtPASTExtension.scala | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 08db3484c..7ee5d6b31 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -306,6 +306,11 @@ case class PConstructorCall(constr: PIdnUse, args: Seq[PExp], typeAnnotated : Op override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = PAdtOpApp.typecheck(this)(t,n) + override def typecheck(t: TypeChecker, n: NameAnalyser, expected: PType): Option[Seq[String]] = { + t.checkTopTyped(this, Some(expected)) + None + } + override def forceSubstitution(ots: PTypeSubstitution): Unit = { val ts = adtTypeRenaming match { From 9b85472b7f44a5971e5966831588709114fb3bcd Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Wed, 16 Mar 2022 10:43:15 +0100 Subject: [PATCH 29/50] Prepare for adding destructors -Refactor PConstructorCall for potential code reuse --- .../standard/adt/AdtPASTExtension.scala | 70 ++++++++++--------- 1 file changed, 37 insertions(+), 33 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 7ee5d6b31..51e692ca8 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -202,7 +202,42 @@ object PAdtTypeKinds { } /** Common trait for ADT operator applications **/ -sealed trait PAdtOpApp extends PExtender with POpApp +sealed trait PAdtOpApp extends PExtender with POpApp { + + // Following fields are set during resolving, respectively in the typecheck method below + var adt: PAdt = null + var adtTypeRenaming: Option[PTypeRenaming] = None + var adtSubstitution: Option[PTypeSubstitution] = None + var _extraLocalTypeVariables: Set[PDomainType] = Set() + + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = PAdtOpApp.typecheck(this)(t,n) + + override def typecheck(t: TypeChecker, n: NameAnalyser, expected: PType): Option[Seq[String]] = { + t.checkTopTyped(this, Some(expected)) + None + } + + override def forceSubstitution(ots: PTypeSubstitution): Unit = { + + val ts = adtTypeRenaming match { + case Some(dtr) => + val s3 = PTypeSubstitution(dtr.mm.map(kv => kv._1 -> (ots.get(kv._2) match { + case Some(pt) => pt + case None => PTypeSubstitution.defaultType + }))) + assert(s3.m.keySet==dtr.mm.keySet) + assert(s3.m.forall(_._2.isGround)) + adtSubstitution = Some(s3) + dtr.mm.values.foldLeft(ots)( + (tss,s)=> if (tss.contains(s)) tss else tss.add(s, PTypeSubstitution.defaultType).get) + case _ => ots + } + super.forceSubstitution(ts) + } + + override def extraLocalTypeVariables: Set[PDomainType] = _extraLocalTypeVariables + +} object PAdtOpApp { /** @@ -295,39 +330,8 @@ case class PConstructorCall(constr: PIdnUse, args: Seq[PExp], typeAnnotated : Op } else List() } - // Following fields are set during resolving, respectively in the typecheck method below - var adt: PAdt = null + // Following fields is set during resolving, respectively in the typecheck method inherited from PAdtOpApp var constructor: PAdtConstructor = null - var adtTypeRenaming: Option[PTypeRenaming] = None - var _extraLocalTypeVariables: Set[PDomainType] = Set() - var adtSubstitution: Option[PTypeSubstitution] = None - - override def extraLocalTypeVariables: Set[PDomainType] = _extraLocalTypeVariables - - override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = PAdtOpApp.typecheck(this)(t,n) - - override def typecheck(t: TypeChecker, n: NameAnalyser, expected: PType): Option[Seq[String]] = { - t.checkTopTyped(this, Some(expected)) - None - } - - override def forceSubstitution(ots: PTypeSubstitution): Unit = { - - val ts = adtTypeRenaming match { - case Some(dtr) => - val s3 = PTypeSubstitution(dtr.mm.map(kv => kv._1 -> (ots.get(kv._2) match { - case Some(pt) => pt - case None => PTypeSubstitution.defaultType - }))) - assert(s3.m.keySet==dtr.mm.keySet) - assert(s3.m.forall(_._2.isGround)) - adtSubstitution = Some(s3) - dtr.mm.values.foldLeft(ots)( - (tss,s)=> if (tss.contains(s)) tss else tss.add(s, PTypeSubstitution.defaultType).get) - case _ => ots - } - super.forceSubstitution(ts) - } override def translateExp(t: Translator): Exp = { val constructor = PAdtConstructor.findAdtConstructor(constr, t) From 035c321babc834046482c34f15291d9fcca4b1cc Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Wed, 16 Mar 2022 16:19:58 +0100 Subject: [PATCH 30/50] Add an AST node for a destructor application -Additionally provide companion object to correctly set the destructor application given the name and the corresponding ADT. --- .../plugin/standard/adt/AdtASTExtension.scala | 49 +++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala index 10a59c7ae..48f10d73c 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala @@ -189,4 +189,53 @@ object AdtConstructorApp { AdtConstructorApp(constructor.name, args, typVarMap)(pos, info, constructor.typ.substitute(typVarMap), constructor.adtName, errT) } +/** + * This class represents an adt destructor application. See also the companion object below, which allows passing a + * Adt - this should be used in general for creation (so that typ is guaranteed to + * be set correctly) + * + * @param name The name of the argument of an ADT constructor the destructor corresponds to + * @param rcv An expression on with the the destructor is applied + * @param typVarMap Maps type parameters to (possibly concrete) types. May not map all + * type parameters, may even be empty. + * @param typ The return type of the destructor + * @param adtName The corresponding ADT name + */ +case class AdtDestructorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, Type])(val pos: Position, val info: Info, override val typ: Type, val adtName:String, val errT: ErrorTrafo) extends ExtensionExp { + + override lazy val check : Seq[ConsistencyError] = Consistency.checkPure(rcv) + + override def prettyPrint: PrettyPrintPrimitives#Cont = show(rcv) <> "." <> name + + override def extensionIsPure: Boolean = true + + override def extensionSubnodes: Seq[Node] = Seq(rcv) ++ typVarMap.keys ++ typVarMap.values + + override def verifyExtExp(): VerificationResult = { + assert(assertion = false, "AdtDestructorApp: verifyExtExp has not been implemented.") + Failure(Seq(ConsistencyError("AdtDestructorApp: verifyExtExp has not been implemented.", pos))) + } + + override def withChildren(children: Seq[Any], pos: Option[(Position, Position)], forceRewrite: Boolean): this.type = { + if (!forceRewrite && this.children == children && pos.isEmpty) + this + else { + assert(children.length == 3, s"AdtDestructorApp : expected length 3 but got ${children.length}") + val first = children.head.asInstanceOf[String] + val second = children(1).asInstanceOf[Exp] + val third = children(2).asInstanceOf[Map[TypeVar, Type]] + AdtDestructorApp(first, second, third)(this.pos, this.info, this.typ, this.adtName, this.errT).asInstanceOf[this.type] + } + } +} + +object AdtDestructorApp { + def apply(adt : Adt, name: String, rcv: Exp, typVarMap: Map[TypeVar, Type])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos) : AdtDestructorApp = { + val matchingConstructors = adt.constructors flatMap (c => c.formalArgs.filter { case LocalVarDecl(lvName, _) => lvName == name }) + assert(matchingConstructors.length == 1, s"AdtDestructorApp : expected length 1 but got ${matchingConstructors.length}") + val typ = matchingConstructors.head.asInstanceOf[LocalVarDecl].typ + AdtDestructorApp(name, rcv, typVarMap)(pos, info, typ.substitute(typVarMap), adt.name, errT) + } +} + From 5ea759c7088e73ac06c6afa4e800d2da5be596d1 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Wed, 16 Mar 2022 16:20:28 +0100 Subject: [PATCH 31/50] Add encoding for ADT destructor calls --- .../standard/adt/encoding/AdtEncoder.scala | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala index 02bbc9360..47eb8c7dd 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala @@ -8,7 +8,7 @@ package viper.silver.plugin.standard.adt.encoding import viper.silver.ast._ import viper.silver.ast.utility.rewriter.{StrategyBuilder, Traverse} -import viper.silver.plugin.standard.adt.{Adt, AdtConstructor, AdtConstructorApp, AdtType} +import viper.silver.plugin.standard.adt._ /** @@ -32,6 +32,7 @@ class AdtEncoder (val program: Program) extends AdtNameManager { val encodedAdtsAsDomains: Seq[Domain] = extensions collect { case a:Adt => encodeAdtAsDomain(a) } Program(domains ++ encodedAdtsAsDomains, fields, functions, predicates, methods, remainingExtensions)(p.pos, p.info, p.errT) case aca: AdtConstructorApp => encodeAdtConstructorApp(aca) + case ada: AdtDestructorApp => encodeAdtDestructorApp(ada) }, Traverse.BottomUp).execute(program) // In a second step encode all occurrences of AdtType's as DomainType's @@ -144,6 +145,20 @@ class AdtEncoder (val program: Program) extends AdtNameManager { } } + /** + * This methods encode an ADT destructor application as a domain function application + * + * @param ada The destructor application + * @return The destructor application encoded as a domain function application + */ + private def encodeAdtDestructorApp(ada: AdtDestructorApp): DomainFuncApp = { + DomainFuncApp( + getDestructorName(ada.adtName, ada.name), + Seq(ada.rcv), + ada.typVarMap + )(ada.pos, ada.info, ada.typ, ada.adtName, ada.errT) + } + /** * This method generates the corresponding injectivity axiom for an ADT constructor. * From 09b3cdda502252f52b9c7f3e6fbb0291e99fce77 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Wed, 16 Mar 2022 16:25:35 +0100 Subject: [PATCH 32/50] Add a Parser AST node for destructor calls and implement typechecking --- .../standard/adt/AdtPASTExtension.scala | 65 +++++++++++++++++-- 1 file changed, 60 insertions(+), 5 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 51e692ca8..d60264f7d 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -6,6 +6,7 @@ package viper.silver.plugin.standard.adt +import viper.silver.FastMessaging import viper.silver.ast._ import viper.silver.parser._ import viper.silver.plugin.standard.adt.PAdtConstructor.findAdtConstructor @@ -272,16 +273,37 @@ object PAdtOpApp { } if (!nestedTypeError) { - val ad = t.names.definition(t.curMember)(constr).asInstanceOf[PAdtConstructor] - pcc.constructor = ad - t.ensure(ad.formalArgs.size == args.size, pcc, "wrong number of arguments") - val adt = t.names.definition(t.curMember)(ad.adtName).asInstanceOf[PAdt] + val ac = t.names.definition(t.curMember)(constr).asInstanceOf[PAdtConstructor] + pcc.constructor = ac + t.ensure(ac.formalArgs.size == args.size, pcc, "wrong number of arguments") + val adt = t.names.definition(t.curMember)(ac.adtName).asInstanceOf[PAdt] pcc.adt = adt val fdtv = PTypeVar.freshTypeSubstitution((adt.typVars map (tv => tv.idndef.name)).distinct) //fresh domain type variables pcc.adtTypeRenaming = Some(fdtv) pcc._extraLocalTypeVariables = (adt.typVars map (tv => PTypeVar(tv.idndef.name))).toSet extraReturnTypeConstraint = pcc.typeAnnotated } + + case pdc@PDestructorCall(name, _) => + pdc.args.head.typ match { + case at:PAdtType => + val adt = t.names.definition(t.curMember)(at.adt).asInstanceOf[PAdt] + pdc.adt = adt + val matchingConstructorArgs: Seq[PFormalArgDecl] = adt.constructors flatMap (c => c.formalArgs.collect { case fad@PFormalArgDecl(idndef, _) if idndef.name == name => fad }) + if (matchingConstructorArgs.nonEmpty) { + pdc.matchingConstructorArg = matchingConstructorArgs.head + val fdtv = PTypeVar.freshTypeSubstitution((adt.typVars map (tv => tv.idndef.name)).distinct) //fresh domain type variables + pdc.adtTypeRenaming = Some(fdtv) + pdc._extraLocalTypeVariables = (adt.typVars map (tv => PTypeVar(tv.idndef.name))).toSet + } else { + nestedTypeError = true + t.messages ++= FastMessaging.message(pdc, "no matching destructor found") + } + case _ => + nestedTypeError = true + t.messages ++= FastMessaging.message(pdc, "expected an adt") + } + case _ => // TODO: Handle the remaining ADT operation applications (e.g discriminators, destructors) here } @@ -330,7 +352,7 @@ case class PConstructorCall(constr: PIdnUse, args: Seq[PExp], typeAnnotated : Op } else List() } - // Following fields is set during resolving, respectively in the typecheck method inherited from PAdtOpApp + // Following field is set during resolving, respectively in the typecheck method inherited from PAdtOpApp var constructor: PAdtConstructor = null override def translateExp(t: Translator): Exp = { @@ -349,4 +371,37 @@ case class PConstructorCall(constr: PIdnUse, args: Seq[PExp], typeAnnotated : Op } } +} + +case class PDestructorCall(name: String, rcv: PExp)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PAdtOpApp { + override def opName: String = name + override def args: Seq[PExp] = Seq(rcv) + override def getSubnodes(): Seq[PNode] = Seq(rcv) + + override def signatures: List[PTypeSubstitution] = if (adt != null && matchingConstructorArg != null) { + assert(args.length == 1, s"PDestructorCall: Expected args to be of length 1 but was of length ${args.length}") + List( + new PTypeSubstitution( + args.indices.map(i => POpApp.pArg(i).domain.name -> adt.getAdtType.substitute(adtTypeRenaming.get)) :+ + (POpApp.pRes.domain.name -> matchingConstructorArg.typ.substitute(adtTypeRenaming.get))) + ) + } else List() + + // Following field is set during resolving, respectively in the typecheck method inherited from PAdtOpApp + var matchingConstructorArg: PFormalArgDecl = null + + override def translateExp(t: Translator): Exp = { + val actualRcv = t.exp(rcv) + val so : Option[Map[TypeVar, Type]] = adtSubstitution match { + case Some(ps) => Some(ps.m.map(kv=>TypeVar(kv._1)->t.ttyp(kv._2))) + case None => None + } + so match { + case Some(s) => + val adt = t.getMembers()(this.adt.idndef.name).asInstanceOf[Adt] + assert(s.keys.toSet == adt.typVars.toSet) + AdtDestructorApp(adt, name, actualRcv, s)(t.liftPos(this)) + case _ => sys.error("type unification error - should report and not crash") + } + } } \ No newline at end of file From eb28ae3d0b5a925ffc284672580c368091be1f14 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Wed, 16 Mar 2022 16:51:22 +0100 Subject: [PATCH 33/50] Enable destructor calls -Since the syntax of field accesses and destructor applications can not be distinguished, we need to transform PFieldAccess's to PDestructorCall's if there is such a destructor --- .../scala/viper/silver/plugin/standard/adt/AdtPlugin.scala | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index a0ef1c76d..a2d158d55 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -62,13 +62,16 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { } override def beforeResolve(input: PProgram): PProgram = { - // Syntax of adt types and adt constructor calls can not be distinguished from ordinary viper syntax, hence we need - // the following transforming step before resolving. + // Syntax of adt types, adt constructor calls and destructor calls can not be distinguished from ordinary + // viper syntax, hence we need the following transforming step before resolving. val declaredAdtNames = input.extensions.collect { case a: PAdt => a.idndef }.toSet val declaredConstructorNames = input.extensions.collect { case a: PAdt => a.constructors.map(c => c.idndef) }.flatten.toSet + val declaredConstructorArgsNames = input.extensions.collect { case a: PAdt => + a.constructors flatMap ( c => c.formalArgs collect {case PFormalArgDecl(idndef, _) => idndef})}.flatten.toSet StrategyBuilder.Slim[PNode]({ case pa@PDomainType(idnuse, args) if declaredAdtNames.exists(_.name == idnuse.name) => PAdtType(idnuse, args)(pa.pos) case pc@PCall(idnuse, args, typeAnnotated) if declaredConstructorNames.exists(_.name == idnuse.name) => PConstructorCall(idnuse, args, typeAnnotated)(pc.pos) + case pfa@PFieldAccess(rcv, idnuse) if declaredConstructorArgsNames.exists(_.name == idnuse.name) => PDestructorCall(idnuse.name, rcv)(pfa.pos) }).execute(input) } From ee6ca75b5ae70d521ae80e3c0c31a98e5b83a2b6 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Thu, 17 Mar 2022 17:16:29 +0100 Subject: [PATCH 34/50] Add an AST node for an adt discriminator application --- .../plugin/standard/adt/AdtASTExtension.scala | 47 +++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala index 48f10d73c..f478b5f6d 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala @@ -238,4 +238,51 @@ object AdtDestructorApp { } } +/** + * This class represents an adt discriminator application. See also the companion object below, which allows passing a + * Adt - this should be used in general for creation (so that adtName is guaranteed to + * be set correctly) + * + * @param name The name of the argument of an ADT constructor the destructor corresponds to + * @param rcv An expression on with the the destructor is applied + * @param typVarMap Maps type parameters to (possibly concrete) types. May not map all + * type parameters, may even be empty. + * @param adtName The corresponding ADT name + */ +case class AdtDiscriminatorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, Type])(val pos: Position, val info: Info, val adtName:String, val errT: ErrorTrafo) extends ExtensionExp { + + override def typ: Type = Bool + + override lazy val check : Seq[ConsistencyError] = Consistency.checkPure(rcv) + + override def prettyPrint: PrettyPrintPrimitives#Cont = show(rcv) <> "." <> name <> "?" + + override def extensionIsPure: Boolean = true + + override def extensionSubnodes: Seq[Node] = Seq(rcv) ++ typVarMap.keys ++ typVarMap.values + + override def verifyExtExp(): VerificationResult = { + assert(assertion = false, "AdtDiscriminatorApp: verifyExtExp has not been implemented.") + Failure(Seq(ConsistencyError("AdtDiscriminatorApp: verifyExtExp has not been implemented.", pos))) + } + + override def withChildren(children: Seq[Any], pos: Option[(Position, Position)], forceRewrite: Boolean): this.type = { + if (!forceRewrite && this.children == children && pos.isEmpty) + this + else { + assert(children.length == 3, s"AdtDestructorApp : expected length 3 but got ${children.length}") + val first = children.head.asInstanceOf[String] + val second = children(1).asInstanceOf[Exp] + val third = children(2).asInstanceOf[Map[TypeVar, Type]] + AdtDiscriminatorApp(first, second, third)(this.pos, this.info, this.adtName, this.errT).asInstanceOf[this.type] + } + } + +} + +object AdtDiscriminatorApp { + def apply(adt : Adt, name: String, rcv: Exp, typVarMap: Map[TypeVar, Type])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos) : AdtDiscriminatorApp = { + AdtDiscriminatorApp(name, rcv, typVarMap)(pos, info, adt.name, errT) + } +} From 6e42ce7d763ff74dc35250b2c193b74e66238ed9 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Thu, 17 Mar 2022 17:20:18 +0100 Subject: [PATCH 35/50] Add encoding for adt discriminator applications -Additionally add a getTag function that maps adt constructor's to its tag identifier --- .../standard/adt/encoding/AdtEncoder.scala | 46 ++++++++++++++++--- 1 file changed, 39 insertions(+), 7 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala index 47eb8c7dd..7d08f9c92 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala @@ -16,12 +16,19 @@ import viper.silver.plugin.standard.adt._ * * @param program The program containing ADT AST nodes, we want to encode. */ -class AdtEncoder (val program: Program) extends AdtNameManager { +class AdtEncoder(val program: Program) extends AdtNameManager { + + /** + * This is field holding the mappings of the adt constructors tag identifier. + */ + private val tagMapping: Map[String, Map[String, Int]] = (program.extensions collect { + case a:Adt => (a.name, a.constructors.map(_.name).sorted.zipWithIndex.toMap) + }).toMap /** * This method encodes all ADT related AST nodes to normal AST nodes. * - * @return + * @return The encoded program. */ def encode(): Program = { @@ -33,12 +40,22 @@ class AdtEncoder (val program: Program) extends AdtNameManager { Program(domains ++ encodedAdtsAsDomains, fields, functions, predicates, methods, remainingExtensions)(p.pos, p.info, p.errT) case aca: AdtConstructorApp => encodeAdtConstructorApp(aca) case ada: AdtDestructorApp => encodeAdtDestructorApp(ada) + case ada: AdtDiscriminatorApp => encodeAdtDiscriminatorApp(ada) }, Traverse.BottomUp).execute(program) // In a second step encode all occurrences of AdtType's as DomainType's encodeAllAdtTypeAsDomainType(newProgram) } + /** + * This method return the tag identifier given a adt constructor name and its correpsonding adt name + * + * @param adtName The name of the adt + * @param contrName The name of the adt constructor we want the tag identifier + * @return The queried tag identifier + */ + private def getTag(adtName: String)(contrName:String) = tagMapping(adtName)(contrName) + /** * This method takes an ADT and encodes it as a Domain. Especially it does * 1. Maps Adt to Domain @@ -57,7 +74,7 @@ class AdtEncoder (val program: Program) extends AdtNameManager { val functions: Seq[DomainFunc] = (constructors map encodeAdtConstructorAsDomainFunc(domain)) ++ (constructors flatMap generateDestructorDeclarations(domain)) ++ Seq(generateTagDeclaration(domain)) val axioms = (constructors flatMap generateInjectivityAxiom(domain)) ++ - (constructors.zipWithIndex map { case (c, i) => generateTagAxiom(domain)(c, i) }) ++ Seq(generateExclusivityAxiom(domain)(constructors)) + (constructors map generateTagAxiom(domain)) ++ Seq(generateExclusivityAxiom(domain)(constructors)) domain.copy(functions = functions, axioms = axioms)(adt.pos, adt.info, adt.errT) } } @@ -159,6 +176,22 @@ class AdtEncoder (val program: Program) extends AdtNameManager { )(ada.pos, ada.info, ada.typ, ada.adtName, ada.errT) } + /** + * This methods encode an ADT discriminator application as an equality expression + * + * @param ada The discriminator application + * @return The discriminator application encoded as an equality expression + */ + private def encodeAdtDiscriminatorApp(ada: AdtDiscriminatorApp): EqCmp = { + val tagApp = DomainFuncApp( + getTagName(ada.adtName), + Seq(ada.rcv), + ada.typVarMap // TODO: not sure about that + )(ada.pos, ada.info, Int, ada.adtName, ada.errT) + + EqCmp(tagApp, IntLit(getTag(ada.adtName)(ada.name))(ada.pos, ada.info, ada.errT))(ada.pos, ada.info, ada.errT) + } + /** * This method generates the corresponding injectivity axiom for an ADT constructor. * @@ -283,12 +316,11 @@ class AdtEncoder (val program: Program) extends AdtNameManager { * * where i is specified by the parameter 'tag'. * - * @param domain The domain that encodes the ADT and the ADT constructor belongs to for which we want a tag axiom + * @param domain The domain that encodes the ADT the constructor belongs to for which we want a tag axiom * @param ac An ADT constructor - * @param tag The assigned tag * @return The generated tag axiom */ - private def generateTagAxiom(domain:Domain)(ac: AdtConstructor, tag: Int): AnonymousDomainAxiom = { + private def generateTagAxiom(domain:Domain)(ac: AdtConstructor): AnonymousDomainAxiom = { assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.") val localVarDecl = ac.formalArgs.collect {case l:LocalVarDecl => l } @@ -315,7 +347,7 @@ class AdtEncoder (val program: Program) extends AdtNameManager { defaultTypeVarsFromDomain(domain) // TODO: not sure about that )(ac.pos, ac.info, Int, ac.adtName, ac.errT) - val right = IntLit(tag)(ac.pos, ac.info, ac.errT) + val right = IntLit(getTag(domain.name)(ac.name))(ac.pos, ac.info, ac.errT) val eq = EqCmp(tagApp, right)(ac.pos, ac.info, ac.errT) val forall = Forall(localVarDecl, Seq(trigger), eq)(ac.pos, ac.info, ac.errT) From be46785c230d49499cfe6e03d1810557dd504e43 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Thu, 17 Mar 2022 17:21:56 +0100 Subject: [PATCH 36/50] Add parser AST node for adt discriminator call -Implement the type-checking for discriminator calls -Implement the translation to an AST node for discriminator calls --- .../standard/adt/AdtPASTExtension.scala | 42 ++++++++++++++++++- 1 file changed, 41 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index d60264f7d..f575dfebb 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -304,7 +304,15 @@ object PAdtOpApp { t.messages ++= FastMessaging.message(pdc, "expected an adt") } - case _ => // TODO: Handle the remaining ADT operation applications (e.g discriminators, destructors) here + case pdc@PDiscriminatorCall(name, _) => + val ac = t.names.definition(t.curMember)(name).asInstanceOf[PAdtConstructor] + val adt = t.names.definition(t.curMember)(ac.adtName).asInstanceOf[PAdt] + pdc.adt = adt + val fdtv = PTypeVar.freshTypeSubstitution((adt.typVars map (tv => tv.idndef.name)).distinct) //fresh domain type variables + pdc.adtTypeRenaming = Some(fdtv) + pdc._extraLocalTypeVariables = (adt.typVars map (tv => PTypeVar(tv.idndef.name))).toSet + + case _ => sys.error("PAdtOpApp#typecheck: unexpectable type") } if (poa.signatures.nonEmpty && poa.args.forall(_.typeSubstitutions.nonEmpty) && !nestedTypeError) { @@ -404,4 +412,36 @@ case class PDestructorCall(name: String, rcv: PExp)(val pos: (Position, Position case _ => sys.error("type unification error - should report and not crash") } } +} + +case class PDiscriminatorCall(name: PIdnUse, rcv: PExp)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PAdtOpApp { + override def opName: String = "." + name + "?" + + override def args: Seq[PExp] = Seq(rcv) + + override def getSubnodes(): Seq[PNode] = Seq(name, rcv) + + override def signatures: List[PTypeSubstitution] = if (adt != null) { + assert(args.length == 1, s"PDiscriminatorCall: Expected args to be of length 1 but was of length ${args.length}") + List( + new PTypeSubstitution( + args.indices.map(i => POpApp.pArg(i).domain.name -> adt.getAdtType.substitute(adtTypeRenaming.get)) :+ + (POpApp.pRes.domain.name -> TypeHelper.Bool)) + ) + } else List() + + override def translateExp(t: Translator): Exp = { + val actualRcv = t.exp(rcv) + val so : Option[Map[TypeVar, Type]] = adtSubstitution match { + case Some(ps) => Some(ps.m.map(kv=>TypeVar(kv._1)->t.ttyp(kv._2))) + case None => None + } + so match { + case Some(s) => + val adt = t.getMembers()(this.adt.idndef.name).asInstanceOf[Adt] + assert(s.keys.toSet == adt.typVars.toSet) + AdtDiscriminatorApp(adt, name.name, actualRcv, s)(t.liftPos(this)) + case _ => sys.error("type unification error - should report and not crash") + } + } } \ No newline at end of file From 3cf21edb0994d1b47328fce58cfa9295fb8d26a9 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Mon, 21 Mar 2022 14:28:03 +0100 Subject: [PATCH 37/50] Fix issue in resolving constructor calls with wrong number of arguments --- .../viper/silver/plugin/standard/adt/AdtPASTExtension.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index f575dfebb..a1f0be546 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -351,7 +351,7 @@ case class PConstructorCall(constr: PIdnUse, args: Seq[PExp], typeAnnotated : Op override def getSubnodes(): Seq[PNode] = Seq(constr) ++ args ++ (typeAnnotated match { case Some(t) => Seq(t) case None => Nil}) override def signatures: List[PTypeSubstitution] = { - if (adt != null && constructor != null) { + if (adt != null && constructor != null && constructor.formalArgs.size == args.size) { List( new PTypeSubstitution( args.indices.map(i => POpApp.pArg(i).domain.name -> constructor.formalArgs(i).typ.substitute(adtTypeRenaming.get)) :+ From 8a2530e1474c25ddd1a86da7d3b4de137c467716 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Tue, 22 Mar 2022 13:55:15 +0100 Subject: [PATCH 38/50] Fix issue in tag axiom -Note that (true or A or B ) is not the same as (A or B) -But (false or A or B ) is the same as (A or B) --- .../viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala index 7d08f9c92..6e94bd487 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala @@ -282,7 +282,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager { val equalities = rhss.map { rhs => EqCmp(localVar, rhs)(rhs.pos, rhs.info, rhs.errT) } - .foldLeft(TrueLit()(domain.pos, domain.info, domain.errT) : Exp)({ + .foldLeft(FalseLit()(domain.pos, domain.info, domain.errT) : Exp)({ (acc, next) => Or(acc, next)(domain.pos, domain.info, domain.errT) }) From 9ba76b88a205ea333f25dcd9fa5800cb0ae17011 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Tue, 22 Mar 2022 17:03:51 +0100 Subject: [PATCH 39/50] Fix issue in AdtNameManager -There was a bug that a new mapping for a name is added, despite already having a mapping for that name --- .../plugin/standard/adt/encoding/AdtNameManager.scala | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala index b9a0da6dc..2a8140cd6 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala @@ -59,12 +59,10 @@ trait AdtNameManager { * @return */ private def getName(trueName: String): String = { - - var newName = trueName - if (!adtNameMappings.contains(trueName) && containsName(trueName)) { - newName = uniqueName(trueName) + if (!adtNameMappings.contains(trueName)) { + val newName = if (containsName(trueName)) uniqueName(trueName) else trueName + adtNameMappings.addOne((trueName, newName)) } - adtNameMappings.addOne((trueName, newName)) adtNameMappings(trueName) } From 71b1c4defbe1b303c50d7a21a0650029e026832c Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Tue, 22 Mar 2022 17:06:23 +0100 Subject: [PATCH 40/50] Fix issue in resolving discriminator calls -There might happen that 'name' corresponds to an identifier of a method, function, etc. which caused an exception. --- .../standard/adt/AdtPASTExtension.scala | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index a1f0be546..2fa156560 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -301,16 +301,21 @@ object PAdtOpApp { } case _ => nestedTypeError = true - t.messages ++= FastMessaging.message(pdc, "expected an adt") + t.messages ++= FastMessaging.message(pdc, "expected an adt as receiver") } case pdc@PDiscriminatorCall(name, _) => - val ac = t.names.definition(t.curMember)(name).asInstanceOf[PAdtConstructor] - val adt = t.names.definition(t.curMember)(ac.adtName).asInstanceOf[PAdt] - pdc.adt = adt - val fdtv = PTypeVar.freshTypeSubstitution((adt.typVars map (tv => tv.idndef.name)).distinct) //fresh domain type variables - pdc.adtTypeRenaming = Some(fdtv) - pdc._extraLocalTypeVariables = (adt.typVars map (tv => PTypeVar(tv.idndef.name))).toSet + t.names.definition(t.curMember)(name) match { + case ac: PAdtConstructor => + val adt = t.names.definition(t.curMember)(ac.adtName).asInstanceOf[PAdt] + pdc.adt = adt + val fdtv = PTypeVar.freshTypeSubstitution((adt.typVars map (tv => tv.idndef.name)).distinct) //fresh domain type variables + pdc.adtTypeRenaming = Some(fdtv) + pdc._extraLocalTypeVariables = (adt.typVars map (tv => PTypeVar(tv.idndef.name))).toSet + case _ => + nestedTypeError = true + t.messages ++= FastMessaging.message(pdc, "invalid adt discriminator") + } case _ => sys.error("PAdtOpApp#typecheck: unexpectable type") } From a761dcb4b590cddc754472530cec1b0a9791970c Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Tue, 29 Mar 2022 17:17:46 +0200 Subject: [PATCH 41/50] Fix the discriminator syntax and its parsing --- .../standard/adt/AdtPASTExtension.scala | 13 +++++++++++- .../plugin/standard/adt/AdtPlugin.scala | 20 +++++++++++++++---- 2 files changed, 28 insertions(+), 5 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 2fa156560..65ea1b7dd 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -11,6 +11,8 @@ import viper.silver.ast._ import viper.silver.parser._ import viper.silver.plugin.standard.adt.PAdtConstructor.findAdtConstructor +import scala.util.{Success, Try} + case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[PAdtConstructor])(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { @@ -85,6 +87,15 @@ case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])( override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { this.formalArgs foreach (a => t.check(a.typ)) + + // Check if there are name clashes for the corresponding discriminator, if so we raise a type-check error + Try { + n.definition(t.curMember)(PIdnUse("is" + idndef.name)(idndef.pos)) + } match { + case Success(decl) => + t.messages ++= FastMessaging.message(idndef, "corresponding adt discriminator identifier `" + decl.idndef.name + "' at " + idndef.pos._1 + " is shadowed at " + decl.idndef.pos._1) + case _ => + } None } @@ -420,7 +431,7 @@ case class PDestructorCall(name: String, rcv: PExp)(val pos: (Position, Position } case class PDiscriminatorCall(name: PIdnUse, rcv: PExp)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PAdtOpApp { - override def opName: String = "." + name + "?" + override def opName: String = "is" + name.name override def args: Seq[PExp] = Seq(rcv) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index a2d158d55..cde1327ae 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -53,11 +53,10 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { def adtConstructorSignature[_: P]: P[(PIdnDef, Seq[PAnyFormalArgDecl])] = P(idndef ~ "(" ~ anyFormalArgList ~ ")") override def beforeParse(input: String, isImported: Boolean): String = { - // Add new keyword + // Add new parser adt declaration keyword ParserExtension.addNewKeywords(Set[String](AdtKeyword)) - // Add new declaration + // Add new parser for adt declaration ParserExtension.addNewDeclAtEnd(adtDecl(_)) - // TODO: Add custom parsers input } @@ -68,11 +67,24 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { val declaredConstructorNames = input.extensions.collect { case a: PAdt => a.constructors.map(c => c.idndef) }.flatten.toSet val declaredConstructorArgsNames = input.extensions.collect { case a: PAdt => a.constructors flatMap ( c => c.formalArgs collect {case PFormalArgDecl(idndef, _) => idndef})}.flatten.toSet - StrategyBuilder.Slim[PNode]({ + def transformStrategy[T <: PNode](input: T): T = StrategyBuilder.Slim[PNode]({ case pa@PDomainType(idnuse, args) if declaredAdtNames.exists(_.name == idnuse.name) => PAdtType(idnuse, args)(pa.pos) case pc@PCall(idnuse, args, typeAnnotated) if declaredConstructorNames.exists(_.name == idnuse.name) => PConstructorCall(idnuse, args, typeAnnotated)(pc.pos) + // A destructor call or discriminator call might be parsed as left-hand side of a field assignment, which is illegal. Hence in this case + // we simply treat the calls as an ordinary field access, which results in an identifier not found error. + case pfa@PFieldAssign(fieldAcc, rhs) if declaredConstructorArgsNames.exists(_.name == fieldAcc.idnuse.name) || + declaredConstructorNames.exists("is" + _.name == fieldAcc.idnuse.name) => + PFieldAssign(PFieldAccess(transformStrategy(fieldAcc.rcv), fieldAcc.idnuse)(fieldAcc.pos), transformStrategy(rhs))(pfa.pos) case pfa@PFieldAccess(rcv, idnuse) if declaredConstructorArgsNames.exists(_.name == idnuse.name) => PDestructorCall(idnuse.name, rcv)(pfa.pos) + case pfa@PFieldAccess(rcv, idnuse) if declaredConstructorNames.exists("is" + _.name == idnuse.name) => PDiscriminatorCall(PIdnUse(idnuse.name.substring(2))(idnuse.pos), rcv)(pfa.pos) + }).recurseFunc({ + // Stop the recursion if a destructor call or discriminator call is parsed as left-hand side of a field assignment + case PFieldAssign(fieldAcc, _) if declaredConstructorArgsNames.exists(_.name == fieldAcc.idnuse.name) || + declaredConstructorNames.exists("is" + _.name == fieldAcc.idnuse.name) => Seq() + case n: PNode => n.children collect {case ar: AnyRef => ar} }).execute(input) + + transformStrategy(input) } override def beforeVerify(input: Program): Program = { From 4fd759e8662f33263048b2714568f1b20d9c5e74 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Tue, 29 Mar 2022 17:22:59 +0200 Subject: [PATCH 42/50] Add test resources for adt plugin --- src/test/resources/adt/adt_as_fields_1.vpr | 25 ++++ src/test/resources/adt/constructors_1.vpr | 33 +++++ src/test/resources/adt/constructors_2.vpr | 26 ++++ src/test/resources/adt/constructors_3.vpr | 23 ++++ src/test/resources/adt/declarations_1.vpr | 35 ++++++ src/test/resources/adt/declarations_2.vpr | 15 +++ src/test/resources/adt/declarations_3.vpr | 6 + src/test/resources/adt/declarations_4.vpr | 6 + src/test/resources/adt/declarations_5.vpr | 9 ++ src/test/resources/adt/destructors_1.vpr | 79 ++++++++++++ src/test/resources/adt/destructors_2.vpr | 25 ++++ src/test/resources/adt/destructors_3.vpr | 35 ++++++ src/test/resources/adt/destructors_4.vpr | 22 ++++ src/test/resources/adt/destructors_5.vpr | 31 +++++ src/test/resources/adt/destructors_6.vpr | 22 ++++ src/test/resources/adt/discriminators_1.vpr | 35 ++++++ src/test/resources/adt/discriminators_2.vpr | 28 +++++ src/test/resources/adt/discriminators_3.vpr | 16 +++ src/test/resources/adt/discriminators_4.vpr | 15 +++ src/test/resources/adt/discriminators_5.vpr | 8 ++ src/test/resources/adt/discriminators_6.vpr | 10 ++ src/test/resources/adt/discriminators_7.vpr | 30 +++++ src/test/resources/adt/encoding_1.vpr | 32 +++++ src/test/resources/adt/encoding_2.vpr | 18 +++ src/test/resources/adt/equality_1.vpr | 19 +++ src/test/resources/adt/equality_2.vpr | 35 ++++++ src/test/resources/adt/example_1.vpr | 54 +++++++++ src/test/resources/adt/example_2.vpr | 114 ++++++++++++++++++ src/test/resources/adt/example_3.vpr | 59 +++++++++ src/test/resources/adt/example_4.vpr | 77 ++++++++++++ src/test/resources/adt/example_5.vpr | 71 +++++++++++ src/test/resources/adt/soundness_1.vpr | 41 +++++++ src/test/resources/adt/type_ascriptions_1.vpr | 15 +++ .../resources/adt/variable_declarations_1.vpr | 34 ++++++ .../resources/adt/variable_declarations_2.vpr | 27 +++++ 35 files changed, 1130 insertions(+) create mode 100644 src/test/resources/adt/adt_as_fields_1.vpr create mode 100644 src/test/resources/adt/constructors_1.vpr create mode 100644 src/test/resources/adt/constructors_2.vpr create mode 100644 src/test/resources/adt/constructors_3.vpr create mode 100644 src/test/resources/adt/declarations_1.vpr create mode 100644 src/test/resources/adt/declarations_2.vpr create mode 100644 src/test/resources/adt/declarations_3.vpr create mode 100644 src/test/resources/adt/declarations_4.vpr create mode 100644 src/test/resources/adt/declarations_5.vpr create mode 100644 src/test/resources/adt/destructors_1.vpr create mode 100644 src/test/resources/adt/destructors_2.vpr create mode 100644 src/test/resources/adt/destructors_3.vpr create mode 100644 src/test/resources/adt/destructors_4.vpr create mode 100644 src/test/resources/adt/destructors_5.vpr create mode 100644 src/test/resources/adt/destructors_6.vpr create mode 100644 src/test/resources/adt/discriminators_1.vpr create mode 100644 src/test/resources/adt/discriminators_2.vpr create mode 100644 src/test/resources/adt/discriminators_3.vpr create mode 100644 src/test/resources/adt/discriminators_4.vpr create mode 100644 src/test/resources/adt/discriminators_5.vpr create mode 100644 src/test/resources/adt/discriminators_6.vpr create mode 100644 src/test/resources/adt/discriminators_7.vpr create mode 100644 src/test/resources/adt/encoding_1.vpr create mode 100644 src/test/resources/adt/encoding_2.vpr create mode 100644 src/test/resources/adt/equality_1.vpr create mode 100644 src/test/resources/adt/equality_2.vpr create mode 100644 src/test/resources/adt/example_1.vpr create mode 100644 src/test/resources/adt/example_2.vpr create mode 100644 src/test/resources/adt/example_3.vpr create mode 100644 src/test/resources/adt/example_4.vpr create mode 100644 src/test/resources/adt/example_5.vpr create mode 100644 src/test/resources/adt/soundness_1.vpr create mode 100644 src/test/resources/adt/type_ascriptions_1.vpr create mode 100644 src/test/resources/adt/variable_declarations_1.vpr create mode 100644 src/test/resources/adt/variable_declarations_2.vpr diff --git a/src/test/resources/adt/adt_as_fields_1.vpr b/src/test/resources/adt/adt_as_fields_1.vpr new file mode 100644 index 000000000..def0c7949 --- /dev/null +++ b/src/test/resources/adt/adt_as_fields_1.vpr @@ -0,0 +1,25 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + +field list:List[Int] +field condtion:Bool + +method adt_as_fields_1() +{ + var f: Ref + f := new (list, condtion) + assert f.list.isNil || f.list.isCons + + + f.list := Cons(42, Nil()) + assert !f.list.tail.isCons + + f.list := Cons(42, Nil()).tail + f.condtion := Cons(42, Nil()).isCons + + assert f.list == Nil() + assert f.condtion == true + +} \ No newline at end of file diff --git a/src/test/resources/adt/constructors_1.vpr b/src/test/resources/adt/constructors_1.vpr new file mode 100644 index 000000000..b278a9161 --- /dev/null +++ b/src/test/resources/adt/constructors_1.vpr @@ -0,0 +1,33 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + +method constructors_1() +{ + var list1: List[Int] + list1 := Cons(1, Cons(1, Cons(1, Cons(1, Cons(1, Cons(1, Nil())))))) + + var list2: List[List[Bool]] + list2 := Cons(Cons(true, Cons(true, Cons(true, Cons(true, Cons(true, Cons(true, Nil())))))), Nil()) + + var list3: List[Seq[Int]] + list3 := Cons(Seq(1,2,3), Nil()) + + var list4: List[Set[Bool]] + list4 := Cons(Set(true, false), Nil()) + + + var list5: List[Map[Int, Int]] + var m1: Map[Int, Int] + m1 := m1[1 := 1] + list5 := Cons(m1, Nil()) + + var list6: List[Map[Int, List[Int]]] + var m2: Map[Int, List[Int]] + m2 := m2[1 := Cons(1, Cons(2, Nil()))] + list6 := Cons(m2, Cons(m2, Nil())) + +} + + diff --git a/src/test/resources/adt/constructors_2.vpr b/src/test/resources/adt/constructors_2.vpr new file mode 100644 index 000000000..0b968d488 --- /dev/null +++ b/src/test/resources/adt/constructors_2.vpr @@ -0,0 +1,26 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + +method constructors_2() +{ + var list1: List[Int] + //:: ExpectedOutput(typechecker.error) + list1 := Cons(Cons(1, Cons(1, Cons(1, Cons(1, Cons(1, Nil())))))) + + var list2: List[List[Bool]] + //:: ExpectedOutput(typechecker.error) + list2 := Cons(Cons(true, Cons(true, Cons(true, Cons(true, Cons(true, Cons(true, Nil(true))))))), Nil()) + + var list3: List[Seq[Int]] + //:: ExpectedOutput(typechecker.error) + list3 := Cons(1, Nil()) + + var list4: List[Set[Int]] + //:: ExpectedOutput(typechecker.error) + list4 := Cons(Set(true, false), Nil()) + +} + + diff --git a/src/test/resources/adt/constructors_3.vpr b/src/test/resources/adt/constructors_3.vpr new file mode 100644 index 000000000..205028180 --- /dev/null +++ b/src/test/resources/adt/constructors_3.vpr @@ -0,0 +1,23 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + +domain DList[T] { + function DNil(): DList[T] + function DCons(value: T, tail: DList[T]): DList[T] +} + +method constructors_3() +{ + var list1: List[Int] + //:: ExpectedOutput(typechecker.error) + list1 := Cons(1, DNil()) + + var list2: List[DList[Int]] + //:: ExpectedOutput(typechecker.error) + list2 := Cons(DCons(1, DNil()), Nil) + +} + + diff --git a/src/test/resources/adt/declarations_1.vpr b/src/test/resources/adt/declarations_1.vpr new file mode 100644 index 000000000..f008ddd46 --- /dev/null +++ b/src/test/resources/adt/declarations_1.vpr @@ -0,0 +1,35 @@ +adt SimpleList { + SimpleNil() + SimpleCons(value: Int, tail: SimpleList) +} + +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + +adt Tree[T] { + Leaf() + Node(value: T, left: Tree[T], right: Tree[T]) +} + +adt Tree3[T] { + Leaf3() + Node3(value: T, left: Tree3[T], middle: Tree3[T], right: Tree3[T]) +} + +adt SpecialList[T, S] { + SpecialNil() + TCons(elemT: T, tailT: SpecialList[T,S]) + SCons(elemS: S, tailS: SpecialList[T,S]) +} + +adt kTree[T] { + kLeaf() + kNode(value: T, children: Seq[kTree[T]]) +} + +adt Mixed[T,S] { + Entity1(sl: SimpleList, ls: List[S], lt: List[T]) + Entity2(t3: Tree3[T], spl1: SpecialList[T,S], spl2: SpecialList[S,T], kt: kTree[T]) +} \ No newline at end of file diff --git a/src/test/resources/adt/declarations_2.vpr b/src/test/resources/adt/declarations_2.vpr new file mode 100644 index 000000000..19502fbd2 --- /dev/null +++ b/src/test/resources/adt/declarations_2.vpr @@ -0,0 +1,15 @@ +adt SimpleList { + SimpleNil() + //:: ExpectedOutput(typechecker.error) + SimpleCons(value: Int, tail: SimpleList) + SimpleCons(value: Int, tail: SimpleList) +} + +adt List[T] { + Nil() + //:: ExpectedOutput(typechecker.error) + Cons(value: T, tail: List[T]) + Cons(value: T, tail: List[T]) +} + + diff --git a/src/test/resources/adt/declarations_3.vpr b/src/test/resources/adt/declarations_3.vpr new file mode 100644 index 000000000..e89e14030 --- /dev/null +++ b/src/test/resources/adt/declarations_3.vpr @@ -0,0 +1,6 @@ +adt SimpleList { + SimpleNil() + //:: ExpectedOutput(typechecker.error) + SimpleCons(value: Int, value: SimpleList) +} + diff --git a/src/test/resources/adt/declarations_4.vpr b/src/test/resources/adt/declarations_4.vpr new file mode 100644 index 000000000..9d704cb0c --- /dev/null +++ b/src/test/resources/adt/declarations_4.vpr @@ -0,0 +1,6 @@ +//:: ExpectedOutput(typechecker.error) +adt SpecialList[T, S] { + SpecialNil() + TCons(elemT: T, tail: SpecialList[T,S]) + SCons(elemS: S, tail: SpecialList[T,S]) +} \ No newline at end of file diff --git a/src/test/resources/adt/declarations_5.vpr b/src/test/resources/adt/declarations_5.vpr new file mode 100644 index 000000000..df0eb8eab --- /dev/null +++ b/src/test/resources/adt/declarations_5.vpr @@ -0,0 +1,9 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + +//:: ExpectedOutput(typechecker.error) +field value: Int + + diff --git a/src/test/resources/adt/destructors_1.vpr b/src/test/resources/adt/destructors_1.vpr new file mode 100644 index 000000000..7050bba27 --- /dev/null +++ b/src/test/resources/adt/destructors_1.vpr @@ -0,0 +1,79 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + + +adt Tree[T] { + Leaf() + Node(value: T, left: Tree[T], right: Tree[T]) +} + + +method destructors_1() +{ + + var tree: Tree[Int] + tree := Node(42, Node(420, Leaf(), Leaf()), Leaf()) + + var left: Tree[Int] + left := tree.left + assert left == tree.left + assert left == Node(420, Leaf(), Leaf()) + + var list: List[Bool] + list := Cons(true, Cons(true, Cons(true, Cons(true, Cons(true, Cons(true, Nil())))))) + + assert list.value + assert list.tail.value + assert !!list.tail.tail.tail.tail.tail.value + + var bigTree: Tree[Bool] + bigTree := Node( + true, + Node( + true, + Node( + true, + Node( + true, + Node( + true, + Node( + true, + Node(true, Leaf(), Leaf()), + Node(true,Leaf(),Leaf())), + Node(true, Leaf(), Leaf())), + Node(true, Leaf(), Leaf())), + Node(true, Leaf(), Leaf())), + Leaf() + ), + Node( + false, + Leaf(), + Node( + false, + Leaf(), + Node( + false, + Leaf(), + Node( + false, + Leaf(), + Node( + false, + Leaf(), + Node(false, Leaf(), Leaf()) + ) + ) + ) + ) + ) + ) + assert bigTree.left.left.left.left.value + assert bigTree.left.left.right.value + assert !bigTree.right.right.value + +} + + diff --git a/src/test/resources/adt/destructors_2.vpr b/src/test/resources/adt/destructors_2.vpr new file mode 100644 index 000000000..025a73d2a --- /dev/null +++ b/src/test/resources/adt/destructors_2.vpr @@ -0,0 +1,25 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + + +adt Tree[T] { + Leaf() + Node(value: T, left: Tree[T], right: Tree[T]) +} + + +method destructors_2() +{ + assert Cons(1, Nil()).value == 1 + + assert Cons(1, Nil()).tail == Nil() + + assert Node(42, Node(42, Leaf(), Node(42, Node(42, Leaf(), Leaf()), Leaf())), Leaf()).value == 42 + + assert Node(42, Node(42, Leaf(), Node(42, Node(42, Leaf(), Leaf()), Leaf())), Leaf()).left.right.left.value == 42 + + assert ((Node(42, Node(42, Leaf(), Node(42, Node(42, Leaf(), Leaf()), Leaf())), Leaf()).left).right.left).value == 42 + +} \ No newline at end of file diff --git a/src/test/resources/adt/destructors_3.vpr b/src/test/resources/adt/destructors_3.vpr new file mode 100644 index 000000000..b830e491d --- /dev/null +++ b/src/test/resources/adt/destructors_3.vpr @@ -0,0 +1,35 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + + +adt Tree[T] { + Leaf() + Node(value: T, left: Tree[T], right: Tree[T]) +} + +domain DList[T] { + function DNil(): DList[T] + function DCons(value: T, tail: DList[T]): DList[T] +} + + +field this_is_a_field: Bool + +method destructor_3() +{ + + //:: ExpectedOutput(typechecker.error) + assert Cons(1, Nil()).this_is_a_field + + //:: ExpectedOutput(typechecker.error) + assert Cons(1, Nil()).right.value == Nil() + + //:: ExpectedOutput(typechecker.error) + assert Cons(1, Nil()).right.value.left == Nil() + + //:: ExpectedOutput(typechecker.error) + assert DCons(1, DNil()).value == 1 + +} diff --git a/src/test/resources/adt/destructors_4.vpr b/src/test/resources/adt/destructors_4.vpr new file mode 100644 index 000000000..9cf440217 --- /dev/null +++ b/src/test/resources/adt/destructors_4.vpr @@ -0,0 +1,22 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + + +adt Tree[T] { + Leaf() + Node(value: T, left: Tree[T], right: Tree[T]) +} + + +method destructors_4() +{ + + //:: ExpectedOutput(typechecker.error) + assert Cons(1, Nil()).dummy == 1 + + //:: ExpectedOutput(typechecker.error) + assert Cons(1, Nil()).value.right.hello.f == 1 + +} diff --git a/src/test/resources/adt/destructors_5.vpr b/src/test/resources/adt/destructors_5.vpr new file mode 100644 index 000000000..7a6643896 --- /dev/null +++ b/src/test/resources/adt/destructors_5.vpr @@ -0,0 +1,31 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + + +adt Tree[T] { + Leaf() + Node(value: T, left: Tree[T], right: Tree[T]) +} + + +method destructors_5a() +{ + + //:: ExpectedOutput(assert.failed:assertion.false) + assert Nil().value == 1 +} + +method destructors_5b() +{ + //:: ExpectedOutput(assert.failed:assertion.false) + assert Cons(1, Nil()).value == 2 +} + +method destructors_5c() +{ + //:: ExpectedOutput(assert.failed:assertion.false) + assert Cons(1, Cons(1, Nil())).tail == Nil() +} + diff --git a/src/test/resources/adt/destructors_6.vpr b/src/test/resources/adt/destructors_6.vpr new file mode 100644 index 000000000..3c88f71ef --- /dev/null +++ b/src/test/resources/adt/destructors_6.vpr @@ -0,0 +1,22 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + + +adt Tree[T] { + Leaf() + Node(value: T, left: Tree[T], right: Tree[T]) +} + + +method destructors_6() +{ + + //:: ExpectedOutput(typechecker.error) + Nil().value := 1 + + var list: List[Int] + //:: ExpectedOutput(typechecker.error) + list.tail := Cons(1, Nil()) +} \ No newline at end of file diff --git a/src/test/resources/adt/discriminators_1.vpr b/src/test/resources/adt/discriminators_1.vpr new file mode 100644 index 000000000..afd07793a --- /dev/null +++ b/src/test/resources/adt/discriminators_1.vpr @@ -0,0 +1,35 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + + +adt Tree[T] { + Leaf() + Node(value: T, left: Tree[T], right: Tree[T]) +} + + +method discriminators_1a() +{ + var list: List[Int] + list := Cons(1, Nil()) + + assert list.isCons + assert list.tail.isNil + assert !list.tail.isCons + +} + +method discriminators_1b() +{ + var tree: Tree[Int] + tree := Node(42, Node(42, Leaf(), Leaf()), Node(42, Leaf(), Leaf())) + + assert !tree.isLeaf + assert tree.left.left.isLeaf + assert tree.left.right.isLeaf + assert tree.left.isNode + assert !tree.right.isLeaf + +} \ No newline at end of file diff --git a/src/test/resources/adt/discriminators_2.vpr b/src/test/resources/adt/discriminators_2.vpr new file mode 100644 index 000000000..78e01aa6d --- /dev/null +++ b/src/test/resources/adt/discriminators_2.vpr @@ -0,0 +1,28 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + + +adt Tree[T] { + Leaf() + Node(value: T, left: Tree[T], right: Tree[T]) +} + + +method discriminators_2() +{ + var list: List[Int] + list := Cons(1, Nil()) + + //:: ExpectedOutput(typechecker.error) + assert list.isLeaf + + //:: ExpectedOutput(typechecker.error) + assert list.isLeaf.isLeaf + + //:: ExpectedOutput(typechecker.error) + assert list.tail.tail.tail.isNode + + +} \ No newline at end of file diff --git a/src/test/resources/adt/discriminators_3.vpr b/src/test/resources/adt/discriminators_3.vpr new file mode 100644 index 000000000..78bdc3bf2 --- /dev/null +++ b/src/test/resources/adt/discriminators_3.vpr @@ -0,0 +1,16 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + +method discriminators_3() +{ + var list: List[Int] + list := Cons(1, Nil()) + + assert list.tail.isNil ? true : false + assert list.tail.isNil?true:false + + assert list.tail.isNil ? list.tail.isCons ? list.tail.isNil ? true : false : list.tail.isNil ? true : false : list.tail.isNil ? true : false + +} \ No newline at end of file diff --git a/src/test/resources/adt/discriminators_4.vpr b/src/test/resources/adt/discriminators_4.vpr new file mode 100644 index 000000000..9ac2f2eac --- /dev/null +++ b/src/test/resources/adt/discriminators_4.vpr @@ -0,0 +1,15 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + +field this_is_a_field:Int + +method discriminators_4() +{ + var list: List[Int] + + //:: ExpectedOutput(typechecker.error) + assert list.this_is_a_field + +} \ No newline at end of file diff --git a/src/test/resources/adt/discriminators_5.vpr b/src/test/resources/adt/discriminators_5.vpr new file mode 100644 index 000000000..27fd52e83 --- /dev/null +++ b/src/test/resources/adt/discriminators_5.vpr @@ -0,0 +1,8 @@ +adt List[T] { + //:: ExpectedOutput(typechecker.error) + Nil() + Cons(value: T, tail: List[T]) +} + + +field isNil:Int \ No newline at end of file diff --git a/src/test/resources/adt/discriminators_6.vpr b/src/test/resources/adt/discriminators_6.vpr new file mode 100644 index 000000000..229b87282 --- /dev/null +++ b/src/test/resources/adt/discriminators_6.vpr @@ -0,0 +1,10 @@ +adt List[T] { + //:: ExpectedOutput(typechecker.error) + Nil() + Cons(value: T, tail: List[T]) +} + +function isNil(x:Int): Bool +{ + true +} \ No newline at end of file diff --git a/src/test/resources/adt/discriminators_7.vpr b/src/test/resources/adt/discriminators_7.vpr new file mode 100644 index 000000000..3d56ff592 --- /dev/null +++ b/src/test/resources/adt/discriminators_7.vpr @@ -0,0 +1,30 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + + +adt Tree[T] { + Leaf() + Node(value: T, left: Tree[T], right: Tree[T]) +} + + +method discriminators_7() +{ + var list: List[Int] + list := Cons(1, Nil()) + + //:: ExpectedOutput(typechecker.error) + list.isCons := true + + //:: ExpectedOutput(typechecker.error) + list.isNil := true + + //:: ExpectedOutput(typechecker.error) + list.isLeaf := true + + //:: ExpectedOutput(typechecker.error) + list.tail.isLeaf := true + +} \ No newline at end of file diff --git a/src/test/resources/adt/encoding_1.vpr b/src/test/resources/adt/encoding_1.vpr new file mode 100644 index 000000000..2ef8ed412 --- /dev/null +++ b/src/test/resources/adt/encoding_1.vpr @@ -0,0 +1,32 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + +/** + * Note that above ADT is by default encoded as a domain with following signatures for destructors and discriminators. + * Propose of defining the domain below is to check name clash handling. + */ +domain DList[T] { + + function get_List_value(t: DList[T]): T + + function get_List_tail(t: DList[T]): DList[T] + + function List_tag(t: DList[T]): Int + } + +method encoding_1() +{ + assert Cons(1, Nil()).isNil == false + assert Cons(1, Nil()).isCons + assert Cons(1, Nil()).value == 1 + assert Cons(1, Nil()).tail == Nil() + + var dlist: DList[Int] + var n: Int + n := get_List_value(dlist) + dlist := get_List_tail(dlist) + n := List_tag(dlist) + +} diff --git a/src/test/resources/adt/encoding_2.vpr b/src/test/resources/adt/encoding_2.vpr new file mode 100644 index 000000000..213e5c91b --- /dev/null +++ b/src/test/resources/adt/encoding_2.vpr @@ -0,0 +1,18 @@ +adt ADT[T] { + C1() + C2(p21: T, p22: ADT[T]) + C3(p31: Int) + C4(p41: Bool, p42: ADT[T], p43:ADT[Int]) + C5() + C6() +} + +method encoding_2(a:ADT[Bool]) +{ + assert a.isC1 || a.isC2 || a.isC3 || a.isC4 || a.isC5 || a.isC6 + + assert a.isC1 <==> a == C1() + assert a.isC2 ==> a != C1() + assert a.isC2 <==> a == C2(a.p21, a.p22) + +} diff --git a/src/test/resources/adt/equality_1.vpr b/src/test/resources/adt/equality_1.vpr new file mode 100644 index 000000000..30b7410f3 --- /dev/null +++ b/src/test/resources/adt/equality_1.vpr @@ -0,0 +1,19 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + +method equality_1a() +{ + //:: ExpectedOutput(assert.failed:assertion.false) + assert Cons(1, Nil()) != Cons(1, Nil()) + +} + +method equality_1b() +{ + //:: ExpectedOutput(assert.failed:assertion.false) + assert Cons(1, Cons(1, Nil())).tail == Nil() +} + + diff --git a/src/test/resources/adt/equality_2.vpr b/src/test/resources/adt/equality_2.vpr new file mode 100644 index 000000000..59adb23ad --- /dev/null +++ b/src/test/resources/adt/equality_2.vpr @@ -0,0 +1,35 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + + +method equality_2a() +{ + assert Cons(1, Nil()) == Cons(1, Nil()) + + assert Cons(1, Cons(1, Nil())).tail == Cons(1, Nil()) +} + +method equality_2b() +{ + var list1: List[Int] + var list2: List[Int] + + //:: ExpectedOutput(assert.failed:assertion.false) + assert list1 == list2 + +} + +method equality_2c() +{ + var list1: List[Int] + list1 := Nil() + var list2: List[Int] + list2 := Nil() + + assert list1 == list2 + +} + + diff --git a/src/test/resources/adt/example_1.vpr b/src/test/resources/adt/example_1.vpr new file mode 100644 index 000000000..51bfd048b --- /dev/null +++ b/src/test/resources/adt/example_1.vpr @@ -0,0 +1,54 @@ +adt Tree { + Leaf() + Node(v: Int, left: Tree, right: Tree) +} + +function isBST(t:Tree): Bool +{ + t.isLeaf + ? true + : allNodesLessThan(t.left, t.v) && isBST(t.left) && allNodesGreaterThan(t.right, t.v) && isBST(t.right) + +} + +function allNodesLessThan(t:Tree, value: Int): Bool +{ + t.isLeaf + ? true + : t.v < value && allNodesLessThan(t.right, value) && allNodesLessThan(t.left, value) +} + +function allNodesGreaterThan(t:Tree, value: Int): Bool +{ + t.isLeaf + ? true + : t.v > value && allNodesGreaterThan(t.left, value) && allNodesGreaterThan(t.right, value) +} + + +method insertValue(v:Int, t:Tree) returns (res: Tree) + ensures forall i:Int :: allNodesGreaterThan(t,i) && i < v ==> allNodesGreaterThan(res, i) + ensures forall i:Int :: allNodesLessThan(t, i) && v < i ==> allNodesLessThan(res, i) + ensures isBST(t) ==> isBST(res) +{ + var new_rightsubtree: Tree + var new_leftsubtree: Tree + + if(t.isLeaf) { + res:= Node(v, Leaf(), Leaf()) + } else { + if (v == t.v) + { + // value is already in tree so we do nothing + res:= t + } + elseif (v < t.v) + { + new_leftsubtree := insertValue(v, t.left) + res := Node(t.v, new_leftsubtree, t.right) + } else { + new_rightsubtree := insertValue(v, t.right) + res := Node(t.v, t.left, new_rightsubtree) + } + } +} \ No newline at end of file diff --git a/src/test/resources/adt/example_2.vpr b/src/test/resources/adt/example_2.vpr new file mode 100644 index 000000000..cf961a6aa --- /dev/null +++ b/src/test/resources/adt/example_2.vpr @@ -0,0 +1,114 @@ +adt Tree { + Leaf() + Node(v: Int, left: Tree, right: Tree) +} + +/* + * Recursive function that computes the length of the longest path from node to a Leaf among all nodes in ts + * + * Remarks: + * - Basically Recursive Breadth-first search + * - For ts == Seq(t) and t:Tree this corresponds to the height + */ +function height_recursive(ts: Seq[Tree]): Int +{ + |ts| == 0 + ? 0 + : 1 + height_recursive(children_seq(ts)) +} + + +/* + * Function that wraps height_recursive for easy use + */ +function height(t: Tree): Int +{ + t.isLeaf + ? 0 + : height_recursive(Seq(t)) +} + + +/* + * Function that computes the direct children of one node + */ +function children(t: Tree): Seq[Tree] +{ + t.isLeaf || (t.isNode && t.left.isLeaf && t.right.isLeaf) + ? Seq() + : t.left.isNode && t.right.isNode + ? Seq(t.right) ++ Seq(t.left) + : t.left.isNode + ? Seq(t.left) + : Seq(t.right) +} + +/* + * Function that computes the direct children of a list of nodes recursivley applying + * the function children + */ +function children_seq(ts: Seq[Tree]): Seq[Tree] +{ + |ts| == 0 + ? Seq[Tree]() + : |ts| == 1 + ? children(ts[0]) + : children_seq(ts[1..]) ++ children(ts[0]) +} + + + +method computeTreeHeight(t: Tree) returns (res: Int) + ensures height(t) == res +{ + // logical variable for invariant of the second loop + var old_current: Seq[Tree] + + if (t.isLeaf){ + res := 0 + }else{ + var current: Seq[Tree] + var next: Seq[Tree] + current := Seq(t) + next := Seq[Tree]() + res := 0 + + while (|current| > 0) + invariant forall i: Int :: i >= 0 && i < |current| ==> current[i].isNode + invariant height(t) == res + height_recursive(current) + + { + res := res + 1 + next := Seq[Tree]() + + // save current to logical variable + assume old_current == current + + while (|current| > 0) + invariant forall i: Int :: i >= 0 && i < |current| ==> current[i].isNode + invariant forall i: Int :: i >= 0 && i < |next| ==> next[i].isNode + invariant children_seq(old_current) == children_seq(current) ++ next + { + var node : Tree := current[0] + POP(current) + if (node.left.isNode){ + PUSH(next, node.left) + } + if (node.right.isNode){ + PUSH(next, node.right) + } + + } + current := next + + } + } +} + +define PUSH(stck, v) { + stck := Seq(v) ++ stck +} + +define POP(stck) { + stck := stck[1..] +} diff --git a/src/test/resources/adt/example_3.vpr b/src/test/resources/adt/example_3.vpr new file mode 100644 index 000000000..60cac1954 --- /dev/null +++ b/src/test/resources/adt/example_3.vpr @@ -0,0 +1,59 @@ +adt List { + Nil() + Cons(head: Int, tail: List) +} + +method prepend(xs: List, v: Int) + returns (ys:List) + ensures ys.head == v + ensures ys.tail == xs +{ + ys := Cons(v, xs) +} + +function len(xs: List): Int + ensures result >= 0 +{ + xs.isNil ? 0 : 1 + len(xs.tail) +} + + +define NO_VALUE (-1) + +function at(xs: List, pos: Int): Int +{ + (xs.isNil || pos < 0) + ? NO_VALUE + : pos == 0 + ? xs.head + : at(xs.tail, pos-1) +} + +method linear_search(xs: List, key: Int) + returns (pos:Int) + requires key >= 0 + ensures 0 <= pos && pos <= len(xs) + ensures at(xs, pos) == key || pos == len(xs) + ensures pos == len(xs) ==> forall k:Int :: 0 <= k && k < len(xs) ==> at(xs, k) != key +{ + pos := 0 + var ys : List + ys := xs + + while (!ys.isNil && ys.head != key) + invariant 0 <= pos + invariant pos + len(ys) == len(xs) + invariant ys.isNil ==> pos == len(xs) + invariant forall k:Int :: 0 <= k ==> at(xs, pos+k) == at(ys, k) + invariant forall k:Int :: 0 <= k && k < pos ==> at(xs, k) != key + { + var old_ys: List + old_ys := ys + ys := ys.tail + assert forall k:Int :: 0 <= k ==> at(old_ys,k+1) == at(ys,k) + assert at(old_ys, 0) == at(xs, pos) // need to trigger this fact + pos := pos + 1 + } + + assert !ys.isNil ==> at(ys, 0) == key +} diff --git a/src/test/resources/adt/example_4.vpr b/src/test/resources/adt/example_4.vpr new file mode 100644 index 000000000..3784c8f98 --- /dev/null +++ b/src/test/resources/adt/example_4.vpr @@ -0,0 +1,77 @@ +adt Option[T] { + Some(value:T) + None() +} + +domain AddDomain[T] { + function add(a:T, b: T): T + + axiom { + forall o1:Perm, o2:Perm :: {add(o1,o2)} add(o1,o2) == (o1 + o2) + } + axiom { + forall o1:Int, o2:Int :: {add(o1,o2)} add(o1,o2) == (o1 + o2) + } + axiom { + forall o1:Seq[T], o2:Seq[T] :: {add(o1,o2)} add(o1,o2) == (o1 ++ o2) + } + axiom { + forall o1:Set[T], o2:Set[T] :: {add(o1,o2)} add(o1,o2) == (o1 union o2) + } + axiom { + forall o1:Option[T], o2:Option[T] :: {add(o1,o2)} add(o1,o2) == ((o1.isSome && o2.isSome) ? Some(add(o1.value, o2.value)) : None()) + } +} + +method request(arg: Int) returns (res: Option[Int]) +ensures arg > 0 ==> res.isSome && res == Some(2*arg) +ensures arg < 0 ==> res.isNone +{ + if (arg > 0) + { + res:= add(Some(arg), Some(arg)) + } + else + { + res:= None() + } +} + +method client() { + + var response: Option[Int] + response := request(1) + if (response.isSome) + { + // resquest successfull + assert response.value == 2 + + var o: Option[Int] + o := Some(3) + + assert add(response, None()) == None() + assert add(o, response).value == 5 + + assert add(Some(Seq(1,2,3)), Some(Seq(1,2,3))).value == Seq(1,2,3,1,2,3) + } + else + { + assert false + } + + + + response := request(-1) + assert response.isNone + if (response.isSome) + { + // resquest successfull + assert false + + } + else + { + assert true + } + +} \ No newline at end of file diff --git a/src/test/resources/adt/example_5.vpr b/src/test/resources/adt/example_5.vpr new file mode 100644 index 000000000..38a9b0f6a --- /dev/null +++ b/src/test/resources/adt/example_5.vpr @@ -0,0 +1,71 @@ +domain SizeDomain[T] { + function size(collection:T): Int +} + +domain AddDomain[T] { + function add(a:T, b: T): T + +} + +domain ToSeqDomain[A,B] { + function toSeq(collection: A): Seq[B] +} + +domain IntUtility { + axiom { + forall o1:Int, o2:Int :: {add(o1,o2)} add(o1,o2) == (o1 + o2) + } +} + +domain SetUtility[T] { + + axiom { + forall set: Set[T] :: { size(set) } size(set) == |set| + } + axiom { + forall o1:Set[T], o2:Set[T] :: {add(o1,o2)} add(o1,o2) == (o1 union o2) + } +} + +domain SeqUtility[T] { + axiom { + forall o1:Seq[T], o2:Seq[T] :: {add(o1,o2)} add(o1,o2) == (o1 ++ o2) + } + axiom { + forall seq: Seq[T] :: { size(seq) } size(seq) == |seq| + } +} + + +adt DAG[T] { + Node(value: T, successor: Seq[DAG[T]]) +} + +domain DAGUtility[T] { + + axiom { + forall dags:Seq[DAG[T]] :: {toSeq(dags)} toSeq(dags) == (|dags| > 0 ? toSeq(dags[0]) ++ toSeq(dags[1..]) : Seq()) + + } + axiom { + forall dag:DAG[T] :: {toSeq(dag)} toSeq(dag) == (|dag.successor| > 0 ? Seq(dag.value) ++ toSeq(dag.successor) : Seq(dag.value)) + } +} + + +method client() +{ + var dag: DAG[Int] + + dag := Node(1, Seq( + Node(2, Seq(Node(3, Seq()))), + Node(2, Seq(Node(3, Seq()))), + Node(2, Seq()), + Node(2, Seq()), + Node(2, Seq()) + )) + + assert toSeq(dag) == Seq(1) ++ toSeq(dag.successor) + + assert toSeq(dag) == Seq(1, 2, 3, 2, 3, 2, 2, 2) +} \ No newline at end of file diff --git a/src/test/resources/adt/soundness_1.vpr b/src/test/resources/adt/soundness_1.vpr new file mode 100644 index 000000000..a1bdfcef1 --- /dev/null +++ b/src/test/resources/adt/soundness_1.vpr @@ -0,0 +1,41 @@ +adt SimpleList { + SimpleNil() + SimpleCons(value: Int, tail: SimpleList) +} + +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + +adt Tree[T] { + Leaf() + Node(value: T, left: Tree[T], right: Tree[T]) +} + +adt Tree3[T] { + Leaf3() + Node3(value: T, left: Tree3[T], middle: Tree3[T], right: Tree3[T]) +} + +adt SpecialList[T, S] { + SpecialNil() + TCons(elemT: T, tailT: SpecialList[T,S]) + SCons(elemS: S, tailS: SpecialList[T,S]) +} + +adt kTree[T] { + kLeaf() + kNode(value: T, children: Seq[kTree[T]]) +} + +adt Mixed[T,S] { + Entity1(sl: SimpleList, ls: List[S], lt: List[T]) + Entity2(t3: Tree3[T], spl1: SpecialList[T,S], spl2: SpecialList[S,T], kt: kTree[T]) +} + +method soundness_1() +{ + //:: ExpectedOutput(assert.failed:assertion.false) + assert false +} \ No newline at end of file diff --git a/src/test/resources/adt/type_ascriptions_1.vpr b/src/test/resources/adt/type_ascriptions_1.vpr new file mode 100644 index 000000000..f432d7205 --- /dev/null +++ b/src/test/resources/adt/type_ascriptions_1.vpr @@ -0,0 +1,15 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + + +method type_ascriptions_1() +{ + assert (Nil(): List[Bool]) == (Nil(): List[Bool]) + + assert (Nil(): List[List[Int]]) == (Nil(): List[List[Int]]) + + // This should trigger a warning but currently there is no way of testing this + assert Nil() == Nil() +} diff --git a/src/test/resources/adt/variable_declarations_1.vpr b/src/test/resources/adt/variable_declarations_1.vpr new file mode 100644 index 000000000..7324e472f --- /dev/null +++ b/src/test/resources/adt/variable_declarations_1.vpr @@ -0,0 +1,34 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + +method var_decls_1a() +{ + var list1: List[Int] + var list2: List[List[Bool]] + var list3: List[List[List[Int]]] + var list4: List[List[List[List[Bool]]]] + + var list5: List[Seq[Int]] + var list6: List[Set[Bool]] + var list7: List[Map[Int, Int]] + var list8: List[Map[Int, List[Int]]] +} + +adt SpecialList[T, S] { + SpecialNil() + TCons(elemT: T, tailT: SpecialList[T,S]) + SCons(elemS: S, tailS: SpecialList[T,S]) +} + +method var_decls_1b() +{ + var slist1: SpecialList[Bool, List[Int]] + var slist2: SpecialList[Int, Seq[Int]] + var slist3: SpecialList[List[List[List[List[Bool]]]], List[List[List[List[Bool]]]]] + var slist4: SpecialList[SpecialList[SpecialList[SpecialList[Int, Int], SpecialList[Bool, Bool]], Int], SpecialList[Bool, SpecialList[SpecialList[Int, Int], SpecialList[Bool, Bool]]]] + +} + + diff --git a/src/test/resources/adt/variable_declarations_2.vpr b/src/test/resources/adt/variable_declarations_2.vpr new file mode 100644 index 000000000..dfc678c17 --- /dev/null +++ b/src/test/resources/adt/variable_declarations_2.vpr @@ -0,0 +1,27 @@ +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} + +method var_decls_2a() +{ + //:: ExpectedOutput(typechecker.error) + var list1: List[Int, Int] + + //:: ExpectedOutput(typechecker.error) + var list2: List + +} + +adt SpecialList[T, S] { + SpecialNil() + TCons(elemT: T, tailT: SpecialList[T,S]) + SCons(elemS: S, tailS: SpecialList[T,S]) +} + +method var_decls_2b() +{ + //:: ExpectedOutput(typechecker.error) + var slist: SpecialList[SpecialList[SpecialList[SpecialList[Int, Int], SpecialList[Bool]], Int], SpecialList[Bool, SpecialList[SpecialList[Int, Int], SpecialList[Bool, Bool]]]] + +} \ No newline at end of file From cacd64be1975a7fff7c07586147b932b06f935ac Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Thu, 31 Mar 2022 10:42:54 +0200 Subject: [PATCH 43/50] Add contains function for ADTs --- src/main/resources/import/adt/contains.vpr | 9 + .../standard/adt/encoding/AdtEncoder.scala | 161 +++++++++++++++++- .../adt/encoding/AdtNameManager.scala | 8 + 3 files changed, 175 insertions(+), 3 deletions(-) create mode 100644 src/main/resources/import/adt/contains.vpr diff --git a/src/main/resources/import/adt/contains.vpr b/src/main/resources/import/adt/contains.vpr new file mode 100644 index 000000000..ed96442de --- /dev/null +++ b/src/main/resources/import/adt/contains.vpr @@ -0,0 +1,9 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// 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-2022 ETH Zurich. + +domain ContainsDomain[A,B] { + function contains(a: A, b: B): Bool +} \ No newline at end of file diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala index 6e94bd487..23070859b 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala @@ -10,6 +10,8 @@ import viper.silver.ast._ import viper.silver.ast.utility.rewriter.{StrategyBuilder, Traverse} import viper.silver.plugin.standard.adt._ +import scala.annotation.tailrec + /** * This class implement the encoder used to encode ADT AST nodes to ordinary AST nodes. @@ -33,7 +35,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager { def encode(): Program = { // In a first step encode all adt top level declarations and constructor calls - val newProgram: Program = StrategyBuilder.Slim[Node]({ + var newProgram: Program = StrategyBuilder.Slim[Node]({ case p@Program(domains, fields, functions, predicates, methods, extensions) => val remainingExtensions = extensions filter { case _:Adt => false; case _ => true } val encodedAdtsAsDomains: Seq[Domain] = extensions collect { case a:Adt => encodeAdtAsDomain(a) } @@ -44,7 +46,15 @@ class AdtEncoder(val program: Program) extends AdtNameManager { }, Traverse.BottomUp).execute(program) // In a second step encode all occurrences of AdtType's as DomainType's - encodeAllAdtTypeAsDomainType(newProgram) + newProgram = encodeAllAdtTypeAsDomainType(newProgram) + + // In a third step generate transitivity axioms if contains domain is present + if (withContainsDomain) { + val domains = newProgram.domains ++ Seq(generateContainsTransitivityDomain(newProgram)) + newProgram = newProgram.copy(domains = domains)(newProgram.pos, newProgram.info, newProgram.errT) + } + + newProgram } /** @@ -74,7 +84,8 @@ class AdtEncoder(val program: Program) extends AdtNameManager { val functions: Seq[DomainFunc] = (constructors map encodeAdtConstructorAsDomainFunc(domain)) ++ (constructors flatMap generateDestructorDeclarations(domain)) ++ Seq(generateTagDeclaration(domain)) val axioms = (constructors flatMap generateInjectivityAxiom(domain)) ++ - (constructors map generateTagAxiom(domain)) ++ Seq(generateExclusivityAxiom(domain)(constructors)) + (constructors map generateTagAxiom(domain)) ++ Seq(generateExclusivityAxiom(domain)(constructors)) ++ + (if (withContainsDomain) constructors filter (_.formalArgs.nonEmpty) map generateContainsAxiom(domain) else Seq.empty) domain.copy(functions = functions, axioms = axioms)(adt.pos, adt.info, adt.errT) } } @@ -359,6 +370,150 @@ class AdtEncoder(val program: Program) extends AdtNameManager { } + /** + * This is a helper method to check if the contains domain, namely + * + * domain ContainsDomain[A,B] { + * function contains(a: A, b: B): Bool + * } + * + * was imported by import . + * + * @return Return true if the contains domain is present + */ + private def withContainsDomain: Boolean = program.domains.exists(_.name == getContainsDomainName) + + /** + * This method generates the corresponding contains axiom for a ADT constructor + * + * axiom { + * forall p_1: T1, ..., p_n: Tn :: {C(p_1, ..., p_n)} contains(p_1, C′) && ... && contains(p_n, C′) + * } + * + * where C′ = C(p_1, ..., p_n). + * + * @param domain The domain that encodes the ADT the constructor belongs to for which we want a contains axiom + * @param ac An ADT constructor + * @return The generated contains axiom + */ + private def generateContainsAxiom(domain: Domain)(ac: AdtConstructor): AnonymousDomainAxiom = { + assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.") + assert(ac.formalArgs.nonEmpty, "AdtEncoder: An error in the ADT encoding occurred.") + + val localVarDecl = ac.formalArgs.collect {case l:LocalVarDecl => l } + val localVars = ac.formalArgs.map { + case LocalVarDecl(name, typ) => + typ match { + case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(name))(ac.pos, ac.info, ac.errT) + case d => localVarTFromType(d, Some(name))(ac.pos, ac.info, ac.errT) + } + } + assert(localVarDecl.size == localVars.size, "AdtEncoder: An error in the ADT encoding occurred.") + + val constructorApp = DomainFuncApp( + ac.name, + localVars, + defaultTypeVarsFromDomain(domain) + )(ac.pos, ac.info, encodeAdtTypeAsDomainType(ac.typ), ac.adtName, ac.errT) + + val trigger = Trigger(Seq(constructorApp))(ac.pos, ac.info, ac.errT) + + val containsApp = (lv: LocalVar) => DomainFuncApp( + getContainsFunctionName, + Seq(lv, constructorApp), + Map(TypeVar("A") -> lv.typ, TypeVar("B") -> constructorApp.typ) + )(ac.pos, ac.info, Bool, getContainsDomainName, ac.errT) + + val axiomBody = localVars.map(containsApp).foldLeft[Exp](TrueLit()(ac.pos, ac.info, ac.errT))((a, b) => And(a, b)(ac.pos, ac.info, ac.errT)) + val forall = Forall(localVarDecl, Seq(trigger), axiomBody)(ac.pos, ac.info, ac.errT) + + AnonymousDomainAxiom(forall)(ac.pos, ac.info, ac.adtName, ac.errT) + } + + /** + * This method encodes the transitivity of the contains function. Namely it collects arguments types of + * all contains applications as tuples, computes its transitive closure and finally the corresponding axioms. + * + * This ensures that we generate one axiom which encodes the transitivity of contains for each possible + * triple of concrete types, which are used in calls to contains. + * + * + * @param program The program + * @return The ContainsTransitivityDomain with axioms that encode transitivity + */ + private def generateContainsTransitivityDomain(program: Program): Domain = { + + def addTransitive(s: Set[(Type, Type)]): Set[(Type, Type)] = + s ++ (for ((x1, y1) <- s; (x2, y2) <- s if y1 == x2) yield (x1, y2)) + + @tailrec + def transitiveClosure(s: Set[(Type, Type)]): Set[(Type, Type)] = { + val t = addTransitive(s) + if (t.size == s.size) s else transitiveClosure(t) + } + + def genAxiom(a: Type, b: Type, c: Type): AnonymousDomainAxiom = { + val aVar = LocalVarDecl("a", a)() + val bVar = LocalVarDecl("b", b)() + val cVar = LocalVarDecl("c", c)() + + def containsApp(l: Exp, r: Exp) = DomainFuncApp( + getContainsFunctionName, + Seq(l, r), + Map( + TypeVar("A") -> l.typ, + TypeVar("B") -> r.typ + ) + )(NoPosition, NoInfo, Bool, getContainsDomainName, NoTrafos) + + AnonymousDomainAxiom( + Forall( + Seq(aVar, bVar, cVar), + Seq( + Trigger( + Seq( + containsApp(aVar.localVar, bVar.localVar), + containsApp(bVar.localVar, cVar.localVar) + ) + )() + ), + Implies( + And( + containsApp(aVar.localVar, bVar.localVar), + containsApp(bVar.localVar, cVar.localVar) + )(), + containsApp(aVar.localVar, cVar.localVar) + )() + )() + )(domainName = getContainsTransitivityDomain) + } + + var tuples: Set[(Type, Type)] = Set.empty + program.visit({ + case dfa@DomainFuncApp(funcname, args, _) if funcname == getContainsFunctionName && dfa.domainName == getContainsDomainName => + assert(args.size == 2, "AdtEncoder: An error in the ADT encoding occurred.") + if (args.head.typ.isConcrete && args(1).typ.isConcrete) { + tuples += ((args.head.typ, args(1).typ)) + } + }) + + var triples: Set[(Type, Type, Type)] = Set.empty + val closure = transitiveClosure(tuples) + for ((a,b) <- closure) { + for ((c,d) <- closure) { + if (b == c) + triples += ((a,b,d)) + } + } + val axioms = triples.toSeq.map(a => genAxiom(a._1, a._2, a._3)) + + Domain( + getContainsTransitivityDomain, + Seq(), + axioms + )() + } + /** * This method traverses the entire AST and encodes any occurrences of an AdtType as a DomainType. Additionaly * it handles DomainFuncApp and FuncApp specially since the argument 'typ' could also be an AdtType. diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala index 2a8140cd6..7a9b84eb0 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala @@ -34,6 +34,14 @@ trait AdtNameManager { */ private val adtNameMappings: mutable.Map[String, String] = mutable.Map() + /** + * Following helper methods return predefined names/identifiers for the contains relation for ADTs. + * Note that the first two names are fixed by resources/adt/contains.vpr + */ + def getContainsDomainName: String = "ContainsDomain" + def getContainsFunctionName: String = "contains" + def getContainsTransitivityDomain: String = getName("ContainsTransitivityDomain") + /** * This method returns the name of the destructor given the name of the ADT and the name of a constructor argument * From 558cbb09793169f3e83465f566208c3270a47167 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Mon, 11 Apr 2022 18:05:11 +0200 Subject: [PATCH 44/50] Implement Syntax for Deriving System --- src/main/resources/import/adt/derives.vpr | 1 + .../plugin/standard/adt/AdtASTExtension.scala | 22 ++++++-- .../standard/adt/AdtPASTExtension.scala | 54 ++++++++++++++----- .../plugin/standard/adt/AdtPlugin.scala | 50 +++++++++++++---- .../standard/adt/encoding/AdtEncoder.scala | 47 ++++++++-------- 5 files changed, 123 insertions(+), 51 deletions(-) create mode 100644 src/main/resources/import/adt/derives.vpr diff --git a/src/main/resources/import/adt/derives.vpr b/src/main/resources/import/adt/derives.vpr new file mode 100644 index 000000000..7dad73f6d --- /dev/null +++ b/src/main/resources/import/adt/derives.vpr @@ -0,0 +1 @@ +import \ No newline at end of file diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala index f478b5f6d..80a80d812 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala @@ -7,7 +7,7 @@ package viper.silver.plugin.standard.adt import viper.silver.ast._ -import viper.silver.ast.pretty.FastPrettyPrinter.{ContOps, braces, brackets, char, defaultIndent, line, nest, nil, parens, show, showVars, space, ssep, text} +import viper.silver.ast.pretty.FastPrettyPrinter.{ContOps, braces, brackets, char, defaultIndent, line, nest, nil, parens, show, showType, showVars, space, ssep, text} import viper.silver.ast.pretty.PrettyPrintPrimitives import viper.silver.ast.utility.Consistency import viper.silver.verifier.{ConsistencyError, Failure, VerificationResult} @@ -18,20 +18,34 @@ import viper.silver.verifier.{ConsistencyError, Failure, VerificationResult} * @param name name of the ADT * @param constructors sequence of corresponding constructors * @param typVars sequence of type variables (generics) + * @param derivingInfo a map that maps identifiers of derivable functions to a tuple containing an optional type param and a set of excluded constructor argument identifiers */ -case class Adt(name: String, constructors: Seq[AdtConstructor], typVars: Seq[TypeVar] = Nil) +case class Adt(name: String, constructors: Seq[AdtConstructor], typVars: Seq[TypeVar] = Nil, derivingInfo: Map[String, (Option[Type], Set[String])] = Map.empty) (val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionMember { val scopedDecls: Seq[Declaration] = Seq() - override def extensionSubnodes: Seq[Node] = constructors ++ typVars + override def extensionSubnodes: Seq[Node] = constructors ++ typVars ++ derivingInfo.map(_._2._1).collect { case Some(v) => v } override def prettyPrint: PrettyPrintPrimitives#Cont = { + + def showDerivingInfo(di: (String, (Option[Type], Set[String]))): PrettyPrintPrimitives#Cont = { + val (func, (param, blocklist)) = di + text(func) <> (if (param.isEmpty) nil else text("[") <> showType(param.get) <> space <> "]") <> + space <> (if (blocklist.isEmpty) nil else text("without") <> space <> ssep(blocklist.toSeq map text, char (',') <> space)) + } + text("adt") <+> name <> (if (typVars.isEmpty) nil else text("[") <> ssep(typVars map show, char (',') <> space) <> "]") <+> braces(nest(defaultIndent, line <> line <> ssep(constructors map show, line <> line) - ) <> line) + ) <> line) <+> + (if (derivingInfo.isEmpty) nil else text("derives") <+> + braces(nest(defaultIndent, + line <> line <> + ssep(derivingInfo.toSeq map showDerivingInfo, line <> line) + ) <> line) + ) } } diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 65ea1b7dd..68e1d1220 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -14,28 +14,48 @@ import viper.silver.plugin.standard.adt.PAdtConstructor.findAdtConstructor import scala.util.{Success, Try} -case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[PAdtConstructor])(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { +case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[PAdtConstructor], derivingInfos: Seq[PAdtDerivingInfo])(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { - override val getSubnodes: Seq[PNode] = Seq(idndef) ++ typVars ++ constructors + override val getSubnodes: Seq[PNode] = Seq(idndef) ++ typVars ++ constructors ++ derivingInfos override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { t.checkMember(this) { constructors foreach (_.typecheck(t, n)) } // Check that formalArg identifiers among all constructors are unique - val allFormalArgsIdentifier = constructors flatMap (_.formalArgs map { - case fad:PFormalArgDecl => fad.idndef.name - case _ => sys.error("AdtEncoder : Only PFormalArgDecl are allowed as arguments of an Adt constructor") - }) - if (allFormalArgsIdentifier.distinct != allFormalArgsIdentifier) { - Some(Seq("duplicate argument identifier in adt constructors")) - } else { - None + val allFormalArgs = constructors flatMap (_.formalArgs collect { case fad:PFormalArgDecl => fad }) + val duplicateArgs = allFormalArgs.groupBy(_.idndef.name).collect { case (_,ys) if ys.size > 1 => ys.head }.toSeq + t.messages ++= duplicateArgs.flatMap { arg => + FastMessaging.message(arg.idndef, "Duplicate argument identifier `" + arg.idndef.name + "' among adt constructors at " + arg.idndef.pos._1) + } + + // Check validity blocklisted identifiers + derivingInfos.foreach { di => + val diff = di.blockList.filterNot(allFormalArgs.map(fad => PIdnUse(fad.idndef.name)(fad.idndef.pos)).toSet) + if (diff.nonEmpty) { + t.messages ++= FastMessaging.message(diff.head, "Invalid identifier `" + diff.head.name + "' at " + diff.head.pos._1) + } + + } + // Check duplicate deriving infos + val duplicateDerivingInfo = derivingInfos.groupBy(_.idnuse).collect { case (_,ys) if ys.size > 1 => ys.head }.toSeq + t.messages ++= duplicateDerivingInfo.flatMap { di => + FastMessaging.message(di.idnuse, "Duplicate derivation of function `" + di.idnuse.name + "' at " + di.idnuse.pos._1) } + + derivingInfos.foreach(_.typecheck(t,n)) + + None } override def translateMemberSignature(t: Translator): Adt = { - Adt(idndef.name, null, typVars map (t => TypeVar(t.idndef.name)))(t.liftPos(this)) + + Adt( + idndef.name, + null, + typVars map (t => TypeVar(t.idndef.name)), + derivingInfos.map( a => (a.idnuse.name, (if (a.param.nonEmpty) Some(t.ttyp(a.param.get)) else None, a.blockList.map(_.name)))).toMap + )(t.liftPos(this)) } override def translateMember(t: Translator): Member = { @@ -133,6 +153,16 @@ object PAdtConstructor { case class PAdtConstructor1(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])(val pos: (Position, Position)) +case class PAdtDerivingInfo(idnuse: PIdnUse, param: Option[PType], blockList: Set[PIdnUse])(val pos: (Position, Position)) extends PExtender { + + override def getSubnodes():Seq[PNode] = Seq(idnuse) ++ param.toSeq + + override def typecheck(t: TypeChecker, n: NameAnalyser):Option[Seq[String]] = { + param.foreach(t.check) + None + } +} + case class PAdtType(adt: PIdnUse, args: Seq[PType])(val pos: (Position, Position)) extends PExtender with PGenericType { var kind: PAdtTypeKinds.Kind = PAdtTypeKinds.Unresolved @@ -181,7 +211,7 @@ case class PAdtType(adt: PIdnUse, args: Seq[PType])(val pos: (Position, Position } x match { - case PAdt(_, typVars, _) => + case PAdt(_, typVars, _, _) => t.ensure(args.length == typVars.length, this, "wrong number of type arguments") at.kind = PAdtTypeKinds.Adt None diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index cde1327ae..2a3ad77ae 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -9,7 +9,7 @@ package viper.silver.plugin.standard.adt import fastparse._ import viper.silver.ast.Program import viper.silver.ast.utility.rewriter.StrategyBuilder -import viper.silver.parser.FastParser.{FP, anyFormalArgList, idndef, whitespace} +import viper.silver.parser.FastParser.{FP, anyFormalArgList, idndef, idnuse, typ, whitespace} import viper.silver.parser._ import viper.silver.plugin.standard.adt.encoding.AdtEncoder import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} @@ -18,9 +18,20 @@ import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} class AdtPlugin extends SilverPlugin with ParserPluginTemplate { /** - * Keyword used to define ADT's + * This field is set during the beforeParse method + */ + private var derivesImported: Boolean = false + private def setDerivesImported(input: String): Unit = "import[\\s]+".r.findFirstIn(input) match { + case Some(_) => derivesImported = true + case None => + } + + /** + * Keywords used to define ADT's */ private val AdtKeyword: String = "adt" + private val AdtDerivesKeyword: String = "derives" + private val AdtDerivesWithoutKeyword: String = "without" /** * Parser for ADT declaration. @@ -34,16 +45,27 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { * */ def adtDecl[_: P]: P[PAdt] = FP(AdtKeyword ~/ idndef ~ ("[" ~ adtTypeVarDecl.rep(sep = ",") ~ "]").? ~ "{" ~ adtConstructorDecl.rep ~ - "}").map { - case (pos, (name, typparams, constructors)) => + "}" ~ adtDerivingDecl.?).map { + case (pos, (name, typparams, constructors, dec)) => PAdt( name, typparams.getOrElse(Nil), - constructors map (c => PAdtConstructor(c.idndef, c.formalArgs)(PIdnUse(name.name)(name.pos))(c.pos)))(pos) + constructors map (c => PAdtConstructor(c.idndef, c.formalArgs)(PIdnUse(name.name)(name.pos))(c.pos)), + dec.getOrElse(Seq.empty) + )(pos) } def adtTypeVarDecl[_: P]: P[PTypeVarDecl] = FP(idndef).map{ case (pos, i) => PTypeVarDecl(i)(pos) } + def adtDerivingDecl[_: P]: P[Seq[PAdtDerivingInfo]] = P(AdtDerivesKeyword ~/ "{" ~ adtDerivingDeclBody.rep ~ "}") + + def adtDerivingDeclBody[_:P]: P[PAdtDerivingInfo] = FP( + idnuse ~ ("[" ~ typ ~ "]").? ~ (AdtDerivesWithoutKeyword ~/ idnuse.rep(sep = ",")).?).map { + case (pos, (func, ttyp, bl)) => PAdtDerivingInfo(func, ttyp, bl.getOrElse(Seq.empty).toSet)(pos) + } + + def adtDerivingFunc[_:P]: P[PIdnUse] = FP(StringIn("contains").!).map { case (pos, id) => PIdnUse(id)(pos) } + def adtConstructorDecl[_: P]: P[PAdtConstructor1] = FP(adtConstructorSignature ~ ";".?).map { case (pos, cdecl) => cdecl match { case (name, formalArgs) => PAdtConstructor1(name, formalArgs)(pos) @@ -53,10 +75,13 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { def adtConstructorSignature[_: P]: P[(PIdnDef, Seq[PAnyFormalArgDecl])] = P(idndef ~ "(" ~ anyFormalArgList ~ ")") override def beforeParse(input: String, isImported: Boolean): String = { - // Add new parser adt declaration keyword - ParserExtension.addNewKeywords(Set[String](AdtKeyword)) - // Add new parser for adt declaration - ParserExtension.addNewDeclAtEnd(adtDecl(_)) + if (!isImported) { + // Add new parser adt declaration keyword + ParserExtension.addNewKeywords(Set[String](AdtKeyword)) + // Add new parser for adt declaration + ParserExtension.addNewDeclAtEnd(adtDecl(_)) + } + setDerivesImported(input) input } @@ -68,6 +93,8 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { val declaredConstructorArgsNames = input.extensions.collect { case a: PAdt => a.constructors flatMap ( c => c.formalArgs collect {case PFormalArgDecl(idndef, _) => idndef})}.flatten.toSet def transformStrategy[T <: PNode](input: T): T = StrategyBuilder.Slim[PNode]({ + // If derives import is missing deriving info is ignored + case pa@PAdt(idndef, typVars, constructors, _) if !derivesImported => PAdt(idndef, typVars, constructors, Seq.empty)(pa.pos) case pa@PDomainType(idnuse, args) if declaredAdtNames.exists(_.name == idnuse.name) => PAdtType(idnuse, args)(pa.pos) case pc@PCall(idnuse, args, typeAnnotated) if declaredConstructorNames.exists(_.name == idnuse.name) => PConstructorCall(idnuse, args, typeAnnotated)(pc.pos) // A destructor call or discriminator call might be parsed as left-hand side of a field assignment, which is illegal. Hence in this case @@ -88,7 +115,10 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { } override def beforeVerify(input: Program): Program = { - new AdtEncoder(input).encode() + println(input) + val newProgram = new AdtEncoder(input).encode() + //println(newProgram) + newProgram } } diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala index 23070859b..9fa135338 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala @@ -48,8 +48,8 @@ class AdtEncoder(val program: Program) extends AdtNameManager { // In a second step encode all occurrences of AdtType's as DomainType's newProgram = encodeAllAdtTypeAsDomainType(newProgram) - // In a third step generate transitivity axioms if contains domain is present - if (withContainsDomain) { + // In a third step generate transitivity axioms if contains function is derived for at least one adt + if (containsFunctionIsDerived) { val domains = newProgram.domains ++ Seq(generateContainsTransitivityDomain(newProgram)) newProgram = newProgram.copy(domains = domains)(newProgram.pos, newProgram.info, newProgram.errT) } @@ -73,20 +73,22 @@ class AdtEncoder(val program: Program) extends AdtNameManager { * 3. Adds destructor declarations encoded as domain functions * 4. Adds a tag functions encoded as domain functions * 5. Generates corresponding axioms for injectivity, exclusivity and the tag function + * 6. Generates axioms for derived functions * * @param adt The ADT to encode * @return An the encoded ADT as a domain */ private def encodeAdtAsDomain(adt: Adt): Domain = { adt match { - case Adt(name, constructors, typVars) => + case Adt(name, constructors, typVars, derivingInfo) => val domain = Domain(name, null, null, typVars)(adt.pos, adt.info, adt.errT) val functions: Seq[DomainFunc] = (constructors map encodeAdtConstructorAsDomainFunc(domain)) ++ (constructors flatMap generateDestructorDeclarations(domain)) ++ Seq(generateTagDeclaration(domain)) val axioms = (constructors flatMap generateInjectivityAxiom(domain)) ++ - (constructors map generateTagAxiom(domain)) ++ Seq(generateExclusivityAxiom(domain)(constructors)) ++ - (if (withContainsDomain) constructors filter (_.formalArgs.nonEmpty) map generateContainsAxiom(domain) else Seq.empty) - domain.copy(functions = functions, axioms = axioms)(adt.pos, adt.info, adt.errT) + (constructors map generateTagAxiom(domain)) ++ Seq(generateExclusivityAxiom(domain)(constructors)) + val derivingAxioms = if (derivingInfo.contains(getContainsFunctionName)) + constructors filter (_.formalArgs.nonEmpty) map generateContainsAxiom(domain, derivingInfo(getContainsFunctionName)._2) else Seq.empty + domain.copy(functions = functions, axioms = axioms ++ derivingAxioms)(adt.pos, adt.info, adt.errT) } } @@ -197,7 +199,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager { val tagApp = DomainFuncApp( getTagName(ada.adtName), Seq(ada.rcv), - ada.typVarMap // TODO: not sure about that + ada.typVarMap )(ada.pos, ada.info, Int, ada.adtName, ada.errT) EqCmp(tagApp, IntLit(getTag(ada.adtName)(ada.name))(ada.pos, ada.info, ada.errT))(ada.pos, ada.info, ada.errT) @@ -232,7 +234,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager { val constructorApp = DomainFuncApp( ac.name, localVars, - defaultTypeVarsFromDomain(domain) // TODO: not sure about that + defaultTypeVarsFromDomain(domain) )(ac.pos, ac.info, encodeAdtTypeAsDomainType(ac.typ), ac.adtName, ac.errT) val trigger = Trigger(Seq(constructorApp))(ac.pos, ac.info, ac.errT) @@ -240,7 +242,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager { val right = DomainFuncApp( getDestructorName(ac.adtName, lv.name), Seq(constructorApp), - defaultTypeVarsFromDomain(domain) // TODO: not sure about that + defaultTypeVarsFromDomain(domain) )(ac.pos, ac.info, lv.typ, ac.adtName, ac.errT) val eq = EqCmp(lv, right)(ac.pos, ac.info, ac.errT) val forall = Forall(localVarDecl, Seq(trigger), eq)(ac.pos, ac.info, ac.errT) @@ -270,7 +272,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager { val tagApp = DomainFuncApp( getTagName(domain.name), Seq(localVar), - (domain.typVars zip domain.typVars).toMap // TODO: not sure about that + (domain.typVars zip domain.typVars).toMap )(domain.pos, domain.info, Int, domain.name, domain.errT) var destructorCalls: Seq[DomainFuncApp] = Seq() @@ -280,13 +282,13 @@ class AdtEncoder(val program: Program) extends AdtNameManager { DomainFuncApp( getDestructorName(domain.name, name), Seq(localVar), - defaultTypeVarsFromDomain(domain) // TODO: not sure about that + defaultTypeVarsFromDomain(domain) )(domain.pos, domain.info, typ, domain.name, domain.errT) } DomainFuncApp( ac.name, destructorCalls, - defaultTypeVarsFromDomain(domain) // TODO: not sure about that + defaultTypeVarsFromDomain(domain) )(domain.pos, domain.info, ac.typ, domain.name, domain.errT) } @@ -347,7 +349,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager { val constructorApp = DomainFuncApp( ac.name, localVars, - defaultTypeVarsFromDomain(domain) // TODO: not sure about that + defaultTypeVarsFromDomain(domain) )(ac.pos, ac.info, encodeAdtTypeAsDomainType(ac.typ), ac.adtName, ac.errT) val trigger = Trigger(Seq(constructorApp))(ac.pos, ac.info, ac.errT) @@ -355,7 +357,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager { val tagApp = DomainFuncApp( getTagName(ac.adtName), Seq(constructorApp), - defaultTypeVarsFromDomain(domain) // TODO: not sure about that + defaultTypeVarsFromDomain(domain) )(ac.pos, ac.info, Int, ac.adtName, ac.errT) val right = IntLit(getTag(domain.name)(ac.name))(ac.pos, ac.info, ac.errT) @@ -371,17 +373,11 @@ class AdtEncoder(val program: Program) extends AdtNameManager { } /** - * This is a helper method to check if the contains domain, namely - * - * domain ContainsDomain[A,B] { - * function contains(a: A, b: B): Bool - * } - * - * was imported by import . + * This is a helper method to check if the contains function is derived for at least one adt, namely * - * @return Return true if the contains domain is present + * @return Return true if the contains function is derived for at least one adt */ - private def withContainsDomain: Boolean = program.domains.exists(_.name == getContainsDomainName) + private def containsFunctionIsDerived: Boolean = program.extensions.exists { case a: Adt => a.derivingInfo.contains(getContainsFunctionName) } /** * This method generates the corresponding contains axiom for a ADT constructor @@ -393,10 +389,11 @@ class AdtEncoder(val program: Program) extends AdtNameManager { * where C′ = C(p_1, ..., p_n). * * @param domain The domain that encodes the ADT the constructor belongs to for which we want a contains axiom + * @param blockList A list of destructor identifiers that should not be considered for the contains relations * @param ac An ADT constructor * @return The generated contains axiom */ - private def generateContainsAxiom(domain: Domain)(ac: AdtConstructor): AnonymousDomainAxiom = { + private def generateContainsAxiom(domain: Domain, blockList: Set[String])(ac: AdtConstructor): AnonymousDomainAxiom = { assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.") assert(ac.formalArgs.nonEmpty, "AdtEncoder: An error in the ADT encoding occurred.") @@ -424,7 +421,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager { Map(TypeVar("A") -> lv.typ, TypeVar("B") -> constructorApp.typ) )(ac.pos, ac.info, Bool, getContainsDomainName, ac.errT) - val axiomBody = localVars.map(containsApp).foldLeft[Exp](TrueLit()(ac.pos, ac.info, ac.errT))((a, b) => And(a, b)(ac.pos, ac.info, ac.errT)) + val axiomBody = localVars.filter(lv => !blockList.contains(lv.name)).map(containsApp).foldLeft[Exp](TrueLit()(ac.pos, ac.info, ac.errT))((a, b) => And(a, b)(ac.pos, ac.info, ac.errT)) val forall = Forall(localVarDecl, Seq(trigger), axiomBody)(ac.pos, ac.info, ac.errT) AnonymousDomainAxiom(forall)(ac.pos, ac.info, ac.adtName, ac.errT) From 993e2a315555d1c9ce9516c47db11d058796e811 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Tue, 12 Apr 2022 10:06:20 +0200 Subject: [PATCH 45/50] Fix small issue in syntax for deriving functions --- .../scala/viper/silver/plugin/standard/adt/AdtPlugin.scala | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index 2a3ad77ae..28ace3520 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -60,7 +60,7 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { def adtDerivingDecl[_: P]: P[Seq[PAdtDerivingInfo]] = P(AdtDerivesKeyword ~/ "{" ~ adtDerivingDeclBody.rep ~ "}") def adtDerivingDeclBody[_:P]: P[PAdtDerivingInfo] = FP( - idnuse ~ ("[" ~ typ ~ "]").? ~ (AdtDerivesWithoutKeyword ~/ idnuse.rep(sep = ",")).?).map { + idnuse ~ ("[" ~ typ ~ "]").? ~ (AdtDerivesWithoutKeyword ~/ idnuse.rep(sep = ",", min=1)).?).map { case (pos, (func, ttyp, bl)) => PAdtDerivingInfo(func, ttyp, bl.getOrElse(Seq.empty).toSet)(pos) } @@ -115,10 +115,7 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { } override def beforeVerify(input: Program): Program = { - println(input) - val newProgram = new AdtEncoder(input).encode() - //println(newProgram) - newProgram + new AdtEncoder(input).encode() } } From 5120fa9a03715ba514702bf1ce2a48e69891b2d1 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Tue, 12 Apr 2022 10:13:43 +0200 Subject: [PATCH 46/50] Add test for deriving system and derivable contains function --- src/test/resources/adt/contains_1.vpr | 49 +++++++++++++++++++++++ src/test/resources/adt/contains_2.vpr | 34 ++++++++++++++++ src/test/resources/adt/declarations_4.vpr | 2 +- src/test/resources/adt/declarations_6.vpr | 20 +++++++++ src/test/resources/adt/declarations_7.vpr | 17 ++++++++ 5 files changed, 121 insertions(+), 1 deletion(-) create mode 100644 src/test/resources/adt/contains_1.vpr create mode 100644 src/test/resources/adt/contains_2.vpr create mode 100644 src/test/resources/adt/declarations_6.vpr create mode 100644 src/test/resources/adt/declarations_7.vpr diff --git a/src/test/resources/adt/contains_1.vpr b/src/test/resources/adt/contains_1.vpr new file mode 100644 index 000000000..e85167110 --- /dev/null +++ b/src/test/resources/adt/contains_1.vpr @@ -0,0 +1,49 @@ +import + +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} derives { + contains +} + +adt Tree[T] { + Leaf() + Node(value: T, left:Tree[T], right:Tree[T]) +} derives { + contains +} + + +method contains_1a() { + + var a: List[Int] + a := Nil() + + var b: List[Int] + b := Cons(2, Nil()) + + var c: List[Int] + c := Cons(1, Cons(2, Nil())) + + assert contains(a,b) + assert contains(b,c) + assert contains(a,c) + assert contains(2,c) + +} + +method contains_1b() { + + var list: List[Int] + list := Cons(42, Nil()) + + var tree: Tree[List[Int]] + tree := Node(list, Leaf(), Leaf()) + + + assert contains(42, list) + assert contains(list, tree) + assert contains(42, tree) + +} \ No newline at end of file diff --git a/src/test/resources/adt/contains_2.vpr b/src/test/resources/adt/contains_2.vpr new file mode 100644 index 000000000..2c0b62817 --- /dev/null +++ b/src/test/resources/adt/contains_2.vpr @@ -0,0 +1,34 @@ +import + +adt List[T] { + Nil() + Cons(value: T, tail: List[T]) +} derives { + contains without value +} + +method contains_2a() { + + //:: ExpectedOutput(assert.failed:assertion.false) + assert contains(2,Cons(2, Nil())) + +} + +method contains_2b() { + + var a: List[Int] + a := Nil() + + var b: List[Int] + b := Cons(2, Nil()) + + var c: List[Int] + c := Cons(1, Cons(2, Nil())) + + assert contains(a,b) + assert contains(b,c) + assert contains(a,c) + //:: ExpectedOutput(assert.failed:assertion.false) + assert contains(2,c) + +} \ No newline at end of file diff --git a/src/test/resources/adt/declarations_4.vpr b/src/test/resources/adt/declarations_4.vpr index 9d704cb0c..cbd4775d6 100644 --- a/src/test/resources/adt/declarations_4.vpr +++ b/src/test/resources/adt/declarations_4.vpr @@ -1,6 +1,6 @@ -//:: ExpectedOutput(typechecker.error) adt SpecialList[T, S] { SpecialNil() + //:: ExpectedOutput(typechecker.error) TCons(elemT: T, tail: SpecialList[T,S]) SCons(elemS: S, tail: SpecialList[T,S]) } \ No newline at end of file diff --git a/src/test/resources/adt/declarations_6.vpr b/src/test/resources/adt/declarations_6.vpr new file mode 100644 index 000000000..775d94bd0 --- /dev/null +++ b/src/test/resources/adt/declarations_6.vpr @@ -0,0 +1,20 @@ +import + +adt List[T] { + Nil() + Cons(value:T, tail:List[T]) +} derives { contains } + +adt SimpleList { + SimpleNil() + SimpleCons(value: Int, tail: SimpleList) +} derives { + contains without tail +} + +adt Tree3[T] { + Leaf3() + Node3(value: T, left: Tree3[T], middle: Tree3[T], right: Tree3[T]) +} derives { + contains without middle, right +} \ No newline at end of file diff --git a/src/test/resources/adt/declarations_7.vpr b/src/test/resources/adt/declarations_7.vpr new file mode 100644 index 000000000..f5bef08ee --- /dev/null +++ b/src/test/resources/adt/declarations_7.vpr @@ -0,0 +1,17 @@ +import + +adt SimpleList { + SimpleNil() + SimpleCons(value: Int, tail: SimpleList) +} derives { + //:: ExpectedOutput(typechecker.error) + contains without Leaf3 +} + +adt Tree3[T] { + Leaf3() + Node3(value: T, left: Tree3[T], middle: Tree3[T], right: Tree3[T]) +} derives { + //:: ExpectedOutput(typechecker.error) + contains without middle, right, hello +} \ No newline at end of file From 8de12f345cca02ad8de3d7f35a359d48b2b3194d Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Tue, 12 Apr 2022 10:43:34 +0200 Subject: [PATCH 47/50] Minor changes in ADT constructor argument handling -Only allow PFormalArgDecl's as PAdtConstructor arguments -Only allow LocalVarDecl's as AdtConstructor arguments --- .../plugin/standard/adt/AdtASTExtension.scala | 12 ++-- .../standard/adt/AdtPASTExtension.scala | 12 ++-- .../plugin/standard/adt/AdtPlugin.scala | 6 +- .../standard/adt/encoding/AdtEncoder.scala | 70 +++++++++---------- 4 files changed, 50 insertions(+), 50 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala index 80a80d812..4bc88628f 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala @@ -59,14 +59,14 @@ case class Adt(name: String, constructors: Seq[AdtConstructor], typVars: Seq[Typ * @param typ the return type of the constructor * @param adtName the name corresponding of the corresponding ADT */ -case class AdtConstructor(name: String, formalArgs: Seq[AnyLocalVarDecl]) +case class AdtConstructor(name: String, formalArgs: Seq[LocalVarDecl]) (val pos: Position, val info: Info, val typ: AdtType, val adtName : String, val errT: ErrorTrafo) extends ExtensionMember { override def getMetadata:Seq[Any] = { Seq(pos, info, errT) } - val scopedDecls: Seq[Declaration] = formalArgs.filter(p => p.isInstanceOf[LocalVarDecl]).asInstanceOf[Seq[LocalVarDecl]] + val scopedDecls: Seq[Declaration] = formalArgs override def extensionSubnodes: Seq[Node] = formalArgs @@ -78,7 +78,7 @@ case class AdtConstructor(name: String, formalArgs: Seq[AnyLocalVarDecl]) else { assert(children.length == 2, s"AdtConstructor : expected length 2 but got ${children.length}") val first = children.head.asInstanceOf[String] - val second = children.tail.head.asInstanceOf[Seq[AnyLocalVarDecl]] + val second = children.tail.head.asInstanceOf[Seq[LocalVarDecl]] AdtConstructor(first, second)(this.pos, this.info, this.typ, this.adtName, this.errT).asInstanceOf[this.type] } @@ -86,7 +86,7 @@ case class AdtConstructor(name: String, formalArgs: Seq[AnyLocalVarDecl]) } object AdtConstructor { - def apply(adt: Adt, name: String, formalArgs: Seq[AnyLocalVarDecl])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): AdtConstructor = { + def apply(adt: Adt, name: String, formalArgs: Seq[LocalVarDecl])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): AdtConstructor = { AdtConstructor(name, formalArgs)(pos, info, AdtType(adt, (adt.typVars zip adt.typVars).toMap), adt.name, errT) } } @@ -245,9 +245,9 @@ case class AdtDestructorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, Type object AdtDestructorApp { def apply(adt : Adt, name: String, rcv: Exp, typVarMap: Map[TypeVar, Type])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos) : AdtDestructorApp = { - val matchingConstructors = adt.constructors flatMap (c => c.formalArgs.filter { case LocalVarDecl(lvName, _) => lvName == name }) + val matchingConstructors = adt.constructors flatMap (c => c.formalArgs.filter { lv => lv.name == name }) assert(matchingConstructors.length == 1, s"AdtDestructorApp : expected length 1 but got ${matchingConstructors.length}") - val typ = matchingConstructors.head.asInstanceOf[LocalVarDecl].typ + val typ = matchingConstructors.head.typ AdtDestructorApp(name, rcv, typVarMap)(pos, info, typ.substitute(typVarMap), adt.name, errT) } } diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index 68e1d1220..d3e7cbfb3 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -101,7 +101,7 @@ object PAdt { } -case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])(val adtName: PIdnUse)(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { +case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl])(val adtName: PIdnUse)(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { override val getSubnodes: Seq[PNode] = Seq(idndef) ++ formalArgs @@ -121,7 +121,11 @@ case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])( override def translateMemberSignature(t: Translator): AdtConstructor = { val adt = PAdt.findAdt(adtName, t) - AdtConstructor(adt, idndef.name, formalArgs map t.liftAnyVarDecl)(t.liftPos(this)) + AdtConstructor( + adt, + idndef.name, + formalArgs map {arg => LocalVarDecl(arg.idndef.name, t.ttyp(arg.typ))(t.liftPos(arg.idndef)) } + )(t.liftPos(this)) } override def translateMember(t: Translator): AdtConstructor = { @@ -134,7 +138,7 @@ case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])( else { assert(children.length == 2, s"PAdtConstructor : expected length 2 but got ${children.length}") val first = children.head.asInstanceOf[PIdnDef] - val second = children.tail.head.asInstanceOf[Seq[PAnyFormalArgDecl]] + val second = children.tail.head.asInstanceOf[Seq[PFormalArgDecl]] PAdtConstructor(first, second)(this.adtName)(pos.getOrElse(this.pos)).asInstanceOf[this.type] } } @@ -151,7 +155,7 @@ object PAdtConstructor { def findAdtConstructor(id: PIdentifier, t: Translator): AdtConstructor = t.getMembers()(id.name).asInstanceOf[AdtConstructor] } -case class PAdtConstructor1(idndef: PIdnDef, formalArgs: Seq[PAnyFormalArgDecl])(val pos: (Position, Position)) +case class PAdtConstructor1(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl])(val pos: (Position, Position)) case class PAdtDerivingInfo(idnuse: PIdnUse, param: Option[PType], blockList: Set[PIdnUse])(val pos: (Position, Position)) extends PExtender { diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index 28ace3520..b6ea085ed 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -9,7 +9,7 @@ package viper.silver.plugin.standard.adt import fastparse._ import viper.silver.ast.Program import viper.silver.ast.utility.rewriter.StrategyBuilder -import viper.silver.parser.FastParser.{FP, anyFormalArgList, idndef, idnuse, typ, whitespace} +import viper.silver.parser.FastParser.{FP, formalArg, idndef, idnuse, typ, whitespace} import viper.silver.parser._ import viper.silver.plugin.standard.adt.encoding.AdtEncoder import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} @@ -72,7 +72,9 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { } } - def adtConstructorSignature[_: P]: P[(PIdnDef, Seq[PAnyFormalArgDecl])] = P(idndef ~ "(" ~ anyFormalArgList ~ ")") + def adtConstructorSignature[_: P]: P[(PIdnDef, Seq[PFormalArgDecl])] = P(idndef ~ "(" ~ formalArgList ~ ")") + + def formalArgList[_: P]: P[Seq[PFormalArgDecl]] = P(formalArg.rep(sep = ",")) override def beforeParse(input: String, isImported: Boolean): String = { if (!isImported) { diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala index 9fa135338..a7a792b8b 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala @@ -159,19 +159,17 @@ class AdtEncoder(val program: Program) extends AdtNameManager { */ private def generateDestructorDeclarations(domain:Domain)(ac: AdtConstructor): Seq[DomainFunc] = { assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.") - ac.formalArgs.map { - case LocalVarDecl(name, typ) => - val args = Seq(localVarTDeclFromType(encodeAdtTypeAsDomainType(ac.typ))(ac.pos, ac.info, ac.errT)) - val ttyp = typ match { - case a:AdtType => encodeAdtTypeAsDomainType(a) - case d => d - } - DomainFunc( - getDestructorName(ac.adtName, name), - args, - ttyp - )(ac.pos, ac.info, ac.adtName, ac.errT) - case _ => sys.error("AdtEncoder : Only LocalVarDecl are allowed as arguments of an Adt constructor") + ac.formalArgs.map { lv => + val args = Seq(localVarTDeclFromType(encodeAdtTypeAsDomainType(ac.typ))(ac.pos, ac.info, ac.errT)) + val ttyp = lv.typ match { + case a:AdtType => encodeAdtTypeAsDomainType(a) + case d => d + } + DomainFunc( + getDestructorName(ac.adtName, lv.name), + args, + ttyp + )(ac.pos, ac.info, ac.adtName, ac.errT) } } @@ -222,12 +220,11 @@ class AdtEncoder(val program: Program) extends AdtNameManager { private def generateInjectivityAxiom(domain: Domain)(ac: AdtConstructor): Seq[AnonymousDomainAxiom] = { assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.") val localVarDecl = ac.formalArgs.collect {case l:LocalVarDecl => l } - val localVars = ac.formalArgs.map { - case LocalVarDecl(name, typ) => - typ match { - case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(name))(ac.pos, ac.info, ac.errT) - case d => localVarTFromType(d, Some(name))(ac.pos, ac.info, ac.errT) - } + val localVars = ac.formalArgs.map { lv => + lv.typ match { + case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(lv.name))(ac.pos, ac.info, ac.errT) + case d => localVarTFromType(d, Some(lv.name))(ac.pos, ac.info, ac.errT) + } } assert(localVarDecl.size == localVars.size, "AdtEncoder: An error in the ADT encoding occurred.") @@ -277,13 +274,12 @@ class AdtEncoder(val program: Program) extends AdtNameManager { var destructorCalls: Seq[DomainFuncApp] = Seq() val rhss = acs.map { ac => - destructorCalls = ac.formalArgs.map { - case LocalVarDecl(name, typ) => - DomainFuncApp( - getDestructorName(domain.name, name), - Seq(localVar), - defaultTypeVarsFromDomain(domain) - )(domain.pos, domain.info, typ, domain.name, domain.errT) + destructorCalls = ac.formalArgs.map { lv => + DomainFuncApp( + getDestructorName(domain.name, lv.name), + Seq(localVar), + defaultTypeVarsFromDomain(domain) + )(domain.pos, domain.info, lv.typ, domain.name, domain.errT) } DomainFuncApp( ac.name, @@ -337,12 +333,11 @@ class AdtEncoder(val program: Program) extends AdtNameManager { assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.") val localVarDecl = ac.formalArgs.collect {case l:LocalVarDecl => l } - val localVars = ac.formalArgs.map { - case LocalVarDecl(name, typ) => - typ match { - case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(name))(ac.pos, ac.info, ac.errT) - case d => localVarTFromType(d, Some(name))(ac.pos, ac.info, ac.errT) - } + val localVars = ac.formalArgs.map { lv => + lv.typ match { + case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(lv.name))(ac.pos, ac.info, ac.errT) + case d => localVarTFromType(d, Some(lv.name))(ac.pos, ac.info, ac.errT) + } } assert(localVarDecl.size == localVars.size, "AdtEncoder: An error in the ADT encoding occurred.") @@ -398,12 +393,11 @@ class AdtEncoder(val program: Program) extends AdtNameManager { assert(ac.formalArgs.nonEmpty, "AdtEncoder: An error in the ADT encoding occurred.") val localVarDecl = ac.formalArgs.collect {case l:LocalVarDecl => l } - val localVars = ac.formalArgs.map { - case LocalVarDecl(name, typ) => - typ match { - case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(name))(ac.pos, ac.info, ac.errT) - case d => localVarTFromType(d, Some(name))(ac.pos, ac.info, ac.errT) - } + val localVars = ac.formalArgs.map { lv => + lv.typ match { + case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(lv.name))(ac.pos, ac.info, ac.errT) + case d => localVarTFromType(d, Some(lv.name))(ac.pos, ac.info, ac.errT) + } } assert(localVarDecl.size == localVars.size, "AdtEncoder: An error in the ADT encoding occurred.") From f55e455dac752fb47ddfa98504ae91bdc199e11e Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Mon, 25 Apr 2022 16:53:52 +0200 Subject: [PATCH 48/50] Make the ADT plugin a default plugin -Add the possibility to disable ADT plugin --- .../silver/frontend/SilFrontEndConfig.scala | 7 +++++++ .../viper/silver/frontend/SilFrontend.scala | 1 + .../silver/plugin/standard/adt/AdtPlugin.scala | 18 ++++++++++++++++-- 3 files changed, 24 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala index 6e4517bbb..26e567cc2 100644 --- a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala +++ b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala @@ -111,6 +111,13 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str hidden = true ) + val adtPlugin = opt[Boolean]("disableAdtPlugin", + descr = "Disable the ADT plugin, which adds support for ADTs as a built-in type.", + default = Some(false), + noshort = true, + hidden = true + ) + val assumeInjectivityOnInhale = opt[Boolean]("assumeInjectivityOnInhale", descr = "Assumes injectivity of the receiver expression when inhaling quantified permissions, instead of checking it.", default = Some(false), diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala index ec6443830..b5793f230 100644 --- a/src/main/scala/viper/silver/frontend/SilFrontend.scala +++ b/src/main/scala/viper/silver/frontend/SilFrontend.scala @@ -81,6 +81,7 @@ trait SilFrontend extends DefaultFrontend { * All default plugins can be excluded from the plugins by providing the --disableDefaultPlugins flag */ private val defaultPlugins: Seq[String] = Seq( + "viper.silver.plugin.standard.adt.AdtPlugin", "viper.silver.plugin.standard.termination.TerminationPlugin", "viper.silver.plugin.standard.predicateinstance.PredicateInstancePlugin" ) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index b6ea085ed..10aa8e8cf 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -15,7 +15,11 @@ import viper.silver.plugin.standard.adt.encoding.AdtEncoder import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin} -class AdtPlugin extends SilverPlugin with ParserPluginTemplate { +class AdtPlugin(reporter: viper.silver.reporter.Reporter, + logger: ch.qos.logback.classic.Logger, + config: viper.silver.frontend.SilFrontendConfig) extends SilverPlugin with ParserPluginTemplate { + + private def deactivated: Boolean = config != null && config.adtPlugin.toOption.getOrElse(false) /** * This field is set during the beforeParse method @@ -77,6 +81,10 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { def formalArgList[_: P]: P[Seq[PFormalArgDecl]] = P(formalArg.rep(sep = ",")) override def beforeParse(input: String, isImported: Boolean): String = { + if (deactivated) { + return input + } + if (!isImported) { // Add new parser adt declaration keyword ParserExtension.addNewKeywords(Set[String](AdtKeyword)) @@ -88,6 +96,9 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { } override def beforeResolve(input: PProgram): PProgram = { + if (deactivated) { + return input + } // Syntax of adt types, adt constructor calls and destructor calls can not be distinguished from ordinary // viper syntax, hence we need the following transforming step before resolving. val declaredAdtNames = input.extensions.collect { case a: PAdt => a.idndef }.toSet @@ -117,7 +128,10 @@ class AdtPlugin extends SilverPlugin with ParserPluginTemplate { } override def beforeVerify(input: Program): Program = { - new AdtEncoder(input).encode() + if (deactivated) { + return input + } + new AdtEncoder(input).encode() } } From 4e4d861491228911a60736efb5fdd459287c5f0b Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Tue, 26 Apr 2022 16:29:03 +0200 Subject: [PATCH 49/50] Fix the plugin tests -In commit f55e455dac752fb47ddfa98504ae91bdc199e1e thee ADT plugin was added to the default plugins, hence the number of defualt plugins is now 3. --- src/test/scala/PluginTests.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/scala/PluginTests.scala b/src/test/scala/PluginTests.scala index 29ed76f7a..d9d3b5be8 100644 --- a/src/test/scala/PluginTests.scala +++ b/src/test/scala/PluginTests.scala @@ -225,7 +225,7 @@ class PluginTests extends AnyFunSuite { ) // number of plugins running by default - val defaultPlugins = 2 + val defaultPlugins = 3 var result: VerificationResult = Success From 81b2a0241fa900631b98c84c157a40fa9c6a7994 Mon Sep 17 00:00:00 2001 From: Alessandro Maissen Date: Tue, 26 Apr 2022 17:22:02 +0200 Subject: [PATCH 50/50] Fix some whitespace and formatting issues --- .../plugin/standard/adt/AdtASTExtension.scala | 94 +++++----- .../standard/adt/AdtPASTExtension.scala | 163 ++++++++++-------- .../plugin/standard/adt/AdtPlugin.scala | 68 ++++---- .../standard/adt/encoding/AdtEncoder.scala | 91 +++++----- .../adt/encoding/AdtNameManager.scala | 26 +-- 5 files changed, 237 insertions(+), 205 deletions(-) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala index 4bc88628f..21766f1e5 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala @@ -15,13 +15,13 @@ import viper.silver.verifier.{ConsistencyError, Failure, VerificationResult} /** * This class represents a user-defined ADT. * - * @param name name of the ADT + * @param name name of the ADT * @param constructors sequence of corresponding constructors - * @param typVars sequence of type variables (generics) + * @param typVars sequence of type variables (generics) * @param derivingInfo a map that maps identifiers of derivable functions to a tuple containing an optional type param and a set of excluded constructor argument identifiers */ case class Adt(name: String, constructors: Seq[AdtConstructor], typVars: Seq[TypeVar] = Nil, derivingInfo: Map[String, (Option[Type], Set[String])] = Map.empty) - (val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionMember { + (val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionMember { val scopedDecls: Seq[Declaration] = Seq() override def extensionSubnodes: Seq[Node] = constructors ++ typVars ++ derivingInfo.map(_._2._1).collect { case Some(v) => v } @@ -31,11 +31,11 @@ case class Adt(name: String, constructors: Seq[AdtConstructor], typVars: Seq[Typ def showDerivingInfo(di: (String, (Option[Type], Set[String]))): PrettyPrintPrimitives#Cont = { val (func, (param, blocklist)) = di text(func) <> (if (param.isEmpty) nil else text("[") <> showType(param.get) <> space <> "]") <> - space <> (if (blocklist.isEmpty) nil else text("without") <> space <> ssep(blocklist.toSeq map text, char (',') <> space)) + space <> (if (blocklist.isEmpty) nil else text("without") <> space <> ssep(blocklist.toSeq map text, char(',') <> space)) } text("adt") <+> name <> - (if (typVars.isEmpty) nil else text("[") <> ssep(typVars map show, char (',') <> space) <> "]") <+> + (if (typVars.isEmpty) nil else text("[") <> ssep(typVars map show, char(',') <> space) <> "]") <+> braces(nest(defaultIndent, line <> line <> ssep(constructors map show, line <> line) @@ -45,7 +45,7 @@ case class Adt(name: String, constructors: Seq[AdtConstructor], typVars: Seq[Typ line <> line <> ssep(derivingInfo.toSeq map showDerivingInfo, line <> line) ) <> line) - ) + ) } } @@ -54,19 +54,20 @@ case class Adt(name: String, constructors: Seq[AdtConstructor], typVars: Seq[Typ * Adt - this should be used in general for creation (so that typ is guaranteed to * be set correctly) * - * @param name name of the ADT constructor + * @param name name of the ADT constructor * @param formalArgs sequence of arguments of the constructor - * @param typ the return type of the constructor - * @param adtName the name corresponding of the corresponding ADT + * @param typ the return type of the constructor + * @param adtName the name corresponding of the corresponding ADT */ case class AdtConstructor(name: String, formalArgs: Seq[LocalVarDecl]) - (val pos: Position, val info: Info, val typ: AdtType, val adtName : String, val errT: ErrorTrafo) + (val pos: Position, val info: Info, val typ: AdtType, val adtName: String, val errT: ErrorTrafo) extends ExtensionMember { - override def getMetadata:Seq[Any] = { + val scopedDecls: Seq[Declaration] = formalArgs + + override def getMetadata: Seq[Any] = { Seq(pos, info, errT) } - val scopedDecls: Seq[Declaration] = formalArgs override def extensionSubnodes: Seq[Node] = formalArgs @@ -86,7 +87,8 @@ case class AdtConstructor(name: String, formalArgs: Seq[LocalVarDecl]) } object AdtConstructor { - def apply(adt: Adt, name: String, formalArgs: Seq[LocalVarDecl])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): AdtConstructor = { + def apply(adt: Adt, name: String, formalArgs: Seq[LocalVarDecl]) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): AdtConstructor = { AdtConstructor(name, formalArgs)(pos, info, AdtType(adt, (adt.typVars zip adt.typVars).toMap), adt.name, errT) } } @@ -96,15 +98,15 @@ object AdtConstructor { * Adt - this should be used in general for creation (so that typeParameters is guaranteed to * be set correctly) * - * @param adtName The name of the underlying adt. + * @param adtName The name of the underlying adt. * @param partialTypVarsMap Maps type parameters to (possibly concrete) types. May not map all * type parameters, may even be empty. - * @param typeParameters The type variables of the ADT type. + * @param typeParameters The type variables of the ADT type. */ case class AdtType(adtName: String, partialTypVarsMap: Map[TypeVar, Type]) (val typeParameters: Seq[TypeVar]) extends ExtensionType { - override lazy val check: Seq[ConsistencyError] = if(!(typeParameters.toSet == typVarsMap.keys.toSet)) { + override lazy val check: Seq[ConsistencyError] = if (!(typeParameters.toSet == typVarsMap.keys.toSet)) { Seq(ConsistencyError(s"${typeParameters.toSet} doesn't equal ${typVarsMap.keys.toSet}", NoPosition)) } else Seq() @@ -120,8 +122,8 @@ case class AdtType(adtName: String, partialTypVarsMap: Map[TypeVar, Type]) * occurrences of those type variables with the corresponding type. */ override def substitute(newTypVarsMap: Map[TypeVar, Type]): Type = { - assert (typVarsMap.keys.toSet equals this.typeParameters.toSet) - val newTypeMap = typVarsMap.map(kv=>kv._1 -> kv._2.substitute(newTypVarsMap)) + assert(typVarsMap.keys.toSet equals this.typeParameters.toSet) + val newTypeMap = typVarsMap.map(kv => kv._1 -> kv._2.substitute(newTypVarsMap)) AdtType(adtName, newTypeMap)(typeParameters) } @@ -130,7 +132,7 @@ case class AdtType(adtName: String, partialTypVarsMap: Map[TypeVar, Type]) override def prettyPrint: PrettyPrintPrimitives#Cont = { val typArgs = typeParameters map (t => show(typVarsMap.getOrElse(t, t))) - text(adtName) <> (if (typArgs.isEmpty) nil else brackets(ssep(typArgs, char (',') <> space))) + text(adtName) <> (if (typArgs.isEmpty) nil else brackets(ssep(typArgs, char(',') <> space))) } override def withChildren(children: Seq[Any], pos: Option[(Position, Position)], forceRewrite: Boolean): this.type = { @@ -146,7 +148,7 @@ case class AdtType(adtName: String, partialTypVarsMap: Map[TypeVar, Type]) } -object AdtType{ +object AdtType { def apply(adt: Adt, typVarsMap: Map[TypeVar, Type]): AdtType = AdtType(adt.name, typVarsMap)(adt.typVars) } @@ -157,24 +159,24 @@ object AdtType{ * Adt constructor - this should be used in general for creation (so that typ is guaranteed to * be set correctly) * - * @param name The name of the ADT constructor - * @param args A sequence of expressions passed as arguments to the constructor + * @param name The name of the ADT constructor + * @param args A sequence of expressions passed as arguments to the constructor * @param typVarMap Maps type parameters to (possibly concrete) types. May not map all * type parameters, may even be empty. - * @param typ The return type of the constructor - * @param adtName The corresponding ADT name + * @param typ The return type of the constructor + * @param adtName The corresponding ADT name */ case class AdtConstructorApp(name: String, args: Seq[Exp], typVarMap: Map[TypeVar, Type]) - (val pos: Position, val info: Info, override val typ: Type, val adtName:String, val errT: ErrorTrafo) + (val pos: Position, val info: Info, override val typ: Type, val adtName: String, val errT: ErrorTrafo) extends ExtensionExp { - override lazy val check : Seq[ConsistencyError] = args.flatMap(Consistency.checkPure) + override lazy val check: Seq[ConsistencyError] = args.flatMap(Consistency.checkPure) override def prettyPrint: PrettyPrintPrimitives#Cont = { if (typVarMap.nonEmpty) // Type may be under-constrained, so to be safe we explicitly print out the type. - parens(text(name) <> parens(ssep(args map show, char (',') <> space)) <> char(':') <+> show(typ)) + parens(text(name) <> parens(ssep(args map show, char(',') <> space)) <> char(':') <+> show(typ)) else - text(name) <> parens(ssep(args map show, char (',') <> space)) + text(name) <> parens(ssep(args map show, char(',') <> space)) } override def extensionIsPure: Boolean = true @@ -198,8 +200,10 @@ case class AdtConstructorApp(name: String, args: Seq[Exp], typVarMap: Map[TypeVa } } } + object AdtConstructorApp { - def apply(constructor : AdtConstructor, args: Seq[Exp], typVarMap: Map[TypeVar, Type])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos) : AdtConstructorApp = + def apply(constructor: AdtConstructor, args: Seq[Exp], typVarMap: Map[TypeVar, Type]) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): AdtConstructorApp = AdtConstructorApp(constructor.name, args, typVarMap)(pos, info, constructor.typ.substitute(typVarMap), constructor.adtName, errT) } @@ -208,16 +212,17 @@ object AdtConstructorApp { * Adt - this should be used in general for creation (so that typ is guaranteed to * be set correctly) * - * @param name The name of the argument of an ADT constructor the destructor corresponds to - * @param rcv An expression on with the the destructor is applied + * @param name The name of the argument of an ADT constructor the destructor corresponds to + * @param rcv An expression on with the the destructor is applied * @param typVarMap Maps type parameters to (possibly concrete) types. May not map all * type parameters, may even be empty. - * @param typ The return type of the destructor - * @param adtName The corresponding ADT name + * @param typ The return type of the destructor + * @param adtName The corresponding ADT name */ -case class AdtDestructorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, Type])(val pos: Position, val info: Info, override val typ: Type, val adtName:String, val errT: ErrorTrafo) extends ExtensionExp { +case class AdtDestructorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, Type]) + (val pos: Position, val info: Info, override val typ: Type, val adtName: String, val errT: ErrorTrafo) extends ExtensionExp { - override lazy val check : Seq[ConsistencyError] = Consistency.checkPure(rcv) + override lazy val check: Seq[ConsistencyError] = Consistency.checkPure(rcv) override def prettyPrint: PrettyPrintPrimitives#Cont = show(rcv) <> "." <> name @@ -244,7 +249,8 @@ case class AdtDestructorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, Type } object AdtDestructorApp { - def apply(adt : Adt, name: String, rcv: Exp, typVarMap: Map[TypeVar, Type])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos) : AdtDestructorApp = { + def apply(adt: Adt, name: String, rcv: Exp, typVarMap: Map[TypeVar, Type]) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): AdtDestructorApp = { val matchingConstructors = adt.constructors flatMap (c => c.formalArgs.filter { lv => lv.name == name }) assert(matchingConstructors.length == 1, s"AdtDestructorApp : expected length 1 but got ${matchingConstructors.length}") val typ = matchingConstructors.head.typ @@ -257,17 +263,18 @@ object AdtDestructorApp { * Adt - this should be used in general for creation (so that adtName is guaranteed to * be set correctly) * - * @param name The name of the argument of an ADT constructor the destructor corresponds to - * @param rcv An expression on with the the destructor is applied + * @param name The name of the argument of an ADT constructor the destructor corresponds to + * @param rcv An expression on with the the destructor is applied * @param typVarMap Maps type parameters to (possibly concrete) types. May not map all * type parameters, may even be empty. - * @param adtName The corresponding ADT name + * @param adtName The corresponding ADT name */ -case class AdtDiscriminatorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, Type])(val pos: Position, val info: Info, val adtName:String, val errT: ErrorTrafo) extends ExtensionExp { +case class AdtDiscriminatorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, Type]) + (val pos: Position, val info: Info, val adtName: String, val errT: ErrorTrafo) extends ExtensionExp { - override def typ: Type = Bool + override lazy val check: Seq[ConsistencyError] = Consistency.checkPure(rcv) - override lazy val check : Seq[ConsistencyError] = Consistency.checkPure(rcv) + override def typ: Type = Bool override def prettyPrint: PrettyPrintPrimitives#Cont = show(rcv) <> "." <> name <> "?" @@ -295,7 +302,8 @@ case class AdtDiscriminatorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, T } object AdtDiscriminatorApp { - def apply(adt : Adt, name: String, rcv: Exp, typVarMap: Map[TypeVar, Type])(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos) : AdtDiscriminatorApp = { + def apply(adt: Adt, name: String, rcv: Exp, typVarMap: Map[TypeVar, Type]) + (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): AdtDiscriminatorApp = { AdtDiscriminatorApp(name, rcv, typVarMap)(pos, info, adt.name, errT) } } diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala index d3e7cbfb3..d34d04abb 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala @@ -14,7 +14,8 @@ import viper.silver.plugin.standard.adt.PAdtConstructor.findAdtConstructor import scala.util.{Success, Try} -case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[PAdtConstructor], derivingInfos: Seq[PAdtDerivingInfo])(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { +case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[PAdtConstructor], derivingInfos: Seq[PAdtDerivingInfo]) + (val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { override val getSubnodes: Seq[PNode] = Seq(idndef) ++ typVars ++ constructors ++ derivingInfos @@ -23,8 +24,8 @@ case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[P constructors foreach (_.typecheck(t, n)) } // Check that formalArg identifiers among all constructors are unique - val allFormalArgs = constructors flatMap (_.formalArgs collect { case fad:PFormalArgDecl => fad }) - val duplicateArgs = allFormalArgs.groupBy(_.idndef.name).collect { case (_,ys) if ys.size > 1 => ys.head }.toSeq + val allFormalArgs = constructors flatMap (_.formalArgs collect { case fad: PFormalArgDecl => fad }) + val duplicateArgs = allFormalArgs.groupBy(_.idndef.name).collect { case (_, ys) if ys.size > 1 => ys.head }.toSeq t.messages ++= duplicateArgs.flatMap { arg => FastMessaging.message(arg.idndef, "Duplicate argument identifier `" + arg.idndef.name + "' among adt constructors at " + arg.idndef.pos._1) } @@ -38,12 +39,12 @@ case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[P } // Check duplicate deriving infos - val duplicateDerivingInfo = derivingInfos.groupBy(_.idnuse).collect { case (_,ys) if ys.size > 1 => ys.head }.toSeq + val duplicateDerivingInfo = derivingInfos.groupBy(_.idnuse).collect { case (_, ys) if ys.size > 1 => ys.head }.toSeq t.messages ++= duplicateDerivingInfo.flatMap { di => FastMessaging.message(di.idnuse, "Duplicate derivation of function `" + di.idnuse.name + "' at " + di.idnuse.pos._1) } - derivingInfos.foreach(_.typecheck(t,n)) + derivingInfos.foreach(_.typecheck(t, n)) None } @@ -54,14 +55,14 @@ case class PAdt(idndef: PIdnDef, typVars: Seq[PTypeVarDecl], constructors: Seq[P idndef.name, null, typVars map (t => TypeVar(t.idndef.name)), - derivingInfos.map( a => (a.idnuse.name, (if (a.param.nonEmpty) Some(t.ttyp(a.param.get)) else None, a.blockList.map(_.name)))).toMap + derivingInfos.map(a => (a.idnuse.name, (if (a.param.nonEmpty) Some(t.ttyp(a.param.get)) else None, a.blockList.map(_.name)))).toMap )(t.liftPos(this)) } override def translateMember(t: Translator): Member = { // In a first step translate constructor signatures - constructors map ( c => { + constructors map (c => { val cc = c.translateMemberSignature(t) t.getMembers().put(c.idndef.name, cc) }) @@ -94,14 +95,15 @@ object PAdt { * This is a helper method helper that can be called if one knows which 'id' refers to an ADT * * @param id identifier of the ADT - * @param t translator unit + * @param t translator unit * @return the corresponding ADT object */ def findAdt(id: PIdentifier, t: Translator): Adt = t.getMembers()(id.name).asInstanceOf[Adt] } -case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl])(val adtName: PIdnUse)(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { +case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl]) + (val adtName: PIdnUse)(val pos: (Position, Position)) extends PExtender with PMember with PGlobalDeclaration { override val getSubnodes: Seq[PNode] = Seq(idndef) ++ formalArgs @@ -124,7 +126,7 @@ case class PAdtConstructor(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl])(val AdtConstructor( adt, idndef.name, - formalArgs map {arg => LocalVarDecl(arg.idndef.name, t.ttyp(arg.typ))(t.liftPos(arg.idndef)) } + formalArgs map { arg => LocalVarDecl(arg.idndef.name, t.ttyp(arg.typ))(t.liftPos(arg.idndef)) } )(t.liftPos(this)) } @@ -159,15 +161,16 @@ case class PAdtConstructor1(idndef: PIdnDef, formalArgs: Seq[PFormalArgDecl])(va case class PAdtDerivingInfo(idnuse: PIdnUse, param: Option[PType], blockList: Set[PIdnUse])(val pos: (Position, Position)) extends PExtender { - override def getSubnodes():Seq[PNode] = Seq(idnuse) ++ param.toSeq + override def getSubnodes(): Seq[PNode] = Seq(idnuse) ++ param.toSeq - override def typecheck(t: TypeChecker, n: NameAnalyser):Option[Seq[String]] = { + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { param.foreach(t.check) None } } -case class PAdtType(adt: PIdnUse, args: Seq[PType])(val pos: (Position, Position)) extends PExtender with PGenericType { +case class PAdtType(adt: PIdnUse, args: Seq[PType]) + (val pos: (Position, Position)) extends PExtender with PGenericType { var kind: PAdtTypeKinds.Kind = PAdtTypeKinds.Unresolved @@ -175,57 +178,57 @@ case class PAdtType(adt: PIdnUse, args: Seq[PType])(val pos: (Position, Position override def typeArguments: Seq[PType] = args - override def isValidOrUndeclared: Boolean = (kind==PAdtTypeKinds.Adt || isUndeclared) && args.forall(_.isValidOrUndeclared) + override def isValidOrUndeclared: Boolean = (kind == PAdtTypeKinds.Adt || isUndeclared) && args.forall(_.isValidOrUndeclared) override def substitute(ts: PTypeSubstitution): PType = { - require(kind==PAdtTypeKinds.Adt || isUndeclared) + require(kind == PAdtTypeKinds.Adt || isUndeclared) - val newArgs = args map (a=>a.substitute(ts)) - if (args==newArgs) + val newArgs = args map (a => a.substitute(ts)) + if (args == newArgs) return this - val newAdtType = PAdtType(adt,newArgs)((NoPosition, NoPosition)) + val newAdtType = PAdtType(adt, newArgs)((NoPosition, NoPosition)) newAdtType.kind = PAdtTypeKinds.Adt newAdtType } - override def getSubnodes(): Seq[PNode] = Seq(adt) ++ args - - def isResolved: Boolean = kind != PAdtTypeKinds.Unresolved - def isUndeclared: Boolean = kind == PAdtTypeKinds.Undeclared + override def getSubnodes(): Seq[PNode] = Seq(adt) ++ args + override def subNodes: Seq[PType] = args override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { - this match { - case at@PAdtType(_, _) if at.isResolved => None - /* Already resolved, nothing left to do */ - case at@PAdtType(adt, args) => - assert(!at.isResolved, "Only yet-unresolved adt types should be type-checked and resolved") - - args foreach t.check - - var x: Any = null - - try { - x = t.names.definition(t.curMember)(adt) - } catch { - case _: Throwable => - } - - x match { - case PAdt(_, typVars, _, _) => - t.ensure(args.length == typVars.length, this, "wrong number of type arguments") - at.kind = PAdtTypeKinds.Adt - None - case _ => - at.kind = PAdtTypeKinds.Undeclared - Option(Seq(s"found undeclared type ${at.adt.name}")) - } - } + this match { + case at@PAdtType(_, _) if at.isResolved => None + /* Already resolved, nothing left to do */ + case at@PAdtType(adt, args) => + assert(!at.isResolved, "Only yet-unresolved adt types should be type-checked and resolved") + + args foreach t.check + + var x: Any = null + + try { + x = t.names.definition(t.curMember)(adt) + } catch { + case _: Throwable => + } + + x match { + case PAdt(_, typVars, _, _) => + t.ensure(args.length == typVars.length, this, "wrong number of type arguments") + at.kind = PAdtTypeKinds.Adt + None + case _ => + at.kind = PAdtTypeKinds.Undeclared + Option(Seq(s"found undeclared type ${at.adt.name}")) + } + } } + def isResolved: Boolean = kind != PAdtTypeKinds.Unresolved + override def translateType(t: Translator): Type = { t.getMembers().get(adt.name) match { case Some(d) => @@ -242,12 +245,15 @@ case class PAdtType(adt: PIdnUse, args: Seq[PType])(val pos: (Position, Position object PAdtTypeKinds { trait Kind + case object Unresolved extends Kind + case object Adt extends Kind + case object Undeclared extends Kind } -/** Common trait for ADT operator applications **/ +/** Common trait for ADT operator applications * */ sealed trait PAdtOpApp extends PExtender with POpApp { // Following fields are set during resolving, respectively in the typecheck method below @@ -256,7 +262,7 @@ sealed trait PAdtOpApp extends PExtender with POpApp { var adtSubstitution: Option[PTypeSubstitution] = None var _extraLocalTypeVariables: Set[PDomainType] = Set() - override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = PAdtOpApp.typecheck(this)(t,n) + override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = PAdtOpApp.typecheck(this)(t, n) override def typecheck(t: TypeChecker, n: NameAnalyser, expected: PType): Option[Seq[String]] = { t.checkTopTyped(this, Some(expected)) @@ -271,11 +277,11 @@ sealed trait PAdtOpApp extends PExtender with POpApp { case Some(pt) => pt case None => PTypeSubstitution.defaultType }))) - assert(s3.m.keySet==dtr.mm.keySet) + assert(s3.m.keySet == dtr.mm.keySet) assert(s3.m.forall(_._2.isGround)) adtSubstitution = Some(s3) dtr.mm.values.foldLeft(ots)( - (tss,s)=> if (tss.contains(s)) tss else tss.add(s, PTypeSubstitution.defaultType).get) + (tss, s) => if (tss.contains(s)) tss else tss.add(s, PTypeSubstitution.defaultType).get) case _ => ots } super.forceSubstitution(ts) @@ -292,17 +298,17 @@ object PAdtOpApp { */ def typecheck(poa: PAdtOpApp)(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = { - def getFreshTypeSubstitution(tvs : Seq[PDomainType]) : PTypeRenaming = + def getFreshTypeSubstitution(tvs: Seq[PDomainType]): PTypeRenaming = PTypeVar.freshTypeSubstitutionPTVs(tvs) // Checks that a substitution is fully reduced (idempotent) - def refreshWith(ts: PTypeSubstitution, rts : PTypeRenaming) : PTypeSubstitution = { + def refreshWith(ts: PTypeSubstitution, rts: PTypeRenaming): PTypeSubstitution = { require(ts.isFullyReduced) require(rts.isFullyReduced) new PTypeSubstitution(ts map (kv => rts.rename(kv._1) -> kv._2.substitute(rts))) } - var extraReturnTypeConstraint : Option[PType] = None + var extraReturnTypeConstraint: Option[PType] = None if (poa.typeSubstitutions.isEmpty) { poa.args.foreach(t.checkInternal) @@ -331,7 +337,7 @@ object PAdtOpApp { case pdc@PDestructorCall(name, _) => pdc.args.head.typ match { - case at:PAdtType => + case at: PAdtType => val adt = t.names.definition(t.curMember)(at.adt).asInstanceOf[PAdt] pdc.adt = adt val matchingConstructorArgs: Seq[PFormalArgDecl] = adt.constructors flatMap (c => c.formalArgs.collect { case fad@PFormalArgDecl(idndef, _) if idndef.name == name => fad }) @@ -394,11 +400,19 @@ object PAdtOpApp { } } -case class PConstructorCall(constr: PIdnUse, args: Seq[PExp], typeAnnotated : Option[PType] = None)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PAdtOpApp with PLocationAccess { +case class PConstructorCall(constr: PIdnUse, args: Seq[PExp], typeAnnotated: Option[PType] = None) + (val pos: (Position, Position) = (NoPosition, NoPosition)) extends PAdtOpApp with PLocationAccess { + // Following field is set during resolving, respectively in the typecheck method inherited from PAdtOpApp + var constructor: PAdtConstructor = null + override def opName: String = constr.name + override def idnuse: PIdnUse = constr - override def getSubnodes(): Seq[PNode] = Seq(constr) ++ args ++ (typeAnnotated match { case Some(t) => Seq(t) case None => Nil}) + override def getSubnodes(): Seq[PNode] = Seq(constr) ++ args ++ (typeAnnotated match { + case Some(t) => Seq(t) + case None => Nil + }) override def signatures: List[PTypeSubstitution] = { if (adt != null && constructor != null && constructor.formalArgs.size == args.size) { @@ -410,14 +424,11 @@ case class PConstructorCall(constr: PIdnUse, args: Seq[PExp], typeAnnotated : Op } else List() } - // Following field is set during resolving, respectively in the typecheck method inherited from PAdtOpApp - var constructor: PAdtConstructor = null - override def translateExp(t: Translator): Exp = { val constructor = PAdtConstructor.findAdtConstructor(constr, t) val actualArgs = args map t.exp - val so : Option[Map[TypeVar, Type]] = adtSubstitution match{ - case Some(ps) => Some(ps.m.map(kv=>TypeVar(kv._1)->t.ttyp(kv._2))) + val so: Option[Map[TypeVar, Type]] = adtSubstitution match { + case Some(ps) => Some(ps.m.map(kv => TypeVar(kv._1) -> t.ttyp(kv._2))) case None => None } so match { @@ -431,9 +442,13 @@ case class PConstructorCall(constr: PIdnUse, args: Seq[PExp], typeAnnotated : Op } -case class PDestructorCall(name: String, rcv: PExp)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PAdtOpApp { +case class PDestructorCall(name: String, rcv: PExp) + (val pos: (Position, Position) = (NoPosition, NoPosition)) extends PAdtOpApp { + // Following field is set during resolving, respectively in the typecheck method inherited from PAdtOpApp + var matchingConstructorArg: PFormalArgDecl = null + override def opName: String = name - override def args: Seq[PExp] = Seq(rcv) + override def getSubnodes(): Seq[PNode] = Seq(rcv) override def signatures: List[PTypeSubstitution] = if (adt != null && matchingConstructorArg != null) { @@ -445,13 +460,12 @@ case class PDestructorCall(name: String, rcv: PExp)(val pos: (Position, Position ) } else List() - // Following field is set during resolving, respectively in the typecheck method inherited from PAdtOpApp - var matchingConstructorArg: PFormalArgDecl = null + override def args: Seq[PExp] = Seq(rcv) override def translateExp(t: Translator): Exp = { val actualRcv = t.exp(rcv) - val so : Option[Map[TypeVar, Type]] = adtSubstitution match { - case Some(ps) => Some(ps.m.map(kv=>TypeVar(kv._1)->t.ttyp(kv._2))) + val so: Option[Map[TypeVar, Type]] = adtSubstitution match { + case Some(ps) => Some(ps.m.map(kv => TypeVar(kv._1) -> t.ttyp(kv._2))) case None => None } so match { @@ -464,11 +478,10 @@ case class PDestructorCall(name: String, rcv: PExp)(val pos: (Position, Position } } -case class PDiscriminatorCall(name: PIdnUse, rcv: PExp)(val pos: (Position, Position) = (NoPosition, NoPosition)) extends PAdtOpApp { +case class PDiscriminatorCall(name: PIdnUse, rcv: PExp) + (val pos: (Position, Position) = (NoPosition, NoPosition)) extends PAdtOpApp { override def opName: String = "is" + name.name - override def args: Seq[PExp] = Seq(rcv) - override def getSubnodes(): Seq[PNode] = Seq(name, rcv) override def signatures: List[PTypeSubstitution] = if (adt != null) { @@ -480,10 +493,12 @@ case class PDiscriminatorCall(name: PIdnUse, rcv: PExp)(val pos: (Position, Posi ) } else List() + override def args: Seq[PExp] = Seq(rcv) + override def translateExp(t: Translator): Exp = { val actualRcv = t.exp(rcv) - val so : Option[Map[TypeVar, Type]] = adtSubstitution match { - case Some(ps) => Some(ps.m.map(kv=>TypeVar(kv._1)->t.ttyp(kv._2))) + val so: Option[Map[TypeVar, Type]] = adtSubstitution match { + case Some(ps) => Some(ps.m.map(kv => TypeVar(kv._1) -> t.ttyp(kv._2))) case None => None } so match { diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala index 10aa8e8cf..19091f525 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala @@ -19,24 +19,41 @@ class AdtPlugin(reporter: viper.silver.reporter.Reporter, logger: ch.qos.logback.classic.Logger, config: viper.silver.frontend.SilFrontendConfig) extends SilverPlugin with ParserPluginTemplate { - private def deactivated: Boolean = config != null && config.adtPlugin.toOption.getOrElse(false) - + /** + * Keywords used to define ADT's + */ + private val AdtKeyword: String = "adt" + private val AdtDerivesKeyword: String = "derives" + private val AdtDerivesWithoutKeyword: String = "without" /** * This field is set during the beforeParse method */ private var derivesImported: Boolean = false + + def adtDerivingFunc[_: P]: P[PIdnUse] = FP(StringIn("contains").!).map { case (pos, id) => PIdnUse(id)(pos) } + + override def beforeParse(input: String, isImported: Boolean): String = { + if (deactivated) { + return input + } + + if (!isImported) { + // Add new parser adt declaration keyword + ParserExtension.addNewKeywords(Set[String](AdtKeyword)) + // Add new parser for adt declaration + ParserExtension.addNewDeclAtEnd(adtDecl(_)) + } + setDerivesImported(input) + input + } + + private def deactivated: Boolean = config != null && config.adtPlugin.toOption.getOrElse(false) + private def setDerivesImported(input: String): Unit = "import[\\s]+".r.findFirstIn(input) match { case Some(_) => derivesImported = true case None => } - /** - * Keywords used to define ADT's - */ - private val AdtKeyword: String = "adt" - private val AdtDerivesKeyword: String = "derives" - private val AdtDerivesWithoutKeyword: String = "without" - /** * Parser for ADT declaration. * @@ -59,17 +76,15 @@ class AdtPlugin(reporter: viper.silver.reporter.Reporter, )(pos) } - def adtTypeVarDecl[_: P]: P[PTypeVarDecl] = FP(idndef).map{ case (pos, i) => PTypeVarDecl(i)(pos) } + def adtTypeVarDecl[_: P]: P[PTypeVarDecl] = FP(idndef).map { case (pos, i) => PTypeVarDecl(i)(pos) } def adtDerivingDecl[_: P]: P[Seq[PAdtDerivingInfo]] = P(AdtDerivesKeyword ~/ "{" ~ adtDerivingDeclBody.rep ~ "}") - def adtDerivingDeclBody[_:P]: P[PAdtDerivingInfo] = FP( - idnuse ~ ("[" ~ typ ~ "]").? ~ (AdtDerivesWithoutKeyword ~/ idnuse.rep(sep = ",", min=1)).?).map { - case (pos, (func, ttyp, bl)) => PAdtDerivingInfo(func, ttyp, bl.getOrElse(Seq.empty).toSet)(pos) + def adtDerivingDeclBody[_: P]: P[PAdtDerivingInfo] = FP( + idnuse ~ ("[" ~ typ ~ "]").? ~ (AdtDerivesWithoutKeyword ~/ idnuse.rep(sep = ",", min = 1)).?).map { + case (pos, (func, ttyp, bl)) => PAdtDerivingInfo(func, ttyp, bl.getOrElse(Seq.empty).toSet)(pos) } - def adtDerivingFunc[_:P]: P[PIdnUse] = FP(StringIn("contains").!).map { case (pos, id) => PIdnUse(id)(pos) } - def adtConstructorDecl[_: P]: P[PAdtConstructor1] = FP(adtConstructorSignature ~ ";".?).map { case (pos, cdecl) => cdecl match { case (name, formalArgs) => PAdtConstructor1(name, formalArgs)(pos) @@ -80,21 +95,6 @@ class AdtPlugin(reporter: viper.silver.reporter.Reporter, def formalArgList[_: P]: P[Seq[PFormalArgDecl]] = P(formalArg.rep(sep = ",")) - override def beforeParse(input: String, isImported: Boolean): String = { - if (deactivated) { - return input - } - - if (!isImported) { - // Add new parser adt declaration keyword - ParserExtension.addNewKeywords(Set[String](AdtKeyword)) - // Add new parser for adt declaration - ParserExtension.addNewDeclAtEnd(adtDecl(_)) - } - setDerivesImported(input) - input - } - override def beforeResolve(input: PProgram): PProgram = { if (deactivated) { return input @@ -104,7 +104,9 @@ class AdtPlugin(reporter: viper.silver.reporter.Reporter, val declaredAdtNames = input.extensions.collect { case a: PAdt => a.idndef }.toSet val declaredConstructorNames = input.extensions.collect { case a: PAdt => a.constructors.map(c => c.idndef) }.flatten.toSet val declaredConstructorArgsNames = input.extensions.collect { case a: PAdt => - a.constructors flatMap ( c => c.formalArgs collect {case PFormalArgDecl(idndef, _) => idndef})}.flatten.toSet + a.constructors flatMap (c => c.formalArgs collect { case PFormalArgDecl(idndef, _) => idndef }) + }.flatten.toSet + def transformStrategy[T <: PNode](input: T): T = StrategyBuilder.Slim[PNode]({ // If derives import is missing deriving info is ignored case pa@PAdt(idndef, typVars, constructors, _) if !derivesImported => PAdt(idndef, typVars, constructors, Seq.empty)(pa.pos) @@ -114,14 +116,14 @@ class AdtPlugin(reporter: viper.silver.reporter.Reporter, // we simply treat the calls as an ordinary field access, which results in an identifier not found error. case pfa@PFieldAssign(fieldAcc, rhs) if declaredConstructorArgsNames.exists(_.name == fieldAcc.idnuse.name) || declaredConstructorNames.exists("is" + _.name == fieldAcc.idnuse.name) => - PFieldAssign(PFieldAccess(transformStrategy(fieldAcc.rcv), fieldAcc.idnuse)(fieldAcc.pos), transformStrategy(rhs))(pfa.pos) + PFieldAssign(PFieldAccess(transformStrategy(fieldAcc.rcv), fieldAcc.idnuse)(fieldAcc.pos), transformStrategy(rhs))(pfa.pos) case pfa@PFieldAccess(rcv, idnuse) if declaredConstructorArgsNames.exists(_.name == idnuse.name) => PDestructorCall(idnuse.name, rcv)(pfa.pos) case pfa@PFieldAccess(rcv, idnuse) if declaredConstructorNames.exists("is" + _.name == idnuse.name) => PDiscriminatorCall(PIdnUse(idnuse.name.substring(2))(idnuse.pos), rcv)(pfa.pos) }).recurseFunc({ // Stop the recursion if a destructor call or discriminator call is parsed as left-hand side of a field assignment case PFieldAssign(fieldAcc, _) if declaredConstructorArgsNames.exists(_.name == fieldAcc.idnuse.name) || declaredConstructorNames.exists("is" + _.name == fieldAcc.idnuse.name) => Seq() - case n: PNode => n.children collect {case ar: AnyRef => ar} + case n: PNode => n.children collect { case ar: AnyRef => ar } }).execute(input) transformStrategy(input) diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala index a7a792b8b..1392f79c3 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala @@ -24,7 +24,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager { * This is field holding the mappings of the adt constructors tag identifier. */ private val tagMapping: Map[String, Map[String, Int]] = (program.extensions collect { - case a:Adt => (a.name, a.constructors.map(_.name).sorted.zipWithIndex.toMap) + case a: Adt => (a.name, a.constructors.map(_.name).sorted.zipWithIndex.toMap) }).toMap /** @@ -37,8 +37,8 @@ class AdtEncoder(val program: Program) extends AdtNameManager { // In a first step encode all adt top level declarations and constructor calls var newProgram: Program = StrategyBuilder.Slim[Node]({ case p@Program(domains, fields, functions, predicates, methods, extensions) => - val remainingExtensions = extensions filter { case _:Adt => false; case _ => true } - val encodedAdtsAsDomains: Seq[Domain] = extensions collect { case a:Adt => encodeAdtAsDomain(a) } + val remainingExtensions = extensions filter { case _: Adt => false; case _ => true } + val encodedAdtsAsDomains: Seq[Domain] = extensions collect { case a: Adt => encodeAdtAsDomain(a) } Program(domains ++ encodedAdtsAsDomains, fields, functions, predicates, methods, remainingExtensions)(p.pos, p.info, p.errT) case aca: AdtConstructorApp => encodeAdtConstructorApp(aca) case ada: AdtDestructorApp => encodeAdtDestructorApp(ada) @@ -60,11 +60,11 @@ class AdtEncoder(val program: Program) extends AdtNameManager { /** * This method return the tag identifier given a adt constructor name and its correpsonding adt name * - * @param adtName The name of the adt + * @param adtName The name of the adt * @param contrName The name of the adt constructor we want the tag identifier * @return The queried tag identifier */ - private def getTag(adtName: String)(contrName:String) = tagMapping(adtName)(contrName) + private def getTag(adtName: String)(contrName: String) = tagMapping(adtName)(contrName) /** * This method takes an ADT and encodes it as a Domain. Especially it does @@ -86,7 +86,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager { (constructors flatMap generateDestructorDeclarations(domain)) ++ Seq(generateTagDeclaration(domain)) val axioms = (constructors flatMap generateInjectivityAxiom(domain)) ++ (constructors map generateTagAxiom(domain)) ++ Seq(generateExclusivityAxiom(domain)(constructors)) - val derivingAxioms = if (derivingInfo.contains(getContainsFunctionName)) + val derivingAxioms = if (derivingInfo.contains(getContainsFunctionName)) constructors filter (_.formalArgs.nonEmpty) map generateContainsAxiom(domain, derivingInfo(getContainsFunctionName)._2) else Seq.empty domain.copy(functions = functions, axioms = axioms ++ derivingAxioms)(adt.pos, adt.info, adt.errT) } @@ -96,29 +96,29 @@ class AdtEncoder(val program: Program) extends AdtNameManager { * This method creates a local variable given a type. One can specify the name of the local variable via the optional * argument 'name'. By default the name is 't'. * - * @param typ The type for which one wants to generate a local variable + * @param typ The type for which one wants to generate a local variable * @param name Optional argument specifying the name og the local variable * @return A local variable typed as 'typ' and with name 'name', if specified */ - private def localVarTFromType(typ:Type, name: Option[String] = None) = { + private def localVarTFromType(typ: Type, name: Option[String] = None) = { name match { - case Some(str) => LocalVar(str, typ)(_,_,_) - case None => LocalVar("t", typ)(_,_,_) + case Some(str) => LocalVar(str, typ)(_, _, _) + case None => LocalVar("t", typ)(_, _, _) } } /** - * This method creates a local variable declaration given a type. One can specify the name of the local variable via the optional - * argument 'name'. By default the name is 't'. + * This method creates a local variable declaration given a type. One can specify the name of the local variable + * via the optional argument 'name'. By default the name is 't'. * - * @param typ The type for which one wants to generate a local variable declaration + * @param typ The type for which one wants to generate a local variable declaration * @param name Optional argument specifying the name og the local variable declaration * @return A local variable declaration typed as 'typ' and with name 'name', if specified */ - private def localVarTDeclFromType(typ:Type, name: Option[String] = None) = { + private def localVarTDeclFromType(typ: Type, name: Option[String] = None) = { name match { - case Some(str) => LocalVarDecl(str, typ)(_,_,_) - case None => LocalVarDecl("t", typ)(_,_,_) + case Some(str) => LocalVarDecl(str, typ)(_, _, _) + case None => LocalVarDecl("t", typ)(_, _, _) } } @@ -126,12 +126,13 @@ class AdtEncoder(val program: Program) extends AdtNameManager { * This method encodes an ADT constructor as a domain function * * @param domain The domain the encoded constructor belongs to - * @param ac The ADT constructor to encode + * @param ac The ADT constructor to encode * @return An encoded ADT constructor as a domain function */ private def encodeAdtConstructorAsDomainFunc(domain: Domain)(ac: AdtConstructor): DomainFunc = { ac match { - case AdtConstructor(name, formalArgs) => DomainFunc(name, formalArgs, encodeAdtTypeAsDomainType(ac.typ))(ac.pos, ac.info, domain.name, ac.errT) + case AdtConstructor(name, formalArgs) => + DomainFunc(name, formalArgs, encodeAdtTypeAsDomainType(ac.typ))(ac.pos, ac.info, domain.name, ac.errT) } } @@ -154,15 +155,15 @@ class AdtEncoder(val program: Program) extends AdtNameManager { * This method generates destructor declarations for a corresponding ADT constructor * * @param domain the domain the encoded constructor belongs to - * @param ac the adt constructor for which we want to generate destructor declarations + * @param ac the adt constructor for which we want to generate destructor declarations * @return A sequence of destructor declarations, empty if constructor has no arguments */ - private def generateDestructorDeclarations(domain:Domain)(ac: AdtConstructor): Seq[DomainFunc] = { + private def generateDestructorDeclarations(domain: Domain)(ac: AdtConstructor): Seq[DomainFunc] = { assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.") ac.formalArgs.map { lv => val args = Seq(localVarTDeclFromType(encodeAdtTypeAsDomainType(ac.typ))(ac.pos, ac.info, ac.errT)) val ttyp = lv.typ match { - case a:AdtType => encodeAdtTypeAsDomainType(a) + case a: AdtType => encodeAdtTypeAsDomainType(a) case d => d } DomainFunc( @@ -212,14 +213,13 @@ class AdtEncoder(val program: Program) extends AdtNameManager { * * where C is the ADT constructor, D_i the destructor for i-th argument of C * - * * @param domain The domain the encoded constructor belongs to - * @param ac The adt constructor for which we want to generate the injectivity axioms + * @param ac The adt constructor for which we want to generate the injectivity axioms * @return A sequence of injectivity axiom */ private def generateInjectivityAxiom(domain: Domain)(ac: AdtConstructor): Seq[AnonymousDomainAxiom] = { assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.") - val localVarDecl = ac.formalArgs.collect {case l:LocalVarDecl => l } + val localVarDecl = ac.formalArgs.collect { case l: LocalVarDecl => l } val localVars = ac.formalArgs.map { lv => lv.typ match { case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(lv.name))(ac.pos, ac.info, ac.errT) @@ -258,7 +258,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager { * where D_ij is the destructor of the j-th argument of constructor C_i * * @param domain The domain the encoded ADT constructors belongs to - * @param acs The sequence adt constructor for which we want to generate the exclusivity axioms + * @param acs The sequence adt constructor for which we want to generate the exclusivity axioms * @return The exclusivity axiom */ private def generateExclusivityAxiom(domain: Domain)(acs: Seq[AdtConstructor]): AnonymousDomainAxiom = { @@ -291,11 +291,11 @@ class AdtEncoder(val program: Program) extends AdtNameManager { val equalities = rhss.map { rhs => EqCmp(localVar, rhs)(rhs.pos, rhs.info, rhs.errT) } - .foldLeft(FalseLit()(domain.pos, domain.info, domain.errT) : Exp)({ + .foldLeft(FalseLit()(domain.pos, domain.info, domain.errT): Exp)({ (acc, next) => Or(acc, next)(domain.pos, domain.info, domain.errT) - }) + }) - val triggers = (Seq(tagApp) ++ destructorCalls).map { t => Trigger(Seq(t))(domain.pos, domain.info, domain.errT)} + val triggers = (Seq(tagApp) ++ destructorCalls).map { t => Trigger(Seq(t))(domain.pos, domain.info, domain.errT) } AnonymousDomainAxiom( Forall(Seq(localVarDecl), triggers, equalities)(domain.pos, domain.info, domain.errT) @@ -326,13 +326,13 @@ class AdtEncoder(val program: Program) extends AdtNameManager { * where i is specified by the parameter 'tag'. * * @param domain The domain that encodes the ADT the constructor belongs to for which we want a tag axiom - * @param ac An ADT constructor + * @param ac An ADT constructor * @return The generated tag axiom */ - private def generateTagAxiom(domain:Domain)(ac: AdtConstructor): AnonymousDomainAxiom = { + private def generateTagAxiom(domain: Domain)(ac: AdtConstructor): AnonymousDomainAxiom = { assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.") - val localVarDecl = ac.formalArgs.collect {case l:LocalVarDecl => l } + val localVarDecl = ac.formalArgs.collect { case l: LocalVarDecl => l } val localVars = ac.formalArgs.map { lv => lv.typ match { case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(lv.name))(ac.pos, ac.info, ac.errT) @@ -372,7 +372,9 @@ class AdtEncoder(val program: Program) extends AdtNameManager { * * @return Return true if the contains function is derived for at least one adt */ - private def containsFunctionIsDerived: Boolean = program.extensions.exists { case a: Adt => a.derivingInfo.contains(getContainsFunctionName) } + private def containsFunctionIsDerived: Boolean = program.extensions.exists { + case a: Adt => a.derivingInfo.contains(getContainsFunctionName) + } /** * This method generates the corresponding contains axiom for a ADT constructor @@ -383,16 +385,16 @@ class AdtEncoder(val program: Program) extends AdtNameManager { * * where C′ = C(p_1, ..., p_n). * - * @param domain The domain that encodes the ADT the constructor belongs to for which we want a contains axiom + * @param domain The domain that encodes the ADT the constructor belongs to for which we want a contains axiom * @param blockList A list of destructor identifiers that should not be considered for the contains relations - * @param ac An ADT constructor + * @param ac An ADT constructor * @return The generated contains axiom */ private def generateContainsAxiom(domain: Domain, blockList: Set[String])(ac: AdtConstructor): AnonymousDomainAxiom = { assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.") assert(ac.formalArgs.nonEmpty, "AdtEncoder: An error in the ADT encoding occurred.") - val localVarDecl = ac.formalArgs.collect {case l:LocalVarDecl => l } + val localVarDecl = ac.formalArgs.collect { case l: LocalVarDecl => l } val localVars = ac.formalArgs.map { lv => lv.typ match { case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(lv.name))(ac.pos, ac.info, ac.errT) @@ -415,7 +417,11 @@ class AdtEncoder(val program: Program) extends AdtNameManager { Map(TypeVar("A") -> lv.typ, TypeVar("B") -> constructorApp.typ) )(ac.pos, ac.info, Bool, getContainsDomainName, ac.errT) - val axiomBody = localVars.filter(lv => !blockList.contains(lv.name)).map(containsApp).foldLeft[Exp](TrueLit()(ac.pos, ac.info, ac.errT))((a, b) => And(a, b)(ac.pos, ac.info, ac.errT)) + val axiomBody = localVars.filter(lv => + !blockList.contains(lv.name)) + .map(containsApp) + .foldLeft[Exp](TrueLit()(ac.pos, ac.info, ac.errT))((a, b) => And(a, b)(ac.pos, ac.info, ac.errT) + ) val forall = Forall(localVarDecl, Seq(trigger), axiomBody)(ac.pos, ac.info, ac.errT) AnonymousDomainAxiom(forall)(ac.pos, ac.info, ac.adtName, ac.errT) @@ -428,7 +434,6 @@ class AdtEncoder(val program: Program) extends AdtNameManager { * This ensures that we generate one axiom which encodes the transitivity of contains for each possible * triple of concrete types, which are used in calls to contains. * - * * @param program The program * @return The ContainsTransitivityDomain with axioms that encode transitivity */ @@ -490,10 +495,10 @@ class AdtEncoder(val program: Program) extends AdtNameManager { var triples: Set[(Type, Type, Type)] = Set.empty val closure = transitiveClosure(tuples) - for ((a,b) <- closure) { - for ((c,d) <- closure) { + for ((a, b) <- closure) { + for ((c, d) <- closure) { if (b == c) - triples += ((a,b,d)) + triples += ((a, b, d)) } } val axioms = triples.toSeq.map(a => genAxiom(a._1, a._2, a._3)) @@ -524,6 +529,8 @@ class AdtEncoder(val program: Program) extends AdtNameManager { /** Several helper methods */ private def encodeAdtTypeAsDomainType(adtType: AdtType): DomainType = DomainType(adtType.adtName, adtType.partialTypVarsMap)(adtType.typeParameters) - private def domainTypeFromDomain(domain:Domain): DomainType = DomainType(domain, defaultTypeVarsFromDomain(domain)) - private def defaultTypeVarsFromDomain(domain:Domain): Map[TypeVar, Type] = (domain.typVars zip domain.typVars).toMap + + private def domainTypeFromDomain(domain: Domain): DomainType = DomainType(domain, defaultTypeVarsFromDomain(domain)) + + private def defaultTypeVarsFromDomain(domain: Domain): Map[TypeVar, Type] = (domain.typVars zip domain.typVars).toMap } diff --git a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala index 7a9b84eb0..812ac11eb 100644 --- a/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala +++ b/src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtNameManager.scala @@ -12,7 +12,6 @@ import viper.silver.ast.Program import scala.collection.mutable - /** * A simple interface to transform/extend a program. * Contains utility functions to avoid name conflicts (e.g. when adding a new domain functions to a domain) @@ -39,13 +38,15 @@ trait AdtNameManager { * Note that the first two names are fixed by resources/adt/contains.vpr */ def getContainsDomainName: String = "ContainsDomain" + def getContainsFunctionName: String = "contains" + def getContainsTransitivityDomain: String = getName("ContainsTransitivityDomain") /** * This method returns the name of the destructor given the name of the ADT and the name of a constructor argument * - * @param adtName The name of the ADT the destructor belongs to + * @param adtName The name of the ADT the destructor belongs to * @param argument The name of a constructor argument for which we want the corresponding destructor * @return The name of the queried constructor */ @@ -74,17 +75,6 @@ trait AdtNameManager { adtNameMappings(trueName) } - - /** - * Checks if a name already occurs in the program. - * - * @param name to be checked - * @return true iff the name is used in the program. - */ - private def containsName(name: String): Boolean = { - usedNames.contains(name) - } - /** * Creates a unique name for the program and adds it to the names already used in the program. * @@ -102,4 +92,14 @@ trait AdtNameManager { newName } + /** + * Checks if a name already occurs in the program. + * + * @param name to be checked + * @return true iff the name is used in the program. + */ + private def containsName(name: String): Boolean = { + usedNames.contains(name) + } + }