diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index aa59c090c4..0c21004334 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -345,7 +345,7 @@ struct let exit_loop max_iter x l : LoopCounts.t list = List.init (max_iter + 1) (fun i -> LoopCounts.add x i l) - let unroll (v,(c,l)) (edges, u) max_iter = + let unroll (v,(c,l)) (edges, u) = let open GobList.Syntax in let u_heads = NodeH.find_default loop_heads u NodeSet.empty in let v_heads = NodeH.find_default loop_heads v NodeSet.empty in @@ -355,7 +355,10 @@ struct (* For each node 'u' within a loop from where the loop is exited, add loop counts from 0 up to the max nr of unroll iterations (max_iter). For nested loops we have to add (combinations of) loop counts for all of the nests. *) - let ls = NodeSet.fold (fun exit ls -> List.concat_map (exit_loop max_iter exit) ls) exits [l] in + let ls = NodeSet.fold (fun exit ls -> + let unroll_factor = NodeH.find_default LoopUnrolling.factorH exit 0 in + List.concat_map (exit_loop unroll_factor exit) ls + ) exits [l] in (* For each node 'u' that is not in the same loop as node 'v', i.e. the loop is entered for the first time from 'u', if loop counts have reached 0, remove the loop counts to take the entry edge. *) @@ -365,7 +368,8 @@ struct - If the loop count includes max_iter, keep it to represent any remaining loop iterations that were not unrolled. - If loop counts has reached 0 for 'v', stop calculating further loop counts, as unrolling stops and loop entry edge must be taken instead. *) if is_back_edge then - List.concat_map (back_edge max_iter v) ls + let unroll_factor = NodeH.find_default LoopUnrolling.factorH v 0 in + List.concat_map (back_edge unroll_factor v) ls else ls @@ -408,7 +412,7 @@ struct let _, locs = List.fold_right (fun (f,e) (t,xs) -> f, (f,t)::xs) edges (Node.location v,[]) in let res = List.fold_left2 (|>) pval (List.map (tf (v,(Obj.repr (fun () -> c),l)) getl sidel getg sideg u) edges) locs in S.D.join acc res - ) (S.D.bot ()) (unroll (v,(c,l)) (edges, u) 10) (* TODO: value hardcoded *) + ) (S.D.bot ()) (unroll (v,(c,l)) (edges, u)) let tf (v,(c,l)) (e,u) getl sidel getg sideg = let old_node = !current_node in diff --git a/src/util/cilCfg.ml b/src/util/cilCfg.ml index d6e74fc8af..0692996ce4 100644 --- a/src/util/cilCfg.ml +++ b/src/util/cilCfg.ml @@ -43,10 +43,9 @@ let createCFG (fileAST: file) = 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 loops; prepareCFG fd; - computeCFGInfo fd true + computeCFGInfo fd true; + if (get_int "exp.unrolling-factor")>0 || AutoTune0.isActivated "loopUnrollHeuristic" then LoopUnrolling.unroll_loops fd loops; | _ -> () ); if get_bool "dbg.run_cil_check" then assert (Check.checkFile [] fileAST); \ No newline at end of file diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 506337ac1b..7f55b8ff08 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -442,6 +442,8 @@ let copy_and_patch_labels break_target current_continue_target stmts = let patchLabelsVisitor = new patchLabelsGotosVisitor(StatementHashTable.find_opt gotos) in List.map (visitCilStmt patchLabelsVisitor) stmts' +let factorH = MyCFG.NodeH.create 100 + 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 @@ -455,18 +457,10 @@ 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 factorH (Statement (fst (CfgTools.find_real_stmt stmt))) factor; Logs.info "unrolling loop at %a with factor %d" CilType.Location.pretty loc factor; annotateArrays b; - (* top-level breaks should immediately go to the end of the loop, and not just break out of the current iteration *) - let break_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel "loop_end",loc, false)]} in - let copies = List.init factor (fun i -> - (* continues should go to the next unrolling *) - let current_continue_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, false)]} in - let one_copy_stmts = copy_and_patch_labels break_target current_continue_target b.bstmts in - one_copy_stmts @ [current_continue_target] - ) - in - mkStmt (Block (mkBlock (List.flatten copies @ [stmt; break_target]))) + stmt ) else stmt (*no change*) | _ -> stmt in diff --git a/src/util/loopUnrolling.mli b/src/util/loopUnrolling.mli index ea45688c77..09b87be02f 100644 --- a/src/util/loopUnrolling.mli +++ b/src/util/loopUnrolling.mli @@ -7,3 +7,5 @@ val unroll_loops: GoblintCil.fundec -> int -> unit val find_original: GoblintCil.stmt -> GoblintCil.stmt (** Find original un-unrolled instance of the statement. *) + +val factorH : int CfgTools.NH.t