34
35:- module(ctrtchecks,
36 ['$with_asr'/2,
37 '$with_gloc'/2,
38 '$with_ploc'/2,
39 assrt_op/4,
40 check_call/3,
41 check_goal/5,
42 check_asrs_pre/5,
43 collect_assertions/4,
44 current_assertion/4,
45 is_prop_check/5,
46 is_valid_status_type/2,
47 part_time/2,
48 rtcheck_assr_status/1]). 49
50:- use_module(library(apply)). 51:- use_module(library(lists)). 52:- use_module(library(pairs)). 53:- use_module(library(assertions)). 54:- use_module(library(send_check)). 55:- use_module(library(extend_args)). 56:- use_module(library(clambda)). 57:- use_module(library(context_values)). 58:- use_module(library(rtcprops)). 59:- use_module(library(metaprops)). 60:- init_expansors. 61
62:- meta_predicate checkif_modl(?, ?, 0, ?, 0). 63checkif_modl(M, M, _, _, Goal) :- !, call(Goal).
64checkif_modl(_, _, GMod, Goal, Goal) :- call(GMod).
65
66is_prop_check(Step, Level, T, Part, Asr) :-
67 part_time(Part, T),
68 asr_aprop(Asr, type, Type, _),
69 asr_aprop(Asr, stat, Status, _),
70 assrt_op(Part, Step, Level, Type),
71 is_valid_status_type(Status, Type), !.
72
73part_time(call, _).
74part_time(succ, _).
75part_time(glob, rt).
79assrt_op(call, step1, exports, calls).
80assrt_op(call, step1, exports, pred).
81assrt_op(call, step1, exports, prop).
82assrt_op(call, step2, inner, calls).
83assrt_op(call, step2, inner, pred).
84assrt_op(call, step2, inner, prop).
85assrt_op(succ, step1, exports, success).
86assrt_op(succ, step1, exports, pred).
87assrt_op(succ, step1, exports, prop).
88assrt_op(succ, step2, inner, success).
89assrt_op(succ, step2, inner, pred).
90assrt_op(succ, step2, inner, prop).
91assrt_op(glob, step1, exports, comp).
92assrt_op(glob, step1, exports, pred).
93assrt_op(glob, step1, exports, prop).
94assrt_op(glob, step2, inner, comp).
95assrt_op(glob, step2, inner, pred).
96assrt_op(glob, step2, inner, prop).
97
98is_valid_status_type(Status, Type) :-
99 rtcheck_assr_type(Type),
100 rtcheck_assr_status(Status).
101
102rtcheck_assr_status(Status) :-
103 current_prolog_flag(rtchecks_status, StatusL),
104 member(Status, StatusL).
105
106rtcheck_assr_type(calls).
107rtcheck_assr_type(pred).
108rtcheck_assr_type(prop).
109rtcheck_assr_type(comp).
110rtcheck_assr_type(success).
111
126
127black_list_pred(_=_).
128
129assertion_is_valid(T, Status, Type, Asr) :-
130 ( \+ prop_asr(glob, acheck(_), _, Asr),
131 \+ prop_asr(glob, acheck(T, _), _, Asr)
132 ->is_valid_status_type(Status, Type),
133 \+ prop_asr(glob, no_acheck(_), _, Asr),
134 \+ prop_asr(glob, no_acheck(T, _), _, Asr)
135 ; true 136 ).
137
138no_acheck_predicate(T, Pred, M) :-
139 prop_asr(Pred, M, true, comp, _, _, Asr),
140 \+ prop_asr(call, _, _, Asr),
141 ( prop_asr(glob, no_acheck(_), _, Asr)
142 ; prop_asr(glob, no_acheck(T, _), _, Asr)
143 ).
144
145current_assertion(T, Pred, M, Asr) :-
146 prop_asr(Pred, M, Status, Type, _, _, Asr),
147 \+ ( T = rt,
148 prop_asr(Pred, M, _, prop, _, _, _)
149 ),
150 \+ no_acheck_predicate(T, Pred, M),
151 assertion_is_valid(T, Status, Type, Asr),
152 ( current_prolog_flag(rtchecks_level, inner)
153 ->true
154 ; current_prolog_flag(rtchecks_level, exports),
155 predicate_property(M:Pred, exported)
156 ->true
157 ),
158 \+ black_list_pred(Pred).
159
160collect_assertions(T, Pred, M, AsrL) :-
161 copy_term_nat(Pred, Head), % copy to avoid duplication of atributes
162 findall(Head-Asr, current_assertion(T, Head, M, Asr), Pairs),
163 maplist([Pred] +\ (Pred-T)^T^true, Pairs, AsrL).
164
165:- meta_predicate check_goal(+, 0, +, +, +). 166
167check_goal(T, Call, M, CM, AsrL) :-
168 current_prolog_flag(rtchecks_level, Level),
169 checkif_modl(M, CM,
170 check_asrs(T, is_prop_check(step1, Level), AsrL, G2), G2,
171 check_asrs(T, is_prop_check(step2, Level), AsrL, Call)).
172
173:- meta_predicate
174 check_asrs(+, 3, +, +),
175 check_asrs_pre(+, 3, +, -, -). 176
177check_asrs(T, IsPropCheck, AsrL, Goal) :-
178 check_asrs_pre(T, IsPropCheck, AsrL, AsrGlobL, AsrSuccL),
179 checkif_asrs_comp(AsrGlobL, T, Goal),
180 checkif_asrs_props(T, success, AsrSuccL).
181
182check_asrs_pre(T, IsPropCheck, AsrL, AsrGlobL, AsrSuccL) :-
183 prop_rtchecks(T, AsrL, IsPropCheck, call, AsrCallL),
184 prop_rtchecks(T, AsrL, IsPropCheck, succ, AsrSuccL),
185 subtract(AsrSuccL, AsrCallL, DAsrSuccL),
186 prop_rtchecks(T, AsrL, IsPropCheck, glob, AsrGlobL),
187 subtract(AsrGlobL, AsrCallL, DAsrGlobL),
188 check_asrs_props_calls(T, AsrCallL),
189 check_asrs_props(T, success, DAsrSuccL),
190 check_asrs_props(T, comp, DAsrGlobL).
191
192prop_rtchecks(T, AsrL1, IsPropCheck, Part, AsrPVL) :-
193 include(call(IsPropCheck, T, Part), AsrL1, AsrL),
194 pairs_keys_values(AsrPVL, AsrL, _PValuesL).
195
196:- meta_predicate checkif_asrs_comp(+, +, 0). 197checkif_asrs_comp([], _, Goal) :-
198 call(Goal).
199checkif_asrs_comp([Asr-PVL|AsrL], T, Goal1) :-
200 checkif_asr_comp(T, PVL, Asr, Goal1, Goal),
201 checkif_asrs_comp(AsrL, T, Goal).
202
203checkif_asr_comp(T, PropValues, Asr, M:Goal1, M:Goal) :-
204 ( memberchk(PropValues, [[], [[]]]),
205 copy_term_nat(Asr, NAsr),
206 findall(g(NAsr, Glob, Loc),
207 ( asr_aprop(NAsr, glob, Glob, Loc),
208 valid_prop(T, Glob)
209 ), GlobL),
210 GlobL \= []
211 ->comps_to_goal(GlobL, comp_pos_to_goal(Asr), Goal2, M:Goal1),
212 Goal = '$with_asr'(Goal2, Asr)
213 ; Goal = Goal1
214 ).
215
216comp_pos_to_goal(Asr, g(Asr, M:Glob, Loc), '$with_gloc'(M:Glob, Loc), Goal) :-
217 functor(Glob, _, N),
218 arg(N, Glob, Goal).
219
220:- meta_predicate '$with_asr'(0, ?). 221'$with_asr'(Comp, Asr) :-
222 with_value(Comp, '$with_asr', Asr).
223
224:- meta_predicate '$with_gloc'(0, ?). 225'$with_gloc'(Comp, GLoc) :-
226 with_value(Comp, '$with_gloc', GLoc).
227
228:- meta_predicate '$with_ploc'(0, ?). 229'$with_ploc'(Comp, GLoc) :-
230 with_value(Comp, '$with_ploc', GLoc).
242:- meta_predicate comps_to_goal(?, 3, ?, ?). 243comps_to_goal([], _) --> [].
244comps_to_goal([Check|Checks], Goal) -->
245 comps_to_goal2(Checks, Check, Goal).
246
247:- meta_predicate comps_to_goal2(?, ?, 3, ?, ?). 248comps_to_goal2([], Check, Goal) -->
249 call(Goal, Check).
250comps_to_goal2([Check|Checks], Check1, Goal) -->
251 call(Goal, Check1),
252 comps_to_goal2(Checks, Check, Goal).
253
254:- meta_predicate check_call(+, +, 0). 255check_call(T, AsrL, Goal) :-
256 predicate_property(Goal, implementation_module(M)),
257 check_call(T, Goal, M, AsrL).
258
260check_call(ct, CM:_, M, AsrL) :- check_goal(ct, CM:true, M, CM, AsrL).
261check_call(rt, CM:Call, M, AsrL) :- check_goal(rt, CM:Call, M, CM, AsrL).
262
263check_asrs_props_calls(T, AsrPVL) :-
264 check_asrs_props_all(T, calls, AsrPVL).
265
266check_asrs_props_all(T, PType, AsrPVL) :-
267 check_asrs_props(T, PType, AsrPVL),
268 ( \+ memberchk(_-[], AsrPVL)
269 ->maplist(send_check_asr(PType), AsrPVL)
270 ; true
271 ).
272
273check_asrs_props(T, PType, AsrPVL) :-
274 maplist(check_asr_props(T, PType), AsrPVL).
275
276checkif_asrs_props(T, PType, AsrPVL) :-
277 maplist(checkif_asr_props(T, PType), AsrPVL).
278
279checkif_asr_props(T, PType, Asr-CondValues) :-
280 checkif_asr_props(T, CondValues, Asr, PType).
281
282check_asr_props(T, PType, Asr-PropValues) :-
283 check_asr_props(T, Asr, inco, PType, PropValues).
284
285send_check_asr(PType, Asr-PropValues) :-
286 ( PropValues = [[]] 287 ->true
288 ; once(asr_aprop(Asr, head, Pred, ALoc)),
289 send_check(PropValues, PType, Pred, ALoc)
290 ).
291
292checkif_asr_props(T, CondValues, Asr, PType) :-
293 ( memberchk(CondValues, [[], [[]]])
294 ->check_asr_props(T, Asr, cond, PType, PropValues),
295 send_check_asr(PType, Asr-PropValues)
296 ; true
297 ).
298
299check_asr_props(T, Asr, Cond, PType, PropValues) :-
300 copy_term_nat(Asr, NAsr),
301 once(asr_aprop(NAsr, head, _:Pred, _)),
302 term_variables(Pred, VU),
303 sort(VU, VS),
304 findall(NAsr-PropValue,
305 current_asr_prop_value(VS, T, Cond, PType, NAsr, PropValue),
306 AsrPropValues),
307 maplist([Asr] +\ (Asr-PV)^PV^true, AsrPropValues, PropValues).
308
309current_asr_prop_value(VS, T, Cond, PType, NAsr, PropValue) :-
310 ( type_cond_part_check_mult(Cond, PType, Part, Check, Mult),
311 asr_aprop(NAsr, Part, Prop, From)
312 *->
313 make_valid_prop(T, Prop, VProp), 314 \+ catch(check_prop(Check, VS, VProp),
315 Error,
316 send_signal(at_location(From, Error))),
317 last_prop_failure(L),
318 (Mult = once -> ! ; true),
319 CheckProp =.. [Check, Prop],
320 PropValue = (From/CheckProp-L)
321 ; PropValue = [] 322 ).
323
324check_prop(compat, VS, Prop) :- compat(Prop, VS).
325check_prop(instan, VS, Prop) :- instan(Prop, VS).
326
327make_valid_prop(T, M:Prop, M:Valid) :-
328 make_valid_prop(Prop, M, T, Valid).
329
330disj_prop(true, A, A).
331disj_prop(A, true, A).
332disj_prop(A, B, (A;B)).
333
334conj_prop(true, _, true).
335conj_prop(_, true, true).
336conj_prop(A, B, (A,B)).
337
338make_valid_prop(A;B, M, T, V) :-
339 !,
340 make_valid_prop(A, M, T, VA),
341 make_valid_prop(B, M, T, VB),
342 once(disj_prop(VA, VB, V)).
343make_valid_prop((A,B), M, T, V) :-
344 !,
345 make_valid_prop(A, M, T, VA),
346 make_valid_prop(B, M, T, VB),
347 once(conj_prop(VA, VB, V)).
348make_valid_prop(list(Type, X), M, T, V) :-
349 350 !,
351 ( extend_args(Type, [_], Type1),
352 valid_prop(T, M, Type1)
353 ->V = list(Type, X)
354 ; V = list(X)
355 ).
356make_valid_prop(A, M, T, V) :-
357 ( valid_prop(T, M, A)
358 ->V = A
359 ; V = true
360 ).
361
362:- meta_predicate valid_prop(+, 0 ). 363
364valid_prop(T, M:Prop) :- valid_prop(T, M, Prop).
365
366valid_prop(T, M, Prop) :-
367 functor(Prop, F, A),
368 tabled_valid_prop(T, M, F, A).
369
370:- table tabled_valid_prop/4. 371
372tabled_valid_prop(T, M, F, A) :-
373 functor(H, F, A),
374 \+ (( prop_asr(head, M:H, _, Asr),
375 ( prop_asr(glob, no_acheck( _), _, Asr)
376 ; prop_asr(glob, no_acheck(T, _), _, Asr)
377 )
378 )).
379
380type_cond_part_check_mult(inco, PType, Part, Check, Mult) :-
381 type_inco_part_check_mult(PType, Part, Check, Mult).
382type_cond_part_check_mult(cond, PType, Part, Check, Mult) :-
383 type_cond_part_check_mult(PType, Part, Check, Mult).
384
385type_inco_part_check_mult(calls, call, instan, call).
386type_inco_part_check_mult(calls, comp, compat, call).
387type_inco_part_check_mult(success, call, instan, once).
388type_inco_part_check_mult(success, comp, compat, once).
389type_inco_part_check_mult(comp, call, instan, once).
390
391type_cond_part_check_mult(success, comp, compat, call).
392type_cond_part_check_mult(success, succ, instan, call)