From 13e12908a6012b174df15dffbcc075af18e174a6 Mon Sep 17 00:00:00 2001 From: Chris Fallin Date: Wed, 20 May 2020 14:10:56 -0700 Subject: [PATCH] MachBuffer branch opts: comments approximating a semi-formal correctness proof. --- cranelift/codegen/src/machinst/buffer.rs | 331 ++++++++++++++++++++++- 1 file changed, 319 insertions(+), 12 deletions(-) diff --git a/cranelift/codegen/src/machinst/buffer.rs b/cranelift/codegen/src/machinst/buffer.rs index 44fa53045b..03b4ab0750 100644 --- a/cranelift/codegen/src/machinst/buffer.rs +++ b/cranelift/codegen/src/machinst/buffer.rs @@ -105,6 +105,40 @@ //! (fixups happen at island emission time, at which point latest-branches are //! cleared, or at the end of emission), so we are sure to catch and redirect //! all possible paths to this instruction. +//! +//! # Branch-optimization Correctness +//! +//! The branch-optimization mechanism depends on a few data structures with +//! invariants, which are always held outside the scope of top-level public +//! methods: +//! +//! - The latest-branches list. Each entry describes a span of the buffer +//! (start/end offsets), the label target, the corresponding fixup-list entry +//! index, and the bytes (must be the same length) for the inverted form, if +//! conditional. The list of labels that are bound to the start-offset of this +//! branch is *complete* (if any label has a resolved offset equal to `start` +//! and is not an alias, it must appear in this list) and *precise* (no label +//! in this list can be bound to another offset). No label in this list should +//! be an alias. No two branch ranges can overlap, and branches are in +//! ascending-offset order. +//! +//! - The labels-at-tail list. This contains all MachLabels that have been bound +//! to (whose resolved offsets are equal to) the tail offset of the buffer. +//! No label in this list should be an alias. +//! +//! - The label_offsets array, containing the bound offset of a label or +//! UNKNOWN. No label can be bound at an offset greater than the current +//! buffer tail. +//! +//! - The label_aliases array, containing another label to which a label is +//! bound or UNKNOWN. A label's resolved offset is the resolved offset +//! of the label it is aliased to, if this is set. +//! +//! We argue below, at each method, how the invariants in these data structures +//! are maintained (grep for "Post-invariant"). +//! +//! Given these invariants, we argue why each optimization preserves execution +//! semantics below (grep for "Preserves execution semantics"). use crate::binemit::{Addend, CodeOffset, CodeSink, Reloc}; use crate::ir::{ExternalName, Opcode, SourceLoc, TrapCode}; @@ -175,6 +209,7 @@ pub struct MachBuffer { /// always describing the tail of the buffer, but we do not clear /// `labels_at_tail` eagerly when the tail grows, rather we lazily clear it /// when the offset has grown past this (`labels_at_tail_off`) point. + /// Always <= `cur_offset()`. labels_at_tail_off: CodeOffset, } @@ -240,6 +275,55 @@ impl MachBuffer { } } + /// Debug-only: check invariants of labels and branch-records described + /// under "Branch-optimization Correctness" above. + #[cfg(debug)] + fn check_label_branch_invariants(&self) { + let cur_off = self.cur_offset(); + // Check that every entry in latest_branches has *correct* + // labels_at_this_branch lists. We do not check completeness because + // that would require building a reverse index, which is too slow even + // for a debug invariant check. + let mut last_end = 0; + for b in &self.latest_branches { + debug_assert!(b.start < b.end); + debug_assert!(b.end <= cur_off); + debug_assert!(b.start >= last_end); + last_end = b.end; + for &l in &b.labels_at_this_branch { + debug_assert_eq!(self.resolve_label_offset(l), b.start); + debug_assert_eq!(self.label_aliases[l.0 as usize], UNKNOWN_LABEL); + } + } + + // Check that every label is unresolved, or resolved at or before + // cur_offset. If at cur_offset, must be in `labels_at_tail`. + for (i, &off) in self.label_offsets.iter().enumerate() { + let label = MachLabel(i as u32); + debug_assert!(off == UNKNOWN_LABEL_OFFSET || off <= cur_off); + if off == cur_off { + debug_assert!( + self.labels_at_tail_off == cur_off && self.labels_at_tail.contains(&label) + ); + } + } + + // Check that every label in `labels_at_tail_off` is precise, i.e., + // resolves to the cur offset. + debug_assert!(self.labels_at_tail_off <= cur_off); + if self.labels_at_tail_off == cur_off { + for &l in &self.labels_at_tail { + debug_assert_eq!(self.resolve_label_offset(l), cur_off); + debug_assert_eq!(self.label_aliases[l.0 as usize], UNKNOWN_LABEL); + } + } + } + + #[cfg(not(debug))] + fn check_label_branch_invariants(&self) { + // Nothing. + } + /// Current offset from start of buffer. pub fn cur_offset(&self) -> CodeOffset { self.data.len() as CodeOffset @@ -249,6 +333,15 @@ impl MachBuffer { pub fn put1(&mut self, value: u8) { trace!("MachBuffer: put byte @ {}: {:x}", self.cur_offset(), value); self.data.push(value); + + // Post-invariant: conceptual-labels_at_tail contains a complete and + // precise list of labels bound at `cur_offset()`. We have advanced + // `cur_offset()`, hence if it had been equal to `labels_at_tail_off` + // before, it is not anymore (and it cannot become equal, because + // `labels_at_tail_off` is always <= `cur_offset()`). Thus the list is + // conceptually empty (even though it is only lazily cleared). No labels + // can be bound at this new offset (by invariant on `label_offsets`). + // Hence the invariant holds. } /// Add 2 bytes. @@ -260,6 +353,8 @@ impl MachBuffer { ); let bytes = value.to_le_bytes(); self.data.extend_from_slice(&bytes[..]); + + // Post-invariant: as for `put1()`. } /// Add 4 bytes. @@ -271,6 +366,8 @@ impl MachBuffer { ); let bytes = value.to_le_bytes(); self.data.extend_from_slice(&bytes[..]); + + // Post-invariant: as for `put1()`. } /// Add 8 bytes. @@ -282,6 +379,8 @@ impl MachBuffer { ); let bytes = value.to_le_bytes(); self.data.extend_from_slice(&bytes[..]); + + // Post-invariant: as for `put1()`. } /// Add a slice of bytes. @@ -292,6 +391,8 @@ impl MachBuffer { data.len() ); self.data.extend_from_slice(data); + + // Post-invariant: as for `put1()`. } /// Reserve appended space and return a mutable slice referring to it. @@ -301,6 +402,8 @@ impl MachBuffer { let new_len = self.data.len() + len; self.data.resize(new_len, 0); &mut self.data[off..] + + // Post-invariant: as for `put1()`. } /// Align up to the given alignment. @@ -310,6 +413,8 @@ impl MachBuffer { while self.cur_offset() & (align_to - 1) != 0 { self.put1(0); } + + // Post-invariant: as for `put1()`. } /// Allocate a `Label` to refer to some offset. May not be bound to a fixed @@ -320,6 +425,9 @@ impl MachBuffer { self.label_aliases.push(UNKNOWN_LABEL); trace!("MachBuffer: new label -> {:?}", MachLabel(l)); MachLabel(l) + + // Post-invariant: the only mutation is to add a new label; it has no + // bound offset yet, so it trivially satisfies all invariants. } /// Reserve the first N MachLabels for blocks. @@ -329,20 +437,35 @@ impl MachBuffer { self.label_offsets .resize(blocks as usize, UNKNOWN_LABEL_OFFSET); self.label_aliases.resize(blocks as usize, UNKNOWN_LABEL); + + // Post-invariant: as for `get_label()`. } - /// Bind a label to the current offset. + /// Bind a label to the current offset. A label can only be bound once. pub fn bind_label(&mut self, label: MachLabel) { trace!( "MachBuffer: bind label {:?} at offset {}", label, self.cur_offset() ); + debug_assert_eq!(self.label_offsets[label.0 as usize], UNKNOWN_LABEL_OFFSET); + debug_assert_eq!(self.label_aliases[label.0 as usize], UNKNOWN_LABEL); let offset = self.cur_offset(); self.label_offsets[label.0 as usize] = offset; self.lazily_clear_labels_at_tail(); self.labels_at_tail.push(label); + + // Invariants hold: bound offset of label is <= cur_offset (in fact it + // is equal). If the `labels_at_tail` list was complete and precise + // before, it is still, because we have bound this label to the current + // offset and added it to the list (which contains all labels at the + // current offset). + + self.check_label_branch_invariants(); self.optimize_branches(); + + // Post-invariant: by `optimize_branches()` (see argument there). + self.check_label_branch_invariants(); } /// Lazily clear `labels_at_tail` if the tail offset has moved beyond the @@ -353,6 +476,11 @@ impl MachBuffer { self.labels_at_tail_off = offset; self.labels_at_tail.clear(); } + + // Post-invariant: either labels_at_tail_off was at cur_offset, and + // state is untouched, or was less than cur_offset, in which case the + // labels_at_tail list was conceptually empty, and is now actually + // empty. } /// Resolve a label to an offset, if known. May return `UNKNOWN_LABEL_OFFSET`. @@ -363,6 +491,8 @@ impl MachBuffer { } else { self.label_offsets[label.0 as usize] } + + // Post-invariant: no mutations. } /// Emit a reference to the given label with the given reference type (i.e., @@ -394,6 +524,9 @@ impl MachBuffer { if deadline < self.island_deadline { self.island_deadline = deadline; } + + // Post-invariant: no mutations to branches/labels data structures. + self.check_label_branch_invariants(); } /// Inform the buffer of an unconditional branch at the given offset, @@ -407,6 +540,9 @@ impl MachBuffer { /// - Call `use_label_at_offset()` to emit the fixup record. /// - Call `add_uncond_branch()` to make note of the branch. /// - Emit the bytes for the branch's machine code. + /// + /// Additional requirement: no labels may be bound between `start` and `end` + /// (exclusive on both ends). pub fn add_uncond_branch(&mut self, start: CodeOffset, end: CodeOffset, target: MachLabel) { assert!(self.cur_offset() == start); debug_assert!(end > start); @@ -421,11 +557,18 @@ impl MachBuffer { inverted: None, labels_at_this_branch: self.labels_at_tail.clone(), }); + + // Post-invariant: we asserted branch start is current tail; the list of + // labels at branch is cloned from list of labels at current tail. + self.check_label_branch_invariants(); } /// Inform the buffer of a conditional branch at the given offset, /// targetting the given label. May be used to optimize branches. /// The last added label-use must correspond to this branch. + /// + /// Additional requirement: no labels may be bound between `start` and `end` + /// (exclusive on both ends). pub fn add_cond_branch( &mut self, start: CodeOffset, @@ -436,6 +579,7 @@ impl MachBuffer { assert!(self.cur_offset() == start); debug_assert!(end > start); assert!(!self.fixup_records.is_empty()); + debug_assert!(inverted.len() == (end - start) as usize); let fixup = self.fixup_records.len() - 1; let inverted = Some(SmallVec::from(inverted)); self.lazily_clear_labels_at_tail(); @@ -447,30 +591,101 @@ impl MachBuffer { inverted, labels_at_this_branch: self.labels_at_tail.clone(), }); + + // Post-invariant: we asserted branch start is current tail; labels at + // branch list is cloned from list of labels at current tail. + self.check_label_branch_invariants(); } fn truncate_last_branch(&mut self) { self.lazily_clear_labels_at_tail(); + // Invariants hold at this point. + let b = self.latest_branches.pop().unwrap(); assert!(b.end == self.cur_offset()); + + // State: + // [PRE CODE] + // Offset b.start, b.labels_at_this_branch: + // [BRANCH CODE] + // cur_off, self.labels_at_tail --> + // (end of buffer) self.data.truncate(b.start as usize); self.fixup_records.truncate(b.fixup); + // State: + // [PRE CODE] + // cur_off, Offset b.start, b.labels_at_this_branch: + // (end of buffer) + // + // self.labels_at_tail --> (past end of buffer) let cur_off = self.cur_offset(); self.labels_at_tail_off = cur_off; + // State: + // [PRE CODE] + // cur_off, Offset b.start, b.labels_at_this_branch, + // self.labels_at_tail: + // (end of buffer) + // + // resolve_label_offset(l) for l in labels_at_tail: + // (past end of buffer) + trace!( "truncate_last_branch: truncated {:?}; off now {}", b, cur_off ); + + // Fix up resolved label offsets for labels at tail. for &l in &self.labels_at_tail { self.label_offsets[l.0 as usize] = cur_off; } + // Old labels_at_this_branch are now at cur_off. self.labels_at_tail .extend(b.labels_at_this_branch.into_iter()); + + // Post-invariant: this operation is defined to truncate the buffer, + // which moves cur_off backward, and to move labels at the end of the + // buffer back to the start-of-branch offset. + // + // latest_branches satisfies all invariants: + // - it has no branches past the end of the buffer (branches are in + // order, we removed the last one, and we truncated the buffer to just + // before the start of that branch) + // - no labels were moved to lower offsets than the (new) cur_off, so + // the labels_at_this_branch list for any other branch need not change. + // + // labels_at_tail satisfies all invariants: + // - all labels that were at the tail after the truncated branch are + // moved backward to just before the branch, which becomes the new tail; + // thus every element in the list should remain (ensured by `.extend()` + // above). + // - all labels that refer to the new tail, which is the start-offset of + // the truncated branch, must be present. The `labels_at_this_branch` + // list in the truncated branch's record is a complete and precise list + // of exactly these labels; we append these to labels_at_tail. + // - labels_at_tail_off is at cur_off after truncation occurs, so the + // list is valid (not to be lazily cleared). + // + // The stated operation was performed: + // - For each label at the end of the buffer prior to this method, it + // now resolves to the new (truncated) end of the buffer: it must have + // been in `labels_at_tail` (this list is precise and complete, and + // the tail was at the end of the truncated branch on entry), and we + // iterate over this list and set `label_offsets` to the new tail. + // None of these labels could have been an alias (by invariant), so + // `label_offsets` is authoritative for each. + // - No other labels will be past the end of the buffer, because of the + // requirement that no labels be bound to the middle of branch ranges + // (see comments to `add_{cond,uncond}_branch()`). + // - The buffer is truncated to just before the last branch, and the + // fixup record referring to that last branch is removed. + self.check_label_branch_invariants(); } fn optimize_branches(&mut self) { self.lazily_clear_labels_at_tail(); + // Invariants valid at this point. + trace!( "enter optimize_branches:\n b = {:?}\n l = {:?}\n f = {:?}", self.latest_branches, @@ -493,11 +708,18 @@ impl MachBuffer { break; } + // Invariant: we are looking at a branch that ends at the tail of + // the buffer. + // For any branch, conditional or unconditional: // - If the target is a label at the current offset, then remove // the conditional branch, and reset all labels that targetted // the current offset (end of branch) to the truncated // end-of-code. + // + // Preserves execution semantics: a branch to its own fallthrough + // address is equivalent to a no-op; in both cases, nextPC is the + // fallthrough. if self.resolve_label_offset(b.target) == cur_off { trace!("branch with target == cur off; truncating"); self.truncate_last_branch(); @@ -505,19 +727,79 @@ impl MachBuffer { } // If latest is an unconditional branch: - // - For each label at this point, make the label an alias of - // the branch target. We can now assume below that the - // unconditional branch is reachable only via fallthrough, and we - // are free to remove it in an optimization. + // + // - If the branch's target is not its own start address, then for + // each label at the start of branch, make the label an alias of the + // branch target, and remove the label from the "labels at this + // branch" list. + // + // - Preserves execution semantics: an unconditional branch's + // only effect is to set PC to a new PC; this change simply + // collapses one step in the step-semantics. + // + // - Post-invariant: the labels that were bound to the start of + // this branch become aliases, so they must not be present in any + // labels-at-this-branch list or the labels-at-tail list. The + // labels are removed form the latest-branch record's + // labels-at-this-branch list, and are never placed in the + // labels-at-tail list. Furthermore, it is correct that they are + // not in either list, because they are now aliases, and labels + // that are aliases remain aliases forever. + // // - If there is a prior unconditional branch that ends just before - // this one begins, then we can truncate this branch, because it is - // entirely unreachable (due to above). Do so and continue around - // the loop. + // this one begins, and this branch has no labels bound to its + // start, then we can truncate this branch, because it is entirely + // unreachable (we have redirected all labels that make it + // reachable otherwise). Do so and continue around the loop. + // + // - Preserves execution semantics: the branch is unreachable, + // because execution can only flow into an instruction from the + // prior instruction's fallthrough or from a branch bound to that + // instruction's start offset. Unconditional branches have no + // fallthrough, so if the prior instruction is an unconditional + // branch, no fallthrough entry can happen. The + // labels-at-this-branch list is complete (by invariant), so if it + // is empty, then the instruction is entirely unreachable. Thus, + // it can be removed. + // + // - Post-invariant: ensured by truncate_last_branch(). + // // - If there is a prior conditional branch whose target label // resolves to the current offset (branches around the // unconditional branch), then remove the unconditional branch, // and make the target of the unconditional the target of the // conditional instead. + // + // - Preserves execution semantics: previously we had: + // + // L1: + // cond_br L2 + // br L3 + // L2: + // (end of buffer) + // + // by removing the last branch, we have: + // + // L1: + // cond_br L2 + // L2: + // (end of buffer) + // + // we then fix up the records for the conditional branch to + // have: + // + // L1: + // cond_br.inverted L3 + // L2: + // + // In the original code, control flow reaches L2 when the + // conditional branch's predicate is true, and L3 otherwise. In + // the optimized code, the same is true. + // + // - Post-invariant: all edits to latest_branches and + // labels_at_tail are performed by `truncate_last_branch()`, + // which maintains the invariants at each step. + if b.is_uncond() { // Set any label equal to current branch's start as an alias of // the branch's target, if the target is not the branch itself @@ -554,10 +836,13 @@ impl MachBuffer { if self.latest_branches.len() > 1 { let prev_b = &self.latest_branches[self.latest_branches.len() - 2]; trace!(" -> more than one branch; prev_b = {:?}", prev_b); - // This uncond is immediately after another uncond; we've - // already redirected labels to this uncond away; so we can - // truncate this uncond. - if prev_b.is_uncond() && prev_b.end == b.start { + // This uncond is immediately after another uncond; we + // should have already redirected labels to this uncond away + // (but check to be sure); so we can truncate this uncond. + if prev_b.is_uncond() + && prev_b.end == b.start + && b.labels_at_this_branch.is_empty() + { trace!(" -> uncond follows another uncond; truncating"); self.truncate_last_branch(); continue; @@ -574,19 +859,33 @@ impl MachBuffer { && self.resolve_label_offset(prev_b.target) == cur_off { trace!(" -> uncond follows a conditional, and conditional's target resolves to current offset"); + // Save the target of the uncond (this becomes the + // target of the cond), and truncate the uncond. let target = b.target; let data = prev_b.inverted.clone().unwrap(); self.truncate_last_branch(); + + // Mutate the code and cond branch. + let off_before_edit = self.cur_offset(); let prev_b = self.latest_branches.last_mut().unwrap(); let not_inverted = SmallVec::from( &self.data[(prev_b.start as usize)..(prev_b.end as usize)], ); + + // Low-level edit: replaces bytes of branch with + // inverted form. cur_off remains the same afterward, so + // we do not need to modify label data structures. self.data.truncate(prev_b.start as usize); self.data.extend_from_slice(&data[..]); + + // Save the original code as the inversion of the + // inverted branch, in case we later edit this branch + // again. prev_b.inverted = Some(not_inverted); self.fixup_records[prev_b.fixup].label = target; trace!(" -> reassigning target of condbr to {:?}", target); prev_b.target = target; + debug_assert_eq!(off_before_edit, self.cur_offset()); continue; } } @@ -607,6 +906,10 @@ impl MachBuffer { } fn purge_latest_branches(&mut self) { + // All of our branch simplification rules work only if a branch ends at + // the tail of the buffer, with no following code; and branches are in + // order in latest_branches; so if the last entry ends prior to + // cur_offset, then clear all entries. let cur_off = self.cur_offset(); if let Some(l) = self.latest_branches.last() { if l.end < cur_off { @@ -614,6 +917,10 @@ impl MachBuffer { self.latest_branches.clear(); } } + + // Post-invariant: no invariant requires any branch to appear in + // `latest_branches`; it is always optional. The list-clear above thus + // preserves all semantics. } /// Emit a constant at some point in the future, binding the given label to