# Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness
with Computational Effects

Noam Zilberstein<EMAIL_ADDRESS>0000-0001-6388-063X Cornell
UniversityUSA ,  Angelina Saliling<EMAIL_ADDRESS>0009-0000-6277-435X
Cornell UniversityUSA and  Alexandra Silva<EMAIL_ADDRESS>0000-0001-5014-9784 Cornell UniversityUSA

(2024; 2023-10-12; 2024-02-24)

###### Abstract.

Separation logic’s compositionality and local reasoning properties have led to
significant advances in scalable static analysis. But program analysis has new
challenges—many programs display _computational effects_ and, orthogonally,
static analyzers must handle _incorrectness_ too. We present Outcome
Separation Logic (OSL), a program logic that is sound for both correctness and
incorrectness reasoning in programs with varying effects. OSL has a frame
rule—just like separation logic—but uses different underlying assumptions that
open up local reasoning to a larger class of properties than can be handled by
any single existing logic.

Building on this foundational theory, we also define symbolic execution
algorithms that use bi-abduction to derive specifications for programs with
effects. This involves a new _tri-abduction_ procedure to analyze programs
whose execution branches due to effects such as nondeterministic or
probabilistic choice. This work furthers the compositionality promised by
separation logic by opening up the possibility for greater reuse of analysis
tools across two dimensions: bug-finding vs verification in programs with
varying effects.

Outcome Logic, Separation Logic, Incorrectness

††copyright: rightsretained††doi: 10.1145/3649821††journalyear:
2024††submissionid: oopslaa24main-p29-p††journal: PACMPL††journalvolume:
8††journalnumber: OOPSLA1††article: 104††publicationmonth: 4††ccs: Theory of
computation Separation logic††ccs: Theory of computation Hoare logic††ccs:
Theory of computation Logic and verification††ccs: Software and its
engineering Software verification

##  1\. Introduction

Compositional reasoning using separation logic (Reynolds, 2002) and bi-
abduction (Calcagno et al., 2009) has helped scale static analysis to
industrial software with hundreds of millions of lines of code, making it
possible to analyze code changes without disrupting the fast-paced engineering
culture that developers are accustomed to (Calcagno et al., 2015; Distefano et
al., 2019).

While the ideal of fully automated program verification remains elusive,
analysis tools can boost confidence in code correctness by ensuring that a
program will not _go wrong_ in a variety of ways. In languages like C or C++,
this includes ensuring that a program will not crash due to a segmentation
fault or leak memory. However, a static analyzer _failing_ to prove the
absence of bugs does not imply that the program is incorrect; it could be a
false positive.

Many programs are, in fact, incorrect. Analysis tools capable of finding bugs
are thus in some cases _more useful_ than verification tools, since the
reported errors lead directly to tangible code improvements (Le et al., 2022).
Motivated by the need to identify bugs, Incorrectness Logic (O’Hearn, 2020)
and Incorrectness Separation Logic (ISL) (Raad et al., 2020; Raad et al.,
2022) were recently introduced.

While ISL enjoys compositionality just like separation logic, the semantics of
SL and ISL are incompatible—specifications and analysis tools cannot readily
be shared between them. Further, the soundness of local reasoning in each
separation logic variant relies on particular assumptions, meaning that no
single program logic has a frame rule that can handle all of the following:

Computational Effects. The idea that program commands must be _local actions_
(Calcagno et al., 2007) is central to the frame rule. In order to achieve
locality, the semantics of memory allocation is often forced to be
nondeterministic (Yang and O’Hearn, 2002), but this approach is not suitable
for local reasoning in alternative execution models such as probabilistic
computation.

May and Must properties. Separation logic can only express properties that
_must_ occur, whereas ISL can only express properties that _may_ occur. A
logic for both correctness and incorrectness properties must handle both _may_
and _must_ properties.

Under-approximation. Bug-finding static analyses operate more efficiently by
only inspecting a subset of the program paths—the ones that lead to a bug. But
many separation logics are _fault avoiding_ ; the precondition must specify
the resources needed to execute all traces, and therefore the entire program
must be inspected. Fault avoidance is unsuitable in logics for incorrectness.

In this paper, we show that local reasoning is sound under new assumptions,
which do not force any particular evaluation model and are therefore
compatible with both correctness and incorrectness reasoning. To that end, we
introduce _Outcome Separation Logic_ (OSL), a single program logic that can
handle all of the aforementioned scenarios. Our contributions are as follows.

Outcome Separation Logic. Our main contribution is Outcome Separation Logic
(OSL), an extension of the recently introduced Outcome Logic (OL) (Zilberstein
et al., 2023) for reasoning about pointer programs. While OL already supports
correctness and incorrectness reasoning in programs with a variety of effects
and much of the metatheory and inference rules carry over from it, the key
novelty of OSL is that it is fundamentally based on separation-logic-style
heap assertions, which allowed us to develop a frame rule for local reasoning
and compositional symbolic execution.

This was no simple feat; while the soundness of the frame rule is intricate
and nuanced even in partial correctness Hoare Logic (Yang and O’Hearn, 2002),
moving to a logic that supports a variety of assertions about termination,
reachability, and probabilistic reasoning complicates the story significantly.
OSL is the first program logic that supports local reasoning for both
correctness and incorrectness, with the ability to also under-approximate
program paths. On top of that, using an algebraic representation of choice,
the soundness proof of our frame rule extends to other execution models too,
such as probabilistic programs.

Symbolic execution algorithms. As a proof of concept for how OSL enables the
consolidation of correctness and incorrectness analysis, we present symbolic
execution algorithms to analyze C-like pointer programs. The core algorithm
finds all the reachable outcomes, and is therefore tailored for correctness
reasoning. We also define a _single-path_ variant—modeled after Incorrectness
Logic based bug-finding algorithms (Pulse (Raad et al., 2020) and Pulse-X (Le
et al., 2022))—inferring specifications in which the postcondition is just one
of the (possibly many) outcomes. While enjoying the scalability benefit of
dropping paths, our algorithm can also soundly re-use procedure summaries
generated by the correctness algorithm so as to not re-analyze the same
procedure.

These algorithms are based on bi-abduction, which handles _sequential_
programs by reconciling the postcondition of one precomputed spec with the
precondition of the next (Calcagno et al., 2009, 2011). Since programs with
effects are not purely sequential, but rather have branching that arises from,
_e.g.,_ nondeterministic or probabilistic choice, we also introduce _tri-
abduction_ , a new form of inference for composing branches in an effectful
program.

We begin in Section 2 by outlining the challenges of local reasoning in a
highly expressive program logic. Next, in Sections 3 and 4, we define Outcome
Separation Logic (OSL), show three instantiations, and prove the soundness of
the frame rule. In Section 5, we define our symbolic execution algorithm and
tri-abduction, which is inspired by bi-abduction but is used for branching
rather than sequential composition. In Section 6, we examine two case studies
to show the applicability of these algorithms and finally we conclude in
Sections 7 and 8 by discussing outlooks and related work.

##  2\. Local Reasoning for Correctness and Incorrectness with Effects

We begin by examining how the local reasoning principles of separation logic,
along with bi-abductive inference, underlie scalable analysis techniques.
These analyses symbolically execute programs and report the result as Hoare
Triples
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{P\\}}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{Q\\}}$:
the postcondition $Q$ describes any result of running $C$ in a state
satisfying the precondition $P$ (Hoare, 1969). Hoare triples are
compositional; a specification for the sequence of two commands is constructed
from specifications for each one.

$\inferrule{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{P\\}}~{}C_{1}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{Q\\}}\\\
{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{Q\\}}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{R\\}}}{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{P\\}}~{}C_{1}\fatsemi
C_{2}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{R\\}}}{\textsc{Sequence}}$

The Sequence rule is a good starting point for building scalable program
analyses, but it is not quite compositional enough. The postcondition of
$C_{1}$ must exactly match the precondition of $C_{2}$, making it difficult to
apply this rule, particularly if $C_{1}$ and $C_{2}$ are procedure calls for
which we already have pre-computed summaries (in the form of Hoare Triples),
none of which exactly match. In response, separation logic offers a second
form of (spatial) compositionality via the Frame rule, which adds information
about unused program resources $F$ to the pre- and postcondition of a
completed proof.

$\inferrule{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{P\\}}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{Q\\}}}{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{P*F\\}}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{Q*F\\}}}{\textsc{Frame}}$

But framing does not immediately answer how to sequentially compose triples.
Given
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{P_{1}\\}}~{}C_{1}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{Q_{1}\\}}$
and
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{P_{2}\\}}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{Q_{2}\\}}$,
it is unclear what— _if anything_ —can be added to make $Q_{1}$ match $P_{2}$.
This is where bi-abduction comes in—a technique that finds a missing resource
$M$ and leftover frame $F$ to make the entailment $Q_{1}\ast M\vDash P_{2}\ast
F$ hold. The question of deciding these entailments for separation logic
assertions is well-studied (Berdine et al., 2005a), and yields a more usable
sequence rule that stitches together two precomputed summaries without
reexamining either program fragment.

$\inferrule{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{P_{1}\\}}~{}C_{1}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{Q_{1}\\}}\\\
Q_{1}*M\vDash P_{2}*F\\\
{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{P_{2}\\}}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{Q_{2}\\}}}{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{P_{1}*M\\}}~{}C_{1}\fatsemi
C_{2}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{Q_{2}*F\\}}}{\textsc{Bi-
Abductive Sequence}}$

While bi-abduction has helped industrial strength static analyzers scale to
massive codebases, current developments use disjoint algorithms for
correctness vs incorrectness, and do not support computational effects such as
probabilistic choice. In the remainder of this section, we will examine why
this is the case and explain how our logic allows for unified bi-abductive
analysis algorithms.

###  2.1. Interlude: Reasoning about Effects and Incorrectness

While identifying bugs in pure programs is already challenging, effects add
more complexity. This is demonstrated below; the program crashes because it
attempts to dereference a null pointer.

${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{\mathsf{ok}:x=\mathsf{null}\\}}~{}[x]\leftarrow
1~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{\mathsf{er}:x=\mathsf{null}\\}}$

The specification is semantically straightforward; if $x$ is null then the
program will crash.111 Caveat: nontermination is an effect, and the typical
_partial correctness_ interpretation of SL is not suitable for incorrectness.
Now, rather than dereferencing a pointer that is _known_ to be invalid,
suppose we dereference a pointer that _might_ be invalid,
and—crucially—whether or not it is allocated comes down to nondeterminism. The
following is one such scenario; $x$ is obtained using malloc, which either
returns a valid pointer or null. In Hoare Logic, the best we can do is specify
this program using a disjunction.

${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{\mathsf{ok}:\mathsf{emp}\\}}~{}x\coloneqq\mathsf{malloc}()\fatsemi[x]\leftarrow
1~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{(\mathsf{ok}:x\mapsto
1)\vee(\mathsf{er}:x=\mathsf{null})\\}}$

While the above specification hints that the program has a bug, it is in fact
inconclusive since the disjunctive postcondition does not guarantee that both
outcomes are _reachable_ by actual program executions. Hoare Logic is
fundamentally unable to characterize this bug, since the postcondition must
describe _all_ possible end states of the program; we cannot express something
that _may_ occur.

Two solutions for characterizing true bugs have been proposed. The first one
is Incorrectness Logic (IL), which uses an alternative semantics to express
that all states described by the postcondition are reachable from a state
described by the precondition (O’Hearn, 2020). Specifying the aforementioned
bug is possible using Incorrectness Logic; the following triple stipulates
that all the states described by the postcondition are reachable, including
ones where the error occurs.

${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}[\mathsf{ok}:\mathsf{emp}]}~{}x\coloneqq\mathsf{malloc}()\fatsemi[x]\leftarrow
1~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}[(\mathsf{ok}:x\mapsto
1)\vee(\mathsf{er}:x=\mathsf{null})]}$

A variant of IL has a frame rule (Raad et al., 2020) and can underlie bi-
abductive symbolic execution algorithms (Le et al., 2022). However—just like
separation logic—IL is specialized to nondeterministic programs and cannot be
used for programs with other effects such as randomization. In addition, being
inherently under-approximate, the semantics of IL cannot capture correctness
properties, which must cover all the reachable outcomes. As such, different
analyses and procedure summaries must be used for verification vs bug-finding.

In this paper, we take a different approach based on Outcome Logic (OL), which
is compatible with both correctness and incorrectness while also supporting a
variety of monadic effects (Zilberstein et al., 2023). OL is similar to Hoare
Logic, but the pre- and postconditions of triples describe _collections_ of
states rather than individual ones. A new logical connective $\oplus$—the
outcome conjunction—guarantees the reachability of multiple outcomes. For
instance, the aforementioned bug can be characterized using the following
Outcome Logic specification by using an outcome conjunction instead of a
disjunction in the postcondition.

${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:\mathsf{emp}\rangle}~{}x\coloneqq\mathsf{malloc}()\fatsemi[x]\leftarrow
1~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{ok}:x\mapsto
1)\oplus(\mathsf{er}:x=\mathsf{null})\rangle}$

The above triple says that running the program in the empty heap will result
in two reachable outcomes. In this case, the program is nondeterministic and
its semantics is accordingly characterized by a _set_ of program states $S$.
The outcome conjunction tells us that there exist nonempty sets $S_{1}$ and
$S_{2}$ with $S=S_{1}\cup S_{2}$ such that $S_{1}\vDash(\mathsf{ok}:x\mapsto
1)$ and $S_{2}\vDash(\mathsf{er}:x=\mathsf{null})$. Since both outcomes are
satisfied by nonempty sets, we know that they are both reachable by a real
program trace.

For efficiency, specifying the bug above should not require recording
information about the $\mathsf{ok}$ outcome. In incorrectness reasoning, it is
desirable to _drop outcomes_ so as to only explore some of the program paths
(O’Hearn, 2020; Le et al., 2022). We achieve this in OL by replacing the
extraneous outcome with $\top$—an assertion that is satisfied by any set of
states, including the empty set.

${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:\mathsf{emp}\rangle}~{}x\coloneqq\mathsf{malloc}()\fatsemi[x]\leftarrow
1~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{er}:x=\mathsf{null})\oplus\top\rangle}$

Since
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\top\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\top\rangle}$
is valid for any program $C$, this trick allows us to propagate the $\top$
forward through the program derivation without determining what would happen
if the memory dereference had succeeded. The following triple is valid too,
regardless of what comes next in the program.

${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:\mathsf{emp}\rangle}~{}x\coloneqq\mathsf{malloc}()\fatsemi[x]\leftarrow
1\fatsemi\cdots\fatsemi\cdots\fatsemi\cdots~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{er}:x=\mathsf{null})\oplus\top\rangle}$

Outcomes apply to more effects than just nondeterminism. For example, Outcome
Logic can also be used to reason about probabilistic programs, where the
(weighted) outcome conjunction additionally quantifies the likelihoods of
outcomes. For example, the following program attempts to ping an IP address,
which succeeds 99% of the time, and fails with probability 1% due to an
unreliable network.

${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:\mathsf{true}\rangle}~{}x\coloneqq\mathsf{ping}(192.0.2.1)~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{ok}:x=0)\oplus_{99\%}(\mathsf{er}:x=1)\rangle}$

Our goal in this paper is to extend local reasoning to Outcome Logic by
augmenting it with a frame rule, and to use the resulting theory to build bi-
abductive symbolic execution algorithms for both correctness (finding all
reachable outcomes) and incorrectness (only exploring one program path at a
time) in pointer programs with varying effects. We will next see the
challenges behind designing a frame rule powerful enough to achieve that goal.

###  2.2. Designing a More Powerful Frame Rule

In their initial development of the frame rule, Yang and O’Hearn (2002, §1)
remarked:

> “ _The first problem we tackle is the soundness of the Frame Rule. This
> turns out to be surprisingly delicate, and it is not difficult to find
> situations where the rule doesn’t work. So a careful treatment of soundness,
> appealing to the semantics of a specific language, is essential._ ”

Today, there are many frame rules that appeal to the semantics in their
respective situations, relying on properties such as nondeterminism, partial
correctness, or under-approximation for soundness. Our challenge is to design
a frame rule supporting _all_ of those features, which means that fundamental
questions must be addressed head on, without appealing to a _particular_
semantic model. We follow the basic formula of standard separation logic (Yang
and O’Hearn, 2002; Calcagno et al., 2007), as it is semantically closest to
Outcome Logic.222 We remark that other proof strategies exist including using
heap monotonicity (ISL) and frame baking (higher-order separation logics), a
comparison to these approaches is available in Section 7.

Local Actions. Framing is sound if all program actions are _local_ (Calcagno
et al., 2007). Roughly speaking, $C$ is local if its behavior does not change
as pointers are added to the heap. Most actions are inherently local, _e.g.,_
dereferencing a pointer depends only on a single heap cell.

But memory allocation is—or at least, some implementations of it
are—inherently non-local; allocating a new address involves reaching into an
unknown region of the heap. To see why this is problematic, consider a
deterministic allocator that always returns the smallest available address.
So, allocating a pointer in the empty heap is guaranteed to return the address
1. The following triple is therefore valid, stating that $x$ is the address 1,
which points to some value.

${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{\mathsf{emp}\\}}~{}x\coloneqq\mathsf{alloc}()~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{x=1\land
x\mapsto-\\}}$

However, applying the frame rule can easily invalidate this specification.

$\inferrule{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{\mathsf{emp}\\}}~{}x\coloneqq\mathsf{alloc}()~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{x=1\land
x\mapsto-\\}}}{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{y\mapsto
2\\}}~{}x\coloneqq\mathsf{alloc}()~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{x=1\land
x\mapsto-\ast y\mapsto 2\\}}}{\textsc{Frame}}$

Since $y$ can have address 1, the fresh pointer $x$ cannot also be equal to 1,
so this application of the frame rule is clearly unsound. Making memory
allocation nondeterministic can solve the problem (Yang and O’Hearn, 2002).
If, in the above program, $x$ could be assigned _any_ fresh address, then the
postcondition cannot say anything specific about _which_ address got
allocated. We cannot conclude that $x=1$, but rather only that $x=1\vee
x=2\vee\cdots$, which remains true in any larger heap.

Moving from Hoare Logic to Outcome Logic, this approach has two problems.
First, Outcome Logic is parametric on an evaluation model, so the availability
of nondeterminism is not a given; we need a strategy for allocation in the
presence of _any_ computational effects. Second, even with nondeterminism,
locality is complicated by the ability to reason about reachable states. The
problematic interaction between framing and reachability is displayed in the
following example, which explicitly states that $x=1$ is a reachable outcome
of allocating $x$ in the empty heap.

$\inferrule{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:\mathsf{emp}\rangle}~{}x\coloneqq\mathsf{alloc}()~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{ok}:x=1)\oplus(\mathsf{ok}:x\neq
1)\rangle}}{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:y\mapsto
2\rangle}~{}x\coloneqq\mathsf{alloc}()~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{ok}:x=1\land
y\mapsto 2)\oplus(\mathsf{ok}:x\neq 1\land y\mapsto
2)\rangle}}{\textsc{Frame}}$

This inference is invalid; the precondition does not preclude $y$ having
address 1, in which case $x=1$ is no longer a reachable outcome. In OSL, we
acknowledge that memory allocation is non-local and instead ensure that
triples cannot specify the result of an allocation too finely. This is
achieved by altering the semantics of a triple
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\psi\rangle}$
to require that if $\varphi$ holds in some initial state, then $\psi$ holds
after running $C$ using _any_ allocation semantics. By universally quantifying
the allocator, we ensure that any concrete semantics is captured, while
retaining soundness of the frame rule. In particular, the premise in the above
inference that $x=1$ is a reachable outcome is invalid according to our
semantics because there are many allocation semantics in which it is false.

Fault Avoidance. Typical formulations of separation logic are _fault avoiding_
, meaning that the precondition must imply that the program execution does not
encounter a memory fault (Reynolds, 2002; Yang and O’Hearn, 2002). Unlike in
Hoare Logic, the triple
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{\mathsf{true}\\}}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{\mathsf{true}\\}}$
is not necessarily valid, which is crucial to the frame rule. If the triple
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{\mathsf{true}\\}}~{}[x]\leftarrow
1~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{\mathsf{true}\\}}$
were valid, then the frame rule would give us
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{x\mapsto
2\ast\mathsf{true}\\}}~{}[x]\leftarrow
1~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{x\mapsto
2\ast\mathsf{true}\\}}$, which is clearly false.

The problem with fault avoidance is that it involves inspecting the entire
program, whereas OSL must be able to ignore some paths to more efficiently
reason about incorrectness. Fortunately, OSL preconditions need not be safe.
Following the previous example,
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:\mathsf{true}\rangle}~{}[x]\leftarrow
1~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:\mathsf{true}\rangle}$
is not a valid OSL specification since $\mathsf{ok}:\mathsf{true}$ is not a
_reachable_ outcome of running the program. Rather, if the precondition of an
OSL triple is unsafe, then the postcondition can only be $\top$, an assertion
representing any _collection_ of outcomes, including divergence. So,
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:\mathsf{true}\rangle}~{}[x]\leftarrow
1~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\top\rangle}$
is a valid triple and framing information into it is perfectly sound since the
$\top$ will absorb _any_ outcome, including undefined behavior:
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:x\mapsto
2\ast\mathsf{true}\rangle}~{}[x]\leftarrow
1~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\top\rangle}$.

OSL allows us to decide how much of the memory footprint to specify. In a
correctness analysis covering all paths, the precondition must be safe for the
entire program. If we instead want to reason about incorrectness and drop
paths, then it must only be safe for the paths we explore.

###  2.3. Symbolic Execution and Tri-Abduction

OSL provides a logical foundation for symbolic execution algorithms that are
capable of _both_ verification _and_ bug-finding. Our approach takes
inspiration from industrial strength bi-abductive analyzers (Abductor and
Infer (Calcagno et al., 2009, 2015)), but paying greater attention to effects,
as the aforementioned tools may fail to find specifications for programs with
control flow branching.

To see what goes wrong, let us examine a program that uses disjoint resources
in the two nondeterministic branches: $([x]\leftarrow 1)+([y]\leftarrow 2)$.
Using bi-abduction, we could conclude that $x\mapsto-$ is a valid precondition
for the first branch whereas $y\mapsto-$ is valid for the second, but there is
no immediate way to find a precondition valid for _both_ branches since the
branches may contain overlapping resources involving pointers and inductive
predicates about more complex data structures such as lists. As a result, the
program must be re-evaluated with each candidate precondition to ensure that
they are safe for all branches.

Calcagno et al. (2011, §4.3) acknowledged this issue, and suggested fixing it
by re-running the abduction procedure until nothing more can be added to each
precondition. Rather than using two passes (as Abductor already does), this
requires a pass for each combination of nondeterministic choices, which is
exponential in the worst case. While a single-pass bi-abduction algorithm has
been proposed (Sextl et al., 2023), it still cannot handle all cases (see
Remark 2 in Section 5.1).

We take a different approach, acknowledging that branching is fundamentally
different from sequential composition and requires a new type of inference,
which we call tri-abduction. As its name suggests, tri-abduction infers three
components (to bi-abduction’s two). Given $P_{1}$ and $P_{2}$—preconditions
for two branches—the goal is to find a single anti-frame $M$ and two leftover
frames $F_{1}$ and $F_{2}$ such that $M\vDash P_{1}\ast F_{1}$ and $M\vDash
P_{2}\ast F_{2}$, in order to compose the summaries for two program branches,
as demonstrated below.

$\inferrule{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle
P_{1}\rangle}~{}C_{1}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle
Q_{1}\rangle}\\\ P_{1}\ast
F_{1}\mathrel{\mathchoice{\reflectbox{$\displaystyle\vDash$}}{\reflectbox{$\textstyle\vDash$}}{\reflectbox{$\scriptstyle\vDash$}}{\reflectbox{$\scriptscriptstyle\vDash$}}}M\vDash
P_{2}\ast F_{2}\\\
{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle
P_{2}\rangle}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle
Q_{2}\rangle}}{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle
M\rangle}~{}C_{1}+C_{2}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(Q_{1}\ast
F_{1})\oplus(Q_{2}\ast F_{2})\rangle}}{\textsc{Tri-Abductive Composition}}$

Tri-abduction does not replace bi-abduction; they work in complementary
ways—bi-abduction is used for sequential composition whereas tri-abduction
composes branches arising from effects.

In addition, we are interested in bug-finding algorithms, which—similar to
Pulse and Pulse-X (Raad et al., 2020; Le et al., 2022)—do not traverse all the
program paths. We achieve this using a single-path version of the algorithm,
producing summaries of the form
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{er}:Q)\oplus\top\rangle}$,
with only a single outcome specified and the remaining ones covered by $\top$.
The soundness of the single-path approach is motivated by the fact that
$P\oplus Q\Rightarrow P\oplus\top$; extraneous outcomes can be converted to
$\top$, ensuring that those paths will not be explored. Just like in Pulse and
Pulse-X, this ability to _drop outcomes_ allows the analysis to retain less
information for increased scalability.

We formalize these concepts starting in Sections 3 and 4, where we define a
program semantics and Outcome Separation Logic and prove the soundness of the
frame rule. Symbolic execution and tri-abduction are defined in Section 5, and
we examine case studies in Section 6.

##  3\. Program Semantics

We begin the technical development by defining the semantics for the
underlying programming language of Outcome Separation Logic. All instances of
OSL share the same program syntax, but this syntax is interpreted in different
ways, corresponding to the choice mechanisms dictated by each instance’s
computational effects. The syntax of the language is given below.

$\displaystyle\mathsf{Cmd}\ni C\Coloneqq$ $\displaystyle~{}\mathsf{skip}\mid
C_{1}\fatsemi C_{2}\mid
C_{1}+C_{2}\mid\mathsf{assume}~{}e\mid\mathsf{while}~{}e~{}\mathsf{do}~{}C\mid
c$ $\displaystyle\mathsf{Act}\ni c\Coloneqq$ $\displaystyle~{}x\coloneqq e\mid
x\coloneqq\mathsf{alloc}()\mid\mathsf{free}(e)\mid[e_{1}]\leftarrow e_{2}\mid
x\leftarrow[e]\mid\mathsf{error}()\mid f(\vec{e})$
$\displaystyle\mathsf{Exp}\ni e\Coloneqq$ $\displaystyle~{}x\mid\kappa\mid
e_{1}\diamond e_{2}\mid\lnot
e\qquad\qquad\qquad\qquad(x\in\mathsf{Var},\kappa\in\mathsf{Val},f\in\mathsf{Proc},{\diamond}\in\mathsf{BinOp})$

Commands $C\in\mathsf{Cmd}$ are similar to those of Dijkstra’s [(1975)]
Guarded Command Language (GCL), containing $\mathsf{skip}$, sequencing
$(C_{1}\fatsemi C_{2})$, choice ($C_{1}+C_{2}$) and while loops. Given a test
$e$ (_i.e.,_ a Boolean-valued expression), conditionals are defined as
syntactic sugar in the typical way:
$\mathsf{if}~{}e~{}\mathsf{then}~{}C_{1}~{}\mathsf{else}~{}C_{2}\triangleq(\mathsf{assume}~{}e\fatsemi
C_{1})+(\mathsf{assume}~{}\lnot e\fatsemi C_{2})$. But—unlike
GCL—$\mathsf{assume}$ also accepts expressions that are interpreted over
_weights_ drawn from a set that has additional algebraic properties described
in Section 3.1 (and can also encode the Booleans). For example, weights in
randomized programs are probabilities $p\in[0,1]$, and we can accordingly
define a probabilistic choice operator
$C_{1}+_{p}C_{2}\triangleq(\mathsf{assume}~{}p\fatsemi
C_{1})+(\mathsf{assume}~{}1-p\fatsemi C_{2})$, which runs $C_{1}$ with
probability $p$ and $C_{2}$ with probability $1-p$.

Atomic actions $c\in\mathsf{Act}$ can assign to variables ($x\coloneqq e$),
allocate ($x\coloneqq\mathsf{alloc}()$) and deallocate ($\mathsf{free}(e)$)
memory, write ($[e_{1}]\leftarrow e_{2}$) and read ($x\leftarrow[e]$)
pointers, crash ($\mathsf{error}()$), and call procedures ($f(\vec{e})$).
Expressions can be variables $x\in\mathsf{Var}$, constants
$\kappa\in\mathsf{Val}$ (_e.g.,_ integers, Booleans, and _weights_), a variety
of binary operations $e_{1}\diamond e_{2}$ where
${\diamond}\in\mathsf{BinOp}=\\{+,-,=,\leq,\ldots\\}$, or logical negation
$\lnot e$.

In the remainder of this section, we will formally define denotational
semantics for the language above. This will first involve discussing the
algebraic properties of the program weights, after which we can define a
(monadic) execution model to interpret sequential composition.

###  3.1. Algebraic Preliminaries

We first recall the definitions of some algebraic structures that will be used
to instantiate the program semantics for different execution models. _Monoids_
model combining and scaling outcomes.

###### Definition 3.1 (Monoid).

A monoid $\langle A,+,\dsser{0}\rangle$ consists of a carrier set $A$, an
associative binary operator $+\colon A\times A\to A$, and an identity element
$\dsser{0}\in A$ such that $a+\dsser{0}=\dsser{0}+a=a$ for all $a\in A$.
Additionally, a monoid is _partial_ if $+$ is partial ($+\colon A\times
A\rightharpoonup A$) and it is _commutative_ if $a+b=b+a$.

For example, $\langle[0,1],+,0\rangle$ is a partial commutative monoid that is
commonly used in probabilistic computation since probabilities come from the
interval $[0,1]$ and addition is undefined if the sum is greater than 1.
Scalar multiplication $\langle[0,1],\cdot,1\rangle$ is another monoid with
with same carrier set, but it is total rather than partial. Two monoids can be
combined to form a semiring, as follows.

###### Definition 3.2 (Semiring).

A semiring $\langle A,+,\cdot,\dsser{0},\dsser{1}\rangle$ consists of a
carrier set $A$, along with an addition operator $+$, a multiplication
operator $\cdot$ and two elements $\dsser{0},\dsser{1}\in A$ such that:

  1. (1)

$\langle A,+,\dsser{0}\rangle$ is a commutative monoid.

  2. (2)

$\langle A,\cdot,\dsser{1}\rangle$ is a monoid (we sometimes omit $\cdot$ and
write $a\cdot b$ as $ab$).

  3. (3)

Multiplication distributes over addition: $a\cdot(b+c)=ab+ac$ and $(b+c)\cdot
a=ba+ca$

  4. (4)

$\dsser{0}$ is the annihilator of multiplication:
$a\cdot\dsser{0}=\dsser{0}\cdot a=\dsser{0}$

A semiring is _partial_ if $\langle A,+,\dsser{0}\rangle$ is instead a partial
commutative monoid (PCM), but multiplication remains total. In the case of a
partial semiring, distributive rules only apply if $b+c$ is defined.

We now define Outcome Algebras that give the interpretation of choice and
weighting. The carrier set $A$ is used to represent the weight of an outcome.
In deterministic and nondeterministic evaluation models, this weight can be 0
or 1 (a Boolean), but in the probabilistic model, it can be any probability in
$[0,1]$. The rules for combining these weights vary by execution model.

###### Definition 3.3 (Outcome Algebra).

An _Outcome Algebra_ is a structure $\langle
A,+,\cdot,\dsser{0},\dsser{1}\rangle$, which is a complete, Scott continuous,
naturally ordered, partial semiring, and:

  1. (1)

Ordering: $\langle A,\leq\rangle$ is a directed complete partial order (dcpo)
and $\sup(A)=\dsser{1}$.

  2. (2)

Normalization: If $\sum_{i\in I}a_{i}$ is defined, then there exist
$(b_{i})_{i\in I}$ such that $\sum_{i\in I}b_{i}=\dsser{1}$ and $\forall i\in
I.a_{i}=(\sum_{j\in I}a_{j})\cdot b_{i}$.

Appendix A defines Scott continuity and completeness. Property (2) guarantees
that any weighting function can be normalized to have a cumulative weight of
$\dsser{1}$ without affecting the relative weights of any of the elements.
This will be necessary later on in order to prove that weights can be
tabulated to witness the relationship between two weighted collections. More
details are available in Appendix A.

Outcome Algebras can encode the following three interpretations of choice:

###### Definition 3.4 (Deterministic Outcome Algebra).

A deterministic program has _at most_ one outcome (zero if it diverges). To
encode this, we use an Outcome Algebra $\langle\\{0,1\\},+,\cdot,0,1\rangle$
where the elements $\\{0,1\\}$ are Booleans indicating whether or not an
outcome has occurred. The sum operation is usual integer addition, but is
undefined for $1+1$, since two outcomes cannot simultaneously occur in a
deterministic setting, and $\cdot$ is typical integer multiplication.

###### Definition 3.5 (Nondeterministic Outcome Algebra).

The Boolean semiring $\langle\\{0,1\\},\lor,\land,0,1\rangle$ represents
nondeterminism. Similar to Definition 3.4, the elements indicate whether an
outcome has occurred, but now addition is logical disjunction so that multiple
outcomes can occur.

###### Definition 3.6 (Probabilistic Outcome Algebra).

Let $\langle[0,1],+,\cdot,0,1\rangle$ be an outcome algebra where $+$ is real-
valued addition (and undefined if $a+b>1$) and $\cdot$ is real-valued
multiplication. The carrier set $[0,1]$ indicates that each outcome has a
probability of occurring.

Now, using these different kinds of weights, we will interpret the result of
running programs as weighted collections of end states. More precisely, it
will be a map $\Sigma\to A$ from states $\sigma\in\Sigma$ to weights $a\in A$.
In the style of Moggi (1991), the language semantics is monadic in order to
sequence effects. We now show how to construct a monad given any Outcome
Algebra.

###### Definition 3.7 (Outcome Monad).

Given an Outcome Algebra $\mathcal{A}=\langle
A,+,\cdot,\dsser{0},\dsser{1}\rangle$ (Definition 3.3), let
$\mathcal{W}_{\mathcal{A}}(S)=\\{m:S\to
A\mid\sum_{s\in\mathsf{supp}(m)}m(s)~{}\text{is defined}\\}$ be the set of
countably supported _weighting functions_ on $\mathcal{A}$. We define a monad
$\langle\mathcal{W}_{\mathcal{A}},\mathsf{unit},\mathsf{bind}\rangle$, where
the monad operations $\mathsf{unit}\colon X\to\mathcal{W}_{\mathcal{A}}(X)$
and
$\mathsf{bind}\colon\mathcal{W}_{\mathcal{A}}(X)\times(X\to\mathcal{W}_{\mathcal{A}}(Y))\to\mathcal{W}_{\mathcal{A}}(Y)$
are defined as follows:

$\mathsf{unit}(s)(t)=\left\\{\begin{array}[]{ll}\dsser{1}&\text{if}~{}s=t\\\
\dsser{0}&\text{if}~{}s\neq
t\end{array}\right.\qquad\qquad\mathsf{bind}(m,f)(t)=\smashoperator[]{\sum_{s\in\mathsf{supp}(m)}^{}}m(s)\cdot
f(s)(t)$

We also let $\mathsf{supp}(m)=\\{s\mid m(s)\neq\dsser{0}\\}$ and
$|m|=\sum_{s\in\mathsf{supp}(m)}m(s)$. This monad is similar to the Giry
(1982) monad, which sequences computations on probability distributions. In
our case, it is generalized to work over any partial semiring, rather than
probabilities $[0,1]\subseteq\mathbb{R}$. It is fairly easy to see that
$\mathcal{W}_{\mathcal{A}}$ obeys the monad laws, given the semiring laws.

So, a weighting function $m\in\mathcal{W}_{\mathcal{A}}(S)$ assigns a weight
$a\in A$ to each program state $s\in S$. Definitions 3.4, 3.5 and 3.6 gave
interpretations for $\mathcal{A}$ in which $\mathcal{W}_{\mathcal{A}}(S)$
encodes deterministic, nondeterministic, and probabilistic computation,
respectively. In the (non)deterministic cases, $m(s)\in\\{0,1\\}$, indicating
whether or not $s$ is present in the collection of outcomes $m$. Due to the
interpretation of $+$ in Definition 3.4, the constraint that
$\sum_{s\in\mathsf{supp}(m)}m(s)$ is defined guarantees that $m$ can contain
at most one outcome, whereas in the nondeterministic case, $m$ can contain
arbitrarily many. In the probabilistic case, $m(s)\in[0,1]$ and gives the
probability of the outcome $s$ in the distribution $m$.

The semiring operations can be lifted to weighting functions. We will overload
some notation to also refer to pointwise liftings as follows:
$m_{1}+m_{2}=\lambda s.(m_{1}(s)+m_{2}(s))$, $\dsser{0}=\lambda s.\dsser{0}$,
and $a\cdot m=\lambda s.(a\cdot m(s))$. When the nondeterministic algebra
(Definition 3.5) is lifted in this way, the result is isomorphic to the
powerset monad with $m_{1}+m_{2}\cong m_{1}\cup m_{2}$ and
$\dsser{0}\cong\emptyset$.

Now, in order to represent errors and undefined states in the language
semantics, we will define a monad transformer (Liang et al., 1995) based on
the coproduct $S+E+1$ where $S$ is the set of program states, $E$ is the set
of errors, and we additionally include an undefined symbol. We define the
following three injection functions, plus shorthand for the undefined element
(where $1=\\{\star\\}$):

$\dsser{i}_{\mathsf{ok}}\colon S\to S+E+1\qquad\dsser{i}_{\mathsf{er}}\colon
E\to S+E+1\qquad\dsser{i}_{\mathsf{undef}}\colon 1\to
S+E+1\qquad\mathsf{undef}=\dsser{i}_{\mathsf{undef}}(\star)$

Borrowing the notation of Incorrectness Logic (O’Hearn, 2020), we use
$\mathsf{ok}$ and $\mathsf{er}$ to denote states in which the program
terminated successfully or crashed, respectively. We will also write
$\dsser{i}_{\epsilon}$ to refer to one of the above injections, where
$\epsilon\in\\{\mathsf{ok},\mathsf{er}\\}$.

###### Definition 3.8 (Error Monad Transformer).

Let
$\langle\mathcal{W}_{\mathcal{A}},\mathsf{bind}_{\mathcal{W}},\mathsf{unit}_{\mathcal{W}}\rangle$
be the monad described in Definition 3.7 and $E$ be a set of error states. We
define a new monad
$\langle\mathcal{W}_{\mathcal{A}}(-+E+1),\mathsf{bind},\mathsf{unit}\rangle$
where the monad operations are defined as follows:

$\mathsf{unit}(s)=\mathsf{unit}_{\mathcal{W}}(\dsser{i}_{\mathsf{ok}}(s))\qquad\mathsf{bind}(m,f)=\mathsf{bind}_{\mathcal{W}}\left(m,\lambda\sigma.\left\\{\begin{array}[]{ll}f(s)&\text{if}~{}\sigma=\dsser{i}_{\mathsf{ok}}(s)\\\
\mathsf{unit}_{\mathcal{W}}(\sigma)&\text{otherwise}\end{array}\right.\right)$

###  3.2. Denotational Semantics

Commands
$\left\llbracket-\right\rrbracket_{\mathsf{alloc}}\colon\mathsf{Cmd}\to\mathcal{S}\times\mathcal{H}\to\mathcal{W}_{\mathcal{A}}(\mathsf{St})$

$\displaystyle\left\llbracket\mathsf{skip}\right\rrbracket_{\mathsf{alloc}}(s,h)$
$\displaystyle=\mathsf{unit}(s,h)$ $\displaystyle\left\llbracket C_{1}\fatsemi
C_{2}\right\rrbracket_{\mathsf{alloc}}(s,h)$
$\displaystyle=\mathsf{bind}(\left\llbracket
C_{1}\right\rrbracket_{\mathsf{alloc}}(s,h),\left\llbracket
C_{2}\right\rrbracket_{\mathsf{alloc}})$ $\displaystyle\left\llbracket
C_{1}+C_{2}\right\rrbracket_{\mathsf{alloc}}(s,h)$
$\displaystyle=\left\llbracket
C_{1}\right\rrbracket_{\mathsf{alloc}}(s,h)+\left\llbracket
C_{2}\right\rrbracket_{\mathsf{alloc}}(s,h)$
$\displaystyle\left\llbracket\mathsf{assume}~{}e\right\rrbracket_{\mathsf{alloc}}(s,h)$
$\displaystyle=\left\llbracket
e\right\rrbracket(s)\cdot\mathsf{unit}(s,h)\quad\text{if}~{}\left\llbracket
e\right\rrbracket(s)\in A$
$\displaystyle\left\llbracket\mathsf{while}~{}e~{}\mathsf{do}~{}C\right\rrbracket_{\mathsf{alloc}}(s,h)$
$\displaystyle=\mathsf{lfp}(F_{\langle C,e,\mathsf{alloc}\rangle})(s,h)$
$\displaystyle\text{where}~{}F_{\langle C,e,\mathsf{alloc}\rangle}(f)(s,h)$
$\displaystyle=\left\\{\begin{array}[]{ll}\mathsf{bind}(\left\llbracket
C\right\rrbracket_{\mathsf{alloc}}(s,h),f)&\text{if}~{}\left\llbracket
e\right\rrbracket(s)=\dsser{1}\\\
\mathsf{unit}(s,h)&\text{if}~{}\left\llbracket
e\right\rrbracket(s)=\dsser{0}\end{array}\right.$

Actions
$\left\llbracket-\right\rrbracket_{\mathsf{alloc}}\colon\mathsf{Act}\to\mathcal{S}\times\mathcal{H}\to\mathcal{W}_{\mathcal{A}}(\mathsf{St})$

$\displaystyle\left\llbracket x\coloneqq
e\right\rrbracket_{\mathsf{alloc}}(s,h)$
$\displaystyle=\mathsf{unit}(s[x\mapsto\left\llbracket
e\right\rrbracket(s)],h)$ $\displaystyle\left\llbracket
x\coloneqq\mathsf{alloc}()\right\rrbracket_{\mathsf{alloc}}(s,h)$
$\displaystyle=\mathsf{bind}_{\mathcal{W}}(\mathsf{alloc}(s,h),\lambda(\ell,v).\mathsf{unit}(s[x\mapsto\ell],h[\ell\mapsto
v]))$
$\displaystyle\left\llbracket\mathsf{free}(e)\right\rrbracket_{\mathsf{alloc}}(s,h)$
$\displaystyle=\mathsf{update}(s,h,\left\llbracket
e\right\rrbracket(s),s,h[\left\llbracket e\right\rrbracket(s)\mapsto\bot])$
$\displaystyle\left\llbracket[e_{1}]\leftarrow
e_{2}\right\rrbracket_{\mathsf{alloc}}(s,h)$
$\displaystyle=\mathsf{update}(s,h,\left\llbracket
e_{1}\right\rrbracket(s),s,h[\left\llbracket
e_{1}\right\rrbracket(s)\mapsto\left\llbracket e_{2}\right\rrbracket(s)])$
$\displaystyle\left\llbracket
x\leftarrow[e]\right\rrbracket_{\mathsf{alloc}}(s,h)$
$\displaystyle=\mathsf{update}(s,h,\left\llbracket
e\right\rrbracket(s),s[x\mapsto h(\left\llbracket e\right\rrbracket(s))],h)$
$\displaystyle\left\llbracket\mathsf{error}()\right\rrbracket_{\mathsf{alloc}}(s,h)$
$\displaystyle=\mathsf{error}(s,h)$ $\displaystyle\left\llbracket
f(\vec{e})\right\rrbracket_{\mathsf{alloc}}(s,h)$
$\displaystyle=\left\llbracket
C\right\rrbracket_{\mathsf{alloc}}(s[\vec{x}\mapsto\left\llbracket\vec{e}\right\rrbracket(s)],h)\quad\text{where}~{}(C,\vec{x})=\mathsf{P}(f)$

Basic Operations

$\mathsf{error}(s,h)=\mathsf{unit}_{\mathcal{W}}(\dsser{i}_{\mathsf{er}}(s,h))\quad\mathsf{update}(s,h,\ell,s^{\prime},h^{\prime})=\left\\{\begin{array}[]{ll}\mathsf{unit}(s^{\prime},h^{\prime})&\text{if}~{}h(\ell)\in\mathsf{Val}\\\
\mathsf{error}(s,h)&\text{if}~{}h(\ell)=\bot\vee\ell=\mathsf{null}\\\
\mathsf{unit}_{\mathcal{W}}(\mathsf{undef})&\text{if}~{}\ell\notin\mathsf{dom}(h)\end{array}\right.$

Figure 1. Denotational semantics of program commands, parametric on an outcome
algebra $\mathcal{A}=\langle A,+,\cdot,\dsser{0},\dsser{1}\rangle$, an
allocator function
$\mathsf{alloc}:\mathcal{S}\times\mathcal{H}\to\mathcal{W}_{\mathcal{A}}(\mathsf{Addr})$,
and a procedure table
$\mathsf{P}\colon\mathsf{Proc}\to\mathsf{Cmd}\times\vec{\mathsf{Var}}$.

The semantics of commands
$\left\llbracket-\right\rrbracket_{\mathsf{alloc}}\colon\mathsf{Cmd}\to\mathcal{S}\times\mathcal{H}\to\mathcal{W}_{\mathcal{A}}(\mathsf{St})$
is defined in Figure 1 and is parametric on an outcome algebra
$\mathcal{A}=\langle A,+,\cdot,\dsser{0},\dsser{1}\rangle$ and an allocator
function $\mathsf{alloc}\in\mathsf{Alloc}_{\mathcal{A}}$, described below. The
semantics of expressions
$\left\llbracket-\right\rrbracket\colon\mathsf{Exp}\to\mathcal{S}\to\mathsf{Val}$
is omitted, but is defined in the obvious way. The set of states is
$\mathsf{St}=(\mathcal{S}\times\mathcal{H})+(\mathcal{S}\times\mathcal{H})+1$,
where $\mathcal{S}=\\{s:\mathsf{Var}\cup\mathsf{LVar}\to\mathsf{Val}\\}$ are
stores (assigning values to both program variables $x\in\mathsf{Var}$ and
logical variables $X\in\mathsf{LVar}$) and
$\mathcal{H}=\\{h:\mathsf{Addr}\rightharpoonup\mathsf{Val}\cup\\{\bot\\}\\}$
are heaps. In the style of Raad et al. (2020), a heap is both a _partial_
mapping and also includes $\bot$ in the codomain, distinguishing between cases
with no information about an address ($\ell\notin\mathsf{dom}(h)$) vs cases
where a pointer is explicitly deallocated ($h(\ell)=\bot$). We additionally
assume that $\\{\mathsf{null}\\}\cup A\subseteq\mathsf{Val}$,
$\mathsf{Addr}\subseteq\mathsf{Val}$ and $\mathsf{null}\notin\mathsf{Addr}$.

Allocators are functions mapping $(s,h)$ to a collection of addresses and
values with cumulative weight of $\dsser{1}$, and each address $\ell$ is not
in the domain of $h$. Allocators can use the same effects supported by the
language semantics (_i.e.,_ nondeterminism or random choice). Formally,
allocators come from the following set.

$\mathsf{Alloc}_{\mathcal{A}}=\left\\{f\colon\mathcal{S}\times\mathcal{H}\to\mathcal{W}_{\mathcal{A}}(\mathsf{Addr}\times\mathsf{Val})\quad\middle|\quad\forall(s,h).\begin{array}[]{l}|f(s,h)|=\dsser{1}\quad\text{and}\\\
\forall(\ell,v)\in\mathsf{supp}(f(s,h)).~{}\ell\notin\mathsf{dom}(h)\end{array}\right\\}$

A deterministic allocator
$\mathsf{alloc\\_det}(s,h)=\mathsf{unit}(\min(\mathsf{Addr}\setminus\mathsf{dom}(h)),0)$
that always picks the first unused address is valid in all OSL instances. Note
that while logical variables $X\in\mathsf{LVar}$ cannot appear in program
expressions $e$, allocators _can_ depend on them. This allows us to model
allocators that depend on hidden state, such as kernel configuration that is
not visible in user space.

A global procedure table
$\mathsf{P}\colon\mathsf{Proc}\to\mathsf{Cmd}\times\vec{\mathsf{Var}}$ that
returns a command and vector of variable names (the arguments) given a
procedure name $f\in\mathsf{Proc}$ is used to interpret procedure calls. We
assume that all procedures used in programs are defined and pass the correct
number of arguments.

The monad operations give semantics to $\mathsf{skip}$ and $\fatsemi$, and
$C_{1}+C_{2}$ is defined as a sum whose meaning depends on the Outcome
Algebra. While loops are defined by a least fixed point, which is guaranteed
to exist (see Theorem A.9). Since the semiring plus is partial, this sum may
be undefined; in Appendix A we discuss simple syntactic checks to ensure
totality. The semantics of $\mathsf{assume}~{}e$ weights the branch by the
value of $e$, as long as it is a valid program weight. Boolean expressions
evaluate to the semiring $\dsser{0}$ (false) or $\dsser{1}$ (true).

We define two operations before giving the semantics of atomic actions:
$\mathsf{error}(s,h)$ constructs an error state and
$\mathsf{update}(s,h,\ell,s^{\prime},h^{\prime})$ returns
$(s^{\prime},h^{\prime})$ if the address $\ell$ is allocated in $h$, it
returns an error if $\ell$ is deallocated, and returns $\mathsf{undef}$ if
$\ell\notin\mathsf{dom}(h)$. Assignment is defined in the usual way by
updating the program store; memory allocation uses $\mathsf{alloc}$ to obtain
a fresh address and initial value (or collection thereof); deallocation,
reads, and writes are implemented using update and errors use error. Procedure
names are looked up in $\mathsf{P}$ to obtain $C$ and $\vec{x}$ before running
$C$ on a store updated by setting $\vec{x}$ to have the values of the inputs
$\vec{e}$. We will additionally occasionally use the Kleisli extension of the
semantics $\left\llbracket
C\right\rrbracket^{\dagger}_{\mathsf{alloc}}\\!\\!(m)\colon\mathcal{W}_{\mathcal{A}}(\mathsf{St})\to\mathcal{W}_{\mathcal{A}}(\mathsf{St})$,
which takes as input a collection of states instead of a single one. It is
defined $\left\llbracket
C\right\rrbracket^{\dagger}_{\mathsf{alloc}}\\!\\!(m)=\mathsf{bind}(m,\left\llbracket
C\right\rrbracket_{\mathsf{alloc}})$.

##  4\. Outcome Separation Logic

We now proceed to formalize Outcome Separation Logic (OSL) and the frame rule.
First, we define an assertion logic for the pre- and postconditions of outcome
triples. These assertions are based on the outcome assertions of Zilberstein
et al. (2023), using SL assertions as basic predicates.

Outcome Assertions. The syntax for OSL assertions is below and the semantics
is in Figure 2. Both are parametric on an Outcome Algebra $\langle
A,+,\cdot,\dsser{0},\dsser{1}\rangle$.

$\varphi\Coloneqq\top\mid\varphi\vee\psi\mid\varphi\oplus\psi\mid\varphi^{(a)}\mid\epsilon:P\qquad\quad\left(a\in
A,\epsilon\in\\{\mathsf{ok},\mathsf{er}\\},P\in\dsser{2}^{\mathcal{S}\times\mathcal{H}}\right)$

Outcome assertions include familiar constructs such as $\top$ (always true)
and disjunctions. The outcome conjunction $\varphi\oplus\psi$ splits $m$ into
two pieces, $m_{1}\vDash\varphi$ and $m_{2}\vDash\psi$, summing to $m$.
Weighting $\varphi^{(a)}$ guarantees that if $m\vDash\varphi$, then $a\cdot
m\vDash\varphi^{(a)}$. Combining these, we also define probabilistic choice:
$\varphi\oplus_{p}\psi\triangleq\varphi^{(p)}\oplus\psi^{(1-p)}$, meaning that
$\varphi$ occurs with probability $p$ and $\psi$ occurs with probability $1-p$
for some probability $p\in[0,1]$.

$\begin{array}[]{lll}m\vDash\top&\lx@intercol\text{always}\hfil\lx@intercol\\\
m\vDash\varphi\lor\psi&\text{iff}&m\vDash\varphi\quad\text{or}\quad
m\vDash\psi\\\ m\vDash\varphi\oplus\psi&\text{iff}&\exists m_{1},m_{2}.\quad
m=m_{1}+m_{2}\quad\text{and}\quad m_{1}\vDash\varphi\quad\text{and}\quad
m_{2}\vDash\psi\\\
m\vDash\varphi^{(a)}&\text{iff}&a=\dsser{0}~{}\text{and}~{}m=\dsser{0}\quad\text{or}\quad\exists
m^{\prime}.\quad m=a\cdot m^{\prime}\quad\text{and}\quad
m^{\prime}\vDash\varphi\\\
m\vDash\epsilon:P&\text{iff}&|m|=\dsser{1}\quad\text{and}\quad\forall\sigma\in\mathsf{supp}(m).\quad\exists(s,h).\quad\sigma=\dsser{i}_{\epsilon}(s,h)\quad\text{and}\quad(s,h)\in
P\end{array}$ Figure 2. Semantics of outcome assertions given an outcome
algebra $\langle A,+,\cdot,\dsser{0},\dsser{1}\rangle$.

Finally, basic assertions $(\mathsf{ok}:P)$ and $(\mathsf{er}:Q)$ require that
$|m|=\dsser{1}$—ensuring that the set of outcomes is nonempty in the
(non)deterministic cases (Definitions 3.5 and 3.4) or that the assertion
occurs with probability 1 (Definition 3.6)—and that all states in
$\mathsf{supp}(m)$ terminated successfully and satisfy $P$ or crashed and
satisfy $Q$, respectively, where
$P,Q\in\dsser{2}^{\mathcal{S}\times\mathcal{H}}$ are semantic heap assertions.
These heap assertions are defined as in standard separation logic, for
example:

$\displaystyle\mathsf{emp}$ $\displaystyle\triangleq\\{(s,\emptyset)\mid
s\in\mathcal{S})\\}$ $\displaystyle P\ast Q$
$\displaystyle\triangleq\\{(s,h_{1}\uplus h_{2})\mid(s,h_{1})\in
P,(s,h_{2})\in Q\\}$ $\displaystyle e_{1}\mapsto e_{2}$
$\displaystyle\triangleq\\{(s,\\{\left\llbracket
e_{1}\right\rrbracket(s)\mapsto\left\llbracket
e_{2}\right\rrbracket(s)\\})\mid s\in\mathcal{S}\\}$

We were motivated to pick this particular set of outcome assertions in light
of our goal to define symbolic execution algorithms in the style of Calcagno
et al. (2009), which compute procedure summaries of the form
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{P\\}}~{}f(\vec{e})~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{Q_{1}\vee\cdots\vee
Q_{n}\\}}$ and the disjunctive post indicates a series of possible outcomes.
In our case, we exchange those disjunctions for outcome conjunctions in the
cases where the outcomes arise due to computational effects. We include $\top$
in order to drop outcomes using the assertion $\varphi\oplus\top$ (as
discussed in Section 2). Finally, we include disjunctions to express joins of
outcomes that occur due to logical choice, and also to express partial
correctness; whereas $\epsilon:P$ guarantees reachability,
$(\epsilon:P)\vee\top^{(\dsser{0})}$ also permits nontermination (no
outcomes).

OSL Triples. The semantics of OSL triples requires that the specification
holds when the program is run using _any_ allocator, ensuring that the
postcondition cannot say anything specific about which addresses were
obtained, as those addresses may change if the program is executed in a larger
heap.

###### Definition 4.1 (Outcome Separation Logic Triples).

For any outcome algebra $\mathcal{A}=\langle
A,+,\cdot,\dsser{0},\dsser{1}\rangle$:

$\vDash{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\psi\rangle}\qquad\text{iff}\qquad\forall
m\in\mathcal{W}_{\mathcal{A}}(\mathsf{St}),\mathsf{alloc}\in\mathsf{Alloc}_{\mathcal{A}}.\quad
m\vDash\varphi\quad\implies\quad\left\llbracket
C\right\rrbracket^{\dagger}_{\mathsf{alloc}}\\!\\!(m)\vDash\psi$

The inference rules for OSL carry over from standard Outcome Logic
(Zilberstein, 2024, Fig. 3), along with the small axioms of separation logic
(O’Hearn et al., 2001). It is also fairly straightforward to derive inference
rules from our symbolic execution algorithm (Figure 5). Instead of repeating
the rules here, we discuss the new local reasoning principle that OSL
supports, namely the frame rule.

###  4.1. The Frame Rule

We now build the necessary foundations to introduce and prove the soundness of
the frame rule. First, we define a new separating conjunction as a
transformation on outcome assertions, using the symbol $\circledast$ to
distinguish it from the usual separating conjunction $\ast$ on symbolic heaps;
$\circledast$ is a binary operation taking an outcome assertion and an SL
assertion (rather than two SL assertions like $\ast$). The operation is
defined below, where ${\bowtie}\Coloneqq\oplus\mid\vee$.

$\top\circledast F\triangleq\top\quad(\varphi\bowtie\psi)\circledast
F\triangleq(\varphi\circledast F)\bowtie(\psi\circledast
F)\quad\varphi^{(a)}\circledast F\triangleq(\varphi\circledast
F)^{(a)}\quad(\epsilon:P)\circledast F\triangleq\epsilon:P\ast F$

So, $\circledast$ has no effect on $\top$, it distributes over $\vee$,
$\oplus$, and $(-)^{(a)}$, and for basic assertions $\epsilon:P$, we simply
join $P\ast F$ with the regular separating conjunction. We can now express the
frame rule.

$\inferrule{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\psi\rangle}\\\
\mathsf{mod}(C)\cap\mathsf{fv}(F)=\emptyset}{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\varphi\circledast
F\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\psi\circledast
F\rangle}}{\textsc{Frame}}$

This rule resembles the frame rule of other separation logics, with the same
side condition that $F$ cannot mention any modified program variables.
However, as we described in Section 2.2, OSL’s expressivity goes beyond that
of existing separation logics, meaning that this frame rule can be used for
both may and must properties in nondeterministic programs, as well as
quantitative properties in probabilistic programs. Further, all of these
capabilities stem from a single soundness proof.

The key to the proof is the _frame property_ (Lemma C.7), which roughly states
that for any $(s,h)\in\mathcal{S}\times\mathcal{H}$, allocator
$\mathsf{alloc}$, and $h^{\prime}$ such that $(s,h^{\prime})\vDash F$, we can
construct a new allocator $\mathsf{alloc}^{\prime}$ such that adding
$h^{\prime}$ to each end state of $\left\llbracket
C\right\rrbracket_{\mathsf{alloc}^{\prime}}(s,h)$ gives us $\left\llbracket
C\right\rrbracket_{\mathsf{alloc}}(s,h\uplus h^{\prime})$ (modulo the
$\mathsf{undef}$ states), guaranteeing that if $\left\llbracket
C\right\rrbracket_{\mathsf{alloc}^{\prime}}(s,h)\vDash\psi$, then
$\left\llbracket C\right\rrbracket_{\mathsf{alloc}}(s,h\uplus
h^{\prime})\vDash\psi\circledast F$. We formalize this idea in the remainder
of the section.

The formalization of the frame property relies on _lifted relations_ , which
describe the relation between two weighted collections in terms of a relation
on individual states. Before we define this formally, we define the notion of
projections $\pi_{1}\colon\mathcal{W}(X\times Y)\to\mathcal{W}(X)$ and
$\pi_{2}\colon\mathcal{W}(X\times Y)\to\mathcal{W}(Y)$, which extract
component weighting functions from weighting functions over a cartesian
product.

$\pi_{1}(m)(x)=\smashoperator[]{\sum_{y\in
Y}^{}}m(x,y)\qquad\qquad\pi_{2}(m)(y)=\smashoperator[]{\sum_{x\in
X}^{}}m(x,y)$

Given these projections, we say that $m_{1}\in\mathcal{W}(X)$ and
$m_{2}\in\mathcal{W}(Y)$ are related by $R$ iff there is some weighting
function $m\in\mathcal{W}(X\times Y)$ whose projections are $m_{1}$ and
$m_{2}$, and where each pair $(x,y)\in\mathsf{supp}(m)$ is related by $R$.
This notion corresponds to the idea of lifting via spans (Kurz and Velebil,
2016) and is defined formally below.

###### Definition 4.2 (Relation Liftings).

Given a relation $R\subseteq X\times Y$, we define a lifting of $R$ on
weighting functions
$\overline{R}\subseteq\mathcal{W}_{\mathcal{A}}(X)\times\mathcal{W}_{\mathcal{A}}(Y)$
as follows:

$\overline{R}=\Big{\\{}~{}(m_{1},m_{2})~{}\Big{|}~{}\exists
m\in\mathcal{W}_{\mathcal{A}}(R).\quad m_{1}=\pi_{1}(m)\quad\text{and}\quad
m_{2}=\pi_{2}(m)~{}\Big{\\}}$

Semantics of the Outcome Separating Conjunction. We now prove semantic
properties about $\circledast$ that allow us to relate program configurations
satisfying $\varphi$ to ones that satisfy $\varphi\circledast F$. First, we
need to relate states satisfying $P$ to states satisfying $P\ast F$.

$\mathsf{frame}(F)=\big{\\{}\left(\dsser{i}_{\epsilon}(s,h),\dsser{i}_{\epsilon}(s,h\uplus
h^{\prime})\right)\mid\dsser{i}_{\epsilon}(s,h)\in\mathsf{St},(s,h^{\prime})\in
F\big{\\}}\cup\big{\\{}(\mathsf{undef},\mathsf{undef})\big{\\}}$

Any state $\dsser{i}_{\epsilon}(s,h)$ is related to all states
$\dsser{i}_{\epsilon}(s,h\uplus h^{\prime})$ such that $(s,h^{\prime})\in F$,
which guarantees that if $(s,h)\in P$, then $(s,h\uplus h^{\prime})\in P\ast
F$. Undefined states are only related to themselves. Now, we can express the
semantics of $\circledast$ by lifting this relation.

###### Lemma 4.3.

If $m\vDash\varphi$ and $(m,m^{\prime})\in\overline{\mathsf{frame}(F)}$, then
$m^{\prime}\vDash\varphi\circledast F$

It is tempting to say that the converse should also hold, but that is not
quite right. We took $\top\circledast F$ to be equal to $\top$, therefore if
$m\vDash\top\circledast F$, then we cannot guarantee that all the states in
$m$ contain information about $F$. We therefore characterize the semantics
only for the states that are not covered by $\top$, leaving the other states
unconstrained.

###### Lemma 4.4.

If $m\vDash\varphi\circledast F$, then there exist $m_{1}$, $m^{\prime}_{1}$,
and $m_{2}$ such that $(m_{1},m^{\prime}_{1})\in\overline{\mathsf{frame}(F)}$,
$m=m_{1}^{\prime}+m_{2}$ and $m_{1}+m^{\prime}_{2}\vDash\varphi$ for any
$m_{2}^{\prime}$ such that $|m_{2}^{\prime}|\leq|m_{2}|$.

In the lemma above, $m_{1}^{\prime}$ represents the nontrivial portion of $m$
and $m_{2}$ is the portion of $m$ that is covered by $\top$. As such,
$m^{\prime}_{1}$ must be the result of framing $F$ into some $m_{1}$. Since
$m_{2}$ is covered by $\top$, we can replace it with anything smaller than
$m_{2}$—$\top$ can absorb at least $|m_{2}|$ worth of weight. These two lemmas
provide a semantic basis to reason about what it means for $\varphi\circledast
F$ to hold relative to $\varphi$.

######  Remark 1 (Asymmetry of the Separating Conjunction).

One could imagine a symmetric definition of $\circledast$, defined
semantically as follows: $m\vDash\varphi\circledast\psi$ iff there exist
$m_{1}\vDash\varphi$ and $m_{2}\vDash\psi$, such that $m_{1}$ and $m_{2}$ are
obtained by _marginalizing_ $m$. More precisely,
$m_{1}(\dsser{i}_{\epsilon}(s,h))$ is equal to the sum of
$m(\dsser{i}_{\epsilon}(s,h\uplus h^{\prime}))$ over all $h^{\prime}$ such
that $\dsser{i}_{\epsilon}(s,h^{\prime})\in\mathsf{supp}(m_{2})$ (and a
similar formula holds for $m_{2}$).

This gives expected properties, for example $(\mathsf{ok}:x\mapsto 1\ast
y\mapsto 2)\oplus(\mathsf{ok}:x\mapsto 3\ast y\mapsto 4)$ implies
$\left((\mathsf{ok}:x\mapsto 1)\oplus(\mathsf{ok}:x\mapsto
3)\right)\circledast\left((\mathsf{ok}:y\mapsto 2)\oplus(\mathsf{ok}:y\mapsto
4)\right)$. However, this approach does not work smoothly with the frame rule.
As a simple counterexample, consider the triple
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:x\not\mapsto\rangle}~{}[x]\leftarrow
1~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{er}:x\not\mapsto\rangle}$,
using the frame rule with $(\mathsf{ok}:y\mapsto 2)$ gives us the precondition
$(\mathsf{ok}:{x\not\mapsto}\ast y\mapsto 2)$, but the postcondition is false
since there is no way to combine an $\mathsf{er}$ assertion with an
$\mathsf{ok}$ one. Other problems occur when some of the program paths
diverge.

The asymmetric definition of $\circledast$ fits our needs, as the spirit of
the frame rule is to run a computation in a larger _heap_ —adding pointers,
but not outcomes. This is in line with how framing is used by Calcagno et al.
(2009), where framing distributes over disjunctions in the postconditions of
Hoare Triples. That is not to say that the symmetric $\circledast$ is useless.
In fact, it could be used in a concurrent variant of Outcome Logic to divide
resources among two parallel branches in the style of Concurrent Separation
Logic (O’Hearn, 2004), but that is out of scope for this paper.

Replacement of Unsafe States. Undefined states arise from dereferencing
pointers not in the domain of the heap. Those pointers may be in the domain of
a larger heap, so previously undefined outcomes can become defined after
framing in more pointers. The soundness of the frame rule depends on this not
affecting the truth of the postcondition.

Whereas standard separation logic is _fault avoiding_ —it requires that all
states satisfying the precondition will not encounter unknown pointers—we omit
this requirement in OSL in order to efficiently reason about incorrectness by
only exploring a subset of the program paths. For example, in the triple
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:x\not\mapsto\rangle}~{}\mathsf{free}(x)+C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{er}:x\not\mapsto)\oplus\top\rangle}$,
the fact that the left path leads to a memory error is enough to conclude that
the program is incorrect; exploring the right path would be wasted effort.
However, the right path may use other pointers not mentioned in the
precondition, meaning that executing $C$ will lead to $\mathsf{undef}$. This
is fine, since the assertion $\top$ covers undefined states.

However, if we use the frame rule to add information about more pointers to
the precondition, the result may no longer be $\mathsf{undef}$. This is still
valid— _any_ outcome from running $C$ trivially satisfies $\top$. To formalize
this, we use
$\mathsf{Rep}\subseteq\mathsf{St}\times(\mathsf{St}\cup\\{\lightning\\})$,
which relates $\mathsf{undef}$ to any state $\sigma\in\mathsf{St}$ or
$\lightning$ (representing nontermination)333 Previously undefined states may
diverge after adding more pointers, _e.g.,_ running
$\mathsf{free}(x)\fatsemi\mathsf{while}~{}\mathsf{true}~{}\mathsf{do}~{}\mathsf{skip}$
in an empty heap leads to $\mathsf{undef}$ whereas it will not terminate if
$x$ is allocated.. All other states ($\mathsf{ok}$ and $\mathsf{er}$) are
related only to themselves. In addition, since $\lightning$ is not a state, we
define an operation $\mathsf{prune}(m)$ to remove it. The formal definitions
of both $\mathsf{Rep}$ and $\mathsf{prune}$ are given in Section C.2. The
replacement lemma guarantees that undefined states can be replaced without
affecting the validity of an assertion.

###### Lemma 4.5 (Replacement).

If $m\vDash\varphi$ and $(m,m^{\prime})\in\overline{\mathsf{Rep}}$, then
$\mathsf{prune}(m^{\prime})\vDash\varphi$

Soundness. We now have all the ingredients needed to prove the soundness of
the frame rule.

###### Theorem 4.6 (The Frame Rule).

If
$\vDash{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\psi\rangle}$
and $\mathsf{mod}(C)\cap\mathsf{fv}(F)=\emptyset$, then
$\vDash{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\varphi\circledast
F\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\psi\circledast
F\rangle}$.

We briefly sketch the proof here, the full version is in Section C.3. Suppose
that $m\vDash\varphi\circledast F$ and take any
$\mathsf{alloc}\in\mathsf{Alloc}$. We now enumerate all the defined states of
$m$ and (using Lemma 4.4) we know that each state has the form
$\sigma_{n}=\dsser{i}_{\epsilon_{n}}(s_{n},h_{n}\uplus h^{\prime}_{n})$ where
$(s_{n},h^{\prime}_{n})\in F$. We pick a fresh logical variable $X$ and
construct $m^{\prime}$ by modifying each $\sigma_{n}\in\mathsf{supp}(m)$ to be
$\dsser{i}_{\epsilon_{n}}(s_{n}[X\mapsto n],h_{n})$. That is, we augment the
variable store such that $X=n$ and remove the $h^{\prime}_{n}$ portion of the
heap. Note that $m^{\prime}\vDash\varphi$. We construct a new allocator as
follows:

$\mathsf{alloc}^{\prime}(s,h)=\mathsf{alloc}(s[X\mapsto s_{n}(X)],h\uplus
h^{\prime}_{n})\qquad\text{where}~{}n=s(X)$

So, $\mathsf{alloc}^{\prime}(s,h)$ uses the value $s(X)=n$ to select the
appropriate $h^{\prime}_{n}$ to add to $h$, guaranteeing that $\left\llbracket
C\right\rrbracket_{\mathsf{alloc}^{\prime}}\\!(s_{n},h_{n})$ allocates the
same addresses as $\left\llbracket
C\right\rrbracket_{\mathsf{alloc}}\\!(s_{n},h_{n}\uplus h^{\prime}_{n})$ for
all $n$. So, $\left\llbracket
C\right\rrbracket^{\dagger}_{\mathsf{alloc}}\\!\\!(m)$ is related to
$\left\llbracket
C\right\rrbracket^{\dagger}_{\mathsf{alloc}^{\prime}}\\!\\!(m^{\prime})$ via
the two relations described previously. By the premise
$\vDash{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\psi\rangle}$,
we know that $\left\llbracket
C\right\rrbracket^{\dagger}_{\mathsf{alloc}^{\prime}}\\!\\!(m^{\prime})\vDash\psi$,
and by Lemmas 4.3 and 4.5, we conclude that $\left\llbracket
C\right\rrbracket^{\dagger}_{\mathsf{alloc}}\\!\\!(m)\vDash\psi\circledast F$.

We have devised a frame rule for Outcome Separation Logic, which supports a
rich variety of computational effects and properties about those effects. More
concretely, OSL can be used to reason about both correctness and incorrectness
across nondeterministic and probabilistic programs. In the next sections, we
will build on this result to create compositional symbolic execution
algorithms.

##  5\. Symbolic Execution

With a sound frame rule, we are now ready to design symbolic execution
algorithms based on OSL. The core algorithm is similar to Abductor and Infer
(Calcagno et al., 2009, 2015), but adapted to better handle program choices
arising from computational effects. We also show how minor modifications to
this algorithm make it suitable for other use cases such as bug-finding and
partial correctness. First, we introduce a restricted assertion syntax to make
OSL compatible with bi-abduction, then we define tri-abduction (Section 5.1)
and the main algorithm (Section 5.2).

Symbolic Heaps. In the remainder of the paper, we will work with a subset of
SL assertions known as symbolic heaps. Although they have limited
expressivity—particularly for pure assertions—implications of symbolic heaps
are decidable (Berdine et al., 2005a), which is necessary for bi-abductive
analysis algorithms. These same symbolic heaps are used by Calcagno et al.
(2009, 2011). The syntax is shown below and the semantics is standard as
defined by Berdine et al. (2005b, §2).

$\displaystyle P$ $\displaystyle\Coloneqq\exists\vec{X}.\Delta$ (Symbolic
Heaps) $\displaystyle\Delta$ $\displaystyle\Coloneqq\Pi\land\Sigma$
(Quantifier-Free Symbolic Heaps) $\displaystyle\Pi$
$\displaystyle\Coloneqq\mathsf{true}\mid\Pi_{1}\land\Pi_{2}\mid
e_{1}=e_{2}\mid e_{1}\neq e_{2}$ (Pure Assertions) $\displaystyle\Sigma$
$\displaystyle\Coloneqq\mathsf{true}\mid\mathsf{emp}\mid\Sigma_{1}\ast\Sigma_{2}\mid
e_{1}\mapsto e_{2}\mid\mathsf{ls}(e_{1},e_{2})$ (Spatial Assertions)

A symbolic heap $P$ consists of existentially quantified logical variables,
along with a pure part $\Pi$ and a spatial part $\Sigma$. Pure assertions are
conjunctions of equalities and inequalities, whereas spatial assertions are
heap assertions joined by _separating_ conjunctions. The separating
conjunction requires that the heap can be split into disjoint components to
satisfy the two assertions separately.

$(s,h)\vDash\Sigma_{1}\ast\Sigma_{2}\qquad\text{iff}\qquad\exists
h_{1},h_{2}.\quad h=h_{1}\uplus
h_{2}\quad\text{and}\quad(s,h_{1})\vDash\Sigma_{1}\quad\text{and}\quad(s,h_{2})\vDash\Sigma_{2}$

The points-to predicate $e_{1}\mapsto e_{2}$ specifies a singleton heap in
which the address $e_{1}$ points to the value $e_{2}$. Negative heap
assertions $e\not\mapsto$ are syntactic sugar for $e\mapsto\bot$. These
assertions were introduced in Incorrectness Separation Logic to prove that a
program crashes when dereferencing invalidated memory (Raad et al., 2020).
Finally, list segments $\mathsf{ls}(e_{1},e_{2})$ are inductive predicates
stating that a sequence of pointers starts with $e_{1}$ and ends with $e_{2}$.
Formally, it is the least solution of
$\mathsf{ls}(e_{1},e_{2})\Leftrightarrow(e_{1}=e_{2}\land\mathsf{emp})\vee(\exists
X.e_{1}\mapsto X\ast\mathsf{ls}(X,e_{2}))$. We also overload $\ast$ and
$\land$ as follows:

$(\exists\vec{X}.\Pi\land\Sigma)\ast(\exists\vec{Y}.\Pi^{\prime}\land\Sigma^{\prime})\triangleq\exists\vec{X}\vec{Y}.(\Pi\land\Pi^{\prime})\land(\Sigma\ast\Sigma^{\prime})\qquad
P\land\Pi\triangleq P\ast(\Pi\land\mathsf{emp})$

###  5.1. Tri-Abduction

We now address the matter of composing paths in programs whose execution
branches due to nondeterminism or random sampling. When symbolically executing
such programs, we must unify the preconditions of the two branches. For
example, the following program chooses to execute $[x]\leftarrow 1$ or
$[y]\leftarrow 2$, so we need a precondition that mentions both $x$ and $y$,
and we need to know what leftover resources to add to the two resulting
outcomes.

|  |  |
---|---|---|---
$\textstyle{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:x\mapsto
X\rangle}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{[x]\leftarrow
1}$$\textstyle{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:x\mapsto
1\rangle}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:\mathord{\textbf{{?}}}\rangle}}$
$\textstyle{+}$
$\textstyle{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{ok}:x\mapsto
1\ast\mathord{\textbf{{?}}})}}$$\textstyle{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\oplus}}$$\textstyle{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}(\mathsf{ok}:y\mapsto
2\ast\mathord{\textbf{{?}}})\rangle}}$$\textstyle{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:y\mapsto
Y\rangle}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{[y]\leftarrow
2}$$\textstyle{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:y\mapsto
2\rangle}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

Tri-abduction provides us the power to reconcile the preconditions of the two
program branches. Given $P_{1}$ and $P_{2}$, the goal is to find the _anti-
frame_ $M$ and two _leftover_ frames $F_{1}$ and $F_{2}$ that make $P_{1}\ast
F_{1}\mathrel{\mathchoice{\reflectbox{$\displaystyle\vDash$}}{\reflectbox{$\textstyle\vDash$}}{\reflectbox{$\scriptstyle\vDash$}}{\reflectbox{$\scriptscriptstyle\vDash$}}}M\vDash
P_{2}\ast F_{2}$ hold. Using this, we can compose program branches as follows:

$\inferrule{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle
P_{1}\rangle}~{}C_{1}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle
Q_{1}\rangle}\\\ P_{1}\ast
F_{1}\mathrel{\mathchoice{\reflectbox{$\displaystyle\vDash$}}{\reflectbox{$\textstyle\vDash$}}{\reflectbox{$\scriptstyle\vDash$}}{\reflectbox{$\scriptscriptstyle\vDash$}}}M\vDash
P_{2}\ast F_{2}\\\
{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle
P_{2}\rangle}~{}C_{2}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle
Q_{2}\rangle}}{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle
M\rangle}~{}C_{1}+C_{2}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(Q_{1}\ast
F_{1})\oplus(Q_{2}\ast F_{2})\rangle}}{\textsc{Tri-Abductive Composition}}$

Tri-abduction would have also been useful in Abductor, which is unable to
analyze the program above despite supporting nondeterminism. Abductor operates
in two passes; first finding candidate preconditions for each trace, and then
re-evaluating the program with each candidate in hopes that one is valid for
the entire program (Calcagno et al., 2009). Since the program above uses
disjoint resources in the two branches, no candidate is valid for all traces.
Using tri-abduction, we infer _more_ summaries and do so in a single pass.
While a single-pass bi-abduction algorithm has more recently been proposed
(Sextl et al., 2023), it still cannot handle the case in the following remark.

######  Remark 2 (Solving Tri-Abduction using Bi-Adbuction).

Our initial approach to tri-abduction was to simply use bi-abduction: given
$P_{1}$ and $P_{2}$, bi-abduction can give us $M$ and $F$ such that $P_{1}\ast
M\vDash P_{2}\ast F$. Using $P_{1}\ast M$ as the anti-frame, $P_{1}\ast
M\mathrel{\mathchoice{\reflectbox{$\displaystyle\vDash$}}{\reflectbox{$\textstyle\vDash$}}{\reflectbox{$\scriptstyle\vDash$}}{\reflectbox{$\scriptscriptstyle\vDash$}}}(P_{1}\ast
M)\vDash P_{2}\ast F$ is a tri-abduction solution.

However, this approach is inherently asymmetric, with the left branch being
favored. While it would be possible to also bi-abduce in the opposite
direction ($P_{2}\ast\mathord{\textbf{?}}\vDash
P_{1}\ast\mathord{\textbf{?}}$) for symmetry, this still precludes valid
solutions, _e.g.,_ there is no bi-abduction solution for $X\mapsto
Y\ast\mathsf{ls}(Y,Z)$ and $\mathsf{ls}(X,Y)\ast Y\mapsto Z$ (in either
direction), whereas tri-abduction finds the anti-frame $X\mapsto Y\ast
Y\mapsto Z$. Tri-abduction is a fundamentally different operation that is
precisely designed for branching.

Similar to (Calcagno et al., 2011, Algorithm 3), tri-abduction is done in two
stages. First, we describe the _abduction_ stage, in which only the anti-frame
$M$ is inferred. Next, we describe how abduction is used as a subroutine to
tri-abduce all three parameters $M$, $F_{1}$, and $F_{2}$.

Abduction. The abductive inference step $\textsf{abduce-par}(P,Q)$ is
performed as a proof search—similar to Calcagno et al. (2011, Algorithm
1)—using the rules in Figure 3 to infer judgements of the form $P\lhd[M]\rhd
Q$, indicating that $M\vDash P$ and $M\vDash Q$. As such, $P$ and $Q$ are the
inputs to the algorithm and $M$ is the output. We describe the algorithm
briefly, the full definition is in Appendix D.

The inference rules are applied in the order in which they are shown, with the
rules at the top being preferred over the rules lower down. The inference
rules ending with -L have symmetric versions that can also be applied (the
full set of rules is shown in Figure 6).

The premise of each inference rule becomes a recursive call, finding a
solution to a smaller abduction query. Some of the rules have side conditions
of the form of $R\not\vdash\mathsf{false}$, which is checked using the proof
system of Berdine et al. (2005b, §4). Given that each recursive call describes
a progressively smaller symbolic heap, the algorithm either eventually reaches
a case with no explicit resources ($\mathsf{emp}$ or $\mathsf{true}$), in
which a base rule applies, or gets stuck and returns no solutions. The
inference rules are described below.

Base Cases

$\inferrule*[rightstyle={\footnotesize\sc},right=\hypertarget{rule:Base-
Emp}{\textsc{Base-
Emp}}]{\Pi\wedge\Pi^{\prime}\not\vdash\mathsf{false}}{\Pi\land\mathsf{emp}\lhd[\Pi\wedge\Pi^{\prime}\land\mathsf{emp}]\rhd\Pi^{\prime}\land\mathsf{emp}}\qquad\inferrule*[rightstyle={\footnotesize\sc},right=\hypertarget{rule:Base-
True-L}{\textsc{Base-
True-L}}]{\Pi\wedge\Pi^{\prime}\land\Sigma^{\prime}\not\vdash\mathsf{false}}{\Pi\land\mathsf{true}\lhd[\Pi\wedge\Pi^{\prime}\land\Sigma^{\prime}]\rhd\Pi^{\prime}\land\Sigma^{\prime}}$

Quantifier Elimination

$\inferrule*[rightstyle={\footnotesize\sc},right=\hypertarget{rule:Exists}{\textsc{Exists}}]{\Delta\lhd[M]\rhd\Delta^{\prime}\\\
\vec{X}\cap(\mathsf{fv}(\Delta^{\prime})\setminus\vec{Y})=\emptyset\\\
\vec{Y}\cap(\mathsf{fv}(\Delta)\setminus\vec{X})=\emptyset}{\exists\vec{X}.\Delta\lhd[\exists\vec{X}\vec{Y}.M]\rhd\exists\vec{Y}.\Delta^{\prime}}$

Resource Matching

$\inferrule*[rightstyle={\footnotesize\sc},right=\hypertarget{rule:Ls-
Start-L}{\textsc{Ls-
Start-L}}]{\Delta\ast\mathsf{ls}(e_{3},e_{2})\lhd[M]\rhd\Delta^{\prime}}{\Delta\ast\mathsf{ls}(e_{1},e_{2})\lhd[M\ast
e_{1}\mapsto e_{3}]\rhd\Delta^{\prime}\ast e_{1}\mapsto
e_{3}}\qquad\inferrule*[rightstyle={\footnotesize\sc},right=\hypertarget{rule:$\mapsto$-Match}{\textsc{$\mapsto$-Match}}]{\Delta\wedge
e_{2}=e_{3}\lhd[M]\rhd\Delta^{\prime}\wedge e_{2}=e_{3}}{\Delta\ast
e_{1}\mapsto e_{2}\lhd[M\ast e_{1}\mapsto e_{2}]\rhd\Delta^{\prime}\ast
e_{1}\mapsto e_{3}}$

$\inferrule*[rightstyle={\footnotesize\sc},right=\hypertarget{rule:Ls-
End-L}{\textsc{Ls-
End-L}}]{\Delta\ast\mathsf{ls}(e_{3},e_{2})\lhd[M]\rhd\Delta^{\prime}}{\Delta\ast\mathsf{ls}(e_{1},e_{2})\lhd[M\ast\mathsf{ls}(e_{1},e_{3})]\rhd\Delta^{\prime}\ast\mathsf{ls}(e_{1},e_{3})}$

Resource Adding

$\inferrule*[rightstyle={\footnotesize\sc},right=\hypertarget{rule:Missing-L}{\textsc{Missing-L}}]{\Delta\lhd[M]\rhd\Pi^{\prime}\land(\Sigma^{\prime}\ast\mathsf{true})\\\
\Pi^{\prime}\land\Sigma^{\prime}\ast
B(e_{1},e_{2})\not\vdash\mathsf{false}}{\Delta\ast B(e_{1},e_{2})\lhd[M\ast
B(e_{1},e_{2})]\rhd\Pi^{\prime}\land(\Sigma^{\prime}\ast\mathsf{true})}\quad\inferrule*[rightstyle={\footnotesize\sc},right=\hypertarget{rule:Emp-
Ls-L}{\textsc{Emp-Ls-L}}]{\Delta\land
e_{1}=e_{2}\lhd[M]\rhd\Delta^{\prime}\land
e_{1}=e_{2}}{\Delta\ast\mathsf{ls}(e_{1},e_{2})\lhd[M]\rhd\Delta^{\prime}}$

Figure 3. Selected abduction proof rules. Similarly to Calcagno et al. (2009),
$B(e_{1},e_{2})$ represents either $\mathsf{ls}(e_{1},e_{2})$ or $e_{1}\mapsto
e_{2}$. Rules ending in -L have symmetric versions not shown here; see Figure
6 for the full proof system.

Base Rules. The first step is to attempt to apply a base rule to complete the
proof. Base-Emp applies when both branches describe empty heaps, as long as
the pure assertions in each branch do not conflict. In Base-True-L, we match
against the case wherein one of the branches has an arbitrary spatial
assertion $\Sigma^{\prime}$ and the other contains the spatial assertion
$\mathsf{true}$, indicating that it can absorb more resources not explicitly
mentioned, so we are able to move $\Sigma^{\prime}$ into the anti-frame.

Quantifier Elimination. The next step is to strip existentials from the inputs
$P$ and $Q$ and add them back to the anti-frame $M$ obtained from the
recursive call. This is achieved using the Exists rule in Figure 3. In bi-
abduction, existentials are not stripped from the assertion to the right of
the entailment—doing so prevents the algorithm from finding solutions in some
cases. For example, $\mathsf{ls}(e,e^{\prime})\ast\textbf{?}\vDash\exists
X.e\mapsto X\ast\textbf{?}$ has a solution ($e\neq e^{\prime}$), but it does
not have a solution with the existential removed since nothing can be added to
$\mathsf{ls}(e,e^{\prime})$ to force $e$ to point to a _specific_ $X$. Tri-
abduction produces a standalone anti-frame $M$, so we are not operating under
such constraints, allowing us to strip existentials at an early step in order
to simplify further analysis.

It is important to note that in the Exists rule, quantified variables in one
assertion cannot overlap with the free variables of the other. This ensures
that no free variables in $P$ or $Q$ end up existentially quantified in the
anti-frame $M$. Without the side condition, the rule is unsound; suppose we
want to tri-abduce $\exists X.X=Y$ with $X=1$, then Exists gives us the anti-
frame $\exists X.X=Y\land X=1$, which is too weak since $\exists
X.X=1\not\vDash X=1$. In practice, our symbolic execution algorithm always
generates fresh logical variables, so we will not have collisions with our
usage of the Exists rule.

Resource Matching. If a base rule does not apply, then we attempt to match
resources from both branches, and then call the algorithm recursively on
smaller symbolic heaps with some resources moved into the returned anti-frame.
Ls-Start-L applies when both branches contain the same resource $e_{1}$;
however, one includes $e_{1}$ as the head of a list segment and the other
refers to $e_{1}$ using a points-to predicate. The points-to predicate must be
the head of the list, so we move it into $M$ and recurse on the tail of the
list. The $\mapsto$-Match rule applies when both branches use $e_{1}$ in a
points-to predicate, therefore the values pointed to must be equal too. Ls-
End-L applies when both branches have list segments starting at the same
address, so one segment must be a prefix of the other.

As in Calcagno et al. (2009), we do not consider cases where pointers are
aliased. For example, if the two branches are $x\mapsto 1$ and $y\mapsto 1$,
then it is possible that $x=y$. Precluding this solution helps limit the
number of options we consider. Calcagno et al. (2009, Example 3) remark that
this loss of precision is not detrimental in practice.

Resource Adding. Adding resources that are only present on one side is the
last resort, since it involves checking a potentially expensive side condition
of the form $\Pi\land\Sigma\ast B(e_{1},e_{2})\not\vdash\mathsf{false}$. The
Missing-L rule handles the case wherein one branch refers to resources not
present in the other. This is different from the Base-True-L rule, since it
handles cases where _both_ branches refer to resources not explicitly present
in the other. For example, Missing-L can solve $x\mapsto
X\ast\mathsf{true}\lhd[\textbf{?}]\rhd y\mapsto Y\ast\mathsf{true}$ even
though the Base-True rules do not apply. If one side of the judgement contains
a list segment, but the other side does _not_ contain the spatial assertion
$\mathsf{true}$, then there is a possible solution where the list segment is
empty. Emp-Ls-L handles such cases by forcing the list segment to be empty.

As we mentioned at the beginning of the section, the tri-abduction algorithm
follows a similar structure to that of bi-abduction (Calcagno et al., 2011,
Algorithm 3).

$\mathsf{triab}(P,Q)=\\{(M,F_{1},F_{2})\mid M\in\textsf{abduce-
par}(P\ast\mathsf{true},Q\ast\mathsf{true}),\;M\vdash P\ast F_{1},\;M\vdash
Q\ast F_{2}\\}$

We first abduce a set of anti-frames using Algorithm 1 such that $M\vDash
P\ast\mathsf{true}$ and $M\vDash Q\ast\mathsf{true}$ for each $M$. Adding the
spatial assertion $\mathsf{true}$ absorbs extra resources; if $P$ and $Q$ have
different memory footprints, then there is no $M$ such that $P\lhd[M]\rhd Q$,
but adding $\mathsf{true}$ to both sides of the entailments allows $M$ to
refer to resources present in only one branch. Next, we use the frame
inference procedure from Berdine et al. (2005b, §5) to find $F_{1}$ and
$F_{2}$ such that $M\vDash P\ast F_{1}$ and $M\vDash Q\ast F_{2}$. Applying
frame inference is necessary because $M$ may mention resources present in $P$,
but not $Q$ (and vice versa). The set of solutions is valid according to the
following correctness result, which follows from the soundness of the proof
system in Berdine et al. (2005b, §5).

###### Theorem 5.1 (Tri-abduction).

If $(M,F_{1},F_{2})\in\mathsf{triab}(P,Q)$, then $M\vDash P\ast F_{1}$ and
$M\vDash Q\ast F_{2}$

###  5.2. Symbolic Execution Algorithm

The algorithm is presented as a symbolic execution, which computes an abstract
semantics for a program—denoted $\left\llbracket
C\right\rrbracket^{\sharp}(T)$—represented as a set of pairs of pre- and
postconditions. The precondition is a single symbolic heap $P$, whereas the
postcondition is an outcome assertion $\varphi$. The parameter $T$ is a lookup
table that gets updated with summaries for procedures as the analysis moves
through the codebase. Intuitively, we think about specifications as starting
in a single state and producing a collection of outcomes, as the execution may
branch due to effects. Abductor operates in a similar fashion, but the
postcondition is a disjunction rather than an outcome conjunction. The
intended semantics is captured by the following soundness result.

###### Theorem 5.2 (Symbolic Execution Soundness).

If $(P,\varphi)\in\left\llbracket C\right\rrbracket^{\sharp}(T)$, then
$\vDash{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\varphi\rangle}$

The strategy for the analysis is to accumulate a set of outcomes while moving
forward through the program. At each step, every outcome in the current
summary must be sequenced with a summary for the next command using bi-
abduction. This is achieved using the seq procedure, defined in Figure 4,
which takes in an outcome assertion $\varphi$, a set of summaries for the next
command $C$, and $\vec{x}$, the variables modified by $C$. It computes a set
of missing anti-frames $M$ and postconditions $\psi$ such that
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\varphi\circledast
M\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\psi\rangle}$
is a valid specification for $C$.

$\displaystyle\mathsf{seq}(\eqmakebox[seqdef][c]{$\top$},S,\vec{x})=~{}$
$\displaystyle\\{(\mathsf{emp},\top)\\}$
$\displaystyle\mathsf{seq}(\eqmakebox[seqdef][c]{$\varphi_{1}\bowtie\varphi_{2}$},S,\vec{x})=~{}$
$\displaystyle\begin{array}[]{ll}\big{\\{}(M,\psi^{\prime}_{1}\bowtie\psi^{\prime}_{2})\mid{}&(M_{1},\psi_{1})\in\mathsf{seq}(\varphi_{1},S,\vec{x})\\\
&(M_{2},\psi_{2})\in\mathsf{seq}(\varphi_{2},S,\vec{x})\\\
&(M,\psi^{\prime}_{1},\psi^{\prime}_{2})\in\mathsf{triab}^{\prime}(M_{1},M_{2},\psi_{1},\psi_{2},\vec{x})\big{\\}}\end{array}$
$\displaystyle\mathsf{seq}(\eqmakebox[seqdef][c]{$\varphi^{(a)}$},S,\vec{x})=~{}$
$\displaystyle\\{(M,\psi^{(a)})\mid(M,\psi)\in\mathsf{seq}(\varphi,S,\vec{x})\\}$
$\displaystyle\mathsf{seq}(\eqmakebox[seqdef][c]{$\mathsf{ok}:P$},S,\vec{x})=~{}$
$\displaystyle\big{\\{}(M,\psi^{\prime})\mid(Q,\psi)\in
S,(M,\psi^{\prime})\in\mathsf{biab}^{\prime}(P,Q,\psi,\vec{x})\big{\\}}$
$\displaystyle\mathsf{seq}(\eqmakebox[seqdef][c]{$\mathsf{er}:Q$},S,\vec{x})=~{}$
$\displaystyle\\{(\mathsf{emp},\mathsf{er}:Q)\\}$

$\displaystyle\mathsf{biab}^{\prime}(\exists\vec{Z}.\Delta,Q,\psi,\vec{x})=$
$\displaystyle\quad\begin{array}[]{l}\big{\\{}(M^{\prime},(\psi\circledast\exists\vec{Z}\vec{X}.F[\vec{X}/\vec{x}])[\vec{e}/\vec{Y}])\\\
\mid(M,F)\in\mathsf{biab}(\Delta,Q)\\\
\quad(\vec{e},\vec{Y},M^{\prime})=\mathsf{rename}(\Delta,M,Q,\\{\psi\\},\vec{X},\vec{x})\big{\\}}\end{array}$
$\displaystyle\mathsf{triab}^{\prime}(P_{1},P_{2},\psi_{1},\psi_{2},\vec{x})=$
$\displaystyle\quad\begin{array}[]{l}\big{\\{}(M^{\prime},(\psi_{1}\circledast\exists\vec{X}.F_{1}[\vec{X}/\vec{x}])[\vec{e}/\vec{Y}],\\\
\phantom{\big{\\{}(M^{\prime},\,}(\psi_{2}\circledast\exists\vec{X}.F_{2}[\vec{X}/\vec{x}])[\vec{e}/\vec{Y}])\\\
~{}\mid(M,F_{1},F_{2})\in\mathsf{triab}(P_{1},P_{2})\\\
\quad(\vec{e},\vec{Y},M^{\prime})=\mathsf{rename}(\mathsf{emp},M,\\{\psi_{1},\psi_{2}\\},\emptyset,\vec{x})\big{\\}}\end{array}$

Figure 4. Sequencing procedure. The vector $\vec{X}$ is assumed to be fresh
and the same size as $\vec{x}$, and $\mathord{\bowtie}\in\\{\vee,\oplus\\}$.

Sequencing after $\top$ and $(\mathsf{er}:Q)$ has no effect, since $\top$
carries no information about the current branch, and $(\mathsf{er}:Q)$ means
the program has crashed. Sequencing after $\varphi^{(a)}$ simply sequences
$\varphi$ and then reapplies the weight. Sequential composition is implemented
in the $(\mathsf{ok}:P)$ case, where bi-abduction is used to reconcile the
current outcome with each summary for the next command. The
$\mathsf{biab}^{\prime}$ procedure is similar to AbduceAndAdapt from Calcagno
et al. (2011, Fig. 4), in which a renaming step is applied to ensure that the
anti-frame $M$ is not phrased in terms of any program variables, therefore
meeting the side condition of the frame rule. The details of renaming and why
it is required for correctness are explained in Appendix E.

Our algorithm differs from Abductor in the cases with multiple program
branches. This is where we use tri-abduction to obtain a precondition that is
guaranteed to be valid for all program paths, allowing us to analyze the
program in a single pass (unlike Abductor, which must re-evaluate the program
using each candidate precondition). After sequencing each of the outcomes in
the precondition $\varphi_{1}$ and $\varphi_{2}$ with the next command, we use
$\mathsf{triab}^{\prime}$ to obtain the single renamed anti-frame $M$ that is
safe for both branches. The soundness property for seq is stated below.

###### Lemma 5.3 (Seq).

If $(M,\psi)\in\mathsf{seq}(\varphi,S,\vec{x})$, $\vec{x}=\mathsf{mod}(C)$,
and
$\vDash{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\vartheta\rangle}$
for all $(P,\vartheta)\in S$, then
$\vDash{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\varphi\circledast
M\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\psi\rangle}$.

Symbolic Execution Algorithm. The core symbolic execution algorithm, shown in
Figure 5, computes a _local_ symbolic semantics which can be augmented using
the frame rule to obtain summaries in larger heaps. For example, the semantics
for $\mathsf{skip}$ is simply the triple
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:\mathsf{emp}\rangle}~{}\mathsf{skip}~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:\mathsf{emp}\rangle}$,
but this implies that running the program in any heap will yield that same
heap in the end. Executing $C_{1}\fatsemi C_{2}$ uses $\mathsf{seq}$;
summaries for $C_{1}$ are sequenced with all the summaries for $C_{2}$.
Choices $C_{1}+C_{2}$ are analyzed by computing summaries for each path and
reconciling them with tri-abduction.

We split $\mathsf{assume}~{}e$ into two cases: if $e$ is a simple test
(equality or inequality), then we generate two specifications with the
precondition stating that $e$ is true and the postcondition being unchanged,
or $e$ being false and the outcome being eliminated. This is similar to the
_“assume-as-assert”_ behavior of Abductor and produces precise specifications
without a priori knowledge of the logical conditions that will occur. If $e$
is a weight literal $a$, then we weight the current outcome by it. Other
expressions are not supported due to limitations of the bi-abduction solver of
Calcagno et al. (2009), which we also use. Similarly, while loops use a least
fixed point to unroll the loop, and produce one summary for each possible
number of iterations. We will see more options for analyzing loops later on.

The abstract semantics of atomic actions mostly follow the small axioms of
O’Hearn et al. (2001), with failure cases inspired by Incorrectness Separation
Logic (Raad et al., 2020). Each memory operation has three specifications: one
in which the pointer is allocated and the operation accordingly succeeds, and
two failure cases where the pointer is not allocated or null. Procedure calls
rely on pre-computed summaries in a lookup table $T$, which is a parameter to
$\left\llbracket C\right\rrbracket^{\sharp}$.

$\begin{array}[]{l|l}C\in\mathsf{Cmd}&\left\llbracket
C\right\rrbracket^{\sharp}(T)\\\
\hline\cr\hline\cr\mathsf{skip}&\\{(\mathsf{emp},\mathsf{ok}:\mathsf{emp})\\}\\\
C_{1}\fatsemi C_{2}&\\{(P\ast M,\psi)\mid(P,\varphi)\in\left\llbracket
C_{1}\right\rrbracket^{\sharp}(T),(M,\psi)\in\mathsf{seq}(\varphi,\left\llbracket
C_{2}\right\rrbracket^{\sharp}(T),\mathsf{mod}(C_{2}))\\}\\\
C_{1}+C_{2}&\begin{array}[]{ll}\\{(M,\psi^{\prime}_{1}\oplus\psi^{\prime}_{2})\mid&(M_{1},\psi_{1})\in\left\llbracket
C_{1}\right\rrbracket^{\sharp}(T),(M_{2},\psi_{2})\in\left\llbracket
C_{2}\right\rrbracket^{\sharp}(T),\\\
&(M,\psi^{\prime}_{1},\psi^{\prime}_{2})\in\mathsf{triab}^{\prime}(M_{1},M_{2},\psi_{1},\psi_{2},\mathsf{mod}(C_{1},C_{2}))\\}\end{array}\\\
\mathsf{assume}~{}b&\\{(b\land\mathsf{emp},\mathsf{ok}:b\land\mathsf{emp}),(\lnot
b\land\mathsf{emp},\top^{(\dsser{0})}\\}\\\
\mathsf{assume}~{}a&\\{(\mathsf{emp},(\mathsf{ok}:\mathsf{emp})^{(a)}\\}\\\
\mathsf{while}~{}b~{}\mathsf{do}~{}C&\begin{array}[]{ll}\mathsf{lfp}~{}S.&\\{(\lnot
b\land\mathsf{emp},\mathsf{ok}:\lnot b\land\mathsf{emp})\\}\mathop{\cup}\\\
&\\{(M_{1}\ast M_{2}\land b,\psi)\\\
&\mid(M_{1},\varphi)\in\mathsf{seq}(\mathsf{ok}:b\land\mathsf{emp},\left\llbracket
C\right\rrbracket^{\sharp}(T),\mathsf{mod}(C)),(M_{2},\psi)\in\mathsf{seq}(\varphi,S,\mathsf{mod}(C))\\}\end{array}\\\
\\\ c\in\mathsf{Act}&\left\llbracket c\right\rrbracket^{\sharp}(T)\\\
\hline\cr\hline\cr x\coloneqq
e&\\{(x=X\land\mathsf{emp},\mathsf{ok}:x=e[X/x]\land\mathsf{emp})\\}\\\
x\coloneqq\mathsf{alloc}()&\\{(x=X\land\mathsf{emp},\mathsf{ok}:\exists
Y.x\mapsto Y)\\}\\\ \mathsf{free}(e)&\\{(e\mapsto
X,\mathsf{ok}:e\not\mapsto),(e\not\mapsto,\mathsf{er}:e\not\mapsto),(\mathsf{emp}\land
e=\mathsf{null},\mathsf{er}:\mathsf{emp}\land e=\mathsf{null})\\}\\\
{[e_{1}]\leftarrow e_{2}}&\\{(e_{1}\mapsto X,\mathsf{ok}:e_{1}\mapsto
e_{2}),(e_{1}\not\mapsto,\mathsf{er}:e_{1}\not\mapsto),(\mathsf{emp}\land
e_{1}=\mathsf{null},\mathsf{er}:\mathsf{emp}\land e_{1}=\mathsf{null})\\}\\\
x\leftarrow[e]&\\{(x=X\\!\land\\!e\mapsto
Y,\mathsf{ok}:x=Y\\!\land\\!e[X/x]\mapsto
Y),\\!(e\not\mapsto,\mathsf{er}\\!:\\!e\not\mapsto),\\!(\mathsf{emp}\\!\land\\!e\\!=\\!\mathsf{null},\\!\mathsf{er}\\!:\\!\mathsf{emp}\\!\land\\!e\\!=\\!\mathsf{null})\\}\\\
\mathsf{error}()&\\{(\mathsf{emp},\mathsf{er}:\mathsf{emp})\\}\\\
f(\vec{e})&\\{(P\land\vec{x}=\vec{X},\varphi)\mid(P,\varphi)\in\mathsf{seq}(\mathsf{ok}:\vec{x}=\vec{e}[\vec{X}/\vec{x}]\land\mathsf{emp},T(f(\vec{x})),\mathsf{mod}(f))\\})\\}\end{array}$
Figure 5. Symbolic execution of commands and actions, all logical variables
$X,Y\in\mathsf{LVar}$ are assumed to be fresh, $a\in A$ is a program weight,
and $b\Coloneqq e_{1}=e_{2}\mid e_{1}\neq e_{2}$ is a simple test.

Simulating Pulse. As recounted by O’Hearn (2020); Raad et al. (2020); Le et
al. (2022), the scalability of IL-based analyses stems from their ability to
_drop disjuncts_. Analyzers such as Abductor accumulate a disjunction of
possible end states at each program point. For incorrectness, it is not
necessary to remember _all_ of these possible states; _any_ of them leading to
an error constitutes a bug. Since IL allows _strengthening_ of postconditions,
those disjuncts can be soundly dropped.

We take a slightly different view, which nonetheless enables us to drop
_paths_ in the same way. We differentiate between program choices that result
from logical conditions (_i.e.,_ if and while statements) vs computational
effects (_i.e.,_ nondeterministic or probabilistic choice). In the former
cases, we generate multiple summaries in order to precisely keep track of
which initial states will result in which outcomes. In the latter case, we use
an outcome conjunction rather than a disjunction to join the outcomes. While
we cannot drop outcomes per se, we can replace them by $\top$, ensuring that
they will not be explored any further according to the definition of seq
(Figure 4). This can be implemented by altering the definition of choice as
follows.

$\left\llbracket
C_{1}+C_{2}\right\rrbracket^{\sharp}(T)=\\{(P,\varphi\oplus\top)\mid(P,\varphi)\in\left\llbracket
C_{1}\right\rrbracket^{\sharp}(T)\\}\cup\\{(P,\varphi\oplus\top)\mid(P,\varphi)\in\left\llbracket
C_{2}\right\rrbracket^{\sharp}(T)\\}$

Given this modification, the algorithm remains sound with respect to the same
semantics (_i.e.,_ Theorem 5.2), but it no longer fits with the spirit of
correctness reasoning, since some of the program outcomes are left
unspecified. We will see in Section 6.1 how it can be used for efficient bug-
finding.

Now, we have a situation where each element of $\left\llbracket
C\right\rrbracket^{\sharp}(T)$ stands alone as a sound summary for the program
$C$, and represents a particular trace. This corresponds to taking a
particular logical branch in if statements, unfolding while loops for a fixed
number of iterations, and specific (nondeterministic or probabilistic)
choices. So, eliminating elements from the set will only preclude possible
summaries without affecting the correctness of the existing ones, meaning that
we can drop paths by, _e.g.,_ unrolling loops for a certain number of
iterations and only taking one path when encountering a $+$. Le et al. (2022)
refer to this as depth and width of the analysis, respectively.

Loop invariants and partial correctness. An alternative to bounded unrolling
for deterministic and non-deterministic programs (but not probabilistic ones)
is to use loop invariants. We achieve this by altering the rule for while
loops to the following.

$\left\llbracket\mathsf{while}~{}e~{}\mathsf{do}~{}C\right\rrbracket^{\sharp}(T)=\\{(I,(\mathsf{ok}:I\land\lnot
e)\vee\top^{(\dsser{0})}\mid(I\land e,\mathsf{ok}:I)\in\left\llbracket
C\right\rrbracket^{\sharp}(T)\\}$

The truth of the invariant $I$ is preserved by the loop body, therefore it
must remain true _if_ the loop exits. However, the invariant cannot guarantee
that the loop terminates, meaning that we lose the typical reachability
guarantees of outcome logic and must use a weaker _partial correctness_
specification. The possibility of nontermination is expressed by the
disjunction with $\top^{(\dsser{0})}$—either $I\land\lnot e$ holds, or the
program diverges and there are no outcomes. Since reachability cannot be
guaranteed, loop invariants are not suitable for true positive bug-finding, in
which errors must be witnessed by an actual trace.

Finding loop invariants is generally undecidable, however techniques from
abstract interpretation (Cousot and Cousot, 1977) can be used to find
invariants by framing the problem as a fixed point computation over a finite
domain, thereby guaranteeing convergence. This is the approach taken in
Abductor (Calcagno et al., 2011), which uses the same symbolic heaps, but
without outcome conjunctions. In nondeterministic programs, we can convert
outcome conjunctions into disjunctions since
$(\mathsf{ok}:P)\oplus(\mathsf{ok}:Q)\Rightarrow(\mathsf{ok}:P\vee Q)$. We
therefore speculate that we can use the same technique as Abductor, although
we leave a complete exploration of this idea to future work.

Nondeterministic Allocation. Memory bugs can arise in C from failing to check
whether the address returned by malloc is non-null. This is often modeled
using nondeterminism, wherein the semantics of malloc returns either a valid
pointer or null, nondeterministically. Our language is generic over effects,
so we do not have a nondeterministic malloc operation, but we can add
$x\coloneqq\mathsf{malloc}()$ as syntactic sugar for
$(x\coloneqq\mathsf{alloc}())+(x\coloneqq\mathsf{null})$, and derive the
following semantics:

$\left\llbracket
x\coloneqq\mathsf{malloc}()\right\rrbracket^{\sharp}(T)=\\{(x=X\land\mathsf{emp},(\mathsf{ok}:x=\mathsf{null}\land\mathsf{emp})\oplus(\mathsf{ok}:\exists
Y.x\mapsto Y))\\}$

Reusing Summaries. Though partial correctness specifications are incompatible
with bug-finding, and under-approximate specifications are incompatible with
verification, there is still overlap in summaries that can be used for both.
Many procedures in a given codebase do not include loops or branching, so
their summaries are equally valid for both correctness and incorrectness, and
also in programs with different interpretations of choice. In other cases,
when a procedure does have multiple outcomes, it is easy to convert a
correctness specification into several individual incorrectness ones, since
the following implication is sound. We will see this in action in Section 6.1.

${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\psi_{1}\oplus\psi_{2}\rangle}\qquad\implies\qquad{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\psi_{1}\oplus\top\rangle}\quad\text{and}\quad{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:P\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\psi_{2}\oplus\top\rangle}$

##  6\. Case Studies

We will now demonstrate how the symbolic execution algorithms work by
examining two case studies, which show the applicability in both
nondeterministic and probabilistic execution models.

###  6.1. Nondeterministic Vector Reallocation

Our first case study involves a common error in C++ when using the std::vector
library in which a call to push_back may reallocate the vector’s underlying
memory buffer, invalidating any pointers to that cell that existed before the
call. This was also used as a motivating example for Incorrectness Separation
Logic (Raad et al., 2020). Following their lead, we model the vector as a
single pointer and we treat reallocation as nondeterministic. The program is
shown below.

$\begin{array}[]{ll}\begin{array}[]{l}\textsf{main}():\\\ \quad
x\leftarrow[v]\fatsemi\\\ \quad\texttt{push\\_back}(v)\fatsemi\\\
\quad{[x]}\leftarrow
1\end{array}&\qquad\qquad\begin{array}[]{l}\textsf{push\\_back}(v):\\\ \hskip
10.00002pt\begin{array}[]{lll}\left(\begin{array}[]{l}y\leftarrow[v]\fatsemi\\\
\textsf{free}(y)\fatsemi\\\ y\coloneqq\textsf{alloc}()\fatsemi\\\
{[v]}\leftarrow
y\end{array}\right)&+&\mathsf{skip}\end{array}\end{array}\end{array}$

Before we analyze the main procedure, we must store
$\left\llbracket\mathsf{push\\_back}(v)\right\rrbracket^{\sharp}(T)$ in the
procedure table. Since push_back is a common library function, it makes sense
to compute summaries describing all the outcomes, which will be reusable for
both correctness and incorrectness analyses. The first step is to analyze the
two nondeterministic branches, which are both simple sequential programs.

$\displaystyle\small\left\llbracket\begin{array}[]{l}y\leftarrow[v]\fatsemi\\\
\textsf{free}(y)\fatsemi\\\ y\coloneqq\textsf{alloc}()\fatsemi\\\
{[v]}\leftarrow y\end{array}\right\rrbracket^{\sharp}\\!\\!\\!\\!(T)$
$\displaystyle=\left\\{\begin{array}[]{lll}(v\mapsto A\ast
A\mapsto-,{}&\mathsf{ok}:\exists B.v\mapsto B\ast B\mapsto-\ast
A\not\mapsto&)\\\ (v\mapsto A\ast A\not\mapsto,&\mathsf{er}:v\mapsto A\ast
A\not\mapsto&)\\\ (v\not\mapsto,&\mathsf{er}:v\not\mapsto&)\\\
&\cdots\end{array}\right\\}$
$\displaystyle\left\llbracket\mathsf{skip}\right\rrbracket^{\sharp}\\!(T)$
$\displaystyle=\large\\{(\mathsf{emp},\mathsf{ok}:\mathsf{emp})\large\\}$

Now, we can compose the two program branches using tri-abduction. Choosing the
first summary for the first branch, we get the following tri-abduction
solution.

$v\mapsto A\ast
A\mapsto-\ast[\mathsf{emp}]\mathrel{\mathchoice{\reflectbox{$\displaystyle\vDash$}}{\reflectbox{$\textstyle\vDash$}}{\reflectbox{$\scriptstyle\vDash$}}{\reflectbox{$\scriptscriptstyle\vDash$}}}[v\mapsto
A\ast A\mapsto-]\vDash\mathsf{emp}\ast[v\mapsto A\ast A\mapsto-]$

So, by framing $\mathsf{emp}$ into the first branch and $v\mapsto A\ast
A\mapsto-$ into the second branch, we get a summary for push_back as a whole.
This can similarly be done for the other summaries of the first branch,
yielding the lookup table below.

${\small\begin{array}[]{ll}T=\left\\{\begin{array}[]{lllclll}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:}&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}v\mapsto
A\ast
A\mapsto-}&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\rangle}&\mathsf{push\\_back}(v)&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{ok}:\exists
B.v\mapsto B\ast
B\mapsto-\ast{A\not\mapsto}}&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25})\oplus(\mathsf{ok}:v\mapsto
A\ast
A\mapsto-}&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25})\rangle}\\\
{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:}&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}v\mapsto
A\ast{A\not\mapsto}}&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\rangle}&\mathsf{push\\_back}(v)&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{er}:v\mapsto
A\ast{A\not\mapsto}}&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25})\oplus(\mathsf{ok}:v\mapsto
A\ast{A\not\mapsto}}&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25})\rangle}\\\
{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:}&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}{v\not\mapsto}}&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\rangle}&\mathsf{push\\_back}(v)&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{er}:{v\not\mapsto}}&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25})\oplus(\mathsf{ok}:{v\not\mapsto}}&{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25})\rangle}\\\
&&&\cdots\end{array}\right\\}\end{array}}$

The first summary tells us that push_back may reallocate the underlying
buffer, in which case the original pointer $A$ will become deallocated. The
next two summaries describe ways in which push_back itself can fail. We will
focus on using the first summary to show how main will fail if the buffer gets
reallocated. We analyze main in an under-approximate fashion in order to look
for bugs. The first step is to compute summaries for the first two commands of
main. The load on the first line has three summaries according to Figure 5, we
select the first one in which $v$ is allocated.

$\footnotesize{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:x=X\land
v\mapsto
Y\rangle}~{}x\leftarrow[v]~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:x=Y\land
v\mapsto Y\rangle}\in\left\llbracket
x\leftarrow[v]\right\rrbracket^{\sharp}(T)$

The procedure call on the second line requires us to look up summaries in $T$.
We select the first one, but we will use an under-approximate version of it so
as to explore only one of the paths

$\footnotesize{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:v\mapsto
A\ast
A\mapsto-\rangle}~{}\mathsf{push\\_back}(v)~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{ok}:\exists
B.v\mapsto B\ast B\mapsto-\ast{A\not\mapsto})\oplus\top\rangle}$

Now, we use seq to sequentially compose these summaries, which involves bi-
abducing the postcondition of $x\leftarrow[v]$ with the precondition of
$\mathsf{push\\_back}(v)$.

$x=Y\land v\mapsto Y\ast[A=Y\ast x\mapsto-]\vDash v\mapsto A\ast
A\mapsto-\ast[\mathsf{emp}]$

So, after renaming, we get the following summary for the composed program:

$\footnotesize{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:v\mapsto
x\ast
x\mapsto-\rangle}~{}x\leftarrow[v]\fatsemi\mathsf{push\\_back}(v)~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{ok}:\exists
B.v\mapsto B\ast B\mapsto-\ast{x\not\mapsto})\oplus\top\rangle}$

Now, observe that the postcondition above is only compatible with one of the
summaries in Figure 5 for the last line of the program. Since $x$ is
deallocated in the only specified outcome, the write into $x$ must fail. Using
bi-abduction again, we can construct the following description of the error.

$\footnotesize{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:v\mapsto
x\ast
x\mapsto-\rangle}~{}x\leftarrow[v]\fatsemi\mathsf{push\\_back}(v)\fatsemi[x]\leftarrow
1~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{er}:\exists
B.v\mapsto B\ast B\mapsto-\ast{x\not\mapsto})\oplus\top\rangle}$

###  6.2. Consensus in Distributed Computing

In this case study, we use OSL to lower bound reliability rates of a
distributed system. In the basic consensus algorithm, shown below, each of
three processes broadcasts a value $v_{i}$ by storing it in a pointer $p_{i}$,
and consensus is reached if any two of these processes broadcasted the same
value. To model unreliability of the network, the broadcast procedure fails
with probability 1%. We would like to know how likely we are to reach
consensus, given that two of the processes agree.

$\begin{array}[]{l}\mathsf{main}():\\\ \quad
p_{1}\coloneqq\mathsf{alloc}()\fatsemi\mathsf{broadcast}(v_{1},p_{1})\fatsemi\\\
\quad
p_{2}\coloneqq\mathsf{alloc}()\fatsemi\mathsf{broadcast}(v_{2},p_{2})\fatsemi\\\
\quad
p_{3}\coloneqq\mathsf{alloc}()\fatsemi\mathsf{broadcast}(v_{3},p_{3})\fatsemi\\\
\quad v\coloneqq\mathsf{alloc}()\fatsemi\\\
\quad\mathsf{decide}(p_{1},p_{2},p_{3},v)\\\ \\\ \mathsf{broadcast}(v,p):\\\
\quad\left([p]\leftarrow
v\right)\oplus_{0.99}\mathsf{error}()\end{array}\qquad\qquad\begin{array}[]{l}\mathsf{decide}(p_{1},p_{2},p_{3},v):\\\
\quad x_{1}\leftarrow[p_{1}]\fatsemi x_{2}\leftarrow[p_{2}]\fatsemi
x_{3}\leftarrow[p_{3}]\fatsemi\\\
\quad\mathsf{if}~{}x_{1}=x_{2}~{}\mathsf{then}\\\ \quad\quad[v]\leftarrow
x_{1}\\\ \quad\mathsf{else\ if}~{}x_{1}=x_{3}~{}\mathsf{then}\\\
\quad\quad[v]\leftarrow x_{1}\\\ \quad\mathsf{else\
if}~{}x_{2}=x_{3}~{}\mathsf{then}\\\ \quad\quad[v]\leftarrow x_{2}\\\
\quad\mathsf{else}~{}\mathsf{skip}\end{array}$

We begin by examining the summary table. The broadcast procedure has two
outcomes corresponding to whether or not the communication went through.
Though there are many summaries for decide, we show only the one in which the
values sent on $p_{1}$ and $p_{2}$ are equal.

$\small
T=\left\\{\begin{array}[]{c}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:p\mapsto-\land
v=V\rangle}~{}\mathsf{broadcast}(v,p)~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{ok}:p\mapsto
V\land v=V)\oplus_{0.99}(\mathsf{er}:p\mapsto-\land v=V)\rangle}\\\
{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:p_{1}\mapsto
V_{1}\ast p_{2}\mapsto V_{2}\ast p_{3}\mapsto V_{3}\ast v\mapsto-\land
V_{1}=V_{2}\rangle}~{}\mathsf{decide}(p_{1},p_{2},p_{3},v)~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:v\mapsto
V_{1}\ast\cdots\rangle}\\\ \cdots\end{array}\right\\}$

We again use the single-path algorithm to analyze main, but this time we are
interested only in the successfully terminating cases. We get the following
summaries for each of the first three lines.

${{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:v_{i}=V_{i}\rangle}~{}p_{i}\coloneqq\mathsf{alloc}()\fatsemi\mathsf{broadcast}(v_{i},p_{i})~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{ok}:v_{i}=V_{i}\land
p_{i}\mapsto V_{i})\oplus_{0.99}\top\rangle}}$

These three summaries can be combined—along with the simplification that
$(\varphi\oplus_{a}\top)\oplus_{b}\top$ implies $\varphi\oplus_{a\cdot
b}\top$—to obtain the following assertion just before the call to decide

$(\mathsf{ok}:v_{1}=V_{1}\land v_{2}=V_{2}\land v_{3}=V_{3}\land p_{1}\mapsto
V_{1}\ast p_{2}\mapsto V_{2}\ast p_{3}\mapsto V_{3})\oplus_{0.99^{3}}\top$

Now, we can bi-abduce the first outcome above with the precondition for decide
shown in $T$. This sends $V_{1}=V_{2}$ backwards into the precondition, and we
get an overall summary for main telling us that if $v_{1}=v_{2}$, then the
protocol will reach consensus ($v\mapsto V_{1}$) with probability _at least_
97%.

${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\mathsf{ok}:v_{1}=V_{1}\land
v_{2}=V_{2}\land v_{3}=V_{3}\land
V_{1}=V_{2}\rangle}~{}\mathsf{main}()~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle(\mathsf{ok}:v\mapsto
V_{1}\ast\cdots)\oplus_{0.9703}\top\rangle}$

##  7\. Related Work

Separation Logic and the Frame Rule. While many variants of separation logic
exist, OSL is the only one that supports alternative effects as well as both
may and must properties. The soundness of the frame rule in both partial and
total correctness separation logic relies on nondeterminism and _must_
properties (Yang and O’Hearn, 2002; Calcagno et al., 2007), so those logics
are suitable only for correctness in nondeterministic languages. Some work has
been done to drop the nondeterminism requirement, for example Baktiev (2006)
proved that the frame rule is sound in a deterministic language if heap
assertions are unaffected by address permutation, however this requires
languages without address arithmetic. Similarly, Tatsuta et al. (2009) created
a deterministic separation logic, but the frame rule only applies to programs
that do not allocate memory.

Incorrectness Separation Logic (ISL) has a frame rule that is compatible with
may properties, but not must properties (Raad et al., 2020). Unlike OSL, ISL
has no restrictions on assertions about memory allocation; it is possible to
prove that a particular address $\ell$ is returned. If, after applying the
frame rule, $\ell$ is already in use, then the postcondition of the ISL triple
becomes false, making the triple vacuous (whereas in regular separation logic
and OSL, a false _pre_ condition makes triples vacuous). However, whereas ISL
has slightly more power to express may properties, ISL cannot express must
(_i.e.,_ correctness) properties and is also specialized only to
nondeterminism.

Exact Separation Logic (ESL) (Maksimović et al., 2023) combines the semantics
of SL and ISL to create a logic that is suitable for both correctness and
incorrectness, while inheriting the limitations of both. That is, ESL can only
express properties that are _both_ may and must properties, meaning that it
cannot under-approximate by dropping paths or over-approximate using loop
invariants.

Higher-order separation logics (Birkedal and Yang, 2007; Birkedal et al.,
2008) including Iris (Jung et al., 2015) bake the frame rule into the
definition of the logic’s triples, making the proof of soundness of the frame
rule trivial without any additional assumptions. More precisely, triples
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{P\\}}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\\{Q\\}}$
are valid iff for any frame $F$, if $\sigma\vDash P\ast F$, then $\tau\vDash
Q\ast F$ for all $\tau\in\left\llbracket C\right\rrbracket(\sigma)$. As a
tradeoff, frame baking introduces additional proof obligations whenever
constructing a triple (_i.e.,_ it must be shown that every inference rule is
_frame preserving_). We could have used this approach in OSL, but there is no
free lunch; it would have involved moving the inductive cases of Lemma C.7
into Theorem 5.2.

We chose not to do this, as we preferred to keep the proof of the frame rule
self contained. The choice is mostly orthogonal to the power of the logic, and
somewhat philosophical: we proved that programs are local _actions_ whereas
the frame baking approach shows that you can only _express_ local properties
about commands. The exception to this is memory allocation, which is not a
local action, so we baked the expressivity limitation into the triple
semantics. We felt this was a good tradeoff, since we baked in a weaker
property, which was just strong enough to complete the proof.

In draft papers published after our work on Outcome Separation Logic,
Sufficient Incorrectness Logic (SIL) (Ascari et al., 2023) and Backwards
Under-Approximate triples (BUA) (Raad et al., 2023) provide frame rules for
triples based on _may_ properties. In both cases, the soundness result is a
bit weaker than our own (Theorem 4.6). That is, whereas we only require in the
premise that the triple
${\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\varphi\rangle}~{}C~{}{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}\langle\psi\rangle}$
is _semantically_ valid, Ascari et al. (2023); Raad et al. (2023) require that
it is _derivable_. While this trick allows them to avoid baking the allocation
restriction into the triple validity, it means that the soundness of the frame
rule depends on the other inference rules in the proof system—a property that
we wished to avoid. In addition, the inference rules for allocation in those
logics are not tight, meaning that the logics are incomplete. Adding a tighter
rule (with the ability to witness _which_ address was nondeterministically
chosen) would make the frame rule unsound, meaning that completeness of those
logics is incompatible with the frame rule.

Probabilistic Separation Logics. While some work has been done to incorporate
probabilistic reasoning into separation logic, these logics differ from OSL in
the scope and applicability of the frame rule, and have not been shown to be
compatible with bi-abduction. Quantitative Separation Logic (Batz et al.,
2019) and its concurrent counterpart (Fesefeldt et al., 2022) use weakest pre-
expectation (Morgan et al., 1996) style predicate transformers to derive
expected values in probabilistic pointer programs. They rely on demonic
nondeterminism for allocation—the expected value is lower bounded over all
possible allocated addresses—and the frame rule gives a lower bound, whereas
OSL is used for propositional reasoning, with each outcome having a
likelihood.

Polaris (Tassarotti and Harper, 2019) incorporates probabilistic reasoning
into Iris (Jung et al., 2015) and is also used to bound expected values using
refinements inspired by probabilistic relational Hoare Logic (Barthe et al.,
2015). Polaris is limited to programs that terminate in finitely many steps
and the program logic itself is only used to relate probabilistic programs to
each other, whereas the quantitative reasoning about expected values must be
done externally to the program logic.

Probabilistic Separation Logic (PSL) (Barthe et al., 2019) and subsequent
works (Bao et al., 2021, 2022; Li et al., 2023) use an alternative model of
separation to characterize probabilistic independence and related probability
theoretic properties. Doing so provides a compositional way to reason about
probabilistic programs, though this work is orthogonal to our own as it does
not deal with heaps.

Pulse and Incorrectness Separation Logic. As recounted by Raad et al. (2020,
§5), Pulse uses under-approximation in four ways in order to achieve
scalability:

  1. (1)

Pulse takes advantage of the IL semantics in order to explore only one path at
a time when the program execution branches, and to unroll loops for a bounded
number of iterations.

  2. (2)

Pulse elects to not consider cases in which memory is re-allocated.

  3. (3)

Pulse uses under-approximate specifications for some library functions.

  4. (4)

Pulse’s bi-abductive inference assumes that pointers are not aliased unless
explicitly stated.

We have shown how (1) is achieved using OSL in the single path algorithm, (2)
and (4) are standard assumptions in bi-abduction (Calcagno et al., 2009, 2011)
(which we also use), and (3) is a corollary to (1), since the ability to drop
paths opens the possibility for under-approximate procedure summaries.

Pulse does not support inductive predicates (_e.g.,_ list segments), so it
uses a simplified bi-abduction procedure capable of handling more types of
pure assertions. This results in _exact_ bi-abduction solutions; the inferred
$M$ and $F$ satisfy $P\ast
M\mathrel{\mathchoice{\reflectbox{$\displaystyle\vDash$}}{\reflectbox{$\textstyle\vDash$}}{\reflectbox{$\scriptstyle\vDash$}}{\reflectbox{$\scriptscriptstyle\vDash$}}}\vDash
Q\ast F$. As a result, Pulse does not use consequences to—since it is based on
IL—strengthen the postcondition, meaning that the resulting specs can be
interpreted as both ISL and OSL triples and that our algorithm from Section 5
does accurately model Pulse. This finding was later confirmed by Raad et al.
(2023).

Unified Metatheory with Effects. Our algebraic program semantics is similar to
Weighted Programming (Batz et al., 2022). Whereas we use an algebraic
interpretation of choice to represent multiple types of (executable) program
semantics, the goal of weighted programming is to specify mathematical models
and find solutions to optimization problems via static analysis. Cîrstea
(2013, 2014) also used partial semirings to represent properties of program
branching in coalgebraic logics.

Delaware et al. (2013a, b) developed 3MT, a unified framework in the Coq proof