171 lines
5.3 KiB
Prolog
171 lines
5.3 KiB
Prolog
% -*- prolog -*-
|
|
%*******************************************************************************
|
|
% Prelude
|
|
%*******************************************************************************
|
|
|
|
% This file implements a basic context-insensitive pointer analysis.
|
|
% Its outputs are the following relations:
|
|
%
|
|
% point_to(V, M) - variable 'V' may point to abstract memory loc 'M'
|
|
% call_edge(INVOKE, TARGET) - invocation site 'INVOKE' calls function 'TARGET'
|
|
|
|
% Based upon: Java context-insensitive inclusion-based pointer analysis
|
|
% by John Whaley
|
|
|
|
% Related work:
|
|
% - Andersen, Steengaard, Manuvir Das, Lin, etc
|
|
% - bddbddb, DOOP, http://pag-www.gtisc.gatech.edu/chord/user_guide/datalog.html
|
|
% - http://blog.jetbrains.com/idea/2009/08/analyzing-dataflow-with-intellij-idea
|
|
% - Frama C, CodeSonar, Coverity, ...
|
|
%
|
|
% note: I always wanted (but was never able to write ...) an interprocedural
|
|
% (dataflow) analysis. With Datalog I did it in one day! It's so easy.
|
|
%
|
|
|
|
% history:
|
|
% - I used to have an array_point_to/2 but it can not work, we have to
|
|
% unify array and pointers and so point_to and array_point_to
|
|
|
|
%*******************************************************************************
|
|
% Relations
|
|
%*******************************************************************************
|
|
|
|
% Abstract memory locations (also called heap objects), are mostly qualified
|
|
% symbols (e.g 'main__foo', 'ret_main', '_cst_line2_'):
|
|
% - each globals, functions, constants
|
|
% - each malloc (context insensitively). will do sensitively later for
|
|
% malloc wrappers or maybe each malloc with certain type. (e.g. any Proc)
|
|
% so have some form of type sensitivty at least
|
|
% - each locals (context insensitively first), when their addresses are taken
|
|
% - each fields (field-based, see sep08.pdf lecture, so *.f, not x.*)
|
|
% - array element (array insensitive, aggregation)
|
|
|
|
% Invocations: line in the file (e.g. '_in_main_line_14_')
|
|
|
|
%assign(dest:V, source:V) input
|
|
%assign_address (dest:V, source:V) input
|
|
%assign_deref(dest:V, source:V) input
|
|
%assign_content(dest:V, source:V) input
|
|
|
|
%parameter(f:F, z:Z, v:V)
|
|
%return(f:F, v:V)
|
|
%argument(i:I, z:Z, v:V)
|
|
%call_direct(i:I, f:F)
|
|
%call_indirect(i:I, v:V)
|
|
%call_ret(i:I, v:V)
|
|
|
|
%assign_array_elt(dest:V, source:V) input
|
|
%assign_array_element_address(dest:V, source:V) input
|
|
|
|
%assign_load_field
|
|
%assign_field_address
|
|
%assign_store_field
|
|
%field_point_to?? hmm maybe once we differentiate objects heap
|
|
% and not do just *.f
|
|
|
|
%*******************************************************************************
|
|
% Rules
|
|
%*******************************************************************************
|
|
|
|
%-------------------------------------------------------------------------------
|
|
% Basic
|
|
%-------------------------------------------------------------------------------
|
|
|
|
% p = &q
|
|
point_to(P, Q) :-
|
|
assign_address(P, Q).
|
|
|
|
% p = q
|
|
point_to(P, L) :-
|
|
assign(P, Q),
|
|
point_to(Q, L).
|
|
|
|
% *p = q, given: q -> l, and p -> w => w now points to l
|
|
point_to(W, L) :-
|
|
assign_deref(P, Q),
|
|
point_to(Q, L),
|
|
point_to(P, W).
|
|
|
|
% p = *q
|
|
point_to(P, L) :-
|
|
assign_content(P, Q),
|
|
point_to(Q, X),
|
|
point_to(X, L).
|
|
% see here that X is used both as first and second argument of point_to
|
|
% because the domain of the variable is included in the domain of abstract
|
|
% memory locations.
|
|
|
|
%-------------------------------------------------------------------------------
|
|
% Arrays insensitive
|
|
%-------------------------------------------------------------------------------
|
|
|
|
% p = a[...], which is really just equivalent to p = *a for array insensitivty
|
|
point_to(P, Q) :-
|
|
assign_array_elt(P, A),
|
|
point_to(A, AELT),
|
|
point_to(AELT, Q).
|
|
|
|
% a[...] = q, again similar to *a = q
|
|
point_to(AELT, L) :-
|
|
assign_array_deref(A, Q),
|
|
point_to(Q, L),
|
|
point_to(A, AELT).
|
|
|
|
% p = &a[...], equivalent to p = a for array insensitivty
|
|
point_to(P, AELT) :-
|
|
assign_array_element_address(P, A),
|
|
point_to(A, AELT).
|
|
|
|
%-------------------------------------------------------------------------------
|
|
% Field-base sensitive (*.f, not x.* nor x.f)
|
|
%-------------------------------------------------------------------------------
|
|
|
|
% p = x->fld
|
|
point_to(P, L) :-
|
|
assign_load_field(P, X, F),
|
|
point_to(F, L).
|
|
|
|
|
|
% p->fld = x
|
|
point_to(F, L) :-
|
|
assign_store_field(P, F, X),
|
|
point_to(X, L).
|
|
|
|
% p = &x->fld
|
|
point_to(P, F) :-
|
|
assign_field_address(P, X, F).
|
|
|
|
%point_to(F, L) :-
|
|
% field_point_to(F, L).
|
|
|
|
|
|
%-------------------------------------------------------------------------------
|
|
% Calls context-insensitive
|
|
%-------------------------------------------------------------------------------
|
|
|
|
% ret = foo(v1, v2, ...)
|
|
assign(PARAM, ARG) :-
|
|
parameter(F, IDX, PARAM),
|
|
call_edge(I, F),
|
|
argument(I, IDX, ARG).
|
|
assign(RET, V) :-
|
|
return(F, V),
|
|
call_edge(I, F),
|
|
call_ret(I, RET).
|
|
|
|
call_edge(I, F) :-
|
|
call_direct(I, F).
|
|
% power of mutually recursive analysis! dataflow -> controlflow -> dataflow
|
|
call_edge(I, F) :-
|
|
call_indirect(I, V),
|
|
point_to(V, F).
|
|
|
|
%note: heartbleed detection strongly relies on accurate calls though
|
|
% function pointers tracking
|
|
|
|
%*******************************************************************************
|
|
% Postlude
|
|
%*******************************************************************************
|
|
|
|
point_to(A,B)?
|
|
%call_edge(A,B)?
|