Mac OS: java.lang.UnsatisfiedLinkError: no FloatingPoints

[Sebastian Junges]

Dear,

I am trying to run CPAchecker on a MacOS--it would be more convenient as some other parts of  my tool chain currently run more stable on a Mac. 

With the binary, I run into the following problem when the program contains a double. I guess I missed some step, but I can't figure out which step.

Exception in thread "main" java.lang.UnsatisfiedLinkError: no FloatingPoints in java.library.path: [/Users/sjunges/Library/Java/Extensions, /Library/Java/Extensions, /Network/Library/Java/Extensions, /System/Library/Java/Extensions, /usr/lib/java, .]

Java version:

openjdk 14.0.1 2020-04-14

OpenJDK Runtime Environment (build 14.0.1+7)

OpenJDK 64-Bit Server VM (build 14.0.1+7, mixed mode, sharing)

Happy to provide more information! Also happy to try out some things as you might not have access to a Mac.

Best regards,

Sebastian Junges 

[Philipp Wendler]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Hi Sebastian,

Am 25.07.20 um 07:48 schrieb Sebastian Junges:

> I am trying to run CPAchecker on a MacOS--it would be more
> convenient as some other parts of my tool chain currently run more
> stable on a Mac.
>
> With the binary, I run into the following problem when the program
> contains a double. I guess I missed some step, but I can't figure
> out which step.
>
>>
>> Exception in thread "main" java.lang.UnsatisfiedLinkError: no
>> FloatingPoints in java.library.path:
>> [/Users/sjunges/Library/Java/Extensions,
>> /Library/Java/Extensions, /Network/Library/Java/Extensions,
>> /System/Library/Java/Extensions, /usr/lib/java, .]

We have an internal component in CPAchecker for handling floats for
which we plan writing an plain-Java implementation but currently have
only a native version, and we do not have a Mac binary for it.
Thus loading it fails.

Could you please post the full command line and stack trace? Maybe
there is a workaround.
Alternatively, it should be possible for you to compile the library.
The compile script is
lib/native/source/cFloatingPointlib.c/compile.sh and it needs the
environment variable JAVA_HOME pointing to your Java directory.
However, we do not know anything about compilation on a Mac, it might
need adjustments (which we would like to incorporate).

However, depending on your configuration it is likely that there will
be more components for which we have no Mac binary. For example, the
default SMT solver of CPAchecker is MathSAT, and all other SMT solvers
miss some features.
There is a MathSAT binary for Mac on
https://mathsat.fbk.eu/download.html
but you would again need to compile a library in order to be able to
use it.

If you wish to work on this we would certainly help you in telling
which components are needed and how they can compiled on Linux, but we
cannot give any Mac-specific advice nor test anything ourselves.
We would like to add any improvements you find or add information to
our documentation though, so it would be great if you could share it.

Greetings
Philipp
- --
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEGdWhCy2XiNh8vuXtYsD3jDGp3owFAl8ecDsACgkQYsD3jDGp
3oxo+g//UHZU3kuyPG5rU2kaLIT/pY5yXDUq2sEZrhXyyH6LUhwBBqrE39c6jB/e
tcTzU+0GtJcTZaLGYmBLF9fSNeTzcS+td5F8ZV/LCfMBAwQWAOYYc9w0PP4errGT
KcyBou0/dZqCunNg8z3j5NNfQnOStf2xKL4Uk1X+2EgFxJc4/eEgJUi/MlXmASCd
eufPj0OEljH5riWHO7LGmT/BgFY6q+I7NNA7ODa/yVzOaOzDK5F8F6puQ2QnvrPq
fZAvXypfMTG/UtQH/3DZldT8b4iY7Xm0X6IEHuKPVhsw5kU7SN4/g6LVVufJYjsm
Qmsy2WLecNMts5VfvmSZgkpyASjKiLuizFCrRkdBKgKgyZZxgtebonv4Tugj56hL
BmEMIDgTzdb0PR53rAAuE4o8ioqr41QJ83Td4Jdquir8VfrpKM8k7px3OMEwuVZy
d3G/kiJS0wHHn671F3xFnQOtTX5zXTtomIxKmCK3Mt7RSH+AQyAdIzNAZ4TVcsew
npiHoxXBqcWcPHgKfrtKAmIzpuiZv4uHFV2CoEoqS2WelZp9a6r7CFSPbrBCwfRt
ozUv4Z2OT6YuM7A8Sa77i3eBCBL8GxnNQcgauboeup0xSBjJXF92l5JDyQ2Thc77
XoO8/cPgUrvYxbYYgsRraTEPS0gQVTz9332QQlO6oHe0SjNAkSk=
=aRtb
-----END PGP SIGNATURE-----

[Sebastian Junges]

Hi Philipp,

Thanks for the answer! I am happy to help figuring this out, and to find/suggest necessary changes. I can in a later stage also test whether any adaptions made do work :-)

I now downloaded CPAChecker from source, and ran ant in the main folder.

I already had an JAVA_HOME set accordingly. 

I then cd’ed in to lib/native/source/cFloatingPointlib.c/, 

Exchanged ‘linux’ with ‘darwin’. The compilation went through. 

However, I still get an error (see below). Also running ant again did not resolve this issue. 

Am I missing to create a java library from the so file?

Best, Sebastian

Current error message:

scripts/cpa.sh   -config config/components/valueAnalysis-generate-cmc-condition.properties \

               -spec config/properties/unreach-call.prp \

               ~/cal/test.c

Running CPAchecker with default heap size (1200M). Specify a larger value with -heap if you have more RAM.

Running CPAchecker with default stack size (1024k). Specify a larger value with -stack if needed.

Running CPAchecker with the following extra VM options:  -Djava.io.tmpdir=/var/folders/7v/9j_1rhzs1ts4cky4d4tm1vtr0000gn/T/

Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO)

Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 1.9.2-svn / valueAnalysis-generate-cmc-condition (OpenJDK 64-Bit Server VM 14.0.1) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "/Users/sjunges/cal/test.c" (CPAchecker.parse, INFO)

line 4392: Dereferencing of non-pointer type destructor  in expression *dealloc (ASTConverter.convert, WARNING)

Exception in thread "main" java.lang.UnsatisfiedLinkError: no FloatingPoints in java.library.path: [/Users/sjunges/Library/Java/Extensions, /Library/Java/Extensions, /Network/Library/Java/Extensions, /System/Library/Java/Extensions, /usr/lib/java, .]

at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2680)

at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:807)

at java.base/java.lang.System.loadLibrary(System.java:1907)

at org.sosy_lab.common.NativeLibraries.loadLibrary(NativeLibraries.java:201)

at org.sosy_lab.cpachecker.util.floatingpoint.CFloatNativeAPI.<clinit>(CFloatNativeAPI.java:25)

at org.sosy_lab.cpachecker.util.floatingpoint.CFloatNative.<init>(CFloatNative.java:19)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTLiteralConverter.parseFloatLiteral(ASTLiteralConverter.java:162)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTLiteralConverter.convert(ASTLiteralConverter.java:81)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convertExpressionWithSideEffectsNotSimplified(ASTConverter.java:366)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convertExpressionWithSideEffects(ASTConverter.java:315)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convert(ASTConverter.java:703)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convertExpressionWithSideEffectsNotSimplified(ASTConverter.java:335)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convertExpressionWithSideEffects(ASTConverter.java:315)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convertExpressionToStatement(ASTConverter.java:1513)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.ASTConverter.convert(ASTConverter.java:1509)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFAFunctionBuilder.handleExpressionStatement(CFAFunctionBuilder.java:643)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFAFunctionBuilder.visit(CFAFunctionBuilder.java:586)

at org.eclipse.cdt.internal.core.dom.parser.c.CASTExpressionStatement.accept(CASTExpressionStatement.java:66)

at org.eclipse.cdt.internal.core.dom.parser.c.CASTCompoundStatement.accept(CASTCompoundStatement.java:81)

at org.eclipse.cdt.internal.core.dom.parser.c.CASTFunctionDefinition.accept(CASTFunctionDefinition.java:133)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFABuilder.handleFunctionDefinition(CFABuilder.java:384)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.CFABuilder.createCFA(CFABuilder.java:337)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.buildCFA(EclipseCParser.java:388)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.parseSomething(EclipseCParser.java:164)

at org.sosy_lab.cpachecker.cfa.parser.eclipse.c.EclipseCParser.parseString(EclipseCParser.java:208)

at org.sosy_lab.cpachecker.cfa.CParserWithLocationMapper.parseFile(CParserWithLocationMapper.java:79)

at org.sosy_lab.cpachecker.cfa.CFACreator.parseToCFAs(CFACreator.java:637)

at org.sosy_lab.cpachecker.cfa.CFACreator.parseFileAndCreateCFA(CFACreator.java:426)

at org.sosy_lab.cpachecker.core.CPAchecker.parse(CPAchecker.java:485)

at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:344)

at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:169)

--
You received this message because you are subscribed to the Google Groups "CPAchecker Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cpachecker-use...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cpachecker-users/37b1c430-43ec-805c-f19b-104d43267af1%40philippwendler.de.

[Philipp Wendler]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Hi Sebastian,

Am 27.07.20 um 21:44 schrieb Sebastian Junges:

> I now downloaded CPAChecker from source, and ran ant in the main
> folder. I already had an JAVA_HOME set accordingly. I then cd’ed in
> to lib/native/source/cFloatingPointlib.c/, Exchanged ‘linux’ with
> ‘darwin’. The compilation went through. However, I still get an
> error (see below). Also running ant again did not resolve this
> issue. Am I missing to create a java library from the so file?

Ok, that was easier than expected :-)
Because I expected more steps to be necessary I had not mentioned that
the resulting file needs to be copied into the appropriate directory
manually.
For Mac, this should be lib/native/x86_64-macosx/

If that does not work, we would need to investigate, but you could
test by putting it into any of the directories mentioned in the error
message:

> Exception in thread "main" java.lang.UnsatisfiedLinkError: no
> FloatingPoints in java.library.path:
> [/Users/sjunges/Library/Java/Extensions, /Library/Java/Extensions,
> /Network/Library/Java/Extensions, /System/Library/Java/Extensions,
> /usr/lib/java, .]

I guess "." is the most convenient of this.
You can even extend this list by specifying a directory with the
"-Djava.library.path=..." argument to the JVM, which you can add to
the JAVA_VM_ARGUMENTS environment variable.
But none of this is hopefully necessary.

Greetings
Philipp
- --
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEGdWhCy2XiNh8vuXtYsD3jDGp3owFAl8fzOsACgkQYsD3jDGp
3ownyQ/7BamG+bWYkSYCZRdMummEWO2y+Pdsij5oxYOc41DSTpqYDC7goNOGNEGZ
KlMEcxW47eU+UJgrTRYurMh4pLoqlgeKy8BYOUGykH0HNeHCvmWtQ8RtDrw573QB
4EhdqPuuxkU0iynJ5jP9D37BSVAdLw5gE+XUc/OZZ3Yt1j6YTxT3HwUmsoswIs+L
/CeWY7XB9RiRFohspZyQ17TK+MiKTKSnLMFL7/JXxrNnn+m5lGuisyjQmnBfFrHf
J+VqT8/OcIWFKhKUb/nvV+HBpQleSxTEiN7wsl2AWiOO8FpHJfsvhbKsUDhbGGu/
4s1rUGmjt9zOGA5LdNcc2bWw+Lk2OLIp4hg4DYAgAKRwuX5+c06uMOWCf2Iru4zQ
vSsErPCmFJNKUYVJMQ1fKrLSuvJpL3ae2QfMpjuZGHmD5LJtztWS9C0+WkkZzu3M
Mv3B23WvnIVY04pOYqFLIffsHOLqliLdRkERBiF+/3rgqVJvKt4Zx0DILkxYJtcj
2Y4U2WCfFoD8yOhnfWlw18CnAnMemD3jLoF3VsGPqL3KzQ3yY9VL6WtJHYTjzhMu
HRljvUB2ngmS0OqpxjRuGzbgGN8AwuG6Y5PhEIn9bFLnz1bJv6sRULH9CPmusTdM
4H8w1efFek08N7dToCrNa/JEPUw0w+/oc+/J8Wi9zB6utAzrNDs=
=+F0c
-----END PGP SIGNATURE-----

[Sebastian Junges]

Hi Philipp,

Many thanks!

I had to additionally change the compile.sh file such that the shared object has a .dylib suffix (i.e., I replaced .so by .dylib).
Then, copying this into the folder you specified resolves the issue. It does not work if the suffix is .so.

In case further issues arrive with macosx, do you want to make a single thread regarding macOS, or should I keep threads close to the error message I get?

Sebastian

> --
> You received this message because you are subscribed to the Google Groups "CPAchecker Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to cpachecker-use...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/cpachecker-users/69358785-5f73-2c5d-93c2-99415510f708%40philippwendler.de.

[Philipp Wendler]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Hi Sebastian,

Am 28.07.20 um 18:46 schrieb Sebastian Junges:

> I had to additionally change the compile.sh file such that the
> shared object has a .dylib suffix (i.e., I replaced .so by
> .dylib). Then, copying this into the folder you specified resolves
> the issue. It does not work if the suffix is .so.

Nice to hear!
You could even send me the file and we check it in such that it will
work for other users?

> In case further issues arrive with macosx, do you want to make a
> single thread regarding macOS, or should I keep threads close to
> the error message I get?

As you wish.
If you encounter specific problems, you could also file them in our
issue tracker:
https://gitlab.com/sosy-lab/software/cpachecker/-/issues
But sending to the list is also ok.

Greetings
Philipp
- --
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEGdWhCy2XiNh8vuXtYsD3jDGp3owFAl8hCgoACgkQYsD3jDGp
3oxEOw/9FuClfqE9T3imMOIRsi5WW5jmwLK3r8KOEbQ+5PYOEKoRYpUrk72Ti2CX
4qlxq53VZstOO3To4EWSlKy7BE/Z6cKe3UC0/hj8GpLz//ux5soBz7D1LEXWSa80
FA7HyGsi58QieHA7aVTKAM+TkqN5gZ0YgrGAFsRqam7xbq2wO361ElYJvn9RnWhh
4PPMnGdNVe3ktNk/v1JzROOEYMHglII9Qgy7QT4DrflfoAKDooF8/JPmT5V72j8K
gZNtIzEz7Lh+N2eFvKvbpy4gjnb+Q2sdKcdSGtV5DgETE0PNYZsfNNja2e5V07IP
3C1tYakZAEfZhY0P3zwS2LOrlYRwDVrP5hOGZf2j0hQeobhXGzxv5c9Ngpy2ep8I
I2xFXTPsZGf/wQqIDWphlh+SR5gdJkLQjXrkwYlfm2PdhbFKT48mONXB20EmsrF2
UEc79UKprTcVqy0Rc6R8Htw0dLDeMm0+bYW3DIXJMbXgKjvW6eMeQvHBPHLV55e7
t79nFMfSs0IIShb+83wh/Ut2tOGfTcajkWJ8huB3MGzyxbO0I1hmKOW0YxRsbMUk
zU5FTJsDlNxIgneqYiAUzUvvpn+nywGU6ZxSZZf0N7nbAe3tzR1EgaMq3OAAVojU
U4g5jrgoVetskSwBs+DTx9hBE3o3UMolx9y8MLixgA5eJBNCaIU=
=Tvhs
-----END PGP SIGNATURE-----