diff --git a/dune-project b/dune-project index 6932d5aaa..424a6c1b6 100644 --- a/dune-project +++ b/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 ) diff --git a/goblint-cil.opam b/goblint-cil.opam index d66c62b82..0a31ec7e0 100644 --- a/goblint-cil.opam +++ b/goblint-cil.opam @@ -42,7 +42,6 @@ depends: [ "conf-perl" "cppo" "conf-gcc" - "domain_shims" ] conflicts: ["cil"] build: [ diff --git a/src/domain.ocaml4.ml b/src/domain.ocaml4.ml new file mode 100644 index 000000000..a382a27be --- /dev/null +++ b/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 diff --git a/src/domain.ocaml4.mli b/src/domain.ocaml4.mli new file mode 100644 index 000000000..63ea923a5 --- /dev/null +++ b/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 diff --git a/src/dune b/src/dune index a804b0a1b..b6a70cb6c 100644 --- a/src/dune +++ b/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) diff --git a/test/Makefile b/test/Makefile index 3463c0f77..d486cfacd 100644 --- a/test/Makefile +++ b/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