Merge pull request #1350 from goblint/rm-libmaincil

Adapt to removed `Libmaincil` module

goblint.opam

@@ -77,7 +77,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#d2760bacfbfdb25a374254de44f2ff1cb5f42abd" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

goblint.opam.locked

@@ -131,6 +131,10 @@ post-messages: [
 ]
 # TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
 pin-depends: [
+  [
+    "goblint-cil.2.0.3"
+    "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51"
+  ]
   [
     "ppx_deriving.5.2.1"
     "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"

goblint.opam.template

@@ -3,7 +3,7 @@
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#d2760bacfbfdb25a374254de44f2ff1cb5f42abd" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

src/analyses/base.ml

@@ -1020,7 +1020,7 @@ struct
     match ofs with
     | NoOffset -> `NoOffset
     | Field (fld, ofs) -> `Field (fld, convert_offset ~ctx st ofs)
-    | Index (exp, ofs) when CilType.Exp.equal exp Offset.Index.Exp.any -> (* special offset added by convertToQueryLval *)
+    | Index (exp, ofs) when CilType.Exp.equal exp (Lazy.force Offset.Index.Exp.any) -> (* special offset added by convertToQueryLval *)
       `Index (IdxDom.top (), convert_offset ~ctx st ofs)
     | Index (exp, ofs) ->
       match eval_rv ~ctx st exp with
@@ -2347,7 +2347,7 @@ struct
                | CArrays.IsNotSubstr -> Address (AD.null_ptr)
                | CArrays.IsSubstrAtIndex0 -> Address (eval_lv ~ctx st (mkMem ~addr:(Cil.stripCasts haystack) ~off:NoOffset))
                | CArrays.IsMaybeSubstr -> Address (AD.join (eval_lv ~ctx st
-                                                              (mkMem ~addr:(Cil.stripCasts haystack) ~off:(Index (Offset.Index.Exp.any, NoOffset)))) (AD.null_ptr)))
+                                                              (mkMem ~addr:(Cil.stripCasts haystack) ~off:(Index (Lazy.force Offset.Index.Exp.any, NoOffset)))) (AD.null_ptr)))
         | None -> st
       end
     | Strcmp { s1; s2; n }, _ ->

src/analyses/memOutOfBounds.ml

@@ -171,7 +171,7 @@ struct
       match ofs with
       | NoOffset -> `NoOffset
       | Field (fld, ofs) -> `Field (fld, convert_offset ofs)
-      | Index (exp, ofs) when CilType.Exp.equal exp Offset.Index.Exp.any -> (* special offset added by convertToQueryLval *)
+      | Index (exp, ofs) when CilType.Exp.equal exp (Lazy.force Offset.Index.Exp.any) -> (* special offset added by convertToQueryLval *)
         `Index (ID.top (), convert_offset ofs)
       | Index (exp, ofs) ->
         let i = match ctx.ask (Queries.EvalInt exp) with

src/cdomain/value/cdomains/arrayDomain.ml

@@ -140,7 +140,7 @@ struct
   let get ?(checkBounds=true) (ask: VDQ.t) a i = a
   let set (ask: VDQ.t) a (ie, i) v =
     match ie with
-    | Some ie when CilType.Exp.equal ie Offset.Index.Exp.all ->
+    | Some ie when CilType.Exp.equal ie (Lazy.force Offset.Index.Exp.all) ->
       v
     | _ ->
       join a v
@@ -164,7 +164,7 @@ struct
     match offset with
     (* invariants for all indices *)
     | NoOffset when get_bool "witness.invariant.goblint" ->
-      let i_lval = Cil.addOffsetLval (Index (Offset.Index.Exp.all, NoOffset)) lval in
+      let i_lval = Cil.addOffsetLval (Index (Lazy.force Offset.Index.Exp.all, NoOffset)) lval in
       value_invariant ~offset ~lval:i_lval x
     | NoOffset ->
       Invariant.none
@@ -246,7 +246,7 @@ struct
     else ((update_unrolled_values min_i (Z.of_int ((factor ())-1))), (Val.join xr v))
   let set ask (xl, xr) (ie, i) v =
     match ie with
-    | Some ie when CilType.Exp.equal ie Offset.Index.Exp.all ->
+    | Some ie when CilType.Exp.equal ie (Lazy.force Offset.Index.Exp.all) ->
       (* TODO: Doesn't seem to work for unassume because unrolled elements are top-initialized, not bot-initialized. *)
       (BatList.make (factor ()) v, v)
     | _ ->
@@ -279,7 +279,7 @@ struct
         if Val.is_bot xr then
           Invariant.top ()
         else if get_bool "witness.invariant.goblint" then (
-          let i_lval = Cil.addOffsetLval (Index (Offset.Index.Exp.all, NoOffset)) lval in
+          let i_lval = Cil.addOffsetLval (Index (Lazy.force Offset.Index.Exp.all, NoOffset)) lval in
           value_invariant ~offset ~lval:i_lval (join_of_all_parts x)
         )
         else
@@ -534,10 +534,10 @@ struct
   let set_with_length length (ask:VDQ.t) x (i,_) a =
     if M.tracing then M.trace "update_offset" "part array set_with_length %a %s %a\n" pretty x (BatOption.map_default Basetype.CilExp.show "None" i) Val.pretty a;
     match i with
-    | Some ie when CilType.Exp.equal ie Offset.Index.Exp.all ->
+    | Some ie when CilType.Exp.equal ie (Lazy.force Offset.Index.Exp.all) ->
       (* TODO: Doesn't seem to work for unassume. *)
       Joint a
-    | Some i when CilType.Exp.equal i Offset.Index.Exp.any ->
+    | Some i when CilType.Exp.equal i (Lazy.force Offset.Index.Exp.any) ->
       (assert !AnalysisState.global_initialization; (* just joining with xm here assumes that all values will be set, which is guaranteed during inits *)
        (* the join is needed here! see e.g 30/04 *)
        let o = match x with Partitioned (_, (_, xm, _)) -> xm | Joint v -> v in
@@ -818,7 +818,7 @@ struct
     match offset with
     (* invariants for all indices *)
     | NoOffset when get_bool "witness.invariant.goblint" ->
-      let i_lval = Cil.addOffsetLval (Index (Offset.Index.Exp.all, NoOffset)) lval in
+      let i_lval = Cil.addOffsetLval (Index (Lazy.force Offset.Index.Exp.all, NoOffset)) lval in
       value_invariant ~offset ~lval:i_lval (join_of_all_parts x)
     | NoOffset ->
       Invariant.none

src/cdomain/value/cdomains/offset.ml

@@ -23,11 +23,11 @@ struct
     let name () = "exp index"
 
     let any = Cilfacade.any_index_exp
-    let all = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index")
+    let all = lazy (CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index"))
 
     (* Override output *)
     let pretty () x =
-      if equal x any then
+      if equal x (Lazy.force any) then
         Pretty.text "?"
       else
         dn_exp () x
@@ -41,7 +41,7 @@ struct
 
     let equal_to _ _ = `Top (* TODO: more precise for definite indices *)
     let to_int _ = None (* TODO: more precise for definite indices *)
-    let top () = any
+    let top () = Lazy.force any
   end
 end
 
@@ -108,7 +108,7 @@ struct
     | `Index (i,o) ->
       let i_exp = match Idx.to_int i with
         | Some i -> Const (CInt (i, Cilfacade.ptrdiff_ikind (), Some (Z.to_string i)))
-        | None -> Index.Exp.any
+        | None -> Lazy.force Index.Exp.any
       in
       `Index (i_exp, to_exp o)
     | `Field (f,o) -> `Field (f, to_exp o)
@@ -118,7 +118,7 @@ struct
     | `Index (i,o) ->
       let i_exp = match Idx.to_int i with
         | Some i -> Const (CInt (i, Cilfacade.ptrdiff_ikind (), Some (Z.to_string i)))
-        | None -> Index.Exp.any
+        | None -> Lazy.force Index.Exp.any
       in
       Index (i_exp, to_cil o)
     | `Field (f,o) -> Field (f, to_cil o)

src/cdomain/value/cdomains/offset_intf.ml

@@ -129,12 +129,12 @@ sig
       (** Special index expression for some unknown index.
           Weakly updates array in assignment.
           Used for [exp.fast_global_inits]. *)
-      val any: GoblintCil.exp
+      val any: GoblintCil.exp Lazy.t
 
       (** Special index expression for all indices.
           Strongly updates array in assignment.
           Used for Goblint-specific witness invariants. *)
-      val all: GoblintCil.exp
+      val all: GoblintCil.exp Lazy.t
     end
   end
 

src/common/framework/cfgTools.ml

@@ -680,7 +680,7 @@ let getGlobalInits (file: file) : edges  =
       lval
     in
     let rec any_index_offset = function
-      | Index (e,o) -> Index (Cilfacade.any_index_exp, any_index_offset o)
+      | Index (e,o) -> Index (Lazy.force Cilfacade.any_index_exp, any_index_offset o)
       | Field (f,o) -> Field (f, any_index_offset o)
       | NoOffset -> NoOffset
     in

src/common/util/cilfacade.ml

@@ -712,4 +712,4 @@ let add_function_declarations (file: Cil.file): unit =
 (** Special index expression for some unknown index.
     Weakly updates array in assignment.
     Used for [exp.fast_global_inits]. *)
-let any_index_exp = CastE (TInt (ptrdiff_ikind (), []), mkString "any_index") (* TODO: move back to Offset *)
+let any_index_exp = lazy (CastE (TInt (ptrdiff_ikind (), []), mkString "any_index")) (* TODO: move back to Offset *)

unittest/cdomains/lvalTest.ml

@@ -6,6 +6,8 @@ module ID = IntDomain.IntDomWithDefaultIkind (IntDomain.IntDomLifter (IntDomain.
 module Offs = Offset.MakeLattice (ID)
 module LV = AddressDomain.AddressLattice (Mval.MakeLattice (Offs))
 
+let () = Cilfacade.init () (* ensure ptrdiff ikind is available *)
+
 let ikind = IntDomain.PtrDiffIkind.ikind ()
 
 let a_var = Cil.makeGlobalVar "a" Cil.intPtrType

unittest/dune

@@ -2,7 +2,7 @@
 
 (test
   (name mainTest)
-  (libraries ounit2 qcheck-ounit goblint.std goblint.lib goblint.constraint goblint.solver goblint.cdomain.value goblint.sites.dune goblint.build-info.dune)
+  (libraries ounit2 qcheck-ounit goblint.std goblint.common goblint.lib goblint.constraint goblint.solver goblint.cdomain.value goblint.sites.dune goblint.build-info.dune)
   (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson))
   (flags :standard -linkall))