[m-rev.] for review: divide and query search for declarative debugger
Ian MacLarty
maclarty at cs.mu.OZ.AU
Tue Dec 21 22:50:29 AEDT 2004
For review by Zoltan and/or Mark. Documentation for review by anyone.
Estimated hours taken: 80
Branches: main
Add divide and query search strategy to declarative debugger. This version of
divide and query uses the number of descendent events as a weighting instead of
the number of descendent nodes, mainly because this is easy to compute when
portions of the annotated trace are not materialized.
browser/declarative_analyser.m
Implement divide and query search.
Introduce a default search mode which can be either top-down or
divide and query.
browser/declarative_debugger.m
Export predicates so the default search mode can be set with the
`dd' command.
browser/declarative_edt.m
Implement helper predicates for divide and query search.
Maintain a weight field for each suspect and adjust this when
suspects are asserted correct, inadmissible or ignored.
Implement a check to make sure all suspects in the portion of the
search space that could contain a bug have the correct weights.
Recalculate the weights when a node is revised.
browser/declarative_execution.m
Record REDO event numbers since these are used to calculate the
number of descendent events for backtracked over calls.
browser/declarative_tree.m
Implement predicate to calculate the number of descendent events
for a node in the EDT.
doc/user_guide.texi
Document divide and query and top-down search strategies and
document the new --default-search-mode dd option.
tests/debugger/declarative/Mmakefile
tests/debugger/declarative/divide_and_query1.exp
tests/debugger/declarative/divide_and_query1.inp
tests/debugger/declarative/divide_and_query1.m
Test divide and query search strategy.
trace/mercury_trace_declarative.h
trace/mercury_trace_declarative.c
Record REDO event numbers.
Add some functions to set the default search mode by calling the
predicate exported from declarative_debugger.m
Add a function to check in a search mode argument string is valid.
trace/mercury_trace_internal.c
Add --default-search-mode option for `dd' command.
Use readline completion for `dd' command options.
Index: browser/declarative_analyser.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/declarative_analyser.m,v
retrieving revision 1.17
diff -u -r1.17 declarative_analyser.m
--- browser/declarative_analyser.m 16 Dec 2004 00:12:38 -0000 1.17
+++ browser/declarative_analyser.m 21 Dec 2004 10:48:05 -0000
@@ -51,11 +51,25 @@
:- type analyser_state(T).
+ % The default search mode for the analyser. The analyser will revert
+ % to this search mode if not told to do otherwise by the oracle.
+ %
+:- type default_search_mode
+ ---> top_down
+ ; divide_and_query.
+
:- pred analyser_state_init(io_action_map::in, analyser_state(T)::out) is det.
-
+
% Resets the state of the analyser except for the io_action_map.
+ %
:- pred reset_analyser(analyser_state(T)::in, analyser_state(T)::out) is det.
+ % Make the given default search mode the default search mode
+ % and the current search mode for the analyser.
+ %
+:- pred set_default_search_mode(default_search_mode::in,
+ analyser_state(T)::in, analyser_state(T)::out) is det.
+
:- pred analyser_state_replace_io_map(io_action_map::in,
analyser_state(T)::in, analyser_state(T)::out) is det.
@@ -156,7 +170,19 @@
suspects :: array(suspect_id),
range :: pair(int, int),
last_tested :: int
- ).
+ )
+ ;
+ %
+ % An adapted version of the divide and query approach
+ % proposed by Shapiro. We weight each node with the
+ % number of events executed by descendent children
+ % plus the internal body events of the call. This is
+ % mainly because it's hard to work out how many
+ % descendents are in unmaterialized portions of the EDT
+ % without using memory proportional to the
+ % unmaterialized portion.
+ %
+ divide_and_query.
% Each search algorithm should respond with either a question
% or a request for an explicit subtree to be generated for a suspect
@@ -188,6 +214,12 @@
% oracle.
search_mode :: search_mode,
+ % The search mode to use by default.
+ % This uses a different type since only
+ % non-parametized search modes can sensibly be
+ % used as the default search mode.
+ default_search_mode :: default_search_mode,
+
% Everytime a search finds a suspect to
% ask the oracle about it is put in this field
% before asking the oracle, so the analyser
@@ -218,12 +250,24 @@
; explicit_supertree.
analyser_state_init(IoActionMap, Analyser) :-
- Analyser = analyser(empty_search_space, no, top_down, no,
- IoActionMap, no).
+ Analyser = analyser(empty_search_space, no, top_down,
+ top_down, no, IoActionMap, no).
reset_analyser(!Analyser) :-
- !:Analyser = analyser(empty_search_space, no, top_down, no,
- !.Analyser ^ io_action_map, no).
+ Default = !.Analyser ^ default_search_mode,
+ search_mode_from_default(Default) = SearchMode,
+ !:Analyser = analyser(empty_search_space, no, SearchMode,
+ Default, no, !.Analyser ^ io_action_map, no).
+
+set_default_search_mode(DefaultSearchMode, !Analyser) :-
+ !:Analyser = !.Analyser ^ default_search_mode := DefaultSearchMode,
+ !:Analyser = !.Analyser ^ search_mode :=
+ search_mode_from_default(DefaultSearchMode).
+
+:- func search_mode_from_default(default_search_mode) = search_mode.
+
+search_mode_from_default(top_down) = top_down.
+search_mode_from_default(divide_and_query) = divide_and_query.
analyser_state_replace_io_map(IoActionMap, !Analyser) :-
!:Analyser = !.Analyser ^ io_action_map := IoActionMap.
@@ -254,7 +298,7 @@
% start of a new declarative debugging session.
%
reset_analyser(!Analyser),
- initialise_search_space(Node, SearchSpace),
+ initialise_search_space(Store, Node, SearchSpace),
!:Analyser = !.Analyser ^ search_space := SearchSpace,
topmost_det(SearchSpace, TopMostId),
!:Analyser = !.Analyser ^ last_search_question :=
@@ -284,8 +328,9 @@
skip_suspect(SuspectId, !.Analyser ^ search_space, SearchSpace),
!:Analyser = !.Analyser ^ search_space := SearchSpace.
-process_answer(_, ignore(_), SuspectId, !Analyser) :-
- ignore_suspect(SuspectId, !.Analyser ^ search_space, SearchSpace),
+process_answer(Store, ignore(_), SuspectId, !Analyser) :-
+ ignore_suspect(Store, SuspectId, !.Analyser ^ search_space,
+ SearchSpace),
!:Analyser = !.Analyser ^ search_space := SearchSpace.
process_answer(_, truth_value(_, correct), SuspectId, !Analyser) :-
@@ -337,15 +382,14 @@
edt_question(!.Analyser ^ io_action_map, Store, Node,
Question),
Response = revise(Question),
- revise_root(SearchSpace, SearchSpace1),
+ revise_root(Store, SearchSpace, SearchSpace1),
!:Analyser = !.Analyser ^ search_space := SearchSpace1,
!:Analyser = !.Analyser ^ last_search_question := yes(RootId),
- !:Analyser = !.Analyser ^ search_mode := top_down
+ set_default_search_mode(!.Analyser ^ default_search_mode,
+ !Analyser)
;
- %
% There must be a root, since a bug was found (and is now
% being revised).
- %
throw(internal_error("revise_analysis", "no root"))
).
@@ -354,6 +398,9 @@
is det <= mercury_edt(S, T).
decide_analyser_response(Store, Response, !Analyser) :-
+ % Check an invarients that should hold for the search space.
+ check_search_space_consistency(Store, !.Analyser ^ search_space,
+ "Start of decide_analyser_response"),
some [!SearchSpace] (
!:SearchSpace = !.Analyser ^ search_space,
(
@@ -371,7 +418,8 @@
are_unknown_suspects(!.SearchSpace)
->
search(Store, !SearchSpace, !.Analyser ^ search_mode,
- NewMode, SearchResponse),
+ !.Analyser ^ default_search_mode, NewMode,
+ SearchResponse),
!:Analyser = !.Analyser ^ search_space :=
!.SearchSpace,
!:Analyser = !.Analyser ^ search_mode := NewMode,
@@ -409,7 +457,11 @@
)
)
)
- ).
+ ),
+ % Check an invarients that should hold for the search space.
+ 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,
@@ -495,26 +547,34 @@
% next time round.
%
:- pred search(S::in, search_space(T)::in, search_space(T)::out,
- search_mode::in, search_mode::out, search_response::out)
- is det <= mercury_edt(S, T).
+ search_mode::in, default_search_mode::in,
+ search_mode::out, search_response::out) is det <= mercury_edt(S, T).
-search(Store, !SearchSpace, top_down, NewMode, Response) :-
- top_down_search(Store, !SearchSpace, Response, NewMode).
+search(Store, !SearchSpace, top_down, DefaultSearchMode, NewMode, Response) :-
+ top_down_search(Store, !SearchSpace, Response),
+ % We always go back to the default search mode after a top-down
+ % search, because some default searches (such as divide and query)
+ % use top-down as a fail safe and we want the default search to
+ % resume after the top-down search.
+ NewMode = search_mode_from_default(DefaultSearchMode).
search(Store, !SearchSpace, follow_subterm_end(SuspectId, ArgPos, TermPath,
- LastUnknown), NewMode, Response) :-
+ LastUnknown), DefaultSearchMode, NewMode, Response) :-
follow_subterm_end_search(Store, !SearchSpace, LastUnknown, SuspectId,
- ArgPos, TermPath, NewMode, Response).
+ ArgPos, TermPath, DefaultSearchMode, NewMode, Response).
search(Store, !SearchSpace, binary(PathArray, Top - Bottom, LastTested),
- NewMode, Response) :-
+ DefaultSearchMode, NewMode, Response) :-
binary_search(Store, PathArray, Top, Bottom, LastTested, !SearchSpace,
- NewMode, Response).
+ DefaultSearchMode, NewMode, Response).
+
+search(Store, !SearchSpace, divide_and_query, _, NewMode, Response) :-
+ divide_and_query_search(Store, !SearchSpace, Response, NewMode).
:- pred top_down_search(S::in, search_space(T)::in, search_space(T)::out,
- search_response::out, search_mode::out) is det <= mercury_edt(S, T).
+ search_response::out) is det <= mercury_edt(S, T).
-top_down_search(Store, !SearchSpace, Response, NewMode) :-
+top_down_search(Store, !SearchSpace, Response) :-
%
% If there's no root yet (because the oracle hasn't asserted any nodes
% are erroneous yet) then use the topmost suspect as a starting point.
@@ -533,16 +593,14 @@
SearchSpace1 = !:SearchSpace,
(
MaybeDescendent = yes(Unknown),
- Response = question(Unknown),
- NewMode = top_down
+ Response = question(Unknown)
;
MaybeDescendent = no,
(
choose_skipped_suspect(!.SearchSpace,
SkippedSuspect)
->
- Response = question(SkippedSuspect),
- NewMode = top_down
+ Response = question(SkippedSuspect)
;
throw(internal_error("top_down_search",
"no unknown or skipped suspects"))
@@ -563,8 +621,7 @@
(
pick_implicit_root(Store, !.SearchSpace, ImplicitRoot)
->
- Response = require_explicit_subtree(ImplicitRoot),
- NewMode = top_down
+ Response = require_explicit_subtree(ImplicitRoot)
;
throw(internal_error("top_down_search",
"first_unknown_descendent requires an "
@@ -577,11 +634,11 @@
:- pred follow_subterm_end_search(S::in, search_space(T)::in,
search_space(T)::out, maybe(suspect_id)::in, suspect_id::in,
- arg_pos::in, term_path::in, search_mode::out,
+ arg_pos::in, term_path::in, default_search_mode::in, search_mode::out,
search_response::out) is det <= mercury_edt(S, T).
follow_subterm_end_search(Store, !SearchSpace, LastUnknown, SuspectId, ArgPos,
- TermPath, NewMode, SearchResponse) :-
+ TermPath, DefaultSearchMode, NewMode, SearchResponse) :-
find_subterm_origin(Store, SuspectId, ArgPos, TermPath, !SearchSpace,
FindOriginResponse),
(
@@ -605,7 +662,8 @@
Unknown, NewMode)
;
LastUnknown = no,
- top_down_search(Store, !SearchSpace,
+ start_default_search(DefaultSearchMode,
+ Store, !SearchSpace,
SearchResponse, NewMode)
)
)
@@ -618,7 +676,8 @@
Unknown, NewMode)
;
LastUnknown = no,
- top_down_search(Store, !SearchSpace,
+ start_default_search(DefaultSearchMode,
+ Store, !SearchSpace,
SearchResponse, NewMode)
)
;
@@ -663,7 +722,8 @@
Unknown, NewMode)
;
LastUnknown = no,
- top_down_search(Store, !SearchSpace,
+ start_default_search(DefaultSearchMode,
+ Store, !SearchSpace,
SearchResponse, NewMode)
)
;
@@ -677,7 +737,7 @@
%
follow_subterm_end_search(Store, !SearchSpace,
NewLastUnknown, OriginId, OriginArgPos,
- OriginTermPath, NewMode,
+ OriginTermPath, DefaultSearchMode, NewMode,
SearchResponse)
)
).
@@ -713,11 +773,11 @@
).
:- pred binary_search(S::in, array(suspect_id)::in, int::in, int::in, int::in,
- search_space(T)::in, search_space(T)::out, search_mode::out,
- search_response::out) is det <= mercury_edt(S, T).
+ search_space(T)::in, search_space(T)::out, default_search_mode::in,
+ search_mode::out, search_response::out) is det <= mercury_edt(S, T).
-binary_search(Store, PathArray, Top, Bottom, LastTested, !SearchSpace, NewMode,
- Response) :-
+binary_search(Store, PathArray, Top, Bottom, LastTested, !SearchSpace,
+ DefaultSearchMode, NewMode, Response) :-
SuspectId = PathArray ^ elem(LastTested),
%
% Check what the result of the query about LastTested was and adjust
@@ -743,8 +803,9 @@
(
NewTop > NewBottom
->
- % Revert to top down search when binary search is over.
- top_down_search(Store, !SearchSpace, Response, NewMode)
+ % Revert to the default search mode when binary search is over.
+ start_default_search(DefaultSearchMode,
+ Store, !SearchSpace, Response, NewMode)
;
(
find_unknown_closest_to_middle(!.SearchSpace,
@@ -757,9 +818,9 @@
UnknownClosestToMiddle))
;
% No unknown suspects on the path, so revert to
- % top down search.
- top_down_search(Store, !SearchSpace, Response,
- NewMode)
+ % the default search strategy.
+ start_default_search(DefaultSearchMode,
+ Store, !SearchSpace, Response, NewMode)
)
).
@@ -810,3 +871,143 @@
OuterTop, OuterBottom, InnerTop - 1, InnerBottom + 1,
Unknown)
).
+
+:- pred divide_and_query_search(S::in, search_space(T)::in,
+ search_space(T)::out, search_response::out, search_mode::out) is det
+ <= mercury_edt(S, T).
+
+divide_and_query_search(Store, !SearchSpace, Response, NewMode) :-
+ %
+ % If there's no root yet (because the oracle hasn't asserted any nodes
+ % are erroneous yet), then use top-down search.
+ %
+ (
+ root(!.SearchSpace, RootId)
+ ->
+ NewMode = divide_and_query,
+ (
+ children(Store, RootId, !SearchSpace, Children)
+ ->
+ find_middle_weight(Store, Children, RootId, no,
+ !SearchSpace, Response)
+ ;
+ Response = require_explicit_subtree(RootId)
+ )
+ ;
+ top_down_search(Store, !SearchSpace, Response),
+ NewMode = divide_and_query
+ ).
+
+ % find_middle_weight(Store, SuspectIds, TopId, MaybeLastUnknown,
+ % !SearchSpace, Response).
+ % Find the suspect that splits the portion of the search space rooted
+ % at TopId into roughly equal portions by weight. SuspectIds is
+ % a list of suspects who's descendents should be searched.
+ % MaybeLastUnknown is the last node that was unknown in the search (
+ % if any).
+ %
+:- pred find_middle_weight(S::in, list(suspect_id)::in, suspect_id::in,
+ maybe(suspect_id)::in, search_space(T)::in,
+ search_space(T)::out, search_response::out)
+ is det <= mercury_edt(S, T).
+
+find_middle_weight(Store, [], _, MaybeLastUnknown, !SearchSpace, Response) :-
+ (
+ MaybeLastUnknown = yes(LastUnknown),
+ Response = question(LastUnknown)
+ ;
+ MaybeLastUnknown = no,
+ % This could happen when there were no unknown suspects
+ % encountered during the search, in which case we revert
+ % to top-down search.
+ top_down_search(Store, !SearchSpace, Response)
+ ).
+find_middle_weight(Store, [SuspectId | SuspectIds], TopId, MaybeLastUnknown,
+ !SearchSpace, Response) :-
+ Target = get_weight(!.SearchSpace, TopId) // 2,
+ %
+ % Find the heaviest suspect:
+ %
+ Weight = get_weight(!.SearchSpace, SuspectId),
+ list.foldl(max_weight(!.SearchSpace), SuspectIds,
+ {Weight, SuspectId}, {MaxWeight, Heaviest}),
+ (
+ MaxWeight > Target
+ ->
+ (
+ children(Store, Heaviest, !SearchSpace, Children)
+ ->
+ (
+ suspect_unknown(!.SearchSpace, Heaviest)
+ ->
+ NewMaybeLastUnknown = yes(Heaviest)
+ ;
+ NewMaybeLastUnknown = MaybeLastUnknown
+ ),
+ find_middle_weight(Store, Children, TopId,
+ NewMaybeLastUnknown, !SearchSpace, Response)
+ ;
+ Response = require_explicit_subtree(Heaviest)
+ )
+ ;
+ (
+ suspect_unknown(!.SearchSpace, Heaviest)
+ ->
+ Response = question(Heaviest)
+ ;
+ (
+ MaybeLastUnknown = yes(LastUnknown),
+ Response = question(LastUnknown)
+ ;
+ MaybeLastUnknown = no,
+ % Look deeper until we find an unknown:
+ (
+ children(Store, Heaviest, !SearchSpace, Children)
+ ->
+ find_middle_weight(Store, Children,
+ TopId, no, !SearchSpace,
+ Response)
+ ;
+ Response = require_explicit_subtree(
+ Heaviest)
+ )
+ )
+ )
+ ).
+
+:- pred max_weight(search_space(T)::in, suspect_id::in,
+ {int, suspect_id}::in, {int, suspect_id}::out)
+ is det.
+
+max_weight(SearchSpace, SuspectId, {PrevMax, PrevSuspectId},
+ {NewMax, NewSuspectId}) :-
+ Weight = get_weight(SearchSpace, SuspectId),
+ (
+ Weight > PrevMax
+ ->
+ NewMax = Weight,
+ NewSuspectId = SuspectId
+ ;
+ NewMax = PrevMax,
+ NewSuspectId = PrevSuspectId
+ ).
+
+ % Start doing a default search of the search space.
+ %
+:- pred start_default_search(default_search_mode::in, S::in,
+ search_space(T)::in, search_space(T)::out,
+ search_response::out, search_mode::out) is det <= mercury_edt(S, T).
+
+start_default_search(DefaultSearchMode, Store, !SearchSpace, SearchResponse,
+ NewMode) :-
+ (
+ DefaultSearchMode = top_down,
+ top_down_search(Store, !SearchSpace,
+ SearchResponse),
+ NewMode = top_down
+ ;
+ DefaultSearchMode = divide_and_query,
+ divide_and_query_search(Store,
+ !SearchSpace, SearchResponse,
+ NewMode)
+ ).
Index: browser/declarative_debugger.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/declarative_debugger.m,v
retrieving revision 1.43
diff -u -r1.43 declarative_debugger.m
--- browser/declarative_debugger.m 16 Dec 2004 00:12:38 -0000 1.43
+++ browser/declarative_debugger.m 16 Dec 2004 03:27:26 -0000
@@ -522,6 +522,36 @@
diagnoser_state_init_store(InStr, OutStr, Browser, Diagnoser) :-
diagnoser_state_init(map__init, InStr, OutStr, Browser, Diagnoser).
+:- pred set_default_search_mode(
+ mdb.declarative_analyser.default_search_mode::in,
+ diagnoser_state(trace_node_id)::in,
+ diagnoser_state(trace_node_id)::out) is det.
+
+:- pragma export(mdb.declarative_debugger.set_default_search_mode(in, in, out),
+ "MR_DD_decl_set_default_search_mode").
+
+set_default_search_mode(SearchMode, !Diagnoser) :-
+ Analyser0 = !.Diagnoser ^ analyser_state,
+ mdb.declarative_analyser.set_default_search_mode(SearchMode,
+ Analyser0, Analyser),
+ !:Diagnoser = !.Diagnoser ^ analyser_state := Analyser.
+
+:- func top_down_default_search_mode =
+ mdb.declarative_analyser.default_search_mode.
+
+top_down_default_search_mode = top_down.
+
+:- pragma export(top_down_default_search_mode = out,
+ "MR_DD_decl_top_down_default_search_mode").
+
+:- func divide_and_query_default_search_mode =
+ mdb.declarative_analyser.default_search_mode.
+
+divide_and_query_default_search_mode = divide_and_query.
+
+:- pragma export(divide_and_query_default_search_mode = out,
+ "MR_DD_decl_divide_and_query_default_search_mode").
+
% Export a monomorphic version of diagnosis/10, to make it
% easier to call from C code.
%
Index: browser/declarative_edt.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/declarative_edt.m,v
retrieving revision 1.2
diff -u -r1.2 declarative_edt.m
--- browser/declarative_edt.m 16 Dec 2004 00:12:38 -0000 1.2
+++ browser/declarative_edt.m 21 Dec 2004 11:25:52 -0000
@@ -11,9 +11,9 @@
% Search spaces are also defined as a layer on top of EDTs.
%
% The search space records extra information like which nodes have been
-% eliminated from the bug search and which nodes have been skipped or are
-% trusted and in future might also store information like the probability of
-% each node being buggy, based on some heursitic(s).
+% eliminated from the bug search, which nodes have been skipped or are
+% trusted, the weight of each node, and in future might also store information
+% like the probability of each node being buggy, based on some heursitic(s).
%
% The search space provides a consistent view of the debug tree - combining
% seperately generated EDT subtrees into one tree. Each node in the search
@@ -24,7 +24,7 @@
% only correspond to implicit roots when an explicit version of the EDT subtree
% rooted at the node has not yet been generated.
%
-% Every node in the EDT may not have a corresponing node in the search space:
+% Every node in the EDT may not have a corresponding node in the search space:
% nodes are only added to the search space when they are needed by a
% particular search algorithm.
%
@@ -126,7 +126,21 @@
% True if it is not possible to materialize any nodes
% above the given node.
%
- pred edt_topmost_node(S::in, T::in) is semidet
+ pred edt_topmost_node(S::in, T::in) is semidet,
+
+ % edt_weight(Store, Node, Weight, ExcessWeight).
+ % True if Weight is the weight of Node. ExcessWeight is
+ % some extra weight that should be added to the ancestors of
+ % Node because the sum of the weights of the Node and its
+ % siblings might otherwise be bigger than Node's parent's
+ % weight. For example if the number of events in descendent
+ % nodes is being used as a weight, then for a FAIL node
+ % some events may be repeated in siblings of the FAIL node.
+ % In this case the number of duplicate events should be
+ % returned in ExcessWeight so they can be added to the
+ % ancestors.
+ %
+ pred edt_weight(S::in, T::in, int::out, int::out) is det
].
:- type subterm_mode
@@ -190,7 +204,8 @@
% Creates a new search space containing just the one EDT node with
% an initial status of unknown.
%
-:- pred initialise_search_space(T::in, search_space(T)::out) is det.
+:- pred initialise_search_space(S::in, T::in, search_space(T)::out)
+ is det <= mercury_edt(S, T).
% The root of the search space is the root of the subtree of the EDT
% that we think contains a bug, based on information received so far.
@@ -237,8 +252,8 @@
% Marks the suspect correct and alls its decendents as pruned.
%
-:- pred assert_suspect_is_correct(suspect_id::in, search_space(T)::in,
- search_space(T)::out) is det.
+:- pred assert_suspect_is_correct(suspect_id::in,
+ search_space(T)::in, search_space(T)::out) is det.
% Marks the supect erroneous and marks the complement of the subtree
% rooted at the erroneous suspect as in_erroneous_subtree_complement.
@@ -248,13 +263,13 @@
% Marks the suspect inadmissible and alls its decendents as pruned.
%
-:- pred assert_suspect_is_inadmissible(suspect_id::in, search_space(T)::in,
- search_space(T)::out) is det.
+:- pred assert_suspect_is_inadmissible(suspect_id::in,
+ search_space(T)::in, search_space(T)::out) is det.
% Marks the suspect ignored.
%
-:- pred ignore_suspect(suspect_id::in, search_space(T)::in,
- search_space(T)::out) is det.
+:- pred ignore_suspect(S::in, suspect_id::in, search_space(T)::in,
+ search_space(T)::out) is det <= mercury_edt(S, T).
% Marks the suspect as skipped.
%
@@ -333,6 +348,10 @@
%
:- func get_edt_node(search_space(T), suspect_id) = T.
+ % Return the weight of the suspect.
+ %
+:- func get_weight(search_space(T), suspect_id) = int.
+
% Succeeds if the suspect has been marked correct or inadmissible
% or is the descendent of a suspect that was marked correct or
% inadmissible. Fails otherwise.
@@ -424,18 +443,22 @@
% Mark the root and it's non-ignored children as unknown.
% Throws an exception if the search space doesn't have a root.
%
-:- pred revise_root(search_space(T)::in, search_space(T)::out) is det.
+:- pred revise_root(S::in, search_space(T)::in, search_space(T)::out)
+ is det <= mercury_edt(S, T).
% Check the consistency of the search space and throw an exception
- % if it's not consistent. Used for debugging.
+ % if it's not consistent. Used for assertion checking during
+ % debugging.
%
-:- pred check_search_space_consistency(search_space(T)::in, string::in) is det.
+:- pred check_search_space_consistency(S::in, search_space(T)::in, string::in)
+ is det <= mercury_edt(S, T).
%-----------------------------------------------------------------------------%
:- implementation.
:- import_module exception, map, int, counter, std_util, string, bool, bimap.
+:- import_module float.
% A suspect is an edt node with some additional information relevant
% to the bug search.
@@ -466,7 +489,11 @@
% no then the children have not yet been
% explored. Children are only added to the
% search space when they are required.
- children :: maybe(list(suspect_id))
+ children :: maybe(list(suspect_id)),
+
+ % A weighting used for divide and query
+ % search.
+ weight :: int
).
:- type suspect_status
@@ -716,9 +743,9 @@
assert_suspect_is_valid(Status, SuspectId, !SearchSpace) :-
lookup_suspect(!.SearchSpace, SuspectId, Suspect),
- map.set(!.SearchSpace ^ store, SuspectId, Suspect ^ status :=
- Status, Store),
- !:SearchSpace = !.SearchSpace ^ store := Store,
+ 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),
@@ -729,6 +756,9 @@
adjust_unexplored_leaves(yes(Suspect ^ status), Status,
!SearchSpace)
),
+ % Remove the suspect's weight from it's ancestors, since its weight is
+ % now zero.
+ add_weight_to_ancestors(SuspectId, - Suspect ^ weight, !SearchSpace),
%
% If the suspect was erroneous or excluded because of another erronoeus
% suspect, then we should update the complement of the subtree rooted
@@ -770,32 +800,24 @@
adjust_unexplored_leaves(yes(Suspect ^ status), erroneous,
!SearchSpace)
;
- Suspect ^ children = yes(Children),
- %
- % If the suspect was correct, inadmissible or pruned then we
- % should make all the descendents unknown again.
- %
- (
- excluded_subtree(Suspect ^ status, yes)
- ->
- list.foldl(propagate_status_downwards(unknown,
- [correct, inadmissible]), Children,
- !SearchSpace)
- ;
- true
- )
+ Suspect ^ children = yes(_)
),
- propagate_status_upwards(in_erroneous_subtree_complement, [erroneous],
- SuspectId, _, !SearchSpace),
+ propagate_status_upwards(in_erroneous_subtree_complement,
+ [erroneous, correct, inadmissible], SuspectId, _,
+ !SearchSpace),
!:SearchSpace = !.SearchSpace ^ root := yes(SuspectId).
-ignore_suspect(SuspectId, !SearchSpace) :-
+ignore_suspect(Store, SuspectId, !SearchSpace) :-
lookup_suspect(!.SearchSpace, SuspectId, Suspect),
- map.set(!.SearchSpace ^ store, SuspectId, Suspect ^ status :=
- ignored, Store),
adjust_unknown_count(yes(Suspect ^ status), ignored, !SearchSpace),
- !:SearchSpace = !.SearchSpace ^ store := Store.
-
+ calc_suspect_weight(Store, Suspect ^ edt_node, Suspect ^ children,
+ ignored, !.SearchSpace, Weight, _),
+ map.set(!.SearchSpace ^ store, SuspectId,
+ (Suspect^ status := ignored) ^ weight := Weight, SuspectStore),
+ !:SearchSpace = !.SearchSpace ^ store := SuspectStore,
+ add_weight_to_ancestors(SuspectId, Weight - Suspect ^ weight,
+ !SearchSpace).
+
skip_suspect(SuspectId, !SearchSpace) :-
lookup_suspect(!.SearchSpace, SuspectId, Suspect),
counter.allocate(N, !.SearchSpace ^ skip_counter, SkipCounter),
@@ -804,27 +826,44 @@
skipped(N), Store),
!:SearchSpace = !.SearchSpace ^ store := Store.
-revise_root(!SearchSpace) :-
+revise_root(Store, !SearchSpace) :-
(
!.SearchSpace ^ root = yes(RootId),
force_propagate_status_downwards(unknown,
- [correct, inadmissible], RootId, Leaves, !SearchSpace),
- list.foldl(force_propagate_status_downwards(unknown, [correct,
- inadmissible]), Leaves, !SearchSpace),
- propagate_status_upwards(unknown, [erroneous], RootId, Lowest,
+ [correct, inadmissible], RootId, StopSuspects,
!SearchSpace),
- (
- suspect_erroneous(!.SearchSpace, Lowest)
- ->
+ list.foldl(force_propagate_status_downwards(unknown, [correct,
+ inadmissible]), StopSuspects, !SearchSpace),
+ propagate_status_upwards(unknown, [erroneous, correct,
+ inadmissible], RootId, Lowest, !SearchSpace),
+ ( suspect_erroneous(!.SearchSpace, Lowest) ->
!:SearchSpace = !.SearchSpace ^ root := yes(Lowest)
;
!:SearchSpace = !.SearchSpace ^ root := no
- )
+ ),
+ %
+ % Recompute the suspect weights from the bottom up.
+ %
+ map.keys(!.SearchSpace ^ store, AllSuspects),
+ list.filter(suspect_is_leaf(!.SearchSpace), AllSuspects,
+ Leaves),
+ recalc_weights_upto_ancestor(Store, Lowest, Leaves,
+ !SearchSpace)
;
!.SearchSpace ^ root = no,
throw(internal_error("revise_root", "no root"))
).
-
+
+ % True if the suspect is a leaf node in the search space (i.e. it has
+ % either `no' or `yes([])' in its children field.
+ %
+:- pred suspect_is_leaf(search_space(T)::in, suspect_id::in)
+ is semidet.
+
+suspect_is_leaf(SearchSpace, SuspectId) :-
+ lookup_suspect(SearchSpace, SuspectId, Suspect),
+ (Suspect ^ children = no ; Suspect ^ children = yes([])).
+
suspect_depth(SearchSpace, SuspectId) = Suspect ^ depth :-
lookup_suspect(SearchSpace, SuspectId, Suspect).
@@ -979,24 +1018,22 @@
"couldn't find suspect"))
).
- % propagate_status_downwards(Status, StopStatusSet, SuspectId, Leaves,
- % !SearchSpace).
+ % propagate_status_downwards(Status, StopStatusSet, SuspectId,
+ % StopSuspects, !SearchSpace).
% Sets the status of SuspectId and all it's descendents to Status.
% If a descendent (including the suspect) already has a status in
% StopStatusSet then propagate_status_downwards won't update any
% further descendents. The list of all the children of the lowest
- % updated suspects is returned in Leaves.
+ % updated suspects is returned in StopSuspects.
%
:- pred propagate_status_downwards(suspect_status::in,
list(suspect_status)::in, suspect_id::in, list(suspect_id)::out,
search_space(T)::in, search_space(T)::out) is det.
- % An accumulator version of propagate_status_downwards.
- %
-propagate_status_downwards(Status, StopStatusSet, SuspectId, Leaves,
+propagate_status_downwards(Status, StopStatusSet, SuspectId, StopSuspects,
!SearchSpace) :-
propagate_status_downwards(Status, StopStatusSet, SuspectId, [],
- Leaves, !SearchSpace).
+ StopSuspects, !SearchSpace).
% A version of propagate_status_downwards which doesn't return leaves.
%
@@ -1008,12 +1045,14 @@
propagate_status_downwards(Status, StopStatusSet, SuspectId, _,
!SearchSpace).
+ % An accumulator version of propagate_status_downwards.
+ %
:- pred propagate_status_downwards(suspect_status::in,
list(suspect_status)::in, suspect_id::in,
list(suspect_id)::in, list(suspect_id)::out,
search_space(T)::in, search_space(T)::out) is det.
-propagate_status_downwards(Status, StopStatusSet, SuspectId, !Leaves,
+propagate_status_downwards(Status, StopStatusSet, SuspectId, !StopSuspects,
!SearchSpace) :-
lookup_suspect(!.SearchSpace, SuspectId, Suspect),
(
@@ -1025,7 +1064,7 @@
(
Suspect ^ children = yes(Children),
list.foldl2(propagate_status_downwards(Status,
- StopStatusSet), Children, !Leaves,
+ StopStatusSet), Children, !StopSuspects,
!SearchSpace)
;
Suspect ^ children = no,
@@ -1035,7 +1074,7 @@
adjust_unknown_count(yes(Suspect ^ status), Status,
!SearchSpace)
;
- list.cons(SuspectId, !Leaves)
+ list.cons(SuspectId, !StopSuspects)
).
% force_propagate_status_downwards is like propagate_status_downwards,
@@ -1055,8 +1094,8 @@
list(suspect_status)::in, suspect_id::in, list(suspect_id)::out,
search_space(T)::in, search_space(T)::out) is det.
-force_propagate_status_downwards(Status, StopStatusSet, SuspectId, Leaves,
- !SearchSpace) :-
+force_propagate_status_downwards(Status, StopStatusSet, SuspectId,
+ StopSuspects, !SearchSpace) :-
lookup_suspect(!.SearchSpace, SuspectId, Suspect),
map.set(!.SearchSpace ^ store, SuspectId,
Suspect ^ status := Status, Store),
@@ -1064,12 +1103,12 @@
(
Suspect ^ children = yes(Children),
list.foldl2(propagate_status_downwards(Status, StopStatusSet),
- Children, [], Leaves, !SearchSpace)
+ Children, [], StopSuspects, !SearchSpace)
;
Suspect ^ children = no,
adjust_unexplored_leaves(yes(Suspect ^ status), Status,
!SearchSpace),
- Leaves = []
+ StopSuspects = []
),
adjust_unknown_count(yes(Suspect ^ status), Status, !SearchSpace).
@@ -1152,7 +1191,7 @@
true
).
-check_search_space_consistency(SearchSpace, Context) :-
+check_search_space_consistency(Store, SearchSpace, Context) :-
(
SearchSpace ^ unknown_count \= calc_num_unknown(SearchSpace)
->
@@ -1169,9 +1208,157 @@
++ string(SearchSpace) ++ "\n Context is:\n" ++
Context))
;
+ check_search_space_weights(Store, SearchSpace)
+ ->
+ % check_search_space_weights will never actually fail, but
+ % will throw an exception if the weights are inconsistent.
+ true
+ ;
true
).
-
+
+ % Calculate the weight of a suspect based on the weights of its
+ % children. If the node is correct or inadmissible then the weight is
+ % zero. If the node is ignored then the weight is the sum of the
+ % weights of the children plus the sum of the excess weights of the
+ % children. Otherwise the weight is the original weight of the node
+ % as reported by edt_weight/4 minus the original weights of the
+ % children as reported by edt_weight/4 plus the current weight of
+ % the children plus any excess weight in the children.
+ %
+:- pred calc_suspect_weight(S::in, T::in, maybe(list(suspect_id))::in,
+ suspect_status::in, search_space(T)::in, int::out, int::out)
+ is det <= mercury_edt(S, T).
+
+calc_suspect_weight(Store, Node, MaybeChildren, Status, SearchSpace, Weight,
+ ExcessWeight) :-
+ (
+ ( Status = correct
+ ; Status = inadmissible
+ )
+ ->
+ Weight = 0,
+ ExcessWeight = 0
+ ;
+ edt_weight(Store, Node, OriginalWeight, ExcessWeight),
+ (
+ MaybeChildren = no,
+ Weight = OriginalWeight
+ ;
+ MaybeChildren = yes(Children),
+ list.map(lookup_suspect(SearchSpace), Children,
+ ChildrenSuspects),
+ ChildrenNodes = list.map(
+ func(S) = N :- N = S ^ edt_node,
+ ChildrenSuspects),
+ list.foldl2(add_original_weight(Store),
+ ChildrenNodes, 0, ChildrenOriginalWeight,
+ 0, ChildrenExcess),
+ list.foldl(add_existing_weight, ChildrenSuspects, 0,
+ ChildrenWeight),
+ (
+ Status = ignored
+ ->
+ Weight = ChildrenWeight + ChildrenExcess
+ ;
+ Weight = OriginalWeight -
+ ChildrenOriginalWeight + ChildrenWeight
+ + ChildrenExcess
+ )
+ )
+ ).
+
+ % Add the given weight to the ancestors of the given suspect
+ % (excluding the given suspect) until an erroneous node is encountered
+ % (the erroneous node is also updated).
+ %
+:- pred add_weight_to_ancestors(suspect_id::in, int::in,
+ search_space(T)::in, search_space(T)::out) is det.
+
+add_weight_to_ancestors(SuspectId, Weight, !SearchSpace) :-
+ (
+ %
+ % Stop if the weight is 0, if the node is erroneous or
+ % if there is no parent.
+ %
+ Weight \= 0,
+ lookup_suspect(!.SearchSpace, SuspectId, Suspect),
+ Suspect ^ parent = yes(ParentId)
+ ->
+ lookup_suspect(!.SearchSpace, ParentId, Parent),
+ map.set(!.SearchSpace ^ store, ParentId,
+ Parent ^ weight := Parent ^ weight + Weight,
+ SuspectStore),
+ !:SearchSpace = !.SearchSpace ^ store := SuspectStore,
+ excluded_complement(Parent ^ status, ExcludedComplement),
+ (
+ ExcludedComplement = yes
+ ;
+ ExcludedComplement = no,
+ add_weight_to_ancestors(ParentId, Weight, !SearchSpace)
+ )
+ ;
+ true
+ ).
+
+:- pred add_original_weight(S::in, T::in, int::in, int::out, int::in, int::out)
+ is det <= mercury_edt(S, T).
+
+add_original_weight(Store, Node, Prev, Prev + Weight, PrevExcess,
+ PrevExcess + Excess) :-
+ edt_weight(Store, Node, Weight, Excess).
+
+:- pred add_existing_weight(suspect(T)::in, int::in, int::out) is det.
+
+add_existing_weight(Suspect, Prev, Prev + Suspect ^ weight).
+
+ % recalc_weights_upto_ancestor(Store, Ancestor, Suspects, !SearchSpace)
+ % Recalculate the weights of the suspects in Suspects and all their
+ % ancestors below Ancestor. Ancestor must be a common ancestor
+ % of all the suspects in Suspects.
+ %
+:- pred recalc_weights_upto_ancestor(S::in, suspect_id::in,
+ list(suspect_id)::in, search_space(T)::in, search_space(T)::out)
+ is det <= mercury_edt(S, T).
+
+recalc_weights_upto_ancestor(Store, Ancestor, SuspectIds, !SearchSpace) :-
+ recalc_weights_and_get_parents(Store, SuspectIds, [], Parents,
+ !SearchSpace),
+ list.filter(unify(Ancestor), Parents, _, FilteredParents),
+ (
+ FilteredParents = [_ | _],
+ list.sort_and_remove_dups(FilteredParents, SortedParents),
+ recalc_weights_upto_ancestor(Store, Ancestor, SortedParents,
+ !SearchSpace)
+ ;
+ FilteredParents = [],
+ recalc_weights_and_get_parents(Store, [Ancestor], [], _,
+ !SearchSpace)
+ ).
+
+:- pred recalc_weights_and_get_parents(S::in, list(suspect_id)::in,
+ list(suspect_id)::in, list(suspect_id)::out,
+ search_space(T)::in, search_space(T)::out) is det <= mercury_edt(S, T).
+
+recalc_weights_and_get_parents(_, [], Parents, Parents, !SearchSpace).
+recalc_weights_and_get_parents(Store, [SuspectId | SuspectIds], PrevParents,
+ Parents, !SearchSpace) :-
+ lookup_suspect(!.SearchSpace, SuspectId, Suspect),
+ calc_suspect_weight(Store, Suspect ^ edt_node, Suspect ^ children,
+ Suspect ^ status, !.SearchSpace, Weight, _),
+ map.set(!.SearchSpace ^ store, SuspectId,
+ Suspect ^ weight := Weight, SuspectStore),
+ !:SearchSpace = !.SearchSpace ^ store := SuspectStore,
+ (
+ Suspect ^ parent = yes(ParentId),
+ NewPrevParents = [ParentId | PrevParents]
+ ;
+ Suspect ^ parent = no,
+ NewPrevParents = PrevParents
+ ),
+ recalc_weights_and_get_parents(Store, SuspectIds, NewPrevParents,
+ Parents, !SearchSpace).
+
% Work out the number of unknown suspects in the search space.
% Used for assertion checking.
:- func calc_num_unknown(search_space(T)) = int.
@@ -1179,7 +1366,7 @@
calc_num_unknown(SearchSpace) = NumUnknown :-
Suspects = map.values(SearchSpace ^ store),
list.filter(
- ( pred(suspect(_, _, Status, _, _)::in) is semidet :-
+ ( pred(suspect(_, _, Status, _, _, _)::in) is semidet :-
questionable(Status, yes)
), Suspects, Questionable),
NumUnknown = list.length(Questionable).
@@ -1191,11 +1378,59 @@
calc_num_unexplored(SearchSpace) = NumUnexplored :-
Suspects = map.values(SearchSpace ^ store),
list.filter(
- ( pred(suspect(_, _, Status, _, no)::in) is semidet :-
+ ( pred(suspect(_, _, Status, _, no, _)::in) is semidet :-
in_buggy_subtree(Status, yes)
), Suspects, Unexplored),
NumUnexplored = list.length(Unexplored).
+ % Check that the weights in the search space are correct and throw
+ % an exception if they aren't.
+ %
+:- pred check_search_space_weights(S::in, search_space(T)::in)
+ is semidet <= mercury_edt(S, T).
+
+check_search_space_weights(Store, SearchSpace) :-
+ ( root(SearchSpace, RootId) ->
+ check_search_space_weights(Store, RootId, SearchSpace)
+ ;
+ topmost_det(SearchSpace, TopMostId),
+ check_search_space_weights(Store, TopMostId, SearchSpace)
+ ).
+
+ % Check that the weights are correct from the given suspect down.
+ %
+:- pred check_search_space_weights(S::in, suspect_id::in, search_space(T)::in)
+ is semidet <= mercury_edt(S, T).
+
+check_search_space_weights(Store, SuspectId, SearchSpace) :-
+ lookup_suspect(SearchSpace, SuspectId, Suspect),
+ calc_suspect_weight(Store, Suspect ^ edt_node, Suspect ^ children,
+ Suspect ^ status, SearchSpace, Weight, _),
+ (
+ Weight = Suspect ^ weight,
+ Weight >= 0
+ ->
+ (
+ Suspect ^ children = yes(Children),
+ in_buggy_subtree(Suspect ^ status, yes)
+ ->
+ all [Child] (
+ member(Child, Children)
+ =>
+ check_search_space_weights(Store, Child,
+ SearchSpace)
+ )
+ ;
+ true
+ )
+ ;
+ throw(internal_error("check_search_space_weights",
+ "Weights not consistent for suspect id " ++
+ int_to_string(SuspectId) ++ ", Suspect = " ++
+ string(Suspect) ++ " Calculated weight = " ++
+ int_to_string(Weight)))
+ ).
+
% propagate_status_upwards(Status, StopStatusSet, SuspectId, Lowest,
% !SearchSpace)
% Marks all suspects not in the subtree rooted at SuspectId
@@ -1273,42 +1508,68 @@
% the given suspect. The suspect_ids for the new suspects will
% also be returned.
%
-:- pred add_children(list(T)::in, suspect_id::in, suspect_status::in,
+:- pred add_children(S::in, list(T)::in, suspect_id::in, suspect_status::in,
search_space(T)::in, search_space(T)::out, list(suspect_id)::out)
- is det.
+ is det <= mercury_edt(S, T).
-add_children(EDTChildren, SuspectId, Status, !SearchSpace, Children) :-
+add_children(Store, EDTChildren, SuspectId, Status, !SearchSpace, Children) :-
Counter0 = !.SearchSpace ^ suspect_id_counter,
- lookup_suspect(!.SearchSpace, SuspectId, Suspect),
- add_children_2(EDTChildren, SuspectId, Status, Suspect ^ depth + 1,
+ lookup_suspect(!.SearchSpace, SuspectId, Suspect0),
+ add_children_2(Store, EDTChildren, SuspectId, Status,
+ Suspect0 ^ depth + 1,
!SearchSpace, Counter0, Counter, Children),
!:SearchSpace = !.SearchSpace ^ suspect_id_counter := Counter,
- map.set(!.SearchSpace ^ store, SuspectId,
- Suspect ^ children := yes(Children), Store),
- !:SearchSpace = !.SearchSpace ^ store := Store,
+ % Lookup the suspect again, since it's weight may have changed.
+ lookup_suspect(!.SearchSpace, SuspectId, Suspect),
+ %
+ % Recalc the weight if the suspect is ignored. This wouldn't have
+ % been done by ignore_suspect/3 since the children wouldn't have been
+ % available.
+ %
+ (
+ Suspect ^ status = ignored
+ ->
+ calc_suspect_weight(Store, Suspect ^ edt_node, yes(Children),
+ ignored, !.SearchSpace, Weight, _),
+ map.set(!.SearchSpace ^ store, SuspectId,
+ (Suspect ^ weight := Weight)
+ ^ children := yes(Children), SuspectStore),
+ !:SearchSpace = !.SearchSpace ^ store := SuspectStore,
+ add_weight_to_ancestors(SuspectId, Weight - Suspect ^ weight,
+ !SearchSpace)
+ ;
+ map.set(!.SearchSpace ^ store, SuspectId,
+ Suspect ^ children := yes(Children), SuspectStore),
+ !:SearchSpace = !.SearchSpace ^ store := SuspectStore
+ ),
decrement_unexplored_leaves(Suspect ^ status, !SearchSpace).
-:- pred add_children_2(list(T)::in, suspect_id::in, suspect_status::in,
+:- 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,
- counter::out, list(suspect_id)::out) is det.
+ counter::out, list(suspect_id)::out) is det <= mercury_edt(S, T).
-add_children_2([], _, _, _, SearchSpace, SearchSpace, Counter, Counter, []).
+add_children_2(_, [], _, _, _, SearchSpace, SearchSpace, Counter, Counter, []).
-add_children_2([EDTChild | EDTChildren], SuspectId, Status, Depth,
+add_children_2(Store, [EDTChild | EDTChildren], SuspectId, Status, Depth,
!SearchSpace, !Counter, Children) :-
allocate(NextId, !Counter),
+ calc_suspect_weight(Store, EDTChild, no, Status, !.SearchSpace, Weight,
+ ExcessWeight),
map.det_insert(!.SearchSpace ^ store, NextId,
- suspect(yes(SuspectId), EDTChild, Status, Depth,
- no), Store),
- !:SearchSpace = !.SearchSpace ^ store := Store,
+ suspect(yes(SuspectId), EDTChild, Status, Depth, no, Weight),
+ 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(EDTChildren, SuspectId, Status, Depth,
+ add_children_2(Store, EDTChildren, SuspectId, Status, Depth,
!SearchSpace, !Counter, OtherChildren),
Children = [NextId | OtherChildren].
-initialise_search_space(Node, SearchSpace) :-
- map.set(init, 0, suspect(no, Node, unknown, 0, no), SuspectStore),
+initialise_search_space(Store, Node, SearchSpace) :-
+ edt_weight(Store, Node, Weight, _),
+ 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).
@@ -1383,8 +1644,10 @@
NewTopMostStatus = new_parent_status(
OldTopMost ^ status),
NewTopMostDepth = OldTopMost ^ depth - 1,
+ % We will update the weight below, so for now we
+ % just use 0.
NewTopMost = suspect(no, NewTopMostEDTNode,
- NewTopMostStatus, NewTopMostDepth, no),
+ NewTopMostStatus, NewTopMostDepth, no, 0),
some [!Counter, !SuspectStore] (
!:Counter = !.SearchSpace ^ suspect_id_counter,
counter.allocate(NewTopMostId, !Counter),
@@ -1398,13 +1661,15 @@
!.SuspectStore
),
SiblingStatus = new_child_status(NewTopMostStatus),
- add_children(append(LeftChildren, RightChildren),
- NewTopMostId, SiblingStatus, !SearchSpace,
- ChildrenIds),
+ add_children(Store,
+ append(LeftChildren, RightChildren),
+ NewTopMostId, SiblingStatus,
+ !SearchSpace, ChildrenIds),
%
% Adjust the unexplored leaves count since the new top
- % most node was added with no children.
+ % most node was added with no children (so add_children
+ % would have incorrectly subtracted 1 from the count).
%
adjust_unexplored_leaves(no, NewTopMostStatus,
!SearchSpace),
@@ -1424,11 +1689,20 @@
throw(internal_error("insert_new_topmost_node",
"invalid position"))
),
+
+ calc_suspect_weight(Store, NewTopMostEDTNode,
+ yes(NewTopMostChildrenIds), NewTopMostStatus,
+ !.SearchSpace, Weight, _),
some [!SuspectStore] (
!:SuspectStore = !.SearchSpace ^ store,
- map.set(!.SuspectStore, NewTopMostId,
+ NewTopMostWithCorrectChildren =
NewTopMost ^ children :=
yes(NewTopMostChildrenIds),
+ NewTopMostWithCorrectWeight =
+ NewTopMostWithCorrectChildren
+ ^ weight := Weight,
+ map.set(!.SuspectStore, NewTopMostId,
+ NewTopMostWithCorrectWeight,
!:SuspectStore),
map.set(!.SuspectStore, OldTopMostId,
OldTopMost ^ parent :=
@@ -1446,7 +1720,6 @@
throw(internal_error("insert_new_topmost_node",
"couldn't find event number"))
)
-
;
throw(internal_error("insert_new_topmost_node",
"couldn't get new topmost node's children"))
@@ -1469,6 +1742,10 @@
lookup_suspect(SearchSpace, SuspectId, Suspect),
Node = Suspect ^ edt_node.
+get_weight(SearchSpace, SuspectId) = Weight :-
+ lookup_suspect(SearchSpace, SuspectId, Suspect),
+ Weight = Suspect ^ weight.
+
% Return the status of the suspect.
:- func get_status(search_space(T), suspect_id) = suspect_status.
@@ -1488,7 +1765,7 @@
Suspect ^ children = no,
edt_children(Store, Suspect ^ edt_node, EDTChildren),
NewStatus = new_child_status(Suspect ^ status),
- add_children(EDTChildren, SuspectId, NewStatus,
+ add_children(Store, EDTChildren, SuspectId, NewStatus,
!SearchSpace, Children)
).
Index: browser/declarative_execution.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/declarative_execution.m,v
retrieving revision 1.29
diff -u -r1.29 declarative_execution.m
--- browser/declarative_execution.m 16 Dec 2004 00:12:38 -0000 1.29
+++ browser/declarative_execution.m 17 Dec 2004 02:29:34 -0000
@@ -75,8 +75,10 @@
; redo(
redo_preceding :: R,
% Preceding event.
- redo_exit :: R
+ redo_exit :: R,
% EXIT event.
+ redo_event :: event_number
+ % REDO event number.
)
; fail(
fail_preceding :: R,
@@ -307,7 +309,7 @@
:- pred call_node_from_id(S, R, trace_node(R)) <= annotated_trace(S, R).
:- mode call_node_from_id(in, in, out(trace_node_call)) is det.
-:- inst trace_node_redo ---> redo(ground, ground).
+:- inst trace_node_redo ---> redo(ground, ground, ground).
% maybe_redo_node_from_id/3 fails if the argument is a
% NULL reference.
@@ -651,7 +653,7 @@
Node = fail(_, _, _, _),
find_prev_contour(Store, Node, Prec).
step_left_in_contour(Store, Node) = Prec :-
- Node = redo(_, _),
+ Node = redo(_, _, _),
find_prev_contour(Store, Node, Prec).
step_left_in_contour(Store, Node) = Prec :-
Node = neg_fail(_, _),
@@ -666,13 +668,13 @@
:- inst trace_node_reverse
---> fail(ground, ground, ground, ground)
- ; redo(ground, ground)
+ ; redo(ground, ground, ground)
; neg_fail(ground, ground).
find_prev_contour(Store, fail(_, Call, _, _), OnContour) :-
call_node_from_id(Store, Call, CallNode),
OnContour = CallNode ^ call_preceding.
-find_prev_contour(Store, redo(_, Exit), OnContour) :-
+find_prev_contour(Store, redo(_, Exit, _), OnContour) :-
exit_node_from_id(Store, Exit, ExitNode),
OnContour = ExitNode ^ exit_preceding.
find_prev_contour(Store, neg_fail(_, Neg), OnContour) :-
@@ -694,7 +696,7 @@
step_over_redo_or_call(Store, Call, MaybeRedo).
step_in_stratum(Store, excp(_, Call, MaybeRedo, _, _)) =
step_over_redo_or_call(Store, Call, MaybeRedo).
-step_in_stratum(Store, redo(_, Exit)) = Next :-
+step_in_stratum(Store, redo(_, Exit, _)) = Next :-
exit_node_from_id(Store, Exit, ExitNode),
Next = ExitNode ^ exit_preceding.
step_in_stratum(_, switch(Next, _)) = Next.
@@ -730,7 +732,7 @@
(
maybe_redo_node_from_id(Store, MaybeRedo, Redo)
->
- Redo = redo(Next, _)
+ Redo = redo(Next, _, _)
;
call_node_from_id(Store, Call, CallNode),
Next = CallNode ^ call_preceding
@@ -758,7 +760,7 @@
maybe_redo_node_from_id(Store, NodeId, Node) :-
trace_node_from_id(Store, NodeId, Node0),
(
- Node0 = redo(_, _)
+ Node0 = redo(_, _, _)
->
Node = Node0
;
@@ -950,7 +952,7 @@
trace_node_port(call(_, _, _, _, _, _, _, _, _)) = call.
trace_node_port(exit(_, _, _, _, _, _)) = exit.
-trace_node_port(redo(_, _)) = redo.
+trace_node_port(redo(_, _, _)) = redo.
trace_node_port(fail(_, _, _, _)) = fail.
trace_node_port(excp(_, _, _, _, _)) = exception.
trace_node_port(switch(_, _)) = switch.
@@ -972,7 +974,7 @@
trace_node_path(_, call(_, _, _, _, _, _, _, P, _)) = P.
trace_node_path(_, exit(_, _, _, _, _, _)) = "".
-trace_node_path(_, redo(_, _)) = "".
+trace_node_path(_, redo(_, _, _)) = "".
trace_node_path(_, fail(_, _, _, _)) = "".
trace_node_path(_, excp(_, _, _, _, _)) = "".
trace_node_path(_, switch(_, P)) = P.
@@ -1012,7 +1014,7 @@
:- pragma export(trace_node_call(in, in, out), "MR_DD_trace_node_call").
trace_node_call(_, exit(_, Call, _, _, _, _), Call).
-trace_node_call(S, redo(_, Exit), Call) :-
+trace_node_call(S, redo(_, Exit, _), Call) :-
exit_node_from_id(S, Exit, ExitNode),
Call = ExitNode ^ exit_call.
trace_node_call(_, fail(_, Call, _, _), Call).
@@ -1110,12 +1112,12 @@
construct_exit_node(Preceding, Call, MaybeRedo, Atom, EventNo, IoSeqNum)
= exit(Preceding, Call, MaybeRedo, Atom, EventNo, IoSeqNum).
-:- func construct_redo_node(trace_node_id, trace_node_id)
+:- func construct_redo_node(trace_node_id, trace_node_id, event_number)
= trace_node(trace_node_id).
-:- pragma export(construct_redo_node(in, in) = out,
+:- pragma export(construct_redo_node(in, in, in) = out,
"MR_DD_construct_redo_node").
-construct_redo_node(Preceding, Exit) = redo(Preceding, Exit).
+construct_redo_node(Preceding, Exit, Event) = redo(Preceding, Exit, Event).
:- func construct_fail_node(trace_node_id, trace_node_id, trace_node_id,
event_number) = trace_node(trace_node_id).
@@ -1372,7 +1374,7 @@
preceding_node(call(P, _, _, _, _, _, _, _, _)) = P.
preceding_node(exit(P, _, _, _, _, _)) = P.
-preceding_node(redo(P, _)) = P.
+preceding_node(redo(P, _, _)) = P.
preceding_node(fail(P, _, _, _)) = P.
preceding_node(excp(P, _, _, _, _)) = P.
preceding_node(switch(P, _)) = P.
Index: browser/declarative_tree.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/declarative_tree.m,v
retrieving revision 1.11
diff -u -r1.11 declarative_tree.m
--- browser/declarative_tree.m 16 Dec 2004 00:12:39 -0000 1.11
+++ browser/declarative_tree.m 21 Dec 2004 11:30:35 -0000
@@ -1,5 +1,5 @@
%-----------------------------------------------------------------------------%
-% Copyright (C) 2002-2004 The University of Melbourne.
+% Copyright (C) 2002-2003 The University of Melbourne.
% This file may only be copied under the terms of the GNU Library General
% Public License - see the file COPYING.LIB in the Mercury distribution.
%-----------------------------------------------------------------------------%
@@ -60,7 +60,8 @@
pred(edt_subterm_mode/5) is trace_subterm_mode,
pred(edt_is_implicit_root/2) is trace_is_implicit_root,
pred(edt_same_nodes/3) is trace_same_event_numbers,
- pred(edt_topmost_node/2) is trace_topmost_node
+ pred(edt_topmost_node/2) is trace_topmost_node,
+ pred(edt_weight/4) is trace_weight
].
%-----------------------------------------------------------------------------%
@@ -152,7 +153,7 @@
get_answers(IoActionMap, Store, RedoId, DeclAtoms0, DeclAtoms) :-
(
- maybe_redo_node_from_id(Store, RedoId, redo(_, ExitId))
+ maybe_redo_node_from_id(Store, RedoId, redo(_, ExitId, _))
->
exit_node_from_id(Store, ExitId, ExitNode),
NextId = ExitNode ^ exit_prev_redo,
@@ -284,6 +285,94 @@
trace_is_implicit_root(wrap(Store), dynamic(Ref)) :-
get_edt_call_node(Store, Ref, CallId),
\+ not_at_depth_limit(Store, CallId).
+
+:- pred trace_weight(wrap(S)::in, edt_node(R)::in, int::out, int::out)
+ is det <= annotated_trace(S, R).
+
+trace_weight(Store, NodeId, Weight, ExcessWeight) :-
+ node_events(Store, NodeId, 0, Weight, no, 0, 0, ExcessWeight).
+
+ % Conservatively guess the number of events in the descendents of the
+ % call corresponding to the given final event plus the number of
+ % internal body events for the call. Also return the number of events
+ % that could be duplicated in siblings of the node in the EDT if the
+ % node is a FAIL event.
+ % We include all the events between the final event and the last
+ % REDO before the final event, plus all the events between previous
+ % EXITs and REDOs and the initial CALL. For EXIT and EXCP events
+ % this is an over approximation, but we can't know which events
+ % will be included in descendent contours when those descendent
+ % events are in unmaterialized portions of the annotated trace.
+ %
+ % node_events(Store, Node, PrevEvents, Events, RecordDups,
+ % DupFactor, PrevDupEvents, DupEvents)
+ % True iff Events is the (conservative approximation of) the number of
+ % descendent events of Node and DupEvents is the number of events that
+ % could be duplicated in siblings. PrevEvents and PrevDupEvents are
+ % accumlators which should initially be zero. RecordDups keeps track
+ % of whether the final node was a FAIL or not - duplicates need only be
+ % recorded for FAIL nodes. This should be `no' initially. DupFactor
+ % keeps track of how many times the events before the last REDO could
+ % have been duplicated and should initially be zero.
+ %
+:- pred node_events(wrap(S)::in, edt_node(R)::in, int::in, int::out, bool::in,
+ int::in, int::in, int::out) is det <= annotated_trace(S, R).
+
+node_events(wrap(Store), dynamic(Ref), PrevEvents, Events, RecordDups,
+ DupFactor, PrevDupEvents, DupEvents) :-
+ det_trace_node_from_id(Store, Ref, Final),
+ (
+ (
+ Final = exit(_, CallId, RedoId, _, FinalEvent, _),
+ NewRecordDups = RecordDups
+ ;
+ Final = fail(_, CallId, RedoId, FinalEvent),
+ NewRecordDups = yes
+ ;
+ Final = excp(_, CallId, RedoId, _, FinalEvent),
+ NewRecordDups = RecordDups
+ )
+ ->
+ (
+ maybe_redo_node_from_id(Store, RedoId, Redo),
+ Redo = redo(_, ExitId, RedoEvent)
+ ->
+ (
+ NewRecordDups = yes,
+ NewPrevDupEvents = PrevDupEvents + DupFactor
+ * (FinalEvent - RedoEvent + 1)
+ ;
+ NewRecordDups = no,
+ NewPrevDupEvents = 0
+ ),
+ node_events(wrap(Store), dynamic(ExitId), PrevEvents +
+ FinalEvent - RedoEvent + 1, Events,
+ NewRecordDups, DupFactor + 1,
+ NewPrevDupEvents, DupEvents)
+ ;
+ det_trace_node_from_id(Store, CallId, Call),
+ (
+ CallEvent = Call ^ call_event
+ ->
+ Events = PrevEvents + FinalEvent - CallEvent
+ + 1,
+ (
+ NewRecordDups = yes,
+ DupEvents = PrevDupEvents + DupFactor *
+ (FinalEvent - CallEvent + 1)
+ ;
+ NewRecordDups = no,
+ DupEvents = 0
+ )
+ ;
+ throw(internal_error("node_events",
+ "not a CALL"))
+ )
+ )
+ ;
+ throw(internal_error("node_events",
+ "not a final event"))
+ ).
:- pred missing_answer_special_case(trace_atom::in) is semidet.
Index: doc/user_guide.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/user_guide.texi,v
retrieving revision 1.404
diff -u -r1.404 user_guide.texi
--- doc/user_guide.texi 20 Dec 2004 01:15:48 -0000 1.404
+++ doc/user_guide.texi 21 Dec 2004 11:44:21 -0000
@@ -75,6 +75,7 @@
@author Peter Ross
@author Tyson Dowd
@author Mark Brown
+ at author Ian MacLarty
@page
@vskip 0pt plus 1filll
Copyright @copyright{} 1995--2004 The University of Melbourne.
@@ -3256,7 +3257,7 @@
@ref{Declarative debugging} for details.
@sp 1
@table @code
- at item dd
+ at item dd [-d at var{depth} -s at var{strategy}]
@c @item dd [--assume-all-io-is-tabled]
@c The --assume-all-io-is-tabled option is for developers only. Specifying it
@c makes an assertion, and if the assertion is incorrect, the resulting
@@ -3273,6 +3274,18 @@
declarative debugger for long running programs since it will not have to rerun
the program as much.
@sp 1
+The @samp{-s at var{strategy}} or @samp{--default-search-mode
+ at var{strategy}} option tells the declarative debugger which
+search strategy to use by default. Either @samp{top-down} or
+ at samp{divide-and-query} may be specified. @samp{top-down} search is more
+predicable and will ask you about the children of the last atom you
+asserted was erroneous (i.e. gave a `no' answer for), however this may
+mean that lots of questions will need to be answered before a bug is located.
+ at samp{divide-and-query} search tries to ask questions that will halve the
+search space with each answer resulting in quicker localization of the bug,
+however the questions asked may appear unrelated to each other.
+ at samp{top-down} is the default when this option is not given.
+ at sp 1
@item trust @var{module-name}|@var{proc-spec}
@kindex trust (mdb command)
Tells the declarative debugger to trust the given module, predicate or
@@ -3623,6 +3636,7 @@
* Oracle questions::
* Declarative debugging commands::
* Diagnoses::
+* Search Strategies::
* Improving the search::
@end menu
@@ -3883,6 +3897,36 @@
If the user aborts the diagnosis,
they are returned to the event at which the @samp{dd} command was given.
+ at node Search Strategies
+ at subsection Search Strategies
+
+Currently the declarative debugger can employ one of two strategies when
+searching for a bug. The initial strategy to use can be specified
+as an option to the @samp{dd} command. See
+ at ref{Declarative debugging mdb commands} for information on how to do this.
+
+ at subsubsection Top-down Search
+
+Using this strategy the declarative debugger will ask about the children
+of the last atom who's assertion was false. This makes the search more
+predictable from the user's point of view as the questions will more
+or less follow the program execution. The drawback of top-down search is that
+it may require a lot of questions to be answered before a bug is found,
+especially with deeply recursive program runs.
+
+This search strategy is used by default when no other strategy is specified.
+
+ at subsubsection Divide and Query Search
+
+With this strategy the declarative debugger will attempt to halve the size of
+the search space with each question. In most cases this will result in the
+bug being found after log(N) questions where N is the number of events
+between the event where the @samp{dd} command was given and the corresponding
+ at samp{CALL} event. This makes the search feasible for deeply recursive runs
+where top-down search would require an unreasonably large number of questions
+to be answered. However, the questions may appear to come from unrelated parts
+of the program which can make them harder to answer.
+
@node Improving the search
@subsection Improving the search
@@ -3966,13 +4010,13 @@
the call that constructed the year part of the date.
This feature is also useful when using the procedural debugger. For example,
-suppose that you come across a CALL event and you would like to know the source
-of a particular input to the call. To find out you could first go to the final
-event by issuing a @samp{finish} command. Invoke the declarative debugger with
-a @samp{dd} command and then mark the input term you are interested in. The
-next question should be about the call that bound the term. Issue a @samp{pd}
-command at this point to return to the procedural debugger. It will now show
-the final event of the call that bound the term.
+suppose that you come across a @samp{CALL} event and you would like to know the
+source of a particular input to the call. To find out you could first go to
+the final event by issuing a @samp{finish} command. Invoke the declarative
+debugger with a @samp{dd} command and then mark the input term you are
+interested in. The next question should be about the call that bound the term.
+Issue a @samp{pd} command at this point to return to the procedural debugger.
+It will now show the final event of the call that bound the term.
@subsubsection Trusting predicates, functions and modules
Index: tests/debugger/declarative/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/debugger/declarative/Mmakefile,v
retrieving revision 1.68
diff -u -r1.68 Mmakefile
--- tests/debugger/declarative/Mmakefile 16 Dec 2004 00:12:40 -0000 1.68
+++ tests/debugger/declarative/Mmakefile 21 Dec 2004 05:40:39 -0000
@@ -19,6 +19,7 @@
deep_warning \
dependency \
dependency2 \
+ divide_and_query1 \
empty_command \
explicit_subtree \
failed_cond \
@@ -228,6 +229,11 @@
dependency2.out: dependency2 dependency2.inp
$(MDB) ./dependency2 < dependency2.inp > dependency2.out 2>&1 \
+ || { grep . $@ /dev/null; exit 1; }
+
+divide_and_query1.out: divide_and_query1.inp
+ $(MDB_STD) ./divide_and_query1 < divide_and_query1.inp \
+ > divide_and_query1.out 2>&1 \
|| { grep . $@ /dev/null; exit 1; }
empty_command.out: empty_command empty_command.inp
Index: tests/debugger/declarative/divide_and_query1.exp
===================================================================
RCS file: tests/debugger/declarative/divide_and_query1.exp
diff -N tests/debugger/declarative/divide_and_query1.exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/debugger/declarative/divide_and_query1.exp 21 Dec 2004 03:59:43 -0000
@@ -0,0 +1,181 @@
+ E1: C1 CALL pred divide_and_query1.main/2-0 (det) divide_and_query1.m:15
+mdb> mdb> Contexts will not be printed.
+mdb> echo on
+Command echo enabled.
+mdb> register --quiet
+mdb> context none
+Contexts will not be printed.
+mdb> echo on
+Command echo enabled.
+mdb> register --quiet
+mdb> context none
+Contexts will not be printed.
+mdb> echo on
+Command echo enabled.
+mdb> register --quiet
+mdb> context none
+Contexts will not be printed.
+mdb> echo on
+Command echo enabled.
+mdb> register --quiet
+mdb> context none
+Contexts will not be printed.
+mdb> echo on
+Command echo enabled.
+mdb> register --quiet
+mdb> context none
+Contexts will not be printed.
+mdb> echo on
+Command echo enabled.
+mdb> register --quiet
+mdb> context none
+Contexts will not be printed.
+mdb> echo on
+Command echo enabled.
+mdb> break to_b
+ 0: + stop interface pred divide_and_query1.to_b/2-0 (det)
+mdb> c -n
+ E2: C2 CALL pred divide_and_query1.to_b/2-0 (det)
+mdb> f -n
+ E3: C2 EXIT pred divide_and_query1.to_b/2-0 (det)
+mdb> dd -s divide_and_query
+to_b([a, a, a, a, a, a, a, a, a, a], [b, b, b, b, b, b, b, b, b, b])
+Valid? n
+to_b([a, a, a, a], [b, b, b, b])
+Valid? n
+to_b([a], [b])
+Valid? y
+to_b([a, a], [b, b])
+Valid? y
+to_b([a, a, a], [b, b, b])
+Valid? y
+Found incorrect contour:
+to_b([a, a, a, a], [b, b, b, b])
+Is this a bug? y
+ E4: C3 EXIT pred divide_and_query1.to_b/2-0 (det)
+mdb> delete *
+ 0: E stop interface pred divide_and_query1.to_b/2-0 (det)
+mdb> break abba
+ 0: + stop interface pred divide_and_query1.abba/1-0 (semidet)
+mdb> c
+[b, b, b, b, b, b, b, b, b, b] E5: C4 CALL pred divide_and_query1.abba/1-0 (semidet)
+mdb> f -n
+ E6: C4 EXIT pred divide_and_query1.abba/1-0 (semidet)
+mdb> dd -s divide_and_query
+abba([b, a, a, b])
+Valid? n
+abba_perm([a, a, b], [a, b, a])
+Valid? y
+abba_delete([a, b, b, a], b, [a, b, a])
+Valid? n
+abba_delete([b, b, a], b, [b, a])
+Valid? n
+Found incorrect contour:
+abba_delete([b, b, a], b, [b, a])
+Is this a bug? y
+ E7: C5 EXIT pred divide_and_query1.abba_delete/3-0 (multi)
+mdb> c
+ E6: C4 EXIT pred divide_and_query1.abba/1-0 (semidet)
+mdb> c
+abba E8: C6 CALL pred divide_and_query1.abba/1-0 (semidet)
+mdb> f
+ E9: C6 FAIL pred divide_and_query1.abba/1-0 (semidet)
+mdb> dd -s divide_and_query
+Call abba([a, a, a, b])
+No solutions.
+Complete? n
+Call abba_perm([a, a, a, b], _)
+Solutions:
+ abba_perm([a, a, a, b], [a, a, a, b])
+ abba_perm([a, a, a, b], [a, a, a, b])
+ abba_perm([a, a, a, b], [a, a, a, b])
+ abba_perm([a, a, a, b], [a, a, b, a])
+ abba_perm([a, a, a, b], [a, a, a, b])
+ abba_perm([a, a, a, b], [a, a, a, b])
+ abba_perm([a, a, a, b], [a, a, a, b])
+ abba_perm([a, a, a, b], [a, a, b, a])
+ abba_perm([a, a, a, b], [a, a, b, a])
+ abba_perm([a, a, a, b], [a, a, b, a])
+ abba_perm([a, a, a, b], [a, b, a, a])
+ abba_perm([a, a, a, b], [a, b, a, a])
+ abba_perm([a, a, a, b], [a, a, b, a])
+ abba_perm([a, a, a, b], [a, a, b, a])
+ abba_perm([a, a, a, b], [a, b, a, a])
+ abba_perm([a, a, a, b], [a, b, a, a])
+ abba_perm([a, a, a, b], [a, b, a, a])
+ abba_perm([a, a, a, b], [b, a, a, a])
+ abba_perm([a, a, a, b], [b, a, a, a])
+ abba_perm([a, a, a, b], [b, a, a, a])
+ abba_perm([a, a, a, b], [a, b, a, a])
+ abba_perm([a, a, a, b], [b, a, a, a])
+ abba_perm([a, a, a, b], [b, a, a, a])
+ abba_perm([a, a, a, b], [b, a, a, a])
+Complete? n
+Call abba_perm([a, a, b], _)
+Solutions:
+ abba_perm([a, a, b], [a, a, b])
+ abba_perm([a, a, b], [a, a, b])
+ abba_perm([a, a, b], [a, b, a])
+ abba_perm([a, a, b], [a, b, a])
+ abba_perm([a, a, b], [b, a, a])
+ abba_perm([a, a, b], [b, a, a])
+Complete? y
+abba_perm([a, a, b], [b, a, a])
+Valid? n
+abba_perm([a, b], [b, a])
+Valid? n
+abba_perm([b], [b])
+Valid? y
+abba_delete([a], a, [])
+Valid? y
+abba_delete([b, a], a, [b])
+Valid? y
+Found incorrect contour:
+abba_perm([a, b], [b, a])
+Is this a bug? y
+ E10: C7 EXIT pred divide_and_query1.abba_perm/2-0 (multi)
+mdb> c
+ E9: C6 FAIL pred divide_and_query1.abba/1-0 (semidet)
+mdb> c
+no abba E11: C8 CALL pred divide_and_query1.abba/1-0 (semidet)
+mdb> f
+ E12: C8 EXIT pred divide_and_query1.abba/1-0 (semidet)
+mdb> trust abba_delete
+Trusting pred divide_and_query1.abba_delete/3
+mdb> dd -s divide_and_query
+abba([a, a, b, b])
+Valid? n
+abba_perm([a, a, b, b], [a, b, b, a])
+Valid? n
+abba_perm([a, b, b], [a, b, b])
+Valid? n
+abba_perm([b, b], [b, b])
+Valid? n
+Found incorrect contour:
+abba_perm([b, b], [b, b])
+Is this a bug? y
+ E13: C9 EXIT pred divide_and_query1.abba_perm/2-0 (multi)
+mdb> delete *
+ 0: E stop interface pred divide_and_query1.abba/1-0 (semidet)
+mdb> break to_b2
+ 0: + stop interface pred divide_and_query1.to_b2/2-0 (det)
+mdb> c
+abba E14: C10 CALL pred divide_and_query1.to_b2/2-0 (det)
+mdb> f
+ E15: C10 EXIT pred divide_and_query1.to_b2/2-0 (det)
+mdb> dd -s divide_and_query
+to_b2([c, c, c, c, c, c, c], [b, b, b, b, b, b, b])
+Valid? b 2
+browser> cd 2/2
+browser> mark
+to_b([c, c, c, c, c], [b, b, b, b, b])
+Valid? n
+to_b([c, c], [b, b])
+Valid? y
+to_b([c, c, c], [b, b, b])
+Valid? n
+Found incorrect contour:
+to_b([c, c, c], [b, b, b])
+Is this a bug? y
+ E16: C11 EXIT pred divide_and_query1.to_b/2-0 (det)
+mdb> quit -y
Index: tests/debugger/declarative/divide_and_query1.inp
===================================================================
RCS file: tests/debugger/declarative/divide_and_query1.inp
diff -N tests/debugger/declarative/divide_and_query1.inp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/debugger/declarative/divide_and_query1.inp 21 Dec 2004 05:22:11 -0000
@@ -0,0 +1,60 @@
+register --quiet
+context none
+echo on
+set depth 100
+break to_b
+c -n
+f -n
+dd -s divide_and_query
+n
+n
+y
+y
+y
+y
+delete *
+break abba
+c
+f -n
+dd -s divide_and_query
+n
+y
+n
+n
+y
+c
+c
+f
+dd -s divide_and_query
+n
+n
+y
+n
+n
+y
+y
+y
+y
+c
+c
+f
+trust abba_delete
+dd -s divide_and_query
+n
+n
+n
+n
+y
+delete *
+break to_b2
+c
+f
+dd -s divide_and_query
+b 2
+cd 2/2
+mark
+n
+y
+n
+y
+quit -y
Index: tests/debugger/declarative/divide_and_query1.m
===================================================================
RCS file: tests/debugger/declarative/divide_and_query1.m
diff -N tests/debugger/declarative/divide_and_query1.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/debugger/declarative/divide_and_query1.m 21 Dec 2004 03:36:27 -0000
@@ -0,0 +1,68 @@
+:- module divide_and_query1.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+:- import_module list.
+
+:- type t ---> a ; b ; c.
+
+main(!IO) :-
+ to_b([a, a, a, a, a, a, a, a, a, a], X),
+ write(X, !IO),
+ (
+ abba([b, a, a, b])
+ ->
+ write_string("abba", !IO)
+ ;
+ write_string("no abba", !IO)
+ ),
+ (
+ abba([a, a, a, b])
+ ->
+ write_string("abba", !IO)
+ ;
+ write_string("no abba", !IO)
+ ),
+ (
+ abba([a, a, b, b])
+ ->
+ write_string("abba", !IO)
+ ;
+ write_string("no abba", !IO)
+ ),
+ to_b2([c, c, c, c, c, c, c], Y),
+ write(Y, !IO).
+
+:- pred to_b(list(t)::in, list(t)::out) is det.
+
+to_b([], []).
+to_b([_ | T], [b | L]) :- to_b(T, L).
+
+:- pred abba(list(t)::in) is semidet.
+
+abba(L) :-
+ abba_perm(L, [a, b, b, a]).
+
+:- pred abba_perm(list(T)::in, list(T)::out) is multi.
+
+abba_perm([], []).
+abba_perm([X | Xs], Ys) :-
+ abba_perm(Xs, Ys0),
+ abba_delete(Ys, X, Ys0).
+
+:- pred abba_delete(list(T)::out, T::in, list(T)::in) is multi.
+
+abba_delete([X | L], X, L).
+abba_delete([X | Xs], Y, [X | L]) :-
+ abba_delete(Xs, Y, L).
+
+:- pred to_b2(list(t)::in, list(t)::out) is det.
+
+to_b2(L0, L) :-
+ to_b(L0, L).
Index: trace/mercury_trace_declarative.c
===================================================================
RCS file: /home/mercury1/repository/mercury/trace/mercury_trace_declarative.c,v
retrieving revision 1.75
diff -u -r1.75 mercury_trace_declarative.c
--- trace/mercury_trace_declarative.c 16 Dec 2004 00:12:41 -0000 1.75
+++ trace/mercury_trace_declarative.c 16 Dec 2004 00:27:20 -0000
@@ -679,7 +679,8 @@
(MR_Word) call);
node = (MR_Trace_Node) MR_DD_construct_redo_node(
(MR_Word) prev,
- last_interface);
+ last_interface,
+ (MR_Word) event_info->MR_event_number);
MR_DD_call_node_set_last_interface((MR_Word) call,
(MR_Word) node);
);
@@ -1171,6 +1172,35 @@
&MR_trace_front_end_state);
);
done = MR_TRUE;
+ }
+}
+
+void
+MR_trace_decl_set_default_search_mode(
+ MR_Decl_Default_Search_Mode default_search_mode)
+{
+ MR_trace_decl_ensure_init();
+ MR_TRACE_CALL_MERCURY(
+ MR_DD_decl_set_default_search_mode(default_search_mode,
+ MR_trace_front_end_state,
+ &MR_trace_front_end_state);
+ );
+}
+
+MR_bool
+MR_trace_is_valid_search_mode_string(const char *search_mode_string,
+ MR_Decl_Default_Search_Mode *default_search_mode)
+{
+ if (MR_streq(search_mode_string, "top_down")) {
+ *default_search_mode =
+ MR_DD_decl_top_down_default_search_mode();
+ return MR_TRUE;
+ } else if (MR_streq(search_mode_string, "divide_and_query")) {
+ *default_search_mode =
+ MR_DD_decl_divide_and_query_default_search_mode();
+ return MR_TRUE;
+ } else {
+ return MR_FALSE;
}
}
Index: trace/mercury_trace_declarative.h
===================================================================
RCS file: /home/mercury1/repository/mercury/trace/mercury_trace_declarative.h,v
retrieving revision 1.20
diff -u -r1.20 mercury_trace_declarative.h
--- trace/mercury_trace_declarative.h 16 Dec 2004 00:12:41 -0000 1.20
+++ trace/mercury_trace_declarative.h 21 Dec 2004 11:38:15 -0000
@@ -62,6 +62,28 @@
extern MR_bool MR_decl_remove_trusted(int n);
/*
+** MR_trace_decl_set_default_search_mode sets the default search mode for
+** the analyser.
+*/
+
+typedef MR_Word MR_Decl_Default_Search_Mode;
+
+extern void MR_trace_decl_set_default_search_mode(
+ MR_Decl_Default_Search_Mode default_search_mode);
+
+/*
+** This function checks to see if the supplied string is a valid
+** default search mode. If it is then it returns MR_TRUE and sets
+** the value at default_search_mode to the corresponding default search mode.
+** If it isn't then it returns MR_FALSE and leaves the value at
+** default_search_mode unchanged.
+*/
+
+extern MR_bool MR_trace_is_valid_search_mode_string(
+ const char *search_mode_string,
+ MR_Decl_Default_Search_Mode *default_search_mode);
+
+/*
** Prints a list of the trusted objects. If mdb_command_format is true it
** prints the list as a series of mdb `trust' commands. Otherwise it
** prints the list in a format suitable for display.
Index: trace/mercury_trace_internal.c
===================================================================
RCS file: /home/mercury1/repository/mercury/trace/mercury_trace_internal.c,v
retrieving revision 1.184
diff -u -r1.184 mercury_trace_internal.c
--- trace/mercury_trace_internal.c 16 Dec 2004 00:12:41 -0000 1.184
+++ trace/mercury_trace_internal.c 16 Dec 2004 00:28:48 -0000
@@ -540,8 +540,10 @@
MR_bool *split, MR_bool *close_window, char ***words,
int *word_count, const char *cat, const char*item);
static MR_bool MR_trace_options_dd(MR_bool *assume_all_io_is_tabled,
- MR_Integer *depth_step_size, char ***words,
- int *word_count, const char *cat, const char *item);
+ MR_Integer *depth_step_size,
+ MR_Decl_Default_Search_Mode *default_search_mode,
+ char ***words, int *word_count, const char *cat,
+ const char *item);
static MR_bool MR_trace_options_type_ctor(MR_bool *print_rep,
MR_bool *print_functors, char ***words,
int *word_count, const char *cat, const char *item);
@@ -5510,10 +5512,19 @@
MR_Event_Info *event_info, MR_Event_Details *event_details,
MR_Code **jumpaddr)
{
+ MR_Decl_Default_Search_Mode default_search_mode;
+
MR_trace_decl_assume_all_io_is_tabled = MR_FALSE;
MR_edt_depth_step_size = MR_TRACE_DECL_INITIAL_DEPTH;
+ if (! MR_trace_is_valid_search_mode_string("top_down",
+ &default_search_mode))
+ {
+ MR_fatal_error("MR_trace_cmd_dd: top_down invalid");
+ }
+
if (! MR_trace_options_dd(&MR_trace_decl_assume_all_io_is_tabled,
- &MR_edt_depth_step_size, &words, &word_count, "dd", "dd"))
+ &MR_edt_depth_step_size, &default_search_mode,
+ &words, &word_count, "dd", "dd"))
{
; /* the usage message has already been printed */
} else if (word_count == 1) {
@@ -5525,6 +5536,8 @@
return KEEP_INTERACTING;
}
+ MR_trace_decl_set_default_search_mode(default_search_mode);
+
if (MR_trace_start_decl_debug(MR_TRACE_DECL_DEBUG,
NULL, cmd, event_info, event_details, jumpaddr))
{
@@ -5544,11 +5557,19 @@
{
MR_Trace_Mode trace_mode;
const char *filename;
+ MR_Decl_Default_Search_Mode default_search_mode;
MR_trace_decl_assume_all_io_is_tabled = MR_FALSE;
- MR_edt_depth_step_size = 3;
+ MR_edt_depth_step_size = MR_TRACE_DECL_INITIAL_DEPTH;
+ if (! MR_trace_is_valid_search_mode_string("top_down",
+ &default_search_mode))
+ {
+ MR_fatal_error("MR_trace_cmd_dd_dd: top_down invalid");
+ }
+
if (! MR_trace_options_dd(&MR_trace_decl_assume_all_io_is_tabled,
- &MR_edt_depth_step_size, &words, &word_count, "dd", "dd_dd"))
+ &MR_edt_depth_step_size, &default_search_mode,
+ &words, &word_count, "dd", "dd_dd"))
{
; /* the usage message has already been printed */
} else if (word_count <= 2) {
@@ -5560,6 +5581,8 @@
filename = (const char *) NULL;
}
+ MR_trace_decl_set_default_search_mode(default_search_mode);
+
if (MR_trace_start_decl_debug(trace_mode, filename,
cmd, event_info, event_details, jumpaddr))
{
@@ -6552,20 +6575,23 @@
static struct MR_option MR_trace_dd_opts[] =
{
- { "assume-all-io-is-tabled", MR_no_argument, NULL, 'a' },
- { "depth-step-size", MR_required_argument, NULL, 'd' },
- { NULL, MR_no_argument, NULL, 0 }
+ { "assume-all-io-is-tabled", MR_no_argument, NULL, 'a' },
+ { "depth-step-size", MR_required_argument, NULL, 'd' },
+ { "default-search-mode", MR_required_argument, NULL, 's' },
+ { NULL, MR_no_argument, NULL, 0 }
};
static MR_bool
MR_trace_options_dd(MR_bool *assume_all_io_is_tabled,
- MR_Integer *depth_step_size, char ***words, int *word_count, const char
+ MR_Integer *depth_step_size,
+ MR_Decl_Default_Search_Mode *default_search_mode,
+ char ***words, int *word_count, const char
*cat, const char *item)
{
int c;
MR_optind = 0;
- while ((c = MR_getopt_long(*word_count, *words, "ad:",
+ while ((c = MR_getopt_long(*word_count, *words, "ad:s:",
MR_trace_dd_opts, NULL)) != EOF)
{
switch (c) {
@@ -6580,6 +6606,14 @@
return MR_FALSE;
}
break;
+ case 's':
+ if (! MR_trace_is_valid_search_mode_string(
+ MR_optarg,
+ default_search_mode)) {
+ MR_trace_usage(cat, item);
+ return MR_FALSE;
+ }
+ break;
default:
MR_trace_usage(cat, item);
return MR_FALSE;
@@ -7444,6 +7478,11 @@
static const char *const MR_trace_scope_cmd_args[] =
{ "all", "interface", "entry", NULL };
+static const char *const MR_trace_dd_cmd_args[] =
+ { "-s", "-a", "-d", "--default-search-mode",
+ "--assume-all-io-is-tabled", "--depth-step-size",
+ "top_down", "divide_and_query", NULL };
+
/*
** "table_io allow" is deliberately not documented as it is developer only
** "table_io begin" and "table_io end" are deliberately not documented in an
@@ -7574,11 +7613,11 @@
NULL, MR_trace_help_completer },
{ "dd", "dd", MR_trace_cmd_dd,
+ MR_trace_dd_cmd_args, MR_trace_null_completer },
+ { "dd", "trust", MR_trace_cmd_trust,
+ NULL, MR_trace_breakpoint_completer },
+ { "dd", "untrust", MR_trace_cmd_untrust,
NULL, MR_trace_null_completer },
- { "dd", "trust", MR_trace_cmd_trust, NULL,
- MR_trace_null_completer },
- { "dd", "untrust", MR_trace_cmd_untrust, NULL,
- MR_trace_null_completer },
{ "dd", "trusted", MR_trace_cmd_trusted, NULL,
MR_trace_null_completer },
@@ -7633,7 +7672,7 @@
{ "developer", "unhide_events", MR_trace_cmd_unhide_events,
MR_trace_on_off_args, MR_trace_null_completer },
{ "developer", "dd_dd", MR_trace_cmd_dd_dd,
- NULL, MR_trace_filename_completer },
+ MR_trace_dd_cmd_args, MR_trace_filename_completer },
{ "developer", "table", MR_trace_cmd_table,
NULL, MR_trace_null_completer },
{ "developer", "type_ctor", MR_trace_cmd_type_ctor,
--------------------------------------------------------------------------
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