[m-dev.] diff: fix tabling determinism bugs
Fergus Henderson
fjh at cs.mu.OZ.AU
Tue Apr 4 02:20:58 AEST 2000
The reason I didn't include a regression test for the bug fix below is that I
couldn't find a test case which would exercise the bug. I found cases for
which the tabling code was definitely generating HLDS code which was not
determinism-correct -- tests/tabling/unused_args includes one such case --
but the compiler was not rerunning determinism analysis on the HLDS,
so the bug didn't show up.
------------------------------
Estimated hours taken: 3
compiler/table_gen.m:
Fix a bug: the generated code was not determinism-correct.
Also clean up the somewhat obfuscated way that the code
inserted `fail' after calls to table_simple_mark_as_failed
and table_nondet_resume.
library/private_builtin.m:
Add a new predicate table_multi_return_all_ans,
for use by the code generated by table_gen.m.
This is the same as table_nondet_return_all_ans
except that it has determinism `multi' rather than `nondet'.
Workspace: /home/mercury0/fjh/mercury
Index: compiler/table_gen.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/table_gen.m,v
retrieving revision 1.18
diff -u -d -r1.18 table_gen.m
--- compiler/table_gen.m 2000/04/03 11:11:39 1.18
+++ compiler/table_gen.m 2000/04/03 16:04:31
@@ -75,7 +75,8 @@
% then
% impure table_simple_mark_as_succeeded(T2)
% else
-% impure table_simple_mark_as_failed(T2)
+% impure table_simple_mark_as_failed(T2),
+% fail
% )
% ).
%
@@ -113,7 +114,8 @@
% impure table_nondet_suspend(T2, Ans),
% impure table_restore_int_ans(Ans, 0, B)
% else
-% ( % Mark that this subgoal is being
+% (
+% % Mark that this subgoal is being
% % evaluated.
% impure table_nondet_mark_as_active(T2),
%
@@ -131,7 +133,8 @@
% % The following pred is semidet;
% % it will fail if the answer is
% % already in the table.
-% semipure table_nondet_answer_is_not_dupl(AT1),
+% semipure
+% table_nondet_answer_is_not_duplicate(AT1),
%
% % Code to save a new ans in the
% % table.
@@ -238,7 +241,8 @@
table_info_init(Module0, PredInfo0, ProcInfo0, TableInfo0),
% grab the appropriate fields from the pred_info and proc_info
- proc_info_interface_code_model(ProcInfo0, CodeModel),
+ proc_info_interface_determinism(ProcInfo0, Detism),
+ determinism_to_code_model(Detism, CodeModel),
proc_info_headvars(ProcInfo0, HeadVars),
proc_info_varset(ProcInfo0, VarSet0),
proc_info_vartypes(ProcInfo0, VarTypes0),
@@ -247,19 +251,19 @@
(
CodeModel = model_det,
- table_gen__create_new_det_goal(EvalMethod, OrigGoal,
+ table_gen__create_new_det_goal(EvalMethod, Detism, OrigGoal,
PredId, ProcId, HeadVars, ArgModes,
VarTypes0, VarTypes, VarSet0, VarSet,
TableInfo0, TableInfo, Goal)
;
CodeModel = model_semi,
- table_gen__create_new_semi_goal(EvalMethod, OrigGoal,
+ table_gen__create_new_semi_goal(EvalMethod, Detism, OrigGoal,
PredId, ProcId, HeadVars, ArgModes,
VarTypes0, VarTypes, VarSet0, VarSet,
TableInfo0, TableInfo, Goal)
;
CodeModel = model_non,
- table_gen__create_new_non_goal(EvalMethod, OrigGoal,
+ table_gen__create_new_non_goal(EvalMethod, Detism, OrigGoal,
PredId, ProcId, HeadVars, ArgModes,
VarTypes0, VarTypes, VarSet0, VarSet,
TableInfo0, TableInfo, Goal)
@@ -292,13 +296,13 @@
%
% Transform deterministic procedures.
%
-:- pred table_gen__create_new_det_goal(eval_method::in, hlds_goal::in,
- pred_id::in, proc_id::in, list(prog_var)::in, list(mode)::in,
- map(prog_var, type)::in, map(prog_var, type)::out,
+:- pred table_gen__create_new_det_goal(eval_method::in, determinism::in,
+ hlds_goal::in, pred_id::in, proc_id::in, list(prog_var)::in,
+ list(mode)::in, map(prog_var, type)::in, map(prog_var, type)::out,
prog_varset::in, prog_varset::out, table_info::in, table_info::out,
hlds_goal::out) is det.
-table_gen__create_new_det_goal(EvalMethod, OrigGoal, PredId, ProcId,
+table_gen__create_new_det_goal(EvalMethod, Detism, OrigGoal, PredId, ProcId,
HeadVars, HeadVarModes, VarTypes0, VarTypes,
VarSet0, VarSet, TableInfo0, TableInfo, Goal) :-
% even if the original goal doesn't use all of the headvars,
@@ -323,11 +327,21 @@
generate_save_goal(OutputVars, TableVar, Context, VarTypes1, VarTypes2,
VarSet1, VarSet2, TableInfo1, TableInfo, SaveAnsGoal0),
generate_restore_goal(OutputVars, TableVar, Module, Context,
- VarTypes2, VarTypes3, VarSet2, VarSet3, RestoreAnsGoal),
+ VarTypes2, VarTypes3, VarSet2, VarSet3, RestoreAnsGoal0),
generate_call("table_simple_mark_as_inactive", [TableVar], det,
impure, [], Module, Context, MarkAsInactiveGoal),
generate_loop_error_goal(TableInfo, Context, VarTypes3, VarTypes,
VarSet3, VarSet, LoopErrorGoal),
+ ( Detism = erroneous ->
+ % In this case, the RestoreAnsGoal will never be reached,
+ % but to ensure that the generated code is determinism-correct,
+ % we need to make sure that RestoreAnsGoal's determinism is
+ % erroneous. So we use the LoopErrorGoal (which calls error/1)
+ % rather than RestoreAnsGoal0.
+ RestoreAnsGoal = LoopErrorGoal
+ ;
+ RestoreAnsGoal = RestoreAnsGoal0
+ ),
set__insert(OrigNonLocals, TableVar, GenAnsNonLocals),
@@ -387,13 +401,13 @@
%
% Transform semi deterministic procedures
%
-:- pred table_gen__create_new_semi_goal(eval_method::in, hlds_goal::in,
- pred_id::in, proc_id::in, list(prog_var)::in, list(mode)::in,
- map(prog_var, type)::in, map(prog_var, type)::out,
+:- pred table_gen__create_new_semi_goal(eval_method::in, determinism::in,
+ hlds_goal::in, pred_id::in, proc_id::in, list(prog_var)::in,
+ list(mode)::in, map(prog_var, type)::in, map(prog_var, type)::out,
prog_varset::in, prog_varset::out, table_info::in, table_info::out,
hlds_goal::out) is det.
-table_gen__create_new_semi_goal(EvalMethod, OrigGoal, PredId, ProcId,
+table_gen__create_new_semi_goal(EvalMethod, Detism, OrigGoal, PredId, ProcId,
HeadVars, HeadVarModes, VarTypes0, VarTypes,
VarSet0, VarSet, TableInfo0, TableInfo, Goal) :-
% even if the original goal doesn't use all of the headvars,
@@ -421,7 +435,8 @@
generate_loop_error_goal(TableInfo, Context,
VarTypes3, VarTypes, VarSet3, VarSet, LoopErrorGoal),
generate_call("table_simple_mark_as_failed", [TableVar],
- failure, impure, [], Module, Context, MarkAsFailedGoal),
+ det, impure, [], Module, Context, MarkAsFailedGoal0),
+ append_fail(MarkAsFailedGoal0, MarkAsFailedGoal),
generate_call("table_simple_has_succeeded", [TableVar],
semidet, semipure, [], Module, Context, HasSucceededCheckGoal),
generate_call("table_simple_mark_as_inactive", [TableVar],
@@ -495,16 +510,32 @@
"table_gen__create_new_semi_goal: unsupported evaluation model")
),
- RestAnsGoalEx = conj([HasSucceededCheckGoal, RestoreTrueAnsGoal]),
- set__singleton_set(RestNonLocals0, TableVar),
- set__insert_list(RestNonLocals0, OutputVars, RestNonLocals),
- create_instmap_delta([HasSucceededCheckGoal, RestoreTrueAnsGoal],
- RestInstMapDelta0),
- instmap_delta_restrict(RestInstMapDelta0, RestNonLocals,
- RestInstMapDelta),
- init_goal_info(RestNonLocals, RestInstMapDelta, semidet,
- Context, RestAnsGoalInfo),
- RestoreAnsGoal = RestAnsGoalEx - RestAnsGoalInfo,
+ ( Detism = failure ->
+ % We need to treat this case specially,
+ % otherwise the code that we generate would not
+ % be statically determinism-correct: there would
+ % be a path through the procedure which determinism
+ % analysis thinks might succeed. In fact that path
+ % would never be executed, but if this case were not
+ % treated specially, the determinism analysis algorithm
+ % could not prove that. So to ensure that the generated
+ % code is determinism-correct, we replace the bit which
+ % retrieves an answer from the table with an
+ % explicit `fail'.
+ fail_goal(Context, RestoreAnsGoal)
+ ;
+ RestAnsGoalEx =
+ conj([HasSucceededCheckGoal, RestoreTrueAnsGoal]),
+ set__singleton_set(RestNonLocals0, TableVar),
+ set__insert_list(RestNonLocals0, OutputVars, RestNonLocals),
+ create_instmap_delta([HasSucceededCheckGoal,
+ RestoreTrueAnsGoal], RestInstMapDelta0),
+ instmap_delta_restrict(RestInstMapDelta0, RestNonLocals,
+ RestInstMapDelta),
+ init_goal_info(RestNonLocals, RestInstMapDelta, semidet,
+ Context, RestAnsGoalInfo),
+ RestoreAnsGoal = RestAnsGoalEx - RestAnsGoalInfo
+ ),
GenAnsGoalEx = if_then_else([], GenTrueAnsGoal, SaveAnsGoal,
MarkAsFailedGoal, StoreMap),
@@ -537,13 +568,13 @@
%
% Transform non deterministic procedures
%
-:- pred table_gen__create_new_non_goal(eval_method::in, hlds_goal::in,
- pred_id::in, proc_id::in, list(prog_var)::in, list(mode)::in,
- map(prog_var, type)::in, map(prog_var, type)::out,
+:- pred table_gen__create_new_non_goal(eval_method::in, determinism::in,
+ hlds_goal::in, pred_id::in, proc_id::in, list(prog_var)::in,
+ list(mode)::in, map(prog_var, type)::in, map(prog_var, type)::out,
prog_varset::in, prog_varset::out, table_info::in, table_info::out,
hlds_goal::out) is det.
-table_gen__create_new_non_goal(EvalMethod, OrigGoal, PredId, ProcId,
+table_gen__create_new_non_goal(EvalMethod, Detism, OrigGoal, PredId, ProcId,
HeadVars, HeadVarModes, VarTypes0, VarTypes,
VarSet0, VarSet, TableInfo0, TableInfo, Goal) :-
% even if the original goal doesn't use all of the headvars,
@@ -567,7 +598,7 @@
generate_non_save_goal(OutputVars, TableVar, Context,
VarTypes1, VarTypes2, VarSet1, VarSet2, TableInfo1, TableInfo,
SaveAnsGoal0),
- generate_restore_all_goal(OutputVars, TableVar, Module, Context,
+ generate_restore_all_goal(Detism, OutputVars, TableVar, Module, Context,
VarTypes2, VarTypes3, VarSet2, VarSet3, RestoreAllAnsGoal),
generate_call("table_nondet_is_active", [TableVar], semidet, semipure,
[], Module, Context, IsActiveCheckGoal),
@@ -577,11 +608,9 @@
VarSet4, VarSet, LoopErrorGoal),
generate_call("table_nondet_mark_as_active", [TableVar], det, impure,
[], Module, Context, MarkAsActiveGoal),
- generate_call("table_nondet_resume", [TableVar], failure, impure,
+ generate_call("table_nondet_resume", [TableVar], det, impure,
[], Module, Context, ResumeGoal0),
-
- true_goal(TrueGoal),
- fail_goal(FailGoal),
+ append_fail(ResumeGoal0, ResumeGoal1),
map__init(StoreMap),
(
@@ -592,6 +621,7 @@
;
EvalMethod = eval_loop_check
->
+ true_goal(TrueGoal),
SaveAnsGoal = TrueGoal,
ActiveGoal = LoopErrorGoal
;
@@ -617,8 +647,9 @@
(
EvalMethod = eval_minimal
->
- ResumeGoal = ResumeGoal0
+ ResumeGoal = ResumeGoal1
;
+ fail_goal(FailGoal),
ResumeGoal = FailGoal
),
GenAnsGoalEx = disj([GenAnsGoalPart1, ResumeGoal], StoreMap),
@@ -1010,18 +1041,25 @@
init_goal_info(NonLocals, InstMapDelta, det, Context, GoalInfo),
Goal = GoalEx - GoalInfo.
-:- pred generate_restore_all_goal(list(prog_var)::in, prog_var::in,
- module_info::in, term__context::in,
+:- pred generate_restore_all_goal(determinism::in, list(prog_var)::in,
+ prog_var::in, module_info::in, term__context::in,
map(prog_var, type)::in, map(prog_var, type)::out,
prog_varset::in, prog_varset::out, hlds_goal::out) is det.
-generate_restore_all_goal(OutputVars, TableVar, Module, Context,
+generate_restore_all_goal(Detism, OutputVars, TableVar, Module, Context,
VarTypes0, VarTypes, VarSet0, VarSet, Goal) :-
generate_new_table_var("AnswerTable", VarTypes0, VarTypes1,
VarSet0, VarSet1, AnsTableVar),
- generate_call("table_nondet_return_all_ans", [TableVar, AnsTableVar],
- nondet, semipure, [AnsTableVar - ground(unique, no)],
+ ( Detism = multidet ->
+ ReturnAllAns = "table_multi_return_all_ans"
+ ; Detism = nondet ->
+ ReturnAllAns = "table_nondet_return_all_ans"
+ ;
+ error("generate_restore_all_goal: invalid determinism")
+ ),
+ generate_call(ReturnAllAns, [TableVar, AnsTableVar],
+ Detism, semipure, [AnsTableVar - ground(unique, no)],
Module, Context, ReturnAnsBlocksGoal),
generate_restore_goals(OutputVars, AnsTableVar, 0, Module, Context,
@@ -1155,17 +1193,8 @@
goal_feature::in, assoc_list(prog_var, inst)::in, module_info::in,
term__context::in, hlds_goal::out) is det.
-generate_call(PredName, Args, Detism0, Feature, InstMap, Module, Context,
- Goal) :-
- % Implement failure as a det call followed by a fail,
- % as this is more efficient.
- (
- Detism0 = failure
- ->
- Detism = det
- ;
- Detism = Detism0
- ),
+generate_call(PredName, Args, Detism, Feature, InstMap, Module, Context,
+ CallGoal) :-
list__length(Args, Arity),
mercury_private_builtin_module(BuiltinModule),
module_info_get_predicate_table(Module, PredTable),
@@ -1206,8 +1235,9 @@
qualified(BuiltinModule, PredName)),
set__init(NonLocals0),
set__insert_list(NonLocals0, Args, NonLocals),
+ determinism_components(Detism, _CanFail, NumSolns),
(
- Detism = erroneous
+ NumSolns = at_most_zero
->
instmap_delta_init_unreachable(InstMapDelta)
;
@@ -1216,18 +1246,18 @@
init_goal_info(NonLocals, InstMapDelta, Detism, Context,
CallGoalInfo0),
goal_info_add_feature(CallGoalInfo0, Feature, CallGoalInfo),
- CallGoal = Call - CallGoalInfo,
- (
- Detism0 = failure
- ->
- fail_goal(FailGoal),
- instmap_delta_init_unreachable(UnreachInstMapDelta),
- init_goal_info(NonLocals, UnreachInstMapDelta, failure,
- Context, GoalInfo),
- Goal = conj([CallGoal, FailGoal]) - GoalInfo
- ;
- Goal = CallGoal
- ).
+ CallGoal = Call - CallGoalInfo.
+
+:- pred append_fail(hlds_goal::in, hlds_goal::out) is det.
+append_fail(Goal, GoalAndThenFail) :-
+ Goal = _ - GoalInfo,
+ goal_info_get_nonlocals(GoalInfo, NonLocals),
+ goal_info_get_context(GoalInfo, Context),
+ instmap_delta_init_unreachable(UnreachInstMapDelta),
+ init_goal_info(NonLocals, UnreachInstMapDelta, failure,
+ Context, ConjGoalInfo),
+ fail_goal(FailGoal),
+ GoalAndThenFail = conj([Goal, FailGoal]) - ConjGoalInfo.
:- pred gen_int_construction(string::in, int::in,
map(prog_var, type)::in, map(prog_var, type)::out,
Index: library/private_builtin.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/private_builtin.m,v
retrieving revision 1.43
diff -u -d -r1.43 private_builtin.m
--- library/private_builtin.m 2000/03/24 10:27:39 1.43
+++ library/private_builtin.m 2000/04/03 15:09:25
@@ -777,6 +777,8 @@
% Return all of the answer blocks stored in the given table.
:- semipure pred table_nondet_return_all_ans(ml_subgoal_table_node::in,
ml_answer_block::out) is nondet.
+:- semipure pred table_multi_return_all_ans(ml_subgoal_table_node::in,
+ ml_answer_block::out) is multi.
%-----------------------------------------------------------------------------%
@@ -961,7 +963,59 @@
#endif
").
+/*
+** Note that the code for this is identical to the code for
+** table_multi_return_all_ans/2 (below).
+** Any changes to this code should also be made there.
+*/
:- pragma c_code(table_nondet_return_all_ans(T::in, A::out),
+ will_not_call_mercury,
+ local_vars("
+#ifdef MR_USE_MINIMAL_MODEL
+ MR_AnswerList cur_node;
+#else
+ /* ensure local var struct is non-empty */
+ char bogus;
+#endif
+ "),
+ first_code("
+#ifdef MR_USE_MINIMAL_MODEL
+ MR_TrieNode table;
+
+ table = (MR_TrieNode) T;
+ LOCALS->cur_node = table->MR_subgoal->answer_list;
+
+ #ifdef MR_TABLE_DEBUG
+ if (MR_tabledebug) {
+ printf(""restoring all answers in %p -> %p\\n"",
+ table, table->MR_subgoal);
+ }
+ #endif
+#endif
+ "),
+ retry_code("
+ "),
+ shared_code("
+#ifdef MR_USE_MINIMAL_MODEL
+ if (LOCALS->cur_node == NULL) {
+ FAIL;
+ } else {
+ A = (Word) &LOCALS->cur_node->answer_data;
+ LOCALS->cur_node = LOCALS->cur_node->next_answer;
+ SUCCEED;
+ }
+#else
+ fatal_error(""minimal model code entered when not enabled"");
+#endif
+ ")
+).
+
+/*
+** Note that the code for this is identical to the code for
+** table_nondet_return_all_ans/2 (above).
+** Any changes to this code should also be made there.
+*/
+:- pragma c_code(table_multi_return_all_ans(T::in, A::out),
will_not_call_mercury,
local_vars("
#ifdef MR_USE_MINIMAL_MODEL
--
Fergus Henderson <fjh at cs.mu.oz.au> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3 | -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to: mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions: mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------
More information about the developers
mailing list