diff --git a/lib/bap_byteweight/bap_byteweight.mli b/lib/bap_byteweight/bap_byteweight.mli index 14416336c..a704072ba 100644 --- a/lib/bap_byteweight/bap_byteweight.mli +++ b/lib/bap_byteweight/bap_byteweight.mli @@ -1,6 +1,6 @@ (** Byteweight library. - Byteweight is a function start identification mechanism [[1]]. This + Byteweight is a function start identification algorithm [[1]]. This library provides a functorized implementation. An auxiliary {!Bap_byteweight_signatures} library provides an @@ -13,7 +13,6 @@ 23rd USENIX Security Symposium (USENIX Security 14). 2014. v} *) - open Bap.Std diff --git a/lib/bap_core_theory/bap_core_theory.ml b/lib/bap_core_theory/bap_core_theory.ml index 78bac1f9b..14d26d744 100644 --- a/lib/bap_core_theory/bap_core_theory.ml +++ b/lib/bap_core_theory/bap_core_theory.ml @@ -53,6 +53,7 @@ module Theory = struct module type Trans = Bap_core_theory_definition.Trans module type Core = Bap_core_theory_definition.Core + type core = (module Core) module Basic = struct module Empty : Basic = Bap_core_theory_empty.Core module Make = Bap_core_theory_basic.Make diff --git a/lib/bap_core_theory/bap_core_theory.mli b/lib/bap_core_theory/bap_core_theory.mli index ded158b6d..336dc8ebe 100644 --- a/lib/bap_core_theory/bap_core_theory.mli +++ b/lib/bap_core_theory/bap_core_theory.mli @@ -264,21 +264,21 @@ ["constant-tracker"] analysis: {[ - let () = Theory.declare "my-constant-tracker" (module struct - include (val Theory.require "constant-tracker") - - (* probably a bad example, but we all do this :) *) - let add x y = - printf "add is called!\n%!"; - add x y + let () = + Theory.declare "my-constant-tracker" + Theory.instance ~require:["bap.std:constant-tracker"] >>= + Theory.require >>| + fun (module Base) : Theory.core -> (module struct + include Base + let add x y = + printf "add is called!\n%!"; + add x y end ]} - The real analysis should store it results either in the knowledge base or directly in denotations of the terms (or in both places). - {2 Instantiating a theory} To use a theory we need to instantiate it. In the previous section @@ -310,15 +310,18 @@ specified context. For example, {[ - module Theory = (val Theory.instance () - ~context:["arm"; "arm-gnueabi"] - ~requires:[ - "variable-recovery"; - "stack-frame-analysis"; - "structural-analysis"; - "floating-point"; - "bap.std:bil-semantics"; - ]) + + Theory.instance () + ~context:["arm"; "arm-gnueabi"] + ~requires:[ + "variable-recovery"; + "stack-frame-analysis"; + "structural-analysis"; + "floating-point"; + "bap.std:bil-semantics" + ] >>= + Theory.require >>= fun (module Theory) -> + ]} In the example above, theories that are specific to ARM @@ -329,9 +332,11 @@ explicitly, the [bap.std:bil-semantics], to ensure that each term has a BIL denotation. - [1]: http://okmij.org/ftp/tagless-final/JFP.pdf - [2]: http://www.cs.utexas.edu/~wcook/Drafts/2012/ecoop2012.pdf - [3]: http://okmij.org/ftp/tagless-final/course/optimizations.html + References: + + - [1]: http://okmij.org/ftp/tagless-final/JFP.pdf + - [2]: http://www.cs.utexas.edu/~wcook/Drafts/2012/ecoop2012.pdf + - [3]: http://okmij.org/ftp/tagless-final/course/optimizations.html {2 Parsing binary code} @@ -1997,6 +2002,10 @@ module Theory : sig end + (** a type abbreviation for the core theory module type. *) + type core = (module Core) + + (** The Basic Theory. Implements the empty basic theory and provides a module for @@ -2049,7 +2058,9 @@ module Theory : sig ?context:string list -> ?provides:string list -> ?package:string -> - name:string -> (module Core) -> unit + name:string -> + (module Core) knowledge -> + unit (** [instance ()] creates an instance of the Core Theory. diff --git a/lib/bap_core_theory/bap_core_theory_manager.ml b/lib/bap_core_theory/bap_core_theory_manager.ml index 0b36486b6..04c2b8bf1 100644 --- a/lib/bap_core_theory/bap_core_theory_manager.ml +++ b/lib/bap_core_theory/bap_core_theory_manager.ml @@ -21,7 +21,7 @@ type 'a theory = { } type core = (module Core) -let known_theories : (Name.t, core theory) Hashtbl.t = +let known_theories : (Name.t, core knowledge theory) Hashtbl.t = Hashtbl.create (module Name) let features = Set.of_list (module String) @@ -312,7 +312,6 @@ let slot = Knowledge.Class.property theory "instance" domain ~desc:"The theory structure" - let str_ctxt () ctxt = List.to_string (Set.to_list ctxt) ~f:ident @@ -321,11 +320,10 @@ module Theory = (val Knowledge.Object.derive theory) let theories () = let init = Map.empty (module Theory) in Hashtbl.to_alist known_theories |> - Knowledge.List.fold ~init ~f:(fun theories (name,structure) -> + Knowledge.List.fold ~init ~f:(fun theories (name,def) -> Knowledge.Symbol.intern (Name.unqualified name) theory ~package:(Name.package name) >>| fun name -> - Map.add_exn theories name structure) - + Map.add_exn theories name def) let is_applicable ~provided ~requires = Set.for_all requires ~f:(Set.mem provided) @@ -350,44 +348,75 @@ let refine ?(context=[]) ?requires theories = is_applicable ~provided ~requires && is_required ~required ~provides) -let new_theory ?context ?requires () = - theories () >>| Map.data >>| refine ?context ?requires >>= function - | [] -> Knowledge.return Empty.theory - | [t] -> Knowledge.return t - | theories -> - Knowledge.return @@ - (List.reduce_balanced_exn theories ~f:merge) - let theory_for_id id = let sym = sprintf "'%s" @@ List.to_string (Set.to_list id) ~f:Name.show in Knowledge.Symbol.intern sym theory ~package:"core-theory-internal" +let is_instantiated id = + Knowledge.collect slot id >>| fun t -> + not t.is_empty + + +(* On instantiation of recursive modules. + + We employ the same techinique as OCaml does [1]. + When a module is instantiated we create an instance + of this module with an empty structure, so that if + a module creates an instance of itself during instantiation, + it will not enter an infinite recursion but will get the + empty denotation. Our merge operator, which will be called, + by the provide operator after the final instance is created, + will notice that the initial structure is ordered strictly + before the new one (because we used the Empty.name for it), + thus it will drop it from the final structure. + + [1]: Leroy, Xavier."A proposal for recursive modules in Objective + Caml." Available from the author’s website (2003). +*) +let instantiate t = + theory_for_id t.id >>= fun id -> + is_instantiated id >>= function + | true -> Knowledge.return id + | false -> + Knowledge.provide slot id { + Empty.theory with is_empty = false + } >>= fun () -> + t.structure >>= fun structure -> + Knowledge.provide slot id {t with structure} >>| fun () -> + id + let instance ?context ?requires () = theories () >>| Map.data >>| refine ?context ?requires >>= function | [] -> theory_for_id Empty.theory.id - | [t] -> theory_for_id t.id + | [t] -> + instantiate t | theories -> List.fold theories ~init:(Set.empty (module Name)) ~f:(fun names t -> Set.union names t.id) |> theory_for_id >>= fun id -> - let theory = List.reduce_balanced_exn theories ~f:merge in - Knowledge.provide slot id theory >>| fun () -> - id + is_instantiated id >>= function + | true -> Knowledge.return id + | false -> + Knowledge.List.map theories + ~f:(instantiate >=> Knowledge.collect slot) >>| + List.reduce_balanced_exn ~f:merge >>= + Knowledge.provide slot id >>| fun () -> + id let require name = let open Knowledge.Syntax in theories () >>= fun theories -> match Map.find theories name with - | Some t -> Knowledge.return t.structure + | Some t -> t.structure | None -> Knowledge.collect slot name >>| fun t -> t.structure module Documentation = struct module Theory = struct - type t = Name.t * core theory + type t = Name.t * core knowledge theory let (-) xs name = Set.remove xs (Name.show name) diff --git a/lib/bap_core_theory/bap_core_theory_manager.mli b/lib/bap_core_theory/bap_core_theory_manager.mli index 0821736fe..55330ea78 100644 --- a/lib/bap_core_theory/bap_core_theory_manager.mli +++ b/lib/bap_core_theory/bap_core_theory_manager.mli @@ -7,7 +7,9 @@ val declare : ?context:string list -> ?provides:string list -> ?package:string -> - name:string -> (module Core) -> unit + name:string -> + (module Core) knowledge -> + unit val instance : ?context:string list -> diff --git a/lib/bap_primus_machine/bap_primus_machine.mli b/lib/bap_primus_machine/bap_primus_machine.mli index 364c3064e..d22a40e1a 100644 --- a/lib/bap_primus_machine/bap_primus_machine.mli +++ b/lib/bap_primus_machine/bap_primus_machine.mli @@ -1,82 +1,85 @@ -open Core_kernel -open Monads.Std -open Bap_knowledge +(* Not yet released. -(** Primus - A non-deterministic interpreter. + open Core_kernel + open Monads.Std + open Bap_knowledge -*) + (** Primus - A non-deterministic interpreter. + + + *) -module Primus : sig - open Knowledge - type 'a machine + module Primus : sig + open Knowledge + type 'a machine - (** The Machine Exception. + (** The Machine Exception. The exn type is an extensible variant, and components usually register their own error constructors. *) - type exn = .. + type exn = .. - (** [an observation] of a value of type [a].*) - type 'a observation + (** [an observation] of a value of type [a].*) + type 'a observation - type observed + type observed - (** Machine exit status. + (** Machine exit status. A machine may terminate normally, or abnormally with the specified exception. *) - type exit_status = + type exit_status = | Normal | Exn of exn - (** the machine computation *) - type 'a t = 'a machine + (** the machine computation *) + type 'a t = 'a machine - type 'a state + type 'a state - type project + type project - (** Machine identifier type. *) - type id = Monad.State.Multi.id + (** Machine identifier type. *) + type id = Monad.State.Multi.id - (** [raise exn] raises the machine exception [exn], intiating + (** [raise exn] raises the machine exception [exn], intiating an abonormal control flow *) - val raise : exn -> 'a t + val raise : exn -> 'a t - (** [catch x f] creates a computation that is equal to [x] if + (** [catch x f] creates a computation that is equal to [x] if it terminates normally, and to [f e] if [x] terminates abnormally with the exception [e]. *) - val catch : 'a t -> (exn -> 'a t) -> 'a t + val catch : 'a t -> (exn -> 'a t) -> 'a t - val collect : ('a,'p) slot -> 'a obj -> 'p t - val provide : ('a,'p) slot -> 'a obj -> 'p -> unit t - val project : project obj t + val collect : ('a,'p) slot -> 'a obj -> 'p t + val provide : ('a,'p) slot -> 'a obj -> 'p -> unit t + val project : project obj t - val die : id -> unit t + val die : id -> unit t - val conflict : conflict -> 'a t + val conflict : conflict -> 'a t - (** [fact x] make the fact [x] determined in the current machine. + (** [fact x] make the fact [x] determined in the current machine. This is the [pure] function w.r.t. to the non-determinism, also known as lift, since it lifts the inner knowledge monad into the outer machine monad. *) - val fact : 'a knowledge -> 'a t + val fact : 'a knowledge -> 'a t - (** [run comp project] runs the Primus system. *) - val run : unit t -> project obj -> unit knowledge + (** [run comp project] runs the Primus system. *) + val run : unit t -> project obj -> unit knowledge - (** Computation State *) - module State : sig + (** Computation State *) + module State : sig (** ['a t] is a type of state that holds a value of type ['a], and can be constructed from the base context of type ['c]. *) @@ -102,15 +105,15 @@ module Primus : sig (** [name state] a state name that was given during the construction. *) val name : 'a t -> string - end + end - (** An interface to the state. + (** An interface to the state. An interface gives an access to operations that query and modify machine state. *) - module type State = sig + module type State = sig (** [get state] extracts the state. *) val get : 'a state -> 'a machine @@ -119,9 +122,9 @@ module Primus : sig (** [update state ~f] updates a state using function [f]. *) val update : 'a state -> f:('a -> 'a) -> unit machine - end + end - (** Observations interface. + (** Observations interface. An observation is a named event, that can occur during the program execution. Observations could be provided (usually @@ -153,78 +156,79 @@ module Primus : sig which is being notified. Here is an example, using our [sum] observation: - {[ - Observation.make sum ~f:(fun observe -> - observe 1 2 3) - ]} + {[ + Observation.make sum ~f:(fun observe -> + observe 1 2 3) +]} - {3 Monitoring Observations} + {3 Monitoring Observations} - It is possible to register a function, which will be called - every time an observation is made via the [provide] function. - The monitor has a little bit more complicated type, as beyond - the actual payload (arguments of the observation), it takes a - [ctrl] instance, which should be used to return from the - observation, via [Observation.continue] or [Observation.stop] - functions. + It is possible to register a function, which will be called + every time an observation is made via the [provide] function. + The monitor has a little bit more complicated type, as beyond + the actual payload (arguments of the observation), it takes a + [ctrl] instance, which should be used to return from the + observation, via [Observation.continue] or [Observation.stop] + functions. - *) - module Observation : sig - type 'f t = 'f observation - type info = Info.t - type ctrl + *) + module Observation : sig + type 'f t = 'f observation + type info = Info.t + type ctrl - val declare : - ?inspect:((info -> observed machine) -> 'f) -> - ?package:string -> string -> - 'f observation + val declare : + ?inspect:((info -> observed machine) -> 'f) -> + ?package:string -> string -> + 'f observation - (** [provide obs f] provides the observation of [obs]. + (** [provide obs f] provides the observation of [obs]. - The function [f] takes one argument a function, - which accepts + The function [f] takes one argument a function, + which accepts - *) - val provide : 'f observation -> f:('f -> observed machine) -> unit machine - val monitor : 'f observation -> f:(ctrl -> 'f) -> unit machine - val inspect : 'f observation -> f:(info -> observed machine) -> unit machine + *) + val provide : 'f observation -> f:('f -> observed machine) -> unit machine + val monitor : 'f observation -> f:(ctrl -> 'f) -> unit machine + val inspect : 'f observation -> f:(info -> observed machine) -> unit machine - val continue : ctrl -> observed machine - val stop : ctrl -> observed machine - end + val continue : ctrl -> observed machine + val stop : ctrl -> observed machine + end - (** [exn_raised exn] occurs every time an abnormal control flow - is initiated *) - val exn_raised : (exn -> observed machine) observation + (** [exn_raised exn] occurs every time an abnormal control flow + is initiated *) + val exn_raised : (exn -> observed machine) observation - (** Computation Syntax.*) - module Syntax : sig - include Monad.Syntax.S with type 'a t := 'a t + (** Computation Syntax.*) + module Syntax : sig + include Monad.Syntax.S with type 'a t := 'a t - (** [x-->p] is [collect p x] *) - val (-->) : 'a obj -> ('a,'p) slot -> 'p t + (** [x-->p] is [collect p x] *) + val (-->) : 'a obj -> ('a,'p) slot -> 'p t - (** [c // s] is [Object.read c s] *) - val (//) : ('a,_) cls -> string -> 'a obj t + (** [c // s] is [Object.read c s] *) + val (//) : ('a,_) cls -> string -> 'a obj t - (** [event >>> action] is the same as - [Observation.monitor event action] *) - val (>>>) : 'f observation -> (Observation.ctrl -> 'f) -> unit t - end + (** [event >>> action] is the same as + [Observation.monitor event action] *) + val (>>>) : 'f observation -> (Observation.ctrl -> 'f) -> unit t + end - include Monad.State.Multi.S with type 'a t := 'a t - and type id := id - and module Syntax := Syntax + include Monad.State.Multi.S with type 'a t := 'a t + and type id := id + and module Syntax := Syntax - (** Local state of the machine. *) - module Local : State + (** Local state of the machine. *) + module Local : State - (** Global state shared across all machine clones. *) - module Global : State -end + (** Global state shared across all machine clones. *) + module Global : State + end +*) diff --git a/lib/graphlib/graphlib.mli b/lib/graphlib/graphlib.mli index 19bba03a4..7e2b1f0b9 100644 --- a/lib/graphlib/graphlib.mli +++ b/lib/graphlib/graphlib.mli @@ -2,66 +2,64 @@ open Core_kernel open Regular.Std (** - {3 Graph library} - - {!Graphlib} is a generic library that extends a well known - OCamlGraph library. {!Graphlib} uses its own, more reach, - {!Graph} interface that is isomorphic to OCamlGraph's [Sigs.P] - signature for persistent graphs. Two functors witness the - isomorphism of the interfaces: - {!Graphlib.To_ocamlgraph} and {!Graphlib.Of_ocamlgraph}. Thanks - to these functors, any algorithm written for OCamlGraph can be - used on [Graphlibs] graph and vice verse. - - The {!Graph} interface provides a richer interface in a Core - style. Nodes and Edges implements {!Opaque} data structure, - i.e., they come with Maps, Sets, Hashtbls, etc, preloaded (e.g., - [G.Node.Set] is a set of node for graph implementation, provided - by a module named [G]). Graphs also implement {!Printable} - interface, that makes them much easier to debug. - - Along with graphs, auxiliary data structures are provided, like - {{!Path}path} to represent paths in graph, {{!Tree}tree} for - representing different graph spannings, {{!Partition}partition} - for graph partitioning, and more. - - {!Graphlib} is a library that provides a set of generic - algorithms, as well as implementations of a {!Graph} interface, - and a suite of preinstantiated graphs. - - Contrary to OCamlGraph, each {!Graphlib} interface is provided - as a function, not a functor. Thus making there use syntactically - easier. Also, {!Graphlib} heavily uses optional and keyword - parameters. For die-hards, many algorithms still have functor - a interface. - - All {!Graphlib} algorithms accept a first-class module with - graph implementation as a first argument. You can think of this - parameter as an explicit type class. Later, when modular - implicits will be accepted in OCaml, this parameter can be - omitted. But for now, we need to pass them. - - A recommended way to work with {!Graphlib} is to bind the - chosen implementation with some short name, usually [G] would be - a good choice: + {3 Graph library} + + {!Graphlib} is a generic library that extends a well known + OCamlGraph library. {!Graphlib} uses its own and richer + {!Graph} interface that is isomorphic to OCamlGraph's [Sigs.P] + signature for persistent graphs. Two functors witnesses + isomorphism of the interfaces: + {!Graphlib.To_ocamlgraph} and {!Graphlib.Of_ocamlgraph}. Thanks + to these functors, any algorithm written for OCamlGraph can be + used on [Graphlibs] graph and vice verse. + + The {!Graph} interface provides a richer interface in a Core + style. Nodes and Edges implements the {!Opaque} interface, + i.e., they come with Maps, Sets, Hashtbls, etc, (e.g., + [G.Node.Set] is a set of node for graph implementation, provided + by a module named [G]). Graphs also implement {!Printable} + interface, that makes them much easier to debug. + + Along with graphs, auxiliary data structures are provided, like + {{!Path}path} to represent paths in graph, {{!Tree}tree} for + representing different graph spannings, {{!Partition}partition} + for graph partitioning, and more. + + The {!Graphlib} module provides a set of generic graph + algorithms. Contrary to OCamlGraph, each {!Graphlib} interface + is provided using functions rather than functors. Which makes + the interface easier to use, at least in simple cases. Also, + {!Graphlib} heavily uses optional and keyword parameters. For + die-hards, many algorithms still have a functor interface. + + All {!Graphlib} algorithms accept a first-class module with + graph implementation as a first argument. You can think of this + parameter as an explicit type class. + + + A recommended way to work with {!Graphlib} is to bind the + chosen implementation to some short name, usually [G] would be + a good choice: {[module G = Graphlib.Make(String)(Bool)]} - This will bind name [G] with a graph implementation that has - [string] nodes, with edges labeled by values of type [bool]. + This will bind [G] to a graph implementation that has + [string] nodes with edges labeled by values of type [bool]. - To create a graph of type [G.t] one can use a generic - {!Graphlib.create} function: + Graphs of type [G.t] could be created using the generic + {!Graphlib.create} function: - {[let g = Graphlib.create (module G) ~edges:[ - "entry", "loop", true; - "loop", "exit", true; - "loop", "loop", false; - ] ()]} + {[ + let g = Graphlib.create (module G) ~edges:[ + "entry", "loop", true; + "loop", "exit", true; + "loop", "loop", false; + ] () + ]} - This will create an instance of type [G.t]. Of course, it is - still possible to use non-generic [G.empty], [G.Node.insert], - [G.Edge.insert]. + This will create an instance of type [G.t]. Of course, it is + still possible to use non-generic [G.empty], [G.Node.insert], + [G.Edge.insert]. *) module Std : sig (** {!Graph} nodes. *) @@ -981,23 +979,6 @@ module Std : sig unique. - {b Lemma}: Everything dominates unreachable block. - - {b Proof}: (by contradiction) suppose there exists a node [u] that - doesn't dominate unreachable block [v]. That means, that there - exists a path from [entry] to [v] that doesn't contain - [u]. But that means, at least, that [v] is reachable. This is - a contradiction with the original statement that [v] is - unreachable. {b Qed.} - - If some nodes of graph [g] are unreachable from the provided - [entry] node, then they are dominated by all other nodes of a - graph. It means that the provided system is under constrained - and has more then one solution (i.e., there exists more than - one tree, that satisfies properties (1) - (5). In a current - implementation each unreachable node is immediately dominated - by the [entry], if the [entry] is in graph. - To get a post-dominator tree, reverse the graph by passing [true] to [rev] and pass exit node as a starting node. @@ -1005,7 +986,11 @@ module Std : sig good idea to have an entry node, that doesn't have any predecessors. Usually, this is what is silently assumed in many program analysis textbooks, but is not true in general - for control-flow graphs that are reconstructed from binaries *) + for control-flow graphs that are reconstructed from binaries. + + Note: all nodes that are not reachable from the specified + [entry] node are parented by the [entry] node. + *) val dominators : (module Graph with type t = 'c and type node = 'n @@ -1169,22 +1154,21 @@ module Std : sig approximation [init] (obtained either with [Solution.create] or from the previous calls to [fixpoint]). - The general representation of the fixpoint equations is + The general representation of the fixpoint equation is {v - x(i) = f(i) (a(i,1) x(1) % ... % a(i,j) x(j)), + x(i) = f(i) (a(1,i) x(1) % ... % a(n,i) x(n)), v} where - [x(i)] is the value of the [i]'th variable (node); - - [a(i,j)] is [1] if there is an edge from the node - [i] to the node [j] and [0] otherwise; + - [a(s,d)] is [1] if there is an edge from the node + [s] to the node [d] and [0] otherwise; - [%] the merge operator; - - [f(i)] is the transfer function for the node [i]; - - [=] is the equivalence operation. + - [f(i)] is the transfer function for the node [i]. A solution is obtained through a series of iterations until - the fixpoint is reached, i.e., until the system + the fixed point is reached, i.e., until the system stabilizes. The total number of iterations could be bound by an arbitrary number. If the maximum number of iterations is reached before the system stabilizes then the solution is not @@ -1229,37 +1213,24 @@ module Std : sig {4 Introduction} The data domain is a set of values equipped with a partial - ordering operation [(L,<=)], also know as a lattice or a - poset. We assume, that the lattice is complete, i.e., there - are two special elements of a set that are called [top] and + ordering operation [(L,<=)], also know as a poset. We assume, + that the poset is bounded complete, i.e., there + are two special elements of the set that are called [top] and [bot] (the bottom value). The top element is the greatest - element of the set L, i.e., for all [x] in [L], [x <= - top]. Correspondingly, the bottom element is the least element + element of the set L, i.e., for all [x] in [L], [x <= top]. + Correspondingly, the bottom element is the least element of the set [L], i.e., for all [x] in [L], [bot <= x]. It is not - required by the framework that the lattice has both or any of - them, however their presence makes the explanation easier, and - since any lattice could be artificially extended with these + required by the framework that the poset has both or any of + the bounds, however their presence makes the explanation easier, and + since any poset could be artificially extended with these two elements, their introduction will not introduce a loss of - generality. Since values of the lattice [L] represent + generality. Since values of the set [L] represent information, the partial ordering between two pieces of information [a] and [b], e.g., [a <= b], tells us that [a] contains no more information than [b]. Therefore the [top] value contains all the information, representable in the - lattice, correspondingly the [bot] value represents an absence - of information. Thus, we will consider the bottom value as an - over approximation (or a lower approximation in terms of the - lattice ordering relation), as an absence of information - cannot contain false statements (vacuous truth). Assuming, - that there is some value [t], [bot <= t <= top] that represents - a ground truth (that is usually unobtainable), we say that all - values that are less than or equal [t] are over-approximations - of the truth, and the rest of the values, are - under-approximations. Under-approximations under estimate a - behavior of a system, and usually represent information about - a system that is not true, hence an under approximate solution, - is usually unsafe to use. In general, our task is to find an - over approximation that is as close as possible to the ground - truth [t]. + set, correspondingly the [bot] value represents an absence + of information. A solution to a fixed point equation (i.e., an equation of the form [x = f(x)]) could be obtainted by starting from some @@ -1268,7 +1239,7 @@ module Std : sig In general, a function may have multiple (or no at all) fixed points. If a function has several fixed points, then we can distinguish two extremums - the least fixed point [lfp] and - the greatest fixed point [gfp] w.r.t the ordering of lattice + the greatest fixed point [gfp] w.r.t the ordering of the poset [L]. Assuming that function [f] is positive monotonic function (i.e., [x <= y] implies that [f(x) <= f(y)]), thechoice of the initial value [x0] denotes which of the two fixed points is @@ -1284,20 +1255,20 @@ module Std : sig ground truth (i.e., we are monotonically aggregating facts). In general, a function may not have a solution at all, or the - solution may not be computable in practice, i.e., when the chain - of function applications [x = f(... f(x0) ...)] is either - infinite or effectively infinite (e.g., 2^64 applications). The - Tarksi theorem states that if [L] is complete and [f] is - monotone, then it has a fixed point. If a lattice has a - limited height (maximum length of chain of elements, such that - x0 < x1 < .. < xM) then we will obtain a solution in no more - than [M] steps. However, if [M] is very big, or infinite, then - the solution won't be find in general, and the computation may - not terminate. + solution may not be computable in practice, i.e., when the + chain of function applications [x = f(... f(x0) ...)] is + either infinite or effectively infinite (e.g., 2^64 + applications). The Tarksi theorem states that if [L] is + complete and [f] is monotone, then it has a fixed point. If a + poset has a limited height (maximum length of an ascending + chain of elements, such that x0 < x1 < .. < xM) then we will + obtain a solution in no more than [M] steps. However, if [M] + is very big, or infinite, then the solution won't be find in + general, and the computation may not terminate. This brings us to the main distinction between Abstract Interpretation and Data Flow Analysis. The latter usually - deals with lattice that have finite heights, while the former + deals with lattices that have finite heights, while the former deals with very big and infinite lattices. To accelerate the convergence of a chain of approximations, a special technique called [widening] is used. Widening can be seen as an diff --git a/oasis/common b/oasis/common index ebed90b00..e0a3a23fe 100644 --- a/oasis/common +++ b/oasis/common @@ -1,6 +1,6 @@ OASISFormat: 0.4 Name: bap -Version: 2.0.0-alpha +Version: 2.0.0 OCamlVersion: >= 4.04.1 Synopsis: BAP Core Library Authors: BAP Team diff --git a/plugins/bil/bil_ir.ml b/plugins/bil/bil_ir.ml index c42139ed5..6555272f5 100644 --- a/plugins/bil/bil_ir.ml +++ b/plugins/bil/bil_ir.ml @@ -309,7 +309,7 @@ let reify = function | None -> [] | Some g -> BIR.reify g -let init () = Theory.declare (module IR) +let init () = Theory.declare !!(module IR : Theory.Core) ~package:"bap.std" ~name:"bir" ~desc:"Builds the graphical representation of a program." ~provides:[ diff --git a/plugins/bil/bil_lifter.ml b/plugins/bil/bil_lifter.ml index 938ca48b0..33aaf014a 100644 --- a/plugins/bil/bil_lifter.ml +++ b/plugins/bil/bil_lifter.ml @@ -390,7 +390,7 @@ let provide_lifter ~with_fp () = let init ~with_fp () = provide_lifter ~with_fp (); provide_bir (); - Theory.declare (module Brancher) + Theory.declare !!(module Brancher : Theory.Core) ~package:"bap.std" ~name:"jump-dests" ~desc:"an approximation of jump destinations" ~provides:[ diff --git a/plugins/bil/bil_main.ml b/plugins/bil/bil_main.ml index 8fc1ad3d5..ce1c973c3 100644 --- a/plugins/bil/bil_main.ml +++ b/plugins/bil/bil_main.ml @@ -116,11 +116,13 @@ let () = Bil.select_passes (ctxt-->norml @ ctxt-->optim @ ctxt-->passes); Bil_lifter.init ~with_fp:(ctxt-->enable_fp_emu) (); Bil_ir.init(); - Theory.declare (module Bil_semantics.Core) + let open KB.Syntax in + Theory.declare !!(module Bil_semantics.Core : Theory.Core) ~package:"bap.std" ~name:"bil" ~desc:"semantics in BIL" ~provides:["bil"; "lifter"]; - Theory.declare (module Bil_semantics.Core_with_fp_emulation) + + Theory.declare !!(module Bil_semantics.Core_with_fp_emulation : Theory.Core) ~package:"bap.std" ~name:"bil-fp-emu" ~extends:["bap.std:bil"] ~desc: "semantics in BIL, including FP emulation"