Fix and refactor syntactic loop unrolling

src/common/util/cilfacade.ml

@@ -66,8 +66,34 @@ let parse fileName =
     E.s (E.error "There were parsing errors in %s" fileName_str);
   file
 
+(** Version of {!defaultCilPrinterClass} which excludes line directives and builtin signatures (in comments).
+    Used for [dbg.justcil-printer]. *)
+class cleanCilPrinterClass =
+object
+  inherit defaultCilPrinterClass as super
+
+  method! pLineDirective ?(forcefile=false) l =
+    Pretty.nil
+
+  method! pGlobal () (g: global) =
+    match g with
+    | GVarDecl (vi, l) when Hashtbl.mem builtinFunctions vi.vname -> Pretty.nil
+    | _ -> super#pGlobal () g
+end
+
+let cleanCilPrinter = new cleanCilPrinterClass
+
+let cleanDumpFile (pp: cilPrinter) (out : out_channel) (outfile: string) file =
+  Pretty.printDepth := 99999;
+  Pretty.fastMode := true;
+  iterGlobals file (fun g -> dumpGlobal pp out g);
+  flush out
+
 let print (fileAST: file) =
-  dumpFile defaultCilPrinter stdout "stdout" fileAST
+  match GobConfig.get_string "dbg.justcil-printer" with
+  | "default" -> dumpFile defaultCilPrinter stdout "stdout" fileAST
+  | "clean" -> cleanDumpFile cleanCilPrinter stdout "stdout" fileAST
+  | _ -> assert false
 
 let rmTemps fileAST =
   RmUnused.removeUnused fileAST

src/config/options.schema.json

@@ -1860,6 +1860,13 @@
           "type": "string",
           "default": ""
         },
+        "justcil-printer": {
+          "title": "dbg.justcil-printer",
+          "description": "Printer to use for justcil: default, or clean (excludes line directives and builtin declarations).",
+          "type": "string",
+          "enum": ["default", "clean"],
+          "default": "default"
+        },
         "timeout": {
           "title": "dbg.timeout",
           "description":

src/util/loopUnrolling.ml

@@ -299,7 +299,7 @@ class arrayVisitor = object
   inherit nopCilVisitor
 
   method! vvrbl info =
-    if not @@ (hasAttribute "goblint_array_domain" info.vattr || AutoTune0.is_large_array info.vtype) then
+    if Cil.isArrayType info.vtype && not @@ (hasAttribute "goblint_array_domain" info.vattr || AutoTune0.is_large_array info.vtype) then
       info.vattr <- addAttribute (Attr ("goblint_array_domain", [AStr "unroll"]) ) info.vattr;
     DoChildren
 end
@@ -390,27 +390,13 @@ end
   Also assigns fresh names to all labels and patches gotos for labels appearing in the current
   fragment to their new name
 *)
-class copyandPatchLabelsVisitor(loopEnd,currentIterationEnd) = object
+class copyandPatchLabelsVisitor(loopEnd, currentIterationEnd, gotos) = object
   inherit nopCilVisitor
 
-  val mutable depth = 0
   val mutable loopNestingDepth = 0
 
-  val gotos = StatementHashTable.create 20
-
   method! vstmt s =
-    let after x =
-      depth <- depth-1;
-      if depth = 0 then
-        (* the labels can only be patched once the entire part of the AST we want has been transformed, and *)
-        (* we know all lables appear in the hash table *)
-        let patchLabelsVisitor = new patchLabelsGotosVisitor(StatementHashTable.find_opt gotos) in
-        let x  = visitCilStmt patchLabelsVisitor x in
-        StatementHashTable.clear gotos;
-        x
-      else
-        x
-    in
+    let after x = x in
     let rename_labels sn =
       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*)
@@ -421,56 +407,59 @@ class copyandPatchLabelsVisitor(loopEnd,currentIterationEnd) = object
         StatementHashTable.add gotos s new_s;
       new_s
     in
-    depth <- depth+1;
     match s.skind with
     | Continue loc ->
       if loopNestingDepth = 0 then
         (* turn top-level continues into gotos to end of current unrolling *)
-        ChangeDoChildrenPost(rename_labels {s with skind = Goto (!currentIterationEnd, loc)}, after)
+        ChangeDoChildrenPost(rename_labels {s with skind = Goto (ref currentIterationEnd, loc)}, after)
       else
         ChangeDoChildrenPost(rename_labels s, after)
     | Break loc ->
       if loopNestingDepth = 0 then
         (* turn top-level breaks into gotos to end of current unrolling *)
-        ChangeDoChildrenPost(rename_labels {s with skind = Goto (loopEnd,loc)}, after)
+        ChangeDoChildrenPost(rename_labels {s with skind = Goto (ref loopEnd,loc)}, after)
       else
         ChangeDoChildrenPost(rename_labels s, after)
     | Loop _ -> loopNestingDepth <- loopNestingDepth+1;
       ChangeDoChildrenPost(rename_labels s, fun x -> loopNestingDepth <- loopNestingDepth-1; after x)
     | _ -> ChangeDoChildrenPost(rename_labels s, after)
 end
 
+let copy_and_patch_labels break_target current_continue_target stmts =
+  let gotos = StatementHashTable.create 20 in
+  let patcher = new copyandPatchLabelsVisitor (break_target, current_continue_target, gotos) in
+  let stmts' = List.map (visitCilStmt patcher) stmts in
+  (* the labels can only be patched once the entire part of the AST we want has been transformed, and *)
+  (* we know all lables appear in the hash table *)
+  let patchLabelsVisitor = new patchLabelsGotosVisitor(StatementHashTable.find_opt gotos) in
+  List.map (visitCilStmt patchLabelsVisitor) stmts'
+
 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
 
   method! vstmt s =
-    match s.skind with
-    | Loop (b,loc, loc2, break , continue) ->
-      let duplicate_and_rem_labels s =
+    let duplicate_and_rem_labels s =
+      match s.skind with
+      | Loop (b,loc, loc2, break , continue) ->
         let factor = loop_unrolling_factor s func totalLoops in
         if(factor > 0) then (
           Logs.info "unrolling loop at %a with factor %d" CilType.Location.pretty loc factor;
           annotateArrays b;
-          match s.skind with
-          | Loop (b,loc, loc2, break , continue) ->
-            (* 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, true)]} in
-            (* continues should go to the next unrolling *)
-            let continue_target i = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, true)]} in
-            (* passed as a reference so we can reuse the patcher for all unrollings of the current loop *)
-            let current_continue_target = ref dummyStmt in
-            let patcher = new copyandPatchLabelsVisitor (ref break_target, ref current_continue_target) in
-            let one_copy () = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in
-            let copies = List.init (factor) (fun i ->
-                current_continue_target := continue_target i;
-                mkStmt (Block (mkBlock [one_copy (); !current_continue_target])))
-            in
-            mkStmt (Block (mkBlock (copies@[s]@[break_target])))
-          | _ -> failwith "invariant broken"
+          (* 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 @ [s; break_target])))
         ) else s (*no change*)
-      in ChangeDoChildrenPost(s, duplicate_and_rem_labels);
-    | _ -> DoChildren
+      | _ -> s
+    in
+    ChangeDoChildrenPost(s, duplicate_and_rem_labels)
 end
 
 let unroll_loops fd totalLoops =