Does jbmc build on MacOS?

[markrtuttle]

CBMC version: 5.38
Operating system: MacOS 15.5.2 (Big Sur) on Apple M1

Does jbmc build on MacOS?

In the cbmc formula for brew, Lines 35-36 say that the java front end won't build on ARM.

I think the issue is that in OpenJDK 17.13 installed by brew under MacOS 15 on Apple M1, the March commit a0c3f242 deleted the methods isOtherUppercase and isOtherLowercase called on Line 5463 and Line 5529 of Character.java in DiffBlue's java-models-library submodule.

In fact, if I delete these lines, then jbmc compiles on MacOS 15 on Apple M1. Assuming brew installs OpenJDK 7.13 independent of ARM, isn't this a problem elsewhere? Is it possible to rewrite these two lines without invoking these methods?

Edit: Changed OpenJDK version from 7.13 to 17.13.

[thomasspriggs]

Isn't OpenJDK 7.13 rather out of date? If I am reading the POM file correctly, the models library is supposed to be built using Java version 8. It might be worth trying a newer version of OpenJDK to see if that fixes the build.

[chrisr-diffblue]

I think 'OpenJDK 7.13' may be a typo for 'OpenJDK 17.3' ? Note also some version confusion on Apple M1 https://stackoverflow.com/questions/67782746/openjdk-16-shows-as-17-on-macos-apple-silicon-when-installed-with-homebrew

Possibly the two 'correct fixes' are:

a) Specifiy compatible java dependencies in the cbmc brew formula (rather than an unversioned java dependency as it currently has),
or
b) Fix the models library to be java version aware....

[markrtuttle]

I strongly prefer to have the models library fixed so everything builds with cmake on everything, especially if it is "easy" to replace the functionality lost by the change in the Character API.

@chrisr-diffblue is right: I was looking at tag-17+13 that appears to be the first release containing the commit a0c3f242 that modifies the Character API.

Maven says the versions installed by brew on Apple M1 are

laptop:~ mvn -v
Apache Maven 3.8.2 (ea98e05a04480131370aa0c110b8c54cf726c06f)
Maven home: /opt/homebrew/Cellar/maven/3.8.2/libexec
Java version: 17, vendor: Homebrew, runtime: /opt/homebrew/Cellar/openjdk/16.0.2/libexec/openjdk.jdk/Contents/Home
Default locale: en_US, platform encoding: UTF-8
OS name: "mac os x", version: "11.5.2", arch: "aarch64", family: "mac"

As @chrisr-diffblue points out, brew installs 16 on x86 and 17 on arm, and for some reasons continues to name the directory 16 on arm. The discussion there claims that 16 won't build on arm, which is why brew is installing a 17 on arm.

[cho-m]

I just noticed this issue.

As heads up on Homebrew-side, I am working on OpenJDK 17 update Homebrew/homebrew-core#85174, which means issue will impact all the supported platforms (Intel macOS, ARM macOS, Intel Linux).

In order to quickly move forward with update, I do have a PR to change cbmc's dependency to openjdk@11 in Homebrew/homebrew-core#85260 as that is the only remaining issue related to openjdk 16 --> 17.

Unless a fix for building JBMC with OpenJDK 17 is available in a few days, I will probably go ahead with the above change and add a comment referencing this issue. Once compilation with OpenJDK 17 is fixed, the cbmc formula's dependency can be set to main openjdk formula again.

[NlightNFotis]

Hi @cho-m, I can build CBMC and all assorted binaries locally with cmake using java 16.0.1.

I believe that as a quick work-around fixing the version of openJDK to openJDK 11 should work, but if we could do it for openJDK 16 it would be even better. To that effect, I'm trying to play around with the formula locally, and try to fix the dependency to openjdk@16 but it doesn't work, installing 17 instead.

In any case, if this works now (in the sense that it doesn't block a homebrew PR making new CBMC releases), then we could keep the 11 version pinning for a couple days while we try to fix the root cause of the compilation failure on our end, and update our dependency to be working with openjdk@17.

[cho-m]

Homebrew won't keep OpenJDK 16 since it is not an LTS release and is no longer maintained. The versioned OpenJDK are openjdk@8 (supported until 2030) and openjdk@11 (supported until 2026). OpenJDK 17 is the next LTS release, so it will probably become a versioned openjdk@17 formula after OpenJDK 18 is released.

EDIT: In terms of M1 ARM support, Homebrew has backported fixes to get openjdk@11 formula working on ARM. Once OpenJDK 17 PR is done, openjdk formula should support ARM out-of-the-box without any extra patches/EA-release. openjdk@8 will probably never support ARM.

[NlightNFotis]

Hi @cho-m, we have now fixed the upstream issues with the Models Library and JDK version 17.

I took the liberty of creating a PR in homebrew so that it lightens your maintenance load. The PR is here https://github.com/Homebrew/homebrew-core/pull/85720/files.

Let me know if there's something else you would like me to do to move the issue forward.

Thanks for your time.

[NlightNFotis]

Hi @markrtuttle, after the merge of Homebrew/homebrew-core#85720, it looks to me like jbmc is built on homebrew/osX without issues.

Can you verify this? If yes, then is this issue good to be closed now?

[markrtuttle]

@NlightNFotis I have successfully built the develop branch on Apple M1 MacOS 11.5.2.

laptop:~/cbmc/build cbmc --version
5.39.3 (cbmc-5.39.3-2-gc3d7235036)
laptop:~/cbmc/build jbmc --version
5.39.3 (cbmc-5.39.3-2-gc3d7235036)

I'm closing this issue. Thanks!