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(b_abstract_interpreter_helpers, [
6 assign_vars/6,
7 assign_var/6,
8 state_store_list/3,
9 state_store/3,
10 assign_vals_to_vars/3,
11 state_lookup/4,
12 absint_build_initial_state/2,
13 absint_set_up_localstate/3,
14 absint_set_up_undefined_localstate/3,
15 absint_get_results/4,
16 unary_operator/3, binary_operator/4, nary_operator/3,
17 execute_statements_in_parallel/5,
18 execute_else_list/4,
19 test_binary_update/6, test_unary_update/4
20 ]).
21
22 :- use_module(probsrc(module_information)).
23 :- module_info(group,plugin_absint).
24 :- module_info(description,'Abstract Interpreter: Helper Predicates').
25 :- module_info(revision,'$Rev$').
26 :- module_info(lastchanged,'$LastChangedDate$').
27
28 :- use_module(library(samsort)).
29 :- use_module(library(lists)).
30
31 :- use_module(probsrc(b_global_sets)).
32 :- use_module(probsrc(bsyntaxtree)).
33 :- use_module(probsrc(error_manager)).
34
35 :- use_module(b_abstract_mappings).
36 :- use_module(b_abstract_interpreter).
37
38 unary_operator(UnExpr, UOP, Arg1) :-
39 functor(UnExpr, UOP, 1),
40 arg(1, UnExpr, Arg1),
41 \+ is_list(Arg1).
42
43 binary_operator(BinExpr, BOP, Arg1, Arg2) :-
44 functor(BinExpr, BOP, 2),
45 arg(1, BinExpr, Arg1),
46 arg(2, BinExpr, Arg2).
47
48 nary_operator(UnExpr, UOP, Arg1) :-
49 functor(UnExpr, UOP, 1),
50 arg(1, UnExpr, Arg1),
51 is_list(Arg1).
52
53 test_binary_update(Arg1, Arg2, NewVal1, NewVal2, StateIn, StateOut) :-
54 test_unary_update(Arg1,NewVal1,StateIn,TempStateOut),
55 test_unary_update(Arg2,NewVal2,TempStateOut,StateOut).
56
57 test_unary_update(Arg,Val,StateIn,StateOut) :-
58 Arg = identifier(ID) -> state_store(bind(ID,Val),StateIn,StateOut) ;
59 otherwise -> StateIn = StateOut.
60
61 execute_statements_in_parallel([],_LocalState,_StateIn,[],[]).
62 execute_statements_in_parallel([Stmt|TS],LocalState,InState,UpdatesOut,[Path1|TPath]) :-
63 absint_execute_statement(Stmt,LocalState,InState,Updates1,Path1),
64 execute_statements_in_parallel(TS,LocalState,InState,Updates2,TPath),
65 append(Updates1,Updates2,UpdatesOut).
66
67 execute_else_list([],_,_State,[]).
68 execute_else_list([TExpr|Rest],LocalState,InState,OutState) :-
69 get_texpr_expr(TExpr,if_elsif(Test,Body)),
70 absint_check_boolean_expression(Test,LocalState,NewLocalState,InState,NewInState,TestResult),
71 (TestResult = true
72 -> absint_execute_statement(Body,NewLocalState,NewInState,OutState,_Path)
73 ; execute_else_list(Rest,NewLocalState,NewInState,OutState)).
74
75 absint_get_results([],OutState,[],OutState).
76 absint_get_results([R|Results],OutState,[NRV|ResultValues],NewOutState) :-
77 def_get_texpr_id(R,ResultId),
78 selectchk(bind(ResultId,NRV),OutState,OutState2),
79 absint_get_results(Results,OutState2,ResultValues,NewOutState).
80
81 absint_set_up_localstate(Parameters,ParaValues,LocalState) :-
82 absint_build_initial_state(Parameters,LocalState),
83 findall(Val, member(bind(_Id,Val),LocalState), ParaValues).
84
85 absint_set_up_undefined_localstate([],S,S).
86 absint_set_up_undefined_localstate([Var|T],InS,[bind(Id,_)|OutS]) :-
87 def_get_texpr_id(Var,Id),
88 absint_set_up_undefined_localstate(T,InS,OutS).
89
90 % build initial state: call alpha on concrete values
91 absint_build_initial_state(BTypeList,InitialState) :-
92 absint_build_initial_state2(BTypeList, UnsortedInitialState),
93 samsort(UnsortedInitialState,InitialState).
94 absint_build_initial_state2([],[]) :- !.
95 absint_build_initial_state2([b(identifier(Name),Type,Args)|T],[bind(Name,InternalType)|StateT]) :-
96 call_alpha(Type,Type,Args,InternalType), !,
97 absint_build_initial_state(T,StateT).
98 % state store and state lookup
99 state_store_list([], State, State).
100 state_store_list([H|T], StateIn, StateOut) :-
101 state_store(H, StateIn, StateIn1),
102 state_store_list(T, StateIn1, StateOut).
103
104 state_store(bind(Key,_), [], []) :-
105 !, add_error(absint_state_store, 'Variable could not be found in state: ', Key).
106 state_store(bind(Key,Value), [bind(Key,_Value)|Rest], [bind(Key,Value2)|Rest]) :-
107 !, Value2=Value.
108 state_store(Pair, [Pair2|Rest], [Pair2|StateOut]) :-
109 Pair \= Pair2,
110 state_store(Pair, Rest, StateOut).
111
112 state_lookup(Id,S1,S2,Val) :-
113 statistics(walltime,_),
114 statistics(runtime,_),
115 state_lookup2(Id,S1,S2,Val),
116 statistics(walltime,[_,Duration]),
117 statistics(runtime,[_,RDuration]),
118 (Duration < 20 -> true ; length(S1,LS1), length(S2,LS2),
119 format('Warning: lookup of ~w took ~w (~w) ms (Val=~w,LS1=~w,LS2=~w)~n', [Id, Duration,RDuration,Val,LS1,LS2])).
120 state_lookup2(Id,LocalState,GlobalState,Value) :-
121 (member(bind(Id,Val),LocalState) -> Value=Val
122 ; member(bind(Id,Val),GlobalState) -> Value=Val
123 ; state_lookup_global(Id,Value)).
124 state_lookup_global(Id,Val) :-
125 lookup_global_constant(Id,fd(_,Set)), !,
126 call_alpha(global(Set),global(Set),[],Val).
127 state_lookup_global(Id,Val) :-
128 b_global_set(Id), !,
129 call_alpha(set(global(Id)),set(global(Id)),[],Val).
130 state_lookup_global(Id,_Val) :- add_error_fail(lookup_value, 'Variable could not be found: ', Id).
131
132 assign_vars([], [], _LocalState, _StateIn, [], []).
133 assign_vars([TVarH|TVarT], [TValH|TValT], LocalState, StateIn, [NewVarH|NewVarT], [NewValH|NewValT]) :-
134 get_texpr_expr(TVarH,VarH),
135 assign_var(VarH, TValH, LocalState,StateIn, NewVarH, NewValH),
136 assign_vars(TVarT, TValT, LocalState,StateIn, NewVarT, NewValT).
137
138 assign_var(identifier(Id),Value,_LS,_S,Id,Value) :- !.
139
140 assign_vals_to_vars([], [], []).
141 assign_vals_to_vars([H1|T1], [H2|T2], [bind(H1,H2)|T]) :-
142 assign_vals_to_vars(T1, T2, T).