diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index 64c61a8d93..c67eee6cac 100644 --- a/src/analyses/accessAnalysis.ml +++ b/src/analyses/accessAnalysis.ml @@ -29,7 +29,7 @@ struct let init _ = collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed"; let activated = get_string_list "ana.activated" in - emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated (* TODO: some of these don't have access as dependency *) + emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated || List.mem (MemOutOfBounds.Spec.name ()) activated (* TODO: some of these don't have access as dependency *) let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) = if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach; diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 4546fda32e..8dd6fb5aa2 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -28,6 +28,13 @@ struct (* HELPER FUNCTIONS *) + let report_oob fmt = + set_mem_safety_flag InvalidDeref; + Pretty.gprintf (fun doc -> + M.warn ~category:(Behavior (Undefined MemoryOutOfBoundsAccess)) ~tags:[CWE 823] "%a" Pretty.insert doc; + Checks.warn Checks.Category.InvalidMemoryAccess "%a" Pretty.insert doc; + ) fmt + let intdom_of_int x = ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) @@ -52,39 +59,9 @@ struct in offs_lt_zero offs, ptr_size_lt_offs - let rec exp_contains_a_ptr (exp:exp) = - match exp with - | Const _ - | SizeOf _ - | SizeOfStr _ - | AlignOf _ - | AddrOfLabel _ -> false - | Real e - | Imag e - | SizeOfE e - | AlignOfE e - | UnOp (_, e, _) - | CastE (_, _, e) -> exp_contains_a_ptr e - | BinOp (_, e1, e2, _) -> - exp_contains_a_ptr e1 || exp_contains_a_ptr e2 - | Question (e1, e2, e3, _) -> - exp_contains_a_ptr e1 || exp_contains_a_ptr e2 || exp_contains_a_ptr e3 - | Lval lval - | AddrOf lval - | StartOf lval -> lval_contains_a_ptr lval - - and lval_contains_a_ptr (lval:lval) = - let (host, offset) = lval in - let host_contains_a_ptr = function - | Var v -> isPointerType v.vtype - | Mem e -> exp_contains_a_ptr e - in - let rec offset_contains_a_ptr = function - | NoOffset -> false - | Index (e, o) -> exp_contains_a_ptr e || offset_contains_a_ptr o - | Field (f, o) -> isPointerType f.ftype || offset_contains_a_ptr o - in - host_contains_a_ptr host || offset_contains_a_ptr offset + let add_offsets x y = + try ID.add x y + with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () let points_to_alloc_only man ptr = match man.ask (Queries.MayPointTo ptr) with @@ -107,9 +84,7 @@ struct begin match addr with | 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; - Checks.warn Checks.Category.InvalidMemoryAccess "Var %a is potentially accessed out-of-scope. Invalid memory access may occur" CilType.Varinfo.pretty v + report_oob "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, _, _) -> @@ -140,48 +115,32 @@ struct | x::xs -> List.fold_left VDQ.ID.join x xs end | _ -> - (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) + report_oob "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 = match Cil.unrollType ptr_typ with | TPtr (t, _) -> Some t | _ -> None - let eval_ptr_offset_in_binop man exp ptr_contents_typ = - let eval_offset = man.ask (Queries.EvalInt exp) in - let ptr_contents_typ_size_in_bytes = size_of_type_in_bytes ptr_contents_typ in - match eval_offset with - | `Lifted eo -> - let casted_eo = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) eo in (* TODO: proper castkind *) - begin - try `Lifted (ID.mul casted_eo ptr_contents_typ_size_in_bytes) - with IntDomain.ArithmeticOnIntegerBot _ -> `Bot - end - | `Top -> `Top - | `Bot -> `Bot + let eight = Z.of_int 8 + (* TODO: investigate why using PreValueDomain.Offs.to_index instead is too imprecise (to do with the Index case) *) let rec offs_to_idx typ offs = match offs with | `NoOffset -> intdom_of_int 0 | `Field (field, o) -> - let bytes_offset = Cilfacade.fieldBytesOffsetOnly field in - let bytes_offset = intdom_of_int bytes_offset in + let bits_offset = Cilfacade.fieldBitsOffsetOnly field in + let bits_offset = Z.of_int bits_offset in + (* Interval of floor and ceil division in case bitfield offset. *) + let bytes_offset = ID.of_interval (Cilfacade.ptrdiff_ikind ()) Z.(fdiv bits_offset eight, cdiv bits_offset eight) in let remaining_offset = offs_to_idx field.ftype o in - begin - try ID.add bytes_offset remaining_offset - with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - end + add_offsets bytes_offset remaining_offset | `Index (x, o) -> - begin try - let typ_size_in_bytes = size_of_type_in_bytes typ in - let bytes_offset = ID.mul typ_size_in_bytes x in - let remaining_offset = offs_to_idx typ o in - ID.add bytes_offset remaining_offset - with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - end + let typ_size_in_bytes = size_of_type_in_bytes typ in + let bytes_offset = ID.mul typ_size_in_bytes x in + let remaining_offset = offs_to_idx typ o in + add_offsets bytes_offset remaining_offset let cil_offs_to_idx man typ offs = (* TODO: Some duplication with convert_offset in base.ml, unclear how to immediately get more reuse *) @@ -200,291 +159,133 @@ struct in PreValueDomain.Offs.to_index (convert_offset offs) - let check_unknown_addr_deref man ptr = let may_contain_unknown_addr = - match man.ask (Queries.EvalValue ptr) with - | a when not (Queries.VD.is_top a) -> - begin match a with - | Address a -> ValueDomain.AD.may_be_unknown a - | _ -> false - end - (* Intuition: if ptr evaluates to top, it could potentially evaluate to the unknown address *) - | _ -> true + ValueDomain.AD.may_be_unknown (man.ask (Queries.MayPointTo ptr)) 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; - Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a contains an unknown address. Invalid dereference may occur" d_exp ptr + report_oob "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 - | a when not (Queries.VD.is_top a) -> - begin match a with - | Address a -> ValueDomain.AD.for_all (fun addr -> match addr with | StrPtr _ -> true | _ -> false) a - | _ -> false - end - (* Intuition: if ptr evaluates to top, it could all sorts of things and not only string addresses *) - | _ -> false - - let rec get_addr_offs man ptr = - match man.ask (Queries.MayPointTo ptr) with + let get_addr_offs_from_ad man ptr a = + match a with | a when not (VDQ.AD.is_top a) -> - let ptr_deref_type = get_ptr_deref_type @@ typeOf ptr in - begin match ptr_deref_type with + begin match get_ptr_deref_type @@ typeOf ptr with | Some t -> - 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; + if VDQ.AD.is_empty a then + ID.top_of @@ Cilfacade.ptrdiff_ikind () + else + (* Get the address offsets of all points-to set elements *) + let addr_offsets = + VDQ.AD.filter (function Addr _ -> true | _ -> false) a + |> VDQ.AD.to_mval + |> List.map (fun (_, o) -> offs_to_idx t o) + in + if List.exists ID.is_bot addr_offsets then + ID.bot_of @@ Cilfacade.ptrdiff_ikind () + else if List.exists (ID.is_top_of (Cilfacade.ptrdiff_ikind ())) addr_offsets then ID.top_of @@ Cilfacade.ptrdiff_ikind () - | false -> - if VDQ.AD.exists (function - | Addr (_, o) -> ID.is_bot @@ offs_to_idx t o - | _ -> 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; - 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; - 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 = - VDQ.AD.filter (function Addr (v, o) -> true | _ -> false) a - |> VDQ.AD.to_mval - |> List.map (fun (_, o) -> offs_to_idx t o) - in + else begin match addr_offsets with | [] -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () | [x] -> x - | x::xs -> List.fold_left ID.join x xs + | x :: xs -> List.fold_left ID.join x xs end - end | None -> M.error "Expression %a doesn't have pointer type" d_exp ptr; ID.top_of @@ Cilfacade.ptrdiff_ikind () end | _ -> - 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 = - (* If the lval does not contain a pointer or if it does contain a pointer, but only points to string addresses, then no need to WARN *) - if (not @@ lval_contains_a_ptr lval) || ptr_only_has_str_addr man (Lval lval) then () - else - (* If the lval doesn't indicate an explicit dereference, we still need to check for an implicit dereference *) - (* An implicit dereference is, e.g., printf("%p", ptr), where ptr is a pointer *) - match lval, is_implicitly_derefed with - | (Var _, _), false -> () - | (Var v, _), true -> check_no_binop_deref man (Lval lval) - | (Mem e, o), _ -> - let ptr_deref_type = get_ptr_deref_type @@ typeOf e in - let offs_intdom = begin match ptr_deref_type with - | Some t -> cil_offs_to_idx man t o + let get_addr_offs man ptr = + get_addr_offs_from_ad man ptr (man.ask (Queries.MayPointTo ptr)) + + let report_unknown_object_size access_desc d_exp ptr_exp size_desc = + report_oob "Size of object %s %a is %s. Memory out-of-bounds access might occur" access_desc d_exp ptr_exp size_desc + + let check_offset_against_object_size access_desc bounds_check man ptr_exp object_size offset = + let ptrdiff_ikind = Cilfacade.ptrdiff_ikind () in + let casted_object_size = ID.cast_to ~kind:Internal ptrdiff_ikind object_size in (* TODO: proper castkind *) + let casted_offset = ID.cast_to ~kind:Internal ptrdiff_ikind offset in (* TODO: proper castkind *) + begin match bounds_check casted_object_size casted_offset with + | Some true, _ + | _, Some true -> + report_oob "Size of object %s %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" + access_desc d_exp ptr_exp ID.pretty casted_object_size ID.pretty casted_offset + | Some false, Some false -> + Checks.safe Checks.Category.InvalidMemoryAccess + | _ -> + report_oob "Could not compare size of object %s %a (%a) (in bytes) with offset (%a) (in bytes). Memory out-of-bounds access may occur" + access_desc d_exp ptr_exp ID.pretty casted_object_size ID.pretty casted_offset + end + + let check_ptr_deref_access man ptr_exp offs = + check_unknown_addr_deref man ptr_exp; + begin match get_size_of_ptr_target man ptr_exp with + | `Top -> + report_unknown_object_size "accessed through" d_exp ptr_exp "top" + | `Bot -> + report_unknown_object_size "accessed through" d_exp ptr_exp "bot" + | `Lifted es -> + let stored_addr_offs = get_addr_offs man ptr_exp in + let lval_offs = + match get_ptr_deref_type @@ typeOf ptr_exp with + | Some t -> cil_offs_to_idx man t offs | None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - end in - let e_size = get_size_of_ptr_target man e in - 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); - 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); - 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 ~kind:Internal (Cilfacade.ptrdiff_ikind ()) es in (* TODO: proper castkind *) - let casted_offs = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) offs_intdom in (* TODO: proper castkind *) - let behavior = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in - begin match check_deref_offset_bounds casted_es casted_offs with - | Some true, _ - | _, 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); - 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, Some false -> - Checks.safe Checks.Category.InvalidMemoryAccess - | _ -> - (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); - 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 - | Lval (Var v, _) as lval_exp -> check_no_binop_deref man lval_exp - | BinOp (binop, e1, e2, t) when binop = PlusPI || binop = MinusPI || binop = IndexPI -> - check_binop_exp man binop e1 e2 t; - check_exp_for_oob_access man ~is_implicitly_derefed e1; - check_exp_for_oob_access man ~is_implicitly_derefed e2 - | _ -> check_exp_for_oob_access man ~is_implicitly_derefed e - end - - and check_no_binop_deref man lval_exp = - check_unknown_addr_deref man lval_exp; - let behavior = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in - let ptr_size = get_size_of_ptr_target man lval_exp in - let addr_offs = get_addr_offs man lval_exp in - let ptr_type = typeOf lval_exp in - let ptr_contents_type = get_ptr_deref_type ptr_type in - match ptr_contents_type with - | Some t -> + in + let offs_intdom = add_offsets stored_addr_offs lval_offs in + check_offset_against_object_size "accessed through" check_deref_offset_bounds man ptr_exp es offs_intdom + end + + let check_ptr_value_access man ptr_exp addr_offs = + match get_ptr_deref_type @@ typeOf ptr_exp with + | Some _ -> + check_unknown_addr_deref man ptr_exp; + let ptr_size = get_size_of_ptr_target man ptr_exp in 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; - 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 + report_unknown_object_size "pointed to by" d_exp ptr_exp "top" | `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; - 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 + report_unknown_object_size "pointed to by" d_exp ptr_exp "bot" | `Lifted ps, ao -> - let casted_ps = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *) - let casted_ao = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ao in (* TODO: proper castkind *) - begin match check_ptr_offset_bounds casted_ps casted_ao with - | Some true, _ - | _, 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; - 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, Some false -> - Checks.safe Checks.Category.InvalidMemoryAccess - | _ -> - 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; - 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 + check_offset_against_object_size "pointed to by" check_ptr_offset_bounds man ptr_exp ps ao end - | _ -> M.error "Expression %a is not a pointer" d_exp lval_exp + | _ -> M.error "Expression %a is not a pointer" d_exp ptr_exp - and check_exp_for_oob_access man ?(is_implicitly_derefed = false) exp = + let check_access_for_oob man exp ad = + let ptr_only_has_str_addr ptr = + ValueDomain.AD.for_all (function StrPtr _ -> true | _ -> false) (man.ask (Queries.MayPointTo ptr)) + in + let exp = Cil.stripCasts exp in match exp with - | Const _ - | SizeOf _ - | SizeOfStr _ - | AlignOf _ - | AddrOfLabel _ -> () - | Real e - | Imag e - | SizeOfE e - | AlignOfE e - | UnOp (_, e, _) - | CastE (_, _, e) -> check_exp_for_oob_access man ~is_implicitly_derefed e - | BinOp (bop, e1, e2, t) -> - check_exp_for_oob_access man ~is_implicitly_derefed e1; - check_exp_for_oob_access man ~is_implicitly_derefed e2 - | Question (e1, e2, e3, _) -> - check_exp_for_oob_access man ~is_implicitly_derefed e1; - check_exp_for_oob_access man ~is_implicitly_derefed e2; - check_exp_for_oob_access man ~is_implicitly_derefed e3 - | Lval lval - | StartOf lval - | AddrOf lval -> check_lval_for_oob_access man ~is_implicitly_derefed lval - - and check_binop_exp man binop e1 e2 t = - check_unknown_addr_deref man e1; - let binopexp = BinOp (binop, e1, e2, t) in - let behavior = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in - match binop with - | PlusPI - | IndexPI - | MinusPI -> - let ptr_size = get_size_of_ptr_target man e1 in - let addr_offs = get_addr_offs man e1 in - let ptr_type = typeOf e1 in - let ptr_contents_type = get_ptr_deref_type ptr_type in - begin match ptr_contents_type with - | Some t -> - let offset_size = eval_ptr_offset_in_binop man e2 t in - (* Make sure to add the address offset to the binop offset *) - let offset_size_with_addr_size = match offset_size with - | `Lifted os -> - let casted_os = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) os in (* TODO: proper castkind *) - let casted_ao = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) addr_offs in (* TODO: proper castkind *) - begin - try `Lifted (ID.add casted_os casted_ao) - with IntDomain.ArithmeticOnIntegerBot _ -> `Bot - end - | `Top -> `Top - | `Bot -> `Bot - in - 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; - 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; - 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; - 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; - 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 ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *) - let casted_o = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) o in (* TODO: proper castkind *) - begin match check_ptr_offset_bounds casted_ps casted_o with - | Some true, _ - | _, 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; - 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, Some false -> - Checks.safe Checks.Category.InvalidMemoryAccess - | _ -> - 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; - 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 - end - | _ -> () + (* Actual dereference/access through a pointer. *) + | AddrOf (Mem e, o) when not (ptr_only_has_str_addr e) -> + check_ptr_deref_access man e o + (* Taking the address of something is not an access itself. *) + | AddrOf _ -> + () + (* Pointer arithmetic / pointer value access. *) + | _ when isPointerType (typeOf exp) && not (ptr_only_has_str_addr exp) -> + check_ptr_value_access man exp (get_addr_offs_from_ad man exp ad) + | _ -> + () (* For memset() and memcpy() *) let check_count man fun_name ptr n = - let (behavior:MessageCategory.behavior) = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in let ptr_size = get_size_of_ptr_target man ptr in let eval_n = man.ask (Queries.EvalInt n) in let addr_offs = get_addr_offs man ptr in 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; - 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 + report_oob "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; - Checks.warn Checks.Category.InvalidMemoryAccess "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name + report_oob "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; - 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 + report_oob "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; - Checks.warn Checks.Category.InvalidMemoryAccess "Count parameter, passed to function %s is bottom" fun_name + report_oob "Count parameter, passed to function %s is bottom" fun_name | `Lifted ds, `Lifted en -> let casted_ds = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ds in (* TODO: proper castkind *) let casted_en = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) en in (* TODO: proper castkind *) @@ -492,44 +293,32 @@ struct let dest_size_lt_count = ID.lt casted_ds (ID.add casted_en casted_ao) in begin match 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; - 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 + report_oob "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; - 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 + report_oob "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 - - - (* TRANSFER FUNCTIONS *) - - let assign man (lval:lval) (rval:exp) : D.t = - check_lval_for_oob_access man lval; - check_exp_for_oob_access man rval; - man.local - - let branch man (exp:exp) (tv:bool) : D.t = - check_exp_for_oob_access man exp; - man.local - - let return man (exp:exp option) (f:fundec) : D.t = - Option.iter (fun x -> check_exp_for_oob_access man x) exp; - man.local - let special man (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = let desc = LibraryFunctions.find f in - let is_arg_implicitly_derefed arg = + let is_arg_accessed_through_pointer arg = let read_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = false } arglist in let read_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = true } arglist in let write_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } arglist in let write_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } arglist in List.mem arg read_shallow_args || List.mem arg read_deep_args || List.mem arg write_shallow_args || List.mem arg write_deep_args in - Option.iter (fun x -> check_lval_for_oob_access man x) lval; - List.iter (fun arg -> check_exp_for_oob_access man ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) arg) arglist; + (* Access events don't preserve whether AddrOf/StartOf arguments were dereferenced by a special access. *) + List.iter (fun arg -> + if is_arg_accessed_through_pointer arg then + match Cil.stripCasts arg with + | AddrOf lval + | StartOf lval -> + let ptr_exp = Lval lval in + check_ptr_value_access man ptr_exp (get_addr_offs man ptr_exp) + | _ -> + () + ) arglist; (* Check calls to memset and memcpy for out-of-bounds-accesses *) match desc.special arglist with | Memset { dest; ch; count; } -> check_count man f.vname dest count; @@ -538,17 +327,18 @@ struct check_count man f.vname dest count;) | _ -> man.local - let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = - List.iter (fun arg -> check_exp_for_oob_access man arg) args; - [man.local, man.local] - - let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t = - Option.iter (fun x -> check_lval_for_oob_access man x) lval; - man.local - let startstate v = () let exitstate v = () + + let event man e oman = + match e with + | Events.Access {exp; ad; _} -> + (* must use original (pre-assign, etc) man queries *) + check_access_for_oob oman exp ad; + man.local + | _ -> + man.local end let _ = - MCP.register_analysis (module Spec : MCPSpec) + MCP.register_analysis ~dep:["access"] (module Spec : MCPSpec) diff --git a/tests/regression/74-invalid_deref/01-oob-heap-simple.t b/tests/regression/74-invalid_deref/01-oob-heap-simple.t index ac3ec99fa8..0458eaa476 100644 --- a/tests/regression/74-invalid_deref/01-oob-heap-simple.t +++ b/tests/regression/74-invalid_deref/01-oob-heap-simple.t @@ -1,7 +1,7 @@ $ goblint --set ana.activated[+] memOutOfBounds --enable ana.int.interval 01-oob-heap-simple.c 2>&1 | tee default-output.txt [Warning] The memOutOfBounds analysis enables cil.addNestedScopeAttr. - [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer in expression ptr + 10 is 5 (in bytes). It is offset by 10 (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) - [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (5) with offset (⊤). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) + [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of object accessed through ptr + 10 is 5 (in bytes). It is offset by 10 (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) + [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of object accessed through ptr + r (5) (in bytes) with offset (⊤) (in bytes). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 8 dead: 0 @@ -11,9 +11,9 @@ $ diff default-output.txt full-output.txt 2,3c2,3 - < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer in expression ptr + 10 is 5 (in bytes). It is offset by 10 (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) - < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (5) with offset (⊤). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) + < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of object accessed through ptr + 10 is 5 (in bytes). It is offset by 10 (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) + < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of object accessed through ptr + r (5) (in bytes) with offset (⊤) (in bytes). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) --- - > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer in expression ptr + 10 is (5,[5,5]) (in bytes). It is offset by (10,[10,10]) (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) - > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size ((5,[5,5])) with offset ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) + > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of object accessed through ptr + 10 is (5,[5,5]) (in bytes). It is offset by (10,[10,10]) (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) + > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of object accessed through ptr + r ((5,[5,5])) (in bytes) with offset ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])) (in bytes). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) [1] diff --git a/tests/regression/74-invalid_deref/36-one-past-pointer.c b/tests/regression/74-invalid_deref/36-one-past-pointer.c index b4ceb506d7..41cc4b54c9 100644 --- a/tests/regression/74-invalid_deref/36-one-past-pointer.c +++ b/tests/regression/74-invalid_deref/36-one-past-pointer.c @@ -7,6 +7,7 @@ int main(void) { char *end; end = buf + 4; //NOWARN printf("%p", (void *) end); //NOWARN + printf("%c", *end); //WARN free(buf); return 0; }