Add semantic loop unrolling analysis

src/analyses/loopUnrollAnalysis.ml

@@ -0,0 +1,91 @@
+(** Semantic loop unrolling ([loopunroll]). *)
+
+open Batteries
+open GoblintCil
+open Analyses
+
+module M = Messages
+
+module ID = Queries.ID
+
+module Spec : Analyses.MCPSpec =
+struct
+  let name () = "loopunroll"
+
+  module CountParam =
+  struct
+    let n () = GobConfig.get_int "exp.unrolling-factor" + 1
+    let names = string_of_int
+  end
+  module Count = Lattice.Chain (CountParam)
+
+  module D = MapDomain.MapBot (Node) (Count)
+  module C = D
+
+  let startstate v = D.bot ()
+  let exitstate = startstate
+
+  include Analyses.DefaultSpec
+  module P = IdentityP (D)
+
+  let emit_splits ctx d =
+    match CfgTools.is_loop_head ctx.node with
+    | Some s ->
+      let cur = D.find ctx.node d in
+      let next =
+        if cur = CountParam.n () then
+          cur
+        else
+          cur + 1
+      in
+      D.add ctx.node next d
+    | None ->
+      d
+
+  let emit_splits_ctx ctx =
+    emit_splits ctx ctx.local
+
+  let assign ctx (lval:lval) (rval:exp) =
+    emit_splits_ctx ctx
+
+  let vdecl ctx (var:varinfo) =
+    emit_splits_ctx ctx
+
+  let branch ctx (exp:exp) (tv:bool) =
+    let d = ctx.local in
+    let d' =
+      match CfgTools.is_loop_head ctx.prev_node with
+      | Some s when tv = false ->
+        D.remove ctx.prev_node d
+      | _ ->
+        d
+    in
+    emit_splits ctx d'
+
+  let enter ctx (lval: lval option) (f:fundec) (args:exp list) =
+    [ctx.local, ctx.local]
+
+  let body ctx (f:fundec) =
+    emit_splits_ctx ctx
+
+  let return ctx (exp:exp option) (f:fundec) =
+    emit_splits_ctx ctx
+
+  let combine_env ctx lval fexp f args fc au f_ask =
+    let d = D.join ctx.local au in
+    emit_splits ctx d (* Update/preserve splits for globals in combined environment. *)
+
+  let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =
+    emit_splits_ctx ctx (* Update/preserve splits over assigned variable. *)
+
+  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) =
+    emit_splits_ctx ctx
+
+  let threadenter ctx ~multiple lval f args = [ctx.local]
+
+  let threadspawn ctx ~multiple lval f args fctx =
+    emit_splits_ctx ctx
+end
+
+let () =
+  MCP.register_analysis (module Spec : MCPSpec)

src/common/framework/cfgTools.ml

@@ -722,3 +722,18 @@ let numGlobals file =
   (* GVar Cannot have storage Extern or function type *)
   Cil.iterGlobals file (function GVar _ -> incr n | _ -> ());
   !n
+
+
+let current_skipped = ref (CfgEdgeH.create 0)
+
+let is_loop_head n =
+  let (module Cfg: CfgBidir) = !current_cfg in
+  let prevs = Cfg.prev n in
+  List.find_map (fun (edges, prev) ->
+      let stmts = CfgEdgeH.find !current_skipped (prev, edges, n) in
+      List.find_map (fun s ->
+          match s.GoblintCil.skind with
+          | Loop (_, loc, _, _, _) -> Some s
+          | _ -> None
+        ) stmts
+    ) prevs

src/config/options.schema.json

@@ -344,15 +344,15 @@
           "default": [
             "expRelation", "base", "threadid", "threadflag", "threadreturn",
             "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp",
-            "assert"
+            "assert", "loopunroll"
           ]
         },
         "path_sens": {
           "title": "ana.path_sens",
           "description": "List of path-sensitive analyses",
           "type": "array",
           "items": { "type": "string" },
-          "default": [ "mutex", "malloc_null", "uninit", "expsplit","activeSetjmp","memLeak" ]
+          "default": [ "mutex", "malloc_null", "uninit", "expsplit","activeSetjmp","memLeak", "loopunroll" ]
         },
         "ctx_insens": {
           "title": "ana.ctx_insens",

src/framework/constraints.ml

@@ -819,6 +819,7 @@ struct
       Timing.Program.enter new_fd.svar.vname;
     let old_context = !M.current_context in
     current_node := Some u;
+    Logs.debug "Node %a loop head: %a" Node.pretty u (Pretty.docOpt (CilType.Stmt.pretty ())) (CfgTools.is_loop_head u);
     M.current_context := Some (Obj.magic c); (* magic is fine because Spec is top-level Control Spec *)
     Fun.protect ~finally:(fun () ->
         current_node := old_node;

src/framework/control.ml

@@ -817,4 +817,5 @@ let analyze change_info (file: file) fs =
   Logs.debug "Generating the control flow graph.";
   let (module CFG), skippedByEdge = compute_cfg_skips file in
   MyCFG.current_cfg := (module CFG);
+  CfgTools.current_skipped := skippedByEdge;
   analyze_loop (module CFG) file fs change_info skippedByEdge

src/util/cilCfg.ml

@@ -63,7 +63,7 @@ let createCFG (fileAST: file) =
       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;
+        (* if (get_int "exp.unrolling-factor")>0 || AutoTune0.isActivated "loopUnrollHeuristic" then LoopUnrolling.unroll_loops fd loops; *)
         prepareCFG fd;
         computeCFGInfo fd true
       | _ -> ()

tests/regression/55-loop-unrolling/07-nested-unroll.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5  --enable dbg.run_cil_check
+// PARAM: --enable ana.int.interval --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5  --enable dbg.run_cil_check --enable solvers.td3.restart.wpoint.enabled
 #include <goblint.h>
 int main(void) {
     int arr[10][10];

tests/regression/67-interval-sets-two/08-nested-unroll.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval_set --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5
+// PARAM: --enable ana.int.interval_set --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable solvers.td3.restart.wpoint.enabled
 #include <goblint.h>
 int main(void) {
     int arr[10][10];