1		% (c) 2014-2019 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(probsrc(unsat_cores), [unsat_core_with_fixed_conjuncts/3]).
37		:- use_module(probsrc(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		% for i = 1 .. K call propagate_clauses_on_level
165		for(I,1,K), fromto(Frames,In,Out,FramesOut)
166		do propagate_clauses_on_level(I,In,Out).
167		propagate_clauses_on_level(I,Frames,FramesOut) :-
168		% pushes from F_I to F_{I+1}
169		IP1 is I + 1,
170		clauses_on_level(I,Frames,_F_From,ClausesFrom),
171		in_solver_on_level(I,Frames,IS),
172
173		include(inductive_clause(IS),ClausesFrom,InductiveClauses),
174
175		add_clauses_to_level(IP1,Frames,InductiveClauses,FramesOut).
176
177		inductive_clause(F_I,ClauseDisjuncts) :-
178		get_transition_predicate(T),
179		disjunct_predicates(ClauseDisjuncts,Clause),
180		% checks if a single clause is inductive relative to F_i
181		% by verifying if F_i => C' (F_i includes T)
182		% i.e. there is a contradiction in not C' & F_i
183		create_negation(Clause,NegClause),
184		prime_predicate(NegClause,NegCPrime),
185		conjunct_predicates([NegCPrime,T|F_I],Pred),
186		solve(Pred,Result), !,
187		Result = contradiction_found(_).
188
189		strengthen(K,Frames,Domain,Property,FramesOut,RefinedDomain) :-
190		findall(op(OpName,Trans),get_single_transition_predicate(OpName,Trans),Transitions),
191		(foreach(Transition,Transitions),
192		fromto(Frames,TFIn,TFOut,FramesOut), fromto(Domain,TDIn,TDOut,RefinedDomain),
193		param(K), param(Property)
194		do strengthen_loop(Transition,K,Property,TFIn,TFOut,TDIn,TDOut)).
195
196		strengthen_loop(op(OpName,Transition),K,Property,FramesIn,FramesOut,DomainIn,DomainOut) :-
197		get_preference(use_po,UsePO),
198		strengthen_get_property(UsePO,OpName,Property,PrimedNegProperty),
199		in_solver_on_level(K,FramesIn,IS),
200		conjunct_predicates([Transition,PrimedNegProperty|IS],RPred),
201		solve(RPred,Result),
202		strengthen_aux(Result,Transition,K,Property,FramesIn,FramesOut,DomainIn,DomainOut).
203
204		strengthen_get_property(false,_OpName,Property,PrimedNegProperty) :-
205		create_negation(Property,NegProperty),
206		prime_predicate(NegProperty,PrimedNegProperty).
207		strengthen_get_property(true,OpName,FullProperty,Primed) :-
208		(b_specialized_invariant_for_op(OpName,Property)
209		-> true ; Property = FullProperty),
210		(get_proven_invariant(OpName,Proven)
211		-> true ; Proven = b(truth,pred,[])),
212		create_negation(Property,NegProperty),
213		conjunct_predicates([Proven,NegProperty],ToPrime),
214		prime_predicate(ToPrime,Primed).
215
216		% strengthen searches for a counter example to the property
217		% it searches for a state that is permitted by F_i that is the predecessor
218		% of a state that violates the property
219		% if there is a contradiction, we are done, because there is no counter example
220		strengthen_aux(contradiction_found(_),_TransitionPredicate,_K,_Property,Frames,Frames,Domain,Domain).
221		% if there is a counter example, we need to strenghten the frames
222		% in order to make it spurious, i.e. (1) - (4) have to be reestablished
223		strengthen_aux(solution(Wit),TransitionPredicate,K,Property,Frames,FramesOut,Domain,DomainOut) :-
224		% extract predecessor
225		create_state_predicate(Wit,Pre),
226		create_succ_state_predicate(Wit,SStatePred),
227		create_primary_inputs_predicate(Wit,Inputs),
228		K2 is K-2,
229		% finds the highest N to which not Pre can be added
230		% this can fail if the counter example is not spurious
231		inductively_generalize(Pre,[Pre],K2,K,Frames,FramesT,N), !,
232		N2 is N + 1,
233		empty_heap(H),
234		generalize_and_add(concrete,TransitionPredicate,K,H,N2,Frames,Domain,RefinedDomain,Pre,Inputs,[SStatePred],Obls),
235		% Obls is a heap of proof obligations that need to hold
236		% push generalization handles those that are on level =< K
237		push_generalization(Obls,K,FramesT,FramesT2,RefinedDomain,ReRefinedDomain),
238		strengthen(K,FramesT2,ReRefinedDomain,Property,FramesOut,DomainOut).
239
240		% generalize Pre and / or split it into multiple obligations
241		generalize_and_add(concrete,TP,I,HIn,N,Frames,Domain,Domain,State,Inputs,[SuccState|SuccStates],HOut) :-
242		concrete_state_to_abstract_state(Domain,State,AbsCTI),
243		write(absstate(AbsCTI)),nl,
244		% check if lifting is possible / if query is actually unsat
245		in_solver_on_level(I,Frames,IS),
246		prime_predicate(SuccState,TPrime),
247		create_negation(TPrime,NotTPrime),
248		conjunct_predicates([NotTPrime,TP|IS],Conjunction),
249		conjunct_predicates([AbsCTI,Conjunction],VerifyQuery),
250		solve(VerifyQuery,Result),
251		write(result(Result)),nl,
252		Result = contradiction_found(_), !,
253		% query is unsat and lifting succeeds
254		unsat_core_with_fixed_conjuncts(AbsCTI,Conjunction,Core),
255		I2 is I-1, M is N+1,
256		NewObligation = obligation(Core,TP,Inputs,[SuccState|SuccStates],I2,M),
257		add_to_heap(HIn,N,NewObligation,HOut).
258		generalize_and_add(concrete,TP,I,HIn,N,Frames,Domain,RefinedDomain,State,Inputs,[SuccState|SuccStates],HOut) :-
259		findall(WP,
260		(b_get_machine_operation(_,_,_,D),weakest_precondition(D,SuccState,WP)),
261		WeakestPreconditions),
262		conjunct_predicates(WeakestPreconditions,BigConjunction),
263		conjunction_to_list(BigConjunction,AllConjuncts),
264		list_to_ord_set(AllConjuncts,OrdAllConjuncts),
265		ord_union(OrdAllConjuncts,Domain,NewDomain),
266		length(Domain,LD), length(NewDomain,NLD),
267		(NLD = LD -> write('diverges'),nl,trace ; true),
268		generalize_and_add(concrete,TP,I,HIn,N,Frames,NewDomain,RefinedDomain,State,Inputs,[SuccState|SuccStates],HOut).
269
270		push_generalization(Obligations,_K,Frames,Frames,Domain,Domain) :-
271		empty_heap(Obligations). % no proof obligations left
272		push_generalization(Obligations,K,Frames,Frames,Domain,Domain) :-
273		min_of_heap(Obligations,N,_S),
274		N > K, !. % only proof obligations on a higher level left - fine for level K
275		push_generalization(Obligations,K,Frames,FramesOut,Domain,DomainOut) :-
276		% grep the proof obligations with the lowest level - somewhat a heuristic
277		min_of_heap(Obligations,N,obligation(S,T,Inputs,Succs,I,M)),
278		in_solver_on_level(N,Frames,IS),
279		prime_predicate(S,SPrimed),
280		conjunct_predicates([SPrimed,T|IS],Pred),
281		solve(Pred,Result), !,
282		push_generalization_aux(Result,T,N,obligation(S,T,Inputs,Succs,I,M),Obligations,K,Frames,FramesT,Domain,RefinedDomain,ObligationsOut),
283		push_generalization(ObligationsOut,K,FramesT,FramesOut,RefinedDomain,DomainOut).
284
285		push_generalization_aux(solution(Pre),_T,N,obligation(S,T,Inputs,Succs,_I,_M),Obligations,K,Frames,FramesOut,Domain,RefinedDomain,ObligationsOut) :-
286		N2 is N - 2,
287		create_state_predicate(Pre,PrePred), !,
288		inductively_generalize(PrePred,[S|Succs],N2,K,Frames,FramesOut,M), !,
289		M2 is M + 1,
290		generalize_and_add(concrete,T,K,Obligations,M2,Frames,Domain,RefinedDomain,PrePred,Inputs,[S|Succs],ObligationsOut).
291		push_generalization_aux(contradiction_found(_),_T,N,obligation(S,T,Inputs,Succs,I,M),Obligations,K,Frames,FramesOut,Domain,Domain,ObligationsOut) :-
292		inductively_generalize(S,[S|Succs],N,K,Frames,FramesOut,Lvl), !,
293		delete_from_heap(Obligations,N,obligation(S,T,Inputs,Succs,I,M),ObligationsT),
294		M2 is M + 1, NLvl is Lvl + 1,
295		add_to_heap(ObligationsT,NLvl,obligation(S,T,Inputs,Succs,I,M2),ObligationsOut).
296
297		:- public print_heap/1. % for debugging
298		print_heap(Obls) :-
299		heap_to_list(Obls,List),
300		write('Content of Obligations Heap:'), nl,
301		print_heap2(List).
302		print_heap2([]).
303		print_heap2([Key-Datum|T]) :-
304		Datum = obligation(Predicate,_,Succs),
305		translate_bexpression(Predicate,PPPredicate),
306		format('On level ~w state predicate ~w~n',[Key,PPPredicate]),
307		format('Successors:~n',[]),
308		print_succs(Succs),
309		print_heap2(T).
310		print_succs([]).
311		print_succs([P|T]) :-
312		write(' '), print_bexpr(P),nl,
313		print_succs(T).
314
315		handle_counter_example(Solution,Succs) :-
316		create_state_predicate(Solution,StatePred),
317		create_succ_state_predicate(Solution,SuccStatePred), !,
318		format('Counterexample found. Trace:~n',[]),
319		print_succs([StatePred,SuccStatePred|Succs]),
320		(create_constants_state_predicate(Solution,ConstantsStatePred)
321		-> replay_counter_example([ConstantsStatePred,StatePred,SuccStatePred|Succs])
322		; replay_counter_example([StatePred,SuccStatePred|Succs])).
323		replay_counter_example(A) :-
324		state_space_reset,
325		replay_aux(A,_).
326		:- use_module(probsrc(b_trace_checking),[find_successor_state/4]).
327		replay_aux([],_).
328		replay_aux([P|Ps],CurId) :-
329		find_successor_state(CurId,P,SuccID,_),
330		replay_aux(Ps,SuccID).
331
332		inductively_generalize(S,Succs,Min,_K,Frames,_FramesOut,_N) :-
333		% if min < 0 and sat(F_0 & T & neg S & S')
334		% fail to report counter example
335		Min < 0,
336		in_solver_on_level(0,Frames,IS),
337		prime_predicate(S,SPrimed),
338		create_negation(S,SNegated),
339		get_transition_predicate(T),
340		conjunct_predicates([SNegated,SPrimed,T|IS],Pred),
341		solve(Pred,Result),
342		Result = solution(Solution), !,
343		throw(ic3_counter_example(Solution,Succs)).
344		inductively_generalize(S,_,Min,K,Frames,FramesOut,N) :-
345		I is max(1, Min + 1),
346		inductively_generalize_aux(I,S,K,Frames,FramesOut,N).
347		inductively_generalize_aux(I,S,K,Frames,FramesOut,N) :-
348		I =< K,
349		in_solver_on_level(I,Frames,IS),
350		prime_predicate(S,SPrimed),
351		create_negation(S,SNegated),
352		get_transition_predicate(T),
353		conjunct_predicates([SNegated,SPrimed,T|IS],Pred),
354		solve(Pred,Result), !,
355		(Result = solution(_) -> N is I - 1, generate_clause(S,N,K,Frames,FramesOut) ;
356		Result = contradiction_found(_) -> I2 is I + 1, inductively_generalize_aux(I2,S,K,Frames,FramesOut,N)).
357		inductively_generalize_aux(I,S,K,Frames,FramesOut,K) :-
358		I > K,
359		generate_clause(S,K,K,Frames,FramesOut).
360
361		generate_clause(S,I,K,Frames,FramesOut) :-
362		mic(S,I,K,Frames,FramesT,Q),
363		translate_bexpression(S,PS),
364		translate_bexpression(Q,PQ),
365		format('minimal inductive clause computation:~n~w to~n~w~n',[PS,PQ]),
366		conjunction_to_list(Q,Conjuncts),
367		maplist(create_negation,Conjuncts,NegConjuncts),
368		generate_clause_aux(1,NegConjuncts,I,FramesT,FramesOut).
369		generate_clause_aux(J,NegS,I,Frames,FramesOut) :-
370		J =< I + 1, !,
371		add_clauses_to_level(J,Frames,[NegS],FramesT),
372		J2 is J + 1,
373		generate_clause_aux(J2,NegS,I,FramesT,FramesOut).
374		generate_clause_aux(_,_,_,Frames,Frames).
375
376		mic(S,I,_K,Frames,Frames,Q) :-
377		mic_algorithm(down), !,
378		conjunction_to_list(S,Conjuncts),
379		down(Conjuncts,I,Frames,ConjunctsOut),
380		conjunct_predicates(ConjunctsOut,Q).
381		mic(S,I,K,FramesIn,FramesOut,Q) :-
382		mic_algorithm(ctgDown), !,
383		conjunction_to_list(S,Conjuncts),
384		ctgDown(Conjuncts,I,K,FramesIn,FramesOut,ConjunctsOut),
385		conjunct_predicates(ConjunctsOut,Q).
386
387		check_convergence(Frames) :-
388		avl_to_list(Frames,L),
389		check_convergence_aux(L).
390		check_convergence_aux([_-F1,K2-F2|Fs]) :-
391		% the algorithm converges if two frames hold the same set of clauses
392		F1 = frame(_,Clauses1),
393		F2 = frame(_,Clauses2),
394		% assumes ordered sets
395		(ord_symdiff(Clauses1, Clauses2, []) ; check_convergence_aux([K2-F2|Fs])).