chenyuxuan/arcs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

chore: migrate project into clean repository

Browse Source
This commit is contained in:
yuuux
2026-08-13 16:50:52 +08:00
commit d1d25a09e7
27405 changed files with 9422808 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

120
arcs-sdk/modules/coresntp/test/CMakeLists.txt Normal file
View File

@@ -0,0 +1,120 @@
cmake_minimum_required( VERSION 3.13.0 )
project( "coreSNTP tests"
VERSION 1.3.1
LANGUAGES C )
# Allow the project to be organized into folders.
set_property( GLOBAL PROPERTY USE_FOLDERS ON )
# Use C90.
set( CMAKE_C_STANDARD 90 )
set( CMAKE_C_STANDARD_REQUIRED ON )
# If no configuration is defined, turn everything on.
if( NOT DEFINED COV_ANALYSIS AND NOT DEFINED UNITTEST AND NOT DEFINED BUILD_CODE_EXAMPLE )
set( COV_ANALYSIS ON )
set( UNITTEST ON )
set( BUILD_CODE_EXAMPLE ON )
endif()
# Do not allow in-source build.
if( ${PROJECT_SOURCE_DIR} STREQUAL ${PROJECT_BINARY_DIR} )
message( FATAL_ERROR "In-source build is not allowed. Please build in a separate directory, such as ${PROJECT_SOURCE_DIR}/build." )
endif()
# Set global path variables.
get_filename_component(__MODULE_ROOT_DIR "${CMAKE_CURRENT_LIST_DIR}/.." ABSOLUTE)
set( MODULE_ROOT_DIR ${__MODULE_ROOT_DIR} CACHE INTERNAL "coreSNTP source root." )
set( UNIT_TEST_DIR ${MODULE_ROOT_DIR}/test/unit-test CACHE INTERNAL "coreSNTP unit test directory." )
set( CMOCK_DIR ${UNIT_TEST_DIR}/CMock CACHE INTERNAL "Unity library source directory." )
# Configure options to always show in CMake GUI.
option( BUILD_CLONE_SUBMODULES
"Set this to ON to automatically clone any required Git submodules. When OFF, submodules must be manually cloned."
OFF )
# Set output directories.
set( CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin )
set( CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib )
set( CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib )
# Include filepaths for source and include.
include( ${MODULE_ROOT_DIR}/coreSntpFilePaths.cmake )
# ================================ Coverity Analysis Configuration =================================
if( COV_ANALYSIS )
# Target for Coverity analysis that builds the library.
add_library( coverity_analysis
${CORE_SNTP_SOURCES} )
# Add coreSNTP library public include path.
target_include_directories( coverity_analysis
PUBLIC
${CORE_SNTP_INCLUDE_PUBLIC_DIRS} )
# Build SNTP library target without custom config dependency.
target_compile_definitions( coverity_analysis PUBLIC SNTP_DO_NOT_USE_CUSTOM_CONFIG=1 )
# Build without debug enabled when performing static analysis
target_compile_options(coverity_analysis PUBLIC -DNDEBUG )
endif()
# ==================================== Code Example Build ====================================
if( BUILD_CODE_EXAMPLE )
# Target for Coverity analysis that builds the library.
add_executable( code_example_posix
${CORE_SNTP_SOURCES}
${MODULE_ROOT_DIR}/docs/doxygen/code_examples/example_sntp_client_posix.c )
target_include_directories( code_example_posix
PUBLIC
${CORE_SNTP_INCLUDE_PUBLIC_DIRS} )
# Build SNTP library target without custom config dependency.
target_compile_definitions( code_example_posix PUBLIC SNTP_DO_NOT_USE_CUSTOM_CONFIG=1 )
# Build without debug enabled when performing static analysis
target_compile_options( code_example_posix PUBLIC -DNDEBUG )
endif()
# ==================================== Unit Test Configuration ====================================
if( UNITTEST )
# Include CMock build configuration.
include( unit-test/cmock_build.cmake )
# Check if the CMock source directory exists, and if not present, clone the submodule
# if BUILD_CLONE_SUBMODULES configuration is enabled.
if( NOT EXISTS ${CMOCK_DIR}/src )
# Attempt to clone CMock.
clone_cmock()
endif()
# Add unit test and coverage configuration.
# Use CTest utility for managing test runs. This has to be added BEFORE
# defining test targets with add_test()
enable_testing()
# Add build targets for CMock, required for unit testing.
add_cmock_targets()
# Add function to enable CMock/Unity based tests and coverage.
include( ${MODULE_ROOT_DIR}/tools/cmock/create_test.cmake )
# Include build configuration for unit tests.
add_subdirectory( unit-test )
endif()
# ==================================== Coverage Analysis configuration ============================
# Add a target for running coverage on tests.
add_custom_target( coverage
COMMAND ${CMAKE_COMMAND} -DCMOCK_DIR=${CMOCK_DIR}
-P ${MODULE_ROOT_DIR}/tools/cmock/coverage.cmake
DEPENDS cmock core_sntp_client_utest core_sntp_serializer_utest
WORKING_DIRECTORY ${CMAKE_BINARY_DIR}
)

24
arcs-sdk/modules/coresntp/test/cbmc/.gitignore vendored Normal file
View File

@@ -0,0 +1,24 @@
# Emitted when running CBMC proofs
proofs/**/logs
proofs/**/gotos
proofs/**/report
proofs/**/html
proofs/output
# Emitted by CBMC Viewer
TAGS-*
# Emitted by Arpa
arpa_cmake/
arpa-validation-logs/
Makefile.arpa
# Emitted by litani
.ninja_deps
.ninja_log
.litani_cache_dir
# These files should be overwritten whenever prepare.py runs
cbmc-batch.yaml
__pycache__/

6
arcs-sdk/modules/coresntp/test/cbmc/include/README.md Normal file
View File

@@ -0,0 +1,6 @@
CBMC proof include files
========================
This directory contains include files written for CBMC proof. It is
common to write some code to model aspects of the system under test,
and the header files for this code go here.

53
arcs-sdk/modules/coresntp/test/cbmc/include/core_sntp_cbmc_state.h Normal file
View File

@@ -0,0 +1,53 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/**
* @file core_sntp_cbmc_state.h
* @brief Allocation and assumption utilities for the SNTP library CBMC proofs.
*/
#ifndef CORE_SNTP_CBMC_STATE_H_
#define CORE_SNTP_CBMC_STATE_H_
#include "core_sntp_client.h"
/* Application defined Network context. */
struct NetworkContext
{
void * networkContext;
};
/* Application defined authentication context. */
struct SntpAuthContext
{
void * authContext;
};
/**
* @brief Allocate a #SntpContext_t object.
*
* @return NULL or allocated #SntpContext_t memory.
*/
SntpContext_t * unconstrainedCoreSntpContext();
#endif /* ifndef CORE_SNTP_CBMC_STATE_H_ */

177
arcs-sdk/modules/coresntp/test/cbmc/include/core_sntp_config.h Normal file
View File

@@ -0,0 +1,177 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/**
* @file core_sntp_config_defaults.h
* @brief This file represents the default values for the configuration macros
* of the coreSNTP library.
*
* @note This file SHOULD NOT be modified. If custom values are needed for
* any configuration macro, a core_sntp_config.h file should be provided to
* the SNTP library to override the default values defined in this file.
* To build the library with the core_sntp_config.h file, make sure to
* not set the SNTP_DO_NOT_USE_CUSTOM_CONFIG preprocessor macro.
*/
#ifndef CORE_SNTP_CONFIG_DEFAULTS_H_
#define CORE_SNTP_CONFIG_DEFAULTS_H_
/* The macro definition for SNTP_DO_NOT_USE_CUSTOM_CONFIG is for Doxygen
* documentation only. */
/**
* @brief Define this macro to build the SNTP library without the custom config
* file core_sntp_config.h.
*
* Without the custom config, the SNTP library builds with
* default values of config macros defined in core_sntp_config_defaults.h file.
*
* If a custom config is provided, then SNTP_DO_NOT_USE_CUSTOM_CONFIG should not
* be defined.
*/
#ifdef DOXYGEN
#define SNTP_DO_NOT_USE_CUSTOM_CONFIG
#endif
/**
* @brief The maximum duration between non-empty network reads while
* receiving an SNTP packet via the #Sntp_ReceiveTimeResponse API function.
*
* When an incoming SNTP packet is detected, the transport receive function
* may be called multiple times until all of the expected number of bytes of the
* packet are received. This timeout represents the maximum polling duration that
* is allowed without any data reception from the network for the incoming packet.
*
* If the timeout expires, the #Sntp_ReceiveTimeResponse function will return
* #SntpErrorNetworkFailure.
*
* <b>Possible values:</b> Any positive 16 bit integer. Recommended to use a
* small timeout value. <br>
* <b>Default value:</b> `10`
*/
#ifndef SNTP_RECV_POLLING_TIMEOUT_MS
#define SNTP_RECV_POLLING_TIMEOUT_MS ( 10U )
#endif
/**
* @brief The maximum duration between non-empty network transmissions while
* sending an SNTP packet via the #Sntp_SendTimeRequest API function.
*
* When sending an SNTP packet, the transport send function may be called multiple
* times until all of the required number of bytes are sent.
* This timeout represents the maximum duration that is allowed for no data
* transmission over the network through the transport send function.
*
* If the timeout expires, the #Sntp_SendTimeRequest function will return
* #SntpErrorNetworkFailure.
*
* <b>Possible values:</b> Any positive 16 bit integer. Recommended to use a small
* timeout value. <br>
* <b>Default value:</b> `10`
*/
#ifndef SNTP_SEND_RETRY_TIMEOUT_MS
#define SNTP_SEND_RETRY_TIMEOUT_MS ( 10U )
#endif
/**
* @brief Macro that is called in the SNTP library for logging "Error" level
* messages.
*
* To enable error level logging in the SNTP library, this macro should be mapped to the
* application-specific logging implementation that supports error logging.
*
* @note This logging macro is called in the SNTP library with parameters wrapped in
* double parentheses to be ISO C89/C90 standard compliant. For a reference
* POSIX implementation of the logging macros, refer to core_sntp_config.h files, and the
* logging-stack in demos folder of the
* [AWS IoT Embedded C SDK repository](https://github.com/aws/aws-iot-device-sdk-embedded-C).
*
* <b>Default value</b>: Error logging is turned off, and no code is generated for calls
* to the macro in the SNTP library on compilation.
*/
#ifndef LogError
#define LogError( message )
#endif
/**
* @brief Macro that is called in the SNTP library for logging "Warning" level
* messages.
*
* To enable warning level logging in the SNTP library, this macro should be mapped to the
* application-specific logging implementation that supports warning logging.
*
* @note This logging macro is called in the SNTP library with parameters wrapped in
* double parentheses to be ISO C89/C90 standard compliant. For a reference
* POSIX implementation of the logging macros, refer to core_sntp_config.h files, and the
* logging-stack in demos folder of the
* [AWS IoT Embedded C SDK repository](https://github.com/aws/aws-iot-device-sdk-embedded-C/).
*
* <b>Default value</b>: Warning logs are turned off, and no code is generated for calls
* to the macro in the SNTP library on compilation.
*/
#ifndef LogWarn
#define LogWarn( message )
#endif
/**
* @brief Macro that is called in the SNTP library for logging "Info" level
* messages.
*
* To enable info level logging in the SNTP library, this macro should be mapped to the
* application-specific logging implementation that supports info logging.
*
* @note This logging macro is called in the SNTP library with parameters wrapped in
* double parentheses to be ISO C89/C90 standard compliant. For a reference
* POSIX implementation of the logging macros, refer to core_sntp_config.h files, and the
* logging-stack in demos folder of the
* [AWS IoT Embedded C SDK repository](https://github.com/aws/aws-iot-device-sdk-embedded-C/).
*
* <b>Default value</b>: Info logging is turned off, and no code is generated for calls
* to the macro in the SNTP library on compilation.
*/
#ifndef LogInfo
#define LogInfo( message )
#endif
/**
* @brief Macro that is called in the SNTP library for logging "Debug" level
* messages.
*
* To enable debug level logging from SNTP library, this macro should be mapped to the
* application-specific logging implementation that supports debug logging.
*
* @note This logging macro is called in the SNTP library with parameters wrapped in
* double parentheses to be ISO C89/C90 standard compliant. For a reference
* POSIX implementation of the logging macros, refer to core_sntp_config.h files, and the
* logging-stack in demos folder of the
* [AWS IoT Embedded C SDK repository](https://github.com/aws/aws-iot-device-sdk-embedded-C/).
*
* <b>Default value</b>: Debug logging is turned off, and no code is generated for calls
* to the macro in the SNTP library on compilation.
*/
#ifndef LogDebug
#define LogDebug( message )
#endif
#endif /* ifndef CORE_SNTP_CONFIG_DEFAULTS_H_ */

156
arcs-sdk/modules/coresntp/test/cbmc/include/core_sntp_stubs.h Normal file
View File

@@ -0,0 +1,156 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/**
* @file core_sntp_stubs_stubs.h
* @brief Stubs definitions of UDP transport interface and authentication interface of coreSNTP API.
*/
#ifndef CORE_SNTP_CBMC_STUBS_H_
#define CORE_SNTP_CBMC_STUBS_H_
#include <stddef.h>
#include <stdint.h>
#include <stdbool.h>
#include "core_sntp_client.h"
/**
* @brief Application defined network interface send function.
*
* @param[in] pNetworkContext Application defined network interface context.
* @param[in] serverAddr Server address to which application sends data.
* @param[in] serverPort Server port to which application sends data.
* @param[out] pBuffer SNTP network send buffer.
* @param[in] bytesToSend Number of bytes to send over the network.
*
* @return Any value from INT32_MIN to INT32_MAX.
*/
int32_t NetworkInterfaceSendStub( NetworkContext_t * pNetworkContext,
uint32_t serverAddr,
uint16_t serverPort,
const void * pBuffer,
uint16_t bytesToSend );
/**
* @brief Application defined network interface receive function.
*
* @param[in] pNetworkContext Application defined network interface context.
* @param[in] serverAddr Server address from which application receives data.
* @param[in] serverPort Server port from which application receives data.
* @param[out] pBuffer SNTP network receive buffer.
* @param[in] bytesToRecv SNTP requested bytes.
*
* @return Any value from INT32_MIN to INT32_MAX.
*/
int32_t NetworkInterfaceReceiveStub( NetworkContext_t * pNetworkContext,
uint32_t serverAddr,
uint16_t serverPort,
void * pBuffer,
uint16_t bytesToRecv );
/**
* @brief Application defined function to generate and append
* authentication code in an SNTP request buffer for the SNTP client to be
* authenticated by the time server, if a security mechanism is used.
*
* @param[in] pContext Application defined authentication interface context.
* @param[in] pTimeServer The time server being used to request time from.
* This parameter is useful to choose the security mechanism when multiple time
* servers are configured in the library, and they require different security
* mechanisms or authentication credentials to use.
* @param[in] pBuffer SNTP request buffer.
* @param[in] bufferSize The maximum amount of data that can be held by the buffer.
* @param[out] pAuthCodeSize This should be filled with size of the authentication
* data appended to the SNTP request buffer, @p pBuffer.
*
* @return The function SHOULD return one of the following integer codes:
* - #SntpSuccess when the authentication data is successfully appended to @p pBuffer.
* - #SntpErrorBufferTooSmall when the user-supplied buffer (to the SntpContext_t through
* @ref Sntp_Init) is not large enough to hold authentication data.
*/
SntpStatus_t GenerateClientAuthStub( SntpAuthContext_t * pContext,
const SntpServerInfo_t * pTimeServer,
void * pBuffer,
size_t bufferSize,
uint16_t * pAuthCodeSize );
/**
* @brief Application defined function to authenticate server by validating
* the authentication code present in its SNTP response to a time request, if
* a security mechanism is supported by the server.
*
* @param[in,out] pContext The application defined NetworkContext_t which
* is opaque to the coreSNTP library.
* @param[in] pTimeServer The time server that has to be authenticated from its
* SNTP response.
* @param[in] pResponseData The SNTP response from the server that contains the
* authentication code after the first #SNTP_PACKET_BASE_SIZE bytes.
* @param[in] responseSize The total size of the response from the server.
*
* @return The function ALWAYS returns #SntpSuccess
*/
SntpStatus_t ValidateServerAuthStub( SntpAuthContext_t * pContext,
const SntpServerInfo_t * pTimeServer,
const void * pResponseData,
uint16_t responseSize );
/**
* @brief Application defined function to resolve time server domain-name
* to an IPv4 address.
*
* @param[in] pTimeServer The time-server whose IPv4 address is to be resolved.
* @param[out] pIpV4Addr This should be filled with the resolved IPv4 address.
* of @p pTimeServer.
*
* @return `true` if DNS resolution is successful; otherwise `false` to represent
* failure.
*/
bool ResolveDnsFuncStub( const SntpServerInfo_t * pServerAddr,
uint32_t * pIpV4Addr );
/**
* @brief Application defined function to obtain the current system time
* in SNTP timestamp format.
*
* @param[out] pCurrentTime This should be filled with the current system time
* in SNTP timestamp format.
*/
void GetTimeFuncStub( SntpTimestamp_t * pCurrentTime );
/**
* @brief Application defined function to update the system clock time
* so that it is synchronized the time server used for getting current time.
*
* @param[in] pTimeServer The time server used to request time.
* @param[in] pServerTime The current time returned by the @p pTimeServer.
* @param[in] clockOffSetMs The calculated clock offset of the system relative
* to the server time.
* @param[in] leapSecondInfo Information about whether there is about an upcoming
* leap second adjustment.
*/
void SetTimeFuncStub( const SntpServerInfo_t * pTimeServer,
const SntpTimestamp_t * pServerTime,
int64_t clockOffsetMs,
SntpLeapSecondInfo_t leapSecondInfo );
#endif /* ifndef CORE_SNTP_CBMC_STUBS_H_ */

39
arcs-sdk/modules/coresntp/test/cbmc/proofs/Makefile-project-defines Normal file
View File

@@ -0,0 +1,39 @@
# -*- mode: makefile -*-
# The first line sets the emacs major mode to Makefile
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
################################################################
# Use this file to give project-specific definitions of the command
# line arguments to pass to CBMC tools like goto-cc to build the goto
# binaries and cbmc to do the property and coverage checking.
#
# Use this file to override most default definitions of variables in
# Makefile.common.
################################################################
# Flags to pass to goto-cc for compilation (typically those passed to gcc -c)
COMPILE_FLAGS += -fPIC
COMPILE_FLAGS += -std=gnu90
# Flags to pass to goto-cc for linking (typically those passed to gcc)
# LINK_FLAGS =
# Preprocessor include paths -I...
# Consider adding
# INCLUDES += -I$(CBMC_ROOT)/include
# You will want to decide what order that comes in relative to the other
# include directories in your project.
#
INCLUDES += -I$(SRCDIR)/test/cbmc/include
INCLUDES += -I$(SRCDIR)/source/include
# Preprocessor definitions -D...
# DEFINES =
# Path to arpa executable
# ARPA =
# Flags to pass to cmake for building the project
# ARPA_CMAKE_FLAGS =

10
arcs-sdk/modules/coresntp/test/cbmc/proofs/Makefile-project-targets Normal file
View File

@@ -0,0 +1,10 @@
# -*- mode: makefile -*-
# The first line sets the emacs major mode to Makefile
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
################################################################
# Use this file to give project-specific targets, including targets
# that may depend on targets defined in Makefile.common.
################################################################

11
arcs-sdk/modules/coresntp/test/cbmc/proofs/Makefile-project-testing Normal file
View File

@@ -0,0 +1,11 @@
# -*- mode: makefile -*-
# The first line sets the emacs major mode to Makefile
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
################################################################
# Use this file to define project-specific targets and definitions for
# unit testing or continuous integration that may depend on targets
# defined in Makefile.common
################################################################

20
arcs-sdk/modules/coresntp/test/cbmc/proofs/Makefile-template-defines Normal file
View File

@@ -0,0 +1,20 @@
PROOF_ROOT ?= $(abspath .)
# Absolute path to the root of the source tree.
#
SRCDIR ?= $(abspath $(PROOF_ROOT)/../../..)
# Absolute path to the litani script.
#
LITANI ?= litani
# Name of this proof project, displayed in proof reports. For example,
# "s2n" or "Amazon FreeRTOS". For projects with multiple proof roots,
# this may be overridden on the command-line to Make, for example
#
# make PROJECT_NAME="FreeRTOS MQTT" report
#
PROJECT_NAME = "coreSNTP"

999
arcs-sdk/modules/coresntp/test/cbmc/proofs/Makefile.common Normal file
View File

@@ -0,0 +1,999 @@
# -*- mode: makefile -*-
# The first line sets the emacs major mode to Makefile
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.5
################################################################
# The CBMC Starter Kit depends on the files Makefile.common and
# run-cbmc-proofs.py. They are installed by the setup script
# cbmc-starter-kit-setup and updated to the latest version by the
# update script cbmc-starter-kit-update. For more information about
# the starter kit and these files and these scripts, see
# https://model-checking.github.io/cbmc-starter-kit
#
# Makefile.common implements what we consider to be some best
# practices for using cbmc for software verification.
#
# Section I gives default values for a large number of Makefile
# variables that control
# * how your code is built (include paths, etc),
# * what program transformations are applied to your code (loop
# unwinding, etc), and
# * what properties cbmc checks for in your code (memory safety, etc).
#
# These variables are defined below with definitions of the form
# VARIABLE ?= DEFAULT_VALUE
# meaning VARIABLE is set to DEFAULT_VALUE if VARIABLE has not already
# been given a value.
#
# For your project, you can override these default values with
# project-specific definitions in Makefile-project-defines.
#
# For any individual proof, you can override these default values and
# project-specific values with proof-specific definitions in the
# Makefile for your proof.
#
# The definitions in the proof Makefile override definitions in the
# project Makefile-project-defines which override definitions in this
# Makefile.common.
#
# Section II uses the values defined in Section I to build your code, run
# your proof, and build a report of your results. You should not need
# to modify or override anything in Section II, but you may want to
# read it to understand how the values defined in Section I control
# things.
#
# To use Makefile.common, set variables as described above as needed,
# and then for each proof,
#
# * Create a subdirectory <DIR>.
# * Write a proof harness (a function) with the name <HARNESS_ENTRY>
# in a file with the name <DIR>/<HARNESS_FILE>.c
# * Write a makefile with the name <DIR>/Makefile that looks
# something like
#
# HARNESS_FILE=<HARNESS_FILE>
# HARNESS_ENTRY=<HARNESS_ENTRY>
# PROOF_UID=<PROOF_UID>
#
# PROJECT_SOURCES += $(SRCDIR)/libraries/api_1.c
# PROJECT_SOURCES += $(SRCDIR)/libraries/api_2.c
#
# PROOF_SOURCES += $(PROOFDIR)/harness.c
# PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_a.c
# PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_b.c
#
# UNWINDSET += foo.0:3
# UNWINDSET += bar.1:6
#
# REMOVE_FUNCTION_BODY += api_stub_a
# REMOVE_FUNCTION_BODY += api_stub_b
#
# DEFINES = -DDEBUG=0
#
# include ../Makefile.common
#
# * Change directory to <DIR> and run make
#
# The proof setup script cbmc-starter-kit-setup-proof from the CBMC
# Starter Kit will do most of this for, creating a directory and
# writing a basic Makefile and proof harness into it that you can edit
# as described above.
#
# Warning: If you get results that are hard to explain, consider
# running "make clean" or "make veryclean" before "make" if you get
# results that are hard to explain. Dependency handling in this
# Makefile.common may not be perfect.
SHELL=/bin/bash
default: report
################################################################
################################################################
## Section I: This section gives common variable definitions.
##
## Override these definitions in Makefile-project-defines or
## your proof Makefile.
##
## Remember that Makefile.common and Makefile-project-defines are
## included into the proof Makefile in your proof directory, so all
## relative pathnames defined there should be relative to your proof
## directory.
################################################################
# Define the layout of the source tree and the proof subtree
#
# Generally speaking,
#
# SRCDIR = the root of the repository
# CBMC_ROOT = /srcdir/cbmc
# PROOF_ROOT = /srcdir/cbmc/proofs
# PROOF_SOURCE = /srcdir/cbmc/sources
# PROOF_INCLUDE = /srcdir/cbmc/include
# PROOF_STUB = /srcdir/cbmc/stubs
# PROOFDIR = the directory containing the Makefile for your proof
#
# The path /srcdir/cbmc used in the example above is determined by the
# setup script cbmc-starter-kit-setup. Projects usually create a cbmc
# directory somewhere in the source tree, and run the setup script in
# that directory. The value of CBMC_ROOT becomes the absolute path to
# that directory.
#
# The location of that cbmc directory in the source tree affects the
# definition of SRCDIR, which is defined in terms of the relative path
# from a proof directory to the repository root. The definition is
# usually determined by the setup script cbmc-starter-kit-setup and
# written to Makefile-template-defines, but you can override it for a
# project in Makefile-project-defines and for a specific proof in the
# Makefile for the proof.
# Absolute path to the directory containing this Makefile.common
# See https://ftp.gnu.org/old-gnu/Manuals/make-3.80/html_node/make_17.html
#
# Note: We compute the absolute paths to the makefiles in MAKEFILE_LIST
# before we filter the list of makefiles for %/Makefile.common.
# Otherwise an invocation of the form "make -f Makefile.common" will set
# MAKEFILE_LIST to "Makefile.common" which will fail to match the
# pattern %/Makefile.common.
#
MAKEFILE_PATHS = $(foreach makefile,$(MAKEFILE_LIST),$(abspath $(makefile)))
PROOF_ROOT = $(dir $(filter %/Makefile.common,$(MAKEFILE_PATHS)))
CBMC_ROOT = $(shell dirname $(PROOF_ROOT))
PROOF_SOURCE = $(CBMC_ROOT)/sources
PROOF_INCLUDE = $(CBMC_ROOT)/include
PROOF_STUB = $(CBMC_ROOT)/stubs
# Project-specific definitions to override default definitions below
# * Makefile-project-defines will never be overwritten
# * Makefile-template-defines may be overwritten when the starter
# kit is updated
sinclude $(PROOF_ROOT)/Makefile-project-defines
sinclude $(PROOF_ROOT)/Makefile-template-defines
# SRCDIR is the path to the root of the source tree
# This is a default definition that is frequently overridden in
# another Makefile, see the discussion of SRCDIR above.
SRCDIR ?= $(abspath ../..)
# PROOFDIR is the path to the directory containing the proof harness
PROOFDIR ?= $(abspath .)
################################################################
# Define how to run CBMC
# Do property checking with the external SAT solver given by
# EXTERNAL_SAT_SOLVER. Do coverage checking with the default solver,
# since coverage checking requires the use of an incremental solver.
# The EXTERNAL_SAT_SOLVER variable is typically set (if it is at all)
# as an environment variable or as a makefile variable in
# Makefile-project-defines.
#
# For a particular proof, if the default solver is faster, do property
# checking with the default solver by including this definition in the
# proof Makefile:
# USE_EXTERNAL_SAT_SOLVER =
#
ifneq ($(strip $(EXTERNAL_SAT_SOLVER)),)
USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver $(EXTERNAL_SAT_SOLVER)
endif
CHECKFLAGS += $(USE_EXTERNAL_SAT_SOLVER)
# Job pools
# For version of Litani that are new enough (where `litani print-capabilities`
# prints "pools"), proofs for which `EXPENSIVE = true` is set can be added to a
# "job pool" that restricts how many expensive proofs are run at a time. All
# other proofs will be built in parallel as usual.
#
# In more detail: all compilation, instrumentation, and report jobs are run with
# full parallelism as usual, even for expensive proofs. The CBMC jobs for
# non-expensive proofs are also run in parallel. The only difference is that the
# CBMC safety checks and coverage checks for expensive proofs are run with a
# restricted parallelism level. At any one time, only N of these jobs are run at
# once, amongst all the proofs.
#
# To configure N, Litani needs to be initialized with a pool called "expensive".
# For example, to only run two CBMC safety/coverage jobs at a time from amongst
# all the proofs, you would initialize litani like
# litani init --pools expensive:2
# The run-cbmc-proofs.py script takes care of this initialization through the
# --expensive-jobs-parallelism flag.
#
# To enable this feature, set
# the ENABLE_POOLS variable when running Make, like
# `make ENABLE_POOLS=true report`
# The run-cbmc-proofs.py script takes care of this through the
# --restrict-expensive-jobs flag.
ifeq ($(strip $(ENABLE_POOLS)),)
POOL =
else ifeq ($(strip $(EXPENSIVE)),)
POOL =
else
POOL = --pool expensive
endif
# Similar to the pool feature above. If Litani is new enough, enable
# profiling CBMC's memory use.
ifeq ($(strip $(ENABLE_MEMORY_PROFILING)),)
MEMORY_PROFILING =
else
MEMORY_PROFILING = --profile-memory
endif
# Property checking flags
#
# Each variable below controls a specific property checking flag
# within CBMC. If desired, a property flag can be disabled within
# a particular proof by nulling the corresponding variable. For
# instance, the following line:
#
# CHECK_FLAG_POINTER_CHECK =
#
# would disable the --pointer-check CBMC flag within:
# * an entire project when added to Makefile-project-defines
# * a specific proof when added to the harness Makefile
CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-may-fail
CBMC_FLAG_MALLOC_FAIL_NULL ?= --malloc-fail-null
CBMC_FLAG_BOUNDS_CHECK ?= --bounds-check
CBMC_FLAG_CONVERSION_CHECK ?= --conversion-check
CBMC_FLAG_DIV_BY_ZERO_CHECK ?= --div-by-zero-check
CBMC_FLAG_FLOAT_OVERFLOW_CHECK ?= --float-overflow-check
CBMC_FLAG_NAN_CHECK ?= --nan-check
CBMC_FLAG_POINTER_CHECK ?= --pointer-check
CBMC_FLAG_POINTER_OVERFLOW_CHECK ?= --pointer-overflow-check
CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= --pointer-primitive-check
CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= --signed-overflow-check
CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= --undefined-shift-check
CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK ?= --unsigned-overflow-check
CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions
CBMC_FLAG_UNWIND ?= --unwind 1
CBMC_FLAG_FLUSH ?= --flush
# CBMC flags used for property checking and coverage checking
CBMCFLAGS += $(CBMC_FLAG_UNWIND) $(CBMC_UNWINDSET) $(CBMC_FLAG_FLUSH)
# CBMC flags used for property checking
CHECKFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL)
CHECKFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
CHECKFLAGS += $(CBMC_FLAG_BOUNDS_CHECK)
CHECKFLAGS += $(CBMC_FLAG_CONVERSION_CHECK)
CHECKFLAGS += $(CBMC_FLAG_DIV_BY_ZERO_CHECK)
CHECKFLAGS += $(CBMC_FLAG_FLOAT_OVERFLOW_CHECK)
CHECKFLAGS += $(CBMC_FLAG_NAN_CHECK)
CHECKFLAGS += $(CBMC_FLAG_POINTER_CHECK)
CHECKFLAGS += $(CBMC_FLAG_POINTER_OVERFLOW_CHECK)
CHECKFLAGS += $(CBMC_FLAG_POINTER_PRIMITIVE_CHECK)
CHECKFLAGS += $(CBMC_FLAG_SIGNED_OVERFLOW_CHECK)
CHECKFLAGS += $(CBMC_FLAG_UNDEFINED_SHIFT_CHECK)
CHECKFLAGS += $(CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK)
CHECKFLAGS += $(CBMC_FLAG_UNWINDING_ASSERTIONS)
# CBMC flags used for coverage checking
COVERFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL)
COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
# Additional CBMC flag to CBMC control verbosity.
#
# Meaningful values are
# 0 none
# 1 only errors
# 2 + warnings
# 4 + results
# 6 + status/phase information
# 8 + statistical information
# 9 + progress information
# 10 + debug info
#
# Uncomment the following line or set in Makefile-project-defines
# CBMC_VERBOSITY ?= --verbosity 4
# Additional CBMC flag to control how CBMC treats static variables.
#
# NONDET_STATIC is a list of flags of the form --nondet-static
# and --nondet-static-exclude VAR. The --nondet-static flag causes
# CBMC to initialize static variables with unconstrained value
# (ignoring initializers and default zero-initialization). The
# --nondet-static-exclude VAR excludes VAR for the variables
# initialized with unconstrained values.
NONDET_STATIC ?=
# Flags to pass to goto-cc for compilation and linking
COMPILE_FLAGS ?= -Wall
LINK_FLAGS ?= -Wall
EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols
# Preprocessor include paths -I...
INCLUDES ?=
# Preprocessor definitions -D...
DEFINES ?=
# CBMC object model
#
# CBMC_OBJECT_BITS is the number of bits in a pointer CBMC uses for
# the id of the object to which a pointer is pointing. CBMC uses 8
# bits for the object id by default. The remaining bits in the pointer
# are used for offset into the object. This limits the size of the
# objects that CBMC can model. This Makefile defines this bound on
# object size to be CBMC_MAX_OBJECT_SIZE. You are likely to get
# unexpected results if you try to malloc an object larger than this
# bound.
CBMC_OBJECT_BITS ?= 8
# CBMC loop unwinding (Normally set in the proof Makefile)
#
# UNWINDSET is a list of pairs of the form foo.1:4 meaning that
# CBMC should unwind loop 1 in function foo no more than 4 times.
# For historical reasons, the number 4 is one more than the number
# of times CBMC actually unwinds the loop.
UNWINDSET ?=
# CBMC early loop unwinding (Normally set in the proof Makefile)
#
# Most users can ignore this variable.
#
# This variable exists to support the use of loop and function
# contracts, two features under development for CBMC. Checking the
# assigns clause for function contracts and loop invariants currently
# assumes loop-free bodies for loops and functions with contracts
# (possibly after replacing nested loops with their own loop
# contracts). To satisfy this requirement, it may be necessary to
# unwind some loops before the function contract and loop invariant
# transformations are applied to the goto program. This variable
# EARLY_UNWINDSET is identical to UNWINDSET, and we assume that the
# loops mentioned in EARLY_UNWINDSET and UNWINDSET are disjoint.
EARLY_UNWINDSET ?=
# CBMC function removal (Normally set set in the proof Makefile)
#
# REMOVE_FUNCTION_BODY is a list of function names. CBMC will "undefine"
# the function, and CBMC will treat the function as having no side effects
# and returning an unconstrained value of the appropriate return type.
# The list should include the names of functions being stubbed out.
REMOVE_FUNCTION_BODY ?=
# CBMC function pointer restriction (Normally set in the proof Makefile)
#
# RESTRICT_FUNCTION_POINTER is a list of function pointer restriction
# instructions of the form:
#
# <fun_id>.function_pointer_call.<N>/<fun_id>[,<fun_id>]*
#
# The function pointer call number <N> in the specified function gets
# rewritten to a case switch over a finite list of functions.
# If some possible target functions are omitted from the list a counter
# example trace will be found by CBMC, i.e. the transformation is sound.
# If the target functions are file-local symbols, then mangled names must
# be used.
RESTRICT_FUNCTION_POINTER ?=
# The project source files (Normally set set in the proof Makefile)
#
# PROJECT_SOURCES is the list of project source files to compile,
# including the source file defining the function under test.
PROJECT_SOURCES ?=
# The proof source files (Normally set in the proof Makefile)
#
# PROOF_SOURCES is the list of proof source files to compile, including
# the proof harness, and including any function stubs being used.
PROOF_SOURCES ?=
# The number of seconds that CBMC should be allowed to run for before
# being forcefully terminated. Currently, this is set to be less than
# the time limit for a CodeBuild job, which is eight hours. If a proof
# run takes longer than the time limit of the CI environment, the
# environment will halt the proof run without updating the Litani
# report, making the proof run appear to "hang".
CBMC_TIMEOUT ?= 21600
# Proof writers could add function contracts in their source code.
# These contracts are ignored by default, but may be enabled in two distinct
# contexts using the following two variables:
# 1. To check whether one or more function contracts are sound with respect to
# the function implementation, CHECK_FUNCTION_CONTRACTS should be a list of
# function names.
# 2. To replace calls to certain functions with their correspondent function
# contracts, USE_FUNCTION_CONTRACTS should be a list of function names.
# One must check separately whether a function contract is sound before
# replacing it in calling contexts.
CHECK_FUNCTION_CONTRACTS ?=
CBMC_CHECK_FUNCTION_CONTRACTS := $(patsubst %,--enforce-contract %, $(CHECK_FUNCTION_CONTRACTS))
USE_FUNCTION_CONTRACTS ?=
CBMC_USE_FUNCTION_CONTRACTS := $(patsubst %,--replace-call-with-contract %, $(USE_FUNCTION_CONTRACTS))
# Similarly, proof writers could also add loop contracts in their source code
# to obtain unbounded correctness proofs. Unlike function contracts, loop
# contracts are not reusable and thus are checked and used simultaneously.
# These contracts are also ignored by default, but may be enabled by setting
# the APPLY_LOOP_CONTRACTS variable to 1.
APPLY_LOOP_CONTRACTS ?= 0
ifeq ($(APPLY_LOOP_CONTRACTS),1)
CBMC_APPLY_LOOP_CONTRACTS ?= --apply-loop-contracts
endif
# Silence makefile output (eg, long litani commands) unless VERBOSE is set.
ifndef VERBOSE
MAKEFLAGS := $(MAKEFLAGS) -s
endif
################################################################
################################################################
## Section II: This section defines the process of running a proof
##
## There should be no reason to edit anything below this line.
################################################################
# Paths
CBMC ?= cbmc
GOTO_ANALYZER ?= goto-analyzer
GOTO_CC ?= goto-cc
GOTO_INSTRUMENT ?= goto-instrument
CRANGLER ?= crangler
VIEWER ?= cbmc-viewer
MAKE_SOURCE ?= make-source
VIEWER2 ?= cbmc-viewer
CMAKE ?= cmake
GOTODIR ?= $(PROOFDIR)/gotos
LOGDIR ?= $(PROOFDIR)/logs
PROJECT ?= project
PROOF ?= proof
HARNESS_GOTO ?= $(GOTODIR)/$(HARNESS_FILE)
PROJECT_GOTO ?= $(GOTODIR)/$(PROJECT)
PROOF_GOTO ?= $(GOTODIR)/$(PROOF)
################################################################
# Useful macros for values that are hard to reference
SPACE :=$() $()
COMMA :=,
################################################################
# Set C compiler defines
CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
COMPILE_FLAGS += --object-bits $(CBMC_OBJECT_BITS)
DEFINES += -DCBMC=1
DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)
DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))"
# CI currently assumes cbmc invocation has at most one --unwindset
ifdef UNWINDSET
ifneq ($(strip $(UNWINDSET)),"")
CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET)))
endif
endif
ifdef EARLY_UNWINDSET
ifneq ($(strip $(EARLY_UNWINDSET)),"")
CBMC_EARLY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(EARLY_UNWINDSET)))
endif
endif
CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY))
CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER))
################################################################
# Targets for rewriting source files with crangler
# Construct crangler configuration files
#
# REWRITTEN_SOURCES is a list of crangler output files source.i.
# This target assumes that for each source.i
# * source.i_SOURCE is the path to a source file,
# * source.i_FUNCTIONS is a list of functions (may be empty)
# * source.i_OBJECTS is a list of variables (may be empty)
# This target constructs the crangler configuration file source.i.json
# of the form
# {
# "sources": [ "/proj/code.c" ],
# "includes": [ "/proj/include" ],
# "defines": [ "VAR=1" ],
# "functions": [ {"function_name": ["remove static"]} ],
# "objects": [ {"variable_name": ["remove static"]} ],
# "output": "source.i"
# }
# to remove the static attribute from function_name and variable_name
# in the source file source.c and write the result to source.i.
#
# This target assumes that filenames include no spaces and that
# the INCLUDES and DEFINES variables include no spaces after -I
# and -D. For example, use "-DVAR=1" and not "-D VAR=1".
#
# Define *_SOURCE, *_FUNCTIONS, and *_OBJECTS in the proof Makefile.
# The string source.i is usually an absolute path $(PROOFDIR)/code.i
# to a file in the proof directory that contains the proof Makefile.
# The proof Makefile usually includes the definitions
# $(PROOFDIR)/code.i_SOURCE = /proj/code.c
# $(PROOFDIR)/code.i_FUNCTIONS = function_name
# $(PROOFDIR)/code.i_OBJECTS = variable_name
# Because these definitions refer to PROOFDIR that is defined in this
# Makefile.common, these definitions must appear after the inclusion
# of Makefile.common in the proof Makefile.
#
$(foreach rs,$(REWRITTEN_SOURCES),$(eval $(rs).json: $($(rs)_SOURCE)))
$(foreach rs,$(REWRITTEN_SOURCES),$(rs).json):
echo '{'\
'"sources": ['\
'"$($(@:.json=)_SOURCE)"'\
'],'\
'"includes": ['\
'$(subst $(SPACE),$(COMMA),$(patsubst -I%,"%",$(strip $(INCLUDES))))' \
'],'\
'"defines": ['\
'$(subst $(SPACE),$(COMMA),$(patsubst -D%,"%",$(subst ",\",$(strip $(DEFINES)))))' \
'],'\
'"functions": ['\
'{'\
'$(subst ~, ,$(subst $(SPACE),$(COMMA),$(patsubst %,"%":["remove~static"],$($(@:.json=)_FUNCTIONS))))' \
'}'\
'],'\
'"objects": ['\
'{'\
'$(subst ~, ,$(subst $(SPACE),$(COMMA),$(patsubst %,"%":["remove~static"],$($(@:.json=)_OBJECTS))))' \
'}'\
'],'\
'"output": "$(@:.json=)"'\
'}' > $@
# Rewrite source files with crangler
#
$(foreach rs,$(REWRITTEN_SOURCES),$(eval $(rs): $(rs).json))
$(REWRITTEN_SOURCES):
$(LITANI) add-job \
--command \
'$(CRANGLER) $@.json' \
--inputs $($@_SOURCE) \
--outputs $@ \
--stdout-file $(LOGDIR)/crangler-$(subst /,_,$(subst .,_,$@))-log.txt \
--interleave-stdout-stderr \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): removing static"
################################################################
# Build targets that make the relevant .goto files
# Compile project sources
$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
$(LITANI) add-job \
--command \
'$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/project_sources-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): building project binary"
# Compile proof sources
$(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
$(LITANI) add-job \
--command \
'$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/proof_sources-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): building proof binary"
# Remove function bodies from project sources
$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/remove_function_body-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): removing function bodies from project sources"
# Link project and proof sources into the proof harness
$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
$(LITANI) add-job \
--command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ $(LINK_FLAGS) -o $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/link_proof_project-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): linking project to proof"
# Restrict function pointers
$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/restrict_function_pointer-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): restricting function pointers in project sources"
# Fill static variable with unconstrained values
$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/nondet_static-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): setting static variables to nondet"
# Omit unused functions (sharpens coverage calculations)
$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/drop_unused_functions-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): dropping unused functions"
# Omit initialization of unused global variables (reduces problem size)
$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/slice_global_inits-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): slicing global initializations"
# Replace function calls with function contracts
# This must be done before enforcing function contracts,
# since contract enforcement inlines all function calls.
$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/use_function_contracts-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): replacing function calls with function contracts"
# Unwind loops for loop and function contracts
$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_EARLY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/unwind_loops-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): unwinding loops"
# Apply loop contracts
$(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/apply_loop_contracts-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): applying loop contracts"
# Check function contracts
$(HARNESS_GOTO)9.goto: $(HARNESS_GOTO)8.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/check_function_contracts-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): checking function contracts"
# Final name for proof harness
$(HARNESS_GOTO).goto: $(HARNESS_GOTO)9.goto
$(LITANI) add-job \
--command 'cp $< $@' \
--inputs $^ \
--outputs $@ \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): copying final goto-binary"
################################################################
# Targets to run the analysis commands
$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
$(LITANI) add-job \
$(POOL) \
--command \
'$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \
--inputs $^ \
--outputs $@ \
--ci-stage test \
--stdout-file $@ \
$(MEMORY_PROFILING) \
--ignore-returns 10 \
--timeout $(CBMC_TIMEOUT) \
--pipeline-name "$(PROOF_UID)" \
--tags "stats-group:safety checks" \
--stderr-file $(LOGDIR)/result-err-log.txt \
--description "$(PROOF_UID): checking safety properties"
$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto
$(LITANI) add-job \
$(POOL) \
--command \
'$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace --xml-ui $<' \
--inputs $^ \
--outputs $@ \
--ci-stage test \
--stdout-file $@ \
$(MEMORY_PROFILING) \
--ignore-returns 10 \
--timeout $(CBMC_TIMEOUT) \
--pipeline-name "$(PROOF_UID)" \
--tags "stats-group:safety checks" \
--stderr-file $(LOGDIR)/result-err-log.txt \
--description "$(PROOF_UID): checking safety properties"
$(LOGDIR)/property.xml: $(HARNESS_GOTO).goto
$(LITANI) add-job \
--command \
'$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --show-properties --xml-ui $<' \
--inputs $^ \
--outputs $@ \
--ci-stage test \
--stdout-file $@ \
--ignore-returns 10 \
--pipeline-name "$(PROOF_UID)" \
--stderr-file $(LOGDIR)/property-err-log.txt \
--description "$(PROOF_UID): printing safety properties"
$(LOGDIR)/coverage.xml: $(HARNESS_GOTO).goto
$(LITANI) add-job \
$(POOL) \
--command \
'$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(COVERFLAGS) --cover location --xml-ui $<' \
--inputs $^ \
--outputs $@ \
--ci-stage test \
--stdout-file $@ \
$(MEMORY_PROFILING) \
--ignore-returns 10 \
--timeout $(CBMC_TIMEOUT) \
--pipeline-name "$(PROOF_UID)" \
--tags "stats-group:coverage computation" \
--stderr-file $(LOGDIR)/coverage-err-log.txt \
--description "$(PROOF_UID): calculating coverage"
define VIEWER_CMD
$(VIEWER) \
--result $(LOGDIR)/result.txt \
--block $(LOGDIR)/coverage.xml \
--property $(LOGDIR)/property.xml \
--srcdir $(SRCDIR) \
--goto $(HARNESS_GOTO).goto \
--htmldir $(PROOFDIR)/html
endef
export VIEWER_CMD
$(PROOFDIR)/html: $(LOGDIR)/result.txt $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml
$(LITANI) add-job \
--command "$$VIEWER_CMD" \
--inputs $^ \
--outputs $(PROOFDIR)/html \
--pipeline-name "$(PROOF_UID)" \
--ci-stage report \
--stdout-file $(LOGDIR)/viewer-log.txt \
--description "$(PROOF_UID): generating report"
# Caution: run make-source before running property and coverage checking
# The current make-source script removes the goto binary
$(LOGDIR)/source.json:
mkdir -p $(dir $@)
$(RM) -r $(GOTODIR)
$(MAKE_SOURCE) --srcdir $(SRCDIR) --wkdir $(PROOFDIR) > $@
$(RM) -r $(GOTODIR)
define VIEWER2_CMD
$(VIEWER2) \
--result $(LOGDIR)/result.xml \
--coverage $(LOGDIR)/coverage.xml \
--property $(LOGDIR)/property.xml \
--srcdir $(SRCDIR) \
--goto $(HARNESS_GOTO).goto \
--reportdir $(PROOFDIR)/report \
--config $(PROOFDIR)/cbmc-viewer.json
endef
export VIEWER2_CMD
# Omit logs/source.json from report generation until make-sources
# works correctly with Makefiles that invoke the compiler with
# mutliple source files at once.
$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml
$(LITANI) add-job \
--command "$$VIEWER2_CMD" \
--inputs $^ \
--outputs $(PROOFDIR)/report \
--pipeline-name "$(PROOF_UID)" \
--stdout-file $(LOGDIR)/viewer-log.txt \
--ci-stage report \
--description "$(PROOF_UID): generating report"
litani-path:
@echo $(LITANI)
# ##############################################################
# Phony Rules
#
# These rules provide a convenient way to run a single proof up to a
# certain stage. Users can browse into a proof directory and run
# "make -Bj 3 report" to generate a report for just that proof, or
# "make goto" to build the goto binary. Under the hood, this runs litani
# for just that proof.
_goto: $(HARNESS_GOTO).goto
goto:
@ echo Running 'litani init'
$(LITANI) init --project $(PROJECT_NAME)
@ echo Running 'litani add-job'
$(MAKE) -B _goto
@ echo Running 'litani build'
$(LITANI) run-build
_result: $(LOGDIR)/result.txt
result:
@ echo Running 'litani init'
$(LITANI) init --project $(PROJECT_NAME)
@ echo Running 'litani add-job'
$(MAKE) -B _result
@ echo Running 'litani build'
$(LITANI) run-build
_property: $(LOGDIR)/property.xml
property:
@ echo Running 'litani init'
$(LITANI) init --project $(PROJECT_NAME)
@ echo Running 'litani add-job'
$(MAKE) -B _property
@ echo Running 'litani build'
$(LITANI) run-build
_coverage: $(LOGDIR)/coverage.xml
coverage:
@ echo Running 'litani init'
$(LITANI) init --project $(PROJECT_NAME)
@ echo Running 'litani add-job'
$(MAKE) -B _coverage
@ echo Running 'litani build'
$(LITANI) run-build
# Choose the invocation of cbmc-viewer depending on which version of
# cbmc-viewer is installed. The --version flag is not implemented in
# version 1 --- it is an "unrecognized argument" --- but it is
# implemented in version 2.
_report1: $(PROOFDIR)/html
_report2: $(PROOFDIR)/report
_report:
(cbmc-viewer --version 2>&1 | grep "unrecognized argument" > /dev/null) && \
$(MAKE) -B _report1 || $(MAKE) -B _report2
report report1 report2:
@ echo Running 'litani init'
$(LITANI) init --project $(PROJECT_NAME)
@ echo Running 'litani add-job'
$(MAKE) -B _report
@ echo Running 'litani build'
$(LITANI) run-build
################################################################
# Targets to clean up after ourselves
clean:
-$(RM) $(DEPENDENT_GOTOS)
-$(RM) TAGS*
-$(RM) *~ \#*
-$(RM) $(REWRITTEN_SOURCES) $(foreach rs,$(REWRITTEN_SOURCES),$(rs).json)
veryclean: clean
-$(RM) -r html report
-$(RM) -r $(LOGDIR) $(GOTODIR)
.PHONY: \
_coverage \
_goto \
_property \
_report \
_report2 \
_result \
clean \
coverage \
goto \
litani-path \
property \
report \
report2 \
result \
setup_dependencies \
testdeps \
veryclean \
#
################################################################
# Rule for generating cbmc-batch.yaml, used by the CI at
# https://github.com/awslabs/aws-batch-cbmc/
JOB_OS ?= ubuntu16
JOB_MEMORY ?= 32000
# Proofs that are expected to fail should set EXPECTED to
# "FAILED" in their Makefile. Values other than SUCCESSFUL
# or FAILED will cause a CI error.
EXPECTED ?= SUCCESSFUL
define yaml_encode_options
"$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')"
endef
CI_FLAGS = $(CBMCFLAGS) $(CHECKFLAGS) $(COVERFLAGS)
cbmc-batch.yaml:
@$(RM) $@
@echo 'build_memory: $(JOB_MEMORY)' > $@
@echo 'cbmcflags: $(strip $(call yaml_encode_options,$(CI_FLAGS)))' >> $@
@echo 'coverage_memory: $(JOB_MEMORY)' >> $@
@echo 'expected: $(EXPECTED)' >> $@
@echo 'goto: $(HARNESS_GOTO).goto' >> $@
@echo 'jobos: $(JOB_OS)' >> $@
@echo 'property_memory: $(JOB_MEMORY)' >> $@
@echo 'report_memory: $(JOB_MEMORY)' >> $@
.PHONY: cbmc-batch.yaml
################################################################
# Run "make echo-proof-uid" to print the proof ID of a proof. This can be
# used by scripts to ensure that every proof has an ID, that there are
# no duplicates, etc.
.PHONY: echo-proof-uid
echo-proof-uid:
@echo $(PROOF_UID)
.PHONY: echo-project-name
echo-project-name:
@echo $(PROJECT_NAME)
################################################################
# Project-specific targets requiring values defined above
sinclude $(PROOF_ROOT)/Makefile-project-targets
# CI-specific targets to drive cbmc in CI
sinclude $(PROOF_ROOT)/Makefile-project-testing
################################################################

27
arcs-sdk/modules/coresntp/test/cbmc/proofs/README.md Normal file
View File

@@ -0,0 +1,27 @@
CBMC proofs
===========
This directory contains the CBMC proofs. Each proof is in its own
directory.
This directory includes four Makefiles.
One Makefile describes the basic workflow for building and running proofs:
* Makefile.common:
* make: builds the goto binary, does the cbmc property checking
and coverage checking, and builds the final report.
* make goto: builds the goto binary
* make result: does cbmc property checking
* make coverage: does cbmc coverage checking
* make report: builds the final report
Three included Makefiles describe project-specific settings and can override
definitions in Makefile.common:
* Makefile-project-defines: definitions like compiler flags
required to build the goto binaries, and definitions to override
definitions in Makefile.common.
* Makefile-project-targets: other make targets needed for the project
* Makefile-project-testing: other definitions and targets needed for
unit testing or continuous integration.

24
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_CalculatePollInterval/Makefile Normal file
View File

@@ -0,0 +1,24 @@
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
HARNESS_ENTRY = harness
HARNESS_FILE = Sntp_CalculatePollInterval_harness
# This should be a unique identifier for this proof, and will appear on the
# Litani dashboard. It can be human-readable and contain spaces if you wish.
PROOF_UID = Sntp_CalculatePollInterval
# Bound for loop unwinding for loop in Sntp_CalculatePollInterval function. Unwinding
# the loop 33 times will be enough as the unsigned 32 integer can take value upto 2^32.
MAX_BOUND_FOR_LOOP=33
DEFINES +=
INCLUDES +=
REMOVE_FUNCTION_BODY +=
UNWINDSET += Sntp_CalculatePollInterval.0:$(MAX_BOUND_FOR_LOOP)
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/source/core_sntp_serializer.c
include ../Makefile.common

23
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_CalculatePollInterval/README.md Normal file
View File

@@ -0,0 +1,23 @@
Sntp_CalculatePollInterval proof
==============
This directory contains a memory safety proof for Sntp_CalculatePollInterval.
The proof runs within 3 minutes on a t2.2xlarge. It provides complete coverage of:
* Sntp_CalculatePollInterval()
To run the proof.
-------------
* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
to your path.
* Run `make`.
* Open html/index.html in a web browser.
To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles.
-------------
* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof.
* Use Makefile.arpa as the starting point for your proof Makefile by:
1. Modifying Makefile.arpa (if required).
2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`).

43
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_CalculatePollInterval/Sntp_CalculatePollInterval_harness.c Normal file
View File

@@ -0,0 +1,43 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/**
* @file Sntp_CalculatePollInterval_harness.c
* @brief Implements the proof harness for Sntp_CalculatePollInterval function.
*/
#include "core_sntp_serializer.h"
void harness()
{
uint16_t clockFreqTolerance;
uint16_t desiredAccuracy;
uint32_t * pPollInterval;
SntpStatus_t sntpStatus;
pPollInterval = malloc( sizeof( uint32_t ) );
sntpStatus = Sntp_CalculatePollInterval( clockFreqTolerance, desiredAccuracy, pPollInterval );
__CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpSuccess || sntpStatus == SntpZeroPollInterval ), "The return value is not a valid SNTP status." );
}

1
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_CalculatePollInterval/cbmc-proof.txt Normal file
View File

@@ -0,0 +1 @@
# This file marks this directory as containing a CBMC proof.

7
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_CalculatePollInterval/cbmc-viewer.json Normal file
View File

@@ -0,0 +1,7 @@
{ "expected-missing-functions":
[
],
"proof-name": "Sntp_CalculatePollInterval",
"proof-root": "test/cbmc/proofs"
}

20
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_ConvertToUnixTime/Makefile Normal file
View File

@@ -0,0 +1,20 @@
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
HARNESS_ENTRY = harness
HARNESS_FILE = Sntp_ConvertToUnixTime_harness
# This should be a unique identifier for this proof, and will appear on the
# Litani dashboard. It can be human-readable and contain spaces if you wish.
PROOF_UID = Sntp_ConvertToUnixTime
DEFINES +=
INCLUDES +=
REMOVE_FUNCTION_BODY +=
UNWINDSET +=
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/source/core_sntp_serializer.c
include ../Makefile.common

23
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_ConvertToUnixTime/README.md Normal file
View File

@@ -0,0 +1,23 @@
Sntp_ConvertToUnixTime proof
==============
This directory contains a memory safety proof for Sntp_ConvertToUnixTime.
The proof runs within 3 minutes on a t2.2xlarge. It provides complete coverage of:
* Sntp_ConvertToUnixTime()
To run the proof.
-------------
* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
to your path.
* Run `make`.
* Open html/index.html in a web browser.
To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles.
-------------
* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof.
* Use Makefile.arpa as the starting point for your proof Makefile by:
1. Modifying Makefile.arpa (if required).
2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`).

46
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_ConvertToUnixTime/Sntp_ConvertToUnixTime_harness.c Normal file
View File

@@ -0,0 +1,46 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/**
* @file Sntp_ConvertToUnixTime_harness.c
* @brief Implements the proof harness for Sntp_ConvertToUnixTime function.
*/
#include "core_sntp_serializer.h"
void harness()
{
SntpTimestamp_t * pSntpTime;
uint32_t * pUnixTimeSecs;
uint32_t * pUnixTimeMicrosecs;
SntpStatus_t sntpStatus;
pSntpTime = malloc( sizeof( SntpTimestamp_t ) );
pUnixTimeSecs = malloc( sizeof( uint32_t ) );
pUnixTimeMicrosecs = malloc( sizeof( uint32_t ) );
sntpStatus = Sntp_ConvertToUnixTime( pSntpTime, pUnixTimeSecs, pUnixTimeMicrosecs );
__CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpErrorTimeNotSupported || sntpStatus == SntpSuccess ), "The return value is not a valid SNTP Status" );
}

1
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_ConvertToUnixTime/cbmc-proof.txt Normal file
View File

@@ -0,0 +1 @@
# This file marks this directory as containing a CBMC proof.

7
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_ConvertToUnixTime/cbmc-viewer.json Normal file
View File

@@ -0,0 +1,7 @@
{ "expected-missing-functions":
[
],
"proof-name": "Sntp_ConvertToUnixTime",
"proof-root": "test/cbmc/proofs"
}

20
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_DeserializeResponse/Makefile Normal file
View File

@@ -0,0 +1,20 @@
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
HARNESS_ENTRY = harness
HARNESS_FILE = Sntp_DeserializeResponse_harness
# This should be a unique identifier for this proof, and will appear on the
# Litani dashboard. It can be human-readable and contain spaces if you wish.
PROOF_UID = Sntp_DeserializeResponse
DEFINES +=
INCLUDES +=
REMOVE_FUNCTION_BODY +=
UNWINDSET +=
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/source/core_sntp_serializer.c
include ../Makefile.common

20
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_DeserializeResponse/README.md Normal file
View File

@@ -0,0 +1,20 @@
Sntp_DeserializeResponse proof
==============
This directory contains a memory safety proof for Sntp_DeserializeResponse.
To run the proof.
-------------
* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
to your path.
* Run `make`.
* Open html/index.html in a web browser.
To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles.
-------------
* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof.
* Use Makefile.arpa as the starting point for your proof Makefile by:
1. Modifying Makefile.arpa (if required).
2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`).

54
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_DeserializeResponse/Sntp_DeserializeResponse_harness.c Normal file
View File

@@ -0,0 +1,54 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/**
* @file Sntp_DeserializeResponse_harness.c
* @brief Implements the proof harness for Sntp_DeserializeResponse function.
*/
#include <stdint.h>
#include "core_sntp_serializer.h"
void harness()
{
SntpTimestamp_t * pRequestTime;
SntpTimestamp_t * pResponseRxTime;
void * pResponseBuffer;
size_t bufferSize;
SntpResponseData_t * pParsedResponse;
SntpStatus_t sntpStatus;
__CPROVER_assume( bufferSize < CBMC_MAX_OBJECT_SIZE );
pRequestTime = malloc( sizeof( SntpTimestamp_t ) );
pResponseRxTime = malloc( sizeof( SntpTimestamp_t ) );
pResponseBuffer = malloc( bufferSize );
pParsedResponse = malloc( sizeof( SntpResponseData_t ) );
sntpStatus = Sntp_DeserializeResponse( pRequestTime, pResponseRxTime, pResponseBuffer, bufferSize, pParsedResponse );
__CPROVER_assert( ( sntpStatus == SntpErrorBadParameter ) || ( sntpStatus == SntpErrorBufferTooSmall ) ||
( sntpStatus == SntpInvalidResponse ) || ( sntpStatus == SntpSuccess ) || ( sntpStatus == SntpRejectedResponseChangeServer ) ||
( sntpStatus == SntpRejectedResponseRetryWithBackoff ) || ( sntpStatus == SntpRejectedResponseOtherCode ), "This is a valid sntp return status" );
}

1
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-proof.txt Normal file
View File

@@ -0,0 +1 @@
# This file marks this directory as containing a CBMC proof.

7
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_DeserializeResponse/cbmc-viewer.json Normal file
View File

@@ -0,0 +1,7 @@
{ "expected-missing-functions":
[
],
"proof-name": "Sntp_DeserializeResponse",
"proof-root": "test/cbmc/proofs"
}

20
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_Init/Makefile Normal file
View File

@@ -0,0 +1,20 @@
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
HARNESS_ENTRY = harness
HARNESS_FILE = Sntp_Init_harness
# This should be a unique identifier for this proof, and will appear on the
# Litani dashboard. It can be human-readable and contain spaces if you wish.
PROOF_UID = Sntp_Init
DEFINES +=
INCLUDES +=
REMOVE_FUNCTION_BODY +=
UNWINDSET +=
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/source/core_sntp_client.c
include ../Makefile.common

15
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_Init/README.md Normal file
View File

@@ -0,0 +1,15 @@
Sntp_Init proof
==============
This directory contains a memory safety proof for Sntp_Init.
The proof runs within 3 minutes on a t2.2xlarge. It provides complete coverage of:
* Sntp_Init()
To run the proof.
-------------
* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
to your path.
* Run `make`.
* Open html/index.html in a web browser.

62
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_Init/Sntp_Init_harness.c Normal file
View File

@@ -0,0 +1,62 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/**
* @file Sntp_Init_harness.c
* @brief Implements the proof harness for Sntp_Init function.
*/
#include <stddef.h>
#include "core_sntp_client.h"
void harness()
{
SntpContext_t * pContext;
SntpServerInfo_t * pTimeServers;
size_t numOfServers;
uint32_t serverResponseTimeoutMs;
uint8_t * pNetworkBuffer;
size_t bufferSize;
SntpResolveDns_t resolveDnsFunc;
SntpGetTime_t getSystemTimeFunc;
SntpSetTime_t setSystemTimeFunc;
UdpTransportInterface_t * pTransportIntf;
SntpAuthenticationInterface_t * pAuthIntf;
SntpStatus_t sntpStatus;
pContext = malloc( sizeof( SntpContext_t ) );
pTimeServers = malloc( sizeof( SntpServerInfo_t ) );
__CPROVER_assume( bufferSize < CBMC_MAX_OBJECT_SIZE );
pNetworkBuffer = malloc( bufferSize );
pTransportIntf = malloc( sizeof( UdpTransportInterface_t ) );
pAuthIntf = malloc( sizeof( SntpAuthenticationInterface_t ) );
sntpStatus = Sntp_Init( pContext, pTimeServers, numOfServers, serverResponseTimeoutMs, pNetworkBuffer,
bufferSize, resolveDnsFunc, getSystemTimeFunc, setSystemTimeFunc,
pTransportIntf, pAuthIntf );
__CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpSuccess || sntpStatus == SntpErrorBufferTooSmall ), "The return value is not a valid SNTP Status" );
}

1
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_Init/cbmc-proof.txt Normal file
View File

@@ -0,0 +1 @@
# This file marks this directory as containing a CBMC proof.

7
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_Init/cbmc-viewer.json Normal file
View File

@@ -0,0 +1,7 @@
{ "expected-missing-functions":
[
],
"proof-name": "Sntp_Init",
"proof-root": "test/cbmc/proofs"
}

43
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_ReceiveTimeResponse/Makefile Normal file
View File

@@ -0,0 +1,43 @@
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
HARNESS_ENTRY = harness
HARNESS_FILE = Sntp_ReceiveTimeResponse_harness
# Please see test/cbmc/stubs/core_sntp_stubs.c for
# more information on MAX_NETWORK_RECV_TRIES.
MAX_NETWORK_RECV_TRIES=5
# Bound on the timeout in Sntp_ReceiveTimeResponse. This timeout is bounded because
# memory saftey can be proven in a only a single iteration.
# Each iteration will try to receive a single packet in its entirey. With a time
# out of 1 we can get coverage of the entire function. Another iteration will
# performed unnecessarily duplicating of the proof.
SNTP_RECEIVE_TIMEOUT=1
# Maximum number of sntp time servers
MAX_NO_OF_SERVERS=5
# Maximum number of attempts in outer loop of Sntp_ReceiveTimeResponse needed to receive a response from server.
MAX_ITERATIONS_RECEIVE_RESPONSE=1
# This should be a unique identifier for this proof, and will appear on the
# Litani dashboard. It can be human-readable and contain spaces if you wish.
PROOF_UID = Sntp_ReceiveTimeResponse
DEFINES +=-DMAX_NO_OF_SERVERS=$(MAX_NO_OF_SERVERS)
DEFINES +=-DSNTP_RECEIVE_TIMEOUT=$(SNTP_RECEIVE_TIMEOUT)
INCLUDES +=
REMOVE_FUNCTION_BODY +=Sntp_DeserializeResponse
UNWINDSET +=__CPROVER_file_local_core_sntp_client_c_receiveSntpResponse.0:$(shell expr $(MAX_NETWORK_RECV_TRIES) + 1 )
UNWINDSET +=__CPROVER_file_local_core_sntp_client_c_Sntp_ReceiveTimeResponse.0:$(shell expr $(MAX_ITERATIONS_RECEIVE_RESPONSE) + 1 )
UNWINDSET +=unconstrainedCoreSntpContext.0:$(shell expr $(MAX_NO_OF_SERVERS) + 1 )
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/core_sntp_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_sntp_stubs.c
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/source/core_sntp_client.c
include ../Makefile.common

20
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_ReceiveTimeResponse/README.md Normal file
View File

@@ -0,0 +1,20 @@
Sntp_ReceiveTimeResponse proof
==============
This directory contains a memory safety proof for Sntp_ReceiveTimeResponse.
To run the proof.
-------------
* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
to your path.
* Run `make`.
* Open html/index.html in a web browser.
To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles.
-------------
* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof.
* Use Makefile.arpa as the starting point for your proof Makefile by:
1. Modifying Makefile.arpa (if required).
2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`).

62
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_ReceiveTimeResponse/Sntp_ReceiveTimeResponse_harness.c Normal file
View File

@@ -0,0 +1,62 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/**
* @file Sntp_ReceiveTimeResponse_harness.c
* @brief Implements the proof harness for Sntp_ReceiveTimeResponse function.
*/
#include <stddef.h>
#include "core_sntp_cbmc_state.h"
#include "core_sntp_stubs.h"
#include "core_sntp_client.h"
void harness()
{
SntpContext_t * pContext;
uint32_t blockTimeMs;
SntpStatus_t sntpStatus;
pContext = unconstrainedCoreSntpContext();
if( pContext != NULL )
{
/* Setting the initial value of request time to check for response timeout
* while reading data from network. */
GetTimeFuncStub( &pContext->lastRequestTime );
}
/* The SNTP_RECEIVE_TIMEOUT is used here to control the number of loops
* when receiving on the network. The default is used here because memory
* safety can be proven in only a few iterations. Please see this proof's
* Makefile for more information. */
__CPROVER_assume( blockTimeMs < SNTP_RECEIVE_TIMEOUT );
sntpStatus = Sntp_ReceiveTimeResponse( pContext, blockTimeMs );
__CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpSuccess ||
sntpStatus == SntpNoResponseReceived || sntpStatus == SntpRejectedResponse ||
sntpStatus == SntpErrorResponseTimeout || sntpStatus == SntpErrorNetworkFailure ),
"The return value is not a valid coreSNTP Status" );
}

1
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_ReceiveTimeResponse/cbmc-proof.txt Normal file
View File

@@ -0,0 +1 @@
# This file marks this directory as containing a CBMC proof.

7
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_ReceiveTimeResponse/cbmc-viewer.json Normal file
View File

@@ -0,0 +1,7 @@
{ "expected-missing-functions":
[
],
"proof-name": "Sntp_ReceiveTimeResponse",
"proof-root": "test/cbmc/proofs"
}

40
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_SendTimeRequest/Makefile Normal file
View File

@@ -0,0 +1,40 @@
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
HARNESS_ENTRY = harness
HARNESS_FILE = Sntp_SendTimeRequest_harness
# Please see test/cbmc/stubs/core_sntp_stubs.c for
# more information on MAX_NETWORK_SEND_TRIES.
MAX_NETWORK_SEND_TRIES=3
# Bound on the timeout in Sntp_ReceiveTimeResponse. This timeout is bounded because
# memory saftey can be proven in a only a single iteration.
# Each iteration will try to receive a single packet in its entirey. With a time
# out of 1 we can get coverage of the entire function. Another iteration will
# performed unnecessarily duplicating of the proof.
SNTP_SEND_TIMEOUT=1
# Maximum number of sntp time servers
MAX_NO_OF_SERVERS=5
# This should be a unique identifier for this proof, and will appear on the
# Litani dashboard. It can be human-readable and contain spaces if you wish.
PROOF_UID = Sntp_SendTimeRequest
DEFINES +=-DMAX_NO_OF_SERVERS=$(MAX_NO_OF_SERVERS)
DEFINES +=-DSNTP_SEND_TIMEOUT=$(SNTP_SEND_TIMEOUT)
INCLUDES +=
# Providing a stub for this function as we have already have a separate proof
# for this function
REMOVE_FUNCTION_BODY +=Sntp_SerializeRequest
UNWINDSET +=__CPROVER_file_local_core_sntp_client_c_sendSntpPacket.0:$(MAX_NETWORK_SEND_TRIES)
UNWINDSET +=unconstrainedCoreSntpContext.0:$(shell expr $(MAX_NO_OF_SERVERS) + 1 )
PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/core_sntp_cbmc_state.c
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_sntp_stubs.c
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/source/core_sntp_client.c
include ../Makefile.common

19
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_SendTimeRequest/README.md Normal file
View File

@@ -0,0 +1,19 @@
Sntp_SendTimeRequest proof
==============
This directory contains a memory safety proof for Sntp_SendTimeRequest.
To run the proof.
-------------
* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
to your path.
* Run `make`.
* Open html/index.html in a web browser.
-------------
* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof.
* Use Makefile.arpa as the starting point for your proof Makefile by:
1. Modifying Makefile.arpa (if required).
2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`).

56
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_SendTimeRequest/Sntp_SendTimeRequest_harness.c Normal file
View File

@@ -0,0 +1,56 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/**
* @file Sntp_SendTimeRequest_harness.c
* @brief Implements the proof harness for Sntp_SendTimeRequest function.
*/
#include <stddef.h>
#include "core_sntp_client.h"
#include "core_sntp_cbmc_state.h"
void harness()
{
SntpContext_t * pContext;
uint32_t randomNumber;
SntpStatus_t sntpStatus;
uint32_t blockTimeMs;
pContext = unconstrainedCoreSntpContext();
/* The SNTP_SEND_TIMEOUT is used here to control the number of loops
* when sending data on the network. The default is used here because memory
* safety can be proven in only a few iterations. Please see this proof's
* Makefile for more information. */
__CPROVER_assume( blockTimeMs < SNTP_SEND_TIMEOUT );
sntpStatus = Sntp_SendTimeRequest( pContext, randomNumber, blockTimeMs );
__CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpSuccess ||
sntpStatus == SntpErrorContextNotInitialized || sntpStatus == SntpErrorSendTimeout ||
sntpStatus == SntpErrorBufferTooSmall || sntpStatus == SntpErrorDnsFailure ||
sntpStatus == SntpErrorAuthFailure || sntpStatus == SntpErrorNetworkFailure ),
"The return value is not a valid coreSNTP Status" );
}

1
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_SendTimeRequest/cbmc-proof.txt Normal file
View File

@@ -0,0 +1 @@
# This file marks this directory as containing a CBMC proof.

7
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_SendTimeRequest/cbmc-viewer.json Normal file
View File

@@ -0,0 +1,7 @@
{ "expected-missing-functions":
[
],
"proof-name": "Sntp_SendTimeRequest",
"proof-root": "test/cbmc/proofs"
}

20
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_SerializeRequest/Makefile Normal file
View File

@@ -0,0 +1,20 @@
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
HARNESS_ENTRY = harness
HARNESS_FILE = Sntp_SerializeRequest_harness
# This should be a unique identifier for this proof, and will appear on the
# Litani dashboard. It can be human-readable and contain spaces if you wish.
PROOF_UID = Sntp_SerializeRequest
DEFINES +=
INCLUDES +=
REMOVE_FUNCTION_BODY +=
UNWINDSET +=
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/source/core_sntp_serializer.c
include ../Makefile.common

23
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_SerializeRequest/README.md Normal file
View File

@@ -0,0 +1,23 @@
Sntp_SerializeRequest proof
==============
This directory contains a memory safety proof for Sntp_SerializeRequest.
The proof runs within 3 minutes on a t2.2xlarge. It provides complete coverage of:
* Sntp_SerializeRequest()
To run the proof.
-------------
* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
to your path.
* Run `make`.
* Open html/index.html in a web browser.
To use [`arpa`](https://awslabs.github.io/aws-proof-build-assistant) to simplify writing Makefiles.
-------------
* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof.
* Use Makefile.arpa as the starting point for your proof Makefile by:
1. Modifying Makefile.arpa (if required).
2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`).

50
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_SerializeRequest/Sntp_SerializeRequest_harness.c Normal file
View File

@@ -0,0 +1,50 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/**
* @file Sntp_SerializeRequest_harness.c
* @brief Implements the proof harness for Sntp_SerializeRequest function.
*/
#include <stdint.h>
#include "core_sntp_serializer.h"
void harness()
{
SntpTimestamp_t * pRequestTime;
uint32_t randomNumber;
void * pBuffer;
size_t bufferSize;
SntpStatus_t sntpStatus;
pRequestTime = malloc( sizeof( SntpTimestamp_t ) );
__CPROVER_assume( bufferSize < CBMC_MAX_OBJECT_SIZE );
pBuffer = malloc( bufferSize );
sntpStatus = Sntp_SerializeRequest( pRequestTime, randomNumber, pBuffer, bufferSize );
__CPROVER_assert( ( sntpStatus == SntpErrorBadParameter || sntpStatus == SntpErrorBufferTooSmall || sntpStatus == SntpSuccess ), "The return value is not a valid SNTP Status" );
}

1
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_SerializeRequest/cbmc-proof.txt Normal file
View File

@@ -0,0 +1 @@
# This file marks this directory as containing a CBMC proof.

7
arcs-sdk/modules/coresntp/test/cbmc/proofs/Sntp_SerializeRequest/cbmc-viewer.json Normal file
View File

@@ -0,0 +1,7 @@
{ "expected-missing-functions":
[
],
"proof-name": "Sntp_SerializeRequest",
"proof-root": "test/cbmc/proofs"
}

0
arcs-sdk/modules/coresntp/test/cbmc/proofs/lib/__init__.py Normal file
View File

74
arcs-sdk/modules/coresntp/test/cbmc/proofs/lib/print_tool_versions.py Executable file
View File

@@ -0,0 +1,74 @@
#!/usr/bin/env python3
#
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
import logging
import pathlib
import shutil
import subprocess
_TOOLS = [
"cadical",
"cbmc",
"cbmc-viewer",
"cbmc-starter-kit-update",
"kissat",
"litani",
]
def _format_versions(table):
lines = [
"<table>",
'<tr><td colspan="2" style="font-weight: bold">Tool Versions</td></tr>',
]
for tool, version in table.items():
if version:
v_str = f'<code><pre style="margin: 0">{version}</pre></code>'
else:
v_str = '<em>not found</em>'
lines.append(
f'<tr><td style="font-weight: bold; padding-right: 1em; '
f'text-align: right;">{tool}:</td>'
f'<td>{v_str}</td></tr>')
lines.append("</table>")
return "\n".join(lines)
def _get_tool_versions():
ret = {}
for tool in _TOOLS:
err = f"Could not determine version of {tool}: "
ret[tool] = None
if not shutil.which(tool):
logging.error("%s'%s' not found on $PATH", err, tool)
continue
cmd = [tool, "--version"]
proc = subprocess.Popen(cmd, text=True, stdout=subprocess.PIPE)
try:
out, _ = proc.communicate(timeout=10)
except subprocess.TimeoutExpired:
logging.error("%s'%s --version' timed out", err, tool)
continue
if proc.returncode:
logging.error(
"%s'%s --version' returned %s", err, tool, str(proc.returncode))
continue
ret[tool] = out.strip()
return ret
def main():
exe_name = pathlib.Path(__file__).name
logging.basicConfig(format=f"{exe_name}: %(message)s")
table = _get_tool_versions()
out = _format_versions(table)
print(out)
if __name__ == "__main__":
main()

143
arcs-sdk/modules/coresntp/test/cbmc/proofs/lib/summarize.py Normal file
View File

@@ -0,0 +1,143 @@
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
import argparse
import json
import logging
import os
import sys
DESCRIPTION = """Print 2 tables in GitHub-flavored Markdown that summarize
an execution of CBMC proofs."""
def get_args():
"""Parse arguments for summarize script."""
parser = argparse.ArgumentParser(description=DESCRIPTION)
for arg in [{
"flags": ["--run-file"],
"help": "path to the Litani run.json file",
"required": True,
}]:
flags = arg.pop("flags")
parser.add_argument(*flags, **arg)
return parser.parse_args()
def _get_max_length_per_column_list(data):
ret = [len(item) + 1 for item in data[0]]
for row in data[1:]:
for idx, item in enumerate(row):
ret[idx] = max(ret[idx], len(item) + 1)
return ret
def _get_table_header_separator(max_length_per_column_list):
line_sep = ""
for max_length_of_word_in_col in max_length_per_column_list:
line_sep += "|" + "-" * (max_length_of_word_in_col + 1)
line_sep += "|\n"
return line_sep
def _get_entries(max_length_per_column_list, row_data):
entries = []
for row in row_data:
entry = ""
for idx, word in enumerate(row):
max_length_of_word_in_col = max_length_per_column_list[idx]
space_formatted_word = (max_length_of_word_in_col - len(word)) * " "
entry += "| " + word + space_formatted_word
entry += "|\n"
entries.append(entry)
return entries
def _get_rendered_table(data):
table = []
max_length_per_column_list = _get_max_length_per_column_list(data)
entries = _get_entries(max_length_per_column_list, data)
for idx, entry in enumerate(entries):
if idx == 1:
line_sep = _get_table_header_separator(max_length_per_column_list)
table.append(line_sep)
table.append(entry)
table.append("\n")
return "".join(table)
def _get_status_and_proof_summaries(run_dict):
"""Parse a dict representing a Litani run and create lists summarizing the
proof results.
Parameters
----------
run_dict
A dictionary representing a Litani run.
Returns
-------
A list of 2 lists.
The first sub-list maps a status to the number of proofs with that status.
The second sub-list maps each proof to its status.
"""
count_statuses = {}
proofs = [["Proof", "Status"]]
for proof_pipeline in run_dict["pipelines"]:
status_pretty_name = proof_pipeline["status"].title().replace("_", " ")
try:
count_statuses[status_pretty_name] += 1
except KeyError:
count_statuses[status_pretty_name] = 1
if proof_pipeline["name"] == "print_tool_versions":
continue
proofs.append([proof_pipeline["name"], status_pretty_name])
statuses = [["Status", "Count"]]
for status, count in count_statuses.items():
statuses.append([status, str(count)])
return [statuses, proofs]
def print_proof_results(out_file):
"""
Print 2 strings that summarize the proof results.
When printing, each string will render as a GitHub flavored Markdown table.
"""
output = "## Summary of CBMC proof results\n\n"
with open(out_file, encoding='utf-8') as run_json:
run_dict = json.load(run_json)
status_table, proof_table = _get_status_and_proof_summaries(run_dict)
for summary in (status_table, proof_table):
output += _get_rendered_table(summary)
print(output)
sys.stdout.flush()
github_summary_file = os.getenv("GITHUB_STEP_SUMMARY")
if github_summary_file:
with open(github_summary_file, "a") as handle:
print(output, file=handle)
handle.flush()
else:
logging.warning(
"$GITHUB_STEP_SUMMARY not set, not writing summary file")
msg = (
"Click the 'Summary' button to view a Markdown table "
"summarizing all proof results")
if run_dict["status"] != "success":
logging.error("Not all proofs passed.")
logging.error(msg)
sys.exit(1)
logging.info(msg)
if __name__ == '__main__':
args = get_args()
logging.basicConfig(format="%(levelname)s: %(message)s")
try:
print_proof_results(args.run_file)
except Exception as ex: # pylint: disable=broad-except
logging.critical("Could not print results. Exception: %s", str(ex))

414
arcs-sdk/modules/coresntp/test/cbmc/proofs/run-cbmc-proofs.py Executable file
View File

@@ -0,0 +1,414 @@
#!/usr/bin/env python3
#
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0
import argparse
import asyncio
import json
import logging
import math
import os
import pathlib
import re
import subprocess
import sys
import tempfile
from lib.summarize import print_proof_results
DESCRIPTION = "Configure and run all CBMC proofs in parallel"
# Keep the epilog hard-wrapped at 70 characters, as it gets printed
# verbatim in the terminal. 70 characters stops here --------------> |
EPILOG = """
This tool automates the process of running `make report` in each of
the CBMC proof directories. The tool calculates the dependency graph
of all tasks needed to build, run, and report on all the proofs, and
executes these tasks in parallel.
The tool is roughly equivalent to doing this:
litani init --project "my-cool-project";
find . -name cbmc-proof.txt | while read -r proof; do
pushd $(dirname ${proof});
# The `make _report` rule adds a single proof to litani
# without running it
make _report;
popd;
done
litani run-build;
except that it is much faster and provides some convenience options.
The CBMC CI runs this script with no arguments to build and run all
proofs in parallel. The value of "my-cool-project" is taken from the
PROJECT_NAME variable in Makefile-project-defines.
The --no-standalone argument omits the `litani init` and `litani
run-build`; use it when you want to add additional proof jobs, not
just the CBMC ones. In that case, you would run `litani init`
yourself; then run `run-cbmc-proofs --no-standalone`; add any
additional jobs that you want to execute with `litani add-job`; and
finally run `litani run-build`.
The litani dashboard will be written under the `output` directory; the
cbmc-viewer reports remain in the `$PROOF_DIR/report` directory. The
HTML dashboard from the latest Litani run will always be symlinked to
`output/latest/html/index.html`, so you can keep that page open in
your browser and reload the page whenever you re-run this script.
"""
# 70 characters stops here ----------------------------------------> |
def get_project_name():
cmd = [
"make",
"--no-print-directory",
"-f", "Makefile.common",
"echo-project-name",
]
logging.debug(" ".join(cmd))
proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE, check=False)
if proc.returncode:
logging.critical("could not run make to determine project name")
sys.exit(1)
if not proc.stdout.strip():
logging.warning(
"project name has not been set; using generic name instead. "
"Set the PROJECT_NAME value in Makefile-project-defines to "
"remove this warning")
return "<PROJECT NAME HERE>"
return proc.stdout.strip()
def get_args():
pars = argparse.ArgumentParser(
description=DESCRIPTION, epilog=EPILOG,
formatter_class=argparse.RawDescriptionHelpFormatter)
for arg in [{
"flags": ["-j", "--parallel-jobs"],
"type": int,
"metavar": "N",
"help": "run at most N proof jobs in parallel",
}, {
"flags": ["--fail-on-proof-failure"],
"action": "store_true",
"help": "exit with return code `10' if any proof failed"
" (default: exit 0)",
}, {
"flags": ["--no-standalone"],
"action": "store_true",
"help": "only configure proofs: do not initialize nor run",
}, {
"flags": ["-p", "--proofs"],
"nargs": "+",
"metavar": "DIR",
"help": "only run proof in directory DIR (can pass more than one)",
}, {
"flags": ["--project-name"],
"metavar": "NAME",
"default": get_project_name(),
"help": "project name for report. Default: %(default)s",
}, {
"flags": ["--marker-file"],
"metavar": "FILE",
"default": "cbmc-proof.txt",
"help": (
"name of file that marks proof directories. Default: "
"%(default)s"),
}, {
"flags": ["--no-memory-profile"],
"action": "store_true",
"help": "disable memory profiling, even if Litani supports it"
}, {
"flags": ["--no-expensive-limit"],
"action": "store_true",
"help": "do not limit parallelism of 'EXPENSIVE' jobs",
}, {
"flags": ["--expensive-jobs-parallelism"],
"metavar": "N",
"default": 1,
"type": int,
"help": (
"how many proof jobs marked 'EXPENSIVE' to run in parallel. "
"Default: %(default)s"),
}, {
"flags": ["--verbose"],
"action": "store_true",
"help": "verbose output",
}, {
"flags": ["--debug"],
"action": "store_true",
"help": "debug output",
}, {
"flags": ["--summarize"],
"action": "store_true",
"help": "summarize proof results with two tables on stdout",
}, {
"flags": ["--version"],
"action": "version",
"version": "CBMC starter kit 2.5",
"help": "display version and exit"
}]:
flags = arg.pop("flags")
pars.add_argument(*flags, **arg)
return pars.parse_args()
def set_up_logging(verbose):
if verbose:
level = logging.DEBUG
else:
level = logging.WARNING
logging.basicConfig(
format="run-cbmc-proofs: %(message)s", level=level)
def task_pool_size():
ret = os.cpu_count()
if ret is None or ret < 3:
return 1
return ret - 2
def print_counter(counter):
# pylint: disable=consider-using-f-string
print("\rConfiguring CBMC proofs: "
"{complete:{width}} / {total:{width}}".format(**counter), end="", file=sys.stderr)
def get_proof_dirs(proof_root, proof_list, marker_file):
if proof_list is not None:
proofs_remaining = list(proof_list)
else:
proofs_remaining = []
for root, _, fyles in os.walk(proof_root):
proof_name = str(pathlib.Path(root).name)
if root != str(proof_root) and ".litani_cache_dir" in fyles:
pathlib.Path(f"{root}/.litani_cache_dir").unlink()
if proof_list and proof_name not in proof_list:
continue
if proof_list and proof_name in proofs_remaining:
proofs_remaining.remove(proof_name)
if marker_file in fyles:
yield root
if proofs_remaining:
logging.critical(
"The following proofs were not found: %s",
", ".join(proofs_remaining))
sys.exit(1)
def run_build(litani, jobs, fail_on_proof_failure, summarize):
cmd = [str(litani), "run-build"]
if jobs:
cmd.extend(["-j", str(jobs)])
if fail_on_proof_failure:
cmd.append("--fail-on-pipeline-failure")
if summarize:
out_file = pathlib.Path(tempfile.gettempdir(), "run.json").resolve()
cmd.extend(["--out-file", str(out_file)])
logging.debug(" ".join(cmd))
proc = subprocess.run(cmd, check=False)
if proc.returncode and not fail_on_proof_failure:
logging.critical("Failed to run litani run-build")
sys.exit(1)
if summarize:
print_proof_results(out_file)
out_file.unlink()
if proc.returncode:
logging.error("One or more proofs failed")
sys.exit(10)
def get_litani_path(proof_root):
cmd = [
"make",
"--no-print-directory",
f"PROOF_ROOT={proof_root}",
"-f", "Makefile.common",
"litani-path",
]
logging.debug(" ".join(cmd))
proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE, check=False)
if proc.returncode:
logging.critical("Could not determine path to litani")
sys.exit(1)
return proc.stdout.strip()
def get_litani_capabilities(litani_path):
cmd = [litani_path, "print-capabilities"]
proc = subprocess.run(
cmd, text=True, stdout=subprocess.PIPE, stderr=subprocess.DEVNULL, check=False)
if proc.returncode:
return []
try:
return json.loads(proc.stdout)
except RuntimeError:
logging.warning("Could not load litani capabilities: '%s'", proc.stdout)
return []
def check_uid_uniqueness(proof_dir, proof_uids):
with (pathlib.Path(proof_dir) / "Makefile").open() as handle:
for line in handle:
match = re.match(r"^PROOF_UID\s*=\s*(?P<uid>\w+)", line)
if not match:
continue
if match["uid"] not in proof_uids:
proof_uids[match["uid"]] = proof_dir
return
logging.critical(
"The Makefile in directory '%s' should have a different "
"PROOF_UID than the Makefile in directory '%s'",
proof_dir, proof_uids[match["uid"]])
sys.exit(1)
logging.critical(
"The Makefile in directory '%s' should contain a line like", proof_dir)
logging.critical("PROOF_UID = ...")
logging.critical("with a unique identifier for the proof.")
sys.exit(1)
def should_enable_memory_profiling(litani_caps, args):
if args.no_memory_profile:
return False
return "memory_profile" in litani_caps
def should_enable_pools(litani_caps, args):
if args.no_expensive_limit:
return False
return "pools" in litani_caps
async def configure_proof_dirs( # pylint: disable=too-many-arguments
queue, counter, proof_uids, enable_pools, enable_memory_profiling, debug):
while True:
print_counter(counter)
path = str(await queue.get())
check_uid_uniqueness(path, proof_uids)
pools = ["ENABLE_POOLS=true"] if enable_pools else []
profiling = [
"ENABLE_MEMORY_PROFILING=true"] if enable_memory_profiling else []
# Allow interactive tasks to preempt proof configuration
proc = await asyncio.create_subprocess_exec(
"nice", "-n", "15", "make", *pools,
*profiling, "-B", "_report", "" if debug else "--quiet", cwd=path,
stdout=asyncio.subprocess.PIPE, stderr=asyncio.subprocess.PIPE)
stdout, stderr = await proc.communicate()
logging.debug("returncode: %s", str(proc.returncode))
logging.debug("stdout:")
for line in stdout.decode().splitlines():
logging.debug(line)
logging.debug("stderr:")
for line in stderr.decode().splitlines():
logging.debug(line)
counter["fail" if proc.returncode else "pass"].append(path)
counter["complete"] += 1
print_counter(counter)
queue.task_done()
async def main(): # pylint: disable=too-many-locals
args = get_args()
set_up_logging(args.verbose)
proof_root = pathlib.Path(os.getcwd())
litani = get_litani_path(proof_root)
litani_caps = get_litani_capabilities(litani)
enable_pools = should_enable_pools(litani_caps, args)
init_pools = [
"--pools", f"expensive:{args.expensive_jobs_parallelism}"
] if enable_pools else []
if not args.no_standalone:
cmd = [
str(litani), "init", *init_pools, "--project", args.project_name,
"--no-print-out-dir",
]
if "output_directory_flags" in litani_caps:
out_prefix = proof_root / "output"
out_symlink = out_prefix / "latest"
out_index = out_symlink / "html" / "index.html"
cmd.extend([
"--output-prefix", str(out_prefix),
"--output-symlink", str(out_symlink),
])
print(
"\nFor your convenience, the output of this run will be symbolically linked to ",
out_index, "\n")
logging.debug(" ".join(cmd))
proc = subprocess.run(cmd, check=False)
if proc.returncode:
logging.critical("Failed to run litani init")
sys.exit(1)
proof_dirs = list(get_proof_dirs(
proof_root, args.proofs, args.marker_file))
if not proof_dirs:
logging.critical("No proof directories found")
sys.exit(1)
proof_queue = asyncio.Queue()
for proof_dir in proof_dirs:
proof_queue.put_nowait(proof_dir)
counter = {
"pass": [],
"fail": [],
"complete": 0,
"total": len(proof_dirs),
"width": int(math.log10(len(proof_dirs))) + 1
}
proof_uids = {}
tasks = []
enable_memory_profiling = should_enable_memory_profiling(litani_caps, args)
for _ in range(task_pool_size()):
task = asyncio.create_task(configure_proof_dirs(
proof_queue, counter, proof_uids, enable_pools,
enable_memory_profiling, args.debug))
tasks.append(task)
await proof_queue.join()
print_counter(counter)
print("", file=sys.stderr)
if counter["fail"]:
logging.critical(
"Failed to configure the following proofs:\n%s", "\n".join(
[str(f) for f in counter["fail"]]))
sys.exit(1)
if not args.no_standalone:
run_build(litani, args.parallel_jobs, args.fail_on_proof_failure, args.summarize)
if __name__ == "__main__":
asyncio.run(main())

6
arcs-sdk/modules/coresntp/test/cbmc/sources/README.md Normal file
View File

@@ -0,0 +1,6 @@
CBMC proof source code
======================
This directory contains source code written for CBMC proofs. It is
common to write some code to model aspects of the system under test,
and this code goes here.

113
arcs-sdk/modules/coresntp/test/cbmc/sources/core_sntp_cbmc_state.c Normal file
View File

@@ -0,0 +1,113 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/**
* @file core_sntp_cbmc_state.c
* @brief Implements the functions defined in core_sntp_cbmc_state.h.
*/
#include <stdint.h>
#include <stdlib.h>
#include "core_sntp_client.h"
#include "core_sntp_cbmc_state.h"
#include "core_sntp_stubs.h"
SntpContext_t * unconstrainedCoreSntpContext()
{
SntpServerInfo_t * pTimeServers;
SntpContext_t * pContext;
size_t currentServerIndex;
size_t numOfServers;
uint32_t serverResponseTimeoutMs;
uint8_t * pNetworkBuffer;
size_t bufferSize;
UdpTransportInterface_t * pNetworkIntf;
SntpAuthenticationInterface_t * pAuthIntf;
SntpStatus_t sntpStatus = SntpSuccess;
pContext = malloc( sizeof( SntpContext_t ) );
__CPROVER_assume( numOfServers < MAX_NO_OF_SERVERS );
__CPROVER_assume( serverResponseTimeoutMs < CBMC_MAX_OBJECT_SIZE );
__CPROVER_assume( currentServerIndex < CBMC_MAX_OBJECT_SIZE );
if( numOfServers == 0 )
{
pTimeServers = NULL;
}
else
{
pTimeServers = malloc( numOfServers * sizeof( SntpServerInfo_t ) );
}
if( pTimeServers != NULL )
{
for( size_t i = 0; i < numOfServers; i++ )
{
__CPROVER_assume( pTimeServers[ i ].serverNameLen < CBMC_MAX_OBJECT_SIZE );
__CPROVER_assume( pTimeServers[ i ].port < CBMC_MAX_OBJECT_SIZE );
pTimeServers[ i ].pServerName = malloc( pTimeServers[ i ].serverNameLen );
}
}
__CPROVER_assume( bufferSize < CBMC_MAX_OBJECT_SIZE );
pNetworkBuffer = malloc( bufferSize );
pNetworkIntf = malloc( sizeof( UdpTransportInterface_t ) );
if( pNetworkIntf != NULL )
{
pNetworkIntf->pUserContext = malloc( sizeof( NetworkContext_t ) );
pNetworkIntf->sendTo = NetworkInterfaceSendStub;
pNetworkIntf->recvFrom = NetworkInterfaceReceiveStub;
}
pAuthIntf = malloc( sizeof( SntpAuthenticationInterface_t ) );
if( pAuthIntf != NULL )
{
pAuthIntf->pAuthContext = malloc( sizeof( SntpAuthContext_t ) );
pAuthIntf->generateClientAuth = GenerateClientAuthStub;
pAuthIntf->validateServerAuth = ValidateServerAuthStub;
}
/* It is part of the API contract to call Sntp_Init() with the SntpContext_t
* before any other function in core_sntp_client.h. */
if( pContext != NULL )
{
pContext->currentServerIndex = currentServerIndex;
sntpStatus = Sntp_Init( pContext, pTimeServers, numOfServers, serverResponseTimeoutMs, pNetworkBuffer,
bufferSize, ResolveDnsFuncStub, GetTimeFuncStub, SetTimeFuncStub,
pNetworkIntf, pAuthIntf );
}
/* If the SntpContext_t initialization failed, then set the context to NULL
* so that function under harness will return immediately upon a NULL
* parameter check. */
if( sntpStatus != SntpSuccess )
{
pContext = NULL;
}
return pContext;
}

6
arcs-sdk/modules/coresntp/test/cbmc/stubs/README.md Normal file
View File

@@ -0,0 +1,6 @@
CBMC proof stubs
======================
This directory contains the stubs written for CBMC proofs. It is
common to stub out functionality like network send and receive methods
when writing a CBMC proof, and the code for these stubs goes here.

237
arcs-sdk/modules/coresntp/test/cbmc/stubs/core_sntp_stubs.c Normal file
View File

@@ -0,0 +1,237 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/**
* @file core_sntp_stubs.c
* @brief Definition of stubs for UDP transport and authentication interfaces of coreSNTP API.
*/
#include <stdint.h>
#include "core_sntp_client.h"
#include "core_sntp_serializer.h"
#include "core_sntp_stubs.h"
#define TEST_TIMESTAMP \
{ \
.seconds = UINT32_MAX, \
.fractions = 1000 \
}
/* An exclusive bound on the times that the NetworkInterfaceSendStub will be
* invoked before returning a loop terminating value. This is usually defined
* in the Makefile of the harnessed function. */
#ifndef MAX_NETWORK_SEND_TRIES
#define MAX_NETWORK_SEND_TRIES 2
#endif
/* An exclusive bound on the times that the NetworkInterfaceReceiveStub will
* return an unbound value. At this value and beyond, the
* NetworkInterfaceReceiveStub will return zero on every call. */
#ifndef MAX_NETWORK_RECV_TRIES
#define MAX_NETWORK_RECV_TRIES 5
#endif
static SntpTimestamp_t testTime = TEST_TIMESTAMP;
int32_t NetworkInterfaceReceiveStub( NetworkContext_t * pNetworkContext,
uint32_t serverAddr,
uint16_t serverPort,
void * pBuffer,
uint16_t bytesToRecv )
{
__CPROVER_assert( pBuffer != NULL,
"NetworkInterfaceReceiveStub pBuffer is NULL." );
__CPROVER_assert( __CPROVER_w_ok( pBuffer, bytesToRecv ),
"NetworkInterfaceReceiveStub pBuffer is not writable up to bytesToRecv." );
/* The havoc fills the buffer with unconstrained values. */
__CPROVER_havoc_object( pBuffer );
int32_t bytesOrError;
static size_t tries = 0;
/* It is a bug for the application defined transport receive function to return
* more than bytesToRecv. */
__CPROVER_assume( bytesOrError <= ( int32_t ) bytesToRecv );
if( tries < ( MAX_NETWORK_RECV_TRIES - 1 ) )
{
tries++;
}
else
{
tries = 0;
bytesOrError = SNTP_PACKET_BASE_SIZE;
}
return bytesOrError;
}
int32_t NetworkInterfaceSendStub( NetworkContext_t * pNetworkContext,
uint32_t serverAddr,
uint16_t serverPort,
const void * pBuffer,
uint16_t bytesToSend )
{
__CPROVER_assert( pBuffer != NULL,
"NetworkInterfaceSendStub pBuffer is NULL." );
__CPROVER_assert( __CPROVER_r_ok( pBuffer, bytesToSend ),
"NetworkInterfaceSendStub pBuffer is not readable up to bytesToSend." );
/* The number of tries to send the message before this invocation. */
static size_t tries = 0;
int32_t bytesOrError;
/* It is a bug for the application defined transport send function to return
* more than bytesToSend. */
__CPROVER_assume( bytesOrError <= ( int32_t ) bytesToSend );
/* If the maximum tries are reached, then return a timeout. In the SNTP library
* this stub is wrapped in a loop that will not end until the bytesOrError
* returned is negative. This means we could loop possibly INT32_MAX
* iterations. Looping for INT32_MAX times adds no value to the proof.
* What matters is that the SNTP library can handle all the possible values
* that could be returned. */
if( tries < ( MAX_NETWORK_SEND_TRIES - 1 ) )
{
tries++;
}
else
{
tries = 0;
/* This ensures that all the remaining bytes are sent in the last try. */
bytesOrError = bytesToSend;
}
return bytesOrError;
}
SntpStatus_t GenerateClientAuthStub( SntpAuthContext_t * pContext,
const SntpServerInfo_t * pTimeServer,
void * pBuffer,
size_t bufferSize,
uint16_t * pAuthCodeSize )
{
__CPROVER_assert( pTimeServer != NULL,
"GenerateClientAuthStub Time Server is NULL." );
__CPROVER_assert( pBuffer != NULL,
"GenerateClientAuthStub pBuffer is NULL." );
SntpStatus_t sntpStatus = SntpSuccess;
if( bufferSize <= SNTP_PACKET_BASE_SIZE )
{
sntpStatus = SntpErrorBufferTooSmall;
}
else
{
*pAuthCodeSize = SNTP_PACKET_BASE_SIZE;
}
return sntpStatus;
}
SntpStatus_t ValidateServerAuthStub( SntpAuthContext_t * pContext,
const SntpServerInfo_t * pTimeServer,
const void * pResponseData,
uint16_t responseSize )
{
return SntpSuccess;
}
bool ResolveDnsFuncStub( const SntpServerInfo_t * pServerAddr,
uint32_t * pIpV4Addr )
{
__CPROVER_assert( pServerAddr != NULL,
"ResolveDnsFuncStub pServerAddr is NULL." );
/* For the proofs, returning a non deterministic boolean value
* will be good enough. */
return nondet_bool();
}
void GetTimeFuncStub( SntpTimestamp_t * pCurrentTime )
{
__CPROVER_assert( pCurrentTime != NULL,
"GetTimeFuncStub pCurrentTime is NULL." );
bool value = nondet_bool();
if( value )
{
testTime.fractions = testTime.fractions + ( uint32_t ) 100000000;
}
else
{
testTime.fractions = testTime.fractions - ( uint32_t ) 1;
}
*pCurrentTime = testTime;
}
void SetTimeFuncStub( const SntpServerInfo_t * pTimeServer,
const SntpTimestamp_t * pServerTime,
int64_t clockOffsetMs,
SntpLeapSecondInfo_t leapSecondInfo )
{
__CPROVER_assert( pTimeServer != NULL,
"SetTimeFuncStub pTimeServer is NULL." );
__CPROVER_assert( pServerTime != NULL,
"SetTimeFuncStub pServerTime is NULL." );
}
SntpStatus_t Sntp_SerializeRequest( SntpTimestamp_t * pRequestTime,
uint32_t randomNumber,
void * pBuffer,
size_t bufferSize )
{
__CPROVER_assert( pRequestTime != NULL,
"Sntp_SerializeRequest pRequestTime is NULL." );
__CPROVER_assert( pBuffer != NULL,
"Sntp_SerializeRequest pBuffer is NULL." );
return SntpSuccess;
}
SntpStatus_t Sntp_DeserializeResponse( const SntpTimestamp_t * pRequestTime,
const SntpTimestamp_t * pResponseRxTime,
const void * pResponseBuffer,
size_t bufferSize,
SntpResponseData_t * pParsedResponse )
{
if( nondet_bool() )
{
return SntpSuccess;
}
else
{
return SntpRejectedResponseRetryWithBackoff;
}
}

103
arcs-sdk/modules/coresntp/test/unit-test/CMakeLists.txt Normal file
View File

@@ -0,0 +1,103 @@
# Include file path configuration for coreSNTP library.
include(${MODULE_ROOT_DIR}/coreSntpFilePaths.cmake)
project ("coreSNTP unit tests")
cmake_minimum_required (VERSION 3.2.0)
# ==================== Define your project name ========================
set(project_name "core_sntp")
# ===================== Create your mock here ========================
# list the files to mock here
list(APPEND mock_list
"${MODULE_ROOT_DIR}/source/include/core_sntp_serializer.h"
)
# list the directories your mocks need
list(APPEND mock_include_list
${CORE_SNTP_INCLUDE_PUBLIC_DIRS}
)
#list the definitions of your mocks to control what to be included
list(APPEND mock_define_list
""
)
# ================= Create the library under test here ==================
# list the files you would like to test here
list(APPEND real_source_files
${CORE_SNTP_SOURCES}
)
# list the directories the module under test includes
list(APPEND real_include_directories
${CORE_SNTP_INCLUDE_PUBLIC_DIRS}
${CMAKE_CURRENT_LIST_DIR}
)
# ===================== Create UnitTest Code here =====================
# list the directories your test needs to include
list(APPEND test_include_directories
${CORE_SNTP_INCLUDE_PUBLIC_DIRS}
${CMAKE_CURRENT_LIST_DIR}
)
# ============================= Create unit test targets ===================================
set(mock_name "${project_name}_mock")
set(real_name "${project_name}_real")
create_mock_list(${mock_name}
"${mock_list}"
"${MODULE_ROOT_DIR}/tools/cmock/project.yml"
"${mock_include_list}"
"${mock_define_list}"
)
create_real_library(${real_name}
"${real_source_files}"
"${real_include_directories}"
"${mock_name}"
)
# As both Mock and Real libraries targets contain the
# symbols for the core_sntp_serializer.c file, the linking
# order has the mock library first for the core_sntp_client_utest.c
# to use the mock for Serializer API calls.
list(APPEND utest_link_list
-l${mock_name}
lib${real_name}.a
)
list(APPEND utest_dep_list
${real_name}
)
# core_sntp_client_utest target
set(utest_name "${project_name}_client_utest")
set(utest_source "${project_name}_client_utest.c")
create_test(${utest_name}
${utest_source}
"${utest_link_list}"
"${utest_dep_list}"
"${test_include_directories}"
)
# Redefine the linking list as the mock is not needed for
# the core_sntp_serializer tests.
set(utest_link_list "")
list(APPEND utest_link_list
lib${real_name}.a
)
# core_sntp_serializer_utest target
set(utest_name "${project_name}_serializer_utest")
set(utest_source "${project_name}_serializer_utest.c")
create_test(${utest_name}
${utest_source}
"${utest_link_list}"
"${utest_dep_list}"
"${test_include_directories}"
)

58
arcs-sdk/modules/coresntp/test/unit-test/cmock_build.cmake Normal file
View File

@@ -0,0 +1,58 @@
# Macro utility to clone the CMock submodule.
macro( clone_cmock )
find_package( Git REQUIRED )
message( "Cloning submodule CMock." )
execute_process( COMMAND rm -rf ${CMOCK_DIR}
COMMAND ${GIT_EXECUTABLE} submodule update --checkout --init --recursive ${CMOCK_DIR}
WORKING_DIRECTORY ${PROJECT_SOURCE_DIR}
RESULT_VARIABLE CMOCK_CLONE_RESULT )
if( NOT ${CMOCK_CLONE_RESULT} STREQUAL "0" )
message( FATAL_ERROR "Failed to clone CMock submodule." )
endif()
endmacro()
# Macro utility to add library targets for Unity and CMock to build configuration.
macro( add_cmock_targets )
# Build Configuration for CMock and Unity libraries.
list( APPEND CMOCK_INCLUDE_DIRS
"${CMOCK_DIR}/vendor/unity/src/"
"${CMOCK_DIR}/vendor/unity/extras/fixture/src"
"${CMOCK_DIR}/vendor/unity/extras/memory/src"
"${CMOCK_DIR}/src"
)
add_library(cmock STATIC
"${CMOCK_DIR}/src/cmock.c"
)
set_target_properties(cmock PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib
POSITION_INDEPENDENT_CODE ON
COMPILE_FLAGS "-Og"
)
target_include_directories(cmock PUBLIC
${CMOCK_DIR}/src
${CMOCK_DIR}/vendor/unity/src/
${CMOCK_DIR}/examples
${CMOCK_INCLUDE_DIRS}
)
add_library(unity STATIC
"${CMOCK_DIR}/vendor/unity/src/unity.c"
"${CMOCK_DIR}/vendor/unity/extras/fixture/src/unity_fixture.c"
"${CMOCK_DIR}/vendor/unity/extras/memory/src/unity_memory.c"
)
set_target_properties(unity PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib
POSITION_INDEPENDENT_CODE ON
)
target_include_directories(unity PUBLIC
${CMOCK_INCLUDE_DIRS}
)
target_link_libraries(cmock unity)
endmacro()

1388
arcs-sdk/modules/coresntp/test/unit-test/core_sntp_client_utest.c Normal file
View File

File diff suppressed because it is too large Load Diff

62
arcs-sdk/modules/coresntp/test/unit-test/core_sntp_config.h Normal file
View File

@@ -0,0 +1,62 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/**
* @file core_sntp_config.h
* @brief This header sets configuration macros for the SNTP library.
*/
#ifndef CORE_SNTP_CONFIG_H_
#define CORE_SNTP_CONFIG_H_
/* Standard include. */
#include <stdio.h>
/* @[code_example_loggingmacros] */
/************* Define Logging Macros using printf function ***********/
#define PrintfError( ... ) printf( "Error: "__VA_ARGS__ ); printf( "\n" )
#define PrintfWarn( ... ) printf( "Warn: "__VA_ARGS__ ); printf( "\n" )
#define PrintfInfo( ... ) printf( "Info: " __VA_ARGS__ ); printf( "\n" )
#define PrintfDebug( ... ) printf( "Debug: " __VA_ARGS__ ); printf( "\n" )
#ifdef LOGGING_LEVEL_ERROR
#define LogError( message ) PrintfError message
#elif defined( LOGGING_LEVEL_WARNING )
#define LogError( message ) PrintfError message
#define LogWarn( message ) PrintfWarn message
#elif defined( LOGGING_LEVEL_INFO )
#define LogError( message ) PrintfError message
#define LogWarn( message ) PrintfWarn message
#define LogInfo( message ) PrintfInfo message
#elif defined( LOGGING_LEVEL_DEBUG )
#define LogError( message ) PrintfError message
#define LogWarn( message ) PrintfWarn message
#define LogInfo( message ) PrintfInfo message
#define LogDebug( message ) PrintfDebug message
#endif /* ifdef LOGGING_LEVEL_ERROR */
/**************************************************/
/* @[code_example_loggingmacros] */
#endif /* ifndef CORE_SNTP_CONFIG_H_ */

970
arcs-sdk/modules/coresntp/test/unit-test/core_sntp_serializer_utest.c Normal file
View File

@@ -0,0 +1,970 @@
/*
* coreSNTP v1.3.1
* Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* SPDX-License-Identifier: MIT
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
/* Standard includes. */
#include <string.h>
#include <stdbool.h>
#include <stdlib.h>
#include <stdint.h>
/* POSIX include. */
#include <arpa/inet.h>
/* Unity include. */
#include "unity.h"
/* coreSNTP Serializer API include */
#include "core_sntp_serializer.h"
#define TEST_TIMESTAMP \
{ \
.seconds = UINT32_MAX, \
.fractions = 1000 \
}
#define ZERO_TIMESTAMP \
{ \
.seconds = 0, \
.fractions = 0 \
}
/* Bits 3-5 are used for Version in 1st byte of SNTP packet. */
#define SNTP_PACKET_VERSION_VAL ( 4 /* Version */ << 3 /* Bits 3-5 used in byte */ )
/* Values for "Mode" field in an SNTP packet. */
#define SNTP_PACKET_MODE_SERVER ( 4 )
#define SNTP_PACKET_MODE_CLIENT ( 3 )
/* The least significant bit position of "Leap Indicator" field
* in the first byte of an SNTP packet. */
#define SNTP_PACKET_LEAP_INDICATOR_LSB ( 6 )
/* The byte positions of SNTP packet fields in the 48 bytes sized
* packet format. */
#define SNTP_PACKET_STRATUM_BYTE_POS ( 1 )
#define SNTP_PACKET_KOD_CODE_FIRST_BYTE_POS ( 12 )
#define SNTP_PACKET_ORIGIN_TIME_FIRST_BYTE_POS ( 24 )
#define SNTP_PACKET_RX_TIMESTAMP_FIRST_BYTE_POS ( 32 )
#define SNTP_PACKET_TX_TIMESTAMP_FIRST_BYTE_POS ( 40 )
/* Values of "Stratum" field in an SNTP packet. */
#define SNTP_PACKET_STRATUM_KOD ( 0 )
#define SNTP_PACKET_STRATUM_SECONDARY_SERVER ( 15 )
/* ASCII string codes that a server can send in a Kiss-o'-Death response. */
#define KOD_CODE_DENY "DENY"
#define KOD_CODE_RSTR "RSTR"
#define KOD_CODE_RATE "RATE"
#define KOD_CODE_OTHER_EXAMPLE_1 "AUTH"
#define KOD_CODE_OTHER_EXAMPLE_2 "CRYP"
#define YEARS_20_IN_SECONDS ( ( 20 * 365 + 20 / 4 ) * 24 * 3600 )
#define YEARS_68_IN_SECONDS ( ( 68 * 365 + 68 / 4 ) * 24 * 3600 )
/* Macro utility to convert the fixed-size Kiss-o'-Death ASCII code
* to integer.*/
#define INTEGER_VAL_OF_KOD_CODE( codePtr ) \
( ( uint32_t ) ( ( ( uint32_t ) codePtr[ 0 ] << 24 ) | \
( ( uint32_t ) codePtr[ 1 ] << 16 ) | \
( ( uint32_t ) codePtr[ 2 ] << 8 ) | \
( ( uint32_t ) codePtr[ 3 ] ) ) )
/* Buffer used for SNTP requests and responses in tests. */
static uint8_t testBuffer[ SNTP_PACKET_BASE_SIZE ];
static SntpResponseData_t parsedData;
static SntpTimestamp_t zeroTimestamp = ZERO_TIMESTAMP;
/* ============================ Helper Functions ============================ */
/* Utility macro to convert seconds to milliseconds. */
static uint64_t TO_MS( uint64_t seconds )
{
return( seconds * 1000 );
}
static void addTimestampToResponseBuffer( SntpTimestamp_t * pTime,
uint8_t * pResponseBuffer,
size_t startingPos )
{
/* Convert the request time into network byte order to use to fill in buffer. */
uint32_t secs = pTime->seconds;
uint32_t fracs = pTime->fractions;
pResponseBuffer[ startingPos ] = secs >> 24; /* seconds, byte 1*/
pResponseBuffer[ startingPos + 1 ] = secs >> 16; /* seconds, byte 2 */
pResponseBuffer[ startingPos + 2 ] = secs >> 8; /* seconds, byte 3 */
pResponseBuffer[ startingPos + 3 ] = secs; /* seconds, byte 4 */
pResponseBuffer[ startingPos + 4 ] = fracs >> 24; /* fractions, byte 1*/
pResponseBuffer[ startingPos + 5 ] = fracs >> 16; /* fractions, byte 2 */
pResponseBuffer[ startingPos + 6 ] = fracs >> 8; /* fractions, byte 3 */
pResponseBuffer[ startingPos + 7 ] = fracs; /* fractions, byte 4 */
}
static void fillValidSntpResponseData( uint8_t * pBuffer,
SntpTimestamp_t * pRequestTime )
{
/* Clear the buffer. */
memset( pBuffer, 0, SNTP_PACKET_BASE_SIZE );
/* Set the "Version" and "Mode" fields in the first byte of SNTP packet. */
pBuffer[ 0 ] = SNTP_PACKET_VERSION_VAL | SNTP_PACKET_MODE_SERVER;
/* Set the SNTP response packet to contain the "originate" timestamp
* correctly, as matching the SNTP request timestamp. */
addTimestampToResponseBuffer( pRequestTime,
pBuffer,
SNTP_PACKET_ORIGIN_TIME_FIRST_BYTE_POS );
SntpTimestamp_t testTime = TEST_TIMESTAMP;
/* Set the SNTP response packet to contain the "receive" timestamp
* correctly, as matching the SNTP request timestamp. */
addTimestampToResponseBuffer( &testTime,
pBuffer,
SNTP_PACKET_RX_TIMESTAMP_FIRST_BYTE_POS );
/* Set the SNTP response packet to contain the "transmit" timestamp
* correctly, as matching the SNTP request timestamp. */
addTimestampToResponseBuffer( &testTime,
pBuffer,
SNTP_PACKET_TX_TIMESTAMP_FIRST_BYTE_POS );
/* Set the "Stratum" byte in the response packet to represent a
* secondary NTP server. */
pBuffer[ SNTP_PACKET_STRATUM_BYTE_POS ] = SNTP_PACKET_STRATUM_SECONDARY_SERVER;
}
/* Common test code that fills SNTP response packet with server times and validates
* that @ref Sntp_DeserializeResponse API correctly calculates the clock offset. */
static void testClockOffsetCalculation( SntpTimestamp_t * clientTxTime,
SntpTimestamp_t * serverRxTime,
SntpTimestamp_t * serverTxTime,
SntpTimestamp_t * clientRxTime,
SntpStatus_t expectedStatus,
int64_t expectedClockOffsetMs )
{
/* Update the response packet with the server time. */
addTimestampToResponseBuffer( clientTxTime,
testBuffer,
SNTP_PACKET_ORIGIN_TIME_FIRST_BYTE_POS );
addTimestampToResponseBuffer( serverRxTime,
testBuffer,
SNTP_PACKET_RX_TIMESTAMP_FIRST_BYTE_POS );
addTimestampToResponseBuffer( serverTxTime,
testBuffer,
SNTP_PACKET_TX_TIMESTAMP_FIRST_BYTE_POS );
/* Call the API under test. */
TEST_ASSERT_EQUAL( expectedStatus, Sntp_DeserializeResponse( clientTxTime,
clientRxTime,
testBuffer,
sizeof( testBuffer ),
&parsedData ) );
/* Make sure that the API has indicated in the output parameter that
* clock-offset could not be calculated. */
TEST_ASSERT_EQUAL( expectedClockOffsetMs, parsedData.clockOffsetMs );
/* Validate other fields in the output parameter. */
TEST_ASSERT_EQUAL( 0, memcmp( &parsedData.serverTime, serverTxTime, sizeof( SntpTimestamp_t ) ) );
TEST_ASSERT_EQUAL( NoLeapSecond, parsedData.leapSecondType );
TEST_ASSERT_EQUAL( SNTP_KISS_OF_DEATH_CODE_NONE, parsedData.rejectedResponseCode );
}
/* ============================ UNITY FIXTURES ============================ */
/* Called before each test method. */
void setUp()
{
memset( &parsedData, 0, sizeof( parsedData ) );
}
/* Called at the beginning of the whole suite. */
void suiteSetUp()
{
}
/* Called at the end of the whole suite. */
int suiteTearDown( int numFailures )
{
return numFailures;
}
/* ========================================================================== */
/**
* @brief Test @ref Sntp_SerializeRequest with invalid parameters.
*/
void test_SerializeRequest_InvalidParams( void )
{
SntpTimestamp_t testTime = TEST_TIMESTAMP;
/* Pass invalid time object. */
TEST_ASSERT_EQUAL( SntpErrorBadParameter,
Sntp_SerializeRequest( NULL,
( rand() % UINT32_MAX ),
testBuffer,
sizeof( testBuffer ) ) );
/* Pass invalid buffer. */
TEST_ASSERT_EQUAL( SntpErrorBadParameter,
Sntp_SerializeRequest( &testTime,
( rand() % UINT32_MAX ),
NULL,
sizeof( testBuffer ) ) );
/* Pass zero timestamp for request time. */
TEST_ASSERT_EQUAL( SntpErrorBadParameter,
Sntp_SerializeRequest( &zeroTimestamp,
( rand() % UINT32_MAX ),
testBuffer,
sizeof( testBuffer ) ) );
/* Pass a buffer size less than 48 bytes of minimum SNTP packet size. */
TEST_ASSERT_EQUAL( SntpErrorBufferTooSmall,
Sntp_SerializeRequest( &testTime,
( rand() % UINT32_MAX ),
testBuffer,
1 ) );
}
/**
* @brief Validate the serialization operation of the @ref Sntp_SerializeRequest API.
*/
void test_SerializeRequest_NominalCase( void )
{
SntpTimestamp_t testTime = TEST_TIMESTAMP;
const uint32_t randomVal = 0xAABBCCDD;
/* Expected transmit timestamp in the SNTP request packet. */
const SntpTimestamp_t expectedTxTime =
{
.seconds = testTime.seconds,
.fractions = ( testTime.fractions | ( randomVal >> 16 ) )
};
/* The expected serialization of the SNTP request packet. */
uint8_t expectedSerialization[ SNTP_PACKET_BASE_SIZE ] =
{
0x00 /* Leap Indicator */ | 0x20 /* Version */ | 0x03, /* Client Mode */
0x00, /* stratum */
0x00, /* poll interval */
0x00, /* precision */
0x00, 0x00, 0x00, 0x00, /* root delay */
0x00, 0x00, 0x00, 0x00, /* root dispersion */
0x00, 0x00, 0x00, 0x00, /* reference ID */
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, /* reference time */
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, /* origin timestamp */
0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, /* receive timestamp */
expectedTxTime.seconds >> 24, /* transmit timestamp - seconds, byte 1 */
expectedTxTime.seconds >> 16, /* transmit timestamp - seconds, byte 2 */
expectedTxTime.seconds >> 8, /* transmit timestamp - seconds, byte 3 */
expectedTxTime.seconds, /* transmit timestamp - seconds, byte 4 */
expectedTxTime.fractions >> 24, /* transmit timestamp - fractions, byte 1 */
expectedTxTime.fractions >> 16, /* transmit timestamp - fractions, byte 2 */
expectedTxTime.fractions >> 8, /* transmit timestamp - fractions, byte 3 */
expectedTxTime.fractions, /* transmit timestamp - fractions, byte 4 */
};
/* Call the API under test. */
TEST_ASSERT_EQUAL( SntpSuccess,
Sntp_SerializeRequest( &testTime,
randomVal,
testBuffer,
sizeof( testBuffer ) ) );
/* Validate that serialization operation by the API. */
TEST_ASSERT_EQUAL_UINT8_ARRAY( expectedSerialization,
testBuffer,
SNTP_PACKET_BASE_SIZE );
/* Check that the request timestamp object has been updated with the random value. */
TEST_ASSERT_EQUAL( 0, memcmp( &expectedTxTime,
&testTime,
sizeof( SntpTimestamp_t ) ) );
}
/**
* @brief Test @ref Sntp_DeserializeResponse with invalid parameters.
*/
void test_DeserializeResponse_InvalidParams( void )
{
SntpTimestamp_t testTime = TEST_TIMESTAMP;
/* Pass invalid time objects. */
TEST_ASSERT_EQUAL( SntpErrorBadParameter,
Sntp_DeserializeResponse( NULL,
&testTime,
testBuffer,
sizeof( testBuffer ),
&parsedData ) );
TEST_ASSERT_EQUAL( SntpErrorBadParameter,
Sntp_DeserializeResponse( &testTime,
NULL,
testBuffer,
sizeof( testBuffer ),
&parsedData ) );
/* Pass invalid buffer. */
TEST_ASSERT_EQUAL( SntpErrorBadParameter,
Sntp_DeserializeResponse( &testTime,
&testTime,
NULL,
sizeof( testBuffer ),
&parsedData ) );
/* Pass a buffer size less than 48 bytes of minimum SNTP packet size. */
TEST_ASSERT_EQUAL( SntpErrorBufferTooSmall,
Sntp_DeserializeResponse( &testTime,
&testTime,
testBuffer,
sizeof( testBuffer ) / 2,
&parsedData ) );
/* Pass invalid output parameter. */
TEST_ASSERT_EQUAL( SntpErrorBadParameter,
Sntp_DeserializeResponse( &testTime,
&testTime,
testBuffer,
sizeof( testBuffer ),
NULL ) );
/* Pass zero timestamp for request time. */
TEST_ASSERT_EQUAL( SntpErrorBadParameter,
Sntp_DeserializeResponse( &zeroTimestamp,
&testTime,
testBuffer,
sizeof( testBuffer ),
&parsedData ) );
}
/**
* @brief Test that @ref Sntp_DeserializeResponse API can detect invalid
* SNTP response packets.
*/
void test_DeserializeResponse_Invalid_Responses( void )
{
SntpTimestamp_t clientTime = TEST_TIMESTAMP;
/* Fill buffer with general SNTP response data. */
fillValidSntpResponseData( testBuffer, &clientTime );
/* ******* Test when SNTP packet does not a non-server value in the "Mode" field. **** */
testBuffer[ 0 ] = SNTP_PACKET_VERSION_VAL | SNTP_PACKET_MODE_CLIENT;
/* Call the API under test. */
TEST_ASSERT_EQUAL( SntpInvalidResponse, Sntp_DeserializeResponse( &clientTime,
&clientTime,
testBuffer,
sizeof( testBuffer ),
&parsedData ) );
/* Set the Mode field to the correct value for Server. */
testBuffer[ 0 ] = SNTP_PACKET_VERSION_VAL | SNTP_PACKET_MODE_SERVER;
/************** Test when "originate timestamp" is zero ***************/
addTimestampToResponseBuffer( &zeroTimestamp,
testBuffer,
SNTP_PACKET_ORIGIN_TIME_FIRST_BYTE_POS );
/* Call the API under test. */
TEST_ASSERT_EQUAL( SntpInvalidResponse, Sntp_DeserializeResponse( &clientTime,
&clientTime,
testBuffer,
sizeof( testBuffer ),
&parsedData ) );
/* Set the "originate timestamp" to a non-zero value for the next test. */
addTimestampToResponseBuffer( &clientTime,
testBuffer,
SNTP_PACKET_ORIGIN_TIME_FIRST_BYTE_POS );
/************** Test when "receive timestamp" is zero ***************/
addTimestampToResponseBuffer( &zeroTimestamp,
testBuffer,
SNTP_PACKET_RX_TIMESTAMP_FIRST_BYTE_POS );
/* Call the API under test. */
TEST_ASSERT_EQUAL( SntpInvalidResponse, Sntp_DeserializeResponse( &clientTime,
&clientTime,
testBuffer,
sizeof( testBuffer ),
&parsedData ) );
/* Set the "receive timestamp" to a non-zero value for the next test. */
addTimestampToResponseBuffer( &clientTime,
testBuffer,
SNTP_PACKET_RX_TIMESTAMP_FIRST_BYTE_POS );
/************** Test when "transmit timestamp" is zero ***************/
addTimestampToResponseBuffer( &zeroTimestamp,
testBuffer,
SNTP_PACKET_TX_TIMESTAMP_FIRST_BYTE_POS );
/* Call the API under test. */
TEST_ASSERT_EQUAL( SntpInvalidResponse, Sntp_DeserializeResponse( &clientTime,
&clientTime,
testBuffer,
sizeof( testBuffer ),
&parsedData ) );
/* Set the "transmit timestamp" to a non-zero value for the next test. */
addTimestampToResponseBuffer( &clientTime,
testBuffer,
SNTP_PACKET_TX_TIMESTAMP_FIRST_BYTE_POS );
/******** Test when SNTP response packet does not have "originate" timestamp matching
* the "transmit" time sent by the client in the SNTP request. ************/
SntpTimestamp_t originateTime = TEST_TIMESTAMP;
/* Test when only the seconds part of the "originate" timestamp does not match
* the client request time .*/
originateTime.seconds = clientTime.seconds + 1;
addTimestampToResponseBuffer( &originateTime,
testBuffer,
SNTP_PACKET_ORIGIN_TIME_FIRST_BYTE_POS );
/* Call the API under test. */
TEST_ASSERT_EQUAL( SntpInvalidResponse, Sntp_DeserializeResponse( &clientTime,
&clientTime,
testBuffer,
sizeof( testBuffer ),
&parsedData ) );
/* Test when only the fractions part of the "originate" timestamp does not match
* the client request time .*/
originateTime.seconds = clientTime.seconds;
originateTime.fractions = clientTime.fractions + 1;
addTimestampToResponseBuffer( &originateTime,
testBuffer,
SNTP_PACKET_ORIGIN_TIME_FIRST_BYTE_POS );
/* Call the API under test. */
TEST_ASSERT_EQUAL( SntpInvalidResponse, Sntp_DeserializeResponse( &clientTime,
&clientTime,
testBuffer,
sizeof( testBuffer ),
&parsedData ) );
}
/**
* @brief Test @ref Sntp_DeserializeResponse API to de-serialize Kiss-o'-Death
* responses from SNTP server.
*
* The API should return an error code appropriate for the Kiss-o'-Death code
* and update the member of output parameter to point the ASCII string code
* in the response packet.
*/
void test_DeserializeResponse_KoD_packets( void )
{
/* Use same value for request and response times, as API should not process
* them for Kiss-o'-Death response packets. */
SntpTimestamp_t testTime = TEST_TIMESTAMP;
uint32_t KodCodeNetworkOrder = 0;
/* Populate the buffer with a valid SNTP response before converting it
* into a Kiss-o'-Death message. */
fillValidSntpResponseData( testBuffer, &testTime );
/* Update the "Stratum" field in the buffer to make the packet a Kiss-o'-Death message. */
testBuffer[ SNTP_PACKET_STRATUM_BYTE_POS ] = SNTP_PACKET_STRATUM_KOD;
/* Common test code for testing de-serialization of Kiss-o'-Death packet containing a specific
* code with@ref Sntp_DeserializeResponse API. */
#define TEST_API_FOR_KOD_CODE( code, expectedStatus ) \
do { \
KodCodeNetworkOrder = INTEGER_VAL_OF_KOD_CODE( code ); \
testBuffer[ SNTP_PACKET_KOD_CODE_FIRST_BYTE_POS ] = KodCodeNetworkOrder >> 24; \
testBuffer[ SNTP_PACKET_KOD_CODE_FIRST_BYTE_POS + 1 ] = KodCodeNetworkOrder >> 16; \
testBuffer[ SNTP_PACKET_KOD_CODE_FIRST_BYTE_POS + 2 ] = KodCodeNetworkOrder >> 8; \
testBuffer[ SNTP_PACKET_KOD_CODE_FIRST_BYTE_POS + 3 ] = KodCodeNetworkOrder; \
\
/* Call API under test. */ \
TEST_ASSERT_EQUAL( expectedStatus, \
Sntp_DeserializeResponse( &testTime, \
&testTime, \
testBuffer, \
sizeof( testBuffer ), \
&parsedData ) ); \
\
/* Test that API has populated the output parameter with the parsed \
* KoD code. */ \
TEST_ASSERT_EQUAL( INTEGER_VAL_OF_KOD_CODE( code ), \
parsedData.rejectedResponseCode ); \
\
} while( 0 )
/* Test Kiss-o'-Death server response with "DENY" code. */
TEST_API_FOR_KOD_CODE( KOD_CODE_DENY, SntpRejectedResponseChangeServer );
/* Test Kiss-o'-Death server response with "RSTR" code. */
TEST_API_FOR_KOD_CODE( KOD_CODE_RSTR, SntpRejectedResponseChangeServer );
/* Test Kiss-o'-Death server response with "RATE" code. */
TEST_API_FOR_KOD_CODE( KOD_CODE_RATE, SntpRejectedResponseRetryWithBackoff );
/* ***** Test de-serialization of Kiss-o'-Death server response with other codes ***** */
TEST_API_FOR_KOD_CODE( KOD_CODE_OTHER_EXAMPLE_1, SntpRejectedResponseOtherCode );
TEST_API_FOR_KOD_CODE( KOD_CODE_OTHER_EXAMPLE_2, SntpRejectedResponseOtherCode );
}
/**
* @brief Test that @ref Sntp_DeserializeResponse API can process an accepted
* SNTP server response, and compute clock-offset when the server and client times
* are >= 68 years apart.
*/
void test_DeserializeResponse_AcceptedResponse_ClockOffset_Edge_Cases( void )
{
SntpTimestamp_t clientTime = TEST_TIMESTAMP;
/* Fill buffer with general SNTP response data. */
fillValidSntpResponseData( testBuffer, &clientTime );
/* Test when the client is 68 years ahead of server time .*/
SntpTimestamp_t serverTime =
{
clientTime.seconds - YEARS_68_IN_SECONDS,
clientTime.fractions
};
testClockOffsetCalculation( &clientTime, &serverTime,
&serverTime, &clientTime,
SntpSuccess,
TO_MS( -YEARS_68_IN_SECONDS ) );
/* Now test when the client is 68 years ahead of server time .*/
serverTime.seconds = clientTime.seconds + YEARS_68_IN_SECONDS;
testClockOffsetCalculation( &clientTime, &serverTime,
&serverTime, &clientTime,
SntpSuccess,
TO_MS( YEARS_68_IN_SECONDS ) );
/* Now test special cases when the server and client times are (INT32_MAX + 1) =
* 2^31 apart seconds apart. The library should ALWAYS think that server
* is ahead of the client in this special case, and thus return the maximum
* signed 32 bit integer as the clock-offset.
*/
/* Case when "Server Time - Client Time" results in negative value. */
serverTime.seconds = clientTime.seconds + INT32_MAX + 1;
testClockOffsetCalculation( &clientTime, &serverTime,
&serverTime, &clientTime,
SntpSuccess,
TO_MS( ( int64_t ) INT32_MAX + 1 ) );
/* Test when "Server Time - Client Time" results in positive value. */
serverTime.seconds = UINT32_MAX;
clientTime.seconds = serverTime.seconds - INT32_MAX - 1;
testClockOffsetCalculation( &clientTime, &serverTime,
&serverTime, &clientTime,
SntpSuccess,
TO_MS( ( int64_t ) INT32_MAX + 1 ) );
/* Reset client time to UINT32_MAX */
clientTime.seconds = UINT32_MAX;
/* Now test cases when the server and client times are exactly
* INT32_MAX seconds apart. */
serverTime.seconds = clientTime.seconds - INT32_MAX;
testClockOffsetCalculation( &clientTime, &serverTime,
&serverTime, &clientTime,
SntpSuccess,
TO_MS( -INT32_MAX ) );
serverTime.seconds = clientTime.seconds + INT32_MAX;
testClockOffsetCalculation( &clientTime, &serverTime,
&serverTime, &clientTime,
SntpSuccess,
TO_MS( INT32_MAX ) );
/* Reset client and server times to be 68 years apart. */
clientTime.seconds = UINT32_MAX;
serverTime.seconds = UINT32_MAX + YEARS_68_IN_SECONDS;
/* Now test the contrived case when only the send network path
* represents timestamps that overflow but the receive network path
* has timestamps that do not overflow.
* As only the single network path contains time difference of 68 years,
* the expected clock-offset, being an average of the network paths, is
* 34 years of duration. */
testClockOffsetCalculation( &clientTime, &serverTime, /* Send Path times are 68 years apart */
&serverTime, &serverTime, /* Receive path times are the same. */
SntpSuccess,
TO_MS( YEARS_68_IN_SECONDS / 2 ) ); /* Expected offset of 34 years. */
/* Now test the contrived case when only the receive network path
* represents timestamps that overflow but the send network path
* has timestamps that do not overflow.
* As only the single network path contains time difference of 68 years,
* the expected clock-offset, being an average of the network paths, is
* 34 years of duration. */
testClockOffsetCalculation( &clientTime, &clientTime, /* Send Path times are the same, i.e. don't overflow */
&serverTime, &clientTime, /* Receive path times are 68 years apart. */
SntpSuccess,
TO_MS( YEARS_68_IN_SECONDS / 2 ) ); /* Expected offset of 34 years. */
}
void test_Sntp_DeserializeResponse_ClockOffset_Milliseconds_Cases( void )
{
SntpTimestamp_t clientTime =
{
.seconds = 0,
/* 500 milliseconds. */
.fractions = 500 * 1000 * SNTP_FRACTION_VALUE_PER_MICROSECOND
};
/* Fill buffer with general SNTP response data. */
fillValidSntpResponseData( testBuffer, &clientTime );
SntpTimestamp_t serverTime =
{
.seconds = clientTime.seconds,
.fractions = clientTime.fractions
};
/* Test when server is ahead of client time. */
serverTime.fractions = 700 * 1000 * SNTP_FRACTION_VALUE_PER_MICROSECOND; /* 700 milliseconds. */
testClockOffsetCalculation( &clientTime, &serverTime, /* Send Path times are 68 years apart */
&serverTime, &clientTime, /* Receive path times are the same. */
SntpSuccess, 200 );
/* Test when server is behind client time. */
serverTime.fractions = 100 * 1000 * SNTP_FRACTION_VALUE_PER_MICROSECOND; /* 100 milliseconds. */
testClockOffsetCalculation( &clientTime, &serverTime, /* Send Path times are 68 years apart */
&serverTime, &clientTime, /* Receive path times are the same. */
SntpSuccess, -400 );
/* Test when complex case of NTP time overflow with client being ahead of server by 3900 milliseconds. */
serverTime.seconds = UINT32_MAX - 3; /* 4 seconds behind in "seconds" value. */
serverTime.fractions = 600 * 1000 * SNTP_FRACTION_VALUE_PER_MICROSECOND; /* 100 milliseconds ahead. */
testClockOffsetCalculation( &clientTime, &serverTime, /* Send Path times are 68 years apart */
&serverTime, &clientTime, /* Receive path times are the same. */
SntpSuccess, -3900 );
}
/**
* @brief Test that @ref Sntp_DeserializeResponse API can process an accepted
* SNTP server response, and calculate the clock offset for non-overflow cases
* (i.e. when the client and server times are within 34 years of each other).
*/
void test_DeserializeResponse_AcceptedResponse_Nominal_Case( void )
{
SntpTimestamp_t clientTxTime = TEST_TIMESTAMP;
/* Fill buffer with general SNTP response data. */
fillValidSntpResponseData( testBuffer, &clientTxTime );
/* Use the the same values for Rx and Tx times for server and client in the first couple
* of tests for simplicity. */
/* ==================Test when client and server are in same NTP era.================ */
/* Test when the client is 20 years ahead of server time to generate a negative offset
* result.*/
SntpTimestamp_t serverTxTime =
{
clientTxTime.seconds - YEARS_20_IN_SECONDS,
clientTxTime.fractions
};
int32_t expectedOffset = -YEARS_20_IN_SECONDS;
testClockOffsetCalculation( &clientTxTime, &serverTxTime,
&serverTxTime, &clientTxTime,
SntpSuccess, TO_MS( expectedOffset ) );
/* Now test for the client being 20 years behind server time to generate a positive
* offset result.*/
serverTxTime.seconds = UINT32_MAX;
clientTxTime.seconds = UINT32_MAX - YEARS_20_IN_SECONDS;
expectedOffset = YEARS_20_IN_SECONDS;
testClockOffsetCalculation( &clientTxTime, &serverTxTime,
&serverTxTime, &clientTxTime,
SntpSuccess, TO_MS( expectedOffset ) );
/* ==================Test when client and server are in different NTP eras.================ */
/* Test when the server is ahead of client to generate a positive clock offset result.*/
clientTxTime.seconds = UINT32_MAX; /* Client is in NTP era 0. */
serverTxTime.seconds = UINT32_MAX + YEARS_20_IN_SECONDS; /* Server is in NTP era 1. */
expectedOffset = YEARS_20_IN_SECONDS;
testClockOffsetCalculation( &clientTxTime, &serverTxTime,
&serverTxTime, &clientTxTime,
SntpSuccess, TO_MS( expectedOffset ) );
/* Test when the client is ahead of server to generate a negative clock offset result.*/
clientTxTime.seconds = UINT32_MAX + YEARS_20_IN_SECONDS; /* Client is in NTP era 1. */
serverTxTime.seconds = UINT32_MAX; /* Server is in NTP era 0. */
expectedOffset = -YEARS_20_IN_SECONDS;
testClockOffsetCalculation( &clientTxTime, &serverTxTime,
&serverTxTime, &clientTxTime,
SntpSuccess, TO_MS( expectedOffset ) );
/* Now test with different values for T1 (client Tx), T2 (server Rx), T3 (server Tx) and T4 (client Rx)
* that are used in the clock-offset calculation.
* The test case uses 2 seconds as network delay on both Client -> Server and Server -> Client path
* and 2 seconds for server processing time between receiving SNTP request and sending SNTP response */
clientTxTime.seconds = UINT32_MAX;
SntpTimestamp_t serverRxTime =
{
clientTxTime.seconds + YEARS_20_IN_SECONDS + 2,
serverTxTime.fractions
};
serverTxTime.seconds = serverRxTime.seconds + 2;
SntpTimestamp_t clientRxTime =
{
clientTxTime.seconds + 6, /* 2 seconds each for Client -> Server, Server -> Server,
* Server -> Client */
clientTxTime.fractions
};
expectedOffset = YEARS_20_IN_SECONDS;
testClockOffsetCalculation( &clientTxTime, &serverRxTime,
&serverTxTime, &clientRxTime,
SntpSuccess, TO_MS( expectedOffset ) );
}
/**
* @brief Test that @ref Sntp_DeserializeResponse API can de-serialize leap-second
* information in an accepted SNTP response packet from a server.
*/
void test_DeserializeResponse_AcceptedResponse_LeapSecond( void )
{
SntpTimestamp_t clientTime = TEST_TIMESTAMP;
SntpTimestamp_t serverTime = TEST_TIMESTAMP;
/* Fill buffer with general SNTP response data. */
fillValidSntpResponseData( testBuffer, &clientTime );
/* Update the response packet with the server time. */
addTimestampToResponseBuffer( &serverTime,
testBuffer,
SNTP_PACKET_RX_TIMESTAMP_FIRST_BYTE_POS );
addTimestampToResponseBuffer( &serverTime,
testBuffer,
SNTP_PACKET_TX_TIMESTAMP_FIRST_BYTE_POS );
#define TEST_LEAP_SECOND_DESERIALIZATION( expectedLeapSecond ) \
do { \
/* Call the API under test. */ \
TEST_ASSERT_EQUAL( SntpSuccess, Sntp_DeserializeResponse( &clientTime, \
&clientTime, \
testBuffer, \
sizeof( testBuffer ), \
&parsedData ) ); \
\
/* As the clock and server times are same, the clock offset, should be zero. */ \
TEST_ASSERT_EQUAL( 0, parsedData.clockOffsetMs ); \
\
/* Validate other fields in the output parameter. */ \
TEST_ASSERT_EQUAL( 0, memcmp( &parsedData.serverTime, &serverTime, sizeof( SntpTimestamp_t ) ) ); \
TEST_ASSERT_EQUAL( expectedLeapSecond, parsedData.leapSecondType ); \
TEST_ASSERT_EQUAL( SNTP_KISS_OF_DEATH_CODE_NONE, parsedData.rejectedResponseCode ); \
} while( 0 )
/* Update SNTP response packet to indicate an upcoming leap second insertion. */
testBuffer[ 0 ] = ( LastMinuteHas61Seconds << SNTP_PACKET_LEAP_INDICATOR_LSB ) |
SNTP_PACKET_VERSION_VAL | SNTP_PACKET_MODE_SERVER;
TEST_LEAP_SECOND_DESERIALIZATION( LastMinuteHas61Seconds );
/* Update SNTP response packet to indicate an upcoming leap second deletion. */
testBuffer[ 0 ] = ( LastMinuteHas59Seconds << SNTP_PACKET_LEAP_INDICATOR_LSB ) |
SNTP_PACKET_VERSION_VAL | SNTP_PACKET_MODE_SERVER;
TEST_LEAP_SECOND_DESERIALIZATION( LastMinuteHas59Seconds );
}
/**
* @brief Tests the @ref Sntp_CalculatePollInterval utility function returns
* error for invalid parameters passed to the API.
*/
void test_CalculatePollInterval_InvalidParams( void )
{
uint32_t pollInterval = 0;
/* Test with invalid clock frequency. */
TEST_ASSERT_EQUAL( SntpErrorBadParameter, Sntp_CalculatePollInterval( 0,
100,
&pollInterval ) );
/* Test with invalid desired accuracy. */
TEST_ASSERT_EQUAL( SntpErrorBadParameter, Sntp_CalculatePollInterval( 100,
0,
&pollInterval ) );
/* Test with invalid output parameter. */
TEST_ASSERT_EQUAL( SntpErrorBadParameter, Sntp_CalculatePollInterval( 100,
50,
NULL ) );
/* Test with parameters that cause poll interval value of less than 1 second. */
TEST_ASSERT_EQUAL( SntpZeroPollInterval, Sntp_CalculatePollInterval( 10000 /* High Error Clock. */,
1 /* High Accuracy Requirement */,
&pollInterval ) );
}
/**
* @brief Tests the @ref Sntp_CalculatePollInterval utility function calculates
* the poll interval period as the closes power of 2 value for achieving the
* desired clock accuracy.
*/
void test_CalculatePollInterval_Nominal( void )
{
uint32_t pollInterval = 0;
uint32_t expectedInterval = 0;
/* Test the SNTPv4 specification example of 200 PPM clock frequency and
* 1 minute of desired accuracy. */
expectedInterval = 0x00040000;
TEST_ASSERT_EQUAL( SntpSuccess, Sntp_CalculatePollInterval( 200 /* Clock Tolerance */,
1 /* minute */ * 60 * 1000 /* Desired Accuracy */,
&pollInterval ) );
TEST_ASSERT_EQUAL( expectedInterval, pollInterval );
/* Test another case where the exact poll interval for achieving desired frequency
* is an exponent of 2 value. For 512 seconds (or 2^9) poll interval, the maximum
* clock drift with 125 PPM is 125 * 512 = 64000 microseconds = 64 milliseconds. */
expectedInterval = 0x00000200;
TEST_ASSERT_EQUAL( SntpSuccess, Sntp_CalculatePollInterval( 125 /* Clock Tolerance (PPM) */,
64 /* Desired Accuracy (ms)*/,
&pollInterval ) );
/* Test for maximum possible value of calculated poll interval when the clock frequency
* tolerance is minimum (i.e. 1 PPM or high accuracy system clock ) but the desired accuracy
* is very low (i.e. largest value of 16 bit parameter as 65535 ms OR ~ 1 minute).
* This test proves that the 32-bit
* width of poll integer value can hold the largest calculation of poll interval value. */
expectedInterval = 0x02000000; /* 536,870,912 seconds OR ~ 17 years */
TEST_ASSERT_EQUAL( SntpSuccess, Sntp_CalculatePollInterval( 1 /* Clock Tolerance (PPM) */,
UINT16_MAX /* Desired Accuracy (ms)*/,
&pollInterval ) );
TEST_ASSERT_EQUAL( expectedInterval, pollInterval );
}
/**
* @brief Tests the @ref Sntp_ConvertToUnixTime utility function returns
* expected error when invalid parameters or unsupported timestamps are passed.
*/
void test_ConvertToUnixTime_InvalidParams( void )
{
SntpTimestamp_t sntpTime;
/* Use same memory for UNIX seconds and microseconds as we are not
* testing those values. */
uint32_t unixTime;
/* Test with NULL SNTP time. */
TEST_ASSERT_EQUAL( SntpErrorBadParameter, Sntp_ConvertToUnixTime( NULL,
&unixTime,
&unixTime ) );
/* Test with NULL output parameters. */
TEST_ASSERT_EQUAL( SntpErrorBadParameter, Sntp_ConvertToUnixTime( &sntpTime,
NULL,
&unixTime ) );
TEST_ASSERT_EQUAL( SntpErrorBadParameter, Sntp_ConvertToUnixTime( &sntpTime,
&unixTime,
NULL ) );
/* Test with time before UNIX epoch or 1st Jan 1970 .*/
sntpTime.seconds = SNTP_TIME_AT_UNIX_EPOCH_SECS - 5;
TEST_ASSERT_EQUAL( SntpErrorTimeNotSupported, Sntp_ConvertToUnixTime( &sntpTime,
&unixTime,
&unixTime ) );
/* Test with timestamp that after largest UNIX time for signed 32-bit integer systems
* (i.e. after 18 Jan 2036 3:14:07) */
sntpTime.seconds = SNTP_TIME_AT_LARGEST_UNIX_TIME_SECS + 5;
TEST_ASSERT_EQUAL( SntpErrorTimeNotSupported, Sntp_ConvertToUnixTime( &sntpTime,
&unixTime,
&unixTime ) );
}
/**
* @brief Tests the @ref Sntp_ConvertToUnixTime utility function returns
* expected error when invalid parameters or unsupported timestamps are passed.
*/
void test_ConvertToUnixTime_Nominal( void )
{
SntpTimestamp_t sntpTime = TEST_TIMESTAMP;
uint32_t unixTimeSecs;
uint32_t unixTimeMs;
#define TEST_SNTP_TO_UNIX_CONVERSION( sntpTimeSecs, sntpTimeFracs, \
expectedUnixTimeSecs, expectedUnixTimeMs ) \
do { \
/* Set the SNTP timestamps. */ \
sntpTime.seconds = sntpTimeSecs; \
sntpTime.fractions = sntpTimeFracs; \
\
/* Call API under test. */ \
TEST_ASSERT_EQUAL( SntpSuccess, Sntp_ConvertToUnixTime( &sntpTime, \
&unixTimeSecs, \
&unixTimeMs ) ); \
/* Validate the generated UNIX time. */ \
TEST_ASSERT_EQUAL( expectedUnixTimeSecs, unixTimeSecs ); \
TEST_ASSERT_EQUAL( expectedUnixTimeMs, unixTimeMs ); \
} while( 0 )
/* Test with SNTP time at UNIX epoch. .*/
TEST_SNTP_TO_UNIX_CONVERSION( SNTP_TIME_AT_UNIX_EPOCH_SECS, /* Sntp Seconds. */
0 /* Sntp Fractions. */,
0 /* Unix Seconds */,
0 /* Unix Microseconds */ );
/* Test with SNTP time in the range between UNIX epoch and Smallest SNTP time in Era 1 .*/
TEST_SNTP_TO_UNIX_CONVERSION( SNTP_TIME_AT_UNIX_EPOCH_SECS + 1000 /* Sntp Seconds. */,
500 /* Sntp Fractions. */,
1000 /* Unix Seconds */,
500 / SNTP_FRACTION_VALUE_PER_MICROSECOND /* Unix Microseconds */ );
/* Test with SNTP time at largest SNTP time in Era 0 .*/
TEST_SNTP_TO_UNIX_CONVERSION( UINT32_MAX /* Sntp Seconds. */,
0 /* Sntp Fractions. */,
UINT32_MAX - SNTP_TIME_AT_UNIX_EPOCH_SECS, /* Unix Seconds */
0 /* Unix Microseconds */ );
/* Test with SNTP time at smallest SNTP time in Era 1 .*/
TEST_SNTP_TO_UNIX_CONVERSION( UINT32_MAX + 1 /* Sntp Seconds. */,
0 /* Sntp Fractions. */,
UNIX_TIME_SECS_AT_SNTP_ERA_1_SMALLEST_TIME, /* Unix Seconds */
0 /* Unix Microseconds */ );
/* Test SNTP time in the range [SNTP Era 1 Epoch, 32-bit signed UNIX max time] .*/
TEST_SNTP_TO_UNIX_CONVERSION( UINT32_MAX + 1000 /* Sntp Seconds. */,
4000 /* Sntp Fractions. */,
UNIX_TIME_SECS_AT_SNTP_ERA_1_SMALLEST_TIME + 999, /* Unix Seconds */
4000 / SNTP_FRACTION_VALUE_PER_MICROSECOND /* Unix Microseconds */ );
/* Test with SNTP time that represents the 32-bit signed maximum UNIX time
* (i.e. at 19 Jan 2038 3:14:07 ) .*/
TEST_SNTP_TO_UNIX_CONVERSION( SNTP_TIME_AT_LARGEST_UNIX_TIME_SECS /* Sntp Seconds. */,
0 /* Sntp Fractions. */,
INT32_MAX, /* Unix Seconds */
0 /* Unix Microseconds */ );
}

38
arcs-sdk/modules/coresntp/test/unit-test/unity_build.cmake Normal file
View File

@@ -0,0 +1,38 @@
# Macro utility to clone the Unity submodule.
macro( clone_unity )
find_package( Git REQUIRED )
message( "Cloning submodule Unity." )
execute_process( COMMAND rm -rf ${UNITY_DIR}
COMMAND ${GIT_EXECUTABLE} submodule update --checkout --init --recursive ${UNITY_DIR}
WORKING_DIRECTORY ${PROJECT_SOURCE_DIR}
RESULT_VARIABLE UNITY_CLONE_RESULT )
if( NOT ${UNITY_CLONE_RESULT} STREQUAL "0" )
message( FATAL_ERROR "Failed to clone Unity submodule." )
endif()
endmacro()
# Macro utility to add library targets for Unity and Unity to build configuration.
macro( add_unity_targets )
# Build Configuration for Unity and Unity libraries.
list( APPEND UNITY_INCLUDE_DIRS
"${UNITY_DIR}/src/"
"${UNITY_DIR}/extras/fixture/src"
"${UNITY_DIR}/extras/memory/src"
)
add_library( unity STATIC
"${UNITY_DIR}/src/unity.c"
"${UNITY_DIR}/extras/fixture/src/unity_fixture.c"
"${UNITY_DIR}/extras/memory/src/unity_memory.c"
)
set_target_properties( unity PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib
POSITION_INDEPENDENT_CODE ON
)
target_include_directories( unity PUBLIC
${UNITY_INCLUDE_DIRS}
)
endmacro()