1		% (c) 2009-2017 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(units, [plugin_info/1]).
6
7		plugin_info([
8		% The name of the Plugin
9		name = 'Unit Analysis'
10		% Author is not used yet
11		,author = 'Sebastian Krings'
12		% marks the plugin as unstable or stable
13		,status = stable
14		% A list of supported file extensions together with a file description
15		% (They are not used here because the plugin is used for an already loaded
16		% file, see plugin_for_modes)
17		% ,file_extensions = [ ('Plugin demonstration spec', ['.xtl2', '.PPP']) ]
18		% The predicate that is used to load a file. The first argument is the
19		% filename, the second the file extension (like '.mch').
20		%,load_file = load_spec/1
21		% The transition skeleton initialises a transition variable in such
22		% way that only a part of all transitions match it. It is used to
23		% separate time outs and maximum number of computations for several
24		% transition classes (like different operations).
25		%,transition_skeleton = trans_skel/1
26		% The predicate that computes a transition in the state-space, its
27		% arguments are SourceState,Operation,DestinationState,ListOfOperationInfos.
28		,transition = do_transition/4
29		% The predicate that computes an initial state, its arguments are
30		% Operation,DestinationState,ListOfOperationInfos.
31		,initialisation = do_initialisation/3
32		% A predicate that returns a property for a given state, its arguments
33		% are State,Property.
34		,state_property = find_state_property/2
35		% A predicate that receives a list of expressions,predicates and
36		% predicates on transitions as input (list of codes) and returns
37		% the parsed expressions.
38		% Its arguments are ListOfExpressionStrings,ListOfPredicateStrings,
39		% ListOfTransitionPredicateStrings,ListOfExpressions,ListOfPredicates,
40		% ListOfTransitionPredicates.
41		%,parser = parse_spec/6
42		% A predicate that computes a value of an expression (returned by
43		% the parser above) in a state. Its arguments are Expression,State
44		%,compute_expression = compute/2
45		% A predicate that evaluates a predicate (returned by the parser above)
46		% in a state. Its arguments are Predicate,State
47		%,evaluate_predicate = eval/2
48		% A predicate that evaluates a predicate (returned by the parser above)
49		% for a transition. Its arguments are Predicate,Transition
50		%,evaluate_transition = evaltrans/2
51		% A predicate that checks if a state is initialised. Its argument is a State
52		%,is_initialised_state = is_init/1
53		% Pretty-print a transition, the first argument is the transition, the
54		% second -the result- is a list of codes.
55		,prettyprint_transition = pp_trans/2
56		% Pretty-print a property, the first argument is the property, the
57		% second -the result- is a list of codes.
58		,prettyprint_property = pp_prop/2
59		,prettyprint_value = pp_value/2
60		% Syntax colouring is defined by specifying a list of rules, each
61		% containing of a regular expression and a colour class
62		%,syntax_colouring = [pair('/\\*', '\\*/',syntax_comment),
63		% expression('(?=\\m)(start|trans|prop)(?=\\M)', syntax_keyword),
64		% expression('(?=\\m)(true|fail|atomic|nonvar|var|functor|op|is|ground|member|append|length)(?=\\M)|=', syntax_type),
65		% expression(':-|!|-->|;|\\.', syntax_assignment),
66		% expression('%(.*)', syntax_comment)]
67		,plugin_for_modes = [b]
68		,plugin_init=plugin_init/0
69		,new_transition_notification=notify_new_transition/4
70		,check_invariant=do_check_invariant/2
71		,preferences=preference/4
72		,output=output/3
73		,internal_representation=internal_representation/1
74		]).
75
76		:- public do_transition/4, do_initialisation/3, find_state_property/2,pp_trans/2, pp_prop/2, pp_value/2.
77		:- public plugin_init/0,notify_new_transition/4,do_check_invariant/2,preference/4,output/3,internal_representation/1.
78
79		:- use_module(library(samsort)).
80		:- use_module(library(lists)).
81
82		:- use_module(probsrc(tools)).
83		:- use_module(probsrc(specfile)).
84		:- use_module(probsrc(state_space)).
85		:- use_module(probsrc(bmachine)).
86		:- use_module(probsrc(preferences)).
87		:- use_module(probsrc(bmachine)).
88		:- use_module(probsrc(bmachine_structure)).
89		:- use_module(probsrc(pragmas)).
90		:- use_module(probsrc(coverage_tools_annotations),['$NOT_COVERED'/1]).
91		:- use_module(probsrc(error_manager)).
92
93		:- use_module(units_interpreter).
94		:- use_module(units_interpreter_helpers).
95		:- use_module(units_prettyprint).
96		:- use_module(units_tools).
97		:- use_module(units_alias).
98		:- use_module(units_domain).
99
100		:- use_module(probsrc(module_information)).
101		:- module_info(group,plugin_units).
102		:- module_info(description,'Units Plugin: This is an experimental plugin that analyses physical units stored in pragmas.').
103
104		:- dynamic iterations/1, static_result/2, units_error_context/1, tcltk_replay_sequence/1.
105
106		preference(fixpoint_on_load, true, 'Perform Static Fix-Point Check on Startup',bool).
107		preference(fixpoint_halt_on_error, true, 'Halt Fix-Point Search on Error',bool).
108		preference(fixpoint_max_iterations, 100, 'Max. Number of Iterations in Fix-Point Check', nat1).
109
110		output('Static Analysis Result', X, [tcltk,cli]) :-
111		(static_result(FixPointState,UnboundInConstraint)
112		-> pp_fixpoint_result(FixPointState,UnboundInConstraint,Output),
113		atom_codes(Output,X)
114		; X = "no result yet"),
115		'$NOT_COVERED'('GUI code not used in automatic tests').
116
117		output('Grounded Result State', X, [eclipse]) :-
118		findall(Error,get_error(incorrect_unit_definition,Error),ListOfErrors),
119		ListOfErrors \= [], !,
120		% we have something to report. skip the rest
121		reset_errors,
122		X = error(ListOfErrors).
123
124		output('Grounded Result State', state(X), [eclipse]) :-
125		(static_result(FixPointState,_UnboundInConstraint)
126		-> maplist(pp(eventb),FixPointState,X)
127		; X = []).
128
129		plugin_init :-
130		units_interpreter_helpers:retractall(cached_global_type(_,_)),
131		retractall(tcltk_replay_sequence(_)),
132		reset_tcltk_replay_sequence,
133		state_space:state_space_initialise,
134		(preference(plugin(units,fixpoint_on_load),true)
135		-> static_pre_check
136		; true),
137		(replay_tcltk_sequence ; write('Could not replay Tcl/Tk Operation Sequence!'), nl).
138
139		static_pre_check :-
140		% pre check can only be performed on an initialised machine
141		bmachine:bmachine_is_precompiled,
142		statistics(walltime,[Start|_]),
143		retractall(iterations(_)),
144		assert(iterations(0)),
145		do_initialisation(Operation, State, [initialisation]),
146		append_to_tcltk_replay_sequence(Operation),
147		to_fixpoint(State,FixPointState),
148		retractall(static_result(_,_)),
149		extract_unbound_in_constraint(FixPointState,Unbound),
150		assert(static_result(FixPointState,Unbound)),
151		insert_result_in_machine,
152		iterations(It),
153		statistics(walltime, [End|_]),
154		Time is End - Start,
155		format('Fixpoint algorithm stopped after ~w iterations and ~w milliseconds ~n', [It, Time]).
156		static_pre_check :- write('Pre-Check failed!\n'), '$NOT_COVERED'('This should not happen').
157
158		extract_unbound_in_constraint([],[]).
159		extract_unbound_in_constraint([bind(Var,Val)|T], [Var|RT]) :-
160		involved_in_constraint(Val),
161		extract_unbound_in_constraint(T,RT).
162		extract_unbound_in_constraint([bind(_Var,_Val)|T], RT) :-
163		extract_unbound_in_constraint(T,RT).
164
165		to_fixpoint(State,FixPointState) :-
166		retract(iterations(LastIt)), preference(plugin(units,fixpoint_max_iterations),MaxIt),
167		LastIt < MaxIt
168		-> CurIt is LastIt + 1, assert(iterations(CurIt)), to_fixpoint2(State,FixPointState)
169		; State=FixPointState, add_warning(units, 'Warning: Fixpoint algorithm stopped, because iteration limit was reached\n').
170
171		to_fixpoint2(concrete_constants(State),FixPointState) :-
172		!, do_transition(concrete_constants(State),Op,PossibleFixPointState,_Op2),
173		append_to_tcltk_replay_sequence(Op),
174		to_fixpoint(PossibleFixPointState,FixPointState).
175		to_fixpoint2(State,FixPointState) :-
176		findall(Operation, do_transition(State,_,_,[op(Operation)]), ListOfOperations),
177		copy_term(State,StoredState),
178		all_operations(ListOfOperations,State,PossibleFixPointState),
179		(
180		another_iteration(StoredState,PossibleFixPointState)
181		-> to_fixpoint(PossibleFixPointState,FixPointState)
182		; FixPointState = PossibleFixPointState
183		).
184
185		another_iteration(StoredState,PossibleFixPointState) :-
186		\+(halt_on_error), state_was_updated(StoredState,PossibleFixPointState).
187
188		halt_on_error :-
189		preference(plugin(units,fixpoint_halt_on_error),true),
190		state_error_exists.
191
192
193		all_operations([],State,State).
194		all_operations([Operation|T],InState,OutState) :-
195		copy_term(InState,StoredInState),
196		(do_transition(InState,OpSpec,IntermediateState,[op(Operation)])), !,
197		(state_was_updated(StoredInState,IntermediateState)
198		-> append_to_tcltk_replay_sequence(OpSpec)
199		; true),%format('Operation ~w did not update~nInState:~n~w~nIntermediateState:~n~w~n', [OpSpec,StoredInState,IntermediateState])),
200		(halt_on_error
201		-> OutState=IntermediateState
202		; all_operations(T,IntermediateState,OutState)).
203		all_operations([_Operation|T],InState,OutState) :-
204		all_operations(T,InState,OutState),
205		(halt_on_error
206		-> OutState=InState
207		; all_operations(T,InState,OutState)),
208		add_error(units_all_operations, 'operation could not be evaluated'),
209		'$NOT_COVERED'('This should not happen').
210
211		do_initialisation(OpSetup, concrete_constants(ConstantsState), [initialisation]) :-
212		bmachine:bmachine_is_precompiled,
213		b_machine_has_constants_or_properties, !,
214		set_units_error_context(operation('SETUP_CONSTANTS',ConstantsState)),
215		init_user_defined_alias,
216		b_get_machine_constants(Constants),
217		units_build_initial_state(Constants,ConstantsState),
218		b_get_properties_from_machine(Properties),
219		units_check_boolean_expression(Properties,ConstantsState,[]),
220		((get_preference(show_initialisation_arguments,true),extract_value_list(ConstantsState,Vals))
221		-> safe_univ(OpSetup,['$setup_constants'|Vals])
222		; (OpSetup = '$setup_constants')
223		).
224
225		do_initialisation(Operation,StateOut,[initialisation]) :-
226		bmachine:bmachine_is_precompiled,
227		\+ b_machine_has_constants_or_properties, !,
228		set_units_error_context(operation('$initialise_machine',StateOut)),
229		init_user_defined_alias,
230		b_get_machine_variables(Variables),
231		units_build_initial_state(Variables,VariablesState),
232		b_get_initialisation_from_machine(Init,_OType),
233		units_execute_statement(Init,[],VariablesState,StateOut,_Path),
234		specfile:create_initialisation_operation(StateOut,Operation).
235
236		do_transition(concrete_constants(StateIn),Operation,StateOut,[op(Operation)]) :-
237		bmachine:bmachine_is_precompiled, !,
238		set_units_error_context(operation('$initialise_machine',StateIn)),
239		b_get_machine_variables(Variables),
240		units_build_initial_state(Variables,VariablesState),
241		append(StateIn,VariablesState,State),
242		b_get_initialisation_from_machine(Init,_OType),
243		units_execute_statement(Init,[],State,UnsortedStateOut,_Path),
244		samsort(UnsortedStateOut,StateOut),
245		specfile:create_initialisation_operation(StateOut,Operation).
246
247		do_transition(State,OpSpec,NewState,[op(Operation)]) :-
248		bmachine:bmachine_is_precompiled,
249		b_top_level_operation(Operation),
250		set_units_error_context(operation(Operation,State)),
251		units_find_transition(Operation, State, NewState, Paras, Results),
252		(Paras \= []
253		-> OpSpec1 =.. [Operation|Paras]
254		; OpSpec1 = Operation
255		),
256		(Results \= []
257		-> OpSpec = '-->'(OpSpec1,Results)
258		; OpSpec = OpSpec1
259		),
260		execute_invariant(NewState).
261
262		notify_new_transition(FromID,TransID,DestID,_Exists) :-
263		%write(notify_new_transition(FromID,TransID,DestID,Exists)),nl,
264		state_space:transition(FromID,Action,TransID,DestID),
265		set_units_error_context(operation(Action,_)),
266		visited_expression(DestID,State),
267		check_state_add_error(DestID,State).
268
269		find_state_property(State,Property):-
270		member(bind(Var,Val),State),
271		Property = '='(Var,Val).
272
273		pp_trans(Transition,Pretty) :-
274		units_pp_trans(Transition,Pretty).
275
276		pp_prop(Property,Pretty) :-
277		units_pp_prop(Property,Pretty).
278
279		pp_value(Value,Pretty) :-
280		units_pp_value(Value,Pretty).
281
282		do_check_invariant(ID,_CurState) :-
283		%write(do_check_invariant(ID,CurState)), nl,
284		invariant_violated(ID), !.
285		do_check_invariant(ID,CurState) :-
286		set_units_error_context(checking_invariant),
287		state_corresponds_to_initialised_b_machine(CurState,CurBState),
288		execute_invariant(CurBState),
289		set_invariant_checked(ID).
290
291		execute_invariant(CurState) :-
292		set_units_error_context(checking_invariant),
293		b_get_properties_from_machine(Properties),
294		units_check_boolean_expression(Properties,CurState,[]),
295		b_get_invariant_from_machine(I),
296		units_check_boolean_expression(I,[],CurState),
297		set_units_error_context(checking_assertions),
298		b_get_static_assertions_from_machine(StaticAssertions),
299		units_check_list_of_boolean_expressions(StaticAssertions,[],CurState),
300		b_get_dynamic_assertions_from_machine(DynamicAssertions),
301		units_check_list_of_boolean_expressions(DynamicAssertions,[],CurState).
302
303		internal_representation(Rep) :-
304		full_b_machine(BMachine),
305		(static_result(_,_) -> true ; static_pre_check),
306		translate:translate_machine1(BMachine,(0,RepWithoutGlobals),(_,[])),
307		findall(alias(AliasName,Definition),
308		global_pragma(unit_alias,[AliasName|Definition]),
309		List),
310		global_pragma_output(List,OutputCodes),
311		append(OutputCodes,RepWithoutGlobals,Rep),
312		'$NOT_COVERED'('GUI code not used in automatic tests').
313
314		global_pragma_output([],[]) :- '$NOT_COVERED'('GUI code not used in automatic tests').
315		global_pragma_output([alias(AliasName,Definition)|T],Codes) :-
316		global_pragma_output(T,CodesTemp),
317		insert_spacer_and_join(Definition,DefinitionCodes),
318		ajoin(['/*@ unit_alias ', AliasName, ' ', DefinitionCodes, ' */'], CodePragma),
319		safe_atom_codes(CodePragma,CodePragmaCodes),
320		append(CodePragmaCodes,CodesTemp,Codes),
321		'$NOT_COVERED'('GUI code not used in automatic tests').
322
323		insert_result_in_machine :-
324		write('Pre-Check finished. Inserting results in machine'), nl,
325		static_result(Result,_),
326		full_b_machine(BMachine),
327		get_section(abstract_variables,BMachine,AbsVarsContent),
328		expand_variables(AbsVarsContent,ExpandedAbsVarsContent,Result),
329		write_section(abstract_variables,ExpandedAbsVarsContent,BMachine,BMachine2),
330		get_section(concrete_variables,BMachine2,ConcVarsContent),
331		expand_variables(ConcVarsContent,ExpandedConcVarsContent,Result),
332		write_section(concrete_variables,ExpandedConcVarsContent,BMachine2,BMachine3),
333		get_section(abstract_constants,BMachine3,AbsConstContent),
334		expand_variables(AbsConstContent,ExpandedAbsConstContent,Result),
335		write_section(abstract_constants,ExpandedAbsConstContent,BMachine3,BMachine4),
336		get_section(concrete_constants,BMachine4,ConcConstContent),
337		expand_variables(ConcConstContent,ExpandedConcConstContent,Result),
338		write_section(concrete_constants,ExpandedConcConstContent,BMachine4,BMachine5),
339		retractall(bmachine:machine(_,_)),
340		bmachine:assert_main_machine(BMachine5).
341
342		expand_variables([],[],_Result).
343		expand_variables([b(identifier(X),Type,Infos)|T],[b(identifier(X),Type,Infos2)|T2],Result) :-
344		member(bind(X,Val),Result), !,
345		(
346		member(unit(ExplicitUnit),Infos) -> atom_codes(Atom,ExplicitUnit), ajoin(['"',Atom,'"'],Output),
347		Infos2 = [output_pragma('unit',Output)|Infos] ;
348		pp(classic,Val,PP) -> ajoin(['"',PP,'"'],AtomPP),
349		Infos2 = [output_pragma('inferred_unit',AtomPP)|Infos] ;
350		otherwise -> Infos2 = Infos
351		),
352		expand_variables(T,T2,Result).
353		expand_variables([b(identifier(X),Type,Infos)|T],[b(identifier(X),Type,Infos)|T2],Result) :-
354		format('Warning: identifier ~w not in result\n', [X]),
355		expand_variables(T,T2,Result),
356		'$NOT_COVERED'('This should not happen.').
357
358		set_units_error_context(Context) :-
359		retractall(units_error_context(_)),
360		assert(units_error_context(Context)).