Skip to content
Snippets Groups Projects
Commit d18736f1 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Removes file eva_types.ml from kernel.

parent eb3252b5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/kernel_services/abstract_interp/eva_types.ml deleted 100644 → 0
+ 0
− 188
View file @ eb3252b5
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
let stable_hash x = Hashtbl.seeded_hash 0 x
let dkey_callstack = Kernel.register_category "callstack"
module Callstack =
struct
module Thread = Int (* Threads are identified by integers *)
module Kf = Kernel_function
module Stmt = Cil_datatype.Stmt
module Var = Cil_datatype.Varinfo
module Call = Datatype.Pair_with_collections(Kf)(Stmt)
(struct let module_name = "Eva.Callstack.Call" end)
module Calls = Datatype.List (Call)
type callstack = {
thread: int;
entry_point: Kernel_function.t;
stack: Call.t list;
}
module Prototype =
struct
include Datatype.Serializable_undefined
type t = callstack = {
thread: int;
entry_point: Kernel_function.t;
stack: Call.t list;
}
[@@deriving eq, ord]
let name = "Eva.Callstack"
let reprs =
List.concat_map (fun stack ->
List.map (fun entry_point -> { thread = 0; entry_point; stack })
Kernel_function.reprs)
Calls.reprs
let pretty fmt cs =
let pp_call fmt (kf,stmt) =
Format.fprintf fmt "%a :: %a <-@ "
Kf.pretty kf
Cil_datatype.Location.pretty (Stmt.loc stmt)
in
Format.fprintf fmt "@[<hv>";
List.iter (pp_call fmt) cs.stack;
Format.fprintf fmt "%a@]" Kernel_function.pretty cs.entry_point
let hash cs =
Hashtbl.hash
(cs.thread, Kernel_function.hash cs.entry_point, Calls.hash cs.stack)
end
type call = Call.t
include Datatype.Make_with_collections (Prototype)
let pretty_debug = pretty
let compare_lex cs1 cs2 =
if cs1 == cs2 then 0 else
let c = Thread.compare cs1.thread cs2.thread in
if c <> 0 then c else
let c = Kernel_function.compare cs1.entry_point cs2.entry_point in
if c <> 0 then c else
Calls.compare (List.rev cs1.stack) (List.rev cs2.stack)
(* Stack manipulation *)
let init ?(thread=0) kf = { thread; entry_point=kf; stack = [] }
let push kf stmt cs =
{ cs with stack = (kf, stmt) :: cs.stack }
let pop cs =
match cs.stack with
| [] -> None
| _ :: tail -> Some { cs with stack = tail }
let top cs =
match cs.stack with
| [] -> None
| (kf, stmt) :: _ -> Some (kf, stmt)
let top_kf cs =
match cs.stack with
| (kf, _stmt) :: _ -> kf
| [] -> cs.entry_point
let top_callsite cs =
match cs.stack with
| [] -> Cil_types.Kglobal
| (_kf, stmt) :: _ -> Cil_types.Kstmt stmt
let top_call cs =
match cs.stack with
| (kf, stmt) :: _ -> kf, Cil_types.Kstmt stmt
| [] -> cs.entry_point, Cil_types.Kglobal
let top_caller cs =
match cs.stack with
| _ :: (kf, _) :: _ -> Some kf
| [_] -> Some cs.entry_point
| [] -> None
(* Conversion *)
let to_kf_list cs = cs.entry_point :: List.rev_map fst cs.stack
let to_stmt_list cs = List.rev_map snd cs.stack
let to_call_list cs =
let l =
List.rev_map (fun (kf, stmt) -> (kf, Cil_types.Kstmt stmt)) cs.stack
in
(cs.entry_point, Cil_types.Kglobal) :: l
(* Stable hash and pretty-printing *)
let stmt_hash s =
let pos = fst (Cil_datatype.Stmt.loc s) in
stable_hash (pos.Filepath.pos_path, pos.Filepath.pos_lnum)
let kf_hash kf = stable_hash (Kernel_function.get_name kf)
let rec calls_hash = function
| [] -> 0
| (kf, stmt) :: tl -> stable_hash (kf_hash kf, stmt_hash stmt, calls_hash tl)
let stable_hash { thread; entry_point; stack } =
let p = stable_hash (thread, kf_hash entry_point, calls_hash stack) in
p mod 11_316_496 (* 58 ** 4 *)
let base58_map = "123456789ABCDEFGHJKLMNPQRSTUVWXYZabcdefghijkmnopqrstuvwxyz"
(* Converts [i] into a fixed-length, 4-wide string in base-58 *)
let base58_of_int n =
let buf = Bytes.create 4 in
Bytes.set buf 0 (String.get base58_map (n mod 58));
let n = n / 58 in
Bytes.set buf 1 (String.get base58_map (n mod 58));
let n = n / 58 in
Bytes.set buf 2 (String.get base58_map (n mod 58));
let n = n / 58 in
Bytes.set buf 3 (String.get base58_map (n mod 58));
Bytes.to_string buf
let pretty_hash fmt callstack =
if Kernel.is_debug_key_enabled dkey_callstack then
Format.fprintf fmt "<%s> " (base58_of_int (stable_hash callstack))
else Format.ifprintf fmt ""
let pretty_short fmt callstack =
Format.fprintf fmt "%a" pretty_hash callstack;
let list = List.rev (to_kf_list callstack) in
Pretty_utils.pp_flowlist ~left:"" ~sep:" <- " ~right:""
(fun fmt kf -> Kernel_function.pretty fmt kf)
fmt list
let pretty fmt callstack =
Format.fprintf fmt "@[<hv>%a" pretty_hash callstack;
pretty fmt callstack;
Format.fprintf fmt "@]"
end
src/kernel_services/abstract_interp/eva_types.mli deleted 100644 → 0
+ 0
− 63
View file @ eb3252b5
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
(** This module is here for compatibility reasons only and will be removed in
future versions. Use [Eva.Callstack] instead *)
module Callstack :
sig
type call = Cil_types.kernel_function * Cil_types.stmt
module Call : Datatype.S with type t = call
type callstack = {
thread: int;
entry_point: Cil_types.kernel_function;
stack: call list;
}
include Datatype.S_with_collections with type t = callstack
val pretty_hash : Format.formatter -> t -> unit
val pretty_short : Format.formatter -> t -> unit
val pretty_debug : Format.formatter -> t -> unit
val compare_lex : t -> t -> int
val init : ?thread:int -> Cil_types.kernel_function -> t
val push : Cil_types.kernel_function -> Cil_types.stmt -> t -> t
val pop : t -> t option
val top : t -> (Cil_types.kernel_function * Cil_types.stmt) option
val top_kf : t -> Cil_types.kernel_function
val top_callsite : t -> Cil_types.kinstr
val top_call : t -> Cil_types.kernel_function * Cil_types.kinstr
val top_caller : t -> Cil_types.kernel_function option
val to_kf_list : t -> Cil_types.kernel_function list
val to_stmt_list : t -> Cil_types.stmt list
val to_call_list : t -> (Cil_types.kernel_function * Cil_types.kinstr) list
end
[@@alert db_deprecated
"Eva_types is only provided for compatibility reason and will be removed \
in a future version of Frama-C. Please use the Eva.Callstack in the \
public API instead."]
src/plugins/eva/Eva.mli
+ 2
− 4
View file @ d18736f1
...@@ -124,7 +124,7 @@ module Callstack: sig ...@@ -124,7 +124,7 @@ module Callstack: sig
module Call : Datatype.S with type t = call module Call : Datatype.S with type t = call
(** Eva callstacks. *) (** Eva callstacks. *)
type callstack = Eva_types.Callstack.callstack = { type callstack = {
thread: int; thread: int;
(* An identifier of the thread's callstack. *) (* An identifier of the thread's callstack. *)
entry_point: Cil_types.kernel_function; entry_point: Cil_types.kernel_function;
...@@ -133,9 +133,7 @@ module Callstack: sig ...@@ -133,9 +133,7 @@ module Callstack: sig
(** A call stack is a list of calls. The head is the latest call. *) (** A call stack is a list of calls. The head is the latest call. *)
} }
include Datatype.S_with_collections include Datatype.S_with_collections with type t = callstack
with type t = callstack
and module Hashtbl = Eva_types.Callstack.Hashtbl
(** Prints a callstack without displaying call sites. *) (** Prints a callstack without displaying call sites. *)
val pretty_short : Format.formatter -> t -> unit val pretty_short : Format.formatter -> t -> unit
......
src/plugins/eva/dune
+ 4
− 1
View file @ d18736f1
...@@ -26,6 +26,8 @@ ...@@ -26,6 +26,8 @@
(action (action
(progn (progn
(echo "EVA:" %{lib-available:frama-c-eva.core} "\n") (echo "EVA:" %{lib-available:frama-c-eva.core} "\n")
(echo " - ppx_deriving.eq:" %{lib-available:ppx_deriving.eq} "\n")
(echo " - ppx_deriving.ord:" %{lib-available:ppx_deriving.ord} "\n")
(echo "Numerors:" %{lib-available:frama-c-eva.numerors.core} "\n") (echo "Numerors:" %{lib-available:frama-c-eva.numerors.core} "\n")
(echo " - MLMPFR:" %{lib-available:mlmpfr} "\n") (echo " - MLMPFR:" %{lib-available:mlmpfr} "\n")
(echo "Apron domains:" %{lib-available:frama-c-eva.apron.core} "\n") (echo "Apron domains:" %{lib-available:frama-c-eva.apron.core} "\n")
...@@ -41,7 +43,8 @@ ...@@ -41,7 +43,8 @@
(flags -open Frama_c_kernel :standard -w -9 -alert -db_deprecated) (flags -open Frama_c_kernel :standard -w -9 -alert -db_deprecated)
(libraries frama-c.kernel frama-c-server.core) (libraries frama-c.kernel frama-c-server.core)
(instrumentation (backend landmarks)) (instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx))) (instrumentation (backend bisect_ppx))
(preprocess (staged_pps ppx_deriving.eq ppx_deriving.ord)))
(plugin (plugin
(name eva) (name eva)
......
src/plugins/eva/types/callstack.ml
+ 163
− 1
View file @ d18736f1
...@@ -20,4 +20,166 @@ ...@@ -20,4 +20,166 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
include Eva_types.Callstack let stable_hash x = Hashtbl.seeded_hash 0 x
let dkey_callstack = Kernel.register_category "callstack"
module Thread = Int (* Threads are identified by integers *)
module Kf = Kernel_function
module Stmt = Cil_datatype.Stmt
module Var = Cil_datatype.Varinfo
module Call = Datatype.Pair_with_collections(Kf)(Stmt)
(struct let module_name = "Eva.Callstack.Call" end)
module Calls = Datatype.List (Call)
type callstack = {
thread: int;
entry_point: Kernel_function.t;
stack: Call.t list;
}
module Prototype =
struct
include Datatype.Serializable_undefined
type t = callstack = {
thread: int;
entry_point: Kernel_function.t;
stack: Call.t list;
}
[@@deriving eq, ord]
let name = "Eva.Callstack"
let reprs =
List.concat_map (fun stack ->
List.map (fun entry_point -> { thread = 0; entry_point; stack })
Kernel_function.reprs)
Calls.reprs
let pretty fmt cs =
let pp_call fmt (kf,stmt) =
Format.fprintf fmt "%a :: %a <-@ "
Kf.pretty kf
Cil_datatype.Location.pretty (Stmt.loc stmt)
in
Format.fprintf fmt "@[<hv>";
List.iter (pp_call fmt) cs.stack;
Format.fprintf fmt "%a@]" Kernel_function.pretty cs.entry_point
let hash cs =
Hashtbl.hash
(cs.thread, Kernel_function.hash cs.entry_point, Calls.hash cs.stack)
end
type call = Call.t
include Datatype.Make_with_collections (Prototype)
let pretty_debug = pretty
let compare_lex cs1 cs2 =
if cs1 == cs2 then 0 else
let c = Thread.compare cs1.thread cs2.thread in
if c <> 0 then c else
let c = Kernel_function.compare cs1.entry_point cs2.entry_point in
if c <> 0 then c else
Calls.compare (List.rev cs1.stack) (List.rev cs2.stack)
(* Stack manipulation *)
let init ?(thread=0) kf = { thread; entry_point=kf; stack = [] }
let push kf stmt cs =
{ cs with stack = (kf, stmt) :: cs.stack }
let pop cs =
match cs.stack with
| [] -> None
| _ :: tail -> Some { cs with stack = tail }
let top cs =
match cs.stack with
| [] -> None
| (kf, stmt) :: _ -> Some (kf, stmt)
let top_kf cs =
match cs.stack with
| (kf, _stmt) :: _ -> kf
| [] -> cs.entry_point
let top_callsite cs =
match cs.stack with
| [] -> Cil_types.Kglobal
| (_kf, stmt) :: _ -> Cil_types.Kstmt stmt
let top_call cs =
match cs.stack with
| (kf, stmt) :: _ -> kf, Cil_types.Kstmt stmt
| [] -> cs.entry_point, Cil_types.Kglobal
let top_caller cs =
match cs.stack with
| _ :: (kf, _) :: _ -> Some kf
| [_] -> Some cs.entry_point
| [] -> None
(* Conversion *)
let to_kf_list cs = cs.entry_point :: List.rev_map fst cs.stack
let to_stmt_list cs = List.rev_map snd cs.stack
let to_call_list cs =
let l =
List.rev_map (fun (kf, stmt) -> (kf, Cil_types.Kstmt stmt)) cs.stack
in
(cs.entry_point, Cil_types.Kglobal) :: l
(* Stable hash and pretty-printing *)
let stmt_hash s =
let pos = fst (Cil_datatype.Stmt.loc s) in
stable_hash (pos.Filepath.pos_path, pos.Filepath.pos_lnum)
let kf_hash kf = stable_hash (Kernel_function.get_name kf)
let rec calls_hash = function
| [] -> 0
| (kf, stmt) :: tl -> stable_hash (kf_hash kf, stmt_hash stmt, calls_hash tl)
let stable_hash { thread; entry_point; stack } =
let p = stable_hash (thread, kf_hash entry_point, calls_hash stack) in
p mod 11_316_496 (* 58 ** 4 *)
let base58_map = "123456789ABCDEFGHJKLMNPQRSTUVWXYZabcdefghijkmnopqrstuvwxyz"
(* Converts [i] into a fixed-length, 4-wide string in base-58 *)
let base58_of_int n =
let buf = Bytes.create 4 in
Bytes.set buf 0 (String.get base58_map (n mod 58));
let n = n / 58 in
Bytes.set buf 1 (String.get base58_map (n mod 58));
let n = n / 58 in
Bytes.set buf 2 (String.get base58_map (n mod 58));
let n = n / 58 in
Bytes.set buf 3 (String.get base58_map (n mod 58));
Bytes.to_string buf
let pretty_hash fmt callstack =
if Kernel.is_debug_key_enabled dkey_callstack then
Format.fprintf fmt "<%s> " (base58_of_int (stable_hash callstack))
else Format.ifprintf fmt ""
let pretty_short fmt callstack =
Format.fprintf fmt "%a" pretty_hash callstack;
let list = List.rev (to_kf_list callstack) in
Pretty_utils.pp_flowlist ~left:"" ~sep:" <- " ~right:""
(fun fmt kf -> Kernel_function.pretty fmt kf)
fmt list
let pretty fmt callstack =
Format.fprintf fmt "@[<hv>%a" pretty_hash callstack;
pretty fmt callstack;
Format.fprintf fmt "@]"
src/plugins/eva/types/callstack.mli
+ 2
− 4
View file @ d18736f1
...@@ -29,7 +29,7 @@ type call = Cil_types.kernel_function * Cil_types.stmt ...@@ -29,7 +29,7 @@ type call = Cil_types.kernel_function * Cil_types.stmt
module Call : Datatype.S with type t = call module Call : Datatype.S with type t = call
(** Eva callstacks. *) (** Eva callstacks. *)
type callstack = Eva_types.Callstack.callstack = { type callstack = {
thread: int; thread: int;
(* An identifier of the thread's callstack. *) (* An identifier of the thread's callstack. *)
entry_point: Cil_types.kernel_function; entry_point: Cil_types.kernel_function;
...@@ -38,9 +38,7 @@ type callstack = Eva_types.Callstack.callstack = { ...@@ -38,9 +38,7 @@ type callstack = Eva_types.Callstack.callstack = {
(** A call stack is a list of calls. The head is the latest call. *) (** A call stack is a list of calls. The head is the latest call. *)
} }
include Datatype.S_with_collections include Datatype.S_with_collections with type t = callstack
with type t = callstack
and module Hashtbl = Eva_types.Callstack.Hashtbl
(** Prints a callstack without displaying call sites. *) (** Prints a callstack without displaying call sites. *)
val pretty_short : Format.formatter -> t -> unit val pretty_short : Format.formatter -> t -> unit
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment