diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/Impl1.class b/jbmc/regression/jbmc/simplify-classid-of-interface/Impl1.class new file mode 100644 index 00000000000..25821a1fa11 Binary files /dev/null and b/jbmc/regression/jbmc/simplify-classid-of-interface/Impl1.class differ diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/Impl1Sub.class b/jbmc/regression/jbmc/simplify-classid-of-interface/Impl1Sub.class new file mode 100644 index 00000000000..6f74077c607 Binary files /dev/null and b/jbmc/regression/jbmc/simplify-classid-of-interface/Impl1Sub.class differ diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/Impl2.class b/jbmc/regression/jbmc/simplify-classid-of-interface/Impl2.class new file mode 100644 index 00000000000..936bc6c3c15 Binary files /dev/null and b/jbmc/regression/jbmc/simplify-classid-of-interface/Impl2.class differ diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/Intf.class b/jbmc/regression/jbmc/simplify-classid-of-interface/Intf.class new file mode 100644 index 00000000000..67b7fdd515f Binary files /dev/null and b/jbmc/regression/jbmc/simplify-classid-of-interface/Intf.class differ diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/Intf.java b/jbmc/regression/jbmc/simplify-classid-of-interface/Intf.java new file mode 100644 index 00000000000..2a1681e13f6 --- /dev/null +++ b/jbmc/regression/jbmc/simplify-classid-of-interface/Intf.java @@ -0,0 +1,5 @@ +interface Intf { + + public int f(); + +} diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/Test.class b/jbmc/regression/jbmc/simplify-classid-of-interface/Test.class new file mode 100644 index 00000000000..7c6cc3eeb96 Binary files /dev/null and b/jbmc/regression/jbmc/simplify-classid-of-interface/Test.class differ diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/Test.java b/jbmc/regression/jbmc/simplify-classid-of-interface/Test.java new file mode 100644 index 00000000000..c9e9055263c --- /dev/null +++ b/jbmc/regression/jbmc/simplify-classid-of-interface/Test.java @@ -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; + } + +} diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/test.desc b/jbmc/regression/jbmc/simplify-classid-of-interface/test.desc new file mode 100644 index 00000000000..a19b15a2ad2 --- /dev/null +++ b/jbmc/regression/jbmc/simplify-classid-of-interface/test.desc @@ -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. diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/test_derived_class.desc b/jbmc/regression/jbmc/simplify-classid-of-interface/test_derived_class.desc new file mode 100644 index 00000000000..e6500364790 --- /dev/null +++ b/jbmc/regression/jbmc/simplify-classid-of-interface/test_derived_class.desc @@ -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. diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify.desc b/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify.desc new file mode 100644 index 00000000000..eccaaa84642 --- /dev/null +++ b/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify.desc @@ -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. diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc b/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc new file mode 100644 index 00000000000..2fc1c821c29 --- /dev/null +++ b/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc @@ -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 \}\)\.@java.lang.Object\.@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. diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp index 2d11add8273..1e162ce03cc 100644 --- a/src/util/simplify_expr_struct.cpp +++ b/src/util/simplify_expr_struct.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #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 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) {