From 74faebf4b46d52b2ec0425da32eeede5aaf9e46e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 24 Sep 2021 11:38:46 +0200
Subject: [PATCH] [kernel] Moves function [loc_to_localizable] from the gui
plugin to the kernel.
This function returns the most precise localizable that contains the given
Filepath.position. It is now also needed by the server plugin.
---
.../ast_printing/printer_tag.ml | 206 ++++++++++++++++++
.../ast_printing/printer_tag.mli | 6 +
src/plugins/gui/design.ml | 2 +-
src/plugins/gui/history.ml | 2 +-
src/plugins/gui/pretty_source.ml | 203 -----------------
src/plugins/gui/pretty_source.mli | 7 -
src/plugins/gui/source_manager.ml | 2 +-
7 files changed, 215 insertions(+), 213 deletions(-)
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 4f07c37e146..c8cc00fef64 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -244,6 +244,212 @@ let loc_of_localizable = function
| None -> Location.unknown
| Some kf -> Kernel_function.get_location kf)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Find localizable at a Filepath.position --- *)
+(* -------------------------------------------------------------------------- *)
+
+let dkey = Kernel.register_category "pretty-source"
+
+module LineToLocalizable =
+ Datatype.Hashtbl(Datatype.Int.Hashtbl)(Datatype.Int)
+ (struct let module_name = "Pretty_source.LineToLocalizable" end)
+module FileToLines =
+ Datatype.Hashtbl(Datatype.Filepath.Hashtbl)(Datatype.Filepath)
+ (struct let module_name = "Pretty_source.FilesToLine" end)
+
+module MappingLineLocalizable = struct
+ module LineToLocalizableAux =
+ LineToLocalizable.Make( Datatype.Pair(Location)(Localizable))
+
+ include State_builder.Hashtbl(FileToLines)(LineToLocalizableAux)
+ (struct
+ let size = 5
+ let dependencies = [Ast.self]
+ let name = "Pretty_source.line_to_localizable"
+ end)
+end
+
+class pos_to_localizable =
+ object (self)
+ inherit Visitor.frama_c_inplace
+
+ (* used to keep track of conditional expressions, to add them to the
+ list of relevant localizables *)
+ val mutable insideIf = None
+
+ method add_range loc (localizable : localizable) =
+ if not (Location.equal loc Location.unknown) then (
+ let p1, p2 = loc in
+ if p1.Filepath.pos_path <> p2.Filepath.pos_path then
+ Kernel.debug ~once:true ~dkey
+ "Localizable over two files: %a and %a; %a"
+ Datatype.Filepath.pretty p1.Filepath.pos_path
+ Datatype.Filepath.pretty p2.Filepath.pos_path
+ Localizable.pretty localizable;
+ let file = p1.Filepath.pos_path in
+ let hfile =
+ try MappingLineLocalizable.find file
+ with Not_found ->
+ let h = LineToLocalizable.create 17 in
+ MappingLineLocalizable.add file h;
+ h
+ in
+ for i = p1.Filepath.pos_lnum to p2.Filepath.pos_lnum do
+ LineToLocalizable.add hfile i (loc, localizable);
+ done
+ );
+
+ method! vstmt_aux s =
+ (* we ignore Block statements, since they tend to overlap existing
+ ones which are more precise *)
+ let skip = match s.skind with
+ | Block _ -> true
+ | _ -> false
+ in
+ if not skip then
+ self#add_range (Stmt.loc s) (PStmt (Option.get self#current_kf, s));
+ begin
+ match s.skind with
+ | If (exp, _, _, _) ->
+ (* conditional expressions are treated in a special way *)
+ insideIf <- Some (Kstmt s);
+ ignore (Cil.visitCilExpr (self :> Cil.cilVisitor) exp);
+ insideIf <- None
+ | _ -> ()
+ end;
+ Cil.DoChildren
+
+ method! vexpr exp =
+ begin
+ match insideIf with
+ | Some ki ->
+ (* expressions inside conditionals have a special treatment *)
+ begin
+ match exp.enode with
+ | Lval lv ->
+ (* lvals must be generated differently from other expressions *)
+ self#add_range exp.eloc (PLval(self#current_kf, ki, lv))
+ | _ ->
+ self#add_range exp.eloc (PExp(self#current_kf, ki, exp))
+ end
+ | None -> ()
+ end;
+ Cil.DoChildren
+
+ method! vvdec vi =
+ if not vi.vglob && not vi.vtemp then
+ begin
+ match self#current_kf with
+ | None -> (* should not happen*) ()
+ | Some kf ->
+ self#add_range vi.vdecl (PVDecl (Some kf,self#current_kinstr,vi));
+ end;
+ Cil.DoChildren
+
+ method! vglob_aux g =
+ (match g with
+ | GFun ({ svar = vi }, loc) ->
+ self#add_range loc
+ (PVDecl (Some (Globals.Functions.get vi), Kglobal, vi))
+ | GVar (vi, _, loc) ->
+ self#add_range loc (PVDecl (None, Kglobal, vi))
+ | GFunDecl (_, vi, loc) ->
+ self#add_range loc
+ (PVDecl (Some (Globals.Functions.get vi), Kglobal, vi))
+ | GVarDecl (vi, loc) ->
+ self#add_range loc (PVDecl (None, Kglobal, vi))
+ | _ -> self#add_range (Global.loc g) (PGlobal g)
+ );
+ Cil.DoChildren
+ end
+
+(* Returns [true] if the column [col] is within location [loc]. *)
+let location_contains_col loc col =
+ let (pos_start, pos_end) = loc in
+ let (col_start, col_end) =
+ pos_start.Filepath.pos_cnum - pos_start.Filepath.pos_bol,
+ pos_end.Filepath.pos_cnum - pos_end.Filepath.pos_bol
+ in
+ col_start <= col && col <= col_end
+
+(* Applies several heuristics to try and match the best localizable to a
+ given location [loc]. The list [possible_locs] should contain all
+ localizables in a given line. If [possible_col] is [true], then we try
+ to take column information into account.
+ Some heuristics may return an empty list, in which case a fallback is
+ later used to return a better choice. *)
+let apply_location_heuristics precise_col possible_locs loc =
+ let col = loc.Filepath.pos_cnum - loc.Filepath.pos_bol in
+ Kernel.debug ~dkey
+ "apply_location_heuristics (precise_col:%b): loc: %a, col: %d@\n\
+ possible_locs:@ %a"
+ precise_col Location.pretty (loc, loc) col
+ (Pretty_utils.pp_list ~sep:"@\n"
+ (Pretty_utils.pp_pair ~sep:" :: " Location.pretty Localizable.pretty)) possible_locs;
+ (* Heuristic 1: we try to obtain a subset of localizables related to a given
+ position, or a given column if [precise_col] is true.
+ May result in an empty list. *)
+ let filter_locs l =
+ List.filter (fun (((pos_start, _) as loc'), _) ->
+ if precise_col then location_contains_col loc' col
+ else loc = pos_start
+ ) l
+ in
+ (* Heuristic 2: prioritize expressions if they are present.
+ May result in an empty list. *)
+ let exps l =
+ List.filter (fun (_, lz) -> match lz with | PExp _ -> true | _ -> false) l
+ in
+ (* Heuristic 3: when we have more than one match with the exact same location,
+ we pick the last one in the list. This will be the first statement that has
+ been encountered, and this criterion seems to work well with temporaries
+ introduced by Cil. *)
+ let last l = match List.rev l with [] -> None | (_, lz) :: _ -> Some lz in
+ (* Heuristic 4: when there are no exact locations, we will consider the
+ innermost ones, that is, those at the top of the list. *)
+ let innermost_in loc l =
+ List.filter (fun (loc', _) -> Location.equal loc loc') l
+ in
+ match possible_locs, filter_locs possible_locs with
+ | [], _ -> (* no possible localizables *) None
+ | _, (_ :: _ as exact) ->
+ (* one or more exact localizables; we prioritize expressions *)
+ begin
+ match exps exact with
+ | [] -> (* no expressions, just take the last localizable *) last exact
+ | exps -> (* take the last (usually only) expression *) last exps
+ end
+ | (loc', _) :: __, [] ->
+ (* No exact loc. We consider the innermost statements,
+ ie those at the top of the list *)
+ let filtered = innermost_in loc' possible_locs in
+ last filtered
+
+let loc_to_localizable ?(precise_col=false) loc =
+ if not (MappingLineLocalizable.is_computed ()) then (
+ let vis = new pos_to_localizable in
+ Visitor.visitFramacFile (vis :> Visitor.frama_c_visitor) (Ast.get ());
+ MappingLineLocalizable.mark_as_computed ();
+ );
+ try
+ (* Find the mapping from this file to locs-by-line *)
+ let hfile = MappingLineLocalizable.find loc.Filepath.pos_path in
+ (* Find the localizable for this line *)
+ let all = LineToLocalizable.find_all hfile loc.Filepath.pos_lnum in
+ match apply_location_heuristics precise_col all loc with
+ | Some locz ->
+ Kernel.feedback ~dkey "loc: %a -> locz: %a"
+ Location.pretty (loc,loc) Localizable.pretty locz;
+ Some locz
+ | None ->
+ Kernel.feedback ~dkey "loc: %a -> NO locz" Location.pretty (loc,loc);
+ None
+ with
+ | Not_found ->
+ Kernel.debug ~once:true ~source:loc "no matching localizable found";
+ None
+
(* -------------------------------------------------------------------------- *)
(* --- Printer API --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/kernel_services/ast_printing/printer_tag.mli b/src/kernel_services/ast_printing/printer_tag.mli
index a35466dfc72..4f67fdebedb 100644
--- a/src/kernel_services/ast_printing/printer_tag.mli
+++ b/src/kernel_services/ast_printing/printer_tag.mli
@@ -62,6 +62,12 @@ val typ_of_localizable: localizable -> typ option
val loc_of_localizable : localizable -> location
(** Might return [Location.unknown] *)
+val loc_to_localizable: ?precise_col:bool -> Filepath.position -> localizable option
+(** return the (hopefully) most precise localizable that contains the given
+ Filepath.position. If [precise_col] is [true], takes the column number into
+ account (possibly a more precise, but costly, result).
+ @since Frama-C+dev *)
+
module type Tag =
sig
val create : localizable -> string
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 1c516ca0d95..1d24782c859 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1697,7 +1697,7 @@ class main_window () : main_window_extension_points =
let callback e _column =
Option.iter
(fun pos ->
- Option.iter self#scroll (Pretty_source.loc_to_localizable pos);
+ Option.iter self#scroll (Printer_tag.loc_to_localizable pos);
(* Note: the code below generates double scrolling:
the previous call to self#scroll causes the original source
viewer to scroll to the beginning of the function, and then
diff --git a/src/plugins/gui/history.ml b/src/plugins/gui/history.ml
index be4771062cb..d6c84731ce8 100644
--- a/src/plugins/gui/history.ml
+++ b/src/plugins/gui/history.ml
@@ -276,7 +276,7 @@ let translate_history_elt old_helt =
Filepath.pos_cnum = old_loc.Filepath.pos_cnum;
}
in
- match Pretty_source.loc_to_localizable new_loc with
+ match Printer_tag.loc_to_localizable new_loc with
| None -> (** the line is unknown *)
Some (Global g)
| Some locali ->
diff --git a/src/plugins/gui/pretty_source.ml b/src/plugins/gui/pretty_source.ml
index c2aa878bbe0..a2852f171ab 100644
--- a/src/plugins/gui/pretty_source.ml
+++ b/src/plugins/gui/pretty_source.ml
@@ -22,7 +22,6 @@
open Cil_types
open Gtk_helper
-open Cil_datatype
open Printer_tag
type localizable = Printer_tag.localizable =
@@ -41,8 +40,6 @@ type localizable = Printer_tag.localizable =
definitions. *)
| PIP of Property.t
-let dkey = Gui_parameters.register_category "pretty-source"
-
let kf_of_localizable = Printer_tag.kf_of_localizable
let ki_of_localizable = Printer_tag.ki_of_localizable
let varinfo_of_localizable = Printer_tag.varinfo_of_localizable
@@ -419,206 +416,6 @@ let display_source globals
(fun () -> GtkSignal.disconnect event_tag#as_tag id);
)
-
-module LineToLocalizable =
- Datatype.Hashtbl(Datatype.Int.Hashtbl)(Datatype.Int)
- (struct let module_name = "Pretty_source.LineToLocalizable" end)
-module FileToLines =
- Datatype.Hashtbl(Datatype.Filepath.Hashtbl)(Datatype.Filepath)
- (struct let module_name = "Pretty_source.FilesToLine" end)
-
-module MappingLineLocalizable = struct
- module LineToLocalizableAux =
- LineToLocalizable.Make( Datatype.Pair(Location)(Localizable))
-
- include State_builder.Hashtbl(FileToLines)(LineToLocalizableAux)
- (struct
- let size = 5
- let dependencies = [Ast.self]
- let name = "Pretty_source.line_to_localizable"
- end)
-end
-
-class pos_to_localizable =
- object (self)
- inherit Visitor.frama_c_inplace
-
- (* used to keep track of conditional expressions, to add them to the
- list of relevant localizables *)
- val mutable insideIf = None
-
- method add_range loc (localizable : localizable) =
- if not (Location.equal loc Location.unknown) then (
- let p1, p2 = loc in
- if p1.Filepath.pos_path <> p2.Filepath.pos_path then
- Gui_parameters.debug ~once:true
- "Localizable over two files: %a and %a; %a"
- Datatype.Filepath.pretty p1.Filepath.pos_path
- Datatype.Filepath.pretty p2.Filepath.pos_path
- Localizable.pretty localizable;
- let file = p1.Filepath.pos_path in
- let hfile =
- try MappingLineLocalizable.find file
- with Not_found ->
- let h = LineToLocalizable.create 17 in
- MappingLineLocalizable.add file h;
- h
- in
- for i = p1.Filepath.pos_lnum to p2.Filepath.pos_lnum do
- LineToLocalizable.add hfile i (loc, localizable);
- done
- );
-
- method! vstmt_aux s =
- (* we ignore Block statements, since they tend to overlap existing
- ones which are more precise *)
- let skip = match s.skind with
- | Block _ -> true
- | _ -> false
- in
- if not skip then
- self#add_range (Stmt.loc s) (PStmt (Option.get self#current_kf, s));
- begin
- match s.skind with
- | If (exp, _, _, _) ->
- (* conditional expressions are treated in a special way *)
- insideIf <- Some (Kstmt s);
- ignore (Cil.visitCilExpr (self :> Cil.cilVisitor) exp);
- insideIf <- None
- | _ -> ()
- end;
- Cil.DoChildren
-
- method! vexpr exp =
- begin
- match insideIf with
- | Some ki ->
- (* expressions inside conditionals have a special treatment *)
- begin
- match exp.enode with
- | Lval lv ->
- (* lvals must be generated differently from other expressions *)
- self#add_range exp.eloc (PLval(self#current_kf, ki, lv))
- | _ ->
- self#add_range exp.eloc (PExp(self#current_kf, ki, exp))
- end
- | None -> ()
- end;
- Cil.DoChildren
-
- method! vvdec vi =
- if not vi.vglob && not vi.vtemp then
- begin
- match self#current_kf with
- | None -> (* should not happen*) ()
- | Some kf ->
- self#add_range vi.vdecl (PVDecl (Some kf,self#current_kinstr,vi));
- end;
- Cil.DoChildren
-
- method! vglob_aux g =
- (match g with
- | GFun ({ svar = vi }, loc) ->
- self#add_range loc
- (PVDecl (Some (Globals.Functions.get vi), Kglobal, vi))
- | GVar (vi, _, loc) ->
- self#add_range loc (PVDecl (None, Kglobal, vi))
- | GFunDecl (_, vi, loc) ->
- self#add_range loc
- (PVDecl (Some (Globals.Functions.get vi), Kglobal, vi))
- | GVarDecl (vi, loc) ->
- self#add_range loc (PVDecl (None, Kglobal, vi))
- | _ -> self#add_range (Global.loc g) (PGlobal g)
- );
- Cil.DoChildren
- end
-
-(* Returns [true] if the column [col] is within location [loc]. *)
-let location_contains_col loc col =
- let (pos_start, pos_end) = loc in
- let (col_start, col_end) =
- pos_start.Filepath.pos_cnum - pos_start.Filepath.pos_bol,
- pos_end.Filepath.pos_cnum - pos_end.Filepath.pos_bol
- in
- col_start <= col && col <= col_end
-
-(* Applies several heuristics to try and match the best localizable to a
- given location [loc]. The list [possible_locs] should contain all
- localizables in a given line. If [possible_col] is [true], then we try
- to take column information into account.
- Some heuristics may return an empty list, in which case a fallback is
- later used to return a better choice. *)
-let apply_location_heuristics precise_col possible_locs loc =
- let col = loc.Filepath.pos_cnum - loc.Filepath.pos_bol in
- Gui_parameters.debug ~dkey
- "apply_location_heuristics (precise_col:%b): loc: %a, col: %d@\n\
- possible_locs:@ %a"
- precise_col Location.pretty (loc, loc) col
- (Pretty_utils.pp_list ~sep:"@\n"
- (Pretty_utils.pp_pair ~sep:" :: " Location.pretty Localizable.pretty)) possible_locs;
- (* Heuristic 1: we try to obtain a subset of localizables related to a given
- position, or a given column if [precise_col] is true.
- May result in an empty list. *)
- let filter_locs l =
- List.filter (fun (((pos_start, _) as loc'), _) ->
- if precise_col then location_contains_col loc' col
- else loc = pos_start
- ) l
- in
- (* Heuristic 2: prioritize expressions if they are present.
- May result in an empty list. *)
- let exps l =
- List.filter (fun (_, lz) -> match lz with | PExp _ -> true | _ -> false) l
- in
- (* Heuristic 3: when we have more than one match with the exact same location,
- we pick the last one in the list. This will be the first statement that has
- been encountered, and this criterion seems to work well with temporaries
- introduced by Cil. *)
- let last l = match List.rev l with [] -> None | (_, lz) :: _ -> Some lz in
- (* Heuristic 4: when there are no exact locations, we will consider the
- innermost ones, that is, those at the top of the list. *)
- let innermost_in loc l =
- List.filter (fun (loc', _) -> Location.equal loc loc') l
- in
- match possible_locs, filter_locs possible_locs with
- | [], _ -> (* no possible localizables *) None
- | _, (_ :: _ as exact) ->
- (* one or more exact localizables; we prioritize expressions *)
- begin
- match exps exact with
- | [] -> (* no expressions, just take the last localizable *) last exact
- | exps -> (* take the last (usually only) expression *) last exps
- end
- | (loc', _) :: __, [] ->
- (* No exact loc. We consider the innermost statements,
- ie those at the top of the list *)
- let filtered = innermost_in loc' possible_locs in
- last filtered
-
-let loc_to_localizable ?(precise_col=false) loc =
- if not (MappingLineLocalizable.is_computed ()) then (
- let vis = new pos_to_localizable in
- Visitor.visitFramacFile (vis :> Visitor.frama_c_visitor) (Ast.get ());
- MappingLineLocalizable.mark_as_computed ();
- );
- try
- (* Find the mapping from this file to locs-by-line *)
- let hfile = MappingLineLocalizable.find loc.Filepath.pos_path in
- (* Find the localizable for this line *)
- let all = LineToLocalizable.find_all hfile loc.Filepath.pos_lnum in
- match apply_location_heuristics precise_col all loc with
- | Some locz ->
- Gui_parameters.feedback ~dkey "loc: %a -> locz: %a"
- Location.pretty (loc,loc) Localizable.pretty locz;
- Some locz
- | None ->
- Gui_parameters.feedback ~dkey "loc: %a -> NO locz" Location.pretty (loc,loc);
- None
- with
- | Not_found ->
- Gui_parameters.debug ~once:true ~source:loc "no matching localizable found";
- None
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/gui/pretty_source.mli b/src/plugins/gui/pretty_source.mli
index a3544e647fb..96e25243efb 100644
--- a/src/plugins/gui/pretty_source.mli
+++ b/src/plugins/gui/pretty_source.mli
@@ -88,13 +88,6 @@ val localizable_from_locs :
This function is inefficient as it iterates on all the current
[Locs.state]. *)
-val loc_to_localizable: ?precise_col:bool -> Filepath.position -> localizable option
-(** return the (hopefully) most precise localizable that contains the given
- Filepath.position. If [precise_col] is [true], takes the column number into
- account (possibly a more precise, but costly, result).
- @since Nitrogen-20111001 *)
-
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/gui/source_manager.ml b/src/plugins/gui/source_manager.ml
index d3d25091072..7a99892c460 100644
--- a/src/plugins/gui/source_manager.ml
+++ b/src/plugins/gui/source_manager.ml
@@ -171,7 +171,7 @@ let load_file w ?title ~(filename : Datatype.Filepath.t) ?(line=(-1)) ~click_cb
Filepath.pos_bol = offset - col;
Filepath.pos_cnum = offset;} in
let localz =
- Pretty_source.loc_to_localizable ~precise_col:true pos
+ Printer_tag.loc_to_localizable ~precise_col:true pos
in
click_cb localz
with Not_found ->
--
GitLab