[Nonterm] Revert to lexicographical comparison between callstack

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 *)
 

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
 

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

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

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