Make failed nondet Enum assignment non-fatal #4287
Conversation
smowton
requested review from
cesaro,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli and
thk123
as code owners
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 05fd4ef).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102518462
| @@ -1460,18 +1460,23 @@ void java_object_factoryt::gen_nondet_array_init( | |||
| /// expr = $VALUES[i]; | |||
| /// where $VALUES is a variable generated by the Java compiler that stores | |||
| /// the array that is returned by Enum.values(). | |||
| void java_object_factoryt::gen_nondet_enum_init( | |||
| /// This may fail if the $VALUES static field is not present, which gives the | |||
| /// possible values of a particular enum subtype. Ensuring that field is in the | |||
There was a problem hiding this comment.
⛏️ "which gives the..." <- a bit confusing to have the explanation of what $VALUES is split like that, maybe add this part to the previous sentence?
There was a problem hiding this comment.
Fixed this and added a warning message
smowton
force-pushed
the
smowton/fix/missing-enum-non-fatal
branch
from
81408c5 to
26fa790
Compare
|
@smowton clang-format and Doxygen are unhappy... |
| code_blockt &assignments, | ||
| const exprt &expr, | ||
| const java_class_typet &java_class_type, | ||
| const source_locationt &location) | ||
| { | ||
| const irep_idt &class_name = java_class_type.get_name(); | ||
| const irep_idt values_name = id2string(class_name) + ".$VALUES"; | ||
| INVARIANT( |
There was a problem hiding this comment.
💡 An exception might be clearer than a boolean here since it is an error condition, even if we do want to gracefully recover from it.
|
Approved prematurely - is there a test case we can add that exhibits this failure at the moment? |
|
@thk123 as far as I'm aware, not with JBMC, as the examples I know of require using test-gen's generic type substitution. |
smowton
force-pushed
the
smowton/fix/missing-enum-non-fatal
branch
from
26fa790 to
ff2a673
Compare
|
@smowton Fair - if you have a test case please send it my way and I'll integrate it into TG |
Previously we always expected an Enum type's VALUES array to be present if it may be created in a stub method. However while this is easy for a front-end to ensure when the Enum is a direct return type or member of a stub return type, there are other cases where the object factory can end up building a nondet Enum, such as generic type substitution and usage-inferred stub return types. Until (if ever) ci-lazy-methods can precisely mimic the object factory's behaviour, we're better off tolerating the case where the VALUES array remains missing than killing the entire run.
smowton
force-pushed
the
smowton/fix/missing-enum-non-fatal
branch
from
ff2a673 to
40d72fb
Compare
|
@thk123 here you go: public class Test {
public static void main() {
MyEnum e = (MyEnum)Stub.get();
}
}
class Stub {
public static Object get() { return null; }
}
enum MyEnum { } |
|
Of course delete |
Previously we always expected an Enum type's VALUES array to be present if it may be created in a
stub method. However while this is easy for a front-end to ensure when the Enum is a direct return
type or member of a stub return type, there are other cases where the object factory can end up
building a nondet Enum, such as generic type substitution and usage-inferred stub return types.
Until (if ever) ci-lazy-methods can precisely mimic the object factory's behaviour, we're better
off tolerating the case where the VALUES array remains missing than killing the entire run.