From c12375b858c5c84b11744f3dd50e01a4cde11e8e Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 13 Jun 2023 15:29:22 +0200
Subject: [PATCH] [Nonterm] Revert to lexicographical comparison between
callstack
---
src/kernel_services/abstract_interp/eva_types.ml | 12 ++++++++++++
src/kernel_services/abstract_interp/eva_types.mli | 2 ++
src/plugins/eva/Eva.mli | 5 +++++
src/plugins/eva/types/callstack.mli | 5 +++++
src/plugins/nonterm/nonterm_run.ml | 2 +-
5 files changed, 25 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/abstract_interp/eva_types.ml b/src/kernel_services/abstract_interp/eva_types.ml
index de54d6beef0..b4b3a8f031b 100644
--- a/src/kernel_services/abstract_interp/eva_types.ml
+++ b/src/kernel_services/abstract_interp/eva_types.ml
@@ -63,6 +63,14 @@ struct
List.iter (pp_call fmt) cs.stack;
Format.fprintf fmt "%a@]" Kernel_function.pretty cs.entry_point
+ let compare_lex ls1 ls2 =
+ if ls1 == ls2 then 0 else
+ let c = Thread.compare ls1.thread ls2.thread in
+ if c <> 0 then c else
+ let c = Kernel_function.compare ls1.entry_point ls2.entry_point in
+ if c <> 0 then c else
+ Calls.compare (List.rev ls1.stack) (List.rev ls2.stack)
+
let hash cs =
Hashtbl.hash
(cs.thread, Kernel_function.hash cs.entry_point, Calls.hash cs.stack)
@@ -105,6 +113,10 @@ struct
include Datatype.Make_with_collections (Prototype)
+ let compare_lex cs1 cs2 =
+ match cs1, cs2 with
+ | Local ls1, Local ls2 -> LocalStack.compare_lex ls1 ls2
+ | cs1, cs2 -> compare cs1 cs2
(* Constructor *)
diff --git a/src/kernel_services/abstract_interp/eva_types.mli b/src/kernel_services/abstract_interp/eva_types.mli
index dc6b71c84df..97a4b2957e0 100644
--- a/src/kernel_services/abstract_interp/eva_types.mli
+++ b/src/kernel_services/abstract_interp/eva_types.mli
@@ -41,6 +41,8 @@ sig
include Datatype.S_with_collections with type t = callstack
+ val compare_lex : t -> t -> int
+
val init_global : Cil_types.varinfo -> t
val init_local : ?thread:int -> Cil_types.kernel_function -> t
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 18d459bb886..1b7b47ac288 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -143,6 +143,11 @@ module Callstack: sig
with type t = callstack
and module Hashtbl = Eva_types.Callstack.Hashtbl
+ (** [compare_lex] compares callstack lexicographically, slightly slower
+ than [compare] but in a more natural order, giving more importance
+ to the function at bottom of the callstack - the first functions called. *)
+ val compare_lex : t -> t -> int
+
(* Constructor *)
val init_global : Cil_types.varinfo -> t
val init_local : ?thread:int -> Cil_types.kernel_function -> t
diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli
index 4a22d47031d..7de74799a42 100644
--- a/src/plugins/eva/types/callstack.mli
+++ b/src/plugins/eva/types/callstack.mli
@@ -48,6 +48,11 @@ include Datatype.S_with_collections
with type t = callstack
and module Hashtbl = Eva_types.Callstack.Hashtbl
+(** [compare_lex] compares callstack lexicographically, slightly slower
+ than [compare] but in a more natural order, giving more importance
+ to the function at bottom of the callstack - the first functions called. *)
+val compare_lex : t -> t -> int
+
(* Constructor *)
val init_global : Cil_types.varinfo -> t
val init_local : ?thread:int -> Cil_types.kernel_function -> t
diff --git a/src/plugins/nonterm/nonterm_run.ml b/src/plugins/nonterm/nonterm_run.ml
index 0f1ae23f1c8..176678b5e49 100644
--- a/src/plugins/nonterm/nonterm_run.ml
+++ b/src/plugins/nonterm/nonterm_run.ml
@@ -328,7 +328,7 @@ let run () =
let warned_kfs =
Stmt.Hptset.fold (fun stmt acc ->
let cs = Hashtbl.find nonterm_stacks stmt in
- let cs = List.sort Eva.Callstack.compare cs in
+ let cs = List.sort Eva.Callstack.compare_lex cs in
warn_nonterminating_statement stmt cs;
Kernel_function.Set.add (Kernel_function.find_englobing_kf stmt) acc
) new_nonterm_stmts Kernel_function.Set.empty
--
GitLab