search

runtimeverification / rv-predict

Code for improved rv-predict and installer
BSD 3-Clause "New" or "Revised" License
2 stars 3 forks source link

RV-Predict basic examples not working? #557

Closed grosu closed 8 years ago

grosu commented 9 years ago

I just downloaded a fresh copy of RV-Predict and tried the basic example in the documentation, and got the following exception:

D:\RV-Predict>java -cp examples/examples.jar account.Account
Bank system started
loop: 2
loop: 2
sum: 256
sum: -174
sum: 76
sum: -33
..
End of the week.
Bank records = 125, accounts balance = 125.
Records match.

D:\RV-Predict>rv-predict -cp examples/examples.jar account.Account

----------------Instrumented execution to record the trace-----------------
[RV-Predict] Log directory: C:\Users\Grigore\AppData\Local\Temp\rv-predict847168
640538487427
java.lang.reflect.InvocationTargetException
        at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
        at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)FATAL ERRO
R in native method: processing of -javaagent failed

        at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
        at java.lang.reflect.Method.invoke(Unknown Source)
        at sun.instrument.InstrumentationImpl.loadClassAndStartAgent(Unknown Sou
rce)
        at sun.instrument.InstrumentationImpl.loadClassAndCallPremain(Unknown So
urce)
Caused by: java.lang.UnsatisfiedLinkError: D:\RV-Predict\lib\native\windows64\li
bz3.dll: Can't find dependent libraries
        at java.lang.ClassLoader$NativeLibrary.load(Native Method)
        at java.lang.ClassLoader.loadLibrary0(Unknown Source)
        at java.lang.ClassLoader.loadLibrary(Unknown Source)
        at java.lang.Runtime.loadLibrary0(Unknown Source)
        at java.lang.System.loadLibrary(Unknown Source)
        at com.runtimeverification.rvpredict.config.Configuration.c(Unknown Sour
ce)
        at com.runtimeverification.rvpredict.engine.main.b.<init>(Unknown Source
)
        at com.runtimeverification.rvpredict.a.k.<init>(Unknown Source)
        at com.runtimeverification.rvpredict.instrument.Agent.premain(Unknown So
urce)
        ... 6 more
Exception in thread "main"

The agent version does not work either.

grosu commented 9 years ago 
D:\RV-Predict>java -version
java version "1.8.0_60"
Java(TM) SE Runtime Environment (build 1.8.0_60-b27)
Java HotSpot(TM) 64-Bit Server VM (build 25.60-b23, mixed mode)
traiansf commented 9 years ago

apparently the z3 libraries are not found. On Linux, one has to set the LD_LIBRARY_PATH for this. On windows there used to work, at least on my machine. Is it possible to have an automated test environment for windows (and MacOS, maybe) like we have Jenkins for linux?

Traian

2015-09-11 14:43 GMT+03:00 Grigore Rosu notifications@github.com:

D:\RV-Predict>java -version java version "1.8.0_60" Java(TM) SE Runtime Environment (build 1.8.0_60-b27) Java HotSpot(TM) 64-Bit Server VM (build 25.60-b23, mixed mode)

— Reply to this email directly or view it on GitHub https://github.com/runtimeverification/rv-predict/issues/557#issuecomment-139523416 .

grosu commented 9 years ago

On Linux, one has to set the LD_LIBRARY_PATH for this.

Is that documented anywhere? Also, is it really needed? We provide z3 as part of the install, so why should we have to also set that environment variable? To me is seems illogical and I would be tempted, as a user, to think of the application as being non-professionally packaged. Please let me know if I am wrong here, because I want to learn this.

Is it possible to have an automated test environment for windows (and MacOS, maybe) like we have Jenkins for linux?

I think we should do that, for all our tools. What do we need?

traiansf commented 9 years ago

2015-09-11 15:42 GMT+03:00 Grigore Rosu notifications@github.com:

On Linux, one has to set the LD_LIBRARY_PATH for this.

Is that documented anywhere? Also, is it really needed? We provide z3 as part of the install, so why should we have to also set that environment variable? To me is seems illogical and I would be tempted, as a user, to think of the application as being non-professionally packaged. Please let me know if I am wrong here, because I want to learn this.

if you run RV predict through the rv-predict script, the library path is automatically set; however, if you run it as an agent, there is no script to set it for you, so it has to be set manually.

What I proposed was to offer a rv-predict.env file which the user interested in running rv-predict as an agent could source in their shell and automatically get the proper environment variables.

Nevertheless, on Windows should have worked out of the box.

Is it possible to have an automated test environment for windows (and MacOS, maybe) like we have Jenkins for linux?

I think we should do that, for all our tools. What do we need?

Apparently Jenkins can be run under windows, too. So I guess we would need virtual machines for all OSes we want to test against and potentially a master coordinating runs on all these machines. Not sure how the github pull request plugin for Jenkins integrates with being run on multiple machines at the same time....

— Reply to this email directly or view it on GitHub https://github.com/runtimeverification/rv-predict/issues/557#issuecomment-139536573 .

grosu commented 9 years ago

however, if you run it as an agent, there is no script to set it for you, so it has to be set manually.

Right, but is that explained anywhere? How can a Linux user of RV-Predict know how to do that right now, with the current RV-Predict version that we are ready to advertise?

What I proposed was to offer a rv-predict.env file which the user interested in running rv-predict as an agent could source in their shell and automatically get the proper environment variables.

But that still means that the user has to do something about it. What I don't understand is the following. We provide z3 with RV-Predict. What stops us from calling the exact z3 that we package with RV-Predict? RV-Predict should be able to know exactly where its main folder is located on the machine, and this should be able to call z3 from its exact place within that RV-Predict folder. That would mean that the user has to do nothing besides the usual, which is to set their PATH and which is expected.

traiansf commented 9 years ago

2015-09-11 15:57 GMT+03:00 Grigore Rosu notifications@github.com:

however, if you run it as an agent, there is no script to set it for you, so it has to be set manually.

Right, but is that explained anywhere? How can a Linux user of RV-Predict know how to do that right now, with the current RV-Predict version that we are ready to advertise?

yes, this is explained in the RV Predict documentation which is on the site.

What I proposed was to offer a rv-predict.env file which the user interested in running rv-predict as an agent could source in their shell and automatically get the proper environment variables.

But that still means that the user has to do something about it. What I don't understand is the following. We provide z3 with RV-Predict. What stops us from calling the exact z3 that we package with RV-Predict? RV-Predict should be able to know exactly where its main folder is located on the machine, and this should be able to call z3 from its exact place within that RV-Predict folder. That would mean that the user has to do nothing besides the usual, which is to set their PATH and which is expected.

that is true; however, java doesn't, so when rv-predict is run as an agent, it doesn't really know. moreover, (on linux) java looks into the LD_LIBRARY_PATH for loading libraries; hence the directory where the libraries are located must be added to that environment variable. When RV Predict is run through a script, the script (which knows where it's run from) sets that variable before calling java.

— Reply to this email directly or view it on GitHub https://github.com/runtimeverification/rv-predict/issues/557#issuecomment-139539225 .

owolabileg commented 9 years ago

@ yes, this is explained in the RV Predict documentation which is on the site.

Can you please point me to where this is explained? I myself have just run into this. I have set my LD_LIBRARY_PATH.

echo $LD_LIBRARY_PATH

yields

/u01/app/oracle/product/11.2.0/xe/lib:/home/owolabi/FSL/k/lib/native/linux/x64:/opt/sybase/OCS-15_0/lib3p/libsbgse2.so:/opt/sybase/OCS-15_0/lib3p64/libsbgse2.so:/home/owolabi/RV-Predict/lib/native/linux64/libz3java.so:/home/owolabi/sqllib/lib64:/home/owolabi/sqllib/lib32

yet, when I run mvn test project configured with RV-Predict part of the error message reads:

FATAL ERROR in native method: processing of -javaagent failed Caused by: java.lang.UnsatisfiedLinkError: /home/owolabi/RV-Predict/lib/native/linux64/libz3java.so: libz3.so: cannot open shared object file: No such file or directory

Lastly, I can confirm that /home/owolabi/RV-Predict/lib/native/linux64/libz3java.so exists.

Thanks.

owolabileg commented 9 years ago

I dug into this a bit more. It seems that I was getting this error because I set LD_LIBRARY_PATH myself to point to the relevant .so files after doing source setenv from /lib. I also found that if I remove those .so files from LD_LIBRARY_PATH, I have to re-run source setenv again before RV-Predict can work. I think this is rather fragile.

I originally modified my LD_LIBRARY_PATH to avoid running source setenv everytime. It be great to have clear instructions for doing that.

Thanks

grosu commented 9 years ago

I really dislike the idea of using LD_LIBRARYPATH and I'm not buying the argument that "it is needed for Linux. See, for example, Section 3.3.1 at http://tldp.org/HOWTO/Program-Library-HOWTO/shared-libraries.html, where they say *LD_LIBRARYPATH is handy for development and testing, but shouldn't be modified by an installation process for normal use by normal users, that it is fragile and does not really work on all systems, and where they also provide an alternative. See also this "Why LD_LIBRARY_PATH is bad" article at http://xahlee.info/UnixResource_dir/_/ldpath.html.

I continue to believe that all we need to do is to have the user set the PATH and nothing else. From there we can find the folder where RV-Predict is installed. Since we know where z3 is in the installation folder, we should be able from there to make an absolute call to z3.

traiansf commented 9 years ago

Well, yes, if our program would install like a regular program, both for windows and linux, it would put its dependent libraries in the default library path, and then one wouldn't need to mess with the LD_LIBRARY_PATH.

However, we currently don't do that, preferring that all RV-Predict files stay in one place, making uninstall easy.

I would support installing it properly and providing uninstall scripts. note that, for linux, this would mean running it with root rights, something we've avoided so far.

2015-09-15 15:05 GMT+03:00 Grigore Rosu notifications@github.com:

I really dislike the idea of using LD_LIBRARYPATH and I'm not buying the argument that "it is needed for Linux . See, for example, Section 3.3.1 at http://tldp.org/HOWTO/Program-Library-HOWTO/shared-libraries.html http://tldp.org/HOWTO/Program-Library-HOWTO/shared-libraries.html, where they say *LD_LIBRARYPATH is handy for development and testing, but shouldn't be modified by an installation process for normal use by normal users, that it is fragile and does not really work on all systems, and where they also provide an alternative. See also this "Why LD_LIBRARY_PATH is bad" article at http://xahlee.info/UnixResource_dir/_/ldpath.html.

I continue to believe that all we need to do is to have the user set the PATH and nothing else. From there we can find the folder where RV-Predict is installed. Since we know where z3 is in the installation folder, we should be able from there to make an absolute call to z3.

— Reply to this email directly or view it on GitHub https://github.com/runtimeverification/rv-predict/issues/557#issuecomment-140368601 .

grosu commented 9 years ago

I am still not convinced that we cannot install everything in one folder as we do now, and at the same time call z3 by its absolute path. Are you saying that you cannot, programmatically, call z3 by its absolute path (calculated in a platform independent way)?

traiansf commented 9 years ago

It's not about the z3 executable. If we were using the executable (as we used to), there wouldn't be any problem.

However, we're using the library, as it has faster response time; moreover, we're actually using 2 libraries: the z3 C library and a z3java C wrapper library over it, which is loaded by java from the z3 java jar library, none of which being written by us.

Now, the java wrapper attempts to load the z3java library, which itself tries to load the z3 library. And all these expect the corresponding libraries to be in the default library path.

On windows, we could indeed add the corresponding directory to the system path (or ask the user to do so) as the library path is the system path; but even here, it depends whether the java installed is 32 or 64 bits.

However, on Linux the default library path includes /lib , /usr/lib, and a couple of other lib directories.

2015-09-15 15:57 GMT+03:00 Grigore Rosu notifications@github.com:

I am still not convinced that we cannot install everything in one folder as we do now, and at the same time call z3 by its absolute path. Are you saying that you cannot, programmatically, call z3 by its absolute path (calculated in a platform independent way)?

— Reply to this email directly or view it on GitHub https://github.com/runtimeverification/rv-predict/issues/557#issuecomment-140379807 .

grosu commented 9 years ago

@yilongli do you also agree with @traiansf that our options here are either to have a proper installer/uninstaller, which requires the user administrator rights on unix machines, or otherwise to live with having them source setenv before running rv-predict as an agent?

Do you both think that there is no way that we ask our users just set the PATH, or do only one thing once at installation time and never bother again with "unexpected exception thrown", keeping all the simplicity that we have now?

traiansf commented 9 years ago

Clarification: for windows it might work to just set the PATH, but in addition to the rv-predict bin path, they would also need to add the right z3 directory to the path (which would be one of lib/native/windows64 or lib/native/windows32), depending on the java version they are using. I think this could be detected and printed out at install time.

2015-09-16 15:01 GMT+03:00 Grigore Rosu notifications@github.com:

@yilongli https://github.com/yilongli do you also agree with @traiansf https://github.com/traiansf that our options here are either to have a proper installer/uninstaller, which requires the user administrator rights on unix machines, or otherwise to live with having them source setenv before running rv-predict as an agent?

Do you both think that there is no way that we ask our users just set the PATH, or do only one thing once at installation time and never bother again with "unexpected exception thrown", keeping all the simplicity that we have now?

— Reply to this email directly or view it on GitHub https://github.com/runtimeverification/rv-predict/issues/557#issuecomment-140720642 .

grosu commented 9 years ago

This non-uniformity between running rv-predict in command line (which automatically sources setenv) and as an agent bothers me so much, that I almost feel that we should only provide the agent version with only one set of instructions on how to install it. People seem to end up using it as an agent mostly anyway. If we could only just have to add one option to java instead of two.

yilongli commented 9 years ago

@grosu After PR #579, users should not see the ugly UnsatisfiedLinkError anymore. They will get an error message saying that their environment variable is not properly set. And the correct library path that needs to be included is also printed. I personally do not like tools to mess with my OS configuration so I prefer not to set the environment variable during installation. I tend to live with the setenv script.