Разработка плагина Frama-C: получение результата анализа стоимости

Question

Я работаю над плагином для Frama-C, используя Value-analysis. Я просто хочу напечатать состояние переменных (значений) после каждого оператора (я думаю, что решение довольно легко, но я не мог понять это).

Я получил текущее состояние с Db.Value.get_stmt_state в vstmt_aux метод в госте.

Как я могу теперь получить значения переменных?

PS: я нашел этот пост, но это не помогло, реального решения нет, и с помощью описания я не смог это сделать: как использовать функции в модулях Value.Eval_expr, Value.Eval_op и т.д. Frama-c Value плагин

Answer 1

Вот конкретный пример того, как вывести для каждой локальной и глобальной переменной результат, вычисленный по значению перед каждым оператором в данной функции (прочитайте функции снизу вверх):

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 (что, кстати, является более мощным, поскольку позволяет получать определенное состояние для каждого стека вызовов).

Answer 2

Обновление с использованием нового API Eva (начиная с Frama-C 25.0)

Это обновление предыдущего ответа с использованием нового API Евы, доступного начиная с Frama-C 25.0 (магний); Я оставил исходный ответ для пользователей на основе более старых версий Frama-C.

Используя новый 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был напечатан как неограниченный интервал[--..--]с предыдущим кодом; здесь это напечатано как[-2147483648..2147483647]при использовании machdep с 32-битными целыми числами).

Новый API также упрощает ответы на такие запросы, как « Есть ли способ получить значения после оператора?». : просто используйтеEva.Results.afterвместоEva.Results.before.

Наконец, для получения информации о стеке вызовов выполните поискcallstackвsrc/plugins/value/utils/results.mliфайл. Этот файл также содержит несколько длинных комментариев, объясняющих API, а также набросок использования.