From f2623868f8f6fbcc9230c62389625f89a1e1c7d5 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Thu, 23 Nov 2023 14:06:46 +0100 Subject: [PATCH 1/3] Fix Not_found exception in autotuner with congruences and termination. --- src/autoTune.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index fefdeb32fd..1fd1fa5ee6 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -99,7 +99,9 @@ let rec setCongruenceRecursive fd depth neigbourFunction = FunctionSet.iter (fun vinfo -> print_endline (" " ^ vinfo.vname); - setCongruenceRecursive (Cilfacade.find_varinfo_fundec vinfo) (depth -1) neigbourFunction + match (Cilfacade.find_varinfo_fundec vinfo) with + | fd -> setCongruenceRecursive fd (depth -1) neigbourFunction + | exception Not_found -> () (* Happens for __goblint_bounded*) ) (FunctionSet.filter (*for extern and builtin functions there is no function definition in CIL*) (fun x -> not (isExtern x.vstorage || BatString.starts_with x.vname "__builtin")) From 5be07e5e96c329ace898bcf973c5d7780bf44da8 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Thu, 23 Nov 2023 14:22:15 +0100 Subject: [PATCH 2/3] Remove unnecessary paranetheses. --- src/autoTune.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/autoTune.ml b/src/autoTune.ml index 1fd1fa5ee6..79f5f51a77 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -99,9 +99,9 @@ let rec setCongruenceRecursive fd depth neigbourFunction = FunctionSet.iter (fun vinfo -> print_endline (" " ^ vinfo.vname); - match (Cilfacade.find_varinfo_fundec vinfo) with + match Cilfacade.find_varinfo_fundec vinfo with | fd -> setCongruenceRecursive fd (depth -1) neigbourFunction - | exception Not_found -> () (* Happens for __goblint_bounded*) + | exception Not_found -> () (* Happens for __goblint_bounded *) ) (FunctionSet.filter (*for extern and builtin functions there is no function definition in CIL*) (fun x -> not (isExtern x.vstorage || BatString.starts_with x.vname "__builtin")) From 9b954b5cd0b14a146267bc80c476d6a81e281643 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Thu, 23 Nov 2023 15:00:25 +0100 Subject: [PATCH 3/3] Add example where autotuner crashed when trying to activate congruence domain when termination was enabled --- tests/regression/78-termination/51-modulo.c | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 tests/regression/78-termination/51-modulo.c diff --git a/tests/regression/78-termination/51-modulo.c b/tests/regression/78-termination/51-modulo.c new file mode 100644 index 0000000000..5f5b8f1924 --- /dev/null +++ b/tests/regression/78-termination/51-modulo.c @@ -0,0 +1,14 @@ +// SKIP TERM PARAM: --enable ana.autotune.enabled --enable ana.sv-comp.functions --enable ana.sv-comp.enabled --set ana.autotune.activated "['congruence']" --set ana.specification "CHECK( init(main()), LTL(F end) )" + +// This task previously crashed due to the autotuner +int main() { + int a; + int odd, count = 0; + while(a > 1) { + odd = a % 2; + if(!odd) a = a / 2; + else a = a - 1; + count++; + } + return count; +}