Merge pull request #1403 from goblint/yaml-witness-unrolled-loop

Record statement copies during loop unrolling

src/common/framework/cfgTools.ml

@@ -559,7 +559,16 @@ struct
       | FunctionEntry _ -> ["shape=box"]
     in
     let styles = String.concat "," (label @ shape @ extraNodeStyles n) in
-    Format.fprintf out ("\t%a [%s];\n") p_node n styles
+    Format.fprintf out ("\t%a [%s];\n") p_node n styles;
+    match n with
+    | Statement s when get_bool "dbg.cfg.loop-unrolling" ->
+      begin match LoopUnrolling0.find_copyof s with
+        | Some s' ->
+          let n' = Statement s' in
+          Format.fprintf out "\t%a -> %a [style=dotted];\n" p_node n p_node n'
+        | None -> ()
+      end
+    | _ -> ()
 end
 
 let fprint_dot (module CfgPrinters: CfgPrinters) iter_edges out =

src/common/util/loopUnrolling0.ml

@@ -0,0 +1,19 @@
+open GoblintCil
+
+module CopyOfHashTable = Hashtbl.Make(struct
+    type t = stmt
+    (* Identity by physical equality. *)
+    let equal = (==)
+    (* Hash only labels and skind (statement itself) because they should remain unchanged between now
+       and lookup after analysis.
+       CFG construction modifies sid, succs, preds and fallthrough, which are empty here.*)
+    let hash (s: stmt) = Hashtbl.hash (s.skind, s.labels)
+  end)
+let copyof = CopyOfHashTable.create 113
+
+let find_copyof = CopyOfHashTable.find_opt copyof
+
+let rec find_original s =
+  match find_copyof s with
+  | None -> s
+  | Some s' -> (find_original [@tailcall]) s'

src/config/options.schema.json

@@ -1991,6 +1991,12 @@
               "description": "Add loop SCC clusters to CFG .dot output.",
               "type": "boolean",
               "default": false
+            },
+            "loop-unrolling": {
+              "title": "dbg.cfg.loop-unrolling",
+              "description": "Add dotted loop unrolling copy-of edges to CFG .dot output.",
+              "type": "boolean",
+              "default": false
             }
           },
           "additionalProperties": false

src/util/loopUnrolling.ml

@@ -1,8 +1,8 @@
-(** Syntactic loop unrolling. *)
-
 open GobConfig
 open GoblintCil
 
+module M = Messages
+
 (*loop unroll heuristics*)
 (*used if AutoTune is activated*)
 
@@ -384,6 +384,8 @@ class patchLabelsGotosVisitor(newtarget) = object
     | _ -> DoChildren
 end
 
+include LoopUnrolling0
+
 (*
   Makes a copy, replacing top-level breaks with goto loopEnd and top-level continues with
   goto currentIterationEnd
@@ -401,6 +403,8 @@ class copyandPatchLabelsVisitor(loopEnd, currentIterationEnd, gotos) = object
       let new_labels = List.map (function Label(str,loc,b) -> Label (Cil.freshLabel str,loc,b) | x -> x) sn.labels in
       (* this makes new physical copy*)
       let new_s = {sn with labels = new_labels} in
+      CopyOfHashTable.replace copyof new_s s;
+      if M.tracing then M.trace "cfg" "Marking %a as copy of %a" CilType.Stmt.pretty new_s CilType.Stmt.pretty s;
       if new_s.labels <> [] then
         (* Use original s, ns might be temporay e.g. if the type of statement changed *)
         (* record that goto s; appearing in the current fragment should later be patched to goto new_s *)

src/util/loopUnrolling.mli

@@ -0,0 +1,9 @@
+(** Syntactic loop unrolling. *)
+
+val unroll_loops: GoblintCil.fundec -> int -> unit
+(** Unroll loops in a function.
+
+    @param totalLoops total number of loops from autotuner *)
+
+val find_original: GoblintCil.stmt -> GoblintCil.stmt
+(** Find original un-unrolled instance of the statement. *)

tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.c

@@ -0,0 +1,13 @@
+int main() {
+  int i = 0;
+  while (i < 10)
+    i++;
+
+  int j = 0, k = 0;
+  while (j < 10) {
+    while (k < 100)
+      k++;
+    j++;
+  }
+  return 0;
+}

tests/regression/55-loop-unrolling/dune

@@ -1,2 +1,8 @@
 (cram
  (deps (glob_files *.c)))
+
+(cram
+ (applies_to 11-unrolled-loop-invariant)
+ (enabled_if %{bin-available:graph-easy})
+ (deps
+   %{bin:cfgDot}))

tests/regression/cfg/util/cfgDot.ml

@@ -1,12 +1,31 @@
+open Goblint_lib
+
+let usage_msg = "cfgDot [--unroll <n>] <file>"
+
+let files = ref []
+let unroll = ref 0
+
+let anon_fun filename =
+  files := filename :: !files
+
+let speclist = [
+  ("--unroll", Arg.Set_int unroll, "Unroll loops");
+]
+
 let main () =
   Goblint_logs.Logs.Level.current := Info;
   Cilfacade.init ();
+  GobConfig.set_bool "dbg.cfg.loop-unrolling" true;
+  GobConfig.set_int "exp.unrolling-factor" !unroll;
 
-  let ast = Cilfacade.getAST (Fpath.v Sys.argv.(1)) in
+  assert (List.length !files = 1);
+  let ast = Cilfacade.getAST (Fpath.v (List.hd !files)) in
   CilCfg0.end_basic_blocks ast;
   (* Part of CilCfg.createCFG *)
   GoblintCil.iterGlobals ast (function
       | GFun (fd, _) ->
+        if !unroll > 0 then
+          LoopUnrolling.unroll_loops fd (-1);
         GoblintCil.prepareCFG fd;
         GoblintCil.computeCFGInfo fd true
       | _ -> ()
@@ -52,4 +71,6 @@ let main () =
       | _ -> ()
     )
 
-let () = main ()
+let () =
+  Arg.parse speclist anon_fun usage_msg;
+  main ()

tests/regression/cfg/util/dune

@@ -4,6 +4,7 @@
    goblint-cil
    goblint_logs
    goblint_common
+   goblint_lib ; TODO: avoid: extract LoopUnrolling from goblint_lib
    fpath
    goblint.sites.dune
    goblint.build-info.dune)