From 97cc1a3938ed866a563a03c5ae55ea9be500465d Mon Sep 17 00:00:00 2001 From: Ivan Gotovchits Date: Fri, 5 Nov 2021 18:20:59 -0400 Subject: [PATCH] extends the knowledge monad interface (#1360) This is a quality of life PR (an extract from another PR that I am currently working on) that adds a few useful primitives to the knowledge base monad interface. The most important addition is the new operator `require` that works like `collect` but raises the empty value conflict if the returned value is empty. This function is inteded to be used in the context of promises and proposals that now catch this exception and evaluate the whole scoped expression to the empty value of the computed domain. This vastly simplify the implementation logic of promises for domains that do not use `None` as the empty value. To make things work even more smoothly we extend the KB.Syntax module with a few new operators. First of all, we include the `Monad.Let` directly into the `KB.Syntax` so that you don't need to open `KB.Let` anymore. Next, we introduce `let*?` and `let+?`, which let-binding couterparts of the already existing `>>=?` and `>>|?` infix operators. Next, we add `-->?` to complement `-->`, it collects an optional domain value and fails if it is `None`. Finally, we add indexing operators for accessing fields of KB values. The also come with the empty-checking variants. The PR also applies the new operators to the existing code for the demonstration purposes (and to show that it works). I also believe that the rewritten code is more reable, even despite that I still prefer the infix syntax to the let-binding operators. --- lib/bap_primus/bap_primus_lisp_semantics.ml | 15 +-- lib/knowledge/bap_knowledge.ml | 50 ++++++- lib/knowledge/bap_knowledge.mli | 140 +++++++++++++++++++- plugins/bil/bil_lifter.ml | 16 +-- plugins/primus_lisp/primus_lisp_main.ml | 6 +- plugins/radare2/radare2_main.ml | 13 +- plugins/x86/x86_legacy_bil_lifter.ml | 8 +- 7 files changed, 205 insertions(+), 43 deletions(-) diff --git a/lib/bap_primus/bap_primus_lisp_semantics.ml b/lib/bap_primus/bap_primus_lisp_semantics.ml index ac1904863..2d7bd17ad 100644 --- a/lib/bap_primus/bap_primus_lisp_semantics.ml +++ b/lib/bap_primus/bap_primus_lisp_semantics.ml @@ -685,17 +685,14 @@ let provide_semantics ?(stdout=Format.std_formatter) () = provide Theory.Semantics.slot |> comment "reifies Primus Lisp definitions" end); - let (>>=?) x f = x >>= function - | None -> !!Insn.empty - | Some x -> f x in let require p k = if p then k () else !!Insn.empty in KB.promise Theory.Semantics.slot @@ fun obj -> - KB.collect Theory.Label.unit obj >>=? fun unit -> - KB.collect Property.name obj >>=? fun name -> - obtain_typed_program unit >>= fun prog -> + 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 () -> - KB.collect Property.args obj >>= fun args -> - KB.collect Theory.Unit.target unit >>= fun target -> + let* args = obj-->Property.args in + let* target = KB.collect Theory.Unit.target unit in let bits = Theory.Target.bits target in KB.Context.set State.var State.{ binds = Map.empty (module Theory.Var.Top); @@ -706,7 +703,7 @@ let provide_semantics ?(stdout=Format.std_formatter) () = } >>= fun () -> let* (module Core) = Theory.current in let open Prelude(Core) in - reify stdout prog obj target name args >>= fun res -> + let* res = reify stdout prog obj target name args in KB.collect Disasm_expert.Basic.Insn.slot obj >>| function | Some basic when Insn.(res <> empty) -> Insn.with_basic res basic diff --git a/lib/knowledge/bap_knowledge.ml b/lib/knowledge/bap_knowledge.ml index d2f4a607f..b4af75207 100644 --- a/lib/knowledge/bap_knowledge.ml +++ b/lib/knowledge/bap_knowledge.ml @@ -2442,7 +2442,14 @@ module Knowledge = struct let pids = ref Pid.zero - let register_promise (s : _ slot) run = + type conflict += Empty : ('a,'b) slot -> conflict + + let with_empty ~missing scope = + Knowledge.catch (scope ()) + (function Empty _ -> Knowledge.return missing + | other -> Knowledge.fail other) + + let register_promise (type a b)(s : (a,b) slot) run = Pid.incr pids; let pid = !pids in Hashtbl.add_exn s.promises pid {run; pid}; @@ -2451,9 +2458,14 @@ module Knowledge = struct let remove_promise (s : _ slot) pid = Hashtbl.remove s.promises pid + let wrap (s : _ slot) get obj = + let missing = Domain.empty s.dom in + with_empty ~missing @@ fun () -> + get obj + let promising s ~promise:get scoped = let pid = register_promise s @@ fun obj -> - get obj >>= fun x -> + wrap s get obj >>= fun x -> if Domain.is_empty s.dom x then Knowledge.return () else provide s obj x in @@ -2464,7 +2476,7 @@ module Knowledge = struct let promise s get = ignore @@ register_promise s @@ fun obj -> - get obj >>= fun x -> + wrap s get obj >>= fun x -> if Domain.is_empty s.dom x then Knowledge.return () else provide s obj x @@ -2576,6 +2588,7 @@ module Knowledge = struct | GT | NC -> collect_inner slot obj promises + let collect : type a p. (a,p) slot -> a obj -> p Knowledge.t = fun slot id -> if Object.is_null id @@ -2592,6 +2605,13 @@ module Knowledge = struct leave_slot slot id >>= fun () -> current slot id + + let require (slot : _ slot) obj = + collect slot obj >>= fun x -> + if (Domain.is_empty slot.dom x) + then Knowledge.fail (Empty slot) + else !!x + let resolve slot obj = collect slot obj >>| Opinions.choice @@ -2792,10 +2812,17 @@ module Knowledge = struct module Syntax = struct include Knowledge.Syntax + include Knowledge.Let + let (-->) x p = collect p x let (<--) p f = promise p f let (//) c s = Object.read c s + let (-->?) x p = + collect p x >>= function + | None -> Knowledge.fail (Empty p) + | Some x -> !!x + let (>>=?) x f = x >>= function | None -> Knowledge.return None @@ -2805,6 +2832,23 @@ module Knowledge = struct x >>| function | None -> None | Some x -> f x + + let (let*?) = (>>=?) + let (let+?) = (>>|?) + + + let (.$[]) v s = Value.get s v + let (.$[]<-) v s x = Value.put s v x + + let (.?[]) v s = match v.$[s] with + | Some v -> !!v + | None -> Knowledge.fail (Empty s) + + let (.![]) v s = + let r = v.$[s] in + if Domain.is_empty (Slot.domain s) r + then Knowledge.fail (Empty s) + else !!r end module type S = sig diff --git a/lib/knowledge/bap_knowledge.mli b/lib/knowledge/bap_knowledge.mli index a86157d56..509557811 100644 --- a/lib/knowledge/bap_knowledge.mli +++ b/lib/knowledge/bap_knowledge.mli @@ -164,6 +164,16 @@ module Knowledge : sig value of the property domain is returned as the result. *) val collect : ('a,'p) slot -> 'a obj -> 'p t + (** [require p x] collects the property [p] and fails if it is empty. + + When [require p x] fails in the scope of a {!promise}, + {!proposal}, or in the scope of [with_empty], then the scoped + computation immediately returns the empty value. + + @since 2.4.0 + *) + val require : ('a,'p) slot -> 'a obj -> 'p t + (** [resolve p x] resolves the multi-opinion property [p] @@ -186,6 +196,7 @@ module Knowledge : sig then [provide p x v] diverges into a conflict. *) val provide : ('a,'p) slot -> 'a obj -> 'p -> unit t + (** [suggest a p x v] suggests [v] as the value for the property [p]. The same as [provide] except the provided value is predicated by @@ -195,19 +206,22 @@ module Knowledge : sig (** [promise p f] promises to compute the property [p]. - If no knowledge exists about the property [p] of - an object [x], then [f x] is invoked to provide an - initial value. + If the property [p] of [x] is not provided, then [f x] is + invoked to provide the initial value, when [p] is collected. If there are more than one promises, then they all must provide a consistent answer. The function [f] may refer to the property [p] directly or indirectly. In that case the least fixed point solution of all functions [g] involved in the property computation is computed. + + @since 2.4.0 if [require] is called in the scope of the promise + and fails, the the whole promise immediately returns the empty + value of the property domain, i.e., [f] is wrapped into + [with_missing]. *) val promise : ('a,'p) slot -> ('a obj -> 'p t) -> unit - (** [promising p ~promise f] evaluates [f ()] under [promise] and retracts it after [f] is evaluated. @@ -215,6 +229,12 @@ module Knowledge : sig evaluation of [f ()]. @since 2.2.0 + + + @since 2.4.0 if [require] is called in the scope of the promise + and fails, the the whole promise immediately returns the empty + value of the property domain, i.e., [promise] (not [f]) wrapped + into [with_missing]. *) val promising : ('a,'p) slot -> promise:('a obj -> 'p t) -> (unit -> 's t) -> 's t @@ -223,6 +243,12 @@ module Knowledge : sig The same as [promise] except that it promises a value for an opinion-based property. + + @since 2.4.0 if [require] is called in the scope of the promise + and fails, the the whole promise immediately returns the empty + value of the property domain, i.e., [f] is wrapped into + [with_missing]. + *) val propose : agent -> ('a, 'p opinions) slot -> ('a obj -> 'p t) -> unit @@ -233,10 +259,25 @@ module Knowledge : sig value for an opinion-based property. @since 2.2.0 + + @since 2.4.0 if [require] are called in the scope of the proposal + and fails, the the whole proposal immediately returns the empty + value of the property domain, i.e., [propose] (not [f]) wrapped + into [with_missing]. + *) val proposing : agent -> ('a, 'p opinions) slot -> propose:('a obj -> 'p t) -> (unit -> 's t) -> 's t + + (** [with_empty ~missing f x] evaluates [f ()] and if it fails on an empty + immediately evaluates to [return missing]. + + @since 2.4.0 + *) + val with_empty : missing:'r -> (unit -> 'r knowledge) -> 'r knowledge + + (** state with no knowledge *) val empty : state @@ -333,10 +374,62 @@ module Knowledge : sig include Monad.Syntax.S with type 'a t := 'a t - (** [x-->p] is [collect p x] *) + (** the monadic let-binding operators. + + Brings [let*] for [bind] and [let+] for [map] to the scope + of the [Syntax] module. + + @since 2.4.0 (before that an explicit [open Knowledge.Let] was + required. *) + include Monad.Syntax.Let.S with type 'a t := 'a t + + + (** [let*? v = x in f] evaluates to [f y] if [v] is [Some r]. + + Otherwise evaluates to [return None]. + + This let-binding operator is synonumous to [>>=?] + + @since 2.4.0 + *) + val (let*?) : 'a option t -> ('a -> 'b option t) -> 'b option t + + (** [let+? v = x in f] evaluates to [!!(f y)] if [v] is [Some r]. + + Otherwise evaluates to [return None]. + + This let-binding operator is synonumous to [>>|?] + + @since 2.4.0 + *) + val (let+?) : 'a option t -> ('a -> 'b option) -> 'b option t + + (** [x-->p] is [collect p x]. + + Example, + {[ + let* addr = label-->address in + ... + ]} + *) val (-->) : 'a obj -> ('a,'p) slot -> 'p t + (** [x-->?p] returns property [p] if it is not empty. + + Otherwise, if [x-->p] evaluates to empty or to [None] + fails with the empty value conflict. + + Example, + {[ + let* addr = label-->?address in + ... + ]} + + See also {!with_empty}. *) + val (-->?) : 'a obj -> ('a, 'p option) slot -> 'p t + + (** [p <-- f] is [promise p f] *) val (<--) : ('a,'p) slot -> ('a obj -> 'p t) -> unit @@ -351,6 +444,42 @@ module Knowledge : sig (** [x >>|? f] evaluates to [f y] if [x] evaluates to [Some y]. *) val (>>|?) : 'a option t -> ('a -> 'b option) -> 'b option t + + + (** [x.$[p]] is the propery [p] of [x]. + + @since 2.4.0 + *) + val (.$[]) : ('a,_) cls value -> ('a,'p) slot -> 'p + + + (** [x.$[p] <- r] updates the property [p] of [x] to [r]. + + Returns the value [x] with the new property. The previous + value is ignored so there is no merging or monotonicity check + involved. + + @since 2.4.0 *) + val (.$[]<-) : ('a,'b) cls value -> ('a,'p) slot -> 'p -> ('a,'b) cls value + + + (** [x.?[p]] returns the non-[None] property [p] or fails. + + The result is [return r] when [x.$[p]] is [Some r] or a + knowledge base conflict otherwise. + + @since 2.4.0 + *) + val (.?[]) : ('a,_) cls value -> ('a,'p option) slot -> 'p knowledge + + (** [x.![p]] returns the property [p] or fails if it is empty. + + The result is [return r] if not [Domain.is_empty dom r], + where [dom] is [Slot.domain p]. + + @since 2.4.0 + *) + val (.![]) : ('a,_) cls value -> ('a,'p) slot -> 'p knowledge end @@ -1388,7 +1517,6 @@ module Knowledge : sig module Conflict : sig type t = conflict = .. - (** [to_string err] is the textual representation of the conflict [err] @since 2.2.0 *) diff --git a/plugins/bil/bil_lifter.ml b/plugins/bil/bil_lifter.ml index 9a8228a05..e351ec877 100644 --- a/plugins/bil/bil_lifter.ml +++ b/plugins/bil/bil_lifter.ml @@ -289,21 +289,17 @@ let provide_bil ~enable_intrinsics () = require Disasm_expert.Basic.Insn.slot |> provide Bil.code |> comment "uses legacy lifters to provide BIL code."); - let unknown = KB.Domain.empty Bil.domain in - let (>>?) x f = x >>= function - | None -> KB.return unknown - | Some x -> f x in let enable_intrinsics = split_specs enable_intrinsics in KB.promise Bil.code @@ fun obj -> - Knowledge.collect Arch.slot obj >>= fun arch -> - Theory.Label.target obj >>= fun target -> - Knowledge.collect Memory.slot obj >>? fun mem -> - Knowledge.collect Disasm_expert.Basic.Insn.slot obj >>? fun insn -> + let* arch = KB.require Arch.slot obj in + let* target = Theory.Label.target obj in + let* mem = obj-->?Memory.slot in + let* insn = obj-->?Disasm_expert.Basic.Insn.slot in match lift ~enable_intrinsics target arch mem insn with | Error err -> info "BIL: the BIL lifter failed with %a" Error.pp err; - !!unknown - | Ok [] -> !!unknown + KB.return [] + | Ok [] -> KB.return [] | Ok bil -> Optimizer.run Bil.Theory.parser bil >>= fun sema -> let bil = Insn.bil sema in diff --git a/plugins/primus_lisp/primus_lisp_main.ml b/plugins/primus_lisp/primus_lisp_main.ml index 4ae7b3aaf..37cf92eb5 100644 --- a/plugins/primus_lisp/primus_lisp_main.ml +++ b/plugins/primus_lisp/primus_lisp_main.ml @@ -292,7 +292,7 @@ module Semantics = struct comment "translates instruction operands to lisp arguments" end); KB.promise Lisp.Semantics.args @@ fun this -> - KB.collect Insn.slot this >>=? fun insn -> + let*? insn = KB.collect Insn.slot this in Theory.current >>= fun theory -> Theory.Label.target this >>= fun target -> args_of_ops theory target insn >>| Option.some @@ -306,8 +306,8 @@ module Semantics = struct end); KB.promise Lisp.Semantics.name @@ fun this -> KB.collect Insn.slot this >>|? fun insn -> - let name = KB.Name.create ~package:(Insn.encoding insn) (Insn.name insn) in - Some name + KB.Name.create ~package:(Insn.encoding insn) (Insn.name insn) |> + Option.some let strip_lisp_extension = String.chop_suffix ~suffix:".lisp" diff --git a/plugins/radare2/radare2_main.ml b/plugins/radare2/radare2_main.ml index ac53310e7..1d8b8509a 100644 --- a/plugins/radare2/radare2_main.ml +++ b/plugins/radare2/radare2_main.ml @@ -20,12 +20,13 @@ let provide_roots file funcs = if Theory.Target.belongs Arm_target.parent t then !!None else - KB.collect Theory.Label.addr label >>=? fun addr -> - KB.collect Theory.Label.unit label >>=? fun unit -> - KB.collect Theory.Unit.bias unit >>= fun bias -> - KB.collect Theory.Unit.target unit >>| - Theory.Target.code_addr_size >>= fun bits -> - KB.collect Theory.Unit.path unit >>|? fun path -> + let*? addr = label-->Theory.Label.addr in + let*? unit = label--> Theory.Label.unit in + let*? path = unit-->Theory.Unit.path in + let* bias = unit-->Theory.Unit.bias in + let+ bits = + KB.collect Theory.Unit.target unit >>| + Theory.Target.code_addr_size in if String.equal path file then let bias = Option.value bias ~default:Bitvec.zero in let addr = diff --git a/plugins/x86/x86_legacy_bil_lifter.ml b/plugins/x86/x86_legacy_bil_lifter.ml index a8d28b1b7..371145dad 100644 --- a/plugins/x86/x86_legacy_bil_lifter.ml +++ b/plugins/x86/x86_legacy_bil_lifter.ml @@ -361,18 +361,14 @@ module Bap_integration = struct let prog = fixrip next prog in Parser.run grammar prog - let (>>?) x f = x >>= function - | None -> KB.return empty - | Some x -> f x - let provide_lifter () = info "providing a lifter for all Legacy AST lifters"; let lifter obj = Knowledge.collect Arch.slot obj >>= fun arch -> Theory.instance ~context:["floating-point"] () >>= Theory.require >>= fun theory -> - Knowledge.collect Memory.slot obj >>? fun mem -> - Knowledge.collect Disasm_expert.Basic.Insn.slot obj >>? fun insn -> + let* mem = obj-->?Memory.slot in + let* insn = obj-->?Disasm_expert.Basic.Insn.slot in match arch with | `x86 | `x86_64 as arch -> KB.catch (lift theory arch mem insn)