[SwayamInSync]

Plan item B13 (library primitives): memcpy, memmove, memset, memcmp, and abs stopped their functions. Stacked on #117 (B11, on #116), whose commits it shows until those merge.

On the base

The example below (with this PR's output further down):

memory.cpp:9:3: error: copy: call to function without a verification contract: memcpy
    9 |   memcpy(dst, src, n * sizeof(int));
      |   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
memory.cpp:16:10: error: same: call to function without a verification contract: memcmp
   16 |   return memcmp(a, b, n * sizeof(int)) == 0;
      |          ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Summary: 2 unresolved (construct.unsupported 2) in 0.0 s

abs was the same error. The coverage investigation counted about 92 uses of these and the string functions in 29 files of LLVM's lib/Support.

With this PR

#include <cstring>

void copy(int *dst, const int *src, int n)
  cv::pre(cv::valid(dst, n) && cv::valid(src, n) && 0 <= n && n <= 1000)
  cv::modifies(dst[0 : n])
  cv::post(cv::forall(k, 0, n, dst[k] == src[k]))
{
  memcpy(dst, src, n * sizeof(int));
}

bool same(const int *a, const int *b, int n)
  cv::pre(cv::valid(a, n) && cv::valid(b, n) && 0 <= n && n <= 1000)
  cv::post(cv::result == cv::forall(k, 0, n, a[k] == b[k]))
{
  return memcmp(a, b, n * sizeof(int)) == 0;
}

Verified: copy [backend=z3] [trusts=memcpy]
Verified: same [backend=z3] [trusts=memcmp]

Design, from the references

• Frama-C's libc (share/libc/string.h) states these functions in ACSL over bytes, through (char *) casts: valid_or_empty(dest, n), \separated ranges for memcpy, assigns dest[0..n-1] \from src[0..n-1], and logic functions memcmp, memset, strlen. That needs a memory of bytes, which WP's Typed+Cast model and Eva have. CBMC's memory is bytes too.
• cpp-verify's memory keeps one value per object. The plan said to ship trusted models in a header, but a contract on void * cannot speak of the objects behind it, and an overload in <cppverify.h> would change overload resolution and need a definition at link time.

So the models are contracted declarations in <cppverify.h>, in cppverify::model, one per type of object (every integer type, and bool for copies and comparisons), readable as C++:

[[cppverify::trusted]] int *memcpy(int *d, const int *s, size_t k)
  cppverify::pre(cppverify::valid(d, k) && cppverify::valid(s, k))
  cppverify::modifies(d[0 : k])
  cppverify::post(cppverify::forall(i, 0, k, d[i] == cppverify::old(s[i])))
  cppverify::post(cppverify::result == d);

ASTConverter::convertLibraryCall recognizes the four functions by builtin ID (memcpy, std::memcpy, __builtin_memcpy, ...), reads the objects each pointer addresses as written, before its conversion to void * (an enumeration as its underlying integer), and lowers the call to a call of that type's model with k = n / sizeof(T). The modular call then does the rest, as for any callee: each extent lies in the caller's object, memcpy's two ranges are separate (two pointer parameters of which one is mutable; memmove's model has aliases), the frame is d[0 : k], and the postconditions hold after it.

• memset(d, c, n): the model takes the object every byte of which is (unsigned char)c, (unsigned char)c * 0x0101... reinterpreted as T, exact for any width and byte order.
• memcmp: 0 exactly when the objects are equal; of bytes, negative exactly when the first difference is smaller as unsigned char. Of wider objects the sign depends on the byte order, which is not modeled.
• A size that splits an object (memcpy(d, s, 6) of int) is defined C++ that this memory cannot represent: an unsupported obligation that n % sizeof(T) == 0, with a note (VAssertStmt::Note, new, passed to the passive statement's).
• Records, pointers, void *, and objects of two sizes are an error naming the types: memcpy of 'Pt *' and 'const Pt *' is unsupported: it is modeled for pointers to integers of one size.

The models are trusted, as the C library is, so every proof that uses one says so ([trusts=memcpy]), and through its callers too. They are converted only where a call uses one (UsedLibraryModels, after the main loop, which skips cppverify::model) and marked IsBuiltin: not verified, not reported, and still trusted for the fixpoint and [trusts=...]. Without that, every file would print one Trusted: line per model.

abs, labs, llabs, and std::abs of an integer are their definition, x < 0 ? -x : x in the parameter's type in the function's integer mode (convertAbs): abs(INT_MIN) is an overflow in executable code, in a contract too, and in a spec, whose integers are mathematical, abs is the absolute value.

Shifted ranges, found here

memmove(a, a + 1, ...) timed out: no quantified claim about a copy between shifted ranges was proved, with any callee. A callee's quantifier that reads through a slice actual base + c is restated over base's indices (rebaseSliceBinders, j := k - c), so that the caller's reads trigger it. It took the first offset it found, though, and a quantifier that reads one pointer directly and another through b + 1 was restated for b + 1, which the reads of the other no longer match. It also did not look under a cast, which every Boolean result has (cv::result == cv::forall(...)).

Now a quantifier is restated when all the loads its binder indexes go through one slice offset (collectSliceOffsets, SliceUse). With several offsets, or a direct load beside a slice, an assumed postcondition keeps the quantifier and adds its restatement over each slice's base: equivalent formulas, each with the triggers of its own form, so the caller's reads trigger one of them. A check (a precondition at a call) is left as it is, since the solver would have to prove each form. memmove(a, a + 1, ...) and memmove(a + 1, a, ...) now verify at once, and so does a user's copy between shifted arrays.

Mutants

Each mutant below, applied alone and rebuilt, is caught by library_models.cpp or slice_quantifier_offsets.cpp (18 of 18). M15 first survived as "abs of a contract is mathematical": inside an executable function the integer mode is machine, contracts included, so it changed only specs, where the absolute value is the right meaning; abs now takes the function's mode, and a spec test catches the machine reading.

Mutant	Change
M1	memcpy is not lowered
M2	the element type is read after the conversion to void *
M3	an enumeration is not its underlying integer
M4	objects of two sizes are copied
M5	a bool is copied from a char
M6	the arguments are not checked for their order
M7	memset stores its byte unrepeated
M8	memset does not reduce c to a byte
M9	the size is not divided into objects
M10	a size that splits an object is not checked
M11	an assert loses its note
M12	the models are reported
M13	every model is converted
M14	abs is the argument
M15	abs in a spec is of machine integers
M16	mixed offsets are restated over the first only
M17	an assumption with mixed offsets is not restated
M18	a cast hides a quantifier from rebasing

Tests

• suite/library_models.cpp (new): memcpy of int (and through a caller, with std::memcpy), of an enumeration over unsigned char; memmove to both sides; memset to 0, to 0xff (each int is -1), and to a byte of unsigned char; memcmp as equality of ints and as order of bytes; failures: a fill claimed 1 where each int is 0x01010101, an overlapping memcpy (aliasing), one past the end (bounds); a size that splits an object (construct.unsupported); records (an error); abs and std::abs verified, at the minimum (overflow), and in a contract.
• suite/slice_quantifier_offsets.cpp (new): copies between shifted ranges both ways and a Boolean callee result over a shifted slice, with --timeout=5000; the passive dumps show the quantifier restated (one offset) and kept beside its restatement (two).
• Differential execution: cases/library.py (new suite library, 36 cases) runs each function of the real C library on 200 random buffers, guard pages around them, under contracts verified with the models: memcpy, memset, and memcmp for nine integer types, memmove both ways, byte order, abs, labs. No run breaks a verified contract, and the false claims (a copy that changes nothing, a fill that stores c, a comparison always 0, abs of the minimum) fail with real counterexamples: 36 cases, 0 problems. cvc5 leaves most of the memory cases unknown.

On the base all 23 functions of library_models.cpp are unresolved (call to function without a verification contract), and in slice_quantifier_offsets.cpp shifted and both_shifted time out (shifted_target verifies there: the first offset the old rule found was the destination's, which its reads match).

The whole Verify suite runs in this PR's CI (Linux release and assertions, macOS, Windows).

Docs

• Pointers: a section, "The C library's memory functions", with the models, an example and its output, and what is not modeled;
• limitations: the library section;
• release notes; ARCHITECTURE (the lowering, the models, rebasing); DESIGN.

Not done

• strlen and the other string functions: a terminator must lie in the string's object, whose end the converter does not know.
• Records and pointers in the memory functions (memset(&s, 0, sizeof s)), field by field.

Stacked on #117.

Found by macOS CI

library_models.cpp failed on macOS: distance (std::abs of a long) was construct.unsupported. libc++ defines abs(long) and abs(long long) in the global namespace of its <stdlib.h>, and its <cstdlib> brings them into std with using ::abs, where libstdc++ defines them in std itself; the model recognized only the latter. A global abs declared in a system header is now std::abs too, and an abs of the user's own is still a function like any other. library_abs_global.cpp (new) mimics libc++'s header (Inputs/global_abs.h, a system header): it fails on the previous head, and fails when the system-header condition is dropped (a user's abs(long) returning x would be taken as the absolute value). The other macOS failure, confirmation_invariants.cpp, is the flake #115 fixes.