From 8c7ba865150f18472d9d1f145098ff47cd327ea6 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Tue, 17 Oct 2023 19:49:48 -0400 Subject: [PATCH] Unbounded proofs of memory safety (#146) * Add a CBMC proof harness for multiSearch function Signed-off-by: Felipe R. Monteiro * Make all CBMC proofs unbounded Signed-off-by: Felipe R. Monteiro * Make coreJSON more verification friendly In order to turn all bounded CBMC proofs into unbounded proofs, we must make some small changes to coreJSON. Basically, we want to avoid uninitialized variables (CBMC sees them as non-deterministic values) and make sure the code in loops is resilient enough when working with inputs of arbitrary size. The latter is important because we must annotate all loops with loop invariants. The implementation should work together with these annotations in order to prove memory safety for inputs of arbitrary size. Signed-off-by: Felipe R. Monteiro * Include patch with loop invariants Modify existing CBMC proofs to remove any assumptions over the size of the input (a.k.a. bound). Instrument all loops with Hoare-style loop invariants and assigns clauses (define the modified memory within a loop), which CBMC uses to prove correctness. Annotate all loops using decreases clauses, which CBMC uses to prove termination. Signed-off-by: Felipe R. Monteiro * Add patch for loop invariants in CI Signed-off-by: Felipe R. Monteiro --------- Signed-off-by: Felipe R. Monteiro --- .github/workflows/ci.yml | 1 + loop_invariants.patch | 202 ++++++++++++++++++ source/core_json.c | 79 +++---- test/cbmc/include/core_json_contracts.h | 82 ++++--- test/cbmc/proofs/JSON_Iterate/Makefile | 7 +- test/cbmc/proofs/JSON_SearchConst/Makefile | 18 +- test/cbmc/proofs/JSON_Validate/Makefile | 11 +- test/cbmc/proofs/Makefile-json.common | 14 +- test/cbmc/proofs/arraySearch/Makefile | 8 +- test/cbmc/proofs/multiSearch/Makefile | 19 ++ test/cbmc/proofs/multiSearch/README.md | 17 ++ test/cbmc/proofs/multiSearch/cbmc-proof.txt | 1 + test/cbmc/proofs/multiSearch/cbmc-viewer.json | 7 + .../proofs/multiSearch/multiSearch_harness.c | 42 ++++ test/cbmc/proofs/objectSearch/Makefile | 12 +- test/cbmc/proofs/skipAnyScalar/Makefile | 8 +- test/cbmc/proofs/skipCollection/Makefile | 9 +- test/cbmc/proofs/skipDigits/Makefile | 7 +- test/cbmc/proofs/skipEscape/Makefile | 7 +- test/cbmc/proofs/skipObjectScalars/Makefile | 11 +- test/cbmc/proofs/skipScalars/Makefile | 9 +- test/cbmc/proofs/skipSpace/Makefile | 7 +- test/cbmc/proofs/skipString/Makefile | 7 +- test/cbmc/proofs/skipUTF8/Makefile | 8 +- test/cbmc/sources/core_json_contracts.c | 94 +++++--- 25 files changed, 466 insertions(+), 221 deletions(-) create mode 100644 loop_invariants.patch create mode 100644 test/cbmc/proofs/multiSearch/Makefile create mode 100644 test/cbmc/proofs/multiSearch/README.md create mode 100644 test/cbmc/proofs/multiSearch/cbmc-proof.txt create mode 100644 test/cbmc/proofs/multiSearch/cbmc-viewer.json create mode 100644 test/cbmc/proofs/multiSearch/multiSearch_harness.c diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e39af014..df6032ba 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -161,3 +161,4 @@ jobs: uses: FreeRTOS/CI-CD-Github-Actions/run_cbmc@main with: proofs_dir: test/cbmc/proofs + run_cbmc_proofs_command: cd ../../../; git apply -v loop_invariants.patch; cd test/cbmc/proofs; ./run-cbmc-proofs.py diff --git a/loop_invariants.patch b/loop_invariants.patch new file mode 100644 index 00000000..f364b92e --- /dev/null +++ b/loop_invariants.patch @@ -0,0 +1,202 @@ +diff --git a/source/core_json.c b/source/core_json.c +index 901b2e1..8bdd89c 100644 +--- a/source/core_json.c ++++ b/source/core_json.c +@@ -62,6 +62,21 @@ typedef union + #define isSquareOpen_( x ) ( ( x ) == '[' ) + #define isSquareClose_( x ) ( ( x ) == ']' ) + ++/** ++ * Renaming all loop-contract clauses from CBMC for readability. ++ * For more information about loop contracts in CBMC, see ++ * https://diffblue.github.io/cbmc/contracts-user.html. ++ */ ++#ifdef CBMC ++#define loopInvariant(...) __CPROVER_loop_invariant(__VA_ARGS__) ++#define decreases(...) __CPROVER_decreases(__VA_ARGS__) ++#define assigns(...) __CPROVER_assigns(__VA_ARGS__) ++#else ++#define loopInvariant(...) ++#define decreases(...) ++#define assigns(...) ++#endif ++ + /** + * @brief Advance buffer index beyond whitespace. + * +@@ -78,6 +93,9 @@ static void skipSpace( const char * buf, + assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); + + for( i = *start; i < max; i++ ) ++ assigns( i ) ++ loopInvariant( *start <= i && i <= max ) ++ decreases( max - i ) + { + if( !isspace_( buf[ i ] ) ) + { +@@ -102,6 +120,13 @@ static size_t countHighBits( uint8_t c ) + size_t i = 0; + + while( ( n & 0x80U ) != 0U ) ++ assigns( i, n ) ++ loopInvariant ( ++ ( 0U <= i ) && ( i <= 8U ) ++ && ( n == ( c & ( 0xFF >> i ) ) << i ) ++ && ( ( ( c >> ( 8U - i ) ) + 1U ) == ( 1U << i ) ) ++ ) ++ decreases( 8U - i ) + { + i++; + n = ( n & 0x7FU ) << 1U; +@@ -210,6 +235,13 @@ static bool skipUTF8MultiByte( const char * buf, + /* The bit count is 1 greater than the number of bytes, + * e.g., when j is 2, we skip one more byte. */ + for( j = bitCount - 1U; j > 0U; j-- ) ++ assigns( j, i, value, c.c ) ++ loopInvariant( ++ ( 0 <= j ) && ( j <= bitCount - 1 ) ++ && ( *start <= i ) && ( i <= max ) ++ && ( ( i == max ) ==> ( j > 0 ) ) ++ ) ++ decreases( j ) + { + i++; + +@@ -345,6 +377,12 @@ static bool skipOneHexEscape( const char * buf, + if( ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) ) + { + for( i += 2U; i < end; i++ ) ++ assigns( value, i ) ++ loopInvariant( ++ ( *start + 2U <= i ) && ( i <= end ) && ++ ( 0U <= value ) && ( value < ( 1U << ( 4U * ( i - ( 2U + *start ) ) ) ) ) ++ ) ++ decreases( end - i ) + { + uint8_t n = hexToInt( buf[ i ] ); + +@@ -522,6 +560,9 @@ static bool skipString( const char * buf, + i++; + + while( i < max ) ++ assigns( i ) ++ loopInvariant( *start + 1U <= i && i <= max ) ++ decreases( max - i ) + { + if( buf[ i ] == '"' ) + { +@@ -580,6 +621,9 @@ static bool strnEq( const char * a, + assert( ( a != NULL ) && ( b != NULL ) ); + + for( i = 0; i < n; i++ ) ++ assigns( i ) ++ loopInvariant( i <= n ) ++ decreases( n - i ) + { + if( a[ i ] != b[ i ] ) + { +@@ -681,6 +725,7 @@ static bool skipAnyLiteral( const char * buf, + * false otherwise. + */ + #define MAX_FACTOR ( MAX_INDEX_VALUE / 10 ) ++ + static bool skipDigits( const char * buf, + size_t * start, + size_t max, +@@ -695,6 +740,9 @@ static bool skipDigits( const char * buf, + saveStart = *start; + + for( i = *start; i < max; i++ ) ++ assigns( value, i ) ++ loopInvariant( *start <= i && i <= max ) ++ decreases( max - i ) + { + if( !isdigit_( buf[ i ] ) ) + { +@@ -944,6 +992,9 @@ static void skipArrayScalars( const char * buf, + i = *start; + + while( i < max ) ++ assigns( i ) ++ loopInvariant( *start <= i && i <= max ) ++ decreases( max - i ) + { + if( skipAnyScalar( buf, &i, max ) != true ) + { +@@ -986,6 +1037,13 @@ static void skipObjectScalars( const char * buf, + i = *start; + + while( i < max ) ++ assigns( i, *start, comma ) ++ loopInvariant( ++ i >= *start ++ && __CPROVER_loop_entry( i ) <= i && i <= max ++ && __CPROVER_loop_entry( *start ) <= *start && *start <= max ++ ) ++ decreases( max - i ) + { + if( skipString( buf, &i, max ) != true ) + { +@@ -1082,6 +1140,14 @@ static JSONStatus_t skipCollection( const char * buf, + i = *start; + + while( i < max ) ++ assigns( i, depth, c, __CPROVER_object_whole( stack ), ret ) ++ loopInvariant( ++ -1 <= depth && depth <= JSON_MAX_DEPTH ++ && *start <= i && i <= max ++ && ( ( ret == JSONSuccess ) ==> i >= *start + 2U ) ++ && ( ret == JSONSuccess || ret == JSONPartial || ret == JSONIllegalDocument || ret == JSONMaxDepthExceeded ) ++ ) ++ decreases( max - i ) + { + c = buf[ i ]; + i++; +@@ -1363,6 +1429,9 @@ static bool objectSearch( const char * buf, + skipSpace( buf, &i, max ); + + while( i < max ) ++ assigns( i, key, keyLength, value, valueLength ) ++ loopInvariant( __CPROVER_loop_entry( i ) <= i && i <= max ) ++ decreases( max - i ) + { + if( nextKeyValuePair( buf, &i, max, &key, &keyLength, + &value, &valueLength ) != true ) +@@ -1430,6 +1499,9 @@ static bool arraySearch( const char * buf, + skipSpace( buf, &i, max ); + + while( i < max ) ++ assigns( i, currentIndex, value, valueLength ) ++ loopInvariant( __CPROVER_loop_entry( i ) <= i && i <= max && currentIndex < i ) ++ decreases( max - i ) + { + if( nextValue( buf, &i, max, &value, &valueLength ) != true ) + { +@@ -1495,6 +1567,9 @@ static bool skipQueryPart( const char * buf, + while( ( i < max ) && + !isSeparator_( buf[ i ] ) && + !isSquareOpen_( buf[ i ] ) ) ++ assigns( i ) ++ loopInvariant( i <= max ) ++ decreases( max - i ) + { + i++; + } +@@ -1541,6 +1616,17 @@ static JSONStatus_t multiSearch( const char * buf, + assert( ( max > 0U ) && ( queryLength > 0U ) ); + + while( i < queryLength ) ++ assigns( i, start, queryStart, value, length ) ++ loopInvariant( ++ 0U <= start && start < max ++ && 0U < length && length <= max ++ && start + length <= max ++ && ( ( i == queryLength && ret == JSONSuccess && buf[ start ] == '"' ) ==> length >= 2U ) ++ && 0U <= value && value < max ++ && 0U <= i && i <= queryLength ++ && 0U <= queryStart && queryStart <= queryLength ++ ) ++ decreases( queryLength - i ) + { + bool found = false; + diff --git a/source/core_json.c b/source/core_json.c index 928bb02a..901b2e16 100644 --- a/source/core_json.c +++ b/source/core_json.c @@ -73,7 +73,7 @@ static void skipSpace( const char * buf, size_t * start, size_t max ) { - size_t i; + size_t i = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -131,7 +131,7 @@ static bool shortestUTF8( size_t length, uint32_t value ) { bool ret = false; - uint32_t min, max; + uint32_t min = 0U, max = 0U; assert( ( length >= 2U ) && ( length <= 4U ) ); @@ -190,9 +190,9 @@ static bool skipUTF8MultiByte( const char * buf, size_t max ) { bool ret = false; - size_t i, bitCount, j; - uint32_t value = 0; - char_ c; + size_t i = 0U, bitCount = 0U, j = 0U; + uint32_t value = 0U; + char_ c = { 0 }; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -283,7 +283,7 @@ static bool skipUTF8( const char * buf, #define NOT_A_HEX_CHAR ( 0x10U ) static uint8_t hexToInt( char c ) { - char_ n; + char_ n = { 0 }; n.c = c; @@ -329,8 +329,8 @@ static bool skipOneHexEscape( const char * buf, uint16_t * outValue ) { bool ret = false; - size_t i, end; - uint16_t value = 0; + size_t i = 0U, end = 0U; + uint16_t value = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); assert( outValue != NULL ); @@ -392,8 +392,8 @@ static bool skipHexEscape( const char * buf, size_t max ) { bool ret = false; - size_t i; - uint16_t value; + size_t i = 0U; + uint16_t value = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -444,7 +444,7 @@ static bool skipEscape( const char * buf, size_t max ) { bool ret = false; - size_t i; + size_t i = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -511,7 +511,7 @@ static bool skipString( const char * buf, size_t max ) { bool ret = false; - size_t i; + size_t i = 0; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -575,7 +575,7 @@ static bool strnEq( const char * a, const char * b, size_t n ) { - size_t i; + size_t i = 0U; assert( ( a != NULL ) && ( b != NULL ) ); @@ -640,7 +640,7 @@ static bool skipAnyLiteral( const char * buf, size_t * start, size_t max ) { - bool ret; + bool ret = false; #define skipLit_( x ) \ ( skipLiteral( buf, start, max, ( x ), ( sizeof( x ) - 1UL ) ) == true ) @@ -687,8 +687,8 @@ static bool skipDigits( const char * buf, int32_t * outValue ) { bool ret = false; - size_t i, saveStart; - int32_t value = 0; + size_t i = 0U, saveStart = 0U; + int32_t value = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -741,7 +741,7 @@ static void skipDecimals( const char * buf, size_t * start, size_t max ) { - size_t i; + size_t i = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -769,7 +769,7 @@ static void skipExponent( const char * buf, size_t * start, size_t max ) { - size_t i; + size_t i = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -806,7 +806,7 @@ static bool skipNumber( const char * buf, size_t max ) { bool ret = false; - size_t i; + size_t i = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -861,7 +861,7 @@ static bool skipAnyScalar( const char * buf, size_t * start, size_t max ) { - bool ret; + bool ret = false; if( skipString( buf, start, max ) == true ) { @@ -902,7 +902,7 @@ static bool skipSpaceAndComma( const char * buf, size_t max ) { bool ret = false; - size_t i; + size_t i = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -937,7 +937,7 @@ static void skipArrayScalars( const char * buf, size_t * start, size_t max ) { - size_t i; + size_t i = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -978,8 +978,8 @@ static void skipObjectScalars( const char * buf, size_t * start, size_t max ) { - size_t i; - bool comma; + size_t i = 0U; + bool comma = false; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -1075,7 +1075,7 @@ static JSONStatus_t skipCollection( const char * buf, JSONStatus_t ret = JSONPartial; char c, stack[ JSON_MAX_DEPTH ]; int16_t depth = -1; - size_t i; + size_t i = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -1092,7 +1092,7 @@ static JSONStatus_t skipCollection( const char * buf, case '[': depth++; - if( depth == JSON_MAX_DEPTH ) + if( depth >= JSON_MAX_DEPTH ) { ret = JSONMaxDepthExceeded; break; @@ -1105,11 +1105,13 @@ static JSONStatus_t skipCollection( const char * buf, case '}': case ']': - if( ( depth > 0 ) && isMatchingBracket_( stack[ depth ], c ) ) + if( ( depth > 0 ) && ( depth < JSON_MAX_DEPTH ) && + isMatchingBracket_( stack[ depth ], c ) ) { depth--; - if( skipSpaceAndComma( buf, &i, max ) == true ) + if( ( skipSpaceAndComma( buf, &i, max ) == true ) && + isOpenBracket_( stack[ depth ] ) ) { skipScalars( buf, &i, max, stack[ depth ] ); } @@ -1152,7 +1154,7 @@ JSONStatus_t JSON_Validate( const char * buf, size_t max ) { JSONStatus_t ret; - size_t i = 0; + size_t i = 0U; if( buf == NULL ) { @@ -1218,7 +1220,7 @@ static bool nextValue( const char * buf, size_t * valueLength ) { bool ret = true; - size_t i, valueStart; + size_t i = 0U, valueStart = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); assert( ( value != NULL ) && ( valueLength != NULL ) ); @@ -1275,7 +1277,7 @@ static bool nextKeyValuePair( const char * buf, size_t * valueLength ) { bool ret = true; - size_t i, keyStart; + size_t i = 0U, keyStart = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); assert( ( key != NULL ) && ( keyLength != NULL ) ); @@ -1348,7 +1350,7 @@ static bool objectSearch( const char * buf, { bool ret = false; - size_t i = 0, key, keyLength, value = 0, valueLength = 0; + size_t i = 0U, key = 0U, keyLength = 0U, value = 0U, valueLength = 0U; assert( ( buf != NULL ) && ( query != NULL ) ); assert( ( outValue != NULL ) && ( outValueLength != NULL ) ); @@ -1414,8 +1416,8 @@ static bool arraySearch( const char * buf, size_t * outValueLength ) { bool ret = false; - size_t i = 0, value = 0, valueLength = 0; - uint32_t currentIndex = 0; + size_t i = 0U, value = 0U, valueLength = 0U; + uint32_t currentIndex = 0U; assert( buf != NULL ); assert( ( outValue != NULL ) && ( outValueLength != NULL ) ); @@ -1440,7 +1442,8 @@ static bool arraySearch( const char * buf, break; } - if( skipSpaceAndComma( buf, &i, max ) != true ) + if( ( skipSpaceAndComma( buf, &i, max ) != true ) || + ( currentIndex == UINT32_MAX ) ) { break; } @@ -1482,7 +1485,7 @@ static bool skipQueryPart( const char * buf, size_t * outLength ) { bool ret = false; - size_t i; + size_t i = 0U; assert( ( buf != NULL ) && ( start != NULL ) && ( outLength != NULL ) ); assert( max > 0U ); @@ -1531,7 +1534,7 @@ static JSONStatus_t multiSearch( const char * buf, size_t * outValueLength ) { JSONStatus_t ret = JSONSuccess; - size_t i = 0, start = 0, queryStart = 0, value = 0, length = max; + size_t i = 0U, start = 0U, queryStart = 0U, value = 0U, length = max; assert( ( buf != NULL ) && ( query != NULL ) ); assert( ( outValue != NULL ) && ( outValueLength != NULL ) ); @@ -1797,7 +1800,7 @@ JSONStatus_t JSON_Iterate( const char * buf, JSONPair_t * outPair ) { JSONStatus_t ret; - size_t key, keyLength, value, valueLength; + size_t key = 0U, keyLength = 0U, value = 0U, valueLength = 0U; if( ( buf == NULL ) || ( start == NULL ) || ( next == NULL ) || ( outPair == NULL ) ) diff --git a/test/cbmc/include/core_json_contracts.h b/test/cbmc/include/core_json_contracts.h index 1f0936f2..fec38860 100644 --- a/test/cbmc/include/core_json_contracts.h +++ b/test/cbmc/include/core_json_contracts.h @@ -87,80 +87,93 @@ * These are declarations for all predicates used in coreJSON function contracts. */ -bool isValidBoundedBuffer( char * buf, - size_t max ); -bool isValidBoundedBufferWithStartIndex( char * buf, - size_t max, - size_t * start ); +bool isValidBuffer( const char * buf, + size_t max ); +bool isValidBufferWithStartIndex( const char * buf, + size_t max, + size_t * start ); bool isValidStart( size_t start, size_t old_start, size_t max ); -bool JSON_SearchConstPreconditions( char * buf, +bool JSON_SearchConstPreconditions( const char * buf, size_t max, - char * query, + const char * query, size_t queryLength, - char ** outValue, + const char ** outValue, size_t * outValueLength, JSONTypes_t * outType ); bool JSON_SearchConstPostconditions( JSONStatus_t result, - char * buf, - char ** outValue, + const char * buf, + const char ** outValue, size_t * outValueLength, size_t max ); -bool JSON_IteratePreconditions( char * buf, +bool JSON_IteratePreconditions( const char * buf, size_t max, size_t * start, size_t * next, JSONPair_t * outPair ); bool JSON_IteratePostconditions( JSONStatus_t result, - char * buf, + const char * buf, size_t max, JSONPair_t * outPair ); -JSONStatus_t JSON_ValidatePreconditions( char * buf, +JSONStatus_t JSON_ValidatePreconditions( const char * buf, size_t max ); -bool arraySearchPreconditions( char * buf, +bool arraySearchPreconditions( const char * buf, size_t max, size_t * outValue, size_t * outValueLength ); bool arraySearchPostconditions( bool result, - char * buf, + const char * buf, size_t max, size_t * outValue, size_t * outValueLength, size_t old_outValue, size_t old_outValueLength ); -bool objectSearchPreconditions( char * buf, +bool objectSearchPreconditions( const char * buf, size_t max, const char * query, size_t queryLength, size_t * outValue, size_t * outValueLength ); +bool multiSearchPreconditions( const char * buf, + size_t max, + const char * query, + size_t queryLength, + size_t * outValue, + size_t * outValueLength ); +bool multiSearchPostconditions( JSONStatus_t result, + const char * buf, + size_t max, + size_t * outValue, + size_t * outValueLength, + size_t old_outValue, + size_t old_outValueLength ); bool skipPostconditions( bool result, - char * buf, + const char * buf, size_t * start, size_t old_start, size_t max, size_t gap ); bool skipCollectionPostconditions( JSONStatus_t result, - char * buf, + const char * buf, size_t * start, size_t old_start, size_t max ); -bool skipScalarsPreconditions( char * buf, +bool skipScalarsPreconditions( const char * buf, size_t * start, size_t max, char mode ); bool skipAnyScalarPostconditions( bool result, - char * buf, + const char * buf, size_t * start, size_t old_start, size_t max ); -bool skipDigitsPreconditions( char * buf, +bool skipDigitsPreconditions( const char * buf, size_t * start, size_t max, int32_t * outValue ); bool skipDigitsPostconditions( bool result, - char * buf, + const char * buf, size_t * start, size_t old_start, size_t max, @@ -229,10 +242,21 @@ assigns( *outValue, *outValueLength ) ensures( arraySearchPostconditions( result, buf, max, outValue, outValueLength, old( *outValue ), old( *outValueLength ) ) ) ; +JSONStatus_t multiSearch( const char * buf, + size_t max, + const char * query, + size_t queryLength, + size_t * outValue, + size_t * outValueLength ) +requires( multiSearchPreconditions( buf, max, query, queryLength, outValue, outValueLength ) ) +assigns( *outValue, *outValueLength ) +ensures( multiSearchPostconditions( result, buf, max, outValue, outValueLength, old( *outValue ), old( *outValueLength ) ) ) +; + JSONStatus_t skipCollection( const char * buf, size_t * start, size_t max ) -requires( isValidBoundedBufferWithStartIndex( buf, max, start ) ) +requires( isValidBufferWithStartIndex( buf, max, start ) ) assigns( *start ) ensures( skipCollectionPostconditions( result, buf, start, old( *start ), max ) ) ; @@ -249,7 +273,7 @@ ensures( isValidStart( *start, old( *start ), max ) ) void skipObjectScalars( const char * buf, size_t * start, size_t max ) -requires( isValidBoundedBufferWithStartIndex( buf, max, start ) ) +requires( isValidBufferWithStartIndex( buf, max, start ) ) assigns( *start ) ensures( isValidStart( *start, old( *start ), max ) ) ; @@ -257,7 +281,7 @@ ensures( isValidStart( *start, old( *start ), max ) ) bool skipAnyScalar( const char * buf, size_t * start, size_t max ) -requires( isValidBoundedBufferWithStartIndex( buf, max, start ) ) +requires( isValidBufferWithStartIndex( buf, max, start ) ) assigns( *start ) ensures( skipAnyScalarPostconditions( result, buf, start, old( *start ), max ) ) ; @@ -265,7 +289,7 @@ ensures( skipAnyScalarPostconditions( result, buf, start, old( *start ), max ) ) void skipSpace( const char * buf, size_t * start, size_t max ) -requires( isValidBoundedBufferWithStartIndex( buf, max, start ) ) +requires( isValidBufferWithStartIndex( buf, max, start ) ) assigns( *start ) ensures( isValidStart( *start, old( *start ), max ) ) ; @@ -273,7 +297,7 @@ ensures( isValidStart( *start, old( *start ), max ) ) bool skipString( const char * buf, size_t * start, size_t max ) -requires( isValidBoundedBufferWithStartIndex( buf, max, start ) ) +requires( isValidBufferWithStartIndex( buf, max, start ) ) assigns( *start ) ensures( skipPostconditions( result, buf, start, old( *start ), max, 1 ) ) ; @@ -281,7 +305,7 @@ ensures( skipPostconditions( result, buf, start, old( *start ), max, 1 ) ) bool skipEscape( const char * buf, size_t * start, size_t max ) -requires( isValidBoundedBufferWithStartIndex( buf, max, start ) ) +requires( isValidBufferWithStartIndex( buf, max, start ) ) assigns( *start ) ensures( skipPostconditions( result, buf, start, old( *start ), max, 1 ) ) ; @@ -289,7 +313,7 @@ ensures( skipPostconditions( result, buf, start, old( *start ), max, 1 ) ) bool skipUTF8( const char * buf, size_t * start, size_t max ) -requires( isValidBoundedBufferWithStartIndex( buf, max, start ) ) +requires( isValidBufferWithStartIndex( buf, max, start ) ) assigns( *start ) ensures( skipPostconditions( result, buf, start, old( *start ), max, 0 ) ) ; diff --git a/test/cbmc/proofs/JSON_Iterate/Makefile b/test/cbmc/proofs/JSON_Iterate/Makefile index 41e87175..ec4d2297 100644 --- a/test/cbmc/proofs/JSON_Iterate/Makefile +++ b/test/cbmc/proofs/JSON_Iterate/Makefile @@ -5,19 +5,14 @@ PROOF_UID=JSON_Iterate CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 CBMC_OBJECT_BITS = 12 -UNWINDSET += JSON_Iterate.0:$(CBMC_MAX_BUFSIZE) - USE_FUNCTION_CONTRACTS += skipAnyScalar USE_FUNCTION_CONTRACTS += skipCollection USE_FUNCTION_CONTRACTS += skipSpace USE_FUNCTION_CONTRACTS += skipString include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/JSON_SearchConst/Makefile b/test/cbmc/proofs/JSON_SearchConst/Makefile index 7d11d945..dcefe78d 100644 --- a/test/cbmc/proofs/JSON_SearchConst/Makefile +++ b/test/cbmc/proofs/JSON_SearchConst/Makefile @@ -5,25 +5,13 @@ PROOF_UID=JSON_SearchConst CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 CBMC_OBJECT_BITS = 11 -UNWINDSET += multiSearch.0:$(CBMC_MAX_QUERYKEYLENGTH) -UNWINDSET += skipQueryPart.0:$(CBMC_MAX_QUERYKEYLENGTH) +USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver kissat -USE_FUNCTION_CONTRACTS += arraySearch -USE_FUNCTION_CONTRACTS += objectSearch -USE_FUNCTION_CONTRACTS += skipAnyScalar -USE_FUNCTION_CONTRACTS += skipCollection -USE_FUNCTION_CONTRACTS += skipDigits -USE_FUNCTION_CONTRACTS += skipSpace -USE_FUNCTION_CONTRACTS += skipString - -USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical +USE_FUNCTION_CONTRACTS += multiSearch include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/JSON_Validate/Makefile b/test/cbmc/proofs/JSON_Validate/Makefile index 1c7ad6b3..9bbf9bc1 100644 --- a/test/cbmc/proofs/JSON_Validate/Makefile +++ b/test/cbmc/proofs/JSON_Validate/Makefile @@ -1,23 +1,16 @@ # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. # SPDX-License-Identifier: MIT-0 -EXPENSIVE = true - PROOF_UID=JSON_Validate CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 -UNWINDSET += skipSpace.0:$(CBMC_MAX_BUFSIZE) +USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical USE_FUNCTION_CONTRACTS += skipAnyScalar USE_FUNCTION_CONTRACTS += skipCollection -USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical - include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/Makefile-json.common b/test/cbmc/proofs/Makefile-json.common index 22d3b60b..cce13279 100644 --- a/test/cbmc/proofs/Makefile-json.common +++ b/test/cbmc/proofs/Makefile-json.common @@ -3,16 +3,6 @@ HARNESS_ENTRY=harness -# This value was experimentally chosen to provide 100% coverage -# without tripping unwinding assertions and without exhausting memory. -CBMC_MAX_BUFSIZE ?= 11 -CBMC_MAX_QUERYKEYLENGTH ?= 6 - -DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE) -ifdef CBMC_MAX_QUERYKEYLENGTH - DEFINES += -DCBMC_MAX_QUERYKEYLENGTH=$(CBMC_MAX_QUERYKEYLENGTH) -endif - INCLUDES += -I$(CBMC_ROOT)/include PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c @@ -28,3 +18,7 @@ include ../Makefile.common cleanclean: veryclean -$(RM) $(PROOFDIR)/core_json.c + +# Substitution command to pass to sed for patching core_json.c. The +# characters " and # must be escaped with backslash. +CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/arraySearch/Makefile b/test/cbmc/proofs/arraySearch/Makefile index dc58e375..e5f31ae7 100644 --- a/test/cbmc/proofs/arraySearch/Makefile +++ b/test/cbmc/proofs/arraySearch/Makefile @@ -5,19 +5,13 @@ PROOF_UID=arraySearch CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 CBMC_OBJECT_BITS = 12 -UNWINDSET += arraySearch.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += arraySearch.1:$(CBMC_MAX_BUFSIZE) - USE_FUNCTION_CONTRACTS += skipAnyScalar USE_FUNCTION_CONTRACTS += skipCollection USE_FUNCTION_CONTRACTS += skipSpace include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/multiSearch/Makefile b/test/cbmc/proofs/multiSearch/Makefile new file mode 100644 index 00000000..63d7ae23 --- /dev/null +++ b/test/cbmc/proofs/multiSearch/Makefile @@ -0,0 +1,19 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: MIT-0 + +PROOF_UID=multiSearch +CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) +HARNESS_FILE= $(PROOF_UID)_harness + +APPLY_LOOP_CONTRACTS = 1 +USE_DYNAMIC_FRAMES = 1 + +CBMC_OBJECT_BITS = 12 + +USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver kissat + +USE_FUNCTION_CONTRACTS += arraySearch +USE_FUNCTION_CONTRACTS += objectSearch +USE_FUNCTION_CONTRACTS += skipDigits + +include ../Makefile-json.common diff --git a/test/cbmc/proofs/multiSearch/README.md b/test/cbmc/proofs/multiSearch/README.md new file mode 100644 index 00000000..44de39eb --- /dev/null +++ b/test/cbmc/proofs/multiSearch/README.md @@ -0,0 +1,17 @@ +multiSearch proof +============== + +This directory contains a memory safety proof for `multiSearch`. +The proof runs in a few seconds and provides 100% coverage. + +For this proof, the following functions are replaced with function contracts. +These functions have separate proofs. +* `arraySearch`; +* `objectSearch`; +* `skipDigits`. + +To run the proof. +* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer` + to your path; +* Run `make`; +* Open `html/index.html` in a web browser. diff --git a/test/cbmc/proofs/multiSearch/cbmc-proof.txt b/test/cbmc/proofs/multiSearch/cbmc-proof.txt new file mode 100644 index 00000000..6ed46f12 --- /dev/null +++ b/test/cbmc/proofs/multiSearch/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/multiSearch/cbmc-viewer.json b/test/cbmc/proofs/multiSearch/cbmc-viewer.json new file mode 100644 index 00000000..e0fc0c4e --- /dev/null +++ b/test/cbmc/proofs/multiSearch/cbmc-viewer.json @@ -0,0 +1,7 @@ +{ "expected-missing-functions": + [ + + ], + "proof-name": "multiSearch", + "proof-root": "test/cbmc/proofs" +} diff --git a/test/cbmc/proofs/multiSearch/multiSearch_harness.c b/test/cbmc/proofs/multiSearch/multiSearch_harness.c new file mode 100644 index 00000000..07b932ab --- /dev/null +++ b/test/cbmc/proofs/multiSearch/multiSearch_harness.c @@ -0,0 +1,42 @@ +/* + * coreJSON v3.2.0 + * Copyright (C) 2020 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. + */ + +/** + * @file multiSearch_harness.c + * @brief Implements the proof harness for the multiSearch function. + */ + +#include "core_json_contracts.h" + +void harness() +{ + char * buf; + size_t max; + char * query; + size_t queryLength; + char * outValue; + size_t * outValueLength; + + multiSearch( buf, max, query, queryLength, outValue, outValueLength ); +} diff --git a/test/cbmc/proofs/objectSearch/Makefile b/test/cbmc/proofs/objectSearch/Makefile index fab42f11..c0af4caf 100644 --- a/test/cbmc/proofs/objectSearch/Makefile +++ b/test/cbmc/proofs/objectSearch/Makefile @@ -1,28 +1,20 @@ # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. # SPDX-License-Identifier: MIT-0 -EXPENSIVE = true - PROOF_UID=objectSearch CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 CBMC_OBJECT_BITS = 11 -UNWINDSET += objectSearch.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnEq.0:$(CBMC_MAX_BUFSIZE) +USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical USE_FUNCTION_CONTRACTS += skipAnyScalar USE_FUNCTION_CONTRACTS += skipCollection USE_FUNCTION_CONTRACTS += skipSpace USE_FUNCTION_CONTRACTS += skipString -USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical - include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/skipAnyScalar/Makefile b/test/cbmc/proofs/skipAnyScalar/Makefile index 96b29a0e..ba922681 100644 --- a/test/cbmc/proofs/skipAnyScalar/Makefile +++ b/test/cbmc/proofs/skipAnyScalar/Makefile @@ -5,16 +5,10 @@ PROOF_UID=skipAnyScalar CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 -UNWINDSET += skipAnyScalar.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += strnEq.0:$(CBMC_MAX_BUFSIZE) - USE_FUNCTION_CONTRACTS += skipDigits USE_FUNCTION_CONTRACTS += skipString include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/skipCollection/Makefile b/test/cbmc/proofs/skipCollection/Makefile index 17e7999d..de423826 100644 --- a/test/cbmc/proofs/skipCollection/Makefile +++ b/test/cbmc/proofs/skipCollection/Makefile @@ -5,19 +5,12 @@ PROOF_UID=skipCollection CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 CBMC_OBJECT_BITS = 10 -DEFINES += -DJSON_MAX_DEPTH="( $(CBMC_MAX_BUFSIZE) - 2 )" - USE_FUNCTION_CONTRACTS += skipScalars USE_FUNCTION_CONTRACTS += skipSpace -UNWINDSET += skipCollection.0:$(CBMC_MAX_BUFSIZE) - include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/skipDigits/Makefile b/test/cbmc/proofs/skipDigits/Makefile index c0b33dff..657ddcbd 100644 --- a/test/cbmc/proofs/skipDigits/Makefile +++ b/test/cbmc/proofs/skipDigits/Makefile @@ -5,12 +5,7 @@ PROOF_UID=skipDigits CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 -UNWINDSET += skipDigits.0:$(CBMC_MAX_BUFSIZE) - include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/skipEscape/Makefile b/test/cbmc/proofs/skipEscape/Makefile index 0ba03f70..84518f98 100644 --- a/test/cbmc/proofs/skipEscape/Makefile +++ b/test/cbmc/proofs/skipEscape/Makefile @@ -5,12 +5,7 @@ PROOF_UID=skipEscape CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 -UNWINDSET += skipOneHexEscape.0:$(CBMC_MAX_BUFSIZE) - include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/skipObjectScalars/Makefile b/test/cbmc/proofs/skipObjectScalars/Makefile index b0e137f5..55d32608 100644 --- a/test/cbmc/proofs/skipObjectScalars/Makefile +++ b/test/cbmc/proofs/skipObjectScalars/Makefile @@ -1,26 +1,19 @@ # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. # SPDX-License-Identifier: MIT-0 -EXPENSIVE = true - PROOF_UID=skipObjectScalars CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 CBMC_OBJECT_BITS = 11 -UNWINDSET += skipObjectScalars.0:$(CBMC_MAX_BUFSIZE) +USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical USE_FUNCTION_CONTRACTS += skipSpace USE_FUNCTION_CONTRACTS += skipAnyScalar USE_FUNCTION_CONTRACTS += skipString -USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical - include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/skipScalars/Makefile b/test/cbmc/proofs/skipScalars/Makefile index c97367be..b2de06a0 100644 --- a/test/cbmc/proofs/skipScalars/Makefile +++ b/test/cbmc/proofs/skipScalars/Makefile @@ -5,21 +5,16 @@ PROOF_UID=skipScalars CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 CBMC_OBJECT_BITS = 11 -UNWINDSET += skipArrayScalars.0:$(CBMC_MAX_BUFSIZE) +USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical USE_FUNCTION_CONTRACTS += skipAnyScalar USE_FUNCTION_CONTRACTS += skipObjectScalars USE_FUNCTION_CONTRACTS += skipSpace USE_FUNCTION_CONTRACTS += skipString -USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical - include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/skipSpace/Makefile b/test/cbmc/proofs/skipSpace/Makefile index 96c26bf3..3c6dc0ef 100644 --- a/test/cbmc/proofs/skipSpace/Makefile +++ b/test/cbmc/proofs/skipSpace/Makefile @@ -5,12 +5,7 @@ PROOF_UID=skipSpace CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 -UNWINDSET += skipSpace.0:$(CBMC_MAX_BUFSIZE) - include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/skipString/Makefile b/test/cbmc/proofs/skipString/Makefile index 50abf69e..8958116a 100644 --- a/test/cbmc/proofs/skipString/Makefile +++ b/test/cbmc/proofs/skipString/Makefile @@ -5,19 +5,14 @@ PROOF_UID=skipString CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 CBMC_OBJECT_BITS = 10 USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical -UNWINDSET += skipString.0:$(CBMC_MAX_BUFSIZE) - USE_FUNCTION_CONTRACTS += skipEscape USE_FUNCTION_CONTRACTS += skipUTF8 include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/proofs/skipUTF8/Makefile b/test/cbmc/proofs/skipUTF8/Makefile index 6c5c769d..a712a1cd 100644 --- a/test/cbmc/proofs/skipUTF8/Makefile +++ b/test/cbmc/proofs/skipUTF8/Makefile @@ -5,13 +5,7 @@ PROOF_UID=skipUTF8 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID) HARNESS_FILE= $(PROOF_UID)_harness +APPLY_LOOP_CONTRACTS = 1 USE_DYNAMIC_FRAMES = 1 -UNWINDSET += countHighBits.0:$(CBMC_MAX_BUFSIZE) -UNWINDSET += skipUTF8MultiByte.0:$(CBMC_MAX_BUFSIZE) - include ../Makefile-json.common - -# Substitution command to pass to sed for patching core_json.c. The -# characters " and # must be escaped with backslash. -CORE_JSON_SED_EXPR = s/^static // diff --git a/test/cbmc/sources/core_json_contracts.c b/test/cbmc/sources/core_json_contracts.c index 6fd2da3c..b4bb2bd7 100644 --- a/test/cbmc/sources/core_json_contracts.c +++ b/test/cbmc/sources/core_json_contracts.c @@ -36,19 +36,19 @@ */ /* Valid allocated buffer up to size max. */ -bool isValidBoundedBuffer( char * buf, - size_t max ) +bool isValidBuffer( const char * buf, + size_t max ) { - return ( 0 < max && max < CBMC_MAX_BUFSIZE ) + return ( 0U < max ) & ( allocated( buf, max ) ); } /* Valid allocated buffer up to size max and allocated start index. */ -bool isValidBoundedBufferWithStartIndex( char * buf, - size_t max, - size_t * start ) +bool isValidBufferWithStartIndex( const char * buf, + size_t max, + size_t * start ) { - return isValidBoundedBuffer( buf, max ) + return isValidBuffer( buf, max ) & ( allocated( start, sizeof( *start ) ) ); } @@ -61,17 +61,15 @@ bool isValidStart( size_t start, ( ( old_start < max ) ? ( start <= max ) : ( start == old_start ) ); } -bool JSON_SearchConstPreconditions( char * buf, +bool JSON_SearchConstPreconditions( const char * buf, size_t max, - char * query, + const char * query, size_t queryLength, - char ** outValue, + const char ** outValue, size_t * outValueLength, JSONTypes_t * outType ) { - return ( max < CBMC_MAX_BUFSIZE ) - & ( queryLength < CBMC_MAX_QUERYKEYLENGTH ) - & ( buf == NULL || allocated( buf, max ) ) + return ( buf == NULL || allocated( buf, max ) ) & ( query == NULL || allocated( query, queryLength ) ) & ( outValue == NULL || allocated( outValue, sizeof( *outValue ) ) ) & ( outValueLength == NULL || allocated( outValueLength, sizeof( *outValueLength ) ) ) @@ -79,8 +77,8 @@ bool JSON_SearchConstPreconditions( char * buf, } bool JSON_SearchConstPostconditions( JSONStatus_t result, - char * buf, - char ** outValue, + const char * buf, + const char ** outValue, size_t * outValueLength, size_t max ) { @@ -96,13 +94,13 @@ bool JSON_SearchConstPostconditions( JSONStatus_t result, return validity; } -bool JSON_IteratePreconditions( char * buf, +bool JSON_IteratePreconditions( const char * buf, size_t max, size_t * start, size_t * next, JSONPair_t * outPair ) { - return ( 0 < max && max < CBMC_MAX_BUFSIZE ) + return ( 0 < max ) & ( buf == NULL || allocated( buf, max ) ) & ( start == NULL || allocated( start, sizeof( *start ) ) ) & ( next == NULL || allocated( next, sizeof( *next ) ) ) @@ -112,7 +110,7 @@ bool JSON_IteratePreconditions( char * buf, } bool JSON_IteratePostconditions( JSONStatus_t result, - char * buf, + const char * buf, size_t max, JSONPair_t * outPair ) { @@ -129,26 +127,25 @@ bool JSON_IteratePostconditions( JSONStatus_t result, return validity; } -JSONStatus_t JSON_ValidatePreconditions( char * buf, +JSONStatus_t JSON_ValidatePreconditions( const char * buf, size_t max ) { - return ( max < CBMC_MAX_BUFSIZE ) - & ( buf == NULL || allocated( buf, max ) ); + return( buf == NULL || allocated( buf, max ) ); } -bool arraySearchPreconditions( char * buf, +bool arraySearchPreconditions( const char * buf, size_t max, size_t * outValue, size_t * outValueLength ) { - return ( isValidBoundedBuffer( buf, max ) ) + return ( isValidBuffer( buf, max ) ) & ( allocated( outValue, sizeof( *outValue ) ) ) & ( allocated( outValueLength, sizeof( *outValueLength ) ) ) & ( *outValueLength <= max ); } bool arraySearchPostconditions( bool result, - char * buf, + const char * buf, size_t max, size_t * outValue, size_t * outValueLength, @@ -159,7 +156,7 @@ bool arraySearchPostconditions( bool result, if( result ) { - validity = ( 0 <= *outValue && *outValue < max ) && + validity = ( *outValue < max ) && ( 0 < *outValueLength && *outValueLength <= max - *outValue ) && IMPLIES( buf[ *outValue ] == '"', ( 2 <= *outValueLength && *outValueLength <= max - *outValue ) ); } @@ -172,7 +169,7 @@ bool arraySearchPostconditions( bool result, return validity; } -bool objectSearchPreconditions( char * buf, +bool objectSearchPreconditions( const char * buf, size_t max, const char * query, size_t queryLength, @@ -180,12 +177,39 @@ bool objectSearchPreconditions( char * buf, size_t * outValueLength ) { return arraySearchPreconditions( buf, max, outValue, outValueLength ) - & ( queryLength < CBMC_MAX_QUERYKEYLENGTH ) & ( allocated( query, queryLength ) ); } +bool multiSearchPreconditions( const char * buf, + size_t max, + const char * query, + size_t queryLength, + size_t * outValue, + size_t * outValueLength ) +{ + return ( isValidBuffer( buf, max ) ) + & ( 0U < queryLength ) + & ( allocated( query, queryLength ) ) + & ( allocated( outValue, sizeof( *outValue ) ) ) + & ( allocated( outValueLength, sizeof( *outValueLength ) ) ); +} + +bool multiSearchPostconditions( JSONStatus_t result, + const char * buf, + size_t max, + size_t * outValue, + size_t * outValueLength, + size_t old_outValue, + size_t old_outValueLength ) +{ + bool validity = isJSONSearchEnum( result ) && + arraySearchPostconditions( result == JSONSuccess, buf, max, outValue, outValueLength, old_outValue, old_outValueLength ); + + return validity; +} + bool skipPostconditions( bool result, - char * buf, + const char * buf, size_t * start, size_t old_start, size_t max, @@ -198,7 +222,7 @@ bool skipPostconditions( bool result, } bool skipCollectionPostconditions( JSONStatus_t result, - char * buf, + const char * buf, size_t * start, size_t old_start, size_t max ) @@ -209,17 +233,17 @@ bool skipCollectionPostconditions( JSONStatus_t result, return validity; } -bool skipScalarsPreconditions( char * buf, +bool skipScalarsPreconditions( const char * buf, size_t * start, size_t max, char mode ) { return ( ( mode == '{' ) || ( mode == '[' ) ) - & isValidBoundedBufferWithStartIndex( buf, max, start ); + & isValidBufferWithStartIndex( buf, max, start ); } bool skipAnyScalarPostconditions( bool result, - char * buf, + const char * buf, size_t * start, size_t old_start, size_t max ) @@ -230,17 +254,17 @@ bool skipAnyScalarPostconditions( bool result, return validity; } -bool skipDigitsPreconditions( char * buf, +bool skipDigitsPreconditions( const char * buf, size_t * start, size_t max, int32_t * outValue ) { return ( outValue == NULL || allocated( outValue, sizeof( *outValue ) ) ) - & isValidBoundedBufferWithStartIndex( buf, max, start ); + & isValidBufferWithStartIndex( buf, max, start ); } bool skipDigitsPostconditions( bool result, - char * buf, + const char * buf, size_t * start, size_t old_start, size_t max,