revise InstallVerifyAttrs to remove need for predicate scanning (#3175)

This commit is contained in:
Mark Thom
2025-11-25 23:17:22 -08:00
parent f2e044e5b8
commit 4bd16b8a2e
5 changed files with 2227 additions and 1885 deletions

View File

@@ -834,12 +834,9 @@ enum InstructionTemplate {
// break from loop instruction. // break from loop instruction.
#[strum_discriminants(strum(props(Arity = "0", Name = "break_from_dispatch")))] #[strum_discriminants(strum(props(Arity = "0", Name = "break_from_dispatch")))]
BreakFromDispatchLoop, BreakFromDispatchLoop,
// swap the verify attr interrupt instruction with the next control instruction. // run verify_attr, eventually.
#[strum_discriminants(strum(props(Arity = "0", Name = "install_verify_attr")))] #[strum_discriminants(strum(props(Arity = "0", Name = "run_verify_attr")))]
InstallVerifyAttr, RunVerifyAttr,
// call verify_attrs.
#[strum_discriminants(strum(props(Arity = "1", Name = "verify_attr_interrupt")))]
VerifyAttrInterrupt(usize),
// procedures // procedures
CallClause(ClauseType, usize, usize, bool, bool), // ClauseType, CallClause(ClauseType, usize, usize, bool, bool), // ClauseType,
// arity, // arity,
@@ -1168,33 +1165,6 @@ fn generate_instruction_preface() -> TokenStream {
pub type CodeDeque = VecDeque<Instruction>; pub type CodeDeque = VecDeque<Instruction>;
impl Instruction { impl Instruction {
#[inline]
pub fn registers(&self) -> Vec<RegType> {
match *self {
Instruction::GetConstant(_, _, r) => vec![r],
Instruction::GetList(_, r) => vec![r],
Instruction::GetPartialString(_, _, r) => vec![r],
Instruction::GetStructure(_, _, _, r) => vec![r],
Instruction::GetVariable(r, t) => vec![r, temp_v!(t)],
Instruction::GetValue(r, t) => vec![r, temp_v!(t)],
Instruction::UnifyLocalValue(r) => vec![r],
Instruction::UnifyVariable(r) => vec![r],
Instruction::PutConstant(_, _, r) => vec![r],
Instruction::PutList(_, r) => vec![r],
Instruction::PutPartialString(_, _, r) => vec![r],
Instruction::PutStructure(_, _, r) => vec![r],
Instruction::PutValue(r, t) => vec![r, temp_v!(t)],
Instruction::PutVariable(r, t) => vec![r, temp_v!(t)],
Instruction::SetLocalValue(r) => vec![r],
Instruction::SetVariable(r) => vec![r],
Instruction::SetValue(r) => vec![r],
Instruction::GetLevel(r) => vec![r],
Instruction::GetPrevLevel(r) => vec![r],
Instruction::GetCutPoint(r) => vec![r],
_ => vec![],
}
}
#[inline] #[inline]
pub fn to_indexing_line_mut(&mut self) -> Option<&mut Vec<IndexingLine>> { pub fn to_indexing_line_mut(&mut self) -> Option<&mut Vec<IndexingLine>> {
match self { match self {
@@ -1211,38 +1181,6 @@ fn generate_instruction_preface() -> TokenStream {
} }
} }
#[inline]
pub fn is_head_instr(&self) -> bool {
matches!(self,
Instruction::Deallocate |
Instruction::GetConstant(..) |
Instruction::GetList(..) |
Instruction::GetPartialString(..) |
Instruction::GetStructure(..) |
Instruction::GetValue(..) |
Instruction::UnifyConstant(..) |
Instruction::UnifyLocalValue(..) |
Instruction::UnifyVariable(..) |
Instruction::UnifyValue(..) |
Instruction::UnifyVoid(..) |
Instruction::GetVariable(..) |
Instruction::PutConstant(..) |
Instruction::PutList(..) |
Instruction::PutPartialString(..) |
Instruction::PutStructure(..) |
Instruction::PutUnsafeValue(..) |
Instruction::PutValue(..) |
Instruction::PutVariable(..) |
Instruction::SetConstant(..) |
Instruction::SetLocalValue(..) |
Instruction::SetVariable(..) |
Instruction::SetValue(..) |
Instruction::SetVoid(..) |
Instruction::GetLevel(..) |
Instruction::GetPrevLevel(..) |
Instruction::GetCutPoint(..))
}
pub fn enqueue_functors( pub fn enqueue_functors(
&self, &self,
arena: &mut Arena, arena: &mut Arena,
@@ -1278,11 +1216,8 @@ fn generate_instruction_preface() -> TokenStream {
fn to_functor(&self, arena: &mut Arena) -> MachineStub { fn to_functor(&self, arena: &mut Arena) -> MachineStub {
match self { match self {
&Instruction::InstallVerifyAttr => { &Instruction::RunVerifyAttr => {
functor!(atom!("install_verify_attr")) functor!(atom!("run_verify_attr"))
}
&Instruction::VerifyAttrInterrupt(arity) => {
functor!(atom!("verify_attr_interrupt"), [fixnum(arity)])
} }
&Instruction::DynamicElse(birth, death, next_or_fail) => { &Instruction::DynamicElse(birth, death, next_or_fail) => {
match (death, next_or_fail) { match (death, next_or_fail) {

View File

@@ -41,13 +41,13 @@ impl MachineState {
pub(super) fn push_attr_var_binding(&mut self, h: usize, addr: HeapCellValue) { pub(super) fn push_attr_var_binding(&mut self, h: usize, addr: HeapCellValue) {
if self.attr_var_init.bindings.is_empty() { if self.attr_var_init.bindings.is_empty() {
// save self.p and self.cp and ensure that the next // save self.p and self.cp and ensure that the next
// instruction is InstallVerifyAttrInterrupt. // instruction is RunVerifyAttrInterrupt.
self.attr_var_init.p = self.p; self.attr_var_init.p = self.p;
self.attr_var_init.cp = self.cp; self.attr_var_init.cp = self.cp;
self.p = INSTALL_VERIFY_ATTR_INTERRUPT - 1; self.p = VERIFY_ATTR_INTERRUPT_LOC - 1;
self.cp = INSTALL_VERIFY_ATTR_INTERRUPT; self.cp = VERIFY_ATTR_INTERRUPT_LOC;
} }
debug_assert_eq!(self.heap[h].get_tag(), HeapCellValueTag::AttrVar); debug_assert_eq!(self.heap[h].get_tag(), HeapCellValueTag::AttrVar);

File diff suppressed because it is too large Load Diff

View File

@@ -141,9 +141,8 @@ mod libraries {
} }
pub static BREAK_FROM_DISPATCH_LOOP_LOC: usize = 0; pub static BREAK_FROM_DISPATCH_LOOP_LOC: usize = 0;
pub static INSTALL_VERIFY_ATTR_INTERRUPT: usize = 1; pub static VERIFY_ATTR_INTERRUPT_LOC: usize = 1;
pub static VERIFY_ATTR_INTERRUPT_LOC: usize = 2; pub static LIB_QUERY_SUCCESS: usize = 2;
pub static LIB_QUERY_SUCCESS: usize = 3;
pub struct MachinePreludeView<'a> { pub struct MachinePreludeView<'a> {
pub indices: &'a mut IndexStore, pub indices: &'a mut IndexStore,
@@ -414,12 +413,11 @@ impl Machine {
} }
pub(crate) fn add_impls_to_indices(&mut self) { pub(crate) fn add_impls_to_indices(&mut self) {
let impls_offset = self.code.len() + 4; let impls_offset = self.code.len() + 3;
self.code.extend(vec![ self.code.extend(vec![
Instruction::BreakFromDispatchLoop, Instruction::BreakFromDispatchLoop,
Instruction::InstallVerifyAttr, Instruction::RunVerifyAttr,
Instruction::VerifyAttrInterrupt(0),
Instruction::BreakFromDispatchLoop, // the location of LIB_QUERY_SUCCESS Instruction::BreakFromDispatchLoop, // the location of LIB_QUERY_SUCCESS
Instruction::ExecuteTermGreaterThan, Instruction::ExecuteTermGreaterThan,
Instruction::ExecuteTermLessThan, Instruction::ExecuteTermLessThan,

View File

@@ -24,7 +24,7 @@ use crate::machine::machine_state::*;
use crate::machine::partial_string::*; use crate::machine::partial_string::*;
use crate::machine::stack::*; use crate::machine::stack::*;
use crate::machine::streams::*; use crate::machine::streams::*;
use crate::machine::{get_structure_index, Machine, VERIFY_ATTR_INTERRUPT_LOC}; use crate::machine::{get_structure_index, Machine};
use crate::parser::ast::*; use crate::parser::ast::*;
use crate::parser::char_reader::*; use crate::parser::char_reader::*;
use crate::parser::dashu::Integer; use crate::parser::dashu::Integer;
@@ -6255,6 +6255,7 @@ impl Machine {
self.machine_st.heap[var.get_value() as usize] = value; self.machine_st.heap[var.get_value() as usize] = value;
} }
/*
#[inline(always)] #[inline(always)]
pub(super) fn restore_instr_at_verify_attr_interrupt(&mut self) { pub(super) fn restore_instr_at_verify_attr_interrupt(&mut self) {
match &self.code[VERIFY_ATTR_INTERRUPT_LOC] { match &self.code[VERIFY_ATTR_INTERRUPT_LOC] {
@@ -6269,10 +6270,11 @@ impl Machine {
} }
} }
} }
*/
#[inline(always)] #[inline(always)]
pub(crate) fn reset_attr_var_state(&mut self, queue_len: usize) { pub(crate) fn reset_attr_var_state(&mut self, queue_len: usize) {
self.restore_instr_at_verify_attr_interrupt(); // self.restore_instr_at_verify_attr_interrupt();
self.machine_st.attr_var_init.reset(queue_len); self.machine_st.attr_var_init.reset(queue_len);
} }
@@ -6303,7 +6305,7 @@ impl Machine {
#[inline(always)] #[inline(always)]
pub(crate) fn return_from_verify_attr(&mut self) { pub(crate) fn return_from_verify_attr(&mut self) {
self.restore_instr_at_verify_attr_interrupt(); // self.restore_instr_at_verify_attr_interrupt();
let e = self.machine_st.e; let e = self.machine_st.e;
let frame_len = self.machine_st.stack.index_and_frame(e).prelude.num_cells; let frame_len = self.machine_st.stack.index_and_frame(e).prelude.num_cells;