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