diff options
Diffstat (limited to 'security/nss/lib/freebl/verified/kremlib_base.h')
| -rw-r--r-- | security/nss/lib/freebl/verified/kremlib_base.h | 191 |
1 files changed, 191 insertions, 0 deletions
diff --git a/security/nss/lib/freebl/verified/kremlib_base.h b/security/nss/lib/freebl/verified/kremlib_base.h new file mode 100644 index 000000000..61bac11d4 --- /dev/null +++ b/security/nss/lib/freebl/verified/kremlib_base.h @@ -0,0 +1,191 @@ +/* Copyright 2016-2017 INRIA and Microsoft Corporation + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +#ifndef __KREMLIB_BASE_H +#define __KREMLIB_BASE_H + +#include <inttypes.h> +#include <stdbool.h> +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <time.h> + +/******************************************************************************/ +/* Some macros to ease compatibility */ +/******************************************************************************/ + +/* Define __cdecl and friends when using GCC, so that we can safely compile code + * that contains __cdecl on all platforms. Note that this is in a separate + * header so that Dafny-generated code can include just this file. */ +#ifndef _MSC_VER +/* Use the gcc predefined macros if on a platform/architectures that set them. + * Otherwise define them to be empty. */ +#ifndef __cdecl +#define __cdecl +#endif +#ifndef __stdcall +#define __stdcall +#endif +#ifndef __fastcall +#define __fastcall +#endif +#endif + +#ifdef __GNUC__ +#define inline __inline__ +#endif + +/* GCC-specific attribute syntax; everyone else gets the standard C inline + * attribute. */ +#ifdef __GNU_C__ +#ifndef __clang__ +#define force_inline inline __attribute__((always_inline)) +#else +#define force_inline inline +#endif +#else +#define force_inline inline +#endif + +/******************************************************************************/ +/* Implementing C.fst */ +/******************************************************************************/ + +/* Uppercase issue; we have to define lowercase versions of the C macros (as we + * have no way to refer to an uppercase *variable* in F*). */ +extern int exit_success; +extern int exit_failure; + +/* This one allows the user to write C.EXIT_SUCCESS. */ +typedef int exit_code; + +void print_string(const char *s); +void print_bytes(uint8_t *b, uint32_t len); + +/* The universal null pointer defined in C.Nullity.fst */ +#define C_Nullity_null(X) 0 + +/* If some globals need to be initialized before the main, then kremlin will + * generate and try to link last a function with this type: */ +void kremlinit_globals(void); + +/******************************************************************************/ +/* Implementation of machine integers (possibly of 128-bit integers) */ +/******************************************************************************/ + +/* Integer types */ +typedef uint64_t FStar_UInt64_t, FStar_UInt64_t_; +typedef int64_t FStar_Int64_t, FStar_Int64_t_; +typedef uint32_t FStar_UInt32_t, FStar_UInt32_t_; +typedef int32_t FStar_Int32_t, FStar_Int32_t_; +typedef uint16_t FStar_UInt16_t, FStar_UInt16_t_; +typedef int16_t FStar_Int16_t, FStar_Int16_t_; +typedef uint8_t FStar_UInt8_t, FStar_UInt8_t_; +typedef int8_t FStar_Int8_t, FStar_Int8_t_; + +static inline uint32_t +rotate32_left(uint32_t x, uint32_t n) +{ + /* assert (n<32); */ + return (x << n) | (x >> (32 - n)); +} +static inline uint32_t +rotate32_right(uint32_t x, uint32_t n) +{ + /* assert (n<32); */ + return (x >> n) | (x << (32 - n)); +} + +/* Constant time comparisons */ +static inline uint8_t +FStar_UInt8_eq_mask(uint8_t x, uint8_t y) +{ + x = ~(x ^ y); + x &= x << 4; + x &= x << 2; + x &= x << 1; + return (int8_t)x >> 7; +} + +static inline uint8_t +FStar_UInt8_gte_mask(uint8_t x, uint8_t y) +{ + return ~(uint8_t)(((int32_t)x - y) >> 31); +} + +static inline uint16_t +FStar_UInt16_eq_mask(uint16_t x, uint16_t y) +{ + x = ~(x ^ y); + x &= x << 8; + x &= x << 4; + x &= x << 2; + x &= x << 1; + return (int16_t)x >> 15; +} + +static inline uint16_t +FStar_UInt16_gte_mask(uint16_t x, uint16_t y) +{ + return ~(uint16_t)(((int32_t)x - y) >> 31); +} + +static inline uint32_t +FStar_UInt32_eq_mask(uint32_t x, uint32_t y) +{ + x = ~(x ^ y); + x &= x << 16; + x &= x << 8; + x &= x << 4; + x &= x << 2; + x &= x << 1; + return ((int32_t)x) >> 31; +} + +static inline uint32_t +FStar_UInt32_gte_mask(uint32_t x, uint32_t y) +{ + return ~((uint32_t)(((int64_t)x - y) >> 63)); +} + +static inline uint64_t +FStar_UInt64_eq_mask(uint64_t x, uint64_t y) +{ + x = ~(x ^ y); + x &= x << 32; + x &= x << 16; + x &= x << 8; + x &= x << 4; + x &= x << 2; + x &= x << 1; + return ((int64_t)x) >> 63; +} + +static inline uint64_t +FStar_UInt64_gte_mask(uint64_t x, uint64_t y) +{ + uint64_t low63 = + ~((uint64_t)((int64_t)((int64_t)(x & UINT64_C(0x7fffffffffffffff)) - + (int64_t)(y & UINT64_C(0x7fffffffffffffff))) >> + 63)); + uint64_t high_bit = + ~((uint64_t)((int64_t)((int64_t)(x & UINT64_C(0x8000000000000000)) - + (int64_t)(y & UINT64_C(0x8000000000000000))) >> + 63)); + return low63 & high_bit; +} + +#endif |