Merge pull request #1288 from goblint/goblint-dune-libs-2

Organize more common modules into dune libraries

.github/workflows/options.yml

@@ -26,10 +26,10 @@ jobs:
         run: npm install -g ajv-cli
 
       - name: Migrate schema # https://github.com/ajv-validator/ajv-cli/issues/199
-        run: ajv migrate -s src/common/util/options.schema.json
+        run: ajv migrate -s src/config/options.schema.json
 
       - name: Validate conf
-        run: ajv validate -s src/common/util/options.schema.json -d "conf/**/*.json"
+        run: ajv validate -s src/config/options.schema.json -d "conf/**/*.json"
 
       - name: Validate incremental tests
-        run: ajv validate -s src/common/util/options.schema.json -d "tests/incremental/*/*.json"
+        run: ajv validate -s src/config/options.schema.json -d "tests/incremental/*/*.json"

.readthedocs.yaml

@@ -20,4 +20,4 @@ build:
       - pip install json-schema-for-humans
     post_build:
       - mkdir _readthedocs/html/jsfh/
-      - generate-schema-doc --config-file jsfh.yml src/common/util/options.schema.json _readthedocs/html/jsfh/
+      - generate-schema-doc --config-file jsfh.yml src/config/options.schema.json _readthedocs/html/jsfh/

docs/user-guide/configuring.md

@@ -24,7 +24,7 @@ In `.vscode/settings.json` add the following:
                 "/conf/*.json",
                 "/tests/incremental/*/*.json"
             ],
-            "url": "/src/common/util/options.schema.json"
+            "url": "/src/config/options.schema.json"
         }
     ]
 }

src/analyses/basePriv.ml

@@ -230,7 +230,7 @@ struct
       CPA.find x st.cpa
   (* let read_global ask getg cpa x =
      let (cpa', v) as r = read_global ask getg cpa x in
-     ignore (Pretty.printf "READ GLOBAL %a (%a, %B) = %a\n" CilType.Varinfo.pretty x CilType.Location.pretty !Tracing.current_loc (is_unprotected ask x) VD.pretty v);
+     ignore (Pretty.printf "READ GLOBAL %a (%a, %B) = %a\n" CilType.Varinfo.pretty x CilType.Location.pretty !Goblint_tracing.current_loc (is_unprotected ask x) VD.pretty v);
      r *)
   let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
     let cpa' = CPA.add x v st.cpa in
@@ -1665,7 +1665,7 @@ struct
   let read_global ask getg st x =
     let v = Priv.read_global ask getg st x in
     if !AnalysisState.postsolving && !is_dumping then
-      LVH.modify_def (VD.bot ()) (!Tracing.current_loc, x) (VD.join v) lvh;
+      LVH.modify_def (VD.bot ()) (!Goblint_tracing.current_loc, x) (VD.join v) lvh;
     v
 
   let dump () =

src/analyses/extractPthread.ml

@@ -220,7 +220,7 @@ module Tbls = struct
       let make_new_val table k =
         (* TODO: all same key occurrences instead *)
         let line = -5 - all_keys_count table in
-        let loc = { !Tracing.current_loc with line } in
+        let loc = { !Goblint_tracing.current_loc with line } in
         MyCFG.Statement
           { (mkStmtOneInstr @@ Set (var dummyFunDec.svar, zero, loc, loc)) with
             sid = new_sid ()

src/analyses/mCPRegistry.ml

@@ -215,7 +215,7 @@ struct
 
   let arbitrary () =
     let arbs = map (fun (n, (module D: Printable.S)) -> QCheck.map ~rev:(fun (_, o) -> obj o) (fun x -> (n, repr x)) @@ D.arbitrary ()) @@ domain_list () in
-    MyCheck.Arbitrary.sequence arbs
+    GobQCheck.Arbitrary.sequence arbs
 
   let relift = unop_map (fun (module S: Printable.S) x -> Obj.repr (S.relift (Obj.obj x)))
 end

src/analyses/stackTrace.ml

@@ -36,7 +36,7 @@ struct
   (* transfer functions *)
 
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    [ctx.local, D.push !Tracing.current_loc ctx.local]
+    [ctx.local, D.push !Goblint_tracing.current_loc ctx.local]
 
   let combine_env ctx lval fexp f args fc au f_ask =
     ctx.local (* keep local as opposed to IdentitySpec *)
@@ -46,7 +46,7 @@ struct
   let exitstate  v = D.top ()
 
   let threadenter ctx ~multiple lval f args =
-    [D.push !Tracing.current_loc ctx.local]
+    [D.push !Goblint_tracing.current_loc ctx.local]
 end
 
 

src/cdomains/intDomain.ml

@@ -996,12 +996,12 @@ struct
 
   let arbitrary ik =
     let open QCheck.Iter in
-    (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint MyCheck.Arbitrary.big_int in *)
+    (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint GobQCheck.Arbitrary.big_int in *)
     (* TODO: apparently bigints are really slow compared to int64 for domaintest *)
-    let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 in
+    let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in
     let pair_arb = QCheck.pair int_arb int_arb in
     let shrink = function
-      | Some (l, u) -> (return None) <+> (MyCheck.shrink pair_arb (l, u) >|= of_interval ik >|= fst)
+      | Some (l, u) -> (return None) <+> (GobQCheck.shrink pair_arb (l, u) >|= of_interval ik >|= fst)
       | None -> empty
     in
     QCheck.(set_shrink shrink @@ set_print show @@ map (*~rev:BatOption.get*) (fun x -> of_interval ik x |> fst ) pair_arb)
@@ -1601,13 +1601,13 @@ struct
 
   let arbitrary ik =
     let open QCheck.Iter in
-    (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint MyCheck.Arbitrary.big_int in *)
+    (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint GobQCheck.Arbitrary.big_int in *)
     (* TODO: apparently bigints are really slow compared to int64 for domaintest *)
-    let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 in
+    let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in
     let pair_arb = QCheck.pair int_arb int_arb in
     let list_pair_arb = QCheck.small_list pair_arb in
     let canonize_randomly_generated_list = (fun x -> norm_intvs ik  x |> fst) in
-    let shrink xs = MyCheck.shrink list_pair_arb xs >|= canonize_randomly_generated_list
+    let shrink xs = GobQCheck.shrink list_pair_arb xs >|= canonize_randomly_generated_list
     in QCheck.(set_shrink shrink @@ set_print show @@ map (*~rev:BatOption.get*) canonize_randomly_generated_list list_pair_arb)
 end
 
@@ -1695,7 +1695,7 @@ struct
   let logand n1 n2 = of_bool ((to_bool' n1) && (to_bool' n2))
   let logor  n1 n2 = of_bool ((to_bool' n1) || (to_bool' n2))
   let cast_to ?torg t x =  failwith @@ "Cast_to not implemented for " ^ (name ()) ^ "."
-  let arbitrary ik = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 (* TODO: use ikind *)
+  let arbitrary ik = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 (* TODO: use ikind *)
   let invariant _ _ = Invariant.none (* TODO *)
 end
 
@@ -2402,8 +2402,8 @@ struct
     let excluded s = from_excl ik s in
     let definite x = of_int ik x in
     let shrink = function
-      | `Excluded (s, _) -> MyCheck.shrink (S.arbitrary ()) s >|= excluded (* S TODO: possibly shrink excluded to definite *)
-      | `Definite x -> (return `Bot) <+> (MyCheck.shrink (BigInt.arbitrary ()) x >|= definite)
+      | `Excluded (s, _) -> GobQCheck.shrink (S.arbitrary ()) s >|= excluded (* S TODO: possibly shrink excluded to definite *)
+      | `Definite x -> (return `Bot) <+> (GobQCheck.shrink (BigInt.arbitrary ()) x >|= definite)
       | `Bot -> empty
     in
     QCheck.frequency ~shrink ~print:show [
@@ -2816,8 +2816,8 @@ module Enums : S with type int_t = BigInt.t = struct
     let neg s = of_excl_list ik (BISet.elements s) in
     let pos s = norm ik (Inc s) in
     let shrink = function
-      | Exc (s, _) -> MyCheck.shrink (BISet.arbitrary ()) s >|= neg (* S TODO: possibly shrink neg to pos *)
-      | Inc s -> MyCheck.shrink (BISet.arbitrary ()) s >|= pos
+      | Exc (s, _) -> GobQCheck.shrink (BISet.arbitrary ()) s >|= neg (* S TODO: possibly shrink neg to pos *)
+      | Inc s -> GobQCheck.shrink (BISet.arbitrary ()) s >|= pos
     in
     QCheck.frequency ~shrink ~print:show [
       20, QCheck.map neg (BISet.arbitrary ());
@@ -3307,7 +3307,7 @@ struct
 
   let arbitrary ik =
     let open QCheck in
-    let int_arb = map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 in
+    let int_arb = map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in
     let cong_arb = pair int_arb int_arb in
     let of_pair ik p = normalize ik (Some p) in
     let to_pair = Option.get in

src/cdomains/offset.ml

@@ -22,7 +22,7 @@ struct
     include CilType.Exp
     let name () = "exp index"
 
-    let any = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "any_index")
+    let any = Cilfacade.any_index_exp
     let all = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index")
 
     (* Override output *)

src/cdomains/valueDomain.ml

@@ -502,7 +502,7 @@ struct
 
   let warn_type op x y =
     if GobConfig.get_bool "dbg.verbose" then
-      ignore @@ printf "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Tracing.current_loc pretty x pretty y
+      ignore @@ printf "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Goblint_tracing.current_loc pretty x pretty y
 
   let rec leq x y =
     match (x,y) with

src/common/cdomains/basetype.ml

@@ -20,8 +20,6 @@ struct
     | _ -> Local
   let name () = "variables"
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
-
-  let arbitrary () = MyCheck.Arbitrary.varinfo
 end
 
 module RawStrings: Printable.S with type t = string =
@@ -35,12 +33,6 @@ struct
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
 end
 
-module Strings: Lattice.S with type t = [`Bot | `Lifted of string | `Top] =
-  Lattice.Flat (RawStrings) (struct
-    let top_name = "?"
-    let bot_name = "-"
-  end)
-
 module RawBools: Printable.S with type t = bool =
 struct
   include Printable.StdLeaf
@@ -52,12 +44,6 @@ struct
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (show x)
 end
 
-module Bools: Lattice.S with type t = [`Bot | `Lifted of bool | `Top] =
-  Lattice.Flat (RawBools) (struct
-    let top_name = "?"
-    let bot_name = "-"
-  end)
-
 module CilExp =
 struct
   include CilType.Exp

src/common/common.mld

@@ -10,6 +10,7 @@ For better context, see {!Goblint_lib} which also documents these modules.
 Node
 Edge
 MyCFG
+CfgTools
 }
 
 {2 Specification}
@@ -18,19 +19,10 @@ AnalysisState
 ControlSpecC
 }
 
-{2 Configuration}
-{!modules:
-GobConfig
-AfterConfig
-JsonSchema
-Options
-}
-
 
 {1 Domains}
 {!modules:
 Printable
-Lattice
 }
 
 {2 Analysis-specific}
@@ -42,7 +34,6 @@ Lattice
 {1 I/O}
 {!modules:
 Messages
-Tracing
 }
 
 
@@ -69,6 +60,3 @@ RichVarinfo
 
 {2 Standard library}
 {!modules:GobFormat}
-
-{2 Other libraries}
-{!modules:MyCheck}

src/common/domains/printable.ml

@@ -233,9 +233,9 @@ struct
   let arbitrary () =
     let open QCheck.Iter in
     let shrink = function
-      | `Lifted x -> (return `Bot) <+> (MyCheck.shrink (Base.arbitrary ()) x >|= lift)
+      | `Lifted x -> (return `Bot) <+> (GobQCheck.shrink (Base.arbitrary ()) x >|= lift)
       | `Bot -> empty
-      | `Top -> MyCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift
+      | `Top -> GobQCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift
     in
     QCheck.frequency ~shrink ~print:show [
       20, QCheck.map lift (Base.arbitrary ());
@@ -626,8 +626,8 @@ struct
   let arbitrary () =
     let open QCheck.Iter in
     let shrink = function
-      | `Lifted x -> MyCheck.shrink (Base.arbitrary ()) x >|= lift
-      | `Top -> MyCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift
+      | `Lifted x -> GobQCheck.shrink (Base.arbitrary ()) x >|= lift
+      | `Top -> GobQCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift
     in
     QCheck.frequency ~shrink ~print:show [
       20, QCheck.map lift (Base.arbitrary ());

src/common/dune

@@ -8,22 +8,18 @@
    batteries.unthreaded
    zarith
    goblint_std
+   goblint_config
+   goblint_tracing
    goblint-cil
    fpath
    yojson
-   json-data-encoding
-   cpu
    goblint_timing
-   goblint_build_info
-   goblint.sites
    qcheck-core.runner)
  (flags :standard -open Goblint_std)
  (preprocess
   (pps
     ppx_deriving.std
     ppx_deriving_hash
-    ppx_deriving_yojson
-    ppx_blob))
- (preprocessor_deps (file util/options.schema.json)))
+    ppx_deriving_yojson)))
 
 (documentation)

src/framework/cfgTools.ml → src/common/framework/cfgTools.ml

@@ -122,10 +122,6 @@ let rec pretty_edges () = function
   | [_,x] -> Edge.pretty_plain () x
   | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs
 
-let get_pseudo_return_id fd =
-  let start_id = 10_000_000_000 in (* TODO get max_sid? *)
-  let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
-  if sid < start_id then sid + start_id else sid
 
 let node_scc_global = NH.create 113
 
@@ -260,7 +256,7 @@ let createCFG (file: file) =
           if Messages.tracing then Messages.trace "cfg" "adding pseudo-return to the function %s.\n" fd.svar.vname;
           let fd_end_loc = {fd_loc with line = fd_loc.endLine; byte = fd_loc.endByte; column = fd_loc.endColumn} in
           let newst = mkStmt (Return (None, fd_end_loc)) in
-          newst.sid <- get_pseudo_return_id fd;
+          newst.sid <- Cilfacade.get_pseudo_return_id fd;
           Cilfacade.StmtH.add Cilfacade.pseudo_return_to_fun newst fd;
           Cilfacade.IntH.replace Cilfacade.pseudo_return_stmt_sids newst.sid newst;
           let newst_node = Statement newst in
@@ -685,7 +681,7 @@ let getGlobalInits (file: file) : edges  =
       lval
     in
     let rec any_index_offset = function
-      | Index (e,o) -> Index (Offset.Index.Exp.any, any_index_offset o)
+      | Index (e,o) -> Index (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

@@ -531,6 +531,12 @@ let stmt_fundecs: fundec StmtH.t ResettableLazy.t =
       h
     )
 
+
+let get_pseudo_return_id fd =
+  let start_id = 10_000_000_000 in (* TODO get max_sid? *)
+  let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
+  if sid < start_id then sid + start_id else sid
+
 let pseudo_return_to_fun = StmtH.create 113
 
 (** Find [fundec] which the [stmt] is in. *)
@@ -706,4 +712,10 @@ let add_function_declarations (file: Cil.file): unit =
   in
   let fun_decls = List.filter_map declaration_from_GFun functions in
   let globals = upto_last_type @ fun_decls @ non_types @ functions in
-  file.globals <- globals
+  file.globals <- globals
+
+
+(** 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 *)

src/common/util/messages.ml

@@ -339,4 +339,23 @@ let msg_final severity ?(tags=[]) ?(category=Category.Unknown) fmt =
   else
     GobPretty.igprintf () fmt
 
-include Tracing
+
+include Goblint_tracing
+
+open Pretty
+
+let tracel sys ?var fmt =
+  let loc = !current_loc in
+  let docloc sys doc =
+    printtrace sys (dprintf "(%a)@?" CilType.Location.pretty loc ++ indent 2 doc);
+  in
+  gtrace true docloc sys var ~loc ignore fmt
+
+let traceli sys ?var ?(subsys=[]) fmt =
+  let loc = !current_loc in
+  let g () = activate sys subsys in
+  let docloc sys doc: unit =
+    printtrace sys (dprintf "(%a)" CilType.Location.pretty loc ++ indent 2 doc);
+    traceIndent ()
+  in
+  gtrace true docloc sys var ~loc g fmt

src/config/config.mld

@@ -0,0 +1,14 @@
+{0 Library goblint.config}
+This library is unwrapped and provides the following top-level modules.
+For better context, see {!Goblint_lib} which also documents these modules.
+
+
+{1 Framework}
+
+{2 Configuration}
+{!modules:
+GobConfig
+AfterConfig
+JsonSchema
+Options
+}