goblint / goblint/analyzer

Strongly update-able `calloc` blobs for more precise zstd analysis

Open
#702 3 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

benchmarking feature precision
Dominant language
OCaml
Stars
252
Forks
90
Avg merge
4d 1m
Merged PRs (30d)
19

Description

Problem

Our analysis of zstd ends up with unexpectedly many unknown pointers due to the following sequence of coincidences.

Thread pool and its queue

In zstd's POOL_create_advanced, the thread pool and its queue are allocated on the heap as follows (simplified):

ctx = (POOL_ctx*)ZSTD_customCalloc(sizeof(POOL_ctx), customMem);
ctx->queueSize = queueSize + 1;
ctx->queue = (POOL_job*)ZSTD_customMalloc(ctx->queueSize * sizeof(POOL_job), customMem);
ctx->queueHead = 0;
// ...

Here ctx and both alloc variables are in the local state. Thanks to #686 the alloc variables escape into global state correctly.

When jobs are added to the queue, their function pointers are nicely joined into the queue's alloc variable, which precisely contains known function pointers and no NULL or unknown pointer.

However later in the thread pool threads, they retrieve jobs from the queue using ctx->queue[ctx->queueHead], i.e. *(ctx->queue + ctx->queueHead) after CIL normalization. Confusingly, the function pointer in the returned job struct contains an additional unknown pointer, despite the queue's alloc variable not containing one.

Extensive invalidation

Turns out this is because ctx's alloc variable also has a NULL pointer possible for the queue field. When pointer arithmetic is applied (and queueHead is no longer constant either), the known alloc pointer is nicely kept, but the NULL pointer is replaced by an unknown pointer using this code:
https://github.com/goblint/analyzer/blob/313793681ce98d1ea2db0e5f853615dd3050095f/src/analyses/base.ml#L208-L214

Analyzing zstd, the unknown function pointer is absolutely disastrous effect:

  1. An unknown function pointer call is analyzed by special to invalidate its arguments.
  2. In zstd, one of the thread pool jobs is passed an argument, which inside it contains a pointer to the same thread pool ctx.
  3. The resulting invalidation is extensive and invalidates:
    • ctx alloc variable (so an unknown pointer is added to queue's address set directly as well),
    • queue alloc variable (so NULL and unknown pointers are added to the job's function pointer and argument sets),
    • all the argument structs for all the jobs (holding all of the relevant data) are totally invalidated.
Culprit

The culprit of all of this is the NULL pointer in the queue field. If we didn't have that there, none of this invalidation would have happened!
Tracking this down was a two-day job since the cyclic pointing structure means that everything ends up being invalidated and it's impossible to tell from the final results, where this imprecision originated from. Moreover, it's practically impossible to trace Goblint when the problematic analysis takes over 40 minutes and produces way too much tracing output (and not to mention being slowed down by all the I/O).

Solution

Ideally, Goblint should know that queue cannot be a NULL pointer, avoiding all of the above. The source of the NULL pointer in the first place is that ctx is allocated using calloc. But clearly that NULL pointer is overwritten before ctx is seen by any other code, so it should be avoidable.

Although simple on the surface, to be able to strongly update the queue field requires many big pieces to work together:

  1. #186 is needed to know that we have a uniquely allocated blob, otherwise strong updates wouldn't be sound.
  2. ValueDomain.update_offset must use that uniqueness information to replace the weak (joining) update with a strong (replacing) one here: https://github.com/goblint/analyzer/blob/313793681ce98d1ea2db0e5f853615dd3050095f/src/cdomains/valueDomain.ml#L900-L904
  3. Even that would not be enough, because calloc creates an abstract array of blobs: https://github.com/goblint/analyzer/blob/313793681ce98d1ea2db0e5f853615dd3050095f/src/analyses/base.ml#L2261
    Therefore that array update also needs to be strong, not weak. In zstd's case (and very commonly), calloc is used with a count of 1, so we get an array of length 1. Hence the array domain(s) should be specialized for the length 1 case to just do strong updates instead.
    (After #145 there's probably a bug in that calloc code because it always creates an array of length 1, instead of using the count from the calloc argument.)
  4. Even with all of the above, I'm not sure if we'd be precise enough, because in zstd thread pools may be created when Goblint is in multithreaded mode, so it might even be necessary to incorporate #690 into the uniqueness and privatization to always have a local strongly update-able copy of the blob.

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start with the cited update_offset code in src/cdomains/valueDomain.ml and calloc handling in src/analyses/base.ml. Read issues #186, #690, and #145 to understand uniqueness, privatization, and calloc array behavior, then run the zstd analysis. Done means calloc-backed fields can be strongly updated without introducing the NULL-derived unknown pointers described here.

Written by the indexing model from the issue text.

Assessment

Tech stack
c, ocaml
Domain
compilers, tooling
Issue type
Feature
Difficulty
5/5
Estimated time
Over a week
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
32/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.