From 3a2ee882019bd9cdf12a4487694001d43f56b6e7 Mon Sep 17 00:00:00 2001 From: ivg Date: Wed, 1 Jun 2022 12:23:40 -0400 Subject: [PATCH] adds the extended lvalue assignment to Primus Interpreter And uses it to specify various argument passing mechanics. An expression is an lvalue if it is a register, a load (which is a generalization of a pointer), an ite of two lvalues, or a cast (including the extraction) of an lvalue. Or, more formally, ``` lvalue ::= Var _ | Load (_,_,_,_) | Ite (_,,) | Cast (_,_,) | Extract (_,_,) | Concat (_,_,) ``` The new `Interpreter.assign` primitive is now used to pass and return arguments to and from Primus Lisp interpreter, so now we can pass and return structures and other non-trivial objects. --- lib/bap_primus/bap_primus.mli | 25 ++++++++- lib/bap_primus/bap_primus_interpreter.ml | 53 ++++++++++++++++++- lib/bap_primus/bap_primus_interpreter.mli | 1 + lib/bap_primus/bap_primus_lisp.ml | 10 +--- plugins/primus_lisp/primus_lisp_primitives.ml | 14 +---- 5 files changed, 79 insertions(+), 24 deletions(-) diff --git a/lib/bap_primus/bap_primus.mli b/lib/bap_primus/bap_primus.mli index 3600602ad..07e0c5b4f 100644 --- a/lib/bap_primus/bap_primus.mli +++ b/lib/bap_primus/bap_primus.mli @@ -1943,9 +1943,10 @@ module Std : sig (** [pos m] current program position. *) val pos : pos m - (** [sub x] computes the subroutine [x]. *) + (** [sub x] evaluates the subroutine [x]. *) val sub : sub term -> unit m + (** [blk x] interprets the block [x]. *) val blk : blk term -> unit m @@ -1958,6 +1959,27 @@ module Std : sig (** [set var x] sets [var] to [x] *) val set : var -> value -> unit m + (** [assign lhs rhs] assigns [rhs] to an lvalue [lhs], fails + if [lhs] is not an lvalue. + + An lvalue is an expression that denotes a program + location. An expression is an lvalue, if it is a variable; + a load; a conditional expersion with lvalues on both branches, + or a cast, extract, concat, from an lvalue. + + {v + lvalue ::= Var _ + | Load (_,_,_,_) + | Ite (_,,) + | Cast (_,_,) + | Extract (_,_,) + | Concat (_,_,) + v} + + @since 2.5.0 *) + val assign : exp -> value -> unit m + + (** [binop op x y] computes a binary operation [op] on [x] and [y]. If [binop op x y] will involve the division by zero, then the @@ -2013,7 +2035,6 @@ module Std : sig [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 diff --git a/lib/bap_primus/bap_primus_interpreter.ml b/lib/bap_primus/bap_primus_interpreter.ml index 4737891c7..af90c4257 100644 --- a/lib/bap_primus/bap_primus_interpreter.ml +++ b/lib/bap_primus/bap_primus_interpreter.ml @@ -326,8 +326,8 @@ let cfi_violation_handler = "__primus_cfi_violation_handler" module Make (Machine : Machine) = struct open Machine.Syntax + open Machine.Let - module Eval = Eval.Make(Machine) module Memory = Primus.Memory.Make(Machine) module Env = Primus.Env.Make(Machine) module Code = Linker.Make(Machine) @@ -615,6 +615,57 @@ module Make (Machine : Machine) = struct | LittleEndian -> do_store a x s LOW HIGH | BigEndian -> do_store a x s HIGH LOW + + let infer x = match Type.infer x with + | Ok Imm m -> Machine.return m + | _ -> + failf "ill-typed expression, expected a bitvector: %a" + Exp.pps x () + + + let rec assign rhs x = match (rhs : exp) with + | Var v -> set v x + | Ite (c,yes,nay) -> + let* c = exp c in + if Value.is_one c then assign yes x else assign nay x + | Cast (LOW,part,v) -> + let* width = infer v in + let* y = exp v in + let* hi = cast HIGH (width-part) y in + let* x = concat hi x in + assign v x + | Cast (HIGH,part,v) -> + let* width = infer v in + let* y = exp v in + let* lo = cast LOW (width-part) y in + let* x = concat x lo in + assign v x + | Cast (_widen,_,v) -> + let* part = infer v in + let* x = cast LOW part x in + assign v x + | Extract (hi,lo,v) -> + let* size = infer v in + let* y = exp v in + let* hi = cast HIGH (size-hi-1) y in + let* lo = cast LOW lo y in + let* x = concat hi x in + let* x = concat x lo in + assign v x + | Load (mem,addr,endian,size) -> + exp mem >>= fun _ -> + exp addr >>= fun addr -> + store addr x endian size + | Concat (high,rest) -> + let* size = infer high in + let* hix = cast HIGH size x in + let* lox = cast LOW (Value.bitwidth x - size) x in + Machine.sequence [ + assign high hix; + assign rest lox; + ] + | exp -> failf "not an lvalue: %a" Exp.pps exp () + let update_pc t = match Term.get_attr t address with | None -> Machine.return () diff --git a/lib/bap_primus/bap_primus_interpreter.mli b/lib/bap_primus/bap_primus_interpreter.mli index fced34b7c..6087ab1fd 100644 --- a/lib/bap_primus/bap_primus_interpreter.mli +++ b/lib/bap_primus/bap_primus_interpreter.mli @@ -89,6 +89,7 @@ module Make (Machine : Machine) : sig val exp : exp -> value m val get : var -> value m val set : var -> value -> unit m + val assign : exp -> value -> unit m val binop : binop -> value -> value -> value m val unop : unop -> value -> value m val cast : cast -> int -> value -> value m diff --git a/lib/bap_primus/bap_primus_lisp.ml b/lib/bap_primus/bap_primus_lisp.ml index 60460db4f..b08491a07 100644 --- a/lib/bap_primus/bap_primus_lisp.ml +++ b/lib/bap_primus/bap_primus_lisp.ml @@ -682,15 +682,7 @@ module Make(Machine : Machine) = struct let eval_ret r = match ret with | None -> Machine.return () - | Some v -> match Arg.rhs v with - | Bil.Var reg -> Eval.set reg r - | Bil.(Cast (LOW, rsize, Var reg)) -> - let vsize = size_of_reg reg in - Eval.get reg >>= fun lhs -> - Eval.extract ~hi:(vsize-1) ~lo:rsize lhs >>= fun high -> - Eval.concat high r >>= fun r -> - Eval.set reg r - | e -> failf "an unsupported return semantics: %a" Exp.pps e () + | Some v -> Eval.assign (Arg.rhs v) r let exec = eval_args >>= fun bs -> diff --git a/plugins/primus_lisp/primus_lisp_primitives.ml b/plugins/primus_lisp/primus_lisp_primitives.ml index 6f9356ca5..c067dec13 100644 --- a/plugins/primus_lisp/primus_lisp_primitives.ml +++ b/plugins/primus_lisp/primus_lisp_primitives.ml @@ -25,6 +25,7 @@ module Closure(Machine : Primus.Machine.S) = struct type 'a m = 'a Machine.t open Machine.Syntax + open Machine.Let let failf = Lisp.failf @@ -220,7 +221,6 @@ module Closure(Machine : Primus.Machine.S) = struct | Some Out -> true | _ -> false - let eval_sub : value list -> 'x = function | [] -> failf "invoke-subroutine: requires at least one argument" () | sub_addr :: sub_args -> @@ -239,17 +239,7 @@ module Closure(Machine : Primus.Machine.S) = struct Machine.Seq.iter ~f:(fun (arg,x) -> let open Bil.Types in if not (is_out_intent arg) - then match Arg.rhs arg with - | Var v -> Eval.set v x - | Load (_,BinOp (op, Var sp, Int off),endian,size) -> - Eval.get sp >>= fun sp -> - Eval.const off >>= fun off -> - Eval.binop op sp off >>= fun addr -> - Eval.store addr x endian size - | exp -> - failf "%s: can't pass argument %s - %s %a" - "invoke-subroutine" (Arg.lhs arg |> Var.name) - "unsupported ABI" Exp.pps exp () + then Eval.assign (Arg.rhs arg) x else Machine.return ()) >>= fun () -> Linker.exec (`addr (Value.to_word sub_addr)) >>= fun () -> Machine.Seq.find_map args ~f:(fun arg ->