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