Fix finding of fixed loop unrolling for dynamic

goblint · Nov 7, 2024 · 3ff3025 · 3ff3025
1 parent 2067ca3
commit 3ff3025
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 2 deletions.
diff --git a/src/common/framework/myCFG.ml b/src/common/framework/myCFG.ml
@@ -85,4 +85,5 @@ sig
 end
 
 (* TODO: move back to LoopUnrolling, now here to break dependency cycle *)
+let factor0: int Cilfacade.StmtH.t = Cilfacade.StmtH.create 100
 let factorH: int NodeH.t = NodeH.create 100
diff --git a/src/util/cilCfg.ml b/src/util/cilCfg.ml
@@ -43,9 +43,12 @@ let createCFG (fileAST: file) =
   iterGlobals fileAST (fun glob ->
       match glob with
       | GFun(fd,_) ->
+        if (get_int "exp.unrolling-factor")>0 || AutoTune0.isActivated "loopUnrollHeuristic" then LoopUnrolling.unroll_loops fd loops; (* must be done before prepareCFG, otherwise cannot find breaks *)
         prepareCFG fd;
         computeCFGInfo fd true;
-        if (get_int "exp.unrolling-factor")>0 || AutoTune0.isActivated "loopUnrollHeuristic" then LoopUnrolling.unroll_loops fd loops;
+        Cilfacade.StmtH.iter (fun stmt factor ->
+            MyCFG.NodeH.add MyCFG.factorH (Statement (fst (CfgTools.find_real_stmt stmt))) factor (* must be done after computeCFGInfo, otherwise no succs *)
+          ) MyCFG.factor0
       | _ -> ()
     );
   if get_bool "dbg.run_cil_check" then assert (Check.checkFile [] fileAST);
diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
@@ -456,7 +456,8 @@ class loopUnrollingVisitor (func, totalLoops) = object
         nests <- nests - 1; Logs.debug "nests: %i" nests;
         let factor = loop_unrolling_factor stmt func totalLoops in
         if factor > 0 then (
-          MyCFG.NodeH.add MyCFG.factorH (Statement (fst (CfgTools.find_real_stmt stmt))) factor;
+          (* MyCFG.NodeH.add MyCFG.factorH (Statement (fst (CfgTools.find_real_stmt stmt))) factor; *)
+          Cilfacade.StmtH.add MyCFG.factor0 stmt factor;
           Logs.info "unrolling loop at %a with factor %d" CilType.Location.pretty loc factor;
           annotateArrays b;
           stmt