Loop Unrolling for the first exp.unrolling-factor Iterations

src/util/cilfacade.ml

@@ -80,71 +80,45 @@ let end_basic_blocks f =
   let thisVisitor = new allBBVisitor in
   visitCilFileSameGlobals thisVisitor f
 
+class removeLabelsVisitor = object
+  inherit nopCilVisitor
+
+  val nestingDepth = ref 0
+
+  method! vstmt s =
+    let new_labels = List.filter_map (function Label(str,loc,b) -> None | x -> Some x) s.labels in
+    match s.skind with
+    | Loop _ -> nestingDepth := !nestingDepth+1; ChangeDoChildrenPost({s with labels = new_labels}, fun x -> nestingDepth := !nestingDepth-1; x)
+    | Continue loc -> if !nestingDepth = 0 then
+        ChangeTo({s with labels = new_labels; skind = Break loc})
+      else
+        ChangeTo({s with labels = new_labels})
+    | _ -> ChangeDoChildrenPost({s with labels = new_labels}, Fun.id)
+end
+
 class loopUnrollingVisitor = object
+  (* Labels are simply handled by removing them. It is always correct to simply jump into the non-unrolled part of the loop!          *)
+  (* The price we need to pay for this simpler handling of labels and still wanting to benefit from unrolling nested loops is that    *)
+  (* we need to put our unrolled code into fake while(1) loops such that breaks have something to break out of, add artificial breaks *)
+  (* at the end of loops, and replacing (top level!) continues with breaks. *)
+  (* This is still a lot more intuitive than complicated handling of gotos as would be required when doing it after the unrolling     *)
   inherit nopCilVisitor
+
   method! vstmt s =
-    (*
-    All the duplicated stmts need to be re-created or the sid will fail, so we create a copy of st, which is physically unequal to it.
-    A new sid is  computed later (as seen in http://goblint.in.tum.de/assets/goblint-cil/api/Cil.html#TYPEstmt), as long as we perform this copies.
-    *)
-    let newsid st = { st with sid = st.sid } in
-    let rec newsid_stmt st =
-      let mkb stml = mkBlock (List.map newsid_stmt stml) in
-      match st.skind with
-      | Instr _ -> newsid st
-      | If(e,b1,b2,l1,l2) -> mkStmt(If(e,(mkb b1.bstmts),(mkb b2.bstmts),l1,l2))
-      | Loop(bl,l1,l2,s1,s2) ->
-        let create_stmt = mkStmt(Loop((mkb bl.bstmts),l1,l2,s1,s2)) in
-        create_stmt.labels <- st.labels;
-        create_stmt
-      | Block(bl) -> mkStmt(Block(mkb bl.bstmts))
-      | Switch(e,bl,stl,l1,l2) -> mkStmt(Switch(e,(mkb bl.bstmts),(List.map newsid_stmt stl),l1,l2))
-      | _ -> newsid st in
-    let create_shallow_copies bl = List.map newsid_stmt bl in
+    let labelsRemover = new removeLabelsVisitor in
     match s.skind with
-    | Loop(b, loc, _, _, _) ->
-      let get_unrolling_factor = GobConfig.get_int "exp.unrolling-factor" in
-      (* All unrollings will leave the original loop at the end. The label makes sure it's not unrolled twice.*)
-      let rec is_remainder_loop loop_stmt_labels =
-        match loop_stmt_labels with
-        | Label(lab,_,_)::tl -> if BatString.starts_with lab "remainder_loop" then true else is_remainder_loop tl
-        | _ -> false in
-      (* Because this is executed before preparedCFG, there are still Breaks instead of Gotos.*)
-      (* We need to transform them so we can replicate the loop's body outside of the loop.*)
-      let break_stmt = mkStmt (Instr []) in
-      break_stmt.labels <- [Label(Cil.freshLabel "unroll_while_break",loc,false)] ;
-      let continue_stmt = mkStmt (Instr []) in
-      continue_stmt.labels <- [Label(Cil.freshLabel "unroll_while_continue",loc,false)] ;
-      let rec rm_breaks_st st =
-        let rm_breaks_st_list stl = mkBlock (List.map rm_breaks_st stl) in
-        match st.skind with
-        | Break(l) -> mkStmt (Goto (ref break_stmt, loc))
-        | Continue(l) -> mkStmt (Goto (ref continue_stmt, loc))
-        | If(e,tb,fb,l1,l2) -> mkStmt (If (e,(rm_breaks_st_list tb.bstmts), (rm_breaks_st_list fb.bstmts),l1,l2))
-        | Block(bl) -> mkStmt (Block (rm_breaks_st_list bl.bstmts))
-        | Switch(e,bl,stl,l1,l2) -> mkStmt (Switch (e, (rm_breaks_st_list bl.bstmts), (List.map rm_breaks_st stl),l1, l2))
-        | _ -> st in
-      let body = List.map rm_breaks_st b.bstmts in
-      (* Prepare remainder loop for unrolling*)
-      let prepare_remainder_loop st_loop loc_loop =
-        st_loop.labels <- (Label(Cil.freshLabel "remainder_loop", loc_loop, false))::st_loop.labels;
-        mkStmt (Block (mkBlock([continue_stmt;st_loop]))) in
-      (* Unrolling *)
-      let rec unroll sl factor =
-        match factor with
-        |0-> sl
-        |_ ->
-          let duplicate_body bd = create_shallow_copies bd in
-          let x = (duplicate_body body) @ sl in
-          unroll x (factor-1) in
-      let unroll_helper st =
-        let x = unroll [(prepare_remainder_loop st loc)] get_unrolling_factor in
-        mkStmt (Block (mkBlock (x @ [break_stmt]))) in
-      let is_loop_unrollable s = not @@ is_remainder_loop s.labels in
-      let check_type_loop =
-        if is_loop_unrollable s then ChangeDoChildrenPost ((unroll_helper s), fun x -> x)
-        else DoChildren in
-      check_type_loop
+    | Loop (b,loc, loc2, break , continue) ->
+      let duplicate_and_rem_labels s =
+        match s.skind with
+        | Loop (b,loc, loc2, break , continue) ->
+          let s = { s with sid = s.sid } in
+          let factor = GobConfig.get_int "exp.unrolling-factor" in
+          let bstmts = b.bstmts @ [mkStmt @@ Break loc] in
+          let copies = List.init (factor) (fun _ -> visitCilStmt labelsRemover (mkStmt (Loop (mkBlock bstmts,loc,loc2,None,None)))) in
+          mkStmt (Block (mkBlock (copies@[s])))
+        | _ -> failwith "invariant broken"
+      in
+      ChangeDoChildrenPost({s with sid = s.sid},duplicate_and_rem_labels)
     | _ -> DoChildren
 end