Replace dependency on domain_shims with lightweight DLS shim for single-threaded OCaml

dune-project

@@ -35,7 +35,6 @@ This is a fork of the 'cil' package used for 'goblint'. Major changes include:
     conf-perl
     cppo
     conf-gcc
-    domain_shims
   )
   (conflicts cil) ; only because we both install the cilly executable
 )

goblint-cil.opam

@@ -42,7 +42,6 @@ depends: [
   "conf-perl"
   "cppo"
   "conf-gcc"
-  "domain_shims"
 ]
 conflicts: ["cil"]
 build: [

src/domain.ocaml4.ml

@@ -0,0 +1,20 @@
+module DLS = struct
+  type 'a key = {
+    mutable value: 'a option;
+    initialiser: unit -> 'a;
+  }
+
+  let new_key ?split_from_parent initialiser =
+    { value = None; initialiser }
+
+  let get (k: 'a key) =
+    match k.value with
+    | Some v -> v
+    | None ->
+        let v = k.initialiser () in
+        k.value <- Some v;
+        v
+
+  let set k v =
+    k.value <- Some v
+end

src/domain.ocaml4.mli

@@ -0,0 +1,30 @@
+module DLS : sig
+(** Domain-local Storage *)
+
+    type 'a key
+    (** Type of a DLS key *)
+
+    val new_key : ?split_from_parent:('a -> 'a) -> (unit -> 'a) -> 'a key
+    (** [new_key f] returns a new key bound to initialiser [f] for accessing
+        domain-local variables.
+
+        If [split_from_parent] is provided, spawning a domain will derive the
+        child value (for this key) from the parent value.
+
+        Note that the [split_from_parent] call is computed in the parent
+        domain, and is always computed regardless of whether the child domain
+        will use it. If the splitting function is expensive or requires
+        client-side computation, consider using ['a Lazy.t key].
+    *)
+
+    val get : 'a key -> 'a
+    (** [get k] returns [v] if a value [v] is associated to the key [k] on
+        the calling domain's domain-local state. Sets [k]'s value with its
+        initialiser and returns it otherwise. *)
+
+    val set : 'a key -> 'a -> unit
+    (** [set k v] updates the calling domain's domain-local state to associate
+        the key [k] with value [v]. It overwrites any previous values associated
+        to [k], which cannot be restored later. *)
+
+end

src/dune

@@ -3,7 +3,7 @@
 (library
   (public_name goblint-cil)
   (name goblintCil)
-  (libraries zarith unix str stdlib-shims domain_shims)
+  (libraries zarith unix str stdlib-shims)
   (modules (:standard \ main mainFeature ciloptions machdepConfigure machdepArchConfigure modelConfigure))
 )
 
@@ -16,6 +16,16 @@
  (target machdep-config.h)
  (action (run ./machdepConfigure.exe)))
 
+(rule
+ (targets domain.ml domain.mli)
+ (deps domain.ocaml4.ml domain.ocaml4.mli)
+ (enabled_if (< %{ocaml_version} 5.0))
+ (action
+  (progn
+   (copy domain.ocaml4.ml domain.ml)
+   (copy domain.ocaml4.mli domain.mli)
+   )))
+
 (rule
  (deps machdep-config.h machdep-ml.c)
  (target machdep-ml.exe)

test/Makefile

@@ -276,7 +276,7 @@ else
 endif
 
 testrun/% : $(SMALL1)/%.ml
-	ocamlfind $(CAMLC) -I $(OBJDIR_DUNE) -I $(OBJDIR_MAKE) -package zarith -package domain_shims unix.$(CMXA) str.$(CMXA) zarith.$(CMXA) threads.$(CMXA) domain_shims.$(CMXA) -thread \
+	ocamlfind $(CAMLC) -I $(OBJDIR_DUNE) -I $(OBJDIR_MAKE) -package zarith unix.$(CMXA) str.$(CMXA) zarith.$(CMXA) threads.$(CMXA) -thread \
                  goblintCil.$(CMXA) \
                  $(EXEOUT) $(basename $<).exe $<
 	$(basename $<).exe