<commit_before>#include <hre/config.h>

#include <dlfcn.h>
#include <limits.h>
#include <stdlib.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <unistd.h>

#include <dm/dm.h>
#include <hre/runtime.h>
#include <hre/stringindex.h>
#include <hre/unix.h>
#include <ltsmin-lib/ltsmin-standard.h>
#include <pins-lib/pins.h>
#include <pins-lib/prob-pins.h>
#include <prob-lib/prob_helpers.h>
#include <prob-lib/prob_client.h>
#include <util-lib/chunk_support.h>
#include <util-lib/util.h>

// is_init is a reserved state variable
static const char* IS_INIT = "is_init";

static int no_close = 0;

typedef struct prob_context {
    int num_vars;
    int op_type_no;
    prob_client_t prob_client;
    int* op_type;
    int* var_type;
} prob_context_t;

static void
prob_popt(poptContext con, enum poptCallbackReason reason, const struct poptOption *opt, const char *arg, void *data)
{
    (void) con; (void) opt; (void) arg; (void) data;

    switch (reason) {
    case POPT_CALLBACK_REASON_PRE:
        break;
    case POPT_CALLBACK_REASON_POST:
        GBregisterLoader("probz", ProBloadGreyboxModel);

        Warning(info, "ProB module initialized");
        return;
    case POPT_CALLBACK_REASON_OPTION:
        break;
    }

    Abort("unexpected call to prob_popt");
}

struct poptOption prob_options[] = {
    { NULL, 0, POPT_ARG_CALLBACK | POPT_CBFLAG_POST | POPT_CBFLAG_SKIPOPTION, (void*) &prob_popt, 0, NULL, NULL },
    { "no-close", 0, POPT_ARG_NONE, &no_close, 0, "do not close the ProB connection (so that it can be reused)", NULL },
    POPT_TABLEEND };

static ProBState
pins2prob_state(model_t model, int* pins)
{
    prob_context_t* ctx = (prob_context_t*) GBgetContext(model);

    ProBState prob;

    prob.size = ctx->num_vars;
    prob.chunks = RTmalloc(sizeof(ProBChunk) * prob.size);

    Debugf("pins2prob state (%d): ", ctx->num_vars);
    for (int i = 0; i < ctx->num_vars; i++) {
        chunk c = GBchunkGet(model, ctx->var_type[i], pins[i]);

        prob.chunks[i].data = c.data;
        prob.chunks[i].size = c.len;
        Debugf("(%u)", c.len);
#ifdef LTSMIN_DEBUG
        for (unsigned int j = 0; j < c.len; j++) Debugf("%x", c.data[j]);
#endif

        Debugf(",");
    }
    Debugf("\n");

    return prob;
}

static void
prob2pins_state(ProBState s, int *state, model_t model)
{
    prob_context_t* ctx = (prob_context_t*) GBgetContext(model);
    HREassert((int) s.size == ctx->num_vars, "expecting %d chunks, but got %zu", ctx->num_vars, s.size);

    Debugf("prob2pins state (%zu): ", s.size);
    for (size_t i = 0; i < s.size; i++) {
        chunk c;
        c.data = s.chunks[i].data;
        c.len = s.chunks[i].size;
        Debugf("(%u)", c.len);
#ifdef LTSMIN_DEBUG
        for (unsigned int j = 0; j < c.len; j++) Debugf("%x", c.data[j]);
#endif
        Debugf(",");
        int chunk_id = GBchunkPut(model, ctx->var_type[i], c);
        state[i] = chunk_id;
    }
    Debugf("\n");
}

static int
get_successors_long(model_t model, int group, int *src, TransitionCB cb, void *ctx)
{
    prob_context_t* prob_ctx = (prob_context_t*) GBgetContext(model);

    /* Don't give any successors for the init group if we have already initialized.
     * This prevents adding a self loop to the initial state. */
    if (group == 0 && src[prob_ctx->num_vars] == 1) return 0;

    // Don't give any successors for groups other than the init group if we have not initialized
    if (group > 0 && src[prob_ctx->num_vars] == 0) return 0;

    int operation_type = prob_ctx->op_type_no;

    chunk op_name = GBchunkGet(model, operation_type, prob_ctx->op_type[group]);

    ProBState prob = pins2prob_state(model, src);

    int nr_successors;
    ProBState *successors = prob_next_state(prob_ctx->prob_client, prob, op_name.data, &nr_successors);
    prob_destroy_state(&prob);

    int s[prob_ctx->num_vars + 1];
    s[prob_ctx->num_vars] = 1;
    for (int i = 0; i < nr_successors; i++) {

        int transition_labels[1] = { prob_ctx->op_type[group] };
        transition_info_t transition_info = { transition_labels, group, 0 };

        prob2pins_state(successors[i], s, model);
        prob_destroy_state(successors + i);
        cb(ctx, &transition_info, s, NULL);
    }

    RTfree(successors);

    return nr_successors;
}

void
prob_exit(model_t model)
{
    prob_context_t* ctx = (prob_context_t*) GBgetContext(model);

    if (!no_close) {
        Warning(info, "terminating ProB connection");
        prob_terminate(ctx->prob_client);
        Warning(info, "disconnecting from zocket %s", prob_get_zocket(ctx->prob_client));
        prob_disconnect(ctx->prob_client);
        prob_client_destroy(ctx->prob_client);
    }
}

void
ProBloadGreyboxModel(model_t model, const char* model_name)
{
    (void) model_name;

    Warning(info, "ProB init");

    char abs_filename[PATH_MAX];
    char* ret_filename = realpath(model_name, abs_filename);

    // check file exists
    struct stat st;
    if (stat(ret_filename, &st) != 0) Abort("Zocket does not exist: %s", model_name);

    prob_context_t* ctx = (prob_context_t*) RTmalloc(sizeof(prob_context_t));
    ctx->prob_client = prob_client_create();
    GBsetContext(model, ctx);

    const char* ipc = "ipc://";
    char zocket[strlen(ipc) + strlen(ret_filename) + 1];
    sprintf(zocket, "%s%s", ipc, ret_filename);

    Warning(info, "connecting to zocket %s", zocket);
    prob_connect(ctx->prob_client, zocket);

    ProBInitialResponse init = prob_init(ctx->prob_client);

    lts_type_t ltstype = lts_type_create();

    // add an "Operation" type for edge labels
    int is_new = 0;<commit_msg>prob: remove unnecessary void cast<commit_after>#include <hre/config.h>

#include <dlfcn.h>
#include <limits.h>
#include <stdlib.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <unistd.h>

#include <dm/dm.h>
#include <hre/runtime.h>
#include <hre/stringindex.h>
#include <hre/unix.h>
#include <ltsmin-lib/ltsmin-standard.h>
#include <pins-lib/pins.h>
#include <pins-lib/prob-pins.h>
#include <prob-lib/prob_helpers.h>
#include <prob-lib/prob_client.h>
#include <util-lib/chunk_support.h>
#include <util-lib/util.h>

// is_init is a reserved state variable
static const char* IS_INIT = "is_init";

static int no_close = 0;

typedef struct prob_context {
    int num_vars;
    int op_type_no;
    prob_client_t prob_client;
    int* op_type;
    int* var_type;
} prob_context_t;

static void
prob_popt(poptContext con, enum poptCallbackReason reason, const struct poptOption *opt, const char *arg, void *data)
{
    (void) con; (void) opt; (void) arg; (void) data;

    switch (reason) {
    case POPT_CALLBACK_REASON_PRE:
        break;
    case POPT_CALLBACK_REASON_POST:
        GBregisterLoader("probz", ProBloadGreyboxModel);

        Warning(info, "ProB module initialized");
        return;
    case POPT_CALLBACK_REASON_OPTION:
        break;
    }

    Abort("unexpected call to prob_popt");
}

struct poptOption prob_options[] = {
    { NULL, 0, POPT_ARG_CALLBACK | POPT_CBFLAG_POST | POPT_CBFLAG_SKIPOPTION, (void*) &prob_popt, 0, NULL, NULL },
    { "no-close", 0, POPT_ARG_NONE, &no_close, 0, "do not close the ProB connection (so that it can be reused)", NULL },
    POPT_TABLEEND };

static ProBState
pins2prob_state(model_t model, int* pins)
{
    prob_context_t* ctx = (prob_context_t*) GBgetContext(model);

    ProBState prob;

    prob.size = ctx->num_vars;
    prob.chunks = RTmalloc(sizeof(ProBChunk) * prob.size);

    Debugf("pins2prob state (%d): ", ctx->num_vars);
    for (int i = 0; i < ctx->num_vars; i++) {
        chunk c = GBchunkGet(model, ctx->var_type[i], pins[i]);

        prob.chunks[i].data = c.data;
        prob.chunks[i].size = c.len;
        Debugf("(%u)", c.len);
#ifdef LTSMIN_DEBUG
        for (unsigned int j = 0; j < c.len; j++) Debugf("%x", c.data[j]);
#endif

        Debugf(",");
    }
    Debugf("\n");

    return prob;
}

static void
prob2pins_state(ProBState s, int *state, model_t model)
{
    prob_context_t* ctx = (prob_context_t*) GBgetContext(model);
    HREassert((int) s.size == ctx->num_vars, "expecting %d chunks, but got %zu", ctx->num_vars, s.size);

    Debugf("prob2pins state (%zu): ", s.size);
    for (size_t i = 0; i < s.size; i++) {
        chunk c;
        c.data = s.chunks[i].data;
        c.len = s.chunks[i].size;
        Debugf("(%u)", c.len);
#ifdef LTSMIN_DEBUG
        for (unsigned int j = 0; j < c.len; j++) Debugf("%x", c.data[j]);
#endif
        Debugf(",");
        int chunk_id = GBchunkPut(model, ctx->var_type[i], c);
        state[i] = chunk_id;
    }
    Debugf("\n");
}

static int
get_successors_long(model_t model, int group, int *src, TransitionCB cb, void *ctx)
{
    prob_context_t* prob_ctx = (prob_context_t*) GBgetContext(model);

    /* Don't give any successors for the init group if we have already initialized.
     * This prevents adding a self loop to the initial state. */
    if (group == 0 && src[prob_ctx->num_vars] == 1) return 0;

    // Don't give any successors for groups other than the init group if we have not initialized
    if (group > 0 && src[prob_ctx->num_vars] == 0) return 0;

    int operation_type = prob_ctx->op_type_no;

    chunk op_name = GBchunkGet(model, operation_type, prob_ctx->op_type[group]);

    ProBState prob = pins2prob_state(model, src);

    int nr_successors;
    ProBState *successors = prob_next_state(prob_ctx->prob_client, prob, op_name.data, &nr_successors);
    prob_destroy_state(&prob);

    int s[prob_ctx->num_vars + 1];
    s[prob_ctx->num_vars] = 1;
    for (int i = 0; i < nr_successors; i++) {

        int transition_labels[1] = { prob_ctx->op_type[group] };
        transition_info_t transition_info = { transition_labels, group, 0 };

        prob2pins_state(successors[i], s, model);
        prob_destroy_state(successors + i);
        cb(ctx, &transition_info, s, NULL);
    }

    RTfree(successors);

    return nr_successors;
}

void
prob_exit(model_t model)
{
    prob_context_t* ctx = (prob_context_t*) GBgetContext(model);

    if (!no_close) {
        Warning(info, "terminating ProB connection");
        prob_terminate(ctx->prob_client);
        Warning(info, "disconnecting from zocket %s", prob_get_zocket(ctx->prob_client));
        prob_disconnect(ctx->prob_client);
        prob_client_destroy(ctx->prob_client);
    }
}

void
ProBloadGreyboxModel(model_t model, const char* model_name)
{
    Warning(info, "ProB init");

    char abs_filename[PATH_MAX];
    char* ret_filename = realpath(model_name, abs_filename);

    // check file exists
    struct stat st;
    if (stat(ret_filename, &st) != 0) Abort("Zocket does not exist: %s", model_name);

    prob_context_t* ctx = (prob_context_t*) RTmalloc(sizeof(prob_context_t));
    ctx->prob_client = prob_client_create();
    GBsetContext(model, ctx);

    const char* ipc = "ipc://";
    char zocket[strlen(ipc) + strlen(ret_filename) + 1];
    sprintf(zocket, "%s%s", ipc, ret_filename);

    Warning(info, "connecting to zocket %s", zocket);
    prob_connect(ctx->prob_client, zocket);

    ProBInitialResponse init = prob_init(ctx->prob_client);

    lts_type_t ltstype = lts_type_create();

    // add an "Operation" type for edge labels
    int is_new = 0;
{'fraction_non_alphanumeric': 0.1385590572270333, 'fraction_numerical': 0.005178109097402018, 'mean_word_length': 3.516935483870968, 'pattern_counts': {'":': 0, '<': 49, '<?xml version=': 0, '>': 85, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5362332', 'n_tokens_mistral': 4142, 'n_tokens_neox': 4017, 'n_words': 967}