Source file register.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2023                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Cil_datatype
open Cil
open Visitor
open Options

module Occurrence_datatype =
  Datatype.Triple(Datatype.Option(Kernel_function))(Kinstr)(Lval)

module Occurrences: sig
  val add: varinfo -> kernel_function option -> kinstr -> lval -> unit
  val get: varinfo -> (kernel_function option * kinstr * lval) list
  val self: State.t
  val get_last_result: unit ->
    ((Kernel_function.t option * Cil_types.kinstr *
      (Cil_types.lhost * Cil_types.offset))
       list * Cil_types.varinfo)
      option
  val iter_sorted:
    (varinfo -> (kernel_function option * kinstr * lval) list -> unit) -> unit
end = struct

  module IState =
    Cil_state_builder.Varinfo_hashtbl
      (Occurrence_datatype)
      (struct
        let size = 17
        let name = "Occurrences.State"
        let dependencies = [ Eva.Analysis.self ]
      end)

  module LastResult =
    State_builder.Option_ref
      (Varinfo)
      (struct
        let name = "Occurrences.LastResult"
        let dependencies = [ Ast.self; IState.self ]
      end)

  let add vi kf ki lv = IState.add vi (kf, ki, lv)

  let unsafe_get vi = try IState.find_all vi with Not_found -> []

  let get vi =
    LastResult.set vi;
    unsafe_get vi

  let get_last_result () =
    try
      let vi = LastResult.get () in
      Some (unsafe_get vi, vi)
    with Not_found ->
      None

  let iter_aux fold f =
    let old, l =
      fold
        (fun v elt (old, l) -> match v, old with
           | v, None ->
             assert (l = []);
             Some v, [ elt ]
           | v, (Some old as some) when Varinfo.equal v old ->
             some, elt :: l
           | v, Some old ->
             f old l;
             Some v, [ elt ])
        (None, [])
    in
    Option.iter (fun v -> f v l) old

  let fold_sorted f init =
    let map = IState.fold Varinfo.Map.add Varinfo.Map.empty in
    Varinfo.Map.fold f map init

  let iter_sorted = iter_aux fold_sorted

  let self = IState.self

end

class occurrence = object (self)

  inherit Visitor.frama_c_inplace as super

  method! vlval lv =
    let ki = self#current_kinstr in
    begin
      let z = Eva.Results.(before_kinstr ki |> eval_address lv |> as_zone) in
      try
        Locations.Zone.fold_topset_ok
          (fun b _ () ->
             match b with
             | Base.Var (vi, _) | Base.Allocated (vi, _, _) ->
               Occurrences.add vi self#current_kf ki lv
             | _ -> ()
          ) z ()
      with Abstract_interp.Error_Top ->
        error ~current:true "Found completely imprecise value (%a). Ignoring@."
          Printer.pp_lval lv
    end;
    DoChildren

  method! vterm_lval tlv =
    (try
       let lv = Logic_to_c.term_lval_to_lval tlv in
       ignore (self#vlval lv)
     with
     (* Translation to lval failed.*)
     | Logic_to_c.No_conversion -> ());
    DoChildren

  method! vstmt_aux s =
    Db.yield ();
    super#vstmt_aux s

  initializer Eva.Analysis.compute ()

end

type access_type = Read | Write | Both

(** Try to find [lv] somewhere within a Cil value *)
class is_sub_lval lv = object
  inherit Cil.nopCilVisitor

  method! vlval lv' =
    if Cil_datatype.Lval.equal lv lv' then raise Exit;
    DoChildren
end

(** Occurrence has found the given [lv] somewhere inside [ki]. We try to find
    whether this was inside a read or a write operation. This is difficult to
    do directly inside the {!occurrence} class, as the [vlval] method
    has no information about the origin of the lval it was called on *)
let classify_accesses (_kf, ki, lv) =
  let vis = new is_sub_lval lv in
  let aux f v = try ignore (f vis v); false with Exit -> true in
  let is_lv = Cil_datatype.Lval.equal lv in
  let contained_exp = aux Cil.visitCilExpr in
  match ki with
  | Kglobal -> (* Probably initializers *) Read

  | Kstmt { skind = Instr i } ->
    (match i with
     | Set (lv', e, _) ->
       if is_lv lv' then
         if contained_exp e then Both
         else Write
       else Read

     | Call (Some lv', f, args, _) ->
       if is_lv lv' then
         if contained_exp f || List.exists contained_exp args then Both
         else Write
       else Read

     | Local_init (v, _, _) ->
       (match lv with
        | Var v', _ when Cil_datatype.Varinfo.equal v v' ->
          (* We are initializing v. We can't read from it at the same time.
             Hence, there's no need to perform the additional checks done
             in the cases above. *)
          Write
        | _ -> Read)

     | Asm (_, _, Some { asm_outputs; asm_inputs },_) ->
       if List.exists (fun (_, _, out) -> is_lv out) asm_outputs then
         if List.exists (fun (_, _, inp) -> contained_exp inp) asm_inputs
         then Both
         else Write
       else Read

     | _ -> Read)
  | _ -> Read

let compute, _self =
  let run () =
    feedback "beginning analysis";
    ignore (visitFramacFile (new occurrence) (Ast.get ()));
    feedback "analysis done"
  in
  State_builder.apply_once "Occurrence.compute" [ Occurrences.self ] run

let get vi =
  compute ();
  try Occurrences.get vi with Not_found -> assert false

let d_ki fmt = function
  | None, Kglobal -> Format.fprintf fmt "global"
  | Some kf, Kglobal ->
    Format.fprintf fmt "specification of %a" Kernel_function.pretty kf
  | _, Kstmt s -> Format.fprintf fmt "sid %d" s.sid

let print_one fmt v l =
  Format.fprintf fmt "variable %s (%s):@\n"
    v.vname
    (if v.vglob then "global"
     else
       let kf_name = match l with
         | [] -> assert false
         | (Some kf, _, _) :: _ -> Kernel_function.get_name kf
         | (None,Kstmt _,_)::_ -> assert false
         | (None,Kglobal,_)::_ ->
           fatal "inconsistent context for occurrence of variable %s" v.vname
       in
       if v.vformal then "parameter of " ^ kf_name
       else "local of " ^ kf_name);
  List.iter
    (fun (kf, ki, lv) ->
       Format.fprintf fmt "  %a: %a@\n" d_ki (kf,ki) Printer.pp_lval lv) l

let print_all () =
  compute ();
  result "%t" (fun fmt -> Occurrences.iter_sorted (print_one fmt))

(* ************************************************************************** *)
(* Exported API *)
(* ************************************************************************** *)

let self = Occurrences.self
let get_last_result = Occurrences.get_last_result
let get = get
let print_all = print_all

(* ************************************************************************** *)
(* Main *)
(* ************************************************************************** *)

let main _fmt = if Print.get () then print_all ()
let () = Db.Main.extend main

(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)