Proper handling of library and __CPROVER built-in functions in contracts

[feliperodri]

CBMC version: 5.67.0
Operating system: N/A

These classes of functions need special care during contract instrumentation:

• Built-in __CPROVER functions
  • they have no written implementation and need to be treated in an ad-hoc manner during instrumentation
• __CPROVER library functions (have a written implementation)
• POSIX library functions:
  • implemented in C on top of built-in functions (src/ansi-c/library/*.c)
  • can have loops, allocate/free memory, perform writes
  • write to global instrumentation variables used to track object sizes, lifetimes, memory leaks, etc.

In the current workflow, instrumentation is performed on user code before __CPROVER or POSIX libraries get added the goto model. This is done on purpose, to avoid dragging internal CBMC machinery in user contracts (library functions), and also to avoid instrumenting the body of trusted functions, and to avoid bringing loops that have no contracts in the instrumentation phase.

As a consequence:

1. except for malloc and free, writes performed by built-in and library function are ignored in assigns clause checking (unsound)
2. once library functions are loaded, new loops appear that need to be unrolled for analysis (prevents unbounded proofs)

As of today (Dec 1st 2021):

• For point 1. we treat calls to malloc and free in an ad-hoc manner during instrumentation
• For point 2. we unwind library function loops in a subsequent pass to make the analysis possible

Steps to improve:

• Built-ins: no choice but ad-hoc handling
• Read-only, loop-free library functions:
  • Add them to the project and instrument their bodies (sound but will cause a performance hit)
  • Skip the instrumentation of their bodies (better performance but puts them in the trusted code base)
• Library functions with loops:
  • equip with full-fledged loop contracts or function contracts and treat them as regular functions
  • Handle them in an ad-hoc manner during instrumentation without instrumenting their bodies
  • Inline them before contract instrumentation and ignore writes to global __CPROVER instrumentation variables during assigns clause instrumentation

The key with these functions is to avoid dragging the __CPROVER internals into user contracts