From 0587da1c51554ae781ca51aa22c10351762a145e Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 8 Feb 2021 13:10:59 -0800
Subject: [PATCH] [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      | 17 +++++++++++------
 sledge/src/llair/llair.ml  | 17 ++++++-----------
 sledge/src/llair/llair.mli |  5 ++---
 sledge/src/report.ml       | 12 ++++++------
 sledge/src/report.mli      |  4 ++--
 5 files changed, 27 insertions(+), 28 deletions(-)

diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 6288b6429..2ffc12acb 100644
--- a/sledge/src/control.ml
+++ b/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
-      =
-   fun inst state ->
+  let exec_inst :
+         Llair.block
+      -> 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) ->
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index 40f31d124..e2a28d456 100644
--- a/sledge/src/llair/llair.ml
+++ b/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
+  type t = inst [@@deriving compare, equal, hash, sexp]
 
-  include T
-  module Tbl = HashTable.Make (T)
+  module Tbl = HashTable.Make (struct
+    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)
+  type t = term [@@deriving compare, equal, hash, sexp_of]
 
   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
 
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index a3940253b..9103f8ab9 100644
--- a/sledge/src/llair/llair.mli
+++ b/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
diff --git a/sledge/src/report.ml b/sledge/src/report.ml
index a30f9f16a..f01f8746f 100644
--- a/sledge/src/report.ml
+++ b/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 =
-  Llair.Inst.Tbl.incr hit_insts i ;
+let step_inst b i =
+  Llair.Inst.Tbl.incr hit_insts (b, i) ;
   Int.incr steps
 
-let step_term t =
-  Llair.Term.Tbl.incr hit_terms t ;
+let step_term b =
+  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
diff --git a/sledge/src/report.mli b/sledge/src/report.mli
index 3a9aa1d9b..bf2395156 100644
--- a/sledge/src/report.mli
+++ b/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_term : Llair.term -> unit
+val step_inst : Llair.block -> Llair.inst -> 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