1		:- module(plspec,[spec_pre/2,spec_post/3,spec_invariant/2,
2
3		defspec/2, defspec_pred/2, defspec_pred_recursive/4,
4		defspec_connective/4,
5
6		setup_uber_check/4, check_posts/4, which_posts/8,
7		plspec_some/3, error_not_matching_any_pre/3,
8		enable_spec_check/1, enable_all_spec_checks/0,
9		set_error_handler/1,
10		asserted_spec_pre/5, asserted_spec_invariant/3,
11		asserted_spec_invariant/4, asserted_spec_post/7,
12		check_predicate/1 % called by term expander
13		]).
14
15		:- use_module(validator).
16		:- use_module(prettyprinter).
17		:- use_module(plspec_logger).
18
19		:- use_module(library(lists)).
20		:- use_module(library(terms), [variant/2]).
21
22		:- dynamic asserted_spec_pre/5, asserted_spec_invariant/3,
23		asserted_spec_invariant/4, asserted_spec_post/7.
24
25		%% set up facts
26
27		named_spec(Name:Spec, Name, Spec).
28
29		asserted_spec_invariant(Pred, Spec) :-
30		asserted_spec_invariant(Pred, _, Spec).
31
32
33		check_ground(_Pred, Spec, _SpecType) :-
34		ground(Spec).
35		check_ground(Pred, Spec, SpecType) :-
36		\+ ground(Spec),
37		log(info,'~w is not ground; got ~w in ~w. It is handled as a specific, but unknown spec.', [SpecType, Spec, Pred]).
38
39		check_arity(_Pred, Spec, _SpecType, Arity) :-
40		length(Spec, Arity).
41		check_arity(Pred, Spec, SpecType, Arity) :-
42		\+ length(Spec, Arity),
43		log(error,'~w of ~w does not match in length!',[SpecType, Pred]),
44		fail.
45
46		spec_pre(Pred,PreSpec) :-
47	?	check_ground(Pred, PreSpec, 'pre specs'),
48		Pred = Module:Functor/Arity,
49	?	check_arity(Pred, PreSpec, 'A pre spec', Arity),
50		(ground(PreSpec) ->
51		assertz(asserted_spec_pre(Functor,Arity,Module,PreSpec,def))
52		;
53		assertz(asserted_spec_pre(Functor,Arity,Module,PreSpec,any))),
54		log(debug,'Asserted spec pre for ~w.',[Pred]).
55
56		spec_invariant(Pred, InvariantSpec) :-
57	?	check_ground(Pred, InvariantSpec, 'invariant specs'),
58		Pred = _:_/Arity,
59	?	check_arity(Pred, InvariantSpec, 'An invariant spec', Arity),
60		(ground(InvariantSpec) ->
61		(maplist(plspec:named_spec, InvariantSpec, Names, Specs) ->
62		assertz(asserted_spec_invariant(Pred, Names, Specs, def))
63		;
64		assertz(asserted_spec_invariant(Pred, InvariantSpec, def)))
65		;
66		(maplist(plspec:named_spec, InvariantSpec, Names, Specs) ->
67		assertz(asserted_spec_invariant(Pred, Names, Specs, any))
68		;
69		assertz(asserted_spec_invariant(Pred, InvariantSpec, any)))),
70		log(debug,'Assertedc spec invariant for ~w.',[Pred]).
71
72		spec_post(Pred,PreSpec,PostSpec) :-
73	?	check_ground(Pred, PreSpec, 'post-specs'),
74	?	check_ground(Pred, PostSpec, 'post-specs'),
75		Pred = Module:F/Arity,
76	?	check_arity(Pred, PreSpec, 'A post spec (precondition)', Arity),
77	?	check_arity(Pred, PostSpec, 'A post spec (postcondition)', Arity),
78		(ground(PreSpec) ->
79		(ground(PostSpec) ->
80		assertz(asserted_spec_post(F,Arity,Module,PreSpec,PostSpec,def,def))
81		;
82		assertz(asserted_spec_post(F,Arity,Module,PreSpec,PostSpec,def,any)))
83		;
84		(ground(PostSpec) ->
85		assertz(asserted_spec_post(F,Arity,Module,PreSpec,PostSpec,any,def))
86		;
87		assertz(asserted_spec_post(F,Arity,Module,PreSpec,PostSpec,any,any)))),
88		log(debug,'Asserted spec post for ~w.',[Pred]).
89
90		log_spec_already_exists(SpecId, ExistingDefinition, NewDefinition) :-
91		(variant(spec(SpecId,ExistingDefinition),spec(SpecId,NewDefinition)) ->
92		log(info,'spec is overwritten with itself, proceeding~n', [SpecId])
93		;
94		log(warning,'spec ~w already exists, will not be redefined~n', [SpecId])).
95
96		:- meta_predicate defspec(+, 1).
97		defspec(SpecId, OtherSpec) :-
98		(spec_exists(SpecId, Existing) ->
99		%% we use variant in order to determine whether it is actually the same spec;
100		% for example, consider defspec(foo(X,Y), bar(X,Y)), defspec(foo(X,Y), bar(Y,X)).
101		% we do not want to unify X = Y but also notice these are not the same specs.
102		log_spec_already_exists(SpecId, Existing, indirection(OtherSpec))
103		;
104		assertz(spec_indirection(SpecId, OtherSpec)),
105		log(info,'Spec ~w defined.',[SpecId])).
106
107		:- meta_predicate defspec_pred(+, 1).
108		defspec_pred(SpecId, Predicate) :-
109		(spec_exists(SpecId, Existing) ->
110		log_spec_already_exists(SpecId, Existing, predicate(Predicate))
111		;
112		assertz(spec_predicate(SpecId, Predicate))).
113
114		:- meta_predicate defspec_pred_recursive(+, 3,3,4).
115		defspec_pred_recursive(SpecId, Predicate, MergePred, MergePredInvariant) :-
116		(spec_exists(SpecId, Existing) ->
117		log_spec_already_exists(
118		SpecId,
119		Existing,
120		predicate_recursive(Predicate, MergePred, MergePredInvariant)
121		)
122		;
123		assertz(
124		spec_predicate_recursive(
125		SpecId,
126		Predicate,
127		MergePred,
128		MergePredInvariant)
129		),
130		log(info, 'Recursive spec ~w defined.',[SpecId])
131		).
132
133		:- meta_predicate defspec_connective(+, 3,3,4).
134		defspec_connective(SpecId, Predicate, MergePred, MergePredInvariant) :-
135		(spec_exists(SpecId, Existing) ->
136		log_spec_already_exists(
137		SpecId,
138		Existing,
139		connective(Predicate, MergePred, MergePredInvariant)
140		)
141		;
142		assertz(
143		spec_connective(
144		SpecId,
145		Predicate,
146		MergePred,
147		MergePredInvariant
148		)
149		),
150		log(info,'Connective spec ~w defined.')
151		).
152
153
154		:- dynamic check_predicate/1.
155		enable_spec_check([H|T]) :- !,
156		maplist(enable_spec_check, [H|T]).
157		enable_spec_check(F/N) :-
158		log(info, 'Spec check enabled for ~w/~w.',[F/N]),
159		functor(X,F,N),
160		assertz(check_predicate(X)).
161		enable_spec_check(X) :-
162		log(error, 'Spec check cannot be enabled for ~w use Functor/Arity syntax!',[X]).
163		% Note: SICStus flag disable_plspec_runtime_checks can turn off all runtime checks
164
165		enable_all_spec_checks :-
166		retractall(check_predicate(_)),
167		assertz(check_predicate(_)).
168
169
170		:- dynamic error_handler/1.
171		error_handler(plspec_default_error_handler).
172
173		:- public plspec_default_error_handler/1.
174		plspec_default_error_handler(X) :-
175		pretty_print_error(X), !,
176		throw(plspec_error).
177
178		:- meta_predicate set_error_handler(1).
179		set_error_handler(Pred) :-
180		retractall(error_handler(_)),
181		assertz(error_handler(Pred)).
182
183		%% check coroutine magic
184		setup_uber_check(Location,any,Spec,Val) :-
185		log(debug,'setup_uber_check'),
186		setup_check(Location,Res,Spec,Val,any),
187		freeze(Res, ((Res == true) -> true ; error_handler(X), call(X, Res))).
188		setup_uber_check(Location,def,Spec,Val) :-
189		log(debug,'setup_uber_check'),
190		setup_check(Location,Res,Spec,Val,def),
191		freeze(Res, ((Res == true) -> true ; error_handler(X), call(X, Res))).
192		setup_check(Location,Res,Spec,Val,Type) :-
193		setup_check_aux(Spec,Location,Val,Res,Type).
194
195		setup_check_aux(Spec, Location, Val, Res, def) :-
196		spec_basic(Spec, Pred), !,
197		freeze(Val, (call(Pred, Val) -> true ; reason(Spec, Location, Val, Res))).
198		setup_check_aux(Spec, Location, Val, Res, _) :-
199		spec_predicate(Spec, Pred), !,
200		freeze(Val, (call(Pred, Val) -> true ; reason(Spec, Location, Val, Res))).
201		setup_check_aux(Spec, Location, Val, Res, Type) :-
202		spec_indirection(Spec, OtherSpec), !,
203		setup_check_aux(OtherSpec, Location, Val, Res, Type).
204		setup_check_aux(Spec, Location, Val, Res, _Type) :-
205		spec_predicate_recursive(Spec, Pred, _MergePred, MergePredInvariant),
206		!,
207		freeze(
208		Val,
209		(call(Pred, Val, NewSpecs, NewVals) ->
210		call(MergePredInvariant, NewSpecs, NewVals, Location, Res)
211		;
212		reason(Spec, Location, Val, Res)
213		)
214		).
215		setup_check_aux(Spec, Location, Val, Res, _Type) :-
216		spec_connective(Spec, Pred, _MergePred, MergePredInvariant), !,
217		freeze(
218		Val,
219		(call(Pred, Val, NewSpecs, NewVals) ->
220		call(MergePredInvariant, NewSpecs, NewVals, Location, Res)
221		;
222		reason(Spec, Location, Val, Res)
223		)
224		).
225		setup_check_aux(
226		Spec,
227		Location,
228		_,
229		fail(spec_not_found(spec(Spec), location(Location))),_).
230
231		reason(T, Location, V, Reason) :-
232		copy_term(Location, LocationWithoutAttributes, _Goals),
233		Reason =
234		fail(
235		spec_violated(
236		spec(T),
237		value(V),
238		location(LocationWithoutAttributes)
239		)
240		).
241
242		which_posts([],[],[],[],_,[],[],[]) :- !.
243		which_posts([Pre|PresBefore], [PreType|PreTypes],
244		[Post|Posts], [PostType|PostTypes], Args,
245		[Pre|PresAfter], [Post|PostAfter], [PostType|PostTypesAfter]) :-
246		maplist(valid(PreType),Pre,Args),!,
247		which_posts(
248		PresBefore,
249		PreTypes,
250		Posts,
251		PostTypes,
252		Args,
253		PresAfter,
254		PostAfter,
255		PostTypesAfter).
256		which_posts([_|Pres],[_|PreTypes],[_|Posts],[_|PostTypes],Args,PreT,T,Z) :-
257		which_posts(Pres,PreTypes,Posts,PostTypes,Args,PreT,T,Z).
258
259
260
261		check_posts([], [], [], _).
262		check_posts([Arg|ArgT], [Pre|PreT], [Post|PostT], PostType) :-
263		evaluate_spec_match(Post, PostType, Arg, Res),!,
264		(Res == true ->
265		check_posts(ArgT, PreT, PostT, PostType)
266		;
267		error_handler(X),
268		call(
269		X,
270		fail(
271		postcondition_violated(
272		matched_pre(Pre),
273		violated_post(Post),
274		value(Arg)
275		)
276		)
277		)
278		).
279
280		%% term expansion
281		:- meta_predicate plspec_some(1, ?, ?).
282		plspec_some(Goal, List, List2) :-
283		plspec_some1(List, List2, Goal).
284		plspec_some1([],[], _) :- fail.
285		plspec_some1([H|_], [G|_], Goal) :-
286		call(Goal,H,G),
287		log(debug, 'Pre-Spec ~w matched!',[H]),
288		!.
289		plspec_some1([_|T], [_|S], Goal) :-
290		plspec_some1(T, S, Goal).
291
292		:- public spec_matches/4. %THIS SEEMS NOT USED - TO DO: investigate
293		spec_matches([], true, [], _).
294		spec_matches([Arg|ArgsT], Res, [Spec|SpecT], Type) :-
295		evaluate_spec_match(Spec, Type, Arg, R),
296		(R == true ->
297		spec_matches(ArgsT, Res, SpecT, Type)
298		;
299		Res = spec_not_matched(Spec, Arg, in(R))).
300
301		error_not_matching_any_pre(Functor, Args, PreSpecs) :-
302		error_handler(X),
303		call(
304		X,
305		fail(
306		prespec_violated(specs(PreSpecs), values(Args), location(Functor))
307		)
308		).
309
310		and_invariant([], [], _, true, _).
311		and_invariant([HSpec|TSpec], [HVal|TVal], Location, R, Type) :-
312		setup_check(Location, ResElement,HSpec, HVal, Type),
313		freeze(TVal, and_invariant(TSpec, TVal, Location, ResTail, Type)), % TODO: do we need this freeze?
314		both_eventually_true(ResElement, ResTail, R).
315
316		:- public and_invariant/4.
317		and_invariant(Specs, Vals, Location, R) :-
318		(ground(Specs) ->
319		and_invariant(Specs, Vals, Location, R, def)
320		;
321		and_invariant(Specs, Vals, Location, R, any)
322		).
323
324
325		or_invariant([], [], Acc, OrigVals, OrigPattern, Location, UberVar) :-
326		freeze(
327		Acc,
328		(Acc == fail ->
329		(reason(OrigPattern, Location, OrigVals, Reason), UberVar = Reason)
330		;
331		true
332		)
333		).
334		or_invariant([H|T], [V|VT], Prior, OrigVals, OrigPattern, Location, UberVar) :-
335		setup_check(Location, ResOption, H, V),
336		freeze(
337		ResOption,
338		(ResOption == true ->
339		(UberVar = true, Current = true)
340		;
341		freeze(
342		Prior,
343		(Prior == true -> true; Current = fail)
344		)
345		)
346		),
347		or_invariant(T, VT, Current, OrigVals, OrigPattern, Location, UberVar).
348
349		:- public or_invariant/4.
350		or_invariant(NewSpecs, NewVals, Location, FutureRes) :-
351		or_invariant(NewSpecs, NewVals, [], NewVals, or(NewSpecs), Location, FutureRes).
352
353		%% merge recursive specs
354		both_eventually_true(V1, V2, Res) :-
355		when((nonvar(V1); nonvar(V2)),
356		(V1 == true
357		-> freeze(V2, Res = V2) %% look at the other co-routined variable
358		; nonvar(V1)
359		-> Res = V1 %% since it is not true
360		; V2 == true
361		-> freeze(V1, Res = V1)
362		; nonvar(V2) -> Res = V2)).