Skip to content

PCC: remove proof-carrying code (for now?). #12800

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
cfallin wants to merge 1 commit into
base: main
Choose a base branch
from
+632 −7,038
Open

PCC: remove proof-carrying code (for now?). #12800

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 0 additions & 14 deletions cranelift/codegen/meta/src/shared/settings.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,20 +77,6 @@ pub(crate) fn define() -> SettingGroup {
true,
);

settings.add_bool(
"enable_pcc",
"Enable proof-carrying code translation validation.",
r#"
This adds a proof-carrying-code mode. Proof-carrying code (PCC) is a strategy to verify
that the compiler preserves certain properties or invariants in the compiled code.
For example, a frontend that translates WebAssembly to CLIF can embed PCC facts in
the CLIF, and Cranelift will verify that the final machine code satisfies the stated
facts at each intermediate computed value. Loads and stores can be marked as "checked"
and their memory effects can be verified as safe.
"#,
false,
);

// Note that Cranelift doesn't currently need an is_pie flag, because PIE is
// just PIC where symbols can't be pre-empted, which can be expressed with the
// `colocated` flag on external functions and global values.
Expand Down
1 change: 0 additions & 1 deletion cranelift/codegen/src/context.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -381,7 +381,6 @@ impl Context {
&self.domtree,
&self.loop_analysis,
&mut alias_analysis,
&fisa.flags,
ctrl_plane,
);
pass.run();
Expand Down
33 changes: 1 addition & 32 deletions cranelift/codegen/src/egraph/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,13 @@ use crate::cursor::{Cursor, CursorPosition, FuncCursor};
use crate::dominator_tree::DominatorTree;
use crate::egraph::elaborate::Elaborator;
use crate::inst_predicates::{is_mergeable_for_egraph, is_pure_for_egraph};
use crate::ir::pcc::Fact;
use crate::ir::{
Block, DataFlowGraph, Function, Inst, InstructionData, Opcode, Type, Value, ValueDef,
ValueListPool,
Block, DataFlowGraph, Function, Inst, InstructionData, Type, Value, ValueDef, ValueListPool,
};
use crate::loop_analysis::LoopAnalysis;
use crate::opts::IsleContext;
use crate::opts::generated_code::SkeletonInstSimplification;
use crate::scoped_hash_map::{Entry as ScopedEntry, ScopedHashMap};
use crate::settings::Flags;
use crate::take_and_replace::TakeAndReplace;
use crate::trace;
use alloc::vec::Vec;
Expand Down Expand Up @@ -60,8 +57,6 @@ pub struct EgraphPass<'a> {
/// Loop analysis results, used for built-in LICM during
/// elaboration.
loop_analysis: &'a LoopAnalysis,
/// Compiler flags.
flags: &'a Flags,
/// Chaos-mode control-plane so we can test that we still get
/// correct results when our heuristics make bad decisions.
ctrl_plane: &'a mut ControlPlane,
Expand Down Expand Up @@ -95,7 +90,6 @@ where
domtree: &'opt DominatorTree,
pub(crate) alias_analysis: &'opt mut AliasAnalysis<'analysis>,
pub(crate) alias_analysis_state: &'opt mut LastStores,
flags: &'opt Flags,
ctrl_plane: &'opt mut ControlPlane,
// Held locally during optimization of one node (recursively):
pub(crate) rewrite_depth: usize,
Expand Down Expand Up @@ -170,7 +164,6 @@ where
let result = self.func.dfg.first_result(inst);
self.value_to_opt_value[result] = orig_result;
self.available_block[result] = self.available_block[orig_result];
self.func.dfg.merge_facts(result, orig_result);
}
orig_result
} else {
Expand All @@ -194,8 +187,6 @@ where
}
};

self.attach_constant_fact(inst, result, ty);

self.available_block[result] = self.get_available_block(inst);
let opt_value = self.optimize_pure_enode(inst);
log::trace!("optimizing inst {inst} orig result {result} gave {opt_value}");
Expand Down Expand Up @@ -387,7 +378,6 @@ where
ctx.eclass_size[union_value] = eclass_size - 1;
ctx.stats.union += 1;
trace!(" -> union: now {}", union_value);
ctx.func.dfg.merge_facts(old_union_value, optimized_value);
ctx.available_block[union_value] =
ctx.merge_availability(old_union_value, optimized_value);
}
Expand Down Expand Up @@ -503,7 +493,6 @@ where
);
self.value_to_opt_value[result] = new_result;
self.available_block[result] = self.available_block[new_result];
self.func.dfg.merge_facts(result, new_result);
Some(SkeletonInstSimplification::Remove)
}
// Otherwise, generic side-effecting op -- always keep it, and
Expand Down Expand Up @@ -695,23 +684,6 @@ where
// Return the best simplification!
best
}

/// Helper to propagate facts on constant values: if PCC is
/// enabled, then unconditionally add a fact attesting to the
/// Value's concrete value.
fn attach_constant_fact(&mut self, inst: Inst, value: Value, ty: Type) {
if self.flags.enable_pcc() {
if let InstructionData::UnaryImm {
opcode: Opcode::Iconst,
imm,
} = self.func.dfg.insts[inst]
{
let imm: i64 = imm.into();
self.func.dfg.facts[value] =
Some(Fact::constant(ty.bits().try_into().unwrap(), imm as u64));
}
}
}
}

impl<'a> EgraphPass<'a> {
Expand All @@ -721,15 +693,13 @@ impl<'a> EgraphPass<'a> {
domtree: &'a DominatorTree,
loop_analysis: &'a LoopAnalysis,
alias_analysis: &'a mut AliasAnalysis<'a>,
flags: &'a Flags,
ctrl_plane: &'a mut ControlPlane,
) -> Self {
Self {
func,
domtree,
loop_analysis,
alias_analysis,
flags,
ctrl_plane,
stats: Stats::default(),
remat_values: FxHashSet::default(),
Expand Down Expand Up @@ -897,7 +867,6 @@ impl<'a> EgraphPass<'a> {
domtree: &self.domtree,
alias_analysis: self.alias_analysis,
alias_analysis_state: &mut alias_analysis_state,
flags: self.flags,
ctrl_plane: self.ctrl_plane,
optimized_values: Default::default(),
optimized_insts: Default::default(),
Expand Down
61 changes: 1 addition & 60 deletions cranelift/codegen/src/ir/dfg.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ use crate::ir;
use crate::ir::builder::ReplaceBuilder;
use crate::ir::dynamic_type::{DynamicTypeData, DynamicTypes};
use crate::ir::instructions::{CallInfo, InstructionData};
use crate::ir::pcc::Fact;
use crate::ir::user_stack_maps::{UserStackMapEntry, UserStackMapEntryVec};
use crate::ir::{
Block, BlockArg, BlockCall, ConstantData, ConstantPool, DynamicType, ExceptionTables,
Expand Down Expand Up @@ -144,9 +143,6 @@ pub struct DataFlowGraph {
/// Primary value table with entries for all values.
values: PrimaryMap<Value, ValueDataPacked>,

/// Facts: proof-carrying-code assertions about values.
pub facts: SecondaryMap<Value, Option<Fact>>,

/// Function signature table. These signatures are referenced by indirect call instructions as
/// well as the external function references.
pub signatures: PrimaryMap<SigRef, Signature>,
Expand Down Expand Up @@ -181,7 +177,6 @@ impl DataFlowGraph {
dynamic_types: DynamicTypes::new(),
value_lists: ValueListPool::new(),
values: PrimaryMap::new(),
facts: SecondaryMap::new(),
signatures: PrimaryMap::new(),
ext_funcs: PrimaryMap::new(),
values_labels: None,
Expand All @@ -207,7 +202,6 @@ impl DataFlowGraph {
self.constants.clear();
self.immediates.clear();
self.jump_tables.clear();
self.facts.clear();
}

/// Get the total number of instructions created in this function, whether they are currently
Expand Down Expand Up @@ -489,21 +483,6 @@ impl DataFlowGraph {
// removed), and unions (but the egraph pass ensures there are no
// aliases before creating unions).

// Merge `facts` from any alias onto the aliased value. Note that if
// there was a chain of aliases, at this point every alias that was in
// the chain points to the same final value, so their facts will all be
// merged together.
for value in self.facts.keys() {
if let ValueData::Alias { original, .. } = self.values[value].into() {
if let Some(new_fact) = self.facts[value].take() {
match &mut self.facts[original] {
Some(old_fact) => *old_fact = Fact::intersect(old_fact, &new_fact),
old_fact => *old_fact = Some(new_fact),
}
}
}
}

// - `signatures` and `ext_funcs` have no values.

if let Some(values_labels) = &mut self.values_labels {
Expand Down Expand Up @@ -1075,13 +1054,7 @@ impl DataFlowGraph {
// Get the controlling type variable.
let ctrl_typevar = self.ctrl_typevar(inst);
// Create new result values.
let num_results = self.make_inst_results(new_inst, ctrl_typevar);
// Copy over PCC facts, if any.
for i in 0..num_results {
let old_result = self.inst_results(inst)[i];
let new_result = self.inst_results(new_inst)[i];
self.facts[new_result] = self.facts[old_result].clone();
}
self.make_inst_results(new_inst, ctrl_typevar);
new_inst
}

Expand Down Expand Up @@ -1416,38 +1389,6 @@ impl DataFlowGraph {
pub fn detach_inst_results(&mut self, inst: Inst) {
self.results[inst].clear(&mut self.value_lists);
}

/// Merge the facts for two values. If both values have facts and
/// they differ, both values get a special "conflict" fact that is
/// never satisfied.
pub fn merge_facts(&mut self, a: Value, b: Value) {
let a = self.resolve_aliases(a);
let b = self.resolve_aliases(b);
match (&self.facts[a], &self.facts[b]) {
(Some(a), Some(b)) if a == b => { /* nothing */ }
(None, None) => { /* nothing */ }
(Some(a), None) => {
self.facts[b] = Some(a.clone());
}
(None, Some(b)) => {
self.facts[a] = Some(b.clone());
}
(Some(a_fact), Some(b_fact)) => {
assert_eq!(self.value_type(a), self.value_type(b));
let merged = Fact::intersect(a_fact, b_fact);
crate::trace!(
"facts merge on {} and {}: {:?}, {:?} -> {:?}",
a,
b,
a_fact,
b_fact,
merged,
);
self.facts[a] = Some(merged.clone());
self.facts[b] = Some(merged);
}
}
}
}

/// Contents of a basic block.
Expand Down
28 changes: 0 additions & 28 deletions cranelift/codegen/src/ir/entities.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -187,25 +187,6 @@ impl GlobalValue {
}
}

/// An opaque reference to a memory type.
///
/// A `MemoryType` is a descriptor of a struct layout in memory, with
/// types and proof-carrying-code facts optionally attached to the
/// fields.
#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
pub struct MemoryType(u32);
entity_impl!(MemoryType, "mt");

impl MemoryType {
/// Create a new memory type reference from its number.
///
/// This method is for use by the parser.
pub fn with_number(n: u32) -> Option<Self> {
if n < u32::MAX { Some(Self(n)) } else { None }
}
}

/// An opaque reference to a constant.
///
/// You can store [`ConstantData`](super::ConstantData) in a
Expand Down Expand Up @@ -400,8 +381,6 @@ pub enum AnyEntity {
DynamicType(DynamicType),
/// A Global value.
GlobalValue(GlobalValue),
/// A memory type.
MemoryType(MemoryType),
/// A jump table.
JumpTable(JumpTable),
/// A constant.
Expand All @@ -427,7 +406,6 @@ impl fmt::Display for AnyEntity {
Self::DynamicStackSlot(r) => r.fmt(f),
Self::DynamicType(r) => r.fmt(f),
Self::GlobalValue(r) => r.fmt(f),
Self::MemoryType(r) => r.fmt(f),
Self::JumpTable(r) => r.fmt(f),
Self::Constant(r) => r.fmt(f),
Self::FuncRef(r) => r.fmt(f),
Expand Down Expand Up @@ -486,12 +464,6 @@ impl From<GlobalValue> for AnyEntity {
}
}

impl From<MemoryType> for AnyEntity {
fn from(r: MemoryType) -> Self {
Self::MemoryType(r)
}
}

impl From<JumpTable> for AnyEntity {
fn from(r: JumpTable) -> Self {
Self::JumpTable(r)
Expand Down
19 changes: 2 additions & 17 deletions cranelift/codegen/src/ir/function.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ use crate::ir::DebugTags;
use crate::ir::{
self, Block, DataFlowGraph, DynamicStackSlot, DynamicStackSlotData, DynamicStackSlots,
DynamicType, ExtFuncData, FuncRef, GlobalValue, GlobalValueData, Inst, JumpTable,
JumpTableData, Layout, MemoryType, MemoryTypeData, SigRef, Signature, SourceLocs, StackSlot,
StackSlotData, StackSlots, Type, pcc::Fact,
JumpTableData, Layout, SigRef, Signature, SourceLocs, StackSlot, StackSlotData, StackSlots,
Type,
};
use crate::isa::CallConv;
use crate::write::{write_function, write_function_spec};
Expand Down Expand Up @@ -173,12 +173,6 @@ pub struct FunctionStencil {
/// Global values referenced.
pub global_values: PrimaryMap<ir::GlobalValue, ir::GlobalValueData>,

/// Global value proof-carrying-code facts.
pub global_value_facts: SecondaryMap<ir::GlobalValue, Option<Fact>>,

/// Memory types for proof-carrying code.
pub memory_types: PrimaryMap<ir::MemoryType, ir::MemoryTypeData>,

/// Data flow graph containing the primary definition of all instructions, blocks and values.
pub dfg: DataFlowGraph,

Expand Down Expand Up @@ -221,8 +215,6 @@ impl FunctionStencil {
self.sized_stack_slots.clear();
self.dynamic_stack_slots.clear();
self.global_values.clear();
self.global_value_facts.clear();
self.memory_types.clear();
self.dfg.clear();
self.layout.clear();
self.srclocs.clear();
Expand Down Expand Up @@ -257,11 +249,6 @@ impl FunctionStencil {
self.global_values.push(data)
}

/// Declares a memory type for use by the function.
pub fn create_memory_type(&mut self, data: MemoryTypeData) -> MemoryType {
self.memory_types.push(data)
}

/// Find the global dyn_scale value associated with given DynamicType.
pub fn get_dyn_scale(&self, ty: DynamicType) -> GlobalValue {
self.dfg.dynamic_types.get(ty).unwrap().dynamic_scale
Expand Down Expand Up @@ -420,8 +407,6 @@ impl Function {
sized_stack_slots: StackSlots::new(),
dynamic_stack_slots: DynamicStackSlots::new(),
global_values: PrimaryMap::new(),
global_value_facts: SecondaryMap::new(),
memory_types: PrimaryMap::new(),
dfg: DataFlowGraph::new(),
layout: Layout::new(),
srclocs: SecondaryMap::new(),
Expand Down
Loading
Loading