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, 0 insertions, 191 deletions
diff --git a/security/nss/lib/freebl/verified/kremlib_base.h b/security/nss/lib/freebl/verified/kremlib_base.h deleted file mode 100644 index 61bac11d41..0000000000 --- a/security/nss/lib/freebl/verified/kremlib_base.h +++ /dev/null @@ -1,191 +0,0 @@ -/* 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 |