uses context variables to store the current theory (#1342)

* Introduces context variables to the knowledge library

* makes theory a part of the context

Introduces the [Theory.current] and [Theory.with_current] functions.

Author: ivg

lib/bap/bap_project.ml

@@ -408,7 +408,10 @@ let create
     Signal.send Info.got_code code;
     Signal.send Info.got_spec spec;
     let run k =
-      let k = KB.(set_package package >>= fun () -> k) in
+      let k = KB.(set_package package >>= fun () ->
+                  Theory.instance () >>= fun theory ->
+                  Theory.with_current theory @@ fun () ->
+                  k) in
       State.Toplevel.run spec target ~code ~memory file k in
     let state = match state with
       | Some state -> state

lib/bap_core_theory/bap_core_theory.mli

@@ -266,8 +266,8 @@
 
     {[
       let () =
-        Theory.declare "my-constant-tracker"
-          Theory.instance ~require:["bap.std:constant-tracker"] >>=
+        Theory.declare "my-constant-tracker" @@
+        Theory.instance ~require:["bap.std:constant-tracker"] >>=
         Theory.require >>|
         fun (module Base) : Theory.core -> (module struct
           include Base
@@ -3030,29 +3030,39 @@ module Theory : sig
     (module Core) knowledge ->
     unit
 
-  (** [instance ()] creates an instance of the Core Theory.
+  (** [instance ()] returns the current or creates a new instance of
+      the core theory.
 
-      The instance is built from all theories that match the context
-      specified by the [features] list and provide features specified
-      by the [requires] list. If any theory is subsumed by other
-      theory, then it is excluded.
+      If no parameters of the [instance] function were specialized
+      and there is an instance of the current theory then this
+      instance is returned.
 
-      If no instances satisfy this requirement than the empty theory
+      Otherwise, the instance is built from all theories that match
+      the context specified by the [context] list and provide features
+      specified by the [requires] list. If any theory is subsumed by
+      other theory, then it is excluded.
+
+      If no instances satisfy this requirement then the empty theory
       is returned. If only one theory satisfies the requirement, then
       it is returned. If many theories match, then a join of all
       theories is computed, stored in the knowledge base, and the
       resulting theory is returned.
 
-      To manifest a theory into an structure, use the [require] function.
+      To manifest a theory into an structure, use the [require]
+      function. The [current] function is equivalent to the
+      composition [instance >=> require], use this function, if you
+      want to use the current theory.
 
-      @param features is a set of features that define the context,
+      @param context is a set of features that define the context,
       only those theories that have a context that is a subset of
       provided will be instantiated.
 
       @param requires is a set of semantic features that are
       required. Defaults to the set of all possible features, i.e., if
       unspecified, then all instances applicable to the context will
       be loaded.
+
+      @since 2.4.0 respects the currently set theory.
   *)
   val instance :
     ?context:string list ->
@@ -3062,15 +3072,19 @@ module Theory : sig
   (** [require theory] manifests the [theory] as an OCaml structure.
 
       It is only possible to create an instance of theory using the
-      {!instance} function. For example, the following will create an
-      theory that is a join all currently declared theories (which are
-      not specific to any context),
+      {!instance} function, but see also {!current}.
+
+      For example, the following will create an theory that is a join
+      all currently declared theories (which are not specific to any
+      context),
 
       {[
-        Theory.(instance>=>require) () -> fun (module Core) ->
+        let* (module CT) = Theory.(instance>=>require) () in
       ]}
 
-      To a create an instance for a specific context and requirements,
+      where [let*] comes from [KB.Let].
+
+      To create an instance for a specific context and requirements,
 
       {[
         Theory.instance ()
@@ -3089,6 +3103,41 @@ module Theory : sig
   *)
   val require : theory -> (module Core) knowledge
 
+
+
+  (** [current] returns the current core theory structure.
+
+      This function is the same as [instance >=> require].
+
+      If there is no current theory set in the contex (via the
+      {!with_current} function) then a new structure is created,
+      otherwise returns the current selected theory.
+
+      An example of usage,
+
+      {[
+        let add x y =
+          let* (module CT) = current in
+          CT.add x y
+      ]}
+
+      @since 2.4.0
+  *)
+  val current : (module Core) knowledge
+
+  (** [with_current t f] sets [t] as the current theory in the scope of [f].
+
+      Evaluates compuation [f] in the theory of [t]. After [f] is
+      evaluated the current theory is restored. This function could be
+      safely called recursively, i.e., in a scope of another call to
+      [with_current]. Effectively, [with_current], which uses
+      [KB.Context.with_var] underneath the hood, creates a dynamic
+      scope for the theory variable.
+
+      @since 2.4.0
+  *)
+  val with_current : theory -> (unit -> 'a knowledge) -> 'a knowledge
+
   (** Sorts implementing IEEE754 formats.
 
       This module provides an infinite set of indexed sorts for

lib/bap_core_theory/bap_core_theory_manager.ml

@@ -311,19 +311,33 @@ let slot = Knowledge.Class.property theory "instance" domain
     ~package:"core"
     ~desc:"The theory structure"
 
-
-let str_ctxt () ctxt =
-  List.to_string (Set.to_list ctxt) ~f:ident
+let current = Knowledge.Context.declare
+    ~package:"core" "*current-theory*"
+    !!(Knowledge.Object.null theory)
 
 module Theory = (val Knowledge.Object.derive theory)
 
+let theories = KB.Context.declare
+    ~package:"core" "*theories*"
+    !!None
+
 let theories () =
-  let init = Map.empty (module Theory) in
-  Hashtbl.to_alist known_theories |>
-  Knowledge.List.fold ~init ~f:(fun theories (name,def) ->
-      Knowledge.Symbol.intern (Name.unqualified name) theory
-        ~package:(Name.package name) >>| fun name ->
-      Map.add_exn theories name def)
+  KB.Context.get theories >>= function
+  | Some theories -> !!theories
+  | None ->
+    let init = Map.empty (module Theory) in
+    Hashtbl.to_alist known_theories |>
+    Knowledge.List.fold ~init ~f:(fun theories (name,def) ->
+        Knowledge.Symbol.intern (Name.unqualified name) theory
+          ~package:(Name.package name) >>| fun name ->
+        Map.add_exn theories name def) >>= fun r ->
+    KB.Context.set theories (Some r) >>| fun () ->
+    r
+
+
+let str_ctxt () ctxt =
+  List.to_string (Set.to_list ctxt) ~f:ident
+
 
 let is_applicable ~provided ~requires =
   Set.for_all requires ~f:(Set.mem provided)
@@ -388,22 +402,30 @@ let instantiate t =
     id
 
 let instance ?context ?requires () =
-  theories () >>| Map.data >>| refine ?context ?requires >>= function
-  | [] -> theory_for_id Empty.theory.id
-  | [t] ->
-    instantiate t
-  | theories ->
-    List.fold theories ~init:(Set.empty (module Name)) ~f:(fun names t ->
-        Set.union names t.id) |>
-    theory_for_id >>= fun id ->
-    is_instantiated id >>= function
-    | true -> Knowledge.return id
-    | false ->
-      Knowledge.List.map theories
-        ~f:(instantiate >=> Knowledge.collect slot) >>|
-      List.reduce_balanced_exn ~f:merge >>=
-      Knowledge.provide slot id >>| fun () ->
-      id
+  KB.Context.get current >>= fun theory ->
+  match context, requires with
+  | None,None when not (Knowledge.Object.is_null theory) -> !!theory
+  | _ ->
+    theories () >>| Map.data >>| refine ?context ?requires >>= function
+    | [] -> theory_for_id Empty.theory.id
+    | [t] ->
+      instantiate t
+    | theories ->
+      List.fold theories ~init:(Set.empty (module Name)) ~f:(fun names t ->
+          Set.union names t.id) |>
+      theory_for_id >>= fun id ->
+      is_instantiated id >>= function
+      | true -> Knowledge.return id
+      | false ->
+        Knowledge.List.map theories
+          ~f:(instantiate >=> Knowledge.collect slot) >>|
+        List.reduce_balanced_exn ~f:merge >>=
+        Knowledge.provide slot id >>| fun () ->
+        id
+
+let with_current t f =
+  Knowledge.Context.with_var current t f
+
 
 let require name =
   let open Knowledge.Syntax in
@@ -413,6 +435,8 @@ let require name =
   | None -> Knowledge.collect slot name >>| fun t ->
     t.structure
 
+let current = (instance >=> require) ()
+
 
 module Documentation = struct
   module Theory = struct

lib/bap_core_theory/bap_core_theory_manager.mli

@@ -18,6 +18,10 @@ val instance :
 
 val require : theory -> (module Core) knowledge
 
+val with_current : theory -> (unit -> 'a knowledge) -> 'a knowledge
+
+val current : (module Core) knowledge
+
 module Documentation : sig
   module Theory : sig
     type t