add a 'language feature' detection facility for goto programs

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