BAP 2.0.0 release (candidate) (#1017)

* BAP 2.0.0 release (candidate)

Polishes documentation as well as fixes the theory declaration
function. And finally bumps the version to 2.0.0.

Whle revising the documentation I've noticed that the interface of
theory declaration is not allowing references to other theories as it
isn't wrapped in the knowledge monad as it should be. I fixed it, but
immediately fell into the trap of a recursive instantiation. Indeed, a
theory may require itself as a base, which will lead to an infinite
recursion and runtime failure. Since it is so easy to fall into this
trap, the implementation has to be robust enough and either forbid
this, with an appropriate error message, or allow it, with an
appropriate semantics. We chose the latter, since our theories are
domains we have a sane semantics for recursive theories (well, this
is what denotational semantics was invented on the first hand). We
employed the same technique for recursive module instantiation as
OCaml does, i.e., first initialize the theory with an empty structure,
then overwrite it with the result.

* updates testsuites commit

Author: ivg

lib/bap_byteweight/bap_byteweight.mli

@@ -1,6 +1,6 @@
 (** Byteweight library.
 
-    Byteweight is a function start identification mechanism [[1]]. This
+    Byteweight is a function start identification algorithm [[1]]. This
     library provides a functorized implementation.
 
     An auxiliary {!Bap_byteweight_signatures} library provides an
@@ -13,7 +13,6 @@
          23rd USENIX Security Symposium (USENIX Security 14). 2014.
     v}
 *)
-
 open Bap.Std
 
 

lib/bap_core_theory/bap_core_theory.ml

@@ -53,6 +53,7 @@ module Theory = struct
   module type Trans = Bap_core_theory_definition.Trans
   module type Core = Bap_core_theory_definition.Core
 
+  type core = (module Core)
   module Basic = struct
     module Empty : Basic = Bap_core_theory_empty.Core
     module Make = Bap_core_theory_basic.Make

lib/bap_core_theory/bap_core_theory.mli

@@ -264,21 +264,21 @@
     ["constant-tracker"] analysis:
 
     {[
-      let () = Theory.declare "my-constant-tracker" (module struct
-          include (val Theory.require "constant-tracker")
-
-          (* probably a bad example, but we all do this :) *)
-          let add x y =
-            printf "add is called!\n%!";
-            add x y
+      let () =
+          Theory.declare "my-constant-tracker"
+          Theory.instance ~require:["bap.std:constant-tracker"] >>=
+          Theory.require >>|
+          fun (module Base) : Theory.core -> (module struct
+            include Base
+            let add x y =
+              printf "add is called!\n%!";
+              add x y
         end
     ]}
 
-
     The real analysis should store it results either in the knowledge
     base or directly in denotations of the terms (or in both places).
 
-
     {2 Instantiating a theory}
 
     To use a theory we need to instantiate it. In the previous section
@@ -310,15 +310,18 @@
     specified context. For example,
 
     {[
-      module Theory = (val Theory.instance ()
-                          ~context:["arm"; "arm-gnueabi"]
-                          ~requires:[
-                            "variable-recovery";
-                            "stack-frame-analysis";
-                            "structural-analysis";
-                            "floating-point";
-                            "bap.std:bil-semantics";
-                          ])
+
+      Theory.instance ()
+        ~context:["arm"; "arm-gnueabi"]
+        ~requires:[
+          "variable-recovery";
+          "stack-frame-analysis";
+          "structural-analysis";
+          "floating-point";
+          "bap.std:bil-semantics"
+      ] >>=
+      Theory.require >>= fun (module Theory) ->
+
     ]}
 
     In the example above, theories that are specific to ARM
@@ -329,9 +332,11 @@
     explicitly, the [bap.std:bil-semantics], to ensure that each term
     has a BIL denotation.
 
-    [1]: http://okmij.org/ftp/tagless-final/JFP.pdf
-    [2]: http://www.cs.utexas.edu/~wcook/Drafts/2012/ecoop2012.pdf
-    [3]: http://okmij.org/ftp/tagless-final/course/optimizations.html
+    References:
+
+    - [1]: http://okmij.org/ftp/tagless-final/JFP.pdf
+    - [2]: http://www.cs.utexas.edu/~wcook/Drafts/2012/ecoop2012.pdf
+    - [3]: http://okmij.org/ftp/tagless-final/course/optimizations.html
 
 
     {2 Parsing binary code}
@@ -1997,6 +2002,10 @@ module Theory : sig
   end
 
 
+  (** a type abbreviation for the core theory module type.  *)
+  type core = (module Core)
+
+
   (** The Basic Theory.
 
       Implements the empty basic theory and provides a module for
@@ -2049,7 +2058,9 @@ module Theory : sig
     ?context:string list ->
     ?provides:string list ->
     ?package:string ->
-    name:string -> (module Core) -> unit
+    name:string ->
+    (module Core) knowledge ->
+    unit
 
   (** [instance ()] creates an instance of the Core Theory.
 

lib/bap_core_theory/bap_core_theory_manager.ml

@@ -21,7 +21,7 @@ type 'a theory = {
 }
 
 type core = (module Core)
-let known_theories : (Name.t, core theory) Hashtbl.t =
+let known_theories : (Name.t, core knowledge theory) Hashtbl.t =
   Hashtbl.create (module Name)
 
 let features = Set.of_list (module String)
@@ -312,7 +312,6 @@ let slot = Knowledge.Class.property theory "instance" domain
     ~desc:"The theory structure"
 
 
-
 let str_ctxt () ctxt =
   List.to_string (Set.to_list ctxt) ~f:ident
 
@@ -321,11 +320,10 @@ module Theory = (val Knowledge.Object.derive theory)
 let theories () =
   let init = Map.empty (module Theory) in
   Hashtbl.to_alist known_theories |>
-  Knowledge.List.fold ~init ~f:(fun theories (name,structure) ->
+  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 structure)
-
+      Map.add_exn theories name def)
 
 let is_applicable ~provided ~requires =
   Set.for_all requires ~f:(Set.mem provided)
@@ -350,44 +348,75 @@ let refine ?(context=[]) ?requires theories =
       is_applicable ~provided ~requires &&
       is_required ~required ~provides)
 
-let new_theory ?context ?requires () =
-  theories () >>| Map.data >>| refine ?context ?requires >>= function
-  | [] -> Knowledge.return Empty.theory
-  | [t] -> Knowledge.return t
-  | theories ->
-    Knowledge.return @@
-    (List.reduce_balanced_exn theories ~f:merge)
-
 let theory_for_id id =
   let sym = sprintf "'%s" @@
     List.to_string (Set.to_list id) ~f:Name.show in
   Knowledge.Symbol.intern sym theory
     ~package:"core-theory-internal"
 
+let is_instantiated id =
+  Knowledge.collect slot id >>| fun t ->
+  not t.is_empty
+
+
+(* On instantiation of recursive modules.
+
+   We employ the same techinique as OCaml does [1].
+   When a module is instantiated we create an instance
+   of this module with an empty structure, so that if
+   a module creates an instance of itself during instantiation,
+   it will not enter an infinite recursion but will get the
+   empty denotation. Our merge operator, which will be called,
+   by the provide operator after the final instance is created,
+   will notice that the initial structure is ordered strictly
+   before the new one (because we used the Empty.name for it),
+   thus it will drop it from the final structure.
+
+   [1]: Leroy, Xavier."A proposal for recursive modules in Objective
+   Caml." Available from the author’s website (2003).
+*)
+let instantiate t =
+  theory_for_id t.id >>= fun id ->
+  is_instantiated id >>= function
+  | true -> Knowledge.return id
+  | false ->
+    Knowledge.provide slot id {
+      Empty.theory with is_empty = false
+    } >>= fun () ->
+    t.structure >>= fun structure ->
+    Knowledge.provide slot id {t with structure} >>| fun () ->
+    id
+
 let instance ?context ?requires () =
   theories () >>| Map.data >>| refine ?context ?requires >>= function
   | [] -> theory_for_id Empty.theory.id
-  | [t] -> theory_for_id t.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 ->
-    let theory = List.reduce_balanced_exn theories ~f:merge in
-    Knowledge.provide slot id theory >>| 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 require name =
   let open Knowledge.Syntax in
   theories () >>= fun theories ->
   match Map.find theories name with
-  | Some t -> Knowledge.return t.structure
+  | Some t -> t.structure
   | None -> Knowledge.collect slot name >>| fun t ->
     t.structure
 
 
 module Documentation = struct
   module Theory = struct
-    type t = Name.t * core theory
+    type t = Name.t * core knowledge theory
 
     let (-) xs name = Set.remove xs (Name.show name)
 

lib/bap_core_theory/bap_core_theory_manager.mli

@@ -7,7 +7,9 @@ val declare :
   ?context:string list ->
   ?provides:string list ->
   ?package:string ->
-  name:string -> (module Core) -> unit
+  name:string ->
+  (module Core) knowledge ->
+  unit
 
 val instance :
   ?context:string list ->