Skip to main content

Module spec

saf_core

Module spec 

Source
Expand description

Function specification system for external/library function modeling.

This module provides a pluggable system for describing the behavior of external functions (libc, POSIX, user libraries) that cannot be analyzed directly. Specs are used by various analyses:

  • PTA: Memory allocation, aliasing, pointer returns
  • Nullness: Pre/post-conditions on pointer validity
  • Taint: Sources, sinks, sanitizers, propagation rules
  • Interval: Numeric return bounds

§Spec Format

Specs are defined in YAML files with version “1.0”:

version: "1.0"
specs:
  - name: malloc
    role: allocator
    returns:
      pointer: fresh_heap
      nullness: maybe_null
    params:
      - index: 0
        semantic: allocation_size

§Name Matching

  • Exact: name: malloc
  • Glob: name: "glob:str*"
  • Regex: name: "regex:^mem(cpy|set|move)$"

§Discovery Order

Specs are loaded from multiple paths (later overrides earlier per-function):

  1. <binary>/../share/saf/specs/*.yaml — shipped defaults
  2. ~/.saf/specs/*.yaml — user global
  3. ./saf-specs/*.yaml — project local
  4. $SAF_SPECS_PATH/*.yaml — explicit override

§Example

use saf_core::spec::{SpecRegistry, FunctionSpec, Role};

// Load from default paths
let registry = SpecRegistry::new(); // Empty for now

// Programmatic construction
let mut registry = SpecRegistry::new();
let mut spec = FunctionSpec::new("my_alloc");
spec.role = Some(Role::Allocator);
registry.add(spec).unwrap();

if let Some(spec) = registry.lookup("my_alloc") {
    assert_eq!(spec.role, Some(Role::Allocator));
}

Modules§

analyzed 🔒
Layered spec registry combining YAML-authored specs with analysis-derived facts.
derived 🔒
Analysis-derived function specifications.
pattern 🔒
Name pattern matching for function specifications.
registry 🔒
Spec registry for loading and querying function specifications.
schema 🔒
YAML schema parsing and validation for function specifications.
types 🔒
Type definitions for function specifications.

Structs§

AnalyzedSpecRegistry
A layered spec registry that combines immutable YAML-authored specs with mutable analysis-derived overlays.
ComputedBound
A computed return bound: return interval depends on an argument property.
DerivedSpec
Analysis-derived specification for a function.
FunctionSpec
A function specification describing external/library function behavior.
ParamSpec
Per-parameter specification.
ReturnSpec
Return value specification.
SpecFile
A spec file containing multiple function specifications.
SpecRegistry
A registry of function specifications.
TaintPropagation
A single taint propagation rule.
TaintSpec
Taint propagation specification.

Enums§

BoundMode
How a return value is bounded by an argument property.
LookupResult
Result of looking up a function in the analyzed registry.
NamePattern
A name pattern for matching function names.
Nullness
Nullness requirements and guarantees for pointers.
PatternError
Errors that can occur when parsing patterns.
Pointer
Describes what a returned pointer points to.
RegistryError
Errors that can occur when loading the registry.
Role
High-level role of a function for analysis purposes.
SchemaError
Errors that can occur when parsing spec files.
TaintLocation
A location in taint propagation rules.

Constants§

CURRENT_VERSION
The current spec file format version.