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