From bc136259b4deb1bcc6f25e94597303a1485653be Mon Sep 17 00:00:00 2001 From: oliver Date: Wed, 31 Jan 2024 19:07:38 +0100 Subject: [PATCH] fix Nooverflow computation recursive calls --- src/analyses/base.ml | 35 ++++++++++++++++++------- src/cdomain/value/cdomains/intDomain.ml | 4 ++- src/domains/queries.ml | 2 +- 3 files changed, 29 insertions(+), 12 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 892f360f3d7..683e8bb9c92 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -97,6 +97,9 @@ struct module VarMap = Map.Make(CilType.Varinfo) let array_map = ref (VarH.create 20) + (*This is a bit of hack to check if we are currently in a NoOverflow query*) + let noOverflow_query_already_started = ref false + type marshal = attributes VarMap.t VarH.t let array_domain_annotation_enabled = lazy (GobConfig.get_bool "annotation.goblint_array_domain") @@ -1398,16 +1401,28 @@ struct let g: V.t = Obj.obj g in query_invariant_global ctx g | Q.NoOverflow e -> - MCP.lookUpCache := false; - IntDomain.local_no_overflow := true; - if M.tracing then M.trace "no_ov" "exp %a\n" d_exp e; - let res = try - ignore(query_evalint ~ctx ctx.local e); - !IntDomain.local_no_overflow - with IntDomain.ArithmeticOnIntegerBot _ -> false - in - MCP.lookUpCache := true; - res + (* NoOverflow calls EvalInt, which in turn can call NoOverflow again in the relational domain *) + if not !noOverflow_query_already_started then ( + noOverflow_query_already_started := true; + IntDomain.local_no_overflow := true; + MCP.lookUpCache := false; (*disable caching to compute the [!Intdomain.local_no_overflow] correctly*) + let res = try + ignore(query_evalint ~ctx ctx.local e); + !IntDomain.local_no_overflow + with IntDomain.ArithmeticOnIntegerBot _ -> false + in + MCP.lookUpCache := true; + noOverflow_query_already_started := false; + res + )else + if not !IntDomain.local_no_overflow then false + else + let res = try + ignore(query_evalint ~ctx ctx.local e); + !IntDomain.local_no_overflow + with IntDomain.ArithmeticOnIntegerBot _ -> false + in + res | _ -> Q.Result.top q let update_variable variable typ value cpa = diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 50445f67e0b..ecea8d5d966 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -80,10 +80,12 @@ let set_overflow_flag ~cast ~underflow ~overflow ik = if !AnalysisState.postsolving && signed && not cast then AnalysisState.svcomp_may_overflow := true; let sign = if signed then "Signed" else "Unsigned" in + if M.tracing then M.trace "no_ov" "set = %b\n" !local_no_overflow; (if signed && not (get_string "sem.int.signed_overflow" = "assume_none") then local_no_overflow := false - else + else if not signed then local_no_overflow := false); + if M.tracing then M.trace "no_ov" "set = %b\n" !local_no_overflow; match underflow, overflow with | true, true -> M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190; CWE 191] "%s integer overflow and underflow" sign diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 3b6e44dd1a9..e2fe64bfc7d 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -512,7 +512,7 @@ struct | Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded" | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv | Any (MayBeOutOfBounds x) -> Pretty.dprintf "MayBeOutOfBounds _" - | Any (NoOverflow e) -> Pretty.dprintf "MayOverflow %a" CilType.Exp.pretty e + | Any (NoOverflow e) -> Pretty.dprintf "NoOverflow %a" CilType.Exp.pretty e | Any (AllocMayBeOutOfBounds x) -> Pretty.dprintf "AllocMayBeOutOfBounds _" | Any (AllocAssignedToGlobal v) -> Pretty.dprintf "AllocAssignedToGlobal %a" CilType.Varinfo.pretty v end