1		% (c) 2015-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(kinduction,[kinduction_symbolic_model_check/1,
6		tinduction_symbolic_model_check/1]).
7
8		:- use_module(probsrc(module_information)).
9		:- module_info(group,symbolic_model_checker).
10		:- module_info(description,'A finite-state symbolic model checker based on k-Induction.').
11
12		:- use_module(library(lists), [append/2,
13		maplist/3,
14		include/3]).
15
16		:- use_module(extension('counter/counter'),[counter_init/0,
17		new_counter/1]).
18
19		:- use_module(extrasrc(before_after_predicates), [before_after_predicate_for_operation/2]).
20		:- use_module(probsrc(translate), [translate_bexpression/2]).
21		:- use_module(probsrc(bmachine),[b_get_invariant_from_machine/1,
22		b_get_machine_constants/1,
23		b_get_machine_variables/1,
24		b_specialized_invariant_for_op/2]).
25		:- use_module(probsrc(btypechecker), [prime_identifiers/2]).
26		:- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2,
27		disjunct_predicates/2,
28		safe_create_texpr/3,
29		create_negation/2]).
30		:- use_module(probsrc(preferences), [get_preference/2]).
31		:- use_module(symbolic_model_checker(predicate_handling), [prime_predicate/2,
32		deprime_state/2,
33		prime_n_times/3,
34		unprimed/1]).
35		:- use_module(symbolic_model_checker(solver_handling), [solve/2]).
36		:- use_module(symbolic_model_checker(bmc), [get_constraint/2,
37		constraint_transitions/2]).
38		:- use_module(symbolic_model_checker(ce_replay), [replay_counter_example/1]).
39
40		kinduction_symbolic_model_check(Res) :-
41		counter_init, new_counter(ic3solvercalls),
42	?	induction_symbolic_model_check(kinduction,0,Res).
43		tinduction_symbolic_model_check(Res) :-
44		counter_init, new_counter(ic3solvercalls),
45		induction_symbolic_model_check(tinduction,0,Res).
46
47		mysolve(Pred,Res) :-
48		catch(solve(Pred,Res),solver_and_provers_too_weak,Res=solver_and_provers_too_weak).
49
50		% base case: search for counter-example of length K
51		induction_symbolic_model_check(_,K,Res) :- % base case is the same for kinduction and tinduction
52		format('K = ~w~n', [K]),
53		get_constraint(K,Base),
54		(debug:debug_mode(off) -> true
55		; translate_bexpression(Base,PPBase),
56		format('Base Constraint (~w): ~w~n',[K,PPBase])
57		),
58		mysolve(Base,Result),
59		Result = solution(Sol), !,
60		Res = counterexample_found,
61		replay_counter_example(Sol).
62		% kinduction statically adds no_loop_constraint
63		induction_symbolic_model_check(kinduction,K,Res) :-
64		get_step_constraint(K,Step),
65	?	no_loop_constraint(K,NoLoop),
66		conjunct_predicates([Step,NoLoop],FullStep),
67		(debug:debug_mode(off) -> true
68		; translate_bexpression(FullStep,PPStep),
69		format('k-Induction Step Constraint (~w): ~w~n',[K,PPStep])
70		),
71		mysolve(FullStep,Result),
72		(Result = contradiction_found(_) -> Res = property_holds ;
73	?	Result = solution(_) -> K2 is K + 1, induction_symbolic_model_check(kinduction,K2,Res) ;
74		Res = solver_and_provers_too_weak).
75		% tinduction dynamically adds no_loop_constraint where two equal states have been computed
76		induction_symbolic_model_check(tinduction,K,Res) :-
77		get_step_constraint(K,Step),
78		t_induction_step(K,Step,Res).
79
80		t_induction_step(K,CurrentStep,Res) :-
81		(debug:debug_mode(off) -> true
82		; translate_bexpression(CurrentStep,PPStep),
83		format('t-Induction Current Step Constraint (~w): ~w~n',[K,PPStep])
84		),
85		mysolve(CurrentStep,Result),
86		t_induction_step_aux(Result,K,CurrentStep,Res).
87		t_induction_step_aux(contradiction_found(_),_,_,property_holds) :- !.
88		t_induction_step_aux(solution(Sol),K,CurrentStep,Res) :-
89		% if there are duplicated states, add no loop Constraint
90		add_no_loop_constraint(Sol,CurrentStep,NewStep), !,
91		t_induction_step(K,NewStep,Res).
92		t_induction_step_aux(solution(_),K,_,Res) :- !,
93		% otherwise increase K
94		K2 is K + 1,
95		(induction_symbolic_model_check(tinduction,K2,Res) ;
96		t_induction_step_aux(_,_,_,solver_and_provers_too_weak)).
97
98		add_no_loop_constraint(Solution,CurrentStep,NewStep) :-
99		add_no_loop_constraint(Solution,0,CurrentStep,NewStep).
100		% no variables left, i.e. no constraint needed
101		add_no_loop_constraint([],_,_,_) :- !, fail.
102		add_no_loop_constraint(Solution,NoOfPrimes,CurrentStep,NewStep) :-
103		include(unprimed,Solution,UnprimedVars),
104		deprime_state(Solution,DePrimedSolution),
105		DePrimedSolution \= [],
106		% if there is a variable that is not the same in the states,
107		% we do not need to add anything
108		(states_have_diff_var(UnprimedVars,DePrimedSolution)
109		-> NewNo is NoOfPrimes + 1,
110		add_no_loop_constraint(DePrimedSolution,NewNo,CurrentStep,NewStep)
111		; no_loop_constraint(1,NL),
112		prime_n_times(NoOfPrimes,NL,PrimedNL),
113		conjunct_predicates([CurrentStep,PrimedNL],NewStep)).
114
115		states_have_diff_var(Unprimed,DePrimed) :-
116		member(binding(Name,Val,_),Unprimed),
117		member(binding(Name,Val2,_),DePrimed),
118		Val \= Val2.
119
120		get_step_constraint(K,Step) :-
121		get_preference(use_po,false), !,
122		b_get_invariant_from_machine(P),
123		constraint_transitions(K,Transitions),
124		step_constraint_property(K,P,Property),
125		K2 is K + 1,
126		prime_n_times(K2,P,PPrimed),
127		create_negation(PPrimed,NegPPrimed),
128		conjunct_predicates([Transitions,Property,NegPPrimed],Step).
129		get_step_constraint(K,Step) :-
130		get_preference(use_po,true), !,
131		b_get_invariant_from_machine(P),
132		K2 is K - 1, K3 is K + 1,
133		constraint_transitions(K2,Transitions),
134		step_constraint_property(K,P,Property),
135		proof_supported_step_constraint(K3,StepConstraint),
136		% translate_bexpression(NL,PPNL),
137		% format('No Loop Constraint: ~w~n',[PPNL]),
138		conjunct_predicates([Transitions,Property,StepConstraint],Step).
139
140		proof_supported_step_constraint(K,b(truth,pred,[])) :-
141		K < 0, !.
142		proof_supported_step_constraint(N,TPred) :-
143		findall(op(OpName,Pred),(before_after_predicate_for_operation(OpName,Pred)),Ops),
144		maplist(op_to_step_constraint,Ops,SingleSteps),
145		disjunct_predicates(SingleSteps,Step),
146		N2 is N - 1,
147		prime_n_times(N2,Step,TPred).
148
149		op_to_step_constraint(op(OpName,BaPred),StepConstraint) :-
150		(b_specialized_invariant_for_op(OpName,UncheckedInvariant)
151		-> true ; b_get_invariant_from_machine(UncheckedInvariant)),
152		create_negation(UncheckedInvariant,NegUncheckedInvariant),
153		prime_predicate(NegUncheckedInvariant,PrimedNegUncheckedInvariant),
154		conjunct_predicates([BaPred,PrimedNegUncheckedInvariant],StepConstraint).
155
156		step_constraint_property(K,P,FullProperty) :-
157		step_constraint_property_aux(K,P,Conjuncts),
158		conjunct_predicates(Conjuncts,FullProperty).
159		step_constraint_property_aux(0,P,[P]) :- !.
160		step_constraint_property_aux(N,P,[P|Rest]) :-
161		prime_predicate(P,PP),
162		N2 is N - 1,
163		step_constraint_property_aux(N2,PP,Rest).
164
165		no_loop_constraint(K,NL) :-
166		b_get_machine_variables(Variables),
167		b_get_machine_constants(Constants),
168		append(Variables,Constants,VarsAndConsts),
169	?	no_loop_constraint_add_primes(K,VarsAndConsts,ListOfPrimedStates),
170	?	no_loop_constraint_aux(ListOfPrimedStates,Conjuncts),
171		conjunct_predicates(Conjuncts,NL).
172
173		no_loop_constraint_aux([],[]).
174		no_loop_constraint_aux([PState|PStates],Conjuncts) :-
175	?	no_loop_constraint_aux(PState,PStates,Conj1),
176	?	no_loop_constraint_aux(PStates,Conj2),
177		append([Conj1,Conj2],Conjuncts).
178		no_loop_constraint_aux(_State,[],[]).
179		no_loop_constraint_aux(PState1,[PState2|States],[NotEqualDisjunct|NotEquals]) :-
180		states_not_equal(PState1,PState2,NotEqual),
181		disjunct_predicates(NotEqual,NotEqualDisjunct),
182	?	no_loop_constraint_aux(PState1,States,NotEquals).
183
184		states_not_equal(P,P,[]) :- !.
185		states_not_equal([V1|V1s],[V2|V2s],[NotEqual|T]) :-
186		safe_create_texpr(not_equal(V1,V2),pred,NotEqual),
187		states_not_equal(V1s,V2s,T).
188
189		no_loop_constraint_add_primes(0,V,[V]).
190		no_loop_constraint_add_primes(1,VarsAndConsts,[PVarsAndConsts,VarsAndConsts]) :-
191		prime_identifiers(VarsAndConsts,PVarsAndConsts).
192		no_loop_constraint_add_primes(N,VAC,[VAC|VACS]) :-
193		prime_identifiers(VAC,PVAC),
194		N2 is N - 1,
195		no_loop_constraint_add_primes(N2,PVAC,VACS).