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(units_interpreter_helpers, [units_build_initial_state/2,
6		assign_vars/6,
7		assign_var/6,
8		state_store_list/3,
9		state_store/3,
10		merge_non_overriding_states/3,
11		assign_vals_to_vars/3,
12		merge_expression_list/2,
13		execute_statements_in_parallel/5,
14		execute_else_list/4,
15		execute_select_list/4,
16		execute_cases_list/5,
17		execute_choice_list/4,
18		execute_sequence/6,
19		execute_while/5,
20		execute_eventb_list/5,
21		units_lookup_value/4,
22		units_set_up_localstate/3,
23		units_set_up_undefined_localstate/3,
24		b_type_to_internal_type/3
25		]).
26
27		:- use_module(library(codesio)).
28		:- use_module(library(lists)).
29		:- use_module(library(samsort)).
30
31		:- use_module(probsrc(bmachine)).
32		:- use_module(probsrc(error_manager)).
33		:- use_module(probsrc(bsyntaxtree)).
34		:- use_module(probsrc(b_global_sets)).
35
36		:- use_module(units_interpreter).
37		:- use_module(units_domain).
38		:- use_module(units_alias).
39		:- use_module(unit_parser).
40
41		:- use_module(probsrc(module_information)).
42		:- module_info(group,plugin_units).
43		:- module_info(description,'Units Plugin: Helper Predicates').
44
45		:- dynamic cached_global_type/2.
46
47		% value lookup: Id to search for, local state, global state and return variable
48		units_lookup_value(Id,S1,S2,Val) :-
49		statistics(walltime,_),
50		statistics(runtime,_),
51		units_lookup_value2(Id,S1,S2,Val),
52		statistics(walltime,[_,Duration]),
53		statistics(runtime,[_,RDuration]),
54		(Duration < 20 -> true ; length(S1,LS1), length(S2,LS2),
55		format('Warning: lookup of ~w took ~w (~w) ms (Val=~w,LS1=~w,LS2=~w)~n', [Id, Duration,RDuration,Val,LS1,LS2])).
56		units_lookup_value2(Id,LocalState,GlobalState,Value) :-
57		(member(bind(Id,Val),LocalState) -> Value=Val
58		; member(bind(Id,Val),GlobalState) -> Value=Val
59		; units_lookup_global_value(Id,Value)).
60
61		units_lookup_global_value(Id,Val) :-
62		lookup_global_constant(Id,fd(_,Set)), !,
63		b_type_to_internal_type(global(Set),[],Val).
64		units_lookup_global_value(Id,Val) :-
65		b_global_set(Id), !,
66		b_type_to_internal_type(set(global(Id)), [], Val).
67		%units_lookup_global_value(Id,Val) :-
68		% b_get_machine_all_constants(Csts),
69		% member(b(identifier(Id),Type,Infos), Csts), !,
70		% b_type_to_internal_type(Type,Infos,Val).
71		units_lookup_global_value(Id,_Val) :- add_error_fail(lookup_value, 'Variable could not be found: ', Id).
72
73		execute_statements_in_parallel([],_Local,State, State, []).
74		execute_statements_in_parallel([Stmt|TS],Local,StateIn, StateOut, [PathH|PathT]) :-
75		units_execute_statement(Stmt, Local,StateIn, StateOut1, PathH),
76		execute_statements_in_parallel(TS, Local,StateIn, StateOut2, PathT),
77		merge_non_overriding_states(StateOut1,StateIn,TempStateOut),
78		merge_non_overriding_states(StateOut2,TempStateOut,StateOut).
79
80		execute_else_list([],_,_State,[]).
81		execute_else_list([TExpr|Rest],LocalState,InState,OutState) :-
82		get_texpr_expr(TExpr,if_elsif(Test,Body)),
83		units_check_boolean_expression(Test,LocalState,InState),
84		execute_else_list2(Body,Rest,LocalState,InState,OutState).
85		execute_else_list2(Body,Rest,LocalState,InState,OutState) :-
86		units_execute_statement(Body,LocalState,InState,OutState1,_Path),
87		execute_else_list(Rest,LocalState,InState,OutState2),
88		merge_non_overriding_states(OutState1,OutState2,OutState).
89
90		execute_select_list([],_,_State,[]).
91		execute_select_list([TExpr|Rest],LocalState,InState,OutState) :-
92		get_texpr_expr(TExpr,select_when(Test,Body)),
93		units_check_boolean_expression(Test,LocalState,InState),
94		execute_select_list2(Body,Rest,LocalState,InState,OutState).
95		execute_select_list2(Body,Rest,LocalState,InState,OutState) :-
96		units_execute_statement(Body,LocalState,InState,OutState1,_Path),
97		execute_select_list(Rest,LocalState,InState,OutState2),
98		merge_non_overriding_states(OutState1,OutState2,OutState).
99
100		execute_cases_list(_ToCompare,[],_,_State,[]).
101		execute_cases_list(ToCompare,[TExpr|Rest],LocalState,InState,OutState) :-
102		get_texpr_expr(TExpr,case_or(Expr,Subst)),
103		units_compute_expressions(Expr,LocalState,InState,Results),
104		merge_expression_list(Results,MergedResult),
105		same_units(ToCompare,MergedResult),
106		units_execute_statement(Subst,LocalState,InState,OutState1,_Path),
107		execute_cases_list(ToCompare,Rest,LocalState,InState,OutState2),
108		merge_non_overriding_states(OutState1,OutState2,OutState).
109
110		execute_choice_list([],_,_State,[]).
111		execute_choice_list([Stmt|Rest],LocalState,InState,OutState) :-
112		units_execute_statement(Stmt,LocalState,InState,OutState1,_Path),
113		execute_choice_list(Rest,LocalState,InState,OutState2),
114		merge_non_overriding_states(OutState1,OutState2,OutState).
115
116		execute_sequence(First,UnwrappedRest,LocalState,InState,OutUpdates,Path) :-
117		Path = sequence(Path1,RestPath),
118		units_execute_statement(First,LocalState,InState,LHSUpdates,Path1),
119		merge_non_overriding_states(InState,LHSUpdates,IntermediateState),
120		execute_statement_when_state_set(UnwrappedRest,LocalState,IntermediateState,LHSUpdates,OutUpdates,RestPath).
121
122		execute_eventb_list([], _LocalState, InState, InState, []).
123		execute_eventb_list([Stmt|Stmts],LocalState,InState,OutState, [Path1|Paths]) :-
124		units_execute_statement(Stmt,LocalState,InState,LHSUpdates,Path1),
125		merge_non_overriding_states(InState,LHSUpdates,IntermediateState),
126		execute_eventb_list(Stmts,LocalState,IntermediateState,OutState,Paths).
127
128		execute_while(Condition,Statement,LocalState,InState,OutState) :-
129		units_check_boolean_expression(Condition,LocalState,InState),
130		units_execute_statement(Statement,LocalState,InState,PossibleOutState,_Path),
131		( PossibleOutState = InState ->
132		OutState = PossibleOutState
133		; execute_while(Condition,Statement,LocalState,PossibleOutState,OutState)
134		).
135
136		execute_statement_when_state_set(Stmt,LS,State,UpdatesSofar,Res,Path) :-
137		units_execute_statement2(Stmt,[],LS,State,StmtUpdates,Path),
138		merge_non_overriding_states(UpdatesSofar,StmtUpdates,Res).
139
140		merge_expression_list([U], U).
141		merge_expression_list([U1|T],U) :-
142		merge_expression_list(T,UList),
143		lub(U1,UList,U).
144
145		merge_non_overriding_states([],State,State).
146		merge_non_overriding_states([bind(Key,Val)|T], State, [bind(Key,Result)|OutTail]) :-
147		(
148		selectchk(bind(Key,Val2),State,SOut)
149		-> lub(Val,Val2,Result)
150		; Result=Val, SOut = State
151		),
152		merge_non_overriding_states(T,SOut,OutTail).
153
154		units_set_up_localstate(Parameters,ParaValues,LocalState) :-
155		units_build_initial_state(Parameters,TypedLocalState),
156		maplist(bind_values,TypedLocalState,ParaValues,LocalState).
157
158		bind_values(bind(Id,Val),Val2,bind(Id,Val3)) :-
159		lub(Val,Val2,Val3).
160
161		units_build_initial_state(BTypeList,InitialState) :-
162		units_build_initial_state2(BTypeList, UnsortedInitialState),
163		samsort(UnsortedInitialState,InitialState).
164		units_build_initial_state2([],[]) :- !.
165		units_build_initial_state2([b(identifier(Name),Type,Args)|T],[bind(Name,InternalType)|StateT]) :-
166		%length(T,Len), format('Still ~w vars to go to build initial state~n', [Len]),
167		b_type_to_internal_type(Type,Args,InternalType), !,
168		units_build_initial_state(T,StateT).
169
170		units_set_up_undefined_localstate([],S,S).
171		units_set_up_undefined_localstate([Var|T],InS,[bind(Id,_)|OutS]) :-
172		def_get_texpr_id(Var,Id),
173		units_set_up_undefined_localstate(T,InS,OutS).
174
175		get_unit_from_pragma(Args,Res) :-
176		member(unit(Unit),Args), !,
177		unit_args_to_list(Unit, Res).
178		get_unit_from_pragma(Args,[[0,AtomUnit,1]]) :-
179		member(new_unit(Unit),Args), !,
180		atom_codes(AtomUnit,Unit).
181		get_unit_from_pragma(_,_).
182
183		b_type_to_internal_type(boolean, Args, boolean(Res)) :-
184		!, get_unit_from_pragma(Args,Res).
185		b_type_to_internal_type(string, Args, string(Res)) :-
186		!, get_unit_from_pragma(Args,Res).
187		b_type_to_internal_type(integer, Args, integer(Res)) :-
188		!, get_unit_from_pragma(Args,Res).
189		b_type_to_internal_type(global(X), _Args, Result) :-
190		cached_global_type(X,Res), !, Result=global(Res,X).
191		b_type_to_internal_type(global(X), Args, global(Res,X)) :-
192		!, full_b_machine(machine(_Name,Parts)),
193		member(deferred_sets/DeferredSetsList, Parts),
194		member(enumerated_sets/EnumeratedSetsList, Parts),
195		append(DeferredSetsList,EnumeratedSetsList, AllGlobalSetsList),
196		find_global_unit_in_list(X,AllGlobalSetsList, UnitFromSet),
197		get_unit_from_pragma(Args,UnitFromPragma),
198		(UnitFromSet = UnitFromPragma -> Res = UnitFromPragma ; fail),
199		assert(cached_global_type(X,Res)).
200		b_type_to_internal_type(set(X), Args, set(Res)) :-
201		!, b_type_to_internal_type(X,Args,Res).
202		b_type_to_internal_type(seq(X), Args, set(couple(integer(_),Res))) :-
203		!, b_type_to_internal_type(X,Args,Res).
204		b_type_to_internal_type(couple(X,Y),Args,couple(XRes,YRes)) :-
205		!, b_type_to_internal_type(X,Args,XRes),
206		b_type_to_internal_type(Y,Args,YRes).
207		b_type_to_internal_type(record(Fields), Args, rec(UnitFields)) :-
208		!, maplist(b_type_to_internal_type_maplist(Args),Fields,UnitFields).
209		b_type_to_internal_type(field(Name,Type),Args,field(Name,UType)) :-
210		!, b_type_to_internal_type(Type,Args,UType).
211		b_type_to_internal_type(X, _Args, _Res) :- !,
212		add_error_fail(b_type_to_internal_type, 'Can not construct internal type for: ', [X]).
213
214		b_type_to_internal_type_maplist(Args,A,B) :-
215		b_type_to_internal_type(A,Args,B).
216
217		find_global_unit_in_list(_Global,[],_Res).
218		find_global_unit_in_list(Global,[H|_T],Res) :-
219		H = b(identifier(Global),set(global(Global)),Infos), !,
220		(member(unit(Unit),Infos) -> unit_args_to_list(Unit, Res) ; true).
221		find_global_unit_in_list(Global,[_H|T],Res) :-
222		find_global_unit_in_list(Global,T,Res).
223
224		assign_vars([], [], _LocalState, _StateIn, [], []).
225		assign_vars([TVarH|TVarT], [TValH|TValT], LocalState, StateIn, [NewVarH|NewVarT], [NewValH|NewValT]) :-
226		get_texpr_expr(TVarH,VarH),
227		assign_var(VarH, TValH, LocalState,StateIn, NewVarH, NewValH),
228		assign_vars(TVarT, TValT, LocalState,StateIn, NewVarT, NewValT).
229
230		assign_var(identifier(Id),Value,_LS,_S,Id,Value) :- !.
231		% dead code?
232		%assign_var(function(Fun,Arg),Value,LocalState,InState,Id,FullValue) :-
233		% !, units_compute_expression(Fun,LocalState,InState,FunVal),
234		% units_compute_expression(Arg,LocalState,InState,ArgVal),
235		% lub(FunVal,set(couple(ArgVal,Value)),NewFun),
236		% get_texpr_expr(Fun,Lhs),
237		% assign_var(Lhs,NewFun,LocalState,InState,Id,FullValue).
238
239		state_store_list([], State, State).
240		state_store_list([H|T], StateIn, StateOut) :-
241		state_store(H, StateIn, StateIn1),
242		state_store_list(T, StateIn1, StateOut).
243
244		state_store(bind(Key,Value), [], []) :-
245		!, add_error_fail(units_state_store, 'Variable could not be found in state: ', [Key,Value]).
246		state_store(bind(Key,Value), [bind(Key,X)|Rest], [bind(Key,Value2)|Rest]) :- var(X), !, Value2 = Value.
247		state_store(bind(Key,integer(Value1)), [bind(Key,integer(Value2))|Rest], [bind(Key,integer(Value3))|Rest]) :- !, lub(Value1,Value2,Value3).
248		state_store(bind(Key,set(Value1)), [bind(Key,set(Value2))|Rest], [bind(Key,set(Value3))|Rest]) :- !, lub(Value1,Value2,Value3).
249		state_store(bind(Key,couple(Value11,Value12)), [bind(Key,couple(Value21,Value22))|Rest],
250		[bind(Key,couple(Value31,Value32))|Rest]) :- !, lub(Value11,Value21,Value31), lub(Value12,Value22,Value32).
251		state_store(bind(Key,global(Value1,Global)), [bind(Key,global(Value2,Global))|Rest],
252		[bind(Key,global(Value3,Global))|Rest]) :- !, lub(Value1,Value2,Value3).
253		state_store(bind(Key,rec(Fields1)), [bind(Key,rec(Fields2))|Rest], [bind(Key,rec(Fields3))|Rest]) :- !,
254		maplist(lub,Fields1,Fields2,Fields3).
255		state_store(bind(Key,boolean(_)), [bind(Key,boolean(_))|Rest], [bind(Key,boolean(_))|Rest]) :- !.
256		state_store(bind(Key,string(_)), [bind(Key,string(_))|Rest], [bind(Key,string(_))|Rest]) :- !.
257		state_store(Pair, [Pair2|Rest], [Pair2|StateOut]) :-
258		Pair \= Pair2, !,
259		state_store(Pair, Rest, StateOut).
260
261		assign_vals_to_vars([], [], []).
262		assign_vals_to_vars([H1|T1], [H2|T2], [bind(H1,H2)|T]) :-
263		assign_vals_to_vars(T1, T2, T).