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/3, asserted_spec_invariant/3,
11		asserted_spec_invariant/4, asserted_spec_post/5,
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/3, asserted_spec_invariant/3,
23		asserted_spec_invariant/4, asserted_spec_post/5.
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 = _:_/Arity),
49	?	check_arity(Pred, PreSpec, 'A pre spec', Arity),
50		(ground(PreSpec) ->
51		assert(asserted_spec_pre(Pred,PreSpec,def))
52		;
53		assert(asserted_spec_pre(Pred,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(named_spec, InvariantSpec, Names, Specs) ->
62		assert(asserted_spec_invariant(Pred, Names, Specs, def))
63		;
64		assert(asserted_spec_invariant(Pred, InvariantSpec, def)))
65		;
66		(maplist(named_spec, InvariantSpec, Names, Specs) ->
67		assert(asserted_spec_invariant(Pred, Names, Specs, any))
68		;
69		assert(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 = _:_/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		assert(asserted_spec_post(Pred,PreSpec,PostSpec,def,def))
81		;
82		assert(asserted_spec_post(Pred,PreSpec,PostSpec,def,any)))
83		;
84		(ground(PostSpec) ->
85		assert(asserted_spec_post(Pred,PreSpec,PostSpec,any,def))
86		;
87		assert(asserted_spec_post(Pred,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_pred(+, 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		assert(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		assert(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		assert(
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		assert(
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(X) :-
158		log(info, 'Spec check enabled for ~w.',[X]),
159		assert(check_predicate(X)).
160
161		enable_all_spec_checks :-
162		assert(check_predicate(_)).
163
164
165		:- dynamic error_handler/1.
166		error_handler(plspec_default_error_handler).
167
168		:- public plspec_default_error_handler/1.
169		plspec_default_error_handler(X) :-
170		pretty_print_error(X), !,
171		throw(plspec_error).
172
173		:- meta_predicate set_error_handler(1).
174		set_error_handler(Pred) :-
175		retractall(error_handler(_)),
176		assert(error_handler(Pred)).
177
178		%% check coroutine magic
179		setup_uber_check(Location,any,Spec,Val) :-
180		log(debug,'setup_uber_check'),
181		setup_check(Location,Res,Spec,Val,any),
182		freeze(Res, ((Res == true) -> true ; error_handler(X), call(X, Res))).
183		setup_uber_check(Location,def,Spec,Val) :-
184		log(debug,'setup_uber_check'),
185		setup_check(Location,Res,Spec,Val,def),
186		freeze(Res, ((Res == true) -> true ; error_handler(X), call(X, Res))).
187		setup_check(Location,Res,Spec,Val,Type) :-
188		setup_check_aux(Spec,Location,Val,Res,Type).
189
190		setup_check_aux(Spec, Location, Val, Res, def) :-
191		spec_basic(Spec, Pred), !,
192		freeze(Val, (call(Pred, Val) -> true ; reason(Spec, Location, Val, Res))).
193		setup_check_aux(Spec, Location, Val, Res, _) :-
194		spec_predicate(Spec, Pred), !,
195		freeze(Val, (call(Pred, Val) -> true ; reason(Spec, Location, Val, Res))).
196		setup_check_aux(Spec, Location, Val, Res, Type) :-
197		spec_indirection(Spec, OtherSpec), !,
198		setup_check_aux(OtherSpec, Location, Val, Res, Type).
199		setup_check_aux(Spec, Location, Val, Res, _Type) :-
200		spec_predicate_recursive(Spec, Pred, _MergePred, MergePredInvariant),
201		!,
202		freeze(
203		Val,
204		(call(Pred, Val, NewSpecs, NewVals) ->
205		call(MergePredInvariant, NewSpecs, NewVals, Location, Res)
206		;
207		reason(Spec, Location, Val, Res)
208		)
209		).
210		setup_check_aux(Spec, Location, Val, Res, _Type) :-
211		spec_connective(Spec, Pred, _MergePred, MergePredInvariant), !,
212		freeze(
213		Val,
214		(call(Pred, Val, NewSpecs, NewVals) ->
215		call(MergePredInvariant, NewSpecs, NewVals, Location, Res)
216		;
217		reason(Spec, Location, Val, Res)
218		)
219		).
220		setup_check_aux(
221		Spec,
222		Location,
223		_,
224		fail(spec_not_found(spec(Spec), location(Location))),_).
225
226		reason(T, Location, V, Reason) :-
227		copy_term(Location, LocationWithoutAttributes, _Goals),
228		Reason =
229		fail(
230		spec_violated(
231		spec(T),
232		value(V),
233		location(LocationWithoutAttributes)
234		)
235		).
236
237		which_posts([],[],[],[],_,[],[],[]) :- !.
238		which_posts([Pre|PresBefore], [PreType|PreTypes],
239		[Post|Posts], [PostType|PostTypes], Args,
240		[Pre|PresAfter], [Post|PostAfter], [PostType|PostTypesAfter]) :-
241		maplist(valid(PreType),Pre,Args),!,
242		which_posts(
243		PresBefore,
244		PreTypes,
245		Posts,
246		PostTypes,
247		Args,
248		PresAfter,
249		PostAfter,
250		PostTypesAfter).
251		which_posts([_|Pres],[_|PreTypes],[_|Posts],[_|PostTypes],Args,PreT,T,Z) :-
252		which_posts(Pres,PreTypes,Posts,PostTypes,Args,PreT,T,Z).
253
254
255
256		check_posts([], [], [], _).
257		check_posts([Arg|ArgT], [Pre|PreT], [Post|PostT], PostType) :-
258		evaluate_spec_match(Post, PostType, Arg, Res),!,
259		(Res == true ->
260		check_posts(ArgT, PreT, PostT, PostType)
261		;
262		error_handler(X),
263		call(
264		X,
265		fail(
266		postcondition_violated(
267		matched_pre(Pre),
268		violated_post(Post),
269		value(Arg)
270		)
271		)
272		)
273		).
274
275		%% term expansion
276		:- meta_predicate plspec_some(1, +).
277		plspec_some(Goal, List, List2) :-
278		plspec_some1(List, List2, Goal).
279		plspec_some1([],[], _) :- fail.
280		plspec_some1([H|_], [G|_], Goal) :-
281		call(Goal,H,G),
282		log(debug, 'Pre-Spec ~w matched!',[H]),
283		!.
284		plspec_some1([_|T], [_|S], Goal) :-
285		plspec_some1(T, S, Goal).
286
287		:- public spec_matches/4. %THIS SEEMS NOT USED - TO DO: investigate
288		spec_matches([], true, [], _).
289		spec_matches([Arg|ArgsT], Res, [Spec|SpecT], Type) :-
290		evaluate_spec_match(Spec, Type, Arg, R),
291		(R == true ->
292		spec_matches(ArgsT, Res, SpecT, Type)
293		;
294		Res = spec_not_matched(Spec, Arg, in(R))).
295
296		error_not_matching_any_pre(Functor, Args, PreSpecs) :-
297		error_handler(X),
298		call(
299		X,
300		fail(
301		prespec_violated(specs(PreSpecs), values(Args), location(Functor))
302		)
303		).
304
305		and_invariant([], [], _, true, _).
306		and_invariant([HSpec|TSpec], [HVal|TVal], Location, R, Type) :-
307		setup_check(Location, ResElement,HSpec, HVal, Type),
308		freeze(TVal, and_invariant(TSpec, TVal, Location, ResTail, Type)), % TODO: do we need this freeze?
309		both_eventually_true(ResElement, ResTail, R).
310
311		:- public and_invariant/4.
312		and_invariant(Specs, Vals, Location, R) :-
313		(ground(Specs) ->
314		and_invariant(Specs, Vals, Location, R, def)
315		;
316		and_invariant(Specs, Vals, Location, R, any)
317		).
318
319
320		or_invariant([], [], Acc, OrigVals, OrigPattern, Location, UberVar) :-
321		freeze(
322		Acc,
323		(Acc == fail ->
324		(reason(OrigPattern, Location, OrigVals, Reason), UberVar = Reason)
325		;
326		true
327		)
328		).
329		or_invariant([H|T], [V|VT], Prior, OrigVals, OrigPattern, Location, UberVar) :-
330		setup_check(Location, ResOption, H, V),
331		freeze(
332		ResOption,
333		(ResOption == true ->
334		(UberVar = true, Current = true)
335		;
336		freeze(
337		Prior,
338		(Prior == true -> true; Current = fail)
339		)
340		)
341		),
342		or_invariant(T, VT, Current, OrigVals, OrigPattern, Location, UberVar).
343
344		:- public or_invariant/4.
345		or_invariant(NewSpecs, NewVals, Location, FutureRes) :-
346		or_invariant(NewSpecs, NewVals, [], NewVals, or(NewSpecs), Location, FutureRes).
347
348		%% merge recursive specs
349		both_eventually_true(V1, V2, Res) :-
350		when((nonvar(V1); nonvar(V2)),
351		(V1 == true
352		-> freeze(V2, Res = V2) %% look at the other co-routined variable
353		; nonvar(V1)
354		-> Res = V1 %% since it is not true
355		; V2 == true
356		-> freeze(V1, Res = V1)
357		; nonvar(V2) -> Res = V2)).