Merge pull request #5365 from danpoe/feature/selective-havocking-of-volatile-variables

Allow selective havocking of volatile variables

Author: danpoe

.gitignore

@@ -1,6 +1,7 @@
 # Local files generated by IDEs
 .vs/*
 .vscode/*
+*.code-workspace
 ~AutoRecover.*
 *.sln
 *.vcxproj*

regression/goto-instrument/nondet-volatile-02/test.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+volatile int a;
+volatile int b;
+
+void main()
+{
+  assert(a == 0);
+
+  assert(b == 0);
+  assert(b != 0);
+}

regression/goto-instrument/nondet-volatile-02/test.desc

@@ -0,0 +1,13 @@
+CORE
+test.c
+--nondet-volatile-variable b
+\[main.assertion.1\] line \d+ assertion a == 0: SUCCESS
+\[main.assertion.2\] line \d+ assertion b == 0: FAILURE
+\[main.assertion.3\] line \d+ assertion b != 0: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Check that volatile global variables are havocked when given via the
+--nondet-volatile-variable option. Variable a is initialized to zero (as it has
+static storage duration), and is not havocked, thus the assert(a == 0) passes.

regression/goto-instrument/nondet-volatile-03/test.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int x;
+
+void main()
+{
+  x;
+}

regression/goto-instrument/nondet-volatile-03/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--nondet-volatile-variable x
+^Invalid User Input$
+given name x does not represent a volatile variable with static lifetime$
+^EXIT=1$
+^SIGNAL=0$
+--
+--
+Check that it is invalid to specify a non-volatile variable to be havocked

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -996,6 +996,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 {
   optionst options;
 
+  parse_nondet_volatile_options(cmdline, options);
+
   // disable simplify when adding various checks?
   if(cmdline.isset("no-simplify"))
     options.set_option("simplify", false);
@@ -1622,13 +1624,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   // label the assertions
   label_properties(goto_model);
 
-  // nondet volatile?
-  if(cmdline.isset("nondet-volatile"))
-  {
-    log.status() << "Making volatile variables non-deterministic"
-                 << messaget::eom;
-    nondet_volatile(goto_model);
-  }
+  nondet_volatile(goto_model, options);
 
   // reachability slice?
   if(cmdline.isset("reachability-slice"))
@@ -1803,7 +1799,7 @@ void goto_instrument_parse_optionst::help()
     " --race-check                 add floating-point data race checks\n"
     "\n"
     "Semantic transformations:\n"
-    " --nondet-volatile            makes reads from volatile variables non-deterministic\n" // NOLINT(*)
+    HELP_NONDET_VOLATILE
     " --unwind <n>                 unwinds the loops <n> times\n"
     " --unwindset L:B,...          unwind loop L with a bound of B\n"
     " --unwindset-file <file>      read unwindset from file\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -33,6 +33,7 @@ Author: Daniel Kroening, [email protected]
 #include "code_contracts.h"
 #include "generate_function_bodies.h"
 #include "insert_final_assert_false.h"
+#include "nondet_volatile.h"
 #include "replace_calls.h"
 
 #include "count_eloc.h"
@@ -65,7 +66,7 @@ Author: Daniel Kroening, [email protected]
   OPT_INSERT_FINAL_ASSERT_FALSE \
   OPT_SHOW_CLASS_HIERARCHY \
   "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
-  "(nondet-volatile)(isr):" \
+  "(isr):" \
   "(stack-depth):(nondet-static)" \
   "(nondet-static-exclude):" \
   "(function-enter):(function-exit):(branch):" \
@@ -119,6 +120,7 @@ Author: Daniel Kroening, [email protected]
   OPT_VALIDATE \
   OPT_ANSI_C_LANGUAGE \
   OPT_RESTRICT_FUNCTION_POINTER \
+  OPT_NONDET_VOLATILE \
   "(ensure-one-backedge-per-target)" \
   // empty last line
 

src/goto-instrument/nondet_volatile.cpp

@@ -13,9 +13,13 @@ Date: September 2011
 
 #include "nondet_volatile.h"
 
+#include <util/cmdline.h>
+#include <util/options.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
+using havoc_predicatet = std::function<bool(const exprt &)>;
+
 static bool is_volatile(const namespacet &ns, const typet &src)
 {
   if(src.get_bool(ID_C_volatile))
@@ -31,16 +35,19 @@ static bool is_volatile(const namespacet &ns, const typet &src)
   return false;
 }
 
-static void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
+static void nondet_volatile_rhs(
+  const symbol_tablet &symbol_table,
+  exprt &expr,
+  havoc_predicatet should_havoc)
 {
   Forall_operands(it, expr)
-    nondet_volatile_rhs(symbol_table, *it);
+    nondet_volatile_rhs(symbol_table, *it, should_havoc);
 
   if(expr.id()==ID_symbol ||
      expr.id()==ID_dereference)
   {
     const namespacet ns(symbol_table);
-    if(is_volatile(ns, expr.type()))
+    if(is_volatile(ns, expr.type()) && should_havoc(expr))
     {
       typet t=expr.type();
       t.remove(ID_C_volatile);
@@ -52,31 +59,42 @@ static void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
   }
 }
 
-static void nondet_volatile_lhs(const symbol_tablet &symbol_table, exprt &expr)
+static void nondet_volatile_lhs(
+  const symbol_tablet &symbol_table,
+  exprt &expr,
+  havoc_predicatet should_havoc)
 {
   if(expr.id()==ID_if)
   {
-    nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond());
-    nondet_volatile_lhs(symbol_table, to_if_expr(expr).true_case());
-    nondet_volatile_lhs(symbol_table, to_if_expr(expr).false_case());
+    nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond(), should_havoc);
+    nondet_volatile_lhs(
+      symbol_table, to_if_expr(expr).true_case(), should_havoc);
+    nondet_volatile_lhs(
+      symbol_table, to_if_expr(expr).false_case(), should_havoc);
   }
   else if(expr.id()==ID_index)
   {
-    nondet_volatile_lhs(symbol_table, to_index_expr(expr).array());
-    nondet_volatile_rhs(symbol_table, to_index_expr(expr).index());
+    nondet_volatile_lhs(
+      symbol_table, to_index_expr(expr).array(), should_havoc);
+    nondet_volatile_rhs(
+      symbol_table, to_index_expr(expr).index(), should_havoc);
   }
   else if(expr.id()==ID_member)
   {
-    nondet_volatile_lhs(symbol_table, to_member_expr(expr).struct_op());
+    nondet_volatile_lhs(
+      symbol_table, to_member_expr(expr).struct_op(), should_havoc);
   }
   else if(expr.id()==ID_dereference)
   {
-    nondet_volatile_rhs(symbol_table, to_dereference_expr(expr).pointer());
+    nondet_volatile_rhs(
+      symbol_table, to_dereference_expr(expr).pointer(), should_havoc);
   }
 }
 
-static void
-nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
+static void nondet_volatile(
+  symbol_tablet &symbol_table,
+  goto_programt &goto_program,
+  havoc_predicatet should_havoc)
 {
   namespacet ns(symbol_table);
 
@@ -86,8 +104,10 @@ nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
 
     if(instruction.is_assign())
     {
-      nondet_volatile_rhs(symbol_table, to_code_assign(instruction.code).rhs());
-      nondet_volatile_lhs(symbol_table, to_code_assign(instruction.code).lhs());
+      nondet_volatile_rhs(
+        symbol_table, to_code_assign(instruction.code).rhs(), should_havoc);
+      nondet_volatile_lhs(
+        symbol_table, to_code_assign(instruction.code).lhs(), should_havoc);
     }
     else if(instruction.is_function_call())
     {
@@ -101,25 +121,105 @@ nondet_volatile(symbol_tablet &symbol_table, goto_programt &goto_program)
           it=code_function_call.arguments().begin();
           it!=code_function_call.arguments().end();
           it++)
-        nondet_volatile_rhs(symbol_table, *it);
+        nondet_volatile_rhs(symbol_table, *it, should_havoc);
 
       // do return value
-      nondet_volatile_lhs(symbol_table, code_function_call.lhs());
+      nondet_volatile_lhs(symbol_table, code_function_call.lhs(), should_havoc);
     }
     else if(instruction.has_condition())
     {
       // do condition
       exprt cond = instruction.get_condition();
-      nondet_volatile_rhs(symbol_table, cond);
+      nondet_volatile_rhs(symbol_table, cond, should_havoc);
       instruction.set_condition(cond);
     }
   }
 }
 
-void nondet_volatile(goto_modelt &goto_model)
+void nondet_volatile(goto_modelt &goto_model, havoc_predicatet should_havoc)
 {
   Forall_goto_functions(f_it, goto_model.goto_functions)
-    nondet_volatile(goto_model.symbol_table, f_it->second.body);
+    nondet_volatile(goto_model.symbol_table, f_it->second.body, should_havoc);
 
   goto_model.goto_functions.update();
 }
+
+void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
+{
+  PRECONDITION(!options.is_set(NONDET_VOLATILE_OPT));
+  PRECONDITION(!options.is_set(NONDET_VOLATILE_VARIABLE_OPT));
+
+  const bool nondet_volatile_opt = cmdline.isset(NONDET_VOLATILE_OPT);
+  const bool nondet_volatile_variable_opt =
+    cmdline.isset(NONDET_VOLATILE_VARIABLE_OPT);
+
+  if(nondet_volatile_opt && nondet_volatile_variable_opt)
+  {
+    throw invalid_command_line_argument_exceptiont(
+      "only one of " NONDET_VOLATILE_OPT "/" NONDET_VOLATILE_VARIABLE_OPT
+      "can "
+      "be given at a time",
+      NONDET_VOLATILE_OPT "/" NONDET_VOLATILE_VARIABLE_OPT);
+  }
+
+  if(nondet_volatile_opt)
+  {
+    options.set_option(NONDET_VOLATILE_OPT, true);
+  }
+  else if(cmdline.isset(NONDET_VOLATILE_VARIABLE_OPT))
+  {
+    options.set_option(
+      NONDET_VOLATILE_VARIABLE_OPT,
+      cmdline.get_values(NONDET_VOLATILE_VARIABLE_OPT));
+  }
+}
+
+void nondet_volatile(goto_modelt &goto_model, const optionst &options)
+{
+  if(options.get_bool_option(NONDET_VOLATILE_OPT))
+  {
+    nondet_volatile(goto_model);
+  }
+  else if(options.is_set(NONDET_VOLATILE_VARIABLE_OPT))
+  {
+    const auto &variable_list =
+      options.get_list_option(NONDET_VOLATILE_VARIABLE_OPT);
+
+    std::set<irep_idt> variables(variable_list.begin(), variable_list.end());
+    const namespacet ns(goto_model.symbol_table);
+
+    // typecheck given variables
+    for(const auto &id : variables)
+    {
+      const symbolt *symbol;
+
+      if(ns.lookup(id, symbol))
+      {
+        throw invalid_command_line_argument_exceptiont(
+          "given name " + id2string(id) + " not found in symbol table",
+          NONDET_VOLATILE_VARIABLE_OPT);
+      }
+
+      if(!symbol->is_static_lifetime || !symbol->type.get_bool(ID_C_volatile))
+      {
+        throw invalid_command_line_argument_exceptiont(
+          "given name " + id2string(id) +
+            " does not represent a volatile "
+            "variable with static lifetime",
+          NONDET_VOLATILE_VARIABLE_OPT);
+      }
+
+      INVARIANT(!symbol->is_type, "symbol must not represent a type");
+
+      INVARIANT(
+        symbol->type.id() != ID_code, "symbol must not represent a function");
+    }
+
+    auto should_havoc = [&variables](const exprt &expr) {
+      return expr.id() == ID_symbol &&
+             variables.count(to_symbol_expr(expr).get_identifier()) != 0;
+    };
+
+    nondet_volatile(goto_model, should_havoc);
+  }
+}

src/goto-instrument/nondet_volatile.h

@@ -14,6 +14,42 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_model.h>
 
-void nondet_volatile(goto_modelt &);
+class cmdlinet;
+class optionst;
+
+// clang-format off
+#define NONDET_VOLATILE_OPT "nondet-volatile"
+#define NONDET_VOLATILE_VARIABLE_OPT "nondet-volatile-variable"
+
+#define OPT_NONDET_VOLATILE \
+  "(" NONDET_VOLATILE_OPT ")" \
+  "(" NONDET_VOLATILE_VARIABLE_OPT "):"
+
+#define HELP_NONDET_VOLATILE \
+  " --" NONDET_VOLATILE_OPT "            makes reads from volatile variables " \
+  "non-deterministic\n" \
+  " --" NONDET_VOLATILE_VARIABLE_OPT " <variable>\n" \
+  "                              makes reads from given volatile variable " \
+  "non-deterministic\n"
+// clang-format on
+
+void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options);
+
+/// Havoc reads from volatile expressions, if enabled in the options
+///
+/// \param goto_model: the goto model in which to havoc volatile reads
+/// \param options: command line options
+void nondet_volatile(goto_modelt &goto_model, const optionst &options);
+
+/// Havoc reads from volatile expressions
+///
+/// \param goto_model: the goto model in which to havoc volatile reads
+/// \param should_havoc: predicate indicating if the given volatile expression
+///   should be havocked
+void nondet_volatile(
+  goto_modelt &goto_model,
+  std::function<bool(const exprt &)> should_havoc = [](const exprt &) {
+    return true;
+  });
 
 #endif // CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H