Remove language_mode from goto_symext

`goto_symex_statet` holds a reference to a language mode, which was
being initialised to `goto_symext::language_mode` in
`goto_symext::initialize_entry_point_state`. That `goto_symext` object,
however, may be the one created in
`single_path_symex_only_checkert::initialize_worklist`, whereupon the
`goto_symex_statet` will outlive it.

Fix this problem by getting rid of the `language_mode` member of
`goto_symext` and initialise `goto_symex_statet::language_mode` from a
mode in the symbol table, which outlives all goto-symex objects.

Author: tautschnig

src/goto-checker/symex_bmc.cpp

@@ -16,8 +16,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/unwindset.h>
 
-#include <linking/static_lifetime_init.h>
-
 #include <limits>
 
 symex_bmct::symex_bmct(
@@ -40,10 +38,6 @@ symex_bmct::symex_bmct(
     unwindset(unwindset),
     symex_coverage(ns)
 {
-  const symbolt *init_symbol = outer_symbol_table.lookup(INITIALIZE_FUNCTION);
-  if(init_symbol)
-    language_mode = init_symbol->mode;
-
   messaget msg{mh};
   msg.status() << "Starting Bounded Model Checking" << messaget::eom;
 }

src/goto-symex/goto_symex.cpp

@@ -36,7 +36,7 @@ void goto_symext::do_simplify(exprt &expr, const statet &state)
   {
     if(state.threads.size() == 1)
     {
-      simplify_expr_with_value_sett{state.value_set, language_mode, ns}
+      simplify_expr_with_value_sett{state.value_set, state.language_mode, ns}
         .simplify(expr);
     }
     else
@@ -113,13 +113,7 @@ void goto_symext::symex_assign(
       assignment_type = symex_targett::assignment_typet::HIDDEN;
 
     symex_assignt symex_assign{
-      shadow_memory,
-      state,
-      assignment_type,
-      ns,
-      symex_config,
-      language_mode,
-      target};
+      shadow_memory, state, assignment_type, ns, symex_config, target};
 
     // Try to constant propagate potential side effects of the assignment, when
     // simplification is turned on and there is one thread only. Constant
@@ -149,13 +143,7 @@ void goto_symext::symex_assign(
 
     exprt::operandst lhs_if_then_else_conditions;
     symex_assignt{
-      shadow_memory,
-      state,
-      assignment_type,
-      ns,
-      symex_config,
-      language_mode,
-      target}
+      shadow_memory, state, assignment_type, ns, symex_config, target}
       .assign_rec(lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions);
 
     if(need_atomic_section)

src/goto-symex/goto_symex.h

@@ -235,10 +235,6 @@ class goto_symext
   messaget::mstreamt &
   print_callstack_entry(const symex_targett::sourcet &target);
 
-  /// language_mode: ID_java, ID_C or another language identifier
-  /// if we know the source language in use, irep_idt() otherwise.
-  irep_idt language_mode;
-
   /// The symbol table associated with the goto-program being executed.
   /// This symbol table will not have objects that are dynamically created as
   /// part of symbolic execution added to it; those object are stored in the

src/goto-symex/goto_symex_state.h

@@ -258,8 +258,11 @@ class goto_symex_statet final : public goto_statet
            lvalue.id() == ID_array;
   }
 
-private:
+  /// language_mode: ID_java, ID_C or another language identifier
+  /// if we know the source language in use, irep_idt() otherwise.
   const irep_idt &language_mode;
+
+private:
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
 
   /// \brief Dangerous, do not use

src/goto-symex/symex_assign.cpp

@@ -207,8 +207,8 @@ void symex_assignt::assign_non_struct_symbol(
 
   if(symex_config.simplify_opt)
   {
-    simplify_expr_with_value_sett{state.value_set, language_mode, ns}.simplify(
-      assignment.rhs);
+    simplify_expr_with_value_sett{state.value_set, state.language_mode, ns}
+      .simplify(assignment.rhs);
   }
 
   const ssa_exprt l2_lhs = state

src/goto-symex/symex_assign.h

@@ -33,14 +33,12 @@ class symex_assignt
     symex_targett::assignment_typet assignment_type,
     const namespacet &ns,
     const symex_configt &symex_config,
-    const irep_idt &language_mode,
     symex_targett &target)
     : shadow_memory(shadow_memory),
       state(state),
       assignment_type(assignment_type),
       ns(ns),
       symex_config(symex_config),
-      language_mode(language_mode),
       target(target)
   {
   }
@@ -67,7 +65,6 @@ class symex_assignt
   symex_targett::assignment_typet assignment_type;
   const namespacet &ns;
   const symex_configt &symex_config;
-  const irep_idt &language_mode;
   symex_targett ⌖
 
   void assign_from_struct(

src/goto-symex/symex_builtin_functions.cpp

@@ -72,8 +72,8 @@ void goto_symext::symex_allocate(
   {
     // to allow constant propagation
     exprt tmp_size = state.rename(size, ns).get();
-    simplify_expr_with_value_sett{state.value_set, language_mode, ns}.simplify(
-      tmp_size);
+    simplify_expr_with_value_sett{state.value_set, state.language_mode, ns}
+      .simplify(tmp_size);
 
     // special treatment for sizeof(T)*x
     {
@@ -167,8 +167,8 @@ void goto_symext::symex_allocate(
 
   // to allow constant propagation
   exprt zero_init = state.rename(to_binary_expr(code).op1(), ns).get();
-  simplify_expr_with_value_sett{state.value_set, language_mode, ns}.simplify(
-    zero_init);
+  simplify_expr_with_value_sett{state.value_set, state.language_mode, ns}
+    .simplify(zero_init);
 
   INVARIANT(
     zero_init.is_constant(), "allocate expects constant as second argument");
@@ -433,7 +433,7 @@ void goto_symext::symex_printf(
   }
 
   const irep_idt format_string =
-    get_string_argument(operands[0], state.value_set, language_mode, ns);
+    get_string_argument(operands[0], state.value_set, state.language_mode, ns);
 
   if(!format_string.empty())
     target.output_fmt(
@@ -459,7 +459,7 @@ void goto_symext::symex_input(
   }
 
   const irep_idt input_id =
-    get_string_argument(id_arg, state.value_set, language_mode, ns);
+    get_string_argument(id_arg, state.value_set, state.language_mode, ns);
 
   target.input(state.guard.as_expr(), state.source, input_id, args);
 }
@@ -478,14 +478,15 @@ void goto_symext::symex_output(
     renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
     if(symex_config.simplify_opt)
     {
-      simplify_expr_with_value_sett simp{state.value_set, language_mode, ns};
+      simplify_expr_with_value_sett simp{
+        state.value_set, state.language_mode, ns};
       l2_arg.simplify(simp);
     }
     args.emplace_back(l2_arg);
   }
 
   const irep_idt output_id =
-    get_string_argument(id_arg, state.value_set, language_mode, ns);
+    get_string_argument(id_arg, state.value_set, state.language_mode, ns);
 
   target.output(state.guard.as_expr(), state.source, output_id, args);
 }

src/goto-symex/symex_clean_expr.cpp

@@ -127,7 +127,7 @@ void goto_symext::process_array_expr(statet &state, exprt &expr)
     ns,
     state.symbol_table,
     symex_dereference_state,
-    language_mode,
+    state.language_mode,
     false,
     log.get_message_handler());
 
@@ -187,7 +187,6 @@ void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
     symex_targett::assignment_typet::HIDDEN,
     ns,
     symex_config,
-    language_mode,
     target}
     .assign_symbol(
       to_ssa_expr(state.rename<L1>(let_expr.symbol(), ns).get()),

src/goto-symex/symex_dereference.cpp

@@ -220,7 +220,7 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state)
                              "symex",
                              "dereference_cache",
                              dereference_result.source_location(),
-                             language_mode,
+                             state.language_mode,
                              ns,
                              state.symbol_table)
                              .symbol_expr();
@@ -236,7 +236,6 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state)
     symex_targett::assignment_typet::STATE,
     ns,
     symex_config,
-    language_mode,
     target};
 
   assign.assign_symbol(
@@ -328,7 +327,7 @@ void goto_symext::dereference_rec(
       ns,
       state.symbol_table,
       symex_dereference_state,
-      language_mode,
+      state.language_mode,
       expr_is_not_null,
       log.get_message_handler());
 

src/goto-symex/symex_function_call.cpp

@@ -131,13 +131,7 @@ void goto_symext::parameter_assignments(
 
       exprt::operandst lhs_conditions;
       symex_assignt{
-        shadow_memory,
-        state,
-        assignment_type,
-        ns,
-        symex_config,
-        language_mode,
-        target}
+        shadow_memory, state, assignment_type, ns, symex_config, target}
         .assign_rec(lhs, expr_skeletont{}, rhs, lhs_conditions);
     }