diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index a910a35bd5..30e3859c42 100644 --- a/src/analyses/accessAnalysis.ml +++ b/src/analyses/accessAnalysis.ml @@ -178,9 +178,14 @@ struct ctx.local | _, x -> let arg_acc act = - match LF.get_threadsafe_inv_ac x with - | Some fnc -> (fnc act arglist) - | _ -> arglist + match act, LF.get_threadsafe_inv_ac x with + | _, Some fnc -> (fnc act arglist) + | `Read, None -> arglist + | (`Write | `Free), None -> + if get_bool "sem.unknown_function.invalidate.args" then + arglist + else + [] in (* TODO: per-argument reach *) let reach = diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index 68ddc11cb9..8105c0d6bd 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -330,6 +330,7 @@ struct let st' = match LibraryFunctions.get_invalidate_action f.vname with | Some fnc -> st (* nothing to do because only AddrOf arguments may be invalidated *) | None -> + (* nothing to do for args because only AddrOf arguments may be invalidated *) if GobConfig.get_bool "sem.unknown_function.invalidate.globals" then ( let globals = foldGlobals !Cilfacade.current_file (fun acc global -> match global with diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c83e3d9aff..9d7b4da753 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2083,6 +2083,12 @@ struct let special_unknown_invalidate ctx ask gs st f args = (if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (LF.use_special f.vname) then M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname); (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn "Unknown function ptr called"); + let addrs = + if get_bool "sem.unknown_function.invalidate.args" then + args + else + [] + in let addrs = if get_bool "sem.unknown_function.invalidate.globals" then ( M.info ~category:Imprecise "INVALIDATING ALL GLOBALS!"; @@ -2092,10 +2098,10 @@ struct mkAddrOf (Var vi, NoOffset) :: acc (* TODO: what about GVarDecl? *) | _ -> acc - ) args + ) addrs ) else - args + addrs in (* TODO: what about escaped local variables? *) (* invalidate arguments and non-static globals for unknown functions *) diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml index 042281e317..ccf0ffe9d7 100644 --- a/src/analyses/symbLocks.ml +++ b/src/analyses/symbLocks.ml @@ -85,7 +85,7 @@ struct | `Unknown fn when VarEq.safe_fn fn -> Messages.warn "Assume that %s does not change lockset." fn; ctx.local - | `Unknown x -> begin + | `Unknown x -> begin (* TODO: _ ? *) let st = match lval with | Some lv -> invalidate_lval (Analyses.ask_of_ctx ctx) lv ctx.local @@ -94,7 +94,11 @@ struct let write_args = match LF.get_invalidate_action f.vname with | Some fnc -> fnc `Write arglist - | _ -> arglist + | None -> + if GobConfig.get_bool "sem.unknown_function.invalidate.args" then + arglist + else + [] in List.fold_left (fun st e -> invalidate_exp (Analyses.ask_of_ctx ctx) e st) st write_args end diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 280779bbc2..ce93e043dd 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -470,7 +470,11 @@ struct let args = match LF.get_invalidate_action f.vname with | Some fnc -> fnc `Write args - | _ -> args + | None -> + if GobConfig.get_bool "sem.unknown_function.invalidate.args" then + args + else + [] in let es = match lval with diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 64dc572de8..67bf49e3b0 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1058,6 +1058,13 @@ "Unknown function call invalidates all globals", "type": "boolean", "default": true + }, + "args": { + "title": "sem.unknown_function.invalidate.args", + "description": + "Unknown function call invalidates arguments passed to it", + "type": "boolean", + "default": true } }, "additionalProperties": false