unsafe stack transition

This commit is contained in:
Mark Thom
2019-11-28 21:22:03 -04:00
parent c219d9ad5f
commit 5723edd765
8 changed files with 49 additions and 45 deletions

View File

@@ -1186,7 +1186,7 @@ indomain(1).
% Examples: % Examples:
% %
% == % ==
% ?- sat(A =< B), Vs = [A,B], sat_count(+[1|Vs], Count). % ?-
% Vs = [A, B], % Vs = [A, B],
% Count = 3, % Count = 3,
% sat(A=:=A*B). % sat(A=:=A*B).
@@ -1197,7 +1197,7 @@ indomain(1).
% Vs = [...], % Vs = [...],
% CountOr = 1329227995784915872903807060280344575, % CountOr = 1329227995784915872903807060280344575,
% CountAnd = 1. % CountAnd = 1.
% == % ==sat(A =< B), Vs = [A,B], sat_count(+[1|Vs], Count).
sat_count(Sat0, N) :- sat_count(Sat0, N) :-
catch((parse_sat(Sat0, Sat), catch((parse_sat(Sat0, Sat),

View File

@@ -48,8 +48,29 @@ call_cleanup(G, C) :- setup_call_cleanup(true, G, C).
setup_call_cleanup(S, G, C) :- '$get_b_value'(B), setup_call_cleanup(S, G, C) :- '$get_b_value'(B),
S, '$set_cp_by_default'(B), '$get_current_block'(Bb), S, '$set_cp_by_default'(B), '$get_current_block'(Bb),
( '$call_with_default_policy'(var(C)) -> throw(error(instantiation_error, setup_call_cleanup/3)) ( '$call_with_default_policy'(var(C)) ->
; '$call_with_default_policy'(scc_helper(C, G, Bb)) ). throw(error(instantiation_error, setup_call_cleanup/3))
; '$call_with_default_policy'(scc_helper(C, G, Bb))
).
:- non_counted_backtracking scc_helper/3.
scc_helper(C, G, Bb) :-
'$get_cp'(Cp), '$install_scc_cleaner'(C, NBb), call(G),
( '$check_cp'(Cp) ->
'$reset_block'(Bb),
'$call_with_default_policy'(run_cleaners_without_handling(Cp))
; '$call_with_default_policy'(true)
; '$reset_block'(NBb),
'$fail').
scc_helper(_, _, Bb) :-
'$reset_block'(Bb), '$get_ball'(Ball),
'$call_with_default_policy'(run_cleaners_with_handling),
'$erase_ball',
'$call_with_default_policy'(throw(Ball)).
scc_helper(_, _, _) :-
'$get_cp'(Cp),
'$call_with_default_policy'(run_cleaners_without_handling(Cp)),
'$fail'.
:- non_counted_backtracking run_cleaners_with_handling/0. :- non_counted_backtracking run_cleaners_with_handling/0.
run_cleaners_with_handling :- run_cleaners_with_handling :-
@@ -67,23 +88,6 @@ run_cleaners_without_handling(Cp) :-
run_cleaners_without_handling(Cp) :- run_cleaners_without_handling(Cp) :-
'$set_cp_by_default'(Cp), '$restore_cut_policy'. '$set_cp_by_default'(Cp), '$restore_cut_policy'.
:- non_counted_backtracking scc_helper/3.
scc_helper(C, G, Bb) :-
'$get_cp'(Cp), '$install_scc_cleaner'(C, NBb), call(G),
( '$check_cp'(Cp) -> '$reset_block'(Bb),
'$call_with_default_policy'(run_cleaners_without_handling(Cp))
; '$call_with_default_policy'(true)
; '$reset_block'(NBb), '$fail').
scc_helper(_, _, Bb) :-
'$reset_block'(Bb), '$get_ball'(Ball),
'$call_with_default_policy'(run_cleaners_with_handling),
'$erase_ball',
'$call_with_default_policy'(throw(Ball)).
scc_helper(_, _, _) :-
'$get_cp'(Cp),
'$call_with_default_policy'(run_cleaners_without_handling(Cp)),
'$fail'.
% call_with_inference_limit % call_with_inference_limit
:- non_counted_backtracking end_block/4. :- non_counted_backtracking end_block/4.

View File

@@ -134,7 +134,7 @@ impl CodeRepo {
); );
Some(RefOrOwned::Owned(call_clause)) Some(RefOrOwned::Owned(call_clause))
} }
&CodePtr::CallN(arity, _) => { &CodePtr::CallN(arity, _, last_call) => {
let call_clause = call_clause!(ClauseType::CallN, arity, 0, last_call); let call_clause = call_clause!(ClauseType::CallN, arity, 0, last_call);
Some(RefOrOwned::Owned(call_clause)) Some(RefOrOwned::Owned(call_clause))
} }

View File

@@ -309,7 +309,7 @@ pub enum REPLCodePtr {
#[derive(Clone, PartialEq)] #[derive(Clone, PartialEq)]
pub enum CodePtr { pub enum CodePtr {
BuiltInClause(BuiltInClauseType, LocalCodePtr), // local is the successor call. BuiltInClause(BuiltInClauseType, LocalCodePtr), // local is the successor call.
CallN(usize, LocalCodePtr), // arity, local. CallN(usize, LocalCodePtr, bool), // arity, local, last call.
Local(LocalCodePtr), Local(LocalCodePtr),
DynamicTransaction(DynamicTransactionType, LocalCodePtr), // the type of transaction, the return pointer. DynamicTransaction(DynamicTransactionType, LocalCodePtr), // the type of transaction, the return pointer.
REPL(REPLCodePtr, LocalCodePtr), // the REPL code, the return pointer. REPL(REPLCodePtr, LocalCodePtr), // the REPL code, the return pointer.
@@ -320,7 +320,7 @@ impl CodePtr {
pub fn local(&self) -> LocalCodePtr { pub fn local(&self) -> LocalCodePtr {
match self { match self {
&CodePtr::BuiltInClause(_, ref local) &CodePtr::BuiltInClause(_, ref local)
| &CodePtr::CallN(_, ref local) | &CodePtr::CallN(_, ref local, _)
| &CodePtr::Local(ref local) => local.clone(), | &CodePtr::Local(ref local) => local.clone(),
&CodePtr::VerifyAttrInterrupt(p) => LocalCodePtr::DirEntry(p), &CodePtr::VerifyAttrInterrupt(p) => LocalCodePtr::DirEntry(p),
&CodePtr::REPL(_, p) | &CodePtr::DynamicTransaction(_, p) => p, &CodePtr::REPL(_, p) | &CodePtr::DynamicTransaction(_, p) => p,
@@ -418,7 +418,7 @@ impl Add<usize> for CodePtr {
| p @ CodePtr::VerifyAttrInterrupt(_) | p @ CodePtr::VerifyAttrInterrupt(_)
| p @ CodePtr::DynamicTransaction(..) => p, | p @ CodePtr::DynamicTransaction(..) => p,
CodePtr::Local(local) => CodePtr::Local(local + rhs), CodePtr::Local(local) => CodePtr::Local(local + rhs),
CodePtr::CallN(_, local) | CodePtr::BuiltInClause(_, local) => { CodePtr::CallN(_, local, _) | CodePtr::BuiltInClause(_, local) => {
CodePtr::Local(local + rhs) CodePtr::Local(local + rhs)
} }
} }

View File

@@ -844,7 +844,7 @@ pub(crate) trait CallPolicy: Any {
return Ok(()); return Ok(());
} }
machine_st.p = CodePtr::CallN(arity, machine_st.p.local()); machine_st.p = CodePtr::CallN(arity, machine_st.p.local(), machine_st.last_call);
} }
ClauseType::BuiltIn(built_in) => { ClauseType::BuiltIn(built_in) => {
machine_st.setup_built_in_call(built_in.clone()); machine_st.setup_built_in_call(built_in.clone());

View File

@@ -608,7 +608,7 @@ impl MachineState {
} }
} }
TrailRef::Ref(Ref::StackCell(b, sc)) => { TrailRef::Ref(Ref::StackCell(b, sc)) => {
if b <= self.b { if b < self.b {
self.trail.push(TrailRef::Ref(Ref::StackCell(b, sc))); self.trail.push(TrailRef::Ref(Ref::StackCell(b, sc)));
self.tr += 1; self.tr += 1;
} }
@@ -693,7 +693,7 @@ impl MachineState {
} }
} }
TrailRef::Ref(Ref::StackCell(b, _)) => { TrailRef::Ref(Ref::StackCell(b, _)) => {
if b <= self.b { if b < self.b {
self.trail[i - offset] = self.trail[i]; self.trail[i - offset] = self.trail[i];
} else { } else {
offset += 1; offset += 1;

View File

@@ -559,12 +559,6 @@ impl Machine {
snapshot.s = self.machine_st.s; snapshot.s = self.machine_st.s;
snapshot.tr = self.machine_st.tr; snapshot.tr = self.machine_st.tr;
snapshot.pstr_tr = self.machine_st.pstr_tr; snapshot.pstr_tr = self.machine_st.pstr_tr;
snapshot.p = self.machine_st.p.clone();
snapshot.cp = self.machine_st.cp;
snapshot.attr_var_init = mem::replace(
&mut self.machine_st.attr_var_init,
AttrVarInitializer::new(0, 0)
);
snapshot.num_of_args = self.machine_st.num_of_args; snapshot.num_of_args = self.machine_st.num_of_args;
snapshot.fail = self.machine_st.fail; snapshot.fail = self.machine_st.fail;
@@ -577,7 +571,6 @@ impl Machine {
snapshot.block = self.machine_st.block; snapshot.block = self.machine_st.block;
snapshot.ball = self.machine_st.ball.take(); snapshot.ball = self.machine_st.ball.take();
snapshot.heap_locs = mem::replace(&mut self.machine_st.heap_locs, IndexMap::new());
snapshot.lifted_heap = mem::replace(&mut self.machine_st.lifted_heap, vec![]); snapshot.lifted_heap = mem::replace(&mut self.machine_st.lifted_heap, vec![]);
snapshot snapshot
@@ -591,9 +584,6 @@ impl Machine {
self.machine_st.s = snapshot.s; self.machine_st.s = snapshot.s;
self.machine_st.tr = snapshot.tr; self.machine_st.tr = snapshot.tr;
self.machine_st.pstr_tr = snapshot.pstr_tr; self.machine_st.pstr_tr = snapshot.pstr_tr;
self.machine_st.p = snapshot.p;
self.machine_st.cp = snapshot.cp;
self.machine_st.attr_var_init = snapshot.attr_var_init;
self.machine_st.num_of_args = snapshot.num_of_args; self.machine_st.num_of_args = snapshot.num_of_args;
self.machine_st.fail = snapshot.fail; self.machine_st.fail = snapshot.fail;
@@ -610,7 +600,6 @@ impl Machine {
self.machine_st.block = snapshot.block; self.machine_st.block = snapshot.block;
self.machine_st.ball = snapshot.ball.take(); self.machine_st.ball = snapshot.ball.take();
self.machine_st.heap_locs = mem::replace(&mut snapshot.heap_locs, IndexMap::new());
self.machine_st.lifted_heap = mem::replace(&mut snapshot.lifted_heap, vec![]); self.machine_st.lifted_heap = mem::replace(&mut snapshot.lifted_heap, vec![]);
} }

View File

@@ -863,7 +863,14 @@ impl MachineState {
let addr = self.store(self.deref(self[temp_v!(1)].clone())); let addr = self.store(self.deref(self[temp_v!(1)].clone()));
match addr { match addr {
Addr::Con(Constant::Usize(old_b)) if self.b <= old_b + 2 => {} Addr::Con(Constant::Usize(old_b)) => {
let prev_b = self.stack.index_or_frame(self.b).prelude.b;
let prev_b = self.stack.index_or_frame(prev_b).prelude.b;
if prev_b > old_b {
self.fail = true;
}
}
_ => self.fail = true, _ => self.fail = true,
}; };
} }
@@ -1511,7 +1518,9 @@ impl MachineState {
match cut_policy.downcast_mut::<SCCCutPolicy>().ok() { match cut_policy.downcast_mut::<SCCCutPolicy>().ok() {
Some(sgc_policy) => { Some(sgc_policy) => {
if let Some((addr, b_cutoff, prev_b)) = sgc_policy.pop_cont_pt() { if let Some((addr, b_cutoff, prev_b)) = sgc_policy.pop_cont_pt() {
if self.b <= b_cutoff + 1 { let b = self.stack.index_or_frame(self.b).prelude.b;
if b <= b_cutoff {
self.block = prev_b; self.block = prev_b;
if let Some(r) = dest.as_var() { if let Some(r) = dest.as_var() {
@@ -1799,7 +1808,9 @@ impl MachineState {
match a2 { match a2 {
Addr::Con(Constant::Usize(bp)) => { Addr::Con(Constant::Usize(bp)) => {
if self.b <= bp + 1 { let prev_b = self.stack.index_or_frame(self.b).prelude.b;
if prev_b <= bp {
let a2 = Addr::Con(atom!("!")); let a2 = Addr::Con(atom!("!"));
self.unify(a1, a2); self.unify(a1, a2);
} else { } else {