forked from FreeRTOS/coreJSON
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Restructure function contracts for readability (FreeRTOS#142)
* Restructure function contracts for readability Signed-off-by: Felipe R. Monteiro <felisous@amazon.com> * Update lexicon list Signed-off-by: Felipe R. Monteiro <felisous@amazon.com> * Update contracts Signed-off-by: Felipe R. Monteiro <felisous@amazon.com> * Avoid code duplication Signed-off-by: Felipe R. Monteiro <felisous@amazon.com> * Upgrade CBMC version in CI Signed-off-by: Felipe R. Monteiro <felisous@amazon.com> --------- Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
- Loading branch information
1 parent
7b24709
commit 8d216b5
Showing
10 changed files
with
451 additions
and
138 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,255 @@ | ||
| /* | ||
| * coreJSON v3.2.0 | ||
| * Copyright (C) 2023 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. | ||
| */ | ||
|
|
||
| #ifndef CORE_JSON_CONTRACTS_C_ | ||
| #define CORE_JSON_CONTRACTS_C_ | ||
|
|
||
| #include "core_json_contracts.h" | ||
|
|
||
| /** | ||
| * When to use `&` vs `&&`: | ||
| * Prefer `cond1 & cond2` when `cond2` can be evaluated without errors without knowing that `cond1` holds: e.g. `( 0 < i ) & ( i < j )`. | ||
| * | ||
| * Use `cond1 && cond2` when `cond1` must be established first to ensure that `cond2` can be evaluated without error: e.g. | ||
| * `( allocated( p, size ) & ( 0 < i & i < size ) ) && p[i] > 0`. | ||
| */ | ||
|
|
||
| /* Valid allocated buffer up to size max. */ | ||
| bool isValidBoundedBuffer( char * buf, | ||
| size_t max ) | ||
| { | ||
| return ( 0 < max && max < CBMC_MAX_BUFSIZE ) | ||
| & ( allocated( buf, max ) ); | ||
| } | ||
|
|
||
| /* Valid allocated buffer up to size max and allocated start index. */ | ||
| bool isValidBoundedBufferWithStartIndex( char * buf, | ||
| size_t max, | ||
| size_t * start ) | ||
| { | ||
| return isValidBoundedBuffer( buf, max ) | ||
| & ( allocated( start, sizeof( *start ) ) ); | ||
| } | ||
|
|
||
| /* Invariant for index in the buffer. */ | ||
| bool isValidStart( size_t start, | ||
| size_t old_start, | ||
| size_t max ) | ||
| { | ||
| return ( start >= old_start ) && | ||
| ( ( old_start < max ) ? ( start <= max ) : ( start == old_start ) ); | ||
| } | ||
|
|
||
| bool JSON_SearchConstPreconditions( char * buf, | ||
| size_t max, | ||
| char * query, | ||
| size_t queryLength, | ||
| char ** outValue, | ||
| size_t * outValueLength, | ||
| JSONTypes_t * outType ) | ||
| { | ||
| return ( max < CBMC_MAX_BUFSIZE ) | ||
| & ( queryLength < CBMC_MAX_QUERYKEYLENGTH ) | ||
| & ( buf == NULL || allocated( buf, max ) ) | ||
| & ( query == NULL || allocated( query, queryLength ) ) | ||
| & ( outValue == NULL || allocated( outValue, sizeof( *outValue ) ) ) | ||
| & ( outValueLength == NULL || allocated( outValueLength, sizeof( *outValueLength ) ) ) | ||
| & ( outType == NULL || allocated( outType, sizeof( *outType ) ) ); | ||
| } | ||
|
|
||
| bool JSON_SearchConstPostconditions( JSONStatus_t result, | ||
| char * buf, | ||
| char ** outValue, | ||
| size_t * outValueLength, | ||
| size_t max ) | ||
| { | ||
| bool validity = isJSONSearchEnum( result ); | ||
|
|
||
| if( validity && ( result == JSONSuccess ) ) | ||
| { | ||
| char * endOfValue = *outValue + *outValueLength; | ||
| char * endOfBuf = buf + max; | ||
| validity = pointer_in_range( buf, endOfValue, endOfBuf ); | ||
| } | ||
|
|
||
| return validity; | ||
| } | ||
|
|
||
| bool JSON_IteratePreconditions( char * buf, | ||
| size_t max, | ||
| size_t * start, | ||
| size_t * next, | ||
| JSONPair_t * outPair ) | ||
| { | ||
| return ( 0 < max && max < CBMC_MAX_BUFSIZE ) | ||
| & ( buf == NULL || allocated( buf, max ) ) | ||
| & ( start == NULL || allocated( start, sizeof( *start ) ) ) | ||
| & ( next == NULL || allocated( next, sizeof( *next ) ) ) | ||
| & ( outPair == NULL || allocated( outPair, sizeof( *outPair ) ) ) | ||
| & IMPLIES( outPair != NULL, ( ( outPair->keyLength == 0 && outPair->key == NULL ) || allocated( outPair->key, outPair->keyLength ) ) ) | ||
| & IMPLIES( outPair != NULL, ( ( outPair->valueLength == 0 && outPair->value == NULL ) || allocated( outPair->value, outPair->valueLength ) ) ); | ||
| } | ||
|
|
||
| bool JSON_IteratePostconditions( JSONStatus_t result, | ||
| char * buf, | ||
| size_t max, | ||
| JSONPair_t * outPair ) | ||
| { | ||
| bool validity = isJSONIterateEnum( result ); | ||
|
|
||
| if( validity && ( result == JSONSuccess ) ) | ||
| { | ||
| validity = IMPLIES( ( outPair->key != NULL ), ( ( outPair->key > buf ) && ( ( outPair->key + outPair->keyLength ) < ( buf + max ) ) ) ) | ||
| & IMPLIES( ( outPair->key != NULL ), ( ( outPair->key + outPair->keyLength ) < outPair->value ) ) | ||
| & ( ( outPair->value > buf ) && ( ( outPair->value + outPair->valueLength ) <= ( buf + max ) ) ) | ||
| & ( isJSONTypesEnum( outPair->jsonType ) ); | ||
| } | ||
|
|
||
| return validity; | ||
| } | ||
|
|
||
| JSONStatus_t JSON_ValidatePreconditions( char * buf, | ||
| size_t max ) | ||
| { | ||
| return ( max < CBMC_MAX_BUFSIZE ) | ||
| & ( buf == NULL || allocated( buf, max ) ); | ||
| } | ||
|
|
||
| bool arraySearchPreconditions( char * buf, | ||
| size_t max, | ||
| size_t * outValue, | ||
| size_t * outValueLength ) | ||
| { | ||
| return ( isValidBoundedBuffer( buf, max ) ) | ||
| & ( allocated( outValue, sizeof( *outValue ) ) ) | ||
| & ( allocated( outValueLength, sizeof( *outValueLength ) ) ) | ||
| & ( *outValueLength <= max ); | ||
| } | ||
|
|
||
| bool arraySearchPostconditions( bool result, | ||
| char * buf, | ||
| size_t max, | ||
| size_t * outValue, | ||
| size_t * outValueLength, | ||
| size_t old_outValue, | ||
| size_t old_outValueLength ) | ||
| { | ||
| bool validity = true; | ||
|
|
||
| if( result ) | ||
| { | ||
| validity = ( 0 <= *outValue && *outValue < max ) && | ||
| ( 0 < *outValueLength && *outValueLength <= max - *outValue ) && | ||
| IMPLIES( buf[ *outValue ] == '"', ( 2 <= *outValueLength && *outValueLength <= max - *outValue ) ); | ||
| } | ||
| else | ||
| { | ||
| validity = ( *outValue == old_outValue ) && | ||
| ( *outValueLength == old_outValueLength ); | ||
| } | ||
|
|
||
| return validity; | ||
| } | ||
|
|
||
| bool objectSearchPreconditions( char * buf, | ||
| size_t max, | ||
| const char * query, | ||
| size_t queryLength, | ||
| size_t * outValue, | ||
| size_t * outValueLength ) | ||
| { | ||
| return arraySearchPreconditions( buf, max, outValue, outValueLength ) | ||
| & ( queryLength < CBMC_MAX_QUERYKEYLENGTH ) | ||
| & ( allocated( query, queryLength ) ); | ||
| } | ||
|
|
||
| bool skipPostconditions( bool result, | ||
| char * buf, | ||
| size_t * start, | ||
| size_t old_start, | ||
| size_t max, | ||
| size_t gap ) | ||
| { | ||
| bool validity = isValidStart( *start, old_start, max ) && | ||
| IMPLIES( result, ( old_start < max ) && ( *start > old_start + gap ) ); | ||
|
|
||
| return validity; | ||
| } | ||
|
|
||
| bool skipCollectionPostconditions( JSONStatus_t result, | ||
| char * buf, | ||
| size_t * start, | ||
| size_t old_start, | ||
| size_t max ) | ||
| { | ||
| bool validity = isSkipCollectionEnum( result ) && | ||
| skipPostconditions( ( result == JSONSuccess ), buf, start, old_start, max, 1 ); | ||
|
|
||
| return validity; | ||
| } | ||
|
|
||
| bool skipScalarsPreconditions( char * buf, | ||
| size_t * start, | ||
| size_t max, | ||
| char mode ) | ||
| { | ||
| return ( ( mode == '{' ) || ( mode == '[' ) ) | ||
| & isValidBoundedBufferWithStartIndex( buf, max, start ); | ||
| } | ||
|
|
||
| bool skipAnyScalarPostconditions( bool result, | ||
| char * buf, | ||
| size_t * start, | ||
| size_t old_start, | ||
| size_t max ) | ||
| { | ||
| bool validity = skipPostconditions( result, buf, start, old_start, max, 0 ) && | ||
| IMPLIES( ( result && ( buf[ old_start ] == '"' ) ), *start >= old_start + 2 ); | ||
|
|
||
| return validity; | ||
| } | ||
|
|
||
| bool skipDigitsPreconditions( char * buf, | ||
| size_t * start, | ||
| size_t max, | ||
| int32_t * outValue ) | ||
| { | ||
| return ( outValue == NULL || allocated( outValue, sizeof( *outValue ) ) ) | ||
| & isValidBoundedBufferWithStartIndex( buf, max, start ); | ||
| } | ||
|
|
||
| bool skipDigitsPostconditions( bool result, | ||
| char * buf, | ||
| size_t * start, | ||
| size_t old_start, | ||
| size_t max, | ||
| size_t gap ) | ||
| { | ||
| bool validity = skipPostconditions( result, buf, start, old_start, max, 0 ) && | ||
| IMPLIES( result, ( ( ( buf[ old_start ] ) >= '0' ) && ( ( buf[ old_start ] ) <= '9' ) ) ); | ||
|
|
||
| return validity; | ||
| } | ||
|
|
||
| #endif /* ifndef CORE_JSON_CONTRACTS_C_ */ |