Improper generation of ctypes bindings for Lib.IntVector.Intrinsics.vec256

[sonmarcho]

When generating ctypes bindings with krml on the below file:

module KremlinVector

open FStar.HyperStack.ST
open LowStar.Buffer

#set-options "--z3rlimit 25 --ifuel 0 --fuel 0"

let t2 = UInt32.t & Lib.IntVector.Intrinsics.vec256
let f2 (x : t2) : t2 = x

We get the following .ml:

open Ctypes
module Bindings(F:Cstubs.FOREIGN) =
  struct
    open F
    let kremlinVector_f2 =
      foreign "KremlinVector_f2"
        (kremlinVector_t2 @-> (returning kremlinVector_t2))
  end

Note that kremlinVector_f2 references the undefined kremlinVector_t2, preventing the file from compiling

[msprotz]

Hey @victor-dumitrescu, would you be able to take a look at this? I think it's relatively simple to fix, when you encounter a struct type that contains forbidden types, just remember the name of the struct, then:

https://github.com/FStarLang/kremlin/blob/master/src/GenCtypes.ml#L85

when you see one of those struct types later on (the Qualified case), then you can also return false.

[victor-dumitrescu]

No problem, I'll submit a fix soon.

[victor-dumitrescu]

I think this should fix it but let me know if you think I'm missing any potential cases.

For the code above it should now still work but throw these warnings:

Warning 22: : Dropping declaration from KremlinVector bindings because it uses unsupported type Lib.IntVector.Intrinsics.vec256
Warning 22: : Dropping declaration from KremlinVector bindings because it uses unsupported type KremlinVector
.t2

and neither t2 not f2 should be bound.