adds forward-chaining rules and Primus Lisp methods (#1363)

* adds forward-chaining rules to the knowledge base

* adds some useful primitives for writing primitives to Primus

* evaluate keywords to themselves in Primus Lisp

The keyword symbols, like `:foo` were treated as variables, but we
want them to be symbols. The change is made on the reader (parser)
level so it will affect both Primus Lisp implementations - static
and dynamic.

* allows any primitive to return non-reified symbol

When a primitive returns a value that has the symbol slot set to
something, the interpreter will automatically intern it. It simplifies
writing the primitives as the implementor doesn't need to bother about
interning and setting the static part of the value.

* implements methods in the Primus Lisp semantics interpreter

* updates the testsuite, uses the newer opam syntax

Makefile

@@ -55,7 +55,7 @@ testsuite:
 	git clone https://github.com/BinaryAnalysisPlatform/bap-testsuite.git testsuite
 
 check: testsuite
-	make REVISION=81d9159 -C testsuite
+	make REVISION=c2324bf -C testsuite
 
 .PHONY: indent check-style status-clean
 

lib/bap_primus/bap_primus.mli

@@ -3867,6 +3867,10 @@ text ::= ?any atom that is not recognized as a <word>?
       *)
       module Semantics : sig
 
+        (** the representation of semantic values.
+
+            @since 2.4.0  *)
+        type value = unit Theory.Value.t
 
         (** occurs when no matching definition is found
 
@@ -3879,6 +3883,13 @@ text ::= ?any atom that is not recognized as a <word>?
         (** occurs when the Lisp program is ill-typed  *)
         type KB.conflict += Illtyped_program of Type.error list
 
+        (** occurs when a primitive fails.
+
+            See also, {!failp}
+
+            @since 2.4.0  *)
+        type KB.conflict += Failed_primitive of KB.Name.t * string
+
 
         (** a property of the program source object in which
             a Lisp program is stored.
@@ -3988,14 +3999,96 @@ text ::= ?any atom that is not recognized as a <word>?
           ?types:Type.signature ->
           ?docs:string ->
           ?package:string ->
-          ?body:(Theory.Target.t -> (Theory.Label.t -> Theory.Value.Top.t list -> unit Theory.eff) KB.t) ->
+          ?body:(Theory.Target.t -> (Theory.Label.t -> value list -> unit Theory.eff) KB.t) ->
           string -> unit
 
+
+        (** [signal ~params ~docs property args] declares a signal.
+
+            Emits a signal with arguments [args l v], when the
+            [property] value of a program label [l] changes to
+            [v]. The name of the signal is the same as the name of the
+            property.
+
+            The signal triggers all methods with the same method name
+            as the signal.
+
+            @since 2.4.0
+        *)
+        val signal :
+          ?params:[< Type.parameters] ->
+          ?docs:string ->
+          (Theory.program, 'p) KB.slot ->
+          (Theory.Label.t -> 'p -> value list KB.t) ->
+          unit
+
+        (** [failp err_msg args...] terminates a primitive with error.
+
+            Must be called from a primitive implementation to stop
+            the evaluation with the [Failed_primitive] conflict.
+
+            This conflict should used to report programmer errors
+            that are not representable via the type system (or slipped
+            through the gradual type checker).
+
+            @since 2.4.0
+        *)
+        val failp : ('a, Format.formatter, unit, 'b KB.t) format4 -> 'a
+
         (** [documentation unit] documentation for [unit]'s lisp source.
 
             Typechecks and loads the unit lisp source and generates
             its documentation. *)
         val documentation : Theory.Unit.t -> Doc.index KB.t
+
+        (** Pure semantic value.
+
+            @since 2.4.0  *)
+        module Value : sig
+          type t = value
+
+          (** [static x] a value statically equal to [x].*)
+          val static : Bitvec.t -> t
+
+          (** [symbol s] a symbolic value.
+
+              A symbolic value is also static and the Primus Lisp
+              lifter will intern symbols by asigning a static value
+              for each symbol so that distinct symbols will have
+              distinct static values. *)
+          val symbol : string -> t
+
+
+          (** [custom prop x] creates a custom static value.
+
+              The property [prop] is set to [x] and the [symbol] slot
+              is set to [t], i.e., to [true] so that the value
+              evaluates to non-nil in the condition expressions.   *)
+          val custom : (Theory.Value.cls, 'a) KB.slot -> 'a -> t
+
+
+          (** the false value that evaluates to [nil] symbol having
+              [0] representation. *)
+          val nil : t
+        end
+
+
+        (** Effectful semantic values.
+
+            @since 2.4.0
+        *)
+        module Effect : sig
+          type t = unit Theory.Effect.t
+
+          (** [pure x] an empty effect with value [x]
+
+              sets the [Theory.Semantics.value] slot to [x].
+          *)
+          val pure : Value.t -> t
+
+          (** [return x] same as [KB.return@@pure x] *)
+          val return : Value.t -> t KB.t
+        end
       end
 
 

lib/bap_primus/bap_primus_lisp.mli

@@ -141,8 +141,10 @@ module Make (Machine : Machine) : sig
 end
 
 module Semantics : sig
+  type value = unit Theory.Value.t
   type KB.conflict += Unresolved_definition of string
   type KB.conflict += Illtyped_program of Type.error list
+  type KB.conflict += Failed_primitive of KB.Name.t * string
 
   val program : (Theory.Source.cls, program) KB.slot
   val definition : (Theory.program, Theory.Label.t option) KB.slot
@@ -151,6 +153,8 @@ module Semantics : sig
   val symbol : (Theory.Value.cls, String.t option) KB.slot
   val static : (Theory.Value.cls, Bitvec.t option) KB.slot
   val enable : ?stdout:Format.formatter -> unit -> unit
+  val failp : ('a, Format.formatter, unit, 'b KB.t) format4 -> 'a
+
 
   val declare :
     ?types:Type.signature ->
@@ -160,6 +164,28 @@ module Semantics : sig
     string -> unit
 
 
+  module Value : sig
+    type t = unit Theory.Value.t
+    val static : Bitvec.t -> t
+    val symbol : string -> t
+    val custom : (Theory.Value.cls, 'a) KB.slot -> 'a -> t
+    val nil : t
+  end
+
+
+  module Effect : sig
+    type t = unit Theory.Effect.t
+    val pure : Value.t -> t
+    val return : Value.t -> t KB.t
+  end
+
+  val signal :
+    ?params:[< Type.parameters] ->
+    ?docs:string ->
+    (Theory.program,'p) KB.slot ->
+    (Theory.Label.t -> 'p -> Value.t list KB.t) ->
+    unit
+
   val documentation : Theory.Unit.t -> Doc.index KB.t
 end
 
@@ -169,6 +195,8 @@ module Unit : sig
   val language : Theory.language
 end
 
+
+
 module Attribute : sig
   type 'a t
   type set

lib/bap_primus/bap_primus_lisp_parse.ml

@@ -66,17 +66,23 @@ let is_quoted s =
   n > 1 && Char.(s.[0] = '"') && Char.(s.[n - 1] = '"')
 
 let is_symbol s =
-  String.length s > 1 && Char.(s.[0] = '\'')
+  String.length s > 1 && match s.[0] with
+  | '\'' | ':' -> true
+  | _ -> false
+
+
+let is_keyword s =
+  String.length s > 1 && Char.(s.[0] = ':')
+
 
 let unquote s =
   if is_quoted s
   then String.sub ~pos:1 ~len:(String.length s - 2) s
   else s
 
-let symbol s =
-  if is_symbol s
-  then String.subo ~pos:1 s
-  else s
+let symbol ~package s =
+  if is_keyword s then KB.Name.read s
+  else KB.Name.read ~package (String.subo ~pos:1 s)
 
 module Parse = struct
   open Program.Items
@@ -209,7 +215,7 @@ module Parse = struct
 
       let sym ({id;eq;data=r} as s)  =
         if is_symbol r
-        then cons (Sym { s with data = qualify@@symbol s.data})
+        then cons (Sym { s with data = symbol ~package s.data})
         else match Var.read ~package id eq r with
           | Error e -> fail (Bad_var_literal e) tree
           | Ok v -> cons (Var v) in
@@ -288,9 +294,6 @@ module Parse = struct
     | Some {data=Atom ":hex"} -> hex
     | Some here -> fail Unknown_subst_syntax here
 
-  let is_keyarg = function
-    | {data=Atom s} -> Char.(s.[0] = ':')
-    | _ -> false
 
   let constrained prog attrs =
     Program.with_context prog @@
@@ -331,6 +334,10 @@ module Parse = struct
     Def.Para.create ?docs
       ~attrs name (parse (constrained prog attrs) body) tree
 
+  let is_keyarg = function
+    | {data=Atom s} -> is_keyword s
+    | _ -> false
+
   let defsubst ?docs ?(attrs=[]) name body prog gattrs tree =
     let syntax = match body with
       | s :: _ when is_keyarg s -> Some s

lib/bap_primus/bap_primus_lisp_program.ml

@@ -115,7 +115,7 @@ let targets {exports} package = match Map.find exports package with
   | Some packs -> packs
 
 (* [transitive_closure p] is the set of packages in which
-   definition from p are visible (p including).
+   the definitions from p are visible (p including).
 *)
 let rec transitive_closure program from =
   let init = Set.singleton (module String) from in
@@ -1447,6 +1447,7 @@ module Typing = struct
       let name = KB.Name.unqualified name in
       match Map.find sigs name with
       | Some [x] -> Some x
+      | Some _ -> None
       | _ -> None
 
   let check_methods glob {context; library} g =

lib/bap_primus/bap_primus_lisp_resolve.ml

@@ -35,10 +35,10 @@ type ('t,'a,'b) many = ('t,'a,('t Def.t * 'b) list) resolver
 
 type exn += Failed of string * Context.t * resolution
 
-let interns d name = String.equal (Def.name d) name
+let has_name d name = String.equal (Def.name d) name
 
 (* all definitions with the given name *)
-let stage1 has_name defs name =
+let stage1 defs name =
   List.filter defs ~f:(fun def -> has_name def name)
 
 let context def =
@@ -147,12 +147,12 @@ let one = function
 
 let many xs = Some xs
 
-let run choose namespace overload prog item name =
+let run choose overload prog item name =
   Program.in_package (KB.Name.package name) prog @@ fun prog ->
   let name = KB.Name.unqualified name in
   let ctxts = Program.context prog in
   let defs = Program.get ~name prog item in
-  let s1 = stage1 namespace defs name in
+  let s1 = stage1 defs name in
   let s2 = stage2 ctxts s1 in
   let s3 = stage3 s2 in
   let s4 = stage4 s3 in
@@ -171,25 +171,25 @@ let run choose namespace overload prog item name =
       })
 
 let extern typechecks prog item name args =
-  run one interns (overload_defun typechecks args) prog item name
+  run one (overload_defun typechecks args) prog item name
 
 let defun typechecks prog item name args =
-  run one interns (overload_defun typechecks args) prog item name
+  run one (overload_defun typechecks args) prog item name
 
 let meth typechecks prog item name args =
-  run many interns (overload_meth typechecks args) prog item name
+  run many (overload_meth typechecks args) prog item name
 
 let macro prog item name code =
-  run one interns (overload_macro code) prog item name
+  run one (overload_macro code) prog item name
 
 let primitive prog item name () =
-  run one interns overload_primitive prog item name
+  run one overload_primitive prog item name
 
 let semantics prog item name () =
-  run one interns overload_primitive prog item name
+  run one overload_primitive prog item name
 
 let subst prog item name () =
-  run one interns overload_primitive prog item name
+  run one overload_primitive prog item name
 
 let const = subst