Adding Support for User Defined Datatypes and Logical Functions

[shiva-tk]

Example of the type of specifications that these new features allow for can be found in wisl/examples/SLL_adt.wisl.

User Defined Datatypes

Added WISL support for user defined datatypes:

• Updated parser
• Extended AST
• Updated compiler

Added support for user defined datatypes in core Gillian:

• Created a Datatype_env to hold definitions
• Extended AST to allow application of datatype constructors within GIL expressions
• Extended AST to allow matching of expressions with datatype constructors
• Extended typing algorithm to handle expressions involving constructor application / case matching
• Extended matching plans to allow bindings to be learnt from equalities involiving constructor applications
• Added reductions of expressions involving constructor applications
• Implemented encoding into SMT

User Defined Functions

Added WISL support for user defined functions:

• Updated parser
• Extended AST
• Updated compiler

Added support for user defined functions in core Gillian:

• Created a Function_env to hold definitions
• Extended AST to allow application of functions within GIL expressions
• Extended typing algorithm to handle expressions involving function application
• Implemented encoding into SMT

Notes

General

• Constructor applications in WISL are prefixed by a quote mark ' to differentiate it from function application in the parsing. This was mainly a quick fix, and I'm happy to take suggestions on other approaches!
• Similarly, pure function denotes a logical function used in specifications, whereas function represents a procedure.
• Moved smt.ml into engine/FOLogic/ in order to avoid circular dependencies: smt.ml requires Datatype_env, from the engine module, but engine requires smt.ml.
• Datatype_env and Function_env are mutable global references. This is for a couple of reasons. Firstly, unlike the typing environment, they aren't modified or copied or replaced during symbolic execution. They are initialised once and stay constant throughout. Secondly, it is too much of a pain to refactor every occurence of gamma to also carry around a Datatype_env and a Function_env. There are some functions which even make gamma optional, however, the other two environments are always a necessity! I did try this approach but it proved to be too much work.
• Unsure of how to handle compilation of wisl pointer arithmetic in the body of pure functions. Have just compiled as plain addition / subtraction for now. Could introduce if then else expressions, and then these pointer arithmetic operations would be expressible as a GIL Expression.

SMT Encoding

• The initial declarations are dependent on the datatypes and functions declared, so initialisation is now delayed until the first query is given to the solver. At this point, the Datatype_env and Function_env are assumed to be initialised.
• Added extra assertions when applying a destructor to an SMT-LIB ADT: In SMT-LIB, if you apply a destructor of a datatype to a value not constructed by the corresponding constructor, the behavior is generally unspecified. This lead to some queries returning sat when they should have been unsat. As a result, we add additional assertions to ensure that expressions were in-fact constructed by the constructor corresponding to the destructor.

[AndreasLoow]

Repeating here what I said in Discord:

Constructor applications in WISL are prefixed by a quote mark ' to differentiate it from function application in the parsing. This was mainly a quick fix, and I'm happy to take suggestions on other approaches!

I think this should be fixed before merge.