:- module(safe_code,
	  [ safe_goal/1
	  ]).
:- use_module(library(assoc)).
:- use_module(library(debug)).

		 /*******************************
		 *	      SAFETY		*
		 *******************************/

:- meta_predicate
	safe_goal(0).

%%	safe_goal(:Goal)
%
%	True if calling Goal provides no   security risc. There are lots
%	of nasty things one can do with Prolog, so providing a whitelist
%	is probably the safest way.

safe_goal(M:Goal) :-
	empty_assoc(Safe0),
	catch(safe(Goal, M, [], Safe0, _), E,
	      (	  print_message(error, E),
		  fail
	      )).
					% basic stuff

%%	safe(+Goal, +Module, +Parents, +Safe0, -Safe) is semidet.
%
%	Is true if Goal can only calls safe code.

safe(V, _, _, _, _) :-
	var(V), !, fail.
safe(M:G, _, Parent, Safe0, Safe) :- !,
	safe(G, M, Parent, Safe0, Safe).
safe(G, _, Parents, _, _) :-
	debugging(safe_code(show)),
	length(Parents, Level),
	format('[~D] SAFE ~q~n', [Level, G]),
	fail.
safe(G, _, _, Safe, Safe) :-
	safe_primitive(G), !.
safe(G, M, Parents, Safe0, Safe) :-
	safe_meta(G, Called), !,
	safe_list(Called, M, Parents, Safe0, Safe).
safe(G, M, Parents, Safe0, Safe) :-
	goal_id(M:G, Id),
	(   get_assoc(Id, Safe0, _)
	->  Safe = Safe0
	;   put_assoc(Id, Safe0, true, Safe1),
	    safe_clauses(G, M, [Id|Parents], Safe1, Safe)
	).

safe_clauses(G, M, Parents, Safe0, Safe) :-
	predicate_property(M:G, interpreted),
	\+ predicate_property(M:G, meta_predicate(_)), !,
	def_module(M:G, MD:G),
	findall(Body, clause(MD:G, Body), Bodies),
	safe_list(Bodies, MD, Parents, Safe0, Safe).
safe_clauses(_, _M, [G|Parents], _, _) :-
	debug(safe_code, 'Unsafe: ~q (parents = ~q)', [G, Parents]),
	fail.

safe_list([], _, _, Safe, Safe).
safe_list([H|T], M, Parents, Safe0, Safe) :-
	copy_term(H, H1),
	safe(H1, M, Parents, Safe0, Safe1),
	safe_list(T, M, Parents, Safe1, Safe).


def_module(M:G, MD:G) :-
	predicate_property(M:G, imported_from(MD)), !.
def_module(G, G).


goal_id(V, _) :-
	var(V),	!, fail.
goal_id(M:Goal, M:Id) :- !,
	goal_id(Goal, Id).
goal_id(Term, Name/Arity) :-
	functor(Term, Name, Arity).

safe_primitive(true).
safe_primitive(false).
safe_primitive(fail).
safe_primitive(repeat).
safe_primitive(!).
					% types
safe_primitive(var(_)).
safe_primitive(nonvar(_)).
safe_primitive(integer(_)).
safe_primitive(float(_)).
safe_primitive(atom(_)).
safe_primitive(compound(_)).
safe_primitive(ground(_)).
safe_primitive(cyclic_term(_)).
					% ordering
safe_primitive(@>(_,_)).
safe_primitive(@>=(_,_)).
safe_primitive(==(_,_)).
safe_primitive(@<(_,_)).
safe_primitive(@=<(_,_)).
safe_primitive(compare(_,_,_)).
safe_primitive(sort(_,_)).
safe_primitive(msort(_,_)).
safe_primitive(keysort(_,_)).
					% unification and equivalence
safe_primitive(=(_,_)).
safe_primitive(\==(_,_)).
					% arithmetic
safe_primitive(is(_,_)).
safe_primitive(>(_,_)).
safe_primitive(>=(_,_)).
safe_primitive(=:=(_,_)).
safe_primitive(=\=(_,_)).
safe_primitive(=<(_,_)).
safe_primitive(<(_,_)).
safe_primitive(between(_,_,_)).
safe_primitive(succ(_,_)).
safe_primitive(plus(_,_,_)).
					% term-handling
safe_primitive(arg(_,_,_)).
safe_primitive(setarg(_,_,_)).
safe_primitive(functor(_,_,_)).
safe_primitive(_ =.. _).
safe_primitive(copy_term(_,_)).
safe_primitive(term_variables(_,_)).
safe_primitive(numbervars(_,_,_)).
					% atoms
safe_primitive(term_to_atom(_,_)).
safe_primitive(concat_atom(_,_)).
					% Lists
safe_primitive(length(_,_)).
safe_primitive(is_list(_)).
safe_primitive(memberchk(_,_)).
safe_primitive('$skip_list'(_,_,_)).
					% exceptions
safe_primitive(throw(_)).
					% attributes
safe_primitive(get_attr(_,_,_)).
safe_primitive(del_attr(_,_)).
					% globals
safe_primitive(b_getval(_,_)).
safe_primitive(b_setval(_,_)).
					% misc
safe_primitive(current_prolog_flag(_,_)).

%%	safe_meta(+Goal, -Called) is semidet.
%
%	True if Goal is a meta-predicate that is considered safe iff all
%	elements in Called are safe.

safe_meta(put_attr(_,M,A), [M:attr_unify_hook(A, _)]) :-
	atom(M), !.
safe_meta(Phrase, [Goal]) :-
	expand_phrase(Phrase, Goal), !.
safe_meta(Goal, Called) :-
	generic_goal(Goal, Gen),
	safe_meta(Gen),
	findall(C, called(Gen, Goal, C), Called).

called(Gen, Goal, Called) :-
	arg(I, Gen, Spec),
	integer(Spec),
	arg(I, Goal, Called0),
	extend(Spec, Called0, Called).

generic_goal(G, Gen) :-
	functor(G, Name, Arity),
	functor(Gen, Name, Arity).

extend(0, G, G) :- !.
extend(I, G0, G) :-
	G0 =.. List,
	length(Extra, I),
	append(List, Extra, All),
	G =.. All.

safe_meta((0,0)).
safe_meta((0;0)).
safe_meta((0->0)).
safe_meta(forall(0,0)).
safe_meta(catch(0,_,0)).
safe_meta(findall(_,0,_)).
safe_meta(setof(_,0,_)).
safe_meta(\+(0)).
safe_meta(maplist(1, _)).
safe_meta(maplist(2, _, _)).
safe_meta(maplist(3, _, _, _)).
safe_meta(call(0)).
safe_meta(call(1, _)).
safe_meta(call(2, _, _)).
safe_meta(call(3, _, _, _)).
safe_meta(prove(_, _)).


		 /*******************************
		 *	       PHRASE		*
		 *******************************/

%%	expand_phrase(+Phrase, -Expanded) is semidet.
%
%	@see Copied from library(apply_macros).

expand_phrase(phrase(NT,Xs0), NewGoal) :-
	expand_phrase(phrase(NT,Xs0,[]), NewGoal).
expand_phrase(phrase(NT,Xs0,Xs), NewGoal) :-
	Goal = phrase(NT,Xs0,Xs),
	nonvar(NT),
	catch('$translate_rule'((pseudo_nt --> NT), Rule),
	      error(Pat,ImplDep),
	      ( \+ harmless_dcgexception(Pat),
		throw(error(Pat,ImplDep))
	      )),
	Rule = (pseudo_nt(Xs0c,Xsc) :- NewGoal0),
	Goal \== NewGoal0,
	\+ contains_illegal_dcgnt(NT), !,	% apply translation only if we are safe
	(   var(Xsc), Xsc \== Xs0c
	->  Xs = Xsc, NewGoal1 = NewGoal0
	;   NewGoal1 = (NewGoal0, Xsc = Xs)
	),
	(   var(Xs0c)
	-> Xs0 = Xs0c,
	   NewGoal = NewGoal1
	;  ( Xs0 = Xs0c, NewGoal1 ) = NewGoal
	).

harmless_dcgexception(instantiation_error).	% ex: phrase(([1],x:X,[3]),L)
harmless_dcgexception(type_error(callable,_)).	% ex: phrase(27,L)

contains_illegal_dcgnt(NT) :-
	sub_term(I, NT),
	nonvar(I),
	( I = ! ; I = phrase(_,_,_) ), !.