From 4bca7728bee90a56ba53d38c118d3143d88041e3 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 8 Jun 2023 18:23:27 +0200
Subject: [PATCH] [Eva] add Callstack to Eva's API
---
src/plugins/eva/Eva.mli | 45 ++++++++++++++++++++++++++++++++++++++++-
src/plugins/eva/dune | 2 +-
2 files changed, 45 insertions(+), 2 deletions(-)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index db84313b85a..5c712b2dfeb 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -115,6 +115,49 @@ module Analysis: sig
val save_results: Cil_types.kernel_function -> bool
end
+module Callstack: sig
+ (* A call is identified by the function called and the call statement *)
+ type call = Cil_types.kernel_function * Cil_types.stmt
+
+ module Call : Datatype.S with type t = call
+
+ (** [callstack] is used to describe the analysis context when analysing a
+ function. It contains the thread, the entry point and the list of
+ calls from the entry point.
+
+ This type is very likely to change in the future. Never use this type
+ directly, prefer the use of the following functions when possible. *)
+
+ type callstack = private {
+ thread: int; (* An identifier of the thread's callstack *)
+ entry_point: Cil_types.kernel_function; (* The first function in the callstack *)
+ stack: call list;
+ }
+
+ include Datatype.S_with_collections with type t = callstack
+
+ (* Constructor *)
+ val init : ?thread:int -> Cil_types.kernel_function -> t
+
+ (* Stack manipulation *)
+ val push : Cil_types.kernel_function -> Cil_types.stmt -> t -> t
+ val pop : t -> (Cil_types.kernel_function * Cil_types.stmt * 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.stmt option
+
+ (* Conversion *)
+
+ (** This function is likely to be removed in future versions*)
+ val to_legacy : t -> Value_types.callstack
+
+ (** Gives the list of kf in the callstack from the entry point to the top of the callstack (i.e. reverse order of the call stack). *)
+ val to_kf_list : t -> Cil_types.kernel_function list
+
+ (** Gives the list of call statements from the bottom to the top of the callstack (i.e. reverse order of the call stack). *)
+ val to_stmt_list : t -> Cil_types.stmt list
+end
+
module Results: sig
(** Eva's result API is a new interface to access the results of an analysis,
@@ -158,7 +201,7 @@ module Results: sig
all requests in the function will lead to a Top error. *)
val are_available : Cil_types.kernel_function -> bool
- type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
+ type callstack = Callstack.t
type request
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index 6877dfd4327..a5aae82cd35 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -105,7 +105,7 @@
(mode (promote (only Eva.mli)))
(deps
gen-api.sh Eva.header
- engine/analysis.mli utils/results.mli parameters.mli
+ engine/analysis.mli types/callstack.mli utils/results.mli parameters.mli
utils/eva_annotations.mli eval.mli domains/cvalue/builtins.mli
utils/cvalue_callbacks.mli legacy/logic_inout.mli utils/eva_results.mli
utils/unit_tests.mli)
--
GitLab