Closed
Description
(We ran into this issue in practice for mlkem-native, where a bad spec led to a successful proof)
It seems that using __CPROVER_is_fresh in disjunctive preconditions is problematic. When __CPROVER_is_fresh is evaluated for a contract verification, it seems to always succeed, leading to the alternative precondition to be ignored. When applying the contract, however, the alternative precondition can be used.
An ad-hoc workaround is to reorder the clauses to use __CPROVER_is_fresh as late as possible, but a more robust approach should be sought?
// instructions
//
// bad_spec:
// goto-cc harness.c --function bad_spec_harness -o a.out
// goto-instrument --dfcc bad_spec_harness --enforce-contract bad_spec a.out b.out
// cbmc b.out --bitwuzla
//
// bad_use:
// goto-cc harness.c --function bad_use_harness -o a.out
// goto-instrument --dfcc bad_use_harness --replace-call-with-contract bad_spec a.out b.out
// cbmc b.out --bitwuzla
#include <stdlib.h>
#include <stdint.h>
#include <stdbool.h>
void bad_spec(uint8_t *x)
__CPROVER_requires(
/* Case A -- pointers valid */
__CPROVER_is_fresh(x, 10)
/* Case B -- void preconditions */
|| true)
__CPROVER_assigns(__CPROVER_object_whole(x))
{
x[9] = 42;
}
void bad_spec_harness(void) {
int8_t *x;
bad_spec(x);
}
void bad_use()
{
uint8_t x[5];
bad_spec(x);
}
void bad_use_harness(void) {
bad_use();
}