From 56c3a93af3d28745605e3b92a037894dff6a0faf Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 27 Sep 2024 11:24:47 +0300
Subject: [PATCH] Add termination analysis success messages for loop bounds
 (closes #1577)

---
 src/analyses/loopTermination.ml | 23 ++++++++++++++---------
 1 file changed, 14 insertions(+), 9 deletions(-)

diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml
index 66a50c17b7..f075ca1293 100644
--- a/src/analyses/loopTermination.ml
+++ b/src/analyses/loopTermination.ml
@@ -8,12 +8,13 @@ open TerminationPreprocessing
 let loop_counters : stmt VarToStmt.t ref = ref VarToStmt.empty
 
 (** Checks whether a variable can be bounded. *)
-let check_bounded ctx varinfo =
+let ask_bound ctx varinfo =
   let open IntDomain.IntDomTuple in
   let exp = Lval (Var varinfo, NoOffset) in
   match ctx.ask (EvalInt exp) with
-  | `Top -> false
-  | `Lifted v -> not (is_top_of (ikind v) v)
+  | `Top -> `Top
+  | `Lifted v when is_top_of (ikind v) v -> `Top
+  | `Lifted v -> `Lifted v
   | `Bot -> failwith "Loop counter variable is Bot."
 
 (** We want to record termination information of loops and use the loop
@@ -52,13 +53,17 @@ struct
         "__goblint_bounded", [Lval (Var loop_counter, NoOffset)] ->
         (try
            let loop_statement = find_loop ~loop_counter in
-           let is_bounded = check_bounded ctx loop_counter in
+           let bound = ask_bound ctx loop_counter in
+           let is_bounded = bound <> `Top in
            ctx.sideg () (G.add (`Lifted loop_statement) is_bounded (ctx.global ()));
-           (* In case the loop is not bounded, a warning is created. *)
-           if not (is_bounded) then (
-             M.warn ~loc:(M.Location.CilLocation (Cilfacade.get_stmtLoc loop_statement)) ~category:Termination "The program might not terminate! (Loop analysis)"
-           );
-           ()
+           let loc = M.Location.CilLocation (Cilfacade.get_stmtLoc loop_statement) in
+           begin match bound with
+             | `Top ->
+               M.warn ~category:Termination ~loc "The program might not terminate! (Loop analysis)"
+             | `Lifted bound ->
+               (* TODO: aggregate these per loop (if unrolled) and warn using WarnGlobal? *)
+               M.success ~category:Termination ~loc "Loop terminates: bounded by %a iteration(s)" IntDomain.IntDomTuple.pretty bound;
+           end
          with Not_found ->
            failwith "Encountered a call to __goblint_bounded with an unknown loop counter variable.")
       | _ -> ()