How do I properly interact with CertiCoq's garbage collector when calling library functions from C++?

Question

I am trying to build a C++ library backed by Coq sets, but I am continuously running into segfaults which I believe are related to garbage collection or memory leaks. I am using Coq 8.17.1 with a fresh build of CertiCoq (https://github.com/CertiCoq/certicoq) as of May 14 2024. In this setting, I am using CertiCoq to compile a Coq structure that consists of the usual set operations---in this case, empty, membership, add, and cardinal. (Full MWE at the bottom of the page).

Record MSet_struct A S :=
    MSet_Struct {
        mset_empty : S;
        mset_mem : A -> S -> bool;
        mset_add : A -> S -> S;
        mset_remove : A -> S -> S;
        mset_cardinal : S -> int;
    }.
…
Module RBT := Coq.MSets.MSetRBT.Make int_as_OT.

Definition RBT_MSet_struct : MSet_struct int RBT.t :=
    {|
        mset_empty := RBT.empty;
        mset_mem := RBT.mem;
        mset_add := RBT.add;
        mset_remove := RBT.remove;
        mset_cardinal := fun x => nat_to_int (RBT.cardinal x);
    |}.

CertiCoq Generate Glue -file "glue" [bool].
CertiCoq Compile -file "RBT" RBT_MSet_struct
    Extract Constants []
    Include ["stdbool.h" as library].

Then, in a .cpp file I define a class called certicoq::set, which is a set of integers. The class has an underlying value which stores the set and implements the usual methods.

class set {
    private:
        // the value underlying the set
        value t_value_;

    public:
        value getValue() const { return t_value_; };
        void setValue(value v) { t_value_ = v; };

        // Constructors and destructors
        set(value);
        set(); // empty set
        ~set() = default;

        void add(int x);
        void remove(int x); // if x is not already in the set, do nothing

        bool isMember(int x) const;
        int size() const;
};

The implementation of each library function (e.g. add, cardinal, mem) is defined via one or more calls to the Coq runtime. For example:

void set::add(int x) {
    value vs = getValue();
    value vx = int_to_value(x);

    value f = get_args(body(tinfo_))[set_add_tag];
    value f0 = LIVEPOINTERS3(tinfo_, call(tinfo_, f, vx), f, vx, vs);
    value v  = LIVEPOINTERS2(tinfo_, call(tinfo_, f0, vs), f0, vs);
    setValue(v);
}

Here, LIVEPOINTERS are macros meant to tell the Coq garbage collector the live pointers a la [1] and [2]. Note that all set values are constructed using API calls, meaning that they all should live on the Coq heap. The only values built outside the Coq heap are primitives such as booleans, primitive integers, and 0-ary constructors.

We can use this library as shown in this main function in CoqSet.cpp:

int main() {
    certicoq::initialize_global_thread_info();
    certicoq::set X;

    for (int i=0; i<1000; i++) {
        std::cout << "Adding " << i << "; ";
        X.add(i);
        std::cout << "new set has size: " << X.size() << "\n";
    }
}

However, after adding only 133 integers, the size of the set resets to zero, and after another 133 integers, I get a segmentation fault. I can get this slightly better by changing how LIVEPOINTERS are used or explicitly making calls to the garbage collector, but even then it is still quite limited. I suspect I am not interacting with the garbage collector properly, but I am not sure what the solution should look like.

A MWE example is shown below.

MSetImplementation.v

Require Import MSets.MSetRBT.

From CertiCoq.Plugin Require Import CertiCoq.

Require Import Coq.Structures.Orders.
From Coq.Numbers.Cyclic.Int63 Require Import PrimInt63.
Require Import CertiCoq.Plugin.PrimInt63.


(* API for MSets, which can be instantiated with any MSet implementation. *)
Record MSet_struct A S :=
    MSet_Struct {
        mset_empty : S;
        mset_mem : A -> S -> bool;
        mset_add : A -> S -> S;
        mset_cardinal : S -> int;
    }.

(* Skeleton definition of primitive ints as an ordered type *)
Module int_as_OT <: UsualOrderedType.
    Definition t := int.
    Definition eq := @eq int.
    
    Definition eq_refl := @eq_refl t.
    Definition eq_sym := @eq_sym t.
    Definition eq_trans := @eq_trans t.
    Definition eq_equiv : Equivalence eq.
    Proof.
        constructor. exact eq_refl. exact eq_sym. exact eq_trans.
    Defined.

    Definition lt := fun z1 z2 => compare z1 z2 = Lt.

    Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
    Admitted.

    Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
    Admitted.

    Lemma int_eqb_eq : forall (x y : int),
        eqb x y = true <-> x = y.
    Admitted.

    Lemma leb_implies_gtb : forall (x y : int),
        ltb x y = false ->
        eqb x y = false ->
        ltb y x = true.
    Admitted.

    Lemma lt_strorder : StrictOrder lt.
    Admitted. 
    Lemma lt_compat : Proper (Logic.eq ==> Logic.eq ==> iff) lt.
    Admitted.

    Definition compare : int -> int -> comparison := compare.

    Lemma compare_spec : forall x y : t,
            CompareSpec (x = y) (lt x y) (lt y x) (compare x y).
    Admitted.

    Lemma compare_eq : forall x y, compare x y = Eq -> x = y.
    Admitted.
    Lemma compare_lt : forall x y, compare x y = Lt -> lt x y.
    Admitted.
    Lemma compare_gt : forall x y, compare x y = Gt <-> compare y x = Lt.
    Admitted.

    Definition eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
    Proof.
        intros x y.
        destruct (compare x y) eqn:Hxy.
        * left. apply compare_eq. exact Hxy.
        * right. apply lt_not_eq. exact Hxy.
        * right. apply compare_gt in Hxy. apply lt_not_eq in Hxy.
          intros Heq. apply Hxy. symmetry. exact Heq.
    Defined.
    
End int_as_OT.

Fixpoint nat_to_int (x : nat) : int :=
    match x with
    | 0 => 0
    | S x' => add 1 (nat_to_int x')
    end.

(* Instantiate red black trees (RBT) MSets with integers. *)
Module RBT := Coq.MSets.MSetRBT.Make int_as_OT.

Definition RBT_MSet_struct : MSet_struct int RBT.t :=
    {|
        mset_empty := RBT.empty;
        mset_mem := RBT.mem;
        mset_add := RBT.add;
        mset_cardinal := fun x => nat_to_int (RBT.cardinal x);
    |}.

CertiCoq Generate Glue -file "glue" [bool].
CertiCoq Compile -file "RBT" RBT_MSet_struct
    Extract Constants []
    Include ["stdbool.h" as library].

CoqSet.cpp

#include <iostream>

extern "C" {
    // Files found in path-to-certicoq/plugin/runtime/
    #include "values.h"
    #include "gc_stack.h"
    #include "prim_int63.h"

    extern struct thread_info *make_tinfo();
    extern value *get_args(value);
    extern value call(struct thread_info *, value, value);
    value body(struct thread_info *);

    extern value make_Coq_Init_Datatypes_bool_true(void);
    extern value make_Coq_Init_Datatypes_bool_false(void);
    extern unsigned int get_Coq_Init_Datatypes_bool_tag(value);
    extern void print_Coq_Init_Datatypes_bool(value);
}

namespace certicoq {

// Global thread info
static struct thread_info* tinfo_ = NULL;
void initialize_global_thread_info() {
    if (tinfo_ == NULL) {
        tinfo_ = make_tinfo();
    }
}

// Set of integers data structure
class set {
    private:
        // the value underlying the set
        value t_value_;

    public:
        value getValue() const { return t_value_; };
        void setValue(value v) { t_value_ = v; };

        // Constructors and destructors
        set(); // empty set
        ~set() = default;

        void add(int x);
        bool isMember(int x) const;
        int size() const;
};

///////////////////
// Instantiation //
///////////////////

// This enum copies the order of constructors of MSet_struct from
// MSetImplementation.v
enum SetOpsTag {
        set_empty_tag,
        set_mem_tag,
        set_add_tag,
        set_cardinal_tag
};

//////////////////////
// Helper functions //
//////////////////////


bool value_to_bool(const value b) {
    return (get_Coq_Init_Datatypes_bool_tag(b) == 0);
}
value bool_to_value(const bool b) {
    if (b) {
        return make_Coq_Init_Datatypes_bool_true();
    } else {
        return make_Coq_Init_Datatypes_bool_false();
    }
}
int value_to_int(const value v) {
    return Int_val((long) v);
}
value int_to_value(const int x) {
    return (value)Val_int(x);
}

// These macros are taken from VeriFFI examples,
// e.g. https://github.com/CertiCoq/VeriFFI/blob/main/examples/array/prims.c
// See https://github.com/CertiCoq/certicoq/wiki/When-C-code-allocates-on-the-Coq-heap
// for more info
#define LIVEPOINTERS1(tinfo, exp, a) ({ \
  value __ROOT__[1] = { a }; \
  struct stack_frame __FRAME__ = { __ROOT__ + 1, __ROOT__, tinfo->fp }; \
  tinfo->fp = &__FRAME__; value __TEMP__ = exp; \
  a = __ROOT__[0]; \
  tinfo->fp = __FRAME__.prev; __TEMP__; })
#define LIVEPOINTERS1_(tinfo, exp, a) ({ \
  value __ROOT__[1] = { a }; \
  struct stack_frame __FRAME__ = { __ROOT__ + 1, __ROOT__, tinfo->fp }; \
  tinfo->fp = &__FRAME__; \
  a = __ROOT__[0]; \
  tinfo->fp = __FRAME__.prev; })
#define LIVEPOINTERS2(tinfo, exp, a, b) ({ \
  value __ROOT__[2] = { a, b }; \
  struct stack_frame __FRAME__ = { __ROOT__ + 2, __ROOT__, tinfo->fp }; \
  tinfo->fp = &__FRAME__; value __TEMP__ = exp; \
  a = __ROOT__[0]; b = __ROOT__[1]; \
  tinfo->fp = __FRAME__.prev; __TEMP__; })
#define LIVEPOINTERS2_(tinfo, exp, a, b) ({ \
  value __ROOT__[2] = { a, b }; \
  struct stack_frame __FRAME__ = { __ROOT__ + 2, __ROOT__, tinfo->fp }; \
  tinfo->fp = &__FRAME__; exp; \
  a = __ROOT__[0]; b = __ROOT__[1]; \
  tinfo->fp = __FRAME__.prev; })
#define LIVEPOINTERS3(tinfo, exp, a, b, c) ({ \
  value __ROOT__[3] = { a, b, c }; \
  struct stack_frame __FRAME__ = { __ROOT__ + 3, __ROOT__, tinfo->fp }; \
  tinfo->fp = &__FRAME__; value __TEMP__ = exp; \
  a = __ROOT__[0]; b = __ROOT__[1]; c = __ROOT__[2]; \
  tinfo->fp = __FRAME__.prev; __TEMP__; })

//////////////////
// Constructors //
//////////////////

// Empty set
set::set() {
    value v = get_args(body(tinfo_))[set_empty_tag];
    setValue(v);
}

/////////////////////
// set Operations //
/////////////////////

void set::add(int x) {
    value vs = getValue();
    value vx = int_to_value(x);

    value f = get_args(body(tinfo_))[set_add_tag];
    value f0 = LIVEPOINTERS3(tinfo_, call(tinfo_, f, vx), f, vx, vs);
    value v  = LIVEPOINTERS2(tinfo_, call(tinfo_, f0, vs), f0, vs);
    setValue(v);
}

bool set::isMember(int x) const {
    value vX = getValue();
    value vx = int_to_value(x);

    value f  = get_args(body(tinfo_))[set_mem_tag];
    value f0 = LIVEPOINTERS3(tinfo_, call(tinfo_, f, vx),  f, vx, vX);
    value v  = LIVEPOINTERS2(tinfo_, call(tinfo_, f0, vX), f0, vX);

    return value_to_bool(v);
}

int set::size() const {
    value vX = getValue();

    value f = get_args(body(tinfo_))[set_cardinal_tag];
    value v = LIVEPOINTERS2(tinfo_, call(tinfo_, f, vX), f, vX);

    return value_to_int(v);
}

}

int main() {
    certicoq::initialize_global_thread_info();
    certicoq::set X;

    for (int i=0; i<1000; i++) {
        std::cout << "Adding " << i << "; ";
        X.add(i);
        std::cout << "new set has size: " << X.size() << "\n";
    }
}

Makefile

PATH_TO_CERTICOQ="../../certicoq"

all:
    coqc MSetImplementation.v
    make -C ../../certicoq/plugin/runtime all
    clang -o RBT.o -Wno-everything -O2 -fomit-frame-pointer -I $(PATH_TO_CERTICOQ)/plugin/runtime -c RBT.c
clang -o glue.o -Wno-everything -O2 -fomit-frame-pointer -I  $(PATH_TO_CERTICOQ)/plugin/runtime -c glue.c
    clang++ -o CoqSet.o -O2 -fomit-frame-pointer -I  $(PATH_TO_CERTICOQ)/plugin/runtime -c CoqSet.cpp
clang++ -o CoqSet  $(PATH_TO_CERTICOQ)/plugin/runtime/gc_stack.o  $(PATH_TO_CERTICOQ)/plugin/runtime/prim_int63.o \
                RBT.o glue.o CoqSet.o -lm

[1] https://github.com/CertiCoq/VeriFFI/blob/main/examples/array/prims.c

[2] https://github.com/CertiCoq/certicoq/wiki/When-C-code-allocates-on-the-Coq-heap

============================ Edit:

Taking Joomy's advice, I motified the member functions as follows:

void set::add(int x) {
    BEGINFRAME(tinfo_, 4)
    value vs = getValue();
    value vx = int_to_value(x);
    nalloc=10000; GC_SAVE2(tinfo_, vs, vx)

    value f = get_args(body(tinfo_))[set_add_tag];
    value f0 = LIVEPOINTERS3(tinfo_, call(tinfo_, f, vx), f, vx, vs);
    value v  = LIVEPOINTERS2(tinfo_, call(tinfo_, f0, vs), f0, vs);
    setValue(v);
    ENDFRAME
}

where

#define GC_SAVE2(tinfo, save0, save1) \
    if (!(_LIMIT=tinfo->limit, _ALLOC=tinfo->alloc, nalloc <= _LIMIT-_ALLOC)) { \
    tinfo->nalloc = nalloc;  \
    LIVEPOINTERS2(tinfo,(garbage_collect(tinfo),(value)NULL),save0,save1);  \
  }

It is not clear to me how the value of nalloc should be calculated, and while high constant values as shown here improve performance (allow me to build a larger set), it does not work forever.

I think the CertiCoq wiki (and the array example in the VeriFFI repo) might be out of date, which we should fix. You can find the current version of the C macros to deal with the GC here: github.com/CertiCoq/VeriFFI/blob/… — Joomy Korkut, Commented May 16 at 1:16
Thanks for that pointer; I had forgotten that I needed to use BEGINFRAME and ENDFRAME. I also added in the GC_SAVE macros to explicitly run garbage collection: However, because I am not allocating data directly, I don't know how much to allocate. E.g. in add, if I have nalloc=100; GC_SAVE2(tinfo_, vs, vx) there is no improvement, but if I have nalloc=10000; GC_SAVE2(tinfo_, vs, vx), then I am able to run the main function without errors. — Jennifer Paykin, Commented May 16 at 21:42

Mario Frank · Accepted Answer · 2024-05-16 12:57:06Z

1

normally, the GC should not lead to a segmentation fault. In my experience, those rather arise from deep recursion when using non-tail recursive functions.

I looked into your code examples and stumbled over that one:

Fixpoint nat_to_int (x : nat) : int :=
match x with
| 0 => 0
| S x' => add 1 (nat_to_int x')
end.

Although I am not completely sure I suspect those lines could be a reason. For a fast check (if you use Linux or Mac), you can try to increase the stack space using ulimit.

answered May 16 at 12:57

Mario Frank

112 bronze badges

$\begingroup$ Thank you, I think your guess is right that the use of unary natural numbers is contributing to the segfault. I will see if there is a more efficient representation of size of the sets. It doesn't seem to be the only issue though; I still need GC_SAVE macros as Joomy suggested . $\endgroup$
– Jennifer Paykin
Commented May 16 at 22:40
$\begingroup$ You're welcome. I had the same problem when compiling for Kernel space where the stack size cannot be increased. You can use the type N instead which reduces the probability of stack overflows. And the changes on proofs are rather moderate in my experience. I also VeriFFI which works really good. However, you can also try to make the functions tail recursive. $\endgroup$
– Mario Frank
Commented May 17 at 7:32
$\begingroup$ Especially for nat_to_int: If I get the semantics right, this is a transformation from nat to uint63. If this is right, then you can also use uint63_from_nat from VeriFFI. $\endgroup$
– Mario Frank
Commented May 17 at 7:39
$\begingroup$ Unfortunately that did not fix the problem, though I'm sure it's a good idea either way. Because I am just using a standard library implementation of sets here, I'm not confident that every underlying method is tail recursive, so even though I tried to write a version of cardinal that returns int/N, that didn't help. Will keep this in mind though. $\endgroup$
– Jennifer Paykin
Commented May 17 at 18:44
$\begingroup$ Oh, and increasing the stack space using ulimit didn't make a difference. $\endgroup$
– Jennifer Paykin
Commented May 17 at 18:45

Add a comment |

Jennifer Paykin · Accepted Answer · 2024-05-20 16:58:49Z

Thanks all for the help! After getting some offline help from Andrew Appel, I wanted to follow up with the solution in case it's useful to anyone else.

The problem was in the use of LIVEPOINTERS. Consider the add function. First of all, I needed to add BEGINFRAME and ENDFRAME surrounding each function. Second, we realized that it is preferable to call body(tinfo_) only once, in which case the pointer it is stored in should be preserved by LIVEPOINTERS.

Third, I needed to think about which values needed to be preserved AFTER each function call. For example, I had previously had:

    value f0 = LIVEPOINTERS3(tinfo_, call(tinfo_, f, vx), f, vx, vs);
    value v  = LIVEPOINTERS2(tinfo_, call(tinfo_, f0, vs), f0, vs);

where f and vx was being preserved by LIVEPOINTERS in the first line. These pointers were actually never used after this line, so they didn't need to be preserved by the garbage collector. However, vs, which was used in the following line, DID need to be preserved. Therefore, the correct implemnentation of add would be:

void set::add(int x) {
    BEGINFRAME(tinfo_, 3)

    value vs = getValue();
    value vx = int_to_value(x);

    value f  = get_args(BODY__)[set_add_tag];
    value f0 = LIVEPOINTERS2(tinfo_, call(tinfo_, f, vx), BODY__, vs);
    value v  = LIVEPOINTERS1(tinfo_, call(tinfo_, f0, vs), BODY__);
    setValue(v);
    ENDFRAME
}

The refined CoqSet.cpp:

#include <iostream>
#include <set>

extern "C" {
    // Files found in path-to-certicoq/plugin/runtime/
    #include "values.h"
    #include "gc_stack.h"
    #include "prim_int63.h"

    extern struct thread_info *make_tinfo();
    extern value *get_args(value);
    extern value call(struct thread_info *, value, value);
    value body(struct thread_info *);

    extern value make_Coq_Init_Datatypes_bool_true(void);
    extern value make_Coq_Init_Datatypes_bool_false(void);
    extern unsigned int get_Coq_Init_Datatypes_bool_tag(value);
    extern void print_Coq_Init_Datatypes_bool(value);
    extern unsigned int get_Coq_Init_Datatypes_nat_tag(value);
}

namespace certicoq {

// Global thread info
static struct thread_info* tinfo_ = NULL;
value BODY__;

void initialize_global_thread_info() {
    if (tinfo_ == NULL) {
        tinfo_ = make_tinfo();
        BODY__ = body(tinfo_);
    }
}

// Set of integers data structure
class set {
    private:
        // the value underlying the set
        value t_value_;

    public:
        value getValue() const { return t_value_; };
        void setValue(value v) {
            t_value_ = v;
        };

        // Constructors and destructors
        set(); // empty set
        ~set() = default;

        void add(int x);
        bool isMember(int x) const;
        int size();
};

///////////////////
// Instantiation //
///////////////////

// This enum copies the order of constructors of MSet_struct from
// MSetImplementation.v
enum SetOpsTag {
        set_empty_tag,
        set_mem_tag,
        set_add_tag,
        set_cardinal_tag
};
enum natTag {
        nat_O_tag,
        nat_S_tag
};

//////////////////////
// Helper functions //
//////////////////////


bool value_to_bool(const value b) {
    return (get_Coq_Init_Datatypes_bool_tag(b) == 0);
}
value bool_to_value(const bool b) {
    if (b) {
        return make_Coq_Init_Datatypes_bool_true();
    } else {
        return make_Coq_Init_Datatypes_bool_false();
    }
}
int value_to_int(const value v) {
    return Int_val((long) v);
}
value int_to_value(const int x) {
    return (value)Val_int(x);
}
value uint63_from_nat(value n) {
  value temp = n;
  uint64_t i = 0;

  while (get_Coq_Init_Datatypes_nat_tag(temp) == nat_S_tag) {
    i++;
    temp = get_args(temp)[0];
  }
  return (value) ((i << 1) + 1);
}


// These macros are taken from VeriFFI examples,
// e.g. https://github.com/CertiCoq/VeriFFI/blob/main/examples/array/prims.c
// e.g. https://github.com/CertiCoq/VeriFFI/blob/d33c677e3af8a62eaa14e262a1bdd1908bf3bc3d/examples/uint63nat/prims.c
// See https://github.com/CertiCoq/certicoq/wiki/When-C-code-allocates-on-the-Coq-heap
// for more info
#define BEGINFRAME(tinfo,n) {{{{{ \
   value *_ALLOC, *_LIMIT; \
   value __ROOT__[n];   \
   struct stack_frame __FRAME__ = { NULL/*bogus*/, __ROOT__, tinfo->fp }; \
   struct stack_frame *__PREV__; \
   size_t nalloc; \
   value __RTEMP__;

#define ENDFRAME }}}}}

#define LIVEPOINTERS0(tinfo, exp) (exp)

#define LIVEPOINTERS1(tinfo, exp, a0) \
   (tinfo->fp= &__FRAME__, __FRAME__.next=__ROOT__+1, \
   __ROOT__[0]=(a0), __RTEMP__=(exp), (a0)=__ROOT__[0], \
   __PREV__=__FRAME__.prev, tinfo->fp=__PREV__, __RTEMP__)

#define LIVEPOINTERS2(tinfo, exp, a0, a1)   \
  (tinfo->fp= &__FRAME__, __FRAME__.next=__ROOT__+2, \
  __ROOT__[0]=(a0), __ROOT__[1]=(a1),       \
  __RTEMP__=(exp),                              \
  (a0)=__ROOT__[0], (a1)=__ROOT__[1],             \
   __PREV__=__FRAME__.prev, tinfo->fp=__PREV__, __RTEMP__)

#define LIVEPOINTERS3(tinfo, exp, a0, a1, a2)   \
  (tinfo->fp= &__FRAME__, __FRAME__.next=__ROOT__+3,                       \
  __ROOT__[0]=(a0), __ROOT__[1]=(a1), __ROOT__[2]=(a2),  \
  __RTEMP__=(exp),                                       \
  (a0)=__ROOT__[0], (a1)=__ROOT__[1], (a2)=__ROOT__[2],    \
   __PREV__=__FRAME__.prev, tinfo->fp=__PREV__, __RTEMP__)

#define LIVEPOINTERS4(tinfo, exp, a0, a1, a2, a3)   \
  (tinfo->fp= &__FRAME__,  __FRAME__.next=__ROOT__+4,  \
  __ROOT__[0]=(a0), __ROOT__[1]=(a1), __ROOT__[2]=(a2), __ROOT__[3]=(a3),  \
  __RTEMP__=(exp),                                       \
  (a0)=__ROOT__[0], (a1)=__ROOT__[1], (a2)=__ROOT__[2], (a3)=__ROOT__[3],    \
   __PREV__=__FRAME__.prev, tinfo->fp=__PREV__, __RTEMP__)

#define GC_SAVE1(tinfo, save0) \
    if (!(_LIMIT=tinfo->limit, _ALLOC=tinfo->alloc, nalloc <= _LIMIT-_ALLOC)) { \
    tinfo->nalloc = nalloc;  \
    LIVEPOINTERS1(tinfo,(garbage_collect(tinfo),(value)NULL),save0);    \
  }

#define GC_SAVE2(tinfo, save0, save1) \
    if (!(_LIMIT=tinfo->limit, _ALLOC=tinfo->alloc, nalloc <= _LIMIT-_ALLOC)) { \
    tinfo->nalloc = nalloc;  \
    LIVEPOINTERS2(tinfo,(garbage_collect(tinfo),(value)NULL),save0,save1);  \
  }
#define GC_SAVE3(tinfo, save0, save1, save2) \
    if (!(_LIMIT=tinfo->limit, _ALLOC=tinfo->alloc, nalloc <= _LIMIT-_ALLOC)) { \
    tinfo->nalloc = nalloc;  \
    LIVEPOINTERS2(tinfo,(garbage_collect(tinfo),(value)NULL),save0,save1,save2);  \
  }


//////////////////
// Constructors //
//////////////////

// Empty set
set::set() {
    value v = get_args(BODY__)[set_empty_tag];
    setValue(v);
}

/////////////////////
// set Operations //
/////////////////////


void set::add(int x) {
    BEGINFRAME(tinfo_, 3)

    value vs = getValue();
    value vx = int_to_value(x);

    value f  = get_args(BODY__)[set_add_tag];
    value f0 = LIVEPOINTERS2(tinfo_, call(tinfo_, f, vx), BODY__, vs);
    value v  = LIVEPOINTERS1(tinfo_, call(tinfo_, f0, vs), BODY__);
    setValue(v);
    ENDFRAME
}

bool set::isMember(int x) const {
    bool result = false;
    BEGINFRAME(tinfo_, 3)

    value vs = getValue();
    value vx = int_to_value(x);


    value f  = get_args(BODY__)[set_mem_tag];
    value f0 = LIVEPOINTERS2(tinfo_, call(tinfo_, f, vx), BODY__, vs);
    value v  = LIVEPOINTERS2(tinfo_, call(tinfo_, f0, vs), BODY__, vs);
    result = value_to_bool(v);

    return result;
    ENDFRAME
}

int set::size() {
    BEGINFRAME(tinfo_, 3);
    value vS = getValue();
    value f = get_args(BODY__)[set_cardinal_tag];

    value vnat = LIVEPOINTERS2(tinfo_, call(tinfo_, f, vS), BODY__, vS);
    setValue(vS);
    return value_to_int(uint63_from_nat(vnat));
    ENDFRAME
}

}

int main() {

    certicoq::initialize_global_thread_info();

    certicoq::set X;

    for (int i=0; i<10000; i++) {
        std::cout << "Adding " << i << "\n";
        X.add(i);
        std::cout << "set has size: " << X.size() << "\n";
    }
    
    for (int i=-100; i<100; i++) {
        std::cout << "Checking membership of " << i << ": " << X.isMember(i) << "\n";
    }
}

Further improvements are possible of course, but this is the solution that solves the segfault bug.

Stack Exchange Network

How do I properly interact with CertiCoq's garbage collector when calling library functions from C++?

2 Answers 2

Your Answer

Not the answer you're looking for? Browse other questions tagged
coq
program-extraction
ffi
or ask your own question.

Hot Network Questions

How do I properly interact with CertiCoq's garbage collector when calling library functions from C++?

2 Answers 2

Your Answer

Sign up or log in

Post as a guest

Not the answer you're looking for? Browse other questions tagged coqprogram-extractionffi or ask your own question.

Related

Hot Network Questions

Not the answer you're looking for? Browse other questions tagged
coq
program-extraction
ffi
or ask your own question.