Add sound models for common C standard-library input and arithmetic functions

[shaobo-he]

Summary

SMACK should provide sound, reusable models for common C standard-library functions instead of treating known library calls as ordinary bodyless externals. The initial gaps covered by this issue are:

• formatted input through fscanf and its implementation aliases;
• integer absolute-value functions such as abs and imaxabs;
• square-root functions such as sqrt and sqrtl.

This is a general C-library modeling issue. It affects any analyzed program that uses these APIs, independently of SV-COMP.

Problem

Treating a standard-library call as a bodyless procedure has different consequences depending on the function:

• Effectful functions can make verification unsound. A bodyless fscanf procedure has no memory effects, so values that should be written through output pointers remain unchanged. SMACK may prove a program safe after omitting feasible executions.
• Pure functions lose essential relations. Bodyless abs/imaxabs and sqrt/sqrtl procedures return unrelated values. This is an overapproximation, but it creates infeasible paths and false counterexamples in code that uses their results in guards.

The implementation should also establish a general fallback policy for recognized but unsupported library calls. In particular, an unsupported effectful function must not silently become an effect-free procedure.

Initial scope

Formatted input

Model fscanf and common implementation aliases such as __isoc99_fscanf. For supported conversions, the model should capture at least:

• successful conversion writes a value representable by the destination type and contributes to the returned assignment count;
• input or matching failure may return before assignment and leave the destination unchanged;
• writes through variadic output pointers are reflected in SMACK's memory model;
• multiple conversions preserve their ordering and partial-success behavior.

Constant format strings and integer conversions (%d, %u, %ld, and related length modifiers) would be a useful first increment. The design should be reusable for the scanf, fscanf, and sscanf families rather than relying on benchmark-specific call patterns.

If a format cannot be interpreted, SMACK should conservatively model possible effects, emit a clear unsupported-feature diagnostic, or return UNKNOWN. It should not prove safety using an empty modifies set.

Integer absolute value

For inputs whose absolute value is representable, models for abs, labs, llabs, and imaxabs should relate the return value to the argument and preserve the correct integer width.

The minimum signed value must follow a documented SMACK policy for standard-library undefined behavior. C11 specifies undefined behavior when the absolute value cannot be represented; the model must not silently assign an arbitrary defined result in that case.

Square root

SMACK already implements sqrt and sqrtl in share/smack/lib/math.c, but those models are linked only when --float is enabled. The behavior should be explicit and consistent:

• use the existing floating-point models when floating-point semantics are enabled;
• when full floating-point reasoning is disabled, either provide a sound relational abstraction, diagnose the unsupported call, or return UNKNOWN;
• do not produce a concrete error report whose feasibility depends only on an arbitrary return from an unmodeled standard function.

Design requirements

• Dispatch by standard-library identity, including compiler intrinsics and platform aliases where applicable, without depending on source-file or benchmark names.
• Keep models compatible with SMACK's memory models and integer encodings.
• Distinguish pure unknown functions from functions that may write through pointer arguments or global state.
• Make flag-dependent model availability visible to users.
• Add a documented policy for unresolved external functions so that missing models cannot silently remove side effects.

Regression tests

Add small, standalone C tests covering:

• successful, failed, and partially successful formatted input;
• an input value that reaches a signed-overflow check;
• safe and unsafe guarded arithmetic using abs/imaxabs and sqrt/sqrtl;
• the minimum signed argument to each absolute-value function;
• glibc aliases such as __isoc99_fscanf;
• behavior with and without --float.

Observed impact

The missing models were exposed by an SV-COMP 2026 Juliet no-overflow run using SMACK develop commit a33d1bdf:

• 722 false negatives belonged to fscanf_*_bad families. Representative generated BPL declared __isoc99_fscanf without a body or memory effects, leaving the destination at its initializer.
• 266 false positives belonged to guarded square families using abs/imaxabs and sqrt/sqrtl. Unrelated return values made infeasible overflow paths appear feasible.

These benchmarks are evidence of the general modeling problem, not the intended boundary of the implementation.

One benchmark caveat should not be encoded as a SMACK requirement: the current SV-COMP *_bad_abs tasks execute imaxabs(INTMAX_MIN). Upstream SV-Benchmarks MR !1523 identifies this as unintended undefined behavior and proposes an explicit overflowing multiplication instead.

References:

• SV-COMP 2026 rules
• C11 draft N1570

[shaobo-he]

Another instance of the fallback policy this issue asks for, and a case where the current default is unsound rather than imprecise.

The string functions are modelled in share/smack/lib/string.c, but that file is only linked with --strings. Without it they are bodyless externals, so their memory accesses are neither performed nor checked:

#include "smack.h"
#include <stdlib.h>
#include <string.h>
int main(void) {
  char *p = malloc(0);
  size_t n = strlen(p);   // reads byte 0 of a block with no bytes
  free(p);
  return (int)n;
}

smack strzero.c --check=memory-safety --verifier=corral (develop @ 9dca4d9, --mem-mod no-reuse-impls, with #853 so that the block is real and inaccessible):

flags	result
default	verified — the invalid read is missed
--strings	error: invalid pointer dereference

The emitted Boogie has procedure strlen($p0: ref); with no body. memcpy and memset are LLVM intrinsics and are checked either way, which is why the same program written with memset is caught by default — so within one program some library reads are checked and others silently are not, depending on whether the call lowered to an intrinsic.

This is the policy point in the description: a recognized but unmodelled effectful function should not become an effect-free procedure. For the string family the model already exists, so the narrower question is whether --strings should be on by default, or at least implied by --check=memory-safety.