Frama-C 插件开发:获取价值分析的结果
Frama-C Plugin development: Getting result of value-analysis
我正在使用价值分析为 Frama-C 开发一个插件。
我只是想在每个语句之后打印变量(值)的状态(我认为解决方案很简单,但我想不通)。
我在访问者的 vstmt_aux
方法中使用 Db.Value.get_stmt_state
获得了当前状态。
我现在如何获取变量的值?
PS:我找到了这个 post,但它没有帮助,没有真正的解决方案,并且在描述的帮助下我无法做到:
下面是一个具体示例,说明如何为每个局部变量和全局变量打印给定函数中每个语句之前由 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 测试。
要在 语句后检索状态 ,只需将 fold_state_callstack
中的 ~after:false
参数替换为 ~after:true
。我以前的代码版本使用了一个函数,该函数已经为预状态绑定了该值,但是没有为 post-状态导出这样的函数,所以我们必须使用 fold_state_callstack
(顺便说一下强大,因为它允许检索每个调用堆栈的特定状态)。
我正在使用价值分析为 Frama-C 开发一个插件。 我只是想在每个语句之后打印变量(值)的状态(我认为解决方案很简单,但我想不通)。
我在访问者的 vstmt_aux
方法中使用 Db.Value.get_stmt_state
获得了当前状态。
我现在如何获取变量的值?
PS:我找到了这个 post,但它没有帮助,没有真正的解决方案,并且在描述的帮助下我无法做到:
下面是一个具体示例,说明如何为每个局部变量和全局变量打印给定函数中每个语句之前由 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 测试。
要在 语句后检索状态 ,只需将 fold_state_callstack
中的 ~after:false
参数替换为 ~after:true
。我以前的代码版本使用了一个函数,该函数已经为预状态绑定了该值,但是没有为 post-状态导出这样的函数,所以我们必须使用 fold_state_callstack
(顺便说一下强大,因为它允许检索每个调用堆栈的特定状态)。