Refactor existing nondet volatile code

Refactor the code such as to allow later addition of new feature to
selectively provide models for volatile reads

Author: danpoe

src/goto-instrument/nondet_volatile.cpp

@@ -19,41 +19,64 @@ Date: September 2011
 #include <util/string_utils.h>
 #include <util/symbol_table.h>
 
-using havoc_predicatet = std::function<bool(const exprt &)>;
-
 class nondet_volatilet
 {
 public:
-  static void nondet_volatile(
-    symbol_tablet &symbol_table,
-    goto_programt &goto_program,
-    havoc_predicatet should_havoc);
+  nondet_volatilet(
+    goto_modelt &goto_model,
+    const optionst &options) : goto_model(goto_model), all_nondet(false)
+  {
+    typecheck_options(options);
+  }
 
-  static const symbolt &typecheck_variable(
-    const irep_idt &id,
-    const namespacet &ns);
+  void operator()()
+  {
+    if(!all_nondet && nondet_variables.empty() && variable_models.empty())
+    {
+      return;
+    }
+
+    for(auto &f : goto_model.goto_functions.function_map)
+    {
+      nondet_volatile(
+        goto_model.symbol_table,
+        f.second.body);
+    }
+
+    goto_model.goto_functions.update();
+  }
 
 private:
   static bool is_volatile(const namespacet &ns, const typet &src);
 
-  static void nondet_volatile_rhs(
-    const symbol_tablet &symbol_table,
+  void handle_volatile_expression(
     exprt &expr,
-    havoc_predicatet should_havoc);
+    const namespacet &ns);
 
-  static void nondet_volatile_lhs(
+  void nondet_volatile_rhs(
     const symbol_tablet &symbol_table,
-    exprt &expr,
-    havoc_predicatet should_havoc);
+    exprt &expr);
+
+  void nondet_volatile_lhs(
+    const symbol_tablet &symbol_table,
+    exprt &expr);
+
+  void nondet_volatile(
+    symbol_tablet &symbol_table,
+    goto_programt &goto_program);
 
-  static void typecheck_model(
+  const symbolt &typecheck_variable(
+    const irep_idt &id,
+    const namespacet &ns);
+
+  void typecheck_model(
     const irep_idt &id,
     const symbolt &variable,
     const namespacet &ns);
 
-  void typecheck_options(
-    const goto_modelt &goto_model,
-    const optionst &options);
+  void typecheck_options(const optionst &options);
+
+  goto_modelt &goto_model;
 
   // configuration obtained from command line options
   bool all_nondet;
@@ -76,66 +99,76 @@ bool nondet_volatilet::is_volatile(const namespacet &ns, const typet &src)
   return false;
 }
 
+void nondet_volatilet::handle_volatile_expression(
+  exprt &expr,
+  const namespacet &ns)
+{
+  if(all_nondet ||
+    (expr.id() == ID_symbol &&
+    nondet_variables.count(to_symbol_expr(expr).get_identifier()) != 0))
+  {
+    typet t = expr.type();
+    t.remove(ID_C_volatile);
+
+    // replace by nondet
+    side_effect_expr_nondett nondet_expr(t, expr.source_location());
+    expr.swap(nondet_expr);
+  }
+}
+
 void nondet_volatilet::nondet_volatile_rhs(
   const symbol_tablet &symbol_table,
-  exprt &expr,
-  havoc_predicatet should_havoc)
+  exprt &expr)
 {
   Forall_operands(it, expr)
-    nondet_volatile_rhs(symbol_table, *it, should_havoc);
+    nondet_volatile_rhs(symbol_table, *it);
 
   if(expr.id()==ID_symbol ||
      expr.id()==ID_dereference)
   {
     const namespacet ns(symbol_table);
-    if(is_volatile(ns, expr.type()) && should_havoc(expr))
-    {
-      typet t=expr.type();
-      t.remove(ID_C_volatile);
 
-      // replace by nondet
-      side_effect_expr_nondett nondet_expr(t, expr.source_location());
-      expr.swap(nondet_expr);
+    if(is_volatile(ns, expr.type()))
+    {
+      handle_volatile_expression(expr, ns);
     }
   }
 }
 
 void nondet_volatilet::nondet_volatile_lhs(
   const symbol_tablet &symbol_table,
-  exprt &expr,
-  havoc_predicatet should_havoc)
+  exprt &expr)
 {
   if(expr.id()==ID_if)
   {
-    nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond(), should_havoc);
+    nondet_volatile_rhs(symbol_table, to_if_expr(expr).cond());
     nondet_volatile_lhs(
-      symbol_table, to_if_expr(expr).true_case(), should_havoc);
+      symbol_table, to_if_expr(expr).true_case());
     nondet_volatile_lhs(
-      symbol_table, to_if_expr(expr).false_case(), should_havoc);
+      symbol_table, to_if_expr(expr).false_case());
   }
   else if(expr.id()==ID_index)
   {
     nondet_volatile_lhs(
-      symbol_table, to_index_expr(expr).array(), should_havoc);
+      symbol_table, to_index_expr(expr).array());
     nondet_volatile_rhs(
-      symbol_table, to_index_expr(expr).index(), should_havoc);
+      symbol_table, to_index_expr(expr).index());
   }
   else if(expr.id()==ID_member)
   {
     nondet_volatile_lhs(
-      symbol_table, to_member_expr(expr).struct_op(), should_havoc);
+      symbol_table, to_member_expr(expr).struct_op());
   }
   else if(expr.id()==ID_dereference)
   {
     nondet_volatile_rhs(
-      symbol_table, to_dereference_expr(expr).pointer(), should_havoc);
+      symbol_table, to_dereference_expr(expr).pointer());
   }
 }
 
 void nondet_volatilet::nondet_volatile(
   symbol_tablet &symbol_table,
-  goto_programt &goto_program,
-  havoc_predicatet should_havoc)
+  goto_programt &goto_program)
 {
   namespacet ns(symbol_table);
 
@@ -146,9 +179,9 @@ void nondet_volatilet::nondet_volatile(
     if(instruction.is_assign())
     {
       nondet_volatile_rhs(
-        symbol_table, to_code_assign(instruction.code).rhs(), should_havoc);
+        symbol_table, to_code_assign(instruction.code).rhs());
       nondet_volatile_lhs(
-        symbol_table, to_code_assign(instruction.code).lhs(), should_havoc);
+        symbol_table, to_code_assign(instruction.code).lhs());
     }
     else if(instruction.is_function_call())
     {
@@ -162,16 +195,16 @@ void nondet_volatilet::nondet_volatile(
           it=code_function_call.arguments().begin();
           it!=code_function_call.arguments().end();
           it++)
-        nondet_volatile_rhs(symbol_table, *it, should_havoc);
+        nondet_volatile_rhs(symbol_table, *it);
 
       // do return value
-      nondet_volatile_lhs(symbol_table, code_function_call.lhs(), should_havoc);
+      nondet_volatile_lhs(symbol_table, code_function_call.lhs());
     }
     else if(instruction.has_condition())
     {
       // do condition
       exprt cond = instruction.get_condition();
-      nondet_volatile_rhs(symbol_table, cond, should_havoc);
+      nondet_volatile_rhs(symbol_table, cond);
       instruction.set_condition(cond);
     }
   }
@@ -246,9 +279,9 @@ void nondet_volatilet::typecheck_model(
 }
 
 void nondet_volatilet::typecheck_options(
-  const goto_modelt &goto_model,
   const optionst &options)
 {
+  PRECONDITION(!all_nondet);
   PRECONDITION(nondet_variables.empty());
   PRECONDITION(variable_models.empty());
 
@@ -317,17 +350,6 @@ void nondet_volatilet::typecheck_options(
   }
 }
 
-void nondet_volatile(goto_modelt &goto_model, havoc_predicatet should_havoc)
-{
-  Forall_goto_functions(f_it, goto_model.goto_functions)
-    nondet_volatilet::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));
@@ -374,28 +396,6 @@ void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
 
 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);
-
-    for(const auto &id : variables)
-    {
-      nondet_volatilet::typecheck_variable(id, ns);
-    }
-
-    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);
-  }
+  nondet_volatilet nv(goto_model, options);
+  nv();
 }