Add support for ADTs in Viper #574
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-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
-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
…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
-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
-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
-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.
… 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
-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
-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
-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.
-Implement the translation for PAdtType to AdtType -Adjust translation flow to respect changes of the plugin infrastructure
-Implement a much simpler solution for withChildren
-Since both classes have a special second argument list, we need to handle them correctly
-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.
-Make use of the fact that all nodes are Rewritable's, so we can traverse the entire tree using a StrategyBuilder
-Add functionality to encode ADT declarations, constructors and types
-Use the AdtEncoder to encode ADT related AST nodes to normal AST nodes before the AST is passed to the verifier
-Implement first version of type checking for ADT operation applications
-Additionally we add a companion object s.t the return type is set correctly
-Additionally, missing methods of AdtType are implemented
- Contains utility to avoid name conflicts when adding tag function declarations and destructor function declarations.
-This includes adding injectivity and exclusivity axioms, adding an encoding for destructors and a tag function for discrimination
-Disallow duplicate argument identifiers of constructors, otherwise we destructors can not be distinguished with the current design of ADT's
…t-extension # Conflicts: # src/main/scala/viper/silver/parser/Translator.scala
…d-adt-past-extension
# Conflicts: # src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala
-Refactor PConstructorCall for potential code reuse
-Additionally provide companion object to correctly set the destructor application given the name and the corresponding ADT.
-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
-Additionally add a getTag function that maps adt constructor's to its tag identifier
-Implement the type-checking for discriminator calls -Implement the translation to an AST node for discriminator calls
-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)
-There was a bug that a new mapping for a name is added, despite already having a mapping for that name
-There might happen that 'name' corresponds to an identifier of a method, function, etc. which caused an exception.
-Only allow PFormalArgDecl's as PAdtConstructor arguments -Only allow LocalVarDecl's as AdtConstructor arguments
-Add the possibility to disable ADT plugin
Add adt extension
-In commit f55e455dac752fb47ddfa98504ae91bdc199e1e thee ADT plugin was added to the default plugins, hence the number of defualt plugins is now 3.
Aurel300
reviewed
Apr 26, 2022
| @@ -111,6 +111,13 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str | |||
| hidden = true | |||
| ) | |||
|
|
|||
| val adtPlugin = opt[Boolean]("disableAdtPlugin", | |||
There was a problem hiding this comment.
I know this is the same as the termination plugin above, but shouldn't this rather be enableAdtPlugin, true by default?
There was a problem hiding this comment.
@Aurel300 I don't have a strong opinion here. If you have, please bring it up in a Viper meeting. Or simply change the implementation when nobody is looking ;-)
There was a problem hiding this comment.
Imo, the bigger issue with disabling default plugins is that they are actually still loaded. Disabling of the plugin's functionality happens by returning from the hooks without doing anything. I adopted this from the termination plugin, personally I don't like this solution. :)
Comment on lines
+278
to
+281
| override def verifyExtExp(): VerificationResult = { | ||
| assert(assertion = false, "AdtDiscriminatorApp: verifyExtExp has not been implemented.") | ||
| Failure(Seq(ConsistencyError("AdtDiscriminatorApp: verifyExtExp has not been implemented.", pos))) | ||
| } |
There was a problem hiding this comment.
No, verifyExtExp() is a method provided by the plugin infrastructure, but actually never used anywhere. If, this method will be used/called in future, the error should happen, since it should not be necessary to call it for new expression added with the ADT plugin.
@amaissen Please fix, if still possible.
@Aurel300 Yes, when the plugin is in use. The syntax has been ran by Peter.
@Aurel300 The deriving system is a proof of concept, and likely to change. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds support for basic use of ADTs in Viper via a Viper plugin.