From 56c3a93af3d28745605e3b92a037894dff6a0faf Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 27 Sep 2024 11:24:47 +0300 Subject: [PATCH 1/3] 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.") | _ -> () From da7cb070f1007a9ed1bd7818db76bc05c536e2c1 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 27 Sep 2024 11:28:23 +0300 Subject: [PATCH 2/3] Add option dbg.termination-bounds (issue #1577) --- src/analyses/loopTermination.ml | 3 ++- src/config/options.schema.json | 6 ++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml index f075ca1293..67bc8d658d 100644 --- a/src/analyses/loopTermination.ml +++ b/src/analyses/loopTermination.ml @@ -62,7 +62,8 @@ struct 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; + 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 with Not_found -> failwith "Encountered a call to __goblint_bounded with an unknown loop counter variable.") 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 From 187672e015028809c80e019bdb2309ad04aac47c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 27 Sep 2024 11:33:03 +0300 Subject: [PATCH 3/3] Clean up LoopTermination.special --- src/analyses/loopTermination.ml | 44 ++++++++++++++++----------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/src/analyses/loopTermination.ml b/src/analyses/loopTermination.ml index 67bc8d658d..05bfbda492 100644 --- a/src/analyses/loopTermination.ml +++ b/src/analyses/loopTermination.ml @@ -42,33 +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 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 - 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