Skip to content

Split octagon autotuner to separate octagonAnalysis and octagonVars autotuners #1952

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
karoliineh wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Split octagon autotuner to separate octagonAnalysis and octagonVars autotuners #1952

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a737c9d
Split octagon autotuner to separate octagonAnalysis and octagonVars a…
karoliineh Mar 5, 2026
af517a4
Update sv-comp configurations according to new schema
karoliineh Mar 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion conf/svcomp-ghost.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,8 @@
"noRecursiveIntervals",
"enums",
"congruence",
"octagon",
"octagonAnalysis",
"octagonVars",
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
Expand Down
3 changes: 2 additions & 1 deletion conf/svcomp23.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,8 @@
"noRecursiveIntervals",
"enums",
"congruence",
"octagon",
"octagonAnalysis",
"octagonVars",
"wideningThresholds",
"loopUnrollHeuristic"
]
Expand Down
3 changes: 2 additions & 1 deletion conf/svcomp24-validate.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,8 @@
"noRecursiveIntervals",
"enums",
"congruence",
"octagon",
"octagonAnalysis",
"octagonVars",
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
Expand Down
3 changes: 2 additions & 1 deletion conf/svcomp24.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,8 @@
"noRecursiveIntervals",
"enums",
"congruence",
"octagon",
"octagonAnalysis",
"octagonVars",
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
Expand Down
3 changes: 2 additions & 1 deletion conf/svcomp25-validate.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,8 @@
"noRecursiveIntervals",
"enums",
"congruence",
"octagon",
"octagonAnalysis",
"octagonVars",
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
Expand Down
3 changes: 2 additions & 1 deletion conf/svcomp25.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,8 @@
"noRecursiveIntervals",
"enums",
"congruence",
"octagon",
"octagonAnalysis",
"octagonVars",
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
Expand Down
3 changes: 2 additions & 1 deletion conf/svcomp26/level01.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,8 @@
"noRecursiveIntervals",
"enums",
"congruence",
"octagon",
"octagonAnalysis",
"octagonVars",
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
Expand Down
3 changes: 2 additions & 1 deletion conf/svcomp26/level04-validate.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,8 @@
"noRecursiveIntervals",
"enums",
"congruence",
"octagon",
"octagonAnalysis",
"octagonVars",
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
Expand Down
3 changes: 2 additions & 1 deletion conf/svcomp26/level04.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,8 @@
"noRecursiveIntervals",
"enums",
"congruence",
"octagon",
"octagonAnalysis",
"octagonVars",
"wideningThresholds",
"loopUnrollHeuristic",
"memsafetySpecification",
Expand Down
25 changes: 17 additions & 8 deletions src/autoTune.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -423,7 +423,14 @@ let congruenceOption factors file =
activate;
}

let apronOctagonOption factors file =
let activateOctagonAnalysis () =
set_string "ana.apron.domain" "octagon";
set_auto "ana.activated[+]" "apron";
set_bool "ana.apron.threshold_widening" true;
set_string "ana.apron.threshold_widening_constants" "comparisons";
Logs.info "Enabled octagon domain."
Comment on lines +426 to +431
Copy link
Copy Markdown
Member

@sim642 sim642 Mar 12, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This doesn't seem right without the costs thing. It will always enable octagons if octagonAnalysis autotuner is activated.
That's not much of an autotuner if it just unconditionally activates things which could be activated directly.

I think I wasn't aware of this dependency when I opened #1449. Maybe it's actually impossible to separate them then?

Copy link
Copy Markdown
Member Author

@karoliineh karoliineh Mar 12, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So, what I did was to just implement the requirements from the issue:

split the autotuner into two:

  1. octagonAnalysis, which is just in charge of enabling the octagon analysis, but not choosing a subset of the variables.
  2. octagonVars, which is in charge of choosing the variables, i.e. disabling octagon analysis for all other variables (because that's what it's really doing, not enabling for additional variables).

where the main problem was that the option octagon:

implicitly means "disabling octagon analysis for all other variables, even if explicitly enabled by the user".

Due to the separation, the confusing behavior is gone as the option names now better reflect what they actually do.

However, it is true that I did not really consider that the autotuner should actually tune something with each option, which is not the case for octagonAnalysis now.

The reason I separated it the way I did is that the cost calculation depends on the number of selected variables. At first glance, this made it seem like the cost belonged purely to the variable selection step. Because of that, I overlooked the fact that the cost value is later used.

Looking at this again from the perspective of autotuning, I see two possible approaches:

  1. Base the cost on all program variables. The cost calculation for octagonAnalysis could consider all variables present in the program, but I am not sure if we can count these easily with some visitor. I am also not sure if the cost will then ever stay under some threshold that the analysis would even be considered (I haven't looked into how the cost is used).
  2. Actually tune the activation of octagonAnalysis meaningfully Instead of simply enabling it through a portfolio configuration, the tuner could decide whether activating it makes sense based not only on the number of variables but also on their structure, e.g., the presence of patterns that would require relational analyses like y = x + 1;.

It definitely is not impossible to separate them cleanly. The question is whether this change is already worthwhile because it makes the options less confusing, even though one of them does not actually tune anything yet, or whether we should wait and introduce that separation only once we also improve the autotuning of enabling octagon in some way.


let octagonVarsOption factors file =
let locals =
if List.mem "specification" (get_string_list "ana.autotune.activated" ) && get_string "ana.specification" <> "" then
if List.mem Svcomp.Specification.NoOverflow (Svcomp.Specification.of_option ()) then
Expand All @@ -447,13 +454,9 @@ let apronOctagonOption factors file =
let allVars = (selectedGlobals @ selectedLocals) in
let cost = (Batteries.Int.pow (locals + globals) 3) * (factors.instructions / 70) in
let activateVars () =
Logs.debug "Octagon: %d" cost;
Logs.debug "Octagon vars: %d" cost;
set_bool "annotation.goblint_relation_track" true;
set_string "ana.apron.domain" "octagon";
set_auto "ana.activated[+]" "apron";
set_bool "ana.apron.threshold_widening" true;
set_string "ana.apron.threshold_widening_constants" "comparisons";
Logs.info "Enabled octagon domain ONLY for:";
Logs.info "Restricted octagon analysis to following tracked variables:";
Logs.info "%s" @@ String.concat ", " @@ List.map (fun info -> info.vname) allVars;
List.iter (fun info -> info.vattr <- addAttribute (Attr("goblint_relation_track",[])) info.vattr) allVars
in
Expand Down Expand Up @@ -556,10 +559,16 @@ let chooseConfig file =
if isActivated "tmpSpecialAnalysis" then
activateTmpSpecialAnalysis ();

let non_termination_task = not (isTerminationTask ()) in

(* octagonVars implies octagonAnalysis *)
if non_termination_task && (isActivated "octagonAnalysis" || isActivated "octagonVars") then
activateOctagonAnalysis ();

let options = [] in
let options = if isActivated "congruence" then (congruenceOption factors file)::options else options in
(* Termination analysis uses apron in a different configuration. *)
let options = if isActivated "octagon" && not (isTerminationTask ()) then (apronOctagonOption factors file)::options else options in
let options = if non_termination_task && isActivated "octagonVars" then (octagonVarsOption factors file)::options else options in
let options = if isActivated "wideningThresholds" then (wideningOption factors file)::options else options in

List.iter (fun o -> o.activate ()) @@ chooseFromOptions (totalTarget - fileCompplexity) options
Expand Down
6 changes: 4 additions & 2 deletions src/config/options.schema.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -556,7 +556,8 @@
"loopUnrollHeuristic",
"forceLoopUnrollForFewLoops",
"arrayDomain",
"octagon",
"octagonAnalysis",
"octagonVars",
"wideningThresholds",
"memsafetySpecification",
"concurrencySafetySpecification",
Expand All @@ -573,7 +574,8 @@
"enums",
"loopUnrollHeuristic",
"arrayDomain",
"octagon",
"octagonAnalysis",
"octagonVars",
"wideningThresholds",
"memsafetySpecification",
"concurrencySafetySpecification",
Expand Down
2 changes: 1 addition & 1 deletion tests/regression/29-svcomp/35-nla-sqrt.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// SKIP PARAM: --enable ana.sv-comp.functions --enable ana.autotune.enabled --set ana.autotune.activated[+] octagon
// SKIP PARAM: --enable ana.sv-comp.functions --enable ana.autotune.enabled --set ana.autotune.activated[+] octagonVars
Copy link
Copy Markdown
Member

@sim642 sim642 Mar 12, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why just octagonVars? I'd think that octagonAnalysis also needs to be activated.

And perhaps octagonVars isn't even necessary? Depends on what the test was added to test: the activation of the analysis or the selection of the variables.

// Extracted from: nla-digbench-scaling/sqrt1-ll_unwindbound5.c
#include <goblint.h>
extern int __VERIFIER_nondet_int(void);
Expand Down
13 changes: 10 additions & 3 deletions tests/regression/29-svcomp/38-autotune-octagon-fun.t
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,17 @@
Should not annotate functions for octagon.

$ goblint --enable ana.autotune.enabled --set ana.autotune.activated[*] octagon 38-autotune-octagon-fun.c
[Info] Enabled octagon domain ONLY for:
[Info] i, count, tmp, count, i, j, i___0, j___0, k, size, r
$ goblint --enable ana.autotune.enabled --set ana.autotune.activated[*] octagonAnalysis 38-autotune-octagon-fun.c
[Info] Enabled octagon domain.
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 5
dead: 0
total lines: 5

$ goblint --enable ana.autotune.enabled --set ana.autotune.activated[*] octagonVars 38-autotune-octagon-fun.c
[Info] Enabled octagon domain.
Comment on lines +10 to +11
Copy link
Copy Markdown
Member

@sim642 sim642 Mar 12, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So octagonVars also enables octagonAnalysis autotuner implicitly?

I think for #1449 they should be independent.

[Info] Restricted octagon analysis to following tracked variables:
[Info] i, count, tmp, count, i, j, i___0, j___0, k, size, r
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 5
dead: 0
total lines: 5
Loading