From 7bb5697b51950921c51e638aaebefe4b80ce3a4c Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Tue, 27 Jun 2023 16:23:52 +0200 Subject: [PATCH 01/35] Add first rough (semi-working) memory OOB analysis --- src/analyses/memOutOfBounds.ml | 194 +++++++++++++++++++++++++++++++++ 1 file changed, 194 insertions(+) create mode 100644 src/analyses/memOutOfBounds.ml diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml new file mode 100644 index 0000000000..db4066d442 --- /dev/null +++ b/src/analyses/memOutOfBounds.ml @@ -0,0 +1,194 @@ +open GoblintCil +open Analyses + +module Spec = +struct + include Analyses.IdentitySpec + + module D = Lattice.Unit(*ValueDomain.AddrSetDomain*) + module C = Lattice.Unit + + (* TODO: Do this later *) + let context _ _ = () + + let name () = "memOutOfBounds" + + (* HELPER FUNCTIONS *) + + let exp_points_to_heap ctx (exp:exp) = + match ctx.ask (Queries.MayPointTo exp) with + | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> + Queries.LS.elements a + |> List.map fst + |> List.exists (fun x -> ctx.ask (Queries.IsHeapVar x)) + | _ -> false + + let lval_points_to_heap ctx (lval:lval) = exp_points_to_heap ctx (mkAddrOf lval) + + 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 lval_is_of_ptr_type lval = + match typeOfLval lval with + | TPtr _ -> true + | _ -> false + in + let (host, offset) = lval in + let host_contains_a_ptr h = + match h with + | Var v -> isPointerType v.vtype + | Mem e -> exp_contains_a_ptr e + in + let rec offset_contains_a_ptr o = + match o with + | 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 + lval_is_of_ptr_type lval || host_contains_a_ptr host || offset_contains_a_ptr offset + + let calc_lval_type_size (lval:lval) = + begin try + let t = typeOfLval lval in + match sizeOf t with + | Const (CInt(i, _, _)) -> Some (cilint_to_int i) + | _ -> None + with _ -> None + end + + let get_ptr_size_for_lval ctx (lval:lval) = + match lval_points_to_heap ctx lval with + | true -> (* We're dealing with a ptr that points to the heap *) + begin match ctx.ask (Queries.BlobSize (mkAddrOf lval)) with + | a when not (Queries.ID.is_top a) -> + begin match Queries.ID.to_int a with + | Some i -> Some (IntOps.BigIntOps.to_int i) + | None -> None + end + | _ -> None + end + (* Assumption here is that if it's not a heap ptr, then it's a stack ptr and the ptr size would be the lval type's size *) + | false -> calc_lval_type_size lval + + let rec get_offset_size ctx offset = + match offset with + | NoOffset -> Some 0 + | Index (e, o) -> + begin match ctx.ask (Queries.EvalInt e) with + | a when not (Queries.ID.is_top a) -> + begin match Queries.ID.to_int a with + | Some i -> + begin match get_offset_size ctx o with + | Some os -> Some (IntOps.BigIntOps.to_int i + os) + | None -> None + end + | None -> None + end + | _ -> None + end + | Field (f, o) -> + let f_size = + begin match sizeOf f.ftype with + | Const (CInt (i, _, _)) -> Some (cilint_to_int i) + | _ -> None + end + in + begin match f_size, get_offset_size ctx o with + | Some fs, Some os -> Some (fs + os) + | _ -> None + end + + let check_lval_for_oob_access ctx (lval:lval) = + match lval_contains_a_ptr lval with + | false -> () + | true -> + let (_, offset) = lval in + begin match get_ptr_size_for_lval ctx lval, get_offset_size ctx offset with + | _, None -> M.warn "Offset unknown, potential out-of-bounds access for lval %a" CilType.Lval.pretty lval + | None, _ -> M.warn "Pointer size unknown, potential out-of-bounds access for lval %a" CilType.Lval.pretty lval + | Some pi, Some oi -> + if oi > pi then + M.warn "Must out-of-bounds memory access: Offset size (%d) is larger than pointer's memory size (%d) for lval %a" oi pi CilType.Lval.pretty lval + end + + let rec check_exp_for_oob_access ctx (exp:exp) = + 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 ctx e + | BinOp (_, e1, e2, _) -> + check_exp_for_oob_access ctx e1; + check_exp_for_oob_access ctx e2 + | Question (e1, e2, e3, _) -> + check_exp_for_oob_access ctx e1; + check_exp_for_oob_access ctx e2; + check_exp_for_oob_access ctx e3 + | Lval lval + | StartOf lval + | AddrOf lval -> check_lval_for_oob_access ctx lval + + + (* TRANSFER FUNCTIONS *) + + let assign ctx (lval:lval) (rval:exp) : D.t = + check_lval_for_oob_access ctx lval; + check_exp_for_oob_access ctx rval; + ctx.local + + let branch ctx (exp:exp) (tv:bool) : D.t = + check_exp_for_oob_access ctx exp; + ctx.local + + let return ctx (exp:exp option) (f:fundec) : D.t = + Option.iter (fun x -> check_exp_for_oob_access ctx x) exp; + ctx.local + + let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = + Option.iter (fun x -> check_lval_for_oob_access ctx x) lval; + List.iter (fun arg -> check_exp_for_oob_access ctx arg) arglist; + ctx.local + + let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = + [ctx.local, ctx.local] + + let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t = + ctx.local + + let combine_assign ctx (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 ctx x) lval; + List.iter (fun arg -> check_exp_for_oob_access ctx arg) args; + ctx.local + + let startstate v = (*D.empty*) () + let exitstate v = (*D.empty*) () +end + +let _ = + MCP.register_analysis (module Spec : MCPSpec) \ No newline at end of file From a5c693efd417720c2baccfd19782cc8592f1f262 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Tue, 27 Jun 2023 16:24:21 +0200 Subject: [PATCH 02/35] Add 2 simple regression tests for memory OOB --- tests/regression/73-mem-oob/01-oob-heap-simple.c | 14 ++++++++++++++ tests/regression/73-mem-oob/02-oob-stack-simple.c | 12 ++++++++++++ 2 files changed, 26 insertions(+) create mode 100644 tests/regression/73-mem-oob/01-oob-heap-simple.c create mode 100644 tests/regression/73-mem-oob/02-oob-stack-simple.c diff --git a/tests/regression/73-mem-oob/01-oob-heap-simple.c b/tests/regression/73-mem-oob/01-oob-heap-simple.c new file mode 100644 index 0000000000..91d9c7605a --- /dev/null +++ b/tests/regression/73-mem-oob/01-oob-heap-simple.c @@ -0,0 +1,14 @@ +// PARAM: --set ana.activated[+] memOutOfBounds +#include + +int main(int argc, char const *argv[]) { + char *ptr = malloc(5 * sizeof(char)); + + *ptr = 'a';//NOWARN + *(ptr + 1) = 'b';//NOWARN + *(ptr + 10) = 'c';//WARN + + free(ptr); + + return 0; +} diff --git a/tests/regression/73-mem-oob/02-oob-stack-simple.c b/tests/regression/73-mem-oob/02-oob-stack-simple.c new file mode 100644 index 0000000000..deedd52781 --- /dev/null +++ b/tests/regression/73-mem-oob/02-oob-stack-simple.c @@ -0,0 +1,12 @@ +// PARAM: --set ana.activated[+] memOutOfBounds +#include + +int main(int argc, char const *argv[]) { + int i = 42; + int *ptr = &i; + + *ptr = 5;//NOWARN + *(ptr + 10) = 55;//WARN + + return 0; +} From f3507455563fa0b9e23f25fe7dfae605d53c04ca Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 1 Jul 2023 18:33:43 +0200 Subject: [PATCH 03/35] Stick with Lattice.Unit --- src/analyses/memOutOfBounds.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index db4066d442..9648f35610 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -5,7 +5,7 @@ module Spec = struct include Analyses.IdentitySpec - module D = Lattice.Unit(*ValueDomain.AddrSetDomain*) + module D = Lattice.Unit module C = Lattice.Unit (* TODO: Do this later *) @@ -186,8 +186,8 @@ struct List.iter (fun arg -> check_exp_for_oob_access ctx arg) args; ctx.local - let startstate v = (*D.empty*) () - let exitstate v = (*D.empty*) () + let startstate v = () + let exitstate v = () end let _ = From 4d5e0dcabe77afa11102f07c50971b12f18b1037 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 8 Jul 2023 16:26:07 +0200 Subject: [PATCH 04/35] Rewrite the majority of the logic and checks performed in memOutOfBounds --- src/analyses/memOutOfBounds.ml | 208 +++++++++++++++++++++------------ 1 file changed, 136 insertions(+), 72 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 9648f35610..d96c59e105 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -15,15 +15,12 @@ struct (* HELPER FUNCTIONS *) - let exp_points_to_heap ctx (exp:exp) = - match ctx.ask (Queries.MayPointTo exp) with - | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> - Queries.LS.elements a - |> List.map fst - |> List.exists (fun x -> ctx.ask (Queries.IsHeapVar x)) - | _ -> false - let lval_points_to_heap ctx (lval:lval) = exp_points_to_heap ctx (mkAddrOf lval) + (* A safe way to call [cilint_to_int] without having to worry about exceptions *) + let cilint_to_int_wrapper i = + try + Some (cilint_to_int i) + with _ -> None let rec exp_contains_a_ptr (exp:exp) = match exp with @@ -47,90 +44,131 @@ struct | StartOf lval -> lval_contains_a_ptr lval and lval_contains_a_ptr (lval:lval) = - let lval_is_of_ptr_type lval = - match typeOfLval lval with - | TPtr _ -> true - | _ -> false - in let (host, offset) = lval in - let host_contains_a_ptr h = - match h with + 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 o = - match o with + 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 - lval_is_of_ptr_type lval || host_contains_a_ptr host || offset_contains_a_ptr offset + host_contains_a_ptr host || offset_contains_a_ptr offset - let calc_lval_type_size (lval:lval) = - begin try - let t = typeOfLval lval in - match sizeOf t with - | Const (CInt(i, _, _)) -> Some (cilint_to_int i) - | _ -> None - with _ -> None - end - - let get_ptr_size_for_lval ctx (lval:lval) = - match lval_points_to_heap ctx lval with - | true -> (* We're dealing with a ptr that points to the heap *) - begin match ctx.ask (Queries.BlobSize (mkAddrOf lval)) with - | a when not (Queries.ID.is_top a) -> - begin match Queries.ID.to_int a with - | Some i -> Some (IntOps.BigIntOps.to_int i) - | None -> None - end - | _ -> None + let lval_is_ptr_var (lval:lval) = + let (host, _) = lval in + match host with + | Var v -> isPointerType v.vtype + (* Intuition: If the lval has a Mem host, then it's not a direct ptr which is what we're looking for here *) + | Mem e -> false + + let exp_points_to_heap ctx (exp:exp) = + match ctx.ask (Queries.MayPointTo exp) with + | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> + Queries.LS.elements a + |> List.map fst + |> List.exists (fun x -> ctx.ask (Queries.IsHeapVar x)) + | _ -> false (* TODO: Is this sound? Maybe not quite. *) + + let get_size_for_heap_ptr ctx (exp:exp) = + (* TODO: + BlobSize always seems to respond with top when it's passed an Lval exp of a ptr var which in turn contains mem allocated via malloc. + Am I doing smth wrong here? + *) + match ctx.ask (Queries.BlobSize exp) with + | a when not (Queries.ID.is_top a) -> + begin match Queries.ID.to_int a with + | Some i -> Some (IntOps.BigIntOps.to_int i) + | None -> None end - (* Assumption here is that if it's not a heap ptr, then it's a stack ptr and the ptr size would be the lval type's size *) - | false -> calc_lval_type_size lval + | _ -> None + + (* TODO: Here we assume that the given exp is a Lval exp *) + let get_size_for_stack_ptr ctx (exp:exp) = + match exp with + | Lval lval -> + if lval_is_ptr_var lval then + let (host, _) = lval in + begin match host with + | Var v -> + begin match sizeOf v.vtype with + | Const (CInt (i, _, _)) -> cilint_to_int_wrapper i + | _ -> None + end + | _ -> None + end + else None + | _ -> None + + let get_ptr_size_for_exp ctx (exp:exp) = + match exp_points_to_heap ctx exp with + (* We're dealing with a ptr that points to the heap *) + | true -> get_size_for_heap_ptr ctx exp + (* Assumption here is that if it doesn't point to the heap, then it points to the stack *) + | false -> get_size_for_stack_ptr ctx exp - let rec get_offset_size ctx offset = - match offset with + (** + * If we get [None], then the offset's size/value is unknown + * In the case [NoOffset], [Some 0] indicates that this offset type simply has value 0 + *) + let rec get_offset_size = function | NoOffset -> Some 0 | Index (e, o) -> - begin match ctx.ask (Queries.EvalInt e) with - | a when not (Queries.ID.is_top a) -> - begin match Queries.ID.to_int a with - | Some i -> - begin match get_offset_size ctx o with - | Some os -> Some (IntOps.BigIntOps.to_int i + os) - | None -> None - end - | None -> None - end + let exp_val = begin match constFold true e with + | Const (CInt (i, _, _)) -> cilint_to_int_wrapper i | _ -> None end - | Field (f, o) -> - let f_size = - begin match sizeOf f.ftype with - | Const (CInt (i, _, _)) -> Some (cilint_to_int i) - | _ -> None - end in - begin match f_size, get_offset_size ctx o with - | Some fs, Some os -> Some (fs + os) - | _ -> None + begin match exp_val, get_offset_size o with + | Some ei, Some oi -> Some (ei + oi) + | _, _ -> None + end + | Field (f, o) -> + begin match get_offset_size o, sizeOf f.ftype with + | Some oi, Const (CInt (i, _, _)) -> + begin match cilint_to_int_wrapper i with + | Some i -> Some (oi + i) + | None -> None + end + | _, _ -> None end - let check_lval_for_oob_access ctx (lval:lval) = + let rec check_lval_for_oob_access ctx (lval:lval) = match lval_contains_a_ptr lval with - | false -> () + | false -> () (* Nothing to do here *) | true -> - let (_, offset) = lval in - begin match get_ptr_size_for_lval ctx lval, get_offset_size ctx offset with - | _, None -> M.warn "Offset unknown, potential out-of-bounds access for lval %a" CilType.Lval.pretty lval - | None, _ -> M.warn "Pointer size unknown, potential out-of-bounds access for lval %a" CilType.Lval.pretty lval - | Some pi, Some oi -> - if oi > pi then - M.warn "Must out-of-bounds memory access: Offset size (%d) is larger than pointer's memory size (%d) for lval %a" oi pi CilType.Lval.pretty lval - end + let (host, offset) = lval in + match host, get_offset_size offset with + | _, None -> M.warn "Offset size for lval %a not known. May have a memory out-of-bounds access" CilType.Lval.pretty lval + | Var v, Some oi -> + begin match sizeOf v.vtype with + | Const (CInt (i, _, _)) -> + begin match cilint_to_int_wrapper i with + | Some i -> + if i < oi then + M.warn "Offset bigger than var type's size for lval %a. A memory out-of-bounds access must occur" CilType.Lval.pretty lval + | _ -> M.warn "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval + end + | _ -> M.warn "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval + end + | Mem e, Some oi -> + check_exp_for_oob_access ctx e; + (* TODO: + * Not sure if we actually need these checks below. + * They never seem to apply + * I.e., for ptrs, it always seems to be the case that we have a binop which adds the offset to the ptr + instead of having the offset represented as an offset of the lval + * For this reason, the checks below are currently commented out + *) + (* begin match get_ptr_size_for_exp ctx e with + | Some ei -> + if ei < oi then + M.warn "Offset bigger than size of pointer memory, denoted by expression %a in lval %a" d_exp e CilType.Lval.pretty lval + | _ -> M.warn "Unknown size of pointer memory, denoted by exp %a for lval %a" d_exp e CilType.Lval.pretty lval + end *) - let rec check_exp_for_oob_access ctx (exp:exp) = + and check_exp_for_oob_access ctx (exp:exp) = match exp with | Const _ | SizeOf _ @@ -143,7 +181,8 @@ struct | AlignOfE e | UnOp (_, e, _) | CastE (_, e) -> check_exp_for_oob_access ctx e - | BinOp (_, e1, e2, _) -> + | BinOp (bop, e1, e2, _) -> + check_binop_exp ctx bop e1 e2; check_exp_for_oob_access ctx e1; check_exp_for_oob_access ctx e2 | Question (e1, e2, e3, _) -> @@ -154,10 +193,35 @@ struct | StartOf lval | AddrOf lval -> check_lval_for_oob_access ctx lval + and check_binop_exp ctx (binop:binop) (e1:exp) (e2:exp) = + match binop with + | PlusPI + | IndexPI + | MinusPI -> + let ptr_size = get_ptr_size_for_exp ctx e1 in + let offset_size = eval_ptr_offset_in_binop e2 in + begin match ptr_size, offset_size with + | Some pi, Some oi -> + if pi < oi then + M.warn "Pointer size in expression %a %a %a is smaller than offset for pointer arithmetic" d_exp e1 CilType.Binop.pretty binop d_exp e2 + | None, _ -> M.warn "Pointer (%a) size in expression %a %a %a not known" d_exp e1 d_exp e1 CilType.Binop.pretty binop d_exp e2 + | _, None -> M.warn "Operand value for pointer arithmetic in expression %a %a %a not known" d_exp e1 CilType.Binop.pretty binop d_exp e2 + end + | _ -> () + + and eval_ptr_offset_in_binop (exp:exp) = + match constFold true exp with + | Const (CInt (i, _, _)) -> cilint_to_int_wrapper i + | _ -> None (* TODO: Maybe try to also Eval the exp via Queries and not rely only on constFold *) + (* TRANSFER FUNCTIONS *) let assign ctx (lval:lval) (rval:exp) : D.t = + let (host,_) = lval in + match host with + | Mem e -> ignore (Pretty.printf "Lval host is Mem e and e is %a\n" d_plainexp e); + | _ -> (); check_lval_for_oob_access ctx lval; check_exp_for_oob_access ctx rval; ctx.local From 098501b62a5f87d764eaf33a9468d576bbcb1435 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 8 Jul 2023 16:28:18 +0200 Subject: [PATCH 05/35] Remove printf calls --- src/analyses/memOutOfBounds.ml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index d96c59e105..58da08c7bc 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -218,10 +218,6 @@ struct (* TRANSFER FUNCTIONS *) let assign ctx (lval:lval) (rval:exp) : D.t = - let (host,_) = lval in - match host with - | Mem e -> ignore (Pretty.printf "Lval host is Mem e and e is %a\n" d_plainexp e); - | _ -> (); check_lval_for_oob_access ctx lval; check_exp_for_oob_access ctx rval; ctx.local From 6496c61ea12a9c686f3b09c2609c2ea88e9b0c0d Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 8 Jul 2023 16:30:43 +0200 Subject: [PATCH 06/35] Improve warning messages a bit --- src/analyses/memOutOfBounds.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 58da08c7bc..d11d876f5b 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -140,7 +140,7 @@ struct | true -> let (host, offset) = lval in match host, get_offset_size offset with - | _, None -> M.warn "Offset size for lval %a not known. May have a memory out-of-bounds access" CilType.Lval.pretty lval + | _, None -> M.warn "Offset size for lval %a not known. A memory out-of-bounds access may occur" CilType.Lval.pretty lval | Var v, Some oi -> begin match sizeOf v.vtype with | Const (CInt (i, _, _)) -> @@ -203,9 +203,9 @@ struct begin match ptr_size, offset_size with | Some pi, Some oi -> if pi < oi then - M.warn "Pointer size in expression %a %a %a is smaller than offset for pointer arithmetic" d_exp e1 CilType.Binop.pretty binop d_exp e2 - | None, _ -> M.warn "Pointer (%a) size in expression %a %a %a not known" d_exp e1 d_exp e1 CilType.Binop.pretty binop d_exp e2 - | _, None -> M.warn "Operand value for pointer arithmetic in expression %a %a %a not known" d_exp e1 CilType.Binop.pretty binop d_exp e2 + M.warn "Pointer size in expression %a %a %a is smaller than offset for pointer arithmetic. Memory out-of-bounds access must occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 + | None, _ -> M.warn "Pointer (%a) size in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp e1 CilType.Binop.pretty binop d_exp e2 + | _, None -> M.warn "Operand value for pointer arithmetic in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 end | _ -> () From a796a0b4963cfae32177d33af27f1e49935ab234 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 8 Jul 2023 16:37:17 +0200 Subject: [PATCH 07/35] Add message category for memory OOB access --- src/analyses/memOutOfBounds.ml | 17 ++++++++++------- src/util/messageCategory.ml | 5 +++++ 2 files changed, 15 insertions(+), 7 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index d11d876f5b..7ea11e8ef1 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -1,5 +1,6 @@ open GoblintCil open Analyses +open MessageCategory module Spec = struct @@ -135,22 +136,23 @@ struct end let rec check_lval_for_oob_access ctx (lval:lval) = + let undefined_behavior = Undefined MemoryOutOfBoundsAccess in match lval_contains_a_ptr lval with | false -> () (* Nothing to do here *) | true -> let (host, offset) = lval in match host, get_offset_size offset with - | _, None -> M.warn "Offset size for lval %a not known. A memory out-of-bounds access may occur" CilType.Lval.pretty lval + | _, None -> M.warn ~category:(Behavior undefined_behavior) "Offset size for lval %a not known. A memory out-of-bounds access may occur" CilType.Lval.pretty lval | Var v, Some oi -> begin match sizeOf v.vtype with | Const (CInt (i, _, _)) -> begin match cilint_to_int_wrapper i with | Some i -> if i < oi then - M.warn "Offset bigger than var type's size for lval %a. A memory out-of-bounds access must occur" CilType.Lval.pretty lval - | _ -> M.warn "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval + M.warn ~category:(Behavior undefined_behavior) "Offset bigger than var type's size for lval %a. A memory out-of-bounds access must occur" CilType.Lval.pretty lval + | _ -> M.warn ~category:(Behavior undefined_behavior) "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval end - | _ -> M.warn "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval + | _ -> M.warn ~category:(Behavior undefined_behavior) "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval end | Mem e, Some oi -> check_exp_for_oob_access ctx e; @@ -194,6 +196,7 @@ struct | AddrOf lval -> check_lval_for_oob_access ctx lval and check_binop_exp ctx (binop:binop) (e1:exp) (e2:exp) = + let undefined_behavior = Undefined MemoryOutOfBoundsAccess in match binop with | PlusPI | IndexPI @@ -203,9 +206,9 @@ struct begin match ptr_size, offset_size with | Some pi, Some oi -> if pi < oi then - M.warn "Pointer size in expression %a %a %a is smaller than offset for pointer arithmetic. Memory out-of-bounds access must occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 - | None, _ -> M.warn "Pointer (%a) size in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp e1 CilType.Binop.pretty binop d_exp e2 - | _, None -> M.warn "Operand value for pointer arithmetic in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 + M.warn ~category:(Behavior undefined_behavior) "Pointer size in expression %a %a %a is smaller than offset for pointer arithmetic. Memory out-of-bounds access must occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 + | None, _ -> M.warn ~category:(Behavior undefined_behavior) "Pointer (%a) size in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp e1 CilType.Binop.pretty binop d_exp e2 + | _, None -> M.warn ~category:(Behavior undefined_behavior) "Operand value for pointer arithmetic in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 end | _ -> () diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml index ef8ee5d6a9..8190f79294 100644 --- a/src/util/messageCategory.ml +++ b/src/util/messageCategory.ml @@ -11,6 +11,7 @@ type undefined_behavior = | ArrayOutOfBounds of array_oob | NullPointerDereference | UseAfterFree + | MemoryOutOfBoundsAccess | Uninitialized | Other [@@deriving eq, ord, hash] @@ -62,6 +63,7 @@ struct let array_out_of_bounds e: category = create @@ ArrayOutOfBounds e let nullpointer_dereference: category = create @@ NullPointerDereference let use_after_free: category = create @@ UseAfterFree + let memory_out_of_bounds_access: category = create @@ MemoryOutOfBoundsAccess let uninitialized: category = create @@ Uninitialized let other: category = create @@ Other @@ -97,6 +99,7 @@ struct | "array_out_of_bounds" -> ArrayOutOfBounds.from_string_list t | "nullpointer_dereference" -> nullpointer_dereference | "use_after_free" -> use_after_free + | "memory_out_of_bounds_access" -> memory_out_of_bounds_access | "uninitialized" -> uninitialized | "other" -> other | _ -> Unknown @@ -106,6 +109,7 @@ struct | ArrayOutOfBounds e -> "ArrayOutOfBounds" :: ArrayOutOfBounds.path_show e | NullPointerDereference -> ["NullPointerDereference"] | UseAfterFree -> ["UseAfterFree"] + | MemoryOutOfBoundsAccess -> ["MemoryOutOfBoundsAccess"] | Uninitialized -> ["Uninitialized"] | Other -> ["Other"] end @@ -214,6 +218,7 @@ let behaviorName = function |Undefined u -> match u with |NullPointerDereference -> "NullPointerDereference" |UseAfterFree -> "UseAfterFree" + |MemoryOutOfBoundsAccess -> "MemoryOutOfBoundsAccess" |Uninitialized -> "Uninitialized" |Other -> "Other" | ArrayOutOfBounds aob -> match aob with From 84e80b1b7f97a0077dae1b63f974c8b0c62d8108 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 8 Jul 2023 16:42:08 +0200 Subject: [PATCH 08/35] Add CWE number 823 for memory OOB access warnings --- src/analyses/memOutOfBounds.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 7ea11e8ef1..ac2b909d6a 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -137,6 +137,7 @@ struct let rec check_lval_for_oob_access ctx (lval:lval) = let undefined_behavior = Undefined MemoryOutOfBoundsAccess in + let cwe_number = 823 in match lval_contains_a_ptr lval with | false -> () (* Nothing to do here *) | true -> @@ -149,10 +150,10 @@ struct begin match cilint_to_int_wrapper i with | Some i -> if i < oi then - M.warn ~category:(Behavior undefined_behavior) "Offset bigger than var type's size for lval %a. A memory out-of-bounds access must occur" CilType.Lval.pretty lval - | _ -> M.warn ~category:(Behavior undefined_behavior) "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Offset bigger than var type's size for lval %a. A memory out-of-bounds access must occur" CilType.Lval.pretty lval + | _ -> M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval end - | _ -> M.warn ~category:(Behavior undefined_behavior) "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval + | _ -> M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval end | Mem e, Some oi -> check_exp_for_oob_access ctx e; @@ -197,6 +198,7 @@ struct and check_binop_exp ctx (binop:binop) (e1:exp) (e2:exp) = let undefined_behavior = Undefined MemoryOutOfBoundsAccess in + let cwe_number = 823 in match binop with | PlusPI | IndexPI @@ -206,9 +208,9 @@ struct begin match ptr_size, offset_size with | Some pi, Some oi -> if pi < oi then - M.warn ~category:(Behavior undefined_behavior) "Pointer size in expression %a %a %a is smaller than offset for pointer arithmetic. Memory out-of-bounds access must occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 - | None, _ -> M.warn ~category:(Behavior undefined_behavior) "Pointer (%a) size in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp e1 CilType.Binop.pretty binop d_exp e2 - | _, None -> M.warn ~category:(Behavior undefined_behavior) "Operand value for pointer arithmetic in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Pointer size in expression %a %a %a is smaller than offset for pointer arithmetic. Memory out-of-bounds access must occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 + | None, _ -> M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Pointer (%a) size in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp e1 CilType.Binop.pretty binop d_exp e2 + | _, None -> M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 end | _ -> () From a07b6903ada4aed962efdba4619657d41273bfe8 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 8 Jul 2023 16:59:44 +0200 Subject: [PATCH 09/35] Add a global variable that indicates whether an invalid pointer deref happened --- src/analyses/memOutOfBounds.ml | 24 +++++++++++++++++++----- src/util/goblintutil.ml | 3 +++ 2 files changed, 22 insertions(+), 5 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index ac2b909d6a..415934b52d 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -2,6 +2,8 @@ open GoblintCil open Analyses open MessageCategory +module GU = Goblintutil + module Spec = struct include Analyses.IdentitySpec @@ -143,17 +145,24 @@ struct | true -> let (host, offset) = lval in match host, get_offset_size offset with - | _, None -> M.warn ~category:(Behavior undefined_behavior) "Offset size for lval %a not known. A memory out-of-bounds access may occur" CilType.Lval.pretty lval + | _, None -> + GU.may_invalid_deref := true; + M.warn ~category:(Behavior undefined_behavior) "Offset size for lval %a not known. A memory out-of-bounds access may occur" CilType.Lval.pretty lval | Var v, Some oi -> begin match sizeOf v.vtype with | Const (CInt (i, _, _)) -> begin match cilint_to_int_wrapper i with | Some i -> if i < oi then + GU.may_invalid_deref := true; M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Offset bigger than var type's size for lval %a. A memory out-of-bounds access must occur" CilType.Lval.pretty lval - | _ -> M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval + | _ -> + GU.may_invalid_deref := true; + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval end - | _ -> M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval + | _ -> + GU.may_invalid_deref := true; + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval end | Mem e, Some oi -> check_exp_for_oob_access ctx e; @@ -208,9 +217,14 @@ struct begin match ptr_size, offset_size with | Some pi, Some oi -> if pi < oi then + GU.may_invalid_deref := true; M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Pointer size in expression %a %a %a is smaller than offset for pointer arithmetic. Memory out-of-bounds access must occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 - | None, _ -> M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Pointer (%a) size in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp e1 CilType.Binop.pretty binop d_exp e2 - | _, None -> M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 + | None, _ -> + GU.may_invalid_deref := true; + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Pointer (%a) size in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp e1 CilType.Binop.pretty binop d_exp e2 + | _, None -> + GU.may_invalid_deref := true; + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 end | _ -> () diff --git a/src/util/goblintutil.ml b/src/util/goblintutil.ml index 2c49395915..ecaa38f338 100644 --- a/src/util/goblintutil.ml +++ b/src/util/goblintutil.ml @@ -14,6 +14,9 @@ let should_warn = ref false (** Whether signed overflow or underflow happened *) let svcomp_may_overflow = ref false +(** Whether an invalid pointer dereference happened *) +let may_invalid_deref = ref false + (** The file where everything is output *) let out = ref stdout From 4c093726b52ba1e3e0966ec5cded850d36bc87b6 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 26 Jul 2023 16:46:50 +0200 Subject: [PATCH 10/35] Add OOB memory access regression case with a loop --- tests/regression/73-mem-oob/03-oob-loop.c | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 tests/regression/73-mem-oob/03-oob-loop.c diff --git a/tests/regression/73-mem-oob/03-oob-loop.c b/tests/regression/73-mem-oob/03-oob-loop.c new file mode 100644 index 0000000000..5e0e08c381 --- /dev/null +++ b/tests/regression/73-mem-oob/03-oob-loop.c @@ -0,0 +1,16 @@ +// PARAM: --set ana.activated[+] memOutOfBounds +#include +#include + +int main(int argc, char const *argv[]) { + char *ptr = malloc(5 * sizeof(char)); + + for (int i = 0; i < 10; i++) { + ptr++; + } + + printf("%s", *ptr); //WARN + free(ptr); //WARN + + return 0; +} From 503fb2416b4669aedbf03f531e0eb405e85c2cd3 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 12 Aug 2023 08:11:06 +0200 Subject: [PATCH 11/35] Remove wrongly overtaken goblintutil.ml --- src/util/goblintutil.ml | 166 ---------------------------------------- 1 file changed, 166 deletions(-) delete mode 100644 src/util/goblintutil.ml diff --git a/src/util/goblintutil.ml b/src/util/goblintutil.ml deleted file mode 100644 index ecaa38f338..0000000000 --- a/src/util/goblintutil.ml +++ /dev/null @@ -1,166 +0,0 @@ -(** Globally accessible flags and utility functions. *) - -open GoblintCil -open GobConfig - - -(** Outputs information about what the goblin is doing *) -(* let verbose = ref false *) - -(** If this is true we output messages and collect accesses. - This is set to true in control.ml before we verify the result (or already before solving if warn = 'early') *) -let should_warn = ref false - -(** Whether signed overflow or underflow happened *) -let svcomp_may_overflow = ref false - -(** Whether an invalid pointer dereference happened *) -let may_invalid_deref = ref false - -(** The file where everything is output *) -let out = ref stdout - -(** Command for assigning an id to a varinfo. All varinfos directly created by Goblint should be modified by this method *) -let create_var (var: varinfo) = - (* TODO Hack: this offset should preempt conflicts with ids generated by CIL *) - let start_id = 10_000_000_000 in - let hash = Hashtbl.hash { var with vid = 0 } in - let hash = if hash < start_id then hash + start_id else hash in - { var with vid = hash } - -(* Type invariant variables. *) -let type_inv_tbl = Hashtbl.create 13 -let type_inv (c:compinfo) : varinfo = - try Hashtbl.find type_inv_tbl c.ckey - with Not_found -> - let i = create_var (makeGlobalVar ("{struct "^c.cname^"}") (TComp (c,[]))) in - Hashtbl.add type_inv_tbl c.ckey i; - i - -let is_blessed (t:typ): varinfo option = - let me_gusta x = List.mem x (get_string_list "exp.unique") in - match unrollType t with - | TComp (ci,_) when me_gusta ci.cname -> Some (type_inv ci) - | _ -> (None : varinfo option) - - -(** A hack to see if we are currently doing global inits *) -let global_initialization = ref false - -(** Another hack to see if earlyglobs is enabled *) -let earlyglobs = ref false - -(** Whether currently in postsolver evaluations (e.g. verify, warn) *) -let postsolving = ref false - -(* None if verification is disabled, Some true if verification succeeded, Some false if verification failed *) -let verified : bool option ref = ref None - -let escape = XmlUtil.escape (* TODO: inline everywhere *) - - -(** Creates a directory and returns the absolute path **) -let create_dir name = - let dirName = GobFpath.cwd_append name in - GobSys.mkdir_or_exists dirName; - dirName - -(** Remove directory and its content, as "rm -rf" would do. *) -let rm_rf path = - let rec f path = - let path_str = Fpath.to_string path in - if Sys.is_directory path_str then begin - let files = Array.map (Fpath.add_seg path) (Sys.readdir path_str) in - Array.iter f files; - Unix.rmdir path_str - end else - Sys.remove path_str - in - f path - - -exception Timeout - -let timeout = Timeout.timeout - -let seconds_of_duration_string = - let unit = function - | "" | "s" -> 1 - | "m" -> 60 - | "h" -> 60 * 60 - | s -> failwith ("Unkown duration unit " ^ s ^ ". Supported units are h, m, s.") - in - let int_rest f s = Scanf.sscanf s "%u%s" f in - let split s = BatString.(head s 1, tail s 1) in - let rec f i s = - let u, r = split s in (* unit, rest *) - i * (unit u) + if r = "" then 0 else int_rest f r - in - int_rest f - -let vars = ref 0 -let evals = ref 0 -let narrow_reuses = ref 0 - -(* print GC statistics; taken from Cil.Stats.print which also includes timing; there's also Gc.print_stat, but it's in words instead of MB and more info than we want (also slower than quick_stat since it goes through the heap) *) -let print_gc_quick_stat chn = - let gc = Gc.quick_stat () in - let printM (w: float) : string = - let coeff = float_of_int (Sys.word_size / 8) in - Printf.sprintf "%.2fMB" (w *. coeff /. 1000000.0) - in - Printf.fprintf chn - "Memory statistics: total=%s, max=%s, minor=%s, major=%s, promoted=%s\n minor collections=%d major collections=%d compactions=%d\n" - (printM (gc.Gc.minor_words +. gc.Gc.major_words - -. gc.Gc.promoted_words)) - (printM (float_of_int gc.Gc.top_heap_words)) - (printM gc.Gc.minor_words) - (printM gc.Gc.major_words) - (printM gc.Gc.promoted_words) - gc.Gc.minor_collections - gc.Gc.major_collections - gc.Gc.compactions; - gc - -let exe_dir = Fpath.(parent (v Sys.executable_name)) -let command_line = match Array.to_list Sys.argv with - | command :: arguments -> Filename.quote_command command arguments - | [] -> assert false - -(* https://ocaml.org/api/Sys.html#2_SignalnumbersforthestandardPOSIXsignals *) -(* https://ocaml.github.io/ocamlunix/signals.html *) -let signal_of_string = let open Sys in function - | "sigint" -> sigint (* Ctrl+C Interactive interrupt *) - | "sigtstp" -> sigtstp (* Ctrl+Z Interactive stop *) - | "sigquit" -> sigquit (* Ctrl+\ Interactive termination *) - | "sigalrm" -> sigalrm (* Timeout *) - | "sigkill" -> sigkill (* Termination (cannot be ignored) *) - | "sigsegv" -> sigsegv (* Invalid memory reference, https://github.com/goblint/analyzer/issues/206 *) - | "sigterm" -> sigterm (* Termination *) - | "sigusr1" -> sigusr1 (* Application-defined signal 1 *) - | "sigusr2" -> sigusr2 (* Application-defined signal 2 *) - | "sigstop" -> sigstop (* Stop *) - | "sigprof" -> sigprof (* Profiling interrupt *) - | "sigxcpu" -> sigxcpu (* Timeout in cpu time *) - | s -> failwith ("Unhandled signal " ^ s) - -let self_signal signal = Unix.kill (Unix.getpid ()) signal - -let rec for_all_in_range (a, b) f = - let module BI = IntOps.BigIntOps in - if BI.compare a b > 0 - then true - else f a && (for_all_in_range (BI.add a (BI.one), b) f) - -let dummy_obj = Obj.repr () - -let jobs () = - match get_int "jobs" with - | 0 -> Cpu.numcores () - | n -> n - -(** call [f], with [r] temporarily set to [x] *) -let with_ref r x = - let x0 = !r in - r := x; - Fun.protect ~finally:(fun () -> r := x0) From 0c53230cd3e0404f86fd2c3de0bc91863eeb7af5 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 12 Aug 2023 08:18:01 +0200 Subject: [PATCH 12/35] Move may_invalid_deref to analysisState --- src/framework/analysisState.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/framework/analysisState.ml b/src/framework/analysisState.ml index 0f3a9f55bc..32b4e4d608 100644 --- a/src/framework/analysisState.ml +++ b/src/framework/analysisState.ml @@ -7,6 +7,9 @@ let should_warn = ref false (** Whether signed overflow or underflow happened *) let svcomp_may_overflow = ref false +(** Whether an invalid pointer dereference happened *) +let svcomp_may_invalid_deref = ref false + (** A hack to see if we are currently doing global inits *) let global_initialization = ref false From c07d867dd75287f00afdbf1c1be1b8a02d463542 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 12 Aug 2023 08:19:23 +0200 Subject: [PATCH 13/35] Use AnalysisState in place of Goblintutil --- src/analyses/memOutOfBounds.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 415934b52d..85e8530de7 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -2,7 +2,7 @@ open GoblintCil open Analyses open MessageCategory -module GU = Goblintutil +module AS = AnalysisState module Spec = struct @@ -146,7 +146,7 @@ struct let (host, offset) = lval in match host, get_offset_size offset with | _, None -> - GU.may_invalid_deref := true; + AS.svcomp_may_invalid_deref := true; M.warn ~category:(Behavior undefined_behavior) "Offset size for lval %a not known. A memory out-of-bounds access may occur" CilType.Lval.pretty lval | Var v, Some oi -> begin match sizeOf v.vtype with @@ -154,14 +154,14 @@ struct begin match cilint_to_int_wrapper i with | Some i -> if i < oi then - GU.may_invalid_deref := true; + AS.svcomp_may_invalid_deref := true; M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Offset bigger than var type's size for lval %a. A memory out-of-bounds access must occur" CilType.Lval.pretty lval | _ -> - GU.may_invalid_deref := true; + AS.svcomp_may_invalid_deref := true; M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval end | _ -> - GU.may_invalid_deref := true; + AS.svcomp_may_invalid_deref := true; M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval end | Mem e, Some oi -> @@ -217,13 +217,13 @@ struct begin match ptr_size, offset_size with | Some pi, Some oi -> if pi < oi then - GU.may_invalid_deref := true; + AS.svcomp_may_invalid_deref := true; M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Pointer size in expression %a %a %a is smaller than offset for pointer arithmetic. Memory out-of-bounds access must occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 | None, _ -> - GU.may_invalid_deref := true; + AS.svcomp_may_invalid_deref := true; M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Pointer (%a) size in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp e1 CilType.Binop.pretty binop d_exp e2 | _, None -> - GU.may_invalid_deref := true; + AS.svcomp_may_invalid_deref := true; M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 end | _ -> () From 434a4c1202382e0a0965a0792948423181bf3813 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 20 Aug 2023 18:39:19 +0200 Subject: [PATCH 14/35] Enable intervals for regression tests --- tests/regression/73-mem-oob/01-oob-heap-simple.c | 2 +- tests/regression/73-mem-oob/02-oob-stack-simple.c | 2 +- tests/regression/73-mem-oob/03-oob-loop.c | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/regression/73-mem-oob/01-oob-heap-simple.c b/tests/regression/73-mem-oob/01-oob-heap-simple.c index 91d9c7605a..10c7864184 100644 --- a/tests/regression/73-mem-oob/01-oob-heap-simple.c +++ b/tests/regression/73-mem-oob/01-oob-heap-simple.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] memOutOfBounds +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval #include int main(int argc, char const *argv[]) { diff --git a/tests/regression/73-mem-oob/02-oob-stack-simple.c b/tests/regression/73-mem-oob/02-oob-stack-simple.c index deedd52781..8d022feca4 100644 --- a/tests/regression/73-mem-oob/02-oob-stack-simple.c +++ b/tests/regression/73-mem-oob/02-oob-stack-simple.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] memOutOfBounds +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval #include int main(int argc, char const *argv[]) { diff --git a/tests/regression/73-mem-oob/03-oob-loop.c b/tests/regression/73-mem-oob/03-oob-loop.c index 5e0e08c381..c800597757 100644 --- a/tests/regression/73-mem-oob/03-oob-loop.c +++ b/tests/regression/73-mem-oob/03-oob-loop.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] memOutOfBounds +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval #include #include From 3db3d8c7c3c42588dc970d4b8f0219ee04a3d6a9 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 20 Aug 2023 19:06:51 +0200 Subject: [PATCH 15/35] Fix memOutOfBounds analysis and make it work --- src/analyses/memOutOfBounds.ml | 212 ++++++++++----------------------- 1 file changed, 66 insertions(+), 146 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 85e8530de7..c4e5f59bc2 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -3,28 +3,22 @@ open Analyses open MessageCategory module AS = AnalysisState +module VDQ = ValueDomainQueries module Spec = struct include Analyses.IdentitySpec module D = Lattice.Unit - module C = Lattice.Unit + module C = D - (* TODO: Do this later *) + (* TODO: Check out later for benchmarking *) let context _ _ = () let name () = "memOutOfBounds" (* HELPER FUNCTIONS *) - - (* A safe way to call [cilint_to_int] without having to worry about exceptions *) - let cilint_to_int_wrapper i = - try - Some (cilint_to_int i) - with _ -> None - let rec exp_contains_a_ptr (exp:exp) = match exp with | Const _ @@ -59,128 +53,57 @@ struct in host_contains_a_ptr host || offset_contains_a_ptr offset - let lval_is_ptr_var (lval:lval) = - let (host, _) = lval in - match host with - | Var v -> isPointerType v.vtype - (* Intuition: If the lval has a Mem host, then it's not a direct ptr which is what we're looking for here *) - | Mem e -> false - - let exp_points_to_heap ctx (exp:exp) = - match ctx.ask (Queries.MayPointTo exp) with + let points_to_heap_only ctx ptr = + match ctx.ask (Queries.MayPointTo ptr) with | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> - Queries.LS.elements a - |> List.map fst - |> List.exists (fun x -> ctx.ask (Queries.IsHeapVar x)) - | _ -> false (* TODO: Is this sound? Maybe not quite. *) - - let get_size_for_heap_ptr ctx (exp:exp) = - (* TODO: - BlobSize always seems to respond with top when it's passed an Lval exp of a ptr var which in turn contains mem allocated via malloc. - Am I doing smth wrong here? - *) - match ctx.ask (Queries.BlobSize exp) with - | a when not (Queries.ID.is_top a) -> - begin match Queries.ID.to_int a with - | Some i -> Some (IntOps.BigIntOps.to_int i) - | None -> None - end - | _ -> None - - (* TODO: Here we assume that the given exp is a Lval exp *) - let get_size_for_stack_ptr ctx (exp:exp) = - match exp with - | Lval lval -> - if lval_is_ptr_var lval then - let (host, _) = lval in - begin match host with - | Var v -> - begin match sizeOf v.vtype with - | Const (CInt (i, _, _)) -> cilint_to_int_wrapper i - | _ -> None - end - | _ -> None + Queries.LS.for_all (fun (v, _) -> ctx.ask (Queries.IsHeapVar v)) a + | _ -> false + + let get_size_of_ptr_target ctx ptr = + (* Call Queries.BlobSize only if ptr points solely to the heap. Otherwise we get bot *) + if points_to_heap_only ctx ptr then + ctx.ask (Queries.BlobSize ptr) + else + match ctx.ask (Queries.MayPointTo ptr) with + | a when not (Queries.LS.is_top a) -> + let pts_list = Queries.LS.elements a in + let pts_elems_to_sizes (v, _) = + if isArrayType v.vtype then + ctx.ask (Queries.EvalLength ptr) + else + let var_type_size = match Cil.getInteger (sizeOf v.vtype) with + | Some z -> + let ikindOfTypeSize = intKindForValue z true in + VDQ.ID.of_int ikindOfTypeSize z + | None -> VDQ.ID.bot () + in + var_type_size + in + (* Map each points-to-set element to its size *) + let pts_sizes = List.map pts_elems_to_sizes pts_list in + (* Take the smallest of all sizes that ptr's contents may have *) + begin match pts_sizes with + | [] -> VDQ.ID.bot () + | [x] -> x + | x::xs -> List.fold_left (fun acc elem -> + if VDQ.ID.compare acc elem >= 0 then elem else acc + ) x xs end - else None - | _ -> None + | _ -> + M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; + VDQ.ID.top () - let get_ptr_size_for_exp ctx (exp:exp) = - match exp_points_to_heap ctx exp with - (* We're dealing with a ptr that points to the heap *) - | true -> get_size_for_heap_ptr ctx exp - (* Assumption here is that if it doesn't point to the heap, then it points to the stack *) - | false -> get_size_for_stack_ptr ctx exp + let eval_ptr_offset_in_binop ctx exp = + ctx.ask (Queries.EvalInt exp) - (** - * If we get [None], then the offset's size/value is unknown - * In the case [NoOffset], [Some 0] indicates that this offset type simply has value 0 - *) - let rec get_offset_size = function - | NoOffset -> Some 0 - | Index (e, o) -> - let exp_val = begin match constFold true e with - | Const (CInt (i, _, _)) -> cilint_to_int_wrapper i - | _ -> None - end - in - begin match exp_val, get_offset_size o with - | Some ei, Some oi -> Some (ei + oi) - | _, _ -> None - end - | Field (f, o) -> - begin match get_offset_size o, sizeOf f.ftype with - | Some oi, Const (CInt (i, _, _)) -> - begin match cilint_to_int_wrapper i with - | Some i -> Some (oi + i) - | None -> None - end - | _, _ -> None - end - - let rec check_lval_for_oob_access ctx (lval:lval) = - let undefined_behavior = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in - match lval_contains_a_ptr lval with - | false -> () (* Nothing to do here *) - | true -> - let (host, offset) = lval in - match host, get_offset_size offset with - | _, None -> - AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior undefined_behavior) "Offset size for lval %a not known. A memory out-of-bounds access may occur" CilType.Lval.pretty lval - | Var v, Some oi -> - begin match sizeOf v.vtype with - | Const (CInt (i, _, _)) -> - begin match cilint_to_int_wrapper i with - | Some i -> - if i < oi then - AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Offset bigger than var type's size for lval %a. A memory out-of-bounds access must occur" CilType.Lval.pretty lval - | _ -> - AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval - end - | _ -> - AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Unknown size of var %a for lval %a. A memory out-of-bounds access might occur" CilType.Varinfo.pretty v CilType.Lval.pretty lval - end - | Mem e, Some oi -> - check_exp_for_oob_access ctx e; - (* TODO: - * Not sure if we actually need these checks below. - * They never seem to apply - * I.e., for ptrs, it always seems to be the case that we have a binop which adds the offset to the ptr - instead of having the offset represented as an offset of the lval - * For this reason, the checks below are currently commented out - *) - (* begin match get_ptr_size_for_exp ctx e with - | Some ei -> - if ei < oi then - M.warn "Offset bigger than size of pointer memory, denoted by expression %a in lval %a" d_exp e CilType.Lval.pretty lval - | _ -> M.warn "Unknown size of pointer memory, denoted by exp %a for lval %a" d_exp e CilType.Lval.pretty lval - end *) + let rec check_lval_for_oob_access ctx lval = + if not @@ lval_contains_a_ptr lval then () + else + match lval with + | Var _, _ -> () + | Mem e, _ -> check_exp_for_oob_access ctx e - and check_exp_for_oob_access ctx (exp:exp) = + and check_exp_for_oob_access ctx exp = match exp with | Const _ | SizeOf _ @@ -193,8 +116,8 @@ struct | AlignOfE e | UnOp (_, e, _) | CastE (_, e) -> check_exp_for_oob_access ctx e - | BinOp (bop, e1, e2, _) -> - check_binop_exp ctx bop e1 e2; + | BinOp (bop, e1, e2, t) -> + check_binop_exp ctx bop e1 e2 t; check_exp_for_oob_access ctx e1; check_exp_for_oob_access ctx e2 | Question (e1, e2, e3, _) -> @@ -205,34 +128,31 @@ struct | StartOf lval | AddrOf lval -> check_lval_for_oob_access ctx lval - and check_binop_exp ctx (binop:binop) (e1:exp) (e2:exp) = - let undefined_behavior = Undefined MemoryOutOfBoundsAccess in + and check_binop_exp ctx binop e1 e2 t = + 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_ptr_size_for_exp ctx e1 in - let offset_size = eval_ptr_offset_in_binop e2 in - begin match ptr_size, offset_size with - | Some pi, Some oi -> - if pi < oi then - AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Pointer size in expression %a %a %a is smaller than offset for pointer arithmetic. Memory out-of-bounds access must occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 - | None, _ -> + let ptr_size = get_size_of_ptr_target ctx e1 in + let offset_size = eval_ptr_offset_in_binop ctx e2 in + begin match VDQ.ID.is_top ptr_size, VDQ.ID.is_top offset_size with + | true, _ -> AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Pointer (%a) size in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp e1 CilType.Binop.pretty binop d_exp e2 - | _, None -> + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Pointer (%a) size in expression %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp + | _, true -> AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a %a %a not known. Memory out-of-bounds access might occur" d_exp e1 CilType.Binop.pretty binop d_exp e2 + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a not known. Memory out-of-bounds access might occur" d_exp binopexp + | false, false -> + if ptr_size < offset_size then begin + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Pointer size (%a) in expression %a is smaller than offset (%a) for pointer arithmetic. Memory out-of-bounds access must occur" VDQ.ID.pretty ptr_size d_exp binopexp VDQ.ID.pretty offset_size + end end | _ -> () - and eval_ptr_offset_in_binop (exp:exp) = - match constFold true exp with - | Const (CInt (i, _, _)) -> cilint_to_int_wrapper i - | _ -> None (* TODO: Maybe try to also Eval the exp via Queries and not rely only on constFold *) - (* TRANSFER FUNCTIONS *) From 6e7664d47f2c85e3cc40cd4ff571038ee55da059 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 20 Aug 2023 19:08:28 +0200 Subject: [PATCH 16/35] Remove unused transfer funs --- src/analyses/memOutOfBounds.ml | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index c4e5f59bc2..655596d3ec 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -174,12 +174,6 @@ struct List.iter (fun arg -> check_exp_for_oob_access ctx arg) arglist; ctx.local - let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = - [ctx.local, ctx.local] - - let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t = - ctx.local - let combine_assign ctx (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 ctx x) lval; List.iter (fun arg -> check_exp_for_oob_access ctx arg) args; From 79d4319ae752893680ed1fa7d7ed2be067629b16 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 20 Aug 2023 19:10:54 +0200 Subject: [PATCH 17/35] Move regression tests to a correctly numbered folder --- tests/regression/{73-mem-oob => 77-mem-oob}/01-oob-heap-simple.c | 0 tests/regression/{73-mem-oob => 77-mem-oob}/02-oob-stack-simple.c | 0 tests/regression/{73-mem-oob => 77-mem-oob}/03-oob-loop.c | 0 3 files changed, 0 insertions(+), 0 deletions(-) rename tests/regression/{73-mem-oob => 77-mem-oob}/01-oob-heap-simple.c (100%) rename tests/regression/{73-mem-oob => 77-mem-oob}/02-oob-stack-simple.c (100%) rename tests/regression/{73-mem-oob => 77-mem-oob}/03-oob-loop.c (100%) diff --git a/tests/regression/73-mem-oob/01-oob-heap-simple.c b/tests/regression/77-mem-oob/01-oob-heap-simple.c similarity index 100% rename from tests/regression/73-mem-oob/01-oob-heap-simple.c rename to tests/regression/77-mem-oob/01-oob-heap-simple.c diff --git a/tests/regression/73-mem-oob/02-oob-stack-simple.c b/tests/regression/77-mem-oob/02-oob-stack-simple.c similarity index 100% rename from tests/regression/73-mem-oob/02-oob-stack-simple.c rename to tests/regression/77-mem-oob/02-oob-stack-simple.c diff --git a/tests/regression/73-mem-oob/03-oob-loop.c b/tests/regression/77-mem-oob/03-oob-loop.c similarity index 100% rename from tests/regression/73-mem-oob/03-oob-loop.c rename to tests/regression/77-mem-oob/03-oob-loop.c From 84bd2cc7331e949607d5b48c3b0766d4c436e20e Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 20 Aug 2023 19:13:37 +0200 Subject: [PATCH 18/35] Add comments to 77/03 test case --- tests/regression/77-mem-oob/03-oob-loop.c | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tests/regression/77-mem-oob/03-oob-loop.c b/tests/regression/77-mem-oob/03-oob-loop.c index c800597757..502a4cc0e2 100644 --- a/tests/regression/77-mem-oob/03-oob-loop.c +++ b/tests/regression/77-mem-oob/03-oob-loop.c @@ -9,8 +9,10 @@ int main(int argc, char const *argv[]) { ptr++; } - printf("%s", *ptr); //WARN - free(ptr); //WARN + //TODO: We cannot currently detect OOB memory accesses happening due to loops like the one above + // => Both lines below can't have WARNs for now + printf("%s", *ptr); //NOWARN + free(ptr); //NOWARN return 0; } From 6ed476e3216d808fb6e6a16a6b15ca19c93efbfd Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Mon, 21 Aug 2023 18:17:46 +0200 Subject: [PATCH 19/35] Warn for function args in enter and not in combine_assign --- src/analyses/memOutOfBounds.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 655596d3ec..cfab5c8b73 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -174,9 +174,12 @@ struct List.iter (fun arg -> check_exp_for_oob_access ctx arg) arglist; ctx.local + let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = + List.iter (fun arg -> check_exp_for_oob_access ctx arg) args; + [ctx.local, ctx.local] + let combine_assign ctx (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 ctx x) lval; - List.iter (fun arg -> check_exp_for_oob_access ctx arg) args; ctx.local let startstate v = () From 4e7b21b7d4c411eaf3576438ac599df91a1a2af9 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 24 Aug 2023 12:20:21 +0200 Subject: [PATCH 20/35] Try to check and warn only upon dereferences Also slightly change some warning messages --- src/analyses/memOutOfBounds.ml | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index cfab5c8b73..9a03968ca3 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -101,7 +101,17 @@ struct else match lval with | Var _, _ -> () - | Mem e, _ -> check_exp_for_oob_access ctx e + | Mem e, _ -> + begin match e with + | Lval lval -> check_lval_for_oob_access ctx lval + | BinOp (PlusPI as binop, e1, e2, t) + | BinOp (MinusPI as binop, e1, e2, t) + | BinOp (IndexPI as binop, e1, e2, t) -> + check_binop_exp ctx binop e1 e2 t; + check_exp_for_oob_access ctx e1; + check_exp_for_oob_access ctx e2 + | _ -> check_exp_for_oob_access ctx e + end and check_exp_for_oob_access ctx exp = match exp with @@ -117,7 +127,6 @@ struct | UnOp (_, e, _) | CastE (_, e) -> check_exp_for_oob_access ctx e | BinOp (bop, e1, e2, t) -> - check_binop_exp ctx bop e1 e2 t; check_exp_for_oob_access ctx e1; check_exp_for_oob_access ctx e2 | Question (e1, e2, e3, _) -> @@ -141,14 +150,14 @@ struct begin match VDQ.ID.is_top ptr_size, VDQ.ID.is_top offset_size with | true, _ -> AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Pointer (%a) size in expression %a not known. 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 not known. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp | _, true -> AS.svcomp_may_invalid_deref := true; M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a not known. Memory out-of-bounds access might occur" d_exp binopexp | false, false -> if ptr_size < offset_size then begin AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Pointer size (%a) in expression %a is smaller than offset (%a) for pointer arithmetic. Memory out-of-bounds access must occur" VDQ.ID.pretty ptr_size d_exp binopexp VDQ.ID.pretty offset_size + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is smaller than offset %a for pointer arithmetic. Memory out-of-bounds access must occur" VDQ.ID.pretty ptr_size d_exp binopexp VDQ.ID.pretty offset_size end end | _ -> () From 291d60cd20d2a5ed29c3d76cd1e4cc05b07a562f Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 25 Aug 2023 18:40:20 +0200 Subject: [PATCH 21/35] Check for OOB mem access on the address level and only warn on deref --- src/analyses/memOutOfBounds.ml | 195 ++++++++++++++++++++++++++++----- 1 file changed, 166 insertions(+), 29 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 9a03968ca3..4b6c6db43f 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -19,6 +19,36 @@ struct (* HELPER FUNCTIONS *) + let intdom_of_int x = + IntDomain.IntDomTuple.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) + + let to_index ?typ offs = + let idx_of_int x = + IntDomain.IntDomTuple.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int (x / 8)) + in + let rec offset_to_index_offset ?typ offs = match offs with + | `NoOffset -> idx_of_int 0 + | `Field (field, o) -> + let field_as_offset = Field (field, NoOffset) in + let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in + let bits_offset = idx_of_int bits_offset in + let remaining_offset = offset_to_index_offset ~typ:field.ftype o in + IntDomain.IntDomTuple.add bits_offset remaining_offset + | `Index (x, o) -> + let (item_typ, item_size_in_bits) = + match Option.map unrollType typ with + | Some TArray(item_typ, _, _) -> + let item_size_in_bits = bitsSizeOf item_typ in + (Some item_typ, idx_of_int item_size_in_bits) + | _ -> + (None, IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind ()) + in + let bits_offset = IntDomain.IntDomTuple.mul item_size_in_bits x in + let remaining_offset = offset_to_index_offset ?typ:item_typ o in + IntDomain.IntDomTuple.add bits_offset remaining_offset + in + offset_to_index_offset ?typ offs + let rec exp_contains_a_ptr (exp:exp) = match exp with | Const _ @@ -61,6 +91,14 @@ struct let get_size_of_ptr_target ctx ptr = (* Call Queries.BlobSize only if ptr points solely to the heap. Otherwise we get bot *) + (* TODO: + * If the ptr's address has been offset, then Queries.BlobSize will answer with bot. For example: + char *ptr = malloc(10 * sizeof(char)); + ptr++; + printf("%s", *ptr); // => Issues a WARN even though it shouldn't + * However, in this case we're too imprecise, since we're always comparing something with bot + * and thus we always get a warning for an OOB memory access. Should we maybe change Queries.BlobSize again? + *) if points_to_heap_only ctx ptr then ctx.ask (Queries.BlobSize ptr) else @@ -68,16 +106,19 @@ struct | a when not (Queries.LS.is_top a) -> let pts_list = Queries.LS.elements a in let pts_elems_to_sizes (v, _) = - if isArrayType v.vtype then - ctx.ask (Queries.EvalLength ptr) - else - let var_type_size = match Cil.getInteger (sizeOf v.vtype) with - | Some z -> - let ikindOfTypeSize = intKindForValue z true in - VDQ.ID.of_int ikindOfTypeSize z - | None -> VDQ.ID.bot () - in - var_type_size + begin match v.vtype with + | TArray (item_typ, _, _) -> + let item_typ_size_in_bytes = (bitsSizeOf item_typ) / 8 in + let item_typ_size_in_bytes = intdom_of_int item_typ_size_in_bytes in + begin match ctx.ask (Queries.EvalLength ptr) with + | `Lifted arr_len -> `Lifted (IntDomain.IntDomTuple.mul item_typ_size_in_bytes arr_len) + | `Bot -> VDQ.ID.bot () + | `Top -> VDQ.ID.top () + end + | _ -> + let type_size_in_bytes = (bitsSizeOf v.vtype) / 8 in + `Lifted (intdom_of_int type_size_in_bytes) + end in (* Map each points-to-set element to its size *) let pts_sizes = List.map pts_elems_to_sizes pts_list in @@ -93,26 +134,109 @@ struct M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; VDQ.ID.top () - let eval_ptr_offset_in_binop ctx exp = - ctx.ask (Queries.EvalInt exp) + let get_ptr_deref_type ptr_typ = + match ptr_typ with + | TPtr (t, _) -> Some t + | _ -> None - let rec check_lval_for_oob_access ctx lval = + let size_of_type_in_bytes typ = + let typ_size_in_bytes = (bitsSizeOf typ) / 8 in + intdom_of_int typ_size_in_bytes + + let eval_ptr_offset_in_binop ctx exp ptr_contents_typ = + let eval_offset = ctx.ask (Queries.EvalInt exp) in + let eval_offset = Option.get @@ VDQ.ID.to_int eval_offset in + let eval_offset = VDQ.ID.of_int (Cilfacade.ptrdiff_ikind ()) eval_offset in + let ptr_contents_typ_size_in_bytes = size_of_type_in_bytes ptr_contents_typ in + match eval_offset with + | `Lifted i -> `Lifted (IntDomain.IntDomTuple.mul i ptr_contents_typ_size_in_bytes) + | `Top -> `Top + | `Bot -> `Bot + + let rec offs_to_idx typ offs = + match offs with + | `NoOffset -> intdom_of_int 0 + | `Field (field, o) -> + let field_as_offset = Field (field, NoOffset) in + let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in + let bytes_offset = intdom_of_int (bits_offset / 8) in + let remaining_offset = offs_to_idx field.ftype o in + IntDomain.IntDomTuple.add bytes_offset remaining_offset + | `Index (x, o) -> + let typ_size_in_bytes = size_of_type_in_bytes typ in + let bytes_offset = IntDomain.IntDomTuple.mul typ_size_in_bytes x in + let remaining_offset = offs_to_idx typ o in + IntDomain.IntDomTuple.add bytes_offset remaining_offset + + let rec get_addr_offs ctx ptr = + match ctx.ask (Queries.MayPointTo ptr) with + | a when not (VDQ.LS.is_top a) -> + let ptr_deref_type = get_ptr_deref_type @@ typeOf ptr in + begin match ptr_deref_type with + | Some t -> + begin match VDQ.LS.is_empty a with + | true -> + M.warn "Pointer %a has an empty points-to-set" d_exp ptr; + IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + | false -> + (* + Offset should be the same for all elements in the points-to set. + Hence, we can just pick one element and obtain its offset + TODO: Does this make sense? + *) + let (_, o) = VDQ.LS.choose a in + let rec to_int_dom_offs = function + | `NoOffset -> `NoOffset + | `Field (f, o) -> `Field (f, to_int_dom_offs o) + | `Index (i, o) -> `Index (VDQ.ID.unlift (fun x -> x) @@ ctx.ask (Queries.EvalInt i), to_int_dom_offs o) + in + offs_to_idx t (to_int_dom_offs o) + end + | None -> + M.error "Expression %a doesn't have pointer type" d_exp ptr; + IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + end + | _ -> + M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; + IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + + and check_lval_for_oob_access ctx lval = if not @@ lval_contains_a_ptr lval then () else match lval with | Var _, _ -> () | Mem e, _ -> begin match e with - | Lval lval -> check_lval_for_oob_access ctx lval - | BinOp (PlusPI as binop, e1, e2, t) - | BinOp (MinusPI as binop, e1, e2, t) - | BinOp (IndexPI as binop, e1, e2, t) -> + | Lval (Var v, _) as lval_exp -> check_no_binop_deref ctx lval_exp + | BinOp (binop, e1, e2, t) when binop = PlusPI || binop = MinusPI || binop = IndexPI -> check_binop_exp ctx binop e1 e2 t; check_exp_for_oob_access ctx e1; check_exp_for_oob_access ctx e2 | _ -> check_exp_for_oob_access ctx e end + and check_no_binop_deref ctx lval_exp = + let behavior = Undefined MemoryOutOfBoundsAccess in + let cwe_number = 823 in + let ptr_size = get_size_of_ptr_target ctx lval_exp in + let addr_offs = get_addr_offs ctx 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 -> + begin match VDQ.ID.is_top ptr_size with + | true -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a not known. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp + | false -> + let offs = `Lifted addr_offs in + if ptr_size < offs then begin + AS.svcomp_may_invalid_deref := true; + 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" VDQ.ID.pretty ptr_size VDQ.ID.pretty offs + end + end + | _ -> M.error "Expression %a is not a pointer" d_exp lval_exp + and check_exp_for_oob_access ctx exp = match exp with | Const _ @@ -146,19 +270,32 @@ struct | IndexPI | MinusPI -> let ptr_size = get_size_of_ptr_target ctx e1 in - let offset_size = eval_ptr_offset_in_binop ctx e2 in - begin match VDQ.ID.is_top ptr_size, VDQ.ID.is_top offset_size with - | true, _ -> - AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp - | _, true -> - AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a not known. Memory out-of-bounds access might occur" d_exp binopexp - | false, false -> - if ptr_size < offset_size then begin - AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is smaller than offset %a for pointer arithmetic. Memory out-of-bounds access must occur" VDQ.ID.pretty ptr_size d_exp binopexp VDQ.ID.pretty offset_size + let addr_offs = get_addr_offs ctx 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 ctx 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 -> `Lifted (IntDomain.IntDomTuple.add os addr_offs) + | `Top -> `Top + | `Bot -> `Bot + in + begin match VDQ.ID.is_top ptr_size, VDQ.ID.is_top offset_size_with_addr_size with + | true, _ -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp + | _, true -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a not known. Memory out-of-bounds access might occur" d_exp binopexp + | false, false -> + if ptr_size < offset_size_with_addr_size then begin + AS.svcomp_may_invalid_deref := true; + 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 VDQ.ID.pretty ptr_size VDQ.ID.pretty offset_size_with_addr_size + end end + | _ -> M.error "Binary expression %a doesn't have a pointer" d_exp binopexp end | _ -> () From 2a3aaaec12b59236608b7b2e4c81e2fe27f3de36 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 25 Aug 2023 18:40:53 +0200 Subject: [PATCH 22/35] Adjust the OOB mem access test case with a loop --- tests/regression/77-mem-oob/03-oob-loop.c | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/tests/regression/77-mem-oob/03-oob-loop.c b/tests/regression/77-mem-oob/03-oob-loop.c index 502a4cc0e2..4f637d487e 100644 --- a/tests/regression/77-mem-oob/03-oob-loop.c +++ b/tests/regression/77-mem-oob/03-oob-loop.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +// PARAM: --set ana.activated[+] memOutOfBounds --set exp.unrolling-factor 10 --enable ana.int.interval #include #include @@ -9,10 +9,8 @@ int main(int argc, char const *argv[]) { ptr++; } - //TODO: We cannot currently detect OOB memory accesses happening due to loops like the one above - // => Both lines below can't have WARNs for now - printf("%s", *ptr); //NOWARN - free(ptr); //NOWARN + printf("%s", *ptr); //WARN + free(ptr); //WARN return 0; } From 46bd81f482cc6407eeddd32297676fbc9b21bb79 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 25 Aug 2023 18:46:05 +0200 Subject: [PATCH 23/35] Add test case with pointer arithmetic and subsequent derefs --- .../77-mem-oob/04-oob-deref-after-ptr-arith.c | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c diff --git a/tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c b/tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c new file mode 100644 index 0000000000..5046a00664 --- /dev/null +++ b/tests/regression/77-mem-oob/04-oob-deref-after-ptr-arith.c @@ -0,0 +1,18 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include +#include + +int main(int argc, char const *argv[]) { + char *ptr = malloc(5 * sizeof(char)); + + ptr++;//NOWARN + printf("%s", *ptr);//NOWARN + ptr = ptr + 5;//NOWARN + printf("%s", *ptr);//WARN + *(ptr + 1) = 'b';//WARN + *(ptr + 10) = 'c';//WARN + + free(ptr); + + return 0; +} From 37fb4e8173a3e1d1b3b6b404219bc9b681e01721 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 25 Aug 2023 18:51:05 +0200 Subject: [PATCH 24/35] Refactor to_int_dom_offs --- src/analyses/memOutOfBounds.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 4b6c6db43f..329539ebfb 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -188,7 +188,12 @@ struct let rec to_int_dom_offs = function | `NoOffset -> `NoOffset | `Field (f, o) -> `Field (f, to_int_dom_offs o) - | `Index (i, o) -> `Index (VDQ.ID.unlift (fun x -> x) @@ ctx.ask (Queries.EvalInt i), to_int_dom_offs o) + | `Index (i, o) -> + let exp_as_int_dom = match ctx.ask (Queries.EvalInt i) with + | `Lifted i -> i + | _ -> IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + in + `Index (exp_as_int_dom, to_int_dom_offs o) in offs_to_idx t (to_int_dom_offs o) end From ff3e644d81efdd7f5adaadaec31f8cff99b0b77c Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 25 Aug 2023 18:52:41 +0200 Subject: [PATCH 25/35] Cover bot and top cases in to_int_dom_offs --- src/analyses/memOutOfBounds.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 329539ebfb..2b4ca3d4c4 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -191,7 +191,8 @@ struct | `Index (i, o) -> let exp_as_int_dom = match ctx.ask (Queries.EvalInt i) with | `Lifted i -> i - | _ -> IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + | `Bot -> IntDomain.IntDomTuple.bot_of @@ Cilfacade.ptrdiff_ikind () + | `Top -> IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () in `Index (exp_as_int_dom, to_int_dom_offs o) in From aceffa897f7294261db65e2531661c64239a0376 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 31 Aug 2023 16:48:35 +0200 Subject: [PATCH 26/35] Allow Queries.BlobSize to be asked for the size from the start address The idea is to ignore address offsets and thus getting bot from Queries.BlobSize --- src/analyses/base.ml | 14 ++++++++++++-- src/domains/queries.ml | 10 ++++++---- 2 files changed, 18 insertions(+), 6 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 824fde18d9..b50fed9c50 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1256,16 +1256,26 @@ struct end | Q.EvalValue e -> eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e - | Q.BlobSize e -> begin + | Q.BlobSize (e, from_base_addr) -> begin let p = eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in (* ignore @@ printf "BlobSize %a MayPointTo %a\n" d_plainexp e VD.pretty p; *) match p with | Address a -> let s = addrToLvalSet a in (* If there's a non-heap var or an offset in the lval set, we answer with bottom *) - if ValueDomainQueries.LS.exists (fun (v, o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || o <> `NoOffset) s then + (* If we're asking for the BlobSize from the base address, then don't check for offsets => we want to avoid getting bot *) + if ValueDomainQueries.LS.exists (fun (v, o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || (if not from_base_addr then o <> `NoOffset else false)) s then Queries.Result.bot q else ( + (* If we need the BlobSize from the base address, then remove any offsets *) + let a = + if from_base_addr then + ValueDomainQueries.LS.elements s + |> List.map (fun (v, _) -> Addr.of_var v) + |> AD.of_list + else + a + in let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a None in (* ignore @@ printf "BlobSize %a = %a\n" d_plainexp e VD.pretty r; *) (match r with diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 214fcf1384..1735a047ea 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -91,7 +91,9 @@ type _ t = | EvalStr: exp -> SD.t t | EvalLength: exp -> ID.t t (* length of an array or string *) | EvalValue: exp -> VD.t t - | BlobSize: exp -> ID.t t (* size of a dynamically allocated `Blob pointed to by exp *) + | BlobSize: exp * bool -> ID.t t + (* Size of a dynamically allocated `Blob pointed to by exp. *) + (* If the second component is set to true, then address offsets are discarded and the size of the `Blob is asked for the base address. *) | CondVars: exp -> ES.t t | PartAccess: access -> Obj.t t (** Only queried by access and deadlock analysis. [Obj.t] represents [MCPAccess.A.t], needed to break dependency cycle. *) | IterPrevVars: iterprevvar -> Unit.t t @@ -334,7 +336,7 @@ struct | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2 | Any (EvalMutexAttr e1), Any (EvalMutexAttr e2) -> CilType.Exp.compare e1 e2 | Any (EvalValue e1), Any (EvalValue e2) -> CilType.Exp.compare e1 e2 - | Any (BlobSize e1), Any (BlobSize e2) -> CilType.Exp.compare e1 e2 + | Any (BlobSize (e1, _)), Any (BlobSize (e2, _)) -> CilType.Exp.compare e1 e2 | Any (CondVars e1), Any (CondVars e2) -> CilType.Exp.compare e1 e2 | Any (PartAccess p1), Any (PartAccess p2) -> compare_access p1 p2 | Any (IterPrevVars ip1), Any (IterPrevVars ip2) -> compare_iterprevvar ip1 ip2 @@ -379,7 +381,7 @@ struct | Any (EvalLength e) -> CilType.Exp.hash e | Any (EvalMutexAttr e) -> CilType.Exp.hash e | Any (EvalValue e) -> CilType.Exp.hash e - | Any (BlobSize e) -> CilType.Exp.hash e + | Any (BlobSize (e, from_base_addr)) -> CilType.Exp.hash e + Hashtbl.hash from_base_addr | Any (CondVars e) -> CilType.Exp.hash e | Any (PartAccess p) -> hash_access p | Any (IterPrevVars i) -> 0 @@ -427,7 +429,7 @@ struct | Any (EvalStr e) -> Pretty.dprintf "EvalStr %a" CilType.Exp.pretty e | Any (EvalLength e) -> Pretty.dprintf "EvalLength %a" CilType.Exp.pretty e | Any (EvalValue e) -> Pretty.dprintf "EvalValue %a" CilType.Exp.pretty e - | Any (BlobSize e) -> Pretty.dprintf "BlobSize %a" CilType.Exp.pretty e + | Any (BlobSize (e, from_base_addr)) -> Pretty.dprintf "BlobSize %a (from base address: %b)" CilType.Exp.pretty e from_base_addr | Any (CondVars e) -> Pretty.dprintf "CondVars %a" CilType.Exp.pretty e | Any (PartAccess p) -> Pretty.dprintf "PartAccess _" | Any (IterPrevVars i) -> Pretty.dprintf "IterPrevVars _" From 7fb671947da29c5f1d6a67b9a1b91d5e8fd3db05 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 31 Aug 2023 16:49:32 +0200 Subject: [PATCH 27/35] Use Queries.BlobSize for getting blob sizes without address offsets --- src/analyses/memOutOfBounds.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 2b4ca3d4c4..e81b097054 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -100,7 +100,8 @@ struct * and thus we always get a warning for an OOB memory access. Should we maybe change Queries.BlobSize again? *) if points_to_heap_only ctx ptr then - ctx.ask (Queries.BlobSize ptr) + (* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *) + ctx.ask (Queries.BlobSize (ptr, true)) else match ctx.ask (Queries.MayPointTo ptr) with | a when not (Queries.LS.is_top a) -> From 0e126df6b638d755af1e36ba4b50bc1b67935eb9 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 31 Aug 2023 16:51:29 +0200 Subject: [PATCH 28/35] Clean up unnecessary comments --- src/analyses/memOutOfBounds.ml | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index e81b097054..acf6eb7660 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -90,15 +90,6 @@ struct | _ -> false let get_size_of_ptr_target ctx ptr = - (* Call Queries.BlobSize only if ptr points solely to the heap. Otherwise we get bot *) - (* TODO: - * If the ptr's address has been offset, then Queries.BlobSize will answer with bot. For example: - char *ptr = malloc(10 * sizeof(char)); - ptr++; - printf("%s", *ptr); // => Issues a WARN even though it shouldn't - * However, in this case we're too imprecise, since we're always comparing something with bot - * and thus we always get a warning for an OOB memory access. Should we maybe change Queries.BlobSize again? - *) if points_to_heap_only ctx ptr then (* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *) ctx.ask (Queries.BlobSize (ptr, true)) From 293d3e7d02bd4a8a52db31611bb4f0ebe4e1ffc5 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 31 Aug 2023 17:22:20 +0200 Subject: [PATCH 29/35] Add check for implicit pointer dereferences in special functions Also remove a resolved TODO comment --- src/analyses/memOutOfBounds.ml | 44 +++++++++++++++++++++------------- 1 file changed, 27 insertions(+), 17 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index acf6eb7660..0e93adb295 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -174,7 +174,6 @@ struct (* Offset should be the same for all elements in the points-to set. Hence, we can just pick one element and obtain its offset - TODO: Does this make sense? *) let (_, o) = VDQ.LS.choose a in let rec to_int_dom_offs = function @@ -198,19 +197,22 @@ struct M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () - and check_lval_for_oob_access ctx lval = + and check_lval_for_oob_access ctx ?(is_implicitly_derefed = false) lval = if not @@ lval_contains_a_ptr lval then () else - match lval with - | Var _, _ -> () - | Mem e, _ -> + (* 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 ctx (Lval lval) + | (Mem e, _), _ -> begin match e with | Lval (Var v, _) as lval_exp -> check_no_binop_deref ctx lval_exp | BinOp (binop, e1, e2, t) when binop = PlusPI || binop = MinusPI || binop = IndexPI -> check_binop_exp ctx binop e1 e2 t; - check_exp_for_oob_access ctx e1; - check_exp_for_oob_access ctx e2 - | _ -> check_exp_for_oob_access ctx e + check_exp_for_oob_access ctx ~is_implicitly_derefed e1; + check_exp_for_oob_access ctx ~is_implicitly_derefed e2 + | _ -> check_exp_for_oob_access ctx ~is_implicitly_derefed e end and check_no_binop_deref ctx lval_exp = @@ -235,7 +237,7 @@ struct end | _ -> M.error "Expression %a is not a pointer" d_exp lval_exp - and check_exp_for_oob_access ctx exp = + and check_exp_for_oob_access ctx ?(is_implicitly_derefed = false) exp = match exp with | Const _ | SizeOf _ @@ -247,17 +249,17 @@ struct | SizeOfE e | AlignOfE e | UnOp (_, e, _) - | CastE (_, e) -> check_exp_for_oob_access ctx e + | CastE (_, e) -> check_exp_for_oob_access ctx ~is_implicitly_derefed e | BinOp (bop, e1, e2, t) -> - check_exp_for_oob_access ctx e1; - check_exp_for_oob_access ctx e2 + check_exp_for_oob_access ctx ~is_implicitly_derefed e1; + check_exp_for_oob_access ctx ~is_implicitly_derefed e2 | Question (e1, e2, e3, _) -> - check_exp_for_oob_access ctx e1; - check_exp_for_oob_access ctx e2; - check_exp_for_oob_access ctx e3 + check_exp_for_oob_access ctx ~is_implicitly_derefed e1; + check_exp_for_oob_access ctx ~is_implicitly_derefed e2; + check_exp_for_oob_access ctx ~is_implicitly_derefed e3 | Lval lval | StartOf lval - | AddrOf lval -> check_lval_for_oob_access ctx lval + | AddrOf lval -> check_lval_for_oob_access ctx ~is_implicitly_derefed lval and check_binop_exp ctx binop e1 e2 t = let binopexp = BinOp (binop, e1, e2, t) in @@ -314,8 +316,16 @@ struct ctx.local let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = + let desc = LibraryFunctions.find f in + let is_arg_implicitly_derefed 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 ctx x) lval; - List.iter (fun arg -> check_exp_for_oob_access ctx arg) arglist; + List.iter (fun arg -> check_exp_for_oob_access ctx ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) arg) arglist; ctx.local let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = From e4b349a61545e00c53f2c4267a496f959b2e83fa Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 31 Aug 2023 17:23:03 +0200 Subject: [PATCH 30/35] Add a test case with implicit dereferences --- .../77-mem-oob/05-oob-implicit-deref.c | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 tests/regression/77-mem-oob/05-oob-implicit-deref.c diff --git a/tests/regression/77-mem-oob/05-oob-implicit-deref.c b/tests/regression/77-mem-oob/05-oob-implicit-deref.c new file mode 100644 index 0000000000..088493d3b9 --- /dev/null +++ b/tests/regression/77-mem-oob/05-oob-implicit-deref.c @@ -0,0 +1,19 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include +#include +#include + +int main(int argc, char const *argv[]) { + int *ptr = malloc(4 * sizeof(int)); + + // Both lines below are considered derefs => no need to warn, since ptr is pointing within its bounds + memset(ptr, 0, 4 * sizeof(int)); //NOWARN + printf("%p", (void *) ptr); //NOWARN + ptr = ptr + 10; // ptr no longer points within its allocated bounds + + // Each of both lines below should now receive a WARN + memset(ptr, 0, 4 * sizeof(int)); //WARN + printf("%p", (void *) ptr); //WARN + + return 0; +} From 2b4549905c80bbca10d82e04a7d2f21b9978143e Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 6 Sep 2023 12:01:45 +0200 Subject: [PATCH 31/35] Disable Info warnings for test case 77/05 for now Also add a comment explaining why it's a temporary solution --- tests/regression/77-mem-oob/05-oob-implicit-deref.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/tests/regression/77-mem-oob/05-oob-implicit-deref.c b/tests/regression/77-mem-oob/05-oob-implicit-deref.c index 088493d3b9..8bec6a72e0 100644 --- a/tests/regression/77-mem-oob/05-oob-implicit-deref.c +++ b/tests/regression/77-mem-oob/05-oob-implicit-deref.c @@ -1,4 +1,8 @@ -// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info +/* + Note: the "--disable warn.info" above is a temporary workaround, + since the GitHub CI seems to be considering Info messages as violations of NOWARN (cf. https://github.com/goblint/analyzer/issues/1151) +*/ #include #include #include From 924130132a766149cc97745629fd52e08ec6b798 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 6 Sep 2023 12:02:35 +0200 Subject: [PATCH 32/35] Remove TODO comment and add a few other explaining comments --- src/analyses/memOutOfBounds.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 0e93adb295..1738970739 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -1,3 +1,5 @@ +(** An analysis for the detection of out-of-bounds memory accesses ([memOutOfBounds]).*) + open GoblintCil open Analyses open MessageCategory @@ -5,6 +7,12 @@ open MessageCategory module AS = AnalysisState module VDQ = ValueDomainQueries +(* + Note: + * This functionality is implemented as an analysis solely for the sake of maintaining + separation of concerns, as well as for having the ablility to conveniently turn it on or off + * It doesn't track any internal state +*) module Spec = struct include Analyses.IdentitySpec @@ -12,7 +20,6 @@ struct module D = Lattice.Unit module C = D - (* TODO: Check out later for benchmarking *) let context _ _ = () let name () = "memOutOfBounds" From 0bae455057d108b3d2e5f368622384ccdf9f8d44 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 6 Sep 2023 12:07:16 +0200 Subject: [PATCH 33/35] Use a record instead of a tuple for Queries.BlobSize --- src/analyses/base.ml | 2 +- src/analyses/memOutOfBounds.ml | 2 +- src/domains/queries.ml | 10 +++++----- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index f237ca8296..28a5b236a3 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1257,7 +1257,7 @@ struct end | Q.EvalValue e -> eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e - | Q.BlobSize (e, from_base_addr) -> begin + | Q.BlobSize {exp = e; base_address = from_base_addr} -> begin let p = eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in (* ignore @@ printf "BlobSize %a MayPointTo %a\n" d_plainexp e VD.pretty p; *) match p with diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 1738970739..97907e9d6f 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -99,7 +99,7 @@ struct let get_size_of_ptr_target ctx ptr = if points_to_heap_only ctx ptr then (* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *) - ctx.ask (Queries.BlobSize (ptr, true)) + ctx.ask (Queries.BlobSize {exp = ptr; base_address = true}) else match ctx.ask (Queries.MayPointTo ptr) with | a when not (Queries.LS.is_top a) -> diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 1735a047ea..d7de0b1e79 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -91,9 +91,9 @@ type _ t = | EvalStr: exp -> SD.t t | EvalLength: exp -> ID.t t (* length of an array or string *) | EvalValue: exp -> VD.t t - | BlobSize: exp * bool -> ID.t t + | BlobSize: {exp: Cil.exp; base_address: bool} -> ID.t t (* Size of a dynamically allocated `Blob pointed to by exp. *) - (* If the second component is set to true, then address offsets are discarded and the size of the `Blob is asked for the base address. *) + (* If the record's second field is set to true, then address offsets are discarded and the size of the `Blob is asked for the base address. *) | CondVars: exp -> ES.t t | PartAccess: access -> Obj.t t (** Only queried by access and deadlock analysis. [Obj.t] represents [MCPAccess.A.t], needed to break dependency cycle. *) | IterPrevVars: iterprevvar -> Unit.t t @@ -336,7 +336,7 @@ struct | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2 | Any (EvalMutexAttr e1), Any (EvalMutexAttr e2) -> CilType.Exp.compare e1 e2 | Any (EvalValue e1), Any (EvalValue e2) -> CilType.Exp.compare e1 e2 - | Any (BlobSize (e1, _)), Any (BlobSize (e2, _)) -> CilType.Exp.compare e1 e2 + | Any (BlobSize {exp = e1; _}), Any (BlobSize {exp = e2; _}) -> CilType.Exp.compare e1 e2 | Any (CondVars e1), Any (CondVars e2) -> CilType.Exp.compare e1 e2 | Any (PartAccess p1), Any (PartAccess p2) -> compare_access p1 p2 | Any (IterPrevVars ip1), Any (IterPrevVars ip2) -> compare_iterprevvar ip1 ip2 @@ -381,7 +381,7 @@ struct | Any (EvalLength e) -> CilType.Exp.hash e | Any (EvalMutexAttr e) -> CilType.Exp.hash e | Any (EvalValue e) -> CilType.Exp.hash e - | Any (BlobSize (e, from_base_addr)) -> CilType.Exp.hash e + Hashtbl.hash from_base_addr + | Any (BlobSize {exp = e; base_address = b}) -> CilType.Exp.hash e + Hashtbl.hash b | Any (CondVars e) -> CilType.Exp.hash e | Any (PartAccess p) -> hash_access p | Any (IterPrevVars i) -> 0 @@ -429,7 +429,7 @@ struct | Any (EvalStr e) -> Pretty.dprintf "EvalStr %a" CilType.Exp.pretty e | Any (EvalLength e) -> Pretty.dprintf "EvalLength %a" CilType.Exp.pretty e | Any (EvalValue e) -> Pretty.dprintf "EvalValue %a" CilType.Exp.pretty e - | Any (BlobSize (e, from_base_addr)) -> Pretty.dprintf "BlobSize %a (from base address: %b)" CilType.Exp.pretty e from_base_addr + | Any (BlobSize {exp = e; base_address = b}) -> Pretty.dprintf "BlobSize %a (base_address: %b)" CilType.Exp.pretty e b | Any (CondVars e) -> Pretty.dprintf "CondVars %a" CilType.Exp.pretty e | Any (PartAccess p) -> Pretty.dprintf "PartAccess _" | Any (IterPrevVars i) -> Pretty.dprintf "IterPrevVars _" From f06a0f5c7592b750c3ddb471d680b19a9634684c Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Tue, 26 Sep 2023 16:49:10 +0200 Subject: [PATCH 34/35] Add check for bot and top address offsets --- src/analyses/memOutOfBounds.ml | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 97907e9d6f..4b39594bb8 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -177,12 +177,7 @@ struct | true -> M.warn "Pointer %a has an empty points-to-set" d_exp ptr; IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () - | false -> - (* - Offset should be the same for all elements in the points-to set. - Hence, we can just pick one element and obtain its offset - *) - let (_, o) = VDQ.LS.choose a in + | false -> let rec to_int_dom_offs = function | `NoOffset -> `NoOffset | `Field (f, o) -> `Field (f, to_int_dom_offs o) @@ -194,6 +189,20 @@ struct in `Index (exp_as_int_dom, to_int_dom_offs o) in + let () = + if VDQ.LS.exists (fun (_, o) -> IntDomain.IntDomTuple.is_bot @@ offs_to_idx t (to_int_dom_offs o)) a then ( + (* TODO: Uncomment once staging-memsafety branch changes are applied *) + (* set_mem_safety_flag InvalidDeref; *) + M.warn "Pointer %a has a bot address offset. An invalid memory access may occur" d_exp ptr + ) else if VDQ.LS.exists (fun (_, o) -> IntDomain.IntDomTuple.is_top @@ offs_to_idx t (to_int_dom_offs o)) a then ( + (* TODO: Uncomment once staging-memsafety branch changes are applied *) + (* set_mem_safety_flag InvalidDeref; *) + M.warn "Pointer %a has a top address offset. An invalid memory access may occur" d_exp ptr + ) + in + (* Offset should be the same for all elements in the points-to set *) + (* Hence, we can just pick one element and obtain its offset *) + let (_, o) = VDQ.LS.choose a in offs_to_idx t (to_int_dom_offs o) end | None -> From a2bea7b3081b9c7ebe92d91dc2cf21283ece3ee8 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 27 Sep 2023 14:45:21 +0200 Subject: [PATCH 35/35] Fix issues after merge with master --- src/analyses/base.ml | 7 ++- src/analyses/memOutOfBounds.ml | 86 +++++++++++++++++----------------- 2 files changed, 47 insertions(+), 46 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c1047f9c6a..8b76a1cc03 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1261,10 +1261,9 @@ struct else ( (* If we need the BlobSize from the base address, then remove any offsets *) let a = - if from_base_addr then - ValueDomainQueries.LS.elements s - |> List.map (fun (v, _) -> Addr.of_var v) - |> AD.of_list + if from_base_addr then AD.map (function + | Addr (v, o) -> Addr (v, `NoOffset) + | addr -> addr) a else a in diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 4b39594bb8..94c16e9c94 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -92,8 +92,11 @@ struct let points_to_heap_only ctx ptr = match ctx.ask (Queries.MayPointTo ptr) with - | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) -> - Queries.LS.for_all (fun (v, _) -> ctx.ask (Queries.IsHeapVar v)) a + | a when not (Queries.AD.is_top a)-> + Queries.AD.for_all (function + | Addr (v, o) -> ctx.ask (Queries.IsHeapVar v) + | _ -> false + ) a | _ -> false let get_size_of_ptr_target ctx ptr = @@ -102,21 +105,25 @@ struct ctx.ask (Queries.BlobSize {exp = ptr; base_address = true}) else match ctx.ask (Queries.MayPointTo ptr) with - | a when not (Queries.LS.is_top a) -> - let pts_list = Queries.LS.elements a in - let pts_elems_to_sizes (v, _) = - begin match v.vtype with - | TArray (item_typ, _, _) -> - let item_typ_size_in_bytes = (bitsSizeOf item_typ) / 8 in - let item_typ_size_in_bytes = intdom_of_int item_typ_size_in_bytes in - begin match ctx.ask (Queries.EvalLength ptr) with - | `Lifted arr_len -> `Lifted (IntDomain.IntDomTuple.mul item_typ_size_in_bytes arr_len) - | `Bot -> VDQ.ID.bot () - | `Top -> VDQ.ID.top () + | a when not (Queries.AD.is_top a) -> + let pts_list = Queries.AD.elements a in + let pts_elems_to_sizes (addr: Queries.AD.elt) = + begin match addr with + | Addr (v, _) -> + begin match v.vtype with + | TArray (item_typ, _, _) -> + let item_typ_size_in_bytes = (bitsSizeOf item_typ) / 8 in + let item_typ_size_in_bytes = intdom_of_int item_typ_size_in_bytes in + begin match ctx.ask (Queries.EvalLength ptr) with + | `Lifted arr_len -> `Lifted (IntDomain.IntDomTuple.mul item_typ_size_in_bytes arr_len) + | `Bot -> VDQ.ID.bot () + | `Top -> VDQ.ID.top () + end + | _ -> + let type_size_in_bytes = (bitsSizeOf v.vtype) / 8 in + `Lifted (intdom_of_int type_size_in_bytes) end - | _ -> - let type_size_in_bytes = (bitsSizeOf v.vtype) / 8 in - `Lifted (intdom_of_int type_size_in_bytes) + | _ -> VDQ.ID.top () end in (* Map each points-to-set element to its size *) @@ -169,41 +176,36 @@ struct let rec get_addr_offs ctx ptr = match ctx.ask (Queries.MayPointTo ptr) with - | a when not (VDQ.LS.is_top a) -> + | 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 | Some t -> - begin match VDQ.LS.is_empty a with + begin match VDQ.AD.is_empty a with | true -> M.warn "Pointer %a has an empty points-to-set" d_exp ptr; IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () | false -> - let rec to_int_dom_offs = function - | `NoOffset -> `NoOffset - | `Field (f, o) -> `Field (f, to_int_dom_offs o) - | `Index (i, o) -> - let exp_as_int_dom = match ctx.ask (Queries.EvalInt i) with - | `Lifted i -> i - | `Bot -> IntDomain.IntDomTuple.bot_of @@ Cilfacade.ptrdiff_ikind () - | `Top -> IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () - in - `Index (exp_as_int_dom, to_int_dom_offs o) - in - let () = - if VDQ.LS.exists (fun (_, o) -> IntDomain.IntDomTuple.is_bot @@ offs_to_idx t (to_int_dom_offs o)) a then ( - (* TODO: Uncomment once staging-memsafety branch changes are applied *) - (* set_mem_safety_flag InvalidDeref; *) - M.warn "Pointer %a has a bot address offset. An invalid memory access may occur" d_exp ptr - ) else if VDQ.LS.exists (fun (_, o) -> IntDomain.IntDomTuple.is_top @@ offs_to_idx t (to_int_dom_offs o)) a then ( - (* TODO: Uncomment once staging-memsafety branch changes are applied *) - (* set_mem_safety_flag InvalidDeref; *) - M.warn "Pointer %a has a top address offset. An invalid memory access may occur" d_exp ptr - ) - in + if VDQ.AD.exists (function + | Addr (_, o) -> IntDomain.IntDomTuple.is_bot @@ offs_to_idx t o + | _ -> false + ) a then ( + (* TODO: Uncomment once staging-memsafety branch changes are applied *) + (* set_mem_safety_flag InvalidDeref; *) + M.warn "Pointer %a has a bot address offset. An invalid memory access may occur" d_exp ptr + ) else if VDQ.AD.exists (function + | Addr (_, o) -> IntDomain.IntDomTuple.is_bot @@ offs_to_idx t o + | _ -> false + ) a then ( + (* TODO: Uncomment once staging-memsafety branch changes are applied *) + (* set_mem_safety_flag InvalidDeref; *) + M.warn "Pointer %a has a top address offset. An invalid memory access may occur" d_exp ptr + ); (* Offset should be the same for all elements in the points-to set *) (* Hence, we can just pick one element and obtain its offset *) - let (_, o) = VDQ.LS.choose a in - offs_to_idx t (to_int_dom_offs o) + begin match VDQ.AD.choose a with + | Addr (_, o) -> offs_to_idx t o + | _ -> IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + end end | None -> M.error "Expression %a doesn't have pointer type" d_exp ptr;