Loop Unrolling for the first exp.unrolling-factor Iterations

src/util/cilfacade.ml

@@ -80,6 +80,51 @@ let end_basic_blocks f =
   let thisVisitor = new allBBVisitor in
   visitCilFileSameGlobals thisVisitor f
 
+class removeLabelsVisitor = object
+  inherit nopCilVisitor
+
+  val nestingDepth = ref 0
+
+  method! vstmt s =
+    let new_labels = List.filter_map (function Label(str,loc,b) -> None | x -> Some x) s.labels in
+    match s.skind with
+    | Loop _ -> nestingDepth := !nestingDepth+1; ChangeDoChildrenPost({s with labels = new_labels}, fun x -> nestingDepth := !nestingDepth-1; x)
+    | Continue loc -> if !nestingDepth = 0 then
+        ChangeTo({s with labels = new_labels; skind = Break loc})
+      else
+        ChangeTo({s with labels = new_labels})
+    | _ -> ChangeDoChildrenPost({s with labels = new_labels}, Fun.id)
+end
+
+class loopUnrollingVisitor = object
+  (* Labels are simply handled by removing them. It is always correct to simply jump into the non-unrolled part of the loop!          *)
+  (* The price we need to pay for this simpler handling of labels and still wanting to benefit from unrolling nested loops is that    *)
+  (* we need to put our unrolled code into fake while(1) loops such that breaks have something to break out of, add artificial breaks *)
+  (* at the end of loops, and replacing (top level!) continues with breaks. *)
+  (* This is still a lot more intuitive than complicated handling of gotos as would be required when doing it after the removal of breaks  *)
+  inherit nopCilVisitor
+
+  method! vstmt s =
+    let labelsRemover = new removeLabelsVisitor in
+    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) ->
+          let s = { s with sid = s.sid } in
+          let factor = GobConfig.get_int "exp.unrolling-factor" in
+          let bstmts = b.bstmts @ [mkStmt @@ Break loc] in
+          let copies = List.init (factor) (fun _ -> visitCilStmt labelsRemover (mkStmt (Loop (mkBlock bstmts,loc,loc2,None,None)))) in
+          mkStmt (Block (mkBlock (copies@[s])))
+        | _ -> failwith "invariant broken"
+      in
+      ChangeDoChildrenPost({s with sid = s.sid},duplicate_and_rem_labels)
+    | _ -> DoChildren
+end
+
+let loop_unrolling f =
+  let thisVisitor = new loopUnrollingVisitor in
+  visitCilFileSameGlobals thisVisitor f
 
 let visitors = ref []
 let register_preprocess name visitor_fun =
@@ -94,6 +139,7 @@ let do_preprocess ast =
   iterGlobals ast (function GFun (fd,_) -> List.iter (f fd) !visitors | _ -> ())
 
 let createCFG (fileAST: file) =
+  if (get_int "exp.unrolling-factor")>0 then loop_unrolling fileAST;
   (* The analyzer keeps values only for blocks. So if you want a value for every program point, each instruction      *)
   (* needs to be in its own block. end_basic_blocks does that.                                                        *)
   (* After adding support for VLAs, there are new VarDecl instructions at the point where a variable was declared and *)

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,13 @@
+int main(void) {
+	int r=5;
+    for (int i = 0; i < 2; ++i) {
+		switch (i) {
+		case 0:
+			break;
+		case 1:
+            r = 8;
+		}
+	}
+
+	return 0;
+}