diff --git a/conf/svcomp-ghost.json b/conf/svcomp-ghost.json index b9c20a7463..334fc75887 100644 --- a/conf/svcomp-ghost.json +++ b/conf/svcomp-ghost.json @@ -86,7 +86,8 @@ "noRecursiveIntervals", "enums", "congruence", - "octagon", + "octagonAnalysis", + "octagonVars", "wideningThresholds", "loopUnrollHeuristic", "memsafetySpecification", diff --git a/conf/svcomp23.json b/conf/svcomp23.json index ef900e763a..88e332b375 100644 --- a/conf/svcomp23.json +++ b/conf/svcomp23.json @@ -68,7 +68,8 @@ "noRecursiveIntervals", "enums", "congruence", - "octagon", + "octagonAnalysis", + "octagonVars", "wideningThresholds", "loopUnrollHeuristic" ] diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json index ff1a7adc8f..15640d7af2 100644 --- a/conf/svcomp24-validate.json +++ b/conf/svcomp24-validate.json @@ -84,7 +84,8 @@ "noRecursiveIntervals", "enums", "congruence", - "octagon", + "octagonAnalysis", + "octagonVars", "wideningThresholds", "loopUnrollHeuristic", "memsafetySpecification", diff --git a/conf/svcomp24.json b/conf/svcomp24.json index dde5407056..c4e0155070 100644 --- a/conf/svcomp24.json +++ b/conf/svcomp24.json @@ -83,7 +83,8 @@ "noRecursiveIntervals", "enums", "congruence", - "octagon", + "octagonAnalysis", + "octagonVars", "wideningThresholds", "loopUnrollHeuristic", "memsafetySpecification", diff --git a/conf/svcomp25-validate.json b/conf/svcomp25-validate.json index 0d414ef439..a1262cf7a4 100644 --- a/conf/svcomp25-validate.json +++ b/conf/svcomp25-validate.json @@ -64,7 +64,8 @@ "noRecursiveIntervals", "enums", "congruence", - "octagon", + "octagonAnalysis", + "octagonVars", "wideningThresholds", "loopUnrollHeuristic", "memsafetySpecification", diff --git a/conf/svcomp25.json b/conf/svcomp25.json index bf1e545e2d..75dd679ba8 100644 --- a/conf/svcomp25.json +++ b/conf/svcomp25.json @@ -63,7 +63,8 @@ "noRecursiveIntervals", "enums", "congruence", - "octagon", + "octagonAnalysis", + "octagonVars", "wideningThresholds", "loopUnrollHeuristic", "memsafetySpecification", diff --git a/conf/svcomp26/level01.json b/conf/svcomp26/level01.json index ead6765999..5e0c42adfc 100644 --- a/conf/svcomp26/level01.json +++ b/conf/svcomp26/level01.json @@ -55,7 +55,8 @@ "noRecursiveIntervals", "enums", "congruence", - "octagon", + "octagonAnalysis", + "octagonVars", "wideningThresholds", "loopUnrollHeuristic", "memsafetySpecification", diff --git a/conf/svcomp26/level04-validate.json b/conf/svcomp26/level04-validate.json index 394f33c4f4..7be2184227 100644 --- a/conf/svcomp26/level04-validate.json +++ b/conf/svcomp26/level04-validate.json @@ -60,7 +60,8 @@ "noRecursiveIntervals", "enums", "congruence", - "octagon", + "octagonAnalysis", + "octagonVars", "wideningThresholds", "loopUnrollHeuristic", "memsafetySpecification", diff --git a/conf/svcomp26/level04.json b/conf/svcomp26/level04.json index 960b2bdb6b..3e98526391 100644 --- a/conf/svcomp26/level04.json +++ b/conf/svcomp26/level04.json @@ -60,7 +60,8 @@ "noRecursiveIntervals", "enums", "congruence", - "octagon", + "octagonAnalysis", + "octagonVars", "wideningThresholds", "loopUnrollHeuristic", "memsafetySpecification", diff --git a/src/autoTune.ml b/src/autoTune.ml index 3ae818435e..30064a7649 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -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." + +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 @@ -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 @@ -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 diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 134ce7eb95..2d6f0992c4 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -556,7 +556,8 @@ "loopUnrollHeuristic", "forceLoopUnrollForFewLoops", "arrayDomain", - "octagon", + "octagonAnalysis", + "octagonVars", "wideningThresholds", "memsafetySpecification", "concurrencySafetySpecification", @@ -573,7 +574,8 @@ "enums", "loopUnrollHeuristic", "arrayDomain", - "octagon", + "octagonAnalysis", + "octagonVars", "wideningThresholds", "memsafetySpecification", "concurrencySafetySpecification", diff --git a/tests/regression/29-svcomp/35-nla-sqrt.c b/tests/regression/29-svcomp/35-nla-sqrt.c index dc382181cc..ee0a06f576 100644 --- a/tests/regression/29-svcomp/35-nla-sqrt.c +++ b/tests/regression/29-svcomp/35-nla-sqrt.c @@ -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 // Extracted from: nla-digbench-scaling/sqrt1-ll_unwindbound5.c #include extern int __VERIFIER_nondet_int(void); diff --git a/tests/regression/29-svcomp/38-autotune-octagon-fun.t b/tests/regression/29-svcomp/38-autotune-octagon-fun.t index 05653bf107..386716eefc 100644 --- a/tests/regression/29-svcomp/38-autotune-octagon-fun.t +++ b/tests/regression/29-svcomp/38-autotune-octagon-fun.t @@ -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. + [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