Hello Cole -
> I am trying to use the Ptranal points-to analysis (with Golf) in CIL
> 1.3.7 to compute points-to sets containing dynamically allocated memory
> locations, but the points-to analysis seems to consider all pointers to
> any malloc'd memory as pointing to the same location (specifically, the
> same varinfo structure).
>
> I am generating the points-to sets by calling Ptranal.analyze_file and
> requesting the points-to set for an lval with Ptranal.resolve_lval.
All functions of so called "High-level Query Interface" of
Ptranal answer Cil entities, i.e. something plain Cil is aware of:
val resolve_lval: Cil.lval -> Cil.varinfo list
val resolve_exp: Cil.exp -> Cil.varinfo list
val resolve_funptr: Cil.exp -> Cil.fundec list
So, you don't get abstract locations, but variables and functions.
This is correct and useful, but I understand that it might not enough
for your purpose.
> Does Ptranal/Golf inherently model all calls to malloc as returning
> pointers to the same abstract location, or am I using it incorrectly? I
> would really like a model where each memory allocation site is treated
> as returning a single, unique abstract location. Can this be done with
> Ptranal?
Dynamic memory allocation is internally modelled with
_different_ abstract locations. You just did not use the functions
that answer them: the "Low-level Query Interface", e.g.:
val absloc_of_lval: Cil.lval -> absloc
val absloc_of_varinfo: Cil.varinfo -> absloc
For a quick test run cilly on
// cil-malloc.c
extern void *malloc(unsigned long int);
char *c_foo, *c_bar;
void foo(void) {c_foo = malloc(1);}
void bar(void) {c_bar = malloc(1);}
int main(void) {foo(); bar(); return 0;}
like
cilly.byte --doptranal --ptr_types --ptr_results cil-malloc.c
to get
Computing points-to sets...
c_foo(1) -> mal...@1
c_bar(1) -> mal...@2
tmp(1) -> mal...@1
tmp(1) -> mal...@2
Total number of things pointed to: 4
Printing inferred types of lvalues...
bar : [{'fi56,fun(|"bar"|,<void>,'fi59)}]^("bar")
foo : [{'fi14,fun(|"foo"|,<void>,'fi17)}]^("foo")
tmp : [{ref(|"l_78"|,'fi85),'fi71}]^("tmp")
tmp : [{ref(|"l_36"|,'fi43),'fi29}]^("tmp")
c_bar : [{ref(|"l_87"|,'fi85),'fi80}]^("c_bar")
main : [{'fi98,fun(|"main"|,<void>,'fi101)}]^("main")
c_foo : [{ref(|"l_45"|,'fi43),'fi38}]^("c_foo")
You see how Ptranal records the different malloc calls.
I have whipped up a tiny visitor to demonstrate what Ptranal can
deliver right now.
class lval_visitor =
object
inherit Cil.nopCilVisitor
method vfunc (a_function: Cil.fundec): Cil.fundec Cil.visitAction =
print_endline ("function `" ^ a_function.Cil.svar.Cil.vname ^ "'");
Cil.DoChildren
method vlval (an_lvalue: Cil.lval): Cil.lval Cil.visitAction =
print_string "lval ";
ignore (Pretty.printf "`%a'" Cil.dn_lval an_lvalue);
print_string ", abstract location: ";
begin
try ignore (Pretty.printf "%a\n" Ptranal.d_absloc
(Ptranal.absloc_of_lval an_lvalue))
with Not_found -> print_string "n/a\n"
end;
List.iter
(fun x -> print_endline (" " ^ x.Cil.vname))
(try Ptranal.resolve_lval an_lvalue
with Not_found -> print_endline (" Could not resolve lval!");
[]);
print_newline ();
Cil.DoChildren
end
let initialize_ptranal a_file =
Ptranal.analyze_mono := false;
Ptranal.no_sub := false;
Ptranal.smart_aliases := true;
Ptranal.feature.Cil.fd_doit a_file
let feature = {
Cil.fd_name = "ptranal_test";
Cil.fd_enabled = ref false;
Cil.fd_description = "Ptranal module test";
Cil.fd_extraopt = [];
Cil.fd_doit = (fun a_file ->
initialize_ptranal a_file;
Cil.visitCilFileSameGlobals (new lval_visitor:>
Cil.cilVisitor) a_file);
Cil.fd_post_check = false
}
You can play with golf.ml around line 1628 and modify
absloc_print_name or d_absloc to get other formats. Probably you need
to extend the interface to Ptranal.absloc to get exactly what you
want.
HTH,
Chris
------------------------------------------------------------------------------
Download Intel® Parallel Studio Eval
Try the new software tools for yourself. Speed compiling, find bugs
proactively, and fine-tune applications for parallel performance.
See why Intel Parallel Studio got high marks during beta.
http://p.sf.net/sfu/intel-sw-dev
_______________________________________________
CIL-users mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/cil-users
