From 5723edd765f52e4f0e022fdb91fd7ca970391df7 Mon Sep 17 00:00:00 2001 From: Mark Thom Date: Thu, 28 Nov 2019 21:22:03 -0400 Subject: [PATCH] unsafe stack transition --- src/prolog/lib/clpb.pl | 4 +-- src/prolog/lib/non_iso.pl | 46 +++++++++++++----------- src/prolog/machine/code_repo.rs | 2 +- src/prolog/machine/machine_indices.rs | 6 ++-- src/prolog/machine/machine_state.rs | 2 +- src/prolog/machine/machine_state_impl.rs | 4 +-- src/prolog/machine/mod.rs | 11 ------ src/prolog/machine/system_calls.rs | 19 +++++++--- 8 files changed, 49 insertions(+), 45 deletions(-) diff --git a/src/prolog/lib/clpb.pl b/src/prolog/lib/clpb.pl index 5aa9561a..3eba9a73 100644 --- a/src/prolog/lib/clpb.pl +++ b/src/prolog/lib/clpb.pl @@ -1186,7 +1186,7 @@ indomain(1). % Examples: % % == -% ?- sat(A =< B), Vs = [A,B], sat_count(+[1|Vs], Count). +% ?- % Vs = [A, B], % Count = 3, % sat(A=:=A*B). @@ -1197,7 +1197,7 @@ indomain(1). % Vs = [...], % CountOr = 1329227995784915872903807060280344575, % CountAnd = 1. -% == +% ==sat(A =< B), Vs = [A,B], sat_count(+[1|Vs], Count). sat_count(Sat0, N) :- catch((parse_sat(Sat0, Sat), diff --git a/src/prolog/lib/non_iso.pl b/src/prolog/lib/non_iso.pl index 84595e83..b4f9394d 100644 --- a/src/prolog/lib/non_iso.pl +++ b/src/prolog/lib/non_iso.pl @@ -48,8 +48,29 @@ call_cleanup(G, C) :- setup_call_cleanup(true, G, C). setup_call_cleanup(S, G, C) :- '$get_b_value'(B), 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'(scc_helper(C, G, Bb)) ). + ( '$call_with_default_policy'(var(C)) -> + 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. run_cleaners_with_handling :- @@ -67,23 +88,6 @@ run_cleaners_without_handling(Cp) :- run_cleaners_without_handling(Cp) :- '$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 :- non_counted_backtracking end_block/4. @@ -119,8 +123,8 @@ call_with_inference_limit(G, L, R, Bb, B) :- call_with_inference_limit(_, _, R, Bb, B) :- '$reset_block'(Bb), '$remove_inference_counter'(B, _), - ( '$get_ball'(Ball), '$get_level'(Cp), '$set_cp_by_default'(Cp) - ; '$remove_call_policy_check'(B), '$fail' ), + ( '$get_ball'(Ball), '$get_level'(Cp), '$set_cp_by_default'(Cp) + ; '$remove_call_policy_check'(B), '$fail' ), '$erase_ball', '$call_with_default_policy'(handle_ile(B, Ball, R)). diff --git a/src/prolog/machine/code_repo.rs b/src/prolog/machine/code_repo.rs index df80644f..fee126e9 100644 --- a/src/prolog/machine/code_repo.rs +++ b/src/prolog/machine/code_repo.rs @@ -134,7 +134,7 @@ impl CodeRepo { ); Some(RefOrOwned::Owned(call_clause)) } - &CodePtr::CallN(arity, _) => { + &CodePtr::CallN(arity, _, last_call) => { let call_clause = call_clause!(ClauseType::CallN, arity, 0, last_call); Some(RefOrOwned::Owned(call_clause)) } diff --git a/src/prolog/machine/machine_indices.rs b/src/prolog/machine/machine_indices.rs index a6c32597..10afcbe4 100644 --- a/src/prolog/machine/machine_indices.rs +++ b/src/prolog/machine/machine_indices.rs @@ -309,7 +309,7 @@ pub enum REPLCodePtr { #[derive(Clone, PartialEq)] pub enum CodePtr { BuiltInClause(BuiltInClauseType, LocalCodePtr), // local is the successor call. - CallN(usize, LocalCodePtr), // arity, local. + CallN(usize, LocalCodePtr, bool), // arity, local, last call. Local(LocalCodePtr), DynamicTransaction(DynamicTransactionType, LocalCodePtr), // the type of transaction, the return pointer. REPL(REPLCodePtr, LocalCodePtr), // the REPL code, the return pointer. @@ -320,7 +320,7 @@ impl CodePtr { pub fn local(&self) -> LocalCodePtr { match self { &CodePtr::BuiltInClause(_, ref local) - | &CodePtr::CallN(_, ref local) + | &CodePtr::CallN(_, ref local, _) | &CodePtr::Local(ref local) => local.clone(), &CodePtr::VerifyAttrInterrupt(p) => LocalCodePtr::DirEntry(p), &CodePtr::REPL(_, p) | &CodePtr::DynamicTransaction(_, p) => p, @@ -418,7 +418,7 @@ impl Add for CodePtr { | p @ CodePtr::VerifyAttrInterrupt(_) | p @ CodePtr::DynamicTransaction(..) => p, CodePtr::Local(local) => CodePtr::Local(local + rhs), - CodePtr::CallN(_, local) | CodePtr::BuiltInClause(_, local) => { + CodePtr::CallN(_, local, _) | CodePtr::BuiltInClause(_, local) => { CodePtr::Local(local + rhs) } } diff --git a/src/prolog/machine/machine_state.rs b/src/prolog/machine/machine_state.rs index 43447666..63612858 100644 --- a/src/prolog/machine/machine_state.rs +++ b/src/prolog/machine/machine_state.rs @@ -844,7 +844,7 @@ pub(crate) trait CallPolicy: Any { 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) => { machine_st.setup_built_in_call(built_in.clone()); diff --git a/src/prolog/machine/machine_state_impl.rs b/src/prolog/machine/machine_state_impl.rs index 90ddcb54..3f6df8b4 100644 --- a/src/prolog/machine/machine_state_impl.rs +++ b/src/prolog/machine/machine_state_impl.rs @@ -608,7 +608,7 @@ impl MachineState { } } TrailRef::Ref(Ref::StackCell(b, sc)) => { - if b <= self.b { + if b < self.b { self.trail.push(TrailRef::Ref(Ref::StackCell(b, sc))); self.tr += 1; } @@ -693,7 +693,7 @@ impl MachineState { } } TrailRef::Ref(Ref::StackCell(b, _)) => { - if b <= self.b { + if b < self.b { self.trail[i - offset] = self.trail[i]; } else { offset += 1; diff --git a/src/prolog/machine/mod.rs b/src/prolog/machine/mod.rs index e71bd826..005bf01c 100644 --- a/src/prolog/machine/mod.rs +++ b/src/prolog/machine/mod.rs @@ -559,12 +559,6 @@ impl Machine { snapshot.s = self.machine_st.s; snapshot.tr = self.machine_st.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.fail = self.machine_st.fail; @@ -577,7 +571,6 @@ impl Machine { snapshot.block = self.machine_st.block; 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 @@ -591,9 +584,6 @@ impl Machine { self.machine_st.s = snapshot.s; self.machine_st.tr = snapshot.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.fail = snapshot.fail; @@ -610,7 +600,6 @@ impl Machine { self.machine_st.block = snapshot.block; 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![]); } diff --git a/src/prolog/machine/system_calls.rs b/src/prolog/machine/system_calls.rs index c8b841c3..3f66dde7 100644 --- a/src/prolog/machine/system_calls.rs +++ b/src/prolog/machine/system_calls.rs @@ -863,7 +863,14 @@ impl MachineState { let addr = self.store(self.deref(self[temp_v!(1)].clone())); 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, }; } @@ -1421,7 +1428,7 @@ impl MachineState { let var_list_addr = Addr::HeapCell(self.heap.to_list(iter)); let list_addr = self[temp_v!(2)].clone(); - + self.unify(var_list_addr, list_addr); } else { self.fail = true; @@ -1511,7 +1518,9 @@ impl MachineState { match cut_policy.downcast_mut::().ok() { Some(sgc_policy) => { 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; if let Some(r) = dest.as_var() { @@ -1799,7 +1808,9 @@ impl MachineState { match a2 { 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!("!")); self.unify(a1, a2); } else { -- 2.54.0