[sledge] Build: Wrap Llair library

Summary:
Refer to Llair modules using `Llair.` qualifier, except for in
`Frontend`, which makes so much use of `Llair` that it is now opened
(`Llair` only contains types and modules, so `open` is safe).

Reviewed By: jvillard

Differential Revision: D21720979

fbshipit-source-id: dd42075d9

sledge/bin/domain_itv.ml

@@ -49,17 +49,18 @@ let pp fs =
 let report_fmt_thunk = Fn.flip pp
 let init _gs = Abstract1.top (Lazy.force man) (Environment.make [||] [||])
 let apron_var_of_name = (fun nm -> "%" ^ nm) >> Apron.Var.of_string
-let apron_var_of_reg = Reg.name >> apron_var_of_name
+let apron_var_of_reg = Llair.Reg.name >> apron_var_of_name
 
-let rec apron_typ_of_llair_typ : Typ.t -> Texpr1.typ option = function
+let rec apron_typ_of_llair_typ : Llair.Typ.t -> Texpr1.typ option = function
-  | Pointer {elt= _} -> apron_typ_of_llair_typ Typ.siz
+  | Pointer {elt= _} -> apron_typ_of_llair_typ Llair.Typ.siz
   | Integer {bits= _} -> Some Texpr1.Int
   | Float {bits= 32; enc= `IEEE} -> Some Texpr1.Single
   | Float {bits= 64; enc= `IEEE} -> Some Texpr1.Double
   | Float {bits= 80; enc= `Extended} -> Some Texpr1.Extended
   | Float {bits= 128; enc= `IEEE} -> Some Texpr1.Quad
   | t ->
-      warn "No corresponding apron type for llair type %a " Typ.pp t () ;
+      warn "No corresponding apron type for llair type %a " Llair.Typ.pp t
+        () ;
       None
 
 let apron_of_q = Q.to_float >> fun fp -> Texpr1.Cst (Coeff.s_of_float fp)
@@ -168,20 +169,21 @@ and mk_bool_binop typ q op te1 te2 =
   else Texpr1.Cst (Coeff.i_of_int (-1) 0)
 
 let assign reg exp q =
-  [%Trace.call fun {pf} -> pf "{%a}@\n%a := %a" pp q Reg.pp reg Exp.pp exp]
+  [%Trace.call fun {pf} ->
+    pf "{%a}@\n%a := %a" pp q Llair.Reg.pp reg Llair.Exp.pp exp]
   ;
   let lval = apron_var_of_reg reg in
   ( match
       Option.bind
         ~f:(apron_texpr_of_llair_term (Term.of_exp exp) q)
-        (apron_typ_of_llair_typ (Reg.typ reg))
+        (apron_typ_of_llair_typ (Llair.Reg.typ reg))
     with
   | Some e ->
       let env = Abstract1.env q in
       let new_env =
         match
           ( Environment.mem_var env lval
-          , apron_typ_of_llair_typ (Reg.typ reg) )
+          , apron_typ_of_llair_typ (Llair.Reg.typ reg) )
         with
         | true, _ -> env
         | false, Some Texpr1.Int -> Environment.add env [|lval|] [||]
@@ -214,18 +216,19 @@ let exec_kill q r =
 (** perform a series [move_vec] of reg:=exp moves at state [q] *)
 let exec_move q move_vec =
   let defs, uses =
-    IArray.fold move_vec ~init:(Reg.Set.empty, Reg.Set.empty)
+    IArray.fold move_vec ~init:(Llair.Reg.Set.empty, Llair.Reg.Set.empty)
       ~f:(fun (defs, uses) (r, e) ->
-        (Reg.Set.add defs r, Exp.fold_regs e ~init:uses ~f:Reg.Set.add) )
+        ( Llair.Reg.Set.add defs r
+        , Llair.Exp.fold_regs e ~init:uses ~f:Llair.Reg.Set.add ) )
   in
-  assert (Reg.Set.disjoint defs uses) ;
+  assert (Llair.Reg.Set.disjoint defs uses) ;
   IArray.fold move_vec ~init:q ~f:(fun a (r, e) -> assign r e a)
 
 let exec_inst q i =
   match (i : Llair.inst) with
   | Move {reg_exps; loc= _} -> Some (exec_move q reg_exps)
   | Store {ptr; exp; len= _; loc= _} -> (
-    match Reg.of_exp ptr with
+    match Llair.Reg.of_exp ptr with
     | Some reg -> Some (assign reg exp q)
     | None -> Some q )
   | Load {reg; ptr; len= _; loc= _} -> Some (assign reg ptr q)
@@ -237,7 +240,7 @@ let exec_inst q i =
 
 (** Treat any intrinsic function as havoc on the return register [aret] *)
 let exec_intrinsic ~skip_throw:_ pre aret i _ =
-  let name = Reg.name i in
+  let name = Llair.Reg.name i in
   if
     List.exists
       [ "malloc"
@@ -264,14 +267,15 @@ let exec_intrinsic ~skip_throw:_ pre aret i _ =
   then Option.map ~f:(Option.some << exec_kill pre) aret
   else None
 
-type from_call = {areturn: Reg.t option; caller_q: t} [@@deriving sexp_of]
+type from_call = {areturn: Llair.Reg.t option; caller_q: t}
+[@@deriving sexp_of]
 
 let recursion_beyond_bound = `prune
 
 (** existentially quantify locals *)
 let post locals _ (q : t) =
   let locals =
-    Reg.Set.fold locals ~init:[] ~f:(fun a r ->
+    Llair.Reg.Set.fold locals ~init:[] ~f:(fun a r ->
         let v = apron_var_of_reg r in
         if Environment.mem_var q.env v then v :: a else a )
     |> Array.of_list
@@ -283,7 +287,7 @@ let retn _ freturn {areturn; caller_q} callee_q =
   match (areturn, freturn) with
   | Some aret, Some fret ->
       let env_fret_only =
-        match apron_typ_of_llair_typ (Reg.typ fret) with
+        match apron_typ_of_llair_typ (Llair.Reg.typ fret) with
         | None -> Environment.make [||] [||]
         | Some Texpr1.Int -> Environment.make [|apron_var_of_reg fret|] [||]
         | _ -> Environment.make [||] [|apron_var_of_reg fret|]
@@ -312,14 +316,16 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_
   if summaries then
     todo "Summaries not yet implemented for interval analysis" ()
   else
-    let mangle r = Reg.program (Reg.typ r) ("__tmp__" ^ Reg.name r) in
+    let mangle r =
+      Llair.Reg.program (Llair.Reg.typ r) ("__tmp__" ^ Llair.Reg.name r)
+    in
     let args = List.zip_exn formals actuals in
     let q' =
       List.fold args ~init:q ~f:(fun q (f, a) -> assign (mangle f) a q)
     in
     let callee_env =
       List.fold formals ~init:([], []) ~f:(fun (is, fs) f ->
-          match apron_typ_of_llair_typ (Reg.typ f) with
+          match apron_typ_of_llair_typ (Llair.Reg.typ f) with
           | None -> (is, fs)
           | Some Texpr1.Int -> (apron_var_of_reg (mangle f) :: is, fs)
           | _ -> (is, apron_var_of_reg (mangle f) :: fs) )
@@ -338,8 +344,8 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_
 let dnf q = [q]
 
 let resolve_callee lookup ptr q =
-  match Reg.of_exp ptr with
+  match Llair.Reg.of_exp ptr with
-  | Some callee -> (lookup (Reg.name callee), q)
+  | Some callee -> (lookup (Llair.Reg.name callee), q)
   | None -> ([], q)
 
 type summary = t

sledge/bin/frontend.ml

@@ -7,6 +7,8 @@
 
 (** Translate LLVM to LLAIR *)
 
+open Llair
+
 let pp_lltype fs t = Format.pp_print_string fs (Llvm.string_of_lltype t)
 
 (* WARNING: SLOW on instructions and functions *)
@@ -722,7 +724,7 @@ let pop_stack_frame_of_function :
     func ;
   let pop retn_loc =
     List.map entry_regs ~f:(fun reg ->
-        Llair.Inst.free ~ptr:(Exp.reg reg) ~loc:retn_loc )
+        Inst.free ~ptr:(Exp.reg reg) ~loc:retn_loc )
   in
   pop
 
@@ -792,27 +794,25 @@ let xlate_jump :
     | At_end blk -> fail "xlate_jump: %a" pp_llblock blk ()
   in
   let dst_lbl = label_of_block dst in
-  let jmp = Llair.Jump.mk dst_lbl in
+  let jmp = Jump.mk dst_lbl in
   match xlate_jump_ reg_exps (Llvm.instr_begin dst) with
   | [] -> (jmp, blocks)
   | reg_exps ->
-      let mov =
+      let mov = Inst.move ~reg_exps:(IArray.of_list_rev reg_exps) ~loc in
-        Llair.Inst.move ~reg_exps:(IArray.of_list_rev reg_exps) ~loc
-      in
       let lbl = find_name instr ^ ".jmp." ^ dst_lbl in
       let blk =
-        Llair.Block.mk ~lbl
+        Block.mk ~lbl
           ~cmnd:(IArray.of_array [|mov|])
-          ~term:(Llair.Term.goto ~dst:jmp ~loc)
+          ~term:(Term.goto ~dst:jmp ~loc)
       in
       let blocks =
         match List.find blocks ~f:(fun b -> String.equal lbl b.lbl) with
         | None -> blk :: blocks
         | Some blk0 ->
-            assert (Llair.Block.equal blk0 blk) ;
+            assert (Block.equal blk0 blk) ;
             blocks
       in
-      (Llair.Jump.mk lbl, blocks)
+      (Jump.mk lbl, blocks)
 
 (** An LLVM instruction is translated to a sequence of LLAIR instructions
     and a terminator, plus some additional blocks to which it may refer
@@ -821,20 +821,18 @@ let xlate_jump :
 type code = Llair.inst list * Llair.term * Llair.block list
 
 let pp_code fs (insts, term, blocks) =
-  Format.fprintf fs "@[<hv>@,@[%a%t@]%t@[<hv>%a@]@]"
+  Format.fprintf fs "@[<hv>@,@[%a%t@]%t@[<hv>%a@]@]" (List.pp "@ " Inst.pp)
-    (List.pp "@ " Llair.Inst.pp)
     insts
     (fun fs ->
       match term with
-      | Llair.Unreachable -> ()
+      | Unreachable -> ()
       | _ ->
           Format.fprintf fs "%t%a"
             (fun fs ->
               if List.is_empty insts then () else Format.fprintf fs "@ " )
-            Llair.Term.pp term )
+            Term.pp term )
     (fun fs -> if List.is_empty blocks then () else Format.fprintf fs "@\n")
-    (List.pp "@ " Llair.Block.pp)
+    (List.pp "@ " Block.pp) blocks
-    blocks
 
 let rec xlate_func_name x llv =
   match Llvm.classify_value llv with
@@ -864,7 +862,7 @@ let xlate_instr :
   let continue insts_term_to_code =
     [%Trace.retn
       fun {pf} () ->
-        pf "%a" pp_code (insts_term_to_code ([], Llair.Term.unreachable))]
+        pf "%a" pp_code (insts_term_to_code ([], Term.unreachable))]
       () ;
     continue insts_term_to_code
   in
@@ -884,7 +882,7 @@ let xlate_instr :
       let reg = xlate_name x instr in
       let exp = xlate instr in
       let reg_exps = IArray.of_array [|(reg, exp)|] in
-      emit_inst (Llair.Inst.move ~reg_exps ~loc)
+      emit_inst (Inst.move ~reg_exps ~loc)
   in
   let opcode = Llvm.instr_opcode instr in
   match opcode with
@@ -892,13 +890,13 @@ let xlate_instr :
       let reg = xlate_name x instr in
       let len = xlate_size_of x instr in
       let ptr = xlate_value x (Llvm.operand instr 0) in
-      emit_inst (Llair.Inst.load ~reg ~ptr ~len ~loc)
+      emit_inst (Inst.load ~reg ~ptr ~len ~loc)
   | Store ->
       let rand0 = Llvm.operand instr 0 in
       let exp = xlate_value x rand0 in
       let len = xlate_size_of x rand0 in
       let ptr = xlate_value x (Llvm.operand instr 1) in
-      emit_inst (Llair.Inst.store ~ptr ~exp ~len ~loc)
+      emit_inst (Inst.store ~ptr ~exp ~len ~loc)
   | Alloca ->
       let reg = xlate_name x instr in
       let rand = Llvm.operand instr 0 in
@@ -909,7 +907,7 @@ let xlate_instr :
       in
       assert (Poly.(Llvm.classify_type (Llvm.type_of instr) = Pointer)) ;
       let len = xlate_size_of x instr in
-      emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc)
+      emit_inst (Inst.alloc ~reg ~num ~len ~loc)
   | Call -> (
       let maybe_llfunc = Llvm.operand instr (Llvm.num_operands instr - 1) in
       let lltyp = Llvm.type_of maybe_llfunc in
@@ -934,7 +932,7 @@ let xlate_instr :
         | Ok () -> warn "ignoring uninterpreted %s %s" msg fname ()
         | Error _ -> () ) ;
         let reg = xlate_name_opt x instr in
-        emit_inst (Llair.Inst.nondet ~reg ~msg:fname ~loc)
+        emit_inst (Inst.nondet ~reg ~msg:fname ~loc)
       in
       (* intrinsics *)
       match xlate_intrinsic_exp fname with
@@ -943,7 +941,7 @@ let xlate_instr :
         match String.split fname ~on:'.' with
         | ["__llair_throw"] ->
             let exc = xlate_value x (Llvm.operand instr 0) in
-            emit_term ~prefix:(pop loc) (Llair.Term.throw ~exc ~loc)
+            emit_term ~prefix:(pop loc) (Term.throw ~exc ~loc)
         | ["__llair_alloc" (* void* __llair_alloc(unsigned size) *)] ->
             let reg = xlate_name x instr in
             let num_operand = Llvm.operand instr 0 in
@@ -953,14 +951,14 @@ let xlate_instr :
                 (xlate_value x num_operand)
             in
             let len = Exp.integer Typ.siz (Z.of_int 1) in
-            emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc)
+            emit_inst (Inst.alloc ~reg ~num ~len ~loc)
         | ["_Znwm" (* operator new(size_t num) *)]
          |[ "_ZnwmSt11align_val_t"
             (* operator new(unsigned long, std::align_val_t) *) ] ->
             let reg = xlate_name x instr in
             let num = xlate_value x (Llvm.operand instr 0) in
             let len = xlate_size_of x instr in
-            emit_inst (Llair.Inst.alloc ~reg ~num ~len ~loc)
+            emit_inst (Inst.alloc ~reg ~num ~len ~loc)
         | ["_ZdlPv" (* operator delete(void* ptr) *)]
          |[ "_ZdlPvSt11align_val_t"
             (* operator delete(void* ptr, std::align_val_t) *) ]
@@ -969,23 +967,23 @@ let xlate_instr :
           ]
          |["free" (* void free(void* ptr) *)] ->
             let ptr = xlate_value x (Llvm.operand instr 0) in
-            emit_inst (Llair.Inst.free ~ptr ~loc)
+            emit_inst (Inst.free ~ptr ~loc)
         | "llvm" :: "memset" :: _ ->
             let dst = xlate_value x (Llvm.operand instr 0) in
             let byt = xlate_value x (Llvm.operand instr 1) in
             let len = xlate_value x (Llvm.operand instr 2) in
-            emit_inst (Llair.Inst.memset ~dst ~byt ~len ~loc)
+            emit_inst (Inst.memset ~dst ~byt ~len ~loc)
         | "llvm" :: "memcpy" :: _ ->
             let dst = xlate_value x (Llvm.operand instr 0) in
             let src = xlate_value x (Llvm.operand instr 1) in
             let len = xlate_value x (Llvm.operand instr 2) in
-            emit_inst (Llair.Inst.memcpy ~dst ~src ~len ~loc)
+            emit_inst (Inst.memcpy ~dst ~src ~len ~loc)
         | "llvm" :: "memmove" :: _ ->
             let dst = xlate_value x (Llvm.operand instr 0) in
             let src = xlate_value x (Llvm.operand instr 1) in
             let len = xlate_value x (Llvm.operand instr 2) in
-            emit_inst (Llair.Inst.memmov ~dst ~src ~len ~loc)
+            emit_inst (Inst.memmov ~dst ~src ~len ~loc)
-        | ["abort"] | ["llvm"; "trap"] -> emit_inst (Llair.Inst.abort ~loc)
+        | ["abort"] | ["llvm"; "trap"] -> emit_inst (Inst.abort ~loc)
         (* dropped / handled elsewhere *)
         | ["llvm"; "dbg"; ("declare" | "value")]
          |"llvm" :: ("lifetime" | "invariant") :: ("start" | "end") :: _ ->
@@ -1033,13 +1031,13 @@ let xlate_instr :
                     xlate_value x (Llvm.operand instr i) )
               in
               let areturn = xlate_name_opt x instr in
-              let return = Llair.Jump.mk lbl in
+              let return = Jump.mk lbl in
-              Llair.Term.call ~callee ~typ ~actuals ~areturn ~return
+              Term.call ~callee ~typ ~actuals ~areturn ~return ~throw:None
-                ~throw:None ~loc
+                ~loc
             in
             continue (fun (insts, term) ->
                 let cmnd = IArray.of_list insts in
-                ([], call, [Llair.Block.mk ~lbl ~cmnd ~term]) ) ) )
+                ([], call, [Block.mk ~lbl ~cmnd ~term]) ) ) )
   | Invoke -> (
       let llfunc = Llvm.operand instr (Llvm.num_operands instr - 3) in
       let lltyp = Llvm.type_of llfunc in
@@ -1063,12 +1061,11 @@ let xlate_instr :
       match String.split fname ~on:'.' with
       | _ when Option.is_some (xlate_intrinsic_exp fname) ->
           let dst, blocks = xlate_jump x instr return_blk loc [] in
-          emit_term (Llair.Term.goto ~dst ~loc) ~blocks
+          emit_term (Term.goto ~dst ~loc) ~blocks
       | ["__llair_throw"] ->
           let dst, blocks = xlate_jump x instr unwind_blk loc [] in
-          emit_term (Llair.Term.goto ~dst ~loc) ~blocks
+          emit_term (Term.goto ~dst ~loc) ~blocks
-      | ["abort"] ->
+      | ["abort"] -> emit_term ~prefix:[Inst.abort ~loc] Term.unreachable
-          emit_term ~prefix:[Llair.Inst.abort ~loc] Llair.Term.unreachable
       | ["_Znwm" (* operator new(size_t num) *)]
        |[ "_ZnwmSt11align_val_t"
           (* operator new(unsigned long num, std::align_val_t) *) ]
@@ -1078,9 +1075,8 @@ let xlate_instr :
           let len = xlate_size_of x instr in
           let dst, blocks = xlate_jump x instr return_blk loc [] in
           emit_term
-            ~prefix:[Llair.Inst.alloc ~reg ~num ~len ~loc]
+            ~prefix:[Inst.alloc ~reg ~num ~len ~loc]
-            (Llair.Term.goto ~dst ~loc)
+            (Term.goto ~dst ~loc) ~blocks
-            ~blocks
       (* unimplemented *)
       | "llvm" :: "experimental" :: "gc" :: "statepoint" :: _ ->
           todo "statepoints:@ %a" pp_llvalue instr ()
@@ -1097,26 +1093,24 @@ let xlate_instr :
           let throw, blocks = xlate_jump x instr unwind_blk loc blocks in
           let throw = Some throw in
           emit_term
-            (Llair.Term.call ~callee ~typ ~actuals ~areturn ~return ~throw
+            (Term.call ~callee ~typ ~actuals ~areturn ~return ~throw ~loc)
-               ~loc)
             ~blocks )
   | Ret ->
       let exp =
         if Llvm.num_operands instr = 0 then None
         else Some (xlate_value x (Llvm.operand instr 0))
       in
-      emit_term ~prefix:(pop loc) (Llair.Term.return ~exp ~loc)
+      emit_term ~prefix:(pop loc) (Term.return ~exp ~loc)
   | Br -> (
     match Option.value_exn (Llvm.get_branch instr) with
     | `Unconditional blk ->
         let dst, blocks = xlate_jump x instr blk loc [] in
-        emit_term (Llair.Term.goto ~dst ~loc) ~blocks
+        emit_term (Term.goto ~dst ~loc) ~blocks
     | `Conditional (cnd, thn, els) ->
         let key = xlate_value x cnd in
         let thn, blocks = xlate_jump x instr thn loc [] in
         let els, blocks = xlate_jump x instr els loc blocks in
-        emit_term (Llair.Term.branch ~key ~nzero:thn ~zero:els ~loc) ~blocks
+        emit_term (Term.branch ~key ~nzero:thn ~zero:els ~loc) ~blocks )
-    )
   | Switch ->
       let key = xlate_value x (Llvm.operand instr 0) in
       let cases, blocks =
@@ -1138,7 +1132,7 @@ let xlate_instr :
       let tbl = IArray.of_list cases in
       let blk = Llvm.block_of_value (Llvm.operand instr 1) in
       let els, blocks = xlate_jump x instr blk loc blocks in
-      emit_term (Llair.Term.switch ~key ~tbl ~els ~loc) ~blocks
+      emit_term (Term.switch ~key ~tbl ~els ~loc) ~blocks
   | IndirectBr ->
       let ptr = xlate_value x (Llvm.operand instr 0) in
       let num_dests = Llvm.num_operands instr - 1 in
@@ -1155,7 +1149,7 @@ let xlate_instr :
         dests 1 []
       in
       let tbl = IArray.of_list lldests in
-      emit_term (Llair.Term.iswitch ~ptr ~tbl ~loc) ~blocks
+      emit_term (Term.iswitch ~ptr ~tbl ~loc) ~blocks
   | LandingPad ->
       (* Translate the landingpad clauses to code to load the type_info from
          the thrown exception, and test the type_info against the clauses,
@@ -1179,7 +1173,7 @@ let xlate_instr :
             ~fld ~lltyp:typ
         in
         let len = Exp.integer Typ.siz (Z.of_int (size_of x typ)) in
-        Llair.Inst.load ~reg:ti ~ptr ~len ~loc
+        Inst.load ~reg:ti ~ptr ~len ~loc
       in
       let ti = Exp.reg ti in
       let typeid = xlate_llvm_eh_typeid_for x tip ti in
@@ -1188,19 +1182,19 @@ let xlate_instr :
       let jump_unwind i sel rev_blocks =
         let exp = Exp.record exc_typ (IArray.of_array [|exc; sel|]) in
         let mov =
-          Llair.Inst.move ~reg_exps:(IArray.of_array [|(reg, exp)|]) ~loc
+          Inst.move ~reg_exps:(IArray.of_array [|(reg, exp)|]) ~loc
         in
         let lbl_i = lbl ^ "." ^ Int.to_string i in
         let blk =
-          Llair.Block.mk ~lbl:lbl_i
+          Block.mk ~lbl:lbl_i
             ~cmnd:(IArray.of_array [|mov|])
-            ~term:(Llair.Term.goto ~dst:(Llair.Jump.mk lbl) ~loc)
+            ~term:(Term.goto ~dst:(Jump.mk lbl) ~loc)
         in
-        (Llair.Jump.mk lbl_i, blk :: rev_blocks)
+        (Jump.mk lbl_i, blk :: rev_blocks)
       in
       let goto_unwind i sel blocks =
         let dst, blocks = jump_unwind i sel blocks in
-        (Llair.Term.goto ~dst ~loc, blocks)
+        (Term.goto ~dst ~loc, blocks)
       in
       let term_unwind, rev_blocks =
         if Llvm.is_cleanup instr then
@@ -1208,9 +1202,9 @@ let xlate_instr :
         else
           let num_clauses = Llvm.num_operands instr in
           let lbl i = name ^ "." ^ Int.to_string i in
-          let jump i = Llair.Jump.mk (lbl i) in
+          let jump i = Jump.mk (lbl i) in
           let block i term =
-            Llair.Block.mk ~lbl:(lbl i) ~cmnd:IArray.empty ~term
+            Block.mk ~lbl:(lbl i) ~cmnd:IArray.empty ~term
           in
           let match_filter i rev_blocks =
             jump_unwind i
@@ -1222,7 +1216,7 @@ let xlate_instr :
             let num_tis = Llvm.num_operands clause in
             if num_tis = 0 then
               let dst, rev_blocks = match_filter i rev_blocks in
-              (Llair.Term.goto ~dst ~loc, rev_blocks)
+              (Term.goto ~dst ~loc, rev_blocks)
             else
               match Llvm.classify_type (Llvm.type_of clause) with
               | Array (* filter *) -> (
@@ -1237,7 +1231,7 @@ let xlate_instr :
                     in
                     let key = xlate_filter 0 in
                     let nzero, rev_blocks = match_filter i rev_blocks in
-                    ( Llair.Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1))
+                    ( Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1))
                     , rev_blocks )
                 | _ -> fail "xlate_instr: %a" pp_llvalue instr () )
               | _ (* catch *) ->
@@ -1249,14 +1243,14 @@ let xlate_instr :
                       (Exp.eq ~typ clause ti)
                   in
                   let nzero, rev_blocks = jump_unwind i typeid rev_blocks in
-                  ( Llair.Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1))
+                  ( Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1))
                   , rev_blocks )
           in
           let rec rev_blocks i z =
             if i < num_clauses then
               let term, z = xlate_clause i z in
               rev_blocks (i + 1) (block i term :: z)
-            else block i Llair.Term.unreachable :: z
+            else block i Term.unreachable :: z
           in
           xlate_clause 0 (rev_blocks 1 [])
       in
@@ -1264,14 +1258,14 @@ let xlate_instr :
           ( [load_ti]
           , term_unwind
           , List.rev_append rev_blocks
-              [Llair.Block.mk ~lbl ~cmnd:(IArray.of_list insts) ~term] ) )
+              [Block.mk ~lbl ~cmnd:(IArray.of_list insts) ~term] ) )
   | Resume ->
       let llrcd = Llvm.operand instr 0 in
       let typ = xlate_type x (Llvm.type_of llrcd) in
       let rcd = xlate_value x llrcd in
       let exc = Exp.select typ rcd 0 in
-      emit_term ~prefix:(pop loc) (Llair.Term.throw ~exc ~loc)
+      emit_term ~prefix:(pop loc) (Term.throw ~exc ~loc)
-  | Unreachable -> emit_term Llair.Term.unreachable
+  | Unreachable -> emit_term Term.unreachable
   | Trunc | ZExt | SExt | FPToUI | FPToSI | UIToFP | SIToFP | FPTrunc
    |FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast | Add | FAdd
    |Sub | FSub | Mul | FMul | UDiv | SDiv | FDiv | URem | SRem | FRem
@@ -1282,7 +1276,7 @@ let xlate_instr :
   | VAArg ->
       let reg = xlate_name_opt x instr in
       warn "variadic function argument: %a" Loc.pp loc () ;
-      emit_inst (Llair.Inst.nondet ~reg ~msg:"vaarg" ~loc)
+      emit_inst (Inst.nondet ~reg ~msg:"vaarg" ~loc)
   | CleanupRet | CatchRet | CatchPad | CleanupPad | CatchSwitch ->
       todo "windows exception handling: %a" pp_llvalue instr ()
   | Fence | AtomicCmpXchg | AtomicRMW ->
@@ -1318,9 +1312,9 @@ let xlate_block : pop_thunk -> x -> Llvm.llbasicblock -> Llair.block list =
   let lbl = label_of_block blk in
   let pos = skip_phis blk in
   let insts, term, blocks = xlate_instrs pop x pos in
-  Llair.Block.mk ~lbl ~cmnd:(IArray.of_list insts) ~term :: blocks
+  Block.mk ~lbl ~cmnd:(IArray.of_list insts) ~term :: blocks
   |>
-  [%Trace.retn fun {pf} blocks -> pf "%s" (List.hd_exn blocks).Llair.lbl]
+  [%Trace.retn fun {pf} blocks -> pf "%s" (List.hd_exn blocks).lbl]
 
 let report_undefined func name =
   if Option.is_some (Llvm.use_begin func) then
@@ -1352,7 +1346,7 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
       in
       let entry =
         let {Llair.lbl; cmnd; term} = entry_block in
-        Llair.Block.mk ~lbl ~cmnd ~term
+        Block.mk ~lbl ~cmnd ~term
       in
       let cfg =
         let rec trav_blocks rev_cfg prev =
@@ -1365,12 +1359,12 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
         in
         trav_blocks (List.rev entry_blocks) entry_blk
       in
-      Llair.Func.mk ~name ~formals ~freturn ~fthrow ~entry ~cfg
+      Func.mk ~name ~formals ~freturn ~fthrow ~entry ~cfg
   | At_end _ ->
       report_undefined llf name ;
-      Llair.Func.mk_undefined ~name ~formals ~freturn ~fthrow )
+      Func.mk_undefined ~name ~formals ~freturn ~fthrow )
   |>
-  [%Trace.retn fun {pf} -> pf "@\n%a" Llair.Func.pp]
+  [%Trace.retn fun {pf} -> pf "@\n%a" Func.pp]
 
 let transform ~internalize : Llvm.llmodule -> unit =
  fun llmodule ->

sledge/bin/sledge_cli.ml

@@ -77,14 +77,15 @@ let used_globals pgm preanalyze : Domain_used_globals.r =
         ; skip_throw= false
         ; function_summaries= true
         ; entry_points= Config.find_list "entry-points"
-        ; globals= Declared Reg.Set.empty }
+        ; globals= Declared Llair.Reg.Set.empty }
         pgm
     in
-    Per_function (Reg.Map.map summary_table ~f:Reg.Set.union_list)
+    Per_function
+      (Llair.Reg.Map.map summary_table ~f:Llair.Reg.Set.union_list)
   else
     Declared
-      (IArray.fold pgm.globals ~init:Reg.Set.empty ~f:(fun acc g ->
+      (IArray.fold pgm.globals ~init:Llair.Reg.Set.empty ~f:(fun acc g ->
-           Reg.Set.add acc g.reg ))
+           Llair.Reg.Set.add acc g.reg ))
 
 let analyze =
   let%map_open bound =

sledge/dune

@@ -38,7 +38,6 @@
  (library
   (name llair)
   (public_name sledge.llair)
-  (wrapped false)
   (libraries nonstdlib)
   (flags
    (:standard -open NS))

sledge/src/control.ml

@@ -31,15 +31,20 @@ module Make (Dom : Domain_intf.Dom) = struct
     val pop_throw :
          t
       -> init:'a
-      -> unwind:(Reg.t list -> Reg.Set.t -> Dom.from_call -> 'a -> 'a)
+      -> unwind:
+           (   Llair.Reg.t list
+            -> Llair.Reg.Set.t
+            -> Dom.from_call
+            -> 'a
+            -> 'a)
       -> (Dom.from_call * Llair.jump * t * 'a) option
   end = struct
     type t =
       | Return of
           { recursive: bool  (** return from a possibly-recursive call *)
           ; dst: Llair.Jump.t
-          ; formals: Reg.t list
+          ; formals: Llair.Reg.t list
-          ; locals: Reg.Set.t
+          ; locals: Llair.Reg.Set.t
           ; from_call: Dom.from_call
           ; stk: t }
       | Throw of Llair.Jump.t * t
@@ -253,13 +258,13 @@ module Make (Dom : Domain_intf.Dom) = struct
   let exec_jump stk state block Llair.{dst; retreating} =
     Work.add ~prev:block ~retreating stk state dst
 
-  let summary_table = Hashtbl.create (module Reg)
+  let summary_table = Hashtbl.create (module Llair.Reg)
 
   let exec_call opts stk state block call globals =
     let Llair.{callee; actuals; areturn; return; recursive} = call in
     let Llair.{name; formals; freturn; locals; entry} = callee in
     [%Trace.call fun {pf} ->
-      pf "%a from %a with state@ %a" Reg.pp name.reg Reg.pp
+      pf "%a from %a with state@ %a" Llair.Reg.pp name.reg Llair.Reg.pp
         return.dst.parent.name.reg Dom.pp state]
     ;
     let dnf_states =
@@ -304,13 +309,13 @@ module Make (Dom : Domain_intf.Dom) = struct
     [%Trace.printf
       "@[<v>%t@]" (fun fs ->
           Hashtbl.iteri summary_table ~f:(fun ~key ~data ->
-              Format.fprintf fs "@[<v>%a:@ @[%a@]@]@ " Reg.pp key
+              Format.fprintf fs "@[<v>%a:@ @[%a@]@]@ " Llair.Reg.pp key
                 (List.pp "@," Dom.pp_summary)
                 data ) )]
 
   let exec_return ~opts stk pre_state (block : Llair.block) exp =
     let Llair.{name; formals; freturn; locals} = block.parent in
-    [%Trace.call fun {pf} -> pf "from: %a" Reg.pp name.reg]
+    [%Trace.call fun {pf} -> pf "from: %a" Llair.Reg.pp name.reg]
     ;
     let summarize post_state =
       if not opts.function_summaries then post_state
@@ -320,7 +325,8 @@ module Make (Dom : Domain_intf.Dom) = struct
         in
         let function_summary, post_state =
           Dom.create_summary ~locals post_state
-            ~formals:(Reg.Set.union (Reg.Set.of_list formals) globals)
+            ~formals:
+              (Llair.Reg.Set.union (Llair.Reg.Set.of_list formals) globals)
         in
         Hashtbl.add_multi summary_table ~key:name.reg ~data:function_summary ;
         pp_st () ;
@@ -343,7 +349,7 @@ module Make (Dom : Domain_intf.Dom) = struct
         if
           opts.function_summaries
           && List.exists opts.entry_points
-               ~f:(String.equal (Reg.name name.reg))
+               ~f:(String.equal (Llair.Reg.name name.reg))
         then summarize exit_state |> (ignore : Dom.t -> unit) ;
         Work.skip )
     |>
@@ -351,7 +357,7 @@ module Make (Dom : Domain_intf.Dom) = struct
 
   let exec_throw stk pre_state (block : Llair.block) exc =
     let func = block.parent in
-    [%Trace.call fun {pf} -> pf "from %a" Reg.pp func.name.reg]
+    [%Trace.call fun {pf} -> pf "from %a" Llair.Reg.pp func.name.reg]
     ;
     let unwind formals scope from_call state =
       Dom.retn formals (Some func.fthrow) from_call
@@ -376,7 +382,7 @@ module Make (Dom : Domain_intf.Dom) = struct
          Stack.t
       -> Dom.t
       -> Llair.block
-      -> Reg.t option
+      -> Llair.Reg.t option
       -> Llair.jump
       -> Work.x =
    fun stk state block areturn return ->
@@ -398,14 +404,15 @@ module Make (Dom : Domain_intf.Dom) = struct
     | Switch {key; tbl; els} ->
         IArray.fold tbl
           ~f:(fun x (case, jump) ->
-            match Dom.exec_assume state (Exp.eq key case) with
+            match Dom.exec_assume state (Llair.Exp.eq key case) with
             | Some state -> exec_jump stk state block jump |> Work.seq x
             | None -> x )
           ~init:
             ( match
                 Dom.exec_assume state
-                  (IArray.fold tbl ~init:Exp.true_ ~f:(fun b (case, _) ->
+                  (IArray.fold tbl ~init:Llair.Exp.true_
-                       Exp.and_ (Exp.dq key case) b ))
+                     ~f:(fun b (case, _) ->
+                       Llair.Exp.and_ (Llair.Exp.dq key case) b ))
               with
             | Some state -> exec_jump stk state block els
             | None -> Work.skip )
@@ -413,9 +420,9 @@ module Make (Dom : Domain_intf.Dom) = struct
         IArray.fold tbl ~init:Work.skip ~f:(fun x (jump : Llair.jump) ->
             match
               Dom.exec_assume state
-                (Exp.eq ptr
+                (Llair.Exp.eq ptr
-                   (Exp.label
+                   (Llair.Exp.label
-                      ~parent:(Reg.name jump.dst.parent.name.reg)
+                      ~parent:(Llair.Reg.name jump.dst.parent.name.reg)
                       ~name:jump.dst.lbl))
             with
             | Some state -> exec_jump stk state block jump |> Work.seq x
@@ -497,9 +504,10 @@ module Make (Dom : Domain_intf.Dom) = struct
     | Some work -> Work.run ~f:(exec_block opts pgm) (work opts.bound)
     | None -> fail "no applicable harness" ()
 
-  let compute_summaries opts pgm : Dom.summary list Reg.Map.t =
+  let compute_summaries opts pgm : Dom.summary list Llair.Reg.Map.t =
     assert opts.function_summaries ;
     exec_pgm opts pgm ;
-    Hashtbl.fold summary_table ~init:Reg.Map.empty ~f:(fun ~key ~data map ->
+    Hashtbl.fold summary_table ~init:Llair.Reg.Map.empty
-        match data with [] -> map | _ -> Reg.Map.set map ~key ~data )
+      ~f:(fun ~key ~data map ->
+        match data with [] -> map | _ -> Llair.Reg.Map.set map ~key ~data )
 end

sledge/src/control.mli

@@ -18,5 +18,5 @@ module Make (Dom : Domain_intf.Dom) : sig
   val exec_pgm : exec_opts -> Llair.program -> unit
 
   val compute_summaries :
-    exec_opts -> Llair.program -> Dom.summary list Reg.Map.t
+    exec_opts -> Llair.program -> Dom.summary list Llair.Reg.Map.t
 end

sledge/src/domain_intf.ml

@@ -11,41 +11,41 @@ module type Dom = sig
 
   val pp : t pp
   val report_fmt_thunk : t -> Formatter.t -> unit
-  val init : Global.t iarray -> t
+  val init : Llair.Global.t iarray -> t
   val join : t -> t -> t option
   val is_false : t -> bool
   val dnf : t -> t list
-  val exec_assume : t -> Exp.t -> t option
+  val exec_assume : t -> Llair.Exp.t -> t option
-  val exec_kill : t -> Reg.t -> t
+  val exec_kill : t -> Llair.Reg.t -> t
-  val exec_move : t -> (Reg.t * Exp.t) iarray -> t
+  val exec_move : t -> (Llair.Reg.t * Llair.Exp.t) iarray -> t
   val exec_inst : t -> Llair.inst -> t option
 
   val exec_intrinsic :
        skip_throw:bool
     -> t
-    -> Reg.t option
+    -> Llair.Reg.t option
-    -> Reg.t
+    -> Llair.Reg.t
-    -> Exp.t list
+    -> Llair.Exp.t list
     -> t option option
 
   type from_call [@@deriving sexp_of]
 
   val call :
        summaries:bool
-    -> globals:Reg.Set.t
+    -> globals:Llair.Reg.Set.t
-    -> actuals:Exp.t list
+    -> actuals:Llair.Exp.t list
-    -> areturn:Reg.t option
+    -> areturn:Llair.Reg.t option
-    -> formals:Reg.t list
+    -> formals:Llair.Reg.t list
-    -> freturn:Reg.t option
+    -> freturn:Llair.Reg.t option
-    -> locals:Reg.Set.t
+    -> locals:Llair.Reg.Set.t
     -> t
     -> t * from_call
 
-  val post : Reg.Set.t -> from_call -> t -> t
+  val post : Llair.Reg.Set.t -> from_call -> t -> t
-  val retn : Reg.t list -> Reg.t option -> from_call -> t -> t
+  val retn : Llair.Reg.t list -> Llair.Reg.t option -> from_call -> t -> t
 
   val resolve_callee :
-    (string -> Llair.func list) -> Exp.t -> t -> Llair.func list * t
+    (string -> Llair.func list) -> Llair.Exp.t -> t -> Llair.func list * t
 
   val recursion_beyond_bound : [`skip | `prune]
 
@@ -54,7 +54,7 @@ module type Dom = sig
   val pp_summary : summary pp
 
   val create_summary :
-    locals:Reg.Set.t -> formals:Reg.Set.t -> t -> summary * t
+    locals:Llair.Reg.Set.t -> formals:Llair.Reg.Set.t -> t -> summary * t
 
   val apply_summary : t -> summary -> t option
 end

sledge/src/domain_relation.ml

@@ -12,8 +12,8 @@ module type State_domain_sig = sig
   include Domain_intf.Dom
 
   val create_summary :
-       locals:Reg.Set.t
+       locals:Llair.Reg.Set.t
-    -> formals:Reg.Set.t
+    -> formals:Llair.Reg.Set.t
     -> entry:t
     -> current:t
     -> summary * t
@@ -76,8 +76,10 @@ module Make (State_domain : State_domain_sig) = struct
       pf
         "@[<v>@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \
          globals: {@[%a@]}@ current: %a@]"
-        (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Reg.pp)
+        (List.pp ",@ " Llair.Exp.pp)
-        (List.rev formals) Reg.Set.pp locals Reg.Set.pp globals
+        (List.rev actuals)
+        (List.pp ",@ " Llair.Reg.pp)
+        (List.rev formals) Llair.Reg.Set.pp locals Llair.Reg.Set.pp globals
         State_domain.pp current]
     ;
     let caller_current, state_from_call =
@@ -90,7 +92,7 @@ module Make (State_domain : State_domain_sig) = struct
     [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln]
 
   let post locals {state_from_call; caller_entry} (_, current) =
-    [%Trace.call fun {pf} -> pf "locals: %a" Reg.Set.pp locals]
+    [%Trace.call fun {pf} -> pf "locals: %a" Llair.Reg.Set.pp locals]
     ;
     (caller_entry, State_domain.post locals state_from_call current)
     |>

sledge/src/domain_relation.mli

@@ -12,8 +12,8 @@ module type State_domain_sig = sig
   include Domain_intf.Dom
 
   val create_summary :
-       locals:Reg.Set.t
+       locals:Llair.Reg.Set.t
-    -> formals:Reg.Set.t
+    -> formals:Llair.Reg.Set.t
     -> entry:t
     -> current:t
     -> summary * t

sledge/src/domain_sh.ml

@@ -18,7 +18,7 @@ let simplify q = if !simplify_states then Sh.simplify q else q
 
 let init globals =
   IArray.fold globals ~init:Sh.emp ~f:(fun q -> function
-    | {Global.reg; init= Some (arr, siz)} ->
+    | {Llair.Global.reg; init= Some (arr, siz)} ->
         let loc = Term.var (Var.of_reg reg) in
         let len = Term.integer (Z.of_int siz) in
         let arr = Term.of_exp arr in
@@ -129,7 +129,7 @@ let localize_entry globals actuals formals freturn locals subst pre entry =
   (* Add the formals here to do garbage collection and then get rid of them *)
   let formals_set = Var.Set.of_list formals in
   let freturn_locals =
-    Var.Set.of_regs (Reg.Set.add_option freturn locals)
+    Var.Set.of_regs (Llair.Reg.Set.add_option freturn locals)
   in
   let function_summary_pre =
     garbage_collect entry
@@ -159,14 +159,17 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
     pf
       "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ \
        globals: {@[%a@]}@ q: %a@]"
-      (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Reg.pp)
+      (List.pp ",@ " Llair.Exp.pp)
-      (List.rev formals) Reg.Set.pp locals Reg.Set.pp globals pp q]
+      (List.rev actuals)
+      (List.pp ",@ " Llair.Reg.pp)
+      (List.rev formals) Llair.Reg.Set.pp locals Llair.Reg.Set.pp globals pp
+      q]
   ;
   let actuals = List.map ~f:Term.of_exp actuals in
   let areturn = Option.map ~f:Var.of_reg areturn in
   let formals = List.map ~f:Var.of_reg formals in
   let freturn_locals =
-    Var.Set.of_regs (Reg.Set.add_option freturn locals)
+    Var.Set.of_regs (Llair.Reg.Set.add_option freturn locals)
   in
   let modifs = Var.Set.of_option areturn in
   (* quantify modifs, their current value will be overwritten and so does
@@ -200,7 +203,7 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
 (** Leave scope of locals: existentially quantify locals. *)
 let post locals _ q =
   [%Trace.call fun {pf} ->
-    pf "@[<hv>locals: {@[%a@]}@ q: %a@]" Reg.Set.pp locals Sh.pp q]
+    pf "@[<hv>locals: {@[%a@]}@ q: %a@]" Llair.Reg.Set.pp locals Sh.pp q]
   ;
   Sh.exists (Var.Set.of_regs locals) q |> simplify
   |>
@@ -212,8 +215,9 @@ let post locals _ q =
 let retn formals freturn {areturn; subst; frame} q =
   [%Trace.call fun {pf} ->
     pf "@[<v>formals: {@[%a@]}%a%a@ subst: %a@ q: %a@ frame: %a@]"
-      (List.pp ", " Reg.pp) formals
+      (List.pp ", " Llair.Reg.pp)
-      (Option.pp "@ freturn: %a" Reg.pp)
+      formals
+      (Option.pp "@ freturn: %a" Llair.Reg.pp)
       freturn
       (Option.pp "@ areturn: %a" Var.pp)
       areturn Var.Subst.pp (Var.Subst.invert subst) pp q pp frame]
@@ -247,8 +251,8 @@ let retn formals freturn {areturn; subst; frame} q =
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
 let resolve_callee lookup ptr q =
-  match Reg.of_exp ptr with
+  match Llair.Reg.of_exp ptr with
-  | Some callee -> (lookup (Reg.name callee), q)
+  | Some callee -> (lookup (Llair.Reg.name callee), q)
   | None -> ([], q)
 
 let recursion_beyond_bound = `prune
@@ -261,8 +265,8 @@ let pp_summary fs {xs; foot; post} =
 
 let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
   [%Trace.call fun {pf} ->
-    pf "formals %a@ entry: %a@ current: %a" Reg.Set.pp formals pp entry pp
+    pf "formals %a@ entry: %a@ current: %a" Llair.Reg.Set.pp formals pp
-      post]
+      entry pp post]
   ;
   let locals = Var.Set.of_regs locals in
   let formals = Var.Set.of_regs formals in

sledge/src/domain_sh.mli

@@ -12,8 +12,8 @@ include Domain_intf.Dom
 (* formals should include all the parameters of the summary. That is both
    formals and globals. *)
 val create_summary :
-     locals:Reg.Set.t
+     locals:Llair.Reg.Set.t
-  -> formals:Reg.Set.t
+  -> formals:Llair.Reg.Set.t
   -> entry:t
   -> current:t
   -> summary * t

sledge/src/domain_unit.ml

@@ -32,8 +32,8 @@ let retn _ _ _ _ = ()
 let dnf () = [()]
 
 let resolve_callee lookup ptr _ =
-  match Reg.of_exp ptr with
+  match Llair.Reg.of_exp ptr with
-  | Some callee -> (lookup (Reg.name callee), ())
+  | Some callee -> (lookup (Llair.Reg.name callee), ())
   | None -> ([], ())
 
 type summary = unit

sledge/src/domain_used_globals.ml

@@ -7,26 +7,28 @@
 
 (** Used-globals abstract domain *)
 
-type t = Reg.Set.t [@@deriving equal, sexp]
+type t = Llair.Reg.Set.t [@@deriving equal, sexp]
 
-let pp = Reg.Set.pp
+let pp = Llair.Reg.Set.pp
 let report_fmt_thunk = Fn.flip pp
-let empty = Reg.Set.empty
+let empty = Llair.Reg.Set.empty
 
 let init globals =
-  [%Trace.info "pgm globals: {%a}" (IArray.pp ", " Global.pp) globals] ;
+  [%Trace.info "pgm globals: {%a}" (IArray.pp ", " Llair.Global.pp) globals] ;
   empty
 
-let join l r = Some (Reg.Set.union l r)
+let join l r = Some (Llair.Reg.Set.union l r)
 let recursion_beyond_bound = `skip
 let is_false _ = false
 let post _ _ state = state
-let retn _ _ from_call post = Reg.Set.union from_call post
+let retn _ _ from_call post = Llair.Reg.Set.union from_call post
 let dnf t = [t]
-let add_if_global gs v = if Reg.is_global v then Reg.Set.add gs v else gs
+
+let add_if_global gs v =
+  if Llair.Reg.is_global v then Llair.Reg.Set.add gs v else gs
 
 let used_globals ?(init = empty) exp =
-  Exp.fold_regs exp ~init ~f:add_if_global
+  Llair.Exp.fold_regs exp ~init ~f:add_if_global
 
 let exec_assume st exp = Some (used_globals ~init:st exp)
 let exec_kill st _ = st
@@ -46,7 +48,7 @@ let exec_inst st inst =
     Option.iter ~f:(fun uses -> pf "post:{%a}" pp uses)]
 
 let exec_intrinsic ~skip_throw:_ st _ intrinsic actuals =
-  let name = Reg.name intrinsic in
+  let name = Llair.Reg.name intrinsic in
   if
     List.exists
       [ "malloc"
@@ -84,8 +86,8 @@ let call ~summaries:_ ~globals:_ ~actuals ~areturn:_ ~formals:_ ~freturn:_
 
 let resolve_callee lookup ptr st =
   let st = used_globals ~init:st ptr in
-  match Reg.of_exp ptr with
+  match Llair.Reg.of_exp ptr with
-  | Some callee -> (lookup (Reg.name callee), st)
+  | Some callee -> (lookup (Llair.Reg.name callee), st)
   | None -> ([], st)
 
 (* A function summary is the set of global registers accessed by that
@@ -94,25 +96,27 @@ type summary = t
 
 let pp_summary = pp
 let create_summary ~locals:_ ~formals:_ state = (state, state)
-let apply_summary st summ = Some (Reg.Set.union st summ)
+let apply_summary st summ = Some (Llair.Reg.Set.union st summ)
 
 (** Query *)
 
-type r = Per_function of Reg.Set.t Reg.Map.t | Declared of Reg.Set.t
+type r =
+  | Per_function of Llair.Reg.Set.t Llair.Reg.Map.t
+  | Declared of Llair.Reg.Set.t
 
-let by_function : r -> Reg.t -> t =
+let by_function : r -> Llair.Reg.t -> t =
  fun s fn ->
-  [%Trace.call fun {pf} -> pf "%a" Reg.pp fn]
+  [%Trace.call fun {pf} -> pf "%a" Llair.Reg.pp fn]
   ;
   ( match s with
   | Declared set -> set
   | Per_function map -> (
-    match Reg.Map.find map fn with
+    match Llair.Reg.Map.find map fn with
     | Some gs -> gs
     | None ->
         fail
           "main analysis reached function %a that was not reached by \
            used-globals pre-analysis "
-          Reg.pp fn () ) )
+          Llair.Reg.pp fn () ) )
   |>
-  [%Trace.retn fun {pf} r -> pf "%a" Reg.Set.pp r]
+  [%Trace.retn fun {pf} r -> pf "%a" Llair.Reg.Set.pp r]

sledge/src/domain_used_globals.mli

@@ -7,11 +7,11 @@
 
 (** Used-globals abstract domain *)
 
-include Domain_intf.Dom with type summary = Reg.Set.t
+include Domain_intf.Dom with type summary = Llair.Reg.Set.t
 
 type r =
-  | Per_function of Reg.Set.t Reg.Map.t
+  | Per_function of Llair.Reg.Set.t Llair.Reg.Map.t
       (** per-function used-globals map *)
-  | Declared of Reg.Set.t  (** program-wide set *)
+  | Declared of Llair.Reg.Set.t  (** program-wide set *)
 
-val by_function : r -> Reg.t -> summary
+val by_function : r -> Llair.Reg.t -> summary

sledge/src/exec.ml

@@ -317,7 +317,7 @@ let calloc_spec us reg num len =
   let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in
   {xs; foot; sub; ms; post}
 
-let size_of_ptr = Term.integer (Z.of_int (Typ.size_of Typ.ptr))
+let size_of_ptr = Term.integer (Z.of_int Llair.Typ.(size_of ptr))
 
 (* { p-[_;_)->⟨W,_⟩ }
  *   posix_memalign r p s
@@ -490,7 +490,7 @@ let nallocx_spec us reg siz =
   {xs; foot; sub; ms; post}
 
 let size_of_int_mul =
-  Term.mul (Term.integer (Z.of_int (Typ.size_of Typ.siz)))
+  Term.mul (Term.integer (Z.of_int Llair.Typ.(size_of siz)))
 
 (* { r-[_;_)->⟨m,_⟩ * i-[_;_)->⟨_,m⟩ * w=0 * n=0 }
  *   mallctl r i w n

sledge/src/llair/llair.ml

@@ -9,6 +9,12 @@
 
 [@@@warning "+9"]
 
+module Loc = Loc
+module Typ = Typ
+module Reg = Reg
+module Exp = Exp
+module Global = Global
+
 type inst =
   | Move of {reg_exps: (Reg.t * Exp.t) iarray; loc: Loc.t}
   | Load of {reg: Reg.t; ptr: Exp.t; len: Exp.t; loc: Loc.t}

sledge/src/llair/llair.mli

@@ -8,6 +8,12 @@
 (** LLAIR (Low-Level Analysis Internal Representation) is an IR tailored for
     static analysis using a low-level model of memory. *)
 
+module Loc = Loc
+module Typ = Typ
+module Reg = Reg
+module Exp = Exp
+module Global = Global
+
 (** Instructions for memory manipulation or other non-control effects. *)
 type inst = private
   | Move of {reg_exps: (Reg.t * Exp.t) iarray; loc: Loc.t}

sledge/src/report.ml

@@ -11,14 +11,14 @@ let unknown_call call =
   [%Trace.kprintf
     Stop.on_unknown_call
       "@\n@[<v 2>%a Unknown function call %a@;<1 2>@[%a@]@]@."
-      (fun fs call -> Loc.pp fs (Llair.Term.loc call))
+      (fun fs call -> Llair.Loc.pp fs (Llair.Term.loc call))
       call
       (fun fs (call : Llair.Term.t) ->
         match call with
         | Call {callee} -> (
-          match Reg.of_exp callee with
+          match Llair.Reg.of_exp callee with
-          | Some reg -> Reg.pp_demangled fs reg
+          | Some reg -> Llair.Reg.pp_demangled fs reg
-          | None -> Exp.pp fs callee )
+          | None -> Llair.Exp.pp fs callee )
         | _ -> () )
       call Llair.Term.pp call]
 
@@ -28,7 +28,7 @@ let invalid_access_count () = !count
 let invalid_access fmt_thunk pp access loc =
   Int.incr count ;
   let rep fs =
-    Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Loc.pp
+    Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Llair.Loc.pp
       (loc access) pp access
   in
   Format.printf "@\n@[<v 2>%t@]@." rep ;

sledge/src/term.ml

@@ -12,7 +12,7 @@
 type op1 =
   | Signed of {bits: int}
   | Unsigned of {bits: int}
-  | Convert of {src: Typ.t; dst: Typ.t}
+  | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t}
   | Splat
   | Select of int
 [@@deriving compare, equal, hash, sexp]
@@ -155,7 +155,7 @@ let rec ppx strength fs term =
     | Ap1 (Signed {bits}, arg) -> pf "((s%i)@ %a)" bits pp arg
     | Ap1 (Unsigned {bits}, arg) -> pf "((u%i)@ %a)" bits pp arg
     | Ap1 (Convert {src; dst}, arg) ->
-        pf "((%a)(%a)@ %a)" Typ.pp dst Typ.pp src pp arg
+        pf "((%a)(%a)@ %a)" Llair.Typ.pp dst Llair.Typ.pp src pp arg
     | Ap2 (Eq, x, y) -> pf "(%a@ = %a)" pp x pp y
     | Ap2 (Dq, x, y) -> pf "(%a@ @<2>≠ %a)" pp x pp y
     | Ap2 (Lt, x, y) -> pf "(%a@ < %a)" pp x pp y
@@ -310,10 +310,11 @@ let invariant e =
   | ApN (Record, elts) -> assert (not (IArray.is_empty elts))
   | Ap1 (Convert {src= Integer _; dst= Integer _}, _) -> assert false
   | Ap1 (Convert {src; dst}, _) ->
-      assert (Typ.convertible src dst) ;
+      assert (Llair.Typ.convertible src dst) ;
       assert (
-        not (Typ.equivalent src dst) (* avoid redundant representations *)
+        not
-      )
+          (Llair.Typ.equivalent src dst)
+          (* avoid redundant representations *) )
   | Rational {data} ->
       assert (Q.is_real data) ;
       assert (not (Z.equal Z.one (Q.den data)))
@@ -940,7 +941,8 @@ let signed bits term = norm1 (Signed {bits}) term
 let unsigned bits term = norm1 (Unsigned {bits}) term
 
 let convert src ~to_:dst arg =
-  if Typ.equivalent src dst then arg else norm1 (Convert {src; dst}) arg
+  if Llair.Typ.equivalent src dst then arg
+  else norm1 (Convert {src; dst}) arg
 
 let eq = norm2 Eq
 let dq = norm2 Dq
@@ -982,11 +984,11 @@ let eq_concat (siz, arr) ms =
 let rec binary mk x y = mk (of_exp x) (of_exp y)
 
 and ubinary mk typ x y =
-  let unsigned typ = unsigned (Typ.bit_size_of typ) in
+  let unsigned typ = unsigned (Llair.Typ.bit_size_of typ) in
   mk (unsigned typ (of_exp x)) (unsigned typ (of_exp y))
 
 and of_exp e =
-  match (e : Exp.t) with
+  match (e : Llair.Exp.t) with
   | Reg {name; global; typ= _} -> Var {name; id= (if global then -1 else 0)}
   | Nondet {msg; typ= _} -> nondet msg
   | Label {parent; name} -> label ~parent ~name
@@ -1050,9 +1052,9 @@ module Var = struct
     | _ -> None
 
   let of_reg r =
-    match of_term (of_exp (r : Reg.t :> Exp.t)) with
+    match of_term (of_exp (r : Llair.Reg.t :> Llair.Exp.t)) with
     | Some v -> v
-    | _ -> violates Reg.invariant r
+    | _ -> violates Llair.Reg.invariant r
 
   let fresh name ~wrt =
     let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in
@@ -1073,7 +1075,8 @@ module Var = struct
       if not (is_empty xs) then
         Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs
 
-    let of_regs = Reg.Set.fold ~init:empty ~f:(fun s r -> add s (of_reg r))
+    let of_regs =
+      Llair.Reg.Set.fold ~init:empty ~f:(fun s r -> add s (of_reg r))
   end
 
   (** Variable renaming substitutions *)

sledge/src/term.mli

@@ -19,7 +19,7 @@ type op1 =
       (** [Ap1 (Unsigned {bits= n}, arg)] is [arg] interpreted as an [n]-bit
           unsigned integer. That is, it unsigned-binary--decodes the low [n]
           bits of the infinite two's-complement encoding of [arg]. *)
-  | Convert of {src: Typ.t; dst: Typ.t}
+  | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t}
       (** [Ap1 (Convert {src; dst}, arg)] is [arg] converted from type [src]
           to type [dst], possibly with loss of information. The [src] and
           [dst] types must be [Typ.convertible] and must not both be
@@ -118,7 +118,7 @@ module Var : sig
     val ppx : strength -> t pp
     val pp : t pp
     val pp_xs : t pp
-    val of_regs : Reg.Set.t -> t
+    val of_regs : Llair.Reg.Set.t -> t
   end
 
   val pp : t pp
@@ -129,7 +129,7 @@ module Var : sig
   val id : t -> int
   val of_ : term -> t
   val of_term : term -> t option
-  val of_reg : Reg.t -> t
+  val of_reg : Llair.Reg.t -> t
   val fresh : string -> wrt:Set.t -> t * Set.t
 
   val identified : name:string -> id:int -> t
@@ -189,7 +189,7 @@ val float : string -> t
 (* type conversions *)
 val signed : int -> t -> t
 val unsigned : int -> t -> t
-val convert : Typ.t -> to_:Typ.t -> t -> t
+val convert : Llair.Typ.t -> to_:Llair.Typ.t -> t -> t
 
 (* comparisons *)
 val eq : t -> t -> t
@@ -239,7 +239,7 @@ val update : rcd:t -> idx:int -> elt:t -> t
 val rec_record : int -> t
 
 (* convert *)
-val of_exp : Exp.t -> t
+val of_exp : Llair.Exp.t -> t
 
 (** Transform *)
 

sledge/src/term_test.ml

@@ -41,49 +41,51 @@ let%test_module _ =
     let%test "unsigned boolean overflow" =
       is_true
         (Term.of_exp
-           (Exp.uge
+           Llair.(
-              (Exp.integer Typ.bool Z.minus_one)
+             Exp.uge
-              (Exp.signed 1 (Exp.integer Typ.siz Z.one) ~to_:Typ.bool)))
+               (Exp.integer Typ.bool Z.minus_one)
+               (Exp.signed 1 (Exp.integer Typ.siz Z.one) ~to_:Typ.bool)))
 
     let pp_exp e =
-      Format.printf "@\nexp= %a; term= %a@." Exp.pp e Term.pp
+      Format.printf "@\nexp= %a; term= %a@." Llair.Exp.pp e Term.pp
         (Term.of_exp e)
 
-    let ( !! ) i = Exp.integer Typ.siz (Z.of_int i)
+    let ( !! ) i = Llair.(Exp.integer Typ.siz (Z.of_int i))
 
     let%expect_test _ =
-      pp_exp (Exp.signed 1 !!1 ~to_:Typ.bool) ;
+      pp_exp Llair.(Exp.signed 1 !!1 ~to_:Typ.bool) ;
       [%expect {| exp= ((i1)(s1) 1); term= -1 |}]
 
     let%expect_test _ =
-      pp_exp (Exp.unsigned 1 !!(-1) ~to_:Typ.byt) ;
+      pp_exp Llair.(Exp.unsigned 1 !!(-1) ~to_:Typ.byt) ;
       [%expect {| exp= ((i8)(u1) -1); term= 1 |}]
 
     let%expect_test _ =
-      pp_exp (Exp.signed 8 !!(-1) ~to_:Typ.int) ;
+      pp_exp Llair.(Exp.signed 8 !!(-1) ~to_:Typ.int) ;
       [%expect {| exp= ((i32)(s8) -1); term= -1 |}]
 
     let%expect_test _ =
-      pp_exp (Exp.unsigned 8 !!(-1) ~to_:Typ.int) ;
+      pp_exp Llair.(Exp.unsigned 8 !!(-1) ~to_:Typ.int) ;
       [%expect {| exp= ((i32)(u8) -1); term= 255 |}]
 
     let%expect_test _ =
-      pp_exp (Exp.signed 8 !!255 ~to_:Typ.byt) ;
+      pp_exp Llair.(Exp.signed 8 !!255 ~to_:Typ.byt) ;
       [%expect {| exp= ((i8)(s8) 255); term= -1 |}]
 
     let%expect_test _ =
-      pp_exp (Exp.signed 7 !!255 ~to_:Typ.byt) ;
+      pp_exp Llair.(Exp.signed 7 !!255 ~to_:Typ.byt) ;
       [%expect {| exp= ((i8)(s7) 255); term= -1 |}]
 
     let%expect_test _ =
-      pp_exp (Exp.unsigned 7 !!255 ~to_:Typ.byt) ;
+      pp_exp Llair.(Exp.unsigned 7 !!255 ~to_:Typ.byt) ;
       [%expect {| exp= ((i8)(u7) 255); term= 127 |}]
 
     let%expect_test _ =
       pp_exp
-        (Exp.uge
+        Llair.(
-           (Exp.integer Typ.bool Z.minus_one)
+          Exp.uge
-           (Exp.signed 1 !!1 ~to_:Typ.bool)) ;
+            (Exp.integer Typ.bool Z.minus_one)
+            (Exp.signed 1 !!1 ~to_:Typ.bool)) ;
       [%expect {| exp= (-1 u≥ ((i1)(s1) 1)); term= -1 |}]
 
     let%expect_test _ =