diff --git a/src/framework/control.ml b/src/framework/control.ml index 9085d313eb..f2bfffde2d 100644 --- a/src/framework/control.ml +++ b/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,7 +30,7 @@ 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) @@ -37,8 +38,8 @@ let spec_module: (module Spec) Lazy.t = lazy ( |> 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) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index ee59c91c01..8cea71f5d0 100644 --- a/src/maingoblint.ml +++ b/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 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 List.mem "remove_dead_code" @@ get_string_list "trans.activated" then ( (* 'assert' transform happens before 'remove_dead_code' transform *) ignore @@ List.fold_left