add a 'language feature' facility for goto programs

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_check.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/instrument_preconditions.h>
+#include <goto-programs/language_features.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_skip.h>
@@ -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");
 

src/assembler/remove_asm.cpp

@@ -23,6 +23,7 @@ Date:   December 2014
 #include <util/string_constant.h>
 
 #include <goto-programs/goto_model.h>
+#include <goto-programs/language_features.h>
 #include <goto-programs/remove_skip.h>
 
 #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:

src/goto-checker/multi_path_symex_checker.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <util/ui_message.h>
 
+#include <goto-programs/language_features.h>
+
 #include <goto-symex/solver_hardness.h>
 
 #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::

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 \

src/goto-programs/language_features.cpp

@@ -0,0 +1,106 @@
+/*******************************************************************\
+
+Module: Language Features
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Language Features
+
+#include "language_features.h"
+
+#include <util/cprover_prefix.h>
+#include <util/namespace.h>
+
+#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);
+}

src/goto-programs/language_features.h

@@ -0,0 +1,36 @@
+/*******************************************************************\
+
+Module: Language Features
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Language Features
+
+#ifndef CPROVER_GOTO_PROGRAMS_LANGUAGE_FEATURES_H
+#define CPROVER_GOTO_PROGRAMS_LANGUAGE_FEATURES_H
+
+#include <util/irep.h>
+
+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

src/goto-programs/remove_function_pointers.cpp

@@ -28,6 +28,7 @@ Author: Daniel Kroening, [email protected]
 
 #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(

src/goto-programs/remove_vector.cpp

@@ -19,6 +19,7 @@ Date:   September 2014
 #include <ansi-c/c_expr.h>
 
 #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

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