Trace Terminology

Table of Contents

Notation§1
Trace Semantics§2
Semantic Program Properties§3
1. Bounded Properties§3.1
Program Analyses§4

This is a short overview of the terminology we use in this class. We know that it is somewhat inconsistent between the lectures, but we hope to clean it up over time.

Notation §1

Before we get started, we need to introduce some basic notation. We use capital letters $I$ and $A$ to indicate sets, and small letters $a$ and $b$ to be elements of those sets.

We use small $p$ and $q$ to indicate programs.

Trace Semantics §2

A Transition System

A Transition system is a triplet $⟨ {𝐒 𝐭 𝐚 𝐭 𝐞}_{p}, δ_{p}, I_{p} ⟩$ where ${𝐒 𝐭 𝐚 𝐭 𝐞}_{p}$ is the set of program states, $δ_{p}$ is the transition relation (defined by the single step semantics) and $I_{p}$ are possible initial states.

A trace is now the sequences of states that a program traverse during execution.

Trace

The traces of a program $p$ is a sequence of states ${𝐓 𝐫 𝐚 𝐜 𝐞}_{p} \subseteq {𝐒 𝐭 𝐚 𝐭 𝐞}_{p}^{n}$ for $n \in [1, \infty]$ . We use $τ$ to refer to individual traces. We sometimes index the traces like so $τ_{i}$ , where $τ_{0}$ is the initial state.

We define the semantics a program to be the set of traces which we can generate from the transition system. This is also known as the Maximal Trace Semantics.

Maximal Trace Semantics

\begin{matrix} Sem & : 𝐏 𝐫 𝐨 𝐠 𝐫 𝐚 𝐦 \to 2^{𝐓 𝐫 𝐚 𝐜 𝐞} \\ Sem & (p) = {τ \in {𝐒 𝐭 𝐚 𝐭 𝐞}_{p}^{n} | \begin{matrix} n \in [1, \infty], \\ τ_{0} \in I_{p}, \\ \forall i \in [1, n - 1], δ_{p} (τ_{i - 1}, τ_{i}) \end{matrix}} \end{matrix}

Semantic Program Properties §3

Using the trace semantics, we can now talk about properties of programs. When the property is generic we use capital letters $Q$ and $R$ , but when we are talking about a concrete property we use $𝚘 𝚔$ okay or $𝚎 𝚛 𝚛$ error.

We differentiate between two kinds of properties, may-properties, and must-properties. A may property is true for one trace, while a must property is true for all traces.

May Property

A may-property is true for at least one trace in the program: $p ⊨^{𝗆 𝖺 𝗒} Q \equiv \exists τ \in Sem (p) . Q (τ)$

Must Property

A must-property is true for all traces in the program: $p ⊨^{𝗆 𝗎 𝗌 𝗍} Q \equiv \forall τ \in Sem (p) . Q (τ)$

Interestingly, if we negate the property of a may analysis we get a must analysis and visa-versa.

\begin{matrix} \neg (p ⊨^{𝗆 𝖺 𝗒} Q) & \equiv \neg \exists τ \in Sem (p) . Q (τ) \\ \equiv \forall τ \in Sem (p) . \neg Q (τ) & \equiv p ⊨^{𝗆 𝗎 𝗌 𝗍} \neg Q \end{matrix}

Bounded Properties §3.1

Sometimes we talk about properties which are bounded by some depth $k$ . In this world we only look at traces shorter than $k$ states.

Bounded Trace Semantics

\begin{matrix} {Sem}^{k} & : 𝐏 𝐫 𝐨 𝐠 𝐫 𝐚 𝐦 \to 2^{𝐓 𝐫 𝐚 𝐜 𝐞} \\ {Sem}^{k} & (p) = {τ \in {𝐒 𝐭 𝐚 𝐭 𝐞}_{p}^{n} | \begin{matrix} n \in [1, k], \\ τ_{0} \in I_{p}, \\ \forall i \in [1, n - 1], δ_{p} (τ_{i - 1}, τ_{i}) \end{matrix}} \end{matrix}

In this world, we can also talk about may and must properties $p, k ⊨^{𝗆 𝗎 𝗌 𝗍} Q$ and $p, k ⊨^{𝗆 𝖺 𝗒} Q$ . Which claims that $Q$ is true for one or all traces smaller than size $k$ in $p$ .

Program Analyses §4

Program analysis is an automatic procedure that attempts to determine a property about a program. Since an analysis $𝐀$ is tailor-made to predict a specific may property $Q$ , we write it like so $p ⊢_{𝐀}^{𝗆 𝖺 𝗒} Q$ , and we write a must property $Q$ as $p ⊢_{𝐀}^{𝗆 𝗎 𝗌 𝗍} Q$ .

Soundness and Completeness §4.1

Since program analysis is undecidable, it is in general impossible for an analysis to perfectly match the true property of the code; therefore, we approximate it.

A common confusion in program analysis is that static analyses accept or reject properties over programs, where dynamic analyses accept and reject properties over traces.

This has consequences over what they consider sound and complete.

A sound analysis is never wrong:

Soundness

In a sound system, every proved fact is a true fact. Any property found by a sound analysis is true.

\begin{matrix} p ⊢_{𝐀}^{𝗆 𝗎 𝗌 𝗍} Q ⟹ p ⊨^{𝗆 𝗎 𝗌 𝗍} Q \\ p ⊢_{𝐀}^{𝗆 𝗎 𝗌 𝗍} Q ⟹ p ⊨^{𝗆 𝖺 𝗒} Q \end{matrix}

A static analysis focuses on properties over all traces: must properties. So when we say a static analysis is sound, it is must sound. A dynamic analysis focuses on properties over some traces, may properties, so when we say it is sound it is may sound.

When we use the notation $p ⊢_{𝐀}^{𝗆 𝗎 𝗌 𝗍} Q$ or $p ⊢_{𝐀}^{𝗆 𝖺 𝗒} Q$ you can assume that they imply $p ⊨^{𝗆 𝗎 𝗌 𝗍} Q$ and $p ⊨^{𝗆 𝖺 𝗒} Q$ respectively.

If a may analysis finds that a program raises a null-pointer exception for some trace, then there exist a trace that raises a null-pointer exception.

If a must analysis finds that the program must raise a null-pointer exception, then the program will raise a null-pointer exception on all traces.

The other side of the coin is completeness. A complete analysis never misses a property. To clearly differentiate the sound analyses from the complete ones, we use not-must and not-may instead, to indicate that the analysis tries to under approximate a property.

Completeness

In a complete system, every true fact can be proved. All false properties can be rejected by a complete analysis.

\begin{matrix} p ⊨^{𝗆 𝖺 𝗒} Q ⟹ p ⊢_{𝐀}^{\neg 𝗆 𝖺 𝗒} Q \\ p ⊨^{𝗆 𝗎 𝗌 𝗍} Q ⟹ p ⊢_{𝐀}^{\neg 𝗆 𝗎 𝗌 𝗍} Q \end{matrix}

When we use the notation $p ⊢_{𝐀}^{\neg 𝗆 𝗎 𝗌 𝗍} Q$ or $p ⊢_{𝐀}^{\neg 𝗆 𝖺 𝗒} Q$ you can assume that they are implied by $p ⊨^{𝗆 𝗎 𝗌 𝗍} Q$ and $p ⊨^{𝗆 𝖺 𝗒} Q$ respectively.

If a program raise a null-pointer exception for any trace, a not-may analysis will find the that the program can raise a null-pointer exception on some trace.

If a program raise a null-pointer exception on all traces (must), a not-must analysis will find the program raises null-pointer exception on all traces.

An analysis can be sound or complete, but never both.

Duality of Analyses §4.2

Recall that it is generally true that a may property is an inverted must property:

\neg (p ⊨^{𝗆 𝖺 𝗒} Q) \equiv p ⊨^{𝗆 𝗎 𝗌 𝗍} \neg Q

This is also the case for program analyses, any complete may analysis can be made into a sound must analysis over the negated property:

\neg (p ⊢_{𝐀}^{\neg 𝗆 𝖺 𝗒} Q) \equiv p ⊢_{𝐀}^{𝗆 𝗎 𝗌 𝗍} \neg Q

We can see this quite clearly. If take the completeness requirement, and flip the implication by negating on both sides:

\begin{matrix} p ⊨^{𝗆 𝖺 𝗒} Q & ⟹ p ⊢_{𝐀}^{\neg 𝗆 𝖺 𝗒} Q \\ \neg (p ⊨^{𝗆 𝖺 𝗒} Q) & ⟸ \neg (p ⊢_{𝐀}^{\neg 𝗆 𝖺 𝗒} Q) \end{matrix}

Now by using the rule above we see that $\neg (p ⊢_{𝐀}^{\neg 𝗆 𝖺 𝗒} Q)$ implies $p ⊨^{𝗆 𝗎 𝗌 𝗍} \neg Q$ , which means that $\neg (p ⊢_{𝐀}^{\neg 𝗆 𝖺 𝗒} Q)$ is a sound must analysis.

Warnings vs Positives §4.3

It is common to use the terminology of false/true positives/negatives, when referring to a classifier. However, this is confusing when referring to program analysis as it unclear if we are referring to classification over programs (must analyses and not-may analyses) or classification over traces (may analyses and not-must analyses).

To clear up this confusion, we use warnings to refer to specific bugs reported in the program, essentially classification over traces.

A sound static analysis might produce false warnings, where a sound dynamic analysis will never produce false warnings.

Bounded Analyses §4.4

Like with our semantics we can bound our analyses, for example we can write $⊢_{𝐀}^{𝗆 𝗎 𝗌 𝗍 / k}$ , and $⊢_{𝐀}^{𝗆 𝖺 𝗒 / k}$ .

However, generally a bounded must analysis is not a must analysis,

\begin{matrix} p, k ⊢_{𝐀}^{𝗆 𝗎 𝗌 𝗍} Q & ⟹̸ p ⊢_{𝐀}^{𝗆 𝗎 𝗌 𝗍} Q \\ because \\ p, k ⊨^{𝗆 𝗎 𝗌 𝗍} Q & ⟹̸ p ⊨^{𝗆 𝗎 𝗌 𝗍} Q \end{matrix}

and a bounded not-may analysis is not a not-may analysis:

\begin{matrix} p, k ⊢_{𝐀}^{\neg 𝗆 𝖺 𝗒} Q & ⟸̸ p ⊢_{𝐐}^{\neg 𝗆 𝖺 𝗒} \\ because \\ p, k ⊨^{𝗆 𝖺 𝗒} Q & ⟸̸ p ⊨^{𝗆 𝖺 𝗒} Q \end{matrix}