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