Skip to content

Fix YAML witness do-while loop_invariant locations #1847

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Fix YAML witness do-while loop_invariant locations #1847

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
385d8d5
Fix YAML witness do-while loop_invariant locations (closes #1736)
sim642 Oct 23, 2025
0428428
Fix __loop_condition label finding with basic blocks
sim642 Oct 23, 2025
b3a8523
Add Cabs2cil.addLoopConditionLabels option to CIL
sim642 Oct 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion goblint.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
# also remember to generate/adjust goblint.opam.locked!
available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
pin-depends: [
[ "goblint-cil.2.0.7" "git+https://github.com/goblint/cil.git#e5b6287c0c85864c6d44f7fa30d0084a3ae11d6c" ]
[ "goblint-cil.2.0.8" "git+https://github.com/goblint/cil.git#2e076120a039b52f174fa799e65773f3a78d383c" ]
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
[ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
]
Expand Down
6 changes: 3 additions & 3 deletions goblint.opam.locked
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ depends: [
"fileutils" {= "0.6.4"}
"fmt" {= "0.9.0"}
"fpath" {= "0.7.3"}
"goblint-cil" {= "2.0.7"}
"goblint-cil" {= "2.0.8"}
"hex" {= "1.5.0"}
"integers" {= "0.7.0"}
"json-data-encoding" {= "1.0.1"}
Expand Down Expand Up @@ -144,8 +144,8 @@ post-messages: [
]
pin-depends: [
[
"goblint-cil.2.0.7"
"git+https://github.com/goblint/cil.git#e5b6287c0c85864c6d44f7fa30d0084a3ae11d6c"
"goblint-cil.2.0.8"
"git+https://github.com/goblint/cil.git#2e076120a039b52f174fa799e65773f3a78d383c"
]
[
"apron.v0.9.15"
Expand Down
2 changes: 1 addition & 1 deletion goblint.opam.template
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
# also remember to generate/adjust goblint.opam.locked!
available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
pin-depends: [
[ "goblint-cil.2.0.7" "git+https://github.com/goblint/cil.git#e5b6287c0c85864c6d44f7fa30d0084a3ae11d6c" ]
[ "goblint-cil.2.0.8" "git+https://github.com/goblint/cil.git#2e076120a039b52f174fa799e65773f3a78d383c" ]
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
[ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
]
Expand Down
3 changes: 2 additions & 1 deletion src/common/util/cilfacade.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,8 @@ let init () =
RmUnused.keepUnused := true;
print_CIL_Input := true;
Cabs2cil.allowDuplication := false;
Cabs2cil.silenceLongDoubleWarning := true
Cabs2cil.silenceLongDoubleWarning := true;
Cabs2cil.addLoopConditionLabels := true

let current_file = ref dummyFile

Expand Down
23 changes: 22 additions & 1 deletion src/witness/witnessUtil.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,27 @@ struct
) stmts
) prevs
| FunctionEntry _ | Function _ -> None

let find_syntactic_loop_condition_label s =
List.find_map (function
| Label (name, loc, false) when String.starts_with ~prefix:"__loop_condition" name -> Some loc
| _ -> None
) s.labels

let find_syntactic_loop_condition = function
| Statement s as n ->
(* No need to LoopUnrolling.find_original because loop unrolling duplicates __loop_condition labels (with new suffixes). *)
begin match find_syntactic_loop_condition_label s with
| Some _ as r -> r
| None ->
(* The __loop_condition label may not be on s itself, but still on the surrounding Block (skipped in CFG) due to basic blocks transformation. *)
let prevs = Cfg.prev n in
List.find_map (fun (edges, prev) ->
let stmts = Cfg.skippedByEdge prev edges n in
List.find_map find_syntactic_loop_condition_label stmts
) prevs
end
| FunctionEntry _ | Function _ -> None
end

module YamlInvariant (FileCfg: MyCFG.FileCfg) =
Expand All @@ -119,7 +140,7 @@ struct
let is_invariant_node n = Option.is_some (location_location n)

let loop_location n =
find_syntactic_loop_head n
find_syntactic_loop_condition n
|> BatOption.filter (fun _loc -> not (is_stub_node n))

let is_loop_head_node n = Option.is_some (loop_location n)
Expand Down
34 changes: 22 additions & 12 deletions tests/regression/00-sanity/21-empty-loops.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,8 +39,10 @@
│ (body)
▼
┌────────────────────────────────────────────┐
│ 21-empty-loops.c:63:3-63:14 (synthetic) │ Pos(1)
│ (21-empty-loops.c:63:10-63:11 (synthetic)) │ ─────────┐
│ 21-empty-loops.c:63:3-63:14 (synthetic) │
│ (21-empty-loops.c:63:10-63:11 (synthetic)) │
│ [21-empty-loops.c:63:3-63:14 (synthetic) │ Pos(1)
│ (unknown)] │ ─────────┐
│ YAML loop: 21-empty-loops.c:63:3-63:14 │ │
│ server: false │ ◀────────┘
└────────────────────────────────────────────┘
Expand Down Expand Up @@ -105,8 +107,10 @@
│ (body)
▼
┌────────────────────────────────────────────┐
│ 21-empty-loops.c:81:3-81:14 (synthetic) │ Pos(1)
│ (21-empty-loops.c:81:10-81:11 (synthetic)) │ ─────────┐
│ 21-empty-loops.c:81:3-81:14 (synthetic) │
│ (21-empty-loops.c:81:10-81:11 (synthetic)) │
│ [21-empty-loops.c:81:3-81:14 (synthetic) │ Pos(1)
│ (unknown)] │ ─────────┐
│ YAML loop: 21-empty-loops.c:81:3-81:14 │ │
│ server: false │ ◀────────┘
└────────────────────────────────────────────┘
Expand Down Expand Up @@ -175,10 +179,12 @@
│ │ (body) │
│ ▼ │
┌─────────────────────────────────────────┐ ┌──────────────────────────────────────────────┐ │
│ 21-empty-loops.c:102:5-102:11 │ │ 21-empty-loops.c:100:3-103:3 (synthetic) │ │
│ (21-empty-loops.c:102:5-102:11) │ │ (21-empty-loops.c:100:10-100:11 (synthetic)) │ │
│ YAML loc: 21-empty-loops.c:102:5-102:11 │ Pos(1) │ YAML loop: 21-empty-loops.c:100:3-103:3 │ │
│ server: true │ ◀──────── │ server: false │ ◀┘
│ │ │ 21-empty-loops.c:100:3-103:3 (synthetic) │ │
│ 21-empty-loops.c:102:5-102:11 │ │ (21-empty-loops.c:100:10-100:11 (synthetic)) │ │
│ (21-empty-loops.c:102:5-102:11) │ │ [21-empty-loops.c:100:3-103:3 (synthetic) │ │
│ YAML loc: 21-empty-loops.c:102:5-102:11 │ │ (unknown)] │ │
│ server: true │ Pos(1) │ YAML loop: 21-empty-loops.c:100:3-103:3 │ │
│ │ ◀──────── │ server: false │ ◀┘
└─────────────────────────────────────────┘ └──────────────────────────────────────────────┘
│
│ Neg(1)
Expand Down Expand Up @@ -254,8 +260,10 @@
│ prefix()
▼
┌──────────────────────────────────────────────┐
│ 21-empty-loops.c:123:3-123:14 (synthetic) │ Pos(1)
│ (21-empty-loops.c:123:10-123:11 (synthetic)) │ ─────────┐
│ 21-empty-loops.c:123:3-123:14 (synthetic) │
│ (21-empty-loops.c:123:10-123:11 (synthetic)) │
│ [21-empty-loops.c:123:3-123:14 (synthetic) │ Pos(1)
│ (unknown)] │ ─────────┐
│ YAML loop: 21-empty-loops.c:123:3-123:14 │ │
│ server: false │ ◀────────┘
└──────────────────────────────────────────────┘
Expand Down Expand Up @@ -313,8 +321,10 @@
│ (body)
▼
┌──────────────────────────────────────────────┐
│ 21-empty-loops.c:136:3-138:3 (synthetic) │ Pos(1)
│ (21-empty-loops.c:136:10-136:11 (synthetic)) │ ─────────┐
│ 21-empty-loops.c:136:3-138:3 (synthetic) │
│ (21-empty-loops.c:136:10-136:11 (synthetic)) │
│ [21-empty-loops.c:136:3-138:3 (synthetic) │ Pos(1)
│ (unknown)] │ ─────────┐
│ YAML loop: 21-empty-loops.c:136:3-138:3 │ │
│ server: false │ ◀────────┘
└──────────────────────────────────────────────┘
Expand Down
Loading
Loading