Merge pull request #912 from leunam99/master

Enable constant loop unrolling for small files

src/util/cilCfg.ml

@@ -22,6 +22,23 @@ let end_basic_blocks f =
   let thisVisitor = new allBBVisitor in
   visitCilFileSameGlobals thisVisitor f
 
+
+class countLoopsVisitor(count) = object
+  inherit nopCilVisitor
+
+  method! vstmt stmt = match stmt.skind with
+    | Loop _ -> count := !count + 1; DoChildren
+    | _ -> DoChildren
+
+end 
+
+let loopCount file = 
+  let count = ref 0 in
+  let visitor = new countLoopsVisitor(count) in
+  ignore (visitCilFileSameGlobals visitor file);
+  !count
+
+
 let createCFG (fileAST: file) =
   (* The analyzer keeps values only for blocks. So if you want a value for every program point, each instruction      *)
   (* needs to be in its own block. end_basic_blocks does that.                                                        *)
@@ -36,11 +53,13 @@ let createCFG (fileAST: file) =
    * Renumbering is problematic for using [Cabs2cil.environment], e.g. in witness invariant generation to use original variable names.
    * See https://github.com/goblint/cil/issues/31#issuecomment-824939793. *)
 
+  let loops = loopCount fileAST in
+
   iterGlobals fileAST (fun glob ->
       match glob with
       | GFun(fd,_) ->
         (* before prepareCfg so continues still appear as such *)
-        if (get_int "exp.unrolling-factor")>0 || AutoTune0.isActivated "loopUnrollHeuristic" then LoopUnrolling.unroll_loops fd;
+        if (get_int "exp.unrolling-factor")>0 || AutoTune0.isActivated "loopUnrollHeuristic" then LoopUnrolling.unroll_loops fd loops;
         prepareCFG fd;
         computeCFGInfo fd true
       | _ -> ()

src/util/loopUnrolling.ml

@@ -332,24 +332,29 @@ class loopUnrollingCallVisitor = object
 
 end
 
-let loop_unrolling_factor loopStatement func =
+let loop_unrolling_factor loopStatement func totalLoops =
   let configFactor = get_int "exp.unrolling-factor" in
-  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 targetInstructions = if unrollFunctionCalled then 50 else 25 in
-  let loopStats = AutoTune0.collectFactors visitCilStmt loopStatement in
-  let targetFactor = if loopStats.instructions > 0 then targetInstructions / loopStats.instructions else 0 in (* Don't unroll empty (= while(1){}) loops*)
-  let fixedLoop = fixedLoopSize loopStatement func in
   if AutoTune0.isActivated "loopUnrollHeuristic" then
-    match fixedLoop with
-    | Some i -> if i * loopStats.instructions < 100 then (print_endline "fixed loop size"; i) else 100 / loopStats.instructions
-    | _ -> targetFactor
+    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 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 (print_endline "fixed loop size"; i) else max unroll_min (100 / loopStats.instructions)
+      | _ -> max unroll_min (targetInstructions / loopStats.instructions)
+    else
+      (* Don't unroll empty (= while(1){}) loops*)
+      0
   else
     configFactor
 
@@ -432,15 +437,15 @@ class copyandPatchLabelsVisitor(loopEnd,currentIterationEnd) = object
     | _ -> ChangeDoChildrenPost(rename_labels s, after)
 end
 
-class loopUnrollingVisitor(func) = object
+class loopUnrollingVisitor(func, totalLoops) = object
   (* Labels are simply handled by giving them a fresh name. Jumps coming from outside will still always go to the original label! *)
   inherit nopCilVisitor
 
   method! vstmt s =
     match s.skind with
     | Loop (b,loc, loc2, break , continue) ->
       let duplicate_and_rem_labels s =
-        let factor = loop_unrolling_factor s func in
+        let factor = loop_unrolling_factor s func totalLoops in
         if(factor > 0) then (
           print_endline @@ "unrolling loop at " ^ CilType.Location.show loc ^" with factor " ^ string_of_int factor;
           annotateArrays b;
@@ -465,7 +470,7 @@ class loopUnrollingVisitor(func) = object
     | _ -> DoChildren
 end
 
-let unroll_loops fd =
+let unroll_loops fd totalLoops =
   Cil.populateLabelAlphaTable fd;
-  let thisVisitor = new loopUnrollingVisitor(fd) in
+  let thisVisitor = new loopUnrollingVisitor(fd, totalLoops) in
   ignore (visitCilFunction thisVisitor fd)

src/util/options.schema.json

@@ -515,7 +515,7 @@
             },
             "activated": {
               "title": "ana.autotune.activated",
-              "description": "Lists of activated tuning options. By default all are activated",
+              "description": "Lists of activated tuning options.",
               "type": "array",
               "items": { "type": "string" },
               "default": [