From 6fb73314143cee8398e2214d17160f21459fb568 Mon Sep 17 00:00:00 2001 From: ivg Date: Tue, 16 Nov 2021 10:50:28 -0500 Subject: [PATCH 1/6] adds forward-chaining rules to the knowledge base --- lib/knowledge/bap_knowledge.ml | 68 ++++++++++++++++++++++++--------- lib/knowledge/bap_knowledge.mli | 23 +++++++++++ 2 files changed, 72 insertions(+), 19 deletions(-) diff --git a/lib/knowledge/bap_knowledge.ml b/lib/knowledge/bap_knowledge.ml index 60178844d..c76ce28b2 100644 --- a/lib/knowledge/bap_knowledge.ml +++ b/lib/knowledge/bap_knowledge.ml @@ -2070,8 +2070,8 @@ module Knowledge = struct open Knowledge.Syntax module Slot = struct - type 'p promise = { - run : Oid.t -> unit Knowledge.t; + type ('p,'r) action = { + run : Oid.t -> 'r; pid : pid; } @@ -2081,7 +2081,8 @@ module Knowledge = struct key : 'p Dict.Key.t; name : Name.t; desc : string option; - promises : (pid, 'p promise) Hashtbl.t; + promises : (pid, ('p,unit knowledge) action) Hashtbl.t; + watchers : (pid, ('p,'p -> unit knowledge) action) Hashtbl.t; } type pack = Pack : ('a,'p) t -> pack @@ -2101,8 +2102,9 @@ module Knowledge = struct Option.iter persistent (Record.register_persistent key); Record.register_domain key dom; let promises = Hashtbl.create (module Pid) in + let watchers = Hashtbl.create (module Pid) in let cls = Class.refine cls () in - let slot = {cls; dom; key; name; desc; promises} in + let slot = {cls; dom; key; name; desc; promises; watchers} in register slot; slot @@ -2454,26 +2456,36 @@ module Knowledge = struct trace; }) + let commit : type a p. (a,p) slot -> a obj -> p -> unit Knowledge.t = + fun slot obj x -> + get () >>= function {classes} as s -> + let {Env.vals} as objs = + match Map.find classes slot.cls.name with + | None -> Env.empty_class + | Some objs -> objs in + try put { + s with classes = Map.set classes ~key:slot.cls.name ~data:{ + objs with vals = Map.update vals obj ~f:(function + | None -> Record.(put slot.key empty x) + | Some v -> match Record.commit slot.dom slot.key v x with + | Ok r -> r + | Error err -> raise (Record.Merge_conflict err))}} + with Record.Merge_conflict err -> + non_monotonic slot obj err @@ + Caml.Printexc.get_raw_backtrace () + + let notify {Slot.watchers} obj data = + Hashtbl.data watchers |> + Knowledge.List.iter ~f:(fun {Slot.run} -> + run obj data) + let provide : type a p. (a,p) slot -> a obj -> p -> unit Knowledge.t = fun slot obj x -> if Object.is_null obj || Domain.is_empty slot.dom x then Knowledge.return () else - get () >>= function {classes} as s -> - let {Env.vals} as objs = - match Map.find classes slot.cls.name with - | None -> Env.empty_class - | Some objs -> objs in - try put { - s with classes = Map.set classes ~key:slot.cls.name ~data:{ - objs with vals = Map.update vals obj ~f:(function - | None -> Record.(put slot.key empty x) - | Some v -> match Record.commit slot.dom slot.key v x with - | Ok r -> r - | Error err -> raise (Record.Merge_conflict err))}} - with Record.Merge_conflict err -> - non_monotonic slot obj err @@ - Caml.Printexc.get_raw_backtrace () + commit slot obj x >>= fun () -> + notify slot obj x let pids = ref Pid.zero @@ -2485,6 +2497,12 @@ module Knowledge = struct (function Empty _ -> Knowledge.return missing | other -> Knowledge.fail other) + let register_watcher (type a b)(s : (a,b) slot) run = + Pid.incr pids; + let pid = !pids in + Hashtbl.add_exn s.watchers pid {run; pid}; + pid + let register_promise (type a b)(s : (a,b) slot) run = Pid.incr pids; let pid = !pids in @@ -2494,6 +2512,9 @@ module Knowledge = struct let remove_promise (s : _ slot) pid = Hashtbl.remove s.promises pid + let remove_watcher (s : _ slot) pid = + Hashtbl.remove s.watchers pid + let wrap (s : _ slot) get obj = let missing = Domain.empty s.dom in with_empty ~missing @@ fun () -> @@ -2642,6 +2663,15 @@ module Knowledge = struct current slot id + let observe s run = + ignore @@ register_watcher s run + + let observing s ~observe:run scoped = + let pid = register_watcher s run in + scoped () >>= fun r -> + remove_watcher s pid; + Knowledge.return r + let require (slot : _ slot) obj = collect slot obj >>= fun x -> if (Domain.is_empty slot.dom x) diff --git a/lib/knowledge/bap_knowledge.mli b/lib/knowledge/bap_knowledge.mli index 509557811..8a7771310 100644 --- a/lib/knowledge/bap_knowledge.mli +++ b/lib/knowledge/bap_knowledge.mli @@ -269,6 +269,29 @@ module Knowledge : sig val proposing : agent -> ('a, 'p opinions) slot -> propose:('a obj -> 'p t) -> (unit -> 's t) -> 's t + (** [observe property push] calls [push] when the [property] changes. + + Dual to [promise], [observe] enables forward-chaining rules and + propagates knowledge whenever [property] value is refined. + + Calls [push x v] when the [property] value of an object [x] is + refined to [v]. It is guaranteed that [v] is never empty. + + @since 2.4.0 + *) + val observe : ('a,'p) slot -> ('a obj -> 'p -> unit knowledge) -> unit + + (** [observing property ~observe:push scope] observes the property in a [scope]. + + This operation is dual to [promising] and it observes the + property only during the time when the [scope] computation is + evaluate and removes the observer after that. + + @since 2.4.0 + + *) + val observing : ('a,'p) slot -> observe:('a obj -> 'p -> unit knowledge) -> + (unit -> 'r knowledge) -> 'r knowledge (** [with_empty ~missing f x] evaluates [f ()] and if it fails on an empty immediately evaluates to [return missing]. From c6b4209f9f53c3ec4f9affd4488b6d6b173c93da Mon Sep 17 00:00:00 2001 From: ivg Date: Thu, 11 Nov 2021 15:30:57 -0500 Subject: [PATCH 2/6] adds some useful primitives for writing primitives to Primus --- lib/bap_primus/bap_primus.mli | 70 +++++++++++++++++++- lib/bap_primus/bap_primus_lisp.mli | 19 ++++++ lib/bap_primus/bap_primus_lisp_semantics.ml | 26 +++++++- lib/bap_primus/bap_primus_lisp_semantics.mli | 19 ++++++ 4 files changed, 132 insertions(+), 2 deletions(-) diff --git a/lib/bap_primus/bap_primus.mli b/lib/bap_primus/bap_primus.mli index 1367391aa..874ed3a33 100644 --- a/lib/bap_primus/bap_primus.mli +++ b/lib/bap_primus/bap_primus.mli @@ -3867,7 +3867,6 @@ text ::= ?any atom that is not recognized as a ? *) module Semantics : sig - (** occurs when no matching definition is found The reason why no match is selected is provided as the @@ -3879,6 +3878,13 @@ text ::= ?any atom that is not recognized as a ? (** 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. @@ -3991,11 +3997,73 @@ text ::= ?any atom that is not recognized as a ? ?body:(Theory.Target.t -> (Theory.Label.t -> Theory.Value.Top.t list -> unit Theory.eff) KB.t) -> string -> 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 programmers 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 = unit Theory.Value.t + + (** [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 diff --git a/lib/bap_primus/bap_primus_lisp.mli b/lib/bap_primus/bap_primus_lisp.mli index e10387fb7..3e18aec68 100644 --- a/lib/bap_primus/bap_primus_lisp.mli +++ b/lib/bap_primus/bap_primus_lisp.mli @@ -143,6 +143,7 @@ end module Semantics : sig 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 +152,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 -> @@ -159,6 +162,20 @@ module Semantics : sig ?body:(Theory.Target.t -> (Theory.Label.t -> Theory.Value.Top.t list -> unit Theory.eff) KB.t) -> 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 documentation : Theory.Unit.t -> Doc.index KB.t end @@ -169,6 +186,8 @@ module Unit : sig val language : Theory.language end + + module Attribute : sig type 'a t type set diff --git a/lib/bap_primus/bap_primus_lisp_semantics.ml b/lib/bap_primus/bap_primus_lisp_semantics.ml index 2d7bd17ad..72090d816 100644 --- a/lib/bap_primus/bap_primus_lisp_semantics.ml +++ b/lib/bap_primus/bap_primus_lisp_semantics.ml @@ -219,6 +219,21 @@ let sym str = intern name >>| set_static v +module Value = struct + type t = value + let empty : t = Theory.Value.Top.empty + let custom p x = empty.$[p] <- x + let static x = custom static_slot (Some x) + let symbol s = custom symbol (Some s) + let nil = static Bitvec.zero +end + +module Effect = struct + type t = effect + let pure x : t = empty.$[Theory.Semantics.value] <- x + let return x : t KB.t = KB.return@@pure x +end + let static x = KB.Value.get static_slot (res x) @@ -601,6 +616,12 @@ module Unit = struct end type KB.conflict += Illtyped_program of Program.Type.error list +type KB.conflict += Failed_primitive of KB.Name.t * string +type KB.conflict += Primitive_failed of string + +let failp fmt = + Format.kasprintf (fun msg -> + KB.fail (Primitive_failed msg)) fmt let primitive name defn args = let open KB.Syntax in @@ -610,7 +631,10 @@ let primitive name defn args = KB.provide definition obj (Some defn); KB.provide Property.args obj (Some args); ] >>= fun () -> - KB.collect Theory.Semantics.slot obj + KB.catch (KB.collect Theory.Semantics.slot obj) + (function Primitive_failed msg -> + KB.fail (Failed_primitive (name,msg)) + | other -> KB.fail other) let link_library target prog = let open KB.Let in diff --git a/lib/bap_primus/bap_primus_lisp_semantics.mli b/lib/bap_primus/bap_primus_lisp_semantics.mli index 399207073..49389c1bb 100644 --- a/lib/bap_primus/bap_primus_lisp_semantics.mli +++ b/lib/bap_primus/bap_primus_lisp_semantics.mli @@ -6,6 +6,7 @@ open Bap_primus_lisp_program 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 @@ -14,6 +15,8 @@ val args : (Theory.program, unit Theory.Value.t list option) KB.slot 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 typed_program : Theory.Unit.t -> program KB.t @@ -30,3 +33,19 @@ module Unit : sig val is_lisp : Theory.Unit.t -> bool KB.t val language : Theory.language end + + +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 From 5a001d15440126fd9d855b7b3b39243dd68a0c79 Mon Sep 17 00:00:00 2001 From: ivg Date: Fri, 12 Nov 2021 11:46:55 -0500 Subject: [PATCH 3/6] 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. --- lib/bap_primus/bap_primus_lisp_parse.ml | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/lib/bap_primus/bap_primus_lisp_parse.ml b/lib/bap_primus/bap_primus_lisp_parse.ml index 60dcf873c..55dc2dd39 100644 --- a/lib/bap_primus/bap_primus_lisp_parse.ml +++ b/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 From 3f948770fa860aaaef71d4fcaa7e6afd474a2388 Mon Sep 17 00:00:00 2001 From: ivg Date: Fri, 12 Nov 2021 11:51:12 -0500 Subject: [PATCH 4/6] 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. --- lib/bap_primus/bap_primus_lisp_semantics.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/bap_primus/bap_primus_lisp_semantics.ml b/lib/bap_primus/bap_primus_lisp_semantics.ml index 72090d816..46ea21b26 100644 --- a/lib/bap_primus/bap_primus_lisp_semantics.ml +++ b/lib/bap_primus/bap_primus_lisp_semantics.ml @@ -512,7 +512,7 @@ module Prelude(CT : Theory.Core) = struct | None -> match Resolve.semantics prog Key.semantics name () with | Some Ok (sema,()) -> - Def.Sema.apply sema defn xs + Def.Sema.apply sema defn xs >>= reify_sym | Some (Error problem) -> unresolved name problem | None -> let msg = Format.asprintf "No definition is found for %a" @@ -579,7 +579,7 @@ module Prelude(CT : Theory.Core) = struct !!beff; ] !!(res beff) and prim ?(package="core") name args = - call (KB.Name.read ~package name) args >>= reify_sym in + call (KB.Name.read ~package name) args in match args with | Some args -> call ~toplevel:true name args From 32194398fa8a746a5212b2087d3a30c74c6f2067 Mon Sep 17 00:00:00 2001 From: ivg Date: Mon, 15 Nov 2021 15:53:42 -0500 Subject: [PATCH 5/6] implements methods in the Primus Lisp semantics interpreter --- lib/bap_primus/bap_primus.mli | 31 +++- lib/bap_primus/bap_primus_lisp.mli | 9 + lib/bap_primus/bap_primus_lisp_program.ml | 3 +- lib/bap_primus/bap_primus_lisp_resolve.ml | 22 +-- lib/bap_primus/bap_primus_lisp_semantics.ml | 161 +++++++++++++----- lib/bap_primus/bap_primus_lisp_semantics.mli | 14 +- .../primus_lisp_semantic_primitives.ml | 2 +- 7 files changed, 185 insertions(+), 57 deletions(-) diff --git a/lib/bap_primus/bap_primus.mli b/lib/bap_primus/bap_primus.mli index 874ed3a33..fcefabe24 100644 --- a/lib/bap_primus/bap_primus.mli +++ b/lib/bap_primus/bap_primus.mli @@ -3867,6 +3867,11 @@ text ::= ?any atom that is not recognized as a ? *) 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 The reason why no match is selected is provided as the @@ -3994,15 +3999,35 @@ text ::= ?any atom that is not recognized as a ? ?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 programmers errors + This conflict should used to report programmer errors that are not representable via the type system (or slipped through the gradual type checker). @@ -4020,7 +4045,7 @@ text ::= ?any atom that is not recognized as a ? @since 2.4.0 *) module Value : sig - type t = unit Theory.Value.t + type t = value (** [static x] a value statically equal to [x].*) val static : Bitvec.t -> t diff --git a/lib/bap_primus/bap_primus_lisp.mli b/lib/bap_primus/bap_primus_lisp.mli index 3e18aec68..3c851c5fe 100644 --- a/lib/bap_primus/bap_primus_lisp.mli +++ b/lib/bap_primus/bap_primus_lisp.mli @@ -141,6 +141,7 @@ 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 @@ -162,6 +163,7 @@ module Semantics : sig ?body:(Theory.Target.t -> (Theory.Label.t -> Theory.Value.Top.t list -> unit Theory.eff) KB.t) -> string -> unit + module Value : sig type t = unit Theory.Value.t val static : Bitvec.t -> t @@ -177,6 +179,13 @@ module Semantics : sig 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 diff --git a/lib/bap_primus/bap_primus_lisp_program.ml b/lib/bap_primus/bap_primus_lisp_program.ml index bbdfe059e..3d3d754b7 100644 --- a/lib/bap_primus/bap_primus_lisp_program.ml +++ b/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 = diff --git a/lib/bap_primus/bap_primus_lisp_resolve.ml b/lib/bap_primus/bap_primus_lisp_resolve.ml index 74dd98a5f..0259de419 100644 --- a/lib/bap_primus/bap_primus_lisp_resolve.ml +++ b/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 diff --git a/lib/bap_primus/bap_primus_lisp_semantics.ml b/lib/bap_primus/bap_primus_lisp_semantics.ml index 46ea21b26..382a4972f 100644 --- a/lib/bap_primus/bap_primus_lisp_semantics.ml +++ b/lib/bap_primus/bap_primus_lisp_semantics.ml @@ -60,11 +60,12 @@ let program = ~join:(fun x y -> Ok (Program.merge x y)) +type kind = Prim | Defn | Meth | Data [@@deriving sexp] type program = { prog : Program.t; places : unit Theory.var Map.M(KB.Name).t; - names : Set.M(KB.Name).t; + names : kind Map.M(KB.Name).t; } let typed = KB.Class.property Theory.Source.cls "typed-program" @@ -73,17 +74,33 @@ let typed = KB.Class.property Theory.Source.cls "typed-program" ~equal:(fun x y -> Program.equal x.prog y.prog) + +type problem = + | Resolution of Resolve.resolution + | Uncallable + | Unexpected of kind + +let pp_problem ppf = function + | Resolution err -> Resolve.pp_resolution ppf err + | Uncallable -> + Format.fprintf ppf "This item is not callable" + | Unexpected Prim -> () + | Unexpected kind -> + Format.fprintf ppf "internal error, unexpected %a" + Sexp.pp (sexp_of_kind kind) + + let unresolved name problem = let msg = - Format.asprintf "Failed to find a definition for %a. %a" + Format.asprintf "Failed to find a definition for %a.@ %a@." KB.Name.pp name - Resolve.pp_resolution problem in + pp_problem problem in KB.fail (Unresolved_definition msg) let resolve prog item name = match Resolve.semantics prog item name () with | None -> !!None - | Some (Error problem) -> unresolved name problem + | Some (Error problem) -> unresolved name (Resolution problem) | Some (Ok (fn,_)) -> !!(Some fn) let check_arg _ _ = true @@ -97,6 +114,7 @@ type info = { types : (Theory.Target.t -> Type.signature); docs : string; body : body option; + kind : [`meth | `defn] } let library = Hashtbl.create (module KB.Name) @@ -134,25 +152,58 @@ let definition = ~equal:Theory.Label.equal ~inspect:Theory.Label.sexp_of_t +let dummy_type _ = Type.{ + args = []; + rest = Some any; + ret = any; + } + + let declare - ?(types=fun _ -> Type.{ - args = []; - rest = Some any; - ret = any; - }) + ?(types=dummy_type) ?(docs="undocumented") ?package ?body name = let name = KB.Name.create ?package name in if Hashtbl.mem library name - then invalid_argf "A primitive `%s' already exists, please \ - choose a different name for your primitive" + then invalid_argf "A semantic primitive `%s' already exists, \ + please choose a different name for your \ + primitive" (KB.Name.show name) (); Hashtbl.add_exn library name { docs; types; body; + kind = `defn; + } + +let signal ?params ?(docs="undocumented") property reflect = + let name = KB.Slot.name property in + if Hashtbl.mem library name + then invalid_argf "The signal `%s' is already reflected." + (KB.Name.show name) (); + let app ts t = List.(ts >>| fun typ -> typ t) in + let types t = match params with + | None -> dummy_type t + | Some (`All typ) -> Type.signature ~rest:(typ t) [] Any + | Some (`Tuple ts) -> Type.signature (app ts t) Any + | Some (`Gen (ts,r)) -> + Type.signature ~rest:(r t) (app ts t) Any in + KB.observe property @@begin fun lbl x -> + let* args = reflect lbl x in + KB.sequence [ + KB.provide Property.name lbl (Some name); + KB.provide Property.args lbl (Some args); + ] >>= fun () -> + KB.collect Theory.Semantics.slot lbl >>| ignore + end; + Hashtbl.add_exn library name { + docs; + types; + body=None; + kind=`meth; } + let sort = Theory.Value.sort let size x = Theory.Bitv.size (sort x) let lisp_machine = @@ -495,6 +546,13 @@ module Prelude(CT : Theory.Core) = struct ]] ] !!cres and call ?(toplevel=false) name xs = + match Map.find program.names name with + | None when toplevel -> !!Insn.empty + | Some Prim | None -> call_primitive name xs + | Some Defn -> call_defn name xs + | Some Meth -> call_meth name xs + | Some Data -> unresolved name Uncallable + and call_defn name xs = match Resolve.defun check_arg prog Key.func name xs with | Some (Ok (fn,_)) when is_external fn -> sym (Def.name fn) >>= fun dst -> @@ -507,17 +565,26 @@ module Prelude(CT : Theory.Core) = struct Env.del_args bs >>= fun () -> !!eff | Some (Error problem) -> - unresolved name problem - | None when toplevel -> !!Insn.empty - | None -> - match Resolve.semantics prog Key.semantics name () with - | Some Ok (sema,()) -> - Def.Sema.apply sema defn xs >>= reify_sym - | Some (Error problem) -> unresolved name problem - | None -> - let msg = Format.asprintf "No definition is found for %a" - KB.Name.pp name in - KB.fail (Unresolved_definition msg) + unresolved name (Resolution problem) + | None -> unresolved name (Unexpected Defn) + and call_meth name xs = + match Resolve.meth check_arg prog Key.meth name xs with + | Some (Error problem) -> unresolved name (Resolution problem) + | Some (Ok mets) -> + KB.List.fold mets ~init:empty ~f:(fun effects (meth,bs) -> + Env.set_args word bs >>= fun bs -> + Scope.clear >>= fun scope -> + eval (Def.Meth.body meth) >>= fun eff -> + Scope.restore scope >>= fun () -> + Env.del_args bs >>| fun () -> + KB.Value.merge effects eff) + | None -> unresolved name (Unexpected Meth) + and call_primitive name xs = + match Resolve.semantics prog Key.semantics name () with + | Some Ok (sema,()) -> + Def.Sema.apply sema defn xs >>= reify_sym + | Some (Error problem) -> unresolved name (Resolution problem) + | None -> unresolved name (Unexpected Prim) and app name xs = map xs >>= fun (aeff,xs) -> call name xs >>= fun peff -> @@ -639,24 +706,37 @@ let primitive name defn args = let link_library target prog = let open KB.Let in Hashtbl.to_alist library |> - KB.List.fold ~init:prog ~f:(fun prog (name,{types; docs; body}) -> + KB.List.fold ~init:prog ~f:(fun prog (name,{types; docs; body; kind}) -> let types = types target in - match body with - | None -> + match kind with + | `meth -> KB.return @@ - Program.add prog Program.Items.semantics @@ - Def.Sema.create ~docs ~types name (primitive name) - | Some body -> - let+ fn = body target in - Program.add prog Program.Items.semantics @@ - Def.Sema.create ~docs ~types name fn) + Program.add prog Program.Items.signal @@ + Def.Signal.create ~types ~docs (KB.Name.show name) + | `defn -> + match body with + | None -> + KB.return @@ + Program.add prog Program.Items.semantics @@ + Def.Sema.create ~docs ~types name (primitive name) + | Some body -> + let+ fn = body target in + Program.add prog Program.Items.semantics @@ + Def.Sema.create ~docs ~types name fn) -let collect_names key prog = +let collect_names kind key prog = Program.fold prog key ~f:(fun ~package def names -> let name = Def.name def in - Set.add names (KB.Name.create ~package name)) - ~init:(Set.empty (module KB.Name)) + Map.set names (KB.Name.create ~package name) kind) + ~init:(Map.empty (module KB.Name)) + +let merge_names names = + List.reduce names ~f:(Map.merge_skewed + ~combine:(fun ~key:_ _ v -> v)) |> + function None -> Map.empty (module KB.Name) + | Some r -> r + let obtain_typed_program unit = let open KB.Syntax in @@ -676,11 +756,12 @@ let obtain_typed_program unit = let name = KB.Name.create ~package (Def.name place) in Map.set places name (Def.Place.location place)) ~init:(Map.empty (module KB.Name)) in - let names = Set.union_list (module KB.Name) [ - collect_names Key.func prog; - collect_names Key.semantics prog; - collect_names Key.para prog; - collect_names Key.const prog + let names = merge_names [ + collect_names Defn Key.func prog; + collect_names Prim Key.semantics prog; + collect_names Data Key.para prog; + collect_names Data Key.const prog; + collect_names Meth Key.meth prog; ] in let program = {prog; places; names} in match Program.Type.errors tprog with @@ -714,7 +795,7 @@ let provide_semantics ?(stdout=Format.std_formatter) () = let* unit = obj-->?Theory.Label.unit in let* name = obj-->?Property.name in let* prog = obtain_typed_program unit in - require (Set.mem prog.names name) @@ fun () -> + require (Map.mem prog.names name) @@ fun () -> let* args = obj-->Property.args in let* target = KB.collect Theory.Unit.target unit in let bits = Theory.Target.bits target in diff --git a/lib/bap_primus/bap_primus_lisp_semantics.mli b/lib/bap_primus/bap_primus_lisp_semantics.mli index 49389c1bb..3e3e4a7b3 100644 --- a/lib/bap_primus/bap_primus_lisp_semantics.mli +++ b/lib/bap_primus/bap_primus_lisp_semantics.mli @@ -3,7 +3,7 @@ open Bap.Std open Bap_primus_lisp_types open Bap_primus_lisp_program - +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 @@ -28,6 +28,8 @@ val declare : string -> unit + + module Unit : sig val create : ?name:string -> Theory.Target.t -> Theory.Unit.t KB.t val is_lisp : Theory.Unit.t -> bool KB.t @@ -49,3 +51,13 @@ module Effect : sig val pure : Value.t -> t val return : Value.t -> t KB.t end + +val signal : + ?params:[< `All of Theory.target -> Bap_primus_lisp_types.typ + | `Gen of + (Theory.target -> Bap_primus_lisp_types.typ) list * + (Theory.target -> Bap_primus_lisp_types.typ) + | `Tuple of (Theory.target -> Bap_primus_lisp_types.typ) list ] -> + ?docs:string -> (Theory.program, 'p) KB.slot -> + (Theory.Label.t -> 'p -> Value.t list KB.t) -> + unit diff --git a/plugins/primus_lisp/primus_lisp_semantic_primitives.ml b/plugins/primus_lisp/primus_lisp_semantic_primitives.ml index 8eef15cfe..d5d7af404 100644 --- a/plugins/primus_lisp/primus_lisp_semantic_primitives.ml +++ b/plugins/primus_lisp/primus_lisp_semantic_primitives.ml @@ -626,7 +626,7 @@ module Primitives(CT : Theory.Core)(T : Target) = struct | Some name -> intern name >>= const_int s |> forget | None -> - illformed "symbol requires a value reified to a variable" + illformed "symbol requires a symbolic value" let is_symbol v = forget@@match KB.Value.get Primus.Lisp.Semantics.symbol v with From 97a8f2dae5f5b6aa318445e4f75e49a304cd9f37 Mon Sep 17 00:00:00 2001 From: ivg Date: Tue, 16 Nov 2021 13:18:30 -0500 Subject: [PATCH 6/6] updates the testsuite, uses the newer opam syntax --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 2f3aad254..adde1aa60 100644 --- a/Makefile +++ b/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