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])). |