Skip to content

Commit 3bd3da1

Browse files
Copilotmichael-schwarz
Copilot
and
michael-schwarz
authored
Warn when ana.opt.hashcons is disabled but implicitly overridden, fail for Apron (#1921)
* Initial plan * Add warning when hashconsing is force-enabled Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Add test for hashcons warning Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Fix missing semicolon in warning logic Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Final: Complete implementation with warnings Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Move hashcons warning to check_arguments in maingoblint.ml Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Remove tests as they are not needed Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * Remove _codeql_detected_source_root file Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> * 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> * Swap order of Apron and ARG hashcons checks Check Apron first (fail) before ARG (warn) since fail is more severe Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
1 parent 762b284 commit 3bd3da1

File tree

6 files changed

+20
-8
lines changed

6 files changed

+20
-8
lines changed

‎src/analyses/apron/affineEqualityAnalysis.apron.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ let get_spec (): (module MCPSpec) =
4343

4444
let after_config () =
4545
let module Spec = (val get_spec ()) in
46-
MCP.register_analysis (module Spec : MCPSpec);
46+
MCP.register_analysis ~usesApron:true (module Spec : MCPSpec);
4747
GobConfig.set_string "ana.path_sens[+]" (Spec.name ())
4848

4949
let _ =

‎src/analyses/apron/apronAnalysis.apron.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ let get_spec (): (module MCPSpec) =
2323

2424
let after_config () =
2525
let module Spec = (val get_spec ()) in
26-
MCP.register_analysis (module Spec : MCPSpec);
26+
MCP.register_analysis ~usesApron:true (module Spec : MCPSpec);
2727
GobConfig.set_string "ana.path_sens[+]" (Spec.name ())
2828

2929
let _ =

‎src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ let get_spec (): (module MCPSpec) =
2424

2525
let after_config () =
2626
let module Spec = (val get_spec ()) in
27-
MCP.register_analysis (module Spec : MCPSpec);
27+
MCP.register_analysis ~usesApron:true (module Spec : MCPSpec);
2828
GobConfig.set_string "ana.path_sens[+]" (Spec.name ())
2929

3030
let _ =

‎src/analyses/mCPRegistry.ml‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,8 @@ type spec_modules = { name : string
1414
; cont : (module Printable.S)
1515
; var : (module SpecSysVar)
1616
; acc : (module MCPA)
17-
; path : (module DisjointDomain.Representative) }
17+
; path : (module DisjointDomain.Representative)
18+
; usesApron : bool }
1819

1920
let activated : (int * spec_modules) list ref = ref []
2021
let activated_context_sens: (int * spec_modules) list ref = ref []
@@ -24,7 +25,7 @@ let registered_name: (string, int) Hashtbl.t = Hashtbl.create 100
2425

2526
let register_analysis =
2627
let count = ref 0 in
27-
fun ?(dep=[]) (module S:MCPSpec) ->
28+
fun ?(dep=[]) ?(usesApron=false) (module S:MCPSpec) ->
2829
let n = S.name () in
2930
let module P =
3031
struct
@@ -41,6 +42,7 @@ let register_analysis =
4142
; var = (module S.V : SpecSysVar)
4243
; acc = (module S.A : MCPA)
4344
; path = (module P : DisjointDomain.Representative)
45+
; usesApron
4446
}
4547
in
4648
Hashtbl.replace registered !count s;
@@ -51,6 +53,9 @@ let find_spec = Hashtbl.find registered
5153
let find_spec_name n = (find_spec n).name
5254
let find_id = Hashtbl.find registered_name
5355

56+
let any_activated_uses_apron () =
57+
List.exists (fun (n, _) -> (find_spec n).usesApron) !activated
58+
5459
module type DomainListPrintableSpec =
5560
sig
5661
val assoc_dom : int -> (module Printable.S)

‎src/framework/control.ml‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
2020
GobConfig.building_spec := true;
2121
let arg_enabled = get_bool "exp.arg.enabled" in
2222
let termination_enabled = List.mem "termination" (get_string_list "ana.activated") in (* check if loop termination analysis is enabled*)
23+
let hashcons_enabled = get_bool "ana.opt.hashcons" in
2324
(* apply functor F on module X if opt is true *)
2425
let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
2526
let module S1 =
@@ -29,16 +30,16 @@ let spec_module: (module Spec) Lazy.t = lazy (
2930
|> lift true (module WidenContextLifterSide) (* option checked in functor *)
3031
|> lift (get_int "ana.widen.delay.local" > 0) (module WideningDelay.DLifter)
3132
(* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
32-
|> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
33+
|> lift (hashcons_enabled || arg_enabled) (module HashconsContextLifter)
3334
|> lift (get_bool "ana.opt.hashcached") (module HashCachedContextLifter)
3435
|> lift arg_enabled (module HashconsLifter)
3536
|> lift arg_enabled (module ArgConstraints.PathSensitive3)
3637
|> lift (not arg_enabled) (module PathSensitive2)
3738
|> lift (get_bool "ana.dead-code.branches") (module DeadBranchLifter)
3839
|> lift true (module DeadCodeLifter)
3940
|> lift (get_bool "dbg.slice.on") (module LevelSliceLifter)
40-
|> lift (get_bool "ana.opt.equal" && not (get_bool "ana.opt.hashcons")) (module OptEqual)
41-
|> lift (get_bool "ana.opt.hashcons") (module HashconsLifter)
41+
|> lift (get_bool "ana.opt.equal" && not hashcons_enabled) (module OptEqual)
42+
|> lift hashcons_enabled (module HashconsLifter)
4243
(* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens.
4344
Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *)
4445
|> lift (get_bool "ana.widen.tokens") (module WideningTokenLifter.Lifter)

‎src/maingoblint.ml‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -136,6 +136,12 @@ let check_arguments () =
136136
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");
137137
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.");
138138
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.");
139+
if not (get_bool "ana.opt.hashcons") then (
140+
if MCPRegistry.any_activated_uses_apron () then
141+
fail "Disabling ana.opt.hashcons is not supported when using Apron domains";
142+
if get_bool "exp.arg.enabled" then
143+
warn "Disabling ana.opt.hashcons has no effect because hashconsing is implicitly enabled by exp.arg.enabled";
144+
);
139145
if List.mem "remove_dead_code" @@ get_string_list "trans.activated" then (
140146
(* 'assert' transform happens before 'remove_dead_code' transform *)
141147
ignore @@ List.fold_left

0 commit comments

Comments
 (0)