Merge pull request #5691 from tautschnig/is_ssa_expr

Use is_ssa_expr to avoid lower-level get_bool(ID_C_SSA_symbol)

Author: tautschnig

src/goto-symex/auto_objects.cpp

@@ -78,7 +78,7 @@ void goto_symext::initialize_auto_object(const exprt &expr, statet &state)
 void goto_symext::trigger_auto_object(const exprt &expr, statet &state)
 {
   expr.visit_pre([&state, this](const exprt &e) {
-    if(e.id() == ID_symbol && e.get_bool(ID_C_SSA_symbol))
+    if(is_ssa_expr(e))
     {
       const ssa_exprt &ssa_expr = to_ssa_expr(e);
       const irep_idt &obj_identifier = ssa_expr.get_object_name();

src/goto-symex/field_sensitivity.cpp

@@ -33,7 +33,7 @@ exprt field_sensitivityt::apply(
       *it = apply(ns, state, std::move(*it), write);
   }
 
-  if(expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol) && !write)
+  if(is_ssa_expr(expr) && !write)
   {
     return get_fields(ns, state, to_ssa_expr(expr));
   }
@@ -59,8 +59,7 @@ exprt field_sensitivityt::apply(
     member_exprt &member = to_member_expr(expr);
 
     if(
-      member.struct_op().id() == ID_symbol &&
-      member.struct_op().get_bool(ID_C_SSA_symbol) &&
+      is_ssa_expr(member.struct_op()) &&
       (member.struct_op().type().id() == ID_struct ||
        member.struct_op().type().id() == ID_struct_tag))
     {
@@ -88,9 +87,7 @@ exprt field_sensitivityt::apply(
     simplify(index.index(), ns);
 
     if(
-      index.array().id() == ID_symbol &&
-      index.array().get_bool(ID_C_SSA_symbol) &&
-      index.array().type().id() == ID_array &&
+      is_ssa_expr(index.array()) && index.array().type().id() == ID_array &&
       index.index().id() == ID_constant)
     {
       // place the entire index expression, not just the array operand, in an
@@ -252,7 +249,7 @@ void field_sensitivityt::field_assignments_rec(
 {
   if(lhs == lhs_fs)
     return;
-  else if(lhs_fs.id() == ID_symbol && lhs_fs.get_bool(ID_C_SSA_symbol))
+  else if(is_ssa_expr(lhs_fs))
   {
     exprt ssa_rhs = state.rename(lhs, ns).get();
     simplify(ssa_rhs, ns);

src/goto-symex/goto_symex_state.cpp

@@ -178,8 +178,7 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
       level == L2,
     "must handle all renaming levels");
 
-  if(expr.id()==ID_symbol &&
-     expr.get_bool(ID_C_SSA_symbol))
+  if(is_ssa_expr(expr))
   {
     exprt original_expr = expr;
     ssa_exprt &ssa=to_ssa_expr(expr);
@@ -546,8 +545,7 @@ bool goto_symex_statet::l2_thread_write_encoding(
 template <levelt level>
 void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
 {
-  if(expr.id()==ID_symbol &&
-     expr.get_bool(ID_C_SSA_symbol))
+  if(is_ssa_expr(expr))
   {
     ssa_exprt &ssa=to_ssa_expr(expr);
 
@@ -751,8 +749,7 @@ static void get_l1_name(exprt &expr)
 {
   // do not reset the type !
 
-  if(expr.id()==ID_symbol &&
-     expr.get_bool(ID_C_SSA_symbol))
+  if(is_ssa_expr(expr))
     to_ssa_expr(expr).remove_level_2();
   else
     Forall_operands(it, expr)
@@ -846,7 +843,7 @@ ssa_exprt goto_symex_statet::declare(ssa_exprt ssa, const namespacet &ns)
   record_events.push(false);
   exprt expr_l2 = rename(std::move(ssa), ns).get();
   INVARIANT(
-    expr_l2.id() == ID_symbol && expr_l2.get_bool(ID_C_SSA_symbol),
+    is_ssa_expr(expr_l2),
     "symbol to declare should not be replaced by constant propagation");
   ssa = to_ssa_expr(expr_l2);
   record_events.pop();

src/goto-symex/postcondition.cpp

@@ -148,8 +148,7 @@ bool postconditiont::is_used(
   {
     return is_used_address_of(to_address_of_expr(expr).object(), identifier);
   }
-  else if(expr.id()==ID_symbol &&
-          expr.get_bool(ID_C_SSA_symbol))
+  else if(is_ssa_expr(expr))
   {
     return to_ssa_expr(expr).get_object_name()==identifier;
   }

src/goto-symex/renaming_level.cpp

@@ -157,7 +157,7 @@ exprt get_original_name(exprt expr)
 {
   expr.type() = get_original_name(std::move(expr.type()));
 
-  if(expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol))
+  if(is_ssa_expr(expr))
     return to_ssa_expr(expr).get_original_expr();
   else
   {

src/goto-symex/symex_assign.cpp

@@ -38,7 +38,7 @@ void symex_assignt::assign_rec(
   const exprt &rhs,
   exprt::operandst &guard)
 {
-  if(lhs.id() == ID_symbol && lhs.get_bool(ID_C_SSA_symbol))
+  if(is_ssa_expr(lhs))
   {
     assign_symbol(to_ssa_expr(lhs), full_lhs, rhs, guard);
   }

src/goto-symex/symex_clean_expr.cpp

@@ -60,9 +60,8 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
     expr.swap(tmp);
     process_array_expr(expr, do_simplify, ns);
   }
-  else if(expr.id()==ID_symbol &&
-          expr.get_bool(ID_C_SSA_symbol) &&
-          to_ssa_expr(expr).get_original_expr().id()==ID_index)
+  else if(
+    is_ssa_expr(expr) && to_ssa_expr(expr).get_original_expr().id() == ID_index)
   {
     const ssa_exprt &ssa=to_ssa_expr(expr);
     const index_exprt &index_expr=to_index_expr(ssa.get_original_expr());

src/goto-symex/symex_dereference.cpp

@@ -139,8 +139,7 @@ exprt goto_symext::address_arithmetic(
 
     // handle field-sensitive SSA symbol
     mp_integer offset=0;
-    if(expr.id()==ID_symbol &&
-       expr.get_bool(ID_C_SSA_symbol))
+    if(is_ssa_expr(expr))
     {
       auto offset_opt = compute_pointer_offset(expr, ns);
       PRECONDITION(offset_opt.has_value());

src/goto-symex/symex_dereference_state.cpp

@@ -30,8 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com
 const symbolt *
 symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
 {
-  if(expr.id()==ID_symbol &&
-     expr.get_bool(ID_C_SSA_symbol))
+  if(is_ssa_expr(expr))
   {
     const ssa_exprt &ssa_expr=to_ssa_expr(expr);
     if(ssa_expr.get_original_expr().id()!=ID_symbol)

src/util/validate_expressions.cpp

@@ -33,7 +33,7 @@ void call_on_expr(const exprt &expr, Args &&... args)
   {
     CALL_ON_EXPR(plus_exprt);
   }
-  else if(expr.get_bool(ID_C_SSA_symbol))
+  else if(is_ssa_expr(expr))
   {
     CALL_ON_EXPR(ssa_exprt);
   }