I am currently implementing type t val null : t val isNull : t -> bool where type t = CInterface.vol. There is no problem doing this but I wondered whether I could improve the CInterface structure to avoid annoying little C library functions.
Would it be at all controversial to include null : vol in CInterface?
Regarding comparison of vols, it makes sense that vol is not an eqtype because it stores more than just the "raw vol". Generally, is it safe to compare vols using their "raw vols"? I.e. could garbage collection or data sharing cause the raw vols to become invalid? Even if the raw vols were valid but changed behind the scenes, such comparisons may be of dubious value if the result could change due to garbage collection or data sharing.
If vol comparison is reliable, would it be useful to have an eq or compare function in CInterface? Otherwise, could CInterface include isNull : vol -> bool ?
I am happy to have a go at a patch is this sounds useful.
Phil
On 11/11/11 20:18, Phil Clayton wrote:
I am currently implementing type t val null : t val isNull : t -> bool where type t = CInterface.vol. There is no problem doing this but I wondered whether I could improve the CInterface structure to avoid annoying little C library functions.
I have realized that C functions are not necessary to implement these - just to toClong and fromClong:
val null = toClong 0 fun isNull v = fromClong v = 0
Would it be at all controversial to include null : vol in CInterface?
For a different reason, this could still be useful. I had forgotten that volatiles do not persist in saved states or executables (it should have been obvious from the name) so I can't see how to create such a null value to implement
val null : t
where type t = CInterface.vol. (There is nothing volatile about null really.)
Perhaps the best approach here is to implement with type t = CInterface.vol option, with NONE representing null.
Phil
Phil, I think it could be possible to provide CInterface.null as a persistent vol pointing to a value containing (void*)0. I know that seems a contradiction but it should be possible. I'm just not sure it's necessary. Why do you need to have "null" and "isNull"? Have you considered instead building converters between the C data structure and ML and doing everything within ML. There's example of this in mlsource/extra/CInterface/Examples/ForeignTest.sml which converts a simple tree structure:
(* Example of creating a conversion for a datatype. *) datatype intTree = NullTree | Node of {left: intTree, right: intTree, valu: int};
(* The corresponding C structure is typedef struct _tree { struct _tree *left, *right; int nValue; } *tree; *)
On the your question about equality for vols: it's possible that there could be an equality test but I'm not sure it would be very useful. All it would do would test whether they were the same vol but that wouldn't tell you whether two vols contained the same C data.
Regards, David
On 13/11/2011 21:35, Phil Clayton wrote:
On 11/11/11 20:18, Phil Clayton wrote:
I am currently implementing type t val null : t val isNull : t -> bool where type t = CInterface.vol. There is no problem doing this but I wondered whether I could improve the CInterface structure to avoid annoying little C library functions.
I have realized that C functions are not necessary to implement these - just to toClong and fromClong:
val null = toClong 0 fun isNull v = fromClong v = 0
Would it be at all controversial to include null : vol in CInterface?
For a different reason, this could still be useful. I had forgotten that volatiles do not persist in saved states or executables (it should have been obvious from the name) so I can't see how to create such a null value to implement
val null : t
where type t = CInterface.vol. (There is nothing volatile about null really.)
Perhaps the best approach here is to implement with type t = CInterface.vol option, with NONE representing null.
Phil
polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
David,
My situation is slightly unusual so perhaps it's useful/interesting to explain some background. I'm working on support for GLib/GTK in SML which involves a significant number of calls to C functions. These C functions need wrapping to provide a suitable ML interface for various reasons. One such reason is for C string matters relating to optional strings using null pointers, in place modification and allocation which the caller must free. Given the number of C functions and the requirement for implementation across different SML compilers, I am creating a portable ML wrapping layer to reduce compiler-specific ML. For C strings, there is a module which provides various wrapping functions with a pointer-like abstract type cstring. It is this cstring type that has a null value.
So, on the one hand, I can actually just remove val null from the interface. A null cstring can be constructed via another function. However, it seems natural to have a null value. On the other hand, using vol option to implement a possibly-null pointer works (taking NONE as null and SOME v as possibly-null). However, it seems perverse having an ML datatype for nothing more than an actual C pointer.
Either way, a null pointer is going to create a new vol each time (as I understand it) which involves a small amount of allocation. Perhaps a persistent null : vol is worthwhile just from an efficiency perspective?
Regarding vol comparison, I actually meant comparison of the underlying C pointers. This was only motivated by considering the implementation of comparison with null, so probably not worth exploring.
Thanks, Phil
On 15/11/11 15:30, David Matthews wrote:
Phil, I think it could be possible to provide CInterface.null as a persistent vol pointing to a value containing (void*)0. I know that seems a contradiction but it should be possible. I'm just not sure it's necessary. Why do you need to have "null" and "isNull"? Have you considered instead building converters between the C data structure and ML and doing everything within ML. There's example of this in mlsource/extra/CInterface/Examples/ForeignTest.sml which converts a simple tree structure:
(* Example of creating a conversion for a datatype. *) datatype intTree = NullTree | Node of {left: intTree, right: intTree, valu: int};
(* The corresponding C structure is typedef struct _tree { struct _tree *left, *right; int nValue; } *tree; *)
On the your question about equality for vols: it's possible that there could be an equality test but I'm not sure it would be very useful. All it would do would test whether they were the same vol but that wouldn't tell you whether two vols contained the same C data.
Regards, David
On 13/11/2011 21:35, Phil Clayton wrote:
On 11/11/11 20:18, Phil Clayton wrote:
I am currently implementing type t val null : t val isNull : t -> bool where type t = CInterface.vol. There is no problem doing this but I wondered whether I could improve the CInterface structure to avoid annoying little C library functions.
I have realized that C functions are not necessary to implement these - just to toClong and fromClong:
val null = toClong 0 fun isNull v = fromClong v = 0
Would it be at all controversial to include null : vol in CInterface?
For a different reason, this could still be useful. I had forgotten that volatiles do not persist in saved states or executables (it should have been obvious from the name) so I can't see how to create such a null value to implement
val null : t
where type t = CInterface.vol. (There is nothing volatile about null really.)
Perhaps the best approach here is to implement with type t = CInterface.vol option, with NONE representing null.
Phil
polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
Phil> David, My situation is slightly unusual so perhaps it's Phil> useful/interesting to explain some background. I'm working on Phil> support for GLib/GTK in SML which involves a significant number of Phil> calls to C functions.
Last I knew, this was impossible in Poly/ML due to no callbacks from C. Has something crucial changed?
On 16/11/2011 04:15, Ian Zimmerman wrote:
Phil> David, My situation is slightly unusual so perhaps it's Phil> useful/interesting to explain some background. I'm working on Phil> support for GLib/GTK in SML which involves a significant number of Phil> calls to C functions.
Last I knew, this was impossible in Poly/ML due to no callbacks from C. Has something crucial changed?
The CInterface structure has had callbacks for a long time. They're only implemented on X86 but that covers the vast majority of users. There's an example in mlsource/extra/CInterface/Examples/ForeignTest.sml.
David
On 16/11/11 11:17, David Matthews wrote:
On 16/11/2011 04:15, Ian Zimmerman wrote:
Phil> David, My situation is slightly unusual so perhaps it's Phil> useful/interesting to explain some background. I'm working on Phil> support for GLib/GTK in SML which involves a significant number of Phil> calls to C functions.
Last I knew, this was impossible in Poly/ML due to no callbacks from C. Has something crucial changed?
The CInterface structure has had callbacks for a long time. They're only implemented on X86 but that covers the vast majority of users. There's an example in mlsource/extra/CInterface/Examples/ForeignTest.sml.
To clarify, callbacks are available on i386 but not x86_64.
I suspect those involved with large scale theorem proving will start moving to 64 bit OSes, if not already, so one application can address more than 4GB memory, as that amount of physical memory is becoming quite common these days.
Phil
On 16/11/2011 15:17, Phil Clayton wrote:
On 16/11/11 11:17, David Matthews wrote:
On 16/11/2011 04:15, Ian Zimmerman wrote:
Phil> David, My situation is slightly unusual so perhaps it's Phil> useful/interesting to explain some background. I'm working on Phil> support for GLib/GTK in SML which involves a significant number of Phil> calls to C functions.
Last I knew, this was impossible in Poly/ML due to no callbacks from C. Has something crucial changed?
The CInterface structure has had callbacks for a long time. They're only implemented on X86 but that covers the vast majority of users. There's an example in mlsource/extra/CInterface/Examples/ForeignTest.sml.
To clarify, callbacks are available on i386 but not x86_64.
I suspect those involved with large scale theorem proving will start moving to 64 bit OSes, if not already, so one application can address more than 4GB memory, as that amount of physical memory is becoming quite common these days.
Yes, you're correct. I'd forgotten that. I seem to recall that there was a problem with floating point on X86/64 but it may be possible to provide call-backs for functions that don't use them.
David
On 16/11/11 15:38, David Matthews wrote:
On 16/11/2011 15:17, Phil Clayton wrote:
On 16/11/11 11:17, David Matthews wrote:
On 16/11/2011 04:15, Ian Zimmerman wrote:
Phil> David, My situation is slightly unusual so perhaps it's Phil> useful/interesting to explain some background. I'm working on Phil> support for GLib/GTK in SML which involves a significant number of Phil> calls to C functions.
Last I knew, this was impossible in Poly/ML due to no callbacks from C. Has something crucial changed?
The CInterface structure has had callbacks for a long time. They're only implemented on X86 but that covers the vast majority of users. There's an example in mlsource/extra/CInterface/Examples/ForeignTest.sml.
To clarify, callbacks are available on i386 but not x86_64.
I suspect those involved with large scale theorem proving will start moving to 64 bit OSes, if not already, so one application can address more than 4GB memory, as that amount of physical memory is becoming quite common these days.
Yes, you're correct. I'd forgotten that. I seem to recall that there was a problem with floating point on X86/64 but it may be possible to provide call-backs for functions that don't use them.
The calling conventions for x86_64 appear to pass via registers not only the initial floating point arguments but also the initial int/pointer arguments: http://en.wikipedia.org/wiki/X86_calling_conventions So I suspect all arguments, not just floating point, would be an issue for callbacks on x86_64?
There is a separate issue with floats/doubles on x86_64 when calling from SML to C but that doesn't relate to callbacks. It looks like an exception is meant to be raised but isn't currently. (Perhaps the preprocessor symbol X86_64 should be HOSTARCHITECTURE_X86_64 in foreign.cpp?)
But now I have confused myself. If x86_64 calling conventions pass initial int/pointer args via registers as well as floating point args, what is it about double/float args that is problematic? (Comment foreign.cpp, line 1037.) Also, a comment (foreign.cpp, line 1041) suggests that the size of doubles is the issue but on x86_64 but pointers are also 8 bytes.
Phil
On 16/11/2011 18:07, Phil Clayton wrote:
The calling conventions for x86_64 appear to pass via registers not only the initial floating point arguments but also the initial int/pointer arguments: http://en.wikipedia.org/wiki/X86_calling_conventions So I suspect all arguments, not just floating point, would be an issue for callbacks on x86_64?
There is a separate issue with floats/doubles on x86_64 when calling from SML to C but that doesn't relate to callbacks. It looks like an exception is meant to be raised but isn't currently. (Perhaps the preprocessor symbol X86_64 should be HOSTARCHITECTURE_X86_64 in foreign.cpp?)
But now I have confused myself. If x86_64 calling conventions pass initial int/pointer args via registers as well as floating point args, what is it about double/float args that is problematic? (Comment foreign.cpp, line 1037.) Also, a comment (foreign.cpp, line 1041) suggests that the size of doubles is the issue but on x86_64 but pointers are also 8 bytes.
Right. Those preprocessor symbols are wrong. I think I changed them elsewhere in the code and somehow those got missed. I think the issue is that on X86/32 all arguments are passed on the stack but on the X86/64 integer-like arguments are passed in the general registers but floating point values are passed in floating-point registers. The code in apply_rec casts everything to (void*) which means that the foreign function will always be called with the arguments in the general registers even if it is expecting them in FP registers. This is frankly horrible and really this should be changed. Instead of interpreting the type information when the foreign function is called it should compile a stub which will convert the arguments into the correct format. I did find a project that would do something like that but it didn't deal with call-backs at all.
David
On 16/11/11 18:27, David Matthews wrote:
On 16/11/2011 18:07, Phil Clayton wrote:
The calling conventions for x86_64 appear to pass via registers not only the initial floating point arguments but also the initial int/pointer arguments: http://en.wikipedia.org/wiki/X86_calling_conventions So I suspect all arguments, not just floating point, would be an issue for callbacks on x86_64?
There is a separate issue with floats/doubles on x86_64 when calling from SML to C but that doesn't relate to callbacks. It looks like an exception is meant to be raised but isn't currently. (Perhaps the preprocessor symbol X86_64 should be HOSTARCHITECTURE_X86_64 in foreign.cpp?)
But now I have confused myself. If x86_64 calling conventions pass initial int/pointer args via registers as well as floating point args, what is it about double/float args that is problematic? (Comment foreign.cpp, line 1037.) Also, a comment (foreign.cpp, line 1041) suggests that the size of doubles is the issue but on x86_64 but pointers are also 8 bytes.
Right. Those preprocessor symbols are wrong. I think I changed them elsewhere in the code and somehow those got missed. I think the issue is that on X86/32 all arguments are passed on the stack but on the X86/64 integer-like arguments are passed in the general registers but floating point values are passed in floating-point registers. The code in apply_rec casts everything to (void*) which means that the foreign function will always be called with the arguments in the general registers even if it is expecting them in FP registers. This is frankly horrible and really this should be changed. Instead of interpreting the type information when the foreign function is called it should compile a stub which will convert the arguments into the correct format. I did find a project that would do something like that but it didn't deal with call-backs at all.
Thanks - knowing that everything is cast to (void *) makes the issue much clearer.
Phil
On 16/11/2011 20:27, Phil Clayton wrote:
On 16/11/11 18:27, David Matthews wrote:
On 16/11/2011 18:07, Phil Clayton wrote: Right. Those preprocessor symbols are wrong. I think I changed them elsewhere in the code and somehow those got missed. I think the issue is that on X86/32 all arguments are passed on the stack but on the X86/64 integer-like arguments are passed in the general registers but floating point values are passed in floating-point registers. The code in apply_rec casts everything to (void*) which means that the foreign function will always be called with the arguments in the general registers even if it is expecting them in FP registers. This is frankly horrible and really this should be changed. Instead of interpreting the type information when the foreign function is called it should compile a stub which will convert the arguments into the correct format. I did find a project that would do something like that but it didn't deal with call-backs at all.
Thanks - knowing that everything is cast to (void *) makes the issue much clearer.
Well, having decided that the existing code is horrible I bit the bullet and investigated libffi more closely. It turns out that it does everything we need including callbacks. I've now modified the foreign-function interface so that it will use libffi if it is available. As with GMP there is a configure option to control whether it is used and the default is to use it if it is there. It may need the development version of the libffi package with all the headers in order for configure to detect it.
So far I've tested callbacks on X86/32 and X86/64 and it all works. I haven't yet tested floating point on X86/64 but I'd expect it to work as well.
Regards, David
On 17/11/11 19:40, David Matthews wrote:
On 16/11/2011 20:27, Phil Clayton wrote:
On 16/11/11 18:27, David Matthews wrote:
On 16/11/2011 18:07, Phil Clayton wrote: Right. Those preprocessor symbols are wrong. I think I changed them elsewhere in the code and somehow those got missed. I think the issue is that on X86/32 all arguments are passed on the stack but on the X86/64 integer-like arguments are passed in the general registers but floating point values are passed in floating-point registers. The code in apply_rec casts everything to (void*) which means that the foreign function will always be called with the arguments in the general registers even if it is expecting them in FP registers. This is frankly horrible and really this should be changed. Instead of interpreting the type information when the foreign function is called it should compile a stub which will convert the arguments into the correct format. I did find a project that would do something like that but it didn't deal with call-backs at all.
Thanks - knowing that everything is cast to (void *) makes the issue much clearer.
Well, having decided that the existing code is horrible I bit the bullet and investigated libffi more closely. It turns out that it does everything we need including callbacks. I've now modified the foreign-function interface so that it will use libffi if it is available. As with GMP there is a configure option to control whether it is used and the default is to use it if it is there. It may need the development version of the libffi package with all the headers in order for configure to detect it.
Fantastic news! It makes a huge difference to me so I am very grateful. libffi seems like a neat idea - I hadn't heard of it.
libffi-devel is required for the headers on Fedora. (The rpm was already present on my system due to the presence of some GHC devel rpm.)
With Fedora, there is a minor configuration issue: like many packages, libffi headers are not installed on a standard path, so relies on pkg-config to supply cflags/libs arguments. I was able to build by simply adding symbolic links in /usr/include. After some investigation, it seems a more general solution can be achieved with the PKG_CHECK_MODULES macro in configure but I don't know whether Fedora is just an unusual case regarding libffi setup.
So far I've tested callbacks on X86/32 and X86/64 and it all works. I haven't yet tested floating point on X86/64 but I'd expect it to work as well.
In my mini-suite of FFI tests, all now work without issue on x86_64. This includes doubles as arguments. Great to see structs can now be used too!
Phil
On 18/11/2011 13:49, Phil Clayton wrote:
On 17/11/11 19:40, David Matthews wrote:
Well, having decided that the existing code is horrible I bit the bullet and investigated libffi more closely. It turns out that it does everything we need including callbacks. I've now modified the foreign-function interface so that it will use libffi if it is available. As with GMP there is a configure option to control whether it is used and the default is to use it if it is there. It may need the development version of the libffi package with all the headers in order for configure to detect it.
Fantastic news! It makes a huge difference to me so I am very grateful. libffi seems like a neat idea - I hadn't heard of it.
libffi-devel is required for the headers on Fedora. (The rpm was already present on my system due to the presence of some GHC devel rpm.)
With Fedora, there is a minor configuration issue: like many packages, libffi headers are not installed on a standard path, so relies on pkg-config to supply cflags/libs arguments. I was able to build by simply adding symbolic links in /usr/include. After some investigation, it seems a more general solution can be achieved with the PKG_CHECK_MODULES macro in configure but I don't know whether Fedora is just an unusual case regarding libffi setup.
So far I've tested callbacks on X86/32 and X86/64 and it all works. I haven't yet tested floating point on X86/64 but I'd expect it to work as well.
In my mini-suite of FFI tests, all now work without issue on x86_64. This includes doubles as arguments. Great to see structs can now be used too!
Phil
I'm glad it works for you. When I tested it with Debian and Ubuntu I had to install the development packages but otherwise it went smoothly. I'm considering adding libffi to the poly source since it's licensed under the BSD licence. I need to look at the configure script and see how easy it would be to merge it into the existing script. Relying on the packages complicates things particularly on Windows and it would be really nice to be able to get rid of the old FFI code.
David
David> I'm glad it works for you. When I tested it with Debian and David> Ubuntu I had to install the development packages but otherwise it David> went smoothly. I'm considering adding libffi to the poly source David> since it's licensed under the BSD licence.
I understand the appeal of this solution, but at least on Debian it is seriously frowned upon. The maintainer of the Debian package would probably have to undo it and use the pkg-config interface anyway to get the package accepted.
On 21/11/2011 16:45, Ian Zimmerman wrote:
David> I'm glad it works for you. When I tested it with Debian and David> Ubuntu I had to install the development packages but otherwise it David> went smoothly. I'm considering adding libffi to the poly source David> since it's licensed under the BSD licence.
I understand the appeal of this solution, but at least on Debian it is seriously frowned upon. The maintainer of the Debian package would probably have to undo it and use the pkg-config interface anyway to get the package accepted.
What is the problem? Is it the licensing or the inclusion of a library that is already separately available as a package? I was really considering it specifically for use on Windows where mingw/msys doesn't include pkg-config (though I did manage to find a version on the gtk download site, so it's not really an issue any more).
David
David> I'm glad it works for you. When I tested it with Debian and David> Ubuntu I had to install the development packages but otherwise it David> went smoothly. I'm considering adding libffi to the poly source David> since it's licensed under the BSD licence.
Ian> I understand the appeal of this solution, but at least on Debian it Ian> is seriously frowned upon. The maintainer of the Debian package Ian> would probably have to undo it and use the pkg-config interface Ian> anyway to get the package accepted.
David> What is the problem? Is it the licensing or the inclusion of a David> library that is already separately available as a package? I was David> really considering it specifically for use on Windows where David> mingw/msys doesn't include pkg-config (though I did manage to David> find a version on the gtk download site, so it's not really an David> issue any more).
As I understand it, the objection to embedding external library sources is twofold: both "philosophical" and practical.
The philosophical part is that Debian tries to do The Right Thing (TM) even if it is hard, and I think that we can all agree that The Right Thing in this context is to link to an existing shared library as opposed to embedding the source.
The practical part has mostly to do with security fixes. If a vulnerability is discovered in libffi, there is no way to scan the sources of all the ~30k packages and hunt for those that might contain a copy of libffi to fix them.
On 23/11/2011 07:35, Ian Zimmerman wrote:
David> I'm glad it works for you. When I tested it with Debian and David> Ubuntu I had to install the development packages but otherwise it David> went smoothly. I'm considering adding libffi to the poly source David> since it's licensed under the BSD licence.
Ian> I understand the appeal of this solution, but at least on Debian it Ian> is seriously frowned upon. The maintainer of the Debian package Ian> would probably have to undo it and use the pkg-config interface Ian> anyway to get the package accepted.
David> What is the problem? Is it the licensing or the inclusion of a David> library that is already separately available as a package? I was David> really considering it specifically for use on Windows where David> mingw/msys doesn't include pkg-config (though I did manage to David> find a version on the gtk download site, so it's not really an David> issue any more).
As I understand it, the objection to embedding external library sources is twofold: both "philosophical" and practical.
The philosophical part is that Debian tries to do The Right Thing (TM) even if it is hard, and I think that we can all agree that The Right Thing in this context is to link to an existing shared library as opposed to embedding the source.
The practical part has mostly to do with security fixes. If a vulnerability is discovered in libffi, there is no way to scan the sources of all the ~30k packages and hunt for those that might contain a copy of libffi to fix them.
Fine. By "adding libffi to the poly source" I wasn't implying that when poly was compiled it would only use that version of libffi. I had in mind the idea that a user/packager would be able to override this and use the version installed on the system. I can envisage situations where the version of libffi on the system might be tailored for the system and the user might want to force poly to use that in preference.
If libffi were like the C/C++ libraries and available consistently on all platforms there would be no need to consider including it in the source. However, it's becoming clear that on a significant range of platforms using it would require users to install libffi from source and/or to make non-trivial tweaks to their system. I think it's important to try and ensure that when users download the tar-ball from Sourceforge they should be able to compile and install Poly/ML with the least amount of trouble. It looks like that can best be achieved by including libffi within the source and building with that by default. Packagers and users with special requirements can override that if they need to. That approach would seem to overcome any objections.
David
David> If libffi were like the C/C++ libraries and available David> consistently on all platforms there would be no need to consider David> including it in the source. However, it's becoming clear that on David> a significant range of platforms using it would require users to David> install libffi from source and/or to make non-trivial tweaks to David> their system. I think it's important to try and ensure that when David> users download the tar-ball from Sourceforge they should be able David> to compile and install Poly/ML with the least amount of trouble. David> It looks like that can best be achieved by including libffi David> within the source and building with that by default. Packagers David> and users with special requirements can override that if they David> need to. That approach would seem to overcome any objections.
Yes, it is quite common to have an autoconf option like --with-system-libffi to force linking to an existing shared library. I don't think there would be any objection to that.
Thanks for entering into this boring discussion ;-)
On 24/11/2011 17:34, Ian Zimmerman wrote:
Yes, it is quite common to have an autoconf option like --with-system-libffi to force linking to an existing shared library. I don't think there would be any objection to that.
I've now added libffi to the Poly/ML source. I was trying to find a good name for the option to select building without the internal version of libffi and --with-system-libffi seemed a good choice. So, if ./configure is run without any option it will use the version included in the source. If --with-system-libffi is given it tries to use pkg-config to find libffi and if that fails it looks for the library and header files using the default paths. With a bit of luck that should mean that Poly/ML will build without needing anything special on all the platforms we support.
David
On Tue, 29 Nov 2011, David Matthews wrote:
On 24/11/2011 17:34, Ian Zimmerman wrote:
Yes, it is quite common to have an autoconf option like --with-system-libffi to force linking to an existing shared library. I don't think there would be any objection to that.
I've now added libffi to the Poly/ML source. I was trying to find a good name for the option to select building without the internal version of libffi and --with-system-libffi seemed a good choice. So, if ./configure is run without any option it will use the version included in the source.
I have tried this version 1379 successfully on my usual build platforms, using the builtin libffi sources: Linux, Mac OS Leopart, Mac OS Snow Leopard, Cygwin, both with x86/x86_64 in various combinations. Our libsha1 module also works as expected.
Makarius
On 29/11/11 18:09, David Matthews wrote:
On 24/11/2011 17:34, Ian Zimmerman wrote:
Yes, it is quite common to have an autoconf option like --with-system-libffi to force linking to an existing shared library. I don't think there would be any objection to that.
I've now added libffi to the Poly/ML source. I was trying to find a good name for the option to select building without the internal version of libffi and --with-system-libffi seemed a good choice. So, if ./configure is run without any option it will use the version included in the source. If --with-system-libffi is given it tries to use pkg-config to find libffi and if that fails it looks for the library and header files using the default paths. With a bit of luck that should mean that Poly/ML will build without needing anything special on all the platforms we support.
I've just tried r1380 on my Fedora 15 x86_64 machine and have a couple of things to report:
1. I get a build error (see output below) for foreign.cpp. Perhaps my C compiler is more pedantic than most but it is just using the default options. I think the issue is that, on x86_64, void * is 8 bytes but unsigned (int) is 4 bytes.
2. When I specify --with-system-libffi, I see that configure still runs for the libffi bundled with Poly/ML. Perhaps that is intentional.
Phil
/bin/sh ../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. -I.. -I/usr/lib64/libffi-3.0.10/include -Wall -O3 -MT foreign.lo -MD -MP -MF .deps/foreign.Tpo -c -o foreign.lo foreign.cpp libtool: compile: g++ -DHAVE_CONFIG_H -I. -I.. -I/usr/lib64/libffi-3.0.10/include -Wall -O3 -MT foreign.lo -MD -MP -MF .deps/foreign.Tpo -c foreign.cpp -fPIC -DPIC -o .libs/foreign.o foreign.cpp: In function 'void callbackEntryPt(ffi_cif*, void*, void**, void*)': foreign.cpp:1505:34: error: cast from 'void*' to 'unsigned int' loses precision [-fpermissive] foreign.cpp: In function 'SaveVecEntry* createCallbackFunction(TaskData*, Handle, ffi_abi)': foreign.cpp:1588:84: warning: cast to pointer from integer of different size [-Wint-to-pointer-cast] make[2]: *** [foreign.lo] Error 1 make[2]: Leaving directory `/home/pclayton/SML/PolyML/svn/trunk/polyml/libpolyml' make[1]: *** [all-recursive] Error 1 make[1]: Leaving directory `/home/pclayton/SML/PolyML/svn/trunk/polyml' make: *** [all] Error 2
On 01/12/2011 16:09, Phil Clayton wrote:
I've just tried r1380 on my Fedora 15 x86_64 machine and have a couple of things to report:
- I get a build error (see output below) for foreign.cpp. Perhaps my C
compiler is more pedantic than most but it is just using the default options. I think the issue is that, on x86_64, void * is 8 bytes but unsigned (int) is 4 bytes.
Thanks. That was a change I made when I tested it with the Windows interface. One of my examples created a lot of callback functions and showed up a bug that hadn't previously appeared. I've now changed this to use uintptr_t rather than "unsigned" so it seems to be fine on my X86/64 setup.
- When I specify --with-system-libffi, I see that configure still runs
for the libffi bundled with Poly/ML. Perhaps that is intentional.
It is intentional. While searching for information on how to configure a sub-directory that had its own configure script I came across a document that suggested that it was best to configure the sub-directory even if it was not actually built. That would then ensure that things like "make dist" work properly.
David
On 01/12/11 17:31, David Matthews wrote:
On 01/12/2011 16:09, Phil Clayton wrote:
I've just tried r1380 on my Fedora 15 x86_64 machine and have a couple of things to report:
- I get a build error (see output below) for foreign.cpp. Perhaps my C
compiler is more pedantic than most but it is just using the default options. I think the issue is that, on x86_64, void * is 8 bytes but unsigned (int) is 4 bytes.
Thanks. That was a change I made when I tested it with the Windows interface. One of my examples created a lot of callback functions and showed up a bug that hadn't previously appeared. I've now changed this to use uintptr_t rather than "unsigned" so it seems to be fine on my X86/64 setup.
Thanks - all is working now.
- When I specify --with-system-libffi, I see that configure still runs
for the libffi bundled with Poly/ML. Perhaps that is intentional.
It is intentional. While searching for information on how to configure a sub-directory that had its own configure script I came across a document that suggested that it was best to configure the sub-directory even if it was not actually built. That would then ensure that things like "make dist" work properly.
Good point. I would certainly want "make distclean" to clean out everything.
Phil
On 18/11/2011 13:49, Phil Clayton wrote:
With Fedora, there is a minor configuration issue: like many packages, libffi headers are not installed on a standard path, so relies on pkg-config to supply cflags/libs arguments. I was able to build by simply adding symbolic links in /usr/include. After some investigation, it seems a more general solution can be achieved with the PKG_CHECK_MODULES macro in configure but I don't know whether Fedora is just an unusual case regarding libffi setup.
I've updated configure to use PKG_CHECK_MODULES and it works for me on Debian as before. I've also managed to get it work with mingw once I sorted out pkg-config. Can you check that it now works for you without the symbolic links?
David
On 21/11/11 11:33, David Matthews wrote:
On 18/11/2011 13:49, Phil Clayton wrote:
With Fedora, there is a minor configuration issue: like many packages, libffi headers are not installed on a standard path, so relies on pkg-config to supply cflags/libs arguments. I was able to build by simply adding symbolic links in /usr/include. After some investigation, it seems a more general solution can be achieved with the PKG_CHECK_MODULES macro in configure but I don't know whether Fedora is just an unusual case regarding libffi setup.
I've updated configure to use PKG_CHECK_MODULES and it works for me on Debian as before. I've also managed to get it work with mingw once I sorted out pkg-config. Can you check that it now works for you without the symbolic links?
This now works on Fedora 15 x86_64 without the symbolic links. I also tested Fedora 12 x86_64 with and without the libffi-devel package and both scenarios worked 'out of the box' i.e. no sym links required.
I also ran tests on a Fedora 14 i386 machine. These were not to successful. Without libffi, build failed during 'make' - see attached file log-nolibffi-f14-i386.txt. With libffi, a callback caused a seg fault. I can supply an example but wondered if you were still tweaking the i386 stuff?
One minor comment: for x86_64, the Foreign exn message for structs and doubles could, perhaps, usefully indicate libffi is required like it now does for callbacks.
Phil
On 21/11/2011 14:19, Phil Clayton wrote:
On 21/11/11 11:33, David Matthews wrote: This now works on Fedora 15 x86_64 without the symbolic links. I also tested Fedora 12 x86_64 with and without the libffi-devel package and both scenarios worked 'out of the box' i.e. no sym links required.
I also ran tests on a Fedora 14 i386 machine. These were not to successful. Without libffi, build failed during 'make' - see attached file log-nolibffi-f14-i386.txt. With libffi, a callback caused a seg fault. I can supply an example but wondered if you were still tweaking the i386 stuff?
One minor comment: for x86_64, the Foreign exn message for structs and doubles could, perhaps, usefully indicate libffi is required like it now does for callbacks.
Phil
I've fixed a problem with the non-libffi callback code so it now seems to compile without libffi. I don't understand the seg-fault with libffi and Fedora 14. Perhaps there's a problem with the version of the library in that version. I don't have any easy way of testing it myself so any debugging you can do would be helpful.
Now I've managed to get libffi working in mingw/msys I'm rather inclined to remove the non-libffi code completely. The build process for Poly/ML would then not include the CInterface structure at all if libffi were not installed, much like X-windows.
David
On 21/11/11 16:46, David Matthews wrote:
On 21/11/2011 14:19, Phil Clayton wrote:
On 21/11/11 11:33, David Matthews wrote: This now works on Fedora 15 x86_64 without the symbolic links. I also tested Fedora 12 x86_64 with and without the libffi-devel package and both scenarios worked 'out of the box' i.e. no sym links required.
I also ran tests on a Fedora 14 i386 machine. These were not to successful. Without libffi, build failed during 'make' - see attached file log-nolibffi-f14-i386.txt. With libffi, a callback caused a seg fault. I can supply an example but wondered if you were still tweaking the i386 stuff?
One minor comment: for x86_64, the Foreign exn message for structs and doubles could, perhaps, usefully indicate libffi is required like it now does for callbacks.
Phil
I've fixed a problem with the non-libffi callback code so it now seems to compile without libffi. I don't understand the seg-fault with libffi and Fedora 14. Perhaps there's a problem with the version of the library in that version. I don't have any easy way of testing it myself so any debugging you can do would be helpful.
I have tried libffi 3.10.0 and the latest 3.11.0-rc2 and the seg fault still occurs. I've attached a simple example but it's nothing special.
I can explain what is happening, but not ultimately why.
The seg fault occurs when attempting to call a function pointer passed to a C foreign function. It is hard to say whether the pointer is duff. The pointer value was created by the call to ffi_closure_alloc in foreign.cpp, line 1841 and returned in resultFunction. For the attached example, the function pointer, written to resultFunction, is 0x115008 and closure, the return value of ffi_closure_alloc, is 0x116008. (On my x86_64 machine, resultFunction is 4K higher, not lower.)
When debugging, if I set cb1 to 0x116008 instead, it all works - no seg fault. I don't understand why calling 0x116008 (closure) works and 0x115008 (resultFunction) doesn't: the comments in ffi_closure_alloc suggest that resultFunction is "the executable corresponding virtual address" of closure.
Now I've managed to get libffi working in mingw/msys I'm rather inclined to remove the non-libffi code completely. The build process for Poly/ML would then not include the CInterface structure at all if libffi were not installed, much like X-windows.
Given the extensive list of platforms supported by libffi, that seems reasonable. Is it just me who has this issue with i386/Linux then? (Personally, I only need x86_64.)
Phil
On 22/11/2011 16:35, Phil Clayton wrote:
On 21/11/11 16:46, David Matthews wrote:
I have tried libffi 3.10.0 and the latest 3.11.0-rc2 and the seg fault still occurs. I've attached a simple example but it's nothing special.
I can explain what is happening, but not ultimately why.
The seg fault occurs when attempting to call a function pointer passed to a C foreign function. It is hard to say whether the pointer is duff. The pointer value was created by the call to ffi_closure_alloc in foreign.cpp, line 1841 and returned in resultFunction. For the attached example, the function pointer, written to resultFunction, is 0x115008 and closure, the return value of ffi_closure_alloc, is 0x116008. (On my x86_64 machine, resultFunction is 4K higher, not lower.)
When debugging, if I set cb1 to 0x116008 instead, it all works - no seg fault. I don't understand why calling 0x116008 (closure) works and 0x115008 (resultFunction) doesn't: the comments in ffi_closure_alloc suggest that resultFunction is "the executable corresponding virtual address" of closure.
Thanks for testing the patch we discussed off-line. I've now committed it so it looks like this is fixed.
Now I've managed to get libffi working in mingw/msys I'm rather inclined to remove the non-libffi code completely. The build process for Poly/ML would then not include the CInterface structure at all if libffi were not installed, much like X-windows.
Given the extensive list of platforms supported by libffi, that seems reasonable. Is it just me who has this issue with i386/Linux then? (Personally, I only need x86_64.)
libffi runs on all the platforms I've tried but there are issues with packages which makes it difficult to rely on using an external package to build Poly/ML. As well as mingw/mys there is a problem with Cygwin. Although libffi is available as a binary library there is no development package with the headers and link library so building on Cygwin is going to require the libffi sources. Cygwin is an important platform for Isabelle so Poly/ML needs to be able to build fairly easily on it.
David
On 16 Nov 2011, at 15:17, Phil Clayton wrote:
I suspect those involved with large scale theorem proving will start moving to 64 bit OSes, if not already, so one application can address more than 4GB memory, as that amount of physical memory is becoming quite common these days.
Seconded: at least one user of ProofPower (me) and many users of Isabelle are already in that situation.
Regards,
Rob.
On Wed, 16 Nov 2011, Rob Arthan wrote:
On 16 Nov 2011, at 15:17, Phil Clayton wrote:
I suspect those involved with large scale theorem proving will start moving to 64 bit OSes, if not already, so one application can address more than 4GB memory, as that amount of physical memory is becoming quite common these days.
Seconded: at least one user of ProofPower (me) and many users of Isabelle are already in that situation.
Yes, the big applications are already using x86_64 routinely, with 8-32 GB memory requirement. Pretty soon, x86 will be only for "small" portable devices.
I've occasionally asked myself about the future of the Cygwin platform for Isabelle users, and was starting to think of MinGW 64 instead. Fortunately, the Cygwin maintainers have recently woke up, and made some initial moves towards proper x86_64 support.
Makarius
On 16/11/2011 17:15, Makarius wrote:
On Wed, 16 Nov 2011, Rob Arthan wrote:
On 16 Nov 2011, at 15:17, Phil Clayton wrote:
I suspect those involved with large scale theorem proving will start moving to 64 bit OSes, if not already, so one application can address more than 4GB memory, as that amount of physical memory is becoming quite common these days.
Seconded: at least one user of ProofPower (me) and many users of Isabelle are already in that situation.
Yes, the big applications are already using x86_64 routinely, with 8-32 GB memory requirement. Pretty soon, x86 will be only for "small" portable devices.
OK. I've now added CInterface.null as a persistent vol (the only one) containing (void*)0. It should be possible to test for null by using fromClong x = 0.
I've just started thinking about how to do callbacks for X86/64. They're more complicated than for X86/32 because some arguments are in registers but I think I can probably get round this.
The other issue for X86/64 is that CInterface doesn't currently support calling foreign functions with floating point arguments. Getting this to work would require some big changes to the code.
David
On 16/11/11 17:59, David Matthews wrote:
On 16/11/2011 17:15, Makarius wrote:
On Wed, 16 Nov 2011, Rob Arthan wrote:
On 16 Nov 2011, at 15:17, Phil Clayton wrote:
I suspect those involved with large scale theorem proving will start moving to 64 bit OSes, if not already, so one application can address more than 4GB memory, as that amount of physical memory is becoming quite common these days.
Seconded: at least one user of ProofPower (me) and many users of Isabelle are already in that situation.
Yes, the big applications are already using x86_64 routinely, with 8-32 GB memory requirement. Pretty soon, x86 will be only for "small" portable devices.
OK. I've now added CInterface.null as a persistent vol (the only one) containing (void*)0. It should be possible to test for null by using fromClong x = 0.
All built and working! Many thanks. I'll be glad to ditch the vol option approach. Also, the Foreign exception is now working as expected for double arguments.
I've just started thinking about how to do callbacks for X86/64. They're more complicated than for X86/32 because some arguments are in registers but I think I can probably get round this.
The other issue for X86/64 is that CInterface doesn't currently support calling foreign functions with floating point arguments. Getting this to work would require some big changes to the code.
From my perspective, callbacks on x86_64 are more important but I accept that any design would need to consider both for the long run.
Phil
-
David.Matthews＠prolingua.co.uk -
itz＠buug.org -
makarius＠sketis.net -
phil.clayton＠lineone.net -
rda＠lemma-one.com