Merge pull request #2874 from svorenova/nondet_static_condition

Small fix and some cleaning in nondet-static [TG-2755]

Author: svorenova

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -347,6 +347,7 @@ static symbol_exprt get_or_create_class_literal_symbol(
     new_class_symbol.is_lvalue = true;
     new_class_symbol.is_state_var = true;
     new_class_symbol.is_static_lifetime = true;
+    new_class_symbol.type.set(ID_C_no_nondet_initialization, true);
     symbol_table.add(new_class_symbol);
   }
 

src/goto-instrument/nondet_static.cpp

@@ -1,7 +1,9 @@
 /*******************************************************************\
 
-Module: Nondeterministic initialization of certain global scope
-        variables
+Module: Nondeterministically initializes global scope variables, except for
+ constants (such as string literals, final fields) and internal variables
+ (such as CPROVER and symex variables, language specific internal
+ variables).
 
 Author: Daniel Kroening, Michael Tautschnig
 
@@ -10,14 +12,56 @@ Date: November 2011
 \*******************************************************************/
 
 /// \file
-/// Nondeterministic initialization of certain global scope variables
+/// Nondeterministically initializes global scope variables, except for
+/// constants (such as string literals, final fields) and internal variables
+/// (such as CPROVER and symex variables, language specific internal
+/// variables).
 
 #include "nondet_static.h"
 
 #include <goto-programs/goto_model.h>
 
 #include <linking/static_lifetime_init.h>
 
+/// See the return.
+/// \param sym The symbol expression to analyze.
+/// \param ns Namespace for resolving type information
+/// \return True if the symbol expression holds a static symbol which can be
+/// nondeterministically initialized, false otherwise.
+bool is_nondet_initializable_static(
+  const symbol_exprt &sym,
+  const namespacet &ns)
+{
+  const irep_idt &id = sym.get_identifier();
+
+  // is it a __CPROVER_* variable?
+  if(has_prefix(id2string(id), CPROVER_PREFIX))
+    return false;
+
+  // variable not in symbol table such as symex variable?
+  if(!ns.get_symbol_table().has_symbol(id))
+    return false;
+
+  // is the type explicitly marked as not to be nondet initialized?
+  if(ns.lookup(id).type.get_bool(ID_C_no_nondet_initialization))
+    return false;
+
+  // static lifetime?
+  if(!ns.lookup(id).is_static_lifetime)
+    return false;
+
+  // constant?
+  return !is_constant_or_has_constant_components(sym.type(), ns) &&
+         !is_constant_or_has_constant_components(ns.lookup(id).type, ns);
+}
+
+/// Nondeterministically initializes global scope variables in a goto-function.
+/// Iterates over instructions in the specified function and replaces all values
+/// assigned to nondet-initializable static variables with nondeterministic
+/// values.
+/// \param ns Namespace for resolving type information.
+/// \param [out] goto_functions Existing goto-functions to be updated.
+/// \param fct_name Name of the goto-function to be updated.
 void nondet_static(
   const namespacet &ns,
   goto_functionst &goto_functions,
@@ -38,34 +82,17 @@ void nondet_static(
       const symbol_exprt &sym=to_symbol_expr(
           to_code_assign(instruction.code).lhs());
 
-      // is it a __CPROVER_* variable?
-      if(has_prefix(id2string(sym.get_identifier()), CPROVER_PREFIX))
-        continue;
-
-      // any other internal variable such as Java specific?
-      if(
-        ns.lookup(sym.get_identifier())
-          .type.get_bool(ID_C_no_nondet_initialization))
+      if(is_nondet_initializable_static(sym, ns))
       {
-        continue;
+        const goto_programt::instructiont original_instruction = instruction;
+        i_it->make_assignment();
+        i_it->code = code_assignt(
+          sym,
+          side_effect_expr_nondett(
+            sym.type(), original_instruction.source_location));
+        i_it->source_location = original_instruction.source_location;
+        i_it->function = original_instruction.function;
       }
-
-      // static lifetime?
-      if(!ns.lookup(sym.get_identifier()).is_static_lifetime)
-        continue;
-
-      // constant?
-      if(is_constant_or_has_constant_components(sym.type(), ns))
-        continue;
-
-      const goto_programt::instructiont original_instruction = instruction;
-      i_it->make_assignment();
-      i_it->code = code_assignt(
-        sym,
-        side_effect_expr_nondett(
-          sym.type(), original_instruction.source_location));
-      i_it->source_location = original_instruction.source_location;
-      i_it->function = original_instruction.function;
     }
     else if(instruction.is_function_call())
     {
@@ -78,6 +105,10 @@ void nondet_static(
   }
 }
 
+/// Nondeterministically initializes global scope variables in
+/// CPROVER_initialize function.
+/// \param ns Namespace for resolving type information.
+/// \param [out] goto_functions Existing goto-functions to be updated.
 void nondet_static(
   const namespacet &ns,
   goto_functionst &goto_functions)
@@ -88,6 +119,11 @@ void nondet_static(
   goto_functions.update();
 }
 
+/// Main entry point of the module. Nondeterministically initializes global
+/// scope variables, except for constants (such as string literals, final
+/// fields) and internal variables (such as CPROVER and symex variables,
+/// language specific internal variables).
+/// \param [out] goto_model Existing goto-model to be updated.
 void nondet_static(goto_modelt &goto_model)
 {
   const namespacet ns(goto_model.symbol_table);

src/goto-instrument/nondet_static.h

@@ -1,7 +1,9 @@
 /*******************************************************************\
 
-Module: Nondeterministic initialization of certain global scope
-        variables
+Module: Nondeterministically initializes global scope variables, except for
+ constants (such as string literals, final fields) and internal variables
+ (such as CPROVER and symex variables, language specific internal
+ variables).
 
 Author: Daniel Kroening, Michael Tautschnig
 
@@ -10,14 +12,22 @@ Date: November 2011
 \*******************************************************************/
 
 /// \file
-/// Nondeterministic initialization of certain global scope variables
+/// Nondeterministically initializes global scope variables, except for
+/// constants (such as string literals, final fields) and internal variables
+/// (such as CPROVER and symex variables, language specific internal
+/// variables).
 
 #ifndef CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
 #define CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
 
 class goto_modelt;
 class namespacet;
 class goto_functionst;
+class symbol_exprt;
+
+bool is_nondet_initializable_static(
+  const symbol_exprt &sym,
+  const namespacet &ns);
 
 void nondet_static(
   const namespacet &ns,