Merge pull request #7389 from peterschrammel/nondet-static-matching

Add --nondet-static-matching regex option

Author: kroening

doc/man/goto-instrument.1

@@ -392,6 +392,10 @@ add nondeterministic initialization of variables with static lifetime
 same as nondet\-static except for the variable \fIe\fR
 (use multiple times if required)
 .TP
+\fB\-\-nondet\-static\-matching\fR \fIr\fR
+add nondeterministic initialization of variables
+with static lifetime matching regex \fIr\fR
+.TP
 \fB\-\-function\-enter\fR \fIf\fR
 .TQ
 \fB\-\-function\-exit\fR \fIf\fR

regression/goto-instrument/nondet_static_matching/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int do_nondet_init1;
+int init1;
+
+int main(int argc, char **argv)
+{
+  static int do_nondet_init2;
+  static int init2;
+
+  assert(do_nondet_init1 == 0);
+  assert(init1 == 0);
+  assert(do_nondet_init2 == 0);
+  assert(init2 == 0);
+
+  return 0;
+}

regression/goto-instrument/nondet_static_matching/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--nondet-static-matching '.*\.c:.*nondet.*'
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+assertion do_nondet_init1 == 0: FAILURE
+assertion init1 == 0: SUCCESS
+assertion do_nondet_init2 == 0: FAILURE
+assertion init2 == 0: SUCCESS
+--
+--

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -154,6 +154,17 @@ int goto_instrument_parse_optionst::doit()
       }
     }
 
+    // ignore default/user-specified initialization
+    // of matching variables with static lifetime
+    if(cmdline.isset("nondet-static-matching"))
+    {
+      log.status() << "Adding nondeterministic initialization "
+                      "of matching static/global variables"
+                   << messaget::eom;
+      nondet_static_matching(
+        goto_model, cmdline.get_value("nondet-static-matching"));
+    }
+
     instrument_goto_program();
 
     if(cmdline.isset("validate-goto-model"))
@@ -1898,6 +1909,8 @@ void goto_instrument_parse_optionst::help()
     " --nondet-static              add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
     " --nondet-static-exclude e    same as nondet-static except for the variable e\n" //NOLINT(*)
     "                              (use multiple times if required)\n"
+    " --nondet-static-matching r   add nondeterministic initialization of variables\n" // NOLINT(*)
+    "                              with static lifetime matching regex r\n"
     " --function-enter <f>, --function-exit <f>, --branch <f>\n"
     "                              instruments a call to <f> at the beginning,\n" // NOLINT(*)
     "                              the exit, or a branch point, respectively\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -65,6 +65,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(isr):" \
   "(stack-depth):(nondet-static)" \
   "(nondet-static-exclude):" \
+  "(nondet-static-matching):" \
   "(function-enter):(function-exit):(branch):" \
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \

src/goto-instrument/nondet_static.cpp

@@ -26,6 +26,8 @@ Date: November 2011
 
 #include <linking/static_lifetime_init.h>
 
+#include <regex>
+
 /// See the return.
 /// \param symbol_expr: The symbol expression to analyze.
 /// \param ns: Namespace for resolving type information
@@ -200,3 +202,31 @@ void nondet_static(
 
   nondet_static(ns, goto_model.goto_functions, INITIALIZE_FUNCTION);
 }
+
+/// Nondeterministically initializes global scope variables that
+/// match the given regex.
+/// \param [out] goto_model: Existing goto-model to be updated.
+/// \param regex: regex for matching variables in the format
+///   "filename:variable" (same format as those of except_values in
+///   nondet_static(goto_model, except_values) variant above).
+void nondet_static_matching(goto_modelt &goto_model, const std::string &regex)
+{
+  const auto regex_matcher = std::regex(regex);
+  symbol_tablet &symbol_table = goto_model.symbol_table;
+
+  for(symbol_tablet::iteratort symbol_it = symbol_table.begin();
+      symbol_it != symbol_table.end();
+      symbol_it++)
+  {
+    symbolt &symbol = symbol_it.get_writeable_symbol();
+    std::string qualified_name = id2string(symbol.location.get_file()) + ":" +
+                                 id2string(symbol.display_name());
+    if(!std::regex_match(qualified_name, regex_matcher))
+    {
+      symbol.value.set(ID_C_no_nondet_initialization, 1);
+    }
+  }
+
+  const namespacet ns(goto_model.symbol_table);
+  nondet_static(ns, goto_model.goto_functions, INITIALIZE_FUNCTION);
+}

src/goto-instrument/nondet_static.h

@@ -40,4 +40,6 @@ void nondet_static(goto_modelt &);
 
 void nondet_static(goto_modelt &, const std::set<std::string> &);
 
+void nondet_static_matching(goto_modelt &, const std::string &);
+
 #endif // CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H