Merge pull request #3562 from smowton/smowton/feature/simplify-truncating-cast

Simplifier: transform ((struct A)x).field1 into x.a.b.field2

Author: tautschnig

jbmc/regression/jbmc/simplify-classid-of-interface/Impl1.class

@@ -0,0 +1,5 @@
+interface Intf {
+
+    public int f();
+
+}

jbmc/regression/jbmc/simplify-classid-of-interface/Impl1Sub.class

@@ -0,0 +1,64 @@
+
+public class Test {
+
+  public static void main() {
+
+    // The following line is only needed so that multiple possible callees
+    // for the interface Intf are found, and so a dispatch table
+    // (if i->@class_identfier == "Impl1" then ...) is generated.
+    Impl2 unused = new Impl2();
+
+    // This should be easily verified, as long as symex can determine that *i
+    // certainly refers to an instance of Impl1, and so i.f() is certainly a
+    // call to Impl1.f. This requires it to simplify the expression
+    // "((struct Intf)some_impl1_instance)[email protected].@class_identifier".
+    Intf i = new Impl1();
+    int got = i.f();
+    assert got == 1;
+
+  }
+
+  public static void main_derived_class() {
+
+    // This is just like the "main" method, except a class with a superclass
+    // is used, to check that the cast to struct Intf can be simplified even
+    // when the object doesn't directly have such a member (instead it has a
+    // member "@Impl1", which itself has a "@java.lang.Object").
+
+    Impl2 unused = new Impl2();
+
+    Intf i = new Impl1Sub();
+    int got = i.f();
+    assert got == 1;
+
+  }
+
+}
+
+class Impl1 implements Intf {
+
+  // This field is important-- without it, the structures of Impl1 and Intf
+  // are the same (both being simply { java.lang.Object @java.lang.Object }),
+  // which allows the expression simplifier to take an easier route than the one
+  // we intend to test.
+  public int x;
+
+  public int f() {
+    return 1;
+  }
+
+}
+
+class Impl1Sub extends Impl1 {
+
+  public int z;
+
+}
+
+class Impl2 implements Intf {
+
+  public int f() {
+    return 2;
+  }
+
+}

jbmc/regression/jbmc/simplify-classid-of-interface/Impl2.class

@@ -0,0 +1,15 @@
+CORE
+Test.class
+--function Test.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^Passing problem to
+^warning: ignoring
+--
+The "Passing problem to..." line is a sign that symex couldn't prove the
+assertion is valid by itself, which in turn probably indicates a weakness of the
+expression simplifier. The companion test_no_simplify.desc checks that the
+"Passing problem to" line is indeed present when we indeed resort to the SAT
+solver.

jbmc/regression/jbmc/simplify-classid-of-interface/Intf.class

@@ -0,0 +1,15 @@
+CORE
+Test.class
+--function Test.main_derived_class
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^Passing problem to
+^warning: ignoring
+--
+The "Passing problem to..." line is a sign that symex couldn't prove the
+assertion is valid by itself, which in turn probably indicates a weakness of the
+expression simplifier. The companion test_no_propagation.desc checks that the
+"Passing problem to" line is indeed present when we indeed resort to the SAT
+solver.

jbmc/regression/jbmc/simplify-classid-of-interface/Intf.java

@@ -0,0 +1,14 @@
+CORE
+Test.class
+--function Test.main --no-simplify --unwind 10
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^Passing problem to
+--
+^warning: ignoring
+--
+This is just to check the "Passing problem to" line is printed when the solver
+is invoked -- the real test (test.desc) depends on that to check that its test
+code was analysed entirely by goto-symex. If the output format changes this test
+should notice that.

jbmc/regression/jbmc/simplify-classid-of-interface/Test.class

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--function Test.main --no-simplify --unwind 10 --show-vcc
+^EXIT=0$
+^SIGNAL=0$
+"java::Impl1" = cast\(\{ \{ "java::Impl1"\}, 0\}, struct \{ struct \{ string @class_identifier \} @java.lang.Object \}\)\[email protected]\.@class_identifier
+--
+^warning: ignoring
+--
+This checks that the test generates the VCC testing the class-id that we're
+intending to simplify away in the main test.

jbmc/regression/jbmc/simplify-classid-of-interface/Test.java

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include "namespace.h"
 #include "pointer_offset_size.h"
 #include "std_expr.h"
+#include "type_eq.h"
 
 bool simplify_exprt::simplify_member(exprt &expr)
 {
@@ -240,6 +241,37 @@ bool simplify_exprt::simplify_member(exprt &expr)
       simplify_member(expr);
       return false;
     }
+
+    // Try to translate into an equivalent member (perhaps nested) of the type
+    // being cast (for example, this might turn ((struct A)x).field1 into
+    // x.substruct.othersubstruct.field2, if field1 and field2 have the same
+    // type and offset with respect to x.
+    if(op_type.id() == ID_struct)
+    {
+      optionalt<mp_integer> requested_offset =
+        member_offset(to_struct_type(op_type), component_name, ns);
+      if(requested_offset.has_value())
+      {
+        exprt equivalent_member = get_subexpression_at_offset(
+          op.op0(), *requested_offset, expr.type(), ns);
+
+        // Guess: turning this into a byte-extract operation is not really an
+        // optimisation.
+        // The type_eq check is because get_subexpression_at_offset uses
+        // base_type_eq, whereas in the context of a simplifier we should not
+        // change the type of the expression.
+        if(
+          equivalent_member.is_not_nil() &&
+          equivalent_member.id() != ID_byte_extract_little_endian &&
+          equivalent_member.id() != ID_byte_extract_big_endian &&
+          type_eq(equivalent_member.type(), expr.type(), ns))
+        {
+          expr = equivalent_member;
+          simplify_rec(expr);
+          return false;
+        }
+      }
+    }
   }
   else if(op.id()==ID_if)
   {