Public interface of class 'TypeChecker'. More...
#include <TypeChecker.h>
Related Functions | |
(Note that these are not member functions.) | |
| SymbType_ptr | type_checker_check_expression (TypeChecker_ptr self, node_ptr expression, node_ptr context) |
| Perform type checking of an expression, and returns its type. | |
| void | type_checker_enable_memoizing (TypeChecker_ptr self, boolean enabled) |
| Enables or disables internal type memoizing. | |
| boolean | type_checker_is_memoizing_enabled (const TypeChecker_ptr self) |
| Returns true if memoizing is currently enabled, false otherwise. | |
| void | type_checker_print_error_message (TypeChecker_ptr self, node_ptr expr, boolean is_error) |
| Prints whther an error or a warning message, depending on the given parameter. | |
| boolean | TypeChecker_check_constrains (TypeChecker_ptr self, node_ptr init, node_ptr trans, node_ptr invar, node_ptr assign, node_ptr justice, node_ptr compassion) |
| Checks all the module contrains are correctly typed. | |
| boolean | TypeChecker_check_layer (TypeChecker_ptr self, SymbLayer_ptr layer) |
| Checks that the types of variable decalarations in the layer are correctly formed. Also defines are checked to have some well-formed type. | |
| boolean | TypeChecker_check_property (TypeChecker_ptr self, struct Prop_TAG *property) |
| Checks that the expression constituting the property is correctly typed. | |
| boolean | TypeChecker_check_symb_table (TypeChecker_ptr self) |
| Calls TypeChecker_check_layer over all the layers of the symbol table of self. | |
| TypeChecker_ptr | TypeChecker_create (struct SymbTable_TAG *symbolTable) |
| TypeChecker class constructor. | |
| TypeChecker_ptr | TypeChecker_create_with_default_checkers (struct SymbTable_TAG *symbolTable) |
| TypeChecker class constructor, with registration of a set of default of checkers. | |
| void | TypeChecker_destroy (TypeChecker_ptr self) |
| The TypeChecker class destructor. | |
| SymbType_ptr | TypeChecker_get_expression_type (TypeChecker_ptr self, node_ptr expression, node_ptr context) |
| Returns the type of an expression. | |
| struct SymbTable_TAG * | TypeChecker_get_symb_table (TypeChecker_ptr self) |
| Returns the symbol table this type checker is associated to. | |
| boolean | TypeChecker_is_expression_type_checked (TypeChecker_ptr self, node_ptr expression, node_ptr context) |
| Returns true iff a given expression has been type checked. | |
| boolean | TypeChecker_is_expression_wellformed (TypeChecker_ptr self, node_ptr expression, node_ptr context) |
| The method type checks an expression and returns true if an expression is wellformed with respect to the type system and false otherwise. | |
| boolean | TypeChecker_is_specification_wellformed (TypeChecker_ptr self, node_ptr expression) |
| Performs type checking of a specification. | |
| boolean | TypeChecker_is_type_wellformed (TypeChecker_ptr self, SymbType_ptr type, node_ptr varName) |
| Checks that a type is well formed. | |
Public interface of class 'TypeChecker'.
Definition of the public type for class TypeChecker
| SymbType_ptr type_checker_check_expression | ( | TypeChecker_ptr | self, | |
| node_ptr | expression, | |||
| node_ptr | context | |||
| ) | [related] |
Perform type checking of an expression, and returns its type.
This function is the core of the expression type checking.
The expression may by unmodified (after compilation), flattened or flattened+expanded.
The return value is the type of the expression. If an expression violates the type system, the violation handler function is invoked and "error" type is returned (not NULL).
NB: As it is said in TypeChecker.h, the expression type checking package uses only memory-shared types (SymbTablePkg_..._type).
NB: This function does not perform the type checking on already checked expressions (even if they were erroneous), but just returns their types (possibly error-type). This avoids multiple error and warning messages for the same subexpression.
| void type_checker_enable_memoizing | ( | TypeChecker_ptr | self, | |
| boolean | enabled | |||
| ) | [related] |
Enables or disables internal type memoizing.
This method is used by checkers to temporary disable internal type memoizing that associates each sub-expression to its type. This can be used to force an already checked formula to be re-checked. For example the PSL checker while checking 'forall' expressions requires the repeated formula to be checked as many times as the id has a range of possible values.
Important: memoizing is enabled by default and re-enabled every time the user calls the top level checking method. However, it is good behaviour for checkers to re-enable memoizing after disabling it
| boolean type_checker_is_memoizing_enabled | ( | const TypeChecker_ptr | self | ) | [related] |
Returns true if memoizing is currently enabled, false otherwise.
| void type_checker_print_error_message | ( | TypeChecker_ptr | self, | |
| node_ptr | expr, | |||
| boolean | is_error | |||
| ) | [related] |
Prints whther an error or a warning message, depending on the given parameter.
This private funciont is called by violation handler into checkers and self, to print a uniform message when type errors and warnings occur
| boolean TypeChecker_check_constrains | ( | TypeChecker_ptr | self, | |
| node_ptr | init, | |||
| node_ptr | trans, | |||
| node_ptr | invar, | |||
| node_ptr | assign, | |||
| node_ptr | justice, | |||
| node_ptr | compassion | |||
| ) | [related] |
Checks all the module contrains are correctly typed.
The module contrains are declarations INIT, INVAR, TRANS, ASSIGN, JUSTICE, COMPASSION.
The first parameter 'checker' is a type checker to perfrom checking. All the remaining parameters are the sets of expressions constituting the bodies of the corresponding high-level declarations. These expressions are created during compilation and then passed to this function unmodified, flattened or flattened+expanded. So this function is relatively specialised to deal with concrete data-structures created during compilation. For example, the expressions in the given sets are expected to be separated by CONS and AND.
NOTE: if an expression has been flattened, then info about line numbers mat not be accurate.
The type checker remebers all the checked expressions and their types, thus TypeChecker_get_expression_type uses memoizing to return the type of already checked expressions.
The parameter 'assign' is actually the 'procs' returned by Compile_FlattenHierarchy, which contains all the assignments.
If some of expressions violates the type system, the type checker's violation handler is invoked. See checkers into the checkers sub-package for more info.
Returns false if the module contrains violate the type system, and otherwise true is returned.
| boolean TypeChecker_check_layer | ( | TypeChecker_ptr | self, | |
| SymbLayer_ptr | layer | |||
| ) | [related] |
Checks that the types of variable decalarations in the layer are correctly formed. Also defines are checked to have some well-formed type.
Constrain: the input layer should belong to the symbol table the type checker is associated with.
The function iterates over all variables in the layer, and checks their type with function TypeChecker_is_type_wellformed.
The function also type checks the expressions provided in defines (also the generated "running" defines) have some type. NB for developers: This is done to allow the type checker to remember the type of these defines (and associated constants and variable _process_selector_). Without this list the evaluation phase will not know the type of these defines (if there were not explicitly used in the input text), since they can be implicitly used in ASSIGN(TRANS) contrains.
Returns true if all the types are correctly formed and the defines are correct, false otherwise.
| boolean TypeChecker_check_property | ( | TypeChecker_ptr | self, | |
| struct Prop_TAG * | property | |||
| ) | [related] |
Checks that the expression constituting the property is correctly typed.
If some of expressions violates the type system, the type checker's violation handler is invoked. See checkers into the checkers sub-package for more info.
The type checker remebers all the checked expressions and their types, thus TypeChecker_get_expression_type uses memoizing to return the type of already checked expressions.
If the property violates the type system, the false value is return, and true value otherwise.
| boolean TypeChecker_check_symb_table | ( | TypeChecker_ptr | self | ) | [related] |
Calls TypeChecker_check_layer over all the layers of the symbol table of self.
| TypeChecker_ptr TypeChecker_create | ( | struct SymbTable_TAG * | symbolTable | ) | [related] |
TypeChecker class constructor.
AutomaticStart
TypeChecker class constructor. The 'symbolTable' is a symbol table to look for the type of found identifiers
| TypeChecker_ptr TypeChecker_create_with_default_checkers | ( | struct SymbTable_TAG * | symbolTable | ) | [related] |
TypeChecker class constructor, with registration of a set of default of checkers.
TypeChecker class constructor, with registration of a set of default of checkers. The 'symbolTable' is a symbol table to look for the type of found identifiers
| void TypeChecker_destroy | ( | TypeChecker_ptr | self | ) | [related] |
| SymbType_ptr TypeChecker_get_expression_type | ( | TypeChecker_ptr | self, | |
| node_ptr | expression, | |||
| node_ptr | context | |||
| ) | [related] |
Returns the type of an expression.
If the expression has been already type-checked by the same type-checker, then the type of an expression is returned. Otherwise, the expression is type checked and its type is returned.
The parameter 'context' indicates the context where expression has been checked. It should be exactly the same as during type checking. For outside user this parameter is usually Nil. NOTE: The returned type may be error-type indicating that the expression violates the type system. NOTE: all returned types are the memory-sharing types (see SymbTablePkg_..._type). So you can compare pointers instead of the type's contents.
TypeChecker_is_expression_wellformed, TypeChecker_is_specification_wellformed
| struct SymbTable_TAG * TypeChecker_get_symb_table | ( | TypeChecker_ptr | self | ) | [related] |
Returns the symbol table this type checker is associated to.
During its lifetime every type checker can deal only with one symbol table instance (because type checker caches the checked expressions and their types). The symbol table is given to the type checker during construction, and this function returns this symbol table.
| boolean TypeChecker_is_expression_type_checked | ( | TypeChecker_ptr | self, | |
| node_ptr | expression, | |||
| node_ptr | context | |||
| ) | [related] |
Returns true iff a given expression has been type checked.
If this function returns true then TypeChecker_get_expression_type will return the cached type without performing the actual type checking.
The parameter 'context' indicates the context where expression has been checked. It should be exactly the same as during type checking. For outside user this parameter is usually Nil.
| boolean TypeChecker_is_expression_wellformed | ( | TypeChecker_ptr | self, | |
| node_ptr | expression, | |||
| node_ptr | context | |||
| ) | [related] |
The method type checks an expression and returns true if an expression is wellformed with respect to the type system and false otherwise.
The main purpose of this function is to be invoked on temporarily created expressions before they are evaluated to ADD or BDD. This function may not be useful for expressions read from files (such as bodies of INVAR, SPEC, etc) since they go through flattening in the compilation package and type-checked there.
NOTE: an expression may be unmodified (after parsing and compilation), flattened or flattened+expanded. The expressions and their types are remembered by the type checker and the expressions types can be obtained with TypeChecker_get_expression_type.
NOTE: memoizing is enabled before checking the expression.
See checkers into the checkers sub-package for more info.
| boolean TypeChecker_is_specification_wellformed | ( | TypeChecker_ptr | self, | |
| node_ptr | expression | |||
| ) | [related] |
Performs type checking of a specification.
A specification is a usual (i.e. able to have a type) expression wrapped into a node with a specification tag such as INIT, INVAR, SPEC, COMPASSION, etc. There are two special case: ASSIGN can contains a list of EQDEF statements, and COMPUTE can contains MIN and MAX statement.
The returned value is true if no violations of the type system are detected, and false otherwise.
NOTE: the expression may be unmodified (after compilation), flattened or flattened+expanded. The expressions and their types are remembered by the type checker and the expressions types can be obtained with TypeChecker_get_expression_type.
NOTE: memizing is enbaled before checking the specification
See checkers into the checkers sub-package for more info.
| boolean TypeChecker_is_type_wellformed | ( | TypeChecker_ptr | self, | |
| SymbType_ptr | type, | |||
| node_ptr | varName | |||
| ) | [related] |
Checks that a type is well formed.
This function is used to check the well-formedness of a type from a symbol table. This type should have properly created body, in particular, bodies should have correct line info.
The constrains on a type are: 1. word type: the width should be a NUMBER and have positive value. The width should not be greater than implemenetation limit WordNumber_max_width() bit (since we do not use arbitrary-precision arithmetic and ADD structores will be too big otherwise) 2. enum type: there should be no duplicate values.
The third parameter is the variable name that type is to be checked. The variable name is used just to output proper message in the case of a type violation.
In the case of a type violation the violation handler obtain an expression CONS with variable name as left child and the body of the type as the right child.
1.6.1
