From 541e671569de83e1450657a24c4a6266cb84ff64 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Tue, 13 Dec 2022 10:34:14 -0500 Subject: [PATCH] Deleted deprecated proofs. --- .../proof/ready_list_predicates.h | 2 - .../proof/snippets/rp2040_port_c_snippets.c | 242 ------------------ .../proof/verifast_bitops_extended.h | 11 - .../proof/verifast_prelude_extended.h | 107 -------- .../tasks/vTaskSwitchContext/src/tasks.c | 4 - 5 files changed, 366 deletions(-) delete mode 100644 Test/VeriFast/tasks/vTaskSwitchContext/proof/snippets/rp2040_port_c_snippets.c delete mode 100644 Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_bitops_extended.h delete mode 100644 Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_prelude_extended.h diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h index ac971fe62..41a04b484 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h @@ -8,8 +8,6 @@ /*@ -// TODO: We know that the list of priority 0 is never empty. -// It contains the idle task and nothing else. predicate readyLists_p(list > gCellLists, list > gOwnerLists) = configMAX_PRIORITIES == length(gCellLists) &*& diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/snippets/rp2040_port_c_snippets.c b/Test/VeriFast/tasks/vTaskSwitchContext/proof/snippets/rp2040_port_c_snippets.c deleted file mode 100644 index d38993779..000000000 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/snippets/rp2040_port_c_snippets.c +++ /dev/null @@ -1,242 +0,0 @@ -/* - * This file contains code snippets from: - * portable/ThirdParty/GCC/RP2040/port.c - */ - - - -// Note currently we support configNUM_CORES == 1 with SMP, thought it isn't 100% clear why you wouldn't -// just use the non SMP version; keeping around for now in case the code bases are merged. -#define portRUNNING_ON_BOTH_CORES (configNUM_CORES == portMAX_CORE_COUNT) - -/* Constants required to manipulate the NVIC. */ -#define portNVIC_SYSTICK_CTRL_REG ( *( ( volatile uint32_t * ) 0xe000e010 ) ) -#define portNVIC_SYSTICK_LOAD_REG ( *( ( volatile uint32_t * ) 0xe000e014 ) ) -#define portNVIC_SYSTICK_CURRENT_VALUE_REG ( *( ( volatile uint32_t * ) 0xe000e018 ) ) -#define portNVIC_INT_CTRL_REG ( *( ( volatile uint32_t * ) 0xe000ed04 ) ) -#define portNVIC_SHPR3_REG ( *( ( volatile uint32_t * ) 0xe000ed20 ) ) -#define portNVIC_SYSTICK_CLK_BIT ( 1UL << 2UL ) -#define portNVIC_SYSTICK_INT_BIT ( 1UL << 1UL ) -#define portNVIC_SYSTICK_ENABLE_BIT ( 1UL << 0UL ) -#define portNVIC_SYSTICK_COUNT_FLAG_BIT ( 1UL << 16UL ) -#define portNVIC_PENDSVSET_BIT ( 1UL << 28UL ) -#define portMIN_INTERRUPT_PRIORITY ( 255UL ) -#define portNVIC_PENDSV_PRI ( portMIN_INTERRUPT_PRIORITY << 16UL ) -#define portNVIC_SYSTICK_PRI ( portMIN_INTERRUPT_PRIORITY << 24UL ) - -/* Constants required to set up the initial stack. */ -#define portINITIAL_XPSR ( 0x01000000 ) - -/* The systick is a 24-bit counter. */ -#define portMAX_24_BIT_NUMBER ( 0xffffffUL ) - -/* A fiddle factor to estimate the number of SysTick counts that would have - * occurred while the SysTick counter is stopped during tickless idle - * calculations. */ -#ifndef portMISSED_COUNTS_FACTOR - #define portMISSED_COUNTS_FACTOR ( 45UL ) -#endif - -/* Let the user override the pre-loading of the initial LR with the address of - * prvTaskExitError() in case it messes up unwinding of the stack in the - * debugger. */ -#ifdef configTASK_RETURN_ADDRESS - #define portTASK_RETURN_ADDRESS configTASK_RETURN_ADDRESS -#else - #define portTASK_RETURN_ADDRESS prvTaskExitError -#endif - -/* - * Setup the timer to generate the tick interrupts. The implementation in this - * file is weak to allow application writers to change the timer used to - * generate the tick interrupt. - */ -void vPortSetupTimerInterrupt( void ); - -/* - * Exception handlers. - */ -void xPortPendSVHandler( void ) __attribute__( ( naked ) ); -void xPortSysTickHandler( void ); -void vPortSVCHandler( void ); - -/* - * Start first task is a separate function so it can be tested in isolation. - */ -static void vPortStartFirstTask( void ) __attribute__( ( naked ) ); - -/* - * Used to catch tasks that attempt to return from their implementing function. - */ -static void prvTaskExitError( void ); - - - - -// ------------------------------------------------- -// Validate stack predicate - -/* Simulates creation and initialisation of a stack that grows down as on RP2040. - */ -StackType_t* test_stack_pred(uint32_t depth) -/*@ requires depth * sizeof(StackType_t) <= UINTPTR_MAX &*& - depth <= UINT_MAX &*& - depth > 0; - @*/ -/*@ ensures result == 0 ? true : stack_p(result, depth, ?top, depth) &*& - malloc_block_chars((char*) result, depth * sizeof(StackType_t)); -@*/ -{ - // Proof boken by switch to nightly build Nov 14, 2022 - // TODO: Adapt proof - //@ assume(false); - // ------------------------------------------------------------ - StackType_t * stack; - - - /* Allocate space for the stack used by the task being created. */ - stack = (StackType_t*) malloc( ( ( ( size_t ) depth ) * sizeof( StackType_t ) ) ); - if(stack == 0) return 0; - - memset(stack, 0, (unsigned int ) depth * sizeof(StackType_t)); - - StackType_t* top = stack + depth -1; - - //@ chars_to_integers_(stack, sizeof(StackType_t), false, depth); - //@ close stack_p(stack, depth, top, depth); - // integers_(stack0, 4, false, depth, _) - return stack; -} -// ------------------------------------------------- - -/* - * See header file for description. - */ -StackType_t * pxPortInitialiseStack( StackType_t * pxTopOfStack, - TaskFunction_t pxCode, - void * pvParameters ) -/*@ requires pxTopOfStack > 0 &*& - stack_p_2(?pxStack, ?ulStackDepth, pxTopOfStack, ?ulFreeBytes, - ?ulUsedCells, ?ulUnalignedBytes) &*& - ulFreeBytes > 17 * sizeof(StackType_t) &*& - pxStack > 0; - @*/ -/*@ ensures stack_p_2(pxStack, ulStackDepth, result, - ulFreeBytes - sizeof(StackType_t) * 16, - ulUsedCells + 16, - ulUnalignedBytes) &*& - result == pxTopOfStack - 16; -@*/ -{ - // Proof boken by switch to nightly build Nov 14, 2022 - // TODO: Adapt proof - //@ assume(false); - // ------------------------------------------------------------ - - //@ StackType_t* gOldTop = pxTopOfStack; - //@ char* gcStack = (char*) pxStack; - //@ open stack_p_2(_, _, _, _, _, _); - - //@ assert( (char*) pxTopOfStack == (char*) pxStack + ulFreeBytes - sizeof(StackType_t) ); - //@ assert( (char*) pxStack + ulFreeBytes == (char*) pxTopOfStack + sizeof(StackType_t) ); - - // skip stack cell #0 - //@ chars_split(gcStack, ulFreeBytes - sizeof(StackType_t)); - //@ chars_to_integers_(gOldTop, sizeof(StackType_t), false, 1); - //@ integers__join(gOldTop); - /* Simulate the stack frame as it would be created by a context switch - * interrupt. */ - pxTopOfStack--; /* Offset added to account for the way the MCU uses the stack on entry/exit of interrupts. */ - - // Ensure maintining stack invariant - //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 1, ulUsedCells + 1, ulUnalignedBytes); - //@ open stack_p_2(pxStack, _, _, _, _, _); - - //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) ); - //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 1) == (char*) pxTopOfStack + sizeof(StackType_t) ); - - // make stack cell #1 available - //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 2)); - //@ chars_to_integers_(gOldTop-1, sizeof(StackType_t), false, 1); - //@ integers__join(gOldTop-1); - *pxTopOfStack = ( 0x01000000 ); /* xPSR */ - //@ close integers_(gOldTop-1, sizeof(StackType_t), false, ulUsedCells+2, _); - pxTopOfStack--; - - // Ensure maintining stack invariant - //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 2, ulUsedCells + 2, ulUnalignedBytes); - //@ open stack_p_2(pxStack, _, _, _, _, _); - - //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) ); - //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 2) == (char*) pxTopOfStack + sizeof(StackType_t) ); - - // prevent overflow - //@ ptr_range(pxCode); - // make stack cell #2 available - //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 3)); - //@ chars_to_integers_(gOldTop-2, sizeof(StackType_t), false, 1); - //@ integers__join(gOldTop-2); - *pxTopOfStack = ( StackType_t ) pxCode; /* PC */ - //@ close integers_(gOldTop-2, sizeof(StackType_t), false, ulUsedCells+3, _); - pxTopOfStack--; - - // Ensure maintining stack invariant - //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 3, ulUsedCells + 3, ulUnalignedBytes); - //@ open stack_p_2(pxStack, _, _, _, _, _); - - //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 4) ); - //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 3) == (char*) pxTopOfStack + sizeof(StackType_t) ); - - // prevent underflow - //@ ptr_range(prvTaskExitError); - // make stack cell #3 available - //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 4)); - //@ chars_to_integers_(gOldTop-3, sizeof(StackType_t), false, 1); - //@ integers__join(gOldTop-3); - *pxTopOfStack = ( StackType_t ) prvTaskExitError; /* LR */ - //@ close integers_(gOldTop-3, sizeof(StackType_t), false, ulUsedCells+4, _); - - pxTopOfStack -= 5; /* R12, R3, R2 and R1. */ - - // jump to stack cell #7 - //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 8)); - //@ chars_to_integers_(gOldTop-7, sizeof(StackType_t), false, 4); - //@ integers__join(gOldTop-7); - - // Ensure maintining stack invariant - //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 8, ulUsedCells + 8, ulUnalignedBytes); - //@ open stack_p_2(pxStack, _, _, _, _, _); - - //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 9) ); - //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 8) == (char*) pxTopOfStack + sizeof(StackType_t) ); - - // prevent overflow - //@ ptr_range(pvParameters); - - // make stack cell #8 available - //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 9)); - //@ chars_to_integers_(gOldTop-8, sizeof(StackType_t), false, 1); - //@ integers__join(gOldTop-8); - *pxTopOfStack = ( StackType_t ) pvParameters; /* R0 */ - //@ close integers_(gOldTop-8, sizeof(StackType_t), false, ulUsedCells+9, _); - - // Ensure maintining stack invariant - //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack-1, ulFreeBytes - sizeof(StackType_t) * 9, ulUsedCells + 9, ulUnalignedBytes); - //@ open stack_p_2(pxStack, _, _, _, _, _); - - - // skip stack cells #9 - #15, leave #16 unused - //@ chars_split(gcStack, ulFreeBytes - (sizeof(StackType_t) * 16)); - //@ chars_to_integers_(gOldTop-15, sizeof(StackType_t), false, 7); - //@ integers__join(gOldTop-15); - pxTopOfStack -= 8; /* R11..R4. */ - - // Ensure maintining stack invariant - //@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes); - //@ assert( stack_p_2(pxStack, ulStackDepth, gOldTop-16, ulFreeBytes - sizeof(StackType_t) * 16, ulUsedCells + 16, ulUnalignedBytes) ); - - //@ assert( (char*) pxTopOfStack == (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 17) ); - //@ assert( (char*) pxStack + (ulFreeBytes - sizeof(StackType_t) * 16) == (char*) pxTopOfStack + sizeof(StackType_t) ); - - return pxTopOfStack; -} \ No newline at end of file diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_bitops_extended.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_bitops_extended.h deleted file mode 100644 index 437ae4102..000000000 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_bitops_extended.h +++ /dev/null @@ -1,11 +0,0 @@ -#ifndef VERIFAST_BITOPS_EXTENDED_H -#define VERIFAST_BITOPS_EXTENDED_H - -/*@ -// TODO: Can we remove this? -lemma void bitand_idempotent_right(int l, int r); -requires true; -ensures (l & r) == ((l & r) & r); -@*/ - -#endif /* VERIFAST_BITOPS_EXTENDED_H */ \ No newline at end of file diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_prelude_extended.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_prelude_extended.h deleted file mode 100644 index beb263831..000000000 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_prelude_extended.h +++ /dev/null @@ -1,107 +0,0 @@ -#ifndef VERIFAST_PRELUDE_EXTENDED_H -#define VERIFAST_PRELUDE_EXTENDED_H - -/* This file contains axioms that would naturally fit into prelude.h - * but are missing. - */ - -/* Reminder: - -predicate chars_(char *array, int count; list > cs) = - count == 0 ? - cs == nil - : - char_(array, ?c) &*& chars_(array + 1, count - 1, ?cs0) &*& cs == cons(c, cs0); - -predicate chars(char *array, int count; list cs) = - count == 0 ? - cs == nil - : - character(array, ?c) &*& chars(array + 1, count - 1, ?cs0) &*& cs == cons(c, cs0); - - -lemma_auto void chars__to_chars(char *array); - requires [?f]chars_(array, ?count, ?cs) &*& cs == map(some, map(the, cs)); - ensures [f]chars(array, count, map(the, cs)); - - - -predicate integers__(void *p, int size, bool signed_, int count; list > vs) = - count == 0 ? - vs == nil - : - integer__(p, size, signed_, ?v0) &*& integers__(p + size, size, signed_, count - 1, ?vs0) &*& vs == cons(v0, vs0); - -predicate integers_(void *p, int size, bool signed_, int count; list vs) = - count == 0 ? - vs == nil - : - integer_(p, size, signed_, ?v0) &*& integers_(p + size, size, signed_, count - 1, ?vs0) &*& vs == cons(v0, vs0); - - - */ - - - - -/*@ -lemma_auto void integers___to_integers_(void *p); - requires [?f]integers__(p, ?size, ?signed_, ?count, _); - ensures [f]integers_(p, size, signed_, count, _); -@*/ - - -/*@ -lemma void chars_split_at(char* start_ptr, char* split_ptr) -requires chars(start_ptr, ?count, ?vs) &*& - start_ptr <= split_ptr &*& split_ptr < start_ptr + count; -ensures chars(start_ptr, ?c1, ?vs1) &*& - chars(split_ptr, ?c2, ?vs2) &*& - start_ptr + c1 == split_ptr &*& - c1 + c2 == count; -{ - if( start_ptr == split_ptr ) - { - close chars(start_ptr, 0, nil); - } else - { - assert( start_ptr < split_ptr ); // Will fail when pointer provenance checks are turned on - open chars(start_ptr, _, _); - chars_split_at(start_ptr+1, split_ptr); - assert( chars(start_ptr+1, ?c1, _) ); - close chars(start_ptr, c1+1, _); - } -} -@*/ - - -/*@ -lemma void division_remainder_def(int l, int r); -requires l >= 0 &*& r > 0 &*& r < l; -ensures l == (l % r) + (l / r) * r &*& -0 <= (l % r) &*& -(l % r) < r; -@*/ - -/*@ -lemma void chars_to_max_integers__suffix(char* startPtr, int intSize, bool signed_) -requires chars(startPtr, ?count, ?vs) &*& intSize > 0 &*& count > intSize; -ensures chars(startPtr, ?cc, _) &*& - integers_(?intStartPtr, intSize, signed_, ?ci, _) &*& - count == cc + ci * intSize &*& - intStartPtr == startPtr + cc &*& - cc < intSize &*& - ci == count / intSize; -{ - int rem = count % intSize; - int ci = count / intSize; - - division_remainder_def(count, intSize); - chars_split(startPtr, rem); - chars_to_integers_(startPtr + rem, intSize, signed_, ci); - -} -@*/ - - -#endif /* VERIFAST_PRELUDE_EXTENDED_H */ \ No newline at end of file diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c index e5ff0b1b0..33a0f507c 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c +++ b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c @@ -79,8 +79,6 @@ #include "task_predicates.h" #include "ready_list_predicates.h" #include "verifast_RP2040_axioms.h" - #include "verifast_prelude_extended.h" - #include "verifast_bitops_extended.h" #include "verifast_asm.h" #include "verifast_port_contracts.h" #include "verifast_lock_predicates.h" @@ -88,8 +86,6 @@ #include "single_core_proofs/scp_list_predicates.h" #include "single_core_proofs_extended/scp_list_predicates_extended.h" - #include "snippets/rp2040_port_c_snippets.c" - #include "list.c" #endif