-
Notifications
You must be signed in to change notification settings - Fork 95
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Support for gmp? #643
Comments
I expect this can be built on top of Ctypes. Since |
I tried to provide a bit more information to @disteph about how to do this, but I realized that this is rather difficult -- I don't know how to do it. (I'm unfamiliar with Ctypes.) Context:
A first idea (which I believe does not work) is to first bind the (* this type represents mpz_t values from the OCaml side *)
type mpz_t = unit ptr (* inspired from examples/ncurses *)
(* C-type for mpz_t *)
let mpz_t : mpz_t typ = ptr void (* inspired from examples/ncurses *)
(* bindings to conversion functions implemented in C (zarith.h or other glue) *)
external zarith_of_mpz : mpz_t -> Zarith.t = "ml_z_from_mpz"
external mpz_of_zarith : Zarith.t -> mpz_t = "?"
(* C-type for Zarith.t *)
let zarith = view ~read:zarith_of_mpz ~write:mpz_of_zarith However, I believe that this approach is incorrect: I think that this is a fundamental issue with Ctypes+Zarith: the conversion functions between |
I was trying the first way, hoping that the conversion from Ctypes representations of C values to naked C values could be simply done in C with
(using But I feel I'm completely out of my depth here. |
The wrapping of zarith.c attempted above was inspired by Zarith's implementation of conversion functions to/from MLGMPIDL, an Ocaml wrapper of GMP, and I was hoping that Ctypes's representation of an But then I'm still stuck with mundane build/linking problems. And perhaps my assumption above is incorrect, or perhaps Ctypes people would approach the problem in a different way :-) I'd be happy to hear. |
@disteph one problem I see with writing your own conversion functions on the C side is that it is not clear, to me, how to get Ctypes to automatically use them when binding third-party C functions to the OCaml world. If you have to write your own C-side wrapper of each third-party function, and then connect this to the OCaml world to ctypes, you lose a part of the value of the tool. (But maybe I misunderstood your approach.) Another approach I considered recently is: instead of trying to use type mpz_t = unit ptr
let mpz_t : mpz_t typ = ptr void
let zarith_of_mpz : mpz_t -> Zarith.t = Cstubs.foreign "ml_z_from_mpz" (mpz_t @-> returning ??)
let mpz_of_zarith : Zarith.t -> mpz_t = Cstubes.foreign "??" (?? @-> returning mpz_t)
let zarith : Zarith.t typ = view mpz_t ~read:zarith_of_mpz ~write:mpz_of_zarith This solves the problem on the |
Well indeed, using Ctypes to bind third-party functions manipulating But I agree it'd be much better to have Ctypes representations of Zarith types, with a handler |
Ctypes can't deal with custom blocks created by hand-written third party libraries. /* from_zarith writes a Z.t value (first parameter) to the location
pointed to by the second parameter. nativeints are used to
store pointers. */
CAMLprim value from_zarith(value zt, value np)
{
CAMLparam2(zt,np);
/* study zariths source code for details */
mpz_t mp = zarith_representation_to_plain_c(zt);
*((mpz_t *)Nativeint_val(np)) = mp;
CAMLreturn(Val_unit);
}
/* reverse: *mpz_t to Z.t */
CAMLprim value to_zarith(value v)
{
CAMLparam1(v);
CAMLlocal1(res);
mpz_t m = *((mpz_t *) Nativeint_val(v));
/* study zariths source code for details again */
res = convert_to_zarith_representation(m);
CAMLreturn(res);
} Now you can define the type with Ctypes and connect both (memory management and other details ignored) type mpz_struct
let mpz_struct : mpz_struct Ctypes.structure Ctypes.typ =
Ctypes.typedef (Ctypes.structure "") "__mpz_struct"
let _x = Ctypes.field mpz_struct "_mp_foo" Ctypes.int
(* more fields *)
let () = Ctypes.seal mpz_struct
external from_zarith : Z.t -> nativeint -> unit = "from_zarith"
let from_zarith x =
let res = Ctypes.allocate_n mpz_struct ~count:1 in
Ctypes.to_voidp res |> Ctypes.raw_address_of_ptr |> from_zarith x;
res
external to_zarith : nativeint -> Z.t = "to_zarith"
let to_zarith (x:mpz_struct Ctypes.structure Ctypes.ptr) =
Ctypes.to_voidp x |> Ctypes.raw_address_of_ptr |> to_zarith
(* simplification. mpz_t only decays to a pointer, when used
as function parameter ... *)
let mpz_t_fparam : Z.t Ctypes.typ =
Ctypes.view
~format_typ:(fun k fmt -> Format.fprintf fmt "mpz_ptr%t" k)
~read:to_zarith
~write:from_zarith
(Ctypes.ptr mpz_struct)
let mpz_t_frparam = Ctypes.typedef (Ctypes.ptr mpz_struct) "mpz_ptr"
let add =
Foreign.foreign "mpz_add"
(mpz_t_frparam @-> mpz_t_fparam @-> mpz_t_fparam @-> returning void)
let add : Z.t -> Z.t -> Z.t =
fun a b ->
let res = Ctypes.allocate_n mpz_struct ~count:1 in
add res a b;
to_zarith res It's of course rather inefficient because of all the allocations and switches between C and the OCaml runtime that would not be necessary, if you write your stubs manually.... |
@fdopen Thanks for the suggestion; I had thought about something along those lines but I discarded it as "not the right way to do it", but thinking about it more it may at least provide a working (if unpleasant) solution to what I was trying to do. I don't think that we need extra allocations to use the idea of wrapping pointers as native integers. We should be able to use Ctypes' own support for this: we can move from a This gives the following sketch: (* C-type for mpz_ptr *)
type mpz_ptr = unit ptr
let mpz_ptr : mpz_ptr typ = ptr void (* inspired from examples/ncurses *)
(* mpz_ptr wrapped as a nativeint *)
let mpz_nativeint = view mpz_ptr ~read:raw_address_of_ptr ~write:ptr_of_raw_address
(* bindings to conversion functions implemented in C,
unwrapping the nativeint before calling zarith.h conversions *)
external zarith_of_mpz_nativeint : nativeint -> Zarith.t = "ml_z_from_mpz_nativeint"
external mpz_nativeint_of_zarith : Zarith.t -> nativeint = "?"
(* C-type for Zarith.t *)
let zarith = view mpz_nativeint ~read:zarith_of_mpz_nativeint ~write:mpz_nativeint_of_zarith I am not completely sure that this use of |
(Note: in practice the API of |
It can't be avoided for the reason you've already mentioned: the garbage collector. Just look at the mentioned mpz_add function whose prototype boils down to something like this (with all constness and obfuscation through typedefs removed): void mpz_add (*__mpz_struct,*__mpz_struct,*__mpz_struct); The function takes pointers to structures. And it's just not possible to convert Zarith.t values to a usable pointer on the fly. A Z.t value might be a plain integer, passed by value, without address. And if it is a custom block, you can't point to anything inside it, because it could be shuffled around by the GC. Another parameter of the function could be created through a Ctypes.view whose functions trigger the GC. So the pointer you’ve created with your view could already be invalid once it reaches the c function. Therefore the view must create deep copies.
I didn't know this header. But now I've read it and seems to provide anything necessary to implement the functions suggested by me: CAMLprim value from_zarith(value zt, value np)
{
CAMLparam2(zt,np);
mpz_ptr ptr = (mpz_ptr)Nativeint_val(np);
ml_z_mpz_init_set_z(ptr, zt);
CAMLreturn(Val_unit);
}
CAMLprim value to_zarith(value v)
{
CAMLparam1(v);
CAMLlocal1(res);
mpz_ptr ptr = (mpz_ptr)Nativeint_val(v);
res = ml_z_from_mpz(ptr);
CAMLreturn(res);
} |
@fdopen I don't disagree but I think we are talking past each other. What I tried to do above is in fact to find a generic solution for the following problem: binding C functions that use a C type This sounds like a fairly common pattern to me, and I would have expected Ctypes to support it easily. As my hesitations show, this is not the case, at least for someone unexperienced with Ctypes. I currently think that the best way to do it, at least when
I am not sure if there would be a better way to do this today with Ctypes (an example of this in |
Re. deep vs. shallow copies: thanks for insisting on the fact that the However, this is not necessary for a first approach to mpz/Zarith binding, the zarith.c functions (which do perform a copy) are the easiest way to proceed. In any case I don't think that copying the bigints is a performance bottleneck for @disteph's applications -- hopefully the bigint-taking functions are long enough to run that this is amortized. |
Ctypes needs to know the internals on any C type: size, etc. These information are necessary for memory management and for code generation (either source code or dynamic through libffi). Therefore the definiton of the C type must be repeated through Ctypes primitives. The connection to your own type is then covered by Ctypes.view. If one also has to write C code, my syntax extension can be helpful. It allows to switch easily between C and OCaml. I've uploaded example code: Line 6 defines the primary Ctypes.typ and line Line 15 and Line 28 demonstrate how to convert an OCaml type at the C level to something that was described earlier as a Ctypes.typ.
Two allocations in C in this case. The first for the structure that is passed to
What about error handling? You've transformed the first two parameters, but it doesn't work for the third one: Out of memory. The useless allocated ressources for the previous params must be cleaned up, before you can return an error value. |
Thanks for the in-depth discussion and the proposed code at https://github.com/fdopen/ctypes-zarith. Yes, the ppx_cstubs is neat!
but some API functions of our SMT-solver Yices; the heavy computation is done in C and I just want the input / output of it to be something that the user can then make sense of in the rest of their OCaml program, via Zarith. |
Thank you for the discussion and the code example. Still it seems that having a |
Feature request:
Would it be possible to have ctypes bridge gmp types with zarith types or mlgmpidl types?
I.e., in the same way that
let ml_function = Foreign.foreign "c_function" Ctypes.(long @-> ...)
wraps a C function taking an argument of (C) type
long
as an ML function of typeSigned.long ->...
,let ml_function = Foreign.foreign "c_function" Ctypes.(mpz @-> ...)
would wrap a C function taking an argument of (C) type
mpz_t
as an ML function of typeZ.t -> ...
for a type handler
val mpz : Z.t Ctypes.typ
?
Is this something I can do myself as syntactic sugar on top of what exists? My trouble was that the types Z.t/Q.t in Zarith or their counter-part in mlgmpidl are abstract and I don't see how I can represent them in the Ctypes world...
The text was updated successfully, but these errors were encountered: