Show unknownPtr origin node info in unsound warnings

goblint · Sep 4, 2023 · 29eda25 · 29eda25
1 parent d90fcf2
commit 29eda25
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 1 deletion.
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
@@ -675,6 +675,8 @@ struct
       Priv.lock (Analyses.ask_of_ctx ctx) ctx.global st addr
     | Events.Unlock addr when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
       begin match addr with
+        | UnknownPtr {node = Some node} ->
+          M.info ~category:Unsound "Unknown mutex (origin: %a) unlocked, relation privatization unsound" Node.pretty node; (* TODO: something more sound *)
         | UnknownPtr _ ->
           M.info ~category:Unsound "Unknown mutex unlocked, relation privatization unsound"; (* TODO: something more sound *)
         | _ -> ()

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -2661,6 +2661,8 @@ struct
       Priv.lock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) st addr
     | Events.Unlock addr when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
       begin match addr with
+        | UnknownPtr {node = Some node} ->
+          M.info ~category:Unsound "Unknown mutex (origin: %a) unlocked, base privatization unsound" Node.pretty node; (* TODO: something more sound *)
         | UnknownPtr _ ->
           M.info ~category:Unsound "Unknown mutex unlocked, base privatization unsound"; (* TODO: something more sound *)
         | _ -> ()

diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
@@ -317,7 +317,7 @@ struct
               if is_recovered_to_st && not @@ Mutexes.is_top held_weak then
                 Mutexes.iter (fun addr -> ctx.sideg (V.protected addr) protected) held_weak;
             )
-        | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound."
+        | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound." (* TODO: show origin *)
       in
       let module AD = Queries.AD in
       let has_escaped g = octx.ask (Queries.MayEscape g) in