From 72066bb7a3774fa218ba2a60f98cb6c4cd1f10ef Mon Sep 17 00:00:00 2001 From: Ivan Gotovchits Date: Tue, 16 Nov 2021 15:00:33 -0500 Subject: [PATCH] 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 | 2 +- lib/bap_primus/bap_primus.mli | 95 ++++++++- lib/bap_primus/bap_primus_lisp.mli | 28 +++ lib/bap_primus/bap_primus_lisp_parse.ml | 25 ++- 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 | 189 ++++++++++++++---- lib/bap_primus/bap_primus_lisp_semantics.mli | 33 ++- lib/knowledge/bap_knowledge.ml | 68 +++++-- lib/knowledge/bap_knowledge.mli | 23 +++ .../primus_lisp_semantic_primitives.ml | 2 +- 11 files changed, 404 insertions(+), 86 deletions(-) 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 diff --git a/lib/bap_primus/bap_primus.mli b/lib/bap_primus/bap_primus.mli index 1367391aa..fcefabe24 100644 --- a/lib/bap_primus/bap_primus.mli +++ b/lib/bap_primus/bap_primus.mli @@ -3867,6 +3867,10 @@ 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 @@ -3879,6 +3883,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. @@ -3988,14 +3999,96 @@ 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 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 diff --git a/lib/bap_primus/bap_primus_lisp.mli b/lib/bap_primus/bap_primus_lisp.mli index e10387fb7..3c851c5fe 100644 --- a/lib/bap_primus/bap_primus_lisp.mli +++ b/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 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 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 2d7bd17ad..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 = @@ -219,6 +270,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) @@ -480,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 -> @@ -492,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 - | 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 -> @@ -564,7 +646,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 @@ -601,6 +683,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,29 +698,45 @@ 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 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 @@ -652,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 @@ -690,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 399207073..3e3e4a7b3 100644 --- a/lib/bap_primus/bap_primus_lisp_semantics.mli +++ b/lib/bap_primus/bap_primus_lisp_semantics.mli @@ -3,9 +3,10 @@ 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 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 @@ -25,8 +28,36 @@ 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 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 + +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/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]. 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