add a 'language feature' detection facility for goto programs

This adds a facility to detect the usage of specific language features by a
goto program.  The features are detected by iterating over the functions
of the program.

Checks for three language features not supported by goto symex are added
(assembler, function pointers, vectors).

Author: kroening

jbmc/src/jbmc/CMakeLists.txt

@@ -9,6 +9,7 @@ generic_includes(jbmc-lib)
 
 target_link_libraries(jbmc-lib
     ansi-c
+    assembler
     big-int
     cbmc-lib
     goto-checker

jbmc/src/jbmc/Makefile

@@ -4,6 +4,7 @@ SRC = jbmc_main.cpp \
 
 OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../java_bytecode/java_bytecode$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/assembler/assembler$(LIBEXT) \
       ../$(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
       ../$(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
       ../$(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \

src/assembler/remove_asm.cpp

@@ -565,3 +565,22 @@ void remove_asm(goto_modelt &goto_model)
 {
   remove_asm(goto_model.goto_functions, goto_model.symbol_table);
 }
+
+bool has_asm(const goto_functionst &goto_functions)
+{
+  for(auto &function_it : goto_functions.function_map)
+    for(auto &instruction : function_it.second.body.instructions)
+      if(
+        instruction.is_other() &&
+        instruction.get_other().get_statement() == ID_asm)
+      {
+        return true;
+      }
+
+  return false;
+}
+
+bool has_asm(const goto_modelt &goto_model)
+{
+  return has_asm(goto_model.goto_functions);
+}

src/assembler/remove_asm.h

@@ -60,4 +60,10 @@ void remove_asm(goto_functionst &, symbol_tablet &);
 
 void remove_asm(goto_modelt &);
 
+/// returns true iff the given goto functions use asm instructions
+bool has_asm(const goto_functionst &);
+
+/// returns true iff the given goto model uses asm instructions
+bool has_asm(const goto_modelt &);
+
 #endif // CPROVER_ASSEMBLER_REMOVE_ASM_H

src/goto-checker/module_dependencies.txt

@@ -1,3 +1,4 @@
+assembler
 cbmc # symex_bmc will be moved next
 goto-checker
 goto-instrument

src/goto-checker/multi_path_symex_checker.cpp

@@ -13,6 +13,10 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <util/ui_message.h>
 
+#include <goto-programs/remove_function_pointers.h>
+#include <goto-programs/remove_vector.h>
+
+#include <assembler/remove_asm.h>
 #include <goto-symex/solver_hardness.h>
 
 #include "bmc_util.h"
@@ -27,6 +31,10 @@ multi_path_symex_checkert::multi_path_symex_checkert(
     equation_generated(false),
     property_decider(options, ui_message_handler, equation, ns)
 {
+  // check for certain unsupported language features
+  PRECONDITION(!has_asm(goto_model.get_goto_functions()));
+  PRECONDITION(!has_function_pointers(goto_model.get_goto_functions()));
+  PRECONDITION(!has_vector(goto_model.get_goto_functions()));
 }
 
 incremental_goto_checkert::resultt multi_path_symex_checkert::

src/goto-programs/remove_function_pointers.cpp

@@ -534,3 +534,30 @@ void remove_function_pointers(
 
   rfp(goto_model.goto_functions);
 }
+
+bool has_function_pointers(const goto_programt &goto_program)
+{
+  for(auto &instruction : goto_program.instructions)
+    if(
+      instruction.is_function_call() &&
+      instruction.call_function().id() == ID_dereference)
+    {
+      return true;
+    }
+
+  return false;
+}
+
+bool has_function_pointers(const goto_functionst &goto_functions)
+{
+  for(auto &function_it : goto_functions.function_map)
+    if(has_function_pointers(function_it.second.body))
+      return true;
+
+  return false;
+}
+
+bool has_function_pointers(const goto_modelt &goto_model)
+{
+  return has_function_pointers(goto_model.goto_functions);
+}

src/goto-programs/remove_function_pointers.h

@@ -18,6 +18,7 @@ Date: June 2003
 
 #include <unordered_set>
 
+class goto_functionst;
 class goto_modelt;
 class message_handlert;
 class symbol_tablet;
@@ -54,4 +55,12 @@ bool function_is_type_compatible(
   const code_typet &function_type,
   const namespacet &ns);
 
+/// returns true iff any of the given goto functions has function calls via
+/// a function pointer
+bool has_function_pointers(const goto_functionst &);
+
+/// returns true iff the given goto model has function calls via
+/// a function pointer
+bool has_function_pointers(const goto_modelt &);
+
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H

src/goto-programs/remove_vector.cpp

@@ -386,3 +386,25 @@ void remove_vector(goto_modelt &goto_model)
 {
   remove_vector(goto_model.symbol_table, goto_model.goto_functions);
 }
+
+bool has_vector(const goto_functionst &goto_functions)
+{
+  for(auto &function_it : goto_functions.function_map)
+    for(auto &instruction : function_it.second.body.instructions)
+    {
+      bool has_vector = false;
+      instruction.apply([&has_vector](const exprt &expr) {
+        if(have_to_remove_vector(expr))
+          has_vector = true;
+      });
+      if(has_vector)
+        return true;
+    }
+
+  return false;
+}
+
+bool has_vector(const goto_modelt &goto_model)
+{
+  return has_vector(goto_model.goto_functions);
+}

src/goto-programs/remove_vector.h

@@ -22,4 +22,12 @@ void remove_vector(symbol_table_baset &, goto_functionst &);
 
 void remove_vector(goto_modelt &);
 
+/// returns true iff any of the given goto functions has instructions that use
+/// the vector type
+bool has_vector(const goto_functionst &);
+
+/// returns true iff the given goto model has instructions that use
+/// the vector type
+bool has_vector(const goto_modelt &);
+
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_VECTOR_H