1		% (c) 2009-2023 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		% WARNING (debug_properties DEPRECATED) :
6		% it is planned to replace the debug_properties commands using the unsat_cores.pl predicates
7		% operation enabling code should be moved to a separate module
8
9		:- module(predicate_debugger,[tcltk_debug_properties/3,
10		tcltk_debug_properties_or_op/4,
11		tcltk_get_unsat_core_with_types/1]).
12
13
14		:- use_module(probsrc(tools)).
15
16		:- use_module(probsrc(module_information),[module_info/2]).
17		:- module_info(group,misc).
18		:- module_info(description,'The predicate debugger adds conjuncts one by one until the predicate becomes unsatisfiable.').
19
20		:- use_module(probsrc(debug)).
21		:- use_module(probsrc(self_check)).
22		:- use_module(probsrc(preferences)).
23		:- use_module(probsrc(error_manager)).
24
25		:- use_module(probsrc(translate)).
26		:- use_module(probsrc(b_interpreter)).
27		:- use_module(probsrc(bsyntaxtree)).
28		:- use_module(probsrc(b_ast_cleanup)).
29
30		:- use_module(library(timeout)).
31		:- use_module(library(lists)).
32
33		:- use_module(probsrc(b_operation_guards),[get_operation_enabling_condition/7]).
34
35
36		/* b_interpreter:b_debug_properties. */
37
38		:- volatile checked_property/1, last_checked_solution/2, failed_property/2, time_out_property/2, cur_conjunct_nr/1, projection_onto_component/1.
39		:- dynamic checked_property/1.
40		:- dynamic last_checked_solution/2.
41		:- dynamic failed_property/2.
42		:- dynamic time_out_property/2.
43		:- dynamic cur_conjunct_nr/1.
44		:- dynamic projection_onto_component/1.
45
46		reset_debug_properties :-
47		retractall(last_debug_info(_,_)),
48		retractall(checked_property(_)),
49		retractall(last_checked_solution(_,_)),
50		retractall(failed_property(_,_)),
51		retractall(time_out_property(_,_)),
52		retractall(cur_conjunct_nr(_)),
53		retractall(projection_onto_component(_)).
54
55		:- use_module(probsrc(b_global_sets),[b_global_set/1, b_fd_card/2, unfixed_deferred_set/1]).
56		tcltk_debug_properties(RealRes,UnsatCore,Satisfiable) :-
57		tcltk_debug_properties_or_op('@PROPERTIES',UnsatCore,RealRes,Satisfiable).
58
59		% code below because names with $ cause problems in Tcl with eval
60		% code duplicated from tcltk_interface; but predicate debugger is deprecated anyway
61		adapt_tcl_operation_name(X,R) :- var(X),!,R=X.
62		adapt_tcl_operation_name('@PROPERTIES','$setup_constants') :- !.
63		adapt_tcl_operation_name('@INITIALISATION','$initialise_machine') :- !.
64		adapt_tcl_operation_name(X,X).
65
66		tcltk_debug_properties_or_op(TclOpName,ComputeUnsatCore,list(RealRes),Satisfiable) :-
67		adapt_tcl_operation_name(TclOpName,OpName),
68		print(tcltk_debug_properties_or_op(OpName,ComputeUnsatCore,RealRes)),nl,
69		(ComputeUnsatCore==false ->
70		(OpName='$setup_constants' -> b_debug_properties
71		; OpName = '@GOAL' -> b_debug_goal
72		; b_debug_operation(OpName))
73		; set_fast_unsat_core(ComputeUnsatCore),
74		print('*** Finding Unsat Core : '), print(ComputeUnsatCore),nl,
75		(b_find_unsat_core
76		-> print('*** Finished '),nl
77		; add_error_fail(predicate_debugger,'Finding Unsat Core failed',OpName))
78		),
79		print(debugged(OpName)),nl,
80		findall(TP, (checked_property(P),
81		translate_bexpression_with_limit(P,TrP),
82		ajoin([TrP,' &\n'],TP)),
83		Res1),
84		(projection_onto_component(_SubNr)
85		-> Res1P = ['(only a sub-component was analysed)\n'|Res1] ; Res1P=Res1),
86		(Res1=[] -> R1=Res1P ;
87		R1=['\n ********\n\nSATISFIABLE CONSTRAINTS and PROPERTIES:\n'|Res1P]
88		),
89		findall(TP2,( (failed_property(P,_),TRES='false' ; time_out_property(P,_),TRES='time_out'),
90		translate_status(P,TRES,TP2)),
91		Res2),
92		(Res2=[] -> R2=['\nNo unsatisfiable PROPERTY or CONSTRAINT'], Satisfiable=true
93		; R2=['\n ********\n\nFirst unsatisfiable PROPERTY or CONSTRAINT:\n'|Res2],
94		Satisfiable=false
95		),
96		findall(TP, (last_checked_solution(ConstantsState,_), % TO DO: Project on remaining variables !?
97		translate_equivalence(b(identifier('SOLUTION'),boolean,[]),ConstantsState,TP)),
98		Res12),
99		append(R2,['\n\n ********\n\nSolution for satisfiable part:\n'|Res12],R2Res12),
100		append(R1,R2Res12,Res),
101		findall(SetDescr,(b_global_set(Set),b_fd_card(Set,Card),
102		create_texpr(identifier(Set),set(global(Set)),[],SetId),
103		create_texpr(card(SetId),integer,[],CardExpr),
104		create_texpr(value(int(Card)),integer,[],ValExpr),
105		create_texpr(equal(CardExpr,ValExpr),prop,[],EqualExpr),
106		translate_bexpression(EqualExpr,SetDescr1),
107		(unfixed_deferred_set(Set) -> Xtra = ' (assumed for deferred set)' ; Xtra=''),
108		ajoin([SetDescr1,Xtra,'\n'],SetDescr)), Sets),
109
110		append(['\nCardinalities of SETS:\n'|Sets],Res,SRes),
111		preferences:get_preference(minint,MININT),
112		preferences:get_preference(maxint,MAXINT),
113		clear_error_context,
114		ajoin(['MININT .. MAXINT = ',MININT,'..',MAXINT],MINMAX),
115		RealRes = ['SETTINGS:\n',MINMAX|SRes].
116		tcltk_debug_properties_or_op([],_,list(['Machine has no PROPERTIES']),true).
117
118		failed_or_time_out_property(P) :- failed_property(P,_) ; time_out_property(P,_).
119
120		:- use_module(library(codesio),[write_to_codes/2]).
121		:- use_module(probsrc(tools),[ajoin/2]).
122		% use_module(probsrc(predicate_debugger)),predicate_debugger:print_unsat_core_with_types
123		tcltk_get_unsat_core_with_types(ResultCodes) :-
124		get_unsat_core(AllConj),
125		translate_predicate_into_machine(AllConj,'UnsatCore',ResultAtom),
126		write_to_codes(ResultAtom,ResultCodes).
127
128		get_unsat_core(AllConj) :- (checked_property(_) ; failed_or_time_out_property(_)), !,
129		findall(P,checked_property(P),Ps),
130		findall(UnsatP,failed_or_time_out_property(UnsatP),UPs),
131		append(Ps,UPs,All),
132		conjunct_predicates(All,AllConj).
133		get_unsat_core(Core) :- print('No predicate debugger analysis run'),nl,
134		print('Trying to extract from b_interpreter'),nl,
135		b_interpreter:get_unsat_component_predicate(_,Core,_Vars),!.
136		get_unsat_core(b(truth,pred,[])).
137
138
139		translate_equivalence(A,B,R) :-
140		translate_bexpression(A,TA),
141		translate_bstate(B,TB),
142		ajoin([TA,'\n == ',TB,'\n'],R).
143		:- use_module(probsrc(translate),[translate_span/2]).
144		translate_status(A,Status,R) :-
145		translate_bexpression(A,TA),
146		(translate_span(A,ASpan)
147		-> ajoin([TA,'\n == ',Status,' ',ASpan],R)
148		; ajoin([TA,'\n == ',Status],R)).
149
150
151
152		:- use_module(probsrc(bmachine)).
153		b_debug_properties :- set_error_context(b_debug_properties),
154		reset_debug_properties,
155		%%b_extract_constants_and_properties(Constants,CstTypes,Properties),
156		%b_machine_has_constants_or_properties,
157		b_get_machine_constants(TypedConstants),
158		get_adapted_properties(TypedConstants,AProperties,ATypedConstants,AllowTimeout),
159		nr_of_conjuncts(AProperties,NrConj),
160		(b_debug_properties2(AProperties,ATypedConstants,[],NrConj,AllowTimeout) -> true ; true).
161
162		b_debug_goal :-
163		bmachine:b_get_machine_goal(Goal),
164		b_debug_predicate(Goal).
165		b_debug_predicate(FullPred) :- set_error_context(b_debug_predicate),
166		reset_debug_properties,
167		get_parameters(FullPred,Params,Pred),
168		get_current_state('@PRED',CurID,CurBState),
169		set_error_context(b_debug_predicate(CurID)),
170		nr_of_conjuncts(Pred,NrConj),
171		(b_debug_properties2(Pred,Params,CurBState,NrConj,allow_timeout) -> true ; true).
172
173		get_parameters(b(exists(Parameters,Pred),pred,_),Parameters,Pred) :- !.
174		get_parameters(Pred,[],Pred).
175
176		:- use_module(library(lists)).
177		get_adapted_properties(TypedConstants,Pred,CTypedConstants,do_not_allow_timeout) :-
178		%(b_interpreter:nr_of_components(NrC), NrC>1),
179		preferences:get_preference(partition_predicates,true),
180		b_interpreter:get_unsat_component_predicate(CompNr,Pred,Vars),!, % means there was no timeout
181		assertz(projection_onto_component(CompNr)),
182		print(debugging_unsat_or_skipped_component(CompNr)),nl,
183		print(component_vars(Vars)),nl,
184		project_texpr_identifiers(TypedConstants,Vars,CTypedConstants).
185		get_adapted_properties(TypedConstants,Properties,TypedConstants,allow_timeout) :-
186		% TO DO determine whether timeout occured
187		b_get_properties_from_machine(Properties).
188
189
190		% only keep texpr_identifiers whose id is in the provided list
191		project_texpr_identifiers([],_,[]).
192		project_texpr_identifiers([TID|T],Vars,Res) :-
193		(get_texpr_id(TID,ID),member(ID,Vars)
194		-> Res = [TID|R2] ; Res=R2),
195		project_texpr_identifiers(T,Vars,R2).
196
197		:- use_module(probsrc(specfile),[state_corresponds_to_initialised_b_machine/2, state_corresponds_to_set_up_constants/2]).
198		/* b_interpreter:tcltk_debug_properties_or_op(prog1,R)*/
199		b_debug_operation(OpName) :-
200		reset_debug_properties,
201		get_current_state(OpName,CurID,CurBState),
202		set_error_context(operation(OpName,CurID)),
203		(get_operation_enabling_condition(OpName,Parameters,EnablingCondition,BSVars,_,true,false) -> true
204		; add_error(b_debug_operation,'Operation does not exist or cannot determine enabling condition: ',OpName),fail),!,
205		print('Enabling: '), print_bexpr(EnablingCondition),nl,
206		flush_output(user),
207		nr_of_conjuncts(EnablingCondition,NrConj),
208		insert_before_substitution_variables(BSVars,[],CurBState,CurBState,NewCurBState),
209		extract_exists_parameters(EnablingCondition,Parameters,NewCond,NewParas),
210		(b_debug_properties2(NewCond,NewParas,NewCurBState,NrConj,allow_timeout) -> true ; true).
211
212		:- use_module(probsrc(state_space),[current_expression/2]).
213		get_current_state(OpName,CurID,CurBState) :-
214		(current_expression(CurID,CurState) -> true
215		; add_error(predicate_debugger,'Could not get current state',OpName),fail),
216		(state_corresponds_to_initialised_b_machine(CurState,CurBState) -> true
217		; (OpName=='$initialise_machine',
218		state_corresponds_to_set_up_constants(CurState,CurBState)) -> true
219		; add_error(b_debug_operation,'Machine not yet initialised! ',CurState),fail).
220
221
222		% Try to lift out existentially quantified variables to the outer level; to make the debugging more fine-grained
223		extract_exists_parameters(Pred,Parameters, NewPred, NewParas) :-
224		get_texpr_expr(Pred,exists(Vars,Body)),
225		disjoint_list_union(Parameters,Vars,Paras1), !, % also checks if no clash exists; otherwise we have to keep exists
226		extract_exists_parameters(Body,Paras1,NewPred,NewParas).
227		extract_exists_parameters(Pred,Parameters, NewPred, NewParas) :-
228		get_texpr_expr(Pred,conjunct(LHS,RHS)),!,
229		extract_exists_parameters(LHS,Parameters, NewLHS, IntParas),
230		extract_exists_parameters(RHS,IntParas,NewRHS,NewParas),
231		conjunct_predicates([NewLHS,NewRHS],NewPred).
232		extract_exists_parameters(Pred,Par,Pred,Par).
233
234		% -----------------------------------------
235
236		:- use_module(library(timeout)).
237
238
239		nr_of_conjuncts(Pred,Nr) :-
240		is_a_conjunct(Pred,LHS,RHS),!,
241		nr_of_conjuncts(LHS,NrL),
242		nr_of_conjuncts(RHS,NrR),
243		Nr is NrL+NrR.
244		nr_of_conjuncts(_,1).
245
246		:- volatile last_debug_info/2.
247		:- dynamic last_debug_info/2.
248		b_debug_properties2(Pred,Constants,GlobalState,TotalNr,AllowTimeout) :-
249		create_texpr(truth,pred,[b_debug_properties],Truth),
250		retractall(last_debug_info(_,_)), assertz(last_debug_info(Constants,GlobalState)),
251		(b_debug_find_first_unsat_property(Pred,Truth,Constants,GlobalState,TotalNr,AllowTimeout)
252		-> print('ALL PROPERTIES SATISFIABLE'),nl
253		; true % get_preference(debug_try_minimise,false) -> true ; b_find_unsat_core(Constants,GlobalState)
254		).
255
256		b_find_unsat_core :- /* assumes that b_debug_properties was run before */
257		% b_machine_has_constants_or_properties,
258		% b_get_machine_constants(TypedConstants),
259		% b_get_properties_from_machine(Properties),!,
260		% get_adapted_properties(TypedConstants,_AProperties,ATypedConstants),
261		%b_find_unsat_core(ATypedConstants,[]).
262		last_debug_info(Constants,GlobalState), b_find_unsat_core(Constants,GlobalState).
263		b_find_unsat_core(Constants,GlobalState) :-
264		print('TRYING TO MINIMISE UNSATISFIABLE PROPERTIES'),nl,
265		(last_checked_solution(_,Time)
266		-> print(' Time for last solution in ms: '), print(Time), nl ; true),
267		findall(P,checked_property(P),SatProps),
268		(failed_property(FailProp,USTime) -> true
269		; time_out_property(FailProp,USTime) -> true
270		; add_error_fail(b_find_unsat_core,'No failed or timed-out property:',SatProps)),
271		print(' Time for unsatisfiable conjuncts in ms: '), print(USTime), nl,
272		append(SatProps,[FailProp],Props),
273		length(SatProps,SL),
274		b_debug_try_remove_props(SatProps,Props,[],Constants,GlobalState,1,SL).
275		% TO DO: partition into components; try removing compnents without FailProp
276
277		b_debug_try_remove_props([],_,_,_,_,_,_) :- !.
278		b_debug_try_remove_props([],_,_,TypedConstants,GlobalState,Count,_) :- !, % for debug
279		format('~nFINISHED (~w); CHECKING CORE~n',[Count]),
280		get_unsat_core(Core),
281		nl,translate:print_bexpr(Core),nl,
282		(timeout_fast_check_property(unsat,Core,TypedConstants,_,GlobalState,TimeOutResC) -> true
283		; TimeOutResC = 'UNSAT'),
284		format('~nCORE RESULT: ~w~n',[TimeOutResC]).
285		b_debug_try_remove_props([H|TSat],[H|TUnsat],Required,TypedConstants,GlobalState,Count,Total) :-
286		append(Required,TSat,ConjunctsWithoutH),
287		conjunct_predicates(ConjunctsWithoutH,SatPred),
288		translate_bexpression(H,PT),
289		format('~nCHECKING REMOVAL(~w/~w) OF: ~w~n',[Count,Total,PT]),
290		(timeout_fast_check_property(sat,SatPred,TypedConstants,Sol,GlobalState,TimeOutResSat)
291		-> (\+ is_time_out_result(TimeOutResSat)
292		-> append(Required,TUnsat,ConjunctsWithoutH2),
293		conjunct_predicates(ConjunctsWithoutH2,UnsatPred),
294		((timeout_fast_check_property(unsat,UnsatPred,TypedConstants,_,GlobalState,TimeOutRes),
295		print(res(TimeOutRes)),nl,
296		(is_time_out_result(TimeOutRes) -> \+ time_out_property(_,_) ; true)
297		)
298		-> print('Required for inconsistency : '), print(TimeOutRes),nl,
299		append(Required,[H],NewRequired)
300		; /* H is not required for inconsistency/timeout */
301		print('NOT required for INCONSISTENCY !'),nl,
302		% print_bexpr(UnsatPred),nl,
303		Required=NewRequired,
304		% TO DO: update found solution
305		(retract(last_checked_solution(_,LastTime)) -> true
306		; print('*** Could not remove last_checked_solution'),nl,
307		preferences:get_computed_preference(debug_time_out,LastTime)
308		),
309		assertz(last_checked_solution(Sol,LastTime)),
310		(retract(checked_property(H)) -> true
311		; print('*** Could not remove checked_property: '), print(H),nl
312		)
313		)
314		; print('Required for efficiency'),nl,
315		append(Required,[H],NewRequired)
316		)
317		; nl,print('*** INTERNAL ERROR: FAILED'),nl,nl,
318		append(Required,[H],NewRequired)
319		),
320		C1 is Count+1,
321		b_debug_try_remove_props(TSat,TUnsat,NewRequired,TypedConstants,GlobalState,C1,Total).
322
323		b_debug_find_first_unsat_property(Pred,Rest,Constants,GlobalState,TotalNr,AllowTimeout) :-
324		is_a_conjunct(Pred,LHS,RHS),!,
325		(b_debug_find_first_unsat_property(LHS,Rest,Constants,GlobalState,TotalNr,AllowTimeout)
326		-> conjunct_predicates([Rest,LHS],Rest2),
327		b_debug_find_first_unsat_property(RHS,Rest2,Constants,GlobalState,TotalNr,AllowTimeout)
328		; fail
329		).
330		b_debug_find_first_unsat_property(Prop,Rest,TypedConstants,GlobalState,TotalNr,AllowTimeout) :-
331		nl,nl,flush_output(user),
332		conjunct_predicates([Rest,Prop],Pred),
333		(retract(cur_conjunct_nr(CurNr)) -> true ; CurNr=1), CurNrP1 is CurNr+1,
334		assertz(cur_conjunct_nr(CurNrP1)),
335		translate_bexpression(Prop,PT),
336		format('~nCHECKING (~w/~w) OF: ~w~n',[CurNr,TotalNr,PT]),
337		statistics(runtime,[Start,_]),
338		(timeout_check_property(Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes)
339		-> statistics(runtime,[Stop,_]), Time is Stop - Start,
340		print_time(TimeOutRes,Time),
341		format('~nINFO: ~w~n~n',[TimeOutRes]),
342		(((\+ last_checked_solution(_,_) % we haven't found a solution yet
343		; AllowTimeout=allow_timeout),
344		is_time_out_result(TimeOutRes))
345		-> assertz(time_out_property(Prop,Time))
346		; is_time_out_failure(TimeOutRes)
347		-> assertz(time_out_property(Prop,Time))
348		;
349		assert_checked_property(Prop,ConstantsState,Time) % could also be timeout
350		)
351		; statistics(runtime,[Stop,_]), Time is Stop - Start,
352		assertz(failed_property(Prop,Time)),
353		print('No Solution Found !! ('),print(Time), print(' ms)'),nl, flush_output(user),
354		%print_bexpr(Pred),nl,
355		fail
356		).
357
358		is_time_out_failure(virtual_time_out(failure_enumeration_warning(_,_,_,_,_))).
359
360		print_time(TimeOutRes,Time) :- is_time_out_result(TimeOutRes),!,
361		(TimeOutRes=virtual_time_out(_) -> print('VIRTUAL ') ; true),
362		print('TIMEOUT !! ('),print(Time), print(' ms)'),nl, flush_output(user).
363		print_time(_TimeOutRes,Time) :-
364		print('OK ('), print(Time), print(' ms)'), flush_output(user).
365
366
367		last_unsat_time(Time) :- time_out_property(_,Time) -> true ; failed_property(_,Time).
368
369		set_fast_unsat_core(T) :- retractall(fast_unsat_core),
370		(T==fast -> assertz(fast_unsat_core) ; true).
371		:- dynamic fast_unsat_core/0.
372		fast_unsat_core.
373
374		additional_time(301). % additional time given to account for variations in solving
375		%additional_time(1301).
376
377		get_timeout(sat,DebugTimeOut) :-
378		last_checked_solution(_,LTime),
379		!,
380		additional_time(AT),
381		DebugTimeOut is LTime+AT.
382		get_timeout(unsat,DebugTimeOut) :-
383		last_unsat_time(USTime),
384		last_checked_solution(_,LSTime),
385		(fast_unsat_core -> TT is min(USTime,LSTime) ; TT is max(USTime,LSTime)),
386		!,
387		additional_time(AT),
388		DebugTimeOut is TT+AT.
389		get_timeout(S,DebugTimeOut) :- print('*** Could not get TimeOut : '), print(S),nl,
390		preferences:get_preference(time_out,CurTO), DebugTimeOut is CurTO * 1.
391
392
393		timeout_fast_check_property(ExpectSat,Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes) :-
394		get_timeout(ExpectSat,DebugTimeOut),
395		% print(time_out_value(DebugTimeOut)),nl,
396		% print_bexpr(Pred),nl,
397		statistics(runtime,[Start,_]),
398		timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState,DebugTimeOut,TimeOutRes),
399		statistics(runtime,[Stop,_]), Time is Stop - Start, print(time(Time)),nl,
400		(is_time_out_result(TimeOutRes) -> print(time_out_occurred(Time,DebugTimeOut)),nl,
401		(debug:debug_mode(on) -> print_bexpr(Pred),nl ; true)
402		; true).
403
404		timeout_check_property(Pred,TypedConstants,ConstantsState,GlobalState,TimeOutRes) :-
405		preferences:get_computed_preference(debug_time_out,DebugTimeOut),
406		timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState,DebugTimeOut,TimeOutRes),
407		% Note: will translate failure with enumeration warning into virtual_timeout; see is_time_out_failure above
408		format('~nCHECKING RESULT is: ~w~n',[TimeOutRes]).
409
410		timeout_check_property_aux(Pred,TypedConstants,ConstantsState,GlobalState, DebugTimeOut,TimeOutRes) :-
411		catch(
412		time_out_with_enum_warning_one_solution(
413		b_check_property_satisfiable(Pred,TypedConstants,ConstantsState,GlobalState),
414		DebugTimeOut,TimeOutRes),
415		E,
416		TimeOutRes = virtual_time_out(exception(E))). % probably CLPFD overflow
417
418
419		assert_checked_property(P,ConstantsState,Time) :-
420		assertz(checked_property(P)),
421		(var(ConstantsState) -> print('NO SOLUTION'),nl
422		; retractall(last_checked_solution(_,_)),
423		assertz(last_checked_solution(ConstantsState,Time))).
424
425		:- use_module(probsrc(kernel_waitflags)).
426		:- use_module(probsrc(b_enumerate)).
427
428		% TO DO: call something which will use predicate_components
429
430		b_check_property_satisfiable(Properties,TypedConstants,ConstantsState,GlobalState) :-
431		b_ast_cleanup:clean_up_pred(Properties,[],Pred),
432		set_up_typed_localstate(TypedConstants,_FreshVars,TypedVals,[],ConstantsState,positive),
433		b_interpreter_components:reset_component_info(false),
434		append(ConstantsState,GlobalState,State),
435		b_interpreter_components:b_trace_test_components(Pred,State,TypedVals),
436		\+ b_interpreter_components:unsat_component_exists.
437
438
439