mirror of
https://github.com/Mercury-Language/mercury.git
synced 2026-04-15 17:33:38 +00:00
62ec97d443
If a module has two or more import_module or use_module declarations
for the same module, (typically, but not always, one being in its interface
and one in its implementation), generate an informational message about
each redundant declaration if --warn-unused-imports is enabled.
compiler/hlds_module.m:
We used to record the set of imported/used modules, and the set of
modules imported/used in the interface of the current module. However,
these sets
- did not record the distinction between imports and uses;
- did not allow distinction between single and multiple imports/uses;
- did not record the locations of the imports/uses.
The first distinction was needed only by module_qual.m, which *did*
pay attention to it; the other two were not needed at all.
To generate messages for imports/uses shadowing other imports/uses,
we need all three, so change the data structure storing such information
for *direct* imports to one that records all three of the above kinds
of information. (For imports made by read-in interface and optimization
files, the old set of modules approach is fine, and this diff leaves
the set of thus *indirectly* imported module names alone.)
compiler/unused_imports.m:
Use the extra information now available to generate a
severity_informational message about any import or use that is made
redundant by an earlier, more general import or use.
Fix two bugs in the code that generated warnings for just plain unused
modules.
(1) It did not consider that a use of the builtin type char justified
an import of char.m, but without that import, the type is not visible.
(2) It scanned cons_ids in goals in procedure bodies, but did not scan
cons_ids that have been put into the const_struct_db. (I did not update
the code here when I added the const_struct_db.)
Also, add a (hopefully temporary) workaround for a bug in
make_hlds_passes.m, which is noted below.
However, there are at least three problems that prevent us from enabling
--warn-unused-imports by default.
(1) In some places, the import of a module is used only by clauses for
a predicate that also has foreign procs. When compiled in a grade that
selects one of those foreign_procs as the implementation of the predicate,
the clauses are discarded *without* being added to the HLDS at all.
This leads unused_imports.m to generate an uncalled-for warning in such
cases. To fix this, we would need to preserve the Mercury clauses for
*all* predicates, even those with foreign procs, and do all the semantic
checks on them before throwing them away. (I tried to do this once, and
failed, but the task should be easier after the item list change.)
(2) We have two pieces of code to generate import warnings. The one in
unused_imports.m operates on the HLDS after type and mode checking,
while module_qual.m operates on the parse tree before the creation of
the HLDS. The former is more powerful, since it knows e.g. what types and
modes are used in the bodies of predicates, and hence can generate warnings
about an import being unused *anywhere* in a module, as opposed to just
unused in its interface.
If --warn-unused-imports is enabled, we will get two separate set of
reports about an interface import being unused in the interface,
*unless* we get a type or mode error, in which case unused_imports.m
won't be invoked. But in case we do get such errors, we don't want to
throw away the warnings from module_qual.m. We could store them and
throw them away only after we know we won't need them, or just get
the two modules to generate identical error_specs for each warning,
so that the sort_and_remove_dups of the error specs will do the
throwing away for us for free, if we get that far.
(3) The valid/bug100.m test case was added as a regression test for a bug
that was fixed in module_qual.m. However the bug is still present in
unused_imports.m.
compiler/make_hlds_passes.m:
Give hlds_module.m the extra information it now needs for each item_avail.
Add an XXX for a bug that cannot be fixed right now: the setting of
the status of abstract instances to abstract_imported. (The "abstract"
part is correct; the "imported" part may not be.)
compiler/intermod.m:
compiler/try_expand.m:
compiler/xml_documentation.m:
Conform to the change in hlds_module.m.
compiler/module_qual.m:
Update the documentation of the relationship of this module
with unused_imports.m.
compiler/hlds_data.m:
Document a problem with the status of instance definitions.
compiler/hlds_out_module.m:
Update the code that prints out the module_info to conform to the change
to hlds_module.m.
Print status information about instances, which was needed to diagnose
one of the bugs in unused_imports.m. Format the output for instances
nicer.
compiler/prog_item.m:
Add a convenience predicate.
compiler/prog_data.m:
Remove a type synonym that makes things harder to understand, not easier.
compiler/modules.m:
Delete an XXX that asks for the feature this diff implements.
Add another XXX about how that feature could be improved.
compiler/Mercury.options.m:
Add some more modules to the list of modules on which the compiler
should be invoked with --no-warn-unused-imports.
compiler/*.m:
library/*.m:
mdbcomp/*.m:
browser/*.m:
deep_profiler/*.m:
mfilterjavac/*.m:
Delete unneeded imports. Many of these shadow other imports, and some
are just plain unneeded, as shown by --warn-unused-imports. In a few
modules, there were a *lot* of unneeded imports, but most had just
one or two.
In a few cases, removing an import from a module, because it *itself*
does not need it, required adding that same import to those of its
submodules which *do* need it.
In a few cases, conform to other changes above.
tests/invalid/Mercury.options:
Test the generation of messages about import shadowing on the existing
import_in_parent.m test case (although it was also tested very thoroughly
when giving me the information needed for the deletion of all the
unneeded imports above).
tests/*/*.{m,*exp}:
Delete unneeded imports, and update any expected error messages
to expect the now-smaller line numbers.
1362 lines
56 KiB
Mathematica
1362 lines
56 KiB
Mathematica
%-----------------------------------------------------------------------------%
|
|
% vim: ft=mercury ts=4 sw=4 et
|
|
%-----------------------------------------------------------------------------%
|
|
% Copyright (C) 1999-2007, 2011 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.
|
|
%-----------------------------------------------------------------------------%
|
|
%
|
|
% File: declarative_analyser.m
|
|
% Authors: Mark Brown, Ian MacLarty
|
|
%
|
|
% This module implements some analysis algorithms that search for bugs in
|
|
% Evaluation Dependency Trees (EDTs). The search algorithms use information
|
|
% provided by the search_space data type which acts as a layer on top of the
|
|
% EDT, storing information relevant to the bug search. Throughout this module
|
|
% the type variables T and S refer to the types of nodes in the EDT and the
|
|
% store of EDT nodes respectively.
|
|
%
|
|
%-----------------------------------------------------------------------------%
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
:- module mdb.declarative_analyser.
|
|
:- interface.
|
|
|
|
:- import_module mdb.declarative_debugger.
|
|
:- import_module mdb.declarative_edt.
|
|
:- import_module mdb.declarative_oracle.
|
|
:- import_module mdb.declarative_user.
|
|
|
|
:- import_module io.
|
|
:- import_module maybe.
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
:- type analyser_response(T)
|
|
---> analyser_response_no_suspects
|
|
% There are no suspects left, and no incorrect
|
|
% nodes have been found.
|
|
|
|
; analyser_response_bug_found(decl_bug, decl_evidence(T))
|
|
% A suspect who is guilty, along with the evidence
|
|
% against the suspect.
|
|
|
|
; analyser_response_oracle_question(decl_question(T))
|
|
% The analyser desires an answer to the question.
|
|
|
|
; analyser_response_require_explicit_subtree(T)
|
|
% The analyser requires the given implicit sub-tree
|
|
% to be made explicit.
|
|
|
|
; analyser_response_require_explicit_supertree(T)
|
|
% The analyser requires an explicit tree above the root
|
|
% of an existing explicit tree.
|
|
|
|
; analyser_response_revise(decl_question(T)).
|
|
% The analyser would like the oracle to re-ask the user
|
|
% this question and then for analysis to continue.
|
|
|
|
:- func reason_to_string(reason_for_question) = string.
|
|
|
|
:- type analyser_state(T).
|
|
|
|
:- type search_mode.
|
|
|
|
:- func divide_and_query_search_mode = search_mode.
|
|
|
|
:- func suspicion_divide_and_query_search_mode = search_mode.
|
|
|
|
:- func top_down_search_mode = search_mode.
|
|
|
|
:- pred analyser_state_init(analyser_state(T)::out) is det.
|
|
|
|
% Resets the state of the analyser.
|
|
%
|
|
:- pred reset_analyser(analyser_state(T)::in, analyser_state(T)::out) is det.
|
|
|
|
% Make the given search mode the fallback search mode
|
|
% and the current search mode for the analyser.
|
|
%
|
|
:- pred set_fallback_search_mode(S::in, search_mode::in,
|
|
analyser_state(T)::in, analyser_state(T)::out)
|
|
is det <= mercury_edt(S, T).
|
|
|
|
:- type analysis_type(T)
|
|
---> new_tree(T)
|
|
% Use the given tree to do analysis. The tree will be
|
|
% a new explicitly generated portion of the annotated trace.
|
|
% start_or_resume_analysis should be called with this type
|
|
% of analysis when a new declarative debugging session has been
|
|
% started or a requested subtree or supertree has been generated.
|
|
|
|
; resume_previous.
|
|
% Continue the previous analysis. This will happen when the user
|
|
% suspends a declarative debugging session with a `pd' or `abort'
|
|
% command and now wants to continue the suspended session.
|
|
|
|
% Perform analysis on the given EDT, which may be a new tree
|
|
% to diagnose, or a sub-tree that was required to be made explicit.
|
|
%
|
|
:- pred start_or_resume_analysis(S::in, oracle_state::in, analysis_type(T)::in,
|
|
analyser_response(T)::out, analyser_state(T)::in,
|
|
analyser_state(T)::out) is det <= mercury_edt(S, T).
|
|
|
|
% Return a response which will cause the last question to be re-asked.
|
|
%
|
|
:- pred reask_last_question(S::in, analyser_state(T)::in,
|
|
analyser_response(T)::out) is semidet <= mercury_edt(S, T).
|
|
|
|
% Continue analysis after the oracle has responded with an answer.
|
|
%
|
|
:- pred continue_analysis(S::in, oracle_state::in, decl_answer(T)::in,
|
|
analyser_response(T)::out, analyser_state(T)::in,
|
|
analyser_state(T)::out) is det <= mercury_edt(S, T).
|
|
|
|
% Change the current search mode of the analyser and return the
|
|
% next question using the new search mode.
|
|
%
|
|
:- pred change_search_mode(S::in, oracle_state::in, user_search_mode::in,
|
|
analyser_state(T)::in, analyser_state(T)::out,
|
|
analyser_response(T)::out) is det <= mercury_edt(S, T).
|
|
|
|
% Display information about the current question and the state
|
|
% of the search to the supplied output stream.
|
|
%
|
|
:- pred show_info(S::in, io.output_stream::in, analyser_state(T)::in,
|
|
io::di, io::uo) is det <= mercury_edt(S, T).
|
|
|
|
% Revise the current analysis. This is done when a bug determined
|
|
% by the analyser has been overruled by the oracle.
|
|
%
|
|
:- pred revise_analysis(S::in, analyser_response(T)::out,
|
|
analyser_state(T)::in, analyser_state(T)::out) is det <= mercury_edt(S, T).
|
|
|
|
% Return information within the analyser state that is intended for
|
|
% debugging the declarative debugger itself.
|
|
%
|
|
:- pred debug_analyser_state(analyser_state(T)::in,
|
|
maybe(subterm_origin(T))::out) is det.
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
:- implementation.
|
|
|
|
:- import_module mdb.browser_info.
|
|
:- import_module mdb.declarative_execution.
|
|
:- import_module mdbcomp.prim_data.
|
|
:- import_module mdbcomp.program_representation.
|
|
:- import_module mdbcomp.rtti_access.
|
|
:- import_module mdbcomp.sym_name.
|
|
|
|
:- import_module array.
|
|
:- import_module bool.
|
|
:- import_module exception.
|
|
:- import_module float.
|
|
:- import_module int.
|
|
:- import_module list.
|
|
:- import_module map.
|
|
:- import_module math.
|
|
:- import_module pair.
|
|
:- import_module string.
|
|
:- import_module unit.
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
% Describes what search strategy is being used by the analyser and the
|
|
% state of the search.
|
|
%
|
|
:- type search_mode
|
|
---> analyser_top_down
|
|
% Look for the first unknown suspect in a top-down fashion,
|
|
% starting at the root. If no unknown suspects are found, then
|
|
% choose a skipped suspect to requery.
|
|
|
|
; analyser_follow_subterm_end(
|
|
% Follow the subterm all the way to where it's bound or
|
|
% until it can't be followed any further (for example
|
|
% when there is a call to a module with no tracing),
|
|
% and ask a question about the nearest unknown suspect
|
|
% on the subterm dependency chain. Then proceed to do
|
|
% a binary search between this node and the root of the
|
|
% search space (the binary search will only come into
|
|
% effect if the oracle asserts the suspect is correct
|
|
% or inadmissible).
|
|
|
|
suspect_id,
|
|
arg_pos,
|
|
term_path,
|
|
% The above 3 args give the position the sub-term tracking
|
|
% algorithm has got up to if it needs to stop to wait for
|
|
% an explicit sub/super-tree to be generated.
|
|
|
|
maybe(suspect_id),
|
|
% The last suspect on the dependency chain whose status was
|
|
% unknown. Initially this is no, but as the sub-term is tracked
|
|
% to where it was initially bound (which could be above or
|
|
% below the node where it was marked incorrect), the most
|
|
% recent node through which the sub-term was tracked that
|
|
% has a status of `unknown' is stored in this field. This is
|
|
% then used as the next question if the node that bound
|
|
% the sub-term is trusted or in an excluded part of the search
|
|
% tree.
|
|
|
|
how_track_subterm
|
|
% This field specifies the algorithm to use when tracking
|
|
% the subterm.
|
|
)
|
|
|
|
; analyser_binary(
|
|
% Perform a binary search on a path in the search space
|
|
% between a suspect and an ancestor of the suspect.
|
|
% The path is represented as an array (the 1st argument)
|
|
% with the deeper suspect at the end of the array and its
|
|
% ancestor at the beginning. The range field gives the
|
|
% inclusive subrange of the array to search. last_tested
|
|
% is the index into the array of the last suspect about which
|
|
% a question was asked.
|
|
|
|
suspects :: array(suspect_id),
|
|
range :: pair(int, int),
|
|
last_tested :: int
|
|
)
|
|
|
|
; analyser_divide_and_query(weighting_heuristic).
|
|
% Divide and query using the given weighting heuristic.
|
|
|
|
divide_and_query_search_mode = analyser_divide_and_query(number_of_events).
|
|
|
|
suspicion_divide_and_query_search_mode = analyser_divide_and_query(suspicion).
|
|
|
|
top_down_search_mode = analyser_top_down.
|
|
|
|
% Each search algorithm should respond with either a question
|
|
% or a request for an explicit subtree to be generated for a suspect
|
|
% which is the root of an implicit subtree.
|
|
%
|
|
:- type search_response
|
|
---> search_response_question(suspect_id, reason_for_question)
|
|
; search_response_require_explicit_subtree(suspect_id)
|
|
; search_response_require_explicit_supertree
|
|
; search_response_no_suspects
|
|
; search_response_found_bug(suspect_id, list(suspect_id),
|
|
list(suspect_id)).
|
|
|
|
% The reason the declarative debugger asked a question.
|
|
%
|
|
:- type reason_for_question
|
|
---> ques_reason_start
|
|
% The first question.
|
|
|
|
; ques_reason_top_down
|
|
|
|
; ques_reason_binding_node(
|
|
binding_prim_op :: primitive_op_type,
|
|
binding_filename :: string,
|
|
binding_line_no :: int,
|
|
|
|
maybe_atom_path :: maybe(term_path),
|
|
% The path of the subterm in the
|
|
% binding node, if it appears in the
|
|
% binding node's atom.
|
|
|
|
binding_proc :: proc_label,
|
|
binding_node_eliminated :: bool
|
|
)
|
|
|
|
; ques_reason_subterm_no_proc_rep
|
|
% No proc rep when tracking subterm.
|
|
|
|
; ques_reason_binding_node_eliminated
|
|
|
|
; ques_reason_binary(
|
|
binary_reason_bottom :: int,
|
|
binary_reason_top :: int,
|
|
binary_reason_split :: int
|
|
)
|
|
|
|
; ques_reason_divide_and_query(
|
|
dq_weighting :: weighting_heuristic,
|
|
|
|
dq_old_weight :: int,
|
|
% The weight of the search space before
|
|
% the question was asked.
|
|
|
|
dq_chosen_subtree_weight :: int
|
|
% The weight the searchspace will be
|
|
% if the user answers `no' to the
|
|
% current question.
|
|
)
|
|
|
|
; ques_reason_skipped
|
|
|
|
; ques_reason_revise.
|
|
|
|
% The analyser state records all of the information that needs
|
|
% to be remembered across multiple invocations of the analyser.
|
|
%
|
|
:- type analyser_state(T)
|
|
---> analyser(
|
|
% Information about the EDT nodes relevant to the bug search.
|
|
search_space :: search_space(T),
|
|
|
|
% This is set to yes when an explicit tree needs to be
|
|
% generated. The maybe argument says what type of explicit
|
|
% tree needs to be generated.
|
|
require_explicit :: maybe(explicit_tree_type),
|
|
|
|
% The method currently being employed to search
|
|
% the search space for questions for the
|
|
% oracle.
|
|
search_mode :: search_mode,
|
|
|
|
% The search mode to use by default.
|
|
% Only non-parametrized search modes should
|
|
% be used as the fallback search mode.
|
|
fallback_search_mode :: 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 knows how to modify the search space when it gets
|
|
% an answer.
|
|
last_search_question :: maybe(suspect_and_reason),
|
|
|
|
% This field is present only to make it easier to debug
|
|
% the dependency tracking algorithm; if bound to yes, it
|
|
% records the result of the invocation of that algorithm
|
|
% on the last analysis step.
|
|
debug_origin :: maybe(subterm_origin(T))
|
|
).
|
|
|
|
:- type suspect_and_reason
|
|
---> suspect_and_reason(suspect_id, reason_for_question).
|
|
|
|
:- type explicit_tree_type
|
|
---> explicit_subtree(suspect_id)
|
|
% Generate an explicit subtree for the implicit root
|
|
% referenced by the suspect_id.
|
|
|
|
; explicit_supertree.
|
|
% Generate a new explicit tree above the current
|
|
% explicit tree.
|
|
|
|
analyser_state_init(Analyser) :-
|
|
Analyser = analyser(empty_search_space, no,
|
|
analyser_top_down, analyser_top_down, no, no).
|
|
|
|
reset_analyser(!Analyser) :-
|
|
FallBack = !.Analyser ^ fallback_search_mode,
|
|
!:Analyser = analyser(empty_search_space, no, FallBack, FallBack, no, no).
|
|
|
|
set_fallback_search_mode(Store, FallBackSearchMode, !Analyser) :-
|
|
!Analyser ^ fallback_search_mode := FallBackSearchMode,
|
|
!Analyser ^ search_mode := FallBackSearchMode,
|
|
!Analyser ^ last_search_question := no,
|
|
(
|
|
FallBackSearchMode = analyser_divide_and_query(Weighting),
|
|
SearchSpace0 = !.Analyser ^ search_space,
|
|
update_weighting_heuristic(Store, Weighting, SearchSpace0,
|
|
SearchSpace),
|
|
!Analyser ^ search_space := SearchSpace
|
|
;
|
|
FallBackSearchMode = analyser_follow_subterm_end(_, _, _, _, _)
|
|
;
|
|
FallBackSearchMode = analyser_binary(_, _, _)
|
|
;
|
|
FallBackSearchMode = analyser_top_down
|
|
).
|
|
|
|
debug_analyser_state(Analyser, Analyser ^ debug_origin).
|
|
|
|
start_or_resume_analysis(Store, Oracle, AnalysisType, Response, !Analyser) :-
|
|
(
|
|
AnalysisType = new_tree(Node),
|
|
MaybeRequireExplicit = !.Analyser ^ require_explicit,
|
|
(
|
|
MaybeRequireExplicit = yes(TreeType),
|
|
SearchSpace0 = !.Analyser ^ search_space,
|
|
(
|
|
TreeType = explicit_supertree,
|
|
incorporate_explicit_supertree(Store, Oracle, Node,
|
|
SearchSpace0, SearchSpace)
|
|
;
|
|
TreeType = explicit_subtree(SuspectId),
|
|
incorporate_explicit_subtree(SuspectId, Node,
|
|
SearchSpace0, SearchSpace)
|
|
),
|
|
!Analyser ^ search_space := SearchSpace,
|
|
!Analyser ^ require_explicit := no,
|
|
decide_analyser_response(Store, Oracle, Response, !Analyser)
|
|
;
|
|
MaybeRequireExplicit = no,
|
|
|
|
% An explicit subtree was not requested, so this is the start
|
|
% of a new declarative debugging session.
|
|
|
|
reset_analyser(!Analyser),
|
|
MaybeWeighting = get_maybe_weighting_from_search_mode(
|
|
!.Analyser ^ search_mode),
|
|
initialise_search_space(Store, MaybeWeighting, Node, SearchSpace),
|
|
!Analyser ^ search_space := SearchSpace,
|
|
topmost_det(SearchSpace, TopMostId),
|
|
!Analyser ^ last_search_question :=
|
|
yes(suspect_and_reason(TopMostId, ques_reason_start)),
|
|
edt_question(Store, Node, Question),
|
|
Response = analyser_response_revise(Question)
|
|
)
|
|
;
|
|
AnalysisType = resume_previous,
|
|
( if reask_last_question(Store, !.Analyser, Response0) then
|
|
Response = Response0
|
|
else
|
|
decide_analyser_response(Store, Oracle, Response, !Analyser)
|
|
)
|
|
).
|
|
|
|
:- func get_maybe_weighting_from_search_mode(search_mode) =
|
|
maybe(weighting_heuristic).
|
|
|
|
get_maybe_weighting_from_search_mode(analyser_divide_and_query(Weighting)) =
|
|
yes(Weighting).
|
|
get_maybe_weighting_from_search_mode(analyser_top_down) = no.
|
|
get_maybe_weighting_from_search_mode(analyser_binary(_, _, _)) = no.
|
|
get_maybe_weighting_from_search_mode(analyser_follow_subterm_end(_, _, _,
|
|
_, _)) = no.
|
|
|
|
reask_last_question(Store, Analyser, Response) :-
|
|
MaybeLastQuestion = Analyser ^ last_search_question,
|
|
MaybeLastQuestion = yes(suspect_and_reason(SuspectId, _)),
|
|
SearchSpace = Analyser ^ search_space,
|
|
Node = get_edt_node(SearchSpace, SuspectId),
|
|
edt_question(Store, Node, OracleQuestion),
|
|
Response = analyser_response_oracle_question(OracleQuestion).
|
|
|
|
continue_analysis(Store, Oracle, Answer, Response, !Analyser) :-
|
|
(
|
|
!.Analyser ^ last_search_question = yes(
|
|
suspect_and_reason(SuspectId, _)),
|
|
process_answer(Store, Answer, SuspectId, !Analyser)
|
|
;
|
|
!.Analyser ^ last_search_question = no,
|
|
throw(internal_error("continue_analysis",
|
|
"received answer to unasked question"))
|
|
),
|
|
decide_analyser_response(Store, Oracle, Response, !Analyser).
|
|
|
|
change_search_mode(Store, Oracle, UserMode, !Analyser, Response) :-
|
|
(
|
|
UserMode = user_top_down,
|
|
set_fallback_search_mode(Store, analyser_top_down, !Analyser)
|
|
;
|
|
UserMode = user_divide_and_query,
|
|
set_fallback_search_mode(Store,
|
|
analyser_divide_and_query(number_of_events), !Analyser)
|
|
;
|
|
UserMode = user_suspicion_divide_and_query,
|
|
set_fallback_search_mode(Store, analyser_divide_and_query(suspicion),
|
|
!Analyser)
|
|
;
|
|
UserMode = user_binary,
|
|
(
|
|
!.Analyser ^ last_search_question =
|
|
yes(suspect_and_reason(SuspectId, _)),
|
|
setup_binary_search(!.Analyser ^ search_space, SuspectId,
|
|
SearchMode),
|
|
!Analyser ^ search_mode := SearchMode
|
|
;
|
|
!.Analyser ^ last_search_question = no,
|
|
throw(internal_error("change_search_mode",
|
|
"binary mode requested, but no last question"))
|
|
)
|
|
),
|
|
decide_analyser_response(Store, Oracle, Response, !Analyser).
|
|
|
|
:- pred process_answer(S::in, decl_answer(T)::in, suspect_id::in,
|
|
analyser_state(T)::in, analyser_state(T)::out) is det <= mercury_edt(S, T).
|
|
|
|
process_answer(Store, Answer, SuspectId, !Analyser) :-
|
|
(
|
|
Answer = skip(_),
|
|
skip_suspect(SuspectId, !.Analyser ^ search_space, SearchSpace),
|
|
!Analyser ^ search_space := SearchSpace
|
|
;
|
|
Answer = ignore(_),
|
|
ignore_suspect(Store, SuspectId, !.Analyser ^ search_space,
|
|
SearchSpace),
|
|
!Analyser ^ search_space := SearchSpace
|
|
;
|
|
Answer = truth_value(_, truth_correct),
|
|
assert_suspect_is_correct(SuspectId, !.Analyser ^ search_space,
|
|
SearchSpace),
|
|
!Analyser ^ search_space := SearchSpace
|
|
;
|
|
Answer = truth_value(_, truth_inadmissible),
|
|
assert_suspect_is_inadmissible(SuspectId, !.Analyser ^ search_space,
|
|
SearchSpace),
|
|
!Analyser ^ search_space := SearchSpace
|
|
;
|
|
Answer = truth_value(_, truth_erroneous),
|
|
assert_suspect_is_erroneous(SuspectId, !.Analyser ^ search_space,
|
|
SearchSpace),
|
|
!Analyser ^ search_space := SearchSpace
|
|
;
|
|
Answer = suspicious_subterm(Node, ArgPos, TermPath, HowTrack,
|
|
ShouldAssertInvalid),
|
|
|
|
% XXX The following 2 lines just done so that debugging info can be
|
|
% printed for tests run when declarative_analyser.m not compiled with
|
|
% tracing (so can't use dd_dd command in mdb). Should be removed when
|
|
% edt_dependency becomes stable enough.
|
|
|
|
edt_dependency(Store, Node, ArgPos, TermPath, _, DebugOrigin),
|
|
!Analyser ^ debug_origin := yes(DebugOrigin),
|
|
(
|
|
ShouldAssertInvalid = assert_invalid,
|
|
edt_subterm_mode(Store, Node, ArgPos, TermPath, Mode),
|
|
(
|
|
Mode = subterm_in,
|
|
assert_suspect_is_inadmissible(SuspectId,
|
|
!.Analyser ^ search_space, SearchSpace)
|
|
;
|
|
Mode = subterm_out,
|
|
assert_suspect_is_erroneous(SuspectId,
|
|
!.Analyser ^ search_space, SearchSpace)
|
|
),
|
|
!Analyser ^ search_space := SearchSpace
|
|
;
|
|
ShouldAssertInvalid = no_assert_invalid
|
|
),
|
|
!Analyser ^ search_mode :=
|
|
analyser_follow_subterm_end(SuspectId, ArgPos, TermPath, no,
|
|
HowTrack)
|
|
).
|
|
|
|
revise_analysis(Store, Response, !Analyser) :-
|
|
SearchSpace = !.Analyser ^ search_space,
|
|
( if root(SearchSpace, RootId) then
|
|
Node = get_edt_node(!.Analyser ^ search_space, RootId),
|
|
edt_question(Store, Node, Question),
|
|
Response = analyser_response_revise(Question),
|
|
revise_root(Store, SearchSpace, SearchSpace1),
|
|
!Analyser ^ search_space := SearchSpace1,
|
|
!Analyser ^ last_search_question :=
|
|
yes(suspect_and_reason(RootId, ques_reason_revise)),
|
|
!Analyser ^ search_mode :=
|
|
!.Analyser ^ fallback_search_mode
|
|
else
|
|
% There must be a root, since a bug was found (and is now
|
|
% being revised).
|
|
throw(internal_error("revise_analysis", "no root"))
|
|
).
|
|
|
|
:- pred decide_analyser_response(S::in, oracle_state::in,
|
|
analyser_response(T)::out, analyser_state(T)::in,
|
|
analyser_state(T)::out) is det <= mercury_edt(S, T).
|
|
|
|
decide_analyser_response(Store, Oracle, Response, !Analyser) :-
|
|
maybe_check_search_space_consistency(Store, !.Analyser ^ search_space,
|
|
"Start of decide_analyser_response"),
|
|
some [!SearchSpace] (
|
|
!:SearchSpace = !.Analyser ^ search_space,
|
|
search_for_question(Store, Oracle, !SearchSpace,
|
|
!.Analyser ^ search_mode, !.Analyser ^ fallback_search_mode,
|
|
NewMode, SearchResponse),
|
|
!Analyser ^ search_space := !.SearchSpace,
|
|
!Analyser ^ search_mode := NewMode,
|
|
handle_search_response(Store, SearchResponse, !Analyser, Response)
|
|
),
|
|
maybe_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).
|
|
|
|
handle_search_response(Store, SearchResponse, !Analyser, AnalyserResponse) :-
|
|
(
|
|
SearchResponse = search_response_question(SuspectId, Reason),
|
|
SearchSpace = !.Analyser ^ search_space,
|
|
Node = get_edt_node(SearchSpace, SuspectId),
|
|
edt_question(Store, Node, OracleQuestion),
|
|
( if
|
|
(
|
|
suspect_unknown(SearchSpace, SuspectId)
|
|
;
|
|
suspect_skipped(SearchSpace, SuspectId)
|
|
)
|
|
then
|
|
AnalyserResponse =
|
|
analyser_response_oracle_question(OracleQuestion)
|
|
else if
|
|
suspect_ignored(SearchSpace, SuspectId)
|
|
then
|
|
% Searches should not respond with questions about suspects we
|
|
% already know to be trusted.
|
|
throw(internal_error("handle_search_response",
|
|
"search responded with query about ignored suspect"))
|
|
else
|
|
% We already known something about this suspect, but the search
|
|
% wants the oracle to be requeried. This may happen if the
|
|
% search thinks the user might have answered the question
|
|
% incorrectly before.
|
|
AnalyserResponse = analyser_response_revise(OracleQuestion)
|
|
),
|
|
!Analyser ^ last_search_question :=
|
|
yes(suspect_and_reason(SuspectId, Reason))
|
|
;
|
|
SearchResponse = search_response_require_explicit_subtree(SuspectId),
|
|
!Analyser ^ require_explicit := yes(explicit_subtree(
|
|
SuspectId)),
|
|
Node = get_edt_node(!.Analyser ^ search_space, SuspectId),
|
|
AnalyserResponse = analyser_response_require_explicit_subtree(Node)
|
|
;
|
|
SearchResponse = search_response_require_explicit_supertree,
|
|
!Analyser ^ require_explicit := yes(explicit_supertree),
|
|
SearchSpace = !.Analyser ^ search_space,
|
|
topmost_det(SearchSpace, TopMostId),
|
|
TopMost = get_edt_node(SearchSpace, TopMostId),
|
|
AnalyserResponse =
|
|
analyser_response_require_explicit_supertree(TopMost)
|
|
;
|
|
SearchResponse = search_response_no_suspects,
|
|
AnalyserResponse = analyser_response_no_suspects
|
|
;
|
|
SearchResponse = search_response_found_bug(BugId, CorrectDescendants,
|
|
InadmissibleChildren),
|
|
bug_response(Store, !.Analyser ^ search_space, BugId,
|
|
[BugId | CorrectDescendants], InadmissibleChildren,
|
|
AnalyserResponse)
|
|
).
|
|
|
|
% bug_response(Store, SearchSpace, BugId, Evidence, InadmissibleChildren,
|
|
% Response):
|
|
%
|
|
% Create a bug analyser-response using the given Evidence.
|
|
% If InadmissibleChildren isn't empty then an i_bug will be created,
|
|
% otherwise an e_bug will be created.
|
|
%
|
|
:- pred bug_response(S::in, search_space(T)::in,
|
|
suspect_id::in, list(suspect_id)::in, list(suspect_id)::in,
|
|
analyser_response(T)::out) is det <= mercury_edt(S, T).
|
|
|
|
bug_response(Store, SearchSpace, BugId, Evidence, InadmissibleChildren,
|
|
Response) :-
|
|
BugNode = get_edt_node(SearchSpace, BugId),
|
|
(
|
|
InadmissibleChildren = [InadmissibleChild | _],
|
|
edt_get_i_bug(Store, BugNode,
|
|
get_edt_node(SearchSpace, InadmissibleChild), IBug),
|
|
Bug = i_bug(IBug)
|
|
;
|
|
InadmissibleChildren = [],
|
|
edt_get_e_bug(Store, BugNode, EBug),
|
|
Bug = e_bug(EBug)
|
|
),
|
|
EDTNodes = list.map(get_edt_node(SearchSpace), Evidence),
|
|
list.map(edt_question(Store), EDTNodes,
|
|
EvidenceAsQuestions),
|
|
Response = analyser_response_bug_found(Bug, EvidenceAsQuestions).
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
% Search the search space for a question for the oracle. The search
|
|
% should respond with a question about a suspect, or a request for an
|
|
% explicit subtree to be generated. A new search mode is returned so
|
|
% that the search algorithm being used can remember its current state
|
|
% next time round.
|
|
%
|
|
:- pred search_for_question(S::in, oracle_state::in,
|
|
search_space(T)::in, search_space(T)::out,
|
|
search_mode::in, search_mode::in,
|
|
search_mode::out, search_response::out) is det <= mercury_edt(S, T).
|
|
|
|
search_for_question(Store, Oracle, !SearchSpace, OldMode, FallBackSearchMode,
|
|
NewMode, Response) :-
|
|
(
|
|
OldMode = analyser_top_down,
|
|
top_down_search(Store, Oracle, !SearchSpace, Response),
|
|
% We always go back to the fallback search mode after a top-down
|
|
% search, because some fallback searches (such as divide and query)
|
|
% use top-down as a fail safe and we want the fallback search to
|
|
% resume after the top-down search.
|
|
NewMode = FallBackSearchMode
|
|
;
|
|
OldMode = analyser_follow_subterm_end(SuspectId, ArgPos, TermPath,
|
|
LastUnknown, HowTrack),
|
|
follow_subterm_end_search(Store, Oracle, !SearchSpace, HowTrack,
|
|
LastUnknown, SuspectId, ArgPos, TermPath, FallBackSearchMode,
|
|
NewMode, Response)
|
|
;
|
|
OldMode = analyser_binary(PathArray, Top - Bottom, LastTested),
|
|
binary_search(Store, Oracle, PathArray, Top, Bottom, LastTested,
|
|
!SearchSpace, FallBackSearchMode, NewMode, Response)
|
|
;
|
|
OldMode = analyser_divide_and_query(Weighting),
|
|
divide_and_query_search(Store, Oracle, Weighting, !SearchSpace,
|
|
Response, NewMode)
|
|
).
|
|
|
|
:- pred top_down_search(S::in, oracle_state::in,
|
|
search_space(T)::in, search_space(T)::out,
|
|
search_response::out) is det <= mercury_edt(S, T).
|
|
|
|
top_down_search(Store, Oracle, !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.
|
|
|
|
( if root(!.SearchSpace, RootId) then
|
|
Start = RootId
|
|
else
|
|
topmost_det(!.SearchSpace, Start)
|
|
),
|
|
first_unknown_descendant(Store, Oracle, Start, !SearchSpace,
|
|
MaybeUnknownDescendant),
|
|
(
|
|
MaybeUnknownDescendant = found(Unknown),
|
|
Response = search_response_question(Unknown, ques_reason_top_down)
|
|
;
|
|
MaybeUnknownDescendant = not_found,
|
|
( if
|
|
choose_skipped_suspect(!.SearchSpace, SkippedSuspect)
|
|
then
|
|
Response = search_response_question(SkippedSuspect,
|
|
ques_reason_skipped)
|
|
else if
|
|
% Since the are no skipped suspects and no unknown suspects
|
|
% in the search space, if there is a root (i.e. an erroneous
|
|
% suspect), then it must be a bug. Note that only top down search
|
|
% actually checks if a bug was found. This is okay, since all the
|
|
% other search algorithms call top down search if they can't find
|
|
% an unknown suspect.
|
|
root(!.SearchSpace, BugId)
|
|
then
|
|
( if
|
|
children(Store, Oracle, BugId, !SearchSpace, BugChildren),
|
|
non_ignored_descendants(Store, Oracle, BugChildren,
|
|
!SearchSpace, NonIgnoredDescendants),
|
|
list.filter(suspect_correct_or_inadmissible(!.SearchSpace),
|
|
NonIgnoredDescendants, CorrectDescendants, [])
|
|
then
|
|
list.filter(suspect_inadmissible(!.SearchSpace), BugChildren,
|
|
InadmissibleChildren),
|
|
Response = search_response_found_bug(BugId, CorrectDescendants,
|
|
InadmissibleChildren)
|
|
else
|
|
throw(internal_error("top_down_search",
|
|
"bug has unexplored or unknown children"))
|
|
)
|
|
else
|
|
% 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.
|
|
( if
|
|
extend_search_space_upwards(Store, Oracle, !.SearchSpace,
|
|
ExtendedSearchSpace)
|
|
then
|
|
top_down_search(Store, Oracle, ExtendedSearchSpace,
|
|
!:SearchSpace, Response)
|
|
else
|
|
topmost_det(!.SearchSpace, TopMostId),
|
|
TopMostNode = get_edt_node(!.SearchSpace, TopMostId),
|
|
( if edt_topmost_node(Store, TopMostNode) then
|
|
% We can't look any higher.
|
|
Response = search_response_no_suspects
|
|
else
|
|
Response = search_response_require_explicit_supertree
|
|
)
|
|
)
|
|
)
|
|
;
|
|
MaybeUnknownDescendant = require_explicit_subtree(RequireExplicitId),
|
|
Response = search_response_require_explicit_subtree(RequireExplicitId)
|
|
).
|
|
|
|
:- pred follow_subterm_end_search(S::in, oracle_state::in,
|
|
search_space(T)::in, search_space(T)::out, how_track_subterm::in,
|
|
maybe(suspect_id)::in, suspect_id::in,
|
|
arg_pos::in, term_path::in, search_mode::in, search_mode::out,
|
|
search_response::out) is det <= mercury_edt(S, T).
|
|
|
|
follow_subterm_end_search(Store, Oracle, !SearchSpace, HowTrack,
|
|
LastUnknown, SuspectId, ArgPos, TermPath, FallBackSearchMode,
|
|
NewMode, SearchResponse) :-
|
|
follow_subterm_end_search_2(Store, Oracle, !SearchSpace, HowTrack,
|
|
map.init, _, LastUnknown, SuspectId, ArgPos, TermPath,
|
|
FallBackSearchMode, NewMode, SearchResponse).
|
|
|
|
:- pred follow_subterm_end_search_2(S::in, oracle_state::in,
|
|
search_space(T)::in, search_space(T)::out, how_track_subterm::in,
|
|
map(proc_layout, unit)::in, map(proc_layout, unit)::out,
|
|
maybe(suspect_id)::in, suspect_id::in,
|
|
arg_pos::in, term_path::in, search_mode::in, search_mode::out,
|
|
search_response::out) is det <= mercury_edt(S, T).
|
|
|
|
follow_subterm_end_search_2(Store, Oracle, !SearchSpace, HowTrack,
|
|
!TriedShortcutProcs, LastUnknown, SuspectId, ArgPos, TermPath,
|
|
FallBackSearchMode, NewMode, SearchResponse) :-
|
|
find_subterm_origin(Store, Oracle, SuspectId, ArgPos, TermPath, HowTrack,
|
|
!TriedShortcutProcs, !SearchSpace, FindOriginResponse),
|
|
(
|
|
FindOriginResponse = primitive_op(BindingSuspectId, FileName,
|
|
LineNo, PrimOpType, Output),
|
|
ProcLabel = get_proc_label_for_suspect(Store, !.SearchSpace,
|
|
BindingSuspectId),
|
|
(
|
|
Output = yes,
|
|
% BindingSuspectId = SuspectId since the subterm is an output
|
|
% of SuspectId.
|
|
BindingNode = get_edt_node(!.SearchSpace, SuspectId),
|
|
ArgNum = edt_arg_pos_to_user_arg_num(Store, BindingNode, ArgPos),
|
|
MaybePath = yes([ArgNum | TermPath])
|
|
;
|
|
Output = no,
|
|
% Since the subterm is not an output of the binding node,
|
|
% it will not appear in any of the arguments of the binding node
|
|
% (it can't be an input, because then it would have been bound
|
|
% outside the node).
|
|
MaybePath = no
|
|
),
|
|
( if
|
|
% We ask about the binding node even if it was previously skipped,
|
|
% since this behaviour is more predictable from the user's
|
|
% perspective.
|
|
|
|
( suspect_unknown(!.SearchSpace, BindingSuspectId)
|
|
; suspect_skipped(!.SearchSpace, BindingSuspectId)
|
|
)
|
|
then
|
|
SearchResponse = search_response_question(BindingSuspectId,
|
|
ques_reason_binding_node(PrimOpType, FileName, LineNo,
|
|
MaybePath, ProcLabel, no)),
|
|
NewMode = FallBackSearchMode
|
|
else
|
|
( if
|
|
LastUnknown = yes(Unknown),
|
|
suspect_still_unknown(!.SearchSpace, Unknown)
|
|
then
|
|
Reason = ques_reason_binding_node(PrimOpType,
|
|
FileName, LineNo, MaybePath, ProcLabel, yes),
|
|
SearchResponse = search_response_question(Unknown, Reason),
|
|
NewMode = FallBackSearchMode
|
|
else
|
|
search_for_question(Store, Oracle, !SearchSpace,
|
|
FallBackSearchMode, FallBackSearchMode, NewMode,
|
|
SearchResponse)
|
|
)
|
|
)
|
|
;
|
|
FindOriginResponse = not_found,
|
|
( if
|
|
LastUnknown = yes(Unknown),
|
|
suspect_still_unknown(!.SearchSpace, Unknown)
|
|
then
|
|
SearchResponse = search_response_question(Unknown,
|
|
ques_reason_subterm_no_proc_rep),
|
|
NewMode = FallBackSearchMode
|
|
else
|
|
search_for_question(Store, Oracle, !SearchSpace,
|
|
FallBackSearchMode, FallBackSearchMode,
|
|
NewMode, SearchResponse)
|
|
)
|
|
;
|
|
FindOriginResponse = require_explicit_subtree,
|
|
SearchResponse = search_response_require_explicit_subtree(SuspectId),
|
|
|
|
% Record the current position of the search so we can continue
|
|
% where we left off once the explicit subtree has been generated.
|
|
NewMode = analyser_follow_subterm_end(SuspectId, ArgPos, TermPath,
|
|
LastUnknown, HowTrack)
|
|
;
|
|
FindOriginResponse = require_explicit_supertree,
|
|
SearchResponse = search_response_require_explicit_supertree,
|
|
NewMode = analyser_follow_subterm_end(SuspectId, ArgPos, TermPath,
|
|
LastUnknown, HowTrack)
|
|
;
|
|
FindOriginResponse = origin(OriginId, OriginArgPos,
|
|
OriginTermPath, SubtermMode),
|
|
( if
|
|
suspect_unknown(!.SearchSpace, OriginId)
|
|
then
|
|
NewLastUnknown = yes(OriginId)
|
|
else
|
|
NewLastUnknown = LastUnknown
|
|
),
|
|
( if
|
|
% Check if it's worth continuing tracking the sub-term.
|
|
% We want to stop if we enter a portion of the search space
|
|
% known not to contain the bug from which we can't return
|
|
% (for example if we come across an erroneous node where
|
|
% the sub-term is an input).
|
|
|
|
give_up_subterm_tracking(!.SearchSpace, OriginId, SubtermMode)
|
|
then
|
|
( if
|
|
LastUnknown = yes(Unknown),
|
|
suspect_still_unknown(!.SearchSpace, Unknown)
|
|
then
|
|
SearchResponse = search_response_question(Unknown,
|
|
ques_reason_binding_node_eliminated),
|
|
NewMode = FallBackSearchMode
|
|
else
|
|
search_for_question(Store, Oracle, !SearchSpace,
|
|
FallBackSearchMode, FallBackSearchMode,
|
|
NewMode, SearchResponse)
|
|
)
|
|
else
|
|
% This recursive call will not lead to an infinite loop
|
|
% because eventually either the sub-term will be bound
|
|
% (and find_subterm_origin will respond with primitive_op/3)
|
|
% or there will be insufficient tracing information to continue
|
|
% (and find_subterm_origin will respond with not_found).
|
|
|
|
follow_subterm_end_search_2(Store, Oracle, !SearchSpace, HowTrack,
|
|
!TriedShortcutProcs, NewLastUnknown, OriginId,
|
|
OriginArgPos, OriginTermPath,
|
|
FallBackSearchMode, NewMode, SearchResponse)
|
|
)
|
|
).
|
|
|
|
% setup_binary_search(SearchSpace, SuspectId, SearchMode):
|
|
%
|
|
% Sets up the search mode to do a binary search between SuspectId
|
|
% and either the root of the search space if a suspect has previously been
|
|
% marked erroneous, or the topmost node if no suspect has yet been marked
|
|
% erroneous.
|
|
%
|
|
:- pred setup_binary_search(search_space(T)::in, suspect_id::in,
|
|
search_mode::out) is det.
|
|
|
|
setup_binary_search(SearchSpace, SuspectId, SearchMode) :-
|
|
( if root(SearchSpace, RootId) then
|
|
TopId = RootId,
|
|
BottomId = SuspectId
|
|
else
|
|
topmost_det(SearchSpace, TopId),
|
|
BottomId = SuspectId
|
|
),
|
|
( if get_path(SearchSpace, BottomId, TopId, Path) then
|
|
PathArray = array.from_list(Path),
|
|
array.bounds(PathArray, Top, Bottom),
|
|
SearchMode = analyser_binary(PathArray, Top - Bottom, Bottom)
|
|
else
|
|
throw(internal_error("setup_binary_search",
|
|
"TopId not an ancestor of BottomId"))
|
|
).
|
|
|
|
:- pred binary_search(S::in, oracle_state::in,
|
|
array(suspect_id)::in, int::in, int::in, int::in,
|
|
search_space(T)::in, search_space(T)::out, search_mode::in,
|
|
search_mode::out, search_response::out) is det <= mercury_edt(S, T).
|
|
|
|
binary_search(Store, Oracle, PathArray, Top, Bottom, LastTested,
|
|
!SearchSpace, FallBackSearchMode, NewMode, Response) :-
|
|
SuspectId = PathArray ^ elem(LastTested),
|
|
|
|
% Check what the result of the query about LastTested was and adjust
|
|
% the range appropriately.
|
|
( if
|
|
% The oracle answered `erroneous'.
|
|
suspect_in_excluded_complement(!.SearchSpace, SuspectId)
|
|
then
|
|
NewTop = LastTested + 1,
|
|
NewBottom = Bottom
|
|
else if
|
|
% The oracle answered `correct' or `inadmissible'
|
|
suspect_in_excluded_subtree(!.SearchSpace, SuspectId)
|
|
then
|
|
NewTop = Top,
|
|
NewBottom = LastTested - 1
|
|
else
|
|
% The suspect is trusted(ignored) or was skipped.
|
|
NewTop = Top,
|
|
NewBottom = Bottom
|
|
),
|
|
( if
|
|
NewTop > NewBottom
|
|
then
|
|
% Revert to the fallback search mode when binary search is over.
|
|
search_for_question(Store, Oracle, !SearchSpace,
|
|
FallBackSearchMode, FallBackSearchMode, NewMode, Response)
|
|
else
|
|
( if
|
|
find_unknown_closest_to_middle(!.SearchSpace, PathArray,
|
|
NewTop, NewBottom, UnknownClosestToMiddle)
|
|
then
|
|
NewMode = analyser_binary(PathArray, NewTop - NewBottom,
|
|
UnknownClosestToMiddle),
|
|
Response = search_response_question(
|
|
PathArray ^ elem(UnknownClosestToMiddle),
|
|
ques_reason_binary(NewBottom, NewTop, UnknownClosestToMiddle))
|
|
else
|
|
% No unknown suspects on the path, so revert to the fallback
|
|
% search mode.
|
|
search_for_question(Store, Oracle, !SearchSpace,
|
|
FallBackSearchMode, FallBackSearchMode, NewMode, Response)
|
|
)
|
|
).
|
|
|
|
% find_unknown_closest_to_middle(SearchSpace, PathArray, Top, Bottom,
|
|
% Unknown):
|
|
%
|
|
% Unknown is the position in PathArray of the suspect which has status
|
|
% unknown and is closest to halfway between From and To which are
|
|
% also indexes into PathArray. Fails if there are no unknown suspects
|
|
% between From and To (inclusive).
|
|
%
|
|
:- pred find_unknown_closest_to_middle(search_space(T)::in,
|
|
array(suspect_id)::in, int::in, int::in, int::out) is semidet.
|
|
|
|
find_unknown_closest_to_middle(SearchSpace, PathArray, Top, Bottom, Unknown) :-
|
|
Middle = Top + ((Bottom - Top) // 2),
|
|
find_unknown_closest_to_range(SearchSpace, PathArray, Top, Bottom,
|
|
Middle, Middle, Unknown).
|
|
|
|
% find_unknown_closest_to_range(SearchSpace, PathArray, OuterTop,
|
|
% OuterBottom, InnerTop, InnerBottom, Unknown):
|
|
%
|
|
% Unknown is a position in PathArray between OuterTop and OuterBottom
|
|
% (inclusive) where the status of the suspect is unknown. The preferred
|
|
% position to return is as close as possible to InnerTop and
|
|
% InnerBottom, with the proviso that elements between InnerTop and
|
|
% InnerBottom (exclusive) aren't tested, since the caller has already
|
|
% found they were not unknown.
|
|
%
|
|
:- pred find_unknown_closest_to_range(search_space(T)::in,
|
|
array(suspect_id)::in, int::in, int::in, int::in, int::in, int::out)
|
|
is semidet.
|
|
|
|
find_unknown_closest_to_range(SearchSpace, PathArray, OuterTop, OuterBottom,
|
|
InnerTop, InnerBottom, Unknown) :-
|
|
InnerTop =< InnerBottom,
|
|
( OuterTop =< InnerTop ; InnerBottom =< OuterBottom ),
|
|
( if
|
|
OuterTop =< InnerTop,
|
|
suspect_unknown(SearchSpace, PathArray ^ elem(InnerTop))
|
|
then
|
|
Unknown = InnerTop
|
|
else if
|
|
InnerBottom =< OuterBottom,
|
|
suspect_unknown(SearchSpace, PathArray ^ elem(InnerBottom))
|
|
then
|
|
Unknown = InnerBottom
|
|
else
|
|
find_unknown_closest_to_range(SearchSpace, PathArray,
|
|
OuterTop, OuterBottom, InnerTop - 1, InnerBottom + 1, Unknown)
|
|
).
|
|
|
|
:- pred divide_and_query_search(S::in, oracle_state::in,
|
|
weighting_heuristic::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, Oracle, Weighting, !SearchSpace,
|
|
Response, analyser_divide_and_query(Weighting)) :-
|
|
% If there's no root yet (because the oracle hasn't asserted any nodes
|
|
% are erroneous yet), then use top-down search.
|
|
( if root(!.SearchSpace, RootId) then
|
|
( if children(Store, Oracle, RootId, !SearchSpace, Children) then
|
|
find_middle_weight(Store, Oracle, Weighting, Children,
|
|
RootId, no, !SearchSpace, Response)
|
|
else
|
|
Response = search_response_require_explicit_subtree(RootId)
|
|
)
|
|
else
|
|
top_down_search(Store, Oracle, !SearchSpace, Response)
|
|
).
|
|
|
|
% Call find_middle_weight if we are able to find the children of the
|
|
% given suspect id, otherwise return a require_explicit_subtree
|
|
% search response in the last argument.
|
|
%
|
|
:- pred find_middle_weight_if_children(S::in,
|
|
oracle_state::in, weighting_heuristic::in, 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_if_children(Store, Oracle, Weighting, SuspectId, TopId,
|
|
MaybeLastUnknown, !SearchSpace, Response) :-
|
|
( if children(Store, Oracle, SuspectId, !SearchSpace, Children) then
|
|
find_middle_weight(Store, Oracle, Weighting, Children, TopId,
|
|
MaybeLastUnknown, !SearchSpace, Response)
|
|
else
|
|
Response = search_response_require_explicit_subtree(SuspectId)
|
|
).
|
|
|
|
% find_middle_weight(Store, Oracle, Weighting, SuspectIds,
|
|
% TopId, MaybeLastUnknown, !SearchSpace, Response):
|
|
%
|
|
% Find the unknown suspect whose weight is closest to half the weight
|
|
% of TopId, considering only the heaviest suspect in SuspectIds, the
|
|
% heaviest child of the heaviest suspect in SuspectIds and so on.
|
|
% MaybeLastUnknown is the last node that was unknown in the search
|
|
% (if any).
|
|
%
|
|
:- pred find_middle_weight(S::in, oracle_state::in,
|
|
weighting_heuristic::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, Oracle, Weighting, [], TopId,
|
|
MaybeLastUnknown, !SearchSpace, Response) :-
|
|
( if
|
|
MaybeLastUnknown = yes(LastUnknown),
|
|
suspect_still_unknown(!.SearchSpace, LastUnknown)
|
|
then
|
|
Response = search_response_question(LastUnknown,
|
|
ques_reason_divide_and_query(Weighting,
|
|
get_weight(!.SearchSpace, TopId),
|
|
get_weight(!.SearchSpace, LastUnknown)))
|
|
else
|
|
% 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, Oracle, !SearchSpace, Response)
|
|
).
|
|
find_middle_weight(Store, Oracle, Weighting, [SuspectId | SuspectIds], TopId,
|
|
MaybeLastUnknown, !SearchSpace, Response) :-
|
|
TopWeight = get_weight(!.SearchSpace, TopId),
|
|
Target = TopWeight // 2,
|
|
|
|
% Find the heaviest suspect.
|
|
Weight = get_weight(!.SearchSpace, SuspectId),
|
|
list.foldl2(max_weight(!.SearchSpace), SuspectIds,
|
|
Weight, MaxWeight, SuspectId, Heaviest),
|
|
( if MaxWeight > Target then
|
|
( if suspect_unknown(!.SearchSpace, Heaviest) then
|
|
NewMaybeLastUnknown = yes(Heaviest)
|
|
else
|
|
NewMaybeLastUnknown = MaybeLastUnknown
|
|
),
|
|
find_middle_weight_if_children(Store, Oracle, Weighting, Heaviest,
|
|
TopId, NewMaybeLastUnknown, !SearchSpace, Response)
|
|
else
|
|
( if suspect_unknown(!.SearchSpace, Heaviest) then
|
|
( if
|
|
MaybeLastUnknown = yes(LastUnknown),
|
|
suspect_still_unknown(!.SearchSpace, LastUnknown)
|
|
then
|
|
LastUnknownWeight = get_weight(!.SearchSpace, LastUnknown),
|
|
|
|
% If the last unknown suspect was closer to the target weight,
|
|
% then ask about it.
|
|
( if LastUnknownWeight - Target < Target - MaxWeight then
|
|
Response = search_response_question(LastUnknown,
|
|
ques_reason_divide_and_query(Weighting, TopWeight,
|
|
LastUnknownWeight))
|
|
else
|
|
Response = search_response_question(Heaviest,
|
|
ques_reason_divide_and_query(Weighting, TopWeight,
|
|
MaxWeight))
|
|
)
|
|
else
|
|
Response = search_response_question(Heaviest,
|
|
ques_reason_divide_and_query(Weighting, TopWeight,
|
|
MaxWeight))
|
|
)
|
|
else
|
|
( if
|
|
MaybeLastUnknown = yes(LastUnknown),
|
|
suspect_still_unknown(!.SearchSpace, LastUnknown)
|
|
then
|
|
LastUnknownWeight = get_weight(!.SearchSpace, LastUnknown),
|
|
Response = search_response_question(LastUnknown,
|
|
ques_reason_divide_and_query(Weighting, TopWeight,
|
|
LastUnknownWeight))
|
|
else
|
|
% Look deeper until we find an unknown.
|
|
find_middle_weight_if_children(Store, Oracle, Weighting,
|
|
Heaviest, TopId, no, !SearchSpace, Response)
|
|
)
|
|
)
|
|
).
|
|
|
|
:- pred max_weight(search_space(T)::in, suspect_id::in,
|
|
int::in, int::out, suspect_id::in, suspect_id::out) is det.
|
|
|
|
max_weight(SearchSpace, SuspectId, PrevMax, NewMax,
|
|
PrevSuspectId, NewSuspectId) :-
|
|
Weight = get_weight(SearchSpace, SuspectId),
|
|
( if Weight > PrevMax then
|
|
NewMax = Weight,
|
|
NewSuspectId = SuspectId
|
|
else
|
|
NewMax = PrevMax,
|
|
NewSuspectId = PrevSuspectId
|
|
).
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
% Check that a suspect is still unknown. This is called by the search
|
|
% algorithms to make double sure that a suspect is still unknown (it
|
|
% might not be unknown if, for example, an erroneous suspect was added
|
|
% to the search space during the search).
|
|
%
|
|
:- pred suspect_still_unknown(search_space(T)::in, suspect_id::in) is semidet.
|
|
|
|
suspect_still_unknown(SearchSpace, SuspectId) :-
|
|
suspect_unknown(SearchSpace, SuspectId).
|
|
|
|
%-----------------------------------------------------------------------------%
|
|
|
|
reason_to_string(ques_reason_start) =
|
|
"this is the node where the `dd' command was issued.".
|
|
reason_to_string(ques_reason_binding_node(PrimOpType, FileName, LineNo,
|
|
MaybePath, ProcLabel, Eliminated)) = Str :-
|
|
PrimOpStr = primitive_op_type_to_string(PrimOpType),
|
|
LineNoStr = int_to_string(LineNo),
|
|
get_pred_attributes(ProcLabel, SymModule, Name, Arity, PredOrFunc),
|
|
(
|
|
PredOrFunc = pf_function,
|
|
PredOrFuncStr = "function"
|
|
;
|
|
PredOrFunc = pf_predicate,
|
|
PredOrFuncStr = "predicate"
|
|
),
|
|
Module = sym_name_to_string(SymModule),
|
|
ArityStr = int_to_string(Arity),
|
|
(
|
|
Eliminated = yes,
|
|
EliminatedSent = " That node was, however, previously "
|
|
++ "eliminated from the bug search."
|
|
;
|
|
Eliminated = no,
|
|
EliminatedSent = ""
|
|
),
|
|
(
|
|
MaybePath = yes(Path),
|
|
PathStrings = list.map(int_to_string, Path),
|
|
PathStr = string.join_list("/", PathStrings),
|
|
PathSent = "The path to the subterm in the atom is " ++ PathStr ++ "."
|
|
;
|
|
MaybePath = no,
|
|
PathSent = ""
|
|
),
|
|
Str = "the marked subterm was bound by the " ++
|
|
PrimOpStr ++ " inside the " ++ PredOrFuncStr ++
|
|
" " ++ Module ++ "." ++ Name ++ "/" ++ ArityStr ++
|
|
" (" ++ FileName ++ ":" ++ LineNoStr ++ "). " ++
|
|
PathSent ++ EliminatedSent.
|
|
reason_to_string(ques_reason_top_down) =
|
|
"this is the next node in the top-down search.".
|
|
reason_to_string(ques_reason_subterm_no_proc_rep) =
|
|
"tracking of the marked subterm had to be aborted here, because of "
|
|
++ "missing tracing information.".
|
|
reason_to_string(ques_reason_binding_node_eliminated) =
|
|
"tracking of the marked subterm was stopped here, because the binding "
|
|
++ "node lies in a portion of the tree which has been eliminated.".
|
|
reason_to_string(ques_reason_binary(Bottom, Top, Split)) = Str :-
|
|
PathLengthStr = int_to_string_thousands(Bottom - Top + 1),
|
|
SubPath1LengthStr = int_to_string_thousands(Bottom - Split),
|
|
SubPath2LengthStr = int_to_string_thousands(Split - Top + 1),
|
|
Str = "this node divides a path of length " ++ PathLengthStr
|
|
++ " into two paths of length " ++
|
|
SubPath1LengthStr ++ " and " ++ SubPath2LengthStr ++ ".".
|
|
reason_to_string(ques_reason_divide_and_query(Weighting, OldWeight,
|
|
SubtreeWeight)) =
|
|
weighting_to_reason_string(Weighting, OldWeight - SubtreeWeight,
|
|
SubtreeWeight).
|
|
reason_to_string(ques_reason_skipped) =
|
|
"there are no more non-skipped questions left.".
|
|
reason_to_string(ques_reason_revise) =
|
|
"this question is being revisited, because of "
|
|
++ "an unsuccessful previous bug search.".
|
|
|
|
:- func weighting_to_reason_string(weighting_heuristic, int, int) = string.
|
|
|
|
weighting_to_reason_string(number_of_events, Weight1, Weight2) = Str :-
|
|
Weight1Str = int_to_string_thousands(Weight1),
|
|
Weight2Str = int_to_string_thousands(Weight2),
|
|
Str = "this node divides the suspect area into two regions of "
|
|
++ Weight1Str ++ " and " ++ Weight2Str ++ " events each.".
|
|
weighting_to_reason_string(suspicion, Weight1, Weight2) = Str :-
|
|
Weight1Str = int_to_string_thousands(Weight1),
|
|
Weight2Str = int_to_string_thousands(Weight2),
|
|
Str = "this node divides the suspect area into " ++
|
|
"two regions of suspicion " ++ Weight1Str ++ " and
|
|
" ++ Weight2Str ++ ".".
|
|
|
|
show_info(Store, OutStream, Analyser, !IO) :-
|
|
SearchSpace = Analyser ^ search_space,
|
|
some [!FieldNames, !Data] (
|
|
!:FieldNames = [],
|
|
!:Data = [],
|
|
|
|
% Get the context of the current question.
|
|
(
|
|
Analyser ^ last_search_question =
|
|
yes(suspect_and_reason(LastId, Reason)),
|
|
( if
|
|
edt_context(Store, get_edt_node(SearchSpace,
|
|
LastId), FileName - LineNo, MaybeReturnContext)
|
|
then
|
|
(
|
|
MaybeReturnContext = yes(ReturnFileName - ReturnLineNo),
|
|
ContextStr = FileName ++ ":" ++ int_to_string(LineNo)
|
|
++ " (" ++ ReturnFileName ++ ":"
|
|
++ int_to_string(ReturnLineNo) ++ ")"
|
|
;
|
|
MaybeReturnContext = no,
|
|
ContextStr = FileName ++ ":" ++ int_to_string(LineNo)
|
|
),
|
|
list.append(!.FieldNames, ["Context of current question"],
|
|
!:FieldNames),
|
|
list.append(!.Data, [ContextStr], !:Data)
|
|
else
|
|
true
|
|
)
|
|
;
|
|
Analyser ^ last_search_question = no,
|
|
throw(internal_error("show_info", "no last question"))
|
|
),
|
|
|
|
!:FieldNames = !.FieldNames ++ ["Search mode"],
|
|
!:Data = !.Data ++ [search_mode_to_string(Analyser ^ search_mode)],
|
|
|
|
MaybeWeighting = get_current_maybe_weighting(SearchSpace),
|
|
( if MaybeWeighting = yes(number_of_events) then
|
|
( if root(SearchSpace, RootId) then
|
|
StartId = RootId
|
|
else
|
|
topmost_det(SearchSpace, StartId)
|
|
),
|
|
Weight = get_weight(SearchSpace, StartId),
|
|
( if
|
|
Analyser ^ search_mode =
|
|
analyser_divide_and_query(number_of_events)
|
|
then
|
|
!:FieldNames = !.FieldNames ++
|
|
["Estimated questions remaining"],
|
|
EstimatedQuestions = float.ceiling_to_int(
|
|
math.log2(float(Weight))),
|
|
!:Data = !.Data ++ [int_to_string(EstimatedQuestions)]
|
|
else
|
|
true
|
|
),
|
|
!:FieldNames = !.FieldNames ++ ["Number of suspect events"],
|
|
!:Data = !.Data ++ [int_to_string_thousands(Weight)]
|
|
else
|
|
true
|
|
),
|
|
|
|
InfoMessage = string.format_table([left(!.FieldNames), left(!.Data)],
|
|
" : ")
|
|
),
|
|
ReasonStr = reason_to_string(Reason),
|
|
ReasonSent = "The current question was chosen because " ++ ReasonStr,
|
|
WrappedReason = string.word_wrap(ReasonSent, 72),
|
|
io.format(OutStream, "%s\n%s\n", [s(InfoMessage), s(WrappedReason)], !IO).
|
|
|
|
:- func search_mode_to_string(search_mode) = string.
|
|
|
|
search_mode_to_string(analyser_top_down) = "top down".
|
|
search_mode_to_string(analyser_follow_subterm_end(_, _, _, _,
|
|
track_accurate)) =
|
|
"tracking marked sub-term (using accurate algorithm)".
|
|
search_mode_to_string(analyser_follow_subterm_end(_, _, _, _,
|
|
track_fast)) =
|
|
"tracking marked sub-term (using fast algorithm)".
|
|
search_mode_to_string(analyser_binary(_, _, _)) = "binary search on path".
|
|
search_mode_to_string(analyser_divide_and_query(number_of_events)) =
|
|
"divide and query".
|
|
search_mode_to_string(analyser_divide_and_query(suspicion)) =
|
|
"suspicion divide and query".
|