/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
   Licensed under the Apache 2.0 License. */

#ifndef __KREMLIN_TARGET_H
#define __KREMLIN_TARGET_H

#include <stdlib.h>
#include <stdio.h>
#include <stdbool.h>
#include <inttypes.h>
#include <limits.h>

#include "kremlin/internal/callconv.h"

/******************************************************************************/
/* Macros that KreMLin will generate.                                         */
/******************************************************************************/

/* For "bare" targets that do not have a C stdlib, the user might want to use
 * [-add-early-include '"mydefinitions.h"'] and override these. */
#ifndef KRML_HOST_PRINTF
#define KRML_HOST_PRINTF printf
#endif

#if (                                                              \
    (defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) && \
    (!(defined KRML_HOST_EPRINTF)))
#define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
#elif !(defined KRML_HOST_EPRINTF) && defined(_MSC_VER)
#define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
#endif

#ifndef KRML_HOST_EXIT
#define KRML_HOST_EXIT exit
#endif

#ifndef KRML_HOST_MALLOC
#define KRML_HOST_MALLOC malloc
#endif

#ifndef KRML_HOST_CALLOC
#define KRML_HOST_CALLOC calloc
#endif

#ifndef KRML_HOST_FREE
#define KRML_HOST_FREE free
#endif

#ifndef KRML_HOST_TIME

#include <time.h>

/* Prims_nat not yet in scope */
inline static int32_t
krml_time()
{
    return (int32_t)time(NULL);
}

#define KRML_HOST_TIME krml_time
#endif

/* In statement position, exiting is easy. */
#define KRML_EXIT                                                                  \
    do {                                                                           \
        KRML_HOST_PRINTF("Unimplemented function at %s:%d\n", __FILE__, __LINE__); \
        KRML_HOST_EXIT(254);                                                       \
    } while (0)

/* In expression position, use the comma-operator and a malloc to return an
 * expression of the right size. KreMLin passes t as the parameter to the macro.
 */
#define KRML_EABORT(t, msg)                                                     \
    (KRML_HOST_PRINTF("KreMLin abort at %s:%d\n%s\n", __FILE__, __LINE__, msg), \
     KRML_HOST_EXIT(255), *((t *)KRML_HOST_MALLOC(sizeof(t))))

/* In FStar.Buffer.fst, the size of arrays is uint32_t, but it's a number of
 * *elements*. Do an ugly, run-time check (some of which KreMLin can eliminate).
 */

#ifdef __GNUC__
#define _KRML_CHECK_SIZE_PRAGMA \
    _Pragma("GCC diagnostic ignored \"-Wtype-limits\"")
#else
#define _KRML_CHECK_SIZE_PRAGMA
#endif

#define KRML_CHECK_SIZE(size_elt, sz)                                             \
    do {                                                                          \
        _KRML_CHECK_SIZE_PRAGMA                                                   \
        if (((size_t)(sz)) > ((size_t)(SIZE_MAX / (size_elt)))) {                 \
            KRML_HOST_PRINTF(                                                     \
                "Maximum allocatable size exceeded, aborting before overflow at " \
                "%s:%d\n",                                                        \
                __FILE__, __LINE__);                                              \
            KRML_HOST_EXIT(253);                                                  \
        }                                                                         \
    } while (0)

#if defined(_MSC_VER) && _MSC_VER < 1900
#define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) _snprintf_s(buf, sz, _TRUNCATE, fmt, arg)
#else
#define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) snprintf(buf, sz, fmt, arg)
#endif

#if defined(__GNUC__) && __GNUC__ >= 4 && __GNUC_MINOR__ > 4
#define KRML_DEPRECATED(x) __attribute__((deprecated(x)))
#elif defined(__GNUC__)
/* deprecated attribute is not defined in GCC < 4.5. */
#define KRML_DEPRECATED(x)
#elif defined(_MSC_VER)
#define KRML_DEPRECATED(x) __declspec(deprecated(x))
#endif

#endif