Extracting Concrete Input Strings from CBMC Counterexamples

[zhoulaifu]

Hello CBMC Developers and Community,

I am currently using CBMC to verify a C program that checks whether an input string starts with the letter 'H'. My goal is to extract the exact concrete input string that triggers an assertion failure when the first character of the string is 'H'.

My C Program

#include <stdio.h>
#include <assert.h>
#include <string.h>

void check_starting_letter(const char *input) {
    size_t len = strlen(input);

    // Accept only strings that start with "H"
    if (len > 0 && input[0] == 'H') {
        assert(0);  // Force CBMC failure when input starts with 'H'
    }
}

My CBMC Command

I am running CBMC with the following command:

cbmc file1.c --function check_starting_letter --unwind 5 --no-standard-checks --trace

**CBMC Output **

CBMC successfully finds a counterexample that causes the assertion failure:

% cbmc file1.c --function check_starting_letter  --unwind 5   --no-standard-checks --trace
**** WARNING: Use --unwinding-assertions to obtain sound verification results
CBMC version 6.4.1 (cbmc-6.4.1) 64-bit arm64 macos
Type-checking file1
Generating GOTO Program
Adding CPROVER library (arm64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is SATISFIABLE
Building error trace

** Results:
file1.c function check_starting_letter
[check_starting_letter.assertion.1] line 12 assertion 0: FAILURE

Trace for check_starting_letter.assertion.1:

State 14 file file1.c function __CPROVER__start line 7 thread 0
----------------------------------------------------
  INPUT tmp: 4 (00000100)

State 15 file file1.c function __CPROVER__start line 7 thread 0
----------------------------------------------------
  INPUT input: ((const char *)NULL) (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 18 file file1.c function __CPROVER__start line 7 thread 0
----------------------------------------------------
  input=((const char *)NULL) (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 23 file file1.c function check_starting_letter line 8 thread 0
----------------------------------------------------
  s=((const char *)NULL) (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 25 file <builtin-library-strlen> function strlen line 17 thread 0
----------------------------------------------------
  len=0ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)

State 27 file <builtin-library-strlen> function strlen line 18 thread 0
----------------------------------------------------
  len=1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)

State 30 file <builtin-library-strlen> function strlen line 19 thread 0
----------------------------------------------------
  goto_symex$$return_value$$strlen=1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)

State 32 file file1.c function check_starting_letter line 8 thread 0
----------------------------------------------------
  return_value_strlen=1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)

State 33 file file1.c function check_starting_letter line 8 thread 0
----------------------------------------------------
  len=1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)

Violated property:
  file file1.c function check_starting_letter line 12 thread 0
  assertion 0
  !((signed long int)(signed long int)!(0 != 0) != 0l)

Thank you in advance for your help!

Best regards,
Zhoulai

[tautschnig]

CBMC itself does not know how to generate (suitable) objects for pointer-type inputs. Please use the goto-harness tool (as documented here: https://diffblue.github.io/cbmc/man/goto-harness.html) to produce a suitable environment.

[zhoulaifu]

Thank you. I have not yet been fruitful with go to harness. But thank you for the pointer. Related to this discussion, is the following a bug or perhaps, I misused the tool?

Potential Bug Report: CBMC Enters If-Branch with Incorrect Condition Evaluation

Description

While using CBMC to verify a simple C program, I encountered unexpected behavior where CBMC prints an empty string with length 1 (which is likely '\0') while entering an if-branch that requires at least three characters (including \0).

Minimal Reproducible Example

#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

void check_starting_letter(const char *input) {
    size_t len = strlen(input);

    // Accept only strings that start with "HI"
    if (len >=3  && input[0] == 'H' && input[1] == 'I') {
        printf("CBMC executing check_starting_letter with input: %s\n", input);
        printf("CBMC executing check_starting_letter with input length: %zu\n", strlen(input));

        assert(0);  // Force CBMC failure when input starts with "HI"
    }
}

Command Used

cbmc file1.c --function check_starting_letter --trace --unwind 5 --no-standard-checks

Unexpected CBMC Output

** Results:
file1.c function check_starting_letter
[check_starting_letter.assertion.1] line 26 assertion 0: FAILURE
.....
CBMC executing check_starting_letter with input: 
....
CBMC executing check_starting_letter with input length: 1