Skip to content

Commit 6983ef4

Browse files
gitolegivg
authored andcommitted
fixes IR graph for instructions with Bil.while (#1004)
The problem After #998, string instructions with the rep prefix are represented with the `Bil.while` statement and have the semantics of a pure data effect (and therefore do not break a basic block). However, when we reify while into IR we still have jump terms. And this wasn't anticipated by the sema lifter, which was glueing IR constituting one basic block, assuming that there will not be any complex control flow. This PR fixes this issue (which is not only specific to #998, this PR just triggered it, in general there could be other cases, when pure data effects are reified into non-simple control structures, cf. conditional moves). Solution Instead of just appending blocks, ensure that they are connected by an explicit jump.
1 parent 80f6254 commit 6983ef4

File tree

1 file changed

+13
-2
lines changed

1 file changed

+13
-2
lines changed

lib/bap_sema/bap_sema_lift.ml

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -64,11 +64,19 @@ module IrBuilder = struct
6464
Term.enum jmp_t b2 |> Seq.iter ~f:(Ir_blk.Builder.add_jmp b);
6565
Ir_blk.Builder.result b
6666

67+
(* [append xs ys]
68+
pre: the first block of [xs] is the exit block;
69+
pre: the first block of [ys] is the entry block;
70+
pre: the last block of [ys] is the exit block;
71+
post: the first block of [append xs ys] is the new exit block. *)
6772
let append xs ys = match xs, ys with
6873
| [],xs | xs,[] -> xs
6974
| x :: xs, y :: ys when def_only x ->
70-
List.rev_append ys (append_def_only x y :: xs)
71-
| xs, ys -> List.rev_append ys xs
75+
List.rev_append ys (append_def_only x y :: xs)
76+
| x::xs, y::_ ->
77+
let jmp = Ir_jmp.reify ~dst:(Ir_jmp.resolved @@ Term.tid y) () in
78+
let x = Term.append jmp_t x jmp in
79+
List.rev_append ys (x::xs)
7280

7381
let ir_of_insn insn = KB.Value.get Term.slot insn
7482

@@ -83,6 +91,9 @@ module IrBuilder = struct
8391
set_attributes jmp_t blk |>
8492
set_attributes def_t)
8593

94+
(* [lift_insn ?mem insn blks]
95+
pre: the first block of [blks] is the exit block;
96+
post: the first block of [lift_insn insn blks] is the new exit block. *)
8697
let lift_insn ?mem insn blks =
8798
append blks @@
8899
set_attributes ?mem insn (ir_of_insn insn)

0 commit comments

Comments
 (0)