From 71fe6602ef901d826454d3529506caf4eb181acc Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 23 Oct 2018 06:05:26 -0700 Subject: [PATCH] [sledge] Change Switch cases from Z.t to Exp.t Summary: This avoids (repeatedly) creating integer expressions during analysis. Reviewed By: mbouaziz Differential Revision: D10488405 fbshipit-source-id: 04b7ac336 --- sledge/src/control.ml | 5 ++--- sledge/src/llair/frontend.ml | 6 +----- sledge/src/llair/llair.ml | 12 ++++++------ sledge/src/llair/llair.mli | 8 ++++---- 4 files changed, 13 insertions(+), 18 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 03b3ed116..b5c7c65ce 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -185,15 +185,14 @@ let exec_term : Llair.t -> stack -> Domain.t -> Llair.block -> Work.x = | Switch {key; tbl; els} -> Vector.fold tbl ~f:(fun x (case, jump) -> - match Domain.assume state (Exp.eq key (Exp.integer case)) with + match Domain.assume state (Exp.eq key case) with | Some state -> exec_jump stk state block jump |> Work.seq x | None -> x ) ~init: ( match Domain.assume state (Vector.fold tbl ~init:(Exp.bool true) - ~f:(fun b (case, _) -> - Exp.and_ (Exp.dq key (Exp.integer case)) b )) + ~f:(fun b (case, _) -> Exp.and_ (Exp.dq key case) b )) with | Some state -> exec_jump stk state block els | None -> Work.skip ) diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index 0bfdee863..830b7e93f 100644 --- a/sledge/src/llair/frontend.ml +++ b/sledge/src/llair/frontend.ml @@ -1096,11 +1096,7 @@ let xlate_instr : let blk = Llvm.block_of_value (Llvm.operand instr ((2 * i) + 1)) in - let num = - match xlate_value x idx with - | Exp.Integer {data} -> data - | _ -> fail "xlate_instr: %a" pp_llvalue instr () - in + let num = xlate_value x idx in let dst = label_of_block blk in let args = jump_args x instr blk in let rest = xlate_cases (i + 1) in diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index 0471d6f69..a7e480e32 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -30,7 +30,7 @@ type 'a control_transfer = type jump = block control_transfer and term = - | Switch of {key: Exp.t; tbl: (Z.t * jump) vector; els: jump; loc: Loc.t} + | Switch of {key: Exp.t; tbl: (Exp.t * jump) vector; els: jump; loc: Loc.t} | Iswitch of {ptr: Exp.t; tbl: jump vector; loc: Loc.t} | Call of { call: Exp.t control_transfer @@ -130,13 +130,13 @@ 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.zero z -> + | [|(z, jmp)|] when Exp.is_false z -> pf "@[if %a@;<1 2>%a@ @[else@;<1 2>%a@]@]\t%a" Exp.pp key pp_goto 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) -> - Format.fprintf fs "%a: %a" Z.pp_print z pp_goto jmp )) + (Vector.pp "@ " (fun fs (case, jmp) -> + Format.fprintf fs "%a: %a" Exp.pp case pp_goto jmp )) tbl pp_goto els Loc.pp loc ) | Iswitch {ptr; tbl; loc} -> pf "@[<2>iswitch %a@ @[%a@]@]\t%a" Exp.pp ptr @@ -274,11 +274,11 @@ module Term = struct | Return _ | Throw _ | Unreachable -> assert true let goto ~dst ~loc = - Switch {key= Exp.integer Z.zero; tbl= Vector.empty; els= dst; loc} + Switch {key= Exp.bool false; tbl= Vector.empty; els= dst; loc} |> check invariant let branch ~key ~nzero ~zero ~loc = - let tbl = Vector.of_array [|(Z.zero, zero)|] in + let tbl = Vector.of_array [|(Exp.bool false, zero)|] in let els = nzero in Switch {key; tbl; els; loc} |> check invariant diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index 5cbd6c751..8008c68b8 100644 --- a/sledge/src/llair/llair.mli +++ b/sledge/src/llair/llair.mli @@ -75,9 +75,9 @@ type jump = block control_transfer (** Block terminators for function call/return or other control transfers. *) and term = private - | Switch of {key: Exp.t; tbl: (Z.t * jump) vector; els: jump; loc: Loc.t} - (** Invoke the [jump] in [tbl] associated with the integer [z] which - is equal to [key], if any, otherwise invoke [els]. *) + | Switch of {key: Exp.t; tbl: (Exp.t * jump) vector; els: jump; loc: Loc.t} + (** Invoke the [jump] in [tbl] associated with the integer expression + [case] which is equal to [key], if any, otherwise invoke [els]. *) | Iswitch of {ptr: Exp.t; tbl: jump vector; loc: Loc.t} (** Invoke the [jump] in [tbl] whose [dst] is equal to [ptr]. *) | Call of @@ -161,7 +161,7 @@ module Term : sig (** Construct a [Switch] representing a conditional branch. *) val switch : - key:Exp.t -> tbl:(Z.t * jump) vector -> els:jump -> loc:Loc.t -> term + key:Exp.t -> tbl:(Exp.t * jump) vector -> els:jump -> loc:Loc.t -> term val iswitch : ptr:Exp.t -> tbl:jump vector -> loc:Loc.t -> term