Skip to content

Commit

Permalink
Merge pull request #1201 from mrstanb/svcomp-memsafety-benchmarks
Browse files Browse the repository at this point in the history 
SV-COMP "Memory Safety" benchmark additions
  • Loading branch information
@michael-schwarz
michael-schwarz authored Oct 14, 2023
2 parents 7ebf97e + 910a11f commit ca6fcba
Show file tree
Hide file tree
Showing 57 changed files with 688 additions and 141 deletions.
117 changes: 105 additions & 12 deletions src/analyses/base.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1043,10 +1043,24 @@ struct
| Mem n, ofs -> begin
match (eval_rv a gs st n) with
| Address adr ->
(if AD.is_null adr
then M.error ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "Must dereference NULL pointer"
else if AD.may_be_null adr
then M.warn ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "May dereference NULL pointer");
(
if AD.is_null adr then (
AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
M.error ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "Must dereference NULL pointer"
)
else if AD.may_be_null adr then (
AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
M.warn ~category:M.Category.Behavior.Undefined.nullpointer_dereference ~tags:[CWE 476] "May dereference NULL pointer"
);
(* Warn if any of the addresses contains a non-local and non-global variable *)
if AD.exists (function
| AD.Addr.Addr (v, _) -> not (CPA.mem v st.cpa) && not (is_global a v)
| _ -> false
) adr then (
AnalysisStateUtil.set_mem_safety_flag InvalidDeref;
M.warn "lval %a points to a non-local variable. Invalid pointer dereference may occur" d_lval lval
)
);
AD.map (add_offset_varinfo (convert_offset a gs st ofs)) adr
| _ ->
M.debug ~category:Analyzer "Failed evaluating %a to lvalue" d_lval lval;
Expand Down Expand Up @@ -2023,14 +2037,78 @@ struct
in
match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local ptr with
| Address a ->
if AD.is_top a then
if AD.is_top a then (
AnalysisStateUtil.set_mem_safety_flag InvalidFree;
M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potentially invalid memory deallocation may occur" d_exp ptr special_fn.vname
else if has_non_heap_var a then
) else if has_non_heap_var a then (
AnalysisStateUtil.set_mem_safety_flag InvalidFree;
M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Free of non-dynamically allocated memory in function %s for pointer %a" special_fn.vname d_exp ptr
else if has_non_zero_offset a then
) else if has_non_zero_offset a then (
AnalysisStateUtil.set_mem_safety_flag InvalidFree;
M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer in function %s for pointer %a" special_fn.vname d_exp ptr
| _ -> M.warn ~category:MessageCategory.Analyzer "Pointer %a in function %s doesn't evaluate to a valid address." d_exp ptr special_fn.vname
)
| _ ->
AnalysisStateUtil.set_mem_safety_flag InvalidFree;
M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Pointer %a in function %s doesn't evaluate to a valid address. Invalid memory deallocation may occur" d_exp ptr special_fn.vname

let points_to_heap_only ctx ptr =
match ctx.ask (Queries.MayPointTo ptr) with
| a when not (Queries.AD.is_top a)->
Queries.AD.for_all (function
| Addr (v, _) -> ctx.ask (Queries.IsHeapVar v)
| _ -> false
) a
| _ -> false

let get_size_of_ptr_target ctx ptr =
let intdom_of_int x =
ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x)
in
let size_of_type_in_bytes typ =
let typ_size_in_bytes = (bitsSizeOf typ) / 8 in
intdom_of_int typ_size_in_bytes
in
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 {exp = ptr; base_address = true})
else
match ctx.ask (Queries.MayPointTo ptr) with
| 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 = size_of_type_in_bytes item_typ in
begin match ctx.ask (Queries.EvalLength ptr) with
| `Lifted arr_len ->
let arr_len_casted = ID.cast_to (Cilfacade.ptrdiff_ikind ()) arr_len in
begin
try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted)
with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
end
| `Bot -> `Bot
| `Top -> `Top
end
| _ ->
let type_size_in_bytes = size_of_type_in_bytes v.vtype in
`Lifted type_size_in_bytes
end
| _ -> `Top
end
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
| [] -> `Bot
| [x] -> x
| x::xs -> List.fold_left ValueDomainQueries.ID.join x xs
end
| _ ->
(M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr;
`Top)

let special ctx (lv:lval option) (f: varinfo) (args: exp list) =
let invalidate_ret_lv st = match lv with
Expand All @@ -2050,13 +2128,28 @@ struct
let st: store = ctx.local in
let gs = ctx.global in
let desc = LF.find f in
let memory_copying dst src =
let memory_copying dst src n =
let dest_size = get_size_of_ptr_target ctx dst in
let n_intdom = Option.map_default (fun exp -> ctx.ask (Queries.EvalInt exp)) `Bot n in
let dest_size_equal_n =
match dest_size, n_intdom with
| `Lifted ds, `Lifted n ->
let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in
let casted_n = ID.cast_to (Cilfacade.ptrdiff_ikind ()) n in
let ds_eq_n =
begin try ID.eq casted_ds casted_n
with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
end
in
Option.default false (ID.to_bool ds_eq_n)
| _ -> false
in
let dest_a, dest_typ = addr_type_of_exp dst in
let src_lval = mkMem ~addr:(Cil.stripCasts src) ~off:NoOffset in
let src_typ = eval_lv (Analyses.ask_of_ctx ctx) gs st src_lval
|> AD.type_of in
(* when src and destination type coincide, take value from the source, otherwise use top *)
let value = if typeSig dest_typ = typeSig src_typ then
let value = if (typeSig dest_typ = typeSig src_typ) && dest_size_equal_n then
let src_cast_lval = mkMem ~addr:(Cilfacade.mkCast ~e:src ~newt:(TPtr (dest_typ, []))) ~off:NoOffset in
eval_rv (Analyses.ask_of_ctx ctx) gs st (Lval src_cast_lval)
else
Expand Down Expand Up @@ -2117,13 +2210,13 @@ struct
let value = VD.zero_init_value dest_typ in
set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
| Memcpy { dest = dst; src; n; }, _ -> (* TODO: use n *)
memory_copying dst src
memory_copying dst src (Some n)
(* strcpy(dest, src); *)
| Strcpy { dest = dst; src; n = None }, _ ->
let dest_a, dest_typ = addr_type_of_exp dst in
(* when dest surely isn't a string literal, try copying src to dest *)
if AD.string_writing_defined dest_a then
memory_copying dst src
memory_copying dst src None
else
(* else return top (after a warning was issued) *)
set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ (VD.top_value (unrollType dest_typ))
Expand Down
16 changes: 13 additions & 3 deletions src/analyses/memLeak.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
open GoblintCil
open Analyses
open MessageCategory
open AnalysisStateUtil

module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)

Expand All @@ -19,15 +20,24 @@ struct

(* HELPER FUNCTIONS *)
let warn_for_multi_threaded ctx =
if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then
if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then (
set_mem_safety_flag InvalidMemTrack;
set_mem_safety_flag InvalidMemcleanup;
M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Program isn't running in single-threaded mode. A memory leak might occur due to multi-threading"
)

let check_for_mem_leak ?(assert_exp_imprecise = false) ?(exp = None) ctx =
let state = ctx.local in
if not @@ D.is_empty state then
match assert_exp_imprecise, exp with
| true, Some exp -> M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty state
| _ -> M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state
| true, Some exp ->
set_mem_safety_flag InvalidMemTrack;
set_mem_safety_flag InvalidMemcleanup;
M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty state
| _ ->
set_mem_safety_flag InvalidMemTrack;
set_mem_safety_flag InvalidMemcleanup;
M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state

(* TRANSFER FUNCTIONS *)
let return ctx (exp:exp option) (f:fundec) : D.t =
Expand Down
Loading

0 comments on commit ca6fcba

Please sign in to comment.