Compiler Optimization: Common Branch Factorization (NuSMV, w/loops)

Description of the Case Study

We study compiler optimization as preservation of input–output behaviors between a source program and an optimized target program. The case focuses on common branch factorization (CBF): finding guards common to several if–then–else branches and hoisting them so the test is executed only once. While CBF reduces control complexity, it must not change observable behavior.

Conformance between source (big) and target (small) executions falls into the \(\forall_{\text{big}}\,\exists_{\text{small}}\) category: for every source run there should exist a target run that matches the source’s observations. In our framework we avoid translating proofs and instead search for a SIMAE simulation that satisfies a conformance formula \(\varphi_{\mathrm{sc}}\).

We consider two targets:

• a correct optimization (expected SAT—a SIMAE witness exists), and

• a buggy optimization where some branches become unreachable (expected UNSAT).

The NuSMV model(s)

Source (big)Target (small) — correctTarget (small) — buggy

MODULE main
VAR
  s : 0..14;

ASSIGN
  init(s) := 0;

  next(s) :=
    case
      -- entry branches
      s = 0  : {1, 3, 5, 7, 9, 11, 13};

      -- each branch: guard/state then terminal self-loop
      s = 1  : 2;
      s = 2  : 2;

      s = 3  : 4;
      s = 4  : 4;

      s = 5  : 6;
      s = 6  : 6;

      s = 7  : 8;
      s = 8  : 8;

      s = 9  : 10;
      s = 10 : 10;

      s = 11 : 12;
      s = 12 : 12;

      s = 13 : 14;
      s = 14 : 14;

      TRUE   : s; -- totalize
    esac;

The HyperLTL formula(s)

We require that whenever the source and target agree on inputs, their observable outputs agree at all steps. With traces \(\pi_{\text{big}}\) (source) and \(\pi_{\text{small}}\) (target):

\[\begin{aligned} \varphi_{\mathrm{sc}} \;=\; \forall \pi_{\text{big}}.\ \exists \pi_{\text{small}}.\ \big( \mathit{in}_{\pi_{\text{big}}} \leftrightarrow \mathit{in}_{\pi_{\text{small}}} \big) \ \rightarrow\ \mathbf{G}\big( \mathit{out}_{\pi_{\text{big}}} \leftrightarrow \mathit{out}_{\pi_{\text{small}}} \big). \end{aligned}\]

Formula

Forall A . Exists B . G(((s[A] = 0) -> (s[B] = 0)) & (((s[A] = 1) | (s[A] = 3) | (s[A] = 5) | (s[A] = 7) | (s[A] = 9) | (s[A] = 11) | (s[A] = 13)) -> (s[B] = 1)) & ((s[A] = 2) -> (s[B] = 2)) & ((s[A] = 4) -> (s[B] = 3)) & ((s[A] = 6) -> (s[B] = 4)) & ((s[A] = 8) -> (s[B] = 5)) & ((s[A] = 10) -> (s[B] = 6)) & ((s[A] = 12) -> (s[B] = 7)) & ((s[A] = 14) -> (s[B] = 8)))

References

Namjoshi, Kedar S.; Tabajara, Lucas M. “Witnessing secure compilation.” In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2020), pp. 1–22. Springer, 2020.