From 444e89bbe58773efd0eda8ae9c2193e9e68f86f7 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Thu, 17 Nov 2022 11:41:01 +0100 Subject: [PATCH 1/4] Autotuner: add check that globally conditionally enables congruences on the whole program. Enables congruence domain on whole program when there is enough complexity-'fuel' left --- src/autoTune.ml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/autoTune.ml b/src/autoTune.ml index 1972dc12af..d1a24cc0a4 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -315,6 +315,21 @@ class octagonFunctionVisitor(list, amount) = object end +let congruenceOption factors file = + let locals, globals = factors.integralVars in + let cost = (locals + globals) * (factors.instructions / 12) + 5 * factors.functionCalls in + let value = 5 * locals + globals in + let activate () = + print_endline @@ "Congruence: " ^ string_of_int cost; + set_bool "ana.int.congruence" true; + print_endline "Enabled congruence domain."; + in + { + value; + cost; + activate; + } + let apronOctagonOption factors file = let locals = if List.mem "specification" (get_string_list "ana.autotune.activated" ) && get_string "ana.specification" <> "" then @@ -429,6 +444,7 @@ let chooseConfig file = print_endline @@ "File: " ^ string_of_int fileCompplexity; let options = [] in + let options = if isActivated "congruence" then (congruenceOption factors file)::options else options in let options = if isActivated "octagon" then (apronOctagonOption factors file)::options else options in let options = if isActivated "wideningThresholds" then (wideningOption factors file)::options else options in From 48cb8dd26aa455f27eef4a062678b262e976a3ba Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Thu, 17 Nov 2022 13:51:15 +0100 Subject: [PATCH 2/4] svcopm23 configuration: Add congruence option to autotune. Enabling this option has two effects: (a) The congruence domain is enabled for functions that use modulo, and (b) the congruence domain is globally enabled for programs where there is still some autotuner "fuel" for the program. --- conf/svcomp23.json | 1 + 1 file changed, 1 insertion(+) diff --git a/conf/svcomp23.json b/conf/svcomp23.json index a5019ffdc5..2b3b8fbfd0 100644 --- a/conf/svcomp23.json +++ b/conf/svcomp23.json @@ -67,6 +67,7 @@ "mallocWrappers", "noRecursiveIntervals", "enums", + "congruence", "octagon", "wideningThresholds" ] From 5585a56f2a96bd873f334c5b89c81e404e7a375a Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Thu, 17 Nov 2022 15:32:13 +0100 Subject: [PATCH 3/4] svcomp23: Remove "congruence" from ana.autotune.activated. By removing the setting, the autotuner will not enable congruences with this configuration. --- conf/svcomp23.json | 1 - 1 file changed, 1 deletion(-) diff --git a/conf/svcomp23.json b/conf/svcomp23.json index 2b3b8fbfd0..a5019ffdc5 100644 --- a/conf/svcomp23.json +++ b/conf/svcomp23.json @@ -67,7 +67,6 @@ "mallocWrappers", "noRecursiveIntervals", "enums", - "congruence", "octagon", "wideningThresholds" ] From 6e18dafe58cb45a5b5e916a397a29764891f630d Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 21 Nov 2022 13:41:41 +0100 Subject: [PATCH 4/4] Add congruence annotations to functions only when totalTarget is not yet reached. --- src/autoTune.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index d1a24cc0a4..c88c112425 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -413,7 +413,16 @@ let chooseFromOptions costTarget options = let isActivated a = get_bool "ana.autotune.enabled" && List.mem a @@ get_string_list "ana.autotune.activated" let chooseConfig file = - if isActivated "congruence" then + let factors = collectFactors visitCilFileSameGlobals file in + let fileCompplexity = estimateComplexity factors file in + + print_endline "Collected factors:"; + printFactors factors; + print_endline ""; + print_endline "Complexity estimates:"; + print_endline @@ "File: " ^ string_of_int fileCompplexity; + + if fileCompplexity < totalTarget && isActivated "congruence" then addModAttributes file; if isActivated "noRecursiveIntervals" then @@ -434,15 +443,6 @@ let chooseConfig file = if isActivated "arrayDomain" then selectArrayDomains file; - let factors = collectFactors visitCilFileSameGlobals file in - let fileCompplexity = estimateComplexity factors file in - - print_endline "Collected factors:"; - printFactors factors; - print_endline ""; - print_endline "Complexity estimates:"; - print_endline @@ "File: " ^ string_of_int fileCompplexity; - let options = [] in let options = if isActivated "congruence" then (congruenceOption factors file)::options else options in let options = if isActivated "octagon" then (apronOctagonOption factors file)::options else options in