Add cram tests for CFGs

.github/workflows/coverage.yml

@@ -38,6 +38,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test

.github/workflows/locked.yml

@@ -40,6 +40,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
@@ -114,6 +119,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install spin
         run: sudo apt-get -y install spin

.github/workflows/unlocked.yml

@@ -49,6 +49,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
         run: opam install . --deps-only --with-test
@@ -139,6 +144,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
         run: opam install . --deps-only --with-test
@@ -255,6 +265,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install Goblint with test
         run: opam install goblint --with-test

goblint.opam

@@ -78,10 +78,13 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ]
   # 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" ]
 ]
+depexts: [
+  ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]

goblint.opam.locked

@@ -134,10 +134,11 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.3"
-    "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51"
+    "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5"
   ]
   [
     "ppx_deriving.5.2.1"
     "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
   ]
 ]
+depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

goblint.opam.template

@@ -3,10 +3,13 @@
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ]
   # 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" ]
 ]
+depexts: [
+  ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]

src/common/framework/cfgTools.ml

@@ -619,6 +619,12 @@ let getCFG (file: file) : cfg * cfg * stmt list CfgEdgeH.t =
   if get_bool "justcfg" then fprint_hash_dot cfgB;
   (fun n -> H.find_default cfgF n []), (fun n -> H.find_default cfgB n []), skippedByEdge
 
+let compute_cfg_skips file =
+  let cfgF, cfgB, skippedByEdge = getCFG file in
+  (module struct let prev = cfgB let next = cfgF end : CfgBidir), skippedByEdge
+
+let compute_cfg file = fst (compute_cfg_skips file)
+
 
 let iter_fd_edges (module Cfg : CfgBackward) fd =
   let ready      = NH.create 113 in

src/common/util/cilCfg0.ml

@@ -0,0 +1,24 @@
+(** CIL CFG functions to avoid dependency problems. *)
+
+open GoblintCil
+
+class allBBVisitor = object (* puts every instruction into its own basic block *)
+  inherit nopCilVisitor
+  method! vstmt s =
+    match s.skind with
+    | Instr(il) ->
+      let list_of_stmts =
+        List.map (fun one_inst -> mkStmtOneInstr one_inst) il in
+      let block = mkBlock list_of_stmts in
+      ChangeDoChildrenPost(s, (fun _ -> s.skind <- Block(block); s))
+    | _ -> DoChildren
+
+  method! vvdec _ = SkipChildren
+  method! vexpr _ = SkipChildren
+  method! vlval _ = SkipChildren
+  method! vtype _ = SkipChildren
+end
+
+let end_basic_blocks f =
+  let thisVisitor = new allBBVisitor in
+  visitCilFileSameGlobals thisVisitor f

src/common/util/cilLocation.ml

@@ -0,0 +1,45 @@
+open GoblintCil
+
+type locs = {
+  loc: location;
+  eloc: location;
+}
+
+let get_labelLoc = function
+  | Label (_, loc, _) -> {loc; eloc = locUnknown}
+  | Case (_, loc, eloc) -> {loc; eloc}
+  | CaseRange (_, _, loc, eloc) -> {loc; eloc}
+  | Default (loc, eloc) -> {loc; eloc}
+
+(* TODO: need get_labelsLoc? *)
+
+(** Following functions are similar to [Cil] versions, but return expression location instead of entire statement location, where possible. *)
+(* Ideally we would have both copies of the functions available, but UpdateCil would have to be adapted per-stmtkind/instr to store and update either one or two locations. *)
+
+(** Get locations for {!Cil.instr}. *)
+let get_instrLoc = function
+  | Set (_, _, loc, eloc) -> {loc; eloc}
+  | Call (_, _, _, loc, eloc) -> {loc; eloc}
+  | Asm (_, _, _, _, _, loc) -> {loc; eloc = locUnknown}
+  | VarDecl (_, loc) -> {loc; eloc = locUnknown}
+
+(** Get locations for {!Cil.stmt}. *)
+(* confusingly {!Cil.get_stmtLoc} works on stmtkind instead *)
+let rec get_stmtLoc stmt: locs =
+  match stmt.skind with
+  (* no stmtkind/instr location in these cases, so try labels instead *)
+  | Instr []
+  | Block {bstmts = []; _} ->
+    (* get_labelsLoc stmt.labels *)
+    {loc = locUnknown; eloc = locUnknown}
+
+  | Instr (hd :: _) -> get_instrLoc hd
+  | Return (_, loc) -> {loc; eloc = locUnknown}
+  | Goto (_, loc) -> {loc; eloc = locUnknown}
+  | ComputedGoto (_, loc) -> {loc; eloc = locUnknown}
+  | Break loc -> {loc; eloc = locUnknown}
+  | Continue loc -> {loc; eloc = locUnknown}
+  | If (_, _, _, loc, eloc) -> {loc; eloc}
+  | Switch (_, _, _, loc, eloc) -> {loc; eloc}
+  | Loop (_, loc, eloc, _, _) -> {loc; eloc}
+  | Block {bstmts = hd :: _; _} -> get_stmtLoc hd

src/framework/control.ml

@@ -806,15 +806,9 @@ let rec analyze_loop (module CFG : CfgBidir) file fs change_info skippedByEdge =
     (* TODO: do some more incremental refinement and reuse parts of solution *)
     analyze_loop (module CFG) file fs change_info skippedByEdge
 
-let compute_cfg_skips file =
-  let cfgF, cfgB, skippedByEdge = CfgTools.getCFG file in
-  (module struct let prev = cfgB let next = cfgF end : CfgBidir), skippedByEdge
-
-let compute_cfg = fst % compute_cfg_skips
-
 (** The main function to perform the selected analyses. *)
 let analyze change_info (file: file) fs =
   Logs.debug "Generating the control flow graph.";
-  let (module CFG), skippedByEdge = compute_cfg_skips file in
+  let (module CFG), skippedByEdge = CfgTools.compute_cfg_skips file in
   MyCFG.current_cfg := (module CFG);
   analyze_loop (module CFG) file fs change_info skippedByEdge

src/util/cilCfg.ml

@@ -3,26 +3,7 @@
 open GobConfig
 open GoblintCil
 
-class allBBVisitor = object (* puts every instruction into its own basic block *)
-  inherit nopCilVisitor
-  method! vstmt s =
-    match s.skind with
-    | Instr(il) ->
-      let list_of_stmts =
-        List.map (fun one_inst -> mkStmtOneInstr one_inst) il in
-      let block = mkBlock list_of_stmts in
-      ChangeDoChildrenPost(s, (fun _ -> s.skind <- Block(block); s))
-    | _ -> DoChildren
-
-  method! vvdec _ = SkipChildren
-  method! vexpr _ = SkipChildren
-  method! vlval _ = SkipChildren
-  method! vtype _ = SkipChildren
-end
-
-let end_basic_blocks f =
-  let thisVisitor = new allBBVisitor in
-  visitCilFileSameGlobals thisVisitor f
+include CilCfg0
 
 
 class countLoopsVisitor(count) = object

tests/regression/00-sanity/19-if-0.t

@@ -0,0 +1,33 @@
+  $ cfgDot 19-if-0.c
+
+  $ graph-easy --as=boxart main.dot
+                                                   ┌────────────────────────┐
+                                                   │ main()                 │
+                                                   └────────────────────────┘
+                                                     │
+                                                     │ (body)
+                                                     ▼
+  ┌────────────────────────┐                       ┌────────────────────────┐
+  │ 19-if-0.c:15:9-15:27   │  Neg(0)               │ 19-if-0.c:9:5-16:5     │
+  │ (19-if-0.c:15:9-15:27) │ ◀──────────────────── │ (19-if-0.c:9:9-9:10)   │
+  └────────────────────────┘                       └────────────────────────┘
+    │                                                │
+    │                                                │ Pos(0)
+    │                                                ▼
+    │                                              ┌────────────────────────┐
+    │                                              │ 19-if-0.c:11:9-11:16   │
+    │                                              │ (19-if-0.c:11:9-11:16) │
+    │                                              └────────────────────────┘
+    │                                                │
+    │                                                │ stuff()
+    │                                                ▼
+    │                                              ┌────────────────────────┐
+    │                        __goblint_check(1)    │ 19-if-0.c:17:5-17:13   │
+    └────────────────────────────────────────────▶ │ (unknown)              │
+                                                   └────────────────────────┘
+                                                     │
+                                                     │ return 0
+                                                     ▼
+                                                   ┌────────────────────────┐
+                                                   │ return of main()       │
+                                                   └────────────────────────┘

tests/regression/00-sanity/20-if-0-realnode.t

@@ -0,0 +1,35 @@
+  $ cfgDot 20-if-0-realnode.c
+
+  $ graph-easy --as=boxart main.dot
+  ┌─────────────────────────────────┐
+  │ main()                          │
+  └─────────────────────────────────┘
+    │
+    │ (body)
+    ▼
+  ┌─────────────────────────────────┐
+  │ 20-if-0-realnode.c:8:5-14:5     │   Neg(0)
+  │ (20-if-0-realnode.c:8:9-8:10)   │ ─────────┐
+  │ [20-if-0-realnode.c:7:5-8:5     │          │
+  │ (unknown)]                      │ ◀────────┘
+  └─────────────────────────────────┘
+    │
+    │ Pos(0)
+    ▼
+  ┌─────────────────────────────────┐
+  │ 20-if-0-realnode.c:10:9-10:16   │
+  │ (20-if-0-realnode.c:10:9-10:16) │
+  └─────────────────────────────────┘
+    │
+    │ stuff()
+    ▼
+  ┌─────────────────────────────────┐
+  │ 20-if-0-realnode.c:15:5-15:13   │
+  │ (unknown)                       │
+  └─────────────────────────────────┘
+    │
+    │ return 0
+    ▼
+  ┌─────────────────────────────────┐
+  │ return of main()                │
+  └─────────────────────────────────┘