diff --git a/OMakefile b/OMakefile index 6343d77fa..89c04a1ca 100644 --- a/OMakefile +++ b/OMakefile @@ -27,8 +27,8 @@ include _oasis_lib.om # At this point you may fine-tune the configuration, and modify defaults: # # OCAML_LIB_MODULE_SUFFIXES += .ml (install also .ml files with libs) -# OCAMLFINDFLAGS += -verbose (be verbose) -# OCAMLFLAGS += -bin-annot (create .cmt/.cmti files) +# OCAMLFINDFLAGS += -thread +OCAMLFLAGS += -bin-annot # (create .cmt/.cmti files) OCAMLFLAGS_ANNOT = -annot -bin-annot OCAMLFLAGS += $(OCAMLFLAGS_ANNOT) diff --git a/lib/bap/bap.mli b/lib/bap/bap.mli index 3d5e05e08..209495e88 100644 --- a/lib/bap/bap.mli +++ b/lib/bap/bap.mli @@ -680,7 +680,7 @@ module Std : sig (** Lazy sequence *) module Seq : module type of Seq - with type 'a t = 'a Sequence.t + with type 'a t = 'a Base.Sequence.t (** type abbreviation for ['a Sequence.t] *) type 'a seq = 'a Seq.t [@@deriving bin_io, compare, sexp] @@ -776,7 +776,7 @@ module Std : sig will create a printer for a [String.Trie] that is populated by integers. *) - val pp : 'a printer -> 'a t printer + val pp : (Format.formatter -> 'a -> unit) -> (Format.formatter -> 'a t -> unit) end end module V2 : sig @@ -1339,7 +1339,7 @@ module Std : sig Note, the [printf] function from examples refers to the [Format.printf], thus it is assumed that the [Format] module is open in the scope. *) - val pp : t printer + val pp : Format.formatter -> t -> unit (** [printf "%a" pp_hex x] prints [x] in the hexadecimal format omitting suffixes, and the prefix if it is not necessary. @@ -1353,7 +1353,7 @@ module Std : sig ]} @since 1.3 *) - val pp_hex : t printer + val pp_hex : Format.formatter -> t -> unit (** [printf "%a" pp_dec x] prints [x] in the decimal format omitting suffixes and prefixes. @@ -1367,7 +1367,7 @@ module Std : sig ]} @since 1.3 *) - val pp_dec : t printer + val pp_dec : Format.formatter -> t -> unit (** [printf "%a" pp_oct x] prints [x] in the octal format omitting suffixes, and the prefix if it is not necessary. @@ -1379,7 +1379,7 @@ module Std : sig # printf "%a\n" pp_oct (Word.of_int32 0x1);; 1 ]} *) - val pp_oct : t printer + val pp_oct : Format.formatter -> t -> unit (** [printf "%a" pp_bin x] prints [x] in the binary (0 and 1) format omitting suffixes, and the prefix if it is not necessary. @@ -1393,7 +1393,7 @@ module Std : sig ]} @since 1.3 *) - val pp_bin : t printer + val pp_bin : Format.formatter -> t -> unit (** [printf "%a" pp_hex x] prints [x] in the hexadecimal format omitting suffixes, and the prefix if it is not necessary. @@ -1405,7 +1405,7 @@ module Std : sig # printf "%a\n" pp_hex (Word.of_int32 0x1);; 1 ]} *) - val pp_hex : t printer + val pp_hex : Format.formatter -> t -> unit (** [printf "%a" pp_dec x] prints [x] in the decimal format omitting suffixes and prefixes. @@ -1419,7 +1419,7 @@ module Std : sig ]} @since 1.3 *) - val pp_dec : t printer + val pp_dec : Format.formatter -> t -> unit (** [printf "%a" pp_oct x] prints [x] in the octal format omitting suffixes, and the prefix if it is not necessary. @@ -1433,7 +1433,7 @@ module Std : sig ]} @since 1.3 *) - val pp_oct : t printer + val pp_oct : Format.formatter -> t -> unit (** [printf "%a" pp_bin x] prints [x] in the binary (0 and 1) format omitting suffixes, and the prefix if it is not necessary. @@ -1447,7 +1447,7 @@ module Std : sig ]} @since 1.3 *) - val pp_bin : t printer + val pp_bin : Format.formatter -> t -> unit (** [printf "%a" pp_hex_full x] prints [x] in the hexadecimal format with suffixes, and the prefix if it is necessary. @@ -1459,7 +1459,7 @@ module Std : sig # printf "%a\n" pp_hex_full (Word.of_int32 0x1);; 1:32u ]} *) - val pp_hex_full : t printer + val pp_hex_full : Format.formatter -> t -> unit (** [printf "%a" pp_dec_full x] prints [x] in the decimal format with suffixes and prefixes. @@ -1473,7 +1473,7 @@ module Std : sig ]} @since 1.3 *) - val pp_dec_full : t printer + val pp_dec_full : Format.formatter -> t -> unit (** [printf "%a" pp_oct_full x] prints [x] in the octal format with suffixes, and the prefix if it is necessary. @@ -1485,7 +1485,7 @@ module Std : sig # printf "%a\n" pp_oct_full (Word.of_int32 0x1);; 1:32u ]} *) - val pp_oct_full : t printer + val pp_oct_full : Format.formatter -> t -> unit (** [printf "%a" pp_bin_full x] prints [x] in the binary (0 and 1) format omitting suffixes, and the prefix if it is necessary. @@ -1497,7 +1497,7 @@ module Std : sig # printf "%a\n" pp_bin_full (Word.of_int32 0x1);; 1:32u v} *) - val pp_bin_full : t printer + val pp_bin_full : Format.formatter -> t -> unit (** [pp_generic ?case ?prefix ?suffix ?format ppf x] - a printer to suit all tastes. @@ -1534,7 +1534,7 @@ module Std : sig ?prefix:[`auto | `base | `none | `this of string ] -> ?suffix:[`none | `full | `size ] -> ?format:[`hex | `dec | `oct | `bin ] -> - t printer + Format.formatter -> t -> unit (** [string_of_value ?hex x] returns a textual representation of the [x] value, i.e., ignores size and signedness. If [hex] is @@ -1969,15 +1969,15 @@ module Std : sig val slot : (Theory.Program.Semantics.cls, stmt list) Knowledge.slot (** [printf "%a" pp_binop op] prints a binary operation [op]. *) - val pp_binop : binop printer + val pp_binop : Format.formatter -> binop -> unit (** [printf "%a" pp_unop op] prints an unary operation [op] *) - val pp_unop : unop printer + val pp_unop : Format.formatter -> unop -> unit (** [printf "%a" pp_cast t] prints a cast type [t] @since 1.3 *) - val pp_cast : cast printer + val pp_cast : Format.formatter -> cast -> unit (** [string_of_binop op] is a textual representation of [op]. @since 1.3 @@ -3614,7 +3614,7 @@ module Std : sig val eval : t -> Bil.value include Regular.S with type t := t - val pp_adt : t printer + val pp_adt : Format.formatter -> t -> unit end (** [Regular] interface for BIL statements *) @@ -3895,7 +3895,7 @@ module Std : sig include Regular.S with type t := t - val pp_adt : t printer + val pp_adt : Format.formatter -> t -> unit end (** Architecture *) @@ -4432,7 +4432,7 @@ module Std : sig (** [pp pp_elem] creates a vector printer that uses [pp_elem] to print elements. *) - val pp : 'a printer -> 'a t printer + val pp : (Format.formatter -> 'a -> unit) -> (Format.formatter -> 'a t -> unit) end (** BAP IR. @@ -5214,7 +5214,7 @@ module Std : sig val elements : ('a t -> 'a seq) ranged (** [pp printer] - creates a printer for table from value printer *) - val pp : 'a printer -> 'a t printer + val pp : (Format.formatter -> 'a -> unit) -> (Format.formatter -> 'a t -> unit) end (** A locations of a chunk of memory *) @@ -5687,7 +5687,7 @@ module Std : sig include Container.S1 with type 'a t := 'a t (** [pp pp_elem] constracts a printer for a memmap to the given element. *) - val pp : 'a printer -> 'a t printer + val pp : (Format.formatter -> 'a -> unit) -> (Format.formatter -> 'a t -> unit) end (** Symbolizer defines a method for assigning symbolic names to addresses *) @@ -6321,7 +6321,7 @@ module Std : sig (** [pp_adt] prints instruction in ADT format, suitable for reading by evaluating in many languages, e.g. Python, Js, etc *) - val pp_adt : t printer + val pp_adt : Format.formatter -> t -> unit (** {3 Prefix Tree} This module provides a trie data structure where a sequence of @@ -8206,10 +8206,10 @@ module Std : sig include S with type ('a,'e) state = ('a,'e) Monad.State.t (** print a set of taints *) - val pp_set : set printer + val pp_set : Format.formatter -> set -> unit (** print a taint map *) - val pp_map : map printer + val pp_map : Format.formatter -> map -> unit module Map : Regular.S with type t = map end [@@deprecated "[since 2018-03] use the Bap Taint Framework instead"] @@ -9052,7 +9052,7 @@ module Std : sig value for the ['a] type. *) type 'a converter - val converter : 'a parser -> 'a printer -> 'a -> 'a converter + val converter : 'a parser -> (Format.formatter -> 'a -> unit) -> 'a -> 'a converter (** Default deprecation warning message, for easy deprecation of parameters. *) diff --git a/lib/bap_c/bap_c_abi.ml b/lib/bap_c/bap_c_abi.ml index 6093ee035..5b5b70bd8 100644 --- a/lib/bap_c/bap_c_abi.ml +++ b/lib/bap_c/bap_c_abi.ml @@ -74,7 +74,7 @@ let data (size : #Bap_c_size.base) (t : Bap_c_type.t) = | None -> off', data t :: seq | Some pad -> off, data t :: Imm (pad,Set []) :: seq) in Seq (List.rev ss) - | `Union {Spec.t=fs} -> + | `Union {Spec.t=_} -> let sz = match size#bits t with | None -> Size.in_bits size#pointer | Some sz -> sz in @@ -93,101 +93,35 @@ let create_arg i addr_size intent name t (data,exp) sub = let arg = Term.set_attr arg Attrs.t t in arg - - -let find_by_name prog name = - Term.enum sub_t prog |> Seq.find ~f:(fun sub -> String.equal (Sub.name sub) name) - -let find_first_caller prog tid = - Term.enum sub_t prog |> Seq.find ~f:(fun sub -> - Term.enum blk_t sub |> Seq.exists ~f:(fun blk -> - Term.enum jmp_t blk |> Seq.exists ~f:(fun jmp -> - match Jmp.kind jmp with - | Call c -> Label.equal (Call.target c) (Direct tid) - | _ -> false))) - -let proj_int = function Bil.Int x -> Some x | _ -> None - -let is_sub_exists prog name = Option.is_some @@ find_by_name prog name -let is_sub_absent prog name = not (is_sub_exists prog name) - -let has_libc_runtime prog = - is_sub_exists prog "__libc_csu_fini" && - is_sub_exists prog "__libc_csu_init" - -let find_entry_point prog = - Term.enum sub_t prog |> - Seq.find ~f:(fun sub -> Term.has_attr sub Sub.entry_point) - - -let find_libc_start_main prog = - let open Monad.Option.Syntax in - find_entry_point prog >>= fun start -> - Term.first blk_t start >>= fun entry -> - Term.first jmp_t entry >>= fun jmp -> - match Jmp.kind jmp with - | Goto _ | Ret _ | Int _ -> None - | Call call -> match Call.target call with - | Indirect _ -> None - | Direct tid -> Some tid - -let detect_main_address prog = - let open Monad.Option.Syntax in - find_by_name prog "__libc_start_main" >>= fun start -> - find_first_caller prog (Term.tid start) >>= fun caller -> - Term.first blk_t caller >>= fun entry -> - Term.first arg_t start >>= fun arg -> - let defs = Term.enum def_t ~rev:true entry in - match Arg.rhs arg with - | Bil.Var reg -> - Seq.find defs ~f:(fun def -> - Var.same (Def.lhs def) reg) >>| Def.rhs >>= proj_int - | Bil.Load (_,addr,_,_) -> - Seq.find_map defs ~f:(fun def -> match Def.rhs def with - | Bil.Store (m,a,e,_,_) when Exp.equal addr a -> Some e - | _ -> None) >>= proj_int - | _ -> None - -let rename_main abi prog = match detect_main_address prog with - | None -> prog - | Some addr -> - Term.map sub_t prog ~f:(fun sub -> - match Term.get_attr sub address with - | Some a when Addr.equal addr a -> - abi#map_sub (Sub.with_name sub "main") - | _ -> sub) - -let rename_libc_start_main abi prog = - if is_sub_absent prog "__libc_start_main" - then match find_libc_start_main prog with - | None -> prog - | Some tid -> - Term.change sub_t prog tid @@ function - | None -> None - | Some sub -> Some (abi#map_sub (Sub.with_name sub "__libc_start_main")) - else prog - -let fix_libc_runtime abi prog = - rename_libc_start_main abi prog |> - rename_main abi - -let stage2 stage1 = object - inherit Term.mapper - method! run prog = - let prog = stage1#run prog in - if has_libc_runtime prog && - (is_sub_absent prog "main" || - (is_sub_absent prog "__libc_start_main")) - then fix_libc_runtime stage1 prog - else prog -end - let registry = Hashtbl.create (module String) let register name abi = Hashtbl.set registry ~key:name ~data:abi let get_processor name = Hashtbl.find registry name +let get_prototype gamma name = match gamma name with + | Some (`Function proto) -> proto + | _ -> + let open Bap_c_type in + Spec.{ + qualifier = `no_qualifier; + attrs = []; + t = Proto.{ + args = []; + variadic = false; + return = `Basic { + qualifier = Qualifier.{ + const = false; + volatile = false; + restrict = (); + }; + attrs = []; + t = `sint; + } + } + } + let create_api_processor size abi : Bap_api.t = let addr_size = size#pointer in + let stage1 gamma = object(self) inherit Term.mapper as super method! map_sub sub = @@ -196,13 +130,12 @@ let create_api_processor size abi : Bap_api.t = method private apply_proto sub = let name = Sub.name sub in - match gamma name with - | Some (`Function {Bap_c_type.Spec.t; attrs}) -> - let sub = self#apply_args sub attrs t in - let sub = Term.set_attr sub Attrs.proto t in - let sub = List.fold_right ~init:sub attrs ~f:Bap_c_attr.apply in - abi.apply_attrs attrs sub - | _ -> super#map_sub sub + let {Bap_c_type.Spec.t; attrs} = get_prototype gamma name in + let sub = self#apply_args sub attrs t in + let sub = Term.set_attr sub Attrs.proto t in + let sub = List.fold_right ~init:sub attrs ~f:Bap_c_attr.apply in + abi.apply_attrs attrs sub + method private apply_args sub attrs t = match abi.insert_args sub attrs t with @@ -237,7 +170,7 @@ let create_api_processor size abi : Bap_api.t = | Ok api -> List.iter api ~f:(fun (key,t) -> Hashtbl.set gamma ~key ~data:t)); - stage2 (stage1 (Hashtbl.find gamma)) + stage1 (Hashtbl.find gamma) let parse get ifs = Or_error.try_with (fun () -> parse_exn get ifs) diff --git a/lib/bap_main/bap_main.ml b/lib/bap_main/bap_main.ml index aada1d044..8d62c4e49 100644 --- a/lib/bap_main/bap_main.ml +++ b/lib/bap_main/bap_main.ml @@ -212,6 +212,44 @@ module Error = struct let register_printer = Caml.Printexc.register_printer let pp ppf e = Format.pp_print_string ppf (Caml.Printexc.to_string e) + + let str fmt = Format.kasprintf Option.some fmt + + let () = register_printer @@ function + | Configuration -> + str "Failed to process command-line options and configuration \ + paratemers." + | Invalid msg -> str "Invalid parameter: %s" msg + | Bug (exn,backtrace) -> + str "Internal error: %a@\nBacktrace:@\n%s" + Exn.pp exn backtrace + | Already_initialized -> + str "The system was already initialized" + | Already_failed e -> + str "The system was left in an inconsistent state after \ + the last attempt to initialize, which failed \ + with:@\n%a" pp e + | Recursive_init -> + str "The system initialization procedure was called during \ + the initialization. Aborting the infinite cycle." + | Broken_plugins errors -> + let pp_error ppf (name,err) = + Format.fprintf ppf + "The plugin `%s' has failed with \ + the following error:@\n%a@\n" name Error.pp err in + let pp_errors = + Format.pp_print_list ~pp_sep:Format.pp_print_newline pp_error in + str "Failed to load %d plugins, details follow:@\n%a" + (List.length errors) + pp_errors errors + | Unknown_plugin p -> + str "There is no plugin %S in the search path." p + | Exit_requested 0 -> str "All is good." + | Exit_requested n -> str "Exiting with %d." n + | Bad_recipe err -> + str "Can't load the specified recipe:@\n%a" + Bap_recipe.pp_error err + | _ -> None end module Markdown : sig diff --git a/lib/bap_primus/.merlin b/lib/bap_primus/.merlin index 2fb3f0bc1..73b2dc662 100644 --- a/lib/bap_primus/.merlin +++ b/lib/bap_primus/.merlin @@ -1 +1,2 @@ -REC \ No newline at end of file +PKG zarith +REC diff --git a/lib/bap_primus/bap_primus.mli b/lib/bap_primus/bap_primus.mli index 35e3ec716..5d012a321 100644 --- a/lib/bap_primus/bap_primus.mli +++ b/lib/bap_primus/bap_primus.mli @@ -549,6 +549,7 @@ module Std : sig and type 'a e = ?boot:unit t -> ?init:unit t -> + ?fini:unit t -> (exit_status * project) m effect (** Local state of the machine. *) @@ -725,7 +726,7 @@ module Std : sig Components should minimize the side-effects on the Primus machine and do not use Interpreter, Linker, and/or any observable operations. In this phase the Primus Machine - operates in a deterministic mode and fork/switch operators are + operates in the deterministic mode and fork/switch operators are disabled. Once this phase is complete, the [init] observation is posted @@ -746,6 +747,10 @@ module Std : sig This stage is used to prepare the Machine for the execution. Once it is finished the [start] observation is posted. + Any exception that is thrown in this phase will prevent + machine from running and terminate the computation + immediately. + {3 The running phase} The [start] observation designates the start of the execution @@ -886,6 +891,7 @@ module Std : sig ?envp:string array -> ?args:string array -> ?init:unit Machine.Make(Knowledge).t -> + ?fini:unit Machine.Make(Knowledge).t -> ?start:unit Machine.Make(Knowledge).t -> system -> project -> Knowledge.state -> (exit_status * project * Knowledge.state, Knowledge.conflict) result @@ -996,6 +1002,7 @@ module Std : sig ?envp:string array -> ?args:string array -> ?init:unit Machine.t -> + ?fini:unit Machine.t -> ?start:unit Machine.t -> t -> project -> (exit_status * project) Machine.m end @@ -1140,6 +1147,7 @@ module Std : sig ?envp:string array -> ?args:string array -> ?init:unit Machine.Make(Knowledge).t -> + ?fini:unit Machine.Make(Knowledge).t -> ?start:unit Machine.Make(Knowledge).t -> system -> unit @@ -1902,6 +1910,9 @@ module Std : sig (** [const x] computes the constant expression [x] *) val const : word -> value m + (** [ite c x y] if [c] evals to [b1] then [x] else [y] *) + val ite : value -> value -> value -> value m + (** [load a d s] computes a load operation, that loads a word of size [s] using an order specified by the endianness [d] from address [a]. @@ -1923,6 +1934,16 @@ module Std : sig invoked and the operation is repeated. Otherwise the [Segmentation_fault] machine exception is raised. *) val store : value -> value -> endian -> size -> unit m + + (** [branch cnd yes no] if [cnd] evaluates to [zero] then + [yes] else [no]. *) + val branch : value -> 'a m -> 'a m -> 'a m + + + (** [repeat cnd body] evaluates [body] until [cnd] evaluates + to [zero]. Returns the value of [cnd]. *) + val repeat : value m -> 'a m -> value m + end end @@ -2178,15 +2199,42 @@ module Std : sig end - (** Value generators *) + (** Value generators. *) module Generator : sig type t = generator [@@deriving sexp_of] + (** [of_iterator iter init] creates a generator from a generic + iterator. + + The generic iterator [iter] may use any type as its domain + (as long as it provides the projection to [Bitvec.t]). The + type of the generator state is also abstract. + + @since 2.1.0 + *) + val of_iterator : + ?width:int -> + ?seed:(int -> 'a) -> + to_bitvec:('d -> Bitvec.t) -> + (module Iterator.Infinite + with type t = 'a + and type dom = 'd) -> 'a -> + t + + (** [create (module Iterator) seed] creates a integer generator from the provided [Iterator], and initializes it with the - given seed. *) + given seed. + + @param width is the width in bits of the generated words. + + Note, that the generator domain is defined by the [Iterator] + domain, not by the [width] parameter of the the + generator. + *) val create : + ?width:int -> (module Iterator.Infinite with type t = 'a and type dom = int) -> 'a -> t @@ -2194,15 +2242,18 @@ module Std : sig (** [static value] returns a generator that always produces the same [value]. *) - val static : int -> t + val static : ?width:int -> int -> t (** [unfold ~min ~max ~seed ~f] creates a generator that generates values by applying a function [f] to a pair of a generator state and previous value. *) - val unfold : ?min:int -> ?max:int -> ?seed:int -> + val unfold : ?width:int -> ?min:int -> ?max:int -> ?seed:int -> f:('a * int -> 'a * int) -> 'a -> t + (** [width] the size in bits of the generated words. *) + val width : t -> int + (** Random Number Generators *) module Random : sig @@ -2214,17 +2265,15 @@ module Std : sig @param min (defaults to 0) @param max (defaults to 1^30) *) - val lcg : ?min:int -> ?max:int -> int -> t - + val lcg : ?width:int -> ?min:int -> ?max:int -> int -> t (** [byte seed] the same as [lcg ~min:0 ~max:255 seed] *) val byte : int -> t - (** Self seeded generators. These generators will be seeded by a value derived from - the Machine clone identifier. *) + the Machine identifier. *) module Seeded : sig (** [create init] creates a self-seeded generator from a @@ -2237,17 +2286,16 @@ module Std : sig - [Random.lcg] - [Random.byte] *) - val create : (int -> t) -> t + val create : ?width:int -> (int -> t) -> t (** [lcg ~min ~max ()] a linear congruential generator. *) - val lcg : ?min:int -> ?max:int -> unit -> t + val lcg : ?width:int -> ?min:int -> ?max:int -> unit -> t (** [byte] is the same as [lcg ~min:0 ~max:255 ()] *) val byte : t end - end @@ -2261,7 +2309,13 @@ module Std : sig (** [word iter bitwidth] constructs a word of the given [bitwidth], - with bytes obtained from consequitive calls to [next].*) + from words obtained from consequitive calls to [next]. + + The generator is called [ceil (bitwidth / width)] times + and the generated words are concatenated in the order of + the increasing significance with any excessive most + significant bits truncated. + *) val word : t -> int -> word Machine.t end end @@ -2275,15 +2329,12 @@ module Std : sig environment. *) type exn += Undefined_var of var + val generated : (var * value) observation (** [Env = Make(Machine)] *) module Make(Machine : Machine.S) : sig - (** [get var] returns a value associated with the variable. - Todo: it looks like that the interface doesn't allow - anyone to save bottom or memory values in the environment, - thus the [get] operation should not return the - [Bil.result].*) + (** [get var] returns a value associated with the variable. *) val get : var -> value Machine.t (** [set var value] binds a variable [var] to the given [value]. *) @@ -2298,6 +2349,19 @@ module Std : sig val add : var -> Generator.t -> unit Machine.t + (** [del v] deletes the variable [v] from the environment. + + The variable [v] will no longer be bound. + *) + val del : var -> unit Machine.t + + + (** [has v] evaluates to [true] if [v] is bound. + + @since 2.1.0 + *) + val has : var -> bool Machine.t + (** [all] is a sequence of all variables defined in the environment. Note, the word _defined_ doesn't mean initialized. *) @@ -2349,15 +2413,29 @@ module Std : sig val unknown : addr_size:int -> data_size:int -> memory - (** [name memory] returns [memory] identifier. *) + (** [name memory] returns [memory] identifier. + @since 2.1.0 + *) val name : memory -> string + + (** [addr_size memory] the number of bits in the address bus. + @since 2.1.0 + *) + val addr_size : memory -> int + + + (** [data_size memory] is the the number of bits in the data bus. *) + val data_size : memory -> int + include Comparable.S with type t := t end (** occurs when a memory operation for the given addr cannot be satisfied. *) type exn += Pagefault of addr + val generated : (addr * value) observation + (** [Make(Machine)] lifts the memory interface into the [Machine] monad. *) @@ -2386,10 +2464,15 @@ module Std : sig raises the [Pagefault] machine exception if [a] is not mapped, or not writable. - Precondition: [Value.bitwidth x = 8]. + Precondition: the size of the address and the size of the + datum match with the current [memory] sizes. *) val set : addr -> value -> unit Machine.t + + (** [del p] removes the value associated with the pointer [p]. *) + val del : addr -> unit Machine.t + (** [load a] loads a byte from the given address [a]. Same as [get a >>= Value.to_word] @@ -2412,17 +2495,35 @@ module Std : sig nonexecutable segment of machine memory. *) val add_data : mem -> unit Machine.t - - (** [allocate addr size] allocates a segment of the specified - [size]. An unitilialized reads from the segment will + (** [add_region ~lower ~upper] allocates a segment of memory + denoted by its [lower] and [upper] bounds (included). + An unitilialized reads from the segment will produce values generated by a generator (defaults to a - [Generator.Random.Seeded.byte]). + [Generator.Random.Seeded.lcg ~width ()], where width is + the data size of the currently selected memory bank ). - If [init] is provided then the region is initialized. + If [init] is provided then the region is initialized, it + is the responsibility of [init] to generates words of + correct size (matching the data size of the currently + selected memory bank). An attempt to write to a readonly segment, or an attempt to execute non-executable segment will generate a - segmentation fault. (TODO: provide more fine-granular traps).*) + segmentation fault. + + @since 2.1.0 + *) + val add_region : + ?readonly:bool -> + ?executable:bool -> + ?init:(addr -> word Machine.t) -> + ?generator:Generator.t -> + lower:addr -> upper:addr -> unit -> unit Machine.t + + (** [allocate addr size] allocates a segment of the specified + [size]. This function uses {!add_region} underneath the + hood, please refer to it for more information. + *) val allocate : ?readonly:bool -> ?executable:bool -> @@ -2438,7 +2539,6 @@ module Std : sig ?executable:bool -> mem -> unit Machine.t - (** [is_mapped addr] a computation that evaluates to true, when the value is mapped, i.e., it is readable. *) val is_mapped : addr -> bool Machine.t @@ -3440,18 +3540,30 @@ ident ::= ?any atom that is not recognized as a ? val pp : Format.formatter -> t -> unit end + (** Machine independent closure. A closure is an anonymous function, that performs some computation in the Machine Monad. Closures are used to extend the Lisp Machine with arbitrary primitive operations implemented in OCaml. *) - module type Closure = functor (Machine : Machine.S) -> sig + module Closure : sig + module type S = functor (Machine : Machine.S) -> sig + + (** [run args] performs the computation. *) + val run : value list -> value Machine.t + end + + type t = (module S) + module Make(Machine : Machine.S) : sig + val name : string Machine.t + end - (** [run args] performs the computation. *) - val run : value list -> value Machine.t end + module type Closure = Closure.S + + (** [(lisp-primitive ... )] is posted when the Lisp primitive with the given is called with @@ -3463,7 +3575,7 @@ ident ::= ?any atom that is not recognized as a ? val primitive : (string * value list) observation (** a closure packed as an OCaml value *) - type closure = (module Closure) + type closure = Closure.t (* dedocumented due to deprecation *) module Primitive : sig diff --git a/lib/bap_primus/bap_primus_env.ml b/lib/bap_primus/bap_primus_env.ml index d4be0c56b..079d9c8f3 100644 --- a/lib/bap_primus/bap_primus_env.ml +++ b/lib/bap_primus/bap_primus_env.ml @@ -19,6 +19,16 @@ type t = { random : Generator.t Var.Map.t; } +let inspect_generated (v,x) = Sexp.List [ + sexp_of_var v; + sexp_of_value x + ] + +let generated,on_generated = + Observation.provide "var-generated" + ~inspect:inspect_generated + ~package:"bap" + let sexp_of_values values = Sexp.List (Map.to_sequence values |> Seq.map ~f:(fun (v,{value}) -> Sexp.List [ @@ -90,6 +100,12 @@ module Make(Machine : Machine) = struct let null = Machine.get () >>| Project.arch >>| Arch.addr_size >>= fun s -> Value.zero (Size.in_bits s) + + let del var = + Machine.Local.update state ~f:(fun s -> { + s with values = Map.remove s.values var; + }) + let get var = Machine.Local.get state >>= fun t -> match Map.find t.values var with @@ -100,7 +116,9 @@ module Make(Machine : Machine) = struct | None -> Machine.raise (Undefined_var var) | Some gen -> Generator.word gen width >>= Value.of_word >>= fun x -> - set var x >>| fun () -> x + set var x >>= fun () -> + Machine.Observation.make on_generated (var,x) >>| fun () -> + x let has var = Machine.Local.get state >>| fun t -> diff --git a/lib/bap_primus/bap_primus_env.mli b/lib/bap_primus/bap_primus_env.mli index 095963703..49b55b6b2 100644 --- a/lib/bap_primus/bap_primus_env.mli +++ b/lib/bap_primus/bap_primus_env.mli @@ -5,10 +5,13 @@ module Generator = Bap_primus_generator type exn += Undefined_var of var +val generated : (var * value) Bap_primus_observation.t + module Make(Machine : Machine) : sig val get : var -> value Machine.t val set : var -> value -> unit Machine.t val add : var -> Generator.t -> unit Machine.t + val del : var -> unit Machine.t val has : var -> bool Machine.t val all : var seq Machine.t end diff --git a/lib/bap_primus/bap_primus_generator.ml b/lib/bap_primus/bap_primus_generator.ml index a1075fca1..2cd1e7ea5 100644 --- a/lib/bap_primus/bap_primus_generator.ml +++ b/lib/bap_primus/bap_primus_generator.ml @@ -6,62 +6,84 @@ open Bap_primus_generator_types module Iterator = Bap_primus_iterator - -let uniform_coverage ~total ~trials = - ~-.(Float.expm1 (float trials *. Float.log1p( ~-.(1. /. float total)))) - - - -let generators : Univ_map.t state = Bap_primus_machine.State.declare - ~name:"rng-states" - ~uuid:"7e81d5ae-46a2-42ff-918f-96c0c2dc95e3" - (fun _ -> Univ_map.empty) - -module States = Univ_map - -module type Iter = - Iterator.Infinite.S with type dom = int - -type 'a iter = (module Iter with type t = 'a) - -type 'a gen = { - iter : 'a iter; - self : 'a; +type 'a iface = + (module Iterator.Infinite.S with type dom = Bitvec.t + and type t = 'a) + +type iterator = Iter : { + ctrl : 'a iface; + self : 'a; + seed : int -> 'a + } -> iterator + +type iterators = { + iterators : iterator Int.Map.t; + salt : int; } -type 'a key = 'a gen States.Key.t - -type 'a ready = { - key : 'a key; - gen : 'a gen; +let iterators = Bap_primus_machine.State.declare + ~name:"iterators" + ~uuid:"9927004d-fe57-4de9-8705-c3d6862238cf" @@ fun _ -> { + iterators = Int.Map.empty; + salt = 1; + } + +type constructor = + | Const of iterator + | Seeded of (int -> iterator) + +type t = { + size : int; + init : constructor; + id : int; } -type 'a wait = { - key : 'a key; - init : int -> 'a gen -} - -type t = - | Static : int -> t - | Ready : 'a ready -> t - | Wait : 'a wait -> t - -let rec sexp_of_t = function - | Static x -> Sexp.(List [Atom "static"; sexp_of_int x]) - | _ -> Sexp.Atom "" - -let make key init iter = Ready {key; gen={iter; self=init}} - -let create iter init = - let state = States.Key.create - ~name:"rng-state" sexp_of_opaque in - make state init iter +let last_id = ref 0 + +let width x = x.size +let sexp_of_t {id} = Sexp.List [ + Atom "generator"; + sexp_of_int id; + ] + +let of_iterator (type dom) (type t) + ?(width=8) + ?seed + ~to_bitvec + (module Iter : Iterator.Infinite.S + with type t = t + and type dom = dom) self = + incr last_id; + let module Iface = struct + type t = Iter.t + type dom = Bitvec.t + let min = to_bitvec Iter.min + let max = to_bitvec Iter.max + let value self = to_bitvec @@ Iter.value self + let next self = Iter.next self + end in { + size=width; + id = !last_id; + init = Const (Iter { + ctrl = (module Iface); + self; + seed = match seed with + | Some seed -> seed + | None -> fun _ -> self + }) + } + +let create ?(width=8) iter init = + let m = Bitvec.modulus width in + of_iterator ~width iter init + ~to_bitvec:(fun x -> Bitvec.(int x mod m)) let unfold (type gen) + ?width ?(min=Int.min_value) ?(max=Int.max_value) ?(seed=0) - ~f init = + ~f init = let module Gen = struct type t = gen * int type dom = int @@ -70,61 +92,43 @@ let unfold (type gen) let next = f let value = snd end in - create (module Gen) (init,seed) + create ?width (module Gen) (init,seed) -let static value = Static value +let static ?(width=8) value = + let value = Bitvec.(int value mod modulus width) in + of_iterator ~width ~to_bitvec:ident (module struct + type t = Bitvec.t + type dom = Bitvec.t + let min = value + let max = value + let next _ = value + let value _ = value + end) value module Random = struct - open Bap_primus_random - - let lcg_key : (LCG.t * int) gen States.Key.t = - States.Key.create ~name:"linear-congruent-generator" - sexp_of_opaque - - let lcg ?(min=LCG.min) ?(max=LCG.max) seed = - let next (gen,_) = - let gen = LCG.next gen in - let x = min + LCG.value gen mod (max-min+1) in - gen,x in - let value = snd in - let init = next (LCG.create seed,0) in - make lcg_key init (module struct - type t = LCG.t * int - type dom = int - let min = min - let max = max - let next = next - let value = value - end) - + module MCG = Bap_primus_random.MCG + let create_lcg ?(width=8) ?min ?max start = + let module Gen = (val MCG.create_small ?min ?max width) in + let seed s = Gen.create (s + start) in + of_iterator ~width ~to_bitvec:ident ~seed + (module Gen) (Gen.create start) + + let lcg = create_lcg let byte seed = lcg ~min:0 ~max:255 seed - let cast_gen : type a b. a key -> b ready -> a gen option = - fun k1 {key=k2; gen} -> match States.Key.same_witness k1 k2 with - | None -> None - | Some Type_equal.T -> Some gen + module Seeded = struct + let create ?(width=8) init = + incr last_id; + let init seed = match init seed with + | {init=Const iter} -> iter + | {init=Seeded init} -> init seed in + {size=width; init = Seeded init; id = !last_id} + let lcg ?width ?min ?max () = + create_lcg ?width ?min ?max 0 - module Seeded = struct - let unpack_make key make = - let init seed = match make seed with - | Wait _ - | Static _ -> failwith "Generator.Seeded: invalid initializer" - | Ready g -> match cast_gen key g with - | Some g -> g - | None -> invalid_arg "Seeded.create changed its type" in - Wait {key; init} - - let create make = match make 0 with - | Ready {key} -> unpack_make key make - | _ -> invalid_arg "Seeded.create must always create \ - an iterator of the same type" - - let lcg ?min ?max () = unpack_make lcg_key (fun seed -> - lcg ?min ?max seed) - - let byte = lcg ~min:0 ~max:255 () + let byte = lcg () end end @@ -132,37 +136,51 @@ end module Make(Machine : Machine) = struct open Machine.Syntax - let call (type a) (state : a key) ({iter; self} : a gen) = - let module Iter : Iter with type t = a = (val iter) in - Machine.Local.get generators >>= fun states -> - let self = match States.find states state with - | None -> self - | Some {self} -> self in - let iter = { - iter; - self = Iter.next self; - } in - let states = States.set states state iter in - Machine.Local.put generators states >>| fun () -> - Iter.value iter.self - - let rec next = function - | Static n -> Machine.return n - | Ready {key; gen} -> call key gen - | Wait {key; init} -> - Machine.Local.get generators >>= fun states -> - match States.find states key with - | None -> - Machine.current () >>= fun id -> - call key (init (Machine.Id.hash id)) - | Some iter -> call key iter + let rec call gen = + Machine.Local.get iterators >>= fun {iterators=iters; salt} -> + match Map.find iters gen.id with + | Some Iter {ctrl=(module Iter); self; seed} -> + let value = Iter.value self in + let next = Iter { + ctrl = (module Iter); + self = Iter.next self; + seed + } in + Machine.Local.put iterators { + iterators = Map.set iters gen.id next; + salt; + } >>| fun () -> + value + | None -> + Machine.current () >>= fun id -> + let seed = Machine.Id.hash id + salt in + match gen.init with + | Const Iter it -> + let iter = Iter {it with self = it.seed seed} in + Machine.Local.put iterators { + iterators = Map.set iters gen.id iter; + salt = salt + 1; + } >>= fun () -> + call gen + | Seeded init -> + Machine.Local.put iterators { + iterators = Map.set iters gen.id (init seed); + salt; + } >>= fun () -> + call gen + + let next gen = call gen >>| fun x -> + if Bitvec.fits_int x + then Bitvec.to_int x + else Int.max_value let word gen width = - let word = Word.of_int ~width:8 in - assert (width > 0); - let rec loop x = - if Word.bitwidth x >= width - then Machine.return (Word.extract_exn ~hi:(width-1) x) - else next gen >>= fun y -> loop (Word.concat x (word y)) in - next gen >>| word >>= loop + let rec loop built x = + if built >= width + then Machine.return (Word.create x width) + else + call gen >>= fun y -> + loop (built+gen.size) @@ + Bitvec.append built gen.size x y in + call gen >>= loop gen.size end diff --git a/lib/bap_primus/bap_primus_generator.mli b/lib/bap_primus/bap_primus_generator.mli index 377285da1..4abc3a992 100644 --- a/lib/bap_primus/bap_primus_generator.mli +++ b/lib/bap_primus/bap_primus_generator.mli @@ -4,22 +4,35 @@ open Bap_primus_types type t [@@deriving sexp_of] +val of_iterator : + ?width:int -> + ?seed:(int -> 'a) -> + to_bitvec:('d -> Bitvec.t) -> + (module Iterator.Infinite + with type t = 'a + and type dom = 'd) -> 'a -> + t + val create : + ?width:int -> (module Iterator.Infinite with type t = 'a and type dom = int) -> 'a -> t -val static : int -> t +val static : ?width:int -> int -> t -val unfold : ?min:int -> ?max:int -> ?seed:int -> +val width : t -> int + +val unfold : ?width:int -> ?min:int -> ?max:int -> ?seed:int -> f:('a * int -> 'a * int) -> 'a -> t module Random : sig - val lcg : ?min:int -> ?max:int -> int -> t + val lcg : ?width:int -> ?min:int -> ?max:int -> int -> t val byte : int -> t + module Seeded : sig - val create : (int -> t) -> t - val lcg : ?min:int -> ?max:int -> unit -> t + val create : ?width:int -> (int -> t) -> t + val lcg : ?width:int -> ?min:int -> ?max:int -> unit -> t val byte : t end end diff --git a/lib/bap_primus/bap_primus_interpreter.ml b/lib/bap_primus/bap_primus_interpreter.ml index 3a966bcd1..2d7217c2f 100644 --- a/lib/bap_primus/bap_primus_interpreter.ml +++ b/lib/bap_primus/bap_primus_interpreter.ml @@ -191,7 +191,6 @@ let eval_cond,on_cond = Observation.provide ~inspect:sexp_of_value "eval-cond" ~desc:"Occurs when the jump condition is evaluated." - let results r op = Sexp.List [op; sexp_of_value r] let sexp_of_binop ((op,x,y),r) = results r @@ sexps [ @@ -200,7 +199,6 @@ let sexp_of_binop ((op,x,y),r) = results r @@ sexps [ string_of_value y; ] - let sexp_of_unop ((op,x),r) = results r @@ sexps [ Bil.string_of_unop op; string_of_value x; @@ -312,7 +310,7 @@ type exn += Runtime_error of string let () = Exn.add_printer (function | Runtime_error msg -> - Some (sprintf "Bap_primus runtime error: %s" msg) + Some (sprintf "Primus interpreter runtime error: %s" msg) | Halt -> Some "Halt" | Segmentation_fault x -> Some (asprintf "Segmentation fault at %a" Addr.pp_hex x) @@ -355,11 +353,6 @@ module Make (Machine : Machine) = struct value (word_of_type t) >>= fun r -> !!on_undefined r >>| fun () -> r - let set v x = - !!on_writing v >>= fun () -> - Env.set v x >>= fun () -> - post on_written ~f:(fun k -> k (v,x)) - let get v = !!on_reading v >>= fun () -> Env.get v >>= fun r -> @@ -377,19 +370,6 @@ module Make (Machine : Machine) = struct s with time = Time.succ s.time; } - let binop op x y = match op with - | Bil.DIVIDE | Bil.SDIVIDE - | Bil.MOD | Bil.SMOD - when Word.is_zero y.value -> - !!will_divide_by_zero () >>= fun () -> - call_when_provided division_by_zero_handler >>= fun called -> - if called - then undefined (Type.Imm (Word.bitwidth x.value)) - else Machine.raise Division_by_zero - | _ -> - value (Bil.Apply.binop op x.value y.value) >>= fun r -> - tick >>= fun () -> - post on_binop ~f:(fun k -> k ((op,x,y),r)) >>| fun () -> r let unop op x = value (Bil.Apply.unop op x.value) >>= fun r -> @@ -408,10 +388,45 @@ module Make (Machine : Machine) = struct value (Word.extract_exn ~hi ~lo x.value) >>= fun r -> post on_extract ~f:(fun k -> k ((hi,lo,x),r)) >>| fun () -> r + + let coerce s x = + if Value.bitwidth x <> s + then extract ~hi:(s-1) ~lo:0 x + else Machine.return x + + let binop op x y = match op with + | Bil.DIVIDE | Bil.SDIVIDE + | Bil.MOD | Bil.SMOD + when Word.is_zero y.value -> + !!will_divide_by_zero () >>= fun () -> + call_when_provided division_by_zero_handler >>= fun called -> + if called + then undefined (Type.Imm (Word.bitwidth x.value)) + else Machine.raise Division_by_zero + | _ -> + let s = max (Value.bitwidth x) (Value.bitwidth y) in + coerce s x >>= fun x -> + coerce s y >>= fun y -> + value (Bil.Apply.binop op x.value y.value) >>= fun r -> + tick >>= fun () -> + post on_binop ~f:(fun k -> k ((op,x,y),r)) >>| fun () -> r + let const c = value c >>= fun r -> !!on_const r >>| fun () -> r + let set v x = + !!on_writing v >>= fun () -> + let x = match Var.typ v with + | Unk | Mem _ -> Machine.return x + | Imm m -> + if Value.bitwidth x <> m + then extract ~hi:(m-1) ~lo:0 x + else Machine.return x in + x >>= fun x -> + Env.set v x >>= fun () -> + post on_written ~f:(fun k -> k (v,x)) + let trapped_memory_access access = Machine.catch access (function | Bap_primus_memory.Pagefault a -> @@ -592,6 +607,11 @@ module Make (Machine : Machine) = struct let store a x e s = let open Bil.Types in let s = Size.in_bits s in + let x = + if Value.bitwidth x <> s + then extract ~hi:(s-1) ~lo:0 x + else Machine.return x in + x >>= fun x -> match e with | LittleEndian -> do_store a x s LOW HIGH | BigEndian -> do_store a x s HIGH LOW @@ -631,6 +651,21 @@ module Make (Machine : Machine) = struct !!pos_left curr + let branch cnd yes no = + Value.zero (Value.bitwidth cnd) >>= fun zero -> + binop Bil.EQ cnd zero >>= fun is_zero -> + !!on_cond is_zero >>= fun () -> + if Value.is_one is_zero then no else yes + + let rec repeat cnd body = + cnd >>= fun x -> + Value.zero (Value.bitwidth x) >>= fun zero -> + binop Bil.EQ x zero >>= fun stop -> + !!on_cond stop >>= fun () -> + if Value.is_one stop + then Machine.return stop + else body >>= fun _ -> repeat cnd body + let term return cls f t = Machine.Local.get state >>= fun s -> match Pos.next s.curr cls t with @@ -734,6 +769,7 @@ module Make (Machine : Machine) = struct let jmp t = eval_exp (Jmp.cond t) >>= fun ({value} as cond) -> !!on_cond cond >>| fun () -> Option.some_if (Word.is_one value) (cond,t) + let jmp = term normal jmp_t jmp let blk t = @@ -744,7 +780,7 @@ module Make (Machine : Machine) = struct | None -> Machine.return () (* return from sub *) | Some (cond,code) -> jump cond code - let blk = term finish blk_t blk + let blk : blk term -> unit m = term finish blk_t blk let arg_def t = match Arg.intent t with | None | Some (In|Both) -> Arg.lhs t := Arg.rhs t @@ -787,6 +823,7 @@ module Make (Machine : Machine) = struct let args = List.rev_append inputs rets in k (name,args)) + let assume x = !!on_cond x let sub = term normal sub_t sub let pos = Machine.Local.get state >>| fun {curr} -> curr diff --git a/lib/bap_primus/bap_primus_interpreter.mli b/lib/bap_primus/bap_primus_interpreter.mli index d475ff4c2..c485d26be 100644 --- a/lib/bap_primus/bap_primus_interpreter.mli +++ b/lib/bap_primus/bap_primus_interpreter.mli @@ -95,9 +95,11 @@ module Make (Machine : Machine) : sig val concat : value -> value -> value m val extract : hi:int -> lo:int -> value -> value m val const : word -> value m + val ite : value -> value -> value -> value m val load : value -> endian -> size -> value m val store : value -> value -> endian -> size -> unit m - + val branch : value -> 'a m -> 'a m -> 'a m + val repeat : value m -> 'a m -> value m val tick : unit m val time : Time.t m end diff --git a/lib/bap_primus/bap_primus_lisp.ml b/lib/bap_primus/bap_primus_lisp.ml index 310b67cf7..490b5b7f8 100644 --- a/lib/bap_primus/bap_primus_lisp.ml +++ b/lib/bap_primus/bap_primus_lisp.ml @@ -8,6 +8,7 @@ open Bap_primus_sexp module Lisp = struct module Attribute = Bap_primus_lisp_attribute + module Attributes = Bap_primus_lisp_attributes module Def = Bap_primus_lisp_def module Var = Bap_primus_lisp_var module Parse = Bap_primus_lisp_parse @@ -25,7 +26,6 @@ open Lisp.Program.Items module Pos = Bap_primus_pos - type exn += Runtime_error of string type exn += Unresolved of string * Lisp.Resolve.resolution @@ -85,18 +85,20 @@ module Errors(Machine : Machine) = struct let failf fmt = error (fun m -> Runtime_error m) fmt end + +let var_of_lisp_var width {data={exp;typ}} = + match typ with + | Type t -> Var.create exp (Type.Imm t) + | _ -> Var.create exp (Type.Imm width) + module Locals(Machine : Machine) = struct open Machine.Syntax include Errors(Machine) - let of_lisp width {data={exp;typ}} = - match typ with - | Type t -> Var.create exp (Type.Imm t) - | _ -> Var.create exp (Type.Imm width) let make_frame width bs = List.fold ~init:([],0) bs ~f:(fun (xs,n) (v,x) -> - (of_lisp width v,x)::xs, n+1) + (var_of_lisp_var width v,x)::xs, n+1) let rec update xs x ~f = match xs with | [] -> [] @@ -145,7 +147,7 @@ end let () = Exn.add_printer (function - | Runtime_error msg -> Some ("primus runtime error - " ^ msg) + | Runtime_error msg -> Some ("Primus Lisp runtime error - " ^ msg) | Unresolved (name,res) -> let msg = asprintf "unable to resolve function %s, because %a" name Lisp.Resolve.pp_resolution res in @@ -166,12 +168,20 @@ let message,new_message = ~inspect:sexp_of_string "lisp-message" ~desc:"Occurs with X when (msg x) is evaluated." +type closure_frame = { + name : string; + args : value list; +} + +let closure_context = Bap_primus_state.declare + ~uuid:"b31c12fc-a131-4966-bcc9-e360ed76fb8e" + ~name:"lisp-closure-context" @@ fun _ -> [] + module Trace = Bap_primus_linker.Trace type dir = [`down | `up] [@@deriving equal] - module Interpreter(Machine : Machine) = struct open Machine.Syntax module Linker = Bap_primus_linker.Make(Machine) @@ -227,6 +237,10 @@ module Interpreter(Machine : Machine) = struct | Some Out -> true | _ -> false + let is_zero x = + Value.zero (Value.bitwidth x) >>= fun zero -> + Eval.binop Bil.EQ x zero + (* we won't notify linker about a call, since the callee will notify it itself. Basically, it is the responsibility of a callee to register itself as a call, if it is a call. *) @@ -285,6 +299,15 @@ module Interpreter(Machine : Machine) = struct | Some r -> notify (name, args@[r])) else Machine.return () + let push_context name args = + Machine.Local.update closure_context ~f:(fun frames -> + {name; args} :: frames) + + let pop_context = + Machine.Local.update closure_context ~f:(function + | [] -> failwith "Bug: empty closure context" + | _ :: frames -> frames) + (* Still an open question. Shall we register an call to an external function, that is done not directly from a program, but internally from other lisp function? @@ -346,7 +369,9 @@ module Interpreter(Machine : Machine) = struct let module Code = Body(Machine) in Eval.const Word.b0 >>= fun init -> eval_advices Advice.Before init name args >>= fun _ -> + push_context name args >>= fun () -> Code.run args >>= fun r -> + pop_context >>= fun () -> Eval.tick >>= fun () -> Machine.Observation.post primitive_called ~f:(fun k -> k (name,args@[r])) >>= fun () -> @@ -359,7 +384,8 @@ module Interpreter(Machine : Machine) = struct | Symbol -> Machine.return Lisp.Type.symbol_size | Any | Name _ -> width () in width >>= fun width -> - Eval.const (Word.of_int64 ~width v) in + let bv = Bitvec.(bigint v mod modulus width) in + Eval.const (Word.create bv width) in let sym v = Value.Symbol.to_value v.data in let rec eval = function | {data=Int {data={exp;typ}}} -> int exp typ @@ -373,25 +399,21 @@ module Interpreter(Machine : Machine) = struct | {data=Set (v,e)} -> eval e >>= set v | {data=Msg (fmt,es)} -> msg fmt es | {data=Err msg} -> Machine.raise (Runtime_error msg) - and rep c e = - Eval.tick >>= fun () -> - eval c >>= function {value} as r -> - if Word.is_zero value then Machine.return r - else eval e >>= fun _ -> rep c e + and rep c e = Eval.repeat (eval c) (eval e) and ite c e1 e2 = - eval c >>= fun {value=w} -> - if Word.is_zero w then eval e2 else eval e1 + eval c >>= fun c -> + Eval.branch c (eval e1) (eval e2) and let_ v e1 e2 = Machine.Local.get state >>= fun {width} -> eval e1 >>= fun w -> - let v = Vars.of_lisp width v in + let v = var_of_lisp_var width v in Machine.Local.update state ~f:(Vars.push v w) >>= fun () -> eval e2 >>= fun r -> Machine.Local.update state ~f:(Vars.pop 1) >>= fun () -> Machine.return r and lookup v = Machine.Local.get state >>= fun {env; width; program} -> - let v = Vars.of_lisp width v in + let v = var_of_lisp_var width v in if Map.mem env.vars v then Machine.return @@ @@ -420,28 +442,28 @@ module Interpreter(Machine : Machine) = struct loop es and set v w = Machine.Local.get state >>= fun s -> - let v = Vars.of_lisp s.width v in + let v = var_of_lisp_var s.width v in if Map.mem s.env.vars v then Machine.Local.put state (Vars.replace v w s) >>| fun () -> w else Eval.set v w >>| fun () -> w and msg fmt es = - let buf = Buffer.create 64 in - let ppf = formatter_of_buffer buf in - let pp_exp e = + let str e = Machine.catch - (eval e >>| fun {value=x} -> fprintf ppf "%a" Word.pp x) + (eval e >>= fun v -> + Value.Symbol.of_value v >>| function + | "" -> asprintf "%a" Word.pp v.value + | s -> asprintf "#<%s %a>" s Word.pp v.value) (fun err -> - fprintf ppf "<%s>" (Exn.to_string err); - Machine.return ()) in - Machine.List.iter fmt ~f:(function - | Lit s -> Machine.return (pp_print_string ppf s) + Machine.return (asprintf "<%s>" (Exn.to_string err))) in + Machine.List.map fmt ~f:(function + | Lit s -> Machine.return s | Pos n -> match List.nth es n with | None -> failf "bad positional argument $%d" n () - | Some e -> pp_exp e) >>= fun () -> - pp_print_flush ppf (); - Machine.Observation.make new_message (Buffer.contents buf) >>= fun () -> + | Some e -> str e) >>= fun contents -> + let msg = String.concat contents in + Machine.Observation.make new_message msg >>= fun () -> Eval.const Word.b0 in Machine.Local.update state (fun s -> {s with cur = exp.id}) >>= fun () -> eval exp @@ -465,10 +487,25 @@ end let init ?log:_ ?paths:_ _features = failwith "Lisp library no longer requires initialization" +module Closure = struct + module type S = Lisp.Def.Closure + type t = (module S) + module Make(Machine : Machine) = struct + open Machine.Syntax + module Lisp = Interpreter(Machine) + let name = + Machine.Local.get closure_context >>= function + | [] -> Lisp.failf "Closure.name is called not from a closure" () + | {name} :: _ -> Machine.return name + end +end + +module type Closure = Closure.S + + type primitives = Lisp.Def.primitives module type Primitives = Lisp.Def.Primitives module Primitive = Lisp.Def.Primitive -module type Closure = Lisp.Def.Closure type closure = Lisp.Def.closure type program = Lisp.Program.t module Load = Lisp.Parse @@ -531,6 +568,7 @@ module Make(Machine : Machine) = struct module Eval = Bap_primus_interpreter.Make(Machine) module Value = Bap_primus_value.Make(Machine) module Vars = Locals(Machine) + module Env = Bap_primus_env.Make(Machine) include Errors(Machine) @@ -598,6 +636,32 @@ module Make(Machine : Machine) = struct Map.to_sequence + let collect_globals arch s = + let open Lisp.Attributes in + let default_width = Size.in_bits (Arch.addr_size arch) in + let add attr def vars = + match Attribute.Set.get (Lisp.Def.attributes def) attr with + | None -> vars + | Some vars' -> Set.union vars @@ + Var.Set.of_list @@ + List.map ~f:(var_of_lisp_var default_width) vars' in + Lisp.Program.get s.program Lisp.Program.Items.func |> + List.fold ~init:Var.Set.empty ~f:(fun vars def -> + add Variables.global def vars |> + add Variables.static def) |> + Set.to_sequence + + + let link_global var = match Var.typ var with + | Imm m -> + Value.zero m >>= Env.set var + | _ -> Machine.return () + + let link_globals () = + Machine.gets Project.arch >>= fun arch -> + Machine.Local.get state >>| collect_globals arch >>= + Machine.Seq.iter ~f:link_global + let find_sub prog name = Term.enum sub_t prog |> Seq.find ~f:(fun s -> String.equal (Sub.name s) name) |> function @@ -630,6 +694,7 @@ module Make(Machine : Machine) = struct let module Code(Machine : Machine) = struct open Machine.Syntax module Eval = Bap_primus_interpreter.Make(Machine) + module Value = Bap_primus_value.Make(Machine) module Interp = Interpreter(Machine) let failf ppf = Format.ksprintf @@ -652,12 +717,12 @@ module Make(Machine : Machine) = struct Eval.extract ~hi:(vsize-1) ~lo:rsize lhs >>= fun high -> Eval.concat high r >>= fun r -> Eval.set reg r - | e -> failf "unknown return semantics: %a" Exp.pps e () + | e -> failf "an unsupported return semantics: %a" Exp.pps e () let exec = eval_args >>= fun bs -> let args = List.rev_map ~f:snd bs in - Eval.const Word.b0 >>= fun init -> + Value.b0 >>= fun init -> Interp.eval_advices Advice.Before init name args >>= fun _ -> Machine.Local.update state ~f:(Vars.push_frame bs) >>= fun () -> Interp.notify_when true Trace.call_entered name args >>= fun () -> @@ -684,7 +749,8 @@ module Make(Machine : Machine) = struct Machine.Local.get state >>= fun s -> let s = {s with program = Lisp.Program.merge s.program program} in Machine.Local.put state s >>= fun () -> - link_features () + link_globals () >>= + link_features let program = Machine.Local.get state >>| fun s -> s.program @@ -758,6 +824,17 @@ module Make(Machine : Machine) = struct if Set.mem known_methods name then subs else sub::subs) in Machine.List.iter useless_subscriptions ~f:Machine.Observation.cancel + + + let refine ctxt = + Machine.Local.update state ~f:(fun s -> { + s with program = + Lisp.Program.with_context s.program + (Lisp.Context.merge + ctxt + (Lisp.Program.context s.program)) + }) + end module Doc = struct diff --git a/lib/bap_primus/bap_primus_lisp.mli b/lib/bap_primus/bap_primus_lisp.mli index 211e0adb5..185b34c06 100644 --- a/lib/bap_primus/bap_primus_lisp.mli +++ b/lib/bap_primus/bap_primus_lisp.mli @@ -75,9 +75,18 @@ module Type : sig val pp_error : Format.formatter -> error -> unit end -module type Closure = functor(Machine : Machine) -> sig - val run : value list -> value Machine.t +module Closure : sig + module type S = functor(Machine : Machine) -> sig + val run : value list -> value Machine.t + end + + type t = (module S) + + module Make(Machine : Machine) : sig + val name : string Machine.t + end end +module type Closure = Closure.S type closure = (module Closure) @@ -123,6 +132,8 @@ module Make (Machine : Machine) : sig val optimize : unit -> unit Machine.t + val refine : Bap_primus_lisp_context.t -> unit Machine.t + (* deprecated *) val link_primitives : primitives -> unit Machine.t end diff --git a/lib/bap_primus/bap_primus_lisp_context.ml b/lib/bap_primus/bap_primus_lisp_context.ml index 87cc45190..32b73927d 100644 --- a/lib/bap_primus/bap_primus_lisp_context.ml +++ b/lib/bap_primus/bap_primus_lisp_context.ml @@ -37,6 +37,10 @@ let of_project proj = Name.Map.of_alist_exn [ "endian", features [endian proj] ] +let create descs = + List.map descs ~f:(fun (name,xs) -> name,features xs) |> + Name.Map.of_alist_reduce ~f:Set.union + let merge xs ys : t = Map.merge xs ys ~f:(fun ~key:_ -> function | `Left v | `Right v -> Some v | `Both (x,y) -> Some (Feature.Set.union x y) ) diff --git a/lib/bap_primus/bap_primus_lisp_context.mli b/lib/bap_primus/bap_primus_lisp_context.mli index 89a178bd0..d92cc8d50 100644 --- a/lib/bap_primus/bap_primus_lisp_context.mli +++ b/lib/bap_primus/bap_primus_lisp_context.mli @@ -215,7 +215,7 @@ dynamic order. - - Do not introduce any mechanism but rely on the advice mechanism + - Do not introduce any mechanism but rely on the advice mechanism instead. In Common Lisp terminology this will only leave us with auxiliary methods, except that the after method allows us to override the return value. Thus, if someone would like to @@ -247,6 +247,8 @@ val t : t Attribute.t (** [of_project p] initializes a context from the project [p]. *) val of_project : project -> t +val create : (string * string list) list -> t + val empty : t diff --git a/lib/bap_primus/bap_primus_lisp_parse.ml b/lib/bap_primus/bap_primus_lisp_parse.ml index 911cace2f..57931ee10 100644 --- a/lib/bap_primus/bap_primus_lisp_parse.ml +++ b/lib/bap_primus/bap_primus_lisp_parse.ml @@ -51,7 +51,6 @@ type error = | Format_error of format_error * Loc.t | Sexp_error of string * source * Source.error | Unresolved_feature of string * source - | Unknown_attr of string * Loc.t exception Fail of error @@ -84,7 +83,7 @@ module Parse = struct let fails err s = raise (Parse_error (err,s)) let fail err s = fails err [s] let bad_form op got = fail (Bad_form op) got - let nil = {exp=0L; typ=Type.word 1} + let nil = {exp=Z.zero; typ=Type.word 1} let expand prog cs = @@ -721,8 +720,6 @@ let pp_error ppf err = match err with | Unresolved_feature (name,req) -> fprintf ppf "Error: no implementation provided for feature `%s' %a" name pp_request req - | Unknown_attr (attr,loc) -> - fprintf ppf "%a@\nError: unknown attribute %s@\n" Loc.pp loc attr | Format_error (err,loc) -> fprintf ppf "%a@\nFormat error: %a" Loc.pp loc pp_format_error err diff --git a/lib/bap_primus/bap_primus_lisp_program.ml b/lib/bap_primus/bap_primus_lisp_program.ml index 07c09a1aa..99463044f 100644 --- a/lib/bap_primus/bap_primus_lisp_program.ml +++ b/lib/bap_primus/bap_primus_lisp_program.ml @@ -51,6 +51,7 @@ let merge p1 p2 = p2 with sigs = p1.sigs @ p2.sigs; codes = p1.codes @ p2.codes; + context = Lisp.Context.merge p1.context p2.context; } @@ -161,7 +162,7 @@ let pp_term pp_exp ppf = function fprintf ppf "@[%a@]" pp_exp exp | {data={exp; typ}} -> fprintf ppf "@[%a:%a@]" pp_exp exp Lisp.Type.pp typ -let pp_word = pp_term Int64.pp +let pp_word = pp_term Z.pp_print let pp_var = pp_term String.pp let rec concat_prog p = diff --git a/lib/bap_primus/bap_primus_lisp_types.ml b/lib/bap_primus/bap_primus_lisp_types.ml index 2595c3532..06ac302c9 100644 --- a/lib/bap_primus/bap_primus_lisp_types.ml +++ b/lib/bap_primus/bap_primus_lisp_types.ml @@ -22,7 +22,7 @@ type typ = | Name of string | Type of int [@@deriving sexp, compare] type 'a term = {exp : 'a; typ : typ} [@@deriving compare] -type word = int64 term indexed [@@deriving compare] +type word = Z.t term indexed [@@deriving compare] type var = string term indexed [@@deriving compare] type sym = string indexed [@@deriving compare] type loc = Loc.t diff --git a/lib/bap_primus/bap_primus_lisp_word.ml b/lib/bap_primus/bap_primus_lisp_word.ml index 1bfe7c3a3..51e611fdc 100644 --- a/lib/bap_primus/bap_primus_lisp_word.ml +++ b/lib/bap_primus/bap_primus_lisp_word.ml @@ -8,13 +8,13 @@ type t = word [@@deriving compare] type read_error = Empty | Not_an_int | Unclosed | Bad_literal | Bad_type let char_of_string s = - try Ok Char.(Int64.of_int @@ to_int @@ of_string s) + try Ok Char.(Z.of_int @@ to_int @@ of_string s) with _ -> Error Bad_literal let read_char str = char_of_string (String.subo ~pos:1 str) let read_int str = - try Ok (Int64.of_string (String.strip str)) + try Ok (Z.of_string (String.strip str)) with _ -> Error Bad_literal let char id eq s = @@ -43,7 +43,7 @@ let read id eq x = | _ -> Error Bad_literal else Error Not_an_int -let sexp_of_word {data={exp}} = sexp_of_int64 exp +let sexp_of_word {data={exp}} = Sexp.Atom (Z.to_string exp) let sexp_of_t = sexp_of_word include Comparable.Make_plain(struct diff --git a/lib/bap_primus/bap_primus_machine.ml b/lib/bap_primus/bap_primus_machine.ml index 008d09cfd..d0e82c3a1 100644 --- a/lib/bap_primus/bap_primus_machine.ml +++ b/lib/bap_primus/bap_primus_machine.ml @@ -81,6 +81,7 @@ module Make(M : Monad.S) = struct type 'a e = ?boot:unit t -> ?init:unit t -> + ?fini:unit t -> (exit_status * project) m effect module C = Monad.Cont.Make(PE)(struct @@ -357,6 +358,7 @@ module Make(M : Monad.S) = struct fun user ?(boot=return ()) ?(init=return ()) + ?(fini=return ()) ?(envp=[||]) ?(args=[||]) sys @@ -367,7 +369,11 @@ module Make(M : Monad.S) = struct init >>= fun () -> catch (start sys >>= fun () -> user) - (fun exn -> stop sys >>= fun () -> raise exn) >>= fun x -> + (fun exn -> + fini >>= fun () -> + stop sys >>= fun () -> + raise exn) >>= fun x -> + fini >>= fun () -> stop sys >>= fun () -> return x in M.bind diff --git a/lib/bap_primus/bap_primus_memory.ml b/lib/bap_primus/bap_primus_memory.ml index eb2dac4eb..500354757 100644 --- a/lib/bap_primus/bap_primus_memory.ml +++ b/lib/bap_primus/bap_primus_memory.ml @@ -17,7 +17,12 @@ let () = Exn.add_printer (function Addr.pp_hex here) | _ -> None) -type dynamic = {base : addr; len : int; value : Generator.t } +type dynamic = { + lower : addr; + upper : addr; + value : Generator.t +} + type region = | Dynamic of dynamic | Static of mem @@ -45,8 +50,8 @@ module Descriptor = struct create addr_size data_size "unknown" let name d = d.name - - + let addr_size d = d.addr + let data_size d = d.size include Comparable.Make(struct type t = memory [@@deriving bin_io, compare, sexp] end) @@ -62,15 +67,13 @@ type t = { mems : state Descriptor.Map.t } -let zero = Word.of_int ~width:8 0 - let sexp_of_word w = Sexp.Atom (asprintf "%a" Word.pp_hex w) -let sexp_of_dynamic {base; len; value} = +let sexp_of_dynamic {lower; upper; value} = Sexp.(List [ Sexp.Atom "dynamic"; - sexp_of_word base; - sexp_of_int len; + sexp_of_word lower; + sexp_of_word upper; Generator.sexp_of_t value]) let sexp_of_mem mem = Sexp.List [ @@ -107,6 +110,17 @@ let inspect_memory {curr; mems} = Sexp.List [ Descriptor.Map.sexp_of_t inspect_state mems; ] +let inspect_generated (ptr,x) = Sexp.List [ + sexp_of_addr ptr; + sexp_of_value x; + ] + + +let generated,on_generated = + Bap_primus_observation.provide "load-generated" + ~inspect:inspect_generated + ~package:"bap" + let virtual_memory arch = let module Target = (val target_of_arch arch) in @@ -128,11 +142,10 @@ let state = Bap_primus_machine.State.declare curr = virtual_memory (Project.arch p); } -let inside {base;len} addr = - let high = Word.(base ++ len) in - if Addr.(high < base) - then Addr.(addr >= base) || Addr.(addr < high) - else Addr.(addr >= base) && Addr.(addr < high) +let inside {lower; upper} addr = + if Addr.(lower <= upper) + then Addr.(addr >= lower) && Addr.(addr <= upper) + else Addr.(addr >= upper) || Addr.(addr <= lower) let find_layer addr = List.find ~f:(function | {mem=Dynamic mem} -> inside mem addr @@ -219,26 +232,50 @@ module Make(Machine : Machine) = struct if size >= 8 then read start size else read_small mem base size - let remembered {values; layers} addr value = - put_curr { - layers; - values = Map.set values ~key:addr ~data:value; - } >>| fun () -> - value - + let store_word arch bytesize ~addr word values = + let bytes = (Word.bitwidth word + bytesize - 1) / bytesize in + let bite x = Word.extract_exn ~hi:(bytesize-1) x in + let shift = let bits = Word.of_int ~width:8 bytesize in + fun x -> Word.lshift x bits in + let addr,next = match Arch.endian arch with + | LittleEndian -> addr,Addr.succ + | BigEndian -> Addr.nsucc addr (bytes-1),Addr.pred in + let notify_if_generated key x values = + if not (Map.mem values key) + then Machine.Observation.make on_generated (key,x) + else Machine.return () in + let rec loop written ~key word values = + if written < bytes then + Value.of_word (bite word) >>= fun data -> + notify_if_generated key data values >>= fun () -> + loop + (written+1) + ~key:(next key) + (shift word) + (Map.update values key ~f:(function + | None -> data + | Some data -> data)) + else Machine.return values in + loop 0 ~key:addr word values + + let remembered {values; layers} addr word = + memory >>= fun {size} -> + Machine.gets Project.arch >>= fun arch -> + store_word arch size addr word values >>= fun values -> + put_curr {layers; values} >>| fun () -> + Map.find_exn values addr let read addr {values;layers} = match find_layer addr layers with | None -> pagefault addr | Some layer -> match Map.find values addr with | Some v -> Machine.return v | None -> - let read_value = - memory >>= fun {size} -> - match layer.mem with - | Dynamic {value} -> - Generate.next value >>= Value.of_int ~width:8 - | Static mem -> Value.of_word (read_word mem addr size) in - read_value >>= remembered {values; layers} addr + memory >>= fun {size} -> + match layer.mem with + | Static mem -> Value.of_word (read_word mem addr size) + | Dynamic {value=g} -> + Generate.word g (Generator.width g) >>= + remembered {values; layers} addr let write addr value {values;layers} = match find_layer addr layers with @@ -249,34 +286,47 @@ module Make(Machine : Machine) = struct values = Map.set values ~key:addr ~data:value; } + let add_layer layer t = {t with layers = layer :: t.layers} let (++) = add_layer - let initialize values base len f = - Machine.Seq.fold (Seq.range 0 len) ~init:values ~f:(fun values i -> - let addr = Addr.(base ++ i) in - f addr >>= fun data -> - Value.of_word data >>| fun data -> - Map.set values ~key:addr ~data) - - + let initialize values lower upper f = + let rec loop values addr = + if addr < upper + then f addr >>= fun data -> + Value.of_word data >>= fun data -> + loop (Map.set values ~key:addr ~data) (Addr.succ addr) + else Machine.return values in + loop values lower - let allocate + let add_region ?(readonly=false) ?(executable=false) ?init - ?(generator=Generator.Random.Seeded.byte) - base len = + ?generator + ~lower ~upper () = + Machine.gets Project.arch >>= fun arch -> + let width = Arch.addr_size arch |> Size.in_bits in get_curr >>| add_layer { perms={readonly; executable}; - mem = Dynamic {base;len; value=generator} + mem = Dynamic {lower;upper; value = match generator with + | Some g -> g + | None -> Generator.Random.Seeded.lcg ~width ()} } >>= fun s -> match init with | None -> put_curr s | Some f -> - initialize s.values base len f >>= fun values -> + initialize s.values lower upper f >>= fun values -> put_curr {s with values} + + let allocate + ?readonly ?executable ?init ?generator base len = + add_region () + ?readonly ?executable ?init ?generator + ~lower:base + ~upper:(Addr.nsucc base (len-1)) + let map ?(readonly=false) ?(executable=false) mem = update state @@ add_layer ({mem=Static mem; perms={readonly; executable}}) let add_text mem = map mem ~readonly:true ~executable:true @@ -290,6 +340,11 @@ module Make(Machine : Machine) = struct write addr value >>= put_curr + let del addr = update state @@ fun s -> { + s with values = Map.remove s.values addr + } + + let load addr = get addr >>| Value.to_word let store addr value = Value.of_word value >>= set addr diff --git a/lib/bap_primus/bap_primus_memory.mli b/lib/bap_primus/bap_primus_memory.mli index 5df7d4234..913d2dd33 100644 --- a/lib/bap_primus/bap_primus_memory.mli +++ b/lib/bap_primus/bap_primus_memory.mli @@ -4,6 +4,8 @@ open Bap_primus_types module Generator = Bap_primus_generator +val generated : (addr * value) Bap_primus_observation.t + type exn += Pagefault of addr type memory module Descriptor : sig @@ -12,7 +14,8 @@ module Descriptor : sig val create : addr_size:int -> data_size:int -> string -> memory val unknown : addr_size:int -> data_size:int -> memory val name : memory -> string - + val addr_size : memory -> int + val data_size : memory -> int include Comparable.S with type t := memory end @@ -26,10 +29,18 @@ module Make(Machine : Machine) : sig val get : addr -> value Machine.t val set : addr -> value -> unit Machine.t + val del : addr -> unit Machine.t val add_text : mem -> unit Machine.t val add_data : mem -> unit Machine.t + val add_region : + ?readonly:bool -> + ?executable:bool -> + ?init:(addr -> word Machine.t) -> + ?generator:Generator.t -> + lower:addr -> upper:addr -> unit -> unit Machine.t + val allocate : ?readonly:bool -> ?executable:bool -> diff --git a/lib/bap_primus/bap_primus_pos.ml b/lib/bap_primus/bap_primus_pos.ml index 82eae438c..fd2b2d153 100644 --- a/lib/bap_primus/bap_primus_pos.ml +++ b/lib/bap_primus/bap_primus_pos.ml @@ -54,7 +54,7 @@ let () = Exn.add_printer (function No transition is defined from the %s level to the %s level" (to_string level) (string_of_sexp (sexp_of_name dst)) - | exn -> None) + | _ -> None) let accept level args = Ok (level args) let reject level dst = Error (Broken_invariant {level; dst}) @@ -63,7 +63,7 @@ let reject level dst = Error (Broken_invariant {level; dst}) let level name f x = Sexp.List [ Sexp.Atom name; Sexp.Atom (f x) -] + ] let (>>) = Fn.compose let leaf name str t = Sexp.List [ Sexp.Atom name; @@ -79,6 +79,13 @@ let sexp_of_t = function | Def {me} -> leaf "def" Def.to_string me | Jmp {me} -> leaf "jmp" Jmp.to_string me +let parent prog blk = + Term.enum sub_t prog |> + Seq.find ~f:(fun sub -> + Option.is_some @@ Term.find blk_t sub (Term.tid blk)) |> + function None -> assert false + | Some sub -> sub + let next level cls t = let reject = reject level in Term.switch cls t @@ -94,6 +101,7 @@ let next level cls t = | _ -> reject `arg) ~blk:(fun me -> match level with | Jmp {up={up}} | Sub up | Arg {up} -> accept blk {me;up} + | Top ({me=prog} as top) -> accept blk {me; up={me=parent prog me; up=top} } | _ -> reject `blk) ~phi:(fun me -> match level with | Blk up | Phi {up} -> accept phi {me;up} diff --git a/lib/bap_primus/bap_primus_random.ml b/lib/bap_primus/bap_primus_random.ml index 81f745747..9a90dffe5 100644 --- a/lib/bap_primus/bap_primus_random.ml +++ b/lib/bap_primus/bap_primus_random.ml @@ -1,157 +1,194 @@ open Core_kernel -open Bap_primus_types - module Iterator = Bap_primus_iterator module type S = Iterator.Infinite.S -module LCG = struct - module type S = sig - include S with type dom = int - val create : dom -> t +(* Taken from arXiv:2001.05304 *) +let mcg16 = "0x7dc5" +let mcg32 = "0xae3cc725" +let mcg64 = "0xcc62fceb9202faad" +let mcg128 = "0xace2628409311ff16a545ebdff0d414d" + +(* Multiplicative Congruental Generator with power of two moduli. + + A generator with modulus m=2^s generates s-3 bits of + pseudorandomness with the period m/4, given that the seed is an odd + number. + + To build an p-bit generator we use k r-bit sub-generators, where k + is $ceil (p / (r-3))$. Each generator is having a different seed + obtained from the seed provided to the p-bit generator. +*) +module MCG = struct + module type Size = sig + val size : int end - module M31 = struct - type t = int - type dom = int - type seed = int - let a = 0x41C64E6D - let c = 12345 - let m = 31 - let min = 0 - let max = 1 lsl m - 1 - let next x = (a * x + c) mod (max + 1) - let create seed = next seed - let value = ident + module type S = sig + include S with type dom = Bitvec.t + include Size + val create : int -> t end - let t = Iterator.Infinite.create (module M31) - include M31 -end -module Unit = struct + module type Z = Bitvec.S with type 'a m = 'a - module type S = sig - include S with type dom = float - type u - val create : u -> t - end - module Make(Rng : Iterator.Infinite.S with type dom = int) - : S with type u = Rng.t = - struct - module Gen = struct - type dom = float - type u = Rng.t - type t = { - base : u; - value : float; - } - let factor = 1. /. (float Rng.max -. float Rng.min +. 1.) - - let rec next {base;value} = - let base = Rng.next base in - let value = - (float (Rng.value base) -. float Rng.min) *. factor in - if Float.(value < 1.) then {base; value} - else next {base;value} - - let value t = t.value - let min = 0.0 - let max = 1.0 - let create base = next {base ; value=1.0} - end - let t = Iterator.Infinite.create (module Gen) - include Gen - end - include Make(LCG) -end + let ceil_div m n = (m + n - 1) / n + let odd_hash seed = max (Hashtbl.hash seed * 2 + 1) 1 -module Geometric = struct + module Make(Z : Z)(P : sig val m : int val a : string end) : S = struct + module Z = Z + let a = Bitvec.of_string P.a + let size = P.m - 3 + type t = Bitvec.t + type dom = Bitvec.t - module type Dom = sig - include Floatable - val max_value : t - end + let noise = Z.int 3 + let min = Z.zero + let max = Z.(ones lsr noise) + let value x = Z.(x lsr noise) + let next x : t = Z.(a * x) + let create seed = next @@ Z.int @@ odd_hash seed - module type S = sig - include S - type u - val create : p:float -> u -> t - val param : t -> float end - module Make - (Dom : Dom) - (Uniform : Iterator.Infinite.S with type dom = int) : - S with type u = Uniform.t - and type dom = Dom.t = struct - module Gen = struct - type dom = Dom.t - type u = Uniform.t - module Unit = Unit.Make(Uniform) - type t = { - rng : Unit.t; - value : dom; - log1mp : float; - p : float; - } - - let next t = - let rng = Unit.next t.rng in - let x = 1.0 -. Unit.value rng in - let y = Float.round (log x /. t.log1mp) in - if Float.(y >= Dom.to_float Dom.max_value) - then {t with rng; value = Dom.max_value} - else {t with rng; value = Dom.of_float y} - - let create ~p rng = - let open Float in - if p < 0. || p > 1. - then invalid_arg - "Geometric distribution: \ - parameter p must be in (0,1] interval"; - let log1mp = Float.log1p(-.p) in - if log1mp = 0.0 then invalid_arg - "Geometric distribution: \ - parameter p is too small"; - next { - rng = Unit.create rng; - value = Dom.of_float 0.; - log1mp; - p; - } - - let value t = t.value - - let min = Dom.of_float 0. - let max = Dom.max_value - let param t = t.p - end - let t = Iterator.Infinite.create (module Gen) - include Gen + module Bitvec_M16 = + Bitvec.Make(struct let modulus = Bitvec.modulus 16 end) + + (* Pre: Output.Size > Sub.size *) + module Cat(Output : Size)(Sub : S) : S = struct + type t = Sub.t array + type dom = Bitvec.t + + module Z = Bitvec.Make(struct + let modulus = Bitvec.modulus Output.size + end) + + let size = Output.size + let min = Bitvec.zero + let max = Z.ones + let generators = ceil_div Output.size Sub.size + let noise = Output.size - generators + + let create seed : t = + Array.init generators (fun salt -> + Sub.create (seed + salt)) + + let next = Array.map ~f:Sub.next + + let value xs = + Array.fold ~f:(fun y x -> + Z.(y lsl int Sub.size lor Sub.value x)) ~init:Z.zero xs end - module Float = Make(Float)(LCG) - module Int = Make(Int)(LCG) -end + (* Pre: Output.Size < Sub.size *) + module Cut(Output : Size)(Sub : S) : S = struct + type t = Sub.t + type dom = Sub.dom + module Z = Bitvec.Make(struct + let modulus = Bitvec.modulus Output.size + end) + let min = Bitvec.zero + let max = Z.ones + let size = Output.size + let noise = Z.int @@ Sub.size - Output.size + let next = Sub.next + let value x = Z.(Sub.value x lsr noise) + let create = Sub.create + end -module Byte = struct - module type S = sig - include Iterator.Infinite.S with type dom = int - type rng - val create : rng -> t + module type Range = sig + include Size + val min : Bitvec.t + val max : Bitvec.t end - module Make(Rng : Iterator.Infinite.S with type dom = int) - = struct - type dom = int - type rng = Rng.t - type t = Rng.t - - let min = 0 - let max = 255 - let size = max - min + 1 - let create = ident - let next = Rng.next - let value rng = Rng.value rng mod size + + + (* pre: + - R.size >= Gen.size + - Gen.size = 2^(max-min+1) + - Gen.min = 0 + - Gen.max = 2^Gen.size + *) + module Range(R : Range)(Gen : S) = struct + include Gen + module Z = Bitvec.Make(struct + let modulus = Bitvec.modulus R.size + end) + let value x = + let u = Gen.value x in + Z.(R.min + u % (R.max-R.min+one)) + let min = R.min + let max = R.max + let size = R.size end - module Basic = Make(LCG) - include Basic + + (* Basis Generators *) + module M13 = Make(Bitvec_M16)(struct let m = 16 let a = mcg16 end) + module M29 = Make(Bitvec.M32)(struct let m = 32 let a = mcg32 end) + module M61 = Make(Bitvec.M64)(struct let m = 64 let a = mcg64 end) + + (* Common Generators *) + module M8 = Cut(struct let size = 8 end)(M13) + module M16 = Cut(struct let size = 16 end)(M29) + module M32 = Cut(struct let size = 32 end)(M61) + module M64 = Cat(struct let size = 64 end)(M29) + + let tabulate (module Gen : S) ~n seed = + let rec loop i g = + if i < n then begin + Format.printf "%3d: %a@\n" i Bitvec.pp (Gen.value g); + loop (i+1) (Gen.next g) + end in + loop 0 (Gen.create seed) + + let tabulate_ints (module Gen : S) ~n seed = + let rec loop i g = + if i < n then begin + Format.printf "%3d: %2ld@\n" i (Bitvec.to_int32 (Gen.value g)); + loop (i+1) (Gen.next g) + end in + loop 0 (Gen.create seed) + + let cut m (module G : S) : (module S) = + (module Cut(struct let size = m end)(G)) + + let cat m (module G : S) : (module S) = + (module Cat(struct let size = m end)(G)) + + let make_for_width : int -> (module S) = function + | 8 -> (module M8) + | 13 -> (module M13) + | 16 -> (module M16) + | 29 -> (module M29) + | 32 -> (module M32) + | 64 -> (module M64) + | n when n < 13 -> cut n (module M13) + | n when n < 29 -> cut n (module M29) + | n when n < 61 -> cut n (module M61) + | n -> cat n (module M61) + + let create ?min ?max width = + if Option.is_none min && Option.is_none max + then make_for_width width + else + let module Z = Bitvec.Make(struct + let modulus = Bitvec.modulus width + end) in + let module R = struct + let min = match min with + | None -> Bitvec.zero + | Some min -> min + let max = match max with + | None -> Z.ones + | Some max -> max + let size = width + end in + let bits = Bitvec.to_int Z.(R.max - R.min + one) in + let module Gen = (val make_for_width bits) in + (module Range(R)(Gen)) + + let create_small ?min ?max width = + let int x = Bitvec.(int x mod modulus width) in + let min = Option.map ~f:int min + and max = Option.map ~f:int max in + create ?min ?max width end diff --git a/lib/bap_primus/bap_primus_random.mli b/lib/bap_primus/bap_primus_random.mli index ac14e4aa5..88140041b 100644 --- a/lib/bap_primus/bap_primus_random.mli +++ b/lib/bap_primus/bap_primus_random.mli @@ -1,57 +1,17 @@ -open Core_kernel - module Iterator = Bap_primus_iterator - -module LCG : sig - module type S = sig - include Iterator.Infinite.S with type dom = int - val create : dom -> t - end - include S -end - - -module Unit : sig +module MCG : sig module type S = sig - include Iterator.Infinite.S with type dom = float - type u - val create : u -> t + include Iterator.Infinite.S with type dom = Bitvec.t + val size : int + val create : int -> t end - module Make (U : Iterator.Infinite.S with type dom = int) - : S with type u = U.t - include S with type u = LCG.t -end -module Geometric : sig - module type S = sig - include Iterator.Infinite.S - type u - val create : p:float -> u -> t - val param : t -> float - end + val create : ?min:Bitvec.t -> ?max:Bitvec.t -> int -> (module S) + val create_small : ?min:int -> ?max:int -> int -> (module S) - module type Dom = sig - include Floatable - val max_value : t - end - - module Make(D : Dom)(U : Iterator.Infinite.S with type dom = int) : - S with type dom = D.t and type u = U.t - - module Float : S with type dom = float and type u = LCG.t - module Int : S with type dom = int and type u = LCG.t -end - - - -module Byte : sig - module type S = sig - include Iterator.Infinite.S with type dom = int - type rng - val create : rng -> t - end - module Make(Rng : Iterator.Infinite.S with type dom = int) - : S with type rng = Rng.t - include S with type rng = LCG.t + module M8 : S + module M16 : S + module M32 : S + module M64 : S end diff --git a/lib/bap_primus/bap_primus_system.ml b/lib/bap_primus/bap_primus_system.ml index a04ca4c77..d934e1bde 100644 --- a/lib/bap_primus/bap_primus_system.ml +++ b/lib/bap_primus/bap_primus_system.ml @@ -8,6 +8,9 @@ module Info = Bap_primus_info module Observation = Bap_primus_observation module Machine = Bap_primus_machine + +let package = "bap" + let fini,finish = Observation.provide ~inspect:sexp_of_unit "fini" ~desc:"Occurs when machine finishes." @@ -47,7 +50,7 @@ module Repository = struct let require name = match Hashtbl.find self name with | Some sys -> sys - | None -> failwithf "Unknown system %s" (Name.show name) () + | None -> invalid_argf "Unknown system %s" (Name.show name) () let get ?package name = require @@ Name.create ?package name @@ -151,6 +154,7 @@ module Components = struct module Generic(Machine : Machine) = struct open Machine.Syntax module Lisp = Bap_primus_lisp.Make(Machine) + module Context = Bap_primus_lisp_context let inited () = Machine.Observation.make inited () @@ -158,8 +162,14 @@ module Components = struct let finish () = Machine.Observation.make finish () - let do_init system loaded = - let comps = Set.diff (components system) loaded in + let do_init s loaded = + let comps = Set.diff (components s) loaded in + let context = Context.create [ + "system", [Knowledge.Name.show s.name]; + "component", Set.to_list (components s) |> + List.map ~f:Knowledge.Name.show + ] in + Lisp.refine context >>= fun () -> Set.to_list comps |> Machine.List.iter ~f:(fun name -> match Hashtbl.find generics name with @@ -170,30 +180,29 @@ module Components = struct failwithf "failed to find a component %s \ required for system %s" (Name.show name) - (Name.show system.name) + (Name.show s.name) ()) let init_system s = do_init s (Set.empty (module Name)) - let run_internal ~boot ~init ~start = + let run_internal ~boot ~init ~fini ~start = Machine.run ~boot ~init:(Lisp.typecheck >>= Lisp.optimize >>= fun () -> init >>= inited) - @@begin Machine.catch start (fun exn -> - finish () >>= fun () -> - Machine.raise exn) >>= fun () -> - finish () - end + ~fini:(fini >>= finish) + start + let run ?envp ?args ?(init=Machine.return ()) + ?(fini=Machine.return ()) ?(start=Machine.return ()) sys proj = run_internal (Name.show sys.name) proj - ?envp ?args ~boot:(init_system sys) ~init ~start + ?envp ?args ~boot:(init_system sys) ~init ~fini ~start end @@ -228,6 +237,7 @@ module Components = struct let run ?envp ?args ?(init=Machine.return ()) + ?(fini=Machine.return ()) ?(start=Machine.return ()) sys proj state = let comp = @@ -238,6 +248,7 @@ module Components = struct ?args ~boot:(init_system sys) ~init + ~fini ~start >>= fun x -> Knowledge.provide result obj (Some x) >>| fun () -> obj in @@ -286,10 +297,10 @@ module Parser = struct let empty name = {name; desc=""; components=[]; depends_on=[]} let comp name s = - {s with components = Name.read name :: s.components} + {s with components = Name.read ~package name :: s.components} let deps name s = - {s with depends_on = Name.read name :: s.depends_on} + {s with depends_on = Name.read ~package name :: s.depends_on} let rec parse_specs push : t -> Sexp.t list -> (t,error) Result.t = fun sys -> function @@ -328,7 +339,7 @@ module Parser = struct let of_sexp : Sexp.t -> (t,error_with_loc) Result.t = function | List (Atom "defsystem" :: Atom name :: items) -> - parse_items (empty (Name.read name)) items |> + parse_items (empty (Name.read ~package name)) items |> Result.map_error ~f:(in_system name) | other -> Error (in_system "unknown" {expects=Defsystem; got=other}) @@ -383,6 +394,7 @@ module Job = struct envp : string array; args : string array; init : unit Machine.Make(Knowledge).t; + fini : unit Machine.Make(Knowledge).t; start : unit Machine.Make(Knowledge).t; system : system; } [@@deriving fields] @@ -394,14 +406,15 @@ module Job = struct ?(desc="") ?(envp=[||]) ?(args=[||]) ?(init=Analysis.return ()) + ?(fini=Analysis.return ()) ?(start=Analysis.return ()) - system = {name; desc; envp; args; init; start; system} + system = {name; desc; envp; args; init; fini; start; system} end module Jobs = struct let jobs : Job.t Queue.t = Queue.create () - let enqueue ?name ?desc ?envp ?args ?init ?start sys = - Queue.enqueue jobs @@ Job.create ?name ?desc ?envp ?args ?init ?start sys + let enqueue ?name ?desc ?envp ?args ?init ?fini ?start sys = + Queue.enqueue jobs @@ Job.create ?name ?desc ?envp ?args ?init ?fini ?start sys let pending () = Queue.length jobs @@ -434,20 +447,22 @@ module Jobs = struct let run ?(on_failure = fun _ _ _ -> Continue) ?(on_success = fun _ _ _ _ -> Continue) = - let rec process result ({Job.envp; args; init; start; system} as job) = + let rec process result ({Job.envp; args; init; fini; start; system} as job) = Components.run system result.project result.state - ~envp ~args ~init ~start |> function + ~envp ~args ~init ~fini ~start |> function | Ok (status,proj,state) -> - handle_success job status proj state result - | Error conflict -> - handle_failure job conflict result - and handle_success job status proj state result = + handle_success job status state @@ + success job proj state result + | Error problem -> + handle_failure job problem @@ + conflict job problem result + and handle_success job status state result = match on_success job status state result with - | Continue -> continue (success job proj state result) + | Continue -> continue result | Stop -> result and handle_failure job problem result = match on_failure job problem result with - | Continue -> continue (conflict job problem result) + | Continue -> continue result | Stop -> result and continue result = match Queue.dequeue jobs with | None -> result diff --git a/lib/bap_primus/bap_primus_system.mli b/lib/bap_primus/bap_primus_system.mli index 03ec5802c..41b4b43a9 100644 --- a/lib/bap_primus/bap_primus_system.mli +++ b/lib/bap_primus/bap_primus_system.mli @@ -64,6 +64,7 @@ module Generic(Machine : Bap_primus_types.Machine) : sig ?envp:string array -> ?args:string array -> ?init:unit Machine.t -> + ?fini:unit Machine.t -> ?start:unit Machine.t -> t -> project -> (exit_status * project) Machine.m end @@ -72,6 +73,7 @@ val run : ?envp:string array -> ?args:string array -> ?init:unit Bap_primus_machine.Make(Knowledge).t -> + ?fini:unit Bap_primus_machine.Make(Knowledge).t -> ?start:unit Bap_primus_machine.Make(Knowledge).t -> t -> project -> Knowledge.state -> (exit_status * project * Knowledge.state, Knowledge.conflict) result @@ -98,6 +100,7 @@ module Jobs : sig ?envp:string array -> ?args:string array -> ?init:unit Bap_primus_machine.Make(Knowledge).t -> + ?fini:unit Bap_primus_machine.Make(Knowledge).t -> ?start:unit Bap_primus_machine.Make(Knowledge).t -> system -> unit val pending : unit -> int diff --git a/lib/bap_primus/bap_primus_types.ml b/lib/bap_primus/bap_primus_types.ml index dff7ea6b6..8b84cf82a 100644 --- a/lib/bap_primus/bap_primus_types.ml +++ b/lib/bap_primus/bap_primus_types.ml @@ -66,6 +66,7 @@ module type Machine = sig and type 'a e = ?boot:unit t -> ?init:unit t -> + ?fini:unit t -> (exit_status * project) m effect module Local : State with type 'a m := 'a t and type 'a t := 'a state diff --git a/lib/bap_primus/bap_primus_value.ml b/lib/bap_primus/bap_primus_value.ml index 6f1b0f66d..fda7d3722 100644 --- a/lib/bap_primus/bap_primus_value.ml +++ b/lib/bap_primus/bap_primus_value.ml @@ -133,13 +133,13 @@ module Make(Machine : Machine) = struct module Symbol = struct let to_value sym = - Machine.Local.get symbols >>= fun index -> + Machine.Global.get symbols >>= fun index -> let index = Index.register index sym in - Machine.Local.put symbols index >>| fun () -> + Machine.Global.put symbols index >>| fun () -> Index.key index sym let of_value value = - Machine.Local.get symbols >>| fun index -> + Machine.Global.get symbols >>| fun index -> Index.string index value end diff --git a/lib/bap_primus_track_visited/bap_primus_track_visited.ml b/lib/bap_primus_track_visited/bap_primus_track_visited.ml new file mode 100644 index 000000000..1749085b9 --- /dev/null +++ b/lib/bap_primus_track_visited/bap_primus_track_visited.ml @@ -0,0 +1,130 @@ +open Core_kernel +open Bap.Std +open Bap_primus.Std + +type state = { + visited : Tid.Set.t; + total : int; +} + +let count_blks p = (object + inherit [int] Term.visitor + method! enter_blk _ bs = bs + 1 +end)#run p 0 + + +let init_visited prog = + (object inherit [Tid.Set.t] Term.visitor + method! enter_blk blk visited = + if Term.has_attr blk Term.visited + then Set.add visited (Term.tid blk) + else visited + end)#run prog Tid.Set.empty + +let state = Primus.Machine.State.declare + ~name:"primus-track-visited" + ~uuid:"6edf3c44-3665-4ec1-8537-ef7fbba78d3d" @@ fun p -> { + visited = init_visited (Project.program p); + total = count_blks (Project.program p) + } + +type marker = { mark : 'a. 'a term -> 'a term} + +let dead = {mark = fun t -> Term.set_attr t Term.dead ()} +let live = {mark = fun t -> + Term.set_attr (Term.del_attr t Term.dead) Term.visited () + } + +let mark_block {mark} t = + mark t |> + Term.map def_t ~f:mark |> + Term.map jmp_t ~f:mark + +let marker p marker = object + inherit Term.mapper + method! map_blk t = + if not (p t) then t + else mark_block marker t +end + +let unvisited t = not (Term.has_attr t Term.visited) +let is_mem xs x = Set.mem xs (Term.tid x) + +let progress,report_progress = + Primus.Observation.provide "visited-blocks" + ~inspect:[%sexp_of:int * int] + ~desc:"visited-blocks (visited,total) is posted every time \ + a new basic block is visited, where [visited] is the \ + number of already visited blocks and [total] \ + is the total number of blocks in the program." + +module Tracker(Machine : Primus.Machine.S) = struct + open Machine.Syntax + + module Linker = Primus.Linker.Make(Machine) + + let visit t = + Machine.Global.get state >>= fun s -> + let s = { + s with + visited = Set.add s.visited (Term.tid t) + } in + Machine.Observation.post report_progress ~f:(fun k -> + k (Set.length s.visited, s.total)) >>= fun () -> + Machine.Global.put state s + + let visit_stub (name,_) = + Linker.resolve_tid (`symbol name) >>= function + | None -> Machine.return () + | Some tid -> Machine.gets Project.program >>= fun prog -> + match Term.find sub_t prog tid with + | None -> Machine.return () + | Some sub -> + Term.enum blk_t sub |> + Machine.Seq.iter ~f:visit + + let mark_live _ = + Machine.Global.get state >>= fun {visited} -> + Machine.update (fun proj -> + let marker = marker (is_mem visited) live in + Project.with_program proj @@ + marker#run (Project.program proj)) + + let mark_dead _ = + Machine.update (fun proj -> + let marker = marker unvisited dead in + Project.with_program proj @@ + marker#run (Project.program proj)) + + let init () = + Machine.sequence [ + Primus.Interpreter.enter_blk >>> visit; + Primus.System.stop >>> mark_live; + Primus.Linker.Trace.lisp_call >>> visit_stub; + Primus.System.start >>> mark_dead; + ] +end + +module Set = struct + module Make(Machine : Primus.Machine.S) = struct + open Machine.Syntax + + let all = Machine.Local.get state >>| fun s -> s.visited + let mem t = all >>| fun s -> Set.mem s t + + let add t = Machine.Local.update state ~f:(fun s -> + {s with visited = Set.add s.visited t}) + + let del t = Machine.Local.update state ~f:(fun s -> + {s with visited = Set.remove s.visited t}) + end +end + +let init () = + Primus.Components.register_generic "mark-visited" (module Tracker) + ~package:"bap" + ~desc:"Marks visited (by Primus) program terms with the \ + [Term.visited] attribute and unvisited with the \ + [Term.dead] attribute. Note, that the attributes \ + are attached only when the system exits"; + Primus.Machine.add_component (module Tracker) [@warning "-D"] diff --git a/lib/bap_primus_track_visited/bap_primus_track_visited.mli b/lib/bap_primus_track_visited/bap_primus_track_visited.mli new file mode 100644 index 000000000..b65602e08 --- /dev/null +++ b/lib/bap_primus_track_visited/bap_primus_track_visited.mli @@ -0,0 +1,90 @@ +open Bap.Std +open Bap_primus.Std + + +(** Tracks program terms evaluated by Primus. + + This module provides a component and an interface to the + visitation tracker that keeps records of all basic block terms + visited during Primus evaluation. + + During the initialization the component adds all basic blocks that have + the [visited] attribute to the list of already visited blocks. This + is done only when the system starts and the visited set is not + synchronized anymore. Also, when a Primus system is started, the + component will mark with the [dead] attribute all terms that are + not already marked with with the [visited] attribute. + + Finally, when the system is stopped, the component will update the + product data structure and mark all terms that was visited during + the system run with the [visited] attribute. + + Although the visitation tracks only basic blocks it adds the + [visited] and [dead] attributes to all subterms of a visited + block. + + If a function is stubbed then when a stub is invoked the whole + body of a function is also marked as visited (and the blocks of + the function are added to the visited set). +*) + + +(** initializes the tracker component. + + This function is called by the [primus-mark-visited] component, + and is not necessary to call, unless this plugin is not used. +*) +val init : unit -> unit + + +(** [progress (visited,total)] is posted every time a Primus machine + makes progress and evaluates a previously unvisited basic block. + + [visited] - is the total number of visited basic blocks; + [total] - is the total number of blocks in the program. +*) +val progress : (int * int) Primus.observation + +(** The online interface to the set of visited basic blocks. + + {3 Example} + + {[ + module Visited = Bap_primus_track_visited.Set.Make(Machine) + + let term_is_visited t = Visited.mem (Term.tid t) + ]} +*) +module Set : sig + + module Make(Machine : Primus.Machine.S) : sig + + (** [mem tid] is if a term with [tid] was visited. + + A term with the term identifier [tid] is visited if some + machine posted an [enter-term] event with this [tid], or + if it was marked with the [visited] attribute, or if it + was forcefully added to the visited set with the [add] + function. + *) + val mem : tid -> bool Machine.t + + + (** [add tid] forcefully adds [tid] to the set of visited terms. + + Does nothing if tid is already visited. + *) + val add : tid -> unit Machine.t + + + (** [del tid] forcefully removes [tid] from the set of visited terms. + + Does nothing if it wasn't visited. + *) + val del : tid -> unit Machine.t + + + (** [all] is the current set of all visited basic blocks. *) + val all : Tid.Set.t Machine.t + end +end diff --git a/oasis/glibc-runtime b/oasis/glibc-runtime new file mode 100644 index 000000000..949855c9d --- /dev/null +++ b/oasis/glibc-runtime @@ -0,0 +1,13 @@ +Flag glibc_runtime + Description: Builds glibc runtime supporing code + Default: false + +Library glibc_runtime_plugin + Build$: flag(everything) || flag(glibc_runtime) + Path: plugins/glibc_runtime + FindlibName: bap-plugin-glibc_runtime + CompiledObject: best + BuildDepends: base, bap-main, bap, bap-abi, bap-c + InternalModules: Glibc_runtime_main + XMETADescription: detects main and libc_start_main functions + XMETAExtraLines: tags="abi, pass" diff --git a/oasis/primus b/oasis/primus index 9346bff2b..e98655130 100644 --- a/oasis/primus +++ b/oasis/primus @@ -9,7 +9,8 @@ Library bap_primus FindlibName: bap-primus CompiledObject: best BuildDepends: bap, bap-abi, bap-c, uuidm, bap-future, parsexp, bap-strings, - core_kernel, ppx_jane, regular, monads, graphlib, bap-knowledge + core_kernel, ppx_jane, regular, monads, graphlib, bap-knowledge, + zarith, bitvec, zarith Modules: Bap_primus InternalModules: Bap_primus_env, diff --git a/oasis/primus-lisp b/oasis/primus-lisp index 92dd1b1c1..ec8777406 100644 --- a/oasis/primus-lisp +++ b/oasis/primus-lisp @@ -6,14 +6,16 @@ Flag primus_lisp Library primus_lisp_library_plugin Build$: flag(everything) || flag(primus_lisp) Path: plugins/primus_lisp - BuildDepends: bap-primus, core_kernel, bap, ppx_jane, monads, regular + BuildDepends: bap-primus, core_kernel, bap, ppx_jane, monads, regular, + bap-knowledge, bap-main FindlibName: bap-plugin-primus_lisp CompiledObject: best InternalModules: Primus_lisp_main, Primus_lisp_config, Primus_lisp_primitives, Primus_lisp_ieee754, - Primus_lisp_io + Primus_lisp_io, + Primus_lisp_run XMETADescription: install and load Primus lisp libraries DataFiles: lisp/*.lisp ($primus_lisp_library_path) XMETAExtraLines: tags="primus, lisp" diff --git a/oasis/primus-random b/oasis/primus-random new file mode 100644 index 000000000..832605186 --- /dev/null +++ b/oasis/primus-random @@ -0,0 +1,14 @@ +Flag primus_random + Description: Build Primus randomization components + Default: false + +Library primus_random_library_plugin + Build$: flag(everything) || flag(primus_random) + Path: plugins/primus_random + BuildDepends: bap-primus, bap, core_kernel, ppx_jane, bap-main, + bitvec, bitvec-sexp, zarith + FindlibName: bap-plugin-primus_random + CompiledObject: best + InternalModules: Primus_random_main + XMETADescription: primus randomization components + XMETAExtraLines: tags="primus" \ No newline at end of file diff --git a/oasis/primus-support b/oasis/primus-support index a0031ab44..104b7a9fd 100644 --- a/oasis/primus-support +++ b/oasis/primus-support @@ -73,17 +73,27 @@ Library primus_print_plugin Modules: Primus_print_main XMETAExtraLines: tags="primus, printer" + +Library bap_primus_track_visited + Path: lib/bap_primus_track_visited + Build$: flag(everything) || flag(primus_support) + FindlibName: bap-primus-track-visited + CompiledObject: best + BuildDepends: bap-primus, bap, core_kernel, ppx_jane + XMETADescription: tracks basic blocks visited by Primus + Modules: Bap_primus_track_visited + XMETAExtraLines: tags="primus" + Library primus_mark_visited_plugin Path: plugins/primus_mark_visited Build$: flag(everything) || flag(primus_support) FindlibName: bap-plugin-primus_mark_visited CompiledObject: best - BuildDepends: bap-primus, bap, core_kernel, monads - XMETADescription: marks terms that were visited by Primus - Modules: Primus_mark_visited_main + BuildDepends: bap-main, bap, bap-primus, bap-primus-track-visited + XMETADescription: registers the bap:mark-visited component + InternalModules: Primus_mark_visited_main XMETAExtraLines: tags="primus" - Library primus_limit Path: plugins/primus_limit Build$: flag(everything) || flag(primus_support) diff --git a/oasis/primus-symbolic-executor b/oasis/primus-symbolic-executor new file mode 100644 index 000000000..ce8e211c2 --- /dev/null +++ b/oasis/primus-symbolic-executor @@ -0,0 +1,17 @@ +Flag primus_symbolic_executor + Description: Build Primus Symbolic Executor + Default: false + + +Library primus_symbolic_executor_plugin + Build$: flag(everything) || flag(primus_symbolic_executor) + Path: plugins/primus_symbolic_executor + BuildDepends: bap-primus, bap, core_kernel, bitvec, ppx_jane, + zarith, z3, regular, bap-main, monads, + bap-primus-track-visited + FindlibName: bap-plugin-primus_symbolic_executor + CompiledObject: best + InternalModules: Primus_symbolic_executor_main + XMETADescription: Enables symbolic execution in Primus + DataFiles: lisp/*.lisp ($primus_symbolic_executor_lisp_path) + XMETAExtraLines: tags="primus, lisp" diff --git a/oasis/primus-symbolic-executor.setup.ml.in b/oasis/primus-symbolic-executor.setup.ml.in new file mode 100644 index 000000000..eeba83ff7 --- /dev/null +++ b/oasis/primus-symbolic-executor.setup.ml.in @@ -0,0 +1,8 @@ +let (/) = Filename.concat + +let () = + add_variable ~doc:"where to install the library" + "primus_symbolic_executor_lisp_path" + ~define:(function + | None -> BaseEnv.var_get "datadir" / "primus" / "site-lisp" + | Some path -> path) diff --git a/oasis/primus-test b/oasis/primus-test index 69e1822d8..2eafc58f7 100644 --- a/oasis/primus-test +++ b/oasis/primus-test @@ -6,7 +6,7 @@ Flag primus_test Library primus_test_library_plugin Build$: flag(everything) || flag(primus_test) Path: plugins/primus_test - BuildDepends: bap-primus, bap, core_kernel, monads, regular + BuildDepends: bap-primus, bap, core_kernel, monads, regular, bitvec, bitvec-order, zarith FindlibName: bap-plugin-primus_test CompiledObject: best InternalModules: Primus_test_main diff --git a/oasis/primus-x86 b/oasis/primus-x86 index 87381880c..fedf90da7 100644 --- a/oasis/primus-x86 +++ b/oasis/primus-x86 @@ -7,7 +7,7 @@ Library primus_x86_plugin Build$: flag(everything) || flag(primus_x86) FindlibName: bap-plugin-primus_x86 CompiledObject: best - BuildDepends: bap, bap-primus, core_kernel, bap-x86-cpu + BuildDepends: bap, bap-primus, core_kernel, bap-x86-cpu, regular XMETADescription: x86 support package Modules: Primus_x86_main InternalModules: Primus_x86_loader diff --git a/opam/opam b/opam/opam index e947b8929..f012d9ab3 100644 --- a/opam/opam +++ b/opam/opam @@ -31,6 +31,7 @@ depends: [ "conf-bap-llvm" {>= "1.1"} "parsexp" "bap-signatures" + "z3" "result" {= "1.4"} ] depopts: ["conf-ida" "conf-binutils"] @@ -88,6 +89,7 @@ install: [ ["ocamlfind" "remove" "bap-plugin-relocatable"] ["ocamlfind" "remove" "bap-plugin-emit_ida_script"] ["ocamlfind" "remove" "bap-plugin-ida"] + ["ocamlfind" "remove" "bap-plugin-glibc_runtime"] ["ocamlfind" "remove" "bap-plugin-objdump"] ["ocamlfind" "remove" "bap-plugin-llvm"] ["ocamlfind" "remove" "bap-plugin-legacy_llvm"] @@ -102,6 +104,7 @@ install: [ ["ocamlfind" "remove" "bap-plugin-primus_limit"] ["ocamlfind" "remove" "bap-plugin-primus_print"] ["ocamlfind" "remove" "bap-plugin-primus_region"] + ["ocamlfind" "remove" "bap-plugin-primus_random"] ["ocamlfind" "remove" "bap-plugin-primus_systems"] ["ocamlfind" "remove" "bap-plugin-primus_taint"] ["ocamlfind" "remove" "bap-plugin-primus_test"] @@ -197,6 +200,7 @@ remove: [ ["ocamlfind" "remove" "bap-plugin-relocatable"] ["ocamlfind" "remove" "bap-plugin-emit_ida_script"] ["ocamlfind" "remove" "bap-plugin-ida"] + ["ocamlfind" "remove" "bap-plugin-glibc_runtime"] ["ocamlfind" "remove" "bap-plugin-objdump"] ["ocamlfind" "remove" "bap-plugin-llvm"] ["ocamlfind" "remove" "bap-plugin-legacy_llvm"] @@ -212,6 +216,7 @@ remove: [ ["ocamlfind" "remove" "bap-plugin-primus_limit"] ["ocamlfind" "remove" "bap-plugin-primus_print"] ["ocamlfind" "remove" "bap-plugin-primus_region"] + ["ocamlfind" "remove" "bap-plugin-primus_random"] ["ocamlfind" "remove" "bap-plugin-primus_systems"] ["ocamlfind" "remove" "bap-plugin-primus_taint"] ["ocamlfind" "remove" "bap-plugin-primus_test"] diff --git a/plugins/api/api/c/posix.h b/plugins/api/api/c/posix.h index 02ad9928b..3744f1aae 100644 --- a/plugins/api/api/c/posix.h +++ b/plugins/api/api/c/posix.h @@ -135,6 +135,8 @@ size_t fwrite(const void * restrict ptr, size_t size, size_t nmemb, FILE * restr __attribute__((warn_unused_result, storage(1,2,3))); void clearerr(FILE *stream); +int fflush(FILE *stream); + int __isoc99_fscanf (FILE *__restrict __stream, const char *__restrict __format, ...) __attribute__((warn_unused_result)); int __isoc99_scanf (const char *__restrict __format, ...) __attribute__((warn_unused_result)); int __isoc99_sscanf (const char *__restrict __s, const char *__restrict __format, ...) __attribute__((warn_unused_result)); @@ -144,7 +146,6 @@ int _IO_getc(FILE *stream); int _IO_putc(int c, FILE *stream); int _IO_puts(const char *s); - // string.h void *memccpy(void *restrict dst, const void *restrict src, int stop, size_t max) @@ -418,3 +419,29 @@ int posix_spawnp(pid_t *pid, const char *file, const void *file_actions, const void *attrp, char *const argv[], char *const envp[]); + +// errno.h + +int *__errno_location(void); + +// unistd.h + +int brk(void *addr); +void *sbrk(int increment); + + +// ctypes.h +int isalnum(int c); +int isalpha(int c); +int iscntrl(int c); +int isdigit(int c); +int isgraph(int c); +int islower(int c); +int isprint(int c); +int ispunct(int c); +int isspace(int c); +int isupper(int c); +int isxdigit(int c); + +int isascii(int c); +int isblank(int c); diff --git a/plugins/disassemble/disassemble_main.ml b/plugins/disassemble/disassemble_main.ml index da96a6f8c..5d6d8b5d2 100644 --- a/plugins/disassemble/disassemble_main.ml +++ b/plugins/disassemble/disassemble_main.ml @@ -339,6 +339,18 @@ let pp_guesses ppf badname = Format.fprintf ppf "did you mean %a?" (Format.pp_print_list ~pp_sep Format.pp_print_string) guesses +let is_verbose = Option.is_some (Sys.getenv_opt "BAP_DEBUG") + +let pp_backtrace ppf bt = + if is_verbose then fprintf ppf "Backtrace:@\n%s" bt + +let pp_exn ppf = function + | Invalid_argument s -> + fprintf ppf "%s" s + | Failure s -> + fprintf ppf "%s" s + | other -> fprintf ppf "%a" Exn.pp other + let nice_pp_error fmt er = let module R = Info.Internal_repr in let rec pp_sexp fmt = function @@ -348,37 +360,37 @@ let nice_pp_error fmt er = let open R in match r with | With_backtrace (r, backtrace) -> - Format.fprintf fmt "%a\n" pp r; - Format.fprintf fmt "Backtrace:\n%s" @@ String.strip backtrace + Format.fprintf fmt "%a@\n%a" pp r + pp_backtrace (String.strip backtrace); | String s -> Format.fprintf fmt "%s" s | r -> pp_sexp fmt (R.sexp_of_t r) in Format.fprintf fmt "%a" pp (R.of_info (Error.to_info er)) let string_of_failure = function | Expects_a_regular_file -> - "expected a regular file as input" + "Unable to open the specified file." | Old_and_new_style_passes -> - "passes are specified in both old an new style, \ + "Bad invocation: passes are specified in both old an new style, \ please switch to the new style, e.g., `-p,,'" | Unknown_pass name -> - asprintf "failed to find the pass named %S, %a" name pp_guesses name + asprintf "Bad invocation: failed to find the pass named %S, %a" name pp_guesses name | Incompatible_options (o1,o2) -> - sprintf "options `%s' and `%s' can not be used together" o1 o2 + sprintf "Bad invocation: the options `%s' and `%s' can not be used together" o1 o2 | Project err -> - asprintf "failed to build a project: %a" nice_pp_error err + asprintf "Failed to build the project:@\n %a" nice_pp_error err | Pass (Project.Pass.Unsat_dep (p,s)) -> - sprintf "dependency %S of pass %S is not available" + sprintf "Can't run passes - the dependency %S of pass %S is not available." s (Project.Pass.name p) | Pass (Project.Pass.Runtime_error (p, Exn.Reraised (bt,exn))) -> - asprintf "pass %S failed in runtime with %a@\nBacktrace:@\n%s@\n" - (Project.Pass.name p) Exn.pp exn bt + asprintf "The pass %S failed with:@\n%a@\n%a" + (Project.Pass.name p) pp_exn exn pp_backtrace bt | Pass (Project.Pass.Runtime_error (p, exn)) -> - asprintf "pass %S failed at runtime with %a" - (Project.Pass.name p) Exn.pp exn + asprintf "The pass %S failed with:@\n%a" + (Project.Pass.name p) pp_exn exn | Unknown_format fmt -> - sprintf "unknown format %S" fmt + sprintf "The format %S is not known." fmt | Unavailable_format_version fmt -> - sprintf "unsupported version of the format %S" fmt + sprintf "The selected version of the format %S is not supported." fmt let () = Extension.Error.register_printer @@ function | Fail err -> Some (string_of_failure err) diff --git a/plugins/glibc_runtime/glibc_runtime_main.ml b/plugins/glibc_runtime/glibc_runtime_main.ml new file mode 100644 index 000000000..bdbcf4f5a --- /dev/null +++ b/plugins/glibc_runtime/glibc_runtime_main.ml @@ -0,0 +1,133 @@ +let doc = " +Enables ad-hoc support for glibc runtime code. In particular it +detects the locations of $(b,main) and $b(,__libc_start_main) +functions (and adds the latter if it is absent). +" +open Base +open Bap_main +open Bap.Std +open Bap_c.Std + +let enable = Extension.Configuration.flag "enable" + ~doc:"Override the glib detection heuristic and enable the \ + runtime fixup." + +let glibc_sections = Set.of_list (module String) [ + ".symtab"; + ".init"; + ".plt"; + ".plt.got"; + ".text"; + ".fini"; + ] + +let is_glibc proj = + Project.memory proj |> + Memmap.to_sequence |> + Sequence.exists ~f:(fun (_,tag) -> + match Value.get Image.section tag with + | None -> false + | Some name -> Set.mem glibc_sections name) + +let find_by_name prog name = + Term.enum sub_t prog |> Seq.find ~f:(fun sub -> String.equal (Sub.name sub) name) + +let find_first_caller prog tid = + Term.enum sub_t prog |> Seq.find ~f:(fun sub -> + Term.enum blk_t sub |> Seq.exists ~f:(fun blk -> + Term.enum jmp_t blk |> Seq.exists ~f:(fun jmp -> + match Jmp.kind jmp with + | Call c -> Label.equal (Call.target c) (Direct tid) + | _ -> false))) + +let proj_int = function Bil.Int x -> Some x | _ -> None + +let is_sub_exists prog name = Option.is_some @@ find_by_name prog name +let is_sub_absent prog name = not (is_sub_exists prog name) + +let find_entry_point prog = + Term.enum sub_t prog |> + Seq.find ~f:(fun sub -> Term.has_attr sub Sub.entry_point) + +let find_libc_start_main prog = + let open Option.Monad_infix in + find_entry_point prog >>= fun start -> + Term.first blk_t start >>= fun entry -> + Term.first jmp_t entry >>= fun jmp -> + match Jmp.kind jmp with + | Goto _ | Ret _ | Int _ -> None + | Call call -> match Call.target call with + | Direct tid -> Some (tid,prog) + | Indirect _ -> + let name = "__libc_start_main" in + let tid = Tid.for_name name in + let sub = Sub.create ~tid ~name () in + let prog = Term.append sub_t prog sub in + let entry = Term.remove jmp_t entry (Term.tid jmp) in + let call = Call.create (Direct (Term.tid sub)) () in + let jmp = Jmp.create_call call in + let entry = Term.prepend jmp_t entry jmp in + let start = Term.update blk_t start entry in + let prog = Term.update sub_t prog start in + Some (Term.tid sub, prog) + +let detect_main_address prog = + let open Option.Monad_infix in + find_by_name prog "__libc_start_main" >>= fun start -> + find_first_caller prog (Term.tid start) >>= fun caller -> + Term.first blk_t caller >>= fun entry -> + Term.first arg_t start >>= fun arg -> + let defs = Term.enum def_t ~rev:true entry in + match Arg.rhs arg with + | Bil.Var reg -> + Seq.find defs ~f:(fun def -> + Var.same (Def.lhs def) reg) >>| Def.rhs >>= proj_int + | Bil.Load (_,addr,_,_) -> + Seq.find_map defs ~f:(fun def -> match Def.rhs def with + | Bil.Store (_,a,e,_,_) when Exp.equal addr a -> Some e + | _ -> None) >>= proj_int + | _ -> None + + +let reinsert_args_for_new_name sub name = + let sub = Term.filter arg_t sub ~f:(fun _ -> false) in + let sub = Term.del_attr sub C.proto in + Sub.with_name sub name + +let rename_main prog = match detect_main_address prog with + | None -> prog + | Some addr -> + Term.map sub_t prog ~f:(fun sub -> + match Term.get_attr sub address with + | Some a when Addr.equal addr a -> + reinsert_args_for_new_name sub "main" + | _ -> sub) + + +let rename_libc_start_main prog = + if is_sub_absent prog "__libc_start_main" + then match find_libc_start_main prog with + | None -> prog + | Some (tid,prog) -> + Term.change sub_t prog tid @@ function + | None -> None + | Some sub -> + Option.some @@ + reinsert_args_for_new_name sub "__libc_start_main" + else prog + +let fix_glibc_runtime prog = + rename_libc_start_main prog |> + rename_main + +let main ctxt proj = + if Extension.Configuration.get ctxt enable || + is_glibc proj + then + Project.with_program proj @@ + fix_glibc_runtime (Project.program proj) + else proj + +let () = Extension.declare ~doc ~provides:["abi"] @@ fun ctxt -> + Bap_abi.register_pass (main ctxt); + Ok () diff --git a/plugins/glibc_runtime/glibc_runtime_main.mli b/plugins/glibc_runtime/glibc_runtime_main.mli new file mode 100644 index 000000000..e69de29bb diff --git a/plugins/ida/ida_main.ml b/plugins/ida/ida_main.ml index 4398b64be..fbfa0652a 100644 --- a/plugins/ida/ida_main.ml +++ b/plugins/ida/ida_main.ml @@ -301,5 +301,5 @@ module Cmdline = struct match Info.create ida_path is_headless with | Ok info -> Bap_ida_service.register info !mode; main () | Error e -> - error "%S. Service not registered." (Error.to_string_hum e)) + warning "%S. Service not registered." (Error.to_string_hum e)) end diff --git a/plugins/primus_dictionary/primus_dictionary_main.ml b/plugins/primus_dictionary/primus_dictionary_main.ml index 9f931a24a..5c2570ba6 100644 --- a/plugins/primus_dictionary/primus_dictionary_main.ml +++ b/plugins/primus_dictionary/primus_dictionary_main.ml @@ -58,6 +58,48 @@ module Get(Machine : Primus.Machine.S) = struct | Some x -> Machine.return x end +module Next(Machine : Primus.Machine.S) = struct + [@@@warning "-P"] + include Pre(Machine) + + let run [dic; key] = + Machine.Local.get state >>= fun s -> + match Map.find s.dicts dic with + | None -> nil + | Some {dict} -> + match Map.closest_key dict `Greater_than key with + | None -> nil + | Some (x,_) -> Machine.return x +end + +module First(Machine : Primus.Machine.S) = struct + [@@@warning "-P"] + include Pre(Machine) + + let run [dic] = + Machine.Local.get state >>= fun s -> + match Map.find s.dicts dic with + | None -> nil + | Some {dict} -> match Map.min_elt dict with + | None -> nil + | Some (x,_) -> Machine.return x +end + + +module Length(Machine : Primus.Machine.S) = struct + [@@@warning "-P"] + include Pre(Machine) + + let run [dic] = + Machine.gets Project.arch >>| + Arch.addr_size >>| + Size.in_bits >>= fun width -> + Machine.Local.get state >>= fun s -> + match Map.find s.dicts dic with + | None -> nil + | Some {dict} -> Value.of_int ~width (Map.length dict) +end + module Del(Machine : Primus.Machine.S) = struct [@@@warning "-P"] include Pre(Machine) @@ -112,6 +154,18 @@ module Main(Machine : Primus.Machine.S) = struct def "dict-del" (tuple [sym; a] @-> bool) (module Del) {|(dict-del DIC KEY) deletes any association with KEY in the dictionary DIC|}; + + def "dict-first" (tuple [sym] @-> a) (module First) + {|(dict-first DIC) is the first key in DIC or nil if DIC is empty.|}; + + def "dict-next" (tuple [sym; a] @-> a) (module Next) + {|(dict-next DIC KEY) returns the next key after KEY + + Returns nil if KEY was the last key in the dictionary. + Could be used together with DICT-FIRST for iterating.|}; + + def "dict-length" (tuple [sym] @-> int) (module First) + {|(dict-first DIC) is the total number of keys in DIC.|}; ] end diff --git a/plugins/primus_limit/primus_limit_main.ml b/plugins/primus_limit/primus_limit_main.ml index bace983d3..cea812b7b 100644 --- a/plugins/primus_limit/primus_limit_main.ml +++ b/plugins/primus_limit/primus_limit_main.ml @@ -53,21 +53,21 @@ module Bound = struct let print ppf {limit; counter} = Format.fprintf ppf "%d%s" limit (suffix_of_counter counter) - let converter = Config.converter parse print {limit=0; counter=Clk} + let t = Config.converter parse print {limit=32768; counter=Clk} end module Cfg = struct open Config - let max_length = param (some Bound.converter) "max-length" + let max_length = param (some Bound.t) "max-length" ~doc: "Limits the maximum number of basic blocks a single machinine - can execute" + can execute." let max_visited = param (some int) "max-visited" ~doc: "Limits the maximum number of executions of the same block in - a given machine" + a given machine." end @@ -109,15 +109,13 @@ module Main(Machine : Primus.Machine.S) = struct | Clk -> "clocks" - let check_bound _ = match get Cfg.max_length with - | None -> Machine.return () - | Some {limit; counter} -> - Machine.Local.get state >>= fun s -> - if s.length > limit - then terminate (string_of_counter counter) - else Machine.Local.put state { - s with length = s.length + 1; - } + let check {limit; counter} _ = + Machine.Local.get state >>= fun s -> + if s.length > limit + then terminate (string_of_counter counter) + else Machine.Local.put state { + s with length = s.length + 1; + } let check_max_visits name visited = match get Cfg.max_visited with | None -> Machine.return () @@ -141,24 +139,26 @@ module Main(Machine : Primus.Machine.S) = struct let register_counter = let open Primus.Interpreter in - match get Cfg.max_length with - | None -> Machine.return () - | Some {counter=(Clk|Exp)} -> clock >>> check_bound - | Some {counter=Blk} -> enter_blk >>> check_bound - | Some {counter=Insn} -> pc_change >>> check_bound - | Some {counter=Term} -> enter_term >>> check_bound + let bound = match get Cfg.max_length with + | None -> {counter=Clk; limit=32768} + | Some bound -> bound in + match bound.counter with + | (Clk|Exp) -> clock >>> check bound + | Blk -> enter_blk >>> check bound + | Insn -> pc_change >>> check bound + | Term -> enter_term >>> check bound let init () = Machine.sequence [ Primus.Interpreter.enter_blk >>> on_blk; register_counter; ] - end - -let () = Config.when_ready (fun _ -> - Primus.Machine.add_component (module Main) [@warning "-D"]; +let () = Config.when_ready (fun {get} -> + if Option.is_some (get Cfg.max_length) || + Option.is_some (get Cfg.max_visited) + then Primus.Machine.add_component (module Main) [@warning "-D"]; Primus.Components.register_generic "limit" (module Main) ~package:"bap" ~desc: "Enables program termination by limiting the maximum \ diff --git a/plugins/primus_limit/primus_limit_main.mli b/plugins/primus_limit/primus_limit_main.mli new file mode 100644 index 000000000..e69de29bb diff --git a/plugins/primus_lisp/lisp/ascii.lisp b/plugins/primus_lisp/lisp/ascii.lisp index 7d81820d6..060a48c25 100644 --- a/plugins/primus_lisp/lisp/ascii.lisp +++ b/plugins/primus_lisp/lisp/ascii.lisp @@ -1,16 +1,45 @@ -(defun ascii-special (s) +(defun ascii-is-special (s) "(ascii-special S) is true if S is an ascii special character" (< s 32)) -(defun ascii-whitespace (s:8) - "(ascii-whitespace S)is true if S is a whitespace" - (or (= s 10) + +(defun ascii-is-whitespace (s) + "(ascii-is-whitespace S) is true if S is \t, \n, \r, or SPACE" + (or (= s 9) + (= s 10) (= s 13) (= s 32))) -(defun ascii-sign (s:8) +(defun ascii-sign (s) "(ascii-sign S) is 1 if S is + and -1 otherwise" (if (= s ?+) 1 -1)) -(defun ascii-digit (s:8) - "(ascii-digit s) is true if S is an ascii representation of decimal digit" +(defun ascii-is-digit (s) + "(ascii-is-digit s) is true if S is an ascii representation of decimal digit" + (declare (external "isdigit")) (< (- s ?0) 10)) + +(defun ascii-is-alphanum (c) + (declare (external "isalnum")) + (or (ascii-is-alpha c) + (ascii-is-digit c))) + +(defun ascii-is-alpha (c) + (declare (external "isalpha")) + (< (- (logor c 32) ?a) 26)) + +(defun ascii-is-upper (c) + (declare (external "isupper")) + (< (- c ?A) 26)) + +(defun ascii-is-lower (c) + (declare (external "islower")) + (< (- c ?a) 26)) + +(defun ascii-to-lower (c) + (declare (external "tolower")) + (if (ascii-is-upper c) (logor c 32) c)) + + +(defun ascii-to-upper (c) + (declare (external "toupper")) + (if (ascii-is-lower c) (logand c 0x5f) c)) diff --git a/plugins/primus_lisp/lisp/atoi.lisp b/plugins/primus_lisp/lisp/atoi.lisp index c07f8470a..c8fd9e5ec 100644 --- a/plugins/primus_lisp/lisp/atoi.lisp +++ b/plugins/primus_lisp/lisp/atoi.lisp @@ -5,7 +5,7 @@ (while (pred (memory-read s)) (incr s))) (defun atoi-prefix (s) - (or (ascii-special s) (ascii-whitespace s))) + (or (ascii-is-special s) (ascii-is-whitespace s))) (defun atoi-read-digit (s) (cast ptr_t (- (memory-read s) ?0))) @@ -14,7 +14,7 @@ (skip-all atoi-prefix s) (let ((v 0) (sign (ascii-sign (memory-read s)))) - (while (ascii-digit (memory-read s)) + (while (ascii-is-digit (memory-read s)) (set v (+ (* v 10) (atoi-read-digit s))) (incr s)) (* sign v))) diff --git a/plugins/primus_lisp/lisp/errno.lisp b/plugins/primus_lisp/lisp/errno.lisp new file mode 100644 index 000000000..21b2727e8 --- /dev/null +++ b/plugins/primus_lisp/lisp/errno.lisp @@ -0,0 +1,12 @@ +(require posix) +(require types) + +(declare (static errno-location)) + +(defmethod init () + (set errno-location brk) + (+= brk (sizeof int))) + +(defun errno-location () + (declare (external "__errno_location")) + errno-location) diff --git a/plugins/primus_lisp/lisp/init.lisp b/plugins/primus_lisp/lisp/init.lisp index f4eca938b..27ac17917 100644 --- a/plugins/primus_lisp/lisp/init.lisp +++ b/plugins/primus_lisp/lisp/init.lisp @@ -13,7 +13,7 @@ "(unless CND BODY) if CND evaluates to false, then BODY is evaluated and the value of the last expression in BODY becomes the value of the whole expression. Otherwise, if CND evaluates to true, nil is returned." - (if (not cnd) () body)) + (if cnd () body)) (defmacro until (c b) "(until COND BODY) if COND evaluates to true, then the whole expression diff --git a/plugins/primus_lisp/lisp/libc-init.lisp b/plugins/primus_lisp/lisp/libc-init.lisp index acc59bc33..2ca2d749f 100644 --- a/plugins/primus_lisp/lisp/libc-init.lisp +++ b/plugins/primus_lisp/lisp/libc-init.lisp @@ -9,6 +9,20 @@ (declare (external "__libc_start_main")) (exit-with (invoke-subroutine main argc argv))) +(defun setup-stack-canary () + (declare (context (abi "sysv"))) + (set FS_BASE (- brk 0x28)) + (memory-allocate brk (sizeof ptr_t)) + (write-word ptr_t brk 0xDEADBEEFBEAFDEAD) + (+= brk (sizeof ptr_t))) + +(defun init (main argc argv auxv) + "GNU libc initialization stub" + (declare (external "__libc_start_main") + (context (abi "sysv"))) + (setup-stack-canary) + (exit-with (invoke-subroutine main argc argv))) + (defun init (args on-exit main) "bionic initialization function" (declare (external "__libc_init")) diff --git a/plugins/primus_lisp/lisp/posix.lisp b/plugins/primus_lisp/lisp/posix.lisp index 0d5495f4a..06a2633da 100644 --- a/plugins/primus_lisp/lisp/posix.lisp +++ b/plugins/primus_lisp/lisp/posix.lisp @@ -1,4 +1,4 @@ (require stdlib) (require stdio) (require string) -(require primus) +(require errno) diff --git a/plugins/primus_lisp/lisp/primus.lisp b/plugins/primus_lisp/lisp/primus.lisp deleted file mode 100644 index f3c70a1db..000000000 --- a/plugins/primus_lisp/lisp/primus.lisp +++ /dev/null @@ -1,4 +0,0 @@ -(defun handle-unresolved-names () - "(handle-unresolved-names) emits a diagnostic message when called" - (declare (external "__primus_linker_unresolved_call")) - (msg "skipping a jump to an unknown destination at $0" (get-current-program-counter))) diff --git a/plugins/primus_lisp/lisp/simple-memory-allocator.lisp b/plugins/primus_lisp/lisp/simple-memory-allocator.lisp index d8dd1e6ef..d341f2673 100644 --- a/plugins/primus_lisp/lisp/simple-memory-allocator.lisp +++ b/plugins/primus_lisp/lisp/simple-memory-allocator.lisp @@ -1,4 +1,5 @@ (require string) +(require types) (defparameter *malloc-max-chunk-size* nil "the maximum size of a single memory chunk, @@ -8,9 +9,16 @@ "the maximum number of bytes totally allocated by malloc, if not set, then there is no limit") +(defparameter *malloc-arena-initial-size* 0x40000 + "the maximum number of bytes totally allocated by malloc, + if not set, then there is no limit") + (defparameter *malloc-arena-start* brk "the starting address of the malloc arena") +(defparameter *malloc-arena-end* brk + "the starting address of the malloc arena") + (defparameter *malloc-guard-edges* 0 "if not nil, then add padding of the specified size around allocated chunks") @@ -24,36 +32,45 @@ (defparameter *malloc-initialize-memory* false "if true then initialize allocated memory with *malloc-initial-value*") +(defparameter *malloc-uniform-min-value* nil + "if set then defines the lower bound of the uniformely distributed + random value that is used to represent an unitialized memory ") + +(defparameter *malloc-uniform-max-value* nil + "if set then defines the lower bound of the uniformely distributed + random value that is used to represent an unitialized memory ") + (defparameter *malloc-initial-value* 0 "initialize allocated memory with the said value") -(defun memory/allocate (ptr len) - (if *malloc-initialize-memory* - (memory-allocate ptr len *malloc-initial-value*) - (memory-allocate ptr len))) - -(defun malloc/put-chunk-size (ptr len) - (write-word ptr_t ptr len)) +(defparameter *malloc/brk* brk) -(defun malloc/get-chunk-size (ptr) - (let ((header-size (/ (word-width) 8))) - (read-word ptr_t (- ptr header-size)))) +(defparameter *malloc/total-bytes-allocated* 0) (defun malloc (n) "allocates a memory region of size N" (declare (external "malloc")) (if (= n 0) *malloc-zero-sentinel* (if (malloc-will-reach-limit n) 0 - (let ((header-size (/ (word-width) 8)) + (malloc/grow-arena-if-needed n) + (+= *malloc/total-bytes-allocated* n) + (let ((header-size (sizeof int)) (chunk-size (+ n (* 2 *malloc-guard-edges*) header-size)) - (ptr brk) - (failed (memory/allocate ptr chunk-size))) - (if failed 0 - (set brk (+ brk chunk-size)) - (malloc/fill-edges ptr chunk-size) - (set ptr (+ ptr *malloc-guard-edges*)) - (malloc/put-chunk-size ptr n) - (+ ptr header-size)))))) + (ptr *malloc/brk*)) + (malloc/initialize ptr chunk-size) + (+= *malloc/brk* chunk-size) + (malloc/fill-edges ptr chunk-size) + (+= ptr *malloc-guard-edges*) + (malloc/put-chunk-size ptr n) + (+ ptr header-size))))) + +(defun brk () + (declare (external "brk")) + brk) + +(defun sbrk (increment) + (declare (external "sbrk")) + (+= brk increment)) (defun realloc (ptr len) (declare (external "realloc")) @@ -61,9 +78,6 @@ (if (not len) (realloc/as-free ptr) (realloc/update-chunk ptr len)))) -(defun realloc/shrink-chunk (ptr len) - (malloc/put-chunk-size ptr len) - ptr) ;; pre: both old-ptr and new-len are not null (defun realloc/update-chunk (old-ptr new-len) @@ -88,11 +102,13 @@ (defun calloc (n s) "allocates memory and initializes it with zero" (declare (external "calloc")) - (malloc (* n s))) ; in our implementation malloc zeros memory + (let ((*malloc-initialize-memory* true) + (*malloc-initial-value* 0)) + (malloc (* n s)))) (defun malloc-heap-size () - (- brk *malloc-arena-start*)) + *malloc/total-bytes-allocated*) (defun malloc-will-reach-limit (n) @@ -109,3 +125,41 @@ (memset (- (+ ptr n) *malloc-guard-edges*) *malloc-guard-pattern* *malloc-guard-edges*))) + + +(defun malloc/allocate-arena (len) + (set *malloc-arena-start* brk) + (+= brk len) + (set *malloc-arena-end* brk) + (if *malloc-initialize-memory* + (memory-allocate *malloc-arena-start* + len + *malloc-initial-value*) + (memory-allocate *malloc-arena-start* + len + *malloc-uniform-min-value* + *malloc-uniform-max-value*))) + +(defun malloc/initialize (ptr len) + (if *malloc-initialize-memory* + (memory-allocate ptr len *malloc-initial-value*) + (when (or *malloc-uniform-min-value* + *malloc-uniform-max-value*) + (memory-allocate ptr len + *malloc-uniform-min-value* + *malloc-uniform-max-value*)))) + +(defun malloc/grow-arena-if-needed (len) + (let ((free-space (- *malloc-arena-end* *malloc/brk*))) + (when (> len free-space) + (malloc/allocate-arena (max *malloc-arena-initial-size* len))))) + +(defun realloc/shrink-chunk (ptr len) + (malloc/put-chunk-size ptr len) + ptr) + +(defun malloc/put-chunk-size (ptr len) + (write-word int ptr len)) + +(defun malloc/get-chunk-size (ptr) + (read-word int (- ptr (sizeof int)))) diff --git a/plugins/primus_lisp/lisp/stdio.lisp b/plugins/primus_lisp/lisp/stdio.lisp index 4991143c6..2bf73ba54 100644 --- a/plugins/primus_lisp/lisp/stdio.lisp +++ b/plugins/primus_lisp/lisp/stdio.lisp @@ -16,20 +16,32 @@ (while (not (points-to-null p)) (fputc (cast int (memory-read p)) stream) (incr p)) - (fputc 0xA stream)) + (let ((r (fputc 0xA stream))) + (fflush stream) + r)) (defun puts (p) (declare (external "puts")) (fputs p *standard-output*)) +(defun fflush (s) + (declare (external "fflush")) + (channel-flush s)) + + ;; the channel module have rough equality between streams and ;; file descriptors, as they both are represented as integers. We are currently ;; ignoring modes, we will add them later, of course. (defun fopen (path mode) - (declare (external "fopen" "open")) + (declare (external "fopen" "open" "fdopen")) (channel-open path)) +(defun fileno (stream) + (declare (external "fileno")) + stream) + + (defun open3 (path flags mode) (declare (external "open")) (fopen path mode)) @@ -62,7 +74,7 @@ (or failure written))) (defun input-item-nth-char (ptr size item desc i) - (let ((c (channel-input desc))) + (let ((c (fgetc desc))) (if (= c -1) 0 (memory-write (+ ptr (* size item) i) (cast char c)) 1))) @@ -89,22 +101,31 @@ (defun fgetc (stream) (declare (external "fgetc" "getc")) + (msg "the concrete fgets is called") (channel-input stream)) -(defun fgets-step (ptr len str i) - (let ((c (channel-input str))) - (if (= c -1) 0 - (memory-write (+ ptr i) (cast char c)) - (not (= c 0xA:8))))) +(defun terminate-string-and-return-null (ptr) + (memory-write ptr 0:8) + 0) (defun fgets (ptr len str) (declare (external "fgets")) - (let ((i 0)) - (while (and (< i len) - (fgets-step ptr len str i)) - (incr i)) - (memory-write (+ ptr (min (-1 len) (+ ptr i))) 0:8) - ptr)) + (if (= len 0) (terminate-string-and-return-null ptr) + (let ((i 0) + (n (-1 len)) + (continue true)) + (while (and continue (< i n)) + (let ((c (fgetc str))) + (if (= c -1) + (set continue false) + (memory-write (+ ptr i) (cast char c)) + (set continue (/= c 0xA:8)) + (incr i)))) + (if (= i 0) + (terminate-string-and-return-null ptr) + (memory-write (+ ptr (min n i)) 0:8) + ptr)))) + (defun getchar () (declare (external "getchar")) diff --git a/plugins/primus_lisp/lisp/stdlib.lisp b/plugins/primus_lisp/lisp/stdlib.lisp index 8e4ea2d3a..12817ae2e 100644 --- a/plugins/primus_lisp/lisp/stdlib.lisp +++ b/plugins/primus_lisp/lisp/stdlib.lisp @@ -29,14 +29,6 @@ (declare (external "atexit")) 0) - -(defun stub () - "stubs that does nothing" - (declare (external - "setlocale" - "bindtextdomain" - "textdomain" - "__cxa_atexit" - "__ctype_get_mb_cur_max" - "__ctype_b_loc" - "__do_global_dtors_aux"))) +(defun abs (x) + (declare (external "abs")) + (if (is-negative x) (neg x) x)) diff --git a/plugins/primus_lisp/lisp/string.lisp b/plugins/primus_lisp/lisp/string.lisp index 89da52877..9cb1e8fef 100644 --- a/plugins/primus_lisp/lisp/string.lisp +++ b/plugins/primus_lisp/lisp/string.lisp @@ -78,11 +78,11 @@ (defun strchr (p c) - (declare (external "strchr")) + (declare (external "strchr" "index")) (memchr p c (+ (strlen p) 1))) (defun strrchr (p c) - (declare (external "strrchr")) + (declare (external "strrchr" "rindex")) (memrchr p c (+ (strlen p) 1))) @@ -96,6 +96,16 @@ (incr p)) found)) +(defun strcat (dst src) + (declare (external "strcat")) + (strcpy (+ dst (cast ptr_t (strlen dst))) src) + dst) + +(defun strncat (dst src len) + (declare (external "strncat")) + (strncpy (+ dst (cast ptr_t (strlen dst))) src len) + dst) + (defun memset (p c n) (declare (external "memset")) @@ -126,6 +136,96 @@ (strlen/with-null s2)))) (defun strcmp (s1 s2) - (declare (external "strcmp")) + (declare (external "strcmp" "strcoll")) (memcmp s1 s2 (min (strlen/with-null s1) (strlen/with-null s2)))) + +(defun strncasecmp (p1 p2 n) + (declare (external "strncasecmp")) + (let ((res 0) (i 0)) + (while (and (< i n) (not res)) + (set res (compare + (tolower (memory-read p1)) + (tolower (memory-read p2)))) + (incr p1 p2 i)) + res)) + +(defun strcasecmp (p1 p2) + (declare (external "strncasecmp")) + (strncasecmp p1 p2 (min (strlen p1) + (strlen p2)))) + + +(defmacro find-substring (compare hay needle) + (let ((found 0) + (n (strlen needle))) + (while (and (memory-read hay) (not found)) + (set found (not (compare hay needle n))) + (incr hay)))) + +(defun strstr (hay needle) + (declare (external "strstr")) + (find-substring strncmp hay needle)) + +(defun strcasestr (hay needle) + (declare (external "strcasestr")) + (find-substring strncasecmp hay needle)) + +(defmacro strspn (str set) + (declare (external "strspn")) + (let ((len 0)) + (while (strpbrk str set) + (incr str len)) + len)) + +(defun strcspn (str set) + (declare (external "strcspn")) + (let ((len 0)) + (until (or (points-to-null str) + (strpbrk str set)) + (incr str len)) + len)) + + +(defun strsep (strp sep) + (declare (external "strsep")) + (let ((str (read-word ptr_t strp)) + (pos (and str (+ str (strcspn str sep))))) + (when str + (if (points-to-null pos) + (write-word ptr_t strp 0) + (memory-write pos 0) + (write-word ptr_t strp (+1 pos)))) + str)) + + +(defun strtok_r (str sep ptr) + (declare (external "strtok_r")) + (when str (write-word ptr_t ptr str)) + (if (not ptr) ptr + (let ((str (read-word ptr_t ptr)) + (del (+ str (strspn str sep))) + (str (+ del (strcspn del sep)))) + (if (points-to-null del) 0 + (write-word ptr_t ptr str) + (memory-write del 0))))) + + +(defparameter *strtok-static-storage* 0) + +(defun strtok (str sep) + (declare (external "strtok")) + (unless *strtok-static-storage* + (set *strtok-static-storage* (malloc (sizeof ptr_t)))) + (strtok_r str sep *strtok-static-storage*)) + + +(defun strxfrm (dst src len) + (declare (external "strxfrm")) + (strncpy dst src len) + len) + +(defun stpcpy (dst src) + (declare (external "stpcpy")) + (let ((len (strlen src))) + (+ (memcpy dst src (+1 len)) (cast ptr_t len)))) diff --git a/plugins/primus_lisp/lisp/types.lisp b/plugins/primus_lisp/lisp/types.lisp index 6e4ee079c..1442d91d8 100644 --- a/plugins/primus_lisp/lisp/types.lisp +++ b/plugins/primus_lisp/lisp/types.lisp @@ -41,43 +41,43 @@ (defun char () (declare (context (abi eabi))) (model-ilp32 'char)) (defun short () (declare (context (abi eabi))) (model-ilp32 'short)) -(defun int () (declare (context (abi eabi))) (model-ilp32 'long)) +(defun int () (declare (context (abi eabi))) (model-ilp32 'int)) (defun long () (declare (context (abi eabi))) (model-ilp32 'long)) (defun ptr_t () (declare (context (abi eabi))) (model-ilp32 'ptr)) (defun char () (declare (context (abi mips32))) (model-ilp32 'char)) (defun short () (declare (context (abi mips32))) (model-ilp32 'short)) -(defun int () (declare (context (abi mips32))) (model-ilp32 'long)) +(defun int () (declare (context (abi mips32))) (model-ilp32 'int)) (defun long () (declare (context (abi mips32))) (model-ilp32 'long)) (defun ptr_t () (declare (context (abi mips32))) (model-ilp32 'ptr)) (defun char () (declare (context (abi mips64))) (model-ilp64 'char)) (defun short () (declare (context (abi mips64))) (model-ilp64 'short)) -(defun int () (declare (context (abi mips64))) (model-ilp64 'long)) +(defun int () (declare (context (abi mips64))) (model-ilp64 'int)) (defun long () (declare (context (abi mips64))) (model-ilp64 'long)) (defun ptr_t () (declare (context (abi mips64))) (model-ilp64 'ptr)) (defun char () (declare (context (abi ppc32))) (model-ilp32 'char)) (defun short () (declare (context (abi ppc32))) (model-ilp32 'short)) -(defun int () (declare (context (abi ppc32))) (model-ilp32 'long)) +(defun int () (declare (context (abi ppc32))) (model-ilp32 'int)) (defun long () (declare (context (abi ppc32))) (model-ilp32 'long)) (defun ptr_t () (declare (context (abi ppc32))) (model-ilp32 'ptr)) (defun char () (declare (context (arch x86_64 sysv))) (model-lp64 'char)) (defun short () (declare (context (arch x86_64 sysv))) (model-lp64 'short)) -(defun int () (declare (context (arch x86_64 sysv))) (model-lp64 'long)) +(defun int () (declare (context (arch x86_64 sysv))) (model-lp64 'int)) (defun long () (declare (context (arch x86_64 sysv))) (model-lp64 'long)) (defun ptr_t () (declare (context (arch x86_64 sysv))) (model-lp64 'ptr)) (defun char () (declare (context (arch x86_64 ms))) (model-llp64 'char)) (defun short () (declare (context (arch x86_64 ms))) (model-llp64 'short)) -(defun int () (declare (context (arch x86_64 ms))) (model-llp64 'long)) +(defun int () (declare (context (arch x86_64 ms))) (model-llp64 'int)) (defun long () (declare (context (arch x86_64 ms))) (model-llp64 'long)) (defun ptr_t () (declare (context (arch x86_64 ms))) (model-llp64 'ptr)) (defun char () (declare (context (arch x86))) (model-lp32 'char)) (defun short () (declare (context (arch x86))) (model-lp32 'short)) -(defun int () (declare (context (arch x86))) (model-lp32 'long)) +(defun int () (declare (context (arch x86))) (model-lp32 'int)) (defun long () (declare (context (arch x86))) (model-lp32 'long)) (defun ptr_t () (declare (context (arch x86))) (model-lp32 'ptr)) diff --git a/plugins/primus_lisp/primus_lisp_primitives.ml b/plugins/primus_lisp/primus_lisp_primitives.ml index 8124f873e..df616d877 100644 --- a/plugins/primus_lisp/primus_lisp_primitives.ml +++ b/plugins/primus_lisp/primus_lisp_primitives.ml @@ -13,16 +13,20 @@ let registers = Primus.Machine.State.declare Map.set regs (Reg.code r) (Reg.name r) | _ -> regs)) -module Make(Machine : Primus.Machine.S) = struct - module Eval = Primus.Interpreter.Make(Machine) +module Closure(Machine : Primus.Machine.S) = struct module Lisp = Primus.Lisp.Make(Machine) - module Memory = Primus.Memory.Make(Machine) module Value = Primus.Value.Make(Machine) + module Eval = Primus.Interpreter.Make(Machine) + module Closure = Primus.Lisp.Closure.Make(Machine) module Linker = Primus.Linker.Make(Machine) + type value = Value.t + type 'a m = 'a Machine.t + open Machine.Syntax - let all f args = List.exists args ~f |> Value.of_bool + let failf = Lisp.failf + let addr_width = Machine.arch >>| Arch.addr_size >>| Size.in_bits let endian = @@ -35,529 +39,303 @@ module Make(Machine : Primus.Machine.S) = struct | [] -> null | x :: xs -> Machine.List.fold xs ~init:x ~f:op - let signed_reduce null op xs = - Machine.List.map xs ~f:Value.signed >>= - reduce (null >>= Value.signed) op - - let ordered order xs = - let rec ordered = function - | [] | [_] -> true - | x :: (y :: _ as rest) -> order x y && ordered rest in - if ordered xs then true_ else false_ -end - -module RegName(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - let run = function - | [] | _::_::_ -> - Lisp.failf "reg-name expects only one argument" () - | [code] -> - Machine.Local.get registers >>= fun regs -> - let code = Word.to_int_exn @@ Primus.Value.to_word code in - match Map.find regs code with - | None -> Lisp.failf "unresolved intruction register %#x" code () - | Some name -> Value.Symbol.to_value name -end - - -module ExecAddr(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - let run = function - | _ :: _ :: _ | [] -> - Lisp.failf "Lisp Type Error: exec-address expects one argument" () - | [addr] -> - Linker.exec (`addr (Primus.Value.to_word addr)) >>= fun () -> - Eval.halt >>= - never_returns -end - -module ExecSym(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - let run = function - | _ :: _ :: _ | [] -> - Lisp.failf "Lisp Type Error: exec-address expects one argument" () - | [name] -> - Value.Symbol.of_value name >>= fun name -> - Linker.exec (`symbol name) >>= fun () -> - Eval.halt >>= - never_returns -end - -module IsZero(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - let run = all Value.is_zero -end - -module IsPositive(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - let run = all Value.is_positive -end + let msb x = + let hi = Value.bitwidth x - 1 in + Value.extract ~hi ~lo:hi x -module IsNegative(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - let run = all Value.is_negative -end + let to_int e = match Word.to_int (Value.to_word e) with + | Ok x -> Machine.return x + | Error _ -> failf "expected smallint" () -module WordWidth(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib + let rec all f = function + | [] -> true_ + | x :: xs -> + f x >>= fun x -> + if Value.is_one x + then + all f xs >>= fun xs -> + Eval.binop AND x xs + else Machine.return x - let run args = + let ordered order xs = + let rec ordered = function + | [] | [_] -> true_ + | x :: (y :: _ as rest) -> + order x y >>= fun r -> + if Value.is_one r + then ordered rest >>= fun r' -> + Eval.binop AND r r' + else Machine.return r in + ordered xs + + let reg_name code = + Machine.Local.get registers >>= fun regs -> + let code = Word.to_int_exn @@ Primus.Value.to_word code in + match Map.find regs code with + | None -> failf "unresolved intruction register %#x" code () + | Some name -> Value.Symbol.to_value name + + let exec_addr addr = + Linker.exec (`addr (Primus.Value.to_word addr)) >>= fun () -> + Eval.halt >>= + never_returns + + let exec_symbol name = + Value.Symbol.of_value name >>= fun name -> + Linker.exec (`symbol name) >>= fun () -> + Eval.halt >>= + never_returns + + let is_zero = all @@ fun x -> + Value.zero (Value.bitwidth x) >>= fun z -> + Eval.binop EQ x z + + let is_positive = all @@ fun x -> + msb x >>= Eval.unop NOT + + let word_width args = addr_width >>= fun width -> match args with | [] -> Value.of_int ~width width | x :: _ -> Value.of_int ~width (Value.bitwidth x) -end -module ExitWith(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = all Value.is_negative - let run _ = + let exit_with _ = Eval.halt >>| Nothing.unreachable_code >>= fun () -> Value.b0 -end - -module MemoryAllocate(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib let negone = Value.one 8 let zero = Value.zero 8 - let make_static_generator x = match Word.to_int x with - | Ok x when x >= 0 && x < 256 -> - Ok (Some (Primus.Generator.static x)) - | _ -> Or_error.errorf "memory-allocate: fill in value must fit into byte" - - let run = function - | addr :: size :: gen -> - let n = Word.to_int (Value.to_word size) in - let gen = match gen with - | [] -> Ok None - | [x] -> make_static_generator (Value.to_word x) - | _ -> Or_error.errorf "memory-allocate requires two or three arguments" in - if Result.is_error n || Result.is_error gen - then negone - else - let generator = Or_error.ok_exn gen in - Memory.allocate ?generator (Value.to_word addr) (Or_error.ok_exn n) >>= - fun () -> zero - | _ -> Lisp.failf "allocate requires two arguments" () -end - - -module MemoryRead(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = function - | [x] -> - endian >>= fun e -> Eval.load x e `r8 - | _ -> Lisp.failf "memory-read requires one argument" () -end - -module MemoryWrite(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = function - | [a;x] -> - endian >>= fun e -> - Eval.store a x e `r8 >>= fun () -> - Value.succ a - | _ -> Lisp.failf "memory-write requires two arguments" () -end - -module GetPC(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = function - | [] -> Eval.pc >>= Value.of_word - | _ -> Lisp.failf - "get-current-program-counter requires zero arguments" () -end - - -module Add(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = reduce null (Eval.binop Bil.PLUS) -end - -module Sub(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = reduce null (Eval.binop Bil.MINUS) -end - -module Div(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = reduce null (Eval.binop Bil.DIVIDE) -end - -module SDiv(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = signed_reduce null (Eval.binop Bil.SDIVIDE) -end - -module Mul(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = reduce null (Eval.binop Bil.TIMES) -end - -module Mod(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = reduce null (Eval.binop Bil.MOD) -end - -module SignedMod(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = signed_reduce null (Eval.binop Bil.SMOD) -end - -module Lshift(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = function - | [x;y] -> Eval.binop Bil.lshift x y - | _ -> Lisp.failf "Type error: lshift expects two arguments" () -end - -module Rshift(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = function - | [x;y] -> Eval.binop Bil.rshift x y - | _ -> Lisp.failf "Type error: rshift expects two arguments" () -end - -module Arshift(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = function - | [x;y] -> Eval.binop Bil.arshift x y - | _ -> Lisp.failf "Type error: arshift expects two arguments" () -end - -module Equal(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = function - | [] -> true_ - | x :: xs -> all (Value.equal x) xs -end - -module NotEqual(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - module Equal = Equal(Machine) - open Machine.Syntax - - let run xs = Equal.run xs >>= (Lib.Eval.unop Bil.NOT) -end - - -module Logand(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = reduce negone (Eval.binop Bil.AND) -end - -module Logor(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = reduce null (Eval.binop Bil.OR) -end - -module Logxor(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = reduce null (Eval.binop Bil.XOR) -end - -module Concat(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = reduce false_ Eval.concat -end - -module Extract(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - - let to_int e = match Word.to_int (Value.to_word e) with - | Ok x -> Machine.return x - | Error _ -> Lisp.failf "expected smallint" () - - let run = function - | [hi; lo; x] -> - to_int hi >>= fun hi -> - to_int lo >>= fun lo -> - Eval.extract ~hi ~lo x - | _ -> Lisp.failf "extract expects exactly three arguments" () -end - -module Not(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = function - | [x] -> if Value.is_zero x then Value.b1 else Value.b0 - | _ -> Lisp.failf "not expects only one argument" () -end - -module Lnot(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = function - | [x] -> Eval.unop Bil.NOT x - | _ -> Lisp.failf "lnot expects only one argument" () -end - -module Neg(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = function - | [x] -> Eval.unop Bil.NEG x - | _ -> Lisp.failf "neg expects only one argument" () -end - -module Less(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let rec run = ordered Value.(<) -end - -module Greater(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let rec run = ordered Value.(>) -end - -module LessEqual(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let rec run = ordered Value.(<=) -end - -module GreaterEqual(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let rec run = ordered Value.(>=) -end - -module SymbolConcat(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run syms = + let value_to_int x = Value.to_word x |> Word.to_int + + let make_static_generator width x = match Word.to_int x with + | Ok x -> Ok (Some (Primus.Generator.static ~width x)) + | _ -> Or_error.errorf "memory-allocate: fill in value must fit into int" + + let is_nil x = Word.equal Word.b0 (Value.to_word x) + + let make_uniform_generator ~width ~min ~max = + let nomin = is_nil min and nomax = is_nil max in + if nomin && nomax then Ok None + else match value_to_int min, value_to_int max with + | Ok min, Ok max -> + let min = if nomin then None else Some min + and max = if nomax then None else Some max in + let g = Primus.Generator.Random.Seeded.lcg ~width ?min ?max () in + Ok (Some g) + | _ -> Or_error.errorf "memory-allocate: random values do not fit into int" + + + let memory_allocate addr size rest = + let module Memory = Primus.Memory.Make(Machine) in + Machine.gets Project.arch >>= fun arch -> + let width = Arch.addr_size arch |> Size.in_bits in + let gen = match rest with + | [] -> Ok None + | [x] -> make_static_generator width (Value.to_word x) + | [min; max] -> make_uniform_generator width min max + | _ -> Or_error.errorf "bad generator" in + if Result.is_error gen + then failf "memory-allocate: bad generator specification" () + else + let generator = Or_error.ok_exn gen in + let lower = Value.to_word addr in + let upper = Word.(lower + pred (Value.to_word size)) in + Memory.add_region ?generator ~lower ~upper () >>= fun () -> + zero + + let memory_read addr = Eval.load addr BigEndian `r8 + let memory_write a x = + Eval.store a x BigEndian `r8 >>= fun () -> + Value.succ a + + let extract hi lo x = + to_int hi >>= fun hi -> + to_int lo >>= fun lo -> + Eval.extract ~hi ~lo x + + let symbol_concat syms = Machine.List.map syms ~f:Value.Symbol.of_value >>= fun strs -> Value.Symbol.to_value (String.concat strs) -end - -module SetSymbol(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - - let run = function - | [reg; x] -> - Value.Symbol.of_value reg >>= fun reg -> - let typ = Type.imm (Word.bitwidth (Value.to_word x)) in - let var = Var.create reg typ in - Eval.set var x >>| fun () -> x - | _ -> Lisp.failf "set-symbol-value expects exactly two arguments" () -end + let set_value reg x = + Value.Symbol.of_value reg >>= fun reg -> + let typ = Type.imm (Word.bitwidth (Value.to_word x)) in + let var = Var.create reg typ in + Eval.set var x >>| fun () -> x + + let symbol_of_cstring ptr = + let module Mem = Primus.Memory.Make(Machine) in + let rec build chars ptr = + Mem.load ptr >>= fun x -> + if Word.is_zero x + then + Machine.return @@ + String.of_char_list (List.rev chars) + else + let char = Word.to_int_exn x |> Char.of_int_exn in + build (char::chars) (Word.succ ptr) in + build [] (Value.to_word ptr) >>= + Value.Symbol.to_value -module Stub(Machine : Primus.Machine.S) = struct - module Lib = Make(Machine) - open Machine.Syntax - open Lib - let run = Lisp.failf "not implemented" + let run args = + Closure.name >>= fun name -> match name, args with + | "reg-name",[arg] -> reg_name arg + | "exec-addr", [addr] -> exec_addr addr + | "exec-symbol", [dst] -> exec_symbol dst + | "is-zero", args -> is_zero args + | "is-positive", args -> is_positive args + | "is-negative", args -> all msb args + | "word-width", args -> word_width args + | "exit-with", [arg] -> exit_with arg + | "memory-allocate", x :: y :: rest -> memory_allocate x y rest + | "memory-read", [x] -> memory_read x + | "memory-write", [a;x] -> memory_write a x + | "get-current-program-counter",[] -> Eval.pc >>= Value.of_word + | "+",args -> reduce null (Eval.binop Bil.PLUS) args + | "-",args -> reduce null (Eval.binop Bil.MINUS) args + | "/",args -> reduce null (Eval.binop Bil.DIVIDE) args + | "s/",args -> reduce null (Eval.binop Bil.SDIVIDE) args + | "*",args -> reduce null (Eval.binop Bil.TIMES) args + | "mod",args -> reduce null (Eval.binop Bil.MOD) args + | "signed-mod",args -> reduce null (Eval.binop Bil.SMOD) args + | "lshift", [x;y] -> Eval.binop Bil.lshift x y + | "rshift", [x;y] -> Eval.binop Bil.rshift x y + | "arshift", [x;y] -> Eval.binop Bil.arshift x y + | "=",args -> ordered (Eval.binop EQ) args + | "/=",args -> ordered (Eval.binop NEQ) args + | "logand",args -> reduce negone (Eval.binop Bil.AND) args + | "logor",args -> reduce negone (Eval.binop Bil.OR) args + | "logxor",args -> reduce negone (Eval.binop Bil.XOR) args + | "concat", args -> reduce false_ Eval.concat args + | "extract", [hi; lo; x] -> extract hi lo x + | "not", [x] -> is_zero [x] + | "lnot", [x] -> Eval.unop Bil.NOT x + | "neg", [x] -> Eval.unop Bil.NEG x + | "<", args -> ordered (Eval.binop LT) args + | ">", args -> ordered (fun x y -> Eval.binop LT y x) args + | "<=", args -> ordered (Eval.binop LE) args + | ">=", args -> ordered (fun x y -> Eval.binop LE y x) args + | "symbol-concat",args -> symbol_concat args + | "set-symbol-value", [reg; x] -> set_value reg x + | "symbol-of-string", [ptr] -> symbol_of_cstring ptr + | name,_ -> Lisp.failf "%s: invalid number of arguments" name () end module Primitives(Machine : Primus.Machine.S) = struct open Machine.Syntax module Lisp = Primus.Lisp.Make(Machine) + module Eval = Primus.Interpreter.Make(Machine) let init () = let open Primus.Lisp.Type.Spec in - let def name types closure docs = - Lisp.define ~types ~docs name closure in + let def name types docs = + Lisp.define ~types ~docs name (module Closure) in Machine.sequence [ - def "exec-addr" (one int @-> any) (module ExecAddr) + def "exec-addr" (one int @-> any) "(exec-addr D) passes the control flow to D and never returns"; - def "exec-symbol" (one sym @-> any) (module ExecSym) + def "exec-symbol" (one sym @-> any) "(exec-symbol D) passes the control flow to D and never returns"; - def "is-zero" (all any @-> bool) (module IsZero) + def "is-zero" (all any @-> bool) "(is-zero X Y ...) returns true if all arguments are zeros"; - def "is-positive" (all any @-> bool) (module IsPositive) + def "is-positive" (all any @-> bool) "(is-positive X Y ...) returns true if all arguments are positive"; - def "is-negative" (all any @-> bool) (module IsNegative) + def "is-negative" (all any @-> bool) "(is-negative X Y ...) returns true if all arguments are negative"; - def "word-width" (unit @-> int) (module WordWidth) + def "word-width" (unit @-> int) "(word-width) returns machine word width in bits"; - def "exit-with" (one int @-> any) (module ExitWith) + def "exit-with" (one int @-> any) "(exit-with N) terminates program with the exit codeN"; - def "memory-read" (one int @-> byte) (module MemoryRead) + def "memory-read" (one int @-> byte) "(memory-read A) loads one byte from the address A"; - def "memory-write" (tuple [int; byte] @-> int) (module MemoryWrite) + def "memory-write" (tuple [int; byte] @-> int) "(memory-write A X) stores by X to A"; - def "memory-allocate" (tuple [int; int] // all byte @-> byte) (module MemoryAllocate) + def "memory-allocate" (tuple [int; int] // all byte @-> byte) "(memory-allocate P N V?) maps memory region [P,P+N), if V is provided, then fills the newly mapped region with the value V"; - def "get-current-program-counter" (unit @-> int) (module GetPC) + def "get-current-program-counter" (unit @-> int) "(get-current-program-counter) returns current program cunnter"; - def "+" (all a @-> a) (module Add) + def "+" (all a @-> a) "(+ X Y ...) returns the sum of arguments, or 0 if there are no arguments,"; - def "-" (all a @-> a) (module Sub) + def "-" (all a @-> a) "(- X Y Z ...) returns X - Y - Z - ..., or 0 if there are no arguments."; - def "*" (all a @-> a) (module Mul) + def "*" (all a @-> a) "(* X Y Z ...) returns the product of arguments or 0 if the list of arguments is empty"; - def "/" (all a @-> a) (module Div) + def "/" (all a @-> a) "(/ X Y Z ...) returns X / Y / Z / ... or 0 if the list of arguments is empty"; - def "s/" (all a @-> a) (module SDiv) + def "s/" (all a @-> a) "(s/ X Y Z ...) returns X s/ Y s/ Z s/ ... or 0 if the list of arguments is empty, where s/ is the signed division operation"; - def "mod" (all a @-> a) (module Mod) + def "mod" (all a @-> a) "(mod X Y Z ...) returns X % Y % Z % ... or 0 if the list of arguments is empty, where % is the modulo operation"; - def "signed-mod" (all a @-> a) (module SignedMod) + def "signed-mod" (all a @-> a) "(signed-mod X Y Z ...) returns X % Y % Z % ... or 0 if the list of arguments is empty, where % is the signed modulo operation"; - def "lshift" (tuple [a; b] @-> a) (module Lshift) + def "lshift" (tuple [a; b] @-> a) "(lshift X N) logically shifts X left by N bits"; - def "rshift" (tuple [a; b] @-> a) (module Rshift) + def "rshift" (tuple [a; b] @-> a) "(rshift X N) logically shifts X right by N bits"; - def "arshift" (tuple [a; b] @-> a) (module Arshift) + def "arshift" (tuple [a; b] @-> a) "(arshift X N) arithmetically shifts X right by N bits"; - def "=" (all a @-> bool) (module Equal) + def "=" (all a @-> bool) "(= X Y Z ...) returns true if all arguments are equal. True if the list of arguments is empty"; - def "/=" (all a @-> bool) (module NotEqual) + def "/=" (all a @-> bool) "(/= X Y Z ...) returns true if at least one argument is not equal to another argument. Returns false if the list of arguments is empty"; - def "logand" (all a @-> a) (module Logand) + def "logand" (all a @-> a) "(logand X Y Z ...) returns X & Y & Z & ... or 0 if the list of arguments is empty, where & is the bitwise AND operation. Returns ~0 if the list of arguments is empty"; - def "logor" (all a @-> a) (module Logor) + def "logor" (all a @-> a) "(logor X Y Z ...) returns X | Y | Z | ... or 0 if the list of arguments is empty, where | is the bitwise OR operation"; - def "logxor" (all a @-> a) (module Logxor) + def "logxor" (all a @-> a) "(logxor X Y Z ...) returns X ^ Y ^ Z ^ ... or 0 if the list of arguments is empty, where ^ is the bitwise XOR operation"; - def "concat" (all any @-> any) (module Concat) + def "concat" (all any @-> any) "(concat X Y Z ...) concatenates words X, Y, Z, ... into one big word"; - def "extract" (tuple [any; any; any] @-> any) (module Extract) + def "extract" (tuple [any; any; any] @-> any) "(extract HI LO X) extracts bits from HI to LO (including both) from the word X "; - def "lnot" (one a @-> a) (module Lnot) + def "lnot" (one a @-> a) "(lnot X) returns the one complement of X"; - def "not" (one a @-> a) (module Not) + def "not" (one a @-> a) "(not X) returns true if X is zero"; - def "neg" (one a @-> a) (module Neg) + def "neg" (one a @-> a) "(neg X) returns the two complement of X"; - def "<" (all a @-> bool) (module Less) + def "<" (all a @-> bool) "(< X Y Z ...) is true if the list of arguments is an strict ascending chain or if it is empty"; - def ">" (all a @-> bool) (module Greater) + def ">" (all a @-> bool) "(< X Y Z ...) is true if the list of arguments is a strict descending chain or if it is empty"; - def "<=" (all a @-> bool) (module LessEqual) + def "<=" (all a @-> bool) "(< X Y Z ...) is true if the list of arguments is an ascending chain or if it is empty"; - def ">=" (all a @-> bool) (module GreaterEqual) + def ">=" (all a @-> bool) "(< X Y Z ...) is true if the list of arguments is a descending chain or if it is empty"; - def "symbol-concat" (all sym @-> sym) (module SymbolConcat) + def "symbol-concat" (all sym @-> sym) "(symbol-concat X Y Z ...) returns a new symbol that is a concatenation of symbols X,Y,Z,... "; - def "set-symbol-value" (tuple [sym; a] @-> a) (module SetSymbol) + def "set-symbol-value" (tuple [sym; a] @-> a) "(set-symbol-value S X) sets the value of the symbol S to X. Returns X"; - def "reg-name" (one int @-> sym) (module RegName) - "(reg-name N) returns the name of the register with the index N" - ; + def "reg-name" (one int @-> sym) + "(reg-name N) returns the name of the register with the index N"; + def "symbol-of-string" (one int @-> sym) + "(symbol-of-string ptr) returns a symbol from a + null-terminated string." + ] end diff --git a/plugins/primus_lisp/primus_lisp_run.ml b/plugins/primus_lisp/primus_lisp_run.ml new file mode 100644 index 000000000..247decc29 --- /dev/null +++ b/plugins/primus_lisp/primus_lisp_run.ml @@ -0,0 +1,71 @@ +let doc = "Runs the Primus lisp program." + +open Core_kernel +open Bap_knowledge +open Bap_main +open Extension.Syntax + +open Bap.Std +open Bap_primus.Std + +type error = + | Unknown_arch of string + | Unknown_system of Knowledge.Name.t + | Conflict of Knowledge.Conflict.t + | Primus_exn of Primus.exn + +type Extension.Error.t += Failed of error + +module Spec = struct + open Extension + open Command + let entry = argument Type.(some string) + let arch = parameter Type.(string =? "x86_64") "arch" + let system = parameter Type.(string =? "bap:stubbed-executor") "system" + let t = args $entry $arch $system +end + +module Linker = Primus.Linker.Make(Primus.Analysis) + +let fail err = Error (Failed err) + +let () = Extension.Command.declare ~doc "eval-lisp" Spec.t @@ + fun entry arch system _ctxt -> + match Arch.of_string arch with + | None -> fail (Unknown_arch arch) + | Some arch -> + let code = Memmap.empty and data = Memmap.empty in + let input = Project.Input.create arch "" ~code ~data in + let proj = ok_exn (Project.create input) in + let start = Option.map entry ~f:(fun x -> Linker.exec (`symbol x)) in + let system = Knowledge.Name.of_string system in + let init = Knowledge.empty in + match Primus.System.Repository.find system with + | None -> fail (Unknown_system system) + | Some system -> + match Primus.System.run ?start system proj init with + | Error err -> fail (Conflict err) + | Ok (status,_proj,_) -> match status with + | Primus.Normal | Exn Primus.Interpreter.Halt -> Ok () + | Exn other -> fail (Primus_exn other) + +let string_of_error = function + | Unknown_arch name -> + sprintf + "Unknown architecture %S. List of supported architectures: %s." + name + (String.concat ~sep:", " @@ List.map ~f:Arch.to_string Arch.all) + | Unknown_system name -> + sprintf + "Unknown system %S, see `bap primus-systems` for the list of \ + known systems." (Knowledge.Name.to_string name) + | Conflict err -> + Format.asprintf "A conflict in the knowledge base: %a" + Knowledge.Conflict.pp err + | Primus_exn exn -> + sprintf "An unexpected Primus exception: %s" + (Primus.Exn.to_string exn) + +let () = Extension.Error.register_printer @@ function + | Failed err -> Some (string_of_error err) + | _ -> None diff --git a/plugins/primus_loader/primus_loader_basic.ml b/plugins/primus_loader/primus_loader_basic.ml index 74a3e420d..709cca298 100644 --- a/plugins/primus_loader/primus_loader_basic.ml +++ b/plugins/primus_loader/primus_loader_basic.ml @@ -20,7 +20,7 @@ module Make(Param : Param)(Machine : Primus.Machine.S) = struct let target = Machine.arch >>| target_of_arch - let make_addr addr = + let make_word addr = Machine.arch >>| Arch.addr_size >>| fun size -> Addr.of_int64 ~width:(Size.in_bits size) addr @@ -38,7 +38,7 @@ module Make(Param : Param)(Machine : Primus.Machine.S) = struct user process *) let setup_stack () = target >>= fun (module Target) -> - make_addr stack_base >>= fun bottom -> + make_word stack_base >>= fun bottom -> let top = Addr.(bottom -- stack_size) in Val.of_word bottom >>= fun bottom -> Env.set Target.CPU.sp bottom >>= fun () -> @@ -72,23 +72,24 @@ module Make(Param : Param)(Machine : Primus.Machine.S) = struct let load_segments () = Machine.project >>= fun proj -> - make_addr 0L >>= fun null -> + make_word 0L >>= fun null -> match get_segmentations proj with | Error _ -> assert false | Ok segs -> Machine.Seq.fold ~init:null segs ~f:(fun endp {Image.Scheme.addr; size; info=(_,w,x)} -> - make_addr addr >>= fun addr -> - let size = Int64.to_int_exn size in - Mem.allocate + make_word addr >>= fun lower -> + make_word Int64.(size-1L) >>= fun diff -> + let upper = Word.(lower + diff) in + Mem.add_region () ~lower ~upper ~readonly:(not w) ~executable:x - ~generator:(Generator.static 0) addr size >>| fun () -> - Addr.max endp Addr.(addr ++ size)) + ~generator:(Generator.static 0) >>| fun () -> + Addr.max endp Addr.(succ upper)) let map_segments () = Machine.project >>= fun proj -> - make_addr 0L >>= fun null -> + make_word 0L >>= fun null -> Memmap.to_sequence (Project.memory proj) |> Machine.Seq.fold ~init:null ~f:(fun endp (mem,tag) -> match Value.get Image.segment tag with @@ -141,7 +142,7 @@ module Make(Param : Param)(Machine : Primus.Machine.S) = struct Machine.arch >>= fun arch -> Machine.args >>= fun argv -> Machine.envp >>= fun envp -> - make_addr stack_base >>= fun sp -> + make_word stack_base >>= fun sp -> let endian = Arch.endian arch in let addr_size = Arch.addr_size arch in let argc = Array.length argv |> diff --git a/plugins/primus_mark_visited/primus_mark_visited_main.ml b/plugins/primus_mark_visited/primus_mark_visited_main.ml index ee2657eef..4078f9231 100644 --- a/plugins/primus_mark_visited/primus_mark_visited_main.ml +++ b/plugins/primus_mark_visited/primus_mark_visited_main.ml @@ -1,121 +1,30 @@ -open Core_kernel +let doc = " +# DESCRIPTION + +Provides the $(b,bap:mark-visited) and $(b,bap:report-visited) components. +" + +open Bap_main open Bap.Std -open Monads.Std open Bap_primus.Std include Self() -type state = { - visited : Tid.Set.t; - total : int; -} - -let count_blks p = (object - inherit [int] Term.visitor - method! enter_blk _ bs = bs + 1 -end)#run p 0 - - -let init_visited prog = - (object inherit [Tid.Set.t] Term.visitor - method! enter_blk blk visited = - if Term.has_attr blk Term.visited - then Set.add visited (Term.tid blk) - else visited - end)#run prog Tid.Set.empty - -let state = Primus.Machine.State.declare - ~name:"primus-mark-visitor" - ~uuid:"6edf3c44-3665-4ec1-8537-ef7fbba78d3d" - (fun p -> { - visited = init_visited (Project.program p); - total = count_blks (Project.program p) - }) - -type marker = { mark : 'a. 'a term -> 'a term} - -let dead = {mark = fun t -> Term.set_attr t Term.dead ()} -let live = {mark = fun t -> - Term.set_attr (Term.del_attr t Term.dead) Term.visited () - } - -let mark_block {mark} t = - mark t |> - Term.map def_t ~f:mark |> - Term.map jmp_t ~f:mark - -let marker p marker = object - inherit Term.mapper - method! map_blk t = - if not (p t) then t - else mark_block marker t -end - -let unvisited t = not (Term.has_attr t Term.visited) -let is_mem xs x = Set.mem xs (Term.tid x) - -module Main(Machine : Primus.Machine.S) = struct +module ReportProgress(Machine : Primus.Machine.S) = struct open Machine.Syntax - module Linker = Primus.Linker.Make(Machine) - - let visit t = - Machine.Global.update state ~f:(fun s -> - let s = { - s with - visited = Set.add s.visited (Term.tid t) - } in - report_progress ~stage:(Set.length s.visited - 1) ~total:s.total (); - s) - - let visit_stub (name,_) = - Linker.resolve_tid (`symbol name) >>= function - | None -> Machine.return () - | Some tid -> Machine.gets Project.program >>= fun prog -> - match Term.find sub_t prog tid with - | None -> Machine.return () - | Some sub -> - Term.enum blk_t sub |> - Machine.Seq.iter ~f:visit - - let mark_live _ = - Machine.Global.get state >>= fun {visited} -> - Machine.update (fun proj -> - let marker = marker (is_mem visited) live in - Project.with_program proj @@ - marker#run (Project.program proj)) - - let mark_dead _ = - Machine.update (fun proj -> - let marker = marker unvisited dead in - Project.with_program proj @@ - marker#run (Project.program proj)) + let report (visited,total) = + report_progress ~stage:(visited-1) ~total (); + Machine.return () let init () = - Machine.sequence [ - Primus.Interpreter.enter_blk >>> visit; - Primus.System.stop >>> mark_live; - Primus.Linker.Trace.lisp_call >>> visit_stub; - Primus.System.start >>> mark_dead; - ] + Bap_primus_track_visited.progress >>> report end - -open Config;; -manpage [ - `S "DESCRIPTION"; - `P - "Marks all terms visited by any Primus machine with the - [Term.visited] attribute and terms that weren't visited. - with [Term.dead]. Terms will not be marked visited during the - execution, but only after a system finishes." -] - -let () = when_ready (fun _ -> - Primus.Machine.add_component (module Main) [@warning "-D"]; - Primus.Components.register_generic "mark-visited" (module Main) - ~package:"bap" - ~desc:"Marks visited (by Primus) program terms with the \ - [Term.visited] attribute and unvisited with the \ - [Term.dead] attribute. Note, that the attributes \ - are attached only when the system exits") +let () = Extension.declare @@ fun _ -> + Bap_primus_track_visited.init (); + Primus.Components.register_generic ~package:"bap" "report-visited" + (module ReportProgress) + ~desc:"Reports progress when a new basic block is discovered."; + Primus.Machine.add_component (module ReportProgress) [@warning "-D"]; + Ok () diff --git a/plugins/primus_print/primus_print_main.ml b/plugins/primus_print/primus_print_main.ml index 454186e5a..70e618220 100644 --- a/plugins/primus_print/primus_print_main.ml +++ b/plugins/primus_print/primus_print_main.ml @@ -175,19 +175,18 @@ let start_monitoring {Config.get=(!)} = ] else Machine.return () - let init () = - setup_tracing () >>= fun () -> - parse_monitors !Param.monitors |> - List.iter ~f:(fun m -> - info "monitoring %s" (Primus.Observation.Provider.name m); - Stream.observe (Primus.Observation.Provider.data m) - (print_event out m)); - Machine.return () + let init () = setup_tracing () + end in Primus.Machine.add_component (module Monitor) [@warning "-D"]; Primus.Components.register_generic "observation-printer" (module Monitor) ~package:"bap" ~desc:"Prints the specified set of observations. Controlled via \ - the primus-print plugin." + the primus-print plugin."; + parse_monitors !Param.monitors |> + List.iter ~f:(fun m -> + info "monitoring %s" (Primus.Observation.Provider.name m); + Stream.observe (Primus.Observation.Provider.data m) + (print_event out m)) let () = Config.when_ready start_monitoring diff --git a/plugins/primus_promiscuous/primus_promiscuous_main.ml b/plugins/primus_promiscuous/primus_promiscuous_main.ml index 378cd1654..6106fc863 100644 --- a/plugins/primus_promiscuous/primus_promiscuous_main.ml +++ b/plugins/primus_promiscuous/primus_promiscuous_main.ml @@ -5,6 +5,8 @@ open Bap_primus.Std open Format include Self() +let package = "bap" + (* In a general case a block is terminated by a sequence of jumps: @@ -33,8 +35,6 @@ include Self() the interpreter requires a program to be in a trivial condition form (TCF). In TCF every jmp condition must be a single variable or a constant true. - - *) type assn = { @@ -100,7 +100,7 @@ end module Id = Monad.State.Multi.Id -module Main(Machine : Primus.Machine.S) = struct +module Forker(Machine : Primus.Machine.S) = struct open Machine.Syntax module Eval = Primus.Interpreter.Make(Machine) module Env = Primus.Env.Make(Machine) @@ -182,63 +182,41 @@ module Main(Machine : Primus.Machine.S) = struct | Jmp {up={me=blk}; me=jmp} -> fork_on_calls blk jmp | _ -> Machine.return () - - let default_page_size = 4096 - let default_generator = Primus.Generator.Random.Seeded.byte - - let map_page already_mapped addr = - let rec map len = - let last = Addr.nsucc addr (len - 1) in - already_mapped last >>= function - | true -> map (len / 2) - | false -> - Mem.allocate ~generator:default_generator addr len in - map default_page_size - - let trap () = - Linker.link ~name:Primus.Interpreter.pagefault_handler - (module TrapPageFault) - - let pagefault x = - Mem.is_mapped x >>= function - | false -> map_page Mem.is_mapped x >>= trap - | true -> - Mem.is_writable x >>= function - | false -> map_page Mem.is_writable x >>= trap - | true -> Machine.return () - - let mark_visited blk = Machine.Global.update state ~f:(fun t -> { t with visited = Set.add t.visited (Term.tid blk) }) - let free_vars proj = - Term.enum sub_t (Project.program proj) |> - Seq.map ~f:Sub.free_vars |> - Seq.to_list_rev |> - Var.Set.union_list - - let setup_vars = - Machine.get () >>= fun proj -> - Set.to_sequence (free_vars proj) |> - Machine.Seq.iter ~f:(fun var -> - Env.add var (Primus.Generator.static 0)) - - let ignore_division_by_zero = - Linker.link ~name:Primus.Interpreter.division_by_zero_handler - (module DoNothing) let init () = Machine.sequence [ - setup_vars; - ignore_division_by_zero; - Primus.Interpreter.pagefault >>> pagefault; Primus.Interpreter.leave_pos >>> step; Primus.Interpreter.leave_blk >>> mark_visited; ] end +module EnableDivisionByZero(Machine : Primus.Machine.S) = struct + module Linker = Primus.Linker.Make(Machine) + let init () = + Linker.link ~name:Primus.Interpreter.division_by_zero_handler + (module DoNothing) +end + +let legacy_promiscous_mode_components = [ + "var-randomizer"; + "mem-randomizer"; + "arg-randomizer"; + "promiscuous-path-explorer"; + "division-by-zero-handler"; + "limit"; +] + +let enable_legacy_promiscuous_mode () = + Primus.System.Repository.update ~package "legacy-main" ~f:(fun init -> + List.fold legacy_promiscous_mode_components ~init + ~f:(fun system component -> + Primus.System.add_component system ~package component)) + open Config;; let desc = @@ -257,13 +235,15 @@ manpage [ ] -let enabled = flag "mode" ~doc:"Enable the mode." - +let enabled = flag "mode" ~doc:"(DEPRECATED) Enable the mode." let () = when_ready (fun {get=(!!)} -> - if !!enabled then - Primus.Machine.add_component (module Main) [@warning "-D"]; - Primus.Components.register_generic - ~package:"bap" "promiscuous-mode" (module Main) - ~desc:("Enables the promiscuous mode. Requires the \ - Trivial Condition Form. " ^ desc)) + Primus.Components.register_generic "promiscuous-path-explorer" + (module Forker) ~package + ~desc:"Forces execution of all linearly independent paths \ + by forcefully flipping the branch conditions."; + Primus.Components.register_generic "division-by-zero-handler" + (module EnableDivisionByZero) ~package + ~desc:"Disables division by zero errors."; + + if !!enabled then enable_legacy_promiscuous_mode ()); diff --git a/plugins/primus_random/.merlin b/plugins/primus_random/.merlin new file mode 100644 index 000000000..73b2dc662 --- /dev/null +++ b/plugins/primus_random/.merlin @@ -0,0 +1,2 @@ +PKG zarith +REC diff --git a/plugins/primus_random/primus_random_main.ml b/plugins/primus_random/primus_random_main.ml new file mode 100644 index 000000000..13df96217 --- /dev/null +++ b/plugins/primus_random/primus_random_main.ml @@ -0,0 +1,614 @@ +let doc = {| +# DESCRIPTION + +Provides components for Primus state randomization and controls their +parameters. + +This module provides three highly customizable components for state +randomization: + +- bap:var-randomizer; + +- bap:mem-randomizer; + +- bap:arg-randomizer. + +The $(b,bap:var-randomizer) component randomizes unbound +variables. When this component is enabled a read operation from a +variable that wasn't set before will produce a random value instead +of terminating the program with the unbound value exception. + +The $(b,mem-randomizer) does the same for the Primus memory. It may +also preload pages of memory with user specified properties, as well +as hot-load pages on each page fault. This component is also disabling +the page protection mechanism, thus preventing the segmentation +faults. The memory protection can be re-enabled with the +$(b,--primus-random-preserve-protection) flag. + +The $(b,arg-randomizer) component traps the unresolved call exception +and enables randomization of the output parameters of the unresolved +functions. It employs the unresolved handler mechanism of the +Primus Linker library. For arguments it uses IR arg terms, which are +commonly provided by the api pass (make sure that you provide the +header file with prototypes for missing functions). Note, that if a +C ABI is detected by one of the ABI modules and function is missing a +prototype, the the $(b, int(void)) prototype is assumed. + +All three components use Primus generators to produce random or static +values. It is possible to set a specific generator for each variable, +subroutine argument, or memory region. The generators can be specified +with the $(b,--primus-random-generators) command line argument or put +in files and loaded with $(b,--primus-random-init). + +The specification is a list of generator specifications, with each +generator specification consisting of two parts: an optional +predicate and the generator parameters. The generators are checked in +order and the first matching generator is used. Each generator +specification is an s-expression. When no predicates or parameters are +specified, then it could be just the name of the generator, e.g., +$(b,random) - matches with all values and uses a uniform pseudo-random +generator, and $(b,static) also matches with any value and use +the static value (zero by default). The more general form of the +specification is + +``` +(? ...) +``` + +E.g., + +``` +((var RAX) random -5 5) +``` + +will create a generator which when the $(b,RAX) variable is read without +being set generates a random number uniformely distributed in the +range -5..5 (bounds included). If the predicate is omitted, then the +specification will match with any read or load target. There are two +kind of predicates, predicates for variables and predicates for memory +regions. The variable predicate accepts a list of variable names and +matches if the variable that is being read is in the list, the +underscore ($(b,_)) denotes the set of all possible variables (i.e., +it will match with any symbol), example, + +``` +((var RAX RDI RBX) static 42) ; if RAX or RDI or RBX is read return 42 +((var _) static 56) ; for all others return 56 +``` + +The memory predicate also accepts the underscore symbol ($(b,_)) as +the wildcard that will match with any address. It is also possible to +specify the memory interval or just a single address. The addresses +could be specified either as a numeral, that will match literally, or +as a variable, that will be evaluated for a concrete value, when the +machine is initialized. It is also possible to specify the a section +by name, e.g., $(b,:), which is a short-hand for the interval +denoted by two variables, $(b,bap:-lower) and +$(b,bap:-upper). Example, + +``` +((mem 0xC0000000 0xFFFFFFFF) static 0xA5A5A5A5) ; color the kernel space +((mem brk RSP) random -1 0x100) ; randomize the heap with -1, 0, ... 256 +((mem RSP 0xC0000000) static 0) ; zero the unitialized stack +((mem _) static 0x5A5A5A5A) ; color the rest of the memory +``` + +There are currently only two generators, the $(b,static) generator +that is parameterized by the list of values that will be enumerated +when this generator is used more than once (e.g., when it is used to +generate a subroutine argument or a memory region) , and the +$(b,random) generator that will produce a uniformely distributed +pseudo-random sequence of numbers. The initial value of the sequence, +(the seed) is the sum of the hash of the Machine identifier, the +sequential number of the generator (each generator has its own +number), the global seed value, specified with the +$(b,--primus-random-seed) option, and the local seed that could be +specified for each generator individually. To accomodate this variety +of options, the $(b,random) generator accepts from zero to three +parameters: + +- $(b,(random)) - the whole range of numbers; + +- $(b,(random )) - between $(b,0) and $(b,); + +- $(b,(random )) - between $(b,) and + $(b,); + +- $(b,(random )) - between $(b,) + and $(b,) with the specified $(b,) mixin. + +Generator specifications are take either directly from the command +line via the $(b,--primus-random-generators) option (in that case +don't forget to delimit it with quotes to prevent your shell program +from misinterpreting the parentheses) or from the initialization +files, specified with the $(b,--primus-random-init) option. If no +generators are specified, then is is the same as specifying the +$(b,random) generator, i.e., all data will be randomized by the +components using the uniform generator. + +# GRAMMAR + +Below is the formal grammar specified in the EBNF notation. Keep in +mind, that $(b, ",") stands for term concatenation in EBNF, and that +terms are separated with whitespaces. The specification syntax is a +subset of the s-expression grammar with common lexical rules, e.g., +multi-word atoms could be delimited with double quotes ($(b,")) and +comments start with the semicolon ($(b,;)). + +``` +specification = {generator}; +generator = + | "random" + | "static" + | "(" [predicate], constructor, ")"; +predicate = + | "_" + | "(", "var", "_", ")" + | "(", "var", ident, {ident}, ")" + | "(", "mem", "_", ")" + | "(", "mem", section, ")" + | "(", "mem", expression, [expression], ")" +constructor = + | "static", {numeral} + | "random", {numeral}; +expression = + | numeral + | ident; +section = ? a literal that starts with ':' ?; +numeral = ? a number of arbitrary length ?; +ident = ? a string of characters that is not a numeral or section ?; +``` + +# NOTES + +The section specification relies on the presence of the corresponding +runtime variables that denote their boundaries, which are expected to +be provided by the corresponding loader components. + +Also, this plugin has control only on generators created by the +three components that this plugin provides and has no control on the +user created generators (in particular the seed parameter has no +effect on user generators) or generators created by other plugins (for +example primus-loader and architecture specific plugins may have their +own randomization policies). + +For backward compatibility the +$(b,bap:var-randomizer),$(b,bap:mem-randomizer), and +$(b,bap:arg-randomizer) are added to the $(b,bap:legacy-main) system +when the $(b,--primus-promiscuous-mode) is enabled. + +|} + +open Core_kernel +open Bap_main +open Bap.Std +open Bap_primus.Std + + +let is_keyword = String.is_prefix ~prefix:":" +let is_numeral s = + String.length s > 0 && Char.is_digit s.[0] + +let parse_exp ~width s = + if is_numeral s then + let m = Bitvec.modulus width in + let x = Bitvec.(bigint (Z.of_string s) mod m) in + Bil.int (Word.create x width) + else Bil.var (Var.create s (Type.Imm width)) + +module Generator = struct + + type region = + | Default + | Address of string + | Section of string + | Interval of string * string + + type predicate = + | Any + | Var of string list + | Mem of region + + type name = + | Static + | Random + [@@deriving sexp] + + type generator = { + predicate : predicate; + distribution : name; + parameters : string list; + } + + let atom = function + | Sexp.Atom x -> x + | xs -> + invalid_argf "Expected a flat list of atoms, got %s" + (Sexp.to_string_hum xs) () + + let atoms = List.map ~f:atom + + let predicate_of_sexp : Sexp.t -> predicate = function + | Atom "_" -> Any + | List [Atom "var"; Atom "_"] -> Var [] + | List (Atom "var" :: vars) -> Var (atoms vars) + | List [Atom "mem"; Atom "_"] -> Mem Default + | List [Atom "mem"; Atom loc] -> + Mem (if is_keyword loc then Section loc else Address loc) + | List [Atom "mem"; Atom lower; Atom upper] -> + Mem (Interval (lower,upper)) + | other -> invalid_argf "Expected a generator specification got %s" + (Sexp.to_string_hum other) () + + let of_sexp : Sexp.t -> generator = function + | Atom ("static"|"random") as dis -> { + predicate = Any; + distribution = name_of_sexp dis; + parameters=[] + } + | List ((Atom ("static"|"random") as dis) :: ps) -> { + predicate = Any; + distribution = name_of_sexp dis; + parameters = atoms ps + } + | List (pred :: dis :: pars) -> { + predicate = predicate_of_sexp pred; + distribution = name_of_sexp dis; + parameters = atoms pars; + } + | other -> + invalid_argf "expected a generator specification, got %s" + (Sexp.to_string_hum other) () + + let pp_name ppf = function + | Static -> Format.fprintf ppf "Static" + | Random -> Format.fprintf ppf "Random" + + let pp_strings = Format.pp_print_list Format.pp_print_string + ~pp_sep:Format.pp_print_space + + let pp_predicate ppf = function + | Any -> Format.fprintf ppf "_" + | Var [] -> Format.fprintf ppf "(var _)" + | Var vars -> Format.fprintf ppf "(var %a)" pp_strings vars + | Mem Default -> Format.fprintf ppf "(mem _)" + | Mem (Address str | Section str) -> + Format.fprintf ppf "(mem %s)" str + | Mem (Interval (lower,upper)) -> + Format.fprintf ppf "(mem %s %s)" lower upper + + let pp ppf {predicate=p; distribution=d; parameters=ps} = + Format.fprintf ppf "(%a %a %a)" + pp_predicate p + pp_name d + pp_strings ps + + let to_string = Format.asprintf "%a" pp + + let from_file filename = + Sexp.load_sexps_conv_exn filename of_sexp + + let parse str = + Sexp.of_string str |> of_sexp + + let default = { + predicate=Any; + distribution=Random; + parameters=[] + } + + let t = + Extension.Type.define + ~name:"GEN" ~parse ~print:to_string default + + + let list = Extension.Type.(list t) + + let create_uniform ?(seed=0) ?width ps = + let min, max,local_seed = match ps with + | [] -> None, None, 0 + | [max] -> None, Some (int_of_string max), seed + | [min; max] -> + Some (int_of_string min), + Some (int_of_string max), + 0 + | [min; max; seed] -> + Some (int_of_string min), + Some (int_of_string max), + int_of_string seed + | _ -> + invalid_argf "Generator Uniform expects less \ + than 3 arguments" () in + Primus.Generator.Random.lcg (seed+local_seed) + ?width ?min ?max + + let create_const ?width = function + | [] -> Primus.Generator.static ?width 0 + | [x] -> Primus.Generator.static ?width (int_of_string x) + | xs -> + let xs = Array.of_list_map xs ~f:Bitvec.of_string in + let min = Array.min_elt xs ~compare:Bitvec.compare in + let max = Array.max_elt xs ~compare:Bitvec.compare in + Primus.Generator.of_iterator (module struct + type t = int + type dom = Bitvec.t + let min = Option.value_exn min + let max = Option.value_exn max + let next i = i + let value i = xs.(i mod Array.length xs) + end) 0 ~to_bitvec:ident ?width + + + let create ?seed ?width n ps = match n with + | Random -> create_uniform ?seed ?width ps + | Static -> create_const ?width ps + + let first_match ?seed ?width matches = List.find_map ~f:(fun s -> + if matches s.predicate + then Some (create ?seed ?width s.distribution s.parameters) + else None) + + let for_var ?seed ?width v = first_match ?seed ?width @@ function + | Var [] | Any -> true + | Var names -> List.mem names ~equal:String.equal (Var.name v) + | _ -> false +end + +let generators = Extension.Configuration.parameter + Generator.list "generators" + ~doc:"A list of generator specifications. The generators are + processed in order, with the first matching operator having + the precedence. This option also has precedence over the + generators specified via the initialization files." + +let init = Extension.Configuration.parameters + Extension.Type.(list file) "init" + ~doc: + "A list of generator initialization scripts. Files are processed + in order, with the first matching operator having the precedence." + +let seed = Extension.Configuration.parameter + Extension.Type.int "seed" + ~doc:"The seed that will be used to initialize all generators." + +let keep_protected = Extension.Configuration.flag + "preserve-protection" + ~doc: "Preserves page protection flags when a new page \ + is swapped in. When this flag is not set the \ + $(b,bap:mem-randomizer) will map missing memory pages \ + as writable." + +type arg_generators = { + args : Primus.Generator.t Var.Map.t +} + + +let debug_msg,post_msg = Primus.Observation.provide "random-debug" + ~inspect:sexp_of_string + +module Debug(Machine : Primus.Machine.S) = struct + open Machine.Syntax + let msg fmt = Format.kasprintf (fun msg -> + let msg = Format.asprintf "%s" msg in + Machine.Observation.make post_msg msg) fmt +end + +let main ctxt = + let open Extension.Syntax in + let generators = + ctxt-->generators @ + List.concat_map (ctxt-->init) ~f:(fun files -> + List.concat_map files ~f:Generator.from_file) @ + [Generator.default] in + let seed = ctxt-->seed in + let args = Primus.Machine.State.declare + ~uuid:"2d9a70fb-8433-4a53-a750-3151f9366cb6" + ~name:"generators-for-arguments" @@ fun proj -> + let prog = Project.program proj in + Term.enum sub_t prog |> + Seq.fold ~init:{args=Var.Map.empty} ~f:(fun init sub -> + Term.enum arg_t sub |> + Seq.fold ~init ~f:(fun {args} arg -> + if Arg.intent arg = Some In then {args} + else match Var.typ (Arg.lhs arg) with + | Unk | Mem _ -> {args} + | Imm width -> + let var = Arg.lhs arg in + match Generator.for_var ~seed ~width var generators with + | None -> {args} + | Some gen -> {args = Map.set args var gen})) in + let module RandomizeEnvironment(Machine : Primus.Machine.S) = struct + open Machine.Syntax + + module Env = Primus.Env.Make(Machine) + + let vars_collector = object + inherit [Set.M(Var).t] Term.visitor + method! enter_var v vs = Set.add vs v + end + + let randomize_vars _ = + Machine.get () >>= fun proj -> + vars_collector#run (Project.program proj) Var.Set.empty |> + Set.to_sequence |> + Machine.Seq.iter ~f:(fun var -> match Var.typ var with + | Mem _ | Unk -> Machine.return () + | Imm width -> + match Generator.for_var ~seed ~width var generators with + | None -> Machine.return () + | Some gen -> Env.add var gen) + let init () = + Primus.System.start >>> + randomize_vars + end in + + let module TrapPageFault(Machine : Primus.Machine.S) = struct + module Code = Primus.Linker.Make(Machine) + let exec = + Code.unlink (`symbol Primus.Interpreter.pagefault_handler) + end in + + + let module RandomizeMemory(Machine : Primus.Machine.S) = struct + open Machine.Syntax + + module Eval = Primus.Interpreter.Make(Machine) + module Memory = Primus.Memory.Make(Machine) + module Linker = Primus.Linker.Make(Machine) + + let allocate ?upper ~width lower generator = + let eval s = + Eval.exp (parse_exp ~width s) >>| Primus.Value.to_word in + + eval lower >>= fun lower -> + match upper with + | None -> Memory.allocate ~generator lower 1 + | Some upper -> + eval upper >>= fun upper -> + Memory.add_region ~generator ~lower ~upper () + + (* in memory the last added layer has precedence over the + previously added, so we start with the last specified region + and then add more specific on top of it. + *) + let initialize_regions _ = + Machine.arch >>= fun arch -> + let width = Arch.addr_size arch |> Size.in_bits in + List.rev generators |> + Machine.List.iter ~f:(function + | {Generator.predicate=Mem Default|Any} -> Machine.return () + | {predicate = Mem region; distribution; parameters} -> + let generator = + Generator.create ~seed ~width distribution parameters in + let lower,upper = match region with + | Address lower -> lower,None + | Section name -> + sprintf "bap%s-lower" name, + Some (sprintf "bap%s-upper" name) + | Interval (lower,upper) -> lower, Some upper + | Default -> assert false in + allocate ~width lower ?upper generator + | _ -> Machine.return ()) + + let default_page_size = 4096 + + let map_page ?generator already_mapped addr = + let rec map len = + let last = Addr.nsucc addr (len - 1) in + already_mapped last >>= function + | true -> map (len / 2) + | false -> + Memory.allocate ?generator addr len in + map default_page_size + + let trap () = + Linker.link ~name:Primus.Interpreter.pagefault_handler + (module TrapPageFault) + + let pagefault ?generator x = + Memory.is_mapped x >>= function + | false -> map_page ?generator Memory.is_mapped x >>= trap + | true -> + Memory.is_writable x >>= function + | false when not (ctxt-->keep_protected) -> + map_page ?generator Memory.is_writable x >>= trap + | _ -> Machine.return () + + let init () = + Machine.arch >>= fun arch -> + let width = Arch.addr_size arch |> Size.in_bits in + let generator = Generator.first_match ~seed ~width (function + | Mem Default | Any -> true + | _ -> false) generators in + Machine.sequence [ + Primus.Interpreter.pagefault >>> pagefault ?generator; + Primus.System.start >>> initialize_regions; + ] + end in + + let module PertubeOutputs(Machine : Primus.Machine.S) = struct + open Machine.Syntax + + module Eval = Primus.Interpreter.Make(Machine) + module Val = Primus.Value.Make(Machine) + module Env = Primus.Env.Make(Machine) + module Mem = Primus.Memory.Make(Machine) + module Gen = Primus.Generator.Make(Machine) + module Debug = Debug(Machine) + + let pertube_var gen v = match Var.typ v with + | Mem _ | Unk -> Machine.return () + | Imm m -> + let n = Primus.Generator.width gen in + Gen.word gen n >>| + Word.extract_exn ~hi:(m-1) >>= + Val.of_word >>= Eval.set v + + let is_entry sub blk = match Term.first blk_t sub with + | Some entry -> Term.same blk entry + | None -> false + + let pertube gen : exp -> unit Machine.t = function + | Var v -> pertube_var gen v + | Load (_,ptr,endian,size) -> + Eval.exp ptr >>= fun ptr -> + Gen.word gen (Size.in_bits size) >>= + Val.of_word >>= fun value -> + Eval.store ptr value endian size + | exp -> + Exp.free_vars exp |> + Set.to_sequence |> + Machine.Seq.iter ~f:(pertube_var gen) + + let exec = + Debug.msg "the unresolved handler is called" >>= fun () -> + Eval.pos >>= function + | Primus.Pos.Jmp {up={me=blk; up={me=sub}}} + when is_entry sub blk -> + Machine.Local.get args >>= fun {args} -> + Term.enum arg_t sub |> + Machine.Seq.iter ~f:(fun arg -> + match Map.find args (Arg.lhs arg) with + | Some gen -> + Debug.msg "pertubing argument %a" Arg.pp arg >>= fun () -> + pertube gen (Arg.rhs arg) + | None -> + Debug.msg + "skipping %a as there is no matching generator" + Arg.pp arg + >>= fun () -> + Machine.return ()) + | p -> + Debug.msg "called in a wrong position: %s" + (Primus.Pos.to_string p) + + end in + + let module HandleUnresolvedCalls(Machine : Primus.Machine.S) = struct + open Machine.Syntax + module Linker = Primus.Linker.Make(Machine) + + let name = Primus.Linker.unresolved_handler + + let init () = + Linker.link ~name (module PertubeOutputs) + end in + + Primus.Components.register_generic "var-randomizer" + (module RandomizeEnvironment) ~package:"bap" + ~desc:"Randomizes registers."; + + Primus.Components.register_generic "mem-randomizer" + (module RandomizeMemory) ~package:"bap" + ~desc:"Randomizes process memory."; + + Primus.Components.register_generic "arg-randomizer" + (module HandleUnresolvedCalls) ~package:"bap" + ~desc:"Randomizes output arguments of unbound procedures, as well + as prevents failures when such procedures are called by trapping + the unresolved handler."; + + Ok () + +let () = Extension.declare ~doc main + ~provides:["primus"] diff --git a/plugins/primus_random/primus_random_main.mli b/plugins/primus_random/primus_random_main.mli new file mode 100644 index 000000000..e69de29bb diff --git a/plugins/primus_region/primus_region_main.ml b/plugins/primus_region/primus_region_main.ml index 187a2d5db..ca928a68b 100644 --- a/plugins/primus_region/primus_region_main.ml +++ b/plugins/primus_region/primus_region_main.ml @@ -49,7 +49,7 @@ module Create(Machine : Primus.Machine.S) = struct }) >>| fun () -> reg end -module Contains(Machine : Primus.Machine.S) = struct +module Lower(Machine : Primus.Machine.S) = struct include Pre(Machine) [@@@warning "-P"] @@ -62,6 +62,33 @@ module Contains(Machine : Primus.Machine.S) = struct | Some ({lower},()) -> Machine.return lower) end +module Upper(Machine : Primus.Machine.S) = struct + include Pre(Machine) + [@@@warning "-P"] + + let run [reg; addr] = + Machine.Local.get state >>= (fun {regions} -> + match Map.find regions reg with + | None -> nil + | Some map -> + match Seq.to_list_rev (Regions.lookup map addr) with + | [] -> nil + | ({upper},())::_ -> Machine.return upper) +end + +module Count(Machine : Primus.Machine.S) = struct + include Pre(Machine) + [@@@warning "-P"] + + let run [reg] = + Machine.gets Project.arch >>= fun arch -> + let width = Size.in_bits @@ Arch.addr_size arch in + Machine.Local.get state >>= (fun {regions} -> + match Map.find regions reg with + | None -> nil + | Some map -> Value.of_int ~width (Regions.length map)) +end + module Move(Machine : Primus.Machine.S) = struct include Pre(Machine) [@@@warning "-P"] @@ -105,8 +132,8 @@ module Main(Machine : Primus.Machine.S) = struct def "region-contains" (tuple [sym; int] @-> int) - (module Contains) - {|(region-contains ID X) return if set ID has X. + (module Lower) + {|(region-contains ID X) return the region in ID that has X. Returns the lower bound of the first region that contains value X in the set of regions with the given ID. Returns nil @@ -121,6 +148,37 @@ module Main(Machine : Primus.Machine.S) = struct {|(region-move DST SRC P) moves all regions that contain the point P from the set SRC to the set DST. Returns nil if SRC didn't contain any such region, otherwise returns t. + |}; + + def "region-lower" (tuple [sym; int] @-> int) + (module Lower) + {|(region-lower ID X) the lower bound of region that contains X. + + Returns nil if ID doesn't exist or if it doesn't have a region + that includes X. + + This fucntion is an alias for REGION-CONTAINS. + See also, REGION-UPPER. + |}; + + def "region-upper" (tuple [sym; int] @-> int) + (module Upper) + {|(region-upper ID X) the upper bound of the region that contains X. + + Returns the upper bound of the region that contains point X or + nil if there is no such region or such set of regions. + + See also, REGION-LOWER.|}; + + def "region-count" (tuple [sym] @-> int) + (module Count) + {|(region-count ID) the total number of regions in the set ID. + + Counts the number of regions (including intersecting) stored + in the set of regions referenced by the symbol ID. + + Returns nil if there is no set with the given ID, otherwise + returns the number of regions in that set. |} ] end diff --git a/plugins/primus_symbolic_executor/.merlin b/plugins/primus_symbolic_executor/.merlin new file mode 100644 index 000000000..193629af6 --- /dev/null +++ b/plugins/primus_symbolic_executor/.merlin @@ -0,0 +1,3 @@ +REC +B ../../lib/bap_primus_track_visited +PKG z3 zarith \ No newline at end of file diff --git a/plugins/primus_symbolic_executor/lisp/symbolic-stdio.lisp b/plugins/primus_symbolic_executor/lisp/symbolic-stdio.lisp new file mode 100644 index 000000000..1815ff141 --- /dev/null +++ b/plugins/primus_symbolic_executor/lisp/symbolic-stdio.lisp @@ -0,0 +1,119 @@ +(require types) + +(declare (static opened-descriptors + opened-streams)) +(declare (context (component bap:symbolic-computer))) + +(defparameter *symbolic-io-buffer-size* 4096) +(defparameter *symbolic-stdin-size* 0x100) +(defparameter *symbolic-initial-file-size* 0x100) +(defconstant minimum-stream-number 0x8000) +(defconstant symbolic-stdin minimum-stream-number) + +(defun symbolic-open-input (name) + (let ((next-desc (+1 opened-descriptors)) + (desc (symbolic-value (symbol-concat name '-desc) + (bitwidth int) + next-desc))) + (symbolic-assume (or (= desc -1) + (= desc next-desc))) + (if (= desc -1) -1 + (set opened-descriptors next-desc) + (let ((size (symbolic-value (symbol-concat name '-size) + (word-width) + *symbolic-initial-file-size*)) + (data (symbolic-memory (symbol-concat name) + 0 (-1 size)))) + (dict-add 'symbolic-open-size desc size) + (dict-add 'symbolic-open-data desc data) + (dict-add 'symbolic-open-fpos desc 0) + (dict-add 'symbolic-open-name desc name) + desc)))) + + +(defun open (name flags) + (declare (external "open")) + (symbolic-open-input (symbol-of-string name))) + + +(defun symbolic-copy-to-concrete (memory cptr sptr len) + (while (> len 0) + (memory-write (+ cptr len -1) + (symbolic-memory-read memory (+ sptr len -1))) + (decr len))) + +(defun symbolic-copy-from-concrete (memory sdst csrc len) + (while (> len 0) + (symbolic-memory-write memory (+ sdst len -1) + (memory-read (+ csrc len -1))) + (decr len))) + + +(defun read (fd buf len) + (declare (external "read")) + (if (= fd -1) -1 + (let ((fpos (dict-get 'symbolic-open-fpos fd)) + (size (dict-get 'symbolic-open-size fd)) + (data (dict-get 'symbolic-open-data fd)) + (len (min len (- size fpos) *symbolic-io-buffer-size*))) + (symbolic-copy-to-concrete data buf fpos len) + (dict-add 'symbolic-open-fpos fd (+ fpos len)) + len))) + +(defun fread (ptr size n stream) + (declare (external "fread")) + (let ((r (read (fileno stream) buf (* n size)))) + (if (< r 0) r + (/ r size)))) + +(defun fopen (path mode) + (declare (external "fopen")) + (let ((name (symbol-of-string path)) + (desc (symbolic-open-input name))) + (if (= desc -1) 0 + (incr opened-streams) + (dict-add 'symbolic-streams opened-streams desc) + opened-streams))) + +(defun fdopen (fd mode) + (declare (external "fdopen")) + (if (< fd opened-descriptors) 0 + (incr opened-streams) + (dict-add 'symbolic-streams opened-streams fd) + opened-streams)) + +;; we return 0 for all unassociated streams thus treating +;; them as stdin. We could, instead, open some symbolic +;; file for an unknown stream. +(defun fileno (stream) + (declare (external "fileno")) + (if (= stream 0) -1 + (or (dict-get 'symbolic-streams stream) 0))) + +(defun fgetc (file) + (declare (external "fgetc" "getc")) + (let ((fd (fileno file))) + (if (= fd -1) -1 + (let ((fpos (dict-get 'symbolic-open-fpos fd)) + (size (dict-get 'symbolic-open-size fd)) + (data (dict-get 'symbolic-open-data fd))) + (if (= fpos size) -1 + (dict-add 'symbolic-open-fpos fd (+1 fpos)) + (symbolic-memory-read data fpos)))))) + +(defun getchar () + (declare (external "getchar")) + (fgetc symbolic-stdin)) + +(defun init-symbolic-stdin () + (dict-add 'symbolic-open-fpos 0 0) + (dict-add 'symbolic-open-size 0 *symbolic-initial-file-size*) + (dict-add 'symbolic-open-data 0 + (symbolic-memory 'stdin 0 (-1 *symbolic-initial-file-size*))) + (set opened-descriptors 2) + (dict-add 'symbolic-streams opened-streams 0) + (set opened-streams minimum-stream-number)) + + +(defmethod init () + (init-symbolic-stdin)) diff --git a/plugins/primus_symbolic_executor/lisp/symbolic-stdlib.lisp b/plugins/primus_symbolic_executor/lisp/symbolic-stdlib.lisp new file mode 100644 index 000000000..2964254d1 --- /dev/null +++ b/plugins/primus_symbolic_executor/lisp/symbolic-stdlib.lisp @@ -0,0 +1 @@ +(declare (context (component bap:symbolic-computer))) diff --git a/plugins/primus_symbolic_executor/primus_symbolic_executor_main.ml b/plugins/primus_symbolic_executor/primus_symbolic_executor_main.ml new file mode 100644 index 000000000..9fdeb03df --- /dev/null +++ b/plugins/primus_symbolic_executor/primus_symbolic_executor_main.ml @@ -0,0 +1,1036 @@ +open Core_kernel +open Bap.Std +open Bap_primus.Std +open Monads.Std +open Bap_main +include Self() + +let cutoff = Extension.Configuration.parameter + Extension.Type.(int =? 1) + "cutoff-level" + ~doc:"The number of times the same branch is retried." + +type memory = { + bank : Primus.Memory.Descriptor.t; + lower : Addr.t; + upper : Addr.t; +} [@@deriving compare, equal] + +let memories = Primus.Machine.State.declare + ~uuid:"15dbb89a-3bfb-421c-8b19-16605425c3f5" + ~name:"symbolic-memories" @@ fun _ -> + String.Map.empty + +module Bank = Primus.Memory.Descriptor +module Id = Monad.State.Multi.Id +let debug_msg,post_msg = Primus.Observation.provide "executor-debug" + ~inspect:sexp_of_string + +module Debug(Machine : Primus.Machine.S) = struct + open Machine.Syntax + let msg fmt = Format.kasprintf (fun msg -> + Machine.current () >>= fun id -> + let msg = Format.asprintf "%a: %s" Id.pp id msg in + Machine.Observation.make post_msg msg) fmt +end + +module Input : sig + type t + val ptr : Primus.Memory.Descriptor.t -> addr -> t + val var : var -> t + val to_symbol : t -> string + val size : t -> int + + module Make(Machine : Primus.Machine.S) : sig + val set : t -> Primus.Value.t -> unit Machine.t + end + include Base.Comparable.S with type t := t +end = struct + type t = + | Var of var + | Ptr of { + bank : Primus.Memory.Descriptor.t; + addr : addr; + } [@@deriving compare, sexp_of] + + let ptr bank addr = Ptr {bank; addr} + let var p = Var p + + let to_symbol = function + | Var v -> Format.asprintf "%a" Var.pp v + | Ptr {bank;addr} -> + Format.asprintf "%s[%a]" + (Primus.Memory.Descriptor.name bank) + Addr.pp_hex addr + + let size = function + | Ptr {bank} -> Primus.Memory.Descriptor.data_size bank + | Var v -> match Var.typ v with + | Imm m -> m + | _ -> 1 + + module Make(Machine : Primus.Machine.S) = struct + open Machine.Syntax + module Mems = Primus.Memory.Make(Machine) + module Env = Primus.Env.Make(Machine) + module Lisp = Primus.Lisp.Make(Machine) + + let allocate bank lower upper = + let width = Bank.data_size bank in + let seed = Hashtbl.hash (Bank.name bank) in + let generator = Primus.Generator.Random.lcg ~width seed in + Mems.add_region ~generator ~lower ~upper () + + let allocate_if_not bank addr = + Mems.is_writable addr >>= function + | true -> Machine.return () + | false -> + let name = Primus.Memory.Descriptor.name bank in + Machine.Global.get memories >>= fun memories -> + match Map.find memories name with + | None -> Lisp.failf "unknown symbolic memory %s" name () + | Some {lower; upper} -> allocate bank lower upper + + let set input value = match input with + | Ptr {bank; addr} -> + Mems.memory >>= fun current -> + Mems.switch bank >>= fun () -> + allocate_if_not bank addr >>= fun () -> + Mems.set addr value >>= fun () -> + Mems.switch current + | Var v -> + Env.set v value + end + + include Base.Comparable.Make(struct + type nonrec t = t [@@deriving compare, sexp_of] + end) +end + +module SMT : sig + type formula + type expr + type value + type model + + val formula : ?refute:bool -> expr -> formula + val inverse : formula -> formula + + val word : Word.t -> expr + val var : string -> int -> expr + + val binop : binop -> expr -> expr -> expr + val unop : unop -> expr -> expr + val extract : int -> int -> expr -> expr + val concat : expr -> expr -> expr + val ite : expr -> expr -> expr -> expr + val cast : cast -> int -> expr -> expr + + val check : formula list -> model option + + module Model : sig + type t = model + val get : model -> Input.t -> value option + end + + module Value : sig + type t = value + val to_word : value -> word + val to_formula : value -> formula + val to_string : value -> string + include Base.Comparable.S with type t := value + end + + module Formula : Base.Comparable.S with type t = formula + + val pp_expr : Format.formatter -> expr -> unit + val pp_formula : Format.formatter -> formula -> unit + val pp_value : Format.formatter -> value -> unit +end = struct + module Bitv = Z3.BitVector + module Bool = Z3.Boolean + module Expr = Z3.Expr + module Sort = Z3.Sort + + type expr = Expr.expr + type formula = expr + type value = expr + + let () = Z3.set_global_param "parallel.enable" "true" + + let ctxt = Z3.mk_context [ + "model", "true"; + "timeout", "16"; + ] + + let to_string = Expr.to_string + let pp_expr ppf expr = Format.fprintf ppf "%s" (to_string expr) + let pp_formula = pp_expr + let pp_value = pp_expr + + let coerce_shift op ctxt x y = + let sx = Bitv.get_size (Expr.get_sort x) + and sy = Bitv.get_size (Expr.get_sort y) in + if sx = sy then op ctxt x y + else + let y = Bitv.mk_zero_ext ctxt (sx-sy) y in + op ctxt x y + + let z3_of_binop : binop -> _ = function + | PLUS -> Bitv.mk_add + | MINUS -> Bitv.mk_sub + | TIMES -> Bitv.mk_mul + | DIVIDE -> Bitv.mk_udiv + | SDIVIDE -> Bitv.mk_sdiv + | MOD -> Bitv.mk_srem + | SMOD -> Bitv.mk_urem + | LSHIFT -> coerce_shift Bitv.mk_shl + | RSHIFT -> coerce_shift Bitv.mk_lshr + | ARSHIFT -> coerce_shift Bitv.mk_ashr + | AND -> Bitv.mk_and + | OR -> Bitv.mk_or + | XOR -> Bitv.mk_xor + | LT -> Bitv.mk_ult + | LE -> Bitv.mk_ule + | SLT -> Bitv.mk_slt + | SLE -> Bitv.mk_sle + | EQ -> fun ctxt x y -> + Bitv.mk_not ctxt @@ + Bitv.mk_redor ctxt @@ + Bitv.mk_xor ctxt x y + | NEQ -> fun ctxt x y -> + Bitv.mk_redor ctxt @@ + Bitv.mk_xor ctxt x y + + let do_simpl x = try Expr.simplify x None with + | Z3.Error "canceled" -> x + + let bit0 = Expr.mk_numeral_int ctxt 0 (Bitv.mk_sort ctxt 1) + let bit1 = Expr.mk_numeral_int ctxt 1 (Bitv.mk_sort ctxt 1) + + let is_bool = Bool.is_bool + + let bit_of_bool x = + if Bool.is_bool x + then do_simpl @@ Bool.mk_ite ctxt x bit1 bit0 + else x + + let bool_of_bit x = + do_simpl @@ Bool.mk_eq ctxt x bit1 + + let z3_of_unop : unop -> _ = function + | NEG -> Bitv.mk_neg + | NOT -> Bitv.mk_not + + let coerce_to_bit x = + if is_bool x then bit_of_bool x else x + + let coerce_to_bool x = + if is_bool x then x else bool_of_bit x + + + let simpl x = do_simpl x |> + coerce_to_bit + + let binop op x y = simpl (z3_of_binop op ctxt x y) + let unop op x = simpl (z3_of_unop op ctxt x) + + let word x = + let s = Bitv.mk_sort ctxt (Word.bitwidth x) in + let x = Word.to_bitvec x in + if Bitvec.fits_int x + then Expr.mk_numeral_int ctxt (Bitvec.to_int x) s + else + let x = Bitvec.to_bigint x in + Expr.mk_numeral_string ctxt (Z.to_string x) s + + let extract hi lo x = + let xs = Bitv.get_size (Expr.get_sort x) + and ns = hi-lo+1 in + simpl @@ + if ns > xs + then if lo = 0 + then Bitv.mk_zero_ext ctxt (ns-xs) x + else + Bitv.mk_extract ctxt hi lo @@ + Bitv.mk_zero_ext ctxt (ns-xs) x + else + Bitv.mk_extract ctxt hi lo x + + let concat x y = simpl @@ Bitv.mk_concat ctxt x y + + let ite c x y = simpl @@ Bool.mk_ite ctxt (coerce_to_bool c) x y + + let cast (c:cast) s x = + let old = Bitv.get_size (Expr.get_sort x) in + simpl @@ match c with + | SIGNED -> if old < s + then Bitv.mk_sign_ext ctxt (s-old) x + else extract (s-1) 0 x + | UNSIGNED -> if old < s + then Bitv.mk_zero_ext ctxt (s-old) x + else extract (s-1) 0 x + | HIGH -> extract (old-1) (old-s) x + | LOW -> extract (s-1) 0 x + + let var name size = + Expr.mk_const_s ctxt name (Bitv.mk_sort ctxt size) + + type model = { + model : Z3.Model.model; + } + + let inverse x = do_simpl@@Bool.mk_not ctxt x + + let formula ?(refute=false) expr = + let lhs = Expr.mk_numeral_int ctxt 0 (Expr.get_sort expr) in + let formula = Bool.mk_eq ctxt lhs expr in + if refute then do_simpl@@formula else inverse formula + + + module Model = struct + type t = model + let get {model} input = + let var = var (Input.to_symbol input) (Input.size input) in + match Z3.Model.eval model var false with + | Some x when Expr.is_numeral x -> Some x + | _ -> None + end + + let solver = Z3.Solver.mk_simple_solver ctxt + + let check assertions = + Z3.Solver.push solver; + Z3.Solver.add solver assertions; + let result = match Z3.Solver.check solver [] with + | exception Z3.Error "canceled" -> None + | UNSATISFIABLE | UNKNOWN -> None + | SATISFIABLE -> match Z3.Solver.get_model solver with + | None -> None + | Some model -> Some {model} in + Z3.Solver.pop solver 1; + result + + module Formula = struct + type t = formula + include Base.Comparable.Make(struct + type t = formula + let compare = Expr.compare + let sexp_of_t x = Sexp.Atom (to_string x) + end) + end + + module Value = struct + type t = value + let to_formula = ident + let to_bigint x = + let s = Expr.to_string x in + let len = String.length s in + if String.length s > 2 && Char.(s.[0] = '#') + then + let base = match s.[1] with + | 'b' -> 2 + | 'x' -> 16 + | _ -> failwithf "Not a literal value %s" s () in + Z.of_substring_base base s ~pos:2 ~len:(len-2) + else Z.of_string s + + let to_word x = + let s = Bitv.get_size (Expr.get_sort x) + and z = to_bigint x in + Word.create Bitvec.(bigint z mod modulus s) s + + let to_string x = Expr.to_string x + + include (Formula : Base.Comparable.S with type t := value) + end +end + +type executor = { + inputs : Set.M(Input).t; + values : SMT.expr Primus.Value.Id.Map.t; +} + +let executor = Primus.Machine.State.declare + ~uuid:"e21aa0fe-bc37-48e3-b398-ce7e764843c8" + ~name:"symbolic-executor-formulae" @@ fun _ -> { + values = Primus.Value.Id.Map.empty; + inputs = Set.empty (module Input); + } + + + +module Context : sig + type scope + + module Scope : sig + type t = scope + val declare : string -> scope + val user : scope + val path : scope + + include Base.Comparable.S with type t := t + end + + module Make(Machine : Primus.Machine.S) : sig + val add : scope -> SMT.formula -> unit Machine.t + val get : scope -> Set.M(SMT.Formula).t Machine.t + end +end = struct + + type scope = string + + type context = { + assertions : Set.M(SMT.Formula).t Map.M(String).t + } + + let context = Primus.Machine.State.declare + ~uuid:"9538b1fa-b6c0-464a-b11e-22377a10b0b6" + ~name:"symbolic-context" @@ fun _ -> { + assertions = Map.empty (module String); + } + + + module Scope = struct + let scopes = String.Hash_set.create () + + let declare scope = + if Hash_set.mem scopes scope + then invalid_argf "the scope named %s \ + is already declared" scope (); + scope + + let user = declare "user" + let path = declare "path" + include (String : Base.Comparable.S with type t = scope) + end + + module Make(Machine : Primus.Machine.S) = struct + open Machine.Syntax + + let add scope x = Machine.Local.update context ~f:(fun s -> { + assertions = Map.update s.assertions scope ~f:(function + | None -> Set.singleton (module SMT.Formula) x + | Some xs -> Set.add xs x) + }) + + let get scope = + Machine.Local.get context >>| fun s -> + match Map.find s.assertions scope with + | None -> Set.empty (module SMT.Formula) + | Some xs -> xs + end +end + +module Executor(Machine : Primus.Machine.S) : sig + val value : Primus.Value.t -> SMT.expr option Machine.t + val inputs : Input.t seq Machine.t + val init : unit -> unit Machine.t + val set_input : Input.t -> Primus.Value.t -> unit Machine.t +end = struct + open Machine.Syntax + + module Value = Primus.Value.Make(Machine) + module Mems = Primus.Memory.Make(Machine) + module Debug = Debug(Machine) + module Ctxt = Context.Make(Machine) + + let id = Primus.Value.id + + let value s x = Map.find s.values (id x) + let word x = SMT.word @@ Primus.Value.to_word x + let to_formula x = function + | None -> word x + | Some x -> x + + let lift1 x r f = + Machine.Local.get executor >>= fun s -> + match value s x with + | None -> Machine.return () + | Some x -> + Machine.Local.put executor { + s with + values = Map.add_exn s.values (id r) (f x) + } + + let lift2 x y r f = + Machine.Local.get executor >>= fun s -> + match value s x, value s y with + | None,None -> Machine.return () + | fx,fy -> + let x = to_formula x fx + and y = to_formula y fy in + Machine.Local.put executor { + s with + values = Map.add_exn s.values (id r) (f x y) + } + + let lift3 x y z r f = + Machine.Local.get executor >>= fun s -> + match value s x, value s y, value s z with + | None,None,None -> Machine.return () + | fx,fy,fz -> + let x = to_formula x fx + and y = to_formula y fy + and z = to_formula z fz in + Machine.Local.put executor { + s with + values = Map.add_exn s.values (id r) (f x y z) + } + + let on_binop ((op,x,y),z) = lift2 x y z @@ SMT.binop op + let on_unop ((op,x),z) = lift1 x z @@ SMT.unop op + let on_extract ((hi,lo,x),z) = lift1 x z @@ SMT.extract hi lo + let on_concat ((x,y),z) = lift2 x y z @@ SMT.concat + let on_ite ((c,x,y),z) = lift3 c x y z @@ SMT.ite + let on_cast ((c,w,x),z) = lift1 x z @@ SMT.cast c w + + let set_input origin x = + let id = Primus.Value.id x in + let size = Input.size origin in + let x = SMT.var (Input.to_symbol origin) size in + Machine.Local.update executor ~f:(fun s -> { + inputs = Set.add s.inputs origin; + values = Map.set s.values id x; + }) + + let on_memory_input (p,x) = + Mems.memory >>= fun desc -> + set_input (Input.ptr desc p) x + + let on_env_input (v,x) = set_input (Input.var v) x + + let inputs = + Machine.Local.get executor >>| fun s -> + Set.to_sequence s.inputs + + let value v = + Machine.Local.get executor >>| fun s -> + value s v + + let init () = Machine.sequence Primus.Interpreter.[ + binop >>> on_binop; + unop >>> on_unop; + extract >>> on_extract; + concat >>> on_concat; + ite >>> on_ite; + cast >>> on_cast; + Primus.Memory.generated >>> on_memory_input; + Primus.Env.generated >>> on_env_input; + ] +end + +module Paths(Machine : Primus.Machine.S) = struct + open Machine.Syntax + module Constraints = Context.Make(Machine) + module Executor = Executor(Machine) + module Value = Primus.Value.Make(Machine) + + let add_constraint x = + Executor.value x >>= function + | None -> Machine.return () + | Some v -> + Constraints.add Context.Scope.path @@ + SMT.formula ~refute:(Value.is_zero x) v + + let init () = + Primus.Interpreter.eval_cond >>> add_constraint +end + +type edge = { + blk : blk term; + src : jmp term; + dst : Jmp.dst; +} + +type task = { + constraints : Set.M(SMT.Formula).t; + inputs : Set.M(Input).t; + edge : edge option; + id : tid; +} + +type master = { + self : Id.t option; + ready : int; + tasks : task Map.M(Int).t; + tries : int Map.M(Tid).t; +} + +type worker = { + tid : tid; + task : task; +} + +let master = Primus.Machine.State.declare + ~uuid:"8d2b41d4-4852-40e9-917a-33f1f5af01a1" + ~name:"symbolic-executor-master" @@ fun _ -> { + self = None; + tasks = Int.Map.empty; + tries = Tid.Map.empty; (* queued or finished forks *) + ready = 0; + } + +let null = Tid.create () + +let worker = Primus.Machine.State.declare + ~uuid:"92f3042c-ba8f-465a-9d57-4c1b9ec7c186" + ~name:"symbolic-executor-worker" @@ fun _ -> { + tid = null; + task = { + id = null; + edge = None; + constraints = Set.empty (module SMT.Formula); + inputs = Set.empty (module Input); + }; + } + +let pp_dst ppf dst = match Jmp.resolve dst with + | First tid -> Format.fprintf ppf "%a" Tid.pp tid + | Second _ -> Format.fprintf ppf "unk" + +let pp_edge ppf {blk; src; dst} = + Format.fprintf ppf "%a(%a) -> %as" + Tid.pp (Term.tid blk) + Tid.pp (Term.tid src) pp_dst dst + +let pp_edge_option ppf = function + | None -> Format.fprintf ppf "sporadic" + | Some edge -> pp_edge ppf edge + +let pp_constraints ppf constrs = + Set.iter constrs ~f:(Format.fprintf ppf "%a@\n" SMT.pp_formula) + +let pp_task ppf {constraints=cs; edge; id} = + Format.fprintf ppf "%a: %a s.t.@\n%a" + Tid.pp id + pp_edge_option edge + pp_constraints cs + +let forker ctxt : Primus.component = + let cutoff = Extension.Configuration.get ctxt cutoff in + let module Forker(Machine : Primus.Machine.S) = struct + open Machine.Syntax + + module Executor = Executor(Machine) + module Eval = Primus.Interpreter.Make(Machine) + module Value = Primus.Value.Make(Machine) + module Visited = Bap_primus_track_visited.Set.Make(Machine) + module Constraints = Context.Make(Machine) + module Debug = Debug(Machine) + + let is_conditional jmp = match Jmp.cond jmp with + | Bil.Int _ -> false + | _ -> true + + (* is Some (blk,jmp) when the current position is a branch point *) + let branch_point = function + | Primus.Pos.Jmp {up={me=blk}; me=jmp} + when Term.length jmp_t blk > 1 && + is_conditional jmp -> + Some (blk,jmp) + | _ -> None + + + let other_dst ~taken blk jmp = + let is_other = if taken + then Fn.non (Term.same jmp) + else Term.same jmp in + Term.enum jmp_t blk |> + Seq.find_map ~f:(fun jmp -> + if not (is_other jmp) then None + else match Jmp.alt jmp with + | None -> Jmp.dst jmp + | dst -> dst) |> function + | Some dst -> dst + | None -> + failwithf "Broken branch %a at:@\n%a" + Jmp.pps jmp Blk.pps blk () + + let count table key = match Map.find table key with + | None -> 0 + | Some x -> x + + let incr table key = Map.update table key ~f:(function + | None -> 1 + | Some n -> n + 1) + + let is_visited visited dst = match Jmp.resolve dst with + | Second _ -> false + | First tid -> Set.mem visited tid + + let compute_edge ~taken pos = match branch_point pos with + | None -> None + | Some (blk,src) -> + let dst = other_dst ~taken blk src in + Some {blk;src;dst} + + let is_edge_dst_visited visited = function + | None -> false + | Some {dst} -> is_visited visited dst + + let append xs x = match Map.max_elt xs with + | None -> Map.add_exn xs 0 x + | Some (k,_) -> Map.add_exn xs (k+1) x + + let push_task task s = { + s with tasks = append s.tasks task; + } + + let on_cond constr = + let taken = Value.is_one constr in + Executor.value constr >>= function + | None -> Machine.return () + | Some constr -> + Machine.Local.get worker >>= fun self -> + Eval.pos >>= fun pos -> + let edge = compute_edge ~taken pos in + Visited.all >>= fun visited -> + Machine.Global.get master >>= fun s -> + if is_edge_dst_visited visited edge || + count s.tries self.tid > cutoff || + Set.mem self.task.constraints + (SMT.formula ~refute:(not taken) constr) + then Machine.return () + else + Constraints.get Context.Scope.user >>= fun cs -> + let constr = SMT.formula ~refute:taken constr in + let constraints = + let (++) = Set.union in + Set.add (cs ++ self.task.constraints) constr in + Executor.inputs >>= fun inputs -> + let inputs = + Seq.fold inputs ~init:self.task.inputs ~f:Set.add in + let task = {inputs; constraints; edge; id=self.tid} in + Machine.Global.update master ~f:(push_task task) + + let pop_task () = + let rec pop visited s ts = + match Map.max_elt ts with + | None -> None + | Some (k,t) -> + let ts = Map.remove ts k in + if count s.tries t.id > cutoff || + is_edge_dst_visited visited t.edge + then pop visited s ts + else match SMT.check (Set.to_list t.constraints) with + | None -> pop visited s ts + | Some m -> Some (m,t,ts) in + Machine.Global.get master >>= fun s -> + Visited.all >>= fun visited -> + match pop visited s s.tasks with + | None -> + let ready = s.ready + Map.length s.tasks in + report_progress ~stage:(ready-1) ~total:ready (); + Machine.Global.put master { + s with tasks = Int.Map.empty + } >>| fun () -> None + | Some (m,t,ts) -> + let queued = Map.length s.tasks in + let left = Map.length ts in + let processed = queued - left in + report_progress + ~stage:(s.ready + processed - 2) + ~total:(s.ready + queued) (); + Machine.Global.put master { + s with tasks = ts; + ready = s.ready + processed; + tries = incr s.tries t.id; + } >>| fun () -> + Some (m,t) + + let exec_task model task = + Debug.msg "SAT" >>= fun () -> + Machine.Local.update worker ~f:(fun t -> + {t with task}) >>= fun () -> + let string_of_input = Input.to_symbol in + let inputs = Set.to_sequence task.inputs in + let module Input = Input.Make(Machine) in + Machine.Seq.iter inputs ~f:(fun input -> + match SMT.Model.get model input with + | None -> Machine.return () + | Some value -> + Debug.msg "%s = %a" + (string_of_input input) + SMT.pp_value value >>= fun () -> + Value.of_word (SMT.Value.to_word value) >>= fun value -> + Executor.set_input input value >>= fun () -> + Input.set input value) + + let rec run_master system = + Machine.Global.get master >>= fun s -> + match s.self with + | None -> + Machine.current () >>= fun master_pid -> + Debug.msg "starting the master process with pid %a" + Id.pp master_pid >>= fun () -> + Machine.Global.put master { + s with self = Some master_pid + } >>= fun () -> + Machine.fork () >>= fun () -> + Machine.current () >>= fun client_pid -> + Debug.msg "the first fork returns at %a" + Id.pp client_pid >>= fun () -> + if Id.equal master_pid client_pid + then run_master system + else Machine.return () + | Some master_pid -> + pop_task () >>= function + | None -> + Debug.msg "Worklist is empty, finishing" >>= fun () -> + Eval.halt >>| never_returns + | Some (m,t) -> + Debug.msg "We have some tasks" >>= fun () -> + Machine.fork () >>= fun () -> + Machine.current () >>= fun client_pid -> + if Id.equal master_pid client_pid + then + Debug.msg "Client is finished, master is resumed" >>= fun () -> + run_master system + else + Debug.msg "Forked a new machine" >>= fun () -> + exec_task m t + + let update_id t = + Machine.Local.update worker ~f:(fun s -> { + s with + tid = t + }) + + let init () = Machine.sequence Primus.Interpreter.[ + eval_cond >>> on_cond; + enter_term >>> update_id; + Primus.System.start >>> run_master; + ] + end in (module Forker) + +let sexp_of_assert_failure (name,model,inputs) = + Sexp.List ( + Atom name :: + List.filter_map inputs ~f:(fun input -> + match SMT.Model.get model input with + | None -> None + | Some value -> Option.some @@ Sexp.List [ + Sexp.Atom (Input.to_symbol input); + Sexp.Atom (SMT.Value.to_string value) + ])) + +let assert_failure,failed_assertion = + Primus.Observation.provide "assert-failure" + ~inspect:sexp_of_assert_failure + ~desc:"occurs when a symbolic executor assertion doesn't hold" + +let to_word x = Primus.Value.to_word x +let to_int x = to_word x |> Word.to_int_exn + +module SymbolicPrimitives(Machine : Primus.Machine.S) = struct + open Machine.Syntax + + module Lisp = Primus.Lisp.Make(Machine) + module Mems = Primus.Memory.Make(Machine) + module Val = Primus.Value.Make(Machine) + module Env = Primus.Env.Make(Machine) + module Executor = Executor(Machine) + module Closure = Primus.Lisp.Closure.Make(Machine) + module Constraints = Context.Make(Machine) + module Debug = Debug(Machine) + + let addr_size arch_addr_size = function + | [addr_size; _data_size] -> Ok (to_int addr_size) + | [] | [_] -> Ok arch_addr_size + | _ -> Error "symbolic-memory: expects 3 to 5 arguments" + + let data_size = function + | [_addr_size; data_size] -> to_int data_size + | _ -> 8 + + let register_memory m = + let name = Bank.name m.bank in + Machine.Global.update memories ~f:(fun mem -> + Map.update mem name ~f:(function + | None -> m + | Some m' when equal_memory m m' -> m + | _ -> + invalid_argf "symbolic-memory: %s was previously \ + defined with different parameters" + name ())) + + let with_memory {bank} perform = + Mems.memory >>= fun current -> + Mems.switch bank >>= fun () -> + perform >>= fun x -> + Mems.switch current >>| fun () -> + x + + let open_bank id = + Machine.Global.get memories >>= fun mems -> + Val.Symbol.of_value id >>= fun name -> + match Map.find mems name with + | None -> + Lisp.failf "unknown memory %s" name () + | Some bank -> Machine.return bank + + let read id ptr = + open_bank id >>= fun bank -> + with_memory bank (Mems.get (to_word ptr)) + + let write id ptr data = + open_bank id >>= fun bank -> + with_memory bank (Mems.set (to_word ptr) data) >>| fun () -> + ptr + + let width default_width = function + | [] -> default_width + | s :: _ -> to_int s + + let generator width = function + | [_; x] -> + let x = Word.to_int_exn @@ Primus.Value.to_word x in + Primus.Generator.static ~width x + | _ -> Primus.Generator.static ~width 0 + + let arch_addr_size = + Machine.gets Project.arch >>| + Arch.addr_size >>| + Size.in_bits + + let create_value var rest = + arch_addr_size >>= fun default_width -> + let width = width default_width rest in + Val.Symbol.of_value var >>= fun name -> + let var = Var.create name (Imm width) in + Env.has var >>= function + | true -> Env.get var + | false -> + Env.add var (generator width rest) >>= fun () -> + Env.get var + + let create_memory id lower upper rest = + let lower = to_word lower and upper = to_word upper in + let data_size = data_size rest in + arch_addr_size >>= fun arch_addr_size -> + Val.Symbol.of_value id >>= fun name -> + Machine.Global.get memories >>= fun memories -> + if Map.mem memories name + then Machine.return id + else match addr_size arch_addr_size rest with + | Error err -> Lisp.failf "symbolic-memory: %s" err () + | Ok addr_size -> + let bank = Bank.create name ~addr_size ~data_size in + let memory = {bank; lower; upper} in + register_memory memory >>= fun () -> + let width = Bank.data_size bank in + let seed = Hashtbl.hash (Bank.name bank) in + let generator = Primus.Generator.Random.lcg ~width seed in + let region = Mems.add_region ~generator ~lower ~upper () in + with_memory memory region >>| fun () -> + id + + let assume assumptions = + Machine.List.iter assumptions ~f:(fun x -> + Executor.value x >>= function + | Some x -> + Constraints.add Context.Scope.user (SMT.formula x) + | None -> + (* should we raise on assert false? *) + if Val.is_zero x then + let false_ = SMT.word Word.b0 in + Constraints.add Context.Scope.user (SMT.formula false_) + else Machine.return ()) + >>= fun () -> + Val.b1 + + (* we can later add operators that manipulate the scopes + in which the assertion is checked *) + let assert_ name assertions = + Machine.Observation.post failed_assertion ~f:(fun report -> + Constraints.get Context.Scope.user >>= fun user -> + Constraints.get Context.Scope.path >>= fun path -> + let constraints = Set.to_list @@ Set.union user path in + Machine.List.fold assertions ~init:constraints + ~f:(fun constraints assertion -> + Executor.value assertion >>| function + | None -> constraints + | Some expr -> + + SMT.formula ~refute:true expr :: constraints) >>| + SMT.check >>= function + | None -> Machine.return () + | Some model -> + Val.Symbol.of_value name >>= fun name -> + Debug.msg "%s doesn't hold!" name >>= fun () -> + Executor.inputs >>| Seq.to_list >>= fun inputs -> + report (name,model,inputs)) >>= fun () -> + Val.b1 + + let run args = + Closure.name >>= fun name -> match name,args with + | "symbolic-value", id :: rest -> create_value id rest + | "symbolic-memory", (id :: lower :: upper :: rest) -> + create_memory id lower upper rest + | "symbolic-memory-read", [id; ptr] -> read id ptr + | "symbolic-memory-write", [id; ptr; data] -> write id ptr data + | "symbolic-assume", args -> assume args + | "symbolic-assert", name :: args -> assert_ name args + | _ -> Lisp.failf "%s: invalid number of arguments" name () +end + +module Primitives(Machine : Primus.Machine.S) = struct + module Lisp = Primus.Lisp.Make(Machine) + open Primus.Lisp.Type.Spec + + let def name types docs = + Lisp.define name (module SymbolicPrimitives) ~types ~docs + + let init () = Machine.sequence [ + def "symbolic-assume" (all bool @-> bool) + "Assumes the specified list of constraints."; + def "symbolic-assert" (one sym // all bool @-> bool) + "(assert NAME C1 ... CM) verifies the specified + list of assertions C1 and posts the assert-failure observation + for each condition that doesn't hold."; + def "symbolic-value" (one sym // all int @-> a) + "(symbolic-value NAME &rest) creates a new symbolic value. + Accepts up to two optional arguments. The first argument + denotes the bitwidth of the created value and the second is + the initial value."; + def "symbolic-memory" (tuple [sym; int; int] // all int @-> sym) + "(symbolic-memory NAME LOWER UPPER &rest) creates a new + symbolic memory region with the given NAME and LOWER and UPPER + bounds. The symbolic memory could be read and written with + the SYMBOLIC-MEMORY-READ and SYMBOLIC-MEMORY-WRITE primitives. + Optionally accepts one or two more arguments. If two optional + arguments are provided, then the first one stands for the + address bus size of the symbolic memory and the second for the + data bus size, all in bits. If only one is provided then it is + interpreted as the data bus size and the address size defaults + to the architecture-specific address size (e.g., 64 bits for + amd64). If none are provided then the address size is + architecture-specific and the data size defaults to 8 bits."; + def "symbolic-memory-read" (tuple [sym; int] @-> byte) + "(symbolic-memory-read MEM POS) reads the value of the + symbolic memory MEM at the specified position POS."; + def "symbolic-memory-write" (tuple [sym; int; byte] @-> byte) + "(symbolic-memory-write MEM POS X) writes X to the symbolic + memory MEM at the specified position POS." + ] +end + +let () = Extension.declare @@ fun ctxt -> + Primus.Components.register_generic "symbolic-computer" + (module Executor) ~package:"bap" + ~desc:"Computes a symbolic formula for each Primus value."; + Primus.Components.register_generic "symbolic-path-explorer" + (forker ctxt) ~package:"bap" + ~desc:"Computes a path constraint for each branch and forks a \ + new machine if the constraint is satisfiable."; + Primus.Components.register_generic "symbolic-lisp-primitives" + ~package:"bap" + ~desc:"Provides assume and assert primitives." + (module Primitives); + Primus.Components.register_generic "symbolic-path-constraints" + ~package:"bap" + ~desc:"tracks the path constraint and records them in the \ + machine's symbolic context" + (module Paths) ; + Ok () diff --git a/plugins/primus_systems/systems/core.asd b/plugins/primus_systems/systems/core.asd index 246857872..4e042b40e 100644 --- a/plugins/primus_systems/systems/core.asd +++ b/plugins/primus_systems/systems/core.asd @@ -2,7 +2,7 @@ :description "Executes a binary program." :components (bap:load-binary bap:program-loader - bap:x86-flag-initializer + bap:x86-registers-initializer bap:powerpc-init bap:observation-printer)) @@ -29,25 +29,42 @@ bap:base-lisp-machine) :components (bap:limit)) -(defsystem bap:greedy-promiscuous-executor - :description "Executes all linearly independent paths and never fails." +(defsystem bap:microexecutor-base + :description "The base system for microexecution systems." :depends-on (bap:terminating-stubbed-executor) :components (bap:greedy-scheduler - bap:promiscuous-mode bap:incident-location-recorder + bap:mark-visited + bap:report-visited + bap:var-randomizer + bap:mem-randomizer + bap:arg-randomizer bap:lisp-incidents - bap:mark-visited)) + bap:division-by-zero-handler)) +(defsystem bap:promiscuous-executor + :description "Executes all linearly independent paths and never fails." + :depends-on (bap:microexecutor-base) + :components (bap:promiscuous-path-explorer)) + +(defsystem bap:symbolic-executor + :description "Uses symbolic execution to analyze all feasible and + linearly independent paths." + :depends-on (bap:microexecutor-base) + :components (bap:symbolic-computer + bap:symbolic-path-explorer + bap:symbolic-path-constraints + bap:symbolic-lisp-primitives)) (defsystem bap:base-taint-analyzer - :description "Uses greedy-promiscuous-executor for taint analysis. + :description "Uses promiscuous-executor for taint analysis. No policy is specified" - :depends-on (bap:greedy-promiscuous-executor) + :depends-on (bap:promiscuous-executor) :components (bap:taint-primitives bap:taint-signals)) (defsystem bap:taint-analyzer - :description "Uses greedy-promiscuous-executor for taint analysis. + :description "Uses promiscuous-executor for taint analysis. Propagates taint by computation." :depends-on (bap:base-taint-analyzer) :components (bap:propagate-taint-by-computation)) @@ -62,15 +79,15 @@ (defsystem bap:exact-taint-analyzer - :description "Uses greedy-promiscuous-executor for taint analysis. + :description "Uses promiscuous-executor for taint analysis. Propagates taint exactly." :depends-on (bap:base-taint-analyzer) :components (bap:propagate-taint-exact)) (defsystem bap:constant-tracker - :description "Uses greedy-promiscuous-executor for constant tracking." - :depends-on (bap:greedy-promiscuous-executor) + :description "Uses promiscuous-executor for constant tracking." + :depends-on (bap:promiscuous-executor) :components (bap:constant-tracker-primitives bap:constant-tracker)) @@ -83,6 +100,6 @@ (defsystem bap:string-deobfuscator - :description "Uses greedy-promiscuous-executor to find obfuscated strings." - :depends-on (bap:greedy-promiscuous-executor) + :description "Uses promiscuous-executor to find obfuscated strings." + :depends-on (bap:promiscuous-executor) :components (bap:beagle-hunter)) diff --git a/plugins/primus_test/lisp/memcheck-malloc.lisp b/plugins/primus_test/lisp/memcheck-malloc.lisp index 71fce2317..c277790b6 100644 --- a/plugins/primus_test/lisp/memcheck-malloc.lisp +++ b/plugins/primus_test/lisp/memcheck-malloc.lisp @@ -3,8 +3,6 @@ (defmethod call (name ptr) (when (and ptr (= name 'free) (not (= ptr *malloc-zero-sentinel*))) - (unless (memcheck-is-tracked 'malloc ptr) - (memcheck-acquire 'malloc ptr 1)) (memcheck-release 'malloc ptr))) (defmethod loaded (ptr) @@ -19,9 +17,14 @@ (defmethod call (name dst src len) - (when (is-in name 'strncpy 'memmove 'memcpy 'memcmp 'strncmp) + (when (is-in name 'memmove 'memcpy 'memcmp) (check/both dst src len))) +(defmethod call (name dst src len) + (when (is-in name 'strncpy 'strncmp) + (check/strn* dst len) + (check/strn* src len))) + (defmethod call (name dst src c len) (when (= name 'memccpy) (check/both dst src len))) @@ -37,3 +40,6 @@ (defun check/both (dst src len) (memcheck-bounds 'malloc src len) (memcheck-bounds 'malloc dst len)) + +(defun check/strn* (str len) + (memcheck-bounds 'malloc str (min len (strlen str)))) diff --git a/plugins/primus_test/lisp/memcheck.lisp b/plugins/primus_test/lisp/memcheck.lisp index e08258940..5f304ab99 100644 --- a/plugins/primus_test/lisp/memcheck.lisp +++ b/plugins/primus_test/lisp/memcheck.lisp @@ -51,8 +51,14 @@ (when (and beg len) (let ((end (-1 (+ beg len))) (r1 (region-contains (symbol-concat 'memcheck/live heap) beg)) - (r2 (region-contains (symbol-concat 'memcheck/live heap) end))) - (when (not (= r1 r2)) + (r2 (region-contains (symbol-concat 'memcheck/live heap) end)) + (b1 (region-contains 'buffer beg)) + (b2 (region-contains 'buffer end))) + (unless b1 + (memcheck-acquire 'buffer beg len)) + (when (/= b1 b2) + (memcheck/report-out-of-bound b1 b2)) + (when (/= r1 r2) (memcheck/report-out-of-bound r1 r2))))) ;; Private @@ -73,10 +79,12 @@ (defun memcheck/report-out-of-bound (r1 r2) - (incident-report 'memcheck-out-of-bound - (dict-get 'memcheck/site/acquire r1) - (dict-get 'memcheck/site/acquire r2) - (incident-location))) + (let ((r1 (dict-get 'memcheck/site/acquire r1)) + (r2 (dict-get 'memcheck/site/acquire r2))) + (incident-report 'memcheck-out-of-bound + (or r1 r2) + (or r2 r1) + (incident-location)))) (defun memcheck/register (ptr site) (dict-add site ptr (incident-location))) diff --git a/plugins/primus_test/primus_test_main.ml b/plugins/primus_test/primus_test_main.ml index 8afa30bea..e790932bf 100644 --- a/plugins/primus_test/primus_test_main.ml +++ b/plugins/primus_test/primus_test_main.ml @@ -10,69 +10,208 @@ type id = Primus.Machine.id module Id = Monad.State.Multi.Id module Location = struct - type point = { - mach : id; - addr : Addr.t; - } + type point = Bitvec.t + + (* + + Each incident is represented by its name and a tuple of + locations. Each location is represented as a trace. It is not + requred, in general, that all traces that denote locations of an + incident should belong to the same path of execution (i.e., + traces could easily be disjoint). The last (the most recent) + point of the trace is called the _endpoint_ or just the location, + when it is obvious from the context that we mean only the + endpoint of the trace. + + Incidents of the same name are partitioned into locality classes, + so each incident belongs to one and only one class. We say that + an incident [i] subsumes an incident [j] iff the endpoint of each + location in [j] is is in the trace of a corresponding location in + [i]. + + Two incidents belong to the same class, if one the incidents + subsumes another. Of the set of incidents that belong to the same + class, an incident that subsumes all other incidents is selected + as a representative of the class. Note, that there could be more + than one incidents, as they may have equal locations, which + differ only in machine identifiers, which are not considered in + the substring relation. + + + When an incident is reported it either belongs to an existing + class or starts its own class. + + When an incident is an instance of an existing class , then + we make an observation: + [(incident-new-instance ... )] + + When an incident is not a member of any class a new class is + created and an observation is made: + + [(incident-new-class ... )]. + + When a newly discovered instance of a class is selected as a new + representative, in addition to the new-instance observation we + also make an observation + [(incident-new-representative ... )] + *) + + type id = {id : string} type trace = { - backtrace : point list + trace : point list; + switches : (int * id) list; + initial : id; + length : int; } type t = trace + type locations = { + points : Set.M(Bitvec_order).t list; + traces : trace list; + } type state = { - incidents : trace Primus.Value.Map.t; + locations : trace Primus.Value.Map.t; + incidents : locations Primus.Value.Map.t String.Map.t; } + let sexp_of_point {id} addr = + Sexp.Atom (asprintf "%s:%s" id @@ + Z.format "%x" (Bitvec.to_bigint addr)) - let sexp_of_point {mach; addr} = - Sexp.Atom (asprintf "%a:%s" - Id.pp mach - (Addr.string_of_value ~hex:true addr)) + let prefixed_trace prefix t = + let rec build id pos switches trace acc = match switches with + | (p,newid) :: switches when p = pos -> + build newid pos switches trace acc + | _ -> match trace with + | [] -> acc + | p::ps -> build id (pos+1) switches ps @@ + prefix id p :: acc in + build t.initial 0 t.switches (List.rev t.trace) [] - let sexp_of_t {backtrace} = - Sexp.List (List.map ~f:sexp_of_point backtrace) + let sexp_of_trace t = Sexp.List (prefixed_trace sexp_of_point t) - let sexp_of_id v = + let sexp_of_key v = Sexp.Atom (asprintf "%a" Word.pp_dec (Primus.Value.to_word v)) - let inspect (key,trace) = - Sexp.List [sexp_of_id key; sexp_of_t trace] + + let inspect_instance (name,key,locations) = + Sexp.List (Sexp.Atom name :: + sexp_of_key key :: + List.map locations ~f:sexp_of_key) let location,report_location = - Primus.Observation.provide ~inspect "incident-location" + Primus.Observation.provide "incident-location" ~desc:"Occurs when the location of a possible incident is created." + ~inspect:(fun (key,trace) -> + Sexp.List [sexp_of_key key; sexp_of_trace trace]) + + let new_instance,report_new_instance = + Primus.Observation.provide "incident-new-instance" + ~inspect:inspect_instance + + let new_class,report_new_class = + Primus.Observation.provide "incident-new-class" + ~inspect:inspect_instance + + let new_representative,report_new_representative = + Primus.Observation.provide "incident-new-representative" + ~inspect:inspect_instance let trace = Primus.Machine.State.declare - ~uuid:"41ed6b21-5ebd-4853-9797-30caff63c9ce" - ~name:"program-trace" - (fun _ -> {backtrace = []}) + ~uuid:"3663b645-87a6-4561-b75f-c447cdc221bc" + ~name:"program-trace" @@ fun _ -> { + trace = []; + switches = []; + initial = {id="unknown"}; + length = 0; + } let state = Primus.Machine.State.declare - ~uuid:"24bb6d34-089e-4c17-81da-e71001600531" - ~name:"incident-locations" - (fun _ -> {incidents = Primus.Value.Map.empty}) + ~uuid:"22d66ae9-82ad-4185-a1f8-5eb99f5569df" + ~name:"incident-locations" @@ fun _ -> { + incidents = String.Map.empty; + locations = Primus.Value.Map.empty; + } + + let push pc machine t = + let pc = Word.to_bitvec pc + and machine = Id.to_string machine in + match t.trace with + | [] -> { + trace = [pc]; + initial = {id=machine}; + switches = []; + length = 1; + } + | _ -> + let current = match t.switches with + | [] -> t.initial.id + | (_,{id})::_ -> id in + let t = if Bitvec.equal (List.hd_exn t.trace) pc + then t else { + t with trace = pc :: t.trace; length = t.length + 1; + } in + if String.equal current machine then t else { + t with + trace = pc :: t.trace; + switches = (t.length,{id=machine}) :: t.switches; + length = t.length + 1 + } + + let set_of_trace {trace} = Set.of_list (module Bitvec_order) trace + + let last_blk = function + | _ :: blk :: _ -> blk + | [blk] -> blk + | [] -> failwith "last_blk: empty trace" + + let is_member cls traces = + List.for_all2_exn traces cls.points ~f:(fun {trace} points -> + Set.mem points (last_blk trace)) + + let set_cls name id cls s = { + s with incidents = Map.update s.incidents name ~f:(function + | None -> Primus.Value.Map.singleton id cls + | Some classes -> Map.set classes id cls) + } + - let push {addr; mach} = function - | [] -> [{mach; addr}] - | x::_ as trace -> - if Addr.equal x.addr addr then trace - else {mach; addr}::trace + let classify {incidents; locations} name traces + ~new_representative + ~new_instance + ~new_class = + let traces = List.filter_map ~f:(Map.find locations) traces in + let points = List.map ~f:set_of_trace traces in + let cls' = {points; traces} in + match Map.find incidents name with + | None -> new_class cls' + | Some classes -> + Map.fold classes ~init:None ~f:(fun ~key ~data:cls found -> + match found with + | Some _ -> found + | None -> + if is_member cls traces + then Some (new_instance key) + else if is_member cls' cls.traces + then Some (new_representative key cls') + else None) |> function + | None -> new_class cls' + | Some other -> other module Record(Machine : Primus.Machine.S) = struct open Machine.Syntax module Eval = Primus.Interpreter.Make(Machine) let update_backtrace ~f = - Machine.Local.update trace ~f:(fun {backtrace} -> - {backtrace = f backtrace}) + Machine.Local.update trace ~f let record_callsite _ = Eval.pc >>= fun addr -> Machine.current () >>= fun mach -> - update_backtrace ~f:(push {addr; mach}) + update_backtrace ~f:(push addr mach) let init () = Primus.Interpreter.leave_blk >>> record_callsite @@ -90,15 +229,16 @@ module Location = struct let record = Eval.pc >>= fun addr -> Machine.current () >>= fun mach -> - Machine.Local.get trace >>= fun {backtrace} -> - Machine.Global.get state >>= fun {incidents} -> - next incidents >>= fun key -> - let trace = {backtrace = push {addr; mach} backtrace} in + Machine.Local.get trace >>= fun t -> + Machine.Global.get state >>= fun s -> + next s.locations >>= fun key -> + let t = push addr mach t in Machine.Global.put state { - incidents = Map.set incidents ~key ~data:trace + s with + locations = Map.set s.locations ~key ~data:t } >>= fun () -> Machine.Observation.post report_location ~f:(fun report -> - report (key,trace)) >>| fun () -> + report (key,t)) >>| fun () -> key end @@ -110,7 +250,7 @@ end module Incident = struct let inspect (name,locs) = - Sexp.List (Sexp.Atom name :: List.map ~f:Location.sexp_of_id locs) + Sexp.List (Sexp.Atom name :: List.map ~f:Location.sexp_of_key locs) let t,report = Primus.Observation.provide ~inspect "incident" @@ -119,14 +259,38 @@ module Incident = struct module Report(Machine : Primus.Machine.S) = struct open Machine.Syntax + open Location module Value = Primus.Value.Make(Machine) + let (!!) = Machine.Observation.make + + let next name incidents = match Map.find incidents name with + | None -> Value.of_int 1 ~width:63 + | Some classes -> match Map.max_elt classes with + | None -> Value.of_int 1 ~width:63 + | Some (k,_) -> Value.succ k + [@@@warning "-P"] let run (name :: locations) = - Machine.Observation.post report ~f:(fun report -> - Value.Symbol.of_value name >>= fun name -> - report (name,locations)) >>= fun () -> + Value.Symbol.of_value name >>= fun name -> + !!report (name,locations) >>= fun () -> + Machine.Global.get Location.state >>= fun s -> + Location.classify s name locations + ~new_representative:(fun id cls -> + !!report_new_instance (name,id,locations) >>= fun () -> + !!report_new_representative (name,id,locations) >>= fun () -> + Machine.Global.update Location.state + (Location.set_cls name id cls)) + ~new_instance:(fun id -> + !!report_new_instance (name,id,locations)) + ~new_class:(fun cls -> + next name s.incidents >>= fun id -> + !!report_new_class (name,id,locations) >>= fun () -> + !!report_new_instance (name,id,locations) >>= fun () -> + Machine.Global.update Location.state + (Location.set_cls name id cls)) + >>= fun () -> Value.b1 end @@ -141,8 +305,8 @@ module Lisp(Machine : Primus.Machine.S) = struct let init () = Machine.sequence [ - def "incident-location" (unit @-> a) (module Location.Create); - def "incident-report" (one sym // all a @-> b) (module Incident.Report) + def "incident-location" (unit @-> sym) (module Location.Create); + def "incident-report" (one sym // all sym @-> bool) (module Incident.Report) ] end diff --git a/plugins/primus_x86/primus_x86_loader.ml b/plugins/primus_x86/primus_x86_loader.ml index 2a119e533..ab614d158 100644 --- a/plugins/primus_x86/primus_x86_loader.ml +++ b/plugins/primus_x86/primus_x86_loader.ml @@ -79,18 +79,31 @@ module SetupPLT(Machine : Primus.Machine.S) = struct end -module InitializeFlags(Machine : Primus.Machine.S) = struct +module InitializeRegisters(Machine : Primus.Machine.S) = struct open Machine.Syntax module Env = Primus.Env.Make(Machine) + let registers (module Vars : X86_env.ModeVars) = Vars.[ + gdt; + ldt; + fs_base; + gs_base; + ] @ Array.to_list Vars.ymms + let zero = Primus.Generator.static 0 - let initialize_flags flags = - Machine.Seq.iter (Set.to_sequence flags) ~f:(fun reg -> + let initialize vars flags = + let registers = registers vars in + Seq.append (Seq.of_list registers) (Set.to_sequence flags) |> + Machine.Seq.iter ~f:(fun reg -> Env.add reg zero) + let init () = Machine.gets Project.arch >>= function - | `x86 -> initialize_flags IA32.flags - | `x86_64 -> initialize_flags AMD64.flags + | `x86 -> initialize (module X86_env.R32) IA32.flags + | `x86_64 -> initialize (module X86_env.R64) AMD64.flags | _ -> Machine.return () end + +module InitializeSpecialRegisters(Machine : Primus.Machine.S) = struct +end diff --git a/plugins/primus_x86/primus_x86_loader.mli b/plugins/primus_x86/primus_x86_loader.mli index b11612ab4..4f8bb1366 100644 --- a/plugins/primus_x86/primus_x86_loader.mli +++ b/plugins/primus_x86/primus_x86_loader.mli @@ -1,4 +1,4 @@ open Bap_primus.Std -module InitializeFlags : Primus.Machine.Component +module InitializeRegisters : Primus.Machine.Component module SetupPLT : Primus.Machine.Component diff --git a/plugins/primus_x86/primus_x86_main.ml b/plugins/primus_x86/primus_x86_main.ml index 2fabc84c4..d90028a0c 100644 --- a/plugins/primus_x86/primus_x86_main.ml +++ b/plugins/primus_x86/primus_x86_main.ml @@ -4,12 +4,12 @@ include Self() let init _ = Primus.Machine.add_component - (module Primus_x86_loader.InitializeFlags) + (module Primus_x86_loader.InitializeRegisters) [@warning "-D"]; Primus.Components.register_generic - ~package:"bap" "x86-flag-initializer" - (module Primus_x86_loader.InitializeFlags) - ~desc:"Intializes x86 flags to zero."; + ~package:"bap" "x86-registers-initializer" + (module Primus_x86_loader.InitializeRegisters) + ~desc:"Intializes all x86/x86-64 registers to zero."; Primus.Machine.add_component (module Primus_x86_loader.SetupPLT) diff --git a/plugins/run/run_main.ml b/plugins/run/run_main.ml index 4ef1a446d..bc9f989de 100644 --- a/plugins/run/run_main.ml +++ b/plugins/run/run_main.ml @@ -29,25 +29,29 @@ module Param = struct ~doc:"Program environemt as a comma separated list of VAR=VAL pairs";; let entry = param (list string) "entry-points" - ~doc:"Can be a list of entry points or a special keyword - $(b,all-subroutines) or $(b,marked-subroutines). An entry point - is either a string denoting a function name, a tid starting with - the $(b,%) percent, or an address in a hexadecimal format - prefixed with $(b,0x). When the option is specified, the Primus - Machine will start the execution from the specified entry - point(s). Otherwise the execution will be started from all - program terms that are marked with the [entry_point] - attribute. If there are several entry points, then the execution - will be started from all of them in parallel, i.e., by forking - the machine and starting each machine from its own entry - point. Consider enabling corresponding scheduler. If neither the + + ~doc:"Can be a list of $(i,entry points) or one of the following + keywords: $(b,all-subroutines), $(b,marked-subroutines), + $(b,only-queue). An $(i,entry point) is either a string denoting + a function name, a tid starting with the $(b,%) (percent) + symbol, or an address in a hexadecimal format prefixed with + $(b,0x). When the option is specified, the Primus Machine will + start the execution from the specified entry point(s). Otherwise + the execution will be started from all program terms that are + marked with the [entry_point] attribute. If there are several + entry points, then they will be executed each in a separate + machine or, if $(b,--run-in-separation) is specified, in a + separate system. In case when each entry point is run in a + separate machine it is necessary to add a scheduler component to + the system that is used to run the entry point. If neither the argument nor there any entry points in the program, then a function called $(b,_start) is called. If $(b,all-subroutines) - are specified then Primus will execute all subroutines in - the topological order. If $(b,marked-subroutines) is specified, - then Primus will execute the specified systems on all - subroutines that has the $(b,mark) attribute." - + are specified then Primus will execute all subroutines in the + topological order. If $(b,marked-subroutines) is specified, then + Primus will execute the specified systems on all subroutines + that has the $(b,mark) attribute. If the $(b,only-queue) is + specified, then only jobs already queued in the Primus Job Queue + will be run and no entry points will be searched in the project." let in_isolation = flag "in-isolation" ~doc:"Run each entry point as new system. @@ -74,6 +78,13 @@ module Param = struct ~doc:"Runs the specified Primus systems. If several systems \ are specified then runs all entry points for each \ specified system." + + let until_visited = flag "until-visited-all" + ~doc:"Runs Primus until all subroutines and blocks are visited. + When this mode is enabled and run plugin finishes it finds + the first unvisited subroutine (or if no such found the first + unvisited block) and spawns a new system with it as an entry + point. This continues until there are no more unvisited blocks." end let pp_id = Monad.State.Multi.Id.pp @@ -158,11 +169,12 @@ let parse_entry_points proj entry = | [] -> List.(entry_points prog >>| fun x -> `tid x) | xs -> List.(xs >>| name_of_entry (Project.arch proj)) -let parse_entry_points proj entries = - match entries,parse_entry_points proj entries with - | ["marked-subroutines"],[] -> [] - | _,[] -> [`symbol "_start"] - | _,xs -> xs +let parse_entry_points proj entries = match entries with + | ["only-queue"] -> [] + | _ -> match entries,parse_entry_points proj entries with + | ["marked-subroutines"],[] -> [] + | _,[] -> [`symbol "_start"] + | _,xs -> xs let exec x = Machine.current () >>= fun cid -> @@ -238,6 +250,7 @@ let is_visited proj = function | None -> true | Some blk -> Term.has_attr blk Term.visited + let enqueue_separate_jobs need_repeat envp args sys xs = List.iter xs ~f:(fun p -> Primus.Jobs.enqueue sys @@ -250,38 +263,89 @@ let enqueue_separate_jobs need_repeat envp args sys xs = else exec p end) +let finished = ref 0 +let total = ref 0 + let update_progress result = - let finished = List.length@@Primus.Jobs.finished result in - let total = finished + Primus.Jobs.pending () + 1 in - report_progress ~stage:finished ~total () + finished := List.length (Primus.Jobs.finished result) + !finished; + let total = !finished + Primus.Jobs.pending () + 1 in + report_progress ~stage:!finished ~total () -let on_success job _ _ result : Primus.Jobs.action = - info "job %s finished successfully" (Primus.Job.name job); +let on_success job status _ result : Primus.Jobs.action = update_progress result; - Continue + match status with + | Primus.Normal | Exn Primus.Interpreter.Halt -> + info "The job `%s' finished successfully" (Primus.Job.name job); + Continue + | Primus.Exn e -> + error "The job `%s' finished abnormally with an exception:@\n%s" + (Primus.Job.name job) + (Primus.Exn.to_string e); + Continue let on_failure job conflict result : Primus.Jobs.action = - info "job %s failed to converge and exited with conflict: %a" + info "The job `%s' failed to converge and exited with conflict: %a" (Primus.Job.name job) Knowledge.Conflict.pp conflict; update_progress result; Continue +let find_first_unvisited_sub prog = + Term.enum sub_t prog |> + Seq.find ~f:(fun sub -> match Term.first blk_t sub with + | None -> false + | Some blk -> not (Term.has_attr blk Term.visited)) + +let find_first_unvisited_blk prog = + Term.enum sub_t prog |> + Seq.find_map ~f:(fun sub -> + Graphlib.reverse_postorder_traverse (module Graphs.Ir) + (Sub.to_cfg sub) |> + Seq.find_map ~f:(fun blk -> + let blk = Graphs.Ir.Node.label blk in + if not (Term.has_attr blk Term.visited) + then Some blk + else None)) + let main {Config.get=(!)} proj = let open Param in let state = Toplevel.current () in + let run_until_visited = !until_visited in let enqueue_jobs = if !in_isolation then enqueue_separate_jobs else enqueue_super_job in let inputs = parse_entry_points proj !entry in - List.concat !systems |> List.iter ~f:(fun sys -> - let name = Knowledge.Name.read sys in - match Primus.System.Repository.find name with - | None -> invalid_argf "Unknown system: %s" sys () - | Some sys -> - enqueue_jobs !with_repetitions !envp !argv sys inputs) ; + let systems = + List.concat !systems |> List.map ~f:(fun sys -> + let name = Knowledge.Name.read sys in + match Primus.System.Repository.find name with + | None -> invalid_argf "Unknown system: %s" sys () + | Some sys -> sys) in + List.iter systems ~f:(fun sys -> + enqueue_jobs !with_repetitions !envp !argv sys inputs) ; report_progress ~total:(Primus.Jobs.pending ()) (); - let result = Primus.Jobs.run ~on_failure ~on_success proj state in - Toplevel.set (Primus.Jobs.knowledge result); - Primus.Jobs.project result + let enqueue_term p = + let p = `tid (Term.tid p) in + List.iter systems ~f:(fun sys -> + Primus.Jobs.enqueue sys + ~args:!argv ~envp:!envp + ~name:(Primus.Linker.Name.to_string p) + ~start:(exec p)) in + let rec run proj state = + let result = Primus.Jobs.run ~on_failure ~on_success proj state in + let state = Primus.Jobs.knowledge result in + Toplevel.set state; + let proj = Primus.Jobs.project result in + let prog = Project.program proj in + if run_until_visited + then match find_first_unvisited_sub prog with + | Some sub -> + enqueue_term sub; run proj state + | None -> match find_first_unvisited_blk prog with + | Some blk -> + enqueue_term blk; + run proj state + | None -> proj + else proj in + run proj state let deps = [ "trivial-condition-form" diff --git a/testsuite b/testsuite index a953c2a13..1e8de5328 160000 --- a/testsuite +++ b/testsuite @@ -1 +1 @@ -Subproject commit a953c2a131957cb5da30c582cc314c5c425b41c4 +Subproject commit 1e8de53286c75f418d67a2f9922232316a4d1c8e