Symbolic Enum classes

[GAJaloyan]

Hi, thanks for the great tool, I've been trying to play with it on some complex tree-like datastructures, and it seems really promising.

More specifically, I'm having some trouble with trying to use symbolic enum classes. I have a structure (Main$MyStruct) with several fields, out of which one is of class Main$MyEnum which is an enum (thus has fields ordinal and name)

Class[(2, Main$MyEnum)]: {
-- No origin is given here.
        Field[0]: Name: FIRST, Type: LMain$MyEnum;, Value: Object[5453] (type: L)
        Field[1]: Name: SECOND, Type: LMain$MyEnum;, Value: Object[5450] (type: L)
        Field[2]: Name: FIRST_VALUE, Type: I, Value: 0 (type: I)
        Field[3]: Name: SECOND_VALUE, Type: I, Value: 1 (type: I)
    }

Object[5418]: {
                 Origin: {ROOT}:myStructure.Main$MyStruct:enum_
        Class: (2,Main$MyEnum)
        Field[0]: Name: name, Type: Ljava/lang/String;, Value: Object[5411] (type: L)
        Field[1]: Name: ordinal, Type: I, Value: 0 (type: I)
    }

The enum has several possible values, being MyEnum.FIRST, and MyEnum.SECOND.

What I'm trying to do is to specify a way to tell that this enum must alias either FIRST or SECOND, so as to compare it afterwards to myStructure.enum == FIRST or myStructure.enum == SECOND.

I've been trying to using the following rules, but it seems that once the class MyEnum gets expanded to an instanceof MyEnum, then it is not possible to alias it to an existing other instance.

{R_ANY}.myStructure.Main$MyStruct:enum_
    instanceof Main$MyEnum
    not null;
{R_ANY}.myStructure.Main$MyStruct:enum_
    instanceof Main$MyEnum
    expands to instanceof Main$MyEnum
    triggers Main:(LMain$MyEnum;)V:triggerValidMyEnum:{$REF};
-- the trigger just asserts that the enum is equal to FIRST || SECOND
{R_ANY}.myStructure.Main$MyStruct:enum_
    instanceof Main$MyEnum
    aliases nothing;

However, if I try to expand it to nothing, then the MyEnum class does not get initialized, and thus I cannot specify that it aliases some values of the heap:

{R_ANY}.myStructure.Main$MyStruct:enum_
    instanceof Main$MyEnum
    not null;
{R_ANY}.myStructure.Main$MyStruct:enum_
    instanceof Main$MyEnum
    expands to nothing;
{R_ANY}.myStructure.Main$MyStruct:enum_
    instanceof Main$MyEnum
    aliases target [Main$MyEnum].(FIRST|SECOND);

Is there a way to specify aliasing on Enum values?

Regards, Georges-Axel.

[pietrobraione]

Hi Georges-Axel, and sorry if I took so much time to answer. I think your problem is a kind of a chicken-and-egg problem. In JBSE for a field a to alias another field b, the field b must be first initialized in some way. But if it is the access to a the only one that causes the initialization to b, then it is possible that everything becomes stuck. The only solution I can imagine right now is to modify the code that you are analyzing so it loads the MyEnum class before it uses the enum_ field, which surely is inelegant, especially if the code you are analyzing is third-party and you would like to keep it as close as possible to the original one. Since it is possible that you spotted a JBSE bug, can you please send me the whole code you are running? This way I hope to give you a more definite answer in the next days.

[GAJaloyan]

Hi Pietro and thank you very much for your answer. Indeed this looks like it requires some source code modification to invoke initialize the class so that the various objects corresponding to the values of Enum are present in stack. But from what you explain, this may definitely be worth the try. I'll have other projects to do in the future months, so I'll put on this on hold (and close the issue). I've sent a patch for a bug I found (in another unrelated issue). Thanks very much for the help!