c - 如何在Frama-C中使用vstmt_aux访问我的语句

我正在开发一个标量替换插件。我对来访者的陈述有些困难。我想分析循环中的指令，对于每个指令，我需要知道它是否包含在循环中，这个循环本身是否包含在另一个循环中。下面是我的vstmt_aux的一个简单示例：

method! vstmt_aux s =
match s.skind with
| Loop(_, body, l, _, _) -> begin
  let lp = (fst l).Lexing.pos_lnum in
  Format.printf "Find outer loop at line %d @.\n" lp;
  let bst = body.bstmts in List.iter(fun vbody ->
    match vbody.skind with
    | Loop(_, subbody, lsub, _, _) -> begin
      let ls = (fst lsub).Lexing.pos_lnum in
      Format.printf "Find inner loop at line %d @.\n" ls;
      let sub_st = subbody.bstmts in List.iter(fun ss_body ->
        match ss_body.skind with
        | Instr(ii) -> Format.printf "Find instruction %a inside inner loop. @.\n" Printer.pp_instr ii
        | Loop(_, l_sub, lss, _, _) -> begin
          let nss = (fst lss).Lexing.pos_lnum in
          Format.printf "Find inner inner loop at line %d @.\n" nss;
          let ss_st = l_sub.bstmts in List.iter(fun ss ->
            match ss.skind with
            | Instr(iii) -> Format.printf "Find instruction %a inner inner loop. @.\n" Printer.pp_instr iii
            | _ -> ()
          ) ss_st
        end
        | _ -> ()
      ) sub_st;
    end
    | Instr(iloop) -> Format.printf "Find instruction %a inside outer loop. @.\n" Printer.pp_instr iloop
    | _ -> ()
  ) bst;
  Cil.SkipChildren
end
| Instr(i) -> Format.printf "Find instruction %a. @.\n" Printer.pp_instr i; Cil.SkipChildren
| _ -> Cil.DoChildren

我要分析的代码示例如下：

void test(int ni, int nj, int nk, float alpha, float *tmp, float *A) {
  int i, j, k;
  for (i = 0; i < ni; i++)
  for (j = 0; j < nk; j++)
    A[i * nk + j] = (float) ((i*j+1) % ni) / ni;

  for (i = 0; i < ni; i++)
    for (j = 0; j < nj; j++) {
      tmp[i * nj + j] = 0.0;
      for (k = 0; k < nk; ++k)
        tmp[i * nj + j] += alpha * A[i * nk + k] * A[i * nk + k];
    }
}

当我在此c代码上运行此脚本时，只检测到指令A[i * nk + j] = (float) ((i*j+1) % ni) / ni;。
Find指令*（A+（i*nk+j））=（float）（i*j+1）%ni）/（float）ni；在内部循环中。
当我在循环模式中使用DoChildren而不是SkipChildren时，循环中的所有指令都会被多次检测到。例如：
指令A[i * nk + j] = (float) ((i*j+1) % ni) / ni;被检测三次：
Find指令*（A+（i*nk+j））=（float）（i*j+1）%ni）/（float）ni；在内部循环中。
Find指令*（A+（i*nk+j））=（float）（i*j+1）%ni）/（float）ni；在外循环内。
Find指令*（A+（i*nk+j））=（float）（i*j+1）%ni）/（float）ni；。
只有第一条信息是真的。
指令tmp[i * nj + j] = 0.0;被检测到一次，但输出消息不正确（当此指令在内部循环中时）
查找指令*（tmp+（i*nj+j））=（float）0.0；。
指令tmp[i * nj + j] += alpha * A[i * nk + k] * B[k * nj + j];也会发生同样的情况。
当我在每个循环和子循环的指令周围添加大括号时，模式| Instr(i) -> Format.printf "Find instruction %a. @.\n" Printer.pp_instr i; Cil.SkipChildren会检测到所有指令。
你知道我怎么解决这个问题吗？
谢谢

最佳答案

我认为最简单的答案是显示Kernel_function.find_enclosing_loop的代码，它返回给定语句所属的最内层循环（如果所述语句不在任何循环中，则引发Not_found）。请注意，主要由于历史原因，原始代码继承自Cil.nopCilVisitor，但这在这里并不重要，除非您有非常特定的用途，否则应该首选Visitor.frama_c_inplace。

let find_enclosing_loop kf stmt =
  let module Res = struct exception Found of Cil_types.stmt end in
  let vis = object
    inherit Visitor.frama_c_inplace
    val loops = Stack.create ()
    method! vstmt_aux s =
      match s.skind with
        | Loop _ ->
          Stack.push s loops;
          Cil.DoChildrenPost (fun s -> ignore (Stack.pop loops); s)
        | _ when Cil_datatype.Stmt.equal s stmt ->
          raise (Res.Found (Stack.top loops))
        | _ -> Cil.DoChildren
  end
  in
  try
    (match stmt.skind with
      | Loop _ -> stmt
      | _ ->
        ignore
          (Visitor.visitFramacFunction vis (get_definition kf));
        raise Not_found)
  with
    | No_Definition -> raise Not_found (* Not the good kf obviously. *)
    | Stack.Empty -> raise Not_found (* statement outside of a loop *)
    | Res.Found s -> s

基本上，这个想法是维护一个当前访问的循环堆栈，每次到达感兴趣的语句时，都可以检查堆栈中有多少元素。访问完循环的子级后，只需弹出堆栈（因此是DoChildrenPost）。