# PR 114

In this document, we detail the features and bugfixes contained in PR #114. Each section contains a description of the feature, a list of the code files changed (test files are not included), and a justification for the changes.

## Feature 1: Importing Functions from Other Modules

### Description
Using a statement of the form `function * = <mod>.*;`, a user can import all of the uninterpreted functions from the module `<mod>`. The ModuleFunctionsImportRewriter will collect all of the function declarations in the `<mod>` module and rewrite all functions with the same name in the caller module. For example, suppose `fun1` is defined in `<mod>` and the caller module calls `fun1`. The call to `fun1` in the caller module is rewritten to the form `<mod>.fun1`. With this method, we ensure that `fun1` is interpreted in the same way across all modules.

This feature is introduced for the sake of user convenience. Prior to this feature, a user would have either to copy function declarations into every module or manually reference externally defined functions in the following form `<mod>.<fun>`. This is espescially inconvenient for large models on the scale of Keystone.

Note that this import statement does not allow shadowing. Suppose we have a module `mod1` that contains an uninterpreted function `fun1` and another module `mod2` that declares a function with the same name, despite being a different signature. If `mod2` contains the statement `function * = mod1.*;`, we will throw an error.

### Changed Files
* UclidMain.scala
* UclidParser.scala (previous branch; already merged to master)
* UclidLanguage.scala
* ASTVisitors.scala (previous branch; already merged to master)
* ModuleCleaner.scala (previous branch; already merged to master)
* ModuleFunctionsImportRewriter.scala
* Scope.scala (pervious branch; already merged to master)
* PassManager.scala
* ParserSpec.scala (For tests)

### Justifications
* **UclidMain.scala**: Changed order of passes for correctness.
* ModuleFunctionsImportRewriter.scala: Rewrote this pass to rewrite imports in the form `<mod>.<fun>` rather than explicitly copying them into the module.
* **PassManager.scala**: Added individual modules to `moduleList` during single invocations of the `run` function. The `moduleList` contains the unmodified modules which is necessary to compute the import dependencies; this is primarily because the full set of compile passes are run on a module before compiling the next one, which results in the import statements being lost.
* **UclidLanguage.scala**: Computing instance type using `moduleType` vs `modTyp`; the former is more graceful (doesn't lead to a None.get if the instance type is None).

## Feature 2: Importing Constants from Other Modules

### Description

Using a statement of the form `const * = <mod>.*;`, a user can import all of the constant literals and uninterpreted constants from the module `<mod>`. The ModuleConstantsImportRewriter will collect all of the constant declarations in the `<mod>` module and rewrite all constants with the same name in the caller module. For example, suppose `const1` is defined in `<mod>` and the caller module uses `const1`. The reference to `const1` in the caller module is rewritten to the form `<mod>.const1`. With this method, we ensure that `const1` is interpreted in the same way across all modules.

This feature is introduced for the sake of user convenience. Prior to this feature, a user would have either to copy constant declarations into every module or manually reference externally defined constants in the following form `<mod>.<constant>`. This is espescially inconvenient for large models on the scale of Keystone.

Note that this import statement does not allow shadowing. Suppose we have a module `mod1` that contains a constant `const1` and another module `mod2` that declares a constant with the same name, despite being a different signature. If `mod2` contains the statement `const * = mod1.*;`, we will throw an error.

### Changed Files

* UclidMain.scala
* UclidParser.scala (previous branch; already merged to master)
* UclidLanguage.scala
* ASTVisitors.scala (previous branch; already merged to master)
* ModuleCleaner.scala (previous branch; already merged to master)
* ModuleConstantsImportRewriter.scala
* Scope.scala (previous branch; already merged to master)
* PassManager.scala
* ParserSpec.scala (For tests)
* VerifierSpec.scala (For tests)

### Justifications
* **UclidMain.scala**: Changed order of passes for correctness.
* **ModuleConstantsImportRewriter.scala**: Rewrote this pass to rewrite imports in the form `<mod>.<const>` rather than explicitly copying them into the module.
* **PassManager.scala**: Added individual modules to `moduleList` during single invocations of the `run` function. The `moduleList` contains the unmodified modules which is necessary to compute the import dependencies; this is primarily because the full set of compile passes are run on a module before compiling the next one, which results in the import statements being lost.
* **UclidLanguage.scala**: Computing instance type using `moduleType` vs `modTyp`; the former is more graceful (doesn't lead to a None.get if the instance type is None).

## Feature 3: Importing Define Macros from Other Modules

### Description

Using a statement of the form `define * = <mod>.*;`, a user can import all of the define macros from the module `<mod>`. The ModuleDefinesImportCollector will collect all of the define macros in the `<mod>` module and explicitly write them into the caller module. Note that this implementation differs from the last two features in that instead of rewriting the names, we copy the declarations into this module. This acceptable because `define` macros are always inlined whenever they are called. Furthermore, this pass is scheduled before the ModuleConstantsImportRewriterPass and the ModuleFunctionsImportRewriterPass, which allows the passes to rewrite any constants or functions in the `define` declarations that were copied over.

This feature is introduced for the sake of user convenience. Prior to this feature, a user would have either to copy `define` macros into every module, with no option of referencing them externally. This is espescially inconvenient for large models on the scale of Keystone.

Note that the redeclaration check is handled by the SemanticAnalyzer pass, since `define` declarations are explictly brought in. Furthermore, only `define` declarations that do not refer to state variables are imported into the caller module.

### Changed Files

* UclidMain.scala
* UclidParser.scala
* UclidLanguage.scala
* ASTVisitors.scala
* ModuleCleaner.scala
* ModuleDefinesImportCollector.scala
* Scope.scala
* PassManager.scala
* ParserSpec.scala (For tests)
* VerifierSpec.scala (For tests)

### Justifications
* **UclidMain.scala**: Changed order of passes for correctness.
* **ModuleFunctionsImportRewriter.scala**: Rewrote this pass to rewrite imports in the form `<mod>.<fun>` rather than explicitly copying them into the module.
* **PassManager.scala**: Added individual modules to `moduleList` during single invocations of the `run` function. The `moduleList` contains the unmodified modules which is necessary to compute the import dependencies; this is primarily because the full set of compile passes are run on a module before compiling the next one, which results in the import statements being lost.
* The other files were changed primarily to support the added language feature.

## Feature 4: Instance Procedure Calls

### Description
Procedure calls in UCLID5 are augmented with the capability to invoke procedures local to a modules instance, thereby changing the state of the instance. The convention is as follows: `call (<bound_vars>) = <inst_name>.<procedure_name>(<params>);`. This was introduced to allow the user to naturally invoke the behavior of submodules while also enabling Floyd-Hoare style program verification for modules that interact with their instances. This was a very natural extension for Keystone and is essential to describing our models in a modular fashion.

This feature was essentially implemented by extending the `ProcedureCallStmt` to include an additional argument denoting the instance. The changes for this feature are primarily centered around fitting this additional argument into the existing code base.

### Changed Files
* PrimedVariableEliminator.scala
* SymbolicSimulator.scala
* UclidMain.scala
* ModuleCleaner.scala
* ModuleFlattener.scala
* ModuleTypeChecker.scala
* ProcedureChecker.scala
* ProcedureInliner.scala
* StatementScheduler.scala
* UclidLanguage.scala
* UclidParser.scala
* VerifierSpec.scala (For tests)
* ModularProductProgram.scala
* PrimedAssignmentChecker.scala

### Justification
* **SymbolicSiluator.scala**: Needed to add additional arguments to ProcedureCallStmt to match the new definition.
* **UclidMain.scala**: Added NewInternalProcedureInlinerPass which performs the first round of inlining.
* **ASTVisitors.scala**: Augmented visits for new definition of ProcedureCallStmt
* ModularProductProgram.scala: Made compatible with new definition of ProcedureCallStmt
* **ModuleCleaner.scala**: The `rewriteProcedure` was removed since it may remove 'noinlined' instance procedure calls that we want to save for later passes. (**Point of Discussion** (Pramod): If we didn't clean until after flattening, we can keep rewrite procedure and also solve the problem with storing the moduleList over multiple passes.)
* **ModuleTypeChecker.scala**: Needed to extend typechecker to look for instance procedures, which requires searching a separate context.
* **PrimedAssignmentChecker.scala**: Made compatible with new definition of ProcedureCallStatement
* **PrimedVariableEliminator.scala**: The `applyOnProcedureCall` was removed since, at this point, only no-inlined instance procedure calls remain in the module and we do not compute their modifies set until later passes. (**Point of Discussion** (Kevin): Check on this reason.)
* **ProcedureChecker.scala**: Needed to check for instance ids in a modifies block of a procedure declaration and check the identifiers for instance procedure calls.
* **ProcedureInliner.scala**: Needed to handle regular procedure calls and 'inlined' instance procedure calls; 'noinlined' instance procedure calls are pushed to the ModuleFlattener pass. See code for comments. (**Point of Discussion** (Pramod): We should consider moving this before the WhileLoopRewriter and ForLoopUnroller passes since an inlined instance procedure call may have loops.)
* **ModuleFlattener.scala**: Needed to handle 'no-inlined' instance procedure calls. See code for comments.
* **StatementScheduler.scala**: Made compatible with the new definition of ProcedureCallStmt. Note that it does not handle instance procedure calls since they have not been processed yet.
* **UclidLanguage.scala**: Augmented definition of ProcedureCallStatement to include instance ids. Annotated statements that may contain procedure calls with `hasInternalCall`; this is mainly to track calls for inlining. Added code for better internal representation of instances and modules.
* **UclidParser.scala**: Needed for user facing language feature.

## Feature 5: Automatic Detection of Modified Instance Variables

### Description

The extension for instance procedure calls brought forth an important issue: how would a user describe which state variables of the instance were modified (within a procedure that makes an instance procedure call). This is espescially important when we 'no-inline' an instance procedure call and need to havoc some of the instance variables. To reduce burden on the user and avoid breaking modular abstraction, we require the user to specify `modifies <inst>;` and find the appropriate state variables through a series of passes.

To enable this feature, we extend the concept of a `ModifiableEntity` and `HavocableEntity` to instance state variables; it is worth noting that this language extension is only available to the internal AST passes. The changes for the feature are primarily centered around tracking instance state variables and fitting this language extension into the existing code base.

### Changed Files
* SymbolicSimulator.scala
* UclidMain.scala
* ASTVisitorUtils.scala
* ASTVisitors.scala
* ModuleFlattener.scala
* ModuleTypeChecker.scala
* ProcedureChecker.scala
* ProcedureInliner.scala
* ProcedureModifiesRewriter.scala
* StatementScheduler.scala
* TaintPass.scala
* UclidLanguage.scala
* UclidParser.scala
* ModularProductProgram.scala
* WhileLoopRewriter.scala

### Justification
* **SymbolicSimulator.scala**: Needed to add case match for HavocableInstanceId
* **UclidMain.scala**: Added the ProcedureModifiesRewriter pass to write in ModifiableInstance Ids
* **ASTVisitorUtils.scala**: Extended the bug fix for the `old` operator to handle ModifiableEntities; this enables using `old` on instance state variables.
* **ASTVisitors.scala**: Added visits for ModifiableEntities in procedure declarations and HavocableInstanceIds in havoc statements; this is needed for full AST traversal
* **ModularProductProgram.scala**: Added support for ModifiableEntities; need for module variables
* **ModuleTypeChecker.scala**: Needed to add case for HavocableInstanceIds.
* **ProcedureChecker.scala**: Made compatible with ModifiableInstanceIds and HavocableInstanceIds.
* **ProcedureInliner.scala**: Added compatibility with ModifiableInstanceIds.
* **ProcedureModifiesRewriter.scala**: Needed to compute the 'modifies' set while tracking specific instance variables. See code for documentation.
* **StatementScheduler.scala**: Added compatibility with HavocableInstanceIds.
* **TaintPass.scala**: Added compatibility with HavocableInstanceIds.
* **UclidLanguage.scala**: Needed to define the internal representation for ModifiableInstanceIds and HavocableInstanceIds.
* **UclidParser.scala**: Needed to make `modifies` expression compatible with ModifiableEntities; not externally facing.
* **WhileLoopRewriter.scala**: Added compatibility with HavocableInstanceIds.

## Bugfix 1: Intermediate Variables for the `old` Operator

### Description

The `old` operator is a user-facing feature of the language that allows users to refer to the 'old' values of a variable; this can be used within the body of the procedure or within the pre- and post-conditions of a procedure. However, if we 'no-inline' a procedure call, the pre- and post-conditions of the callee procedure are brought into the body of the caller procedure. Any invocations of the `old` operator in the pre- and post-conditions then refer to the values of the variable before the execution of the caller procedure rather than before the execution of the callee procedure.

To fix this issue, we introduce dummy variables before every procedure call; the dummy variables store the values of the state variables that the procedure modifies. These values then replace the 'old' values within the pre- and post-conditions. While this does introduce overhead in terms of the total number of variables and model size, this can be addressed by enforcing Static Single Assignment in UCLID5 and then performing Dead Code Elimination; it is also worth noting that there has been interest in implementing this.

### Changed Files
* ASTVisitorUtils.scala
* ProcedureInliner.scala
* ModuleFlattener.scala
* TypeChecker.scala
* UclidLanguage.scala
* VerifierSpec.scala

### Justification
* **ASTVisitorUtils.scala**: Prevent our various rewrite passes from implicitly modifying any uses of the `old` operator.
* **ProcedureInliner.scala**: Needed to handle generation of dummy variables and rewrites of `old` operators depending on whether or not a procedure is 'inlined' or not.
* **TypeChecker.scala**: Augmented typechecking for the old operator to allow for polymorphic selects.
* **UclidLanguage.scala**: Needed to add support for old instance variables.