Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

adds the extended lvalue assignment to Primus Interpreter #1498

Merged
merged 1 commit into from
Jun 2, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 23 additions & 2 deletions lib/bap_primus/bap_primus.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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 (_,<lvalue>,<lvalue>)
| Cast (_,_,<lvalue>)
| Extract (_,_,<lvalue>)
| Concat (_,_,<lvalue>)
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
Expand Down Expand Up @@ -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
Expand Down
53 changes: 52 additions & 1 deletion lib/bap_primus/bap_primus_interpreter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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 ()
Expand Down
1 change: 1 addition & 0 deletions lib/bap_primus/bap_primus_interpreter.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 1 addition & 9 deletions lib/bap_primus/bap_primus_lisp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down
14 changes: 2 additions & 12 deletions plugins/primus_lisp/primus_lisp_primitives.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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 ->
Expand All @@ -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 ->
Expand Down