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

Question

我是从 Frama-c 开始的，所以我没有很好地掌握它。我想用 Frama-c 来实现一个指针别名分析器。除非我弄错了，否则在我看来 value 插件没有提供有关指针别名的信息。

首先，这是我所拥有的：

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]分配变量__malloc_main_l11

/home/rokiatou/Documents/frama-c-scripts/test.c:12:[value] 分配变量__malloc_main_l12

以及inout插件的这些消息：

[inout] 函数 main 的 Derefs：__malloc_main_l11[0..19]

我在第 4.6.4 节中阅读了 value 插件指南：

动态分配是通过创建新的基础来建模的。每次调用 malloc 和 realloc 都可能创建一个新基。

在第 8.1.1 节中，重视这种形式的消息：

[value] 分配变量__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。