Frama-C插件开发：数组信息获取与形参修改技术问询

Hey there! Let's walk through how to build your Frama-C plugin for alias analysis and restrict qualification—this is a great use case, and Frama-C's APIs have you covered.

First, let's split this into static arrays and dynamically allocated pointers, since Frama-C handles them differently:

静态数组（比如int tab[100];） #

Static arrays are represented in CIL as TArray types. When iterating over local variables or function parameters, you can pattern-match on the variable's type to extract key details:

• TArray (elem_typ, Some size_exp, _, _): The second argument is the compile-time size expression (like 100 as an integer literal).
• elem_typ gives you the type of each element (e.g., int for the example above).

动态分配指针（比如float *A = malloc(ni * nk * sizeof(float));） #

For dynamically allocated memory, you'll need to leverage Frama-C's Value Analysis (Db.Value) to get runtime memory information:

1. Use Db.Value.get_state () to retrieve the current analysis state after running Value.
2. Convert the pointer variable to an lvalue with Cil.var v, then use Db.Value.lval_to_zone state lval to get the memory zone the pointer points to.
3. Db.Zone.size zone returns the total size of the allocated memory (in bytes). To get the number of elements, divide this by the size of the pointee type (use Cil.bitsSizeOf typ / 8 to convert bits to bytes).
4. The pointee type comes from the TPtr type: TPtr (pointee_typ, attrs) gives you pointee_typ (e.g., float in the example).

To determine where to add __restrict__, you need to confirm a pointer has no aliases (i.e., no other pointer in scope points to the same memory region).

别名检查方法 #

• Use Value Analysis's alias information: Db.Value.lval_to_zone gives you the memory zone for each pointer. If two zones do not overlap (or one is not a subset of the other), the pointers are not aliased.
• For more precise control, you can also use the Program Dependence Graph (PDG) analysis (Db.Pdg), which tracks dependencies between variables—if a pointer has no data dependencies with other pointers, it's a strong candidate for restrict.

标记__restrict__ #

Once you confirm a pointer has no aliases, modify its type to include the restrict qualifier. In CIL, pointer types (TPtr) have an attribute record with a restrict boolean flag—set this to true to mark the pointer as restricted.

To update a function parameter like int *tmp to int *__restrict__ tmp, follow these steps:

1. Locate the target fundec (CIL's Cil_types.fundec type representing the function).
2. Iterate over its sformals list to find the parameter by name.
3. For the matching parameter, update its vtype from TPtr (typ, attrs) to TPtr (typ, { attrs with restrict = true }).

Here are concrete OCaml snippets to tie this all together:

处理变量（静态数组/动态指针） #

open Cil_types
open Cil_printer

let process_variable (v : varinfo) =
  match v.vtype with
  | TArray (elem_typ, Some size_exp, _, _) ->
      Format.printf "Static array '%s': element type = %a, size = %a@."
        v.vname pp_typ elem_typ pp_exp size_exp
  | TPtr (pointee_typ, attrs) ->
      let state = Db.Value.get_state () in
      let lval = Cil.var v in
      (match Db.Value.lval_to_zone state lval with
       | Some zone ->
           let total_bytes = Db.Zone.size zone in
           let elem_bytes = Cil.bitsSizeOf pointee_typ / 8 in
           let elem_count = total_bytes / elem_bytes in
           Format.printf "Pointer '%s': pointee type = %a, allocated size = %d bytes (%d elements)@."
             v.vname pp_typ pointee_typ total_bytes elem_count
       | None ->
           Format.printf "Pointer '%s': pointee type = %a, no known allocated size@."
             v.vname pp_typ pointee_typ)
  | _ -> ()

检查指针别名 #

let are_pointers_aliased (v1 : varinfo) (v2 : varinfo) =
  let state = Db.Value.get_state () in
  let lval1 = Cil.var v1 in
  let lval2 = Cil.var v2 in
  match Db.Value.lval_to_zone state lval1, Db.Value.lval_to_zone state lval2 with
  | Some z1, Some z2 -> Db.Zone.is_included z1 z2 || Db.Zone.is_included z2 z1
  | _ -> false (* If either zone is unknown, assume potential aliasing *)

添加restrict到函数形参 #

let add_restrict_to_param (f : fundec) (param_name : string) =
  let update_param p =
    if p.vname = param_name then
      match p.vtype with
      | TPtr (typ, attrs) ->
          let new_attrs = { attrs with restrict = true } in
          { p with vtype = TPtr (typ, new_attrs) }
      | _ -> p (* Skip non-pointer parameters *)
    else p
  in
  f.sformals <- List.map update_param f.sformals

插件入口（确保分析运行） #

let () =
  Db.Main.extend (fun () ->
      (* Run Value Analysis first *)
      Db.Value.compute ();
      (* Optional: Run PDG for more precise dependence analysis *)
      Db.Pdg.compute ();

      (* Example: Process the 'test' function *)
      let test_func = Globals.Functions.find_by_name "test" in
      List.iter process_variable test_func.slocals;
      List.iter process_variable test_func.sformals;

      (* Add restrict to 'tmp' parameter if no aliases *)
      let tmp_param = List.find (fun p -> p.vname = "tmp") test_func.sformals in
      let has_aliases = List.exists (fun p -> are_pointers_aliased tmp_param p) test_func.sformals in
      if not has_aliases then
        begin
          add_restrict_to_param test_func "tmp";
          Format.printf "Added __restrict__ to parameter 'tmp' in function 'test'@."
        end
    )

• Make sure your plugin declares dependencies on Value and PDG analyses (Frama-C will handle running them in order if you use Db.Value.compute() and Db.Pdg.compute()).
• For dynamically allocated pointers, Value Analysis might return a range of possible sizes (not an exact value) if the malloc argument is a variable—use Db.Value.eval_exp to get the size expression's possible interval values.
• Always test your plugin on small examples first to verify alias checks and restrict modifications work as expected.

内容的提问来源于stack exchange，提问作者R. Fomba