Loop Unrolling for the first exp.unrolling-factor Iterations

src/util/cilfacade.ml

@@ -80,6 +80,118 @@ let end_basic_blocks f =
   let thisVisitor = new allBBVisitor in
   visitCilFileSameGlobals thisVisitor f
 
+(* replaces goto s with goto s' when newtarget s = Some s' IN PLACE *)
+class patchLabelsGotosVisitor(newtarget) = object
+  inherit nopCilVisitor
+
+  method! vstmt s =
+    match s.skind with
+    | Goto (target,loc) ->
+      (match newtarget !target with
+       | None -> SkipChildren
+       | Some nt -> s.skind <- Goto (ref nt, loc); DoChildren)
+    | _ -> DoChildren
+end
+
+(* Hashtable used to patch gotos later *)
+module StatementHashTable = Hashtbl.Make(struct
+    type t = stmt
+    (* Identity by physical equality. *)
+    let equal = (==)
+    let hash = Hashtbl.hash
+  end)
+
+(*
+  Makes a copy, replacing top-level breaks with goto loopEnd and top-level continues with
+  goto currentIterationEnd
+  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
+  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 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*)
+      let new_s = {sn with labels = new_labels} in
+      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 *)
+        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)
+      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)
+      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
+
+class loopUnrollingVisitor = 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 =
+        match s.skind with
+        | Loop (b,loc, loc2, break , continue) ->
+          (* We copy the statement to later be able to modify it without worrying about invariants *)
+          let s = { s with sid = s.sid } in
+          let factor = GobConfig.get_int "exp.unrolling-factor" in
+          (* 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"
+      in
+      ChangeDoChildrenPost({s with sid = s.sid},duplicate_and_rem_labels)
+    | _ -> DoChildren
+end
+
+let loop_unrolling fd =
+  let thisVisitor = new loopUnrollingVisitor in
+  ignore (visitCilFunction thisVisitor fd)
 
 let visitors = ref []
 let register_preprocess name visitor_fun =
@@ -110,6 +222,8 @@ let createCFG (fileAST: file) =
   iterGlobals fileAST (fun glob ->
       match glob with
       | GFun(fd,_) ->
+        (* before prepareCfg so continues still appear as such *)
+        if (get_int "exp.unrolling-factor")>0 then loop_unrolling fd;
         prepareCFG fd;
         computeCFGInfo fd true
       | _ -> ()

src/util/options.schema.json

@@ -1312,6 +1312,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

tests/regression/55-loop-unrolling/01-simple-cases.c

@@ -0,0 +1,194 @@
+// PARAM: --set solver td3 --enable ana.int.interval --set exp.unrolling-factor 5
+int global;
+
+int main(void)
+{
+    example1();
+    example2();
+    example3();
+    example4();
+    example5();
+    example6();
+    example7();
+    example8();
+    example9();
+    example10();
+    return 0;
+}
+
+// Simple example
+void example1(void)
+{
+    int a[5];
+    int i = 0;
+
+    while (i < 5) {
+        a[i] = i;
+        i++;
+    }
+
+    assert(a[0] == 0); // UNKNOWN
+    assert(a[3] == 3); // UNKNOWN
+}
+
+// Do-while loop simple example
+void example2(void)
+{
+    int a[5];
+    int i = 0;
+
+    do {
+        a[i] = i;
+        i++;
+    } while (i<=5);
+
+    assert(a[0] == 0); // UNKNOWN
+    assert(a[3] == 3); // UNKNOWN
+}
+
+// Initialization not completed, yet the array representation is not precise
+void example3(void)
+{
+    int a[10];
+    int i = 0;
+
+    while (i < 5) {
+        a[i] = i;
+        i++;
+    }
+
+    assert(a[0] == 0); // UNKNOWN
+    assert(a[3] == 0); // UNKNOWN
+    assert(a[7] == 0); // UNKNOWN
+}
+
+// Example with increased precision. Goblint detects in which iteration it is during the unrolled part.
+void example4(void)
+{
+    int a[10];
+    int i = 0;
+    int first_iteration = 1;
+
+    while (i < 10) {
+        if (first_iteration == 1) assert(i==0);
+        else if (i > 5) assert(i == 6); // UNKNOWN
+        first_iteration = 0;
+        a[i] = 0;
+        i++;
+    }
+
+    assert(a[0] == 0);
+    assert(first_iteration == 0);
+}
+
+
+// Example where the precision increase can be appreciated by a variable that 
+// is modified in the loop other than the ones used in the loop head
+void example5(void)
+{
+    int a[4];
+    int i = 0;
+    int top = 0;
+
+    while (i < 4) {
+        a[i] = 0;
+        top += i;
+        if(i==2){
+            assert(top == 3);
+        }
+        else{
+            assert(top == 3); // FAIL
+        }
+        i++;
+    }
+
+    assert(a[0] == 0);
+    assert(a[3] == 0);
+    assert(top == 6);
+}
+
+// Loop has less iterations than the unrolling factor
+void example6(void)
+{
+    int a[5];
+    int i = 0;
+    int top = 0;
+
+    while (i < 3) {
+        a[i] = 0;
+        assert(a[0]==0);
+        i++;
+    }
+
+    assert(a[0] == 0);
+    assert(a[3] == 0);
+    assert(top == 6); // FAIL
+}
+
+// There is a call on the loop's condition
+int update(int i) {
+    if (i>5){
+        return 0;
+    }
+    else{
+        return 1;
+    }
+}
+void example7(void)
+{
+    int a[10];
+	int i = 0;
+	while(update(i)){
+		a[i] = i;
+		++i;
+	}
+    assert(a[0] == 0); //UNKNOWN
+    assert(a[6] == 0); //UNKNOWN
+}
+
+// nested loops
+void example8(void)
+{
+    int a[5];
+    int b[] = {0,0,0,0,0};
+	int i = 0;
+	while(i < 5){
+		a[i] = i;
+        int j = 0;
+        while(j < 5){
+            b[j] += a[i];
+            ++j;
+        }
+		++i;
+	}
+	return 0;
+}
+
+// example with loop like the ones CIL does internally (while(1) + break)
+void example9(void)
+{
+    int a[5];
+	int i = 0;
+	while(1){
+		a[i] = i;
+		++i;
+		if (i == 5) break;
+	}
+	return 0;
+}
+
+// example with loop containing a "continue" instruction
+void example10(void)
+{
+    int a[5];
+	int i = 0;
+	while(i<5){
+		if (i == 3) {
+			i++;
+			continue;
+		}
+		a[i] = i;
+		++i;
+	}
+	return 0;
+}

tests/regression/55-loop-unrolling/02-break.c

@@ -0,0 +1,17 @@
+// PARAM: --set exp.unrolling-factor 5
+int main(void) {
+	int r=5;
+    for (int i = 0; i < 2; ++i) {
+		switch (i) {
+		case 0:
+			break;
+		case 1:
+            r = 8;
+		}
+		r = 17;
+		break;
+	}
+
+	assert(r==17);
+	return 0;
+}

tests/regression/55-loop-unrolling/03-break-right-place.c

@@ -0,0 +1,18 @@
+// PARAM: --set exp.unrolling-factor 5
+#include<assert.h>
+
+int main(void) {
+    int i = 0;
+    int j = 0;
+
+    while(i< 17) {
+        if (j==0) {
+            j = 1;
+            // the break is not just out of this unrolling, but out of the entire loop!
+            break;
+        }
+        i++;
+    }
+
+    assert(i == 0);
+}

tests/regression/55-loop-unrolling/04-simple.c

@@ -0,0 +1,15 @@
+// PARAM: --set solver td3 --enable ana.int.interval --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5
+// Simple example
+void main(void)
+{
+    int a[5];
+    int i = 0;
+
+    while (i < 5) {
+        a[i] = i;
+        i++;
+    }
+
+    assert(a[0] == 0);
+    assert(a[3] == 3); 
+}