Merge pull request #6508 from tautschnig/refer-by-label

Support labels in unwindset/function-pointer-restrictions

Author: tautschnig

doc/architectural/restrict-function-pointer.md

@@ -73,9 +73,12 @@ function where function pointers are being called, to this pattern:
 ```
 <function-name>.function_pointer_call.<N>
 ```
-
 where `N` is referring to which function call it is - so the first call to a
-function pointer in a function will have `N=1`, the 5th `N=5` etc.
+function pointer in a function will have `N=1`, the 5th `N=5` etc, or
+```
+<function-name>.<label>
+```
+when the function call is labelled.
 
 We can call `goto-instrument --restrict-function-pointer
 call.function_pointer_call.1/f,g in.gb out.gb`. This can be read as

regression/cbmc/unwindset1/label.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwindset main.for_loop:2,main.1:6
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/unwindset1/main.c

@@ -0,0 +1,10 @@
+int main()
+{
+  int x;
+for_loop:
+  for(int i = 0; i < x; ++i)
+    --x;
+  for(int j = 0; j < 5; ++j)
+    ++x;
+  __CPROVER_assert(0, "can be reached");
+}

regression/cbmc/unwindset1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--unwindset main.0:2,main.2:2
+^Invalid User Input$
+^Option: unwindset$
+^Reason: invalid loop identifier main\.2$
+^EXIT=1$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/goto-instrument/restrict-function-pointer-by-label/test.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+
+typedef int (*fptr_t)(int);
+
+void use_f(fptr_t fptr)
+{
+labelled_call:
+  assert(fptr(10) == 11);
+}
+
+int f(int x)
+{
+  return x + 1;
+}
+
+int g(int x)
+{
+  return x;
+}
+
+int main(void)
+{
+  int one = 1;
+
+  // We take the address of f and g. In this case remove_function_pointers()
+  // would create a case distinction involving both f and g in the function
+  // use_f() above.
+  use_f(one ? f : g);
+}

regression/goto-instrument/restrict-function-pointer-by-label/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--restrict-function-pointer use_f.labelled_call/f
+\[use_f\.assertion\.1\] line \d+ assertion fptr\(10\) == 11: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test checks that the function f is called for the first function pointer
+call in function use_f when using the label to refer to the call site.

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -28,13 +28,15 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
     goto_model(goto_model),
     ns(goto_model.get_symbol_table(), symex_symbol_table),
     equation(ui_message_handler),
+    unwindset(goto_model),
     symex(
       ui_message_handler,
       goto_model.get_symbol_table(),
       equation,
       options,
       path_storage,
-      guard_manager)
+      guard_manager,
+      unwindset)
 {
   setup_symex(symex, ns, options, ui_message_handler);
 }

src/goto-checker/multi_path_symex_only_checker.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-symex/path_storage.h>
 
+#include <goto-instrument/unwindset.h>
+
 #include "symex_bmc.h"
 
 class multi_path_symex_only_checkert : public incremental_goto_checkert
@@ -35,6 +37,7 @@ class multi_path_symex_only_checkert : public incremental_goto_checkert
   symex_target_equationt equation;
   guard_managert guard_manager;
   path_fifot path_storage; // should go away
+  unwindsett unwindset;
   symex_bmct symex;
 
   /// Generates the equation by running goto-symex

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -30,13 +30,15 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
     goto_model(goto_model),
     ns(goto_model.get_symbol_table(), symex_symbol_table),
     equation(ui_message_handler),
+    unwindset(goto_model),
     symex(
       ui_message_handler,
       goto_model.get_symbol_table(),
       equation,
       options,
       path_storage,
       guard_manager,
+      unwindset,
       ui_message_handler.get_ui()),
     property_decider(options, ui_message_handler, equation, ns)
 {

src/goto-checker/single_loop_incremental_symex_checker.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-symex/path_storage.h>
 
+#include <goto-instrument/unwindset.h>
+
 #include "goto_symex_property_decider.h"
 #include "goto_trace_provider.h"
 #include "incremental_goto_checker.h"
@@ -57,6 +59,7 @@ class single_loop_incremental_symex_checkert : public incremental_goto_checkert,
   symex_target_equationt equation;
   path_fifot path_storage; // should go away
   guard_managert guard_manager;
+  unwindsett unwindset;
   symex_bmc_incremental_one_loopt symex;
   bool initial_equation_generated = false;
   bool full_equation_generated = false;