Skip to content

Commit 1e134df

Browse files
sim642sim642
committed
Merge branch 'cfg-test-pred' into fix-locations-pred
2 parents 854f47d + 994d287 commit 1e134df

File tree

12 files changed

+416
-200
lines changed

12 files changed

+416
-200
lines changed

‎src/analyses/unassumeAnalysis.ml

+2-4
Original file line numberDiff line numberDiff line change
@@ -48,18 +48,16 @@ struct
4848
let file = !Cilfacade.current_file
4949
module Cfg = (val !MyCFG.current_cfg)
5050
end in
51-
let module WitnessInvariant = WitnessUtil.Invariant (FileCfg) in
51+
let module WitnessInvariant = WitnessUtil.YamlInvariantValidate (FileCfg) in
5252

5353
(* DFS, copied from CfgTools.find_backwards_reachable *)
5454
let reachable = NH.create 100 in
5555
let rec iter_node node =
5656
if not (NH.mem reachable node) then begin
5757
NH.replace reachable node ();
58-
(* TODO: filter synthetic?
59-
See YamlWitness. *)
6058
if WitnessInvariant.is_invariant_node node then
6159
Locator.add locator (Node.location node) node;
62-
if WitnessUtil.NH.mem WitnessInvariant.loop_heads node then
60+
if WitnessInvariant.is_loop_head_node node then
6361
Locator.add loop_locator (Node.location node) node;
6462
List.iter (fun (_, prev_node) ->
6563
iter_node prev_node

‎src/util/server.ml

+6-2
Original file line numberDiff line numberDiff line change
@@ -121,6 +121,10 @@ let serve serv =
121121
|> Seq.map Packet.t_of_yojson
122122
|> Seq.iter (handle_packet serv)
123123

124+
let is_server_node cfgnode =
125+
let loc = UpdateCil.getLoc cfgnode in
126+
not loc.synthetic
127+
124128
let arg_wrapper: (module ArgWrapper) ResettableLazy.t =
125129
ResettableLazy.from_fun (fun () ->
126130
let module Arg = (val (Option.get_exn !ArgTools.current_arg Response.Error.(E (make ~code:RequestFailed ~message:"not analyzed or arg disabled" ())))) in
@@ -133,7 +137,7 @@ let arg_wrapper: (module ArgWrapper) ResettableLazy.t =
133137
Arg.iter_nodes (fun n ->
134138
let cfgnode = Arg.Node.cfgnode n in
135139
let loc = UpdateCil.getLoc cfgnode in
136-
if not loc.synthetic then
140+
if is_server_node cfgnode then
137141
Locator.add locator loc n;
138142
StringH.replace ids (Arg.Node.to_string n) n;
139143
StringH.add cfg_nodes (Node.show_id cfgnode) n (* add for find_all *)
@@ -248,7 +252,7 @@ let node_locator: Locator.t ResettableLazy.t =
248252
if not (NH.mem reachable node) then begin
249253
NH.replace reachable node ();
250254
let loc = UpdateCil.getLoc node in
251-
if not loc.synthetic then
255+
if is_server_node node then
252256
Locator.add locator loc node;
253257
List.iter (fun (_, prev_node) ->
254258
iter_node prev_node

‎src/witness/witnessUtil.ml

+34
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,40 @@ struct
8181
emit_other
8282
end
8383

84+
module YamlInvariant (FileCfg: MyCFG.FileCfg) =
85+
struct
86+
include Invariant (FileCfg)
87+
88+
let is_stub_node n =
89+
let fundec = Node.find_fundec n in
90+
Cil.hasAttribute "goblint_stub" fundec.svar.vattr
91+
92+
let is_invariant_node (n : Node.t) =
93+
let loc = Node.location n in
94+
match n with
95+
| Statement _ ->
96+
not loc.synthetic && is_invariant_node n && not (is_stub_node n)
97+
| FunctionEntry _ | Function _ ->
98+
(* avoid FunctionEntry/Function, because their locations are not inside the function where asserts could be inserted *)
99+
false
100+
101+
let is_loop_head_node n =
102+
NH.mem loop_heads n && not (is_stub_node n)
103+
end
104+
105+
module YamlInvariantValidate (FileCfg: MyCFG.FileCfg) =
106+
struct
107+
include Invariant (FileCfg)
108+
109+
(* TODO: filter synthetic?
110+
111+
Almost all loops are transformed by CIL, so the loop constructs all get synthetic locations. Filtering them from the locator could give some odd behavior: if the location is right before the loop and all the synthetic loop head stuff is filtered, then the first non-synthetic node is already inside the loop, not outside where the location actually was.
112+
Similarly, if synthetic locations are then filtered, witness.invariant.loop-head becomes essentially useless.
113+
I guess at some point during testing and benchmarking I achieved better results with the filtering removed. *)
114+
115+
let is_loop_head_node = NH.mem loop_heads
116+
end
117+
84118
module InvariantExp =
85119
struct
86120
module ES = SetDomain.Make (CilType.Exp)

‎src/witness/yamlWitness.ml

+8-32
Original file line numberDiff line numberDiff line change
@@ -165,7 +165,7 @@ struct
165165
open SpecSys
166166

167167
module NH = BatHashtbl.Make (Node)
168-
module WitnessInvariant = WitnessUtil.Invariant (FileCfg)
168+
module WitnessInvariant = WitnessUtil.YamlInvariant (FileCfg)
169169
module FMap = BatHashtbl.Make (CilType.Fundec)
170170
module FCMap = BatHashtbl.Make (Printable.Prod (CilType.Fundec) (Spec.C))
171171
type con_inv = {node: Node.t; context: Spec.C.t; invariant: Invariant.t; state: Spec.D.t}
@@ -193,25 +193,6 @@ struct
193193
in
194194
let task = Entry.task ~input_files ~data_model ~specification in
195195

196-
let is_stub_node n =
197-
let fundec = Node.find_fundec n in
198-
Cil.hasAttribute "goblint_stub" fundec.svar.vattr
199-
in
200-
201-
let is_invariant_node (n : Node.t) =
202-
let loc = Node.location n in
203-
match n with
204-
| Statement _ ->
205-
not loc.synthetic && WitnessInvariant.is_invariant_node n && not (is_stub_node n)
206-
| FunctionEntry _ | Function _ ->
207-
(* avoid FunctionEntry/Function, because their locations are not inside the function where asserts could be inserted *)
208-
false
209-
in
210-
211-
let is_loop_head_node n =
212-
WitnessUtil.NH.mem WitnessInvariant.loop_heads n && not (is_stub_node n)
213-
in
214-
215196
let local_lvals n local =
216197
if GobConfig.get_bool "witness.invariant.accessed" then (
217198
match R.ask_local_node n ~local MayAccessed with
@@ -254,7 +235,7 @@ struct
254235
let entries =
255236
if entry_type_enabled YamlWitnessType.LocationInvariant.entry_type then (
256237
LH.fold (fun loc ns acc ->
257-
if List.exists is_invariant_node ns then (
238+
if List.exists WitnessInvariant.is_invariant_node ns then (
258239
let inv = List.fold_left (fun acc n ->
259240
let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
260241
let lvals = local_lvals n local in
@@ -287,7 +268,7 @@ struct
287268
let entries =
288269
if entry_type_enabled YamlWitnessType.LoopInvariant.entry_type then (
289270
LH.fold (fun loc ns acc ->
290-
if WitnessInvariant.emit_loop_head && List.exists is_loop_head_node ns then (
271+
if WitnessInvariant.emit_loop_head && List.exists WitnessInvariant.is_loop_head_node ns then (
291272
let inv = List.fold_left (fun acc n ->
292273
let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
293274
Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
@@ -392,7 +373,7 @@ struct
392373

393374
(* 3. Generate precondition invariants *)
394375
LHT.fold (fun ((n, c) as lvar) local acc ->
395-
if is_invariant_node n then (
376+
if WitnessInvariant.is_invariant_node n then (
396377
let fundec = Node.find_fundec n in
397378
let pre_lvar = (Node.FunctionEntry fundec, c) in
398379
let query = Queries.Invariant Invariant.default_context in
@@ -449,7 +430,7 @@ struct
449430
let invariants =
450431
if invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then (
451432
LH.fold (fun loc ns acc ->
452-
if List.exists is_invariant_node ns then (
433+
if List.exists WitnessInvariant.is_invariant_node ns then (
453434
let inv = List.fold_left (fun acc n ->
454435
let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
455436
let lvals = local_lvals n local in
@@ -482,7 +463,7 @@ struct
482463
let invariants =
483464
if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then (
484465
LH.fold (fun loc ns acc ->
485-
if WitnessInvariant.emit_loop_head && List.exists is_loop_head_node ns then (
466+
if WitnessInvariant.emit_loop_head && List.exists WitnessInvariant.is_loop_head_node ns then (
486467
let inv = List.fold_left (fun acc n ->
487468
let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
488469
Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
@@ -565,7 +546,7 @@ struct
565546

566547
module Locator = WitnessUtil.Locator (EQSys.LVar)
567548
module LvarS = Locator.ES
568-
module WitnessInvariant = WitnessUtil.Invariant (FileCfg)
549+
module WitnessInvariant = WitnessUtil.YamlInvariantValidate (FileCfg)
569550
module InvariantParser = WitnessUtil.InvariantParser
570551
module VR = ValidationResult
571552

@@ -585,14 +566,9 @@ struct
585566
let loop_locator = Locator.create () in
586567
LHT.iter (fun ((n, _) as lvar) _ ->
587568
let loc = Node.location n in
588-
(* TODO: filter synthetic?
589-
590-
Almost all loops are transformed by CIL, so the loop constructs all get synthetic locations. Filtering them from the locator could give some odd behavior: if the location is right before the loop and all the synthetic loop head stuff is filtered, then the first non-synthetic node is already inside the loop, not outside where the location actually was.
591-
Similarly, if synthetic locations are then filtered, witness.invariant.loop-head becomes essentially useless.
592-
I guess at some point during testing and benchmarking I achieved better results with the filtering removed. *)
593569
if WitnessInvariant.is_invariant_node n then
594570
Locator.add locator loc lvar;
595-
if WitnessUtil.NH.mem WitnessInvariant.loop_heads n then
571+
if WitnessInvariant.is_loop_head_node n then
596572
Locator.add loop_locator loc lvar
597573
) lh;
598574

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

+39-30
Original file line numberDiff line numberDiff line change
@@ -1,33 +1,42 @@
11
$ cfgDot 19-if-0.c
22

33
$ graph-easy --as=boxart main.dot
4-
┌─────────────────────────┐
5-
│ main() │
6-
└─────────────────────────┘
7-
│
8-
│ (body)
9-
▼
10-
┌────────────────────────┐ ┌─────────────────────────┐
11-
│ 19-if-0.c:15:9-15:27 │ Neg(0) │ 19-if-0.c:9:5-16:5 │
12-
│ (19-if-0.c:15:9-15:27) │ ◀──────────────────── │ (19-if-0.c:9:9-9:10) │
13-
└────────────────────────┘ └─────────────────────────┘
14-
│ │
15-
│ │ Pos(0)
16-
│ ▼
17-
│ ┌─────────────────────────┐
18-
│ │ 19-if-0.c:11:9-11:16 │
19-
│ │ (19-if-0.c:11:9-11:16) │
20-
│ └─────────────────────────┘
21-
│ │
22-
│ │ stuff()
23-
│ ▼
24-
│ ┌─────────────────────────┐
25-
│ __goblint_check(1) │ 19-if-0.c:17:5-17:13 │
26-
└────────────────────────────────────────────▶ │ (19-if-0.c:17:12-17:13) │
27-
└─────────────────────────┘
28-
│
29-
│ return 0
30-
▼
31-
┌─────────────────────────┐
32-
│ return of main() │
33-
└─────────────────────────┘
4+
┌────────────────────────────────┐
5+
│ main() │
6+
└────────────────────────────────┘
7+
│
8+
│ (body)
9+
▼
10+
┌────────────────────────────────┐ ┌────────────────────────────────┐
11+
│ 19-if-0.c:15:9-15:27 │ │ 19-if-0.c:9:5-16:5 │
12+
│ (19-if-0.c:15:9-15:27) │ │ (19-if-0.c:9:9-9:10) │
13+
│ YAML loc: true, loop: false │ │ YAML loc: true, loop: false │
14+
│ YAMLval loc: true, loop: false │ Neg(0) │ YAMLval loc: true, loop: false │
15+
│ GraphML: true; server: true │ ◀──────────────────── │ GraphML: true; server: true │
16+
└────────────────────────────────┘ └────────────────────────────────┘
17+
│ │
18+
│ │ Pos(0)
19+
│ ▼
20+
│ ┌────────────────────────────────┐
21+
│ │ 19-if-0.c:11:9-11:16 │
22+
│ │ (19-if-0.c:11:9-11:16) │
23+
│ │ YAML loc: true, loop: false │
24+
│ │ YAMLval loc: true, loop: false │
25+
│ │ GraphML: true; server: true │
26+
│ └────────────────────────────────┘
27+
│ │
28+
│ │ stuff()
29+
│ ▼
30+
│ ┌────────────────────────────────┐
31+
│ │ 19-if-0.c:17:5-17:13 │
32+
│ │ (19-if-0.c:17:12-17:13) │
33+
│ │ YAML loc: true, loop: false │
34+
│ __goblint_check(1) │ YAMLval loc: true, loop: false │
35+
└────────────────────────────────────────────────────▶ │ GraphML: true; server: true │
36+
└────────────────────────────────┘
37+
│
38+
│ return 0
39+
▼
40+
┌────────────────────────────────┐
41+
│ return of main() │
42+
└────────────────────────────────┘

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

+13-4
Original file line numberDiff line numberDiff line change
@@ -8,24 +8,33 @@
88
│ (body)
99
▼
1010
┌──────────────────────────────────┐
11-
│ 20-if-0-realnode.c:8:5-14:5 │ Neg(0)
12-
│ (20-if-0-realnode.c:8:9-8:10) │ ─────────┐
13-
│ [20-if-0-realnode.c:7:5-8:5 │ │
14-
│ (unknown)] │ ◀────────┘
11+
│ 20-if-0-realnode.c:8:5-14:5 │
12+
│ (20-if-0-realnode.c:8:9-8:10) │
13+
│ [20-if-0-realnode.c:7:5-8:5 │
14+
│ (unknown)] │ Neg(0)
15+
│ YAML loc: true, loop: true │ ─────────┐
16+
│ YAMLval loc: true, loop: true │ │
17+
│ GraphML: true; server: true │ ◀────────┘
1518
└──────────────────────────────────┘
1619
│
1720
│ Pos(0)
1821
▼
1922
┌──────────────────────────────────┐
2023
│ 20-if-0-realnode.c:10:9-10:16 │
2124
│ (20-if-0-realnode.c:10:9-10:16) │
25+
│ YAML loc: true, loop: false │
26+
│ YAMLval loc: true, loop: false │
27+
│ GraphML: true; server: true │
2228
└──────────────────────────────────┘
2329
│
2430
│ stuff()
2531
▼
2632
┌──────────────────────────────────┐
2733
│ 20-if-0-realnode.c:15:5-15:13 │
2834
│ (20-if-0-realnode.c:15:12-15:13) │
35+
│ YAML loc: true, loop: false │
36+
│ YAMLval loc: true, loop: false │
37+
│ GraphML: true; server: true │
2938
└──────────────────────────────────┘
3039
│
3140
│ return 0

0 commit comments

Comments
 (0)