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_mappings,[
6		call_unary_test/4,
7		call_binary_test/6,
8
9		call_alpha/4,
10
11		call_unary_expression/3,
12		call_binary_expression/4,
13		call_nary_expression/3,
14
15		glb/3,
16		lub/3
17		]).
18
19		:- use_module(probsrc(error_manager)).
20		:- use_module(probsrc(tools)).
21
22		:- use_module(library(file_systems)).
23		:- use_module(probsrc(module_information)).
24		:- module_info(group,plugin_absint).
25		:- module_info(description,'Experimental abstract interpretation plugin: this module maps regular operators to the ones in the selected abstract domain.').
26		:- module_info(revision,'$Rev$').
27		:- module_info(lastchanged,'$LastChangedDate$').
28
29		:- dynamic domain/2.
30
31		% ---------
32		% loading of the abstract domain modules at compiletime, lookup in directory
33		% ---------
34
35		load_compiletime_domains :-
36		findall(Module,
37		(directory_member_of_directory('domains',Dir,Fullname),
38		atom_concat(Dir,'.pl',PrologFilename),
39		file_member_of_directory(Fullname,PrologFilename,_),
40		ajoin([Dir,'/',PrologFilename], Modulename),
41		Module = abstract_domains(Modulename)),
42		Domains),
43		load_domains2(Domains).
44
45		load_domains2([]).
46		load_domains2([Module|Prest]) :-
47		load_domain(Module,Id),
48		(nonvar(Id) -> assert(domain(Id,Module)); true),
49		load_domains2(Prest).
50
51		load_domain(Module,Id) :-
52		catch( ( load_domain2(Module,Id) ->
53		ajoin(['Loaded domain ', Id], Msg),
54		print_message(informational, Msg)
55		; otherwise ->
56		ajoin(['Loading of module ', Id, ' failed: '], Msg),
57		print_message(error, Msg)),
58		E,
59		( ajoin(['Loading of module ', Id, ' raised an exception: ', E], Msg),
60		print_message(error, Msg))).
61
62		load_domain2(Module,Id) :-
63		use_module(IdVar,Module,[]),
64		IdVar = Id,
65		( domain(Id,_) ->
66		ajoin(['Domain ID ',Id,'used twice'],Msg),
67		print_message(error,Msg),
68		fail
69		; otherwise ->
70		true).
71
72
73		:- load_compiletime_domains.
74
75		% ----------------
76		% Call GLB and LUB
77		% ----------------
78		lub(X, Y, Z) :-
79		preferences:preference(plugin(absint,abstract_domain_module), DomainModule),
80		current_predicate(DomainModule:lub/1),
81		DomainModule:lub(LUB),
82		call(DomainModule:LUB, X, Y, Z),
83		!.
84		lub(_, _, _) :-
85		add_error(lub, 'Least upper bound is not defined or failed. Define a lub/3 predicate in the abstract domain file'), fail.
86
87		glb(X, Y, Z) :-
88		preferences:preference(plugin(absint,abstract_domain_module), DomainModule),
89		current_predicate(DomainModule:glb/1),
90		DomainModule:glb(GLB),
91		call(DomainModule:GLB, X, Y, Z),
92		!.
93		glb(_, _, _) :-
94		add_error(glb, 'Greatest lower bound is not defined or failed. Define a glb/3 predicate in the abstract domain file'), fail.
95
96		% -----------------
97		% Call Alpha
98		% -----------------
99		call_alpha(Concrete,Type,Infos,Abstract) :-
100		preferences:preference(plugin(absint,abstract_domain_module), DomainModule),
101		DomainModule:map_alpha(alpha, CallAlpha),
102		call(DomainModule:CallAlpha,Concrete,Type,Infos,Abstract), !.
103		call_alpha(C,T,I,top) :-
104		add_error(call_alpha, 'no mapping for alpha or no result defined (using top instead) for ', [C,T,I]).
105
106		% ----------------
107		% Call predicates
108		% ----------------
109		call_unary_test(UOP, Arg1, NewArg1, Test) :-
110		preferences:preference(plugin(absint,abstract_domain_module), DomainModule),
111		(DomainModule:map_unary_test_operator(UOP, CallUOP) -> true
112		; Expr =.. [UOP, Arg1],add_error(call_unary_test, 'no mapping for operator or no result defined (using true instead) for ', Expr)),
113		!,
114		(call(DomainModule:CallUOP, Arg1, NewArg1, Test1) -> Test = Test1
115		; Test = false, Arg1 = NewArg1).
116
117		call_binary_test(BOP, Arg1, Arg2, NewArg1, NewArg2, Test) :-
118		preferences:preference(plugin(absint,abstract_domain_module), DomainModule),
119		(DomainModule:map_binary_test_operator(BOP, CallBOP) -> true
120		; Expr =.. [BOP, Arg1, Arg2],add_error(call_binary_test, 'no mapping for operator or no result defined (using true instead) for ', Expr)),
121		!,
122		(call(DomainModule:CallBOP, Arg1, Arg2, NewArg1, NewArg2, Test1) -> Test = Test1
123		; Test = false, Arg1 = NewArg1, Arg2 = NewArg2).
124
125		% -----------------
126		% Call expressions
127		% -----------------
128		call_unary_expression(UOP, Arg1, Result) :-
129		preferences:preference(plugin(absint,abstract_domain_module), DomainModule),
130		DomainModule:map_unary_operator(UOP, CallUOP),
131		!,
132		call(DomainModule:CallUOP, Arg1, Result).
133		call_unary_expression(UOP, Arg1, top) :-
134		Expr =.. [UOP, Arg1],
135		add_error_fail(call_unary_expression, 'no mapping for operator or no result defined for ', Expr).
136
137		call_binary_expression(BOP, Arg1, Arg2, Result) :-
138		preferences:preference(plugin(absint,abstract_domain_module), DomainModule),
139		DomainModule:map_binary_operator(BOP, CallBOP),
140		!,
141		call(DomainModule:CallBOP, Arg1, Arg2, Result).
142		call_binary_expression(BOP, Arg1, Arg2, top_) :-
143		Expr =.. [BOP, Arg1, Arg2],
144		add_error_fail(call_binary_expression, 'no mapping for operator or no result defined for ', Expr).
145
146		call_nary_expression(OP, Arg, Result) :-
147		preferences:preference(plugin(absint,abstract_domain_module), DomainModule),
148		DomainModule:map_nary_operator(OP, CallOP),
149		!,
150		call(DomainModule:CallOP, Arg, Result).
151		call_nary_expression(OP, Arg, top) :-
152		Expr =.. [OP, Arg],
153		add_error_fail(call_unary_expression, 'no mapping for operator or no result defined for ', Expr).