Abstract Invariant.exp

Author: sim642

src/cdomain/value/domains/invariant.ml

@@ -24,6 +24,10 @@ struct
   let narrow = meet
 end
 
+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. *)
+let show_exp = ExpLat.show
+let exp_to_cil = Fun.id
+
 module ES = SetDomain.Make (ExpLat)
 
 (* Turns an expression into alist of conjuncts, pulling out common conjuncts from top-level disjunctions *)

src/cdomain/value/domains/invariant.mli

@@ -1,8 +1,13 @@
 (** Invariants for witnesses. *)
 
-include Lattice.S with type t = [ `Bot | `Lifted of GoblintCil.exp | `Top ]
+type exp
+val show_exp: exp -> string
+val exp_to_cil: exp -> GoblintCil.exp
+(** Breaks abstraction, only for use in {!EvalAssert}! *)
 
-val process_exp: GoblintCil.exp -> GoblintCil.exp list
+include Lattice.S with type t = [ `Bot | `Lifted of exp | `Top ]
+
+val process_exp: exp -> exp list
 
 val none: t
 val of_exp: GoblintCil.exp -> t

src/transform/evalAssert.ml

@@ -61,7 +61,7 @@ struct
         match (ask ~node loc).f (Queries.Invariant context) with
         | `Lifted e ->
           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
+          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/yamlWitness.ml

@@ -295,7 +295,7 @@ struct
                   let location = Entry.location ~location:loc ~location_function in
                   let invs = Invariant.process_exp inv in
                   List.fold_left (fun acc inv ->
-                      let invariant = CilType.Exp.show inv in
+                      let invariant = Invariant.show_exp inv in
                       let invariant = Entry.location_invariant ~location ~invariant in
                       incr cnt_location_invariant;
                       invariant :: acc
@@ -325,7 +325,7 @@ struct
                     let location = Entry.location ~location:loc ~location_function in
                     let invs = Invariant.process_exp inv in
                     List.fold_left (fun acc inv ->
-                        let invariant = CilType.Exp.show inv in
+                        let invariant = Invariant.show_exp inv in
                         let invariant = Entry.loop_invariant ~location ~invariant in
                         incr cnt_loop_invariant;
                         invariant :: acc
@@ -351,15 +351,15 @@ struct
                     | `Lifted inv, "invariant_set-flow_insensitive_invariant" ->
                       let invs = Invariant.process_exp inv in
                       List.fold_left (fun acc inv ->
-                          let invariant = CilType.Exp.show inv in
+                          let invariant = Invariant.show_exp 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.show_exp inv in
                           let invariant = Entry.location_invariant ~location ~invariant in
                           incr cnt_location_invariant;
                           invariant :: acc