[m-rev.] for review: fix two bugs in declarative debugger

Ian MacLarty maclarty at cs.mu.OZ.AU
Thu Jan 13 13:49:46 AEDT 2005


Out of interest I used the declarative debugger's divide and query stategy to 
find both these bugs.  One search space spanned 893 events and took 11 answers
to locate the bug and the other spanned 166 events and took 8 answers.

For review by anyone.

Estimated hours taken: 3
Branches: main

Fix two bugs in the declarative debugger that caused an exception to be thrown
if the `dd' command was issued at a node all of whose descendents were trusted.

Remove a whole lot of now useless code.

browser/declarative_analyser.m
	Instead of aborting when no unknown or skipped suspects can be found
	with top down search, try to extend the search space upward.  Previously
	this was done in decide_analyser_response, however the mechanism to 
	determine if there were any unknown or skipped suspects in the search
	space (are_unknown_suspects) was faulty.  This was fixed by instead 
	checking for this condition in top_down_search, so it made sense to 
	try to extend the search space upwards in top_down_search instead
	of in decide_analyser_response.  The other search strategies don't need 
	to be updated since they all revert to top down search if they can't 
	find any unknown suspects.  The fault with are_unknown_suspects was
	that it assumed that an unexplored suspect would have unknown children,
	which is not the case if it has no children at all.

browser/declarative_edt.m
	Remove are_unknown_suspects and all supporting machinery.

	Fix another bug in least_skipped which determines which of two suspects
	was least skipped: when both suspects were not skipped the wrong 
	suspect was returned, so when called with foldl on a search space with
	no skipped suspects, the starting suspect would be different from the
	final suspect, and choose_skipped_suspect depends on them being the
	same when there are no skipped suspects.

tests/debugger/declarative/Mmakefile
tests/debugger/declarative/all_trusted.exp
tests/debugger/declarative/all_trusted.inp
tests/debugger/declarative/all_trusted.m
	Add a regression test.

Index: browser/declarative_analyser.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/declarative_analyser.m,v
retrieving revision 1.18
diff -u -r1.18 declarative_analyser.m
--- browser/declarative_analyser.m	9 Jan 2005 01:14:02 -0000	1.18
+++ browser/declarative_analyser.m	12 Jan 2005 14:30:35 -0000
@@ -194,7 +194,8 @@
 :- type search_response
 	--->	question(suspect_id)
 	;	require_explicit_subtree(suspect_id)
-	;	require_explicit_supertree.
+	;	require_explicit_supertree
+	;	no_suspects.
 
 	% The analyser state records all of the information that needs
 	% to be remembered across multiple invocations of the analyser.
@@ -412,8 +413,6 @@
 				[RootId | CorrectDescendents], 
 				InadmissibleChildren, Response)
 		;
-			are_unknown_suspects(!.SearchSpace)
-		->
 			search(Store, !SearchSpace, !.Analyser ^ search_mode,
 				!.Analyser ^ fallback_search_mode, NewMode, 
 				SearchResponse),
@@ -422,37 +421,6 @@
 			!:Analyser = !.Analyser ^ search_mode := NewMode,
 			handle_search_response(Store, SearchResponse, 
 				!Analyser, Response)
-		;		
-			%
-			% Try to extend the search space upwards.  If this
-			% fails and we're not at the topmost traced node, then
-			% request that an explicit supertree be generated.
-			%
-			(
-				extend_search_space_upwards(Store,
-					!SearchSpace)
-			->
-				!:Analyser = !.Analyser ^ search_space :=
-					!.SearchSpace,
-				decide_analyser_response(Store, Response,
-					!Analyser)
-			;
-				topmost_det(!.SearchSpace, TopMostId),
-				TopMostNode = get_edt_node(!.SearchSpace,
-					TopMostId),
-				(
-					edt_topmost_node(Store, TopMostNode)
-				->
-					% We can't look any higher.
-					Response = no_suspects
-				;
-					Response = require_explicit_supertree(
-						TopMostNode),
-					!:Analyser = !.Analyser ^
-						require_explicit := yes(
-							explicit_supertree)
-				)
-			)
 		)
 	),
 	% Do a sanity check after the search to determine if the search 
@@ -461,7 +429,6 @@
 	check_search_space_consistency(Store, !.Analyser ^ search_space,
 		"End of decide_analyser_response").
 
-
 :- pred handle_search_response(S::in, search_response::in, 
 	analyser_state(T)::in, analyser_state(T)::out, 
 	analyser_response(T)::out) is det <= mercury_edt(S, T).
@@ -509,6 +476,8 @@
 	TopMost = get_edt_node(SearchSpace, TopMostId),
 	Response = require_explicit_supertree(TopMost).
 
+handle_search_response(_, no_suspects, !Analyser, no_suspects).
+
 	% bug_response(Store, IoActionMap, SearchSpace, BugId, Evidence, 
 	%	InadmissibleChildren, Response)
 	% Create a bug analyser-response using the given Evidence.  If 
@@ -601,8 +570,36 @@
 			->
 				Response = question(SkippedSuspect)
 			;
-				throw(internal_error("top_down_search",
-					"no unknown or skipped suspects"))
+				%
+				% Try to extend the search space upwards.  If
+				% this fails and we're not at the topmost
+				% traced node, then request that an explicit
+				% supertree be generated.
+				%
+				(
+					extend_search_space_upwards(Store,
+						!.SearchSpace,
+						ExtendedSearchSpace)
+				->
+					top_down_search(Store,
+						ExtendedSearchSpace,
+						!:SearchSpace, Response)
+				;
+					topmost_det(!.SearchSpace, TopMostId),
+					TopMostNode =
+						get_edt_node(!.SearchSpace,
+						TopMostId),
+					(
+						edt_topmost_node(Store,
+							TopMostNode)
+					->
+						% We can't look any higher.
+						Response = no_suspects
+					;
+						Response =
+						    require_explicit_supertree
+					)
+				)
 			)
 		)
 	;
Index: browser/declarative_edt.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/declarative_edt.m,v
retrieving revision 1.3
diff -u -r1.3 declarative_edt.m
--- browser/declarative_edt.m	9 Jan 2005 01:14:02 -0000	1.3
+++ browser/declarative_edt.m	13 Jan 2005 02:00:47 -0000
@@ -442,10 +442,6 @@
 :- pred give_up_subterm_tracking(search_space(T)::in, suspect_id::in) 
 	is semidet.
 
-	% Are there any unknown or skipped suspects in the search space?
-	%
-:- pred are_unknown_suspects(search_space(T)::in) is semidet.
-
 	% Mark the root and it's non-ignored children as unknown.
 	% Throws an exception if the search space doesn't have a root.
 	%
@@ -552,22 +548,11 @@
 				% We use a bimap so we can also find the
 				% implicit root given an explicit root.
 				%
-			implicit_roots_to_explicit_roots	:: bimap(T, T),
-
-				% How many skipped or unknown suspects are in
-				% the search space?
-			unknown_count		:: int,
-
-				% How many suspects in the search space have
-				% we not explored the children of whos children
-				% might be worth exploring? (i.e. we don't 
-				% include unexplored children of correct,
-				% inadmissible or pruned suspects)
-			unexplored_leaves	:: int
+			implicit_roots_to_explicit_roots	:: bimap(T, T)
 	).
 
 empty_search_space = search_space(no, no, counter.init(0), counter.init(0), 
-	map.init, bimap.init, 0, 0).
+	map.init, bimap.init).
 
 root(SearchSpace, RootId) :- SearchSpace ^ root = yes(RootId).
 
@@ -580,9 +565,6 @@
 		throw(internal_error("topmost_det", "search space empty"))
 	).
 
-are_unknown_suspects(SearchSpace) :- SearchSpace ^ unknown_count > 0.
-are_unknown_suspects(SearchSpace) :- SearchSpace ^ unexplored_leaves > 0.
-
 suspect_is_bug(Store, SuspectId, !SearchSpace, CorrectDescendents,
 		InadmissibleChildren) :-
 	suspect_erroneous(!.SearchSpace, SuspectId),
@@ -752,15 +734,12 @@
 	map.set(!.SearchSpace ^ store, SuspectId, 
 		(Suspect ^ status := Status) ^ weight := 0, SuspectStore),
 	!:SearchSpace = !.SearchSpace ^ store := SuspectStore,
-	adjust_unknown_count(yes(Suspect ^ status), Status, !SearchSpace),
 	(
 		Suspect ^ children = yes(Children),
 		list.foldl(propagate_status_downwards(pruned, 
 			[correct, inadmissible]), Children, !SearchSpace)
 	;
-		Suspect ^ children = no,
-		adjust_unexplored_leaves(yes(Suspect ^ status), Status, 
-			!SearchSpace)
+		Suspect ^ children = no
 	),
 	% Remove the suspect's weight from its ancestors, since its weight is
 	% now zero.
@@ -800,14 +779,6 @@
 	map.set(!.SearchSpace ^ store, SuspectId, Suspect ^ status :=
 		erroneous, Store),
 	!:SearchSpace = !.SearchSpace ^ store := Store,
-	adjust_unknown_count(yes(Suspect ^ status), erroneous, !SearchSpace),
-	(
-		Suspect ^ children = no,
-		adjust_unexplored_leaves(yes(Suspect ^ status), erroneous, 
-			!SearchSpace)
-	;
-		Suspect ^ children = yes(_)
-	),
 	propagate_status_upwards(in_erroneous_subtree_complement, 
 		[erroneous, correct, inadmissible], SuspectId, _,
 		!SearchSpace),
@@ -815,7 +786,6 @@
 
 ignore_suspect(Store, SuspectId, !SearchSpace) :-
 	lookup_suspect(!.SearchSpace, SuspectId, Suspect),
-	adjust_unknown_count(yes(Suspect ^ status), ignored, !SearchSpace),
 	calc_suspect_weight(Store, Suspect ^ edt_node, Suspect ^ children, 
 		ignored, !.SearchSpace, Weight, _),
 	map.set(!.SearchSpace ^ store, SuspectId, 
@@ -1073,12 +1043,8 @@
 				StopStatusSet), Children, !StopSuspects,
 				!SearchSpace)
 		;
-			Suspect ^ children = no,
-			adjust_unexplored_leaves(yes(Suspect ^ status), Status, 
-				!SearchSpace)
-		),
-		adjust_unknown_count(yes(Suspect ^ status), Status, 
-			!SearchSpace)
+			Suspect ^ children = no
+		)
 	;
 		list.cons(SuspectId, !StopSuspects)
 	).
@@ -1112,112 +1078,15 @@
 			Children, [], StopSuspects, !SearchSpace)
 	;
 		Suspect ^ children = no,
-		adjust_unexplored_leaves(yes(Suspect ^ status), Status, 
-			!SearchSpace),
 		StopSuspects = []
-	),
-	adjust_unknown_count(yes(Suspect ^ status), Status, !SearchSpace).
-
-	% Increments or decrements the unknown suspect count after a status
-	% change.  The first argument should be the previous status of the 
-	% changed suspect or no if a new suspect is being added and the second
-	% argument should be the suspect's new status.
-	%
-:- pred adjust_unknown_count(maybe(suspect_status)::in, suspect_status::in, 
-	search_space(T)::in, search_space(T)::out) is det.
-
-adjust_unknown_count(MaybeOldStatus, NewStatus, !SearchSpace) :- 
-	(
-		MaybeOldStatus = yes(OldStatus),
-		questionable(OldStatus, yes),
-		questionable(NewStatus, no)
-	->
-		!:SearchSpace = !.SearchSpace ^ unknown_count :=
-			!.SearchSpace ^ unknown_count - 1
-	;
-		questionable(NewStatus, yes),
-		(
-			MaybeOldStatus = no
-		;
-			MaybeOldStatus = yes(OldStatus),
-			questionable(OldStatus, no)
-		)
-	->
-		!:SearchSpace = !.SearchSpace ^ unknown_count :=
-			!.SearchSpace ^ unknown_count + 1
-	;
-		true
-	).
-
-	% Increments or decrements the unexplored leaves count after a status
-	% change.  The first argument should be the previous status of the 
-	% changed suspect or no if a new suspect is being added and the second
-	% argument should be the suspect's new status.  The changed suspect
-	% should be a leaf node (i.e. have its children field set to no).
-	%
-:- pred adjust_unexplored_leaves(maybe(suspect_status)::in, suspect_status::in, 
-	search_space(T)::in, search_space(T)::out) is det.
-
-adjust_unexplored_leaves(MaybeOldStatus, NewStatus, !SearchSpace) :- 
-	(
-		MaybeOldStatus = yes(OldStatus),
-		in_buggy_subtree(OldStatus, yes),
-		in_buggy_subtree(NewStatus, no)
-	->
-		!:SearchSpace = !.SearchSpace ^ unexplored_leaves :=
-			!.SearchSpace ^ unexplored_leaves - 1
-	;
-		in_buggy_subtree(NewStatus, yes),
-		(
-			MaybeOldStatus = no
-		;
-			MaybeOldStatus = yes(OldStatus),
-			in_buggy_subtree(OldStatus, no)
-		)
-	->
-		!:SearchSpace = !.SearchSpace ^ unexplored_leaves :=
-			!.SearchSpace ^ unexplored_leaves + 1
-	;
-		true
-	).
-
-	% Decrement the unexplored leaves count if the given status indicates
-	% that the suspect is in a potentially buggy part of the search space.
-	%
-:- pred decrement_unexplored_leaves(suspect_status::in, 
-	search_space(T)::in, search_space(T)::out) is det.
-
-decrement_unexplored_leaves(OldStatus, !SearchSpace) :-
-	(
-		in_buggy_subtree(OldStatus, yes)
-	->
-		!:SearchSpace = !.SearchSpace ^ unexplored_leaves :=
-			!.SearchSpace ^ unexplored_leaves - 1
-	;
-		true
 	).
 
 check_search_space_consistency(Store, SearchSpace, Context) :-
 	(
-		SearchSpace ^ unknown_count \= calc_num_unknown(SearchSpace)
-	->
-		throw(internal_error("check_search_space_consistency",
-			"unknown count incorrect. search space follows.\n" 
-			++ string(SearchSpace) ++ "\n Context is:\n" ++
-			Context))
-	;
-		SearchSpace ^ unexplored_leaves \= calc_num_unexplored(
-			SearchSpace)
-	->
-		throw(internal_error("check_search_space_consistency",
-			"unexplored leaves incorrect. search space follows.\n"
-			++ string(SearchSpace) ++ "\n Context is:\n" ++
-			Context))
-	;
 		find_inconsistency_in_weights(Store, SearchSpace, Message)
 	->
 		throw(internal_error("check_search_space_consistency",
-			Message))
+			Message ++ "\n Context = " ++ Context))
 	;
 		true
 	).
@@ -1460,8 +1329,6 @@
 				ParentId, Lowest, !SearchSpace),
 			map.set(!.SearchSpace ^ store, ParentId, 
 				Parent ^ status := Status, Store),
-			adjust_unknown_count(yes(Parent ^ status), Status,
-				!SearchSpace),
 			!:SearchSpace = !.SearchSpace ^ store := Store
 		;
 			Lowest = ParentId
@@ -1539,8 +1406,7 @@
 		map.set(!.SearchSpace ^ store, SuspectId, 
 			Suspect ^ children := yes(Children), SuspectStore),
 		!:SearchSpace = !.SearchSpace ^ store := SuspectStore
-	),
-	decrement_unexplored_leaves(Suspect ^ status, !SearchSpace).
+	).
 
 :- pred add_children_2(S::in, list(T)::in, suspect_id::in, suspect_status::in, 
 	int::in, search_space(T)::in, search_space(T)::out, counter::in,
@@ -1558,8 +1424,6 @@
 		SuspectStore),
 	!:SearchSpace = !.SearchSpace ^ store := SuspectStore,
 	add_weight_to_ancestors(NextId, ExcessWeight, !SearchSpace),
-	adjust_unknown_count(no, Status, !SearchSpace),
-	adjust_unexplored_leaves(no, Status, !SearchSpace),
 	add_children_2(Store, EDTChildren, SuspectId, Status, Depth, 
 		!SearchSpace, !Counter, OtherChildren),
 	Children = [NextId | OtherChildren].
@@ -1569,7 +1433,7 @@
 	map.set(init, 0, suspect(no, Node, unknown, 0, no, Weight), 
 		SuspectStore),
 	SearchSpace = search_space(no, yes(0), counter.init(1), 
-		counter.init(0), SuspectStore, bimap.init, 1, 1).
+		counter.init(0), SuspectStore, bimap.init).
 
 incorporate_explicit_subtree(SuspectId, Node, !SearchSpace) :-
 	lookup_suspect(!.SearchSpace, SuspectId, Suspect),
@@ -1664,14 +1528,6 @@
 				NewTopMostId, SiblingStatus,
 				!SearchSpace, ChildrenIds),
 			
-			% 
-			% Adjust the unexplored leaves count since the new top
-			% most node was added with no children (so add_children
-			% would have incorrectly subtracted 1 from the count).
-			%
-			adjust_unexplored_leaves(no, NewTopMostStatus, 
-				!SearchSpace),
-
 			%
 			% Now add the old topmost node as a child to the new
 			% topmost node.
@@ -1710,10 +1566,7 @@
 					!.SuspectStore
 			),
 			!:SearchSpace = !.SearchSpace ^ topmost :=
-				yes(NewTopMostId),
-
-			adjust_unknown_count(no, NewTopMostStatus, 
-				!SearchSpace)
+				yes(NewTopMostId)
 		;
 			throw(internal_error("insert_new_topmost_node",
 				"couldn't find event number"))
@@ -1811,7 +1664,7 @@
 	%	LeastSkipped) :-
 	% LeastSkipped is whichever of SuspectId1 and SuspectId2 has the lowest
 	% skip order?  If neither has been skipped then LeastSuspect =
-	% SuspectId1.  Suspect1 is the suspect referenced by SuspectId1 and is
+	% SuspectId2.  Suspect1 is the suspect referenced by SuspectId1 and is
 	% present so we can use this predicate with map.foldl.
 	%
 :- pred least_skipped(search_space(T)::in, suspect_id::in, suspect(T)::in, 
@@ -1831,11 +1684,11 @@
 			LeastSkipped = SuspectId1
 		)
 	;
-		Status2 = skipped(_)
+		Status1 = skipped(_)
 	->
-		LeastSkipped = SuspectId2
-	;
 		LeastSkipped = SuspectId1
+	;
+		LeastSkipped = SuspectId2
 	).
 
 first_unknown_descendent(Store, SuspectId, !SearchSpace, 
@@ -1918,8 +1771,13 @@
 	).
 
 pick_implicit_root(Store, SearchSpace, ImplicitRoot) :-
-	SearchSpace ^ root = yes(RootId),
-	find_first_implicit_root(Store, SearchSpace, [RootId], ImplicitRoot).
+	(
+		SearchSpace ^ root = yes(StartId)
+	;
+		SearchSpace ^ root = no,
+		SearchSpace ^ topmost = yes(StartId)
+	),
+	find_first_implicit_root(Store, SearchSpace, [StartId], ImplicitRoot).
 
 	% Look for an implicit root in the descendents of each suspect in
 	% the list in a depth first fashion.
Index: tests/debugger/declarative/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/debugger/declarative/Mmakefile,v
retrieving revision 1.69
diff -u -r1.69 Mmakefile
--- tests/debugger/declarative/Mmakefile	9 Jan 2005 01:14:05 -0000	1.69
+++ tests/debugger/declarative/Mmakefile	12 Jan 2005 14:15:38 -0000
@@ -6,6 +6,7 @@
 
 DECLARATIVE_PROGS=		\
 	aadebug			\
+	all_trusted		\
 	app			\
 	args			\
 	backtrack		\
@@ -166,6 +167,10 @@
 
 aadebug.out: aadebug aadebug.inp
 	$(MDB_STD) ./aadebug < aadebug.inp > aadebug.out 2>&1 \
+	|| { grep . $@ /dev/null; exit 1; }
+
+all_trusted.out: all_trusted all_trusted.inp
+	$(MDB_STD) ./all_trusted < all_trusted.inp > all_trusted.out 2>&1 \
 	|| { grep . $@ /dev/null; exit 1; }
 
 app.out: app app.inp
Index: tests/debugger/declarative/all_trusted.exp
===================================================================
RCS file: tests/debugger/declarative/all_trusted.exp
diff -N tests/debugger/declarative/all_trusted.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/debugger/declarative/all_trusted.exp	12 Jan 2005 14:13:11 -0000
@@ -0,0 +1,26 @@
+      E1:     C1 CALL pred all_trusted.main/2-0 (det) all_trusted.m:13
+mdb> mdb> Contexts will not be printed.
+mdb> echo on
+Command echo enabled.
+mdb> table_io allow
+mdb> table_io start
+I/O tabling started.
+mdb> trust all_trusted
+Trusting module all_trusted
+mdb> break p
+ 0: + stop  interface pred all_trusted.p/2-0 (det)
+mdb> c
+      E2:     C2 CALL pred all_trusted.p/2-0 (det)
+mdb> f
+      E3:     C2 EXIT pred all_trusted.p/2-0 (det)
+mdb> dd -a
+2No bug found.
+      E3:     C2 EXIT pred all_trusted.p/2-0 (det)
+mdb> break main
+ 1: + stop  interface pred all_trusted.main/2-0 (det)
+mdb> c
+2      E4:     C1 EXIT pred all_trusted.main/2-0 (det)
+mdb> dd -a
+2No bug found.
+2      E4:     C1 EXIT pred all_trusted.main/2-0 (det)
+mdb> quit -y
Index: tests/debugger/declarative/all_trusted.inp
===================================================================
RCS file: tests/debugger/declarative/all_trusted.inp
diff -N tests/debugger/declarative/all_trusted.inp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/debugger/declarative/all_trusted.inp	12 Jan 2005 14:12:45 -0000
@@ -0,0 +1,14 @@
+register --quiet
+context none
+echo on
+table_io allow
+table_io start
+trust all_trusted
+break p
+c
+f
+dd -a
+break main
+c
+dd -a
+quit -y
Index: tests/debugger/declarative/all_trusted.m
===================================================================
RCS file: tests/debugger/declarative/all_trusted.m
diff -N tests/debugger/declarative/all_trusted.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/debugger/declarative/all_trusted.m	12 Jan 2005 13:12:48 -0000
@@ -0,0 +1,23 @@
+:- module all_trusted.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- import_module int.
+
+main(!IO) :-
+	p(1, X),
+	io.write_int(X, !IO).
+
+:- pred p(int::in, int::out) is det.
+
+p(X, Y) :- q(X, Y).
+
+:- pred q(int::in, int::out) is det.
+
+q(X, X+1).
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------



More information about the reviews mailing list