Frama-C 插件开发:获取价值分析的结果

Question

我正在使用值分析为Frama-C开发插件。我只想在每个语句之后打印变量（值）的状态（我认为解决方案很简单，但我无法弄清楚）。

我在访问者的vstmt_aux方法中获得了Db.Value.get_stmt_state的当前状态。

我现在如何获取变量的值？

PS：我找到了这篇文章，但它没有帮助，没有真正的解决方案，在描述的帮助下我无法做到：如何使用 Frama-c 值插件的 Value.Eval_expr、Value.Eval_op 等模块中的函数

Answer 1

下面是一个具体示例，说明如何为每个局部变量和全局变量打印给定函数中每个语句之前由 Value 计算的结果（从下到上阅读函数）：

open Cil_types
(* Prints the value associated to variable [vi] before [stmt]. *)
let pretty_vi fmt stmt vi =
  let kinstr = Kstmt stmt in (* make a kinstr from a stmt *)
  let lval = (Var vi, NoOffset) in (* make an lval from a varinfo *)
  let loc = (* make a location from a kinstr + an lval *)
    !Db.Value.lval_to_loc 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.fprintf fmt "%a -> %a@." Printer.pp_varinfo vi
         Locations.Location_Bytes.pretty value (* print mapping *)
    ) () ~after:false kinstr
(* Prints the state at statement [stmt] for each local variable in [kf],
   and for each global variable. *)
let pretty_local_and_global_vars kf fmt stmt =
  let locals = Kernel_function.get_locals kf in
  List.iter (fun vi -> pretty_vi fmt stmt vi) locals;
  Globals.Vars.iter (fun vi _ -> pretty_vi fmt stmt vi)
(* Visits each statement in [kf] and prints the result of Value before the
   statement. *)
class stmt_val_visitor kf =
  object (self)
    inherit Visitor.frama_c_inplace
    method! vstmt_aux stmt =
      (match stmt.skind with
       | Instr _ ->
         Format.printf "state for all variables before stmt: %a@.%a@."
           Printer.pp_stmt stmt (pretty_local_and_global_vars kf) stmt
       | _ -> ());
      Cil.DoChildren
  end
(* usage: frama-c file.c -load-script print_vals.ml *)
let () =
  Db.Main.extend (fun () ->
      Format.printf "computing value...@.";
      !Db.Value.compute ();
      let fun_name = "main" in
      Format.printf "visiting function: %s@." fun_name;
      let kf_vis = new stmt_val_visitor in
      let kf = Globals.Functions.find_by_name fun_name in
      let fundec = Kernel_function.get_definition kf in
      ignore (Visitor.visitFramacFunction (kf_vis kf) fundec);
      Format.printf "done!@.")

这远非理想，输出比简单地使用Cvalue.Model.pretty state更丑陋，但它可以作为进一步修改的基础。

此脚本已使用 Frama-C 镁进行了测试。

要检索语句后的状态，只需将 fold_state_callstack 中的 ~after:false 参数替换为 ~after:true 。我以前的代码版本使用了一个函数，该函数已经为前状态绑定了该值，但没有为后状态导出此类函数，因此我们必须使用 fold_state_callstack（顺便说一下，它更强大，因为它允许检索每个调用堆栈的特定状态）。

Answer 2

使用Eva的新API进行更新（从Frama-C 25.0开始）

这是对之前答案的更新，使用Eva的新API，自Frama-C 25.0（镁）起可用;我为基于旧版 Frama-C 的用户留下了原始答案。

使用Eva的新API，上面的答案可以写得更简洁：

(* Prints the value associated to variable [vi] before [stmt]. *)
let pretty_vi fmt stmt vi =
  let req = Eva.Results.before stmt in
  let cvalue = Eva.Results.(eval_var vi req |> as_cvalue) in
  Format.fprintf fmt "%a -> %a@." Printer.pp_varinfo vi
    Cvalue.V.pretty cvalue (* print mapping *)
(* Prints the state at statement [stmt] for each local variable in [kf],
   and for each global variable. *)
let pretty_local_and_global_vars kf fmt stmt =
  let locals = Kernel_function.get_locals kf in
  List.iter (fun vi -> pretty_vi fmt stmt vi) locals;
  Globals.Vars.iter (fun vi _ -> pretty_vi fmt stmt vi)
(* Visits each statement in [kf] and prints the result of Value before the
   statement. *)
class stmt_val_visitor kf =
  object
    inherit Visitor.frama_c_inplace
    method! vstmt_aux stmt =
      (match stmt.skind with
       | Instr _ ->
         Format.printf "state for all variables before stmt: %a@.%a@."
           Printer.pp_stmt stmt (pretty_local_and_global_vars kf) stmt
       | _ -> ());
      Cil.DoChildren
  end
(* usage: frama-c file.c -load-script print_vals.ml *)
let () =
  Db.Main.extend (fun () ->
      Format.printf "computing value...@.";
      Eva.Analysis.compute ();
      let fun_name = "main" in
      Format.printf "visiting function: %s@." fun_name;
      let kf_vis = new stmt_val_visitor in
      let kf = Globals.Functions.find_by_name fun_name in
      let fundec = Kernel_function.get_definition kf in
      ignore (Visitor.visitFramacFunction (kf_vis kf) fundec);
      Format.printf "done!@.")

请注意，输出并不相同;它实际上更精简，例如，而不是打印。 score -> {{ NULL -> {0} }} ，这意味着，对于位置score，与 NULL 基数关联的偏移量，即常量值，为 0，它只是打印score -> {0} 。它还根据变量类型打印最小/最大边界（例如 int __fc_errno被打印为与前面的代码[--..--]的无限间隔;在这里，当使用具有 32 位整数的 Machdep 时，它被打印为 [-2147483648..2147483647]）。

新的 API 还可以更轻松地回答诸如"是否也有办法获取语句后的值？"：只需使用 Eva.Results.after 而不是 Eva.Results.before 等查询。

最后，对于特定于调用堆栈的信息，请在src/plugins/value/utils/results.mli文件中搜索callstack。此文件还包含一些解释 API 的长篇注释，以及使用草图。