diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 4b47a66e15..3d02f33dc5 100644 --- a/.github/workflows/coverage.yml +++ b/.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 diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml index 8e6e1bccb3..505384f672 100644 --- a/.github/workflows/locked.yml +++ b/.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 diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml index b1719c4edf..6ef35fb176 100644 --- a/.github/workflows/unlocked.yml +++ b/.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 diff --git a/goblint.opam b/goblint.opam index a81d3f29e6..d7724aad34 100644 --- a/goblint.opam +++ b/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"} ] diff --git a/goblint.opam.locked b/goblint.opam.locked index c55b97928f..2bb831d6ba 100644 --- a/goblint.opam.locked +++ b/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} diff --git a/goblint.opam.template b/goblint.opam.template index 8289cd4e2f..1364586310 100644 --- a/goblint.opam.template +++ b/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"} ] diff --git a/gobview b/gobview index 543c48f143..b5ab4dbd7b 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit 543c48f143532a024c75001a176792acacc9421c +Subproject commit b5ab4dbd7b1b1dc4f0bf2a912012cb1879f54903 diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml index 77460f9f41..6a2540fd18 100644 --- a/src/common/framework/cfgTools.ml +++ b/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 diff --git a/src/common/util/cilCfg0.ml b/src/common/util/cilCfg0.ml new file mode 100644 index 0000000000..d48884135f --- /dev/null +++ b/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 diff --git a/src/common/util/cilLocation.ml b/src/common/util/cilLocation.ml new file mode 100644 index 0000000000..23c1b8df5b --- /dev/null +++ b/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 diff --git a/src/framework/control.ml b/src/framework/control.ml index 4349b881d0..6e8e5b7fc4 100644 --- a/src/framework/control.ml +++ b/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 diff --git a/src/util/cilCfg.ml b/src/util/cilCfg.ml index df766d5bdd..d6e74fc8af 100644 --- a/src/util/cilCfg.ml +++ b/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 diff --git a/tests/regression/00-sanity/19-if-0.t b/tests/regression/00-sanity/19-if-0.t new file mode 100644 index 0000000000..f847d75446 --- /dev/null +++ b/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() │ + └────────────────────────┘ diff --git a/tests/regression/00-sanity/20-if-0-realnode.t b/tests/regression/00-sanity/20-if-0-realnode.t new file mode 100644 index 0000000000..06a0bba865 --- /dev/null +++ b/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() │ + └─────────────────────────────────┘ diff --git a/tests/regression/00-sanity/21-empty-loops.t b/tests/regression/00-sanity/21-empty-loops.t new file mode 100644 index 0000000000..202a4d1071 --- /dev/null +++ b/tests/regression/00-sanity/21-empty-loops.t @@ -0,0 +1,401 @@ + $ cfgDot 21-empty-loops.c + + $ graph-easy --as=boxart f_empty_goto_loop.dot + ┌───────────────────────────────┐ + │ f_empty_goto_loop() │ + └───────────────────────────────┘ + │ + │ (body) + ▼ + ┌───────────────────────────────┐ + │ 21-empty-loops.c:57:3-57:31 │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:56:1-57:3 │ │ + │ (unknown)] │ ◀──────┘ + └───────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌───────────────────────────────┐ + │ 21-empty-loops.c:58:1-58:1 │ + │ (unknown) │ + └───────────────────────────────┘ + │ + │ return + ▼ + ┌───────────────────────────────┐ + │ return of f_empty_goto_loop() │ + └───────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_while_loop.dot + ┌────────────────────────────────────────────┐ + │ f_empty_while_loop() │ + └────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌────────────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:62:3-62:14 (synthetic) │ ─────────┐ + │ (21-empty-loops.c:62:10-62:11 (synthetic)) │ │ + │ │ ◀────────┘ + └────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌────────────────────────────────────────────┐ + │ 21-empty-loops.c:63:1-63:1 │ + │ (unknown) │ + └────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌────────────────────────────────────────────┐ + │ return of f_empty_while_loop() │ + └────────────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_goto_loop_suffix.dot + ┌──────────────────────────────────────┐ + │ 21-empty-loops.c:75:3-75:11 │ + │ (21-empty-loops.c:75:3-75:11) │ + └──────────────────────────────────────┘ + │ + │ suffix() + ▼ + ┌──────────────────────────────────────┐ + │ 21-empty-loops.c:76:1-76:1 │ + │ (unknown) │ ◀┐ + └──────────────────────────────────────┘ │ + │ │ + │ return │ + ▼ │ + ┌──────────────────────────────────────┐ │ + │ return of f_empty_goto_loop_suffix() │ │ + └──────────────────────────────────────┘ │ + ┌──────────────────────────────────────┐ │ Neg(1) + │ f_empty_goto_loop_suffix() │ │ + └──────────────────────────────────────┘ │ + │ │ + │ (body) │ + ▼ │ + ┌──────────────────────────────────────┐ │ + skip │ 21-empty-loops.c:73:3-73:38 │ │ + ┌─────── │ (unknown) │ │ + │ │ [21-empty-loops.c:72:1-73:3 │ │ + └──────▶ │ (unknown)] │ ─┘ + └──────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_while_loop_suffix.dot + ┌────────────────────────────────────────────┐ + │ f_empty_while_loop_suffix() │ + └────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌────────────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:80:3-80:14 (synthetic) │ ─────────┐ + │ (21-empty-loops.c:80:10-80:11 (synthetic)) │ │ + │ │ ◀────────┘ + └────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌────────────────────────────────────────────┐ + │ 21-empty-loops.c:82:3-82:11 │ + │ (21-empty-loops.c:82:3-82:11) │ + └────────────────────────────────────────────┘ + │ + │ suffix() + ▼ + ┌────────────────────────────────────────────┐ + │ 21-empty-loops.c:83:1-83:1 │ + │ (unknown) │ + └────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌────────────────────────────────────────────┐ + │ return of f_empty_while_loop_suffix() │ + └────────────────────────────────────────────┘ + + $ graph-easy --as=boxart f_nonempty_goto_loop.dot + ┌──────────────────────────────────┐ + │ f_nonempty_goto_loop() │ + └──────────────────────────────────┘ + │ + │ (body) + ▼ + ┌──────────────────────────────────┐ body() + │ 21-empty-loops.c:93:3-93:9 │ ─────────┐ + │ (21-empty-loops.c:93:3-93:9) │ │ + │ │ ◀────────┘ + └──────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌──────────────────────────────────┐ + │ 21-empty-loops.c:95:1-95:1 │ + │ (unknown) │ + └──────────────────────────────────┘ + │ + │ return + ▼ + ┌──────────────────────────────────┐ + │ return of f_nonempty_goto_loop() │ + └──────────────────────────────────┘ + + $ graph-easy --as=boxart f_nonempty_while_loop.dot + + ┌───────────────────────────────────────────────────────────────────────────────────────────┐ + │ │ + │ ┌────────────────────────────────────────────┐ │ + │ │ f_nonempty_while_loop() │ │ + │ └────────────────────────────────────────────┘ │ + │ │ │ body() + │ │ (body) │ + │ ▼ │ + ┌─────────────────────────────────┐ ┌────────────────────────────────────────────┐ │ + │ 21-empty-loops.c:101:5-101:11 │ Pos(1) │ 21-empty-loops.c:99:3-102:3 (synthetic) │ │ + │ (21-empty-loops.c:101:5-101:11) │ ◀──────── │ (21-empty-loops.c:99:10-99:11 (synthetic)) │ ◀┘ + └─────────────────────────────────┘ └────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌────────────────────────────────────────────┐ + │ 21-empty-loops.c:103:1-103:1 │ + │ (unknown) │ + └────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌────────────────────────────────────────────┐ + │ return of f_nonempty_while_loop() │ + └────────────────────────────────────────────┘ + + + $ graph-easy --as=boxart f_empty_goto_loop_prefix.dot + ┌──────────────────────────────────────┐ + │ f_empty_goto_loop_prefix() │ + └──────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌──────────────────────────────────────┐ + │ 21-empty-loops.c:112:3-112:11 │ + │ (21-empty-loops.c:112:3-112:11) │ + └──────────────────────────────────────┘ + │ + │ prefix() + ▼ + ┌──────────────────────────────────────┐ + │ 21-empty-loops.c:115:3-115:38 │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:114:1-115:3 │ │ + │ (unknown)] │ ◀──────┘ + └──────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌──────────────────────────────────────┐ + │ 21-empty-loops.c:116:1-116:1 │ + │ (unknown) │ + └──────────────────────────────────────┘ + │ + │ return + ▼ + ┌──────────────────────────────────────┐ + │ return of f_empty_goto_loop_prefix() │ + └──────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_while_loop_prefix.dot + ┌──────────────────────────────────────────────┐ + │ f_empty_while_loop_prefix() │ + └──────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌──────────────────────────────────────────────┐ + │ 21-empty-loops.c:120:3-120:11 │ + │ (21-empty-loops.c:120:3-120:11) │ + └──────────────────────────────────────────────┘ + │ + │ prefix() + ▼ + ┌──────────────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:122:3-122:14 (synthetic) │ ─────────┐ + │ (21-empty-loops.c:122:10-122:11 (synthetic)) │ │ + │ │ ◀────────┘ + └──────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌──────────────────────────────────────────────┐ + │ 21-empty-loops.c:123:1-123:1 │ + │ (unknown) │ + └──────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌──────────────────────────────────────────────┐ + │ return of f_empty_while_loop_prefix() │ + └──────────────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_goto_loop_semicolon.dot + ┌─────────────────────────────────────────┐ + │ f_empty_goto_loop_semicolon() │ + └─────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────┐ + │ unknown │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:127:1-128:3 │ │ + │ (unknown)] │ ◀──────┘ + └─────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────┐ + │ 21-empty-loops.c:131:1-131:1 │ + │ (unknown) │ + └─────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────┐ + │ return of f_empty_goto_loop_semicolon() │ + └─────────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_while_loop_semicolon.dot + ┌──────────────────────────────────────────────┐ + │ f_empty_while_loop_semicolon() │ + └──────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌──────────────────────────────────────────────┐ Pos(1) + │ 21-empty-loops.c:135:3-137:3 (synthetic) │ ─────────┐ + │ (21-empty-loops.c:135:10-135:11 (synthetic)) │ │ + │ │ ◀────────┘ + └──────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌──────────────────────────────────────────────┐ + │ 21-empty-loops.c:138:1-138:1 │ + │ (unknown) │ + └──────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌──────────────────────────────────────────────┐ + │ return of f_empty_while_loop_semicolon() │ + └──────────────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_goto_loop_multiple.dot + ┌────────────────────────────────────────┐ + │ f_empty_goto_loop_multiple() │ + └────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌────────────────────────────────────────┐ + │ 21-empty-loops.c:143:3-143:42 │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:142:1-143:3 │ │ + │ (unknown)] │ ◀──────┘ + └────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌────────────────────────────────────────┐ + │ 21-empty-loops.c:146:1-146:1 │ + │ (unknown) │ + └────────────────────────────────────────┘ + │ + │ return + ▼ + ┌────────────────────────────────────────┐ + │ return of f_empty_goto_loop_multiple() │ + └────────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_goto_loop_multiple_semicolon_first.dot + ┌────────────────────────────────────────────────────────┐ + │ f_empty_goto_loop_multiple_semicolon_first() │ + └────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌────────────────────────────────────────────────────────┐ + │ unknown │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:150:1-151:3 │ │ + │ (unknown)] │ ◀──────┘ + └────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:155:1-155:1 │ + │ (unknown) │ + └────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌────────────────────────────────────────────────────────┐ + │ return of f_empty_goto_loop_multiple_semicolon_first() │ + └────────────────────────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_goto_loop_multiple_semicolon_second.dot + ┌─────────────────────────────────────────────────────────┐ + │ f_empty_goto_loop_multiple_semicolon_second() │ + └─────────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:160:3-160:59 │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:159:1-160:3 │ │ + │ (unknown)] │ ◀──────┘ + └─────────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:164:1-164:1 │ + │ (unknown) │ + └─────────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌─────────────────────────────────────────────────────────┐ + │ return of f_empty_goto_loop_multiple_semicolon_second() │ + └─────────────────────────────────────────────────────────┘ + + $ graph-easy --as=boxart f_empty_goto_loop_multiple_semicolon_both.dot + ┌───────────────────────────────────────────────────────┐ + │ f_empty_goto_loop_multiple_semicolon_both() │ + └───────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌───────────────────────────────────────────────────────┐ + │ unknown │ skip + │ (unknown) │ ───────┐ + │ [21-empty-loops.c:168:1-169:3 │ │ + │ (unknown)] │ ◀──────┘ + └───────────────────────────────────────────────────────┘ + │ + │ Neg(1) + ▼ + ┌───────────────────────────────────────────────────────┐ + │ 21-empty-loops.c:174:1-174:1 │ + │ (unknown) │ + └───────────────────────────────────────────────────────┘ + │ + │ return + ▼ + ┌───────────────────────────────────────────────────────┐ + │ return of f_empty_goto_loop_multiple_semicolon_both() │ + └───────────────────────────────────────────────────────┘ diff --git a/tests/regression/00-sanity/dune b/tests/regression/00-sanity/dune index 23c0dd3290..d6e0ac7094 100644 --- a/tests/regression/00-sanity/dune +++ b/tests/regression/00-sanity/dune @@ -1,2 +1,8 @@ (cram (deps (glob_files *.c))) + +(cram + (applies_to 19-if-0 20-if-0-realnode 21-empty-loops) + (enabled_if %{bin-available:graph-easy}) + (deps + %{bin:cfgDot})) diff --git a/tests/regression/cfg/dune b/tests/regression/cfg/dune new file mode 100644 index 0000000000..c91c970cd9 --- /dev/null +++ b/tests/regression/cfg/dune @@ -0,0 +1,9 @@ +(env + (_ + (binaries ./util/cfgDot.exe))) + +(cram + (applies_to :whole_subtree) + (enabled_if %{bin-available:graph-easy}) + (deps + %{bin:cfgDot})) diff --git a/tests/regression/cfg/foo.t/foo.c b/tests/regression/cfg/foo.t/foo.c new file mode 100644 index 0000000000..597e0457f2 --- /dev/null +++ b/tests/regression/cfg/foo.t/foo.c @@ -0,0 +1,8 @@ +int main() { + int a = 1, b = 1; + while (a > 0 && b) { + a++; + b--; + } + return 0; +} diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t new file mode 100644 index 0000000000..a9f91bf4a6 --- /dev/null +++ b/tests/regression/cfg/foo.t/run.t @@ -0,0 +1,48 @@ + $ cfgDot foo.c + + $ graph-easy --as=boxart main.dot + ┌───────────────────────────────┐ + │ main() │ + └───────────────────────────────┘ + │ + │ (body) + ▼ + ┌───────────────────────────────┐ + │ foo.c:2:7-2:12 │ + │ (foo.c:2:7-2:12) │ + └───────────────────────────────┘ + │ + │ a = 1 + ▼ + ┌───────────────────────────────┐ + │ foo.c:2:14-2:19 │ + │ (foo.c:2:14-2:19) │ + └───────────────────────────────┘ + │ + │ b = 1 + ▼ + ┌──────────────────┐ ┌───────────────────────────────┐ + │ foo.c:7:3-7:11 │ Neg(a > 0) │ foo.c:3:3-6:3 (synthetic) │ + ┌──────▶ │ (unknown) │ ◀──────────── │ (foo.c:3:10-3:20 (synthetic)) │ ◀┐ + │ └──────────────────┘ └───────────────────────────────┘ │ + │ │ │ │ + │ │ return 0 │ Pos(a > 0) │ + │ ▼ ▼ │ + │ Neg(b) ┌──────────────────┐ ┌───────────────────────────────┐ │ + │ │ return of main() │ │ foo.c:3:3-6:3 (synthetic) │ │ + │ │ │ ┌─────────── │ (foo.c:3:10-3:20 (synthetic)) │ │ + │ └──────────────────┘ │ └───────────────────────────────┘ │ + │ │ │ │ + └──────────────────────────────┘ │ Pos(b) │ b = b - 1 + ▼ │ + ┌───────────────────────────────┐ │ + │ foo.c:4:5-4:8 │ │ + │ (foo.c:4:5-4:8) │ │ + └───────────────────────────────┘ │ + │ │ + │ a = a + 1 │ + ▼ │ + ┌───────────────────────────────┐ │ + │ foo.c:5:5-5:8 │ │ + │ (foo.c:5:5-5:8) │ ─┘ + └───────────────────────────────┘ diff --git a/tests/regression/cfg/issue-1356.t/issue-1356.c b/tests/regression/cfg/issue-1356.t/issue-1356.c new file mode 100644 index 0000000000..b773f6cf66 --- /dev/null +++ b/tests/regression/cfg/issue-1356.t/issue-1356.c @@ -0,0 +1,20 @@ +extern int __VERIFIER_nondet_int(void); + +extern void abort(void); +void assume_abort_if_not(int cond) { + if(!cond) {abort();} +} + +int minus(int a, int b) { + assume_abort_if_not(b <= 0 || a >= b - 2147483648); // there shouldn't be invariants 1 <= b and b != 0 before this line + assume_abort_if_not(b >= 0 || a <= b + 2147483647); // there shouldn't be invariants b <= -1 and b != 0 before this line + return a - b; +} + +int main() { + int x, y; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + minus(x, y); + return 0; +} diff --git a/tests/regression/cfg/issue-1356.t/run.t b/tests/regression/cfg/issue-1356.t/run.t new file mode 100644 index 0000000000..78a81aff68 --- /dev/null +++ b/tests/regression/cfg/issue-1356.t/run.t @@ -0,0 +1,78 @@ + $ cfgDot issue-1356.c + + $ graph-easy --as=boxart minus.dot + + ┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ + │ │ + │ ┌─────────────────────────────────────────┐ │ + │ │ minus() │ │ + │ └─────────────────────────────────────────┘ │ + │ │ │ + │ Pos((long )a >= (long )b - 2147483648) │ (body) │ + ▼ ▼ │ + ┌─────────────────────────────────────────┐ ┌─────────────────────────────────────────┐ │ + │ issue-1356.c:9:3-9:53 (synthetic) │ Pos(b <= 0) │ issue-1356.c:9:3-9:53 │ │ + │ (issue-1356.c:9:3-9:53 (synthetic)) │ ◀────────────────────────── │ (issue-1356.c:9:3-9:53) │ │ + └─────────────────────────────────────────┘ └─────────────────────────────────────────┘ │ + │ │ │ + │ │ Neg(b <= 0) │ + │ ▼ │ + │ ┌─────────────────────────────────────────┐ │ + │ │ issue-1356.c:9:3-9:53 (synthetic) │ │ + │ │ (issue-1356.c:9:3-9:53 (synthetic)) │ ─┘ + │ └─────────────────────────────────────────┘ + │ │ + │ │ Neg((long )a >= (long )b - 2147483648) + │ ▼ + │ ┌─────────────────────────────────────────┐ + │ │ issue-1356.c:9:3-9:53 (synthetic) │ + │ │ (issue-1356.c:9:3-9:53 (synthetic)) │ + │ └─────────────────────────────────────────┘ + │ │ + │ │ tmp = 0 + │ ▼ + │ ┌─────────────────────────────────────────┐ + │ tmp = 1 │ issue-1356.c:9:3-9:53 (synthetic) │ + └───────────────────────────────────────────────────────────────────▶ │ (issue-1356.c:9:3-9:53 (synthetic)) │ + └─────────────────────────────────────────┘ + │ + │ assume_abort_if_not(tmp) + ▼ + ┌─────────────────────────────────────────┐ + │ issue-1356.c:10:3-10:53 │ + │ (issue-1356.c:10:3-10:53) │ ─┐ + └─────────────────────────────────────────┘ │ + │ │ + │ Neg(b >= 0) │ + ▼ │ + ┌─────────────────────────────────────────┐ ┌─────────────────────────────────────────┐ │ + │ issue-1356.c:10:3-10:53 (synthetic) │ Neg(a <= b + 2147483647) │ issue-1356.c:10:3-10:53 (synthetic) │ │ + │ (issue-1356.c:10:3-10:53 (synthetic)) │ ◀────────────────────────── │ (issue-1356.c:10:3-10:53 (synthetic)) │ │ Pos(b >= 0) + └─────────────────────────────────────────┘ └─────────────────────────────────────────┘ │ + │ │ │ + │ │ Pos(a <= b + 2147483647) │ + │ ▼ │ + │ ┌─────────────────────────────────────────┐ │ + │ │ issue-1356.c:10:3-10:53 (synthetic) │ │ + │ │ (issue-1356.c:10:3-10:53 (synthetic)) │ ◀┘ + │ └─────────────────────────────────────────┘ + │ │ + │ │ tmp___0 = 1 + │ ▼ + │ ┌─────────────────────────────────────────┐ + │ tmp___0 = 0 │ issue-1356.c:10:3-10:53 (synthetic) │ + └───────────────────────────────────────────────────────────────────▶ │ (issue-1356.c:10:3-10:53 (synthetic)) │ + └─────────────────────────────────────────┘ + │ + │ assume_abort_if_not(tmp___0) + ▼ + ┌─────────────────────────────────────────┐ + │ issue-1356.c:11:3-11:15 │ + │ (unknown) │ + └─────────────────────────────────────────┘ + │ + │ return a - b + ▼ + ┌─────────────────────────────────────────┐ + │ return of minus() │ + └─────────────────────────────────────────┘ diff --git a/tests/regression/cfg/pr-758.t/pr-758.c b/tests/regression/cfg/pr-758.t/pr-758.c new file mode 100644 index 0000000000..87aa41889d --- /dev/null +++ b/tests/regression/cfg/pr-758.t/pr-758.c @@ -0,0 +1,22 @@ +// Code from https://github.com/goblint/cil/pull/98 + +int main() { + // for loop + int x = 42; + for (x = 0; x < 10; x++) { // there shouldn't be invariants x <= 9, x <= 10 and 0 <= x before this line + // ... + } + + // expression with side effect + int i, k; + i = k = 0; // there shouldn't be invariant k == 0 before this line + + // compound initializers + struct kala { + int kaal; + int hind; + }; + + struct kala a = {2, 3}; // there shouldn't be invariant a.kaal == 2 before this line + return 0; +} diff --git a/tests/regression/cfg/pr-758.t/run.t b/tests/regression/cfg/pr-758.t/run.t new file mode 100644 index 0000000000..d87d9128c7 --- /dev/null +++ b/tests/regression/cfg/pr-758.t/run.t @@ -0,0 +1,71 @@ + $ cfgDot pr-758.c + + $ graph-easy --as=boxart main.dot + + ┌────────────────────────────────────────────────────────────────────────────────────────┐ + │ │ + │ ┌────────────────────────────────────┐ │ + │ │ main() │ │ + │ └────────────────────────────────────┘ │ + │ │ │ + │ │ (body) │ + │ ▼ │ + │ ┌────────────────────────────────────┐ │ + │ │ pr-758.c:5:7-5:13 │ │ + │ │ (pr-758.c:5:7-5:13) │ │ + │ └────────────────────────────────────┘ │ + │ │ │ x = x + 1 + │ │ x = 42 │ + │ ▼ │ + │ ┌────────────────────────────────────┐ │ + │ │ pr-758.c:6:3-8:3 (synthetic) │ │ + │ │ (pr-758.c:6:7-6:26 (synthetic)) │ │ + │ └────────────────────────────────────┘ │ + │ │ │ + │ │ x = 0 │ + │ ▼ │ + ┌─────────────────────────────────┐ ┌────────────────────────────────────┐ │ + │ pr-758.c:6:3-8:3 (synthetic) │ Pos(x < 10) │ pr-758.c:6:3-8:3 (synthetic) │ │ + │ (pr-758.c:6:7-6:26 (synthetic)) │ ◀───────────── │ (pr-758.c:6:7-6:26 (synthetic)) │ ◀┘ + └─────────────────────────────────┘ └────────────────────────────────────┘ + │ + │ Neg(x < 10) + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:12:3-12:12 │ + │ (pr-758.c:12:3-12:12) │ + └────────────────────────────────────┘ + │ + │ k = 0 + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:12:3-12:12 (synthetic) │ + │ (pr-758.c:12:3-12:12 (synthetic)) │ + └────────────────────────────────────┘ + │ + │ i = k + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:20:15-20:24 │ + │ (pr-758.c:20:15-20:24) │ + └────────────────────────────────────┘ + │ + │ a.kaal = 2 + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:20:15-20:24 (synthetic) │ + │ (pr-758.c:20:15-20:24 (synthetic)) │ + └────────────────────────────────────┘ + │ + │ a.hind = 3 + ▼ + ┌────────────────────────────────────┐ + │ pr-758.c:21:3-21:11 │ + │ (unknown) │ + └────────────────────────────────────┘ + │ + │ return 0 + ▼ + ┌────────────────────────────────────┐ + │ return of main() │ + └────────────────────────────────────┘ diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml new file mode 100644 index 0000000000..8d28933596 --- /dev/null +++ b/tests/regression/cfg/util/cfgDot.ml @@ -0,0 +1,55 @@ +let main () = + Goblint_logs.Logs.Level.current := Info; + Cilfacade.init (); + + let ast = Cilfacade.getAST (Fpath.v Sys.argv.(1)) in + CilCfg0.end_basic_blocks ast; + (* Part of CilCfg.createCFG *) + GoblintCil.iterGlobals ast (function + | GFun (fd, _) -> + GoblintCil.prepareCFG fd; + GoblintCil.computeCFGInfo fd true + | _ -> () + ); + let (module Cfg) = CfgTools.compute_cfg ast in + + let module LocationExtraNodeStyles = + struct + let defaultNodeStyles = ["align=\"left\""] + + let pp_loc ppf (loc: GoblintCil.location) = + if loc.line < 0 then + Format.pp_print_string ppf "unknown" + else if loc.synthetic then + Format.fprintf ppf "%a (synthetic)" CilType.Location.pp loc + else + CilType.Location.pp ppf loc + + let pp_locs ppf {CilLocation.loc; eloc} = + Format.fprintf ppf "@[%a@;(%a)@]" pp_loc loc pp_loc eloc + + let pp_label_locs ppf label = + let locs = CilLocation.get_labelLoc label in + Format.fprintf ppf "[%a]" pp_locs locs + + let extraNodeStyles = function + | Node.Statement stmt -> + let locs: CilLocation.locs = CilLocation.get_stmtLoc stmt in + let label = Format.asprintf "@[%a@;%a@]" pp_locs locs (Format.pp_print_list ~pp_sep:Format.pp_print_cut pp_label_locs) stmt.labels in + [Printf.sprintf "label=\"%s\"" (Str.global_replace (Str.regexp "\n") "\\n" label)] + | _ -> [] + end + in + + GoblintCil.iterGlobals ast (function + | GFun (fd, _) -> + let out = open_out (fd.svar.vname ^ ".dot") in + let iter_edges = CfgTools.iter_fd_edges (module Cfg) fd in + let ppf = Format.formatter_of_out_channel out in + CfgTools.fprint_dot (module CfgTools.CfgPrinters (LocationExtraNodeStyles)) iter_edges ppf; + Format.pp_print_flush ppf (); + close_out out + | _ -> () + ) + +let () = main () diff --git a/tests/regression/cfg/util/dune b/tests/regression/cfg/util/dune new file mode 100644 index 0000000000..8528aca384 --- /dev/null +++ b/tests/regression/cfg/util/dune @@ -0,0 +1,10 @@ +(executable + (name cfgDot) + (libraries + goblint-cil + goblint_logs + goblint_common + fpath + goblint.sites.dune + goblint.build-info.dune) + (preprocess (pps ppx_deriving.std))) diff --git a/tests/regression/dune b/tests/regression/dune index fdb1d941c2..ab95324fa4 100644 --- a/tests/regression/dune +++ b/tests/regression/dune @@ -1,3 +1,9 @@ +(env + (_ + (binaries ./cfg/util/cfgDot.exe))) + (cram (applies_to :whole_subtree) - (deps %{bin:goblint} (package goblint))) ; need entire package for includes/ + (deps + %{bin:goblint} + (package goblint))) ; need entire package for includes/