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