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

Question

我正在使用价值分析为Frama-C制作插件.我只想在每个语句之后打印变量(值)的状态(我认为解决方案很容易安静,但我无法弄明白).

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

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

PS:我发现这篇文章,但它没有帮助,没有真正的解决方案,并且在描述的帮助下我无法做到: 如何在Value.Eval_expr,Value.Eval_op等模块中使用函数Frama-c Value插件

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 Magnesium测试.

要检索状态后的声明中,只需更换~after:false参数fold_state_callstack与~after:true.我之前的代码版本使用了一个函数,该函数已经为前置状态绑定了该值,但是没有为后置状态导出这样的函数,所以我们必须使用fold_state_callstack(顺便说一下,它更强大,因为它允许检索特定的状态每个callstack).