#include <stdlib.h>
#include <stdint.h>
#include <assert.h>

typedef int8_t* fsm_id;
typedef uint64_t a_size;

typedef enum {
        FSM_STATE_ALLOCATED,
        FSM_STATE_FREED,
        FSM_STATE_ERROR,
        FSM_STATE_NONE
} fsm_state;

typedef enum {
        FSM_ALPHABET_FREE,
        FSM_ALPHABET_MALLOC,
} fsm_alphabet;

// finite state machine
typedef struct {
        fsm_id id;
        a_size size;
        fsm_state state;
} fsm;


// FSM list type
typedef struct fsm_list_node{
        fsm *fsm;
        struct fsm_list_node *next;
} fsm_list_node;

static fsm_list_node *fsm_list = NULL;

static void __INSTR_fsm_list_append(fsm_list_node *node) {
        fsm_list_node *cur = fsm_list;

        while((cur) && (cur->next)) {
          cur = cur->next;
        }

        if (cur == NULL) {
                cur = node;
                fsm_list = node;
        } else {
                cur->next = node;
        }
}

static fsm* __INSTR_fsm_create(fsm_id id, fsm_state state) {
        fsm *new_fsm = (fsm *) malloc(sizeof(fsm));
        new_fsm->id = id;
        new_fsm->state = state;

        fsm_list_node *node = (fsm_list_node *) malloc(sizeof(fsm_list_node));
        node->next = NULL;
        node->fsm = new_fsm;

        __INSTR_fsm_list_append(node);
        return new_fsm;
}

static fsm* __INSTR_fsm_list_search(fsm_id id) {
        fsm_list_node *cur = fsm_list;

        while(cur) {
                /* check wether 'id' is a pointer to
                 * some memory that we registred, that is if it points
                 * to some memory region in range [cur.id, cur.id + size] */
                if (cur->fsm->id == id) {
        //      if (cur->fsm->id <= id
        //           && id < cur->fsm->id + cur->fsm->size) {
                        return cur->fsm;
                }
          cur = cur->next;
        }

        return NULL;
}

// FSM manipulation

static fsm_state fsm_transition_table[4][2] = {{ FSM_STATE_FREED, FSM_STATE_ALLOCATED }, // allocated
                                        { FSM_STATE_ERROR, FSM_STATE_ALLOCATED }, // freed
                                        { FSM_STATE_ERROR, FSM_STATE_ERROR }, // error
                                        { FSM_STATE_NONE, FSM_STATE_NONE}};

static void __INSTR_fsm_change_state(fsm_id id, fsm_alphabet action) {

        // there is no FSM for NULL
        if (id == 0) {
                return;
        }

        fsm *m = __INSTR_fsm_list_search(id);
        if (m != NULL) {
                if(action == FSM_ALPHABET_FREE && m->id != id){
                        assert(0 && "free on non-allocated memory");
                        __VERIFIER_error();
                }
                m->state = fsm_transition_table[m->state][action];
        } else {
                if (action == FSM_ALPHABET_FREE) {
                        assert(0 && "free on non-allocated memory");
                        __VERIFIER_error();
                }
                m = __INSTR_fsm_create(id, FSM_STATE_ALLOCATED);
        }

        if (m != NULL && m->state == FSM_STATE_ERROR) {
                assert(0 && "double free");
                __VERIFIER_error();
        }
}
static fsm* __INSTR_remember(fsm_id id, a_size size, int num) {
        fsm *new_rec = (fsm *) malloc(sizeof(fsm));
        new_rec->id = id;
        new_rec->size = size * num;
        new_rec->state = FSM_STATE_NONE;

        fsm_list_node *node = (fsm_list_node *) malloc(sizeof(fsm_list_node));
        node->next = NULL;
        node->fsm = new_rec;

        __INSTR_fsm_list_append(node);

        return new_rec;
}

static void __INSTR_remember_malloc_size(fsm_id id, size_t size) {
        fsm *m = __INSTR_fsm_list_search(id);
        if (m != NULL) {
                m->size = size;
        }
}

static void __INSTR_check_range(fsm_id id, int range) {
        fsm *r = __INSTR_fsm_list_search(id);

        if (r != NULL) {
                /* (id - rec->id) is the offset into allocated memory
                 * it must be possitive, since id >= rec->id */
                if ((a_size)(id - r->id + range) > r->size) {
                        assert(0 && "memset/memcpy out of range");
                        __VERIFIER_error();
                }

                // this memory was already freed
                if(r->state == FSM_STATE_FREED) {
                        assert(0 && "memset/memcpy on freed memory");
                        __VERIFIER_error();
                }
        } else {
                /* we register all memory allocations, so if we
                 * haven't found the allocation, then this is
                 * invalid pointer */
                assert(0 && "memset/memcpy on invalid pointer");
                __VERIFIER_error();
        }
}

int main(void) {
        int i = 0;
        void *mem = __VERIFIER_nondet_pointer();
        __INSTR_fsm_change_state(mem, 1);
        __INSTR_remember_malloc_size(mem, 119);
        __INSTR_check_range(mem, 119);

        return 0;
}
                                                                                                                                                                                                                             175,1       Konec