Skip to content

Commit edadcab

Browse files
sim642sim642
authored
Merge pull request #586 from goblint/queries-id
Optimize `Queries.ID`
2 parents 39f37ea + 4b993f3 commit edadcab

File tree

10 files changed

+266
-41
lines changed

10 files changed

+266
-41
lines changed

‎bench/basic/benchTuple4.ml‎

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
(* dune exec bench/basic/benchTuple4.exe -- -a *)
2+
3+
open Benchmark
4+
open Benchmark.Tree
5+
6+
7+
let () =
8+
let exists0 =
9+
let open Batteries in
10+
let to_list x = Tuple4.enum x |> List.of_enum |> List.filter_map identity in
11+
let f g = g identity % to_list in
12+
List.(f exists)
13+
in
14+
15+
let exists1 = function
16+
| (Some true, _, _, _)
17+
| (_, Some true, _, _)
18+
| (_, _, Some true, _)
19+
| (_, _, _, Some true) ->
20+
true
21+
| _ ->
22+
false
23+
in
24+
25+
let exists2 (a, b, c, d) = a = Some true || b = Some true || c = Some true || d = Some true in
26+
27+
28+
register (
29+
"exists" @>>> [
30+
"all None" @> lazy (
31+
let args = (None, None, None, None) in
32+
throughputN 1 [
33+
("0", exists0, args);
34+
("1", exists1, args);
35+
("2", exists2, args);
36+
]
37+
);
38+
"all Some true" @> lazy (
39+
let args = (Some true, Some true, Some true, Some true) in
40+
throughputN 1 [
41+
("0", exists0, args);
42+
("1", exists1, args);
43+
("2", exists2, args);
44+
]
45+
);
46+
"all Some false" @> lazy (
47+
let args = (Some false, Some false, Some false, Some false) in
48+
throughputN 1 [
49+
("0", exists0, args);
50+
("1", exists1, args);
51+
("2", exists2, args);
52+
]
53+
);
54+
"all None except last Some true" @> lazy (
55+
let args = (None, None, None, Some true) in
56+
throughputN 1 [
57+
("0", exists0, args);
58+
("1", exists1, args);
59+
("2", exists2, args);
60+
]
61+
);
62+
"all Some false except last Some true" @> lazy (
63+
let args = (Some false, Some false, Some false, Some true) in
64+
throughputN 1 [
65+
("0", exists0, args);
66+
("1", exists1, args);
67+
("2", exists2, args);
68+
]
69+
);
70+
]
71+
)
72+
73+
74+
let () =
75+
let for_all0 =
76+
let open Batteries in
77+
let to_list x = Tuple4.enum x |> List.of_enum |> List.filter_map identity in
78+
let f g = g identity % to_list in
79+
List.(f for_all)
80+
in
81+
82+
let for_all1 = function
83+
| (Some false, _, _, _)
84+
| (_, Some false, _, _)
85+
| (_, _, Some false, _)
86+
| (_, _, _, Some false) ->
87+
false
88+
| _ ->
89+
true
90+
in
91+
92+
let for_all2 (a, b, c, d) = not (a = Some false || b = Some false || c = Some false || d = Some false) in
93+
94+
95+
register (
96+
"for_all" @>>> [
97+
"all None" @> lazy (
98+
let args = (None, None, None, None) in
99+
throughputN 1 [
100+
("0", for_all0, args);
101+
("1", for_all1, args);
102+
("2", for_all2, args);
103+
]
104+
);
105+
"all Some true" @> lazy (
106+
let args = (Some true, Some true, Some true, Some true) in
107+
throughputN 1 [
108+
("0", for_all0, args);
109+
("1", for_all1, args);
110+
("2", for_all2, args);
111+
]
112+
);
113+
"all Some false" @> lazy (
114+
let args = (Some false, Some false, Some false, Some false) in
115+
throughputN 1 [
116+
("0", for_all0, args);
117+
("1", for_all1, args);
118+
("2", for_all2, args);
119+
]
120+
);
121+
"all None except last Some false" @> lazy (
122+
let args = (None, None, None, Some false) in
123+
throughputN 1 [
124+
("0", for_all0, args);
125+
("1", for_all1, args);
126+
("2", for_all2, args);
127+
]
128+
);
129+
"all Some true except last Some false" @> lazy (
130+
let args = (Some true, Some true, Some true, Some false) in
131+
throughputN 1 [
132+
("0", for_all0, args);
133+
("1", for_all1, args);
134+
("2", for_all2, args);
135+
]
136+
);
137+
]
138+
)
139+
140+
let () =
141+
run_global ()

‎bench/basic/dune‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
(executable
2+
(name benchTuple4)
3+
(optional) ; TODO: for some reason this doesn't work: `dune build` still tries to compile if benchmark missing (https://github.com/ocaml/dune/issues/4065)
4+
(libraries benchmark batteries.unthreaded))

‎src/analyses/base.ml‎

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -602,9 +602,10 @@ struct
602602
let a = a.f (Q.EvalInt exp) in (* through queries includes eval_next, so no (exponential) branching is necessary *)
603603
if M.tracing then M.traceu "evalint" "base ask EvalInt %a -> %a\n" d_exp exp Queries.ID.pretty a;
604604
begin match a with
605-
| x when Queries.ID.is_bot x -> eval_next () (* Base EvalInt returns bot on incorrect type (e.g. pthread_t); ignore and continue. *)
605+
| `Bot -> eval_next () (* Base EvalInt returns bot on incorrect type (e.g. pthread_t); ignore and continue. *)
606606
(* | x -> Some (`Int x) *)
607-
| x -> `Int x (* cast should be unnecessary, EvalInt should guarantee right ikind already *)
607+
| `Lifted x -> `Int x (* cast should be unnecessary, EvalInt should guarantee right ikind already *)
608+
| `Top -> `Int (ID.top_of (Cilfacade.get_ikind typ)) (* query cycle *)
608609
end
609610
| exception Cilfacade.TypeOfError _ (* Bug: typeOffset: Field on a non-compound *)
610611
| _ -> eval_next ()
@@ -865,10 +866,10 @@ struct
865866
let query_evalint ask gs st e =
866867
if M.tracing then M.traceli "evalint" "base query_evalint %a\n" d_exp e;
867868
let r = match eval_rv_no_ask_evalint ask gs st e with
868-
| `Int i -> i (* cast should be unnecessary, eval_rv should guarantee right ikind already *)
869-
| `Bot -> Queries.ID.bot () (* TODO: remove? *)
870-
(* | v -> M.warn ("Query function answered " ^ (VD.show v)); Queries.Result.top q *)
871-
| v -> M.debug ~category:Analyzer "Base EvalInt %a query answering bot instead of %a" d_exp e VD.pretty v; Queries.ID.bot ()
869+
| `Int i -> `Lifted i (* cast should be unnecessary, eval_rv should guarantee right ikind already *)
870+
| `Bot -> Queries.ID.bot () (* TODO: remove? *)
871+
(* | v -> M.warn ("Query function answered " ^ (VD.show v)); Queries.Result.top q *)
872+
| v -> M.debug ~category:Analyzer "Base EvalInt %a query answering bot instead of %a" d_exp e VD.pretty v; Queries.ID.bot ()
872873
in
873874
if M.tracing then M.traceu "evalint" "base query_evalint %a -> %a\n" d_exp e Queries.ID.pretty r;
874875
r
@@ -934,7 +935,7 @@ struct
934935
let alen = List.filter_map (fun v -> lenOf v.vtype) (AD.to_var_may a) in
935936
let d = List.fold_left ID.join (ID.bot_of (Cilfacade.ptrdiff_ikind ())) (List.map (ID.of_int (Cilfacade.ptrdiff_ikind ()) %BI.of_int) (slen @ alen)) in
936937
(* ignore @@ printf "EvalLength %a = %a\n" d_exp e ID.pretty d; *)
937-
d
938+
`Lifted d
938939
| `Bot -> Queries.Result.bot q (* TODO: remove *)
939940
| _ -> Queries.Result.top q
940941
end
@@ -946,7 +947,7 @@ struct
946947
let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a None in
947948
(* ignore @@ printf "BlobSize %a = %a\n" d_plainexp e VD.pretty r; *)
948949
(match r with
949-
| `Blob (_,s,_) -> s
950+
| `Blob (_,s,_) -> `Lifted s
950951
| _ -> Queries.Result.top q)
951952
| _ -> Queries.Result.top q
952953
end

‎src/cdomains/apron/apronDomain.apron.ml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -632,13 +632,13 @@ struct
632632
match check_assert d e with
633633
| `True -> ID.of_bool ik true
634634
| `False -> ID.of_bool ik false
635-
| `Top -> ID.top ()
635+
| `Top -> ID.top_of ik
636636
else
637637
match eval_interval_expr d e with
638638
| (Some min, Some max) -> ID.of_interval ik (min, max)
639639
| (Some min, None) -> ID.starting ik min
640640
| (None, Some max) -> ID.ending ik max
641-
| (None, None) -> ID.top ()
641+
| (None, None) -> ID.top_of ik
642642
end
643643

644644

@@ -878,7 +878,7 @@ sig
878878
val assert_inv : t -> exp -> bool -> t
879879
val check_assert : t -> exp -> [> `False | `Top | `True ]
880880
val eval_interval_expr : t -> exp -> Z.t option * Z.t option
881-
val eval_int : t -> exp -> IntDomain.IntDomTuple.t
881+
val eval_int : t -> exp -> Queries.ID.t
882882
end
883883

884884
type ('a, 'b) aproncomponents_t = { apr : 'a; priv : 'b; } [@@deriving eq, ord, hash, to_yojson]

‎src/cdomains/intDomain.ml‎

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2536,7 +2536,24 @@ module IntDomTupleImpl = struct
25362536

25372537
let to_list x = Tuple4.enum x |> List.of_enum |> List.filter_map identity (* contains only the values of activated domains *)
25382538
let to_list_some x = List.filter_map identity @@ to_list x (* contains only the Some-values of activated domains *)
2539-
let exists, for_all = let f g = g identity % to_list in List.(f exists, f for_all)
2539+
2540+
let exists = function
2541+
| (Some true, _, _, _)
2542+
| (_, Some true, _, _)
2543+
| (_, _, Some true, _)
2544+
| (_, _, _, Some true) ->
2545+
true
2546+
| _ ->
2547+
false
2548+
2549+
let for_all = function
2550+
| (Some false, _, _, _)
2551+
| (_, Some false, _, _)
2552+
| (_, _, Some false, _)
2553+
| (_, _, _, Some false) ->
2554+
false
2555+
| _ ->
2556+
true
25402557

25412558
(* f0: constructors *)
25422559
let top () = create { fi = fun (type a) (module I:S with type t = a) -> I.top } ()

‎src/domains/hoareDomain.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -224,7 +224,7 @@ struct
224224
fold (fun other acc ->
225225
(dprintf "not leq %a because %a\n" B.pretty other B.pretty_diff (evil, other)) ++ acc
226226
) s2 nil
227-
with _ ->
227+
with Not_found ->
228228
dprintf "choose failed b/c of empty set s1: %d s2: %d"
229229
(cardinal s1)
230230
(cardinal s2)
@@ -336,7 +336,7 @@ struct
336336
fold' (fun other otherr acc ->
337337
(dprintf "not leq %a because %a\nand not mem %a because %a\n" SpecD.pretty other SpecD.pretty_diff (evil, other) R.pretty otherr R.pretty_diff (R.singleton evilr', otherr)) ++ acc
338338
) s2 nil
339-
with _ ->
339+
with Not_found ->
340340
dprintf "choose failed b/c of empty set s1: %d s2: %d"
341341
(cardinal s1)
342342
(cardinal s2)

‎src/domains/queries.ml‎

Lines changed: 28 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -5,30 +5,34 @@ open Cil
55
module GU = Goblintutil
66
module ID =
77
struct
8-
include IntDomain.IntDomTuple
9-
(* Special IntDomTuple that has _some_ top and bot which MCP2.query can use *)
10-
let top () = top_of IInt
11-
let is_top x = equal (top ()) x
12-
let bot () = bot_of IInt
13-
let is_bot x = equal (bot ()) x
14-
let join x y =
15-
if is_top x || is_top y then
16-
top ()
17-
else if is_bot x then
18-
y
19-
else if is_bot y then
20-
x
21-
else
22-
join x y
23-
let meet x y =
24-
if is_bot x || is_bot y then
25-
bot ()
26-
else if is_top x then
27-
y
28-
else if is_top y then
29-
x
30-
else
31-
meet x y
8+
module I = IntDomain.IntDomTuple
9+
include Lattice.Lift (I) (Printable.DefaultNames)
10+
11+
let lift op x = `Lifted (op x)
12+
let unlift op x = match x with
13+
| `Lifted x -> op x
14+
| _ -> failwith "Queries.ID.unlift"
15+
16+
let bot_of = lift I.bot_of
17+
let top_of = lift I.top_of
18+
19+
let of_int ik = lift (I.of_int ik)
20+
let of_bool ik = lift (I.of_bool ik)
21+
let of_interval ik = lift (I.of_interval ik)
22+
let of_excl_list ik = lift (I.of_excl_list ik)
23+
let of_congruence ik = lift (I.of_congruence ik)
24+
let starting ik = lift (I.starting ik)
25+
let ending ik = lift (I.ending ik)
26+
27+
let to_int x = unlift I.to_int x
28+
let is_int x = unlift I.is_int x
29+
let to_bool x = unlift I.to_bool x
30+
let is_bool x = unlift I.is_bool x
31+
32+
let is_bot_ikind = function
33+
| `Bot -> false
34+
| `Lifted x -> I.is_bot x
35+
| `Top -> false
3236
end
3337
module LS = SetDomain.ToppedSet (Lval.CilLval) (struct let topname = "All" end)
3438
module TS = SetDomain.ToppedSet (CilType.Typ) (struct let topname = "All" end)

‎src/transform/expressionEvaluation.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,7 @@ module ExpEval : Transform.S =
127127
(* Evaluable: Definite *)
128128
| Some x when Queries.ID.is_int x -> Some (Some (not(IntOps.BigIntOps.equal (Option.get @@ Queries.ID.to_int x) IntOps.BigIntOps.zero)))
129129
(* Inapplicable: Unreachable *)
130-
| Some x when Queries.ID.is_bot x -> None
130+
| Some x when Queries.ID.is_bot_ikind x -> None
131131
(* Evaluable: Inconclusive *)
132132
| Some x -> Some None
133133
(* Inapplicable: Unlisted *)

‎src/witness/witnessConstraints.ml‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,15 @@ struct
8888
let bot () = failwith "VIE bot"
8989
let is_bot _ = failwith "VIE is_bot"
9090

91-
let pretty_diff () _ = failwith "VIE pretty_diff"
91+
let pretty_diff () (((v, c, x'), e), ((w, d, y'), f)) =
92+
if not (Node.equal v w) then
93+
Pretty.dprintf "%a not equal %a" Node.pretty v Node.pretty w
94+
else if not (Spec.C.equal c d) then
95+
Pretty.dprintf "%a not equal %a" Spec.C.pretty c Spec.C.pretty d
96+
else if not (Edge.equal e f) then
97+
Pretty.dprintf "%a not equal %a" Edge.pretty e Edge.pretty f
98+
else
99+
I.pretty_diff () (x', y')
92100
end
93101
(* Bot is needed for Hoare widen *)
94102
(* TODO: could possibly rewrite Hoare to avoid introducing bots in widen which get reduced away anyway? *)

0 commit comments

Comments
 (0)