Skip to content

Commit f5ad06d

Browse files
sim642sim642
authored
Merge pull request #1847 from goblint/issue-1736
 Fix YAML witness `do`-`while` `loop_invariant` locations
2 parents af24b3b + 218124a commit f5ad06d

File tree

20 files changed

+449
-64
lines changed

20 files changed

+449
-64
lines changed

‎goblint.opam‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
9898
# also remember to generate/adjust goblint.opam.locked!
9999
available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
100100
pin-depends: [
101-
[ "goblint-cil.2.0.7" "git+https://github.com/goblint/cil.git#e5b6287c0c85864c6d44f7fa30d0084a3ae11d6c" ]
101+
[ "goblint-cil.2.0.8" "git+https://github.com/goblint/cil.git#2e076120a039b52f174fa799e65773f3a78d383c" ]
102102
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
103103
[ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
104104
]

‎goblint.opam.locked‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ depends: [
6666
"fileutils" {= "0.6.4"}
6767
"fmt" {= "0.9.0"}
6868
"fpath" {= "0.7.3"}
69-
"goblint-cil" {= "2.0.7"}
69+
"goblint-cil" {= "2.0.8"}
7070
"hex" {= "1.5.0"}
7171
"integers" {= "0.7.0"}
7272
"json-data-encoding" {= "1.0.1"}
@@ -144,8 +144,8 @@ post-messages: [
144144
]
145145
pin-depends: [
146146
[
147-
"goblint-cil.2.0.7"
148-
"git+https://github.com/goblint/cil.git#e5b6287c0c85864c6d44f7fa30d0084a3ae11d6c"
147+
"goblint-cil.2.0.8"
148+
"git+https://github.com/goblint/cil.git#2e076120a039b52f174fa799e65773f3a78d383c"
149149
]
150150
[
151151
"apron.v0.9.15"

‎goblint.opam.template‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
# also remember to generate/adjust goblint.opam.locked!
33
available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
44
pin-depends: [
5-
[ "goblint-cil.2.0.7" "git+https://github.com/goblint/cil.git#e5b6287c0c85864c6d44f7fa30d0084a3ae11d6c" ]
5+
[ "goblint-cil.2.0.8" "git+https://github.com/goblint/cil.git#2e076120a039b52f174fa799e65773f3a78d383c" ]
66
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
77
[ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
88
]

‎src/common/util/cilfacade.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,8 @@ let init () =
9191
RmUnused.keepUnused := true;
9292
print_CIL_Input := true;
9393
Cabs2cil.allowDuplication := false;
94-
Cabs2cil.silenceLongDoubleWarning := true
94+
Cabs2cil.silenceLongDoubleWarning := true;
95+
Cabs2cil.addLoopConditionLabels := true
9596

9697
let current_file = ref dummyFile
9798

‎src/witness/witnessUtil.ml‎

Lines changed: 22 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,27 @@ struct
9494
) stmts
9595
) prevs
9696
| FunctionEntry _ | Function _ -> None
97+
98+
let find_syntactic_loop_condition_label s =
99+
List.find_map (function
100+
| Label (name, loc, false) when String.starts_with ~prefix:"__loop_condition" name -> Some loc
101+
| _ -> None
102+
) s.labels
103+
104+
let find_syntactic_loop_condition = function
105+
| Statement s as n ->
106+
(* No need to LoopUnrolling.find_original because loop unrolling duplicates __loop_condition labels (with new suffixes). *)
107+
begin match find_syntactic_loop_condition_label s with
108+
| Some _ as r -> r
109+
| None ->
110+
(* The __loop_condition label may not be on s itself, but still on the surrounding Block (skipped in CFG) due to basic blocks transformation. *)
111+
let prevs = Cfg.prev n in
112+
List.find_map (fun (edges, prev) ->
113+
let stmts = Cfg.skippedByEdge prev edges n in
114+
List.find_map find_syntactic_loop_condition_label stmts
115+
) prevs
116+
end
117+
| FunctionEntry _ | Function _ -> None
97118
end
98119

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

121142
let loop_location n =
122-
find_syntactic_loop_head n
143+
find_syntactic_loop_condition n
123144
|> BatOption.filter (fun _loc -> not (is_stub_node n))
124145

125146
let is_loop_head_node n = Option.is_some (loop_location n)

‎tests/regression/00-sanity/21-empty-loops.t‎

Lines changed: 22 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,10 @@
3939
│ (body)
4040
▼
4141
┌────────────────────────────────────────────┐
42-
│ 21-empty-loops.c:63:3-63:14 (synthetic) │ Pos(1)
43-
│ (21-empty-loops.c:63:10-63:11 (synthetic)) │ ─────────┐
42+
│ 21-empty-loops.c:63:3-63:14 (synthetic) │
43+
│ (21-empty-loops.c:63:10-63:11 (synthetic)) │
44+
│ [21-empty-loops.c:63:3-63:14 (synthetic) │ Pos(1)
45+
│ (unknown)] │ ─────────┐
4446
│ YAML loop: 21-empty-loops.c:63:3-63:14 │ │
4547
│ server: false │ ◀────────┘
4648
└────────────────────────────────────────────┘
@@ -105,8 +107,10 @@
105107
│ (body)
106108
▼
107109
┌────────────────────────────────────────────┐
108-
│ 21-empty-loops.c:81:3-81:14 (synthetic) │ Pos(1)
109-
│ (21-empty-loops.c:81:10-81:11 (synthetic)) │ ─────────┐
110+
│ 21-empty-loops.c:81:3-81:14 (synthetic) │
111+
│ (21-empty-loops.c:81:10-81:11 (synthetic)) │
112+
│ [21-empty-loops.c:81:3-81:14 (synthetic) │ Pos(1)
113+
│ (unknown)] │ ─────────┐
110114
│ YAML loop: 21-empty-loops.c:81:3-81:14 │ │
111115
│ server: false │ ◀────────┘
112116
└────────────────────────────────────────────┘
@@ -175,10 +179,12 @@
175179
│ │ (body) │
176180
│ ▼ │
177181
┌─────────────────────────────────────────┐ ┌──────────────────────────────────────────────┐ │
178-
│ 21-empty-loops.c:102:5-102:11 │ │ 21-empty-loops.c:100:3-103:3 (synthetic) │ │
179-
│ (21-empty-loops.c:102:5-102:11) │ │ (21-empty-loops.c:100:10-100:11 (synthetic)) │ │
180-
│ YAML loc: 21-empty-loops.c:102:5-102:11 │ Pos(1) │ YAML loop: 21-empty-loops.c:100:3-103:3 │ │
181-
│ server: true │ ◀──────── │ server: false │ ◀┘
182+
│ │ │ 21-empty-loops.c:100:3-103:3 (synthetic) │ │
183+
│ 21-empty-loops.c:102:5-102:11 │ │ (21-empty-loops.c:100:10-100:11 (synthetic)) │ │
184+
│ (21-empty-loops.c:102:5-102:11) │ │ [21-empty-loops.c:100:3-103:3 (synthetic) │ │
185+
│ YAML loc: 21-empty-loops.c:102:5-102:11 │ │ (unknown)] │ │
186+
│ server: true │ Pos(1) │ YAML loop: 21-empty-loops.c:100:3-103:3 │ │
187+
│ │ ◀──────── │ server: false │ ◀┘
182188
└─────────────────────────────────────────┘ └──────────────────────────────────────────────┘
183189
│
184190
│ Neg(1)
@@ -254,8 +260,10 @@
254260
│ prefix()
255261
▼
256262
┌──────────────────────────────────────────────┐
257-
│ 21-empty-loops.c:123:3-123:14 (synthetic) │ Pos(1)
258-
│ (21-empty-loops.c:123:10-123:11 (synthetic)) │ ─────────┐
263+
│ 21-empty-loops.c:123:3-123:14 (synthetic) │
264+
│ (21-empty-loops.c:123:10-123:11 (synthetic)) │
265+
│ [21-empty-loops.c:123:3-123:14 (synthetic) │ Pos(1)
266+
│ (unknown)] │ ─────────┐
259267
│ YAML loop: 21-empty-loops.c:123:3-123:14 │ │
260268
│ server: false │ ◀────────┘
261269
└──────────────────────────────────────────────┘
@@ -313,8 +321,10 @@
313321
│ (body)
314322
▼
315323
┌──────────────────────────────────────────────┐
316-
│ 21-empty-loops.c:136:3-138:3 (synthetic) │ Pos(1)
317-
│ (21-empty-loops.c:136:10-136:11 (synthetic)) │ ─────────┐
324+
│ 21-empty-loops.c:136:3-138:3 (synthetic) │
325+
│ (21-empty-loops.c:136:10-136:11 (synthetic)) │
326+
│ [21-empty-loops.c:136:3-138:3 (synthetic) │ Pos(1)
327+
│ (unknown)] │ ─────────┐
318328
│ YAML loop: 21-empty-loops.c:136:3-138:3 │ │
319329
│ server: false │ ◀────────┘
320330
└──────────────────────────────────────────────┘

0 commit comments

Comments
 (0)