Add no-context attribute and ana.context.no_fun option for per-function context-insensitivity

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/5d5147c1-4b56-47f6-b7ef-01b3c007d358

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>

Author: Copilot

docs/user-guide/annotating.md

@@ -26,6 +26,7 @@ The following string arguments are supported:
 4. `base.non-ptr`/`base.no-non-ptr` to override the `ana.base.context.non-ptr` option.
 5. `relation.context`/`relation.no-context` to override the `ana.relation.context` option.
 6. `widen`/`no-widen` to override the `ana.context.widen` option.
+7. `no-context` to disable context-sensitivity for this function entirely (for all analyses).
 
 ### Apron attributes
 The Apron library can be set to only track variables with the attribute `goblint_apron_track`

src/analyses/mCP.ml

@@ -237,13 +237,22 @@ struct
   and context man fd x =
     let man'' = outer_man "context_computation" man in
     let x = spec_list x in
-    filter_map (fun (n,(module S:MCPSpec),d) ->
-        if Set.is_empty !act_cont_sens || not (Set.mem n !act_cont_sens) then (*n is insensitive*)
-          None
-        else
-          let man' : (S.D.t, S.G.t, S.C.t, S.V.t) man = inner_man "context_computation" man'' n d in
-          Some (n, Obj.repr @@ S.context man' fd (Obj.obj d))
-      ) x
+    (* Check if this function should be analyzed context-insensitively *)
+    let no_ctx =
+      ContextUtil.has_attribute "goblint_context" "no-context" fd.svar.vattr
+      || ContextUtil.has_option "goblint_context" "no-context" fd
+      || List.mem fd.svar.vname (get_string_list "ana.context.no_fun")
+    in
+    if no_ctx then
+      [] (* context-insensitive: return empty context list *)
+    else
+      filter_map (fun (n,(module S:MCPSpec),d) ->
+          if Set.is_empty !act_cont_sens || not (Set.mem n !act_cont_sens) then (*n is insensitive*)
+            None
+          else
+            let man' : (S.D.t, S.G.t, S.C.t, S.V.t) man = inner_man "context_computation" man'' n d in
+            Some (n, Obj.repr @@ S.context man' fd (Obj.obj d))
+        ) x
 
   and branch (man:(D.t, G.t, C.t, V.t) man) (e:exp) (tv:bool) =
     let spawns = ref [] in

src/config/options.schema.json

@@ -1073,6 +1073,13 @@
               "description": "Length of the call string that should be used as context for the call_string and/or call_site analyses. In case the value is zero, the analysis is context-insensitive. For a negative value, an infinite call string is used! For this option to have an effect, one of the analyses in `callstring.ml` must be activated.",
               "type": "integer",
               "default": 2
+            },
+            "no_fun": {
+              "title": "ana.context.no_fun",
+              "description": "List of functions to be analyzed context-insensitively (regardless of other context options).",
+              "type": "array",
+              "items": { "type": "string" },
+              "default": []
             }
           },
           "additionalProperties": false
@@ -1821,7 +1828,7 @@
             "type": "array",
             "items": {
               "type": "string",
-              "enum": ["base.no-non-ptr", "base.non-ptr", "base.no-int", "base.int", "base.no-interval", "base.no-interval_set", "base.no-bitfield", "base.interval", "base.interval_set", "base.bitfield", "relation.no-context", "relation.context", "no-widen", "widen"]
+              "enum": ["base.no-non-ptr", "base.non-ptr", "base.no-int", "base.int", "base.no-interval", "base.no-interval_set", "base.no-bitfield", "base.interval", "base.interval_set", "base.bitfield", "relation.no-context", "relation.context", "no-widen", "widen", "no-context"]
             },
             "default": []
           }

tests/regression/90-context/01-no-context-attribute.c

@@ -0,0 +1,16 @@
+// PARAM: --enable ana.int.interval --disable ana.context.widen
+#include <goblint.h>
+
+int f(int x) __attribute__((goblint_context("no-context"))); // attributes are not permitted in a function definition
+int f(int x) {
+  if (x)
+    return f(x+1);
+  else
+    return x;
+}
+
+int main () {
+  int a = f(1);
+  __goblint_check(!a); // UNKNOWN (intended: context-insensitive due to no-context attribute)
+  return 0;
+}

tests/regression/90-context/02-no-context-option.c

@@ -0,0 +1,15 @@
+// PARAM: --enable ana.int.interval --disable ana.context.widen --set ana.context.no_fun[+] f
+#include <goblint.h>
+
+int f(int x) {
+  if (x)
+    return f(x+1);
+  else
+    return x;
+}
+
+int main () {
+  int a = f(1);
+  __goblint_check(!a); // UNKNOWN (intended: context-insensitive due to ana.context.no_fun option)
+  return 0;
+}

tests/regression/90-context/03-no-context-annotation.c

@@ -0,0 +1,15 @@
+// PARAM: --enable ana.int.interval --disable ana.context.widen --set annotation.goblint_context.f[+] no-context
+#include <goblint.h>
+
+int f(int x) {
+  if (x)
+    return f(x+1);
+  else
+    return x;
+}
+
+int main () {
+  int a = f(1);
+  __goblint_check(!a); // UNKNOWN (intended: context-insensitive due to annotation option)
+  return 0;
+}