[sledge] Add Llair.Term.branch wrapper for Switch

Summary:
The main motivation is to factor out the code that determines the test
condition, e.g. to uniformly test `!= 0` vs `= 1`.

Also a convenience, and there are enough uses to make it worthwhile
and a readability improvement.

Reviewed By: mbouaziz

Differential Revision: D10488408

fbshipit-source-id: 520e843f3
master
Josh Berdine 6 years ago committed by Facebook Github Bot
parent 0e5239682d
commit e73e6c6448

@ -1082,11 +1082,10 @@ let xlate_instr :
let thn_lbl = label_of_block thn in
let thn_args = jump_args x instr thn in
let thn = Llair.Jump.mk thn_lbl thn_args in
let tbl = Vector.of_array [|(Z.one, thn)|] in
let els_lbl = label_of_block els in
let els_args = jump_args x instr els in
let els = Llair.Jump.mk els_lbl els_args in
terminal [] (Llair.Term.switch ~key ~tbl ~els ~loc) [] )
terminal [] (Llair.Term.branch ~key ~nzero:thn ~zero:els ~loc) [] )
| Switch ->
let key = xlate_value x (Llvm.operand instr 0) in
let cases =
@ -1200,18 +1199,16 @@ let xlate_instr :
else Exp.dq tiI ti
in
let key = xlate_filter 0 in
let thn = match_filter in
let tbl = Vector.of_array [|(Z.one, thn)|] in
Llair.Term.switch ~key ~tbl ~els:(jump (i + 1)) ~loc
Llair.Term.branch ~loc ~key ~nzero:match_filter
~zero:(jump (i + 1))
| _ -> fail "xlate_instr: %a" pp_llvalue instr () )
| _ (* catch *) ->
let clause = xlate_value x clause in
let key =
Exp.or_ (Exp.eq clause Exp.null) (Exp.eq clause ti)
in
let thn = jump_unwind typeid in
let tbl = Vector.of_array [|(Z.one, thn)|] in
Llair.Term.switch ~key ~tbl ~els:(jump (i + 1)) ~loc
Llair.Term.branch ~loc ~key ~nzero:(jump_unwind typeid)
~zero:(jump (i + 1))
in
let rec rev_blocks i z =
if i < num_clauses then

@ -130,9 +130,9 @@ let pp_term fs term =
| Switch {key; tbl; els; loc} -> (
match Vector.to_array tbl with
| [||] -> pf "@[%a@]\t%a" pp_goto els Loc.pp loc
| [|(z, jmp)|] when Z.equal Z.one z ->
| [|(z, jmp)|] when Z.equal Z.zero z ->
pf "@[if %a@;<1 2>%a@ @[else@;<1 2>%a@]@]\t%a" Exp.pp key pp_goto
jmp pp_goto els Loc.pp loc
els pp_goto jmp Loc.pp loc
| _ ->
pf "@[<2>switch %a@ @[%a@ else: %a@]@]\t%a" Exp.pp key
(Vector.pp "@ " (fun fs (z, jmp) ->
@ -277,6 +277,11 @@ module Term = struct
Switch {key= Exp.integer Z.zero; tbl= Vector.empty; els= dst; loc}
|> check invariant
let branch ~key ~nzero ~zero ~loc =
let tbl = Vector.of_array [|(Z.zero, zero)|] in
let els = nzero in
Switch {key; tbl; els; loc} |> check invariant
let switch ~key ~tbl ~els ~loc =
Switch {key; tbl; els; loc} |> check invariant

@ -157,6 +157,9 @@ module Term : sig
val goto : dst:jump -> loc:Loc.t -> term
(** Construct a [Switch] representing an unconditional branch. *)
val branch : key:Exp.t -> nzero:jump -> zero:jump -> loc:Loc.t -> term
(** Construct a [Switch] representing a conditional branch. *)
val switch :
key:Exp.t -> tbl:(Z.t * jump) vector -> els:jump -> loc:Loc.t -> term

Loading…
Cancel
Save