Skip to content

Commit

Permalink
Tweak jumping and eval cond (#1142)
Browse files Browse the repository at this point in the history 
* tweaks eval-cond and jumping observations

Now the guard condition is computed from all outcoming edges, which
simplifies taint analysis and symbolic execution. This is true for
both jumping and eval-cond.

* simplifies and optimizes symbolic executor

now, when eval-cond takes into account path constraint (i.e., that
previous branches in the same basic block were not taken) we can
simplify the code of the symbolic executor that is responsible for
executing physical (i.e., represented with actual basic blocks)
braches as we now have to investigate only non-taken branches.

* removes the eval-cond signal from the Primus Lisp interface

We might put it back before the release, but right now it is the
easiest and less error-prone solution.

* bumps the timeout value in the symexec tests

Since functional tests take five times more time on the Mac OS X
machines, it is not surprising that we are occasionally hitting the
timeout on them, see also #1136. I hope that double would be enough.
  • Loading branch information
@ivg
ivg authored Jun 23, 2020
1 parent 303beb4 commit 582e9e4
Show file tree
Hide file tree
Showing 5 changed files with 125 additions and 76 deletions.
38 changes: 33 additions & 5 deletions lib/bap_primus/bap_primus.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1668,15 +1668,43 @@ module Std : sig

(** [jumping (cond,dest)] happens just before a jump to [dest]
is taken under the specified condition [cond].
Note: [cond] is always [true]
Note: the [cond] expression is always [true] and is computed
from the path constraints of all outcoming edges of a
block.
@since 1.5.0 *)
@since 1.5.0
@since 2.2.0 the condition is built from all edge
constraints. *)
val jumping : (value * value) observation

(** [eval_cond v] occurs every time the [cond] part of a jump is
evaluated.
(** [eval_cond c] occurs on every decision making operation.
@since 1.5.0 *)
The conditional expression is a one bit wide bitvector
could be true or false (contrary to the jumping
observation).
The [eval_cond] observation is posted for all outcoming
edges of a basic block with proper edge constraints.
For example, for a block
{v
when c1 goto d1
when c2 goto d2
goto d3
v}
which has three edges with constraints, correspondingly,
- [c1]
- [not c1 && c2]
- [not c1 && not c2 && true]
@since 1.5.0 introduced
@since 2.1.0 is posted by [branch] and [repeat] operations
@since 2.2.0 the condition is a disjunction of negations
of the previous conditions.
*)
val eval_cond : value observation

(** [undefined x] happens when a computation produces an
Expand Down
62 changes: 44 additions & 18 deletions lib/bap_primus/bap_primus_interpreter.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -666,15 +666,15 @@ module Make (Machine : Machine) = struct
then Machine.return stop
else body >>= fun _ -> repeat cnd body

let term return cls f t =
let term return cls f x t =
Machine.Local.get state >>= fun s ->
match Pos.next s.curr cls t with
| Error err -> Machine.raise err
| Ok curr ->
update_pc t >>= fun () ->
Machine.Local.update state (fun s -> {s with curr}) >>= fun () ->
enter cls curr t >>= fun () ->
f t >>= fun r ->
f x t >>= fun r ->
leave cls curr t >>= fun () ->
return r

Expand All @@ -684,8 +684,8 @@ module Make (Machine : Machine) = struct
!!will_halt () >>= fun () -> Machine.raise Halt

let (:=) v x = eval_exp x >>= set v
let def t = Def.lhs t := Def.rhs t
let def = term normal def_t def
let def () t = Def.lhs t := Def.rhs t
let def = term normal def_t def ()

let will_jump_to_tid cond dst =
Code.resolve_addr (`tid dst) >>= function
Expand Down Expand Up @@ -766,33 +766,59 @@ module Make (Machine : Machine) = struct
interrupt n >>= fun () ->
Code.exec (`tid r)

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)
type constr =
| Init
| Conj of Value.t
| Disj of Value.t * Jmp.t

let jmp constr t =
eval_exp (Jmp.cond t) >>= fun v ->
match constr, Word.is_one v.value with
| Init,true ->
!!on_cond v >>= fun () ->
Machine.return (Disj (v,t))
| Init,false ->
!!on_cond v >>= fun () ->
unop Bil.NOT v >>| fun u ->
Conj u
| Conj u,false ->
binop Bil.AND u v >>= !!on_cond >>= fun () ->
unop Bil.NOT v >>= fun v ->
binop Bil.AND u v >>| fun w ->
Conj w
| Conj u,true ->
binop Bil.AND u v >>= fun w ->
!!on_cond w >>| fun () ->
Disj (w,t)
| Disj (u,t),_ ->
unop Bil.NOT u >>= fun p ->
binop Bil.AND p v >>= !!on_cond >>= fun () ->
binop Bil.OR u v >>| fun w ->
Disj (w,t)

let jmp = term normal jmp_t jmp

let blk t =
let blk () t =
Machine.Seq.iter (Term.enum def_t t) ~f:def >>= fun () ->
Machine.Seq.find_map (Term.enum jmp_t t) ~f:jmp
Machine.Seq.fold ~init:Init (Term.enum jmp_t t) ~f:jmp

let finish = function
| None -> Machine.return () (* return from sub *)
| Some (cond,code) -> jump cond code
| Init | Conj _ -> Machine.return () (* return from sub *)
| Disj (cond,code) -> jump cond code

let blk : blk term -> unit m = 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
let arg_def () t = match Arg.intent t with
| None | Some (In|Both) -> Arg.lhs t := Arg.rhs t
| _ -> Machine.return ()

let arg_def = term normal arg_t arg_def
let arg_def = term normal arg_t arg_def ()

let arg_use t = match Arg.intent t with
let arg_use () t = match Arg.intent t with
| Some Out -> Arg.lhs t := Arg.rhs t
| _ -> Machine.return ()

let arg_use = term normal arg_t arg_use
let arg_use = term normal arg_t arg_use ()

let is_out_intent x = match Arg.intent x with
| Some Out -> true
Expand All @@ -808,7 +834,7 @@ module Make (Machine : Machine) = struct

let iter_args t f = Machine.Seq.iter (Term.enum arg_t t) ~f

let sub t = match Term.first blk_t t with
let sub () t = match Term.first blk_t t with
| None -> Machine.return ()
| Some entry ->
let name = Sub.name t in
Expand All @@ -825,7 +851,7 @@ module Make (Machine : Machine) = struct

let assume x = !!on_cond x

let sub = term normal sub_t sub
let sub = term normal sub_t sub ()
let pos = Machine.Local.get state >>| fun {curr} -> curr
let pc = Machine.Local.get state >>| fun {addr} -> addr
end
Expand Down
2 changes: 0 additions & 2 deletions plugins/primus_lisp/primus_lisp_main.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,8 +101,6 @@ module Signals(Machine : Primus.Machine.S) = struct
{|(written V X) is emitted when X is written to V|};
signal pc_change word one Type.(one int)
{|(pc-change PC) is emitted when PC is updated|};
signal eval_cond value one Type.(one bool)
{|(eval-cond V) is emitted after evaluating a conditional to V|};
signal jumping (value,value) pair Type.(tuple [bool; int])
{|(jumping C D) is emitted before jump to D occurs under the
condition C|};
Expand Down
97 changes: 47 additions & 50 deletions plugins/primus_symbolic_executor/primus_symbolic_executor_main.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -626,27 +626,10 @@ let forker ctxt : Primus.component =
(* 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 ->
when Term.length jmp_t blk > 1 ->
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
Expand All @@ -659,15 +642,18 @@ let forker ctxt : Primus.component =
| Second _ -> false
| First tid -> Set.mem visited tid

let compute_edge ~taken pos = match branch_point pos with
let compute_edge pos = match branch_point pos with
| None -> None
| Some (blk,src) ->
let dst = other_dst ~taken blk src in
Some {blk;src;dst}
let dst = match Jmp.alt src with
| None -> Jmp.dst src
| dst -> dst in
match dst with
| None -> None
| Some dst -> Some {blk; src; dst}

let is_edge_dst_visited visited = function
| None -> false
| Some {dst} -> is_visited visited dst
let is_edge_dst_visited visited {dst} =
is_visited visited dst

let append xs x = match Map.max_elt xs with
| None -> Map.add_exn xs 0 x
Expand All @@ -677,41 +663,52 @@ let forker ctxt : Primus.component =
s with tasks = append s.tasks task;
}

let on_cond constr =
let taken = Value.is_one constr in
Executor.value constr >>= function
let new_task ?edge ~refute constr =
let constr = SMT.formula ~refute constr
and contra = SMT.formula ~refute:(not refute) constr in
Machine.Local.get worker >>= fun self ->
if Set.mem self.task.constraints contra
then Machine.return ()
else
Constraints.get Context.Scope.user >>= fun cs ->
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 require cnd body =
if cnd then body ()
else Machine.return ()

let on_cond cond =
Executor.value cond >>= 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)
Eval.pos >>| compute_edge >>= function
| Some edge ->
require (Value.is_zero cond) @@ fun () ->
Visited.all >>= fun visited ->
require (not (is_edge_dst_visited visited edge)) @@ fun () ->
new_task ~refute:false ~edge constr
| None ->
Machine.Local.get worker >>= fun self ->
Machine.Global.get master >>= fun s ->
require (count s.tries self.tid < cutoff) @@ fun () ->
new_task ~refute:(Value.is_one cond) constr

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
if count s.tries t.id > cutoff || match t.edge with
| None -> false
| Some e -> is_edge_dst_visited visited e
then pop visited s ts
else match SMT.check (Set.to_list t.constraints) with
| None -> pop visited s ts
Expand Down
2 changes: 1 addition & 1 deletion testsuite
Submodule testsuite updated 1 files
+1 −1 bap.tests/symexec.exp

0 comments on commit 582e9e4

Please sign in to comment.