Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add termination analysis success messages for loop bounds #1580

Merged
merged 4 commits into from
Dec 20, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 26 additions & 20 deletions src/analyses/loopTermination.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
6 changes: 6 additions & 0 deletions src/config/options.schema.json
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading