Do not use base_type_eq with non-code types [blocks: #4056]

jbmc/regression/jbmc-generics/constant_propagation/Test.java

@@ -0,0 +1,27 @@
+public class Test {
+  public static void main() {
+    Generic<Integer> g = new GenericSub<Integer>();
+
+    int x = 0;
+    for(int i = 0; i < 1000; ++i)
+      x += g.get();
+
+    assert x == 0;
+  }
+}
+
+class Generic<T> {
+  T key;
+  int x;
+
+  public int get() { return 0; }
+
+  public Generic() {
+    key = null;
+    x = 5;
+  }
+}
+
+class GenericSub<S> extends Generic<S> {
+  public int get() { return x; }
+}

jbmc/regression/jbmc-generics/constant_propagation/test.desc

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.main --show-vcc
+^EXIT=0$
+^SIGNAL=0$
+^\{-\d+\} symex_dynamic::dynamic_object1#3 = \{ \{ \{ "java::GenericSub" \}, NULL, 0 \} \}$
+^\{-\d+\} symex_dynamic::dynamic_object1#4 = \{ \{ \{ "java::GenericSub" \}, NULL, 5 \} \}$
+--
+byte_extract_(big|little)_endian
+--
+The use of generics should not result in any byte_extract operations being
+generated for this test.

jbmc/unit/java-testing-utils/require_type.cpp

@@ -9,7 +9,6 @@ Author: Diffblue Ltd.
 #include "require_type.h"
 
 #include <testing-utils/use_catch.h>
-#include <util/base_type.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 
@@ -26,10 +25,8 @@ pointer_typet require_type::require_pointer(
   const pointer_typet &pointer = to_pointer_type(type);
 
   if(subtype)
-  {
-    namespacet ns{symbol_tablet{}};
-    base_type_eq(pointer.subtype(), subtype.value(), ns);
-  }
+    REQUIRE(pointer.subtype() == subtype.value());
+
   return pointer;
 }
 

regression/cbmc/Pointer_byte_extract4/program-only.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+: dynamic_object1#\d+\) WITH
+--
+The above pattern makes sure we don't have a conditional choice of objects
+within a "with" expression. We avoid having this by running the simplifier after
+dereferencing.

src/analyses/constant_propagator.cpp

@@ -17,7 +17,6 @@ Author: Peter Schrammel
 #endif
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
@@ -103,7 +102,7 @@ void constant_propagator_domaint::assign_rec(
     if(dest_values.is_constant(tmp))
     {
       DATA_INVARIANT(
-        base_type_eq(ns.lookup(s).type, tmp.type(), ns),
+        ns.lookup(s).type == tmp.type(),
         "type of constant to be replaced should match");
       dest_values.set_to(s, tmp);
     }
@@ -624,7 +623,7 @@ bool constant_propagator_domaint::valuest::meet(
     {
       const typet &m_id_type = ns.lookup(m.first).type;
       DATA_INVARIANT(
-        base_type_eq(m_id_type, m.second.type(), ns),
+        m_id_type == m.second.type(),
         "type of constant to be stored should match");
       set_to(symbol_exprt(m.first, m_id_type), m.second);
       changed=true;

src/goto-instrument/dump_c.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "dump_c.h"
 
-#include <util/base_type.h>
 #include <util/config.h>
 #include <util/find_symbols.h>
 #include <util/invariant.h>
@@ -1277,9 +1276,9 @@ void dump_ct::cleanup_expr(exprt &expr)
       expr.swap(tmp);
     }
   }
-  else if(expr.id()==ID_typecast &&
-      expr.op0().id()==ID_typecast &&
-      base_type_eq(expr.type(), expr.op0().type(), ns))
+  else if(
+    expr.id() == ID_typecast && expr.op0().id() == ID_typecast &&
+    expr.type() == expr.op0().type())
   {
     exprt tmp=expr.op0();
     expr.swap(tmp);
@@ -1309,8 +1308,7 @@ void dump_ct::cleanup_expr(exprt &expr)
           if(type.id()==ID_union &&
              type.get_bool(ID_C_transparent_union))
           {
-            if(it2->id()==ID_typecast &&
-               base_type_eq(it2->type(), type, ns))
+            if(it2->id() == ID_typecast && it2->type() == type)
               *it2=to_typecast_expr(*it2).op();
 
             // add a typecast for NULL or 0

src/goto-programs/goto_inline_class.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #endif
 
-#include <util/base_type.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
@@ -83,7 +82,7 @@ void goto_inlinet::parameter_assignments(
     {
       // it should be the same exact type as the parameter,
       // subject to some exceptions
-      if(!base_type_eq(parameter_type, actual.type(), ns))
+      if(parameter_type != actual.type())
       {
         const typet &f_partype = parameter_type;
         const typet &f_acttype = actual.type();

src/goto-programs/goto_program.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <ostream>
 #include <iomanip>
 
+#include <util/base_type.h>
 #include <util/expr_iterator.h>
 #include <util/find_symbols.h>
 #include <util/invariant.h>
@@ -715,10 +716,9 @@ void goto_programt::instructiont::validate(
             // Return removal sets the return type of a function symbol table
             // entry to 'void', but some callsites still expect the original
             // type (e.g. if a function is passed as a parameter)
-            symbol_expr_type_matches_symbol_table = base_type_eq(
-              goto_symbol_expr.type(),
-              original_return_type(ns.get_symbol_table(), goto_id),
-              ns);
+            symbol_expr_type_matches_symbol_table =
+              goto_symbol_expr.type() ==
+              original_return_type(ns.get_symbol_table(), goto_id);
 
             if(
               !symbol_expr_type_matches_symbol_table &&
@@ -760,8 +760,8 @@ void goto_programt::instructiont::validate(
               auto symbol_table_array_type = to_array_type(table_symbol->type);
               symbol_table_array_type.size() = nil_exprt();
 
-              symbol_expr_type_matches_symbol_table = base_type_eq(
-                goto_symbol_expr.type(), symbol_table_array_type, ns);
+              symbol_expr_type_matches_symbol_table =
+                goto_symbol_expr.type() == symbol_table_array_type;
             }
           }
 

src/goto-programs/graphml_witness.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening
 
 #include "graphml_witness.h"
 
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/arith_tools.h>
@@ -75,8 +74,9 @@ std::string graphml_witnesst::convert_assign_rec(
   {
     // dereferencing may have resulted in an lhs that is the first
     // struct member; undo this
-    if(assign.lhs().id()==ID_member &&
-       !base_type_eq(assign.lhs().type(), assign.rhs().type(), ns))
+    if(
+      assign.lhs().id() == ID_member &&
+      assign.lhs().type() != assign.rhs().type())
     {
       code_assignt tmp=assign;
       tmp.lhs()=to_member_expr(assign.lhs()).struct_op();

src/goto-programs/wp.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/std_expr.h>
 #include <util/std_code.h>
-#include <util/base_type.h>
 
 #include <util/invariant.h>
 
@@ -79,7 +78,7 @@ aliasingt aliasing(
     return aliasing(e1, e2.op0().op0(), ns);
 
   // fairly radical. Ignores struct prefixes and the like.
-  if(!base_type_eq(e1.type(), e2.type(), ns))
+  if(e1.type() != e2.type())
     return aliasingt::A_MUSTNOT;
 
   // syntactically the same?

src/goto-symex/symex_assign.cpp

@@ -27,8 +27,7 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
   exprt rhs=code.rhs();
 
   DATA_INVARIANT(
-    base_type_eq(lhs.type(), rhs.type(), ns),
-    "assignments must be type consistent");
+    lhs.type() == rhs.type(), "assignments must be type consistent");
 
   clean_expr(lhs, state, true);
   clean_expr(rhs, state, false);

src/goto-symex/symex_clean_expr.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include "goto_symex.h"
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
@@ -37,7 +36,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
     process_array_expr(if_expr.true_case(), do_simplify, ns);
     process_array_expr(if_expr.false_case(), do_simplify, ns);
 
-    if(!base_type_eq(if_expr.true_case(), if_expr.false_case(), ns))
+    if(if_expr.true_case() != if_expr.false_case())
     {
       byte_extract_exprt be(
         byte_extract_id(),

src/goto-symex/symex_dereference.cpp

@@ -12,10 +12,10 @@ Author: Daniel Kroening, [email protected]
 #include "goto_symex.h"
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
+#include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
 
@@ -60,7 +60,7 @@ exprt goto_symext::address_arithmetic(
 
       // turn &a of type T[i][j] into &(a[0][0])
       for(const typet *t = &(a.type().subtype());
-          t->id() == ID_array && !base_type_eq(expr.type(), *t, ns);
+          t->id() == ID_array && expr.type() != *t;
           t = &(t->subtype()))
         a.object()=index_exprt(a.object(), from_integer(0, index_type()));
     }
@@ -183,9 +183,10 @@ exprt goto_symext::address_arithmetic(
       "goto_symext::address_arithmetic does not handle " + expr.id_string());
 
   const typet &expr_type = expr.type();
-  INVARIANT((expr_type.id()==ID_array && !keep_array) ||
-            base_type_eq(pointer_type(expr_type), result.type(), ns),
-            "either non-persistent array or pointer to result");
+  INVARIANT(
+    (expr_type.id() == ID_array && !keep_array) ||
+      pointer_type(expr_type) == result.type(),
+    "either non-persistent array or pointer to result");
 
   return result;
 }
@@ -285,12 +286,11 @@ void goto_symext::dereference_rec(exprt &expr, statet &state)
     exprt &tc_op=to_typecast_expr(expr).op();
 
     // turn &array into &array[0] when casting to pointer-to-element-type
-    if(tc_op.id()==ID_address_of &&
-       to_address_of_expr(tc_op).object().type().id()==ID_array &&
-       base_type_eq(
-         expr.type(),
-         pointer_type(to_address_of_expr(tc_op).object().type().subtype()),
-         ns))
+    if(
+      tc_op.id() == ID_address_of &&
+      to_address_of_expr(tc_op).object().type().id() == ID_array &&
+      expr.type() ==
+        pointer_type(to_address_of_expr(tc_op).object().type().subtype()))
     {
       expr=
         address_of_exprt(
@@ -363,4 +363,30 @@ void goto_symext::dereference(exprt &expr, statet &state)
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
   expr = state.rename<L1>(std::move(l1_expr), ns);
+
+  // Dereferencing is likely to introduce new member-of-if constructs --
+  // for example, "x->field" may have become "(x == &o1 ? o1 : o2).field."
+  // Run expression simplification, which converts that to
+  // (x == &o1 ? o1.field : o2.field))
+  // before applying field sensitivity. Field sensitivity can then turn such
+  // field-of-symbol expressions into atomic SSA expressions instead of having
+  // to rewrite all of 'o1' otherwise.
+  // Even without field sensitivity this can be beneficial: for example,
+  // "(b ? s1 : s2).member := X" results in
+  // (b ? s1 : s2) := (b ? s1 : s2) with (member := X)
+  // and then
+  // s1 := b ? ((b ? s1 : s2) with (member := X)) : s1
+  // when all we need is
+  // s1 := s1 with (member := X) [and guard b]
+  // s2 := s2 with (member := X) [and guard !b]
+  do_simplify(expr);
+
+  if(symex_config.run_validation_checks)
+  {
+    // make sure simplify has not re-introduced any dereferencing that
+    // had previously been cleaned away
+    INVARIANT(
+      !has_subexpr(expr, ID_dereference),
+      "simplify re-introduced dereferencing");
+  }
 }

src/goto-symex/symex_function_call.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include "goto_symex.h"
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
@@ -79,7 +78,7 @@ void goto_symext::parameter_assignments(
     else
     {
       // It should be the same exact type.
-      if(!base_type_eq(parameter_type, rhs.type(), ns))
+      if(parameter_type != rhs.type())
       {
         const typet &rhs_type = rhs.type();
 

src/goto-symex/symex_other.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include "goto_symex.h"
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/pointer_offset_size.h>
@@ -149,7 +148,7 @@ void goto_symext::symex_other(
     process_array_expr(state, src_array);
 
     // check for size (or type) mismatch and adjust
-    if(!base_type_eq(dest_array.type(), src_array.type(), ns))
+    if(dest_array.type() != src_array.type())
     {
       if(statement==ID_array_copy)
       {
@@ -217,7 +216,7 @@ void goto_symext::symex_other(
 
     const array_typet &array_type = to_array_type(array_expr.type());
 
-    if(!base_type_eq(array_type.subtype(), value.type(), ns))
+    if(array_type.subtype() != value.type())
       value = typecast_exprt(value, array_type.subtype());
 
     code_assignt assignment(array_expr, array_of_exprt(value, array_type));
@@ -250,7 +249,7 @@ void goto_symext::symex_other(
     code_assignt assignment(code.op2(), equal_exprt(array1, array2));
 
     // check for size (or type) mismatch
-    if(!base_type_eq(array1.type(), array2.type(), ns))
+    if(array1.type() != array2.type())
       assignment.lhs() = false_exprt();
 
     symex_assign(state, assignment);

src/goto-symex/symex_target_equation.cpp

@@ -940,7 +940,7 @@ void symex_target_equationt::SSA_stept::validate(
     validate_full_expr(ssa_rhs, ns, vm);
     DATA_CHECK(
       vm,
-      base_type_eq(ssa_lhs.get_original_expr().type(), ssa_rhs.type(), ns),
+      ssa_lhs.get_original_expr().type() == ssa_rhs.type(),
       "Type inequality in SSA assignment\nlhs-type: " +
         ssa_lhs.get_original_expr().type().id_string() +
         "\nrhs-type: " + ssa_rhs.type().id_string());