Frama-C Plugin development: Getting result of value-analysis

Question

I am working on a Plugin for Frama-C, using the Value-analysis. I simply want to print the state of the variables (values) after each statement (I think the solution is quiet easy, but I couldn't figure it out).

I got the current state with Db.Value.get_stmt_state in the vstmt_aux method in the visitor.

How can I now get the values of the variables?

PS: I found this post, but it didn't help, there is no real solution, and with the help of the description I was not able to do it: How to use functions in Value.Eval_expr, Value.Eval_op etc modules of Frama-c Value plugin

Answer 1

Update using Eva's new API (since Frama-C 25.0)

This is an update to the previous answer, using Eva's new API, available since Frama-C 25.0 (Magnesium); I left the original answer for users based on older Frama-C versions.

Using Eva's new API, the above answer can be written more succinctly:

(* 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!@.")

Note that the output is not identical; it is actually more condensed, as in, instead of printing e.g. score -> {{ NULL -> {0} }}, which means, for location score, the offset associated to the NULL base, that is, a constant value, is 0, it simply prints score -> {0}. It also prints minimum/maximum bounds according to the variable type (e.g. int __fc_errno was printed as an unbounded interval [--..--] with the previous code; here, it is printed as [-2147483648..2147483647] when using a machdep with 32-bit integers).

The new API also makes it easier to answer queries such as Is there also a way to get the values after the statement?: just use Eva.Results.after instead of Eva.Results.before.

Finally, for callstack-specific information, search for callstack in the src/plugins/value/utils/results.mli file. This file also contains some lenghty comments explaining the API, as well as a usage sketch.

Answer 2

Here's a concrete example of how to print, for each local and global variable, the result computed by Value before each statement in a given function (read the functions from bottom to top):

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!@.")

This is far from ideal, and the output is uglier than simply using Cvalue.Model.pretty state, but it could serve as base for further modifications.

This script has been tested with Frama-C Magnesium.

To retrieve the state after a statement, simply replace the ~after:false parameter in fold_state_callstack with ~after:true. My previous version of the code used a function which already bound that value for the pre-state, but no such function is exported for the post-state, so we must use fold_state_callstack (which is incidentally more powerful, because it allows retrieving a specific state per callstack).