Move WitnessUtil.InvariantExp into Invariant module

Author: sim642

src/cdomain/value/domains/invariant.ml

@@ -24,6 +24,47 @@ struct
   let narrow = meet
 end
 
+module ES = SetDomain.Make (ExpLat)
+
+(* Turns an expression into alist of conjuncts, pulling out common conjuncts from top-level disjunctions *)
+let rec pullOutCommonConjuncts e =
+  let rec to_conjunct_set = function
+    | Cil.BinOp(LAnd,e1,e2,_) -> ES.join (to_conjunct_set e1) (to_conjunct_set e2)
+    | e -> ES.singleton e
+  in
+  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
+  match e with
+  | Cil.BinOp(LOr, e1, e2,t) ->
+    let e1s = pullOutCommonConjuncts e1 in
+    let e2s = pullOutCommonConjuncts e2 in
+    let common = ES.inter e1s e2s in
+    let e1s' = ES.diff e1s e2s in
+    let e2s' = ES.diff e2s e1s in
+    (match combine_conjuncts e1s', combine_conjuncts e2s' with
+     | Some e1e, Some e2e -> ES.add (BinOp(LOr,e1e,e2e,Cil.intType)) common
+     | _ -> common (* if one of the disjuncts is empty, it is equivalent to true here *)
+    )
+  | e -> to_conjunct_set e
+
+let process_exp inv =
+  let exp_deep_unroll_types =
+    if GobConfig.get_bool "witness.invariant.typedefs" then
+      Fun.id
+    else
+      InvariantCil.exp_deep_unroll_types
+  in
+  let inv' =
+    inv
+    |> exp_deep_unroll_types
+    |> InvariantCil.exp_replace_original_name
+  in
+  if GobConfig.get_bool "witness.invariant.split-conjunction" then
+    ES.elements (pullOutCommonConjuncts inv')
+    |> List.filter (Fun.negate InvariantCil.exp_contains_anon_type)
+  else
+    [inv']
+
+
 (** Lift {!ExpLat} such that join/meet folds don't introduce excessive [|| 0|] or [&& 1] expressions. *)
 
 module N =

src/cdomain/value/domains/invariant.mli

@@ -2,6 +2,8 @@
 
 include Lattice.S with type t = [ `Bot | `Lifted of GoblintCil.exp | `Top ]
 
+val process_exp: GoblintCil.exp -> GoblintCil.exp list
+
 val none: t
 val of_exp: GoblintCil.exp -> t
 

src/transform/evalAssert.ml

@@ -60,7 +60,7 @@ struct
         let context = {Invariant.default_context with lvals} in
         match (ask ~node loc).f (Queries.Invariant context) with
         | `Lifted e ->
-          let es = WitnessUtil.InvariantExp.process_exp e in
+          let es = Invariant.process_exp e in
           let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv assert_function); ("exp", Fe e)]) es in
           if surroundByAtomic then
             let abegin = (cInstr ("%v:__VERIFIER_atomic_begin();") loc [("__VERIFIER_atomic_begin", Fv atomicBegin)]) in

src/witness/witnessUtil.ml

@@ -139,48 +139,6 @@ struct
 end
 [@@deprecated]
 
-module InvariantExp =
-struct
-  module ES = SetDomain.Make (CilType.Exp)
-
-  (* Turns an expression into alist of conjuncts, pulling out common conjuncts from top-level disjunctions *)
-  let rec pullOutCommonConjuncts e =
-    let rec to_conjunct_set = function
-      | Cil.BinOp(LAnd,e1,e2,_) -> ES.join (to_conjunct_set e1) (to_conjunct_set e2)
-      | e -> ES.singleton e
-    in
-    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
-    match e with
-    | Cil.BinOp(LOr, e1, e2,t) ->
-      let e1s = pullOutCommonConjuncts e1 in
-      let e2s = pullOutCommonConjuncts e2 in
-      let common = ES.inter e1s e2s in
-      let e1s' = ES.diff e1s e2s in
-      let e2s' = ES.diff e2s e1s in
-      (match combine_conjuncts e1s', combine_conjuncts e2s' with
-       | Some e1e, Some e2e -> ES.add (BinOp(LOr,e1e,e2e,Cil.intType)) common
-       | _ -> common (* if one of the disjuncts is empty, it is equivalent to true here *)
-      )
-    | e -> to_conjunct_set e
-
-  let process_exp inv =
-    let exp_deep_unroll_types =
-      if GobConfig.get_bool "witness.invariant.typedefs" then
-        Fun.id
-      else
-        InvariantCil.exp_deep_unroll_types
-    in
-    let inv' =
-      inv
-      |> exp_deep_unroll_types
-      |> InvariantCil.exp_replace_original_name
-    in
-    if GobConfig.get_bool "witness.invariant.split-conjunction" then
-      ES.elements (pullOutCommonConjuncts inv')
-      |> List.filter (Fun.negate InvariantCil.exp_contains_anon_type)
-    else
-      [inv']
-end
 
 module InvariantParser =
 struct

src/witness/yamlWitness.ml

@@ -232,7 +232,7 @@ struct
       (* Currently same invariants (from InvariantGlobal query) for all nodes (from InvariantGlobalNodes query).
          The alternative would be querying InvariantGlobal per local unknown when looping over them to generate location invariants.
          See: https://github.com/goblint/analyzer/pull/1394#discussion_r1698149514. *)
-      let invs = WitnessUtil.InvariantExp.process_exp inv in
+      let invs = Invariant.process_exp inv in
       Queries.NS.fold (fun n acc ->
           let fundec = Node.find_fundec n in
           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,7 +293,7 @@ struct
                   let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
                   let location_function = fundec.svar.vname in
                   let location = Entry.location ~location:loc ~location_function in
-                  let invs = WitnessUtil.InvariantExp.process_exp inv in
+                  let invs = Invariant.process_exp inv in
                   List.fold_left (fun acc inv ->
                       let invariant = CilType.Exp.show inv in
                       let invariant = Entry.location_invariant ~location ~invariant in
@@ -323,7 +323,7 @@ struct
                     let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
                     let location_function = fundec.svar.vname in
                     let location = Entry.location ~location:loc ~location_function in
-                    let invs = WitnessUtil.InvariantExp.process_exp inv in
+                    let invs = Invariant.process_exp inv in
                     List.fold_left (fun acc inv ->
                         let invariant = CilType.Exp.show inv in
                         let invariant = Entry.loop_invariant ~location ~invariant in
@@ -349,7 +349,7 @@ struct
                 | `Left g -> (* global unknown from analysis Spec *)
                   begin match R.ask_global (InvariantGlobal (Obj.repr g)), GobConfig.get_string "witness.invariant.flow_insensitive-as" with
                     | `Lifted inv, "invariant_set-flow_insensitive_invariant" ->
-                      let invs = WitnessUtil.InvariantExp.process_exp inv in
+                      let invs = Invariant.process_exp inv in
                       List.fold_left (fun acc inv ->
                           let invariant = CilType.Exp.show inv in
                           let invariant = Entry.flow_insensitive_invariant ~invariant in