Frama-c: how to access a __malloc* variable allocated by value plugin

Question

I start with Frama-c, so I do not master it well enough. I would like to use Frama-c to implement a pointer aliasing analyzer. Unless I'm mistaken, it seems to me that value plugin does not give information about pointer aliasing.

For a start, here is what I have:

class vtest = object(self)
   inherit Visitor.frama_c_inplace as super

   method private try_khow_exp_from_inst vi loc exp (typ : string) = 
     let vname = vi.vname in 
     match exp.enode with
     | Const _ | SizeOfE _ | AlignOfE _ | SizeOf _ | AlignOf _ | SizeOfStr _-> 
       Format.printf "Local %s of #%s# (of type %a) with a constant (%a) at %a @.\n" 
       typ vname Printer.pp_typ vi.vtype Printer.pp_exp exp Printer.pp_location loc;
       if Cil.isPointerType vi.vtype then 
         Format.printf "#%s# is a pointer type !!! warning: initialization makes pointer from integer without a cast @.\n" vname;

     | Lval(Var v, _) -> 
       Format.printf "Local %s of #%s# with a variable (%s) at %a @.\n" 
       typ vname v.vname Printer.pp_location loc;
       if Cil.isPointerType vi.vtype && Cil.isPointerType v.vtype then 
         Format.printf "Pointer #%s# is aliased with pointer (%s) --> #%s# can't be declared as restrict neither (%s) @.\n" 
         vname v.vname vname v.vname;

     | Lval (Mem e, _) -> 
       let state = Db.Value.get_state (Kstmt (Extlib.the self#current_stmt)) in
       Format.printf "Local %s of variable #%s# with the value pointed by (%a) pointer at %a @.\n"
       typ vname Printer.pp_exp e Printer.pp_location loc;

     | UnOp(op, {enode = Lval (Mem {enode = Lval(Var v_un, _)}, _)}, _) when Cil.isPointerType v_un.vtype -> 
       Format.printf "Local %s of variable #%s# with an unary operation on pointer (%s) at %a @.\n"
       typ vname v_un.vname Printer.pp_location loc;

     | BinOp((PlusPI | IndexPI | MinusPI | MinusPP), {enode = Lval(Var v_ptr, _)}, e2, _) -> 
       if Cil.isPointerType vi.vtype && Cil.isPointerType v_ptr.vtype then
       begin
         Format.printf "Local %s of pointer #%s# with pointer (%s) +|- an offset at %a @.\n" 
         typ vname v_ptr.vname Printer.pp_location loc;
         Format.printf "Pointer #%s# is aliased with pointer (%s) --> #%s# can't be declared as restrict neither (%s) @.\n" 
         vname v_ptr.vname vname v_ptr.vname;
       end

     | StartOf(Var va, _) when Cil.isPointerType vi.vtype -> 
       Format.printf "Local %s of pointer #%s# with start addr of array (%s) at %a @.\n" typ vname va.vname Printer.pp_location loc;
       Format.printf "Pointer #%s# is aliased with array (%s) --> #%s# can't be declared as restrict@.\n" 
       vname va.vname vname;

     | AddrOf(Var v_ad, _) when Cil.isPointerType vi.vtype -> 
       Format.printf "Local %s of pointer #%s# with address of variable (%s) at %a @.\n" 
       typ vname v_ad.vname Printer.pp_location loc;
       Format.printf "Pointer #%s# is aliased with variable (%s) --> #%s# can't be declared as restrict @.\n" 
       vname v_ad.vname vname;

     | _ -> Format.printf "Found unknow case at %a...@.\n" Printer.pp_location loc;

method private do_call var f args l =
let kf = Globals.Functions.get f in 
let name = Kernel_function.get_name kf in
let params = Globals.Functions.get_params kf in
Format.printf "Local init of #%s# at %a: through a call to (%s) with following params --> @." 
var.vname Printer.pp_location l name;
if params != [] then List.iter(fun vi -> 
                               let lval = (Var vi, NoOffset) in (* make an lval from a varinfo *)
                               let loc = !Db.Value.lval_to_loc self#current_kinstr ~with_alarms:CilE.warn_none_mode lval in 
                               Db.Value.fold_state_callstack (fun state () -> (* for each state in the callstack *)
                                let value = Db.Value.find state loc in (* obtain value for location *)
                                Format.printf "%a -> %a@." Printer.pp_varinfo vi
                                Locations.Location_Bytes.pretty value (* print mapping *)
                               ) () ~after:true self#current_kinstr
                              ) params;
Format.printf "@.\n"

method! vinst i = 
  if Db.Value.is_reachable (Db.Value.get_state self#current_kinstr) then 
    match i with
    | Local_init (vi, AssignInit(SingleInit e), loc) ->  
      let t = "init" in
      self#try_khow_exp_from_inst vi loc e t;
      Cil.SkipChildren

    (*| Local_init (ci, AssignInit(CompoundInit _), loc)*)(**ToDo*)

    | (Local_init(v, ConsInit(f, args, k), l)) when Cil.isPointerType v.vtype -> begin
       match k with
       | Plain_func -> self#do_call v f args l ; Cil.SkipChildren 
       | Constructor -> Cil.SkipChildren
    end

    | Set((Var(vi),NoOffset), exp, place) -> 
      let s = "setting" in
      self#try_khow_exp_from_inst vi place exp s; 
      Cil.SkipChildren

    | Call(Some(Var call, _), {enode = Lval(Var vfunc, _)}, argl, lsome) ->
      Format.printf "Call to (%s) and result is the lval #%s# at %a @." vfunc.vname call.vname Printer.pp_location lsome;
      Format.printf "Function (%s) is called with following params: @.\n" vfunc.vname;
      if argl != [] then
        List.iter (fun exp -> match exp.enode with
                     | Lval(Var e, _) when Cil.isPointerType e.vtype -> Format.printf "pointer #%s#  " e.vname;
                     | Lval(Var e, _) when not( Cil.isPointerType e.vtype || Cil.isArrayType e.vtype) -> 
                       Format.printf "variable #%s#  " e.vname;
                     | Lval(Var e, _) when Cil.isArrayType e.vtype -> Format.printf "static array #%s#  " e.vname;
                     | AddrOf(Var v_ad, _) -> Format.printf "variable #%s#  " v_ad.vname;
                     | _ -> ()
         ) argl;
      Format.printf "@.\n"; 
      Cil.SkipChildren

    | Call(None, {enode = Lval(Var vfunc, _)}, argl, lnone) -> 
      Format.printf "Call to (%s) at %a with following params: @.\n" vfunc.vname Printer.pp_location lnone; 
      if argl != [] then
        List.iter (fun exp -> match exp.enode with
                     | Lval(Var e, _) when Cil.isPointerType e.vtype -> Format.printf "pointer #%s#  " e.vname;
                     | Lval(Var e, _) when not( Cil.isPointerType e.vtype || Cil.isArrayType e.vtype) -> 
                       Format.printf "variable #%s#  " e.vname;
                     | Lval(Var e, _) when Cil.isArrayType e.vtype -> Format.printf "static array #%s#  " e.vname;
                     | AddrOf(Var v_ad, _) -> Format.printf "variable #%s#  " v_ad.vname;
                     | _ -> ()
        ) argl;
      Format.printf "@.\n"; 
      Cil.SkipChildren

    | _ -> Cil.DoChildren

   else begin
     Format.printf "Not reachable by Db.Value ...@.";
     Cil.SkipChildren 
   end 

   initializer !Db.Value.compute();

end

With this script I can detect some pointers aliasing case. But, for dynamically allocated array with malloc for example, I have some difficulties.

Take for example this little program:

int main(int argc, char** argv) {
  int n = 20;
  int *a = malloc(n * sizeof(int)); 
  int *b = malloc(n * sizeof(int));
  int i;
  for(i = 0; i<n; i++)
    *(a + i) = 14 + i;
  return 0;
}

When I launch inout plugin for example with -deref option, I can see the two value messages:

/home/rokiatou/Documents/frama-c-scripts/test.c:11:[value] allocating variable __malloc_main_l11

/home/rokiatou/Documents/frama-c-scripts/test.c:12:[value] allocating variable __malloc_main_l12

And these messages of inout plugin:

[inout] Derefs for function main: __malloc_main_l11[0..19]

And I read in value plug-in guide, in section 4.6.4:

Dynamic allocation is modeled by creating new bases. Each call to malloc and realloc potentially creates a new base.

And in section 8.1.1 that value messages of this form:

[value] allocating variable __malloc_main_l42_2981

Indicate that new bases are being created.

So my questions are:

1) How can I access to the base address of variables __malloc* allocated by value and associate it to my real variables present in my source code (for example here the variables a and b)?

2) How can I get the number of elements allocated by a malloc function (here in my example, it is n (=20))?

I already look at the files cil_types.mli (where I found TPtr and TArray type) and base.mli but I did not really understand their use.

Answer 1

What you're trying to achieve is not extremely clear, but there are several points in your do_call methods that look suspicious:

• From what I've understood, you should treat int *x = malloc (sizeof(*x)); and x = malloc(sizeof(*x)); in quite similar ways. In other words, you can probably factorize most of the work between Local_init (with Cons_init) and Call cases
• You should probably discriminate against the name of the callee. Basically only malloc, calloc and realloc are relevant here.
• (Probably the main source of your issue at the moment) You're confusing the formal parameters of the function declaration with the actual parameters of the call. At call site, EVA has no value associated with the formers: you should evaluate the expressions in the args list instead of the varinfo in the params list.