appendix sectionrules

Symbolic execution and information-flow rules

SymImp-DL

Concrete configurations contain a command, store, fixed input oracle, and cursor. Besides the congruence rules for sequence, the rules are $\frac{}{⟨ input x, s, I, n ⟩ ⟶_{c} ⟨ skip, s [x \mapsto I (n)], I, n + 1 ⟩} C - Input$ $\frac{}{⟨ x := a, s, I, n ⟩ ⟶_{c} ⟨ skip, s [x \mapsto [[a {]]}_{s}], I, n ⟩} C - Assign$ $\frac{[[g {]]}_{s} = true}{⟨ if g then c_{1} else c_{2}, s, I, n ⟩ ⟶_{c} ⟨ c_{1}, s, I, n ⟩} C - If - T$ $\frac{[[g {]]}_{s} = false}{⟨ if g then c_{1} else c_{2}, s, I, n ⟩ ⟶_{c} ⟨ c_{2}, s, I, n ⟩} C - If - F .$ $\frac{[[g {]]}_{s} = true}{⟨ assert g, s, I, n ⟩ ⟶_{c} ⟨ skip, s, I, n ⟩} C - Assert - T$ $\frac{[[g {]]}_{s} = false}{⟨ assert g, s, I, n ⟩ ⟶_{c} fail (s, I, n)} C - Assert - F .$ Put $unroll (g, c) = if g then (c; while g do c) else skip$ . Then $\frac{}{⟨ while g do c, s, I, n ⟩ ⟶_{c} ⟨ unroll (g, c), s, I, n ⟩} C - While$ $\frac{⟨ c_{1}, s, I, n ⟩ ⟶_{c} ⟨ c_{1}^{'}, s^{'}, I, n^{'} ⟩}{⟨ c_{1}; c_{2}, s, I, n ⟩ ⟶_{c} ⟨ c_{1}^{'}; c_{2}, s^{'}, I, n^{'} ⟩} C - Seq - Step$ $\frac{}{⟨ skip; c, s, I, n ⟩ ⟶_{c} ⟨ c, s, I, n ⟩} C - Seq - Skip .$ Failure propagates through a surrounding sequence. The symbolic input, assignment, and branch rules are

⟨ input x, σ, Φ, n ⟩ ⟶_{s} ⟨ skip, σ [x \mapsto α_{n}], Φ, n + 1 ⟩

S-Input

⟨ x := a, σ, Φ, n ⟩ ⟶_{s} ⟨ skip, σ [x \mapsto [[a {]]}_{σ}], Φ, n ⟩

S-Assign

⟨ if g then c_{1} else c_{2}, σ, Φ, n ⟩ ⟶_{s} ⟨ c_{1}, σ, Φ \land [[g {]]}_{σ}, n ⟩

S-If-T

⟨ if g then c_{1} else c_{2}, σ, Φ, n ⟩ ⟶_{s} ⟨ c_{2}, σ, Φ \land \neg [[g {]]}_{σ}, n ⟩

S-If-F

Symbolic conditionals fork and conjoin $[g]_{σ}$ or its integer complement; assertions fork into skip and a failure obligation; while unfolds exactly as C-While and then uses those conditional forks. Symbolic sequencing mirrors C-Seq-Step and C-Seq-Skip. No symbolic rule contains a satisfiability premise.

The graph representation maps $u - v \leq k$ to $v \overset{k}{\to} u$ . A checked negative-cycle certificate verifies that every selected edge occurs in the path condition, endpoints compose and close, and the weight sum is strictly negative. Models are accepted only after every atom and deterministic replay are checked; unknown retains the path.

Imperative information flow

Expressions have the join of the labels of their free variables. Commands use the program-counter judgment $Γ ⊢_{p}^{IF} c$ . Its assignment, sequence, branch, and loop rules are

Γ ⊢ e : ℓ

p ⊔ ℓ ⊑_{\sec} Γ (x)

Γ ⊢_{p}^{IF} x := e

IF-Assign

Γ ⊢_{p}^{IF} c_{1}

Γ ⊢_{p}^{IF} c_{2}

Γ ⊢_{p}^{IF} c_{1}; c_{2}

IF-Seq

Γ ⊢ b : ℓ

Γ ⊢_{p ⊔ ℓ}^{IF} c_{1}

Γ ⊢_{p ⊔ ℓ}^{IF} c_{2}

Γ ⊢_{p}^{IF} if b then c_{1} else c_{2}

IF-If

Γ ⊢ b : ℓ

Γ ⊢_{p ⊔ ℓ}^{IF} c

Γ ⊢_{p}^{IF} while b do c

IF-While

Skip is always admissible. The terminating evaluation rules are $\frac{}{⟨ skip, s ⟩ ⇓_{IF} s} E - Skip$ $\frac{}{⟨ x := e, s ⟩ ⇓_{IF} s [x \mapsto [[e {]]}_{s}]} E - Assign$ $\frac{\begin{matrix} ⟨ c_{1}, s ⟩ ⇓_{IF} s_{1} \\ ⟨ c_{2}, s_{1} ⟩ ⇓_{IF} s_{2} \end{matrix}}{⟨ c_{1}; c_{2}, s ⟩ ⇓_{IF} s_{2}} E - Seq$ $\frac{\begin{matrix} [[b {]]}_{s} = true \\ ⟨ c_{1}, s ⟩ ⇓_{IF} s^{'} \end{matrix}}{⟨ if b then c_{1} else c_{2}, s ⟩ ⇓_{IF} s^{'}} E - If - T$ $\frac{\begin{matrix} [[b {]]}_{s} = false \\ ⟨ c_{2}, s ⟩ ⇓_{IF} s^{'} \end{matrix}}{⟨ if b then c_{1} else c_{2}, s ⟩ ⇓_{IF} s^{'}} E - If - F .$ For $w = while b do c$ , the two loop rules are $\frac{[[b {]]}_{s} = false}{⟨ w, s ⟩ ⇓_{IF} s} E - While - F$ $\frac{\begin{matrix} [[b {]]}_{s} = true \\ ⟨ c, s ⟩ ⇓_{IF} s_{1} \\ ⟨ w, s_{1} ⟩ ⇓_{IF} s_{2} \end{matrix}}{⟨ w, s ⟩ ⇓_{IF} s_{2}} E - While - T .$ TINI quantifies over two derivations of this relation. It makes no conclusion when either derivation is absent.

Delete the input oracle and cursor from C-Assign, C-If-T, and C-If-F to obtain the assignment and branch rules of $⟶_{IF}$ . Its sequence rules arise from C-Seq-Step and C-Seq-Skip; its loop rule arises from C-While. Those are all its rules; it has no input, assertion, or failure state.