From 446da4f340a3b456c9cb134380a9c45ca9a370b5 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 27 Sep 2024 15:12:49 +0300 Subject: [PATCH 1/4] Simplify fixed loop size heuristics --- src/util/loopUnrolling.ml | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index ea92b0d1e6..f8b53bed1c 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -347,15 +347,11 @@ let loop_unrolling_factor loopStatement func totalLoops = Found -> true in (*unroll up to near an instruction count, higher if the loop uses malloc/lock/threads *) - let targetInstructions = if unrollFunctionCalled then 50 else 25 in let loopStats = AutoTune0.collectFactors visitCilStmt loopStatement in if loopStats.instructions > 0 then - let fixedLoop = fixedLoopSize loopStatement func in - (* Unroll at least 10 times if there are only few (17?) loops *) - let unroll_min = if totalLoops < 17 && AutoTune0.isActivated "forceLoopUnrollForFewLoops" then 10 else 0 in - match fixedLoop with - | Some i -> if i * loopStats.instructions < 100 then (Logs.debug "fixed loop size"; i) else max unroll_min (100 / loopStats.instructions) - | _ -> max unroll_min (targetInstructions / loopStats.instructions) + match fixedLoopSize loopStatement func with + | Some i when i <= 20 -> Logs.debug "fixed loop size %d" i; i + | _ -> 4 else (* Don't unroll empty (= while(1){}) loops*) 0 From e8f51dcaa712c619b4e7b25c26081c6229a55a9f Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 27 Sep 2024 19:53:38 +0300 Subject: [PATCH 2/4] Remove unused loopUnrollingCallVisitor --- src/util/loopUnrolling.ml | 39 --------------------------------------- 1 file changed, 39 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index f8b53bed1c..0872eb9b1c 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -305,48 +305,9 @@ class arrayVisitor = object end let annotateArrays loopBody = ignore @@ visitCilBlock (new arrayVisitor) loopBody -(*unroll loops that handle locks, threads and mallocs, asserts and reach_error*) -class loopUnrollingCallVisitor = object - inherit nopCilVisitor - - method! vinst = function - | Call (_,Lval ((Var info), NoOffset),args,_,_) when LibraryFunctions.is_special info -> ( - Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo info) @@ fun () -> - let desc = LibraryFunctions.find info in - match desc.special args with - | Malloc _ - | Calloc _ - | Realloc _ - | Alloca _ - | Lock _ - | Unlock _ - | ThreadCreate _ - | Assert _ - | Bounded _ - | ThreadJoin _ -> - raise Found; - | _ -> - if List.mem "specification" @@ get_string_list "ana.autotune.activated" && get_string "ana.specification" <> "" then ( - if Svcomp.is_error_function' info (SvcompSpec.of_option ()) then - raise Found - ); - DoChildren - ) - | _ -> DoChildren - -end - let loop_unrolling_factor loopStatement func totalLoops = let configFactor = get_int "exp.unrolling-factor" in if AutoTune0.isActivated "loopUnrollHeuristic" then - let unrollFunctionCalled = try - let thisVisitor = new loopUnrollingCallVisitor in - ignore (visitCilStmt thisVisitor loopStatement); - false; - with - Found -> true - in - (*unroll up to near an instruction count, higher if the loop uses malloc/lock/threads *) let loopStats = AutoTune0.collectFactors visitCilStmt loopStatement in if loopStats.instructions > 0 then match fixedLoopSize loopStatement func with From 42c3f5a4274fcd868a5255c1393c880df21af4d3 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Mon, 30 Sep 2024 17:21:51 +0300 Subject: [PATCH 3/4] Do not turn on autotune loop unrolling when the only specification is NoDataRace --- src/util/loopUnrolling.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index a191e414f9..aea2a2cd92 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -307,6 +307,11 @@ class arrayVisitor = object end let annotateArrays loopBody = ignore @@ visitCilBlock (new arrayVisitor) loopBody +let max_default_unrolls_per_spec (spec: Svcomp.Specification.t) = + match spec with + | NoDataRace -> 0 + | _ -> 4 + let loop_unrolling_factor loopStatement func totalLoops = let configFactor = get_int "exp.unrolling-factor" in if AutoTune0.isActivated "loopUnrollHeuristic" then @@ -314,7 +319,10 @@ let loop_unrolling_factor loopStatement func totalLoops = if loopStats.instructions > 0 then match fixedLoopSize loopStatement func with | Some i when i <= 20 -> Logs.debug "fixed loop size %d" i; i - | _ -> 4 + | _ -> + match Svcomp.Specification.of_option () with + | [] -> 4 + | specs -> BatList.max @@ List.map max_default_unrolls_per_spec specs else (* Don't unroll empty (= while(1){}) loops*) 0 From 5ba3996c496dca577cfeacc3a90f7872b81679c6 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Wed, 2 Oct 2024 11:47:02 +0300 Subject: [PATCH 4/4] Default to unrolling 2 times for no-overflow spec --- src/util/loopUnrolling.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index aea2a2cd92..c883e121fc 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -310,6 +310,7 @@ let annotateArrays loopBody = ignore @@ visitCilBlock (new arrayVisitor) loopBod let max_default_unrolls_per_spec (spec: Svcomp.Specification.t) = match spec with | NoDataRace -> 0 + | NoOverflow -> 2 | _ -> 4 let loop_unrolling_factor loopStatement func totalLoops =