[sledge] Refactor: Move Llair.t to separate Program module

Reviewed By: jvillard

Differential Revision: D21720975

fbshipit-source-id: fb743b35f

sledge/bin/frontend.ml

@@ -1453,7 +1453,7 @@ let cleanup llmodule llcontext =
   Llvm.dispose_module llmodule ;
   Llvm.dispose_context llcontext
 
-let translate ~models ~fuzzer ~internalize : string list -> Llair.t =
+let translate ~models ~fuzzer ~internalize : string list -> Llair.program =
  fun inputs ->
   [%Trace.call fun {pf} ->
     pf "%a" (List.pp "@ " Format.pp_print_string) inputs]
@@ -1504,7 +1504,7 @@ let translate ~models ~fuzzer ~internalize : string list -> Llair.t =
       [] llmodule
   in
   cleanup llmodule llcontext ;
-  Llair.mk ~globals ~functions
+  Llair.Program.mk ~globals ~functions
   |>
   [%Trace.retn fun {pf} _ ->
     pf "number of globals %d, number of functions %d" (List.length globals)

sledge/bin/frontend.mli

@@ -10,6 +10,10 @@
 exception Invalid_llvm of string
 
 val translate :
-  models:bool -> fuzzer:bool -> internalize:bool -> string list -> Llair.t
+     models:bool
+  -> fuzzer:bool
+  -> internalize:bool
+  -> string list
+  -> Llair.program
 (** Translate the compilation units in the named (llvm or bitcode) files to
     LLAIR. Attempts to raise [Invalid_llvm] when the input is invalid LLVM. *)

sledge/bin/sledge_cli.ml

@@ -66,7 +66,7 @@ let marshal program file =
 
 let unmarshal file () =
   In_channel.with_file
-    ~f:(fun ic -> (Marshal.from_channel ic : Llair.t))
+    ~f:(fun ic -> (Marshal.from_channel ic : Llair.program))
     file
 
 let used_globals pgm preanalyze : Domain_used_globals.r =
@@ -221,11 +221,11 @@ let disassemble_cmd =
     fun () ->
       let program = unmarshal input () in
       match llair_txt_output with
-      | None -> Format.printf "%a@." Llair.pp program
+      | None -> Format.printf "%a@." Llair.Program.pp program
       | Some file ->
           Out_channel.with_file file ~f:(fun oc ->
               let fs = Format.formatter_of_out_channel oc in
-              Format.fprintf fs "%a@." Llair.pp program )
+              Format.fprintf fs "%a@." Llair.Program.pp program )
   in
   command ~summary ~readme param
 

sledge/src/control.ml

@@ -385,7 +385,12 @@ module Make (Dom : Domain_intf.Dom) = struct
     exec_jump stk state block return
 
   let exec_term :
-      exec_opts -> Llair.t -> Stack.t -> Dom.t -> Llair.block -> Work.x =
+         exec_opts
+      -> Llair.program
+      -> Stack.t
+      -> Dom.t
+      -> Llair.block
+      -> Work.x =
    fun opts pgm stk state block ->
     [%Trace.info
       "@[<2>exec term@\n@[%a@]@\n%a@]" Dom.pp state Llair.Term.pp block.term] ;
@@ -456,7 +461,12 @@ module Make (Dom : Domain_intf.Dom) = struct
     Dom.exec_inst state inst |> Result.of_option ~error:(state, inst)
 
   let exec_block :
-      exec_opts -> Llair.t -> Stack.t -> Dom.t -> Llair.block -> Work.x =
+         exec_opts
+      -> Llair.program
+      -> Stack.t
+      -> Dom.t
+      -> Llair.block
+      -> Work.x =
    fun opts pgm stk state block ->
     [%Trace.info "exec block %%%s" block.lbl] ;
     match IArray.fold_result ~f:exec_inst ~init:state block.cmnd with
@@ -465,7 +475,7 @@ module Make (Dom : Domain_intf.Dom) = struct
         Report.invalid_access_inst (Dom.report_fmt_thunk state) inst ;
         Work.skip
 
-  let harness : exec_opts -> Llair.t -> (int -> Work.t) option =
+  let harness : exec_opts -> Llair.program -> (int -> Work.t) option =
    fun opts pgm ->
     List.find_map ~f:(Llair.Func.find pgm.functions) opts.entry_points
     |> function
@@ -481,7 +491,7 @@ module Make (Dom : Domain_intf.Dom) = struct
              entry)
     | _ -> None
 
-  let exec_pgm : exec_opts -> Llair.t -> unit =
+  let exec_pgm : exec_opts -> Llair.program -> unit =
    fun opts pgm ->
     match harness opts pgm with
     | Some work -> Work.run ~f:(exec_block opts pgm) (work opts.bound)

sledge/src/control.mli

@@ -15,6 +15,8 @@ type exec_opts =
   ; globals: Domain_used_globals.r }
 
 module Make (Dom : Domain_intf.Dom) : sig
-  val exec_pgm : exec_opts -> Llair.t -> unit
-  val compute_summaries : exec_opts -> Llair.t -> Dom.summary list Reg.Map.t
+  val exec_pgm : exec_opts -> Llair.program -> unit
+
+  val compute_summaries :
+    exec_opts -> Llair.program -> Dom.summary list Reg.Map.t
 end

sledge/src/llair/llair.ml

@@ -116,7 +116,7 @@ let equal_block x y = Int.equal x.sort_index y.sort_index
 
 type functions = func String.Map.t [@@deriving sexp_of]
 
-type t = {globals: Global.t iarray; functions: functions}
+type program = {globals: Global.t iarray; functions: functions}
 [@@deriving sexp_of]
 
 let pp_inst fs inst =
@@ -576,22 +576,26 @@ let set_derived_metadata functions =
   set_sort_indices tips_to_roots ;
   functions
 
-let invariant pgm =
-  let@ () = Invariant.invariant [%here] pgm [%sexp_of: t] in
-  assert (
-    not
-      (IArray.contains_dup pgm.globals ~compare:(fun g1 g2 ->
-           Reg.compare g1.Global.reg g2.Global.reg )) )
-
-let mk ~globals ~functions =
-  { globals= IArray.of_list_rev globals
-  ; functions= set_derived_metadata functions }
-  |> check invariant
-
-let pp fs {globals; functions} =
-  Format.fprintf fs "@[<v>@[%a@]@ @ @ @[%a@]@]"
-    (IArray.pp "@\n@\n" Global.pp_defn)
-    globals
-    (List.pp "@\n@\n" Func.pp)
-    ( String.Map.data functions
-    |> List.sort ~compare:(fun x y -> compare_block x.entry y.entry) )
+module Program = struct
+  type t = program
+
+  let invariant pgm =
+    let@ () = Invariant.invariant [%here] pgm [%sexp_of: program] in
+    assert (
+      not
+        (IArray.contains_dup pgm.globals ~compare:(fun g1 g2 ->
+             Reg.compare g1.Global.reg g2.Global.reg )) )
+
+  let mk ~globals ~functions =
+    { globals= IArray.of_list_rev globals
+    ; functions= set_derived_metadata functions }
+    |> check invariant
+
+  let pp fs {globals; functions} =
+    Format.fprintf fs "@[<v>@[%a@]@ @ @ @[%a@]@]"
+      (IArray.pp "@\n@\n" Global.pp_defn)
+      globals
+      (List.pp "@\n@\n" Func.pp)
+      ( String.Map.data functions
+      |> List.sort ~compare:(fun x y -> compare_block x.entry y.entry) )
+end

sledge/src/llair/llair.mli

@@ -95,16 +95,10 @@ and func = private
 
 type functions
 
-type t = private
+type program = private
   { globals: Global.t iarray  (** Global variable definitions. *)
   ; functions: functions  (** (Global) function definitions. *) }
 
-val pp : t pp
-
-include Invariant.S with type t := t
-
-val mk : globals:Global.t list -> functions:func list -> t
-
 module Inst : sig
   type t = inst
 
@@ -201,3 +195,13 @@ module Func : sig
   val is_undefined : func -> bool
   (** Holds of functions that are declared but not defined. *)
 end
+
+module Program : sig
+  type t = program
+
+  val pp : t pp
+
+  include Invariant.S with type t := t
+
+  val mk : globals:Global.t list -> functions:func list -> t
+end