Loop Unrolling for the first exp.unrolling-factor Iterations

goblint.opam

@@ -61,7 +61,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#b77c663690519be8a672f871a036df3d89b677d5" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#52161cdedf012e9328e516d83e38f7fcdc0534dc" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

goblint.opam.locked

@@ -108,7 +108,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#b77c663690519be8a672f871a036df3d89b677d5"
+    "git+https://github.com/goblint/cil.git#52161cdedf012e9328e516d83e38f7fcdc0534dc"
   ]
   [
     "apron.v0.9.13"

goblint.opam.template

@@ -1,7 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#b77c663690519be8a672f871a036df3d89b677d5" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#52161cdedf012e9328e516d83e38f7fcdc0534dc" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

src/util/cilfacade.ml

@@ -79,6 +79,62 @@ let end_basic_blocks f =
   let thisVisitor = new allBBVisitor in
   visitCilFileSameGlobals thisVisitor f
 
+class loopUnrollingVisitor = object
+  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 mkBlock' b = mkBlock (List.map newsid_stmt b) in
+    let mk_stmt_from_stmt_list bl = mkStmt(Block(mkBlock' bl)) 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 add_label_to_remainder_loop st_loop loc_loop = 
+        st_loop.labels <- (Label(Cil.freshLabel "remainder_loop", loc_loop, false))::st_loop.labels;
+        st_loop in
+      let rec is_remainder_loop loop_stmt_labels =
+        match loop_stmt_labels with
+        | [] -> false
+        | Label(lab,_,_)::tl -> 
+          if BatString.starts_with lab "remainder_loop" then true else is_remainder_loop tl
+        | _ -> false in
+      (* Unrolling *)
+      let rec unroll sl factor =
+        match factor with
+        |0-> sl
+        |_ ->
+          let x = b.bstmts @ sl in
+          unroll x (factor-1) in      
+      let check_type_loop =
+        let is_loop_unrollable s =
+          if is_remainder_loop s.labels then false
+          else true in
+        let unroll_helper st = mk_stmt_from_stmt_list (unroll [(add_label_to_remainder_loop st loc)] get_unrolling_factor) in
+        if is_loop_unrollable s then ChangeDoChildrenPost ((unroll_helper s), fun x -> x)
+        else  DoChildren in
+      check_type_loop
+    | _ -> DoChildren
+end
+
+let loop_unrolling f =
+  let thisVisitor = new loopUnrollingVisitor in
+  visitCilFileSameGlobals thisVisitor f
 
 let visitors = ref []
 let register_preprocess name visitor_fun =
@@ -107,12 +163,21 @@ let createCFG (fileAST: file) =
    * See https://github.com/goblint/cil/issues/31#issuecomment-824939793. *)
 
   iterGlobals fileAST (fun glob ->
-      match glob with
-      | GFun(fd,_) ->
-        prepareCFG fd;
-        computeCFGInfo fd true
-      | _ -> ()
-    );
+    match glob with
+    | GFun(fd,_) ->
+      prepareCFG fd;
+    | _ -> ()
+  );
+  (* The unrolling needs to take place between prepareCFG and computeCFGInfo, since prepareCFG handles the breaks     *)
+  (* and continues, which allow us to replicate the loop's body outside of the loop. computeCFG info creates the CFG, *)
+  (* so it needs to happen before that.                                                                               *)
+  if (get_int "exp.unrolling-factor")>0 then loop_unrolling fileAST;
+  iterGlobals fileAST (fun glob ->
+    match glob with
+    | GFun(fd,_) ->
+      computeCFGInfo fd true
+    | _ -> ()
+  );
   do_preprocess fileAST
 
 let getAST fileName =

src/util/options.schema.json

@@ -1401,6 +1401,13 @@
             "Path to C preprocessor (cpp) to use. If empty, then automatically searched.",
           "type": "string",
           "default": ""
+        },
+        "unrolling-factor": {
+          "title": "exp.unrolling-factor",
+          "description":
+            "Sets the unrolling factor for the loopUnrollingVisitor.",
+          "type": "integer",
+          "default": 0
         }
       },
       "additionalProperties": false