[m-rev.] diff: avoid runtime aborts from the decl debug oracle

Mark Brown dougl at cs.mu.OZ.AU
Fri Oct 11 05:30:50 AEST 2002


Hi,

This change fixes two of the test cases I recently committed.  There
is still one remaining test case to fix; I'm working on that now.

Cheers,
Mark.

Estimated hours taken: 2
Branches: main

The "complete" and "incomplete" maps in the declarative debugging oracle
can cause a runtime abort if higher order terms are present in the debuggee,
because the maps use sets to represent the solutions to a goal, and sets make
use of builtin comparison.  This change fixes the problem by replacing the
two maps with a single map from initial atom to truth value.  The set of
solutions is no longer stored explicitly.

This change causes no loss of accuracy of the oracle, because we weren't
really using the explicit knowledge about solutions anyway.  The main
drawback of this change is that if in future we implement support for "edit
and continue" style debugging (e.g. by allowing previous answers to be
saved in/restored from a file), we will lose some of the information
pertaining to previous versions of the program, which will make the oracle
slightly less effective at deducing new answers from previous ones.  Since
runtime aborts are a much more serious problem, we will have to live with
this drawback for the moment.

Another solution to this problem may have been to implement a 'set_cc'
module, which would be to 'set' as 'tree234_cc' is to 'tree234'.
Unfortunately, we would need to implement 'set_cc__intersect' but it
appears not to be possible to implement a satisfactory committed choice
version of intersection.

browser/declarative_oracle.m:
	Replace the two maps with the new one, and update the code
	that accesses the knowledge base.

tests/debugger/declarative/Mmakefile:
	Enable tests 'ho3' and 'ho4', which now work.

tests/debugger/declarative/ho3.m:
	Fix a typo in the test case.  It wasn't testing precisely the thing
	it was supposed to test.

tests/debugger/declarative/ho3.exp:
tests/debugger/declarative/ho3.inp:
tests/debugger/declarative/ho4.exp:
tests/debugger/declarative/ho4.inp:
	Input and expected output for the enabled tests.

Index: browser/declarative_oracle.m
===================================================================
RCS file: /home/mercury1/repository/mercury/browser/declarative_oracle.m,v
retrieving revision 1.16
diff -u -r1.16 declarative_oracle.m
--- browser/declarative_oracle.m	3 Oct 2002 07:34:26 -0000	1.16
+++ browser/declarative_oracle.m	10 Oct 2002 11:08:42 -0000
@@ -161,17 +161,13 @@
 		%
 		kb_ground_map :: map_cc(final_decl_atom, decl_truth),
 
-		% Mapping from call atoms to their solution sets.
-		% The sets in this map are all complete---but they may
-		% contain wrong answers.
+		% This map stores knowledge about the completeness of the
+		% set of solutions generated by calling the given initial
+		% atom.  This is used, for example, in the common case that
+		% the user supplies a truth value for a "missing answer"
+		% node.
 		%
-		kb_complete_map :: map_cc(init_decl_atom, final_decl_atoms),
-
-		% Mapping from call atoms to their solution sets.
-		% The sets in this map are all incomplete---there
-		% exists a correct solution which is not in the set.
-		%
-		kb_incomplete_map :: map_cc(init_decl_atom, final_decl_atoms),
+		kb_complete_map :: map_cc(init_decl_atom, decl_truth),
 
 		% Mapping from call atoms to information about which
 		% exceptions are possible or impossible.
@@ -181,8 +177,6 @@
 
 :- type map_cc(K, V) == tree234_cc(K, V).
 
-:- type final_decl_atoms	== set(final_decl_atom).
-
 :- type known_exceptions
 	--->	known_excp(
 			set(univ),		% Possible exceptions.
@@ -192,58 +186,45 @@
 :- pred oracle_kb_init(oracle_kb).
 :- mode oracle_kb_init(out) is det.
 
-oracle_kb_init(oracle_kb(G, Y, N, X)) :-
+oracle_kb_init(oracle_kb(G, C, X)) :-
 	tree234_cc__init(G),
-	tree234_cc__init(Y),
-	tree234_cc__init(N),
+	tree234_cc__init(C),
 	tree234_cc__init(X).
 
 :- pred get_kb_ground_map(oracle_kb, map_cc(final_decl_atom, decl_truth)).
 :- mode get_kb_ground_map(in, out) is det.
 
-get_kb_ground_map(oracle_kb(Map, _, _, _), Map).
+get_kb_ground_map(KB, KB ^ kb_ground_map).
 
 :- pred set_kb_ground_map(oracle_kb, map_cc(final_decl_atom, decl_truth),
 	oracle_kb).
 :- mode set_kb_ground_map(in, in, out) is det.
 
-set_kb_ground_map(oracle_kb(_, Y, N, X), G, oracle_kb(G, Y, N, X)).
+set_kb_ground_map(KB, M, KB ^ kb_ground_map := M).
 
 :- pred get_kb_complete_map(oracle_kb,
-	map_cc(init_decl_atom, final_decl_atoms)).
+	map_cc(init_decl_atom, decl_truth)).
 :- mode get_kb_complete_map(in, out) is det.
 
-get_kb_complete_map(oracle_kb(_, Map, _, _), Map).
+get_kb_complete_map(KB, KB ^ kb_complete_map).
 
 :- pred set_kb_complete_map(oracle_kb,
-	map_cc(init_decl_atom, final_decl_atoms), oracle_kb).
+	map_cc(init_decl_atom, decl_truth), oracle_kb).
 :- mode set_kb_complete_map(in, in, out) is det.
 
-set_kb_complete_map(oracle_kb(G, _, N, X), Y, oracle_kb(G, Y, N, X)).
-
-:- pred get_kb_incomplete_map(oracle_kb,
-	map_cc(init_decl_atom, final_decl_atoms)).
-:- mode get_kb_incomplete_map(in, out) is det.
-
-get_kb_incomplete_map(oracle_kb(_, _, Map, _), Map).
-
-:- pred set_kb_incomplete_map(oracle_kb,
-	map_cc(init_decl_atom, final_decl_atoms), oracle_kb).
-:- mode set_kb_incomplete_map(in, in, out) is det.
-
-set_kb_incomplete_map(oracle_kb(G, Y, _, X), N, oracle_kb(G, Y, N, X)).
+set_kb_complete_map(KB, M, KB ^ kb_complete_map := M).
 
 :- pred get_kb_exceptions_map(oracle_kb,
 	map_cc(init_decl_atom, known_exceptions)).
 :- mode get_kb_exceptions_map(in, out) is det.
 
-get_kb_exceptions_map(oracle_kb(_, _, _, Map), Map).
+get_kb_exceptions_map(KB, KB ^ kb_exceptions_map).
 
 :- pred set_kb_exceptions_map(oracle_kb,
 	map_cc(init_decl_atom, known_exceptions), oracle_kb).
 :- mode set_kb_exceptions_map(in, in, out) is det.
 
-set_kb_exceptions_map(oracle_kb(G, Y, N, _), X, oracle_kb(G, Y, N, X)).
+set_kb_exceptions_map(KB, M, KB ^ kb_exceptions_map := M).
 
 %-----------------------------------------------------------------------------%
 
@@ -279,31 +260,15 @@
 	).
 
 query_oracle_kb(KB, Question, Result) :-
-	Question = missing_answer(Node, Call, Solns),
-	set__list_to_set(Solns, Ss),
+	Question = missing_answer(Node, Call, _Solns),
 	get_kb_complete_map(KB, CMap),
-	tree234_cc__search(CMap, Call, MaybeCSs),
+	tree234_cc__search(CMap, Call, MaybeTruth),
 	(
-		MaybeCSs = yes(CSs),
-		set__subset(CSs, Ss)
-	->
-		Result = yes(truth_value(Node, yes))
+		MaybeTruth = yes(Truth),
+		Result = yes(truth_value(Node, Truth))
 	;
-		get_kb_incomplete_map(KB, IMap),
-		tree234_cc__search(IMap, Call, MaybeISs),
-		(
-			MaybeISs = yes(ISs),
-			(
-				set__subset(Ss, ISs)
-			->
-				Result = yes(truth_value(Node, no))
-			;
-				Result = no
-			)
-		;
-			MaybeISs = no,
-			Result = no
-		)
+		MaybeTruth = no,
+		Result = no
 	).
 
 query_oracle_kb(KB, Question, Result) :-
@@ -344,34 +309,10 @@
 	tree234_cc__set(Map0, Atom, Truth, Map),
 	set_kb_ground_map(KB0, Map, KB).
 
-assert_oracle_kb(missing_answer(_, Call, Solns), truth_value(_, yes),
-		KB0, KB) :-
+assert_oracle_kb(missing_answer(_, Call, _), truth_value(_, Truth), KB0, KB) :-
 	get_kb_complete_map(KB0, Map0),
-	set__list_to_set(Solns, Ss0),
-	tree234_cc__search(Map0, Call, MaybeOldSs),
-	(
-		MaybeOldSs = yes(OldSs),
-			%
-			% The sets are both complete, so their
-			% intersection must be also.
-			%
-		set__intersect(OldSs, Ss0, Ss)
-	;
-		MaybeOldSs = no,
-		Ss = Ss0
-	),
-	tree234_cc__set(Map0, Call, Ss, Map),
+	tree234_cc__set(Map0, Call, Truth, Map),
 	set_kb_complete_map(KB0, Map, KB).
-
-assert_oracle_kb(missing_answer(_, Call, Solns), truth_value(_, no), KB0, KB) :-
-	get_kb_incomplete_map(KB0, Map0),
-	set__list_to_set(Solns, Ss),
-		%
-		% XXX should also keep the old incomplete set around, too.
-		% It can still give us information that the new one can't.
-		%
-	tree234_cc__set(Map0, Call, Ss, Map),
-	set_kb_incomplete_map(KB0, Map, KB).
 
 assert_oracle_kb(unexpected_exception(_, Call, Exception),
 		truth_value(_, Truth), KB0, KB) :-
Index: tests/debugger/declarative/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/debugger/declarative/Mmakefile,v
retrieving revision 1.47
diff -u -r1.47 Mmakefile
--- tests/debugger/declarative/Mmakefile	10 Oct 2002 10:49:07 -0000	1.47
+++ tests/debugger/declarative/Mmakefile	10 Oct 2002 14:38:24 -0000
@@ -22,6 +22,8 @@
 	gcf			\
 	higher_order		\
 	ho2			\
+	ho3			\
+	ho4			\
 	if_then_else		\
 	input_term_dep		\
 	ite_2			\
@@ -45,17 +47,11 @@
 NONDEBUG_DECLARATIVE_PROGS=	\
 	untraced_subgoal
 
-# XXX 'ho3' and 'ho4' test cases fail due to an attempt to compare higher
-# order terms.  This happens because for missing answer questions the oracle
-# stores the solutions in a set, which relies on builtin comparison.
-#
-# XXX 'ho5' also fails due to an attempt to compare higher order terms.  This
-# happens because thrown exceptions are stored in a set, and exceptions are
-# not necessarily first order terms.
+# XXX 'ho5' fails due to an attempt to compare higher order terms.  This
+# happens because thrown exceptions are stored in a set, which uses builtin
+# comparison, and exceptions are not necessarily first order terms.
 #
 NONWORKING_DECLARATIVE_PROGS=	\
-	ho3			\
-	ho4			\
 	ho5
 
 # Some of the test cases require a different input in debug grades,
Index: tests/debugger/declarative/ho3.exp
===================================================================
RCS file: /home/mercury1/repository/tests/debugger/declarative/ho3.exp,v
retrieving revision 1.1
diff -u -r1.1 ho3.exp
--- tests/debugger/declarative/ho3.exp	9 Oct 2002 08:50:02 -0000	1.1
+++ tests/debugger/declarative/ho3.exp	10 Oct 2002 14:16:54 -0000
@@ -0,0 +1,54 @@
+       1:      1  1 CALL pred ho3:main/2-0 (det) ho3.m:8
+mdb> echo on
+Command echo enabled.
+mdb> register --quiet
+mdb> break p
+ 0: + stop  interface pred ho3:p/1-0 (semidet)
+mdb> continue
+       3:      2  2 CALL pred ho3:p/1-0 (semidet) ho3.m:28 (ho3.m:10)
+mdb> finish
+      16:      2  2 FAIL pred ho3:p/1-0 (semidet) ho3.m:28 (ho3.m:10)
+mdb> dd
+Call p(1)
+No solutions.
+Complete? no
+q(0, x(0))
+Valid? yes
+Call x(0, 1)
+No solutions.
+Complete? yes
+q(0, y(0))
+Valid? yes
+Call y(0, 1)
+No solutions.
+Complete? yes
+Call q(0, _)
+Solutions:
+	q(0, x(0))
+	q(0, y(0))
+Complete? yes
+Found partially uncovered atom:
+p(1)
+Is this a bug? yes
+      16:      2  2 FAIL pred ho3:p/1-0 (semidet) ho3.m:28 (ho3.m:10)
+mdb> continue
+      19:      6  2 CALL pred ho3:p/1-0 (semidet) ho3.m:28 (ho3.m:17)
+mdb> finish
+      32:      6  2 FAIL pred ho3:p/1-0 (semidet) ho3.m:28 (ho3.m:17)
+mdb> dd
+Call p(2)
+No solutions.
+Complete? no
+Call x(0, 2)
+No solutions.
+Complete? yes
+Call y(0, 2)
+No solutions.
+Complete? yes
+Found partially uncovered atom:
+p(2)
+Is this a bug? yes
+      32:      6  2 FAIL pred ho3:p/1-0 (semidet) ho3.m:28 (ho3.m:17)
+mdb> continue
+\+ p(1).
+\+ p(2).
Index: tests/debugger/declarative/ho3.inp
===================================================================
RCS file: /home/mercury1/repository/tests/debugger/declarative/ho3.inp,v
retrieving revision 1.1
diff -u -r1.1 ho3.inp
--- tests/debugger/declarative/ho3.inp	9 Oct 2002 08:50:02 -0000	1.1
+++ tests/debugger/declarative/ho3.inp	10 Oct 2002 14:16:46 -0000
@@ -5,3 +5,17 @@
 finish
 dd
 no
+yes
+yes
+yes
+yes
+yes
+yes
+continue
+finish
+dd
+no
+yes
+yes
+yes
+continue
Index: tests/debugger/declarative/ho3.m
===================================================================
RCS file: /home/mercury1/repository/tests/debugger/declarative/ho3.m,v
retrieving revision 1.1
diff -u -r1.1 ho3.m
--- tests/debugger/declarative/ho3.m	9 Oct 2002 08:50:02 -0000	1.1
+++ tests/debugger/declarative/ho3.m	10 Oct 2002 14:08:09 -0000
@@ -26,8 +26,8 @@
 :- mode p(in) is semidet.
 
 p(N) :-
-	q(N, Q),
-	Q(0).
+	q(0, Q),
+	Q(N).
 
 :- pred q(int, pred(int)).
 :- mode q(in, out(pred(in) is semidet)) is multi.
Index: tests/debugger/declarative/ho4.exp
===================================================================
RCS file: /home/mercury1/repository/tests/debugger/declarative/ho4.exp,v
retrieving revision 1.1
diff -u -r1.1 ho4.exp
--- tests/debugger/declarative/ho4.exp	9 Oct 2002 09:25:21 -0000	1.1
+++ tests/debugger/declarative/ho4.exp	10 Oct 2002 14:10:18 -0000
@@ -0,0 +1,42 @@
+       1:      1  1 CALL pred ho4:main/2-0 (det) ho4.m:8
+mdb> echo on
+Command echo enabled.
+mdb> register --quiet
+mdb> break p
+ 0: + stop  interface pred ho4:p/1-0 (semidet)
+mdb> continue
+       3:      2  2 CALL pred ho4:p/1-0 (semidet) ho4.m:28 (ho4.m:10)
+mdb> finish
+      18:      2  2 FAIL pred ho4:p/1-0 (semidet) ho4.m:28 (ho4.m:10)
+mdb> dd
+Call p(1)
+No solutions.
+Complete? no
+q(r(5), 5)
+Valid? yes
+q(r(5), 0)
+Valid? yes
+Call q(r(5), _)
+Solutions:
+	q(r(5), 5)
+	q(r(5), 0)
+Complete? yes
+Found partially uncovered atom:
+p(1)
+Is this a bug? yes
+      18:      2  2 FAIL pred ho4:p/1-0 (semidet) ho4.m:28 (ho4.m:10)
+mdb> continue
+      21:      5  2 CALL pred ho4:p/1-0 (semidet) ho4.m:28 (ho4.m:17)
+mdb> finish
+      36:      5  2 FAIL pred ho4:p/1-0 (semidet) ho4.m:28 (ho4.m:17)
+mdb> dd
+Call p(2)
+No solutions.
+Complete? no
+Found partially uncovered atom:
+p(2)
+Is this a bug? yes
+      36:      5  2 FAIL pred ho4:p/1-0 (semidet) ho4.m:28 (ho4.m:17)
+mdb> continue
+\+ p(1).
+\+ p(2).
Index: tests/debugger/declarative/ho4.inp
===================================================================
RCS file: /home/mercury1/repository/tests/debugger/declarative/ho4.inp,v
retrieving revision 1.1
diff -u -r1.1 ho4.inp
--- tests/debugger/declarative/ho4.inp	9 Oct 2002 09:25:21 -0000	1.1
+++ tests/debugger/declarative/ho4.inp	10 Oct 2002 14:10:09 -0000
@@ -5,3 +5,13 @@
 finish
 dd
 no
+yes
+yes
+yes
+yes
+continue
+finish
+dd
+no
+yes
+continue
--------------------------------------------------------------------------
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