tor-browser

The Tor Browser
git clone https://git.dasho.dev/tor-browser.git
Log | Files | Refs | README | LICENSE

fstar_int.h (2499B)

      1 #ifndef KRML_HEADER_FSTAR_INT_H
      2 #define KRML_HEADER_FSTAR_INT_H
      3 
      4 #include "internal/types.h"
      5 
      6 /*
      7 * Arithmetic Shift Right operator
      8 *
      9 * In all C standards, a >> b is implementation-defined when a has a signed
     10 * type and a negative value. See e.g. 6.5.7 in
     11 * http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2310.pdf
     12 *
     13 * GCC, MSVC, and Clang implement a >> b as an arithmetic shift.
     14 *
     15 * GCC: https://gcc.gnu.org/onlinedocs/gcc-9.1.0/gcc/Integers-implementation.html#Integers-implementation
     16 * MSVC: https://docs.microsoft.com/en-us/cpp/cpp/left-shift-and-right-shift-operators-input-and-output?view=vs-2019#right-shifts
     17 * Clang: tested that Clang 7, 8 and 9 compile this to an arithmetic shift
     18 *
     19 * We implement arithmetic shift right simply as >> in these compilers
     20 * and bail out in others.
     21 */
     22 
     23 #if !(defined(_MSC_VER) || defined(__GNUC__) || (defined(__clang__) && (__clang_major__ >= 7)))
     24 
     25 static inline int8_t
     26 FStar_Int8_shift_arithmetic_right(int8_t a, uint32_t b)
     27 {
     28    do {
     29        KRML_HOST_EPRINTF("Could not identify compiler so could not provide an implementation of signed arithmetic shift right.\n");
     30        KRML_HOST_EXIT(255);
     31    } while (0);
     32 }
     33 
     34 static inline int16_t
     35 FStar_Int16_shift_arithmetic_right(int16_t a, uint32_t b)
     36 {
     37    do {
     38        KRML_HOST_EPRINTF("Could not identify compiler so could not provide an implementation of signed arithmetic shift right.\n");
     39        KRML_HOST_EXIT(255);
     40    } while (0);
     41 }
     42 
     43 static inline int32_t
     44 FStar_Int32_shift_arithmetic_right(int32_t a, uint32_t b)
     45 {
     46    do {
     47        KRML_HOST_EPRINTF("Could not identify compiler so could not provide an implementation of signed arithmetic shift right.\n");
     48        KRML_HOST_EXIT(255);
     49    } while (0);
     50 }
     51 
     52 static inline int64_t
     53 FStar_Int64_shift_arithmetic_right(int64_t a, uint32_t b)
     54 {
     55    do {
     56        KRML_HOST_EPRINTF("Could not identify compiler so could not provide an implementation of signed arithmetic shift right.\n");
     57        KRML_HOST_EXIT(255);
     58    } while (0);
     59 }
     60 
     61 #else
     62 
     63 static inline int8_t
     64 FStar_Int8_shift_arithmetic_right(int8_t a, uint32_t b)
     65 {
     66    return (a >> b);
     67 }
     68 
     69 static inline int16_t
     70 FStar_Int16_shift_arithmetic_right(int16_t a, uint32_t b)
     71 {
     72    return (a >> b);
     73 }
     74 
     75 static inline int32_t
     76 FStar_Int32_shift_arithmetic_right(int32_t a, uint32_t b)
     77 {
     78    return (a >> b);
     79 }
     80 
     81 static inline int64_t
     82 FStar_Int64_shift_arithmetic_right(int64_t a, uint32_t b)
     83 {
     84    return (a >> b);
     85 }
     86 
     87 #endif /* !(defined(_MSC_VER) ... ) */
     88 
     89 #endif /* KRML_HEADER_FSTAR_INT_H */