Warn when ana.opt.hashcons is disabled but implicitly overridden, fail for Apron

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/framework/control.ml

@@ -20,6 +20,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
   GobConfig.building_spec := true;
   let arg_enabled = get_bool "exp.arg.enabled" in
   let termination_enabled = List.mem "termination" (get_string_list "ana.activated") in (* check if loop termination analysis is enabled*)
+  let hashcons_enabled = get_bool "ana.opt.hashcons" in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
   let module S1 =
@@ -29,16 +30,16 @@ let spec_module: (module Spec) Lazy.t = lazy (
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
       |> lift (get_int "ana.widen.delay.local" > 0) (module WideningDelay.DLifter)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
-      |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
+      |> lift (hashcons_enabled || arg_enabled) (module HashconsContextLifter)
       |> lift (get_bool "ana.opt.hashcached") (module HashCachedContextLifter)
       |> lift arg_enabled (module HashconsLifter)
       |> lift arg_enabled (module ArgConstraints.PathSensitive3)
       |> lift (not arg_enabled) (module PathSensitive2)
       |> lift (get_bool "ana.dead-code.branches") (module DeadBranchLifter)
       |> lift true (module DeadCodeLifter)
       |> lift (get_bool "dbg.slice.on") (module LevelSliceLifter)
-      |> lift (get_bool "ana.opt.equal" && not (get_bool "ana.opt.hashcons")) (module OptEqual)
-      |> lift (get_bool "ana.opt.hashcons") (module HashconsLifter)
+      |> lift (get_bool "ana.opt.equal" && not hashcons_enabled) (module OptEqual)
+      |> lift hashcons_enabled (module HashconsLifter)
       (* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens.
          Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *)
       |> lift (get_bool "ana.widen.tokens") (module WideningTokenLifter.Lifter)

src/maingoblint.ml

@@ -136,6 +136,12 @@ let check_arguments () =
   if get_bool "ana.autotune.enabled" && get_bool "incremental.load" then (set_bool "ana.autotune.enabled" false; warn "ana.autotune.enabled implicitly disabled by incremental.load");
   if get_bool "exp.basic-blocks" && not (get_bool "justcil") && List.mem "assert" @@ get_string_list "trans.activated" then (set_bool "exp.basic-blocks" false; warn "The option exp.basic-blocks implicitly disabled by activating the \"assert\" transformation.");
   if (not @@ get_bool "witness.invariant.all-locals") && (not @@ get_bool "cil.addNestedScopeAttr") then (set_bool "cil.addNestedScopeAttr" true; warn "Disabling witness.invariant.all-locals implicitly enables cil.addNestedScopeAttr.");
+  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 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 *)
     ignore @@ List.fold_left