Re: [CIL users] Ptranal Heap Model

[Christoph S. <cs...@fr...>]

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) -> malloc@1
        c_bar(1) -> malloc@2
        tmp(1) -> malloc@1
        tmp(1) -> malloc@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