NuSMV Developers Manual: NuSMV/code/nusmv/core/compile/symb

00001 /* ---------------------------------------------------------------------------
00002 
00003    This file is part of the ``compile.symb_table'' package of NuSMV
00004    version 2.  Copyright (C) 2004 by FBK-irst.
00005 
00006    NuSMV version 2 is free software; you can redistribute it and/or
00007    modify it under the terms of the GNU Lesser General Public
00008    License as published by the Free Software Foundation; either
00009    version 2 of the License, or (at your option) any later version.
00010 
00011    NuSMV version 2 is distributed in the hope that it will be useful,
00012    but WITHOUT ANY WARRANTY; without even the implied warranty of
00013    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
00014    Lesser General Public License for more details.
00015 
00016    You should have received a copy of the GNU Lesser General Public
00017    License along with this library; if not, write to the Free Software
00018    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA.
00019 
00020    For more information on NuSMV see <http://nusmv.fbk.eu>
00021    or email to <nusmv-users@fbk.eu>.
00022    Please report bugs to <nusmv-users@fbk.eu>.
00023 
00024    To contact the NuSMV development board, email to <nusmv@fbk.eu>.
00025 
00026    --------------------------------------------------------------------------*/
00027 
00037 #ifndef __NUSMV_CORE_COMPILE_SYMB_TABLE_SYMB_TABLE_CLASS_H__
00038 #define __NUSMV_CORE_COMPILE_SYMB_TABLE_SYMB_TABLE_CLASS_H__
00039 
00040 #if HAVE_CONFIG_H
00041 #  include "nusmv-config.h"
00042 #endif
00043 
00044 #include "nusmv/core/compile/symb_table/SymbLayer.h"
00045 #include "nusmv/core/compile/symb_table/SymbCache.h"
00046 #include "nusmv/core/cinit/NuSMVEnv.h"
00047 #include "nusmv/core/compile/type_checking/TypeChecker.h"
00048 #include "nusmv/core/utils/utils.h"
00049 #include "nusmv/core/utils/array.h"
00050 #include "nusmv/core/utils/assoc.h"
00051 #include "nusmv/core/node/node.h"
00052 #include "nusmv/core/compile/symb_table/NFunction.h"
00053 #include "nusmv/core/set/set.h"
00054 #include "nusmv/core/compile/symb_table/ResolveSymbol.h"
00055 #include "nusmv/core/utils/UStringMgr.h"
00056 #include "nusmv/core/utils/Pair.h"
00057 #include "nusmv/core/node/anonymizers/NodeAnonymizerBase.h"
00058 
00065 typedef struct SymbTable_TAG* SymbTable_ptr;
00066 
00072 #define SYMB_TABLE(x)                           \
00073   ((SymbTable_ptr) x)
00074 
00080 #define SYMB_TABLE_CHECK_INSTANCE(x)                    \
00081   (nusmv_assert(SYMB_TABLE(x) != SYMB_TABLE(NULL)))
00082 
00083 
00133 typedef enum SymbFilterType_TAG {
00134   VFT_CURRENT     = 1,
00135   VFT_NEXT        = VFT_CURRENT << 1,
00136   VFT_INPUT       = VFT_CURRENT << 2,
00137   VFT_FROZEN      = VFT_CURRENT << 3,
00138   VFT_DEFINE      = VFT_CURRENT << 4,
00139   VFT_FUNCTION    = VFT_CURRENT << 5,
00140   VFT_CONSTANTS   = VFT_CURRENT << 6,  /* only symbols */
00141 
00142   /* handy combinations */
00143   VFT_STATE       = (VFT_CURRENT | VFT_NEXT),
00144   VFT_CURR_INPUT  = (VFT_CURRENT | VFT_INPUT),
00145   VFT_CURR_FROZEN = (VFT_CURRENT | VFT_FROZEN),
00146   VFT_CNIF        = (VFT_CURRENT | VFT_NEXT   |
00147                      VFT_INPUT   | VFT_FROZEN), /* It was VFT_ALL */
00148   VFT_CNIFD       = (VFT_CNIF | VFT_DEFINE),    /* It was VFT_ALL_DEFINE */
00149   VFT_ALL         = (VFT_CNIFD | VFT_FUNCTION | VFT_CONSTANTS),
00150 
00151 } SymbFilterType;
00152 
00153 
00160 typedef enum SymbCategory_TAG {
00161   SYMBOL_INVALID = 0, /* This is required by current implementation */
00162   SYMBOL_CONSTANT,
00163   SYMBOL_FROZEN_VAR,
00164   SYMBOL_STATE_VAR,
00165   SYMBOL_INPUT_VAR,
00166   SYMBOL_STATE_DEFINE,
00167   SYMBOL_INPUT_DEFINE,
00168   SYMBOL_STATE_INPUT_DEFINE,
00169   SYMBOL_NEXT_DEFINE,
00170   SYMBOL_STATE_NEXT_DEFINE,
00171   SYMBOL_INPUT_NEXT_DEFINE,
00172   SYMBOL_STATE_INPUT_NEXT_DEFINE,
00173   SYMBOL_DEFINE,
00174   SYMBOL_FUNCTION,
00175   SYMBOL_PARAMETER,
00176   SYMBOL_ARRAY_DEFINE,
00177   SYMBOL_VARIABLE_ARRAY,
00178 } SymbCategory;
00179 
00180 
00181 typedef enum SymbTableType_TAG {
00182   STT_NONE           = 0,
00183   STT_CONSTANT       = 1,
00184 
00185   STT_STATE_VAR      = STT_CONSTANT << 1, /* 2 */
00186   STT_INPUT_VAR      = STT_CONSTANT << 2, /* 4 */
00187   STT_FROZEN_VAR     = STT_CONSTANT << 3, /* 8 */
00188   STT_VAR            = (STT_STATE_VAR | STT_INPUT_VAR |
00189                         STT_FROZEN_VAR), /* 14 */
00190 
00191   STT_DEFINE         = STT_CONSTANT << 4, /* 16 */
00192   STT_ARRAY_DEFINE   = STT_CONSTANT << 5, /* 32 */
00193 
00194   STT_PARAMETER      = STT_CONSTANT << 6, /* 64 */
00195 
00196   STT_FUNCTION       = STT_CONSTANT << 7, /* 128 */
00197 
00198   STT_VARIABLE_ARRAY = STT_CONSTANT << 8, /* 256 */
00199 
00200   STT_ALL            = (STT_CONSTANT | STT_VAR | STT_DEFINE |
00201                         STT_ARRAY_DEFINE | STT_PARAMETER | STT_FUNCTION |
00202                         STT_VARIABLE_ARRAY), /* 511 */
00203 } SymbTableType;
00204 
00205 typedef enum SymbTableTriggerAction_TAG {
00206   ST_TRIGGER_SYMBOL_ADD,
00207   ST_TRIGGER_SYMBOL_REMOVE,
00208   ST_TRIGGER_SYMBOL_REDECLARE
00209 } SymbTableTriggerAction;
00210 
00216 typedef void (*SymbTableForeachFun)(const SymbTable_ptr,
00217                                     const node_ptr sym,
00218                                     void* arg);
00219 
00225 typedef boolean (*SymbTableIterFilterFun)(const SymbTable_ptr table,
00226                                           const node_ptr sym, void* arg);
00227 
00228 
00235 typedef void (*SymbTableTriggerFun)(const SymbTable_ptr table,
00236                                     const node_ptr sym,
00237                                     SymbTableTriggerAction action,
00238                                     void* arg);
00239 
00240 typedef struct SymbTableIter_TAG {
00241   unsigned int index;
00242   unsigned int mask;
00243   SymbTableIterFilterFun filter;
00244   SymbTable_ptr st;
00245   void* arg;
00246 } SymbTableIter;
00247 
00253 #define SYMB_TABLE_FOREACH(self, iter, mask)    \
00254   for (SymbTable_gen_iter(self, &iter, mask);   \
00255        !SymbTable_iter_is_end(self, &iter);     \
00256        SymbTable_iter_next(self, &iter))
00257 
00263 #define SYMB_TABLE_FOREACH_FILTER(self, iter, mask, filter, arg)        \
00264   for (SymbTable_gen_iter(self, &iter, mask),                           \
00265            SymbTable_iter_set_filter(self, &iter, filter, arg);         \
00266        !SymbTable_iter_is_end(self, &iter);                             \
00267        SymbTable_iter_next(self, &iter))
00268 
00269 /* ---------------------------------------------------------------------- */
00270 /*     Public methods                                                     */
00271 /* ---------------------------------------------------------------------- */
00272 
00285 SymbTable_ptr SymbTable_create(NuSMVEnv_ptr env);
00286 
00293 void SymbTable_destroy(SymbTable_ptr self);
00294 
00301 TypeChecker_ptr
00302 SymbTable_get_type_checker(const SymbTable_ptr self);
00303 
00304 /* -------------------------------------- */
00305 /*            ITERATORS                   */
00306 /* -------------------------------------- */
00307 
00320 void SymbTable_gen_iter(const SymbTable_ptr self,
00321                         SymbTableIter* iter,
00322                         unsigned int mask);
00323 
00330 void SymbTable_iter_next(const SymbTable_ptr self,
00331                          SymbTableIter* iter);
00332 
00339 boolean SymbTable_iter_is_end(const SymbTable_ptr self,
00340                               const SymbTableIter* iter);
00341 
00349 node_ptr SymbTable_iter_get_symbol(const SymbTable_ptr self,
00350                                    const SymbTableIter* iter);
00351 
00361 void SymbTable_iter_set_filter(const SymbTable_ptr self,
00362                                SymbTableIter* iter,
00363                                SymbTableIterFilterFun fun,
00364                                void* arg);
00365 
00374 void SymbTable_foreach(const SymbTable_ptr self, unsigned int mask,
00375                        SymbTableForeachFun fun, void* arg);
00376 
00385 Set_t SymbTable_iter_to_set(const SymbTable_ptr self,
00386                             SymbTableIter iter);
00387 
00396 NodeList_ptr SymbTable_iter_to_list(const SymbTable_ptr self,
00397                                     SymbTableIter iter);
00398 
00406 unsigned int SymbTable_iter_count(const SymbTable_ptr self,
00407                                   SymbTableIter iter);
00408 
00447 void
00448 SymbTable_add_trigger(const SymbTable_ptr self,
00449                       SymbTableTriggerFun trigger,
00450                       SymbTableTriggerAction action,
00451                       void* arg1, boolean must_free_arg);
00452 
00461 void
00462 SymbTable_remove_trigger(const SymbTable_ptr self,
00463                          SymbTableTriggerFun trigger,
00464                          SymbTableTriggerAction action);
00465 
00466 /* -------------------------------------- */
00467 /*            Built-in filters            */
00468 /* -------------------------------------- */
00469 
00479 boolean
00480 SymbTable_iter_filter_i_symbols(const SymbTable_ptr self,
00481                                 const node_ptr sym,
00482                                 void* arg);
00483 
00493 boolean
00494 SymbTable_iter_filter_sf_i_symbols(const SymbTable_ptr self,
00495                                    const node_ptr sym,
00496                                    void* arg);
00497 
00507 boolean
00508 SymbTable_iter_filter_sf_symbols(const SymbTable_ptr self,
00509                                  const node_ptr sym,
00510                                  void* arg);
00511 
00518 boolean SymbTable_iter_filter_out_var_array_elems(const SymbTable_ptr self,
00519                                                   const node_ptr sym,
00520                                                   void* arg);
00521 
00522 
00523 /* -------------------------------------- */
00524 /*            Layers handling             */
00525 /* -------------------------------------- */
00526 
00539 SymbLayer_ptr
00540 SymbTable_create_layer(SymbTable_ptr self, const char* layer_name,
00541                        const LayerInsertPolicy ins_policy);
00542 
00559 void
00560 SymbTable_remove_layer(SymbTable_ptr self, SymbLayer_ptr layer);
00561 
00568 SymbLayer_ptr
00569 SymbTable_get_layer(const SymbTable_ptr self,
00570                     const char* layer_name);
00571 
00578 boolean
00579 SymbTable_has_layer(const SymbTable_ptr self,
00580                     const char* layer_name);
00581 
00589 void
00590 SymbTable_rename_layer(const SymbTable_ptr self,
00591                        const char* layer_name, const char* new_name);
00592 
00600 NodeList_ptr SymbTable_get_layers(const SymbTable_ptr self);
00601 
00602 
00603 /* -------------------------------------- */
00604 /*                Symbols                 */
00605 /* -------------------------------------- */
00606 
00607 /* Lists of symbols: */
00608 
00619 NodeList_ptr
00620 SymbTable_get_layers_sf_symbols(SymbTable_ptr self,
00621                                 const array_t* layer_names);
00622 
00632 NodeList_ptr
00633 SymbTable_get_layers_sf_vars(SymbTable_ptr self,
00634                              const array_t* layer_names);
00635 
00645 NodeList_ptr
00646 SymbTable_get_layers_i_symbols(SymbTable_ptr self,
00647                                const array_t* layer_names);
00648 
00658 NodeList_ptr
00659 SymbTable_get_layers_i_vars(SymbTable_ptr self,
00660                             const array_t* layer_names);
00661 
00673 NodeList_ptr
00674 SymbTable_get_layers_sf_i_symbols(SymbTable_ptr self,
00675                                   const array_t* layer_names);
00676 
00685 NodeList_ptr
00686 SymbTable_get_layers_sf_i_vars(SymbTable_ptr self,
00687                                const array_t* layer_names);
00688 
00689 /* Number of symbols: */
00690 
00697 int SymbTable_get_vars_num(const SymbTable_ptr self);
00698 
00705 int SymbTable_get_state_vars_num(const SymbTable_ptr self);
00706 
00713 int SymbTable_get_frozen_vars_num(const SymbTable_ptr self);
00714 
00721 int SymbTable_get_input_vars_num(const SymbTable_ptr self);
00722 
00729 int SymbTable_get_defines_num(const SymbTable_ptr self);
00730 
00737 int SymbTable_get_array_defines_num(const SymbTable_ptr self);
00738 
00745 int SymbTable_get_parameters_num(const SymbTable_ptr self);
00746 
00753 int SymbTable_get_constants_num(const SymbTable_ptr self);
00754 
00761 int SymbTable_get_functions_num(const SymbTable_ptr self);
00762 
00769 int SymbTable_get_symbols_num(const SymbTable_ptr self);
00770 
00771 
00772 /* Classes of layers: */
00773 
00789 void
00790 SymbTable_create_layer_class(SymbTable_ptr self,
00791                              const char* class_name);
00792 
00803 boolean
00804 SymbTable_layer_class_exists(SymbTable_ptr self,
00805                              const char* class_name);
00806 
00821 void
00822 SymbTable_layer_add_to_class(SymbTable_ptr self,
00823                              const char* layer_name,
00824                              const char* class_name);
00825 
00837 void
00838 SymbTable_layer_remove_from_class(SymbTable_ptr self,
00839                                   const char* layer_name,
00840                                   const char* class_name);
00841 
00853 array_t*
00854 SymbTable_get_class_layer_names(SymbTable_ptr self,
00855                                 const char* class_name);
00856 
00863 boolean
00864 SymbTable_is_layer_in_class(SymbTable_ptr self,
00865                             const char* layer_name,
00866                             const char* class_name);
00867 
00874 void
00875 SymbTable_set_default_layers_class_name(SymbTable_ptr self,
00876                                         const char* class_name);
00877 
00892 const char*
00893 SymbTable_get_default_layers_class_name(const SymbTable_ptr self);
00894 
00895 
00896 /* Symbols related info: */
00897 
00905 SymbType_ptr
00906 SymbTable_get_var_type(const SymbTable_ptr self, const node_ptr name);
00907 
00908 /* Symbols related info: */
00909 
00916 SymbType_ptr
00917 SymbTable_get_function_type(const SymbTable_ptr self, const node_ptr name);
00918 
00925 node_ptr
00926 SymbTable_get_define_body(const SymbTable_ptr self,
00927                           const node_ptr name);
00928 
00935 NFunction_ptr
00936 SymbTable_get_function(const SymbTable_ptr self,
00937                        const node_ptr name);
00938 
00945 node_ptr
00946 SymbTable_get_actual_parameter(const SymbTable_ptr self,
00947                                const node_ptr name);
00948 
00955 node_ptr
00956 SymbTable_get_array_define_body(const SymbTable_ptr self,
00957                                 const node_ptr name);
00958 
00965 SymbType_ptr
00966 SymbTable_get_variable_array_type(const SymbTable_ptr self,
00967                                   const node_ptr name);
00968 
00976 node_ptr
00977 SymbTable_get_define_flatten_body(const SymbTable_ptr self,
00978                                   const node_ptr name);
00979 
00987 node_ptr
00988 SymbTable_get_flatten_actual_parameter(const SymbTable_ptr self,
00989                                        const node_ptr name);
00990 
00997 node_ptr
00998 SymbTable_get_array_define_flatten_body(const SymbTable_ptr self,
00999                                         const node_ptr name);
01000 
01007 node_ptr
01008 SymbTable_get_define_context(const SymbTable_ptr self,
01009                              const node_ptr name);
01010 
01017 node_ptr
01018 SymbTable_get_function_context(const SymbTable_ptr self,
01019                                const node_ptr name);
01020 
01028 node_ptr
01029 SymbTable_get_actual_parameter_context(const SymbTable_ptr self,
01030                                        const node_ptr name);
01031 
01038 node_ptr
01039 SymbTable_get_array_define_context(const SymbTable_ptr self,
01040                                    const node_ptr name);
01041 
01055 SymbCategory
01056 SymbTable_get_symbol_category(const SymbTable_ptr self,
01057                               const node_ptr name);
01058 
01059 /* Queries: */
01060 
01067 boolean
01068 SymbTable_is_symbol_state_var(const SymbTable_ptr self,
01069                               const node_ptr name);
01070 
01079 SymbType_ptr
01080 SymbTable_get_symbol_type(const SymbTable_ptr self,
01081                           const node_ptr name);
01082 
01089 boolean
01090 SymbTable_is_symbol_frozen_var(const SymbTable_ptr self,
01091                                const node_ptr name);
01092 
01099 boolean
01100 SymbTable_is_symbol_state_frozen_var(const SymbTable_ptr self,
01101                                      const node_ptr name);
01102 
01109 boolean
01110 SymbTable_is_symbol_input_var(const SymbTable_ptr self,
01111                               const node_ptr name);
01112 
01120 boolean
01121 SymbTable_is_symbol_var(const SymbTable_ptr self, const node_ptr name);
01122 
01130 boolean
01131 SymbTable_is_symbol_bool_var(const SymbTable_ptr self,
01132                              const node_ptr name);
01133 
01140 boolean
01141 SymbTable_is_symbol_declared(const SymbTable_ptr self,
01142                              const node_ptr name);
01143 
01151 boolean
01152 SymbTable_is_symbol_define(const SymbTable_ptr self,
01153                            const node_ptr name);
01154 
01162 boolean
01163 SymbTable_is_symbol_function(const SymbTable_ptr self,
01164                              const node_ptr name);
01165 
01173 boolean
01174 SymbTable_is_symbol_parameter(const SymbTable_ptr self,
01175                               const node_ptr name);
01176 
01184 boolean
01185 SymbTable_is_symbol_array_define(const SymbTable_ptr self,
01186                                  const node_ptr name);
01187 
01195 boolean
01196 SymbTable_is_symbol_variable_array(const SymbTable_ptr self,
01197                                    const node_ptr name);
01198 
01210 boolean
01211 SymbTable_is_symbol_constant(const SymbTable_ptr self,
01212                              const node_ptr name);
01213 
01219 boolean
01220 SymbTable_is_symbol_array_var_element(const SymbTable_ptr symb_table,
01221                                       const node_ptr name);
01222 
01232 node_ptr SymbTable_get_var_array_from_element(const SymbTable_ptr self,
01233                                               node_ptr element);
01234 
01241 node_ptr SymbTable_get_array_lower_bound_variable(const SymbTable_ptr self,
01242                                                   node_ptr array);
01249 node_ptr SymbTable_get_array_upper_bound_variable(const SymbTable_ptr self,
01250                                                   node_ptr array);
01251 
01256 boolean SymbTable_is_symbol_input_var_array(const SymbTable_ptr self,
01257                                             node_ptr array);
01258 
01263 boolean SymbTable_is_symbol_frozen_var_array(const SymbTable_ptr self,
01264                                              node_ptr array);
01265 
01270 boolean SymbTable_is_symbol_state_var_array(const SymbTable_ptr self,
01271                                             node_ptr array);
01272 
01273 
01280 boolean
01281 SymbTable_is_var_finite(const SymbTable_ptr self, const node_ptr name);
01282 
01291 boolean
01292 SymbTable_list_contains_input_var(const SymbTable_ptr self,
01293                                   const NodeList_ptr var_list);
01294 
01303 boolean
01304 SymbTable_list_contains_state_frozen_var(const SymbTable_ptr self,
01305                                          const NodeList_ptr var_list);
01306 
01315 boolean
01316 SymbTable_list_contains_undef_var(const SymbTable_ptr self,
01317                                   const NodeList_ptr var_list);
01318 
01326 Set_t SymbTable_get_type_tags(const SymbTable_ptr self);
01327 
01336 boolean
01337 SymbTable_contains_infinite_precision_variables(const SymbTable_ptr self);
01338 
01345 boolean
01346 SymbTable_contains_enum_variables(const SymbTable_ptr self);
01347 
01354 boolean
01355 SymbTable_contains_word_variables(const SymbTable_ptr self);
01356 
01363 boolean
01364 SymbTable_contains_array_variables(const SymbTable_ptr self);
01365 
01372 boolean
01373 SymbTable_contains_functions(const SymbTable_ptr self);
01374 
01382 SymbLayer_ptr
01383 SymbTable_variable_get_layer(SymbTable_ptr  self, node_ptr name);
01384 
01392 SymbLayer_ptr
01393 SymbTable_define_get_layer(SymbTable_ptr  self, node_ptr name);
01394 
01402 SymbLayer_ptr
01403 SymbTable_symbol_get_layer(SymbTable_ptr  self, node_ptr name);
01404 
01412 SymbLayer_ptr
01413 SymbTable_function_get_layer(SymbTable_ptr  self, node_ptr name);
01414 
01432 node_ptr
01433 SymbTable_get_determinization_var_name(const SymbTable_ptr self);
01434 
01443 node_ptr
01444 SymbTable_get_fresh_symbol_name(const SymbTable_ptr self,
01445                                 const char * prefix);
01446 
01447 
01456 node_ptr SymbTable_get_symbol_from_str(const SymbTable_ptr self,
01457                                        const char* symbol_str);
01458 
01464 const char*
01465 SymbTable_get_class_of_layer(const SymbTable_ptr self,
01466                              const char* layer_name);
01467 
01472 ResolveSymbol_ptr
01473 SymbTable_resolve_symbol(SymbTable_ptr self,
01474                          node_ptr expr, node_ptr context);
01475 
01489 SymbTable_ptr SymbTable_copy(SymbTable_ptr self,
01490                              Set_t blacklist);
01491 
01515 hash_ptr SymbTable_get_handled_hash_ptr(SymbTable_ptr self,
01516                                         const char* key,
01517                                         ST_PFICPCP compare_func,
01518                                         ST_PFICPI hash_func,
01519                                         ST_PFSR destroy_func,
01520                                         SymbTableTriggerFun add_action,
01521                                         SymbTableTriggerFun remove_action,
01522                                         SymbTableTriggerFun redeclare_action
01523                                         );
01524 
01534 void
01535 SymbTable_clear_handled_remove_action_hash(const SymbTable_ptr st,
01536                                            const node_ptr sym,
01537                                            SymbTableTriggerAction action,
01538                                            void* arg);
01539 
01545 char* SymbTable_sprint_category(SymbTable_ptr self,
01546                                 node_ptr symbol);
01547 
01554 SymbTable_ptr SymbTable_anonymize(const SymbTable_ptr self,
01555                                   Set_t blacklist,
01556                                   NodeAnonymizerBase_ptr anonymizer);
01557 
01558 
01559 #endif /* __NUSMV_CORE_COMPILE_SYMB_TABLE_SYMB_TABLE_CLASS_H__ */
NuSMV/code/nusmv/core/compile/symb_table/SymbTable.h
