diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml index 66a50c17b7..05bfbda492 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 @@ -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 ctx (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 ctx loop_counter 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)" - ); - () - 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 ctx loop_counter in + let is_bounded = bound <> `Top in + ctx.sideg () (G.add (`Lifted loop_statement) is_bounded (ctx.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 ctx (type a) (q: a Queries.t): a Queries.result = match q with diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 447290b44d..99f7dc2fa2 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -2150,6 +2150,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