1		% (c) 2014-2022 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		:- module(ctigar,[ctigar_symbolic_model_check/1]).
6
7		:- use_module(probsrc(module_information)).
8		:- module_info(group,symbolic_model_checker).
9		:- module_info(description,'An infinite-state symbolic model checker based on CTIGAR.').
10
11		:- use_module(library(heaps)).
12		:- use_module(library(avl)).
13		:- use_module(library(ordsets)).
14		:- use_module(library(lists)).
15
16		:- use_module(extension('counter/counter'),[counter_init/0,
17		new_counter/1,
18		get_counter/2]).
19
20		:- use_module(probsrc(preferences), [get_preference/2]).
21		:- use_module(probsrc(bmachine),[b_get_invariant_from_machine/1,
22		%b_get_initialisation_from_machine/2,
23		b_get_properties_from_machine/1,
24		b_get_machine_operation/4,
25		b_specialized_invariant_for_op/2,
26		get_proven_invariant/2]).
27		:- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2,
28		disjunct_predicates/2,
29		conjunction_to_list/2,
30		create_implication/3,
31		create_negation/2
32		%create_exists/3, replace_id_by_expr/4
33		]).
34		:- use_module(probsrc(translate), [translate_bexpression/2, print_bexpr/1]).
35		:- use_module(probsrc(state_space),[state_space_reset/0]).
36		:- use_module(extrasrc(unsat_cores), [unsat_core_with_fixed_conjuncts/3]).
37		:- use_module(extrasrc(weakest_preconditions), [weakest_precondition/3]).
38
39		:- use_module(symbolic_model_checker(predicate_handling)).
40		:- use_module(symbolic_model_checker(solver_handling)).
41		:- use_module(symbolic_model_checker(mic_generation)).
42		:- use_module(symbolic_model_checker(predicate_abstraction)).
43
44		% algorithm for computing the minimal inductive clause
45		mic_algorithm(down).
46		% mic_algorithm(ctgDown).
47
48		ctigar_symbolic_model_check(Res) :-
49		statistics(walltime,[Start,_]),
50		catch(symbolic_model_check_aux(Res),solver_and_provers_too_weak,Res=solver_and_provers_too_weak),
51		statistics(walltime,[End,_]),
52		Took is End - Start,
53		get_counter(ic3solvercalls,Calls),
54		format('Result of CTIGAR based model checking: ~w,~nCTIGAR took ~w ms and ~w solver calls~n',[Res,Took,Calls]).
55
56		symbolic_model_check_aux(Result) :-
57		% count number of solver calls
58		counter_init, new_counter(ic3solvercalls),
59		% fetch the invariant we want to check
60		b_get_invariant_from_machine(Invariant),
61		% and the predicate describing the initial state
62		get_initial_state_predicate(Init),
63		% debug output
64		translate_bexpression(Init,PPInit), translate_bexpression(Invariant,PPInvariant),
65		format('Symbolic Model Checking:~nProperty: ~w~nInitial Predicate: ~w~n',[PPInvariant,PPInit]),
66		symbolic_model_check(Invariant,Init,Result).
67
68		% check base cases (length 0 and 1) first - as in Bradleys implementation
69		symbolic_model_check(Property,Init,ResultOut) :-
70		% ce of length 0? check if Init => Invariant
71		create_implication(Init,Property,Predicate),
72		% debug output
73		translate_bexpression(Predicate,PPPredicate),
74		format('Checking: ~w~n',[PPPredicate]),
75		solve_negated(Predicate,Result),
76		functor(Result,ForPrint,_),
77		format('Counter-Example of Length 0 exists: ~w~n', [ForPrint]),
78		Result = solution(Sol), !,
79		create_state_predicate(Sol,StatePred),
80		replay_counter_example([StatePred]),
81		ResultOut = counterexample_found.
82		symbolic_model_check(Property,Init,ResultOut) :-
83		% ce of length 1? check if Init & Transition => Invariant'
84		prime_predicate(Property,PrimedProperty),
85		get_single_transition_predicate(OpName,Transition),
86		conjunct_predicates([Init,Transition],LHS),
87		create_implication(LHS,PrimedProperty,Predicate),
88		% debug output
89		translate_bexpression(Predicate,PPPredicate),
90		format('Checking: ~w~n',[PPPredicate]),
91		solve_negated(Predicate,Result),
92		functor(Result,ForPrint,_),
93		format('Counter-Example of Length 1 (transition ~w) exists: ~w~n', [OpName,ForPrint]),
94		Result = solution(Sol), !,
95		handle_counter_example(Sol,[]),
96		ResultOut = counterexample_found.
97		% recursively check other cases. this corresponds to method "check" of Bradleys reference implementation
98		% internal data structures taken from Bradleys original paper:
99		% frame(F_i as in the paper (+transition), set of clauses to check for convergence)
100		% i/K (= level) is the key to the AVL tree
101		% obligation(state / predicate, primary inputs / predicate, list of successor states)
102		% level is the key to the priority queue
103		symbolic_model_check(Property,Init,Result) :-
104		K = 1,
105		% two initial frames:
106		% F_0 holds the initial condition
107		% F_1 holds the property
108		% further frames will be added by extend later on
109		% we store the transition in the frames as well in order to spare passing it around
110		b_get_properties_from_machine(PropertiesOnConstants),
111		F_0 = frame([Init,PropertiesOnConstants],[]), F_1 = frame([Property,PropertiesOnConstants],[]),
112		empty_avl(E),
113		avl_store(0,E,F_0,FramesT),
114		avl_store(1,FramesT,F_1,Frames),
115		get_abstract_domain(Domain),
116		catch(symbolic_model_check_fx(K,Frames,Domain,Property,Init,Result),
117		ic3_counter_example(Solution,Succs),
118		(handle_counter_example(Solution,Succs),Result=counterexample_found)).
119
120		symbolic_model_check_fx(K,Frames,Domain,Property,Init,Result) :-
121		% initially, K is 1
122		% the algorithm tries to maintain the following invariants:
123		% (1) ! i . i > 0 . I => F_i
124		% (2) ! i . i > 0 . F_i => P (P = Property to check / Invariant)
125		% (3) ! i . i > 0 . clauses(F_{i+1}) <: clauses(F_i)
126		% (4) ! i . 0 <= i < k . F_i & T => F_{i+1}'
127		extend(Frames,K,[Property],Frames2),
128		% strengthen establishes (1) - (4)
129		% if impossible => counter example
130		strengthen(K,Frames2,Domain,Property,FramesOut,RefinedDomain), !,
131		% propagate_clauses assumes (1) - (4)
132		% pushes clauses from one frame to a later one (as far as possible)
133		propagate_clauses(K,FramesOut,FramesOut2),
134		(check_convergence(FramesOut2)
135		-> Result = property_holds
136		; K2 is K + 1,
137		symbolic_model_check_fx(K2,FramesOut2,RefinedDomain,Property,Init,Result)).
138
139		:- public print_frames/1. % for debugging
140		print_frames(Frames) :-
141		avl_to_list(Frames,List),
142		print_frames_list(List).
143		print_frames_list([]).
144		print_frames_list([K-frame(_,Clauses)|T]) :-
145		length(Clauses,L),
146		format('frame ~w holds ~w clauses:~n',[K,L]),
147		%print_clauses(Clauses),
148		print_frames_list(T).
149
150		:- public print_clauses/1. % for debugging
151		print_clauses([]).
152		print_clauses([C|Cs]) :-
153		disjunct_predicates(C,DC),
154		translate:print_bexpr(DC),nl,
155		print_clauses(Cs).
156
157		extend(FramesIn,K,Content,FramesOut) :-
158		% any new frame holds the properties in addition to the content (usually the transition)
159		NextFrameId is K + 1,
160		b_get_properties_from_machine(PropertiesOnConstants),
161		avl_store(NextFrameId,FramesIn,frame([PropertiesOnConstants|Content],[]),FramesOut).
162
163		propagate_clauses(K,Frames,FramesOut) :-
164		propagate_clauses_aux(1,K,Frames,FramesOut).
165		propagate_clauses_aux(I,K,Frames,FramesOut) :-
166		% for i = 1 .. K call propagate_clauses_on_level
167		propagate_clauses_on_level(I,Frames,FramesTemp),
168		(I < K -> J is I+1, propagate_clauses_aux(J,K,FramesTemp,FramesOut) ; true).
169		propagate_clauses_on_level(I,Frames,FramesOut) :-
170		% pushes from F_I to F_{I+1}
171		IP1 is I + 1,
172		clauses_on_level(I,Frames,_F_From,ClausesFrom),
173		in_solver_on_level(I,Frames,IS),
174
175		include(inductive_clause(IS),ClausesFrom,InductiveClauses),
176
177		add_clauses_to_level(IP1,Frames,InductiveClauses,FramesOut).
178
179		inductive_clause(F_I,ClauseDisjuncts) :-
180		get_transition_predicate(T),
181		disjunct_predicates(ClauseDisjuncts,Clause),
182		% checks if a single clause is inductive relative to F_i
183		% by verifying if F_i => C' (F_i includes T)
184		% i.e. there is a contradiction in not C' & F_i
185		create_negation(Clause,NegClause),
186		prime_predicate(NegClause,NegCPrime),
187		conjunct_predicates([NegCPrime,T|F_I],Pred),
188		solve(Pred,Result), !,
189		Result = contradiction_found(_).
190
191		strengthen(K,Frames,Domain,Property,FramesOut,RefinedDomain) :-
192		findall(op(OpName,Trans),get_single_transition_predicate(OpName,Trans),Transitions),
193		strengthen_aux1(Transitions,K,Property,Frames,FramesOut,Domain,RefinedDomain).
194
195		strengthen_aux1([],_K,_Property,Frames,Frames,Domain,Domain).
196		strengthen_aux1([Transition|Transitions],K,Property,Frames,FramesOut,Domain,RefinedDomain) :-
197		strengthen_loop(Transition,K,Property,Frames,FramesTemp,Domain,TempDomain),
198		strengthen_aux1(Transitions,K,Property,FramesTemp,FramesOut,TempDomain,RefinedDomain).
199
200		strengthen_loop(op(OpName,Transition),K,Property,FramesIn,FramesOut,DomainIn,DomainOut) :-
201		get_preference(use_po,UsePO),
202		strengthen_get_property(UsePO,OpName,Property,PrimedNegProperty),
203		in_solver_on_level(K,FramesIn,IS),
204		conjunct_predicates([Transition,PrimedNegProperty|IS],RPred),
205		solve(RPred,Result),
206		strengthen_aux(Result,Transition,K,Property,FramesIn,FramesOut,DomainIn,DomainOut).
207
208		strengthen_get_property(false,_OpName,Property,PrimedNegProperty) :-
209		create_negation(Property,NegProperty),
210		prime_predicate(NegProperty,PrimedNegProperty).
211		strengthen_get_property(true,OpName,FullProperty,Primed) :-
212		(b_specialized_invariant_for_op(OpName,Property)
213		-> true ; Property = FullProperty),
214		(get_proven_invariant(OpName,Proven)
215		-> true ; Proven = b(truth,pred,[])),
216		create_negation(Property,NegProperty),
217		conjunct_predicates([Proven,NegProperty],ToPrime),
218		prime_predicate(ToPrime,Primed).
219
220		% strengthen searches for a counter example to the property
221		% it searches for a state that is permitted by F_i that is the predecessor
222		% of a state that violates the property
223		% if there is a contradiction, we are done, because there is no counter example
224		strengthen_aux(contradiction_found(_),_TransitionPredicate,_K,_Property,Frames,Frames,Domain,Domain).
225		% if there is a counter example, we need to strenghten the frames
226		% in order to make it spurious, i.e. (1) - (4) have to be reestablished
227		strengthen_aux(solution(Wit),TransitionPredicate,K,Property,Frames,FramesOut,Domain,DomainOut) :-
228		% extract predecessor
229		create_state_predicate(Wit,Pre),
230		create_succ_state_predicate(Wit,SStatePred),
231		create_primary_inputs_predicate(Wit,Inputs),
232		K2 is K-2,
233		% finds the highest N to which not Pre can be added
234		% this can fail if the counter example is not spurious
235		inductively_generalize(Pre,[Pre],K2,K,Frames,FramesT,N), !,
236		N2 is N + 1,
237		empty_heap(H),
238		generalize_and_add(concrete,TransitionPredicate,K,H,N2,Frames,Domain,RefinedDomain,Pre,Inputs,[SStatePred],Obls),
239		% Obls is a heap of proof obligations that need to hold
240		% push generalization handles those that are on level =< K
241		push_generalization(Obls,K,FramesT,FramesT2,RefinedDomain,ReRefinedDomain),
242		strengthen(K,FramesT2,ReRefinedDomain,Property,FramesOut,DomainOut).
243
244		% generalize Pre and / or split it into multiple obligations
245		generalize_and_add(concrete,TP,I,HIn,N,Frames,Domain,Domain,State,Inputs,[SuccState|SuccStates],HOut) :-
246		concrete_state_to_abstract_state(Domain,State,AbsCTI),
247		write(absstate(AbsCTI)),nl,
248		% check if lifting is possible / if query is actually unsat
249		in_solver_on_level(I,Frames,IS),
250		prime_predicate(SuccState,TPrime),
251		create_negation(TPrime,NotTPrime),
252		conjunct_predicates([NotTPrime,TP|IS],Conjunction),
253		conjunct_predicates([AbsCTI,Conjunction],VerifyQuery),
254		solve(VerifyQuery,Result),
255		write(result(Result)),nl,
256		Result = contradiction_found(_), !,
257		% query is unsat and lifting succeeds
258		unsat_core_with_fixed_conjuncts(AbsCTI,Conjunction,Core),
259		I2 is I-1, M is N+1,
260		NewObligation = obligation(Core,TP,Inputs,[SuccState|SuccStates],I2,M),
261		add_to_heap(HIn,N,NewObligation,HOut).
262		generalize_and_add(concrete,TP,I,HIn,N,Frames,Domain,RefinedDomain,State,Inputs,[SuccState|SuccStates],HOut) :-
263		findall(WP,
264		(b_get_machine_operation(_,_,_,D),weakest_precondition(D,SuccState,WP)),
265		WeakestPreconditions),
266		conjunct_predicates(WeakestPreconditions,BigConjunction),
267		conjunction_to_list(BigConjunction,AllConjuncts),
268		list_to_ord_set(AllConjuncts,OrdAllConjuncts),
269		ord_union(OrdAllConjuncts,Domain,NewDomain),
270		length(Domain,LD), length(NewDomain,NLD),
271		(NLD = LD -> write('diverges'),nl,trace ; true),
272		generalize_and_add(concrete,TP,I,HIn,N,Frames,NewDomain,RefinedDomain,State,Inputs,[SuccState|SuccStates],HOut).
273
274		push_generalization(Obligations,_K,Frames,Frames,Domain,Domain) :-
275		empty_heap(Obligations). % no proof obligations left
276		push_generalization(Obligations,K,Frames,Frames,Domain,Domain) :-
277		min_of_heap(Obligations,N,_S),
278		N > K, !. % only proof obligations on a higher level left - fine for level K
279		push_generalization(Obligations,K,Frames,FramesOut,Domain,DomainOut) :-
280		% grep the proof obligations with the lowest level - somewhat a heuristic
281		min_of_heap(Obligations,N,obligation(S,T,Inputs,Succs,I,M)),
282		in_solver_on_level(N,Frames,IS),
283		prime_predicate(S,SPrimed),
284		conjunct_predicates([SPrimed,T|IS],Pred),
285		solve(Pred,Result), !,
286		push_generalization_aux(Result,T,N,obligation(S,T,Inputs,Succs,I,M),Obligations,K,Frames,FramesT,Domain,RefinedDomain,ObligationsOut),
287		push_generalization(ObligationsOut,K,FramesT,FramesOut,RefinedDomain,DomainOut).
288
289		push_generalization_aux(solution(Pre),_T,N,obligation(S,T,Inputs,Succs,_I,_M),Obligations,K,Frames,FramesOut,Domain,RefinedDomain,ObligationsOut) :-
290		N2 is N - 2,
291		create_state_predicate(Pre,PrePred), !,
292		inductively_generalize(PrePred,[S|Succs],N2,K,Frames,FramesOut,M), !,
293		M2 is M + 1,
294		generalize_and_add(concrete,T,K,Obligations,M2,Frames,Domain,RefinedDomain,PrePred,Inputs,[S|Succs],ObligationsOut).
295		push_generalization_aux(contradiction_found(_),_T,N,obligation(S,T,Inputs,Succs,I,M),Obligations,K,Frames,FramesOut,Domain,Domain,ObligationsOut) :-
296		inductively_generalize(S,[S|Succs],N,K,Frames,FramesOut,Lvl), !,
297		delete_from_heap(Obligations,N,obligation(S,T,Inputs,Succs,I,M),ObligationsT),
298		M2 is M + 1, NLvl is Lvl + 1,
299		add_to_heap(ObligationsT,NLvl,obligation(S,T,Inputs,Succs,I,M2),ObligationsOut).
300
301		:- public print_heap/1. % for debugging
302		print_heap(Obls) :-
303		heap_to_list(Obls,List),
304		write('Content of Obligations Heap:'), nl,
305		print_heap2(List).
306		print_heap2([]).
307		print_heap2([Key-Datum|T]) :-
308		Datum = obligation(Predicate,_,Succs),
309		translate_bexpression(Predicate,PPPredicate),
310		format('On level ~w state predicate ~w~n',[Key,PPPredicate]),
311		format('Successors:~n',[]),
312		print_succs(Succs),
313		print_heap2(T).
314		print_succs([]).
315		print_succs([P|T]) :-
316		write(' '), print_bexpr(P),nl,
317		print_succs(T).
318
319		handle_counter_example(Solution,Succs) :-
320		create_state_predicate(Solution,StatePred),
321		create_succ_state_predicate(Solution,SuccStatePred), !,
322		format('Counterexample found. Trace:~n',[]),
323		print_succs([StatePred,SuccStatePred|Succs]),
324		(create_constants_state_predicate(Solution,ConstantsStatePred)
325		-> replay_counter_example([ConstantsStatePred,StatePred,SuccStatePred|Succs])
326		; replay_counter_example([StatePred,SuccStatePred|Succs])).
327		replay_counter_example(A) :-
328		state_space_reset,
329		replay_aux(A,_).
330		:- use_module(probsrc(b_trace_checking),[find_successor_state/4]).
331		replay_aux([],_).
332		replay_aux([P|Ps],CurId) :-
333		find_successor_state(CurId,P,SuccID,_),
334		replay_aux(Ps,SuccID).
335
336		inductively_generalize(S,Succs,Min,_K,Frames,_FramesOut,_N) :-
337		% if min < 0 and sat(F_0 & T & neg S & S')
338		% fail to report counter example
339		Min < 0,
340		in_solver_on_level(0,Frames,IS),
341		prime_predicate(S,SPrimed),
342		create_negation(S,SNegated),
343		get_transition_predicate(T),
344		conjunct_predicates([SNegated,SPrimed,T|IS],Pred),
345		solve(Pred,Result),
346		Result = solution(Solution), !,
347		throw(ic3_counter_example(Solution,Succs)).
348		inductively_generalize(S,_,Min,K,Frames,FramesOut,N) :-
349		I is max(1, Min + 1),
350		inductively_generalize_aux(I,S,K,Frames,FramesOut,N).
351		inductively_generalize_aux(I,S,K,Frames,FramesOut,N) :-
352		I =< K,
353		in_solver_on_level(I,Frames,IS),
354		prime_predicate(S,SPrimed),
355		create_negation(S,SNegated),
356		get_transition_predicate(T),
357		conjunct_predicates([SNegated,SPrimed,T|IS],Pred),
358		solve(Pred,Result), !,
359		(Result = solution(_) -> N is I - 1, generate_clause(S,N,K,Frames,FramesOut) ;
360		Result = contradiction_found(_) -> I2 is I + 1, inductively_generalize_aux(I2,S,K,Frames,FramesOut,N)).
361		inductively_generalize_aux(I,S,K,Frames,FramesOut,K) :-
362		I > K,
363		generate_clause(S,K,K,Frames,FramesOut).
364
365		generate_clause(S,I,K,Frames,FramesOut) :-
366		mic(S,I,K,Frames,FramesT,Q),
367		translate_bexpression(S,PS),
368		translate_bexpression(Q,PQ),
369		format('minimal inductive clause computation:~n~w to~n~w~n',[PS,PQ]),
370		conjunction_to_list(Q,Conjuncts),
371		maplist(create_negation,Conjuncts,NegConjuncts),
372		generate_clause_aux(1,NegConjuncts,I,FramesT,FramesOut).
373		generate_clause_aux(J,NegS,I,Frames,FramesOut) :-
374		J =< I + 1, !,
375		add_clauses_to_level(J,Frames,[NegS],FramesT),
376		J2 is J + 1,
377		generate_clause_aux(J2,NegS,I,FramesT,FramesOut).
378		generate_clause_aux(_,_,_,Frames,Frames).
379
380		mic(S,I,_K,Frames,Frames,Q) :-
381		mic_algorithm(down), !,
382		conjunction_to_list(S,Conjuncts),
383		down(Conjuncts,I,Frames,ConjunctsOut),
384		conjunct_predicates(ConjunctsOut,Q).
385		mic(S,I,K,FramesIn,FramesOut,Q) :-
386		mic_algorithm(ctgDown), !,
387		conjunction_to_list(S,Conjuncts),
388		ctgDown(Conjuncts,I,K,FramesIn,FramesOut,ConjunctsOut),
389		conjunct_predicates(ConjunctsOut,Q).
390
391		check_convergence(Frames) :-
392		avl_to_list(Frames,L),
393		check_convergence_aux(L).
394		check_convergence_aux([_-F1,K2-F2|Fs]) :-
395		% the algorithm converges if two frames hold the same set of clauses
396		F1 = frame(_,Clauses1),
397		F2 = frame(_,Clauses2),
398		% assumes ordered sets
399		(ord_symdiff(Clauses1, Clauses2, []) ; check_convergence_aux([K2-F2|Fs])).