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).

Author: kroening

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,11 @@ 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 vectors.
+  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