Tracking of sort lifetimes is incomplete, leads to multiple frees

[smuenzel]

When running the tests with dune, sorts seem to be free'd multiple times.

To reliably reproduce, use this branch: https://github.com/bitwuzla/ocaml-bitwuzla/compare/master...smuenzel:test-sort-multiple-delete Here, we assert that each sort is only deleted once, but it seems like it is deleted multiple times.

The test that usually triggers this is (resulting in a segfault):

let%expect_test "mk_array_sort" =
  Sort.pp Format.std_formatter ar32_8_sort;
  [%expect {| (Array (_ BitVec 32) (_ BitVec 8)) |}]

I've added a Gc.full_major after each test, which is usually good about triggering Gc errors quickly, since it will eagerly delete "unused" values.

[smuenzel]

I now believe this is not actually a multiple free, rather, it is caused when an exception is raised in ocaml_bitwuzla_mk_fun_sort in the following test:

let%test "mk_fun_sort" =
  let result =
  (try
     ignore (mk_fun_sort [||] bool_sort);
     false
   with Invalid_argument _ -> true
  )
  in
  result

The allocation of a new sort that raises an exception seems to leave the heap in a bad state (maybe a partially-initialized value?).

[smuenzel]

Here's what happens: In the function ocaml_bitwuzla_mk_fun_sort, we use a custom new: https://github.com/bitwuzla/ocaml-bitwuzla/blob/f40b7c00bcc0ee2c9c17a6d6367073d4f3485ea4/cxx_stubs.cpp#L505 This allocates a block using caml_alloc_custom, with a finalizer specialized for Sort. Then, the constructor raises an exception, so it doesn't initialize the block with a valid value. So on the next GC, we run the finalizer on un-initialized memory.