`goto-instrument --enforce-contract-rec` does nothing

[vikramnitin9]

Version: CBMC 6.7.1
OS: Ubuntu 24.04

I'm trying to write function contracts for a quicksort program, and I'm running into some difficulties verifying contracts. This is my program, qsort.c:

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <stddef.h>
#include <limits.h>

// Function that swaps the integer values pointed to by a and b
void swap(int* a, int* b)
__CPROVER_requires(__CPROVER_r_ok(a) && __CPROVER_r_ok(b) && \
    __CPROVER_w_ok(a) && __CPROVER_w_ok(b))
__CPROVER_ensures(*a == __CPROVER_old(*b) && *b == __CPROVER_old(*a))
__CPROVER_assigns(*a, *b)
{
    int t = *a;
    *a = *b;
    *b = t;
}

// Divides the array into two partitions
int partition (int arr[], int low, int high)
__CPROVER_requires(arr != NULL && \
    low >= 0 && high >= 0 && low <= high && high < INT_MAX && \
    __CPROVER_is_fresh(arr, sizeof(int) * (high + 1)))
__CPROVER_ensures(__CPROVER_return_value >= low && __CPROVER_return_value <= high)
__CPROVER_assigns(__CPROVER_object_whole(arr))
{
    int pivot = arr[high]; // Choose the last element as the pivot
    int i = low - 1; // Temporary pivot index

    for (int j = low; j <= high - 1; j++) {
        // If the current element is less than or equal to the pivot
        if (arr[j] <= pivot) {
            // Move the temporary pivot index forward
            i++;
            // Swap the current element with the element at the temporary pivot index
            swap(&arr[i], &arr[j]);
        }
    }
    // Swap the pivot with the last element
    swap(&arr[i + 1], &arr[high]);
    return i + 1; // the pivot index
}

// Sorts (a portion of) an array, divides it into partitions, then sorts those
void quickSort(int arr[], int low, int high)
__CPROVER_requires(arr != NULL && \
    low >= 0 && high >= 0 && low <= high && high < INT_MAX && \
    __CPROVER_is_fresh(arr, sizeof(int) * (high + 1)))
__CPROVER_ensures(
  __CPROVER_forall{int i; (low <= i && i < high) ==> arr[i] <= arr[i + 1]}
)
__CPROVER_assigns(__CPROVER_object_whole(arr))
{
    // Ensure indices are in correct order
    if (low < high) {
        // Partition array and get the pivot index
        int i = partition(arr, low, high);
        // Sort the two partitions
        quickSort(arr, low, i - 1); // Left side of pivot
        quickSort(arr, i + 1, high); // Right side of pivot
    }
}

I'm then compiling these to goto programs with goto-cc, instrumenting them to enforce contracts using goto-instrument, and finally running verification for each function with cbmc. This process works fine for swap and partition, but when I try it for quickSort, it fails.
(Note - ... indicates that some lines of output have been omitted.)

> goto-cc -o quicksort.goto qsort.c --function quickSort
...
> goto-instrument --partial-loops --unwind 5 quicksort.goto quicksort.goto
> goto-instrument --replace-call-with-contract partition quicksort.goto quicksort.goto
> goto-instrument --replace-call-with-contract swap quicksort.goto quicksort.goto
> goto-instrument --enforce-contract-rec quickSort quicksort.goto checking-quicksort-contracts.goto
> cbmc checking-quicksort-contracts.goto --function quickSort --depth 100
...
...
Running propositional reduction
SAT checker: instance is UNSATISFIABLE

** Results:
qsort_gold_specs.c function partition
...
[partition.precondition.1] line 62 Check requires clause of partition in quickSort: FAILURE

qsort_gold_specs.c function quickSort
[quickSort.overflow.1] line 64 arithmetic overflow on signed - in i - 1: FAILURE
[quickSort.overflow.2] line 65 arithmetic overflow on signed + in i + 1: FAILURE

qsort_gold_specs.c function swap
...

** 3 of 508 failed (4 iterations)
VERIFICATION FAILED

To investigate what was exactly was failing, I added assertions just before the call to partition from quickSort, like this:

void quickSort(int arr[], int low, int high)
__CPROVER_requires(arr != NULL && \
    low >= 0 && high >= 0 && low <= high && high < INT_MAX && \
    __CPROVER_is_fresh(arr, sizeof(int) * (high + 1)))
__CPROVER_ensures(
  __CPROVER_forall{int i; (low <= i && i < high) ==> arr[i] <= arr[i + 1]}
)
__CPROVER_assigns(__CPROVER_object_whole(arr))
{
    // Ensure indices are in correct order
    if (low < high) {
        __CPROVER_assert(arr != NULL,           "arr non-NULL");
        __CPROVER_assert(low  >= 0,             "low ≥ 0");
        __CPROVER_assert(high >= 0,             "high ≥ 0");
        __CPROVER_assert(low  <= high,          "low ≤ high");
        __CPROVER_assert(high < INT_MAX,        "high < INT_MAX");
        // Partition array and get the pivot index
        int i = partition(arr, low, high);
        // Sort the two partitions
        quickSort(arr, low, i - 1); // Left side of pivot
        quickSort(arr, i + 1, high); // Right side of pivot
    }
}

Surprisingly, all the assertions failed except for low ≤ high.

qsort_gold_specs.c function quickSort
[quickSort.assertion.1] line 61 arr non-NULL: FAILURE
[quickSort.assertion.2] line 62 low ≥ 0: FAILURE
[quickSort.assertion.3] line 63 high ≥ 0: FAILURE
[quickSort.assertion.4] line 64 low ≤ high: SUCCESS
[quickSort.assertion.5] line 65 high < INT_MAX: FAILURE
[quickSort.overflow.1] line 69 arithmetic overflow on signed - in i - 1: FAILURE
[quickSort.overflow.2] line 70 arithmetic overflow on signed + in i + 1: FAILURE

This indicates that the predicates in __CPROVER_requires are not being assumed at all when verifying the function body. I observed this behaviour only for the recursive function quickSort using --enforce-contract-rec, not with the other functions.

[remi-delmas-3000]

Hi ! Thanks for reaching out to us.

First, in contract pre conditions you must use __CPROVER_is_fresh(ptr, size) instead of r_ok/w_ok to describe the memory layout of the arguments.

I was able to prove the safety of the partition function using this contract (swap does not really need a contract it is very simple:

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <stddef.h>
#include <limits.h>

// Function that swaps the integer values pointed to by a and b
void swap(int* a, int* b)
{
    int t = *a;
    *a = *b;
    *b = t;
}

// Divides the array into two partitions
int partition(int arr[], int low, int high)
__CPROVER_requires(low >= 0)
__CPROVER_requires(high >= 0)
__CPROVER_requires(low <= high)
__CPROVER_requires(high < INT_MAX)
__CPROVER_requires(__CPROVER_is_fresh(arr, sizeof(int) * (high + 1)))
__CPROVER_ensures(__CPROVER_return_value >= low)
__CPROVER_ensures(__CPROVER_return_value <= high)
__CPROVER_assigns(__CPROVER_object_whole(arr))
{
    int pivot = arr[high]; // Choose the last element as the pivot
    int i = low - 1; // Temporary pivot index
    for (int j = low; j < high; j++)
    __CPROVER_assigns(i, j, __CPROVER_object_whole(arr))
    __CPROVER_loop_invariant(low <= j && j <= high)
    __CPROVER_loop_invariant(low - 1 <= i && i < j)
    __CPROVER_decreases(high-j)
    {
        // If the current element is less than or equal to the pivot
        if (arr[j] <= pivot) {
            // Move the temporary pivot index forward
            i++;
            // Swap the current element with the element at the temporary pivot index
            swap(&arr[i], &arr[j]);
        }
        int i_dummy = i;
    }
    // Swap the pivot with the last element
    swap(&arr[i + 1], &arr[high]);
    return i + 1; // the pivot index
}

void main() {
    int *arr;
    int low;
    int high;
    partition(arr, low, high);
}

goto-cc main.c --function main -o a.out
goto-instrument --dfcc main --enforce-contract partition --apply-loop-contracts a.out b.out
cbmc b.out

main.c function swap
[swap.assigns.1] line 8 Check that the assigns clause of contract::swap is included in the caller's assigns clause: SUCCESS
[swap.frees.1] line 8 Check that the frees clause of contract::swap is included in the caller's frees clause: SUCCESS
[swap.no_alloc_dealloc_in_ensures.1] line 8 Check that ensures do not allocate or deallocate memory: SUCCESS
[swap.no_alloc_dealloc_in_requires.1] line 8 Check that requires do not allocate or deallocate memory: SUCCESS

** 0 of 103 failed (1 iterations)
VERIFICATION SUCCESSFUL

Then I tried to analyse this contract for the quickSort function (I dropped the quantified post condition for now, just trying to prove memory safety)

// Sorts (a portion of) an array, divides it into partitions, then sorts those
void quickSort(int arr[], int low, int high)
__CPROVER_requires(low >= 0)
__CPROVER_requires(high >= 0)
__CPROVER_requires(low <= high)
__CPROVER_requires(high < INT_MAX)
__CPROVER_requires(__CPROVER_is_fresh(arr, sizeof(int) * (high + 1)))
__CPROVER_assigns(__CPROVER_object_whole(arr))
{
    // Ensure indices are in correct order
    if (low < high) {
        // Partition array and get the pivot index
        int i = partition(arr, low, high);
        // Sort the two partitions
        quickSort(arr, low, i - 1); // Left side of pivot
        quickSort(arr, i + 1, high); // Right side of pivot
    }
}

int main() {
    int *arr;
    int low;
    int high;
    quickSort(arr, low, high);
    return 0;
}

(Since we are replacing partition by its contract we don't need to apply loop contracts anymore)

goto-cc main.c -o a.out
goto-instrument --dfcc main --enforce-contract-rec quickSort --replace-call-with-contract partition a.out b.out
cbmc b.out

...

[quickSort.precondition.1] line 57 Check requires clause of contract contract::quickSort for function quickSort: SUCCESS
[quickSort.precondition.2] line 58 Check requires clause of contract contract::quickSort for function quickSort: FAILURE
[quickSort.precondition.3] line 59 Check requires clause of contract contract::quickSort for function quickSort: FAILURE
[quickSort.precondition.4] line 60 Check requires clause of contract contract::quickSort for function quickSort: SUCCESS
[quickSort.overflow.1] line 61 arithmetic overflow on signed + in high_wrapper + 1: SUCCESS
[quickSort.overflow.2] line 61 arithmetic overflow on signed + in high_wrapper + 1: SUCCESS
[quickSort.precondition.5] line 61 Check requires clause of contract contract::quickSort for function quickSort: SUCCESS
[quickSort.overflow.3] line 69 arithmetic overflow on signed - in i - 1: SUCCESS
[quickSort.overflow.4] line 70 arithmetic overflow on signed + in i + 1: SUCCESS

** 2 of 59 failed (3 iterations)
VERIFICATION FAILED

Which indicates that conditions do not hold when going into the recursive calls

__CPROVER_requires(high >= 0)
__CPROVER_requires(low <= high)

Could be because the post condition for the partition contract is too weak and does not constrain its return value enough, allowing to violate the preconditions of quickCheck on the recursive call ?

If you want to prove that the array is going to be sorted as post condition of quickSort you will have to find a quantified loop invariant and post condition for the partition that is strong enough to entail the post condition of the quickSort function

When your contracts involve quantifiers, you have to tell CBMC to use an SMT solver as back end using --z3 or --bitwuzla (which must be installed on your system and available in the path).

[remi-delmas-3000]

I asked Claude to diagnose the problem and it produced this explanation:

> The violation of those preconditions on the recursive calls is likely caused by integer underflow when computing the partition boundaries. Let me analyze the 
specific issue:

## The Problem

In your quickSort function, you make these recursive calls:
c
quickSort(arr, low, i - 1);     // Left partition
quickSort(arr, i + 1, high);   // Right partition


The issue occurs with quickSort(arr, low, i - 1) when i equals low. Here's why:

1. When partition() returns i = low (meaning the pivot was the smallest element)
2. The left recursive call becomes quickSort(arr, low, low - 1)
3. This violates __CPROVER_requires(low <= high) because low > low - 1


The partition() function guarantees that low <= i <= high, but:
• When i = low, then i - 1 = low - 1 < low, violating the precondition
• When i = high, then i + 1 = high + 1 > high, which could also cause issues

with suggested fixes:

void quickSort(int arr[], int low, int high)
__CPROVER_requires(low >= 0)
__CPROVER_requires(high >= 0)
__CPROVER_requires(low <= high)
__CPROVER_requires(high < INT_MAX)
__CPROVER_requires(__CPROVER_is_fresh(arr, sizeof(int) * (high + 1)))
__CPROVER_assigns(__CPROVER_object_whole(arr))
{
    if (low < high) {
        int i = partition(arr, low, high);
        // Only recurse if the partition has valid bounds
        if (low < i) {
            quickSort(arr, low, i - 1);     // Left side of pivot
        }
        if (i < high) {
            quickSort(arr, i + 1, high);   // Right side of pivot
        }
    }
}

I'm able to prove memory safety using

goto-cc main.c -o a.out
goto-instrument --dfcc main --enforce-contract-rec quickSort --replace-call-with-contract partition a.out b.out


** 0 of 59 failed (1 iterations)
VERIFICATION SUCCESSFUL
cbmc b.out  0.19s user 0.01s system 96% cpu 0.209 total

[remi-delmas-3000]

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <stddef.h>
#include <limits.h>

// Function that swaps the integer values pointed to by a and b
void swap(int* a, int* b)
{
    int t = *a;
    *a = *b;
    *b = t;
}

// Divides the array into two partitions
int partition(int arr[], int low, int high)
__CPROVER_requires(low >= 0)
__CPROVER_requires(high >= 0)
__CPROVER_requires(low <= high)
__CPROVER_requires(high < INT_MAX)
__CPROVER_requires(__CPROVER_is_fresh(arr, sizeof(int) * (high + 1)))
__CPROVER_assigns(__CPROVER_object_whole(arr))
__CPROVER_ensures(__CPROVER_return_value >= low)
__CPROVER_ensures(__CPROVER_return_value <= high)
// The pivot is in its final sorted position
__CPROVER_ensures(arr[__CPROVER_return_value] == __CPROVER_old(arr[high]))
// All elements to the left of pivot are <= pivot
__CPROVER_ensures(
  __CPROVER_forall{ int k1; (low <= k1 && k1 < __CPROVER_return_value) ==> 
    arr[k1] <= arr[__CPROVER_return_value] }
)
// All elements to the right of pivot are >= pivot  
__CPROVER_ensures(
  __CPROVER_forall{ int k2; (__CPROVER_return_value < k2 && k2 <= high) ==> 
    arr[k2] >= arr[__CPROVER_return_value]}
)
{
    int pivot = arr[high]; // Choose the last element as the pivot
    int i = low - 1; // Temporary pivot index
    for (int j = low; j < high; j++)
    __CPROVER_assigns(i, j, __CPROVER_object_whole(arr))
    __CPROVER_loop_invariant(low <= j && j <= high)
    __CPROVER_loop_invariant(low - 1 <= i && i < j)
    // Partitioning invariant: elements [low..i] are <= pivot
    __CPROVER_loop_invariant(
      __CPROVER_forall{int k1; (low <= k1 && k1 <= i) ==> arr[k1] <= pivot}
    )
    // Partitioning invariant: elements [i+1..j-1] are > pivot
    __CPROVER_loop_invariant(
      __CPROVER_forall{int k2; (i < k2 && k2 < j) ==> arr[k2] > pivot}
    )
    // The pivot value hasn't changed
    __CPROVER_loop_invariant(arr[high] == pivot)
    __CPROVER_decreases(high-j)
    {
        // If the current element is less than or equal to the pivot
        if (arr[j] <= pivot) {
            // Move the temporary pivot index forward
            i++;
            // Swap the current element with the element at the temporary pivot index
            swap(&arr[i], &arr[j]);
        }
    }
    // Swap the pivot with the last element
    swap(&arr[i + 1], &arr[high]);
    return i + 1; // the pivot index
}

int main_partition() {
    int *arr;
    int low;
    int high;
    partition(arr, low, high);
    return 0;
}

// Sorts (a portion of) an array, divides it into partitions, then sorts those
void quickSort(int arr[], int low, int high)
__CPROVER_requires(low >= 0)
__CPROVER_requires(high >= 0)
__CPROVER_requires(low <= high)
__CPROVER_requires(high < INT_MAX)
__CPROVER_requires(__CPROVER_is_fresh(arr, sizeof(int) * (high + 1)))
__CPROVER_assigns(__CPROVER_object_whole(arr))
__CPROVER_ensures(
  __CPROVER_forall{int i; (low <= i && i < high) ==> arr[i] <= arr[i + 1]}
)
{
    if (low < high) {
        int i = partition(arr, low, high);
        // Only recurse if the partition has valid bounds
        if (low < i) {
            quickSort(arr, low, i - 1);     // Left side of pivot
        }
        if (i < high) {
            quickSort(arr, i + 1, high);   // Right side of pivot
        }
    }
}

int main_quickSort() {
    int *arr;
    int low;
    int high;
    quickSort(arr, low, high);
    return 0;
}

The partition contract is proved:

goto-cc main.c  --function main_partition
goto-instrument --dfcc main_partition --enforce-contract partition --apply-loop-contracts a.out b.out
cbmc b.out

[partition.pointer_dereference.115] line 53 dereference failure: pointer NULL in arr[(signed long int)high]: SUCCESS
[partition.pointer_dereference.116] line 53 dereference failure: pointer invalid in arr[(signed long int)high]: SUCCESS
[partition.pointer_dereference.117] line 53 dereference failure: deallocated dynamic object in arr[(signed long int)high]: SUCCESS
[partition.pointer_dereference.118] line 53 dereference failure: dead object in arr[(signed long int)high]: SUCCESS
[partition.pointer_dereference.119] line 53 dereference failure: pointer outside object bounds in arr[(signed long int)high]: SUCCESS
[partition.pointer_dereference.120] line 53 dereference failure: invalid integer address in arr[(signed long int)high]: SUCCESS
[partition.overflow.5] line 54 arithmetic overflow on signed - in high - j: SUCCESS
[partition.overflow.9] line 54 arithmetic overflow on signed - in high - j: SUCCESS
[partition.overflow.13] line 54 arithmetic overflow on signed - in high - j: SUCCESS
[partition.pointer_dereference.61] line 57 dereference failure: pointer NULL in arr[(signed long int)j]: SUCCESS
[partition.pointer_dereference.62] line 57 dereference failure: pointer invalid in arr[(signed long int)j]: SUCCESS
[partition.pointer_dereference.63] line 57 dereference failure: deallocated dynamic object in arr[(signed long int)j]: SUCCESS
[partition.pointer_dereference.64] line 57 dereference failure: dead object in arr[(signed long int)j]: SUCCESS
[partition.pointer_dereference.65] line 57 dereference failure: pointer outside object bounds in arr[(signed long int)j]: SUCCESS
[partition.pointer_dereference.66] line 57 dereference failure: invalid integer address in arr[(signed long int)j]: SUCCESS
[partition.pointer_dereference.97] line 57 dereference failure: pointer NULL in arr[(signed long int)j]: SUCCESS
[partition.pointer_dereference.98] line 57 dereference failure: pointer invalid in arr[(signed long int)j]: SUCCESS
[partition.pointer_dereference.99] line 57 dereference failure: deallocated dynamic object in arr[(signed long int)j]: SUCCESS
[partition.pointer_dereference.100] line 57 dereference failure: dead object in arr[(signed long int)j]: SUCCESS
[partition.pointer_dereference.101] line 57 dereference failure: pointer outside object bounds in arr[(signed long int)j]: SUCCESS
[partition.pointer_dereference.102] line 57 dereference failure: invalid integer address in arr[(signed long int)j]: SUCCESS
[partition.assigns.1] line 59 Check that i is assignable: SUCCESS
[partition.assigns.3] line 59 Check that i is assignable: SUCCESS
[partition.overflow.6] line 59 arithmetic overflow on signed + in i + 1: SUCCESS
[partition.overflow.10] line 59 arithmetic overflow on signed + in i + 1: SUCCESS
[partition.overflow.14] line 65 arithmetic overflow on signed + in i + 1: SUCCESS
[partition.overflow.15] line 66 arithmetic overflow on signed + in i + 1: SUCCESS

main.c function swap
[swap.pointer_dereference.1] line 10 dereference failure: pointer NULL in *a: SUCCESS
[swap.pointer_dereference.2] line 10 dereference failure: pointer invalid in *a: SUCCESS
[swap.pointer_dereference.3] line 10 dereference failure: deallocated dynamic object in *a: SUCCESS
[swap.pointer_dereference.4] line 10 dereference failure: dead object in *a: SUCCESS
[swap.pointer_dereference.5] line 10 dereference failure: pointer outside object bounds in *a: SUCCESS
[swap.pointer_dereference.6] line 10 dereference failure: invalid integer address in *a: SUCCESS
[swap.assigns.1] line 11 Check that *a is assignable: SUCCESS
[swap.pointer_dereference.7] line 11 dereference failure: pointer NULL in *a: SUCCESS
[swap.pointer_dereference.8] line 11 dereference failure: pointer invalid in *a: SUCCESS
[swap.pointer_dereference.9] line 11 dereference failure: deallocated dynamic object in *a: SUCCESS
[swap.pointer_dereference.10] line 11 dereference failure: dead object in *a: SUCCESS
[swap.pointer_dereference.11] line 11 dereference failure: pointer outside object bounds in *a: SUCCESS
[swap.pointer_dereference.12] line 11 dereference failure: invalid integer address in *a: SUCCESS
[swap.pointer_dereference.13] line 11 dereference failure: pointer NULL in *b: SUCCESS
[swap.pointer_dereference.14] line 11 dereference failure: pointer invalid in *b: SUCCESS
[swap.pointer_dereference.15] line 11 dereference failure: deallocated dynamic object in *b: SUCCESS
[swap.pointer_dereference.16] line 11 dereference failure: dead object in *b: SUCCESS
[swap.pointer_dereference.17] line 11 dereference failure: pointer outside object bounds in *b: SUCCESS
[swap.pointer_dereference.18] line 11 dereference failure: invalid integer address in *b: SUCCESS
[swap.assigns.2] line 12 Check that *b is assignable: SUCCESS
[swap.pointer_dereference.19] line 12 dereference failure: pointer NULL in *b: SUCCESS
[swap.pointer_dereference.20] line 12 dereference failure: pointer invalid in *b: SUCCESS
[swap.pointer_dereference.21] line 12 dereference failure: deallocated dynamic object in *b: SUCCESS
[swap.pointer_dereference.22] line 12 dereference failure: dead object in *b: SUCCESS
[swap.pointer_dereference.23] line 12 dereference failure: pointer outside object bounds in *b: SUCCESS
[swap.pointer_dereference.24] line 12 dereference failure: invalid integer address in *b: SUCCESS

** 0 of 218 failed (1 iterations)
VERIFICATION SUCCESSFUL

However the quickSort contract does not hold, this needs some more tweaking !

[vikramnitin9]

Hi,

Thanks for your reply!

I was able to verify partition according to the previous contracts too. However, for quickSort, the issue is probably not related to the postconditions of partition being too weak. I think it's just a case of the __CPROVER_requires predicates not being translated as assumptions. Seems to be a bug in the implementation of --enforce-contract-rec.

You can cross-check this by adding __CPROVER_assume statements at the beginning of quickSort corresponding to the same conditions in __CPROVER_requires, and re-running verification with these assumptions added.

[vikramnitin9]

I just verified this manually by printing the goto programs using --show-goto-functions, before and after running

goto-instrument --enforce-contract-rec quickSort quicksort.goto checking-quicksort-contracts.goto

quicksort.goto and checking-quicksort-contracts.goto are identical, apart from some differences in the comments. So the goto-instrument --enforce-contract-rec is effectively a no-op.

[remi-delmas-3000]

is effectively a no-op.

--enforce-contract-rec it is not a no-op, it instruments the goto-binary to perform contracts checking for recursive functions.

However it is only effective if you pass in the --dfcc flag with the entry point harness as argument. Have you tried to use the full command lines I've specified above ?

[remi-delmas-3000]

here's the full file I have working on my side:

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <stddef.h>
#include <limits.h>

// Function that swaps the integer values pointed to by a and b
void swap(int* a, int* b)
{
    int t = *a;
    *a = *b;
    *b = t;
}

// Divides the array into two partitions
int partition(int arr[], int low, int high)
__CPROVER_requires(low >= 0)
__CPROVER_requires(high >= 0)
__CPROVER_requires(low <= high)
__CPROVER_requires(high < INT_MAX)
__CPROVER_requires(__CPROVER_is_fresh(arr, sizeof(int) * (high + 1)))
__CPROVER_assigns(__CPROVER_object_whole(arr))
__CPROVER_ensures(__CPROVER_return_value >= low)
__CPROVER_ensures(__CPROVER_return_value <= high)
// The pivot is in its final sorted position
__CPROVER_ensures(arr[__CPROVER_return_value] == __CPROVER_old(arr[high]))
// All elements to the left of pivot are <= pivot
__CPROVER_ensures(
  __CPROVER_forall{ int k1; (low <= k1 && k1 < __CPROVER_return_value) ==> 
    arr[k1] <= arr[__CPROVER_return_value] }
)
// All elements to the right of pivot are >= pivot  
__CPROVER_ensures(
  __CPROVER_forall{ int k2; (__CPROVER_return_value < k2 && k2 <= high) ==> 
    arr[k2] >= arr[__CPROVER_return_value]}
)
{
    int pivot = arr[high]; // Choose the last element as the pivot
    int i = low - 1; // Temporary pivot index
    for (int j = low; j < high; j++)
    __CPROVER_assigns(i, j, __CPROVER_object_whole(arr))
    __CPROVER_loop_invariant(low <= j && j <= high)
    __CPROVER_loop_invariant(low - 1 <= i && i < j)
    // Partitioning invariant: elements [low..i] are <= pivot
    __CPROVER_loop_invariant(
      __CPROVER_forall{int k1; (low <= k1 && k1 <= i) ==> arr[k1] <= pivot}
    )
    // Partitioning invariant: elements [i+1..j-1] are > pivot
    __CPROVER_loop_invariant(
      __CPROVER_forall{int k2; (i < k2 && k2 < j) ==> arr[k2] > pivot}
    )
    // The pivot value hasn't changed
    __CPROVER_loop_invariant(arr[high] == pivot)
    __CPROVER_decreases(high-j)
    {
        // If the current element is less than or equal to the pivot
        if (arr[j] <= pivot) {
            // Move the temporary pivot index forward
            i++;
            // Swap the current element with the element at the temporary pivot index
            swap(&arr[i], &arr[j]);
        }
    }
    // Swap the pivot with the last element
    swap(&arr[i + 1], &arr[high]);
    return i + 1; // the pivot index
}

int main_partition() {
    int *arr;
    int low;
    int high;
    partition(arr, low, high);
    return 0;
}

// Sorts (a portion of) an array, divides it into partitions, then sorts those
void quickSort(int arr[], int low, int high)
__CPROVER_requires(low >= 0)
__CPROVER_requires(high >= 0)
__CPROVER_requires(low <= high)
__CPROVER_requires(high < INT_MAX)
__CPROVER_requires(__CPROVER_is_fresh(arr, sizeof(int) * (high + 1)))
__CPROVER_assigns(__CPROVER_object_whole(arr))
__CPROVER_ensures(
  (low >= high) ||  // Base case: empty or single element
  __CPROVER_forall{int i; (low <= i && i < high) ==> arr[i] <= arr[i + 1]}
)
{
    int dummy_low = low;
    int dummy_high = high;
    if (low < high) {
        int i = partition(arr, low, high);
        int dummy_i = i;
        if (low < i) {                    // Only recurse if the partition has valid bounds
            quickSort(arr, low, i - 1);     // Left side of pivot
        }
        if (i < high) {
            quickSort(arr, i + 1, high);   // Right side of pivot
        }
    }
}

int main_quickSort() {
    int *arr;
    int low;
    int high;
    quickSort(arr, low, high);
    return 0;
}

and the full command lines

For the partition contract proof

goto-cc main.c -o a.out --function main_partition 
goto-instrument --dfcc main_partition --enforce-contract partition --apply-loop-contracts a.out b.out
cbmc --bitwuzla b.out
...
** 0 of 218 failed (1 iterations)
VERIFICATION SUCCESSFUL

goto-cc main.c -o a.out --function main_quickSort
goto-instrument --dfcc main_quickSort --enforce-contract-rec quickSort --replace-call-with-contract partition a.out b.out
cbmc --bitwuzla b.out
...
[quickSort.postcondition.1] line 86 Check ensures clause of contract contract::quickSort for function quickSort: FAILURE
...

** 1 of 126 failed (2 iterations)
VERIFICATION FAILED

The counter example trace reveals the failure happens for values

  low=2147483645 (01111111 11111111 11111111 11111101)
  high=2147483646 (01111111 11111111 11111111 11111110)
  i=2147483646 (01111111 11111111 11111111 11111110)

[vikramnitin9]

Thanks for that clarification! I wasn't using --dfcc and the harness function.

--enforce-contract-rec it is not a no-op, it instruments the goto-binary to perform contracts checking for recursive functions.

Sorry, I didn't mean to imply that it does nothing in general! Just that in this specific case with the way I was running it, it did not modify the goto program. That's because of the incorrect setting, I realize that now.

I have two follow-up questions:

1. I'm unable to run --bitwuzla or --z3 due to this error:

Starting Bounded Model Checking
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA
Running SMT2 QF_AUFBV using Z3
--- begin invariant violation report ---
Invariant check failed
File: ../src/solvers/smt2/smt2_conv.cpp:2600 function: convert_expr
Condition: smt2_convt::convert_expr should not be applied to unsupported expression
Reason: false
Backtrace:
cbmc(+0xb1d353) [0x559e7140c353]
cbmc(+0xb1e473) [0x559e7140d473]
cbmc(+0x1b4767) [0x559e70aa3767]
cbmc(+0x84c2d6) [0x559e7113b2d6]
cbmc(+0x82dbcb) [0x559e7111cbcb]
cbmc(+0x84417c) [0x559e7113317c]
cbmc(+0x844300) [0x559e71133300]
cbmc(+0x85504f) [0x559e7114404f]
cbmc(+0x7dc4cc) [0x559e710cb4cc]
cbmc(+0x2cc43a) [0x559e70bbb43a]
cbmc(+0x2dc6dc) [0x559e70bcb6dc]
cbmc(+0x192093) [0x559e70a81093]
cbmc(+0x18e15e) [0x559e70a7d15e]
cbmc(+0x18576b) [0x559e70a7476b]
cbmc(+0x177398) [0x559e70a66398]
/lib/x86_64-linux-gnu/libc.so.6(+0x2a1ca) [0x7f361b4af1ca]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x8b) [0x7f361b4af28b]
cbmc(+0x186a35) [0x559e70a75a35]

Diagnostics:
<< EXTRA DIAGNOSTICS >>
infinity
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---
Aborted (core dumped)

2. When I run verification on your above program, in addition to the one failed check you had, I have one more:

[__CPROVER_contracts_write_set_check_assignment.assertion.4] line 805 ptr NULL or writable up to size: FAILURE

I'm guessing this is because I'm using the default solver?

[tautschnig]

Could you please add (or point me to, in case it's already in a prior comment in this issue) the exact command line and input program that resulted in the above failure when trying to use an SMT solver?

[remi-delmas-3000]

I'm guessing this is because I'm using the default solver?

when using the default solver some quantified expressions can be ignored (because the internal SAT solver does not handle quantifiers like z3 or bitwuzla do) so you may get spurious counter examples, but no suprious proofs.

[remi-delmas-3000]

The reason why the quicksort post condition fails is that it is too weak to imply itself through recursive calls:

• it just says that elements of the slice from low..high are going to be ordered, but it does not say it is also a permutation of the original array. So the contract allows for behaviours where the elements of the slice processed the recursive would be ordered in postcondition but would lose their relation to the pivot value produced by the partition function.

For this contract to be come inductive, would need to either say that

1. in post, the slice is a permutation of the original slice, which entails that all values in the left and right slices retain their relative ordering with respect to the pivot,
   or
2. propagate ghost min and max values through the program to strengthen the contracts of partition and quicksort (which is what I ended up trying)

[remi-delmas-3000]

Below is the working solution:

#include <stdio.h>
#include <stdlib.h>
#include <stdbool.h>
#include <assert.h>
#include <stddef.h>
#include <limits.h>

// Function that swaps the integer values pointed to by a and b
void swap(int* a, int* b)
{
    int t = *a;
    *a = *b;
    *b = t;
}

// Divides the array into two partitions
int partition(int arr[], int low, int high
#ifdef CBMC
    , int __ghost_min, int __ghost_max
#endif
)
#ifdef CBMC
__CPROVER_requires(low >= 0)
__CPROVER_requires(high >= 0)
__CPROVER_requires(low <= high)
__CPROVER_requires(high < INT_MAX)
__CPROVER_requires(__CPROVER_is_fresh(arr, sizeof(int) * (high + 1)))
__CPROVER_requires(__CPROVER_forall{int k1; (low <= k1 && k1 <= high) ==> (__ghost_min <= arr[k1] && arr[k1] <= __ghost_max)})
__CPROVER_assigns(__CPROVER_object_upto(&arr[low], sizeof(int) * (high-low + 1)))
__CPROVER_ensures(__CPROVER_forall{int k2; (low <= k2 && k2 <= high) ==> (__ghost_min <= arr[k2] && arr[k2] <= __ghost_max)})
__CPROVER_ensures(__CPROVER_return_value >= low)
__CPROVER_ensures(__CPROVER_return_value <= high)
__CPROVER_ensures(arr[__CPROVER_return_value] == __CPROVER_old(arr[high]))
__CPROVER_ensures(__CPROVER_forall{ int k3; (low <= k3 && k3 < __CPROVER_return_value) ==> arr[k3] <= __CPROVER_old(arr[high])})
__CPROVER_ensures(__CPROVER_forall{ int k4; (__CPROVER_return_value < k4 && k4 <= high) ==> arr[k4] >= __CPROVER_old(arr[high])})
#endif
{
    int pivot = arr[high]; // Choose the last element as the pivot
    int i = low - 1; // Temporary pivot index
    for (int j = low; j < high; j++)
#ifdef CBMC
    __CPROVER_assigns(i, j, __CPROVER_object_upto(&arr[low], sizeof(int) * (high-low+1)))
    __CPROVER_loop_invariant(low <= j && j <= high)
    __CPROVER_loop_invariant(low - 1 <= i && i < j)
    __CPROVER_loop_invariant(__ghost_min <= pivot && pivot <= __ghost_max)
    __CPROVER_loop_invariant(__CPROVER_forall{int k1; (low <= k1 && k1 <= i) ==> arr[k1] <= pivot})
    __CPROVER_loop_invariant(__CPROVER_forall{int k2; (i < k2 && k2 < j) ==> pivot < arr[k2]})
    __CPROVER_loop_invariant(__CPROVER_forall{int k3; (low <= k3 && k3 <= high) ==> (__ghost_min <= arr[k3] && arr[k3] <= __ghost_max)})
    // The pivot value hasn't changed
    __CPROVER_loop_invariant(arr[high] == pivot)
    __CPROVER_decreases(high-j)
#endif
    {
        // If the current element is less than or equal to the pivot
        if (arr[j] <= pivot) {
            // Move the temporary pivot index forward
            i++;
            // Swap the current element with the element at the temporary pivot index
            swap(&arr[i], &arr[j]);
        }
    }
    // Swap the pivot with the last element
    swap(&arr[i + 1], &arr[high]);
    return i + 1; // the pivot index
}

#ifdef CBMC
int main_partition() {
    int *arr;
    int low;
    int high;
    int __ghost_min;
    int __ghost_max;
    partition(arr, low, high, __ghost_min, __ghost_max);
    return 0;
}
#endif

// Sorts (a portion of) an array, divides it into partitions, then sorts those
void quickSort(int arr[], int low, int high
// we implement ghost parameters using macros
#ifdef CBMC
    , int __ghost_min, int __ghost_max
#endif
)
#ifdef CBMC
// bounds are ordered
__CPROVER_requires(low >= 0)
__CPROVER_requires(high >= 0)
__CPROVER_requires(low <= high)
// we avoid overflows thanks to this constraint
__CPROVER_requires(high < INT_MAX)
// we have some allocated memory
__CPROVER_requires(__CPROVER_is_fresh(arr, sizeof(int) * (high + 1)))
// we have an interval for all the values in the array
__CPROVER_requires(__CPROVER_forall{int k1; (low <= k1 && k1 <= high) ==> (__ghost_min <= arr[k1] && arr[k1] <= __ghost_max)})
// we only assign the required slice
__CPROVER_assigns(__CPROVER_object_upto(&arr[low], sizeof(int) * (high-low+1)))
// the array elements are still within the same bounds
__CPROVER_ensures(__CPROVER_forall{int k2; (low <= k2 && k2 <= high) ==> (__ghost_min <= arr[k2] && arr[k2] <= __ghost_max)})
// and they are sorted in weak increasing order
__CPROVER_ensures(__CPROVER_forall{int k3; (low <= k3 && k3 < high) ==> arr[k3] <= arr[k3 + 1]})
#endif
{
    // we propagate the initial bounds throughout the computation
    if (low < high) {
        int i = partition(arr, low, high
            #ifdef CBMC
            , __ghost_min, __ghost_max
            #endif
        );
        // partitioning preserves min and max bounds over the whole slice
        if (low < i) {
            // all elements to the left are between the min and the pivot
            quickSort(arr, low, i - 1
            #ifdef CBMC
                ,__ghost_min, arr[i]
            #endif
            );
        }
        if (i < high) {
            // all elements to the right are between the pivot and the max
            quickSort(arr, i + 1, high
            #ifdef CBMC
                ,arr[i], __ghost_max
            #endif
            );
        }
    }
}

#ifdef CBMC
int main_quickSort() {
    int *arr;
    int low;
    int high;
    int __ghost_min;
    int __ghost_max;
    quickSort(arr, low, high, __ghost_min, __ghost_max);
    return 0;
}
#endif

# Makefile for CBMC analysis of quicksort implementation
# Analyzes partition and quickSort functions with contracts

# Variables
CC = goto-cc
INSTRUMENT = goto-instrument
CBMC = cbmc
SOURCE = main.c
PARTITION_SOLVER = --bitwuzla
QUICKSORT_SOLVER = --bitwuzla
CFLAGS = -DCBMC

# Default target
.PHONY: all clean partition quicksort help partition-program quicksort-program partition-smt2 quicksort-smt2

all: partition quicksort

# Analyze partition function
partition: partition.out
	@echo "=== Analyzing partition function ==="
	time $(CBMC) $(PARTITION_SOLVER) partition.out

partition.out: partition_instrumented.out
	@cp partition_instrumented.out partition.out

partition_instrumented.out: partition_compiled.out
	$(INSTRUMENT) --dfcc main_partition --enforce-contract partition --apply-loop-contracts partition_compiled.out partition_instrumented.out

partition_compiled.out: $(SOURCE)
	$(CC) $(CFLAGS) $(SOURCE) -o partition_compiled.out --function main_partition

# Analyze quickSort function
quicksort: quicksort.out
	@echo "=== Analyzing quickSort function ==="
	time $(CBMC) $(QUICKSORT_SOLVER) quicksort.out

quicksort.out: quicksort_instrumented.out
	@cp quicksort_instrumented.out quicksort.out

quicksort_instrumented.out: quicksort_compiled.out
	$(INSTRUMENT) --dfcc main_quickSort --enforce-contract-rec quickSort --replace-call-with-contract partition quicksort_compiled.out quicksort_instrumented.out

quicksort_compiled.out: $(SOURCE)
	$(CC) $(CFLAGS) $(SOURCE) -o quicksort_compiled.out --function main_quickSort

# Run both analyses
verify: partition quicksort
	@echo "=== Both analyses completed ==="

# Clean up generated files
clean:
	rm -f *.out *.txt *.smt2

# Program-only output targets
partition-program: partition.out
	@echo "=== Generating program-only output for partition function ==="
	$(CBMC) $(PARTITION_SOLVER) --program-only partition.out > partition_program.txt

quicksort-program: quicksort.out
	@echo "=== Generating program-only output for quickSort function ==="
	$(CBMC) $(QUICKSORT_SOLVER) --program-only quicksort.out > quicksort_program.txt

# SMT2 file generation targets
partition-smt2: partition.out
	@echo "=== Generating SMT2 file for partition function ==="
	$(CBMC) $(PARTITION_SOLVER) --outfile partition.smt2 partition.out

quicksort-smt2: quicksort.out
	@echo "=== Generating SMT2 file for quickSort function ==="
	$(CBMC) $(QUICKSORT_SOLVER) --outfile quicksort.smt2 quicksort.out

# Show available targets
help:
	@echo "Available targets:"
	@echo "  all               - Run both partition and quicksort analysis (default)"
	@echo "  partition         - Analyze partition function only"
	@echo "  quicksort         - Analyze quickSort function only"
	@echo "  verify            - Run both analyses with summary"
	@echo "  partition-program - Generate program-only output for partition (saves to partition_program.txt)"
	@echo "  quicksort-program - Generate program-only output for quickSort (saves to quicksort_program.txt)"
	@echo "  partition-smt2    - Generate SMT2 file for partition (saves to partition.smt2)"
	@echo "  quicksort-smt2    - Generate SMT2 file for quickSort (saves to quicksort.smt2)"
	@echo "  clean             - Remove generated files"
	@echo "  help              - Show this help message"

# Declare intermediate files as secondary to prevent deletion
.SECONDARY: partition_compiled.out partition_instrumented.out quicksort_compiled.out quicksort_instrumented.out

These are the times on an M4 Pro macbook pro 14" using bitwuzla 0.8.1 and cbmc 6.7.1.

make partition
...
** 0 of 293 failed (1 iterations)
VERIFICATION SUCCESSFUL
       14.48 real        14.20 user         0.26 sys 

make quicksort
...
** 0 of 225 failed (1 iterations)
VERIFICATION SUCCESSFUL
      360.54 real       354.46 user         5.85 sys

But this contract is still kind of weak since it allows sorting functions that would replace elements of the original array with any other elements as long as they are ordered and in the original range of values.

@tautschnig I still see that some byte_update expressions caused by havoc_slice operations turn into gigantic expressions at the SMT-level, i.e. our recent optimization does not kick in for things like this:

__CPROVER_assigns(__CPROVER_object_upto(&arr[low], sizeof(int) * (high-low + 1)))

And overall it is still a bit slow to prove (360s)