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;

src/goto-checker/single_path_symex_only_checker.cpp

@@ -30,7 +30,8 @@ single_path_symex_only_checkert::single_path_symex_only_checkert(
     goto_model(goto_model),
     ns(goto_model.get_symbol_table(), symex_symbol_table),
     worklist(get_path_strategy(options.get_option("exploration-strategy"))),
-    symex_runtime(0)
+    symex_runtime(0),
+    unwindset(goto_model)
 {
 }
 
@@ -70,7 +71,8 @@ void single_path_symex_only_checkert::initialize_worklist()
     equation,
     options,
     *worklist,
-    guard_manager);
+    guard_manager,
+    unwindset);
   setup_symex(symex);
 
   symex.initialize_path_storage_from_entry_point_of(
@@ -95,7 +97,8 @@ bool single_path_symex_only_checkert::resume_path(path_storaget::patht &path)
     path.equation,
     options,
     *worklist,
-    guard_manager);
+    guard_manager,
+    unwindset);
   setup_symex(symex);
 
   symex.resume_symex_from_saved_state(

src/goto-checker/single_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 <chrono>
 
 class symex_bmct;
@@ -40,6 +42,7 @@ class single_path_symex_only_checkert : public incremental_goto_checkert
   guard_managert guard_manager;
   std::unique_ptr<path_storaget> worklist;
   std::chrono::duration<double> symex_runtime;
+  unwindsett unwindset;
 
   void equation_output(
     const symex_bmct &symex,

src/goto-checker/symex_bmc.cpp

@@ -16,13 +16,16 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/source_location.h>
 
+#include <goto-instrument/unwindset.h>
+
 symex_bmct::symex_bmct(
   message_handlert &mh,
   const symbol_tablet &outer_symbol_table,
   symex_target_equationt &_target,
   const optionst &options,
   path_storaget &path_storage,
-  guard_managert &guard_manager)
+  guard_managert &guard_manager,
+  unwindsett &unwindset)
   : goto_symext(
       mh,
       outer_symbol_table,
@@ -33,6 +36,7 @@ symex_bmct::symex_bmct(
     record_coverage(!options.get_option("symex-coverage-report").empty()),
     havoc_bodyless_functions(
       options.get_bool_option("havoc-undefined-functions")),
+    unwindset(unwindset),
     symex_coverage(ns)
 {
 }

src/goto-checker/symex_bmc.h

@@ -16,10 +16,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-symex/goto_symex.h>
 
-#include <goto-instrument/unwindset.h>
-
 #include "symex_coverage.h"
 
+class unwindsett;
+
 class symex_bmct : public goto_symext
 {
 public:
@@ -29,7 +29,8 @@ class symex_bmct : public goto_symext
     symex_target_equationt &_target,
     const optionst &options,
     path_storaget &path_storage,
-    guard_managert &guard_manager);
+    guard_managert &guard_manager,
+    unwindsett &unwindset);
 
   // To show progress
   source_locationt last_source_location;
@@ -81,7 +82,7 @@ class symex_bmct : public goto_symext
   const bool record_coverage;
   const bool havoc_bodyless_functions;
 
-  unwindsett unwindset;
+  unwindsett &unwindset;
 
 protected:
   /// Callbacks that may provide an unwind/do-not-unwind decision for a loop

src/goto-checker/symex_bmc_incremental_one_loop.cpp

@@ -12,21 +12,25 @@ Author: Peter Schrammel, Daniel Kroening, [email protected]
 
 #include <util/structured_data.h>
 
+#include <goto-instrument/unwindset.h>
+
 symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
   message_handlert &message_handler,
   const symbol_tablet &outer_symbol_table,
   symex_target_equationt &target,
   const optionst &options,
   path_storaget &path_storage,
   guard_managert &guard_manager,
+  unwindsett &unwindset,
   ui_message_handlert::uit output_ui)
   : symex_bmct(
       message_handler,
       outer_symbol_table,
       target,
       options,
       path_storage,
-      guard_manager),
+      guard_manager,
+      unwindset),
     incr_loop_id(options.get_option("incremental-loop")),
     incr_max_unwind(
       options.is_set("unwind-max") ? options.get_signed_int_option("unwind-max")

src/goto-checker/symex_bmc_incremental_one_loop.h

@@ -22,6 +22,7 @@ class symex_bmc_incremental_one_loopt : public symex_bmct
     const optionst &,
     path_storaget &,
     guard_managert &,
+    unwindsett &,
     ui_message_handlert::uit output_ui);
 
   /// Return true if symex can be resumed

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -165,7 +165,7 @@ int goto_instrument_parse_optionst::doit()
 
       if(unwind_given || unwindset_given || unwindset_file_given)
       {
-        unwindsett unwindset;
+        unwindsett unwindset{goto_model};
 
         if(unwind_given)
           unwindset.parse_unwind(cmdline.get_value("unwind"));