Skip to content

Commit af3a1d5

Browse files
sim642sim642
committed
Extract Invariant.Exp module
1 parent 0dcc2c8 commit af3a1d5

File tree

4 files changed

+65
-61
lines changed

4 files changed

+65
-61
lines changed

‎src/cdomain/value/domains/invariant.ml‎

Lines changed: 45 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@
33
open GoblintCil
44

55
(** Symbolic (and fully syntactic) expression "lattice". *)
6-
module ExpLat =
6+
module Exp =
77
struct
88
include CilType.Exp
9+
(* This type is abstract in the interface because invariant expressions may be optimized for readability but lack implicit casts, etc, which are required to normally use CIL exp-s in Goblint. *)
910

1011
let bot () = zero (* false *)
1112
let top () = one (* true *)
@@ -22,51 +23,50 @@ struct
2223
let meet x y = BinOp (LAnd, x, y, intType)
2324
let widen x y = y
2425
let narrow = meet
25-
end
2626

27-
type exp = GoblintCil.exp (* This is abstract in the interface because invariant expressions may be optimized for readability but lack implicit casts, etc, which are required to normally use CIL exp-s in Goblint. *)
28-
let show_exp = ExpLat.show
29-
let exp_to_cil = Fun.id
30-
31-
module ES = SetDomain.Make (ExpLat)
32-
33-
(* Turns an expression into alist of conjuncts, pulling out common conjuncts from top-level disjunctions *)
34-
let rec pullOutCommonConjuncts e =
35-
let rec to_conjunct_set = function
36-
| Cil.BinOp(LAnd,e1,e2,_) -> ES.join (to_conjunct_set e1) (to_conjunct_set e2)
37-
| e -> ES.singleton e
38-
in
39-
let combine_conjuncts es = ES.fold (fun e acc -> match acc with | None -> Some e | Some acce -> Some (BinOp(LAnd,acce,e,Cil.intType))) es None in
40-
match e with
41-
| Cil.BinOp(LOr, e1, e2,t) ->
42-
let e1s = pullOutCommonConjuncts e1 in
43-
let e2s = pullOutCommonConjuncts e2 in
44-
let common = ES.inter e1s e2s in
45-
let e1s' = ES.diff e1s e2s in
46-
let e2s' = ES.diff e2s e1s in
47-
(match combine_conjuncts e1s', combine_conjuncts e2s' with
48-
| Some e1e, Some e2e -> ES.add (BinOp(LOr,e1e,e2e,Cil.intType)) common
49-
| _ -> common (* if one of the disjuncts is empty, it is equivalent to true here *)
50-
)
51-
| e -> to_conjunct_set e
52-
53-
let process_exp inv =
54-
let exp_deep_unroll_types =
55-
if GobConfig.get_bool "witness.invariant.typedefs" then
56-
Fun.id
27+
let to_cil = Fun.id
28+
29+
30+
module ES = SetDomain.Make (CilType.Exp)
31+
32+
(* Turns an expression into alist of conjuncts, pulling out common conjuncts from top-level disjunctions *)
33+
let rec pullOutCommonConjuncts e =
34+
let rec to_conjunct_set = function
35+
| Cil.BinOp(LAnd,e1,e2,_) -> ES.join (to_conjunct_set e1) (to_conjunct_set e2)
36+
| e -> ES.singleton e
37+
in
38+
let combine_conjuncts es = ES.fold (fun e acc -> match acc with | None -> Some e | Some acce -> Some (BinOp(LAnd,acce,e,Cil.intType))) es None in
39+
match e with
40+
| Cil.BinOp(LOr, e1, e2,t) ->
41+
let e1s = pullOutCommonConjuncts e1 in
42+
let e2s = pullOutCommonConjuncts e2 in
43+
let common = ES.inter e1s e2s in
44+
let e1s' = ES.diff e1s e2s in
45+
let e2s' = ES.diff e2s e1s in
46+
(match combine_conjuncts e1s', combine_conjuncts e2s' with
47+
| Some e1e, Some e2e -> ES.add (BinOp(LOr,e1e,e2e,Cil.intType)) common
48+
| _ -> common (* if one of the disjuncts is empty, it is equivalent to true here *)
49+
)
50+
| e -> to_conjunct_set e
51+
52+
let process inv =
53+
let exp_deep_unroll_types =
54+
if GobConfig.get_bool "witness.invariant.typedefs" then
55+
Fun.id
56+
else
57+
InvariantCil.exp_deep_unroll_types
58+
in
59+
let inv' =
60+
inv
61+
|> exp_deep_unroll_types
62+
|> InvariantCil.exp_replace_original_name
63+
in
64+
if GobConfig.get_bool "witness.invariant.split-conjunction" then
65+
ES.elements (pullOutCommonConjuncts inv')
66+
|> List.filter (Fun.negate InvariantCil.exp_contains_anon_type)
5767
else
58-
InvariantCil.exp_deep_unroll_types
59-
in
60-
let inv' =
61-
inv
62-
|> exp_deep_unroll_types
63-
|> InvariantCil.exp_replace_original_name
64-
in
65-
if GobConfig.get_bool "witness.invariant.split-conjunction" then
66-
ES.elements (pullOutCommonConjuncts inv')
67-
|> List.filter (Fun.negate InvariantCil.exp_contains_anon_type)
68-
else
69-
[inv']
68+
[inv']
69+
end
7070

7171

7272
(** Lift {!ExpLat} such that join/meet folds don't introduce excessive [|| 0|] or [&& 1] expressions. *)
@@ -78,7 +78,7 @@ struct
7878
let top_name = "true"
7979
end
8080

81-
include Lattice.LiftConf (N) (ExpLat)
81+
include Lattice.LiftConf (N) (Exp)
8282

8383
let none = top ()
8484
let of_exp = lift

‎src/cdomain/value/domains/invariant.mli‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,17 @@
11
(** Invariants for witnesses. *)
22

3-
type exp
4-
val show_exp: exp -> string
5-
val exp_to_cil: exp -> GoblintCil.exp
6-
(** Breaks abstraction, only for use in {!EvalAssert}! *)
3+
module Exp:
4+
sig
5+
include Printable.S
76

8-
include Lattice.S with type t = [ `Bot | `Lifted of exp | `Top ]
7+
val process: t -> t list
98

10-
val process_exp: exp -> exp list
9+
val to_cil: t -> GoblintCil.exp
10+
(** Breaks abstraction, only for use in {!EvalAssert}! *)
11+
end
12+
13+
14+
include Lattice.S with type t = [ `Bot | `Lifted of Exp.t | `Top ]
1115

1216
val none: t
1317
val of_exp: GoblintCil.exp -> t

‎src/transform/evalAssert.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -60,8 +60,8 @@ struct
6060
let context = {Invariant.default_context with lvals} in
6161
match (ask ~node loc).f (Queries.Invariant context) with
6262
| `Lifted e ->
63-
let es = Invariant.process_exp e in
64-
let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv assert_function); ("exp", Fe (Invariant.exp_to_cil e))]) es in
63+
let es = Invariant.Exp.process e in
64+
let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv assert_function); ("exp", Fe (Invariant.Exp.to_cil e))]) es in
6565
if surroundByAtomic then
6666
let abegin = (cInstr ("%v:__VERIFIER_atomic_begin();") loc [("__VERIFIER_atomic_begin", Fv atomicBegin)]) in
6767
let aend = (cInstr ("%v:__VERIFIER_atomic_end();") loc [("__VERIFIER_atomic_end", Fv atomicEnd)]) in

‎src/witness/yamlWitness.ml‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -232,7 +232,7 @@ struct
232232
(* Currently same invariants (from InvariantGlobal query) for all nodes (from InvariantGlobalNodes query).
233233
The alternative would be querying InvariantGlobal per local unknown when looping over them to generate location invariants.
234234
See: https://github.com/goblint/analyzer/pull/1394#discussion_r1698149514. *)
235-
let invs = Invariant.process_exp inv in
235+
let invs = Invariant.Exp.process inv in
236236
Queries.NS.fold (fun n acc ->
237237
let fundec = Node.find_fundec n in
238238
match WitnessInvariant.location_location n with (* Not just using Node.location because it returns expression location which may be invalid for location invariant (e.g. inside conditional). *)
@@ -293,9 +293,9 @@ struct
293293
let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
294294
let location_function = fundec.svar.vname in
295295
let location = Entry.location ~location:loc ~location_function in
296-
let invs = Invariant.process_exp inv in
296+
let invs = Invariant.Exp.process inv in
297297
List.fold_left (fun acc inv ->
298-
let invariant = Invariant.show_exp inv in
298+
let invariant = Invariant.Exp.show inv in
299299
let invariant = Entry.location_invariant ~location ~invariant in
300300
incr cnt_location_invariant;
301301
invariant :: acc
@@ -323,9 +323,9 @@ struct
323323
let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
324324
let location_function = fundec.svar.vname in
325325
let location = Entry.location ~location:loc ~location_function in
326-
let invs = Invariant.process_exp inv in
326+
let invs = Invariant.Exp.process inv in
327327
List.fold_left (fun acc inv ->
328-
let invariant = Invariant.show_exp inv in
328+
let invariant = Invariant.Exp.show inv in
329329
let invariant = Entry.loop_invariant ~location ~invariant in
330330
incr cnt_loop_invariant;
331331
invariant :: acc
@@ -349,17 +349,17 @@ struct
349349
| `Left g -> (* global unknown from analysis Spec *)
350350
begin match R.ask_global (InvariantGlobal (Obj.repr g)), GobConfig.get_string "witness.invariant.flow_insensitive-as" with
351351
| `Lifted inv, "invariant_set-flow_insensitive_invariant" ->
352-
let invs = Invariant.process_exp inv in
352+
let invs = Invariant.Exp.process inv in
353353
List.fold_left (fun acc inv ->
354-
let invariant = Invariant.show_exp inv in
354+
let invariant = Invariant.Exp.show inv in
355355
let invariant = Entry.flow_insensitive_invariant ~invariant in
356356
incr cnt_flow_insensitive_invariant;
357357
invariant :: acc
358358
) acc invs
359359
| `Lifted inv, "invariant_set-location_invariant" ->
360360
(* TODO: fold_flow_insensitive_as_location is now only used here, inline/move? *)
361361
fold_flow_insensitive_as_location ~inv (fun ~location ~inv acc ->
362-
let invariant = Invariant.show_exp inv in
362+
let invariant = Invariant.Exp.show inv in
363363
let invariant = Entry.location_invariant ~location ~invariant in
364364
incr cnt_location_invariant;
365365
invariant :: acc

0 commit comments

Comments
 (0)