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

This will take place if field1 and field2 have matching types and offsets within
struct A and the original struct type of 'x'. This is particularly important for the Java
frontend, where Java like "Map m = new HashMap(); return m.size()" will generate GOTO that
extracts the class-identifier from a Map*, but Map* and HashMap* are likely not structurally
equivalent (HashMap might have a superclass other than Object, or have fields above those
posessed by Map (which is an interface in fact, so has none)).

That means value_set_dereferencet leaves us with an expression like
((Map)dynamic_object1).@java.lang.Object.@class_identifier, which the simplifier can now
handle, enabling symex to determine the actual type is HashMap and so avoid exploring code
that is in truth unreachable.

Author: smowton

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).@java.lang.Object.@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.