Add option sem.unknown_function.invalidate.args

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 =

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

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 *)

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

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

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