Change Apron hashcons check to fail and use usesApron flag

- Add usesApron flag to MCPRegistry.spec_modules
- Add optional ~usesApron parameter to register_analysis (default false)
- Add any_activated_uses_apron() function to check registry
- Mark Apron analyses with ~usesApron:true flag
- Change warning to fail when hashcons disabled with Apron

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

Author: Copilot

src/analyses/apron/affineEqualityAnalysis.apron.ml

@@ -43,7 +43,7 @@ let get_spec (): (module MCPSpec) =
 
 let after_config () =
   let module Spec = (val get_spec ()) in
-  MCP.register_analysis (module Spec : MCPSpec);
+  MCP.register_analysis ~usesApron:true (module Spec : MCPSpec);
   GobConfig.set_string "ana.path_sens[+]"  (Spec.name ())
 
 let _ =

src/analyses/apron/apronAnalysis.apron.ml

@@ -23,7 +23,7 @@ let get_spec (): (module MCPSpec) =
 
 let after_config () =
   let module Spec = (val get_spec ()) in
-  MCP.register_analysis (module Spec : MCPSpec);
+  MCP.register_analysis ~usesApron:true (module Spec : MCPSpec);
   GobConfig.set_string "ana.path_sens[+]"  (Spec.name ())
 
 let _ =

src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml

@@ -24,7 +24,7 @@ let get_spec (): (module MCPSpec) =
 
 let after_config () =
   let module Spec = (val get_spec ()) in
-  MCP.register_analysis (module Spec : MCPSpec);
+  MCP.register_analysis ~usesApron:true (module Spec : MCPSpec);
   GobConfig.set_string "ana.path_sens[+]"  (Spec.name ())
 
 let _ =

src/analyses/mCPRegistry.ml

@@ -14,7 +14,8 @@ type spec_modules = { name : string
                     ; cont : (module Printable.S)
                     ; var  : (module SpecSysVar)
                     ; acc  : (module MCPA)
-                    ; path : (module DisjointDomain.Representative) }
+                    ; path : (module DisjointDomain.Representative)
+                    ; usesApron : bool }
 
 let activated  : (int * spec_modules) list ref = ref []
 let activated_context_sens: (int * spec_modules) list ref = ref []
@@ -24,7 +25,7 @@ let registered_name: (string, int) Hashtbl.t = Hashtbl.create 100
 
 let register_analysis =
   let count = ref 0 in
-  fun ?(dep=[]) (module S:MCPSpec) ->
+  fun ?(dep=[]) ?(usesApron=false) (module S:MCPSpec) ->
     let n = S.name () in
     let module P =
     struct
@@ -41,6 +42,7 @@ let register_analysis =
             ; var  = (module S.V : SpecSysVar)
             ; acc  = (module S.A : MCPA)
             ; path = (module P : DisjointDomain.Representative)
+            ; usesApron
             }
     in
     Hashtbl.replace registered !count s;
@@ -51,6 +53,9 @@ let find_spec = Hashtbl.find registered
 let find_spec_name n = (find_spec n).name
 let find_id = Hashtbl.find registered_name
 
+let any_activated_uses_apron () =
+  List.exists (fun (n, _) -> (find_spec n).usesApron) !activated
+
 module type DomainListPrintableSpec =
 sig
   val assoc_dom : int -> (module Printable.S)

src/maingoblint.ml

@@ -139,8 +139,8 @@ let check_arguments () =
   if not (get_bool "ana.opt.hashcons") then (
     if get_bool "exp.arg.enabled" then
       warn "Disabling ana.opt.hashcons has no effect because hashconsing is implicitly enabled by exp.arg.enabled";
-    if List.mem "apron" (get_string_list "ana.activated") then
-      warn "Disabling ana.opt.hashcons has no effect because hashconsing is implicitly enabled by Apron (ana.activated includes 'apron')";
+    if MCPRegistry.any_activated_uses_apron () then
+      fail "Disabling ana.opt.hashcons is not supported when using Apron domains";
   );
   if List.mem "remove_dead_code" @@ get_string_list "trans.activated" then (
     (* 'assert' transform happens before 'remove_dead_code' transform *)