compile.h
External header file
compileInt.h
Internal header file
compileBEval.c
compileCheck.c
Performs semantic checks on the model.
compileCmd.c
Shell interface for the compile package.
compileCone.c
Computes the cone of influence of the model variables.
compileFlatten.c
Flattening of the model.
compileStruct.c
Structure used to store compilation results.
compileUtil.c
Routines for model computation.
compileWrite.c
Creation of an SMV file containing the flattened or booleanized model.
compileWriteUdg.c
Creation of a UDG file containing the flattened or booleanized model.

compile.h

External header file

By: Marco Roveri, Emanuele Olivetti

()
The name of the standard layer dedicated to model symbols

compileInt.h

Internal header file

By: Marco Roveri, Roberto Cavada


compileBEval.c

By: Alessandro Cimatti and Marco Roveri

Conversion from scalar expressions to boolean expressions.

See Alsooptional

Compile_expr2bexpr()
Converts a scalar expression into a boolean expression.
Compile_detexpr2bexpr()
Converts a scalar expression into a boolean expression.
Compile_detexpr2bexpr_list()
Converts a scalar expression into a boolean expression.
Compile_is_expr_booleanizable()
Check if an expr is of a finite range type
Compile_cleanup_booleanizer_cache_about()
Cleans those hashed entries that are about a symbol that is being removed
expr2bexpr_shift_left()
Creates the encoding of the left-shifting circuit for words
expr2bexpr_shift_right()
Creates the encoding of the unsigned right-shifting circuit for words
expr2bexpr_get_shift_def_value()
Private service for shifting operations
expr2bexpr_shift()
High-level function for shifting operations
expr2bexpr_rotate()
High-level function for rotating words
expr2bexpr_recur_unary()
This function booleanize an unary expression in a standard way: at first process the argument. Then for words apply a corresponding unary word function, for all other type just create exp of the same kind with find_node.
expr2bexpr_recur_binary()
This function booleanize a binary expression in a standard way.
expr2bexpr_ite()
Creates an encoding for CASE node. If CASE evaluates to a word, a WORD encoding is created.
expr2bexpr_word_ite_aux()
Service of expr2bexpr_word_ite, that creates the word encoding
expr2bexpr_recur()
Converts a generic expression into a boolean expression.
scalar_atom2bexpr()
Converts an atomic expression into the corresponding (boolean) expression.
compile_is_booleanizable_aux()
true if expression is booleanizable

compileCheck.c

Performs semantic checks on the model.

By: Marco Roveri

The routines to perform some the semantic checks.
The performed checks are:

Compile_CheckAssigns()
Semantic checks on assignments of the module.
compileCheckForInputVars()
Checks expressions for illegal occurrences of input vars
Compile_check_next()
Checks that given expression contains either no nested next, or no next operator at all.
Compile_check_input_next()
Checks that given expression contains either no input variables in next.
compileCheckInitForInputVars()
Checks flattened init statement for input variables
compileCheckInvarForInputVars()
Checks flattened invar statement for input variables
compileCheckTransForInputVars()
Checks flattened trans statement for input variables
compileCheckAssignForInputVars()
Checks flattened assign statement for input variables
compileCheckNoNextInputs()
Checks expression for input variables in next statements
init_check_program()
Initializes the data structure to perform semantic checks.
check_circ()
Checks for circular definitions.
check_circular_assign()
Performs circular assignment checking
check_assign()
Checks for multiple or circular assignments.
check_assign_both()
Given a variable, it checks if there are multiple assignments to it.
compile_check_print_io_atom_stack_assign()

compileCmd.c

Shell interface for the compile package.

By: Marco Roveri

This file contains the interface of the compile package with the interactive shell.

See AlsocmdCmd.c

Compile_init()
Initializes the compile package.
Compile_init_cmd()
Initializes the commands provided by this package
Compile_quit()
Shut down the compile package
CommandProcessModel()
Performs the batch steps and then returns control to the interactive shell.
CommandFlattenHierarchy()
Flattens the hierarchy of modules
CommandShowVars()
Shows model's symbolic variables and their values
CommandEncodeVariables()
Builds the BDD variables necessary to compile the model into BDD.
CommandBuildModel()
Compiles the flattened hierarchy into BDD
CommandBuildFlatModel()
Compiles the flattened hierarchy into SEXP
CommandBuildBooleanModel()
Compiles the flattened hierarchy into boolean SEXP
CommandWriteOrder()
Writes variable order to file.
CommandCPPrintClusterInfo()
Prints out information about the clustering. ** DEPRECATED in 2.4 **
CommandPrintFsmStats()
Prints out information about the fsm and clustering.
CommandIwls95PrintOption()
Prints the Iwls95 Options.
CommandGo()
Implements the go command
CommandGoBmc()
Implements the go_bmc command
CommandGetInternalStatus()
Implements the get_internal_status command
CommandWriteModelFlat()
Writes the currently loaded SMV model in the specified file, after having flattened it
CommandWriteModelFlatUdg()
Writes the currently loaded SMV model in the specified uDraw file, after having flattened it
CommandWriteModelFlatBool()
Writes a flat and boolean model of a given SMV file
CommandWriteCoiModel()
Writes a flat model of a given SMV file, restricted to the COI of the model properties
UsageWriteCoiModel()
Prints the usage for the write_coi_command
CommandShowDependencies()
Show expression dependencies
compile_encode_variables()
Encodes variables in the model (BDD only).
compile_flatten_smv()
Traverses the parse tree coming from the smv parser and flattens the smv file.
compile_create_flat_model()
creates the master scalar fsm if needed
compile_create_boolean_model()
Creates the master boolean fsm if needed. A new layer called DETERM_LAYER_NAME will be added if the bool fsm is created.
compile_build_model()
Builds the BDD fsm.
compile_cmd_remove_assignments()
Removes expression in the form "a := b" from the given expression
compile_cmd_write_coi_prop()
Dumps the COI for the given property
compile_cmd_write_coi_prop_fsm()
Dumps the model applied to COI for the given property
get_bits()
Computes the total bit number of symbols in the given list
up_log2()
Computes the log2 of the given argument rounding the result to the closest upper integer
compile_cmd_write_global_coi_fsm()
Dumps on output_file the global coi FSM
compile_cmd_write_properties_coi()
Dumps properties shared COI FSMs or sets
compile_cmd_print_type()
Prints the given type to the given stream
compile_cmd_get_var_type()
Creates an internal representaion of the symbol type

compileCone.c

Computes the cone of influence of the model variables.

By: Marco Roveri and Marco Pistore

This file contains the functions needed for computing the cone of influence (COI) of a given formula. The COI of all the variables in the model is pre-computed ancd cached the first time a cone of influence is required (function initCoi. Functions are also provided that compute the dependency variables for a formula, namely those variables that appear in the formula or in one of the definitions the formula depends on.

()
Indicates that the dependency computation is ongoing.
()
Indicates that the dependency is empty
()
Indicates that no dependency has been yet computed.
()
Indicates that the COI computation should be verbose.
()
Clears and frees (with entries) given hash
Formula_GetDependencies()
Computes dependencies of a given SMV expression
Formula_GetDependenciesByType()
Computes the dependencies of an SMV expression by type
Formulae_GetDependencies()
Compute the dependencies of two set of formulae
Formula_GetConstants()
Calculates the set of constants occurring into the given formula
ComputeCOIFixpoint()
Computes the COI of a given expression
ComputeCOI()
Computes the COI of a given set of variables, defined within the given symb_table
formulaGetDefinitionDependencies()
Compute the dependencies of an atom
formulaGetDependenciesRecur()
Recursive call to Formula_GetDependenciesByType
coiInit()
Pre-compute the COI of the variables
computeCoiVar()
Computes the complete cone for a given variable.
_coi_get_var_coi0()
Given a variable it returns the cone at depth 0.

compileFlatten.c

Flattening of the model.

By: Marco Roveri

Performs the flattening of the model. We start from the module main and we recursively instantiate all the modules or processes declared in it.
Consider the following example:

MODULE main
...
VAR
a : boolean;
b : foo;
...

MODULE foo
VAR
z : boolean;
ASSIGN
z := 1;
The flattening instantiate the module foo in the main module. You can refer to the variables "z" declared in the module foo after the flattening by using the dot notation b.z.

()
Body of define in evaluation
()
Cleans and frees the hash
Compile_FlattenHierarchy()
Traverse the module hierarchy, collect all required the informations and flatten the hierarchy.
Compile_ConstructHierarchy()
Traverses the module hierarchy and extracts the information needed to compile the automaton.
Compile_ProcessHierarchy()
This function processes a hierarchy after collecting all its subparts.
Compile_FlattenSexp()
Builds the flattened version of an expression.
Compile_FlattenSexpExpandDefine()
Flattens an expression and expands defined symbols.
Flatten_GetDefinition()
Gets the flattened version of an atom.
Flatten_remove_symbol_info()
Resets the hashed information about the given symbol
compile_concat_contexts()
Concatenates contexts ctx1 and ctx2
error_bit_selection_assignment_not_supported()
Error message for unsupported feature
compileFlattenProcess()
Flatten a hierarchy of SMV processes.
CompileFlatten_expand_range()
Returns a range going from a to b
CompileFlatten_normalise_value_list()
Takes a list of values and returns the same list being normalised
CompileFlatten_resolve_number()
Resolves the given symbol to be a number
CompileFlatten_resolve_define_chains()
Takes an expression, and if it is a define or parameter resolves it to the actual expression.
CompileFlatten_init_flattener()
Inits the flattener module
CompileFlatten_quit_flattener()
Quits the flattener module
CompileFlatten_hash_module()
Add the tableau module to the list of known modules
Compile_InstantiateType()
convert a type from node_ptr-form constructed by parser into not-memory-shared SymbType_ptr.
Compile_DeclareVariable()
Instantiates the given variable.
compile_add_vars_to_hierarhcy()
Given a fully resolved array name and its type the function adds all the variables in the array to the hierarchy
compile_instantiate_var()
Instantiates the given variable.
compile_instantiate_vars()
Recursively applies compile_instantiate_var.
resolve_range()
This function takes a TWODOTS node, and tries to resolve the bounds to integer numbers which are returned.
put_in_context()
Put a variable in the current "context"
make_params()
Builds the parameters of a module from the list of formal parameters of the module itself.
make_params_hrc()
Builds the parameters of a module from the list of formal and actual parameters of the module itself.
compile_instantiate()
Instantiates all in the body of a module.
compile_instantiate_by_name()
Starts the flattening from a given point in the module hierarchy.
compileFlattenSexpRecur()
Recursive function for flattenig a sexp.
compileFlattenProcessRecur()
Recursive definition of compileFlattenProcess
create_process_symbolic_variables()
Creates the internal process selector variable, within the given layer
construct_array_multiplexer()
Create array multiplexer in order to get rid of dynamic indexes.
push_array_index_down()
Pushes the index-access operator down to if-then-else expressions leaves.
compile_flatten_eval_number()
Tries to resolve recursively to a number
flatten_declare_constants_within_list()
Traverses the list of values, and declare all constants (leaves) it finds
instantiate_array_define()
Instantiates the elements of an array define
compile_insert_assign_hrc()
Add an assign declaration in hrc_result.
get_hrc_root_node()
Get the HRC root node from a child
compile_flatten_get_int()
Given a numeric constant in node_ptr representation the function returns its value as int
compile_flatten_normalise_value_list()
Aux function for the CompileFlatten_normalise_value_list
compile_flatten_build_word_toint_ith_bit_case()
Aux function for the compile_flatten_rewrite_word_toint_cast, which is used for toint cast operator rewriting
compile_flatten_rewrite_word_toint_cast()
Rewrites the toint operator for word expressions conversion

compileStruct.c

Structure used to store compilation results.

By: Marco Roveri

Structure used to store compilation results.

Compile_get_global_predicate_normaliser()
Returns a global predicate normaliser
Compile_get_global_fsm_builder()
Returns the global fsm builder
cmp_struct_init()
Initializes the cmp structure
cmp_struct_quit()
Free the cmp structure

compileUtil.c

Routines for model computation.

By: Marco Roveri

This file contains the code for the compilation of the flattened hierarchy into BDD:

[1] R. K. Ranjan and A. Aziz and B. Plessier and C. Pixley and R. K. Brayton, "Efficient BDD Algorithms for FSM Synthesis and Verification, IEEE/ACM Proceedings International Workshop on Logic Synthesis, Lake Tahoe (NV), May 1995.

sym_intern()
Builds an internal representation for a given string.
()
Private macros for the sake of readability of the function Compile_pop_global
Compile_pop_distrib_ops()
Simplifies the given property by exploiting the distributivity of G, AG and H over AND, and distributivity of F, AF and O over OR
Compile_make_sorted_vars_list_from_order()
This function creates a new list of variables that will contain the same symbols into 'vars', but ordered wrt to 'vars_order' content
Compile_check_if_model_was_built()
Checks if bdd model has been constructed
Compile_check_if_bool_model_was_built()
Checks if boolean model has been constructed
Compile_check_if_flat_model_was_built()
Checks if flat model has been constructed
Compile_check_if_encoding_was_built()
Checks if the variables enconding has been constructed
Compile_check_if_flattening_was_built()
Checks if the flattening has been carried out

compileWrite.c

Creation of an SMV file containing the flattened or booleanized model.

By: Marco Roveri, Roberto Cavada

Creation of an SMV file containing the flattened or booleanized model, processes will be removed by explicitly introducing a process variable and modifying assignments to take care of inertia.

Compile_WriteFlattenModel()
Compile_WriteRestrictedFlattenModel()
Dumps the flatten model on the given FILE
Compile_WriteObfuscatedFlattenModel()
Compile_WriteFlattenFsm()
Prints the flatten version of FSM of an SMV model.
Compile_WriteFlattenSpecs()
Prints the given flatten specifications.
Compile_WriteBoolModel()
Prints the given boolean model
Compile_WriteBoolFsm()
Prints the boolean FSM of an SMV model.
Compile_WriteBoolSpecs()
Prints the boolean specifications of an SMV model.
Compile_make_dag_info()
Compile_destroy_dag_info()
Frees the content of given structures.
Compile_write_dag_defines()
Compile_convert_to_dag()
Top level function to create dags from expressions
Compile_print_array_define()
Prints an array define node to out file.
is_array_define_element()
Returns true iff this name is sub-element of an array define.
is_array_var_element()
Returns true iff this name is sub-element of a variable array.
compile_write_flat_define()
Writes DEFINE declarations in SMV format on a file.
compile_write_obfuscated_flat_define()
Writes DEFINE declarations in SMV format on a file.
compile_write_flat_define_aux()
Writes a DEFINE declarations in SMV format on a file.
compile_write_obfuscated_flat_define_aux()
Writes a DEFINE declarations in SMV format on a file.
compile_write_flatten_vars()
Writes VAR, FROZENVAR, and IVAR declarations in SMV format on a file.
compile_write_obfuscated_flatten_vars()
Writes VAR, FROZENVAR, and IVAR declarations in SMV format on a file.
compile_write_flatten_vars_aux()
Print the variable declaration.
compile_write_obfuscated_flatten_vars_aux()
Print the variable declaration after obfuscation
Compile_obfuscate_expression()
Apply the obfuscation over an expression
compile_write_flat_asgn()
Writes flattened ASSIGN declarations in SMV format on a file.
compile_write_obfuscated_flat_asgn()
Writes flattened ASSIGN declarations in SMV format on a file.
compile_print_assign()
Prints an assignement statement
compile_write_flatten_bool_vars()
Writes boolean VAR, FROZENVAR and IVAR declarations in SMV format on a file. Non boolean vars are dumped as defines for the sake of readability of conterexamples.
compile_write_flatten_spec_split()
Writes flattened spec in SMV format on a file.
compile_write_obfuscated_flatten_spec_split()
Writes flattened spec in SMV format on a file.
compile_write_flatten_spec()
Writes flattened spec in SMV format on a file.
compile_write_obfuscated_flatten_spec()
Writes flattened spec in SMV format on a file.
compile_write_obfuscated_flatten_expr_split()
Writes flattened expression in SMV format on a file.
compile_write_flatten_expr_split()
Writes flattened expression in SMV format on a file.
compile_write_flatten_expr()
Writes flattened expression in SMV format on a file.
compile_write_obfuscated_flatten_expr()
Writes flattened expression in SMV format on a file.
compile_write_flatten_psl()
Writes PSL properties as they are.
compile_write_flatten_bfexpr()
Writes flattened expression in SMV format on a file.
compile_write_flatten_expr_pair()
Writes flattened expression pairs in SMV format on a file.
compile_write_obfuscated_flatten_expr_pair()
Writes flattened expression pairs in SMV format on a file.
compile_write_constants()
Writes the set of non-numeric constants as CONSTANTS statement
compile_write_obfuscated_constants()
Writes the set of non-numeric constants as CONSTANTS statement
Compile_get_obfuscation_map()
Generates the obfuscation map
compile_write_obfuscated_flat_fsm()
Prints the obfuscated flatten version of FSM of an SMV model.
compile_write_flat_fsm()
Prints the flatten version of FSM of an SMV model.
compile_write_get_restricted_vars()
Processes the intersection between the given set and the given list
compile_write_restricted_flat_fsm()
Prints the restricted flatten version of FSM of an SMV model.
compile_write_flat_spec()
Prints the given flatten specifications.
compile_write_obfuscated_flat_spec()
Prints the given flatten specifications.
compile_write_flat_specs()
Prints the flatten specifications of an SMV model.
compile_write_obfuscated_flat_specs()
Prints the obfuscated flatten specifications of an SMV model.
compile_write_bool_fsm()
Prints the boolean FSM of an SMV model.
compile_write_bool_spec()
Private service to print a boolean specification
compile_write_bool_specs()
Prints the boolean specifications of an SMV model.
compile_convert_to_dag_aux()
compile_create_dag_info_from_hierarchy()
compile_make_dag_info_aux()
compile_pack_dag_info()
compile_unpack_dag_info()
compile_set_dag_info()
compile_free_node()
Internal service of Compile_destroy_dag_info
compile_free_define()
Internal service of Compile_destroy_dag_info
compile_symbtype_obfuscated_print()
Prints the obfuscation of the given type
compile_get_rid_of_define_chain()
Get rids of chain of defines
compile_write_obfuscated_dag_defines()
__create_define_name()
Creates a meaningful name for defines needed for dag printing

compileWriteUdg.c

Creation of a UDG file containing the flattened or booleanized model.

By: Marco Roveri, Roberto Cavada, Cristian Mattarei

Creation of a UDG file containing the flattened or booleanized model, processes will be removed by explicitly introducing a process variable and modifying assignments to take care of inertia.

()
Short way of calling printer_base_throw_print_node
()
Short way of print a node with sharing
()
Short way of print a node without sharing
()
Short way of print a node
Compile_WriteFlattenModel_udg()
Compile_WriteFlattenFsm_udg()
Prints the flatten version of FSM of an SMV model.
Compile_WriteFlattenSpecs_udg()
Prints the given flatten specifications.
Compile_WriteBoolModel_udg()
Prints the given boolean model
Compile_WriteBoolFsm_udg()
Prints the boolean FSM of an SMV model.
Compile_WriteBoolSpecs_udg()
Prints the boolean specifications of an SMV model.
Compile_make_dag_info_udg()
Compile_destroy_dag_info_udg()
Frees the content of given structures.
Compile_write_dag_defines_udg()
Compile_convert_to_dag_udg()
Top level function to create dags from expressions
Compile_print_array_define_udg()
Prints a array define node to out file.
compile_write_udg_flatten_array_define()
Writes DEFINE declarations in SMV format on a file.
compile_write_udg_flat_define()
Writes DEFINE declarations in SMV format on a file.
compile_write_flat_array_define_udg()
Writes ARRAY DEFINE declarations in SMV format on a file.
compile_write_udg_flat_asgn()
Writes flattened ASSIGN declarations in SMV format on a file.
compile_print_assign_udg()
Prints an assignement statement
compile_write_udg_flatten_vars()
Writes VAR, FROZENVAR, and IVAR declarations in SMV format on a file.
compile_write_udg_flatten_bool_vars()
Writes boolean VAR, FROZENVAR and IVAR declarations in SMV format on a file. Non boolean vars are dumped as defines for the sake of readability of conterexamples.
compile_write_udg_flatten_spec_split()
Writes flattened spec in SMV format on a file.
compile_write_udg_flatten_spec()
Writes flattened spec in SMV format on a file.
compile_write_udg_flatten_psl()
Writes PSL properties as they are.
compile_write_udg_flatten_bfexpr()
Writes flattened expression in SMV format on a file.
compile_write_udg_flatten_expr_split()
Writes flattened expression in SMV format on a file.
compile_write_udg_flatten_expr()
Writes flattened expression in SMV format on a file.
compile_write_udg_flatten_expr_pair()
Writes flattened expression pairs in SMV format on a file.
compile_write_udg_constants()
Writes the set of non-numeric constants as CONSTANTS statement
compile_write_udg_flat_fsm()
Prints the flatten version of FSM of an SMV model.
compile_write_udg_flat_specs()
Prints the flatten specifications of an SMV model.
compile_write_udg_bool_fsm()
Prints the boolean FSM of an SMV model.
compile_write_udg_bool_spec()
Private service to print a boolean specification
compile_write_udg_bool_specs()
Prints the boolean specifications of an SMV model.
compile_convert_to_dag_aux_udg()
compile_create_dag_info_from_hierarchy_udg()
compile_make_dag_info_aux_udg()
compile_pack_dag_info_udg()
compile_unpack_dag_info_udg()
compile_set_dag_info_udg()
compile_free_node_udg()
Internal service of Compile_destroy_dag_info_udg
compile_free_define_udg()
Internal service of Compile_destroy_dag_info_udg
is_array_define_cell_udg()
Print to the given file the array define represerntation
compile_write_udg_print_node()
Menthod that prints the given node in udg format
insert_assoc_w()
Virtual menthod that prints the given node (core nodes are handled here)
compile_write_udg_print_2_ary()
Printer in udg format for a node with children arity equal to 2
compile_write_udg_print_2_arya()
Printer in udg format for a node with children arity equal to 2
compile_write_udg_print_1_ary()
Printer in udg format for a node with a child
compile_write_udg_print_3_aryc()
Printer in udg format for a node with children arity equal to 3
compile_write_udg_print_3_aryc_color()
Printer in udg format for a node with children arity equal to 3 with different colors

Last updated on 2011/04/06 21h:16