From e4f28ec28497ace46257dd558d4463859f94552a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 1 May 2023 16:11:12 +0100 Subject: [PATCH] add a 'language feature' facility for goto programs This adds a facility to track the language features used by a goto program. The features are stored in the value of a symbol in the symbol table part of a goto model. The default, when not specificd, is 'true', i.e., we conservatively assume that the feature might be in use unless we know otherwise. Checks for three language features not supported by goto symex are added (assembler, function pointers, vectors). --- jbmc/src/jbmc/jbmc_parse_options.cpp | 7 ++ src/assembler/remove_asm.cpp | 3 + src/goto-checker/multi_path_symex_checker.cpp | 6 + src/goto-programs/Makefile | 1 + src/goto-programs/language_features.cpp | 106 ++++++++++++++++++ src/goto-programs/language_features.h | 36 ++++++ .../remove_function_pointers.cpp | 5 + src/goto-programs/remove_vector.cpp | 2 + src/util/irep_ids.def | 1 + 9 files changed, 167 insertions(+) create mode 100644 src/goto-programs/language_features.cpp create mode 100644 src/goto-programs/language_features.h diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 324a0868fe3..0736c77e7fe 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -811,6 +812,12 @@ bool jbmc_parse_optionst::process_goto_functions( log.status() << "Running GOTO functions transformation passes" << messaget::eom; + // Our transformations remove function pointers, and + // Java does not have assembler or vectors. + clear_language_feature(goto_model, ID_asm); + clear_language_feature(goto_model, ID_function_pointers); + clear_language_feature(goto_model, ID_vector); + bool using_symex_driven_loading = options.get_bool_option("symex-driven-lazy-loading"); diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp index 9374b3d41e9..fe2017737fe 100644 --- a/src/assembler/remove_asm.cpp +++ b/src/assembler/remove_asm.cpp @@ -23,6 +23,7 @@ Date: December 2014 #include #include +#include #include #include "assembler_parser.h" @@ -39,6 +40,8 @@ class remove_asmt { for(auto &f : goto_functions.function_map) process_function(f.first, f.second); + + clear_language_feature(symbol_table, ID_asm); } protected: diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/src/goto-checker/multi_path_symex_checker.cpp index 76c72b203c2..a2e1b389b78 100644 --- a/src/goto-checker/multi_path_symex_checker.cpp +++ b/src/goto-checker/multi_path_symex_checker.cpp @@ -13,6 +13,8 @@ Author: Daniel Kroening, Peter Schrammel #include +#include + #include #include "bmc_util.h" @@ -27,6 +29,10 @@ multi_path_symex_checkert::multi_path_symex_checkert( equation_generated(false), property_decider(options, ui_message_handler, equation, ns) { + // check the language features used vs. what we support + PRECONDITION(!has_language_feature(goto_model, ID_asm)); + PRECONDITION(!has_language_feature(goto_model, ID_function_pointers)); + PRECONDITION(!has_language_feature(goto_model, ID_vector)); } incremental_goto_checkert::resultt multi_path_symex_checkert:: diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 3d6a56f5416..e09108f549c 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -32,6 +32,7 @@ SRC = allocate_objects.cpp \ json_expr.cpp \ json_goto_trace.cpp \ label_function_pointer_call_sites.cpp \ + language_features.cpp \ link_goto_model.cpp \ link_to_library.cpp \ loop_ids.cpp \ diff --git a/src/goto-programs/language_features.cpp b/src/goto-programs/language_features.cpp new file mode 100644 index 00000000000..4163cb6b2da --- /dev/null +++ b/src/goto-programs/language_features.cpp @@ -0,0 +1,106 @@ +/*******************************************************************\ + +Module: Language Features + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Language Features + +#include "language_features.h" + +#include +#include + +#include "goto_model.h" + +static const irep_idt language_features_identifier = + CPROVER_PREFIX "language_features"; + +static const symbolt * +language_features_symbol(const symbol_tablet &symbol_table) +{ + const namespacet ns(symbol_table); + const symbolt *result; + if(!ns.lookup(language_features_identifier, result)) + return result; + else + return nullptr; +} + +static symbolt &language_features_symbol(symbol_tablet &symbol_table) +{ + symbolt *result = symbol_table.get_writeable(language_features_identifier); + + if(result == nullptr) + { + // need to add + symbolt new_symbol; + new_symbol.base_name = language_features_identifier; + new_symbol.name = language_features_identifier; + new_symbol.mode = + ID_C; // arbitrary, to make symbolt::is_well_formed() happy + new_symbol.value = exprt(irep_idt()); + symbol_table.move(new_symbol, result); + return *result; + } + else + return *result; +} + +bool has_language_feature( + const symbol_tablet &symbol_table, + const irep_idt &feature) +{ + auto symbol = language_features_symbol(symbol_table); + if(symbol == nullptr) + { + // Legacy model without annotations, we conservatively + // assume that the model might use the feature. + return true; + } + else + { + auto &feature_irep = symbol->value.find(feature); + if(feature_irep.is_nil()) + { + // No annotation. We assume that the feature is not used. + return false; + } + else + return symbol->value.get_bool(feature); + } +} + +bool has_language_feature( + const abstract_goto_modelt &model, + const irep_idt &feature) +{ + return has_language_feature(model.get_symbol_table(), feature); +} + +void add_language_feature(symbol_tablet &symbol_table, const irep_idt &feature) +{ + auto &symbol = language_features_symbol(symbol_table); + symbol.value.set(feature, true); +} + +void add_language_feature(goto_modelt &model, const irep_idt &feature) +{ + add_language_feature(model.symbol_table, feature); +} + +void clear_language_feature( + symbol_tablet &symbol_table, + const irep_idt &feature) +{ + auto &symbol = language_features_symbol(symbol_table); + symbol.value.set(feature, false); +} + +void clear_language_feature(goto_modelt &model, const irep_idt &feature) +{ + clear_language_feature(model.symbol_table, feature); +} diff --git a/src/goto-programs/language_features.h b/src/goto-programs/language_features.h new file mode 100644 index 00000000000..48d1f21d461 --- /dev/null +++ b/src/goto-programs/language_features.h @@ -0,0 +1,36 @@ +/*******************************************************************\ + +Module: Language Features + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Language Features + +#ifndef CPROVER_GOTO_PROGRAMS_LANGUAGE_FEATURES_H +#define CPROVER_GOTO_PROGRAMS_LANGUAGE_FEATURES_H + +#include + +class abstract_goto_modelt; +class goto_modelt; +class symbol_tablet; + +/// Returns true when the given goto model indicates that +/// the given language feature might be used. +bool has_language_feature(const abstract_goto_modelt &, const irep_idt &); +bool has_language_feature(const symbol_tablet &, const irep_idt &); + +/// Indicate that the given goto model might use +/// the given language feature. +void add_language_feature(goto_modelt &, const irep_idt &); +void add_language_feature(symbol_tablet &, const irep_idt &); + +/// Indicate that the given goto model does not use +/// the given language feature. +void clear_language_feature(goto_modelt &, const irep_idt &); +void clear_language_feature(symbol_tablet &, const irep_idt &); + +#endif // CPROVER_GOTO_PROGRAMS_LANGUAGE_FEATURES_H diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 23c8b068ad0..38b1a593036 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -28,6 +28,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "compute_called_functions.h" #include "goto_model.h" +#include "language_features.h" #include "remove_const_function_pointers.h" #include "remove_skip.h" @@ -519,6 +520,10 @@ void remove_function_pointerst::operator()(goto_functionst &functions) if(did_something) functions.compute_location_numbers(); + + // We always clear the 'function pointers' feature, even when none + // were present. + clear_language_feature(symbol_table, ID_function_pointers); } void remove_function_pointers( diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index 468d22f3141..8c77609824d 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -19,6 +19,7 @@ Date: September 2014 #include #include "goto_model.h" +#include "language_features.h" static bool have_to_remove_vector(const typet &type); @@ -379,6 +380,7 @@ void remove_vector( { remove_vector(symbol_table); remove_vector(goto_functions); + clear_language_feature(symbol_table, ID_vector); } /// removes vector data type diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index e66f620b755..42e985e65d2 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -904,6 +904,7 @@ IREP_ID_TWO(overflow_result_unary_minus, overflow_result-unary-) IREP_ID_ONE(field_sensitive_ssa) IREP_ID_ONE(checked_assigns) IREP_ID_ONE(enum_is_in_range) +IREP_ID_ONE(function_pointers) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree