c - Frama-c:如何访问由值插件分配的 __malloc* 变量

Question

我是从 Frama-c 开始的，所以我对它的掌握还不够好。我想使用 Frama-c 来实现指针别名分析器。除非我弄错了，否则在我看来，值插件不会提供有关指针别名的信息。

首先，这是我所拥有的:

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

通过这个脚本，我可以检测到一些指针别名的情况。但是，例如，对于使用 malloc 动态分配的数组，我遇到了一些困难。

以这个小程序为例:

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;
}

例如，当我使用 -deref 选项启动 inout 插件时，我可以看到两个值消息:

/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

以及 inout 插件的这些消息:

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

我在第 4.6.4 节中阅读了值(value)插件指南:

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

在第 8.1.1 节中，这种形式的值消息:

[value] allocating variable __malloc_main_l42_2981

表示正在创建新的基地。

所以我的问题是:

1) 我如何访问按值分配的变量 __malloc* 的基地址并将其关联到我的源代码中存在的真实变量(例如这里的变量 a 和 b)?

2) 如何获取 malloc 函数分配的元素数量(在我的示例中，它是 n (=20))？

我已经查看了文件 cil_types.mli(我在其中找到了 TPtr 和 TArray 类型)和 base.mli，但我并没有真正理解它们的用途。

Answer 1

您要实现的目标不是很清楚，但是您的 do_call 方法中有几点看起来很可疑:

• 据我了解，您应该对待 int *x = malloc (sizeof(*x)); 和 x = malloc(sizeof(*x)); 以非常相似的方式。换句话说，您可能可以分解 Local_init(使用 Cons_init)和 Call 情况
之间的大部分工作
• 您可能应该歧视被叫者的名字。基本上只有 malloc、calloc 和 realloc 在这里是相关的。
• (目前可能是您问题的主要来源)您将函数声明的形式参数与调用的实际参数混淆了。在调用点，EVA 没有与前者相关的值:您应该计算 args 列表中的表达式，而不是 params 中的 varinfo列表。