Fix handling of labels in unrolling & add possibility to run CIL checks on CFGs

goblint.opam

@@ -74,7 +74,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#bfb977b48d6d92e0ecbdab2e04f2576095506107" ]
+  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#638a407306d3ce1646ef2536af173d9ba38cfd33" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # TODO: add back after release, only pinned for CI stability

goblint.opam.locked

@@ -124,7 +124,7 @@ available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   [
     "goblint-cil.2.0.0"
-    "git+https://github.com/goblint/cil.git#bfb977b48d6d92e0ecbdab2e04f2576095506107"
+    "git+https://github.com/goblint/cil.git#638a407306d3ce1646ef2536af173d9ba38cfd33"
   ]
   [
     "apron.v0.9.13"

goblint.opam.template

@@ -2,7 +2,7 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#bfb977b48d6d92e0ecbdab2e04f2576095506107" ]
+  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#638a407306d3ce1646ef2536af173d9ba38cfd33" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # TODO: add back after release, only pinned for CI stability

src/util/cilCfg.ml

@@ -45,4 +45,6 @@ let createCFG (fileAST: file) =
         computeCFGInfo fd true
       | _ -> ()
     );
+  if get_bool "dbg.run_cil_check" then assert (Check.checkFile [] fileAST);
+
   Cilfacade.do_preprocess fileAST

src/util/loopUnrolling.ml

@@ -446,9 +446,6 @@ class loopUnrollingVisitor(func) = object
           annotateArrays b;
           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
-
             (* 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 *)
@@ -464,10 +461,11 @@ class loopUnrollingVisitor(func) = object
             mkStmt (Block (mkBlock (copies@[s]@[break_target])))
           | _ -> failwith "invariant broken"
         ) else s (*no change*)
-      in ChangeDoChildrenPost({s with sid = s.sid},duplicate_and_rem_labels);
+      in ChangeDoChildrenPost(s, duplicate_and_rem_labels);
     | _ -> DoChildren
 end
 
 let unroll_loops fd =
+  Cil.populateLabelAlphaTable fd;
   let thisVisitor = new loopUnrollingVisitor(fd) in
-  ignore (visitCilFunction thisVisitor fd)
+  ignore (visitCilFunction thisVisitor fd)

src/util/options.schema.json

@@ -1803,6 +1803,13 @@
             "Should the analysis print information on which globals are protected by which mutex?",
           "type": "boolean",
           "default": false
+        },
+        "run_cil_check" : {
+          "title": "dbg.run_cil_check",
+          "description":
+            "Should the analysis call Check.checkFile after creating the CFG (helpful to verify that transformations respect CIL's invariants.",
+          "type": "boolean",
+          "default": false
         }
       },
       "additionalProperties": false

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

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --set exp.unrolling-factor 5
+// PARAM: --enable ana.int.interval --set exp.unrolling-factor 5 --enable dbg.run_cil_check
 #include <goblint.h>
 
 int global;
@@ -193,4 +193,4 @@ void example10(void)
 		++i;
 	}
 	return 0;
-}
+}

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

@@ -1,4 +1,4 @@
-// PARAM: --set exp.unrolling-factor 5
+// PARAM: --set exp.unrolling-factor 5  --enable dbg.run_cil_check
 #include <goblint.h>
 
 int main(void) {

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

@@ -1,4 +1,4 @@
-// PARAM: --set exp.unrolling-factor 5
+// PARAM: --set exp.unrolling-factor 5  --enable dbg.run_cil_check
 #include <goblint.h>
 
 int main(void) {

tests/regression/55-loop-unrolling/04-simple.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
+// 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
 // Simple example
 #include <goblint.h>
 

tests/regression/55-loop-unrolling/05-continue.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
+// 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
 // Simple example
 #include <goblint.h>
 

tests/regression/55-loop-unrolling/06-simple-cases-unrolled.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
+// 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
 #include <goblint.h>
 
 int global;

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
+// 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
 #include <goblint.h>
 int main(void) {
     int arr[10][10];

tests/regression/55-loop-unrolling/08-bad.c

@@ -0,0 +1,17 @@
+// PARAM: --set exp.unrolling-factor 1 --enable dbg.run_cil_check
+int main() {
+  int m;
+
+  switch (m)
+  {
+      default:
+      do { } while (0);
+  }
+
+
+  goto lab;
+
+  lab: do { } while (0);
+
+  return 0;
+}

tests/regression/55-loop-unrolling/09-weird.c

@@ -0,0 +1,14 @@
+// PARAM: --set exp.unrolling-factor 2 --enable dbg.run_cil_check
+#include <goblint.h>
+
+void main(void)
+{
+    int j = 0;
+
+    for(int i=0;i < 50;i++) {
+        goto somelab;
+        somelab: j = 8;
+    }
+
+    __goblint_check(j==8);
+}