queue.c: Change some asserts into conditionals and improve overflow checks #328

dan4thewin · 2021-05-19T20:51:58Z

This PR is paired with changes to the CBMC queue proofs: FreeRTOS/FreeRTOS#603

These changes allow certain CBMC proofs to be written with few or no assumptions. The overflow checks now preempt an overflow, rather than checking for the consequence of an overflow.

AniruddhaKanhere

Please see the comments.
I am not sure whether replacing multiple asserts with just one assert would benefit users.

queue.c

AniruddhaKanhere · 2021-05-19T21:36:31Z

queue.c

@@ -369,8 +375,7 @@ BaseType_t xQueueGenericReset( QueueHandle_t xQueue,
        }
        else
        {
-            traceQUEUE_CREATE_FAILED( ucQueueType );
-            mtCOVERAGE_TEST_MARKER();
+            configASSERT( pdFAIL );


This configASSERT would not help while debugging. In the previous source, one could simply see which configASSERT (with a proper implementation using __FILE__ and __LINE__) was failing and find the issue.
Now one would need to print out the values or step through the code with debugger. Shall we try to find a better way?

This was the approach Richard suggested. Changing the asserts to conditionals means there is still protection when assertions are compiled out, but loses debugging information as you point out. Adding in the trailing assert is a compromise to provide some information without repeating every check.

I see. Can we add all the asserts instead of the single assert? That would be a win win. In that case, we'll be able to debug effectively and protection will still be there if the assertions are compiled out.
I am asking this since we are anyways making a compromise with the pdFAIL assert.

I'm assuming you mean that we could have an else block where the tests are repeated as asserts. Manually keeping the two sets of tests in sync strikes me as a big drawback. Let's get Richard's opinion.

This is a great place for an ASSERT_CONTINUE macro. The idea would be to log the assertion to NV storage or to a debugging port (uart or similar), but not go into the typical infinite loop. This also lets customers test the edge cases in their applications without entering an infinite loop.

Same comment as in the queue reset function about using a constant as the parameter in the configASSERT() macro - will generate compiler warnings ("condition is always true"). Extending Paul's thoughts above, what we really need is an assert always function. I think, also as per my comments in the queue reset function, using a status variable that gets set to pass or fail, then asserting on the status variable just before exiting the function would be fine. I understand that loses information when debugging, but if you see that line is failing I think it would be possible to see why from within the debugger.

changed to assert on the return value

queue.c

paulbartell · 2021-05-20T18:26:41Z

Note: the unit tests for queue.c need to be updated over in the FreeRTOS/FreeRTOS repository ( https://github.com/FreeRTOS/FreeRTOS/tree/main/FreeRTOS/Test/CMock/queue ).

To validate that they run correctly on github, I would suggest making a branch in the FreeRTOS/FreeRTOS repository with the Source submodule pointer set to the tip of this branch. Then update the tests as necessary and disregard any failures displayed for unit tests in this PR.

Alternatively, you could modify the github workflow for unit tests in this repository to check for a branch with the same name from the same user's fork and use that branch is available.

RichardBarry · 2021-05-21T04:03:13Z

Brief answer for now due to it being late - I need to do a deeper dive into the PR before a full answer.

My understanding is that the prior asserts at the top of the file made the CBMC memory safety checks cumbersome and potentially long running - hence they were replaced with inline checks that are much more CBMC friendly. The new assert at the end then made it backward compatible for code that relied on the assert behavior.

I understand the desire to make it easier to debug - debuggability is a very important attribute. Adding the asserts() back at the front would probably re-introduce the CBMC issue this PR is trying to improve, plus it would look cumbersome to effectively have the same checks twice. It may be possible to replace the single assert at the end with something that provides more information to developers, but as per, I would need to look a bit deeper before having an opinion on that.

RichardBarry · 2021-05-24T00:31:05Z

queue.c

+    if( ( pxQueue != NULL ) &&
+        ( pxQueue->uxLength >= 1 ) &&
+        /* Check for multiplication overflow. */
+        ( ( SIZE_MAX / pxQueue->uxLength ) >= pxQueue->uxItemSize ) )


uxLength and uxItemSize are both UBaseType_t, rather than size_t, so this assumes sizeof( UBaseType_t ) == sizeof( size_t ) -> can we create a local constant that is equivalent to UBaseType_t_MAX?

I think SIZE_MAX or PTRDIFF_MAX are reasonable choices. Given that the pxQueue->uxLength and pxQueue->uxItemSize are used to do pointer arithmetic and also with pvPortMalloc(), we want the product of these to always be <= to the largest theoretical object.

RichardBarry · 2021-05-24T00:32:50Z

queue.c

@@ -268,8 +268,13 @@ BaseType_t xQueueGenericReset( QueueHandle_t xQueue,

    configASSERT( pxQueue );

-    taskENTER_CRITICAL();
+    if( ( pxQueue != NULL ) &&
+        ( pxQueue->uxLength >= 1 ) &&


Should put a "U" on the 1, as per 1U.

RichardBarry · 2021-05-24T00:40:12Z

queue.c

+    }
+    else
+    {
+        configASSERT( pdFAIL );


The problem with asserting on "pdFAIL" is that the condition is always true so this will generate compiler warnings. That is - the assert test will always trigger (which is the intention of course), and there is no ASSERT_ALWAYS() macro.

The previous version of this function only asserted when pxQueue was NULL, and that assert still exists at the top of the file, so that behaviour has not changed. Now however the code will also assert if either of the two additional checks fail. Perhaps introduce a status variable that is set to pdPASS in the happy path, and pdFAIL on what is currently line 318 - then assert on and return the status variable at the end of the function:

else { xReturn = pdFAIL; } configASSERT( xReturn != pdFAIL ); return xReturn;

RichardBarry · 2021-05-24T00:44:34Z

queue.c

@@ -369,8 +375,7 @@ BaseType_t xQueueGenericReset( QueueHandle_t xQueue,
        }
        else
        {
-            traceQUEUE_CREATE_FAILED( ucQueueType );
-            mtCOVERAGE_TEST_MARKER();
+            configASSERT( pdFAIL );


Same comment as in the queue reset function about using a constant as the parameter in the configASSERT() macro - will generate compiler warnings ("condition is always true"). Extending Paul's thoughts above, what we really need is an assert always function. I think, also as per my comments in the queue reset function, using a status variable that gets set to pass or fail, then asserting on the status variable just before exiting the function would be fine. I understand that loses information when debugging, but if you see that line is failing I think it would be possible to see why from within the debugger.

RichardBarry · 2021-05-24T00:45:17Z

queue.c

        }
        else
        {
-            traceQUEUE_CREATE_FAILED( ucQueueType );
-            mtCOVERAGE_TEST_MARKER();
+            configASSERT( pdFAIL );


Same comment here on asserting on an always true test.

…#328) Add missing power libraries. Also increase the size of the privileged data section as heap is now placed in the privileged data section. Signed-off-by: Gaurav Aggarwal <aggarg@amazon.com>

Changed some asserts into conditionals and improved overflow checks

2ab4275

dan4thewin requested a review from a team as a code owner May 19, 2021 20:51

AniruddhaKanhere requested changes May 19, 2021

View reviewed changes

markrtuttle previously approved these changes May 20, 2021

View reviewed changes

RichardBarry requested changes May 24, 2021

View reviewed changes

PR feedback

c248100

dan4thewin dismissed markrtuttle’s stale review via c248100 May 27, 2021 04:05

RichardBarry approved these changes May 27, 2021

View reviewed changes

Merge branch 'main' into audit-1

c5d45c6

AniruddhaKanhere approved these changes May 27, 2021

View reviewed changes

dan4thewin merged commit 8e2f723 into FreeRTOS:main May 27, 2021

This was referenced May 27, 2021

Update unit tests to match changes in queue.c FreeRTOS/FreeRTOS#614

Merged

Improve heap2 bounds checking #224

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

queue.c: Change some asserts into conditionals and improve overflow checks #328

queue.c: Change some asserts into conditionals and improve overflow checks #328

dan4thewin commented May 19, 2021

AniruddhaKanhere left a comment

AniruddhaKanhere May 19, 2021

dan4thewin May 19, 2021

AniruddhaKanhere May 19, 2021

dan4thewin May 19, 2021

paulbartell May 20, 2021 •

edited

Loading

RichardBarry May 24, 2021

dan4thewin May 27, 2021

paulbartell commented May 20, 2021

RichardBarry commented May 21, 2021

RichardBarry May 24, 2021

dan4thewin May 27, 2021

RichardBarry May 24, 2021

dan4thewin May 27, 2021

RichardBarry May 24, 2021

dan4thewin May 27, 2021

RichardBarry May 24, 2021

RichardBarry May 24, 2021

dan4thewin May 27, 2021

queue.c: Change some asserts into conditionals and improve overflow checks #328

queue.c: Change some asserts into conditionals and improve overflow checks #328

Conversation

dan4thewin commented May 19, 2021

AniruddhaKanhere left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

paulbartell May 20, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

paulbartell commented May 20, 2021

RichardBarry commented May 21, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

paulbartell May 20, 2021 •

edited

Loading