Consider handling ocaml-ctypes bindings in the presence of undefined C abstract types that are only manipulated through pointers

[msprotz]

Hello @victor-dumitrescu,

Son and I were debugging bindings a little further, and we found the interesting use-case below:

module Test

module B = LowStar.Buffer
module ST = FStar.HyperStack.ST

open FStar.HyperStack.ST

[@ CAbstractStruct ]
type t = {
  x: UInt32.t;
  y: UInt128.t;
}

type u = B.pointer t

let create (): St u =
  B.malloc FStar.HyperStack.root ({ x = 0ul; y = Int.Cast.Full.uint64_to_uint128 0UL }) 1ul

what happens here is that t is a "C abstract struct", i.e. it is not defined in the header, meaning that any function in the header will pass pointers to it.

typedef struct Test_t_s Test_t;

Test_t *Test_create();

This is a standard C programming idiom that forces clients of this header to go through the allocation functions exposed in the header, and prevents clients from seeing the internal definition of the struct type. (This is the best you can get in terms of abstraction in C).

Here, the type t cannot be described in ocaml-ctype's DSL, because it uses the uint128 type. However, if there was a way to bind the type t as an opaque type, then we could happily let ocaml clients manipulate opaque pointers to a struct whose definition has not been exposed by ocaml-ctypes.

Do you know if this is something that's feasible in ocaml-ctypes and whether we could have support for it? That way, we would make sure that i) kremlin's ctypes generation honors C abstract types and ii) Son's code, which uses non-bindable types but only behind a pointer, compiles properly.

Right now, this is what the bindings file contains:

open Ctypes
module Bindings(F:Cstubs.FOREIGN) =
  struct
    open F
    let test_create =
      foreign "Test_create" (void @-> (returning (ptr test_t)))

is there any way to do

let test_t = opaque "Test_t"

?

Thanks!

Jonathan

[victor-dumitrescu]

Assuming I understood the situation correctly, I think this is something we already do in other places, for example, in EverCrypt.AEAD.fsti

[@CAbstractStruct]
val state_s: alg -> Type0

gets compiled to typedef struct EverCrypt_AEAD_state_s_s EverCrypt_AEAD_state_s; in EverCrypt_AEAD.h and gets this Ctypes binding:

    type everCrypt_AEAD_state_s = [ `everCrypt_AEAD_state_s ] structure
    let (everCrypt_AEAD_state_s : [ `everCrypt_AEAD_state_s ] structure typ)
      = structure "EverCrypt_AEAD_state_s_s"

Values of this type are then created and manipulated in client code only through the provided functions, e.g.

    let everCrypt_AEAD_encrypt =
      foreign "EverCrypt_AEAD_encrypt"
        ((ptr everCrypt_AEAD_state_s) @->
           (ocaml_bytes @-> ... )

So I'd say this is definitely something doable, it just seems not to work as intended for your use case. I think that something like the above

    type test_t = [ `test_t ] structure
    let (test_t : [ `test_t ] structure typ)
      = structure "Test_t_s"

would make it work, but I'm not sure why it's not there. It might be because since t contains an unsupported type we decided not to bind it, ignoring the fact that it's supposed to remain abstract anyway.

[msprotz]

Ah yes indeed it looks C abstract structs are already handled. Then as you say, fixing this bug is just a matter of making sure that binding generation code works in the presence of a C abstract struct whose underlying representation cannot be expressed in the ocaml-ctypes DSL.

Thanks for the excellent analysis. Do you think that's someone you could easily fix?

[victor-dumitrescu]

I added this functionality (along with tests) but actually I was wrong when I described the current situation above. In fact the type everCrypt_AEAD_state_s is bound just like any other struct, ignoring the abstract flag. Its actual binding is

    type everCrypt_AEAD_state_s = [ `everCrypt_AEAD_state_s ] structure
    let (everCrypt_AEAD_state_s : [ `everCrypt_AEAD_state_s ] structure typ)
      = structure "EverCrypt_AEAD_state_s_s"
    let everCrypt_AEAD_state_s_impl =
      field everCrypt_AEAD_state_s "impl" spec_Cipher_Expansion_impl
    let everCrypt_AEAD_state_s_ek =
      field everCrypt_AEAD_state_s "ek" (ptr uint8_t)
    let _ = seal everCrypt_AEAD_state_s

For the moment I only added opaque bindings for abstract structs that would not have been otherwise bound, like in your example. But perhaps it would be good to treat all abstract structs in this way?

[msprotz]

Hi Victor,

Thanks for fixing this issue so promptly, this is really great!

For the moment I only added opaque bindings for abstract structs that would not have been otherwise bound, like in your example.

This is great and unblocks us, so let's merge this.

But perhaps it would be good to treat all abstract structs in this way?

Absolutely, if that's not too much work, I think a followup patch that makes the behavior more uniform would be top-notch!

[victor-dumitrescu]

Shouldn't be too much work but I'll have to check that it doesn't break HACL

[msprotz]

Unfortunately we are not exactly unblocked:

Fatal error: exception Ctypes_static.IncompleteType
Raised at file "src/ctypes/ctypes_static.ml", line 140, characters 40-60
Called from file "src/ctypes/ctypes_structs_computed.ml", line 31, characters 44-61
Called from file "lib/Hacl_Streaming_Blake2b_256_bindings.ml", line 35, characters 6-228
Called from file "lib_gen/Hacl_Streaming_Blake2b_256_gen.ml", line 5, characters 15-59
Called from file "src/cstubs/cstubs.ml", line 171, characters 17-33

you can reproduce this by running, with the latest F*, your branch of kremlin, and branch son_blake of HACL*:

OTHERFLAGS="--admit_smt_queries true" make -j compile-gcc-compatible

let me know if I can provide any other useful information to help debug this

[victor-dumitrescu]

Should be fixed now, the way I was identifying the relevant abstract structs wasn't quite right.