Merge pull request #1668 from goblint/invariant-mli

Add abstract interface to `Invariant`

Author: sim642

src/cdomain/value/domains/invariant.ml

@@ -1,11 +1,10 @@
-(** Invariants for witnesses. *)
-
 open GoblintCil
 
 (** Symbolic (and fully syntactic) expression "lattice". *)
-module ExpLat =
+module Exp =
 struct
   include CilType.Exp
+  (* 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. *)
 
   let bot () = zero (* false *)
   let top () = one (* true *)
@@ -22,8 +21,52 @@ struct
   let meet x y = BinOp (LAnd, x, y, intType)
   let widen x y = y
   let narrow = meet
+
+  let to_cil = Fun.id
+
+
+  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 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
 
+
 (** Lift {!ExpLat} such that join/meet folds don't introduce excessive [|| 0|] or [&& 1] expressions. *)
 
 module N =
@@ -33,7 +76,7 @@ struct
   let top_name = "true"
 end
 
-include Lattice.LiftConf (N) (ExpLat)
+include Lattice.LiftConf (N) (Exp)
 
 let none = top ()
 let of_exp = lift

src/cdomain/value/domains/invariant.mli

@@ -0,0 +1,28 @@
+(** Invariants for witnesses. *)
+
+module Exp:
+sig
+  include Printable.S
+
+  val process: t -> t list
+
+  val to_cil: t -> GoblintCil.exp
+  (** Breaks abstraction, only for use in {!EvalAssert}! *)
+end
+
+
+include Lattice.S with type t = [ `Bot | `Lifted of Exp.t | `Top ]
+
+val none: t
+val of_exp: GoblintCil.exp -> t
+
+val (&&): t -> t -> t
+val (||): t -> t -> t
+
+
+type context = {
+  path: int option;
+  lvals: Lval.Set.t;
+}
+
+val default_context : context

src/transform/evalAssert.ml

@@ -60,8 +60,8 @@ 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 asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv assert_function); ("exp", Fe e)]) es in
+          let es = Invariant.Exp.process e in
+          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
           if surroundByAtomic then
             let abegin = (cInstr ("%v:__VERIFIER_atomic_begin();") loc [("__VERIFIER_atomic_begin", Fv atomicBegin)]) in
             let aend = (cInstr ("%v:__VERIFIER_atomic_end();") loc [("__VERIFIER_atomic_end", Fv atomicEnd)]) 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.Exp.process 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,9 +293,9 @@ 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.Exp.process inv in
                   List.fold_left (fun acc inv ->
-                      let invariant = CilType.Exp.show inv in
+                      let invariant = Invariant.Exp.show inv in
                       let invariant = Entry.location_invariant ~location ~invariant in
                       incr cnt_location_invariant;
                       invariant :: acc
@@ -323,9 +323,9 @@ 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.Exp.process inv in
                     List.fold_left (fun acc inv ->
-                        let invariant = CilType.Exp.show inv in
+                        let invariant = Invariant.Exp.show inv in
                         let invariant = Entry.loop_invariant ~location ~invariant in
                         incr cnt_loop_invariant;
                         invariant :: acc
@@ -349,17 +349,17 @@ 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.Exp.process inv in
                       List.fold_left (fun acc inv ->
-                          let invariant = CilType.Exp.show inv in
+                          let invariant = Invariant.Exp.show inv in
                           let invariant = Entry.flow_insensitive_invariant ~invariant in
                           incr cnt_flow_insensitive_invariant;
                           invariant :: acc
                         ) acc invs
                     | `Lifted inv, "invariant_set-location_invariant" ->
                       (* TODO: fold_flow_insensitive_as_location is now only used here, inline/move? *)
                       fold_flow_insensitive_as_location ~inv (fun ~location ~inv acc ->
-                          let invariant = CilType.Exp.show inv in
+                          let invariant = Invariant.Exp.show inv in
                           let invariant = Entry.location_invariant ~location ~invariant in
                           incr cnt_location_invariant;
                           invariant :: acc