\section{Activation Traces and the Coverage Contract}
\label{sec:traces}

An abstract state at node $v$ in context $c$ needs a concrete interpretation.
We adapt local traces~\cite{schwarz21} to retain activations and callers, then
relate them to contexts, including call histories~\cite{sharir81}. The
coverage contract is independent of abstract domains, equations, and solvers.

A graph execution with a
plain frame stack does not record contexts. A frame holds only what is
needed to resume the caller and disappears at the return. Frames could carry a
ghost context, an annotation used only in the proof
(\cref{sec:mechanization}). We keep contexts out of the base trace semantics
and relate them to traces separately. Each call starts a new activation linked
to its caller; a return combines the completed callee trace with the caller
trace and resumes the caller.

\subsection{Activation traces}

An \emph{activation path} is the list of node--store pairs visited by one
activation. The constructors of an activation trace describe how an activation begins
or continues (\isaname{activation_trace}). $\ctor{Root}~\pi$ records
the activation of \texttt{main}. $\ctor{Call}~t'~\pi$ records a callee
activation and retains the caller trace $t'$ at the call site.
$\ctor{Resume}~t'~t''~\pi$ records the caller's continuation after the callee
trace $t''$ has completed. The observers $\mathit{path\_of}\;t$,
$\mathit{sink\_node}\;t$, and $\mathit{sink\_store}\;t$ return the path, its last
node, and its last store, respectively. The observer $\mathit{caller\_of}\;t$
returns the creating caller trace wrapped in $\mathit{Some}$, or
$\mathit{None}$ for the main activation. The operation
$\mathit{extend}\;t\;(v, s)$ appends a step to the path.

The datatype admits terms that no execution produces. Let $\mathit{entry}_g$ be the entry node of \texttt{main}. The set
$\Traces_{\Glob,g,S}$ of \emph{valid} traces of graph $g$ from initial stores
$S$ is defined by four rules mirroring graph execution
(\isaname{valid_activation_trace}). We omit the fixed subscripts below;
$@$ concatenates lists and $\#$ prepends an element. A rule derives the
conclusion below its line from the premises above it:
\begin{gather*}
\frac{s \in S}{\ctor{Root}\,[(\mathit{entry}_g, s)] \in \Traces}
\\[1ex]
\frac{t \in \Traces \quad (\mathit{sink\_node}\;t, a, v) \in \mathit{intra}\;g \quad s' \in \mathit{step}_a(\mathit{sink\_store}\;t)}{\mathit{extend}\;t\;(v, s') \in \Traces}
\\[1ex]
\frac{t \in \Traces \quad (\mathit{sink\_node}\;t, e, \ctor{FunctionEntry}\;p, k) \in \mathit{calls}\;g}{\ctor{Call}\;t\;[(\ctor{FunctionEntry}\;p,\; \mathit{enter}_e(\mathit{sink\_store}\;t))] \in \Traces}
\\[1ex]
\frac{\begin{array}{c}t'' \in \Traces \quad \mathit{caller\_of}\;t'' = \mathit{Some}\;t' \quad \mathit{sink\_node}\;t'' = \ctor{FunctionResult}\;p\\ (\mathit{sink\_node}\;t', e, \ctor{FunctionEntry}\;p, k) \in \mathit{calls}\;g\end{array}}{\ctor{Resume}\;t'\;t''\;\bigl(\mathit{path\_of}\;t' \mathbin{@} [(k, \mathit{combine}_e(\mathit{sink\_store}\;t', \mathit{sink\_store}\;t''))]\bigr) \in \Traces}
\end{gather*}
Here $\mathit{step}_a$ is the concrete meaning of an action, $\mathit{enter}_e$
binds the callee's formals to the call's arguments and resets its locals, and
$\mathit{combine}_e$ keeps the caller's locals, takes the callee's globals, and
assigns the return value to the call's destination (\isaname{combine_collect}).
A return resumes the activation identified by $\mathit{caller\_of}$.
The traces are defined for arbitrary graphs, so the return rule takes \emph{some} call edge from the caller's call site into $p$. It does
not require the edge through which the callee was entered. On compiled graphs
every call site has exactly one call edge (\isaname{calls_source_unique}), so
the two coincide.

Every finite source execution of a well-formed program yields a valid trace
that ends at the corresponding node with the same store, and whose chain of
callers represents the runtime frame stack
(\isaname{source_run_has_activation_trace}). The final stores of valid traces,
collected per node, form the node collecting semantics
$\NodeColl_{\Glob,g,S}(v)$ (\isaname{node_collect}).

The constructors follow patterns from the local traces of Schwarz et
al.~\cite{schwarz21}: initial traces, thread creation, and binary lock
acquisition incorporating a second trace. Voblint adapts these patterns to
procedure entry and return (\cref{sec:related}).

\subsection{Calling contexts as a relation}

Call-string contexts record the last $k$ call sites; entry-state contexts
record the abstract values of the formals at entry. A \emph{context policy}
specifies which callee contexts a concrete call may belong to. It maps a call
site $u$, a caller context $c$, a description of the call, the caller's store,
and the entered store to the
\emph{set} of admitted callee contexts (\isaname{context_policy}). The result
is a set because Goblint's enter may return several
alternatives for one call, each routed separately. The set may be empty, for instance at a
call the analysis considers unreachable. The supplied analyses return a single
entry alternative, so a call is admitted in at most one context per caller
context. A Sign-analysis instance demonstrates the relational case: its enter
returns two overlapping alternatives, the plain entry state and one that
forgets the formals. One concrete call is then admitted in two contexts
(\isaname{ov_two_contexts_admitted}).

For a call edge $e$ into $p$, we write $\adm_{u,c}(e, s, s')$ for the set the
policy returns for the call described by $e$ and $p$, caller store $s$ and
entered store $s'$. We write $c' \in \adm^{\exists}_{u,c}(p, s, s')$ when some call edge from $u$
into $p$ maps $s$ to the entered store $s'$ and the policy admits $c'$ for it
(\isaname{admits_call_context}). For a fixed initial context $c_0$, the contexts a trace carries are defined
inductively (\isaname{activation_context_rel}):
\begin{gather*}
\frac{}{\ctor{Root}\;\pi \text{ carries } c_0}
\qquad
\frac{t' \text{ carries } c}{\ctor{Resume}\;t'\;t''\;\pi \text{ carries } c}
\\[1ex]
\frac{t \text{ carries } c \quad c' \in \adm^{\exists}_{\mathit{sink\_node}\,t,\,c}(p, \mathit{sink\_store}\;t, s')}{\ctor{Call}\;t\;((\ctor{FunctionEntry}\;p, s') \mathbin{\#} \pi) \text{ carries } c'}
\end{gather*}
That is, the root carries the initial context $c_0$, a callee carries every
context admitted for its call from some context of its caller, and a resumed activation keeps the contexts it had
before the call. Traces store no context, so the policy is a parameter of
every theorem below. The activation collecting semantics collects the final
stores of the valid traces that end at $v$ and carry $c$
(\isaname{activation_collect}):
\[
\ActColl_{\Glob,\adm,c_0,g,S}(v, c) \;=\; \{\, \mathit{sink\_store}\;t \mid t \in \Traces_{\Glob,g,S},\; \mathit{sink\_node}\;t = v,\; t \text{ carries } c \,\}.
\]
In the running example, the final store of \texttt{bump(5)} lies in
$\ActColl(\ctor{FunctionResult}\;\texttt{bump}, [5,5])$ and that of
\texttt{bump(4)} in $\ActColl(\ctor{FunctionResult}\;\texttt{bump}, [4,4])$,
whereas $\NodeColl$ at that node contains both.

\subsection{The coverage contract}

A \emph{cover} assigns a set of stores to each node and context. The four
rules for valid traces give rise to four preservation obligations on a cover.
A fifth obligation ensures that each call from a covered store is admitted in
at least one context. We express this contract in the locale
\isaname{activation_coverage}; an Isabelle locale packages named parameters and
assumptions~\cite{ballarin14}. Write $\cover(v,c)$ for the assigned set. The obligations are as follows, with the call obligations
quantified over every call edge $(u, e, \ctor{FunctionEntry}\;p, k)$:
\begin{align*}
  &\oblig{Init} && s \in S \implies s \in \cover(\mathit{entry}_g, c_0)\\
  &\oblig{Intra} && (u, a, v) \in \mathit{intra}\;g,\; s \in \cover(u, c),\; s' \in \mathit{step}_a(s) \implies s' \in \cover(v, c)\\
  &\oblig{Call} && s \in \cover(u, c),\; c' \in \adm_{u,c}(e, s, \mathit{enter}_e(s))\\
  &&&\quad \implies \mathit{enter}_e(s) \in \cover(\ctor{FunctionEntry}\;p, c')\\
  &\oblig{Return} && s \in \cover(u, c),\; c' \in \adm^{\exists}_{u,c}(p', s, s'),\\
  &&&\quad t \in \cover(\ctor{FunctionResult}\;p, c') \implies \mathit{combine}_e(s, t) \in \cover(k, c)\\
  &\oblig{Total} && s \in \cover(u, c) \implies \adm_{u,c}(e, s, \mathit{enter}_e(s)) \neq \emptyset
\end{align*}
\oblig{Return} ranges over every procedure $p'$ and entered store $s'$
admitted at the call site. As in the return rule, the call edge $e$ used to
resume the caller can differ from the edge used to enter the callee. On a
graph with one call edge per call site, $p' = p$ and both operations use the
same edge.

If no context admits a call from a covered store, \oblig{Call} and
\oblig{Return} hold vacuously. They therefore do not ensure that the cover at
the continuation includes the returned store, even though the resumed caller
still carries its contexts there. Without \oblig{Total}, a cover that meets the
other four obligations can miss a reached store
(\isaname{total_dropped_unsound}). \oblig{Total} asks only about covered
stores, because an entry-state policy admits no context for stores the
analysis has excluded. Call strings and the unit policy, which admits one
context for every activation, meet it for every cover
(\isaname{call_context_total_on_of_fun}).

\begin{theorem}[Context-indexed soundness, \isaname{activation_collect_sound}]
\label{thm:contract}
If a cover meets the five obligations of \isaname{activation_coverage}, then
$\ActColl(v, c) \subseteq \cover(v, c)$ for every node $v$ and context $c$.
\end{theorem}

\subparagraph*{Proof idea.}
The proof inducts over valid traces. The invariant states that a trace
carries some context and its final store is covered in every context it carries. A single-trace invariant does not suffice for the return rule, which
needs the invariant for the caller recovered through $\mathit{caller\_of}$.
The induction therefore carries the invariant along the whole chain of
callers (\isaname{caller_chain_covered}, an instance of the induction
principle \isaname{caller_chain_closure}).

\oblig{Total} is used twice. In the call case, it supplies a context for the
new callee. In the return case, it supplies an admitted callee context $c'$
for each context $c$ of the resumed caller, using the callee's own entry edge.
The callee then carries $c'$ (\isaname{activation_context_rel_caller_entryI}),
so its exit store is covered at $c'$. \oblig{Return} ensures that combining
the caller store and callee exit store yields a store in the cover at the
continuation in context $c$. This is why \oblig{Return} ranges over the admitted
entry ($p'$, $s'$), which can differ from the entry specified by the call edge used for resumption.

Under the contract, every valid trace therefore carries at least one context,
so taking the union over contexts recovers the node collecting semantics
(\isaname{node_collect_eq_Union_activation_collect}):
\[
\NodeColl(v) \;=\; \textstyle\bigcup_c \ActColl(v, c).
\]