From 7f69232893203e6db91196f0d9bfbee27f5a196d Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Tue, 11 Oct 2022 15:26:00 -0400 Subject: [PATCH] Resolved VF parse error in pico sdk's `platform.h` and deleted stub. --- .../verifast/proof_setup/pico/README.md | 2 - .../verifast/proof_setup/pico/platform.h | 504 ------------------ verification/verifast/sdks/pico-sdk | 2 +- verification/verifast/start-vfide.sh | 2 +- 4 files changed, 2 insertions(+), 508 deletions(-) delete mode 100644 verification/verifast/proof_setup/pico/README.md delete mode 100644 verification/verifast/proof_setup/pico/platform.h diff --git a/verification/verifast/proof_setup/pico/README.md b/verification/verifast/proof_setup/pico/README.md deleted file mode 100644 index 9f7c7f9c3..000000000 --- a/verification/verifast/proof_setup/pico/README.md +++ /dev/null @@ -1,2 +0,0 @@ -This directory contains files that originally resided in: -`$PICO_SDK_PATH/src/rp2_common/pico_platform/include/pico` diff --git a/verification/verifast/proof_setup/pico/platform.h b/verification/verifast/proof_setup/pico/platform.h deleted file mode 100644 index 213446f7b..000000000 --- a/verification/verifast/proof_setup/pico/platform.h +++ /dev/null @@ -1,504 +0,0 @@ -/* This is a stub used for the VeriFast proof. */ -/* - * Copyright (c) 2020 Raspberry Pi (Trading) Ltd. - * - * SPDX-License-Identifier: BSD-3-Clause - */ - -#ifndef _PICO_PLATFORM_H_ -#define _PICO_PLATFORM_H_ - -/** \file platform.h - * \defgroup pico_platform pico_platform - * - * Macros and definitions (and functions when included by non assembly code) for the RP2 family device / architecture - * to provide a common abstraction over low level compiler / platform specifics. - * - * This header may be included by assembly code - */ - -#include "hardware/platform_defs.h" -#include "hardware/regs/addressmap.h" -#include "hardware/regs/sio.h" - -// Marker for builds targeting the RP2040 -#define PICO_RP2040 1 - -// PICO_CONFIG: PICO_STACK_SIZE, Stack Size, min=0x100, default=0x800, advanced=true, group=pico_platform -#ifndef PICO_STACK_SIZE -#define PICO_STACK_SIZE _u(0x800) -#endif - -// PICO_CONFIG: PICO_HEAP_SIZE, Heap size to reserve, min=0x100, default=0x800, advanced=true, group=pico_platform -#ifndef PICO_HEAP_SIZE -#define PICO_HEAP_SIZE _u(0x800) -#endif - -// PICO_CONFIG: PICO_NO_RAM_VECTOR_TABLE, Enable/disable the RAM vector table, type=bool, default=0, advanced=true, group=pico_platform -#ifndef PICO_NO_RAM_VECTOR_TABLE -#define PICO_NO_RAM_VECTOR_TABLE 0 -#endif - -// PICO_CONFIG: PICO_RP2040_B0_SUPPORTED, Whether to include any specific software support for RP2040 B0 revision, type=bool, default=1, advanced=true, group=pico_platform -#ifndef PICO_RP2040_B0_SUPPORTED -#define PICO_RP2040_B0_SUPPORTED 1 -#endif - -// PICO_CONFIG: PICO_FLOAT_SUPPORT_ROM_V1, Include float support code for RP2040 B0 when that chip revision is supported , type=bool, default=1, advanced=true, group=pico_platform -#ifndef PICO_FLOAT_SUPPORT_ROM_V1 -#define PICO_FLOAT_SUPPORT_ROM_V1 1 -#endif - -// PICO_CONFIG: PICO_DOUBLE_SUPPORT_ROM_V1, Include double support code for RP2040 B0 when that chip revision is supported , type=bool, default=1, advanced=true, group=pico_platform -#ifndef PICO_DOUBLE_SUPPORT_ROM_V1 -#define PICO_DOUBLE_SUPPORT_ROM_V1 1 -#endif - - -// PICO_CONFIG: PICO_RP2040_B1_SUPPORTED, Whether to include any specific software support for RP2040 B1 revision, type=bool, default=1, advanced=true, group=pico_platform -#ifndef PICO_RP2040_B1_SUPPORTED -#define PICO_RP2040_B1_SUPPORTED 1 -#endif - -// PICO_CONFIG: PICO_RP2040_B2_SUPPORTED, Whether to include any specific software support for RP2040 B2 revision, type=bool, default=1, advanced=true, group=pico_platform -#ifndef PICO_RP2040_B2_SUPPORTED -#define PICO_RP2040_B2_SUPPORTED 1 -#endif - -// --- remainder of file is not included by assembly code --- - -#ifndef __ASSEMBLER__ - -#include -#include "pico/types.h" - -#ifdef __cplusplus -extern "C" { -#endif - -/*! \brief Marker for an interrupt handler - * \ingroup pico_platform - * For example an IRQ handler function called my_interrupt_handler: - * - * void __isr my_interrupt_handler(void) { - */ -#define __isr - -/*! \brief Section attribute macro for placement in RAM after the `.data` section - * \ingroup pico_platform - * - * For example a 400 element `uint32_t` array placed after the .data section - * - * uint32_t __after_data("my_group_name") a_big_array[400]; - * - * The section attribute is `.after_data.` - * - * \param group a string suffix to use in the section name to distinguish groups that can be linker - * garbage-collected independently - */ -#define __after_data(group) __attribute__((section(".after_data." group))) - -/*! \brief Section attribute macro for placement not in flash (i.e in RAM) - * \ingroup pico_platform - * - * For example a 3 element `uint32_t` array placed in RAM (even though it is `static const`) - * - * static const uint32_t __not_in_flash("my_group_name") an_array[3]; - * - * The section attribute is `.time_critical.` - * - * \param group a string suffix to use in the section name to distinguish groups that can be linker - * garbage-collected independently - */ -#define __not_in_flash(group) __attribute__((section(".time_critical." group))) - -/*! \brief Section attribute macro for placement in the SRAM bank 4 (known as "scratch X") - * \ingroup pico_platform - * - * Scratch X is commonly used for critical data and functions accessed only by one core (when only - * one core is accessing the RAM bank, there is no opportunity for stalls) - * - * For example a `uint32_t` variable placed in "scratch X" - * - * uint32_t __scratch_x("my_group_name") foo = 23; - * - * The section attribute is `.scratch_x.` - * - * \param group a string suffix to use in the section name to distinguish groups that can be linker - * garbage-collected independently - */ -#define __scratch_x(group) __attribute__((section(".scratch_x." group))) - -/*! \brief Section attribute macro for placement in the SRAM bank 5 (known as "scratch Y") - * \ingroup pico_platform - * - * Scratch Y is commonly used for critical data and functions accessed only by one core (when only - * one core is accessing the RAM bank, there is no opportunity for stalls) - * - * For example a `uint32_t` variable placed in "scratch Y" - * - * uint32_t __scratch_y("my_group_name") foo = 23; - * - * The section attribute is `.scratch_y.` - * - * \param group a string suffix to use in the section name to distinguish groups that can be linker - * garbage-collected independently - */ -#define __scratch_y(group) __attribute__((section(".scratch_y." group))) - -/*! \brief Section attribute macro for data that is to be left uninitialized - * \ingroup pico_platform - * - * Data marked this way will retain its value across a reset (normally uninitialized data - in the .bss - * section) is initialized to zero during runtime initialization - * - * For example a `uint32_t` foo that will retain its value if the program is restarted by reset. - * - * uint32_t __uninitialized_ram("my_group_name") foo; - * - * The section attribute is `.uninitialized_ram.` - * - * \param group a string suffix to use in the section name to distinguish groups that can be linker - * garbage-collected independently - */ -#define __uninitialized_ram(group) __attribute__((section(".uninitialized_ram." #group))) group - -/*! \brief Section attribute macro for placement in flash even in a COPY_TO_RAM binary - * \ingroup pico_platform - * - * For example a `uint32_t` variable explicitly placed in flash (it will hard fault if you attempt to write it!) - * - * uint32_t __in_flash("my_group_name") foo = 23; - * - * The section attribute is `.flashdata.` - * - * \param group a string suffix to use in the section name to distinguish groups that can be linker - * garbage-collected independently - */ -#define __in_flash(group) __attribute__((section(".flashdata" group))) - -/*! \brief Indicates a function should not be stored in flash - * \ingroup pico_platform - * - * Decorates a function name, such that the function will execute from RAM (assuming it is not inlined - * into a flash function by the compiler) - * - * For example a function called my_func taking an int parameter: - * - * void __not_in_flash_func(my_func)(int some_arg) { - * - * The function is placed in the `.time_critical.` linker section - * - * \see __no_inline_not_in_flash_func - */ -#define __not_in_flash_func(func_name) __not_in_flash(__STRING(func_name)) func_name - -/*! \brief Indicates a function is time/latency critical and should not run from flash - * \ingroup pico_platform - * - * Decorates a function name, such that the function will execute from RAM (assuming it is not inlined - * into a flash function by the compiler) to avoid possible flash latency. Currently this macro is identical - * in implementation to `__not_in_flash_func`, however the semantics are distinct and a `__time_critical_func` - * may in the future be treated more specially to reduce the overhead when calling such function from a flash - * function. - * - * For example a function called my_func taking an int parameter: - * - * void __time_critical(my_func)(int some_arg) { - * - * The function is placed in the `.time_critical.` linker section - * - * \see __not_in_flash_func - */ -#define __time_critical_func(func_name) __not_in_flash_func(func_name) - -/*! \brief Indicate a function should not be stored in flash and should not be inlined - * \ingroup pico_platform - * - * Decorates a function name, such that the function will execute from RAM, explicitly marking it as - * noinline to prevent it being inlined into a flash function by the compiler - * - * For example a function called my_func taking an int parameter: - * - * void __no_inline_not_in_flash_func(my_func)(int some_arg) { - * - * The function is placed in the `.time_critical.` linker section - */ -#define __no_inline_not_in_flash_func(func_name) __noinline __not_in_flash_func(func_name) - -#define __packed_aligned __packed __aligned(4) - -#ifdef VERIFAST_PROOF - /* Reason for rewrite: - * VeriFast cannot handle defines for `__force_inline`. - */ -#else - /*! \brief Attribute to force inlining of a function regardless of optimization level - * \ingroup pico_platform - * - * For example my_function here will always be inlined: - * - * int __force_inline my_function(int x) { - * - */ - #if defined(__GNUC__) && (__GNUC__ <= 6 || (__GNUC__ == 7 && (__GNUC_MINOR__ < 3 || !defined(__cplusplus)))) - #define __force_inline inline __always_inline - #else - #define __force_inline __always_inline - #endif -#endif /* VERIFAST_PROOF */ - -/*! \brief Macro to determine the number of elements in an array - * \ingroup pico_platform - */ -#ifndef count_of -#define count_of(a) (sizeof(a)/sizeof((a)[0])) -#endif - -/*! \brief Macro to return the maximum of two comparable values - * \ingroup pico_platform - */ -#ifndef MAX -#define MAX(a, b) ((a)>(b)?(a):(b)) -#endif - -/*! \brief Macro to return the minimum of two comparable values - * \ingroup pico_platform - */ -#ifndef MIN -#define MIN(a, b) ((b)>(a)?(a):(b)) -#endif - -/*! \brief Execute a breakpoint instruction - * \ingroup pico_platform - */ -static inline void __breakpoint(void) { - __asm__("bkpt #0"); -} - -/*! \brief Ensure that the compiler does not move memory access across this method call - * \ingroup pico_platform - * - * For example in the following code: - * - * *some_memory_location = var_a; - * __compiler_memory_barrier(); - * uint32_t var_b = *some_other_memory_location - * - * The compiler will not move the load from `some_other_memory_location` above the memory barrier (which it otherwise - * might - even above the memory store!) - */ -#ifdef VERIFAST_PROOF - /* Reason for rewrite: VeriFast cannot parse: - * - `__force_inline` - * - the function body - */ - static void __compiler_memory_barrier(void); -#else - __force_inline static void __compiler_memory_barrier(void) { - __asm__ volatile ("" : : : "memory"); - } -#endif - - -/*! \brief Macro for converting memory addresses to 32 bit addresses suitable for DMA - * \ingroup pico_platform - * - * This is just a cast to `uintptr_t` on the RP2040, however you may want to use this when developing code - * that also runs in "host" mode. If the host mode is 64 bit and you are embedding data pointers - * in other data (e.g. DMA chaining), then there is a need in "host" mode to convert a 64 bit native - * pointer to a 32 bit value for storage, which can be done using this macro. - */ -#define host_safe_hw_ptr(x) ((uintptr_t)(x)) -#define native_safe_hw_ptr(x) host_safe_hw_ptr(x) - - -/*! \brief Panics with the message "Unsupported" - * \ingroup pico_platform - * \see panic - */ -#ifdef VERIFAST_PROOF - /* Reason for rewrite: VeriFast cannot parse `__attribute__((noreturn))`. */ - void panic_unsupported(void); -#else - void __attribute__((noreturn)) panic_unsupported(void); -#endif - -/*! \brief Displays a panic message and halts execution - * \ingroup pico_platform - * - * An attempt is made to output the message to all registered STDOUT drivers - * after which this method executes a BKPT instruction. - * - * @param fmt format string (printf-like) - * @param ... printf-like arguments - */ -#ifdef VERIFAST_PROOF - /* Reason for rewrite: VeriFast cannot parse `__attribute__((noreturn))`. */ - void panic(const char *fmt, ...); -#else - void __attribute__((noreturn)) panic(const char *fmt, ...); -#endif - -// PICO_CONFIG: PICO_NO_FPGA_CHECK, Remove the FPGA platform check for small code size reduction, type=bool, default=0, advanced=true, group=pico_runtime -#ifndef PICO_NO_FPGA_CHECK -#define PICO_NO_FPGA_CHECK 0 -#endif - -#if PICO_NO_FPGA_CHECK -static inline bool running_on_fpga(void) {return false;} -#else -bool running_on_fpga(void); -#endif - -/*! \brief Returns the RP2040 chip revision number - * \ingroup pico_platform - * @return the RP2040 chip revision number (1 for B0/B1, 2 for B2) - */ -uint8_t rp2040_chip_version(void); - -/*! \brief Returns the RP2040 rom version number - * \ingroup pico_platform - * @return the RP2040 rom version number (1 for RP2040-B0, 2 for RP2040-B1, 3 for RP2040-B2) - */ -static inline uint8_t rp2040_rom_version(void) { - #ifdef VERIFAST_PROOF - /* Reason for rewrite: VeriFast cannot parse GCC pragmas */ - return *(uint8_t*)0x13; - #else - #pragma GCC diagnostic push - #pragma GCC diagnostic ignored "-Warray-bounds" - return *(uint8_t*)0x13; - #pragma GCC diagnostic pop - #endif /* VERIFAST_PROOF */ -} - -/*! \brief No-op function for the body of tight loops - * \ingroup pico_platform - * - * No-op function intended to be called by any tight hardware polling loop. Using this ubiquitously - * makes it much easier to find tight loops, but also in the future \#ifdef-ed support for lockup - * debugging might be added - */ -#ifdef VERIFAST_PROOF - /* Reason for rewrite: VeriFast cannot parse `__force_inline`. */ - static void tight_loop_contents(void) {} -#else - static __force_inline void tight_loop_contents(void) {} -#endif /* VERIFAST_PROOF */ - - -/*! \brief Multiply two integers using an assembly `MUL` instruction - * \ingroup pico_platform - * - * This multiplies a by b using multiply instruction using the ARM mul instruction regardless of values (the compiler - * might otherwise choose to perform shifts/adds), i.e. this is a 1 cycle operation. - * - * \param a the first operand - * \param b the second operand - * \return a * b - */ -#ifdef VERIFAST_PROOF - /* Reason for rewrite: VeriFast cannot parse: - * - `__force_inline` - * - function body - */ - static int32_t __mul_instruction(int32_t a, int32_t b); -#else - __force_inline static int32_t __mul_instruction(int32_t a, int32_t b) { - asm ("mul %0, %1" : "+l" (a) : "l" (b) : ); - return a; - } -#endif /* VERIFAST_PROOF */ - -/*! \brief multiply two integer values using the fastest method possible - * \ingroup pico_platform - * - * Efficiently multiplies value a by possibly constant value b. - * - * If b is known to be constant and not zero or a power of 2, then a mul instruction is used rather than gcc's default - * which is often a slow combination of shifts and adds. If b is a power of 2 then a single shift is of course preferable - * and will be used - * - * \param a the first operand - * \param b the second operand - * \return a * b - */ -#define __fast_mul(a, b) __builtin_choose_expr(__builtin_constant_p(b) && !__builtin_constant_p(a), \ -(__builtin_popcount(b) >= 2 ? __mul_instruction(a,b) : (a)*(b)), \ -(a)*(b)) - -/*! \brief Utility macro to assert two types are equivalent. - * \ingroup pico_platform - * - * This macro can be useful in other macros along with `typeof` to assert that two parameters are of equivalent type - * (or that a single parameter is of an expected type) - */ -#define __check_type_compatible(type_a, type_b) static_assert(__builtin_types_compatible_p(type_a, type_b), __STRING(type_a) " is not compatible with " __STRING(type_b)); - -/*! \brief Get the current exception level on this core - * \ingroup pico_platform - * - * \return the exception number if the CPU is handling an exception, or 0 otherwise - */ -uint __get_current_exception(void); - -#define WRAPPER_FUNC(x) __wrap_ ## x -#define REAL_FUNC(x) __real_ ## x - -#ifdef __cplusplus -} -#endif - -/*! \brief Helper method to busy-wait for at least the given number of cycles - * \ingroup pico_platform - * - * This method is useful for introducing very short delays. - * - * This method busy-waits in a tight loop for the given number of system clock cycles. The total wait time is only accurate to within 2 cycles, - * and this method uses a loop counter rather than a hardware timer, so the method will always take longer than expected if an - * interrupt is handled on the calling core during the busy-wait; you can of course disable interrupts to prevent this. - * - * You can use \ref clock_get_hz(clk_sys) to determine the number of clock cycles per second if you want to convert an actual - * time duration to a number of cycles. - * - * \param minimum_cycles the minimum number of system clock cycles to delay for - */ -#ifdef VERIFAST_PROOF - /* Reason for rewrite: VeriFast cannot parse function body. */ - static inline void busy_wait_at_least_cycles(uint32_t minimum_cycles); -#else - static inline void busy_wait_at_least_cycles(uint32_t minimum_cycles) { - __asm volatile ( - ".syntax unified\n" - "1: subs %0, #3\n" - "bcs 1b\n" - : "+r" (minimum_cycles) : : "memory" - ); - } -#endif /* VERIFAST_PROOF */ - -/*! \brief Get the current core number - * \ingroup pico_platform - * - * \return The core number the call was made from - */ -#ifdef VERIFAST_PROOF - /* Reason for rewrite: VeriFast cannot parse `__force_inline`. */ - static uint get_core_num(void) -#else - __force_inline static uint get_core_num(void) -#endif /* VERIFAST_PROOF */ -{ - return (*(uint32_t *) (SIO_BASE + SIO_CPUID_OFFSET)); -} - -#else // __ASSEMBLER__ - -#define WRAPPER_FUNC_NAME(x) __wrap_##x -#define SECTION_NAME(x) .text.##x -#define RAM_SECTION_NAME(x) .time_critical.##x - -#endif // !__ASSEMBLER__ - -#endif diff --git a/verification/verifast/sdks/pico-sdk b/verification/verifast/sdks/pico-sdk index 2e6142b15..0c8802074 160000 --- a/verification/verifast/sdks/pico-sdk +++ b/verification/verifast/sdks/pico-sdk @@ -1 +1 @@ -Subproject commit 2e6142b15b8a75c1227dd3edbe839193b2bf9041 +Subproject commit 0c8802074d519ed0354400d85113c98618277c8b diff --git a/verification/verifast/start-vfide.sh b/verification/verifast/start-vfide.sh index 05137be8b..ba01278cc 100755 --- a/verification/verifast/start-vfide.sh +++ b/verification/verifast/start-vfide.sh @@ -80,7 +80,7 @@ PICO_SDK_DIR="sdks/pico-sdk" -I $PICO_SDK_DIR/src/rp2_common/pico_unique_id/include \ -I $PICO_SDK_DIR/src/rp2_common/hardware_flash/include \ -I $PICO_SDK_DIR/src/common/pico_usb_reset_interface/include \ - +-I $PICO_SDK_DIR/src/rp2_common/pico_platform/include/ # Defines used during the built of the FreeRTOS SMP Demo that might be relevant # in the future: