From a65ac9b6281afb764bbe0deaf530fb895c9cf7be Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Thu, 26 Jun 2025 16:00:20 +0300 Subject: [PATCH 01/36] added a check module to get a custom output for the dashboard --- src/common/util/checks.ml | 71 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 71 insertions(+) create mode 100644 src/common/util/checks.ml diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml new file mode 100644 index 0000000000..a9bbb65444 --- /dev/null +++ b/src/common/util/checks.ml @@ -0,0 +1,71 @@ +module Kind = struct + type t = + | Error + | Warning + | Success + + let to_yojson x = `String (match x with + | Error -> "error" + | Warning -> "warning" + | Success -> "success") + + let of_yojson = function + | `String "error" -> Ok Error + | `String "warning" -> Ok Warning + | `String "success" -> Ok Success + | kind -> Error ("Checks.Kind.of_yojson: Invalid kind :" ^ Yojson.Safe.to_string kind) +end + +module Category = struct + type t = + | AssersionFaillure + | InvalidMemoryAccess + | DivisionByZero + | IntegerOverflow + | InvalidPointerComparison + | InvalidPointerSubtraction + | DoubleFree + | NegativeArraySize + + let to_yojson x = `String (match x with + | AssersionFaillure -> "Assertion failure" + | InvalidMemoryAccess -> "Invalid memory access" + | DivisionByZero -> "Division by zero" + | IntegerOverflow -> "Integer overflow" + | InvalidPointerComparison -> "Invalid pointer comparison" + | InvalidPointerSubtraction -> "Invalid pointer subtraction" + | DoubleFree -> "Double free" + | NegativeArraySize -> "Negative array size") + + let of_yojson = function + | `String "Assertion failure" -> Ok AssersionFaillure + | `String "Invalid memory access" -> Ok InvalidMemoryAccess + | `String "Division by zero" -> Ok DivisionByZero + | `String "Integer overflow" -> Ok IntegerOverflow + | `String "Invalid pointer comparison" -> Ok InvalidPointerComparison + | `String "Invalid pointer subtraction" -> Ok InvalidPointerSubtraction + | `String "Double free" -> Ok DoubleFree + | `String "Negative array size" -> Ok NegativeArraySize + | category -> Error ("Checks.Category.of_yojson: Invalid category :" ^ Yojson.Safe.to_string category) +end + +module Check = struct + type t = { + kind: Kind.t; + category: Category.t; + location: CilType.Location.t; + message: string; + } [@@deriving yojson, make] + + let checks = ref [] + + let check kind category location message = + let check = make ~kind ~category ~location ~message in + checks := check :: !checks +end + +let error = Check.check Kind.Error + +let warning = Check.check Kind.Warning + +let success = Check.check Kind.Success From 48acfda2c181c2b070d5b83b1f972f8cf3c0751e Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Wed, 25 Jun 2025 13:51:41 +0300 Subject: [PATCH 02/36] exposed the root_with_current function for timing purposes --- src/util/timing/goblint_timing_intf.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/util/timing/goblint_timing_intf.ml b/src/util/timing/goblint_timing_intf.ml index 2321f79bb4..b6a697eae8 100644 --- a/src/util/timing/goblint_timing_intf.ml +++ b/src/util/timing/goblint_timing_intf.ml @@ -57,6 +57,10 @@ sig val print: Format.formatter -> unit (** Pretty-print current timing hierarchy. *) + val root_with_current: unit -> tree + (** Root tree with current (entered but not yet exited) frame resources added. + This allows printing with in-progress resources also accounted for *) + val root: tree (** Root node of timing tree. Must not be mutated! *) From e6796da817e6a5e1ea82170d35292f2497b0d2f5 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Mon, 30 Jun 2025 16:08:14 +0300 Subject: [PATCH 03/36] replaced success by safe --- src/analyses/assert.ml | 4 + src/analyses/base.ml | 60 ++++++++---- src/analyses/baseInvariant.ml | 6 +- src/analyses/malloc_null.ml | 5 +- src/analyses/memOutOfBounds.ml | 89 +++++++++++------ src/analyses/useAfterFree.ml | 6 +- src/cdomain/value/cdomains/addressDomain.ml | 5 +- src/cdomain/value/cdomains/arrayDomain.ml | 103 +++++++++++++++----- src/cdomain/value/cdomains/intDomain0.ml | 9 +- src/common/util/checks.ml | 78 ++++++++++++--- src/framework/analysisResult.ml | 8 ++ 11 files changed, 277 insertions(+), 96 deletions(-) diff --git a/src/analyses/assert.ml b/src/analyses/assert.ml index c9045037f7..b811f8c73b 100644 --- a/src/analyses/assert.ml +++ b/src/analyses/assert.ml @@ -44,15 +44,19 @@ struct match check_assert e man.local with | `Lifted false -> warn (M.error ~category:Assert "%s") ~annot:"FAIL" ("Assertion \"" ^ expr ^ "\" will fail."); + Checks.error Checks.Category.AssersionFaillure "Assertion \"%s\" will fail." expr; if refine then raise Analyses.Deadcode else man.local | `Lifted true -> warn (M.success ~category:Assert "%s") ("Assertion \"" ^ expr ^ "\" will succeed"); + Checks.safe Checks.Category.AssersionFaillure; man.local | `Bot -> M.error ~category:Assert "%s" ("Assertion \"" ^ expr ^ "\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)"); + Checks.error Checks.Category.AssersionFaillure "Assertion \"%s\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)" expr; man.local | `Top -> warn (M.warn ~category:Assert "%s") ~annot:"UNKNOWN" ("Assertion \"" ^ expr ^ "\" is unknown."); + Checks.warn Checks.Category.AssersionFaillure "Assertion \"%s\" is unknown." expr; man.local let special man (lval: lval option) (f:varinfo) (args:exp list) : D.t = diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 9ae487fc52..49ecd3e614 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -204,19 +204,25 @@ struct fun x y -> (match ID.equal_to Z.zero y with | `Eq -> - M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division is zero" + M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division is zero"; + Checks.error Checks.Category.DivisionByZero "Second argument of division is zero" | `Top -> - M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division might be zero" - | `Neq -> ()); + M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division might be zero"; + Checks.warn Checks.Category.DivisionByZero "Second argument of division might be zero" + | `Neq -> + Checks.safe Checks.Category.DivisionByZero); ID.div x y | Mod -> fun x y -> (match ID.equal_to Z.zero y with | `Eq -> - M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo is zero" + M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo is zero"; + Checks.error Checks.Category.DivisionByZero "Second argument of modulo is zero" | `Top -> - M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo might be zero" - | `Neq -> ()); + M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo might be zero"; + Checks.warn Checks.Category.DivisionByZero "Second argument of modulo might be zero" + | `Neq -> + Checks.safe Checks.Category.DivisionByZero); ID.rem x y | Lt -> ID.lt | Gt -> ID.gt @@ -1088,11 +1094,15 @@ struct ( if AD.is_null adr then ( AnalysisStateUtil.set_mem_safety_flag InvalidDeref; - M.error ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "Must dereference NULL pointer" + M.error ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "Must dereference NULL pointer"; + Checks.error Checks.Category.InvalidMemoryAccess "Must dereference NULL pointer" ) else if AD.may_be_null adr then ( AnalysisStateUtil.set_mem_safety_flag InvalidDeref; - M.warn ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "May dereference NULL pointer" + M.warn ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "May dereference NULL pointer"; + Checks.warn Checks.Category.InvalidMemoryAccess "May dereference NULL pointer" + ) else ( + Checks.safe Checks.Category.InvalidMemoryAccess ); (* Warn if any of the addresses contains a non-local and non-global variable *) if AD.exists (function @@ -1100,7 +1110,8 @@ struct | _ -> false ) adr then ( AnalysisStateUtil.set_mem_safety_flag InvalidDeref; - M.warn "lval %a points to a non-local variable. Invalid pointer dereference may occur" d_lval lval + M.warn "lval %a points to a non-local variable. Invalid pointer dereference may occur" d_lval lval; + Checks.warn Checks.Category.InvalidMemoryAccess "lval %a points to a non-local variable. Invalid pointer dereference may occur" d_lval lval ) ); AD.map (add_offset_varinfo (convert_offset ~man st ofs)) adr @@ -1172,10 +1183,13 @@ struct let eval_funvar man fval: Queries.AD.t = let fp = eval_fv ~man man.local fval in if AD.is_top fp then ( - if AD.cardinal fp = 1 then - M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval - else - M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval + if AD.cardinal fp = 1 then ( + M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval; + Checks.warn Checks.Category.InvalidMemoryAccess "Unknown call to function %a." d_exp fval + ) else ( + M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval; + Checks.warn Checks.Category.InvalidMemoryAccess "Function pointer %a may contain unknown functions." d_exp fval + ) ); fp @@ -2242,7 +2256,10 @@ struct end let special_unknown_invalidate man f args = - (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn ~category:Imprecise ~tags:[Category Call] "Unknown function ptr called"); + (if CilType.Varinfo.equal f dummyFunDec.svar then ( + M.warn ~category:Imprecise ~tags:[Category Call] "Unknown function ptr called"; + Checks.warn Checks.Category.InvalidMemoryAccess "Unknown function ptr called" + )); let desc = LF.find f in let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in @@ -2278,17 +2295,23 @@ struct | Address a -> if AD.is_top a then ( AnalysisStateUtil.set_mem_safety_flag InvalidFree; - M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potentially invalid memory deallocation may occur" d_exp ptr special_fn.vname + M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potentially invalid memory deallocation may occur" d_exp ptr special_fn.vname; + Checks.warn Checks.Category.InvalidMemoryAccess "Points-to set for pointer %a in function %s is top. Potentially invalid memory deallocation may occur" d_exp ptr special_fn.vname ) else if has_non_heap_var a then ( AnalysisStateUtil.set_mem_safety_flag InvalidFree; - M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Free of non-dynamically allocated memory in function %s for pointer %a" special_fn.vname d_exp ptr + M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Free of non-dynamically allocated memory in function %s for pointer %a" special_fn.vname d_exp ptr; + Checks.warn Checks.Category.InvalidMemoryAccess "Free of non-dynamically allocated memory in function %s for pointer %a" special_fn.vname d_exp ptr ) else if has_non_zero_offset a then ( AnalysisStateUtil.set_mem_safety_flag InvalidFree; - M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer in function %s for pointer %a" special_fn.vname d_exp ptr + M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer in function %s for pointer %a" special_fn.vname d_exp ptr; + Checks.warn Checks.Category.InvalidMemoryAccess "Free of memory not at start of buffer in function %s for pointer %a" special_fn.vname d_exp ptr + ) else ( + Checks.safe Checks.Category.InvalidMemoryAccess ) | _ -> AnalysisStateUtil.set_mem_safety_flag InvalidFree; - M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Pointer %a in function %s doesn't evaluate to a valid address. Invalid memory deallocation may occur" d_exp ptr special_fn.vname + M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Pointer %a in function %s doesn't evaluate to a valid address. Invalid memory deallocation may occur" d_exp ptr special_fn.vname; + Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a in function %s doesn't evaluate to a valid address. Invalid memory deallocation may occur" d_exp ptr special_fn.vname let points_to_heap_only man ptr = match man.ask (Queries.MayPointTo ptr) with @@ -2346,6 +2369,7 @@ struct end | _ -> (M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; + Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; `Top) let special man (lv:lval option) (f: varinfo) (args: exp list) = diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 51bc436348..37217bdee5 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -287,9 +287,11 @@ struct let warn_and_top_on_zero x = if GobOption.exists (Z.equal Z.zero) (ID.to_int x) then (M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top"; + Checks.error Checks.Category.DivisionByZero "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top"; ID.top_of ikind) - else - x + else ( + Checks.safe Checks.Category.DivisionByZero; + x) in let meet_bin a' b' = id_meet_down ~old:a ~c:a', id_meet_down ~old:b ~c:b' in let meet_com oi = (* commutative *) diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml index e990272700..604d1a6728 100644 --- a/src/analyses/malloc_null.ml +++ b/src/analyses/malloc_null.ml @@ -27,7 +27,10 @@ struct if D.exists (fun x -> GobOption.exists (fun x -> is_prefix_of x v) (Addr.to_mval x)) st then let var = Addr.of_mval v in - Messages.warn ~category:Messages.Category.Behavior.Undefined.nullpointer_dereference "Possible dereferencing of null on variable '%a'." Addr.pretty var + Messages.warn ~category:Messages.Category.Behavior.Undefined.nullpointer_dereference "Possible dereferencing of null on variable '%a'." Addr.pretty var; + Checks.warn Checks.Category.InvalidMemoryAccess "Possible dereferencing of null on variable '%a'." Addr.pretty var + else + Checks.safe Checks.Category.InvalidMemoryAccess with SetDomain.Unsupported _ -> () (* Warn null-lval dereferences, but not normal (null-) lvals*) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index ff3946d047..2f760f0772 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -123,6 +123,7 @@ struct | _ -> (set_mem_safety_flag InvalidDeref; M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; + Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; `Top) let get_ptr_deref_type ptr_typ = @@ -195,8 +196,10 @@ struct in if may_contain_unknown_addr then begin set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior (Undefined Other)) "Pointer %a contains an unknown address. Invalid dereference may occur" d_exp ptr - end + M.warn ~category:(Behavior (Undefined Other)) "Pointer %a contains an unknown address. Invalid dereference may occur" d_exp ptr; + Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a contains an unknown address. Invalid dereference may occur" d_exp ptr + end else + Checks.safe Checks.Category.InvalidMemoryAccess let ptr_only_has_str_addr man ptr = match man.ask (Queries.EvalValue ptr) with @@ -217,6 +220,7 @@ struct begin match VDQ.AD.is_empty a with | true -> M.warn "Pointer %a has an empty points-to-set" d_exp ptr; + Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a has an empty points-to-set" d_exp ptr; ID.top_of @@ Cilfacade.ptrdiff_ikind () | false -> if VDQ.AD.exists (function @@ -224,13 +228,17 @@ struct | _ -> false ) a then ( set_mem_safety_flag InvalidDeref; - M.warn "Pointer %a has a bot address offset. An invalid memory access may occur" d_exp ptr + M.warn "Pointer %a has a bot address offset. An invalid memory access may occur" d_exp ptr; + Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a has a bot address offset. An invalid memory access may occur" d_exp ptr ) else if VDQ.AD.exists (function | Addr (_, o) -> ID.is_top_of (Cilfacade.ptrdiff_ikind ()) (offs_to_idx t o) | _ -> false ) a then ( set_mem_safety_flag InvalidDeref; - M.warn "Pointer %a has a top address offset. An invalid memory access may occur" d_exp ptr + M.warn "Pointer %a has a top address offset. An invalid memory access may occur" d_exp ptr; + Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a has a top address offset. An invalid memory access may occur" d_exp ptr + ) else ( + Checks.safe Checks.Category.InvalidMemoryAccess ); (* Get the address offsets of all points-to set elements *) let addr_offsets = @@ -251,6 +259,7 @@ struct | _ -> set_mem_safety_flag InvalidDeref; M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; + Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; ID.top_of @@ Cilfacade.ptrdiff_ikind () and check_lval_for_oob_access man ?(is_implicitly_derefed = false) lval = @@ -272,10 +281,12 @@ struct let () = begin match e_size with | `Top -> (set_mem_safety_flag InvalidDeref; - M.warn "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp e) + M.warn "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp e); + Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp e | `Bot -> (set_mem_safety_flag InvalidDeref; - M.warn "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp e) + M.warn "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp e); + Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp e | `Lifted es -> let casted_es = ID.cast_to (Cilfacade.ptrdiff_ikind ()) es in let casted_offs = ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom in @@ -291,11 +302,14 @@ struct begin match ID.to_bool ptr_size_lt_offs with | Some true -> (set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of lval dereference expression is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" ID.pretty casted_es ID.pretty casted_offs) - | Some false -> () + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of lval dereference expression is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" ID.pretty casted_es ID.pretty casted_offs); + Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" ID.pretty casted_es ID.pretty casted_offs + | Some false -> + Checks.safe Checks.Category.InvalidMemoryAccess | None -> (set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of lval dereference expression (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_es ID.pretty casted_offs) + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of lval dereference expression (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_es ID.pretty casted_offs); + Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare size of lval dereference expression (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_es ID.pretty casted_offs end end in begin match e with @@ -320,10 +334,12 @@ struct begin match ptr_size, addr_offs with | `Top, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp; + Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp | `Bot, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp; + Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp | `Lifted ps, ao -> let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ao in @@ -331,11 +347,14 @@ struct begin match ID.to_bool ptr_size_lt_offs with | Some true -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" ID.pretty casted_ps ID.pretty casted_ao - | Some false -> () + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" ID.pretty casted_ps ID.pretty casted_ao; + Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" ID.pretty casted_ps ID.pretty casted_ao + | Some false -> + Checks.safe Checks.Category.InvalidMemoryAccess | None -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of pointer (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_ps ID.pretty casted_ao + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of pointer (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_ps ID.pretty casted_ao; + Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare size of pointer (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_ps ID.pretty casted_ao end end | _ -> M.error "Expression %a is not a pointer" d_exp lval_exp @@ -395,16 +414,20 @@ struct begin match ptr_size, offset_size_with_addr_size with | `Top, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is top. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is top. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp; + Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a in expression %a is top. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp | _, `Top -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is top. Memory out-of-bounds access might occur" d_exp binopexp + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is top. Memory out-of-bounds access might occur" d_exp binopexp; + Checks.warn Checks.Category.InvalidMemoryAccess "Operand value for pointer arithmetic in expression %a is top. Memory out-of-bounds access might occur" d_exp binopexp | `Bot, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is bottom. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is bottom. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp; + Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a in expression %a is bottom. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp | _, `Bot -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is bottom. Memory out-of-bounds access might occur" d_exp binopexp + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is bottom. Memory out-of-bounds access might occur" d_exp binopexp; + Checks.warn Checks.Category.InvalidMemoryAccess "Operand value for pointer arithmetic in expression %a is bottom. Memory out-of-bounds access might occur" d_exp binopexp | `Lifted ps, `Lifted o -> let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in let casted_o = ID.cast_to (Cilfacade.ptrdiff_ikind ()) o in @@ -412,11 +435,14 @@ struct begin match ID.to_bool ptr_size_lt_offs with | Some true -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o - | Some false -> () + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o; + Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o + | Some false -> + Checks.safe Checks.Category.InvalidMemoryAccess | None -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare pointer size (%a) with offset (%a). Memory out-of-bounds access may occur" ID.pretty casted_ps ID.pretty casted_o + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare pointer size (%a) with offset (%a). Memory out-of-bounds access may occur" ID.pretty casted_ps ID.pretty casted_o; + Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare pointer size (%a) with offset (%a). Memory out-of-bounds access may occur" ID.pretty casted_ps ID.pretty casted_o end end | _ -> M.error "Binary expression %a doesn't have a pointer" d_exp binopexp @@ -433,16 +459,20 @@ struct match ptr_size, eval_n with | `Top, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp ptr fun_name + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp ptr fun_name; + Checks.warn Checks.Category.InvalidMemoryAccess "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp ptr fun_name | _, `Top -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name; + Checks.warn Checks.Category.InvalidMemoryAccess "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name | `Bot, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp ptr fun_name + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp ptr fun_name; + Checks.warn Checks.Category.InvalidMemoryAccess "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp ptr fun_name | _, `Bot -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is bottom" fun_name + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is bottom" fun_name; + Checks.warn Checks.Category.InvalidMemoryAccess "Count parameter, passed to function %s is bottom" fun_name | `Lifted ds, `Lifted en -> let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in let casted_en = ID.cast_to (Cilfacade.ptrdiff_ikind ()) en in @@ -451,11 +481,14 @@ struct begin match ID.to_bool dest_size_lt_count with | Some true -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of %a in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en - | Some false -> () + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of %a in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en; + Checks.warn Checks.Category.InvalidMemoryAccess "Size of %a in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en + | Some false -> + Checks.safe Checks.Category.InvalidMemoryAccess | None -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name; + Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare size of dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name end diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 32a095a13c..c26a396fb8 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -110,8 +110,10 @@ struct let warn_for_heap_var v = if HeapVars.mem v (snd state) then begin if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name - end + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name; + Checks.warn Checks.Category.DoubleFree "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name; + end else + Checks.safe Checks.Category.DoubleFree in let pointed_to_heap_vars = Queries.AD.fold (fun addr vars -> diff --git a/src/cdomain/value/cdomains/addressDomain.ml b/src/cdomain/value/cdomains/addressDomain.ml index da684cc4f4..70041d8498 100644 --- a/src/cdomain/value/cdomains/addressDomain.ml +++ b/src/cdomain/value/cdomains/addressDomain.ml @@ -322,9 +322,12 @@ struct (* if the destination address set contains a StrPtr, writing to such a string literal is undefined behavior *) if exists (fun a -> Option.is_some (Addr.to_c_string a)) dest then (M.warn ~category:M.Category.Behavior.Undefined.other "May write to a string literal, which leads to a segmentation fault in most cases"; + Checks.warn Checks.Category.InvalidMemoryAccess "May write to a string literal, which leads to a segmentation fault in most cases"; false) - else + else ( + Checks.safe Checks.Category.InvalidMemoryAccess; true + ) (* add an & in front of real addresses *) module ShortAddr = diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml index 4192489c3a..e2564f8798 100644 --- a/src/cdomain/value/cdomains/arrayDomain.ml +++ b/src/cdomain/value/cdomains/arrayDomain.ml @@ -838,22 +838,27 @@ let array_oob_check ( type a ) (module Idx: IntDomain.Z with type t = a) (x, l) (* For an explanation of the warning types check the Pull Request #255 *) match(idx_after_start, idx_before_end) with | Some true, Some true -> (* Certainly in bounds on both sides.*) - () + Checks.safe Checks.Category.InvalidMemoryAccess | Some true, Some false -> (* The following matching differentiates the must and may cases*) AnalysisStateUtil.set_mem_safety_flag InvalidDeref; - M.error ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.past_end "Must access array past end" + M.error ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.past_end "Must access array past end"; + Checks.error Checks.Category.InvalidMemoryAccess "Invalid array access: Must access past end" | Some true, None -> AnalysisStateUtil.set_mem_safety_flag InvalidDeref; - M.warn ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.past_end "May access array past end" + M.warn ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.past_end "May access array past end"; + Checks.warn Checks.Category.InvalidMemoryAccess "Invalid array access: May access past end" | Some false, Some true -> AnalysisStateUtil.set_mem_safety_flag InvalidDeref; - M.error ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.before_start "Must access array before start" + M.error ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.before_start "Must access array before start"; + Checks.error Checks.Category.InvalidMemoryAccess "Invalid array access: Must access before start" | None, Some true -> AnalysisStateUtil.set_mem_safety_flag InvalidDeref; - M.warn ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.before_start "May access array before start" + M.warn ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.before_start "May access array before start"; + Checks.warn Checks.Category.InvalidMemoryAccess "Invalid array access: May access before start" | _ -> AnalysisStateUtil.set_mem_safety_flag InvalidDeref; - M.warn ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.unknown "May access array out of bounds" + M.warn ~category:M.Category.Behavior.Undefined.ArrayOutOfBounds.unknown "May access array out of bounds"; + Checks.warn Checks.Category.InvalidMemoryAccess "Invalid array access: May access out of bounds" module TrivialWithLength (Val: LatticeWithInvalidate) (Idx: IntDomain.Z): S with type value = Val.t and type idx = Idx.t = @@ -1023,7 +1028,9 @@ struct type substr = IsNotSubstr | IsSubstrAtIndex0 | IsMaybeSubstr module ArrayOobMessage = M.Category.Behavior.Undefined.ArrayOutOfBounds - let warn_past_end = M.error ~category:ArrayOobMessage.past_end + let warn_past_end ?loc ?tags fmt = + let () = M.error ~category:ArrayOobMessage.past_end ?loc ?tags fmt |> ignore in + Checks.warn Checks.Category.InvalidMemoryAccess fmt let min_nat_of_idx i = Z.max Z.zero (BatOption.default Z.zero (Idx.minimal i)) @@ -1158,25 +1165,35 @@ struct | Some min_i, Some max_i -> if min_i <. Z.zero && max_i <. Z.zero then (M.error ~category:ArrayOobMessage.before_start "Tries to create an array of negative size"; + Checks.error Checks.Category.NegativeArraySize "Tries to create an array of negative size"; Z.zero, Some Z.zero) else if min_i <. Z.zero then (M.warn ~category:ArrayOobMessage.before_start "May try to create an array of negative size"; + Checks.warn Checks.Category.NegativeArraySize "May try to create an array of negative size"; Z.zero, Some max_i) - else - min_i, Some max_i + else ( + Checks.safe Checks.Category.NegativeArraySize; + min_i, Some max_i) | None, Some max_i -> if max_i <. Z.zero then (M.error ~category:ArrayOobMessage.before_start "Tries to create an array of negative size"; + Checks.error Checks.Category.NegativeArraySize "Tries to create an array of negative size"; Z.zero, Some Z.zero) - else + else ( + Checks.safe Checks.Category.NegativeArraySize; Z.zero, Some max_i + ) | Some min_i, None -> if min_i <. Z.zero then (M.warn ~category:ArrayOobMessage.before_start "May try to create an array of negative size"; + Checks.warn Checks.Category.NegativeArraySize "May try to create an array of negative size"; Z.zero, None) - else - min_i, None - | None, None -> Z.zero, None + else ( + Checks.safe Checks.Category.NegativeArraySize; + min_i, None) + | None, None -> + Checks.safe Checks.Category.NegativeArraySize; + Z.zero, None in let size = BatOption.map_default (fun max -> Idx.of_interval ILong (min_i, max)) (Idx.starting ILong min_i) max_i in match Val.is_null v with @@ -1227,6 +1244,7 @@ struct else if Nulls.is_empty Possibly nulls then (warn_past_end "May access array past end: potential buffer overflow"; x) else + let () = Checks.safe Checks.Category.InvalidMemoryAccess in let min_must_null = Nulls.min_elem Definitely nulls in let new_size = Idx.of_int ILong (Z.succ min_must_null) in let min_may_null = Nulls.min_elem Possibly nulls in @@ -1257,13 +1275,15 @@ struct else let n = Z.of_int n in let warn_no_null min_must_null min_may_null = - if Z.geq min_may_null n then - M.warn "Resulting string might not be null-terminated because src doesn't contain a null byte in the first n bytes" + if Z.geq min_may_null n then ( + M.warn "Resulting string might not be null-terminated because src doesn't contain a null byte in the first n bytes"; + Checks.warn Checks.Category.StubCondition "Resulting string might not be null-terminated because src doesn't contain a null byte in the first n bytes") else (match min_must_null with - | Some min_must_null when not (min_must_null >=. n || min_must_null >. min_may_null) -> () + | Some min_must_null when not (min_must_null >=. n || min_must_null >. min_may_null) -> Checks.safe Checks.Category.StubCondition | _ -> - M.warn "Resulting string might not be null-terminated because src might not contain a null byte in the first n bytes" + M.warn "Resulting string might not be null-terminated because src might not contain a null byte in the first n bytes"; + Checks.warn Checks.Category.StubCondition "Resulting string might not be null-terminated because src might not contain a null byte in the first n bytes" ) in (match Idx.minimal size, Idx.maximal size with @@ -1272,13 +1292,19 @@ struct warn_past_end "Array size is smaller than n bytes; can cause a buffer overflow" else if n >. min_size then warn_past_end "Array size might be smaller than n bytes; can cause a buffer overflow" + else + Checks.safe Checks.Category.InvalidMemoryAccess | Some min_size, None -> if n >. min_size then warn_past_end "Array size might be smaller than n bytes; can cause a buffer overflow" + else + Checks.safe Checks.Category.InvalidMemoryAccess | None, Some max_size -> if n >. max_size then warn_past_end "Array size is smaller than n bytes; can cause a buffer overflow" - | None, None -> ()); + else + Checks.safe Checks.Category.InvalidMemoryAccess + | None, None -> Checks.safe Checks.Category.InvalidMemoryAccess); let nulls = (* if definitely no null byte in array, i.e. must_nulls_set = may_nulls_set = empty set *) if Nulls.is_empty Definitely nulls then @@ -1291,6 +1317,7 @@ struct (* if only must_nulls_set empty, remove indexes >= n from may_nulls_set and add all indexes from minimal may null index to n - 1; * warn as in any case, resulting array not guaranteed to contain null byte *) else if Nulls.is_empty Possibly nulls then + let () = Checks.safe Checks.Category.InvalidMemoryAccess in let min_may_null = Nulls.min_elem Possibly nulls in warn_no_null None min_may_null; if min_may_null =. Z.zero then @@ -1299,6 +1326,7 @@ struct let nulls = Nulls.add_interval Possibly (min_may_null, Z.pred n) nulls in Nulls.filter (fun x -> x <. n) nulls else + let () = Checks.safe Checks.Category.InvalidMemoryAccess in let min_must_null = Nulls.min_elem Definitely nulls in let min_may_null = Nulls.min_elem Possibly nulls in (* warn if resulting array may not contain null byte *) @@ -1331,8 +1359,9 @@ struct (warn_past_end "Array might not contain a null byte: potential buffer overflow"; Idx.starting !Cil.kindOfSizeOf (Nulls.min_elem Possibly nulls)) (* else return interval [minimal may null, minimal must null] *) - else - Idx.of_interval !Cil.kindOfSizeOf (Nulls.min_elem Possibly nulls, Nulls.min_elem Definitely nulls) + else ( + Checks.safe Checks.Category.InvalidMemoryAccess; + Idx.of_interval !Cil.kindOfSizeOf (Nulls.min_elem Possibly nulls, Nulls.min_elem Definitely nulls)) let string_copy (dstnulls, dstsize) ((srcnulls, srcsize) as src) n = let must_nulls_set1, may_nulls_set1 = dstnulls in @@ -1344,7 +1373,9 @@ struct (if max_dstsize <. min_srclen then warn_past_end "The length of string src is greater than the allocated size for dest" else if min_dstsize <. max_srclen then - warn_past_end "The length of string src may be greater than the allocated size for dest"); + warn_past_end "The length of string src may be greater than the allocated size for dest" + else + Checks.safe Checks.Category.InvalidMemoryAccess); let must_nulls_set_result = let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in (* get must nulls from src string < minimal size of dest *) @@ -1362,7 +1393,9 @@ struct | Some min_size1, None, Some min_len2, Some max_len2 -> (if min_size1 <. max_len2 then - warn_past_end "The length of string src may be greater than the allocated size for dest"); + warn_past_end "The length of string src may be greater than the allocated size for dest" + else + Checks.safe Checks.Category.InvalidMemoryAccess); let must_nulls_set_result = let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in MustSet.filter ~min_size: min_size2 (Z.gt min_size1) must_nulls_set2' @@ -1376,7 +1409,9 @@ struct (if max_size1 <. min_len2 then warn_past_end "The length of string src is greater than the allocated size for dest" else if min_size1 <. min_len2 then - warn_past_end"The length of string src may be greater than the allocated size for dest"); + warn_past_end"The length of string src may be greater than the allocated size for dest" + else + Checks.safe Checks.Category.InvalidMemoryAccess); (* do not keep any index of dest as no maximal strlen of src *) let must_nulls_set_result = let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in @@ -1388,7 +1423,9 @@ struct ((must_nulls_set_result, may_nulls_set_result), dstsize) | Some min_size1, None, Some min_len2, None -> (if min_size1 <. min_len2 then - warn_past_end "The length of string src may be greater than the allocated size for dest"); + warn_past_end "The length of string src may be greater than the allocated size for dest" + else + Checks.safe Checks.Category.InvalidMemoryAccess); (* do not keep any index of dest as no maximal strlen of src *) let min_size2 = BatOption.default Z.zero (Idx.minimal truncatedsize) in let truncatednulls = Nulls.remove_interval Possibly (Z.zero, min_size1) min_size2 truncatednulls in @@ -1406,21 +1443,31 @@ struct warn_past_end "src doesn't contain a null byte at an index smaller than the size of dest" else if not (Nulls.exists Definitely (Z.gt min_dstsize) srcnulls) then warn_past_end "src may not contain a null byte at an index smaller than the size of dest" + else + Checks.safe Checks.Category.InvalidMemoryAccess | Some min_dstsize, _, _, Some max_srcsize when min_dstsize <. max_srcsize -> if not (Nulls.exists Possibly (Z.gt min_dstsize) srcnulls) then warn_past_end "src doesn't contain a null byte at an index smaller than the size of dest" else if not (Nulls.exists Definitely (Z.gt min_dstsize) srcnulls) then warn_past_end "src may not contain a null byte at an index smaller than the size of dest" + else + Checks.safe Checks.Category.InvalidMemoryAccess | Some min_dstsize, _, _, None -> if not (Nulls.exists Definitely (Z.gt min_dstsize) srcnulls) then warn_past_end "src may not contain a null byte at an index smaller than the size of dest" + else + Checks.safe Checks.Category.InvalidMemoryAccess | _, Some mac_dstsize, _, Some max_srcsize when mac_dstsize <. max_srcsize -> if not (Nulls.exists Definitely (Z.gt mac_dstsize) srcnulls) then warn_past_end "src may not contain a null byte at an index smaller than the size of dest" + else + Checks.safe Checks.Category.InvalidMemoryAccess |_, Some max_dstsize, _, None -> if not (Nulls.exists Definitely (Z.gt max_dstsize) srcnulls) then warn_past_end "src may not contain a null byte at an index smaller than the size of dest" - | _ -> ()) in + else + Checks.safe Checks.Category.InvalidMemoryAccess + | _ -> Checks.safe Checks.Category.InvalidMemoryAccess) in match n with (* strcpy *) @@ -1443,7 +1490,7 @@ struct "The length of the concatenation of the strings in src and dest is greater than the allocated size for dest" else (match maxlen1, maxlen2 with - | Some maxlen1, Some maxlen2 when min_size1 >. (maxlen1 +. maxlen2) -> () + | Some maxlen1, Some maxlen2 when min_size1 >. (maxlen1 +. maxlen2) -> Checks.safe Checks.Category.InvalidMemoryAccess | _ -> warn_past_end "The length of the concatenation of the strings in src and dest may be greater than the allocated size for dest") ); @@ -1634,6 +1681,8 @@ struct warn_past_end "Array of string %s doesn't contain a null byte: buffer overflow" name else if Nulls.is_empty Possibly nulls then warn_past_end "Array of string %s might not contain a null byte: potential buffer overflow" name + else + Checks.safe Checks.Category.InvalidMemoryAccess in warn_missing_nulls nulls1 "1"; warn_missing_nulls nulls2 "2"; @@ -1651,7 +1700,7 @@ struct warn_past_end "The size of the array of string %s might be smaller than n bytes" name | None when n >. min -> warn_past_end "The size of the array of string %s might be smaller than n bytes" name - | _ -> () + | _ -> Checks.safe Checks.Category.InvalidMemoryAccess in warn_size size1 "1"; warn_size size2 "2"; diff --git a/src/cdomain/value/cdomains/intDomain0.ml b/src/cdomain/value/cdomains/intDomain0.ml index ed9e6ea549..d2bb7358d8 100644 --- a/src/cdomain/value/cdomains/intDomain0.ml +++ b/src/cdomain/value/cdomains/intDomain0.ml @@ -83,11 +83,14 @@ let set_overflow_flag ~cast ~underflow ~overflow ik = let sign = if signed then "Signed" else "Unsigned" in match underflow, overflow with | true, true -> - M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190; CWE 191] "%s integer overflow and underflow" sign + M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190; CWE 191] "%s integer overflow and underflow" sign; + Checks.warn Checks.Category.IntegerOverflow "%s integer overflow and underflow" sign | true, false -> - M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 191] "%s integer underflow" sign + M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 191] "%s integer underflow" sign; + Checks.warn Checks.Category.IntegerOverflow "%s integer underflow" sign | false, true -> - M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190] "%s integer overflow" sign + M.warn ~category:M.Category.Integer.overflow ~tags:[CWE 190] "%s integer overflow" sign; + Checks.warn Checks.Category.IntegerOverflow "%s integer overflow" sign | false, false -> assert false let reset_lazy () = diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index a9bbb65444..c8d4f43b42 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -2,17 +2,21 @@ module Kind = struct type t = | Error | Warning - | Success + | Safe + + let is_safe = function + | Safe -> true + | _ -> false let to_yojson x = `String (match x with | Error -> "error" | Warning -> "warning" - | Success -> "success") + | Safe -> "safe") let of_yojson = function | `String "error" -> Ok Error | `String "warning" -> Ok Warning - | `String "success" -> Ok Success + | `String "safe" -> Ok Safe | kind -> Error ("Checks.Kind.of_yojson: Invalid kind :" ^ Yojson.Safe.to_string kind) end @@ -26,6 +30,7 @@ module Category = struct | InvalidPointerSubtraction | DoubleFree | NegativeArraySize + | StubCondition let to_yojson x = `String (match x with | AssersionFaillure -> "Assertion failure" @@ -35,7 +40,8 @@ module Category = struct | InvalidPointerComparison -> "Invalid pointer comparison" | InvalidPointerSubtraction -> "Invalid pointer subtraction" | DoubleFree -> "Double free" - | NegativeArraySize -> "Negative array size") + | NegativeArraySize -> "Negative array size" + | StubCondition -> "Stub condition") let of_yojson = function | `String "Assertion failure" -> Ok AssersionFaillure @@ -52,20 +58,64 @@ end module Check = struct type t = { kind: Kind.t; - category: Category.t; - location: CilType.Location.t; - message: string; + title: Category.t; + range: CilType.Location.t option; + messages: string; } [@@deriving yojson, make] - let checks = ref [] + let to_yojson check = + `Assoc [ + ("kind", Kind.to_yojson check.kind); + ("title", Category.to_yojson check.title); + ("range", match check.range with + | Some loc -> `Assoc [ + ("start", `Assoc [ + ("file", `String loc.file); + ("line", `Int loc.line); + ("column", `Int loc.column) + ]); + ("end", `Assoc [ + ("file", `String loc.file); + ("line", `Int loc.endLine); + ("column", `Int loc.endColumn) + ]) + ] + | None -> `Null); + ("messages", `String check.messages) + ] + + type key = (Category.t * CilType.Location.t option) + let checks : (key, t list) Hashtbl.t = Hashtbl.create 113 + + let add_check check = + if !AnalysisState.should_warn then ( + let check_key = (check.title, check.range) in + match Hashtbl.find_opt checks check_key with + | Some existing_checks -> + if Kind.is_safe check.kind then + () + else if Kind.is_safe (List.hd existing_checks).kind then + Hashtbl.replace checks check_key [check] + else + Hashtbl.replace checks check_key (check :: existing_checks) + | None -> + Hashtbl.add checks check_key [check]) + + let check kind title = + let finish doc = + let loc = Option.map UpdateCil0.getLoc !Node0.current_node in + let messages = GobPretty.show doc in + let check = make ~kind ~title ?range:loc ~messages () in + add_check check + in GoblintCil.Pretty.gprintf finish + - let check kind category location message = - let check = make ~kind ~category ~location ~message in - checks := check :: !checks + let export () = + `List (List.map to_yojson @@ Hashtbl.fold (fun _ checks acc -> List.rev_append checks acc) checks []) end -let error = Check.check Kind.Error +let error category = Check.check Kind.Error category -let warning = Check.check Kind.Warning +let warn category = Check.check Kind.Warning category -let success = Check.check Kind.Success +let safe category = Check.check Kind.Safe category "" diff --git a/src/framework/analysisResult.ml b/src/framework/analysisResult.ml index c1d7fde8a5..d2cc65744d 100644 --- a/src/framework/analysisResult.ml +++ b/src/framework/analysisResult.ml @@ -188,6 +188,14 @@ struct ] in Yojson.Safe.to_channel ~std:true out json + | "dashboard" -> + let timings = Timing.Default.root_with_current () in + let json = `Assoc [ + ("files", Preprocessor.dependencies_to_yojson ()); + ("time", `Float (if get_bool "dbg.timing.enabled" then timings.cputime else -1.)); + ("checks", Checks.Check.export ()); + ] in + Yojson.Safe.to_channel ~std:true out json | "none" -> () | s -> failwith @@ "Unsupported value for option `result`: "^s end From 5edf32770141bf75ba9879757dc58bfaa0fc5fad Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Mon, 30 Jun 2025 16:53:03 +0300 Subject: [PATCH 04/36] changed lines numbering to start from 0 --- src/common/util/checks.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index c8d4f43b42..5d5700462c 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -72,12 +72,12 @@ module Check = struct ("start", `Assoc [ ("file", `String loc.file); ("line", `Int loc.line); - ("column", `Int loc.column) + ("column", `Int (loc.column - 1)) ]); ("end", `Assoc [ ("file", `String loc.file); ("line", `Int loc.endLine); - ("column", `Int loc.endColumn) + ("column", `Int (loc.endColumn - 1)) ]) ] | None -> `Null); From 4641a2e0601716392b60f5c4bab3d1c1c0505d4e Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Mon, 30 Jun 2025 18:05:56 +0300 Subject: [PATCH 05/36] added a missing integer overflow success message --- src/cdomain/value/cdomains/int/intDomTuple.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml index 64f251de46..e96274956c 100644 --- a/src/cdomain/value/cdomains/int/intDomTuple.ml +++ b/src/cdomain/value/cdomains/int/intDomTuple.ml @@ -74,6 +74,7 @@ module IntDomTupleImpl = struct let overflow = overflow_intv && overflow_intv_set && overflow_bf in set_overflow_flag ~cast ~underflow ~overflow ik; ); + if no_ov && not suppress_ovwarn then Checks.safe Checks.Category.IntegerOverflow; no_ov let create2_ovc ik r x ((p1, p2, p3, p4, p5, p6): int_precision) = From b4b39ddd8b670720e3623155d5e347e4d596faf1 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Tue, 1 Jul 2025 17:13:03 +0300 Subject: [PATCH 06/36] fixed invalid success checks --- src/analyses/useAfterFree.ml | 13 ++++++++++--- src/cdomain/value/cdomains/int/intDomTuple.ml | 3 ++- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index c26a396fb8..1d6ef48046 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -109,11 +109,18 @@ struct | ad when not (Queries.AD.is_top ad) -> let warn_for_heap_var v = if HeapVars.mem v (snd state) then begin - if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; + if is_double_free then ( + set_mem_safety_flag InvalidFree; + Checks.warn Checks.Category.DoubleFree "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name) + else ( + set_mem_safety_flag InvalidDeref; + Checks.warn Checks.Category.InvalidMemoryAccess "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name + ); M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name; - Checks.warn Checks.Category.DoubleFree "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name; - end else + end else if is_double_free then Checks.safe Checks.Category.DoubleFree + else + Checks.safe Checks.Category.InvalidMemoryAccess in let pointed_to_heap_vars = Queries.AD.fold (fun addr vars -> diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml index e96274956c..d8eec058be 100644 --- a/src/cdomain/value/cdomains/int/intDomTuple.ml +++ b/src/cdomain/value/cdomains/int/intDomTuple.ml @@ -74,7 +74,8 @@ module IntDomTupleImpl = struct let overflow = overflow_intv && overflow_intv_set && overflow_bf in set_overflow_flag ~cast ~underflow ~overflow ik; ); - if no_ov && not suppress_ovwarn then Checks.safe Checks.Category.IntegerOverflow; + if no_ov && not suppress_ovwarn && not !AnalysisState.executing_speculative_computations then + Checks.safe Checks.Category.IntegerOverflow; no_ov let create2_ovc ik r x ((p1, p2, p3, p4, p5, p6): int_precision) = From e0a4a98e293189191a56b150f78a8047bcd8c5dd Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Wed, 9 Jul 2025 14:09:37 +0300 Subject: [PATCH 07/36] fixed overflow detection --- src/cdomain/value/cdomains/int/intDomTuple.ml | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml index d8eec058be..2d824b4b14 100644 --- a/src/cdomain/value/cdomains/int/intDomTuple.ml +++ b/src/cdomain/value/cdomains/int/intDomTuple.ml @@ -66,16 +66,16 @@ module IntDomTupleImpl = struct let check_ov ?(suppress_ovwarn = false) ~cast ik intv intv_set bf = let no_ov = (no_overflow ik intv) || (no_overflow ik intv_set) || (no_overflow ik bf) in - if not no_ov && not suppress_ovwarn && ( BatOption.is_some intv || BatOption.is_some intv_set || BatOption.is_some bf) then ( - let (_,{underflow=underflow_intv; overflow=overflow_intv}) = match intv with None -> (I2.bot (), {underflow= true; overflow = true}) | Some x -> x in - let (_,{underflow=underflow_intv_set; overflow=overflow_intv_set}) = match intv_set with None -> (I5.bot (), {underflow= true; overflow = true}) | Some x -> x in - let (_,{underflow=underflow_bf; overflow=overflow_bf}) = match bf with None -> (I6.bot (), {underflow= true; overflow = true}) | Some x -> x in - let underflow = underflow_intv && underflow_intv_set && underflow_bf in - let overflow = overflow_intv && overflow_intv_set && overflow_bf in - set_overflow_flag ~cast ~underflow ~overflow ik; - ); - if no_ov && not suppress_ovwarn && not !AnalysisState.executing_speculative_computations then - Checks.safe Checks.Category.IntegerOverflow; + if not suppress_ovwarn && (BatOption.is_some intv || BatOption.is_some intv_set || BatOption.is_some bf) then + if not no_ov then ( + let (_,{underflow=underflow_intv; overflow=overflow_intv}) = match intv with None -> (I2.bot (), {underflow= true; overflow = true}) | Some x -> x in + let (_,{underflow=underflow_intv_set; overflow=overflow_intv_set}) = match intv_set with None -> (I5.bot (), {underflow= true; overflow = true}) | Some x -> x in + let (_,{underflow=underflow_bf; overflow=overflow_bf}) = match bf with None -> (I6.bot (), {underflow= true; overflow = true}) | Some x -> x in + let underflow = underflow_intv && underflow_intv_set && underflow_bf in + let overflow = overflow_intv && overflow_intv_set && overflow_bf in + set_overflow_flag ~cast ~underflow ~overflow ik; + ) else if not !AnalysisState.executing_speculative_computations then + Checks.safe Checks.Category.IntegerOverflow; no_ov let create2_ovc ik r x ((p1, p2, p3, p4, p5, p6): int_precision) = From 8b8d5a70b637a130924ce23afce50b69f31bbdfb Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Sat, 19 Jul 2025 17:13:45 +0300 Subject: [PATCH 08/36] fixed an anoying message with ranges hash in checks --- src/common/util/checks.ml | 87 ++++++++++++++++++++++++++++----------- 1 file changed, 63 insertions(+), 24 deletions(-) diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index 5d5700462c..5510462727 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -3,6 +3,7 @@ module Kind = struct | Error | Warning | Safe + [@@deriving hash, eq, show] let is_safe = function | Safe -> true @@ -21,7 +22,7 @@ module Kind = struct end module Category = struct - type t = + type t = | AssersionFaillure | InvalidMemoryAccess | DivisionByZero @@ -31,6 +32,7 @@ module Category = struct | DoubleFree | NegativeArraySize | StubCondition + [@@deriving hash, eq, show] let to_yojson x = `String (match x with | AssersionFaillure -> "Assertion failure" @@ -61,7 +63,7 @@ module Check = struct title: Category.t; range: CilType.Location.t option; messages: string; - } [@@deriving yojson, make] + } [@@deriving make, hash, eq] let to_yojson check = `Assoc [ @@ -84,34 +86,71 @@ module Check = struct ("messages", `String check.messages) ] - type key = (Category.t * CilType.Location.t option) - let checks : (key, t list) Hashtbl.t = Hashtbl.create 113 + let pp fmt check = + Format.fprintf fmt "Check: %a: %s at %a" + Kind.pp check.kind + check.messages + (Format.pp_print_option CilType.Location.pp) check.range + + type check_t = t + let check_t_to_yojson = to_yojson + module CheckMap = Hashtbl.Make (struct + type t = check_t + let equal = equal + let hash = hash + end) + + + module CategoryLocationMap = Hashtbl.Make (struct + type t = Category.t * CilType.Location.t [@@deriving hash, eq] + end) + + type key = Category.t * CilType.Location.t option [@@deriving yojson] + + let checks_list : (bool ref * unit CheckMap.t) CategoryLocationMap.t = CategoryLocationMap.create 113 let add_check check = + match check.range with + | Some range -> ( + (* Mark all ranges as synthetic for hash purposes *) + let range = { range with synthetic = true } in + let check = { check with range = Some range } in + let check_key = (check.title, range) in + match CategoryLocationMap.find_opt checks_list check_key with + | Some (safe, existing_checks) -> + if !safe && Kind.is_safe check.kind then + CheckMap.replace existing_checks check () + else if not @@ Kind.is_safe check.kind then ( + if !safe then CheckMap.clear existing_checks; + safe := false; + CheckMap.replace existing_checks check () + ) + | None -> + let table = CheckMap.create 10 in + CheckMap.replace table check (); + CategoryLocationMap.replace checks_list check_key (ref (Kind.is_safe check.kind), table)) + | None -> + () + + let check kind title fmt = if !AnalysisState.should_warn then ( - let check_key = (check.title, check.range) in - match Hashtbl.find_opt checks check_key with - | Some existing_checks -> - if Kind.is_safe check.kind then - () - else if Kind.is_safe (List.hd existing_checks).kind then - Hashtbl.replace checks check_key [check] - else - Hashtbl.replace checks check_key (check :: existing_checks) - | None -> - Hashtbl.add checks check_key [check]) - - let check kind title = - let finish doc = - let loc = Option.map UpdateCil0.getLoc !Node0.current_node in - let messages = GobPretty.show doc in - let check = make ~kind ~title ?range:loc ~messages () in - add_check check - in GoblintCil.Pretty.gprintf finish + let finish doc = + let loc = Option.map UpdateCil0.getLoc !Node0.current_node in + let messages = GobPretty.show doc in + let check = make ~kind ~title ?range:loc ~messages () in + add_check check in + GoblintCil.Pretty.gprintf finish fmt) + else + GobPretty.igprintf () fmt let export () = - `List (List.map to_yojson @@ Hashtbl.fold (fun _ checks acc -> List.rev_append checks acc) checks []) + `List ( + List.map to_yojson @@ CategoryLocationMap.fold ( + fun _ (checks: (bool ref * unit CheckMap.t)) acc -> + List.rev_append (CheckMap.to_seq_keys @@ snd checks |> List.of_seq) acc + ) checks_list [] + ) end let error category = Check.check Kind.Error category From 7125a02499cf9accb7c03f8dc4776bf7b2e41293 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Fri, 25 Jul 2025 17:01:00 +0300 Subject: [PATCH 09/36] fixed an issue where safe checks are put on functions --- src/cdomain/value/cdomains/int/intDomTuple.ml | 5 +++-- src/common/util/checks.ml | 6 +++++- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml index 2d824b4b14..e3a532ed33 100644 --- a/src/cdomain/value/cdomains/int/intDomTuple.ml +++ b/src/cdomain/value/cdomains/int/intDomTuple.ml @@ -74,8 +74,9 @@ module IntDomTupleImpl = struct let underflow = underflow_intv && underflow_intv_set && underflow_bf in let overflow = overflow_intv && overflow_intv_set && overflow_bf in set_overflow_flag ~cast ~underflow ~overflow ik; - ) else if not !AnalysisState.executing_speculative_computations then - Checks.safe Checks.Category.IntegerOverflow; + ) else if not !AnalysisState.executing_speculative_computations then ( + Checks.safe Checks.Category.IntegerOverflow + ); no_ov let create2_ovc ik r x ((p1, p2, p3, p4, p5, p6): int_precision) = diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index 5510462727..b79a400505 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -157,4 +157,8 @@ let error category = Check.check Kind.Error category let warn category = Check.check Kind.Warning category -let safe category = Check.check Kind.Safe category "" +let safe category = + match !Node0.current_node with + | Some (Statement _) -> + Check.check Kind.Safe category "" + | _ -> () From aabb778c65af88013b18aae39616fa21df163e19 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Fri, 25 Jul 2025 17:51:25 +0300 Subject: [PATCH 10/36] fixed messages according to the last goblint version --- src/analyses/memOutOfBounds.ml | 3 ++- src/cdomain/value/cdomains/arrayDomain.ml | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 2f760f0772..f59441df3a 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -90,7 +90,8 @@ struct | Addr (v, _) -> if hasAttribute "goblint_cil_nested" v.vattr then ( set_mem_safety_flag InvalidDeref; - M.warn "Var %a is potentially accessed out-of-scope. Invalid memory access may occur" CilType.Varinfo.pretty v + M.warn "Var %a is potentially accessed out-of-scope. Invalid memory access may occur" CilType.Varinfo.pretty v; + Checks.warn Checks.Category.InvalidMemoryAccess "Var %a is potentially accessed out-of-scope. Invalid memory access may occur" CilType.Varinfo.pretty v ); begin match Cil.unrollType v.vtype with | TArray (item_typ, _, _) -> diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml index e2564f8798..c5283ddc37 100644 --- a/src/cdomain/value/cdomains/arrayDomain.ml +++ b/src/cdomain/value/cdomains/arrayDomain.ml @@ -1030,7 +1030,7 @@ struct module ArrayOobMessage = M.Category.Behavior.Undefined.ArrayOutOfBounds let warn_past_end ?loc ?tags fmt = let () = M.error ~category:ArrayOobMessage.past_end ?loc ?tags fmt |> ignore in - Checks.warn Checks.Category.InvalidMemoryAccess fmt + Checks.error Checks.Category.InvalidMemoryAccess fmt let min_nat_of_idx i = Z.max Z.zero (BatOption.default Z.zero (Idx.minimal i)) From c0826cf13a3760831bd3b1f580339cbfa8ea2e79 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Tue, 29 Jul 2025 18:02:52 +0300 Subject: [PATCH 11/36] added the possibility to add messages to safe --- src/common/util/checks.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index b79a400505..9bf711cd8e 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -157,8 +157,8 @@ let error category = Check.check Kind.Error category let warn category = Check.check Kind.Warning category -let safe category = +let safe ?(message = "") category = match !Node0.current_node with | Some (Statement _) -> - Check.check Kind.Safe category "" + Check.check Kind.Safe category "%s" message | _ -> () From 6e0b95a29c1b59369d1f60a0c539472eafe5023f Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Wed, 30 Jul 2025 14:38:32 +0300 Subject: [PATCH 12/36] removed constant overflow safe checks --- src/cdomain/value/cdomains/int/intDomTuple.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml index 1e6533c12b..9c97ca87e0 100644 --- a/src/cdomain/value/cdomains/int/intDomTuple.ml +++ b/src/cdomain/value/cdomains/int/intDomTuple.ml @@ -64,9 +64,9 @@ module IntDomTupleImpl = struct | Some(_, {underflow; overflow}) -> not (underflow || overflow) | _ -> false - let check_ov ?(suppress_ovwarn = false) ~cast ik intv intv_set bf = + let check_ov ?(suppress_ovwarn = false) ?(no_safe = false) ~cast ik intv intv_set bf = let no_ov = (no_overflow ik intv) || (no_overflow ik intv_set) || (no_overflow ik bf) in - if not suppress_ovwarn && (BatOption.is_some intv || BatOption.is_some intv_set || BatOption.is_some bf) then + if not suppress_ovwarn && (BatOption.is_some intv || BatOption.is_some intv_set || BatOption.is_some bf) then ( if not no_ov then ( let (_,{underflow=underflow_intv; overflow=overflow_intv}) = match intv with None -> (I2.bot (), {underflow= true; overflow = true}) | Some x -> x in let (_,{underflow=underflow_intv_set; overflow=overflow_intv_set}) = match intv_set with None -> (I5.bot (), {underflow= true; overflow = true}) | Some x -> x in @@ -74,9 +74,10 @@ module IntDomTupleImpl = struct let underflow = underflow_intv && underflow_intv_set && underflow_bf in let overflow = overflow_intv && overflow_intv_set && overflow_bf in set_overflow_flag ~cast ~underflow ~overflow ik; - ) else if not !AnalysisState.executing_speculative_computations then ( - Checks.safe Checks.Category.IntegerOverflow - ); + ) else if not !AnalysisState.executing_speculative_computations && not no_safe then ( + Checks.safe Checks.Category.IntegerOverflow ~message:("Cast: " ^ string_of_bool cast) + ) + ); no_ov let create2_ovc ik r x ((p1, p2, p3, p4, p5, p6): int_precision) = @@ -85,7 +86,7 @@ module IntDomTupleImpl = struct let intv = f p2 @@ r.fi2_ovc (module I2) in let intv_set = f p5 @@ r.fi2_ovc (module I5) in let bf = f p6 @@ r.fi2_ovc (module I6) in - ignore (check_ov ~cast:false ik intv intv_set bf); + ignore (check_ov ~no_safe:true ~cast:false ik intv intv_set bf); map @@ f p1 @@ r.fi2_ovc (module I1), map @@ f p2 @@ r.fi2_ovc (module I2), map @@ f p3 @@ r.fi2_ovc (module I3), map @@ f p4 @@ r.fi2_ovc (module I4), map @@ f p5 @@ r.fi2_ovc (module I5) , map @@ f p6 @@ r.fi2_ovc (module I6) let create2_ovc ik r x = (* use where values are introduced *) From 80322bc2a0fab041033e0af4da63b01e37d78d97 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Wed, 30 Jul 2025 15:28:10 +0300 Subject: [PATCH 13/36] fixed a bug with warning messages order --- src/cdomain/value/cdomains/arrayDomain.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml index c5283ddc37..7a1fe8392c 100644 --- a/src/cdomain/value/cdomains/arrayDomain.ml +++ b/src/cdomain/value/cdomains/arrayDomain.ml @@ -1029,8 +1029,8 @@ struct module ArrayOobMessage = M.Category.Behavior.Undefined.ArrayOutOfBounds let warn_past_end ?loc ?tags fmt = - let () = M.error ~category:ArrayOobMessage.past_end ?loc ?tags fmt |> ignore in - Checks.error Checks.Category.InvalidMemoryAccess fmt + let () = Checks.error Checks.Category.InvalidMemoryAccess fmt |> ignore in + M.error ~category:ArrayOobMessage.past_end ?loc ?tags fmt let min_nat_of_idx i = Z.max Z.zero (BatOption.default Z.zero (Idx.minimal i)) From 84ed5fc2ef457c01c848b0e0f287c3ebf28d019b Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Mon, 20 Oct 2025 17:11:02 +0200 Subject: [PATCH 14/36] quoted the paper from which the check.ml file is inspired --- src/common/util/checks.ml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index 9bf711cd8e..5d419b7036 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -1,3 +1,11 @@ +(** + Implements a method described in this paper from Raphaël Monat, + Abdelraouf Ouadjaout and Antoine Miné : https://inria.hal.science/hal-04652657v2 + + This allows to track checks performed during the analysis, and to mark whether they are safe, + unsafe or unknown (resp. Safe, Error, Warning). +*) + module Kind = struct type t = | Error From 8d46b14907d43ce5f1b78b4687e5cd0705d9f14d Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Fri, 28 Nov 2025 14:51:05 +0100 Subject: [PATCH 15/36] replaced 'let unit in' in arrayDomain --- src/cdomain/value/cdomains/arrayDomain.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml index 1189ad60a1..dcc7fa4082 100644 --- a/src/cdomain/value/cdomains/arrayDomain.ml +++ b/src/cdomain/value/cdomains/arrayDomain.ml @@ -998,7 +998,7 @@ struct module ArrayOobMessage = M.Category.Behavior.Undefined.ArrayOutOfBounds let warn_past_end ?loc ?tags fmt = - let () = Checks.error Checks.Category.InvalidMemoryAccess fmt |> ignore in + Checks.error Checks.Category.InvalidMemoryAccess fmt |> ignore; M.error ~category:ArrayOobMessage.past_end ?loc ?tags fmt let min_nat_of_idx i = Z.max Z.zero (BatOption.default Z.zero (Idx.minimal i)) @@ -1213,7 +1213,7 @@ struct else if Nulls.is_empty Possibly nulls then (warn_past_end "May access array past end: potential buffer overflow"; x) else - let () = Checks.safe Checks.Category.InvalidMemoryAccess in + (Checks.safe Checks.Category.InvalidMemoryAccess; let min_must_null = Nulls.min_elem Definitely nulls in let new_size = Idx.of_int ILong (Z.succ min_must_null) in let min_may_null = Nulls.min_elem Possibly nulls in @@ -1233,7 +1233,7 @@ struct let nulls' = Nulls.remove_all Possibly nulls in Nulls.filter (Z.leq min_must_null) nulls' in - (nulls, new_size) + (nulls, new_size)) (** [to_n_string index_set n] returns an abstract value with a potential null byte * marking the end of the string and if needed followed by further null bytes to obtain @@ -1286,16 +1286,16 @@ struct (* if only must_nulls_set empty, remove indexes >= n from may_nulls_set and add all indexes from minimal may null index to n - 1; * warn as in any case, resulting array not guaranteed to contain null byte *) else if Nulls.is_empty Possibly nulls then - let () = Checks.safe Checks.Category.InvalidMemoryAccess in + (Checks.safe Checks.Category.InvalidMemoryAccess; let min_may_null = Nulls.min_elem Possibly nulls in warn_no_null None min_may_null; if min_may_null =. Z.zero then Nulls.add_all Possibly nulls else let nulls = Nulls.add_interval Possibly (min_may_null, Z.pred n) nulls in - Nulls.filter (fun x -> x <. n) nulls + Nulls.filter (fun x -> x <. n) nulls) else - let () = Checks.safe Checks.Category.InvalidMemoryAccess in + (Checks.safe Checks.Category.InvalidMemoryAccess; let min_must_null = Nulls.min_elem Definitely nulls in let min_may_null = Nulls.min_elem Possibly nulls in (* warn if resulting array may not contain null byte *) @@ -1313,7 +1313,7 @@ struct else let nulls = Nulls.remove_all Possibly nulls in let nulls = Nulls.add_interval Possibly (min_may_null, Z.pred n) nulls in - Nulls.filter (fun x -> x <. n) nulls + Nulls.filter (fun x -> x <. n) nulls) in (nulls, Idx.of_int ILong n) From 1d2a46c64a9366c5fb357ccd785407de407874f4 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Fri, 28 Nov 2025 14:51:23 +0100 Subject: [PATCH 16/36] added a message to valid check of assertions --- src/analyses/assert.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/assert.ml b/src/analyses/assert.ml index f0afbaa4ff..d695f1f751 100644 --- a/src/analyses/assert.ml +++ b/src/analyses/assert.ml @@ -39,7 +39,7 @@ struct if refine then raise Analyses.Deadcode else man.local | `Lifted true -> warn (M.success ~category:Assert "%s") ("Assertion \"" ^ expr ^ "\" will succeed"); - Checks.safe Checks.Category.AssersionFaillure; + Checks.safe Checks.Category.AssersionFaillure ~message:("Assertion \"%s\" will succeed"); man.local | `Bot -> M.error ~category:Assert "%s" ("Assertion \"" ^ expr ^ "\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)"); From cff6077bc457bc6d9c2b79063fd20b32e4a5f281 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Fri, 28 Nov 2025 15:33:48 +0100 Subject: [PATCH 17/36] added back "dashboard" output kind --- src/config/options.schema.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 52f98ac84c..75d491ef41 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -79,9 +79,9 @@ "result": { "title": "result", "description": - "Result style: none, fast_xml, json, pretty, pretty-deterministic, json-messages, sarif.", + "Result style: none, fast_xml, json, pretty, pretty-deterministic, json-messages, sarif, dashboard.", "type": "string", - "enum": ["none", "fast_xml", "g2html", "xslt", "json", "pretty", "pretty-deterministic", "json-messages", "sarif"], + "enum": ["none", "fast_xml", "g2html", "xslt", "json", "pretty", "pretty-deterministic", "json-messages", "sarif", "dashboard"], "default": "none" }, "solver": { From 5b26dd0f8ee82643aba3d0135bda34ee38dedb13 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Tue, 2 Dec 2025 16:58:43 +0100 Subject: [PATCH 18/36] removed unused type --- src/common/util/checks.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index 5d419b7036..97a3ca63e1 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -113,7 +113,6 @@ module Check = struct type t = Category.t * CilType.Location.t [@@deriving hash, eq] end) - type key = Category.t * CilType.Location.t option [@@deriving yojson] let checks_list : (bool ref * unit CheckMap.t) CategoryLocationMap.t = CategoryLocationMap.create 113 From 9b1aaa8d93aa92ea2d1402cecca4a4c179157712 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Tue, 2 Dec 2025 16:59:19 +0100 Subject: [PATCH 19/36] replaced recursive type in module CheckMap in checks.ml by a non recursive one --- src/common/util/checks.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index 97a3ca63e1..9fb0777999 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -99,11 +99,8 @@ module Check = struct Kind.pp check.kind check.messages (Format.pp_print_option CilType.Location.pp) check.range - - type check_t = t - let check_t_to_yojson = to_yojson module CheckMap = Hashtbl.Make (struct - type t = check_t + type nonrec t = t let equal = equal let hash = hash end) From d0023557c0a0fe6e4caceecaafeddd8aa387edea Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Tue, 2 Dec 2025 17:07:37 +0100 Subject: [PATCH 20/36] moved the CheckMap related code to the top level of the checks.ml --- src/common/util/checks.ml | 121 +++++++++++++++++++------------------- 1 file changed, 61 insertions(+), 60 deletions(-) diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index 9fb0777999..c2ac0aab11 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -99,70 +99,71 @@ module Check = struct Kind.pp check.kind check.messages (Format.pp_print_option CilType.Location.pp) check.range - module CheckMap = Hashtbl.Make (struct - type nonrec t = t - let equal = equal - let hash = hash - end) - - - module CategoryLocationMap = Hashtbl.Make (struct - type t = Category.t * CilType.Location.t [@@deriving hash, eq] - end) - - - let checks_list : (bool ref * unit CheckMap.t) CategoryLocationMap.t = CategoryLocationMap.create 113 - - let add_check check = - match check.range with - | Some range -> ( - (* Mark all ranges as synthetic for hash purposes *) - let range = { range with synthetic = true } in - let check = { check with range = Some range } in - let check_key = (check.title, range) in - match CategoryLocationMap.find_opt checks_list check_key with - | Some (safe, existing_checks) -> - if !safe && Kind.is_safe check.kind then - CheckMap.replace existing_checks check () - else if not @@ Kind.is_safe check.kind then ( - if !safe then CheckMap.clear existing_checks; - safe := false; - CheckMap.replace existing_checks check () - ) - | None -> - let table = CheckMap.create 10 in - CheckMap.replace table check (); - CategoryLocationMap.replace checks_list check_key (ref (Kind.is_safe check.kind), table)) - | None -> - () - - let check kind title fmt = - if !AnalysisState.should_warn then ( - let finish doc = - let loc = Option.map UpdateCil0.getLoc !Node0.current_node in - let messages = GobPretty.show doc in - let check = make ~kind ~title ?range:loc ~messages () in - add_check check in - GoblintCil.Pretty.gprintf finish fmt) - else - GobPretty.igprintf () fmt - - - let export () = - `List ( - List.map to_yojson @@ CategoryLocationMap.fold ( - fun _ (checks: (bool ref * unit CheckMap.t)) acc -> - List.rev_append (CheckMap.to_seq_keys @@ snd checks |> List.of_seq) acc - ) checks_list [] - ) end -let error category = Check.check Kind.Error category - -let warn category = Check.check Kind.Warning category +module CheckMap = Hashtbl.Make (struct + type t = Check.t + let equal = Check.equal + let hash = Check.hash + end) + + +module CategoryLocationMap = Hashtbl.Make (struct + type t = Category.t * CilType.Location.t [@@deriving hash, eq] + end) + + +let checks_list : (bool ref * unit CheckMap.t) CategoryLocationMap.t = CategoryLocationMap.create 113 + +let add_check check = + match check.Check.range with + | Some range -> ( + (* Mark all ranges as synthetic for hash purposes *) + let range = { range with synthetic = true } in + let check = { check with range = Some range } in + let check_key = (check.title, range) in + match CategoryLocationMap.find_opt checks_list check_key with + | Some (safe, existing_checks) -> + if !safe && Kind.is_safe check.kind then + CheckMap.replace existing_checks check () + else if not @@ Kind.is_safe check.kind then ( + if !safe then CheckMap.clear existing_checks; + safe := false; + CheckMap.replace existing_checks check () + ) + | None -> + let table = CheckMap.create 10 in + CheckMap.replace table check (); + CategoryLocationMap.replace checks_list check_key (ref (Kind.is_safe check.kind), table)) + | None -> + () + +let check kind title fmt = + if !AnalysisState.should_warn then ( + let finish doc = + let loc = Option.map UpdateCil0.getLoc !Node0.current_node in + let messages = GobPretty.show doc in + let check = Check.make ~kind ~title ?range:loc ~messages () in + add_check check in + GoblintCil.Pretty.gprintf finish fmt) + else + GobPretty.igprintf () fmt + + +let export () = + `List ( + List.map Check.to_yojson @@ CategoryLocationMap.fold ( + fun _ (checks: (bool ref * unit CheckMap.t)) acc -> + List.rev_append (CheckMap.to_seq_keys @@ snd checks |> List.of_seq) acc + ) checks_list [] + ) + +let error category = check Kind.Error category + +let warn category = check Kind.Warning category let safe ?(message = "") category = match !Node0.current_node with | Some (Statement _) -> - Check.check Kind.Safe category "%s" message + check Kind.Safe category "%s" message | _ -> () From 0f0c3e32b6c3d312ef699f62b94e16fb9274aa72 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Tue, 2 Dec 2025 17:15:59 +0100 Subject: [PATCH 21/36] added documentation to the check_list variable --- src/common/util/checks.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index c2ac0aab11..b9444330dc 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -114,6 +114,10 @@ module CategoryLocationMap = Hashtbl.Make (struct let checks_list : (bool ref * unit CheckMap.t) CategoryLocationMap.t = CategoryLocationMap.create 113 +(** Store the list of checks raised by the analysis. The [bool ref] stores whether all checks in the map are safe. + The [unit CheckMap.t] is the set of checks associated with the given [Category.t * CilType.Location.t] pair. + The [bool] is a reference to avoid having to use the [update] function when updating the value. The [CheckMap.t] is mutable anyway + so it is not a problem. *) let add_check check = match check.Check.range with From ec7564be97c6625b9e15f0f96b3d2772b63cbe48 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Tue, 2 Dec 2025 17:27:10 +0100 Subject: [PATCH 22/36] fix a wrong function path --- src/framework/analysisResultOutput.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/framework/analysisResultOutput.ml b/src/framework/analysisResultOutput.ml index 335bb4d1aa..29f2006f8e 100644 --- a/src/framework/analysisResultOutput.ml +++ b/src/framework/analysisResultOutput.ml @@ -97,7 +97,7 @@ struct let json = `Assoc [ ("files", Preprocessor.dependencies_to_yojson ()); ("time", `Float (if get_bool "dbg.timing.enabled" then timings.cputime else -1.)); - ("checks", Checks.Check.export ()); + ("checks", Checks.export ()); ] in Yojson.Safe.to_channel ~std:true out json | "none" -> () From 172956accc91098495b7d3ea9cb9cc1b716e0c60 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Wed, 3 Dec 2025 10:17:18 +0100 Subject: [PATCH 23/36] removed incorrect warnings --- src/analyses/base.ml | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 53373f9f84..67f6b37eb1 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1189,10 +1189,8 @@ struct if AD.is_top fp then ( if AD.cardinal fp = 1 then ( M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval; - Checks.warn Checks.Category.InvalidMemoryAccess "Unknown call to function %a." d_exp fval ) else ( M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval; - Checks.warn Checks.Category.InvalidMemoryAccess "Function pointer %a may contain unknown functions." d_exp fval ) ); fp From b6ce5f796b9429657873b9ceb537d913310ec5d0 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Wed, 3 Dec 2025 10:18:35 +0100 Subject: [PATCH 24/36] removed incorrect warnings --- src/analyses/base.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 67f6b37eb1..3123543bd0 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2237,7 +2237,6 @@ struct let special_unknown_invalidate man f args = (if CilType.Varinfo.equal f dummyFunDec.svar then ( M.warn ~category:Imprecise ~tags:[Category Call] "Unknown function ptr called"; - Checks.warn Checks.Category.InvalidMemoryAccess "Unknown function ptr called" )); let desc = LF.find f in let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in From a3cad06c195797ac732c35442eeed7837d2085a9 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Wed, 3 Dec 2025 10:21:33 +0100 Subject: [PATCH 25/36] fixed a typo --- src/analyses/assert.ml | 8 ++++---- src/common/util/checks.ml | 6 +++--- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/analyses/assert.ml b/src/analyses/assert.ml index d695f1f751..047e31ddec 100644 --- a/src/analyses/assert.ml +++ b/src/analyses/assert.ml @@ -35,19 +35,19 @@ struct match Queries.eval_bool (Analyses.ask_of_man man) e with | `Lifted false -> warn (M.error ~category:Assert "%s") ~annot:"FAIL" ("Assertion \"" ^ expr ^ "\" will fail."); - Checks.error Checks.Category.AssersionFaillure "Assertion \"%s\" will fail." expr; + Checks.error Checks.Category.AssertionFailure "Assertion \"%s\" will fail." expr; if refine then raise Analyses.Deadcode else man.local | `Lifted true -> warn (M.success ~category:Assert "%s") ("Assertion \"" ^ expr ^ "\" will succeed"); - Checks.safe Checks.Category.AssersionFaillure ~message:("Assertion \"%s\" will succeed"); + Checks.safe Checks.Category.AssertionFailure ~message:("Assertion \"%s\" will succeed"); man.local | `Bot -> M.error ~category:Assert "%s" ("Assertion \"" ^ expr ^ "\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)"); - Checks.error Checks.Category.AssersionFaillure "Assertion \"%s\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)" expr; + Checks.error Checks.Category.AssertionFailure "Assertion \"%s\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)" expr; man.local | `Top -> warn (M.warn ~category:Assert "%s") ~annot:"UNKNOWN" ("Assertion \"" ^ expr ^ "\" is unknown."); - Checks.warn Checks.Category.AssersionFaillure "Assertion \"%s\" is unknown." expr; + Checks.warn Checks.Category.AssertionFailure "Assertion \"%s\" is unknown." expr; man.local let special man (lval: lval option) (f:varinfo) (args:exp list) : D.t = diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index b9444330dc..5edc5cf21e 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -31,7 +31,7 @@ end module Category = struct type t = - | AssersionFaillure + | AssertionFailure | InvalidMemoryAccess | DivisionByZero | IntegerOverflow @@ -43,7 +43,7 @@ module Category = struct [@@deriving hash, eq, show] let to_yojson x = `String (match x with - | AssersionFaillure -> "Assertion failure" + | AssertionFailure -> "Assertion failure" | InvalidMemoryAccess -> "Invalid memory access" | DivisionByZero -> "Division by zero" | IntegerOverflow -> "Integer overflow" @@ -54,7 +54,7 @@ module Category = struct | StubCondition -> "Stub condition") let of_yojson = function - | `String "Assertion failure" -> Ok AssersionFaillure + | `String "Assertion failure" -> Ok AssertionFailure | `String "Invalid memory access" -> Ok InvalidMemoryAccess | `String "Division by zero" -> Ok DivisionByZero | `String "Integer overflow" -> Ok IntegerOverflow From 0f1e6b9910196adcbc4de2b6f426caa1e50f1a74 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Tue, 9 Dec 2025 15:21:57 +0100 Subject: [PATCH 26/36] fixed a typo --- src/common/util/checks.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index 5edc5cf21e..7ffe6437c7 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -26,7 +26,7 @@ module Kind = struct | `String "error" -> Ok Error | `String "warning" -> Ok Warning | `String "safe" -> Ok Safe - | kind -> Error ("Checks.Kind.of_yojson: Invalid kind :" ^ Yojson.Safe.to_string kind) + | kind -> Error ("Checks.Kind.of_yojson: Invalid kind: " ^ Yojson.Safe.to_string kind) end module Category = struct @@ -62,7 +62,7 @@ module Category = struct | `String "Invalid pointer subtraction" -> Ok InvalidPointerSubtraction | `String "Double free" -> Ok DoubleFree | `String "Negative array size" -> Ok NegativeArraySize - | category -> Error ("Checks.Category.of_yojson: Invalid category :" ^ Yojson.Safe.to_string category) + | category -> Error ("Checks.Category.of_yojson: Invalid category: " ^ Yojson.Safe.to_string category) end module Check = struct From 12c37432936506064e6a23619a462a9635fedf5e Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Tue, 9 Dec 2025 15:22:48 +0100 Subject: [PATCH 27/36] added a missing case in Category of_yojson function --- src/common/util/checks.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index 7ffe6437c7..be95b1ebce 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -62,6 +62,7 @@ module Category = struct | `String "Invalid pointer subtraction" -> Ok InvalidPointerSubtraction | `String "Double free" -> Ok DoubleFree | `String "Negative array size" -> Ok NegativeArraySize + | `String "Stub condition" -> Ok StubCondition | category -> Error ("Checks.Category.of_yojson: Invalid category: " ^ Yojson.Safe.to_string category) end From 798b44c2cfd8a363361b8628dbf302f674eeb1c3 Mon Sep 17 00:00:00 2001 From: Robotechnic Date: Tue, 9 Dec 2025 15:25:07 +0100 Subject: [PATCH 28/36] fixed safe messages --- src/analyses/assert.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/assert.ml b/src/analyses/assert.ml index 047e31ddec..d383b8db2f 100644 --- a/src/analyses/assert.ml +++ b/src/analyses/assert.ml @@ -39,7 +39,7 @@ struct if refine then raise Analyses.Deadcode else man.local | `Lifted true -> warn (M.success ~category:Assert "%s") ("Assertion \"" ^ expr ^ "\" will succeed"); - Checks.safe Checks.Category.AssertionFailure ~message:("Assertion \"%s\" will succeed"); + Checks.safe Checks.Category.AssertionFailure ~message:("Assertion \"" ^ expr ^ "\" will succeed"); man.local | `Bot -> M.error ~category:Assert "%s" ("Assertion \"" ^ expr ^ "\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)"); From bf9996b5c12bd3891687ffa2bae9a64bdf1ec55e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 9 Dec 2025 16:27:16 +0200 Subject: [PATCH 29/36] Trim trailing whitespace in Checks --- src/common/util/checks.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index 5edc5cf21e..5b9a67963e 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -1,8 +1,8 @@ (** - Implements a method described in this paper from Raphaël Monat, + Implements a method described in this paper from Raphaël Monat, Abdelraouf Ouadjaout and Antoine Miné : https://inria.hal.science/hal-04652657v2 - This allows to track checks performed during the analysis, and to mark whether they are safe, + This allows to track checks performed during the analysis, and to mark whether they are safe, unsafe or unknown (resp. Safe, Error, Warning). *) @@ -114,8 +114,8 @@ module CategoryLocationMap = Hashtbl.Make (struct let checks_list : (bool ref * unit CheckMap.t) CategoryLocationMap.t = CategoryLocationMap.create 113 -(** Store the list of checks raised by the analysis. The [bool ref] stores whether all checks in the map are safe. - The [unit CheckMap.t] is the set of checks associated with the given [Category.t * CilType.Location.t] pair. +(** Store the list of checks raised by the analysis. The [bool ref] stores whether all checks in the map are safe. + The [unit CheckMap.t] is the set of checks associated with the given [Category.t * CilType.Location.t] pair. The [bool] is a reference to avoid having to use the [update] function when updating the value. The [CheckMap.t] is mutable anyway so it is not a problem. *) From af1acd59d735565f0f30e5cb2c9d7337dbdbfa9d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 9 Dec 2025 16:38:27 +0200 Subject: [PATCH 30/36] Make safe check messages also format strings --- src/analyses/assert.ml | 2 +- src/cdomain/value/cdomains/int/intDomTuple.ml | 2 +- src/common/util/checks.ml | 11 +++++++++-- 3 files changed, 11 insertions(+), 4 deletions(-) diff --git a/src/analyses/assert.ml b/src/analyses/assert.ml index 22cf470713..1d500f7f31 100644 --- a/src/analyses/assert.ml +++ b/src/analyses/assert.ml @@ -27,7 +27,7 @@ struct if refine then raise Analyses.Deadcode else man.local | `Lifted true -> assert_msg Success "Assertion \"%a\" will succeed" CilType.Exp.pretty e; - Checks.safe Checks.Category.AssertionFailure ~message:("Assertion \"%s\" will succeed"); + Checks.safe_msg Checks.Category.AssertionFailure "Assertion \"%a\" will succeed" CilType.Exp.pretty e; man.local | `Bot -> M.error ~category:Assert "Assertion \"%a\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)" CilType.Exp.pretty e; diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml index f5b33b455e..317ba460d8 100644 --- a/src/cdomain/value/cdomains/int/intDomTuple.ml +++ b/src/cdomain/value/cdomains/int/intDomTuple.ml @@ -75,7 +75,7 @@ module IntDomTupleImpl = struct let overflow = overflow_intv && overflow_intv_set && overflow_bf in set_overflow_flag ~cast ~underflow ~overflow ik; ) else if not !AnalysisState.executing_speculative_computations && not no_safe then ( - Checks.safe Checks.Category.IntegerOverflow ~message:("Cast: " ^ string_of_bool cast) + Checks.safe_msg Checks.Category.IntegerOverflow "Cast: %B" cast ) ); no_ov diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index 5b9a67963e..d8060039a9 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -166,8 +166,15 @@ let error category = check Kind.Error category let warn category = check Kind.Warning category -let safe ?(message = "") category = +let safe category = match !Node0.current_node with | Some (Statement _) -> - check Kind.Safe category "%s" message + check Kind.Safe category "" | _ -> () + +let safe_msg category = + match !Node0.current_node with + | Some (Statement _) -> + check Kind.Safe category + | _ -> + GobPretty.igprintf () From 2332951902e56f887f52c79c8e99552528bbaa71 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 9 Dec 2025 16:43:12 +0200 Subject: [PATCH 31/36] Document Checks in Goblint_lib --- src/goblint_lib.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index d69eb8101e..3283697120 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -327,6 +327,7 @@ module CilMaps = CilMaps module Messages = Messages module Logs = Logs +module Checks = Checks (** {2 Front-end} From 9316b182e987740335fbf157c0e63dc75f4af7df Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 9 Dec 2025 17:18:24 +0200 Subject: [PATCH 32/36] Fix warn_past_end not outputting checks in ArrayDomain --- src/cdomain/value/cdomains/arrayDomain.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml index dcc7fa4082..d938edf9b9 100644 --- a/src/cdomain/value/cdomains/arrayDomain.ml +++ b/src/cdomain/value/cdomains/arrayDomain.ml @@ -997,9 +997,13 @@ struct type substr = IsNotSubstr | IsSubstrAtIndex0 | IsMaybeSubstr module ArrayOobMessage = M.Category.Behavior.Undefined.ArrayOutOfBounds - let warn_past_end ?loc ?tags fmt = - Checks.error Checks.Category.InvalidMemoryAccess fmt |> ignore; - M.error ~category:ArrayOobMessage.past_end ?loc ?tags fmt + let warn_past_end ?loc ?tags fmt = + (* Must do it this way to use same format string for multiple functions and also pass all arguments after. + Just calling Checks.error and M.error with fmt as last argument will silently not call Checks.error! *) + Pretty.gprintf (fun doc -> + Checks.error Checks.Category.InvalidMemoryAccess "%a" Pretty.insert doc; + M.error ~category:ArrayOobMessage.past_end ?loc ?tags "%a" Pretty.insert doc + ) fmt let min_nat_of_idx i = Z.max Z.zero (BatOption.default Z.zero (Idx.minimal i)) From 475acce96d1cfd6cb6fb4737c892aeea58925111 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 12 Dec 2025 12:38:46 +0200 Subject: [PATCH 33/36] Add checks.json to .gitignore --- .gitignore | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.gitignore b/.gitignore index da004ca979..58b64efd19 100644 --- a/.gitignore +++ b/.gitignore @@ -91,6 +91,9 @@ gobview_out/* witness.yml witness.certificate.yml +# checks +checks.json + # transformations transformed.c From c3ba196dac7a57a20c9d3af12c34cb153d418953 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 12 Dec 2025 12:40:30 +0200 Subject: [PATCH 34/36] Remove questionable current_node condition for safe checks --- src/common/util/checks.ml | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index 5ca06425b1..a6cdd46065 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -167,15 +167,6 @@ let error category = check Kind.Error category let warn category = check Kind.Warning category -let safe category = - match !Node0.current_node with - | Some (Statement _) -> - check Kind.Safe category "" - | _ -> () - -let safe_msg category = - match !Node0.current_node with - | Some (Statement _) -> - check Kind.Safe category - | _ -> - GobPretty.igprintf () +let safe category = check Kind.Safe category "" + +let safe_msg category = check Kind.Safe category From 6d5ec33323cd8e0233d0e97ea2b2638601c3e92e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 12 Dec 2025 12:49:18 +0200 Subject: [PATCH 35/36] Remove questionable no_safe condition for int overflow safe checks --- src/cdomain/value/cdomains/int/intDomTuple.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml index 317ba460d8..ef11f30598 100644 --- a/src/cdomain/value/cdomains/int/intDomTuple.ml +++ b/src/cdomain/value/cdomains/int/intDomTuple.ml @@ -64,7 +64,7 @@ module IntDomTupleImpl = struct | Some(_, {underflow; overflow}) -> not (underflow || overflow) | _ -> false - let check_ov ?(suppress_ovwarn = false) ?(no_safe = false) ~cast ik intv intv_set bf = + let check_ov ?(suppress_ovwarn = false) ~cast ik intv intv_set bf = let no_ov = (no_overflow ik intv) || (no_overflow ik intv_set) || (no_overflow ik bf) in if not suppress_ovwarn && (BatOption.is_some intv || BatOption.is_some intv_set || BatOption.is_some bf) then ( if not no_ov then ( @@ -74,7 +74,7 @@ module IntDomTupleImpl = struct let underflow = underflow_intv && underflow_intv_set && underflow_bf in let overflow = overflow_intv && overflow_intv_set && overflow_bf in set_overflow_flag ~cast ~underflow ~overflow ik; - ) else if not !AnalysisState.executing_speculative_computations && not no_safe then ( + ) else if not !AnalysisState.executing_speculative_computations then ( Checks.safe_msg Checks.Category.IntegerOverflow "Cast: %B" cast ) ); @@ -86,7 +86,7 @@ module IntDomTupleImpl = struct let intv = f p2 @@ r.fi2_ovc (module I2) in let intv_set = f p5 @@ r.fi2_ovc (module I5) in let bf = f p6 @@ r.fi2_ovc (module I6) in - ignore (check_ov ~suppress_ovwarn ~no_safe:true ~cast:false ik intv intv_set bf); + ignore (check_ov ~suppress_ovwarn ~cast:false ik intv intv_set bf); map @@ f p1 @@ r.fi2_ovc (module I1), map @@ f p2 @@ r.fi2_ovc (module I2), map @@ f p3 @@ r.fi2_ovc (module I3), map @@ f p4 @@ r.fi2_ovc (module I4), map @@ f p5 @@ r.fi2_ovc (module I5) , map @@ f p6 @@ r.fi2_ovc (module I6) let create2_ovc ?(suppress_ovwarn = false) ik r x = (* use where values are introduced *) From 3266e4d0153386f8dd12f3ef0cfc5719f47c553b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 12 Dec 2025 12:52:17 +0200 Subject: [PATCH 36/36] Simplify Checks code --- src/common/util/checks.ml | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/common/util/checks.ml b/src/common/util/checks.ml index a6cdd46065..ec112c5eca 100644 --- a/src/common/util/checks.ml +++ b/src/common/util/checks.ml @@ -40,7 +40,7 @@ module Category = struct | DoubleFree | NegativeArraySize | StubCondition - [@@deriving hash, eq, show] + [@@deriving hash, eq] let to_yojson x = `String (match x with | AssertionFailure -> "Assertion failure" @@ -102,12 +102,7 @@ module Check = struct (Format.pp_print_option CilType.Location.pp) check.range end -module CheckMap = Hashtbl.Make (struct - type t = Check.t - let equal = Check.equal - let hash = Check.hash - end) - +module CheckMap = Hashtbl.Make (Check) module CategoryLocationMap = Hashtbl.Make (struct type t = Category.t * CilType.Location.t [@@deriving hash, eq]