From 3e9f06ed64abb76f0eefa931507edeb1368ecb50 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Thu, 5 Jan 2023 15:49:07 -0500 Subject: [PATCH] Deleted submodule pointing to pico sdk and added copies of the pico headers relevant for our proof. We had to modify the headers such that VeriFast can parse them. --- .gitmodules | 4 - .../smp/tasks/vTaskSwitchContext/README.md | 10 +- .../tasks/vTaskSwitchContext/pico-sdk/pico.h | 34 +++++++ .../vTaskSwitchContext/pico-sdk/pico/types.h | 94 +++++++++++++++++++ .../preprocessing_scripts/pp_flags.sh | 39 +------- .../tasks/vTaskSwitchContext/sdks/pico-sdk | 1 - 6 files changed, 133 insertions(+), 49 deletions(-) create mode 100644 FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/pico-sdk/pico.h create mode 100644 FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/pico-sdk/pico/types.h delete mode 160000 FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/sdks/pico-sdk diff --git a/.gitmodules b/.gitmodules index 63eb65be52..88ad6e43c3 100644 --- a/.gitmodules +++ b/.gitmodules @@ -76,7 +76,3 @@ [submodule "FreeRTOS-Plus/Source/FreeRTOS-Cellular-Modules/sara-r4"] path = FreeRTOS-Plus/Source/FreeRTOS-Cellular-Modules/sara-r4 url = https://github.com/FreeRTOS/Lab-FreeRTOS-Cellular-Interface-Reference-ublox-SARA-R4.git -[submodule "FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/sdks/pico-sdk.git"] - path = FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/sdks/pico-sdk - url = https://github.com/Tobias-internship-AWS-2022/pico-sdk.git - branch = verifast diff --git a/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/README.md b/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/README.md index b3fa71a50e..a972fc5768 100644 --- a/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/README.md +++ b/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/README.md @@ -168,12 +168,10 @@ FreeRTOS/FreeRTOS │ Contains config files for the proof. The proof assumes a setup for │ RP2040. │ - ├── sdks/pico-sdk - │ Contains the Pico sdk referenced by the proof setup. - │ Some files are annotated with VeriFast contracts. Further, they contain - │ code VeriFast cannot parse and that we had to adapt. Hence, we currently - │ use a fork of the Pico sdk repository until the corresponding VeriFast - │ issues have been fixed. + ├── pico-sdk + │ Contains headers from the Pico sdk referenced by the proof setup. + │ Some files contain parts we had to rewrite so that VeriFast would parse + │ them. │ ├── src │ Contains the source files used by our proof. diff --git a/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/pico-sdk/pico.h b/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/pico-sdk/pico.h new file mode 100644 index 0000000000..784566e032 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/pico-sdk/pico.h @@ -0,0 +1,34 @@ +/* + * Copyright (c) 2020 Raspberry Pi (Trading) Ltd. + * + * SPDX-License-Identifier: BSD-3-Clause + */ + +#ifndef PICO_H_ +#define PICO_H_ + +/** \file pico.h + * \defgroup pico_base pico_base + * + * Core types and macros for the Raspberry Pi Pico SDK. This header is intended to be included by all source code + * as it includes configuration headers and overrides in the correct order + * + * This header may be included by assembly code +*/ + +#define __PICO_STRING(x) #x +#define __PICO_XSTRING(x) __PICO_STRING(x) + +#include "pico/types.h" +#include "pico/version.h" + +// PICO_CONFIG: PICO_CONFIG_HEADER, unquoted path to header include in place of the default pico/config.h which may be desirable for build systems which can't easily generate the config_autogen header, group=pico_base +#ifdef PICO_CONFIG_HEADER +#include __PICO_XSTRING(PICO_CONFIG_HEADER) +#else +#include "pico/config.h" +#endif +#include "pico/platform.h" +#include "pico/error.h" + +#endif diff --git a/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/pico-sdk/pico/types.h b/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/pico-sdk/pico/types.h new file mode 100644 index 0000000000..8e1627ca81 --- /dev/null +++ b/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/pico-sdk/pico/types.h @@ -0,0 +1,94 @@ +/* + * Copyright (c) 2020 Raspberry Pi (Trading) Ltd. + * + * SPDX-License-Identifier: BSD-3-Clause + */ + +#ifndef _PICO_TYPES_H +#define _PICO_TYPES_H + +#ifndef __ASSEMBLER__ + +#include "pico/assert.h" + +#include +#include +#include + +typedef unsigned int uint; + +/*! \typedef absolute_time_t + \brief An opaque 64 bit timestamp in microseconds + + The type is used instead of a raw uint64_t to prevent accidentally passing relative times or times in the wrong + time units where an absolute time is required. It is equivalent to uint64_t in release builds. + + \see to_us_since_boot() + \see update_us_since_boot() + \ingroup timestamp +*/ +#ifdef NDEBUG +typedef uint64_t absolute_time_t; +#else +typedef struct { + uint64_t _private_us_since_boot; +} absolute_time_t; +#endif + +/*! fn to_us_since_boot + * \brief convert an absolute_time_t into a number of microseconds since boot. + * \param t the absolute time to convert + * \return a number of microseconds since boot, equivalent to t + * \ingroup timestamp + */ +static inline uint64_t to_us_since_boot(absolute_time_t t) { +#ifdef NDEBUG + return t; +#else + return t._private_us_since_boot; +#endif +} + +/*! fn update_us_since_boot + * \brief update an absolute_time_t value to represent a given number of microseconds since boot + * \param t the absolute time value to update + * \param us_since_boot the number of microseconds since boot to represent. Note this should be representable + * as a signed 64 bit integer + * \ingroup timestamp + */ +static inline void update_us_since_boot(absolute_time_t *t, uint64_t us_since_boot) { +#ifdef NDEBUG + *t = us_since_boot; +#else + assert(us_since_boot <= INT64_MAX); + t->_private_us_since_boot = us_since_boot; +#endif +} + +#ifdef NDEBUG +#define ABSOLUTE_TIME_INITIALIZED_VAR(name, value) name = value +#else +#define ABSOLUTE_TIME_INITIALIZED_VAR(name, value) name = {value} +#endif + +/** \struct datetime_t + * \ingroup util_datetime + * \brief Structure containing date and time information + * + * When setting an RTC alarm, set a field to -1 tells + * the RTC to not match on this field + */ +typedef struct { + int16_t year; ///< 0..4095 + int8_t month; ///< 1..12, 1 is January + int8_t day; ///< 1..28,29,30,31 depending on month + int8_t dotw; ///< 0..6, 0 is Sunday + int8_t hour; ///< 0..23 + int8_t min; ///< 0..59 + int8_t sec; ///< 0..59 +} datetime_t; + +#define bool_to_bit(x) ((uint)!!(x)) + +#endif +#endif diff --git a/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/preprocessing_scripts/pp_flags.sh b/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/preprocessing_scripts/pp_flags.sh index 63be7c7c85..6d9fb6792b 100755 --- a/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/preprocessing_scripts/pp_flags.sh +++ b/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/preprocessing_scripts/pp_flags.sh @@ -74,44 +74,7 @@ BUILD_FLAGS=( declare -a PICO_INCLUDE_FLAGS PICO_INCLUDE_FLAGS=( - -I"$PICO_SDK_DIR/src/boards/include" - -I"$PICO_SDK_DIR/src/common/pico_base/include" - -I"$PICO_SDK_DIR/src/common/pico_binary_info/include" - -I"$PICO_SDK_DIR/src/common/pico_bit_ops/include" - -I"$PICO_SDK_DIR/src/common/pico_divider/include" - -I"$PICO_SDK_DIR/src/common/pico_stdlib/include" - -I"$PICO_SDK_DIR/src/common/pico_sync/include" - -I"$PICO_SDK_DIR/src/common/pico_time/include" - -I"$PICO_SDK_DIR/src/common/pico_util/include" - -I"$PICO_SDK_DIR/src/rp2040/hardware_regs/include" - -I"$PICO_SDK_DIR/src/rp2040/hardware_structs/include" - -I"$PICO_SDK_DIR/src/rp2_common/boot_stage2/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_base/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_claim/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_clocks/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_divider/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_exception/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_gpio/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_irq/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_pll/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_resets/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_sync/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_timer/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_uart/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_vreg/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_watchdog/include" - -I"$PICO_SDK_DIR/src/rp2_common/hardware_xosc/include" - -I"$PICO_SDK_DIR/src/rp2_common/pico_bootrom/include" - -I"$PICO_SDK_DIR/src/rp2_common/pico_double/include" - -I"$PICO_SDK_DIR/src/rp2_common/pico_float/include" - -I"$PICO_SDK_DIR/src/rp2_common/pico_int64_ops/include" - -I"$PICO_SDK_DIR/src/rp2_common/pico_malloc/include" - -I"$PICO_SDK_DIR/src/rp2_common/pico_multicore/include" - -I"$PICO_SDK_DIR/src/rp2_common/pico_platform/include" - -I"$PICO_SDK_DIR/src/rp2_common/pico_printf/include" - -I"$PICO_SDK_DIR/src/rp2_common/pico_runtime/include" - -I"$PICO_SDK_DIR/src/rp2_common/pico_stdio/include" - -I"$PICO_SDK_DIR/src/rp2_common/pico_stdio_uart/include" + -I"pico-sdk" ) declare -a RP2040_INCLUDE_FLAGS diff --git a/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/sdks/pico-sdk b/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/sdks/pico-sdk deleted file mode 160000 index 780173e22f..0000000000 --- a/FreeRTOS/Test/VeriFast/smp/tasks/vTaskSwitchContext/sdks/pico-sdk +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 780173e22f197ec7481001f45a5daa1ae5d1788a