adds a Primus Lisp fronted

.merlin

@@ -60,6 +60,7 @@ B lib/bap_image
 B lib/bap_plugins
 B lib/bap_primus
 B lib/bap_sema
+B lib/bap_strings
 B lib/bap_types
 B lib/bap_core_theory
 B lib/graphlib

lib/bap_core_theory/bap_core_theory.mli

@@ -414,6 +414,7 @@ module Theory : sig
     (** the value type is an instance of Knowledge.value   *)
     type 'a t = (cls,'a sort) KB.cls KB.value
 
+    type 'a value = 'a t
 
     (** the class of all values.  *)
     val cls : (cls,unit) KB.cls
@@ -434,6 +435,106 @@ module Theory : sig
     val sort : 'a t -> 'a sort
 
 
+    (** [resort refine x] applies [refine] to the sort of [x].
+
+        Returns the value [x] with the refined sort, if applicable,
+        otherwise returns the original value.
+
+        @since 2.3.0
+    *)
+    val resort : ('a sort -> 'b sort option) -> 'a t -> 'b t option
+
+
+    (** [forget v] erases the type index of the value.
+
+        The returned value has the monomorphized [Top.t] type and can
+        be stored in containers, serialized, etc.
+
+        To restore the type index use the {!refine} function.
+
+        @since 2.3.0
+
+        Note: this is a convenient function that just does
+        [Knowledge.Value.refine v @@ Sort.forget @@ sort v]
+    *)
+    val forget : 'a t -> unit t
+
+    (** A value with an erased sort type index.
+
+        The monomorphized value could be stored in a container,
+        serialized and deserialized and otherwise treated as a
+        regular value. To erase the type index, use the
+        [Value.forget] function.
+
+        The type index could be restored using [Value.refine] or
+        [Value.Sort.refine] functions.
+
+        @since 2.3.0
+    *)
+    module Top : sig
+      type t = (cls,unit sort) KB.cls KB.value
+      val cls : (cls, unit sort) KB.cls
+      include KB.Value.S with type t := t
+    end
+
+
+    (** A eDSL for dispatching on multiple types.
+
+        The syntax involves only two operators, [can] that
+        applys a sort refinining function, and [let|]
+        glues several cases together. Let's start with a simple
+        example,
+        {[
+          let f x = Match.(begin
+              let| x = can Bool.refine x @@ fun x ->
+                (* here x has type [Bool.t value] *)
+                `Bool x in
+              let| x = can Bitv.refine x @@ fun x ->
+                (* and here x is ['a Bitv.t value] *)
+                `Bitv x in
+              let| x = can Mem.refine x @@ fun x ->
+                (* and now x is [('a,'b) Mem.t value] *)
+                `Mem x in
+              `Other x
+            end)
+        ]}
+
+        In general, the syntax is
+        {v
+          let| x = can s1 x @@ fun (x : t1) ->
+            body1 in
+          ...
+          let| x = can sN x @@ fun (x : tN) ->
+            bodyN in
+          default
+        v}
+
+        where [s1],...,[sN] a refiners to types [t1],...,[tN],
+        respectively.
+
+        {3 Semantics}
+
+        If in [can s1 x body] the sort of [x] can be refined to [t1] using
+        the refiner [s1] then [body] is applied to the value [x] with
+        the refined sort (and freshly generated type index if
+        needed) and the result of the whole expression is [body x]
+        and the nested below expressions are never
+        evaluated. Otherwise, if there is no refinement, the
+        expression [can s1 x body] is evaluated to [x]
+        and the next case is tried until the [default] case is hit.
+    *)
+    module Match : sig
+      type 'a t
+      type 'a refiner = unit sort -> 'a sort option
+      val (let|) : 'b t -> (unit -> 'b) -> 'b
+      val can : 'a refiner -> unit value -> ('a value -> 'b) -> 'b t
+      val both :
+        'a refiner -> unit value ->
+        'b refiner -> unit value ->
+        ('a value -> 'b value -> 'c) -> 'c t
+    end
+
+
     (** Value Sorts.
 
         A concrete and extensible representation of a value sort. The
@@ -828,7 +929,6 @@ module Theory : sig
   type 'a value = 'a Value.t
   type 'a effect = 'a Effect.t
 
-
   (** The sort for boolean values.
 
       Booleans are one bit values.
@@ -1120,9 +1220,13 @@ module Theory : sig
 
     (** the slot to store program semantics.  *)
     val slot : (program, t) Knowledge.slot
+
+    val value : (cls, unit Value.t) Knowledge.slot
+
     include Knowledge.Value.S with type t := t
   end
 
+
   (** The denotation of programs.
 
       Values of class [program] are used to express the semantics of

lib/bap_core_theory/bap_core_theory_program.ml

@@ -3,6 +3,7 @@ open Bitvec_order.Comparators
 open Bap_knowledge
 
 let package = "core-theory"
+module Value  = Bap_core_theory_value
 module Effect = Bap_core_theory_effect
 module Target = Bap_core_theory_target
 
@@ -288,6 +289,11 @@ module Semantics = struct
       ~persistent:(Knowledge.Persistent.of_binable (module Self))
       ~public:true
       ~desc:"the program semantics"
+  let value = Knowledge.Class.property ~package cls "value" Value.Top.domain
+      ~persistent:(Knowledge.Persistent.of_binable (module Value.Top))
+      ~public:true
+      ~desc:"the program semantics"
+
   include Self
 end
 

lib/bap_core_theory/bap_core_theory_program.mli

@@ -1,6 +1,7 @@
 open Core_kernel
 open Bap_knowledge
 
+module Value  = Bap_core_theory_value
 module Effect = Bap_core_theory_effect
 module Target = Bap_core_theory_target
 
@@ -11,11 +12,13 @@ type compiler
 
 type t = (program,unit) Knowledge.cls Knowledge.value
 val cls : (program,unit) Knowledge.cls
+
 module Semantics : sig
   type cls = Effect.cls
   type t = unit Effect.t
   val cls : (cls, unit Effect.sort) Knowledge.cls
   val slot : (program, t) Knowledge.slot
+  val value : (cls, unit Value.t) Knowledge.slot
   include Knowledge.Value.S with type t := t
 end
 

lib/bap_core_theory/bap_core_theory_value.ml

@@ -37,6 +37,7 @@ module Sort : sig
 
   module Top : sig
     type t = top [@@deriving bin_io, compare, sexp]
+    val t : top
     include Base.Comparable.S with type t := t
   end
 
@@ -148,6 +149,9 @@ end
 
   module Top = struct
     type t = top
+    let any = Name.declare ~package "Top"
+    let t = forget (sym any)
+
     include Sexpable.Of_sexpable(Exp)(struct
         type t = top
         let to_sexpable x = x
@@ -176,7 +180,21 @@ type 'a t = (cls,'a sort) KB.cls KB.value
 let cls = Sort.cls
 let empty s : 'a t = KB.Value.empty (KB.Class.refine cls s)
 let sort v : 'a sort = KB.Class.sort (KB.Value.cls v)
+let resort : ('a sort -> 'b sort option) -> 'a t -> 'b t option =
+  fun refine v ->
+  Option.(refine (sort v) >>| KB.Value.refine v)
+
+let forget : 'a t -> unit t = fun v ->
+  KB.Value.refine v @@ Sort.forget @@ sort v
 
+module type Sort = sig
+  val refine : unit sort -> 'a sort option
+end
+
+module Top = struct
+  let cls = KB.Class.refine cls Sort.Top.t
+  include (val KB.Value.derive cls)
+end
 
 module Bool : sig
   type t
@@ -265,3 +283,29 @@ end
   let t = Sort.(sym rmode)
   let refine x = Sort.refine rmode x
 end
+
+type 'a value = 'a t
+
+module Match : sig
+  type 'a t
+  type 'a refiner = unit sort -> 'a sort option
+  val (let|) : 'b t -> (unit -> 'b) -> 'b
+  val can : 'a refiner -> unit value -> ('a value -> 'b) -> 'b t
+  val both :
+    'a refiner -> unit value ->
+    'b refiner -> unit value ->
+    ('a value -> 'b value -> 'c) -> 'c t
+end = struct
+  type 'a refiner = unit sort -> 'a sort option
+  type 'a value = 'a t
+  type 'b t = (unit -> 'b) -> 'b
+  let (let|) = (@@)
+  let can cast x action k =
+    match resort cast x with
+    | None -> k ()
+    | Some x -> action x
+  let both castx x casty y action k =
+    match resort castx x, resort casty y with
+    | Some x, Some y -> action x y
+    | _ -> k ()
+end

lib/bap_core_theory/bap_core_theory_value.mli

@@ -3,15 +3,34 @@ open Caml.Format
 open Bap_knowledge
 
 module KB = Knowledge
-
 type +'a sort
 type cls
 
 type 'a t = (cls,'a sort) KB.cls KB.value
+type 'a value = 'a t
 val cls : (cls,unit) KB.cls
 
 val empty : 'a sort -> 'a t
 val sort : 'a t -> 'a sort
+val resort : ('a sort -> 'b sort option) -> 'a t -> 'b t option
+val forget : 'a t -> unit t
+
+module Top : sig
+  type t = (cls,unit sort) KB.cls KB.value
+  val cls : (cls,unit sort) KB.cls
+  include KB.Value.S with type t := t
+end
+
+module Match : sig
+  type 'a t
+  type 'a refiner = unit sort -> 'a sort option
+  val (let|) : 'b t -> (unit -> 'b) -> 'b
+  val can : 'a refiner -> unit value -> ('a value -> 'b) -> 'b t
+  val both :
+    'a refiner -> unit value ->
+    'b refiner -> unit value ->
+    ('a value -> 'b value -> 'c) -> 'c t
+end
 
 module Sort : sig
   type +'a t = 'a sort
@@ -40,6 +59,7 @@ module Sort : sig
 
   module Top : sig
     type t = unit sort [@@deriving bin_io, compare, sexp]
+    val t : t
     include Base.Comparable.S with type t := t
   end