diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index 5c19d65cf4..59d3827700 100644 --- a/src/analyses/accessAnalysis.ml +++ b/src/analyses/accessAnalysis.ml @@ -29,7 +29,7 @@ struct let init _ = collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed"; let activated = get_string_list "ana.activated" in - emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated + emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) = if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach; diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 9f080dfb62..ae0cf3b209 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -85,87 +85,6 @@ struct M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom" end - (** - [is_free] indicates that the lval is passed to free, i.e., whether we consider a call [free(lval)]. - *) - let rec warn_lval_might_contain_freed ?(is_implicitly_derefed = false) ?(is_free = false) (transfer_fn_name:string) man (lval:lval) = - match is_implicitly_derefed, is_free, lval with - (* If we're not checking for a double-free and there's no deref happening, then there's no need to check for an invalid deref or an invalid free *) - | false, false, (Var _, NoOffset) -> () - | _ -> - let rec offset_might_contain_freed offset = - match offset with - | NoOffset -> () - | Field (f, o) -> - offset_might_contain_freed o - | Index (e, o) -> - warn_exp_might_contain_freed transfer_fn_name man e; - offset_might_contain_freed o - in - let (lval_host, o) = lval in - offset_might_contain_freed o; (* Check the lval's offset *) - - let freed_heap_vars = snd man.local in - let undefined_behavior = if is_free then Undefined DoubleFree else Undefined UseAfterFree in - let cwe_number = if is_free then 415 else 416 in - - let check_adress adresses = - let warn_for_heap_var v = - if HeapVars.mem v freed_heap_vars then begin - if is_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name - end - in - let pointed_to_heap_vars = - Queries.AD.fold (fun addr vars -> - match addr with - | Queries.AD.Addr.Addr (v,_) when man.ask (Queries.IsAllocVar v) -> v :: vars - | _ -> vars - ) adresses [] - in - if not (Queries.AD.is_top adresses) then begin - (* Warn for all heap vars that the lval possibly points to *) - List.iter warn_for_heap_var pointed_to_heap_vars; - (* Warn for a potential multi-threaded UAF for all heap vars that the lval possibly points to *) - List.iter (fun heap_var -> warn_for_multi_threaded_access man ~is_free heap_var undefined_behavior cwe_number) pointed_to_heap_vars - end - in - let addresses = man.ask (Queries.MayPointTo (Lval lval)) in - check_adress addresses; - match lval_host with - | Var _ -> () - | Mem exp -> - (* We have (\*x).o', so we check recursively whether x has been freed. *) - warn_exp_might_contain_freed ~is_implicitly_derefed:true ~is_free:false transfer_fn_name man exp - - (** [is_free] indicates that the exp is passed to free, i.e., we consider a call [free(exp)]*) - and warn_exp_might_contain_freed ?(is_implicitly_derefed = false) ?(is_free = false) (transfer_fn_name:string) man (exp:exp) = - match exp with - (* Base recursion cases *) - | Const _ - | SizeOf _ - | SizeOfStr _ - | AlignOf _ - | AddrOfLabel _ -> () - (* Non-base cases *) - | Real e - | Imag e - | SizeOfE e - | AlignOfE e - | UnOp (_, e, _) - | CastE (_, e) -> warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e - | BinOp (_, e1, e2, _) -> - warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e1; - warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e2 - | Question (e1, e2, e3, _) -> - warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e1; - warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e2; - warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e3 - (* Lval cases (need [warn_lval_might_contain_freed] for them) *) - | Lval lval - | StartOf lval - | AddrOf lval -> warn_lval_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man lval - let side_effect_mem_free man freed_heap_vars threadid joined_threads = let side_effect_globals_to_heap_var heap_var = let current_globals = man.global heap_var in @@ -178,21 +97,16 @@ struct (* TRANSFER FUNCTIONS *) let assign man (lval:lval) (rval:exp) : D.t = - warn_lval_might_contain_freed "assign" man lval; - warn_exp_might_contain_freed "assign" man rval; man.local let branch man (exp:exp) (tv:bool) : D.t = - warn_exp_might_contain_freed "branch" man exp; man.local let return man (exp:exp option) (f:fundec) : D.t = - Option.iter (fun x -> warn_exp_might_contain_freed "return" man x) exp; man.local let enter man (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = let caller_state = man.local in - List.iter (fun arg -> warn_exp_might_contain_freed "enter" man arg) args; (* TODO: The 2nd component of the callee state needs to contain only the heap vars from the caller state which are reachable from: *) (* * Global program variables *) (* * The callee arguments *) @@ -208,21 +122,11 @@ struct (caller_stack_state, HeapVars.join caller_heap_state callee_combined_state) let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t = - Option.iter (fun x -> warn_lval_might_contain_freed "enter" man x) lval; man.local let special man (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = let state = man.local in 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 -> warn_lval_might_contain_freed ("special: " ^ f.vname) man x) lval; - List.iter (fun arg -> warn_exp_might_contain_freed ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) ~is_free:(match desc.special arglist with Free _ -> true | _ -> false) ("special: " ^ f.vname) man arg) arglist; match desc.special arglist with | Free ptr -> begin match man.ask (Queries.MayPointTo ptr) with @@ -251,6 +155,39 @@ struct let startstate v = D.bot () let exitstate v = D.top () + let event man e oman = + match e with + | Events.Access {exp; ad; kind; reach} -> + (* must use original (pre-assign, etc) man queries *) + let check_adress adresses = + let freed_heap_vars = snd oman.local in + let undefined_behavior = Undefined UseAfterFree in + let cwe_number = 416 in + let warn_for_heap_var v = + if HeapVars.mem v freed_heap_vars then begin + set_mem_safety_flag InvalidDeref; + M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname "event" + end + in + let pointed_to_heap_vars = + Queries.AD.fold (fun addr vars -> + match addr with + | Queries.AD.Addr.Addr (v,_) when oman.ask (Queries.IsAllocVar v) -> v :: vars + | _ -> vars + ) adresses [] + in + if not (Queries.AD.is_top adresses) then begin + (* Warn for all heap vars that the lval possibly points to *) + List.iter warn_for_heap_var pointed_to_heap_vars; + (* Warn for a potential multi-threaded UAF for all heap vars that the lval possibly points to *) + List.iter (fun heap_var -> warn_for_multi_threaded_access oman ~is_free:false heap_var undefined_behavior cwe_number) pointed_to_heap_vars + end + in + check_adress ad; + man.local + | _ -> + man.local + end let _ =