Extensibility of MAF

[bramvdbogaerde]

We might want to split this issue into multiple different issues, but I hope to give an overview of the ways in which one might want to extend MAF.

• Annotated values: both in the incremental and scv analyses the values returned from "eval" in the big step semantics are annotated with additional information. In the case of the incremental analysis with information about the flows, in case of scv with symbolic information of the value. Currently, a workaround is required to add this additional information to the values: (a) creating a special lattice that annotates the value elements with additional information or (b) extending the monad such that it can implicitly return the annotations
• Extending the target language: in MAF we have multiple "languages": CScheme, ContractScheme, ... currently they need to be in the same hierarchy as the base Scheme language, and even in the same file (as we like to keep SchemeExp sealed). This comes down somewhat to the well-known expression problem.
• Extending the abstract domain with additional values: it seems rather difficult at the moment to introduce additional abstract values into the scheme lattice. Additionally, these values need to be introduced in the SchemeLattice and therefore need to be implemented for particular abstract domains and analyses for which they might not even make much sense.
• Changing the exploration semantics of the intra-analysis: One analysis might want to join after an if expression, another might want to keep them as separate states that need to be explored further. Currently, the big step semantics somewhat accommodate for this by defining the semantics in a monadic style. Changing the behaviour of the intra-analysis therefore often comes down to changing the monad. However, a more generic set of monads might be introduced so that the burden of implementing a compatible monad with only slightly different semantics is lessened.

[noahvanes]

We'll definitely need to split this :-)

Bullets 1 & 3 are also related to previous issues tagged with "Abstract Domain" (e.g., #24, #22, ...), so we might want to take all of those into account when we start refactoring the implementation of these abstract domains.

Not sure what bullet 4 is about. The flexibility (e.g., for the given example with if-expressions) is already enabled by the monadic style. Does this boil down then to having more monad transformers to make it easier to construct those monads?