[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

@@ -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, _) ->
+                   ~f:(fun b (case, _) -> Exp.and_ (Exp.dq key case) b ))
-                     Exp.and_ (Exp.dq key (Exp.integer case)) b ))
             with
           | Some state -> exec_jump stk state block els
           | None -> Work.skip )

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 =
+            let num = xlate_value x idx in
-              match xlate_value x idx with
-              | Exp.Integer {data} -> data
-              | _ -> fail "xlate_instr: %a" pp_llvalue instr ()
-            in
             let dst = label_of_block blk in
             let args = jump_args x instr blk in
             let rest = xlate_cases (i + 1) in

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) ->
+          (Vector.pp "@ " (fun fs (case, jmp) ->
-               Format.fprintf fs "%a: %a" Z.pp_print z pp_goto 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@ @[<hv>%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
 

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}
+  | Switch of {key: Exp.t; tbl: (Exp.t * jump) vector; els: jump; loc: Loc.t}
-      (** Invoke the [jump] in [tbl] associated with the integer [z] which
+      (** Invoke the [jump] in [tbl] associated with the integer expression
-          is equal to [key], if any, otherwise invoke [els]. *)
+          [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