[sledge] Fix coverage stats being too low due to clashes

Summary:
Instructions and terminators are not themselves unique, there can be
two instructions that compare equal in distinct blocks, and likewise
for terminators. Such clashes make the coverage statistics report
incorrectly low coverage. This diff fixes this by also considering the
parent blocks.

Reviewed By: jvillard

Differential Revision: D26250514

fbshipit-source-id: 93f916eab

sledge/src/control.ml

@@ -454,7 +454,7 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
    fun pgm stk state block ->
     [%Trace.info
       "@[<2>exec term@\n@[%a@]@\n%a@]" Dom.pp state Llair.Term.pp block.term] ;
-    Report.step_term block.term ;
+    Report.step_term block ;
     match block.term with
     | Switch {key; tbl; els} ->
         IArray.fold
@@ -491,12 +491,15 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
     | Throw {exc} -> exec_throw stk state block exc
     | Unreachable -> Work.skip
 
-  let exec_inst : Llair.inst -> Dom.t -> (Dom.t, Dom.t * Llair.inst) result
+  let exec_inst :
-      =
+         Llair.block
-   fun inst state ->
+      -> Llair.inst
+      -> Dom.t
+      -> (Dom.t, Dom.t * Llair.inst) result =
+   fun block inst state ->
     [%Trace.info
       "@[<2>exec inst@\n@[%a@]@\n%a@]" Dom.pp state Llair.Inst.pp inst] ;
-    Report.step_inst inst ;
+    Report.step_inst block inst ;
     Dom.exec_inst inst state
     |> function
     | Some state -> Result.Ok state | None -> Result.Error (state, inst)
@@ -513,7 +516,9 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
           block.parent.name )
     @@ fun () ->
     match
-      Iter.fold_result ~f:exec_inst (IArray.to_iter block.cmnd) state
+      Iter.fold_result ~f:(exec_inst block)
+        (IArray.to_iter block.cmnd)
+        state
     with
     | Ok state -> exec_term pgm stk state block
     | Error (state, inst) ->

sledge/src/llair/llair.ml

@@ -368,12 +368,11 @@ and dummy_func =
 (** Instructions *)
 
 module Inst = struct
-  module T = struct
   type t = inst [@@deriving compare, equal, hash, sexp]
-  end
 
-  include T
+  module Tbl = HashTable.Make (struct
-  module Tbl = HashTable.Make (T)
+    type t = block * inst [@@deriving equal, hash]
+  end)
 
   let pp = pp_inst
   let move ~reg_exps ~loc = Move {reg_exps; loc}
@@ -440,12 +439,7 @@ end
 (** Basic-Block Terminators *)
 
 module Term = struct
-  module T = struct
   type t = term [@@deriving compare, equal, hash, sexp_of]
-  end
-
-  include T
-  module Tbl = HashTable.Make (T)
 
   let pp = pp_term
 
@@ -532,6 +526,7 @@ module Block = struct
 
   include T
   module Map = Map.Make (T)
+  module Tbl = HashTable.Make (T)
 
   let pp = pp_block
 

sledge/src/llair/llair.mli

@@ -135,7 +135,7 @@ module Inst : sig
   val locals : inst -> Reg.Set.t
   val fold_exps : inst -> 's -> f:(Exp.t -> 's -> 's) -> 's
 
-  module Tbl : HashTable.S with type key := t
+  module Tbl : HashTable.S with type key := block * t
 end
 
 module Jump : sig
@@ -185,8 +185,6 @@ module Term : sig
   val throw : exc:Exp.t -> loc:Loc.t -> term
   val unreachable : term
   val loc : term -> Loc.t
-
-  module Tbl : HashTable.S with type key := t
 end
 
 module Block : sig
@@ -196,6 +194,7 @@ module Block : sig
   val mk : lbl:label -> cmnd:cmnd -> term:term -> block
 
   module Map : Map.S with type key := t
+  module Tbl : HashTable.S with type key := t
 end
 
 module Func : sig

sledge/src/report.ml

@@ -44,14 +44,14 @@ let solver_steps = ref 0
 let step_solver () = Int.incr solver_steps
 let steps = ref 0
 let hit_insts = Llair.Inst.Tbl.create ()
-let hit_terms = Llair.Term.Tbl.create ()
+let hit_terms = Llair.Block.Tbl.create ()
 
-let step_inst i =
+let step_inst b i =
-  Llair.Inst.Tbl.incr hit_insts i ;
+  Llair.Inst.Tbl.incr hit_insts (b, i) ;
   Int.incr steps
 
-let step_term t =
+let step_term b =
-  Llair.Term.Tbl.incr hit_terms t ;
+  Llair.Block.Tbl.incr hit_terms b ;
   Int.incr steps
 
 let bound = ref (-1)
@@ -170,7 +170,7 @@ let coverage (pgm : Llair.program) =
             n + IArray.length blk.cmnd + 1 ) )
   in
   let hit =
-    Llair.Inst.Tbl.length hit_insts + Llair.Term.Tbl.length hit_terms
+    Llair.Inst.Tbl.length hit_insts + Llair.Block.Tbl.length hit_terms
   in
   let fraction = Float.(of_int hit /. of_int size) in
   output

sledge/src/report.mli

@@ -9,8 +9,8 @@
 
 val init : ?append:bool -> string -> unit
 val step_solver : unit -> unit
-val step_inst : Llair.inst -> unit
+val step_inst : Llair.block -> Llair.inst -> unit
-val step_term : Llair.term -> unit
+val step_term : Llair.block -> unit
 val hit_bound : int -> unit
 val unknown_call : Llair.term -> unit
 val invalid_access_inst : (Format.formatter -> unit) -> Llair.inst -> unit