jvm: Difficulties with "hello world"

[langston-barrett]

crucible-jvm can't verify the following main method that simply calls System.out.println. This may be the intended behavior. Regardless, this error message is sub-optimal - it doesn't make it clear what's gone wrong, how to fix it, or if this is a user error or a problem with crucible-jvm.

class Main {
    public static void main(String args[]) {
        System.out.println("Hello, world!");
    }
}

javac -g Main.java && cabal run exe:crucible-jvm -- Main.class

resolveField: Field FieldId {fieldIdClass = ClassName "java/lang/Object", fieldIdName = "value", fieldIdType = char[]} not found
CallStack (from HasCallStack):
  error, called at src/Lang/Crucible/JVM/Translation/Monad.hs:61:15 in crucible-jvm-0.2-inplace:Lang.Crucible.JVM.Translation.Monad
  jvmFail, called at src/Lang/Crucible/JVM/Translation/Class.hs:843:23 in crucible-jvm-0.2-inplace:Lang.Crucible.JVM.Translation.Class

Update:

javac --version
javac 17.0.3

[RyanGlScott]

Which version of the JVM are you using?

[langston-barrett]

@RyanGlScott Good question :-) javac --version says javac 17.0.3.

[RyanGlScott]

That would explain it, then. Really, this is an issue with crucible-jvm's special treatment of the String class, which is tracked in #641. This special treatment makes a lot of assumptions about the class fields of String that work for JDK 8 and earlier, but not later versions of the JDK. To make this work for later versions of the JDK, we'd need to revisit how String is defined and change the special-casing in crucible-jvm accordingly.

[langston-barrett]

Gotcha, I'll close this in favor of #641 then. Thanks!