1		% (c) 2009-2013 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(absint, [plugin_info/1]).
6
7		plugin_info([
8		name = 'Abstract Interpretation'
9		,author = 'René Bartelmus, Sebastian Krings'
10		,status = stable
11		,transition = do_transition/4
12		,initialisation = do_initialisation/3
13		,state_property = find_state_property/2
14		,prettyprint_transition = pp_trans/2
15		,prettyprint_property = pp_prop/2
16		,prettyprint_value = pp_value/2
17		,plugin_for_modes = [b]
18		,plugin_init=plugin_init/0
19		,new_transition_notification=notify_new_transition/4
20		,check_invariant=do_check_invariant/2
21		,preferences=preference/4
22		%,output=output/3
23		%,internal_representation=internal_representation/1
24		]).
25
26		:- public do_transition/4, do_initialisation/3, find_state_property/2,pp_trans/2, pp_prop/2, pp_value/2.
27		:- public plugin_init/0,notify_new_transition/4,do_check_invariant/2,preference/4.
28
29		:- use_module(probsrc(module_information)).
30		:- module_info(group,plugin_absint).
31		:- module_info(description,'This is an experimental plugin that applies abstract interpretation on B models.').
32		:- module_info(revision,'$Rev$').
33		:- module_info(lastchanged,'$LastChangedDate$').
34
35		:- use_module(probsrc(tools)).
36		:- use_module(probsrc(state_space)).
37		:- use_module(probsrc(specfile)).
38		:- use_module(probsrc(bmachine)).
39		:- use_module(probsrc(preferences),[get_preference/2]).
40
41		:- use_module(b_abstract_interpreter).
42		:- use_module(b_abstract_interpreter_helpers).
43
44		preference(abstract_domain_module, 'interval', 'Module name with abstract domain and operations',string).
45
46		plugin_init :-
47		state_space:state_space_initialise.
48
49		do_initialisation(OpSetup, concrete_constants(ConstantsStateOut), [initialisation]) :-
50		bmachine:bmachine_is_precompiled,
51		b_machine_has_constants_or_properties, !,
52		b_get_machine_constants(Constants),
53		absint_build_initial_state(Constants,ConstantsState),
54		b_get_properties_from_machine(Properties),
55		absint_check_boolean_expression(Properties,[],[],ConstantsState,ConstantsStateOut,true),
56		((get_preference(show_initialisation_arguments,true),
57		extract_value_list(ConstantsStateOut,Vals))
58		-> safe_univ(OpSetup,['$setup_constants'|Vals])
59		; (OpSetup = '$setup_constants')
60		).
61
62		do_initialisation(Operation,StateOut,[initialisation]) :-
63		bmachine:bmachine_is_precompiled,
64		\+ b_machine_has_constants_or_properties, !,
65		b_get_machine_variables(Variables),
66		absint_build_initial_state(Variables,VariablesState),
67		b_get_initialisation_from_machine(Init,_OType),
68		absint_execute_statement(Init,[],VariablesState,StateOut,_Path),
69		specfile:create_initialisation_operation(StateOut,Operation).
70
71		do_transition(concrete_constants(StateIn),Operation,StateOut,[op(Operation)]) :-
72		bmachine:bmachine_is_precompiled, !,
73		b_get_machine_variables(Variables),
74		absint_build_initial_state(Variables,VariablesState),
75		append(StateIn,VariablesState,State),
76		b_get_initialisation_from_machine(Init,_OType),
77		absint_execute_statement(Init,[],State,UnsortedStateOut,_Path),
78		sort(UnsortedStateOut,StateOut),
79		specfile:create_initialisation_operation(StateOut,Operation).
80
81		do_transition(State,OpSpec,NewState,[op(Operation)]) :-
82		bmachine:bmachine_is_precompiled,
83		b_top_level_operation(Operation),
84		find_abstract_transition(Operation, State, NewState, Paras, Results),
85		( Paras \= [] ->
86		OpSpec1 =.. [Operation|Paras]
87		; OpSpec1 = Operation
88		),
89		(Results \= [] ->
90		OpSpec = '-->'(OpSpec1,Results)
91		; OpSpec = OpSpec1
92		).
93
94		notify_new_transition(_FromID,_TransID,_DestID,_Exists).
95
96		find_state_property(State,Property):-
97		member(bind(Var,Val),State),
98		Property = '='(Var,Val).
99
100		pp_trans(Transition,Pretty) :-
101		ajoin([Transition], Pretty).
102
103		pp_prop(Property,Pretty) :-
104		ajoin([Property], Pretty).
105
106		pp_value(Value,Pretty) :-
107		ajoin([Value], Pretty).
108
109		do_check_invariant(ID,_CurState) :-
110		invariant_violated(ID), !.
111		do_check_invariant(ID,CurState) :-
112		state_corresponds_to_initialised_b_machine(CurState,CurBState),
113		b_get_invariant_from_machine(I),
114		absint_check_boolean_expression(I,[],[],CurBState,_UpdatedCurState,false),
115		set_invariant_violated(ID).
116
117		extract_value_list([],[]).
118		extract_value_list([bind(_,X)|T],[X|ET]) :- extract_value_list(T,ET).