Performance Cliff and Excessive Memory Usage at --unwind 6

[zhoulaifu]

CBMC Bug Report: Performance Cliff and Excessive Memory Usage at --unwind 6

Performance Degradation and Memory Explosion in CBMC 6.4.1 on macOS ARM64 with --unwind 6 When Verifying cJSON.c.

Please advise if this is a known bug, and suggest patches or workarounds. I’m happy to provide more logs, test cases, or assist in debugging.

Description

I am experiencing a severe performance issue with CBMC 6.4.1 when increasing the --unwind value from 5 to 6 while verifying a C program that uses the cJSON library (cJSON.c). For --unwind ≤ 5, CBMC completes execution within seconds with reasonable memory usage. However, at --unwind 6, CBMC runs for over 10 hours without producing a result, and memory usage exceeds 100GB, which is unexpected and appears to indicate a state space explosion or bug.

Steps to Reproduce

1. Environment:

   • OS: macOS (Apple M3)
   • CBMC Version: 6.4.1

2. Project Structure:

   • Source files:
     • main.c: Contains a harness function provided below.
     • lib/cJSON/cJSON.c: The cJSON JSON parsing library (version 1.7.99, linked from https://github.com/DaveGamble/cJSON/blob/master/cJSON.c). The file also contains manually inserted assertions.
     • lib/cJSON/cJSON_Utils.c: Utilities for cJSON.
     • lib/cJSON/cJSON.h and lib/cJSON/cJSON_Utils.h: Corresponding headers (assumed to be included).

3. Harness and Command:

   • Harness Code (in main.c):

     #include <assert.h>
     #include <string.h>
     
     #define MAX_INPUT_SIZE 512
     
     // Forward declaration
     char *process_command(const char *command);
     
     void harness() {
         char buffer[3][MAX_INPUT_SIZE]; // Process up to 3 commands
         for (int i = 0; i < 3; i++) {
             __CPROVER_assume(buffer[i][MAX_INPUT_SIZE - 1] == '\0');
             __CPROVER_assume(strncmp(buffer[i], "ADD", 3) == 0 || strncmp(buffer[i], "MOD", 3) == 0 || 
                              strncmp(buffer[i], "GET id", 6) == 0 || strncmp(buffer[i], "EXIT", 4) == 0);
             char *response = process_command(buffer[i]);
             if (response) {
                 assert(response[strlen(response)] == '\0');
                 free(response);
             }
         }
     }

   • Command for Low Unwind (Works Fine):

     cbmc -Ilib/cJSON main.c lib/cJSON/cJSON.c lib/cJSON/cJSON_Utils.c --function harness --trace --no-standard-checks --no-built-in-assertions --unwind 5

     • Completes in seconds with normal memory usage.

   • Command for High Unwind (Fails):

     cbmc -Ilib/cJSON app/main.c lib/cJSON/cJSON.c lib/cJSON/cJSON_Utils.c --function harness --trace --no-standard-checks --no-built-in-assertions --unwind 6

     • Runs for >10 hours without completing and consumes >100GB of memory.

4. Verbose Output (With --verbosity 9):

   • When running with --unwind 6 and --verbosity 9, the following lines seem to repeat indefinitely, suggesting a potentially infinite loop or excessive unrolling:

     Unwinding loop cJSON_Delete.0 iteration 5 file lib/cJSON/cJSON.c line 260 function cJSON_Delete thread 0
     Unwinding recursion cJSON_Delete iteration 5
     Unwinding recursion cJSON_Delete iteration 6
     Not unwinding recursion cJSON_Delete iteration 7
     Unwinding loop cJSON_Delete.0 iteration 1 file lib/cJSON/cJSON.c line 260 function cJSON_Delete thread 0
     Not unwinding recursion cJSON_Delete iteration 7
     Unwinding loop cJSON_Delete.0 iteration 2 file lib/cJSON/cJSON.c line 260 function cJSON_Delete thread 0
     Not unwinding recursion cJSON_Delete iteration 7
     [And so on...]
     

   • For a single-command harness (processing one process_command call), the output is concise and fast:

     Unwinding recursion cJSON_Delete iteration 1
     Unwinding loop cJSON_Delete.0 iteration 1 file lib/cJSON/cJSON.c line 260 function cJSON_Delete thread 0
     Unwinding loop cJSON_Delete.0 iteration 1 file lib/cJSON/cJSON.c line 260 function cJSON_Delete thread 0
     ....
     

     This completes quickly with low memory usage.

Expected Behavior

• I expected runtime and memory usage to increase gradually with each increment of --unwind (e.g., from 5 to 6), not exponentially. For --unwind 6, CBMC should complete within minutes (or at most hours) with reasonable memory usage (e.g., <10GB), not >10 hours and >100GB.

Actual Behavior

• At --unwind 6, CBMC hangs for >10 hours, consumes >100GB of memory, and appears stuck in excessive unrolling of cJSON_Delete’s loop and recursion in lib/cJSON/cJSON.c (line 260).

Additional Context

• Assertions in cJSON.c:

  • I have manually injected three assertions in cJSON.c to test for vulnerabilities.

• Workarounds Tried:

  • Constrained buffer[i] to specific commands (ADD, MOD, GET id, EXIT) using __CPROVER_assume, but the issue persists.
  • Used a single-command harness, which works fast but doesn’t test the multi-command sequence needed for potential bugs.

Impact

This performance cliff prevents effective verification of multi-command sequences.

Possible Cause

• The cJSON_Delete function (line 260 in cJSON.c) contains a while loop and recursive calls (cJSON_Delete(item->child)), which CBMC unrolls excessively at --unwind 6. This likely causes a state space explosion.

[tautschnig]

Trying to Explain Why You Might See this Behaviour

It seems that increasing the unwinding by 1 triggers execution of a whole new set of program statements. Most likely you will have CBMC running on a very wide call tree, caused by excessive branching. This, in turn, is often caused by CBMC resolving function pointers to some over-approximate set of functions over the ones that can actually be called at any such point. A possible scenario is that you are iterating beyond the bounds of an array of function pointers such that the sixth element isn't initialised anymore and, therefore, CBMC's over-approximate function pointer resolution behaviour becomes apparent.

Remark: The above is some speculation as I couldn't find version 1.7.99 of cJSON, and neither was I able to find the function process_command in the cJSON repository.

A Simple Remediation

To tell whether you are likely facing this scenario or not you may wish to review the early stages of the log output with --verbosity 9. You will find a line saying "Removal of function pointers and virtual functions" followed by lines that give a source location and then "replacing function pointer by possible targets". (If no such line is present then my guess is wrong and you don't actually have any function pointers.) If you do have such lines, consider using goto-instrument's --restrict-function-pointer capability as documented here: https://diffblue.github.io/cbmc/man/goto-instrument.html.

The Better Remediation

Instead of trying to work around the limitations of bounded model checking you might instead opt for unbounded verification, using code contracts and/or loop invariants. See our documentation at https://diffblue.github.io/cbmc/contracts-user.html. For an practical example see coreJSON where we insert loop invariants described in this patch.

[zhoulaifu]

Thank you! We'll look into these remediations.

[kroening]

Also consider --depth -- this limits the number of instructions, as opposed to the number of loop iterations, and often has less of a performance cliff.

[zhoulaifu]

Daniel, thank you! I’ll definitely give that a try. CBMC is truly an awesome tool, and I’m excited about the prospect of using it for real-world projects.

I’ve had some success by simplifying a loop-heavy function in CJSON, although I’m a bit worried that these simplified functions or using the --depth flag might affect CBMC’s soundness. Still, I’m exploring that direction.

Also, could you possibly take a look at another question I posted? Here’s the link: #8602. It’s about CBMC’s modeling of library functions like sscanf and strcmp, and the related challenge of generating a counterexample for a char*.

[zhoulaifu]

I reran CBMC on cJSON using a high-performance server. After running for over 55 hours, CBMC terminated with a segmentation fault.

Here is the command I used:

time cbmc -Ilib/cJSON app/main.c lib/cJSON/cJSON.c lib/cJSON/cJSON_Utils.c --function harness_2_commands --trace --no-standard-checks --no-built-in-assertions --unwind 6

The output was as follows:

**** WARNING: Use --unwinding-assertions to obtain sound verification results
CBMC version 6.4.1 (cbmc-6.4.1) 64-bit x86_64 linux
Type-checking cJSON
Type-checking cJSON_Utils
Type-checking main
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Segmentation fault

real    3438m49.379s
user    3426m8.898s
sys     10m45.516s

This performance issue and the segmentation fault disappeared after I replaced two blocking functions (shown from --verbosity 9) with manually written ones that adheres to the original function's interface. I noticed that both blocking functions were calling themselvesm directly or indirectly, within a while loop. This makes me wonder whether CBMC has been fully tested for cases where a function combines recursion with a while loop. Any idea?

[remi-delmas-3000]

If you have recursive functions and loops you may want to try using function contracts ?

Here is a regression test example that checks a function that contains loops and also calls itself:

https://github.com/diffblue/cbmc/tree/f55f63666bbf06e2a59a57a984f3cb977187a796/regression/contracts-dfcc/recursive-function-and-loop-contracts

When using loop contracts and contracts for recursive functions you need to provide invariants and pre/post conditions but then CBMC reasons using induction instead of unwinding.

[zhoulaifu]

Thank you, Remi, for the great pointer! Did you mean that CBMC, when using unwind, is known to struggle with functions that call themselves within a while loop?

If it helps, I can provide a minimal working example for you to debug—assuming the regression test doesn’t already expose the issue.

I’ll try the approach of generating function contracts and loop invariants. However, since producing function contracts isn’t something that can be easily automated, I’d still like to explore the possibility of relying on unwind—if that’s feasible.

[remi-delmas-3000]

Hi, I've looked at the JSON parser code and I can tell you there's very little hope to verify all of that in one go using just unwinding. I could not really figure out what function you are analyzing (process_command does not exist in the cJSON source).

Some of the reasons::

• the internal_hooks structure in cJSON contains function pointers, by default CBMC supposes that any function with a compatible signature can be invoked via these pointers and symbolically executes all of them, even if they are in fact unreachable. You'll need to add extra CLI switches to tell CBMC what are the actual targets for these functions pointers each time they are dereferenced and reduce explosion this way.

Look at this regression test for an example of --restrict-function-pointer

https://github.com/diffblue/cbmc/tree/f55f63666bbf06e2a59a57a984f3cb977187a796/regression/goto-instrument/restrict-function-pointer-by-name-local

• the code contains a LOT of loops where the iterations seem to depend on the length of a string, for which there is no obvious bound. Symbolic execution cannot unwind these loops to completion without knowing the length of the string it is processing.
• If you want to prove the code for any size of input you'll need to use loop contracts + function contracts for recursive functions, there's no way around it.

However there's some prior art that shows that it is possible to verify such JSON parsers using CBMC

A couple of years ago we verified the coreJSON parser of freeRTOS for memory safety using CBMC, with function and loop contracts. It seems really similar to what you're currently trying to do.

https://github.com/feliperodri/coreJSON/tree/52918f1ab0df56932af929008a9f7af2c7dc4d49/test/cbmc

You can see the function contracts we defined for the basic functions of the parser here:

• https://github.com/feliperodri/coreJSON/blob/52918f1ab0df56932af929008a9f7af2c7dc4d49/test/cbmc/include/core_json_contracts.h
• https://github.com/feliperodri/coreJSON/blob/52918f1ab0df56932af929008a9f7af2c7dc4d49/test/cbmc/sources/core_json_contracts.c
• https://github.com/FreeRTOS/coreJSON/blob/main/loop_invariants.patch

With all of this we were able to prove the memory safety without using unwinding, for any byte buffer input size.

Getting to that sort of result is however a non-trivial amount of work.