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 diff --git a/src/analyses/assert.ml b/src/analyses/assert.ml index 2dd2b6cd89..1d500f7f31 100644 --- a/src/analyses/assert.ml +++ b/src/analyses/assert.ml @@ -23,15 +23,19 @@ struct match Queries.eval_bool (Analyses.ask_of_man man) e with | `Lifted false -> assert_msg Error "Assertion \"%a\" will fail." CilType.Exp.pretty e; + Checks.error Checks.Category.AssertionFailure "Assertion \"%a\" will fail." CilType.Exp.pretty e; if refine then raise Analyses.Deadcode else man.local | `Lifted true -> assert_msg Success "Assertion \"%a\" will succeed" CilType.Exp.pretty e; + 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; + Checks.error Checks.Category.AssertionFailure "Assertion \"%a\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)" CilType.Exp.pretty e; man.local | `Top -> assert_msg Warning "Assertion \"%a\" is unknown." CilType.Exp.pretty e; + Checks.warn Checks.Category.AssertionFailure "Assertion \"%a\" is unknown." CilType.Exp.pretty e; 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 ab0d61a874..3123543bd0 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -202,19 +202,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 @@ -1092,11 +1098,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 @@ -1104,7 +1114,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 @@ -1176,10 +1187,11 @@ 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; + ) else ( + M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval; + ) ); fp @@ -2223,7 +2235,9 @@ 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"; + )); 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 @@ -2259,17 +2273,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 @@ -2327,6 +2347,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 08ad447b5a..4d9d11df2c 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -293,9 +293,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/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 72daac3a51..b839219a81 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, _, _) -> @@ -123,6 +124,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 +197,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 +221,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 +229,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 +260,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 +282,12 @@ struct 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 +303,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; begin match e with @@ -320,10 +335,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 +348,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 +415,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 +436,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 +460,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 +482,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 78fab33d89..cc94866c7e 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -154,9 +154,18 @@ struct let cwe_number = if is_free then 415 else 416 in let warn_for_heap_var v = if HeapVars.mem v freed_heap_vars then begin - if is_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) points to a maybe freed memory region" v.vname - end + if is_free then ( + set_mem_safety_flag InvalidFree; + Checks.warn Checks.Category.DoubleFree "lval (%s) points to a maybe freed memory region" v.vname) + else ( + set_mem_safety_flag InvalidDeref; + Checks.warn Checks.Category.InvalidMemoryAccess "lval (%s) points to a maybe freed memory region" v.vname + ); + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) points to a maybe freed memory region" v.vname; + end else if is_free then + Checks.safe Checks.Category.DoubleFree + else + Checks.safe Checks.Category.InvalidMemoryAccess in if not (Queries.AD.is_top ad) then begin let pointed_to_heap_vars = diff --git a/src/cdomain/value/cdomains/addressDomain.ml b/src/cdomain/value/cdomains/addressDomain.ml index f84cd58acb..e86a928040 100644 --- a/src/cdomain/value/cdomains/addressDomain.ml +++ b/src/cdomain/value/cdomains/addressDomain.ml @@ -320,9 +320,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 46d602d774..d938edf9b9 100644 --- a/src/cdomain/value/cdomains/arrayDomain.ml +++ b/src/cdomain/value/cdomains/arrayDomain.ml @@ -807,22 +807,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 = @@ -992,7 +997,13 @@ 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 = + (* 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)) @@ -1127,25 +1138,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 @@ -1196,6 +1217,7 @@ struct else if Nulls.is_empty Possibly nulls then (warn_past_end "May access array past end: potential buffer overflow"; x) else + (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 @@ -1215,7 +1237,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 @@ -1226,13 +1248,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 @@ -1241,13 +1265,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 @@ -1260,14 +1290,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 + (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 + (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 *) @@ -1285,7 +1317,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) @@ -1300,8 +1332,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 @@ -1313,7 +1346,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 *) @@ -1331,7 +1366,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' @@ -1345,7 +1382,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 @@ -1357,7 +1396,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 @@ -1375,21 +1416,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 *) @@ -1412,7 +1463,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") ); @@ -1603,6 +1654,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"; @@ -1620,7 +1673,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/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml index 1887571ce1..ef11f30598 100644 --- a/src/cdomain/value/cdomains/int/intDomTuple.ml +++ b/src/cdomain/value/cdomains/int/intDomTuple.ml @@ -66,13 +66,17 @@ 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 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_msg Checks.Category.IntegerOverflow "Cast: %B" cast + ) ); no_ov diff --git a/src/cdomain/value/cdomains/intDomain0.ml b/src/cdomain/value/cdomains/intDomain0.ml index 39371a4bf2..f2b88be75e 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 new file mode 100644 index 0000000000..ec112c5eca --- /dev/null +++ b/src/common/util/checks.ml @@ -0,0 +1,167 @@ +(** + 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 + | Warning + | Safe + [@@deriving hash, eq, show] + + let is_safe = function + | Safe -> true + | _ -> false + + let to_yojson x = `String (match x with + | Error -> "error" + | Warning -> "warning" + | Safe -> "safe") + + let of_yojson = function + | `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) +end + +module Category = struct + type t = + | AssertionFailure + | InvalidMemoryAccess + | DivisionByZero + | IntegerOverflow + | InvalidPointerComparison + | InvalidPointerSubtraction + | DoubleFree + | NegativeArraySize + | StubCondition + [@@deriving hash, eq] + + let to_yojson x = `String (match x with + | AssertionFailure -> "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" + | StubCondition -> "Stub condition") + + let of_yojson = function + | `String "Assertion failure" -> Ok AssertionFailure + | `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 + | `String "Stub condition" -> Ok StubCondition + | category -> Error ("Checks.Category.of_yojson: Invalid category: " ^ Yojson.Safe.to_string category) +end + +module Check = struct + type t = { + kind: Kind.t; + title: Category.t; + range: CilType.Location.t option; + messages: string; + } [@@deriving make, hash, eq] + + 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 - 1)) + ]); + ("end", `Assoc [ + ("file", `String loc.file); + ("line", `Int loc.endLine); + ("column", `Int (loc.endColumn - 1)) + ]) + ] + | None -> `Null); + ("messages", `String check.messages) + ] + + 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 +end + +module CheckMap = Hashtbl.Make (Check) + +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 +(** 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 + | 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 category = check Kind.Safe category "" + +let safe_msg category = check Kind.Safe category diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 02e634d9e7..134ce7eb95 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": { diff --git a/src/framework/analysisResultOutput.ml b/src/framework/analysisResultOutput.ml index e7b9eb6bd6..29f2006f8e 100644 --- a/src/framework/analysisResultOutput.ml +++ b/src/framework/analysisResultOutput.ml @@ -92,6 +92,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.export ()); + ] in + Yojson.Safe.to_channel ~std:true out json | "none" -> () | s -> failwith @@ "Unsupported value for option `result`: "^s end 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} 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! *)