saf_core/spec/
derived.rs

1//! Analysis-derived function specifications.
2//!
3//! These types represent function contract information discovered by
4//! static analysis, as opposed to YAML-authored `FunctionSpec` entries.
5
6use std::collections::BTreeMap;
7
8/// How a return value is bounded by an argument property.
9#[derive(Debug, Clone, PartialEq, Eq)]
10pub enum BoundMode {
11    /// Return ∈ `[0, alloc_size(param) - 1]`.
12    /// Models: `strlen(buf)`, `strnlen(buf, n)` (first arg).
13    AllocSizeMinusOne,
14    /// Return ∈ `[0, alloc_size(param)]`.
15    /// Models: `fread(buf, 1, size, fp)` where size = `alloc_size(buf)`.
16    AllocSize,
17    /// Return ∈ `[-1, param_value - 1]`.
18    /// Models: `read(fd, buf, count)` returns `[-1, count-1]`.
19    ParamValueMinusOne,
20}
21
22/// A computed return bound: return interval depends on an argument property.
23#[derive(Debug, Clone, PartialEq, Eq)]
24pub struct ComputedBound {
25    /// Which parameter's property bounds the return value.
26    pub param_index: u32,
27    /// How the return is bounded.
28    pub mode: BoundMode,
29}
30
31/// Analysis-derived specification for a function.
32///
33/// Produced by the summary module and merged with YAML specs in
34/// `AnalyzedSpecRegistry`.
35#[derive(Debug, Clone, PartialEq, Eq)]
36pub struct DerivedSpec {
37    /// Computed return interval bound (if applicable).
38    pub computed_return_bound: Option<ComputedBound>,
39    /// Whether the callee frees `param[i]` (directly or transitively).
40    pub param_freed: BTreeMap<usize, bool>,
41    /// Whether the callee dereferences `param[i]`.
42    pub param_dereferenced: BTreeMap<usize, bool>,
43    /// Whether the function returns newly allocated memory.
44    pub return_is_allocated: bool,
45}
46
47impl DerivedSpec {
48    /// Create an empty derived spec with no discovered properties.
49    #[must_use]
50    pub fn empty() -> Self {
51        Self {
52            computed_return_bound: None,
53            param_freed: BTreeMap::new(),
54            param_dereferenced: BTreeMap::new(),
55            return_is_allocated: false,
56        }
57    }
58
59    /// Create from a `ParameterEffectSummary`-style tuple.
60    #[must_use]
61    pub fn from_effects(
62        param_freed: BTreeMap<usize, bool>,
63        param_dereferenced: BTreeMap<usize, bool>,
64        return_is_allocated: bool,
65    ) -> Self {
66        Self {
67            computed_return_bound: None,
68            param_freed,
69            param_dereferenced,
70            return_is_allocated,
71        }
72    }
73}
saf_core/spec/derived.rs

saf_core/spec/
derived.rs
