Fix based on comments

Author: Petr Bauch

src/cbmc/bmc.cpp

@@ -637,11 +637,6 @@ int bmct::do_language_agnostic_bmc(
 void bmct::perform_symbolic_execution(
   goto_symext::get_goto_functiont get_goto_function)
 {
-  if(options.get_bool_option("validate-ssa-equation"))
-  {
-    symex.global_validation_mode = validation_modet::INVARIANT;
-  }
-
   symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
 
   if(options.get_bool_option("validate-ssa-equation"))

src/goto-symex/goto_symex.h

@@ -77,7 +77,7 @@ class goto_symext
       path_segment_vccs(0),
       _total_vccs(std::numeric_limits<unsigned>::max()),
       _remaining_vccs(std::numeric_limits<unsigned>::max()),
-      global_validation_mode(validation_modet::IGNORE)
+      run_validation_checks(options.get_bool_option("validate-ssa-equation"))
   {
   }
 
@@ -524,7 +524,7 @@ class goto_symext
   {
     target.validate(ns, vm);
   }
-  validation_modet global_validation_mode;
+  bool run_validation_checks;
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H

src/goto-symex/goto_symex_state.cpp

@@ -30,9 +30,7 @@ goto_symex_statet::goto_symex_statet()
     total_vccs(0),
     remaining_vccs(0),
     record_events(true),
-    dirty(),
-    global_validation_mode(validation_modet::IGNORE)
-
+    dirty()
 {
   threads.resize(1);
   new_frame();
@@ -217,16 +215,19 @@ void goto_symex_statet::assignment(
   // the type might need renaming
   rename(lhs.type(), l1_identifier, ns);
   lhs.update_type();
-  const validation_modet vm = global_validation_mode;
-  DATA_CHECK(!check_renaming_l1(lhs), "lhs renaming failed on l1");
-
+  const validation_modet local_validation_mode = validation_modet::INVARIANT;
+  if(run_validation_checks)
+  {
+    const validation_modet vm = local_validation_mode;
+    DATA_CHECK(!check_renaming_l1(lhs), "lhs renaming failed on l1");
+  }
 #if 0
   PRECONDITION(l1_identifier != get_original_name(l1_identifier)
       || l1_identifier=="goto_symex::\\guard"
       || ns.lookup(l1_identifier).is_shared()
       || has_prefix(id2string(l1_identifier), "symex::invalid_object")
       || has_prefix(id2string(l1_identifier), "symex_dynamic::dynamic_object"));
-  #endif
+#endif
 
   // do the l2 renaming
   if(level2.current_names.find(l1_identifier)==level2.current_names.end())
@@ -237,9 +238,12 @@ void goto_symex_statet::assignment(
   // in case we happen to be multi-threaded, record the memory access
   bool is_shared=l2_thread_write_encoding(lhs, ns);
 
-  DATA_CHECK(!check_renaming(lhs), "lhs renaming failed on l2");
-  DATA_CHECK(!check_renaming(rhs), "rhs renaming failed on l2");
-
+  if(run_validation_checks)
+  {
+    const validation_modet vm = local_validation_mode;
+    DATA_CHECK(!check_renaming(lhs), "lhs renaming failed on l2");
+    DATA_CHECK(!check_renaming(rhs), "rhs renaming failed on l2");
+  }
   // see #305 on GitHub for a simple example and possible discussion
   if(is_shared && lhs.type().id() == ID_pointer && !allow_pointer_unsoundness)
     throw unsupported_operation_exceptiont(
@@ -261,8 +265,12 @@ void goto_symex_statet::assignment(
     ssa_exprt l1_lhs(lhs);
     get_l1_name(l1_lhs);
 
-    DATA_CHECK(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
-    DATA_CHECK(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
+    if(run_validation_checks)
+    {
+      const validation_modet vm = local_validation_mode;
+      DATA_CHECK(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
+      DATA_CHECK(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
+    }
 
     value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
   }

src/goto-symex/goto_symex_state.h

@@ -43,7 +43,6 @@ class goto_symex_statet final
     : goto_symex_statet(other) // NOLINT
   {
     symex_target = target;
-    global_validation_mode = other.global_validation_mode;
   }
 
   /// contains symbols that are minted during symbolic execution, such as
@@ -391,7 +390,7 @@ class goto_symex_statet final
   /// of a GOTO
   bool has_saved_next_instruction;
   bool saved_target_is_backwards;
-  validation_modet global_validation_mode;
+  bool run_validation_checks;
 
 private:
   /// \brief Dangerous, do not use

src/goto-symex/symex_main.cpp

@@ -301,7 +301,7 @@ void goto_symext::symex_from_entry_point_of(
 
   statet state;
 
-  state.global_validation_mode = global_validation_mode;
+  state.run_validation_checks = run_validation_checks;
 
   initialize_entry_point(
     state,

src/util/validate.h

@@ -36,8 +36,6 @@ Author: Daniel Poetzl
       if(!(condition))                                                         \
         throw incorrect_goto_program_exceptiont(message);                      \
       break;                                                                   \
-    case validation_modet::IGNORE:                                             \
-      break;                                                                   \
     }                                                                          \
   } while(0)
 
@@ -58,8 +56,6 @@ Author: Daniel Poetzl
       if(!(condition))                                                         \
         throw incorrect_goto_program_exceptiont(message, __VA_ARGS__);         \
       break;                                                                   \
-    case validation_modet::IGNORE:                                             \
-      break;                                                                   \
     }                                                                          \
   } while(0)
 

src/util/validation_mode.h

@@ -12,8 +12,7 @@ Author: Daniel Poetzl
 enum class validation_modet
 {
   INVARIANT,
-  EXCEPTION,
-  IGNORE
+  EXCEPTION
 };
 
 #endif /* CPROVER_UTIL_VALIDATION_MODE_H */