Merge pull request #1580 from goblint/issue-1577

Add termination analysis success messages for loop bounds

Author: sim642

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 man varinfo =
+let ask_bound man varinfo =
   let open IntDomain.IntDomTuple in
   let exp = Lval (Var varinfo, NoOffset) in
   match man.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
@@ -41,28 +42,33 @@ struct
   let startstate _ = ()
   let exitstate = startstate
 
-  let find_loop ~loop_counter =
-    VarToStmt.find loop_counter !loop_counters
-
   (** Recognizes a call of [__goblint_bounded] to check the EvalInt of the
    * respective loop counter variable at that position. *)
   let special man (lval : lval option) (f : varinfo) (arglist : exp list) =
-    if !AnalysisState.postsolving then
+    if !AnalysisState.postsolving then (
       match f.vname, arglist with
-        "__goblint_bounded", [Lval (Var loop_counter, NoOffset)] ->
-        (try
-           let loop_statement = find_loop ~loop_counter in
-           let is_bounded = check_bounded man loop_counter in
-           man.sideg () (G.add (`Lifted loop_statement) is_bounded (man.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)"
-           );
-           ()
-         with Not_found ->
-           failwith "Encountered a call to __goblint_bounded with an unknown loop counter variable.")
+      | "__goblint_bounded", [Lval (Var loop_counter, NoOffset)] ->
+        begin match VarToStmt.find_opt loop_counter !loop_counters with
+          | Some loop_statement ->
+            let bound = ask_bound man loop_counter in
+            let is_bounded = bound <> `Top in
+            man.sideg () (G.add (`Lifted loop_statement) is_bounded (man.global ()));
+            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? *)
+                if GobConfig.get_bool "dbg.termination-bounds" then
+                  M.success ~category:Termination ~loc "Loop terminates: bounded by %a iteration(s)" IntDomain.IntDomTuple.pretty bound;
+            end
+          | None ->
+            failwith "Encountered a call to __goblint_bounded with an unknown loop counter variable."
+        end
+      | "__goblint_bounded", _ ->
+        failwith "__goblint_bounded call unexpected arguments"
       | _ -> ()
-    else ()
+    )
 
   let query man (type a) (q: a Queries.t): a Queries.result =
     match q with

src/config/options.schema.json

@@ -2197,6 +2197,12 @@
           "description": "Output abstract values, etc. with full internal details, without readability-oriented simplifications.",
           "type": "boolean",
           "default": false
+        },
+        "termination-bounds": {
+          "title": "dbg.termination-bounds",
+          "description": "Output loop iteration bounds for terminating loops when termination analysis is activated.",
+          "type": "boolean",
+          "default": false
         }
       },
       "additionalProperties": false